Search papers, labs, and topics across Lattice.
This paper presents a formal semantics of the RISC-V ISA in Rocq, built on Interaction Trees (ITrees), to enable cross-level verification between compilers and hardware. It leverages ITree bisimulation and refinement to verify the ISA contract from compiler IR to hardware implementations. The formalization is validated by extracting an executable simulator that passes standard RISC-V test suites, and demonstrated through case studies including LLVM IR to RISC-V code equivalence, instruction reordering validation, and hardware ALU correctness.
Proving semantic equivalence between LLVM IR and RISC-V code is now possible within a single framework, thanks to a new formal RISC-V semantics built on Interaction Trees.
The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compilers and hardware implementations. As an open, modular ISA gaining adoption across embedded, mobile, and cloud platforms, RISC-V makes a formally verified ISA specification particularly valuable. However, existing formal RISC-V specifications focus on hardware tooling rather than cross-level verification: they provide no machine-checked instruction-level properties and lack support for verifying this contract across levels. We address these limitations with a formal semantics of the RISC-V ISA in Rocq, built on Interaction Trees (ITrees). By leveraging ITree bisimulation and refinement, our semantics enables cross-level verification from compiler IR to hardware within a single framework. Our formalization covers a wide spectrum of RISC-V extensions. The correctness of individual instruction semantics is backed by machine-checked lemmas in Rocq. We further validate it by extracting an executable simulator that passes all standard RISC-V test suites. Three case studies demonstrate the effectiveness of our semantics for cross-level verification: first, we prove semantic equivalence via bisimulation between LLVM IR and RISC-V code on an array access pattern via Vellvm (LLVM ITree semantics); second, we apply translation validation to a specific instruction reordering for macro-operation fusion, distinguishing safe reorderings from those that break program-counter-relative addressing; third, we prove that a K么ika hardware ALU correctly implements all R-type integer operations (e.g., ADD, SUB, AND) against our ISA contract.
