feat(core): balance conservation + signed policy_commit binding (#448, §9.5)#474
Merged
Merged
Conversation
…#448) Normative doctrine governing token-policy installation (authoritative-source only, no absorption from peer/inbox/contact/offline/envelope), policy_commit binding in every transfer (§9.5), and per-transfer counterparty readiness (online published surface, offline direct exchange), with fail-closed semantics. Each enforcement surface is marked Layer A (shipped) or Layer B (planned), cross-referencing tracked issues #466-#473. Custom-token transfer readiness is marked INCOMPLETE until the Layer-B issues close. The first mandatory blocker (policy_commit binding into the signed Transfer op + conservation + fail-closed) lands in this branch.
…, #467) Per whitepaper §9.5 ("All TokenOps MUST include policy_commit") and the token-policy doctrine §4, bind the token's CPTA policy commitment into the signed Transfer operation. Adds a required [u8;32] `policy_commit` field to Operation::Transfer and threads it through both serializers in lockstep (operations.rs canonical to_bytes/from_bytes tag-3, and storage codecs). Production send sites resolve policy_commit from the local source-of-truth installed policy via CoreSDK/TokenSDK::resolve_policy_commit_strict (builtins -> canonical constants; custom -> BCR-history anchor walk; unknown -> fail closed). The b0x receiver reconstruction takes the sender's signed policy_commit from the canonical preimage. Commitment-scaffolding/placeholder and test literals use a zero placeholder. Wire-format change: persisted Transfer operation bytes (bcr_chain_states, bilateral_sessions) change layout — beta installs must reset their local DB. Round-trip verified for both serializers. Conservation guard + receive-side mismatch rejection follow in subsequent commits.
…te::advance (#448) Add validate_conservation() at the sole balance-mutation chokepoint (DeviceState::advance), called before the mutation loop. It requires the supplied BalanceDeltas to exactly realize the signed operation: - Transfer: exactly one delta, amount == op.amount, direction Credit iff this device is the recipient (op.to_device_id == self.devid) else Debit, and delta.policy_commit == op.policy_commit (§9.5 token binding). - Mint: one Credit == amount. Burn: one Debit == amount. - Every other operation: no balance deltas. This rejects value creation/substitution regardless of caller, replacing the previous enforce-by-convention model. Ports the rules of the dead, &State-typed verify_token_balance_consistency onto &[BalanceDelta]. Code correspondence: lean4 DSMOfflineFinality.lean commit_conservation / commitTransfer (no Lean change). Test fixtures that paired a Generic op with non-empty deltas (or empty deltas with a Transfer) updated to matching value ops (mint_op/burn_op/value_op helpers); two SMT-advance state_machine tests switched to a non-balance Generic op. Added conservation_guard_rules unit test. Full dsm lib suite green.
…ding (#448, #467) Make the bilateral BLE path consistent with the online path: the three sender/receiver delta builders now independently resolve the device's own installed policy_commit via the new AppRouter::resolve_policy_commit_strict (builtins -> constants; custom -> BCR-history anchor walk) instead of the builtin-only resolver that silently dropped the credit on any custom token. An unresolved/uninstalled policy yields empty deltas, which the conservation guard now rejects (fail closed) — no silent value skip, no peer-policy absorption. §9.5 receive-side enforcement is realized end-to-end: the signed op carries policy_commit, the receiver derives the balance delta's policy_commit by independent resolution, and DeviceState::advance's conservation guard rejects unless delta.policy_commit == op.policy_commit (i.e. the receiver's installed policy matches the sender's committed policy). Adds AppRouter::resolve_policy_commit_strict (default fails closed; AppRouterImpl delegates to CoreSDK).
… to guard (#448) - wallet.sendOffline: encode_offline_transfer_operation_canonical now writes the token's policy_commit (resolved from the local installed policy) so the offline-authored Transfer decodes and binds policy_commit like every other path. - Test fixtures aligned to the conservation guard: bcr sample_operation is now a recipient-credit bound to its delta's policy_commit with matching amounts; smart_commitment_sdk execute_commitment tests use the builtin ERA token so policy resolution succeeds. dsm (1434) and dsm_sdk (1506) lib suites pass; clippy clean.
#448) CI builds the whole workspace; the validation harness binaries construct Operation::Transfer and broke on the new required policy_commit field. These tools build+sign ops and never apply through DeviceState::advance (no guard interaction), so they carry a zero placeholder policy_commit. 7 sites across adversarial_bilateral, bilateral_throughput, implementation_traces (x3), property_tests, tla_trace_replay. Full workspace build + vertical_validation tests (19) pass; clippy clean.
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
1 participant
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.
What
Closes #448. Closes #467.
Enforces balance conservation by construction on the live state-advance path and binds the token's CPTA
policy_commitinto the signedOperation::Transferper whitepaper §9.5. This is the first mandatory blockerof the custom-token policy + per-transfer readiness doctrine (added as a normative spec in this PR); the remaining
enforcement surfaces are tracked as Layer-B follow-ups.
Why
DeviceState::advanceapplied caller-suppliedBalanceDeltas blindly— conservation was enforced by convention at callers, not by construction; the real check
(
verify_token_balance_consistency) was dead (test-only,&State-typed).policy_commit; verifiers reject if it differs from the token's creationpolicy_commit") was normative butOperation::Transfercarried onlytoken_id(a spec↔code gap).How
.github/instructions/token-policy-readiness.instructions.md): authoritative-source install,no absorption from peer/inbox/contact/offline,
policy_commitbound in every transfer, per-transfercounterparty readiness, fail-closed. Each surface marked Layer A (shipped) or Layer B (planned, tracked).
policy_commitfield added (required[u8;32]) toOperation::Transfer, threaded through all threeserializers in lockstep (canonical
to_bytes/from_bytes, storagecodecs, offline encoder) and everyconstruction site. Production send sites resolve from the local source-of-truth installed policy via
resolve_policy_commit_strict(builtins → constants; custom → BCR-history anchor walk; unknown → fail closed).DeviceState::advance: for a Transfer, exactly one delta,amount == op.amount,direction
Creditiff this device is the recipient elseDebit, anddelta.policy_commit == op.policy_commit;Mint = one Credit==amount; Burn = one Debit==amount; every other op carries no deltas. Rejects value
creation/substitution regardless of caller. Code correspondence: lean4
DSMOfflineFinality.leancommit_conservation(no Lean change — the code realizes the existing theorem).policy_commitvia the newAppRouter::resolve_policy_commit_strict(no silent skip, no peer-policyabsorption); unresolved → empty deltas → guard rejects. §9.5 receive enforcement is realized end-to-end: signed
op carries
policy_commit, receiver independently resolves the delta's commit, guard rejects unless they match.Migration
The required field changes the persisted Transfer-op wire layout (
bcr_chain_states,bilateral_sessions), sobeta installs must wipe their local DB on upgrade (no auto-reset machinery). Early beta — acceptable.
Tests / verification
conservation_guard_rulesunit test + round-trip tests for all three serializers.cargo clippy -p dsm -p dsm_sdk --all-featuresclean.cargo test -p dsm --lib1434 passed;dsmintegration tests pass.cargo test -p dsm_sdk --lib(single-threaded) 1506 passed; offlinedsm_sdkintegration tests pass.Tracked Layer-B follow-ups
#466 (issuer/root-signed anchor verification), #468 (receiver-side install verification), #469 (sender readiness
preflight), #470 (online published readiness object), #471 (offline readiness exchange), #472 (fail-closed test
matrix), #473 (extend
policy_commitbinding to Mint/Burn/CreateToken). Custom-token transfer readiness is markedINCOMPLETE until these close.
Coordination with sibling PRs
to_bytes()(now incl.policy_commit), not the divergentencode_dsm_operation_det.