module set_option linter.unusedSimpArgs false open BitVec namespace BitVec' theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) : (BitVec.ofFin x)[i] = x.val.testBit i := rfl theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by grind [getMsbD] theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by grind theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w := by grind theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by grind theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by grind theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w, l[n] = a := by grind theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a := by grind theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by grind theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by grind theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := by grind theorem getElem?_eq (l : BitVec w) (i : Nat) : l[i]? = if h : i < w then some l[i] else none := by grind theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : (some l[i] = l[i]?) ↔ True := by grind theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) : (l[i]? = some l[i]) ↔ True := by grind theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by grind theorem getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : l[i] = l[i]?.get (by simp [h]) := by grind theorem getLsbD_eq_getElem?_getD {x : BitVec w} {i : Nat} : x.getLsbD i = x[i]?.getD false := by rw [getElem?_def] split · rfl · grind theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = true) : (x[i]'(lt_of_getLsbD h) = true) = True := by grind /-- This normalized a bitvec using `ofFin` to `ofNat`. -/ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt] /-- Prove nonequality of bitvectors in terms of nat operations. -/ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by grind [eq_of_toNat_eq] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat := by grind [eq_of_toNat_eq] theorem toNat_inj {x y : BitVec n} : x.toNat = y.toNat ↔ x = y := toNat_eq.symm @[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by grind [toNat_eq] protected theorem toNat_lt_twoPow_of_le (h : m ≤ n) {x : BitVec m} : x.toNat < 2 ^ n := by apply Nat.lt_of_lt_of_le x.isLt apply Nat.pow_le_pow_of_le <;> grind theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w} (hi : i < w) (hx : x[i] = true) : 2^i ≤ x.toNat := by apply Nat.ge_two_pow_of_testBit grind theorem msb_eq_getMsbD (x : BitVec w) : x.msb = x.getMsbD 0 := by grind [BitVec.msb] theorem getMsb_eq_getLsb (x : BitVec w) (i : Fin w) : x.getMsb i = x.getLsb ⟨w - 1 - i, by omega⟩ := by simp only [getMsb, getLsb] theorem getMsb?_eq_getLsb? (x : BitVec w) (i : Nat) : x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none := by grind [getMsb?] theorem getMsbD_eq_getLsbD (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i)) := by grind [getMsbD] theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i)) := by rw [getMsbD, getLsbD] theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i)) := by grind theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by grind theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by grind theorem lt_of_getElem?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by grind theorem lt_of_getMsb?_eq_some (x : BitVec w) (i : Nat) : getMsb? x i = some b → i < w := by grind theorem lt_of_isSome_getElem? (x : BitVec w) (i : Nat) : x[i]?.isSome → i < w := by grind theorem lt_of_isSome_getMsb? (x : BitVec w) (i : Nat) : (getMsb? x i).isSome → i < w := by grind theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) : x.getMsbD i = (x.getMsb? i).getD false := by grind theorem eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} : x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i := by have iff := @BitVec.eq_of_getElem_eq_iff w x y constructor <;> grind theorem eq_of_getMsbD_eq {x y : BitVec w} (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by simp only [getMsbD] at pred apply eq_of_getLsbD_eq intro i i_lt if w_zero : w = 0 then grind else have w_pos : 0 < w := by grind have r : i ≤ w - 1 := by -- FIXME: `grind` fails with a kernel type mismatch here -- with a failure in reduction of `Lean.Grind.CommRing.Stepwise.imp_1eq_cert` -- We need an `@[expose]` somewhere, but where? simp [Nat.le_sub_iff_add_le w_pos] grind have q_lt : w - 1 - i < w := by simp only [Nat.sub_sub] -- FIXME: `grind` fails with a kernel type mismatch here -- with a failure in reduction of `Lean.Grind.CommRing.Stepwise.imp_1eq_cert` apply Nat.sub_lt w_pos grind have q := pred (w - 1 - i) q_lt simpa [q_lt, Nat.sub_sub_self, r] using q -- This cannot be a `@[simp]` lemma, as it would be tried at every term. theorem of_length_zero {x : BitVec 0} : x = 0#0 := by grind theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero] theorem toInt_zero_length (x : BitVec 0) : x.toInt = 0 := by simp [of_length_zero] theorem toNat_zero : (0#w).toNat = 0 := rfl theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by grind theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by grind theorem msb_zero_length (x : BitVec 0) : x.msb = false := by grind theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by grind theorem toInt_of_zero_length (h : w = 0) (x : BitVec w) : x.toInt = 0 := by grind theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by grind theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by grind theorem msb_of_zero_length (h : w = 0) (x : BitVec w) : x.msb = false := by grind theorem eq_of_zero_length (h : w = 0) {x y : BitVec w} : x = y := by grind theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w := by grind theorem ofFin_ofNat (n : Nat) : ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat] -- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term. grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w)) theorem ofFin_neg {x : Fin (2 ^ w)} : ofFin (-x) = -(ofFin x) := by rfl open Fin.NatCast in @[simp, norm_cast] theorem ofFin_natCast (n : Nat) : ofFin (n : Fin (2^w)) = (n : BitVec w) := by rfl theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y := ⟨@eq_of_toFin_eq w x y, by grind⟩ theorem toFin_zero : toFin (0 : BitVec w) = 0 := rfl theorem toFin_one : toFin (1 : BitVec w) = 1 := by rw [toFin_inj]; grind open Fin.NatCast in @[simp, norm_cast] theorem toFin_natCast (n : Nat) : toFin (n : BitVec w) = (n : Fin (2^w)) := by rfl theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat 2 (b.toNat) := by cases b <;> rfl theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := by rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat] theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by decide theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) : getLsbD (x#'lt) i = x.testBit i := by simp [getLsbD, BitVec.ofNatLT] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) : getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by grind theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n := eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn]) theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat (2^w) x := rfl theorem finMk_toNat (x : BitVec w) : Fin.mk x.toNat x.isLt = x.toFin := rfl theorem toFin_ofNatLT {n : Nat} (h : n < 2 ^ w) : (BitVec.ofNatLT n h).toFin = Fin.mk n h := rfl theorem toFin_ofFin (n : Fin (2 ^ w)) : (BitVec.ofFin n).toFin = n := rfl theorem ofFin_toFin (x : BitVec w) : BitVec.ofFin x.toFin = x := rfl theorem ofNatLT_finVal (n : Fin (2 ^ w)) : BitVec.ofNatLT n.val n.isLt = BitVec.ofFin n := rfl theorem ofNatLT_toNat (x : BitVec w) : BitVec.ofNatLT x.toNat x.isLt = x := rfl theorem ofNat_finVal (n : Fin (2 ^ w)) : BitVec.ofNat w n.val = BitVec.ofFin n := by rw [← BitVec.ofNatLT_eq_ofNat n.isLt, ofNatLT_finVal] -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals. -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea. theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : getLsbD (BitVec.ofNat n x) i = (i < n && x.testBit i) := by simp [getLsbD, BitVec.ofNat, Fin.val_ofNat] theorem getLsbD_zero : (0#w).getLsbD i = false := by grind [getLsbD] theorem getElem_zero (h : i < w) : (0#w)[i] = false := by grind [getElem_eq_testBit_toNat] theorem getMsbD_zero : (0#w).getMsbD i = false := by grind [getMsbD] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow] by_cases h : i = 0 <;> simp [h, Nat.testBit_eq_decide_div_mod_eq, Nat.div_eq_of_lt] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by grind [=_ getLsbD_eq_getElem] /-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero. -/ theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w)) := by grind -- This is not a good `grind` lemma because we would have to index on `%`. theorem toNat_mod_cancel (x : BitVec n) : x.toNat % 2^n = x.toNat := Nat.mod_eq_of_lt x.isLt theorem toNat_mod_cancel' {x : BitVec n} : (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat := by grind [toNat_mod_cancel] theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h rw [Nat.mod_eq_of_lt (by omega)] theorem sub_toNat_mod_cancel_of_toNat {x : BitVec w} (h : x.toNat ≠ 0) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by have := x.isLt grind [= Nat.mod_eq_of_lt] theorem toNat_mod_cancel_of_lt {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h exact Nat.mod_eq_of_lt (by omega) theorem sub_sub_toNat_cancel {x : BitVec w} : 2 ^ w - (2 ^ w - x.toNat) = x.toNat := by grind theorem sub_add_bmod_cancel {x y : BitVec w} : ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) = ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by /- **Note**: This is a goal containing nonlinear integer arithmetic. This is not in `grind`s scope. The following command used to work before we expanded `Int.bmod` into `Int.emod`. -/ -- grind [=_ Int.add_bmod_right] sorry private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n := Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_right (by trivial : 0 < 2) le) theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by grind theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by grind theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by grind theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by grind -- This does not need to be a `@[simp]` or `@[grind]` theorem as it is already handled by -- `getElem_zero_ofBool` and `getElem?_eq_getElem`. theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by simp only [ofBool, ofNat_eq_ofNat, cond_eq_ite] split <;> -- FIXME: `grind` gives a kernel type mismatch here: -- (kernel) application type mismatch -- forall_prop_domain_congr (Eq.trans (Lean.Grind.Nat.lt_eq 0 1) (eq_true_of_decide (Eq.refl true))) fun h => -- Eq.refl ((1#1)[0]? = some true) -- argument has type -- True → ((1#1)[0]? = some true) = ((1#1)[0]? = some true) -- but function has type -- (∀ (a : True), (fun h => (1#1)[0]? = some (1#1)[0]) ⋯ = (fun h => (1#1)[0]? = some true) a) → -- (∀ (a : 0 < 1), (fun h => (1#1)[0]? = some (1#1)[0]) a) = ∀ (a : True), (fun h => (1#1)[0]? = some true) a simp_all theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by grind [getElem?_zero_ofBool] theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by grind theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b) := by grind theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by grind theorem getElem_ofBool {b : Bool} {h : i < 1} : (ofBool b)[i] = b := by grind theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by grind theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by grind theorem one_eq_zero_iff : 1#w = 0#w ↔ w = 0 := by constructor · intro h cases w · rfl · replace h := congrArg BitVec.toNat h simp at h · grind /-- `0#w = 1#w` iff the width is zero. -/ theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by grind [one_eq_zero_iff] /-! ### msb -/ theorem msb_zero : (0#w).msb = false := by grind theorem msb_one : (1#w).msb = decide (w = 1) := by grind theorem msb_eq_getLsbD_last (x : BitVec w) : x.msb = x.getLsbD (w - 1) := by grind @[bitvec_to_nat] theorem getLsbD_last (x : BitVec w) : x.getLsbD (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat) := by rcases w with rfl | w · grind · simp only [getLsbD, Nat.testBit_eq_decide_div_mod_eq, Nat.succ_sub_succ_eq_sub, Nat.sub_zero] rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h · grind [Nat.div_eq_of_lt] · simp only [h] rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt] · grind · omega -- TODO: `grind` can't do this because it doesn't know that `0 < 2^w` and `2^(w+1) = 2 * 2^w`. @[bitvec_to_nat] theorem getLsbD_succ_last (x : BitVec (w + 1)) : x.getLsbD w = decide (2 ^ w ≤ x.toNat) := getLsbD_last x @[bitvec_to_nat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w - 1) ≤ x.toNat) := by grind theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2 ^ (n - 1) := by grind theorem msb_eq_getMsbD_zero (x : BitVec w) : x.msb = x.getMsbD 0 := by grind [msb_eq_getLsbD_last] /-! ### cast -/ theorem toFin_cast (h : w = v) (x : BitVec w) : (x.cast h).toFin = x.toFin.cast (by rw [h]) := rfl theorem getLsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getLsbD i = x.getLsbD i := by grind theorem getMsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getMsbD i = x.getMsbD i := by grind theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (x.cast h)[i] = x[i] := by subst h; grind theorem msb_cast (h : w = v) (x : BitVec w) : (x.cast h).msb = x.msb := by grind /-! ### toInt/ofInt -/ /-- Prove equality of bitvectors in terms of nat operations. -/ theorem toInt_eq_toNat_cond (x : BitVec n) : x.toInt = if 2*x.toNat < 2^n then (x.toNat : Int) else (x.toNat : Int) - (2^n : Nat) := rfl theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) : x.toInt = x.toNat := by grind [toInt_eq_toNat_cond] theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w := by cases w <;> grind [msb_eq_decide] grind_pattern msb_eq_false_iff_two_mul_lt => x.msb, x.toNat theorem msb_eq_true_iff_two_mul_ge {x : BitVec w} : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by grind /-- Characterize `x.toInt` in terms of `x.msb`. -/ theorem toInt_eq_msb_cond (x : BitVec w) : x.toInt = if x.msb then (x.toNat : Int) - (2^w : Nat) else (x.toNat : Int) := by grind [BitVec.toInt] theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) : x.toInt = x.toNat := by grind [toInt_eq_msb_cond] -- Activate `toInt_eq_toNat_of_msb` if we have already seen both `x.toInt` and `x.toNat` grind_pattern toInt_eq_toNat_of_msb => x.toInt, x.toNat theorem toNat_toInt_of_msb {w : Nat} (b : BitVec w) (hb : b.msb = false) : b.toInt.toNat = b.toNat := by grind theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by simp only [toInt_eq_toNat_cond] split next g => rw [Int.bmod_pos] <;> simp only [← Int.natCast_emod, toNat_mod_cancel] grind next g => rw [Int.bmod_neg] <;> simp only [← Int.natCast_emod, toNat_mod_cancel] grind grind_pattern toInt_eq_toNat_bmod => x.toInt, x.toNat theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by grind [BitVec.toInt] theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt := by grind theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by rw [toInt_eq_msb_cond] simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte, toNat_ofNat, Int.natCast_emod] norm_cast apply Nat.mod_eq_of_lt apply Nat.one_lt_two_pow (by grind) /-- Prove equality of bitvectors in terms of integer operations. -/ theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by grind [toInt_eq_toNat_cond, eq_of_toNat_eq] theorem toInt_inj {x y : BitVec n} : x.toInt = y.toInt ↔ x = y := by grind [eq_of_toInt_eq] theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y := by rw [Ne, toInt_inj] @[simp, bitvec_to_nat] theorem toNat_ofInt {n : Nat} (i : Int) : (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by unfold BitVec.ofInt simp theorem toInt_ofNat' {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by simp [toInt_eq_toNat_bmod, -Int.natCast_pow] theorem toInt_ofNat {n : Nat} (x : Nat) : (no_index (OfNat.ofNat (α := BitVec n) x)).toInt = (x : Int).bmod (2^n) := toInt_ofNat' x theorem toInt_ofFin {w : Nat} (x : Fin (2^w)) : (BitVec.ofFin x).toInt = Int.bmod x (2^w) := by grind [toInt_eq_toNat_bmod] theorem toInt_ofInt {n : Nat} (i : Int) : (BitVec.ofInt n i).toInt = i.bmod (2^n) := by have _ := Nat.two_pow_pos n have p : 0 ≤ i % (2^n : Nat) := by omega simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p, -Int.natCast_pow] theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int} (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = n := by have hw : w = (w - 1) + 1 := by omega rw [toInt_ofInt, Int.bmod_eq_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega) theorem ofInt_natCast (w n : Nat) : BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl theorem ofInt_ofNat (w n : Nat) : BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl grind_pattern ofInt_ofNat => BitVec.ofInt w (OfNat.ofNat n) theorem toInt_neg_iff {w : Nat} {x : BitVec w} : BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by grind [toInt_eq_toNat_cond] theorem toInt_pos_iff {w : Nat} {x : BitVec w} : 0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by grind [toInt_eq_toNat_cond] theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by obtain ⟨a, ha⟩ := a simp only [Nat.reducePow] have acases : a = 0 ∨ a = 1 := by grind rcases acases with ⟨rfl | rfl⟩ · grind case inr h => -- TODO: why can't `grind` do this? subst h grind theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by simp [BitVec.toInt, show 0 < 2^w from Nat.two_pow_pos w] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by cases b <;> simp theorem toNat_one (h : 0 < w) : (1#w : BitVec w).toNat = 1 := by simp grind theorem toInt_one (h : 1 < w) : (1#w : BitVec w).toInt = 1 := by grind [toInt_eq_toNat_of_msb] theorem sub_toNat_mod_cancel_of_msb_true {x : BitVec w} (h : x.msb = true) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by simp only [msb_eq_decide, decide_eq_true_eq] at h have := Nat.two_pow_pos (w-1) exact sub_toNat_mod_cancel_of_toNat (by grind) theorem toNat_lt_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) : x.toNat < 2 ^ (w - 1) := by grind theorem le_toNat_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : 2 ^ (w - 1) ≤ x.toNat := by grind /-- `x.toInt` is less than `2^(w-1)`. We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used. -/ theorem two_mul_toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by simp only [BitVec.toInt] rcases w with _|w' · grind · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.cast_ofNat_Int] norm_cast -- TODO: `grind` won't do this because it doesn't have special handling for `2 ^ (w + 1)`. omega theorem two_mul_toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1 := Int.le_sub_one_of_lt two_mul_toInt_lt theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by by_cases h : w = 0 · subst h grind · have := @two_mul_toInt_lt w x rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this grind theorem toInt_le {w : Nat} {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1 := Int.le_sub_one_of_lt toInt_lt /-- `x.toInt` is greater than or equal to `-2^(w-1)`. We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used. -/ theorem le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by simp only [BitVec.toInt] rcases w with _|w' · grind · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.cast_ofNat_Int] norm_cast omega theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by by_cases h : w = 0 · grind · have := le_two_mul_toInt (w := w) (x := x) generalize x.toInt = x at * rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this grind theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by apply eq_of_toInt_eq rw [toInt_ofInt, Int.bmod_eq_of_le_mul_two] · simpa [Int.mul_comm _ 2] using le_two_mul_toInt · simpa [Int.mul_comm _ 2] using two_mul_toInt_lt theorem toNat_intCast {w : Nat} (x : Int) : (x : BitVec w).toNat = (x % 2^w).toNat := by change (BitVec.ofInt w x).toNat = _ simp theorem toInt_intCast {w : Nat} (x : Int) : (x : BitVec w).toInt = Int.bmod x (2^w) := by rw [toInt_eq_toNat_bmod, toNat_intCast, Int.natCast_toNat_eq_self.mpr] · have h : (2 ^ w : Int) = (2 ^ w : Nat) := by simp rw [h, Int.emod_bmod] · apply Int.emod_nonneg exact Int.pow_ne_zero (by decide) /-! ### sle/slt -/ /-- A bitvector, when interpreted as an integer, is less than zero iff its most significant bit is true. -/ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by have := toInt_eq_msb_cond x constructor · intro h apply Classical.byContradiction intro hmsb simp only [Bool.not_eq_true] at hmsb simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/ · intro h simp only [h, ↓reduceIte] at this simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq] omega theorem slt_zero_eq_msb {w : Nat} {x : BitVec w} : x.slt 0#w = x.msb := by grind [BitVec.slt_zero_iff_msb_cond] theorem sle_eq_decide {x y : BitVec w} : x.sle y = decide (x.toInt ≤ y.toInt) := rfl theorem slt_eq_decide {x y : BitVec w} : x.slt y = decide (x.toInt < y.toInt) := rfl theorem ule_eq_decide {x y : BitVec w} : x.ule y = decide (x.toNat ≤ y.toNat) := rfl theorem ult_eq_decide {x y : BitVec w} : x.ult y = decide (x.toNat < y.toNat) := rfl theorem ule_eq_decide_le {x y : BitVec w} : x.ule y = decide (x ≤ y) := rfl theorem ult_eq_decide_lt {x y : BitVec w} : x.ult y = decide (x < y) := rfl theorem ule_iff_le {x y : BitVec w} : x.ule y ↔ x ≤ y := decide_eq_true_iff theorem ult_iff_lt {x y : BitVec w} : x.ult y ↔ x < y := decide_eq_true_iff theorem sle_iff_toInt_le {w : Nat} {x y : BitVec w} : x.sle y ↔ x.toInt ≤ y.toInt := decide_eq_true_iff theorem slt_iff_toInt_lt {w : Nat} {x y : BitVec w} : x.slt y ↔ x.toInt < y.toInt := decide_eq_true_iff theorem ule_iff_toNat_le {x y : BitVec w} : x.ule y ↔ x.toNat ≤ y.toNat := decide_eq_true_iff theorem ult_iff_toNat_lt {x y : BitVec w} : x.ult y ↔ x.toNat < y.toNat := decide_eq_true_iff theorem sle_eq_slt_or_eq {x y : BitVec w} : x.sle y = (x.slt y || x == y) := by apply Bool.eq_iff_iff.2 simp only [BitVec.sle, decide_eq_true_eq, BitVec.slt, Bool.or_eq_true, beq_iff_eq, ← toInt_inj] omega theorem slt_eq_sle_and_ne {x y : BitVec w} : x.slt y = (x.sle y && x != y) := by apply Bool.eq_iff_iff.2 simp [BitVec.slt, BitVec.sle, Int.lt_iff_le_and_ne, BitVec.toInt_inj] /-- For all bitvectors `x, y`, either `x` is signed less than `y`, or is equal to `y`, or is signed greater than `y`. -/ theorem slt_trichotomy (x y : BitVec w) : x.slt y ∨ x = y ∨ y.slt x := by simpa [slt_iff_toInt_lt, ← toInt_inj] using Int.lt_trichotomy x.toInt y.toInt /-- For all bitvectors `x, y`, either `x` is unsigned less than `y`, or is equal to `y`, or is unsigned greater than `y`. -/ theorem lt_trichotomy (x y : BitVec w) : x < y ∨ x = y ∨ y < x := by simpa [← ult_iff_lt, ult_eq_decide, decide_eq_true_eq, ← toNat_inj] using Nat.lt_trichotomy x.toNat y.toNat /-! ### setWidth, zeroExtend and truncate -/ theorem truncate_eq_setWidth {v : Nat} {x : BitVec w} : truncate v x = setWidth v x := rfl theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} : zeroExtend v x = setWidth v x := rfl theorem toInt_setWidth (x : BitVec w) : (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by grind [toInt_eq_toNat_bmod, Int.emod_bmod] theorem toFin_setWidth {x : BitVec w} : (x.setWidth v).toFin = Fin.ofNat (2^v) x.toNat := by ext; grind theorem setWidth_eq (x : BitVec n) : setWidth n x = x := by grind theorem setWidth_zero (m n : Nat) : setWidth m 0#n = 0#m := by grind /-- Moves one-sided left toNat equality to BitVec equality. -/ theorem toNat_eq_nat {x : BitVec w} {y : Nat} : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by apply Iff.intro · intro eq simp [←eq, x.isLt] · intro eq simp [Nat.mod_eq_of_lt, eq] grind_pattern toNat_eq_nat => BitVec.ofNat w y, x.toNat /-- Moves one-sided right toNat equality to BitVec equality. -/ theorem nat_eq_toNat {x : BitVec w} {y : Nat} : (y = x.toNat) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by grind theorem getElem?_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) : (setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none := by grind theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) : (x.setWidth m)[i]? = if i < m then some (x.getLsbD i) else none := by grind theorem getLsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) : getLsbD (setWidth' ge x) i = getLsbD x i := by grind theorem getMsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) : getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by grind (splits := 10) theorem getLsbD_setWidth (m : Nat) (x : BitVec n) (i : Nat) : getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by grind theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} : getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by unfold setWidth by_cases h : n ≤ m <;> grind -- This is a simp lemma as there is only a runtime difference between `setWidth'` and `setWidth`, -- and for verification purposes they are equivalent. theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by apply eq_of_toNat_eq rw [toNat_setWidth, toNat_setWidth'] rw [Nat.mod_eq_of_lt] exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (Nat.zero_lt_two) h) theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) : (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by grind (splits := 12) theorem cast_setWidth (h : v = v') (x : BitVec w) : (x.setWidth v).cast h = x.setWidth v' := by grind theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) : (x.setWidth l).setWidth k = x.setWidth k := by grind theorem setWidth_cast {x : BitVec w} {h : w = v} : (x.cast h).setWidth k = x.setWidth k := by grind theorem msb_setWidth (x : BitVec w) : (x.setWidth v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by grind [msb_eq_getLsbD_last] theorem msb_setWidth' (x : BitVec w) (h : w ≤ v) : (x.setWidth' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by grind theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k := by grind /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/ theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) : x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by grind /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/ theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) : (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by ext i h have hv := (@Nat.testBit_one_eq_true_iff_self_eq_zero i) grind /-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/ theorem setWidth_one {x : BitVec w} : x.setWidth 1 = ofBool (x.getLsbD 0) := by grind theorem setWidth_ofNat_of_le (h : v ≤ w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x := by apply BitVec.eq_of_toNat_eq simp only [toNat_setWidth, toNat_ofNat] rw [Nat.mod_mod_of_dvd] exact Nat.pow_dvd_pow_iff_le_right'.mpr h /-- Iterated `setWidth` agrees with the second `setWidth` except in the case the first `setWidth` is a non-trivial truncation, and the second `setWidth` is a non-trivial extension. -/ -- Note that in the special cases `v = u` or `v = w`, -- `simp` can discharge the side condition itself. theorem setWidth_setWidth {x : BitVec u} {w v : Nat} (h : ¬ (v < u ∧ v < w)) : setWidth w (setWidth v x) = setWidth w x := by grind theorem msb_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} : (setWidth' (by omega : m ≤ n) x).msb = false := by grind theorem toInt_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} : (setWidth' (by omega : m ≤ n) x).toInt = x.toNat := by grind [toInt_eq_toNat_of_msb] theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} : (setWidth' p x).toInt = if m = n then x.toInt else x.toNat := by grind theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) : (setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by ext grind [Nat.mod_eq_of_lt] /-! ## extractLsb -/ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) : extractLsb hi lo (@BitVec.ofFin n x) = .ofNat (hi-lo+1) (x.val >>> lo) := rfl protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by ext i grind [BitVec.ofNat] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) : (extractLsb' s m x).toNat = (x.toNat >>> s) % 2^m := rfl theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) : (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by simp [extractLsb', toInt_ofNat'] theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by simp [extractLsb] theorem toFin_extractLsb' {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toFin = Fin.ofNat (2 ^ m) (x.toNat >>> s) := by simp [extractLsb'] theorem toFin_extractLsb {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toFin = Fin.ofNat (2 ^ (hi - lo + 1)) (x.toNat >>> lo) := by simp [extractLsb] theorem getElem_extractLsb' {start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) : (extractLsb' start len x)[i] = x.getLsbD (start+i) := by grind [getElem_eq_testBit_toNat, getLsbD] theorem getLsbD_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) : (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by grind [getLsbD] /-- Get the most significant bit after `extractLsb'`. With `extractLsb'`, we extract a `BitVec len` `x'` with length `len` from `BitVec w` `x`, starting from the element at position `start`. The function `getMsb` extracts a bit counting from the most significant bit. Assuming certain conditions, `(@extractLsbD' w x start len).getMsbD i` is equal to `@getMsbD w x (w - (start + len - i))`. Example (w := 10, start := 3, len := 4): |---| = w - (start + len) = 3 |start + len| = 7 |start| = 3 | len | = 4 let x = 9 8 7 6 5 4 3 2 1 0 let x' = x.extractLsb' 3 4 = 6 5 4 3 | | | x'.getMsbD 1 = x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 1) = 4) | x'.getMsbD 0 = x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 0) = 3) # Condition 1: `i < len` The index `i` must be within the range of `len`. # Condition 2: `start + len - i ≤ w` If `start + len` is larger than `w`, the high bits at `i` with `w ≤ i` are filled with 0, meaning that `getMsbD[i] = false` for these `i`. If `i` is large enough, `getMsbD[i]` is again within the bounds `x`. The precise condition is: `start + len - i ≤ w` Example (w := 10, start := 7, len := 5): |= w - (start + len) = 0 | start + len | = 12 | start | = 7 | len | = 5 let x = 9 8 7 6 5 4 3 2 1 0 let x' = x.extractLsb' 7 5 = _ _ 9 8 7 | | | x'.getMsbD (i := 2) = | x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 2)) = | x.getMsbD 0 | ✅ start + len - i ≤ w | 7 + 5 - 2 = 10 ≤ 10 | x'.getMsbD (i := 0) = x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 0)) = x.getMsbD (i := w - (start + len - i) = x.getMsbD (i := -2) -- in Nat becomes 0 ❌ start + len - i ≤ w 7 + 5 - 0 ≤ w -/ theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} : (extractLsb' start len x).getMsbD i = (decide (i < len) && (decide (start + len - i ≤ w) && x.getMsbD (w - (start + len - i)))) := by grind (splits := 13) theorem msb_extractLsb' {start len : Nat} {x : BitVec w} : (extractLsb' start len x).msb = (decide (0 < len) && (decide (start + len ≤ w) && x.getMsbD (w - (start + len)))) := by simp [BitVec.msb] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) : (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by grind [getElem_eq_testBit_toNat, getLsbD] theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) : getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by grind theorem getLsbD_extractLsb {hi lo : Nat} {x : BitVec n} {i : Nat} : (extractLsb hi lo x).getLsbD i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by grind theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} : (extractLsb hi lo x).getMsbD i = (decide (i < hi - lo + 1) && (decide (max hi lo - i < w) && x.getMsbD (w - 1 - (max hi lo - i)))) := by grind (splits := 14) theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} : (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by simp [BitVec.msb] theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) : x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by grind /-- Extracting all the bits of a bitvector is an identity operation. -/ theorem extractLsb'_eq_self {x : BitVec w} : x.extractLsb' 0 w = x := by grind theorem getLsbD_eq_extractLsb' (x : BitVec w) (i : Nat) : x.getLsbD i = (x.extractLsb' i 1 == 1#1) := by rw [Bool.eq_iff_iff] simp [BitVec.eq_of_getLsbD_eq_iff] theorem getElem_eq_extractLsb' (x : BitVec w) (i : Nat) (h : i < w) : x[i] = (x.extractLsb' i 1 == 1#1) := by rw [← getLsbD_eq_getElem, getLsbD_eq_extractLsb'] theorem extractLsb'_zero {w start len : Nat} : (0#w).extractLsb' start len = 0#len := by grind theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} : x.extractLsb' start 0 = 0#0 := by grind /-! ### allOnes -/ theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by grind [allOnes] theorem toInt_allOnes : (allOnes w).toInt = if 0 < w then -1 else 0 := by by_cases h : w = 0 · grind · have : 1 < 2 ^ w := by simp [h] grind [BitVec.toInt] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat (2^w) (2^w - 1) := by ext simp theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by simp [allOnes] theorem getMsbD_allOnes : (allOnes v).getMsbD i = decide (i < v) := by grind theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true := by grind [getElem_eq_testBit_toNat] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by ext simp only [Fin.rev, getElem_ofFin, getElem_allOnes] rw [Fin.add_def] simp only [Nat.testBit_mod_two_pow] have h : (x : Nat) + (2 ^ n - (x + 1)) = 2 ^ n - 1 := by omega rw [h, Nat.testBit_two_pow_sub_one] grind theorem msb_allOnes (hw : 0 < w) : (allOnes w).msb = true := by grind /-! ### or -/ theorem toNat_or (x y : BitVec v) : BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y := rfl theorem toInt_or (x y : BitVec w) : BitVec.toInt (x ||| y) = Int.bmod (BitVec.toNat x ||| BitVec.toNat y) (2^w) := by rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] grind theorem toFin_or (x y : BitVec v) : BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by ext exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm theorem getLsbD_or {x y : BitVec v} : (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i) := by grind [testBit_toNat, getLsbD] theorem getMsbD_or {x y : BitVec w} : (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i) := by grind theorem getElem_or {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i]) := by grind [getElem_eq_testBit_toNat] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by grind theorem setWidth_or {x y : BitVec w} : (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by grind theorem or_assoc (x y z : BitVec w) : x ||| y ||| z = x ||| (y ||| z) := by grind instance : Std.Associative (α := BitVec n) (· ||| ·) := ⟨BitVec.or_assoc⟩ theorem or_comm (x y : BitVec w) : x ||| y = y ||| x := by grind instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩ theorem or_self {x : BitVec w} : x ||| x = x := by grind instance : Std.IdempotentOp (α := BitVec n) (· ||| · ) where idempotent _ := BitVec.or_self theorem or_zero {x : BitVec w} : x ||| 0#w = x := by grind instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where right_id _ := BitVec.or_zero theorem zero_or {x : BitVec w} : 0#w ||| x = x := by grind theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by grind theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by grind theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by grind theorem or_eq_zero_iff {x y : BitVec w} : (x ||| y) = 0#w ↔ x = 0#w ∧ y = 0#w := by grind theorem extractLsb'_or {x y : BitVec w} {start len : Nat} : (x ||| y).extractLsb' start len = (x.extractLsb' start len) ||| (y.extractLsb' start len) := by grind theorem extractLsb_or {x : BitVec w} {hi lo : Nat} : (x ||| y).extractLsb lo hi = (x.extractLsb lo hi) ||| (y.extractLsb lo hi) := by grind theorem ofNat_or {x y : Nat} : BitVec.ofNat w (x ||| y) = BitVec.ofNat w x ||| BitVec.ofNat w y := eq_of_toNat_eq (by simp [Nat.or_mod_two_pow]) /-! ### and -/ theorem toNat_and (x y : BitVec v) : BitVec.toNat (x &&& y) = BitVec.toNat x &&& BitVec.toNat y := rfl theorem toInt_and (x y : BitVec w) : BitVec.toInt (x &&& y) = Int.bmod (BitVec.toNat x &&& BitVec.toNat y) (2^w) := by rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))] omega theorem toFin_and (x y : BitVec v) : BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by apply Fin.eq_of_val_eq exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm theorem getLsbD_and {x y : BitVec v} : (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i) := by grind [testBit_toNat, getLsbD] theorem getMsbD_and {x y : BitVec w} : (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i) := by grind theorem getElem_and {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i]) := by grind [getElem_eq_testBit_toNat] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by grind theorem setWidth_and {x y : BitVec w} : (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by grind theorem and_assoc (x y z : BitVec w) : x &&& y &&& z = x &&& (y &&& z) := by grind instance : Std.Associative (α := BitVec n) (· &&& ·) := ⟨BitVec.and_assoc⟩ theorem and_comm (x y : BitVec w) : x &&& y = y &&& x := by grind instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩ theorem and_self {x : BitVec w} : x &&& x = x := by grind instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where idempotent _ := BitVec.and_self theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by grind theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by grind theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by grind theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by grind instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where right_id _ := BitVec.and_allOnes theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by grind theorem and_eq_allOnes_iff {x y : BitVec w} : x &&& y = allOnes w ↔ x = allOnes w ∧ y = allOnes w := by grind theorem extractLsb'_and {x y : BitVec w} {start len : Nat} : (x &&& y).extractLsb' start len = (x.extractLsb' start len) &&& (y.extractLsb' start len) := by grind theorem extractLsb_and {x : BitVec w} {hi lo : Nat} : (x &&& y).extractLsb lo hi = (x.extractLsb lo hi) &&& (y.extractLsb lo hi) := by grind theorem ofNat_and {x y : Nat} : BitVec.ofNat w (x &&& y) = BitVec.ofNat w x &&& BitVec.ofNat w y := eq_of_toNat_eq (by simp [Nat.and_mod_two_pow]) /-! ### xor -/ theorem toNat_xor (x y : BitVec v) : BitVec.toNat (x ^^^ y) = BitVec.toNat x ^^^ BitVec.toNat y := rfl theorem toInt_xor (x y : BitVec w) : BitVec.toInt (x ^^^ y) = Int.bmod (BitVec.toNat x ^^^ BitVec.toNat y) (2^w) := by rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] omega theorem toFin_xor (x y : BitVec v) : BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by apply Fin.eq_of_val_eq exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm theorem getLsbD_xor {x y : BitVec v} : (x ^^^ y).getLsbD i = ((x.getLsbD i) ^^ (y.getLsbD i)) := by grind [testBit_toNat, getLsbD] theorem getMsbD_xor {x y : BitVec w} : (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i) := by grind theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i]) := by grind [getElem_eq_testBit_toNat] theorem msb_xor {x y : BitVec w} : (x ^^^ y).msb = (x.msb ^^ y.msb) := by grind theorem setWidth_xor {x y : BitVec w} : (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by grind theorem xor_assoc (x y z : BitVec w) : x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by grind instance : Std.Associative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_assoc⟩ theorem xor_comm (x y : BitVec w) : x ^^^ y = y ^^^ x := by grind instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩ theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by grind theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by grind instance : Std.LawfulCommIdentity (α := BitVec n) (· ^^^ · ) (0#n) where right_id _ := BitVec.xor_zero theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by grind theorem xor_left_inj {x y : BitVec w} (z : BitVec w) : (x ^^^ z = y ^^^ z) ↔ x = y := by constructor · intro h ext i ih have := BitVec.eq_of_getElem_eq_iff.mp h i simp only [getElem_xor, Bool.xor_left_inj] at this exact this ih · grind theorem xor_right_inj {x y : BitVec w} (z : BitVec w) : (z ^^^ x = z ^^^ y) ↔ x = y := by grind [xor_comm, xor_left_inj] theorem xor_eq_zero_iff {x y : BitVec w} : (x ^^^ y = 0#w) ↔ x = y := by constructor · intro h apply (xor_left_inj y).mp grind · grind theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by grind theorem extractLsb'_xor {x y : BitVec w} {start len : Nat} : (x ^^^ y).extractLsb' start len = (x.extractLsb' start len) ^^^ (y.extractLsb' start len) := by grind theorem extractLsb_xor {x : BitVec w} {hi lo : Nat} : (x ^^^ y).extractLsb lo hi = (x.extractLsb lo hi) ^^^ (y.extractLsb lo hi) := by grind theorem ofNat_xor {x y : Nat} : BitVec.ofNat w (x ^^^ y) = BitVec.ofNat w x ^^^ BitVec.ofNat w y := eq_of_toNat_eq (by simp [Nat.xor_mod_two_pow]) /-! ### not -/ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl @[simp, bitvec_to_nat] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor] apply Nat.eq_of_testBit_eq intro i simp only [toNat_allOnes, Nat.testBit_xor, Nat.testBit_two_pow_sub_one] match h : BitVec.toNat x with | 0 => simp | y+1 => rw [Nat.succ_eq_add_one] at h rw [← h] rw [Nat.testBit_two_pow_sub_succ (isLt _)] · cases w : decide (i < v) · simp only [decide_eq_false_iff_not, Nat.not_lt] at w simp only [Bool.false_bne, Bool.false_and] rw [Nat.testBit_lt_two_pow] calc BitVec.toNat x < 2 ^ v := isLt _ _ ≤ 2 ^ i := Nat.pow_le_pow_right Nat.zero_lt_two w · grind theorem toInt_not {x : BitVec w} : (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w) := by rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def] simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega, -Int.natCast_pow] rw_mod_cast [Nat.mod_eq_of_lt (by omega)] omega theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} : BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLT, toNat_not, toNat_ofNat] cases h : Int.negSucc n % ((2 ^ w : Nat) : Int) case ofNat => rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h · dsimp only omega · omega case negSucc a => have neg := Int.negSucc_lt_zero a have _ : 0 ≤ Int.negSucc n % ((2 ^ w : Nat) : Int) := Int.emod_nonneg _ (by omega) omega theorem toFin_not (x : BitVec w) : (~~~x).toFin = x.toFin.rev := by apply Fin.val_inj.mp grind theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by grind [not_def] theorem getMsbD_not {x : BitVec v} : (~~~x).getMsbD i = (decide (i < v) && ! x.getMsbD i) := by grind theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i] := by grind [getElem_eq_testBit_toNat] theorem setWidth_not {x : BitVec w} (_ : k ≤ w) : (~~~x).setWidth k = ~~~(x.setWidth k) := by grind theorem not_zero : ~~~(0#n) = allOnes n := by grind theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by grind theorem not_allOnes : ~~~ allOnes w = 0#w := by grind theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by grind theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by grind theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by grind protected theorem not_inj {x y : BitVec w} : ~~~x = ~~~y ↔ x = y := ⟨fun h => by rw [← @not_not w x, ← @not_not w y, h], congrArg _⟩ theorem and_not_self (x : BitVec w) : x &&& ~~~x = 0 := by grind theorem not_and_self (x : BitVec w) : ~~~x &&& x = 0 := by grind theorem or_not_self (x : BitVec w) : x ||| ~~~x = allOnes w := by grind theorem not_or_self (x : BitVec w) : ~~~x ||| x = allOnes w := by grind theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by grind theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by grind /-- Negating `x` and then extracting [start..start+len) is the same as extracting and then negating, as long as the range [start..start+len) is in bounds. See that if the index is out-of-bounds, then `extractLsb` will return `false`, which makes the operation not commute. -/ theorem extractLsb'_not_of_lt {x : BitVec w} {start len : Nat} (h : start + len < w) : (~~~ x).extractLsb' start len = ~~~ (x.extractLsb' start len) := by grind /-- Negating `x` and then extracting [lo:hi] is the same as extracting and then negating. For the extraction to be well-behaved, we need the range [lo:hi] to be a valid closed interval inside the bitvector: 1. `lo ≤ hi` for the interval to be a well-formed closed interval. 2. `hi < w`, for the interval to be contained inside the bitvector. -/ theorem extractLsb_not_of_lt {x : BitVec w} {hi lo : Nat} (hlo : lo ≤ hi) (hhi : hi < w) : (~~~ x).extractLsb hi lo = ~~~ (x.extractLsb hi lo) := by grind theorem ne_not_self {a : BitVec w} (h : 0 < w) : a ≠ ~~~a := by have : ∃ x, x < w := ⟨w - 1, by omega⟩ simp [BitVec.eq_of_getElem_eq_iff, this] theorem not_self_ne {a : BitVec w} (h : 0 < w) : ~~~a ≠ a := by grind [ne_not_self] theorem not_and {x y : BitVec w} : ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by grind theorem not_or {x y : BitVec w} : ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by grind theorem not_xor_left {x y : BitVec w} : ~~~ (x ^^^ y) = ~~~ x ^^^ y := by grind theorem not_xor_right {x y : BitVec w} : ~~~ (x ^^^ y) = x ^^^ ~~~ y := by grind /-! ### cast -/ theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h := by grind theorem and_cast {x y : BitVec w} (h : w = w') : x.cast h &&& y.cast h = (x &&& y).cast h := by grind theorem or_cast {x y : BitVec w} (h : w = w') : x.cast h ||| y.cast h = (x ||| y).cast h := by grind theorem xor_cast {x y : BitVec w} (h : w = w') : x.cast h ^^^ y.cast h = (x ^^^ y).cast h := by grind /-! ### shiftLeft -/ @[simp, bitvec_to_nat] theorem toNat_shiftLeft {x : BitVec v} : (x <<< n).toNat = x.toNat <<< n % 2^v := BitVec.toNat_ofNat _ _ theorem toInt_shiftLeft {x : BitVec w} : (x <<< n).toInt = (x.toNat <<< n : Int).bmod (2^w) := by grind [toInt_eq_toNat_bmod, Int.emod_bmod] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) : (x <<< n).toFin = Fin.ofNat (2^w) (x.toNat <<< n) := rfl theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by apply eq_of_toNat_eq grind [toNat_mod_cancel] theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by simp [bitvec_to_nat] theorem getLsbD_shiftLeft (x : BitVec m) (n) : getLsbD (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsbD x (i - n)) := by grind [getLsbD] theorem getElem_shiftLeft {x : BitVec m} {n : Nat} (h : i < m) : (x <<< n)[i] = (!decide (i < n) && x[i - n]) := by grind [getElem_eq_testBit_toNat] theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) : (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by grind theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) : (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by grind theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) : (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by grind theorem getMsbD_shiftLeft (x : BitVec w) (i) : (x <<< i).getMsbD k = x.getMsbD (k + i) := by grind theorem shiftLeftZeroExtend_eq {x : BitVec w} : shiftLeftZeroExtend x n = setWidth (w+n) x <<< n := by apply eq_of_toNat_eq rw [shiftLeftZeroExtend, setWidth] split · simp only [toNat_ofNatLT, toNat_shiftLeft, toNat_setWidth'] rw [Nat.mod_eq_of_lt] rw [Nat.shiftLeft_eq, Nat.pow_add] exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _) · grind theorem toNat_shiftLeftZeroExtend {x : BitVec w} : (shiftLeftZeroExtend x n).toNat = x.toNat <<< n := by rcases n with _|n · grind [shiftLeftZeroExtend] · simp only [shiftLeftZeroExtend_eq, toNat_shiftLeft, toNat_setWidth] have := Nat.pow_lt_pow_of_lt (a := 2) (n := w) (m := w + (n + 1)) (by omega) (by omega) have : x.toNat <<< (n + 1) < 2 ^ (w + (n + 1)) := by rw [Nat.shiftLeft_eq, Nat.pow_add (m := w) (n := n + 1), Nat.mul_lt_mul_right (by apply Nat.two_pow_pos (w := n + 1))] grind rw [Nat.mod_eq_of_lt (by rw [Nat.mod_eq_of_lt (by omega)]; omega), Nat.mod_eq_of_lt (by omega)] theorem toInt_shiftLeftZeroExtend {x : BitVec w} : (shiftLeftZeroExtend x n).toInt = x.toInt * 2 ^ n := by rw [shiftLeftZeroExtend_eq] rcases w with _|w · simp [of_length_zero] · rcases n with _|n · simp · have := Nat.pow_pos (a := 2) (n := n + 1) (by omega) have : x.toNat <<< (n + 1) < 2 ^ (w + 1 + (n + 1)) := by rw [Nat.shiftLeft_eq, Nat.pow_add (a := 2) (m := w + 1) (n := n + 1), Nat.mul_lt_mul_right (by omega)] omega simp only [toInt_shiftLeft, toNat_setWidth, Nat.lt_add_right_iff_pos, Nat.zero_lt_succ, toNat_mod_cancel_of_lt, Int.bmod_def] by_cases hmsb : x.msb · have hge := toNat_ge_of_msb_true hmsb simp only [Nat.add_one_sub_one, ge_iff_le] at hge rw [Int.emod_eq_of_lt (by norm_cast; rw [Nat.shiftLeft_eq]; omega) (by omega)] rw_mod_cast [← Nat.add_assoc] rw [show (2 ^ (w + 1 + n + 1) + 1) / 2 = 2 ^ (w + 1 + n) by omega, Int.natCast_pow, Int.cast_ofNat_Int, Nat.shiftLeft_eq, Nat.add_assoc, Nat.pow_add (a := 2) (m := w) (n := 1 + n), Nat.add_comm 1 n] simp only [Nat.mul_lt_mul_right (by omega), show ¬x.toNat < 2 ^ w by omega, reduceIte, Int.natCast_mul, Int.natCast_pow, Int.cast_ofNat_Int, toInt_eq_toNat_cond, show ¬2 * x.toNat < 2 ^ (w + 1) by simp [Nat.pow_add, Nat.mul_comm (2 ^ w) 2, hge]] norm_cast simp [Int.natCast_mul, Int.natCast_pow, Int.cast_ofNat_Int, Int.sub_mul, show w + (n + 1) + 1 = (w + 1) + (n + 1) by omega, Nat.pow_add] · simp only [Bool.not_eq_true] at hmsb have hle := toNat_lt_of_msb_false (x := x) hmsb simp only [Nat.add_one_sub_one] at hle rw [Int.emod_eq_of_lt (by norm_cast; rw [Nat.shiftLeft_eq]; omega) (by omega)] rw_mod_cast [← Nat.add_assoc] rw [show (2 ^ (w + 1 + n + 1) + 1) / 2 = 2 ^ (w + 1 + n) by omega, Int.natCast_pow, Int.cast_ofNat_Int, Nat.shiftLeft_eq, Nat.add_assoc, Nat.pow_add (a := 2) (m := w) (n := 1 + n), Nat.add_comm 1 n] simp [Nat.mul_lt_mul_right (b := x.toNat) (c := 2 ^ w) (a := 2 ^ (n + 1)) (by omega), hle, reduceIte, Int.natCast_mul, Int.natCast_pow, Int.cast_ofNat_Int, toInt_eq_toNat_of_msb hmsb] theorem toFin_shiftLeftZeroExtend {x : BitVec w} : (shiftLeftZeroExtend x n).toFin = Fin.ofNat (2 ^ (w + n)) (x.toNat * 2 ^ n) := by rcases w with _|w · simp [of_length_zero, shiftLeftZeroExtend_eq] · have := Nat.pow_le_pow_of_le (a := 2) (n := w + 1) (m := w + 1 + n) (by omega) (by omega) rw [shiftLeftZeroExtend_eq, toFin_shiftLeft, toNat_setWidth, Nat.mod_eq_of_lt (by omega), Nat.shiftLeft_eq] theorem getElem_shiftLeftZeroExtend {x : BitVec m} {n : Nat} (h : i < m + n) : (shiftLeftZeroExtend x n)[i] = if h' : i < n then false else x[i - n] := by grind theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) : getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n)) := by grind theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) : getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by grind (splits := 11) theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) : (shiftLeftZeroExtend x i).msb = x.msb := by grind theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) : x <<< (n + m) = (x <<< n) <<< m := by grind theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by grind theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by grind theorem setWidth_shiftLeft_of_le {x : BitVec w} {y : Nat} (hi : i ≤ w) : (x <<< y).setWidth i = x.setWidth i <<< y := by grind /-! ### shiftLeft reductions from BitVec to Nat -/ theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := rfl theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp theorem shiftLeft_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} : x <<< y <<< z = x <<< (y.toNat + z.toNat) := by simp [shiftLeft_add] theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} : (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by grind theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) : (x <<< y)[i] = (!decide (i < y.toNat) && x[i - y.toNat]) := by grind theorem shiftLeft_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w := by grind theorem shiftLeft_ofNat_eq {x : BitVec w} {k : Nat} : x <<< (BitVec.ofNat w k) = x <<< (k % 2^w) := rfl /-! ### ushiftRight -/ @[simp, bitvec_to_nat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) : (x >>> i).toNat = x.toNat >>> i := rfl theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) : getLsbD (x >>> i) j = getLsbD x (i+j) := by grind [getLsbD] theorem getElem_ushiftRight (x : BitVec w) (i n : Nat) (h : i < w) : (x >>> n)[i] = x.getLsbD (n + i) := by grind [getElem_eq_testBit_toNat, getLsbD] theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) : (x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n) := by grind theorem ushiftRight_and_distrib (x y : BitVec w) (n : Nat) : (x &&& y) >>> n = (x >>> n) &&& (y >>> n) := by grind theorem ushiftRight_or_distrib (x y : BitVec w) (n : Nat) : (x ||| y) >>> n = (x >>> n) ||| (y >>> n) := by grind theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by simp [bitvec_to_nat] theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by simp [bitvec_to_nat] /-- Shifting right by `n < w` yields a bitvector whose value is less than `2 ^ (w - n)`. -/ theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) : (x >>> n).toNat < 2 ^ (w - n) := by rw [toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul] · rw [Nat.pow_sub_mul_pow] · apply x.isLt · apply hn · apply Nat.pow_pos (by decide) /-- Shifting right by `n`, which is larger than the bitwidth `w` produces `0. -/ theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x >>> n = 0#w := by simp only [toNat_eq, toNat_ushiftRight, toNat_ofNat, Nat.zero_mod] have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)] /-- Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree, because it makes the value of the bitvector less than or equal to `2^(w-1)`. -/ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) : (x >>> n).toInt = x.toNat >>> n := by rw [toInt_eq_toNat_cond] simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt] intro h by_cases hn : n ≤ w · have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1 have : 2 ^ (w - n).succ ≤ 2^ w := Nat.pow_le_pow_of_le (by decide) (by omega) have := show 2 * x.toNat >>> n < 2 ^ w by omega omega · have : x.toNat >>> n = 0 := by apply Nat.shiftRight_eq_zero have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le (by decide) (by omega) omega simp [this] at h /-- Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree, because it makes the value of the bitvector less than or equal to `2^(w-1)`. In the case when `n = 0`, then the shift right value equals the integer interpretation. -/ theorem toInt_ushiftRight {x : BitVec w} {n : Nat} : (x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n := by grind [toInt_ushiftRight_of_lt] theorem toFin_ushiftRight {x : BitVec w} {n : Nat} : (x >>> n).toFin = x.toFin / (Fin.ofNat (2^w) (2^n)) := by apply Fin.eq_of_val_eq by_cases hn : n < w · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)] · simp only [Nat.not_lt] at hn rw [ushiftRight_eq_zero (by omega)] simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)] theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n))) := by grind (splits := 11) theorem msb_ushiftRight {x : BitVec w} {n : Nat} : (x >>> n).msb = (!decide (0 < n) && x.msb) := by grind theorem setWidth_ushiftRight {x : BitVec w} {y : Nat} (hi : w ≤ i) : (x >>> y).setWidth i = x.setWidth i >>> y := by grind /-! ### ushiftRight reductions from BitVec to Nat -/ theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) : x >>> y = x >>> y.toNat := rfl theorem ushiftRight_ofNat_eq {x : BitVec w} {k : Nat} : x >>> (BitVec.ofNat w k) = x >>> (k % 2^w) := rfl theorem ushiftRight_self (n : BitVec w) : n >>> n.toNat = 0#w := by simp [BitVec.toNat_eq, Nat.shiftRight_eq_div_pow, Nat.lt_two_pow_self, Nat.div_eq_of_lt] /-! ### sshiftRight -/ theorem sshiftRight_eq {x : BitVec n} {i : Nat} : x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i) := by grind [BitVec.sshiftRight] /-- if the msb is false, the arithmetic shift right equals logical shift right -/ @[local grind =] theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) : (x.sshiftRight s) = x >>> s := by apply BitVec.eq_of_toNat_eq rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond] have hxbound : 2 * x.toNat < 2 ^ w := BitVec.msb_eq_false_iff_two_mul_lt.mp h simp only [hxbound, ↓reduceIte, Int.natCast_shiftRight, ofInt_natCast, toNat_ofNat, toNat_ushiftRight] replace hxbound : x.toNat >>> s < 2 ^ w := by rw [Nat.shiftRight_eq_div_pow] exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt apply Nat.mod_eq_of_lt hxbound /-- If the msb is `true`, the arithmetic shift right equals negating, then logical shifting right, then negating again. The double negation preserves the lower bits that have been shifted, and the outer negation ensures that the high bits are '1'. -/ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) : (x.sshiftRight s) = ~~~((~~~x) >>> s) := by apply BitVec.eq_of_toNat_eq rcases w with rfl | w · simp [toNat_of_zero_length] · rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond] have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := BitVec.msb_eq_true_iff_two_mul_ge.mp h replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega simp only [hxbound, ↓reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight] rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega), Nat.pred_eq_sub_one, Int.negSucc_shiftRight, Int.emod_negSucc, Int.natAbs_natCast, Nat.succ_eq_add_one, Int.subNatNat_of_le (by omega), Int.toNat_natCast, Nat.mod_eq_of_lt, Nat.sub_right_comm] omega · rw [Nat.shiftRight_eq_div_pow] apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega) theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) : getLsbD (x.sshiftRight s) i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb) := by grind theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) : (x.sshiftRight s)[i] = (if h : s + i < w then x[s + i] else x.msb) := by rw [← getLsbD_eq_getElem] grind theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) : (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by grind theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) : (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n) := by grind theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) : (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n) := by grind theorem sshiftRight'_ofNat_eq_sshiftRight {x : BitVec w} {k : Nat} : x.sshiftRight' (BitVec.ofNat w k) = x.sshiftRight (k % 2^w) := rfl /-- The msb after arithmetic shifting right equals the original msb. -/ theorem msb_sshiftRight {n : Nat} {x : BitVec w} : (x.sshiftRight n).msb = x.msb := by grind (splits := 11) theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by grind theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by grind theorem sshiftRight_add {x : BitVec w} {m n : Nat} : x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by grind (splits := 15) theorem not_sshiftRight {b : BitVec w} : ~~~b.sshiftRight n = (~~~b).sshiftRight n := by grind theorem not_sshiftRight_not {x : BitVec w} {n : Nat} : ~~~((~~~x).sshiftRight n) = x.sshiftRight n := by grind theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by grind (splits := 16) theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} : x.toInt >>> n < 2 ^ (w - 1) := by have := @Int.shiftRight_le_of_nonneg x.toInt n have := @Int.shiftRight_le_of_nonpos x.toInt n have := @BitVec.toInt_lt w x have := @Nat.one_le_two_pow (w-1) norm_cast at * grind theorem le_toInt_shiftRight {x : BitVec w} {n : Nat} : -(2 ^ (w - 1)) ≤ x.toInt >>> n := by have := @Int.le_shiftRight_of_nonpos x.toInt n have := @Int.le_shiftRight_of_nonneg x.toInt n have := @BitVec.le_toInt w x have := @Nat.one_le_two_pow (w-1) norm_cast at * grind theorem toFin_sshiftRight_of_msb_true {x : BitVec w} {n : Nat} (h : x.msb = true) : (x.sshiftRight n).toFin = Fin.ofNat (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) := by apply Fin.eq_of_val_eq simp only [val_toFin, toNat_sshiftRight, h, ↓reduceIte, Fin.val_ofNat] rw [Nat.mod_eq_of_lt] grind theorem toFin_sshiftRight_of_msb_false {x : BitVec w} {n : Nat} (h : x.msb = false) : (x.sshiftRight n).toFin = Fin.ofNat (2^w) (x.toNat >>> n) := by apply Fin.eq_of_val_eq simp only [val_toFin, toNat_sshiftRight, h, Bool.false_eq_true, ↓reduceIte, Fin.val_ofNat] have := Nat.shiftRight_le x.toNat n rw [Nat.mod_eq_of_lt (by omega)] theorem toFin_sshiftRight {x : BitVec w} {n : Nat} : (x.sshiftRight n).toFin = if x.msb then Fin.ofNat (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) else Fin.ofNat (2^w) (x.toNat >>> n) := by grind [toFin_sshiftRight_of_msb_true, toFin_sshiftRight_of_msb_false] theorem toInt_sshiftRight {x : BitVec w} {n : Nat} : (x.sshiftRight n).toInt = x.toInt >>> n := by by_cases h : w = 0 · subst h simp [BitVec.eq_nil x] · rw [sshiftRight, toInt_ofInt, ←Nat.two_pow_pred_add_two_pow_pred (by omega)] have := @toInt_shiftRight_lt w x n have := @le_toInt_shiftRight w x n norm_cast at * exact Int.bmod_eq_of_le (by omega) (by omega) /-! ### sshiftRight reductions from BitVec to Nat -/ theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl theorem toNat_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) : (x.sshiftRight' y).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat := by rw [sshiftRight_eq', toNat_sshiftRight_of_msb_true h] theorem toNat_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) : (x.sshiftRight' y).toNat = x.toNat >>> y.toNat := by rw [sshiftRight_eq', toNat_sshiftRight_of_msb_false h] theorem toNat_sshiftRight' {x y : BitVec w} : (x.sshiftRight' y).toNat = if x.msb then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat else x.toNat >>> y.toNat := by rw [sshiftRight_eq', toNat_sshiftRight] theorem toFin_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) : (x.sshiftRight' y).toFin = Fin.ofNat (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) := by rw [sshiftRight_eq', toFin_sshiftRight_of_msb_true h] theorem toFin_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) : (x.sshiftRight' y).toFin = Fin.ofNat (2^w) (x.toNat >>> y.toNat) := by rw [sshiftRight_eq', toFin_sshiftRight_of_msb_false h] theorem toFin_sshiftRight' {x y : BitVec w} : (x.sshiftRight' y).toFin = if x.msb then Fin.ofNat (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) else Fin.ofNat (2^w) (x.toNat >>> y.toNat) := by rw [sshiftRight_eq', toFin_sshiftRight] theorem toInt_sshiftRight' {x y : BitVec w} : (x.sshiftRight' y).toInt = x.toInt >>> y.toNat := by grind -- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form. theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by grind -- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form. theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) : (x.sshiftRight' y)[i] = (if h : y.toNat + i < w then x[y.toNat + i] else x.msb) := by grind theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by grind theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by simp /-! ### signExtend -/ /-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat` -/ private theorem Int.ofNat_sub_ofNat_of_lt {n m : Nat} (hlt : n < m) : (n : Int) - (m : Int) = -(↑(m - 1 - n) + 1) := by omega /-- Equation theorem for `Int.mod` -/ private theorem Int.negSucc_emod (m : Nat) (n : Int) : -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl /-- The sign extension is the same as zero extending when `msb = false`. -/ theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) : x.signExtend v = x.setWidth v := by grind [signExtend] /-- The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not when `msb = true`. The double bitwise not ensures that the high bits are '1', and the lower bits are preserved. -/ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) : x.signExtend v = ~~~((~~~x).setWidth v) := by apply BitVec.eq_of_toNat_eq simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not, toNat_setWidth, hmsb, ↓reduceIte] norm_cast rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod] simp only [Int.natAbs_natCast] rw [Int.subNatNat_of_le] · rw [Int.toNat_natCast, Nat.add_comm, Nat.sub_add_eq] · apply Nat.le_trans · apply Nat.succ_le_of_lt apply Nat.mod_lt apply Nat.two_pow_pos · apply Nat.le_refl · omega theorem getLsbD_signExtend (x : BitVec w) {v i : Nat} : (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by grind [signExtend_eq_setWidth_of_msb_false, signExtend_eq_not_setWidth_not_of_msb_true] theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} : (x.signExtend v).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by grind (splits := 16) [signExtend_eq_setWidth_of_msb_false, signExtend_eq_not_setWidth_not_of_msb_true] theorem getElem_signExtend {x : BitVec w} {v i : Nat} (h : i < v) : (x.signExtend v)[i] = if h : i < w then x[i] else x.msb := by simp [←getLsbD_eq_getElem, getLsbD_signExtend, h] theorem msb_signExtend {x : BitVec w} : (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by grind (splits := 10) /-- Sign extending to a width smaller than the starting width is a truncation. -/ theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) : x.signExtend v = x.setWidth v := by grind /-- Sign extending to the same bitwidth is a no op. -/ theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by grind /-- Sign extending to a larger bitwidth depends on the msb. If the msb is false, then the result equals the original value. If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. -/ private theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) : (x.signExtend v).toNat = x.toNat + if x.msb then 2^v - 2^w else 0 := by apply Nat.eq_of_testBit_eq intro i have ⟨k, hk⟩ := Nat.exists_eq_add_of_le hv rw [hk, testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one, Nat.add_comm (x.toNat)] by_cases hx : x.msb · simp only [hx, ↓reduceIte, Nat.testBit_two_pow_mul_add _ x.isLt, Nat.testBit_two_pow_sub_one] grind · simp only [hx] grind [testBit_toNat] /-- Sign extending to a larger bitwidth depends on the msb. If the msb is false, then the result equals the original value. If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. -/ theorem toNat_signExtend (x : BitVec w) {v : Nat} : (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 := by by_cases h : v ≤ w · have : 2^v ≤ 2^w := Nat.pow_le_pow_right Nat.two_pos h simp [signExtend_eq_setWidth_of_le x h, toNat_setWidth, Nat.sub_eq_zero_of_le this] · have : 2^w ≤ 2^v := Nat.pow_le_pow_right Nat.two_pos (by omega) rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)] /-- If the current width `w` is smaller than the extended width `v`, then the value when interpreted as an integer does not change. -/ theorem toInt_signExtend_of_le {x : BitVec w} (h : w ≤ v) : (x.signExtend v).toInt = x.toInt := by by_cases hlt : w < v · rw [toInt_signExtend_of_lt hlt] · obtain rfl : w = v := by omega simp where toInt_signExtend_of_lt {x : BitVec w} (hv : w < v): (x.signExtend v).toInt = x.toInt := by simp only [toInt_eq_msb_cond, toNat_signExtend] have : (x.signExtend v).msb = x.msb := by grind have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega) simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod] by_cases h : x.msb <;> norm_cast <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow] omega /-- If the current width `w` is larger than the extended width `v`, then the value when interpreted as an integer is truncated, and we compute a modulo by `2^v`. -/ theorem toInt_signExtend_eq_toNat_bmod_of_le {x : BitVec w} (hv : v ≤ w) : (x.signExtend v).toInt = Int.bmod x.toNat (2^v) := by grind [signExtend_eq_setWidth_of_le] /-- Interpreting the sign extension of `(x : BitVec w)` to width `v` computes `x % 2^v` (where `%` is the balanced mod). See `toInt_signExtend` for a version stated in terms of `toInt` instead of `toNat`. -/ theorem toInt_signExtend_eq_toNat_bmod (x : BitVec w) : (x.signExtend v).toInt = Int.bmod x.toNat (2 ^ min v w) := by grind [toInt_signExtend_eq_toNat_bmod_of_le, toInt_signExtend_of_le] theorem toInt_signExtend (x : BitVec w) : (x.signExtend v).toInt = x.toInt.bmod (2 ^ min v w) := by rw [toInt_signExtend_eq_toNat_bmod, BitVec.toInt_eq_toNat_bmod, Int.bmod_bmod_of_dvd] exact Nat.pow_dvd_pow _ (Nat.min_le_right v w) theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) : (x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by grind [BitVec.toInt_signExtend] theorem toFin_signExtend_of_le {x : BitVec w} (hv : v ≤ w): (x.signExtend v).toFin = Fin.ofNat (2 ^ v) x.toNat := by grind [signExtend_eq_setWidth_of_le] theorem toFin_signExtend (x : BitVec w) : (x.signExtend v).toFin = Fin.ofNat (2 ^ v) (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0):= by by_cases hv : v ≤ w · simp [toFin_signExtend_of_le hv, show 2 ^ v - 2 ^ w = 0 by rw [@Nat.sub_eq_zero_iff_le]; apply Nat.pow_le_pow_of_le (by decide) (by omega)] · simp only [Nat.not_le] at hv apply Fin.eq_of_val_eq simp only [val_toFin, Fin.val_ofNat] rw [toNat_signExtend_of_le _ (by omega)] have : 2 ^ w < 2 ^ v := by apply Nat.pow_lt_pow_of_lt <;> omega rw [Nat.mod_eq_of_lt] grind theorem signExtend_and {x y : BitVec w} : (x &&& y).signExtend v = (x.signExtend v) &&& (y.signExtend v) := by grind (splits := 11) theorem signExtend_or {x y : BitVec w} : (x ||| y).signExtend v = (x.signExtend v) ||| (y.signExtend v) := by grind (splits := 12) theorem signExtend_xor {x y : BitVec w} : (x ^^^ y).signExtend v = (x.signExtend v) ^^^ (y.signExtend v) := by grind (splits := 11) theorem signExtend_not {x : BitVec w} (h : 0 < w) : (~~~x).signExtend v = ~~~(x.signExtend v) := by grind (splits := 11) /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : x ++ y = (shiftLeftZeroExtend x w ||| setWidth' (Nat.le_add_left w v) y) := rfl theorem getLsbD_append {x : BitVec n} {y : BitVec m} : getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m) := by grind [append_def] theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) : (x ++ y)[i] = if h : i < m then y[i] else x[i - m] := by grind [append_def] theorem getMsbD_append {x : BitVec n} {y : BitVec m} : getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by grind (splits := 13) [append_def] theorem msb_append {x : BitVec w} {y : BitVec v} : (x ++ y).msb = if w = 0 then y.msb else x.msb := by grind (splits := 14) [append_def] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by grind theorem toInt_append {x : BitVec n} {y : BitVec m} : (x ++ y).toInt = if n = 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by by_cases n0 : n = 0 · subst n0 simp [BitVec.eq_nil x, BitVec.toInt] · by_cases m0 : m = 0 · subst m0; rw [BitVec.eq_nil y, append_zero_width]; simp [n0] · simp only [n0, ↓reduceIte] by_cases x.msb case pos h => rw [toInt_eq_msb_cond] simp only [show ((x ++ y).msb = true) by simp [msb_append, n0, h], ↓reduceIte, toNat_append, Nat.pow_add, ← Nat.shiftLeft_eq, toInt_eq_msb_cond, h] rw_mod_cast [← Nat.shiftLeft_add_eq_or_of_lt (by omega), Nat.shiftLeft_eq, Nat.shiftLeft_eq, Nat.mul_comm, Int.mul_sub] norm_cast rw [Int.natCast_add, Nat.mul_comm (n := 2 ^ n)] omega case neg h => rw [Bool.not_eq_true] at h rw [toInt_eq_toNat_of_msb h, toInt_eq_toNat_of_msb (by simp [msb_append, n0, h])] rw_mod_cast [toNat_append, ← Nat.shiftLeft_add_eq_or_of_lt (by omega), Nat.shiftLeft_eq, Nat.mul_comm] theorem toInt_append_zero {n m : Nat} {x : BitVec n} : (x ++ 0#m).toInt = (2 ^ m) * x.toInt := by simp only [toInt_append, toInt_zero, toNat_ofNat, Nat.zero_mod, Int.cast_ofNat_Int, Int.add_zero, ite_eq_right_iff] -- FIXME: `grind` fails because of a reduction failure in`Lean.Grind.CommRing.Stepwise.d_step1_cert`. -- Something needs `@[expose]`, but what? -- grind only [two_mul_toInt_lt, le_two_mul_toInt, = toInt_zero_length] intro h subst h simp [BitVec.eq_nil x] theorem toInt_zero_append {n m : Nat} {x : BitVec n} : (0#m ++ x).toInt = if m = 0 then x.toInt else x.toNat := by simp [toInt_append] /-- Show that `(x.toNat <<< n) ||| y.toNat` is within bounds of `BitVec (m + n)`. -/ theorem toNat_shiftLeft_or_toNat_lt_two_pow_add {m n : Nat} (x : BitVec m) (y : BitVec n) : x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := by have hnLe : 2^n ≤ 2 ^(m + n) := by rw [Nat.pow_add] exact Nat.le_mul_of_pos_left (2 ^ n) (Nat.two_pow_pos m) apply Nat.or_lt_two_pow · have := Nat.two_pow_pos n rw [Nat.shiftLeft_eq, Nat.pow_add, Nat.mul_lt_mul_right] <;> omega · omega theorem toFin_append {x : BitVec m} {y : BitVec n} : (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (toNat_shiftLeft_or_toNat_lt_two_pow_add x y) := by ext simp theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = y.cast (by omega) := by ext i ih simp [getElem_append, show i < v by omega] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by grind theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) : (x ++ y).cast h = x ++ y.cast (by omega) := by grind theorem cast_append_left (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) : (x ++ y).cast h = x.cast (by omega) ++ y := by grind theorem setWidth_append {x : BitVec w} {y : BitVec v} : (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by grind theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by subst h grind theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by grind theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by grind theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by grind theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by grind theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by grind theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) : x >>> (n + m) = (x >>> n) >>> m:= by grind theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}: x >>> n <<< n = x &&& BitVec.allOnes w <<< n := by induction n generalizing x with grind theorem msb_shiftLeft {x : BitVec w} {n : Nat} : (x <<< n).msb = x.getMsbD n := by grind /-- A `(x : BitVec v)` set to width `w` equals `(v - w)` zeros, followed by the low `(min v w) bits of `x` -/ theorem setWidth_eq_append_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} : x.setWidth w = ((0#(w - v)) ++ x.extractLsb' 0 (min v w)).cast (by omega) := by ext i hi simp only [getElem_cast] grind /-- A `(x : BitVec v)` set to a width `w ≥ v` equals `(w - v)` zeros, followed by `x`. -/ theorem setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) : x.setWidth w = ((0#(w - v)) ++ x).cast (by omega) := by grind theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) : x.setWidth w = x.extractLsb' 0 w := by rw [setWidth_eq_append_extractLsb'] ext i hi simp only [getElem_cast, getElem_append] grind theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) : x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by grind theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) : x <<< n = (x.extractLsb' 0 (w - n) ++ 0#n).cast (by omega) := by grind /-- Combine adjacent `extractLsb'` operations into a single `extractLsb'`. -/ theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) : ((x.extractLsb' start₂ len₂) ++ (x.extractLsb' start₁ len₁)) = (x.extractLsb' start₁ (len₁ + len₂)).cast (by omega) := by grind (splits := 14) /-- Combine adjacent `~~~ (extractLsb _)'` operations into a single `~~~ (extractLsb _)'`. -/ theorem not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) : (~~~ (x.extractLsb' start₂ len₂) ++ ~~~ (x.extractLsb' start₁ len₁)) = (~~~ x.extractLsb' start₁ (len₁ + len₂)).cast (by omega) := by grind (splits := 14) /-- A sign extension of `x : BitVec w` equals high bits of either `0` or `1` depending on `x.msb`, followed by the low bits of `x`. -/ theorem signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} : x.signExtend v = ((if x.msb then allOnes (v - w) else 0#(v - w)) ++ x.extractLsb' 0 (min w v)).cast (by omega) := by ext i hi simp only [getElem_cast] grind (splits := 12) /-- A sign extension of `x : BitVec w` to a larger bitwidth `v ≥ w` equals high bits of either `0` or `1` depending on `x.msb`, followed by `x`. -/ theorem signExtend_eq_append_of_le {w v : Nat} {x : BitVec w} (h : w ≤ v) : x.signExtend v = ((if x.msb then allOnes (v - w) else 0#(v - w)) ++ x).cast (by omega) := by grind /-- The 'master theorem' for extracting bits from `(xhi ++ xlo)`, which performs a case analysis on the start index, length, and the lengths of `xlo, xhi`. · If the start index is entirely out of the `xlo` bitvector, then grab the bits from `xhi`. · If the start index is entirely contained in the `xlo` bitvector, then grab the bits from `xlo`. · If the start index is split between the two bitvectors, then append `(w - start)` bits from `xlo` with `(len - (w - start))` bits from xhi. Diagramatically: ``` xhi xlo (<---------------------](<-------w--------] start+len..start: (<-----len---*------] w - start: *------* len - (w -start): *------------* ``` -/ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} : extractLsb' start len (xhi ++ xlo) = if hstart : start < w then if hlen : start + len ≤ w then extractLsb' start len xlo else (((extractLsb' (start - w) (len - (w - start)) xhi) ++ extractLsb' start (w - start) xlo)).cast (by omega) else extractLsb' (start - w) len xhi := by grind (splits := 21) /-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting the bits from `xlo` when `start + len` is within `xlo`. -/ theorem extractLsb'_append_eq_of_add_le {v w} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} (h : start + len ≤ w) : extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo := by grind /-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting the bits from `xhi` when `start` is outside `xlo`. -/ theorem extractLsb'_append_eq_of_le {v w} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} (h : w ≤ start) : extractLsb' start len (xhi ++ xlo) = extractLsb' (start - w) len xhi := by grind /-! ### rev -/ theorem getLsbD_rev (x : BitVec w) (i : Fin w) : x.getLsbD i.rev = x.getMsbD i := by grind [Fin.is_lt] theorem getElem_rev {x : BitVec w} {i : Fin w}: x[i.rev] = x.getMsbD i := by grind [Fin.is_lt] theorem getMsbD_rev (x : BitVec w) (i : Fin w) : x.getMsbD i.rev = x.getLsbD i := by simp only [← getLsbD_rev] simp only [Fin.rev] congr omega /-! ### cons -/ /-- Variant of `toNat_cons` using `+` instead of `|||`. -/ theorem toNat_cons' {x : BitVec w} : (cons a x).toNat = (a.toNat <<< w) + x.toNat := by simp [cons, Nat.shiftLeft_eq, Nat.mul_comm _ (2^w), Nat.two_pow_add_eq_or_of_lt, x.isLt] theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) : getLsbD (cons b x) i = if i = n then b else getLsbD x i := by grind [cases Bool, testBit_toNat] theorem msb_cons : (cons a x).msb = a := by grind theorem getMsbD_cons_zero : (cons a x).getMsbD 0 = a := by grind theorem getMsbD_cons_succ : (cons a x).getMsbD (i + 1) = x.getMsbD i := by grind theorem setWidth_succ (x : BitVec w) : setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by grind theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by grind theorem cons_or_cons (x y : BitVec w) (a b : Bool) : (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by grind theorem cons_and_cons (x y : BitVec w) (a b : Bool) : (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by grind theorem cons_xor_cons (x y : BitVec w) (a b : Bool) : (cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y) := by grind theorem cons_append (x : BitVec w₁) (y : BitVec w₂) (a : Bool) : (cons a x) ++ y = (cons a (x ++ y)).cast (by omega) := by grind theorem cons_append_append (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool) : (cons a x) ++ y ++ z = (cons a (x ++ y ++ z)).cast (by omega) := by grind /-! ### concat -/ theorem toNat_concat (x : BitVec w) (b : Bool) : (concat x b).toNat = x.toNat * 2 + b.toNat := by apply Nat.eq_of_testBit_eq simp only [concat, toNat_append, Nat.shiftLeft_eq, Nat.pow_one, toNat_ofBool, Nat.testBit_or] cases b · simp · rintro (_ | i) <;> simp [Nat.add_comm, Nat.add_mul_div_right, Nat.testBit_add_one] theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) : (concat x b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1) := by simp only [concat, getLsbD, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq] cases i · simp [Nat.mod_eq_of_lt b.toNat_lt] · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one] theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) : (concat x b)[i] = if h : i = 0 then b else x[i - 1] := by simp only [concat, getElem_eq_testBit_toNat, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq] cases i · simp [Nat.mod_eq_of_lt b.toNat_lt] · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one] theorem getElem_concat_zero {x : BitVec w} : (concat x b)[0] = b := by grind theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by grind theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by grind theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i + 1 < w + 1) : (concat x b)[i + 1] = x[i] := by grind theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} : (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b := by grind theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} : (x.concat b).msb = if 0 < w then x.msb else b := by grind theorem toInt_concat (x : BitVec w) (b : Bool) : (concat x b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt := by simp only [BitVec.toInt, toNat_concat] cases w · grind [cases Bool] · cases b <;> simp <;> omega theorem toFin_concat (x : BitVec w) (b : Bool) : (concat x b).toFin = Fin.mk (x.toNat * 2 + b.toNat) (by have := Bool.toNat_lt b simp [← Nat.two_pow_pred_add_two_pow_pred] omega ) := by simp [← Fin.val_inj] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by grind theorem concat_or_concat (x y : BitVec w) (a b : Bool) : (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by grind theorem concat_and_concat (x y : BitVec w) (a b : Bool) : (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by grind theorem concat_xor_concat (x y : BitVec w) (a b : Bool) : (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by grind theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by grind /-! ### shiftConcat -/ theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) : (shiftConcat x b).getLsbD i = (decide (i < w) && (if (i = 0) then b else x.getLsbD (i - 1))) := by grind [shiftConcat] theorem getElem_shiftConcat {x : BitVec w} {b : Bool} (h : i < w) : (x.shiftConcat b)[i] = if i = 0 then b else x[i-1] := by rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h, Bool.true_and] theorem getElem_shiftConcat_zero {x : BitVec w} (b : Bool) (h : 0 < w) : (x.shiftConcat b)[0] = b := by grind theorem getElem_shiftConcat_succ {x : BitVec w} {b : Bool} (h : i + 1 < w) : (x.shiftConcat b)[i+1] = x[i] := by grind theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) : (shiftConcat x b).getLsbD i = (decide (i < w) && ((decide (i = 0) && b) || (decide (0 < i) && x.getLsbD (i - 1)))) := by grind theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) : n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by grind @[simp, bitvec_to_nat] theorem toNat_shiftConcat {x : BitVec w} {b : Bool} : (x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w := by grind [shiftConcat, Nat.shiftLeft_eq] /-- `x.shiftConcat b` does not overflow if `x < 2^k` for `k < w`, and so `x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat`. -/ theorem toNat_shiftConcat_eq_of_lt {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) : (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat := by simp only [toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one] have : 2 ^ k < 2 ^ w := Nat.pow_lt_pow_of_lt (by omega) (by omega) have : 2 ^ k * 2 ≤ 2 ^ w := (Nat.pow_lt_pow_iff_pow_mul_le_pow (by omega)).mp this rw [Nat.mod_eq_of_lt (by cases b <;> simp [bitvec_to_nat] <;> omega)] theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) : (x.shiftConcat b).toNat < 2 ^ (k + 1) := by rw [toNat_shiftConcat_eq_of_lt hk hx] have := Bool.toNat_lt b omega /-! ### add -/ theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl /-- Definition of bitvector addition as a nat. -/ @[simp, bitvec_to_nat] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) : .ofFin x + y = .ofFin (x + y.toFin) := rfl theorem add_ofFin (x : BitVec n) (y : Fin (2^n)) : x + .ofFin y = .ofFin (x.toFin + y) := rfl theorem ofNat_add {n} (x y : Nat) : BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y := by apply eq_of_toNat_eq simp [BitVec.ofNat, Fin.ofNat_add] theorem ofNat_add_ofNat {n} (x y : Nat) : BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y) := (ofNat_add x y).symm theorem toNat_add_of_not_uaddOverflow {x y : BitVec w} (h : ¬ uaddOverflow x y) : (x + y).toNat = x.toNat + y.toNat := by rcases w with _|w · simp [of_length_zero] · simp only [uaddOverflow, ge_iff_le, decide_eq_true_eq, Nat.not_le] at h rw [toNat_add, Nat.mod_eq_of_lt h] /-- Unsigned addition overflow reassociation. If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows. -/ theorem uaddOverflow_assoc {x y z : BitVec w} (h : ¬ x.uaddOverflow y) (h' : ¬ y.uaddOverflow z) : (x + y).uaddOverflow z = x.uaddOverflow (y + z) := by simp only [uaddOverflow, ge_iff_le, decide_eq_true_eq, Nat.not_le] at h h' simp only [uaddOverflow, toNat_add, ge_iff_le, decide_eq_decide] repeat rw [Nat.mod_eq_of_lt (by grind)] grind protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by apply eq_of_toNat_eq ; simp [Nat.add_assoc] instance : Std.Associative (α := BitVec n) (· + ·) := ⟨BitVec.add_assoc⟩ protected theorem add_comm (x y : BitVec n) : x + y = y + x := by simp [add_def, Nat.add_comm] instance : Std.Commutative (α := BitVec n) (· + ·) := ⟨BitVec.add_comm⟩ @[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def] @[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def] instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where left_id := BitVec.zero_add right_id := BitVec.add_zero theorem setWidth_add (x y : BitVec w) (h : i ≤ w) : (x + y).setWidth i = x.setWidth i + y.setWidth i := by have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h simp [bitvec_to_nat, Nat.mod_mod_of_dvd _ dvd] @[simp, bitvec_to_nat] theorem toInt_add (x y : BitVec w) : (x + y).toInt = (x.toInt + y.toInt).bmod (2^w) := by simp [toInt_eq_toNat_bmod, -Int.natCast_pow] theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y := by apply eq_of_toInt_eq simp theorem toInt_add_of_not_saddOverflow {x y : BitVec w} (h : ¬ saddOverflow x y) : (x + y).toInt = x.toInt + y.toInt := by rcases w with _|w · simp [of_length_zero] · simp only [saddOverflow, Nat.add_one_sub_one, ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, _root_.not_or, Int.not_le, Int.not_lt] at h rw [toInt_add, Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] /-- Signed addition overflow reassociation. If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows. -/ theorem saddOverflow_assoc {x y z : BitVec w} (h : ¬ x.saddOverflow y) (h' : ¬ y.saddOverflow z) : (x + y).saddOverflow z = x.saddOverflow (y + z) := by rcases w with _|w · simp [of_length_zero] · simp only [saddOverflow, Nat.add_one_sub_one, ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, _root_.not_or, Int.not_le, Int.not_lt] at h h' simp only [bool_to_prop, saddOverflow, toInt_add, ge_iff_le, Nat.add_one_sub_one] repeat rw [Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] grind theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} : (x + y) <<< n = x <<< n + y <<< n := by induction n case zero => simp case succ n ih => simp [toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul] theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _ have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _ rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h'])) /-! ### sub/neg -/ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := rfl theorem toNat_sub {n} (x y : BitVec n) : (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl @[simp, bitvec_to_nat] theorem toInt_sub {x y : BitVec w} : (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega), -Int.natCast_pow] theorem toNat_sub_of_not_usubOverflow {x y : BitVec w} (h : ¬ usubOverflow x y) : (x - y).toNat = x.toNat - y.toNat := by rcases w with _|w · simp [of_length_zero] · simp only [usubOverflow, decide_eq_true_eq, Nat.not_lt] at h rw [toNat_sub, ← Nat.sub_add_comm (by omega), Nat.add_sub_assoc h, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)] theorem toInt_sub_of_not_ssubOverflow {x y : BitVec w} (h : ¬ ssubOverflow x y) : (x - y).toInt = x.toInt - y.toInt := by rcases w with _|w · simp [of_length_zero] · simp only [ssubOverflow, Nat.add_one_sub_one, ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, _root_.not_or, Int.not_le, Int.not_lt] at h rw [toInt_sub, Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} : (x.toInt - y.toInt < - 2 ^ (w - 1)) ↔ (x.toInt < 0 ∧ 0 ≤ y.toInt ∧ 0 ≤ (x.toInt - y.toInt).bmod (2 ^ w)) := by rcases w with _|w · simp [of_length_zero] · have := le_two_mul_toInt (x := x) have := two_mul_toInt_lt (x := y) simp only [Nat.add_one_sub_one] constructor · intro h rw_mod_cast [← Int.add_bmod_right, Int.bmod_eq_of_le] <;> omega · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1)) push_cast at this omega theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} : (2 ^ (w - 1) ≤ x.toInt - y.toInt) ↔ (0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ w) < 0) := by rcases w with _|w · simp [of_length_zero] · have := le_two_mul_toInt (x := x); have := two_mul_toInt_lt (x := x) have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y) simp only [Nat.add_one_sub_one] constructor · intro h simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and] rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)] omega · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1)) push_cast at this omega -- We prefer this lemma to `toNat_sub` for the `bitvec_to_nat` simp set. -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes -- results in `omega` generating proof terms that are very slow in the kernel. @[bitvec_to_nat] theorem toNat_sub' {n} (x y : BitVec n) : (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by rw [toNat_sub, Nat.add_comm] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) := rfl theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) := rfl -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals. -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea. theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y = .ofNat n ((2^n - y % 2^n) + x) := by apply eq_of_toNat_eq simp [BitVec.ofNat] theorem ofNat_sub_ofNat_of_le (x y : Nat) (hy : y < 2 ^ w) (hlt : y ≤ x): BitVec.ofNat w x - BitVec.ofNat w y = BitVec.ofNat w (x - y) := by apply eq_of_toNat_eq simp [Nat.mod_eq_of_lt hy, show 2 ^ w - y + x = 2 ^ w + (x - y) by omega, Nat.add_mod_left] @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp @[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl @[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by apply eq_of_toNat_eq simp only [toNat_sub] rw [Nat.add_comm, Nat.add_sub_of_le] · simp · exact Nat.le_of_lt x.isLt theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) : (- x).toNat = 2^n - x.toNat := by change 0 < x.toNat at h rw [toNat_neg, Nat.mod_eq_of_lt] omega theorem toInt_neg {x : BitVec w} : (-x).toInt = (-x.toInt).bmod (2 ^ w) := by rw [← BitVec.zero_sub, toInt_sub] simp theorem toInt_neg_of_not_negOverflow {x : BitVec w} (h : ¬ negOverflow x): (-x).toInt = -x.toInt := by rcases w with _|w · simp [of_length_zero] · have := toInt_lt (x := x); simp only [Nat.add_one_sub_one] at this have := le_toInt (x := x); simp only [Nat.add_one_sub_one] at this simp only [negOverflow, Nat.add_one_sub_one, beq_iff_eq] at h rw [toInt_neg, Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] theorem ofInt_neg {w : Nat} {n : Int} : BitVec.ofInt w (-n) = -BitVec.ofInt w n := eq_of_toInt_eq (by simp [toInt_neg]) theorem toFin_neg (x : BitVec n) : (-x).toFin = Fin.ofNat (2^n) (2^n - x.toNat) := rfl theorem sub_eq_add_neg {n} (x y : BitVec n) : x - y = x + - y := by apply eq_of_toNat_eq simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod] rw [Nat.add_comm] theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by apply toInt_inj.mp simp [toInt_neg, Int.add_left_neg] theorem add_right_neg (x : BitVec w) : x + -x = 0#w := by rw [BitVec.add_comm] exact add_left_neg x theorem neg_zero (n : Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by apply eq_of_toNat_eq have y_toNat_le := Nat.le_of_lt y.isLt rw [toNat_sub, toNat_add, Nat.add_comm, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le, Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel] theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by rw [sub_eq_add_neg, BitVec.add_assoc, BitVec.add_comm _ y, ← BitVec.add_assoc, ← sub_eq_add_neg, add_sub_cancel] theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z := by apply Iff.intro <;> intro h · simp [h, sub_add_cancel] · simp [←h, add_sub_cancel] theorem sub_eq_iff_eq_add {x y z : BitVec w} : x - y = z ↔ x = z + y := by apply Iff.intro <;> intro h · simp [← h, sub_add_cancel] · simp [h, add_sub_cancel] theorem neg_one_eq_allOnes : -1#w = allOnes w := by apply eq_of_toNat_eq if g : w = 0 then simp [g] else have q : 1 < 2^w := by simp [g] have r : (2^w - 1) < 2^w := by omega simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r] theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by apply eq_of_toNat_eq simp only [toNat_neg, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod] congr have hx : x.toNat < 2^w := x.isLt rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)] theorem not_eq_neg_add (x : BitVec w) : ~~~ x = -x - 1#w := by rw [eq_sub_iff_add_eq, neg_eq_not_add, BitVec.add_comm] theorem neg_neg {x : BitVec w} : - - x = x := by by_cases h : x = 0#w · simp [h] · simp [bitvec_to_nat, h] protected theorem neg_inj {x y : BitVec w} : -x = -y ↔ x = y := ⟨fun h => by rw [← @neg_neg w x, ← @neg_neg w y, h], congrArg _⟩ theorem neg_eq_iff_eq_neg {x y : BitVec w} : -x = y ↔ x = -y := by constructor all_goals intro h symm at h subst h simp theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by constructor all_goals intro h h' subst h' simp at h theorem neg_eq_zero_iff {x : BitVec w} : -x = 0#w ↔ x = 0#w := by constructor · intro h have : - (- x) = - 0 := by simp [h] simpa using this · intro h simp [h] theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _ have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _ rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h'])) theorem sub_eq_self {x : BitVec 1} : -x = x := by have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _ rcases ha with h | h <;> simp [h] theorem not_neg (x : BitVec w) : ~~~(-x) = x - 1#w := by rw [not_eq_neg_add, neg_neg] theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by apply eq_of_toInt_eq simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub] theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by apply eq_of_toInt_eq simp [toInt_neg, Int.sub_eq_add_neg] theorem sub_neg {x y : BitVec w} : x - - y = x + y := by apply eq_of_toInt_eq simp [toInt_neg] theorem neg_sub {x y : BitVec w} : - (x - y) = - x + y := by rw [sub_eq_add_neg, neg_add, sub_neg] /- ### add/sub injectivity -/ protected theorem add_left_inj {x y : BitVec w} (z : BitVec w) : (x + z = y + z) ↔ x = y := by apply Iff.intro · intro p rw [← add_sub_cancel x z, ← add_sub_cancel y z, p] · exact congrArg (· + z) protected theorem add_right_inj {x y : BitVec w} (z : BitVec w) : (z + x = z + y) ↔ x = y := by simp [BitVec.add_comm z] protected theorem sub_left_inj {x y : BitVec w} (z : BitVec w) : (x - z = y - z) ↔ x = y := by simp [sub_eq_add_neg] protected theorem sub_right_inj {x y : BitVec w} (z : BitVec w) : (z - x = z - y) ↔ x = y := by simp [sub_eq_add_neg] /-! ### add self -/ protected theorem add_left_eq_self {x y : BitVec w} : x + y = y ↔ x = 0#w := by conv => lhs; rhs; rw [← BitVec.zero_add y] exact BitVec.add_left_inj y protected theorem add_right_eq_self {x y : BitVec w} : x + y = x ↔ y = 0#w := by rw [BitVec.add_comm] exact BitVec.add_left_eq_self protected theorem self_eq_add_right {x y : BitVec w} : x = x + y ↔ y = 0#w := by rw [Eq.comm] exact BitVec.add_right_eq_self protected theorem self_eq_add_left {x y : BitVec w} : x = y + x ↔ y = 0#w := by rw [BitVec.add_comm] exact BitVec.self_eq_add_right /-! ### fill -/ theorem getLsbD_fill {w i : Nat} {v : Bool} : (fill w v).getLsbD i = (v && decide (i < w)) := by grind [cases Bool, BitVec.fill, BitVec.neg_one_eq_allOnes] theorem getMsbD_fill {w i : Nat} {v : Bool} : (fill w v).getMsbD i = (v && decide (i < w)) := by grind theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) : (fill w v)[i] = v := by grind [cases Bool, BitVec.fill, BitVec.neg_one_eq_allOnes] theorem msb_fill {w : Nat} {v : Bool} : (fill w v).msb = (v && decide (0 < w)) := by grind theorem fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w := by grind theorem fill_true {w : Nat} : fill w true = allOnes w := by grind theorem fill_false {w : Nat} : fill w false = 0#w := by grind theorem fill_toNat {w : Nat} {v : Bool} : (fill w v).toNat = if v = true then 2^w - 1 else 0 := by by_cases h : v <;> simp [h] theorem fill_toInt {w : Nat} {v : Bool} : (fill w v).toInt = if v = true && 0 < w then -1 else 0 := by by_cases h : v <;> simp [h] theorem fill_toFin {w : Nat} {v : Bool} : (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat (2 ^ w) 0 := by by_cases h : v <;> simp [h] /-! ### mul -/ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := rfl @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl theorem ofNat_mul {n} (x y : Nat) : BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y := by apply eq_of_toNat_eq simp [BitVec.ofNat] theorem ofNat_mul_ofNat {n} (x y : Nat) : BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y) := (ofNat_mul x y).symm protected theorem mul_comm (x y : BitVec w) : x * y = y * x := by apply eq_of_toFin_eq; simpa using Fin.mul_comm .. instance : Std.Commutative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_comm⟩ protected theorem mul_assoc (x y z : BitVec w) : x * y * z = x * (y * z) := by apply eq_of_toFin_eq; simpa using Fin.mul_assoc .. instance : Std.Associative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_assoc⟩ @[simp] protected theorem mul_one (x : BitVec w) : x * 1#w = x := by cases w · apply Subsingleton.elim · apply eq_of_toNat_eq; simp [Nat.mod_eq_of_lt] @[simp] protected theorem one_mul (x : BitVec w) : 1#w * x = x := by rw [BitVec.mul_comm, BitVec.mul_one] instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where right_id := BitVec.mul_one theorem mul_zero {x : BitVec w} : x * 0#w = 0#w := by apply eq_of_toNat_eq simp [toNat_mul] theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by apply eq_of_toNat_eq simp [toNat_mul] theorem mul_add {x y z : BitVec w} : x * (y + z) = x * y + x * z := by apply eq_of_toNat_eq simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod] rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat), ← Nat.mul_mod, Nat.mul_add] theorem add_mul {x y z : BitVec w} : (x + y) * z = x * z + y * z := by rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z] theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add] theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add] theorem mul_two {x : BitVec w} : x * 2#w = x + x := by have : 2#w = 1#w + 1#w := by apply BitVec.eq_of_toNat_eq; simp simp [this, mul_succ] theorem two_mul {x : BitVec w} : 2#w * x = x + x := by rw [BitVec.mul_comm, mul_two] @[simp, bitvec_to_nat] theorem toInt_mul (x y : BitVec w) : (x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by simp [toInt_eq_toNat_bmod, -Int.natCast_pow] theorem toNat_mul_of_not_umulOverflow {x y : BitVec w} (h : ¬ umulOverflow x y) : (x * y).toNat = x.toNat * y.toNat := by rcases w with _|w · simp [of_length_zero] · simp only [umulOverflow, ge_iff_le, decide_eq_true_eq, Nat.not_le] at h rw [toNat_mul, Nat.mod_eq_of_lt h] /-- Unsigned multiplication overflow reassociation. If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows. -/ theorem umulOverflow_assoc {x y z : BitVec w} (h : ¬ x.umulOverflow y) (h' : ¬ y.umulOverflow z) : (x * y).umulOverflow z = x.umulOverflow (y * z) := by simp only [umulOverflow, ge_iff_le, decide_eq_true_eq, Nat.not_le] at h h' simp only [umulOverflow, toNat_mul, ge_iff_le, decide_eq_decide] repeat rw [Nat.mod_eq_of_lt (by omega)] rw [Nat.mul_assoc] theorem toInt_mul_of_not_smulOverflow {x y : BitVec w} (h : ¬ smulOverflow x y) : (x * y).toInt = x.toInt * y.toInt := by rcases w with _|w · simp [of_length_zero] · simp only [smulOverflow, Nat.add_one_sub_one, ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, _root_.not_or, Int.not_le, Int.not_lt] at h rw [toInt_mul, Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] /-- Signed multiplication overflow reassociation. If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows. -/ theorem smulOverflow_assoc {x y z : BitVec w} (h : ¬ x.smulOverflow y) (h' : ¬ y.smulOverflow z) : (x * y).smulOverflow z = x.smulOverflow (y * z) := by rcases w with _|w · simp [of_length_zero] · simp only [smulOverflow, Nat.add_one_sub_one, ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, _root_.not_or, Int.not_le, Int.not_lt] at h h' simp only [smulOverflow, toInt_mul, Nat.add_one_sub_one, ge_iff_le, bool_to_prop] repeat rw [Int.bmod_eq_of_le (by push_cast; omega) (by push_cast; omega)] rw [Int.mul_assoc] theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y := by apply eq_of_toInt_eq simp theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b := by have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _ have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _ rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h'])) @[simp] protected theorem neg_mul (x y : BitVec w) : -x * y = -(x * y) := by apply eq_of_toInt_eq simp [toInt_neg, Int.neg_mul] @[simp] protected theorem mul_neg (x y : BitVec w) : x * -y = -(x * y) := by rw [BitVec.mul_comm, BitVec.neg_mul, BitVec.mul_comm] protected theorem neg_mul_neg (x y : BitVec w) : -x * -y = x * y := by simp protected theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y := by simp theorem mul_sub {x y z : BitVec w} : x * (y - z) = x * y - x * z := by rw [← add_neg_eq_sub, mul_add, BitVec.mul_neg, add_neg_eq_sub] theorem neg_add_mul_eq_mul_not {x y : BitVec w} : - (x + x * y) = x * ~~~ y := by rw [neg_add, sub_eq_add_neg, ← BitVec.mul_neg, neg_eq_not_add y, mul_add, BitVec.mul_one, BitVec.add_comm, BitVec.add_assoc, BitVec.add_right_eq_self, add_neg_eq_sub, BitVec.sub_self] theorem neg_mul_not_eq_add_mul {x y : BitVec w} : - (x * ~~~ y) = x + x * y := by rw [not_eq_neg_add, mul_sub, neg_sub, ← BitVec.mul_neg, neg_neg, BitVec.mul_one, BitVec.add_comm] theorem neg_eq_neg_one_mul (b : BitVec w) : -b = -1#w * b := BitVec.eq_of_toInt_eq (by simp) theorem setWidth_mul (x y : BitVec w) (h : i ≤ w) : (x * y).setWidth i = x.setWidth i * y.setWidth i := by have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h simp [bitvec_to_nat, Nat.mod_mod_of_dvd _ dvd] /-! ### pow -/ protected theorem pow_zero {x : BitVec w} : x ^ 0 = 1#w := rfl protected theorem pow_succ {x : BitVec w} : x ^ (n + 1) = x ^ n * x := rfl protected theorem pow_one {x : BitVec w} : x ^ 1 = x := by simp [BitVec.pow_succ] protected theorem pow_add {x : BitVec w} {n m : Nat}: x ^ (n + m) = (x ^ n) * (x ^ m):= by induction m with | zero => simp | succ m ih => rw [← Nat.add_assoc, BitVec.pow_succ, ih, BitVec.mul_assoc, BitVec.pow_succ] /-! ### le and lt -/ @[bitvec_to_nat] theorem le_def {x y : BitVec n} : x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl theorem le_ofFin {x : BitVec n} {y : Fin (2^n)} : x ≤ BitVec.ofFin y ↔ x.toFin ≤ y := Iff.rfl theorem ofFin_le {x : Fin (2^n)} {y : BitVec n} : BitVec.ofFin x ≤ y ↔ x ≤ y.toFin := Iff.rfl theorem ofNat_le_ofNat {n} {x y : Nat} : (BitVec.ofNat n x) ≤ (BitVec.ofNat n y) ↔ x % 2^n ≤ y % 2^n := by simp [le_def] @[bitvec_to_nat] theorem lt_def {x y : BitVec n} : x < y ↔ x.toNat < y.toNat := Iff.rfl theorem lt_ofFin {x : BitVec n} {y : Fin (2^n)} : x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl theorem ofFin_lt {x : Fin (2^n)} {y : BitVec n} : BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl theorem ofNat_lt_ofNat {n} {x y : Nat} : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n := by simp [lt_def] @[simp] protected theorem not_le {x y : BitVec n} : ¬ x ≤ y ↔ y < x := by simp [le_def, lt_def] @[simp] protected theorem not_lt {x y : BitVec n} : ¬ x < y ↔ y ≤ x := by simp [le_def, lt_def] @[simp] protected theorem le_refl (x : BitVec n) : x ≤ x := by simp [le_def] @[simp] protected theorem lt_irrefl (x : BitVec n) : ¬x < x := by simp [lt_def] protected theorem le_trans {x y z : BitVec n} : x ≤ y → y ≤ z → x ≤ z := by simp only [le_def] apply Nat.le_trans protected theorem lt_trans {x y z : BitVec n} : x < y → y < z → x < z := by simp only [lt_def] apply Nat.lt_trans protected theorem le_total (x y : BitVec n) : x ≤ y ∨ y ≤ x := by simp only [le_def] apply Nat.le_total protected theorem le_antisymm {x y : BitVec n} : x ≤ y → y ≤ x → x = y := by simp only [le_def, BitVec.toNat_eq] apply Nat.le_antisymm protected theorem lt_asymm {x y : BitVec n} : x < y → ¬ y < x := by simp only [lt_def] apply Nat.lt_asymm protected theorem lt_of_le_ne {x y : BitVec n} : x ≤ y → ¬ x = y → x < y := by simp only [lt_def, le_def, BitVec.toNat_eq] apply Nat.lt_of_le_of_ne protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by simp only [lt_def, ne_eq, toNat_eq] apply Nat.ne_of_lt protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod] apply Nat.mod_lt theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by constructor <;> (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega) protected theorem le_of_lt {x y : BitVec w} (h : x < y) : x ≤ y := Nat.le_of_lt h protected theorem le_of_eq {x y : BitVec w} (h : x = y) : x ≤ y := Nat.le_of_eq (toNat_eq.mp h) theorem not_lt_zero {x : BitVec w} : ¬x < 0#w := of_decide_eq_false rfl theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by constructor · intro h have : x ≥ 0 := not_lt_iff_le.mp not_lt_zero exact Eq.symm (BitVec.le_antisymm this h) · simp_all theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by constructor · intro h₂ rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow, Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂ simp [toNat_eq, show x.toNat = 0 by omega] · simp_all theorem not_allOnes_lt {x : BitVec w} : ¬allOnes w < x := by have : 2^w ≠ 0 := Ne.symm (NeZero.ne' (2^w)) rw [BitVec.not_lt, le_def, Nat.le_iff_lt_add_one, toNat_allOnes, Nat.sub_one_add_one this] exact isLt x theorem allOnes_le_iff {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w := by constructor · intro h have : x ≤ allOnes w := not_lt_iff_le.mp not_allOnes_lt exact Eq.symm (BitVec.le_antisymm h this) · simp_all theorem lt_allOnes_iff {x : BitVec w} : x < allOnes w ↔ x ≠ allOnes w := by have := not_congr (@allOnes_le_iff w x) rw [BitVec.not_le] at this exact this theorem le_of_zero_length (h : w = 0) {x y : BitVec w} : x ≤ y := by exact BitVec.le_of_eq (eq_of_zero_length h) theorem pos_of_msb {x : BitVec w} (hx : x.msb = true) : 0#w < x := by apply Decidable.by_contra intro h rw [BitVec.not_lt, le_zero_iff] at h simp [h] at hx theorem lt_of_msb_false_of_msb_true {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) : x < y := by simp only [LT.lt] have := toNat_ge_of_msb_true hy have := toNat_lt_of_msb_false hx simp omega /-! ### udiv -/ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega) rw [← udiv_eq] simp [udiv, bitvec_to_nat, h, Nat.mod_eq_of_lt] theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by rfl @[simp, bitvec_to_nat] theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by rfl theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by simp [bitvec_to_nat] theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n := by simp [udiv_def] theorem udiv_one {x : BitVec w} : x / 1#w = x := by simp only [toNat_eq, toNat_udiv, toNat_ofNat] cases w · simp [eq_nil x] · simp theorem udiv_eq_and {x y : BitVec 1} : x / y = (x &&& y) := by have hx : x = 0#1 ∨ x = 1#1 := by bv_omega have hy : y = 0#1 ∨ y = 1#1 := by bv_omega rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> rfl theorem udiv_self {x : BitVec w} : x / x = if x == 0#w then 0#w else 1#w := by by_cases h : x = 0#w · simp [h] · simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h simp only [beq_iff_eq, toNat_eq, toNat_ofNat, Nat.zero_mod, h, ↓reduceIte, toNat_udiv] rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)] theorem msb_udiv (x y : BitVec w) : (x / y).msb = (x.msb && y == 1#w) := by cases msb_x : x.msb · suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide] calc x.toNat / y.toNat ≤ x.toNat := by apply Nat.div_le_self _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x . rcases w with _|w · contradiction · have : (y == 1#_) = decide (y.toNat = 1) := by simp [(· == ·), toNat_eq] simp only [this, Bool.true_and] match hy : y.toNat with | 0 => obtain rfl : y = 0#_ := eq_of_toNat_eq hy simp | 1 => obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy]) simpa using msb_x | y + 2 => suffices x.toNat / (y + 2) < 2 ^ w by simp_all [msb_eq_decide] calc x.toNat / (y + 2) ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega) _ < 2 ^ w := by omega theorem msb_udiv_eq_false_of {x : BitVec w} {y : BitVec w} (h : x.msb = false) : (x / y).msb = false := by simp [msb_udiv, h] /-- If `x` is nonnegative (i.e., does not have its msb set), then `x / y` is nonnegative, thus `toInt` and `toNat` coincide. -/ theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) : (x / y).toInt = x.toNat / y.toNat := by simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h] /-- Unsigned division is zero if and only if either the denominator is zero, or the numerator is unsigned less than the denominator -/ theorem udiv_eq_zero_iff_eq_zero_or_lt {x y : BitVec w} : x / y = 0#w ↔ (y = 0#w ∨ x < y) := by simp [toNat_eq, toNat_udiv, toNat_ofNat, Nat.zero_mod, Nat.div_eq_zero_iff, BitVec.lt_def] theorem udiv_ne_zero_iff_ne_zero_and_le {x y : BitVec w} : ¬ (x / y = 0#w) ↔ (y ≠ 0#w ∧ y ≤ x) := by simp only [ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt] /-! ### umod -/ theorem umod_def {x y : BitVec n} : x % y = BitVec.ofNat n (x.toNat % y.toNat) := by rw [← umod_eq] have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt simp [umod, bitvec_to_nat, Nat.mod_eq_of_lt h] @[simp, bitvec_to_nat] theorem toNat_umod {x y : BitVec n} : (x % y).toNat = x.toNat % y.toNat := rfl theorem toFin_umod {x y : BitVec w} : (x % y).toFin = x.toFin % y.toFin := rfl theorem umod_zero {x : BitVec n} : x % 0#n = x := by simp [umod_def] theorem zero_umod {x : BitVec w} : (0#w) % x = 0#w := by simp [bitvec_to_nat] theorem umod_one {x : BitVec w} : x % (1#w) = 0#w := by simp only [toNat_eq, toNat_umod, toNat_ofNat, Nat.zero_mod] cases w · simp [eq_nil x] · simp [Nat.mod_one] theorem umod_self {x : BitVec w} : x % x = 0#w := by simp [bitvec_to_nat] theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by have hx : x = 0#1 ∨ x = 1#1 := by bv_omega have hy : y = 0#1 ∨ y = 1#1 := by bv_omega rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> rfl theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) : x % y = x := by apply eq_of_toNat_eq simp [Nat.mod_eq_of_lt h] theorem msb_umod {x y : BitVec w} : (x % y).msb = (x.msb && (x < y || y == 0#w)) := by rw [msb_eq_decide, toNat_umod] cases msb_x : x.msb · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa calc x.toNat % y.toNat ≤ x.toNat := by apply Nat.mod_le _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x . by_cases hy : y = 0 · simp_all [msb_eq_decide] · suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all by_cases x_lt_y : x < y . simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide] · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa [x_lt_y] have y_le_x : y.toNat ≤ x.toNat := by simpa using x_lt_y replace hy : y.toNat ≠ 0 := toNat_ne_iff_ne.mpr hy by_cases msb_y : y.toNat < 2 ^ (w - 1) · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega) omega · rcases w with _|w · contradiction simp only [Nat.add_one_sub_one] replace msb_y : 2 ^ w ≤ y.toNat := by simpa using msb_y have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by apply Nat.le_mul_of_pos_right apply Nat.div_pos y_le_x omega have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by rw [Nat.mod_eq_sub]; omega omega theorem toInt_umod {x y : BitVec w} : (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by simp [toInt_eq_toNat_bmod] theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) : (x % y).toInt = x.toInt % y.toNat := by simp [toInt_eq_msb_cond, h] theorem msb_umod_of_msb_false_of_ne_zero {x y : BitVec w} (hmsb : y.msb = false) (h_ne_zero : y ≠ 0#w) : (x % y).msb = false := by simp only [msb_umod, Bool.and_eq_false_imp, Bool.or_eq_false_iff, beq_eq_false_iff_ne, ne_eq, h_ne_zero] intro h simp [BitVec.le_of_lt, lt_of_msb_false_of_msb_true hmsb h] /-! ### smtUDiv -/ theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by simp [smtUDiv] theorem smtUDiv_zero {x : BitVec n} : x.smtUDiv 0#n = allOnes n := rfl /-! ### sdiv -/ /-- Equation theorem for `sdiv` in terms of `udiv`. -/ theorem sdiv_eq (x y : BitVec w) : x.sdiv y = match x.msb, y.msb with | false, false => udiv x y | false, true => - (x.udiv (- y)) | true, false => - ((- x).udiv y) | true, true => (- x).udiv (- y) := by rw [BitVec.sdiv] rcases x.msb <;> rcases y.msb <;> simp @[bitvec_to_nat] theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat = match x.msb, y.msb with | false, false => (udiv x y).toNat | false, true => (- (x.udiv (- y))).toNat | true, false => (- ((- x).udiv y)).toNat | true, true => ((- x).udiv (- y)).toNat := by simp only [sdiv_eq] by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h'] theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w := by simp only [sdiv_eq] rcases x.msb with msb | msb <;> simp theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by simp only [sdiv_eq, msb_zero] rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x := by simp only [sdiv_eq] · by_cases h : w = 1 · subst h rcases x.msb with msb | msb <;> simp · rcases x.msb with msb | msb <;> simp [h] theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by have hx : x = 0#1 ∨ x = 1#1 := by bv_omega have hy : y = 0#1 ∨ y = 1#1 := by bv_omega rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp theorem sdiv_self {x : BitVec w} : x.sdiv x = if x == 0#w then 0#w else 1#w := by simp [sdiv_eq] /-- Unsigned division never overflows. -/ theorem toNat_div_toNat_lt {w : Nat} {x y : BitVec w} : x.toNat / y.toNat < 2 ^ w := by have hy : y.toNat = 0 ∨ y.toNat = 1 ∨ 1 < y.toNat := by omega rcases hy with hy|hy|hy · simp [hy]; omega · simp [hy]; omega · rw [Nat.div_lt_iff_lt_mul (k := y.toNat) (x := x.toNat) (y := 2 ^ w) (by omega), show x.toNat = x.toNat * 1 by omega] apply Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega) /-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg. -/ theorem toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) : x.toInt / y.toInt < 2 ^ (w - 1) := by rcases w with _|w · simp [of_length_zero] · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x) by_cases hy' : y.toInt = 1 · simp [hy', Int.ediv_one]; omega · by_cases hx' : x.toInt = 0 · simp only [hx', Int.zero_ediv, Nat.add_one_sub_one, gt_iff_lt] norm_cast exact Nat.two_pow_pos (w := w) · have := Int.ediv_lt_self_of_pos_of_ne_one (x := x.toInt) (y := y.toInt) (by omega) (by omega) simp; omega /-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg. -/ theorem toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) : x.toInt / y.toInt ≤ 0 := by rcases w with _|w · simp [of_length_zero] · by_cases hx' : x.toInt = 0 · simp [hx'] · by_cases hy' : y.toInt = 0 · simp [hy'] · have := Int.ediv_neg_of_neg_of_pos (a := x.toInt) (b := y.toInt) (by omega) (by omega) simp; omega /-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos. -/ theorem toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) : x.toInt / y.toInt ≤ 0 := by rcases w with _|w · simp [of_length_zero] · by_cases hy' : y.toInt = -1 · simp [hy']; omega · have := Int.ediv_nonpos_of_nonneg_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega) simp; omega /-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862) we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y` and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`. from which it follows that: (-1)/0 = 0 (-1)/y = -1 when 0 < y (-1)/(-5) = 1 when y < 0 -/ theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} : (-1) / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1 := by rcases w with _|_|w · simp [of_length_zero] · cases eq_zero_or_eq_one y case _ h => simp [h] case _ h => simp [h] · by_cases 0 < y.toInt · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv] omega · by_cases hy : y.toInt = 0 · simp [hy] · simp [Int.sign_eq_neg_one_of_neg (a := y.toInt) (by omega), Int.neg_one_ediv] omega /-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1. -/ theorem toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) : x.toInt / y.toInt < 2 ^ (w - 1) := by rcases w with _|_|w · simp [of_length_zero] · have hy := eq_zero_or_eq_one (a := y) simp [← toInt_inj, toInt_zero] at hy omega · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x) have hx' : x.toInt = 0 ∨ x.toInt = - 1 ∨ x.toInt < - 1 := by omega rcases hx' with hx'|hx'|hx' · simp [hx']; omega · have := BitVec.neg_one_ediv_toInt_eq (y := y) simp [hx', this] omega · have := Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one (x := x.toInt) (y := y.toInt) (by omega) hy simp; omega /-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt. -/ theorem neg_two_pow_le_toInt_ediv {x y : BitVec w} : - 2 ^ (w - 1) ≤ x.toInt / y.toInt := by have xlt := @toInt_lt w x; have lex := @le_toInt w x by_cases hx : 0 ≤ x.toInt <;> by_cases hy : 0 ≤ y.toInt · have := Int.ediv_nonneg_of_nonneg_of_nonneg (x := x.toInt) (y := y.toInt) hx hy omega · have := Int.neg_self_le_ediv_of_nonneg_of_nonpos (x := x.toInt) (y := y.toInt) hx (by omega) omega · have := Int.self_le_ediv_of_nonpos_of_nonneg (x := x.toInt) (y := y.toInt) (by omega) hy omega · have := Int.ediv_nonneg_of_nonpos_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega) omega /-! ### smtSDiv -/ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y = match x.msb, y.msb with | false, false => smtUDiv x y | false, true => -(smtUDiv x (-y)) | true, false => -(smtUDiv (-x) y) | true, true => smtUDiv (-x) (-y) := by rw [BitVec.smtSDiv] rcases x.msb <;> rcases y.msb <;> simp theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← neg_one_eq_allOnes] /-! ### srem -/ theorem srem_eq (x y : BitVec w) : srem x y = match x.msb, y.msb with | false, false => x % y | false, true => x % (-y) | true, false => - ((-x) % y) | true, true => -((-x) % (-y)) := by rw [BitVec.srem] rcases x.msb <;> rcases y.msb <;> simp theorem srem_zero {x : BitVec w} : x.srem 0#w = x := by cases h : x.msb <;> simp [h, srem_eq] theorem zero_srem {x : BitVec w} : (0#w).srem x = 0#w := by cases h : x.msb <;> simp [h, srem_eq] theorem srem_one {x : BitVec w} : x.srem 1#w = 0#w := by cases h : x.msb <;> by_cases hw : w = 1 <;> (try subst hw) <;> simp_all [srem_eq] theorem srem_self {x : BitVec w} : x.srem x = 0#w := by cases h : x.msb <;> simp [h, srem_eq] /-! ### smod -/ /-- Equation theorem for `smod` in terms of `umod`. -/ theorem smod_eq (x y : BitVec w) : x.smod y = match x.msb, y.msb with | false, false => x.umod y | false, true => let u := x.umod (- y) (if u = 0#w then u else u + y) | true, false => let u := umod (- x) y (if u = 0#w then u else y - u) | true, true => - ((- x).umod (- y)) := by rw [BitVec.smod] rcases x.msb <;> rcases y.msb <;> simp @[bitvec_to_nat] theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat = match x.msb, y.msb with | false, false => (x.umod y).toNat | false, true => let u := x.umod (- y) (if u = 0#w then u.toNat else (u + y).toNat) | true, false => let u := (-x).umod y (if u = 0#w then u.toNat else (y - u).toNat) | true, true => (- ((- x).umod (- y))).toNat := by simp only [smod_eq] by_cases h : x.msb <;> by_cases h' : y.msb <;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w <;> simp only [h, h', h'', h'''] <;> simp only [umod, toNat_eq, toNat_ofNatLT, toNat_ofNat, Nat.zero_mod] at h'' h''' <;> simp theorem smod_zero {x : BitVec w} : x.smod 0#w = x := by simp only [smod_eq, msb_zero] rcases x.msb with msb | msb <;> apply eq_of_toNat_eq · simp · by_cases h : x = 0#w <;> simp [h] theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by cases _ : x.msb <;> simp_all [smod_eq] /-! ### ofBoolList -/ theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE] theorem getLsbD_ofBoolListBE : (ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by simp [getLsbD_eq_getMsbD] theorem getElem_ofBoolListBE (h : i < bs.length) : (ofBoolListBE bs)[i] = bs[bs.length - 1 - i] := by rw [← getLsbD_eq_getElem] grind theorem getLsbD_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE] theorem getMsbD_ofBoolListLE : (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by simp [getMsbD_eq_getLsbD] /-! # Rotate Left -/ /--`rotateLeft` is defined in terms of left and right shifts. -/ theorem rotateLeft_def {x : BitVec w} {r : Nat} : x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by simp only [rotateLeft, rotateLeftAux] /-- `rotateLeft` is invariant under `mod` by the bitwidth. -/ theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} : x.rotateLeft (r % w) = x.rotateLeft r := by simp only [rotateLeft, Nat.mod_mod] /-- `rotateLeft` equals the bit fiddling definition of `rotateLeftAux` when the rotation amount is smaller than the bitwidth. -/ theorem rotateLeft_eq_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) : x.rotateLeft r = x.rotateLeftAux r := by simp only [rotateLeft, Nat.mod_eq_of_lt hr] /-- Accessing bits in `x.rotateLeft r` the range `[0, r)` is equal to accessing bits `x` in the range `[w - r, w)`. Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5> (x.rotateLeft 2).getLsbD ⟨i, i < 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨i, i < 2⟩ = <6 5>[i] = <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)] = <6 5 | 4 3 2 1 0>[i + 7 - 2] -/ theorem getLsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) : (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i) := by grind [rotateLeftAux] /-- Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to accessing bits `x` in the range `[0, w - r)`. Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5> (x.rotateLeft 2).getLsbD ⟨i, i ≥ 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨i, i ≥ 2⟩ = <3 2 1 0>[i - 2] = <6 5 | 3 2 1 0>[i - 2] Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)` Then, access the bit at `i` from the right `(+i)`. -/ theorem getLsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) : (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r)) := by grind [rotateLeftAux] /-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/ theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) : (x.rotateLeft r).getLsbD i = cond (i < r) (x.getLsbD (w - r + i)) (decide (i < w) && x.getLsbD (i - r)) := by · grind [rotateLeft_eq_rotateLeftAux_of_lt, getLsbD_rotateLeftAux_of_lt, getLsbD_rotateLeftAux_of_ge] theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat} : (x.rotateLeft r).getLsbD i = cond (i < r % w) (x.getLsbD (w - (r % w) + i)) (decide (i < w) && x.getLsbD (i - (r % w))) := by rcases w with ⟨rfl, w⟩ · simp · rw [← rotateLeft_mod_eq_rotateLeft, getLsbD_rotateLeft_of_le (Nat.mod_lt _ (by omega))] theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) : (x.rotateLeft r)[i] = if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by simp [← BitVec.getLsbD_eq_getElem, h] theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) : (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i) := by grind [rotateLeftAux] theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) : (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r))) := by simp [rotateLeftAux, getMsbD_or, show i + r ≥ w by omega, show ¬i < w - r by omega] /-- If a number `w * n ≤ i < w * (n + 1)`, then `i - w * n` equals `i % w`. This is true by subtracting `w * n` from the inequality, giving `0 ≤ i - w * n < w`, which uniquely identifies `i % w`. -/ private theorem Nat.sub_mul_eq_mod_of_lt_of_le (hlo : w * n ≤ i) (hhi : i < w * (n + 1)) : i - w * n = i % w := by rw [Nat.mod_def] congr symm apply Nat.div_eq_of_lt_le (by rw [Nat.mul_comm]; omega) (by rw [Nat.mul_comm]; omega) /-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`. -/ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w): (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by rcases w with rfl | w · simp · rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)] by_cases h : n < (w + 1) - r · simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega] · simp only [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h] by_cases h₁ : n < w + 1 · simp only [h₁, decide_true, Bool.true_and] have h₂ : (r + n) < 2 * (w + 1) := by omega congr 1 rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega)] grind · grind theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} : (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by rcases w with rfl | w · simp · by_cases h : r < w · rw [getMsbD_rotateLeft_of_lt (by omega)] · rw [← rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)] simp theorem msb_rotateLeft {m w : Nat} {x : BitVec w} : (x.rotateLeft m).msb = x.getMsbD (m % w) := by grind theorem toNat_rotateLeft {x : BitVec w} {r : Nat} : (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or] theorem toInt_rotateLeft {x : BitVec w} {r : Nat} : (x.rotateLeft r).toInt = ((x <<< (r % w)).toNat ||| (x >>> (w - r % w)).toNat : Int).bmod (2 ^ w) := by simp [rotateLeft_def, toInt_or] theorem toFin_rotateLeft {x : BitVec w} {r : Nat} : (x.rotateLeft r).toFin = Fin.ofNat (2 ^ w) (x.toNat <<< (r % w)) ||| x.toFin / Fin.ofNat (2 ^ w) (2 ^ (w - r % w)) := by simp [rotateLeft_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or] /-! ## Rotate Right -/ /-- `rotateRight` is defined in terms of left and right shifts. -/ theorem rotateRight_def {x : BitVec w} {r : Nat} : x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by simp only [rotateRight, rotateRightAux] /-- Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to accessing bits `x` in the range `[r, w)`. Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2> (x.rotateLeft 2).getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <6 5 4 3 2>.getLsbD i = <6 5 4 3 2 | 1 0>[i + 2] -/ theorem getLsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) : (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i) := by grind [rotateRightAux] /-- Accessing bits in `x.rotateRight r` the range `[w-r, w)` is equal to accessing bits `x` in the range `[0, r)`. Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2> (x.rotateLeft 2).getLsbD ⟨i, i ≥ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0>.getLsbD (i - len(<6 5 4 3 2>) = <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>) -/ theorem getLsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) : (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r))) := by grind [rotateRightAux] /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is smaller than the bitwidth. -/ theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) : x.rotateRight r = x.rotateRightAux r := by simp only [rotateRight, Nat.mod_eq_of_lt hr] /-- rotateRight is invariant under `mod` by the bitwidth. -/ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} : x.rotateRight (r % w) = x.rotateRight r := by simp only [rotateRight, Nat.mod_mod] /-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/ theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) : (x.rotateRight r).getLsbD i = cond (i < w - r) (x.getLsbD (r + i)) (decide (i < w) && x.getLsbD (i - (w - r))) := by · grind [rotateRight_eq_rotateRightAux_of_lt, getLsbD_rotateRightAux_of_lt, getLsbD_rotateRightAux_of_ge] theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} : (x.rotateRight r).getLsbD i = cond (i < w - (r % w)) (x.getLsbD ((r % w) + i)) (decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by rcases w with ⟨rfl, w⟩ · simp · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))] theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) : (x.rotateRight r)[i] = if h' : i < w - (r % w) then x[(r % w) + i] else x[(i - (w - (r % w)))] := by simp [← BitVec.getLsbD_eq_getElem, getLsbD_rotateRight, h] theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) : (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight] simp [show i < r by omega] theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) : (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r)) := by simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega] /-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/ -- This should not be a simp lemma as `getMsbD_rotateRight` will apply first. theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w) : (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w) then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))) := by rcases w with rfl | w · simp · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)] by_cases h : n < m · simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true, show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, ↓reduceIte, show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and] grind · simp [getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h] by_cases h₁ : n < w + 1 · simp [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr] · simp [h₁] theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} : (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w) then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by rcases w with rfl | w · simp · by_cases h₀ : m < w · rw [getMsbD_rotateRight_of_lt (by omega)] · rw [← rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)] simp theorem msb_rotateRight {r w : Nat} {x : BitVec w} : (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by simp only [BitVec.msb, getMsbD_rotateRight] by_cases h₀ : 0 < w · simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and, ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq] intro h₁ simp [h₁] · grind theorem toNat_rotateRight {x : BitVec w} {r : Nat} : (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or] theorem toInt_rotateRight {x : BitVec w} {r : Nat} : (x.rotateRight r).toInt = ((x >>> (r % w)).toNat ||| (x <<< (w - r % w)).toNat : Int).bmod (2 ^ w) := by simp [rotateRight_def, toInt_or] theorem toFin_rotateRight {x : BitVec w} {r : Nat} : (x.rotateRight r).toFin = x.toFin / Fin.ofNat (2 ^ w) (2 ^ (r % w)) ||| Fin.ofNat (2 ^ w) (x.toNat <<< (w - r % w)) := by simp [rotateRight_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or] /- ## twoPow -/ theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by dsimp [twoPow] @[simp, bitvec_to_nat] theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by rcases w with rfl | w · simp [Nat.mod_one, toNat_of_zero_length] · simp only [twoPow, toNat_shiftLeft, toNat_ofNat] have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega) rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul] theorem toNat_twoPow_of_le {i w : Nat} (h : w ≤ i) : (twoPow w i).toNat = 0 := by rw [toNat_twoPow] apply Nat.mod_eq_zero_of_dvd exact Nat.pow_dvd_pow_iff_le_right'.mpr h theorem toNat_twoPow_of_lt {i w : Nat} (h : i < w) : (twoPow w i).toNat = 2^i := by rw [toNat_twoPow] apply Nat.mod_eq_of_lt apply Nat.pow_lt_pow_of_lt (by omega) (by omega) theorem toNat_twoPow_eq_ite {i w : Nat} : (twoPow w i).toNat = if i < w then 2^i else 0 := by by_cases h : i < w · simp only [h, toNat_twoPow_of_lt, if_true] · simp only [h, if_false] rw [toNat_twoPow_of_le (by omega)] theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j)) := by rcases w with rfl | w · simp · simp only [twoPow, getLsbD_shiftLeft, getLsbD_ofNat] by_cases hj : j < i · simp only [hj, decide_true, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not] grind · by_cases hi : Nat.testBit 1 (j - i) · obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi have hij : j = i := by omega grind · have hij : i ≠ j := by intro h; subst h grind grind theorem msb_twoPow {i w: Nat} : (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by grind theorem toInt_twoPow {w i : Nat} : (BitVec.twoPow w i).toInt = if w ≤ i then 0 else if i + 1 = w then (-(2^i : Nat) : Int) else 2^i := by simp only [BitVec.toInt_eq_msb_cond, toNat_twoPow_eq_ite] rcases w with _ | w · simp · by_cases h : i = w · simp [h, show ¬ (w + 1 ≤ w) by omega] omega · by_cases h' : w + 1 ≤ i · simp [h', show ¬ i < w + 1 by omega] · simp [h, h', show i < w + 1 by omega, Int.natCast_pow] theorem toFin_twoPow {w i : Nat} : (BitVec.twoPow w i).toFin = Fin.ofNat (2^w) (2^i) := by rcases w with rfl | w · simp [BitVec.twoPow, Fin.fin_one_eq_zero] · simp [BitVec.twoPow, toFin_shiftLeft, Nat.shiftLeft_eq] theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i) := by grind [=_ getLsbD_eq_getElem] theorem getMsbD_twoPow {i j w: Nat} : (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by grind theorem and_twoPow (x : BitVec w) (i : Nat) : x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by grind theorem twoPow_and (x : BitVec w) (i : Nat) : (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by grind theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) : x * (twoPow w i) = x <<< i := by apply eq_of_toNat_eq simp only [toNat_mul, toNat_twoPow, Nat.mul_mod_mod, Nat.shiftLeft_eq, toNat_shiftLeft] theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) : (twoPow w i) * x = x <<< i := by rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft] theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by grind theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) : x <<< n = x * (BitVec.twoPow w n) := by ext i simp [mul_twoPow_eq_shiftLeft] /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/ theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by apply BitVec.eq_of_toNat_eq simp only [toNat_mul, toNat_twoPow] rw [← Nat.mul_mod, Nat.pow_add] /-- The unsigned division of `x` by `2^k` equals shifting `x` right by `k`, when `k` is less than the bitwidth `w`. -/ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / (twoPow w k) = x >>> k := by have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk simp [bitvec_to_nat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this] theorem toInt_mul_toInt_le {x y : BitVec w} : x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2) := by rcases w with _|w · simp [of_length_zero] · have xlt := two_mul_toInt_lt (x := x); have xle := le_two_mul_toInt (x := x) have ylt := two_mul_toInt_lt (x := y); have yle := le_two_mul_toInt (x := y) have h : 2 ^ ((w + 1) * 2 - 2) = 2 ^ ((w + 1) - 1) * 2 ^ ((w + 1) - 1) := by rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w + 1) - 1), Nat.mul_sub_one, Nat.mul_comm] rw_mod_cast [h] rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle exact Int.mul_le_mul_of_natAbs_le (by omega) (by omega) theorem le_toInt_mul_toInt {x y : BitVec w} : - (2 ^ (w * 2 - 2)) ≤ x.toInt * y.toInt := by rcases w with _|w · simp [of_length_zero] · have xlt := two_mul_toInt_lt (x := x); have xle := le_two_mul_toInt (x := x) have ylt := two_mul_toInt_lt (x := y); have yle := le_two_mul_toInt (x := y) have h : 2 ^ ((w + 1) * 2 - 2) = 2 ^ ((w + 1) - 1) * 2 ^ ((w + 1) - 1) := by rw [← Nat.pow_add, ←Nat.mul_two, Nat.mul_comm (m := 2) (n := (w + 1) - 1), Nat.mul_sub_one, Nat.mul_comm] rw_mod_cast [h] rw [← Nat.two_pow_pred_mul_two (by omega), Int.natCast_mul] at xlt ylt xle yle exact Int.neg_mul_le_mul (by omega) (by omega) (by omega) (by omega) theorem shiftLeft_neg {x : BitVec w} {y : Nat} : (-x) <<< y = - (x <<< y) := by rw [shiftLeft_eq_mul_twoPow, shiftLeft_eq_mul_twoPow, BitVec.neg_mul] /- ### cons -/ theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by grind theorem false_cons_zero : cons false 0#w = 0#(w + 1) := by grind theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by grind /- ### setWidth, setWidth, and bitwise operations -/ /-- When the `(i+1)`th bit of `x` is false, keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits. -/ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) : setWidth w (x.setWidth (i + 1)) = setWidth w (x.setWidth i) := by grind /-- When the `(i+1)`th bit of `x` is true, keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits and then performing bitwise-or with `twoPow i = (1 << i)`, -/ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) : setWidth w (x.setWidth (i + 1)) = setWidth w (x.setWidth i) ||| (twoPow w i) := by grind /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} : (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by grind theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by grind theorem replicate_one {w : Nat} {x : BitVec w} : (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by simp only [replicate]; rw [append_zero_width] theorem replicate_succ {x : BitVec w} : x.replicate (n + 1) = (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by simp [replicate] theorem getLsbD_replicate {n w : Nat} {x : BitVec w} : (x.replicate n).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w)) := by induction n generalizing x case zero => simp case succ n ih => simp only [replicate_succ, getLsbD_cast, getLsbD_append] by_cases hi : i < w * (n + 1) · simp only [hi, decide_true, Bool.true_and] by_cases hi' : i < w * n · grind · simp only [hi', ↓reduceIte] rw [Nat.sub_mul_eq_mod_of_lt_of_le (by omega) (by omega)] · rw [Nat.mul_succ] at hi ⊢ grind theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) : (x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega)) := by grind [=_ getLsbD_eq_getElem, getLsbD_replicate] theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} : (x₁ ++ x₂) ++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega) := by grind theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} : (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by grind theorem replicate_append_self {x : BitVec w} : x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by induction n with | zero => grind | succ n ih => rw [replicate_succ] conv => lhs; rw [ih] simp only [BitVec.cast_cast, BitVec.cast_eq] rw [← cast_append_left] · grind · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega theorem replicate_succ' {x : BitVec w} : x.replicate (n + 1) = (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by simp [replicate_append_self] theorem BitVec.setWidth_add_eq_mod {x y : BitVec w} : BitVec.setWidth i (x + y) = (BitVec.setWidth i x + BitVec.setWidth i y) % (BitVec.twoPow i w) := by apply BitVec.eq_of_toNat_eq rw [toNat_setWidth] simp only [toNat_setWidth, toNat_add, toNat_umod, Nat.add_mod_mod, Nat.mod_add_mod, toNat_twoPow] by_cases h : i ≤ w · rw [Nat.mod_eq_zero_of_dvd (Nat.pow_dvd_pow 2 h), Nat.mod_zero, Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 h)] · have hk : 2 ^ w < 2 ^ i := Nat.pow_lt_pow_of_lt (by decide) (Nat.lt_of_not_le h) rw [Nat.mod_eq_of_lt hk, Nat.mod_mod_eq_mod_mod_of_dvd (Nat.pow_dvd_pow _ (Nat.le_of_not_le h))] /-! ### intMin -/ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) := by grind [intMin] theorem getMsbD_intMin {w i : Nat} : (intMin w).getMsbD i = (decide (0 < w) && decide (i = 0)) := by grind /-- The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`. -/ @[simp, bitvec_to_nat] theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by simp [intMin] theorem toNat_intMin_of_pos (hw : 0 < w) : (intMin w).toNat = 2 ^ (w - 1) := by rw [toNat_intMin, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt (by decide) (Nat.sub_one_lt_of_lt hw))] theorem intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0 := by by_cases h : w = 0 · subst h decide +revert · constructor · have := Nat.two_pow_pos (w - 1) simp [toNat_eq, show 0 < w by omega] · simp [h] /-- The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`. -/ theorem toInt_intMin {w : Nat} : (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by by_cases h : w = 0 · subst h simp [BitVec.toInt] · have w_pos : 0 < w := by omega simp only [BitVec.toInt, toNat_intMin, w_pos, Nat.two_pow_pred_mod_two_pow, Int.two_pow_pred_sub_two_pow, ite_eq_right_iff] rw [Nat.mul_comm] simp [w_pos] theorem toInt_intMin_of_pos {v : Nat} (hv : 0 < v) : (intMin v).toInt = -2 ^ (v - 1) := by rw [toInt_intMin, Nat.mod_eq_of_lt] · simp [Int.natCast_pow] · rw [Nat.pow_lt_pow_iff_right (by omega)] omega theorem toInt_intMin_le (x : BitVec w) : (intMin w).toInt ≤ x.toInt := by cases w case zero => simp [toInt_intMin, @of_length_zero x] case succ w => simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod] have : 0 < 2 ^ w := Nat.two_pow_pos w rw [Int.emod_eq_of_lt (by omega) (by omega)] rw [BitVec.toInt_eq_toNat_bmod] rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega] apply Int.le_bmod (by omega) theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by simp only [BitVec.sle, toInt_intMin_le x, decide_true] theorem neg_intMin {w : Nat} : -intMin w = intMin w := by by_cases h : 0 < w · simp [bitvec_to_nat, h] · simp only [Nat.not_lt, Nat.le_zero_eq] at h simp [bitvec_to_nat, h] theorem neg_eq_intMin {x : BitVec w} : -x = intMin w ↔ x = intMin w := by rw [← BitVec.neg_inj, neg_neg, neg_intMin] theorem neg_ne_intMin_inj {x : BitVec w} : -x ≠ intMin w ↔ x ≠ intMin w := by rw [←neg_intMin, neg_ne_iff_ne_neg, neg_neg, neg_intMin] theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by simp [BitVec.abs, bitvec_to_nat] theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) : (-x).toInt = -(x.toInt) := by simp only [ne_eq, toNat_eq, toNat_intMin] at rs by_cases x_zero : x = 0 · subst x_zero simp [BitVec.toInt] omega by_cases w_0 : w = 0 · subst w_0 simp [BitVec.eq_nil x] have : 0 < w := by omega rw [Nat.two_pow_pred_mod_two_pow (by omega)] at rs simp only [BitVec.toInt, BitVec.toNat_neg, BitVec.sub_toNat_mod_cancel x_zero] have := @Nat.two_pow_pred_mul_two w (by omega) split <;> split <;> omega theorem toInt_neg_eq_ite {x : BitVec w} : (-x).toInt = if x = intMin w then x.toInt else -(x.toInt) := by by_cases hx : x = intMin w <;> simp [hx, neg_intMin, toInt_neg_of_ne_intMin] theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by grind theorem ne_intMin_of_msb_eq_false (h : 0 < w) {n : BitVec w} (hn : n.msb = false) : n ≠ intMin w := by rintro rfl simp only [msb_intMin, decide_eq_false_iff_not, Nat.not_lt, Nat.le_zero_eq] at hn omega theorem toInt_neg_eq_of_msb {x : BitVec w} (h : x.msb = false) : (-x).toInt = -x.toInt := by match w with | 0 => rw [of_length_zero (x := x), neg_zero, toInt_zero, Int.neg_zero] | w' + 1 => exact toInt_neg_of_ne_intMin (ne_intMin_of_msb_eq_false (Nat.zero_lt_succ _) h) theorem lt_intMin_iff_msb_eq_false {x : BitVec w} (hw : 0 < w) : x < intMin w ↔ x.msb = false := by simp only [msb_eq_false_iff_two_mul_lt, toNat_intMin_of_pos hw, lt_def] rw [← Nat.mul_lt_mul_left (by decide : 0 < 2), ← Nat.pow_add_one', Nat.sub_one_add_one_eq_of_pos hw] theorem intMin_le_iff_msb_eq_true {x : BitVec w} (hw : 0 < w) : intMin w ≤ x ↔ x.msb = true := by rw [← Decidable.not_iff_not, BitVec.not_le, Bool.not_eq_true] exact lt_intMin_iff_msb_eq_false hw theorem le_intMin_of_msb_eq_false {x : BitVec w} (hx : x.msb = false) : x ≤ intMin w := by match w with | 0 => exact le_of_zero_length rfl | w' + 1 => apply BitVec.le_of_lt exact (lt_intMin_iff_msb_eq_false (Nat.zero_lt_succ _)).mpr hx theorem neg_le_intMin_of_msb_eq_true {x : BitVec w} (hx : x.msb = true) : -x ≤ intMin w := by match w with | 0 => exact le_of_zero_length rfl | w' + 1 => rw [le_def, toNat_neg_of_pos (pos_of_msb hx), toNat_intMin_of_pos (Nat.zero_lt_succ _)] simp only [Nat.succ_eq_add_one, Nat.add_one_sub_one, Nat.pow_add_one] rw [msb_eq_true_iff_two_mul_ge, Nat.pow_add_one] at hx omega /-! ### intMax -/ @[simp, bitvec_to_nat] theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1 := by simp only [intMax] by_cases h : w = 0 · simp [h] · have h' : 0 < w := by omega rw [toNat_sub, toNat_twoPow, ← Nat.sub_add_comm (by simpa [h'] using Nat.one_le_two_pow), Nat.add_sub_assoc (by simpa [h'] using Nat.one_le_two_pow), Nat.two_pow_pred_mod_two_pow h', ofNat_eq_ofNat, toNat_ofNat, Nat.one_mod_two_pow h', Nat.add_mod_left, Nat.mod_eq_of_lt] have := Nat.two_pow_pred_lt_two_pow h' have := Nat.two_pow_pos w omega theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := by rw [← testBit_toNat, toNat_intMax, Nat.testBit_two_pow_sub_one, decide_eq_decide] omega theorem intMax_add_one {w : Nat} : intMax w + 1#w = intMin w := by simp only [toNat_eq, toNat_intMax, toNat_add, toNat_intMin, toNat_ofNat, Nat.add_mod_mod] by_cases h : w = 0 · simp [h] · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)] theorem toInt_intMax : (BitVec.intMax w).toInt = 2 ^ (w - 1) - 1 := by refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [BitVec.toInt_of_zero_length]) (fun hw => ?_) rw [BitVec.toInt, toNat_intMax, if_pos] · rw [Int.ofNat_sub Nat.one_le_two_pow, Int.natCast_pow, Int.cast_ofNat_Int, Int.cast_ofNat_Int] · rw [Nat.mul_sub_left_distrib, ← Nat.pow_succ', Nat.succ_eq_add_one, Nat.sub_add_cancel hw] apply Nat.sub_lt_self (by decide) rw [Nat.mul_one] apply Nat.le_pow hw /-! ### Non-overflow theorems -/ /-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/ theorem toNat_add_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_add, Nat.mod_eq_of_lt h] /-- If `y ≤ x`, then the subtraction `(x - y)` does not overflow. Thus, `(x - y).toNat = x.toNat - y.toNat` -/ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) : (x - y).toNat = x.toNat - y.toNat := by simp only [toNat_sub] rw [BitVec.le_def] at h by_cases h' : x.toNat = y.toNat · rw [h', Nat.sub_self, Nat.sub_add_cancel (by omega), Nat.mod_self] · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)] /-- If `y > x`, then the subtraction `(x - y)` *does* overflow, and the result is the wraparound. Thus, `(x - y).toNat = 2^w - (y.toNat - x.toNat)`. -/ theorem toNat_sub_of_lt {x y : BitVec w} (h : x < y) : (x - y).toNat = 2^w - (y.toNat - x.toNat) := by simp only [toNat_sub] rw [Nat.mod_eq_of_lt (by bv_omega)] bv_omega /-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. Thus, `(x * y).toNat = 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] theorem toNat_mul_toNat_lt {x y : BitVec w} : x.toNat * y.toNat < 2 ^ (w * 2) := by have := BitVec.isLt x; have := BitVec.isLt y simp only [Nat.mul_two, Nat.pow_add] exact Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega) /-- `x ≤ y + z` if and only if `x - z ≤ y` when `x - z` and `y + z` do not overflow. -/ theorem le_add_iff_sub_le {x y z : BitVec w} (hxz : z ≤ x) (hbz : y.toNat + z.toNat < 2^w) : x ≤ y + z ↔ x - z ≤ y := by simp_all only [BitVec.le_def] rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega), BitVec.toNat_add_of_lt (by omega)] omega /-- `x - z ≤ y - z` if and only if `x ≤ y` when `x - z` and `y - z` do not overflow. -/ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) : (x - z ≤ y - z) ↔ x ≤ y := by simp_all only [BitVec.le_def] rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega), BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)] omega theorem sdiv_neg_one {w : Nat} {x : BitVec w} : x.toInt / -1 = -x.toInt := by rcases w with _|w · simp [of_length_zero] · simp theorem sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) : sdivOverflow x y = negOverflow x := by rcases w with _|w · simp [sdivOverflow, negOverflow, of_length_zero] · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x) simp only [sdivOverflow, hy, negOverflow] by_cases hx : x.toInt = - 2 ^ w · simp [hx] · simp [show ¬x.toInt == -2 ^ w by simp only [beq_iff_eq, hx, not_false_eq_true]]; omega theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} : 2 ^ (w - 1) ≤ x.toInt * y.toInt ↔ (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) := by rcases w with _|w · simp [of_length_zero] · have := Int.pow_lt_pow_of_lt (a := 2) (b := (w + 1) * 2 - 2) (c := (w + 1) * 2 - 1) (by omega) have := @BitVec.le_toInt_mul_toInt (w + 1) x y have := @BitVec.toInt_mul_toInt_le (w + 1) x y simp only [Nat.add_one_sub_one, BitVec.slt, intMax, ofNat_eq_ofNat, toInt_mul, decide_eq_true_eq] repeat rw [BitVec.toInt_signExtend_of_le (by omega)] simp only [show BitVec.twoPow (w + 1) w - 1#(w + 1) = BitVec.intMax (w + 1) by simp [intMax], toInt_intMax, Nat.add_one_sub_one] push_cast rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.bmod_eq_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega) (by rw [← Nat.mul_two]; push_cast; omega)] omega theorem toInt_mul_toInt_lt_neg_two_pow_iff {x y : BitVec w} : x.toInt * y.toInt < - 2 ^ (w - 1) ↔ (signExtend (w * 2) x * signExtend (w * 2) y).slt (signExtend (w * 2) (intMin w)) := by rcases w with _|w · simp [of_length_zero] · have := Int.pow_lt_pow_of_lt (a := 2) (b := (w + 1) * 2 - 2) (c := (w + 1) * 2 - 1) (by omega) have := @BitVec.le_toInt_mul_toInt (w + 1) x y have := @BitVec.toInt_mul_toInt_le (w + 1) x y simp only [BitVec.slt, toInt_mul, intMin, Nat.add_one_sub_one, decide_eq_true_eq] repeat rw [BitVec.toInt_signExtend_of_le (by omega)] simp only [toInt_twoPow, show ¬w + 1 ≤ w by omega, ↓reduceIte] push_cast rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.bmod_eq_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega) (by rw [← Nat.mul_two]; push_cast; omega)] /-! ### neg -/ theorem msb_eq_toInt {x : BitVec w}: x.msb = decide (x.toInt < 0) := by by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond, -Int.natCast_pow] <;> omega theorem msb_eq_toNat {x : BitVec w}: x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by simp only [msb_eq_decide, ge_iff_le] /-- Negating a bitvector created from a natural number equals creating a bitvector from the negative of that number. -/ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} : - BitVec.ofNat w x = BitVec.ofInt w (- x) := by apply BitVec.eq_of_toInt_eq simp [BitVec.toInt_neg, BitVec.toInt_ofNat'] theorem neg_toInt_neg {x : BitVec w} (h : x.msb = false) : -(-x).toInt = x.toNat := by simp [toInt_neg_eq_of_msb h, toInt_eq_toNat_of_msb, h] theorem toNat_pos_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) : 0 < x.toNat := by simp [toNat_eq] at hx; omega theorem toNat_neg_lt_of_msb (x : BitVec w) (hmsb : x.msb = true) : (-x).toNat ≤ 2^(w-1) := by rcases w with _|w · simp [BitVec.eq_nil x] · by_cases hx : x = 0#(w + 1) · simp [hx] · have := BitVec.le_toNat_of_msb_true hmsb have := toNat_pos_of_ne_zero hx rw [toNat_neg, Nat.mod_eq_of_lt (by omega), ← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul] omega /-! ### abs -/ theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl @[simp, bitvec_to_nat] theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by simp only [BitVec.abs, neg_eq] by_cases h : x.msb = true · simp only [h, ↓reduceIte, toNat_neg] have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h rw [Nat.mod_eq_of_lt (by omega)] · simp [h] theorem getLsbD_abs {i : Nat} {x : BitVec w} : getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by grind [BitVec.abs] theorem getElem_abs {i : Nat} {x : BitVec w} (h : i < w) : x.abs[i] = if x.msb then (-x)[i] else x[i] := by grind [BitVec.abs] theorem getMsbD_abs {i : Nat} {x : BitVec w} : getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i := by grind /- The absolute value of `x : BitVec w` is naively a case split on the sign of `x`. However, recall that when `x = intMin w`, `-x = x`. Thus, the full value of `abs x` is computed by the case split: - If `x : BitVec w` is `intMin`, then its absolute value is also `intMin w`, and thus `toInt` will equal `intMin.toInt`. - Otherwise, if `x` is negative, then `x.abs.toInt = (-x).toInt`. - If `x` is positive, then it is equal to `x.abs.toInt = x.toInt`. -/ theorem toInt_abs_eq_ite {x : BitVec w} : x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb then -x.toInt else x.toInt := by by_cases hx : x = intMin w · simp [hx] · simp [hx] by_cases hx₂ : x.msb · simp [hx₂, abs_eq, toInt_neg_of_ne_intMin hx] · simp [hx₂, abs_eq] /- The absolute value of `x : BitVec w` is a case split on the sign of `x`, when `x ≠ intMin w`. This is a variant of `toInt_abs_eq_ite`. -/ theorem toInt_abs_eq_ite_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) : x.abs.toInt = if x.msb then -x.toInt else x.toInt := by simp [toInt_abs_eq_ite, hx] /-- The absolute value of `x : BitVec w`, interpreted as an integer, is a case split: - When `x = intMin w`, then `x.abs = intMin w` - Otherwise, `x.abs.toInt` equals the absolute value (`x.toInt.natAbs`). This is a simpler version of `BitVec.toInt_abs_eq_ite`, which hides a case split on `x.msb`. -/ theorem toInt_abs_eq_natAbs {x : BitVec w} : x.abs.toInt = if x = intMin w then (intMin w).toInt else x.toInt.natAbs := by rw [toInt_abs_eq_ite] by_cases hx : x = intMin w · simp [hx] · simp [hx] by_cases h : x.msb · simp only [h, ↓reduceIte] have : x.toInt < 0 := by rw [toInt_neg_iff] have := msb_eq_true_iff_two_mul_ge.mp h omega omega · simp only [h, Bool.false_eq_true, ↓reduceIte] have : 0 ≤ x.toInt := by rw [toInt_pos_iff] exact msb_eq_false_iff_two_mul_lt.mp (by simp [h]) omega /- The absolute value of `(x : BitVec w)`, when interpreted as an integer, is the absolute value of `x.toInt` when `(x ≠ intMin)`. -/ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) : x.abs.toInt = x.toInt.natAbs := by simp [toInt_abs_eq_natAbs, hx] theorem toFin_abs {x : BitVec w} : x.abs.toFin = if x.msb then Fin.ofNat (2 ^ w) (2 ^ w - x.toNat) else x.toFin := by by_cases h : x.msb <;> simp [BitVec.abs, h] /-! ### Reverse -/ theorem getLsbD_reverse {i : Nat} {x : BitVec w} : (x.reverse).getLsbD i = x.getMsbD i := by induction w generalizing i case zero => grind case succ n ih => cases i <;> grind [reverse] theorem getElem_reverse (x : BitVec w) (h : i < w) : x.reverse[i] = x.getMsbD i := by grind [=_ getLsbD_eq_getElem] theorem getMsbD_reverse {i : Nat} {x : BitVec w} : (x.reverse).getMsbD i = x.getLsbD i := by grind theorem msb_reverse {x : BitVec w} : (x.reverse).msb = x.getLsbD 0 := by grind theorem reverse_append {x : BitVec w} {y : BitVec v} : (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega) := by grind theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) : (x.cast h).reverse = x.reverse.cast h := by grind theorem reverse_replicate {n : Nat} {x : BitVec w} : (x.replicate n).reverse = (x.reverse).replicate n := by induction n with | zero => rfl | succ n ih => conv => lhs; simp only [replicate_succ'] simp [reverse_append, ih] theorem getMsbD_replicate {n w : Nat} {x : BitVec w} : (x.replicate n).getMsbD i = (decide (i < w * n) && x.getMsbD (i % w)) := by rw [← getLsbD_reverse, reverse_replicate, getLsbD_replicate, getLsbD_reverse] theorem msb_replicate {n w : Nat} {x : BitVec w} : (x.replicate n).msb = (decide (0 < n) && x.msb) := by simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod] cases n <;> cases w <;> simp /-! ### Count leading zeros -/ theorem clzAuxRec_zero (x : BitVec w) : x.clzAuxRec 0 = if x.getLsbD 0 then BitVec.ofNat w (w - 1) else BitVec.ofNat w w := by rfl theorem clzAuxRec_succ (x : BitVec w) : x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) then BitVec.ofNat w (w - 1 - (n + 1)) else BitVec.clzAuxRec x n := by rfl theorem clzAuxRec_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) : x.clzAuxRec n = x.clzAuxRec (w - 1) := by let k := n - (w - 1) rw [show n = (w - 1) + k by omega] induction k case zero => simp case succ k ihk => simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk, show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]] /-! ### Inequalities (le / lt) -/ theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by simp [BitVec.ule, BitVec.ult, ← decide_not] /-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide -/ theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) : x.slt y = x.ult y := by simp only [BitVec.slt, toInt_eq_msb_cond, BitVec.ult, decide_eq_decide, h] cases y.msb <;> simp /-- If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit -/ theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) : x.ult y = y.msb := by simp only [BitVec.ult, msb_eq_decide, ne_eq, decide_eq_decide] at * omega /-- If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites -/ theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) : x.slt y = !x.ult y := by simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h] cases y.msb <;> (simp [-Int.natCast_pow]; omega) theorem slt_eq_ult {x y : BitVec w} : x.slt y = (x.msb != y.msb).xor (x.ult y) := by by_cases h : x.msb = y.msb · simp [h, slt_eq_ult_of_msb_eq] · have h' : x.msb != y.msb := by simp_all simp [slt_eq_not_ult_of_msb_neq h, h'] theorem sle_eq_not_slt {x y : BitVec w} : x.sle y = !y.slt x := by simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]; omega theorem zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb := by rw [sle_eq_not_slt, BitVec.slt_zero_eq_msb] theorem zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : BitVec.sle 0#w x ↔ x.msb = false := by simp [zero_sle_eq_not_msb] theorem toNat_toInt_of_sle {w : Nat} {x : BitVec w} (hx : BitVec.sle 0#w x) : x.toInt.toNat = x.toNat := toNat_toInt_of_msb x (zero_sle_iff_msb_eq_false.1 hx) theorem sle_eq_ule {x y : BitVec w} : x.sle y = (x.msb != y.msb ^^ x.ule y) := by rw [sle_eq_not_slt, slt_eq_ult, ← Bool.xor_not, ← ule_eq_not_ult, bne_comm] theorem sle_eq_ule_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) : x.sle y = x.ule y := by simp [BitVec.sle_eq_ule, h] end BitVec'