gotta debug why we are unable to run properly

leanprover · Sep 24, 2024 · e737213 · e737213
1 parent 6fcdc24
commit e737213
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 17 deletions.
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
@@ -459,7 +459,8 @@ def omega : TacticM Unit := do
       (simprocs := #[])
   let _ ← simpLocation simpCtx simprocs (loc := Location.wildcard)
   let g ← getMainGoal
-  trace[simp_mem] "omega goal: {g}"
+  TacticM.withTraceNode m!"omega goal (Note: can be large)" do
+    trace[simp_mem] "{g}"
   g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
 
 section Hypotheses
@@ -926,18 +927,23 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMem
       trace[simp_mem.info] "{processingEmoji} read({er.span})⟂/⊆write({ew.span})"
 
       let separate := MemSeparateProp.mk er.span ew.span
-      let subset := MemSubsetProp.mk er.span ew.span
+      trace[simp_mem.info] "{processingEmoji} {separate}"
       if let .some separateProof ← proveWithOmega? separate hyps then do
         trace[simp_mem.info] "{checkEmoji} {separate}"
         rewriteReadOfSeparatedWrite er ew separateProof
         return true
-      else if let .some subsetProof ← proveWithOmega? subset hyps then do
-        trace[simp_mem.info] "{checkEmoji} {subset}"
-        rewriteReadOfSubsetWrite er ew subsetProof
-        return true
-      else
-        trace[simp_mem.info] "{crossEmoji} Could not prove {er.span} ⟂/⊆ {ew.span}"
-        return false
+      else do
+        trace[simp_mem.info] "{crossEmoji} {separate}"
+        let subset := MemSubsetProp.mk er.span ew.span
+        trace[simp_mem.info] "{processingEmoji} {subset}"
+        if let .some subsetProof ← proveWithOmega? subset hyps then do
+          trace[simp_mem.info] "{checkEmoji} {subset}"
+          rewriteReadOfSubsetWrite er ew subsetProof
+          return true
+        else
+          trace[simp_mem.info] "{crossEmoji} {subset}"
+          trace[simp_mem.info] "{crossEmoji} Could not prove {er.span} ⟂/⊆ {ew.span}"
+          return false
     else
       -- read
       trace[simp_mem.info] "{checkEmoji} Found read {er}."

diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -20,6 +20,9 @@ import Arm.Memory.SeparateAutomation
 import Arm.Syntax
 import Tactics.SkipProof
 
+/- The linters take quite a long time. -/
+set_option linter.all false
+
 namespace Memcpy
 
 /-
@@ -505,10 +508,10 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
   have h_upper_bound := hsep.hb.omega_def
   have h_upper_bound₂ := h_pre_1.hb.omega_def
   have h_upper_bound₃ := hsep.ha.omega_def
-  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by mem_omega
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
-    skip_proof simp_mem
+    skip_proof mem_omega -- slow.
   · -- @bollu: TODO: figure out why this is so slow!
     apply mem_separate'.symm
     apply mem_separate'.of_subset'_of_subset' hsep
@@ -551,9 +554,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
   apply And.intro
   · intros i hi
     have h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16) := by
-      skip_proof simp_mem
+      skip_proof omega_mem
     have h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16) := by
-      skip_proof simp_mem
+      skip_proof omega_mem
     have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega
     have s2_sum_inbounds := h_pre_1.hb.omega_def
     have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega
@@ -564,13 +567,13 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
       · simp only [Nat.reduceMul, BitVec.toNat_add, BitVec.toNat_mul, BitVec.toNat_ofNat,
         Nat.reducePow, Nat.reduceMod, BitVec.toNat_sub, Nat.add_mod_mod, Nat.sub_self,
         BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
-        rw [h_assert_6 _ _ (by simp_mem)]
-      · skip_proof simp_mem
+        rw [h_assert_6 _ _ (by omega_mem)]
+      · skip_proof omega_mem
     · rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
       · apply h_assert_5 _ hi
       · constructor
-        · skip_proof simp_mem
-        · skip_proof simp_mem
+        · skip_proof omega_mem
+        · skip_proof omega_mem
         · left
           -- @bollu: TODO, see if `simp_mem` can figure this out given less aggressive
           -- proof states.