[lifthrasiir]

While it is a difficult problem, it is not an infeasible problem nowdays, at least for trigonometric, logarithmic and exponential functions. (All possible arguments have been mapped to prove how many additional bits are needed for correct rounding.) Two-argument pow remains an unsolved problem in my knowledge though.

[jcranmer]

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.

[lifthrasiir]

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