These notes re-cap the steps required to transplile the RISC-V sail specification to Lean. NOTE: As confirmed from the original documentation, only the non-computable Lean code builds and compiles cleanly. Some work is still needed to get the executable CPU to work. I do not imagine a whole lot, but as of the date of writing this, the executable build is not clean.

Tested on:

  • macOS (Apple Silicon)
  • Intel CPU Arch Linux (TODO:)

Step 0: Clone Both Repos

Here I've forked the two repositories with the hope of eventually fixing the executable issue. But there's nothing special about my fork right now. Cloning the original repos will also work.

git clone git@github.com:abiswas3/sail-riscv.git
git clone git@github.com:abiswas3/sail.git
parent/
├── sail/                  # Sail compiler (transpiler) -- clone from github.com/rems-project/sail
└── sail-riscv/            # This repo -- RISC-V ISA model written in Sail

Step 1: Install System Dependencies

Note To Reader

I do not particularly understand the Sail DSL, nor am I an expert ocaml programmer. These steps mostly follow the README.md's in the repo, a bit of googling and some Claude code help. Hopefully with time, I will be able to write a better version of what the hell is going on.

macOS (Homebrew)

xcode-select --install    # if not already done
brew install opam gmp z3 pkgconf cmake

Arch Linux

sudo pacman -S opam        # OCaml package manager -- needed to fetch and install Sail's OCaml dependencies
sudo pacman -S gmp         # GNU Multiple Precision arithmetic library -- Sail uses it internally for big integer arithmetic
sudo pacman -S z3          # SMT solver from Microsoft Research -- Sail calls Z3 during type-checking to prove
                           #   arithmetic constraints on dependent types (e.g. that bitvector widths are correct)
sudo pacman -S cmake       # build system generator -- sail-riscv uses CMake to orchestrate the Sail-to-Lean code generation
sudo pacman -S base-devel  # C compiler, make, binutils, etc. -- OCaml's runtime is written in C and some opam
                           #   packages have C bindings (e.g. GMP). Also provides C++ compiler which sail-riscv's
                           #   CMake build needs for the emulator harness, even if you only want Lean output.
sudo pacman -S pkgconf     # pkg-config implementation -- CMake uses it to locate system libraries like GMP

Both Platforms: Initialize opam (one-time)

Run the following code from anywhere -- opam stores its state in ~/.opam/.

TODO: ocaml crash course

opam init                 # follow prompts, say yes to shell setup
eval $(opam env)          # or restart your shell

opam init creates the ~/.opam/ directory, downloads the OCaml package registry, and installs a default OCaml compiler. eval $(opam env) sets shell environment variables (PATH, OCAML_TOPLEVEL_PATH, etc.) so that your shell can find the OCaml tools and libraries that opam installed. You need to run eval $(opam env) in each new shell session, or let opam's shell hook do it automatically (it offers to set this up during opam init).

Step 2: Build and Install the Sail Compiler Locally

You should be in the parent/ directory (the one containing both sail/ and sail-riscv/).

The Sail compiler is a single binary called sail. On its own, it can only parse and type-check Sail code. To actually generate output for a specific language (Lean, C++, Coq, etc.), it needs a backend plugin loaded at startup.

What The Hell Is A Plugin

Note that I do not understand ocaml's plugin infrastructure properly. I had to ask Calude and this is what it gave me:

A plugin is a .cmxs file -- an OCaml shared library (see OCaml manual on native plugins). When sail starts, it scans a known directory for .cmxs files and loads them. Each plugin registers new command-line flags. For example, loading sail_plugin_lean.cmxs adds the --lean flag to the sail binary. There is no separate "lean binary" -- it's all one sail binary with plugins extending its capabilities.

dune is OCaml's build system (like make or cargo). It reads build instructions from dune files in the source tree. Below, we use three commands. Each is explained with what it does and what it produces:

cd sail

2a. Install OCaml dependencies

opam install . --deps-only

Reads the .opam files in the sail repo and installs all required OCaml libraries into the current opam switch. Does not build sail itself.

2b. Build the compiler and plugins

dune build --release

Compiles everything in the sail repo. Produces build artifacts under _build/, including:

  • _build/default/src/bin/sail.exe -- the core sail binary
  • _build/default/src/sail_lean_backend/sail_plugin_lean.cmxs -- the Lean plugin

At this point the binary exists but doesn't know where to find its plugins.

2c. Install into a local prefix

dune install --prefix _local_install

Copies the binary, plugins, and standard library files into a structured directory:

  • _local_install/bin/sail -- the sail binary
  • _local_install/share/libsail/plugins/sail_plugin_lean.cmxs -- the Lean plugin
  • _local_install/share/sail/lib/ -- Sail's standard library (prelude, etc.)

This is what "installing a plugin" means concretely: copying the .cmxs file into the share/libsail/plugins/ directory where the sail binary knows to look for it.

cd ..

Verify the Lean backend is loaded

SAIL_DIR=sail/_local_install/share/sail sail/_local_install/bin/sail --help | grep lean

SAIL_DIR tells the sail binary where to find its standard library and plugins. You should see --lean and related flags listed. If you don't, the plugin file is not in the expected share/libsail/plugins/ directory -- re-run dune install.

Step 3: Configure the sail-riscv Build

From the parent directory (or from sail-riscv/):

cd sail-riscv

SAIL_DIR=$(realpath ../sail/_local_install/share/sail) \
cmake -S . -B build \
  -DCMAKE_BUILD_TYPE=RelWithDebInfo \
  -DSAIL_BIN=$(realpath ../sail/_local_install/bin/sail)

Key variables:

  • SAIL_DIR -- points to the installed Sail share directory. This is where the compiler finds its standard library, include files, and plugins.
  • SAIL_BIN -- path to the locally-installed sail binary.

Important: Both paths must be absolute. CMake runs sail --dir internally to locate the Sail library directory, and the sail binary echoes back whatever SAIL_DIR was set to. If that's a relative path like ../sail/..., CMake resolves it relative to the build directory (build/), not the source directory, causing "Cannot find source file" errors for the C runtime files.

Step 4: Generate Lean Code

Two variants can be generated. Both take a few minutes (the Sail compiler type-checks the full model, calling Z3 to solve arithmetic constraints).

I also do not understand any of the Z3 stuff right now.

Noncomputable (for theorem proving)

SAIL_DIR=$(realpath ../sail/_local_install/share/sail) \
  cmake --build build --target generated_lean_rv64d

Output: build/model/Lean_RV64D/ (~155 .lean files)

This version uses noncomputable sections, suitable for interactive proof in Lean.

Executable (for running + theorem provin + theorem provingg)

SAIL_DIR=$(realpath ../sail/_local_install/share/sail) \
  cmake --build build --target generated_lean_executable_rv64d

Output: build/model/Lean_RV64D_executable/ (~155 .lean files)

This version generates computable code that can be built and executed with lake build.

RV32 Variants

Replace rv64d with rv32d in the target names for 32-bit:

  • generated_lean_rv32d
  • generated_lean_executable_rv32d

Step 5: Build the Generated Lean Code (Optional)

Each output directory contains a lakefile.toml and lean-toolchain. To compile:

cd build/model/Lean_RV64D/          # or Lean_RV64D_executable/
lake update
lake build

The generated Lean requires a specific Lean toolchain version (specified in lean-toolchain) and the lean-sail support library (fetched automatically by lake).

Rebuilding After Sail Compiler Changes

Since you're running from source, after modifying the Sail compiler:

# 1. Rebuild and reinstall the compiler
cd ../sail
dune build --release
dune install --prefix _local_install

# 2. Clean stale outputs and re-generate Lean (from sail-riscv)
cd ../sail-riscv
rm -rf build/model/Lean_RV64D build/model/Lean_RV64D_executable

SAIL_DIR=$(realpath ../sail/_local_install/share/sail) \
  cmake --build build --target generated_lean_rv64d

SAIL_DIR=$(realpath ../sail/_local_install/share/sail) \
  cmake --build build --target generated_lean_executable_rv64d

Troubleshooting

  • Cannot find source file: ../sail/_local_install/share/sail/lib/elf.c: You used relative paths for SAIL_DIR. CMake resolves paths relative to the build directory, not where you ran the command. Use $(realpath ../sail/_local_install/share/sail) to get an absolute path.

  • --lean flag not found: The plugin wasn't installed. Make sure you ran dune install --prefix _local_install and that SAIL_DIR points to the _local_install/share/sail directory (not the repo root or lib/).

  • sail: command not found during cmake: You need to pass -DSAIL_BIN= pointing to your local install, and set SAIL_DIR as an environment variable.

  • Plugin load error (symbol not found): Version mismatch between the sail binary and the plugin. Run dune build --release && dune install --prefix _local_install again to rebuild both from the same source.

  • CMake cache error about mismatched source directory: Delete build/ and reconfigure: rm -rf build && cmake -S . -B build ...

What Gets Generated

The Sail compiler translates the entire RISC-V ISA model into Lean definitions:

  • Instruction encodings/decodings
  • Instruction semantics
  • CSR definitions
  • Memory model
  • Exception handling
  • Extension support (M, A, F, D, C, V, etc.)

The noncomputable version is for reasoning about the spec in Lean's type theory. The executable version can simulate RISC-V binaries.