Loading [MathJax]/jax/output/HTML-CSS/jax.js

Memory Consistency Constraints

Handling the Constraints using Sorting Technique

For an array of execution traces tr=(addri,ti,opi,vali)ni=1, one known method to prove the correctness of tr is to use the sorting technique, which can be found in [FKLO0W21]. At a high level, we create a new array tr, which is a sorted version of tr. The elements of tr are sorted in increasing order by its address, then time log. We prove that the elements of tr satisfy some specified constraints, then prove that tr and tr are permutations of each other.

First, let us delve into the details of the constraints in tr. The constraints are as follows:

{timei<timei+1,(opi+1=1)(addri=addri+1),(addri<addri+1)((addri=addri+1)(timei<timei+1)),(opi+1=1)(vali=vali+1)(addriaddri+1).

Let us explain the above constraints: Recall that in memory consistency, we simply need to prove that, for each memory cell, the value of the current step is equal to the value in the last step it was written. With this idea, we could sort the trace by their address first, then time and check them via the constraint (addri<addri+1)((addri=addri+1)(timeitimei+1)). In this way, we can divide the array into consecutive ''blocks'' where each block contains the traces with the same address. In each block and each trace of it, we consider the time when the value is written (determined by val and op). We see that, if the value is written in the current step (op=1), then there is nothing to consider because we are writing a new value. Otherwise (op=0) meaning that we are reading from the cell, then the value val must be equal to the value of the previous trace in the block, and this can be captured by the constraint (opi+1=1)(vali=vali+1)(addriaddri+1).. Moreover, we need to ensure that the first time we access a memory cell, then the operation must be WRITE, which can be constrained by (opi+1=1)(addri=addri+1), meaning that in every first trace in each block, the opcode of the trace must be 1. Finally, we need the original array to be sorted in ascending time, which can be captured via the constraint timeitimei+1. Thus, these constraints together are sufficient to check the consistency of the memory.

Integrating Halo2

In this Section, we give a brief overview of handling constraints using Halo2. For readers who are new to Halo2, we refer to halo2. With the execution trace, we define our witness table where each row has the following config:

(addr,time,op,val,addr,dif,inv,time,op,val)

and the constraints (each must be equal to 0) are rewritten in Halo2 as follows:

{C(timei,timei+1)=0,(opi+11)(addriaddri+1)=0,C(addri||timei,addri+1||timei+1)=0,(opi+11)(vali+1vali)((addri+1addri)invi+11)=0.

In the constraints above, we denote C to be the expression such that C(a,b)=0 iff a<b. The idea for construction this expression can be found in here. At a high level, we parse a and b into 256-bit chunks (ai) and (bi) for i={1,2,32} and look for the smallest j such that ajbj. Hence, it is equivalent to prove that (bjaj){1,,255} and ai=bi for all 1ij1. With this, the expression C can be written in high level as C=lookup(bjaj,{1,,255})+β(j1i=1(biai)αi) where α,β are random challenges generated by verifier, and lookup(c,{1,,255}) is an expression that returns 0 if and only if c{1,2,255}. Note that by Schwartz-Zippel lemma, we can see that if ab, then the expression C above does not return 0 with overwhelming probability. In addition, for proving that tr and tr are permutation of each other, we simply use the shuffle API from here

Finally, with the constraints above, we could support proving memory consistency using Halo2. Our implementation for this can be found here.