Migrate our core representation to the typed choice sequence

[Liam-DeVoe]

This epic-style issue tracks our work on migrating the internals of Hypothesis from a bytestring to the typed choice sequence.

This is a huge change that touches every part of Hypothesis. The short version is that we have encountered several shortcomings of Hypothesis internals over time, which have limited the efficiency of input generation and shrinking, and made alternative backends infeasible. We expect this migration to give moderate efficiency gains and pave a clear path forward to future integration with alternative backends or other powerful features which are currently intractable.

Bytestring

Hypothesis currently works at the level of a bytestring (a sequence of bytes).

• To generate inputs, view strategies as a parser of the bytestring which interpret bytes as a series of random choices
• Store inputs in the db as their bytestring representation
• Shrink inputs by shrinking their corresponding bytestring ("internal shrinking").
• Generate novel inputs by generating a novel prefix of the bytestring (via DataTree internally) and randomly generating the remaining bytes.

But, the bytestring has its limitations.

• Redundancy. The mapping of bytes ↦ input is not injective, so an input may have many byte representations. For instance, 0 is represented by many different bytestrings, so any strategy using st.integers() effectively wastes some number of inputs (except for detecting flakiness). See also generate_novel_prefix interacts poorly with biased_coin (and lists) #1574.
• Precision. Effecting predictable changes in the input via changes in the bytestring is difficult, in e.g. shrinking. For instance, we would like to be able to "naturally" shrink floats, eg by exponentially ramping up division or truncation. Doing this in the byte representation is quite nasty. In fact, we currently hack around this by parsing bytes which look like they could represent floats into a float, shrinking that, and serializing it back into the bytestring.

These limitations extend equally to alternative backends over the bytestring. e.g. for CrossHair (#3086) integration, bytes is simply too low level to get an efficient SMT algorithm out of.

Typed Choice Sequence

Enter the typed choice sequence, which replaces the bytestring. We lift up the representation from bytes to a slightly higher representation at the level of five types: boolean, integer, float, string, and bytes.

class PrimitiveProvider(abc.ABC):
    @abc.abstractmethod
    def draw_boolean(
        self,
        p: float = 0.5,
    ) -> bool:
        ...

    @abc.abstractmethod
    def draw_integer(
        self,
        min_value: int | None = None,
        max_value: int | None = None,
        *,
        # weights are for choosing an element index from a bounded range
        weights: Sequence[float] | None = None,
        shrink_towards: int = 0,
    ) -> int:
        ...

    @abc.abstractmethod
    def draw_float(
        self,
        *,
        min_value: float = -math.inf,
        max_value: float = math.inf,
        allow_nan: bool = True,
        smallest_nonzero_magnitude: float,
    ) -> float:
        ...

    @abc.abstractmethod
    def draw_string(
        self,
        intervals: IntervalSet,
        *,
        min_size: int = 0,
        max_size: int | None = None,
    ) -> str:
        ...

    @abc.abstractmethod
    def draw_bytes(
        self,
        min_size: int = 0,
        max_size: int | None = None,
    ) -> bytes:
        ...

This improves redundancy (as DataTree operates at this higher level) and precision (as we retain type and shape information about what was previously spans of the bytestring). The end goal is rebuilding input generation, shrinking, targeted pbt, the explain phase, the database, etc on the typed choice sequence, and we expect to see performance gains in each (except the database).

Roadmap

• initial refactorings
  • Move float, integer, string, byte, and boolean drawing logic into PrimitiveProvider #3788
  • Support forcing all primitives #3801
• Migrate DataTree to the new IR #3818
• Add support for crosshair backend #3806
• migrate Float shrinker to the ir #3899
• Migrate most shrinker functions to the ir #3962
• Remove sub-ir examples #4007 (+ migrate generate_mutations_from)
• Add support for variable-width bytes in the IR #4097
• Fold integer endpoint upweighting into weights= #4138
• Implement extend for cached_test_function_ir #4159
• Migrate explain phase to the typed choice sequence #4162
• Migrate Optimiser to the typed choice sequence #4163
• Migrate generate_novel_prefix to the typed choice sequence #4172
• Implement choice_{to, from}_index #4209
• Implement and use sort_key_ir #4215
• Use ConjectureData.for_choices #4219
• Use the typed choice sequence for @reproduce_failure #4220
• lower_blocks_together -> lower_integers_together #4235
• Add and use BytestringProvider in fuzz_one_input #4221
• Use typed choice sequence in database #4241
• Fully move to the typed choice sequence cache #4247
• Define extend: int = 0 and NodeTemplate in terms of choice count #4249
• Remove ConjectureData.buffer #4250
• cmd + f TODO_IR

[JonathanPlasse]

This is super interesting!
Thank you for writing this detailed issue.
I would like to get involved with hypothesis.
What would constitute a good first contribution here?

[Zac-HD]

Welcome, Jonathan! We'd love to have you continue contributing - I already really appreciate the type-annotation-improvements for our numpy and pandas extras, so this would be a third contribution 😻

@tybug might have some ideas here, but my impression is that the "refactor for an IR" project in this issue is more-or-less a serialized set of tasks and so adding a second person is unlikely to help much - even with just one we've had a few times where there were two or three PRs stacked up and accumulating merge conflicts between them.

As an alternative, #3764 should be a fairly self-contained bugfix. On the more ambitious side, #3914 would also benefit from ongoing work on that - testing, observability, reporting whatever bugs you surface, etc. Or of course you're welcome to work on any other open issue which appeals to you!

[JonathanPlasse]

Thanks, I will start with #3764 and then take on the different issue on #3914.

[Zac-HD]

We may still use the bitstream representation for some things (database?).

I was thinking that we'd still serialize to a bytestring - that's the ultimate interop format, and when we need to handle weird unicode and floats like subnormals or non-standard bitpatterns for nan I don't want to trust whatever database backend our users cook up to round-trip correctly. Existing formats like protobuf or msgpack all have constraints like "unicode strings must be valid utf-8" or "numbers limited to bits", so I wrote a custom serializer instead 🙂

[Liam-DeVoe]

yeah, this is a hard one to parallelize 😄. Some of the steps may subtly depend on others in ways that aren't obvious until one is knee deep in implementing it.

so I wrote a custom serializer instead 🙂

Nice! I agree with the reasoning here. Added a task for this. This probably needs to be the absolute last thing to switch to the ir.

[Zac-HD]

Definitely the last thing to switch, I just got nerdsniped 😅

[Zac-HD]

467ab23 (#3924) uses a nocover pragma to get the PR merged after I reduced our use of ParetoFront - I think it was tested mostly by accident before, but you'll have a better sense than I for where deliberate tests should go.

[Liam-DeVoe]

This should be covered by test_data_with_misaligned_ir_tree_is_invalid. I think the coverage there is just flaky because the condition is too permissive. Will address in #3923 by splitting the test

[Liam-DeVoe]

I'm working on migrating shrinker block programs. Our upweighting for large integer ranges is giving the shrinker trouble, because it means that a simpler tree can result in a longer buffer: the buffer runs through the weighted distribution and draws n bits from some small bucket, while the tree runs through the uniform distribution (as a result of forced=True) and draws m > n bits, where the difference in m and n is large enough that it offsets whatever simplification is made by the tree.

Real example of this:

b1 = b'\x01\x00\x01\x00\x00\x00\x01\x00\x01\x00\x00\x00\x01\x00\x01\x00\x00\x00\x01\x00\x01\x00\x00\x00\x01\x00\x01\x00\x00\x00\x00'
b2 = b'\x01\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00'
s = st.lists(st.integers(0, 2**40))

print("complex result, smaller buffer", ConjectureData.for_buffer(b1).draw(s))
# complex result, smaller buffer [0, 0, 0, 0, 0]
print("simpler result, larger buffer", ConjectureData.for_buffer(b2).draw(s))
# simpler result, larger buffer [0, 0, 0, 0]

As a result I'd like to look at moving that weighting logic into IntegerStrategy, which imo is where it logically belongs anyway, not at the ir layer. To accommodate this with weights, we'll need a structure that can express weights for entire ranges, not just "weight points and everything else is uniform". What do you think of weights=[(a, b, p), ...] where union((a, b), ...) == [min_value, max_value], sum(p) == 1, and len((a, b), ...) <= 255?

[Zac-HD]

What if we forced even more instead?

If we choose a smaller bits size, instead of drawing the main value from a narrower range we draw a value-to-force from the narrower range, and then force-draw it from the full range. The choice of fewer bits is then cleanly deletable without changing the interpretation of subsequent bits.

[Liam-DeVoe]

We could do that! I'm fairly confident exactly what you stated, or some small variation, would work.

I was thinking of killing two birds with one stone here, though. Do you think the upweighting belongs in the ir or in st.integers()? If we're going to move it out of the ir eventually anyway, I think now is the right time to do it, both while it's causing problems and we're changing the weights interface.