The verifier side of speculative window decoding: a predictability bracket, a machine-checked blast-radius bound, and a decoder-agnostic recover loop

Technical Summary: The Verifier Side of Speculative Window Decoding

Problem Statement
Real-time quantum error correction (QEC) faces a critical latency bottleneck. Syndrome rounds arrive on a fixed hardware cadence (approximately one microsecond for superconducting qubits), but decoders often cannot keep pace, allowing syndrome backlogs to grow until decoherence destroys the logical state. While "window decoding" splits the syndrome history into parallelizable chunks, adjacent windows remain serially dependent: the correction committed in one window determines the decoding problem for the next. Previous work, specifically SWIPER and ARTERY, attempted to remove this serial bottleneck using speculation: predicting cross-boundary decisions to allow downstream windows to start early, with full decoding running lazily to verify. However, these systems only implemented the predictor half (achieving ~90% accuracy) and lacked a rigorous verifier side. Consequently, four fundamental questions remained unanswered: the theoretical limit of prediction accuracy, the worst-case "blast radius" of a misprediction, whether speculation is worth the risk given those limits, and whether the full predict-verify-recover loop actually hides latency and recovers correctly on a real decoder.

Methodology
The authors constructed a reconstructed SWIPER harness using Stim (rotated surface code) and PyMatching (minimum-weight perfect matching, MWPM) to answer these questions. The methodology proceeds in four stages:

1. Predictability Bracketing: Instead of relying on a single heuristic predictor, the authors established an upper bound ("ceiling") on achievable accuracy using a radius-$R$ local MWPM decoder. This decoder uses only syndrome data within $R$ rounds of the boundary cut, treating open boundaries exactly as a window decoder would. This brackets the theoretical limit of what any predictor can achieve given local information.
2. Blast Radius Bounding and Falsification: The authors modeled the propagation of a misprediction (wrong dependency bits) through a window. They first established a worst-case temporal bound using a machine-checked probability core in Lean 4, conditional on a reduction hypothesis that a misprediction requires a faulty path to propagate. They then rigorously tested this hypothesis "shot-by-shot" against a sharp single-bit adversary to falsify the reduction mechanism.
3. Compiler Pass Derivation: Using the measured predictability and blast radius, a compiler pass was developed to derive an optimal restart policy. This pass operates on an abstract window dependency graph, annotating boundaries with speculation flags based on a cost model: $cost = predictability \times slack - blast\_radius$.
4. Runtime Execution and Decoder Agnosticism: A runtime executor was built to run the full predict-verify-recover loop on the harness. To determine which findings are intrinsic to the speculation framework versus specific to the MWPM decoder, the authors re-ran key experiments using a second, algorithmically distinct decoder: the Union-Find decoder (unweighted cluster growth).

Key Contributions and Results

• Predictability is Local and Near-Saturated: The cross-boundary decision is determined by roughly three rounds of syndrome on each side of the cut. A local MWPM with a receptive field of $R=3$ achieves ~0.999 accuracy, indicating that the ~90% accuracy of previous predictors (SWIPER) was not a fundamental limit but left a small, diffuse headroom (0.019 to 0.063 depending on code distance).
• Blast Radius is One (Temporal Containment): The worst-case probability of a misprediction propagating to the next window decays exponentially with the commit width $W$. At the standard width ($W=d$), the propagation probability is orders of magnitude lower than the logical error rate (e.g., $10^{-7}$ vs $10^{-5}$ at $d=7$). This establishes that the temporal blast radius is effectively one, meaning speculation adds no error floor.
• Refutation of the Faulty-Path Mechanism: The Lean 4 proof was conditional on the hypothesis that propagation requires a "faulty path" (a chain of errors connecting the flip to the cut). Shot-by-shot falsification showed this hypothesis is false: propagation occurs routinely without any faulty path near the flipped bit. The true mechanism is a global minimum-weight re-pairing, where the decoder re-routes an existing defect to the flipped bit because it is cheaper than local absorption. This mechanism is driven by degeneracy, particularly at near-threshold noise.
• Exact Recovery and Latency Hiding: The runtime executor confirmed that the predict-verify-recover loop recovers exactly. On a chain of 16 windows, the system achieves a speedup of ~16.00 (the theoretical maximum), removing the serial commit-chain stall up to a negligible restart penalty ($\sim 10^{-5}$).
• Decoder-Agnostic Structural Phenomenology: While absolute accuracy magnitudes and the specific "min-weight" mechanism are decoder-specific, the structural findings are robust. The Union-Find decoder confirmed that the cut decision is local (saturating at $R=3$) and that propagation without a faulty path persists, validating the structural phenomenology of the speculation wrapper.

Significance and Claims
The paper claims to have built the missing "verifier side" of speculative window decoding, transforming it from an empirical heuristic into a rigorously bounded system. The significance lies in:

1. Proving Safety: Demonstrating that speculation does not introduce an error floor, as mispredictions are contained to a radius of one with machine-checked probability bounds.
2. Clarifying Mechanism: Replacing the intuitive "faulty path" model with the correct "global re-pairing" mechanism, explaining why propagation happens even without direct error chains.
3. Enabling Automation: Providing a compiler pass that derives restart policies from measured numbers rather than hardcoding them, making the approach portable across different code layouts and control stacks.
4. Reusability: Establishing the predict-verify-recover wrapper as a reusable layer that sits above any decoder, decoupling the speculation logic from the specific decoding algorithm.

The authors remain modest regarding the scope, noting that the speedup numbers are based on an analytic linear-chain map (as the full SWIPER-SIM pipeline is not public) and that the formalization of the matching-weight bound (the source of the exponential decay) remains a target for future work. The work is presented as a foundational layer for real-time QEC, validated on a reconstructed harness with reproducible code and machine-checked proofs.