proof(agda): model the speculative CAS + cancel-token race; replace the trivial cancellation-safety lemma

CLAUDE.md

@@ -140,7 +140,7 @@ Shape, by area:
 - **Idris2 ABI**: `EchidnaABI.TacticRecord` (fixed-point confidence, total-order proofs, in-range round-trip lemmas) + sibling modules; type-checked on every push by `idris2-abi-ci.yml`.
 - **GNN integration**: graph construction (7 node kinds, 8 edge kinds), 32-dim local term embeddings, GNN inference client, hybrid GNN + symbolic scoring, Julia `/gnn/rank` with cosine fallback.
 - **Corpus identity**: `src/rust/corpus/canonical.rs` hashes a declaration's canonical type shape (`dk-shape-v1`) so the same theorem matches across provers without a synonym table — tier 1 keeps binders and sorts, tier 2 (`skeleton`) erases them for Isabelle/Why3. The Vector octad defaults to a 256-dim structural n-gram embedder (`echidna-corpus-structural-v2`); the 32-dim `HashEmbedder` is legacy/GNN-parity only. See `docs/CORPUS.adoc`.
-- **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` formalises soundness, completeness, and cancellation-safety with zero postulate / admit / believe_me. L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc).
+- **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` models the speculative CAS + cancel-token protocol over every interleaving and proves the winner is stable, really succeeded and is the first successful prover to reach the CAS, that preempted losers are inert and that a success always yields a winner (zero postulate / admit / believe_me; assumes sequentially consistent atomics). L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc).
 - **Wave-3 container infrastructure**: per-prover images in `.containerization/Containerfile.wave3`; weekly cron in `container-ci.yml` runs stub-sentinel detection across all 8 Tier-3 cells.
 - **Julia ML layer**: logistic-regression tactic prediction shipped; Flux.jl scaffolds for GNN/Transformer training present but not yet trained on real data — corpus ready under `training_data/`.
 - **Migrations in flight**: AffineScript → AffineScript-TEA (UI); npm → Bun (`echidna-playground`); CI workflow consolidation under the governance ruleset.

docs/bench/README.adoc

@@ -125,5 +125,6 @@ is currently measured anywhere.
 
 * `+docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc+` — the `+-5+`
   preemption contract and why it is distinct from `+-3+`.
-* `+proofs/agda/ParallelSoundness.agda+` — cancellation-safety.
+* `+proofs/agda/ParallelSoundness.agda+` — race-protocol model:
+  `+winner-stable+`, `+preempted-inert+`, `+cancel-after-win+`.
 * `+docs/handover/TODO.adoc+` — real-corpus speedup bench (#161).

docs/decisions/2026-05-30-chapel-l23-cancel-token.adoc

@@ -1,3 +1,3 @@
 == 2026-05-30 — L2.3 cancel-token preemption for speculative search
 
 ADR-style addendum to
@@ -86,6 +86,20 @@
 The Agda module’s header docstring is updated in this PR to spell out
 the L2.3 cross-reference.
 
+[NOTE]
+====
+*Superseded 2026-11-09.* The `+cancellation-safety _ = tt+` lemma quoted
+above held by definition (`+true ∨ x = true+`), covered only index 0 and did
+not model the CAS, the token or any interleaving, so it did not establish
+the claim made for it. `+proofs/agda/ParallelSoundness.agda+` now has a
+layer B: a small-step model of this procedure, run over every interleaving
+of `+done i+` and the cancel write. It proves `+winner-stable+`,
+`+preempted-inert+`, `+cancel-after-win+`, `+race-sound+`, `+race-complete+`,
+`+winner-is-first+` and `+race-agrees+`, assuming that Chapel's atomics are
+sequentially consistent. The paragraphs above are kept as the record of
+the original decision.
+====
+
 The CAS itself is the linearisation point: any prover whose poll
 observes `+cancelled = true+` ran AFTER the winning CAS. The
 happens-before edge from `+winnerIdx.compareAndSwap(-1, i)+` →