bugfixes in pairing with @shilgoel, @alexkeizer

leanprover · Oct 1, 2024 · 1a996fc · 1a996fc
1 parent 057237e
commit 1a996fc
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 30 deletions.
diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
@@ -331,8 +331,7 @@ abbrev Nat.bv64 (n : Nat) : BitVec 64 := BitVec.ofNat 64 n
 macro_rules
 | `(tactic| mem_unfold_bv) =>
     `(tactic| simp (config := {failIfUnchanged := false}) only
-      [memory_defs_bv, bitvec_rules, minimal_theory, BitVec.ofNat_toNat] at *)
-
+      [memory_defs_bv, state_value, bitvec_rules, minimal_theory, BitVec.ofNat_toNat] at *)
 
 macro_rules
 | `(tactic| mem_decide_bv) =>

diff --git a/Arm/Memory/SeparateProofs.lean b/Arm/Memory/SeparateProofs.lean
@@ -72,7 +72,6 @@ theorem addr_add_one_add_m_sub_one  (n : Nat) (addr : BitVec 64)
 
 ----------------------------------------------------------------------
 ---- mem_subset ----
-
 theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
   simp [mem_subset]
   bv_check "lrat_files/SeparateProofs.lean-mem_subset_refl-77-2.lrat"

diff --git a/Arm/State.lean b/Arm/State.lean
@@ -313,7 +313,7 @@ attribute [state_simp_rules] StateField.GPR.injEq
 attribute [state_simp_rules] StateField.SFP.injEq
 attribute [state_simp_rules] StateField.FLAG.injEq
 
-@[reducible]
+@[reducible, state_simp_rules]
 def state_value (fld : StateField) : Type :=
   open StateField in
   match fld with

diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -515,13 +515,24 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
       (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0))
         (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) =
     Memory.read_bytes n addr s0.mem := by
-  simp [memory_defs_bv] at h_non_overflowing
+  rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
+  · sorry
+    -- rw [h_assert_6]
+    -- skip_proof simp_mem
+  · -- @bollu: TODO: figure out why this is so slow!
+    sorry
+    -- apply mem_separate'.symm
+    -- apply mem_separate'.of_subset'_of_subset' hsep
+    -- · apply mem_subset'.of_omega
+    --   skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega
+    -- · apply mem_subset'_refl hsep.hb
+
+  -- simp [memory_defs_bv] at h_non_overflowing
   -- mem_decide_bv
   -- simp_mem_debug
-  rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' (by sorry)]
-  · apply h_assert_6 _ _ (by sorry)
+  -- rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' (by sorry)]
+  -- · apply h_assert_6 _ _ (by sorry)
 
-#print axioms Memcpy.extracted_2
 
 -- set_option trace.Meta.Tactic.bv true in
 -- -- set_option skip_proof.skip true in

diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
@@ -117,28 +117,7 @@ theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
       bv_decide
     generalize hx : (r (StateField.GPR 31#5) s0) = x
     simp only [hx] at *
-    simp_mem
-  /-
-    [] ❌️ mem_decide_bv with error:
-    The prover found a potential counterexample, consider the following assignment:
-    r StateField.PC s0 = 0x00000000004005b4#64
-    n = 0x8000000000000000#64
-    r (StateField.GPR 31#5) s0 = 0x8000000000000000#64
-    addr = 0x0000000000000000#64
-    r (StateField.GPR 31#5) s0 - 16#64 = 0x8000000000000000#64
-  -/
-    rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' (by
-      exact this)]
-      -- mem_unfold_bv;
-      -- mem_decide_bv)]
-    -- simp_mem
-    sym_aggregate
-    rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' (by
-      exact this)]
-    sym_aggregate
-    rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' (by
-      exact this)]
-
+    repeat (simp_mem; sym_aggregate)
     repeat (simp_mem (config := { useOmegaToClose := false }); sym_aggregate)
   · apply Aligned_BitVecSub_64_4 -- TODO(@bollu): automation
     · assumption

diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
@@ -266,6 +266,7 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
       · -- (FIXME @bollu) simp_mem doesn't make progress here. :-(
         -- simp only [←h_s0_sp] at h_s0_mem_sep
         -- simp_mem
+
         rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
         -- (FIXME @bollu) Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
         -- works here, but using it is painful. Also, mispelled lemma.