Merge branch 'main' into memory-effects-struct

Arm/Memory/SeparateAutomation.lean

@@ -88,9 +88,12 @@ The tactic shall be implemented as follows:
 
 section BvOmega
 
--- |TODO: Upstream BitVec.le_def unfolding to bv_omega.
-macro "bv_omega'" : tactic =>
-  `(tactic| (try simp only [bv_toNat, mem_legal'] at * <;> try rw [BitVec.le_def]) <;> bv_omega)
+/- We tag `mem_legal'` as `bv_toNat` here, since we want to actually lazily unfold this.
+Doing it here lets us remove it from `bv_toNat` simp-set as a change to `SeparateAutomation.lean`,
+without needing us to modify the core definitions file which incurs a recompile cost,
+making experimentation annoying.
+-/
+attribute [bv_toNat] mem_legal'
 
 end BvOmega
 
@@ -112,7 +115,7 @@ structure SimpMemConfig where
     ⊢ a + 5 < b
     ```
   -/
-  useOmegaToClose : Bool := true
+  useOmegaToClose : Bool := false
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -427,7 +430,7 @@ def omega : SimpMemM Unit := do
   -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
   -- @bollu: TODO: understand what precisely we are recovering from.
   withoutRecover do
-    evalTactic (← `(tactic| bv_omega'))
+    evalTactic (← `(tactic| bv_omega))
 
 section Hypotheses
 

Benchmarks/Command.lean

@@ -13,16 +13,20 @@ elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do
   let n := 5
   let mut runTimes := #[]
   let mut totalRunTime := 0
+  -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) = 
+  -- exp(1/n * (log a₁ + log a₂ + log aₙ)).
+  let mut totalRunTimeLog := 0
   for _ in [0:n] do
     let start ← IO.monoMsNow
     elabCommand stx
     let endTime ← IO.monoMsNow
     let runTime := endTime - start
     runTimes := runTimes.push runTime
     totalRunTime := totalRunTime + runTime
+    totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat
 
   let avg := totalRunTime.toFloat / n.toFloat / 1000
-  let geomean := (totalRunTime.toFloat.pow (1.0 / n.toFloat)) / 1000.0
+  let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0
   logInfo m!"\
 {id}:
   average runtime over {n} runs:

Proofs/Experiments/Memcpy/MemCpyVCG.lean

@@ -469,7 +469,7 @@ 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 simp_mem (config := {useOmegaToClose := true})
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
     skip_proof simp_mem

Proofs/Experiments/MemoryAliasing.lean

@@ -47,7 +47,7 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
 
 /-- 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
+  simp_mem (config := {useOmegaToClose := true})
 
 /-- Show that we can perform address arithmetic based on subset constraints.
 Only two configurations possible:
@@ -59,7 +59,7 @@ a0 a1 a2 ..
 b0 b1 b2 b3
 -/
 theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
-  simp_mem
+  simp_mem (config := {useOmegaToClose := true})
 
 end MemSubset
 
@@ -134,7 +134,8 @@ 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
+  (hab : a < b) : a + 50 ≤ b := by
+  simp_mem (config := {useOmegaToClose := true})
 
 end MemSeparate
 
@@ -199,7 +200,7 @@ theorem mem_automation_test_4
   simp only [memory_rules]
   simp_mem
   congr 1
-  bv_omega' -- TODO: address normalization.
+  bv_omega -- TODO: address normalization.
 
 /-- info: 'mem_automation_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_4
@@ -214,8 +215,9 @@ 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, BitVec.cast_eq]
 
-/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Quot.sound] -/
+/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms overlapping_read_test_1
 
 /-- A read overlapping with another read. -/
@@ -227,7 +229,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    bv_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_2' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -246,13 +248,13 @@ theorem overlapping_read_test_3
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    bv_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_3' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs in #print axioms overlapping_read_test_3
 
-/- TODO(@bollu): This test case hangs at `bv_omega'`. This is to be debugged.
+/- TODO(@bollu): This test case hangs at `bv_omega`. This is to be debugged.
 /-- A read in the goal state overlaps with a read in the
 right hand side of the hypotheis `h`.
 -/
@@ -266,7 +268,7 @@ theorem overlapping_read_test_4
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega' -- TODO: Lean gets stuck here?
+    bv_omega -- TODO: Lean gets stuck here?
 
 #guard_msgs in #print axioms overlapping_read_test_4
 -/
@@ -288,7 +290,7 @@ theorem test_2 {val : BitVec _}
     Memory.read_bytes 6 (src_addr + 10) (Memory.write_bytes 16 src_addr val mem) =
     val.extractLsBytes 10 6 := by
   simp_mem
-  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega'
+  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega
   rw [this]
 
 /--
@@ -427,14 +429,6 @@ 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.
@@ -453,14 +447,6 @@ 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.

Proofs/Experiments/SHA512MemoryAliasing.lean

@@ -97,7 +97,7 @@ theorem sha512_block_armv8_prelude_sym_ctx_access (s0 : ArmState)
   -- @shilpi: should this also be proven automatically? feels a little unreasonable to me.
   · congr
     -- ⊢ (ctx_addr s0 + 48#64).toNat - (ctx_addr s0).toNat = 48
-    bv_omega'
+    bv_omega
 
 /--
 info: 'SHA512MemoryAliasing.sha512_block_armv8_prelude_sym_ctx_access' depends on axioms: [propext,

Tactics/Reflect/AxEffects.lean

@@ -371,19 +371,12 @@ return an `AxEffects` where `s` is the intial state, and `e` is `currentState`.
 Note that as soon as an unsupported expression (e.g., an `if`) is encountered,
 the whole expression is taken to be the initial state,
 even if there might be more `w`/`write_mem`s in sub-expressions. -/
-partial def fromExpr (e : Expr) : MetaM AxEffects := do
-  let msg := m!"Building effects with writes from: {e}"
-  withTraceNode `Tactic.sym (fun _ => pure msg) <| do match_expr e with
-    | write_mem_bytes n addr val e =>
-        let eff ← fromExpr e
-        eff.update_write_mem n addr val
+def fromExpr (e : Expr) : MetaM AxEffects := do
+  let s0 ← mkFreshExprMVar mkArmState
+  let eff := initial s0
+  let eff ← eff.updateWithExpr e
+  return { eff with initialState := ← instantiateMVars eff.initialState}
 
-    | w field value e =>
-        let eff ← fromExpr e
-        eff.update_w field value
-
-    | _ =>
-        return initial e
 
 /-- Given a proof `eq : s = <currentState>`,
 set `s` to be the new `currentState`, and update all proofs accordingly -/
@@ -413,25 +406,34 @@ def adjustCurrentStateWithEq (eff : AxEffects) (s eq : Expr) :
       currentState, fields, nonEffectProof, memoryEffects, programProof
     }
 
-/-- Given a proof `eq : ?s = <sequence of w/write_mem to ?s0>`,
+/-- Given a proof `eq : ?s = <sequence of w/write_mem to eff.currentState>`,
 where `?s` and `?s0` are arbitrary `ArmState`s,
-return an `AxEffect` with `?s0` as the initial state,
-the rhs of the equality as the current state, and
-`eq` stored as `currentStateEq`,
-so that `?s` is the public-facing current state -/
-def fromEq (eq : Expr) : MetaM AxEffects :=
+return an `AxEffect` with the rhs of the equality as the current state,
+and the (non-)effects updated accordingly -/
+def updateWithEq (eff : AxEffects) (eq : Expr) : MetaM AxEffects :=
   let msg := m!"Building effects with equality: {eq}"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do
     let s ← mkFreshExprMVar mkArmState
     let rhs ← mkFreshExprMVar mkArmState
     assertHasType eq <| mkEqArmState s rhs
 
-    let eff ← fromExpr (← instantiateMVars rhs)
+    let eff ← eff.updateWithExpr (← instantiateMVars rhs)
     let eff ← eff.adjustCurrentStateWithEq s eq
     withTraceNode `Tactic.sym (fun _ => pure "new state") do
       trace[Tactic.sym] "{eff}"
     return eff
 
+/-- Given a proof `eq : ?s = <sequence of w/write_mem to ?s0>`,
+where `?s` and `?s0` are arbitrary `ArmState`s,
+return an `AxEffect` with `?s0` as the initial state,
+the rhs of the equality as the current state,
+and the (non-)effects updated accordingly -/
+def fromEq (eq : Expr) : MetaM AxEffects := do
+  let s0 ← mkFreshExprMVar mkArmState
+  let eff := initial s0
+  let eff ← eff.updateWithEq eq
+  return { eff with initialState := ← instantiateMVars eff.initialState}
+
 /-- Given an equality `eq : ?currentProgram = ?newProgram`,
 where `currentProgram` is the rhs of `eff.programProof`,
 apply transitivity to make `newProgram` the rhs of `programProof`

Tactics/SymContext.lean

@@ -247,7 +247,7 @@ Falling back to the default numbering scheme, \
 with `s1` as the first new intermediate state"
     modifyThe SymContext ({ · with
       state_prefix := "s",
-      currentStateNumber := 1 })
+      currentStateNumber := 0 })
 
 /-- Annotate any errors thrown by `k` with a local variable (and its type) -/
 private def withErrorContext (name : Name) (type? : Option Expr) (k : MetaM α) :