chore: delete bv_omega', reuse bv_omega (#194)

### Description:

We want to reuse as much of `bv_omega` as possible, and implement
`bv_omega` within `simp_mem` by calling the appropriate `simp` and
`omega` meta level functions, with the goal of extracting the
counter-example model from `omega` for lazy unfolding (ala CEGAR). To do
this, we first delete our layers on top of `bv_omega`. The next patch in
the series will replace the call of `evalTactic (tactic| bv_omega)` with
the appropriate meta-level functions. This will allow us to inspect the
state of `bv_omega`, instead of it being a black-box tactic invocation.

This is a chore PR.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

Conformance succeeds. 

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

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
 
@@ -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
 

Proofs/Experiments/MemoryAliasing.lean

@@ -200,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
@@ -229,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]
 -/
@@ -248,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`.
 -/
@@ -268,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
 -/
@@ -290,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]
 
 /--

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,