arXiv:2609.39009 · v2
Improved Tristate Multiplication With Formalization in Rocq
摘要
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. 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. Our algorithm is now part of the upstream Linux kernel. We also provide the first machine-checked proofs for tnum arithmetic operations that work for all bit widths. Our proofs include the soundness of the new multiplication algorithm and the soundness and optimality of supporting operations.
作者备注：- Related Rocq code can be found at https://github.com/nandedamana/trirocq - Related benchmark code can be found at https://github.com/nandedamana/improved-tnum-mul - v2 changelog: (1) reporting end-to-end verification, (2) updated presentation, (3) text updates following code updates