> ## Documentation Index > Fetch the complete documentation index at: https://mintlify.com/a16z/jolt/llms.txt > Use this file to discover all available pages before exploring further. # Instruction Lookup System > Learn how Jolt verifies instruction execution via lookup tables ## Overview Jolt's **instruction lookup system** proves that each instruction in the execution trace produces the correct output. Instead of implementing instruction logic as R1CS constraints (which would be massive), Jolt uses a novel **lookup argument** that proves instruction correctness by looking up precomputed outputs in committed tables. ## Role in the Proving System Instruction lookups are central to Jolt's efficiency: 1. **Stage**: Stage 5 (Instruction Lookups) 2. **Input**: Execution trace with instruction operands (RS1, RS2, immediate) 3. **Method**: Lookup outputs in committed tables, prove via sumcheck 4. **Output**: Opening claims for instruction flags and lookup results 5. **Benefit**: Drastically smaller proof size than constraint-per-instruction approaches ## Instruction Decomposition ### Subtable Structure Jolt decomposes each instruction into **small subtables**: **Example: 64-bit XOR** * Naive approach: 2^128 entry table (operands A, B) * Jolt approach: Split operands into 8-byte chunks * 8 subtables, each 2^16 entries (8-bit input, 8-bit output) * Total size: 8 · 2^16 = 524,288 entries (vs. 2^128) **General pattern**: ``` instruction(A, B) = combine( subtable_0(A[0..7], B[0..7]), subtable_1(A[8..15], B[8..15]), ... subtable_k(A[...], B[...]) ) ``` ### Virtual vs. Physical Instructions **Physical instructions**: * Direct RISC-V opcodes (ADD, XOR, LOAD, etc.) * One lookup per instruction **Virtual instructions**: * Multi-cycle operations (e.g., 256-bit multiplication) * Decomposed into multiple subtable lookups * Used by jolt-inlines for optimized cryptographic operations ## Lookup Argument Protocol Jolt uses the **Twist/Shout** lookup argument (modified Lasso): ### High-Level Protocol 1. **Prover commits** to subtables (one-time preprocessing) 2. **Trace generation**: For each instruction, record: * Instruction flags (one-hot encoding of opcode) * Operands (RS1, RS2, immediate) * Chunk indices (operands split into subtable indices) 3. **Sumcheck**: Prove that looked-up values match instruction outputs 4. **Opening proofs**: Verify subtable commitments at queried indices ### RA (Read-After) Polynomial The RA polynomial encodes **which table entry** is accessed: ``` RA[instruction_id, subtable_id, entry_index] = count of lookups ``` In one-hot form: ``` RA[i] = 1 if entry i is accessed, else 0 ``` **Sumcheck claim**: ``` Σ_{i} RA[i] · subtable_value[i] = Σ_{instruction} expected_output ``` This proves that looked-up values sum to expected instruction outputs. ### RAF (Read-After-Final) Checking Similar to RAM checking, instruction lookups verify **RAF=0** to ensure: * No lookups to invalid table entries * All lookups reference valid subtable indices ## Instruction Flags Each cycle has **instruction flags** (one-hot encoding): ```rust theme={null} pub struct InstructionFlags { pub flag_add: bool, pub flag_sub: bool, pub flag_xor: bool, // ... ~50 instruction flags ... } ``` **Purpose**: * Activate correct subtable lookups for each instruction * Used in R1CS constraints to conditionally enforce instruction semantics * One flag set per cycle (except no-ops) ## Subtable Implementations ### Lookup Table Trait ```rust theme={null} pub trait LookupTable { fn materialize(K: usize) -> Vec; // Generate table entries fn suffix_materialize() -> Vec; // Suffix table variant fn prefix_materialize() -> Vec; // Prefix table variant } ``` ### Example: XOR Table ```rust theme={null} pub struct XorLookupTable; impl LookupTable for XorLookupTable { fn materialize(K: usize) -> Vec { (0..2^K).map(|i| { let a = (i >> 8) as u8; let b = (i & 0xFF) as u8; F::from(a ^ b) }).collect() } } ``` ### Subtable Categories **Arithmetic**: ADD, SUB, MUL, DIV **Logical**: AND, OR, XOR, NOT **Shifts**: SLL, SRL, SRA, rotate **Comparisons**: LT, LTE, EQ **Memory**: Load/store address computation **Specialized**: Sign extension, byte reversal, bit counting ## Instruction Lookups Sumcheck (Stage 5) ### RA Virtual Sumcheck **Purpose**: Reduce RA polynomial claims to subtable evaluations. **Sumcheck claim**: ``` Σ_{x ∈ {0,1}^m} eq(r, x) · RA_instruction(x) = claimed_eval ``` where `RA_instruction(x)` is the RA polynomial for instruction lookups at cycle x. **Polynomial structure**: * One RA polynomial per instruction type * Shared across multiple subtables (prefix/suffix decomposition) * Lazy materialization via `SharedRaPolynomials` (memory optimization) ### Read-RAF Checking **Purpose**: Verify no invalid lookups (like RAM RAF checking). **Sumcheck claim**: ``` Σ_{subtable, index} RAF[subtable, index] · RA[subtable, index] = 0 ``` If any lookup is invalid (RAF=1), the sumcheck fails. ## Performance Characteristics ### Prover Time **Subtable commitment** (one-time preprocessing): * O(table\_size · log(table\_size)) field operations * \~1-5 seconds for all subtables (amortized across all proofs) **Lookup sumcheck** (per proof): * O(trace\_length · num\_subtables · log(table\_size)) * \~15-20% of total proving time ### Memory Usage **Subtable storage**: * \~50-100MB for all RISC-V subtables * Shared across all proofs (one-time cost) **RA polynomial storage**: * Uses `SharedRaPolynomials` to deduplicate equality tables * \~10-20MB for 10⁶ cycles ### Proof Size **Without lookups** (naive R1CS): * Would require \~1000 constraints per instruction type * Proof size: O(num\_instructions · trace\_length) **With lookups**: * O(num\_subtables · log(table\_size)) * \~10x smaller proof size for typical workloads ### Verifier Time * O(num\_subtables · log(trace\_length)) * \~1-3ms for typical traces * Verifies sumcheck round polynomials + subtable commitment openings ## Comparison with Other zkVMs | Approach | Jolt (Lookups) | Cairo (AIR) | RISC Zero (AIR) | Polygon Miden (Lookups) | | ---------------- | -------------------- | ----------- | --------------- | ----------------------- | | Instruction cost | O(log table\_size) | O(degree) | O(degree) | O(log table\_size) | | Proof size | Logarithmic | Linear | Logarithmic | Logarithmic | | Setup | Subtable commitment | None | None | Subtable commitment | | Flexibility | High (custom tables) | Medium | Medium | High | ## Optimizations ### Prefix/Suffix Decomposition **Problem**: Some instructions need different lookup tables for different operand chunks. **Solution**: Split polynomials as: ``` P(x) = Σ P_i(x_prefix) · Q_i(x_suffix) ``` Allows efficient sumcheck over decomposed operands. ### Shared RA Polynomials **Problem**: Multiple instructions share subtable structures (e.g., all shifts use same bit-extraction tables). **Solution**: `SharedRaPolynomials` deduplicates equality tables: ```rust theme={null} pub struct SharedRaPolynomials { shared_eq_tables: Vec>, // Shared across N polynomials ra_indices: Vec>, // Per-polynomial index selection } ``` Reduces memory from O(N · table\_size) to O(table\_size + N · trace\_length). ### Lazy RA Materialization **Problem**: Materializing full RA polynomials for all instructions is expensive. **Solution**: `RaPolynomial` uses lazy state machine: ``` Round1 → Round2 → Round3 → RoundN ``` Each round binds one challenge bit, progressively filtering table entries. ## Key Files * `jolt-core/src/zkvm/instruction_lookups/ra_virtual.rs`: RA polynomial sumcheck * `jolt-core/src/zkvm/instruction_lookups/read_raf_checking.rs`: RAF verification * `jolt-core/src/zkvm/lookup_table/`: All subtable implementations * `jolt-core/src/poly/ra_polynomial.rs`: Lazy RA polynomial materialization * `jolt-core/src/poly/shared_ra_polynomials.rs`: Shared equality table optimization ## Next Steps * [Bytecode](/architecture/bytecode): Instruction encoding and PC mapping * [Opening Proofs](/architecture/opening-proof): Verifying subtable commitments * [Spartan](/architecture/spartan): Integration with R1CS constraints