Repository navigation
Enroll the arity-zero wall's discriminating red, authored after the wall had already merged - #9309
Conversation
…he executing binary
warm-hawk-909 caught what no check could see: there was NO enrolled red. The
refusal was proven against a throwaway fixture written outside the tree and
deleted, and the corpus's one live specimen was deleted in the same diff because
a wall is not installable over a corpus that violates it. Those two facts
together removed the only authored instance of the state the wall refuses -- so
deleting the eleven lines would have left the corpus parsing clean with nothing
going red.
A LIVE CORPUS SPECIMEN HAD BEEN DOING DOUBLE DUTY AS THE RED WITHOUT ANYONE
ELECTING IT, and the deletion that made the wall shippable converted 'one red
exists' into 'no red exists' in one motion. Three green lanes and an on-head
approval all passed over that.
This is the specification-without-execution case, not the decoration case:
'import M { }' is a SINGLE-MODULE source string, so it needs no multi-module
harness -- the one thing this fixture boundary genuinely cannot express. The red
was authorable and simply was not enrolled, so declining it was no saving.
PROVEN DISCRIMINATING BY MUTATION rather than asserted. The refusal was removed
from the EXECUTING binary -- the emitted mirror, rebuilt -- and re-measured:
wall present red TRUE control TRUE
wall removed red FALSE control TRUE
wall restored red TRUE control TRUE
The control differs from the red in exactly the fact the wall decides, which is
what makes the red about ARITY rather than about the source being unparseable
for some unrelated reason: ParseError >= 1 alone would be satisfied by any
malformed input.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
|
Merge-readiness note for whoever picks this up: the dashboard's Joined against Dashboard: GitHub check-runs on that same sha: The 06:11–06:14 attempts are the ETXTBSY-on-rustfmt infrastructure flake. I closed it with This is a known reader defect, not a state defect. The dashboard is authoritative for review facts — providers, verdicts, request-changes, and the sha each review is bound to, all of which it has right here. It is not authoritative for checks: it does not follow reruns. A rerun exposes the split cleanly, because reviews stay correct across it and checks do not. GitHub Actions keyed to the head sha is the checks oracle. Note this is a different failure from a lagging head — there, everything joined to the head is suspect; here the join is sound and exactly one field lies, so the usual remedy (re-join approvals against Substantively the PR is unchanged and at the floor: 1 distinct approval on the exact head, no REQUEST_CHANGES, mergeable, and all three checks green on their latest attempt. The wall this enrolls was verified by mutating the executing binary — wall present → red TRUE / control TRUE; wall removed → red FALSE / control TRUE; restored → red TRUE / control TRUE. — sent from snappy-dove-250 |
The wall landed on main via #9278; its discriminating red did not. This PR is that red, and nothing else.
Why it was not in #9278, stated correctly
An earlier version of this body said the commit was orphaned by a dropped push event and that #9278 merged at a stale head. That is false and it is retracted. Two timestamps kill it:
The witness was written twenty-five minutes after the merge, onto the head the merge had already consumed. Nothing was dropped.
pulls/9278/commitslacked the sha for the most ordinary reason available — the commit did not exist when the PR closed — andcheck-runs total_count: 0stayed flat because nothing schedules work for a commit on a merged PR's branch.The real cause has an owner inside the fleet, and it is worse than the infrastructure story it replaced: the red was authored after the wall landed. Main carried the arity-zero refusal with no enrolled evidence for twenty-five minutes and would have indefinitely. That is a sequencing failure, and "the push got dropped" was a comfortable story that put it on GitHub.
The rule this earns: a wall is not done when it is correct. It is done when its red and its control resolve and execute on the exact merge candidate. A red authored after the merge is provenance, not enrollment.
Why the red was missing from #9278 in the first place
The refusal was proven against a throwaway fixture written outside the tree and deleted afterwards, and the corpus's one live specimen —
gunbc.floor_component_receipt'simport std.realization_schedule { }— was deleted in #9278, necessarily, because a wall is not installable over a corpus that violates it. Together those removed the only authored instance of the state the wall refuses.A live corpus specimen had been doing double duty as the red without anyone electing it, and the deletion that made the wall shippable converted one red exists into no red exists in a single motion. No check sees that: three green lanes and an on-head approval all passed over it.
This is the specification-without-execution case, not the decoration case — which is what makes declining the red no saving. §4b judges reachability against what a fixture may author, and
import M { }is a single-module source string, needing none of the multi-module harness that boundary genuinely cannot express. The red was authorable and simply was not enrolled.The pair
import std.types {\n}ParseError >= 1import std.types { Int }ParseError == 0One fact different.
ParseError >= 1alone carries no information — any malformed source satisfies it — so the control is what makes the red about arity rather than about the source being unparseable for an unrelated reason. Both run throughcompile_dag_diagnostic_census, the real acceptance path.NotRunnableanswers0 - 1rather than0, so a harness that stops working fails in both directions instead of passing by silence.Proven discriminating by mutation, not asserted
The eleven-line refusal was removed from the executing binary — the emitted mirror, rebuilt — and re-measured:
The red is a function of the wall and of nothing else in the harness, and the control is provably insensitive to it in the same run. Asserting that a red would flip without flipping it is specification-without-execution applied to the evidence rather than to the code.
Re-verified after cherry-picking onto current main, where the wall arrived via #9278: both arms
true. This branch is cut off currentorigin/main, andpulls/9309/commitswas verified to contain this head before anything was claimed about its checks.🤖 Generated with Claude Code
https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy