fix proofs with new representation

leanprover · Oct 7, 2024 · 072cea4 · 072cea4
1 parent 1702d61
commit 072cea4
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 26 deletions.
diff --git a/Arm/State.lean b/Arm/State.lean
@@ -1142,6 +1142,11 @@ by_cases h : ix < base
   · simp only [h₂, ↓reduceIte]
   · simp only [h₂, ↓reduceIte, BitVec.getLsbD_extractLsByte]
 
+@[memory_rules]
+theorem Memory.read_bytes_write_bytes (m : Memory) :
+    Memory.read_bytes n addr (m.write_bytes n addr val) = val := by
+  sorry
+
 end Memory
 
 

diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -57,37 +57,16 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   simp (config := {ground := true}) only at h_s0_pc
   -- ^^ Still needed, because `gcm_gmult_v8_program.min` is somehow
   --    unable to be reflected
+
   sym_n 27
   -- Epilogue
   simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
   simp only [memory_rules] at *
   sym_aggregate
+
+  -- stop
   -- Split conjunction
   repeat' apply And.intro
-  · -- Aggregate the memory (non)effects.
-    -- (FIXME) This will be tackled by `sym_aggregate` when `sym_n` and `simp_mem`
-    -- are merged.
-    simp only [*]
-    /-
-    (FIXME @bollu) `simp_mem; rfl` creates a malformed proof here. The tactic produces
-    no goals, but we get the following error message:
-
-    application type mismatch
-    Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
-      (Eq.mp (congrArg (Eq HTable) (Memory.State.read_mem_bytes_eq_mem_read_bytes s0))
-        (Eq.mp (congrArg (fun x => HTable = read_mem_bytes 256 x s0) zeroExtend_eq_of_r_gpr) h_HTable))
-    argument has type
-      HTable = Memory.read_bytes 256 (r (StateField.GPR 1#5) s0) s0.mem
-    but function has type
-      Memory.read_bytes 256 (r (StateField.GPR 1#5) s0) s0.mem = HTable →
-      mem_subset' (r (StateField.GPR 1#5) s0) 256 (r (StateField.GPR 1#5) s0) 256 →
-        Memory.read_bytes 256 (r (StateField.GPR 1#5) s0) s0.mem =
-          HTable.extractLsBytes (BitVec.toNat (r (StateField.GPR 1#5) s0) - BitVec.toNat (r (StateField.GPR 1#5) s0)) 256
-
-    simp_mem; rfl
-    -/
-    rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
-    simp_mem
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
     sym_aggregate
   · intro n addr h_separate

diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
@@ -70,7 +70,7 @@ def popcount32_program : Program :=
 
 #genStepEqTheorems popcount32_program
 
-set_option trace.simp_mem.info true in
+-- set_option trace.simp_mem.info true in
 theorem popcount32_sym_meets_spec (s0 sf : ArmState)
   (h_s0_pc         : read_pc s0 = 0x4005b4#64)
   (h_s0_program    : s0.program = popcount32_program)

diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
@@ -153,7 +153,6 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   -- Only memory-related obligations are left.
   -- (TODO @alex/@bollu) Remove ∀ in memory (non)effect hyps generated by
   -- `sym_n`. The user may still state memory properties using quantifiers.
-  simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
   -- Rewrite *_mem_bytes (in terms of ArmState) to *_bytes (in terms of Memory).
   simp only [memory_rules] at *
   -- (FIXME) Need to aggregate memory effects here automatically.