Init.Data.BitVec.BasicAux

BitVec.ofNat definition

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

Full source

/--
The bitvector with value `i mod 2^n`.
-/
@[match_pattern]
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
  toFin := Fin.ofNat' (2^n) i

Bitvector from natural number modulo $ 2^n $

Informal description

The function constructs a bitvector of width $ n $ from a natural number $ i $, where the value is $ i \mod 2^n $. The result is represented as an element of the finite type $ \text{Fin } 2^n $.

BitVec.instOfNat instance

: OfNat (BitVec n) i

Full source

instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i

Numeric Literal Interpretation for Bitvectors

Informal description

For any bitvector width $n$ and natural number $i$, the bitvector type $\text{BitVec}\,n$ can interpret numeric literals via the $\text{OfNat}$ instance, where the value is taken modulo $2^n$.

BitVec.isLt theorem

(x : BitVec w) : x.toNat < 2 ^ w

Full source

/-- Return the bound in terms of toNat. -/
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt

Bitvector Natural Representation Bounded by $2^w$

Informal description

For any bitvector $x$ of width $w$, the natural number representation of $x$ is strictly less than $2^w$, i.e., $\text{toNat}(x) < 2^w$.

BitVec.add definition

(x y : BitVec n) : BitVec n

Full source

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

SMT-LIB name: `bvadd`.
-/
protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)

Bitvector addition modulo $ 2^n $

Informal description

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

BitVec.instAdd instance

: Add (BitVec n)

Full source

instance : Add (BitVec n) := ⟨BitVec.add⟩

Addition Operation on Bitvectors

Informal description

For any natural number $n$, the type of bitvectors of width $n$ has an addition operation defined as addition modulo $2^n$.

BitVec.sub definition

(x y : BitVec n) : BitVec n

Full source

/--
Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo `2^n`. Usually accessed via the `-` operator.

-/
protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)

Bitvector subtraction modulo $2^n$

Informal description

The function subtracts two bitvectors $x$ and $y$ of width $n$, returning a bitvector of the same width. The subtraction is performed modulo $2^n$ as $(2^n - y) + x \mod 2^n$, which can be interpreted equivalently as either signed or unsigned subtraction. This operation is typically accessed via the `-` operator.

BitVec.instSub instance

: Sub (BitVec n)

Full source

instance : Sub (BitVec n) := ⟨BitVec.sub⟩

Subtraction Operation on Bitvectors

Informal description

For any natural number $n$, the type of bitvectors of width $n$ is equipped with a subtraction operation that computes the difference modulo $2^n$.