> ## 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.

# RAM Read-Write Checking

> Learn how Jolt verifies memory consistency across the execution trace

## 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**:

```rust theme={null}
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](/architecture/opening-proof) for batching details.

## Initial and Final Memory States

### Initial State Construction

```rust theme={null}
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

```rust theme={null}
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:

```rust theme={null}
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

```rust theme={null}
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

```rust theme={null}
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

* [Register Checking](/architecture/registers): Simpler version of same protocol
* [Bytecode](/architecture/bytecode): Program image preprocessing
* [Opening Proofs](/architecture/opening-proof): Batched commitment verification