From 315e3a6c878c097357566d7add2355203057404d Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Thu, 23 May 2024 19:26:04 -0500
Subject: [PATCH 1/2] Bump lean-toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 1a4d2185..7e31ea5c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-05-16
+leanprover/lean4:nightly-2024-05-23

From b232891359301bdee8bf09213e18e533ef85ba34 Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Thu, 23 May 2024 19:26:31 -0500
Subject: [PATCH 2/2] Add functions to trace the ArmState during concrete
 simulations

---
 .gitignore                                    |  1 +
 .../LDST/Advanced_simd_multiple_struct.lean   |  2 +-
 Tests/Debug.lean                              | 63 +++++++++++++++++++
 Tests/SHA512ProgramTest.lean                  |  5 ++
 4 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 Tests/Debug.lean

diff --git a/.gitignore b/.gitignore
index 796aa295..eb73941b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@
 /lakefile.olean
 /lake-packages/*
 /.lake/*
+*.log
\ No newline at end of file
diff --git a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
index 8d9eb70c..9964fa4b 100644
--- a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
+++ b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
@@ -27,7 +27,7 @@ deriving DecidableEq, Repr
 @[state_simp_rules]
 def ld1_st1_operation (wback : Bool) (inst : Multiple_struct_inst_fields)
   (inst_str : String) (s : ArmState)
-  (H_opcode : inst.opcode ∈
+  (_H_opcode : inst.opcode ∈
               [0b0000#4, 0b0010#4, 0b0100#4, 0b0110#4, 0b0111#4,
               0b1000#4, 0b1010#4])
   : ArmState :=
diff --git a/Tests/Debug.lean b/Tests/Debug.lean
new file mode 100644
index 00000000..940c5934
--- /dev/null
+++ b/Tests/Debug.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
+
+-- Some utilities for debugging concrete simulations
+
+import Arm.Exec
+
+section Debug
+
+open BitVec
+
+/-- `trace_run`: Print `(debug s)` before simulating each instruction. -/
+def trace_run (debug : ArmState → String) (n : Nat) (s : ArmState) : ArmState :=
+  match n with
+  | 0 => s
+  | n' + 1 =>
+    dbg_trace (debug s)
+    let s' := stepi s
+    trace_run debug n' s'
+
+/-- `log_run`: Log `(debug s)` to a file `filename` before
+     simulating each instruction. Note that we append to file, so
+     any old contents are not overwritten. -/
+def log_run (filename : System.FilePath) (debug : ArmState → String)
+  (n : Nat) (s : ArmState) : IO ArmState := do
+  let h ← IO.FS.Handle.mk filename IO.FS.Mode.append
+  h.putStrLn (debug s)
+  match n with
+  | 0 => pure s
+  | n' + 1 =>
+    let s' := stepi s
+    log_run filename debug n' s'
+
+/-- `run_until`: Run until `cond` is true or `n` instructions are simulated,
+  whichever comes first. -/
+def run_until (cond : ArmState → Bool) (n : Nat) (s : ArmState) : ArmState :=
+  match n with
+  | 0 => s
+  | n' + 1 =>
+    if (cond s) then
+      dbg_trace "Stopping condition reached!"
+      s
+    else
+      let s' := stepi s
+      run_until cond n' s'
+
+-- Examples of debug functions for use in `trace_run` and `log_run`:
+
+/-- `pc_trace`: Unconditionally trace the program counter. -/
+def pc_trace (s : ArmState) : String :=
+  "pc: " ++ (read_pc s).toHex
+
+/-- `non_zero_x2_trace`: Trace the program counter if x2 != 0#64. -/
+def non_zero_x2_trace (s : ArmState) : String :=
+  if (read_gpr 64 2 s) != 0#64 then
+    "pc: " ++ (read_pc s).toHex ++ ": x2 != 0"
+  else
+    ""
+
+end Debug
diff --git a/Tests/SHA512ProgramTest.lean b/Tests/SHA512ProgramTest.lean
index 32c28e64..027e929c 100644
--- a/Tests/SHA512ProgramTest.lean
+++ b/Tests/SHA512ProgramTest.lean
@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.Exec
 import Arm.Cfg.Cfg
 import Specs.SHA512
+import Tests.Debug
 
 section SHA512ProgramTest
 
@@ -596,6 +597,10 @@ def init_sha512_test : ArmState :=
   let s := write_mem_bytes (80 * 8) ktbl_address SHA512_K s
   s
 
+-- Log the PCs of all the instructions that were simulated in
+-- `Tests/SHA512_PC.log`.
+-- #eval (log_run "Tests/SHA512_PC.log" pc_trace 503 init_sha512_test)
+
 def final_sha512_state : ArmState := run 503 init_sha512_test
 def final_sha512_pc : BitVec 64 := final_sha512_state.pc