位向量是固定宽度的二进制数字序列。 它们经常用于软件验证，因为它们紧密地模拟了与硬件类似的高效数据结构和操作。 位向量可以从两个角度理解：作为位序列，或者作为由位序列编码的数字。 当位向量表示数字时，它可以作为有符号数或无符号数。 有符号数以二进制补码形式表示。
位向量表示为具有适当界限的 Fin 的包装器。
由于 Fin 本身是 Nat 的包装器，因此位向量能够使用内核的特殊支持来通过自然数进行高效计算。
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.
BitVec.ofFin
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.
位向量表示为具有相应范围的 Fin。
由于 BitVec 是 Fin 周围的 简单包装器，而 Fin 是 Nat 周围的简单包装器，因此位向量在编译代码中使用与 Nat 相同的运行时表示形式。
所有宽度 w 和自然数n 都有一个 OfNat (BitVec w) n 实例。
自然数文字（包括使用十六进制或二进制表示法的文字）可用于在已知预期类型的上下文中表示位向量。
当预期类型未知时，专用语法允许指定位向量的宽度及其值。
term ::= ...
| Notation for bitvector 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`).
该表示法将数字文字与表示其宽度的术语配对。
# 周围禁止有空格。
超出位向量宽度的文字将被截断。
term ::= ...
| Notation for bitvector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`.
仅当 BitVec 命名空间已打开时，此表示法才可用。
它不需要显式宽度，而是需要证明文字值可以由相应宽度的位向量表示。
除了 Lean 为每种类型提供的全套自动化和工具之外，bv_decide策略还可以解决许多与位向量相关的问题。
该策略调用外部自动 定理证明器 (cadical) 并重建它在 Lean 自己的逻辑中提供的证明。
由此产生的证明仅依赖于公理 Lean.ofReduceBool；外部证明者不是可信代码库的一部分。
函数 popcount 返回位向量中设置的位数。
它可以实现为一个 32 次迭代循环来测试每个位，如果该位被设置则递增计数器：
def popcount_spec (x : BitVec 32) : BitVec 32 :=
(32 : Nat).fold (init := 0) fun i _ pop =>
pop + ((x >>> i) &&& 1)
Henry S. Warren 的《黑客之乐》第二版中描述了 popcount 的替代实现，
第 5-2 页中的 Jr. 82.
它使用低级按位运算以更少的运算来计算相同的值：
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
使用 bv_decide 可以证明这两种实现是等效的：
theorem popcount_correct : popcount = popcount_spec := ⊢ popcount = popcount_spec
x:BitVec 32⊢ popcount x = popcount_spec x
x: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)
All goals completed! 🐙
The bitvector of width w that has the largest value when interpreted as an integer.
The bitvector of width w that has the smallest value when interpreted as an integer.
Fills a bitvector with w copies of the bit b.
Returns a bitvector of size n where all bits are 0.
Returns a bitvector of size n where all bits are 1.
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 ith bit as 1 and all other bits as 0.
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.
Interprets the bitvector as an integer stored in two's complement form.
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).
The bitvector 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).
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.
Unsigned less-than-or-equal-to for bitvectors.
SMT-LIB name: bvule.
Signed less-than-or-equal-to for bitvectors.
SMT-LIB name: bvsle.
Unsigned less-than for bitvectors.
SMT-LIB name: bvult.
Signed less-than for bitvectors.
SMT-LIB name: bvslt.
Examples:
BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false
这些操作将位向量视为位序列，而不是数字编码。
Prepends a single bit to the front of a bitvector, using big-endian order (see append).
The new bit is the most significant bit.
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.
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.
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.
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.
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.
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.
Concatenates i copies of x into a new vector of length w * i.
Reverses the bits in a bitvector.
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
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
Returns the most significant bit in a bitvector.
Returns the ith most significant bit.
Returns the ith least significant bit.
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.
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.
这些运算符修改一个或多个位向量的各个位。
Bitwise and for bitvectors. Usually accessed via the &&& operator.
SMT-LIB name: bvand.
Example:
0b1010#4 &&& 0b0110#4 = 0b0010#4
Bitwise or for bitvectors. Usually accessed via the ||| operator.
SMT-LIB name: bvor.
Example:
0b1010#4 ||| 0b0110#4 = 0b1110#4
Bitwise complement for bitvectors. Usually accessed via the ~~~ prefix operator.
SMT-LIB name: bvnot.
Example:
~~~(0b0101#4) == 0b1010
Bitwise xor for bitvectors. Usually accessed via the ^^^ operator.
SMT-LIB name: bvxor.
Example:
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
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.
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.
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.
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.
这些运算符将位向量视为数字。 有些操作是有符号的，而另一些则没有符号。 因为位向量被理解为二进制补码，所以加法、减法和乘法对于有符号和无符号解释是一致的。
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.
Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo 2^n. Usually accessed via the - operator.
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.
Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the / operator.
Unsigned division of bitvectors using the
SMT-LIB convention,
where division by zero returns BitVector.allOnes n.
SMT-LIB name: bvudiv.
Unsigned modulo for bitvectors. Usually accessed via the % operator.
SMT-LIB name: bvurem.
Checks whether addition of x and y results in unsigned overflow.
SMT-LIB name: bvuaddo.
Checks whether subtraction of x and y results in unsigned overflow.
SMT-Lib name: bvusubo.
Returns the absolute value of a signed bitvector.
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.
Signed division for bitvectors using the SMT-LIB using the
SMT-LIB convention,
where division by zero returns BitVector.allOnes n.
Specifically, x.smtSDiv 0 = if x >= 0 then -1 else 1
SMT-LIB name: bvsdiv.
Remainder for signed division rounded to negative infinity.
SMT-LIB name: bvsmod.
Remainder for signed division rounding to zero.
SMT-LIB name: bvsrem.
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.
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.
Constructs a bitvector by iteratively computing a state for each bit using the function f,
starting with the initial state s. At each step, the prior state and the current bit index are
passed to f, and it produces a bit along with the next state value. These bits are assembled into
the final bitvector.
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).
The theorem iunfoldr_replace allows uses of BitVec.iunfoldr to be replaced with declarative
specifications that are easier to reason about.
Given a function state that provides the correct state for every potential iteration count and a
function that computes these states from the correct initial state, the result of applying
BitVec.iunfoldr f to the initial state is the state corresponding to the bitvector's width paired
with the bitvector that consists of each computed bit.
This theorem can be used to prove properties of functions that are defined using BitVec.iunfoldr.
标准库包含许多有助于实现位爆破的帮助器实现，这是 bv_decide 用于将命题编码为外部求解器的布尔可满足性问题的技术。
Bitwise addition implemented via a ripple carry adder.
Carry function for bitwise addition.
carry i x y c returns true if the i carry bit is true when computing x + y + c.
A recurrence that describes multiplication as repeated addition.
This function is useful for bit blasting multiplication.
BitVec.divRec {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState wBitVec.divRec {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState w
A recursive definition of division for bit blasting, in terms of a shift-subtraction circuit.
BitVec.divSubtractShift {w : Nat} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState wBitVec.divSubtractShift {w : Nat} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState w
One round of the division algorithm. It tries to perform a subtract shift.
This should only be called when r.msb = false, so it will not overflow.
Shifts x to the left by the first n bits of y.
The theorem BitVec.shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and
BitVec.shiftLeftRec x y.
Together with equations BitVec.shiftLeftRec_zero and BitVec.shiftLeftRec_succ, this allows
BitVec.shiftLeft to be unfolded into a circuit for bit blasting.
Shifts x arithmetically (signed) to the right by the first n bits of y.
The theorem BitVec.sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and
BitVec.sshiftRightRec x y. Together with equations BitVec.sshiftRightRec_zero, and
BitVec.sshiftRightRec_succ, this allows BitVec.sshiftRight to be unfolded into a circuit for
bit blasting.
Shifts x logically to the right by the first n bits of y.
The theorem BitVec.shiftRight_eq_ushiftRightRec proves the equivalence
of (x >>> y) and BitVec.ushiftRightRec.
Together with equations BitVec.ushiftRightRec_zero and BitVec.ushiftRightRec_succ,
this allows BitVec.ushiftRight to be unfolded into a circuit for bit blasting.