feat(economic): 3.5b PR1 — the write-set rule as a verifier conjunct; v2 operation identity; typed substrate - #735
Merged
Conversation
…peration identity, typed substrate, exact operation semantics
3.5b PR1 of 4. advance_validated proved a witness internally consistent and
funded but never that its mutations were the exact economic effect of the
authenticated operation — an adversarial producer could pair a valid accepted
operation with a DIFFERENT internally consistent write set. This PR closes
that, plus the two identity gaps the owner's review found in merged code.
Core (dsm):
- economic/write_set.rs (new): BOTH sides of one deterministic rule.
build_write_set derives the exact mutations (key-ordered, progressively
proved) + credit sources from a verified operation and the pre-state;
verify_operation_write_set requires a witness to be EXACTLY that effect —
no missing mutation, no extra mutation, exact asset, exact amount, exact
role, exact source kind. Transfer role derives from
to_device_id == the authenticated local DevID, never a supplied enum.
CreateToken: fee-only validates; initial_supply > 0 gets the named
CreateTokenInitialSupplyRequiresIssuancePredicate refusal (funding the new
asset from the ERA fee would turn a fee into arbitrary issuance). Mint
refused; DlvSettle/DlvClose deferred to 3.6.
- EconomicOperationId_dsm corrected: /v1 BURNED (its preimage
G‖DevID‖operation_digest cannot distinguish two successors carrying
byte-identical operations), /v2 = G‖DevID‖C_dsm+ — load-bearing the moment
consumed_source.consumer_economic_operation_id exists.
- AcceptedSubstrate becomes TYPED: DsmSuccessor{verified_operation,
c_dsm_plus, evidence_addr} (boxed; digest DERIVED from the operation
bytes, never supplied) | OfflineBoundary. advance_validated now requires
same-kind equality with the manifest's substrate slot and exact evidence
equality, recomputes the v2 id from the successor's C_dsm+, and runs the
write-set conjunct; OfflineBoundary admissions fail closed until Step 5
specifies boundary write sets.
- PendingEconomicAdmission restructured: Prepared carries ONLY the digest —
under the v2 identity the acceptance coordinates (post-root, substrate
addr, manifest addr, and now the durable c_dsm_plus) cannot exist before
the successor does, and the type no longer pretends they do. Constructors
enforce coords-iff-post-Prepared; the DB refuses to persist Prepared.
This is also what resolves the producer circularity the v2 id creates.
- decode_admission_manifest (new, strict): refuses non-canonical index
order rather than canonicalizing; exactly one substrate slot.
SDK (the minimal faucet adaptation the v2 contract forces):
- The producer is PREPARE-FIRST: the successor is prepared in memory, its
chain-state commitment feeds the witness/manifest/coordinates built in
faucet_claim_advance's build phase, and successor + pending + frozen
evidence commit in ONE transaction. Resume recovers the exact operation
from the frozen substrate artifact and re-derives nothing.
- Client DB schema 8 -> 9: economic_pending_admissions gains c_dsm_plus.
Tests: economic_write_set.rs (15 — round-trips for all five ops, the
owner's two CreateToken rulings, adversarial near-misses, and the first
REAL multi-mutation sequencing failures: permuted order and stale
non-progressive siblings); economic_admission_lifecycle reworked onto a
genuine faucet transition (13 — the old 'valueless record insertion'
fixture is exactly what the new conjunct forbids), including the write-set
forgery control and the two new binding controls. Three mutation controls
run red-under-a-compiling-mutant and restored: the write-set conjunct, the
v2-id conjunct, the substrate-evidence binding.
Boards (pinned 1.98.0, exact final tree): workspace 69 suites 3844/0
(dsm lib 1664/0, dsm_sdk lib 1775/0), dsm_storage_node 270/0, make lint
exit 0, production_safety_checks.sh exit 0.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
3.5b PR 1 of 4 (write-set semantics → peer-lineage validation → sender wiring → recipient wiring), per the owner-approved plan and its three review rounds.
The gap this closes
advance_validatedproved a witness internally consistent (mutation sequence) and funded (provenance), but never that its mutations were the exact economic effect of the authenticated operation. An adversarial producer could pair a valid accepted operation with a different internally consistent write set. The classifier deliberately only names the category (ClosedWriteSet); the computation of the set existed nowhere.What lands
economic/write_set.rs— both sides of one deterministic rule.build_write_set(producer: key-ordered mutations, siblings captured progressively against the tree after each prior mutation applies) andverify_operation_write_set(verifier: no missing mutation, no extra mutation, exact asset, exact amount, exact role, exact source kind), generated from one semantic table. Transfer role derives fromto_device_id == the authenticated local DevID— never a supplied enum. Per the owner's rulings: CreateToken fee-only validates,initial_supply > 0gets the namedCreateTokenInitialSupplyRequiresIssuancePredicaterefusal; Mint refused;DlvSettle/DlvClosedeferred to 3.6. The conjunct is wired intoadvance_validated.v2 operation identity,
/v1burned. The shipped preimage (G‖DevID‖operation_digest) cannot distinguish two successors carrying byte-identical operations — load-bearing the momentconsumed_source.consumer_economic_operation_idexists./v2 = G‖DevID‖C_dsm+; one domain, one meaning; the burn rationale lives in the tag's doc comment.Typed
AcceptedSubstrate.DsmSuccessor { verified_operation, c_dsm_plus, evidence_addr }(boxed; the digest is derived from the operation bytes, never supplied) |OfflineBoundary.advance_validatedrequires same-kind equality with the manifest's substrate slot and exact evidence equality — without it a caller validates one successor while the registered manifest names a different evidence object, and the DAG stops being the evidence actually used. Offline-boundary admissions fail closed until Step 5 specifies boundary write sets (never a silent pass-through, never a hardDsmSuccessorrequirement that would break Step 5).Preparedadmissions carry only the digest. Under the v2 identity, the acceptance coordinates (post-root, substrate addr, manifest addr, and the now-durablec_dsm_plus) cannot exist before the successor does — the type no longer pretends they do. Constructors enforce coords-iff-post-Prepared; the DB refuses to persistPrepared. This struct split is also exactly what resolves the producer circularity the v2 id creates (witness needsC_dsm+→ needs the prepared successor → the gate needs an attached admission, which now needs only the digest).Prepare-first faucet producer (the minimal SDK adaptation the contract forces): successor prepared in memory → its
C_dsm+feeds the witness/manifest/coords built in the advance's build phase → successor + pending + frozen evidence commit in ONE transaction. Resume recovers the exact operation from the frozen substrate artifact. Client DB schema 8 → 9 (c_dsm_pluscolumn; beta wipe policy).Strict
decode_admission_manifest— refuses non-canonical provenance-index order rather than canonicalizing (two byte strings must never decode to one object).Consequences named
Tests and mutation controls
economic_write_set.rs(15): round-trips for all five ops; the owner's two CreateToken tests; adversarial near-misses (extra mutation, wrong amount/asset/role, stripped consumed-source); the first REAL multi-mutation sequencing failures (permuted order, stale non-progressive siblings).economic_admission_lifecycle(13): the write-set forgery control (a_witness_that_is_not_the_operations_exact_effect_is_refused), the v2-id control, the substrate-binding controls, plus all prior structural clauses on the new fixture. Three mutation controls run red-under-a-compiling-mutant and restored: write-set conjunct discarded → forgery control red; id conjunct self-compares → successor-binding control red; evidence equality self-compares → manifest-binding control red.Boards (pinned 1.98.0, exact final tree)
Next: PR 2 — peer-lineage validation (replayable successor/authority evidence, the recursive walker with cycle guard, the exact
ValidatedPeerDebitpredicate incl. B-side acceptance-evidence verification, the validated-peer cache).