Draft PR for lean riscv emulator

src/sail_lean_backend/Sail/Sail.lean

@@ -220,6 +220,7 @@ def trivialChoiceSource : ChoiceSource where
 class Arch where
   va_size : Nat
   pa : Type
+  pa_OfNat {n : Nat} : OfNat pa n
   arch_ak : Type
   translation : Type
   abort : Type

src/sail_lean_backend/pretty_print_lean.ml

@@ -1197,6 +1197,7 @@ let doc_instantiations ctx env =
              string "instance : Arch where";
              string "va_size := 64";
              string "pa := " ^^ doc_typ ctx params.pa_type;
+             string "pa_OfNat := BitVec.instOfNat"; (* TODO: Hardcoding this for now.. ^^ doc_typ ctx params.pa_type; *)
              string "abort := " ^^ doc_typ ctx params.abort_type;
              string "translation := " ^^ doc_typ ctx params.translation_summary_type;
              string "fault := " ^^ doc_typ ctx params.fault_type;

test/lean-riscv/LeanRiscv.lean

@@ -0,0 +1,95 @@
+-- This module serves as the root of the `LeanRiscv` library.
+-- Import modules here that should be built as part of the library.
+import ELFSage
+import LeanRV64D
+import LeanRV64D.Sail.Sail
+
+def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) := do
+  let bytes <- IO.FS.readBinFile elfFilepath
+  match mkRawELFFile? bytes with
+  | .error warning => do
+    pure (.error warning)
+  | .ok (.elf32 elf) => do
+    -- IO.println s!"{repr elf}"
+    pure (.ok elf)
+  | .ok (.elf64 _elf) => do
+    pure (.error "64 bit ELF file not supported")
+
+inductive MachineBits where
+  | B32
+  | B64
+
+def DEFAULT_RSTVEC := 0x00001000
+
+def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (BitVec 8) :=
+  -- From: sail-riscv/c_emulator/riscv_sim.cpp
+  --
+  -- let RST_VEC_SIZE : UInt32 := 8
+  -- let is_32bit_model := match size with
+  --   | .B32 => true
+  --   | .B64 => false
+  -- let entry : UInt64 := sorry
+  -- -- Little endian
+  -- let reset_vec : List UInt32 := [
+  --   0x297,                                                     -- auipc  t0,0x0
+  --   (0x28593 : UInt32) + (RST_VEC_SIZE * (4 : UInt32) <<< 20), -- addi   a1, t0, &dtb
+  --   0xf1402573,                                                -- csrr   a0, mhartid
+  --   if is_32bit_model then 0x0182a283                          -- lw     t0,24(t0)
+  --                     else 0x0182b283,                         -- ld     t0,24(t0)
+  --   0x28067,                                                   -- jr     t0
+  --   0,
+  --   UInt64.toUInt32 (entry &&& 0xffffffff),
+  --   UInt64.toUInt32 (entry >>> 32)
+  -- ]
+  -- let rv_rom_base := DEFAULT_RSTVEC
+
+  let update_mem_segment mem first_addr body :=
+    let addrs := Array.range' first_addr (Array.size body)
+    Array.foldl (λ mem (addr, byte) =>
+      if mem.contains addr then
+        panic s!"Address {addr} is already written to!"
+      else
+        mem.insert addr byte.toBitVec
+    ) mem (Array.zip addrs body)
+
+  -- Handle interpreted_segments
+  let mem'' := List.foldl (λ mem (_header, inst) =>
+          -- TODO(JP): Is this address correct?
+          update_mem_segment mem inst.segment_base inst.segment_body.data
+        ) default elf.interpreted_segments
+  -- Handle interpreted_sections
+  let mem' := mem''
+  -- let mem' := List.foldl (λ mem (_header, inst) =>
+  --         -- TODO(JP): Is this address correct?
+  --         update_mem_segment mem inst.section_offset inst.section_body.data
+  --       ) mem'' elf.interpreted_sections
+  -- Handle bits_and_bobs
+  let mem := List.foldl (λ mem (addr, data) =>
+          update_mem_segment mem addr data.data
+        ) mem' elf.bits_and_bobs
+
+  mem
+
+def initializeRegisters : Std.ExtDHashMap Register RegisterType :=
+  -- TODO: initialize register properly
+  Std.ExtDHashMap.emptyWithCapacity
+
+def my_main (_ : PUnit) :=
+  open LeanRV64D.Functions in
+  open Sail in
+  do
+  -- monadLift (IO.print "TEST")
+  -- let _ <- pure (unsafeIO (IO.print "TEST"))
+  dbg_trace "In my_main!"
+  -- print_effect
+  sail_main ()
+
+
+def runElf32 (elf : ELF32File) : IO UInt32 :=
+  open Sail in
+  open LeanRV64D.Functions in
+  let mem := initializeMemory MachineBits.B32 elf
+  let regs := initializeRegisters
+  let initialState := ⟨regs, (), mem, default, default, default⟩
+  main_of_sail_main initialState (sail_model_init >=> my_main)
+  -- main_of_sail_main initialState my_main

test/lean-riscv/LeanRiscv/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

test/lean-riscv/Main.lean

@@ -0,0 +1,20 @@
+import LeanRiscv
+
+def main (args : List String) : IO UInt32 := do
+  if args.length != 2 then do
+    IO.println "usage: run-riscv-lean <elf_file>"
+
+    pure 255
+  else do
+    -- Parse input elf file.
+    let elfE <- readElf32 args[1]!
+    match elfE with
+    | Except.error err => do
+      IO.println "Failed to parse elf file:"
+      IO.println err
+
+      pure 255
+
+    | Except.ok elf => do
+      -- Run program
+      runElf32 elf

test/lean-riscv/README.md

@@ -0,0 +1 @@
+# lean-riscv

test/lean-riscv/lake-manifest.json

@@ -0,0 +1,35 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/opencompl/sail-riscv-lean.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
+   "name": "Lean_RV64D",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/jn80842/ELFSage.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3cbf753d3596f9c361f877950fb079de701c0144",
+   "name": "ELFSage",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3cbf753d3596f9c361f877950fb079de701c0144",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "427778edba8deb053372e5d9de22dc5426b6d175",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«lean-riscv»",
+ "lakeDir": ".lake"}

test/lean-riscv/lakefile.toml

@@ -0,0 +1,22 @@
+name = "lean-riscv"
+version = "0.1.0"
+defaultTargets = ["run-riscv-lean"]
+
+[[lean_lib]]
+name = "LeanRiscv"
+
+[[lean_exe]]
+name = "run-riscv-lean"
+root = "Main"
+
+[[require]]
+name = "ELFSage"
+git = "https://github.com/jn80842/ELFSage.git"
+rev = "3cbf753d3596f9c361f877950fb079de701c0144"
+
+[[require]]
+name = "Lean_RV64D"
+git = "https://github.com/opencompl/sail-riscv-lean.git"
+rev = "5b601c9012c093087e1584f7a2dc3972838f1b54"
+
+

test/lean-riscv/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2025-05-26