Repository navigation
refactor(sofi): vault genesis acceptance is formal only - #955
Merged
Merged
Conversation
genesis_accepted was a twelve-conjunct predicate that took a PRESENTED creation operation and an owner root and returned a vault id. It could never acquire a production caller, because VaultCreation carries no asset commitments: proving the creation leaf establishes the AMOUNTS and never which balances were debited, so a caller could hand in an A/B-shaped sibling of an operation that actually debited X/Y. A CI gate existed to keep it callerless, and the G1 baseline told R14 to wire or delete it. Wiring failed the gate; deleting contradicted the spec. Owner ruling §44.4: the standalone production predicate was the stale piece, not the gate. It is deleted from Rust with CreationFunding, the eight GenesisError variants only it used, and its six tests. The three variants build_vault_create actually uses stay. The rule is not deleted. It is stated in the formal layer, which already carried it: Lean GenesisAccepted and genesis_requires_validated_creation, TLA GenesisCanonicalOnlyIfCreationValid. The binding gate is repurposed to keep BOTH halves true — no Rust predicate, and the formal definitions still present, because a deletion that quietly took the statement with it would be the same hole by another route. What production does instead is RECOGNIZE, not accept: the genesis is kept if its recomputed vault_id is the locator it was found under, and genesis_root is compared to the parent root the trader's own precommit names. vault_id does not depend on the vault state, so those three public coordinates let any party index a preimage under the right locator and the recognizer keeps the first that arrives. Nothing yet binds a genesis to the owner transition that funded it; F10's VerifiedVaultCreation owes that. Executed against the gap: the TLA fault _RegisteredGenesisAccepted, which models a walk starting from a merely stored genesis, violates GenesisCanonicalOnlyIfCreationValid (1,758,084 states) — a vault's parent is consumed though its creation was never validated. Gate controls, each restored byte-identical: M1 a Rust genesis-acceptance predicate returns -> the gate fails, naming it M2' the formal statement is renamed away -> the gate fails, naming it M2 first passed while the definition had been renamed away, because a use site still spelled the name. The gate now requires the DEFINITION. That is the third time in this step that matching a spelling instead of the thing produced a green gate, and it is the same defect G1 carried for thirteen. G1 baseline 7 -> 6 lines. Spec §19.8, §28.5, §30.1, §41.3.
cryptskii
deleted the
refactor/sofi-genesis-acceptance-is-formal-only
branch
September 21, 2026 13:45
Collaborator
Author
Correction to the scope of the gap, and the design that closes itThe PR body and the commit message overstate what the recognition weakness permits. The correct bound, ruled today: A token must be pre-added to the device's validated state before any trade or vault operation can use it. A SoFi operation cannot introduce a new token by naming an asset id, so What closes it, and it needs no new proof system. The creation operation carries, or commits to, the ordinary SMT inclusion proofs against the creator's actual validated predecessor root — That also explains this PR cleanly: Recorded as spec §44.5, with §19.8 corrected to state the bound rather than imply a wider one. One enforcement question I could not answer from sourceI could not find where the pre-add rule is enforced on the SoFi resolved path, and I would rather ask than assume.
So either the rule is enforced at a layer I have not found — the device-level token registry, or the market policy being a content-addressed object the vault commits — or it is the second half of the same binding F10 owes. Which is it? |
cryptskii
added a commit
that referenced
this pull request
Sep 22, 2026
`SofiVaultCreate` already planned two real balance debits against the
admitted `R_econ` and bound the funded AMOUNTS to the genesis reserves,
on the owner's path and on foreign walks alike. Five other facts it
stated were taken on the caller's word.
The sharpest was the funding ASSETS. `funding_a/b_policy_commit` went
straight into `pair_legs`, which checks only canonical order and
non-zero, and `write_set.rs` named `market_policy` nowhere. So a
creation could debit X and Y while declaring a market in A and B — and
a later close credits the owner the MARKET's pair, which it never
funded. 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.
Only the KEPT error variants were checked for remaining references, 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.
Core now refuses unless all of it holds, before any debit is planned:
the three preimages strictly decode; the owner coordinates are the
authenticated local ones; `create_position` is the position the
operation actually lands at; the record names the vault the preimage
derives; `genesis_root` is recomputed rather than accepted; the funded
amounts are the genesis reserves; the state's owner coordinates equal
the preimage's; the carried policy re-addresses to what the state
commits; and the decoded pair is the pair being funded.
The operation carries `market_policy_preimage`, so acceptance is a
function of the operation's bytes and the authenticated pre-state
alone — no resolver, no storage availability, no foreign-walk liveness
between a local decision and its answer. 72 fixed-width bytes against
the 49,856-byte signature already there. Coverage is automatic:
`operation_signing_bytes` is the whole canonical encoding with the
signature cleared, so one line in the encode arm is necessary and
sufficient — and a test proves it by altering only that field after
signing.
No decode-and-re-encode check. `MarketPolicy` is 72 bytes with no
optional position, its decoder pins the envelope and the beta family
before reconstruction, enforces `a < b` and refuses trailing bytes, so
`encode(decode(P)) == P` always and the assertion would have no
reachable rejection case.
ADDRESS EQUALITY AND PAIR EQUALITY ARE SEPARATE BINDINGS. 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 creation fixture now takes the MARKET pair separately from the
FUNDING pair. A fixture that conflated them could not express the
defect, which is why seven existing tests passed over it.
cryptskii
added a commit
that referenced
this pull request
Sep 22, 2026
`SofiVaultCreate` already planned two real balance debits against the
admitted `R_econ` and bound the funded AMOUNTS to the genesis reserves,
on the owner's path and on foreign walks alike. Five other facts it
stated were taken on the caller's word.
The sharpest was the funding ASSETS. `funding_a/b_policy_commit` went
straight into `pair_legs`, which checks only canonical order and
non-zero, and `write_set.rs` named `market_policy` nowhere. So a
creation could debit X and Y while declaring a market in A and B — and
a later close credits the owner the MARKET's pair, which it never
funded. 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.
Only the KEPT error variants were checked for remaining references, 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.
Core now refuses unless all of it holds, before any debit is planned:
the three preimages strictly decode; the owner coordinates are the
authenticated local ones; `create_position` is the position the
operation actually lands at; the record names the vault the preimage
derives; `genesis_root` is recomputed rather than accepted; the funded
amounts are the genesis reserves; the state's owner coordinates equal
the preimage's; the carried policy re-addresses to what the state
commits; and the decoded pair is the pair being funded.
The operation carries `market_policy_preimage`, so acceptance is a
function of the operation's bytes and the authenticated pre-state
alone — no resolver, no storage availability, no foreign-walk liveness
between a local decision and its answer. 72 fixed-width bytes against
the 49,856-byte signature already there. Coverage is automatic:
`operation_signing_bytes` is the whole canonical encoding with the
signature cleared, so one line in the encode arm is necessary and
sufficient — and a test proves it by altering only that field after
signing.
No decode-and-re-encode check. `MarketPolicy` is 72 bytes with no
optional position, its decoder pins the envelope and the beta family
before reconstruction, enforces `a < b` and refuses trailing bytes, so
`encode(decode(P)) == P` always and the assertion would have no
reachable rejection case.
ADDRESS EQUALITY AND PAIR EQUALITY ARE SEPARATE BINDINGS. 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 creation fixture now takes the MARKET pair separately from the
FUNDING pair. A fixture that conflated them could not express the
defect, which is why seven existing tests passed over it.
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.
Vault genesis acceptance is formal only
genesis_acceptedwas a twelve-conjunct predicate that took a presented creation operation and an owner root and returned a vault id. It could never acquire a production caller, becauseVaultCreationcarries no asset commitments: proving the creation leaf establishes the amounts and never which balances were debited, so a caller could hand in anA/B-shaped sibling of an operation that actually debitedX/Y.Three artifacts disagreed about what to do. A CI gate failed the build on any production caller. The G1 baseline told R14 to wire it or delete it. Spec §28.5 and §30.1 required it. Wiring it failed the gate; deleting it contradicted the spec.
Per the ruling in §44.4: the standalone production predicate was the stale piece, not the gate.
What goes, and what does not
Deleted from Rust:
genesis_accepted,CreationFunding, the eightGenesisErrorvariants only it raised, and its six tests. The three variantsbuild_vault_createactually uses stay, and the enum's doc now says what it is rather than what it was.The rule is not deleted. It is stated in the formal layer, which already carried it:
GenesisAcceptedandgenesis_requires_validated_creationin Lean,GenesisCanonicalOnlyIfCreationValidin TLA.ci/sofi_genesis_acceptance_binding.shis repurposed to keep both halves true — no Rust predicate, and the formal definitions still present. A deletion that quietly took the statement with it would be the same hole by another route.What production actually does, stated plainly
It recognizes, it does not accept. A trader fetches a vault's genesis by its locator and keeps the first candidate whose recomputed
vault_idis that locator, then comparesgenesis_root(v, state)against the parent root its own precommit names.vault_idisH(tag ‖ G_o ‖ DevID_o ‖ p_create)and does not depend on the vault state. So those three public coordinates are enough for any party to index a preimage with arbitrary reserves and policies under the right locator, and the recognizer keeps whichever arrives first. Nothing yet binds a genesis to the owner transition that funded it.This is not an argument from reading. The TLA fault
_RegisteredGenesisAcceptedmodels a walk that starts from a merely stored genesis, which is exactly what production does, and it violatesGenesisCanonicalOnlyIfCreationValidover 1,758,084 states: a vault's parent is consumed though its creation was never validated. Closing it is F10'sVerifiedVaultCreation, bound to the exact accepted owner transition atp_create. §19.8 now records the gap instead of implying it is closed.Controls
The second passed on its first run: the gate grepped for the bare name, and a use site still spelled it after the definition was renamed. It now requires the definition form. That is the third time in this step that matching a spelling instead of the thing produced a green gate, and it is the same defect the reachability gate carried for thirteen steps.
Gates
sofi::175/0. SDK (release,--features test-utils):sdk::sofi_*48/0.make lintexit 0;ci/production_safety_checks.shpassed; G1 baseline 7 → 6 lines.Spec
§19.8 gains the rule that this predicate has no Rust form and why, with the executed fault. §28 step 5 and §30 step 1 say recognize rather than accept. §41.3's row records the deletion.