VacuityFloors

How much searching a binding's generator has to do before its green counts for anything.

A lattice law is a statement about a set of states, so a green run says exactly as much as the pool it ran over. LatticeLawHarness measures four rates while it builds that pool and fails the binding when one falls outside these bounds — not because the type is broken, but because the evidence is too thin to say it is not. The measured values print on a green run too (LatticeLawHarness.measureVacuity), because a floor whose actual value nobody sees is a floor nobody notices drifting toward.

The pair definition, stated exactly

This is the one thing about these floors that must not be left to the reader, and it has already been read two ways: two independent measurements of ORSetConvergenceTest reported 66.7% and 30.4% strict ancestry over the same pool builder — a factor of 2.2, entirely definitional.

A "pair" is an ordered pair of distinct pool positions. For a pool of n states the denominator is n(n − 1) — (i, j) and (j, i) are two pairs, and (i, i) is not a pair. Both numerators are then counted over that same denominator:

• strict-ancestor counts (a, b) with a ⊔ b == b and b ⊔ a != a — a is strictly below b. Only one of the two directions of a comparable pair ever counts, so a total order reads 50%, not 100% — that is the ceiling, and IntMax's chain sits exactly on it.

• concurrent counts (a, b) with a ⊔ b != b and b ⊔ a != a — neither is below the other. Incomparability is symmetric, so both directions count.

The two are therefore related by 2 × strictAncestor + concurrent + equal = 100%, where equal is the pairs of positions holding the same value (a no-op step puts one in the pool). That identity is worth checking against any number quoted here: the design's controlled experiment reads 2 × 30.15 + 39.69 = 99.99, which is what makes its convention recoverable at all.

The alternative reading — count unordered pairs {a, b} in which either is a strict ancestor, over n(n − 1)/2 — is not wrong, it is just twice as large, and it loses the 50% chain ceiling that makes a total order legible at a glance. Everything here uses the ordered one.

The step rates

A step is one op the pool builder applied to a replica: every op of every critical shape, every replica's leading assert, plus every op of the random exploration. Absorbing a peer's state (the gossip draw) is not a step — it is not drawn from the alphabet and has no OpKind to classify.

The leading asserts are LatticeLawHarness.leadEveryReplicaWithAnAssert — one asserting op per replica, on any alphabet with something to retire, so that no replica takes its first exploration draw from the lattice bottom. They are constructed steps and count for the same three reasons the shape steps do.

Whether the constructed ops count is a real choice, and it moves the numbers a long way. ORSetConvergenceTest reads 8.6% no-ops counting them and 15.0% excluding them, on the same pool over the same seeds. The case for excluding them is that the harness already asserts every constructed step changed the state, so they are validated constants that dilute a ceiling and inflate a floor. They are counted anyway, for three reasons:

1. They are not free. A shape whose step does not move the state fails the binding outright, so a shape cannot be padding — declaring one is doing the work, not dodging it. The same check guards the leading asserts.

2. They are the design's own thesis. Constructed shapes are what reach the interesting configuration on every seed rather than on a lucky one. A denominator that excludes exactly the constructed part measures only the part this suite considers weaker.

3. Consistency with the pair rates. Ancestry and concurrency are measured over the whole pool, constructed states included. Excluding constructed steps would have one table describing two different populations.

The cost is that the default assert · retire · assert shape contributes about 9 points of retirement rate at these pool sizes — most of the 10% floor — so a binding must not be read as clearing the retirement floor on its shape alone. Every retiring binding does also clear it on exploration alone; the paragraph below gives that figure and says what it does and does not buy.

That margin is a property of the binding, not of the floor, and #2158 is the standing record of the difference. Since #2145 every retiring binding clears the 10% floor on its exploration retirement alone — the weakest is JsonCrdt at 11.5% of all steps over seeds 0..63, where before the leading asserts it was 10.0% and therefore had no margin at all. What has not changed is the floor's own discriminating power: the shape still contributes ~8.6 points of the 10%, so a mutant whose retirement is dead on two of three replicas still clears it (an ORSet shaped that way measures 17.0%). Read this floor as evidence about a healthy binding's generator, not as a detector for retirement that has died unevenly across replicas. What catches that shape is the no-op ceiling — see maxNoOpSteps, which is where #2145 left a debt and where it was paid.

• effective retire steps — steps whose op is OpKind.RETIRE and which changed the state. The and is the whole point: a remove of something absent is the lattice identity, and a generator can spend most of its budget there. This is the floor the design exists for; see OpKind for the controlled experiment showing it is the only one of the four that separates a searching generator from a vacuous one.

• no-op steps — steps of any kind that left the state unchanged. A ceiling, not a floor.

The no-op ceiling is per-binding, and on a retiring binding it is the load-bearing one

maxNoOpSteps defaults to 25%, which is a shared value and therefore pinned by whichever binding sits highest — GSet, at 24.7%. That makes the shared default nearly decorative on the twelve retiring bindings, whose healthy rates run 0.0% – 19.3% over seeds 0..15. Each of them declares its own instead, and the rule is:

The ceiling sits at the midpoint between the binding's measured healthy rate and the lowest rate it must catch, rounded to a whole percent.

The two rates it must catch are (i) the same binding with LatticeLawHarness.leadEveryReplicaWithAnAssert removed, and (ii) the same binding with retirement dead off replica 0 — #2158's shape. Where those sit so close to the healthy rate that no ceiling has two points on both sides, the constant targets the one it can separate and the binding's comment says which, with the numbers. Nine of the twelve pin the leading assert; eleven catch #2158's shape; VacuityBreakdownProbe (-Plattice.vacuity.breakdown=true) re-derives every figure.

This is the debt #2145 created, and the reason to read a lowered ceiling as different in kind from a raised one. Before the leading asserts, six retiring bindings caught #2158's mutant on this ceiling — ORSet 28.6%, CausalDotMap 28.9%, CausalDotSet 25.8%, Fugue/Rga 26.1%, TwoPhaseSet 40.0%, all over the 25% default. That was an accident: the mutant cleared the ceiling only because the healthy binding was itself wasting a fifth of its budget at the lattice bottom. #2145 removed that waste, healthy ORSet fell 20.3% → 8.6%, and the mutant fell with it to 21.7% — under the default, uncaught, on five of the six. The signal had in fact grown (11.7 points of excess against the healthy rate, up from 8.3); only the constant was in the wrong place. Raising a ceiling buys the number without buying the search, which is why the failure message says not to. Lowering one onto a measured healthy rate buys the search back.

The two waivers, and why they are shaped differently

totalOrder is a boolean, because "this pool is a chain" is a structural claim about the type — IntMax cannot be given concurrency by a better generator, and pretending otherwise would mean fabricating states it cannot reach. It waives the concurrency floor only; a total order still has to clear ancestry (it reads 50%), retirement and no-ops.

Having nothing to retire gets no boolean. Such a binding sets effectiveRetireSteps = 0.0 and says why in a comment — see NOTHING_TO_RETIRE. The asymmetry is deliberate: a growOnly = true flag would be reachable by deleting a binding's retiring op, and deleting the retiring op is exactly the mutation this floor exists to catch. Spelling the waived value out keeps the floor at its default on every binding that has something to retire, so removing that op reds it rather than quietly reclassifying it.

Parameters