Repository navigation
Wire generic type argument inhabitance - #10226
Merged
Merged
Conversation
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
Settles whether PR #10265 carries content. The branch's work landed on main via the #10156 squash, so every path is already byte-identical there; this merge takes main's forward movement, including #10226's EffectRealizationKey at effect_demand.dag, which the stale branch would otherwise point backwards. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE
briansrls
pushed a commit
that referenced
this pull request
Sep 3, 2026
…: eight refusals, eight repairs The floor did not judge a claim and find it wrong. It REFUSED during strict preparation -- phases_run=3 phases_failed=1, no required-floor summary line at all -- so nothing here executed. SEVEN of the eight are #10226's new wall catching pre-existing mismatches that had no obligation producer until this evening. Three test helpers were declared -> List<String> while observed_ruleset_divergences returns List<RulesetDivergence>, and every call passing one to render_divergences was a generic-argument mismatch nothing had ever judged. The declared type was simply wrong and had been wrong since before this branch; the wall's first outing in the wild found it. Fixed at the declaration rather than at the seven call sites, because the call sites were correct. THE EIGHTH IS MINE AND IT IS NOT THE KNOWN if-JOIN FALSE POSITIVE, which I checked rather than assumed because the shape is identical to the defect filed in #10232. That defect makes a WELL-TYPED construction fail: the join compares branches against each other and never against the declared return context. Here the construction is not well-typed under either rule. concat yields String, the declared payload is NonEmptyStr, and String does not inhabit NonEmptyStr -- so a join that DID consult the declared return would refuse this too, for the same reason. The repair is the cast the corpus already uses for a concat whose first operand is a non-empty literal, and it is safe by construction rather than by check. Both refusal messages take it, not just the one the floor reached. The second was on the same path and would have refused on the next run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 4, 2026
…ission, the merge_queue ruleset rule, and a sign-off gate on the live change (#10204) * Model the merge queue the substrate already declares: merge_group admission, the merge_queue ruleset rule, and a sign-off gate on the live change gunbc.repo_ruleset states that strict_required_status_checks_policy is false BECAUSE the merge queue is the construction that establishes the same invariant without re-running the floor for every PR behind a merge, and that the queue is not configured yet. The workflow already lists the merge_group trigger. Nothing declared the queue itself, so "turn it on" was a web-form change nobody in this repository could see -- the exact condition the ruleset module exists to end for the required context. Three things land, and no live setting is touched. 1. extdeps.github.rulesets gains the merge_queue rule: the MergeQueueRule tag, the two SCREAMING wire enums (grouping strategy, merge method) parsed into closed coproducts with unrecognized arms, and MergeQueueStanding with the same three states RequiredStatusCheckStanding has -- absent, configured, and more-than-one-refuses. Interface shape only; no policy. 2. gunbc.repo_ruleset declares the proposal with the SIGN-OFF IN THE TYPE. MergeQueueDesire is MergeQueueUnsigned | MergeQueueSignedOff, and only the signed arm yields a policy. Desired state here is ACTUATED -- converge PUTs the whole ruleset -- so writing the queue into desired_ruleset_rules would enable a merge queue on a live repository on one worker's edit. Under Unsigned the settings are declared, readable and diffed against the live ruleset, and contribute no rule to what converge sends. A live queue nobody signed off is reported with its grouping strategy, because an undeclared ALLGREEN queue and an undeclared HEADGREEN one are different guarantees. The same change closes a hole found while modelling it: the divergence fold only asked "is every declared rule present". The PUT is a whole-ruleset replace, so a rule that exists live and is absent from desired was DELETED by the next converge run with no divergence reported before or after -- the read-back compares against the same desired that dropped it. That is not a divergence to repair, because applying desired is what destroys it, so converge now REFUSES rather than writing (verify still reports it). 3. gunbc.merge_queue_admission models what a queue must satisfy: the exact-subject identity (the checked composition IS the commit that lands), the ordering chain (entry 0 onto the observed target tip, entry N onto entry N-1 -- which is what breaks when main moves under the queue), and the grouping strategy, which is where ALLGREEN and HEADGREEN answer differently. It carries the two terminals as separate constructors. MergeQueueOperational is "the queue can do its job"; MergeQueueExclusive is "no route around admission survives". Operational does not imply Exclusive -- a bypass standing leaves a route past every check while the queue runs correctly beside it -- and reporting the second on the first's evidence would be rung inflation on the axis a queue is adopted for. The type makes it unwritable. WITNESSES. Both files carry a positive control plus discriminating reds: an all-green chained queue admits, and the same queue admits nothing once only the observed tip differs; a green entry whose composition is not what lands is refused by identity; ALLGREEN and HEADGREEN are shown answering the SAME queue differently; the unsigned proposal is shown contributing no rule; and the actuation refusal fires on a merge_queue rule while not firing on the rule list this repository declares. LIVE READ-BACK, and what it did not establish. Read 2026-09-03 against gunb-ai/gunbc ruleset 16178731: rules are deletion, non_fast_forward, required_status_checks -- so merge_queue_standing is NoMergeQueueRule, merge_queue_divergences is empty under the unsigned desire, the actuation refusal does not fire, and merge_queue_terminal is Unconfigured. The repository now allows squash only (allow_merge_commit and allow_rebase_merge both false), which is why the proposal's merge method is SQUASH. bypass_actors is omitted from the response and current_user_can_bypass reads never FOR THIS READER, which is reader-relative by the module's own annotation -- so this read cannot establish Exclusive in either direction, which is precisely why Exclusive is a separate terminal rather than a field. The documented actuator route `gunbc run --entry .../repo_ruleset.dag --function verify` does not execute today: it refuses with ~3124 resolution diagnostics. Measured identical on origin/main in a detached worktree, so it is pre-existing and not introduced here; the live read above went through the same REST endpoints the model declares. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Fix the parse error, carry the units in the domain, and derive the queue timeout from the floor's own envelope The parse failure first: `grouping_strategy:` had its value on the next line in merge_queue_standing, which is not a field-value form the parser admits (rulesets.dag:331:29, "expected expression, found Newline"). Every "source annotation names no subject" line in that CI log is downstream of it. A local `gunbc compile` did not catch it -- the installed binary predates main's head -- so CI was the first honest reader. REVIEW 59188 (codex/gpt-5.6-sol), unit modelling, ACCEPTED AND FIXED. The reviewer is right that bare `Int` for minutes and for entry counts is a second authority beside std.measure. Applied along this module's own stated split: the WIRE stays bare, because GitHub sends plain JSON integers, and the DOMAIN does not. MergeQueueStanding and MergeQueuePolicy now carry `Minute` and a `MergeQueueEntryCount = Measure<Count, One, Nat>`. The distinction is load-bearing rather than cosmetic -- all six of those fields are bare integers on the wire, and only the carrier stops a wait in minutes being compared against a count of entries. THE TIMEOUT IS NOW DERIVED, WHICH IS THE POINT THE REVIEW EXPOSED WITHOUT NAMING. It was a transcribed 180 whose annotation claimed it came from the floor lane's job timeout. That is precisely the second authority the same review objects to, one level up: two numbers that must not drift apart, with no edge between them. `witness_floor_workflow` gains ONE row -- witness_floor_lane_timeout_minutes, value unchanged, the emitted YAML byte-identical -- and repo_ruleset reads it and adds a declared margin. The witness asserts the ORDERING, not the number, so raising the floor's timeout cannot silently invert it. A queue whose response timeout sits below the repository's execution envelope dequeues green work for being slow, which is a manufactured failure, not a real one. MergeQueuePolicy carries the COMPLETE documented parameter set, stated in the type's annotation: a `merge_queue_required: Bool` would say "queue on" while seven unmodeled parameters decided what the queue does, with provider defaults standing as the second authority. THREE CARRIER STATEMENTS, each because it was doing real work only in a message. Do not enable the queue in the GitHub UI, at the sign-off row where a future operator will be tempted: this module PUTs the whole ruleset, so a UI-enabled queue rule is unmodeled and the next converge run would delete it. A UI flip is not a shortcut past the model, it is a change with a scheduled silent self-reversal. The queue is not the shared-row remedy, as a stated non-goal: it composes trees, not two edits to one multi-kilobyte authority row. Receipt 2026-09-03, #10194 merged and knocked two sibling PRs DIRTY on one generated projection. The one-row/one-writer rule stands. The bounded gap, with its trigger, as a DissolutionCondition rather than a caveat: nothing here proves the required aggregate executes on a real merge_group composition, because no queue exists to compose one. The in-repo half is witnessed from the workflow authority; the world half dissolves on the signed flip plus one observed merge_group run whose subject commit equals the composition GitHub fast-forwards. And the bypass status is recorded as UNDETERMINED-BECAUSE-UNREADABLE, not as either answer: three reads on 2026-09-03 returned two results, the field is reader-relative, and no reader available here settles it. That is the shape MergeQueueExclusive exists to hold. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Move MergeQueueEntryCount to std.measure beside its Count siblings Review 59197 (claude/claude-opus-4-7) is right, and it caught the annotation contradicting the placement: the comment argued that std.measure already owns count-at-unit-scale and then minted a fresh alias for it in an extdeps module, which forks that axis once per upstream that happens to count something. MergeQueueEntryCount and its two accessors now live in std.measure beside HardwareThreadCount, CharacterCount, TokenCount and Millicore, and every consumer -- extdeps.github.rulesets, gunbc.repo_ruleset, both witness files -- imports them from there. No values change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * The rule parameters record must carry both rules' readable shapes, because the transport cannot answer a coproduct CI on ded1329 refused with seven `no field 'X' on type 'RulesetRuleParametersWire'` errors: `parameters` was statically typed to the required_status_checks shape, so merge_queue_standing could not read the fields GitHub sends for a merge_queue rule. The shape that says what GitHub actually sends is a coproduct discriminated on the rule's `type` tag. It cannot be READ. The REST realization decodes a nested object into an untagged map and this record is a static read-shape over it, so a coproduct arm would have no constructor tag to match on and every read would refuse. So the record becomes the UNION OF THE READABLE SHAPES -- what the transport can actually answer -- and the module states why rather than leaving it to look like a flat-record preference. That is safe only because of an invariant now written down: every read guards on the type tag first. required_status_check_standing and merge_queue_standing each `filter` on the rule type before touching a field, so no field is ever read off a rule whose parameters object does not carry it. The guard is load-bearing, so it is named as such, with a next-rung trigger stated as a capability -- a transport decode that carries a discriminator from the enclosing object into a tagged value, at which point the coproduct becomes readable and the guard becomes unnecessary instead of required. required_status_checks_rule keeps omitting the merge_queue fields, also stated: it builds the rule GitHub is SENT, and supplying zeroes for seven scheduling fields GitHub does not accept on a required_status_checks rule would be a fabricated value on the wire. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Commission max_entries_to_build at 1, with the rise to 5 as a trigger rather than a note Operator ruling via the lane manager: the commissioning value is 1, and 5 is the intended change gated on receipts showing the one-entry protocol converging. The argument for 5 stands on its own -- building ahead of the head is what makes a candidate already validated when the head merges, and it does not weaken ALLGREEN -- and it is withheld for a reason that is not about throughput. With five compositions in flight, a failed commissioning run says which of five candidates was involved rather than which protocol step failed. A queue is adopted to make landings deterministic, so starting it at its throughput setting instead of its legible one inverts the thing being commissioned. Throughput is recoverable later; a muddled first receipt is not. Written as a DissolutionCondition rather than a TODO so it is retired by evidence -- entries composed, the required aggregate executing on each composition, successful candidates advancing -- and not by someone remembering. The row states that this is a legibility bound on commissioning, not a claim that 1 is the right steady-state value. A witness asserts the commissioned 1, so it cannot be raised without touching the assertion that names the trigger. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Split the reader's bypass standing from the ruleset's bypass roster, and record the always-bypass actor that settles the question Separate Operational and Exclusive constructors did not close the defect, because the EVIDENCE used to reach Exclusive answered the wrong quantifier. current_user_can_bypass is a fact about the READER; "no route around admission exists" is a fact about the RULESET's bypass_actors roster. One carrier let the first masquerade as the second. Two carriers now, named for their subjects. ReaderBypassStanding is ThisReaderCannotBypass / ThisReaderCanBypassPullRequestsOnly / ThisReaderCanBypassAlways / unrecognized -- the same four inhabitants review 56496 established must stay apart, renamed so the spelling stops naming the ruleset. BypassActorRosterObservation is BypassRosterObserved { actors } | BypassRosterUnavailable { reader, cause }. AN ABSENT bypass_actors KEY IS UNAVAILABLE, NEVER EMPTY. GitHub omits it both when the roster is empty and when the reading credential may not see it, and the response carries nothing separating those. So the field is deliberately NOT decoded onto RulesetWire -- adding it would decode absence to an empty list, which is the exact conflation -- and every observation built from that endpoint is Unavailable, carrying who asked and why. Only a complete, authorized observation of an EMPTY roster may contribute to Exclusive, and there is no path from Unavailable to `none` in first_bypass_route, so an unauthorized read cannot mint the claim by construction rather than by care. WHY A QUEUE IS NOT EXCLUSIVE IS ITSELF A COPRODUCT: AlwaysBypassActorObserved, PullRequestBypassActorObserved, BypassRosterNotObserved. Three remedies -- revoke the grant, revoke the narrower grant, obtain an authorized read -- and only the third is about evidence rather than about the world. An unrecognized bypass_mode reads as the WIDER grant, fail-closed. AND THE QUESTION IS SETTLED IN THE POSITIVE DIRECTION. A privileged observation reports an always-bypass actor on ruleset 16178731: actor_type RepositoryRole, actor_id 2. The paragraph claiming no available reader could settle it is stale and is replaced: Exclusive for this repository is not unproven, it is FALSE while that grant stands. Four witnesses carry it -- observed-empty is Exclusive, an unavailable roster cannot mint Exclusive and keeps its cause, the observed RepositoryRole 2 always-grant holds the terminal at Operational, and the two grants plus an unreadable mode do not collapse. RepoRulesetConvergedEvidence.bypass_is_never becomes reader_cannot_bypass, for the same reason: it was computed from the reader-relative field while its name claimed the roster. Merged origin/main 1ea6a94 first. The emitted witnesses.yml is byte-identical to that main -- naming the subject this time, which is what I left out before. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * A record literal must be complete, so the merge_queue wire fields are optional — and an incomplete rule refuses instead of defaulting CI on f7d0c06 refused with seven `missing required field ... in literal of type RulesetRuleParametersWire`. The behaviour I relied on -- that an omitted optional field is unwritten and only refuses at the read -- is not what this compiler does for a record literal: every declared field must be supplied. So `required_status_checks_rule` could not build its rule without inventing seven scheduling values GitHub does not accept on a required_status_checks rule. The merge_queue fields become optional and the constructor passes `none`, which is the true statement: this rule carries no merge-queue parameters. The required_status_checks fields stay mandatory, because a rule of that type always carries them -- the union now says something about presence rather than only about shape. That gains a wall rather than only fixing a build. merge_queue_standing REFUSES on a merge_queue rule whose parameters arrived incomplete -- MergeQueueParametersIncomplete { missing } -- instead of reading zeroes, so a truncated response cannot present as a configured queue. It surfaces as its own divergence naming the absent fields, and as Unconfigured at the terminal, because "a queue is configured" and "a queue is configured and we could not read what it does" are different facts. This is the second half of the type-tag guard: the tag says which fields to expect, the optionals say whether they came. Two witnesses: an incomplete rule names exactly the two absent fields and not the present one, and the rule this repository actually sends reads back as NO queue rather than an incomplete one. STATED, NOT ASSUMED: how the REST body serializer renders an absent optional in the PUT is not established by this change. If it emits explicit nulls, a converge run would send seven null keys on a required_status_checks rule and GitHub may refuse the body. No CI step exercises converge, so it has not been observed either way; the annotation says so rather than implying it works. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Brace interpolation in a diagnostic string: reword rather than escape CI on e4d38a4 refused with one error -- `undefined variable 'id'` at rulesets.dag:275. The cause string spelled the endpoint as /repos/{owner}/{repo}/rulesets/{id}, and braces in a string are interpolation, so the compiler read {id} as a variable reference. The service block escapes its path templates for the same reason. Reworded to name the endpoint in prose rather than escaping the braces: this is a human-facing cause carried in a refusal, and the ESCAPED form would still read as a path template a caller might copy. The path itself is already declared once, in the operation's transport block, which is the authority for it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * The two duration rows become Minute, and the unit disappears at the boundary rather than in the model Review 59242 (claude/claude-opus-4-7, non-blocking) is right and the diagnosis is exact: `witness_floor_lane_timeout_minutes` and `merge_queue_response_margin_minutes` were bare `Int` purely so that `+` type-checked, in a diff that is otherwise scrupulous about carriers. A duration kept as a scalar to make arithmetic convenient is std.measure's authority declined for the author's convenience. Both are `Minute` now, and the sum goes through `measure_add` rather than through raw integers. The unit disappears exactly once, at the Actions boundary: the job field is an Int, so the projection unwraps with `minute_count`. That is the right place for it -- the YAML key `timeout-minutes` carries the unit in its spelling, while the value handed to a second consumer in this repository carries it in its type. No emitted bytes change: minute_count(minute(count: 180)) is 180. The ordering witness compares two Minutes by their counts rather than a Minute against an Int, so it keeps asserting the relation and not a literal. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Regenerate the stage0 mirror for the std.measure addition The build lane refused: `regen FAIL generated surface drift: std_measure.rs`. Adding MergeQueueEntryCount and its two accessors to `dag/std/measure.dag` moves the emitted stage0 Rust with it, and that mirror is committed. Regenerated with the producer rather than hand-edited: claim_executor --required-regen over both source roots, and the drifted file taken from the candidate it wrote. Re-run over the updated tree reports `first_generation_equal=true`, which is the check the lane makes -- so this is the emitter's output, not a plausible transcription of it. The +13 lines are the MergeQueueEntryCount alias and its constructor and accessor, in the position the .dag declaration order puts them: beside TokenCount and its pair. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Read the trigger row, not the whole Workflow, so the terminal witnesses stay inside the floor's CPU budget The floor refused with five INTERRUPTED-BEFORE-VERDICT rows, all at cpu_at_least ~501-507ms against the 500ms per-claim budget, and all five are the witnesses that reach merge_queue_terminal or floor_workflow_admits_merge_group. The cause is one field access. `witness_floor_workflow.on` forces the whole Workflow value -- every job, every step, every expression -- to answer a question about four trigger constructors. `witness_floor_triggers()` is the row the workflow's `on` block is assembled FROM, so reading it is not a shortcut past the authority: it is the same authority without the jobs attached, and deleting the merge_group trigger still drops the terminal. Worth naming as a shape rather than a tuning fix: a cheap question asked through an expensive carrier costs the carrier, not the question. Nothing about the witnesses changed -- five of them were paying for the CI workflow's entire job graph to ask whether a four-element list contains a constructor. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * The wire receipt exists, and signing off without wiring the projection now stops the line TWO THINGS, both closing gaps this PR had stated rather than resolved. THE SERIALIZER QUESTION IS ANSWERED BY EXECUTION. The PR said it was not established whether an absent optional in the shared parameters record is omitted from the PUT body or sent as an explicit null -- a wire fact a converge body depends on, and an actuation prerequisite for the sign-off. It now has a receipt: cli_run wire_body_omits_absent_optional_record_fields serializes a record carrying one present and one absent field through the same value_to_wire_json the REST body goes through, and requires the body to contain exactly the present one. The control is the same record with the field PRESENT, so a serializer that dropped everything cannot pass it. It runs in the required unit lane. So a required_status_checks rule sends its own three keys, not seven nulls. Reading the two mechanisms would have suggested the same answer -- the record arm skips nulls, `none` is the host null carrier -- and that is precisely why the test exists: a mechanism argument about a wire is not a wire receipt. SIGNING OFF WITHOUT WIRING THE PROJECTION NOW REFUSES. Review 59298 flagged, as a don't-forget, that desired_ruleset_rules appends no merge_queue rule under either arm. The consequence is worse than a forgotten follow-up: the day the arm flips to MergeQueueSignedOff and nothing else changes, converge would PUT a ruleset with no queue in it while verify reported a MergeQueueRuleAbsent divergence no apply could ever clear -- a signed policy silently not in force. Converge now stops the line and names what is missing, so the flip fails loudly at the moment it happens rather than being remembered. The check takes the policy as an OPERAND, which is what makes its RED authorable: the signed state does not exist in this tree, so a check reading the desire row alone would be permanently green by construction and would be cited as coverage while asserting nothing. The witness hands it the proposal as though signed and requires the refusal; the control passes an unsigned desire and requires none. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * The five interrupted claims were one cost SHAPE, and the roster had no row for it The crossing test came first: gunbc.recurring_failure_mode carries no cost-shape class today -- nothing about forcing extent, demanded grain, or a carrier priced above its consumer -- so this is a new row and not a second authority beside a standing one. The class: a claim needs one narrow fact and reaches it by naming a carrier that must be forced whole to yield it. floor_workflow_admits_merge_group read the FIELD witness_floor_workflow.on, forcing the entire Workflow value to answer a membership test over a four-element list, while the narrow producer sat beside it -- witness_floor_triggers(), which the workflow's own on: is bound to, so reading the function is not a copy of the authority but IS the authority. The harm is that the cost is charged to the QUESTION. Five claims crossed the 500ms per-claim CPU deadline and were reported as interrupted_before_verdict, which is not claims_failed: the PR goes red with a disposition naming no failing claim, and the author looks for a defect in logic that has none. The measurement is the row's content, and it is a shape rather than a magnitude: 501 -> 35, 501 -> 82, 502 -> 86, 507 -> 109, 505 -> 154, from run 33754056276's own required_floor_claim_cost.tsv at cost_basis=cpu. On the lightest, ~465ms of a 501ms claim was carrier and ~93% of the cost answered nothing the claim asked -- the CHEAPEST question paid the most, because forcing cost is denominated in the carrier while the question's own work is what varies. Rung mitigatable, stated honestly: nothing refuses a field read whose forcing cost exceeds its consumer's demand, and the cost ledger is a detector that fires only after the claim is authored, enrolled and interrupted -- which is why these five were found by a red and not by review. The next-rung trigger names the capability and not an artifact: a demanded-extent producer, sufficient to refuse or narrow a read that forces strictly more than its consumer observes. The cost line is explicitly not that trigger; a line separates expensive from cheap and says nothing about whether the expense was demanded. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * chore: regenerate drifted generated artifacts (ci auto-heal) * The wall now compares the RAW WIRE FIELDS of the projected rule, not a value lifted out of it The first form of this check asked whether the desired rule-TYPE roster contained a merge_queue entry. Two defects, one inside the other. The roster was a second hand-maintained list beside desired_ruleset_rules -- one fact with two authorities, agreeing by diligence. A rule added to the projection without a matching hand-edit was invisible to every reader of the roster. It is now derived: ruleset_rule_types(rules: desired_ruleset_rules()). The deeper one is that a rule TYPE says nothing about the seven parameters that decide what the queue does. A merge_queue rule projected with the wrong strategy carries the right type and the wrong queue, and the check passed on exactly that input. The second form compared against merge_queue_standing(rules) -- the reader that interprets a live GET. That is not a JSON round trip, but it is still a value lifted out of the subject: it compares the policy to the result of a parse rather than to what the PUT carries, which is the roster defect one layer down. This form walks the projected RulesetRuleWire list itself and compares each declared setting, rendered to the spelling GitHub is sent, against the exact optional the serializer receives. The policy side goes through the wire labels because a declared AllGreenGrouping and a projected "ALLGREEN" are only comparable in one vocabulary, and the upstream's own spelling is the one that lands in the body. One value, two consumers, neither reading the other's output as evidence: the admission check asks whether this policy is correct, of the typed list; wire_body_omits_absent_optional_record_fields asks whether that typed list reaches the wire intact. The structural arms mirror merge_queue_standing deliberately -- absent, ambiguous, incomplete, then the field walk -- because the two must agree about what a well-formed projection is even though they answer different questions, and where they would disagree the disagreement is the finding. WHY THE PROJECTION STILL CARRIES NO QUEUE RULE, now stated as a structural blocker rather than a to-do, because the difference decides whether this wall is a guard or a placeholder. RulesetRuleParametersWire is one flat union, and two of its fields are non-optional Bools belonging to required_status_checks. A merge_queue rule built through it cannot omit them, and sending them would put keys on the wire GitHub does not accept there -- the fabricated wire value the required_status_checks constructor refuses in the other direction. The capability that ends it, named as a capability: a wire decoding that admits a coproduct discriminated on a sibling key. Until then every arm of the wall is exercised against a fixture rule, which DESIGN 4b explicitly sanctions -- a state unrepresentable in the accepted corpus may still be authorable as source handed to the compiler, and declining to enroll it there is specification-without-execution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Hold the cost-shape row out of this PR: it belongs in the split shape, not the monolith The operator has frozen dag/gunbc/recurring_failure_mode.dag until the per-class split lands, and the reason to back this out is stronger than the freeze. After the split a new class needs two edits -- a per-class row file plus a roster import and entry -- so a row landed in the monolith today is an edit that must be undone and re-authored in a different shape within the day. That is the throwaway artifact DESIGN section 6 says to back out of rather than schedule around. The row is genuinely severable from the rest of this PR, which is why the split is honest rather than cosmetic. It documents a cost-shape class found while measuring this lane's own floor red; the merge-queue model neither produces it nor consumes it, and nothing in the remaining diff resolves, imports or cites it. The measurement that is its content -- 501 to 35, 501 to 82, 502 to 86, 507 to 109, 505 to 154, cpu-vs-cpu against the interrupting line -- is already carried in the PR body and in the annotation on floor_workflow_admits_merge_group, where it explains a construction rather than filing a class. Held for re-landing after the split, authored in the split shape from the start, so it never touches the monolith at all. This also removes this branch's only claim on the file every other lane is appending to, which is where both of my merge conflicts today came from. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * The generic-argument wall and a String where NonEmptyStr was declared: eight refusals, eight repairs The floor did not judge a claim and find it wrong. It REFUSED during strict preparation -- phases_run=3 phases_failed=1, no required-floor summary line at all -- so nothing here executed. SEVEN of the eight are #10226's new wall catching pre-existing mismatches that had no obligation producer until this evening. Three test helpers were declared -> List<String> while observed_ruleset_divergences returns List<RulesetDivergence>, and every call passing one to render_divergences was a generic-argument mismatch nothing had ever judged. The declared type was simply wrong and had been wrong since before this branch; the wall's first outing in the wild found it. Fixed at the declaration rather than at the seven call sites, because the call sites were correct. THE EIGHTH IS MINE AND IT IS NOT THE KNOWN if-JOIN FALSE POSITIVE, which I checked rather than assumed because the shape is identical to the defect filed in #10232. That defect makes a WELL-TYPED construction fail: the join compares branches against each other and never against the declared return context. Here the construction is not well-typed under either rule. concat yields String, the declared payload is NonEmptyStr, and String does not inhabit NonEmptyStr -- so a join that DID consult the declared return would refuse this too, for the same reason. The repair is the cast the corpus already uses for a concat whose first operand is a non-empty literal, and it is safe by construction rather than by check. Both refusal messages take it, not just the one the floor reached. The second was on the same path and would have refused on the next run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Regenerate the stage0 mirror from the merged authority rather than resolving its conflict Merging main conflicted on src/v1/stage0/src/std_measure.rs, which is a GENERATED artifact: both sides had added rows to it because both sides had added rows to dag/std/measure.dag. Resolving those bytes by hand would have been an author writing a projection, and either side taken whole drops the other's rows silently. So the conflict was not resolved, it was DISCHARGED by the producer. The authority merged cleanly on its own; the mirror was regenerated from it with claim_executor --required-regen and the candidate installed verbatim. Taking main's side first was only to get a tree that compiles well enough to build the regenerator -- a deliberately stale intermediate, never a resolution. The receipt is the producer's own predicate rather than a diff I read: first_generation_equal=false before, first_generation_equal=true after, planned=156 executed=156 adjudicated=156 on both runs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Name the producer behind the parameters-coproduct trigger, and say what it must be sufficient for Review 59455 is right that the trigger did not qualify as written. It named a capability with no owner and no bound, and 4b(3) is explicit that a trigger naming only an artifact is satisfied while the capability stays dead -- the symmetric failure is a trigger naming only a capability, which anything can claim to satisfy. The producer is v1_interpreter json_to_value. Its object arm collects every key into a map_value with no type context and no discriminator, so a nested JSON object reaches the substrate as an untagged map and a coproduct arm has nothing to select on. That is the whole mechanism, and it is one function. What it must be SUFFICIENT FOR is now stated rather than implied: a decode of a rule object must be able to yield a value whose parameters is the merge_queue ARM, not a map that a later guard classifies, so that reading a required_status_checks field off a merge_queue rule becomes a resolve refusal instead of a read this module prevents by filtering first. Anything less leaves the guard load-bearing and this class stays at mitigatable regardless of what lands. And the obvious objection now has its mechanical answer in the carrier rather than in a review thread: declaring the coproduct today changes nothing about what can be READ, because the decode produces the same untagged map either way. Every arm would refuse, and merge_queue_standing would report NoMergeQueueRule for a ruleset that has a merge queue -- a silently wrong answer replacing a correct one, which is the direction DESIGN section 5 forbids outright. The declaration is not deferred for convenience; it is unreadable until its producer changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Two wildcard arms answering for constructors that do not exist yet Review 59488 flagged three constructor predicates. Checking them found a real defect its stated rationale does not name, and it is mine: I wrote workflow_trigger_is_merge_group out exhaustively when the earlier review asked for it, and left rule_is_merge_queue on `_ => false` three hundred lines away in the module I was already editing. Two predicates over two coproducts, the same question, two different answers about what an unknown constructor means. A wildcard here answers for constructors that DO NOT EXIST YET. GitHub adds rule types -- this module has already had to carry UnrecognizedRuleType for the ones it does not model -- so a new arm on RulesetRuleType would be silently classified as not-a-merge-queue rather than failing here until someone decides what it means. That is the fabricated default DESIGN section 5 reserves for a refusal. rule_is_required_status_checks carried the identical wildcard and is older than this work. It is repaired with its sibling, because leaving one of two identical predicates exhaustive makes the pair a worse guide than either choice applied consistently: whoever adds a third copies whichever one they happened to read first. It is not repaired because it was flagged -- it was not flagged -- but because the flag was right about the shape, and this is the same shape in the same module guarding the same coproduct. No wildcard arm now remains in any of the three modules under review. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * Close the bypass-actor deletion hazard: it was the rule hazard's other half, left open desired_ruleset_rules projects no bypass_actors and converge sends the WHOLE ruleset, so an apply against a live ruleset carrying an actor grant DELETES it, and nothing in the divergence fold reports it -- the fold compares rules and required contexts, and a bypass actor is neither. This repository has an observed always-bypass RepositoryRole actor id 2, so that is a live silent destructive write and not a hypothetical. It is the same class rule_unexpected_divergences already closes one field over. The two halves were written days apart and only one was closed; the asymmetry is the defect, not the actor. It refuses rather than repairing for the same reason: "the world is not what we declared, apply desired" is exactly backwards when applying desired is what destroys the thing. THE UNREADABLE ARM IS THE ONE THAT MATTERS MOST. BypassRosterUnavailable means GitHub omitted the key -- indistinguishably because the roster is empty or because this credential may not see it -- so an apply would delete either nothing or an unknown number of grants and the observation cannot say which. Treating unavailable as empty would let the empty-observation narrow decide a destructive write, which is the exact inversion this module's reader-versus- roster split exists to prevent. It refuses instead. Three witnesses, including the positive control on an OBSERVED empty roster, without which the check could be "always refuse" and both REDs would still pass. This closes a hazard; it does not discharge the standing hold on modelling the bypass carriers, and it is a reason that hold is right rather than a reason to hurry the sign-off. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL * verify could not see the actor converge now refuses on: complete the pair Closing the write half left the reporting half open, and the asymmetry was the same shape as the one it repaired. observation_divergences bound the roster to `_`, so an undeclared bypass actor was invisible to verify even after converge learned to refuse on it. The refusal stops the write and tells nobody the grant is there -- which is the wrong half to have alone, because the operator's question is "what is on this ruleset that we did not declare", and verify is what answers it. The rule side already had both halves: RulesetRuleUnexpected reported by verify, actuation refused by converge. This is that pair completed for actors, with the same two constructors and the same argument. AN UNOBSERVED ROSTER IS ITS OWN DIVERGENCE RATHER THAN SILENCE. Reporting nothing for BypassRosterUnavailable would collapse "we could not see whether a bypass exists" into "no bypass exists" -- the exact distinction the reader-versus-roster split was built to keep -- at the moment a reader is asking. So it renders as UNKNOWN rather than none, naming the reader. Three witnesses including the positive control on an observed empty roster, so verify cannot invent a finding on a ruleset that genuinely grants none. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
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 join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Outcome
Direct calls now construct one
PositionGenericTypeArgumentobligation for each aligned argument of a same-constructor, same-arity applied type. Imported child identities are peeled before the existingdeclared_type_inhabitanceauthority decides them; the shared relation itself is unchanged.The whole-corpus passes proved the position is load-bearing by finding two pre-existing real defects. In
dag/gunbc/spark/serving_realization.dag,List<SparkServingRealization>was passed through helpers declared forList<ServingRequirementRefusal>; the helpers now have correctly typed realization-specific counterparts. Insrc/v2/compiler/effect_demand.dag,effect_demand_v2_realized_operationswas declaredList<PrimitiveIdentity>while its sole consumer requiresList<EffectRealizationKey>; the empty population now carries the consumer’s authored element type.This closes both independently found specimens:
FreeMonoid<Node>supplied whereFreeMonoid<NormalizedTree>is declared.List<RightCensoredCost>supplied whereList<ExactCompletionCost>is declared (the second specimen is on A right-censored bound could inhabit the field consumers read as an exact cost — close the artifact path #10210 and will be tightened here after that PR lands).The application-head gate prevents ordinary product/coproduct children from being mistaken for generic arguments. Bare, malformed, different-constructor, and unequal-arity pairs remain outside this producer rather than receiving fabricated comparisons. Raw generic formals (
T/K/V) and unresolved inference placeholders (element) also remain with the outer obligation until they name an identity; concrete authored generic arguments are the population judged at this position.Trigger correction and chunk 23 transition
floor_expected_red_chunk_23said its trigger wascontainer_element_nominal_brand_mismatchreaching the direct-call seam. That condition was already true:direct_call_arg_type_mismatchalready called it there while the invalid program remained accepted. The trigger named a route rather than the missing capability and could therefore retire the row while the wall was dead.The corrected capability is: construct a child obligation at
PositionGenericTypeArgumentand decide it throughdeclared_type_inhabitance.direct_call_generic_type_argument_inhabitance_diagsnow constructs that exact obligation and hands it todeclared_type_obligation_diags, so the trigger is explicitly discharged.Chunk 23 was green for the wrong reason and is now green for the right one. Before this change, its negated emission oracle passed because inherited
UnresolvedTypediagnostics refused the fixture while the generic-argument wall was dead. After this change, the same 3/3 total hides a material transition: the mismatch arm passes because it receives exactly one blockingDeclaredTypeNotInhabitedat subject/positiongeneric type argument; the matching arm passes by emission. The witness is therefore retained and tightened as the permanent regression control, while only its obsolete expected-red admission is deleted. The admission is deleted because its wall landed—not merely because an assertion happened to stop failing.Evidence
Local session container, fresh release binary built after the Rust seed change:
cargo check -p v1-compiler— pass.generated_artifact_gate.main_wetcorpus pass — pass; no generated drift.claim_batchover all threerecord_literal_call_arg_handoff_witnessarms — 3/3 pass, exit 0. The mismatch arm structurally asserts diagnostic classDeclaredTypeNotInhabited, blocking severity, and subject/positiongeneric type argument; anUnresolvedType, parse error, lookup miss, or other refusal cannot satisfy it. The matching nominal arm compiles and emits.List<GenericRedLeft>passed toList<GenericRedRight>exits 1 with the verbatim diagnosticvalue does not inhabit its declared type at the generic type argument: declared 'Product(GenericRedRight)', produced 'Product(GenericRedLeft)'. An otherwise identicalList<GenericGreenElement>control emits with zero blocking diagnostics.value does not inhabit its declared type at the generic type argument: declared 'Product(NormalizedTree)', produced 'Primitive(Node)'.Local corpus evidence justifies the push; the required runner lane remains the authoritative corpus receipt.
Sequencing
#10210 is currently open. After it merges, this branch will merge main, invert its
probe_censored_arm_onlyfrom today's admitted-state assertion to the permanent refusal assertion, run all five calibrated arms locally, and push the result before merge readiness.