Bitvector utilities

This file contains definitions and lemmas for working with bitvectors. These lemmas are true in general, but the general proofs are much harder. So, we prove them only for the specific bitwidths we need.

@[simp]

theorem BitVec.toInt_ofInt64_toBitVec {bv : BitVec 64} : (Int64.ofInt bv.toInt).toBitVec = bv

@[simp]

theorem BitVec.Int64_toBitVec_toInt_eq_toInt (x : Int64) : x.toBitVec.toInt = x.toInt

theorem BitVec.eq_iff_UInt64_toInt64_eq_64 {bv₁ bv₂ : BitVec 64} : bv₁ = bv₂ ↔ { toBitVec := bv₁ }.toInt64 = { toBitVec := bv₂ }.toInt64

theorem BitVec.toInt_min_64 {bv : BitVec 64} : signedMin 64 ≤ bv.toInt

theorem BitVec.toInt_max_64 {bv : BitVec 64} : bv.toInt ≤ signedMax 64

theorem BitVec.toInt_ge_INT64_MIN (bv : BitVec 64) : Int64.MIN ≤ bv.toInt

theorem BitVec.toInt_le_INT64_MAX (bv : BitVec 64) : bv.toInt ≤ Int64.MAX

theorem BitVec.signedMin_eq_INT64_MIN : signedMin 64 = Int64.MIN

theorem BitVec.signedMax_eq_INT64_MAX : signedMax 64 = Int64.MAX

@[simp]

theorem BitVec.toInt_ofInt_64 {bv : BitVec 64} : BitVec.ofInt 64 bv.toInt = bv

theorem BitVec.overflows_false_64 {i : Int} : Int64.MIN ≤ i ∧ i ≤ Int64.MAX ↔ overflows 64 i = false

theorem BitVec.overflows_true_64 {i : Int} : ¬(Int64.MIN ≤ i ∧ i ≤ Int64.MAX) ↔ overflows 64 i = true

theorem BitVec.Int64_ofInt?_eq_none_iff_overflows {i : Int} : Int64.ofInt? i = none ↔ overflows 64 i = true

theorem BitVec.neg_toInt_eq_neg_64 {bv : BitVec 64} {i : Int64} (h₁ : Int64.MIN ≤ -i.toInt ∧ -i.toInt ≤ Int64.MAX) (h₂ : bv.toInt = i.toInt) : (-bv).toInt = -i.toInt

theorem BitVec.add_toInt_eq_add_64 {bv₁ bv₂ : BitVec 64} {i₁ i₂ : Int64} (h₀ : Int64.MIN ≤ i₁.toInt + i₂.toInt ∧ i₁.toInt + i₂.toInt ≤ Int64.MAX) (h₁ : bv₁.toInt = i₁.toInt) (h₂ : bv₂.toInt = i₂.toInt) : (bv₁ + bv₂).toInt = i₁.toInt + i₂.toInt

theorem BitVec.sub_toInt_eq_sub_64 {bv₁ bv₂ : BitVec 64} {i₁ i₂ : Int64} (h₀ : Int64.MIN ≤ i₁.toInt - i₂.toInt ∧ i₁.toInt - i₂.toInt ≤ Int64.MAX) (h₁ : bv₁.toInt = i₁.toInt) (h₂ : bv₂.toInt = i₂.toInt) : (bv₁ - bv₂).toInt = i₁.toInt - i₂.toInt

theorem BitVec.mul_eq_toInt_mul_ofInt_64 {bv₁ bv₂ : BitVec 64} : bv₁ * bv₂ = BitVec.ofInt 64 (bv₁.toInt * bv₂.toInt)

theorem BitVec.mul_toInt_eq_mul_64 {bv₁ bv₂ : BitVec 64} {i₁ i₂ : Int64} (h₀ : Int64.MIN ≤ i₁.toInt * i₂.toInt ∧ i₁.toInt * i₂.toInt ≤ Int64.MAX) (h₁ : bv₁.toInt = i₁.toInt) (h₂ : bv₂.toInt = i₂.toInt) : (bv₁ * bv₂).toInt = i₁.toInt * i₂.toInt

theorem BitVec.mul_toInt_eq_toInt_mul {bv₁ bv₂ : BitVec 64} (h : Int64.MIN ≤ bv₁.toInt * bv₂.toInt ∧ bv₁.toInt * bv₂.toInt ≤ Int64.MAX) : (bv₁ * bv₂).toInt = bv₁.toInt * bv₂.toInt

theorem BitVec.sdiv_pos_lt_INT64_MAX {bv₁ bv₂ : BitVec 64} (h : 1 < bv₂.toInt) : (bv₁.sdiv bv₂).toInt < Int64.MAX

theorem BitVec.sdiv_pos_gt_INT64_MIN {bv₁ bv₂ : BitVec 64} (h : 1 < bv₂.toInt) : Int64.MIN < (bv₁.sdiv bv₂).toInt

theorem BitVec.toInt_sdiv_eq_tdiv_toInt {bv₁ bv₂ : BitVec 64} (h₀ : 0 < bv₂.toInt) : (bv₁.sdiv bv₂).toInt = bv₁.toInt.tdiv bv₂.toInt

theorem BitVec.sdiv_pos_bounded {bv₁ bv₂ : BitVec 64} (h₀ : 0 < bv₂.toInt) : Int64.MIN.tdiv bv₂.toInt ≤ (bv₁.sdiv bv₂).toInt ∧ (bv₁.sdiv bv₂).toInt ≤ Int64.MAX.tdiv bv₂.toInt

theorem BitVec.mul_toInt_sdiv_eq_toInt_mul_sdiv {bv₁ bv₂ : BitVec 64} (h : 0 < bv₂.toInt) : bv₂.toInt * (bv₁.sdiv bv₂).toInt = (bv₂ * bv₁.sdiv bv₂).toInt

theorem BitVec.smtSDiv_eq_sdiv {n : Nat} {bv₁ bv₂ : BitVec n} (h : bv₂ ≠ 0) : bv₁.smtSDiv bv₂ = bv₁.sdiv bv₂

theorem BitVec.bvule_iff_le {n : Nat} {bv₁ bv₂ : BitVec n} : bv₁.ule bv₂ = decide (bv₁ ≤ bv₂)

theorem Int.bmod_bounded_eq_self {n : Nat} {i : Int} (hlow : -2 ^ n ≤ i) (hhigh : i ≤ 2 ^ n - 1) : i.bmod (2 ^ (n + 1)) = i