On Friday, 29 January 2021 at 18:48:42 UTC, Ola Fosheim Grøstad wrote:
> 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.

Have you seen KLEE?  It applies a solver like Z3 to normal code with assert() statements, as long as it can be compiled to LLVM bitcode and run with KLEE-compatible standard libraries.

The original KLEE doesn't support floating point, but there's a fork that does (which I've never used).

https://theartofmachinery.com/2019/05/28/d_and_klee.html
(There are some things I need to fix/update in that post.)

On Friday, 29 January 2021 at 21:11:02 UTC, sarn wrote:
> Have you seen KLEE?  It applies a solver like Z3 to normal code with assert() statements, as long as it can be compiled to LLVM bitcode and run with KLEE-compatible standard libraries.

I've only read about KLEE, which looks interesting. Using LLVMIR  is one approach one can use for analysis when the input/output is tiny. You can (after unrolling) convert the IR  to  64 logical propositions. One big logical (boolean) formula for each bit in the output.

In this specific application you could try to prove that output bit 1 only depends on input bit 1, output bit 2 only depends on input bit 2 and so on.

(After applying the inverse function, so that the function returns the same value as the input.)

On 1/28/21 1:21 AM, H. S. Teoh wrote:
> On Wed, Jan 27, 2021 at 10:18:58PM -0500, Steven Schveighoffer via Digitalmars-d wrote:
>> On 1/26/21 9:17 PM, H. S. Teoh wrote:
>>>
>>> If there was a way to make these tables pay-as-you-go, I'd vote for
>>> it.  Adding 104KB or 52KB even if the code never once formats a
>>> float, is not ideal, though granted, in this day and age of cheap,
>>> high-capacity RAM not really a big issue.
>>
>> There is a way -- dynamic libraries. It's how C does it.
> 
> That's total overkill for 100KB of data.

The idea is it would go into the phobos shared library, not a specific shared library just for floats.

> 
> 
>> But seriously, I can't imagine why we are concerned about 100KB of
>> code space. My vibe.d server is 80MB compiled (which I admit is a lot
>> more than I would like, but still). My phone has as much code space as
>> 100 computers from 10 years ago. Are you still using floppies to share
>> D code?
> [...]
> 
> It's not so much this specific 100KB that I'm concerned about; it's the
> general principle of pay-as-you-go.  You can have 100KB here and 50KB
> there and 70KB for something else, and pretty soon it adds up to
> something not so small. Individually they're not worth bothering with;
> together they can add quite a bit of bloat, which may be desirable to
> get rid of, for embedded applications say.

I get that there is a need for it in niche cases. But those are very niche, and I'd expect a custom runtime for them anyway.

But the solution to having code that is small is to use a shared library for the common code. This seems like a perfect fit for that.

-Steve

On Friday, 29 January 2021 at 22:03:26 UTC, Ola Fosheim Grøstad wrote:
> input/output is tiny. You can (after unrolling) convert the IR  to  64 logical propositions. One big logical (boolean) formula for each bit in the output.

Or more likely 128 boolean expressions, since you probably have more chance of resolution if you first show that there is no solution for output1 == false && input1 == true, then you do the same for output1 == true && input1 == false.

On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad wrote:
> I do however refute the idea that an exhaustive test is needed, since the problem involves regular patterns.

how about a full coverage of a half float type, assuming the function tested works the same with float and double and anay arbitrary lond FP type, e.g template param for mantissa and exp. Sof if a smaller FP type fully passes the for loop test, e.g all permutations we can assume bigger FP types will be 100% correctly converted.

On Saturday, 30 January 2021 at 11:02:54 UTC, Afgdr wrote:
> On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad wrote:
>> I do however refute the idea that an exhaustive test is needed, since the problem involves regular patterns.
>
> how about a full coverage of a half float type, assuming the function tested works the same with float and double and anay arbitrary lond FP type, e.g template param for mantissa and exp. Sof if a smaller FP type fully passes the for loop test, e.g all permutations we can assume bigger FP types will be 100% correctly converted.

Well I forgot that it may use LUTs so maybe not in this case, but otherwise you should get the idea.

On Saturday, 30 January 2021 at 11:06:34 UTC, Afgdr wrote:
> Well I forgot that it may use LUTs so maybe not in this case, but otherwise you should get the idea.

Yes, I get your idea, but I think one has to be a bit more careful and base what is tested on what the implementation does. For instance, float32 does not expose overflow issues.

We can assume that LUTs are correct if they are pre-generated, though.