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'.

source

@[simp]

theorem BitVec.getLsbD_sshiftRight {w : Nat} (x : BitVec w) (s : Nat) (i : Nat) :

(x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb)

source

theorem BitVec.sshiftRight_xor_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :

(x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n

source

theorem BitVec.sshiftRight_and_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :

(x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n

source

theorem BitVec.sshiftRight_or_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :

(x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n

source

theorem BitVec.sshiftRight_msb_eq_msb {w : Nat} {n : Nat} {x : BitVec w} :

(x.sshiftRight n).msb = x.msb

The msb after arithmetic shifting right equals the original msb.

source

@[simp]

theorem BitVec.sshiftRight_zero {w : Nat} {x : BitVec w} :

x.sshiftRight 0 = x

source

theorem BitVec.sshiftRight_add {w : Nat} {x : BitVec w} {m : Nat} {n : Nat} :

x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n

sshiftRight reductions from BitVec to Nat #

source

@[simp]

theorem BitVec.sshiftRight_eq' {w : Nat} :

∀ {w_1 : Nat} {y : BitVec w_1} (x : BitVec w), x.sshiftRight' y = x.sshiftRight y.toNat

udiv #

source

theorem BitVec.udiv_eq {n : Nat} {x : BitVec n} {y : BitVec n} :

x.udiv y = BitVec.ofNat n (x.toNat / y.toNat)

source

@[simp]

theorem BitVec.toNat_udiv {n : Nat} {x : BitVec n} {y : BitVec n} :

(x.udiv y).toNat = x.toNat / y.toNat

umod #

source

theorem BitVec.umod_eq {n : Nat} {x : BitVec n} {y : BitVec n} :

x.umod y = BitVec.ofNat n (x.toNat % y.toNat)

source

@[simp]

theorem BitVec.toNat_umod {n : Nat} {x : BitVec n} {y : BitVec n} :

(x.umod y).toNat = x.toNat % y.toNat

signExtend #

source

theorem BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :

BitVec.signExtend v x = BitVec.zeroExtend v x

The sign extension is the same as zero extending when msb = false.

source

theorem BitVec.signExtend_eq_not_zeroExtend_not_of_msb_true {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :

BitVec.signExtend v x = ~~~BitVec.zeroExtend v (~~~x)

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.

source

@[simp]

theorem BitVec.getLsbD_signExtend {w : Nat} (x : BitVec w) {v : Nat} {i : Nat} :

(BitVec.signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)

source

theorem BitVec.signExtend_eq_truncate_of_lt {w : Nat} (x : BitVec w) {v : Nat} (hv : v ≤ w) :

BitVec.signExtend v x = BitVec.truncate v x

Sign extending to a width smaller than the starting width is a truncation.

source

theorem BitVec.signExtend_eq {w : Nat} (x : BitVec w) :

BitVec.signExtend w x = x

Sign extending to the same bitwidth is a no op.

append #

source

theorem BitVec.append_def {v : Nat} {w : Nat} (x : BitVec v) (y : BitVec w) :

x ++ y = x.shiftLeftZeroExtend w ||| BitVec.zeroExtend' ⋯ y

source

@[simp]

theorem BitVec.toNat_append {m : Nat} {n : Nat} (x : BitVec m) (y : BitVec n) :

(x ++ y).toNat = x.toNat <<< n ||| y.toNat

source

@[simp]

theorem BitVec.getLsbD_append {n : Nat} {m : Nat} {i : Nat} {x : BitVec n} {y : BitVec m} :

(x ++ y).getLsbD i = bif decide (i < m) then y.getLsbD i else x.getLsbD (i - m)

source

@[simp]

theorem BitVec.getMsbD_append {n : Nat} {m : Nat} {i : Nat} {x : BitVec n} {y : BitVec m} :

(x ++ y).getMsbD i = bif decide (n ≤ i) then y.getMsbD (i - n) else x.getMsbD i

source

theorem BitVec.msb_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :

(x ++ y).msb = bif w == 0 then y.msb else x.msb

source

@[simp]

theorem BitVec.truncate_append {w : Nat} {v : Nat} {k : Nat} {x : BitVec w} {y : BitVec v} :

BitVec.truncate k (x ++ y) = if h : k ≤ v then BitVec.truncate k y else BitVec.cast ⋯ (BitVec.truncate (k - v) x ++ y)

source

@[simp]

theorem BitVec.truncate_cons {w : Nat} {a : Bool} {x : BitVec w} :

BitVec.truncate w (BitVec.cons a x) = x

source

@[simp]

theorem BitVec.not_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :

~~~(x ++ y) = ~~~x ++ ~~~y

source

@[simp]

theorem BitVec.and_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :

x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)

source

@[simp]

theorem BitVec.or_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :

x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)

source

@[simp]

theorem BitVec.xor_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :

x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)

source

theorem BitVec.shiftRight_add {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :

x >>> (n + m) = x >>> n >>> m

source

@[deprecated BitVec.shiftRight_add]

theorem BitVec.shiftRight_shiftRight {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :

x >>> n >>> m = x >>> (n + m)

rev #

source

theorem BitVec.getLsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) :

x.getLsbD ↑i.rev = x.getMsbD ↑i

source

theorem BitVec.getMsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) :

x.getMsbD ↑i.rev = x.getLsbD ↑i

cons #

source

@[simp]

theorem BitVec.toNat_cons {w : Nat} (b : Bool) (x : BitVec w) :

(BitVec.cons b x).toNat = b.toNat <<< w ||| x.toNat

source

theorem BitVec.toNat_cons' {w : Nat} {a : Bool} {x : BitVec w} :

(BitVec.cons a x).toNat = a.toNat <<< w + x.toNat

Variant of toNat_cons using + instead of |||.

source

@[simp]

theorem BitVec.getLsbD_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) :

(BitVec.cons b x).getLsbD i = if i = n then b else x.getLsbD i

source

@[simp]

theorem BitVec.msb_cons {a : Bool} :

∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).msb = a

source

@[simp]

theorem BitVec.getMsbD_cons_zero {a : Bool} :

∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).getMsbD 0 = a

source

@[simp]

theorem BitVec.getMsbD_cons_succ {a : Bool} :

∀ {w : Nat} {x : BitVec w} {i : Nat}, (BitVec.cons a x).getMsbD (i + 1) = x.getMsbD i

source

theorem BitVec.truncate_succ {w : Nat} {i : Nat} (x : BitVec w) :

BitVec.truncate (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.truncate i x)

source

theorem BitVec.eq_msb_cons_truncate {w : Nat} (x : BitVec (w + 1)) :

x = BitVec.cons x.msb (BitVec.truncate w x)

source

@[simp]

theorem BitVec.not_cons {w : Nat} (x : BitVec w) (b : Bool) :

~~~BitVec.cons b x = BitVec.cons (!b) (~~~x)

source

@[simp]

theorem BitVec.cons_or_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

BitVec.cons a x ||| BitVec.cons b y = BitVec.cons (a || b) (x ||| y)

source

@[simp]

theorem BitVec.cons_and_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

BitVec.cons a x &&& BitVec.cons b y = BitVec.cons (a && b) (x &&& y)

source

@[simp]

theorem BitVec.cons_xor_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

BitVec.cons a x ^^^ BitVec.cons b y = BitVec.cons (xor a b) (x ^^^ y)

concat #

source

@[simp]

theorem BitVec.toNat_concat {w : Nat} (x : BitVec w) (b : Bool) :

(x.concat b).toNat = x.toNat * 2 + b.toNat

source

theorem BitVec.getLsbD_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :

(x.concat b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)

source

@[simp]

theorem BitVec.getLsbD_concat_zero :

∀ {w : Nat} {x : BitVec w} {b : Bool}, (x.concat b).getLsbD 0 = b

source

@[simp]

theorem BitVec.getLsbD_concat_succ :

∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, (x.concat b).getLsbD (i + 1) = x.getLsbD i

source

@[simp]

theorem BitVec.not_concat {w : Nat} (x : BitVec w) (b : Bool) :

~~~x.concat b = (~~~x).concat !b

source

@[simp]

theorem BitVec.concat_or_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

x.concat a ||| y.concat b = (x ||| y).concat (a || b)

source

@[simp]

theorem BitVec.concat_and_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

x.concat a &&& y.concat b = (x &&& y).concat (a && b)

source

@[simp]

theorem BitVec.concat_xor_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

x.concat a ^^^ y.concat b = (x ^^^ y).concat (xor a b)

add #

source

theorem BitVec.add_def {n : Nat} (x : BitVec n) (y : BitVec n) :

x + y = BitVec.ofNat n (x.toNat + y.toNat)

source

@[simp]

theorem BitVec.toNat_add {w : Nat} (x : BitVec w) (y : BitVec w) :

(x + y).toNat = (x.toNat + y.toNat) % 2 ^ w

Definition of bitvector addition as a nat.

source

@[simp]

theorem BitVec.toFin_add {w : Nat} (x : BitVec w) (y : BitVec w) :

(x + y).toFin = x.toFin + y.toFin

source

@[simp]

theorem BitVec.ofFin_add {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :

{ toFin := x } + y = { toFin := x + y.toFin }

source

@[simp]

theorem BitVec.add_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :

x + { toFin := y } = { toFin := x.toFin + y }

source

theorem BitVec.ofNat_add {n : Nat} (x : Nat) (y : Nat) :

BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y

source

theorem BitVec.ofNat_add_ofNat {n : Nat} (x : Nat) (y : Nat) :

BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y)

source

theorem BitVec.add_assoc {n : Nat} (x : BitVec n) (y : BitVec n) (z : BitVec n) :

x + y + z = x + (y + z)

source

instance BitVec.instAssociativeHAdd {n : Nat} :

Std.Associative fun (x1 x2 : BitVec n) => x1 + x2

Equations

⋯ = ⋯

source

theorem BitVec.add_comm {n : Nat} (x : BitVec n) (y : BitVec n) :

x + y = y + x

source

instance BitVec.instCommutativeHAdd {n : Nat} :

Std.Commutative fun (x1 x2 : BitVec n) => x1 + x2

Equations

⋯ = ⋯

source

@[simp]

theorem BitVec.add_zero {n : Nat} (x : BitVec n) :

x + 0#n = x

source

@[simp]

theorem BitVec.zero_add {n : Nat} (x : BitVec n) :

0#n + x = x

source

instance BitVec.instLawfulIdentityHAddOfNatOfNatNat {n : Nat} :

Std.LawfulIdentity (fun (x1 x2 : BitVec n) => x1 + x2) 0#n

Equations

⋯ = ⋯

source

theorem BitVec.truncate_add {w : Nat} {i : Nat} (x : BitVec w) (y : BitVec w) (h : i ≤ w) :

BitVec.truncate i (x + y) = BitVec.truncate i x + BitVec.truncate i y

source

@[simp]

theorem BitVec.toInt_add {w : Nat} (x : BitVec w) (y : BitVec w) :

(x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)

source

theorem BitVec.ofInt_add {n : Nat} (x : Int) (y : Int) :

BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y

sub/neg #

source

theorem BitVec.sub_def {n : Nat} (x : BitVec n) (y : BitVec n) :

x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)

source

@[simp]

theorem BitVec.toNat_sub {n : Nat} (x : BitVec n) (y : BitVec n) :

(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n

source

theorem BitVec.toNat_sub' {n : Nat} (x : BitVec n) (y : BitVec n) :

(x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n

source

@[simp]

theorem BitVec.toFin_sub {n : Nat} (x : BitVec n) (y : BitVec n) :

(x - y).toFin = x.toFin - y.toFin

source

@[simp]

theorem BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :

{ toFin := x } - y = { toFin := x - y.toFin }

source

@[simp]

theorem BitVec.sub_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :

x - { toFin := y } = { toFin := x.toFin - y }

source

theorem BitVec.ofNat_sub_ofNat {n : Nat} (x : Nat) (y : Nat) :

BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)

source

@[simp]

theorem BitVec.sub_zero {n : Nat} (x : BitVec n) :

x - 0#n = x

source

@[simp]

theorem BitVec.sub_self {n : Nat} (x : BitVec n) :

x - x = 0#n

source

@[simp]

theorem BitVec.toNat_neg {n : Nat} (x : BitVec n) :

(-x).toNat = (2 ^ n - x.toNat) % 2 ^ n

source

@[simp]

theorem BitVec.toFin_neg {n : Nat} (x : BitVec n) :

(-x).toFin = Fin.ofNat' (2 ^ n - x.toNat) ⋯

source

theorem BitVec.sub_toAdd {n : Nat} (x : BitVec n) (y : BitVec n) :

x - y = x + -y

source

@[simp]

theorem BitVec.neg_zero (n : Nat) :

-0#n = 0#n

source

theorem BitVec.add_sub_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :

x + y - y = x

source

theorem BitVec.sub_add_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :

x - y + y = x

source

theorem BitVec.eq_sub_iff_add_eq {w : Nat} {x : BitVec w} {y : BitVec w} {z : BitVec w} :

x = z - y ↔ x + y = z

source

theorem BitVec.negOne_eq_allOnes {w : Nat} :

-1#w = BitVec.allOnes w

source

theorem BitVec.neg_eq_not_add {w : Nat} (x : BitVec w) :

-x = ~~~x + 1

source

@[simp]

theorem BitVec.neg_neg {w : Nat} {x : BitVec w} :

- -x = x

source

theorem BitVec.neg_ne_iff_ne_neg {w : Nat} {x : BitVec w} {y : BitVec w} :

-x ≠ y ↔ x ≠ -y

mul #

source

theorem BitVec.mul_def {n : Nat} {x : BitVec n} {y : BitVec n} :

x * y = { toFin := x.toFin * y.toFin }

source

@[simp]

theorem BitVec.toNat_mul {n : Nat} (x : BitVec n) (y : BitVec n) :

(x * y).toNat = x.toNat * y.toNat % 2 ^ n

source

@[simp]

theorem BitVec.toFin_mul {n : Nat} (x : BitVec n) (y : BitVec n) :

(x * y).toFin = x.toFin * y.toFin

source

theorem BitVec.mul_comm {w : Nat} (x : BitVec w) (y : BitVec w) :

x * y = y * x

source

instance BitVec.instCommutativeHMul {w : Nat} :

Std.Commutative fun (x y : BitVec w) => x * y

Equations

⋯ = ⋯

source

theorem BitVec.mul_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :

x * y * z = x * (y * z)

source

instance BitVec.instAssociativeHMul {w : Nat} :

Std.Associative fun (x y : BitVec w) => x * y

Equations

⋯ = ⋯

source

@[simp]

theorem BitVec.mul_one {w : Nat} (x : BitVec w) :

x * 1#w = x

source

@[simp]

theorem BitVec.one_mul {w : Nat} (x : BitVec w) :

1#w * x = x

source

instance BitVec.instLawfulCommIdentityHMulOfNatOfNatNat {w : Nat} :

Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) 1#w

Equations

⋯ = ⋯

source

@[simp]

theorem BitVec.BitVec.mul_zero {w : Nat} {x : BitVec w} :

x * 0#w = 0#w

source

theorem BitVec.BitVec.mul_add {w : Nat} {x : BitVec w} {y : BitVec w} {z : BitVec w} :

x * (y + z) = x * y + x * z

source

@[simp]

theorem BitVec.toInt_mul {w : Nat} (x : BitVec w) (y : BitVec w) :

(x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)

source

theorem BitVec.ofInt_mul {n : Nat} (x : Int) (y : Int) :

BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y

le and lt #

source

theorem BitVec.le_def {n : Nat} (x : BitVec n) (y : BitVec n) :

x ≤ y ↔ x.toNat ≤ y.toNat

source

@[simp]

theorem BitVec.le_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :

x ≤ { toFin := y } ↔ x.toFin ≤ y

source

@[simp]

theorem BitVec.ofFin_le {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :

{ toFin := x } ≤ y ↔ x ≤ y.toFin

source

@[simp]

theorem BitVec.ofNat_le_ofNat {n : Nat} (x : Nat) (y : Nat) :

BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n

source

theorem BitVec.lt_def {n : Nat} (x : BitVec n) (y : BitVec n) :

x < y ↔ x.toNat < y.toNat

source

@[simp]

theorem BitVec.lt_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :

x < { toFin := y } ↔ x.toFin < y

source

@[simp]

theorem BitVec.ofFin_lt {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :

{ toFin := x } < y ↔ x < y.toFin

source

@[simp]

theorem BitVec.ofNat_lt_ofNat {n : Nat} (x : Nat) (y : Nat) :

BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n

source

theorem BitVec.lt_of_le_ne {n : Nat} (x : BitVec n) (y : BitVec n) (h1 : x ≤ y) (h2 : ¬x = y) :

x < y

ofBoolList #

source

@[simp]

theorem BitVec.getMsbD_ofBoolListBE {bs : List Bool} {i : Nat} :

(BitVec.ofBoolListBE bs).getMsbD i = bs.getD i false

source

@[simp]

theorem BitVec.getLsbD_ofBoolListBE {bs : List Bool} {i : Nat} :

(BitVec.ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

source

@[simp]

theorem BitVec.getLsb_ofBoolListLE {bs : List Bool} {i : Nat} :

(BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false

source

@[simp]

theorem BitVec.getMsbD_ofBoolListLE {bs : List Bool} {i : Nat} :

(BitVec.ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Rotate Left #

source

@[simp]

theorem BitVec.rotateLeft_mod_eq_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} :

x.rotateLeft (r % w) = x.rotateLeft r

rotateLeft is invariant under mod by the bitwidth.

source

theorem BitVec.rotateLeft_eq_rotateLeftAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :

x.rotateLeft r = x.rotateLeftAux r

rotateLeft equals the bit fiddling definition of rotateLeftAux when the rotation amount is smaller than the bitwidth.

source

theorem BitVec.getLsbD_rotateLeftAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :

(x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i)

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]

source

theorem BitVec.getLsbD_rotateLeftAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :

(x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r))

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).

source

theorem BitVec.getLsbD_rotateLeft_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :

(x.rotateLeft r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

When r < w, we give a formula for (x.rotateRight r).getLsbD i.

source

@[simp]

theorem BitVec.getLsbD_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :

(x.rotateLeft r).getLsbD i = bif decide (i < r % w) then x.getLsbD (w - r % w + i) else decide (i < w) && x.getLsbD (i - r % w)

Rotate Right #

source

theorem BitVec.getLsbD_rotateRightAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :

(x.rotateRightAux r).getLsbD i = x.getLsbD (r + i)

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]

source

theorem BitVec.getLsbD_rotateRightAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :

(x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r)))

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>)

source

theorem BitVec.rotateRight_eq_rotateRightAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :

x.rotateRight r = x.rotateRightAux r

rotateRight equals the bit fiddling definition of rotateRightAux when the rotation amount is smaller than the bitwidth.

source

@[simp]

theorem BitVec.rotateRight_mod_eq_rotateRight {w : Nat} {x : BitVec w} {r : Nat} :

x.rotateRight (r % w) = x.rotateRight r

rotateRight is invariant under mod by the bitwidth.

source

theorem BitVec.getLsbD_rotateRight_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :

(x.rotateRight r).getLsbD i = bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

When r < w, we give a formula for (x.rotateRight r).getLsb i.

source

@[simp]

theorem BitVec.getLsbD_rotateRight {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :

(x.rotateRight r).getLsbD i = bif decide (i < w - r % w) then x.getLsbD (r % w + i) else decide (i < w) && x.getLsbD (i - (w - r % w))

source

@[simp]

theorem BitVec.toNat_twoPow (w : Nat) (i : Nat) :

(BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w

source

@[simp]

theorem BitVec.getLsbD_twoPow {w : Nat} (i : Nat) (j : Nat) :

(BitVec.twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))

source

@[simp]

theorem BitVec.and_twoPow {w : Nat} (x : BitVec w) (i : Nat) :

x &&& BitVec.twoPow w i = if x.getLsbD i = true then BitVec.twoPow w i else 0#w

source

@[simp]

theorem BitVec.twoPow_and {w : Nat} (x : BitVec w) (i : Nat) :

BitVec.twoPow w i &&& x = if x.getLsbD i = true then BitVec.twoPow w i else 0#w

source

@[simp]

theorem BitVec.mul_twoPow_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) :

x * BitVec.twoPow w i = x <<< i

source

theorem BitVec.twoPow_zero {w : Nat} :

BitVec.twoPow w 0 = 1#w

source

@[simp]

theorem BitVec.getLsbD_one {w : Nat} {i : Nat} :

(1#w).getLsbD i = (decide (0 < w) && decide (0 = i))

source

theorem BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :

BitVec.zeroExtend w (BitVec.truncate (i + 1) x) = BitVec.zeroExtend w (BitVec.truncate i x)

When the (i+1)th bit of x is false, keeping the lower (i + 1) bits of x equals keeping the lower i bits.

source

theorem BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :

BitVec.zeroExtend w (BitVec.truncate (i + 1) x) = BitVec.zeroExtend w (BitVec.truncate i x) ||| BitVec.twoPow w i

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),

source