{"id":"0144a28d-9e1c-4ebd-b6c9-4eb8a8d21b35","arxiv_id":"2608.09761","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Certified split windows generalize split-point certificates to bounded byte strings, recovering the origin of the covering token for token sets where no single byte certifies.","lead":"This paper extends parallel lexing certificates from single bytes to bounded windows, so a lexer can recover where a token began even when no individual byte guarantees a safe cut. The method provably recovers the covering token's origin for many token sets where byte-level certification fails, including every exact-empty row of the prior study.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the central soundness and decision theorems hold up under scrutiny within their explicitly scoped non-nullable, completely-tokenizable setting.","rationale":"The reader's weakest assumption, non-nullability, is real and the paper itself calls it load-bearing; it is also an explicit scope condition, not an unstated gap. I agree it is the most notable limitation, especially because two-thirds of the random grammars are excluded, but it does not undermine the theorems as stated. I scrutinized the proof of Lemma 1, including the base case, the re-entrancy rename, and the handling of maximal-munch rewind via seeded boundaries, and found no case where the actual final-segmentation pair leaves the cloud. I also checked the quotient argument: the single-occupancy invariant, the saturation-at-two reasoning, the freshness of inserted origins, and the key-readable update of the before-support all appear coherent. The conservatism of the seed rule is a deliberate source of false negatives and is exhibited by concrete strictness witnesses, so it does not threaten soundness. The evaluation figures are asserted by the artifact but were not independently rerun here; that keeps confidence at moderate rather than high, but it is not an identified mathematical defect. Therefore the verdict should remain ACCEPT.","tokens_in":14537,"tokens_out":47536,"duration_ms":454477,"concrete_test":"Run an independent implementation of the raw unquotiented cloud model plus an exhaustive semantic oracle over completely tokenizable inputs up to length 8 on the three-symbol alphabet, then re-run the 134 non-nullable random grammars: every quotient-BFS certificate must coincide with a raw-cloud certificate, and every model-certified window up to length 5 must satisfy Definition 1 at all oracle-checked occurrences; any mismatch would falsify Lemma 2 or Theorem 1.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I found no load-bearing flaw in the central argument. Lemma 1 is a valid containment invariant: the actual final-segmentation prefix pair is always in the cloud, and surplus hypotheses can only break unanimity, not manufacture false unanimity. The quotient congruence in Lemma 2 is sound under the single-occupancy invariant; saturated counts suffice because co-located in-window origins move together or die together. The non-nullability assumption is genuinely load-bearing—Lemma 1's seed/gate argument and the maximal-munch semantics need tokens to consume bytes—but it is stated up front, and the paper scopes all claims to it, excluding 266/400 random grammars. The model's conservatism is an acknowledged source of false negatives, not false positives. The main residual risk is that the hand proofs are not machine-checked and the artifact was not independently executed; this is a verification gap rather than an identified error.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper generalizes certified split points for parallel lexing from a single byte to a bounded window (W, o). It defines a conservative cloud model of maximal-munch scanner histories across W, proves that the actual final-segmentation history is always represented (Lemma 1) and hence that cloud unanimity implies a semantic certificate (Theorem 1), and then gives a finite quotient of reachable clouds, exact under a stated single-occupancy invariant, which makes breadth-first search a terminating decision procedure for the model (Lemma 2, Theorem 2). A specialization theorem shows exact agreement with the predecessor's length-one predicate (Theorem 3), two strictness witnesses show non-vacuous conservatism beginning at length two, and an artifact-backed evaluation covers the predecessor's exact-empty rows and 400 random token sets. All positive claims are explicitly scoped to flat, non-nullable, completely-tokenizable token sets; negative results are explicitly model-relative.","tokens_in":14621,"tokens_out":8101,"duration_ms":69927,"significance":"If correct, the paper is a substantive and cleanly bounded extension of certified split points: it recovers a usable boundary where no single byte can be certified, it proves the decision procedure exhaustive for the model, and it keeps the honesty conditions unusually visible by separating model certificates from witnessed occurrences and from model-relative negatives. The main strengths are the representation-invariant soundness proof, the exact finite quotient with a stated invariant, the specialization theorem that anchors the new construction to the predecessor, and an artifact whose asserted figures and rewind-stress counts make the evaluation falsifiable. The principal residual risk is that the proofs are hand proofs and the artifact was not independently executed in this review; I found no load-bearing flaw in the central argument.","major_comments":[],"minor_comments":[{"comment":"The notation x[σ_j .. t+j) is terse: please state explicitly that intervals are half-open and that ρ_j is the state after consuming through byte t+j−1. The current prose is easy to misread as containing an off-by-one error.","section":"Section 4, Lemma 1"},{"comment":"The term 'exact-empty row' is used before it is defined; please define it on first use, for example as a row of the predecessor's applicability table whose certified-byte set is empty.","section":"Sections 1 and 9, Table 1"},{"comment":"The freshness argument is dense; a sentence making explicit that 'every origin in a length-ℓ cloud lies below ℓ' is what guarantees the inserted offset is fresh for both successor computations would improve readability and prevent a natural misreading of the depth-aligned clause.","section":"Section 5, Lemma 2"},{"comment":"The sentence reporting '4 exhaust the quotient with no window under the model, and none are inconclusive or unresolved' would be clearer if it distinguished exhaustion of the quotient search from an unresolved outcome of the bounded witness search, since those are different notions introduced in Section 5.","section":"Section 9, random sweep paragraph"}],"recommendation":"accept","confidential_remarks":"I concur with the stress-test assessment: no load-bearing technical flaw was identified. The non-nullability restriction is explicitly load-bearing and the evaluation excludes 266 of 400 random grammars, so the headline rescue rates describe only the non-nullable subpopulation; this is stated clearly in the manuscript. The related-work section is unusually long and might be tightened during production, but that is a presentation matter. The main residual risk is verification risk rather than correctness risk: the central theorems are hand proofs and the artifact was not independently executed for this review."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read it twice, including the proofs. The central result is real: the cloud model with acceptance-gated seeding is a conservative over-approximation of maximal-munch histories, Lemma 1 is a genuine representation invariant, and the finite quotient in Lemma 2 is exact for reachable clouds. Theorem 1 is sound, and Theorem 3's specialization to length one correctly recovers the published byte predicate. The strictness witnesses and the corollary that non-vacuous refusal starts at length two are convincing.\n\nWhat is actually new: the window object, the origin-recovery certificate, and the quotient decision procedure. The paper also does something rare: it states its own limitations up front and then respects them. The exclusion of nullable token sets is load-bearing and honestly quantified — 266 of 400 random grammars are nullable. Negatives are explicitly model-relative. Vacuous certificates are separated from witnessed ones. That is the right way to build a negative result.\n\nSoft spots, in proportion: (1) The evaluation is on random three-symbol grammars, not real corpora; the paper says no frequency claim is made, but that leaves the practical value unmeasured. (2) The artifact is archived and asserted, but I did not run it; the proofs are hand-written, not machine-checked, so confidence is moderate rather than high. (3) The worst-case complexity is exponential in the state count; the retained-key counts are small in practice, which is evidence but not a guarantee. Minor: the paper leans on its predecessor for the prefix-stability composition that turns a boundary into a parallel cut; the composition is stated, not re-proved, which is fine but should be kept in mind.\n\nI disagree with the stress-test note on one small thing: the non-nullability exclusion is not a flaw, it is a properly scoped assumption. The paper says it repeatedly. So I would not hold it against the authors.\n\nWho this is for: anyone working on parallel lexing, verified tokenization, or automata-based chunking. It deserves a serious referee. I would send it to review with encouragement; the main asks would be an independent artifact run and some real-corpus frequency numbers, but neither is a correctness issue.","headline":"A solid, honestly scoped extension of certified split bytes to windows; the central soundness and decision theorems hold up, and the limitations are explicitly owned.","tokens_in":15171,"tokens_out":1823,"would_cite":true,"duration_ms":14954,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A parallel lexer can recover a token boundary from a short window of bytes even when no single byte certifies a safe cut, and 91 of 95 previously stuck token sets gain such a window.","keywords":["parallel lexing","certified split windows","maximal munch","token boundaries","deterministic finite automata","cloud model","finite quotient","soundness proof"],"falsifier":"One completely tokenizable input containing a model-certified window $(W,o)$ whose maximal-munch tokenization makes the token covering the window's final byte begin at an offset different from $o$ would falsify Theorem 1; the paper's own rewind-stress rows, which found zero such disagreements across 1,079,392 generated executions, are exactly the kind of check that could uncover such a counterexample.","tokens_in":14288,"feed_emoji":"✂️","tokens_out":8909,"duration_ms":72493,"temperature":0.7,"pith_summary":"The paper extends certified split points—single bytes where a parallel lexer can cut input without changing the serial token stream—to certified split windows: a short byte string after which the start of the token containing the window's final byte is provably fixed in every completely tokenizable input. The central claim is that these windows can be discovered automatically from a compiled token automaton, and that they exist for many token sets for which no single byte certifies a safe cut. The method carries a cloud of possible token-prefix histories across the window, proves by a representation invariant that unanimity on an origin can only land on the truth, and decides reachability by exhausting a finite quotient of clouds. In the evaluation, 91 of 95 non-nullable random token sets that certified no byte gain a witnessed window, and every exact-empty row of the predecessor's study gains a window of two to four bytes. This makes provably safe parallel lexing reach conventional lexical forms such as strings, comments, and whitespace runs that previously resisted it.","feed_headline":"Bounded windows restore safe splitting to 91 of 95 token sets","feed_subtitle":"A scanner can prove where the current token began after a few bytes, so parallel chunks need no speculation.","key_machinery":"The load-bearing object is the cloud: a set of pairs $(q,\\omega)$ where $q$ is a live automaton state and $\\omega$ is either 'before' (a token that began before the window) or an offset inside the window. Reading each window byte advances the cloud by a direct step for surviving hypotheses and an acceptance-gated seed that starts a fresh trajectory at the current offset whenever some hypothesis is accepting, allowing a new token to begin only where the previous one could have ended. A window is certified when the final cloud is non-empty and all surviving pairs agree on a single in-window origin. The search terminates because clouds are deduplicated on a finite quotient—the set of states carrying 'before' plus per-state in-window origin counts saturated at two—so breadth-first search exhausts at most $6^{|Q^+|}$ keys. The soundness argument is a representation invariant: the final segmentation's true token-prefix history is always among the hypotheses, which is why unanimity can only land on the truth.","core_discovery":"The central discovery is the certified split window $(W,o)$: a byte string $W$ such that in every completely tokenizable input containing $W$, the token covering the window's final byte begins exactly $o$ bytes into the window. Theorem 1 states that if the model's cloud after reading $W$ is non-empty and every pair in the cloud carries the same in-window origin $o$, then $(W,o)$ is certified. Theorem 2 states that breadth-first search over a finite quotient of reachable clouds, keyed by the before-support set and per-state in-window origin counts saturated at two, decides whether the model certifies any window and returns the minimum certified length. The construction specializes exactly to the predecessor's single-byte predicate at length one, so multi-byte windows are a conservative continuation of certified split points. The paper also proves that the model's deliberate conservatism—it refuses some windows a greedy scanner would allow—cannot begin before length two, exhibiting two semantically certified length-two windows it refuses.","pith_inferences":["The four random grammars that still exhaust with no window are only model-negatives, so a tightened model that tracks maximal-munch behavior more faithfully could certify windows there; the paper gives no bound on how much room remains.","A certified window behaves like a reset device for token origins rather than for raw automaton states, so the natural analogue of synchronization in this setting lives in the cloud quotient, not in the token DFA.","A corpus-frequency study is the direct next test: whether two-to-four-byte windows like newline-bang or tab-quote appear often enough in real code and JSON to plan balanced parallel chunks is open, and the paper explicitly leaves it to a measurement campaign.","Extending the proof to nullable token sets would broaden coverage from roughly one-third of random grammars to nearly all of them, but the acceptance-gated seed and the representation invariant would both need reworking."],"forward_implications":["Every exact-empty row of the predecessor's table—C-like strings, line comments, block comments, conventional whitespace handling, and JSON—now carries a certified window of length two to four bytes with a verified occurrence witness.","A worker that finds a certified window in completely tokenizable input can resume scanning at the recovered boundary with no speculation, no state-recovery pass, and no re-execution, exactly as at a certified byte.","For flat, non-nullable token sets on completely tokenizable inputs, a model-positive search result is a semantic certificate, while an exhausted search is a model-relative negative rather than a proof that no window exists.","Because the certificate is derived from the compiled tables before any input exists, the analysis runs once after automaton construction and imposes no runtime cost on the scanner.","At length one the model reduces exactly to the published single-byte predicate, so the new windows extend the old guarantee without changing what the old guarantee meant."],"supporting_citations":[{"why":"Supplies the scanner model, the single-byte certified split point predicate, and the applicability table whose exact-empty rows this paper rescues.","marker":"[25]"},{"why":"The munch artifact whose asserted probes, random grammar sweep, and scanner executions produce every empirical figure in the evaluation.","marker":"[24]"},{"why":"Provides the RFC 8259 JSON lexical forms over bytes used for the JSON row of the named token-set evaluation.","marker":"[6]"}],"fun_headline_variants":["Windows prove token starts where bytes fail","91 token sets gain certified split windows","Certified windows: safe splitting without speculation","From bytes to windows: 91 token sets re-enabled"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that no token matches the empty string, so every successfully scanned token consumes at least one byte; if a token could match empty, the maximal-munch semantics, the acceptance-gated seed, and the representation invariant would break, and the proof would not cover the token set.","fun_headline_variants_meta":{"raw":{"variants":["Windows prove token starts where bytes fail","91 token sets gain certified split windows","Certified windows: safe splitting without speculation","From bytes to windows: 91 token sets re-enabled"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000998,"raw_usage":{"total_tokens":4298,"prompt_tokens":1088,"completion_tokens":3210,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":704,"completion_tokens_details":{"reasoning_tokens":3154}},"tokens_in":704,"tokens_out":3210,"duration_ms":21396,"temperature":1.0,"reasoning_tokens":3154,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T11:15:59.109678+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One completely tokenizable input containing a model-certified window $(W,o)$ whose maximal-munch tokenization makes the token covering the window's final byte begin at an offset different from $o$ would falsify Theorem 1; the paper's own rewind-stress rows, which found zero such disagreements across 1,079,392 generated executions, are exactly the kind of check that could uncover such a counterexample.","supporting_citations":[{"cited_title":"Certified Split Points for Parallel Lexing: Exact and Modulo Discarded Tokens","cited_arxiv_id":"2608.03473","evidence_quote":"Supplies the scanner model, the single-byte certified split point predicate, and the applicability table whose exact-empty rows this paper rescues."}],"review_version":1}