The Jolt-qed project verifies, in Lean, that each Jolt bytecode expansion has the same effect as the RISC-V instruction it replaces. These equivalence theorems are not unconditional: they rely on explicit hypotheses about the RISC-V/Jolt state, plus a small number of trusted edits to the generated RISC-V model so that it matches the Jolt CPU. This post records those proof assumptions and trusted-code changes.

Changes to the Trusted RISC-V Model

The Lean RISC-V model lives in LeanRV64D/, with the top-level entry point in LeanRV64D.lean. It was generated by automatically transpiling the Sail specification of a RISC-V CPU to Lean1. The Sail-to-Lean post explains how we obtained this generated code. We treat that generated model as trusted throughout the project, except for the two changes below.

1

This translation was done by Galois and researchers at Cambridge University. See the Sail-to-Lean post for further details.

  1. We say that the RISC-V CPU should not support misaligned memory addressing. We do this because Jolt does not support misaligned addressing, and it would be impossible to prove equivalence otherwise. The Ethereum zkVM Standards v0 recommend that zk-VMs use RV64IM+Zicclsm as the target baseline, where Zicclsm is included to support misaligned loads and stores. We highlight this drawback off the bat.
-- WARNING: CHANGE IN TRANSPILED CODE
def plat_enable_misaligned_access : Bool := false
  1. Jolt does not support the Zicfiss and Zicfilp extensions. Leaving them on makes it impossible to prove equivalences about writing to control status registers.
-- WARNING: (change to sail, Jolt does not support Zicfilp extension).
| Ext_Zicfilp => false
-- WARNING: (change to sail, Jolt does not support Zicfiss extension).
| Ext_Zicfiss => false

These are the only changes we make to the generated RISC-V model.

Equivalence Statement Structure

Shown below is the equivalence statement for the sra instruction. It says that running the Jolt instruction sraProgram with arguments rd rs2 rs1 on the current Jolt state js, and then projecting down to the RISC-V state, is identical to running sra rd rs2 rs1 on the RISC-V state of the current Jolt CPU. In simple words, we could either run the original RISC-V instruction or run the Jolt expansion on the same starting state, and the effect is the same. If we showed this for all RISC-V instructions, then we would show that Jolt faithfully simulates RISC-V. Now to prove this theorem, we use an assumption bundle. The goal of this post is to explain what an assumption bundle is.

/-- Main program-level equivalence for `SRA`. -/
def sraProgramEqSailStatement
    (rs2 : regidx)
    (rs1 : regidx)
    (rd : regidx)
    (js : SailJoltState)
    (_h : BinarySourceReadWithLinkedCSRs rs2 rs1 js) -- <--- Assumption bundle
  : Prop :=
  System.systemProjectResult
      ((JoltISA.execProgram (JoltISA.sraProgram rs2 rs1 rd)).run js) =
    (execute_RTYPE rs2 rs1 rd rop.SRA).run js.sail

Assumption bundles are conjunctions of assumptions defined in JoltBytecode/Assumptions.lean and collected in JoltBytecode/Bundles.lean. Each equivalence statement in Jolt-qed uses an assumption bundle. Bundles describe exactly which assumptions were used to prove equivalence for a given instruction. An assumption bundle is always made up of a list of assumptions2.

2

We could not figure out a way to get the Lean kernel to enforce this in a clean manner without completely redoing the project. So we do this manually by enforcing that each field uses something from the Assumptions namespace. If you, the reader, know a better way to do this, please reach out with a pull request.

This specific assumption bundle is made up of the two groups of assumptions shown below.

abbrev BinarySourceReadAssumptions
    (rs2 rs1 : regidx) (js : SailJoltState) :=
  Assumptions.BinarySourceReadAssumptions rs2 rs1 js.sail

private structure LinkedCSRRegisterAssumptions (js : SailJoltState) where
  mstatus_matches : Assumptions.MstatusVRegMatchesSail js
  mtvec_matches : Assumptions.MtvecVRegMatchesSail js
  mscratch_matches : Assumptions.MscratchVRegMatchesSail js
  mepc_matches : Assumptions.MepcVRegMatchesSail js
  mcause_matches : Assumptions.McauseVRegMatchesSail js
  mtval_matches : Assumptions.MtvalVRegMatchesSail js

We will explain what these mean below, but the takeaway message is that every equivalence theorem uses an assumption bundle. Any assumption bundle can only be made up of core assumptions listed in Assumptions.lean.

Assumptions

For the rest of the document, we list every assumption used in Jolt. If any assumption that is not listed here, or in Assumptions.lean, is used in a proof bundle, then that should be remedied immediately, and we should check whether the assumption is justified.

Privilege Is Always Machine

structure CurPrivilegeMachine (s : SailState) : Prop where
  value : s.regs.get? Register.cur_privilege =
    some (Privilege.Machine : RegisterType Register.cur_privilege)

In simple English, the value in current_privilege indicates that the Jolt CPU runs in machine mode all the time. According to the Jolt Rust code base, Jolt always runs in machine mode. The above Lean code simply states that the value in the cur_privilege register is Privilege.Machine.

MPP Bit Set To Machine

structure MstatusMppMachine (js : SailJoltState) : Prop where
  value_eq :
    _get_Mstatus_MPP (js.vregs JoltISA.mstatusVReg) =
      privLevel_to_bits Privilege.Machine

Jolt uses virtual register 39 to model the mstatus control status register of the Jolt CPU. Based on the Jolt source code, Jolt always runs in machine mode, and the MPP bit of the status register is always set to Machine.

MISA User Enabled

structure MisaUserEnabled (s : SailState) : Prop where
  exists_value : ∃ misa : BitVec 64,
    s.regs.get? Register.misa = some (misa : RegisterType Register.misa) ∧
    _get_Misa_U misa = 1#1

Jolt initialises misa to 0x800000008014312f based on jolt/tracer/src/emulator/cpu.rs:399. The function _get_Misa_U reads bit 20 of the misa CSR, which, based on the written value, is 1. According to the RISC-V ISA, having bit 20 set to 1 implies user mode is enabled.

MPRV Bit

structure MstatusMprvZero (s : SailState) : Prop where
  value : ∃ mval : RegisterType Register.mstatus,
    s.regs.get? Register.mstatus = some mval ∧
    _get_Mstatus_MPRV mval = 0#1

According to Jolt, the MPRV bit of the mstatus register is set to 0 in Jolt. As a direct consequence of this, we get bare translation: virtual addresses are the same as physical addresses, which is also true in the Jolt code base. In Lean, this is captured by the following three bare-translation theorems for loads, stores, and atomics. We only show the theorem statements here; the proofs are in JoltBytecode/InstructionEquivalence/ProofSupport/BundleLemmas.lean.

theorem translateAddr_load_data_of_machine_mprv_zero
    (addr : BitVec 64) (s : SailState)
    (hpriv : Assumptions.CurPrivilegeMachine s)
    (hmprv : Assumptions.MstatusMprvZero s) :
    translateAddr (Virtaddr addr) (Load Data) s =
      .ok (Ok (physaddr.Physaddr addr, init_ext_ptw)) s
theorem translateAddr_store_data_of_machine_mprv_zero
    (addr : BitVec 64) (s : SailState)
    (hpriv : Assumptions.CurPrivilegeMachine s)
    (hmprv : Assumptions.MstatusMprvZero s) :
    translateAddr (Virtaddr addr) (Store Data) s =
      .ok (Ok (physaddr.Physaddr addr, init_ext_ptw)) s
theorem translateAddr_atomic_data_of_machine_mprv_zero
    (op : amoop) (addr : BitVec 64) (s : SailState)
    (hpriv : Assumptions.CurPrivilegeMachine s)
    (hmprv : Assumptions.MstatusMprvZero s) :
    translateAddr (Virtaddr addr) (Atomic (op, Data, Data)) s =
      .ok (Ok (physaddr.Physaddr addr, init_ext_ptw)) s

Zicfilp Extension

structure ZicfilpDisabled (s : SailState) : Prop where
  value : currentlyEnabled extension.Ext_Zicfilp s = .ok false s

Jolt does not support the Zicfilp extension.

Mtvec

structure MtvecWriteDirectMode (value : BitVec 64) : Prop where
  mode_eq : _get_Mtvec_Mode value = 0b00#2

The RISC-V ISA requires that we legalise values before writing to control and status registers. See this blog for more details. When writing the contents of rs1 into the mtvec control and status register, if the value in rs1 has the two least significant bits set to 00, then we write rs1's contents directly into mtvec. Otherwise, we need to legalise the value. The above assumption says the value in rs1 will always have the lower two bits set to 00.

The ZeroOS/Jolt boot path writes _trap_handler to mtvec with

csrw mtvec, t0

ZeroOS defines _trap_handler under .align 2, which gives 4-byte alignment, so the lower two bits are 00. Evidence from ZeroOS source code is given below.

The ZeroOS boot code writes to mtvec, and the trap handler definition is aligned.

Warning

This assumption holds when we use the write to mtvec operation as it is meant to be used in Jolt. If a malicious program were to write a different value to Jolt mtvec, Jolt does not have any mechanism to legalise the value. In that case, Jolt would not be following the RISC-V spec. We will rely on the proof mechanism to catch this.

Align PC

Jolt supports compressed instructions (+c / RV64IMAC), as seen here, so we can only guarantee that the least significant bit of PC is 0. The relevant assumption is that mepc[0] = 0. Thus, the legalisation operation according to the specification is a no-op because the lowest bit is already cleared.

structure MepcReadAligned (value : BitVec 64) (s : SailState) : Prop where
  value_eq : align_pc value s = .ok value s

This is the write-side counterpart of MepcReadAligned: CSRRW writes the new rs1 value, so the assumption must be about that source value rather than only the old stored mepc.

structure MepcWriteLegalized (value : BitVec 64) : Prop where
  value_eq : legalize_xepc value = value

Legalise MStatus

structure MstatusWriteLegalized
    (old value : BitVec 64) (s : SailState) : Prop where
  value_eq : legalize_mstatus old value s = .ok value s

Jolt does not legalise before writing to mstatus. The evidence is in the Jolt CSR expansions: CSRRW writes rs1 directly into the CSR virtual register, and CSRRS writes the OR of the old CSR value and rs1. See csrrw.rs and csrrs.rs.

Virtual Register Modelling

Here we are saying that certain virtual registers in Jolt correspond to the control status registers in the Sail state. We could have written directly to the Sail registers in our Jolt semantics, but to be faithful to the Jolt expansion, we write the virtual registers and record that correspondence as an assumption. The Jolt code confirms this.

/-- Sail `mstatus` agrees with Jolt's persistent `mstatus` virtual register. -/
structure MstatusVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mstatus =
      some (js.vregs JoltISA.mstatusVReg)

/-- Sail `mtvec` agrees with Jolt's persistent trap-handler virtual register. -/
structure MtvecVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mtvec =
      some (js.vregs JoltISA.trapHandlerVReg)

/-- Sail `mscratch` agrees with Jolt's persistent `mscratch` virtual register. -/
structure MscratchVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mscratch =
      some (js.vregs JoltISA.mscratchVReg)

/-- Sail `mepc` agrees with Jolt's persistent `mepc` virtual register. -/
structure MepcVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mepc =
      some (js.vregs JoltISA.mepcVReg)

/-- Sail `mcause` agrees with Jolt's persistent `mcause` virtual register. -/
structure McauseVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mcause =
      some (js.vregs JoltISA.mcauseVReg)

/-- Sail `mtval` agrees with Jolt's persistent `mtval` virtual register. -/
structure MtvalVRegMatchesSail (js : SailJoltState) : Prop where
  value_eq :
    js.sail.regs.get? Register.mtval =
      some (js.vregs JoltISA.mtvalVReg)

Memory Assumptions

structure DwordPresent (addr : BitVec 64) (s : SailState) : Prop where
  bytes :
    ∃ bytes : Fin 8 → BitVec 8,
      ∀ k : Fin 8, s.mem.get? (addr.toNat + k.val) = some (bytes k)

Lean models memory as a hash map from natural numbers to 8-bit bitstrings. The natural numbers are countably infinite, while the address space of any CPU is not. Additionally, because memory is modelled as a hash map, Lean needs a hypothesis that the key already exists before it can retrieve the value. This is a proof-engineering issue: the generated model represents memory as a partial map, so we must state that the relevant bytes are present. Thus, the following assumption says that addresses can be read from memory and that they return valid bytes across the entire doubleword window.

abbrev LoadPmpOk (addr : BitVec 64) (width : Nat) (s : SailState) : Prop :=
  phys_access_check (Load Data) Privilege.Machine
    (physaddr.Physaddr addr) width false s = .ok none s

/-- Machine-mode PMP accepts every explicit sub-load inside a memory window. -/
structure LoadPmpOkWindow
    (base : BitVec 64) (width : Nat) (s : SailState) : Prop where
  ok :
    ∀ offset accessWidth : Nat, offset + accessWidth ≤ width →
      LoadPmpOk (base + BitVec.ofNat 64 offset) accessWidth s

abbrev StorePmpOk (addr : BitVec 64) (width : Nat) (s : SailState) : Prop :=
  phys_access_check (Store Data) Privilege.Machine
    (physaddr.Physaddr addr) width false s = .ok none s

/-- Machine-mode PMP accepts every explicit sub-store inside a memory window. -/
structure StorePmpOkWindow
    (base : BitVec 64) (width : Nat) (s : SailState) : Prop where
  ok :
    ∀ offset accessWidth : Nat, offset + accessWidth ≤ width →
      StorePmpOk (base + BitVec.ofNat 64 offset) accessWidth s

abbrev AtomicPmpOk
    (op : amoop) (addr : BitVec 64) (width : Nat) (s : SailState) : Prop :=
  phys_access_check (Atomic (op, Data, Data)) Privilege.Machine
    (physaddr.Physaddr addr) width true s = .ok none s

/-- Machine-mode PMP accepts every explicit sub-AMO inside a memory window. -/
structure AtomicPmpOkWindow
    (op : amoop) (base : BitVec 64) (width : Nat) (s : SailState) : Prop where
  ok :
    ∀ offset accessWidth : Nat, offset + accessWidth ≤ width →
      AtomicPmpOk op (base + BitVec.ofNat 64 offset) accessWidth s

Jolt's Rust MMU explicitly says memory protection is not implemented. These predicates constrain the generated RISC-V model to the corresponding no-PMP-fault path.

Rust source: https://github.com/abiswas3/jolt/blob/main/tracer/src/emulator/mmu.rs#L17.

The above assumption says the entire doubleword block read by LD at physical address addr is not protected and can be read. The same applies to writing to memory. To prove equivalence, we need to tell the generated RISC-V model that the address is safe to read from or write to. The generated RISC-V model uses different checks for LD, SD, and atomic operations, so we need three sets of assumptions that say the same thing.

abbrev NotReadableMmio (addr : BitVec 64) (width : Nat) (s : SailState) : Prop :=
  within_mmio_readable (physaddr.Physaddr addr) width s = .ok false s

structure NotReadableMmioWindow
    (base : BitVec 64) (width : Nat) (s : SailState) : Prop where
  ok :
    ∀ offset accessWidth : Nat, offset + accessWidth ≤ width →
      NotReadableMmio (base + BitVec.ofNat 64 offset) accessWidth s

abbrev NotWritableMmio (addr : BitVec 64) (width : Nat) (s : SailState) : Prop :=
  within_mmio_writable (physaddr.Physaddr addr) width s = .ok false s

/-- Every explicit sub-store inside a memory window avoids writable MMIO. -/
structure NotWritableMmioWindow
    (base : BitVec 64) (width : Nat) (s : SailState) : Prop where
  ok :
    ∀ offset accessWidth : Nat, offset + accessWidth ≤ width →
      NotWritableMmio (base + BitVec.ofNat 64 offset) accessWidth s

Rust source: tracer/src/emulator/mmu.rs:139-213.

Jolt splits VM memory into reserved low-memory regions for advice, inputs, outputs, panic, and termination, followed by ordinary RAM. These regions share one VM address space and are mapped into the memory witness layout. Ordinary RAM is backed by the emulator memory map, while advice/input/output are modelled by JoltDevice.

Jolt does not support device MMIO such as UART, CLINT, PLIC, or disk; accesses to those ranges panic in the tracer. On the generated RISC-V side, memory operations can branch on memory-mapped device addresses, so the proof needs assumptions such as NotReadableMmio and NotWritableMmio to keep execution on the ordinary/Jolt-supported memory path.

Register Assumptions

structure XRegReadable (r : regidx) (s : SailState) : Prop where
  exists_value : ∃ value : BitVec 64, rX_bits r s = .ok value s

structure SailRegReadable (r : Register) (s : SailState) : Prop where
  exists_value : ∃ value : RegisterType r, s.regs.get? r = some value

/-- Assumptions for an instruction that reads one architectural source register. -/
structure UnarySourceReadAssumptions (rs1 : regidx) (s : SailState) where
  rs1_val : BitVec 64
  rs1_read : rX_bits rs1 s = .ok rs1_val s

/-- Assumptions for an instruction that reads two architectural source registers. -/
structure BinarySourceReadAssumptions
    (rs2 rs1 : regidx) (s : SailState) where
  rs1_val : BitVec 64
  rs1_read : rX_bits rs1 s = .ok rs1_val s
  rs2_val : BitVec 64
  rs2_read : rX_bits rs2 s = .ok rs2_val s

These assumptions say that the Sail register file is readable.