migrate Float shrinker to the ir

[tybug]

I had originally tried writing a shrinker_v2.py from scratch...and quickly abandoned it as infeasible. I think my current plan is to convert shrinking passes one by one (where possible, which may or may not be all of them). minimize_floats is one of the more directly applicable ones.

Definitely open to feedback on the details of the migration approach here.

There is overlap in the IRTree definition with #3806, though it's not exactly the same. Either is fine to merge before the other; I'll handle conflict resolution whichever way.

[tybug]

Seeing some slow shrinks locally (-k test_shrinks_downwards_to_integers_when_fractional). I think I'll need to add ir_tree support to cached_test_function, alongside buffers. We'll maintain both and then drop buffers once everything is on the ir.

[tybug]

shrinking may make modifications that misalign the ir tree. When working with buffers, we still run these all the way to a result, but my guess is they are very unlikely to be useful shrinks.

I don't know if there's anything better we can do for ir trees than giving up, beyond realigning tricks that are research papers in their own right. One idea is passing shrinker.engine.random here and continuing randomly, which might work, but I don't know if the same ir tree prefix running to different buffers will blow up.

By bailing out early we do less work in the test function, which means we could actually be spending more time proportionally on useful shrinks by overrunning. So it might be a wash at the end of the day. But I don't have a good intuition.

(also, just realizing: this should maybe be mark_invalid rather than overrun)

[Zac-HD]

@DRMacIver would be the world expert on this one 😅

Let's start with the simplest implementation that gets all our tests passing, and then we can profile it and see if there's anything obviously-silly going on. "Continue randomly until not-a-shrink" would make sense to me, although I'm not confident it'd be a win; "continue but try realigning each time we leave an Example" is also salient to me for the explain phase (for shrinking, we'd also abandon if the misaligned-Example was > the base).

[tybug]

Good and bad news, mostly good:

• cached_test_function actually already caches our ConjectureData.for_ir_tree datas, because running an ir_tree= data is no different from a prefix= data from the outside; both run to a buffer. No need to add a separate cache for ir trees. yay!
  • I think this means this shrinker migration will come at no cost?
• ...as a consequence, this forces — no pun intended — our hand in implementing fake_forced. The ConjectureResult returned by an ir_tree= data needs to be completely correct, because it will be cached as the result for a buffer. fake_forced is messy, hard to verify correct, and will probably need to stick around even after the ir migration is complete. oh well, can't have everything.
• pending ci, float shrinking basically works! There's a single failure in test_float_shrink_can_run_when_canonicalisation_does_not_work, which isn't a "float shrinking is broken" failure, but "you are calling the float shrinker on 1000.0 where you didn't used to". related review comment below.

I've pushed all my work here so we can see how everything fits together in a single place, but I'm going to bundle a few smaller changes in a split pr shortly. As is typical, this pr got very large very quickly 😄

[tybug]

Right now, we call Float.shrink on any float node (+ some short circuiting behavior in Float). The previous behavior skipped Float.shrink on floats that happened to also be integers:

        buf = self.shrink_target.buffer
        b = buf[u:v]
        f = lex_to_float(int_from_bytes(b))
        b2 = int_to_bytes(float_to_lex(f), 8)
        if b == b2 or self.consider_new_buffer(buf[:u] + b2 + buf[v:]):

I think the if b == b2 condition there is equivalent to checking if is_simple(f). i.e., don't try to float-shrink float nodes if they are already integers. The comments in lexical.py in this commit give some further insight:

        # This floating point number can be represented in our simple format.
        # So we try converting it to that (which will give the same float, but
        # a different encoding of it). If that doesn't work then the float
        # value of this doesn't unambiguously give the desired predicate, so
        # this approach isn't useful. If it *does* work, then we're now in a
        # situation where we don't need it, so either way we return here.
        if is_simple(f):
            self.incorporate_float(f)
            return

To be honest, I'm not sold that we don't want to shrink float nodes as floats even if they happen to currently be integers. We mostly defer to the Integer shrinker anyway, and it also seems to make logical sense to keep all float-shrink-logic in the same place instead of jumping around. But I'm probably missing a good historical reason for it to be done this way. It's easy to put this condition back either way.

[Zac-HD]

I think the intuition here is that we consider integer-valued floats simpler than all non-integer-valued floats, and so once we get to an integer-value we might as well use the machinery we have for shrinking integers.

You could probably convince me that a different ordering is better, but that's how I understand the status quo.

[tybug]

ok, I think that makes sense to me. I'll add this safeguard back. I was thinking about the case where shrinking an integer-valued float is faster if you allow it to try intermediate float values. But Integer probably gets you close enough to the minimum and then you can finish it off with a final Float pass.

I'd like to take a detailed look at the shrink ordering at some point. I saw a few weird things like values in (0, 1) being ordered after almost everything else; assert float_to_lex(sys.float_info.max) < float_to_lex(0.5). But for another day!

I think Hypothesis' shrinker is so well tuned that I shouldn't make changes like this without profiling or being very confident in them first. Of course, we may have no choice but to be adventurous when we get to the more complicated passes 🙂

[Zac-HD]

Values between zero and one: not integers, and we order kinda by number of decimal places, so. And the largest finite float is an integer, which means "simpler" than 0.5! (I did say I'm not that attached to the ordering)

[tybug]

Unfortunately ran out of time tonight for the aforementioned split pr, but will get to it tomorrow.

[tybug]

Now that the infra is in place, I'm hopeful we can fly through these shrinker migrations. Only had time for this tonight, but more pulls to come!

[tybug]

ahh, coverage failure - will have to wait for tomorrow.

[Zac-HD]

Looking good! Small comments below, but this doesn't look like it'll suddenly grow on us...

[tybug]

3ca282e is a probably-bug-fix: we weren't considering smallest_nonzero_magnitude when counting the number of possible float children. This was probably a ticking time bomb for someone trying to use a small-range float strategy without subnormal support, though I haven't tried writing a strategy that would manifest this.

[Zac-HD]

Looks great with some very small comments below, please merge when they're addressed (or not) to your satisfaction!

[tybug]

thanks for the comments, they were all helpful!

[Zac-HD]

Since we've closed #3086, do you want to open an issue to track all the remaining parts of the migrate-to-IR project? #3086 (comment) is not particularly detailed and I think we could probably break it down further now that we've come this far.

[tybug]

have also been thinking that we need a better issue for the IR project. I'll write something up.