fix(2c-F): a lost receipt obligation is rediscovered after release — the #859 merge condition

[cryptskii]

The #859 merge condition — a lost receipt obligation is never lost

Why this is a separate PR. The owner's ruling made this change a precondition for merging #859. #859 merged at f29284c5, but this commit (f0b14ac2) reached the branch after the PR object's head was fixed, so it is not in main. ./scripts/check-pr-head-sync.sh 859 reports exactly that divergence. This PR carries f0b14ac2 cherry-picked unchanged onto main, following the recovery the script prescribes, as was done for #699 and #701.

Until this merges, main has the behaviour the owner blocked on: a failed receipt freeze is logged, the fence releases, and a crash then loses the Def 14.2 publication obligation.

The question, answered from source before any code changed (2c-F §7.3)

After certification, a failed receipt write, a release and a crash — what durable state lets the next process discover the owed publication?

• The released trader fence is the durable certification record. Released is reachable only through SuccessorAccepted carrying the exact permitted successor. Its sole production caller is complete_settlement's release step, which runs only after may_certify() for exactly b. Fence rows are never deleted, and each carries addr(B) and the bind set.
• CCB(B) has been at quorum since before binding.
• This device's own admission froze TA_B and its locator locally.

Nothing read those facts for this purpose: D-f lists only unreleased fences, and the sweep replays only rows already frozen.

The mechanism

recover_owed_receipts runs from storage.sync, beside D-f. For every released fence on the device's own market chain that has no receipt row for b, it rebuilds the byte-identical closure:

• B is fetched by b and must sit at the fence's addr(B).
• S_v is the fence's set, and must equal the set B's successor commits.
• TA_B is this device's own, re-hashed, and must accept exactly b.

It never composes, binds, advances, admits or touches a fence, and needs no signing key. The three-row closure freeze is now atomic (a savepoint), so a receipt row always means all three are recorded. The fence still never waits on any of this, as ruled.

Tests (the owner's A–J)

	Where
A–H, J	a_receipt_whose_freeze_failed_is_recovered_after_release_and_restart: an injected freeze failure; the fence still releases; a second router over the same database recovers a byte-identical receipt; it is published on the vault's set; a second pass does nothing; fence, frontier, head and binding log are unchanged
I	a_recovered_receipt_cannot_be_rebuilt_from_substituted_facts: another addr(B), another storage set, or a locator naming another bundle's acceptance are each refused, with nothing frozen
atomicity	a_closure_that_fails_part_way_freezes_nothing

Mutation controls — executed

#	Mutation	Named test red
MR1	the rediscovery hook removed	the restart test: "exactly the one lost obligation is rebuilt"
MR2	the acceptance need not accept exactly b	the substitution test, at the locator case
MR3	the fence's set need not be the one B commits	the substitution test, at the storage-set case
MR4	B need not sit at the fence's addr(B)	the substitution test, at the bundle-address case
L3	Lean: recovery removed	a_lost_obligation_is_rebuilt_after_release proved false

Each source was restored from a byte copy and checked with cmp.

Verification (pinned 1.98.0, --release, targeted)

Check	Result
dsm_sdk recovery, receipt, D-f, fence, frozen-artifact, register and republish filters	39 passed, 0 failed
handlers::storage_routes (sync now runs the recovery pass)	20 passed, 1 ignored (pre-existing)
dlv_regression_guards + vault_funding_routes	3/3 + 12/12
make lint + ci/production_safety_checks.sh	pass (run after the mutation controls)
Lean DSMSofiReceipt.lean with freeze failure + recovery	OK; L1–L3 each prove their named sample false

CI is the board.