riscv-lean

Hand-polished, bitblastable semantics for RISC-V (RV64) in Lean 4, proven equivalent to the auto-generated authoritative semantics of the Sail RISC-V model.

Supported Extensions

Extension	Description	Status
RV64I	Base Integer Instruction Set	✅
M	Integer Multiplication and Division	✅
B - Zba	Address generation	✅
B - Zbb	Basic bit-manipulation	✅
B - Zbs	Single-bit instructions	✅
B - Zbkb	Bit-manipulation for Cryptography	✅
B - Zbc	Carry-less multiplication	🚧
B - Zbkc	Carry-less multiplication for Cryptography	🚧
B - Zbkx	Crossbar permutations for Cryptography	🚧

Project Structure

Core files are in the RISCV/ directory:

File	Description
ForLean.lean	Theorems to be upstreamed to Lean
Instructions.lean	Bitblastable RISC-V semantics
SailPure.lean	Purified (i.e., monad-free) Sail specifications
SailPureToInstructions.lean	Equivalence proofs between monad-free Sail specification and bitblastable RISC-V semantics
SailToRV64.lean	Equivalence proofs between monadic and monad-free Sail Specifications
Skeleton.lean	Monadic wrappers and proving infrastructure

Building

# Clone the repository
git clone https://github.com/opencompl/riscv-lean.git
cd riscv-lean

# Build the project
lake build

Usage

Add riscv-lean as a dependency in your lakefile.toml:

[[require]]
name = "SailRV64"
git = "https://github.com/opencompl/riscv-lean"
rev = "main"

Then import the library in your Lean files:

import RISCV

Development & Support

This project is developed and maintained by Tobias Grosser, Luisa Cicolini, Sarah Kuhn, and Osman Yasar at the University of Cambridge.

Related Projects

• sail-riscv — Official Sail RISC-V specification
• sail-riscv-lean — Semantics of Sail RISC-V specification in Lean 4