Exact division semantics should separate underflow

[pavpanchekha]

Per my understanding, VCFloat has an annotation for exact division by powers of two. That is, the expression x / 2 can be annotated, and in that case it doesn't generate an epsilon (a relative error), though it does generate a delta (an absolute error). Same for other powers of two. I was just talking to Andrew at POPL and he asked me to file this example of where that is insufficient.

In the fdlibm implementation of acos, inputs in [0.5, 1.0] are range-reduced with the expression sqrt((1 - x) / 2). (The else block.) The subtraction is Sterbenz-exact and the division is also exact, and that allows the square root to be done efficiently in double-double (look for the c variable), which is important for the accuracy of this algorithm.

The input x = 1.0 thus divides 0.0 / 2 = 0.0. A tiny absolute error then matters; intuitively, acos is vertical at 1.0 so even a tiny error can create a large difference. The proof is still doable if you treat 1.0 as a special case; the next-largest floating-point number 1.0 - eps has a slope of about ~sqrt(eps) which amplifies a tiny absolute error to still a tiny number. But you wouldn't need the separate case for 1.0 if the tiny absolute error were gone too.

Fixing this might require two different kinds of exact division annotations, one which has a VC for no underflow and a another of which allows underflow but has a tiny absolute error.