NyaOJ

题目描述

我们研究计算机系统中两个整数减法运算的底层二进制实现机制。以 $121 - 35 = 86$ 为例：

被减数 121 的二进制表示：0111 1001
减数 35 的二进制表示：0010 0011
结果 86 的二进制表示：0101 0110

观察发现，该减法在第 1 位和第 2 位发生了借位 (borrow) 现象。为形式化描述此过程，假设以下辅助函数：

位提取函数：bit(a, n) 表示整数 $a$ 的二进制表示中第 $n$ 位是否取值为 1
借位传播函数：sub_borrow_bit(x, y, b, n) 表示计算 $x - y$ 时，第 $n$ 位是否因低位借位 $b$ 而产生新的借位

任务

试证明定理 testbit_sub_sound（基于 SMT 策略的证明结果，相应引理的分数减半）：

$\forall n, \text{bit}(x - y, n) = (\text{bit}(x, n) \oplus \text{bit}(y, n)) \oplus \text{sub\_borrow\_bit}(x, y, \text{false}, n)$

注意：我们需要证明一个更一般化的结论，其中 b2z 将布尔值转化为整数。

1. b2z_exists (20 分)

theorem b2z_exists (x y : Int) (c0 : Bool) :
    ∃ (cr : Bool),
    Bool.toInt ((!Int.bodd x) && Int.bodd y) +
    Bool.toInt (!(xor (Int.bodd x) (Int.bodd y)) && c0) = Bool.toInt cr

2. sub_borrow_bit 定义 (30 分)

试补充 sub_borrow_bit 递归函数的实现：

def sub_borrow_bit : Int → Int → Bool → Nat → Bool

3. sub_shift (40 分)

theorem sub_shift (a b : Int) :
    (a - b) / 2 = a / 2 - b / 2 - Bool.toInt ((!Int.bodd a) && Int.bodd b)

4. sub_borrow_bit_eq (50 分)

theorem sub_borrow_bit_eq (n : Nat) (x y : Int) (cr c0 : Bool) :
    Bool.toInt ((!Int.bodd x) && Int.bodd y) +
    Bool.toInt (!(xor (Int.bodd x) (Int.bodd y)) && c0) = Bool.toInt cr →
    sub_borrow_bit (x / 2) (y / 2) cr n =
    ((!Int.testBit x n) && Int.testBit y n) ||
    (sub_borrow_bit x y c0 n && !(xor (Int.testBit x n) (Int.testBit y n)))

5. testbit_sub_sound (60 分)

根据上述 lemma，试证明 xtestbit_sub_sound，进而完成证明 testbit_sub_sound。

分值

b2z_exists: 20 分
sub_borrow_bit 定义: 30 分
sub_shift: 40 分
sub_borrow_bit_eq: 50 分
testbit_sub_sound: 60 分

总计: 200 分