fix(sofi): a vault creation cannot contradict itself (F9.x)

[cryptskii]

Split out of F10 by owner ruling, because it protects a different invariant.

F9.x — a creation operation cannot internally contradict itself, whatever produced it.
F10 — a creation cannot be presented as authoritative unless it actually occurred in the creator's accepted lineage.

Procedural note. This change was first pushed directly to main as d2734be3, with no PR. That was my error: the branch had been created with git checkout -b <name> origin/main, which set its upstream to origin/main; I filtered the push output through a grep and then printed a "pushed" line that was an echo of my own local HEAD rather than evidence of where anything landed. main was repaired with a plain revert (e72c41d4) — no force-push, no history rewrite — and this branch reapplies the identical tree from that revert. git diff --quiet d2734be3 HEAD confirms the tree is unchanged. Nothing about the implementation was altered during the repair.

What was already there

semantic_write_set's SofiVaultCreate arm already planned two real balance debits against the admitted R_econ (refusing InsufficientBalance) plus an insert-only creation leaf, with the verifier half requiring exactly those three mutations — on the owner's path and on foreign walks alike. S_pre −(x,y)→ S_post was derivable, and the funded amounts were bound to the genesis reserves. The framing "creation carries no balance evidence" is wrong about amounts.

The asset-substitution door

funding_a/b_policy_commit passed straight into pair_legs, which checks only leg_a.0 < leg_b.0 and non-zero. write_set.rs referenced market_policy nowhere. So a creation could debit X and Y while its genesis declared a market in A and B — and a later close credits the owner policies.market.token_a()/token_b(). Fund with junk, close for real assets.

That binding had existed, in genesis_accepted:

if funding.pair() != (token_a, token_b) {
    return Err(GenesisError::FundingIsNotTheMarketPair);
}

#955 deleted that function correctly — it could not derive provenance and was never callable — but the deletion took a working check with it. I verified only that the kept error variants were still referenced, and those references were the SDK producer. Deleting an architectural dead end without relocating the valid invariant it happened to enforce is the defect, not the deletion.

The rule, in Core, before any debit is planned

Three preimages strictly decode · owner genesis and DevID are the authenticated local ones · create_position is the position the operation lands at · record.vault_id == preimage.vault_id() · record.genesis_root == lineage::genesis_root(vault_id, state) · record.amount_{a,b} == state.reserve_{a,b} · the inner state's owner coordinates equal the outer preimage's · policy_object_address(MARKET_POLICY, market_policy_preimage) == state.market_policy · the decoded pair equals the funding pair · the pair stays canonically ordered with both amounts non-zero.

Address equality and pair equality are separate bindings and are not collapsed. One proves the carried bytes are the policy object the state named; the other proves the assets debited are the two that policy authorizes. Their mutations red disjoint test sets.

The wire change

Operation::SofiVaultCreate carries market_policy_preimage: Vec<u8>, so acceptance is a function of the operation's bytes and the authenticated pre-state alone — no resolver, storage-availability or foreign-walk liveness assumption between a local decision and its answer. 72 fixed-width bytes against the 49,856-byte SPHINCS+ signature already there.

Signature coverage is automatic — operation_signing_bytes(op) = op.with_cleared_signature().to_bytes(), the verify arm passes the whole operation, no separate signed-field list — so one line in the encode arm is necessary and sufficient. A test proves it isn't tautological by altering only that field after signing.

No decode-and-re-encode check. MarketPolicy is 72 bytes with no optional position; decode_market_policy pins class and schema, pins the beta family and version before reconstruction (load-bearing, since beta_constant_product overwrites them), enforces a < b, and finish_exact refuses trailing bytes. encode(decode(P)) == P for every accepted P, so the assertion would have no reachable rejection case — and an assertion no mutation can red is a finding about the test.

Mutation controls

Each alone, grep-verified present, restored. M1–M6 ran against the full 1,787-test dsm lib.

Mutation	Test that goes red
M1 funding pair not bound to the decoded market pair	funding_assets_that_are_not_the_markets_pair_are_refused, a_funding_pair_out_of_canonical_order_is_refused
MA carried policy not bound to the address the state names	policy_bytes_that_are_not_the_ones_the_state_names_are_refused, a_market_policy_preimage_that_is_not_canonical_is_refused
M4 create_position not held to the landing position	a_creation_naming_a_position_it_does_not_land_at_is_refused
M5 inner/outer owner coordinates not held equal	a_state_naming_other_owner_coordinates_than_its_preimage_is_refused
M6 the stated genesis_root is trusted	a_creation_stating_a_genesis_root_the_state_does_not_derive_is_refused
MS the carried policy dropped from the canonical encoding	altering_the_carried_market_policy_after_signing_is_refused, a_creation_round_trips_both_funding_commits_in_order, every_sofi_operation_round_trips_through_the_byte_codec

The fixture change is the substantive one

sofi_genesis_state and sofi_create_operation now take the market pair separately from the funding pair. A fixture that conflated them could not express this defect — which is why seven existing tests passed straight over it, treating funding assets as free parameters.

Added at the real seam: funding_assets_outside_the_declared_market_are_refused_even_when_funded — funded from assets the device genuinely holds, canonically ordered, in the exact reserve amounts, declaring a market in two different assets. Every other binding holds. Still refused.

Two corrections to my own earlier reports

Both from judging coverage by cargo test --lib, which does not compile tests/*.rs:

• I said the creation arm had zero behavioural coverage. Wrong — dsm/tests/economic_write_set.rs had a real creation fixture and seven tests. What was true and sharper: the fixture took funding assets as free parameters.
• I said no SoFi operation had a round-trip test. Wrong — dsm/tests/sofi_v8_operations.rs has two. I deleted the duplicate I had added to operations.rs and extended the real one instead, which is why MS now reds three tests rather than two.

The vector corpus is not the obligation here

Five copies of tests/vectors/v1 exist and the corpus contains zero operation-encoding vectors — all 8 cases are Envelope-v3 Invoke/ReceiptCommit, never touching Operation::to_bytes. Regeneration would produce byte-identical files, so it is not done. Two separate repository-hygiene defects recorded and deliberately not folded in: the generator writes four of the five copies and frontend/public/vectors/v1 has no writer at all; and no CI job ever invokes vector_builder, so corpus staleness cannot be detected.

Gates

Run locally on the identical tree before the accidental push, and preserved here as evidence rather than as a substitute for this PR's CI: the board — the exact CI command, cargo test --locked --workspace --exclude dsm_storage_node --release — 3,834 passed, 0 failed, exit 0; cargo fmt --all --check 0; cargo clippy --all-targets -D warnings 0; ci/production_safety_checks.sh 0 including TLA+; G1 87 reachable / 0 baselined. Re-running against 884cef68, and PR CI is the board that decides.

make lint stops after the Rust half in this worktree (no node_modules); zero frontend files are touched, so CI's Frontend job is the authority there.