feat(2c-G): owner catch-up — admitted, ordered DlvOwnerApplyV2 behind storage.sync and dlv.reconcile (PR 1 of 3: G1 + G2)

[cryptskii]

PR 1 of 3 for amendment 2c-G (owner catch-up), per the owner's delivery ruling of 2026-09-11. This PR covers rulings G1 + G2: owner catch-up execution. PR 2 (G4, the admitted terminal close) and PR 3 (G3, the re-anchor) follow, each cut from main after its predecessor merges.

The rulings text is frozen in #862, which recovers #861's unmerged freeze commit. This PR does not touch that doc.

What this does

An owner returning to an active DLV now catches up on every certified market settlement traders realized while it was away. Each one is applied oldest first as an admitted DlvOwnerApplyV2, and afterwards the owner's reserve leaves are exactly the composed frontier.

The invariant is: catch-up consumes certified history; it never creates certified history.

• The 0x0027 producer now exists. The composition walk already proved the trader's 0x0021 receipt leaf and its 256-sibling path under the validated R_T^+ when it certified the fold (Req 21.16). It then discarded the path. certify_market_evidence now carries the leaf, the path and the trader coordinates on the certified fold as CertifiedPayment, alongside certified_acceptance.
• settlement_payment_producer projects that payment into SettlementPaymentEvidenceV1. Nothing is fetched again.
  • It mirrors the arm's leaf-equality and inclusion checks, and runs the arm's strict decoder, before signing.
  • The mirror is load-bearing. The arm runs inside finish_admission, after the advance has committed, so evidence the arm refused would strand the admission.
• admitted_dlv_owner_apply (in economic_admission_flow) uses the 0x0027 ValidatedDlvSettlementPayment credit arm, with the evidence frozen in the advance transaction.
  • It shares one admit_reserve_mutation body with funded create, so the staged advance and finish_admission are not duplicated per operation.
• One engine (catch_up_owner_vault_locked) serves both entrypoints:
  • It composes the vault through the same walk a stranger runs.
  • It takes the certified market folds and applies the owed ones oldest first.
  • Consume-once works by settlement identity: a replay is skipped, and a different settlement at a consumed generation stops the run.
  • An interruption leaves every completed apply durable, and the next run resumes after it.
  • owed_certified_folds is pure: Through(x) is exactly the prefix of Frontier that ends at x.
• Automatic on storage.sync. resume_owner_catch_up is the last sync pass.
  • It gates nothing, and failures are local to their vault.
  • It skips outright while another catch-up holds the device lock, and it never calls sync, so there is no re-entrant loop.
• Explicit entrypoint. dlv.reconcile { vault_id, x } now means "catch up through x". It waits on the lock.
  • Behavior change: it used to refuse x when an older settlement was still unapplied. Now it applies the older ones first, in order. The later settlement is still never applied over a state that lacks the earlier ones. The frontend's loop over pendingX is unchanged and still works.
• Core chokepoint. DlvOwnerApplyV2 now requires its own attached Prepared admission in advance.
  • The comment beside the funded-create fence said owner apply was left unfenced until a producer existed. It now exists, so the raw doorway closes.
  • The dependents move to the test-only advance_admitted: six core tests, dlv_owner_apply_preservation, dlv_value_op_signing, and one vault_rehydration test.
• Cleanup. dlv.unlockRouted's doc block was displaced onto dlv_reconcile. It is moved back onto dlv_unlock_routed, which had none.

What this does not do

• No G4. DlvClose / DlvWithdraw are still unadmitted. That is PR 2.
• No G3. No fresh AnchorPresentationV3 is published after catch-up, and Req 6.31 is annotated as owed. That is PR 3.
• Settle's fencing is unchanged.

Formal

lean4/DSMOwnerCatchUp.lean is the 20th module; ci.yml now expects 20. It has no sorry, and its axioms are propext / Quot.sound only. It proves:

• creates-no-history;
• never past certified;
• only-extends;
• ends exactly at the frontier;
• ends exactly after x;
• an uncertified target writes nothing;
• through-last = frontier;
• resume = uninterrupted;
• idempotent.

Mutations, each executed as the kernel proving a named sample's negation, with the unmutated control refused:

• L1: an uncertified target is read as the frontier;
• L2: the goal clamp is removed;
• L3: consume-once is removed.

Tests

Targeted --release runs, each filtered by the edited module's path. These are not the board; CI is.

• dsm types::device_state::tests::: 67/0. This includes the new an_owner_apply_is_refused_without_its_own_attached_admission.
• dsm_sdk integration binaries dlv_owner_apply_preservation (4/0) and dlv_value_op_signing (7/0). These are the chokepoint dependents.
• dsm_sdk lib:
  • handlers::dlv_routes::: 55/0
  • handlers::storage_routes::: 20/0, 1 ignored
  • sdk::economic_admission_flow::: 1/0
  • sdk::vault_state_composition::: 17/0
  • sdk::sofi_receipt_publication::: 5/0
  • sdk::vault_rehydration::tests::: 14/0

New route tests:

• an_offline_owner_catches_up_on_sync_to_exactly_the_composed_frontier. It runs through the real storage.sync and checks that:
  • both entrypoints plan the same history, oldest first;
  • the owner's leaves equal the composed frontier;
  • the consume-once row for each generation names its certified settlement;
  • spendable balance is unchanged;
  • the composed c_n and every trader head are unchanged;
  • a catch-up with nothing owed changes neither the root nor the fleet put log.
• an_interrupted_catch_up_resumes_without_applying_anything_twice.
• a_certified_fold_with_any_fact_altered_is_refused_and_writes_nothing. It covers the receipt leaf, the inclusion path, the parent reserves and the parent generation.
• a_sync_pass_skips_while_another_catch_up_runs.

Updated tests:

• The offline-LP test becomes …_lp_catches_up_oldest_first: an explicit catch-up through generation 1, then the sync pass finishes generation 2.
• The certified-only test now also checks that the sync pass applies nothing uncertified.

The first focused run found a real bug. The engine's ? discarded partial progress, so an interrupted pass reported 0 of its durable applies. The engine now always returns CatchUpReport { applied, already_applied, stopped }. The sync pass counts every durable apply, and dlv.reconcile reports N applied, then stopped.

Mutation controls

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

#	Mutation	Test that goes red
MR8	delete the DlvOwnerApplyV2 arm of the core fence	an_owner_apply_is_refused_without_its_own_attached_admission: the raw apply moved the reserves
MR1	remove the catch-up pass from storage.sync	an_offline_owner_catches_up_on_sync_to_exactly_the_composed_frontier
MR2	empty the producer's leaf-equality refusal	a_certified_fold_with_any_fact_altered_is_refused_and_writes_nothing
MR3	disable the producer's inclusion check	a_certified_fold_with_any_fact_altered_is_refused_and_writes_nothing
MR4	make the sync pass wait on the lock instead of skipping	a_sync_pass_skips_while_another_catch_up_runs (timeout)
MR5	apply newest first	an_offline_owner_catches_up_on_sync_to_exactly_the_composed_frontier
MR6	drop the consume-once skip	an_offline_owner_catches_up_on_sync_to_exactly_the_composed_frontier
MR7	drop the Through(x) truncation	lp_offline_market_advances_three_generations_and_lp_catches_up_oldest_first

The first MR2 was an invalid mutation and stayed green. It read false && a || …, and operator precedence meant only the first two comparisons were disabled. The corrected control empties the refusal branch and goes red.

Gates:

• make lint: exit 0. The single eslint warning is in frontend code this PR does not touch.
• ci/production_safety_checks.sh: exit 0. This includes clippy with the production lints and TLA+.

Docs

• sofispecs.instructions.md: the Req 4.5 implementation note, and the Req 6.31 status (the baseline is owed by G3).
• ccb-object-registry.md §5.37: the producer and the chokepoint.