Overview
Speculative window decoding is a take on branch prediction for QEC. The idea is a lightweight predictor guessing the cross-boundary matching for a decoding window so the pipeline can run ahead, and the full decoder then verifies lazily. The recent architecture literature (SWIPER at ISCA 2025 and relatives) have worked on a built the predictor side. This paper is about the verifier side of the pipeline.
Three questions, each answered on a reconstructed SWIPER-style harness (Stim rotated surface code, PyMatching reference decoder):
- How predictable is the boundary? Not "how good is my predictor" but rather a two-sided bracket on how well any predictor could do, with a synthetic known-entropy gate to validate the estimator itself.
- What does a misprediction cost? A worst-case blast-radius bound whose probability core is machine-checked in Lean 4 (no sorry, standard Mathlib axioms), with the physical reduction hypothesis kept explicit. A caveat here is the intuitive containment story (propagation needs a connected faulty path) was empirically refuted by an adversarial falsification harness before any proof. Containment is real, but the mechanism is global min-weight re-pairing, not faulty percolation. In other words falsify before you formalize.
- Who decides what to speculate, and what happens on a miss? A speculation-decision compiler pass (cost = predictability x slack - blast radius) and a decoder-agnostic predict/verify/recover runtime executor that measures as opposed to trusting the proxy.
Links
Citation
Malarchick, R. (2026). "The verifier side of speculative window decoding: a predictability bracket, a machine-checked blast-radius bound, and a decoder-agnostic recover loop." arXiv:2607.13062.