Fix a bug in the application of mkNeProofOfNotMemAndMem

leanprover · Nov 12, 2024 · dd971b2 · dd971b2
1 parent c59a393
commit dd971b2
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 14 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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