Four properties for one codec

People think property-based testing is about generating random input. It is not. Random input is the easy part — Hypothesis does it for you, and does it better than you would. The skill is naming a property: a statement that must hold for every input, which you can therefore assert without knowing the answer in advance.

This problem removes the generator entirely so that only the skill is left. The samples are handed to you. Your job is the four predicates.

The system under test

A run-length codec over lowercase ASCII: "aaab" encodes to "a3b1". Five encoder/decoder pairs are given, under CODECS. Exactly one is correct; the others are the kind of thing that gets merged on a Friday. You do not know which is which, and you do not need to.

What to write

Four functions, each returning True when the property holds for sample:

def round_trip(encode: Encoder, decode: Decoder, sample: str) -> bool
def oracle(encode: Encoder, decode: Decoder, sample: str) -> bool
def length_preserved(encode: Encoder, decode: Decoder, sample: str) -> bool
def never_crashes(encode: Encoder, decode: Decoder, sample: str) -> bool

Each is one line of real content. The work is deciding what they say.

• round-trip — decoding an encoding returns the original. The archetypal property for anything with an inverse: serialisers, parsers, compressors, migrations up and down.
• oracle — the fast implementation agrees with naive_encode, a slow, obviously-correct reference that is provided. The classic move when you are optimising something that already worked.
• invariance — a quantity that survives the transformation. Here, the run lengths written into the encoding must sum to the length of the input. counts_in(...) parses them out for you.
• never crashes — the weakest property and still worth having: encoding then decoding completes without raising, for any input.

solve is provided. It runs each property over each sample and returns, per property name, the samples that violated it — in the order they were given.

A property that raises is a property that failed. The driver catches the exception for you and records the sample. That is Hypothesis’s rule too: an unexpected exception is a falsification, not a test error.

The lesson buried in the test cases

One of the five codecs passes round-trip, invariance and never-crashes for every sample, and is still wrong. It encodes with the letter upper-cased and lower-cases it again on the way back in — perfectly self-consistent, and producing bytes no other implementation on the planet will accept.

Round-trip alone cannot see it, because round-trip only ever compares your system against itself. That is why the oracle property exists, and why “we round-trip our serialiser in CI” is not the assurance people think it is when the thing on the other end of the wire was written by someone else.

Another test case runs a genuinely broken codec against a sample set that never triggers the bug — every property passes. A property is only as strong as the inputs it is offered, which is the argument for a generator, and the reason @given beats a fixture list once you have the properties right.