feat: Switch to using bv_decide to decide memory goals instead of bv_omega

Arm/BitVec.lean

@@ -14,6 +14,9 @@ namespace BitVec
 
 open BitVec
 
+@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
+abbrev truncate_truncate_of_le := @setWidth_setWidth_of_le
+
 -- Adding some useful simp lemmas to `bitvec_rules`: we do not include
 -- `bv_toNat` lemmas here.
 -- See Init.Data.BitVec.Lemmas.
@@ -161,6 +164,8 @@ attribute [bitvec_rules] BitVec.ofBool_false
 attribute [bitvec_rules] BitVec.ofNat_eq_ofNat
 attribute [bitvec_rules] BitVec.zero_eq
 attribute [bitvec_rules] BitVec.truncate_eq_zeroExtend
+attribute [bitvec_rules] BitVec.or_self
+attribute [minimal_theory] BitVec.zero_or
 
 attribute [bitvec_rules] BitVec.add_sub_cancel
 attribute [bitvec_rules] BitVec.sub_add_cancel
@@ -213,7 +218,7 @@ attribute [bitvec_rules] BitVec.reduceULT
 attribute [bitvec_rules] BitVec.reduceULE
 attribute [bitvec_rules] BitVec.reduceSLT
 attribute [bitvec_rules] BitVec.reduceSLE
-attribute [bitvec_rules] BitVec.reduceZeroExtend'
+attribute [bitvec_rules] BitVec.reduceSetWidth'
 attribute [bitvec_rules] BitVec.reduceShiftLeftZeroExtend
 attribute [bitvec_rules] BitVec.reduceExtracLsb'
 attribute [bitvec_rules] BitVec.reduceReplicate
@@ -245,6 +250,7 @@ attribute [bitvec_rules] Nat.reduceLTLE
 attribute [bitvec_rules] Nat.reduceLeDiff
 attribute [bitvec_rules] Nat.reduceSubDiff
 attribute [bitvec_rules] BitVec.toNat_ofNat
+attribute [bitvec_rules] BitVec.natCast_eq_ofNat
 
 -- Some Fin lemmas useful for bitvector reasoning:
 attribute [bitvec_rules] Fin.eta
@@ -456,9 +462,6 @@ theorem toNat_ofNat_lt {n w₁ : Nat} (hn : n < 2^w₁) :
 
 ---------------------------- Comparison Lemmas -----------------------
 
-@[simp] protected theorem not_lt {n : Nat} {a b : BitVec n} : ¬ a < b ↔ b ≤ a := by
-  exact Fin.not_lt ..
-
 theorem ge_of_not_lt (x y : BitVec w₁) (h : ¬ (x < y)) : x ≥ y := by
   simp_all only [BitVec.le_def, BitVec.lt_def]
   omega
@@ -500,32 +503,12 @@ protected theorem zero_le_sub (x y : BitVec n) :
 
 ----------------------------- Logical  Lemmas ------------------------
 
-@[bitvec_rules]
-protected theorem zero_or (x : BitVec n) : 0#n ||| x = x := by
-  unfold HOr.hOr instHOrOfOrOp OrOp.or instOrOp BitVec.or
-  simp only [toNat_ofNat, Nat.zero_mod, Nat.zero_or]
-  congr
-
-@[bitvec_rules]
-protected theorem or_zero (x : BitVec n) : x ||| 0#n = x := by
-  rw [BitVec.or_comm]
-  rw [BitVec.zero_or]
-  done
-
-@[bitvec_rules]
-protected theorem or_self (x : BitVec n) :
-  x ||| x = x := by
-  refine eq_of_toNat_eq ?_
-  rw [BitVec.toNat_or]
-  apply Nat.eq_of_testBit_eq
-  simp only [Nat.testBit_or, Bool.or_self, implies_true]
-  done
 
 --------------------- ZeroExtend/Append/Extract  Lemmas ----------------
 
 @[bitvec_rules]
 theorem zeroExtend_zero_width : (zeroExtend 0 x) = 0#0 := by
-  unfold zeroExtend
+  unfold zeroExtend setWidth
   split <;> simp [bitvec_zero_is_unique]
 
 -- During symbolic simulation, we often encounter an `if` in the first argument
@@ -1087,21 +1070,6 @@ theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
   intro ⟨0, _⟩
   simp
 
-/-- If multiplication does not overflow,
-then `(x * y).toNat` equals `x.toNat * y.toNat` -/
-theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) :
-    (x * y).toNat = x.toNat * y.toNat := by
-  rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h]
-
-/-- If subtraction does not overflow,
-then `(x - y).toNat` equals `x.toNat - y.toNat` -/
-theorem toNat_sub_of_lt {w} {x y : BitVec w} (h : x.toNat < y.toNat) :
-    (y - x).toNat = y.toNat - x.toNat := by
-  rw [BitVec.toNat_sub,
-    show (2^w - x.toNat + y.toNat) = 2^w + (y.toNat - x.toNat) by omega,
-    Nat.add_mod, Nat.mod_self, Nat.zero_add, Nat.mod_mod,
-    Nat.mod_eq_of_lt (by omega)]
-
 /-- `x.toNat * z.toNat ≤ k` if `z ≤ y` and `x.toNat * y.toNat ≤ k` -/
 theorem toNat_mul_toNat_le_of_le_of_le {w} (x y z : BitVec w)
     (hxy : x.toNat * y.toNat ≤ k)

Arm/Cfg/Cfg.lean

@@ -216,8 +216,8 @@ protected def addToCfg (address : BitVec 64) (program : Program) (cfg : Cfg)
 -- is in terms of Fin so that we can take advantage of Fin lemmas. We
 -- will map this theorem to BitVecs (using lemmas like
 -- BitVec.fin_bitvec_lt) in create'.
-private theorem termination_lemma (i j max : Fin n) (h : n > 0)
-  (h0 : i < max) (h1 : j <= max - i) (h2 : ((Fin.ofNat' 0 h) : Fin n) < j) :
+private theorem termination_lemma (i j max : Fin n) (h : NeZero n)
+  (h0 : i < max) (h1 : j <= max - i) (h2 : ((Fin.ofNat' n 0)) < j) :
   (max - (i + j)) < (max - i) := by
   -- Our strategy is to convert this proof obligation in terms of Nat,
   -- which is made possible by h0 and h1 hypotheses above.
@@ -270,7 +270,7 @@ private def create' (address : BitVec 64) (max_address : BitVec 64)
     else if h₂ : 4#64 <= max_address - address then
          have ?term_lemma : (max_address - (address + 4#64)).toNat < (max_address - address).toNat := by
            have := termination_lemma address.toFin (4#64).toFin max_address.toFin
-                   (by decide)
+                   (by exact inferInstance)
                    (by simp_all! only [BitVec.not_lt, BitVec.fin_bitvec_lt, not_false_eq_true, BitVec.lt_of_le_ne, h₁])
                    (by rw [← BitVec.toFin_sub]; exact h₂)
                    (by simp_arith)

Arm/Insts/Common.lean

@@ -401,9 +401,6 @@ dsimproc [state_simp_rules] reduceInvalidBitMasks (invalid_bit_masks _ _ _ _) :=
                       imm.expr.isTrue
                       M)
 
-theorem Nat.lt_one_iff {n : Nat} : n < 1 ↔ n = 0 := by
-  omega
-
 theorem M_divisible_by_esize_of_valid_bit_masks (immN : BitVec 1) (imms : BitVec 6)
   (immediate : Bool) (M : Nat):
   ¬ invalid_bit_masks immN imms immediate M →

Arm/Insts/LDST/Reg_imm.lean

@@ -31,7 +31,7 @@ instance : ToString Reg_imm_cls where toString a := toString (repr a)
 @[state_simp_rules]
 def reg_imm_operation (inst_str : String) (op : BitVec 1)
   (wback : Bool) (postindex : Bool) (SIMD? : Bool)
-  (datasize : Nat) (regsize : Option Nat) (Rn : BitVec 5)
+  (datasize : Nat) (hdatasize : datasize < 2^64) (regsize : Option Nat) (Rn : BitVec 5)
   (Rt : BitVec 5) (offset : BitVec 64) (s : ArmState)
   (H : 8 ∣ datasize) : ArmState :=
   let address := read_gpr 64 Rn s
@@ -48,7 +48,15 @@ def reg_imm_operation (inst_str : String) (op : BitVec 1)
       match op with
       | 0#1 => -- STORE
         let data := ldst_read SIMD? datasize Rt s
-        write_mem_bytes (datasize / 8) address (BitVec.cast h.symm data) s
+        write_mem_bytes' (datasize / 8) address (data.cast (by 
+          simp [bv_toNat]
+          show _ = (BitVec.udiv _ _).toNat * 8
+          rw [BitVec.toNat_udiv]
+          simp
+          rw [Nat.mod_eq_of_lt (by omega)]
+          omega
+        )) s
+        -- write_mem_bytes (datasize / 8) address (BitVec.cast h.symm data) s
       | _ => -- LOAD
         let data := read_mem_bytes (datasize / 8) address s
         if SIMD? then write_sfp datasize Rt (BitVec.cast h data) s
@@ -79,12 +87,13 @@ def supported_reg_imm (size : BitVec 2) (opc : BitVec 2) (SIMD? : Bool) : Bool :
   | 0b00#2, 0b11#2, true => true -- LDR, 128-bit, SIMD&FP
   | _, _, _ => false -- other instructions that are not supported or illegal
 
+
 @[state_simp_rules]
 def exec_reg_imm_common
   (inst : Reg_imm_cls) (inst_str : String) (s : ArmState) : ArmState :=
-  let scale :=
-    if inst.SIMD? then ((lsb inst.opc 1) ++ inst.size).toNat
-    else inst.size.toNat
+  let ⟨scale, hscale⟩ : { n : Nat //  n ≤ 10} :=
+    if inst.SIMD? then ⟨((lsb inst.opc 1) ++ inst.size).toNat, by bv_omega⟩
+    else ⟨inst.size.toNat, by bv_omega⟩
   -- Only allow supported LDST Reg immediate instructions
   if not $ supported_reg_imm inst.size inst.opc inst.SIMD? then
     write_err (StateError.Unimplemented "Unsupported instruction {inst_str} encountered!") s
@@ -100,6 +109,12 @@ def exec_reg_imm_common
       | Sum.inl imm12 => (BitVec.zeroExtend 64 imm12) <<< scale
       | Sum.inr imm9 => signExtend 64 imm9
     let datasize := 8 <<< scale
+    have : datasize < 2^64 := by 
+      simp [datasize]
+      rw [Nat.shiftLeft_eq]
+      have : 2^scale ≤ 2^10 := by apply Nat.pow_le_pow_of_le (by decide) (by omega)
+      simp at this
+      omega
     let regsize :=
       if inst.SIMD? then none
       else if inst.size = 0b11#2 then some 64 else some 32
@@ -108,7 +123,7 @@ def exec_reg_imm_common
     -- State Updates
     let s' := reg_imm_operation inst_str
               (lsb inst.opc 0) inst.wback inst.postindex
-              inst.SIMD? datasize regsize inst.Rn inst.Rt offset s (H)
+              inst.SIMD? datasize (by omega) regsize inst.Rn inst.Rt offset s (H)
     let s' := write_pc ((read_pc s) + 4#64) s'
     s'