如何证明ClickHouse中256位整数乘法实现的正确性？

ClickHouse的256位整数乘法实现，核心是将大整数拆分为64位分段，通过类似竖式乘法的方式计算并处理进位。要证明其正确性，可从以下几个维度展开：

1. 核心实现逻辑拆解 #

该实现将256位无符号整数拆分为4个64位分段，记为：

• 整数A：[a3, a2, a1, a0]，对应数值为 A = a3 × 2^192 + a2 × 2^128 + a1 × 2^64 + a0
• 整数B：[b3, b2, b1, b0]，对应数值为 B = b3 × 2^192 + b2 × 2^128 + b1 × 2^64 + b0

代码中会计算所有分段的乘积 p_ij = ai × bj（i、j从0到3），每个p_ij是128位结果，随后将这些乘积按位权累加到对应位置，最后逐段处理进位，得到最终的512位乘积结果（256位整数相乘的最大结果为512位）。

2. 数学等价性证明 #

分段乘积的位权对应 #

根据代数展开，A×B的数学表达式为所有ai×bj × 2^(64×(i+j))的总和。而ai×bj可拆分为低64位和高64位：ai×bj = low64(p_ij) + high64(p_ij) × 2^64，代入后可得：
ai×bj × 2^(64×(i+j)) = low64(p_ij) × 2^(64×(i+j)) + high64(p_ij) × 2^(64×(i+j+1))
这和代码中将low64(p_ij)累加到结果的第i+j段、high64(p_ij)累加到第i+j+1段的逻辑完全一致，确保了每一部分的位权对应正确。

进位处理的正确性 #

代码中每完成一段的累加后，会将该段数值超过64位的部分进位到下一段：

• 计算当前段的进位值：carry = current_value >> 64
• 保留当前段的64位有效值：current_value & ((1 << 64) - 1)
• 将进位值加到下一段

这个过程和十进制乘法的进位逻辑完全相同，本质是将每一段的数值约束在64位范围内，确保所有分段的累加结果最终等价于数学上的A×B。

3. 边界用例验证 #

通过极端用例验证实现的正确性：

• 全0值：任何数与0相乘结果为0，代码中所有分段乘积均为0，累加后结果全为0，符合预期。
• 全1值：计算(2^256 - 1) × (2^256 - 1)，数学结果为2^512 - 2^257 + 1，验证代码输出的分段是否与该结果的64位分段完全匹配。
• 单段非零：例如仅a0 = 2^64 - 1、b0 = 2^64 - 1，此时乘积的低64位应为(2^64 - 1)^2的低64位，高64位为(2^64 - 1)^2的高64位，其余段为0，代码输出应符合此结果。

4. 形式化验证（可选） #

若需要更严谨的证明，可使用定理证明工具（如Coq、Isabelle）将代码逻辑转化为数学命题，通过形式化方法证明：对于任意256位无符号整数A、B，代码计算的结果与A×B的数学值完全相等。

内容的提问来源于stack exchange，提问作者qhsong