Over the last two months I've done a full review of all files except
_decimal.c and mpdecimal.c.

I now have additional ACL2 proofs for a couple of functions in basearith.c
(some are partial proofs), a full proof for the special case (d = 10**19)
of Granlund/Montgomery's "Divide double word by constant" algorithm and a
full proof for the Chinese Remainder Theorem in crt.c.


I didn't find anything important. I found a couple of useless variable
initializations, missing comments etc.

There was one (deliberate) incompatibility in the format function:
If rounding lead to an Overflow, _decimal printed 'Infinity'.

_decimal can't read back numbers that are out of bounds, so this
was done to ensure that a roundtrip is always possible.


But I changed the function so _decimal now uses exactly the same algorithm
for formatting as decimal.py.