fix(mgtt): carry facts compared with both a sibling and a constant - #3
Merged
Conversation
A pair of facts shares one cell. When a constant is also compared against either of them, an ordering alone cannot say it and two independent region domains cannot say the ordering — so the cell now carries a region per fact, cut by the constants applied to either, with the ordering falling out of comparing the two representatives. Regions gained bounds. A lone representative could not produce a second distinct value inside the same region, so the first cut let it escape: a member named below-0-more satisfied desired == 0. Pinned by a test that every member's values lie in the region it names. The storefront model now emits its draining states and declines nothing; 36 -> 64 situations.
The version field already refuses a document writ does not know. What it cannot catch is mgtt changing what a field MEANS while shape and version stay put, so a real export is committed and read end to end. Verified to fail when the propagation protocol is silently emptied. See mgtt's docs/decisions/0001-where-the-writ-bridge-lives.md.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the one known gap from #1 — the only one that cost coverage rather than merely reporting less.
The problem
A pair of facts compared with each other shares one cell. When a constant is also compared against either of them —
ready_replicas == desired_replicasalongsidedesired_replicas == 0— neither available shape works alone:fewer/equal/more) cannot saydesired_replicas == 0;ready == desired, because independent regions cannot decide it when both values land inside one region.Previously the ordering was emitted and the constant comparison refused, so the moves needing it were dropped and declined. Sound, but the storefront model lost its
drainingstates.The fix
The shared cell carries a region for each fact, cut by the constants applied to either, with the ordering falling out of comparing the two representatives rather than stored beside them — a stored ordering is a third fact that can contradict the first two. Combinations that cannot occur are not members: where the regions differ, which is lower already settles the ordering, so there is one member and not three.
Domains also gained an interpretation table (member → value). The old code read meaning back out of the member's name, which worked while a domain was one fact deep and stopped working when a member had to say two things at once.
A bug the tests missed, and now pin
Regions had a representative but no bounds. Representing "both in this region, left larger" as
(rep, rep+1)let the left value escape into the region above, so a member namedbelow-0-moresatisfieddesired == 0. It passed every coherence check I had written and was still a lie about what it named — I found it reading the generated model, not from a red test.Regions now carry inclusive bounds, and a test asserts that every member's values lie in the region the member names, in both directions.
Effect
On the storefront model: declines nothing (was three), emits its
drainingstates, 18 transitions rather than 13. The space grows 36 → 64 situations and 138 → 268 edges — more of the model is now represented — which is well inside the 200 000 floor of kernel-spec §14.make testgreen, 68 checks intest_mgtt.ml. Docs and README updated; measured numbers refreshed throughout.Needs mgt-tool/mgtt#6 alongside it, which refreshes the same numbers in mgtt's user-facing page.