From dd971b2faec8768166d1e96b178e0e746a1985ba Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Tue, 12 Nov 2024 17:51:41 -0600
Subject: [PATCH] Fix a bug in the application of mkNeProofOfNotMemAndMem

---
 Proofs/SHA512/SHA512.lean           |  2 +-
 Proofs/SHA512/SHA512BlockSym.lean   | 15 ++++++---------
 Proofs/SHA512/SHA512LoopBlocks.lean |  4 ++--
 Tactics/Sym/AxEffects.lean          |  2 +-
 Tests/Tactics/SymBlock.lean         |  3 ++-
 5 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/Proofs/SHA512/SHA512.lean b/Proofs/SHA512/SHA512.lean
index 202f9d24..699bc9b9 100644
--- a/Proofs/SHA512/SHA512.lean
+++ b/Proofs/SHA512/SHA512.lean
@@ -5,4 +5,4 @@ Author(s): Shilpi Goel
 -/
 import Proofs.SHA512.SHA512_block_armv8_rules
 import Proofs.SHA512.SHA512Sym
--- import Proofs.SHA512.SHA512BlockSym
+import Proofs.SHA512.SHA512BlockSym
diff --git a/Proofs/SHA512/SHA512BlockSym.lean b/Proofs/SHA512/SHA512BlockSym.lean
index f92347c5..70929983 100644
--- a/Proofs/SHA512/SHA512BlockSym.lean
+++ b/Proofs/SHA512/SHA512BlockSym.lean
@@ -11,11 +11,11 @@ import Tactics.ClearNamed
 open BitVec
 
 namespace SHA512
-#eval SHA2.k_512.length
 
 #time
-set_option trace.Tactic.sym.info true in
-set_option trace.Tactic.sym true in
+set_option linter.unusedVariables false in
+-- set_option trace.Tactic.sym.info true in
+-- set_option trace.Tactic.sym true in
 set_option pp.maxSteps 100 in
 theorem sha512_loop_sym {s0 sf : ArmState}
  { a b c d e f g h
@@ -92,14 +92,11 @@ theorem sha512_loop_sym {s0 sf : ArmState}
 
   (h_run : sf = run 485 s0) :
   r .ERR sf = .None
-  /-
-  More generally:
-  r .PC sf = (if ¬r (StateField.GPR 0x2#5) s0 - 0x1#64 = 0x0#64
+  -- More generally:
+  ∧ r .PC sf = (if ¬r (StateField.GPR 0x2#5) s0 - 0x1#64 = 0x0#64
               then 0x126500#64
               else 0x126c94#64)
-  -/
-  -- ∧ r .PC sf = 0x126c94#64
---   ∧ r (.SFP 1) sf = q1
+  -- ∧ r (.SFP 1) sf = q1
   -- ∧ (r (.SFP 3) sf ++ r (.SFP 2) sf ++ r (.SFP 1) sf ++ r (.SFP 0) sf) = final_hash
   := by
   -- Symbolic Simulation
diff --git a/Proofs/SHA512/SHA512LoopBlocks.lean b/Proofs/SHA512/SHA512LoopBlocks.lean
index 5d99da84..5044ec9e 100644
--- a/Proofs/SHA512/SHA512LoopBlocks.lean
+++ b/Proofs/SHA512/SHA512LoopBlocks.lean
@@ -38,6 +38,7 @@ namespace SHA512
   -- done
   -- sorry
 
+/-
 set_option trace.Tactic.prune_updates true in
 theorem program.blocki_eq_0x126500_1 {s : ArmState}
   (h_program : s.program = program)
@@ -76,8 +77,8 @@ theorem program.blocki_eq_0x126500_1 {s : ArmState}
   -- exact h_step_20
   -- done
   sorry
+-/
 
-/-
 -- #eval ((Cfg.create' (0x126500#64) (0x126500#64 + 20*4) SHA512.program).toOption.get!).maybe_modified_regs
 #time
 theorem program.blocki_eq_0x126500 {s : ArmState}
@@ -15666,4 +15667,3 @@ theorem program.blocki_eq_0x126c80 {s : ArmState}
   -- explode_step h_step_5 at s5
   exact h_step_5
   done
--/
diff --git a/Tactics/Sym/AxEffects.lean b/Tactics/Sym/AxEffects.lean
index e701ca41..fb1a6956 100644
--- a/Tactics/Sym/AxEffects.lean
+++ b/Tactics/Sym/AxEffects.lean
@@ -377,7 +377,7 @@ private def update_w (eff : AxEffects) (fld val : Expr) :
       -- `fld` was previously modified
 
       let neProof := -- : `<f> ≠ <fld>`
-        mkNeProofOfNotMemAndMem 0 (mkConst ``StateField) f fld modifiedFields h nonMemHyp
+        mkNeProofOfNotMemAndMem 0 (mkConst ``StateField) f fld modifiedFields nonMemHyp h
       -- Adjust the proof
       let proof ← newProofOfNe proof neProof
       -- And abstract `f` and `nonMemHyp` again, without changing their types
diff --git a/Tests/Tactics/SymBlock.lean b/Tests/Tactics/SymBlock.lean
index 7539062b..627cbb2b 100644
--- a/Tests/Tactics/SymBlock.lean
+++ b/Tests/Tactics/SymBlock.lean
@@ -57,6 +57,7 @@ theorem ugh_program.blocki_eq_0x12650c_alt {s : ArmState}
   -- simp (config := {decide := true})
   -- [h_step_3, h_step_2, h_step_1, state_simp_rules] at h_step_4
   sorry
+
 theorem ugh_program.blocki_eq_0x12651c {s : ArmState}
   (h_program : s.program = ugh_program)
   (h_pc : r StateField.PC s = 0x12651c#64)
@@ -78,7 +79,7 @@ theorem test_orig {s0 : ArmState}
   (h_err : r StateField.ERR s0 = StateError.None)
   (h_run : sf = run 8 s0) :
   sf.program = ugh_program := by
-  sym_n 8 (add_hyps := true)
+  sym_n 8
 
 
 #time