Jolt Constraints

In progresss

At this point we have that the Jolt ISA is expressive enough to simulate the RISC-V CPU^[1]. Thus, from here onwards, we can forget that the input to Jolt is a RISC-V program, and just pretend the input is a program written in the Jolt ISA. This post is about how we go from guest program to an NP witness, and how we define constraints over this witness space. The picture you should have is the following:

TODO picture.

The Jolt Program And Initial State#

You start with a Jolt program and some initial jolt state.

/-- Static bytecode and the complete initial state for one execution.
Rust stores the [program image](jolt/crates/jolt-program/src/execution/trace.rs:17)
and [execution inputs](jolt/crates/jolt-program/src/execution/trace.rs:129)
separately; 
-/
structure JoltProgram where
  -- Rust: JoltProgram::expanded_bytecode.
  expandedBytecode : Array JoltProgramRow
  -- Rust: [create_emulator](jolt/tracer/src/lib.rs:366).
  initialState : SailJoltState

A JoltProgram is an array of Jolt Instructions which is defined in lean to mimick to the rust implementation. Notice that the instruction field re-uses our Lean Jolt ISA.

-- Rust: crates/jolt-riscv/src/row.rs::JoltInstructionRow.
structure JoltProgramRow where
  instruction : JoltISA.Instr
  address : BitVec 64
  virtualSequenceRemaining : Option (BitVec 16)
  isFirstInSequence : Bool
  isCompressed : Bool

Given this initial state and guest program, the Jolt tracers first task is to simply execute this program to get a trace

The Trace (Jolt Executes The Guest Program)#

structure JoltTrace (program : JoltProgram) where
  rows : Array (JoltTraceRow program)
  startsAtInitial : ∀ h : 0 < rows.size, (getElem rows 0 h).preState = program.initialState
  linked : ∀ (i : Nat) (currentExists : i < rows.size) (nextExists : i + 1 < rows.size),
    (getElem rows i currentExists).postState = (getElem rows (i + 1) nextExists).preState

The fields of the structure are as follows. rows is an array of trace rows which snapshots the jolt state before and after execution. Let $T$ denote the number of cycles this guest program runs for (below T = program.expandedBytecode.size). Then rowIndex $\in [T]$. executes is an assumption that instruction retires successfully i.e. the guest program is even runnable. If this were not true then Jolt is not required to do anything. Finally, as the memory is implemented as a hashmap we assume the key exists. TODO: Tidy this up

structure JoltTraceRow (program : JoltProgram) where
  rowIndex : Fin program.expandedBytecode.size
  preState : SailJoltState
  postState : SailJoltState
  executes : JoltISA.execInstr program.expandedBytecode[rowIndex].instruction preState =
    .ok (.Retire_Success ()) postState

  -- Rust: [trace_store](/Users/ari.biswas/Work-with-A16z/jolt/tracer/src/emulator/mmu.rs:609)
  -- reads the old word before every store. For RAM, this certifies that all eight
  -- bytes exist in preState.sail.mem; for device memory, it certifies a valid read
  -- from preState.io. Successful Sail writes alone do not establish this fact.
  storeMemoryPresent :
    match program.expandedBytecode[rowIndex].instruction with
    | .SD base _ imm =>
        (JoltISA.memoryWord? preState
          (Memory.effectiveAddr12 (JoltISA.sourceValue base preState) imm)).isSome = true
    | _ => True

Witness#

At this point we have a guest program. We have run every instruction successfully. We have stored the before/after state after the execution of each instruction. From this information, we want to create a term of type Witness. Or in normal speak, we have a bunch of arrays whose cells need filling. The honest tracer is meant to fill these values using the before/after state information it got from tracing the code.

The picture looks like this TODO:

In Lean, Witness is a dependent type that depends on the Parameters which define how the size of the above arrays.

structure WitnessParams where
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/dimensions.rs::TraceDimensions::log_t.
  -- Base-two logarithm of the padded witness length; actual execution may be shorter.
  logT : Nat
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/dimensions.rs::ReadWriteDimensions::log_k.
  logRamK : Nat
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/bytecode.rs::BytecodeReadRafDimensions::log_k.
  logBytecodeK : Nat
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/dimensions.rs::JoltOneHotDimensions::committed_chunk_bits.
  chunkBits : Nat
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/dimensions.rs::JoltOneHotDimensions::lookup_virtual_chunk_bits.
  virtualChunkBits : Nat
  -- Rust: crates/jolt-claims/src/protocols/jolt/geometry/dimensions.rs::JoltFormulaDimensions::try_from.
  chunkBits_pos : 0 < chunkBits
  virtualChunkBits_pos : 0 < virtualChunkBits
  chunkBits_dvd_virtual : chunkBits ∣ virtualChunkBits
  virtualChunkBits_dvd_lookup : virtualChunkBits ∣ 128