This normalized a bitvec using ofFin
to ofNat
.
msb #
cast #
toInt/ofInt #
zeroExtend and truncate #
extractLsb #
allOnes #
or #
and #
xor #
not #
cast #
shiftLeft #
ushiftRight #
sshiftRight #
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'.
signExtend #
The sign extension is the same as zero extending when msb = false
.
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.
append #
rev #
cons #
Variant of toNat_cons
using +
instead of |||
.
concat #
add #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
sub/neg #
mul #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
le and lt #
intMax #
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
ofBoolList #
Rotate Left #
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]
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)
.
Rotate Right #
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]
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>)