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

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

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

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.getLsb_signExtend {w : Nat} (x : BitVec w) {v : Nat} {i : Nat} :

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

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.getLsb_append {n : Nat} {m : Nat} {i : Nat} {v : BitVec n} {w : BitVec m} :

(v ++ w).getLsb i = bif decide (i < m) then w.getLsb i else v.getLsb (i - m)

source

@[simp]

theorem BitVec.getMsb_append {n : Nat} {m : Nat} {i : Nat} {v : BitVec n} {w : BitVec m} :

(v ++ w).getMsb i = bif decide (n ≤ i) then w.getMsb (i - n) else v.getMsb 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.getLsb_rev {w : Nat} (x : BitVec w) (i : Fin w) :

x.getLsb ↑i.rev = x.getMsb ↑i

source

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

x.getMsb ↑i.rev = x.getLsb ↑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.getLsb_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) :

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

source

@[simp]

theorem BitVec.msb_cons {a : Bool} :

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

source

@[simp]

theorem BitVec.getMsb_cons_zero {a : Bool} :

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

source

@[simp]

theorem BitVec.getMsb_cons_succ {a : Bool} :

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

source

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

BitVec.truncate (i + 1) x = BitVec.cons (x.getLsb 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.getLsb_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :

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

source

@[simp]

theorem BitVec.getLsb_concat_zero :

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

source

@[simp]

theorem BitVec.getLsb_concat_succ :

∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, (x.concat b).getLsb (i + 1) = x.getLsb 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 (x x_1 : BitVec n) => x + x_1

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 (x x_1 : BitVec n) => x + x_1

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 (x x_1 : BitVec n) => x + x_1) 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

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

intMax #

source

def BitVec.intMax (w : Nat) :

BitVec w

The bitvector of width w that has the largest value when interpreted as an integer.

Equations

BitVec.intMax w = BitVec.ofNat w (2 ^ w - 1)

Instances For

source

theorem BitVec.getLsb_intMax_eq {i : Nat} (w : Nat) :

(BitVec.intMax w).getLsb i = decide (i < w)

source

theorem BitVec.toNat_intMax_eq {w : Nat} :

(BitVec.intMax w).toNat = 2 ^ w - 1

ofBoolList #

source

@[simp]

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

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

source

@[simp]

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

(BitVec.ofBoolListBE bs).getLsb 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).getLsb i = bs.getD i false

source

@[simp]

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

(BitVec.ofBoolListLE bs).getMsb 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.getLsb_rotateLeftAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :

(x.rotateLeftAux r).getLsb i = x.getLsb (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).getLsb ⟨i, i < 2⟩ = <3 2 1 0 | 6 5>.getLsb ⟨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.getLsb_rotateLeftAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :

(x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (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).getLsb ⟨i, i ≥ 2⟩ = <3 2 1 0 | 6 5>.getLsb ⟨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.getLsb_rotateLeft_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :

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

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

source

@[simp]

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

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

Rotate Right #

source

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

(x.rotateRightAux r).getLsb i = x.getLsb (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).getLsb ⟨i, i ≤ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩ = <6 5 4 3 2>.getLsb i = <6 5 4 3 2 | 1 0>[i + 2]

source

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

(x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (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).getLsb ⟨i, i ≥ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩ = <1 0>.getLsb (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.getLsb_rotateRight_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :

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

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

source

@[simp]

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

(x.rotateRight r).getLsb i = bif decide (i < w - r % w) then x.getLsb (r % w + i) else decide (i < w) && x.getLsb (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.getLsb_twoPow {w : Nat} (i : Nat) (j : Nat) :

(BitVec.twoPow w i).getLsb 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.getLsb 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.getLsb 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.getLsb_one {w : Nat} {i : Nat} :

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

source

theorem BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsb 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_getLsb_true {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsb 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