Advent of Jolt (Day 3): Prologue Before The Sumchecks

jolt draft

2025-10-28 By Ari

A Theoretical Detour

Before we look at code and analyse intermediate outputs, we pause and contemplate what it means for a prover to execute a program correctly? How does one express correct exceution as a sequence of mathematical equaitions? The goal os this post is to outline the constraints that the prover must prove they satisfy?

Note to the informed reader: For the sake of simplicity, we will defer the discussion about virtual polynomials and sum-checks for a later post. When we get to enforcing each constraint with a sum-check, we’ll formerly introduce these polynomials.

For each cycle, we have a Cycle struct as discussed earlier. The vector of these structs is what we call the dynamic trace.
From this struct we construct the following R1CSCycleInput struct. The field of this type are annoated with self explanatory comments. We will often denote this struct below with z_t or \(z_t\) to denote the witness constructed for cycle \(t \in [T]\). There are a total of 36 fields in this struct and each field is either a boolean valued byte or an arithmetic type of u64 or i128 or s64 (signed u64).

#[derive(Clone, Debug)]
pub struct R1CSCycleInputs {
    /// Left instruction input as a u64 bit-pattern.
    /// Typically `Rs1Value` or the current `UnexpandedPC`, depending on `CircuitFlags`.
    pub left_input: u64,
    /// Right instruction input as signed-magnitude `S64`.
    /// Typically `Imm` or `Rs2Value` with exact integer semantics.
    pub right_input: S64,
    /// Signed-magnitude `S128` product consistent with the `Product` witness.
    /// Computed from `left_input` × `right_input` using the same truncation semantics as the witness.
    pub product: S128,

    /// Left lookup operand (u64) for the instruction lookup query.
    /// Matches `LeftLookupOperand` virtual polynomial semantics.
    pub left_lookup: u64,
    /// Right lookup operand (u128) for the instruction lookup query.
    /// Full-width integer encoding used by add/sub/mul/advice cases.
    pub right_lookup: u128,
    /// Instruction lookup output (u64) for this cycle.
    pub lookup_output: u64,

    /// Value read from Rs1 in this cycle.
    pub rs1_read_value: u64,
    /// Value read from Rs2 in this cycle.
    pub rs2_read_value: u64,
    /// Value written to Rd in this cycle.
    pub rd_write_value: u64,

    /// RAM address accessed this cycle.
    pub ram_addr: u64,
    /// RAM read value for `Read`, pre-write value for `Write`, or 0 for `NoOp`.
    pub ram_read_value: u64,
    /// RAM write value: equals read value for `Read`, post-write value for `Write`, or 0 for `NoOp`.
    pub ram_write_value: u64,

    /// Expanded PC used by bytecode instance.
    pub pc: u64,
    /// Expanded PC for next cycle, or 0 if this is the last cycle in the domain.
    pub next_pc: u64,
    /// Unexpanded PC (normalized instruction address) for this cycle.
    pub unexpanded_pc: u64,
    /// Unexpanded PC for next cycle, or 0 if this is the last cycle in the domain.
    pub next_unexpanded_pc: u64,

    /// Immediate operand as signed-magnitude `S64`.
    pub imm: S64,

    /// Per-instruction circuit flags indexed by `CircuitFlags`.
    pub flags: [bool; NUM_CIRCUIT_FLAGS],
    /// `IsNoop` flag for the next cycle (false for last cycle).
    pub next_is_noop: bool,

    /// Derived: `Jump && !NextIsNoop`.
    pub should_jump: bool,
    /// Derived: `Branch && (LookupOutput == 1)`.
    pub should_branch: bool,

    /// `IsRdNotZero` && ` `WriteLookupOutputToRD`
    pub write_lookup_output_to_rd_addr: bool,
    /// `IsRdNotZero` && `Jump`
    pub write_pc_to_rd_addr: bool,

    /// `VirtualInstruction` flag for the next cycle (false for last cycle).
    pub next_is_virtual: bool,
    /// `FirstInSequence` flag for the next cycle (false for last cycle).
    pub next_is_first_in_sequence: bool,
}

where the circuit flags are given by

pub enum CircuitFlags {
    /// 1 if the first lookup operand is the sum of the two instruction operands.
    AddOperands,
    /// 1 if the first lookup operand is the difference between the two instruction operands.
    SubtractOperands,
    /// 1 if the first lookup operand is the product of the two instruction operands.
    MultiplyOperands,
    /// 1 if the instruction is a load (i.e. `LW`)
    Load,
    /// 1 if the instruction is a store (i.e. `SW`)
    Store,
    /// 1 if the instruction is a jump (i.e. `JAL`, `JALR`)
    Jump,
    /// 1 if the lookup output is to be stored in `rd` at the end of the step.
    WriteLookupOutputToRD,
    /// 1 if the instruction is "virtual", as defined in Section 6.1 of the Jolt paper.
    VirtualInstruction,
    /// 1 if the instruction is an assert, as defined in Section 6.1.1 of the Jolt paper.
    Assert,
    /// Used in inline sequences; the program counter should be the same for the full sequence.
    DoNotUpdateUnexpandedPC,
    /// Is (virtual) advice instruction
    Advice,
    /// Is a compressed instruction (i.e. increase UnexpandedPc by 2 only)
    IsCompressed,
    /// Is instruction the first in a virtual sequence
    IsFirstInSequence,
}

The mental model for this vector is think of a 36 dimensional vector which each cell is filled with values of the above type. The method to go from a Cycle struct to the above witness objects is in the from_trace method.

Constraints

One example of what it means to execute a program correctly is the following: In RISCV loads/stores look like the following:

lb   rd, offset(rs1)    # Load byte (sign-extended)
lh   rd, offset(rs1)    # Load halfword (sign-extended)
lw   rd, offset(rs1)    # Load word (sign-extended)
ld   rd, offset(rs1)    # Load doubleword (RV64)
lbu  rd, offset(rs1)    # Load byte unsigned
lhu  rd, offset(rs1)    # Load halfword unsigned
lwu  rd, offset(rs1)    # Load word unsigned (RV64)

sb   rs2, offset(rs1)   # Store byte
sh   rs2, offset(rs1)   # Store halfword
sw   rs2, offset(rs1)   # Store word
sd   rs2, offset(rs1)   # Store doubleword (RV64)

So if a vector has the Load flag set to 1 or Store flag set to 1, then the address from which we read/write must be equal to rs1+offset. Using propositional logic we write:

if { Load + Store }
=> ( RamAddress ) == ( Rs1Value + Imm )

The same thing expressed as algebraic constraints:

(Load + Store) * (RamAddress - (Rs1Value + Imm)) = 0

Thus, any program that is correctly executed, the witness \(z_t\) constructed from cycle \(t\) must satisfy the above constraint.

Foreshadowing the future

Imagine a make believe world where that’s all we needed to check if a program was executed correctly. then one can already see the outline of a sum-check. for all \(t \in \{ 0, 1\}^{\log t}\), load[t], store[t], ramaddr[t], rs1value[t], imm[t] are vectors of size \(T\) (see figure above), and we can now have a sumecheck, where the use the multilinear extensions of the above vectors below, where \(r_{\text{cycle}}\) is the random point where we check equality of polynomials (and invoke Schwartz-Zippel).

TODO: Format these with macros

\[\sum_{j \in \{ 0, 1\}^{\log t}} \text{eq}(\text{r_cycle}, j) \Big(\text{load}[t] + \text{store}[t]) * (\text{ramaddress}[t] - (\text{rs1value}[t] + \text{imm}[t])\Big) = 0\]

Of course, successfully executing this sum-check involes being able to open these polynomials at random points, which in the real world means the prover MUST commit to these polynomials. But we already know what the prover has committed to and the above polynomials were not in the list. So how will this work? This is where we will get into the business of virtual polynomials. They happen to be polynomials the prover does not actually commit to, but can reliably open by committing to different polynomials, and opening them at the desired random location. In fact you can go and see that the above polynomials do indeed exist as virtual polynomials inside of Jolt. More on that in the coming posts. For now we go back to describing what it means for a program to be correct.

For now we talk about all the constraints in Jolt. The links contain full details about each constraint.

R1CS Equality Constraints/Named Constraints: These are constraints like the above example where we can write a constraint as a product of two linear equations equalling 0.
Product Constraints: This is exactly the same as above, but the product equals a non-zero value.
Shift Constraints: The order in which we execute a program matters. These constraints that the order is respected.
Twist/Shout Constraints So far all constraints assume that we read/write correctly from memory. We get to these finally.

Together – all 4 of these constraints describe the correct execution of a programmer. All that is left now is to define a sum-check for each of these constraints, and then compute the sum-checks.

What’s next

That ends our detour. We’ve writtend down a set of constraints as equations. If we were to satisfy said equations, then we it is fair game for us to say that the program is correct.

I do not know if there is a formal proof that the above constraints are enough. It feels as if they are, but such things must be formally proved. Talk to Quang Dao for more details.

We now once more follow the code chronologically, and next we arrive at the 7 sumcheck stages in Jolt.§