How state proof/range-check proof works in Ceno zkVM
============

### lookup argument: Logup

The LogUp formula in summary like this
Where
- LHS is the witness vector `W` to be lookup and $W(j) = W_j$, for $j \in [1, l]$
- RHS is the target table $T(x)$ with $T(i) = T_i$, for $i \in [1, i]$
- $i << j$ range check scenario
- $M(x)$ is the couting for the respective lookup record, for $M(i) = m_i$
> This is called Indexed Lookup

A random challenge `alpha` derived for `X`, and prover witness $W(x), M(x)$

There is a nice property, for the $W(X)$ and $T(X)$ can be concat as a super vector/table. The tricks is by make $W(X)$ and $T(X)$ as a rlc result, by deriving another challenge `beta`, with define constant as table derivative.

For example, we can concat u5 and u16 table as this way

T := [
    // U5 Table
    ROMType::U5 * beta^0 + 0 * beta^1,
    ROMType::U5 * beta^0 + 1 * beta^1,
    ...
    ROMType::U5 * beta^0 + (max_u5 - 1) * beta^1,
    // U16 table
    ROMType::U16 * beta^0 + 0 * beta^1,
    ROMType::U16 * beta^0 + 1 * beta^1,
    ...
    ROMType::U16 * beta^0 + (max_u16 - 1) * beta^1,
]

And the similar RLC tricks applid $W(X)$ so we make literally treat there is a huge table T for `Indexed Lookup`

### GKR sumcheck for fraction sum proof

refer: https://eprint.iacr.org/2023/1284.pdf


it can be view as

$$
\frac{p(1)}{q(1)} + \frac{p(2)}{q(2)} + ... \frac{p(N)}{q(N)} = 0
$$

- we can select any pair of them in any order, e.g. 2 consecutive, or divide into 2 equal sub slice and point-wise sum
- from math we know to sum 2 frac
$$
\frac{p(1)}{q(1)} + \frac{p(2)}{q(2)} = \frac{p(1) \times q(2) + p(2) \times q(1)}{q(1) \times q(2)}
$$

So we can design GKR circuit to layer by layer reduce $p(x), q(x)$ half size from k+1 -> k

and finally in output layer we just check


for $q_0 > 0$ and $p_0 = 0$ the

### GKR logup and codebase

Recap

Both left hand side & right hand side are exposing pattern for fraction sum.

For example, in LHS, $p(x)$ is constant vector 1, and $q(x)$ is witness vector to be lookup.

In practice, we concat all expression to be lookup into a huge vector


notes that concated vector size will be > column vector. This can't be achieved in traditional plonkish without GKR. GKR + sumcheck will assure source + flatten vector are well form.

The concated vector is the LHS $q(x)$, and $p(x)$ is constant vector 1. Then we can use GKR+Logup to reduce huge concated vector half each time and check final result in output layer


The RHS table part $p(x) = m(x)$ and $q(x) = T(x)$. This part is agnostic for any opcode, so we can have a separate GKR + sumcheck to prove it. At the end, we just collect output layer from RHS and LHS and check they are equal, with both demoninato > 0.

### Logup application in zkVM
- range check
- bitwise operation, e.g. z = xor8(x, y), where x, y are 8 bit

### Padding to Power of 2


There are 2 option for padding
1. set 0 on LHS numerator
2. or set $w_i$ = 0 in LHS denominator, and on RHS prover witness $M(x)$ for $m_i$ counting on $t_i$ = 0

We choose option 2 for constant vector p(x) is friendly to deal with in verifier.

### Another variant: set equality check
Logup is optimal when


when j >> i.

In zkVM, we have another kind of set equality: memory offline check protocol, such that giving R, W, at the end we check $R$ ?= $W$. Giving a global state in/out case, we will append record [pc, ts] to $R$ and [pc_next, ts_next] to $W$ set. You can imagine at the end $|R|$ == $|W|$.

We can use logup to prove $R$ == $W$, via treat $R$ and $W$ in LHS/RHS demominator of Logup, and make $m_i$ also be constant vector 1. However we can have another choice by prove it via product arguments


> $r$ challenge can be alpha, and $v_i$ can be rlc from beta, similar tricks as logup

Product argument is good in this case due to
- LHS set and RHS set are equal, so we benefit less from Logup
- For Logup, in GKR when do fraction sum we need 3 multiplication $p1 \times q2$, $p2 \times q1$, $q1 \times q2$ and 1 sum $p1 \times q2 + p2 \times q1$ vs 1 multiplication in product check.