Improved Tristate Multiplication With Formalization in Rocq
Nandakumar Edamana, Piyush P Kurur, Unnikrishnan Cheramangalath
原文摘要
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.
cs.LO