chapel: real-corpus speedup bench (10-30s prover invocations)

[hyperpolymath]

Surfaced by the Wave-1 MRR baseline (#148) and L2.3 ADR (PR #154).

Problem

The current `bench_mrr` uses three trivial-success fixtures (Coq, Lean, Idris2). On these, each prover invocation returns in 200-700 ms, so cofork-overhead dominates and parallel strategies look similar-or-worse vs sequential. The L2.3 cancel-token preemption gain is structurally present but invisible.

Acceptance

• A fixture set of 5-10 goals that each take 10-30 s in their native prover (mid-difficulty SMT / Coq / Lean / Idris2).
• Bench reports per-strategy wallclock with multiple succeeding provers per goal.
• Speculative << bestof shown quantitatively (target: ≥ 5×).
• L2.3 preemption gain visible in the numbers.

Gated on

• Idris2 env-hook and Agda filename-hook issues so the fixture set isn't artificially restricted to Coq + Lean.
• The L3 corpus hand-off (per chapel-rehab ADR Wave-3 plan).