14.5. Bitvectors🔗

Bitvectors are fixed-width sequences of binary digits. They are frequently used in software verification, because they closely model efficient data structures and operations that are similar to hardware. A bitvector can be understood from two perspectives: as a sequence of bits, or as a number encoded by a sequence of bits. When a bitvector represents a number, it can do so as either a signed or an unsigned number. Signed numbers are represented in two's complement form.

14.5.1. Logical Model

Bitvectors are represented as a wrapper around a Fin with a suitable bound. Because Fin itself is a wrapper around a Nat, bitvectors are able to use the kernel's special support for efficient computation with natural numbers.

structure

BitVec (w : Nat) : Type

A bitvector of the specified width.

This is represented as the underlying Nat number in both the runtime and the kernel, inheriting all the special support for Nat.

Constructor

BitVec.ofFin

Construct a BitVec w from a number less than 2^w. O(1), because we use Fin as the internal representation of a bitvector.

Fields

toFin : Fin (2 ^ w)

Interpret a bitvector as a number less than 2^w. O(1), because we use Fin as the internal representation of a bitvector.

14.5.2. Runtime Representation

Bitvectors are represented as a Fin with the corresponding range. Because BitVec is a trivial wrapper around Fin and Fin is a trivial wrapper around Nat, bitvectors use the same runtime representation as Nat in compiled code.

14.5.3. Syntax

There is an OfNat (BitVec w) n instance for all widths w and natural numbers n. Natural number literals, including those that use hexadecimal or binary notation, may be used to represent bitvectors in contexts where the expected type is known. When the expected type is not known, a dedicated syntax allows the width of the bitvector to be specified along with its value.

Numeric Literals for Bitvectors

The following literals are all equivalent:

example : BitVec 8 := 0xff
example : BitVec 8 := 255
example : BitVec 8 := 0b1111_1111

syntaxFixed-Width Bitvector Literals

term ::= ...
    | Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. 

Conventions for notations in identifiers:

 * The recommended spelling of `0#n` in identifiers is `zero` (not `ofNat_zero`).

 * The recommended spelling of `1#n` in identifiers is `one` (not `ofNat_one`).num#term

This notation pairs a numeric literal with a term that denotes its width. Spaces are forbidden around the #. Literals that overflow the width of the bitvector are truncated.

Fixed-Width Bitvector Literals

Bitvectors may be represented by natural number literals, so (5 : BitVec 8) is a valid bitvector. Additionally, a width may be specified directly in the literal:

5#8

Spaces are not allowed on either side of the #:

5 expected end of input#8

<example>:1:2: expected end of input

5# expected no space before8

<example>:1:3: expected no space before

A numeric literal is required to the left of the #:

(3 + 2)expected end of input#8

<example>:1:7: expected end of input

However, a term is allowed to the right of the #:

5#(4 + 4)

If the literal is too large to fit in the specified number of bits, then it is truncated:

3#2#eval 7#2

3#2

syntaxBounded Bitvector Literals

term ::= ...
    | Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`. num#'term

This notation is available only when the BitVec namespace has been opened. Rather than an explicit width, it expects a proof that the literal value is representable by a bitvector of the corresponding width.

Bounded Bitvector Literals

The bounded bitvector literal notation ensures that literals do not overflow the specified number of bits. The notation is only available when the BitVec namespace has been opened.

open BitVec

Literals that are in bounds require a proof to that effect:

example : BitVec 8 := 1#'(by⊢ 1 < 2 ^ 8 decideAll goals completed! 🐙)

Literals that are not in bounds are not allowed:

example : BitVec 8 := 256#'(by⊢ 256 < 2 ^ 8 tactic 'decide' proved that the proposition
  256 < 2 ^ 8
is falsedecide⊢ 256 < 2 ^ 8)

tactic 'decide' proved that the proposition
  256 < 2 ^ 8
is false

14.5.4. Automation🔗

In addition to the full suite of automation and tools provided by Lean for every type, the bv_decide tactic can solve many bitvector-related problems. This tactic invokes an external automated theorem prover (cadical) and reconstructs the proof that it provides in Lean's own logic. The resulting proofs rely only on the axiom Lean.ofReduceBool; the external prover is not part of the trusted code base.

Popcount

The function popcount returns the number of set bits in a bitvector. It can be implemented as a 32-iteration loop that tests each bit, incrementing a counter if the bit is set:

def popcount_spec (x : BitVec 32) : BitVec 32 :=
  (32 : Nat).fold (init := 0) fun i _ pop =>
    pop + ((x >>> i) &&& 1)

An alternative implementation of popcount is described in Hacker's Delight, Second Edition, by Henry S. Warren, Jr. in Figure 5-2 on p. 82. It uses low-level bitwise operations to compute the same value with far fewer operations:

def popcount (x : BitVec 32) : BitVec 32 :=
  let x := x - ((x >>> 1) &&& 0x55555555)
  let x := (x &&& 0x33333333) + ((x >>> 2) &&& 0x33333333)
  let x := (x + (x >>> 4)) &&& 0x0F0F0F0F
  let x := x + (x >>> 8)
  let x := x + (x >>> 16)
  let x := x &&& 0x0000003F
  x

These two implementations can be proven equivalent using bv_decide:

theorem popcount_correct : popcount = popcount_spec := by⊢ popcount = popcount_spec
  funext xhx:BitVec 32⊢ popcount x = popcount_spec x
  simp [popcount, popcount_spec]hx:BitVec 32⊢ ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) + ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
            ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
              4 &&&
          252645135#32) +
        ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
              ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                  ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
                4 &&&
            252645135#32) >>>
          8 +
      (((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
              ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                  ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
                4 &&&
            252645135#32) +
          ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                  ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
                ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
                    ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
                  4 &&&
              252645135#32) >>>
            8) >>>
        16 &&&
    63#32 =
  (x &&& 1#32) + (x >>> 1 &&& 1#32) + (x >>> 2 &&& 1#32) + (x >>> 3 &&& 1#32) + (x >>> 4 &&& 1#32) +
                                                        (x >>> 5 &&& 1#32) +
                                                      (x >>> 6 &&& 1#32) +
                                                    (x >>> 7 &&& 1#32) +
                                                  (x >>> 8 &&& 1#32) +
                                                (x >>> 9 &&& 1#32) +
                                              (x >>> 10 &&& 1#32) +
                                            (x >>> 11 &&& 1#32) +
                                          (x >>> 12 &&& 1#32) +
                                        (x >>> 13 &&& 1#32) +
                                      (x >>> 14 &&& 1#32) +
                                    (x >>> 15 &&& 1#32) +
                                  (x >>> 16 &&& 1#32) +
                                (x >>> 17 &&& 1#32) +
                              (x >>> 18 &&& 1#32) +
                            (x >>> 19 &&& 1#32) +
                          (x >>> 20 &&& 1#32) +
                        (x >>> 21 &&& 1#32) +
                      (x >>> 22 &&& 1#32) +
                    (x >>> 23 &&& 1#32) +
                  (x >>> 24 &&& 1#32) +
                (x >>> 25 &&& 1#32) +
              (x >>> 26 &&& 1#32) +
            (x >>> 27 &&& 1#32) +
          (x >>> 28 &&& 1#32) +
        (x >>> 29 &&& 1#32) +
      (x >>> 30 &&& 1#32) +
    (x >>> 31 &&& 1#32)
  bv_decideAll goals completed! 🐙

14.5.5. API Reference🔗

14.5.5.1. Bounds

def

BitVec.intMax (w : Nat) : BitVec w

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

def

BitVec.intMin (w : Nat) : BitVec w

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

14.5.5.2. Construction

def

BitVec.fill (w : Nat) (b : Bool) : BitVec w

Fills a bitvector with w copies of the bit b.

def

BitVec.zero (n : Nat) : BitVec n

Return a bitvector 0 of size n. This is the bitvector with all zero bits.

def

BitVec.allOnes (n : Nat) : BitVec n

Bit vector of size n where all bits are 1s

def

BitVec.twoPow (w i : Nat) : BitVec w

twoPow w i is the bitvector 2^i if i < w, and 0 otherwise. That is, 2 to the power i. For the bitwise point of view, it has the ith bit as 1 and all other bits as 0.

14.5.5.3. Conversion

def

BitVec.toHex {n : Nat} (x : BitVec n) : String

Convert bitvector into a fixed-width hex number.

def

BitVec.toInt {n : Nat} (x : BitVec n) : Int

Interpret the bitvector as an integer stored in two's complement form.

def

BitVec.toNat {n : Nat} (x : BitVec n) : Nat

Given a bitvector x, return the underlying Nat. This is O(1) because BitVec is a (zero-cost) wrapper around a Nat.

def

BitVec.ofBool (b : Bool) : BitVec 1

Turn a Bool into a bitvector of length 1

def

BitVec.ofBoolListBE (bs : List Bool) :
  BitVec bs.length

Converts a list of Bools to a big-endian BitVec.

def

BitVec.ofBoolListLE (bs : List Bool) :
  BitVec bs.length

Converts a list of Bools to a little-endian BitVec.

def

BitVec.ofInt (n : Nat) (i : Int) : BitVec n

The BitVec with value (2^n + (i mod 2^n)) mod 2^n.

def

BitVec.ofNat (n i : Nat) : BitVec n

The BitVec with value i mod 2^n.

Conventions for notations in identifiers:

The recommended spelling of 0#n in identifiers is zero (not ofNat_zero).
The recommended spelling of 1#n in identifiers is one (not ofNat_one).

def

BitVec.ofNatLT {n : Nat} (i : Nat)
  (p : i < 2 ^ n) : BitVec n

The BitVec with value i, given a proof that i < 2^n.

def

BitVec.cast {n m : Nat} (eq : n = m)
  (x : BitVec n) : BitVec m

cast eq x embeds x into an equal BitVec type.

14.5.5.4. Comparisons

def

BitVec.ule {n : Nat} (x y : BitVec n) : Bool

Unsigned less-than-or-equal-to for bit vectors.

SMT-Lib name: bvule.

def

BitVec.sle {n : Nat} (x y : BitVec n) : Bool

Signed less-than-or-equal-to for bit vectors.

SMT-Lib name: bvsle.

def

BitVec.ult {n : Nat} (x y : BitVec n) : Bool

Unsigned less-than for bit vectors.

SMT-Lib name: bvult.

def

BitVec.slt {n : Nat} (x y : BitVec n) : Bool

Signed less-than for bit vectors.

BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false

SMT-Lib name: bvslt.

def

BitVec.decEq {n : Nat} (x y : BitVec n) :
  Decidable (x = y)

Bitvectors have decidable equality. This should be used via the instance DecidableEq (BitVec n).

14.5.5.5. Hashing

def

BitVec.hash {n : Nat} (bv : BitVec n) : UInt64

Compute a hash of a bitvector, combining 64-bit words using mixHash.

14.5.5.6. Sequence Operations

These operations treat bitvectors as sequences of bits, rather than as encodings of numbers.

def

BitVec.nil : BitVec 0

The empty bitvector

def

BitVec.cons {n : Nat} (msb : Bool)
  (lsbs : BitVec n) : BitVec (n + 1)

Prepend a single bit to the front of a bitvector, using big endian order (see append). That is, the new bit is the most significant bit.

def

BitVec.concat {n : Nat} (msbs : BitVec n)
  (lsb : Bool) : BitVec (n + 1)

Append a single bit to the end of a bitvector, using big endian order (see append). That is, the new bit is the least significant bit.

def

BitVec.shiftConcat {n : Nat} (x : BitVec n)
  (b : Bool) : BitVec n

x.shiftConcat b shifts all bits of x to the left by 1 and sets the least significant bit to b. It is a non-dependent version of concat that does not change the total bitwidth.

def

BitVec.truncate {w : Nat} (v : Nat)
  (x : BitVec w) : BitVec v

Transform x of length w into a bitvector of length v, by either:

zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.

SMT-Lib name: zero_extend.

def

BitVec.setWidth {w : Nat} (v : Nat)
  (x : BitVec w) : BitVec v

Transform x of length w into a bitvector of length v, by either:

zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.

SMT-Lib name: zero_extend.

def

BitVec.setWidth' {n w : Nat} (le : n ≤ w)
  (x : BitVec n) : BitVec w

A version of setWidth that requires a proof the new width is at least as large, and is a computational noop.

def

BitVec.append {n m : Nat} (msbs : BitVec n)
  (lsbs : BitVec m) : BitVec (n + m)

Concatenation of bitvectors. This uses the "big endian" convention that the more significant input is on the left, so 0xAB#8 ++ 0xCD#8 = 0xABCD#16.

SMT-Lib name: concat.

def

BitVec.replicate {w : Nat} (i : Nat) :
  BitVec w → BitVec (w * i)

replicate i x concatenates i copies of x into a new vector of length w*i.

def

BitVec.reverse {w : Nat} : BitVec w → BitVec w

Reverse the bits in a bitvector.

def

BitVec.rotateLeft {w : Nat} (x : BitVec w)
  (n : Nat) : BitVec w

Rotate left for bit vectors. All the bits of x are shifted to higher positions, with the top n bits wrapping around to fill the low bits.

rotateLeft 0b0011#4 3 = 0b1001

SMT-Lib name: rotate_left except this operator uses a Nat shift amount.

def

BitVec.rotateRight {w : Nat} (x : BitVec w)
  (n : Nat) : BitVec w

Rotate right for bit vectors. All the bits of x are shifted to lower positions, with the bottom n bits wrapping around to fill the high bits.

rotateRight 0b01001#5 1 = 0b10100

SMT-Lib name: rotate_right except this operator uses a Nat shift amount.

14.5.5.6.1. Bit Extraction

def

BitVec.msb {n : Nat} (x : BitVec n) : Bool

Return most-significant bit in bitvector.

def

BitVec.getMsbD {w : Nat} (x : BitVec w)
  (i : Nat) : Bool

Return the i-th most significant bit or false if i ≥ w.

def

BitVec.getMsb' {w : Nat} (x : BitVec w)
  (i : Fin w) : Bool

Return the i-th most significant bit.

This will be renamed getMsb after the existing deprecated alias is removed.

def

BitVec.getMsb? {w : Nat} (x : BitVec w)
  (i : Nat) : Option Bool

Return the i-th most significant bit or none if i ≥ w.

def

BitVec.getLsbD {w : Nat} (x : BitVec w)
  (i : Nat) : Bool

Return the i-th least significant bit or false if i ≥ w.

def

BitVec.getLsb' {w : Nat} (x : BitVec w)
  (i : Fin w) : Bool

Return the i-th least significant bit.

This will be renamed getLsb after the existing deprecated alias is removed.

def

BitVec.getLsb? {w : Nat} (x : BitVec w)
  (i : Nat) : Option Bool

Return the i-th least significant bit or none if i ≥ w.

def

BitVec.extractLsb {n : Nat} (hi lo : Nat)
  (x : BitVec n) : BitVec (hi - lo + 1)

Extraction of bits hi (inclusive) down to lo (inclusive) from a bit vector of size n to yield a new bitvector of size hi - lo + 1.

SMT-Lib name: extract.

def

BitVec.extractLsb' {n : Nat} (start len : Nat)
  (x : BitVec n) : BitVec len

Extraction of bits start to start + len - 1 from a bit vector of size n to yield a new bitvector of size len. If start + len > n, then the vector will be zero-padded in the high bits.

14.5.5.7. Bitwise Operators

These operators modify the individual bits of one or more bitvectors.

def

BitVec.and {n : Nat} (x y : BitVec n) : BitVec n

Bitwise AND for bit vectors.

0b1010#4 &&& 0b0110#4 = 0b0010#4

SMT-Lib name: bvand.

def

BitVec.or {n : Nat} (x y : BitVec n) : BitVec n

Bitwise OR for bit vectors.

0b1010#4 ||| 0b0110#4 = 0b1110#4

SMT-Lib name: bvor.

def

BitVec.not {n : Nat} (x : BitVec n) : BitVec n

Bitwise NOT for bit vectors.

~~~(0b0101#4) == 0b1010

SMT-Lib name: bvnot.

def

BitVec.xor {n : Nat} (x y : BitVec n) : BitVec n

Bitwise XOR for bit vectors.

0b1010#4 ^^^ 0b0110#4 = 0b1100#4

SMT-Lib name: bvxor.

def

BitVec.zeroExtend {w : Nat} (v : Nat)
  (x : BitVec w) : BitVec v

Transform x of length w into a bitvector of length v, by either:

zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.

SMT-Lib name: zero_extend.

def

BitVec.signExtend {w : Nat} (v : Nat)
  (x : BitVec w) : BitVec v

Sign extend a vector of length w, extending with i additional copies of the most significant bit in x. If x is an empty vector, then the sign is treated as zero.

SMT-Lib name: sign_extend.

def

BitVec.ushiftRight {n : Nat} (x : BitVec n)
  (s : Nat) : BitVec n

(Logical) right shift for bit vectors. The high bits are filled with zeros. As a numeric operation, this is equivalent to x / 2^s, rounding down.

SMT-Lib name: bvlshr except this operator uses a Nat shift value.

def

BitVec.sshiftRight {n : Nat} (x : BitVec n)
  (s : Nat) : BitVec n

Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. As a numeric operation, this is equivalent to x.toInt >>> s.

SMT-Lib name: bvashr except this operator uses a Nat shift value.

def

BitVec.sshiftRight' {n m : Nat} (a : BitVec n)
  (s : BitVec m) : BitVec n

Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. As a numeric operation, this is equivalent to a.toInt >>> s.toNat.

SMT-Lib name: bvashr.

def

BitVec.shiftLeft {n : Nat} (x : BitVec n)
  (s : Nat) : BitVec n

Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is equivalent to x * 2^s, modulo 2^n.

SMT-Lib name: bvshl except this operator uses a Nat shift value.

def

BitVec.shiftLeftZeroExtend {w : Nat}
  (msbs : BitVec w) (m : Nat) : BitVec (w + m)

shiftLeftZeroExtend x n returns zeroExtend (w+n) x <<< n without needing to compute x % 2^(2+n).

14.5.5.8. Arithmetic

These operators treat bitvectors as numbers. Some operations are signed, while others are unsigned. Because bitvectors are understood as two's complement numbers, addition, subtraction and multiplication coincide for the signed and unsigned interpretations.

def

BitVec.add {n : Nat} (x y : BitVec n) : BitVec n

Addition for bit vectors. This can be interpreted as either signed or unsigned addition modulo 2^n.

SMT-Lib name: bvadd.

def

BitVec.sub {n : Nat} (x y : BitVec n) : BitVec n

Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction modulo 2^n.

def

BitVec.mul {n : Nat} (x y : BitVec n) : BitVec n

Multiplication for bit vectors. This can be interpreted as either signed or unsigned multiplication modulo 2^n.

SMT-Lib name: bvmul.

14.5.5.8.1. Unsigned Operations

def

BitVec.udiv {n : Nat} (x y : BitVec n) :
  BitVec n

Unsigned division for bit vectors using the Lean convention where division by zero returns zero.

def

BitVec.smtUDiv {n : Nat} (x y : BitVec n) :
  BitVec n

Unsigned division for bit vectors using the SMT-Lib convention where division by zero returns the allOnes bitvector.

SMT-Lib name: bvudiv.

def

BitVec.umod {n : Nat} (x y : BitVec n) :
  BitVec n

Unsigned modulo for bit vectors.

SMT-Lib name: bvurem.

def

BitVec.uaddOverflow {w : Nat} (x y : BitVec w) :
  Bool

uaddOverflow x y returns true if addition of x and y results in unsigned overflow.

SMT-Lib name: bvuaddo.

14.5.5.8.2. Signed Operations

def

BitVec.abs {n : Nat} (x : BitVec n) : BitVec n

Return the absolute value of a signed bitvector.

def

BitVec.neg {n : Nat} (x : BitVec n) : BitVec n

Negation for bit vectors. This can be interpreted as either signed or unsigned negation modulo 2^n.

SMT-Lib name: bvneg.

def

BitVec.sdiv {n : Nat} (x y : BitVec n) :
  BitVec n

Signed t-division for bit vectors using the Lean convention where division by zero returns zero.

sdiv 7#4 2 = 3#4
sdiv (-9#4) 2 = -4#4
sdiv 5#4 -2 = -2#4
sdiv (-7#4) (-2) = 3#4

def

BitVec.smtSDiv {n : Nat} (x y : BitVec n) :
  BitVec n

Signed division for bit vectors using SMTLIB rules for division by zero.

Specifically, smtSDiv x 0 = if x >= 0 then -1 else 1

SMT-Lib name: bvsdiv.

def

BitVec.smod {m : Nat} (x y : BitVec m) :
  BitVec m

Remainder for signed division rounded to negative infinity.

SMT_Lib name: bvsmod.

def

BitVec.srem {n : Nat} (x y : BitVec n) :
  BitVec n

Remainder for signed division rounding to zero.

SMT_Lib name: bvsrem.

def

BitVec.saddOverflow {w : Nat} (x y : BitVec w) :
  Bool

saddOverflow x y returns true if addition of x and y results in signed overflow, treating x and y as 2's complement signed bitvectors.

SMT-Lib name: bvsaddo.

14.5.5.9. Iteration

def

BitVec.iunfoldr.{u_1} {w : Nat} {α : Type u_1}
  (f : Fin w → α → α × Bool) (s : α) :
  α × BitVec w

iunfoldr is an iterative operation that applies a function f repeatedly.

It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit in v (e.g., getLsb v i = b_i).

Theorems involving iunfoldr can be eliminated using iunfoldr_replace below.

14.5.5.10. Proof Automation

14.5.5.10.1. Bit Blasting

The standard library contains a number of helper implementations that are useful to implement bit blasting, which is the technique used by bv_decide to encode propositions as Boolean satisfiability problems for external solvers.

def

BitVec.adc {w : Nat} (x y : BitVec w) :
  Bool → Bool × BitVec w

Bitwise addition implemented via a ripple carry adder.

def

BitVec.adcb (x y c : Bool) : Bool × Bool

Carry function for bitwise addition.

def

BitVec.carry {w : Nat} (i : Nat)
  (x y : BitVec w) (c : Bool) : Bool

carry i x y c returns true if the i carry bit is true when computing x + y + c.

def

BitVec.mulRec {w : Nat} (x y : BitVec w)
  (s : Nat) : BitVec w

A recurrence that describes multiplication as repeated addition. Is useful for bitblasting multiplication.

def

BitVec.divRec {w : Nat} (m : Nat)
  (args : BitVec.DivModArgs w)
  (qr : BitVec.DivModState w) :
  BitVec.DivModState w

A recursive definition of division for bitblasting, in terms of a shift-subtraction circuit.

def

BitVec.divSubtractShift {w : Nat}
  (args : BitVec.DivModArgs w)
  (qr : BitVec.DivModState w) :
  BitVec.DivModState w

One round of the division algorithm, that tries to perform a subtract shift. Note that this should only be called when r.msb = false, so we will not overflow.

def

BitVec.shiftLeftRec {w₁ w₂ : Nat}
  (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
  BitVec w₁

shiftLeftRec x y n shifts x to the left by the first n bits of y.

The theorem shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and shiftLeftRec.

Together with equations shiftLeftRec_zero, shiftLeftRec_succ, this allows us to unfold shiftLeft into a circuit for bitblasting.

def

BitVec.sshiftRightRec {w₁ w₂ : Nat}
  (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
  BitVec w₁

sshiftRightRec x y n shifts x arithmetically/signed to the right by the first n bits of y. The theorem sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and sshiftRightRec. Together with equations sshiftRightRec_zero, sshiftRightRec_succ, this allows us to unfold sshiftRight into a circuit for bitblasting.

def

BitVec.ushiftRightRec {w₁ w₂ : Nat}
  (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
  BitVec w₁

ushiftRightRec x y n shifts x logically to the right by the first n bits of y.

The theorem shiftRight_eq_ushiftRightRec proves the equivalence of (x >>> y) and ushiftRightRec.

Together with equations ushiftRightRec_zero, ushiftRightRec_succ, this allows us to unfold ushiftRight into a circuit for bitblasting.

14.5.5.10.2. Quotation

def

BitVec.fromExpr? (e : Lean.Expr) :
  Lean.Meta.SimpM (Option BitVec.Literal)

Try to convert OfNat.ofNat/BitVec.OfNat application into a bitvector literal.

14.5.5.10.3. Simprocs

def

BitVec.reduceAbs : Lean.Meta.Simp.DSimproc

Simplification procedure for absolute value of BitVecs.

def

BitVec.reduceAdd : Lean.Meta.Simp.DSimproc

Simplification procedure for addition of BitVecs.

def

BitVec.reduceAllOnes : Lean.Meta.Simp.DSimproc

Simplification procedure for allOnes

def

BitVec.reduceAnd : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise and of BitVecs.

def

BitVec.reduceAppend : Lean.Meta.Simp.DSimproc

Simplification procedure for append on BitVec.

def

BitVec.reduceBEq : Lean.Meta.Simp.DSimproc

Simplification procedure for == on BitVecs.

def

BitVec.reduceBNe : Lean.Meta.Simp.DSimproc

Simplification procedure for != on BitVecs.

def

BitVec.reduceBin (declName : Lean.Name)
  (arity : Nat)
  (op :
    {n : Nat} → BitVec n → BitVec n → BitVec n)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous binary bitvector operators.

def

BitVec.reduceBinPred (declName : Lean.Name)
  (arity : Nat)
  (op : {n : Nat} → BitVec n → BitVec n → Bool)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing bitvector predicates.

def

BitVec.reduceBitVecOfFin :
  Lean.Meta.Simp.DSimproc

def

BitVec.reduceBitVecToFin :
  Lean.Meta.Simp.DSimproc

def

BitVec.reduceBoolPred (declName : Lean.Name)
  (arity : Nat)
  (op : {n : Nat} → BitVec n → BitVec n → Bool)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

BitVec.reduceCast : Lean.Meta.Simp.DSimproc

Simplification procedure for casting BitVecs along an equality of the size.

def

BitVec.reduceDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs.

def

BitVec.reduceEq : Lean.Meta.Simp.Simproc

Simplification procedure for = on BitVecs.

def

BitVec.reduceExtend (declName : Lean.Name)
  (op :
    {n : Nat} → (m : Nat) → BitVec n → BitVec m)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Simplification procedure for setWidth, zeroExtend and signExtend on BitVecs.

def

BitVec.reduceExtracLsb' :
  Lean.Meta.Simp.DSimproc

Simplification procedure for extractLsb' on BitVecs.

def

BitVec.reduceGE : Lean.Meta.Simp.Simproc

Simplification procedure for ≥ on BitVecs.

def

BitVec.reduceGT : Lean.Meta.Simp.Simproc

Simplification procedure for > on BitVecs.

def

BitVec.reduceGetBit (declName : Lean.Name)
  (op : {n : Nat} → BitVec n → Nat → Bool)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as getLsb and getMsb.

def

BitVec.reduceGetElem : Lean.Meta.Simp.DSimproc

Simplification procedure for getElem on BitVec.

def

BitVec.reduceGetLsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getLsb (lowest significant bit) on BitVec.

def

BitVec.reduceGetMsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getMsb (most significant bit) on BitVec.

def

BitVec.reduceHShiftLeft :
  Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def

BitVec.reduceHShiftLeft' :
  Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def

BitVec.reduceHShiftRight :
  Lean.Meta.Simp.DSimproc

Simplification procedure for shift right on BitVec.

def

BitVec.reduceHShiftRight' :
  Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def

BitVec.reduceLE : Lean.Meta.Simp.Simproc

Simplification procedure for ≤ on BitVecs.

def

BitVec.reduceLT : Lean.Meta.Simp.Simproc

Simplification procedure for < on BitVecs.

def

BitVec.reduceMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the modulo operation on BitVecs.

def

BitVec.reduceMul : Lean.Meta.Simp.DSimproc

Simplification procedure for multiplication of BitVecs.

def

BitVec.reduceNe : Lean.Meta.Simp.Simproc

Simplification procedure for ≠ on BitVecs.

def

BitVec.reduceNeg : Lean.Meta.Simp.DSimproc

Simplification procedure for negation of BitVecs.

def

BitVec.reduceNot : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise not of BitVecs.

def

BitVec.reduceOfInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.ofInt.

def

BitVec.reduceOfNat : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring BitVec.ofNat literals are normalized.

def

BitVec.reduceOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise or of BitVecs.

def

BitVec.reduceReplicate : Lean.Meta.Simp.DSimproc

Simplification procedure for replicate on BitVecs.

def

BitVec.reduceRotateLeft :
  Lean.Meta.Simp.DSimproc

Simplification procedure for rotate left on BitVec.

def

BitVec.reduceRotateRight :
  Lean.Meta.Simp.DSimproc

Simplification procedure for rotate right on BitVec.

def

BitVec.reduceSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed t-division of BitVecs.

def

BitVec.reduceSLE : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than or equal sle on BitVecs.

def

BitVec.reduceSLT : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than slt on BitVecs.

def

BitVec.reduceSMTSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed division of BitVecs using the SMT-Lib conventions.

def

BitVec.reduceSMTUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs using the SMT-Lib conventions.

def

BitVec.reduceSMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the signed modulo operation on BitVecs.

def

BitVec.reduceSRem : Lean.Meta.Simp.DSimproc

Simplification procedure for signed remainder of BitVecs.

def

BitVec.reduceSShiftRight :
  Lean.Meta.Simp.DSimproc

Simplification procedure for signed shift right on BitVec.

def

BitVec.reduceSetWidth : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth on BitVecs.

def

BitVec.reduceSetWidth' : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth' on BitVecs.

def

BitVec.reduceShift (declName : Lean.Name)
  (arity : Nat)
  (op : {n : Nat} → BitVec n → Nat → BitVec n)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as shiftLeft and rotateRight.

def

BitVec.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def

BitVec.reduceShiftLeftShiftLeft :
  Lean.Meta.Simp.Simproc

def

BitVec.reduceShiftLeftZeroExtend :
  Lean.Meta.Simp.DSimproc

Simplification procedure for shiftLeftZeroExtend on BitVecs.

def

BitVec.reduceShiftRightShiftRight :
  Lean.Meta.Simp.Simproc

def

BitVec.reduceShiftShift
  (declName thmName : Lean.Name)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing (x <<< i) <<< j (and (x >>> i) >>> j) where i and j are natural number literals.

def

BitVec.reduceShiftWithBitVecLit
  (declName : Lean.Name) (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing x <<< i and x >>> i where i is a bitvector literal, into one that is a natural number literal.

def

BitVec.reduceSignExtend :
  Lean.Meta.Simp.DSimproc

Simplification procedure for signExtend on BitVecs.

def

BitVec.reduceSub : Lean.Meta.Simp.DSimproc

Simplification procedure for subtraction of BitVecs.

def

BitVec.reduceToInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toInt.

def

BitVec.reduceToNat : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toNat.

def

BitVec.reduceUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned division of BitVecs.

def

BitVec.reduceULE : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than or equal ule on BitVecs.

def

BitVec.reduceULT : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than ult on BitVecs.

def

BitVec.reduceUMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the unsigned modulo operation on BitVecs.

def

BitVec.reduceUShiftRight :
  Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned shift right on BitVec.

def

BitVec.reduceUnary (declName : Lean.Name)
  (arity : Nat)
  (op : {n : Nat} → BitVec n → BitVec n)
  (e : Lean.Expr) :
  Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous unary bitvector operators.

def

BitVec.reduceXOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise xor of BitVecs.

def

BitVec.reduceZeroExtend :
  Lean.Meta.Simp.DSimproc

Simplification procedure for zeroExtend on BitVecs.