{"id":"25279717-9121-493b-b9bb-3ea2ec50fe1a","arxiv_id":"2608.03473","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A byte that no live mid-token state can consume, with no re-entry into the start state, is provably always a token boundary; splitting there reproduces the serial token stream exactly, and a conservative discarded-token variant recovers newline for C-like and JSON lexers.","lead":"This paper defines a per-byte property of a compiled lexer automaton: a byte is a certified split symbol when no mid-token state can consume it into a live state, and the start state cannot be re-entered. Parallel scanners can split input at such bytes and stitch per-chunk token streams together exactly, with no speculation or reconciliation, replacing delimiter folklore with a property a lexer library can check.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorems 1–3 appear sound under the stated scanner model; the load-bearing gap is empirical reproducibility of the headline speedups, not a flaw in the certificate.","rationale":"The reader's weakest_assumption names the scanner model, which is a genuine boundary but one the paper states explicitly in §9; it does not threaten the theorems as scoped. My closer reading of the proof chain found no counterexample to Lemma 1, Theorem 1, Theorem 2, or Theorem 3, including the re-entrancy cases and the modulo-discarded-token construction. The more decisive risk for the paper's central claim as a whole is that the measured performance, which appears in the abstract and is the main practical payoff, rests on a single machine, two benchmark revisions, favorable corpora, and incomplete archiving of the pinned run. This matches the reader's CONDITIONAL verdict, so I do not propose changing it; I would only sharpen the reason: the theory appears reliable, while the empirical half is not yet independently reproducible.","tokens_in":27361,"tokens_out":15384,"duration_ms":194392,"concrete_test":"On a second bare-metal machine (or the same machine after recording the exact commit, `taskset -c 0-7` command, and per-pass logs), rerun the pinned Environment B scaling scenario on the 512 MiB dense corpus. Compare eight-chunk efficiency against the one-chunk baseline and the four-chunk end-to-end ratio against the plain scan. If either falls outside the reported ranges by more than 5 percentage points or 0.5×, the abstract's ranges must be re-scoped as single-machine observations rather than general speedups.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I re-derived the key steps and found no soundness hole in the theoretical core. Lemma 1 forces q = q0 before a mid-token certified byte and then contradicts Definition 2 via re-entrancy; Theorem 2's witnesses w = u b v are genuinely completely tokenizable because the longest-match scan runs to the accepting end of v; Theorem 3 confines an interior cut to a single discarded token via the row equality δ+(q0,b) = δ+(q,b) and T(q) ⊆ I. The §9 scanner-model limitation is explicit and does not undermine the conditional claim. The real load-bearing concern is empirical: the abstract's 92.6–95.3% parallel efficiency and 3.46–3.94× end-to-end ranges are reported for one machine, two benchmark revisions taken at different commits, corpora that deliberately exclude strings and comments, and a pinned run whose launch command and core mask were not archived. The relaxed condition is never measured at run time. Since these numbers are the headline evidence that the technique pays for itself, the conditional verdict should remain until the artifact gap is closed by an independent repeat.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies a table-driven longest-match DFA lexer that resets to a single initial state q0 at every token boundary. It defines a byte b to be a certified split symbol when, in the live reachable/co-accessible subautomaton A+, no state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it consumes b. Lemma 1 and Theorem 1 show every occurrence of such a byte in completely tokenizable input is a token boundary, so ordered concatenation of per-chunk token streams reproduces the serial stream. Theorem 2 proves the converse. Definition 3 and Theorem 3 weaken equality to equality after deleting a declared discarded-token set, via a conservative local condition. The paper contributes a linear-time derivation, a planner, an applicability study over eleven token sets, and an evaluation in the munch library. The theoretical core is sound; the main weakness is reproducibility of the headline empirical numbers.","tokens_in":27500,"tokens_out":11630,"duration_ms":145983,"significance":"The result, if correct, is a genuinely useful static characterization: safe split points for a class of parallel lexers become a decidable per-symbol property of the compiled transition table rather than a language-specific assumption. The proofs are explicit and checkable; the paper goes beyond folklore by giving necessity, by identifying the re-entrancy condition, and by handling discarded tokens. The artifact includes property tests, an exhaustive oracle on small alphabets, regression tests for the counterexamples, and archived benchmark summaries. These are real strengths. The scope is carefully limited to the Section 3 scanner model, and the paper's own limitations section names what falls outside (modes, predicates, non-regular constructs). The empirical speedup claims, however, are not yet on the same footing as the theory.","major_comments":[{"comment":"The headline quantitative claims—92.6–95.3% parallel efficiency and 3.46–3.94× end-to-end speedup—are not reproducible from the archived artifact. As the text itself discloses, the two Environment B collections are two benchmark revisions at different commits, each placement has a single run, the launch command and core mask were not archived, the machine was not quiesced, and the clock on Environment B is observable but not fixed. Since these numbers are the paper's main empirical evidence that the technique pays for itself, this is load-bearing rather than cosmetic. I request either an archived pinned run with exact command, mask, and commit plus interleaved repeats, or a clear demotion of the quantitative claims to illustrative/pilot status in the abstract and conclusion.","section":"§8 / Table 2 / §11"},{"comment":"The end-to-end ratio is dominated by an unstable denominator. The paper reports that the plain-scan row rose 14.3% (pinned) and 17.4% (unpinned) between revisions at 512 MiB, while the multi-chunk rows moved by at most about 1.4%, and that the plain-scan versus one-chunk comparison changed sign across collections. The 3.46–3.94× range therefore mostly reflects revision-to-revision baseline movement, not a stable treatment effect. Because the paper uses ratio-of-medians as a single estimator and does not report paired per-round ratios except for win counts, the reader cannot separate the parallel gain from the baseline drift. Please report per-round paired ratios and/or a controlled repeat with the same commit and interleaved conditions.","section":"§8.1"}],"minor_comments":[{"comment":"The paper's own limitation statement is accurate and should perhaps be moved earlier: the certificate is sound only for the Section 3 scanner model (restart from q0, positive-length tokens, no carried state). Lexer modes, indentation stacks, and semantic predicates are outside scope. This is a disclosed scope limit rather than an internal inconsistency, but it should be reflected on the first page.","section":"§9"},{"comment":"Typos/formatting: 'DF A' should be 'DFA', and 'n n' / '2 n2' should be mathematical notation for n^n and 2^{n^2}.","section":"§2"},{"comment":"The phrase 'Condition 3' is ambiguous; it should refer to Definition 3 or to clause C(3). Also, the statement 'the relaxation is free at scan time' should be qualified by the fact that the planner does not use the relaxed map; no runtime measurement of the relaxed path is reported.","section":"§6.1"},{"comment":"Formatting in the first row ('0.1µs<1 KiB') is unclear; state that the median bytes scanned is below 1 KiB.","section":"Table 3"}],"recommendation":"major_revision","confidential_remarks":"The theoretical part is solid and the paper is unusually honest about its limitations and artifact gaps. The main risk is that the abstract and conclusion present non-reproducible benchmark numbers as established. I would not reject, because the theorems and the published validators are the actual contribution and are checkable; I would require the empirical section to be either reproduced or explicitly downgraded. No concerns about novelty or attribution beyond what the paper itself documents."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing you should know: this paper has the goods on the theory side. The re-entrancy requirement in Definition 1 is genuinely new, and the counterexamples in Section 4.2 are not noise—they show the naive incoming-transition criterion is unsound. I re-derived Lemma 1 and Theorem 2 and found no holes. The condition is necessary and sufficient on the live subautomaton, not a heuristic. That is worth taking seriously.\n\nWhat is new: the per-symbol certificate, the necessity theorem, and the modulo-discarded-tokens relaxation. The prior work survey is careful and the Section 10 connection to reset words is honest framing rather than hype. The paper also does something rare: it tells you exactly where the method fails (Table 1), and the negative rows are statements about tokenizations, not about the analysis.\n\nThe soft spots are empirical and archival, not theoretical. The headline 92.6–95.3% efficiency and 3.46–3.94x speedups come from one machine, two benchmark revisions taken at different commits, and corpora that deliberately exclude strings and comments. The pinned run's launch command and core mask were not archived. The relaxed condition is never measured at run time. The paper discloses all of this, which helps its credibility, but it means the performance claims are conditionally reproducible at best.\n\nOne more thing: the scanners model is explicitly limited to table-driven DFAs that reset to a single start state at every token boundary. Lexer modes, indentation stacks, and nullable tokens are out of scope. That boundary is stated plainly in Section 9, so it is not a hidden flaw—but anyone applying this to a real lexer has to check those conditions first.\n\nWho this is for: people working on parallel scanning, lexer generators, or tokenization theory. It deserves a serious referee. The theory should be reviewed and probably published; the empirical claims need artifact closure before the abstract ranges are relied on.\n\nRecommendation: send it out. The referee should focus on the benchmark reproducibility and the gap between the exact and relaxed conditions, not on the core theorems—those are solid.","headline":"The certificate is real and the theorems hold up; the only serious weakness is that the headline speedups rest on an incompletely archived benchmark.","tokens_in":28088,"tokens_out":915,"would_cite":true,"duration_ms":12228,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68W10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Certified split bytes are points where a longest-match scanner is provably between tokens; chunks starting there concatenate to the exact serial token stream.","keywords":["parallel lexing","DFA tokenizer","longest match","certified split symbol","reset words","modulo discarded tokens","static analysis","parallel efficiency"],"falsifier":"Compile any token set to a minimized DFA, compute Q+ and Definition 2, then exhaustively scan all strings over a three-byte alphabet up to length eight, recording whether each occurrence of each byte begins a token. Any byte certified by the definition but found inside a token—or rejected despite no such witness existing—refutes Theorem 2. The paper itself shows this kind of brute-force oracle is feasible for the modulo condition.","tokens_in":27150,"feed_emoji":"⚡","tokens_out":11895,"duration_ms":124063,"temperature":0.7,"pith_summary":"Serial lexing is a dependency chain: each table lookup needs the previous state, so scanning one input in parallel requires knowing each chunk's entry state. This paper establishes a static, input-independent property that removes that requirement for a useful class of scanners: a byte is a certified split symbol when the trimmed live automaton's only transitions on that byte leave the initial state, and the initial state cannot be re-entered mid-scan. Every occurrence of such a byte in fully tokenizable input begins a token, so chunks cut immediately before it reproduce the serial (token, length) stream by ordered concatenation—no speculation, prescanning, or overlap. The condition is both necessary and sufficient, so a token set that certifies no byte genuinely has no single-byte split symbol preserving the exact stream. Because the exact condition is fragile—one string literal, comment, or whitespace run can erase every useful certificate—the paper weakens the guarantee to equality after deleting declared discarded tokens, which recovers newline for conventional C-like and JSON tokenizations; on an out-of-cache corpus the exact certificate measures 92.6–95.3% parallel efficiency at eight threads.","feed_headline":"Parallel lexing can split at proven-safe bytes, no guessing","feed_subtitle":"A static check on the token automaton certifies bytes that always begin a token, so parallel chunks concatenate exactly.","key_machinery":"The load-bearing object is the trimmed live subautomaton A+ = (Q+, Σ, δ+, q0, τ), where Q+ contains only states that are reachable from the initial state and can still reach acceptance, and δ+ discards transitions whose targets leave Q+. Certification is defined over A+ rather than the full table: byte b is certified if every q ∈ Q+ with δ+(q,b) defined satisfies q = q0, and if δ+(q0,b) is defined, q0 is not re-entrant. The re-entrancy clause is the subtlety: without it, the nullable token set a* would certify a and split one emitted token into two, and cyclic re-entry through (ab)*c would certify c. The relaxed modulo-I condition adds a second constant-time one-bit query: a state q consumin","core_discovery":"Central claim: the question 'where may a parallel scanner cut without changing the answer?' can be settled per token set from the compiled transition table. Fix a longest-match scanner restarting at q0 after each token; let Q+ be the states both reachable from q0 and able to reach acceptance. Byte b is certified if every live b-transition in Q+ starts at q0, and if q0 consumes b, q0 is not re-entrant. Then every occurrence of b in completely tokenizable input begins a token, and conversely; chunks cut before certified bytes reproduce the serial stream. A second, conservative condition preserves equality only after deleting a declared discarded set, and it admits newline for conventional C-li","pith_inferences":["If the necessity theorem holds, a token set that certifies nothing is not a failure of the test but a fact about the grammar; a natural untested engineering response is to automate the tokenization refactoring the paper describes by hand, such as making newline its own token.","The relaxed certificate is shipped only as a query—planner and benchmarks use the exact map—so the practical throughput gain from modulo-I splitting for conventional grammars remains unmeasured; building a planner on the relaxed map is a concrete next experiment.","Because certified bytes are one-letter reset words of the partial live automaton, searching for multi-letter reset words or short windows such as ')' followed by newline could yield conditional certificates for grammars with no single certified byte; the paper lists this as future work rather than a result.","The measured scaling comes from a corpus free of strings and comments and a grammar that certifies 13 of 14 candidate bytes, so extrapolating those efficiency numbers to typical source code would require the relaxed planner the paper does not ship."],"forward_implications":["Delimiter safety stops being a language-specific folklore assumption: for any compiled token set, the certificate is decided from the transition table, and a row that certifies nothing is a statement about the tokenization, not about the test.","Because the condition is necessary as well as sufficient, no token set that certifies no byte admits any single-byte split symbol that preserves the exact stream; regaining a split point requires changing the tokenization, weakening the guarantee, or framing the input.","Declaring discarded tokens extends the method to conventional grammars as written: the relaxed certificate recovers newline for a C-like tokenization and tab, newline, and carriage return for JSON, with no change to their token definitions.","In the measured implementation, exact-certificate splitting reaches 92.6–95.3% parallel efficiency at eight threads and a 3.46–3.94× end-to-end speedup at four threads on a 512 MiB corpus beyond last-level cache, with chunks guaranteed to reproduce the serial stream.","A producer that reserves a byte excluded from all token interiors and escapes it in content can make any grammar chunkable, including grammars with block comments."],"supporting_citations":[{"why":"Supplies the delimiter-relocation and parallel-parsing precedent whose language-specific separator assumptions the certificate makes decidable, and the JSON/Lua applicability claims re-derived in Section 7.","marker":"[1]"},{"why":"Defines reset words for partial DFAs; the paper shows a useful certified byte is exactly a one-letter reset word of the live automaton.","marker":"[3]"},{"why":"Gives the modulo-token equivalence for separator insertion that Theorem 3 adapts to raw cuts inside discarded tokens.","marker":"[8]"},{"why":"Provides the prescan-based parallel lexer whose newline-for-JSON folklore the paper derives from the token set, and the main alternative it contrasts with.","marker":"[18]"},{"why":"The accompanying lexer library implements the predicate, planner, executor, benchmarks, and artifact assertions behind the measured claims.","marker":"[22]"},{"why":"Records the closest prior static check, a safe-after sentinel test for one declared byte; the paper shows it is incomparable with the safe-before certificate.","marker":"[24]"},{"why":"Fixes the scanner model as a Mealy-machine-like longest-match analyser, used to justify attaching token output and lookahead behaviour.","marker":"[35]"}],"fun_headline_variants":["Lexing in parallel: certified cut points replace guessing","Certified bytes: split lexer input without rescanning","Proof-based splits for exact parallel lexing","Safe split bytes: parallel lexer without overlap","No-simulation parallel lexing via certified bytes"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The approach assumes the scanner is a table-driven automaton that restarts from one fixed start state at each token boundary, carries no other state, and emits no empty tokens; lexers with modes, indentation stacks, semantic predicates, or nullable tokens fall outside the model, and the exact guarantee additionally presumes completely tokenizable input.","fun_headline_variants_meta":{"raw":{"variants":["Lexing in parallel: certified cut points replace guessing","Certified bytes: split lexer input without rescanning","Proof-based splits for exact parallel lexing","Safe split bytes: parallel lexer without overlap","No-simulation parallel lexing via certified bytes"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000627,"raw_usage":{"total_tokens":2811,"prompt_tokens":895,"completion_tokens":1916,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":639,"completion_tokens_details":{"reasoning_tokens":1856}},"tokens_in":639,"tokens_out":1916,"duration_ms":13850,"temperature":1.0,"reasoning_tokens":1856,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T18:29:32.894844+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile any token set to a minimized DFA, compute Q+ and Definition 2, then exhaustively scan all strings over a three-byte alphabet up to length eight, recording whether each occurrence of each byte begins a token. Any byte certified by the definition but found inside a token—or rejected despite no such witness existing—refutes Theorem 2. The paper itself shows this kind of brute-force oracle is feasible for the modulo condition.","supporting_citations":[{"cited_title":"Berlinkov, Robert Ferens, Andrew Ryzhikov, and Marek Szyku la","cited_arxiv_id":null,"evidence_quote":"Defines reset words for partial DFAs; the paper shows a useful certified byte is exactly a one-letter reset word of the live automaton."},{"cited_title":"Formally Verified Linear-Time Invertible Lexing","cited_arxiv_id":"2510.18479","evidence_quote":"Gives the modulo-token equivalence for separator insertion that Theorem 3 adapts to raw cuts inside discarded tokens."},{"cited_title":"munch: a lexical analysis library based on automata theory, version 1.2.0, 2026","cited_arxiv_id":null,"evidence_quote":"The accompanying lexer library implements the predicate, planner, executor, benchmarks, and artifact assertions behind the measured claims."},{"cited_title":"Added warning: -Wsentinel-in-midrule","cited_arxiv_id":null,"evidence_quote":"Records the closest prior static check, a safe-after sentinel test for one declared byte; the paper shows it is incomparable with the safe-before certificate."},{"cited_title":"Mealy machines are a better model of lexical analyzers.Computer Languages, 22(1): 27–38, 1996.doi:10.1016/0096-0551(96)00003-3","cited_arxiv_id":null,"evidence_quote":"Fixes the scanner model as a Mealy-machine-like longest-match analyser, used to justify attaching token output and lookahead behaviour."}],"review_version":1}