指定宽度的位向量。
这在运行时和内核中都表示为底层的 Nat 数字，继承了对 Nat 的所有特殊支持。
构造子
BitVec.ofFin
20.5. 位向量
位向量是固定宽度的二进制数字序列。 它们经常用于软件验证，因为它们能贴切地建模与硬件相似的高效数据结构和操作。 位向量可以从两个角度来理解：既可视为位的序列，也可视为由位序列编码的数。 当位向量表示一个数时，它既可以表示有符号数，也可以表示无符号数。 有符号数采用二进制补码形式表示。
20.5.1. 逻辑模型
位向量表示为对具有适当界限的 Fin 的包装。
由于 Fin 本身是对 Nat 的包装，位向量能够利用内核对自然数高效计算的特殊支持。
20.5.2. 运行时表示
位向量表示为具有相应范围的 Fin。
由于 BitVec 是对 Fin 的平凡包装，而 Fin 又是对 Nat 的平凡包装，因此在编译后的代码中，位向量与 Nat 使用相同的运行时表示。
20.5.3. 语法
实例 OfNat (BitVec w) n 对所有宽度 w 和自然数 n 都存在。
在预期类型已知的上下文中，可以使用自然数文本——包括十六进制或二进制记法——来表示位向量。
当预期类型未知时，可以使用专用语法同时指定该位向量的宽度和值。
位向量的数值文本
语法固定宽度位向量文本
term ::= ...
|
此记法将数值文本与表示其宽度的项配对。
# 两侧禁止出现空格。
超出位向量宽度的文本将被截断。
固定宽度位向量文本
语法有界位向量文本
term ::= ...
|
此记法仅在打开 BitVec 命名空间后可用。
它不要求显式给出宽度，而是要求提供一个证明，表明文本值可由相应宽度的位向量表示。
20.5.4. 自动化
除了 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,
Jr. 所著 Hacker's Delight, Second Edition 第 82 页的图 5-2 描述了 popcount 的另一种实现。
它使用底层位运算，以少得多的操作计算出相同的值：
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! 🐙
20.5.5. API 参考
20.5.5.1. 界限
20.5.5.2. 构造
定义
用 w 个位 b 填充位向量。
定义
twoPow w i 是位向量 2^i 如果 i < w，否则是 0。换句话说，它是 2 的 i 次方。
从按位的角度来看，它的第i位是1，所有其他位都是0。
20.5.5.3. 转换
定义
将位向量转换为固定宽度的十六进制数字，具有足够的数字来表示它。
如果 n 是 0，则返回一个数字。否则，返回 ⌊(n + 3) / 4⌋ 个数字。
定义
将位向量解释为以二进制补码形式存储的整数。
定义
定义
定义
定义
将整数转换为给定宽度 n 的二进制补码位向量，并按需上溢或下溢。
底层 Nat 为 (2^n + (i mod 2^n)) mod 2^n。将位向量转回 Int 时，使用 BitVec.toInt 所得值为 i.bmod (2^n)。
定义
值为 i mod 2^n 的位向量。
标识符中的记号约定：
-
在标识符中推荐的
0#n拼写是zero（而不是ofNat_zero）。 -
在标识符中推荐的
1#n拼写是one（而不是ofNat_one）。
定义
如果两个自然数 n 和 m 相等，那么宽度为 n 的位向量也是宽度为 m 的位向量。
应该优先使用 x.cast eq 而不是 eq ▸ x，因为有专用的 simp 引理可以更一致地简化 BitVec.cast。
20.5.5.4. 比较
定义
位向量的无符号小于或等于。
SMT-LIB 名称：bvule。
定义
针对位向量的有符号小于或等于。
SMT-LIB 名称: bvsle。
定义
位向量的无符号小于。
SMT-LIB 名称：bvult。
定义
20.5.5.5. 哈希
20.5.5.6. 序列操作
这些操作将位向量视为位的序列，而非数的编码。
定义
在位向量的前面添加一个比特，使用大端序（参见 append）。
新位是最高有效位。
定义
将一个单独的比特附加到位向量的末尾，使用大端顺序（参见 append）。也就是说，新的比特是最低有效位。
定义
将长度为 w 的位向量转换为长度为 v 的位向量，并根据需要使用 0 进行填充。
具体行为取决于起始宽度 w 与最终宽度之间的关系
v:
-
如果
v > w，则进行零扩展；高位用零填充，直到位向量达到v位。 -
如果
v = w，位向量将保持不变返回。 -
如果
v < w，高位将被截断。
BitVec.setWidth、BitVec.zeroExtend 和 BitVec.truncate 是此操作的别名。
SMT-LIB 名称: zero_extend。
定义
将长度为 w 的位向量转换为长度为 v 的位向量，并根据需要使用 0 进行填充。
具体行为取决于起始宽度 w 与最终宽度之间的关系
v:
-
如果
v > w，则进行零扩展；高位用零填充，直到位向量达到v位。 -
如果
v = w，位向量将保持不变返回。 -
如果
v < w，高位将被截断。
BitVec.setWidth、BitVec.zeroExtend 和 BitVec.truncate 是此操作的别名。
SMT-LIB 名称: zero_extend。
定义
使用“大端”约定连接两个位向量，即更高有效位的输入在左侧。通常通过 ++ 运算符访问。
SMT-LIB 名称：concat。
示例：
-
0xAB#8 ++ 0xCD#8 = 0xABCD#16。
定义
连接 i 个 x，得到长度为 w * i 的新向量。
定义
反转位向量中的比特位。
定义
将位向量中的位向左旋转。
x 的所有位都被移到更高的位置，最上面的 n 位会回绕以填充腾出的低位。
SMT-LIB 名称：rotate_left，不过该运算符使用 Nat 位移量。
示例：
-
(0b0011#4).rotateLeft 3 = 0b1001
定义
将位向量中的位向右旋转。
x 的所有位都被移到较低的位置，底部的 n 位会环绕以填充腾出的高位。
SMT-LIB 名称：rotate_right，不过该运算符使用 Nat 位移量。
示例：
-
rotateRight 0b01001#5 1 = 0b10100
20.5.5.6.1. 位提取
定义
返回第i个最重要的位。
定义
返回第i个最低有效位。
定义
从位向量中提取从 hi 到 lo（包括两者）的位，如果有必要，会隐式地进行零扩展。
生成的位向量大小为 hi - lo + 1。
SMT-LIB 名称：extract。
定义
提取第 start 位到第 start + len - 1 位，来源是大小为 n 的位向量，并得到大小为 len 的新位向量。如果 start + len > n，则对位向量进行零扩展。
20.5.5.7. 位运算符
这些运算符修改一个或多个位向量中的各个位。
定义
位向量的按位与。通常通过 &&& 运算符访问。
SMT-LIB 名称：bvand。
示例：
-
0b1010#4 &&& 0b0110#4 = 0b0010#4
定义
位向量的按位或。通常通过 ||| 运算符访问。
SMT-LIB 名称：bvor。
示例：
-
0b1010#4 ||| 0b0110#4 = 0b1110#4
定义
位向量的按位取反。通常通过 ~~~ 前缀运算符访问。
SMT-LIB 名称: bvnot。
示例：
-
~~~(0b0101#4) == 0b1010
定义
位向量的按位异或。通常通过 ^^^ 操作符访问。
SMT-LIB 名称：bvxor。
示例：
-
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
定义
将长度为 w 的位向量转换为长度为 v 的位向量，并根据需要使用 0 进行填充。
具体行为取决于起始宽度 w 与最终宽度之间的关系
v:
-
如果
v > w，则进行零扩展；高位用零填充，直到位向量达到v位。 -
如果
v = w，位向量将保持不变返回。 -
如果
v < w，高位将被截断。
BitVec.setWidth、BitVec.zeroExtend 和 BitVec.truncate 是此操作的别名。
SMT-LIB 名称: zero_extend。
定义
将长度为 w 的位向量转换为长度为 v 的位向量，并根据需要使用最高有效位的值进行填充。
如果x是一个空位向量，则符号被视为零。
SMT-LIB 名称：sign_extend。
定义
定义
定义
20.5.5.8. 算术
这些运算符将位向量视为数。 有些操作按有符号方式进行，另一些则按无符号方式进行。 由于位向量被解释为二进制补码数，因此加法、减法和乘法在有符号与无符号解释下是一致的。
定义
将两个位向量相加。这可以解释为带符号或无符号加法，模 2^n。
通常通过 + 运算符访问。
SMT-LIB 名称：bvadd。
定义
将一个位向量从另一个位向量中减去。这可以解释为有符号或无符号的减法，模 2^n。通常通过 - 运算符访问。
定义
将两个位向量相乘。这可以解释为有符号或无符号乘法，模 2^n。通常通过*运算符访问。
SMT-LIB 名称：bvmul。
20.5.5.8.1. 无符号操作
定义
使用 Lean 约定的位向量无符号除法，其中除以零返回零。通常通过 / 操作符访问。
定义
位向量的无符号取模。通常通过 % 操作符访问。
SMT-LIB 名称：bvurem。
定义
检查x和y的相加是否导致无符号溢出。
SMT-LIB 名称：bvuaddo。
定义
检查 x 和 y 的减法是否导致无符号溢出。
SMT-Lib 名称：bvusubo。
20.5.5.8.2. 有符号操作
定义
返回有符号位向量的绝对值。
定义
位向量的取反。这可以解释为模 2^n 的有符号或无符号取反。
通常通过 - 前缀运算符访问。
SMT-LIB 名称：bvneg。
定义
定义
使用 SMT-LIB 对位向量进行有符号除法，使用 SMT-LIB 约定，其中除以零返回 BitVector.allOnes n。
具体来说，x.smtSDiv 0 = if x >= 0 then -1 else 1
SMT-LIB 名称：bvsdiv。
定义
有符号除法的余数向负无穷舍入。
SMT-LIB 名称：bvsmod。
定义
带符号除法取零舍入的余数。
SMT-LIB 名称：bvsrem。
定义
检查将 x 和 y 相加是否导致有符号溢出，将 x 和 y 视为二进制补码有符号位向量。
SMT-LIB 名称：bvsaddo。
定义
检查 x 与 y 相减是否会导致有符号溢出，将 x 和 y 视为二进制补码有符号位向量。
SMT-Lib 名称：bvssubo。
20.5.5.9. 迭代
定义
使用函数 f 为每一位迭代计算状态，并从初始状态 s 开始，从而构造位向量。每一步都把前一状态和当前位索引传给 f，由它生成一个位以及下一状态。这些位随后组合成最终的位向量。
它生成状态序列 [s_0, s_1 .. s_w] 和位向量 v，其中 f i s_i = (s_{i+1}, b_i)，并且 b_i 表示第 i 个最低有效位，它位于 v 中（例如 getLsb v i = b_i）。
定理 iunfoldr_replace 可将 BitVec.iunfoldr 的使用替换为更便于推理的声明式规范。
定理
给定一个函数 state，它为每一个潜在的迭代次数提供正确的状态，以及一个从正确初始状态计算这些状态的函数，将 BitVec.iunfoldr f 应用于初始状态的结果就是与位向量宽度对应的状态，配对着由每个计算得出的比特组成的位向量。
这个定理可以用来证明使用 BitVec.iunfoldr 定义的函数的性质。
20.5.5.10. 证明自动化
20.5.5.10.1. 位爆破
标准库包含许多有助于实现位爆破的辅助实现；位爆破是 bv_decide 用来将命题编码为供外部求解器处理的布尔可满足性问题的技术。
定义
通过连锁进位加法器实现的按位加法。
定义
如果第 i 个进位在计算 x + y + c 时为真，则 carry i x y c 返回 true。
定义
一个描述乘法为重复加法的递推关系。
这个函数对于位爆炸乘法很有用。
定义
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
用于位爆炸的除法递归定义，以移位-减法电路为基础。
定义
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
除法算法的一个回合。它尝试执行减位移操作。
这应仅在 r.msb = false 时调用，因此不会溢出。
定义
将 x 左移前 n 位的 y 所表示的位数。
定理 BitVec.shiftLeft_eq_shiftLeftRec 证明 (x <<< y) 与 BitVec.shiftLeftRec x y 等价。
结合方程 BitVec.shiftLeftRec_zero 和 BitVec.shiftLeftRec_succ，可将 BitVec.shiftLeft 展开为用于位级展开的电路。
定义
将 x 以算术（有符号）方式右移前 n 位的 y 所表示的位数。
定理 BitVec.sshiftRight_eq_sshiftRightRec 证明 (x.sshiftRight y) 与 BitVec.sshiftRightRec x y 等价。结合方程 BitVec.sshiftRightRec_zero 和 BitVec.sshiftRightRec_succ，可将 BitVec.sshiftRight 展开为用于位级展开的电路。
定义
将 x 以逻辑方式右移前 n 位的 y 所表示的位数。
定理 BitVec.shiftRight_eq_ushiftRightRec 证明 (x >>> y) 与 BitVec.ushiftRightRec 等价。
结合方程 BitVec.ushiftRightRec_zero 和 BitVec.ushiftRightRec_succ，可将 BitVec.ushiftRight 展开为用于位级展开的电路。