feat(2c-F): the Def 14.2 SofiReceipt — frozen rulings, 0x0034, and a publication obligation that never gates the release

[cryptskii]

Merged without its merge-condition fix. This PR merged at f29284c5 (2026-09-11T10:09:25Z, squash 4d24ba2e). The section "Merge condition — a lost obligation is never lost" and the matching verification rows below describe commit f0b14ac2, which landed on this branch after the merge and is not in main. It ships cherry-picked, unchanged, in #860. Until #860 merges, main has the behaviour the owner blocked on: a failed receipt freeze followed by a release and a crash loses the Def 14.2 publication obligation.

2c-F — the Def 14.2 settlement receipt, frozen and implemented

This implements the owner's 2026-09-11 rulings on the 2c-F draft (#858). The first commit freezes them: they are recorded verbatim in docs/papers/amendment-2c-f-sofi-receipt-rulings.md and carried into the spec and the registry. The later commits implement them. There are no other changes.

Rulings → implementation

Ruling	What it says	Where
R1	Ratify the shipped X = H(DSM/ext ‖ RC*). No bytes move. Q is the signed RouteCommit that B already carries. 0x000C and 0x0017 are burned.	ccb/mod.rs; registry §2.10 (exception 2), §3, §5.12, §5.14; spec §7.2, §9.3, §16.2
FB-4	B's pre-bind durability stays pre-bind. "After certification" applies to the SofiReceipt only.	spec Req 14.7
R2	New tag DSM/sofi-receipt/v1. DSM/receipt stays the stitched receipt, which signed tombstones already depend on.	domain_tags/dsm/core.rs
R3	successor_hash = c_{n+1}. witness_hash is always absent in schema 1, and proof material never refuses a receipt.	dlv/sofi_receipt.rs
R4	0x0034 SofiReceipt schema 1, 137 bytes.	registry §5.42; class-1 vector
R5	Quorum is counted over the authenticated consumed parent's S_v, never a set read off B. B's existing durability counts when it was achieved over that set.	sofi_receipt_publication.rs; complete_settlement freezes for composed.storage_set_id
R6	The receipt never gates fence release. It is built only after certification, and may publish after the release. Failure leaves a recoverable obligation and never re-fences, re-binds, re-admits or re-certifies.	complete_settlement; DSMSofiReceipt.lean
R7	Nothing reads the receipt or its publication state as authority.	module headers; publication() is a report only

R2, R4 and R7 had no competing option in the draft. They are adopted as proposed and are open to objection before merge.

How the obligation works

After the walk certifies exactly b, complete_settlement projects the receipt from the certified fold's own TA_B. The fold now carries it as certified_acceptance. The pass then freezes {receipt, CCB(B), CCB(TA_B)} for the composed V_n's committed set, before the release step. The generic sweep publishes those exact bytes. A projection or freeze failure is logged, never returned, so C2's release condition is unchanged. A receipt can only be built from a certified fold, because the acceptance it binds exists nowhere else.

One set per frozen row (I-5). If TA_B was admitted under a different set than S_v, publication() reports BoundToAnotherSet rather than counting that set's quorum. In beta every consumer resolves the one catalog set, so this case cannot occur. Per-set rows are left owed.

Mutation controls — executed

#	Mutation	Named test red
MS1	the release waits for the receipt at quorum	the_def_14_2_receipt_never_gates_the_release_and_publishes_after_it
MS2	the closure is frozen for a set the vault does not commit	a_realized_settlement_publishes_its_def_14_2_receipt_on_the_vaults_set
MS3	the receipt binds an a_B other than the certified acceptance's	the same (at verify), and a_closure_is_a_pure_projection_of_its_inputs
L1	Lean: the release also waits for the receipt	the_release_does_not_wait_for_the_receipt proved false
L2	Lean: the obligation is created without certification	an_uncertified_settlement_has_no_receipt proved false

Each source was restored from a byte copy and verified with cmp. The first attempt at MS3 did not compile (an unused binding), so it was discarded and re-run with a mutation that compiles; the table shows the re-run.

Merge condition (owner, 2026-09-11) — a lost obligation is never lost

In the first version, a failed receipt freeze was logged and the fence still released. D-f lists only unreleased fences, and the sweep replays only rows that are already frozen. So a failed freeze followed by a release and a crash lost the obligation. The owner's question — what durable state lets a restarted process rediscover it — was answered from source before any code changed (2c-F §7.3):

• The released trader fence is the durable certification record. Released is reachable only through SuccessorAccepted, whose sole production caller is the certified completion. Fence rows are never deleted, and the row 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.

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 from those facts:

• 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 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.

Owner's test	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	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

Verification

All runs used the pinned 1.98.0 toolchain and --release, targeted by module per project policy. CI is the board.

Check	Result
make lint (fmt + clippy --all-targets)	pass — see the note below
ci/production_safety_checks.sh	pass (run twice: before and after the lint fixes)
dsm lib: sofi_receipt, domain_tags, ccb::	pass (12 receipt tests on the final tree)
dsm settlement_bundle_conformance (full binary)	pass, including the new 137-byte receipt vector and the namespace test
dsm route_commitment_x_conformance (new)	2/2
dsm_sdk lib: handlers::dlv_routes, sdk::vault_state_composition, handlers::artifact_republish, sdk::sofi_receipt_publication	75 passed, 0 failed
dsm_sdk dlv_regression_guards + vault_funding_routes	3/3 + 12/12
Lean DSMSofiReceipt.lean (-DwarningAsError=true, v4.23.0)	OK; axioms are propext only; no sorryAx
Merge-condition commit: 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

The first make lint failed on rustfmt alone, and that hid clippy. Clippy then found two no-op ..Default::default() struct updates and one needless mut, all in new dsm test code; all three are fixed. The dsm_sdk suites ran on the tree before rustfmt. The only changes since are whitespace and those dsm test-only fixes, and lint, the safety checks and the affected dsm tests were re-run on the final tree.

The existing D-f suite, including the resume test that asserts "every PUT the resume made is the receipt", passes unchanged: the receipt closure is published during the settle pass, not the resume.

Not in this PR

• Per-set frozen rows (I-5). Not needed in beta; outside beta that case is reported, never counted.
• Receipts for settlements completed before this change. Beta is a clean cut, so nothing is backfilled.
• Two docs/plans/2026-04-24-*.md "DeTFi → SoFi" edits that appeared in the working tree from an unknown source. They were left untouched and excluded.