Basic operations on bitvectors #
This is a work-in-progress, and contains additions to other theories.
This file was moved to mathlib from core Lean in the switch to Lean 3.20.0c. It is not fully in compliance with mathlib style standards.
Create a zero bitvector
Equations
- bitvec.zero n = vector.repeat ff n
Create a bitvector of length n
whose n-1
st entry is 1 and other entries are 0.
Equations
- bitvec.one n.succ = (vector.repeat ff n).append (tt::ᵥvector.nil)
- bitvec.one 0 = vector.nil
Create a bitvector from another with a provably equal length.
Equations
- bitvec.cong h ⟨x, p⟩ = ⟨x, _⟩
bitvec
specific version of vector.append
Equations
Shift operations #
shl x i
is the bitvector obtained by left-shifting x
i
times and padding with ff
.
If x.length < i
then this will return the all-ff
s bitvector.
Equations
- x.shl i = bitvec.cong _ ((vector.drop i x).append (vector.repeat ff (min n i)))
fill_shr x i fill
is the bitvector obtained by right-shifting x
i
times and then
padding with fill : bool
. If x.length < i
then this will return the constant fill
bitvector.
Equations
- x.fill_shr i fill = bitvec.cong _ ((vector.repeat fill (min n i)).append (vector.take (n - i) x))
signed shift right
Equations
- x.sshr i = vector.head x::ᵥbitvec.fill_shr (vector.tail x) i (vector.head x)
- _x.sshr _x_1 = vector.nil
Bitwise operations #
bitwise not
Equations
bitwise and
Equations
bitwise xor
Equations
Arithmetic operators #
xor3 x y c
is ((x XOR y) XOR c)
.
Equations
- bitvec.xor3 x y c = bxor (bxor x y) c
Add with carry (no overflow)
Equations
- x.adc y c = let f : bool → bool → bool → bool × bool := λ (x y c : bool), (bitvec.carry x y c, bitvec.xor3 x y c) in bitvec.adc._match_1 (vector.map_accumr₂ f x y c)
- bitvec.adc._match_1 (c, z) = c::ᵥz
The sum of two bitvectors
Equations
- x.add y = vector.tail (x.adc y ff)
Equations
- bitvec.has_zero = {zero := bitvec.zero n}
Equations
- bitvec.has_one = {one := bitvec.one n}
Equations
- bitvec.has_add = {add := bitvec.add n}
Equations
- bitvec.has_sub = {sub := bitvec.sub n}
Equations
- bitvec.has_neg = {neg := bitvec.neg n}
Equations
- bitvec.has_mul = {mul := bitvec.mul n}
Comparison operators #
sborrow x y
returns tt
iff x < y
as two's complement integers
Equations
- x.sborrow y = bitvec.sborrow._match_1 n x y (vector.head x, vector.head y)
- _x.sborrow _x_1 = ff
- bitvec.sborrow._match_1 n x y (tt, tt) = bitvec.uborrow (vector.tail x) (vector.tail y)
- bitvec.sborrow._match_1 n x y (tt, ff) = tt
- bitvec.sborrow._match_1 n x y (ff, tt) = ff
- bitvec.sborrow._match_1 n x y (ff, ff) = bitvec.uborrow (vector.tail x) (vector.tail y)
Create a bitvector from a nat
Equations
- bitvec.of_nat n.succ x = vector.append (bitvec.of_nat n (x / 2)) (to_bool (x % 2 = 1)::ᵥvector.nil)
- bitvec.of_nat 0 x = vector.nil
Create a bitvector in the two's complement representation from an int
Equations
- bitvec.of_int n -[1+ m] = tt::ᵥ(bitvec.of_nat n m).not
- bitvec.of_int n (int.of_nat m) = ff::ᵥbitvec.of_nat n m
add_lsb r b
is r + r + 1
if b
is tt
and r + r
otherwise.
Equations
- bitvec.add_lsb r b = r + r + cond b 1 0
Return the natural number encoded by the input bitvector
Equations
Return the integer encoded by the input bitvector
Equations
- v.to_int = cond (vector.head v) -[1+ (bitvec.not (vector.tail v)).to_nat] (int.of_nat (bitvec.to_nat (vector.tail v)))
- _x.to_int = 0
Miscellaneous instances #
Equations
- bitvec.has_repr n = {repr := repr n}