Before diving into the details of a theorem, we briefly review how the RISC-V CPU is currently modelled in the above transpilation. At the centre of the modelling decision is the SailM Monad.

The Sail Monad

SailM is the monad that all transpiled RISC-V instructions live in. Under the hood, it leverages Lean's built-in error-state monad, with the error and state types defined below. Note that EStateM ε σ α is just a function σ → Result ε σ α that takes a state and returns either .ok value newState or .error e newState.1 So what it really models is the step function of a single fetch-decode-execute cycle.

1

pure v constructs an EStateM computation that, when run, always returns .ok v s — it cannot error, the value is v, and the state s passes through unchanged.

See the official EStateM documentation for further details.

The Sail library defines a generic version called PreSailM, leaving the register types, choice source, and user-exception type as parameters:

abbrev PreSailM (RegisterType : Register → Type) (c : ChoiceSource) (ue : Type) :=
  EStateM (Error ue) (SequentialState RegisterType c)

SailM is just PreSailM instantiated with the RISC-V RegisterType, trivialChoiceSource, and exception:

abbrev SailM := EStateM (Error exception) SailState

State

abbrev SailState := SequentialState RegisterType trivialChoiceSource

SequentialState is the full machine state from the Sail model. It is parameterised by a function RegisterType : Register → Type and a ChoiceSource:

structure SequentialState (RegisterType : Register → Type) (c : ChoiceSource) where
  regs : Std.ExtDHashMap Register RegisterType
  choiceState : c.α
  mem : Std.ExtHashMap Nat (BitVec 8)
  tags : Unit
  cycleCount : Nat
  sailOutput : Array String

The regs field models the register file of the CPU. It is modelled in Lean as an Std.ExtDHashMap Register RegisterType — a hash map where the keys are of type Register and the value type depends on the key. That is, if the key is k : Register, the corresponding value has type RegisterType k. This is what makes it a dependent hash map rather than an ordinary one.

Register is an inductive with ~180 variants — one for every named register in the RISC-V spec:

inductive Register : Type where
  | hart_state
  | satp
  | PC
  | nextPC
  | x1 | x2 | x3 | ... | x31   -- general-purpose registers
  -- ... CSRs, vector registers, debug state, ~170 variants total ...

RegisterType is the function that tells the hash map what the type of the value is for each key:

abbrev RegisterType : Register → Type
  | .hart_state => HartState
  | .mhpmcounter => (Vector (BitVec 64) 32)
  | .tlb => (Vector (Option TLB_Entry) (2 ^ 6))
  | .PC => (BitVec 64)
  | .x1 => (BitVec 64)   -- all x1–x31 map to BitVec 64
  | .x2 => (BitVec 64)
  -- ...

So regs[.PC] has type RegisterType .PC = BitVec 64, while regs[.tlb] has type RegisterType .tlb = Vector (Option TLB_Entry) (2 ^ 6). Each register gets exactly the type it needs.

The mem field models byte-addressable memory as a hash map from Nat addresses to BitVec 8 bytes. The second parameter c : ChoiceSource provides a way to pick default values for primitive types when the spec needs to make a choice:

structure ChoiceSource where
  (α : Type)
  (nextState : Primitive → α → α)
  (choose : ∀ p : Primitive, α → p.reflect)
def trivialChoiceSource : ChoiceSource where
  α := Unit
  nextState _ _ := ()
  choose p _ :=
    match p with
    | .bool => false
    | .bit => 0
    | .int => 0
    | .nat => 0
    | .string => ""
    | .fin _ => 0
    | .bitvector _ => 0

We use trivialChoiceSource, which returns zeros, false, and empty strings for everything.

Errors

These are all the error variants. Error is from the Sail library:

inductive Error (ue : Type) where
  | Exit
  | Unreachable
  | OutOfMemoryRange (n : Nat)
  | Assertion (s : String)
  | User (e : ue)

The User constructor wraps a user-exception type ue, which is instantiated with exception from the RISC-V model:

inductive exception where
  | Error_not_implemented (_ : String)
  | Error_internal_error (_ : String)
  | Error_reserved_behavior (_ : String)

Execution Results

inductive ExecutionResult where
  | Retire_Success (_ : Unit)
  | ExecuteAs (_ : instruction)
  | Enter_Wait (_ : WaitReason)
  | Illegal_Instruction (_ : Unit)
  | Virtual_Instruction (_ : Unit)
  | Trap (_ : (Privilege × ctl_result × xlenbits))
  | Memory_Exception (_ : (virtaddr × ExceptionType))
  | Ext_CSR_Check_Failure (_ : Unit)
  | Ext_ControlAddr_Check_Failure (_ : ext_control_addr_error)
  | Ext_DataAddr_Check_Failure (_ : ext_data_addr_error)
  | Ext_XRET_Priv_Failure (_ : Unit)

In the happy path, instructions return RETIRE_SUCCESS (which is Retire_Success ()).

Register Indices

inductive regidx where
  | Regidx (_ : BitVec 5)

A 5-bit index into the 32 general-purpose RISC-V registers.

Jolt Monad

Jolt has virtual registers that are not present in the above state definition. So to model Jolt state we just define SailJoltState which is the Sail state with extra virtual registers:

structure SailJoltState where
  sail : SailState
  vregs : BitVec 7 → BitVec 64 := fun _ => 0
abbrev JoltMonad (α : Type) := EStateM (Error exception) SailJoltState α

Finally the Jolt Monad is just the same as SailM but with SailJoltState as state instead of SailState.

Helpers

Below are some helpers that we use to relate the Jolt Monad and the Sail Monad.

liftSail

liftSail takes a SailM α computation and runs it as a JoltMonad α computation:

def liftSail (m : SailM α) : JoltMonad α := fun js =>
  match m js.sail with
  | .ok a ss' => .ok a { js with sail := ss' }
  | .error e ss' => .error e { js with sail := ss' }

It takes the current SailJoltState (js), extracts the Sail state (js.sail), and runs the Sail computation m on it — m js.sail is direct function application, the same as m.run js.sail. Then it pattern matches on the result:

  • .ok a ss' — the computation succeeded with value a and new Sail state ss'. It rebuilds the SailJoltState by updating the sail field with ss' while keeping vregs unchanged.
  • .error e ss' — same, but propagates the error.

In other words, liftSail lets Jolt reuse Sail instructions directly — it runs them on the embedded Sail state and leaves the virtual registers untouched.

projectResult

projectResult strips the Jolt-specific state from an EStateM.Result, keeping only the SailState component:

def projectResult (r : EStateM.Result (Error exception) SailJoltState α) :
    EStateM.Result (Error exception) SailState α :=
  match r with
  | .ok a js' => .ok a (project js')
  | .error e js' => .error e (project js')

It pattern matches on the result — whether .ok or .error — and replaces the SailJoltState with just project js' (i.e. js'.sail), discarding the virtual registers.