samplesReAssertAfterRetirement

A binding that can retire must keep a sample that re-asserts what an earlier sample retired — assert, retire, assert again.

That third state is the one a hand-picked sample list reliably lacks, and it is the one the interesting defects need: a value blended into an entry at join time survives a later retirement of the tag that carried it, and the survival depends on the order the operands were joined in (#2086). Without it, every law here passes on a lattice that loses writes — measured: ORMap's five samples found 0 violations against the broken type, and one added sample found 12.

This test is what stops that sample being deleted by a future tidy-up: a list that loses the shape fails rather than quietly passing.

What "loses the shape" has to mean, and why ordering alone cannot say it. Membership, distinctness and asserted ⊑ retired ⊑ reAsserted are satisfied by any three ascending writes, so a tidy-up that swaps the re-asserting sample for a put on an unrelated key — and updates retirementReAssertion to match, which is what a real tidy-up looks like — passed every one of them (#2157). The subject predicate the binding supplies is what closes that: RetirementReAssertion.shows must be true for asserted, false for retired, and true again for reAsserted. Nothing weaker distinguishes a retirement from an addition, because in the lattice they are the same move.

Still not checked here: that the re-asserted contribution is one the retired value does not dominate (see retirementReAssertion). That is an authorship judgement about which contribution comes back, not about whether the subject comes back, and it has no expression in terms the suite can evaluate.