sofi: R6, the producer fails closed

[cryptskii]

R6 — the producer fails closed

Rebuild step R6 of the SoFi build order (spec §44): the producer validates with the evidence it acquired and stops on anything but Valid (rule T5, gate G5).

What is built

The draft (sdk/sofi_sdk.rs): builds the preimage, refuses what beta will not execute through preimage_admissible (now wired; its G1 baseline line is burned), and runs validate over the evidence the caller acquired (R5). Ok builds the draft. Invalid is BuildError::StaticallyInvalid(reason). Unavailable is the new BuildError::Unavailable(Missing): no PrecommitDraft exists, so nothing is published, exercised or advanced, and what is missing is named. The three-valued conjunction keeps missing evidence from hiding a refusal and from passing for one.

route_validation stays on the G1 baseline, retagged R12: it is the verdict-only wrapper the resolution ladder consumes; the producer needs the reason, which only validate carries.

Shared fixtures (sdk/sofi_test_fixtures.rs, cfg(test)): whole operations built the way a trader builds them, against vaults at their genesis — VaultAtGenesis (state, genesis preimage, the three policies; publishes and indexes them on the fake fleet), RouteFixture::swap(n) and RouteFixture::close() with real trees, Fold(T°, E) for the realize root, and acquire. The evidence tests (R5) and the producer tests now share them, because a producer that fails closed can only be exercised with evidence that was actually fetched.

Formal side, in tandem

lean4/DSMSofiStorage.lean §13 (R6): Verdict.and, the three-valued conjunction of sofi::conformance::Validation::and; proceeds. Theorems: invalid_dominates_and_unavailable_never_becomes_invalid (the Core test's twin), unavailable_stops_the_producer, missing_evidence_never_hides_a_refusal, the_producer_proceeds_only_on_valid. No new TLA model.

Correspondence and controls

Property	Lean	Rust
Unavailable stops the producer; nothing produced	unavailable_stops_the_producer, the_producer_proceeds_only_on_valid	SDK unavailable_stops_the_producer_and_nothing_is_produced (G5: each policy withheld, then the genesis)
missing evidence never hides a refusal	missing_evidence_never_hides_a_refusal, invalid_dominates_and_unavailable_never_becomes_invalid	Core invalid_dominates_and_unavailable_never_becomes_invalid; SDK missing_evidence_never_hides_a_refusal
the producer builds over acquired evidence	—	SDK an_exercise_is_signed_twice_and_p_travels_with_its_signature, a_two_hop_route_that_chains_builds, a_close_is_the_same_variant_and_only_the_origin_owner

Mutation controls executed (each restored afterwards):

• Rust: the producer proceeding on Unavailable (the pre-R6 arm) → unavailable_stops_the_producer_and_nothing_is_produced red.
• Lean: Verdict.and reading Unavailable as its other conjunct → unavailable_stops_the_producer and the_producer_proceeds_only_on_valid fail to check.

Gates

• SDK (release, --features test-utils): sdk::sofi_evidence sdk::sofi_sdk 23/0. Core: sofi::admission sofi::conformance 3/0.
• Lean: DSMSofiStorage.lean kernel-checks with -DwarningAsError=true.
• make lint exit 0; ci/production_safety_checks.sh passed (sofi reachability: 63 pub fn reachable, 17 in the baseline; G2 script green).

Spec

§44.2 gains the R6 row.