Restart by proof

A lexer hits a byte it cannot turn into a token. The normal recovery advice is useful and a little suspicious: skip one character, or jump to a newline or semicolon, then try again. The scanner moved forward. Whether it moved to a real token boundary is a separate question.

Nicklas Nidhögg's Certified Panic Mode, submitted on September 7, gives that question an unusually concrete answer for maximal-munch lexers. A restart point can be accompanied by evidence from the compiled DFA showing that the point remains a token boundary across every relevant repair of the damaged prefix. The implementation shipped a day earlier in munch 1.6.0.

The suffix can lie#

The annoying part of lexer recovery is that token boundaries depend on what came before them. A suffix can tokenize perfectly when scanned by itself and still begin in the middle of a token after the broken prefix is repaired. The paper's tiny two-token witness makes the problem hard to unsee:

tokens = { "ab", "b" }suffix alone:       "b"       -> ["b"]repair the prefix:  "a" + "b" -> ["ab"]

With tokens ab and b, the suffix b looks safe in isolation. Put an a before it and maximal munch consumes ab as one token. There is no token boundary before that b anymore. So “the remaining text tokenizes” is too weak a recovery test.

Delimiter panic mode sidesteps this by using language knowledge. A parser or scanner skips until a chosen landmark appears and hopes the landmark is outside the damaged construct. This is often good engineering; it is also a convention about the language and the input. A quote, comment, or longer token can make a byte that looks special from the outside very ordinary from inside the token that owns it.

A boundary can carry evidence#

Certified Panic Mode reuses two results that were originally built for parallel lexing. The August paper on certified split bytes identifies bytes whose useful occurrences begin tokens. Its companion on certified split windows extends that idea to short byte sequences and can identify where the token covering the window's final byte must have started. The analysis runs over the lexer's compiled tables rather than over a hand-picked list of delimiters.

The recovery paper adds the bridge from a failed scan to those older certificates. Its committed-prefix lemma says that whatever a maximal-munch scan has already committed before failing is itself completely tokenizable with exactly that segmentation. That sounds almost tautological. It matters because a repaired scan may fail again later; the proof only needs the committed prefix that actually reaches the returned evidence.

The quantifier is the interesting bit. The guarantee ranges over prefix repairs whose scans commit through the returned evidence. A repaired file does not have to tokenize successfully all the way to EOF before the boundary claim becomes meaningful. Complete repairs are included, but the theorem covers failed repaired scans that got far enough as well.

This is a very specific promise. It does not say the original program can be repaired, and it does not say the next tokenization attempt will succeed. It says that if the bytes supporting the certificate are still the bytes you meant to preserve, the returned restart point is a token boundary in every scan covered by that repair condition.

The scanner cannot know where the damage ends#

The evidence-returning API is what makes the theorem useful outside the paper. The scanner knows where it failed; it usually does not know whether the user replaced one byte, pasted across four tokens, or handed it a truncated transport frame. munch therefore exposes the evidence interval instead of pretending the lexer can infer the edit span.

auto result = tokenizer.next<TokenKind>();if (result.has_error()) {  auto recovery = tokenizer.recover_from_failure();  if (!recovery) {    return stop_with_error();  }  // recovery->start is where scanning can resume.  // evidence_begin..evidence_end is what justifies that answer.}

Tokenizer::next() leaves the reading position unchanged on error. The driver can stop, move by its own rule with seek(), call the simple recover() skip-count API, or use recover_from_failure() to get the certified start plus its evidence. The shipped search checks certified bytes and windows two through four bytes wide and returns std::nullopt if it finds no searched certificate ahead.

There is also recover_from_clean(clean_from). That version is for a caller with information the automaton cannot have. An editor may know the end of the edited range; a framed protocol may know the first byte of the next intact frame. Flooring the search at that clean offset makes the returned evidence live in the undamaged suffix by construction. The lexer proves the boundary property, while the surrounding system supplies the fact that the proof's evidence survived.

90.8 percent is not the theorem#

The paper also runs a deterministic corruption campaign because a sound certificate can still be useless if it almost never appears. Across the measured first answers, certified recovery landed on the pristine token boundary 90.8% of the time; pooled skip-one landed 10.0%. For every recovery move whose returned evidence survived the synthetic damage, the campaign's executable landing check passed: 40,885 out of 40,885.

Those numbers are implementation and quality evidence, not the proof. The paper is careful about the difference. Its strongest empirical result only applies when the evidence survives the modeled corruption. When the damage reaches into the evidence, the boundary certificate no longer transfers to the pristine input, and the study reports those moves separately instead of silently counting them as guaranteed.

Delimiters are not embarrassed by the comparison either. In some rows, a newline placed at the right side of a token is a very strong recovery heuristic. Move the placement convention or change the grammar and the result can fall apart. The useful distinction is where the claim comes from: delimiter quality belongs to a corpus, grammar, and placement rule; the certified boundary belongs to the automaton plus preserved evidence.

The limits are worth keeping next to the headline number. Most corpora in the study are generated, edits are synthetic substitutions, deletions, and insertions, and the campaign measures recovery quality rather than throughput. The implementation searches windows only up to length four. The certificate is per automaton, so a mode-driven lexer recovers relative to the active mode; there is no free proof across a mode change.

Refusal is part of the contract#

My favorite API outcome here is std::nullopt. Classic panic mode tends to keep eating input until it reaches its chosen landmark or the file ends. Certified recovery can look ahead and say it has no certificate to offer. That is less convenient, but it keeps the boundary guarantee honest.

Error recovery still needs policy. A compiler may prefer a fast heuristic after a refusal; an editor may know a clean region that makes a later certificate usable; a batch parser may simply stop. The new part is that one of those policy choices can begin from a restart point the lexer can actually justify. For a stage of the compiler pipeline that usually treats “probably synchronized again” as good enough, that is a neat upgrade in what an error path is allowed to know.