Handle zig-zagging when doing more global lexicographic minimization

[DRMacIver]

Note: This is part of #1093, where I encourage people to work on the shrinker. As such I will not be working on it myself and encourage you to take a look at it if it takes your fancy.

This particular issue is intended more by means of an interesting intellectual puzzle than an actual useful goal to achieve. Being able to solve it well probably implies that we are in very good shape at lexicographic minimization, but it doesn't actually in and of itself imply anything very useful (and thus hyper-specific changes that target exactly this are probably not that useful). I recommend doing it in pieces, and I recommend not doing it as your first pull.

Context: There is a problem that I refer to as "zig zagging" where small changes to the byte stream in one place keep unlocking small changes to the byte stream in a different place. The canonical example of this is:

@given(st.integers(), st.integers())
def test_zig_zag(m, n):
    assert abs(m - n) != 1

Shrinking is forced to repeatedly subtract 2 from each of m and n on their own unless it can lower the two together, so this takes O(m) to complete, which is exponential in the data size.

Hitting this sort of problem sucks because it means that we will hit the max_shrinks limit, which means we'll end up with a rubbish final example, not just for this part of the data but also for everything else that we got distracted before getting to.

Since #1082 we handle this example correctly, by finding the right simultaneous lowering of both blocks, but there are other ways to trigger similar examples.

One such way is to simply choose a worse encoding of integers. Suppose we were to encode integers as 64 separate single bits, then smoosh them together as a big-endian encoding, and then run the same test. Because of the way that heuristic detection works on blocks, it is unable to make the same sort of large changes that get us out of this hole in the main case.

Here's an engine unit test that demonstrates the problem, or would if we were actually able to hit it:

def test_weird_zig_zag(monkeypatch):
    monkeypatch.setattr(
        ConjectureRunner, 'generate_new_examples',
        lambda runner: runner.test_function(ConjectureData.for_buffer(
            [1] * 64 + [1] * 63 + [0]
        ))
    )

    @run_to_buffer
    def x(data):
        bits = []
        for _ in range(2):
            k = 0
            for _ in range(64):
                k <<= 1
                k |= data.draw_bits(1)
            bits.append(k)
        m, n = bits
        if abs(m - n) == 1:
            data.mark_interesting()

    assert x == hbytes([0] * 64 + [0] * 63 + [1])

Right now we get out of this issue by being absolutely rubbish at minimizing this example! This is because we don't do global lexicographic minimization at all right now. If we did the minimizer would just go "Hey, how about hbytes([0] * 64 + [0] * 63 + [1])?" as its second call and bam we're done. But then we could patch the test to instead check if, say, n = m + 1, which would make the final example hbytes([0] * 63 + [1] + [0] * 64) instead so that wouldn't work.

A partial list of things that I think might be useful for this:

1. Solving Handle non-equality constraints when performing simultaneous shrinking #1095 - the n = m + 1 version can be solved by simultaneously replacing two one-blocks by zero-blocks. This would probably be a decent first pass at this, although it has the frustrating problem that the only way we can make progress like that is quadratically.
2. Turning on global lexicographic minimization, so that we run the minimizer on if not the whole shrink target at least the non-structural parts (i.e. any block not marked as shrinking) parts, might allow us to offload this problem to somewhere where at least it has all the moving parts required simultaneously.

My recommended approach to working on this is to do multiple iterations of trying the simplest thing that isn't ridiculously overfitted to make a version of the above test work and then seeing if you can modify it to break your fix and try something else.

[Zac-HD]

I'm closing this because after four years I don't expect a volunteer to take it on soon - and as we said in #1093:

At present there is literally no good reason to improve the Hypothesis shrinker except enjoyment and weird aesthetic obsessions: due to the combination of better underlying model and a truly disproportionate amount of invested effort, it is currently so good that everyone else's shrinking looks comedically bad in comparison.