Lookup Argument in Nova tricks: permutation checking without re-ordering

Changed History

Requirements

• Applications: memory read/write in VM, bitwise operations, range check in folding scheme.
• Folding pattern: lookup argument must able to de-couple and amortized into each rounds.
• Cost: The NIFS.P/V cost for lookup argument in folding must be as low as possible. Costly operation must be able to deferrable to the end with one SNARK.
• Rolling accumulation without access re-ordering, since any re-ordering is not friendly to folding to memorize

Proposed Methdology

Below proposed a lookup argument to achieve constant time prover complexity, for per lookup cost is just few fields operations, and per increamental folding just ONE random oracle hash without any EC group operations! Giving m lookups happend in foldings rounds with lookup table \(T\) and size \(|T|\), the cost in overall folding process is just \(\Theta(m) \times \mathbb{F}\), agnostic to lookup table size or rounds of foldings! Deferring the lookup checks via STOA tricks: sumcheck on grand product, in the end prover just incur SNARK once, with prover cost \(O(|T|)\) (only once) and proof size \(O(log(|T|))\).

Memory-checking via permutation-checking, without re-ordering

Snipped from Jolt paper Appendix B.3 Memory-checking via permutation-checking, without re-ordering.

It leverages a skill called offline memory checking from paper BEG+91

The idea is prove RS, WS are permutation of each others at the end after dust settles.

RS => Read-Set, WS => Write-Set

• at begining, WS fill with N initial value tuples (addr, value, 0), where \(N=|T|\) is the table size, and T is the lookup table initial value

• for every read/write

  • read operation: (addr, v, c) append to RS set, along with write append (addr, v, c+1) to WS set. v is value read from memory.
  • write operation: said a write value is v', and v is value before write. Firstly (addr, v, c) append to RS set, along with write append (addr, v', max(c, global_counter) + 1) to WS set. If there are multiple read/write the flow is as usual.

    introduce global_counter to avoid out-of-order read. For more detail see Jolt paper pp.42 Overview of Spice’s memory-checking argument

  • If there are multiple reads/writes the flow then this process just repeat as-is.
  • c is a counter for each memory entry.

• At the end, read through whole lookup table and apend to WS set

• read/write consistent iff WS and RS are permutation with each others

Recognize Folding Pattern in Grand Product Terms

Take grand product expression from Jolt

Expression (12) RHS \(T[i]\) should be \(T'[i]\), represents the final state of tables. \(T'[i]\) and \(c_{m+i}\) are non-deterministics input from prover.

m represent number of read/write accesss. N represent overall memory space. \(b_i\) means memory address or table index, \(a_i\) means value, \(c_i\) means counter. In other word, \(T[b_i] = a_i\) with counter \(c_i\).

Proof of completeness & knowledge soundness analysis

For Equation (12), define

\(LHS = \prod_{i=0}^{m-1} (\alpha - (b_{i} + \gamma \times a_{i} + \gamma^2 \times c_i))\)

For Equation (13), define

\(RHS = \prod_{i=0}^{m-1} (\alpha - (b_{i} + \gamma \times a_{i} + \gamma^2 \times (c_i + 1))\)

And \(LHS, RHS \in F\)

RHS & LHS both demonstrate nice pattern to be able to folding by purely F-arithmetics. Giving there are k round of foldings, each round just contribute \(m_1, m_2, ...,\) and satisfy \(m = m_1 + m_2 + ... + m_k\).
\(m_i\) can be 0 if at that round there is no lookup operation.

During each round of folding:

• Address \(b_i\) constrained by step circuit opcode. If its for memory load/store, its constrained by instruction itself. If it's for range check, then address can be witness from prover. \(a_i\), \(c_i\) are aux witness from prover.
• Most interesting is in challenge \(\alpha\) and \(\gamma\). We trust \(\alpha\) and \(\gamma\) as aux input from prover starting at round 0, and defer verification of challenge in the end of folding. In each folding, we assure \(\alpha\) and \(\gamma\) are consistent across each round (E.g bypass them in Nova state)
• challenge verification: It verified in the end of folding. To make it work, each round there is mechanism to update some intemediate variable \(\alpha_i\), \(\gamma_i\), and at the end, IVC.verify \(\alpha == \alpha_n\) and \(\gamma == \gamma_n\), for \(\alpha\) and \(\gamma\) are pass from first round. This is a variant of Fiat Shamir, but working in a rolling hash way.

  idea background come from https://zkresear.ch/t/folding-endgame/106. prover need to compute \(\alpha\) and \(\gamma\) in advance before kick off folding.

Here share a Fiat-Shamir variant for non-iteractive incremental computation

• logic to update \(\alpha_i\)
  • incremental i=0: \(\alpha_0 = hash(b_0, a_0, c_0, 0)\)
  • incremental i=1: \(\alpha_1 = hash(b_1, a_1, c_1, \alpha_0)\)
  • incremental i=2: \(\alpha_2 = hash(b_2, a_2, c_2, \alpha_1)\)
  • …
• \(\gamma_i\)
  • incremental i=0: \(\gamma_0 = hash(b_0, a_0, c_0, 1)\)
  • incremental i=1: \(\gamma_1 = hash(b_1, a_1, c_1, \gamma_0)\)
  • incremental i=2: \(\gamma_2 = hash(b_2, a_2, c_2, \gamma_1)\)
  • …

Final IVC verifier need to verify in circuit to assure \(\alpha == \alpha_n\) and \(\gamma == \gamma_n\), where \(\alpha, \alpha_n, \gamma , \gamma_n \in F\). \(\alpha\) and \(\gamma\) are aux from prover on round 0.

• in each round of folding, if there are read(s) or write(s), update RHS & LHS with challenge \(\alpha\) and \(\gamma\), which is an pure F-arithmetics, no group operation. "update" is implemented in folding augmented circuit. In Nova term, F augmented circuit.

15-Sep-2023 Updated: first version we set \(\alpha == \gamma\) so we just need to have 1 random oracle hash for challenge.

Grand product argument

recap

For LHS of equation (12) and RHS of equation (13) we can collect them in the end of folding. So the final formula is like

\[ F_{LHS} \times SomeGrandProduct_l(T) = F_{RHS} \times SomeGrandProduct_r(T) \]

where

\[ F_{LHS}, F_{RHS} \in F \]

and accumulated in folding.

Then we can apply any grandproduct argument like via
Quarks: Quadruple-efficient transparent zkSNARKs pp.17 A new transparent SNARK for proving grand product relations

Lemma 5.1 \(P = \prod_{x∈{0,1}^{log(m)}}^{m-1}v(x)\) if and only if there exists a multilinear polynomial f in \(log(m) + 1\) variables such that f(1, . . . , 1, 0) = P, and \(∀x ∈ {\{0,1\}^{log(m)}}\) , the following hold: f(0, x) = v(x), f(1, x) = f(x, 0) · f(x, 1)

Define \(v_{lhs}(X) = (\alpha - (i + \gamma \times T(X) + \gamma^2 \times c(X))\). Giving random some verifier selected random \(k\), \(l\) Prover need to prove there exist f with folloing holds

• \(0 = \sum_{x ∈ {\{0,1\}^{log(m)}}} eq^{}(x, k ) · (f(1, x) − f(x, 0) · f(x, 1))\)
• \(f(0, l) = v_{lhs}(l) = (\alpha - (i + \gamma \times T(l) + \gamma^2 \times c(l))\)
• \(f(1, ...., 0) = GrandProductF_{lhs} \in F\)

Prover & Verifier run sum-check protocol to prove claim 1 by evaluation of G at some point \(r \in \mathbb{F}\). Also prover convince verifier the correctness of commitment f(0,r), f(1,r), f(r, 0), f(r, 1) and f(1, . . . , 1, 0). With f(1, . . . , 1, 0), prover able to obtain \(GrandProduct_{lhs}\)

Similar process apply on \(v_{rhs}(X)\) as well

Verifier verify:

\(F_{LHS} \times GrandProduct_{lhs} = F_{RHS} \times GrandProduct_{rhs}\)

We can further apply sparse vector tricks to optimise commitment T (table T likely to be sparse). We can implement grand product augment verification in IVC.verify circuit.

Complexity

• F-arithmetics in each round of folding: O(#numbers_of_memory_rw \(\times\) fields_arithmetics). No group or EC operation.
• Final sum-check protocol for grand product: prover cost linear time to table size O(|T|) with prove size O(log(|T|))

Application

• Memory read/write of VM
• Bit operation
• Range lookup
• any proof-carrying data between folding.