Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions .github/instructions/sofispecs.instructions.md
Original file line number Diff line number Diff line change
Expand Up @@ -562,6 +562,17 @@ nor constitutes a new approval, veto, rollback, or ordering step. If a terminal
SoFi: Sovereign Deterministic Finance Revision 15
has already become binding-final and folded under Requirement 6.30, the DLV is retired and no
separate catch-up step is required for that closed vault.
Implementation (amendment 2c-G, rulings G1 + G2). Catch-up applies each certified market
successor V_g → V_n in causal order as one admitted DlvOwnerApplyV2 per generation: a
synchronization step that consumes certified history and never creates it — no authority, no second
value move, no re-certification, no new realization boundary, no veto and no ordering step. Each
apply's input-reserve credit is funded by the trader's own admitted payment (0x0027), whose
evidence is projected from the exact receipt leaf and path the composition walk proved under the
trader's validated root when it certified that fold; the terminal owner reserve state equals the
composed frontier. One engine runs it — automatically on storage.sync and on an explicit owner
request — and it gates no trader settlement, market realization, composition, future admission,
QuorumBind, fence release or close finality. A failure is local to its vault, and an interrupted
catch-up resumes idempotently after its last durable apply.
Requirement 4.6 (Governed reverse encumbrance; owner-local beta profile). The LP
must not be able to move DLV reserves directly back into ordinary spendable owner balance merely
by virtue of ownership. The vault birth state commits a release/withdraw/close policy PR. Any
Expand Down Expand Up @@ -1242,6 +1253,10 @@ already-verified market history when the owner participates, but it does not imp
time or maximum number of market advances for which the owner may remain absent. A terminal
owner close under Requirement 6.30 is itself the final owner/DLV state update and does not require
a separate catch-up step.
Status (amendment 2c-G, ruling G3). The catch-up of Requirement 4.5 is implemented; the fresh
baseline this requirement demands — an AnchorPresentationV3 over exactly the caught-up V_n, built
by the same owner-anchor machinery as the birth baseline — is not yet published. It is owed by the
third 2c-G change, after the admitted terminal close (G4).
7 Smart Commitments and Atomic Composition
Definition 7.1 (Smart Commitment). A bounded deterministic predicate over committed
inputs:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -553,7 +553,7 @@ jobs:
- name: Kernel-check every module, sorry-free
run: |
set -euo pipefail
expected=19
expected=20
found=$(ls lean4/*.lean | wc -l)
if [ "$found" -ne "$expected" ]; then
echo "::error::lean4/ has $found modules, expected $expected."
Expand Down
9 changes: 9 additions & 0 deletions docs/papers/ccb-object-registry.md
Original file line number Diff line number Diff line change
Expand Up @@ -1599,6 +1599,15 @@ storage-object address (amendment 2c-C1 ruling A).
| 7 | `trader_economic_position` | `u64` | **the schema-2 field** — an untrusted locator |
| 8 | `payment_evidence_addr` | `digest32` | |

**Producer (amendment 2c-G).** The owner's catch-up builds the `SettlementPaymentEvidenceV1`
bundle (transport proto, no CCB class) from the certified fold: the exact `0x0021` leaf and
256-sibling path the composition walk proved under the trader's validated `R_T^+` at the
acceptance's position (Req 21.16), carried on the fold and never fetched again. Fields 5–7 are the
walk's authenticated trader and that position. The producer mirrors the arm's leaf-equality and
inclusion checks before signing — the arm runs after the advance commits, where a refusal would
strand the admission — and the arm alone decides. `DlvOwnerApplyV2` is admission-fenced at the
core chokepoint: an owner apply is admitted with this arm or it does not advance.

**Two schema-2 arms, one reason.** Both carry a peer/owner `*_economic_position` that schema 1 did
not, and both are labelled **untrusted locators**: they say where to start looking, never what is
true. The verifier derives the position independently. That is the same locator-not-authority
Expand Down
139 changes: 128 additions & 11 deletions dsm_client/deterministic_state_machine/dsm/src/types/device_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1843,15 +1843,26 @@ impl DeviceState {
// raw operation and encumber reserves the economic lineage never saw,
// leaving a head whose reserves `R_econ` cannot account for.
//
// Deliberately NARROW. Settle, close and owner-apply are not fenced
// here: they consume or return an existing position rather than
// originating one, and their admission wiring is a separate cut with a
// separate evidence story. Widening this gate before those producers
// exist would strand the trader path with no replacement.
// Deliberately NARROW. Settle and close are not fenced here: they
// consume or return an existing position rather than originating one,
// and their admission wiring is a separate cut with a separate evidence
// story. Widening this gate before those producers exist would strand
// the trader path with no replacement.
if matches!(operation, Operation::DlvCreateFundedV2 { .. }) {
self.require_attached_dsm_admission(&operation, "a funded vault creation")?;
}

// THE OWNER APPLY (amendment 2c-G). `DlvOwnerApplyV2` moves both vault
// reserve leaves a generation, so an unadmitted apply leaves a head
// whose reserves `R_econ` never saw — and every later admission that
// reads those leaves (the next apply, the close) builds against a root
// that disagrees with the head. Its producer now exists: the owner's
// catch-up admits every apply with its `0x0027` settlement-payment
// evidence, so the raw doorway closes here.
if matches!(operation, Operation::DlvOwnerApplyV2 { .. }) {
self.require_attached_dsm_admission(&operation, "an owner apply")?;
}

// THE SECOND ISSUANCE OPERATION. `CreateToken` carries an issuance leg,
// and `validate_conservation` deliberately PERMITS it (the arm requires
// exactly one credit of `initial_supply` under the new token's own
Expand Down Expand Up @@ -6914,7 +6925,7 @@ mod tests {

// A third asset on the input side: refused, nothing moves.
let root_before = funded.root();
let err = funded.advance(
let err = funded.advance_admitted(
rk,
funded.devid,
apply_op(dbtc, rigb, out_amt),
Expand Down Expand Up @@ -6945,7 +6956,7 @@ mod tests {

// The real settlement: legs move AND the vault-state leaf follows.
let out = funded
.advance(
.advance_admitted(
rk,
funded.devid,
apply_op(era, rigb, out_amt),
Expand Down Expand Up @@ -7227,7 +7238,7 @@ mod tests {
signature: vec![],
mode: TransactionMode::Unilateral,
});
let err = funded.advance(
let err = funded.advance_admitted(
rk,
funded.devid,
op,
Expand Down Expand Up @@ -7283,7 +7294,7 @@ mod tests {
mode: TransactionMode::Unilateral,
});
let out = funded
.advance(
.advance_admitted(
rk,
funded.devid,
op,
Expand Down Expand Up @@ -7311,6 +7322,112 @@ mod tests {
assert_eq!(out.vault_reserve(&vault, &rigb), 5_000 - out_amt);
}

/// THE OWNER APPLY IS ADMITTED OR IT DOES NOT HAPPEN (amendment 2c-G).
///
/// The same matching, curve-priced v2 apply as the positive control above,
/// advanced RAW: no pending admission attached. It must be refused by the
/// fence's own precondition, with the reserves exactly where they were —
/// otherwise the head moves two reserve leaves `R_econ` never saw, and the
/// next admission that reads them builds against a root that disagrees
/// with the head. An admission bound to a DIFFERENT operation authorizes
/// nothing either.
///
/// MUTATION CONTROL: delete the `DlvOwnerApplyV2` arm of the fence in
/// `advance` and the first assertion goes red by moving the reserves.
#[test]
fn an_owner_apply_is_refused_without_its_own_attached_admission() {
let (era, rigb) = (pc(0xE0), pc(0xF0));
let (funded, vault, rk, tip) = funded_for_close(0xD7, era, rigb, 10_000, 5_000);
let funded = funded.with_pending_economic_admission(None);
let out_amt = crate::dlv::route_commit::constant_product_output(100, 10_000, 5_000, 30)
.expect("curve");
let (parent_binding, parent_state) = parent_of(&funded, vault, vault_pair(era, rigb));
let op = sign_op(Operation::DlvOwnerApplyV2 {
vault_id: vault.to_vec(),
settlement_receipt_id: [0x21; 32],
pending_pointer_x: [0x22; 32],
parent_sequence: 0,
new_sequence: 1,
parent_binding,
input_policy_commit: era,
output_policy_commit: rigb,
input_amount: 100,
output_amount: out_amt,
fee_bps: 30,
signature: vec![],
mode: TransactionMode::Unilateral,
});
let mutation = || VaultReserveMutation::ApplySettlement {
vault_id: vault,
input_policy_commit: era,
input_amount: 100,
output_policy_commit: rigb,
output_amount: out_amt,
parent_sequence: 0,
new_sequence: 1,
pair: vault_pair(era, rigb),
parent_state: parent_state.clone(),
};
let root_before = funded.root();

// (1) No admission attached at all.
let err = format!(
"{}",
funded
.advance(
rk,
funded.devid,
op.clone(),
entropy(2),
None,
&[],
Some(tip),
None,
None,
Some(mutation()),
)
.expect_err("a raw owner apply must not move the reserves")
);
assert!(
err.contains("no pending economic admission"),
"the refusal is the fence's own, got: {err}"
);

// (2) An admission attached, but bound to a DIFFERENT operation.
let staged = funded.with_pending_economic_admission(Some(
crate::economic::admission::PendingEconomicAdmission::prepared(
crate::economic::admission::PendingAdmissionKind::DsmBacked,
1,
[0u8; 32],
crate::economic::faucet::dsm_operation_digest(&Operation::Noop.to_bytes()),
),
));
let err = format!(
"{}",
staged
.advance(
rk,
staged.devid,
op,
entropy(2),
None,
&[],
Some(tip),
None,
None,
Some(mutation()),
)
.expect_err("an admission for another operation authorizes nothing")
);
assert!(
err.contains("does not match the pending economic admission"),
"the refusal names the digest mismatch, got: {err}"
);
assert_eq!(funded.root(), root_before, "nothing moved");
assert_eq!(funded.vault_reserve(&vault, &era), 10_000);
assert_eq!(funded.vault_reserve(&vault, &rigb), 5_000);
}

/// The head's OWN parent state for `vault` under `pair`: its commitment
/// (what the owner signs as `parent_binding`) and its bytes (what the
/// mutation carries). Exactly what `dlv.reconcile` derives from the
Expand Down Expand Up @@ -7375,7 +7492,7 @@ mod tests {
op: Operation,
mutation: VaultReserveMutation,
) -> Result<AdvanceOutcome, DsmError> {
head.advance(
head.advance_admitted(
rk,
head.devid,
op,
Expand Down Expand Up @@ -7728,7 +7845,7 @@ mod tests {
mode: TransactionMode::Bilateral,
});
let traded = funded
.advance(
.advance_admitted(
rk,
funded.devid,
apply,
Expand Down
Loading
Loading