Lookup Argument in Nova tricks: permutation checking without re-ordering
=======
### Changed History

| Date | Memo | Editor|
| -------------- | ------------------|------------------|
| 2023-09-19 | address few typo and comments | @sungmingwu |
| 2023-09-16 | optimise global challenge and simple cost summary | @sungmingwu |
| Aug 2023 | first version | @sungmingwu |

### 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](https://eprint.iacr.org/2023/1217) paper `Appendix B.3 Memory-checking via permutation-checking, without re-ordering.`

It leverages a skill called offline memory checking from paper [BEG+91](https://www.cs.ubc.ca/~will/papers/memcheck.pdf)

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](https://eprint.iacr.org/2023/1217) 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.

| Prover work | NIFS Verifier work|
| -------- | -------- |
| $\Theta(m_i) \times \mathbb{F}$, $m_i$ is the number of lookup in i folding round| 1 random oracle hash to compute challenge||

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](https://eprint.iacr.org/2020/1275.pdf) `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.