This translation of the official SAIL RISC-V SPEC into the Lean Theorem Prover covers the full RISC-V SPEC and passes the Lean type-checkers without errors.

⚠️ However, our Lean backend for sail is still work-in-progress. This means, this resulting Lean code is neither executable nor polished in any way. ⚠️

This repository generates automatically the RISC-V Lean model from the official Sail model. To generate it locally, follow the following steps.

The released version of Sail does not support Lean output, so we need to build Sail from its git repository. All the details are given in the official instructions. What follows here is a summary:

On Debian/Ubuntu

sudo apt-get install build-essential libgmp-dev z3 pkg-config

or on MacOS

brew install gmp z3 pkgconf

git clone https://github.com/rems-project/sail.git

Using opam:

opam pin add sail

With dune, inside the Sail root directory:

opam install . --deps-only
dune build --release
dune install

To build the RISC-V model, first clone the repository

git clone https://github.com/riscv/sail-riscv.git

and then build it using the cmake:

cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo
cmake --build build/ --target generated_lean_rv64d

The resulting Lean model will be in build/model/Lean_RV64D and can be built using lake build

This project is developed by Tobias Grosser and Leo Stefanesco at the University of Cambridge, James Parker, Lee Newcomb, Ben Selfridge, and Ben Hamlin at Galois Inc., and Jakob von Raumer and Ryan Lahfa at LindyLabs. Peter Sewell, Alasdair Armstrong (both Cambridge) and Brian Campbell (University of Edinburgh) supported through consulting and code.

Luisa Cicolini, Leo Stefanesco, Siddharth Bhat, Sarah Kuhn and Tobias Grosser (all Cambridge) also polish Lean's BitVector library (maintained by the Lean FRO), develop further proof automation, and work on manually improving the bitvector level statements of these SAIL semantics in support of this project.

We also thank Arthur Adjedj for support and code.

This work was funded by a grant provided by the Ethereum Foundation and its Verified zkEVM Project led by Alexander Hicks.

Lines: 133,819
Definitions: 4,001
Inductive definitions: 165
Abbreviations: 144

Errors found: 0
Warnings found: 0