arXiv:2609.10600 · v3
Certified Panic Mode: Repair-Invariant Error Recovery for Maximal-Munch Lexing
摘要
Classical panic-mode recovery skips a failed scan forward by convention, promising progress but no repair-universal boundary guarantee for where it lands. We choose the resume position by theorem, via a committed-prefix lemma over certificates posted for parallel lexing (arXiv:2608.03473, arXiv:2608.09761): a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there. This quantifier is strictly stronger than its complete-repair special case, and at a sound recovery point the inclusion is strict precisely when no repair completes while some scan commits through the evidence. The evidence-returning interface pairs each answer with the interval it rests on, so a caller who knows what the scanner cannot check decides whether the boundary transfers to the intended input. The search provably terminates; the guarantee is relative to the active mode's automaton. For an automaton of n states the quantifier is decided exactly from the preserved tail by at most n + 1 representative repairs, and a shortest reaching repair has at most n - 1 symbols and a shortest counterrepair at most n, both tight. Every anchor of an m-byte input is profiled in $O(nm + n|Σ|)$ time. The shipped repair routines are the complete-repair case, which proves their contracts. In a deterministic corruption study of munch's procedure beside skip-one and delimiter recovery, every certified answer whose evidence survives the damage passes its landing check on every move, 40,885 of 40,885, while the 5,595 first answers resting on evidence the damage reached land 1,589 times, reported, not asserted. Of the 16,808 trials labeled beyond repair, 13,522 resume on a suffix that tokenizes whole, where both quantifiers are provably empty, and 3,286 stay undetermined, their damaged inputs not archived.
作者备注：32 pages, 4 figures, 7 tables. v3: decides the evidence-reaching quantifier exactly with sharp counterrepair bounds, and reworks the prose. Artifact: https://doi.org/10.5281/zenodo.22178507 . The campaign data, mutation suite and reproduction scripts are in the artifact; every reported aggregate is regenerated from it. Companion to arXiv:2608.03473 and arXiv:2608.09761