Overview
Stage 1
Stage 2
Stage 3
Stage 4
Stage 5
Stage 6
Stage 7
Openings
Polynomials
Resolve
Polynomial Registry
Registers
$\textcolor{ForestGreen}{\textsf{RdInc}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
rd_write_timestamp[t] - rd_write_timestamp[t-1]
RAM
$\textcolor{ForestGreen}{\textsf{RamInc}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
ram_write_timestamp[t] - ram_write_timestamp[t-1]
Instruction lookup
$\textcolor{ForestGreen}{\textsf{InstructionRa}(i)}$
$$\{0,1\}^{\log_2 N_{\text{instr}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot over N_instr values; 1 iff chunk i of instruction address = k at cycle t. i in 0..d_instr-1
Bytecode
$\textcolor{ForestGreen}{\textsf{BytecodeRa}(i)}$
$$\{0,1\}^{\log_2 N_{\text{instr}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot over N_instr values; 1 iff chunk i of bytecode row index = k at cycle t. i in 0..d_bc-1
RAM
$\textcolor{ForestGreen}{\textsf{RamRa}(i)}$
$$\{0,1\}^{\log_2 N_{\text{instr}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot over N_instr values; 1 iff chunk i of RAM address = k at cycle t. i in 0..d_ram-1
Advice
$\textcolor{ForestGreen}{\textsf{TrustedAdvice}}$
(no fixed domain)
committed before proving; verifier has the commitment
$\textcolor{ForestGreen}{\textsf{UntrustedAdvice}}$
(no fixed domain)
committed during proving; commitment included in proof
Program counter
$\textcolor{BurntOrange}{\textsf{PC}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
trace[t].pc (expanded ELF address)
$\textcolor{BurntOrange}{\textsf{UnexpandedPC}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
trace[t].unexpanded_pc (raw ELF address)
$\textcolor{BurntOrange}{\textsf{NextPC}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
PC(t+1); left-shift of PC by one cycle
$\textcolor{BurntOrange}{\textsf{NextUnexpandedPC}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
UnexpandedPC(t+1); left-shift of UnexpandedPC by one cycle
Instruction lookup
$\textcolor{BurntOrange}{\textsf{LookupOutput}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
T_{table(t)}(address(t)); the lookup table output at cycle t
$\textcolor{BurntOrange}{\textsf{LeftLookupOperand}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
LeftOp(address(t)) if interleaved, else 0
$\textcolor{BurntOrange}{\textsf{RightLookupOperand}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
RightOp(address(t)) if interleaved, else unmap(address(t))
$\textcolor{BurntOrange}{\textsf{LeftInstructionInput}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
left operand to the ALU: rs1_val, pc, or imm depending on flags
$\textcolor{BurntOrange}{\textsf{RightInstructionInput}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
right operand to the ALU: rs2_val or imm depending on flags
$\textcolor{BurntOrange}{\textsf{InstructionRa}(i)}$
$$\{0,1\}^{\log_2 N_v} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
prod_{j=0}^{M-1} cp:InstructionRa(i*M+j)(k_j, t); product of M committed chunks
$\textcolor{BurntOrange}{\textsf{InstructionRafFlag}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
OpFlags(Add) + OpFlags(Sub) + OpFlags(Mul); 1 iff single-value range check
$\textcolor{BurntOrange}{\textsf{LookupTableFlag}_{i}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff lookup table i is active at cycle t; at most one flag is 1 per cycle
Product constraints
$\textcolor{BurntOrange}{\textsf{Product}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
LeftInstructionInput(t) * RightInstructionInput(t)
$\textcolor{BurntOrange}{\textsf{ShouldJump}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
OpFlags(Jump)(t) * (1 - NextIsNoop(t))
$\textcolor{BurntOrange}{\textsf{ShouldBranch}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
LookupOutput(t) * InstructionFlags(Branch)(t)
$\textcolor{BurntOrange}{\textsf{WritePCtoRD}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
InstructionFlags(IsRdNotZero)(t) * OpFlags(Jump)(t)
$\textcolor{BurntOrange}{\textsf{WriteLookupOutputToRD}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
InstructionFlags(IsRdNotZero)(t) * OpFlags(WriteLookupOutputToRD)(t)
Registers
$\textcolor{BurntOrange}{\textsf{Rd}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
trace[t].rd; destination register index
$\textcolor{BurntOrange}{\textsf{Imm}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
trace[t].imm; immediate value
$\textcolor{BurntOrange}{\textsf{Rs1Value}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
registers[trace[t].rs1] before cycle t
$\textcolor{BurntOrange}{\textsf{Rs2Value}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
registers[trace[t].rs2] before cycle t
$\textcolor{BurntOrange}{\textsf{RdWriteValue}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
value written to registers[rd] at cycle t
$\textcolor{BurntOrange}{\textsf{Rs1Ra}}$
$$\{0,1\}^{\log_2 K_{\text{reg}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot: 1 iff k = trace[t].rs1
$\textcolor{BurntOrange}{\textsf{Rs2Ra}}$
$$\{0,1\}^{\log_2 K_{\text{reg}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot: 1 iff k = trace[t].rs2
$\textcolor{BurntOrange}{\textsf{RdWa}}$
$$\{0,1\}^{\log_2 K_{\text{reg}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
one-hot: 1 iff k = trace[t].rd
$\textcolor{BurntOrange}{\textsf{RegistersVal}}$
$$\{0,1\}^{\log_2 K_{\text{reg}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
registers[k] right before cycle t
RAM
$\textcolor{BurntOrange}{\textsf{RamAddress}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
trace[t].ram_address (rs1 + imm if load/store, else 0)
$\textcolor{BurntOrange}{\textsf{RamRa}}$
$$\{0,1\}^{\log_2 K_{\text{ram}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
prod_{i=0}^{d_ram-1} cp:RamRa(i)(k_i, t); product of committed chunks
$\textcolor{BurntOrange}{\textsf{RamReadValue}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
memory[ram_address] before cycle t
$\textcolor{BurntOrange}{\textsf{RamWriteValue}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
memory[ram_address] after cycle t
$\textcolor{BurntOrange}{\textsf{RamVal}}$
$$\{0,1\}^{\log_2 K_{\text{ram}}} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
memory[k] right before cycle t
$\textcolor{BurntOrange}{\textsf{RamValInit}}$
$$\{0,1\}^{\log_2 K_{\text{ram}}} \to \mathbb{F}$$
memory[k] at t=0 (initial memory image)
$\textcolor{BurntOrange}{\textsf{RamValFinal}}$
$$\{0,1\}^{\log_2 K_{\text{ram}}} \to \mathbb{F}$$
memory[k] at t=T (final memory image)
$\textcolor{BurntOrange}{\textsf{RamHammingWeight}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
sum_k RamRa(k, t); number of active RAM chunks at cycle t (0 or 1)
Circuit flags
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{AddOperands})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) computes x+y (ADD, ADDI, AUIPC, ...)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{SubtractOperands})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) computes x-y (SUB)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{MultiplyOperands})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) computes x*y (MUL, MULH, ...)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Load})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is LB/LH/LW/LBU/LHU/LD/LWU
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Store})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is SB/SH/SW/SD
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Jump})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is JAL/JALR
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{WriteLookupOutputToRD})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff lookup output is written to rd
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{VirtualInstruction})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is a Jolt virtual instruction
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Assert})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is an assert (lookup output must be 1)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{DoNotUpdateUnexpandedPC})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff unexpanded PC should not advance (mid-virtual-sequence)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{Advice})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is a virtual advice instruction
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsCompressed})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is a 16-bit compressed instruction (PC += 2)
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsFirstInSequence})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is the first in a virtual instruction sequence
$\textcolor{BurntOrange}{\textsf{OpFlags}(\text{IsLastInSequence})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is the last in a virtual instruction sequence
Instruction flags
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{LeftOperandIsPC})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff left ALU operand = PC (e.g. AUIPC, JAL)
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{RightOperandIsImm})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff right ALU operand = imm (I-type instructions)
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{LeftOperandIsRs1Value})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff left ALU operand = rs1_val
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{RightOperandIsRs2Value})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff right ALU operand = rs2_val
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{Branch})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff instr(t) is BEQ/BNE/BLT/BGE/BLTU/BGEU
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsNoop})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff cycle t is a padding no-op
$\textcolor{BurntOrange}{\textsf{InstructionFlags}(\text{IsRdNotZero})}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
1 iff trace[t].rd != x0
Shift-derived
$\textcolor{BurntOrange}{\textsf{NextIsNoop}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
InstructionFlags(IsNoop)(t+1); left-shift by one cycle
$\textcolor{BurntOrange}{\textsf{NextIsVirtual}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
OpFlags(VirtualInstruction)(t+1); left-shift by one cycle
$\textcolor{BurntOrange}{\textsf{NextIsFirstInSequence}}$
$$\{0,1\}^{\log_2 T} \to \mathbb{F}$$
OpFlags(IsFirstInSequence)(t+1); left-shift by one cycle
Lookup tables
$T_i$
$$\{0,1\}^{\log_2 K_{\text{instr}}} \to \mathbb{F}$$
MLE of lookup table i
Operand extraction
$\textsf{LeftOp}$
$$\{0,1\}^{\log_2 K_{\text{instr}}} \to \mathbb{F}$$
MLE of left operand extraction from interleaved address bits
$\textsf{RightOp}$
$$\{0,1\}^{\log_2 K_{\text{instr}}} \to \mathbb{F}$$
MLE of right operand extraction from interleaved address bits
$\textsf{unmap}$
$$\{0,1\}^{\log_2 K} \to \mathbb{F}$$
MLE of identity function: {0,1}^n -> {0, ..., 2^n - 1}
Comparison
$\textsf{LT}$
$$\{0,1\}^{\log_2 T} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
MLE of less-than: 1 iff a < b
$\textsf{EqPlusOne}$
$$\{0,1\}^{\log_2 T} \times \{0,1\}^{\log_2 T} \to \mathbb{F}$$
MLE of successor: 1 iff b = a + 1
Lagrange basis
$\textsf{eq}$
$$\{0,1\}^{\log_2 n} \times \{0,1\}^{\log_2 n} \to \mathbb{F}$$
Multilinear Lagrange basis: eq(r,x) = prod_i (r_i*x_i + (1-r_i)(1-x_i))
$\textsf{L}$
$$\{0,1\}^{\log_2 |S|} \times \{0,1\}^{\log_2 |S|} \to \mathbb{F}$$
Univariate Lagrange selector over domain S ⊂ F: L(τ,x) = Σ_{s∈S} ℓ_s(τ)·ℓ_s(x). Used in Stage 1 (S={-5,...,4}) and Stage 2 (S={-2,...,2}) for the 'univariate skip'
Symbol Code name Description Formula
$T$
trace_length
Number of execution cycles (padded to power of 2)
—
$log_2 N_chunk$
log_k_chunk
Committed one-hot chunk bit-size (4 or 8)
—
$N_{\text{chunk}}$
k_chunk
Committed one-hot chunk size
2^log_k_chunk
$log_2 N_virtual$
lookups_ra_virtual_log_k_chunk
Virtual RA chunk bit-size
LOG_K/8 if log_T < 25 else LOG_K/4
$d_{\text{instr}}$
instruction_d
Number of committed RA chunks (instruction)
ceil(128 / log_2 N_instr)
$d_virutal_instr$
n_virtual_ra_polys
Number of virtual RA chunks (instruction)
128 / log_2 N_v
$M$
n_committed_per_virtual
Fan-in: committed chunks per virtual chunk
d_instr / d_v
$K_{\text{bc}}$
bytecode_k
Bytecode table size (program-dependent, padded to power of 2)
—
$d_{\text{bc}}$
bytecode_d
Number of committed RA chunks (bytecode)
ceil(log_2 K_bc / log_2 N_instr)
$K_{\text{ram}}$
ram_k
RAM address-space size
—
$d_{\text{ram}}$
ram_d
Number of committed RA chunks (RAM)
ceil(log_2 K_ram / log_2 N_instr)
$K_{\text{reg}}$
—
Register file size (32 for RV32, 64 for RV64)
—
$N_{\text{tables}}$
—
Number of lookup tables (42)
—