Give DemandCommand a core effect: the two-provider argument demand.dag makes in prose, enforced by something

[briansrls]

What was wrong

dag/product/fabric/demand.dag declares the split in prose — the binding owns INTERPRETATION, the core owns EFFECT: whether the transition is authorized, whether any other demand still requires the Work, whether a running Attempt should continue, whether capacity and budget should be released — and declares SatisfactionRequirement's three independent answers and DemandCommand<P>. It then shipped three field accessors. No function anywhere took a command plus the demand population and returned a typed effect.

So the module's central load-bearing claim was specification without execution. The two-provider argument it exists to make — a GitHub withdrawal must not destroy Work a GitLab demand still requires — was enforced by nothing, and a binding could cancel directly because no core surface existed to route through.

What lands

demand.dag — the population half. A refusal vocabulary (DemandRefusal<P>) whose first two arms are the pair that matters: UnknownDemand (no such key registered at all — stale binding, or a replay) and DemandPrincipalMismatch (the key IS registered, under a different principal). Collapsing those would report a cross-tenant authorization failure as a bookkeeping miss, in the exact carrier whose whole design puts the principal inside identity so it cannot be dropped by accident. apply_demand_command is total over submit / withdraw / supersede and carries the subject Work out with the transition, so the execution half needs no second lookup that could disagree. work_requirement answers the question a binding cannot. satisfaction_directive consumes the three fields independently.

There is deliberately no MissingEvidence arm: ObservationReceiptRef is branded over NonEmptyStr, so a command carrying no evidence has no spelling, and an arm for it would be permanently green by construction — cited as coverage while carrying no information (DESIGN §4b).

product.fabric.arbitration — the execution half. DemandCommandEffect<P> with six named arms, no Bool, no Option, no wildcard over the others. It is a peer module rather than more functions on demand.dag, and that is forced: execution.dag already imports demand.dag, so the join cannot live in demand.dag without inverting a live edge, and acyclicity is the import graph's only law (§3). It mints no carrier — in-flight execution is read as ExecutionGrant, which already carries the attempt, the work, the lease and both reservation sets.

It decides; it does not actuate. ReleaseDirective names the lease and both reservation sets and hands them to budget.dag, which owns the money ledger. Deciding and releasing in one function would put a second authority for the released quantity in the caller's hands — exactly what release_money refuses by deriving the amount from the entry. The lease travels whole rather than as a bare generation, for the reason execution.dag already gives about receipt admission.

Two arms exist because they differ in what the caller must DO, not for symmetry: WorkReleasedNothingRunning is a real state — a Work can lose its last demand before any grant issued — and folding it into the stopping arm would hand back a release directive naming an attempt and reservations that do not exist.

Authorization (added after review 55256)

A binding holding another requester's correctly spelled FabricIdentity could withdraw that requester's demand and every check passed — the mismatch arm sees a falsely presented principal, never an impersonated correct one.

The gate: CommandAttestation<P> is an input, AttestationDoesNotCoverPrincipal refuses the mismatch, and it runs before any lookup so the two refusals cannot be differenced into an existence oracle for another principal's keys. The withdrawal's receipt lands on ReleaseDirective.authorized_by, so a capacity/budget movement names the observation that caused it.

The comparison alone was not enough, and the first attempt at this shipped claiming it was. As a plain record with public fields, anyone holding the victim's identity could write CommandAttestation { principal: victim, evidence: anything } and the comparison passed — it tested the attestation against itself. The carrier is now sole_constructor, so the record has no cross-module literal and attest_command_principal is the only route to one. Measured on the acceptance path: a cross-module literal returns sole_constructor type 'CommandAttestation' cannot be constructed outside its defining module, and the suite is 16/16 green with that literal removed.

Confinement was still one construction short. A separately-passed attestation is mandatory only by the signature that happens to ask for it — nothing stopped a command reaching a decision with no attestation beside it. CoreCommand<P> is sole_constructor and pairs the two, so "decide this command, I have no attestation" has no spelling; decide_demand_command takes a CoreCommand, not a command plus a record. Measured: a cross-module CoreCommand literal returns sole_constructor type 'CoreCommand' cannot be constructed outside its defining module, suite 16/16 green without it.

The invariant is deliberately narrower than the type name might suggest, and the carrier says so: every core command carries an attestation witness produced by the declared authority — not that every core command is authenticated. The first is a theorem about this module; the second is a claim about the world that no carrier here can hold.

admit_command also moves the consistency check to construction. Whether the attestation covers the acting principal is decidable from two values in hand and needs no observation, so an inconsistent CoreCommand does not exist to be checked and apply_demand_command carries no attestation arm — a check there would be a second representation whose RED is unauthorable. The two discriminating tests stay enrolled, retargeted at the mint (§4b: the climb deletes the production machinery, never the evidence).

verification_authority: DeclarationRef names who claims the attestation is valid, so the core can answer that without pretending to answer whether the claim is true. Without it the declared residual becomes unattributable at exactly the moment someone needs to attribute it.

The population was the remaining forgery surface (review 55310). withdrawal_effect folded a caller-supplied List<Demand<P>>, so a provider omitting another provider's demand got WorkReleasedAttemptStops — the headline failure, reachable by passing a shorter argument, undetectable because a shorter list and a genuinely smaller population are the same value. Unlike authentication this is inside the core's observation boundary: population completeness is the core's own state, so it is a construction, not a residual. DemandPopulation<P> is sole_constructor — the only routes are the empty registry and the output of an admitted transition. Measured: a cross-module literal returns sole_constructor type 'DemandPopulation' cannot be constructed outside its defining module. Invariant, again stated at the width it holds: every population reaching a decision was produced by this module's transitions, not that it is globally complete. Stale-snapshot is a registry obligation; next-rung trigger (registry identity + generation, fenced as execution.dag fences leases) is on the carrier.

Known residual, declared rather than left to be found: the grant roster is still an unsealed list, so a caller omitting a grant causes under-release. Same defect class; sealing it belongs with grant issuance, which has no authority carrier yet.

Verifier provenance reaches the release. verification_authority was dropped when the effect was produced, so the release could not name who authorized it. ReleaseDirective now carries vouched_by beside authorized_by — two facts, kept two.

The boundary, stated on the carrier. The core owns shape, identity consistency, grant accounting, resource release, effect admission. It does not own identity truth, credential truth, or human authorization truth — those sit with the verifier, above the mint. The core has no external observation channel, so any "authentication" written inside it would necessarily be one of three failures: reimplementing an external authority, trusting an input field, or inventing a model of reality.

Ceiling, declared on the carrier. sole_constructor confines WHO MAY CONSTRUCT and says nothing about WHAT a sanctioned caller proves, so the class splits and only one half moved: forgery by an arbitrary caller is structurally guaranteed against; a binding that mints an attestation it did not verify is a boundary obligation on the binding, not something the core closed. Making the core verify evidence would fabricate the external fact §4b says a boundary must refuse rather than manufacture. Next-rung trigger: admit_callers narrows the mint to a provider binding's entry points once such a module exists to name.

Coverage of concurrent grants (added after review 55256)

new_attempt_required admits a fresh attempt while one is running, so two grants against one Work is ordinary. Both execution-bearing arms carry lists — releasing only the head stranded the tail's capacity and budget under a Work nothing requires. Uniqueness is deliberately not enforced structurally, because the model permits concurrent attempts.

Evidence — green by execution, with the discriminating RED

claim_batch --claim-run over dag/test/claim/fabric_demand_effect_witness_test.dag, remote (BuildBuddy, invocation ad698271): 18/18 PASS.

The green is not the evidence. The mutation is. Replacing the work_requirement call in withdrawal_effect with an unconditional WorkNoLongerRequired — a fabric that cancels on every withdrawal, the precise defect the core surface exists to prevent — produces:

FAIL withdrawing_one_of_two_demands_leaves_the_work_required
PASS withdrawing_the_last_demand_releases_the_work_and_stops_the_attempt
PASS releasing_a_work_with_nothing_running_names_no_attempt

Exactly one test flips, and it is the two-provider one. Both release-direction tests stay green under the mutation, which is what makes them a mirror rather than a second copy of the same assertion: a witness exercising only the single-demand path would have gone green against that mutant. withdrawing_the_last_demand_... is the paired direction — without it, the first test is satisfied by an implementation that never releases anything at all.

Two further mutation controls, one per review finding. Attestation gate neutered (if false): the two attestation tests red, the pre-existing principal-mismatch test stays green — so they test the new wall, not the old one. Matching grants take(1)'d: the two count-based tests red, the single-grant test stays green — which is precisely why the count tests were needed, the old test cannot see that defect.

The three SatisfactionRequirement fields each get their own test holding the other two and the whole world fixed, so none of them is a decoration: terminal_receipt_may_satisfy moves between satisfaction and execution, new_attempt_required between attaching and a fresh attempt, step_reuse_permitted changes what that attempt may reuse without changing whether it exists.

One thing deliberately not asserted

That an unauthorized withdrawal cannot also have cancelled something is not a runtime assertion here, because it is not a runtime property: CommandRefused carries no population and no release directive, so a refusal that took effect has no spelling. Asserting an empty population through the test helper would only measure that the helper returns [] on the refusal arm — a permanently-green check standing where the carrier already made the state unwritable (§5, construction over validation).

Scope

Touches dag/product/fabric/demand.dag (appended), adds dag/product/fabric/arbitration.dag and its witness. Reads execution.dag / budget.dag, edits neither. Checked against silent-bear-842, whose identically-titled lane is gunbc.fabric_cell_converge: disjoint — they import CellId from sanitation.dag, which this does not touch or move.

product.fabric.sanitation observation_for's first-match fail-open is not repaired here. It is assigned to be repaired with its first consumer, and this is not that consumer: nothing here reads a readback — the inputs are the demand population, the live grants, and the command. Adopting it without a consumer would be the wrong shape.

[gunbai-bot]

Both findings in review 55256 verified against the code and fixed in 3c53b96a63. Each fix has a mutation control, because a new green test is not evidence that a new wall stands.

Finding 1 — authorization not enforced

Confirmed, and sharper than "evidence is discarded": the hole was reachable with a correctly presented identity. DemandPrincipalMismatch fires when the presented principal does not match the registered one; when a binding holds another requester's full FabricIdentity the pair genuinely matches, every check passed, and the demand was removed. Possession of an identity was authorization to mutate it.

What I did not do is have the core verify evidence. demand.dag states the core treats provenance as opaque and never interprets it, and authentication is an external fact — inventing a verification here would fabricate exactly what §4b says a boundary must refuse rather than manufacture. So the residual (is the attestation itself true?) stays the binding's obligation, and is now stated in the module rather than silently assumed.

What the core can decide, and did not, is that a caller may only act as the principal it attested to being. CommandAttestation<P> (principal + the receipt that established it) is now an input to apply_demand_command, acting_principal names the principal each command acts as, and AttestationDoesNotCoverPrincipal refuses the mismatch. The gate runs before any lookup — checking it after would let an unattested caller learn whether a key exists under another principal from the difference between the two refusals.

Evidence stopped being an unread field too: the withdrawal's own receipt now lands on ReleaseDirective.authorized_by, so a capacity and budget movement can name the observation that caused it.

Mutation control — if attestation.principal != acting replaced with if false, i.e. the pre-review behaviour:

FAIL a_binding_may_not_withdraw_a_demand_it_did_not_attest_to
FAIL a_binding_may_not_submit_a_demand_under_a_principal_it_did_not_attest_to
PASS a_withdrawal_from_the_wrong_principal_refuses_by_principal_not_as_unknown

The third staying green is the point: the old check is untouched and orthogonal, so the two new tests are testing the new wall and not re-testing the old one. Each new test also carries its truthful-attestation mirror, so neither is satisfied by a gate that refuses everything.

Finding 2 — release leaks the tail

Confirmed. Cons { head: g, tail: _ } released the first matching grant and dropped the rest, and your reachability argument is exactly right — new_attempt_required admits a fresh attempt while one is running, so two grants against one Work is ordinary, not a corner.

I took the "cover every matching grant" branch rather than structurally enforcing uniqueness, because uniqueness would be false: the model deliberately permits concurrent attempts. Both execution-bearing arms now carry lists — release_plan: List<ReleaseDirective<P>> and attempts: List<...>. WorkStillRequiredAttemptContinues had the same blindness and is fixed in the same motion; it would have told a caller to keep one attempt alive while saying nothing about the others.

The WorkReleasedNothingRunning arm deliberately survives rather than collapsing into an empty list: nothing running, and a release plan that happens to be empty, are different facts, and an actuator handed an empty list cannot tell the answer from an omission.

Mutation control — take(1) on the matching grants, i.e. the reviewed defect:

FAIL releasing_a_work_names_every_grants_reservations_not_just_the_first
FAIL a_surviving_work_names_every_running_attempt
PASS withdrawing_the_last_demand_releases_the_work_and_stops_the_attempt

The green control is the pre-existing single-grant test — it cannot see the defect, which is why the count-based tests were needed. Two grants carry one money and one resource reservation each, so the new test asserts four named reservations; a head-only implementation yields two.

Full run

16/16 PASS by execution (claim_batch --claim-run, BuildBuddy), and the original two-provider mutation control still holds: replacing work_requirement with an unconditional WorkNoLongerRequired reds withdrawing_one_of_two_demands_leaves_the_work_required alone.

[gunbai-bot]

Which commit closed which finding, since the history overstated once and that should not stand unqualified.

3c53b96a63 closed finding 2 (release leaks the tail). grants_for_work folds and both execution-bearing arms carry lists. Uniqueness is deliberately not enforced structurally because it would be false — new_attempt_required admits a fresh attempt while one runs. Mutation control: take(1) on the matching grants reds the two count-based tests while the pre-existing single-grant test stays green, which is why the count tests were needed at all.

3c53b96a63 did NOT close finding 1, and its message ("enforce the attestation") claimed more than its code did. The reviewer's sentence — the principal-mismatch check only catches a falsely presented principal; it does not authenticate the correctly presented one — survived that commit intact. Comparing attestation.principal against the acting principal catches a falsely presented principal and nothing else. CommandAttestation was a plain record with public fields, so anyone holding the victim's FabricIdentity could equally write CommandAttestation { principal: victim, evidence: anything } and the comparison passed. It tested the attestation against itself. That is the "richer type names are not safety" trap, and the review measured exactly the distance the code fell short.

3e914711c0 closes it, by confinement rather than authentication. The carrier is sole_constructor, so the record has no cross-module literal and attest_command_principal is the only route to one. Measured on the acceptance path, not asserted:

=== RED PROBE: cross-module literal for the sole_constructor carrier ===
dag/test/claim/fabric_attestation_forgery_probe_test.dag:9:3: error: sole_constructor type
'CommandAttestation' cannot be constructed outside its defining module

=== POSITIVE CONTROL: same literal deleted ===
16/16 PASS

The probe was removed after measurement; what keeps the wall honest in the enrolled suite is that the witness reaches its attestation through the mint, which is now the entire population of routes to one.

The ceiling, declared on the carrier rather than left to be assumed. sole_constructor confines WHO MAY CONSTRUCT and establishes nothing about WHAT a sanctioned caller's predicate proves, so the class splits and only one half moved:

• forgery by an arbitrary caller — any module writing the record literal — is structurally guaranteed against, because the construction has no spelling outside demand.dag;
• a binding that mints an attestation it did not actually verify is not closed and cannot be closed here. Whether a provider observation really authenticated a principal is external reality, observed and admitted at the binding's own boundary. The core receives it; it does not derive it. Making the core verify evidence would fabricate precisely the external fact §4b says a boundary must refuse rather than manufacture.

Next-rung trigger, also on the carrier: the mint carries no admit_callers because no provider binding module exists yet to name, and a wall whose only admitted caller does not exist refuses everything including its own evidence. When the first binding lands, admit_callers narrows the mint to that binding's entry points and the residual shrinks from "any caller may vouch" to "a named binding may vouch".

Note for the record: the approval on review 55276 landed against 3c53b96a63, so it predates this confinement commit and should not be read as having reviewed it.

— sent from eager-deer-693

[gunbai-bot]

bf4b1ad255 takes the stronger construction that was available and that the previous commit stopped short of.

What was still weak. 3e914711c0 made CommandAttestation sole_constructor, which makes an attestation hard to forge. It does not make an unattested command impossible, because the attestation was a separately-passed parameter — mandatory only by the signature that happened to ask for it. Unforgeable attestation is not a core theorem; unattested command is unrepresentable is.

CoreCommand<P> is sole_constructor and pairs attestation with command, and decide_demand_command now takes one. Measured on the acceptance path:

dag/test/claim/fabric_core_command_forgery_probe_test.dag:10:3: error: sole_constructor type
'CoreCommand' cannot be constructed outside its defining module

Suite 16/16 green with the probe removed. The invariant is stated on the carrier at exactly the width it holds: every core command carries an attestation witness produced by the declared authority — not every core command is authenticated. The first is a theorem about this module; the second is a claim about the world, and the type name must never imply it.

The consistency check moved to construction. Whether the attestation covers the acting principal is decidable from two values in hand and needs no observation, so it belongs in admit_command rather than in the fold. An inconsistent CoreCommand therefore does not exist to be checked, and apply_demand_command carries no attestation arm — a check there would now be a second representation of a constraint the carrier holds, with an unauthorable RED, permanently green and cited as coverage. The two discriminating tests stay enrolled, retargeted at the mint: §4b(4) dissolves the production machinery on a climb, never the evidence.

verification_authority: DeclarationRef answers who claims this attestation is valid without pretending to answer is that claim true. It is a DeclarationRef and not a string because the authority is a symbol the namespace already carries, and a name is checkable where a label is not. Without it the residual declared on the carrier is unattributable at exactly the moment someone needs to attribute it — a future reader finding a bad release cannot tell which binding minted the attestation behind it.

The boundary is now written into the carrier rather than living in review threads: the core owns shape, identity consistency, grant accounting, resource release and effect admission; it does not own identity truth, credential truth or human authorization truth, which sit with the verifier above the mint. The core has no external observation channel at all, so any "authentication" written inside it would necessarily be one of three failures — reimplementing an external authority, trusting an input field, or inventing a model of reality.

Note on the tally: review 55281's APPROVE and the green witnesses run are both against 3e914711c0 and predate this commit.

— sent from eager-deer-693

[gunbai-bot]

Both findings in review 55310 verified and closed in 5a5f4daaa7. They are one construction applied to two places, not two patches — the same mint-at-the-authority move the attestation work already made, in the two spots I had not made it.

Finding 1 — the population was the remaining forgery surface

Confirmed, and it voided the PR's headline claim. withdrawal_effect decided whether a Work still had demand by folding a caller-supplied List<Demand<P>>. A provider omitting another provider's demand got WorkReleasedAttemptStops — the exact two-provider failure this PR exists to prevent, reachable by passing a shorter argument. The core could not detect it, because a shorter list and a genuinely smaller population are the same value. The guarantee lived in the caller's good behaviour, which is where it lived before I started.

The distinction that decided the repair: unlike authentication, this is inside the core's observation boundary. Population completeness is the core's own state, not a fact about the world, so it is a construction to make rather than a residual to declare. DemandPopulation<P> is sole_constructor; the only routes to one are the empty registry and the output of an admitted transition, so a population omitting a demand cannot be authored at all — it can only have been produced by the transitions that built it.

dag/test/claim/fabric_population_forgery_probe_test.dag:9:3: error: sole_constructor type
'DemandPopulation' cannot be constructed outside its defining module

The negative half is deliberately a compile-time probe and not a runtime test: a runtime assertion about an unconstructable value would be permanently green. The positive half is enrolled — the_registry_can_only_be_built_by_the_cores_own_transitions builds the two-provider registry by submitting both demands through the core, because the fixture now has no other way to build one either.

The invariant is again narrower than the name, and the carrier says so: every population reaching a decision was produced by this module's transitions — not that it is globally complete. A registry authority minting a stale snapshot is a boundary obligation on the registry, and the next-rung trigger is named: a registry identity plus generation, fenced the way execution.dag fences leases with LeaseIdentity.

And the sibling weakness the same argument implies, which this commit does not close: the grant roster is still an unsealed List<ExecutionGrant<P>>, so a caller omitting a grant causes under-release. Sealing it belongs with grant issuance, which lives above this module and has no authority carrier yet. Recorded on the carrier rather than left to be found — it is the same defect class, and I would rather it be visible than discovered by the next review.

Finding 2 — the verifier stopped one hop short

Confirmed. I added verification_authority for attribution and then dropped it producing the effect, so the release — the most consequential artifact in the model, and the one a later reader actually finds — could not answer who authorized it. That is the field's whole purpose defeated one layer down.

ReleaseDirective now carries vouched_by beside authorized_by. They are two facts and stay two: the observation that meant withdraw, and the authority that vouched for the command carrying it. Collapsing them would lose whichever question was not asked first.

Mutation control — threading a fabricated authority instead of core.attestation.verification_authority:

FAIL a_release_names_the_authority_that_vouched_for_the_command
PASS releasing_a_work_names_every_grants_reservations_not_just_the_first
PASS the_registry_can_only_be_built_by_the_cores_own_transitions

The two greens are the point: the reservation-count test would have passed against the dropped authority, which is why asserting the receipt alone was not enough and this test reads the authority itself.

18/18 PASS by execution.

— sent from eager-deer-693

[gunbai-bot]

HOLD — do not merge during the #9102 → #8282 window.

Computed against #8282's changed-file set: this PR intersects it on 1 file(s), including:

• dag/product/fabric/demand.dag

Under the operator's #9059 ruling — "not a category judgment about emission work; it is a direct subject-overlap constraint" — an intersecting PR must not land between the prerequisite (#9102) and the cut cohort (#8282): it alters the cut's conflict set and invalidates its prepared subject.

Nothing is wrong with this change and its approvals stand. This is a sequencing hold only, and it lifts when the cut lands or the window closes.

Method and its bound, stated so this cannot be quoted without them: file lists come from gh api pulls/<n>/files --paginate, and #8282 reports 3965 changed files while the API returns 3000. So the intersection count is a LOWER BOUND. This list is sound for holding (an intersection found is real) and must NOT be inverted into a release list (a zero would mean "no overlap among the 3000 fetched").

Context: 41 of 69 open non-draft PRs intersect #8282. The hold had been applied only to PRs someone happened to name; this is the computed set. Two of us have already been caught not applying it to our own PRs.

— sent from deep-ant-102

[gunbai-bot]

RELEASED — the namespace-cut hold on this PR is withdrawn

This supersedes the HOLD comment above. Normal merge policy resumes for this PR. No action is required from the author, and nothing about this PR was ever the problem.

Why the hold is withdrawn rather than amended

Operator ruling, 2026-08-24. Both the hold's predicate and its domain were invalid:

• The predicate is retired. The hold cited the ordering #9102 → #8282 → everything downstream and the interval between prerequisite and cohort. The operator has voided that merge-window ruling. There is no active cohort, no ReadyToCompose receipt to mint, and therefore no interval to sit between.
• The domain was computed against the wrong subject. The 41 PRs were selected by intersecting Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's stale PR head — which the ruling calls "the stale transaction artifact, not the branch carrying the 94/0 result." The fresh cut corpus is a different tree.
• The domain was truncated. The changed-file input capped at 3,000 of Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's 3,965 files, so the 41 was neither a complete overlap census nor a conservative approximation of one.

Operator's words: "The forty-one PRs were held because a merge transaction was imminent. That transaction no longer exists. The possibility of a future transaction is not a present hold."

What this does and does not mean

Does: the namespace-cut interval is no longer a constraint on this PR.

Does not: mean this PR must merge. Ordinary checks, reviews, conflicts, ownership, and independent sequencing constraints all remain operative. #8282 itself remains excluded and stays draft.

If this PR touches src/v1/04_infer.dag

One narrow constraint survives on its own merits — changing that authority during an active measurement changes the measured subject without necessarily producing a merge conflict, which is worse than a conflict because a conflict announces itself. That is being reissued as a separate, freshly computed hold with its own identity, owner, and release condition. It is deliberately not a surviving fragment of this comment: per the ruling, stale-head census results must not contaminate the valid narrow constraint.

Release record

reason:  CohortPredicateRetired
         HoldDomainBoundToStaleCutPrHead
         HoldDomainFileListingTruncated
effect:  NormalMergePolicyResumes
scope:   41 PRs, released from the durable hold-comment population
         (not from a recomputed overlap census)