2020.12.31 13:55:52 (1344628336891318277) from Daniel J. Bernstein, replying to "Abraham D. Smith (@abrahamdsmith)" (1344623511650889729):
The code has passed many billions of tests, but this doesn't rule out the possibility of wrong results for some inputs. (Low-cost protection: multiply 1/x by x; if result isn't 1, try again with random xr.) Verification would analyze what the code does for all possible inputs.
2020.12.31 14:06:49 (1344631092012150786) from Daniel J. Bernstein:
It's clear from the relevant literature how to write down a computer-verified proof of correctness of inversion code along these lines, assuming the machine instructions work as documented, but the situation today is that a proof hasn't been written down for this particular code.
2020.12.31 14:14:15 (1344632964756328454) from Daniel J. Bernstein:
Example of the importance of verifying gcd/inversion code: https://www.forbes.com/sites/daveywinder/2019/06/12/warning-windows-10-crypto-vulnerability-outed-by-google-researcher-before-microsoft-can-fix-it/ Our new code doesn't have data-dependent branches, so it won't hang on some inputs the way Microsoft's code did, but one also doesn't want to have to analyze the security impact of wrong outputs.