Repository navigation
An expected-red enrolment cannot hold an identity that never executes - #9036
gunbai-bot[bot] wants to merge 1 commit into
Conversation
Main's required run refuses with ExpectedRedIdentityDidNotExecute count=3, naming the three compile_accepted_unevaluable_program_control rows landed by #9022: primitive_call_with_extra_argument_must_refuse_at_compile primitive_call_with_missing_argument_must_refuse_at_compile primitive_call_with_wrong_argument_type_must_refuse_at_compile THE FILE DECLARES ReadsLiveTree, so it is DeclinedLiveTree: discovered, counted, and never run. The floor requires every enrolled expected-red identity to be OBSERVED AMONG THE EXECUTED CLAIMS, so enrolling an unexecutable identity makes the roster stale by construction. THE ENROLMENT'S OWN ANNOTATION ASSERTED THE OPPOSITE, and that is the defect worth naming rather than the three rows. It read "held here so that admission does not red main" -- believing enrolment protects a not-yet-planned identity. It does the reverse: the enrolment IS what reddens main. Nothing related the expected-red roster to the decline arm, and no carrier was consulted to check; the claim was that registering in A makes B behave, with B never named. That is the authority-substitution class DESIGN's recurring-failure-modes paragraph records, and this is a second receipt for it. IT WENT UNSEEN FOR A REASON WORTH RECORDING: an unrelated ArgvCommand seal break stopped strict preparation before the fold, so the roster check never ran. Fixing that break did not cause this one -- it revealed it. Two breaks from one landing, the second masked by the first. THE REPAIR USES THE EXISTING VEHICLE, not a new one. floor_expected_red_is_live already excludes rows kept for provenance but not currently live -- the mock-totality family uses it for exactly this. The three names join that exclusion; the chunk rows stay for provenance. DISSOLUTION IS A DELETION, NOT AN ADDITION: when the decline arm lands (gunbc#8977, gunbc#8982) and the file executes, remove the three exclusions. Nothing has to be re-added. WHAT THIS DOES NOT CLAIM. This repairs one roster, not the class. Nothing prevents the next author enrolling an identity that cannot execute -- the floor still catches it only at the end of a full run, and only when no earlier refusal masks the check. The next-rung trigger is enrolment deriving admissibility from the identity's own home disposition, so an unexecutable enrolment is unwritable rather than caught ~40 minutes later. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
Completeness join — this is the only instance of the class, not a sampleThe three identities in this PR were found because they reddened main. That says nothing about whether others of the same shape are enrolled and waiting to surface, so I joined the two populations directly rather than assuming. Method: every identity enrolled in Result: exactly one intersection. That is the module this PR excludes. No other enrolled identity is declined, so there is no fourth break of this class queued behind the merge. Why that matters for sequencing: today's failures have surfaced one at a time, each revealed by repairing the one in front of it — the What this does not cover, stated so the join is not read as broader than it is:
— sent from smart-ram-730 |
Nothing to push — this failure is the other half of a two-PR deadlock, now measured on both sidesThe failing check is the floor phase, and every error in it is the
The deadlock is now confirmed from both directions, not inferred
Each PR's run shows its own fix landing and dies on the break the other one repairs. Both are cut from Both are approved, What I am deliberately not doingI could merge #9031's one-line change into this branch and manufacture a green. I have not, because fusing two unrelated repairs into one vehicle makes each harder to revert independently, and these have genuinely different causes, owners and dissolution conditions — one is a call site that predated a seal, the other an enrolment that asserted the opposite of what the floor does. The precedent set earlier today was to merge a mutually-blocking set together rather than fuse it. That is an operator action, and it is where this sits. One thing that de-risks the mergeA completeness join posted above establishes that this is the only instance of its class: 203 enrolled expected-red identities against 158 modules declaring — sent from smart-ram-730 |
|
Closing: consolidated onto #9031, which now carries this exact change to The reason for consolidating rather than leaving both open is that neither could go green alone. Main's floor refuses at compile on the argv break before any witness executes, so the stale enrolment here was masked; and this change alone leaves that compile refusal in place. Two PRs answering for one merge is the duplication that makes a green run ambiguous about which fix produced it. Verified on #9031 head |
Main is red on a stale expected-red roster
Required CI on
mainrefuses with:These three were enrolled by #9022. Their file declares
ReadsLiveTree, so it isDeclinedLiveTree— discovered, counted, and never executed. The floor requires every enrolled expected-red identity to be observed among the executed claims, so an enrolment for an unexecutable identity is stale by construction, not by drift.The defect is the belief, not the three rows
The enrolment's own annotation said the enrolment was protective:
That is backwards. Enrolment does not shelter a not-yet-planned identity — it is the thing that reddens main. Nothing in the tree relates the expected-red roster to the decline arm, and no carrier was consulted to check: the claim was that registering in A makes B behave, with B never named.
That is the authority substitution class from DESIGN's recurring-failure-modes paragraph, and this is a second receipt for it. The tell is exactly the one the class describes — a sentence of the form "I registered it in A, so B now does X" where B never appears.
Why it went unseen
An unrelated
ArgvCommandseal break stopped strict preparation before the fold, so the roster check never ran. Repairing that break (#9031) did not cause this failure — it revealed it. Two breaks from one landing, the second masked by the first, which is the same masking shape that hid downstream defects behind an annotation break earlier today.The repair uses the vehicle that already exists
floor_expected_red_is_livealready excludes rows kept for provenance but not currently live — the mock-totality family uses it for precisely this case. The three names join that exclusion. The chunk rows stay for provenance, so nothing is lost.No new mechanism, no second roster, no parallel authority.
Dissolution is a deletion, not an addition
When the decline arm lands (#8977, #8982) and the file executes, remove the three exclusions. Nothing has to be re-added, and the removal is the signal that the class closed.
What this does NOT claim
This repairs one roster, not the class. Nothing prevents the next author enrolling an identity that cannot execute. The floor still catches it only at the end of a ~40-minute run, and only when no earlier refusal masks the check — which is exactly what happened here.
Next-rung trigger: enrolment deriving admissibility from the identity's own home disposition, so an unexecutable enrolment is unwritable rather than caught forty minutes later.
Test plan
ExpectedRedIdentityDidNotExecuterefusal must not recur. Note the branch still inherits Convert the one ArgvCommand site the seal missed, through a builder rather than by widening the seal #9031's argv fix requirement and the observedrustfmt: Text file busyregen race, neither of which is this PR's.🤖 Generated with Claude Code