On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal wrote:
> Regardless, you clearly do not understand what I'm asking in question 1) and I do not think it likely that additional interaction on this topic will be useful to either of us.

Asking for a mapping does not really make much sense without specifying the domain/codomain, but my answer actually holds even then.

Anyway, if you _actually_ are interested in this topic then you could start by looking at automatic test case generation using SMT solvers.

On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal wrote:
>> Regardless, you clearly do not understand what I'm asking in question 1) and I do not think it likely that additional interaction on this topic will be useful to either of us.
>
> Asking for a mapping does not really make much sense without specifying the domain/codomain, but my answer actually holds even then.

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.

The correctness check for the mapping in this case is trivial, by which I mean: obvious, readily understood, not needing further explanation, ... a *good* thing in this context.

>
> Anyway, if you _actually_ are interested in this topic then you could start by looking at automatic test case generation using SMT solvers.

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).  This is what I thought that you said you had accomplished with a trivial coverage, your "no problem" remark.  IOW, I thought you claimed to have solved the problem.

I found such a claim remarkable, I did not see it, so I sought clarification.  IIUC now, I was mistaken then.  You have no particular insight to offer toward the solution of the above problem and, by your lights, never made such a claim.

Apparently I took your well meaning remarks much too seriously.

On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal wrote:
> On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad wrote:
>
> For the problem under discussion the domain is 0 .. 2**NBits (binary FP)...
That should be 2**N - 1.

On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad wrote:
> On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal wrote:
>> Regardless, you clearly do not understand what I'm asking in question 1) and I do not think it likely that additional interaction on this topic will be useful to either of us.
>
> Asking for a mapping does not really make much sense without specifying the domain/codomain, but my answer actually holds even then.
>
> Anyway, if you _actually_ are interested in this topic then you could start by looking at automatic test case generation using SMT solvers.

We seem to repeatedly misunderstand one another on this topic so a quick back and forth, without burdening others in the forum, would be a good way to go from here.

I'll be at the end-of-Jan beerconf for much of the time (I'm GMT+8 but will probably overlap with your daytime hours) so if you're interested we can establish a 2-way comm channel there and quickly, I believe, converge on understanding.

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.

On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad wrote:
> 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.

No, of course not.  The parenthetical phrase was meant to apply to everything that preceeded it.  An SMT like solution is what I thought you had asserted, something that substantially cut down the work while provably covering the full domain.

>
> 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.

Well, you've not refuted anything that I can see.  You've asserted something, yes, something that I think is quite useful if provable.  The intutition that prompts you to make such an assertion is what I'm most interested in.  I do not believe the assertion is provable but would be very happy to be proven wrong as that would be a win for everyone.

Since you continue to take offense at my writing, where none was intended, I think direct two way communication would be better than continuing here.  I'll be hanging out at beerconf if you think it's worth your time to converge on understanding.  Even if we aren't able to take your intuition to a proof or refutation quickly, we should at least be able to comprehend a lack of ill will.

On Friday, 29 January 2021 at 02:58:38 UTC, Bruce Carneal wrote:
> The parenthetical phrase was meant to apply to everything that preceeded it.  An SMT like solution is what I thought you had asserted, something that substantially cut down the work while provably covering the full domain.

I am not asserting anything, other than that I don't think full formal verification (unless bitblasting works) is within the perimeter of the D community, so that leaves informal proofs combined with selective testing as the viable option that the D community as a whole (not any specific individual) can accomplish.

A solver is a tool that can be used to make this viable. Without a solver, maybe a reimplementation with a correspondence proof is easier.


> better than continuing here.  I'll be hanging out at beerconf if you think it's worth your time to converge on understanding.


I like the idea of beerconf, but I have a deliverable deadline on monday, so I don't have time this week.

On Friday, 29 January 2021 at 13:42:49 UTC, Ola Fosheim Grøstad wrote:
> On Friday, 29 January 2021 at 02:58:38 UTC, Bruce Carneal wrote:
>> The parenthetical phrase was meant to apply to everything that preceeded it.  An SMT like solution is what I thought you had asserted, something that substantially cut down the work while provably covering the full domain.
>
> I am not asserting anything, other than that I don't think full formal verification (unless bitblasting works) is within the perimeter of the D community, so that leaves informal proofs combined with selective testing as the viable option that the D community as a whole (not any specific individual) can accomplish.

Then I misunderstood you all along.  I thought that you were describing something that would be part of a formal proof.

As an aside: I consider an exhaustive f32 proof to be very strong evidence that an implementation will likely be correct for larger formats.

>
> A solver is a tool that can be used to make this viable. Without a solver, maybe a reimplementation with a correspondence proof is easier.
>
>
>> better than continuing here.  I'll be hanging out at beerconf if you think it's worth your time to converge on understanding.
>
>
> I like the idea of beerconf, but I have a deliverable deadline on monday, so I don't have time this week.

OK.  I hope we have the opportunity to chat directly at a later date.  Good luck meeting your deadline.

On Friday, 29 January 2021 at 14:24:17 UTC, Bruce Carneal wrote:
> Then I misunderstood you all along.  I thought that you were describing something that would be part of a formal proof.

A formal proof would have to be machine checked. So you need a good solver/verifiers. And experience to make good use of, and patience... I think we can safely say that this is out of scope for the D community at this point.

On Friday, 29 January 2021 at 18:35:54 UTC, Ola Fosheim Grøstad wrote:
> On Friday, 29 January 2021 at 14:24:17 UTC, Bruce Carneal wrote:
>> Then I misunderstood you all along.  I thought that you were describing something that would be part of a formal proof.
>
> A formal proof would have to be machine checked. So you need a good solver/verifiers. And experience to make good use of, and patience... I think we can safely say that this is out of scope for the D community at this point.

And you would also need to annotate the D code with Hoare logic and generate verification conditions. Although there are tools that can help with that. But you would still need expertise to make good use of it. It is not a push-button topic.

The only other alternative would be bit blasting, as I mentioned, which may or may not work out. Probably not if the code is too convoluted, but it might. Depends on the solver and structure of the input.