From 2fe27a89d2c50613b42a63ef9bf65a445858aadf Mon Sep 17 00:00:00 2001 From: Cryptskii <47649969+cryptskii@users.noreply.github.com> Date: Mon, 21 Sep 2026 04:05:41 -0400 Subject: [PATCH] sofi: R11, the exercise The value written to every successor key of a route: `SofiExercise` (class 0x005E; 0x005D went to the native-reserve credit source in R4), carrying the signed envelopes of F and P, P(E), every G_j and every closure object, bounded by a member's cell cap. Core `sofi::exercise`: the parts rebuild and bind to one another (`recognize_exercise`); an object naming K^(a) of v at R_n is an exercise whose F names (v, a) and whose P names (v, R_n), anything else at the key being nothing (`exercise_names_key`, P1); the ladder's SuccessorResolution from the cell (`attempt_resolution`). SDK `sofi_exercise`: `build_exercise` over the evidence conformance was decided on, `write_exercise` to every leg's cell leader-first under the vault's storage seed, `read_attempt_cell`. The signed two-leg route rig moves into the shared fixtures. Lean `namesKey`/`occupant` with two theorems (mutation 8 executed); the TLA exercise faults re-executed. G1: `successor_attempt_key` burned; `next_attempt`/`next_generation` retagged. --- ci/sofi_reachability_baseline.txt | 5 +- .../dsm/src/ccb/mod.rs | 8 + .../dsm/src/sofi/exercise.rs | 367 ++++++++++++++++++ .../dsm/src/sofi/mod.rs | 4 +- .../dsm/src/sofi/wire/mod.rs | 11 + .../dsm/src/sofi/wire/objects.rs | 148 ++++++- .../dsm_sdk/src/sdk/mod.rs | 1 + .../dsm_sdk/src/sdk/sofi_exercise.rs | 342 ++++++++++++++++ .../dsm_sdk/src/sdk/sofi_register.rs | 149 +------ .../dsm_sdk/src/sdk/sofi_test_fixtures.rs | 148 +++++++ lean4/DSMSofiSuccessorCells.lean | 76 ++++ 11 files changed, 1109 insertions(+), 150 deletions(-) create mode 100644 dsm_client/deterministic_state_machine/dsm/src/sofi/exercise.rs create mode 100644 dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_exercise.rs diff --git a/ci/sofi_reachability_baseline.txt b/ci/sofi_reachability_baseline.txt index 29cffae48..5a5acca5a 100644 --- a/ci/sofi_reachability_baseline.txt +++ b/ci/sofi_reachability_baseline.txt @@ -4,7 +4,6 @@ # this file only shrinks, except that a Core-only step landing a predicate # ahead of the steps that call it adds that one line (R7); R14 deletes the # file and G1 passes with no exceptions. -dsm_client/deterministic_state_machine/dsm/src/sofi/derive.rs successor_attempt_key # R11 dsm_client/deterministic_state_machine/dsm/src/sofi/lineage.rs advance_resolved # R13 dsm_client/deterministic_state_machine/dsm/src/sofi/lineage.rs genesis_accepted # R14 dsm_client/deterministic_state_machine/dsm/src/sofi/resolution.rs effect_of # R12 @@ -14,5 +13,5 @@ dsm_client/deterministic_state_machine/dsm/src/sofi/smt/fold.rs verify_batch # dsm_client/deterministic_state_machine/dsm/src/sofi/smt/tree.rs commit_shadow # R13 dsm_client/deterministic_state_machine/dsm/src/sofi/smt/tree.rs prove # R13 dsm_client/deterministic_state_machine/dsm/src/sofi/validation.rs route_validation # R12: the verdict wrapper the resolution ladder consumes; the producer takes the reason from `validate` -dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs next_attempt # R11 -dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs next_generation # R11 +dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs next_attempt # R12: the walk advances the attempt counter; R11 takes the attempts from F +dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs next_generation # R13: the resolved vault state's successor generation diff --git a/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs index 1c8d1a0ed..cb2169854 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/ccb/mod.rs @@ -233,6 +233,14 @@ pub mod class { /// canonical body, so a different valid signature encoding over the same /// body is the same object, not a second one. pub const SOFI_SIGNED_OBJECT: u16 = 0x005C; + /// The exercise (Section 17.5, rebuild step R11): the value written to + /// every successor key of a route β€” the signed envelope of `F`, the + /// signed envelope of `P`, `P(E)`, every `G_j` in leg order, and every + /// object `π’ž_E^pre` references. It proves itself from its own bytes and + /// state the reader already holds, and names its own attempt, so it + /// cannot count at another key. `0x005D` is the native-reserve credit + /// source (R4), which is why this is `0x005E`. + pub const SOFI_EXERCISE: u16 = 0x005E; } /// Discriminants **allocated but not encodable** β€” see [`class`] for the ones diff --git a/dsm_client/deterministic_state_machine/dsm/src/sofi/exercise.rs b/dsm_client/deterministic_state_machine/dsm/src/sofi/exercise.rs new file mode 100644 index 000000000..1db39352e --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm/src/sofi/exercise.rs @@ -0,0 +1,367 @@ +// SPDX-License-Identifier: Apache-2.0 + +//! Section 17.5, rebuild step R11: the exercise, and what counts at a +//! successor key. +//! +//! The value written to each successor key of a route is one canonical +//! object, [`SofiExercise`], carrying the signed envelope of `F`, the signed +//! envelope of `P`, `P(E)`, every `G_j` and every closure object. At the key +//! `K^(a)` of vault `v` at parent `R_n`, the value that counts is the first +//! exercise at the leader whose `F` names `(v, a)` in its attempts and whose +//! `P` names `(v, R_n)` in its legs β€” everything else at the key counts as +//! nothing (P1, OnlyExercisesCount). An exercise cannot exist unless the +//! trader exercised, because it carries `F`, which only the trader can sign; +//! everything else in it is bound to `F` by hashed preimages; and it names +//! its own attempt, so it cannot count at another key. +//! +//! Recognition establishes that the bytes ARE an exercise naming the key. It +//! is not validation: whether the route it carries realizes is the ladder's +//! question (rebuild step R12), answered from the same bytes. + +use super::arith::{CellResolution, ObjectResolution}; +use super::derive; +use super::publication::{ + recognize_policy_fulfillment, recognize_precommit, recognize_fulfillment, Signed, +}; +use super::wire::{ + DlvPolicyFulfillmentBody, SettlementPreimage, SofiExercise, TraderFulfillmentBody, + TraderPrecommitBody, +}; + +type D32 = [u8; 32]; + +/// An exercise whose bytes rebuilt into the objects it carries, bound to one +/// another: `F` is `P`'s, `P(E)` recomputes `P`'s `E`, the witnesses are the +/// set `F` commits. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct RecognizedExercise { + pub fulfillment: Signed, + pub precommit: Signed, + pub preimage: SettlementPreimage, + pub witnesses: Vec, + pub closure: Vec>, + /// `E`, as `P` commits it and `P(E)` recomputes it. + pub external_commitment: D32, +} + +/// Rebuild the objects an exercise carries and check their binding to one +/// another. `None` for bytes that are not one exercise of one operation. +pub fn recognize_exercise(bytes: &[u8]) -> Option { + let exercise = SofiExercise::decode(bytes).ok()?; + let (_, fulfillment) = recognize_fulfillment(exercise.fulfillment())?; + let (pid, precommit) = recognize_precommit(exercise.precommit())?; + if *fulfillment.body.precommit_id() != pid { + return None; + } + let preimage = SettlementPreimage::decode(exercise.preimage()).ok()?; + let e = derive::recompute_e(&preimage).ok()?; + if e != *precommit.body.external_commitment() { + return None; + } + // The witnesses are P's own, one per leg in leg order, and together they + // are exactly the set F commits. + if exercise.witnesses().len() != precommit.body.legs().len() { + return None; + } + let mut witnesses = Vec::with_capacity(exercise.witnesses().len()); + let mut ids = Vec::with_capacity(exercise.witnesses().len()); + for (leg, w) in precommit.body.legs().iter().zip(exercise.witnesses()) { + let (id, body) = recognize_policy_fulfillment(w)?; + if body.precommit_id != pid + || body.external_commitment != e + || body.vault_id != leg.vault_id + || body.parent_root != leg.parent_root + { + return None; + } + ids.push(id); + witnesses.push(body); + } + ids.sort(); + if fulfillment.body.policy_fulfillment_set() != ids.as_slice() { + return None; + } + if exercise.closure().len() != preimage.settlement().closure().refs().len() { + return None; + } + Some(RecognizedExercise { + fulfillment, + precommit, + preimage, + witnesses, + closure: exercise.closure().to_vec(), + external_commitment: e, + }) +} + +/// An object naming the successor key `K^(attempt)` of `vault_id` at +/// `parent_root`: an exercise whose `F` names `(vault_id, attempt)` and +/// whose `P` names `(vault_id, parent_root)`. Anything else at the key is +/// nothing β€” neither a rival nor a winner, however early it arrived. +pub fn exercise_names_key( + bytes: &[u8], + vault_id: &D32, + parent_root: &D32, + attempt: u64, +) -> Option { + let recognized = recognize_exercise(bytes)?; + let names_attempt = recognized + .fulfillment + .body + .attempts() + .iter() + .any(|a| a.vault_id == *vault_id && a.attempt == attempt); + let names_parent = recognized + .precommit + .body + .legs() + .iter() + .any(|l| l.vault_id == *vault_id && l.parent_root == *parent_root); + (names_attempt && names_parent).then_some(recognized) +} + +/// `SuccessorResolution(K)` (Section 23.1) as the ladder reads it: the cell's +/// resolution over the recognized view, carrying the `E` of the exercise +/// that won β€” `Final(E)`, `LeaderHeld(E)`, or `Unresolved` β€” and the +/// exercise itself when there is one. A cell whose leader holds no exercise +/// naming the key is open; an unread leader establishes nothing; both are +/// `Unresolved`, and no key is ever dead. +pub fn attempt_resolution( + objects: &ObjectResolution, + vault_id: &D32, + parent_root: &D32, + attempt: u64, +) -> (CellResolution, Option) { + let recognized = |bytes: &Vec| exercise_names_key(bytes, vault_id, parent_root, attempt); + match objects { + ObjectResolution::Final(bytes) => match recognized(bytes) { + Some(x) => (CellResolution::Final(x.external_commitment), Some(x)), + None => (CellResolution::Unresolved, None), + }, + ObjectResolution::LeaderHeld(bytes) => match recognized(bytes) { + Some(x) => (CellResolution::LeaderHeld(x.external_commitment), Some(x)), + None => (CellResolution::Unresolved, None), + }, + ObjectResolution::Open | ObjectResolution::Unavailable => { + (CellResolution::Unresolved, None) + } + } +} + +#[cfg(test)] +#[allow(clippy::disallowed_methods)] // test asserts; a failure here is the signal +mod tests { + use super::*; + use crate::ccb::sigalg::SPHINCS_PLUS_SPX256F as ALG; + use crate::sofi::conformance::derive_policy_fulfillments; + use crate::sofi::derive::precommit_id; + use crate::sofi::publication::Publication; + use crate::sofi::validation::fixtures::{swap_fixture_n, Fixture}; + use crate::sofi::wire::AttemptEntry; + + const KEY: [u8; 64] = [0x31; 64]; + const SIG: [u8; 8] = [0x77; 8]; + + /// One two-leg operation as an exercise: F over attempts (0, 1), the + /// canonical witnesses over the shadows P(E) commits, no closure. + fn exercise( + f: &Fixture, + attempts: &[u64], + ) -> (SofiExercise, TraderPrecommitBody, TraderFulfillmentBody) { + let p = &f.precommit; + let canonical = derive::canonical_legs(&f.preimage).unwrap(); + let shadows: Vec = p + .legs() + .iter() + .map(|leg| { + canonical + .iter() + .find(|l| l.vault_id == leg.vault_id) + .unwrap() + .shadow_core + }) + .collect(); + let witnesses = derive_policy_fulfillments(p, &shadows).unwrap(); + let mut set: Vec = witnesses + .iter() + .map(derive::policy_fulfillment_id) + .collect(); + set.sort(); + let fb = TraderFulfillmentBody::new( + precommit_id(p), + set, + p.legs() + .iter() + .zip(attempts) + .map(|(l, a)| AttemptEntry { + vault_id: l.vault_id, + attempt: *a, + }) + .collect(), + p.position() + 1, + ALG, + &KEY, + ) + .unwrap(); + let x = SofiExercise::new( + Publication::Fulfillment { + body: &fb, + signature: &SIG, + } + .object_bytes() + .unwrap(), + Publication::Precommit { + body: p, + signature: &SIG, + } + .object_bytes() + .unwrap(), + f.preimage.encode().unwrap(), + witnesses + .iter() + .map(DlvPolicyFulfillmentBody::encode) + .collect(), + Vec::new(), + ) + .unwrap(); + (x, p.clone(), fb) + } + + #[test] + fn an_exercise_round_trips_and_rebuilds_into_bound_objects() { + let f = swap_fixture_n(2); + let (x, p, fb) = exercise(&f, &[0, 1]); + let bytes = x.encode(); + assert_eq!(SofiExercise::decode(&bytes).unwrap(), x); + let r = recognize_exercise(&bytes).unwrap(); + assert_eq!(r.fulfillment.body, fb); + assert_eq!(r.precommit.body, p); + assert_eq!(r.preimage, f.preimage); + assert_eq!(r.external_commitment, *p.external_commitment()); + assert_eq!(r.witnesses.len(), 2); + } + + /// P1: an exercise names exactly the keys its F and P name. The same + /// bytes count at `(v_0, R_0, 0)` and `(v_1, R_1, 1)` and nowhere else β€” + /// not at another attempt of the same vault, not at another parent, not + /// at a vault the route does not touch. + #[test] + fn an_exercise_names_exactly_the_keys_its_fulfillment_and_precommit_name() { + let f = swap_fixture_n(2); + let (x, p, _) = exercise(&f, &[0, 1]); + let bytes = x.encode(); + let legs = p.legs(); + assert!(exercise_names_key(&bytes, &legs[0].vault_id, &legs[0].parent_root, 0).is_some()); + assert!(exercise_names_key(&bytes, &legs[1].vault_id, &legs[1].parent_root, 1).is_some()); + assert!(exercise_names_key(&bytes, &legs[0].vault_id, &legs[0].parent_root, 1).is_none()); + assert!(exercise_names_key(&bytes, &legs[1].vault_id, &legs[1].parent_root, 0).is_none()); + assert!(exercise_names_key(&bytes, &legs[0].vault_id, &[0x99; 32], 0).is_none()); + assert!(exercise_names_key(&bytes, &[0x98; 32], &legs[0].parent_root, 0).is_none()); + assert!(exercise_names_key( + b"not an exercise", + &legs[0].vault_id, + &legs[0].parent_root, + 0 + ) + .is_none()); + } + + /// The objects inside are bound to one another by hashed preimages: an + /// F of another P, a preimage that is not P(E), a witness set that is not + /// the one F commits β€” none of these is an exercise. + #[test] + fn an_exercise_whose_parts_are_not_one_operations_is_nothing() { + let f = swap_fixture_n(2); + let (x, p, fb) = exercise(&f, &[0, 1]); + let other = swap_fixture_n(1); + let (ox, _, _) = exercise(&other, &[0]); + // F of another P. + let bent = SofiExercise::new( + ox.fulfillment().to_vec(), + x.precommit().to_vec(), + x.preimage().to_vec(), + x.witnesses().to_vec(), + Vec::new(), + ) + .unwrap(); + assert!(recognize_exercise(&bent.encode()).is_none()); + // A preimage that is not this P's. + let bent = SofiExercise::new( + x.fulfillment().to_vec(), + x.precommit().to_vec(), + other.preimage.encode().unwrap(), + x.witnesses().to_vec(), + Vec::new(), + ) + .unwrap(); + assert!(recognize_exercise(&bent.encode()).is_none()); + // One witness swapped for another leg's: its leg binding is wrong. + let mut ws = x.witnesses().to_vec(); + ws.swap(0, 1); + let bent = SofiExercise::new( + x.fulfillment().to_vec(), + x.precommit().to_vec(), + x.preimage().to_vec(), + ws, + Vec::new(), + ) + .unwrap(); + assert!(recognize_exercise(&bent.encode()).is_none()); + // A witness bound to the right leg, P and E but claiming another + // shadow: only the set F commits β€” the ids β€” catches it, because the + // shadow is not in the leg binding. Mutation: drop the set check. + let mut wrong_shadow = DlvPolicyFulfillmentBody::decode(&x.witnesses()[0]).unwrap(); + wrong_shadow.shadow_core = [0xEE; 32]; + let mut ws = x.witnesses().to_vec(); + ws[0] = wrong_shadow.encode(); + let bent = SofiExercise::new( + x.fulfillment().to_vec(), + x.precommit().to_vec(), + x.preimage().to_vec(), + ws, + Vec::new(), + ) + .unwrap(); + assert!(recognize_exercise(&bent.encode()).is_none()); + let _ = (p, fb); + } + + /// The ladder's read of a successor key: the E of the exercise that won, + /// final or leader-held; anything that names no exercise for the key β€” + /// an open cell, an unread leader, bytes the recognizer refuses β€” is + /// unresolved, and no key is dead. + #[test] + fn a_successor_key_resolves_to_the_e_of_the_exercise_that_names_it_or_stays_open() { + let f = swap_fixture_n(2); + let (x, p, _) = exercise(&f, &[0, 1]); + let bytes = x.encode(); + let leg = &p.legs()[0]; + let e = *p.external_commitment(); + let (res, got) = attempt_resolution( + &ObjectResolution::Final(bytes.clone()), + &leg.vault_id, + &leg.parent_root, + 0, + ); + assert_eq!(res, CellResolution::Final(e)); + assert!(got.is_some()); + let (res, _) = attempt_resolution( + &ObjectResolution::LeaderHeld(bytes.clone()), + &leg.vault_id, + &leg.parent_root, + 0, + ); + assert_eq!(res, CellResolution::LeaderHeld(e)); + for objects in [ + ObjectResolution::Final(b"garbage".to_vec()), + ObjectResolution::Final(bytes.clone()), + ObjectResolution::Open, + ObjectResolution::Unavailable, + ] { + // the second one: right bytes, wrong attempt + let (res, got) = attempt_resolution(&objects, &leg.vault_id, &leg.parent_root, 7); + assert_eq!(res, CellResolution::Unresolved); + assert!(got.is_none()); + } + } +} diff --git a/dsm_client/deterministic_state_machine/dsm/src/sofi/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/sofi/mod.rs index 905898246..037781951 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/sofi/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/sofi/mod.rs @@ -24,7 +24,8 @@ //! ([`storage`]), three-valued validation composition and the mechanical //! fulfillment-against-precommit checks ([`conformance`]), what a producer //! publishes and how a reader recognizes it ([`publication`]), the exercise -//! boundary derived from the two position cells ([`registration`]), and the +//! boundary derived from the two position cells ([`registration`]), the +//! exercise object and what counts at a successor key ([`exercise`]), and the //! persistent DLV tree with structurally shared shadows ([`smt`]). //! //! ## What it is not @@ -38,6 +39,7 @@ pub mod admission; pub mod arith; pub mod conformance; pub mod derive; +pub mod exercise; pub mod fisher_yates; pub mod leader; pub mod lineage; diff --git a/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs b/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs index 108caf6fb..b6027039c 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/mod.rs @@ -97,6 +97,14 @@ //! Both leaf values are `H(vault-leaf-state/v1 β€– CCB(leaf))`. One tag is safe //! because the leaf's own envelope is inside the preimage. //! +//! `0x005E SofiExercise` (the value at a successor key, Section 17.5): 1 +//! `fulfillment` var bytes (a `0x005C` envelope over `F`) Β· 2 `precommit` var +//! bytes (a `0x005C` envelope over `P`) Β· 3 `preimage` var bytes (`0x0059`) Β· +//! 4 `witnesses` `seq` of `0x0038`, `1..=CANONICAL_MAX_LEGS`, in +//! P's leg order Β· 5 `closure` `seq`, `0..=MAX_CLOSURE_REFS`, in +//! `π’ž_E^pre` reference order. The whole object is bounded by +//! `MAX_EXERCISE_BYTES`, a member's cell value cap. +//! //! `0x004D TraderRelationshipLeaf` (the `R_econ` leaf state, at `k_{T,v}`): //! 1 `vault_id` digest32 Β· 2 `leaf` digest32 (`hΚ²`). //! @@ -202,6 +210,9 @@ pub const VAULT_STATUS_RETIRED: u16 = 0x0002; /// Distinct `ValidationRef` values in one closure; duplicates are malformed. pub const MAX_CLOSURE_REFS: usize = 64; +/// The largest exercise a member's cell takes (`MAX_CELL_VALUE_BYTES` at the +/// node). Two SPHINCS+ envelopes and a beta preimage sit well inside it. +pub const MAX_EXERCISE_BYTES: usize = 256 * 1024; /// Canonical encoded bytes of one referenced object (transport excluded). pub const MAX_CLOSURE_OBJECT_BYTES: usize = 256 * 1024; /// Authorization envelopes one candidate may require. diff --git a/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/objects.rs b/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/objects.rs index 63f2bd78d..b04129bb7 100644 --- a/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/objects.rs +++ b/dsm_client/deterministic_state_machine/dsm/src/sofi/wire/objects.rs @@ -9,7 +9,7 @@ use crate::ccb::{class, push_bytes, push_digest32, push_u16, push_u32, push_u64, use crate::economic::tree::ECONOMIC_SMT_HEIGHT; use super::{ - SofiWireError, CANONICAL_MAX_LEGS, MAX_CLOSURE_REFS, MAX_CORE_ENTRIES, + SofiWireError, CANONICAL_MAX_LEGS, MAX_CLOSURE_REFS, MAX_CORE_ENTRIES, MAX_EXERCISE_BYTES, MAX_SETTLEMENT_PREIMAGE_BYTES, ROUTE_MIN_LEGS, VAULT_STATUS_ACTIVE, VAULT_STATUS_RETIRED, }; @@ -754,6 +754,152 @@ fn read_var_bytes(c: &mut Cursor<'_>, max: usize) -> Result, DecodeError // ── ValidationRef: 0x003D..=0x0040 ───────────────────────────────────────── +// ── 0x005E SofiExercise ───────────────────────────────────────────────────── + +/// The exercise: the value written to every successor key of a route +/// (Section 17.5). Everything a reader needs to classify it is inside β€” `F` +/// and `P` in the envelopes their signatures travel in, `P(E)`, the witnesses +/// and the closure objects β€” and everything is bound to `F` by hashed +/// preimages. It names its own attempt through `F` and its own parents +/// through `P`, so it cannot count at another key. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SofiExercise { + fulfillment: Vec, + precommit: Vec, + preimage: Vec, + witnesses: Vec>, + closure: Vec>, +} + +const MAX_EXERCISE_PART_BYTES: usize = MAX_SETTLEMENT_PREIMAGE_BYTES + MAX_SIGNATURE_BYTES; + +impl SofiExercise { + /// The only constructor. Each part is the canonical bytes of the object + /// it carries; the codec bounds the parts and the whole. What the parts + /// MEAN β€” that the envelopes decode, that `F` is `P`'s, that the + /// witnesses are the canonical set β€” is recognition (`sofi::exercise`), + /// not construction. + pub fn new( + fulfillment: Vec, + precommit: Vec, + preimage: Vec, + witnesses: Vec>, + closure: Vec>, + ) -> Result { + for (field, bytes) in [ + ("fulfillment", &fulfillment), + ("precommit", &precommit), + ("preimage", &preimage), + ] { + if bytes.is_empty() || bytes.len() > MAX_EXERCISE_PART_BYTES { + return Err(SofiWireError::ObjectTooLarge { + field, + bytes: bytes.len(), + max: MAX_EXERCISE_PART_BYTES, + }); + } + } + check_count("witnesses", 1, CANONICAL_MAX_LEGS, witnesses.len())?; + check_count("closure objects", 0, MAX_CLOSURE_REFS, closure.len())?; + for (field, list) in [("witness", &witnesses), ("closure object", &closure)] { + for bytes in list { + if bytes.is_empty() || bytes.len() > MAX_EXERCISE_PART_BYTES { + return Err(SofiWireError::ObjectTooLarge { + field, + bytes: bytes.len(), + max: MAX_EXERCISE_PART_BYTES, + }); + } + } + } + let v = Self { + fulfillment, + precommit, + preimage, + witnesses, + closure, + }; + let total = v.encode().len(); + if total > MAX_EXERCISE_BYTES { + return Err(SofiWireError::ObjectTooLarge { + field: "exercise", + bytes: total, + max: MAX_EXERCISE_BYTES, + }); + } + Ok(v) + } + + pub fn fulfillment(&self) -> &[u8] { + &self.fulfillment + } + + pub fn precommit(&self) -> &[u8] { + &self.precommit + } + + pub fn preimage(&self) -> &[u8] { + &self.preimage + } + + pub fn witnesses(&self) -> &[Vec] { + &self.witnesses + } + + pub fn closure(&self) -> &[Vec] { + &self.closure + } + + pub fn encode(&self) -> Vec { + let mut out = Vec::new(); + push_env(&mut out, class::SOFI_EXERCISE); + let _ = push_bytes(&mut out, &self.fulfillment); + let _ = push_bytes(&mut out, &self.precommit); + let _ = push_bytes(&mut out, &self.preimage); + push_u32(&mut out, self.witnesses.len() as u32); + for w in &self.witnesses { + let _ = push_bytes(&mut out, w); + } + push_u32(&mut out, self.closure.len() as u32); + for o in &self.closure { + let _ = push_bytes(&mut out, o); + } + out + } + + pub fn decode(bytes: &[u8]) -> Result { + if bytes.len() > MAX_EXERCISE_BYTES { + return Err(DecodeError::Invalid(format!( + "exercise of {} bytes exceeds {MAX_EXERCISE_BYTES}", + bytes.len() + ))); + } + let mut c = Cursor { b: bytes, i: 0 }; + c.envelope(class::SOFI_EXERCISE, SCHEMA_V1)?; + let fulfillment = read_var_bytes(&mut c, MAX_EXERCISE_PART_BYTES)?; + let precommit = read_var_bytes(&mut c, MAX_EXERCISE_PART_BYTES)?; + let preimage = read_var_bytes(&mut c, MAX_EXERCISE_PART_BYTES)?; + let n = read_count(&mut c, "witnesses", 1, CANONICAL_MAX_LEGS)?; + let mut witnesses = Vec::with_capacity(n); + for _ in 0..n { + witnesses.push(read_var_bytes(&mut c, MAX_EXERCISE_PART_BYTES)?); + } + let m = read_count(&mut c, "closure objects", 0, MAX_CLOSURE_REFS)?; + let mut closure = Vec::with_capacity(m); + for _ in 0..m { + closure.push(read_var_bytes(&mut c, MAX_EXERCISE_PART_BYTES)?); + } + let v = Self { + fulfillment, + precommit, + preimage, + witnesses, + closure, + }; + finish(&c, v) + } +} + /// One typed validation reference. Each variant has exactly one fetch and /// verification rule, and randomized signature envelopes are never /// content-bound. 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 3987edce4..8de37b41b 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 @@ -60,6 +60,7 @@ pub mod counterparty_genesis_helpers; pub mod device_admission_sdk; pub mod dlv_sdk; /// SoFi v8 producers: setup, vault creation, trade, route and close. +pub mod sofi_exercise; pub mod sofi_publish; pub mod sofi_register; pub mod sofi_sdk; diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_exercise.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_exercise.rs new file mode 100644 index 000000000..e3d2d57f9 --- /dev/null +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_exercise.rs @@ -0,0 +1,342 @@ +// SPDX-License-Identifier: Apache-2.0 + +//! Section 17.5 and stage 8 of Β§31, rebuild step R11: the exercise, written +//! to every successor key of a route and read back as the ladder reads it. +//! +//! After `F` registers, any party MAY write the exercise (P2): the object +//! carries `F`, which only the trader could sign, and everything else in it +//! is bound to `F` by hashed preimages, so a relayer adds nothing and can +//! forge nothing. Each leg's cell is `K^(a_j)` of vault `v_j` at parent +//! `R_j`, written leader-first under the vault's storage seed (Part II Β§8); +//! the member stores bytes and decides nothing. What counts at a key is +//! Core's (`sofi::exercise::exercise_names_key`): the first exercise at the +//! leader whose `F` names `(v, a)` and whose `P` names `(v, R_n)`. + +use dsm::common::domain_tags::TAG_DSM_SOFI_SUCC_CELL_V2; +use dsm::sofi::arith::{resolve_objects, CellResolution}; +use dsm::sofi::conformance::{derive_policy_fulfillments, ConformanceEvidence}; +use dsm::sofi::derive; +use dsm::sofi::exercise::{attempt_resolution, exercise_names_key, RecognizedExercise}; +use dsm::sofi::publication::Publication; +use dsm::sofi::wire::{DlvPolicyFulfillmentBody, SofiExercise}; +use dsm::types::error::DsmError; + +use crate::sdk::sofi_register::InstallRequest; +use crate::sdk::storage_io::{read_cell_raw, successor_cell_leader_index, write_cell_leader_first}; +use crate::sdk::storage_set::StorageSet; + +type D32 = [u8; 32]; + +fn err(what: &str, e: impl core::fmt::Display) -> DsmError { + DsmError::verification(format!("{what}: {e}")) +} + +/// The exercise of a request, over the evidence its conformance was decided +/// on: `F` and `P` in their envelopes, `P(E)`, the canonical witnesses +/// derived from `P` and the shadows `P(E)` commits, and every closure object +/// in reference order. A closure object the evidence does not hold is an +/// error here β€” the exercise carries the closure, so it cannot be built +/// without it. +pub fn build_exercise( + request: &InstallRequest<'_>, + evidence: &ConformanceEvidence, +) -> Result { + let canonical = + derive::canonical_legs(request.preimage).map_err(|e| err("canonical legs", e))?; + let shadows: Vec = request + .precommit + .legs() + .iter() + .map(|leg| { + canonical + .iter() + .find(|l| l.vault_id == leg.vault_id) + .map(|l| l.shadow_core) + .ok_or_else(|| err("witnesses", "a leg P(E) does not derive")) + }) + .collect::>()?; + let witnesses: Vec> = derive_policy_fulfillments(request.precommit, &shadows) + .map_err(|e| err("witnesses", format!("{e:?}")))? + .iter() + .map(DlvPolicyFulfillmentBody::encode) + .collect(); + let mut closure = Vec::new(); + for reference in request.preimage.settlement().closure().refs() { + let bytes = evidence + .closure + .get(reference) + .ok_or_else(|| err("closure", format!("object not acquired for {reference:?}")))?; + closure.push(bytes.clone()); + } + SofiExercise::new( + Publication::Fulfillment { + body: request.fulfillment, + signature: request.fulfillment_signature, + } + .object_bytes() + .map_err(|e| err("fulfillment envelope", e))?, + Publication::Precommit { + body: request.precommit, + signature: request.precommit_signature, + } + .object_bytes() + .map_err(|e| err("precommit envelope", e))?, + request.preimage.encode().map_err(|e| err("preimage", e))?, + witnesses, + closure, + ) + .map_err(|e| err("exercise", e)) +} + +/// One leg's cell write. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct LegWrite { + pub vault_id: D32, + pub parent_root: D32, + pub attempt: u64, + pub key: D32, + pub leader_reached: bool, + pub copies: u32, +} + +/// Write `exercise` to every successor key its `F` names β€” `K^(a_j)` of +/// `v_j` at the parent `R_j` its `P` names β€” the leader of each vault's +/// storage seed first, the other members after. Nothing is checked at the +/// member; the bytes are the same everywhere. +pub async fn write_exercise( + set: &StorageSet, + exercise: &SofiExercise, + recognized: &RecognizedExercise, +) -> Result, DsmError> { + let bytes = exercise.encode(); + let mut writes = Vec::new(); + for attempt in recognized.fulfillment.body.attempts() { + let leg = recognized + .precommit + .body + .legs() + .iter() + .find(|l| l.vault_id == attempt.vault_id) + .ok_or_else(|| err("exercise", "an attempt names a vault P has no leg for"))?; + let key = derive::successor_attempt_key(&leg.vault_id, &leg.parent_root, attempt.attempt); + let seed = derive::storage_seed(&leg.vault_id, &leg.parent_root); + let write = write_cell_leader_first( + set, + TAG_DSM_SOFI_SUCC_CELL_V2.source_bytes(), + &key, + &seed, + &bytes, + ) + .await?; + writes.push(LegWrite { + vault_id: leg.vault_id, + parent_root: leg.parent_root, + attempt: attempt.attempt, + key, + leader_reached: write.leader_reached, + copies: write.copies, + }); + } + Ok(writes) +} + +/// `SuccessorResolution(K^(attempt))` of `vault_id` at `parent_root`, as the +/// ladder reads it (Section 23.1): raw reads of the cell, the leader from the +/// vault's storage seed over the committed set, the recognized view +/// (`exercise_names_key`), then the `E` of the exercise that won, final or +/// leader-held, with the exercise itself. `Unresolved` for an open cell or an +/// unread leader; no key is ever dead. +pub async fn read_attempt_cell( + set: &StorageSet, + vault_id: &D32, + parent_root: &D32, + attempt: u64, +) -> Result<(CellResolution, Option), DsmError> { + let key = derive::successor_attempt_key(vault_id, parent_root, attempt); + let leader = successor_cell_leader_index(set, vault_id, parent_root)?; + let reads = read_cell_raw(set, TAG_DSM_SOFI_SUCC_CELL_V2.source_bytes(), &key).await?; + let objects = resolve_objects(&reads, leader, |bytes| { + exercise_names_key(bytes, vault_id, parent_root, attempt).is_some() + }) + .map_err(|e| err("cell read", e))?; + Ok(attempt_resolution(&objects, vault_id, parent_root, attempt)) +} + +#[cfg(test)] +#[allow(clippy::disallowed_methods)] // test asserts; a failure here is the signal +mod tests { + use dsm::sofi::exercise::recognize_exercise; + use serial_test::serial; + + use super::*; + use crate::sdk::sofi_register::{acquire_conformance_evidence, install_fulfillment}; + use crate::sdk::sofi_test_fixtures::{block_on, install_request, signed_route, SignedRoute}; + use crate::sdk::storage_io::fake_registers; + + fn succ_ns() -> &'static [u8] { + TAG_DSM_SOFI_SUCC_CELL_V2.source_bytes() + } + + /// The installed route's exercise, built over the evidence its + /// conformance was decided on. + fn exercise_of(r: &SignedRoute) -> (SofiExercise, RecognizedExercise) { + let req = install_request(r); + let ev = block_on(acquire_conformance_evidence(&r.set, &req)).unwrap(); + let x = build_exercise(&req, &ev).unwrap(); + let recognized = recognize_exercise(&x.encode()).unwrap(); + (x, recognized) + } + + fn members(set: &StorageSet) -> Vec { + set.members().iter().map(|m| m.member_id.clone()).collect() + } + + /// Stage 8 of Β§31: after registration, the exercise lands at every leg's + /// successor key, the leader of that vault's storage seed first and every + /// other member after, and each cell reads back final on the route's + /// one `E` with the exercise inside. + #[test] + #[serial] + fn an_exercise_is_written_to_every_successor_key_at_its_leader() { + let r = signed_route(true); + block_on(install_fulfillment(&r.set, &install_request(&r))).unwrap(); + let (x, recognized) = exercise_of(&r); + let writes = block_on(write_exercise(&r.set, &x, &recognized)).unwrap(); + assert_eq!(writes.len(), 2, "one cell per leg"); + let bytes = x.encode(); + for w in &writes { + assert!(w.leader_reached); + assert_eq!(w.copies, 4); + assert_eq!( + w.key, + derive::successor_attempt_key(&w.vault_id, &w.parent_root, w.attempt) + ); + assert_eq!( + fake_registers::holders(&r.set, succ_ns(), &w.key, &bytes), + members(&r.set) + ); + let (res, got) = block_on(read_attempt_cell( + &r.set, + &w.vault_id, + &w.parent_root, + w.attempt, + )) + .unwrap(); + assert_eq!( + res, + CellResolution::Final(*r.precommit.external_commitment()) + ); + assert_eq!( + got.as_ref().map(|g| &g.fulfillment.body), + Some(&r.fulfillment) + ); + } + } + + /// P1, OnlyExercisesCount: bytes that are not an exercise naming the key + /// β€” garbage, and an exercise whose F names another attempt of this + /// vault β€” count as nothing, however early they reached the leader. The + /// route's own exercise is the first RECOGNIZED object and is final. + #[test] + #[serial] + fn only_an_exercise_naming_the_key_counts() { + let r = signed_route(true); + block_on(install_fulfillment(&r.set, &install_request(&r))).unwrap(); + let (x, recognized) = exercise_of(&r); + let leg = &recognized.precommit.body.legs()[0]; + let key = derive::successor_attempt_key(&leg.vault_id, &leg.parent_root, 0); + let leader = successor_cell_leader_index(&r.set, &leg.vault_id, &leg.parent_root).unwrap(); + fake_registers::put_cell(&r.set, leader, succ_ns(), &key, b"not an exercise"); + // An exercise of the same route whose F names attempt 1 of this vault: + // it is an exercise, and it names another key. + let other = other_attempt(&r, 1); + fake_registers::put_cell(&r.set, leader, succ_ns(), &key, &other.encode()); + let (res, _) = block_on(read_attempt_cell( + &r.set, + &leg.vault_id, + &leg.parent_root, + 0, + )) + .unwrap(); + assert_eq!( + res, + CellResolution::Unresolved, + "nothing naming the key has arrived" + ); + block_on(write_exercise(&r.set, &x, &recognized)).unwrap(); + let (res, got) = block_on(read_attempt_cell( + &r.set, + &leg.vault_id, + &leg.parent_root, + 0, + )) + .unwrap(); + assert_eq!( + res, + CellResolution::Final(*r.precommit.external_commitment()) + ); + assert_eq!(got.map(|g| g.fulfillment.body), Some(r.fulfillment.clone())); + } + + /// An exercise cannot count at a key it does not name: written at + /// `K^(1)` of a leg whose attempt it names as 0, it is nothing there. + #[test] + #[serial] + fn an_exercise_cannot_count_at_another_key() { + let r = signed_route(true); + block_on(install_fulfillment(&r.set, &install_request(&r))).unwrap(); + let (x, recognized) = exercise_of(&r); + let leg = &recognized.precommit.body.legs()[0]; + let elsewhere = derive::successor_attempt_key(&leg.vault_id, &leg.parent_root, 1); + let leader = successor_cell_leader_index(&r.set, &leg.vault_id, &leg.parent_root).unwrap(); + fake_registers::put_cell(&r.set, leader, succ_ns(), &elsewhere, &x.encode()); + assert_eq!( + fake_registers::holders(&r.set, succ_ns(), &elsewhere, &x.encode()).len(), + 5, + "the member keeps what it is given" + ); + let (res, got) = block_on(read_attempt_cell( + &r.set, + &leg.vault_id, + &leg.parent_root, + 1, + )) + .unwrap(); + assert_eq!(res, CellResolution::Unresolved); + assert!(got.is_none()); + } + + /// The same route, exercised with every leg at `attempt`: another + /// fulfillment of the same P, signed by the trader. + fn other_attempt(r: &SignedRoute, attempt: u64) -> SofiExercise { + use crate::sdk::sofi_test_fixtures::trader_sign; + use dsm::sofi::wire::{AttemptEntry, TraderFulfillmentBody}; + let f = TraderFulfillmentBody::new( + *r.fulfillment.precommit_id(), + r.fulfillment.policy_fulfillment_set().to_vec(), + r.fulfillment + .attempts() + .iter() + .map(|a| AttemptEntry { + vault_id: a.vault_id, + attempt, + }) + .collect(), + r.fulfillment.position(), + r.fulfillment.signature_alg(), + r.fulfillment.claimant_public_key(), + ) + .unwrap(); + let sig = trader_sign(&derive::fulfillment_signing_digest(&f)); + let req = InstallRequest { + precommit: &r.precommit, + precommit_signature: &r.p_sig, + preimage: &r.preimage, + fulfillment: &f, + fulfillment_signature: &sig, + own_objects: &r.own, + }; + let ev = block_on(acquire_conformance_evidence(&r.set, &req)).unwrap(); + build_exercise(&req, &ev).unwrap() + } +} diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_register.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_register.rs index b0b04ba14..b34a015d9 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_register.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_register.rs @@ -301,158 +301,17 @@ pub async fn read_registration( #[cfg(test)] #[allow(clippy::disallowed_methods)] // test asserts; a failure here is the signal mod tests { - use std::sync::OnceLock; - use dsm::ccb::sigalg::SPHINCS_PLUS_SPX256F as ALG; - use dsm::crypto::sphincs::{generate_sphincs_keypair, sphincs_sign}; - use dsm::sofi::signature::SigningPayload; - use dsm::sofi::wire::{SofiResolutionClaim, SofiSetupBody}; - use dsm::types::operations::Operation; + use dsm::sofi::wire::SofiResolutionClaim; use serial_test::serial; use super::*; use crate::sdk::economic_registers::{read_economic_root_cell, register_economic_root}; - use crate::sdk::sofi_publish::publish_produced; - use crate::sdk::sofi_sdk::{build_fulfillment, draft_route, Produced, ToPublish}; use crate::sdk::sofi_test_fixtures::{ - all_policies, d, five, token, RouteFixture, DEV, G, OWNER_DEV, OWNER_G, P_CREATE, P_POS, + block_on, d, install_request as request, pair_bytes, signed_route as rig, + trader_keys as keys, trader_sign as sign, DEV, G, }; - use crate::sdk::storage_io::{fake_fleet, fake_registers, leader_index}; - - fn keys() -> &'static (Vec, Vec) { - static KEYS: OnceLock<(Vec, Vec)> = OnceLock::new(); - KEYS.get_or_init(|| generate_sphincs_keypair().unwrap()) - } - - fn sign(message: &[u8]) -> Vec { - sphincs_sign(&keys().1, message).unwrap() - } - - fn block_on(f: impl core::future::Future) -> T { - crate::runtime::get_runtime().block_on(f) - } - - /// A two-hop route whose legs carry the `ρ` of real setups, everything - /// published to the fake fleet β€” the setups too, when asked β€” and the - /// signed exercise ready to install. - struct Rig { - set: StorageSet, - precommit: TraderPrecommitBody, - p_sig: Vec, - preimage: SettlementPreimage, - fulfillment: TraderFulfillmentBody, - f_sig: Vec, - own: BTreeMap>, - setups: Vec, - } - - fn produced_setup(body: &SofiSetupBody) -> Produced { - Produced { - operation: Operation::SofiSetup { - setup_body: body.encode(), - signature: Vec::new(), - }, - signs: SigningPayload::SetupDigest(derive::setup_signing_digest(body)), - publish: vec![ToPublish::Setup(body.clone())], - } - } - - fn rig(publish_setups: bool) -> Rig { - fake_fleet::reset(); - fake_registers::reset(); - let set = five(); - let setups: Vec = (0..2) - .map(|j| { - let vault_id = derive::vault_id(&OWNER_G, &OWNER_DEV, P_CREATE + j as u64); - SofiSetupBody::new( - G, - DEV, - P_POS - 1, - vault_id, - d(0x0B), - d(0x0C), - ALG, - &keys().0, - ) - .unwrap() - }) - .collect(); - let rhos: Vec = setups.iter().map(derive::setup_ref).collect(); - let fx = RouteFixture::swap_with_setups( - 2, - set.id(), - |j| (token(j), token(j + 1)), - |j, _| rhos[j], - ); - fx.publish(&set, &all_policies()); - let evidence = fx.acquire(&set); - let draft = draft_route( - fx.hops.clone(), - fx.cores.clone(), - &fx.ctx(&keys().0), - fx.realize_root, - fx.void_root, - &evidence, - ) - .unwrap(); - let p_sig = sign(&draft.precommit_signing_digest()); - let attempts: Vec<(D32, u64)> = draft - .precommit() - .legs() - .iter() - .map(|l| (l.vault_id, 0)) - .collect(); - let produced = build_fulfillment(&draft, p_sig.clone(), &attempts).unwrap(); - let f_sig = sign(produced.signs.bytes()); - block_on(publish_produced(&set, &produced, &f_sig)).unwrap(); - if publish_setups { - for body in &setups { - let sig = sign(&derive::setup_signing_digest(body)); - block_on(publish_produced(&set, &produced_setup(body), &sig)).unwrap(); - } - } - let fulfillment = produced - .publish - .iter() - .find_map(|p| match p { - ToPublish::Fulfillment(f) => Some(f.clone()), - _ => None, - }) - .unwrap(); - Rig { - set, - precommit: draft.precommit().clone(), - p_sig, - preimage: draft.preimage().clone(), - fulfillment, - f_sig, - own: BTreeMap::new(), - setups, - } - } - - fn request(r: &Rig) -> InstallRequest<'_> { - InstallRequest { - precommit: &r.precommit, - precommit_signature: &r.p_sig, - preimage: &r.preimage, - fulfillment: &r.fulfillment, - fulfillment_signature: &r.f_sig, - own_objects: &r.own, - } - } - - fn pair_bytes(r: &Rig) -> (Vec, Vec) { - ( - Publication::Fulfillment { - body: &r.fulfillment, - signature: &r.f_sig, - } - .object_bytes() - .unwrap(), - derive::resolution_claim(&r.precommit, &r.fulfillment).encode(), - ) - } + use crate::sdk::storage_io::{fake_registers, leader_index}; fn ful_ns() -> &'static [u8] { TAG_DSM_SOFI_FULFILLMENT.source_bytes() diff --git a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_test_fixtures.rs b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_test_fixtures.rs index e740d54ba..d1a95db3c 100644 --- a/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_test_fixtures.rs +++ b/dsm_client/deterministic_state_machine/dsm_sdk/src/sdk/sofi_test_fixtures.rs @@ -629,3 +629,151 @@ fn fold_under(trader_core: &TraderCore, leaves: &[(D32, EconomicLeafState)], e: .collect(); batch_fold(&entries).unwrap().post_root } + +// ── A signed route, installed or ready to be: the R9/R10/R11 rig ──────────── + +use std::collections::BTreeMap; +use std::sync::OnceLock; + +use dsm::crypto::sphincs::{generate_sphincs_keypair, sphincs_sign}; +use dsm::sofi::publication::Publication; +use dsm::sofi::signature::SigningPayload; +use dsm::sofi::wire::{SofiSetupBody, TraderFulfillmentBody, ValidationRef}; +use dsm::types::operations::Operation; + +use crate::sdk::sofi_publish::publish_produced; +use crate::sdk::sofi_register::InstallRequest; +use crate::sdk::sofi_sdk::{build_fulfillment, draft_route, Produced, ToPublish}; +use crate::sdk::storage_io::fake_registers; + +/// The trader's SPHINCS+ key, generated once. +pub fn trader_keys() -> &'static (Vec, Vec) { + static KEYS: OnceLock<(Vec, Vec)> = OnceLock::new(); + KEYS.get_or_init(|| generate_sphincs_keypair().unwrap()) +} + +pub fn trader_sign(message: &[u8]) -> Vec { + sphincs_sign(&trader_keys().1, message).unwrap() +} + +pub fn block_on(f: impl core::future::Future) -> T { + crate::runtime::get_runtime().block_on(f) +} + +/// A two-hop route whose legs carry the `ρ` of real setups, everything +/// published to the fake fleet β€” the setups too, when asked β€” and the +/// signed exercise ready to install. +pub struct SignedRoute { + pub set: StorageSet, + pub precommit: TraderPrecommitBody, + pub p_sig: Vec, + pub preimage: SettlementPreimage, + pub fulfillment: TraderFulfillmentBody, + pub f_sig: Vec, + pub own: BTreeMap>, + pub setups: Vec, +} + +pub fn produced_setup(body: &SofiSetupBody) -> Produced { + Produced { + operation: Operation::SofiSetup { + setup_body: body.encode(), + signature: Vec::new(), + }, + signs: SigningPayload::SetupDigest(derive::setup_signing_digest(body)), + publish: vec![ToPublish::Setup(body.clone())], + } +} + +pub fn signed_route(publish_setups: bool) -> SignedRoute { + fake_fleet::reset(); + fake_registers::reset(); + let set = five(); + let setups: Vec = (0..2) + .map(|j| { + let vault_id = derive::vault_id(&OWNER_G, &OWNER_DEV, P_CREATE + j as u64); + SofiSetupBody::new( + G, + DEV, + P_POS - 1, + vault_id, + d(0x0B), + d(0x0C), + SIG_ALG, + &trader_keys().0, + ) + .unwrap() + }) + .collect(); + let rhos: Vec = setups.iter().map(derive::setup_ref).collect(); + let fx = + RouteFixture::swap_with_setups(2, set.id(), |j| (token(j), token(j + 1)), |j, _| rhos[j]); + fx.publish(&set, &all_policies()); + let evidence = fx.acquire(&set); + let draft = draft_route( + fx.hops.clone(), + fx.cores.clone(), + &fx.ctx(&trader_keys().0), + fx.realize_root, + fx.void_root, + &evidence, + ) + .unwrap(); + let p_sig = trader_sign(&draft.precommit_signing_digest()); + let attempts: Vec<(D32, u64)> = draft + .precommit() + .legs() + .iter() + .map(|l| (l.vault_id, 0)) + .collect(); + let produced = build_fulfillment(&draft, p_sig.clone(), &attempts).unwrap(); + let f_sig = trader_sign(produced.signs.bytes()); + block_on(publish_produced(&set, &produced, &f_sig)).unwrap(); + if publish_setups { + for body in &setups { + let sig = trader_sign(&derive::setup_signing_digest(body)); + block_on(publish_produced(&set, &produced_setup(body), &sig)).unwrap(); + } + } + let fulfillment = produced + .publish + .iter() + .find_map(|p| match p { + ToPublish::Fulfillment(f) => Some(f.clone()), + _ => None, + }) + .unwrap(); + SignedRoute { + set, + precommit: draft.precommit().clone(), + p_sig, + preimage: draft.preimage().clone(), + fulfillment, + f_sig, + own: BTreeMap::new(), + setups, + } +} + +pub fn install_request(r: &SignedRoute) -> InstallRequest<'_> { + InstallRequest { + precommit: &r.precommit, + precommit_signature: &r.p_sig, + preimage: &r.preimage, + fulfillment: &r.fulfillment, + fulfillment_signature: &r.f_sig, + own_objects: &r.own, + } +} + +pub fn pair_bytes(r: &SignedRoute) -> (Vec, Vec) { + ( + Publication::Fulfillment { + body: &r.fulfillment, + signature: &r.f_sig, + } + .object_bytes() + .unwrap(), + derive::resolution_claim(&r.precommit, &r.fulfillment).encode(), + ) +} diff --git a/lean4/DSMSofiSuccessorCells.lean b/lean4/DSMSofiSuccessorCells.lean index ee6fcf457..4db60f499 100644 --- a/lean4/DSMSofiSuccessorCells.lean +++ b/lean4/DSMSofiSuccessorCells.lean @@ -34,6 +34,9 @@ - ORDERING no numeric holes in attempt indices; counters never wrap - STORAGEREACHABLE a noncanonical DAG whose producer is (parent, E) β€” never the attempt; reachable is not canonical + - THE EXERCISE (R11) an exercise names its key through its own legs and + counts at one key per vault; the first exercise naming the + key is the occupant, whatever junk precedes it (P1) - REGISTRATION (R10) FulfillmentRegistered is both cells final with the root on this F's own claim β€” a conclusion from reads, never a record; a rival first at the leader settles loss; the root @@ -80,6 +83,7 @@ witness of what that admits and stays green) 7. (R10) `registered` accepting a leader- -> `registration_needs_both_finals` held F at K_ful + 8. (R11) `namesKey` ignoring the attempt -> `an_exercise_counts_at_one_key_per_vault` Run: `lean -DwarningAsError=true DSMSofiSuccessorCells.lean` -/ @@ -946,6 +950,78 @@ theorem root_final_on_another_claim_never_registers (ful : Res) (c f : Val) (cla | leaderHeld _ => rfl | unresolved => rfl +-- ── the exercise: what counts at a successor key (rebuild step R11) ──────── + +/-- An exercise, as a successor key sees it: the `(v, a)` its `F` names and +the `(v, R_n)` its `P` names, per leg β€” one attempt per vault, one parent per +vault (`sofi::exercise::RecognizedExercise`). -/ +structure Exercise where + legs : List (Nat Γ— Nat Γ— Nat) -- (vault, parent, attempt) + +/-- A successor key: `K^(attempt)` of `vault` at `parent`. -/ +structure Key where + vault : Nat + parent : Nat + attempt : Nat + deriving DecidableEq + +/-- `exercise_names_key`: the value counts at `k` iff some leg of the exercise +is exactly `k`'s `(v, R_n, a)`. -/ +def namesKey (x : Exercise) (k : Key) : Bool := + x.legs.any fun l => decide (l = (k.vault, k.parent, k.attempt)) + +/-- P1, OnlyExercisesCount, at the level of one cell's occupant: what a key +holds is the first object that names it; bytes that rebuild into no exercise +(`none`) or into one naming another key are passed over. -/ +def occupant (held : List (Option Exercise)) (k : Key) : Option Exercise := + held.findSome? fun o => match o with + | some x => if namesKey x k then some x else none + | none => none + +/-- AN EXERCISE NAMES ITS KEY THROUGH ITS OWN LEGS +(`an_exercise_names_exactly_the_keys_its_fulfillment_and_precommit_name`, +`an_exercise_cannot_count_at_another_key`): an exercise whose legs each name +one vault once counts at a key only for the attempt and parent its leg +names β€” two keys of one vault it counts at are the same key. Mutation: +`namesKey` ignoring the attempt β€” this fails. -/ +theorem Key.ext' {a b : Key} (h1 : a.vault = b.vault) (h2 : a.parent = b.parent) + (h3 : a.attempt = b.attempt) : a = b := by + cases a; cases b; simp_all + +theorem an_exercise_counts_at_one_key_per_vault (x : Exercise) (k k' : Key) + (hone : βˆ€ l ∈ x.legs, βˆ€ l' ∈ x.legs, l.1 = l'.1 β†’ l = l') + (hk : namesKey x k = true) (hk' : namesKey x k' = true) (hv : k.vault = k'.vault) : + k = k' := by + unfold namesKey at hk hk' + simp only [List.any_eq_true, decide_eq_true_eq] at hk hk' + obtain ⟨l, hl, hle⟩ := hk + obtain ⟨l', hl', hle'⟩ := hk' + have hll : l = l' := hone l hl l' hl' (by rw [hle, hle']; exact hv) + rw [hle, hle'] at hll + simp only [Prod.mk.injEq] at hll + exact Key.ext' hv hll.2.1 hll.2.2 + +/-- ONLY AN EXERCISE NAMING THE KEY COUNTS (`only_an_exercise_naming_the_key_counts`): +whatever is held before it β€” unrecognized bytes, exercises naming other keys β€” +the first exercise naming the key is the occupant. -/ +theorem only_an_exercise_naming_the_key_counts (junk : List (Option Exercise)) (x : Exercise) + (k : Key) (hx : namesKey x k = true) + (hjunk : βˆ€ o ∈ junk, βˆ€ y, o = some y β†’ namesKey y k = false) (rest : List (Option Exercise)) : + occupant (junk ++ some x :: rest) k = some x := by + induction junk with + | nil => simp [occupant, hx] + | cons o os ih => + have hos : βˆ€ o' ∈ os, βˆ€ y, o' = some y β†’ namesKey y k = false := + fun o' h y hy => hjunk o' (List.mem_cons_of_mem _ h) y hy + have := ih hos + cases o with + | none => simpa [occupant, List.findSome?] using this + | some y => + have hy : namesKey y k = false := hjunk (some y) (List.mem_cons_self ..) y rfl + simpa [occupant, List.findSome?, hy] using this + +#print axioms an_exercise_counts_at_one_key_per_vault +#print axioms only_an_exercise_naming_the_key_counts #print axioms registration_needs_both_finals #print axioms a_rival_first_at_the_leader_settles_loss #print axioms root_final_on_another_claim_never_registers