Support giving a minimum & maximum to Data.Floats

[Seelengrab]

This is currently not supported since the data model is not rich enough to provide good shrinks (without rejecting too many test cases), but would be very nice to have. This would mostly copy what Hypothesis is doing here, which might require #25 so that the generated values continue to shrink well.

The workaround for now is to use assume! in user code involving Data.Floats to reject any unwanted samples.

[raineszm]

This is probably the biggest feature missing from Supposition for me.

Are there any code contributions that would make it easier to move towards this?

Thanks!

[Seelengrab]

Thank you! Mind you, this is just 2). If you like, you can still give 1) a try. You'd add that here, instead of the reinterpret. There's a bunch of floating point utilities in util.jl that should make it easy to pull the number apart & put it back together. As for a test that shows the difference - I haven't thought of one yet! I think it'd basically converge faster, so maybe something could be tested there? That'd probably require keeping the current implementation around in the testsuite.

[raineszm]

I was looking at doing just that. Perhaps it would a test could check that the shrinking works as expected, i.e. shrinking the input integer shrinks the float in the corresponding way.

Do you have a preference for where the supporting functions like decode_exponent should go? In utils.jl or data.jl or a new file?

[Seelengrab]

i.e. shrinking the input integer shrinks the float in the corresponding way.

That's not directly exposed/accessible - you could check how SuppositionReport.final_state.calls compares when running the two side-by-side with the same RNG seed. Whether this will actually improve or not is I guess something that we'll find out afterwards 😅

One complication might be that there's already a bit of floating point special handling just for shrinking in shrink.jl - see shrink_float. We'll have to see how that interacts.

Do you have a preference for where the supporting functions like decode_exponent should go? In utils.jl or data.jl or a new file?

You can chuck the lookup table right above produce! for Floats. I don't think you'll need the dedicated function, just indexing should be fine. Note that you likely won't need update_mantissa; assemble from utils.jl should already be able to handle the various manipulations you need to do. IIRC, the IR they've chosen matches the layout of a floating point value exactly, so that should work out fine. It's easier to work on the parts of the floating point directly instead of manually hacking around with shifts and such, and that also allows extending this to Float32 and Float16 in one fell swoop.

For other utility functions (e.g. things like max_exponent) that would need to be extended to more than Float64, putting them in util.jl is good 👍 I'll probably reorganize all of data.jl at some point anyway, it's starting to get quite unwieldy.

[raineszm]

Cool. I'm working on implementing that. We'll see if I get it figured out in a reasonable amount of time; this is my first time mucking about with floating point encodings.

What I meant for tests was that the encoding used by hypothesis is supposed to mean that smaller integers -> 'simpler' floats which is testable. I know the encoding table handles this for the exponents but I thought update_mantissa did a bit of fiddling with the encoding to make this true also for fractional bits.

[Seelengrab]

What I meant for tests was that the encoding used by hypothesis is supposed to mean that smaller integers -> 'simpler' floats which is testable.

Right, what I mean is that Hypothesis does that by having access to an object dedicated to shrinking int -> float; Supposition.jl has an analog in shrink_float (see src/shrink.jl:93), but that requires having access to both a TestState and an Attempt. That makes this kind of test much more complicated than it needs to be, so I think we can postpone that until I get to finish the implementation of #25.

There's a bunch of other good tests in the hypothesis tests though that don't require this kind of access, so porting those would be good!

I know the encoding table handles this for the exponents but I thought update_mantissa did a bit of fiddling with the encoding to make this true also for fractional bits.

Most of update_mantissa is fiddling around with just the extraction of the fractional part, which is the part that the functions in util.jl take care of for you generically ;) The reverse_bits function should be implementable with bitreverse and/or bitrotate from Base.