sofi: R7, FulfillmentConformance as the full predicate of Part IV

[cryptskii]

R7 — Core FulfillmentConformance, the full predicate

Rebuild step R7 of the SoFi build order (spec §44): FulfillmentConformance(F) as Part IV §20.2 states it, three-valued, over what a verifier actually fetched, one named test per item.

What is built

The predicate (dsm/src/sofi/conformance.rs): fulfillment_conformance(F, σ_F, &ConformanceEvidence) -> FulfillmentConformance, which is Valid, Invalid(FulfillmentConformanceError) or Unavailable(ConformanceMissing). The eight items are evaluated and folded in item order: the first Invalid names the reason, else the first Unavailable names what is missing. So a withheld object can never hide a refusal, and nothing missing is ever read as one.

Two rules shape every arm. A fact about bytes in hand — an unsigned or non-verifying F, a key that is not P's, a non-canonical policy set, a hole in the attempts, legs that are not what P(E) derives, a setup that names another trader or vault or sits at or after p, a closure reference to a class no rule can address — is Invalid, permanently. A read that established nothing — P not fetched or fetched by another id, a P copy whose envelope does not verify (another envelope may), a preimage that does not recompute E, bytes at ρ that do not re-hash to ρ, a closure object that does not re-derive its reference, an earlier attempt key that is not Final — is Unavailable, never Invalid. A hostile relayer serving garbage cannot end a lineage with it.

• Item 1: the exact P (by PrecommitId, envelope verified with verify_precommit), q = p + 1 checked.
• Item 2: verify_fulfillment under F's own key, then key and algorithm equality with P.
• Item 3: the canonical set over the shadows P(E) commits (canonical_legs), in P's leg order.
• Item 4: attempts cover exactly P's legs, one per leg, none missing or repeated.
• Item 5: for a_j > 0, K^(a_j − 1) is Final on anything — a lost key counts, LeaderHeld waits, an unread key waits.
• Item 6: SetupRegistered per leg: Stored bytes at ρ that decode and re-derive ρ.
• Item 7: the setup names (G, DevID) and the leg's vault, with setup.position < p; P's (v, R, ρ) legs equal those P(E) derives.
• Item 8: recompute_e(P(E)) = P.E; every 𝒞_E^pre reference verified under its variant's rule (policy_object_address for content, claim_ref for a single-root claim, the SofiResolutionClaim fields for a conditional claim, setup_ref for a setup).

ConformanceEvidence derives Default only under cfg(test) (the G2 posture of Evidence); production builds it only from fetched bytes and resolved cells, keyed by ρ, by ValidationRef and by (v, a).

The producer's half. check_fulfillment_against_precommit stays as the pre-sign subset (items 1 to 4 before F is signed and before anything is stored) and is now built from the same per-item helpers as the predicate, so the two cannot drift; the_producers_pre_sign_check_is_the_structural_half_of_the_predicate pins that.

Small wire additions: SettlementBody::closure(), ValidationRef: Ord (a map key). The validation tests' real-P(E) rig moves into validation::fixtures (test-only, pub(crate)) and gains swap_fixture_with(hops, setup_ref_of, closure), so the conformance tests run over an operation whose legs carry the ρ of real setup bodies and whose closure names one object of every reference kind.

Formal side, in tandem

lean4/DSMSofiAtomicity.lean §10 (new): ConfEvidence (the twin of ConformanceEvidence), known (a fact about bytes) and fetched (a storage read), conformance (the eight items in order under allV; a P by another id is no P). Theorems:

• conformance_valid_iff — Valid ⇔ the structural Conforming over the exact P and P(E), F signed, every storage fact established.
• more_evidence_only_refines — Extends ev ev' → Refines (conformance ev) (conformance ev'): Invalid is permanent, Valid is never withdrawn, an unmade read is never a refusal.
• a_missing_p_waits_and_only_an_unsigned_f_refuses, unread_storage_is_unavailable_never_invalid.

TLA: TrueConformance in DSM_SofiFulfillment.tla now names its Rust twin; no configuration changes.

Correspondence and controls

Property	Lean	Rust
Valid exactly when everything is in hand and conforms	conformance_valid_iff	a_fulfillment_with_everything_in_hand_is_valid, item_1_… to item_8_…
more evidence only refines; Invalid dominates in item order	more_evidence_only_refines	invalid_dominates_unavailable_in_item_order, item_5_…, item_6_…, item_8_…
a missing P waits; an unsigned F refuses	a_missing_p_waits_and_only_an_unsigned_f_refuses	item_1_…, item_2_…
unread storage is Unavailable, never Invalid	unread_storage_is_unavailable_never_invalid	item_5_…, item_6_…, item_8_…

Mutation controls executed, each restored afterwards:

• Rust M1: LeaderHeld accepted as a permanent resolution → item_5_an_earlier_attempt_must_have_a_permanent_storage_resolution red.
• Rust M2: a missing setup read as Invalid → item_6_setup_registered_holds_for_every_leg red (invalid_dominates_unavailable_in_item_order does not reach setups and stayed green; the item test is the control).
• Rust M3: the key-equality check dropped → item_2_f_is_signed_under_the_key_p_committed red.
• Rust M4: a wrong-id P read as Invalid → item_1_the_referenced_p_is_available_verifies_and_q_is_its_successor red.
• Rust M5: any bytes satisfy a closure reference → item_8_the_preimage_and_closure_are_available_and_verify red.
• Lean 35: a missing P read as Invalid → a_missing_p_waits_and_only_an_unsigned_f_refuses and more_evidence_only_refines fail to check.
• Lean 36: an unfetched setup read as Invalid (fetched → known in item 6) → unread_storage_is_unavailable_never_invalid and more_evidence_only_refines fail to check.

Gates

• Core (release): sofi::conformance 12/0, sofi::validation 33/0, tests/sofi_v8_independent 17/0. SDK (release, --features test-utils): sdk::sofi_sdk 13/0.
• Lean: DSMSofiAtomicity.lean kernel-checks with -DwarningAsError=true; the four new theorems print their axioms.
• G1 (ci/sofi_reachability.py): fulfillment_conformance is added to the baseline (R9 wires it into the producer before F is written; R12 into the ladder) — the predicate lands ahead of both by the build order, and this is the one line the burn-down file gains; setup_ref is burned, reached through it.
• make lint exit 0 (after cargo fmt); ci/production_safety_checks.sh passed (sofi reachability: 64 pub fn reachable, 17 in the baseline; G2 script green).

Spec

§20.2 and §17.3 point at the predicate; §44.2 gains the R7 row.