sofi: R5, real evidence acquisition

[cryptskii]

R5 — real evidence acquisition

Rebuild step R5 of the SoFi build order (spec §44): Evidence is built only from fetched bytes, Default is test-only (gate G2), and every evidence item has its withheld and corrupted controls (gate G3).

What is built

Core. sofi::validation::Evidence derives Default only under cfg(test); Evidence::acquired is the one production constructor. EvidenceNeeds::of(preimage) states what a verifier must fetch — every trader key a core touches, and for every vault the core touches its state key and every touched key — and EvidenceNeeds::policies_of(state) names the three policy objects by class and address once the state is in hand. sofi::lineage::vault_leaves_at_genesis states the vault tree at R_0: exactly its state leaf, Absent everywhere else. New tag DSM/sofi/vault-genesis-object/v1, the immutable-store namespace of the exact genesis preimage bytes (registry 377 → 378).

SDK (sdk/sofi_evidence.rs, new):

• LocalLeaves: the verifier's own R_econ leaves, rebuilt and checked against the validated root before they can be evidence (of_validated from the leaf cache; checked for a caller holding leaves).
• fetch_vault_genesis: the genesis preimage under vault_genesis_locator(v) through the R1 index scan, recognized by Core — strict decode, vault_id() recomputed from the bytes and compared to the locator.
• acquire_evidence: trader leaf pre values from the local tree; vault leaf pre values from the genesis when the core's pre root is R_0; policy objects Stored on three members at the address the state commits. What is not fetched is absent and Core answers Unavailable. A vault past its genesis stays unfetched until the successor walk (R12).
• storage_io::read_stored_bytes: Stored by address.
• The producers draft_trade / draft_route / draft_close take &Evidence; sofi_sdk.rs no longer validates over a default.

Gate G2 script ci/sofi_no_default_evidence.sh, wired into ci/production_safety_checks.sh: Default on Evidence must be #[cfg_attr(test, derive(Default))], and no Evidence::default() may appear in production code (before the first #[cfg(test)], outside tests/).

G1 baseline: vault_genesis_locator now has a production caller; its line is burned down (19 → 18 entries).

Formal side, in tandem

lean4/DSMSofiStorage.lean §13 (the R1 module, extended): Evidence as address → bytes; acquire needs reads = the Stored bytes at every needed address and nothing else; need three-valued. Theorems: acquired_bytes_are_stored, nothing_is_defaulted, silence_acquires_nothing, missing_evidence_is_unavailable_never_invalid, acquisition_decides_nothing. No new TLA model: the interleaving statement is UnavailableNeverRejects in DSM_SofiSuccessorCells.tla.

Correspondence and controls

Property	Lean	Rust
acquisition holds only Stored bytes	acquired_bytes_are_stored	SDK acquired_bytes_are_stored
nothing is defaulted	nothing_is_defaulted, silence_acquires_nothing	SDK nothing_is_defaulted; G2 script
missing ⇒ Unavailable, never Invalid	missing_evidence_is_unavailable_never_invalid	Core missing_evidence_is_unavailable_never_invalid; SDK a_withheld_policy_object_is_unavailable_never_invalid (×3), a_vault_past_genesis_is_unavailable_until_the_walk
non-authenticating bytes are never an item	wrong_bytes_never_count (R1)	SDK bytes_that_do_not_authenticate_to_their_address_are_never_acquired
acquisition decides nothing; Core refuses the wrong object	acquisition_decides_nothing	SDK an_authentic_but_wrong_policy_is_acquired_and_refused_by_core
recognition recomputes the identity	kept_verifies, garbage_is_never_kept (R1)	SDK a_genesis_of_another_vault_under_the_locator_is_never_kept
the verifier's own leaves recompute its root	—	SDK local_leaves_must_recompute_the_validated_root, a_trader_leaf_cannot_be_withheld_from_the_verifiers_own_root
acquired evidence validates	—	SDK acquired_evidence_validates_a_first_trade_at_vault_genesis

Mutation controls executed (each restored afterwards):

• Lean: acquire defaulting an unread address to bytes → acquired_bytes_are_stored and silence_acquires_nothing fail to check.
• Rust: acquire_evidence filling an unfetched vault's leaves with Absent → nothing_is_defaulted red; Evidence deriving Default unconditionally → ci/sofi_no_default_evidence.sh red; fetch_vault_genesis recognizing a genesis without recomputing vault_id() → a_genesis_of_another_vault_under_the_locator_is_never_kept red.

Gates

• Core (release, --features testing): sofi::validation sofi::lineage common::domain_tags 59/0.
• SDK (release, --features test-utils): sdk::sofi_evidence sdk::sofi_sdk 21/0.
• Lean: DSMSofiStorage.lean kernel-checks with -DwarningAsError=true; the new theorems rest on propext/Quot.sound only.
• make lint exit 0; ci/production_safety_checks.sh passed (sofi reachability: 62 pub fn reachable, 18 in the baseline; G2 script green).

Spec

§44.2 gains the R5 row.