Bytecode

Jolt proves the validity of registers and RAM using offline memory checking.

Decoding an ELF file

The tracer iterates over the .text sections of the program ELF file and decode RISC-V instructions. Each instruction gets mapped to a BytecodeRow struct:

#![allow(unused)]
fn main() {
pub struct BytecodeRow {
    /// Memory address as read from the ELF.
    address: usize,
    /// Packed instruction/circuit flags, used for r1cs
    bitflags: u64,
    /// Index of the destination register for this instruction (0 if register is unused).
    rd: u64,
    /// Index of the first source register for this instruction (0 if register is unused).
    rs1: u64,
    /// Index of the second source register for this instruction (0 if register is unused).
    rs2: u64,
    /// "Immediate" value for this instruction (0 if unused).
    imm: u64,
}
}

The registers (rd, rs1, rs2) and imm are described in the RISC-V spec. The bitflags field is described in greater detail below.

The preprocessed bytecode serves as the (read-only) "memory" over which we perform offline memory checking.

We currently assume the program bytecode is sufficiently short and known by the verifier, so the prover doesn't need to provide a commitment to it –– the verifier can compute the MLE of the bytecode on its own. This guarantees that the bytecode trace is consistent with the agreed-upon program.

Instead of $(a,v,t)$ tuples, each step in the bytecode trace is mapped to a tuple $(a,v_{\text{bitflags}},v_{\text{rd}},v_{\text{rs1}},v_{\text{rs2}},v_{\text{imm}},t)$. Otherwise, the offline memory checking proceeds as described in Offline Memory Checking.

Bitflags

The bitflags of a given instruction is the concatenation of its circuit flags and instruction flags. This concatenation is enforced by R1CS constraints.