docs(2c-F): Def 14.2 settlement receipt — survey and rulings draft (FOR RULING) - #858
Merged
Merged
Conversation
…or owner ruling
A survey of the four blockers on the Def 14.2 receipt and Q publication, with a
proposed smallest ruling for each. Nothing is frozen, nothing is implemented,
and no registry row or domain tag is changed: this is returned for ruling.
- X: Rev 15 says H(DSM/route-set ‖ CCB(Q)); the shipped X is
H(DSM/ext ‖ signature-cleared RouteCommitV1), signed by two parties and carried
in b. Recommends ratifying the shipped X (no bytes move). The shipped Q preimage
is already inside b via 0x0031's operation bytes.
- DSM/receipt: already hashed into recovery rollups that are sealed in capsules
and signed in tombstones. Recommends a fresh DSM/sofi-receipt/v1 for the new
class only.
- Set members: successor_hash_v = c_{n+1}; witness_hash_v absent in schema 1;
publication set is exactly {receipt, B, TA_B}; lineage by reference.
- Registry: proposes 0x0034 SofiReceipt schema 1 (137 bytes), not applied.
Also records that "Q" (the route-commitment body) and "q" (the quorum) were
conflated, and five incidental findings (stale TradeIntent field references in
registry §5.13/§5.14 among them).
cryptskii
marked this pull request as ready for review
September 11, 2026 08:45
cryptskii
added a commit
that referenced
this pull request
Sep 11, 2026
…publication obligation that never gates the release (#859) * docs(2c-F): freeze the Def 14.2 rulings — spec, registry and amendment The owner ruled 2026-09-11 on the draft merged as #858. This records the rulings verbatim and carries them into the normative text, before the code that implements them. - 2c-F: status FROZEN; the four answers quoted; two corrections applied in place — S_v is the authenticated consumed parent's committed set, never one read off B's proposed successor, and proof material never refuses a receipt. Recovery replays the frozen bytes and never re-certifies. R2, R4 and R7 had no competing option and are adopted as proposed. - Spec: Def 14.2 is SofiReceipt with rho_B under DSM/sofi-receipt/v1 and the publication set {receipt, B, A_B}; Req 14.6-14.10 (quorum over the authenticated S_v, ordering, determinism, recovery, non-authority); §9.3 and §7.2 ratify X = H(DSM/ext ‖ RC*); §16.2 re-quotes instead of retrying a pre-committed alternative; the tag table retires DSM/route-set. - Registry: 0x0034 SofiReceipt (§5.42, 137 bytes); 0x000C and 0x0017 burned; §2.10 names RC* as a second foreign grammar, on its own ground; §4 counts; stale TradeIntent field citations (I-1) and schema headings (I-2) corrected. - 2c-D: C2-R1 point 9 marked discharged; I-3 (the Rev 15 text is in-repo). - 2c-A Ruling 2: Q is the signed RouteCommit that B already carries. * feat(2c-F): SofiReceipt 0x0034 — the Def 14.2 receipt as a projection of (B, TA_B) dsm::dlv::sofi_receipt: a pure projection of the canonical market bundle and the certified acceptance identity — b, X, a_B, and one successor commitment per transition with witness_hash always absent in schema 1. It carries no signature, entropy, clock or node order, so every holder of (B, TA_B) produces identical bytes. It has a strict decoder, and verify re-derives and compares field by field; neither is authority for anything (2c-F R7). Proof material never refuses a receipt. - TAG_DSM_SOFI_RECEIPT_V1 = "DSM/sofi-receipt/v1", registered (count 350). DSM/receipt stays the stitched receipt: its recovery rollup already reaches sealed capsules and signed tombstones. - ccb: class 0x0034 allocated; RouteSet 0x000C and RouteCommitmentBody 0x0017 move from declared_unencoded to burned_class (R1 ratified the shipped X). - Class-1 vectors: the 137-byte receipt of the pinned market bundle, from the pinned identities alone; and RC* -> X from hand-written protobuf bytes, so a protobuf-library refactor that moved X is caught. * feat(2c-F): publish the Def 14.2 receipt as an obligation that never gates the release After the walk certifies a market settlement, complete_settlement projects the SofiReceipt from the certified fold's own acceptance, and freezes the closure {receipt, CCB(B), CCB(TA_B)} for the composed V_n's committed storage set, before the release step. The generic sweep then publishes it. A failure to project or freeze is logged and never holds the fence. Publication may land after the release. Nothing re-fences, re-binds, re-admits or re-certifies (owner ruling on R6). - FoldedParent carries certified_acceptance: the exact TA_B 2c-D §7 accepted, so the receipt is built from what certified. - MarketCompletion carries CCB(B); both the settle route and D-f supply it. - sofi_receipt_publication: closure / freeze / publication. publication() reports BoundToAnotherSet rather than counting another set's quorum as the vault's (I-5; unreachable in beta). - Tests: the published receipt is exactly the projection, frozen for the vault's own set; with receipt PUTs refused the fence still releases, and the sweep alone publishes afterwards with no binding round and no transition; an uncertified settlement has no receipt. - Mutation controls MS1-MS3 executed: each named test red, each source restored and cmp-verified. * formal(2c-F): DSMSofiReceipt — the receipt never gates the release The 19th Lean module restates C2's completion pass with the 2c-F obligation and proves: - the fence follows C2's rule alone, and neither the receipt's state nor its reachability moves it; - a receipt obligation is created only by a certified pass; - the sweep alone finishes a frozen obligation, after the release, and touches nothing else; - a second pass and a second sweep change nothing. The samples show a release with the receipt still owed and the sweep then publishing it. Two mutation controls were executed, each with the kernel proving the named sample false. CI Lean pin 18 -> 19.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For owner ruling — do not merge before the rulings
docs/papers/amendment-2c-f-sofi-receipt-rulings.md: a survey of the four Def 14.2 blockers and Q publication, structured as requested (existing state → conflicts → compatibility → proposed rulings → alternatives → frozen text → implementation work). No code, no registry change, no tag change. The registry entries in §6.5–6.6 are proposals only.The four blockers, and the smallest ruling proposed for each
X = H(DSM/route-set ‖ CCB(Q)), withQcarrying a multi-route choice set. Shipped:X = H(DSM/ext ‖ RouteCommitV1 with signature cleared), one route per signature. It is signed in DlvSettle (fields 10 and 17), carried inb, and committed in0x0021leaves and owner applies.QandRhave never been encodable.b(DlvSettle preimage field 9, inside0x0031), so "Q in the publication set" is met byBitself. Burn0x000Cand0x0017.DSM/receiptcollisionDSM/sofi-receipt/v1for the new class only. No migration.successor_hash_vandwitness_hash_vare defined nowhere, and "the published receipt set" is never enumerated.successor_hash_v = c_{n+1}.witness_hash_vmust be absent in schema 1 (P_v present ⇒ refuse). Publication set is exactly{receipt, B, TA_B}; trader lineage by reference to 2c-D §7.0x0034is free.0x0034 SofiReceiptschema 1, 137 bytes.Also for ruling
Qis the route-commitment body (C2-R1 point 9's sense);qis the quorum (the brief's sense). R5 answers both. Quorum is measured overS_v, which is derivable fromB, using the existing Req 15.8 counting; there is no quorum certificate.(B, TA_B), built only after certification, and independent of fence release. C2's release condition is untouched. The alternative, O1, is in §5.4.All eleven frozen boundaries are checked per ruling (§4). Five incidental findings are recorded but not ruled (§2), among them registry §5.13/§5.14 citing TradeIntent fields that schema 2 no longer has.
PR #857 is independent and decides none of these questions.