zlacker

My understanding is we have exhaustively enumerated the unary binary32 functions and proved the correctness of correct-rounding for them. For binary64, exhaustive enumeration is not a viable strategy, but we generally have a decent idea of what cases end up being hard-to-round, and in a few cases, we may have mechanical proofs of correctness.

There was a paper last year on binary64 pow (https://inria.hal.science/hal-04159652/document) which suggests that they have a correctly-rounded pow implementation, but I don't have enough technical knowledge to assess the validity of the claim.

>>jcranm+(OP)
For your information, binary64 has been indeed mapped exhaustively for several functions [1], so it is known that at most triple-double representation is enough for correct rounding.

[1] https://inria.hal.science/inria-00072594/document

> There was a paper last year on binary64 pow (https://inria.hal.science/hal-04159652/document) which suggests that they have a correctly-rounded pow implementation, but I don't have enough technical knowledge to assess the validity of the claim.

Thank you for the pointer. These were written by usual folks you'd expect from such papers (e.g. Paul Zimmermann) so I believe they did achieve significant improvement. Unfortunately it is still not complete, the paper notes that the third and final phase may still fail but is unknown whether it indeed occurs or not. So we will have to wait...