diff --git a/.github/instructions/sofispecs.instructions.md b/.github/instructions/sofispecs.instructions.md index 0e0127ca..3349ef74 100644 --- a/.github/instructions/sofispecs.instructions.md +++ b/.github/instructions/sofispecs.instructions.md @@ -1244,6 +1244,15 @@ Permanent unresolution remains possible on the market-first path or while a quor transaction itself has not reached a recoverable terminal decision. Beta defines no timeout, automatic eviction, direct-owner withdrawal bypass, or override that discards a market candidate whose DLV parent may already be bound. +Implementation (amendment 2c-G, G4). The release/close is economically admitted: its write set +drains exactly the owner's admitted reserve leaves at exactly the parent generation and credits +ordinary balance from them in the same conservation-preserving update, so the released value exists +in the owner's economic lineage. The one canonical close commit derives the parent, generation, +reserves and storage set from the composed vault state — never from its caller — and refuses a +close whose parent a realized market successor already consumed, a skipped or stale generation, +amounts other than the parent's, and a parent another candidate holds. Close authority, QuorumBind +and the accepted-successor rules are unchanged, and a close still requires the owner caught up to +the composed frontier first. Requirement 6.31 (Owner catch-up baseline). When the LP returns to an active DLV and catches its bilateral relationship state against the DLV up through all then-known realized market successors, the resulting authenticated owner state must commit a fresh DLV baseline/anchor. Later diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f04313e9..3b3b1e9e 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=20 + expected=21 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 990c0b21..36368ee3 100644 --- a/docs/papers/ccb-object-registry.md +++ b/docs/papers/ccb-object-registry.md @@ -1564,6 +1564,12 @@ storage-object address (amendment 2c-C1 ruling A). | 1 | `credit_mutation_index` | `u32` | **must differ from field 2** | | 2 | `debit_mutation_index` | `u32` | a transition cannot fund itself from itself | +**Producers.** The write-set builder derives `0x0024` itself; no caller supplies it. It funds a +funded create's reserve credits from the balances it debits and a close's balance credits from the +reserves it drains. Since amendment 2c-G (G4) `DlvClose` is admission-fenced at the core chokepoint, +like `DlvCreateFundedV2` and `DlvOwnerApplyV2`: a close's proceeds exist in `R_econ`, or the close +does not advance. + **§5.35 — `0x0025 CreditSourceValidatedPeerDebit`**, schema 1 | # | Field | Type | Notes | 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 1acd1b22..c918b434 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,11 +1843,11 @@ 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 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. + // Deliberately NARROW. Settle is not fenced here: it consumes an + // existing position rather than originating one, and its admission + // wiring is a separate cut with a separate evidence story. Widening this + // gate before a producer exists would strand the trader path with no + // replacement. if matches!(operation, Operation::DlvCreateFundedV2 { .. }) { self.require_attached_dsm_admission(&operation, "a funded vault creation")?; } @@ -1863,6 +1863,17 @@ impl DeviceState { self.require_attached_dsm_admission(&operation, "an owner apply")?; } + // THE TERMINAL CLOSE (amendment 2c-G, G4). `DlvClose` drains both vault + // reserve leaves into spendable balance. Unadmitted, that balance is + // head-only — `R_econ` never withdraws the reserve leaf nor credits the + // balance, so the proceeds can fund no admitted operation — and a close + // at a generation `R_econ` does not hold would retire a vault whose + // economic lineage never reached it. Admitted, its write set drains + // exactly the `R_econ` reserve leaves at exactly the parent generation. + if matches!(operation, Operation::DlvClose { .. }) { + self.require_attached_dsm_admission(&operation, "a vault close")?; + } + // 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 @@ -7428,6 +7439,75 @@ mod tests { assert_eq!(funded.vault_reserve(&vault, &rigb), 5_000); } + /// THE CLOSE IS ADMITTED OR IT DOES NOT HAPPEN (amendment 2c-G, G4). + /// + /// A matching close of a funded vault, advanced RAW, is refused by the + /// fence's own precondition, with the reserves and the balances exactly + /// where they were: unadmitted, the proceeds would exist on the head and + /// nowhere in `R_econ`. The same close with its own admission attached + /// drains the vault — the positive control that makes the refusal the + /// fence's. + /// + /// MUTATION CONTROL: delete the `DlvClose` arm of the fence in `advance` + /// and the first assertion goes red by crediting the reserves to balance. + #[test] + fn a_close_is_refused_without_its_own_attached_admission() { + let (era, rigb) = (pc(0xE0), pc(0xF0)); + let (funded, vault, rk, tip) = funded_for_close(0xD8, era, rigb, 7_000, 3_000); + let funded = funded.with_pending_economic_admission(None); + let root_before = funded.root(); + let (free_a, free_b) = (funded.balance(&era), funded.balance(&rigb)); + + let err = format!( + "{}", + funded + .advance( + rk, + funded.devid, + dlv_close_op(vault, era, 7_000, rigb, 3_000, 0, 1), + entropy(2), + None, + &[], + Some(tip), + None, + None, + Some(withdraw_mutation(vault, era, 7_000, rigb, 3_000, 0, 1)), + ) + .expect_err("a raw close must not credit the reserves") + ); + assert!( + err.contains("no pending economic admission"), + "the refusal is the fence's own, got: {err}" + ); + assert_eq!(funded.root(), root_before, "nothing moved"); + assert_eq!(funded.vault_reserve(&vault, &era), 7_000); + assert_eq!( + (funded.balance(&era), funded.balance(&rigb)), + (free_a, free_b) + ); + + let closed = funded + .advance_admitted( + rk, + funded.devid, + dlv_close_op(vault, era, 7_000, rigb, 3_000, 0, 1), + entropy(2), + None, + &[], + Some(tip), + None, + None, + Some(withdraw_mutation(vault, era, 7_000, rigb, 3_000, 0, 1)), + ) + .expect("the admitted close advances") + .new_device_state; + assert_eq!(closed.vault_reserve(&vault, &era), 0); + assert_eq!( + (closed.balance(&era), closed.balance(&rigb)), + (free_a + 7_000, free_b + 3_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 @@ -7744,7 +7824,7 @@ mod tests { let (free_a_before, free_b_before) = (funded.balance(&era), funded.balance(&rigb)); let out = funded - .advance( + .advance_admitted( rk, funded.devid, dlv_close_op(vault, era, 10_000, rigb, 5_000, 0, 1), @@ -7780,7 +7860,7 @@ mod tests { // SINGLE USE. A second close is refused (already zero), and re-funding // is refused because the leaves EXIST — not because an amount is // non-zero. - let second = after.advance( + let second = after.advance_admitted( rk, after.devid, dlv_close_op(vault, era, 0, rigb, 0, 1, 2), @@ -7872,7 +7952,7 @@ mod tests { let (free_a, free_b) = (traded.balance(&era), traded.balance(&rigb)); // Closing at the FUNDING amounts is refused: they are not the leaves. - let stale = traded.advance( + let stale = traded.advance_admitted( rk, traded.devid, dlv_close_op(vault, era, 10_000, rigb, 5_000, 1, 2), @@ -7888,7 +7968,7 @@ mod tests { assert!(e.contains("exactly the leaf's amount"), "got: {e}"); let after = traded - .advance( + .advance_admitted( rk, traded.devid, dlv_close_op(vault, era, 11_000, rigb, 5_000 - out_amt, 1, 2), @@ -8057,8 +8137,11 @@ mod tests { ), ]; + // Each malformed close carries its own admission, so every case is + // refused by the check it names — not by the missing-admission fence + // (pinned separately by `a_close_is_refused_without_its_own_attached_admission`). for case in attempts { - let res = funded.advance( + let res = funded.advance_admitted( rk, funded.devid, case.op, @@ -8168,7 +8251,7 @@ mod tests { // Same head, same operation, no pending admission: it succeeds. This // is what makes the assertion above about the fence specifically. funded - .advance( + .advance_admitted( rk, funded.devid, dlv_close_op(vault, era, 7_000, rigb, 3_000, 0, 1), @@ -8426,7 +8509,7 @@ mod tests { let (era, rigb) = (pc(0xE0), pc(0xF0)); let (funded, vault, rk, tip) = funded_for_close(0xD4, era, rigb, 7_000, 3_000); let closed = funded - .advance( + .advance_admitted( rk, funded.devid, dlv_close_op(vault, era, 7_000, rigb, 3_000, 0, 1), 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 2a4319c2..d261e3ef 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 @@ -1734,21 +1734,32 @@ impl AppRouterImpl { /// Shared by `dlv.close` and by recovery, so a resumed close commits through /// exactly the same path (with the same frozen operation bytes) as the /// original attempt. - #[allow(clippy::too_many_arguments)] + /// + /// ADMITTED, AND DERIVED (amendment 2c-G, G4). The advance is the admitted + /// close, so the proceeds exist in `R_econ`. Every fact it consumes — parent, + /// generation, reserves, parent binding, storage set — is read off + /// `composed` by [`close_plan`], which holds the signed operation to them; + /// no caller supplies one, and a close the market has moved past, one that + /// skips a generation, one with other amounts, or one whose parent another + /// candidate holds never reaches the advance. async fn commit_canonical_close( &self, vault_id: &[u8; 32], - parent_sequence: u64, - new_sequence: u64, - pair: &dsm::types::device_state::VaultStatePair, - storage_set_id: &[u8; 32], + composed: &crate::sdk::vault_state_composition::ComposedVaultState, close_commitment: &[u8; 32], op: dsm::types::operations::Operation, - reserve_a: u64, - reserve_b: u64, - parent_binding: [u8; 32], ) -> Result<(), String> { use crate::storage::client_db::dlv_close_intent as intent_db; + let ClosePlan { + pair, + parent_sequence, + new_sequence, + reserve_a, + reserve_b, + parent_binding, + storage_set_id, + } = close_plan(vault_id, composed, &op).map_err(|e| format!("dlv.close: {e}"))?; + let (pair, storage_set_id) = (&pair, &storage_set_id); // One staged advance: the release, the consume-once claim for this // generation, and the FIVE frozen terminal objects commit together, or // none of them do. Value is spendable at this commit — and durable, @@ -1865,19 +1876,24 @@ impl AppRouterImpl { })?; Ok(()) }; - if let Err(e) = self - .core_sdk - .execute_on_relationship_staged_with_reserve_mutation( - rel_key, - actor, - op, - &[], - Some(init_tip), - Some(mutation), - build, - write, - ) + if let Err(e) = crate::sdk::economic_admission_flow::admitted_dlv_close( + &self.core_sdk, + op, + rel_key, + actor, + init_tip, + mutation, + build, + write, + ) + .await { + // An admission that stops AFTER its advance committed (evidence + // below quorum, a register miss) is held, not lost: the close and + // its terminal objects are durable, and the sync pass resumes the + // pending admission. What follows concerns a close that did not + // commit. + // // NOT abandoned here. This error can be transient (a busy database, // a lock) or permanent (the owner folded a settlement in between, so // the generation moved and the reserve arm refuses). Abandoning on @@ -2098,10 +2114,6 @@ impl AppRouterImpl { abandon("the frozen close operation no longer decodes"); continue; }; - let Some(new_sequence) = intent.parent_sequence.checked_add(1) else { - abandon("sequence overflow"); - continue; - }; // The permitted continuation this close prepared: `c_{n+1}` of the // exact drained successor the owner authorized (2c-A.1 ruling 3). // Recorded, never re-derived — a re-derivation could name a @@ -2111,13 +2123,8 @@ impl AppRouterImpl { .finish_prepared_close( &intent.vault_id, intent.parent_sequence, - new_sequence, - &pair, - &composed.storage_set_id, &close_commitment, op, - live.reserve_a, - live.reserve_b, ) .await { @@ -2140,18 +2147,12 @@ impl AppRouterImpl { /// claim must never be, and keeping the key out of that scope is what makes /// "never" a property of the code rather than of the current author's /// discipline. - #[allow(clippy::too_many_arguments)] async fn finish_prepared_close( &self, vault_id: &[u8; 32], parent_sequence: u64, - new_sequence: u64, - pair: &dsm::types::device_state::VaultStatePair, - storage_set_id: &[u8; 32], close_commitment: &[u8; 32], op: dsm::types::operations::Operation, - reserve_a: u64, - reserve_b: u64, ) -> Result<(), String> { // The terminal state's predecessor edge: the c_n of the frontier this // close consumes, recomputed from the vault's own published baseline. @@ -2167,9 +2168,7 @@ impl AppRouterImpl { // it on the way through — it is the folded parent binding for exactly // this generation. Any other composed generation means the vault moved // for some other reason and the close must not proceed blind. - let parent_binding = if composed.sequence == parent_sequence { - composed.c_n - } else if composed.sequence == parent_sequence.saturating_add(1) { + if composed.sequence == parent_sequence.saturating_add(1) { let folded = composed .folded_parents .iter() @@ -2230,27 +2229,18 @@ impl AppRouterImpl { else's transaction" )); } - folded.c_n - } else { + } else if composed.sequence != parent_sequence { return Err(format!( "resumed close: the composed state is at generation {} but this close \ consumes {parent_sequence} — reconcile first", composed.sequence )); - }; - self.commit_canonical_close( - vault_id, - parent_sequence, - new_sequence, - pair, - storage_set_id, - close_commitment, - op, - reserve_a, - reserve_b, - parent_binding, - ) - .await + } + // The parent binding, the reserves and the storage set are the + // composition's, derived inside the commit by `close_plan` — the same + // derivation a fresh close runs. + self.commit_canonical_close(vault_id, &composed, close_commitment, op) + .await } /// `dlv.close` — the owner withdraws ALL remaining liquidity and retires the @@ -2678,18 +2668,7 @@ impl AppRouterImpl { } if let Err(e) = self - .commit_canonical_close( - &vault_id, - parent_sequence, - new_sequence, - &pair, - &storage_set_id, - &close_commitment, - op, - live.reserve_a, - live.reserve_b, - composed.c_n, - ) + .commit_canonical_close(&vault_id, &composed, &close_commitment, op) .await { return err(e); @@ -4466,6 +4445,133 @@ const BIRTH_ARTIFACT_PURPOSE: &str = "dlv-birth"; /// Purpose label frozen on a vault's TERMINAL objects. const TERMINAL_ARTIFACT_PURPOSE: &str = "dlv-terminal"; +/// What a close consumes, read off the composition — never supplied by a +/// caller (amendment 2c-G, G4). +struct ClosePlan { + pair: dsm::types::device_state::VaultStatePair, + parent_sequence: u64, + new_sequence: u64, + reserve_a: u64, + reserve_b: u64, + parent_binding: [u8; 32], + storage_set_id: [u8; 32], +} + +/// Derive the parent a close consumes from the composed vault state, and hold +/// the signed operation to it field by field. +/// +/// The parent is the composed frontier — free, or fenced by this device's own +/// close — or, once this close has bound and folded, the parent the walk folded +/// it from. Anything else is a close the market has moved past: a realized +/// market successor consumed that generation (a close may not erase it), later +/// generations exist (a close may not skip them), the generation lies beyond +/// the frontier (a close may not skip ahead), or another candidate holds the +/// parent unrealized (an uncertified predecessor blocks the close). The owner +/// being caught up to that parent is the admission's precondition, checked +/// against `R_econ`, not this function's. +fn close_plan( + vault_id: &[u8; 32], + composed: &crate::sdk::vault_state_composition::ComposedVaultState, + op: &dsm::types::operations::Operation, +) -> Result { + use crate::sdk::vault_state_composition::FrontierBinding; + use dsm::dlv::settlement_bundle::BundleShape; + let dsm::types::operations::Operation::DlvClose { + vault_id: op_vault, + leg_a_policy_commit, + leg_a_amount, + leg_b_policy_commit, + leg_b_amount, + parent_sequence, + new_sequence, + fee_bps, + .. + } = op + else { + return Err("the close commit takes a DlvClose".into()); + }; + let parent = *parent_sequence; + let (parent_state, parent_binding) = if composed.sequence == parent { + match composed.frontier_binding { + FrontierBinding::Free | FrontierBinding::LocallyFenced { .. } => { + (&composed.state, composed.c_n) + } + FrontierBinding::BoundUnrealized { .. } => { + return Err(format!( + "another candidate holds generation {parent} unrealized — an uncertified \ + predecessor blocks the close" + )) + } + FrontierBinding::NotObserved => { + return Err( + "the composition did not observe the frontier this close consumes".into(), + ) + } + } + } else if composed.sequence == parent.saturating_add(1) { + match composed + .folded_parents + .iter() + .find(|f| f.generation == parent) + { + Some(f) if f.bound_kind == BundleShape::OwnerClose => (&f.state, f.c_n), + Some(_) => { + return Err(format!( + "a realized market successor consumed generation {parent} — a close may not \ + erase it" + )) + } + None => { + return Err(format!( + "the composition names no parent for generation {parent}" + )) + } + } + } else if composed.sequence > parent { + return Err(format!( + "the market realized generations past {parent} (the composed frontier is {}) — a \ + close may not erase or skip them", + composed.sequence + )); + } else { + return Err(format!( + "generation {parent} lies beyond the composed frontier {} — a close may not skip a \ + generation", + composed.sequence + )); + }; + let pair = dsm::types::device_state::VaultStatePair::new( + *parent_state.market_policy.token_a(), + *parent_state.market_policy.token_b(), + parent_state.fee_policy.fee_bps(), + ) + .map_err(|e| format!("the parent state's pair is not canonical: {e}"))?; + if parent_state.vault_id != *vault_id + || op_vault.as_slice() != vault_id.as_slice() + || parent_state.generation != parent + || parent.checked_add(1) != Some(*new_sequence) + || *leg_a_policy_commit != pair.a() + || *leg_b_policy_commit != pair.b() + || *leg_a_amount != parent_state.reserve_a + || *leg_b_amount != parent_state.reserve_b + || *fee_bps != pair.fee_bps() + { + return Err(format!( + "the signed close does not drain exactly the composed generation {parent} — its \ + vault, legs, amounts, fee or generation step differ" + )); + } + Ok(ClosePlan { + pair, + parent_sequence: parent, + new_sequence: *new_sequence, + reserve_a: parent_state.reserve_a, + reserve_b: parent_state.reserve_b, + parent_binding, + storage_set_id: composed.storage_set_id, + }) +} + /// A vault generation's publication set, built and signed off ONE /// `AdvanceOutcome` — the exact reserves the advance landed — before anything /// is persisted, then frozen byte-for-byte inside the advance transaction. @@ -11549,6 +11655,275 @@ mod funded_creation_tests { assert_eq!(leaves(owner, &vault_id, &pc_a, &pc_b), (0, 0, 2)); } + /// G4 — BELOW THE ROUTE'S GATE, A CLOSE STILL DRAINS EXACTLY THE CAUGHT-UP + /// FRONTIER, OR NOTHING. + /// + /// The route refuses a stale close before recording anything + /// (`a_close_is_refused_while_a_settlement_is_unreconciled`), and a parent + /// another candidate holds refuses it too + /// (`a_contested_parent_refuses_the_close_and_moves_nothing`). This drives + /// the ONE close commit directly, as a defect upstream of the gate would: + /// + /// - the owner's stale baseline — generation 0, which a certified market + /// successor already consumed — is refused by `close_plan`: a close may + /// not erase a realized successor; + /// - the composed frontier, while the owner has NOT caught up to it, is + /// refused by the admitted advance: `R_econ` and the head hold generation + /// 0, not the parent the close drains; + /// + /// and each writes nothing. Caught up by the sync pass, the route's close + /// succeeds, and its proceeds are ADMITTED: they fund a second vault the + /// pre-close admitted balance could not. + /// + /// MUTATION CONTROL: commit the close through the unadmitted staged advance + /// (with the core fence's close arm removed) and the final create is + /// refused as insufficient — the proceeds never reached `R_econ`. + #[test] + #[serial] + fn a_close_below_the_gate_drains_exactly_the_caught_up_frontier_or_nothing() { + install_identity(); + let owner_dev = participant("owner", 0x41); + let owner = owner_dev.router(); + // 55_000/20_000: after the 10_000/5_000 legs and the 5_000 sent to the + // trader, the owner holds (40_000, 15_000) admitted. + let (pc_a, pc_b) = + crate::sdk::funded_vault_fixture::admitted_device_holding(owner, 55_000, 20_000); + let (vault_id, reserves, _x) = vault_after_one_trade(&owner_dev, &pc_a, &pc_b, false); + assert_eq!(leaves(owner, &vault_id, &pc_a, &pc_b), (10_000, 5_000, 0)); + + let rt = crate::runtime::get_runtime(); + let composed = rt + .block_on(super::compose_own_vault(&vault_id)) + .expect("the owner composes its own vault"); + assert_eq!( + composed.sequence, 1, + "the market moved the vault a generation" + ); + // A signed close of `state` at its own generation, with the commitment + // of its drained successor — exactly what a caller below the gate could + // hand the commit. + let close_of = |state: &dsm::ccb::VaultStateV2, c_n: [u8; 32]| { + let next = match dsm::dlv::successor_validity::derive_close_successor(state, c_n) { + dsm::dlv::successor_validity::DeriveExpected::Derived(v) => *v, + dsm::dlv::successor_validity::DeriveExpected::Refused(r) => { + panic!("the successor predicate refused the close: {r}") + } + }; + let commitment = dsm::ccb::vault_state_commitment(&next).expect("c_{n+1}"); + let op = owner + .core_sdk + .sign_operation_sphincs(dsm::types::operations::Operation::DlvClose { + vault_id: vault_id.to_vec(), + leg_a_policy_commit: *state.market_policy.token_a(), + leg_a_amount: state.reserve_a, + leg_b_policy_commit: *state.market_policy.token_b(), + leg_b_amount: state.reserve_b, + parent_sequence: state.generation, + new_sequence: state.generation + 1, + fee_bps: state.fee_policy.fee_bps(), + signature: Vec::new(), + mode: dsm::types::operations::TransactionMode::Unilateral, + }) + .expect("sign the close"); + (commitment, op) + }; + let root = owner.core_sdk.device_head().expect("head").root(); + let spend = spendable(owner, &pc_a, &pc_b); + let nothing_written = |what: &str| { + assert_eq!( + owner.core_sdk.device_head().expect("head").root(), + root, + "{what}: the root did not move" + ); + assert_eq!( + spendable(owner, &pc_a, &pc_b), + spend, + "{what}: nothing was credited" + ); + assert_eq!( + leaves(owner, &vault_id, &pc_a, &pc_b), + (10_000, 5_000, 0), + "{what}: the leaves did not move" + ); + for g in [0u64, 1] { + assert!( + crate::storage::client_db::load_vault_generation_consumer(&vault_id, g) + .expect("load") + .is_none(), + "{what}: generation {g} was not claimed" + ); + } + }; + + // (1) The stale baseline: generation 0, which the market consumed. + let stale = composed + .folded_parents + .iter() + .find(|f| f.generation == 0) + .expect("the folded parent"); + let (commitment, op) = close_of(&stale.state, stale.c_n); + let e = rt + .block_on(owner.commit_canonical_close(&vault_id, &composed, &commitment, op)) + .expect_err("a close of the stale baseline"); + assert!( + e.contains("a realized market successor consumed generation 0"), + "the refusal names the erased successor: {e}" + ); + nothing_written("stale baseline"); + + // (2) The composed frontier, which the owner has not caught up to. + let (commitment, op) = close_of(&composed.state, composed.c_n); + let e = rt + .block_on(owner.commit_canonical_close(&vault_id, &composed, &commitment, op)) + .expect_err("a close of a frontier the owner has not caught up to"); + nothing_written(&format!("uncaught frontier ({e})")); + + // Caught up by the sync pass, the route closes it — admitted. + let n = rt + .block_on(owner.resume_owner_catch_up()) + .expect("the sync pass"); + assert_eq!(n, 1, "the one owed settlement is applied"); + let res = close(owner, &vault_id); + assert!( + res.success, + "the caught-up vault closes: {:?}", + res.error_message + ); + let after = spendable(owner, &pc_a, &pc_b); + assert_eq!(after, (spend.0 + reserves.0, spend.1 + reserves.1)); + + // THE PROCEEDS ARE IN R_econ. A second vault funded with more B than the + // owner held before the close is admitted: its sufficiency check reads + // the ADMITTED balances, which only an admitted close could have raised. + assert!(reserves.1 > 0, "the close returned some B"); + let second = crate::sdk::funded_vault_fixture::create_funded_amm_vault( + owner, + &pc_a, + &pc_b, + 1_000, + spend.1 + 1, + ); + assert_ne!(second, vault_id); + } + + /// `close_plan` TAKES EVERY FACT OF A CLOSE FROM THE COMPOSITION (G4). + /// + /// Pure, over one real composition: a funded vault one market generation + /// on. The exact frontier close plans, and its plan IS the composition's + /// parent, reserves, parent binding and storage set. Every other close is + /// refused by name: the stale baseline a realized successor consumed, a + /// skipped generation, an older parent with later generations realized, + /// altered reserves, another vault, and a parent another candidate holds + /// unrealized (an uncertified predecessor). + /// + /// MUTATION CONTROL: let `close_plan` fold from a MARKET-consumed parent and + /// the stale-baseline case goes red. + #[test] + #[serial] + fn close_plan_takes_every_fact_of_a_close_from_the_composition() { + install_identity(); + let owner_dev = participant("owner", 0x41); + let owner = owner_dev.router(); + let (pc_a, pc_b) = + crate::sdk::funded_vault_fixture::admitted_device_holding(owner, 55_000, 20_000); + let (vault_id, _reserves, _x) = vault_after_one_trade(&owner_dev, &pc_a, &pc_b, false); + let composed = crate::runtime::get_runtime() + .block_on(super::compose_own_vault(&vault_id)) + .expect("the owner composes its own vault"); + assert_eq!(composed.sequence, 1); + let s = composed.state.clone(); + let close = |parent: u64, ra: u64, rb: u64, vault: [u8; 32]| { + dsm::types::operations::Operation::DlvClose { + vault_id: vault.to_vec(), + leg_a_policy_commit: *s.market_policy.token_a(), + leg_a_amount: ra, + leg_b_policy_commit: *s.market_policy.token_b(), + leg_b_amount: rb, + parent_sequence: parent, + new_sequence: parent + 1, + fee_bps: s.fee_policy.fee_bps(), + signature: Vec::new(), + mode: dsm::types::operations::TransactionMode::Unilateral, + } + }; + + let plan = super::close_plan( + &vault_id, + &composed, + &close(1, s.reserve_a, s.reserve_b, vault_id), + ) + .expect("the exact frontier close plans"); + assert_eq!( + ( + plan.parent_sequence, + plan.new_sequence, + plan.reserve_a, + plan.reserve_b + ), + (1, 2, s.reserve_a, s.reserve_b) + ); + assert_eq!(plan.parent_binding, composed.c_n); + assert_eq!(plan.storage_set_id, composed.storage_set_id); + assert_eq!( + (plan.pair.a(), plan.pair.b()), + (*s.market_policy.token_a(), *s.market_policy.token_b()) + ); + + let refused = |what: &str, + c: &crate::sdk::vault_state_composition::ComposedVaultState, + op: dsm::types::operations::Operation, + needle: &str| { + match super::close_plan(&vault_id, c, &op) { + Ok(_) => panic!("{what} must not plan"), + Err(e) => assert!(e.contains(needle), "{what}: {e}"), + } + }; + refused( + "the stale baseline", + &composed, + close(0, 10_000, 5_000, vault_id), + "a realized market successor consumed generation 0", + ); + refused( + "a skipped generation", + &composed, + close(2, s.reserve_a, s.reserve_b, vault_id), + "beyond the composed frontier", + ); + refused( + "altered reserves", + &composed, + close(1, s.reserve_a + 1, s.reserve_b, vault_id), + "does not drain exactly", + ); + refused( + "another vault", + &composed, + close(1, s.reserve_a, s.reserve_b, [0xEE; 32]), + "does not drain exactly", + ); + let mut ahead = composed.clone(); + ahead.sequence = 3; + refused( + "an older parent with later generations realized", + &ahead, + close(1, s.reserve_a, s.reserve_b, vault_id), + "realized generations past 1", + ); + let mut held = composed.clone(); + held.frontier_binding = + crate::sdk::vault_state_composition::FrontierBinding::BoundUnrealized { + bundle_digest: [0x11; 32], + route_set_commitment: [0x22; 32], + }; + refused( + "an uncertified predecessor", + &held, + close(1, s.reserve_a, s.reserve_b, vault_id), + "uncertified predecessor", + ); + } + /// A CONTESTED PARENT. Exclusivity over a generation belongs to the quorum /// register, not to the owner: if a trader's claim is already at quorum on /// this parent, the close loses and must move nothing. The intent is 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 eb64a3bf..2b621fe7 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 @@ -803,9 +803,62 @@ pub(crate) async fn admitted_dlv_owner_apply( .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 +/// The owner's terminal close, admitted into `R_econ` (amendment 2c-G, G4). +/// +/// The close drains both vault reserve leaves into spendable balance. Its write +/// set reads the ADMITTED reserve leaves at exactly the parent generation and +/// funds each balance credit by the reserve it drains — two `0x0024` +/// same-transition moves the builder derives itself — so the facts are fixed at +/// `CreditSourceFacts::None` and are not a parameter. Admitting it is what makes +/// the proceeds real in the owner's economic lineage, spendable by the next +/// admitted operation, and what makes a close at a generation `R_econ` does not +/// hold unbuildable. +/// +/// Close authority stays the owner's and binding stays QuorumBind's: this runs +/// only through the one canonical close commit, after the route or the resume +/// pass has established both. +#[allow(clippy::too_many_arguments)] +pub(crate) async fn admitted_dlv_close( + core: &CoreSDK, + operation: Operation, + rel_key: [u8; 32], + counterparty_devid: [u8; 32], + initial_chain_tip: [u8; 32], + reserve_mutation: dsm::types::device_state::VaultReserveMutation, + 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::DlvClose { .. }) { + return Err(DsmError::invalid_operation( + "admitted_dlv_close takes a DlvClose", + )); + } + let staged = stage_admission(core, &operation, |_| { + Ok((CreditSourceFacts::None, Vec::new())) + }) + .await?; + admit_reserve_mutation( + core, + staged, + operation, + rel_key, + counterparty_devid, + initial_chain_tip, + reserve_mutation, + "close", + build_artifacts, + write_extra, + ) + .await +} + +/// The advance and admission shared by the three reserve-mutation facades — a +/// funded create, an owner apply and a close. 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)] diff --git a/lean4/DSMAdmittedClose.lean b/lean4/DSMAdmittedClose.lean new file mode 100644 index 00000000..b829f256 --- /dev/null +++ b/lean4/DSMAdmittedClose.lean @@ -0,0 +1,195 @@ +/- + The admitted terminal close — self-contained Lean 4 (no Mathlib, no imports) + + Machine-checks amendment 2c-G's G4 ruling over one vault: a close is admitted + at exactly the caught-up composed frontier, or it writes nothing. + + - CAUGHT UP a close requires the owner's admitted generation to be + the composed frontier: no close from a stale baseline + - EXACT PARENT a close consumes exactly the frontier generation: no + skipped generation, no already-consumed parent + - EXACT RESERVES it drains exactly the frontier's reserves + - NOT HELD a parent another candidate holds unrealized — an + uncertified predecessor — refuses the close + - NOTHING WRITTEN a refused close leaves the vault exactly as it was + - NEVER ERASES the realized history survives a close as a prefix + - TERMINAL a second close is refused + - CATCH-UP FIRST caught up to a free frontier, the exact close is + admitted + + The model. `history` is the composed vault's reserves at each generation, + oldest first; its last entry is the frontier's. `applied` is the owner's + admitted generation — where `R_econ`'s reserve leaves stand. `binding` is the + frontier's binding. The close's two checks are the implementation's two + layers: `planOk` is `close_plan` (every fact read off the composition) and + `admitOk` is the admission's write set (the reserve leaves at exactly the + parent generation). + + What this module does NOT claim: + + * Close authority, QuorumBind and the accepted-successor rules. Unchanged + by G4, and modelled where they live (DSMValidDlvSuccessor, + DSMSettlementCompletion); here the close is already authorized and bound. + * Catch-up itself. DSMOwnerCatchUp owns it; here it is `applied := frontier`. + * Reserves as two legs. One number per generation carries the argument. + + Mutation controls, executed rather than asserted — the kernel proving the + NEGATION of a named sample theorem: + + 1. the admission's caught-up precondition dropped + -> `a_close_of_an_uncaught_frontier_is_refused` is proved FALSE + 2. the held-parent check dropped + -> `a_held_parent_refuses_the_close_sample` is proved FALSE + 3. any parent at or below the frontier accepted, at its own reserves + -> `a_close_of_the_consumed_generation_is_refused` is proved FALSE + + All mutations were reverted; this file is the unmutated module. +-/ + +namespace DSMAdmittedClose + +inductive Binding where + | free + | ours + | heldByOther + deriving DecidableEq, Repr + +structure Vault where + /-- The composed reserves at each generation, oldest first. -/ + history : List Nat + /-- The owner's admitted generation. -/ + applied : Nat + /-- The frontier's binding. -/ + binding : Binding + closed : Bool + deriving DecidableEq, Repr + +structure Close where + parent : Nat + amount : Nat + deriving DecidableEq, Repr + +def frontier (v : Vault) : Nat := v.history.length - 1 + +def frontierReserves (v : Vault) : Nat := v.history.getLastD 0 + +/-- `close_plan`: the parent is the frontier, nobody else holds it, and the +amount is the frontier's. -/ +def planOk (v : Vault) (c : Close) : Bool := + !v.closed && c.parent == frontier v && v.binding != .heldByOther && + c.amount == frontierReserves v + +/-- The admission: `R_econ` holds exactly the parent generation. -/ +def admitOk (v : Vault) (c : Close) : Bool := v.applied == c.parent + +def closeOk (v : Vault) (c : Close) : Bool := planOk v c && admitOk v c + +/-- The one close commit: a terminal zero generation appended, or nothing. -/ +def commitClose (v : Vault) (c : Close) : Vault := + if closeOk v c then + { v with history := v.history ++ [0], applied := c.parent + 1, closed := true } + else v + +-- ───────────────────────────────────────────────────────────────────────────── +-- Lemmas +-- ───────────────────────────────────────────────────────────────────────────── + +theorem take_length_append (l₁ l₂ : List Nat) : (l₁ ++ l₂).take l₁.length = l₁ := by + induction l₁ with + | nil => simp + | cons a t ih => simp [ih] + +-- ───────────────────────────────────────────────────────────────────────────── +-- General statements +-- ───────────────────────────────────────────────────────────────────────────── + +/-- NOTHING WRITTEN: a refused close leaves the vault exactly as it was. -/ +theorem a_refused_close_writes_nothing (v : Vault) (c : Close) + (h : closeOk v c = false) : commitClose v c = v := by + simp [commitClose, h] + +/-- CAUGHT UP: an admitted close means the owner stood at the frontier. -/ +theorem a_close_requires_the_owner_caught_up (v : Vault) (c : Close) + (h : closeOk v c = true) : v.applied = frontier v := by + simp [closeOk, planOk, admitOk] at h + omega + +/-- EXACT PARENT: no skipped generation, no already-consumed parent. -/ +theorem a_close_consumes_exactly_the_frontier (v : Vault) (c : Close) + (h : closeOk v c = true) : c.parent = frontier v := by + simp [closeOk, planOk] at h + exact h.1.1.1.2 + +/-- EXACT RESERVES. -/ +theorem a_close_drains_exactly_the_frontier_reserves (v : Vault) (c : Close) + (h : closeOk v c = true) : c.amount = frontierReserves v := by + simp [closeOk, planOk] at h + exact h.1.2 + +/-- NOT HELD: an uncertified predecessor refuses the close. -/ +theorem a_held_parent_refuses_the_close (v : Vault) (c : Close) + (h : v.binding = .heldByOther) : closeOk v c = false := by + simp [closeOk, planOk, h] + +/-- NEVER ERASES: the realized history survives a close as a prefix. -/ +theorem a_close_never_erases_realized_history (v : Vault) (c : Close) : + (commitClose v c).history.take v.history.length = v.history := by + unfold commitClose + split + · exact take_length_append v.history [0] + · simp + +/-- TERMINAL: once a close is admitted, no further close is. -/ +theorem a_second_close_is_refused (v : Vault) (c c' : Close) + (h : closeOk v c = true) : closeOk (commitClose v c) c' = false := by + have hc : commitClose v c = + { v with history := v.history ++ [0], applied := c.parent + 1, closed := true } := by + unfold commitClose + rw [if_pos h] + rw [hc] + simp [closeOk, planOk] + +/-- CATCH-UP FIRST: caught up to a free frontier, the exact close is admitted. -/ +theorem a_caught_up_exact_close_is_admitted (v : Vault) + (hc : v.closed = false) (hb : v.binding ≠ .heldByOther) : + closeOk { v with applied := frontier v } ⟨frontier v, frontierReserves v⟩ = true := by + simp [closeOk, planOk, admitOk, frontier, frontierReserves, hc, hb] + +-- ───────────────────────────────────────────────────────────────────────────── +-- Samples — the statements above are not vacuous +-- ───────────────────────────────────────────────────────────────────────────── + +/-- Born at 100, moved to 120 by one realized market generation; the owner's +admitted generation is still 0. -/ +def traded : Vault := ⟨[100, 120], 0, .free, false⟩ + +theorem a_close_of_an_uncaught_frontier_is_refused : + closeOk traded ⟨1, 120⟩ = false := by decide + +theorem a_close_of_the_consumed_generation_is_refused : + closeOk traded ⟨0, 100⟩ = false := by decide + +theorem a_held_parent_refuses_the_close_sample : + closeOk { traded with applied := 1, binding := .heldByOther } ⟨1, 120⟩ = false := by + decide + +theorem a_caught_up_close_is_admitted_sample : + closeOk { traded with applied := 1 } ⟨1, 120⟩ = true := by decide + +theorem a_skipped_generation_is_refused : + closeOk { traded with applied := 2 } ⟨2, 0⟩ = false := by decide + +-- ───────────────────────────────────────────────────────────────────────────── +-- Axiom report +-- ───────────────────────────────────────────────────────────────────────────── + +#print axioms a_refused_close_writes_nothing +#print axioms a_close_requires_the_owner_caught_up +#print axioms a_close_consumes_exactly_the_frontier +#print axioms a_close_drains_exactly_the_frontier_reserves +#print axioms a_held_parent_refuses_the_close +#print axioms a_close_never_erases_realized_history +#print axioms a_second_close_is_refused +#print axioms a_caught_up_exact_close_is_admitted + +end DSMAdmittedClose