chore: get big wins on perf

Arm/Memory/MemOmega.lean

@@ -110,37 +110,9 @@ def mkGoalWithOnlyUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : M
       let mut g := g
       for h in hyps do
         if !keepHyps.contains h then
-          g ← g.clear h
+          g ← g.withContext <| g.clear h
       return g
 
-def memOmega' (g : MVarId) : MemOmegaM Unit := do
-  g.withContext do
-    /- We need to explode all pairwise separate hyps -/
-    let rawHyps ← getLocalHyps
-    let mut hyps := #[]
-    -- extract out structed values for all hyps.
-    for h in rawHyps do
-      hyps ← hypothesisOfExpr h hyps
-
-    -- only enable pairwise constraints if it is enabled.
-    let isPairwiseEnabled := (← readThe Context).cfg.explodePairwiseSeparate
-    hyps := hyps.filter (!·.isPairwiseSeparate || isPairwiseEnabled)
-
-    -- used specialized procedure that doesn't unfold everything for the easy case.
-    if ← closeMemSideCondition g (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then
-      return ()
-    else
-      -- in the bad case, just rip through everything.
-      let (_, g) ← Hypothesis.addOmegaFactsOfHyps g hyps.toList #[]
-
-      TacticM.withTraceNode' m!"Reducion to omega" do
-        try
-          TacticM.traceLargeMsg m!"goal (Note: can be large)"  m!"{g}"
-          omega g (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs
-          trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
-        catch e =>
-          trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
-
 def memOmega (g : MVarId) : MemOmegaM Unit := do
     let g ← mkGoalWithOnlyUserHyps g (← readThe Context).userHyps? 
     g.withContext do
@@ -168,6 +140,7 @@ def memOmega (g : MVarId) : MemOmegaM Unit := do
             trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
           catch e =>
             trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
+            throw e
 
 -- syntax memOmegaRule := term
 

Proofs/Experiments/Memcpy/MemCpyVCG.lean

@@ -440,7 +440,7 @@ section PartialCorrectness
 -- set_option skip_proof.skip true in
 -- set_option trace.profiler true in
 -- set_option profiler true in
-set_option maxHeartbeats 0 in
+#time set_option maxHeartbeats 0 in
 theorem Memcpy.extracted_2 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -464,19 +464,20 @@ 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
-  have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by bv_omega_bench
-  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 mem_omega
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by 
+    mem_omega with [h_assert_1, h_pre_1]
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
-    skip_proof mem_omega
+    skip_proof mem_omega with [h_assert_1, h_pre_1, hsep]
   · -- @bollu: TODO: figure out why this is so slow!/
     apply mem_separate'.symm
     apply mem_separate'.of_subset'_of_subset' hsep
     · apply mem_subset'.of_omega
-      skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega_bench
+      skip_proof refine ⟨?_, ?_, ?_, ?_⟩
+      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1] -- TODO: add support for patterns like *, -<hyp1>, ... -<hypN>
+      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1]
+      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1]
+      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1] -- , hsep] -- adding `hsep` makes this way slower.
     · apply mem_subset'_refl hsep.hb
 
 -- set_option skip_proof.skip true in