diff --git a/.github/instructions/sofispecs.instructions.md b/.github/instructions/sofispecs.instructions.md index 3cdd4034..4c196365 100644 --- a/.github/instructions/sofispecs.instructions.md +++ b/.github/instructions/sofispecs.instructions.md @@ -419,13 +419,14 @@ DSM/fulfillment owner-committed fulfillment mechanism DSM/enc encumbrance set DSM/enc-claim encumbrance claim identifier DSM/intent trade intent -DSM/route-set route-set external commitment +DSM/route-set RETIRED by amendment 2c-F R1 — never reused DSM/allocation canonical same-pair allocation bundle -DSM/ext external commitment +DSM/ext external commitment X = H(DSM/ext ∥ RC*) (amendment 2c-F R1) DSM/digest trade digest DSM/ref-window reference window DSM/ref-rule unilateral reference rule DSM/receipt stitched receipt +DSM/sofi-receipt/v1 Def 14.2 SofiReceipt identity ρ_B (amendment 2c-F R2) DSM/settlement-bundle complete signed settlement bundle DSM/trader-settlement-acceptance/v2 canonical trader post-advance acceptance artifact DSM/binding-tx client-driven opaque quorum transaction identifier @@ -1256,10 +1257,9 @@ i,t + ∑︂ int−feet. i Checked unsigned arithmetic is used throughout. 7.2 External commitments -ExtCommit(X) = H(DSM/ext ∥X). -There is no Canon(X): X is already a 32-byte digest, and a digest is a primitive with no canonical -form of its own. X binds the entire user intent, route set, allocation bundles and every distinct -vault parent identity cn . It does NOT bind a separate encumbrance commitment: the deleted {ECv } +X is itself the external commitment (amendment 2c-F R1): X = H(DSM/ext ∥ RC*), fixed by §9.3. +There is no second ExtCommit(X) digest and no Canon(X). X binds the one signed route, its +allocations, the exact amounts and fee, and every distinct vault parent identity cn . It does NOT bind a separate encumbrance commitment: the deleted {ECv } operand was the only one, and each cn commits its vault's encumbrance set directly. A participating vault must reject a hop not bound by the same X. Requirement 7.2. Multi-vault execution is all-or-none. No Class C verifier may accept a subset @@ -1349,15 +1349,16 @@ independent even when one trade atomically consumes several of them. A route is a sequence of logical legs, each leg being either a one-vault allocation or a same-pair allocation bundle: ri = ⟨Ai,1,Ai,2,...,Ai,h⟩, h≤maxhops. -The route set is -R= {r1,...,rk}, -canonicalized by route CCB ascending. -The route commitment is -X= H(DSM/route-set ∥CCB(Q)), -where Q is the canonical RouteCommitmentBody carrying the trade intent I, the route set R, -and nonceX . X is always a 32-byte digest; -there is no Canon(X), because a digest is already a primitive, and §7.2's external commitment -is ExtCommit(X) = H(DSM/ext ∥X) over that digest. +The route commitment is (amendment 2c-F R1) +X= H(DSM/ext ∥RC*), +where RC is the initiating trader's signed RouteCommitV1 (version 2) and RC* is its commitment +form (registry §2.10): RC with initiator_signature cleared. RC binds exactly one route, so the +committed route set of this profile is the singleton R = {selected_route}; a different route is a +fresh quote under a fresh RC, never a pre-committed alternative. X is always a 32-byte digest and is +itself the external commitment: there is no Canon(X) and no second ExtCommit(X). X is carried in B +as MarketTerms.route_set_commitment, and RC is carried in B as field 9 of the +DlvSettleOperationPreimageV1 in MarketTerms.recovery_material.operation_bytes, so a verifier +recomputes X from B alone. Why {ECv } is DELETED. It was carried because every allocation named pv , and pv committed the PARENT state commitment hn and the reserves digest but not the CURRENT generation's encumbrance set. That justification was conditional on pv . Allocations now name cn , and E is a @@ -1510,17 +1511,20 @@ T and cannot substitute for σ+ T. AB therefore adds no market-specific authorization payload or signing round; it packages the ordinary DSM authenticated successor-state evidence and binds it to the exact (b,X) market execution. -Definition 14.2 (Settlement receipt). A successful SoFi receipt is a compact content- -addressed projection of one realized SettlementBundle: -Receipt= H(DSM/receipt ∥b∥X ∥aB ∥Canon({successor -_ -hashv ,witness_ -hashv }v∈B )). +Definition 14.2 (Settlement receipt; amended by 2c-F). A successful SoFi receipt is the +canonical object SofiReceipt (CCB class 0x0034) projecting one realized Market-shape +SettlementBundle B: +SofiReceipt = (b, X, aB , {(successor_hashv , witness_hashv ) : Tv ∈ B.transitions}) +ρB = H(DSM/sofi-receipt/v1 ∥CCB(SofiReceipt)) +where b = H(DSM/settlement-bundle ∥CCB(B)); X = B.market_terms.route_set_commitment; aB is +Definition 14.1's; successor_hashv = H(DSM/vault-state ∥CCB(Tv .successor)); and witness_hashv is +always absent in schema 1. Proof material in B never makes a receipt unconstructible, and the +receipt adds no witness-validity rule. 31 SoFi: Sovereign Deterministic Finance Revision 15 -The publication set for a successful receipt must include the immutable bytes of B, the immutable -bytes of AB , and the DLV successor/witness objects needed by the verifier. A digest without -retrievable acceptance bytes is insufficient evidence of bilateral completion. +The publication set is exactly P(ρB ) = {CCB(SofiReceipt), CCB(B), CCB(AB )}. RC, the DLV +successors and their proof material are carried inside CCB(B), so no separate object is needed. A +digest without retrievable acceptance bytes is insufficient evidence of bilateral completion. A receipt is evidence and an index object. It does not create DLV binding Finality, trader acceptance, or realization. A verifier that needs the full settlement follows the receipt to b and aB , verifies the bundle, establishes the DLV binding decision, verifies AB against the exact bundled @@ -1550,6 +1554,27 @@ T , and verifying the settlement inclusion proof under that authenticated root, and (d) equality between the trader exchange proved by AB and the DLV reserve deltas committed by B. If any of these facts cannot be established, the verifier must not report a completed trade. +Requirement 14.6 (Quorum publication; 2c-F). ρB is published iff every member of P(ρB ) has +been accepted, at its canonical content address, by at least qv distinct authenticated members of +exactly Sv , for every Tv ∈ B.transitions. Sv and qv are the committed storage set and threshold +of the authenticated consumed parent Vn , established by the DLV state and lineage — never taken +from B's proposed successor and never from local configuration. Counting follows Requirement 15.8. +B's existing pre-bind durability counts when it was achieved over that Sv . No quorum certificate +exists; publication is re-observable, never carried. +Requirement 14.7 (Ordering; 2c-F). SofiReceipt is constructed only after the composition walk +certifies exactly b, and only from that certified fold. It does not gate trader-fence release: it +may be published after the release, and C2's completion and release ordering is unchanged. B's +pre-bind durability before a mutating QuorumBind is a separate obligation and stays pre-bind. +Requirement 14.8 (Determinism and duplicates; 2c-F). SofiReceipt is a pure function of +(CCB(B), CCB(AB )). Any holder may publish it, and re-publication of identical bytes is idempotent. +A receipt whose fields do not re-derive from B and a certifying AB is invalid evidence: it is +refused, and never a safety violation. +Requirement 14.9 (Recovery; 2c-F). Certification creates the publication obligation once, as +frozen bytes; recovery replays exactly those bytes. A publication failure never undoes +realization, re-fences the trader, re-binds, re-admits or re-certifies. +Requirement 14.10 (Non-authority; 2c-F). No composition, admission, realization, fence, +certification or reserve-provenance rule may take a SofiReceipt, its address, its presence or its +publication state as input. 15 Storage Node Specification Storage nodes are non-authoritative byte persistence, byte retrieval, and generic storage-engine state. They do not validate market economics, construct routes, calculate a quorum, or choose a @@ -1768,7 +1793,7 @@ function verifyBindAndMaterialize(route, X, intent): 2. verify ALL history-bound state/proof/anchor bindings 3. verify ALL owner-authority forms and concrete successor signatures 4. verify ALL encumbrance availability, solvency, and exact consumption -5. verify Member(route, R) and ExtCommit(X) +5. verify the signed RC and X = H(DSM/ext ∥ RC*) (amendment 2c-F R1) 6. deterministically re-simulate EVERY allocation and hop 7. verify route-wide conservation 8. enforce total_out >= intent.min_out and total_fee <= intent.max_fee @@ -1791,8 +1816,8 @@ return SUCCESS 15. if ABORTED(B) or CONFLICT_FINAL(other): fold NO DLV successor from B release the trader-parent fence without bilateral advancement -choose the next admissible route already in R -retry from step 1 +return NO_ADMISSIBLE_ROUTE: R is the singleton {selected_route} (amendment 2c-F R1), +and a new route is a fresh quote under a fresh RC 16. if RECOVERING or INDETERMINATE: recover THIS transaction to a terminal outcome keep trader_parent fenced; do NOT permit any different successor from it diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7ccd5a6b..4f6b2335 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -553,7 +553,7 @@ jobs: - name: Kernel-check every module, sorry-free run: | set -euo pipefail - expected=18 + expected=19 found=$(ls lean4/*.lean | wc -l) if [ "$found" -ne "$expected" ]; then echo "::error::lean4/ has $found modules, expected $expected." diff --git a/docs/papers/amendment-2c-a-bundle-and-transition.md b/docs/papers/amendment-2c-a-bundle-and-transition.md index 12767b81..c8a4f892 100644 --- a/docs/papers/amendment-2c-a-bundle-and-transition.md +++ b/docs/papers/amendment-2c-a-bundle-and-transition.md @@ -198,6 +198,12 @@ The boundary is: > **`B` proves exactly which route was executed. The receipt/evidence set proves that route came > from the exact committed choice set and intent.** +> **Amended by [2c-F](amendment-2c-f-sofi-receipt-rulings.md) R1 (2026-09-11).** `Q` is `RC`, the +> signed RouteCommit that `B` already carries, and `0x0017` is burned. The proof that the executed +> route came from the committed choice is `B`-internal: the RC signature and hop (provenance step +> 7), the recomputation of `X`, CORR.2, and Tier-1 SAT over `MarketTerms.intent`, +> `MarketTerms.selected_route` and RC. No separate `Q` object is published. + --- ## Ruling 3 — beta carries exactly one `T_v`, but the field remains a set diff --git a/docs/papers/amendment-2c-d-bundle-acceptance-and-realization.md b/docs/papers/amendment-2c-d-bundle-acceptance-and-realization.md index 88065c07..062eac21 100644 --- a/docs/papers/amendment-2c-d-bundle-acceptance-and-realization.md +++ b/docs/papers/amendment-2c-d-bundle-acceptance-and-realization.md @@ -781,7 +781,9 @@ receipt objects three live consumers, all on the legacy self-verifying check: the walk's 5-c-1 gate, dlv_reconcile (owner apply), unapplied_settlements_for_vault (owner display) - Def 14.2 public receipt binds ta_B; NOT implemented; the Rev 15 text is not in-repo + Def 14.2 public receipt binds ta_B; NOT implemented at C2 (since: amendment 2c-F); + the Rev 15 text IS in-repo, at + .github/instructions/sofispecs.instructions.md (2c-F I-3) CORR.4 frozen as semantics only; the two digests carrying it have no production producer, so CORR.4 is unreachable live Tier-1 intent satisfaction NOT enforced on any live path; the 5-c-1 RouteCommit gate @@ -853,6 +855,10 @@ make V1 live, so C2 closes it. > not claim that publishing V1 satisfies those requirements. > ``` +*Point 9 is discharged by [amendment 2c-F](amendment-2c-f-sofi-receipt-rulings.md): the Def 14.2 +receipt is `0x0034 SofiReceipt`, and "Q" is the signed RouteCommit that `B` already carries. V1 is +unchanged and still is not that receipt.* + **Why publication precedes release (point 4).** A same-step publish-and-release is not atomic across a distributed boundary. If the fence released and the process died before V1 became discoverable, every foreign composer would lose the evidence R1 itself requires. Publishing first is safe because diff --git a/docs/papers/amendment-2c-f-sofi-receipt-rulings.md b/docs/papers/amendment-2c-f-sofi-receipt-rulings.md index ab979bf3..ab89d484 100644 --- a/docs/papers/amendment-2c-f-sofi-receipt-rulings.md +++ b/docs/papers/amendment-2c-f-sofi-receipt-rulings.md @@ -1,12 +1,44 @@ -# Amendment 2c-F — the Def 14.2 settlement receipt: survey and rulings draft +# Amendment 2c-F — the Def 14.2 settlement receipt: survey and rulings -> **STATUS: DRAFT FOR OWNER RULING. Nothing in this document is frozen.** -> It changes no code, no registry row, no domain tag and no formal model. §6 is the text proposed for -> freezing **if** the recommended rulings are taken; §5 holds the real alternatives. The registry -> entries in §6.5–§6.6 are proposals and have **not** been applied. +> **STATUS: FROZEN — owner rulings of 2026-09-11, recorded verbatim below, and IMPLEMENTED by the +> change that carries this text (§7).** §1–§5 are the survey as it was put for ruling. Where they +> differ from the rulings, the rulings govern; the two corrections the rulings forced are applied in +> place and marked *(ruled)*. §6 is the text as frozen; the spec, the registry and 2c-D now carry it. > -> Base: `main` at `e58340cf` (C2, #856). PR #857 (C2 formal alignment) is independent of this -> document: it models V1 completion and composed reserves and decides none of the questions below. +> The draft merged as #858 (`b2271d7a`) as a draft. Merging it was not a ruling; the rulings below are. + +## Owner rulings (2026-09-11) + +Put to the owner as four questions; the answers, verbatim: + +- **R1 — X:** ratify the shipped X. +- **FB-4 — publication timing:** *"Pre-bind B durability stays pre-bind. B, including the embedded + RouteCommit, must already satisfy the existing quorum durability requirement before mutating + QuorumBind. The “after certification” requirement applies to the new Def. 14.2 SofiReceipt, not to + B's pre-bind availability. These are two different publication obligations."* +- **R6 — fence ordering:** *"The Def. 14.2 SofiReceipt does not gate trader-fence release. C2's + existing completion/fence-release ordering remains untouched. Construct the public SofiReceipt + only after full certification; it may be published after the existing C2 fence-release boundary. + Publication failure creates an idempotent recoverable publication obligation, but does not undo + realization, re-fence the trader, re-bind, re-admit, or re-certify."* +- **R3/R5 — TA_B and witness:** *"TA_B must satisfy publication durability over the authenticated + committed vault storage set S_v and threshold q_v established by the DLV state/lineage—not a set + chosen merely because B names it. Existing B durability can count if already sufficient. For + schema 1, witness_hash_v is always absent. Do not reject an otherwise certified settlement merely + because optional proof material exists. The public receipt must not create a new witness-validity + rule."* + +**Two corrections to the draft follow, and are applied below.** +- `S_v` is the authenticated consumed parent's committed set, established by the DLV state and + lineage. It is never the set `B`'s proposed successor names; the draft's "derivable from `B` + alone" is withdrawn. Registry §5.19 already said the proposed successor is never authoritative for + its own quorum. +- Proof material never refuses a receipt. The draft's "`P_v` present makes the receipt + unconstructible" is withdrawn. + +**Not separately put:** R2 (the fresh tag), R4 (class `0x0034`) and R7 (non-authority) had no +competing option in the draft. They are adopted as proposed and remain open to the owner's +objection before this change merges. **Sources.** Revision 15 is quoted from `.github/instructions/sofispecs.instructions.md` as `spec:N` (line numbers). The registry is `docs/papers/ccb-object-registry.md` (`reg §N`). Code is @@ -348,10 +380,9 @@ SAT, §7 or Req 21.16 compute moves (FB-1, 6, 7, 8). No owner action is added (F - `v` ranges over the elements of `B.transitions` (reg §5.19 field 2). Beta: exactly one. - `successor_hash_v := c_{v,n+1} = H(DSM/vault-state ∥ CCB(T_v.successor))`. This is the successor's existing registered identity; no new tag. -- `witness_hash_v` is an optional `digest32` and **must be absent** in schema 1. Receipt-bearing - bundles are Market shape, where `close_authorization` is absent, and beta `P_v` is absent. A `T_v` - carrying `P_v` makes the receipt **unconstructible** (a refusal, never an omission) until an - amendment gives `P_v` an identity under a new schema. +- `witness_hash_v` is an optional `digest32` and is **always absent** in schema 1. *(ruled)* Proof + material in `B` never makes a receipt unconstructible: the receipt does not commit to it and adds + no witness-validity rule. Giving `P_v` a receipt commitment would need a new schema. - Entry encoding is inline (reg §5.2 precedent): `enc(entry) = successor_hash ‖ opt(witness_hash)`. Entries are sorted by `enc(entry)` per §2.4; duplicates are invalid; the count equals `|B.transitions|`. @@ -376,9 +407,11 @@ economic family. **R5 — `Q` and quorum publication.** - *What `Q` means:* the route-commitment body. Under R1 it is RC, carried in `CCB(B)`; there is no separate `Q` object and no separate `Q` publication act. -- *Storage set:* for each `v`, `S_v := V_{n+1}.storage_set` and `q_v := V_{n+1}.quorum` of - `T_v.successor`, which bundle validity makes equal to `V_n`'s. `S_v` is **derivable from `B` - alone**, and resolved through the catalog, never from local fleet configuration. +- *Storage set:* *(ruled)* for each `v`, `S_v` and `q_v` are the committed storage set and + threshold of the **authenticated consumed parent** `V_n`, established by the DLV state and lineage + — the composed `V_n` that `c_n` names. They are never the set `B`'s proposed successor names, and + never local fleet configuration. `B`'s existing pre-bind durability counts when it was achieved over + that same `S_v`. - *Attributable successful publication of `p`:* at least `q_v` distinct authenticated members of exactly `S_v`, each echoing its own member identity, have accepted the exact bytes of `p` at `addr(N_p, p)` (Req 15.8, 15.2). This is the existing `put_immutable_to_all_members` and @@ -398,16 +431,19 @@ economic family. holds for exactly `b`, from that pass's certified fold. It is never constructed otherwise. - **Independent of fence release (O2).** Receipt construction and publication are neither a precondition nor a consequence of fence release. C2's pass is unchanged: certify, V1 at quorum, - release. The receipt step follows it in the same pass and in every D-f resume pass. This restores + release. *(ruled)* The receipt closure is frozen in that same certified pass, before the release + step, so the obligation is durable before anything is released. A failure to project or freeze it + is logged and never holds the fence, and publication may land after the release. This restores Rev 15 §16.2's order for this object (I-4). - **Duplicates.** Identical bytes: `PutImmutable` and freeze are idempotent. Different bytes for the same `b` can differ only in field 3. A different `a_B` that does not certify `b` makes an invalid receipt: it is refused, and is **never** a `SAFETY_VIOLATION` or a quarantine trigger, so forged evidence cannot be used for denial of service. -- **Recovery.** Any partial state (receipt unfrozen, frozen and pending, or `TA_B` pending on `S_v`) - is finished by the D-f pass: re-certify, recompute (identical bytes), freeze (a no-op if already - frozen), sweep. It never re-binds, re-advances or alters `b`. Below quorum, the receipt stays - pending and is retried. The settlement is unaffected throughout. +- **Recovery.** *(ruled)* Certification creates the obligation once, as frozen bytes. Recovery is + the generic sweep replaying exactly those bytes until a quorum of `S_v` holds each. It never + re-certifies, re-binds, re-advances, re-admits, re-fences or alters `b`, and it never undoes + realization. Below quorum, the receipt stays pending and is retried. The settlement is unaffected + throughout. **R7 — non-authority.** No composition, admission, realization, fence, certification or reserve-provenance predicate may take a `0x0034` object, its address, its presence or its @@ -456,9 +492,10 @@ used nowhere else is rejected. ### 5.5 Where `TA_B`'s durability is measured -- **L-1 (recommended):** every member of `P` is at quorum on `S_v`, including `TA_B`. `S_v` is - derivable from `B`, so Req 21.16's third party learns the set from the receipt set itself. Cost: - one extra freeze of `TA_B` for `S_v` when it differs from the network set (I-5). +- **L-1 (recommended, and ruled):** every member of `P` is at quorum on `S_v`, including `TA_B`. + *(ruled)* `S_v` is the authenticated consumed parent's committed set, not one read off `B`. Cost: + `TA_B` needs a row bound to `S_v` when its admission froze it for a different set (I-5). Until + per-set rows exist, that case is reported as not published and never counted. - **L-2:** accept `TA_B`'s admission durability on the network root-register set. This is smaller in code, but the verifier must learn a second set that `B` does not name. - **L-3 (reject):** replicate `Λ` to `S_v`. It is unbounded (the whole trader lineage). @@ -533,9 +570,10 @@ DSM/sofi-receipt/v1 Def 14.2 SofiReceipt identity ρ_B > **Req 14.6 (Quorum publication).** `ρ_B` is *published* iff every member of `P(ρ_B)` has been > accepted, at its canonical content address, by at least `q_v` distinct authenticated members of -> exactly `S_v`, for every `T_v ∈ B.transitions`. Here `S_v` and `q_v` are the successor's -> committed storage set and threshold. Counting follows Req 15.8. No quorum certificate exists; -> publication is re-observable, never carried. +> exactly `S_v`, for every `T_v ∈ B.transitions`. Here `S_v` and `q_v` are the committed storage +> set and threshold of the authenticated consumed parent `V_n`, established by the DLV state and +> lineage. Counting follows Req 15.8. `B`'s pre-bind durability counts when it was achieved over +> that `S_v`. No quorum certificate exists; publication is re-observable, never carried. > > **Req 14.7 (Ordering).** `SofiReceipt` is constructed only after the composition walk certifies > exactly `b`, and only from that certified fold. Its construction and publication are neither a @@ -546,9 +584,9 @@ DSM/sofi-receipt/v1 Def 14.2 SofiReceipt identity ρ_B > receipt whose fields do not re-derive from `B` and a certifying `TA_B` is invalid evidence: it is > refused, and never a safety violation. > -> **Req 14.9 (Recovery).** A partially published receipt is completed by recomputation and -> re-publication of identical bytes. Recovery never re-binds, re-advances or alters `b`, and a -> receipt below quorum leaves the settlement unchanged. +> **Req 14.9 (Recovery).** Certification creates the publication obligation once, as frozen bytes; +> recovery replays exactly those bytes. A publication failure never undoes realization, re-fences the +> trader, re-binds, re-admits or re-certifies. > > **Req 14.10 (Non-authority).** No composition, admission, realization, fence, certification or > reserve-provenance rule may take a `SofiReceipt`, its address, its presence or its publication @@ -604,7 +642,46 @@ DSM/sofi-receipt/v1 Def 14.2 SofiReceipt identity ρ_B --- -## 7. Exact implementation work unlocked by those rulings (NOT started) +## 7. Implementation + +### 7.1 What the adopting change implements + +| Ruling | Where | What | +|---|---|---| +| R2 | `dsm/src/common/domain_tags/dsm/core.rs` | `TAG_DSM_SOFI_RECEIPT_V1 = "DSM/sofi-receipt/v1"`, registered, so the uniqueness and prefix-freedom checks cover it | +| R1, R4 | `dsm/src/ccb/mod.rs` | class `0x0034` allocated; `0x000C` and `0x0017` moved from `declared_unencoded` to `burned_class` | +| R3, R4, R7 | `dsm/src/dlv/sofi_receipt.rs` | `SofiReceipt::project(B, a_B)`, a strict decoder, and `verify`, which re-derives and compares field by field. There is no `P_v` refusal *(ruled)*. Nothing returned can serve as authority | +| R1, R4 | `dsm/tests/settlement_bundle_conformance.rs`, `dsm/tests/route_commitment_x_conformance.rs` | class-1 vectors: the 137-byte receipt of the pinned market bundle, and `RC*` → `X` from hand-written protobuf bytes | +| R6 | `dsm_sdk/src/sdk/vault_state_composition.rs` | a certified market fold carries the exact `TA_B` §7 accepted, so the receipt is built from what certified | +| R5, R6 | `dsm_sdk/src/sdk/sofi_receipt_publication.rs`, `handlers/dlv_routes.rs` | `complete_settlement` projects the closure from the certified fold and freezes it for the composed `V_n`'s set, before the release and never gating it; the generic sweep publishes it. `publication()` reports `BoundToAnotherSet` rather than counting another set's quorum | +| R6 | `lean4/DSMSofiReceipt.lean` (19th module) | the fence follows C2's rule alone; a receipt exists only after certification; the sweep alone finishes it, after the release; idempotence | +| — | spec, registry, 2c-D | §6 applied: Def 14.2, Req 14.6–14.10, §7.2, §9.3, §16.2; registry §2.10 exception 2, §3, §4, §5.12–§5.14, §5.20, §5.42, §6a F3; I-1, I-2 and I-3 corrected | + +**Mutation controls — executed.** Each removes or weakens one property. A **named** test then goes +red by performing the forbidden action. Each source was restored from a byte copy and checked with +`cmp`. + +| # | Mutation | Named test red | +|---|---|---| +| MS1 | the release waits for the receipt closure 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**, and both never-gate theorems fail | +| L2 | Lean: the obligation is created without certification | `an_uncertified_settlement_has_no_receipt` proved **false** | + +That the receipt is built only from a certified fold is also **structural**. The acceptance it binds +exists only on a certified market fold (`FoldedParent::certified_acceptance`), so there is nothing +to build it from otherwise. `an_uncertified_settlement_cannot_be_resumed_into_a_release` asserts that +no receipt row exists. + +**Settlements completed before this change** carry no receipt. Beta is a clean cut, so nothing is +backfilled. + +**Owed, not done here:** per-set frozen rows (I-5). They matter only when a vault's committed set +differs from the network set `TA_B` was admitted under. That cannot happen in beta, and outside +beta it is reported, never counted. + +### 7.2 The plan as drafted (superseded where §7.1 differs) **Core (`dsm`).** 1. `TAG_DSM_SOFI_RECEIPT_V1 = "DSM/sofi-receipt/v1"`, covered by diff --git a/docs/papers/ccb-object-registry.md b/docs/papers/ccb-object-registry.md index 81619c52..44a6732c 100644 --- a/docs/papers/ccb-object-registry.md +++ b/docs/papers/ccb-object-registry.md @@ -286,10 +286,10 @@ but a serialized protobuf message is never a valid CCB blob and must never be ha as if it were. Protobuf field numbers and CCB field numbers are independent namespaces and need not agree. -#### The one named exception — `BindingRecordWireV1` +#### Named exception 1 — `BindingRecordWireV1` -Amendment 2c-C2 ruling F freezes exactly one structure outside CCB, and names it so that it can -never be cited as a general precedent. +Amendment 2c-C2 ruling F freezes this structure outside CCB, and names it so that it can never be +cited as a general precedent. (Amendment 2c-F R1 names a second, `RC*`, below, on its own ground.) ```text BindingRecordWireV1 is a frozen storage-layer canonical BYTE GRAMMAR. @@ -317,6 +317,27 @@ protobuf library refactor MUST NOT silently change them.** This is a narrowly named storage-substrate exception. **It is not permission for arbitrary protobuf-derived identities**, and no other object may cite it. +#### Named exception 2 — `RC*`, the RouteCommitV1 commitment form (amendment 2c-F R1) + +```text +RC* = the proto3 binary encoding of RouteCommitV1 (proto/dsm_app.proto, version 2) + with initiator_signature empty: fields in ascending field number, + implicit-presence scalars equal to their default omitted, hops in carried + order with each RouteCommitHopV1 encoded likewise, no unknown fields +X = H_dom(DSM/ext, RC*) +``` + +`RC*` is computed over the re-encoding of the decoded message. It is the preimage of `X` and of the +initiator's SPHINCS+ signature, and it is **never** a CCB blob. The signed `RC` rides inside `B` as +field 9 of the `DlvSettleOperationPreimageV1` in `MarketTerms.recovery_material.operation_bytes` +(§5.23), so `X` is recomputable from `B` alone. + +2c-F R1 ratified it rather than cutting it to a CCB `Q` because it shipped: the settler's operation +signature, `b`, the `0x0021` leaves and every owner apply already commit to this `X`. That is its +own ground, not a citation of exception 1. It permits no other protobuf-derived identity. The +grammar is pinned by bytes, not by `prost`, in `dsm/tests/route_commitment_x_conformance.rs`: the +expected bytes there are written by hand, so a protobuf-library refactor that moved them is caught. + ### 2.11 Authenticated retrieval — the retrieval obligation Fetching an addressed object is not the same as obtaining it. The retrieval obligation is stated at @@ -388,8 +409,8 @@ storage address, a resource key or an authority check appears here. | `0x0009` | `ReleasePolicy` (`P_R`) | 1 | nested in `0x0001` | §5.4 defined | | `0x000A` | `FeePolicy` (`Φ`) | 1 | nested in `0x0001` | §5.9 defined | | `0x000B` | `TradeIntent` | **2** | `I = H(DSM/intent ‖ CCB)` | §5.5 defined; schema 1 burned by 2c-E | -| `0x000C` | `RouteSet` (`R`) | **2** | nested in `0x0017` | §5.14 defined; schema 1 **burned** | -| `0x000D` | `Route` (`r_i`) | **2** | set element of `0x000C` | §5.13 defined; schema 1 **burned** | +| `0x000C` | ~~`RouteSet`~~ | — | — | **BURNED by 2c-F R1** — schema 1 burned by the route cut; schema 2 never encoded | +| `0x000D` | `Route` (`r_i`) | **2** | nested in `0x0033` field 3 | §5.13 defined; schema 1 **burned** | | `0x000E` | `SettlementBundle` (`B`) | **2** | `b = H(DSM/settlement-bundle ‖ CCB)` | §5.19 defined; schema 1 burned by 2c-E's transitive bump | | `0x000F` | `ConsumedDlvTransition` (`T_v`) | 1 | nested in `0x000E` | §5.21 defined | | `0x0010` | `DlvProofMaterial` (`P_v`) | 1 | nested in `0x000F` | §5.22 defined; zero fields in schema 1 | @@ -397,7 +418,7 @@ storage address, a resource key or an authority check appears here. | `0x0012` | `TradeDigest` | 1 | `d = H(DSM/digest ‖ CCB)` | **blocked, see §6** | | `0x0013` | `ReferenceWindow` (`{d_i}`) | 1 | `W = H(DSM/ref-window ‖ pair_id ‖ CCB)` | §5.8 defined | | `0x0014` | ~~`ExternalCommitmentBody`~~ | — | — | **BURNED — §6a finding 3** | -| `0x0017` | `RouteCommitmentBody` (`Q`) | **2** | `X = H(DSM/route-set ‖ CCB(Q))` | §5.12 defined; schema 1 **burned** | +| `0x0017` | ~~`RouteCommitmentBody`~~ | — | — | **BURNED by 2c-F R1** — `X = H_dom(DSM/ext, RC*)` (§2.10); schema 2 never encoded | | `0x0015` | `Allocation` (`a`) | **2** | leg element; nested in `0x000D` | §5.10 defined; schema 1 **burned** | | `0x0016` | `AllocationBundle` (`AB_{A→B}`) | **2** | leg element; nested in `0x000D` | §5.11 defined; schema 1 **burned** | | `0x0018` | **substrate** `GenesisParamsV3` | 1 | `G = H(DSM/genesis/v3 ‖ CCB)` | §5.15 defined | @@ -405,6 +426,7 @@ storage address, a resource key or an authority check appears here. | `0x001A` | **substrate** `DeviceTreeRootTransition` (`T_j`) | 1 | `t_j = H(DSM/devtree-transition ‖ CCB)`, and the delegate-signed bytes | §5.17 defined | | `0x0031` | **substrate** `DsmSuccessorEvidence` | 1 | `evidence_addr = H(DSM/economic-dsm-successor-evidence/v1 ‖ CCB)`; nested in `0x0033` | §5.23 defined | | `0x0033` | `MarketTerms` | **2** | nested in `0x000E` | §5.20 defined; schema 1 burned by 2c-E's transitive bump | +| `0x0034` | `SofiReceipt` (Def 14.2 Receipt) | 1 | `ρ_B = H_dom(DSM/sofi-receipt/v1, CCB)` | §5.42 defined by 2c-F | | `0x001B` | **substrate** `EconomicRootClaimBody` | 1 | signed over `H_dom(DSM/economic-root-claim-sign/v1, CCB)` | §5.24 defined | | `0x001C` | **substrate** `EconomicAdmissionManifest` | 1 | inner `H_dom(N, P)`; named by `0x001B` field 5 | §5.25 defined | | `0x001D` | **substrate** `EconomicTransitionWitness` | 1 | inner identity; named by `0x001C` field 2 | §5.26 defined | @@ -441,7 +463,8 @@ tuple's `enc(entry)` inline, so it still needs no class of its own. Per §2.8 a is never re-assigned. `0xFF00`–`0xFFFF` reserved for test classes. **Burned schema versions.** `0x0004`, `0x0005`, `0x000C`, `0x000D`, `0x0015`, `0x0016` and -`0x0017` have schema 1 burned by the state/route identity cut. `0x000B`, `0x0033` and `0x000E` have +`0x0017` have schema 1 burned by the state/route identity cut; amendment 2c-F R1 has since burned +`0x000C` and `0x0017` outright. `0x000B`, `0x0033` and `0x000E` have **schema 1 burned by amendment 2c-E** — `0x000B` because the exact-output cut changed its members, and the other two transitively, because §2.7 nests by complete CCB. No production path decodes, accepts, emits or falls back to any of the three, and schema-1 bytes must be refused as **burned** @@ -604,12 +627,13 @@ normative network parameters (§3.2) and the one named non-CCB grammar (§2.10), `signature_alg` member — framework and namespace content, not object classes. No field table was added, changed or burned. -Of the **twenty-two live** object classes above — `0x0014` is burned and not counted, and -`0x0033` `MarketTerms` was added by amendment 2c-A: +Of the **twenty-one live** object classes above — `0x0014`, `0x000C` and `0x0017` are burned and +not counted; `0x0033` `MarketTerms` was added by amendment 2c-A and `0x0034` `SofiReceipt` by +amendment 2c-F: -- **19 are fully specified** in §5 — `0x0001`, `0x0002`, `0x0004`, `0x0005`, `0x0007`, - `0x0008`, `0x0009`, `0x000A`, `0x000B`, `0x000C`, `0x000D`, `0x000E`, `0x000F`, `0x0010`, - `0x0013`, `0x0015`, `0x0016`, `0x0017`, `0x0033`. (Substrate `0x0031` is defined at §5.23 and, +- **18 are fully specified** in §5 — `0x0001`, `0x0002`, `0x0004`, `0x0005`, `0x0007`, + `0x0008`, `0x0009`, `0x000A`, `0x000B`, `0x000D`, `0x000E`, `0x000F`, `0x0010`, + `0x0013`, `0x0015`, `0x0016`, `0x0033`, `0x0034`. (Substrate `0x0031` is defined at §5.23 and, like `0x0018`–`0x001A`, is **outside** this count.) - **Encoding closure for the settlement bundle is ACHIEVED.** 2c-B closed `MarketTerms` field 6, so a conformant market `b` is constructible; the owner-close shape is encodable once the exact @@ -954,7 +978,11 @@ are distinct DLVs when the `vault_id` values recovered from their bound `V_n` di duplicate identifier inside the allocation purely to preserve a sorting explanation would be the alias this cut removes. -### 5.12 `RouteCommitmentBody` — class `0x0017`, schema 2 +### 5.12 `RouteCommitmentBody` — class `0x0017` — **BURNED by 2c-F R1** + +> **Burned 2026-09-11.** The shipped `X` is `H_dom(DSM/ext, RC*)` over the signed RouteCommit that +> `B` carries (§2.10), so no `Q` object exists and nothing encodes this class at any schema. What +> follows is the record of what was defined, not a live layout. `X = H(DSM/route-set ‖ CCB(Q))`. Replaces the four-operand concatenation of §9.3. @@ -993,8 +1021,10 @@ a same-pair allocation bundle", `r_i = ⟨A_{i,1},…,A_{i,h}⟩`, `h ≤ max_ho **Schema 2, schema 1 burned.** Both leg classes moved to schema 2 and legs nest by complete CCB, so this object's bytes changed even though its single field did not. -One field, deliberately. `max_hops` is not carried: it is authoritative in `TradeIntent` -field 6, and route validity checks `len(legs) ≤ max_hops` against the intent the route serves. +One field, deliberately. `max_hops` is not carried — and since 2c-E it is not a `TradeIntent` +member either: schema 1, which carried it, is burned. The beta route is exactly one leg (2c-A ruling +3), and what now protects each dropped bound is 2c-E §5's. *(Corrected by 2c-F finding I-1: this +sentence cited `TradeIntent` field 6, which is `nonce` in schema 2.)* **Sequence, not set** — this is the distinction §2.5 exists for. A route's hops are ordered by execution; reordering them is a *different route*, not the same one written differently. @@ -1009,7 +1039,12 @@ disagree. A leg count of zero is invalid: a route with no legs executes nothing and would give the empty sequence a meaning the specification does not define. -### 5.14 `RouteSet` — class `0x000C`, schema 2 +### 5.14 `RouteSet` — class `0x000C` — **BURNED by 2c-F R1** + +> **Burned 2026-09-11.** One signature binds one route, so the committed route set is the singleton +> selected route and no `R` object exists. What follows is the record of what was defined, not a +> live layout. Its reference to `TradeIntent` field 8 was stale even before the burn: schema 2 has +> no field 8 (2c-F finding I-1). §9.3: `R = {r_1,…,r_k}`, "canonicalized by route CCB ascending", with `k` bounded by `TradeIntent.k`. @@ -1168,7 +1203,7 @@ differ per vault and `V_n` has no other field forcing it to. [amendment 2c-A](amendment-2c-a-bundle-and-transition.md), which carries the reasoning, the seven owner rulings and the full verification obligations. This registry supplies their bytes.* -### 5.19 `SettlementBundle` — class `0x000E`, schema 1 +### 5.19 `SettlementBundle` — class `0x000E`, schema 2 `b = H_dom(DSM/settlement-bundle, CCB(SettlementBundle))`, and `tx_id = value_digest = b`. @@ -1215,7 +1250,7 @@ hashes protobuf bytes, which §2.10 says is never a CCB blob. No current identif > `H_dom(DSM/settlement-bundle, CCB(B))` over canonical bytes. No prost-era identifier is > grandfathered — the cut is a reprovision (2c-A.1 ruling 4), owed at deployment. -### 5.20 `MarketTerms` — class `0x0033`, schema 1 +### 5.20 `MarketTerms` — class `0x0033`, schema 2 Everything a market settlement has and an owner close does not. Nested by value in `0x000E` field 1 and never separately content-addressed, so it adds **no entry to §15.8's canonical immutable-object @@ -1231,7 +1266,7 @@ inventory** — the same footing as `MarketPolicy`, `FeePolicy`, `Route` and `Tr | # | Field | Type | Notes | |---|---|---|---| | 1 | `intent` | nested `0x000B` schema 2 | the complete `TradeIntent`; `I = H_dom(DSM/intent, CCB(field 1))` is **derived, never carried** | -| 2 | `route_set_commitment` (`X`) | `digest32` | `H_dom(DSM/route-set, CCB(Q))` | +| 2 | `route_set_commitment` (`X`) | `digest32` | `H_dom(DSM/ext, RC*)` (2c-F R1, §2.10); `RC` itself rides in field 6's `operation_bytes` (`DlvSettleOperationPreimageV1` field 9) | | 3 | `selected_route` (`r`) | nested `0x000D` schema 2 | the complete executed route, inline by value | | 4 | `trader_parent` | `digest32` | exact ordinary-DSM bilateral parent-state commitment | | 5 | `trader_successor` | `digest32` | exact prepared `C_dsm+` | @@ -1697,6 +1732,41 @@ post-state fact not derivable from `Operation::DlvSettle`, so the content-to-ope other leaf enjoys structurally cannot apply, and an arm that appears to check it is worse than one that visibly declines to. Amendment 2c §9.1's two-conjunct rule is what replaces it. +### 5.42 `SofiReceipt` — class `0x0034`, schema 1 + +The Def 14.2 settlement receipt, frozen by +[amendment 2c-F](amendment-2c-f-sofi-receipt-rulings.md). `ρ_B = H_dom(DSM/sofi-receipt/v1, +CCB(SofiReceipt))`; stored under `immutable_addr(DSM/sofi-receipt/v1, CCB)` per §2.11. **137 bytes** +at beta cardinality: 4 envelope + 3×32 + 4 count + one 33-byte entry. Its encoder lives in +`dsm::dlv::sofi_receipt`: it is a projection of `(B, TA_B)`, not reachable from a `VaultStateV2`. + +| # | Field | Type | Notes | +|---|---|---|---| +| 1 | `bundle` (`b`) | `digest32` | `H_dom(DSM/settlement-bundle, CCB(B))`; `B` must be Market shape | +| 2 | `route_commitment` (`X`) | `digest32` | must equal `B.market_terms.route_set_commitment` | +| 3 | `trader_acceptance` (`a_B`) | `digest32` | `H_dom(DSM/trader-settlement-acceptance/v2, CCB(TA_B))`: the **inner identity**, never the storage address | +| 4 | `transitions` | set of inline `enc(entry)` | `enc(entry) = successor_hash: digest32 ‖ witness_hash: optional digest32` (§2.3), declared inline as §5.2 declares its tuple; one entry per `T_v`; §2.4 order; count `== |B.transitions|` | + +`successor_hash = H_dom(DSM/vault-state, CCB(T_v.successor))`, the successor's existing identity. +**`witness_hash` is always absent in schema 1.** Proof material in `B` never makes a receipt +unconstructible, and the receipt adds no witness-validity rule (2c-F ruling on R3). + +**Deliberately not fields.** No `vault_id` or parent `c_n`: `V_{n+1}` commits both. No +`economic_operation_id`: it is bound through `a_B` (`TA_B` field 3 → `0x0032` field 2), and 2c-D +D3's three-way equality is the check. No `settlement_receipt_id`: that is the V1 / economic family. +No `storage_set_id` or `q`: those are the authenticated parent's. No signature, so §2.9 applies +vacuously. No timestamp, sequence or node order (Req 14.3). + +**Validity, stated as rejections.** A wrong class or schema; a count of 0, or a count +`≠ |B.transitions|`; a `witness_hash` marker `0x01`, or any marker but `0x00`/`0x01`; misordered or +duplicate entries; trailing bytes; any field `≠` its re-derivation from `(B, TA_B)`; `B` not Market +shape. The strict decoder refuses the layout failures, and an exact-length parse of this layout is +the canonical encoding. §2.11 re-hash comes **before** any field is read. + +**Not authority.** No composition, admission, realization, fence, certification or +reserve-provenance rule may take a `SofiReceipt`, its address, its presence or its publication +state as input (2c-F R7). + ## 6. Blocked objects — what each one needs These object classes are assigned but cannot be given field tables from Revision 15 as @@ -1811,6 +1881,13 @@ and §2.8 forbids reassigning a shipped identity to different semantics. An assi not become vacant because it never received a field table. `RouteCommitmentBody` takes a fresh `0x0017`. +> **Superseded in part by amendment 2c-F R1 (2026-09-11).** `X` stays one 32-byte digest and +> `Canon(X)` stays gone. But the body is `RC*`, the signed RouteCommit's commitment form (§2.10), +> not a CCB `Q`, and `ExtCommit(X)` folds into `X` itself. `0x0017` and `0x000C` are burned. This +> finding's objection to preserving a preimage concerned the four-operand concatenation; R1 does not +> revive it. It ratifies a single-body preimage that shipped, that two parties sign, and that `b` +> carries. + ### Finding 4 — `A_B` denoted two objects; both renamed (settled) Def 6.26's trader-acceptance artifact and Def 9.2's allocation bundle shared one symbol with @@ -1922,8 +1999,9 @@ In order, and not combined: **2b. Routing and commitment profile — COMPLETE.** `Route` `0x000D`, `RouteSet` `0x000C`, `Allocation` `0x0015`, `AllocationBundle` `0x0016` and `RouteCommitmentBody` `0x0017` are - specified; `ExternalCommitmentBody` `0x0014` is burned. The original framing follows, kept - for the record: + specified; `ExternalCommitmentBody` `0x0014` is burned. (Amendment 2c-F R1 later burned + `0x000C` and `0x0017`: the shipped `X` commits the signed RouteCommit, §2.10.) The original + framing follows, kept for the record: **2b (as originally scoped).** `Route` `0x000D`, `RouteSet` `0x000C`, `ExternalCommitmentBody` `0x0014`, `TradeDigest` `0x0012`. One dependency cluster: @@ -2166,5 +2244,5 @@ be *implemented* is step 3 of this list, not another normative amendment: an enc `CCB(VaultStateV2)` and is checked against an independent one. The one still-blocked class — `0x0012` — belongs to the remaining settlement sub-amendments and -does not gate Anchor V2. (`0x0011` was the second until 2c-D defined it at §5.40; `0x000C`, -`0x000D` and `0x0010` are now defined, and `0x0014` is burned.) +does not gate Anchor V2. (`0x0011` was the second until 2c-D defined it at §5.40; `0x000D` and +`0x0010` are now defined; `0x0014` is burned, and 2c-F burned `0x000C` and `0x0017`.) diff --git a/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs index 0f881e6e..b477701c 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs @@ -145,6 +145,11 @@ pub mod class { /// is a single namespace. pub const TRADER_ACCEPTANCE: u16 = 0x0011; + /// `SofiReceipt`, the Def 14.2 settlement receipt — amendment 2c-F, + /// registry §5.42. Its encoder lives in `crate::dlv::sofi_receipt`: it is + /// a projection of `(B, TA_B)` and is not reachable from a `VaultStateV2`. + pub const SOFI_RECEIPT: u16 = 0x0034; + /// A complete pre-root → post-root economic transition, carrying its /// mutations and its inline credit sources. pub const ECONOMIC_TRANSITION_WITNESS: u16 = 0x001D; @@ -240,23 +245,15 @@ pub mod declared_unencoded { pub const FULFILLMENT_MECHANISM: u16 = 0x0006; /// §5.6. pub const MARKET_BOUNDS: u16 = 0x0008; - /// §5.14 `RouteSet` `R`, schema 2; schema 1 burned. - pub const ROUTE_SET: u16 = 0x000C; /// Blocked — §6. pub const TRADE_DIGEST: u16 = 0x0012; /// §5.8. pub const REFERENCE_WINDOW: u16 = 0x0013; - /// §5.12 `RouteCommitmentBody` `Q`, schema 2; schema 1 burned. `X` is - /// carried as a digest in `MarketTerms`; `Q` lives in the receipt - /// publication set (2c-A ruling 2). - pub const ROUTE_COMMITMENT_BODY: u16 = 0x0017; pub const ALL: &[u16] = &[ FULFILLMENT_MECHANISM, MARKET_BOUNDS, - ROUTE_SET, TRADE_DIGEST, REFERENCE_WINDOW, - ROUTE_COMMITMENT_BODY, ]; pub fn is_declared_unencoded(object_class: u16) -> bool { @@ -272,8 +269,22 @@ pub mod burned_class { pub const STORAGE_MEMBER_ID: u16 = 0x0003; /// `ExternalCommitmentBody` — §6a finding 3. pub const EXTERNAL_COMMITMENT_BODY: u16 = 0x0014; + /// `RouteSet` `R` — burned by amendment 2c-F R1. The shipped `X` commits + /// one signed route, never a set of alternatives, so nothing encodes `R` + /// at any schema; schema 2 never shipped an encoder. + pub const ROUTE_SET: u16 = 0x000C; + /// `RouteCommitmentBody` `Q` — burned by amendment 2c-F R1. `X` is + /// `H_dom(DSM/ext, RC*)` over the signed RouteCommit carried inside `B` + /// (registry §2.10), so no separate `Q` object exists; schema 2 never + /// shipped an encoder. + pub const ROUTE_COMMITMENT_BODY: u16 = 0x0017; - pub const ALL: &[u16] = &[STORAGE_MEMBER_ID, EXTERNAL_COMMITMENT_BODY]; + pub const ALL: &[u16] = &[ + STORAGE_MEMBER_ID, + EXTERNAL_COMMITMENT_BODY, + ROUTE_SET, + ROUTE_COMMITMENT_BODY, + ]; pub fn is_burned_class(object_class: u16) -> bool { ALL.contains(&object_class) @@ -312,14 +323,14 @@ pub mod schema { (super::class::ENCUMBRANCE_CLAIM, 1), (super::class::ENCUMBRANCE_SET, 1), // The route family moved to schema 2 when `p_v` became `c_n` and legs - // began nesting by complete CCB (registry §5.10–§5.14). Recorded for - // the two classes this crate does not encode as well, so a schema-1 - // envelope classifies as burned rather than unknown (2c-A.1 ruling 10). - (super::declared_unencoded::ROUTE_SET, 1), + // began nesting by complete CCB (registry §5.10–§5.14). Schema 1 of + // `R` and `Q` stays recorded (2c-A.1 ruling 10) now that 2c-F R1 has + // burned both classes outright. + (super::burned_class::ROUTE_SET, 1), (super::class::ROUTE, 1), (super::class::ALLOCATION, 1), (super::class::ALLOCATION_BUNDLE, 1), - (super::declared_unencoded::ROUTE_COMMITMENT_BODY, 1), + (super::burned_class::ROUTE_COMMITMENT_BODY, 1), // Amendment 2c-E cut `TradeIntent` to the exact-output model, and the // bump propagates by §2.7 nesting: `0x0033` carries the intent and // `0x000E` carries the terms. Recorded so a schema-1 envelope for any diff --git a/dsm_client/deterministic_state_machine/dsm/src/ccb/settlement.rs b/dsm_client/deterministic_state_machine/dsm/src/ccb/settlement.rs index 44b75e07..a3f464e2 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/ccb/settlement.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/ccb/settlement.rs @@ -340,8 +340,9 @@ impl DsmSuccessorEvidence { #[derive(Debug, Clone, PartialEq, Eq)] pub struct MarketTerms { pub intent: TradeIntent, - /// `X = H_dom(DSM/route-set, CCB(Q))`; `Q` itself lives in the receipt - /// publication set (2c-A ruling 2). + /// `X = H_dom(DSM/ext, RC*)` (amendment 2c-F R1, registry §2.10): the + /// signed RouteCommit's commitment form. `RC` itself rides in + /// `recovery_material.operation_bytes`, so `X` is recomputable from `B`. pub route_set_commitment: [u8; 32], pub selected_route: Route, /// The exact ordinary-DSM bilateral parent-state commitment of the TRADER diff --git a/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/dsm/core.rs b/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/dsm/core.rs index 7347aacd..e6fe94d7 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/dsm/core.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/dsm/core.rs @@ -97,6 +97,15 @@ pub const TAG_SETTLEMENT_RECEIPT_COMMIT: TaggedHashDomain<'static> = /// in for an acceptance's. pub const TAG_DSM_TRADER_SETTLEMENT_ACCEPTANCE: TaggedHashDomain<'static> = crate::tagged_domain!(b"DSM/trader-settlement-acceptance/v2"); +/// `ρ_B = H(tag ‖ 0x00 ‖ CCB(SofiReceipt))` — the identity of the Def 14.2 +/// settlement receipt (class `0x0034`, amendment 2c-F R2, registry §5.42). +/// +/// Fresh on purpose. `DSM/receipt` is the stitched receipt, and its recovery +/// rollup already reaches sealed capsules and signed tombstones; the +/// `settlement-receipt` family above names the V1 / economic receipt. A +/// Def 14.2 receipt is neither, and must not share a domain with either. +pub const TAG_DSM_SOFI_RECEIPT_V1: TaggedHashDomain<'static> = + crate::tagged_domain!(b"DSM/sofi-receipt/v1"); /// Deterministic receipt id: `H(tag ‖ vault_id ‖ x)`. Derived, not chosen, so the pointer /// publisher and the settling advance agree on it without coordinating. pub const TAG_SETTLEMENT_RECEIPT_ID: TaggedHashDomain<'static> = @@ -146,6 +155,7 @@ pub(super) const TAGS: &[TaggedHashDomain<'static>] = &[ TAG_SETTLEMENT_RECEIPT_LEAF, TAG_SETTLEMENT_RECEIPT_STATE, TAG_DSM_TRADER_SETTLEMENT_ACCEPTANCE, + TAG_DSM_SOFI_RECEIPT_V1, TAG_SETTLEMENT_RECEIPT_SIGN, TAG_SETTLEMENT_RECEIPT_COMMIT, TAG_SETTLEMENT_RECEIPT_ID, diff --git a/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/mod.rs index c1b82dcd..5298f43c 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/common/domain_tags/mod.rs @@ -143,7 +143,7 @@ mod tests { /// deliberately when adding a tag — the same idiom as the CI Lean gate's /// hardcoded module count. It is the weakest of the three checks and is /// here only to make an accidental edit to the registry loud. - const EXPECTED_TAG_COUNT: usize = 349; + const EXPECTED_TAG_COUNT: usize = 350; /// Scan the crate source for every declared domain-tag constant. /// diff --git a/dsm_client/deterministic_state_machine/dsm/src/dlv/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/dlv/mod.rs index bba8fa3e..0594dcdb 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/dlv/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/dlv/mod.rs @@ -19,6 +19,7 @@ pub mod route_commit; pub mod settlement_bundle; // Def 6.14 — the canonical immutable SettlementBundle + K(B) pub mod settlement_receipt_leaf; pub mod settlement_slot_claim; // write-once claim envelope for the settlement-slot quorum register +pub mod sofi_receipt; // 2c-F — the Def 14.2 settlement receipt: a projection, never authority pub mod successor_validity; // 2c-C3 — ValidDlvSuccessorCore: what makes a DLV continuation valid pub mod trader_fence; // Req 6.23 — the initiating-trader parent fence (pure state machine) pub mod vault_pending_pointer; diff --git a/dsm_client/deterministic_state_machine/dsm/src/dlv/sofi_receipt.rs b/dsm_client/deterministic_state_machine/dsm/src/dlv/sofi_receipt.rs new file mode 100644 index 00000000..d92ef7f6 --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm/src/dlv/sofi_receipt.rs @@ -0,0 +1,534 @@ +// SPDX-License-Identifier: Apache-2.0 + +//! `SofiReceipt` — class `0x0034` schema 1, the Def 14.2 settlement receipt +//! (amendment 2c-F). +//! +//! A PROJECTION, NEVER A SOURCE. Every field re-derives from the canonical +//! market bundle `B` and the trader acceptance `TA_B` the walk certified: +//! +//! ```text +//! 1 bundle b = H_dom(DSM/settlement-bundle, CCB(B)) +//! 2 route_commitment X = B.market_terms.route_set_commitment +//! 3 trader_acceptance a_B = H_dom(DSM/trader-settlement-acceptance/v2, CCB(TA_B)) +//! 4 transitions one entry c_{n+1} ‖ absent per T_v, strictly ascending +//! ``` +//! +//! It carries no signature, no entropy, no clock and no node order, so every +//! party holding `(B, TA_B)` produces identical bytes. That determinism is what +//! makes publication idempotent and recovery a replay of the same bytes. +//! +//! WHAT IT IS NOT (2c-F R7). A receipt is evidence and an index object. It is +//! not certification, realization, binding finality or trader acceptance, and +//! no composition, admission, realization, fence, certification or +//! reserve-provenance rule may take one — its bytes, its address, its presence +//! or its publication state — as input. [`verify`] establishes only that bytes +//! are the projection of a given `(B, a_B)`. Whether that `B` was realized is +//! the composition walk's question, never this module's. +//! +//! `witness_hash` IS ALWAYS ABSENT in schema 1 (2c-F, the ruling on R3). It is +//! emitted as the §2.3 absent marker so Def 14.2's pair shape survives, and a +//! present marker is refused. Proof material in `B` never makes a receipt +//! unconstructible: the receipt does not commit to it and adds no +//! witness-validity rule of its own. +//! +//! The digest `ρ_B` is NOT `settlement_receipt_id`. That value is +//! `derive_receipt_id(vault_id, X)` and names the V1 / economic receipt family. + +use crate::ccb::decode::{Cursor, DecodeError}; +use crate::ccb::{ + class, push_absent, push_digest32, push_envelope, push_u32, vault_state_commitment, CcbError, + CcbObject, SettlementBundle, +}; +use crate::common::domain_tags::TAG_DSM_SOFI_RECEIPT_V1; +use crate::storage_object::{immutable_addr, immutable_inner}; + +/// One field-4 entry: the successor commitment and the absent witness marker. +const ENTRY_LEN: usize = 32 + 1; + +/// The canonical length at beta cardinality (one `T_v`): 4 envelope, three +/// `digest32`, a 4-byte count and one entry. +pub const SOFI_RECEIPT_BETA_LEN: usize = 4 + 3 * 32 + 4 + ENTRY_LEN; + +/// `0x0034` schema 1 (registry §5.42). +/// +/// Private fields and one constructor, [`SofiReceipt::project`], so a value +/// of this type is always the projection of some market bundle. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SofiReceipt { + bundle: [u8; 32], + route_commitment: [u8; 32], + trader_acceptance: [u8; 32], + /// `c_{n+1}` of each transition, strictly ascending. Every entry's + /// `enc` is `c_{n+1} ‖ 0x00`, so byte order over the successors IS the + /// §2.4 order over the entries. + successors: Vec<[u8; 32]>, +} + +impl CcbObject for SofiReceipt { + const CLASS: u16 = class::SOFI_RECEIPT; + const SCHEMA: u16 = 1; +} + +/// Why a bundle has no receipt. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ProjectionRefusal { + /// An owner close carries no trader acceptance, so Def 14.2 does not + /// apply to it. + NotMarket, + /// The bundle or one of its successors could not be encoded. + Encode(CcbError), + /// Two transitions name the same successor. Unreachable under beta's + /// cardinality; kept because the set rule forbids duplicates. + DuplicateSuccessor, +} + +impl core::fmt::Display for ProjectionRefusal { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + match self { + Self::NotMarket => write!( + f, + "an owner close has no trader acceptance to bind, so it has no Def 14.2 receipt" + ), + Self::Encode(e) => write!(f, "the bundle does not encode: {e}"), + Self::DuplicateSuccessor => write!( + f, + "two transitions name one successor, and a receipt's transitions are a set" + ), + } + } +} + +impl SofiReceipt { + /// The receipt of market bundle `bundle`, binding the trader acceptance + /// whose identity is `trader_acceptance`. + /// + /// `trader_acceptance` is `a_B` — the INNER identity `ta_B`, never the + /// acceptance's storage address. + pub fn project( + bundle: &SettlementBundle, + trader_acceptance: [u8; 32], + ) -> Result { + let terms = bundle.market_terms().ok_or(ProjectionRefusal::NotMarket)?; + let canon = bundle.encode().map_err(ProjectionRefusal::Encode)?; + let mut successors = bundle + .transitions() + .iter() + .map(|t| vault_state_commitment(&t.successor)) + .collect::, _>>() + .map_err(ProjectionRefusal::Encode)?; + successors.sort_unstable(); + if successors.windows(2).any(|w| w[0] == w[1]) { + return Err(ProjectionRefusal::DuplicateSuccessor); + } + Ok(Self { + bundle: crate::dlv::settlement_bundle::bundle_digest(&canon), + route_commitment: terms.route_set_commitment, + trader_acceptance, + successors, + }) + } + + /// Field 1, `b`. + pub const fn bundle(&self) -> [u8; 32] { + self.bundle + } + + /// Field 2, `X`. + pub const fn route_commitment(&self) -> [u8; 32] { + self.route_commitment + } + + /// Field 3, `a_B`. + pub const fn trader_acceptance(&self) -> [u8; 32] { + self.trader_acceptance + } + + /// Field 4's successor commitments, in canonical order. + pub fn successors(&self) -> &[[u8; 32]] { + &self.successors + } + + /// Canonical CCB bytes, registry §5.42. + pub fn encode(&self) -> Vec { + let mut out = Vec::with_capacity(4 + 3 * 32 + 4 + ENTRY_LEN * self.successors.len()); + push_envelope::(&mut out); + push_digest32(&mut out, &self.bundle); // 1 + push_digest32(&mut out, &self.route_commitment); // 2 + push_digest32(&mut out, &self.trader_acceptance); // 3 + push_u32(&mut out, self.successors.len() as u32); // 4 — a §2.4 set + for successor in &self.successors { + push_digest32(&mut out, successor); + push_absent(&mut out); // witness_hash: absent in schema 1 + } + out + } + + /// `ρ_B = H_dom(DSM/sofi-receipt/v1, CCB(SofiReceipt))`. + pub fn digest(&self) -> [u8; 32] { + immutable_inner(TAG_DSM_SOFI_RECEIPT_V1, &self.encode()) + } + + /// The content address the receipt is stored and retrieved under. + pub fn address(&self) -> [u8; 32] { + immutable_addr(TAG_DSM_SOFI_RECEIPT_V1, &self.encode()) + } +} + +/// Why bytes are not a canonical `SofiReceipt` (registry §5.42). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SofiReceiptDecodeError { + /// Wrong envelope, truncated, or trailing input. + Layout(DecodeError), + /// Field 4 carries no entry: a receipt projects at least one transition. + NoTransitions, + /// An entry carries a witness: schema 1 carries none. + WitnessPresent, + /// An entry's marker is neither the absent nor the present byte. + BadMarker(u8), + /// Field 4 is not strictly ascending: misordered, or a duplicate. + NotStrictlyAscending, +} + +impl core::fmt::Display for SofiReceiptDecodeError { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + match self { + Self::Layout(e) => write!(f, "not a SofiReceipt layout: {e}"), + Self::NoTransitions => write!(f, "a receipt that projects no transition projects nothing"), + Self::WitnessPresent => write!( + f, + "schema 1 carries no witness hash; a present marker names a rule that does not exist" + ), + Self::BadMarker(m) => write!(f, "optional marker {m:#04x} is neither absent nor present"), + Self::NotStrictlyAscending => write!( + f, + "field 4 is a set: entries must be strictly ascending, with no duplicate" + ), + } + } +} + +/// Decode canonical `SofiReceipt` bytes, strictly. +/// +/// Every field is fixed-width and the order is pinned, so an exact-length +/// parse of this layout IS the canonical encoding; +/// `decoded_bytes_re_encode_to_themselves` pins that claim. **A decoded +/// receipt is still only a claim** about some `(B, a_B)`: [`verify`] checks +/// it against a given pair, and nothing makes it authority. +pub fn decode_sofi_receipt(bytes: &[u8]) -> Result { + let layout = SofiReceiptDecodeError::Layout; + let mut c = Cursor { b: bytes, i: 0 }; + c.envelope(SofiReceipt::CLASS, SofiReceipt::SCHEMA) + .map_err(layout)?; + let bundle = c.digest32().map_err(layout)?; + let route_commitment = c.digest32().map_err(layout)?; + let trader_acceptance = c.digest32().map_err(layout)?; + let count = c.u32().map_err(layout)? as usize; + if count == 0 { + return Err(SofiReceiptDecodeError::NoTransitions); + } + // Bound the allocation by what the remaining bytes can actually hold. + if count > (bytes.len() - c.i) / ENTRY_LEN { + return Err(layout(DecodeError::Truncated)); + } + let mut successors: Vec<[u8; 32]> = Vec::with_capacity(count); + for _ in 0..count { + let successor = c.digest32().map_err(layout)?; + match c.u8().map_err(layout)? { + 0x00 => {} + 0x01 => return Err(SofiReceiptDecodeError::WitnessPresent), + other => return Err(SofiReceiptDecodeError::BadMarker(other)), + } + if successors.last().is_some_and(|prev| *prev >= successor) { + return Err(SofiReceiptDecodeError::NotStrictlyAscending); + } + successors.push(successor); + } + if c.i != bytes.len() { + return Err(layout(DecodeError::TrailingBytes { + extra: bytes.len() - c.i, + })); + } + Ok(SofiReceipt { + bundle, + route_commitment, + trader_acceptance, + successors, + }) +} + +/// A receipt field that does not re-derive from `(B, a_B)`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ReceiptField { + Bundle, + RouteCommitment, + TraderAcceptance, + Transitions, +} + +/// Why receipt bytes are not the receipt of a given `(B, a_B)`. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SofiReceiptVerifyError { + Decode(SofiReceiptDecodeError), + Projection(ProjectionRefusal), + /// The first field, in field order, whose carried value is not the one + /// `(B, a_B)` derives. + Mismatch(ReceiptField), +} + +impl core::fmt::Display for SofiReceiptVerifyError { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + match self { + Self::Decode(e) => write!(f, "{e}"), + Self::Projection(e) => write!(f, "{e}"), + Self::Mismatch(field) => write!( + f, + "the receipt's {field:?} is not the one the bundle and acceptance derive — a \ + receipt is a projection, so a field it carries is never believed over its source" + ), + } + } +} + +/// Check that `receipt_bytes` are exactly the receipt of `bundle` binding +/// `trader_acceptance`: decode strictly, re-derive, compare field by field. +/// +/// Establishes a PROJECTION fact only. It says nothing about whether `bundle` +/// was binding-final, accepted or realized, and its result must not be read as +/// if it did (2c-F R7). +pub fn verify( + receipt_bytes: &[u8], + bundle: &SettlementBundle, + trader_acceptance: [u8; 32], +) -> Result { + let carried = decode_sofi_receipt(receipt_bytes).map_err(SofiReceiptVerifyError::Decode)?; + let derived = SofiReceipt::project(bundle, trader_acceptance) + .map_err(SofiReceiptVerifyError::Projection)?; + let checks = [ + (ReceiptField::Bundle, carried.bundle == derived.bundle), + ( + ReceiptField::RouteCommitment, + carried.route_commitment == derived.route_commitment, + ), + ( + ReceiptField::TraderAcceptance, + carried.trader_acceptance == derived.trader_acceptance, + ), + ( + ReceiptField::Transitions, + carried.successors == derived.successors, + ), + ]; + if let Some((field, _)) = checks.iter().find(|(_, holds)| !holds) { + return Err(SofiReceiptVerifyError::Mismatch(*field)); + } + Ok(carried) +} + +#[cfg(test)] +#[allow(clippy::unwrap_used, clippy::expect_used)] +mod tests { + use super::*; + use crate::ccb::settlement::fixtures; + + const PARENT: [u8; 32] = [0xC0; 32]; + const X: [u8; 32] = [0x58; 32]; + const A_B: [u8; 32] = [0xAB; 32]; + + fn market() -> SettlementBundle { + fixtures::market_bundle(PARENT, fixtures::successor(PARENT, 1_010_000, 495_065), X) + } + + fn receipt_bytes() -> Vec { + SofiReceipt::project(&market(), A_B).unwrap().encode() + } + + /// The first entry's witness marker: after the envelope, three digests, + /// the count and the successor. + const MARKER_AT: usize = 4 + 3 * 32 + 4 + 32; + + #[test] + fn a_beta_receipt_encodes_to_the_frozen_length() { + assert_eq!(receipt_bytes().len(), SOFI_RECEIPT_BETA_LEN); + assert_eq!(SOFI_RECEIPT_BETA_LEN, 137, "registry §5.42 pins 137 bytes"); + } + + #[test] + fn every_field_re_derives_from_the_bundle_and_the_acceptance() { + let bundle = market(); + let r = SofiReceipt::project(&bundle, A_B).unwrap(); + let canon = bundle.encode().unwrap(); + assert_eq!( + r.bundle(), + crate::dlv::settlement_bundle::bundle_digest(&canon) + ); + assert_eq!(r.route_commitment(), X); + assert_eq!(r.trader_acceptance(), A_B); + assert_eq!( + r.successors(), + &[vault_state_commitment(&bundle.transitions()[0].successor).unwrap()] + ); + // The same inputs, twice: identical bytes. Nothing else enters. + assert_eq!( + SofiReceipt::project(&market(), A_B).unwrap().encode(), + r.encode() + ); + } + + #[test] + fn the_layout_is_the_registry_table() { + let bytes = receipt_bytes(); + let r = decode_sofi_receipt(&bytes).unwrap(); + assert_eq!(&bytes[..4], &[0x00, 0x34, 0x00, 0x01], "0x0034 schema 1"); + assert_eq!(&bytes[4..36], &r.bundle()); + assert_eq!(&bytes[36..68], &X); + assert_eq!(&bytes[68..100], &A_B); + assert_eq!(&bytes[100..104], &[0, 0, 0, 1], "one transition"); + assert_eq!(&bytes[104..136], &r.successors()[0]); + assert_eq!(bytes[MARKER_AT], 0x00, "witness_hash absent"); + } + + #[test] + fn decoded_bytes_re_encode_to_themselves() { + let bytes = receipt_bytes(); + assert_eq!(decode_sofi_receipt(&bytes).unwrap().encode(), bytes); + } + + #[test] + fn the_digest_and_address_are_the_domain_separated_identities() { + let bytes = receipt_bytes(); + let r = decode_sofi_receipt(&bytes).unwrap(); + // Independent of `immutable_inner`: the frozen `BLAKE3(N ‖ 0x00 ‖ P)`. + let mut h = blake3::Hasher::new(); + h.update(b"DSM/sofi-receipt/v1"); + h.update(&[0u8]); + h.update(&bytes); + assert_eq!(r.digest(), *h.finalize().as_bytes()); + let mut a = blake3::Hasher::new(); + a.update(b"DSM/storage-object"); + a.update(&[0u8]); + a.update(b"DSM/sofi-receipt/v1"); + a.update(&r.digest()); + assert_eq!(r.address(), *a.finalize().as_bytes()); + } + + #[test] + fn an_owner_close_has_no_receipt() { + let close = fixtures::owner_close_bundle(PARENT, fixtures::successor(PARENT, 0, 0)); + assert_eq!( + SofiReceipt::project(&close, A_B), + Err(ProjectionRefusal::NotMarket) + ); + } + + #[test] + fn a_present_witness_is_refused() { + let mut bytes = receipt_bytes(); + bytes[MARKER_AT] = 0x01; + bytes.extend_from_slice(&[0x77; 32]); + assert_eq!( + decode_sofi_receipt(&bytes), + Err(SofiReceiptDecodeError::WitnessPresent) + ); + } + + #[test] + fn a_marker_that_is_neither_absent_nor_present_is_refused() { + let mut bytes = receipt_bytes(); + bytes[MARKER_AT] = 0x02; + assert_eq!( + decode_sofi_receipt(&bytes), + Err(SofiReceiptDecodeError::BadMarker(0x02)) + ); + } + + #[test] + fn an_empty_transition_set_is_refused() { + let mut bytes = receipt_bytes()[..100].to_vec(); + bytes.extend_from_slice(&[0, 0, 0, 0]); + assert_eq!( + decode_sofi_receipt(&bytes), + Err(SofiReceiptDecodeError::NoTransitions) + ); + } + + fn with_entries(entries: &[[u8; 32]]) -> Vec { + let mut bytes = receipt_bytes()[..100].to_vec(); + bytes.extend_from_slice(&(entries.len() as u32).to_be_bytes()); + for e in entries { + bytes.extend_from_slice(e); + bytes.push(0x00); + } + bytes + } + + #[test] + fn misordered_and_duplicated_entries_are_refused() { + assert_eq!( + decode_sofi_receipt(&with_entries(&[[0x02; 32], [0x01; 32]])), + Err(SofiReceiptDecodeError::NotStrictlyAscending) + ); + assert_eq!( + decode_sofi_receipt(&with_entries(&[[0x01; 32], [0x01; 32]])), + Err(SofiReceiptDecodeError::NotStrictlyAscending) + ); + assert!(decode_sofi_receipt(&with_entries(&[[0x01; 32], [0x02; 32]])).is_ok()); + } + + #[test] + fn the_wrong_envelope_truncation_and_trailing_bytes_are_refused() { + let mut wrong = receipt_bytes(); + wrong[1] = 0x33; + assert_eq!( + decode_sofi_receipt(&wrong), + Err(SofiReceiptDecodeError::Layout(DecodeError::WrongClass { + got: 0x0033 + })) + ); + let bytes = receipt_bytes(); + assert_eq!( + decode_sofi_receipt(&bytes[..bytes.len() - 1]), + Err(SofiReceiptDecodeError::Layout(DecodeError::Truncated)) + ); + let mut long = receipt_bytes(); + long.push(0x00); + assert_eq!( + decode_sofi_receipt(&long), + Err(SofiReceiptDecodeError::Layout(DecodeError::TrailingBytes { + extra: 1 + })) + ); + // A count the bytes cannot hold is refused before anything is + // allocated for it. + let mut huge = receipt_bytes()[..100].to_vec(); + huge.extend_from_slice(&u32::MAX.to_be_bytes()); + assert_eq!( + decode_sofi_receipt(&huge), + Err(SofiReceiptDecodeError::Layout(DecodeError::Truncated)) + ); + } + + #[test] + fn verification_names_the_first_field_that_does_not_re_derive() { + let bundle = market(); + let good = receipt_bytes(); + assert!(verify(&good, &bundle, A_B).is_ok()); + + assert_eq!( + verify(&good, &bundle, [0xAC; 32]), + Err(SofiReceiptVerifyError::Mismatch( + ReceiptField::TraderAcceptance + )) + ); + let field = |at: usize, which: ReceiptField| { + let mut bytes = good.clone(); + bytes[at] ^= 0x01; + assert_eq!( + verify(&bytes, &bundle, A_B), + Err(SofiReceiptVerifyError::Mismatch(which)) + ); + }; + field(4, ReceiptField::Bundle); + field(36, ReceiptField::RouteCommitment); + field(104, ReceiptField::Transitions); + } +} diff --git a/dsm_client/deterministic_state_machine/dsm/tests/route_commitment_x_conformance.rs b/dsm_client/deterministic_state_machine/dsm/tests/route_commitment_x_conformance.rs new file mode 100644 index 00000000..021e1715 --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm/tests/route_commitment_x_conformance.rs @@ -0,0 +1,175 @@ +// SPDX-License-Identifier: Apache-2.0 +#![allow(clippy::disallowed_methods)] // test asserts; a failure here is the signal + +//! CLASS-1 CONFORMANCE VECTOR FOR `X` — amendment 2c-F R1, registry §2.10. +//! +//! R1 ratified the shipped route commitment: +//! +//! ```text +//! X = H_dom(DSM/ext, RC*) +//! RC* = the RouteCommitV1 (version 2) proto3 encoding with +//! initiator_signature cleared: fields ascending, implicit-presence +//! defaults omitted, hops in carried order, no unknown fields +//! ``` +//! +//! `RC*` is a foreign grammar, not CCB, so a second implementation can only +//! reproduce `X` if the grammar is pinned by bytes. The expected bytes below +//! are written by hand from the proto definition — tag bytes, varint lengths, +//! field order — and never produced by `prost` (amendment 2c-C2 ruling D). +//! The production side must agree on both `RC*` and `X`, and must clear a +//! carried signature before hashing. +//! +//! Byte arrays throughout, never hex. + +#[path = "common/indep_ccb.rs"] +mod indep; + +use dsm::types::proto::{RouteCommitHopV1, RouteCommitV1}; + +const VAULT: [u8; 32] = [0x03; 32]; +const TOKEN_IN: [u8; 32] = [0x10; 32]; +const TOKEN_OUT: [u8; 32] = [0x20; 32]; +const NONCE: [u8; 32] = [0x5E; 32]; +const AD_DIGEST: [u8; 32] = [0xAD; 32]; +const UNLOCK_SPEC: [u8; 32] = [0x05; 32]; +const PARENT: [u8; 32] = [0xC0; 32]; +const OWNER_PK: [u8; 64] = [0x0A; 64]; +const INITIATOR_PK: [u8; 64] = [0x1A; 64]; +const FEE_BPS: u32 = 30; + +fn u128_be(v: u64) -> [u8; 16] { + u128::from(v).to_be_bytes() +} + +// ── an independent proto3 writer: only what RC* needs ──────────────────────── + +fn varint(mut v: u64) -> Vec { + let mut out = Vec::new(); + loop { + let byte = (v & 0x7F) as u8; + v >>= 7; + if v == 0 { + out.push(byte); + return out; + } + out.push(byte | 0x80); + } +} + +/// A length-delimited field (wire type 2). +fn len_field(number: u64, bytes: &[u8]) -> Vec { + [ + varint((number << 3) | 2), + varint(bytes.len() as u64), + bytes.to_vec(), + ] + .concat() +} + +/// A varint field (wire type 0). proto3 omits a default; none here is zero. +fn varint_field(number: u64, v: u64) -> Vec { + assert_ne!(v, 0, "a zero value would be omitted, not encoded"); + [varint(number << 3), varint(v)].concat() +} + +fn indep_hop() -> Vec { + [ + len_field(1, &VAULT), + len_field(2, &TOKEN_IN), + len_field(3, &TOKEN_OUT), + len_field(4, &u128_be(1_000)), + len_field(5, &u128_be(453)), + varint_field(6, u64::from(FEE_BPS)), + len_field(7, &AD_DIGEST), + // 8 burned; 11-14 reserved. + len_field(9, &UNLOCK_SPEC), + len_field(10, &OWNER_PK), + len_field(15, &PARENT), + ] + .concat() +} + +/// `RC*`: field 10, `initiator_signature`, is cleared and therefore omitted. +fn indep_rc_star() -> Vec { + [ + varint_field(1, 2), + len_field(2, &NONCE), + len_field(3, &TOKEN_IN), + len_field(4, &TOKEN_OUT), + len_field(5, &u128_be(1_000)), + len_field(6, &u128_be(453)), + varint_field(7, u64::from(FEE_BPS)), + len_field(8, &indep_hop()), + len_field(9, &INITIATOR_PK), + ] + .concat() +} + +fn prod_signed_rc() -> RouteCommitV1 { + RouteCommitV1 { + version: 2, + nonce: NONCE.to_vec(), + input_token: TOKEN_IN.to_vec(), + output_token: TOKEN_OUT.to_vec(), + input_amount_u128: u128_be(1_000).to_vec(), + expected_final_output_amount_u128: u128_be(453).to_vec(), + total_fee_bps: u64::from(FEE_BPS), + hops: vec![RouteCommitHopV1 { + vault_id: VAULT.to_vec(), + token_in: TOKEN_IN.to_vec(), + token_out: TOKEN_OUT.to_vec(), + input_amount_u128: u128_be(1_000).to_vec(), + expected_output_amount_u128: u128_be(453).to_vec(), + fee_bps: FEE_BPS, + advertisement_digest: AD_DIGEST.to_vec(), + unlock_spec_digest: UNLOCK_SPEC.to_vec(), + owner_public_key: OWNER_PK.to_vec(), + parent_binding: PARENT.to_vec(), + }], + initiator_public_key: INITIATOR_PK.to_vec(), + // A carried signature: RC* and X must be blind to it. + initiator_signature: vec![0x99; 128], + } +} + +#[test] +fn the_commitment_form_is_the_hand_written_grammar() { + let expected = indep_rc_star(); + // The hop is longer than 127 bytes, so its length is a two-byte varint — + // the first place a hand-rolled encoder and prost could part company. + assert_eq!(indep_hop().len(), 308); + assert_eq!( + &expected[expected.len() - 66 - 311..][..3], + &[0x42, 0xB4, 0x02] + ); + assert_eq!( + prost::Message::encode_to_vec(&dsm::dlv::route_commit::canonicalise_for_commitment( + &prod_signed_rc() + )), + expected, + "the production commitment form is the frozen RC*" + ); +} + +#[test] +fn x_is_the_ext_domain_hash_of_the_commitment_form() { + let x = indep::h_dom(b"DSM/ext", &indep_rc_star()); + assert_eq!( + dsm::dlv::route_commit::compute_external_commitment(&prod_signed_rc()), + x + ); + // The signature is outside the preimage: a different one, the same X. + let mut resigned = prod_signed_rc(); + resigned.initiator_signature = vec![0x42; 128]; + assert_eq!( + dsm::dlv::route_commit::compute_external_commitment(&resigned), + x + ); + // Every committed byte is inside it: one hop field moved, a different X. + let mut moved = prod_signed_rc(); + moved.hops[0].parent_binding[0] ^= 0x01; + assert_ne!( + dsm::dlv::route_commit::compute_external_commitment(&moved), + x + ); +} diff --git a/dsm_client/deterministic_state_machine/dsm/tests/settlement_bundle_conformance.rs b/dsm_client/deterministic_state_machine/dsm/tests/settlement_bundle_conformance.rs index 2e372a97..be462468 100644 --- a/dsm_client/deterministic_state_machine/dsm/tests/settlement_bundle_conformance.rs +++ b/dsm_client/deterministic_state_machine/dsm/tests/settlement_bundle_conformance.rs @@ -356,6 +356,51 @@ fn market_identities_are_pinned_and_the_decoder_records_the_span() { assert_eq!(dsm::dlv::settlement_bundle::bundle_digest(&bytes), b); } +// ── the Def 14.2 receipt of the market vector (amendment 2c-F, §5.42) ───────── + +/// `a_B` for the vector. The receipt binds the acceptance identity as a bare +/// digest, so any 32 bytes exercise the layout; the walk, not this vector, is +/// what says which acceptance a settlement has. +const A_B: [u8; 32] = [0xAB; 32]; + +#[test] +fn the_market_vector_projects_the_frozen_receipt() { + // Expected bytes from the pinned identities and the independent encoder + // alone: `b` and `c_{n+1}` are the literals pinned above, never recomputed + // by the production helpers. + let expected = [ + indep::envelope(0x0034, 1), + MARKET_B.to_vec(), + X.to_vec(), + A_B.to_vec(), + indep::u32be(1), + MARKET_C_NEXT.to_vec(), + vec![0x00], // witness_hash: absent in schema 1 + ] + .concat(); + assert_eq!(expected.len(), 137, "registry §5.42 pins 137 bytes"); + + let produced = dsm::dlv::sofi_receipt::SofiReceipt::project(&prod_market_bundle(), A_B) + .expect("a market bundle has a receipt"); + assert_eq!( + produced.encode(), + expected, + "the production projection is frozen" + ); + + const TAG: &[u8] = b"DSM/sofi-receipt/v1"; + let rho = indep::h_dom(TAG, &expected); + assert_eq!(produced.digest(), rho); + assert_eq!(produced.address(), indep::storage_addr(TAG, &rho)); + + let decoded = dsm::dlv::sofi_receipt::decode_sofi_receipt(&expected).expect("decodes"); + assert_eq!(decoded, produced); + assert_eq!( + dsm::dlv::sofi_receipt::verify(&expected, &prod_market_bundle(), A_B), + Ok(produced) + ); +} + // ── shape and structure vectors: hand-built bytes the decoder must refuse ───── #[test] @@ -539,8 +584,11 @@ fn every_registry_number_is_in_exactly_one_namespace_set() { // `declared_unencoded` when its encoder landed, so it belongs here or // it belongs to no set at all. 0x0031, 0x0032, 0x0033, + // 0x0034 is the Def 14.2 SofiReceipt (amendment 2c-F R4), allocated + // with its encoder. + 0x0034, ]; - for n in 0x0001u16..=0x0033 { + for n in 0x0001u16..=0x0034 { let sets = [ encodable.contains(&n), reserved::is_reserved(n), @@ -567,6 +615,15 @@ fn every_registry_number_is_in_exactly_one_namespace_set() { "{n:#06x} schema 1 is burned" ); } + // 2c-F R1 ratified the shipped X, so `R` and `Q` have no encoder at ANY + // schema: both classes are burned outright, never merely unencoded. + for n in [0x000C, 0x0017] { + assert!( + burned_class::is_burned_class(n), + "{n:#06x} burned by 2c-F R1" + ); + assert!(!declared_unencoded::is_declared_unencoded(n)); + } // 2c-E's burns: the intent cut, and the two classes it propagates through. // Recorded in the machine-readable table, not only in a comment, so a // schema-1 envelope classifies as BURNED rather than as an unknown schema — diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/dlv_routes.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/dlv_routes.rs index 13257548..0b708dd8 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/dlv_routes.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/dlv_routes.rs @@ -3631,10 +3631,11 @@ impl AppRouterImpl { // bundle-acceptance leaf (2c-D producer adoption) and the // response reports it; deriving it twice would be two chances // to derive it differently. - let b = match dsm::dlv::settlement_bundle::canon(&bundle) { - Ok(c) => dsm::dlv::settlement_bundle::bundle_digest(&c), + let bundle_canon = match dsm::dlv::settlement_bundle::canon(&bundle) { + Ok(c) => c, Err(e) => return err(format!("dlv.unlockRouted: canon: {e:?}")), }; + let b = dsm::dlv::settlement_bundle::bundle_digest(&bundle_canon); // `expected_successor` is the exact successor the bundle was // BOUND to. The advance refuses if it would commit any other, // checked after the pure prepare and before anything is @@ -3695,6 +3696,7 @@ impl AppRouterImpl { }, receipt_id, b, + bundle: bundle_canon, rel_key, fenced_parent: embedded_parent, permitted_successor: prepared.trader_successor(), @@ -3811,6 +3813,9 @@ struct MarketCompletion { trade: dsm::dlv::settlement_receipt_leaf::SettledTrade, receipt_id: [u8; 32], b: [u8; 32], + /// `CCB(B)`, the exact bound bundle `b` names: what the Def 14.2 receipt + /// projects and publishes (2c-F). + bundle: Vec, /// The fence's coordinates, exactly as `bind_settlement` placed it. rel_key: [u8; 32], fenced_parent: [u8; 32], @@ -3840,6 +3845,7 @@ enum CompletionOutcome { /// compose with that V1 as the candidate the walk is the only certifier /// require a CERTIFIED fold for exactly b may_certify(), or nothing /// freeze V1, sweep, require quorum durable BEFORE release (point 4) +/// freeze the Def 14.2 receipt closure for S_v an obligation, NEVER a gate (2c-F R6) /// SuccessorAccepted at the exact placed fence only now; twice is not an error /// ``` /// @@ -3926,14 +3932,16 @@ async fn complete_settlement( Ok(composed) => composed, Err(e) => return Pending(format!("the settlement is not certifiable yet: {e}")), }; - let Some(certified) = composed + let Some(fold) = composed .folded_parents .iter() .find(|f| f.bound_by == c.b && f.verdict.may_certify()) - .and_then(|f| f.realized_trade.as_ref()) else { return Pending("no certified fold for this bundle yet".into()); }; + let Some(certified) = fold.realized_trade.as_ref() else { + return Pending("no certified fold for this bundle yet".into()); + }; if certified.vault_id() != c.vault_id || certified.receipt_id() != c.receipt_id || certified.trade() != c.trade @@ -3946,6 +3954,29 @@ async fn complete_settlement( // released only once a quorum of that set holds the exact bytes. Freezing // the same bytes again is a no-op. let bytes = crate::sdk::settlement_receipt_codec::receipt_to_proto(&receipt).encode_to_vec(); + // THE DEF 14.2 RECEIPT (2c-F) — an obligation this certification creates, + // never a condition of the release below (R6). Projected here and only + // here, from the certified fold's own acceptance; frozen for the vault's + // authenticated committed set; published by the same sweep. Any failure is + // reported and never holds the fence. + let sofi_closure = fold + .certified_acceptance + .as_ref() + .ok_or_else(|| "the certified fold carries no acceptance".to_string()) + .and_then(|acceptance| { + crate::sdk::sofi_receipt_publication::closure( + &c.bundle, + acceptance, + composed.storage_set_id, + ) + }) + .and_then(|closure| { + if closure.receipt.bundle() == c.b { + Ok(closure) + } else { + Err("the carried bundle is not the one this settlement bound".to_string()) + } + }); { let binding = match crate::storage::client_db::get_connection() { Ok(binding) => binding, @@ -3962,6 +3993,22 @@ async fn complete_settlement( ) { return Pending(format!("the settlement receipt could not be frozen: {e}")); } + match &sofi_closure { + Ok(closure) => { + if let Err(e) = + crate::sdk::sofi_receipt_publication::freeze_closure_with_conn(&conn, closure) + { + log::error!( + "[settlement completion] the Def 14.2 receipt could not be frozen ({e}); \ + the release does not wait for it" + ); + } + } + Err(e) => log::error!( + "[settlement completion] no Def 14.2 receipt for this settlement ({e}); the \ + release does not wait for it" + ), + } } let receipt_published = |key: &str| fpa::is_artifact_published(key).unwrap_or(false); if !receipt_published(&receipt_key) { @@ -4168,6 +4215,7 @@ pub(crate) async fn resume_settlement_completion( }, receipt_id: settlement_receipt_id, b, + bundle: bytes, rel_key: stored.trader_chain_id, fenced_parent: stored.trader_parent_state_commitment, permitted_successor, @@ -9407,6 +9455,205 @@ mod funded_creation_tests { ); } + /// The Def 14.2 receipt closure of a realized settlement, read back from + /// what the fleet and the fold hold — never from the completion's own + /// return value. + fn realized_receipt_closure( + vault_id: &[u8; 32], + pc_a: &[u8; 32], + pc_b: &[u8; 32], + b: &[u8; 32], + ) -> ( + crate::sdk::sofi_receipt_publication::ReceiptClosure, + crate::sdk::vault_state_composition::ComposedVaultState, + Vec, + ) { + let frontier = composed_frontier(vault_id, pc_a, pc_b); + let acceptance = frontier + .folded_parents + .iter() + .find(|f| f.bound_by == *b) + .and_then(|f| f.certified_acceptance.clone()) + .expect("a certified market fold carries the acceptance §7 accepted"); + let bundle = crate::runtime::get_runtime() + .block_on(crate::sdk::storage_io::fetch_immutable_payload( + dsm::common::domain_tags::TAG_DSM_SETTLEMENT_BUNDLE, + b, + )) + .expect("bundle read") + .expect("the bound bundle is held"); + let closure = crate::sdk::sofi_receipt_publication::closure( + &bundle, + &acceptance, + frontier.storage_set_id, + ) + .expect("a certified market settlement has a receipt closure"); + (closure, frontier, bundle) + } + + /// 2c-F — a realized settlement's Def 14.2 receipt is exactly the + /// projection of `(B, the certified TA_B)`, frozen for the vault's OWN + /// committed set, and published there by the generic sweep. + #[test] + #[serial] + fn a_realized_settlement_publishes_its_def_14_2_receipt_on_the_vaults_set() { + use crate::sdk::sofi_receipt_publication::{publication, ClosurePublication}; + + install_identity(); + let (vault_id, (pc_a, pc_b), _owner_dev, traders) = + market_with_traders("sofi/spec/sofi-receipt", &[("trader0", 0x51)]); + let trader_dev = &traders[0]; + trader_dev.enter(); + let trader = trader_dev.router(); + let out = crate::sdk::routing_path_sdk::constant_product_output(1_000, 10_000, 5_000, 30) + .expect("curve output"); + let (res, x) = trader_settles( + trader, + &trader_dev.ak_pk.clone(), + &trader_dev.device_id, + &vault_id, + &pc_a, + &pc_b, + 0, + (10_000, 5_000), + 1_000, + out, + 0xF1, + ); + assert!(res.success, "the settle realizes: {:?}", res.error_message); + let b = settle_outcome(&res, "realized"); + crate::runtime::get_runtime() + .block_on(crate::handlers::artifact_republish::republish_unpublished_artifacts()) + .expect("sweep"); + + let (closure, frontier, bundle) = realized_receipt_closure(&vault_id, &pc_a, &pc_b, &b); + assert_eq!( + publication(&closure).expect("publication state"), + ClosurePublication::Published, + "receipt, bundle and acceptance are each at quorum on the vault's own set" + ); + let receipt_row = crate::storage::client_db::frozen_publication_artifact::get_artifact( + &closure.objects[0].key, + &crate::storage::client_db::frozen_publication_artifact::content_digest( + &closure.objects[0].key, + &closure.objects[0].bytes, + ), + ) + .expect("row read") + .expect("the completion froze the receipt"); + assert_eq!( + receipt_row.storage_set_id, frontier.storage_set_id, + "frozen for the set the composed V_n commits, not a locally chosen one" + ); + + // EXACTLY THE PROJECTION of the bound bundle and the certified acceptance. + let decoded = dsm::dlv::settlement_bundle::decode_canonical(&bundle).expect("canonical"); + let a_b = frontier + .folded_parents + .iter() + .find(|f| f.bound_by == b) + .and_then(|f| f.certified_acceptance.as_ref()) + .expect("acceptance") + .ta_b() + .expect("ta_b"); + let receipt = + dsm::dlv::sofi_receipt::verify(&closure.objects[0].bytes, &decoded.bundle, a_b) + .expect("the published receipt is the projection"); + assert_eq!(receipt.bundle(), b); + assert_eq!(receipt.route_commitment(), x, "the shipped X (2c-F R1)"); + assert_eq!(receipt.trader_acceptance(), a_b); + assert_eq!( + receipt.successors(), + &[frontier.c_n], + "the realized successor" + ); + assert_eq!( + crate::sdk::storage_io::fake_fleet::any_member_holding(&closure.objects[0].key), + Some(closure.objects[0].bytes.clone()), + "held at the receipt's own content address" + ); + } + + /// 2c-F R6 — the receipt NEVER gates the release. With every receipt PUT + /// refused the settlement still realizes and its fence releases, leaving + /// the receipt an owed obligation. Once healed, the sweep alone publishes + /// the same bytes: no binding round, no transition, no re-fence. + #[test] + #[serial] + fn the_def_14_2_receipt_never_gates_the_release_and_publishes_after_it() { + use crate::sdk::sofi_receipt_publication::{publication, ClosurePublication}; + + install_identity(); + let (vault_id, (pc_a, pc_b), _owner_dev, traders) = + market_with_traders("sofi/spec/sofi-receipt-late", &[("trader0", 0x51)]); + let trader_dev = &traders[0]; + trader_dev.enter(); + let trader = trader_dev.router(); + let (rel_key, fenced_parent) = trader_position_of(trader_dev); + let out = crate::sdk::routing_path_sdk::constant_product_output(1_000, 10_000, 5_000, 30) + .expect("curve output"); + const RECEIPT_KEYS: &str = "immutable::DSM/sofi-receipt/v1::"; + crate::sdk::storage_io::fake_fleet::fail_keys_with_prefix(RECEIPT_KEYS); + let (res, _x) = trader_settles( + trader, + &trader_dev.ak_pk.clone(), + &trader_dev.device_id, + &vault_id, + &pc_a, + &pc_b, + 0, + (10_000, 5_000), + 1_000, + out, + 0xF2, + ); + assert!(res.success, "the settle realizes: {:?}", res.error_message); + let b = settle_outcome(&res, "realized"); + let fence_state = || { + crate::storage::client_db::trader_parent_fence::get_fence(&rel_key, &fenced_parent, &b) + .expect("fence read") + .expect("the fence row") + .state + }; + assert_eq!( + fence_state(), + dsm::dlv::trader_fence::FenceState::Released, + "released on C2's condition although the receipt is below quorum" + ); + let (closure, _, _) = realized_receipt_closure(&vault_id, &pc_a, &pc_b, &b); + assert!( + matches!( + publication(&closure).expect("publication state"), + ClosurePublication::Pending(_) + ), + "the receipt is owed, not published" + ); + + // HEALED: the generic sweep finishes the obligation, and nothing else moves. + crate::sdk::storage_io::fake_fleet::heal_keys_with_prefix(RECEIPT_KEYS); + let root_before = trader.core_sdk.device_head().expect("trader head").root(); + let binds_before = crate::sdk::binding_fleet_double::cas_log().len(); + crate::runtime::get_runtime() + .block_on(crate::handlers::artifact_republish::republish_unpublished_artifacts()) + .expect("sweep"); + assert_eq!( + publication(&closure).expect("publication state"), + ClosurePublication::Published, + "the same frozen bytes, published after the release" + ); + assert_eq!(fence_state(), dsm::dlv::trader_fence::FenceState::Released); + assert_eq!( + trader.core_sdk.device_head().expect("trader head").root(), + root_before, + "no transition and no admission" + ); + assert_eq!( + crate::sdk::binding_fleet_double::cas_log().len(), + binds_before, + "no binding round" + ); + } + /// 2c-D §14, D-f (e): the continuation cannot operate on an UNCERTIFIED /// settlement. The acceptance's locator is withheld, so the settle binds /// and advances but the walk cannot find `TA_B` and certifies nothing. @@ -9470,6 +9717,17 @@ mod funded_creation_tests { ); held_fence(&rel_key, &fenced_parent, &b); assert!(no_receipt(), "and the resume froze no receipt for it"); + // …NOR A DEF 14.2 RECEIPT: it is projected only from a certified fold + // (2c-F R6), so an uncertified settlement has none to publish. + assert!( + crate::storage::client_db::frozen_publication_artifact::find_current_payload_with_prefix_and_purpose( + "immutable::DSM/sofi-receipt/v1::", + crate::sdk::sofi_receipt_publication::RECEIPT_PURPOSE, + ) + .expect("row read") + .is_none(), + "no Def 14.2 receipt exists for an uncertified settlement" + ); let frontier = composed_frontier(&vault_id, &pc_a, &pc_b); match frontier.frontier_binding { diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/mod.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/mod.rs index 3207e7c6..728f5761 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/mod.rs @@ -118,6 +118,7 @@ pub mod routing_sdk; pub mod settlement_receipt_codec; pub mod settlement_slot; pub mod smart_commitment_sdk; +pub(crate) mod sofi_receipt_publication; pub mod trader_acceptance_locator; pub mod transfer_hooks; pub mod vault_rehydration; diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/route_commit_sdk.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/route_commit_sdk.rs index 6455b202..0d3dc306 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/route_commit_sdk.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/route_commit_sdk.rs @@ -29,8 +29,8 @@ use crate::sdk::routing_path_sdk::Path; use crate::util::text_id::encode_base32_crockford; /// BLAKE3 domain tag for the external commitment derivation -/// `X = BLAKE3("DSM/ext\0" || canonical(RouteCommit))`. -/// Matches SoFi spec §3.2 `ExtCommit(X) = H("DSM/ext" || X)`. +/// `X = BLAKE3("DSM/ext\0" || canonical(RouteCommit))` — Rev 15 §9.3 as +/// amended by 2c-F R1: `X` IS the external commitment, with no second digest. pub(crate) const EXT_COMMIT_DOMAIN: dsm::crypto::domain::TaggedHashDomain<'static> = dsm::common::domain_tags::TAG_DSM_EXT_COMMIT; diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_receipt_publication.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_receipt_publication.rs new file mode 100644 index 00000000..52605b55 --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_receipt_publication.rs @@ -0,0 +1,312 @@ +// SPDX-License-Identifier: Apache-2.0 + +//! The Def 14.2 receipt's publication obligation (amendment 2c-F, R5 and R6). +//! +//! AN OBLIGATION, NEVER A GATE. Once the walk certifies a market settlement, +//! its completion freezes the receipt closure for the vault's authenticated +//! committed storage set `S_v`, re-derived from the composed `V_n`: +//! +//! ```text +//! SofiReceipt the projection of (B, TA_B) DSM/sofi-receipt/v1 +//! CCB(B) the bound bundle, byte for byte DSM/settlement-bundle +//! CCB(TA_B) the acceptance §7 certified DSM/trader-settlement-acceptance/v2 +//! ``` +//! +//! The ONE generic sweep then replays those exact bytes until a quorum of `S_v` +//! holds each. Nothing waits for that. The fence releases on C2's condition +//! alone, and a closure below quorum is a pending obligation — never a reason +//! to re-fence, re-bind, re-admit or re-certify (the ruling on R6). +//! +//! NOTHING READS THIS AS AUTHORITY (R7). [`publication`] reports whether the +//! obligation is met, and nothing more. No composition, admission, +//! realization, fence, certification or reserve-provenance path may consult it. +//! +//! ONE SET PER ROW. A frozen row binds one storage set per `(key, digest)`. If +//! `TA_B` was already frozen by its admission for a DIFFERENT set, freezing it +//! again for `S_v` is a no-op, and [`publication`] reports +//! [`ClosurePublication::BoundToAnotherSet`] rather than counting the other +//! set's quorum as `S_v`'s. Every beta consumer resolves the one catalog set, +//! so beta never reaches that arm. + +use anyhow::Result; +use dsm::common::domain_tags::{ + TAG_DSM_SETTLEMENT_BUNDLE, TAG_DSM_SOFI_RECEIPT_V1, TAG_DSM_TRADER_SETTLEMENT_ACCEPTANCE, +}; +use dsm::dlv::sofi_receipt::SofiReceipt; +use dsm::economic::trader_acceptance::TraderAcceptance; + +use crate::sdk::economic_registers::immutable_object_key; +use crate::storage::client_db::frozen_publication_artifact as fpa; + +/// The frozen-artifact purpose of the receipt row itself. +pub(crate) const RECEIPT_PURPOSE: &str = "sofi-receipt"; +const BUNDLE_PURPOSE: &str = "sofi-receipt-bundle"; +const ACCEPTANCE_PURPOSE: &str = "sofi-receipt-acceptance"; + +/// One member of the publication set: the exact bytes and the immutable key +/// they travel under. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct ClosureObject { + pub key: String, + pub bytes: Vec, + pub purpose: &'static str, +} + +/// `P(ρ_B)` for one settlement, bound to the set its quorum is counted on. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct ReceiptClosure { + pub receipt: SofiReceipt, + pub storage_set_id: [u8; 32], + /// The receipt, the bundle and the acceptance, in that order. + pub objects: [ClosureObject; 3], +} + +/// The closure of the settlement whose canonical bundle is `bundle_canon` and +/// whose certified acceptance is `acceptance`, for storage set +/// `storage_set_id`. +/// +/// A pure projection: the same inputs produce the same keys and bytes on +/// every call, which is what makes re-freezing and re-publishing idempotent. +pub(crate) fn closure( + bundle_canon: &[u8], + acceptance: &TraderAcceptance, + storage_set_id: [u8; 32], +) -> std::result::Result { + let decoded = dsm::dlv::settlement_bundle::decode_canonical(bundle_canon) + .map_err(|e| format!("the bundle is not canonical: {e}"))?; + let acceptance_bytes = acceptance + .encode() + .map_err(|e| format!("the acceptance does not encode: {e}"))?; + let a_b = acceptance + .ta_b() + .map_err(|e| format!("the acceptance has no identity: {e}"))?; + let receipt = SofiReceipt::project(&decoded.bundle, a_b).map_err(|e| e.to_string())?; + let object = |namespace, bytes: Vec, purpose| ClosureObject { + key: immutable_object_key(namespace, &bytes), + bytes, + purpose, + }; + Ok(ReceiptClosure { + objects: [ + object(TAG_DSM_SOFI_RECEIPT_V1, receipt.encode(), RECEIPT_PURPOSE), + object( + TAG_DSM_SETTLEMENT_BUNDLE, + bundle_canon.to_vec(), + BUNDLE_PURPOSE, + ), + object( + TAG_DSM_TRADER_SETTLEMENT_ACCEPTANCE, + acceptance_bytes, + ACCEPTANCE_PURPOSE, + ), + ], + receipt, + storage_set_id, + }) +} + +/// Freeze every member of `closure` for its set. Re-freezing identical bytes +/// is a no-op, so this is safe on every completion pass. +pub(crate) fn freeze_closure_with_conn( + conn: &rusqlite::Connection, + closure: &ReceiptClosure, +) -> Result<()> { + let b = closure.receipt.bundle(); + for o in &closure.objects { + fpa::freeze_artifact_with_conn( + conn, + &closure.storage_set_id, + &o.key, + &o.bytes, + &b, + o.purpose, + )?; + } + Ok(()) +} + +/// Where the obligation stands. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ClosurePublication { + /// Every member is frozen for `S_v` and a quorum of `S_v` holds it. + Published, + /// Some member is not frozen yet, or not yet at quorum. The sweep owes it. + Pending(String), + /// A member's only frozen row is bound to another storage set, whose + /// quorum is not `S_v`'s. + BoundToAnotherSet { purpose: &'static str }, +} + +/// Whether `closure` is published over its own set (Req 14.6, as 2c-F states +/// it). A report, never an input to any validity or release decision. +pub(crate) fn publication(closure: &ReceiptClosure) -> Result { + for o in &closure.objects { + let digest = fpa::content_digest(&o.key, &o.bytes); + match fpa::get_artifact(&o.key, &digest)? { + None => { + return Ok(ClosurePublication::Pending(format!( + "{} is not frozen", + o.purpose + ))) + } + Some(row) if row.storage_set_id != closure.storage_set_id => { + return Ok(ClosurePublication::BoundToAnotherSet { purpose: o.purpose }) + } + Some(row) if row.state != fpa::ArtifactState::Published => { + return Ok(ClosurePublication::Pending(format!( + "{} is {}", + o.purpose, + row.state.as_str() + ))) + } + Some(_) => {} + } + } + Ok(ClosurePublication::Published) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::storage::client_db::{get_connection, init_database, reset_database_for_tests}; + use dsm::ccb::settlement::fixtures; + use dsm::economic::state::EconomicBundleAcceptanceState; + use serial_test::serial; + + const PARENT: [u8; 32] = [0xC0; 32]; + const SET: [u8; 32] = [0xB2; 32]; + const OTHER_SET: [u8; 32] = [0xA1; 32]; + + fn bundle_canon() -> Vec { + let bundle = fixtures::market_bundle( + PARENT, + fixtures::successor(PARENT, 1_010_000, 495_065), + [0x58; 32], + ); + dsm::dlv::settlement_bundle::canon(&bundle).expect("canon") + } + + fn acceptance(b: [u8; 32]) -> TraderAcceptance { + TraderAcceptance::new( + [0x11; 32], + 3, + EconomicBundleAcceptanceState { + bundle: b, + economic_operation_id: [0x50; 32], + }, + vec![[0x00; 32]; dsm::economic::tree::ECONOMIC_SMT_HEIGHT], + ) + .expect("well formed") + } + + fn fixture_closure(set: [u8; 32]) -> ReceiptClosure { + let canon = bundle_canon(); + let b = dsm::dlv::settlement_bundle::bundle_digest(&canon); + closure(&canon, &acceptance(b), set).expect("closure") + } + + fn freeze(closure: &ReceiptClosure) { + let binding = get_connection().expect("db"); + let conn = binding.lock().unwrap_or_else(|p| p.into_inner()); + freeze_closure_with_conn(&conn, closure).expect("freeze"); + } + + #[test] + fn a_closure_is_a_pure_projection_of_its_inputs() { + let one = fixture_closure(SET); + assert_eq!( + one, + fixture_closure(SET), + "same inputs, same keys and bytes" + ); + assert_eq!( + one.objects[1].bytes, + bundle_canon(), + "the bundle travels byte for byte" + ); + assert_eq!( + one.receipt.bundle(), + dsm::dlv::settlement_bundle::bundle_digest(&bundle_canon()) + ); + assert_eq!( + one.receipt.trader_acceptance(), + acceptance(one.receipt.bundle()).ta_b().expect("ta_b"), + "a_B is the acceptance's inner identity" + ); + for (o, ns) in one.objects.iter().zip([ + TAG_DSM_SOFI_RECEIPT_V1, + TAG_DSM_SETTLEMENT_BUNDLE, + TAG_DSM_TRADER_SETTLEMENT_ACCEPTANCE, + ]) { + assert_eq!(o.key, immutable_object_key(ns, &o.bytes)); + } + } + + #[test] + #[serial] + fn an_obligation_is_pending_until_every_member_is_frozen_and_at_quorum() { + reset_database_for_tests(); + init_database().expect("init"); + let c = fixture_closure(SET); + assert!(matches!( + publication(&c).unwrap(), + ClosurePublication::Pending(_) + )); + freeze(&c); + assert!( + matches!(publication(&c).unwrap(), ClosurePublication::Pending(_)), + "frozen is owed, not published" + ); + freeze(&c); // idempotent + for o in &c.objects { + fpa::upsert_artifact_publication_state( + &o.key, + &fpa::content_digest(&o.key, &o.bytes), + fpa::ArtifactState::Published, + "", + ) + .expect("mark published"); + } + assert_eq!(publication(&c).unwrap(), ClosurePublication::Published); + } + + /// The honesty arm: a member frozen for ANOTHER set is reported, never + /// counted as published on `S_v` — even when that other row is published. + #[test] + #[serial] + fn a_member_frozen_for_another_set_is_reported_not_counted() { + reset_database_for_tests(); + init_database().expect("init"); + let c = fixture_closure(SET); + let acceptance = &c.objects[2]; + { + let binding = get_connection().expect("db"); + let conn = binding.lock().unwrap_or_else(|p| p.into_inner()); + fpa::freeze_artifact_with_conn( + &conn, + &OTHER_SET, + &acceptance.key, + &acceptance.bytes, + &[0u8; 32], + "trader-settlement-acceptance", + ) + .expect("admission freeze"); + } + freeze(&c); + for o in &c.objects { + fpa::upsert_artifact_publication_state( + &o.key, + &fpa::content_digest(&o.key, &o.bytes), + fpa::ArtifactState::Published, + "", + ) + .expect("mark published"); + } + assert_eq!( + publication(&c).unwrap(), + ClosurePublication::BoundToAnotherSet { + purpose: "sofi-receipt-acceptance" + } + ); + } +} diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_state_composition.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_state_composition.rs index 6d0be8c3..be93104e 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_state_composition.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_state_composition.rs @@ -117,6 +117,11 @@ pub(crate) struct FoldedParent { /// close. This is what an owner's reconcile acts on (2c-D §14, C2-R1 /// point 6): the exact certified fold, never a receipt read on the side. pub realized_trade: Option, + /// For a CERTIFIED market fold, the exact `TA_B` 2c-D §7 accepted for it — + /// the acceptance the Def 14.2 receipt binds (amendment 2c-F). `None` for + /// a close. Carried so the receipt is built from what certified, never + /// from an acceptance fetched again afterwards. + pub certified_acceptance: Option, } /// What the binding register — plus this device's own fence table — says about @@ -753,10 +758,11 @@ async fn compose_vault_state_inner( // (2c-D §14, C2-R1 point 3): CORR.1–CORR.5, 2c-D §7's acceptance // witness, and Tier-1 intent satisfaction. Nothing uncertified is ever // installed as the composed state. - let (verdict, realized_trade) = match bound.shape { + let (verdict, realized_trade, certified_acceptance) = match bound.shape { dsm::dlv::settlement_bundle::BundleShape::OwnerClose => ( C3Verdict::Valid(CompleteValidity::from_close_witness(witness)), None, + None, ), dsm::dlv::settlement_bundle::BundleShape::Market => { let (Some(ev), Some(terms)) = (market_evidence.take(), bound.bundle.market_terms()) @@ -798,6 +804,7 @@ async fn compose_vault_state_inner( ( C3Verdict::Valid(CompleteValidity::from_market_witness(witness, realization)), Some(ev.receipt), + Some(ev.acceptance), ) } }; @@ -815,6 +822,7 @@ async fn compose_vault_state_inner( bound_kind: bound.shape, verdict, realized_trade, + certified_acceptance, }); let _ = transition; cursor_state = next_state; diff --git a/lean4/DSMSofiReceipt.lean b/lean4/DSMSofiReceipt.lean new file mode 100644 index 00000000..42ffce54 --- /dev/null +++ b/lean4/DSMSofiReceipt.lean @@ -0,0 +1,197 @@ +/- + The Def 14.2 SofiReceipt obligation — self-contained Lean 4 (no Mathlib, no imports) + + Machine-checks amendment 2c-F's owner rulings on R6 against C2's completion + pass (DSMSettlementCompletion), restated here over one record: + + - NEVER A GATE the fence follows C2's rule alone: certification and V1 at + quorum. The receipt's existence, its publication and + whether a quorum is reachable for it change nothing about + the release + - AFTER CERTIFY a receipt obligation is created only by a certified pass + - AFTER RELEASE a released fence with its receipt still owed is + reachable, and the sweep alone then publishes it + - RECOVERABLE the sweep finishes a frozen obligation, and never moves + the fence, the bundle, the successor or V1 + - IDEMPOTENT a second pass or a second sweep changes nothing + + What this module does NOT claim: + + * The projection. That the receipt's bytes are the projection of (B, TA_B) + is `dsm::dlv::sofi_receipt`'s, pinned by its class-1 vector; here the + receipt is a flag. + * Certification and quorum. Both are inputs, re-supplied every pass, as in + DSMSettlementCompletion. + * Which set. That the obligation is counted on the vault's authenticated + committed set is the SDK's; here there is one set. + + Mutation controls, executed rather than asserted — the kernel proving the + NEGATION of a named sample theorem: + + 1. the release also waits for the receipt at quorum + -> `the_release_does_not_wait_for_the_receipt` is proved FALSE + 2. the obligation is created without certification + -> `an_uncertified_settlement_has_no_receipt` is proved FALSE + + Both mutations were reverted; this file is the unmutated module. +-/ + +namespace DSMSofiReceipt + +inductive Fence where + | held + | released + deriving DecidableEq, Repr + +/-- One bound, advanced market settlement: C2's state, plus the 2c-F +obligation. `b` and `successor` are fixed at binding. -/ +structure Settlement where + b : Nat + successor : Nat + /-- V1 at quorum — C2's release condition. -/ + v1Published : Bool + fence : Fence + /-- The receipt closure is frozen: the obligation exists. -/ + receiptFrozen : Bool + /-- The receipt closure is at quorum on the vault's set. -/ + receiptPublished : Bool + deriving DecidableEq, Repr + +/-- What one pass meets. -/ +structure World where + certifiable : Bool + v1QuorumReachable : Bool + receiptQuorumReachable : Bool + deriving DecidableEq, Repr + +/-- **One completion pass** (`complete_settlement`): C2's pass, with the +obligation frozen in the certified branch and swept in the same pass. A +released fence is finished; D-f never resumes it. -/ +def pass (w : World) (s : Settlement) : Settlement := + match s.fence with + | .released => s + | .held => + if w.certifiable then + let v1 := s.v1Published || w.v1QuorumReachable + { s with + fence := if v1 then .released else .held, + v1Published := v1, + receiptFrozen := true, + receiptPublished := s.receiptPublished || w.receiptQuorumReachable } + else s + +/-- **The generic sweep**: replays a frozen obligation, and touches nothing else. -/ +def sweep (w : World) (s : Settlement) : Settlement := + { s with receiptPublished := s.receiptPublished || (s.receiptFrozen && w.receiptQuorumReachable) } + +/-- C2's release rule, stated over C2's inputs only. -/ +def c2Releases (w : World) (s : Settlement) : Bool := + s.fence == .released || (w.certifiable && (s.v1Published || w.v1QuorumReachable)) + +-- ───────────────────────────────────────────────────────────────────────────── +-- General statements +-- ───────────────────────────────────────────────────────────────────────────── + +/-- **NEVER A GATE.** The fence a pass produces is C2's rule, and nothing else. -/ +theorem the_fence_follows_c2s_rule_alone (w : World) (s : Settlement) : + ((pass w s).fence = .released) ↔ c2Releases w s = true := by + obtain ⟨b, succ, v1, fence, rf, rp⟩ := s + obtain ⟨c, q, rq⟩ := w + cases fence <;> cases v1 <;> cases c <;> cases q <;> simp [pass, c2Releases] + +/-- **NEVER A GATE.** Neither the receipt's state nor its reachability moves the +fence. -/ +theorem the_receipt_never_moves_the_fence + (w : World) (s : Settlement) (r f p : Bool) : + (pass { w with receiptQuorumReachable := r } + { s with receiptFrozen := f, receiptPublished := p }).fence + = (pass w s).fence := by + obtain ⟨b, succ, v1, fence, rf, rp⟩ := s + obtain ⟨c, q, rq⟩ := w + cases fence <;> cases v1 <;> cases c <;> cases q <;> simp [pass] + +/-- **AFTER CERTIFY.** A pass that creates the obligation was certified. -/ +theorem a_receipt_is_created_only_by_a_certified_pass + (w : World) (s : Settlement) + (h0 : s.receiptFrozen = false) (h1 : (pass w s).receiptFrozen = true) : + w.certifiable = true := by + obtain ⟨b, succ, v1, fence, rf, rp⟩ := s + obtain ⟨c, q, rq⟩ := w + cases fence <;> cases c <;> simp_all [pass] + +/-- **RECOVERABLE.** A frozen obligation is finished by the sweep alone. -/ +theorem the_sweep_finishes_a_frozen_obligation + (w : World) (s : Settlement) + (hf : s.receiptFrozen = true) (hq : w.receiptQuorumReachable = true) : + (sweep w s).receiptPublished = true := by + simp [sweep, hf, hq] + +/-- **RECOVERABLE.** The sweep never touches the settlement or its release. -/ +theorem the_sweep_changes_nothing_but_publication (w : World) (s : Settlement) : + (sweep w s).fence = s.fence ∧ (sweep w s).b = s.b + ∧ (sweep w s).successor = s.successor ∧ (sweep w s).v1Published = s.v1Published + ∧ (sweep w s).receiptFrozen = s.receiptFrozen := by + simp [sweep] + +/-- **IDEMPOTENT.** -/ +theorem a_second_pass_changes_nothing (w : World) (s : Settlement) : + pass w (pass w s) = pass w s := by + obtain ⟨b, succ, v1, fence, rf, rp⟩ := s + obtain ⟨c, q, rq⟩ := w + cases fence <;> cases v1 <;> cases c <;> cases q <;> cases rp <;> cases rq <;> simp [pass] + +theorem a_second_sweep_changes_nothing (w : World) (s : Settlement) : + sweep w (sweep w s) = sweep w s := by + obtain ⟨b, succ, v1, fence, rf, rp⟩ := s + obtain ⟨c, q, rq⟩ := w + cases rf <;> cases rp <;> cases rq <;> simp [sweep] + +-- ───────────────────────────────────────────────────────────────────────────── +-- Samples — the statements above are not vacuous +-- ───────────────────────────────────────────────────────────────────────────── + +def bound : Settlement := + { b := 7, successor := 12, v1Published := false, fence := .held, + receiptFrozen := false, receiptPublished := false } + +/-- Certified, V1 reachable, every receipt PUT refused. -/ +def receiptRefused : World := + { certifiable := true, v1QuorumReachable := true, receiptQuorumReachable := false } +def healed : World := + { certifiable := true, v1QuorumReachable := true, receiptQuorumReachable := true } +def uncertified : World := + { certifiable := false, v1QuorumReachable := true, receiptQuorumReachable := true } + +/-- The release does not wait: released with the receipt still owed. -/ +theorem the_release_does_not_wait_for_the_receipt : + (pass receiptRefused bound).fence = .released + ∧ (pass receiptRefused bound).receiptFrozen = true + ∧ (pass receiptRefused bound).receiptPublished = false := by + decide + +/-- …and the sweep alone, once healed, publishes it after the release. -/ +theorem the_sweep_publishes_after_the_release : + (sweep healed (pass receiptRefused bound)).receiptPublished = true + ∧ (sweep healed (pass receiptRefused bound)).fence = .released := by + decide + +/-- No certification, no receipt — whatever quorum offers. -/ +theorem an_uncertified_settlement_has_no_receipt : + (pass uncertified bound).receiptFrozen = false := by decide + +-- ───────────────────────────────────────────────────────────────────────────── +-- Axiom report +-- ───────────────────────────────────────────────────────────────────────────── + +#print axioms the_fence_follows_c2s_rule_alone +#print axioms the_receipt_never_moves_the_fence +#print axioms a_receipt_is_created_only_by_a_certified_pass +#print axioms the_sweep_finishes_a_frozen_obligation +#print axioms the_sweep_changes_nothing_but_publication +#print axioms a_second_pass_changes_nothing +#print axioms a_second_sweep_changes_nothing +#print axioms the_release_does_not_wait_for_the_receipt +#print axioms the_sweep_publishes_after_the_release +#print axioms an_uncertified_settlement_has_no_receipt + +end DSMSofiReceipt