feat: increase simp_mem power by trying to close goals with omega [6/…

…? memcpy] (leanprover#169)

This lets us close goals where the hypotheses are about memory, and the
goal is an LIA goal. For example:

```
h : mem_separate' a 10 b 10
hab : a < b
-----------
a + 5 < b
```

---------

Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Arm/Memory/SeparateAutomation.lean

@@ -101,6 +101,18 @@ structure SimpMemConfig where
   rewriteFuel : Nat := 1000
   /-- whether an error should be thrown if the tactic makes no progress. -/
   failIfUnchanged : Bool := true
+  /-- whether `simp_mem` should always try to use `omega` to close the goal,
+    even if goal state is not recognized as one of the blessed states.
+    This is useful when one is trying to establish some numerical invariant
+    about addresses based on knowledge of memory.
+    e.g.
+    ```
+    h : mem_separate' a 10 b 10
+    hab : a < b
+    ⊢ a + 5 < b
+    ```
+  -/
+  useOmegaToClose : Bool := true
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -396,7 +408,7 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
 
     -- unfold `state_value.
     simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
-    let simpCtx : Simp.Context := { 
+    let simpCtx : Simp.Context := {
       simpTheorems,
       config := { decide := true, failIfUnchanged := false },
       congrTheorems := (← Meta.getSimpCongrTheorems)
@@ -702,7 +714,6 @@ For example, `mem_legal.of_omega` is a function of type:
 class OmegaReducible (α : Type) where
   reduceToOmega : α → Expr
 
-
 /--
 info: mem_legal'.of_omega {n : Nat} {a : BitVec 64} (h : a.toNat + n ≤ 2 ^ 64) : mem_legal' a n
 -/
@@ -962,12 +973,30 @@ partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM
           g.assign proof.h
     if let .some e := MemSubsetProp.ofExpr? gt then
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ←  proveWithOmega? e hyps then
+        if let .some proof ← proveWithOmega? e hyps then
           g.assign proof.h
     if let .some e := MemSeparateProp.ofExpr? gt then
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ←  proveWithOmega? e hyps then
+        if let .some proof ← proveWithOmega? e hyps then
           g.assign proof.h
+
+    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
   return ← g.isAssigned
 
 

Proofs/Experiments/MemoryAliasing.lean

@@ -45,6 +45,22 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
 /-- info: 'MemSubset.subset_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_3
 
+/-- Show that we can perform address arithmetic based on subset constraints. -/
+theorem subset_4 (l : mem_subset' a 16 b 16) : a = b := by
+  simp_mem
+
+/-- Show that we can perform address arithmetic based on subset constraints.
+Only two configurations possible:
+
+..  a0 a1 a2
+b0 b1 b2 b3
+
+a0 a1 a2 ..
+b0 b1 b2 b3
+-/
+theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
+  simp_mem
+
 end MemSubset
 
 namespace MemSeparate
@@ -71,7 +87,6 @@ theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by
 /-- info: 'MemSeparate.separate_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_3
 
-
 /-- sliding subset to the right. -/
 theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) :
     mem_separate' a 17 (b+1) 15 := by
@@ -114,6 +129,13 @@ theorem separate_6 {n : Nat} (hn : n ≠ 0)
   simp_mem /- Need better address normalization. -/
   trace_state
 
+/--
+Check that we can close address relationship goals that require
+us to exploit memory separateness properties.
+-/
+theorem mem_separate_9  (h : mem_separate' a 100 b 100)
+  (hab : a < b) : a + 50 ≤ b := by simp_mem
+
 end MemSeparate
 
 
@@ -192,11 +214,8 @@ theorem overlapping_read_test_1 {out : BitVec (16 * 8)}
     read_mem_bytes 16 src_addr s = out := by
   simp only [memory_rules] at h ⊢
   simp_mem
-  simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self]
 
-/--
-info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound]
--/
+/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Quot.sound] -/
 #guard_msgs in #print axioms overlapping_read_test_1
 
 /-- A read overlapping with another read. -/
@@ -408,6 +427,14 @@ error: unsolved goals
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
 [simp_mem.info] ⚙️ Matching on ⊢ False
+[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
+  [simp_mem.info] Adding omega facts from hypotheses
+  [simp_mem.info] Executing `omega` to close False
+  [simp_mem.info] goal (Note: can be large)
+    [simp_mem.info] ⊢ False
+  [simp_mem.info] ❌️ `omega` failed with error:
+      omega could not prove the goal:
+      No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.
@@ -426,6 +453,14 @@ error: ❌️ simp_mem failed to make any progress.
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
 [simp_mem.info] ⚙️ Matching on ⊢ False
+[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
+  [simp_mem.info] Adding omega facts from hypotheses
+  [simp_mem.info] Executing `omega` to close False
+  [simp_mem.info] goal (Note: can be large)
+    [simp_mem.info] ⊢ False
+  [simp_mem.info] ❌️ `omega` failed with error:
+      omega could not prove the goal:
+      No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.