Skip to content

A refusal decided by which unrelated modules are in the pool, and a join that never consults its declared context - #10232

Merged
briansrls merged 6 commits into
mainfrom
session/cool-koi-858
Sep 3, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/cool-koi-858

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

A well-typed coproduct construction is refused by the if-join, and the verdict depends on
corpus scope. Two cross-linked gunbc.recurring_failure_mode rows, plus the regenerated
projection. No code change: this is the diagnosis, filed. The repairs are two agreed lanes
that follow, resolution first.

The root is an asymmetry, not a precedence bug

My first reading was that a local declaration loses to an unimported foreign one. That is
wrong and the row does not say it. v1.compiler.infer_env lookup_binding_by_name is
local-first — module bindings, then ancestry bindings, then the intern table, and only on a
miss global_bare_lookup. Nothing outranks a local declaration.

What actually happens is narrower: a coproduct arm is pool-visible corpus-wide while not
being a local binding under its own spelling.
So an arm reference misses local lookup
entirely and lands in the pool beside any foreign top-level type of that spelling. An
off-chain module importing nothing can reference another module's arm name and get only an
advisory; and inside the declaring module not even that fires, because there the spelling
is in source_visible_names. That is why the specimen was silent.

Downstream, lookup_variant_parent_enum / variant_owner_node widen a record literal to its
owner coproduct only when the binding resolves to a Disj owning that name — so the
uncollided arm widens and the collided arm stays bare, which is the whole of the asymmetry
the diagnostic reports.

The discriminating pair

Byte-identical source at fcf1347dfa, both entry-scoped, locally built gunbc:

closure verdict
probe importing only gunbc.floor_cost_distribution — 21 sources 0 blocking errors
same + v2.workflow.claim_cost_observation — 45 sources error[dag/gunbc/floor_cost_distribution.dag:221:3]: if branches resolve to incompatible types: Coproduct(ClaimCostReading) vs Product(RightCensoredCost)

Character for character the required-floor refusal. The second module declares a same-named
RightCensoredCost that the first neither imports nor reaches through. A 3-module synthetic
isolates it in a 6-module closure — A declares Shape = Circle | Square and returns one
variant per if-arm, B declares an unrelated Square, C imports A and B, and the verdict flips
on B's presence alone, symmetric under swapping which arm collides.

So the RED is reachable on the ordinary acceptance path and needs no whole-corpus harness —
the §4b question asked before the check, answered: nothing here is permanently green. It was
believed for a while that only the whole-corpus path could discriminate; that is refuted above.

The rule is already ratified and already default on

namespace-resolution-design.md §13, operator-ratified 2026-07-21, is ancestor-chain
uniqueness
: exactly one on-chain candidate resolves, two-plus on-chain refuses a typed
AmbiguousReference, zero on-chain refuses UnresolvedType. Its bracket
NAME_RESOLUTION_POLICY_NAMESPACE_ONLY defaults to true.

It executes on the function-signature channel — flat_parents_preserve_deep_first_last_import_first_shadowing
must set the policy false to assert first-hit-wins, then re-asserts the default refuses.

It does not execute on the type and variant-arm channel. Two competing off-chain
declarations are silently picked between; the only refusal is a consequence at an innocent
site (field 'a' not found, missing required field 'b'), with no AmbiguousReference, and
the pick does not move when the losing module is renamed. So the next-rung trigger names a
capability that is not missing but not reaching a channel.

The telemetry beside it is inert in two ways

Both read, not assumed. SILENT-PICK-GATE consults only fn_parent_first_hits — the
global_bare_lcp_picks and global_bare_lcp_ties vectors, which are this class, are
collected and never read. And resolution_silent_pick_enable is reached only after the
--source-root arm has already exited, so on every modern compile the telemetry is never
armed at all and the gate guards only the legacy --source-dir flat scan.

Why the if-join is a second row and not a clause

prefer_specific_type already returns the correct join for the refused pair — it returns the
left, the declared return, because every re-selection arm falls through. The check refuses a
pair it can already join, corroborated by the refusing runs carrying that as their only
blocking error. That makes it narrow and cheap when its turn comes. Repairing it first would
silence the diagnostic while leaving the wrong binding in place, so the ordering is resolution
first.

Two deliberate omissions, stated rather than left to be found

No §4b(3) rung-drop row. A drop row is a declaration made by the party lowering the rung.
Filing this retroactively as one would launder an undeclared regression into a sanctioned one
and hand out a runway nobody asked for. The absence of that row is part of the finding.

The synthetic is not committed as a fixture here. It goes red today, so enrolling it
asserting the correct behavior reds main, and enrolling it asserting the current behavior is a
change detector. It lands in the resolution lane together with the wall that makes it green —
which is §4b(4)'s shape, an expecting-red probe flipping to a permanent regression control.
Committing it now with no consumer would be the experimental-residue tell.

Rung

Root: below the ladder on source-to-interpretation — the wrong binding is taken silently.
Ceiling structurally guaranteed (3), not impossible (4): nothing stops two modules
spelling a type the same, so the invalid state stays writable; what is attainable is that no
Accepted program resolves through one. Rung 4 needs a declaration-identity capability making
the second declaration unwritable, named as the further trigger.

If-join: mitigatable — loud, typed, located; the verdict is wrong, not its containment.
Ceiling structurally guaranteed, since an if-expression whose arms disagree under no declared
context is authorable by construction and must still be refused.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq

gunbc-ci-auto-heal and others added 5 commits September 3, 2026 12:38
…pool

A well-typed coproduct construction is refused by the if-join, and the
verdict depends on corpus scope. Both halves are filed, cross-linked, as
their own classes.

THE ROOT IS AN ASYMMETRY, not a precedence bug. A coproduct arm is
pool-visible corpus-wide while not being a local binding under its own
spelling, so an arm reference misses local lookup entirely and lands in the
pool beside any foreign top-level type of that spelling. Inside the
declaring module not even the unlisted-import advisory fires, which is why
the specimen was silent.

MEASURED, both entry-scoped, byte-identical source at fcf1347: a
21-module closure over gunbc.floor_cost_distribution compiles with 0
blocking errors; a 45-module closure adding only
v2.workflow.claim_cost_observation -- which declares a same-named
RightCensoredCost that the first module neither imports nor references
through it -- reproduces the required-floor refusal character for
character. A 3-module synthetic isolates it in a 6-module closure and is
symmetric under swapping which arm collides. So the discriminating RED is
reachable on the ordinary acceptance path and nothing here is permanently
green.

THE RULE IS ALREADY RATIFIED AND ALREADY DEFAULT ON.
namespace-resolution-design.md section 13 is ancestor-chain uniqueness --
two-plus on-chain refuses AmbiguousReference, zero on-chain refuses
UnresolvedType -- with NAME_RESOLUTION_POLICY_NAMESPACE_ONLY true in v1_rt.
It executes on the function-signature channel and does not execute on the
type and variant-arm channel, where two off-chain competitors are silently
picked between and the only refusal is a consequence at an innocent site.
So the next-rung trigger names a capability that is not missing but not
reaching a channel.

The silent-pick telemetry beside that behavior is inert in two ways, both
read rather than assumed: the SILENT-PICK-GATE consults only
fn_parent_first_hits, leaving the global-bare pick and tie vectors
collected and never read; and resolution_silent_pick_enable is reached only
after the --source-root arm has exited, so on every modern compile it is
never armed at all.

The if-join is its own row because the defect there is narrow and cheap:
prefer_specific_type already returns the correct join for the refused pair,
so the check refuses a pair it can already join. Repairing it first would
silence the diagnostic while leaving the wrong binding in place, so the
ordering is resolution first.

No 4b(3) drop is filed. An undeclared regression filed retroactively as a
declared one would launder it and hand out a runway nobody asked for; the
absence of that row is part of the finding.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
Three additions to the two rows, none of them new claims.

THE SPECIMEN IS COMMITTED RATHER THAN DESCRIBED. The probes that produced
the 21-versus-45 result were deleted after measuring, which left the row
citing executable evidence that no longer existed -- a transcription
wearing a citation's clothes, since the numbers survive and the thing that
produced them does not. fixtures/if_join_pool_binding carries the four
modules: declaring_module is the subject and is byte-identical across both
arms, colliding_module is the whole of the perturbation, and the two
closure_* entry points are the red arm and its positive control. Measured
here: the with-collision entry refuses at declaring_module with
Coproduct(PoolSpecimenShape) vs Product(PoolSpecimenSquare); the
without-collision entry reports 0 diagnostics.

It sits OUTSIDE the compiled source roots deliberately. An authentic
collision committed into dag or src/v2 would be a real corpus fork rather
than a specimen of one, so this is source handed to the compiler by a
fixture -- the position DESIGN section 4b names when it asks whether a RED
is authorable. No enrollment and no assertions: the expecting-red probe
lands with the wall that greens it, in the resolution lane.

THE INVARIANT NOW HAS ITS NAME. Irrelevant-scope extension invariance: for
source S with resolved closure C, an environment E1 derived from C and an
E2 that is E1 plus declarations unreachable from S, typecheck(S, E1) must
equal typecheck(S, E2). It does not. That says what went wrong -- the local
judgment consumes more environment than its subject owns -- where "the
verdict depends on scope" only says that something did.

THE SILENT-PICK GATE CANNOT GO RED ON THIS CLASS BY CONSTRUCTION, and the
row now says so in those words. It is permanently green for two
independent reasons, wrong field and wrong code path, either of which alone
would suffice -- so fixing one would leave it looking fixed. That is worse
than an absent check because it will be cited as coverage: a reader finding
a fail-closed exit 1 on silent picks concludes the class is walled. Repair
or delete it, and prove the repaired RED rather than assume it.

Plus independent corroboration from the lane that hit this first: a
four-arm table whose decisive row holds the branch restructure constant and
renames only the two arms -- green -- with its mirror restructured, green,
and still forked. That isolates the collision as the cause from a direction
these probes do not test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
# Conflicts:
#	docs/design-failure-modes.md
… not

The row asserted that section 13 ancestor-chain uniqueness "does not
execute on the type and variant-arm channel." That is wrong, and a wrong
diagnosis in the authority for a class outlasts any approval: it sends the
next reader hunting a policy bypass, which is the hypothesis this settles.

SETTLED BY EXECUTION, with a discriminating pair that isolates one
variable. Two same-named TOP-LEVEL types on the referencing module's chain
refuse correctly -- ambiguous reference naming both declaring modules and
telling the author to qualify, alias or rename. Change one candidate from a
top-level type to a coproduct ARM, holding policy, chain geometry and
closure size fixed, and there is no AmbiguousReference at all: the foreign
product binds silently. A third-module variant gives the same result and
removes the confound that the reference sat inside its own declaring
module. The wall is alive; the arm is not in front of it.

THEN LOCATED BY READING, because behavior had already told the wrong
mechanism twice about this class. global_bare_fallback_invariant declares
the rule: tracking is decl-only over type, fn and data names plus ONLY
those Disj variant aliases unique across the whole bare-name space -- a
variant whose name any declaration claims stays qualified-only and never
becomes a candidate -- because admitting it would create a type-versus-
variant tie that refuses every FAR use of the type.

SO "COMPLETE THE CANDIDATE POPULATION" IS WITHDRAWN. Re-admitting arms
re-creates exactly the tie the exclusion exists to prevent. What the
exclusion does is trade one refusal for another and take the silent one:
it protects far uses of the type at the cost of the arm's own declaring
module losing its arm with no diagnostic. The decidable question is WHERE
THE TIE IS REPORTED, not whether the arm is a candidate -- and the
exclusion's own justification is about FAR uses, which is the asymmetry a
locality-respecting rule would exploit.

Three further corrections, each recorded rather than quietly fixed.

The two-competing-top-level-declarations probe, which this row first
offered as evidence about the policy branch, is not evidence about it. Its
competitors arrive through ancestry_str_bindings -- a map with one entry
per name -- so the bind is settled at map-build time and global_bare_lookup
is never consulted. That is a second route to the same harm with a
different cause, kept separate because folding it in would hide it, and
recorded because the next reader will run that probe and misread it.

global_bare_nearest_ancestor is reached only on the non-namespace-only arm
and is dead code under the shipped default. Deleting it is hygiene and
CENSUSES NOTHING. A census over unreachable code returns the empty set for
the same reason a healthy tree does.

The corroborating lane is now cited as gunbc#10210 rather than by branch
commits, which do not survive squash-merge, and is named as an orthogonal
perturbation axis: every probe here varies pool membership with the
spelling fixed, that table varies the spelling with membership fixed, so
neither alone excludes the other's confound.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
# Conflicts:
#	dag/gunbc/recurring_failure_mode.dag
#	docs/design-failure-modes.md
# Conflicts:
#	dag/gunbc/recurring_failure_mode.dag
#	docs/design-failure-modes.md
@briansrls
briansrls merged commit cb0ec47 into main Sep 3, 2026
6 checks passed
@briansrls
briansrls deleted the session/cool-koi-858 branch September 3, 2026 17:14
@briansrls
briansrls restored the session/cool-koi-858 branch September 3, 2026 17:19
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant