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.