Skip to main content

​
Overview

Register read-write checking ensures that register values are consistent throughout program execution. Every register read must return the value from the most recent write to that register, and initial register values must be zero (except the stack pointer).

​
Role in the Proving System

Register checking is a critical component of memory consistency:
  1. Stage: Part of Stage 3 (Register and Bytecode checking)
  2. Input: Execution trace with register reads/writes per instruction
  3. Output: Opening claims proving register consistency
  4. Integration: Feeds into final claim reductions (Stage 7)

​
Register Architecture

​
RISC-V Register File

Jolt supports the RISC-V register file:
  • 32 integer registers (x0-x31) for RV32
  • 32 integer registers (x0-x31) for RV64 (64-bit values)
  • Special registers:
    • x0: Hardwired to zero (all writes ignored)
    • x2 (sp): Stack pointer (initialized to top of memory)
    • x1 (ra): Return address

​
Register Traces

Each instruction cycle records:
  • RS1 read: Source register 1 (address and value)
  • RS2 read: Source register 2 (address and value)
  • RD write: Destination register (address and value)
Not all instructions use all registers (e.g., lui only writes RD).

​
Memory Checking Protocol

Jolt uses an offline memory checking protocol based on multiset equality:

​
Multiset Representation

Reads multiset R: 
R = {(time, addr, value) | instruction at time reads value from register addr}
Writes multiset W: 
W = {(0, sp, stack_top), ...initial...} ∪ 
    {(time, addr, value) | instruction at time writes value to register addr}
Correctness condition: 
R ⊆ W
Every read must have a corresponding earlier write.

​
Fingerprinting via Polynomial Evaluation

Multiset equality is proved via random fingerprinting:
  1. Verifier samples random challenge γ
  2. Prover computes polynomial products:
    • Read fingerprint: ∏_{r ∈ R} (γ - hash(r))
    • Write fingerprint: ∏_{w ∈ W} (γ - hash(w))
  3. Check: Read fingerprint divides write fingerprint

​
Sumcheck Structure

​
Stage 3a: Register Val Evaluation

Purpose: Compute multilinear extension of register values at each cycle. Sumcheck claim: 
Σ_{x ∈ {0,1}^m} eq(r, x) · reg_val(x) = claimed_eval
where:
  • reg_val(x): Register value at cycle x (derived from trace)
  • r: Random evaluation point
  • claimed_eval: Value to be verified
Polynomials involved:
  • RegisterValues: Virtual polynomial from execution trace
  • RegisterAddresses: Which register is accessed
  • EqPolynomial: Equality check at challenge point

​
Stage 3b: Register Read-Write Checking

Purpose: Verify read/write consistency via fingerprint sumcheck. Sumcheck claim: 
Σ_{x ∈ {0,1}^m} eq(r, x) · [write_fingerprint(x) / read_fingerprint(x)] = final_ratio
where:
  • write_fingerprint(x): Product of (γ - hash(write)) for all writes up to cycle x
  • read_fingerprint(x): Product of (γ - hash(read)) for all reads up to cycle x
  • final_ratio: Should equal 1 if R ⊆ W
Incremental computation: Fingerprints are computed incrementally: 
fingerprint[i+1] = fingerprint[i] · (γ - hash(access[i+1]))
This allows efficient sumcheck evaluation without materializing full products.

​
Read-After-Final (RAF) Polynomial

Jolt uses a Read-After-Final (RAF) polynomial to detect invalid reads:

​
Definition

RAF[addr, time] = {
    1  if there exists a read from addr after the final write to addr
    0  otherwise
}

​
Purpose

RAF detects two error cases:
  1. No writes: Register never written but is read
  2. Stale reads: Read after execution ends (shouldn’t happen in valid trace)

​
Sumcheck Integration

RAF is checked via a separate sumcheck: 
Σ_{addr, time} RAF[addr, time] · read_flag[addr, time] = 0
If RAF=1 for any read, the check fails.

​
Initial and Final States

​
Initial Register State

Most registers: Initialize to 0 
reg[x0] = 0  (hardwired)
reg[x1..x31] = 0
Stack pointer: Initialize to top of stack 
reg[sp] = memory_layout.stack_top
Initial writes are included in the write multiset W.

​
Final Register State

Not checked: Register values at program end are not constrained (only consistency during execution matters). Termination: Detected by heuristic (PC stops changing) rather than explicit register state.

​
Implementation Details

​
Module Structure

val_evaluation.rs:
  • Computes register value evaluations at challenge points
  • Uses multilinear polynomial evaluation over trace
read_write_checking.rs:
  • Implements fingerprint-based memory checking sumcheck
  • Handles incremental fingerprint computation
  • Verifies RAF polynomial is zero

​
Key Types

RegisterValEvaluationParams: 
pub struct RegisterValEvaluationParams<F: JoltField> {
    pub r: Vec<F::Challenge>,  // Evaluation point
    // ... metadata ...
}
RegisterReadWriteCheckingParams: 
pub struct RegisterReadWriteCheckingParams<F: JoltField> {
    pub gamma: F::Challenge,      // Fingerprinting challenge
    pub init_fingerprint: F,      // Initial write fingerprint
    // ... metadata ...
}

​
Performance Characteristics

​
Prover Time

Register Val Evaluation:
  • O(trace_length · log(trace_length)) field operations
  • ~5-10% of total proving time
Read-Write Checking:
  • O(trace_length) field operations per round
  • ~10-15% of total proving time
  • Incremental fingerprint updates are efficient

​
Memory Usage

  • No materialized polynomials: Register values derived on-the-fly from trace
  • Streaming: Uses streaming sumcheck windows for memory efficiency
  • Typical usage: ~10-20MB for 10⁶ cycles

​
Verifier Time

  • O(log(trace_length)) field operations
  • Verifies sumcheck round polynomials
  • ~0.1-1ms for typical traces

​
Comparison with RAM Checking

Register checking is simpler than RAM checking:
AspectRegister CheckingRAM Checking
Address space32 registers2^K memory words
InitializationAll zeros + spBytecode + inputs
Read-after-finalSimple RAF checkComplex RAF with advice
Performance~10-15% proving time~30-40% proving time
However, the underlying protocol is identical (multiset-based offline memory checking).

​
Key Files

  • jolt-core/src/zkvm/registers/val_evaluation.rs: Register value evaluation sumcheck
  • jolt-core/src/zkvm/registers/read_write_checking.rs: Fingerprint-based consistency checking
  • jolt-core/src/zkvm/claim_reductions/: Final claim aggregation

​
Next Steps

Build docs developers (and LLMs) love

Get started for freeTalk to us