No Duck Left Behind

The annual bathtub parade has twelve rubber ducks and three flotillas. Each duck arrives with a short biography; a model assigns every duck to adventure_crew, shore_crew, or ceremonial_crew and gives a reason.

Three specimens establish the tone:

D-03  Moby Duck          enormous, dramatic, afraid of deep water
D-07  Professor Waddles  wears spectacles and audits breadcrumbs
D-11  Quack Sparrow      tiny hat, unreliable around crackers

The complete roster lives in ducks.py. The sorter is represented by a frozen two-attempt fixture so the failure and recovery remain reproducible; the seam machinery around it is executable.

The first manifest looks plausible. Every row has a recognizable duck, a valid flotilla, and a fluent reason. But Professor Waddles is absent and Moby Duck appears twice:

duck_id,flotilla,reason
D-03,shore_crew,Afraid of deep water
D-03,ceremonial_crew,Has undeniable stage presence

The receiver cannot repair the omission. It can see that D-07 is missing, but choosing Professor Waddles's flotilla requires interpreting the biography the sorter was asked to judge.

Reconstruct the keystone at this return seam:

spec:       exact CSV shape + every supplied duck exactly once
assertion:  deterministic census returns bounded clause errors
recovery:   reject the manifest and re-dispatch with those errors

The nearest alternative is to let the parade coordinator patch the manifest. That makes the receiver a second sorter: it must invent Professor Waddles's assignment and choose which Moby Duck row to preserve. This example rejects the whole candidate instead.

The baseline stops after declaration:

duck biographies ──▶ sorter instructed to return CSV ──▶ coordinator trusts it

The contract is legible, but nothing at the seam distinguishes a complete manifest from one that merely looks complete. A twelve-row file can still contain eleven ducks.

The single structural shift is inserting an enforcing return seam whose failure has a declared recovery.

Spec

contract.py owns the mechanically expressible clauses:

EXPECTED_HEADER = ("duck_id", "flotilla", "reason")
ALLOWED_FLOTILLAS = frozenset(
    {"adventure_crew", "shore_crew", "ceremonial_crew"}
)
MAX_ERRORS = 3

Every supplied duck_id must appear exactly once, every flotilla must come from the allowlist, and every reason must be non-empty.

Assertion

checker.py parses the return, checks its exact header and field rules, then compares the returned ID multiset with the supplied roster. The first attempt produces a bounded report in contract vocabulary:

missing duck_id: D-07 Professor Waddles
duplicate duck_id: D-03 Moby Duck

The census can name both violations without deciding where either duck belongs.

Recovery

demo.py rejects that candidate and invokes the same sorting task again with the two errors. The fresh return contains one row for Professor Waddles and one for Moby Duck:

duck_id,flotilla,reason
D-03,shore_crew,Afraid of deep water
D-07,ceremonial_crew,Can audit the breadcrumb budget

The checker returns no errors, so the seam accepts the manifest. The receiver never authors a duck assignment.

The same roster and the same contract produce two candidates separated by one assertion:

attempt 1 ──▶ REJECT: D-07 missing; D-03 duplicated
                         │
                         └── bounded error report ──▶ fresh attempt

attempt 2 ──▶ ACCEPT: twelve ducks, twelve rows, twelve unique IDs

The declaration became operational. A failed clause now selects a defined recovery instead of becoming an inconsistency the coordinator works around.

Run the example from its directory:

python3 demo.py

The script asserts that the first return fails for exactly one missing and one duplicated duck, its report stays under the three-error bound, the sorter is invoked again rather than repaired by the receiver, and the second return passes. The checker is deterministic: the same roster, bytes, and contract produce the same verdict.

This proves only the clauses expressed in contract.py. It does not prove that Moby Duck belongs on shore crew, that Professor Waddles deserves ceremonial duty, or that every useful semantic clause was captured. It also does not license redispatch after external effects. Those are Verification Asymmetry and Effect Discipline questions; neither is part of this example.

No duck left behind; no duck counted twice. The spec names the acceptable crossing, the assertion distinguishes a candidate from it, and recovery gives rejection somewhere to go.

Rubber ducks are furniture. The three-role loop travels to ticket manifests, batch classifications, generated files, and return envelopes. What matters is that the assertion speaks the contract's clauses and that failure selects recovery at the seam.