Ari

Ram Ra

jolt
By Ari

RamRa Construction: Tracking Memory Accesses

What is RamRa?

RamRa (RAM Read Address) is a collection of ram_d polynomials that track which memory address each cycle accesses. Like BytecodeRa, we chunk addresses into smaller pieces for efficient lookup proofs.

Structure:

RamRa = [
    RamRa[0]: Vec<Option<u8>>,  // First chunk, length = trace_length
    RamRa[1]: Vec<Option<u8>>,  // Second chunk, length = trace_length
    ...
    RamRa[ram_d-1]: Vec<Option<u8>>, // Last chunk, length = trace_length
]

Key difference from BytecodeRa: Not every cycle accesses memory! Cycles without RAM access store None.

The Construction Process

Input Data

1. RAMPreprocessing - Dense word storage from earlier:

RAMPreprocessing {
    min_bytecode_address: 0x7fffa000,  // Lowest memory address used
    bytecode_words: [
        0x0000000000000002,  // 8 bytes at 0x7fffa000-0x7fffa007
        ...
    ]
}

2. Memory Layout - Defines valid memory regions:

MemoryLayout {
    input_start: 0x7fffa000,
    input_end: 0x7fffafff,
    output_start: 0x7fffb000,
    output_end: 0x7fffbfff,
    ...
}

3. Execution Trace - Cycles with memory accesses:

Cycle 0-7:   No RAM access
Cycle 8:     No RAM access
Cycle 9:     No RAM access
Cycle 10:    RAMRead { address: 0x7fffa000, value: 2 }
Cycle 11-59: Various RAM accesses...
Cycle 60:    RAMWrite { address: 0x7fffb008, pre: 0, post: 1 }

Step-by-Step Construction

if let Some(dth_log) = dth_root_log {
    let address_opt = remap_address(
        cycle.ram_access().address() as u64,
        &preprocessing.shared.memory_layout,
    );
    for j in 0..ram_d {
        let index = address_opt.map(|address| {
            ((address as usize >> (dth_log * (ram_d - 1 - j))) % DTH_ROOT_OF_K) as u8
        });
        batch_ref.ram_ra[j][i] = index;
    }
}

For each cycle i:

Step 1: Get Memory Address (if any)

let mem_address = cycle.ram_access().address();

If no RAM access, all RamRa[j][i] = None.

Step 2: Remap Address to Relative Offset

let address_opt = remap_address(mem_address, &memory_layout);

The remap_address function converts absolute memory addresses into relative word indices:

pub fn remap_address(address: u64, memory_layout: &MemoryLayout) -> Option<u64> {
    if address == 0 {
        return None;  // Address 0 means no memory access
    }
    let lowest_address = memory_layout.get_lowest_address();
    if address >= lowest_address {
        Some((address - lowest_address) / 8)  // Divide by 8 for word index
    } else {
        panic!("Unexpected address {address}")
    }
}
  1. Returns None for address 0 - indicates no memory access
  2. Subtracts lowest_address - creates relative offset from program’s memory base
    • In your program: lowest_address = 0x7FFF8000 = 2147450880
  3. Divides by 8 - converts byte address to word index (since memory is stored as 8-byte words)

Why divide by 8? Remember RAMPreprocessing stores memory as Vec<u64> (8-byte words). The remapped address is actually a word index into that array, not a byte offset!

Examples from your program:

// Byte address: 0x7FFFA000 (reading at location)
// lowest_address: 0x7FFF8000
// Remapped: (0x7FFFA000 - 0x7FFF8000) / 8 = 0x2000 / 8 = 8192 / 8 = 1024 (word index 1024)

// Byte address: 0x7FFFB000 (reading at location)
// lowest_address: 0x7FFF8000
// Remapped: (0x7FFFB000 - 0x7FFF8000) / 8 = 0x3000 / 8 = 12288 / 8 = 1536 (word index 1536)

// Byte address: 0x7FFFC008 (writing at location)
// lowest_address: 0x7FFF8000
// Remapped: (0x7FFFC008 - 0x7FFF8000) / 8 = 0x4008 / 8 = 16392 / 8 = 2049 (word index 2049)

Step 3: Chunk the Remapped Address

for j in 0..ram_d {
    let shift = dth_log * (ram_d - 1 - j);
    let index = (remapped_address >> shift) % DTH_ROOT_OF_K;
    RamRa[j][i] = Some(index as u8);
}

Chunking parameters: - ram_d = number of chunks (determined by memory size) - dth_log = bits per chunk - DTH_ROOT_OF_K = 2^dth_log (size of each lookup table)

Concrete Example 1: Cycle 10 (Memory Read)

Cycle 10: LD {
    instruction: LD {
        address: 2147483714,  // Instruction at 0x80000042
        operands: FormatLoad { rd: 34, rs1: 33, imm: 0 },
        virtual_sequence_remaining: Some(5),
    },
    ram_access: RAMRead {
        address: 2147459072,  // 0x7fffa000 (input buffer)
        value: 2,
    }
}

Step 1: Get RAM address

mem_address = 2147459072  // 0x7fffa000

Step 2: Remap to relative word index

lowest_address = 0x7fff8000  // Start of memory region
byte_offset = 0x7fffa000 - 0x7fff8000 = 0x2000 = 8192 bytes
word_index = 8192 / 8 = 1024

Step 3: Chunk the word index

With ram_d = 2 and dth_log = 8 (so DTH_ROOT_OF_K = 256):

// 1024 in binary: 0000 0100 0000 0000
// 1024 = 4 * 256 + 0

j = 0: shift = 8
       index = (1024 >> 8) % 256 = 4
       RamRa[0][10] = Some(4)

j = 1: shift = 0
       index = (1024 >> 0) % 256 = 0
       RamRa[1][10] = Some(0)

Result: RAM byte address 0x7fffa000 → word index 1024 → chunked as [4, 0]

Verify reconstruction: 4 * 256 + 0 = 1024

This matches our actual RamRa output!

Concrete Example 2: Cycle 60 (Memory Write)

Cycle 60: SD {
    ram_access: RAMWrite {
        address: 2147467272,  // 0x7FFFC008
        pre_value: 0,
        post_value: 1,
    }
}

Step 1: Get RAM address

mem_address = 2147467272  // 0x7FFFC008

Step 2: Remap to relative word index

lowest_address = 0x7FFF8000  // Start of memory region
byte_offset = 0x7FFFC008 - 0x7FFF8000 = 0x4008 = 16392 bytes  
word_index = 16392 / 8 = 2049

Step 3: Chunk the word index

With ram_d = 2 and dth_log = 8:

// 2049 in binary: 0000 1000 0000 0001
// 2049 = 8 * 256 + 1

j = 0: shift = 8
       index = (2049 >> 8) % 256 = 8
       RamRa[0][60] = Some(8)

j = 1: shift = 0
       index = (2049 >> 0) % 256 = 1
       RamRa[1][60] = Some(1)

Result: RAM byte address 0x7FFFC008 → word index 2049 → chunked as [8, 1]

Verify reconstruction: 8 * 256 + 1 = 2048 + 1 = 2049 ✓

Concrete Example 3: Cycle 8 (No Memory Access)

Cycle 8: ADDI {
    // No RAM access - just register operations
}

Result:

RamRa[0][8] = None
RamRa[1][8] = None

Not every cycle accesses memory, so we use Option<u8> to represent “no access.”

The Complete RamRa Polynomials (Your Actual Trace)

After processing all 63 cycles in your trace, here are the actual values:

RamRa[0] = [
    None, None, None, None, None, None, None, None, None, None,
    Some(4),   // Cycle 10: word index 1024 (input buffer read)
    None, None, None, None, None, None, None, None, None, None,
    None, None, None, None, None, None, None, None, None, None,
    None, None, None, None, None, None,
    Some(6),   // Cycle 37: word index 1536
    None, None, None, None, None, None, None, None, None,
    Some(6),   // Cycle 47: word index 1536 (same address)
    None, None,
    Some(8),   // Cycle 50: word index 2049 (output buffer)
    None, None, None, None, None, None, None, None, None,
    Some(8),   // Cycle 60: word index 2049 (same address, write)
    None, None, None,
]

RamRa[1] = [
    None, None, None, None, None, None, None, None, None, None,
    Some(0),   // Cycle 10: chunk 1 of word 1024
    None, None, None, None, None, None, None, None, None, None,
    None, None, None, None, None, None, None, None, None, None,
    None, None, None, None, None, None,
    Some(0),   // Cycle 37: chunk 1 of word 1536
    None, None, None, None, None, None, None, None, None,
    Some(0),   // Cycle 47: chunk 1 of word 1536
    None, None,
    Some(1),   // Cycle 50: chunk 1 of word 2049
    None, None, None, None, None, None, None, None, None,
    Some(1),   // Cycle 60: chunk 1 of word 2049
    None, None, None,
]

Memory access summary: - Cycle 10: Read from word 1024 → [4, 0] - Cycle 37: Access word 1536 → [6, 0] - Cycle 47: Access word 1536 → [6, 0] (same location as cycle 37) - Cycle 50: Read from word 2049 → [8, 1] - Cycle 60: Write to word 2049 → [8, 1] (same location as cycle 50)

Notice that cycles 37 and 47 access the same word (1536), and cycles 50 and 60 access the same word (2049).

Connection to RAMPreprocessing

Remember the RAMPreprocessing structure we built earlier? It stores memory as 8-byte words:

RAMPreprocessing {
    min_bytecode_address: 0x7FFF8000,  // = 2147450880 = lowest_address
    bytecode_words: [
        ...                          // Word 0: bytes 0x7FFF8000-0x7FFF8007
        ...                          // Word 1024: bytes 0x7FFFA000-0x7FFFA007
        ...                          // Word 1536: bytes 0x7FFFB000-0x7FFFB007
        ...                          // Word 2049: bytes 0x7FFFC008-0x7FFFC00F
    ],
}

The remapping creates perfect alignment: - RAMPreprocessing stores memory as bytecode_words[word_index] - RamRa chunks the same word_index for lookups - Both work with word-aligned indices, not byte addresses

When the verifier checks memory accesses, they can: 1. Reconstruct word index from RamRa chunks: word_index = RamRa[0] * 256 + RamRa[1] 2. Look up in RAMPreprocessing: bytecode_words[word_index] 3. Verify the memory operation was correct

Why Option?

Unlike BytecodeRa where every cycle executes an instruction, not every cycle accesses memory: - Cycles with LD/SD/etc. → Some(chunk_value) - Cycles with ADDI/MUL/etc. → None

Summary

Input: - Memory accesses from trace (byte addresses) - Memory layout (provides lowest_address for remapping) - RAMPreprocessing (word-aligned storage)

Process: For each cycle i: 1. Check if cycle accesses memory 2. If yes: Get absolute byte address 3. Remap to relative word index: (address - lowest_address) / 8 4. Chunk word index into ram_d pieces using bit shifts 5. Store chunks in RamRa[0][i], RamRa[1][i], …, RamRa[ram_d-1][i] 6. If no: Store None in all RamRa polynomials

Output: ram_d polynomials tracking memory accesses as word indices, ready for memory consistency checks in the proof.