发表机构
Indian Institute of Technology Palakkad（印度理工学院帕拉克德分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出一种更精确的三态数乘法算法，在 Rocq 中形式化验证其正确性，性能与旧算法相当，并已纳入 Linux 内核。
AI 中文摘要
我们提出了一种新的三态数乘法算法，在精度和形式化证明方面改进了 Linux 内核中现有的最先进实现。实验评估表明，我们的算法显著更加精确（在峰值情况下，对于31位样本，与先前工作相比，在95.59%的情况下给出了更好的结果）。重要的是，基准测试证明，我们在获得额外精度的同时，性能与先前算法相当。最后，我们在 Rocq 证明助手中形式化并证明了该算法的正确性，增强了对最终实现的信任。我们的算法现已纳入 Linux 内核上游。我们针对新乘法算法在 Rocq 中的正确性证明适用于所有位宽，而先前算法附带的基于 SAT/SMT 的机器检查证明仅限于8位。我们还提供了 Rocq 证明，用于新添加的 tnum 并集操作和 Linux 内核中现有 tnum 加法算法的正确性与最优性。我们针对 tnum 加法的最优性证明提出了一个比先前工作更简单直接的引理。
英文摘要
We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at the peak, giving better results in 95.59% cases compared to the previous work for 31-bit samples). Importantly, we achieve this additional precision with performance comparable to the previous algorithm, as demonstrated by benchmarks. Finally, we formalize and prove the soundness of the algorithm in the Rocq proof assistant, adding to the trust in the resulting implementation. Our algorithm is now part of the upstream Linux kernel. Our soundness proof in Rocq for the new multiplication algorithm works for all bit widths, while the SAT/SMT-based machine-checked proof accompanying the previous algorithm was restricted to 8 bits. We also provide Rocq proofs for the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm from the Linux kernel. Our optimality proof for tnum addition presents a simpler and straightforward lemma compared to prior work.
