A formal specification of the RISC-V RV32EM instruction set in Lean 4.
Work in Progress - Skeleton only, implementation needed.
Formalize a subset of RISC-V RV32EM with:
- Instruction encoding/decoding
- Operational semantics (step function)
- Basic correctness proofs
| Format | Instructions |
|---|---|
| R-type | ADD, SUB, AND, OR, XOR, SLT |
| I-type | ADDI, ANDI, ORI, XORI, SLTI |
| I-type (load) | LW |
| S-type | SW |
| B-type | BEQ, BNE, BLT |
| U-type | LUI, AUIPC |
| J-type | JAL |
| I-type (jump) | JALR |
| M-ext | MUL, DIV |
rv32em-lean/
├── lakefile.lean # Build configuration
├── lean-toolchain # Lean version
├── RV32EM.lean # Module root
└── RV32EM/
├── Basic.lean # Types: Word32, Reg, Imm
├── Instr.lean # Instruction datatype
├── Encode.lean # Instr → BitVec 32
├── Decode.lean # BitVec 32 → Option Instr
├── Mach.lean # Machine state
├── Step.lean # Execution semantics
└── Proofs.lean # Correctness theorems
lake build- RISC-V Spec (Unprivileged)
- RISC-V Instruction Reference
- risc0-lean4 - Reference implementation
| Section | Topic | Relevant Files |
|---|---|---|
| 2.1 | Programmers' Model | Mach.lean |
| 2.2 | Base Instruction Formats | Encode.lean, Decode.lean |
| 2.3 | Immediate Encoding | Encode.lean, Decode.lean |
| 2.4 | Integer Computational | Instr.lean, Step.lean |
| 2.5 | Control Transfer | Instr.lean, Step.lean |
| 2.6 | Load and Store | Instr.lean, Step.lean |
| 7.1 | M Extension | Instr.lean, Step.lean |
- Project setup
- Basic types (Word32, Reg, Imm)
- Machine state structure
- Instruction datatype (15-20 instructions)
- Encode function
- Decode function
- Step function
- Roundtrip proof (decode ∘ encode = id)
- x0 preservation proof