feat: add bv_omega_bench to run omega and produce goal states + timing inf.

Arm/Memory/MemoryProofs.lean

@@ -7,7 +7,7 @@ import Arm.FromMathlib
 import Arm.State
 import Arm.Memory.Separate
 import Arm.Memory.SeparateProofs
-
+import Tactics.BvOmegaBench
 -- In this file, we have memory (non-)interference proofs.
 
 ----------------------------------------------------------------------
@@ -321,7 +321,7 @@ private theorem mem_subset_neq_first_addr_small_second_region
       omega
     simp only [l1, Nat.lt_irrefl] at h1
   · rename_i h
-    bv_omega
+    bv_omega_bench
     done
 
 private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt
@@ -756,7 +756,7 @@ private theorem mem_legal_lemma (h0 : 0 < n) (h1 : n < 2^64)
   revert h0 h1 h2
   have : 2^64 = 18446744073709551616 := by decide
   simp_all [mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem addr_diff_upper_bound_lemma (h0 : 0 < n1) (h1 : n1 ≤ 2 ^ 64)
   (h2 : 0 < n2) (h3 : n2 < 2^64)
@@ -768,7 +768,7 @@ private theorem addr_diff_upper_bound_lemma (h0 : 0 < n1) (h1 : n1 ≤ 2 ^ 64)
   have _ : 2^64 = 18446744073709551616 := by decide
   have _ : 2^64 - 1 = 18446744073709551615 := by decide
   simp_all [mem_subset, mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_lt
   (h0 : 0 < n1) (h1 : n1 <= 2^64) (h2 : 0 < n2) (h3 : n2 < 2^64)
@@ -850,7 +850,7 @@ theorem entire_memory_subset_of_only_itself
   have : 2^64 = 18446744073709551616 := by decide
   unfold my_pow at *
   simp_all [mem_subset, BitVec.add_sub_self_left_64]
-  bv_omega
+  bv_omega_bench
 
 theorem entire_memory_subset_legal_regions_eq_addr
   (h1 : mem_subset addr2 (addr2 + (BitVec.ofNat 64 (my_pow 2 64 - 1))) addr1 (addr1 + (BitVec.ofNat 64 (my_pow 2 64 - 1))))
@@ -860,7 +860,7 @@ theorem entire_memory_subset_legal_regions_eq_addr
   have : 2^64-1 = 18446744073709551615 := by decide
   unfold my_pow at *
   simp_all [mem_subset, mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
   (h0 : 0 < n1) (h1 : n1 <= my_pow 2 64) (h2 : 0 < n2) (h3 : n2 = my_pow 2 64)

Arm/Memory/Separate.lean

@@ -5,7 +5,7 @@ Author(s): Shilpi Goel, Siddharth Bhat
 -/
 import Arm.State
 import Arm.BitVec
-
+import Tactics.BvOmegaBench
 section Separate
 
 open BitVec
@@ -137,7 +137,7 @@ theorem lt_or_gt_of_mem_separate_of_mem_legal_of_mem_legal (h : mem_separate a1
   · by_cases h₆ : a1.toNat > b2.toNat
     · simp only  [BitVec.val_bitvec_lt, gt_iff_lt, h₆, or_true]
     · exfalso
-      bv_omega
+      bv_omega_bench
 
 /--
 Given two legal memory regions `[a1, a2]` and `[b1, b2]`,
@@ -153,7 +153,7 @@ theorem mem_separate_of_lt_or_gt_of_mem_legal_of_mem_legal (h : a2 < b1 ∨ a1 >
   unfold mem_legal at ha hb
   simp only [decide_eq_true_eq] at ha hb
   rw [BitVec.le_def] at ha hb
-  bv_omega
+  bv_omega_bench
 
 /--
 Given two legal memory regions `[a1, a2]` and `[b1, b2]`,
@@ -183,7 +183,7 @@ theorem add_lt_of_mem_legal_of_lt
   by_cases hadd : a.toNat + n.toNat < 2^64
   · assumption
   · exfalso
-    bv_omega
+    bv_omega_bench
 
 /--
 If we express a memory region as `[a..(a+n)]` for `(n : Nat)`,
@@ -274,7 +274,7 @@ theorem mem_legal_of_mem_legal' (h : mem_legal' a n) :
   simp only [mem_legal', mem_legal, BitVec.le_def] at h ⊢
   rw [BitVec.toNat_add_eq_toNat_add_toNat]
   simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.le_add_right, decide_True]
-  bv_omega
+  bv_omega_bench
 
 /--
 Legal in the new sense implies legal in the old sense.
@@ -283,7 +283,7 @@ Note that the subtraction could also have been written as `(b - a).toNat + 1`
 theorem mem_legal'_of_mem_legal (h: mem_legal a b) : mem_legal' a (b.toNat - a.toNat + 1) := by
   simp only [mem_legal, decide_eq_true_eq] at h
   rw [mem_legal']
-  bv_omega
+  bv_omega_bench
 
 def mem_legal'_of_mem_legal'_of_lt (h : mem_legal' a n) (m : Nat) (hm : m ≤ n) :
     mem_legal' a m := by
@@ -304,7 +304,7 @@ theorem mem_legal_iff_mem_legal' : mem_legal a b ↔
   · intros h
     simp only [mem_legal'] at h
     simp only [mem_legal, BitVec.le_def, decide_eq_true_eq]
-    bv_omega
+    bv_omega_bench
 
 /--
 `mem_separate' a an b bn` asserts that two memory regions [a..an) and [b..bn) are separate.
@@ -449,7 +449,7 @@ theorem mem_subset'_refl (h : mem_legal' a an) : mem_subset' a an a an where
 theorem mem_separate'.symm (h : mem_separate' addr₁ n₁ addr₂ n₂) : mem_separate' addr₂ n₂ addr₁ n₁ := by
   have := h.omega_def
   apply mem_separate'.of_omega
-  bv_omega
+  bv_omega_bench
 
 theorem mem_separate'.of_subset'_of_subset'
   (h : mem_separate' addr₁ n₁ addr₂ n₂)
@@ -460,7 +460,7 @@ theorem mem_separate'.of_subset'_of_subset'
   have := h₁.omega_def
   have := h₂.omega_def
   apply mem_separate'.of_omega
-  bv_omega
+  bv_omega_bench
 
 /--
 If `[a'..a'+an')` begins at least where `[a..an)` begins,
@@ -522,8 +522,8 @@ theorem mem_subset_of_mem_subset' (h : mem_subset' a an b bn) (han : an > 0) (hb
   simp only [bitvec_rules, minimal_theory]
   by_cases hb : bn = 2^64
   · left
-    bv_omega
-  · bv_omega
+    bv_omega_bench
+  · bv_omega_bench
 
 /- value of read_mem_bytes when separate from the write. -/
 theorem Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'
@@ -541,7 +541,7 @@ theorem Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'
   simp only [decide_True, ite_eq_left_iff, Bool.true_and]
   intros h₁
   intros h₂
-  bv_omega
+  bv_omega_bench
 
 /- value of `read_mem_bytes'` when subset of the write. -/
 theorem Memory.read_bytes_write_bytes_eq_of_mem_subset'
@@ -619,17 +619,17 @@ theorem Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
     have ⟨h1, h2, h3, h4⟩ := hsubset.omega_def
     apply BitVec.eq_of_extractLsByte_eq
     intros i
-    rw [extractLsByte_read_bytes (by bv_omega)]
+    rw [extractLsByte_read_bytes (by bv_omega_bench)]
     rw [BitVec.extractLsByte_extractLsBytes]
     by_cases h : i < an
     · simp only [h, ↓reduceIte]
       apply BitVec.eq_of_getLsbD_eq
       intros j
       rw [← hread]
-      rw [extractLsByte_read_bytes (by bv_omega)]
-      simp only [show a.toNat - b.toNat + i < bn by bv_omega, if_true]
+      rw [extractLsByte_read_bytes (by bv_omega_bench)]
+      simp only [show a.toNat - b.toNat + i < bn by bv_omega_bench, if_true]
       congr 2
-      bv_omega
+      bv_omega_bench
     · simp only [h, ↓reduceIte]
 
 /-- A region of memory, given by (base pointer, length) -/

Arm/Memory/SeparateAutomation.lean

@@ -20,10 +20,10 @@ import Lean.Meta.Tactic.Rewrites
 import Lean.Elab.Tactic.Conv
 import Lean.Elab.Tactic.Conv.Basic
 import Tactics.Simp
+import Tactics.BvOmegaBench
 
 open Lean Meta Elab Tactic
 
-
 /-! ## Memory Separation Automation
 
 ##### A Note on Notation
@@ -431,7 +431,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_bench))
 
 section Hypotheses
 

Arm/Memory/SeparateProofs.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.State
 import Arm.Memory.Separate
 import Std.Tactic.BVDecide
+import Tactics.BvOmegaBench
 
 ----------------------------------------------------------------------
 
@@ -30,45 +31,45 @@ theorem n_minus_1_lt_2_64_1 (n : Nat)
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_left_64 (a m : BitVec 64) :
   a + m - a = m := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_right_64 (a m : BitVec 64) :
   a + m - m = a := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_add_left (a m n : BitVec 64) :
   a + m - (a + n) = m - n := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths, using general assoc/comm
 -- BitVec lemmas.
 theorem BitVec.sub_of_add_is_sub_sub (a b c : BitVec 64) :
   (a - (b + c)) = a - b - c := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths, using general assoc/comm
 -- BitVec lemmas.
 theorem BitVec.add_of_sub_sub_of_add (a b c : BitVec 64) :
   (a + b - c) = a - c + b := by
-  bv_omega
+  bv_omega_bench
 
 theorem nat_bitvec_sub1 (x y : BitVec 64)
   (_h : y.toNat <= x.toNat) :
   (x - y).toNat = (x.toNat - y.toNat) % 2^64 := by
-  bv_omega
+  bv_omega_bench
 
 theorem nat_bitvec_sub2 (x y : Nat)
   (h : y <= x) (xub : x < 2^64) :
   BitVec.ofNat 64 (x - y) =
   (BitVec.ofNat 64 x) - (BitVec.ofNat 64 y) := by
-  bv_omega
+  bv_omega_bench
 
 theorem addr_add_one_add_m_sub_one  (n : Nat) (addr : BitVec 64)
   (h_lb : Nat.succ 0 ≤ n) (h_ub : n + 1 ≤ 2 ^ 64) :
   (addr + 1#64 + (BitVec.ofNat 64 (n - 1))) = addr + (BitVec.ofNat 64 n) := by
-  bv_omega
+  bv_omega_bench
 
 ----------------------------------------------------------------------
 ---- mem_subset ----
@@ -124,7 +125,7 @@ theorem first_address_add_one_is_subset_of_region (n : Nat) (addr : BitVec 64)
   mem_subset (addr + 1#64) (addr + (BitVec.ofNat 64 n)) addr (addr + (BitVec.ofNat 64 n)) := by
   simp [mem_subset]
   apply first_address_add_one_is_subset_of_region_helper
-  bv_omega
+  bv_omega_bench
 
 private theorem first_addresses_add_one_is_subset_of_region_general_helper
   (n m addr1 addr2 : BitVec 64) (h0 : 0#64 < m) :
@@ -146,7 +147,7 @@ theorem first_addresses_add_one_is_subset_of_region_general
   revert h3
   simp [mem_subset]
   apply first_addresses_add_one_is_subset_of_region_general_helper
-  bv_omega
+  bv_omega_bench
 
 private theorem first_addresses_add_one_preserves_subset_same_addr_helper (h1l : 0#64 < m) :
   m - 1#64 ≤ (BitVec.ofNat 64 (2^64 - 1)) - 1#64 := by
@@ -208,26 +209,26 @@ theorem mem_subset_one_addr_region_lemma (addr1 addr2 : BitVec 64) (h : n1 <= 2
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1) - 1#64) addr2 addr2 → (n1 = 1) ∧ (addr1 = addr2) := by
   simp [mem_subset]
   have h0 := mem_subset_one_addr_region_lemma_helper (BitVec.ofNat 64 n1) addr1 addr2
-  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega
+  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega_bench
   simp_all only [ofNat_eq_ofNat, and_imp, ne_eq, false_or]
-  have h2 : (BitVec.ofNat 64 n1) = 1#64 → n1 = 1 := by bv_omega
+  have h2 : (BitVec.ofNat 64 n1) = 1#64 → n1 = 1 := by bv_omega_bench
   intro h₀ h₁
   simp_all only [true_implies, BitVec.sub_self, and_self]
 
 theorem mem_subset_one_addr_region_lemma_alt (addr1 addr2 : BitVec 64)
   (h : n1 < 2 ^ 64) :
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1)) addr2 addr2 → (n1 = 0) ∧ (addr1 = addr2) := by
   simp only [mem_subset, bitvec_rules, minimal_theory]
-  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega
+  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega_bench
   simp_all only [ne_eq, false_or, and_imp]
-  bv_omega
+  bv_omega_bench
 
 theorem mem_subset_same_region_lemma
   (h0 : 0 < n)
   (h1 : Nat.succ n ≤ 2 ^ 64) :
   mem_subset (addr + 1#64) (addr + 1#64 + (BitVec.ofNat 64 (n - 1))) addr (addr + (BitVec.ofNat 64 (Nat.succ n - 1))) := by
   simp [mem_subset]
-  bv_omega
+  bv_omega_bench
   done
 
 theorem mem_subset_trans
@@ -281,7 +282,7 @@ theorem mem_separate_contiguous_regions_one_address (addr : BitVec 64) (h : n' <
   mem_separate addr addr (addr + 1#64) (addr + 1#64 + (BitVec.ofNat 64 (n' - 1))) := by
   simp [mem_separate, mem_overlap]
   have h' : (BitVec.ofNat 64 (n' - 1)) < 0xffffffffffffffff#64 := by
-    bv_omega
+    bv_omega_bench
   apply mem_separate_contiguous_regions_one_address_helper
   assumption
 

Proofs/Experiments/AddLoop/AddLoop.lean

@@ -11,6 +11,7 @@ import Arm
 import Tactics.StepThms
 import Tactics.Sym
 import Correctness.ArmSpec
+import Tactics.BvOmegaBench
 
 namespace AddLoop
 
@@ -523,18 +524,18 @@ private theorem loop_inv_x0_le (x y : BitVec 64)
   (h_assert_x0 : x ≤ y)
   (h_assert_x0_nz : ¬x = 0x0#64) :
   x - 0x1#64 ≤ y := by
-  bv_omega
+  bv_omega_bench
 
 private theorem AddWithCarry.add_one_64 (x : BitVec 64) :
   (AddWithCarry x 0x1#64 0x0#1).fst = x + 0x1#64 := by
   simp only [AddWithCarry, bitvec_rules]
-  bv_omega
+  bv_omega_bench
 
 private theorem crock_lemma (x y z : BitVec 64) :
   x + (y - z) + 1#64 = x + (y - (z - 1#64)) := by
-  -- (FIXME) Without this apply below, bv_omega crashes my editor.
+  -- (FIXME) Without this apply below, bv_omega_bench crashes my editor.
   apply BitVec.eq_sub_iff_add_eq.mp
-  bv_omega
+  bv_omega_bench
 
 theorem partial_correctness :
   PartialCorrectness ArmState := by