OpKind

Whether an op asserts something new or retires something an earlier op asserted.

The test, stated once

An op retires when it takes an observation back without putting another in its place.

Read that off the type's observable value, never its encoding. remove, unset, leave and disable retire; MovableTree.move retires, because the node stops being under its old parent, even though the move log only grows. A register's set does not: it stops the old value being shown, but only by showing a new one in the same place. That is supersession, and the without-a-replacement clause is exactly what excludes it. PNCounter.decrement does not either — it adds to a second grow-only tally, and the earlier increment's contribution stays where it was.

This is the definition, and it is meant to be stated only here. A surface that classifies an op cites this section rather than re-deriving it — VacuityFloors.NOTHING_TO_RETIRE, a binding's alphabet comment, and across the module us.tractat.kuilt.conformance.QuiltedConformanceSuite.retirementIsMeaningful all do. Adding a fourth statement of it is the defect, not the documentation.

Where a surface may answer differently, and the only reason it may

QuiltedConformanceSuite.retirementIsMeaningful reads a register's set as a retirement — the opposite answer, on the same op, of the one above — and is right to. The licence is not about the op:

Classify strictly where the answer is averaged. A surface may classify generously where the answer is checked.

Here the answer is averaged, so a generous label destroys the measurement. VacuityFloors.effectiveRetireSteps is a rate over every step the pool builder took, and LatticeLawHarness.measureVacuity counts a step toward it when the op is RETIRE and the step changed the state. On an alphabet whose ops are all RETIRE those two counters partition the steps, so the retirement rate is identically 1 − noOpRate — pinned at ≥ 75% by the 25% no-op ceiling alone, and unable to come out low whatever the generator does. MVRegisterConvergenceTest's alphabet is a single set; declaring it RETIRE would clear its retirement floor by construction. That is the very vacuity this floor exists to catch, arriving through the classification instead of through the generator.

There the answer is checked, so a generous label costs an obligation instead. retirementIsMeaningful gates one constructed triple in which every step is asserted: the named subject must be shown, then not shown, then shown again. Reading supersession as retirement buys one more checked shape and can inflate nothing, because nothing is averaged — and if a register's set did not really stop the old value being shown, the guard reds rather than passes. Both surfaces are therefore right about set, for a reason each states where it declares.

Why the definition lives here

Because this KDoc has already been wrong about retirement twice. It claimed LWWRegister "has no removal at all" — false when written, since unset is a documented tombstone, and contradicted outright once #2142 bound an unset-high op as RETIRE; #2146 corrected it. Then this surface and surface 3 were caught shipping opposite tests for the same set on the same type (#2159). A definition restated in three places drifts in three places; stated once and cited, a surface that disagrees has to say why — which is the section above.

This cannot be computed; the binding has to declare it. A removal is more information, so s → s.remove(k) moves up the join-semilattice exactly as s → s.add(k) does, and s ⊔ s.remove(k) == s.remove(k) holds. There is no expression in the us.tractat.kuilt.crdt.Quilted algebra that separates the two.

The cheap proxy is a false detector in both directions. The harness already holds the serializer, so "did the encoding shrink?" is free — and wrong, measured over the live bindings as they stood when the proxy was evaluated:

A proxy that reads 62.1% on an alphabet where nothing retires and 0.0% on three where every retiring op does is not a weak signal, it is an inverted one. Hence the declaration.

(The 62.1% row is the reason to state this carefully rather than by type name. LWWRegister does retire — unset is a documented last-writer-wins tombstone, and LWWRegisterConvergenceTest now declares an unset-high op as RETIRE. What the row measures is the alphabet that produced it, a single set; the proxy called 62.1% of those steps retirements and every one of them was an assignment. Read as a claim about the type the row would now be false, and the number would be lost with it.)

Why it is worth declaring at all. A generator that never retires cannot reach the bug class this suite exists for, and no computable floor notices. Same broken ORMap, same harness, differing only in whether the generator could remove:

Ancestry, concurrency and join-non-triviality — the three a reviewer reaches for, and the three a generic Quilted can compute — are all satisfied by the arm that finds nothing. Concurrency and join-non-triviality even go up when the removes are deleted. The retirement rate is the only column that separates a searching generator from a vacuous one.

The asymmetry is a standing assertion, not only this table. VacuityFloorSelfTest (:kuilt-conformance's commonTest) runs the two arms live — the ORMapConvergenceTest harness as it stands, and that same harness with every RETIRE op filtered out of its alphabet — and asserts the vacuous one breaches the retirement floor while clearing all three others. It prints both reports, so the contrast is visible on a green run rather than only here.

The table is not re-derivable from its own description, and the self-test does not try to be. "Same generator, removes deleted" leaves the branch structure open, and the branch structure decides where the pool cap truncates — so it decides the triple and step counts. Four spellings were measured while closing #2152 and none reproduces both the published 47,059 triples and the published percentages; all four reach this same conclusion, which is what is pinned. (Note also that join-non-triviality was the probe's own measurement: the shipped fourth rate is the no-op ceiling, and VacuityReport carries no inner-join column.)