feat(2c-G): the admitted terminal close — one commit path that derives every close fact from the composition (PR 2 of 3: G4)

[cryptskii]

PR 2 of 3 for amendment 2c-G, per the owner's delivery ruling of 2026-09-11. This PR implements G4: the admitted terminal close. It is cut from main after PR 1 (#863) merged, and PR 3 (G3, the re-anchor) follows once this one merges.

What this does

The close now runs on PR 1's economic-admission foundation rather than beside it.

The close is admitted.

• admitted_dlv_close goes through the same admit_reserve_mutation body that funded create and owner apply use. Its facts are fixed at CreditSourceFacts::None: the builder derives the two 0x0024 same-transition-move credits itself.
• The write set drains exactly the owner's admitted reserve leaves at exactly the parent generation, and credits balance from them. The proceeds now exist in R_econ.
• Before this PR, a close credited the head only. The R_econ reserve leaf was never withdrawn, so close proceeds could fund no admitted operation.

The one close commit derives every fact from the composition. commit_canonical_close is shared by dlv.close and by the resume pass. It now takes only (vault_id, composed, close_commitment, op). A new pure function, close_plan:

• reads the parent, generation, reserves, parent binding and storage set off the composed vault state;
• holds the signed operation to them field by field;
• refuses a close whose parent a realized market successor already consumed ("a close may not erase it");
• refuses when later generations exist, or when the named generation lies beyond the frontier;
• refuses when another candidate holds the parent unrealized (an uncertified predecessor).

No caller supplies a reserve, generation, parent or storage set any more. finish_prepared_close keeps its resume-specific checks: the kind, the terminal commitment, and this device's fence identity. Its parent-binding derivation moves into close_plan.

Core chokepoint. advance now refuses a DlvClose that has no attached Prepared admission, as it already does for funded create and owner apply.

• The fence check runs before the chokepoint. A raw close on a head holding a fencing admission is therefore still refused by the fence itself, and advance_refuses_an_economic_write_while_an_admission_is_pending is unchanged.
• Dependents that now use the test-only advance_admitted:
  • six core close sites;
  • that test's positive control;
  • the table-driven malformed-close loop.
• The pattern sweep missed the table-driven loop, and the module run caught it. The sweep found no raw DlvClose advance outside device_state.rs.

Close before catch-up still refuses, as the survey recommended.

• The route's frontier gate is unchanged: composed generation, reserves digest, storage set and occupancy.
• The owner catches up first, through storage.sync or dlv.reconcile. That catch-up consumes the certified frontier and is not approval of it.

Boundaries kept (G4 ruling)

• Close authority stays the owner's, verified against the parent's committed authority.
• QuorumBind, the accepted-successor rules and close-auth are untouched.
• A terminal close remains distinct from market realization.
• Nothing here adds a dependency for trader settlement.

Not in this PR

• G3, the fresh AnchorPresentationV3 after catch-up, is PR 3.
• Settle's core fencing is unchanged.

Formal

lean4/DSMAdmittedClose.lean is the 21st module, and ci.yml now expects 21. It is sorry-free and uses only the propext and Quot.sound axioms. It proves:

• an admitted close requires the owner caught up;
• it consumes exactly the frontier and drains exactly its reserves;
• a held parent refuses the close;
• a refused close writes nothing;
• a close never erases the realized history;
• a second close is refused;
• a caught-up exact close is admitted.

Three mutation controls each make the kernel prove a named sample's negation, and the unmutated control refuses it:

• L1 drops the caught-up precondition.
• L2 drops the held-parent check.
• L3 accepts any earlier parent at its own reserves.

Tests

These are targeted --release runs, filtered by the module path of each edited module. CI is the board.

• dsm types::device_state::tests::: 68/0. This includes the new a_close_is_refused_without_its_own_attached_admission and the dependents moved to advance_admitted.
  • The first run was 67/1. The table-driven every_malformed_close_is_refused_with_zero_mutation drives its cases through one raw .advance(case.op …). My pattern-matching dependent sweep could not see that call; the module run caught it. The fix gives each case its own admission, so every case is refused by the check it names.
• dsm_sdk lib:
  • handlers::dlv_routes::: 57/0. This covers every existing close, resume and catch-up test, plus the two new ones:
    • close_plan_takes_every_fact_of_a_close_from_the_composition. It checks the exact plan, then six named refusals: stale baseline, skipped generation, older parent with later generations realized, altered reserves, another vault, and uncertified predecessor.
    • a_close_below_the_gate_drains_exactly_the_caught_up_frontier_or_nothing. It drives the one commit below the gate:
      • a close of the stale baseline is refused by close_plan;
      • a close of the uncaught frontier is refused by the admitted advance;
      • neither writes anything (checked: root, spendable balance, leaves, consume-once claims);
      • after the sync pass catches up, the route close succeeds, and its proceeds fund an admitted create that the pre-close admitted balance could not.
  • sdk::economic_admission_flow::: 1/0
  • handlers::storage_routes::: 20/0 (1 ignored)
• The existing a_contested_parent_refuses_the_close_and_moves_nothing still covers the uncertified predecessor at the route: a rival bound at quorum and never realized.
• Lean: 21/21 modules.

Mutation controls

Each mutation is applied to a byte copy of the source file. A named test is run against it, and the file is then restored and checked byte for byte.

#	Mutation	Test that goes red
G1	delete the DlvClose arm of the core fence	a_close_is_refused_without_its_own_attached_admission
G2	let close_plan fold from a MARKET-consumed parent	close_plan_takes_every_fact_of_a_close_from_the_composition: "the stale baseline must not plan"
G3	accept a parent another candidate holds unrealized	the same test: "an uncertified predecessor must not plan"
G4	drop close_plan's field-equality check	the same test: "altered reserves must not plan"
G5	commit through the unadmitted staged advance, with the core fence arm removed	a_close_below_the_gate_drains_exactly_the_caught_up_frontier_or_nothing: the proceeds-funded create is refused, because the proceeds never reached R_econ

The first two versions of G2 and G3 were invalid: they failed to compile rather than running. dsm_sdk is #![deny(warnings)]:

• An arm made unreachable is a compile error.
• An if true guard that drops the only use of BundleShape leaves an import unused, which is an error.
• A guarded or-arm does not count toward exhaustiveness.

My first runner keyed compile detection on error[ and missed these errors, which carry no code. It now treats any could not compile as an invalid control. The third definitions keep the import used and put a guarded arm ahead of the untouched ones. Both compile and go red.

Gates:

• make lint: exit 0. The one eslint warning is in frontend code this PR does not touch.
• ci/production_safety_checks.sh: exit 0. This covers clippy with production lints, plus TLA+.

Docs

• sofispecs.instructions.md: an implementation note under Req 6.30.
• ccb-object-registry.md §5.34: the 0x0024 producers, and the close now being admission-fenced.