sofi: R4, the Core read adapter, and the faucet becomes a release of the native ERA reserve

[cryptskii]

R4 — the Core read adapter, and the beta faucet becomes a release of the native ERA reserve

Rebuild step R4 of the SoFi build order (spec §44), plus the owner's R4 addition (§44.3, 2026-09-20): the dead SoFi-named counting goes, and the beta faucet's quorum-backed ticket register is replaced by the native ERA reserve — one canonical lineage per network, released leader first, replicated to every member in the background.

What is built

Core read adapter (R4 proper). sofi::arith::resolve_objects derives Final / LeaderHeld / Open / Unavailable from raw member reads over a recognition predicate; read_economic_root_cell now runs on it. Nothing is counted; the leader's read decides, and an unread leader is Unavailable, never empty.

The native ERA reserve (CORE/economic/native_reserve.rs, new):

• R_0 = NativeReserveState { era_reserve_id(network), ERA, remaining = 80,000,000,000, generation 0, S } — computed from public inputs, never stored.
• One transition: release_constructible(parent, release) → remaining' = remaining − amount, generation' = generation + 1. No mint arm, no creator withdrawal; an overdraft or a zero release is not an object naming the cell and counts as nothing.
• The release names its recipient directly. ReleaseSource::FaucetClaimant { claimant_public_key } is the beta source: the recipient IS the claimant; the seam for a later EmissionLotteryRecipient is another arm of that enum, not a change to the mechanics.
• Cells: K(reserve, R_n), seed (reserve, R_n), leader = FisherYates(seed, S)[0] over the committed set; recognize_release, resolve_successor, walk_lineage.
• Credit source 0x005D CreditSourceNativeReserveRelease; 0x0030 burned. Operation::FaucetClaim { reserve_id, generation } (tag 31, byte-identical layout). The provenance arm re-runs the construction predicate against the parent state the walk validated, then checks recipient = the identity under validation with the proven AK, position + operation-digest binding, the canonical set, and the evidence address.

Finality vs replication (owner ruling, §44.3 item 11). Finality is the deterministic leader plus two other members holding the same recognized object — a release final on three members is exposed to the recipient at once. Replication is all-member, asynchronous: sdk::native_reserve::carry_pending_releases runs in the artifact sync pass until every member holds each successor. An unavailable non-leader never blocks a claim.

Committed set, never live membership. S_commit(R_n) decides R_n → R_{n+1}: every reserve state commits storage_set_id, release_constructible refuses a release naming any other set, and the SDK's read_successor / write_release refuse a StorageSet whose id is not the state's before computing a leader or touching a member (committed_set_only). S_live is only ever the carry's target; nothing the carry writes is read back into resolve_objects, which reads the committed members only.

SDK. sdk/native_reserve.rs (memoised walk from R_0, leader-first write, release_at for the live resolver, the carry), faucet_claim_flow.rs rewritten (walk to the head → sign once per parent root → write leader first → read back Final of our bytes; a lost race re-walks; a crash after finality is resumed from the memo), client schema v14 → v15.

What is deleted

Core: economic/faucet.rs, economic/cell_observation.rs (observe_cell, canonical_quorum), dlv/beta_storage_profile.rs (sofi_beta_quorum_for, SOFI_BETA_QUORUM, dev_only_single_node_quorum), RootRegisterProfile.quorum, AuthenticatedCaller / verify_claim_attribution / MAX_CLAIM_BYTES. SDK: the one-shot claim machinery (ClaimFanout, classify_one_shot_response, answer_counts_for, MemberEcho, submit_one_shot_claim, read_register_cell), the ticket fake register, select_ticket. Node: api/economic/faucet_ticket.rs, the faucet_ticket_claims table on both backends, node.network_id, db/write_once_properties.rs, tests/economic_register_conformance.rs. Formal: DSM_EconRegisterObservation.tla and its 6 configs, the §10 quorum theorems of DSMEconomicSmtSeparation.lean. Scripts: init_faucet_dlv.sh (wrote a 1 MB dlv_slots quota row, nothing the faucet ever read).

Kept as ruled (§44.3 item 9): StorageSet::quorum / publication::quorum_for — artifact delivery and identity publication, unrelated subsystems.

Formal side, in tandem

• tla/DSM_NativeReserveRelease.tla (new, exhaustive): Conservation, NoValidReserveTransitionMints, NoCreatorBackout, RecipientIsClaimant, ReleaseAccounting, FinalRequiresLeader, AtMostOneFinal, LeaderFromCommittedSet, UnrecognizedBytesNeverOccupy, ThreeHoldersIsFinal, UnavailableNonLeaderNeverBlocks, ReplicasDoNotAlterTheWinner. 8 fault configs + 3 reachability configs; every one violates exactly its named invariant under TLC. Runner: 69 → 75 standard specs.
• lean4/DSMNativeReserve.lean (new): the one transition, Reach with a single step constructor (no creator backout by shape), total_era_is_conserved, leader-first winner/final. Lean modules 15 → 16.

Correspondence and controls

Property	TLA	Lean	Rust
reserve_after = reserve_before − release	Conservation, ReleaseAccounting	a_release_conserves_the_reserve	Core a_release_conserves_the_reserve
no valid transition mints	NoValidReserveTransitionMints	no_valid_reserve_transition_can_mint_era, an_overdraft_is_refused	Core no_valid_reserve_transition_can_mint_era; wire a_release_that_is_not_its_parents_successor_funds_nothing
total ERA conserved	Conservation	total_era_is_conserved	Core total_era_is_conserved_along_the_lineage; wire credits_funded_along_a_lineage_sum_to_what_the_reserve_released
no creator backout	NoCreatorBackout	no_creator_backout (single constructor)	Core no_creator_backout_the_only_transition_is_a_release_to_its_recipient
FaucetClaim(A,x) ⇒ recipient = A	RecipientIsClaimant	faucet_claim_names_its_claimant_as_recipient	wire faucet_claim_names_its_claimant_as_recipient
finality without the leader is impossible	FinalRequiresLeader	finality_without_the_deterministic_leader_is_impossible	Core + SDK fake fleet, same name
replicas do not alter the winner	ReplicasDoNotAlterTheWinner	additional_replicas_do_not_alter_the_winner	Core additional_replicas_do_not_alter_the_winner
leader/finality over the committed set, not live membership	LeaderFromCommittedSet	—	SDK a_set_other_than_the_one_the_reserve_commits_never_names_a_leader
an unavailable non-leader never blocks; carry reaches it	UnavailableNonLeaderNeverBlocks, _AllMembersHoldReachable	three_holders_is_final	SDK an_unavailable_non_leader_never_blocks_finality_and_the_carry_reaches_it_later

Mutation controls executed (each restored afterwards):

• TLC: the 11 falsification configs above (FinalRequiresLeader, LeaderFromCommittedSet, ThreeHoldersIsFinal, UnavailableNonLeaderNeverBlocks, NoValidReserveTransitionMints, Conservation, NoCreatorBackout, RecipientIsClaimant, and the three reachability claims).
• Lean: dropping amount ≤ remaining fails a_release_conserves_the_reserve, release_never_exceeds_the_reserve, an_overdraft_is_refused, total_era_is_conserved; dropping recipient = claimant fails faucet_claim_names_its_claimant_as_recipient; counting without the leader fails finality_without_the_deterministic_leader_is_impossible.
• Rust (each restored, restored tree re-run green): dropping the overdraft refusal in release_constructible → no_valid_reserve_transition_can_mint_era and a_release_that_is_not_its_parents_successor_funds_nothing red; dropping the recipient/AK check in the provenance arm → faucet_claim_names_its_claimant_as_recipient red; letting sofi::arith::resolve fall back to any holder when the leader holds nothing → three_non_leaders_agreeing_is_not_final, Core finality_without_the_deterministic_leader_is_impossible and the SDK fake-fleet twin red; dropping committed_set_only → a_set_other_than_the_one_the_reserve_commits_never_names_a_leader red.

Gates

• Core (release, --features testing): lib filter economic::native_reserve sofi::arith economic::write_set economic::provenance economic::credit types::operations types::device_state 134/0; integration native_reserve_wire 12/0, economic_admission_lifecycle 14/0, economic_write_set 23/0, economic_lineage_register 12/0, economic_provenance_semantics 3/0, economic_peer_evidence 9/0, economic_authorized_issuance 12/0, economic_root_primitives 20/0, domain_encoding_byte_preservation 9/0, universal_faucet_invoke_test 1/0.
• SDK (release, --features test-utils): sdk::native_reserve 4/0, handlers::faucet_flow_tests 6/0, plus storage_io/client_db filters 15/0 total; faucet_claim 2/0, bearer_staging_fail_closed 2/0.
• Node (release, sqlite): db::cell_properties 6/0, cells_keep_everything 6/0, immutable_store_round_trip 4/0; ci/storage_is_dumb.sh OK.
• TLC: DSM_NativeReserveRelease.cfg exhaustive, 1,768,960 distinct states, no error; all 11 falsification configs violate exactly their invariant. Lean: DSMNativeReserve.lean and DSMEconomicSmtSeparation.lean kernel-check with -DwarningAsError=true.
• make lint exit 0; ci/production_safety_checks.sh passed (sofi reachability: 60 pub fn reachable, 19 in the baseline).
• Postgres job: the counted floor moves 13 → 10 (the faucet write-once suite is gone; cells 6 + durability 4 remain).

Frontend: proto bindings regenerated (npm run proto:gen); the faucet.claim route and its request/response are unchanged. Android: unchanged.

Spec

§44.2 gains the R4 row; §44.3 carries the owner's R4 addition and the finality-vs-replication ruling; Appendix A reconciled (native supply is its own reserve lineage, not a Market DLV).