An Introduction to Jolt: Core Proofs and Protocol Frameworks
Jolt: lookup-singularity SNARKs and the protocol stack around them.
TLDR：
- Type: SNARK ZK proof system.
- Advantages: Utilizes lookup tables for a simplified proving system, and is friendly to ZKVM.
- Current Status: Still maturing; key components like the continuation feature are in development.
- Foundation: Based on lookup table arguments.
- Core Proofs: Byte-code memory checking, Instruction lookup proofs, Read-write memory proofs, R1CS (Rank-1 Constraint System).
0. Purpose
Our aim is to introduce Jolt (Just one lookup table), a SNARK ZK proof system based on lookup table arguments.
We will present its strengths, the underlying protocol and the core proof process,
Finally, we will introduce its shortcomings and speculate on its possible directions of development.
1. Jolt’s Flow, Advantages, Status and Direction
1.1 Flow
Jolt is a SNARK ZK proof system based on table lookup argument and RISCV instruction set. Its input is the client’s execution program (such as Rust or C implementation) and the input of the execution program itself. Jolt believes that the execution of instructions is equivalent to table lookup operations.
Jolt runs the execution program under the given input and proves that the execution program is correct without revealing the data generated during the execution process.
1. Compile the execution program into assembly code of the RISCV instruction set;
2. Construct the lookup table corresponding to all instructions in the RISCV instruction set;
3. For the given execution program input, execute the compiled RISCV instructions one by one, and record the input, output, RAM read and write behavior of each instruction, register access behavior, record the input and output of the lookup table of each instruction, and record the input and output of the execution program itself.
4. Use the data recorded during the execution of the instruction to run the underlying proof protocol and complete the proof，and finally get the transcript.
1.2 Advantages
From the above process, we can see that Jolt has the following advantages:
1. Security analysis and auditing are relatively easy.
Jolt proves the execution of instructions through the table lookup operation of the instructions, and the lookup table itself and the table lookup operation itself are relatively simple, thus avoiding a large number of arithmetic operations.
It is more difficult to analyze and review the security of arithmetic operation proofs, such as STARK and RISC0, because they involve a large number of complex mathematical theorem proofs (see the relevant papers of STARK).
2. The underlying protocol (sum-check, introduced below) that the proof system relies on is relatively simple and requires very little mathematical knowledge to understand. Simple means low maintenance cost and is not prone to bugs;
3. The amount of committed data is small (commitment). Each executed instruction only needs to commit 5 finite field elements, while RISC0 needs to commit 34 finite field elements (from Jolt paper). A small commitment means a smaller transcript, that is, less data is sent to the verifier;
4. Convenient to support other ISAs or more RISCV instructions. If you need to support different RISCV instructions, you only need to increase the lookup table of the instruction.
1.3 Development status
Jolt is relatively new (the alpha version was not implemented until April 2024), and there are the following problems:
A. The maturity of the project implementation is not high, as shown in the figure below, many tasks have not been completed;
B. Recursion is not supported, and the execution process of the program is divided into multiple steps for proof. If recursion is not supported, it will take a long time to prove the program with a long execution process;
C. The underlying protocol of Jolt currently is simple, but not suitable for hardware parallel computation.
1.4 Development direction
A. In the currently implemented version of Jolt, all calculations in the proof process are done on the finite field F, that is, the coefficients of all polynomials involved belongs to F, and 256 bits are required to represent each coefficient.
Why 256 bits? Because it involves security issues. The current security error of sum-check ε = O(1 / |F|) = O(1 / 2²⁵⁶), where |F| is the number of elements in F. Without reducing security, is there a finite field whose elements occupy a relatively small memory ?
B. Recursion support, solve the problem of long proof time when the program execution or calculation process is long ?
C. The underlying protocol it relies on is sum-check, which is not suitable for parallel. Can a similar protocol be found to improve parallelism ?
D. Jolt requires memory checking in many places. It is implemented through grand_product. Is there a more efficient memory checking algorithm ?
Below we will introduce the definitions and core proof process of Jolt.
2. Definitions
Because Jolt is a SNARK ZK proof system based on lookup table argument, in order to introduce Jolt, it is inevitable that we need to give the definitions of some terms, such as SNARK ZK and lookup table argument system.
For the sake of space, we just briefly introduce these terms without making strict and rigorous mathematical definitions.
Definition 1: SNARK ZK proof system
We are concerned with the prover and the verifier, the prover in order to prove to the verifier that a statement or a computational procedure or the execution of a program is correct. SNARK refers to:
<S: succinct> i.e., it is short, and the cost (in terms of time and memory) of the prover to prove a statement is correct is small. A text file, the transcript, is produced after the proof is complete, and when the verifier get the transcript. The cost of the verifier to verify that the transcript produced by the prover is correct(which is equivalent to the proposition being correct) is also small;
<N: non-interactive> i.e., non-interactive, we want the proof process to be free of two-way communication between the prover and the verifier, because communication between the two sides introduces time and cost.
<ARK: argument of knowledge> i.e., an argument of knowledge system where the prover does know the details of the statement or the details of the computation. And does know the details of the computational process, which we call witness;
<ZK: zero knowledge> i.e., zero knowledge, where the result of the proof produced by the prover does not contain any information other than the statement itself. Or the verifier, after getting the transcript, will not get any information other than the correctness of the proposition.
Also SNARK ZK, the following conditions must be satisfied:
<completeness> For an honest proof party, if the statement or the proof computational procedure is correct, then the verifying party must accept that the proposition is correct;
<soundness> Security, i.e., if the proposition or procedure is false, then the probability ε that the verifier accepts the statement as correct is very small, e.g. ε<1/(2¹²⁸). The analysis and mathematical proof of security is the snark’s core and the most difficult aspect of many ZK systems.
Definition 2: Lookup table argument
Given a lookup table T∈F^N and w = (a, b), where, <F> a finite field (similar to the real number field R, with arithmetic operations such as addition defined, but the number of its elements is finite); <N> the size of the lookup table; <a> an m-dimensional vector on F, as the input of the lookup table; <b> an m-dimensional vector on F, as the output of the lookup table.
Then, the lookup table argument refers to a SNARK ZK system, which proves that b[i] = T[a[i]] without revealing vector a and vector b to the prover, that is, it proves that the lookup behavior is honest or correct.
Definition 3: Multilinear polynomial
A multivariate polynomial _f(x_1,x_2, …, x_n) over a finite field F is called linear. If the degree of any unknown variable x_i: deg(x_i)≤1, in which x_1, …, x_n∈F and the coefficients of _f belong to F.
Note that here we define polynomials as polynomial functions (although this is not the strict mathematical definition, but it is good for us). For example, the _eq polynomial, which is extremely important in ZK.
Definition 4: _eq polynomial
For any function f: {0,1}^n → F, the MLE is a multilinear polynomial _f: Fn → F, such that _f(x) = f(x), when x ∈ {0,1}^n ⊆ Fn, that is, _f is a function extension of f and _f is a multilinear polynomial.
Definition 6: Sum-check Protocol
Jolt used the sum-check protocol in many places in the proof.
The purpose of sum-check is to prove that the following equation holds:
Where g is a v-variate polynomial g: Fv → F, and F is a finite field. We need the prover to prove that the equation is true without revealing the polynomial coefficients of g. From the above equation, we can see that the right side of the equation is actually the sum of the function values of the polynomial on all vertices of the “hypercube”, that is, sum-check.
Prover: There are v rounds in total, and the proof process is as follows:
For j = round_1, …, round_v:
A. The prover calculates the coefficients of the univariate polynomial Gj:
B. Add the coefficients of Gj to the end of the current transcript;
C. The prover uses the generated transcript as input to generate a random challenge value r_j;
D. Calculate the coefficients of the multivariate polynomial g(r_1, …, r_j, x_j+1, …, x_v).
Verifier: After getting the transcript, find the corresponding place of the sum-check, take out each univariate polynomial Gj,
For j=round_1, …, round_v:
Check whether Gj(0) + Gj(1) == Gj-1(r_j-1) ?
If they are equal, accept that the sum-check is correct,
Otherwise, consider that the sum-check is wrong.
(Note that for the sake of simplicity, many details are omitted here. Please refer to the relevant papers and codes for details).
Why sum-check?
1. Very useful. Sum-check seems to be just summing, but in fact we can use it to prove a variety of problems. For example, the proof of the legality of memory access mentioned below; For example, proving that the constraints between the various steps in the calculation process are satisfied;
2. The proof time is short (single thread);
3. The theory is very simple.
Why MLE?
From A and B in the above proof process, the number of coefficients of the univariate polynomial Gj saved in the transcript is equal to the degree of the variable x_j of g. In practical use, we hope that the degree of the variable in g is as small as possible, that is, it consists of multiple MLEs.
Why is sum-check not highly parallel?
From the proof process of sum-check, we can see that each round of the proof is serial computing. Due to the existence of the random challenge value r_j, multiple rounds cannot be calculated simultaneously, that is, round_j depends on r_j, and r_j depends on the calculation result of round_j-1.
So far, we have introduced most of the foundation needed for the Jolt proof process. Next, we will introduce the core proof process of Jolt.
3. The core process of Jolt
As we said before, our goal is to prove the correctness of a program execution or calculation process. That is, the prover will execute the program to be proved (the program is implemented by rust or c), and then prove that the execution process is correct.
To this end, Jolt first compiles the program into the RISCV instructions to get byte-code;
Get Computation Frontier’s stories in your inbox
Join Medium for free to get updates from this writer.Subscribe
Then, given the input, Jolt executes the instructions in the byte-code step by step, and records the reading of the byte-code (such as the number of times), the input and output of each instruction, the reading and writing of RAM/registers, and records the output after querying the corresponding lookup table using the input of each instruction.
Using the information obtained from the above records, the core proof steps in Jolt are mainly the following 4 steps:
<Byte-code prove memory checking> proves that reading each instruction, that is, the reading behavior of byte-code is correct;
<Instruction Lookups Proof> proves that the execution of each instruction is correct, implemented through lookup argument;
<Read Write Memory Proof> proves that the behavior of each instruction accessing ram and registers is correct;
<R1CS proof> proves that the constraints between instructions are satisfied, such as the output of the i step instruction is equal to the input of the i+1 step instruction.
The proof process is shown in the figure below:
We will now analyze the proof process and memory access of the above four steps in detail.
3.1 Core proof step 1: byte-code memory checking proof
3.1.1 Why byte-code memory checking proof?
Note that our goal is to prove the correctness of a program execution or calculation process, that is, the prover will execute the program to be proved and then prove that the execution process is correct.
First the client program is compiled to elf file. Then the elf file is loaded into the memory, byte-code is obtained. Jolt vm will execute the byte-code. During the execution process, the byte-code needs to be read to obtain the execution instructions. The purpose of byte-code prove is to ensure that the reading process of byte-code is correct.
3.1.2 Principle of byte-code memory checking proof
Byte-code proof is actually the proof of memory reading behavior, that is, memory_checking.
In Jolt, the problem of proving whether the memory reading behavior is correct is converted into the following problem of whether the product of all elements in two sets is equal, that is, constructing sets A and B, and proving whether the product of all elements in A is equal to the product of all elements in set B.
How to construct sets A and B? Consider byte-code as a series of consecutive memory addresses and values, such as:
Construct the multi-set byte-code = { (0, v_0), (1, v_1), …, (n, v_n) },
where <n> is the size of the memory occupied by the byte-code, and <0, v_0> means that the value of the byte-code address 0 is v_0.
By using the reading of byte-code recorded during the execution of each instruction, we the number of times each address is read after the program is completed, that is, we get: multi-set final = { (0, v_0, t_0), (1, v_1, t_1), …, (n, v_n, t_n) },
At the same time, we construct the multi-set init = { (0, v_0, 0) , (1, v_1, 0) , …, (n, v_n, 0) },
where: <n> The size of the memory occupied by the byte-code; <0, v_0, t_0> means that after the execution of the program is finished, the value of byte-code address 0 is v_0, and the total number of times that the address is accessed is t_0.
We then construct multi-set read and multi-set write:
multi-set read = { (a_0, v_a_0, t_0) , …, (a_i, v_a_i, t_i) , …, (a_m, v_a_m, t_m) },
At the same time, we construct: multi-set write = { (a_0, v_a_0, t_0+1), …, (a_i, v_a_i, t_i+1), …, (a_m, v_a_m, t_m+1) },
where: <m> is the total number of instructions executed, <a_i, v_a_i, t_i> means that the address of the byte-code read by the i step instruction is a_i, the value is v_a_i, t_i is the number of times the address is read when the i step instruction is reached.
Finally, we get the set A = init ∪ write, and the set B = read ∪ final.
Then there is a mathematical theorem: the reading behavior of byte-code is correct if and only if A = B.
How to prove A = B ? Use sum-check. For the specific derivation process and details, please refer to the Jolt paper.
The figure below shows byte-code’s proof process. The prove_grand_product in the figure is calculating the elements of the multi-set A, B and proving A = B.
3.2 Core Proof Step 2: Instruction Lookups Proof
3.2.1 Why Instruction Lookups Proof ?
Note that our goal is to prove the correctness of a program execution or calculation process, that is, the prover will execute the program to be proved and then prove that the execution process is correct.
First the client program is compiled to elf file. Then the elf file is loaded into the memory, byte-code is obtained. Jolt vm will execute each instruction one by one. The purpose of Instruction Lookups Proof is to ensure that the execution of each instruction is correct.
Proving that the execution of each instruction is correct is achieved through the lookup argument; we need to ensure that the result of each instruction is equal to the result of the table lookup operation. At the same time, because the table lookup operation also involves access to the lookup table, memory checking similar to byte-code proof is also required.
3.2.2 Instruction Lookups Proof Proof Principle
A. The ISA instruction set consists of many instructions. When any instruction f is executed, we can treat it as a table lookup operation;
B. Since the input of f is generally 32 or 64 bits, if a simple table lookup is implemented, the lookup table of f will be very large. To reduce the size of the lookup table, we divide the lookup table into multiple sub-tables.
We divide the input into multiple chunks, one chunk corresponds to one sub-table. For example, for the “and instruction”, the input x and y, assuming a 32-bit word length, cut the binary numbers of x and y into 4 parts respectively, and get x=(x3,x2,x1,x0) y=(y3,y2,y1,y0), then x3|x3, x2|y2, x1|y1, x0|y0 are called 4 chunks, as the input of the sub-table; then, for the and instruction, in a naive implementation, the table size is 2⁶⁴; and after being cut into sub-tables, the sub-table size is 2¹⁶. This is the core contribution of Jolt.
C. For some complex instructions f’, we need multiple sub-table lookup operations and combine multiple lookup results to implement f’;
D. At this time, the execution of instruction f will correspond to the query operation and combination operation of the f sub-tables. To prove the correctness of instruction f, that is, to prove that the result of instruction f execution output(f) is equal to the result of f sub-table lookup operation and combined operation;
How to prove that output(f) is equal to the result of f subtable query and combined operation?
That is, primary sum-check in the corresponding proof process. Use sum-check to prove that the following formula is equal to _output(r), where _output is the MLE of output and r is the random challenge value.
Where <m> is the total number of instructions executed during the execution process; <_eq> is a multilinear polynomial; <F> is the number of instructions in the RISCV instruction set; <_flags> indicates the instruction id used by the x step instruction; <terms f> is the output of all sub-lookup tables queried by the x step instruction; <gf> is the combined operation of the output of the sub-lookup table corresponding to instruction f.
For details, please refer to Jolt’s proof process.
In addition, because the table lookup operation also involves access to the lookup table, memory checking similar to byte-code is also required.
The following is the instruction table lookup proof process:
3.3 Core Proof Step 3: Read Write Memory Proof
3.3.1 Why read write memory proof ?
Note that our goal is to prove the correctness of a program execution or calculation process, that is, the prover will execute the program to be proved and then prove that the execution process is correct.
First the client program is compiled to elf file. Then the elf file is loaded into the memory, byte-code is obtained. Jolt vm will execute each instruction one by one.
The instructions will access ram/register during the execution process. The purpose of read_write memory proof is to ensure that the behavior of each instruction accessing memory is correct.
3.3.2 Proof Principle
The following figure shows the proof process of read_write_memory_proof:
<memory_checking> is similar to the proof of byte-code memory checking.
<timestampValidity> Because when the executing program accesses ram/registers, it is not only reading, but also writing. To prevent dishonest provers, when proving the legitimacy of a certain address, for example, address is read at the j step instruction, but the recorded read value is the value written to the address by an instruction after the j step instruction. Therefore, in addition to proofs similar to byte-code memory checking, timestamp checking is also required, which is what timestampValidity does.
<prove_output> To prevent dishonest provers, when proving the correctness of ram/register access, the prover uses incorrect “input and output of the proven program” for proof. To do this, we need to use sum-check to prove that the prover honestly uses the correct input and output for proof, which is what the prove_output function does. As shown in the figure below:
3.4 Core proof step 4: R1CS proof
3.4.1 why R1CS proof?
Note that our goal is to prove the correctness of a program execution or calculation process, that is, the prover will execute the program to be proved and then prove that the execution process is correct.
First the client program is compiled to elf file. Then the elf file is loaded into the memory, byte-code is obtained. Jolt vm will execute each instruction one by one.
R1CS proof is to ensure that the constraints between instructions are satisfied, such as the output of the i step instruction is equal to the input of the i+1 step instruction.
3.4.2 Proof Principle
The proof of “constraints between instructions in executing the program” is reduced to the proof of “sum-check’s summation problem”.
R1CS refers to the proof of the following equation, which we call the equation (Equation 4.1)
Where <A,B,C> are three matrices, m is number of rows of each matrix, n is number of columns of each matrix; <_fA> MLE (multi linear extension) after matrix A is regarded as a function; <_fB> MLE of matrix B; <_fC> MLE of matrix C;<Z> Function Z: {0,1}^log(n) → F, data involved in the execution of client program.
Why can R1CS be used to prove that the constraints between instructions of program execution are satisfied?
You can see the example in the figure below, which includes the operation of 3 instructions, with inputs z1, z2, z3, while z4 and z5 are intermediate calculation results, and z6 is the final calculation result.
The first matrix in the equation in the figure is matrix A, the second is B, and the third is C.
Then the constraints between the 3 instructions are satisfied if and only if (Equation 4.1) holds.
How to prove that (Equation 4.1) holds ?
To do this, we construct the following polynomial:
Then (Equation 4.1) holds if and only if gZ(X) == 0. In addition, we construct the polynomial:
where m is the number of rows of matrix A, and _β is the equal polynomial.
Finally, we get that the constraints between the instructions executed by the program are satisfied if and only if:
The proof of this formula can be achieved through sum-check.
Here, we have omitted some proof details, but it is not difficult to complete them. The following figure shows the proof process of R1CS:
Finally, we introduce the shortcomings and development direction of Jolt
4. Future Perspectives
We have thoroughly introduced the Jolt, and we expect it to become more popular as more developers join to work on it. We are particularly focused on accelerating with hardware, and we will publish more articles in the future.