diff --git a/.github/instructions/sofispecs.instructions.md b/.github/instructions/sofispecs.instructions.md index 0eb4d402..0e0127ca 100644 --- a/.github/instructions/sofispecs.instructions.md +++ b/.github/instructions/sofispecs.instructions.md @@ -562,6 +562,17 @@ nor constitutes a new approval, veto, rollback, or ordering step. If a terminal SoFi: Sovereign Deterministic Finance Revision 15 has already become binding-final and folded under Requirement 6.30, the DLV is retired and no separate catch-up step is required for that closed vault. +Implementation (amendment 2c-G, rulings G1 + G2). Catch-up applies each certified market +successor V_g → V_n in causal order as one admitted DlvOwnerApplyV2 per generation: a +synchronization step that consumes certified history and never creates it — no authority, no second +value move, no re-certification, no new realization boundary, no veto and no ordering step. Each +apply's input-reserve credit is funded by the trader's own admitted payment (0x0027), whose +evidence is projected from the exact receipt leaf and path the composition walk proved under the +trader's validated root when it certified that fold; the terminal owner reserve state equals the +composed frontier. One engine runs it — automatically on storage.sync and on an explicit owner +request — and it gates no trader settlement, market realization, composition, future admission, +QuorumBind, fence release or close finality. A failure is local to its vault, and an interrupted +catch-up resumes idempotently after its last durable apply. Requirement 4.6 (Governed reverse encumbrance; owner-local beta profile). The LP must not be able to move DLV reserves directly back into ordinary spendable owner balance merely by virtue of ownership. The vault birth state commits a release/withdraw/close policy PR. Any @@ -1242,6 +1253,10 @@ already-verified market history when the owner participates, but it does not imp time or maximum number of market advances for which the owner may remain absent. A terminal owner close under Requirement 6.30 is itself the final owner/DLV state update and does not require a separate catch-up step. +Status (amendment 2c-G, ruling G3). The catch-up of Requirement 4.5 is implemented; the fresh +baseline this requirement demands — an AnchorPresentationV3 over exactly the caught-up V_n, built +by the same owner-anchor machinery as the birth baseline — is not yet published. It is owed by the +third 2c-G change, after the admitted terminal close (G4). 7 Smart Commitments and Atomic Composition Definition 7.1 (Smart Commitment). A bounded deterministic predicate over committed inputs: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4f6b2335..f04313e9 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=19 + expected=20 found=$(ls lean4/*.lean | wc -l) if [ "$found" -ne "$expected" ]; then echo "::error::lean4/ has $found modules, expected $expected." diff --git a/docs/papers/ccb-object-registry.md b/docs/papers/ccb-object-registry.md index 44a6732c..990c0b21 100644 --- a/docs/papers/ccb-object-registry.md +++ b/docs/papers/ccb-object-registry.md @@ -1599,6 +1599,15 @@ storage-object address (amendment 2c-C1 ruling A). | 7 | `trader_economic_position` | `u64` | **the schema-2 field** — an untrusted locator | | 8 | `payment_evidence_addr` | `digest32` | | +**Producer (amendment 2c-G).** The owner's catch-up builds the `SettlementPaymentEvidenceV1` +bundle (transport proto, no CCB class) from the certified fold: the exact `0x0021` leaf and +256-sibling path the composition walk proved under the trader's validated `R_T^+` at the +acceptance's position (Req 21.16), carried on the fold and never fetched again. Fields 5–7 are the +walk's authenticated trader and that position. The producer mirrors the arm's leaf-equality and +inclusion checks before signing — the arm runs after the advance commits, where a refusal would +strand the admission — and the arm alone decides. `DlvOwnerApplyV2` is admission-fenced at the +core chokepoint: an owner apply is admitted with this arm or it does not advance. + **Two schema-2 arms, one reason.** Both carry a peer/owner `*_economic_position` that schema 1 did not, and both are labelled **untrusted locators**: they say where to start looking, never what is true. The verifier derives the position independently. That is the same locator-not-authority diff --git a/dsm_client/deterministic_state_machine/dsm/src/types/device_state.rs b/dsm_client/deterministic_state_machine/dsm/src/types/device_state.rs index 3bd7f1f0..1acd1b22 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/types/device_state.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/types/device_state.rs @@ -1843,15 +1843,26 @@ impl DeviceState { // raw operation and encumber reserves the economic lineage never saw, // leaving a head whose reserves `R_econ` cannot account for. // - // Deliberately NARROW. Settle, close and owner-apply are not fenced - // here: they consume or return an existing position rather than - // originating one, and their admission wiring is a separate cut with a - // separate evidence story. Widening this gate before those producers - // exist would strand the trader path with no replacement. + // Deliberately NARROW. Settle and close are not fenced here: they + // consume or return an existing position rather than originating one, + // and their admission wiring is a separate cut with a separate evidence + // story. Widening this gate before those producers exist would strand + // the trader path with no replacement. if matches!(operation, Operation::DlvCreateFundedV2 { .. }) { self.require_attached_dsm_admission(&operation, "a funded vault creation")?; } + // THE OWNER APPLY (amendment 2c-G). `DlvOwnerApplyV2` moves both vault + // reserve leaves a generation, so an unadmitted apply leaves a head + // whose reserves `R_econ` never saw — and every later admission that + // reads those leaves (the next apply, the close) builds against a root + // that disagrees with the head. Its producer now exists: the owner's + // catch-up admits every apply with its `0x0027` settlement-payment + // evidence, so the raw doorway closes here. + if matches!(operation, Operation::DlvOwnerApplyV2 { .. }) { + self.require_attached_dsm_admission(&operation, "an owner apply")?; + } + // THE SECOND ISSUANCE OPERATION. `CreateToken` carries an issuance leg, // and `validate_conservation` deliberately PERMITS it (the arm requires // exactly one credit of `initial_supply` under the new token's own @@ -6914,7 +6925,7 @@ mod tests { // A third asset on the input side: refused, nothing moves. let root_before = funded.root(); - let err = funded.advance( + let err = funded.advance_admitted( rk, funded.devid, apply_op(dbtc, rigb, out_amt), @@ -6945,7 +6956,7 @@ mod tests { // The real settlement: legs move AND the vault-state leaf follows. let out = funded - .advance( + .advance_admitted( rk, funded.devid, apply_op(era, rigb, out_amt), @@ -7227,7 +7238,7 @@ mod tests { signature: vec![], mode: TransactionMode::Unilateral, }); - let err = funded.advance( + let err = funded.advance_admitted( rk, funded.devid, op, @@ -7283,7 +7294,7 @@ mod tests { mode: TransactionMode::Unilateral, }); let out = funded - .advance( + .advance_admitted( rk, funded.devid, op, @@ -7311,6 +7322,112 @@ mod tests { assert_eq!(out.vault_reserve(&vault, &rigb), 5_000 - out_amt); } + /// THE OWNER APPLY IS ADMITTED OR IT DOES NOT HAPPEN (amendment 2c-G). + /// + /// The same matching, curve-priced v2 apply as the positive control above, + /// advanced RAW: no pending admission attached. It must be refused by the + /// fence's own precondition, with the reserves exactly where they were — + /// otherwise the head moves two reserve leaves `R_econ` never saw, and the + /// next admission that reads them builds against a root that disagrees + /// with the head. An admission bound to a DIFFERENT operation authorizes + /// nothing either. + /// + /// MUTATION CONTROL: delete the `DlvOwnerApplyV2` arm of the fence in + /// `advance` and the first assertion goes red by moving the reserves. + #[test] + fn an_owner_apply_is_refused_without_its_own_attached_admission() { + let (era, rigb) = (pc(0xE0), pc(0xF0)); + let (funded, vault, rk, tip) = funded_for_close(0xD7, era, rigb, 10_000, 5_000); + let funded = funded.with_pending_economic_admission(None); + let out_amt = crate::dlv::route_commit::constant_product_output(100, 10_000, 5_000, 30) + .expect("curve"); + let (parent_binding, parent_state) = parent_of(&funded, vault, vault_pair(era, rigb)); + let op = sign_op(Operation::DlvOwnerApplyV2 { + vault_id: vault.to_vec(), + settlement_receipt_id: [0x21; 32], + pending_pointer_x: [0x22; 32], + parent_sequence: 0, + new_sequence: 1, + parent_binding, + input_policy_commit: era, + output_policy_commit: rigb, + input_amount: 100, + output_amount: out_amt, + fee_bps: 30, + signature: vec![], + mode: TransactionMode::Unilateral, + }); + let mutation = || VaultReserveMutation::ApplySettlement { + vault_id: vault, + input_policy_commit: era, + input_amount: 100, + output_policy_commit: rigb, + output_amount: out_amt, + parent_sequence: 0, + new_sequence: 1, + pair: vault_pair(era, rigb), + parent_state: parent_state.clone(), + }; + let root_before = funded.root(); + + // (1) No admission attached at all. + let err = format!( + "{}", + funded + .advance( + rk, + funded.devid, + op.clone(), + entropy(2), + None, + &[], + Some(tip), + None, + None, + Some(mutation()), + ) + .expect_err("a raw owner apply must not move the reserves") + ); + assert!( + err.contains("no pending economic admission"), + "the refusal is the fence's own, got: {err}" + ); + + // (2) An admission attached, but bound to a DIFFERENT operation. + let staged = funded.with_pending_economic_admission(Some( + crate::economic::admission::PendingEconomicAdmission::prepared( + crate::economic::admission::PendingAdmissionKind::DsmBacked, + 1, + [0u8; 32], + crate::economic::faucet::dsm_operation_digest(&Operation::Noop.to_bytes()), + ), + )); + let err = format!( + "{}", + staged + .advance( + rk, + staged.devid, + op, + entropy(2), + None, + &[], + Some(tip), + None, + None, + Some(mutation()), + ) + .expect_err("an admission for another operation authorizes nothing") + ); + assert!( + err.contains("does not match the pending economic admission"), + "the refusal names the digest mismatch, got: {err}" + ); + assert_eq!(funded.root(), root_before, "nothing moved"); + assert_eq!(funded.vault_reserve(&vault, &era), 10_000); + assert_eq!(funded.vault_reserve(&vault, &rigb), 5_000); + } + /// The head's OWN parent state for `vault` under `pair`: its commitment /// (what the owner signs as `parent_binding`) and its bytes (what the /// mutation carries). Exactly what `dlv.reconcile` derives from the @@ -7375,7 +7492,7 @@ mod tests { op: Operation, mutation: VaultReserveMutation, ) -> Result { - head.advance( + head.advance_admitted( rk, head.devid, op, @@ -7728,7 +7845,7 @@ mod tests { mode: TransactionMode::Bilateral, }); let traded = funded - .advance( + .advance_admitted( rk, funded.devid, apply, 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 94b67753..2a4319c2 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 @@ -1670,32 +1670,23 @@ impl AppRouterImpl { pack_envelope_ok(generated::envelope::Payload::AppStateResponse(resp)) } - /// dlv.unlockRouted — atomic-route unlock path for SoFi (chunk #4). - /// - /// Decodes a `DlvUnlockRoutedV1` carrying a typed `RouteCommitV1`, - /// runs the SDK eligibility check (vault_id ∈ RouteCommit AND - /// `is_external_commitment_visible(X)` returns Ok(true)) before - /// emitting the standard `Operation::DlvUnlock` on the unlocker's - /// self-loop. No new on-chain operation type — atomicity is - /// achieved off-chain via the visibility of X (SoFi spec §3.2, - /// §5.1; the state machine does not know about routing). - /// - /// Failure modes are typed via `RouteCommitVerifyError` so a - /// failed verification returns a precise error (rather than a - /// generic `dlv.unlock failed`) — this is what unlocks - /// fail-closed semantics for vault owners that haven't yet seen - /// the trader's anchor publish. - /// `dlv.reconcile` — the OWNER folds a verified settlement into its reserves. + /// `dlv.reconcile` — the OWNER's explicit catch-up (amendment 2c-G, ruling + /// G2). /// - /// The trader's credit was final at the trader's own advance. This is the - /// owner learning what already happened, so it AUTHORIZES nothing: every - /// value acted on is re-derived from the receipt fetched under `(vault, x)` - /// The request says only which settlement to look at; the trade applied - /// is the one the composition walk CERTIFIED (2c-D §14, C2-R1 point 6). + /// The trader's credit was final at the trader's own advance and the + /// composition walk certified it, so this is the owner learning what already + /// happened: it AUTHORIZES nothing. The request names one settlement `x`; + /// the owner applies every certified settlement it has not yet applied, + /// oldest first, up to and including that one — through the SAME engine the + /// `storage.sync` pass runs to the frontier. A fold consumes exactly the + /// current parent, so a later settlement is never applied over a state that + /// has not received the earlier ones. Every trade fact comes from the + /// certified fold (2c-D §14, C2-R1 point 6), never from a receipt read on + /// the side, and every apply is admitted into `R_econ`. /// - /// Idempotent. Folding the same receipt twice would move the reserves twice - /// on a trade that happened once, so a receipt whose sequence step the vault - /// has already taken applies nothing and reports success. + /// Idempotent. A settlement already applied is recognised by its + /// consume-once claim and applies nothing; a request with nothing owed + /// writes nothing. async fn dlv_reconcile(&self, i: AppInvoke) -> AppResult { let bytes = match unwrap_argpack(&i.args) { Ok(b) => b, @@ -1711,276 +1702,27 @@ impl AppRouterImpl { ) else { return err("dlv.reconcile: vault_id and x must both be 32 bytes".into()); }; - - // THE CERTIFIED FOLD IS THE AUTHORITY (2c-D §14, C2-R1 point 6). A - // receipt is Req 21.16's evidence inside the composition walk and never - // settlement: this route acts only on the exact fold the walk certified - // for this commitment and takes every trade fact from it. An owner - // apply therefore cannot invent or modify economics — it can only apply - // what was certified. let vault_b32 = crate::util::text_id::encode_base32_crockford(&vault_id); - - // Precondition: a reconcile needs a device head to advance. - if self.core_sdk.device_head().is_none() { - return err("dlv.reconcile: no device head".into()); - } - let composed = match compose_own_vault(&vault_id).await { - Ok(c) => c, - Err(e) => { - return err(format!( - "dlv.reconcile: cannot compose the vault to find its certified settlement: {e}" - )) - } - }; - // 2c-C3.1 ruling D, effect 4: independent of the walk. - if let Err(e) = - refuse_quarantined_lineage("dlv.reconcile", &vault_id, composed.sequence, &composed.c_n) - { - return err(e); - } - let Some((fold, certified)) = - composed - .folded_parents - .iter() - .find_map(|f| match (&f.bound_kind, &f.realized_trade) { - (dsm::dlv::settlement_bundle::BundleShape::Market, Some(t)) - if f.verdict.may_certify() && t.trade().x == x => - { - Some((f, t)) - } - _ => None, - }) - else { - return err(format!( - "dlv.reconcile: vault {vault_b32} has no CERTIFIED settlement at that commitment — \ - a receipt is evidence, never settlement (2c-D §14, C2-R1)" - )); - }; - let receipt_id = certified.receipt_id(); - let trade = certified.trade(); - - // CONSUME-ONCE, by settlement IDENTITY — not by sequence alone. The - // reserve leaf carries the generation but not WHICH settlement produced - // it, so a sequence-only check cannot tell the winner's idempotent - // replay from a DIFFERENT settlement that raced the same parent. The - // durable consume-once claim can tell them apart. - match crate::storage::client_db::load_vault_generation_consumer( - &vault_id, - trade.parent_sequence, - ) { - Ok(Some(existing)) => { - if existing.source_commitment == receipt_id { - // The SAME settlement, already applied: idempotent success. - return pack_envelope_ok(generated::envelope::Payload::AppStateResponse( - generated::AppStateResponse { - key: "dlv.reconcile".to_string(), - value: Some(crate::util::text_id::encode_base32_crockford(&vault_id)), - }, - )); - } - return err(format!( - "dlv.reconcile: vault {vault_b32} generation {} was already consumed by a \ - different settlement — this settlement cannot consume it", - trade.parent_sequence, - )); - } - Ok(None) => {} - Err(e) => return err(format!("dlv.reconcile: consumption lookup failed: {e}")), - } - - // THE PARENT STATE is the certified fold's own: the state the walk - // consumed at this generation — never a local record, never a receipt. - let parent_state: dsm::ccb::VaultStateV2 = fold.state.clone(); - let parent_binding = match dsm::ccb::vault_state_commitment(&parent_state) { - Ok(c) => c, - Err(e) => { - return err(format!( - "dlv.reconcile: the parent state does not commit: {e}" - )) - } - }; - let parent_state_bytes = match parent_state.encode() { - Ok(b) => b, - Err(e) => { - return err(format!( - "dlv.reconcile: the parent state does not encode: {e}" - )) - } - }; - let fee_bps = parent_state.fee_policy.fee_bps(); - let pair = match dsm::types::device_state::VaultStatePair::new( - *parent_state.market_policy.token_a(), - *parent_state.market_policy.token_b(), - fee_bps, - ) { - Ok(p) => p, - Err(e) => { - return err(format!( - "dlv.reconcile: the parent state's pair is not canonical: {e}" - )) - } - }; - - // THE PRE-SIGN MIRROR of the core check — an early refusal, not an - // authority: `advance` re-derives every one of these facts from the - // leaves it consumes and would refuse the same fold after signing. - // Refusing HERE keeps the owner from ever signing arithmetic it has not - // checked. A certified fold already satisfies it — CORR.5 derived this - // output — so only a defect upstream of the walk could reach it. Same inputs as core, in the same order: the parent state's - // committed pair and fee, the reserve of the asset the trader paid as - // the input reserve (by asset identity, never by pair order), the one - // canonical curve, exact equality. - let (reserve_in, reserve_out) = if trade.input_policy_commit == pair.a() - && trade.output_policy_commit == pair.b() - { - (parent_state.reserve_a, parent_state.reserve_b) - } else if trade.input_policy_commit == pair.b() && trade.output_policy_commit == pair.a() { - (parent_state.reserve_b, parent_state.reserve_a) - } else { - return err( - "dlv.reconcile: the receipt's legs are not this vault's pair — refusing before \ - signing" - .into(), - ); - }; - match crate::sdk::routing_path_sdk::constant_product_output( - trade.input_amount, - reserve_in, - reserve_out, - fee_bps, - ) { - Some(curve) if curve == trade.output_amount => {} - Some(curve) => { - return err(format!( - "dlv.reconcile: the receipt's output is not what this vault's curve yields \ - from the parent state's reserves (curve {curve}, receipt {}) — refusing \ - before signing", - trade.output_amount, - )) - } - None => { - return err( - "dlv.reconcile: the receipt's trade does not simulate against the parent \ - state's reserves — refusing before signing" - .into(), - ) - } - } - let op = dsm::types::operations::Operation::DlvOwnerApplyV2 { - vault_id: vault_id.to_vec(), - settlement_receipt_id: receipt_id, - pending_pointer_x: x, - parent_sequence: trade.parent_sequence, - new_sequence: trade.new_sequence, - parent_binding, - input_policy_commit: trade.input_policy_commit, - output_policy_commit: trade.output_policy_commit, - input_amount: trade.input_amount, - output_amount: trade.output_amount, - // The parent state's committed fee — the same one the curve above ran on. - fee_bps, - signature: Vec::new(), - mode: dsm::types::operations::TransactionMode::Unilateral, - }; - - // Sign BEFORE the advance, for the same reason as `DlvSettle`: the signature is - // inside the committed operation bytes and therefore inside the chain tip. - let op = match self.core_sdk.sign_operation_sphincs(op) { - Ok(signed) => signed, - Err(e) => { - return err(format!( - "dlv.reconcile: failed to sign DlvOwnerApplyV2: {e}" - )) - } - }; - // The fold moves reserve value under both pair assets; each must - // satisfy the applicable token policy before the apply is derived. - for pc in [pair.a(), pair.b()] { - if let Err(e) = require_rooted_market_leg("dlv.reconcile", &pc).await { - return err(e); - } - } - - let mutation = dsm::types::device_state::VaultReserveMutation::ApplySettlement { - vault_id, - input_policy_commit: trade.input_policy_commit, - input_amount: trade.input_amount, - output_policy_commit: trade.output_policy_commit, - output_amount: trade.output_amount, - parent_sequence: trade.parent_sequence, - new_sequence: trade.new_sequence, - pair, - parent_state: parent_state_bytes, - }; - - let reference_state = match self.core_sdk.get_current_state() { - Ok(s) => s, - Err(e) => return err(format!("dlv.reconcile: get_current_state failed: {e}")), - }; - let actor = reference_state.device_info.device_id; - let rel_key = dsm::core::bilateral_transaction_manager::compute_smt_key(&actor, &actor); - let init_tip = dsm::core::bilateral_transaction_manager::initial_chain_tip_from_device_ids( - &actor, &actor, - ); - // The consume-once claim is written INSIDE the fold's advance - // transaction, so the claim and the reserve move commit together or not at - // all. `UNIQUE(vault_id, parent_sequence)` decides a race that slipped past - // the pre-check above: a losing racer's claim resolves to `Conflict`, which - // this closure turns into an error, rolling back the whole advance so the - // loser moves no reserve. - let claim_vault = vault_id; - let claim_parent = trade.parent_sequence; - let claim_child = trade.new_sequence; - let claim_source = receipt_id; - let record_consumption = move |tx: &rusqlite::Transaction<'_>, - _outcome: &dsm::types::device_state::AdvanceOutcome| - -> Result<(), dsm::types::error::DsmError> { - use crate::storage::client_db::{ - cas_consume_vault_generation_with_conn, VaultGenerationConsumeOutcome, - }; - match cas_consume_vault_generation_with_conn( - tx, - &claim_vault, - claim_parent, - claim_child, - &claim_source, - ) - .map_err(|e| { - dsm::types::error::DsmError::storage( - format!("dlv.reconcile: consume-once claim failed: {e}"), - None::, - ) - })? { - VaultGenerationConsumeOutcome::Consumed - | VaultGenerationConsumeOutcome::AlreadyConsumedSameSettlement => Ok(()), - VaultGenerationConsumeOutcome::Conflict { .. } => { - Err(dsm::types::error::DsmError::invalid_operation( - "dlv.reconcile: this vault generation was consumed by a different \ - settlement (race) — rolling back the fold", - )) - } - } - }; - // EMPTY deltas: the owner's spendable balance is not part of a - // settlement. Only the reserve leaves move, in this same advance. - if let Err(e) = self.core_sdk.execute_on_relationship_with_reserve_mutation( - rel_key, - actor, - op, - &[], - Some(init_tip), - Some(mutation), - Some(&record_consumption), - ) { - return err(format!("dlv.reconcile: advance failed: {e}")); + // The explicit request WAITS for a running sync pass rather than racing + // it; the sync pass skips while this runs. + let _one_at_a_time = owner_catch_up_lock().lock().await; + let report = self + .catch_up_owner_vault_locked(&vault_id, CatchUpTarget::Through(x)) + .await; + match report.stopped { + None => pack_envelope_ok(generated::envelope::Payload::AppStateResponse( + generated::AppStateResponse { + key: "dlv.reconcile".to_string(), + value: Some(vault_b32), + }, + )), + // The applies that landed before the stop stay durable; the next + // request resumes after them. + Some(e) => err(format!( + "dlv.reconcile: vault {vault_b32}: {} applied, then stopped: {e}", + report.applied + )), } - - pack_envelope_ok(generated::envelope::Payload::AppStateResponse( - generated::AppStateResponse { - key: "dlv.reconcile".to_string(), - value: Some(crate::util::text_id::encode_base32_crockford(&vault_id)), - }, - )) } /// Commit the canonical close: ONE staged advance in which the release, the @@ -2961,6 +2703,21 @@ impl AppRouterImpl { )) } + /// dlv.unlockRouted — atomic-route unlock path for SoFi (chunk #4). + /// + /// Decodes a `DlvUnlockRoutedV1` carrying a typed `RouteCommitV1`, + /// runs the SDK eligibility check (vault_id ∈ RouteCommit AND + /// `is_external_commitment_visible(X)` returns Ok(true)) before + /// emitting the standard `Operation::DlvUnlock` on the unlocker's + /// self-loop. No new on-chain operation type — atomicity is + /// achieved off-chain via the visibility of X (SoFi spec §3.2, + /// §5.1; the state machine does not know about routing). + /// + /// Failure modes are typed via `RouteCommitVerifyError` so a + /// failed verification returns a precise error (rather than a + /// generic `dlv.unlock failed`) — this is what unlocks + /// fail-closed semantics for vault owners that haven't yet seen + /// the trader's anchor publish. async fn dlv_unlock_routed(&self, i: AppInvoke) -> AppResult { let bytes = match unwrap_argpack(&i.args) { Ok(b) => b, @@ -4264,25 +4021,442 @@ impl AppRouterImpl { log::warn!("[settlement resume] {b32}: refused, fence held — {why}") } } - } - Ok(realized) + } + Ok(realized) + } + + /// 2c-F's recovery pass: every settlement of THIS device whose fence is + /// released but whose Def 14.2 receipt obligation was never recorded — + /// its closure freeze failed and did not hold the fence (R6) — rebuilt + /// from durable facts and frozen. Returns how many were frozen. + /// + /// Needs no signing authority and re-decides nothing: the released fence + /// is the durable record that certification happened, and the pass never + /// composes, binds, advances, admits or touches a fence. + pub(crate) async fn resume_receipt_publications(&self) -> Result { + let Some(head) = self.core_sdk.device_head() else { + return Ok(0); + }; + let chain = + dsm::core::bilateral_transaction_manager::compute_smt_key(&head.devid(), &head.devid()); + crate::sdk::sofi_receipt_publication::recover_owed_receipts(&chain).await + } + + /// Amendment 2c-G's catch-up pass, run by `storage.sync` (ruling G2): for + /// every vault THIS device owns, every certified settlement it has not + /// applied, oldest first, to the composed frontier. Returns how many applies + /// it admitted. + /// + /// It GATES NOTHING. It runs after every other sync pass, a failure is local + /// to its vault and retried on a later sync, and nothing a trader, a + /// binding, a fence or a close does waits for it. It never calls + /// `storage.sync`, and it skips outright while another catch-up holds the + /// device's catch-up lock, so it cannot re-enter itself. + pub(crate) async fn resume_owner_catch_up(&self) -> Result { + let Some(head) = self.core_sdk.device_head() else { + return Ok(0); + }; + // A locked wallet cannot sign an apply: leave every vault as it is. + if !crate::sdk::signing_authority::can_sign() { + return Ok(0); + } + let Ok(_one_at_a_time) = owner_catch_up_lock().try_lock() else { + log::info!("[owner catch-up] a catch-up is already running; this pass skips"); + return Ok(0); + }; + let records = crate::storage::client_db::amm_vault_records::list_amm_vault_records() + .map_err(|e| format!("reading vault records failed: {e}"))?; + let mut applied = 0u32; + for rec in &records { + // Only a vault this device owns is this device's to apply. + if crate::sdk::vault_rehydration::rehydrate_amm_vault(rec, &head).is_err() { + continue; + } + let b32 = crate::util::text_id::encode_base32_crockford(&rec.vault_id); + let report = self + .catch_up_owner_vault_locked(&rec.vault_id, CatchUpTarget::Frontier) + .await; + // Counted whether or not the run finished: each is durable. + applied += report.applied; + match &report.stopped { + Some(why) => log::warn!( + "[owner catch-up] vault {b32}: {} applied, then not caught up this pass — \ + {why}", + report.applied + ), + None if report.applied > 0 => log::info!( + "[owner catch-up] vault {b32}: {} applied, {} already applied", + report.applied, + report.already_applied + ), + None => {} + } + } + Ok(applied) + } + + /// THE catch-up engine (amendment 2c-G, rulings G1 + G2) — the one both + /// entrypoints drive. The caller holds [`owner_catch_up_lock`]. + /// + /// Consumes certified history and creates none: it composes the vault + /// through the same walk a stranger runs, takes the certified market folds + /// that walk produced, and applies the owed ones oldest first. A fold + /// already applied is recognised by its consume-once claim; a generation + /// consumed by a DIFFERENT settlement stops the catch-up. An interruption + /// leaves every completed apply durable, and the next run resumes after it. + /// + /// The report is returned whether or not the run finished: `applied` + /// counts every apply that landed, and `stopped` says why a run ended + /// early. A stop never hides an apply that is already durable. + async fn catch_up_owner_vault_locked( + &self, + vault_id: &[u8; 32], + target: CatchUpTarget, + ) -> CatchUpReport { + let mut report = CatchUpReport::default(); + if let Err(why) = self.catch_up_into(vault_id, target, &mut report).await { + report.stopped = Some(why); + } + report + } + + /// The engine's body. Progress is recorded in `report` as each apply + /// lands, so an error returned from here stops the run without erasing it. + async fn catch_up_into( + &self, + vault_id: &[u8; 32], + target: CatchUpTarget, + report: &mut CatchUpReport, + ) -> Result<(), String> { + if self.core_sdk.device_head().is_none() { + return Err("no device head".into()); + } + let composed = compose_own_vault(vault_id).await.map_err(|e| { + format!("cannot compose the vault to find its certified settlements: {e}") + })?; + // 2c-C3.1 ruling D, effect 4: independent of the walk. + refuse_quarantined_lineage("owner catch-up", vault_id, composed.sequence, &composed.c_n)?; + for fold in owed_certified_folds(&composed, target)? { + let Some(certified) = fold.realized_trade.as_ref() else { + continue; + }; + let trade = certified.trade(); + // CONSUME-ONCE, by settlement IDENTITY — not by sequence alone. The + // reserve leaf carries the generation but not WHICH settlement + // produced it; the durable claim tells a replay from a race. + match crate::storage::client_db::load_vault_generation_consumer( + vault_id, + trade.parent_sequence, + ) { + Ok(Some(existing)) if existing.source_commitment == certified.receipt_id() => { + report.already_applied += 1; + continue; + } + Ok(Some(_)) => { + return Err(format!( + "generation {} was already consumed by a different settlement — this \ + settlement cannot consume it", + trade.parent_sequence + )) + } + Ok(None) => {} + Err(e) => return Err(format!("consumption lookup failed: {e}")), + } + #[cfg(test)] + take_catch_up_apply_budget()?; + self.apply_certified_fold(vault_id, fold).await?; + report.applied += 1; + } + Ok(()) + } + + /// Apply ONE certified fold: the owner's `DlvOwnerApplyV2`, admitted with + /// its `0x0027` evidence, the consume-once claim written inside the same + /// advance. + /// + /// THE CERTIFIED FOLD IS THE AUTHORITY (2c-D §14, C2-R1 point 6): the + /// parent state is the state the walk consumed at this generation, every + /// trade fact is the one it certified, and the evidence is the payment it + /// proved. An apply therefore cannot invent or modify economics — it can + /// only materialize what was certified. + async fn apply_certified_fold( + &self, + vault_id: &[u8; 32], + fold: &crate::sdk::vault_state_composition::FoldedParent, + ) -> Result<(), String> { + let (Some(certified), Some(payment)) = ( + fold.realized_trade.as_ref(), + fold.certified_payment.as_ref(), + ) else { + return Err("the fold carries no certified settlement".into()); + }; + let vault_id = *vault_id; + let receipt_id = certified.receipt_id(); + let trade = certified.trade(); + + // THE 0x0027 EVIDENCE, first: projected from the payment certification + // proved, so a fold whose evidence the arm would refuse is refused + // before anything is signed. + let payment_evidence = + crate::sdk::settlement_payment_producer::build_settlement_payment_evidence( + certified, payment, + ) + .map_err(|e| e.to_string())?; + + // THE PARENT STATE is the certified fold's own: the state the walk + // consumed at this generation — never a local record, never a receipt. + let parent_state: dsm::ccb::VaultStateV2 = fold.state.clone(); + let parent_binding = dsm::ccb::vault_state_commitment(&parent_state) + .map_err(|e| format!("the parent state does not commit: {e}"))?; + let parent_state_bytes = parent_state + .encode() + .map_err(|e| format!("the parent state does not encode: {e}"))?; + let fee_bps = parent_state.fee_policy.fee_bps(); + let pair = dsm::types::device_state::VaultStatePair::new( + *parent_state.market_policy.token_a(), + *parent_state.market_policy.token_b(), + fee_bps, + ) + .map_err(|e| format!("the parent state's pair is not canonical: {e}"))?; + + // THE PRE-SIGN MIRROR of the core check — an early refusal, not an + // authority: `advance` re-derives every one of these facts from the + // leaves it consumes and would refuse the same fold after signing. + // Refusing HERE keeps the owner from ever signing arithmetic it has not + // checked. A certified fold already satisfies it — CORR.5 derived this + // output — so only a defect upstream of the walk could reach it. Same + // inputs as core, in the same order: the parent state's committed pair + // and fee, the reserve of the asset the trader paid as the input + // reserve (by asset identity, never by pair order), the one canonical + // curve, exact equality. + let (reserve_in, reserve_out) = if trade.input_policy_commit == pair.a() + && trade.output_policy_commit == pair.b() + { + (parent_state.reserve_a, parent_state.reserve_b) + } else if trade.input_policy_commit == pair.b() && trade.output_policy_commit == pair.a() { + (parent_state.reserve_b, parent_state.reserve_a) + } else { + return Err( + "the certified trade's legs are not this vault's pair — refusing before signing" + .into(), + ); + }; + match crate::sdk::routing_path_sdk::constant_product_output( + trade.input_amount, + reserve_in, + reserve_out, + fee_bps, + ) { + Some(curve) if curve == trade.output_amount => {} + Some(curve) => { + return Err(format!( + "the certified output is not what this vault's curve yields from the parent \ + state's reserves (curve {curve}, certified {}) — refusing before signing", + trade.output_amount, + )) + } + None => { + return Err( + "the certified trade does not simulate against the parent state's reserves \ + — refusing before signing" + .into(), + ) + } + } + let op = dsm::types::operations::Operation::DlvOwnerApplyV2 { + vault_id: vault_id.to_vec(), + settlement_receipt_id: receipt_id, + pending_pointer_x: trade.x, + parent_sequence: trade.parent_sequence, + new_sequence: trade.new_sequence, + parent_binding, + input_policy_commit: trade.input_policy_commit, + output_policy_commit: trade.output_policy_commit, + input_amount: trade.input_amount, + output_amount: trade.output_amount, + // The parent state's committed fee — the same one the curve above ran on. + fee_bps, + signature: Vec::new(), + mode: dsm::types::operations::TransactionMode::Unilateral, + }; + + // Sign BEFORE the advance, for the same reason as `DlvSettle`: the + // signature is inside the committed operation bytes and therefore + // inside the chain tip. + let op = self + .core_sdk + .sign_operation_sphincs(op) + .map_err(|e| format!("failed to sign DlvOwnerApplyV2: {e}"))?; + // The fold moves reserve value under both pair assets; each must + // satisfy the applicable token policy before the apply is derived. + for pc in [pair.a(), pair.b()] { + require_rooted_market_leg("owner catch-up", &pc).await?; + } + + let mutation = dsm::types::device_state::VaultReserveMutation::ApplySettlement { + vault_id, + input_policy_commit: trade.input_policy_commit, + input_amount: trade.input_amount, + output_policy_commit: trade.output_policy_commit, + output_amount: trade.output_amount, + parent_sequence: trade.parent_sequence, + new_sequence: trade.new_sequence, + pair, + parent_state: parent_state_bytes, + }; + + let reference_state = self + .core_sdk + .get_current_state() + .map_err(|e| format!("get_current_state failed: {e}"))?; + let actor = reference_state.device_info.device_id; + let rel_key = dsm::core::bilateral_transaction_manager::compute_smt_key(&actor, &actor); + let init_tip = dsm::core::bilateral_transaction_manager::initial_chain_tip_from_device_ids( + &actor, &actor, + ); + // The consume-once claim is written INSIDE the apply's advance + // transaction, so the claim and the reserve move commit together or + // not at all. `UNIQUE(vault_id, parent_sequence)` decides a race that + // slipped past the engine's pre-check: a losing racer's claim resolves + // to `Conflict`, which this closure turns into an error, rolling back + // the whole advance so the loser moves no reserve. + let (claim_parent, claim_child) = (trade.parent_sequence, trade.new_sequence); + let record_consumption = move |tx: &rusqlite::Transaction<'_>, + _outcome: &dsm::types::device_state::AdvanceOutcome, + _artifacts: &()| + -> Result<(), dsm::types::error::DsmError> { + use crate::storage::client_db::{ + cas_consume_vault_generation_with_conn, VaultGenerationConsumeOutcome, + }; + match cas_consume_vault_generation_with_conn( + tx, + &vault_id, + claim_parent, + claim_child, + &receipt_id, + ) + .map_err(|e| { + dsm::types::error::DsmError::storage( + format!("owner catch-up: consume-once claim failed: {e}"), + None::, + ) + })? { + VaultGenerationConsumeOutcome::Consumed + | VaultGenerationConsumeOutcome::AlreadyConsumedSameSettlement => Ok(()), + VaultGenerationConsumeOutcome::Conflict { .. } => { + Err(dsm::types::error::DsmError::invalid_operation( + "owner catch-up: this vault generation was consumed by a different \ + settlement (race) — rolling back the apply", + )) + } + } + }; + // EMPTY deltas inside the facade: the owner's spendable balance is not + // part of a settlement. Only the reserve leaves move, in this advance. + crate::sdk::economic_admission_flow::admitted_dlv_owner_apply( + &self.core_sdk, + op, + rel_key, + actor, + init_tip, + mutation, + payment.trader_genesis, + payment.trader_devid, + payment.trader_economic_position, + payment_evidence, + |_outcome: &dsm::types::device_state::AdvanceOutcome| Ok(()), + record_consumption, + ) + .await + .map(|_| ()) + .map_err(|e| format!("the admitted apply failed: {e}")) } +} - /// 2c-F's recovery pass: every settlement of THIS device whose fence is - /// released but whose Def 14.2 receipt obligation was never recorded — - /// its closure freeze failed and did not hold the fence (R6) — rebuilt - /// from durable facts and frozen. Returns how many were frozen. - /// - /// Needs no signing authority and re-decides nothing: the released fence - /// is the durable record that certification happened, and the pass never - /// composes, binds, advances, admits or touches a fence. - pub(crate) async fn resume_receipt_publications(&self) -> Result { - let Some(head) = self.core_sdk.device_head() else { - return Ok(0); +/// Where an owner catch-up stops (amendment 2c-G, ruling G2). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum CatchUpTarget { + /// Every certified settlement the owner has not applied: the composed + /// frontier. What the `storage.sync` pass asks for. + Frontier, + /// The owed prefix that ends at the settlement committed as `x`. What + /// `dlv.reconcile` asks for. + Through([u8; 32]), +} + +/// What one catch-up did to one vault. Every apply counted is durable, whether +/// or not the run finished. +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub(crate) struct CatchUpReport { + pub applied: u32, + pub already_applied: u32, + /// Why the run ended before its target, if it did. + pub stopped: Option, +} + +/// ONE catch-up at a time on this device: an explicit request waits for a +/// running sync pass, and a sync pass skips while any catch-up runs. +fn owner_catch_up_lock() -> &'static tokio::sync::Mutex<()> { + static LOCK: std::sync::OnceLock> = std::sync::OnceLock::new(); + LOCK.get_or_init(|| tokio::sync::Mutex::new(())) +} + +/// The certified settlements a catch-up to `target` consumes, oldest first. +/// +/// A pure function of the composition, which is what makes the two +/// entrypoints agree: `Through(x)` is exactly the prefix of `Frontier` that +/// ends at `x`. Only a certified MARKET fold counts — the walk installs +/// nothing uncertified, and a close is the owner's own terminal act rather +/// than a settlement to apply. +fn owed_certified_folds( + composed: &crate::sdk::vault_state_composition::ComposedVaultState, + target: CatchUpTarget, +) -> Result, String> { + let mut owed: Vec<_> = composed + .folded_parents + .iter() + .filter(|f| { + matches!( + f.bound_kind, + dsm::dlv::settlement_bundle::BundleShape::Market + ) && f.verdict.may_certify() + && f.realized_trade.is_some() + }) + .collect(); + // A fold consumes exactly the current parent: generation order is the only + // order in which the applies can land. + owed.sort_by_key(|f| f.generation); + if let CatchUpTarget::Through(x) = target { + let Some(end) = owed + .iter() + .position(|f| f.realized_trade.as_ref().is_some_and(|t| t.trade().x == x)) + else { + return Err( + "no CERTIFIED settlement at that commitment — a receipt is evidence, never \ + settlement (2c-D §14, C2-R1)" + .into(), + ); }; - let chain = - dsm::core::bilateral_transaction_manager::compute_smt_key(&head.devid(), &head.devid()); - crate::sdk::sofi_receipt_publication::recover_owed_receipts(&chain).await + owed.truncate(end + 1); + } + Ok(owed) +} + +/// TEST-ONLY: how many applies a catch-up may still make before the next is +/// refused as an interruption between applies. Negative means unlimited. +#[cfg(test)] +static CATCH_UP_APPLY_BUDGET: std::sync::atomic::AtomicI64 = std::sync::atomic::AtomicI64::new(-1); + +#[cfg(test)] +fn take_catch_up_apply_budget() -> Result<(), String> { + use std::sync::atomic::Ordering; + match CATCH_UP_APPLY_BUDGET.load(Ordering::SeqCst) { + 0 => Err("interrupted between applies (test injection)".into()), + n if n > 0 => { + CATCH_UP_APPLY_BUDGET.store(n - 1, Ordering::SeqCst); + Ok(()) + } + _ => Ok(()), } } @@ -7097,6 +7271,20 @@ mod funded_creation_tests { !reconcile(r, &vault_id, &x_b).success, "the loser's replay stays refused" ); + // And the storage.sync pass finds nothing owed: a receipt with no + // certified fold behind it is not a settlement to catch up on. + assert_eq!( + crate::runtime::get_runtime() + .block_on(r.resume_owner_catch_up()) + .expect("the sync pass"), + 0, + "nothing uncertified is ever owed" + ); + assert_eq!( + r.core_sdk.device_head().expect("head").root(), + root_before, + "and the pass wrote nothing" + ); } /// What the vault created by these tests pays for 1 000 of A at birth: @@ -10351,7 +10539,7 @@ mod funded_creation_tests { /// the probes go through the same route. #[test] #[serial] - fn lp_offline_market_advances_three_generations_and_lp_reconciles_each_once() { + fn lp_offline_market_advances_three_generations_and_lp_catches_up_oldest_first() { use prost::Message as _; install_identity(); @@ -10602,49 +10790,45 @@ mod funded_creation_tests { 0 ); - // Folding out of order is REFUSED: generation 1 is not current. + // An explicit catch-up THROUGH generation 1 applies generation 0 first: + // a fold consumes exactly the current parent, so generation 1 is never + // applied over a state that has not received generation 0 (2c-G, G2). let res = reconcile(owner, &vault_id, &xs[1]); assert!( - !res.success, - "folding generation 1->2 before 0->1 must be refused (parent not current)" - ); - let h = owner.core_sdk.device_head().expect("owner head"); - assert_eq!( - h.vault_reserve(&vault_id, &pc_a), - 10_000, - "a refused fold moved nothing" + res.success, + "catch-up through generation 1: {:?}", + res.error_message ); - - // In order, each fold consumes exactly the next parent, once. let mut expect = (10_000u64, 5_000u64); - for (i, &input) in inputs.iter().enumerate() { + for &input in &inputs[..2] { let out = cp(input, expect.0, expect.1); - let res = reconcile(owner, &vault_id, &xs[i]); - assert!(res.success, "fold {i} failed: {:?}", res.error_message); expect = (expect.0 + input, expect.1 - out); - let h = owner.core_sdk.device_head().expect("owner head"); - assert_eq!( - ( - h.vault_reserve(&vault_id, &pc_a), - h.vault_reserve(&vault_id, &pc_b) - ), - expect, - "after fold {i} the reserves reflect exactly generations 0..={i}" - ); - assert_eq!( - h.vault_reserve_entry(&vault_id, &pc_a) - .expect("leg") - .sequence, - i as u64 + 1, - "each fold advances the generation by exactly one" - ); + } + assert_eq!( + leaves(owner, &vault_id, &pc_a, &pc_b), + (expect.0, expect.1, 2), + "generations 0 and 1 applied, in order, and nothing past the named settlement" + ); + + // The storage.sync pass finishes what is still owed, and only that. + let n = crate::runtime::get_runtime() + .block_on(owner.resume_owner_catch_up()) + .expect("the sync pass"); + assert_eq!(n, 1, "only generation 2 was still owed"); + let out = cp(inputs[2], expect.0, expect.1); + expect = (expect.0 + inputs[2], expect.1 - out); + assert_eq!( + leaves(owner, &vault_id, &pc_a, &pc_b), + (expect.0, expect.1, 3) + ); + for (i, x) in xs.iter().enumerate() { let consumer = crate::storage::client_db::load_vault_generation_consumer(&vault_id, i as u64) .expect("load") .expect("generation consumed"); assert_eq!( consumer.source_commitment, - dsm::dlv::settlement_receipt_leaf::derive_receipt_id(&vault_id, &xs[i]), + dsm::dlv::settlement_receipt_leaf::derive_receipt_id(&vault_id, x), "generation {i} is recorded as consumed by trader {i}'s settlement" ); } @@ -10668,6 +10852,374 @@ mod funded_creation_tests { assert!(res.success, "replaying the last fold must not error"); assert_eq!(owner.core_sdk.device_head().expect("head").root(), root); } + /// The market moves the vault while its owner is away: trader `i` settles + /// `inputs[i]` of A against the reserves the COMPOSED state holds at + /// generation `i`. Returns each settlement's commitment `x`, oldest first. + fn market_moves( + vault_id: &[u8; 32], + pc_a: &[u8; 32], + pc_b: &[u8; 32], + traders: &[crate::test_support::two_device::TestDevice], + inputs: &[u64], + ) -> Vec<[u8; 32]> { + let mut xs = Vec::new(); + for (i, (t, &input)) in traders.iter().zip(inputs).enumerate() { + t.enter(); + let (gen, ra, rb) = composed(vault_id, pc_a, pc_b); + assert_eq!(gen, i as u64, "trader {i} settles the next generation"); + let out = crate::sdk::routing_path_sdk::constant_product_output(input, ra, rb, 30) + .expect("curve output"); + let (res, x) = trader_settles( + t.router(), + &t.ak_pk, + &t.device_id, + vault_id, + pc_a, + pc_b, + gen, + (ra, rb), + input, + out, + 0x40 + i as u8, + ); + assert!(res.success, "trader {i} settles: {:?}", res.error_message); + settle_outcome(&res, "realized"); + xs.push(x); + } + xs + } + + /// AMENDMENT 2c-G, G1 + G2, on the REAL `storage.sync`. + /// + /// An owner offline for two generations comes back and syncs. The sync pass + /// applies both certified settlements, oldest first, admitted, and the + /// owner's reserve leaves are then EXACTLY the composed frontier. Both + /// entrypoints plan the same certified history (an explicit catch-up + /// through the last settlement IS the frontier), the catch-up creates no + /// certified history (the composed frontier and every trader head are + /// untouched), and a catch-up with nothing owed writes nothing. + /// + /// MUTATION CONTROL: remove the owner catch-up pass from `storage.sync` and + /// the frontier assertion goes red with the leaves still at generation 0. + #[test] + #[serial_test::serial] + fn an_offline_owner_catches_up_on_sync_to_exactly_the_composed_frontier() { + install_identity(); + let (vault_id, (pc_a, pc_b), owner_dev, traders) = market_with_traders( + "sofi/spec/catch-up-sync", + &[("trader0", 0xD1), ("trader1", 0xD2)], + ); + let xs = market_moves(&vault_id, &pc_a, &pc_b, &traders, &[1_000, 700]); + let frontier = composed_frontier(&vault_id, &pc_a, &pc_b); + assert_eq!( + frontier.sequence, 2, + "the market moved the vault two generations" + ); + let trader_roots: Vec<_> = traders + .iter() + .map(|t| { + t.enter(); + t.router() + .core_sdk + .device_head() + .expect("trader head") + .root() + }) + .collect(); + + owner_dev.enter(); + let owner = owner_dev.router(); + // THE SAME ENGINE: the explicit plan through the LAST settlement is the + // frontier plan, oldest first; through the first it stops there. + let own = crate::runtime::get_runtime() + .block_on(super::compose_own_vault(&vault_id)) + .expect("the owner composes its own vault"); + let plan = |t: super::CatchUpTarget| -> Vec<(u64, [u8; 32])> { + super::owed_certified_folds(&own, t) + .expect("plan") + .iter() + .map(|f| { + let trade = f.realized_trade.as_ref().expect("certified").trade(); + (f.generation, trade.x) + }) + .collect() + }; + assert_eq!( + plan(super::CatchUpTarget::Frontier), + vec![(0, xs[0]), (1, xs[1])] + ); + assert_eq!( + plan(super::CatchUpTarget::Through(xs[1])), + plan(super::CatchUpTarget::Frontier) + ); + assert_eq!(plan(super::CatchUpTarget::Through(xs[0])), vec![(0, xs[0])]); + + let spendable_before = spendable(owner, &pc_a, &pc_b); + let resp = crate::runtime::get_runtime().block_on(owner_dev.sync()); + assert!( + !resp.errors.iter().any(|e| e.contains("owner catch-up")), + "the pass ran clean: {:?}", + resp.errors + ); + assert_eq!( + leaves(owner, &vault_id, &pc_a, &pc_b), + (frontier.reserves_a, frontier.reserves_b, frontier.sequence), + "the owner's reserve leaves ARE the composed frontier" + ); + for (i, x) in xs.iter().enumerate() { + assert_eq!( + crate::storage::client_db::load_vault_generation_consumer(&vault_id, i as u64) + .expect("load") + .expect("generation consumed") + .source_commitment, + dsm::dlv::settlement_receipt_leaf::derive_receipt_id(&vault_id, x), + "generation {i} consumed by its certified settlement" + ); + } + assert_eq!( + spendable(owner, &pc_a, &pc_b), + spendable_before, + "a synchronization step moves no value a second time" + ); + + // It CONSUMED certified history and created none. + let after = composed_frontier(&vault_id, &pc_a, &pc_b); + assert_eq!( + (after.sequence, after.c_n), + (frontier.sequence, frontier.c_n) + ); + for (t, root) in traders.iter().zip(&trader_roots) { + t.enter(); + assert_eq!( + t.router() + .core_sdk + .device_head() + .expect("trader head") + .root(), + *root, + "the trader's frontier is untouched by the owner's catch-up" + ); + } + + // NOTHING OWED WRITES NOTHING, through either entrypoint. + owner_dev.enter(); + let root = owner.core_sdk.device_head().expect("head").root(); + let puts = crate::sdk::storage_io::fake_fleet::put_log().len(); + let n = crate::runtime::get_runtime() + .block_on(owner.resume_owner_catch_up()) + .expect("the sync pass"); + assert_eq!(n, 0, "nothing was owed"); + let res = reconcile(owner, &vault_id, &xs[1]); + assert!(res.success, "an explicit replay: {:?}", res.error_message); + assert_eq!(owner.core_sdk.device_head().expect("head").root(), root); + assert_eq!( + crate::sdk::storage_io::fake_fleet::put_log().len(), + puts, + "and published nothing" + ); + } + + /// Resets the catch-up interruption budget even when an assertion fails. + struct UnlimitedCatchUpOnDrop; + impl Drop for UnlimitedCatchUpOnDrop { + fn drop(&mut self) { + super::CATCH_UP_APPLY_BUDGET.store(-1, std::sync::atomic::Ordering::SeqCst); + } + } + + /// AN INTERRUPTED CATCH-UP RESUMES AFTER ITS LAST DURABLE APPLY (ruling G1). + /// + /// Three generations owed; the pass is interrupted after one apply. That + /// apply is durable, nothing past it moved, and the next pass applies only + /// what is still owed — generation 0 is never applied a second time — and + /// ends at the composed frontier. + #[test] + #[serial_test::serial] + fn an_interrupted_catch_up_resumes_without_applying_anything_twice() { + install_identity(); + let (vault_id, (pc_a, pc_b), owner_dev, traders) = market_with_traders( + "sofi/spec/catch-up-resume", + &[("trader0", 0xD5), ("trader1", 0xD6), ("trader2", 0xD7)], + ); + market_moves(&vault_id, &pc_a, &pc_b, &traders, &[1_000, 700, 400]); + let frontier = composed_frontier(&vault_id, &pc_a, &pc_b); + + owner_dev.enter(); + let owner = owner_dev.router(); + let _reset = UnlimitedCatchUpOnDrop; + super::CATCH_UP_APPLY_BUDGET.store(1, std::sync::atomic::Ordering::SeqCst); + let n = crate::runtime::get_runtime() + .block_on(owner.resume_owner_catch_up()) + .expect("the interrupted pass still reports"); + assert_eq!(n, 1, "one apply landed before the interruption"); + assert_eq!(leaves(owner, &vault_id, &pc_a, &pc_b).2, 1); + assert!( + crate::storage::client_db::load_vault_generation_consumer(&vault_id, 1) + .expect("load") + .is_none(), + "nothing past the interruption moved" + ); + let first = crate::storage::client_db::load_vault_generation_consumer(&vault_id, 0) + .expect("load") + .expect("generation 0 consumed"); + + super::CATCH_UP_APPLY_BUDGET.store(-1, std::sync::atomic::Ordering::SeqCst); + let n = crate::runtime::get_runtime() + .block_on(owner.resume_owner_catch_up()) + .expect("the resumed pass"); + assert_eq!(n, 2, "the resumed pass applies only what is still owed"); + assert_eq!( + leaves(owner, &vault_id, &pc_a, &pc_b), + (frontier.reserves_a, frontier.reserves_b, frontier.sequence) + ); + assert_eq!( + crate::storage::client_db::load_vault_generation_consumer(&vault_id, 0) + .expect("load") + .expect("generation 0 consumed") + .source_commitment, + first.source_commitment, + "generation 0 was never applied again" + ); + } + + /// AN APPLY MATERIALIZES THE CERTIFIED FOLD OR NOTHING (ruling G1). + /// + /// The certified fold with one fact altered at a time — the receipt leaf, + /// its inclusion path, the parent's reserves, the parent's generation — is + /// refused, and the refusal writes nothing: the owner's root, its + /// consume-once claims and the fleet are untouched. The honest fold then + /// applies. The leaf and path refusals are the 0x0027 producer's mirror of + /// the arm, BEFORE signing: the arm itself runs only after the advance + /// commits, where a refusal would strand the admission. + /// + /// MUTATION CONTROL: delete either check in + /// `build_settlement_payment_evidence` and the matching case goes red. + #[test] + #[serial_test::serial] + fn a_certified_fold_with_any_fact_altered_is_refused_and_writes_nothing() { + install_identity(); + let (vault_id, (pc_a, pc_b), owner_dev, traders) = + market_with_traders("sofi/spec/catch-up-altered", &[("trader0", 0xD9)]); + market_moves(&vault_id, &pc_a, &pc_b, &traders, &[1_000]); + + owner_dev.enter(); + let owner = owner_dev.router(); + let own = crate::runtime::get_runtime() + .block_on(super::compose_own_vault(&vault_id)) + .expect("the owner composes its own vault"); + let fold = super::owed_certified_folds(&own, super::CatchUpTarget::Frontier).expect("plan") + [0] + .clone(); + + let mut altered_leaf = fold.clone(); + altered_leaf + .certified_payment + .as_mut() + .expect("payment") + .receipt + .output_amount += 1; + let mut altered_path = fold.clone(); + altered_path + .certified_payment + .as_mut() + .expect("payment") + .receipt_siblings[0][0] ^= 0x01; + let mut altered_reserves = fold.clone(); + altered_reserves.state.reserve_a += 1_000; + altered_reserves.state.reserve_b += 1_000; + let mut altered_generation = fold.clone(); + altered_generation.state.generation += 1; + + let root = owner.core_sdk.device_head().expect("head").root(); + let puts = crate::sdk::storage_io::fake_fleet::put_log().len(); + for (what, altered, needle) in [ + ( + "receipt leaf", + altered_leaf, + "does not state this settlement", + ), + ( + "inclusion path", + altered_path, + "does not prove into the root", + ), + ( + "parent reserves", + altered_reserves, + "refusing before signing", + ), + ("parent generation", altered_generation, ""), + ] { + let e = crate::runtime::get_runtime() + .block_on(owner.apply_certified_fold(&vault_id, &altered)) + .expect_err(what); + assert!(e.contains(needle), "{what}: {e}"); + assert_eq!( + owner.core_sdk.device_head().expect("head").root(), + root, + "{what}: the refused apply moved nothing" + ); + assert!( + crate::storage::client_db::load_vault_generation_consumer(&vault_id, 0) + .expect("load") + .is_none(), + "{what}: and claimed no generation" + ); + assert_eq!( + crate::sdk::storage_io::fake_fleet::put_log().len(), + puts, + "{what}: and published nothing" + ); + } + crate::runtime::get_runtime() + .block_on(owner.apply_certified_fold(&vault_id, &fold)) + .expect("the certified fold itself applies"); + assert_eq!(leaves(owner, &vault_id, &pc_a, &pc_b).2, 1); + } + + /// NO RE-ENTRANT CATCH-UP (ruling G2): a sync pass that finds a catch-up + /// already running returns at once and writes nothing, rather than waiting + /// on it or running beside it; once the lock is free it runs. + /// + /// MUTATION CONTROL: make the pass wait on the lock (`lock().await`) and the + /// timeout goes red. + #[test] + #[serial_test::serial] + fn a_sync_pass_skips_while_another_catch_up_runs() { + install_identity(); + let (vault_id, (pc_a, pc_b), owner_dev, traders) = + market_with_traders("sofi/spec/catch-up-lock", &[("trader0", 0xDB)]); + market_moves(&vault_id, &pc_a, &pc_b, &traders, &[1_000]); + + owner_dev.enter(); + let owner = owner_dev.router(); + let root = owner.core_sdk.device_head().expect("head").root(); + let rt = crate::runtime::get_runtime(); + let running = super::owner_catch_up_lock() + .try_lock() + .expect("no catch-up is running yet"); + let n = rt + .block_on(async { + tokio::time::timeout( + std::time::Duration::from_secs(5), + owner.resume_owner_catch_up(), + ) + .await + }) + .expect("the pass returns at once rather than waiting on the running catch-up") + .expect("the pass"); + assert_eq!(n, 0); + assert_eq!(owner.core_sdk.device_head().expect("head").root(), root); + drop(running); + assert_eq!( + rt.block_on(owner.resume_owner_catch_up()) + .expect("the pass"), + 1, + "and runs once the lock is free" + ); + assert_eq!(leaves(owner, &vault_id, &pc_a, &pc_b).2, 1); + } + // ── CLOSE / WITHDRAWAL ─────────────────────────────────────────────────── // Invariant 4 at the ROUTE. The core arm proves the mutation is unforgeable; // these prove the route that drives it: what the owner gets back, when the diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/storage_routes.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/storage_routes.rs index 944451d7..fdb852b3 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/storage_routes.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/handlers/storage_routes.rs @@ -2996,6 +2996,19 @@ impl AppRouterImpl { errors.push(format!("receipt recovery failed: {e}")); } } + // OWNER CATCH-UP (amendment 2c-G, ruling G2): every + // certified settlement traders realized against this + // device's own vaults while it was away, applied oldest + // first and admitted. LAST, and it gates nothing: a failure + // is local to its vault and retried on a later sync, and it + // never calls sync, so there is no loop. + match self.resume_owner_catch_up().await { + Ok(n) => pushed += n, + Err(e) => { + log::warn!("[storage.sync] owner catch-up errored: {e}"); + errors.push(format!("owner catch-up failed: {e}")); + } + } } // Record network success for connectivity monitoring diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/economic_admission_flow.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/economic_admission_flow.rs index 7d023759..eb64a3bf 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/economic_admission_flow.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/economic_admission_flow.rs @@ -673,20 +673,7 @@ pub(crate) async fn admitted_dlv_create_funded( &A, ) -> Result<(), DsmError>, ) -> Result<(dsm::types::device_state::AdvanceOutcome, AdmittedOutcome), DsmError> { - let StagedAdmission { - network_id, - genesis, - devid, - set, - validated, - mut tree, - pre_state, - authority, - facts, - extra_artifacts, - prepared, - .. - } = stage_admission(core, &operation, |_| { + let staged = stage_admission(core, &operation, |_| { Ok((CreditSourceFacts::None, Vec::new())) }) .await?; @@ -712,7 +699,7 @@ pub(crate) async fn admitted_dlv_create_funded( (leg_a_policy_commit, *leg_a_amount), (leg_b_policy_commit, *leg_b_amount), ] { - let have = pre_state.balances.get(pc).copied().unwrap_or(0); + let have = staged.pre_state.balances.get(pc).copied().unwrap_or(0); if have < need { return Err(DsmError::invalid_operation(format!( "insufficient {} to encumber (need {need}, have {have} admitted)", @@ -722,6 +709,136 @@ pub(crate) async fn admitted_dlv_create_funded( } } + admit_reserve_mutation( + core, + staged, + operation, + rel_key, + counterparty_devid, + initial_chain_tip, + reserve_mutation, + "funded create", + build_artifacts, + write_extra, + ) + .await +} + +/// The owner's settlement apply, admitted into `R_econ` (amendment 2c-G, +/// ruling G1+G2). +/// +/// A SYNCHRONIZATION STEP, never an authority. The settlement was realized on +/// the trader's chain and certified by the composition walk before this runs; +/// the apply moves the owner's two reserve leaves one generation to match what +/// already happened. It moves no value a second time — conservation refuses any +/// balance delta for it — and it can apply only the exact certified fold: the +/// credit arm is `0x0027 ValidatedDlvSettlementPayment`, which proves the +/// trader's own receipt leaf into the trader's validated root and checks it +/// field by field against this operation. +/// +/// `payment_evidence_bytes` is the `SettlementPaymentEvidenceV1` the +/// settlement-payment producer built from the certified fold. It is frozen in +/// the SAME transaction as the advance, as every admission's evidence is, and +/// published before the root registers. +#[allow(clippy::too_many_arguments)] +pub(crate) async fn admitted_dlv_owner_apply( + core: &CoreSDK, + operation: Operation, + rel_key: [u8; 32], + counterparty_devid: [u8; 32], + initial_chain_tip: [u8; 32], + reserve_mutation: dsm::types::device_state::VaultReserveMutation, + trader_genesis: [u8; 32], + trader_devid: [u8; 32], + trader_economic_position: u64, + payment_evidence_bytes: Vec, + build_artifacts: impl FnOnce(&dsm::types::device_state::AdvanceOutcome) -> Result, + write_extra: impl Fn( + &rusqlite::Transaction<'_>, + &dsm::types::device_state::AdvanceOutcome, + &A, + ) -> Result<(), DsmError>, +) -> Result<(dsm::types::device_state::AdvanceOutcome, AdmittedOutcome), DsmError> { + if !matches!(operation, Operation::DlvOwnerApplyV2 { .. }) { + return Err(DsmError::invalid_operation( + "admitted_dlv_owner_apply takes a DlvOwnerApplyV2", + )); + } + let payment_evidence_addr = dsm::storage_object::immutable_inner( + dsm::common::domain_tags::TAG_DSM_DLV_SETTLEMENT_PAYMENT_EVIDENCE, + &payment_evidence_bytes, + ); + let evidence_key = crate::sdk::economic_registers::immutable_object_key( + dsm::common::domain_tags::TAG_DSM_DLV_SETTLEMENT_PAYMENT_EVIDENCE, + &payment_evidence_bytes, + ); + let staged = stage_admission(core, &operation, |_position| { + Ok(( + CreditSourceFacts::DlvSettlementPayment { + trader_genesis, + trader_devid, + trader_economic_position, + payment_evidence_addr, + }, + vec![( + evidence_key, + payment_evidence_bytes, + "dlv-settlement-payment-evidence", + )], + )) + }) + .await?; + admit_reserve_mutation( + core, + staged, + operation, + rel_key, + counterparty_devid, + initial_chain_tip, + reserve_mutation, + "owner apply", + build_artifacts, + write_extra, + ) + .await +} + +/// The advance and admission shared by the two reserve-mutation facades — a +/// funded create and an owner apply. They differ only in their facts and their +/// pre-checks; the ONE staged advance (the reserve mutation, the frozen +/// evidence and the Prepared admission together) and the shared +/// [`finish_admission`] are never duplicated per operation. +#[allow(clippy::too_many_arguments)] +async fn admit_reserve_mutation( + core: &CoreSDK, + staged: StagedAdmission, + operation: Operation, + rel_key: [u8; 32], + counterparty_devid: [u8; 32], + initial_chain_tip: [u8; 32], + reserve_mutation: dsm::types::device_state::VaultReserveMutation, + what: &'static str, + build_artifacts: impl FnOnce(&dsm::types::device_state::AdvanceOutcome) -> Result, + write_extra: impl Fn( + &rusqlite::Transaction<'_>, + &dsm::types::device_state::AdvanceOutcome, + &A, + ) -> Result<(), DsmError>, +) -> Result<(dsm::types::device_state::AdvanceOutcome, AdmittedOutcome), DsmError> { + let StagedAdmission { + network_id, + genesis, + devid, + set, + validated, + mut tree, + pre_state, + authority, + facts, + extra_artifacts, + prepared, + .. + } = staged; let set_id = set.id(); let op_for_build = operation.clone(); let mut built: Option = None; @@ -768,7 +885,7 @@ pub(crate) async fn admitted_dlv_create_funded( let pending = accepted_out.ok_or_else(|| { DsmError::storage( - "funded create committed without an accepted admission".to_string(), + format!("{what} committed without an accepted admission"), None::, ) })?; 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 728f5761..e10003fa 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 @@ -115,6 +115,7 @@ pub mod reserve_consumption_producer; pub mod route_commit_sdk; pub mod routing_path_sdk; pub mod routing_sdk; +pub(crate) mod settlement_payment_producer; pub mod settlement_receipt_codec; pub mod settlement_slot; pub mod smart_commitment_sdk; diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/settlement_payment_producer.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/settlement_payment_producer.rs new file mode 100644 index 00000000..f3f641d5 --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/settlement_payment_producer.rs @@ -0,0 +1,95 @@ +// SPDX-License-Identifier: Apache-2.0 + +//! THE OWNER'S SIDE OF 0x0027 (amendment 2c-G). +//! +//! An owner applying a settlement a trader already realized must hand the +//! economic verifier a `SettlementPaymentEvidenceV1`: the trader's `0x0021` +//! settlement-receipt leaf and its 256-sibling inclusion path. The +//! `ValidatedDlvSettlementPayment` arm proves that leaf into the trader's +//! validated economic root at the descriptor's position and cross-checks it +//! field by field against the apply. Nothing produced it, so no owner apply +//! could be admitted. +//! +//! Nothing here is fetched. The composition walk already proved exactly this +//! leaf under exactly that root when it certified the fold (Req 21.16), and +//! carried both on the fold ([`CertifiedPayment`]). This module re-encodes +//! that material — which is why a catch-up consumes certified history and +//! creates none: the evidence is a projection of the certification, never a +//! second observation. +//! +//! Nothing here proves anything either. The two checks below MIRROR the arm, +//! so a defect upstream is refused before the owner signs and advances. They +//! matter more than a courtesy: the arm runs inside `finish_admission`, after +//! the advance has committed, so evidence it refuses would leave an advance +//! whose admission can never finish. The arm is still what decides. + +use dsm::types::error::DsmError; +use prost::Message; + +use crate::sdk::vault_state_composition::CertifiedPayment; + +/// The `SettlementPaymentEvidenceV1` bytes for applying `realized`, built +/// from the payment the walk certified with it. +pub(crate) fn build_settlement_payment_evidence( + realized: &dsm::dlv::published_receipt::VerifiedReceipt, + payment: &CertifiedPayment, +) -> Result, DsmError> { + let trade = realized.trade(); + let leaf = &payment.receipt; + // The arm's step 4, stated: the leaf names exactly this settlement. + if leaf.vault_id != realized.vault_id() + || leaf.receipt_id != realized.receipt_id() + || leaf.x != trade.x + || leaf.parent_sequence != trade.parent_sequence + || leaf.new_sequence != trade.new_sequence + || leaf.input_policy_commit != trade.input_policy_commit + || leaf.input_amount != trade.input_amount + || leaf.output_policy_commit != trade.output_policy_commit + || leaf.output_amount != trade.output_amount + { + return Err(DsmError::invalid_operation( + "0x0027 evidence: the certified receipt leaf does not state this settlement", + )); + } + // The arm's inclusion check, stated: at the trader's own key, the leaf + // proves into the root certification validated for that trader. + let state = dsm::economic::state::EconomicLeafState::SettlementReceipt(leaf.clone()); + let key = state.leaf_key(&payment.trader_genesis, &payment.trader_devid); + let value = state.leaf_value().map_err(|e| { + DsmError::invalid_operation(format!( + "0x0027 evidence: the receipt leaf does not commit: {e}" + )) + })?; + let folded = dsm::economic::tree::root_from_path( + &key, + &dsm::economic::tree::leaf_node(&key, Some(&value)), + &payment.receipt_siblings, + ); + if folded != realized.economic_root() { + return Err(DsmError::invalid_operation( + "0x0027 evidence: the receipt leaf does not prove into the root certification \ + validated", + )); + } + let receipt_state = state.encode().map_err(|e| { + DsmError::invalid_operation(format!( + "0x0027 evidence: the receipt leaf does not encode: {e}" + )) + })?; + let bytes = dsm::types::proto::SettlementPaymentEvidenceV1 { + receipt_state, + receipt_siblings: payment + .receipt_siblings + .iter() + .map(|s| s.to_vec()) + .collect(), + } + .encode_to_vec(); + // And through the arm's own strict decoder, so a bundle it would refuse + // as a shape never reaches an advance. + dsm::economic::settlement_payment_evidence::decode_settlement_payment_evidence(&bytes) + .map_err(|e| { + DsmError::invalid_operation(format!("0x0027 evidence does not decode strictly: {e}")) + })?; + Ok(bytes) +} diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_rehydration.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_rehydration.rs index 0a998c75..a9dcf78e 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_rehydration.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/vault_rehydration.rs @@ -433,7 +433,7 @@ mod tests { dsm::crypto::sphincs::sphincs_sign(sk, &unsigned.with_cleared_signature().to_bytes()) .expect("sign the owner apply"); let head = head - .advance( + .advance_admitted( rel_key, DEVID, unsigned.with_signature(signature), 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 be93104e..9e0f8944 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 @@ -122,6 +122,32 @@ pub(crate) struct FoldedParent { /// a close. Carried so the receipt is built from what certified, never /// from an acceptance fetched again afterwards. pub certified_acceptance: Option, + /// For a CERTIFIED market fold, the trader's payment exactly as Req 21.16 + /// proved it — what the owner's catch-up funds its `0x0027` apply from + /// (amendment 2c-G). `None` for a close. + pub certified_payment: Option, +} + +/// The trader's settlement payment exactly as Req 21.16 proved it: the +/// `0x0021` receipt leaf and its 256-sibling path under the VALIDATED `R_T^+` +/// at the trader's own economic position (amendment 2c-G). +/// +/// Carried on the certified fold for the reason `certified_acceptance` is: +/// the owner's catch-up builds its `0x0027` evidence from the material +/// certification checked, never from an inclusion proof fetched again +/// afterwards. HOLDING ONE ASSERTS NOTHING — the `0x0027` arm re-derives the +/// trader's root at `trader_economic_position` and re-proves the leaf into it. +#[derive(Debug, Clone)] +pub(crate) struct CertifiedPayment { + /// The trader as the walk authenticated it: the acceptance's genesis and + /// the bundle's own settler. + pub trader_genesis: [u8; 32], + pub trader_devid: [u8; 32], + /// The position whose validated root the walk proved the leaf under. + pub trader_economic_position: u64, + /// The exact leaf the trader's inclusion proof committed, and its path. + pub receipt: dsm::economic::state::EconomicSettlementReceiptState, + pub receipt_siblings: Box<[[u8; 32]; dsm::economic::tree::ECONOMIC_SMT_HEIGHT]>, } /// What the binding register — plus this device's own fence table — says about @@ -758,11 +784,12 @@ 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, certified_acceptance) = match bound.shape { + let (verdict, realized_trade, certified_acceptance, certified_payment) = match bound.shape { dsm::dlv::settlement_bundle::BundleShape::OwnerClose => ( C3Verdict::Valid(CompleteValidity::from_close_witness(witness)), None, None, + None, ), dsm::dlv::settlement_bundle::BundleShape::Market => { let (Some(ev), Some(terms)) = (market_evidence.take(), bound.bundle.market_terms()) @@ -805,6 +832,7 @@ async fn compose_vault_state_inner( C3Verdict::Valid(CompleteValidity::from_market_witness(witness, realization)), Some(ev.receipt), Some(ev.acceptance), + Some(ev.payment), ) } }; @@ -823,6 +851,7 @@ async fn compose_vault_state_inner( verdict, realized_trade, certified_acceptance, + certified_payment, }); let _ = transition; cursor_state = next_state; @@ -906,6 +935,8 @@ struct EstablishedMarketEvidence { trader: ValidatedPeerTransition, intent: IntentSatisfaction, receipt: VerifiedReceipt, + /// The receipt leaf and path Req 21.16 just proved, for the fold. + payment: CertifiedPayment, } /// Gather and verify everything a market certification needs, in the order @@ -1103,11 +1134,11 @@ async fn certify_market_evidence( )); } let receipt_id = derive_receipt_id(vault_id, &x); - let Some(path) = artifact.leaves.iter().find_map(|leaf| match &leaf.state { + let Some((receipt_leaf, path)) = artifact.leaves.iter().find_map(|leaf| match &leaf.state { dsm::economic::state::EconomicLeafState::SettlementReceipt(s) if s.vault_id == *vault_id && s.receipt_id == receipt_id => { - Some(leaf.siblings.clone()) + Some((s.clone(), leaf.siblings.clone())) } _ => None, }) else { @@ -1130,6 +1161,16 @@ async fn certify_market_evidence( } }; + // What the owner's apply is funded by (2c-G): the leaf and path just + // proven, at the position whose validated root they were proven under. + let payment = CertifiedPayment { + trader_genesis: acceptance.trader_genesis(), + trader_devid: settler_devid, + trader_economic_position: acceptance.economic_position(), + receipt: receipt_leaf, + receipt_siblings: path, + }; + MarketEvidence::Established(Box::new(EstablishedMarketEvidence { expected, accepted, @@ -1138,6 +1179,7 @@ async fn certify_market_evidence( trader, intent, receipt, + payment, })) } diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_owner_apply_preservation.rs b/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_owner_apply_preservation.rs index ab8a122a..ba32d98c 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_owner_apply_preservation.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_owner_apply_preservation.rs @@ -191,7 +191,7 @@ fn try_apply_settlement( op: Operation, ) -> Result { let rel = compute_smt_key(&OWNER, &OWNER); - head.advance( + head.advance_admitted( rel, OWNER, op, diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_value_op_signing.rs b/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_value_op_signing.rs index 3ad09d52..3d28f1ef 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_value_op_signing.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/tests/dlv_value_op_signing.rs @@ -187,7 +187,7 @@ fn advance_with( }, ] }; - head.advance( + head.advance_admitted( compute_smt_key(&ACTOR, &ACTOR), ACTOR, op, diff --git a/lean4/DSMOwnerCatchUp.lean b/lean4/DSMOwnerCatchUp.lean new file mode 100644 index 00000000..ca358d1a --- /dev/null +++ b/lean4/DSMOwnerCatchUp.lean @@ -0,0 +1,285 @@ +/- + Owner catch-up — self-contained Lean 4 (no Mathlib, no imports) + + Machine-checks amendment 2c-G's rulings G1 + G2 over one vault: the owner's + invariant "owner catch-up consumes certified history; it never creates + certified history", and the engine both entrypoints share. + + - CREATES NONE a catch-up never changes the certified history + - CERTIFIED ONLY the owner never applies past what was certified + - ORDERED the applied record is a prefix of the certified history, + and a catch-up only ever extends it + - FRONTIER a catch-up to the frontier ends exactly there + - THROUGH x an explicit catch-up ends exactly after x; one naming no + certified settlement writes nothing + - SAME ENGINE through the last certified settlement IS the frontier + - RESUMABLE interrupted after b1 applies and resumed for b2, it ends + where one uninterrupted run of b1 + b2 would + - IDEMPOTENT a second catch-up changes nothing + + The model. `certified` is the certified market folds the composition walk + produced, oldest first — settlement identities in generation order. `applied` + is how many of them the owner has materialized: its reserve generation above + the baseline. The applied RECORD is `certified.take applied`, so an owner + state that names a settlement outside the certified history, or out of its + order, is not representable — which is the point: ORDERED is structural here, + and what the theorems pin is that no catch-up moves `applied` past what was + certified, backwards, or on a target that names nothing. + + `budget` is how many applies a run completes before it is interrupted. An + uninterrupted run is any budget at least as large as what is owed. + + What this module does NOT claim: + + * Certification. `certified` is the walk's output, an input here; that the + walk installs nothing uncertified is 2c-C3/2c-D's, modelled in + DSMValidDlvSuccessor and DSMAcceptedSuccessorWalk. + * The apply's validity. That each apply is exactly its certified fold — + the 0x0027 arm, the write set, the core curve and parent checks — is + the implementation's, pinned by its tests; here an apply is an index. + * Admission liveness. A run refused inside one apply is `budget = n`. + + Mutation controls, executed rather than asserted — the kernel proving the + NEGATION of a named sample theorem: + + 1. a target naming no certified settlement is read as the frontier + -> `an_uncertified_target_applies_nothing` is proved FALSE + 2. the goal clamp removed (a run applies its whole budget) + -> `a_catch_up_stops_at_the_frontier` is proved FALSE + 3. consume-once removed (an applied settlement is applied again) + -> `a_second_catch_up_changes_nothing_sample` is proved FALSE + + All mutations were reverted; this file is the unmutated module. +-/ + +namespace DSMOwnerCatchUp + +/-- One vault, as the owner's catch-up sees it. -/ +structure Vault where + /-- The certified market settlements, oldest first. -/ + certified : List Nat + /-- How many of them the owner has applied. -/ + applied : Nat + deriving DecidableEq, Repr + +/-- Where a catch-up stops. -/ +inductive Target where + | frontier + | through (x : Nat) + deriving DecidableEq, Repr + +/-- The index of `x` in the certified history, if it is there. -/ +def position (x : Nat) : List Nat → Option Nat + | [] => none + | y :: ys => if y = x then some 0 else (position x ys).map (· + 1) + +/-- One past the last settlement a catch-up to `t` applies, or `none` when +`t` names no certified settlement. -/ +def goal (h : List Nat) : Target → Option Nat + | .frontier => some h.length + | .through x => (position x h).map (· + 1) + +/-- Advance `a` applied settlements toward goal `g`, completing at most `b` +applies. Already past the goal: nothing is owed and nothing moves. -/ +def advanceTo (a g b : Nat) : Nat := + if g ≤ a then a else if a + b ≤ g then a + b else g + +/-- THE engine: a target that names nothing writes nothing; otherwise the +owed prefix is applied oldest first, up to the goal. -/ +def catchUp (t : Target) (b : Nat) (v : Vault) : Vault := + match goal v.certified t with + | none => v + | some g => { v with applied := advanceTo v.applied g b } + +/-- The owner's applied record: the certified prefix it has materialized. -/ +def appliedRecord (v : Vault) : List Nat := + v.certified.take v.applied + +-- ───────────────────────────────────────────────────────────────────────────── +-- Lemmas +-- ───────────────────────────────────────────────────────────────────────────── + +theorem position_lt (x : Nat) : ∀ (h : List Nat) (i : Nat), + position x h = some i → i < h.length + | [], i, hp => by simp [position] at hp + | y :: ys, i, hp => by + unfold position at hp + split at hp + · simp at hp + subst hp + simp + · cases hq : position x ys with + | none => simp [hq] at hp + | some j => + simp [hq] at hp + have := position_lt x ys j hq + simp + omega + +theorem goal_le_length (h : List Nat) (t : Target) (g : Nat) + (hg : goal h t = some g) : g ≤ h.length := by + cases t with + | frontier => simp [goal] at hg; omega + | through x => + simp [goal] at hg + obtain ⟨i, hi, rfl⟩ := hg + have := position_lt x h i hi + omega + +theorem advanceTo_ge (a g b : Nat) : a ≤ advanceTo a g b := by + unfold advanceTo + repeat' split + all_goals omega + +theorem advanceTo_le (a g b : Nat) (ha : a ≤ g) : advanceTo a g b ≤ g := by + unfold advanceTo + repeat' split + all_goals omega + +theorem advanceTo_resume (a g b1 b2 : Nat) : + advanceTo (advanceTo a g b1) g b2 = advanceTo a g (b1 + b2) := by + unfold advanceTo + repeat' split + all_goals omega + +-- ───────────────────────────────────────────────────────────────────────────── +-- General statements +-- ───────────────────────────────────────────────────────────────────────────── + +/-- CREATES NONE: the certified history after a catch-up is the certified +history before it. -/ +theorem catch_up_creates_no_certified_history (t : Target) (b : Nat) (v : Vault) : + (catchUp t b v).certified = v.certified := by + unfold catchUp + split <;> rfl + +/-- CERTIFIED ONLY: an owner that has applied nothing uncertified never +applies past the certified history. -/ +theorem the_owner_never_applies_past_what_was_certified (t : Target) (b : Nat) (v : Vault) + (hv : v.applied ≤ v.certified.length) : + (catchUp t b v).applied ≤ (catchUp t b v).certified.length := by + unfold catchUp + split + · exact hv + · rename_i g hg + have := goal_le_length v.certified t g hg + show advanceTo v.applied g b ≤ v.certified.length + unfold advanceTo + repeat' split + all_goals omega + +/-- ORDERED: a catch-up only ever extends the applied record — it never +un-applies, and the record is always a certified prefix. -/ +theorem a_catch_up_only_extends_the_record (t : Target) (b : Nat) (v : Vault) : + v.applied ≤ (catchUp t b v).applied ∧ + appliedRecord (catchUp t b v) = v.certified.take (catchUp t b v).applied := by + unfold catchUp appliedRecord + split + · exact ⟨Nat.le_refl _, rfl⟩ + · exact ⟨advanceTo_ge _ _ _, rfl⟩ + +/-- FRONTIER: an uninterrupted catch-up to the frontier ends exactly at the +composed frontier. -/ +theorem the_frontier_catch_up_ends_at_the_frontier (b : Nat) (v : Vault) + (hv : v.applied ≤ v.certified.length) + (hb : v.certified.length ≤ v.applied + b) : + (catchUp .frontier b v).applied = v.certified.length := by + show advanceTo v.applied v.certified.length b = v.certified.length + unfold advanceTo + repeat' split + all_goals omega + +/-- THROUGH x: an uninterrupted explicit catch-up ends exactly after `x`. -/ +theorem the_explicit_catch_up_ends_after_its_settlement (x i b : Nat) (v : Vault) + (hp : position x v.certified = some i) + (hv : v.applied ≤ i + 1) + (hb : i + 1 ≤ v.applied + b) : + (catchUp (.through x) b v).applied = i + 1 := by + unfold catchUp + simp only [goal, hp, Option.map_some] + show advanceTo v.applied (i + 1) b = i + 1 + unfold advanceTo + repeat' split + all_goals omega + +/-- A target naming no certified settlement writes nothing. -/ +theorem an_uncertified_target_writes_nothing (x b : Nat) (v : Vault) + (hp : position x v.certified = none) : + catchUp (.through x) b v = v := by + unfold catchUp + simp only [goal, hp, Option.map_none] + +/-- SAME ENGINE: through the last certified settlement is the frontier. -/ +theorem through_the_last_settlement_is_the_frontier (x b : Nat) (v : Vault) + (hp : position x v.certified = some (v.certified.length - 1)) : + catchUp (.through x) b v = catchUp .frontier b v := by + have hlt := position_lt x v.certified _ hp + unfold catchUp + simp only [goal, hp, Option.map_some] + have : v.certified.length - 1 + 1 = v.certified.length := by omega + rw [this] + +/-- RESUMABLE: interrupted after `b1` applies and resumed for `b2`, a catch-up +ends where one uninterrupted run of `b1 + b2` would. -/ +theorem an_interrupted_catch_up_resumes_to_the_same_state (t : Target) (b1 b2 : Nat) + (v : Vault) : + catchUp t b2 (catchUp t b1 v) = catchUp t (b1 + b2) v := by + unfold catchUp + cases hg : goal v.certified t with + | none => simp [hg] + | some g => simp [hg, advanceTo_resume] + +/-- IDEMPOTENT: once caught up, a second catch-up changes nothing. -/ +theorem a_second_catch_up_changes_nothing (t : Target) (b b' : Nat) (v : Vault) + (hb : v.certified.length ≤ v.applied + b) : + catchUp t b' (catchUp t b v) = catchUp t b v := by + unfold catchUp + cases hg : goal v.certified t with + | none => simp [hg] + | some g => + have := goal_le_length v.certified t g hg + simp only [hg] + congr 1 + unfold advanceTo + repeat' split + all_goals omega + +-- ───────────────────────────────────────────────────────────────────────────── +-- Samples — the statements above are not vacuous +-- ───────────────────────────────────────────────────────────────────────────── + +/-- Three certified settlements; the owner, back from offline, has applied none. -/ +def back : Vault := ⟨[10, 11, 12], 0⟩ + +theorem an_uncertified_target_applies_nothing : + catchUp (.through 99) 10 back = back := by decide + +theorem a_catch_up_stops_at_the_frontier : + (catchUp .frontier 10 back).applied = 3 := by decide + +theorem an_explicit_catch_up_applies_the_older_ones_first : + appliedRecord (catchUp (.through 11) 10 back) = [10, 11] := by decide + +theorem an_interrupted_sample_resumes : + catchUp .frontier 10 (catchUp .frontier 1 back) = catchUp .frontier 10 back := by + decide + +theorem a_second_catch_up_changes_nothing_sample : + catchUp .frontier 10 (catchUp .frontier 10 back) = catchUp .frontier 10 back := by + decide + +-- ───────────────────────────────────────────────────────────────────────────── +-- Axiom report +-- ───────────────────────────────────────────────────────────────────────────── + +#print axioms catch_up_creates_no_certified_history +#print axioms the_owner_never_applies_past_what_was_certified +#print axioms a_catch_up_only_extends_the_record +#print axioms the_frontier_catch_up_ends_at_the_frontier +#print axioms the_explicit_catch_up_ends_after_its_settlement +#print axioms an_uncertified_target_writes_nothing +#print axioms through_the_last_settlement_is_the_frontier +#print axioms an_interrupted_catch_up_resumes_to_the_same_state +#print axioms a_second_catch_up_changes_nothing + +end DSMOwnerCatchUp