INTAKE-AGENT-0A: an observed duplicate is refused; completeness is not claimed; the receipt's architecture is checked

[gunbai-bot]

INTAKE-AGENT-0A, the slice covering ruling 3's exit point 3 (replay and duplicate-callback refusal) and the wrong-architecture half of exit point 4. Both invalid states were authorable and silently attested.

The title's original claim — that the nonce's one-time-ness is checked — is withdrawn. What is checked is that an observed duplicate is refused. One-time-ness itself is a property of a closed callback population, and this repository has nothing that can close one; see What is definite and what is not, below. The body promised more than the diff delivers, and a merged body that overclaims outlives the diff.

Duplicate callback

attest_diagnostic_boot took ONE optional receipt. IntakeAttemptNonce is documented as a one-time callback token, but an optional cannot express the state that makes it one-time — a second callback bearing the same nonce — so a replay was not merely unrefused, it was unrepresentable.

It now takes the list of callbacks observed for one issuance. More than one is DuplicateAgentCallback { received } on a DiagnosticBootNotAttested { cause, population_evidence } wrapper, and a duplicate is refused even when the two callbacks are byte-identical: picking one of two to honour is an absorbing fallback (DESIGN §5) — widening on ambiguity instead of stopping the line. Cardinality is read before any callback is inspected, because a replay is a fact about the population and not about any one receipt.

What is definite and what is not

Review 57762 and the reviewing authority independently found that the list's completeness was still the caller's assertion: observed_agent_callback_population is publicly callable and accepts the callbacks and the acquisition evidence independently, so a caller handed [r1, r2] can pass [r1] with the evidence for both. sole_constructor stops the record literal being written elsewhere; it does not constrain who calls the mint or where they got the list.

The knife is monotonicity under hidden callbacks — whether a reading survives every completion of the population:

observed	conclusion	survives completion?
more than one	DuplicateAgentCallback	yes — a hidden sibling only makes it more true
exactly one, mismatching	field refusal	yes — any hidden sibling would itself be a duplicate, also a refusal
exactly one, matching	—	no — a hidden sibling makes it a replay
none	—	no — a caller can prefilter a real callback to zero

So the two indefinite readings no longer produce a verdict. DiagnosticBootAttestation is three-valued, and the third arm, DiagnosticBootCompletenessUnestablished { observed_callbacks, population_evidence, supporting }, reports what was seen and the record it was seen in. Collapsing it into either neighbour is state_space_conflation: into refusal it reports a boot as failed on a caller's filtering decision; into attestation it reports one as proven on the same.

AgentReceiptAbsent is deleted. Reading "the agent never called back" off a list's length is a claim about the world drawn from a caller's filtering decision. It returns with the producer that can close a population.

DiagnosticBootAttested is constructed by nothing, deliberately

No path in this repository constructs it, and that is a declared terminal state rather than dead code — do not delete it as unreachable. It is the terminal the intake transaction requires, held at its honest arity, declared here so the future producer has one authority to satisfy instead of a shape invented later. population_evidence is on it because the durable-provenance half of the design is already settled.

Its next-rung trigger is the annotation on attest_diagnostic_boot, under RUNG, HONESTLY, and it names a capability, not an artifact: an acquisition producer that closes a population — exact issuance identity, the exact callbacks, evidence derived from that same acquisition rather than passed beside it, and a declared closure boundary or one-shot nonce consumption. Producer identity alone is insufficient: without the closure boundary a producer can mint a singleton after the first callback and accept a second afterwards.

Architecture

IntakeAgentBootReceipt.architecture was carried into the attestation and never compared with anything, so an x86-64 agent callback attested an AArch64 unit's issuance. The architecture is a fact ABOUT the issued artifact, so it lands on the artifact beside the digest that names it, rather than being re-derived from the receipt it is meant to check. Refusal is ArchitectureMismatch { expected, received }.

BootArtifact and its neighbours moved to a new leaf authority, gunbc.boot_artifact: issuance must carry the artifact it issued a nonce for, and gunbc.boot_artifact_delivery already imports the receipt module, so importing back would have closed a cycle. Ordinary single-authority relocation — nothing is defined twice at any point. It produces five TargetChanged binding deltas, adjudicated by five exact (module, declaration, spelling) rows with blast radius 0 and a dissolve-on-merge trigger.

Evidence

Every witness in test.claim.machine_intake_disposition_witness_test returns true under gunbc run. The controls discriminate on the live adjudication path — not the acceptance path, since nothing constructs DiagnosticBootAttested — proven by MUTATION rather than rested on green:

• replacing the architecture comparison with (true) turns an_agent_on_the_wrong_architecture_does_not_attest_the_boot false;
• disabling the received > 1 refusal turns a_second_callback_on_one_nonce_is_a_replay_not_a_boot false.

Provenance is on the wrapper, so the claim is true by construction. An earlier cut carried the acquisition record on DuplicateAgentCallback and on the unestablished arm, annotated as "every outcome names the population it was read from" — which was false for the four field mismatches, and the control greened anyway because it only exercised the unestablished path. population_evidence now sits on DiagnosticBootNotAttested, so no adjudication path can return without it, and a_definite_refusal_carries_the_acquiring_record_it_was_read_from reads the arm that was actually lying, using two definite BoardSerialMismatch refusals differing only in their acquisition record.

One nonce constructor was answering for two failures. A population bound to another issuance is an acquisition splice, produced by whoever assembled the input; a callback returning the wrong nonce inside a correctly bound population is agent content. Different producers, evidence locations and remedies, now CallbackPopulationForOtherIssuance and AgentCallbackNonceMismatch. Neither carries the nonce — it is a secret with no place in durable output — so the cause names which comparison failed and the wrapper says where to look.

a_matching_callback_is_unestablished_and_a_wrong_nonce_refuses reads the asymmetry directly: from the same call, differing only in the callback, a match yields Unestablished and a wrong nonce yields a definite refusal. an_outcome_carries_the_acquiring_record_it_was_read_from uses two populations identical in every way except their acquisition record, so it reads the field rather than checking that some constant is present.

Not in this slice

Exit points 1, 2, 5, 6 and 7 (deterministic per-architecture artifacts with content identities, canonical durable receipt bytes and their SHA identity, raw EDAC/RAS capture, local execution without a physical BMC) are untouched here and remain open.

[gunbai-bot]

Review 57762's finding is correct and I have reworked rather than defended — the reviewing authority in my side chat reached the same conclusion independently and pushed it further. Pushed on the new head.

The finding: observed_agent_callback_population (was agent_callback_delivery_batch) is publicly callable and takes the callbacks and the acquisition evidence as independent arguments, so a caller handed [r1, r2] can pass [r1] with the evidence for both. sole_constructor stops the record literal being written elsewhere; it does not constrain who calls the mint or where they got the list. The old name asserted a property the construction did not hold.

What I did not do is bind the mint to a producer that does not exist. Instead the outcome type now says only what is definite, and the test is monotonicity under hidden callbacks — whether a reading survives every completion of the population:

• received > 1 survives: a hidden sibling only makes a duplicate more true.
• A field mismatch survives: any hidden sibling would itself be a duplicate and also refuse, so every completion refuses.
• One matching callback does not survive — a sibling turns it into a replay.
• Zero does not survive — a caller can prefilter a real callback to zero exactly as easily as a duplicate to one.

So the two indefinite readings no longer produce a verdict. DiagnosticBootAttestation is three-valued; DiagnosticBootCompletenessUnestablished reports what was observed, the record it was observed in, and the supporting activity. AgentReceiptAbsent is deleted — reading "the agent did not call back" off a list's length was a claim about the world drawn from a caller's filtering decision.

DiagnosticBootAttested is now constructed by nothing in the repository. That is deliberate and declared, not dead code: it is the terminal the intake transaction requires, held at its honest arity. Its trigger names the capability — an acquisition producer that closes a population, with a declared closure boundary or one-shot nonce consumption, since producer identity alone still lets a producer mint a singleton after the first callback and accept a second afterwards.

The PR title and body claimed one-time-ness is checked. That claim is withdrawn in the body text; what is checked is that an observed duplicate is refused.

31 witnesses green by execution. Two changed meaning rather than shape, and the separate CI red was namespace-wave-admission (floor was FloorClean), fixed with five exact transition-admission rows for the BootArtifact relocation.

— sent from silent-crab-842

[gunbai-bot]

Review 57801 is right on both halves — the rows do expand hand-written compiler Rust, and a dissolution condition alone does not authorize growth (DESIGN §6). Receipt filed on the roster row itself, in the shape #9436 filed for the 53-row cut, measured rather than argued:

• git diff --numstat origin/main -- src/v1/stage0/src/namespace_wave_admission.rs → 65 added / 1 removed. Of the added lines, 16 are the justification and 49 are the five row literals; the single removed line is the const's own = &[];, reopened as = &[.
• grep -cE '^(pub )?(fn|struct|enum|const|static) ' → 38 on origin/main, 38 here. No function, type, const, capability or mechanism is added. The rows are data consumed by the already-rostered NAMESPACE_TRANSITION_ADMISSIONS declaration, from an authored literal with no scan, file read, environment read, or computed predicate. Expansion in maintained lines only.

On the framing: these rows are not a scaffold standing beside the wall, they are the wall's required input. The roster's own rule is that a run carrying a real namespace delta refuses it as UNADJUDICATED until its author adds a row — empty is not permissive. The relocation was forced by §4 acyclicity (issuance must carry the artifact it issued a nonce for, and boot_artifact_delivery already imports the receipt module, so importing back closes a cycle), so it has exactly one sanctioned way to land. Declining to author the rows would not reduce hand Rust; it would leave the relocation unmergeable.

The change that would reduce it is migrating the roster's pure fold to .dag, and that is blocked upstream on ModuleDeclarationRecord / DeclarationIndex having no .dag carrier — which this module's own CLASS A justification already names as its trigger, and which authoring one here would fork away from gunbc.declaration_index_seed_growth. So the honest deferral is to that existing trigger, not a new one.

Each row is stale the moment this PR merges, and a stale row reds every unrelated PR in the repository — so the deletion is enforced by the same wall rather than by anyone remembering. That mechanism is why the count has returned to zero seven times in the ledger above.

— sent from silent-crab-842