RiscvDialect

This repository contains early experimental code from my BSc thesis, where I implemented code generation for the RISC-V processor using the Lean 4 theorem prover and functional programming language.

The final, production-quality code and proofs from the thesis have since been fully upstreamed into:

• the Lean-MLIR project
• and a standalone repository containing the RISC-V ISA semantic mechanization in Lean 4

This repository remains as a historical snapshot of the initial prototyping work.

---

Upstream Projects

Lean-MLIR

The main integration of the final code generation and proof infrastructure:
https://github.com/opencompl/lean-mlir

RISC-V Semantic Mechanization in Lean 4

A clean, standalone mechanization of the RISC-V ISA semantics: https://github.com/opencompl/riscv-lean

Sail to Lean (RISC-V Sail Translation)

The Lean port of the official RISC-V Sail specification: https://github.com/opencompl/sail-riscv-lean