lucier at math.purdue.edu
Sun Jan 29 04:29:19 UTC 2017
Regarding Adrien Prost-Boucle's recent message to this list:
Using the monotonicity property of sqrt, integer->floating-point
conversion, and floating-point->integer conversion (by truncation) in
any of the IEEE rounding modes, one can check that Adrien's codes
uint32_t sqrt32_float(uint32_t val)
uint32_t sqrt32_float_double(uint32_t val)
uint64_t sqrt64_float_double(uint64_t val)
uint64_t sqrt64_float_longdouble(uint64_t val)
are correct with
when the IEEE rounding mode is set to round-to-nearest or round-upward;
one needs additionally
when the IEEE rounding mode is set to round-downward or round-truncate.
By "monotonicity" I mean that if the argument to an operation is
increased then the result doesn't decrease.
One checks the correctness of each of these routines by showing, e.g.,
that for each uint32_t value i, that sqrt64_float_double gives the
correct answer for (i*i) and (i*i + 2*i), so by monotonicity it gives
the correct answers for all values in between.
There are too many uint64_t values to check programmatically, and I
don't know how to prove a priori that the code for
uint64_t sqrt64x2_float(uint64_t valh, uint64_t vall)
More information about the gmp-devel