From 14d2eaa60bdd06f7a04177f19e5ee69c1798b3d2 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 13 Mar 2025 11:58:56 -0400
Subject: [PATCH 01/18] Initialize Lean testing for RISC-V tests

---
 test/lean-riscv/LeanRiscv.lean       |  4 ++++
 test/lean-riscv/LeanRiscv/Basic.lean |  1 +
 test/lean-riscv/Main.lean            |  4 ++++
 test/lean-riscv/README.md            |  1 +
 test/lean-riscv/lake-manifest.json   | 25 +++++++++++++++++++++++++
 test/lean-riscv/lakefile.toml        | 15 +++++++++++++++
 test/lean-riscv/lean-toolchain       |  1 +
 7 files changed, 51 insertions(+)
 create mode 100644 test/lean-riscv/LeanRiscv.lean
 create mode 100644 test/lean-riscv/LeanRiscv/Basic.lean
 create mode 100644 test/lean-riscv/Main.lean
 create mode 100644 test/lean-riscv/README.md
 create mode 100644 test/lean-riscv/lake-manifest.json
 create mode 100644 test/lean-riscv/lakefile.toml
 create mode 100644 test/lean-riscv/lean-toolchain

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
new file mode 100644
index 000000000..6eba14612
--- /dev/null
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -0,0 +1,4 @@
+-- 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 LeanRiscv.Basic
diff --git a/test/lean-riscv/LeanRiscv/Basic.lean b/test/lean-riscv/LeanRiscv/Basic.lean
new file mode 100644
index 000000000..99415d9d9
--- /dev/null
+++ b/test/lean-riscv/LeanRiscv/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
diff --git a/test/lean-riscv/Main.lean b/test/lean-riscv/Main.lean
new file mode 100644
index 000000000..a3136a6ae
--- /dev/null
+++ b/test/lean-riscv/Main.lean
@@ -0,0 +1,4 @@
+import LeanRiscv
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/test/lean-riscv/README.md b/test/lean-riscv/README.md
new file mode 100644
index 000000000..c9232798e
--- /dev/null
+++ b/test/lean-riscv/README.md
@@ -0,0 +1 @@
+# lean-riscv
\ No newline at end of file
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
new file mode 100644
index 000000000..d02aed049
--- /dev/null
+++ b/test/lean-riscv/lake-manifest.json
@@ -0,0 +1,25 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/draperlaboratory/ELFSage",
+   "type": "git",
+   "subDir": null,
+   "scope": "draperlaboratory",
+   "rev": "8f3d6e753febf602a07a4495504738b968719520",
+   "name": "ELFSage",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "8f3d6e7",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«lean-riscv»",
+ "lakeDir": ".lake"}
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
new file mode 100644
index 000000000..73c854a1e
--- /dev/null
+++ b/test/lean-riscv/lakefile.toml
@@ -0,0 +1,15 @@
+name = "lean-riscv"
+version = "0.1.0"
+defaultTargets = ["lean-riscv"]
+
+[[lean_lib]]
+name = "LeanRiscv"
+
+[[lean_exe]]
+name = "lean-riscv"
+root = "Main"
+
+[[require]]
+name = "ELFSage"
+scope = "draperlaboratory"
+rev = "8f3d6e7"
diff --git a/test/lean-riscv/lean-toolchain b/test/lean-riscv/lean-toolchain
new file mode 100644
index 000000000..143740cb3
--- /dev/null
+++ b/test/lean-riscv/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2024-10-07

From 159ec8421bfcb6992b79528ea352499a805ee4b2 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 13 Mar 2025 14:19:25 -0400
Subject: [PATCH 02/18] Parse an elf file

---
 test/lean-riscv/LeanRiscv.lean | 13 ++++++++++++-
 test/lean-riscv/Main.lean      | 15 +++++++++++++--
 test/lean-riscv/lakefile.toml  |  4 ++--
 3 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 6eba14612..7e0b7dd9a 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -1,4 +1,15 @@
 -- 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 LeanRiscv.Basic
+
+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
+    -- sorry
+    IO.println s!"{repr elf}"
+    pure (.ok elf)
+  | .ok (.elf64 elf) => do
+    pure (.error "64 bit ELF file not supported")
diff --git a/test/lean-riscv/Main.lean b/test/lean-riscv/Main.lean
index a3136a6ae..7ff6cc0b1 100644
--- a/test/lean-riscv/Main.lean
+++ b/test/lean-riscv/Main.lean
@@ -1,4 +1,15 @@
 import LeanRiscv
 
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+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 elfF <- readElf32 args[1]!
+    
+    pure 0
+    -- TODO:
+    -- Convert to Sail's AST
+    -- Run program
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 73c854a1e..965db3078 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -1,12 +1,12 @@
 name = "lean-riscv"
 version = "0.1.0"
-defaultTargets = ["lean-riscv"]
+defaultTargets = ["run-riscv-lean"]
 
 [[lean_lib]]
 name = "LeanRiscv"
 
 [[lean_exe]]
-name = "lean-riscv"
+name = "run-riscv-lean"
 root = "Main"
 
 [[require]]

From f6f7a10212d597655a6de34b52ed84649fee835d Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 18 Mar 2025 17:26:47 -0400
Subject: [PATCH 03/18] Update ELFSage to patched version

---
 test/lean-riscv/lake-manifest.json | 26 +++++++++++++-------------
 test/lean-riscv/lakefile.toml      |  5 +++--
 test/lean-riscv/lean-toolchain     |  2 +-
 3 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index d02aed049..13f929060 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -1,25 +1,25 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/draperlaboratory/ELFSage",
-   "type": "git",
-   "subDir": null,
-   "scope": "draperlaboratory",
-   "rev": "8f3d6e753febf602a07a4495504738b968719520",
-   "name": "ELFSage",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "8f3d6e7",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli.git",
+ [{"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/ineol/ELFSage.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f9b66dc2f1d3beb409d8982b3452e60edfae5d99",
+   "name": "ELFSage",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "f9b66dc2f1d3beb409d8982b3452e60edfae5d99",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "«lean-riscv»",
  "lakeDir": ".lake"}
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 965db3078..89277b12f 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -11,5 +11,6 @@ root = "Main"
 
 [[require]]
 name = "ELFSage"
-scope = "draperlaboratory"
-rev = "8f3d6e7"
+git = "https://github.com/ineol/ELFSage.git"
+rev = "f9b66dc2f1d3beb409d8982b3452e60edfae5d99"
+
diff --git a/test/lean-riscv/lean-toolchain b/test/lean-riscv/lean-toolchain
index 143740cb3..2b37244f7 100644
--- a/test/lean-riscv/lean-toolchain
+++ b/test/lean-riscv/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-07
+leanprover/lean4:nightly-2025-03-17

From 07a92551d848765bee957a6acc7ee476a48bdd87 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 18 Mar 2025 22:21:28 -0400
Subject: [PATCH 04/18] Attempt to add and use RISC-V model as dependency

---
 test/lean-riscv/LeanRiscv.lean     | 16 ++++++++++++++++
 test/lean-riscv/Main.lean          |  9 ++++++---
 test/lean-riscv/lake-manifest.json | 24 +++++++++++++++++-------
 test/lean-riscv/lakefile.toml      |  6 ++++++
 4 files changed, 45 insertions(+), 10 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 7e0b7dd9a..ffd64cacb 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -1,6 +1,8 @@
 -- 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 LeanRV64DLEAN
+import LeanRV64DLEAN.Sail.Sail
 
 def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) := do
   let bytes <- IO.FS.readBinFile elfFilepath
@@ -13,3 +15,17 @@ def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) :=
     pure (.ok elf)
   | .ok (.elf64 elf) => do
     pure (.error "64 bit ELF file not supported")
+
+
+#check mkRawELFFile?
+-- #check sail_model_init
+
+-- open LeanRV64DLEAN.Sail.Sail
+def runElf32 (elf : EF32File) : IO PUnit := do
+    -- IO.println "TODO"
+    let _ := sail_model_init
+    main_of_sail_main ⟨default, (), default, default, default, default⟩ (sail_model_init >=> sail_main)
+
+
+  
+
diff --git a/test/lean-riscv/Main.lean b/test/lean-riscv/Main.lean
index 7ff6cc0b1..01df4e8e6 100644
--- a/test/lean-riscv/Main.lean
+++ b/test/lean-riscv/Main.lean
@@ -8,8 +8,11 @@ def main (args : List String) : IO UInt32 := do
   else do
     -- Parse input elf file.
     let elfF <- readElf32 args[1]!
-    
-    pure 0
+
     -- TODO:
-    -- Convert to Sail's AST
     -- Run program
+    runElf32 elfF
+
+
+    
+    pure 0
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 13f929060..2235add2e 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -1,15 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/lean4-cli.git",
+ [{"url": "https://github.com/ineol/sail-riscv.git",
    "type": "git",
-   "subDir": null,
+   "subDir": "build/model/Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
-   "name": "Cli",
+   "rev": "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6",
+   "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6",
+   "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/ineol/ELFSage.git",
    "type": "git",
@@ -20,6 +20,16 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "f9b66dc2f1d3beb409d8982b3452e60edfae5d99",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "«lean-riscv»",
  "lakeDir": ".lake"}
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 89277b12f..9aa6d851c 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -14,3 +14,9 @@ name = "ELFSage"
 git = "https://github.com/ineol/ELFSage.git"
 rev = "f9b66dc2f1d3beb409d8982b3452e60edfae5d99"
 
+[[require]]
+name = "Lean_RV64D_LEAN"
+git = "https://github.com/ineol/sail-riscv.git"
+rev = "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6"
+subDir = "build/model/Lean_RV64D_LEAN"
+

From 053d96fe80f253f6b007c244fc6c6a090ed53170 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 18 Mar 2025 22:36:29 -0400
Subject: [PATCH 05/18] Imports working

---
 test/lean-riscv/LeanRiscv.lean | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index ffd64cacb..5f247f0a0 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -1,7 +1,7 @@
 -- 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 LeanRV64DLEAN
+import LeanRV64DLEAN
 import LeanRV64DLEAN.Sail.Sail
 
 def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) := do
@@ -17,14 +17,12 @@ def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) :=
     pure (.error "64 bit ELF file not supported")
 
 
-#check mkRawELFFile?
--- #check sail_model_init
-
--- open LeanRV64DLEAN.Sail.Sail
-def runElf32 (elf : EF32File) : IO PUnit := do
-    -- IO.println "TODO"
-    let _ := sail_model_init
-    main_of_sail_main ⟨default, (), default, default, default, default⟩ (sail_model_init >=> sail_main)
+def runElf32 (elf : EF32File) : IO UInt32 :=
+  open Sail in
+  open Functions in
+  do
+  -- IO.println "TODO"
+  main_of_sail_main ⟨default, (), default, default, default, default⟩ (sail_model_init >=> sail_main)
 
 
   

From 01c7d9c8eaa511e54bf874d0b59fe2d79d693848 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 19 Mar 2025 15:55:05 -0400
Subject: [PATCH 06/18] Initial ELF in memory

---
 test/lean-riscv/LeanRiscv.lean | 76 ++++++++++++++++++++++++++++++----
 test/lean-riscv/Main.lean      |  5 +--
 2 files changed, 68 insertions(+), 13 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 5f247f0a0..d81551f36 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -10,20 +10,78 @@ def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) :=
   | .error warning => do
     pure (.error warning)
   | .ok (.elf32 elf) => do
-    -- sorry
-    IO.println s!"{repr elf}"
+    -- IO.println s!"{repr elf}"
     pure (.ok elf)
-  | .ok (.elf64 elf) => do
+  | .ok (.elf64 _elf) => do
     pure (.error "64 bit ELF file not supported")
 
+inductive MachineBits where
+  | B32
+  | B64
 
-def runElf32 (elf : EF32File) : IO UInt32 :=
-  open Sail in
-  open Functions in
-  do
-  -- IO.println "TODO"
-  main_of_sail_main ⟨default, (), default, default, default, default⟩ (sail_model_init >=> sail_main)
+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_offset inst.segment_body.data
+        ) default elf.interpreted_segments
+  -- Handle interpreted_sections
+  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.DHashMap Register RegisterType :=
+  Std.DHashMap.insert default sorry sorry -- DEFAULT_RSTVEC
+
+#check @Register
+#check @RegisterType
+
+
+noncomputable def runElf32 (elf : ELF32File) : IO UInt32 :=
+  open Sail in
+  open 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 >=> sail_main)
   
 
diff --git a/test/lean-riscv/Main.lean b/test/lean-riscv/Main.lean
index 01df4e8e6..a43f7dbe2 100644
--- a/test/lean-riscv/Main.lean
+++ b/test/lean-riscv/Main.lean
@@ -9,10 +9,7 @@ def main (args : List String) : IO UInt32 := do
     -- Parse input elf file.
     let elfF <- readElf32 args[1]!
 
-    -- TODO:
     -- Run program
-    runElf32 elfF
-
-
+    -- runElf32 elfF
     
     pure 0

From 801d563c7ede8992bbc734a65fff6c547866e357 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 20 Mar 2025 10:02:11 -0400
Subject: [PATCH 07/18] Add `pa_OfNat` to `Arch` class

---
 src/sail_lean_backend/Sail/Sail.lean       | 1 +
 src/sail_lean_backend/pretty_print_lean.ml | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
index 31aee2cb2..f286675f6 100644
--- a/src/sail_lean_backend/Sail/Sail.lean
+++ b/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 : forall n, OfNat pa n
   arch_ak : Type
   translation : Type
   abort : Type
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index e1125313a..5f6dbf129 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/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 := fun i => BitVec.instOfNat (n := 64) (i := i)"; (* 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;

From c1a6dd26df5aa97ea90c5b72c8bb583161c4ed66 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 20 Mar 2025 10:36:38 -0400
Subject: [PATCH 08/18] Fix `pa_OfNat`

---
 src/sail_lean_backend/Sail/Sail.lean       | 2 +-
 src/sail_lean_backend/pretty_print_lean.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
index f286675f6..fbe2122fd 100644
--- a/src/sail_lean_backend/Sail/Sail.lean
+++ b/src/sail_lean_backend/Sail/Sail.lean
@@ -220,7 +220,7 @@ def trivialChoiceSource : ChoiceSource where
 class Arch where
   va_size : Nat
   pa : Type
-  pa_OfNat : forall n, OfNat pa n
+  pa_OfNat {n : Nat} : OfNat pa n
   arch_ak : Type
   translation : Type
   abort : Type
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 5f6dbf129..c5205d4ce 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -1197,7 +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 := fun i => BitVec.instOfNat (n := 64) (i := i)"; (* TODO: Hardcoding this for now.. ^^ 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;

From ce235a9ea6e206640cfd25152802db8e78008bf5 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 20 Mar 2025 11:17:21 -0400
Subject: [PATCH 09/18] Update dependency to Lean model with axioms removed

---
 test/lean-riscv/LeanRiscv.lean     | 4 ----
 test/lean-riscv/lake-manifest.json | 4 ++--
 test/lean-riscv/lakefile.toml      | 2 +-
 3 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index d81551f36..a55b9fa7d 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -72,10 +72,6 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
 def initializeRegisters : Std.DHashMap Register RegisterType :=
   Std.DHashMap.insert default sorry sorry -- DEFAULT_RSTVEC
 
-#check @Register
-#check @RegisterType
-
-
 noncomputable def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
   open Functions in
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 2235add2e..33f7a6b67 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "build/model/Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6",
+   "rev": "745fa2f5cb099ba9c5d8c652c3c8473278703a6b",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6",
+   "inputRev": "745fa2f5cb099ba9c5d8c652c3c8473278703a6b",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/ineol/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 9aa6d851c..4e741093b 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "f9b66dc2f1d3beb409d8982b3452e60edfae5d99"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "e730c409acf5cf1b6935e9c79b576ab0b7ab1bf6"
+rev = "745fa2f5cb099ba9c5d8c652c3c8473278703a6b"
 subDir = "build/model/Lean_RV64D_LEAN"
 

From 4731737a0f1daf933a2d02a469eb27a4509b4ace Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 26 Mar 2025 17:55:31 +0200
Subject: [PATCH 10/18] Update dependencies

---
 test/lean-riscv/lake-manifest.json | 4 ++--
 test/lean-riscv/lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 33f7a6b67..f03faf070 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "build/model/Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "745fa2f5cb099ba9c5d8c652c3c8473278703a6b",
+   "rev": "3930f37cdc31049b380c8cbc6f6dc989bd097809",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "745fa2f5cb099ba9c5d8c652c3c8473278703a6b",
+   "inputRev": "3930f37cdc31049b380c8cbc6f6dc989bd097809",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/ineol/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 4e741093b..68f16cfbd 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "f9b66dc2f1d3beb409d8982b3452e60edfae5d99"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "745fa2f5cb099ba9c5d8c652c3c8473278703a6b"
+rev = "3930f37cdc31049b380c8cbc6f6dc989bd097809"
 subDir = "build/model/Lean_RV64D_LEAN"
 

From 7dec8d0e7fb3c05aa4d79aafc748e31af5df385b Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 8 Apr 2025 16:37:09 -0400
Subject: [PATCH 11/18] Update to computable dependencies

---
 test/lean-riscv/LeanRiscv.lean     | 12 +++++++-----
 test/lean-riscv/Main.lean          | 15 ++++++++++-----
 test/lean-riscv/lake-manifest.json | 14 +++++++-------
 test/lean-riscv/lakefile.toml      |  8 ++++----
 test/lean-riscv/lean-toolchain     |  2 +-
 5 files changed, 29 insertions(+), 22 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index a55b9fa7d..f49dae40f 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -10,7 +10,7 @@ def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) :=
   | .error warning => do
     pure (.error warning)
   | .ok (.elf32 elf) => do
-    -- IO.println s!"{repr elf}"
+    IO.println s!"{repr elf}"
     pure (.ok elf)
   | .ok (.elf64 _elf) => do
     pure (.error "64 bit ELF file not supported")
@@ -55,7 +55,7 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
   -- Handle interpreted_segments
   let mem'' := List.foldl (λ mem (_header, inst) => 
           -- TODO(JP): Is this address correct?
-          update_mem_segment mem inst.segment_offset inst.segment_body.data
+          update_mem_segment mem inst.segment_base inst.segment_body.data
         ) default elf.interpreted_segments
   -- Handle interpreted_sections
   let mem' := List.foldl (λ mem (_header, inst) => 
@@ -70,11 +70,13 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
   mem
 
 def initializeRegisters : Std.DHashMap Register RegisterType :=
-  Std.DHashMap.insert default sorry sorry -- DEFAULT_RSTVEC
+  Std.DHashMap.empty
+  -- TODO: initialize register properly
+  -- Std.DHashMap.insert default sorry sorry -- DEFAULT_RSTVEC
 
-noncomputable def runElf32 (elf : ELF32File) : IO UInt32 :=
+def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
-  open Functions in
+  open LeanRV64DLEAN.Functions in
   let mem := initializeMemory MachineBits.B32 elf
   let regs := initializeRegisters
   let initialState := ⟨regs, (), mem, default, default, default⟩
diff --git a/test/lean-riscv/Main.lean b/test/lean-riscv/Main.lean
index a43f7dbe2..9c334afc8 100644
--- a/test/lean-riscv/Main.lean
+++ b/test/lean-riscv/Main.lean
@@ -7,9 +7,14 @@ def main (args : List String) : IO UInt32 := do
     pure 255
   else do
     -- Parse input elf file.
-    let elfF <- readElf32 args[1]!
+    let elfE <- readElf32 args[1]!
+    match elfE with
+    | Except.error err => do
+      IO.println "Failed to parse elf file:"
+      IO.println err
 
-    -- Run program
-    -- runElf32 elfF
-    
-    pure 0
+      pure 255
+      
+    | Except.ok elf => do
+      -- Run program
+      runElf32 elf
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index f03faf070..a75551aef 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -3,29 +3,29 @@
  "packages":
  [{"url": "https://github.com/ineol/sail-riscv.git",
    "type": "git",
-   "subDir": "build/model/Lean_RV64D_LEAN",
+   "subDir": "Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "3930f37cdc31049b380c8cbc6f6dc989bd097809",
+   "rev": "a091b3cbb6ee057d7c78084fa44835ad40b85230",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3930f37cdc31049b380c8cbc6f6dc989bd097809",
+   "inputRev": "a091b3cbb6ee057d7c78084fa44835ad40b85230",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/ineol/ELFSage.git",
+  {"url": "https://github.com/GaloisInc/ELFSage.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f9b66dc2f1d3beb409d8982b3452e60edfae5d99",
+   "rev": "0338e21ae318eeea9ce551345f1b5288bc36e238",
    "name": "ELFSage",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f9b66dc2f1d3beb409d8982b3452e60edfae5d99",
+   "inputRev": "0338e21ae318eeea9ce551345f1b5288bc36e238",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
+   "rev": "427778edba8deb053372e5d9de22dc5426b6d175",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 68f16cfbd..0b0c344a0 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -11,12 +11,12 @@ root = "Main"
 
 [[require]]
 name = "ELFSage"
-git = "https://github.com/ineol/ELFSage.git"
-rev = "f9b66dc2f1d3beb409d8982b3452e60edfae5d99"
+git = "https://github.com/GaloisInc/ELFSage.git"
+rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
 
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "3930f37cdc31049b380c8cbc6f6dc989bd097809"
-subDir = "build/model/Lean_RV64D_LEAN"
+rev = "a091b3cbb6ee057d7c78084fa44835ad40b85230"
+subDir = "Lean_RV64D_LEAN"
 
diff --git a/test/lean-riscv/lean-toolchain b/test/lean-riscv/lean-toolchain
index 2b37244f7..dcca6df98 100644
--- a/test/lean-riscv/lean-toolchain
+++ b/test/lean-riscv/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-03-17
+lean4

From 7a2a2f7925e2aef350b20f432b329faafb45f6a1 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 8 Apr 2025 17:22:50 -0400
Subject: [PATCH 12/18] Don't load sections into memory

---
 test/lean-riscv/LeanRiscv.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index f49dae40f..9a176aaa7 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -58,10 +58,11 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
           update_mem_segment mem inst.segment_base inst.segment_body.data
         ) default elf.interpreted_segments
   -- Handle interpreted_sections
-  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
+  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

From fbc0c31515b3e4a8b77ad61c5f2f30a2dea65ffd Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 9 Apr 2025 15:20:14 -0400
Subject: [PATCH 13/18] Update dependency to hack PC

---
 test/lean-riscv/LeanRiscv.lean     | 18 ++++++++++++++----
 test/lean-riscv/lake-manifest.json |  4 ++--
 test/lean-riscv/lakefile.toml      |  2 +-
 3 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 9a176aaa7..4e618b116 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -10,7 +10,7 @@ def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) :=
   | .error warning => do
     pure (.error warning)
   | .ok (.elf32 elf) => do
-    IO.println s!"{repr elf}"
+    -- IO.println s!"{repr elf}"
     pure (.ok elf)
   | .ok (.elf64 _elf) => do
     pure (.error "64 bit ELF file not supported")
@@ -71,9 +71,18 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
   mem
 
 def initializeRegisters : Std.DHashMap Register RegisterType :=
-  Std.DHashMap.empty
   -- TODO: initialize register properly
-  -- Std.DHashMap.insert default sorry sorry -- DEFAULT_RSTVEC
+  Std.DHashMap.empty
+
+def my_main (_ : PUnit) :=
+  open LeanRV64DLEAN.Functions in
+  open Sail in
+  do
+  -- monadLift (IO.print "TEST")
+  -- let _ <- pure (unsafeIO (IO.print "TEST"))
+  print_effect "TEST!"
+  -- print_effect
+  sail_main ()
 
 def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
@@ -81,6 +90,7 @@ def runElf32 (elf : ELF32File) : IO UInt32 :=
   let mem := initializeMemory MachineBits.B32 elf
   let regs := initializeRegisters
   let initialState := ⟨regs, (), mem, default, default, default⟩
-  main_of_sail_main initialState (sail_model_init >=> sail_main)
+  main_of_sail_main initialState (sail_model_init >=> my_main)
+  -- main_of_sail_main initialState my_main
   
 
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index a75551aef..31f78bd10 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "a091b3cbb6ee057d7c78084fa44835ad40b85230",
+   "rev": "548be075a7b875a599717db1ca6a2a096e50a652",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a091b3cbb6ee057d7c78084fa44835ad40b85230",
+   "inputRev": "548be075a7b875a599717db1ca6a2a096e50a652",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/GaloisInc/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 0b0c344a0..fcb4973bf 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "a091b3cbb6ee057d7c78084fa44835ad40b85230"
+rev = "548be075a7b875a599717db1ca6a2a096e50a652"
 subDir = "Lean_RV64D_LEAN"
 

From 4c35c76a091a1c4bb1d765e9c238b01044c967a8 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 9 Apr 2025 16:47:11 -0400
Subject: [PATCH 14/18] Include more hacks in dependencies

---
 test/lean-riscv/lake-manifest.json | 4 ++--
 test/lean-riscv/lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 31f78bd10..5e035f877 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "548be075a7b875a599717db1ca6a2a096e50a652",
+   "rev": "7f5683e64ee694253383fbb0ffced028536c4e90",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "548be075a7b875a599717db1ca6a2a096e50a652",
+   "inputRev": "7f5683e64ee694253383fbb0ffced028536c4e90",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/GaloisInc/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index fcb4973bf..47ec143ae 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "548be075a7b875a599717db1ca6a2a096e50a652"
+rev = "7f5683e64ee694253383fbb0ffced028536c4e90"
 subDir = "Lean_RV64D_LEAN"
 

From a260bf3d6d8419e552f57dd4b7dcedd2bb501291 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Fri, 11 Apr 2025 14:51:06 -0400
Subject: [PATCH 15/18] Debugging with Lee

---
 test/lean-riscv/LeanRiscv.lean     | 3 ++-
 test/lean-riscv/lake-manifest.json | 4 ++--
 test/lean-riscv/lakefile.toml      | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 4e618b116..48e33baae 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -80,10 +80,11 @@ def my_main (_ : PUnit) :=
   do
   -- monadLift (IO.print "TEST")
   -- let _ <- pure (unsafeIO (IO.print "TEST"))
-  print_effect "TEST!"
+  dbg_trace "In my_main!"
   -- print_effect
   sail_main ()
 
+
 def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
   open LeanRV64DLEAN.Functions in
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 5e035f877..3cc6f90c7 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "7f5683e64ee694253383fbb0ffced028536c4e90",
+   "rev": "520cbc8f7888f9957e8a872eaae5344138f6caae",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7f5683e64ee694253383fbb0ffced028536c4e90",
+   "inputRev": "520cbc8f7888f9957e8a872eaae5344138f6caae",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/GaloisInc/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 47ec143ae..d3e9ef9bb 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "7f5683e64ee694253383fbb0ffced028536c4e90"
+rev = "520cbc8f7888f9957e8a872eaae5344138f6caae"
 subDir = "Lean_RV64D_LEAN"
 

From d0d30a078f120c06a369c9300c90f82e1ecb1f2f Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Wed, 16 Apr 2025 17:14:20 -0400
Subject: [PATCH 16/18] Update dependencies

---
 test/lean-riscv/lake-manifest.json | 4 ++--
 test/lean-riscv/lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 3cc6f90c7..0ae5bf435 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": "Lean_RV64D_LEAN",
    "scope": "",
-   "rev": "520cbc8f7888f9957e8a872eaae5344138f6caae",
+   "rev": "169afb2eb695a5f71f09dbd615cb660280f62ccb",
    "name": "Lean_RV64D_LEAN",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "520cbc8f7888f9957e8a872eaae5344138f6caae",
+   "inputRev": "169afb2eb695a5f71f09dbd615cb660280f62ccb",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/GaloisInc/ELFSage.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index d3e9ef9bb..67a51d6b4 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -17,6 +17,6 @@ rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
 [[require]]
 name = "Lean_RV64D_LEAN"
 git = "https://github.com/ineol/sail-riscv.git"
-rev = "520cbc8f7888f9957e8a872eaae5344138f6caae"
+rev = "169afb2eb695a5f71f09dbd615cb660280f62ccb"
 subDir = "Lean_RV64D_LEAN"
 

From 201341fbc23d883d7728574ba837e181669228e7 Mon Sep 17 00:00:00 2001
From: jn80842 <newcomb@galois.com>
Date: Thu, 29 May 2025 19:39:30 -0700
Subject: [PATCH 17/18] point lean emulator at current sail-riscv-lean build

---
 test/lean-riscv/LeanRiscv.lean     | 18 ++++++++----------
 test/lean-riscv/lake-manifest.json | 16 ++++++++--------
 test/lean-riscv/lakefile.toml      | 12 ++++++------
 test/lean-riscv/lean-toolchain     |  2 +-
 4 files changed, 23 insertions(+), 25 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 48e33baae..218ccfd22 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -1,8 +1,8 @@
 -- 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 LeanRV64DLEAN
-import LeanRV64DLEAN.Sail.Sail
+import LeanRV64D
+import LeanRV64D.Sail.Sail
 
 def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) := do
   let bytes <- IO.FS.readBinFile elfFilepath
@@ -45,7 +45,7 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
 
   let update_mem_segment mem first_addr body :=
     let addrs := Array.range' first_addr (Array.size body)
-    Array.foldl (λ mem (addr, byte) => 
+    Array.foldl (λ mem (addr, byte) =>
       if mem.contains addr then
         panic s!"Address {addr} is already written to!"
       else
@@ -53,7 +53,7 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
     ) mem (Array.zip addrs body)
 
   -- Handle interpreted_segments
-  let mem'' := List.foldl (λ mem (_header, inst) => 
+  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
@@ -70,12 +70,12 @@ def initializeMemory (_size: MachineBits) (elf : ELF32File) : Std.HashMap Nat (B
 
   mem
 
-def initializeRegisters : Std.DHashMap Register RegisterType :=
+def initializeRegisters : Std.ExtDHashMap Register RegisterType :=
   -- TODO: initialize register properly
-  Std.DHashMap.empty
+  Std.ExtDHashMap.emptyWithCapacity
 
 def my_main (_ : PUnit) :=
-  open LeanRV64DLEAN.Functions in
+  open LeanRV64D.Functions in
   open Sail in
   do
   -- monadLift (IO.print "TEST")
@@ -87,11 +87,9 @@ def my_main (_ : PUnit) :=
 
 def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
-  open LeanRV64DLEAN.Functions 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
-  
-
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index 0ae5bf435..a00f1951b 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -1,24 +1,24 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/ineol/sail-riscv.git",
+ [{"url": "https://github.com/opencompl/sail-riscv-lean.git",
    "type": "git",
-   "subDir": "Lean_RV64D_LEAN",
+   "subDir": null,
    "scope": "",
-   "rev": "169afb2eb695a5f71f09dbd615cb660280f62ccb",
-   "name": "Lean_RV64D_LEAN",
+   "rev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
+   "name": "Lean_RV64D",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "169afb2eb695a5f71f09dbd615cb660280f62ccb",
+   "inputRev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/GaloisInc/ELFSage.git",
+  {"url": "https://github.com/jn80842/ELFSage.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0338e21ae318eeea9ce551345f1b5288bc36e238",
+   "rev": "3cbf753d3596f9c361f877950fb079de701c0144",
    "name": "ELFSage",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0338e21ae318eeea9ce551345f1b5288bc36e238",
+   "inputRev": "3cbf753d3596f9c361f877950fb079de701c0144",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 67a51d6b4..8cdf272e2 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -11,12 +11,12 @@ root = "Main"
 
 [[require]]
 name = "ELFSage"
-git = "https://github.com/GaloisInc/ELFSage.git"
-rev = "0338e21ae318eeea9ce551345f1b5288bc36e238"
+git = "https://github.com/jn80842/ELFSage.git"
+rev = "3cbf753d3596f9c361f877950fb079de701c0144"
 
 [[require]]
-name = "Lean_RV64D_LEAN"
-git = "https://github.com/ineol/sail-riscv.git"
-rev = "169afb2eb695a5f71f09dbd615cb660280f62ccb"
-subDir = "Lean_RV64D_LEAN"
+name = "Lean_RV64D"
+git = "https://github.com/opencompl/sail-riscv-lean.git"
+rev = "5b601c9012c093087e1584f7a2dc3972838f1b54"
+
 
diff --git a/test/lean-riscv/lean-toolchain b/test/lean-riscv/lean-toolchain
index dcca6df98..c315f9cd2 100644
--- a/test/lean-riscv/lean-toolchain
+++ b/test/lean-riscv/lean-toolchain
@@ -1 +1 @@
-lean4
+leanprover/lean4:nightly-2025-05-26
\ No newline at end of file

From 7a02b9d4a80b71cbccbfd5a04cd916ee015e1018 Mon Sep 17 00:00:00 2001
From: jn80842 <newcomb@galois.com>
Date: Wed, 4 Jun 2025 18:52:01 -0700
Subject: [PATCH 18/18] update configs for executable lean-riscv model

---
 test/lean-riscv/LeanRiscv.lean     |  8 ++++----
 test/lean-riscv/lake-manifest.json | 14 +++++++-------
 test/lean-riscv/lakefile.toml      |  9 +++++----
 test/lean-riscv/lean-toolchain     |  2 +-
 4 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/test/lean-riscv/LeanRiscv.lean b/test/lean-riscv/LeanRiscv.lean
index 218ccfd22..24299e619 100644
--- a/test/lean-riscv/LeanRiscv.lean
+++ b/test/lean-riscv/LeanRiscv.lean
@@ -1,8 +1,8 @@
 -- 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
+import LeanRV64DExecutable
+import LeanRV64DExecutable.Sail.Sail
 
 def readElf32 (elfFilepath : System.FilePath) : IO (Except String ELF32File) := do
   let bytes <- IO.FS.readBinFile elfFilepath
@@ -75,7 +75,7 @@ def initializeRegisters : Std.ExtDHashMap Register RegisterType :=
   Std.ExtDHashMap.emptyWithCapacity
 
 def my_main (_ : PUnit) :=
-  open LeanRV64D.Functions in
+  open LeanRV64DExecutable.Functions in
   open Sail in
   do
   -- monadLift (IO.print "TEST")
@@ -87,7 +87,7 @@ def my_main (_ : PUnit) :=
 
 def runElf32 (elf : ELF32File) : IO UInt32 :=
   open Sail in
-  open LeanRV64D.Functions in
+  open LeanRV64DExecutable.Functions in
   let mem := initializeMemory MachineBits.B32 elf
   let regs := initializeRegisters
   let initialState := ⟨regs, (), mem, default, default, default⟩
diff --git a/test/lean-riscv/lake-manifest.json b/test/lean-riscv/lake-manifest.json
index a00f1951b..98f7b1a3e 100644
--- a/test/lean-riscv/lake-manifest.json
+++ b/test/lean-riscv/lake-manifest.json
@@ -1,24 +1,24 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/opencompl/sail-riscv-lean.git",
+ [{"url": "https://github.com/jn80842/sail-riscv.git",
    "type": "git",
-   "subDir": null,
+   "subDir": "Lean_RV64D_executable",
    "scope": "",
-   "rev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
-   "name": "Lean_RV64D",
+   "rev": "822f0439d3f44af8bf585e16f4e4f25061a83469",
+   "name": "Lean_RV64D_executable",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5b601c9012c093087e1584f7a2dc3972838f1b54",
+   "inputRev": "822f0439d3f44af8bf585e16f4e4f25061a83469",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/jn80842/ELFSage.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3cbf753d3596f9c361f877950fb079de701c0144",
+   "rev": "d5ccd4520e3c51b855a3646ad83b316eaf7ad243",
    "name": "ELFSage",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3cbf753d3596f9c361f877950fb079de701c0144",
+   "inputRev": "d5ccd4520e3c51b855a3646ad83b316eaf7ad243",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli.git",
diff --git a/test/lean-riscv/lakefile.toml b/test/lean-riscv/lakefile.toml
index 8cdf272e2..fa9acf313 100644
--- a/test/lean-riscv/lakefile.toml
+++ b/test/lean-riscv/lakefile.toml
@@ -12,11 +12,12 @@ root = "Main"
 [[require]]
 name = "ELFSage"
 git = "https://github.com/jn80842/ELFSage.git"
-rev = "3cbf753d3596f9c361f877950fb079de701c0144"
+rev = "d5ccd4520e3c51b855a3646ad83b316eaf7ad243"
 
 [[require]]
-name = "Lean_RV64D"
-git = "https://github.com/opencompl/sail-riscv-lean.git"
-rev = "5b601c9012c093087e1584f7a2dc3972838f1b54"
+name = "Lean_RV64D_executable"
+git = "https://github.com/jn80842/sail-riscv.git"
+rev = "822f0439d3f44af8bf585e16f4e4f25061a83469"
+subDir = "Lean_RV64D_executable"
 
 
diff --git a/test/lean-riscv/lean-toolchain b/test/lean-riscv/lean-toolchain
index c315f9cd2..7ea4290d0 100644
--- a/test/lean-riscv/lean-toolchain
+++ b/test/lean-riscv/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-05-26
\ No newline at end of file
+leanprover/lean4-pr-releases:pr-release-8577
\ No newline at end of file