Sail To Lean Translation

Since we started this project sometime around April of 2026, there have been improvements to Lean and the compiler. Quang Dao^[1] generously took the time to upgrade jolt-qed to use Lean version 4.35 (from 4.29), and a more up to date version of the sail compiler (PR #36). Additionally, Mathlib and lean-sail (the runtime library for the generated Lean code) were also upgraded. Last time, we did a poor job of describing how we get this “trusted” generated Lean code for the RISC-V instruction set architecture (ISA)^[2]. As enough files have changed, we feel we should give a detailed of account of what is going on. How do we get this trusted Lean code for the RISC-V ISA?

The Specification

There is a lot of code that is needed to get this translation, so we first, we introduce the characters of our play.

The Sail Files

The main character is the source specification of the RISC-V ISA. It is written in Sail, a domain-specific language for describing ISA semantics. This specification has been adopted by RISC-V International as the formal specification of the RISC-V ISA. The code can be found in the sail-riscv repository, at commit 266473f. These files describe the RISC-V ISA. How each instruction updates the RISCV cpu and the whole shabang.

As everything is clearer with a working example, here is some code from the specification that describes 6 RISC-V instructions.

function clause execute ITYPE(imm, rs1, rd, op) = {
  let immext : xlenbits = sign_extend(imm);
  X(rd) = match op {
    ADDI  => X(rs1) + immext,
    SLTI  => zero_extend(bool_to_bit(X(rs1) <_s immext)),
    SLTIU => zero_extend(bool_to_bit(X(rs1) <_u immext)),
    ANDI  => X(rs1) & immext,
    ORI   => X(rs1) | immext,
    XORI  => X(rs1) ^ immext
  };
  RETIRE_SUCCESS
}

Snippet 1: the specification code for 6 RISC-V instructions.

It is in model/extensions/I/base_insts.sail, lines 158–169. So this function in the specification is describing what happens when these 6 instructions are executed on a RISC-V CPU. Eventually, we will want an equivalent version of this in the generated Lean code.

The Modules

The RISC-V specification is a collection of 158 .sail files in the model/ folder of sail-riscv repository. Each file holds some code from the specification which describes something about the RISC-V ISA. A module is a named group of .sail files and other modules, together with a list of the modules it depends on. That was a mouthful. In more simple words, loosely, a module is the logical grouping of files in the project and a description of what those file depends on. Now there is a single file model/riscv.sail_project that lists every module, its .sail files and the modules it depends on. For example, here is the module I from that file. I is a module that itself contains the two modules I_types and I_insts, and it depends on the module core.

I {
  requires core

  I_types {
    before sys
    files extensions/I/base_types.sail
  }
  I_insts {
    requires exceptions, sys, I_types, Zicfilp_regs

    files
      extensions/I/base_insts.sail,
      if $RMEM then
        extensions/I/jalr_rmem.sail
      else
        extensions/I/jalr_seq.sail
  }
}

Snippet 2: the module I in model/riscv.sail_project.

The module I_types includes one file, extensions/I/base_types.sail. Its line before sys is not a dependency. It only tells the compiler^[3] to process I_types before the module sys.

The module I_insts depends on 4 other modules named exceptions, sys, I_types and Zicfilp_regs, and on the modules its parent modules depend on. RMEM is a flag that can be true or false, and only one of the two files jalr_rmem or jalr_seq is included. Dependency is described by require is what one might expect if they have programmed in any other language. In Snippet 1, the different variants of op were ADDI, SLTI and so on. Where did these names come from? They are defined in model/extensions/I/base_types.sail as shown below.

enum iop = {ADDI, SLTI, SLTIU, XORI, ORI, ANDI}  // immediate ops

Snippet 3: the names of the 6 instructions, in model/extensions/I/base_types.sail.

As I_types is required by I_insts, the compiler will know what files to pull in. Finally, we need some additional help to get the generated Lean code for the RISCV-cpu to build.

The Helpers

When writing the specification, the sail-riscv authors sometimes use functions whose body is not defined in any .sail file. For example, look at the following code from the specification in model/sys/sys_reservation.sail (Snippet 4):

val load_reservation = impure {interpreter: "Platform.load_reservation", cpp: "load_reservation", c: "load_reservation", lem: "load_reservation"} : forall 'n, 0 < 'n < max_mem_access . (/* addr */ physaddrbits, /* width */ int('n)) -> unit

Snippet 4: the declaration of load_reservation.

It says that there is a function called load_reservation, which takes an address and a width and returns nothing. It does not say what the function does, and no .sail file gives it a body. The list in braces gives, for each tool that runs the specification, the name of the function that tool should call.^[4] Lean is not in the list, so the generated Lean code calls load_reservation by its own name. The compiler will translate every call to load_reservation fine, but there is no body for it to translate. As a result, the generated Lean code will not build. For builds to pass, the sail-riscv authors handwrote some Lean code, which the compiler copies over to the generated Lean project unchanged. All this code is listed in one file, handwritten_support/RiscvExtras.lean. For load_reservation, the authors hand wrote this line of Lean code (Snippet 5):

axiom load_reservation : Arch.pa → Nat → SailM Unit

Snippet 5: the handwritten Lean stand-in for load_reservation, line 34 of handwritten_support/RiscvExtras.lean.

They too did not give it any body, but they gave it a type. This is enough for the generated Lean code to typecheck, but it is not enough for execution. This is part of the reason the generated Lean code is noncomputable.

Getting The Specification Locally

Let us get a local copy of the specification files and the handwritten Lean helpers. Start in the directory where you want to keep the build; we will put everything in scratch/sail-build/. We clone our fork of sail-riscv and check out the commit used by jolt-qed. Replace /absolute/path/to/jolt-qed with the absolute path to your checkout of jolt-qed, where we keep the patch. We apply that patch to make the handwritten helpers work with the newer compiler and Lean version.^[5]

# Where to find the patch.
# For Fish use this instead: set JOLT_QED /absolute/path/to/jolt-qed
JOLT_QED=/absolute/path/to/jolt-qed

# Keep the specification and compiler builds in the same scratch folder.
mkdir -p scratch/sail-build

# Download the RISC-V specification.
git clone https://github.com/abiswas3/sail-riscv.git scratch/sail-build/sail-riscv

# Go to the exact version of the specification that we use.
git -C scratch/sail-build/sail-riscv checkout 266473f8b2872ac25f5cfaf5a4293d6421a40b5d

# Apply our two-line change to RiscvExtras.lean.
git -C scratch/sail-build/sail-riscv apply "$JOLT_QED/sail-import/patches/sail-riscv-lean-handwritten.patch"

The Compiler

With these three characters, we have everything we need to describe the RISC-V ISA, but we still need a compiler to translate the specification into Lean code.

We now introduce the compiler, a program written in OCaml. It is general purpose in that it can generate code in several languages, including Lean. It can also generate C code from the specification. We will use the generated C code later to do differential testing, but that is a topic for another post.

Our first step is to compile the compiler from its source to a binary file that is executable. Then we will take that executable, feed it appropriate command line arguments and complete our translation. Below are detailed instructions on how to build the compiler from source^[6]. We tested this build with opam 2.6.1, OCaml 5.4.1, Dune 3.24.2 and Z3 4.16.0.

First install a C compiler, Git, GMP (a library for large numbers), Z3 (a solver the compiler uses to check the specification), pkgconf (which helps find installed libraries) and opam (OCaml’s package manager). On Arch Linux:

sudo pacman -S --needed base-devel git gmp z3 pkgconf opam

On macOS:

# Install a C compiler and Git.
xcode-select --install
brew install gmp z3 pkgconf opam

Run the remaining commands in the same terminal. The examples use Bash; comments beside commands whose syntax differs show what to use in Fish instead. Run this from the same directory where you created scratch/sail-build/ above. Replace /absolute/path/to/jolt-qed with the absolute path to your checkout of jolt-qed, which contains the patch.

# Where to find the patch. Replace this with your checkout's absolute path.
# For Fish use this instead: set JOLT_QED /absolute/path/to/jolt-qed
JOLT_QED=/absolute/path/to/jolt-qed

# Keep the sources, OCaml environment, cache and installed compiler together.
mkdir -p scratch/sail-build
cd scratch/sail-build
# For Fish use this instead: set -gx SAIL_BUILD_DIR "$PWD"
export SAIL_BUILD_DIR="$PWD"
# For Fish use this instead: set -gx OPAMROOT "$SAIL_BUILD_DIR/opam"
export OPAMROOT="$SAIL_BUILD_DIR/opam"
# For Fish use this instead: set -gx XDG_CACHE_HOME "$SAIL_BUILD_DIR/cache"
export XDG_CACHE_HOME="$SAIL_BUILD_DIR/cache"

# Initialise this separate opam root without changing shell startup files
# or creating a default OCaml environment.
opam init --bare --no-setup

# Create a separate environment called "sail", with its own OCaml 5.4.1 compiler
# and its own libraries (like a Python virtual environment).
opam switch create sail 5.4.1

# Make this terminal use that OCaml installation.
# For Fish use this instead: opam env --switch sail --shell=fish | source
eval "$(opam env --switch sail --shell=bash)"

# Check the OCaml compiler version (5.4.1).
ocamlc -version

# Download the source code of the compiler.
git clone https://github.com/rems-project/sail.git
cd sail

# Go to the exact version of the compiler that we use.
git checkout 2ae2199f8890180a8f9653f6ea08e54cd9790220

# Apply the fix from the unmerged pull request rems-project/sail#1774.
# We keep this fix as a patch file in our repository, jolt-qed.
git apply "$JOLT_QED/sail-import/patches/1774-type-arithmetic.patch"

# Install the OCaml libraries that the compiler depends on.
opam install --deps-only .

# Compile the compiler.
dune build --release

# Install the compiler beside the source checkout.
dune install --release --prefix "$SAIL_BUILD_DIR/sail-install"

# Check that it works. This prints the compiler's version, 0.20.3.
"$SAIL_BUILD_DIR/sail-install/bin/sail" --version

OPAMROOT tells opam where this environment lives. The activation command (eval in Bash, or source in Fish) puts the sail switch’s tools on this terminal’s PATH, so the subsequent dune commands use the dependencies installed in that switch. The source checkout is in scratch/sail-build/sail/, and the installed compiler is in scratch/sail-build/sail-install/bin/sail.

To return to the build in a new terminal, replace the path below with the absolute path to the directory created above:

cd /absolute/path/to/scratch/sail-build
# For Fish use this instead: set -gx SAIL_BUILD_DIR "$PWD"
export SAIL_BUILD_DIR="$PWD"
# For Fish use this instead: set -gx OPAMROOT "$SAIL_BUILD_DIR/opam"
export OPAMROOT="$SAIL_BUILD_DIR/opam"
# For Fish use this instead: set -gx XDG_CACHE_HOME "$SAIL_BUILD_DIR/cache"
export XDG_CACHE_HOME="$SAIL_BUILD_DIR/cache"
# For Fish use this instead: opam env --switch sail --shell=fish | source
eval "$(opam env --switch sail --shell=bash)"
cd sail

"$SAIL_BUILD_DIR/sail-install/bin/sail" --version

Generating Lean Code

Continue in the same terminal, using JOLT_QED and SAIL_BUILD_DIR from the build instructions above. Before running the compiler, set the variables below and move into the specification’s model/ directory. Reading the module list requires Python 3.11 or later.

# The compiler's installed libraries.
# For Fish use this instead: set -gx SAIL_DIR "$SAIL_BUILD_DIR/sail-install/share/sail"
export SAIL_DIR="$SAIL_BUILD_DIR/sail-install/share/sail"

# For Fish use this instead: set CONFIG "$JOLT_QED/sail-import/rv64d_jolt.json"
CONFIG="$JOLT_QED/sail-import/rv64d_jolt.json"

# For Fish use this instead: set MODULES (python3 -c 'import sys, tomllib; print(*tomllib.load(open(sys.argv[1], "rb"))["modules"]["selected"], sep="\n")' "$JOLT_QED/sail-import/PROVENANCE.toml")
MODULES=($(python3 -c 'import sys, tomllib; print(*tomllib.load(open(sys.argv[1], "rb"))["modules"]["selected"], sep="\n")' "$JOLT_QED/sail-import/PROVENANCE.toml"))

cd "$SAIL_BUILD_DIR/sail-riscv/model"
mkdir -p ../build

 1# Run the compiler. The flags are the ones upstream sail-riscv uses to generate its own Lean code.
 2# The result goes into the folder ../build/Lean_RV64D.
 3# For Fish use this instead on the last line: riscv.sail_project $MODULES
 4"$SAIL_BUILD_DIR/sail-install/bin/sail" \
 5  --strict-var --strict-bitvector --strict-exponentials \
 6  --require-version 0.20.1 \
 7  --memo-z3-path ../build/sail_smt_cache \
 8  --config "$CONFIG" \
 9  --lean \
10  --memo-z3 \
11  --lean-output-dir ../build \
12  --lean-force-output \
13  --lean-non-beq-type instruction \
14  --lean-non-beq-type ExecutionResult \
15  --lean-non-beq-type Step \
16  --lean-noncomputable \
17  --lean-noncomputable-function encdec_forwards \
18  --lean-noncomputable-function encdec_backwards \
19  --lean-noncomputable-function encdec_forwards_matches \
20  --lean-noncomputable-function encdec_backwards_matches \
21  --lean-noncomputable-function encdec_compressed_forwards \
22  --lean-noncomputable-function encdec_compressed_backwards \
23  --lean-noncomputable-function encdec_compressed_forwards_matches \
24  --lean-noncomputable-function encdec_compressed_backwards_matches \
25  --lean-import-file ../handwritten_support/RiscvExtras.lean \
26  -o Lean_RV64D \
27  riscv.sail_project "${MODULES[@]}"

Now there is a lot going on here. All we had done so far was get the specification locally along with a few more files, and we built the compiler from source. The executable was tagged with version 0.20.3. We did not really go over how to use this compiler.

• Line 9 tells the compiler to generate Lean code.

• Line 7 sets the path to the SMT solver’s cache, we do not need to worry about this. It is the implementation detail of the compiler and how it uses z3. We do not care how the compiler works for now, just how to use it.

• Line 4 is the path of the compiler executable.

• Line 11 chooses ../build as the directory in which to create the generated Lean project. Line 26 supplies its name, Lean_RV64D, so the project goes in ../build/Lean_RV64D/.

• Line 25 supplies the handwritten Lean helper we introduced earlier, handwritten_support/RiscvExtras.lean. The compiler copies it into the generated Lean project and imports it. While copying it, the compiler replaces THE_MODULE_NAME with LeanRV64D.

• Line 26 names the generated Lean project Lean_RV64D. This is the name used with the output directory on line 11.

• Line 27 supplies the specification’s project file and the list of modules we want to translate.

  • riscv.sail_project is the project file we saw earlier: it lists the modules and the .sail files they contain. Sail manual: modules. This file is in sail-riscv/model/, where we run the command.

  • MODULES holds our chosen subset of the module names listed in riscv.sail_project. Bash replaces "${MODULES[@]}" with those names, passing each one to the compiler as a separate argument.

    The module list comes from $JOLT_QED/sail-import/PROVENANCE.toml.

• Line 5 enables three compiler checks on the specification.

  • --strict-var makes the compiler report an error and stop translation if a mutable variable in the specification is introduced without var. Sail manual: mutable variables. In this function in the specification, count is mutable: the loop changes it with count = new_count. It is already declared with var, so it passes this check.

    val count_ones : forall 'n, 'n >= 0. (bits('n)) -> range(0, 'n)
    function count_ones(x) = {
      var count : range(0, 'n) = 0;
      foreach (i from 0 to ('n - 1)) {
        if x[i] == 0b1 then {
          let new_count = count + 1;
          assert(new_count <= 'n);
          count = new_count;
        }
      };
      count
    }

    In the generated Lean code, the changing count is stored in loop_vars, marked as mutable with let mut:

    /-- Type quantifiers: k_n : Nat, k_n ≥ 0, k_n ≥ 0 -/
    def count_ones (x : (BitVec k_n)) : SailM Nat := do
      let count : Nat := 0
      let loop_i_lower := 0
      let loop_i_upper := ((Sail.BitVec.length x) -i 1)
      let mut loop_vars := count
      for i in [loop_i_lower:loop_i_upper:1]i do
        let count := loop_vars
        loop_vars ← do
          if (((BitVec.access x i) == 1#1) : Bool)
          then
            (do
              let new_count := (count +i 1)
              sail_assert (new_count ≤b (Sail.BitVec.length x)) "core/arithmetic.sail:85.28-85.29"
              (pure new_count))
          else (pure count)
      (pure loop_vars)

  • --strict-bitvector requires bitvector lengths in the specification to be nonnegative.

  • --strict-exponentials requires exponents in type-level expressions in the specification, such as 2 ^ n, to be nonnegative.

• Line 6 requires compiler version 0.20.1 or later. Our compiler is version 0.20.3, so it passes this check. Sail manual: version check.

• Line 8 gives the compiler a JSON configuration file. We change three settings in the default RV64D configuration from true to false, because Jolt does not support these features:

  • memory.misaligned.supported: misaligned memory accesses, such as a four-byte load from an address that is not a multiple of four.
  • extensions.Zicfilp.supported: landing pads, which check where indirect calls and jumps land.
  • extensions.Zicfiss.supported: shadow stacks, which check function return addresses.

  The modified file is $JOLT_QED/sail-import/rv64d_jolt.json, whose path we store in CONFIG above.

• Line 10 tells the compiler to save and reuse answers from Z3, so repeated checks can be faster. Line 7 specifies where to keep that cache. Sail manual: solver caching.

• Line 12 allows the compiler to generate into that project directory again if it already exists, removing the old generated Lean files first.

• Lines 13–15 tell the compiler to omit deriving BEq for three types in the generated Lean code. BEq supplies Boolean equality, used by ==. The three types are instruction, ExecutionResult, and Step.

  For example, the generated Step type derives Inhabited and Repr, with no BEq:

  inductive Step where
    | Step_Pending_Interrupt (_ : (InterruptType × Privilege))
    | Step_Ext_Fetch_Failure (_ : ext_fetch_addr_error)
    | Step_Fetch_Failure (_ : (virtaddr × ExceptionType))
    | Step_Execute (_ : (ExecutionResult × instbits))
    | Step_Waiting (_ : WaitReason)
    deriving Inhabited, Repr

• Line 16 adds noncomputable section to the generated Lean code. This allows definitions to depend on helpers declared as axioms, such as load_reservation, without requiring executable implementations of those helpers.

• Lines 17–24 mark the eight named functions as noncomputable in the generated Lean code. The generated Lean code still contains their definitions, as seen in encdec_forwards, one of the functions listed above.

At the end of all this, you should have a folder called Lean_RV64D at $SAIL_BUILD_DIR/sail-riscv/build/Lean_RV64D/. It contains the generated Lean code in the LeanRV64D/ folder and the LeanRV64D.lean file. We then copy both into jolt-qed:

cp -R "$SAIL_BUILD_DIR/sail-riscv/build/Lean_RV64D/LeanRV64D" "$JOLT_QED/"
cp "$SAIL_BUILD_DIR/sail-riscv/build/Lean_RV64D/LeanRV64D.lean" "$JOLT_QED/"

The Runtime Library

Go back to Snippet 1. To execute ADDI, the specification reads the register rs1 with X(rs1). X is a shorthand, and reading with it calls rX_bits, which turns the register index into a number and calls rX (model/core/regs.sail, lines 229–235). Here is rX in the specification.

function rX (Regno(r) : regno) -> xlenbits = {
  let v : regtype =
    match r {
      0 => zero_reg,
      1 => x1,
      2 => x2,
      // ... and so on for registers 3 to 30
      31 => x31,
    };
  regval_from_reg(v)
}

Register 0 in RISC-V always holds zero, so rX returns the constant zero_reg for it. Every other number picks one of the registers x1 to x31, which are declared a few lines above with register x1 : regtype and so on. In Sail, writing the name of a register reads it. There is no function call.

Here is the Lean code the compiler generated for rX.

def rX (app_0 : regno) : SailM (BitVec 64) := do
  let .Regno r := app_0
  let v ← (( do
    match r with
    | 0 => (pure zero_reg)
    | 1 => readReg x1
    | 2 => readReg x2
    -- ... and so on for registers 3 to 30
    | _ => readReg x31 ) : SailM regtype )
  (pure (regval_from_reg v))

The Lean rX is generated, like everything else in LeanRV64D/. Each register read in the Sail code has become a call to readReg. But none of the 135 files in LeanRV64D/ defines readReg. Reading a register is built into the Sail language, so the specification does not define it either, and the compiler has no Sail code to translate.

The body of readReg comes from lean-sail, a small Lean library written by the same people who wrote the compiler. Every generated Lean file starts with import Sail, and that import is lean-sail. Here is readReg in Sail/ConcurrencyInterfaceV1.lean.

@[simp_sail]
def readReg (r : Register) : PreSailM RegisterType c ue (RegisterType r) := do
  let .some s := (← get).regs.get? r
    | throw .Unreachable
  pure s

readReg looks up the register r in the machine’s state and returns its value. lean-sail also defines that state, which we discussed in detail in How to Model a CPU in Lean.

So readReg is in the same position as load_reservation from The Helpers. The generated code calls both, and neither has a body in the specification. load_reservation is specific to RISC-V, so the sail-riscv authors wrote a stand-in for it in RiscvExtras.lean. readReg is needed by every Sail specification, whatever the ISA, so the compiler’s authors wrote it once, in lean-sail. Without import Sail, readReg would be an unknown name, and the generated code would not build. The same is true of writeReg, which wX uses to write a register.

The compiler and lean-sail are released together, and the compiler at commit 2ae2199 expects lean-sail tag v8. We copied only LeanRV64D/ into jolt-qed, so jolt-qed’s own lakefile.toml asks for lean-sail at v8. lake-manifest.json pins that tag to commit 1e5b216.

Summary

Putting everything together we get the following picture

1. Thanks Quang! ↩

2. I wish in a rush, and got Claude to get the thing to pass and then forgot about it. We left behind instructions on how to reproduce the work, but admittedly, I myself was not sure of what I was doing. ↩

3. We have not introduced this guy yet. ↩

4. For example, the interpreter uses Platform.load_reservation, while the C target uses load_reservation. ↩

5. The patch adds open THE_MODULE_NAME so the helper can refer to types inside the generated model’s namespace; the compiler replaces this placeholder with LeanRV64D when copying the file. It also changes extension.toCtorIdx to extension.ctorIdx, the name available in Lean 4.35, in the helper’s SizeOf extension instance. ↩

6. We apply the fix from rems-project/sail#1774 for missing parentheses in the Lean translation of type-level arithmetic. Without it, the compiler translates (if true then 8 else 4) * 8 as if true then 8 else 4 * 8, which Lean reads as if true then 8 else (4 * 8). This makes flen, the floating-point register width, 8 bits instead of 64. The PR is still open as of 9 November 2026, so we apply the saved patch in sail-import/patches/1774-type-arithmetic.patch before building the compiler. ↩