Jolt: Introduction

Jolt : Hundred Thousand Feet Overview#

Jolt is a state-of-the-art zero-knowledge virtual machine (zk-VM) that powers the proving machinery of blockchains in research and industry. A traditional virtual machine executes a guest program compiled for a specified instruction set architecture (ISA), such as RISC-V, ARM, x86, etc. by emulating the guest CPU in software. A zk-VM is a virtual machine with the added responsibility that it is required to output an efficiently checkable cryptographic proof that it executed every instruction of the guest program correctly. Thus, Jolt being a zk-VM, can be logically split into the tracer and the prover. The tracer takes a guest program $x$ compiled down to RISC-V, executes instructions in order, and generates a witness $w$.

In the language of computational complexity theory, the guest program $x$ is often referred to as the problem instance, and the honest trace witness $w$ is referred to as the $\NP$ witness which can be compared with the program to validate that the output was generated by executing the program’s actual instructions. The NP relation $\mathcal{R}$ checks if the witness was generated by running every instruction of the program correctly. If it was, then

$$ \mathcal{R}(x, w) = 1 $$ Outputting an $\NP$ witness as the proof on its own accomplishes little. A client wishing to confirm the result came from the program could simply run the program to generate its own witness $w’$, and compare it against the prover’s witness $w$. The challenge is to generate a substantially cheaper procedure for validating program execution. The Jolt prover’s task, then, can be viewed as compressing the witness $w$ to output a proof $\pi:= \pi(w,x) \in \bit^{*}$ that a client can efficiently process to validate whether the program was in fact run correctly. These compressed proofs are often referred to as SNARKs in the literature.

Conditions For Efficient Proof Generation#

To efficiently generate a proof, the Jolt zk-VM leverages the fact that all instructions in the guest program’s ISA satisfy the decomposability condition. Intuitively, an instruction is decomposable if it can be evaluated on inputs $(\vec{x},\vec{y})$ by decomposing the inputs into smaller chunks, evaluating a function on each chunk, and then efficiently combining the outputs of each chunk into the final output. The AND instruction, for example, is decomposable.

Let $m \in \Naturals$, then for any $\vec{x}, \vec{y} \in \{0,1\}^m$, let $f_{\text{AND}}(\vec{x},\vec{y}) = (x_{m-1} || … || x_0) \land (y_{m-1} || …|| y_0)$ be the bitwise AND operation. We can decompose the computation of the AND function as follows:

$$ f_{\text{AND}}(\vec{x}, \vec{y}) = \sum_{i=0}^{m-1} 2^i \cdot f_{\text{AND}} (x_i, y_i) $$

Unfortunately, not all native RISC-V instructions are decomposable in this way. For example, the SLL rd, rs1, rs2 instruction models the computation $f(x,y) = x \ll y$ where $x,y \in \{0,1\}^{64}$ represent the contents of registers rs1 and rs2 respectively. $\ll$ denotes the logical left bit shift operator, and the value $f(x,y) \in \bit^{64}$ is written into the contents of rd. Here, in order to know the bit $i$ of $f(x, y)$, we need to know one bit of $x$ and every bit of $y$. There is no way to decompose SLL.

Bytecode Expansion#

But the input to Jolt however is still RISC-V program, and so it needs some mechanism to decompose these instructions for efficient proof generation. The approach the Jolt zk-VM takes is to re-write the guest RISC-V program into a program in the Jolt ISA, which consists solely of decomposable instructions, but is still expressive enough to permit all RISC-V instructions to be efficiently rewritten into Jolt ISA instructions. Thus, Jolt re-writes all troublesome non-decomposable RISC-V instructions with a sequence of one or more decomposable Jolt instructions. In order to aid this emulation process the Jolt CPU includes the usual RISC-V registers plus some additional “virtual” general-purpose registers in which it stores intermediate results.

Continuing with the same example from above, the SLL RISC-V instruction is replaced with the following sequence of Jolt instructions.

VirtualPow2  v1,  rs2
MUL          rd, rs1, v1

where VirtualPow2 v1 rs2 is a Jolt ISA instruction that represents computation which sets the contents of virtual register v1 with $2^x$, where $x$ represents the contents of register rs2. As VirtualPow2 is not present in the RISC-V ISA, it is referred to as a virtual instruction. MUL on the other hand is the extension of the RISC-V instruction MUL to the Jolt ISA by allowing it to operate on both RISC-V general-purpose registers and Jolt ISA virtual registers. It is not too hard to see that the above sequence is equivalent to the original SLL instruction in that value in rd is the same whether we run one SLL instruction, or the expanded sequence. In summary, the Jolt ISA can be viewed as a strict subset of the RISC-V ISA, plus some virtual instructions, that can operate on RISC-V registers, plus some virtual registers.

TODO: (Ari) Insert figure

Reflecting back on the job of the tracer, in practice, witness generation proceeds in two steps. The Jolt tracer first translates all RISC-V instructions into one or more Jolt ISA instructions (the Jolt documentation refers to this process as bytecode expansion). Once translation is complete, the Jolt CPU executes Jolt instructions to generate the witness. Thus, the Jolt proof guarantees that it ran every Jolt (not RISC-V) instruction of the transformed guest program correctly. As the honest witness is generated by executing decomposable instructions, it is amenable to be compressed into an efficiently checkable proof. This added bytecode expansion step however, creates another potential for failure. RISC-V execution semantics are complex, and it is now necessary to ensure that the expanded Jolt ISA versions of all RISC-V instructions implement equivalent semantics.

The Jolt Constraints#

This phase of the project is currently under progress.

At this point we have a way of generating the NP witness. We briefly mentioned that a proof allows to assert that Jolt ran every instruction of the Jolt program correctly i.e. it generated the witness as prescribed. Note that we do not particularly care how the prover did this. Say in some bizarre world, the prover actually does not follow the ISA semantics, but is still able to generate the correct witness $w$, as if it ran the instructions correctly, then that is fine. What are after is a statement of the following form.

• Completenss: If tracer generated $w$ as prescribed, then the downstream verifying algorithm will always accept.

• Soundness: If the tracer generated $w^{*}$ that is not the honest witness, the downstream verifier will always reject.

For a well informed reader, it might seem peculiar that we say always above. They are well aware that to achieve succinctness of the SNARK, the above guarantees should hold with high probability. Still we claim in this phase of the verification project the above completeness and soundness guarantees must always hold. To justify why, we must understand what the verification algorithm is. We will still be somewhat high level about the verifier (without compromising correctness). When we say the verifying algorithm accepts, what we really mean is that set of constraints/equations are satisfied. The honest witness is simply the unique solution that ensures these equations are satisfied. So mentally, you can think that there exists 50 or so equations over $n$ variables over some finite field $\Field$. Verification involves checking that $w$ satisfies all the constraints.

Of course in reality, the real verifier does not have $w$ in the clear, and neither do they verify each constraint manually. Instead we design a randomised check for constraint satisfaction using the sum-check protocol. See Chapters 2 and 3 of Justin Thaler’s book for a concrete example (Frievald’s algorithm does the same thing).

By modelling the deterministic version of the thing the verifier is checking, we can later just check if the sum-checks are randomised tests for these constraints or not. The actual completeness and soundness checks are handled here, and the we can reduce the remaining security to purely algebraic statements about equations. If this is still vague, then we recommend keeping tabs on the progress documented in Jolt Constraints.
Here we document the full process, and the lean proofs.

The Jolt Sum-checks#

Not yet Started

The Sum-Check Reductions#

Note yet Started

The Commitment Scheme#

Not yet started