This module contains the `BitVec` simplifying part of the `bv_normalize` simp set.

source
theorem Std.Tactic.BVDecide.Normalize.BitVec.le_ult {w : Nat} (x y : BitVec w) :
x ≤ y ↔ (!y.ult x) = true
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.gt_ult {w : Nat} (x y : BitVec w) :
x > y ↔ y.ult x = true
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ge_ule {w : Nat} (x y : BitVec w) :
x ≥ y ↔ (!x.ult y) = true
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.slt_eq_ult {w : Nat} (x y : BitVec w) :
x.slt y = (!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ x.ult y)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.sle_eq_ult {w : Nat} (x y : BitVec w) :
x.sle y = !(!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ y.ult x)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ofNatLT_reduce {w : Nat} (n : Nat) (h : n < 2 ^ w) :
n#'h = BitVec.ofNat w n
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_if (b : Bool) :
BitVec.ofBool b = bif b then 1#1 else 0#1
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.sdiv_udiv {w : Nat} (x y : BitVec w) :
x.sdiv y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -x / -y else -(-x / y) else bif y.getLsbD (w - 1) then -(x / -y) else x / y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.smod_umod {w : Nat} (x y : BitVec w) :
x.smod y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y else bif y.getLsbD (w - 1) then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.smtSDiv_smtUDiv {w : Nat} (x y : BitVec w) :
x.smtSDiv y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then (-x).smtUDiv (-y) else -(-x).smtUDiv y else bif y.getLsbD (w - 1) then -x.smtUDiv (-y) else x.smtUDiv y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.srem_umod {w : Nat} (x y : BitVec w) :
x.srem y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else -(-x % y) else bif y.getLsbD (w - 1) then x % -y else x % y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.abs_eq {w : Nat} (x : BitVec w) :
x.abs = bif x.getLsbD (w - 1) then -x else x
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD {w : Nat} (a : BitVec w) (i : Nat) (h : i < w) :
a[i] = a.getLsbD i
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_and {w : Nat} (a : BitVec w) :
-1#w &&& a = a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_ones {w : Nat} (a : BitVec w) :
a &&& -1#w = a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.one_plus_not_eq_not_plus_one {w : Nat} (x : BitVec w) :
1#w + ~~~x = ~~~x + 1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra {w : Nat} (a : BitVec w) :
a &&& ~~~a = 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra' {w : Nat} (a : BitVec w) :
~~~a &&& a = 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_not {w : Nat} (a : BitVec w) :
a + ~~~a = -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_add {w : Nat} (a : BitVec w) :
~~~a + a = -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg {w : Nat} (a : BitVec w) :
a + (~~~a + 1#w) = 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add {w : Nat} (a : BitVec w) :
~~~a + 1#w + a = 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg {w : Nat} (x : BitVec w) :
~~~(~~~x + 1#w) = x + -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg' {w : Nat} (x : BitVec w) :
~~~(x + 1#w) = ~~~x + -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg'' {w : Nat} (x : BitVec w) :
~~~(1#w + x) = ~~~x + -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_same {w : Nat} (a : BitVec w) :
a + a = a * 2#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left {w a b : Nat} {c : BitVec w} :
BitVec.ofNat w a + (BitVec.ofNat w b + c) = BitVec.ofNat w a + BitVec.ofNat w b + c
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right {w a : Nat} {b : BitVec w} {c : Nat} :
BitVec.ofNat w a + (b + BitVec.ofNat w c) = BitVec.ofNat w a + BitVec.ofNat w c + b
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left' {w a : Nat} {b : BitVec w} {c : Nat} :
BitVec.ofNat w a + b + BitVec.ofNat w c = BitVec.ofNat w a + BitVec.ofNat w c + b
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' {w b c : Nat} {a : BitVec w} :
a + BitVec.ofNat w b + BitVec.ofNat w c = BitVec.ofNat w b + BitVec.ofNat w c + a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_mul {w : Nat} (x y : BitVec w) :
(~~~x + 1#w) * y = ~~~(x * y) + 1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_neg {w : Nat} (x y : BitVec w) :
x * (~~~y + 1#w) = ~~~(x * y) + 1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero' {w w' : Nat} (n : BitVec w) :
n <<< 0#w' = n
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_neg {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :
(~~~x + 1#w₁) <<< y = ~~~(x <<< y) + 1
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_zero' {w w' : Nat} (n : BitVec w) :
n >>> 0#w' = n
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self {w : Nat} (n : BitVec w) :
n >>> n = 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_lt_iff_zero_neq {w : Nat} (a : BitVec w) :
0#w < a ↔ a ≠ 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' {w : Nat} (a : BitVec w) :
(0#w).ult a = !a == 0#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.lt_irrefl {n : Nat} (a : BitVec n) :
a.ult a = false
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.not_lt_zero {n : Nat} (a : BitVec n) :
a.ult 0#n = false
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.lt_one_iff {n : Nat} (a : BitVec n) (h : 0 < n) :
a.ult 1#n = (a == 0#n)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult' {w : Nat} (a : BitVec w) :
(-1#w).ult a = false
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ult_max' {w : Nat} (a : BitVec w) :
a.ult (-1#w) = !a == -1#w
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n k : Nat) (hk : 2 ^ k = n) (hlt : k < w) :
x / BitVec.ofNat w n = x >>> k

`x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`.

source
theorem Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_if {w : Nat} {c : Bool} {x y : BitVec w} (s l : Nat) :
BitVec.extractLsb' s l (bif c then x else y) = bif c then BitVec.extractLsb' s l x else BitVec.extractLsb' s l y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_mul {w : Nat} (a : BitVec w) :
-1#w * a = -a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ones {w : Nat} (a : BitVec w) :
a * -1#w = -a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_beq_const {w b c : Nat} {a : BitVec w} :
(a + BitVec.ofNat w b == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.const_add_beq_const {w b : Nat} {a : BitVec w} {c : Nat} :
(BitVec.ofNat w b + a == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.const_beq_add_const_beq {w c : Nat} {a : BitVec w} {b : Nat} :
(BitVec.ofNat w c == a + BitVec.ofNat w b) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.const_beq_const_add_beq {w c b : Nat} {a : BitVec w} :
(BitVec.ofNat w c == BitVec.ofNat w b + a) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_left {w a b : Nat} {c : BitVec w} :
BitVec.ofNat w a &&& (BitVec.ofNat w b &&& c) = BitVec.ofNat w a &&& BitVec.ofNat w b &&& c
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_right {w a : Nat} {b : BitVec w} {c : Nat} :
BitVec.ofNat w a &&& (b &&& BitVec.ofNat w c) = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_left' {w a : Nat} {b : BitVec w} {c : Nat} :
BitVec.ofNat w a &&& b &&& BitVec.ofNat w c = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_right' {w b c : Nat} {a : BitVec w} :
a &&& BitVec.ofNat w b &&& BitVec.ofNat w c = BitVec.ofNat w b &&& BitVec.ofNat w c &&& a
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.append_const_left {w3 w1 a w2 b : Nat} {c : BitVec w3} :
BitVec.ofNat w1 a ++ (BitVec.ofNat w2 b ++ c) = BitVec.cast ⋯ (BitVec.ofNat w1 a ++ BitVec.ofNat w2 b ++ c)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.append_const_right {w1 w2 b w3 c : Nat} {a : BitVec w1} :
a ++ BitVec.ofNat w2 b ++ BitVec.ofNat w3 c = BitVec.cast ⋯ (a ++ (BitVec.ofNat w2 b ++ BitVec.ofNat w3 c))
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
BitVec.signExtend w x = BitVec.cast ⋯ ((bif x.msb then -1#(w - v) else 0#(w - v)) ++ x)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
BitVec.signExtend w x = BitVec.extractLsb' 0 w x
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul {w : Nat} {x y : BitVec w} :
~~~(x + x * y) + 1#w = x * ~~~y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul' {w : Nat} {x y : BitVec w} :
~~~(x + y * x) + 1#w = ~~~y * x
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul'' {w : Nat} {x y : BitVec w} :
~~~(x * y + x) + 1#w = x * ~~~y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul''' {w : Nat} {x y : BitVec w} :
~~~(y * x + x) + 1#w = ~~~y * x
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul {w : Nat} {x y : BitVec w} :
~~~(x * ~~~y) + 1#w = x + x * y
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul' {w : Nat} {x y : BitVec w} :
~~~(~~~y * x) + 1#w = x + y * x
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_left {w : Nat} {x₁ x₂ y : BitVec w} :
(x₁ * y == x₂ * y) = !(!x₁ == x₂ && !x₁ * y == x₂ * y)
source
theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_right {w : Nat} {x y₁ y₂ : BitVec w} :
(x * y₁ == x * y₂) = !(!y₁ == y₂ && !x * y₁ == x * y₂)
source
theorem Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_cond {c : Bool} {t e : UInt8} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_cond {c : Bool} {t e : UInt16} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_cond {c : Bool} {t e : UInt32} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_cond {c : Bool} {t e : UInt64} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.USize.toBitVec_cond {c : Bool} {t e : USize} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int8.toBitVec_cond {c : Bool} {t e : Int8} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int16.toBitVec_cond {c : Bool} {t e : Int16} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int32.toBitVec_cond {c : Bool} {t e : Int32} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int64.toBitVec_cond {c : Bool} {t e : Int64} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.ISize.toBitVec_cond {c : Bool} {t e : ISize} :
(bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_ite {c : Prop} {t e : UInt8} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_ite {c : Prop} {t e : UInt16} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_ite {c : Prop} {t e : UInt32} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_ite {c : Prop} {t e : UInt64} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.USize.toBitVec_ite {c : Prop} {t e : USize} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int8.toBitVec_ite {c : Prop} {t e : Int8} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int16.toBitVec_ite {c : Prop} {t e : Int16} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int32.toBitVec_ite {c : Prop} {t e : Int32} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.Int64.toBitVec_ite {c : Prop} {t e : Int64} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.ISize.toBitVec_ite {c : Prop} {t e : ISize} [Decidable c] :
(if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
source
theorem Std.Tactic.BVDecide.Normalize.UInt8.beq_eq_decide_eq {a b : UInt8} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.UInt16.beq_eq_decide_eq {a b : UInt16} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.UInt32.beq_eq_decide_eq {a b : UInt32} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.UInt64.beq_eq_decide_eq {a b : UInt64} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.USize.beq_eq_decide_eq {a b : USize} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.Int8.beq_eq_decide_eq {a b : Int8} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.Int16.beq_eq_decide_eq {a b : Int16} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.Int32.beq_eq_decide_eq {a b : Int32} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.Int64.beq_eq_decide_eq {a b : Int64} :
(a == b) = decide (a = b)
source
theorem Std.Tactic.BVDecide.Normalize.ISize.beq_eq_decide_eq {a b : ISize} :
(a == b) = decide (a = b)