CI: test Lean emulator on some ELF files

Author: Ptival

.github/workflows/compile-lean.yml

@@ -51,3 +51,9 @@ jobs:
         uses: leanprover/lean-action@v1
         with:
           lake-package-directory: "build/model/Lean_RV64D/"
+
+      - name: Test the Lean emulator
+        run: |
+          eval $(opam config env)
+          cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -DSAIL_MODULES="H;Zca;Zicbom_insts;Zicboz;Zicsr_insts;Zkr;Sscofpmf;postlude" -DPRINT_EFFECTS=true
+          cmake --build build --target test_lean_emulator

CMakeLists.txt

@@ -168,6 +168,9 @@ add_subdirectory("model")
 # Emulator binary.
 add_subdirectory("c_emulator")
 
+# Lean emulator
+add_subdirectory("lean_emulator")
+
 # Old pre-compiled riscv-tests & first-party tests.
 add_subdirectory("test")
 

handwritten_support/RiscvExtrasExecutable.lean

@@ -33,7 +33,7 @@ def plat_term_read : Unit → SailM String := λ _ => panic "TODO: plat_term_rea
 -- Reservations
 def load_reservation : Arch.pa → Nat → SailM Unit := λ _ => panic "TODO: load_reservation"
 def match_reservation : Arch.pa → Bool := λ _ => panic "TODO: match_reservation"
-def cancel_reservation : Unit → SailM Unit := λ _ => panic "TODO: cancel_reservation"
+def cancel_reservation : Unit → SailM Unit := λ _ => dbg_trace "TODO: cancel_reservation"; return ()
 def valid_reservation : Unit → Bool := λ _ => false
 
 def get_16_random_bits : Unit → SailM (BitVec 16) := λ _ => panic "TODO: get_16_random_bits"
@@ -112,6 +112,6 @@ def riscv_f64roundToInt : BitVec 3 → BitVec 64 → Bool → (BitVec 5 × BitVe
 
 -- Termination of extensionEnabled
 instance : SizeOf extension where
-  sizeOf := extension.toCtorIdx
+  sizeOf := extension.ctorIdx
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| decide)

lean_emulator/CMakeLists.txt

@@ -0,0 +1,16 @@
+add_custom_target(test_lean_emulator
+    COMMAND cmake -P "${CMAKE_CURRENT_SOURCE_DIR}/test_lean_emulator.cmake"
+)
+
+# We need to copy the whole `lean_emulator` directory structure in the build
+# add_custom_target(copy_lean_emulator
+#     COMMAND cmake -E copy_directory
+#         ${CMAKE_CURRENT_SOURCE_DIR}
+#         ${CMAKE_CURRENT_BINARY_DIR}
+#     COMMENT "Copying Lean emulator directory to build directory"
+# )
+
+add_dependencies(
+    test_lean_emulator
+    # copy_lean_emulator
+    generated_lean_executable_rv64d)

lean_emulator/LeanRiscv.lean

@@ -246,7 +246,7 @@ def initializeRegisters (elf: ELF64File): SailM PUnit :=
     writeReg htif_payload_writes (← (undefined_bitvector 4))
     writeReg satp (← (undefined_bitvector ((2 ^i 2) *i 8)))
 
-def my_main (elf: ELF64File) :=
+def my_main (elf: ELF64File) : SailM Int :=
   open LeanRV64DExecutable.Functions in
   open Sail in
   do
@@ -260,20 +260,32 @@ def my_main (elf: ELF64File) :=
       print_bits_effect "htif_tohost = " (← readReg htif_tohost)
       loop ()
     )
-    (λ the_exception ↦
+    (λ the_exception ↦ do
       match the_exception with
       | .Error_not_implemented s => (pure (print_string "Error: Not implemented: " s))
       | .Error_internal_error () => (pure (print "Error: internal error"))
       | .Error_reserved_behavior s => (pure (print_string "Error: Reserved behavior: " s))
+      return 1
     )
 
 def runElf64 (elf : ELF64File) : IO UInt32 :=
   open Sail in
   open LeanRV64DExecutable.Functions in
-  let mem := initializeMemory MachineBits.B64 elf
-  let regs := Std.ExtDHashMap.emptyWithCapacity
-  let initialState := ⟨regs, (), mem, default, default, default⟩
-  main_of_sail_main initialState $ fun () => do
-    sail_model_init ()
-    initializeRegisters elf
-    my_main elf
+  do
+    let mem := initializeMemory MachineBits.B64 elf
+    let regs := Std.ExtDHashMap.emptyWithCapacity
+    let initialState := ⟨regs, (), mem, default, default, default⟩
+    let main := do
+      sail_model_init ()
+      initializeRegisters elf
+      my_main elf
+    match main.run initialState with
+    | .ok res s => do
+      for m in s.sailOutput do
+        IO.print m
+      IO.Process.exit $ UInt8.ofInt res
+    | .error e s => do
+      for m in s.sailOutput do
+        IO.print m
+      IO.eprintln s!"Error while running the sail program!: {e.print}"
+      IO.Process.exit 1

lean_emulator/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-22
+leanprover/lean4:nightly-2026-01-22

lean_emulator/test_lean_emulator.cmake

@@ -0,0 +1,80 @@
+include(${CMAKE_CURRENT_LIST_DIR}/../test/download_riscv_tests.cmake)
+
+set(TARBALL_NAME "riscv-tests")
+set(DOWNLOAD_PATH "${CMAKE_CURRENT_BINARY_DIR}/${TEST_DOWNLOAD_VERSION}")
+set(DOWNLOAD_URL "${TEST_DOWNLOAD_URL}/${TEST_DOWNLOAD_VERSION}/${TARBALL_NAME}.tar.gz")
+
+download_riscv_tests(
+    "${DOWNLOAD_PATH}"
+    "${TARBALL_NAME}"
+    "${DOWNLOAD_URL}"
+)
+
+# Note: this is a bit slow, so only testing a handful of arbitrarily picked ELF
+# files.
+set(LEAN_EMULATOR_TEST_ELFS
+    rv64ui-p-add
+    rv64ui-p-addi
+    rv64ui-p-addiw
+    rv64ui-p-addw
+    rv64ui-p-and
+    rv64ui-p-andi
+    rv64ui-p-auipc
+    rv64ui-p-beq
+    rv64ui-p-bge
+    rv64ui-p-bgeu
+    rv64ui-p-blt
+    rv64ui-p-bltu
+    rv64ui-p-bne
+    # rv64ui-p-fence_i # does not work at the moment
+    rv64ui-p-jal
+    rv64ui-p-jalr
+    rv64ui-p-lb
+    rv64ui-p-lbu
+    rv64ui-p-ld
+    rv64ui-p-lh
+    rv64ui-p-lhu
+    rv64ui-p-lui
+    rv64ui-p-lw
+    rv64ui-p-lwu
+    rv64ui-p-or
+    rv64ui-p-ori
+    rv64ui-p-sb
+    rv64ui-p-sd
+    rv64ui-p-sh
+    rv64ui-p-simple
+    rv64ui-p-sll
+    rv64ui-p-slli
+    rv64ui-p-slliw
+    rv64ui-p-sllw
+    rv64ui-p-slt
+    rv64ui-p-slti
+    rv64ui-p-sltiu
+    rv64ui-p-sltu
+    rv64ui-p-sra
+    rv64ui-p-srai
+    rv64ui-p-sraiw
+    rv64ui-p-sraw
+    rv64ui-p-srl
+    rv64ui-p-srli
+    rv64ui-p-srliw
+    rv64ui-p-srlw
+    rv64ui-p-sub
+    rv64ui-p-subw
+    rv64ui-p-sw
+    rv64ui-p-xor
+    rv64ui-p-xori
+)
+
+execute_process(
+    COMMAND lake build lean_riscv_emulator
+    WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
+)
+foreach(file IN LISTS LEAN_EMULATOR_TEST_ELFS)
+    message(STATUS "Testing Lean emulator on file ${file}")
+    execute_process(
+        COMMAND lake exec lean_riscv_emulator -- "${DOWNLOAD_PATH}/riscv-tests/${file}"
+        WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
+        COMMAND_ERROR_IS_FATAL ANY
+    )
+endforeach()

model/CMakeLists.txt

@@ -24,6 +24,12 @@ set(sail_common
     --memo-z3-path "${CMAKE_CURRENT_BINARY_DIR}/sail_smt_cache"
 )
 
+# Mirroring Sail's PRINT_EFFECTS flag
+option(PRINT_EFFECTS "Pass PRINT_EFFECTS to Sail (used in Lean and Rocq backends)" OFF)
+if(PRINT_EFFECTS)
+    list(APPEND sail_common -D PRINT_EFFECTS)
+endif()
+
 set(project_file "riscv.sail_project")
 
 # Reconfigure if the project file changes.

model/main/main.sail

@@ -14,7 +14,8 @@ function main() : unit -> unit = {
     init_model("");
     print_bits("PC = ", PC);
     sail_end_cycle();
-    loop()
+    let _ = loop();
+    return ()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
     Error_internal_error() => print("Error: internal error")

model/postlude/step.sail

@@ -268,7 +268,7 @@ function try_step(step_no : nat, exit_wait : bool) -> bool = {
   }
 }
 
-function loop () : unit -> unit = {
+function loop () : unit -> int = {
   var i : nat = 0;
   var step_no : nat = 0;
   while not(htif_done) do {
@@ -283,20 +283,21 @@ function loop () : unit -> unit = {
       sail_end_cycle()
     };
 
-    // check htif exit
-    if htif_done then {
-      let exit_val = unsigned(htif_exit_code);
-      if exit_val == 0 then print("SUCCESS")
-      else print_int("FAILURE: ", exit_val);
-    } else {
+    if not(htif_done) then {
       // update time
       i = i + 1;
       if i == plat_insns_per_tick then {
         tick_clock();
         i = 0;
       }
     }
-  }
+  };
+
+  let exit_val = unsigned(htif_exit_code);
+  if exit_val == 0
+    then print_endline("SUCCESS")
+    else print_int("FAILURE: ", exit_val);
+  return exit_val
 }
 
 // Termination measures for loops are not supported by the Lean backend, so they