RISC-V ISA Semantics for Lean

These semantics are generated from the official RISC-V SPEC available at https://github.com/riscv/sail-riscv/.

⚠️ While this repository covers the full RISC-V SPEC, our Lean backend for sail is still work-in-progress. As a result, our semantics are still full of warnings and errors. Similarly, our output is not yet polished for readability.

Statistics

Lines: 125708
Definitions: 3667
Inductive definitions: 159
Abbreviations: 136

Warnings and Errors

Errors found: 1
Warnings found: 1

Error Classes

• 1x Lean exited with code 137