mpn_sqrtrem{1,2}

[Bradley Lucier]

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

//#define FLOAT_CORR_P1

when the IEEE rounding mode is set to round-to-nearest or round-upward; 
one needs additionally

#define FLOAT_CORR_P1

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)

is correct.

Brad