feat(sofi): the vault head past its genesis

[cryptskii]

The vault head past its genesis

A vault's leaves were only fetchable at R_0. acquire_evidence gave up on any vault whose core named another root, so a second trade against the same vault could never be validated by anyone — and it gave up silently for a vault no core names, loading genesis leaves as if that were the case.

Per the ruling in §44.4: replace the responsibility. What a later acquisition consumes is leaf preimages, which is why a node store could never have served this and why R14 deleted it rather than wiring it.

Core

vault_post_states (CORE/sofi/validation.rs) is the vault side of R13's trader_post_states. For every vault the operation touches it recomputes the post state from the pre state the evidence holds and the settlement's own terms, binds it to the post value that vault's core states, and takes the root from the fold against the pre-root the core states — the same value the verdict computes and then discards.

It decides no canonicality. advance_resolved already selected the state; this only says what the state is.

Each record carries both ends of its chain link, pre_root at pre_generation and the post root at generation. A store of post roots alone is a set, and a parent's status is asked about a generation.

The store

SDK/storage/client_db/sofi_vault_head.rs:

Table	Holds	Why
sofi_vault_root	(vault, generation) → root, forever	a parent's status is asked about a generation
sofi_vault_leaf	the current head's leaves with preimages, replaced wholesale	evidence needs preimages, and a mixture of two generations is not a tree

record_resolved_with_conn runs inside the admit transaction, so a head and the position that chose it cannot disagree. It reads the previous leaves through the caller's transaction, because the admit path already holds the connection and a second acquisition would deadlock rather than fail.

A read is checked, never trusted. leaves_at_head rebuilds the tree from every stored leaf and requires the recomputed root to equal the recorded one. That equality is what detects an incomplete record: a vault another trader moved between this device's trades leaves it missing their relationship leaf. An incomplete record yields nothing, so Core answers Unavailable and the position waits rather than standing on a state this device never established.

acquire_evidence serves R_0 from the genesis and past it from that store, requiring the record to be the head the core was built on. A vault named by no core is now skipped rather than loaded as if at genesis.

Controls

Each run alone for attribution, each restored byte-identical.

Mutation	Test that goes red
The post state is not bound to what V° states	a_vault_core_stating_another_post_state_yields_no_head
The root is the pre-root rather than the fold's	vault_post_states_are_recomputed_and_bound_to_the_stated_values
leaves_at_head skips the root check	a_vault_record_that_cannot_reproduce_its_own_root_is_not_evidence
The predecessor row is not written, so the chain is a set	a_resolved_route_leaves_the_vault_head_the_next_trade_stands_on

The first did not land on its initial run: the marker did not match after formatting, so those passes were the unmutated tree. Re-run grep-verified, and recorded rather than dropped.

Two of the tests also caught my own errors before the mutations did. One asserted that the vault's relationship leaf sits at a different key from the trader's; it does not — one key derivation, two trees, and the values differ in shape. The other asserted a leg both final on this operation's commitment and consumed by another, which the ladder rightly called Realized.

Gates

• Core (release): sofi:: 156/0, two tests new; tests/sofi_v8_independent 17/0. SDK (release, --features test-utils): sdk::sofi_* 53/0, two tests new; storage::client_db 388/0.
• make lint exit 0; ci/production_safety_checks.sh passed; G1 84 reachable, 0 baselined.

A dead function this branch introduced, and removed

record_genesis_with_conn had exactly one occurrence in the tree: its own definition. No caller, not even a test.

It also had no distinct responsibility. record_resolved_with_conn already writes generation zero as the pre-side of the first resolved chain link, and a vault's evidence at its genesis is served by vault_leaves_at_genesis from the accepted genesis object rather than from this store — so the doc comment's claim, "without it the first trade's parent has no status", was false as written. That is the same shape as the dark tree store its sibling PR deleted: reachable from nothing, reading as live.

The gate did not catch it and structurally cannot. sofi_reachability scans CORE_SOFI = "/dsm/src/sofi/", so G1 proves Core production reachability, not SDK production reachability — a green G1 coexists with dead SDK capability, and as of today the whole SDK SoFi producer surface has no production caller. Closing that blind spot is ruled into the facade work (spec §44.6).

Still owed, and visible in the type

ParentStatus::Orphaned has no producer. Until one lands, a leg whose parent this verifier has not established is Unavailable and the position waits — never silently "not refuted", which is what the two booleans this replaced would have said.

The producer is the forward walk over successor cells — extend the recorded chain from its last contiguous root, applying vault_post_states per consumed attempt. It is decided per generation, never by absence from a chain. An earlier draft of this paragraph said a root absent from a chain complete to an open head is refuted; that is wrong, and I would rather say so before it is merged as a description of the next change. A head is open precisely so the next root can still arrive, so an absent root may be one an in-flight operation is about to realize — and refuting it answers Orphaned, a RouteImpossible arm, hence a permanent Void on a route whose only defect is that the verifier looked early.

The sound criterion is the ruling's own, against root_at(v, g): equal is Canonical, different is Orphaned, absent is Unavailable. R*_g is permanent once established — either consumed to produce g+1, or it is the head — which OneConsumerPerParent already model-checks across crash and recover, so the walk inherits its uniqueness rather than needing a new concurrency argument.

[cryptskii]

Correction to this PR's "still owed" paragraph

The body says the producer for ParentStatus::Orphaned is a chain walked complete to an open head, and that "a claimed root absent from a complete chain is then refuted."

That criterion is unsound, and I would rather say so before it is merged as a description of the next change.

A head is open precisely so that the next root can still arrive. Take a chain R*_0 … R*_n where R*_n is the open head, and a leg claiming parent R ∉ chain. R may simply be the root that the operation currently reserving R*_n's successor cell is about to realize — not yet canonical, but not refuted either. Absence would have declared it Orphaned, and Orphaned is a RouteImpossible arm, so that is a permanent Void on a route whose only defect is that this verifier looked early. That is the "unknown encoded as a verdict" failure the three-valued type was introduced to remove, reintroduced one layer up.

The sound criterion is the one in the ruling, per generation (§44.4 ruling 3): for a leg claiming (v, g, R),

root_at(v, g) == Some(R)  ->  Canonical
root_at(v, g) == Some(_)  ->  Orphaned      // a DIFFERENT root was established at that same generation
root_at(v, g) == None     ->  Unavailable   // the chain has not reached g; it waits

This refutes only against an established R*_g, and R*_g is permanent once established: it was either consumed to produce g+1, or it is the head, and a successor cell admits at most one realized consumption per attempt key. Absence never refutes — it waits.

Two consequences worth recording, both of which make the next change smaller rather than larger:

• The generation is already available and already bound. VaultPostState.pre_generation (this PR, validation.rs) carries it, taken from the pre state that acquire_evidence will only serve at a root it recorded — so the generation a leg's parent sits at is tied to the root, not asserted by the operation claiming it.
• root_at(v, g) is already the store's read (sofi_vault_head.rs), so the forward walk's only job is to extend the recorded chain until it covers g, not to prove a head open. The Open-vs-unread-leader distinction that read_attempt_cell currently collapses into CellResolution::Unresolved turns out not to be needed for this at all, so no new read is owed either.

Nothing in the code in this PR changes — vault_post_states, the store and the Unavailable the resolver returns today are all as described. It is the one forward-looking paragraph that was wrong.