Preprint
Sep 2026
Improved Tristate Multiplication With Formalization in Rocq
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 is given, and the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm are provided.
Nandakumar Edamana, Piyush P. Kurur, Unnikrishnan Cheramangalath
· 0 citations