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.