chore:simp_mem -> mem_omega

Arm/Memory/Separate.lean

@@ -230,12 +230,12 @@ theorem mem_legal'.omega_def (h : mem_legal' a n) : a.toNat + n ≤ 2^64 := h
 
 /-- The linear constraint is equivalent to `mem_legal'`. -/
 theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) :
-    (a.toNat + n ≤ 2^64) ↔ mem_legal' a n := by
+    mem_legal' a n ↔ (a.toNat + n ≤ 2^64)  := by
   constructor
-  · intros h
-    apply mem_legal'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_legal'.of_omega h
 
 instance : Decidable (mem_legal' a n) :=
   if h : a.toNat + n ≤ 2^64 then
@@ -341,14 +341,15 @@ theorem mem_separate'.of_omega
 
 /-- The linear constraint is equivalent to `mem_separate'`. -/
 theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_separate' a an b bn ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
-    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) ↔ mem_separate' a an b bn := by
+    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) := by
   constructor
-  · intros h
-    apply mem_separate'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_separate'.of_omega h
 
 instance : Decidable (mem_separate' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then
@@ -424,15 +425,16 @@ constructor
 
 /-- The linear constraint is equivalent to `mem_subset'`. -/
 theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_subset' a an b bn ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
     b.toNat ≤ a.toNat ∧
-    a.toNat + an ≤ b.toNat + bn) ↔ mem_subset' a an b bn := by
+    a.toNat + an ≤ b.toNat + bn) := by
   constructor
-  · intros h
-    apply mem_subset'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_subset'.of_omega h
 
 instance : Decidable (mem_subset' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then

Arm/Memory/SeparateAutomation.lean

@@ -433,38 +433,34 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : TacticM FVarId  := do
 attribute [bv_toNat] BitVec.le_def
 -- bv_omega' := (try simp only [bv_toNat, BitVec.le_def] at *) <;> omega)
 -- #check Lean.Elab.Tactic.Omega.omega
--- #check Lean.Elab.Tactic.Omega.bvOmega
+-- #check Lean.Elab.Tactic.Omega.
 -- simpTargetStar
 
 
+    -- let proof  := localDecl.toExpr
+
+    -- let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
+    -- ctx := { ctx with simpTheorems }
+
 /-- SimpMemM's omega invoker -/
 def omega : TacticM Unit := do
-  let g ← getMainGoal
+  let g ← match ← (← getMainGoal).falseOrByContra with
+    | none =>
+      trace[simp_mem] "omega converting goal to false/contra *closed* goal."
+      return ()
+    | some g' =>
+      pure g'
+  replaceMainGoal [g]
   let (simpCtx, simprocs) ← LNSymSimpContext
-      (config := {})
-      (simp_attrs := #[`bv_toNat]) (useDefaultSimprocs := false) (simprocs := #[])
-  let (result, stats) ← simpTargetStar g simpCtx simprocs
-  trace[simp_mem] "simp stats: {stats.usedTheorems.toArray.map Origin.key}"
-  if let .closed := result then
-    trace[simp_mem] "omega preprocessor *closed* goal."
-    replaceMainGoal []
-    return ()
-  else
-    let g :=
-      match result with
-      | .modified g' => g'
-      | .noChange | .closed => g
-    -- Step 2: prove goal with omega.
-    let g ←
-      match ← g.falseOrByContra with
-      | none =>
-        trace[simp_mem] "omega converting goal to false/contra *closed* goal."
-        return ()
-      | some g' =>
-        pure g'
-    trace[simp_mem] "omega goal: {g}"
-    replaceMainGoal [g]
-    g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
+      (config := { failIfUnchanged := false })
+      (simp_attrs := #[`bv_toNat])
+      (useDefaultSimprocs := false)
+      (thms := #[``mem_legal'.iff_omega, ``mem_separate'.iff_omega, ``mem_subset'.iff_omega, ``BitVec.le_def])
+      (simprocs := #[])
+  let _ ← simpLocation simpCtx simprocs (loc := Location.wildcard)
+  let g ← getMainGoal
+  trace[simp_mem] "omega goal: {g}"
+  g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
 
 section Hypotheses
 
@@ -1016,23 +1012,23 @@ partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
         if let .some proof ← proveWithOmega? e hyps then
           g.assign proof.h
-    else if (← getConfig).useOmegaToClose then
-      withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do
-        let oldGoals := (← getGoals)
-        try
-          let gproof ← mkFreshExprMVar (type? := gt)
-          setGoals (gproof.mvarId! :: (← getGoals))
-          SimpMemM.withMainContext do
-          let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
-          trace[simp_mem.info] m!"Executing `omega` to close {gt}"
-          SimpMemM.withTraceNode m!"goal (Note: can be large)" do
-            trace[simp_mem.info] "{← getMainGoal}"
-          omega
-          trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
-          g.assign gproof
-        catch e =>
-          trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
-          setGoals oldGoals
+    -- else if false && (← getConfig).useOmegaToClose then
+    --   withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do
+    --     let oldGoals := (← getGoals)
+    --     try
+    --       let gproof ← mkFreshExprMVar (type? := gt)
+    --       setGoals (gproof.mvarId! :: (← getGoals))
+    --       SimpMemM.withMainContext do
+    --       let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
+    --       trace[simp_mem.info] m!"Executing `omega` to close {gt}"
+    --       SimpMemM.withTraceNode m!"goal (Note: can be large)" do
+    --         trace[simp_mem.info] "{← getMainGoal}"
+    --       omega
+    --       trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
+    --       g.assign gproof
+    --     catch e =>
+    --       trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
+    --       setGoals oldGoals
   return ← g.isAssigned
 
 
@@ -1068,9 +1064,9 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
       for (i, h) in foundHyps.toList.enum do
         trace[simp_mem.info] m!"{i+1}) {h}"
 
-    if ← SimpMemM.closeGoal g foundHyps then
-      trace[simp_mem.info] "{checkEmoji} goal closed."
-      return ()
+    -- if ← SimpMemM.closeGoal g foundHyps then
+    --   trace[simp_mem.info] "{checkEmoji} goal closed."
+    --   return ()
 
     -- goal was not closed, try and improve.
     let mut changedInAnyIter? := false

Proofs/Experiments/Max/MaxTandem.lean

@@ -626,7 +626,7 @@ theorem partial_correctness :
       -- 2/15
       name h_s1_run : s2 := run 1 s1
       obtain ⟨h_s2_cut, h_s2_pc, h_s2_err, h_s2_program, h_s2_read_sp_8, h_s2_read_sp_12, h_s2_x0, h_s2_x1, h_s2_sp, h_s2_sp_aligned⟩ :=
-        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by simp_mem) h_s1_run.symm
+        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by mem_omega) h_s1_run.symm
       rw [Correctness.snd_cassert_of_not_cut h_s2_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s2 = run 1 s2 by rfl]
       replace h_s2_sp : s2.sp = (s0.sp - 32#64) := by simp_all
@@ -637,7 +637,7 @@ theorem partial_correctness :
 
       -- 3/15
       name h_run : s3 := run 1 s2
-      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by simp_mem) h_run.symm
+      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by mem_omega) h_run.symm
       obtain ⟨h_s3_cut, h_s3_read_sp_8, h_s3_read_sp_12, h_s3_x0, h_s3_x1, h_s3_sp, h_s3_pc, h_s3_err, h_s3_program, h_s3_sp_aligned⟩ := h
       rw [Correctness.snd_cassert_of_not_cut h_s3_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s3 = run 1 s3 by rfl]