Skip to main content

​
Overview

RAM read-write checking ensures that memory accesses are consistent throughout program execution. Every memory read must return the value from the most recent write to that address, and initial memory must match the program’s bytecode and inputs.

​
Role in the Proving System

RAM checking is one of the most complex and performance-critical components:
  1. Stages: Spans multiple stages (2, 4, 7)
    • Stage 2: RAF evaluation and read-write checking
    • Stage 4: Val evaluation and output checking
    • Stage 7: Claim reductions
  2. Input: Execution trace with memory reads/writes
  3. Output: Opening claims proving memory consistency
  4. Cost: ~30-40% of total proving time

​
Memory Model

​
Address Space

Jolt uses a word-addressed memory model:
  • Word size: 8 bytes (64 bits)
  • Address space: 2^K words (K configured per trace)
  • Addressing: Byte addresses divided by 8, remapped to [0, 2^K)

​
Memory Layout

┌─────────────────────┐ ← 0
│  Bytecode           │ (program image)
├─────────────────────┤
│  Trusted Advice     │ (prover-supplied, verified)
├─────────────────────┤
│  Untrusted Advice   │ (prover-supplied, constraints)
├─────────────────────┤
│  Inputs             │ (public inputs)
├─────────────────────┤
│  Outputs            │ (public outputs)
├─────────────────────┤
│  Panic / Term bits  │
├─────────────────────┤ ← RAM_START_ADDRESS
│  DRAM               │ (heap + stack)
└─────────────────────┘ ← 2^K
Address remapping: 
pub fn remap_address(address: u64, memory_layout: &MemoryLayout) -> Option<u64> {
    if address == 0 { return None; }  // Null pointer → no access
    let lowest = memory_layout.get_lowest_address();
    if address >= lowest {
        Some((address - lowest) / 8)
    } else {
        panic!("Unexpected address")
    }
}

​
Memory Checking Protocol

Like register checking, RAM uses offline memory checking via multiset equality.

​
Multiset Representation

Reads multiset R: 
R = {(time, addr, value) | instruction at time reads value from memory addr}
Writes multiset W: 
W = {(0, addr, value) | addr initialized to value} ∪ 
    {(time, addr, value) | instruction at time writes value to memory addr}
Correctness condition: 
R ⊆ W

​
Incremental Fingerprints

Fingerprints computed incrementally (like registers): 
fingerprint[i+1] = fingerprint[i] · (γ - hash(access[i+1]))
where hash encodes (timestamp, address, value) as a field element.

​
RAM Checking Stages

​
Stage 2: Read-Write Checking & RAF Evaluation

Purpose: Core memory consistency check via fingerprint sumcheck. Sumcheck claim: 
Σ_{x ∈ {0,1}^m} eq(r, x) · [write_fingerprint(x) / read_fingerprint(x)] = final_ratio
Key insight: final_ratio should equal ratio of initial states if R ⊆ W. RAF Evaluation: Read-After-Final (RAF) polynomial detects invalid reads: 
RAF[addr, time] = 1 if read from addr after final write, else 0
Checked via sumcheck: 
Σ_{addr, time} RAF[addr, time] · read_flag[addr, time] = 0

​
Stage 4: Val Evaluation & Output Check

Val Evaluation: Computes memory value evaluations at challenge points: 
Σ_{x ∈ {0,1}^m} eq(r, x) · mem_val(x) = claimed_eval
Output Check: Verifies public outputs match final memory state: 
Σ_{addr ∈ output_region} eq(r, addr) · final_mem[addr] = output_eval
Public outputs (program results, panic bit, termination bit) are exposed to verifier.

​
Stage 7: Claim Reductions

Aggregates RAM opening claims:
  • RA (Read-After) polynomial evaluations
  • Incremental polynomial evaluations
  • Final state polynomial evaluations
See Opening Proof for batching details.

​
Initial and Final Memory States

​
Initial State Construction

pub fn gen_ram_initial_memory_state<F: JoltField>(
    ram_K: usize,
    ram_preprocessing: &RAMPreprocessing,
    program_io: &JoltDevice,
) -> Vec<u64>
Components:
  1. Bytecode: Program image at min_bytecode_address
  2. Inputs: Public inputs at memory_layout.input_start
  3. Advice: Trusted/untrusted advice at respective start addresses
  4. Zero padding: Remaining memory initialized to 0

​
Final State Verification

pub fn gen_ram_memory_states<F: JoltField>(
    ram_K: usize,
    ram_preprocessing: &RAMPreprocessing,
    program_io: &JoltDevice,
    final_memory: &Memory,
) -> (Vec<u64>, Vec<u64>)
Final state includes:
  • DRAM: Final heap/stack state from emulator
  • Outputs: Public outputs at memory_layout.output_start
  • Panic bit: 1 if program panicked, else 0
  • Termination bit: 1 if program terminated normally, else 0

​
Sparse Memory Evaluation

Jolt uses sparse evaluation to avoid materializing full memory vectors: 
fn sparse_eval_u64_block<F: JoltField>(
    start_index: usize,
    values: &[u64],
    r: &[F::Challenge],
) -> F
Optimization:
  • Only evaluates non-zero regions (bytecode, inputs, outputs)
  • Uses aligned power-of-two block decomposition
  • Avoids O(2^K) memory materialization
  • Critical for large address spaces

​
Example: Initial RAM Evaluation

pub fn eval_initial_ram_mle<F: JoltField>(
    ram_preprocessing: &RAMPreprocessing,
    program_io: &JoltDevice,
    r_address: &[F::Challenge],
) -> F {
    let bytecode_start = remap_address(...);
    let mut acc = sparse_eval_u64_block::<F>(bytecode_start, &ram_preprocessing.bytecode_words, r_address);
    
    if !program_io.inputs.is_empty() {
        let input_start = remap_address(...);
        let input_words = pack_bytes_to_words(&program_io.inputs);
        acc += sparse_eval_u64_block::<F>(input_start, &input_words, r_address);
    }
    
    acc
}
This evaluates the initial memory MLE at random point r_address in O(bytecode_size + input_size) instead of O(2^K).

​
Advice Polynomials

Jolt supports advice inputs (prover-supplied data not part of program inputs):

​
Trusted vs. Untrusted Advice

Trusted Advice:
  • Prover commits to advice via polynomial commitment
  • Verifier checks commitment against public hash/digest
  • Used for pre-verified data (e.g., Merkle proofs)
Untrusted Advice:
  • Prover commits to advice
  • Constraints verify correctness (e.g., witness for cryptographic operations)
  • Used for optimization (e.g., bigint multiplication)

​
Advice Integration

Advice is embedded in initial memory state: 
init_mem[advice_start..advice_end] = advice_bytes
But opened separately to avoid verifier computation:
  • Prover: Opens advice commitment at challenge point
  • Verifier: Uses opening to compute init_eval contribution
  • BlindFold constraints: Decompose init_eval as public + Σ(selector_i · advice_i)

​
Advice Selector Computation

pub fn compute_advice_selector<F: JoltField>(
    advice_num_vars: usize,
    advice_start: u64,
    memory_layout: &MemoryLayout,
    r_address: &[F::Challenge],
    total_memory_vars: usize,
) -> F
Computes the scaling factor for embedding advice block into full memory MLE: 
selector = ∏_{i} (r[i] if bit[i]=1 else 1-r[i])
where bits are the binary prefix of advice_start in memory.

​
Hamming Weight Booleanity

RAM checking includes booleanity checks for one-hot encodings: Purpose: Verify that RA (Read-After) indices are valid one-hot encodings. Sumcheck: 
Σ_{x ∈ {0,1}^m} eq(r, x) · [hamming_weight(RA[x]) - 1] = 0
Each RA index should have exactly 1 bit set (indicating which write it depends on).

​
Stage Alignment Constraints

Critical invariant from ram/mod.rs documentation:
After Stage 2 address-round alignment, there is exactly one RAM address point: r_address.
Why this matters:
  • Multiple RAM sumchecks (RW-checking, RAF-eval, Val-check) open RA polynomials
  • All must use the same address challenge vector r_address
  • Enforced by careful padding/alignment of sumcheck rounds
  • Violation causes RA reduction sumcheck to fail
Implementation:
  • RamReadWriteChecking binds address variables in config-dependent schedule
  • RamRafEvaluation and OutputCheck padded to align with same global rounds
  • RamValCheck caches openings at the same r_address point

​
Performance Characteristics

​
Prover Time

Stage 2 (Read-Write Checking + RAF):
  • O(trace_length · K) field operations
  • ~20-25% of total proving time
  • Dominated by incremental fingerprint updates
Stage 4 (Val Evaluation + Output):
  • O(trace_length · K) field operations
  • ~10-15% of total proving time
Total RAM checking: ~30-40% of proving time

​
Memory Usage

With sparse evaluation:
  • ~50-100MB for 10⁶ cycles with K=20
  • No materialized memory vectors
Without sparse evaluation:
  • Would require ~8GB for K=20 (2^20 · 8 bytes · 2 states)

​
Verifier Time

  • O(K · log(trace_length)) field operations
  • ~1-5ms for typical traces
  • Sparse evaluation critical for verifier efficiency

​
Key Files

  • jolt-core/src/zkvm/ram/mod.rs: Core RAM checking protocol and utilities
  • jolt-core/src/zkvm/ram/read_write_checking.rs: Fingerprint-based consistency checking
  • jolt-core/src/zkvm/ram/raf_evaluation.rs: Read-After-Final polynomial checking
  • jolt-core/src/zkvm/ram/val_check.rs: Memory value evaluation
  • jolt-core/src/zkvm/ram/output_check.rs: Public output verification
  • jolt-core/src/zkvm/ram/hamming_booleanity.rs: One-hot encoding verification

​
Next Steps

Build docs developers (and LLMs) love

Get started for freeTalk to us