The microblog: 2020.12.31 13:55:52

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: 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.