sofi: R11, the exercise

[cryptskii]

R11 — the exercise

Rebuild step R11 of the SoFi build order (spec §44): the exercise object (Section 17.5), written to every successor key of a route; nothing but an exercise naming the key counts; discharges P1 (OnlyExercisesCount).

What is built

Core.

• Class SOFI_EXERCISE = 0x005E. The spec said 0x005D; R4 had already allocated 0x005D to the native-reserve credit source (class_discriminants_do_not_collide pins it), so the exercise takes the next free discriminant and the spec now says so.
• SofiExercise (wire/objects.rs): the signed envelope of F, the signed envelope of P, P(E), every G_j in leg order, every closure object in reference order; a strict codec bounded per part and as a whole by MAX_EXERCISE_BYTES, a member's cell value cap.
• sofi/exercise.rs: recognize_exercise — the parts rebuild and are bound to one another (F is P's by PrecommitId; P(E) recomputes the E P commits; the witnesses are P's own, one per leg, and together exactly the set F commits; one closure object per reference); exercise_names_key — the recognized view at K^(a) of v at R_n: an exercise whose F names (v, a) in its attempts and whose P names (v, R_n) in its legs, anything else at the key being nothing; attempt_resolution — SuccessorResolution(K) as the ladder reads it: the E of the exercise that won, Final or LeaderHeld, else Unresolved, and no key is ever dead.

SDK, sdk/sofi_exercise.rs. build_exercise over the evidence conformance was decided on (the witnesses derived from P and the shadows P(E) commits; a closure object the evidence does not hold is an error, because the exercise carries the closure); write_exercise — every leg's K^(a_j) of v_j at R_j, the leader of storage_seed(v_j, R_j) first and every other member after, under TAG_DSM_SOFI_SUCC_CELL_V2; read_attempt_cell — raw reads, the leader from the vault's seed over the committed set, the recognized view, then the ladder's CellResolution with the exercise. Any party may write (P2); the member decides nothing.

The R9 test rig (a signed two-leg route with real setups) moves into sofi_test_fixtures as SignedRoute/signed_route, shared by the R9, R10 and R11 tests.

Gate G1. successor_attempt_key is burned. next_attempt and next_generation were tagged R11 but R11 takes the attempts from F; they are retagged R12 (the walk advances the counter) and R13 (the resolved vault state's successor generation).

Formal side, in tandem

• TLA DSM_SofiSuccessorCells.tla: ExerciseNamesItsKey, RecognizedAttemptNamesItsKey, UnrecognizedBytesNeverOccupy with the _ExerciseCountsAnywhere* and _RecognizeAnyBytes* faults — pre-existing since step 3. Re-executed: _ExerciseCountsAnywhere → Error: Invariant ExerciseNamesItsKey is violated (423,664 states generated); _ExerciseCountsAnywhereRecognized → Error: Invariant RecognizedAttemptNamesItsKey is violated.
• Lean DSMSofiSuccessorCells.lean, THE EXERCISE (new): namesKey, occupant, an_exercise_counts_at_one_key_per_vault (an exercise whose legs each name one vault once counts at one key per vault), only_an_exercise_naming_the_key_counts (whatever junk precedes it — unrecognized bytes, exercises naming other keys — the first exercise naming the key is the occupant). Mutation 8 (namesKey ignoring the attempt) executed: an_exercise_counts_at_one_key_per_vault is rejected by the kernel (module exit 1); restored.

Correspondence and controls

Property	Formal	Rust
an exercise names its key through its own legs; it cannot count elsewhere	Lean an_exercise_counts_at_one_key_per_vault; TLA ExerciseNamesItsKey, RecognizedAttemptNamesItsKey	Core an_exercise_names_exactly_the_keys_its_fulfillment_and_precommit_name; SDK an_exercise_cannot_count_at_another_key
only an exercise naming the key counts (P1)	Lean only_an_exercise_naming_the_key_counts; TLA UnrecognizedBytesNeverOccupy	SDK only_an_exercise_naming_the_key_counts; Core a_successor_key_resolves_to_the_e_of_the_exercise_that_names_it_or_stays_open
the parts are one operation's, bound by hashed preimages	—	Core an_exercise_whose_parts_are_not_one_operations_is_nothing, an_exercise_round_trips_and_rebuilds_into_bound_objects
written to every successor key, leader first	TLA FinalRequiresLeader (cells)	SDK an_exercise_is_written_to_every_successor_key_at_its_leader

Mutation controls executed, each restored afterwards:

• Rust M1 (SDK layer): the cell read counts any exercise, whatever key it names → only_an_exercise_naming_the_key_counts red (a foreign exercise first at the leader wins the cell and masks the route's own).
• Rust M2 (SDK layer): the exercise written to the first leg only → an_exercise_is_written_to_every_successor_key_at_its_leader red.
• Rust M3 (Core): naming the key ignores the attempt → an_exercise_names_exactly_the_keys_its_fulfillment_and_precommit_name red.
• Rust M4 (Core): the witness set not bound to F → an_exercise_whose_parts_are_not_one_operations_is_nothing red, on the wrong-shadow witness case.
• Rust M5 (Core registry): SOFI_EXERCISE aliased to 0x005D → class_discriminants_do_not_collide red: class 0x005d allocated twice: CREDIT_SOURCE_NATIVE_RESERVE_RELEASE and SOFI_EXERCISE. The registry uniqueness invariant is executed, not assumed.
• Lean 8: namesKey ignoring the attempt → an_exercise_counts_at_one_key_per_vault rejected (module exit 1).
• TLA: _ExerciseCountsAnywhere → ExerciseNamesItsKey violated; _ExerciseCountsAnywhereRecognized → RecognizedAttemptNamesItsKey violated.

Control-mapping findings on the way: M1 was first run against an_exercise_cannot_count_at_another_key and stayed green — Core's attempt_resolution re-applies exercise_names_key to the winning bytes, so a permissive SDK recognizer cannot make a wrong key resolve; what it CAN do is let a foreign exercise win the cell and mask the route's own, which is only_an_exercise_naming_the_key_counts. M4 first stayed green because the test lacked the one case the set check is load-bearing for: a witness bound to the right leg, P and E but claiming another shadow — the per-leg binding does not see the shadow, only the ids do; that case is now in the test.

Gates

• Core (release): sofi::exercise 4/0 (sofi::registration 2/0 unchanged), tests/sofi_v8_independent 17/0. SDK (release, --features test-utils): sdk::sofi_exercise 3/0, sdk::sofi_register 9/0, sdk::sofi_publish 6/0.
• Lean: DSMSofiSuccessorCells.lean kernel-checks with -DwarningAsError=true; the two new theorems print their axioms. TLC as above.
• G1 (ci/sofi_reachability.py): 82 pub fn reachable, 11 in the baseline; ci/storage_is_dumb.sh OK.
• make lint exit 0 (after cargo fmt); ci/production_safety_checks.sh passed.

Spec

§17.5 carries the class correction and the R11 code block; §44's R11 row says 0x005E; §44.2 gains the R11 row.