Offline Memory Checking

by Blum at al. (1994)

Sources:

• Explanation (YouTube)
• Unlocking the lookup singularity with Lasso

Read-only memory

The problem they tried to solve is to force an untrusted memory to prove it worked correctly, with very low space requirements of the verifier.

The verifier maintains two sets, which can be compressed and updated incrementally via permutation-invariant fingerprinting (see Permutation Check via Product Check):

• Read Set: The tuples $(addres{s}_i,valu{e}_i,coun{t}_i)$ returned by the prover
• Write Set: $(addres{s}_i,valu{e}_i,coun{t}_i)$ written to memory

Then, the verifier behaves as follows:

• At the beginning of the execution, they write for each address $a_i$ the tuple $(a_i,0,0)$ (or some other initial value)
• Each read returning $(a_i,v_i,c_i)$ is followed by a write of $(a_i,v_i,c_i+1)$
• At the end of the execution, the verifier reads all addresses

If and only if the prover is honest, the read and write multi-sets will be equal.

Application: Indexed Lookup

Source: Unlocking the lookup singularity with Lasso

Suppose we have:

• A multi-linear extension $t:{\mathbb{F}}^{\log M}\to \mathbb{F}$ of some table (i.e., read-only memory)
• A multi-linear extension $a:{\mathbb{F}}^{\log m}\to \mathbb{F}$ of addresses
• A multi-linear extension $v:{\mathbb{F}}^{\log m}\to \mathbb{F}$ of values

We want to show that:

$$\forall {j\in \{0,1\}}^{\log m}:v(j)=t(\mathtt{bits}(a(j)))$$

where $\mathtt{bits}:\mathbb{F}\to {\mathbb{F}}^{\log N}$ is the function that maps a field element to its bit representation.

We can show this is the case by simulating the offline memory verifier in a SNARK.

Specifically, the prover commits to two polynomials, $c_{read}:{\mathbb{F}}^{\log m}\to \mathbb{F}$ and $c_{final}:{\mathbb{F}}^{\log M}\to \mathbb{F}$, containing the counts returned by the offline memory prover for the “normal” and final read operations.

The memory operations were performed correctly if $RS=WS$ where:

$$\begin{array}{c}\begin{array}{rl}RS=& \{(a(j),v(j),c_{read}(j)):j\in \{0,1{\}}^{\log m}\}\\ & \cup \{(to\_field(j),t(j),c_{final}(j)):j\in \{0,1{\}}^{\log M}\}\end{array}\end{array}$$ $$\begin{array}{c}\begin{array}{rl}WS=& \{(to\_field(j),t(j),0):j\in \{0,1{\}}^{\log M}\}\\ & \cup \{(a(j),v(j),c_{read}(j)+1):j\in \{0,1{\}}^{\log m}\}\end{array}\end{array}$$

where $to\_field$ is also a multi-linear polynomial:

$$to\_field(x_1,...,x_{\log M}):=\sum _{i=1}^{\log M}{2}^{i-1}\cdot x_i$$

The two multi-sets can be shown to be equal using the Permutation Check via Product Check! In particular, the grand product can be computed using a layered arithmetic circuit of depth $O(\log m+\log M)$ and proven using GKR.

Read-write memory

The original paper actually describes a read-write memory which is slightly more complex:

• As described above, all memory cells are initialized with some value at time step $t=0$
• For each memory write of value $v_{cur}$ to address $addr$ at time $t_{cur}$:
  • The prover provides $t_{prev}$ and $v_{prev}$
  • The verifier asserts that $t_{prev}<t_{cur}$
  • The tuple $(addr,t_{prev},v_{prev})$ is added to the read set
  • The tuple $(addr,t_{cur},v_{cur})$ is added to the write set
• A memory read works the same, but with $v_{prev}=v_{cur}$