3 ms·
The proof is implicitly modulo 2^96, which I believed to be the intention of the original code, but it does miss a possible overflow when c is too large, which
by klogic 12y ago
The proof is implicitly modulo 2^96, which I believed to be the intention of the original code, but it does miss a possible overflow when c is too large, which shouldn't happen in its intended use: c2 is already meant to be the overflow limb. I've added an addendum to the post describing, and fixing, this.
- nullc 12y agoThanks! One of the things I find useful for avoiding overconfidence in proof results, beyond making sure to test the proof on multiple broken versions, is to spell out many additional implications of the function that I and/or the caller might expect of it and ask for proofs on them too, even if they seem somewhat redundant. For example, cout = 2ab + cin; I would also prove that for all a,b,cin that cout >= cin; for a or b ==0 that cout == cin, etc.