refactor: the unreached receipt verifier is deleted; its checks run on production's decisions

[cryptskii]

Owner ruling (2026-09-30): the unreached receipt verifier goes. Its checks are ported onto the production path first, then it is deleted.

Why

verification::receipt_verification::verify_stitched_receipt and its ParentConsumptionTracker had no production caller. That is recorded in CONFORMANCE §6.3 and §6.11, and in #1068's §6.44. Production decides a bilateral step with bilateral::offline:

• decide_prepare and decide_confirm on the receiver's side, decide_commit_ack on the sender's;
• a second child of one tip is refused because the receiver holds the tip it committed.

The verifier's only users were tests and tools/vertical_validation. So CI's attack suite, fork-exclusion property, Tripwire traces and TLA replays were reporting on code production never runs.

What changes

The validation harness runs production's step (tools/vertical_validation/src/live_device.rs):

• the sender proposes on the shared tip it holds (h₀ from initial_chain_tip_from_device_ids, then each committed successor) and signs the step commitment (σ_A);
• its stitched receipt is signed by a per-step EK that its chain head certifies over the parent tip;
• the receiver decides with decide_prepare and decide_confirm, against its held tip and the keys its contact pins, including a real Kyber identity binding;
• both devices commit and move the shared tip.

Every judge is ported onto it.

Check	Production refusal it asserts
double spend (second child of one tip)	decide_prepare → StaleTip
step replay	StaleTip
receiver behind (a device restored from before a step)	StaleTip
wrong-key and garbage σ_A	decide_prepare: "is not signed over its commitment by the pinned AK"
receipt under an EK the sender's chain never certified	decide_confirm: "does NOT chain"
forged child root, bent path	decide_confirm: "do not fold"
fork_exclusion property; receiver_tripwire, tripwire_first_contact_binding, state_machine_fork_divergence traces	first child commits, second is StaleTip
TLA DSM replay (net_deliver)	every step delivered through the decisions
TLA Tripwire replay	the model's tips map onto the shared tips real devices hold; every model receipt is a step production accepts

Deleted from dsm:

• verify_stitched_receipt and its signature helper;
• ReceiptVerificationContext, ReceiptAcceptance and ParentConsumptionTracker;
• the tests that exercised only those, and the tripwire_parent_consumption trace.

dsm/tests/smt_tripwire_theorem.rs::theorem2_two_successors_same_parent_rejected now asserts the refusal through decide_prepare: StaleTip once h₁ is held, Consider while h₀ is held.

Evidence

• vertical-validation adversarial: 6/6; property-tests --iterations 5 --seed 42: 6/6; implementation-traces: 15/15; tla-check: all 91 specs. The Tripwire, DSM_tiny, DSM_small and DSM_system trace replays pass literal and direct.
• cargo test -p dsm -p dsm_vertical_validation --release: 1,630 passed, 0 failed.
• Mutation control: decide_prepare's stale-tip arm disabled turns theorem2_two_successors_same_parent_rejected and a_stale_proposal_says_whether_its_claimed_tip_recomputes red, and fails the double-spend, replay and receiver-behind attacks. Restored.
• cargo fmt --check, clippy --all-targets -D warnings (1.98.0), scripts/real_code_guard.py, ci/conformance_evidence.py: clean.
• Gemini gate: satisfied.

Records

• CONFORMANCE §6.45, new. The earlier findings in §6.3, §6.11 and §6.44 are marked resolved, and MR-DSM-0092's note is updated.
• Verification matrix:
  • The row for a second child now names decide_prepare, with the mutation result above.
  • The row for the old verifier's rule 2c is deleted: a receipt's parent root compared with a root the verifier expects has no production counterpart. MR-DSM-0028 and MR-DSM-0041 are Met on other evidence.

Not driven by the tool

A forged countersignature (σ_B) is judged by the sender's decide_commit_ack. Core's dsm::bilateral::offline::tests::an_ack_is_only_the_receivers_counter_signed_receipt refuses it.