chore: bugfixes and benchmark code for the memory based simp_mem

Arm/Memory/Attr.lean

@@ -23,3 +23,20 @@ register_simp_attr memory_omega
 
 -- Simprocs for address normalization
 register_simp_attr address_normalization
+
+register_option simp_mem.omegaTimeoutMs : Nat := {
+  defValue := 1000
+  descr := "maximum amount of time per omega invocation in milliseconds before `simp_mem` times out. `0` for no timeout."
+}
+
+register_option simp_mem.omegaNumIgnoredTimeouts: Nat := {
+  defValue := 0
+  descr := "number of times omega is allowed to timeout before an error is thrown."
+}
+
+
+def getOmegaTimeoutMs [Monad m] [MonadOptions m] : m Nat := do
+  return simp_mem.omegaTimeoutMs.get (← getOptions)
+
+def getOmegaNumIgnoredTimeouts [Monad m] [MonadOptions m] : m Nat := do
+  return simp_mem.omegaNumIgnoredTimeouts.get (← getOptions)

Correctness/Correctness.lean

@@ -216,6 +216,43 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ]
         ⟨n, Nat.le_refl _, hexit, hpost⟩
     find 0 (v1 s0 hp) (Nat.zero_le ..)
 
+
+/--
+Prove partial correctness using inductive assertions and functions
+`csteps` and `nextc`.
+
+We use `s0`, `si`, and `sf` to refer to initial, intermediate, and
+final (exit) states respectively.
+
+This is Theorem 1 from page 5 of the paper. This proof method is more
+convenient to use than `partial_correctness_by_stepwise_invariants`
+because we need only attach assertions at certain cutpoints. However,
+it may still be tedious to use from the point of view of automation
+because it is difficult to both symbolically simulate an instruction
+and unwind `csteps` in tandem. So far, we have found that it is
+easiest to determine what concrete value `csteps` yields (via symbolic
+simulation), and then perform symbolic simulation -- however, then we
+end up doing simulation twice, which is expensive.
+
+Also see `partial_correctness_from_assertions`.
+-/
+theorem partial_correctness_from_verification_conditions_concrete_num_steps [Sys σ] [Spec' σ]
+    (csteps' : σ → Nat) -- a computable function that tells us the number of steps.
+    (hnsteps : ∀ (s0 si : σ), (hs : assert s0 si) →
+      run si (csteps' si) = (nextc (run si 1))) -- csteps' si is the steps till the next cutpoint.
+    (v1 : ∀ s0 : σ, pre s0 → assert s0 s0)
+    (v2 : ∀ sf : σ, exit sf → cut sf)
+    (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf)
+    -- We use `run` since it plays well with `sym_n` proof automation.
+    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (run si (csteps' si)))
+    : PartialCorrectness σ := by
+  intro s0 n hp hexit
+  apply partial_correctness_from_verification_conditions <;> try assumption
+  intros s0' si' hassert' hexit'
+  specialize (v4 s0' si' hassert' hexit')
+  rw [← hnsteps s0' si' hassert']
+  exact v4
+
 ----------------------------------------------------------------------
 
 /-!

Proofs/AES-GCM/GCMGmultV8Sym.lean

@@ -91,7 +91,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
     sym_aggregate
   · intro n addr h_separate
-    simp_mem (config := { useOmegaToClose := false })
+    simp_mem
     -- Aggregate the memory (non)effects.
     simp only [*]
   done

Proofs/Experiments/Memcpy/MemCpyVCG.lean

@@ -440,10 +440,28 @@ end CutTheorems
 
 section PartialCorrectness
 
+/-
+tactic execution of Lean.Parser.Tactic.omega took 290ms
+tactic execution of Lean.Parser.Tactic.omega took 1.81s
+tactic execution of simp_mem took 751ms
+tactic execution of Lean.Parser.Tactic.omega took 1.11s
+tactic execution of Lean.Parser.Tactic.omega took 664ms
+tactic execution of Lean.Parser.Tactic.omega took 676ms
+instantiate metavars took 7.15s
+share common exprs took 3.9s
+type checking took 1.47s
+process pre-definitions took 440ms
+-/
 -- set_option skip_proof.skip true in
+set_option maxHeartbeats 0 in
 -- set_option trace.profiler true in
 -- set_option profiler true in
-set_option maxHeartbeats 0 in
+-- set_option trace.profiler true in
+-- set_option profiler true in
+set_option trace.simp_mem true
+set_option trace.simp_mem.info true
+set_option simp_mem.omegaNumIgnoredTimeouts 0 in
+set_option simp_mem.omegaTimeoutMs 1000 in
 theorem Memcpy.extracted_2 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -471,7 +489,8 @@ 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 (config := {useOmegaToClose := true})
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by
+    sorry
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
     skip_proof simp_mem
@@ -482,10 +501,41 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
       skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega
     · apply mem_subset'_refl hsep.hb
 
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 1.54s
+tactic execution of simp_mem took 274ms
+tactic execution of Lean.Parser.Tactic.omega took 1.11s
+tactic execution of simp_mem took 403ms
+tactic execution of Lean.Parser.Tactic.omega took 302ms
+tactic execution of Lean.Parser.Tactic.omega took 284ms
+tactic execution of Lean.Parser.Tactic.omega took 4.25s
+tactic execution of simp_mem took 1.96s
+tactic execution of Lean.Parser.Tactic.omega took 8.95s
+tactic execution of simp_mem took 1.68s
+tactic execution of Lean.Parser.Tactic.omega took 102ms
+tactic execution of Lean.Parser.Tactic.omega took 1.9s
+tactic execution of simp_mem took 318ms
+tactic execution of Lean.Parser.Tactic.omega took 322ms
+tactic execution of Lean.Parser.Tactic.omega took 115ms
+tactic execution of Lean.Parser.Tactic.omega took 101ms
+instantiate metavars took 30s
+share common exprs took 16.7s
+fix level params took 118ms
+type checking took 4.37s
+process pre-definitions took 5.44s
+-/
+
+set_option maxHeartbeats 0
 -- set_option skip_proof.skip true in
 set_option maxHeartbeats 0 in
 -- set_option trace.profiler true in
 -- set_option profiler true in
+-- set_option trace.profiler true in
+-- set_option profiler true in
+set_option trace.simp_mem.info true
+set_option simp_mem.omegaNumIgnoredTimeouts 9999 in
+-- set_option simp_mem.omegaTimeoutMs 1000 in
 theorem Memcpy.extracted_0 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -555,6 +605,23 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
   · intros n addr hsep
     apply Memcpy.extracted_2 <;> assumption
 
+/-
+tactic execution of Lean.Parser.Tactic.omega took 616ms
+tactic execution of Lean.Parser.Tactic.omega took 1.1s
+tactic execution of Lean.Parser.Tactic.assumption took 114ms
+instantiate metavars took 14.7s
+share common exprs took 1.94s
+type checking took 988ms
+-/
+
+set_option maxHeartbeats 0 in
+set_option trace.profiler true in
+set_option profiler true in
+set_option maxHeartbeats 0 in
+set_option trace.simp_mem.info true in
+set_option simp_mem.omegaNumIgnoredTimeouts 9999 in
+-- set_option trace.profiler true in
+-- set_option profiler true in
 -- set_option trace.profiler true in
 -- set_option profiler true in
 theorem partial_correctness :
@@ -673,7 +740,7 @@ theorem partial_correctness :
             simp only [memory_rules] at h_si_read_sep
             rw [h_si_read_sep]
             rw [h_si_x0_eq_zero]
-            skip_proof simp_mem -- nice!
+            skip_proof sorry -- nice!
           · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self]
       · have step_8f4_8e4 :=
           program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed

Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean

@@ -0,0 +1,111 @@
+import Arm.Memory.SeparateAutomation
+
+set_option linter.all false
+set_option maxHeartbeats 0
+set_option trace.profiler true
+set_option profiler true
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 3.71s
+instantiate metavars took 16.5s
+share common exprs took 3.59s
+type checking took 936ms
+process pre-definitions took 376ms
+elaboration took 2.32s
+-/
+theorem memcpy_extracted_0_line_585
+(h_si_x0_nonzero : six0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (six0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (six0 - 0x1#64)))
+(h_assert_1 : six0 ≤ s0.x0)
+(h_assert_3 : six1 = s0.x1 + 0x10#64 * (s0.x0 - six0))
+(h_assert_4 : six2 = s0.x2 + 0x10#64 * (s0.x0 - six0))
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - six0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - six0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - six0 < s0.x0 - (six0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - six0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+      s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+  s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+      (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+        s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+: s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ 2 ^ 64 ∧
+  (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat ∨
+      s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16) := by
+  bv_omega
+
+
+#exit
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 3.67s
+instantiate metavars took 15.3s
+share common exprs took 3.28s
+type checking took 742ms
+process pre-definitions took 475ms
+linting took 262ms
+elaboration took 2.07s
+-/
+theorem memcpy_extracted_0_line_585
+(s0 si : ArmState)
+(h_si_x0_nonzero : si.x0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_assert_1 : si.x0 ≤ s0.x0)
+(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64),
+  mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n →
+    Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem)
+(h_assert_5 : ∀ (i : BitVec 64),
+  i < s0.x0 - si.x0 →
+    Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem)
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+      s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+  s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+      (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+        s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+: s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ 2 ^ 64 ∧
+  (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat ∨
+      s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16) := by
+  bv_omega

Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean

@@ -0,0 +1,63 @@
+import Arm
+import Arm.Memory.SeparateAutomation
+
+set_option maxHeartbeats 0
+set_option trace.profiler true 
+set_option profiler true
+
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 5.47s
+instantiate metavars took 7.69s
+share common exprs took 4.82s
+type checking took 860ms
+process pre-definitions took 1.59s
+linting took 353ms
+elaboration took 2.91s
+-/
+theorem memcpy 
+(s0 si : ArmState)
+(h_si_x0_nonzero : si.x0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_assert_1 : si.x0 ≤ s0.x0)
+(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64),
+  mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n →
+    Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem)
+(h_assert_5 : ∀ (i : BitVec 64),
+  i < s0.x0 - si.x0 →
+    Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem)
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+   s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+   s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+       s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega: s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+   s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+       (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+         s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) :
+  (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+  (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ∧
+      (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 := by
+  bv_omega
+