Printing floating points

[Ola Fosheim Grøstad]

On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal wrote:
> For the problem under discussion the domain is 0 .. 2**NBits 
> (binary FP) and the codomain is the problem specified string 
> output of the function.  This has not changed and I had thought 
> it was clear to all concerned throughout.

Let's backtrack then. My suggestion was that one does an informal 
proof of the easier aspects one can reason about and then do 
testing to cover those aspects which one cannot convince oneself 
of. So in order to list those tests one would have to do a deep 
analysis of the actual implementation informed by the 
properties/proofs of the abstract algorithm (the spec). Without 
such an analysis one cannot give examples of dependencies 
expressed as propositions.

The core problem float2string is comparable to fixedpoint2string 
which is comparable to integer2string, because the transform from 
float to fixed point is trivial. (We also note that float is 
base2 and the target is base10, and that 10=5·2 so we may be 
rewarded for paying attention to modulo 5.) Then we may choose to 
represent a base 10 digit with something that is easier to deal 
with for a solver. We then need to think about, not increments of 
1, but relationships in terms of modular arithmetic/congruence - 
related formalizations.


> I am actually interested in proving correctness by establishing 
> full coverage of the domain with something less expensive than 
> direct enumeration, less expensive than a for loop across all 
> possibilities (an SMT-like solution).

SMT/SAT based solutions are not like a for-loop across all 
possibilities.

Are you actually serious about proving correctness? I don't get 
that feeling.


> You have no particular insight to offer toward the solution of 
> the above problem and, by your lights, never made such a claim.

I am not sure what you mean by this, but you sure manage to make 
it sound offensive... I've suggested utilizing bit-blasting, 
identity transform, modular arithmetics etc. I've never hinted or 
suggested that I have any intent of working on this problem, and 
explicitly stated that I have not taken a close look at the Mir 
implementation, nor do I intend to.

I do however refute the idea that an exhaustive test is needed, 
since the problem involves regular patterns.