Init.Data.BitVec.Basic

BitVec.ofNatLt definition

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

Full source

@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
  BitVec.ofNatLT i p

Bitvector from natural number with bound check

Informal description

Given a natural number $ i $ and a proof that $ i < 2^n $, the function returns a bitvector of width $ n $ with value $ i $.

BitVec.natCastInst instance

: NatCast (BitVec w)

Full source

instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩

Natural Number Coercion to Bitvectors

Informal description

For any bitvector width $w$, the type $\text{BitVec}\, w$ has a canonical coercion from the natural numbers, where a natural number $n$ is mapped to the bitvector representing $n \mod 2^w$.

BitVec.ofNat_eq_ofNat theorem

: @OfNat.ofNat (BitVec n) i _ = .ofNat n i

Full source

/-- Theorem for normalizing the bitvector literal representation. -/
-- TODO: This needs more usage data to assess which direction the simp should go.
@[simp, bitvec_to_nat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

Equality of Numeric Literal and Modulo Bitvector Construction

Informal description

For any bitvector width $n$ and natural number $i$, the bitvector constructed from the numeric literal $i$ is equal to the bitvector obtained by taking $i$ modulo $2^n$.

BitVec.natCast_eq_ofNat theorem

(w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x

Full source

@[simp] theorem natCast_eq_ofNat (w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x := rfl

Equality of Natural Coercion and Modulo Construction for Bitvectors

Informal description

For any natural numbers $w$ and $x$, the canonical coercion of $x$ to a bitvector of width $w$ is equal to the bitvector obtained by taking $x \mod 2^w$.

BitVec.instSubsingletonOfNatNat instance

: Subsingleton (BitVec 0)

Full source

/-- All empty bitvectors are equal -/
instance : Subsingleton (BitVec 0) where
  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl

Uniqueness of Empty Bitvectors

Informal description

The type of bitvectors of width 0 is a subsingleton, meaning all bitvectors of width 0 are equal.

BitVec.nil abbrev

: BitVec 0

Full source

/-- The empty bitvector. -/
abbrev nil : BitVec 0 := 0

Empty Bitvector

Informal description

The empty bitvector, denoted as $\text{BitVec}\,0$, is the unique bitvector of width zero.

BitVec.zero definition

(n : Nat) : BitVec n

Full source

/-- Returns a bitvector of size `n` where all bits are `0`. -/
protected def zero (n : Nat) : BitVec n := .ofNatLT 0 (Nat.two_pow_pos n)

Zero bitvector of width $ n $

Informal description

The function returns a bitvector of width $ n $ where all bits are set to $ 0 $. The value is represented as $ 0 $, which is guaranteed to be less than $ 2^n $ for any $ n $.

BitVec.instInhabited instance

: Inhabited (BitVec n)

Full source

instance : Inhabited (BitVec n) where default := .zero n

Inhabitedness of Bitvector Type

Informal description

For any natural number $n$, the type of bitvectors of width $n$ is inhabited, with the default element being the zero bitvector (all bits set to 0).

BitVec.allOnes definition

(n : Nat) : BitVec n

Full source

/-- Returns a bitvector of size `n` where all bits are `1`. -/
def allOnes (n : Nat) : BitVec n :=
  .ofNatLT (2^n - 1) (Nat.le_of_eq (Nat.sub_add_cancel (Nat.two_pow_pos n)))

Bitvector with all bits set to 1

Informal description

The function returns a bitvector of width $ n $ where all $ n $ bits are set to 1. The value is represented as $ 2^n - 1 $, ensuring it fits within $ n $ bits.

BitVec.getLsb' definition

(x : BitVec w) (i : Fin w) : Bool

Full source

/--
Returns the `i`th least significant bit.

This will be renamed `getLsb` after the existing deprecated alias is removed.
-/
@[inline] def getLsb' (x : BitVec w) (i : Fin w) : Bool := x.toNat.testBit i

$ i $-th least significant bit of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and an index $ i $ (where $ i < w $), the function returns the $ i $-th least significant bit of $ x $ as a Boolean value. This is equivalent to testing the $ i $-th bit in the natural number representation of $ x $.

BitVec.getLsb? definition

(x : BitVec w) (i : Nat) : Option Bool

Full source

/-- Returns the `i`th least significant bit, or `none` if `i ≥ w`. -/
@[inline] def getLsb? (x : BitVec w) (i : Nat) : Option Bool :=
  if h : i < w then some (getLsb' x ⟨i, h⟩) else none

Optional $ i $-th least significant bit of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and a natural number $ i $, the function returns the $ i $-th least significant bit of $ x $ as an optional Boolean value. If $ i $ is less than $ w $, it returns `some b` where $ b $ is the $ i $-th bit; otherwise, it returns `none`.

BitVec.getMsb' definition

(x : BitVec w) (i : Fin w) : Bool

Full source

/--
Returns the `i`th most significant bit.

This will be renamed `BitVec.getMsb` after the existing deprecated alias is removed.
-/
@[inline] def getMsb' (x : BitVec w) (i : Fin w) : Bool := x.getLsb' ⟨w-1-i, by omega⟩

$ i $-th most significant bit of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and an index $ i $ (where $ i < w $), the function returns the $ i $-th most significant bit of $ x $ as a Boolean value. This is equivalent to testing the $ (w - 1 - i) $-th least significant bit in the natural number representation of $ x $.

BitVec.getMsb? definition

(x : BitVec w) (i : Nat) : Option Bool

Full source

/-- Returns the `i`th most significant bit or `none` if `i ≥ w`. -/
@[inline] def getMsb? (x : BitVec w) (i : Nat) : Option Bool :=
  if h : i < w then some (getMsb' x ⟨i, h⟩) else none

Optional $ i $-th most significant bit of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and a natural number $ i $, the function returns the $ i $-th most significant bit of $ x $ as an optional Boolean value. If $ i $ is less than $ w $, it returns `some b` where $ b $ is the $ i $-th most significant bit; otherwise, it returns `none`.

BitVec.getLsbD definition

(x : BitVec w) (i : Nat) : Bool

Full source

/-- Returns the `i`th least significant bit or `false` if `i ≥ w`. -/
@[inline] def getLsbD (x : BitVec w) (i : Nat) : Bool :=
  x.toNat.testBit i

Least significant bit of a bitvector with default value

Informal description

The function returns the `i`-th least significant bit of the bitvector `x` of width `w`, interpreted as a Boolean value. If the index `i` is greater than or equal to `w`, the function returns `false`.

BitVec.getMsbD definition

(x : BitVec w) (i : Nat) : Bool

Full source

/-- Returns the `i`th most significant bit, or `false` if `i ≥ w`. -/
@[inline] def getMsbD (x : BitVec w) (i : Nat) : Bool :=
  i < w && x.getLsbD (w-1-i)

Most significant bit of a bitvector with default value

Informal description

The function returns the `i`-th most significant bit of the bitvector `x` of width `w`, interpreted as a Boolean value. If the index `i` is greater than or equal to `w`, the function returns `false`. The function is implemented by checking if `i` is within bounds and then accessing the corresponding least significant bit at position `w-1-i`.

BitVec.msb definition

(x : BitVec n) : Bool

Full source

/-- Returns the most significant bit in a bitvector. -/
@[inline] protected def msb (x : BitVec n) : Bool := getMsbD x 0

Most significant bit of a bitvector

Informal description

The function returns the most significant bit of a bitvector $ x $ of width $ n $, interpreted as a Boolean value. This is equivalent to accessing the bit at index 0 using the `getMsbD` function.

BitVec.instGetElemNatBoolLt instance

: GetElem (BitVec w) Nat Bool fun _ i => i < w

Full source

instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
  getElem xs i h := xs.getLsb' ⟨i, h⟩

Bitvector Indexing with Bounds Check

Informal description

For any bitvector $x$ of width $w$ and natural number index $i$, the notation $x[i]$ returns the $i$-th bit of $x$ (as a Boolean value) when $i < w$ is satisfied. This provides an indexing operation for bitvectors where the validity condition ensures the index is within bounds.

BitVec.getLsb'_eq_getElem theorem

(x : BitVec w) (i : Fin w) : x.getLsb' i = x[i]

Full source

/-- We prefer `x[i]` as the simp normal form for `getLsb'` -/
@[simp] theorem getLsb'_eq_getElem (x : BitVec w) (i : Fin w) :
    x.getLsb' i = x[i] := rfl

Equivalence of Bitvector Indexing Operations: $\text{getLsb'}\,x\,i = x[i]$

Informal description

For any bitvector $x$ of width $w$ and any index $i$ (where $i < w$), the $i$-th least significant bit of $x$ obtained via `getLsb'` is equal to the $i$-th bit accessed via the indexing notation $x[i]$. That is, $\text{getLsb'}\,x\,i = x[i]$.

BitVec.getLsb?_eq_getElem? theorem

(x : BitVec w) (i : Nat) : x.getLsb? i = x[i]?

Full source

/-- We prefer `x[i]?` as the simp normal form for `getLsb?` -/
@[simp] theorem getLsb?_eq_getElem? (x : BitVec w) (i : Nat) :
    x.getLsb? i = x[i]? := rfl

Equivalence of Bitvector Least Significant Bit Access and Optional Indexing: $\text{getLsb?}(x, i) = x[i]?$

Informal description

For any bitvector $x$ of width $w$ and any natural number index $i$, the operation `x.getLsb? i` that retrieves the $i$-th least significant bit of $x$ (returning `none` if $i$ is out of bounds) is equal to the optional element access notation `x[i]?`.

BitVec.getElem_eq_testBit_toNat theorem

(x : BitVec w) (i : Nat) (h : i < w) : x[i] = x.toNat.testBit i

Full source

theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl

Bitvector Indexing Equals TestBit on Natural Representation

Informal description

For any bitvector $x$ of width $w$ and natural number index $i$ such that $i < w$, the $i$-th bit of $x$ (accessed via $x[i]$) is equal to the $i$-th bit of the natural number representation of $x$ (accessed via `testBit`). That is, $x[i] = \text{testBit}(x.\text{toNat}, i)$.

BitVec.getLsbD_eq_getElem theorem

{x : BitVec w} {i : Nat} (h : i < w) : x.getLsbD i = x[i]

Full source

@[simp]
theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
    x.getLsbD i = x[i] := rfl

Equality of Least Significant Bit Access and Indexing for Bitvectors

Informal description

For any bitvector $x$ of width $w$ and any natural number index $i$ such that $i < w$, the $i$-th least significant bit of $x$ (with default value) is equal to the $i$-th bit of $x$ accessed via indexing.

BitVec.toInt definition

(x : BitVec n) : Int

Full source

/--
Interprets the bitvector as an integer stored in two's complement form.
-/
protected def toInt (x : BitVec n) : Int :=
  if 2 * x.toNat < 2^n then
    x.toNat
  else
    (x.toNat : Int) - (2^n : Nat)

Two's complement interpretation of a bitvector

Informal description

The function interprets a bitvector $ x $ of width $ n $ as a two's complement signed integer. If the unsigned value of $ x $ is less than $ 2^{n-1} $, it returns the natural number representation of $ x $. Otherwise, it returns the negative integer obtained by subtracting $ 2^n $ from the unsigned value of $ x $.

BitVec.ofInt definition

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

Full source

/--
Converts an integer to its two's complement representation as a bitvector of the given width `n`,
over- and underflowing as needed.

The underlying `Nat` is `(2^n + (i mod 2^n)) mod 2^n`. Converting the bitvector back to an `Int`
with `BitVec.toInt` results in the value `i.bmod (2^n)`.
-/
protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLT (i % (Int.ofNat (2^n))).toNat (by
  apply (Int.toNat_lt _).mpr
  · apply Int.emod_lt_of_pos
    exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
  · apply Int.emod_nonneg
    intro eq
    apply Nat.ne_of_gt (Nat.two_pow_pos n)
    exact Int.ofNat_inj.mp eq)

Two's complement bitvector from integer

Informal description

Given a bit width $ n $ and an integer $ i $, the function returns a bitvector of width $ n $ representing $ i $ in two's complement form. The value is computed as $ (2^n + (i \bmod 2^n)) \bmod 2^n $, ensuring proper handling of overflow and underflow. When converted back to an integer using `BitVec.toInt`, the result is $ i \bmod 2^n $.

BitVec.instIntCast instance

: IntCast (BitVec w)

Full source

instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩

Integer to Bitvector Cast via Two's Complement

Informal description

For any bit width $w$, there is a canonical way to interpret an integer as a bitvector of width $w$ using two's complement representation.

BitVec.term__#__ definition

: Lean.ParserDescr✝

Full source

/-- Notation for bitvector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
syntax:max num noWs "#" noWs term:max : term

Bitvector literal notation `i#n`

Informal description

The notation `i#n` represents a bitvector literal, where `i` is a natural number and `n` is the bit width. This is shorthand for `BitVec.ofNat n i`, which constructs a bitvector of width `n` containing the value `i`.

BitVec.unexpandBitVecOfNat definition

: Lean.PrettyPrinter.Unexpander

Full source

/-- Unexpander for bitvector literals. -/
@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
  | `($(_) $n $i:num) => `($i:num#$n)
  | _ => throw ()

Bitvector literal unexpander

Informal description

The unexpander function for bitvector literals converts expressions of the form `BitVec.ofNat n i` back into the more concise notation `i#n`, where `i` is a natural number and `n` is the bit width. This function operates within the syntax unexpansion monad and fails if the input syntax doesn't match the expected pattern.

BitVec.term__#'__ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for bitvector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`. -/
scoped syntax:max term:max noWs "#'" noWs term:max : term

Bitvector literal notation

Informal description

The notation `i#'lt` represents a bitvector literal without truncation, where `i` is a natural number and `lt` specifies the bit width. This is syntactic sugar for `BitVec.ofNatLT i lt`, which constructs a bitvector of width `lt` from the natural number `i`.

BitVec.unexpandBitVecOfNatLt definition

: Lean.PrettyPrinter.Unexpander

Full source

/-- Unexpander for bitvector literals without truncation. -/
@[app_unexpander BitVec.ofNatLT] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
  | `($(_) $i $p) => `($i#'$p)
  | _ => throw ()

Bitvector literal unexpander

Informal description

The unexpander function for bitvector literals without truncation converts expressions of the form `BitVec.ofNatLT i p` into the notation `i#'p`, where `i` is a natural number and `p` specifies the bit width. This function operates in the `UnexpandM` monad and will fail if the input syntax doesn't match the expected pattern.

BitVec.toHex definition

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

Full source

/--
Converts a bitvector into a fixed-width hexadecimal number with enough digits to represent it.

If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits are returned.
-/
protected def toHex {n : Nat} (x : BitVec n) : String :=
  let s := (Nat.toDigits 16 x.toNat).asString
  let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
  t ++ s

Bitvector to hexadecimal string conversion

Informal description

The function converts a bitvector $ x $ of width $ n $ into a fixed-width hexadecimal string representation. The number of digits in the output is determined by $ \lfloor (n + 3) / 4 \rfloor $, ensuring that the string has enough digits to represent the bitvector. If $ n = 0 $, the output is a single digit. Leading zeros are added as necessary to maintain the fixed width.

BitVec.instRepr instance

: Repr (BitVec n)

Full source

instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n

Standard Representation of Bitvectors

Informal description

For any bitvector of width $n$, there is a standard representation format that converts it into a human-readable form.

BitVec.instToString instance

: ToString (BitVec n)

Full source

instance : ToString (BitVec n) where toString a := toString (repr a)

String Representation of Bitvectors

Informal description

For any bitvector of width $n$, there is a canonical string representation.

BitVec.neg definition

(x : BitVec n) : BitVec n

Full source

/--
Negation of bitvectors. This can be interpreted as either signed or unsigned negation modulo `2^n`.
Usually accessed via the `-` prefix operator.

SMT-LIB name: `bvneg`.
-/
protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)

Bitvector negation (mod $ 2^n $)

Informal description

The negation operation on bitvectors of width $ n $ is defined as $ \text{neg}(x) = (2^n - x) \mod 2^n $, where $ x $ is interpreted as an unsigned integer. This operation can be viewed as either signed or unsigned negation modulo $ 2^n $.

BitVec.instNeg instance

: Neg (BitVec n)

Full source

instance : Neg (BitVec n) := ⟨.neg⟩

Negation Operation on Bitvectors

Informal description

For any bitvector of width $n$, there is a negation operation defined by $\text{neg}(x) = (2^n - x) \mod 2^n$, where $x$ is interpreted as an unsigned integer.

BitVec.abs definition

(x : BitVec n) : BitVec n

Full source

/--
Returns the absolute value of a signed bitvector.
-/
protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x

Absolute value of a signed bitvector

Informal description

The absolute value of a signed bitvector $ x $ of width $ n $ is defined as follows: if the most significant bit of $ x $ is set (indicating a negative value in two's complement representation), return the negation of $ x $; otherwise, return $ x $ itself. The negation is computed modulo $ 2^n $.

BitVec.mul definition

(x y : BitVec n) : BitVec n

Full source

/--
Multiplies two bitvectors. This can be interpreted as either signed or unsigned multiplication
modulo `2^n`. Usually accessed via the `*` operator.

SMT-LIB name: `bvmul`.
-/
protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)

Bitvector multiplication modulo $ 2^n $

Informal description

The function takes two bitvectors $ x $ and $ y $ of width $ n $ and returns their product as a bitvector of the same width. The multiplication is performed modulo $ 2^n $, interpreting the bitvectors as either signed or unsigned integers. This operation corresponds to the `bvmul` operation in SMT-LIB.

BitVec.instMul instance

: Mul (BitVec n)

Full source

instance : Mul (BitVec n) := ⟨.mul⟩

Multiplication Operation on Bitvectors Modulo $2^n$

Informal description

For any bitvector width $n$, the bitvector type $\text{BitVec}\,n$ has a multiplication operation defined as multiplication modulo $2^n$.

BitVec.udiv definition

(x y : BitVec n) : BitVec n

Full source

/--
Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the `/` operator.
-/
def udiv (x y : BitVec n) : BitVec n :=
  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)

Unsigned division of bitvectors

Informal description

The unsigned division of two bitvectors $ x $ and $ y $ of width $ n $ is defined as the bitvector of width $ n $ whose underlying natural number value is the integer division of the natural number representations of $ x $ and $ y $. If $ y $ is zero, the result is zero.

BitVec.instDiv instance

: Div (BitVec n)

Full source

instance : Div (BitVec n) := ⟨.udiv⟩

Unsigned Division Operation on Bitvectors

Informal description

For any bitvector width $n$, the bitvector type $\text{BitVec}\,n$ has a division operation defined as unsigned division modulo $2^n$.

BitVec.umod definition

(x y : BitVec n) : BitVec n

Full source

/--
Unsigned modulo for bitvectors. Usually accessed via the `%` operator.

SMT-LIB name: `bvurem`.
-/
def umod (x y : BitVec n) : BitVec n :=
  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)

Unsigned modulo for bitvectors (bvurem)

Informal description

For bitvectors $ x $ and $ y $ of width $ n $, the unsigned modulo operation $ \text{umod}(x, y) $ returns a bitvector of width $ n $ whose underlying natural number value is $ x \mod y $, where $ x $ and $ y $ are interpreted as unsigned integers. This operation corresponds to the `bvurem` operation in SMT-LIB.

BitVec.instMod instance

: Mod (BitVec n)

Full source

instance : Mod (BitVec n) := ⟨.umod⟩

Modulo Operation on Bitvectors

Informal description

For any bitvector width $n$, the bitvector type $\text{BitVec}\,n$ is equipped with a modulo operation that corresponds to the unsigned modulo operation on bitvectors (bvurem in SMT-LIB). This operation takes two bitvectors $x$ and $y$ of width $n$ and returns a bitvector of width $n$ whose value is $x \mod y$, where $x$ and $y$ are interpreted as unsigned integers.

BitVec.smtUDiv definition

(x y : BitVec n) : BitVec n

Full source

/--
Unsigned division of bitvectors using the
[SMT-LIB convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml),
where division by zero returns `BitVector.allOnes n`.

SMT-LIB name: `bvudiv`.
-/
def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then allOnes n else udiv x y

Unsigned division of bitvectors (SMT-LIB convention)

Informal description

The unsigned division operation for bitvectors of width $ n $, following the SMT-LIB convention. Given two bitvectors $ x $ and $ y $, it returns $ x $ divided by $ y $ when $ y $ is nonzero, and a bitvector with all bits set to 1 (i.e., $ 2^n - 1 $) when $ y $ is zero.

BitVec.sdiv definition

(x y : BitVec n) : BitVec n

Full source

/--
Signed T-division (using the truncating rounding convention) for bitvectors. This function obeys the
Lean convention that division by zero returns zero.

Examples:
* `(7#4).sdiv 2 = 3#4`
* `(-9#4).sdiv 2 = -4#4`
* `(5#4).sdiv -2 = -2#4`
* `(-7#4).sdiv (-2) = 3#4`
-/
def sdiv (x y : BitVec n) : BitVec n :=
  match x.msb, y.msb with
  | false, false => udiv x y
  | false, true  => .neg (udiv x (.neg y))
  | true,  false => .neg (udiv (.neg x) y)
  | true,  true  => udiv (.neg x) (.neg y)

Signed division of bitvectors (truncating convention)

Informal description

The signed division operation for bitvectors of width $ n $ (using truncating rounding convention). Given two bitvectors $ x $ and $ y $, it returns: - $ x $ divided by $ y $ when both $ x $ and $ y $ are non-negative, - the negation of $ x $ divided by the negation of $ y $ when both $ x $ and $ y $ are negative, - the negation of $ x $ divided by $ y $ when $ x $ is negative and $ y $ is non-negative, - the negation of $ x $ divided by the negation of $ y $ when $ x $ is non-negative and $ y $ is negative. If $ y $ is zero, the result is zero.

BitVec.smtSDiv definition

(x y : BitVec n) : BitVec n

Full source

/--
Signed division for bitvectors using the SMT-LIB using the
[SMT-LIB convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml),
where division by zero returns `BitVector.allOnes n`.

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

SMT-LIB name: `bvsdiv`.
-/
def smtSDiv (x y : BitVec n) : BitVec n :=
  match x.msb, y.msb with
  | false, false => smtUDiv x y
  | false, true  => .neg (smtUDiv x (.neg y))
  | true,  false => .neg (smtUDiv (.neg x) y)
  | true,  true  => smtUDiv (.neg x) (.neg y)

Signed division of bitvectors (SMT-LIB convention)

Informal description

The signed division operation for bitvectors of width $ n $, following the SMT-LIB convention. Given two bitvectors $ x $ and $ y $, it returns: - $ x $ divided by $ y $ (using unsigned division) if both $ x $ and $ y $ are non-negative (i.e., their most significant bits are false), - the negation of $ x $ divided by the negation of $ y $ if $ x $ is non-negative and $ y $ is negative, - the negation of the negation of $ x $ divided by $ y $ if $ x $ is negative and $ y $ is non-negative, - the negation of $ x $ divided by the negation of $ y $ if both $ x $ and $ y $ are negative. In the case of division by zero, the result is a bitvector with all bits set to 1 (i.e., $ 2^n - 1 $) if $ x $ is non-negative, and a bitvector with all bits set to 0 except the least significant bit (i.e., 1) if $ x $ is negative.

BitVec.srem definition

(x y : BitVec n) : BitVec n

Full source

/--
Remainder for signed division rounding to zero.

SMT-LIB name: `bvsrem`.
-/
def srem (x y : BitVec n) : BitVec n :=
  match x.msb, y.msb with
  | false, false => umod x y
  | false, true  => umod x (.neg y)
  | true,  false => .neg (umod (.neg x) y)
  | true,  true  => .neg (umod (.neg x) (.neg y))

Signed remainder for bitvectors (bvsrem)

Informal description

The signed remainder operation for bitvectors of width $ n $, denoted as $ \text{srem}(x, y) $, is defined as follows based on the most significant bits (sign bits) of $ x $ and $ y $: 1. If both $ x $ and $ y $ are non-negative (i.e., their most significant bits are false), then $ \text{srem}(x, y) = x \mod y $ (unsigned modulo). 2. If $ x $ is non-negative and $ y $ is negative, then $ \text{srem}(x, y) = x \mod (-y) $. 3. If $ x $ is negative and $ y $ is non-negative, then $ \text{srem}(x, y) = -((-x) \mod y) $. 4. If both $ x $ and $ y $ are negative, then $ \text{srem}(x, y) = -((-x) \mod (-y)) $. This operation corresponds to the `bvsrem` operation in SMT-LIB, which computes the remainder of signed division rounding towards zero.

BitVec.smod definition

(x y : BitVec m) : BitVec m

Full source

/--
Remainder for signed division rounded to negative infinity.

SMT-LIB name: `bvsmod`.
-/
def smod (x y : BitVec m) : BitVec m :=
  match x.msb, y.msb with
  | false, false => umod x y
  | false, true =>
    let u := umod x (.neg y)
    (if u = .zero m then u else .add u y)
  | true, false =>
    let u := umod (.neg x) y
    (if u = .zero m then u else .sub y u)
  | true, true => .neg (umod (.neg x) (.neg y))

Signed modulo for bitvectors (rounding to negative infinity)

Informal description

The signed modulo operation for bitvectors of width $ m $, denoted $\text{smod}(x, y)$, computes the remainder of signed division rounded towards negative infinity. It is defined as follows based on the most significant bits (sign bits) of $ x $ and $ y $: 1. If both $ x $ and $ y $ are non-negative (i.e., their most significant bits are false), then $\text{smod}(x, y) = \text{umod}(x, y)$ (unsigned modulo). 2. If $ x $ is non-negative and $ y $ is negative, then: - Compute $ u = \text{umod}(x, -y) $. - If $ u = 0 $, return $ u $; otherwise, return $ u + y $. 3. If $ x $ is negative and $ y $ is non-negative, then: - Compute $ u = \text{umod}(-x, y) $. - If $ u = 0 $, return $ u $; otherwise, return $ y - u $. 4. If both $ x $ and $ y $ are negative, then $\text{smod}(x, y) = -\text{umod}(-x, -y)$. This operation corresponds to the `bvsmod` operation in SMT-LIB.

BitVec.ofBool definition

(b : Bool) : BitVec 1

Full source

/-- Turns a `Bool` into a bitvector of length `1`. -/
def ofBool (b : Bool) : BitVec 1 := cond b 1 0

Bitvector representation of a Boolean value

Informal description

The function maps a Boolean value $b$ to a bitvector of length $1$, where $b = \text{true}$ is represented as $1$ and $b = \text{false}$ is represented as $0$.

BitVec.ofBool_false theorem

: ofBool false = 0

Full source

@[simp] theorem ofBool_false : ofBool false = 0 := by trivial

Bitvector Representation of False: $\text{ofBool}(\text{false}) = 0$

Informal description

The bitvector representation of the Boolean value `false` is equal to the bitvector `0` of width 1, i.e., $\text{ofBool}(\text{false}) = 0$.

BitVec.ofBool_true theorem

: ofBool true = 1

Full source

@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial

Bitvector representation of `true` equals `1`

Informal description

The bitvector representation of the Boolean value `true` as a 1-bit bitvector is equal to the bitvector `1`.

BitVec.fill definition

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

Full source

/-- Fills a bitvector with `w` copies of the bit `b`. -/
def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0

Bitvector filled with a single bit value

Informal description

Given a width $ w $ and a bit $ b $, the function `BitVec.fill` constructs a bitvector of width $ w $ where every bit is set to $ b $. Specifically, if $ b $ is true, the result is the bitvector with all bits set to 1 (represented as $-1$ in two's complement), and if $ b $ is false, the result is the bitvector with all bits set to 0.

BitVec.ult definition

(x y : BitVec n) : Bool

Full source

/--
Unsigned less-than for bitvectors.

SMT-LIB name: `bvult`.
-/
protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat

Unsigned less-than for bitvectors (`bvult`)

Informal description

The function `BitVec.ult` takes two bitvectors `x` and `y` of width `n` and returns a boolean indicating whether the natural number representation of `x` is strictly less than that of `y`. This corresponds to the unsigned less-than comparison for bitvectors, denoted as `bvult` in SMT-LIB.

BitVec.ule definition

(x y : BitVec n) : Bool

Full source

/--
Unsigned less-than-or-equal-to for bitvectors.

SMT-LIB name: `bvule`.
-/
protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat

Unsigned less-than-or-equal-to for bitvectors (`bvule`)

Informal description

The function `BitVec.ule` takes two bitvectors `x` and `y` of width `n` and returns a Boolean value indicating whether the natural number representation of `x` is less than or equal to the natural number representation of `y`. This corresponds to the unsigned less-than-or-equal-to comparison for bitvectors, denoted as `bvule` in SMT-LIB v2.

BitVec.slt definition

(x y : BitVec n) : Bool

Full source

/--
Signed less-than for bitvectors.

SMT-LIB name: `bvslt`.

Examples:
 * `BitVec.slt 6#4 7 = true`
 * `BitVec.slt 7#4 8 = false`
-/
protected def slt (x y : BitVec n) : Bool := x.toInt < y.toInt

Signed less-than for bitvectors (`bvslt`)

Informal description

The function `BitVec.slt` takes two bitvectors `x` and `y` of width `n` and returns a boolean indicating whether the two's complement signed integer interpretation of `x` is strictly less than that of `y`. This corresponds to the signed less-than comparison for bitvectors, denoted as `bvslt` in SMT-LIB.

BitVec.sle definition

(x y : BitVec n) : Bool

Full source

/--
Signed less-than-or-equal-to for bitvectors.

SMT-LIB name: `bvsle`.
-/
protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt

Signed less-than-or-equal-to for bitvectors (`bvsle`)

Informal description

The function `BitVec.sle` takes two bitvectors `x` and `y` of width `n` and returns a Boolean value indicating whether the two's complement signed integer interpretation of `x` is less than or equal to that of `y`. This corresponds to the signed less-than-or-equal-to comparison for bitvectors, denoted as `bvsle` in SMT-LIB v2.

BitVec.cast definition

(eq : n = m) (x : BitVec n) : BitVec m

Full source

/--
If two natural numbers `n` and `m` are equal, then a bitvector of width `n` is also a bitvector of
width `m`.

Using `x.cast eq` should be preferred over `eq ▸ x` because there are special-purpose `simp` lemmas
that can more consistently simplify `BitVec.cast` away.
-/
@[inline] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLT x.toNat (eq ▸ x.isLt)

Bitvector width cast

Informal description

Given a proof that two natural numbers $ n $ and $ m $ are equal, the function converts a bitvector of width $ n $ to a bitvector of width $ m $. The underlying value of the bitvector remains unchanged, and the operation is valid because $ x < 2^n $ implies $ x < 2^m $ when $ n = m $.

BitVec.cast_ofNat theorem

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

Full source

@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
    (BitVec.ofNat n x).cast h = BitVec.ofNat m x := by
  subst h; rfl

Commutativity of Bitvector Cast and Construction: $(x \mod 2^n).\text{cast}_h = x \mod 2^m$ when $n = m$

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any natural number $x$, casting the bitvector created from $x$ with width $n$ to width $m$ (using the equality proof $h$) results in the same bitvector as directly creating a bitvector from $x$ with width $m$.

BitVec.cast_cast theorem

{n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) : (x.cast h₁).cast h₂ = x.cast (h₁ ▸ h₂)

Full source

@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
    (x.cast h₁).cast h₂ = x.cast (h₁ ▸ h₂) :=
  rfl

Transitivity of Bitvector Casting: $(x \text{ cast } h₁) \text{ cast } h₂ = x \text{ cast } (h₁ \circ h₂)$

Informal description

For any natural numbers $n$, $m$, and $k$, if $n = m$ and $m = k$, then for any bitvector $x$ of width $n$, casting $x$ to width $m$ and then to width $k$ is equal to casting $x$ directly to width $k$ using the transitivity of equality $n = k$.

BitVec.cast_eq theorem

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

Full source

@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) : x.cast h = x := rfl

Bitvector Cast to Same Width is Identity

Informal description

For any bitvector $x$ of width $n$ and any proof $h$ that $n = n$, casting $x$ to the same width $n$ via $h$ results in $x$ itself, i.e., $x.\text{cast}(h) = x$.

BitVec.extractLsb' definition

(start len : Nat) (x : BitVec n) : BitVec len

Full source

/--
Extracts the bits `start` to `start + len - 1` from a bitvector of size `n` to yield a
new bitvector of size `len`. If `start + len > n`, then the bitvector is zero-extended.
-/
def extractLsb' (start len : Nat) (x : BitVec n) : BitVec len := .ofNat _ (x.toNat >>> start)

Bitvector extraction with zero-extension

Informal description

Given a bitvector $x$ of width $n$ and two natural numbers `start` and `len`, the function extracts a subsequence of $len$ bits starting from position `start` (0-based index). If `start + len` exceeds $n$, the result is zero-extended to maintain the specified length $len$. The result is a new bitvector of width $len$.

BitVec.extractLsb definition

(hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1)

Full source

/--
Extracts the bits from `hi` down to `lo` (both inclusive) from a bitvector, which is implicitly
zero-extended if necessary.

The resulting bitvector has size `hi - lo + 1`.

SMT-LIB name: `extract`.
-/
def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x

Bitvector extraction from $hi$ to $lo$ (inclusive) with zero-extension

Informal description

Given a bitvector $x$ of width $n$ and two natural numbers $hi$ and $lo$ (with $hi \geq lo$), the function extracts the subsequence of bits from position $lo$ to $hi$ (inclusive) from $x$. If necessary, the result is zero-extended to ensure the output has width $hi - lo + 1$. The operation corresponds to the SMT-LIB `extract` function.

BitVec.setWidth' definition

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

Full source

/--
Increases the width of a bitvector to one that is at least as large by zero-extending it.

This is a constant-time operation because the underlying `Nat` is unmodified; because the new width
is at least as large as the old one, no overflow is possible.
-/
def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
  x.toNat#'(by
    apply Nat.lt_of_lt_of_le x.isLt
    exact Nat.pow_le_pow_right (by trivial) le)

Zero-extension of a bitvector to a larger width

Informal description

Given a bitvector $x$ of width $n$ and a proof that $n \leq w$, the function returns a bitvector of width $w$ by zero-extending $x$. This operation is performed in constant time since the underlying natural number representation remains unchanged, and the proof ensures no overflow occurs.

BitVec.zeroExtend' abbrev

Full source

@[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'

Zero-extension of bitvector to larger width

Informal description

Given a bitvector $x$ of width $n$ and a proof that $n \leq w$, the function returns a bitvector of width $w$ by zero-extending $x$. This operation preserves the original value while increasing its width by padding with zeros on the most significant side.

BitVec.shiftLeftZeroExtend definition

(msbs : BitVec w) (m : Nat) : BitVec (w + m)

Full source

/--
Returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`.
-/
def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) :=
  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w + m) := by
        simp [Nat.shiftLeft_eq, Nat.pow_add]
        apply Nat.mul_lt_mul_of_pos_right p
        exact (Nat.two_pow_pos m)
  (msbs.toNat <<< m)#'(shiftLeftLt msbs.isLt m)

Left-shift and zero-extend a bitvector

Informal description

Given a bitvector `msbs` of width `w` and a natural number `m`, the function returns a bitvector of width `w + m` obtained by left-shifting `msbs` by `m` bits and zero-extending the result. This operation avoids the need to compute the modulus `msbs % 2^(w + m)` explicitly by leveraging the fact that the shift operation naturally produces a value within the desired bounds.

BitVec.setWidth definition

(v : Nat) (x : BitVec w) : BitVec v

Full source

/--
Transforms a bitvector of length `w` into a bitvector of length `v`, padding with `0` as needed.

The specific behavior depends on the relationship between the starting width `w` and the final width
`v`:
 * If `v > w`, it is zero-extended; the high bits are padded with zeroes until the bitvector has `v`
   bits.
 * If `v = w`, the bitvector is returned unchanged.
 * If `v < w`, the high bits are truncated.

`BitVec.setWidth`, `BitVec.zeroExtend`, and `BitVec.truncate` are aliases for this operation.

SMT-LIB name: `zero_extend`.
-/
def setWidth (v : Nat) (x : BitVec w) : BitVec v :=
  if h : w ≤ v then
    setWidth' h x
  else
    .ofNat v x.toNat

Bitvector width adjustment (zero-extend/truncate)

Informal description

Given a bitvector $ x $ of width $ w $ and a target width $ v $, this function transforms $ x $ into a bitvector of width $ v $. The behavior depends on the relationship between $ w $ and $ v $: - If $ v > w $, the bitvector is zero-extended by padding with zeros in the high bits. - If $ v = w $, the bitvector is returned unchanged. - If $ v < w $, the high bits are truncated. This operation is also known as `zero_extend` in SMT-LIB terminology.

BitVec.zeroExtend abbrev

Full source

@[inherit_doc setWidth]
abbrev zeroExtend := @setWidth

Bitvector Zero Extension/Truncation to Width $v$

Informal description

Given a bitvector $x$ of width $w$ and a target width $v$, the function `zeroExtend` transforms $x$ into a bitvector of width $v$ by zero-extending (padding with zeros in the high bits) if $v > w$, or truncating (discarding high bits) if $v < w$. If $v = w$, the bitvector is returned unchanged.

BitVec.truncate abbrev

Full source

@[inherit_doc setWidth]
abbrev truncate := @setWidth

Bitvector Truncation Operation

Informal description

Given a bitvector $x$ of width $w$, the operation `truncate` reduces the width of $x$ to a specified smaller width $v$ by discarding the most significant bits (high bits). The resulting bitvector has width $v$ and consists of the $v$ least significant bits of $x$.

BitVec.signExtend definition

(v : Nat) (x : BitVec w) : BitVec v

Full source

/--
Transforms a bitvector of length `w` into a bitvector of length `v`, padding as needed with the most
significant bit's value.

If `x` is an empty bitvector, then the sign is treated as zero.

SMT-LIB name: `sign_extend`.
-/
def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt

Sign extension of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and a target width $ v $, the function extends $ x $ to width $ v $ by padding with the value of the most significant bit (sign bit). If $ x $ is empty (i.e., $ w = 0 $), the padding is treated as zero. The operation preserves the two's complement interpretation of the bitvector.

BitVec.and definition

(x y : BitVec n) : BitVec n

Full source

/--
Bitwise and for bitvectors. Usually accessed via the `&&&` operator.

SMT-LIB name: `bvand`.

Example:
 * `0b1010#4 &&& 0b0110#4 = 0b0010#4`
-/
protected def and (x y : BitVec n) : BitVec n :=
  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)

Bitwise AND of bitvectors

Informal description

The bitwise AND operation on two bitvectors $ x $ and $ y $ of the same width $ n $, returning a new bitvector of width $ n $ where each bit is the logical AND of the corresponding bits in $ x $ and $ y $. The operation is performed by converting the bitvectors to their natural number representations, applying the natural number bitwise AND operation, and then converting back to a bitvector while ensuring the result fits within $ n $ bits. **Example:** \[ 0b1010\#4 \mathbin{\&\&\&} 0b0110\#4 = 0b0010\#4 \]

BitVec.instAndOp instance

: AndOp (BitVec w)

Full source

instance : AndOp (BitVec w) := ⟨.and⟩

Bitwise AND Operation on Bitvectors

Informal description

For any bitvector of width $w$, there is a bitwise AND operation defined on it, where the operation takes two bitvectors of the same width and returns a new bitvector where each bit is the logical AND of the corresponding bits in the input vectors.

BitVec.or definition

(x y : BitVec n) : BitVec n

Full source

/--
Bitwise or for bitvectors. Usually accessed via the `|||` operator.

SMT-LIB name: `bvor`.

Example:
 * `0b1010#4 ||| 0b0110#4 = 0b1110#4`
-/
protected def or (x y : BitVec n) : BitVec n :=
  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)

Bitwise OR for bitvectors

Informal description

The bitwise OR operation for bitvectors of width $ n $. Given two bitvectors $ x $ and $ y $, it returns a new bitvector where each bit is the logical OR of the corresponding bits in $ x $ and $ y $. This operation is denoted by `|||` in practice. Example: $ 0b1010\#4 \mathbin{|||} 0b0110\#4 = 0b1110\#4 $, where $ \#4 $ denotes a bitvector of width 4.

BitVec.instOrOp instance

: OrOp (BitVec w)

Full source

instance : OrOp (BitVec w) := ⟨.or⟩

Bitwise OR Operation on Bitvectors

Informal description

For any bitvector width $w$, the bitwise OR operation `|||` is defined on bitvectors of width $w$, where for any two bitvectors $x$ and $y$, the operation $x \mathbin{|||} y$ returns a new bitvector where each bit is the logical OR of the corresponding bits in $x$ and $y$.

BitVec.xor definition

(x y : BitVec n) : BitVec n

Full source

/--
Bitwise xor for bitvectors. Usually accessed via the `^^^` operator.

SMT-LIB name: `bvxor`.

Example:
 * `0b1010#4 ^^^ 0b0110#4 = 0b1100#4`
-/
protected def xor (x y : BitVec n) : BitVec n :=
  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)

Bitwise XOR for bitvectors

Informal description

The bitwise XOR operation for bitvectors of width $ n $. Given two bitvectors $ x $ and $ y $, it returns a new bitvector where each bit is the XOR of the corresponding bits in $ x $ and $ y $. The operation is performed by converting the bitvectors to natural numbers, applying the natural number XOR operation, and then converting back to a bitvector while ensuring the result fits within $ n $ bits. **Example:** \[ \text{0b1010\#4} \oplus \text{0b0110\#4} = \text{0b1100\#4} \]

BitVec.instXor instance

: Xor (BitVec w)

Full source

instance : Xor (BitVec w) := ⟨.xor⟩

Bitwise XOR Operation on Bitvectors

Informal description

For any bitvector width $w$, the bitvector type $\text{BitVec}\,w$ has a homogeneous XOR operation defined by performing bitwise XOR on the underlying natural number representations.

BitVec.not definition

(x : BitVec n) : BitVec n

Full source

/--
Bitwise complement for bitvectors. Usually accessed via the `~~~` prefix operator.

SMT-LIB name: `bvnot`.

Example:
 * `~~~(0b0101#4) == 0b1010`
-/
protected def not (x : BitVec n) : BitVec n := allOnes n ^^^ x

Bitwise complement (NOT) for bitvectors

Informal description

The bitwise complement (NOT) operation for a bitvector $ x $ of width $ n $. It returns a new bitvector where each bit is the logical negation of the corresponding bit in $ x $. This is implemented as the bitwise XOR of $ x $ with a bitvector of all ones (i.e., $ \text{allOnes}\,n \oplus x $). **Example:** \[ \sim \text{0b0101\#4} = \text{0b1010\#4} \]

BitVec.instComplement instance

: Complement (BitVec w)

Full source

instance : Complement (BitVec w) := ⟨.not⟩

Bitwise Complement Operation on Bitvectors

Informal description

For any bitvector width $w$, the bitvector type $\text{BitVec}\,w$ has a logical complement operation defined by performing bitwise negation on the underlying natural number representation.

BitVec.shiftLeft definition

(x : BitVec n) (s : Nat) : BitVec n

Full source

/--
Shifts a bitvector to the left. 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.
-/
protected def shiftLeft (x : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (x.toNat <<< s)

Left shift operation on bitvectors

Informal description

The left shift operation on a bitvector $ x $ of width $ n $ by $ s $ positions, where the low bits are filled with zeros. Numerically, this is equivalent to $ x \cdot 2^s \mod 2^n $.

BitVec.instHShiftLeftNat instance

: HShiftLeft (BitVec w) Nat (BitVec w)

Full source

instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩

Left Shift Operation on Bitvectors

Informal description

For any bitvector $x$ of width $w$ and natural number $s$, the left shift operation $x \lll s$ produces another bitvector of width $w$ where the bits of $x$ are shifted left by $s$ positions, filling the low bits with zeros. Numerically, this is equivalent to $x \cdot 2^s \mod 2^w$.

BitVec.ushiftRight definition

(x : BitVec n) (s : Nat) : BitVec n

Full source

/--
Shifts a bitvector to the right. This is a logical right shift - 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 ushiftRight (x : BitVec n) (s : Nat) : BitVec n :=
  (x.toNat >>> s)#'(by
  let ⟨x, lt⟩ := x
  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
  rw [←Nat.mul_one x]
  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1))

Logical right shift of a bitvector

Informal description

The function performs a logical right shift on a bitvector $ x $ of width $ n $ by $ s $ positions. The high bits are filled with zeros. Numerically, this operation is equivalent to $ \lfloor x / 2^s \rfloor $, where $ x $ is interpreted as an unsigned integer.

BitVec.instHShiftRightNat instance

: HShiftRight (BitVec w) Nat (BitVec w)

Full source

instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩

Logical Right Shift Operation on Bitvectors by Natural Numbers

Informal description

For any bitvector of width $w$, there is a right shift operation that takes a natural number $s$ and returns a bitvector of width $w$. This operation performs a logical right shift, filling the high bits with zeros.

BitVec.sshiftRight definition

(x : BitVec n) (s : Nat) : BitVec n

Full source

/--
Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with
most significant bit's value.

As a numeric operation, this is equivalent to `x.toInt >>> s`.

SMT-LIB name: `bvashr` except this operator uses a `Nat` shift value.
-/
def sshiftRight (x : BitVec n) (s : Nat) : BitVec n := .ofInt n (x.toInt >>> s)

Arithmetic right shift of a bitvector

Informal description

The function performs an arithmetic right shift on a bitvector $ x $ of width $ n $ by $ s $ positions. The high bits are filled with the value of the most significant bit (sign extension). Numerically, this operation is equivalent to the two's complement interpretation of $ x $ right-shifted by $ s $ positions, i.e., $ \lfloor x / 2^s \rfloor $ where $ x $ is treated as a signed integer.

BitVec.instHShiftLeft instance

{n} : HShiftLeft (BitVec m) (BitVec n) (BitVec m)

Full source

instance {n} : HShiftLeft  (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩

Left Shift Operation on Bitvectors by Bitvectors

Informal description

For any bitvector $x$ of width $m$ and bitvector $s$ of width $n$, the left shift operation $x \lll s$ produces another bitvector of width $m$ where the bits of $x$ are shifted left by the value of $s$ (interpreted as a natural number), filling the low bits with zeros. Numerically, this is equivalent to $x \cdot 2^{\text{val}(s)} \mod 2^m$, where $\text{val}(s)$ is the natural number value of $s$.

BitVec.instHShiftRight instance

{n} : HShiftRight (BitVec m) (BitVec n) (BitVec m)

Full source

instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >>> y.toNat⟩

Logical Right Shift Operation on Bitvectors by Bitvectors

Informal description

For any bitvector $x$ of width $m$ and bitvector $s$ of width $n$, the right shift operation $x \ggg s$ produces another bitvector of width $m$ where the bits of $x$ are shifted right by the value of $s$ (interpreted as a natural number), filling the high bits with zeros. Numerically, this is equivalent to $\lfloor x / 2^{\text{val}(s)} \rfloor \mod 2^m$, where $\text{val}(s)$ is the natural number value of $s$.

BitVec.sshiftRight' definition

(a : BitVec n) (s : BitVec m) : BitVec n

Full source

/--
Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with
most significant bit's value.

As a numeric operation, this is equivalent to `a.toInt >>> s.toNat`.

SMT-LIB name: `bvashr`.
-/
def sshiftRight' (a : BitVec n) (s : BitVec m) : BitVec n := a.sshiftRight s.toNat

Arithmetic right shift of a bitvector by another bitvector

Informal description

The function performs an arithmetic right shift on a bitvector $ a $ of width $ n $ by $ s $ positions, where $ s $ is another bitvector of width $ m $. The high bits are filled with the value of the most significant bit (sign extension). Numerically, this operation is equivalent to the two's complement interpretation of $ a $ right-shifted by $ s $ positions, i.e., $ \lfloor a / 2^s \rfloor $ where $ a $ is treated as a signed integer.

BitVec.rotateLeftAux definition

(x : BitVec w) (n : Nat) : BitVec w

Full source

/-- Auxiliary function for `rotateLeft`, which does not take into account the case where
the rotation amount is greater than the bitvector width. -/
def rotateLeftAux (x : BitVec w) (n : Nat) : BitVec w :=
  x <<< n ||| x >>> (w - n)

Auxiliary left rotation of a bitvector

Informal description

Given a bitvector $x$ of width $w$ and a natural number $n$, the auxiliary rotation function computes the left rotation of $x$ by $n$ positions. This is achieved by taking the bitwise OR of the left shift of $x$ by $n$ positions and the logical right shift of $x$ by $w - n$ positions.

BitVec.rotateLeft definition

(x : BitVec w) (n : Nat) : BitVec w

Full source

/--
Rotates the bits in a bitvector to the left.

All the bits of `x` are shifted to higher positions, with the top `n` bits wrapping around to fill
the vacated low bits.

SMT-LIB name: `rotate_left`, except this operator uses a `Nat` shift amount.

Example:
 * `(0b0011#4).rotateLeft 3 = 0b1001`
-/
def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := rotateLeftAux x (n % w)

Left rotation of a bitvector

Informal description

Given a bitvector $x$ of width $w$ and a natural number $n$, the left rotation function computes the left rotation of $x$ by $n$ positions modulo $w$. This operation shifts all bits of $x$ to higher positions, with the top $n \bmod w$ bits wrapping around to fill the vacated low bits.

BitVec.rotateRightAux definition

(x : BitVec w) (n : Nat) : BitVec w

Full source

/--
Auxiliary function for `rotateRight`, which does not take into account the case where
the rotation amount is greater than the bitvector width.
-/
def rotateRightAux (x : BitVec w) (n : Nat) : BitVec w :=
  x >>> n ||| x <<< (w - n)

Auxiliary right rotation of a bitvector

Informal description

Given a bitvector $x$ of width $w$ and a natural number $n$, the auxiliary function for right rotation computes the right rotation of $x$ by $n$ positions. This is achieved by taking the bitwise OR of the logical right shift of $x$ by $n$ positions and the left shift of $x$ by $w - n$ positions. Note that this function does not handle cases where $n$ exceeds $w$.

BitVec.rotateRight definition

(x : BitVec w) (n : Nat) : BitVec w

Full source

/--
Rotates the bits in a bitvector to the right.

All the bits of `x` are shifted to lower positions, with the bottom `n` bits wrapping around to fill
the vacated high bits.

SMT-LIB name: `rotate_right`, except this operator uses a `Nat` shift amount.

Example:
 * `rotateRight 0b01001#5 1 = 0b10100`
-/
def rotateRight (x : BitVec w) (n : Nat) : BitVec w := rotateRightAux x (n % w)

Right rotation of a bitvector

Informal description

Given a bitvector $ x $ of width $ w $ and a natural number $ n $, the right rotation of $ x $ by $ n $ positions is defined as the right rotation of $ x $ by $ n \mod w $ positions. This operation shifts all bits of $ x $ to lower positions, with the bottom $ n \mod w $ bits wrapping around to fill the vacated high bits. **Example:** For a 5-bit bitvector $ x = 0b01001 $, rotating right by 1 position yields $ 0b10100 $.

BitVec.append definition

(msbs : BitVec n) (lsbs : BitVec m) : BitVec (n + m)

Full source

/--
Concatenates two bitvectors using the “big-endian” convention that the more significant
input is on the left. Usually accessed via the `++` operator.

SMT-LIB name: `concat`.

Example:
 * `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
-/
def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
  shiftLeftZeroExtend msbs m ||| setWidth' (Nat.le_add_left m n) lsbs

Bitvector concatenation (big-endian)

Informal description

Given two bitvectors `msbs` of width `n` and `lsbs` of width `m`, the function returns a new bitvector of width `n + m` obtained by concatenating `msbs` and `lsbs` in big-endian order (with `msbs` as the more significant bits). This is implemented by left-shifting `msbs` by `m` bits and zero-extending it to width `n + m`, then performing a bitwise OR with `lsbs` zero-extended to width `n + m`.

BitVec.instHAppendHAddNat instance

: HAppend (BitVec w) (BitVec v) (BitVec (w + v))

Full source

instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩

Bitvector Concatenation via Heterogeneous Append

Informal description

For any two bitvectors of widths $w$ and $v$, there is a heterogeneous append operation that concatenates them into a new bitvector of width $w + v$.

BitVec.replicate definition

: (i : Nat) → BitVec w → BitVec (w * i)

Full source

/-- Concatenates `i` copies of `x` into a new vector of length `w * i`. -/
def replicate : (i : Nat) → BitVec w → BitVec (w*i)
  | 0,   _ => 0#0
  | n+1, x =>
    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega)

Repeated concatenation of a bitvector

Informal description

Given a natural number $ i $ and a bitvector $ x $ of width $ w $, the function constructs a new bitvector of width $ w \cdot i $ by concatenating $ i $ copies of $ x $. When $ i = 0 $, the result is the zero bitvector of width 0.

BitVec.concat definition

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

Full source

/-- 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 concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)

Bitvector concatenation with a Boolean least significant bit

Informal description

Given a bitvector `msbs` of width `n` and a Boolean value `lsb`, the function `BitVec.concat` appends `lsb` as the least significant bit to `msbs`, resulting in a new bitvector of width `n + 1`. More formally, for a bitvector `msbs : BitVec n` and a Boolean `lsb`, the concatenation `BitVec.concat msbs lsb` is defined as `msbs ++ (BitVec.ofBool lsb)`, where `++` denotes bitvector concatenation and `BitVec.ofBool lsb` converts `lsb` to a bitvector of width 1.

BitVec.shiftConcat definition

(x : BitVec n) (b : Bool) : BitVec n

Full source

/--
Shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.

This is a non-dependent version of `BitVec.concat` that does not change the total bitwidth.
-/
def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
  (x.concat b).truncate n

Bitvector shift-and-concatenate operation

Informal description

Given a bitvector $ x $ of width $ n $ and a Boolean value $ b $, the function shifts all bits of $ x $ to the left by 1 and sets the least significant bit to $ b $, while maintaining the original width $ n $. This is equivalent to concatenating $ b $ to $ x $ and then truncating the result to width $ n $. More formally, for $ x : \text{BitVec} \, n $ and $ b : \text{Bool} $, the operation is defined as: \[ \text{shiftConcat} \, x \, b = \text{truncate} \, (\text{concat} \, x \, b) \, n \]

BitVec.cons definition

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

Full source

/--
Prepends a single bit to the front of a bitvector, using big-endian order (see `append`).

The new bit is the most significant bit.
-/
def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
  ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)

Bitvector cons operation (prepend a bit)

Informal description

Given a Boolean value `msb` (most significant bit) and a bitvector `lsbs` of width `n`, the function constructs a new bitvector of width `n + 1` by prepending `msb` to `lsbs`. The resulting bitvector has `msb` as its most significant bit and `lsbs` as the remaining bits.

BitVec.append_ofBool theorem

(msbs : BitVec w) (lsb : Bool) : msbs ++ ofBool lsb = concat msbs lsb

Full source

theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
    msbs ++ ofBool lsb = concat msbs lsb :=
  rfl

Concatenation of Bitvector with Boolean via `ofBool` Equals `concat` Operation

Informal description

For any bitvector `msbs` of width `w` and any Boolean value `lsb`, the concatenation of `msbs` with the bitvector representation of `lsb` (of width 1) is equal to the result of the `concat` operation applied to `msbs` and `lsb`. In symbols: $\text{msbs} \mathbin{+\!\!+} \text{ofBool}(\text{lsb}) = \text{concat}(\text{msbs}, \text{lsb})$, where $\mathbin{+\!\!+}$ denotes bitvector concatenation and $\text{ofBool}(\text{lsb})$ converts `lsb` to a bitvector of width 1.

BitVec.ofBool_append theorem

(msb : Bool) (lsbs : BitVec w) : ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..)

Full source

theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
    ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
  rfl

Concatenation of Single-Bit Bitvector with Another Bitvector Equals Prepend Operation

Informal description

For any Boolean value $msb$ and bitvector $lsbs$ of width $w$, the concatenation of the bitvector representation of $msb$ (of width 1) with $lsbs$ is equal to the bitvector obtained by prepending $msb$ to $lsbs$ (resulting in a bitvector of width $w + 1$), after casting to account for the commutativity of addition on natural numbers.

BitVec.twoPow definition

(w : Nat) (i : Nat) : BitVec w

Full source

/--
`twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise. In other words, it is 2 to the
power `i`.

From the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
-/
def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w1#w <<< i

Bitvector representation of `2^i` (with zero padding)

Informal description

The function `twoPow w i` returns a bitvector of width `w` representing the value `2^i` if `i < w`, and `0` otherwise. In bitwise terms, the result has the `i`-th bit set to `1` and all other bits set to `0`.

BitVec.hash definition

(bv : BitVec n) : UInt64

Full source

/--
Computes a hash of a bitvector, combining 64-bit words using `mixHash`.
-/
def hash (bv : BitVec n) : UInt64 :=
  if n ≤ 64 then
    bv.toFin.val.toUInt64
  else
    mixHash (bv.toFin.val.toUInt64) (hash ((bv >>> 64).setWidth (n - 64)))

Hash function for bitvectors

Informal description

The function computes a hash value for a bitvector `bv` of width `n`. If the bitvector width is at most 64 bits, it directly converts the bitvector to a 64-bit unsigned integer. For wider bitvectors, it combines the hash of the lower 64 bits with the hash of the remaining bits (shifted right by 64 positions) using the `mixHash` function.

BitVec.instHashable instance

: Hashable (BitVec n)

Full source

instance : Hashable (BitVec n) where
  hash := hash

Bitvectors are Hashable

Informal description

For any bitvector of width $n$, there is a canonical hashable structure defined on it.

BitVec.append_eq theorem

(x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y

Full source

@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl

Concatenation Equivalence: $\text{append}(x, y) = x \mathbin{+\!\!+} y$

Informal description

For any bitvector $x$ of width $w$ and any bitvector $y$ of width $v$, the concatenation of $x$ and $y$ via `BitVec.append` is equal to the result of the heterogeneous append operation $x \mathbin{+\!\!+} y$, producing a bitvector of width $w + v$.

BitVec.shiftLeft_eq theorem

(x : BitVec w) (n : Nat) : BitVec.shiftLeft x n = x <<< n

Full source

@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl

Left Shift Operation Equivalence: $\text{shiftLeft}(x, n) = x \lll n$

Informal description

For any bitvector $x$ of width $w$ and any natural number $n$, the left shift operation `BitVec.shiftLeft x n` is equal to the bitvector notation $x \lll n$.

BitVec.ushiftRight_eq theorem

(x : BitVec w) (n : Nat) : BitVec.ushiftRight x n = x >>> n

Full source

@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl

Logical Right Shift Equivalence: $\text{ushiftRight}(x, n) = x \gg\gg n$

Informal description

For any bitvector $x$ of width $w$ and any natural number $n$, the logical right shift operation `BitVec.ushiftRight` applied to $x$ and $n$ is equal to the notation $x \gg\gg n$.

BitVec.not_eq theorem

(x : BitVec w) : BitVec.not x = ~~~x

Full source

@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl

Bitwise Complement Equivalence: $\text{BitVec.not}\,x = \sim x$

Informal description

For any bitvector $x$ of width $w$, the bitwise complement operation $\text{BitVec.not}\,x$ is equal to the bitwise negation notation $\sim x$.

BitVec.and_eq theorem

(x y : BitVec w) : BitVec.and x y = x &&& y

Full source

@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl

Bitwise AND Operation Equality for Bitvectors

Informal description

For any two bitvectors $x$ and $y$ of width $w$, the bitwise AND operation `BitVec.and x y` is equal to the bitwise AND operation written as $x \mathbin{\&\&\&} y$.

BitVec.or_eq theorem

(x y : BitVec w) : BitVec.or x y = x ||| y

Full source

@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl

Bitwise OR Operation Equality: $\text{BitVec.or}(x, y) = x \mathbin{|||} y$

Informal description

For any bitvectors $x$ and $y$ of width $w$, the bitwise OR operation `BitVec.or x y` is equal to $x \mathbin{|||} y$, where $\mathbin{|||}$ denotes the bitwise OR operation on bitvectors.

BitVec.xor_eq theorem

(x y : BitVec w) : BitVec.xor x y = x ^^^ y

Full source

@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl

Bitwise XOR Operation Equivalence: $\text{BitVec.xor}\,x\,y = x \ ^\wedge\ y$

Informal description

For any two bitvectors $x$ and $y$ of width $w$, the bitwise XOR operation `BitVec.xor x y` is equal to the infix XOR operation $x \ ^\wedge\ y$.

BitVec.neg_eq theorem

(x : BitVec w) : BitVec.neg x = -x

Full source

@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl

Bitvector Negation Equals Arithmetic Negation Modulo $2^w$

Informal description

For any bitvector $x$ of width $w$, the negation operation `BitVec.neg x` is equal to the arithmetic negation $-x$ modulo $2^w$.

BitVec.add_eq theorem

(x y : BitVec w) : BitVec.add x y = x + y

Full source

@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl

Bitvector Addition Equivalence: $\text{BitVec.add}(x, y) = x + y \mod 2^w$

Informal description

For any bitvectors $x$ and $y$ of width $w$, the bitvector addition operation `BitVec.add` is equivalent to the standard addition operation $x + y$ modulo $2^w$.

BitVec.sub_eq theorem

(x y : BitVec w) : BitVec.sub x y = x - y

Full source

@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl

Bitvector Subtraction Equivalence: $\text{BitVec.sub}(x, y) = x - y \mod 2^w$

Informal description

For any bitvectors $x$ and $y$ of width $w$, the result of the bitvector subtraction operation `BitVec.sub x y` is equal to $x - y$ modulo $2^w$.

BitVec.mul_eq theorem

(x y : BitVec w) : BitVec.mul x y = x * y

Full source

@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl

Bitvector Multiplication Equivalence: $\text{BitVec.mul}\,x\,y = x * y$

Informal description

For any bitvectors $x$ and $y$ of width $w$, the bitvector multiplication operation $\text{BitVec.mul}\,x\,y$ is equal to the product $x * y$ interpreted modulo $2^w$.

BitVec.udiv_eq theorem

(x y : BitVec w) : BitVec.udiv x y = x / y

Full source

@[simp] theorem udiv_eq (x y : BitVec w)                  : BitVec.udiv x y = x / y           := rfl

Equivalence of Unsigned Division and Bitvector Division: $\text{udiv}(x, y) = x / y$

Informal description

For any bitvectors $x$ and $y$ of width $w$, the unsigned division operation $\text{udiv}(x, y)$ is equal to the division operation $x / y$ on bitvectors.

BitVec.umod_eq theorem

(x y : BitVec w) : BitVec.umod x y = x % y

Full source

@[simp] theorem umod_eq (x y : BitVec w)                  : BitVec.umod x y = x % y           := rfl

Equality of Bitvector Unsigned Modulo and Natural Number Modulo

Informal description

For any bitvectors $x$ and $y$ of width $w$, the unsigned modulo operation $\text{umod}(x, y)$ is equal to $x \bmod y$, where both operations are interpreted as unsigned integer operations.

BitVec.zero_eq theorem

: BitVec.zero n = 0#n

Full source

@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl

Zero Bitvector Equality: $\text{zero}_n = 0\#n$

Informal description

For any bitvector width $n$, the zero bitvector of width $n$ is equal to the bitvector literal `0#n` (which represents a bitvector of width $n$ with all bits set to 0).

BitVec.ofBoolListBE definition

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

Full source

/-- Converts a list of `Bool`s into a big-endian `BitVec`. -/
def ofBoolListBE : (bs : List Bool) → BitVec bs.length
| [] => 0#0
| b :: bs => cons b (ofBoolListBE bs)

Big-endian bitvector from Boolean list

Informal description

The function converts a list of Booleans `bs` into a big-endian bitvector of width equal to the length of the list. The most significant bit is the head of the list, and the least significant bits are constructed recursively from the tail of the list. An empty list results in a zero-width bitvector.

BitVec.ofBoolListLE definition

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

Full source

/-- Converts a list of `Bool`s into a little-endian `BitVec`. -/
def ofBoolListLE : (bs : List Bool) → BitVec bs.length
| [] => 0#0
| b :: bs => concat (ofBoolListLE bs) b

Little-endian bitvector from Boolean list

Informal description

The function converts a list of Booleans `bs` into a little-endian bitvector of width `bs.length`. The least significant bit (LSB) is the first element of the list, and the most significant bit (MSB) is the last element. The empty list is converted to a bitvector of width 0. More formally, for a list `bs = [b₀, b₁, ..., b_{n-1}]`, the resulting bitvector has value `∑_{i=0}^{n-1} b_i * 2^i`.

BitVec.uaddOverflow definition

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

Full source

/--
Checks whether addition of `x` and `y` results in *unsigned* overflow.

SMT-LIB name: `bvuaddo`.
-/
def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w

Unsigned addition overflow check for bitvectors

Informal description

Given two bitvectors $ x $ and $ y $ of width $ w $, the function checks whether their natural number sum $ x + y $ is greater than or equal to $ 2^w $, indicating unsigned overflow.

BitVec.saddOverflow definition

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

Full source

/--
Checks whether addition of `x` and `y` results in *signed* overflow, treating `x` and `y` as 2's
complement signed bitvectors.

SMT-LIB name: `bvsaddo`.
-/
def saddOverflow {w : Nat} (x y : BitVec w) : Bool :=
  (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))

Signed addition overflow check for bitvectors

Informal description

Given two bitvectors $ x $ and $ y $ of width $ w $, the function checks whether their two's complement signed addition $ x + y $ results in overflow. Specifically, it returns `true` if either: - The sum $ x + y $ is greater than or equal to $ 2^{w-1} $ (positive overflow), or - The sum $ x + y $ is less than $ -2^{w-1} $ (negative overflow). This corresponds to the SMT-LIB operation `bvsaddo`.

BitVec.usubOverflow definition

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

Full source

/--
Checks whether subtraction of `x` and `y` results in *unsigned* overflow.

SMT-Lib name: `bvusubo`.
-/
def usubOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat < y.toNat

Unsigned subtraction overflow check for bitvectors

Informal description

Given two bitvectors $ x $ and $ y $ of width $ w $, the function checks whether the subtraction $ x - y $ results in unsigned overflow. This occurs when the natural number representation of $ x $ is less than that of $ y $, i.e., $ \text{toNat}(x) < \text{toNat}(y) $.

BitVec.ssubOverflow definition

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

Full source

/--
Checks whether the subtraction of `x` and `y` results in *signed* overflow, treating `x` and `y` as
2's complement signed bitvectors.

SMT-Lib name: `bvssubo`.
-/
def ssubOverflow {w : Nat} (x y : BitVec w) : Bool :=
  (x.toInt - y.toInt ≥ 2 ^ (w - 1)) || (x.toInt - y.toInt < - 2 ^ (w - 1))

Signed subtraction overflow check for bitvectors

Informal description

Given two bitvectors $ x $ and $ y $ of width $ w $, the function checks whether the subtraction $ x - y $ results in *signed* overflow when interpreted as two's complement signed integers. Specifically, it returns `true` if the result $ x - y $ is either greater than or equal to $ 2^{w-1} $ or less than $ -2^{w-1} $, indicating that the result cannot be represented as a signed $ w $-bit integer.

BitVec.negOverflow definition

{w : Nat} (x : BitVec w) : Bool

Full source

/--
Checks whether the negation of a bitvector results in overflow.

For a bitvector `x` with nonzero width, this only happens if `x = intMin`.

SMT-Lib name: `bvnego`.
-/
def negOverflow {w : Nat} (x : BitVec w) : Bool :=
  x.toInt == - 2 ^ (w - 1)

Two's complement negation overflow check for bitvectors

Informal description

For a bitvector $ x $ of width $ w $, the function checks whether the negation of $ x $ results in overflow. This occurs precisely when $ x $ represents the minimum value in two's complement representation, i.e., when $ x $ interpreted as a signed integer equals $-2^{w-1}$.

BitVec.reverse definition

: {w : Nat} → BitVec w → BitVec w

Full source

/-- Reverses the bits in a bitvector. -/
def reverse : {w : Nat} → BitVec w → BitVec w
  | 0, x => x
  | w + 1, x => concat (reverse (x.truncate w)) (x.msb)

Bitvector bit reversal

Informal description

The function reverses the bits in a bitvector of width $ w $. For a bitvector $ x $ of width $ w + 1 $, the reversed bitvector is constructed by concatenating the reversed version of the $ w $ least significant bits of $ x $ with the most significant bit of $ x $. The base case for width $ 0 $ returns the input bitvector unchanged. More precisely, for a bitvector $ x $ of width $ w + 1 $, the operation is defined recursively as: \[ \text{reverse}(x) = \text{concat}(\text{reverse}(\text{truncate}(x, w)), \text{msb}(x)) \] where: - $\text{truncate}(x, w)$ extracts the $ w $ least significant bits of $ x $, - $\text{msb}(x)$ is the most significant bit of $ x $, - $\text{concat}$ appends the most significant bit to the reversed truncated bits. For the base case $ w = 0 $, the function returns $ x $ directly since there are no bits to reverse.