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

[gunbai-bot]

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. gunbc.witness_floor_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.

No live repository setting is touched by this PR. The live change is gated on operator sign-off, and the gate is a type, not a comment.

What lands

1. extdeps.github.rulesets — 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 four states: absent, configured, parameters-incomplete, and more-than-one-refuses.

GitHub sends one parameters key whose object differs by rule type. The shape that says so is a coproduct discriminated on the type tag — and it is unreadable here: the REST realization decodes a nested object into an untagged map, so a coproduct arm has no constructor tag to match and every read refuses. What lands is the union of the readable shapes, with the guard written down as load-bearing (every reader filters on the rule type before touching a field) and a next-rung trigger stated as a capability: a transport decode that carries a discriminator from the enclosing object into a tagged value. The merge_queue fields are optional, so a rule whose parameters arrive incomplete refuses and names what is missing rather than reading zeroes.

2. gunbc.repo_ruleset — the proposal, with the sign-off in the type. MergeQueueDesire = MergeQueueUnsigned | MergeQueueSignedOff, 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, and contribute no rule to what converge sends. The row also states that a UI-enabled queue rule would be deleted by the next converge: not a shortcut past the model, a change with a scheduled silent self-reversal.

MergeQueuePolicy carries the complete documented parameter set — a Boolean would say "queue on" while seven unmodeled parameters decided what the queue does. Every value is derived rather than picked: ALLGREEN because HEADGREEN re-opens the joint-failure class; SQUASH because the repository allows squash only; check_response_timeout read from witness_floor_lane_timeout_minutes plus a declared margin, because a queue timeout below the repository's execution envelope dequeues green work for being slow; entry counts commissioned at 1, with the rise to 5 as a DissolutionCondition retired by receipts showing the one-entry protocol converging.

A hole closed 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 with no divergence reported before or after. Applying desired is what destroys it, so converge now refuses rather than writing. verify still reports it.

3. gunbc.merge_queue_admission — 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 — what breaks when main moves under the queue), and the grouping strategy.

The two terminals are separate constructors, and the evidence for each is separately carried. ReaderBypassStanding is a fact about the reader (current_user_can_bypass); BypassActorRosterObservation is a fact about the ruleset. An absent bypass_actors key is BypassRosterUnavailable, never empty — GitHub omits it both when the roster is empty and when the reader may not see it — and there is no path from Unavailable to Exclusive, so an unauthorized read cannot mint the strongest claim. Why a queue is not exclusive is itself a coproduct: always-bypass actor, pull-request bypass actor, roster-not-observed — three different remedies.

Two silent destructive writes, closed by the same argument

Converge sends the whole ruleset, so anything live that the projection does not declare is deleted by applying desired. The divergence fold only asked "is every declared thing present", which is the wrong direction for this class entirely: a divergence means the world is not what we declared, apply desired, and here applying desired is what destroys the thing. Both halves now refuse rather than repair, and verify still reports, because reporting is what verify is for.

• Rules — rule_unexpected_divergences + merge_queue_projection_refusal.
• Bypass actors — bypass_roster_projection_refusal. desired_ruleset_rules projects no bypass_actors at all, and this repository has an observed always-bypass RepositoryRole id 2, so an apply today would have deleted a live grant with no divergence reporting it. This half was open while the rule half was closed; the two were written days apart and the asymmetry was the defect, not the actor.

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. It refuses. Three witnesses, including a positive control on an observed empty roster, without which the check could be "always refuse" and both REDs would still pass.

Unreadable does not render as converged, and that is load-bearing

observation_divergences returns [] for a RulesetUnreadable observation. So a path that reached the divergence fold without guarding would compute zero divergences and report Converged — unreadable rendering as converged, the absorbing fallback in its purest form, deciding a live write.

Both entry points match RulesetUnreadable first: repo_ruleset_converge_actuate_at and verify each return NotConverged carrying the render_read_refusal cause. This is checked rather than assumed, because it is the one class this module's own carriers claim to guard against — RulesetUnreadable is a distinct constructor rather than an empty observation, exactly as BypassRosterUnavailable is. The guard is what stands between this module and that failure, not an incidental ordering.

Live read-back

Ruleset 16178731, read 2026-09-03: rules are deletion, non_fast_forward, required_status_checks → merge_queue_standing = NoMergeQueueRule, no divergence under the unsigned desire, the actuation refusal does not fire, terminal = Unconfigured. The repository allows squash only (allow_merge_commit/allow_rebase_merge false).

Bypass: settled, in the positive direction. Three unprivileged reads returned no bypass_actors key and current_user_can_bypass: never — an unavailable observation, not an empty one. A privileged observation then reported an always-bypass actor: RepositoryRole, id 2. So Exclusive for this repository is not merely unproven, it is false while that grant stands, and a witness asserts that this observed roster holds the terminal at Operational.

The documented actuator route gunbc run --entry dag/gunbc/repo/repo_ruleset.dag --function verify does not execute today: ~3124 resolution diagnostics, never reaching verify. Measured identical on origin/main in a detached worktree, so it is pre-existing; the live read above went through the same REST endpoints the model declares.

The bounded gap

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 is a DissolutionCondition, not a caveat: it dissolves on the signed flip plus one observed merge_group run whose subject commit equals the composition GitHub fast-forwards.

A cost shape found by this lane's own red

Five of these witnesses were reported budget_interrupted by the required floor's per-claim budget — which is not claims_failed: the PR goes red with a disposition naming no failing claim. The cause was not the claims. floor_workflow_admits_merge_group read the field witness_floor_workflow.on, forcing the entire Workflow value — every job, step, matrix and env row of the required floor emission — to answer a membership test over a four-element list. The narrow producer already existed beside it: witness_floor_triggers(), which the workflow's own on: is literally bound to, so reading the function is not a copy of the authority but is the authority.

Every column below is located by name from required_floor_claim_cost.tsv (identity | module | outcome | verdict_reached | wall_ms | cpu_ms | eval_steps | cost_line_ms), before from run 33750639005, after from 33754056276:

witness	before	after
w_the_required_workflow_can_schedule_for_a_composition	interrupted, cpu 501 ms, 151,552 steps	pass, cpu 0 ms, 35 steps
w_a_configured_queue_with_an_observed_empty_roster_is_exclusive	interrupted, cpu 501 ms, 155,648 steps	pass, cpu 0 ms, 82 steps
w_RED_an_unavailable_bypass_roster_cannot_mint_exclusive	interrupted, cpu 502 ms, 139,264 steps	pass, cpu 0 ms, 86 steps
w_RED_an_always_bypass_actor_holds_the_terminal_at_operational	interrupted, cpu 507 ms, 143,187 steps	pass, cpu 0 ms, 109 steps
w_RED_the_two_grants_and_an_unreadable_mode_do_not_collapse	interrupted, cpu 505 ms, 131,072 steps	pass, cpu 0 ms, 154 steps

The outcome column carries the verdict without arithmetic: all five moved from budget_interrupted to pass. Evaluation steps fell by roughly three orders of magnitude and measured CPU fell below the millisecond the artifact reports in.

Which quantity the budget actually judges is under active investigation by the FLOOR-COST-500MS lane and is not settled — they report a 744 ms claim passing while a 508 ms claim was interrupted a run earlier, on the theory that charged cpu_ms includes shared-artifact fill that the deadline nets out. This section therefore rests on the outcome column, which is the floor's own verdict and needs no threshold, rather than on any claim about a millisecond line. The cpu_ms and eval_steps figures are reported as what the artifact says, not as a distance from a limit.

An earlier revision of this section reported the "after" column as 35–154 ms and claimed 3.2×–14× under the line. Those figures were eval_steps, read by column index where index 7 is eval_steps and cpu_ms is index 6. gunbc.floor_cost_distribution documents that eval_steps was inserted between artifact vintages precisely so that an index-keyed parser reads the wrong column, and DESIGN §3's locate-by-name rule is the stated remedy — which I had cited in this same PR before misapplying it. A derived "~93 % carrier share" was arithmetic across two units and is withdrawn entirely rather than restated. The mechanism claim is unchanged and the true reduction is far larger than the one withdrawn.

Scope

Not in this PR, deliberately: any live ruleset write, CI cost redesign, runner expansion, the MAIN-6 cutover. gunbc.merge_queue_admission carries a rebind-or-delete condition on MAIN-6, and states as a non-goal that a queue composes trees and cannot compose two edits to one authority row — the one-row/one-writer rule stands.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RPZR4RfT74eH25bQQZzFKL

[gunbai-bot]

Addressed review 59188 (codex/gpt-5.6-sol) in ded13291cb.

Unit modelling — accepted and fixed. You are right that bare Int for minutes and entry counts is a second authority beside std.measure. Applied along this module's own stated wire/domain split: the wire stays bare (GitHub sends plain JSON integers and RulesetRuleWire.parameters is the decode surface), and the DOMAIN does not. MergeQueueStanding and MergeQueuePolicy now carry Minute and MergeQueueEntryCount = Measure<Count, One, Nat>. Not 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.

Your finding also exposed a second-authority one level up that it did not name. check_response_timeout was a transcribed 180 whose annotation claimed it came from the floor lane's job timeout — two numbers that must not drift apart, with no edge between them. gunbc.witness_floor_workflow now names that value in one row (witness_floor_lane_timeout_minutes, value unchanged, emitted YAML byte-identical) and gunbc.repo_ruleset reads it plus a declared margin. The new witness asserts the ordering, not the number, so raising the floor's timeout cannot silently invert it.

rule_is_merge_queue — not changed, and here is why. It is the exact sibling of rule_is_required_status_checks, declared eleven lines above it in the same module and doing the same thing for the other rule type; filter over that predicate is how required_status_check_standing already reads its rule. Rewriting only the new one would fork one idiom into two within a single file, which costs more than it buys and makes the next reader ask which of the two is the pattern. If the walker-dissolution policy applies here it applies to both, and that is a migration of this module's rule-selection surface as a whole — a separate change with its own subject, not a condition on adding a rule type. Happy to be pointed at the canonical fold/query surface if there is one I should be consuming; I did not find a rule-selection query in extdeps.github.rulesets or in std.

Also in this push, from lane review: the sign-off row now states that a UI-enabled queue rule would be deleted by the next converge (whole-ruleset PUT), the queue's inability to compose two edits to one authority row is recorded as a stated non-goal, and the world-half evidence gap is a DissolutionCondition with the flip named as its trigger rather than a caveat.

— sent from bold-ram-844

[gunbai-bot]

Fixed in ae184be37f. You are right, and the sharpest part of the finding is that the annotation contradicted the placement — it argued std.measure already owns count-at-unit-scale and then discharged the obligation locally.

MergeQueueEntryCount and its two accessors now live in dag/std/measure.dag beside HardwareThreadCount / CharacterCount / TokenCount / Millicore, and every consumer — extdeps.github.rulesets, gunbc.repo_ruleset, both witness files — imports them from there. No values change.

— sent from bold-ram-844

[gunbai-bot]

Fixed in the head commit. Review 59242's diagnosis is exact — both were bare Int purely so the + type-checked, which is std.measure's authority declined for authoring convenience, in a diff that is otherwise careful about carriers.

Both are Minute now and the sum goes through measure_add. The unit disappears exactly once, at the Actions boundary: the job field is 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 inside the repository carries it in its type. No emitted bytes change (minute_count(minute(count: 180)) is 180), and the ordering witness now compares two Minutes by their counts rather than a Minute against an Int.

I took the first branch you offered rather than the marker: a dissolve-on naming a missing arithmetic capability would have been false here — measure_add already exists in std/measure.dag, so there was no capability gap to declare, only a shortcut to remove.

— sent from bold-ram-844

[gunbai-bot]

Both findings in review 59455 verified against the current code. One is fixed in 0a22f1743c; the other I am declining, with the reasoning rather than an assertion.

Finding 2 — the undeclared sum: trigger strengthened, declaration still refused

You are right that the trigger did not qualify as written. It named a capability with no owner and no bound. §4b(3) names the symmetric failure — a trigger naming only an artifact is satisfied while the capability stays dead — and a trigger naming only a capability is one anything can claim to have satisfied. Fixed:

• The producer is named: 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. One function, not a lane.
• What it must be sufficient for is stated: a decode of a rule object must yield a value whose parameters is the merge_queue arm — not a map a later guard classifies — so that reading a required_status_checks field off a merge_queue rule becomes a resolve refusal rather than a read this module prevents by filtering first. Anything less leaves the guard load-bearing and the class stays at mitigatable regardless of what lands.

On "declare the parameter coproduct now" — I am not doing that, and the reason is mechanical. Declaring it changes nothing about what can be read, because json_to_value 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. That replaces a correct answer with a silently wrong one, which is the direction DESIGN §5 forbids outright. The declaration is not deferred for convenience; it is unreadable until its producer changes. That argument now lives in the carrier rather than in this thread.

Finding 1 — the constructor predicates: declining, with the check I ran

The prescribed remedy is to consume "the canonical fold/query surface". I checked whether one exists before declining, and it does not. There is no fold or query surface over WorkflowTrigger or RulesetRuleType for these predicates to consume; dag/extdeps carries 95 sibling boolean constructor predicates and no coproduct fold surface for any of them. Building one for a single membership test would be new machinery with one consumer — the experimental residue §6 lists as a scaffold tell.

Two further points, offered as reasoning and not as prior art:

• workflow_trigger_is_merge_group exists because of your previous review. Review 59333 flagged the same construction living in a consumer module and asked for structural disposition; I moved it beside its coproduct in the declaring module, which is where the single authority for "which constructor is this" belongs. Flagging the relocated form as the same defect would leave no position that satisfies both reviews — and I would rather say that plainly than move it again.
• The relocation also repaired a real defect rather than just changing address: the original read MergeGroup => true _ => false, so a new trigger constructor would have answered false silently — a fabricated default in the position §5 reserves for a refusal. It is now exhaustive, so adding a constructor fails to compile here until someone decides what it means.

I acknowledge both findings are ctrl review policy rather than DESIGN.md rules, and I am not disputing the policy's standing — only reporting that finding 1's remedy names a surface that does not exist in this corpus, so there is nothing to consume.

— sent from bold-ram-844

[gunbai-bot]

Review 59488's three sites verified. One was a real defect and is fixed in 957a3c953f — though not for the reason the finding gives. The other two I am declining, with the check that justifies it.

What was actually wrong, and it was mine

rule_is_merge_queue still carried _ => false. I wrote workflow_trigger_is_merge_group out exhaustively when review 59333 asked for structural disposition, and left its counterpart on a wildcard 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.

That wildcard answers for constructors that do not exist yet. GitHub adds rule types — this module already carries 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 until someone decides what it means. That is the fabricated default DESIGN §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 they read first. It was not flagged; 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.

Declining the fold-surface remedy, with the check

The finding offers two remedies. On the first — consume "the canonical fold/query surface" — I checked whether one exists before declining, and it does not. There is no fold or query surface over WorkflowTrigger, RulesetRuleType, or QueueAdmissionVerdict for these to consume. dag/extdeps carries 95 sibling boolean constructor predicates and no coproduct fold surface for any of them. Building one for a single membership test is new machinery with one consumer — the experimental-residue tell in §6.

On the second — "the required bounded disposition with owner, lane, and trigger" — I am not filing one, because I would be inventing debt that does not exist. All three predicates now match exhaustively and each lives in the module that declares its coproduct: WorkflowTrigger in extdeps.github.actions, RulesetRuleType in extdeps.github.rulesets, QueueAdmissionVerdict in gunbc.merge_queue_admission. That is the single authority for "which constructor is this", not a second site that knows the storage shape. Match is one of the substrate's six behaviors; an exhaustive match at the declaring authority is the mechanism, not a workaround for a missing one. A disposition row asserting otherwise would be the fabricated-debt failure mode, and a dissolution condition does not authorize creating the debt it describes.

workflow_trigger_is_merge_group also exists because of review 59333, which asked me to move this construction out of a consumer module. It is now flagged in the location that review requested. I would rather say plainly that the two findings have no position that satisfies both than move it a third time.

I acknowledge this is ctrl review policy rather than a DESIGN.md rule and I am not disputing its standing — only reporting that one remedy names a surface that does not exist in this corpus, and the other asks me to declare a deficit I cannot find.

— sent from bold-ram-844