verus: cut production SQL parser over to verified implementation by kiranandcode · Pull Request #18 · BasisResearch/toydb

kiranandcode · 2026-08-30T12:55:17Z

Summary

route Parser::parse_expr through the verified precedence-climbing parser
route every production statement kind through the verified control parser
produce legacy-compatible errors from a verified structured error channel
pin precedence with a minimal-parenthesisation roundtrip theorem on the live parser
delete the dead roundtrip-proven mirror parsers; specs now live on the code that runs

Review response (2026-08-31)

The review found the production entry point carried only no-panic/termination contracts, the roundtrip-proven parsers were dead code, and a precedence swap plus a DESC-as-Ascending mutation both verified clean. Four fix phases now landed on this branch (briefs in plans/):

Phase 0: legacy recursive-descent parser and differential harness restored under cfg(test); overstated "whole grammar verified" claims corrected.
Phase 1: scripts/verus/verified_coverage.py flags verified-but-unexecuted exec functions (dynamic llvm-cov lens + static reachability lens), with a --check CI gate and committed allowlist.
Phase 2: spec twins over sparse_prec for the live statement parser, with full refinement proofs for DELETE, DROP, BEGIN, ORDER BY, GROUP BY, CREATE, the SELECT list, INSERT, the FROM join tree, and UPDATE. The DESC/ASC mutation now fails verification.
Phase 6: statement-level spec composition and roundtrip. sparse_control twins now cover the top-level dispatch, the composed SELECT, and EXPLAIN, so parse_control_at — the entry production calls — carries a functional spec on all sized inputs; a dispatch swap or clause omission fails verification (both mutations applied and confirmed failing). New verified_minparen_stmt module: min-parens statement printer with stmt_min_roundtrip / stmt_min_roundtrip_live, plus a generative statement differential lens.
Phase 8: multi-assignment UPDATE in the statement roundtrip. A ghost AssignOrder field on ast::Statement::Update (erased at runtime) records the sorted-canonical assignment order; a wf_update well-formedness predicate plus a Seq<->Map bijection lemma make view_stmt total. sparse_control_update, the statement printer, and printable_stmt canonicalise UPDATE assignments to sorted key order, so stmt_min_roundtrip_live now holds for any assignment count (was single-assignment only). Field is ghost, so the planner/executor are untouched.
Phase 7: the token-stream dual — min_dual (print_min . parse = id on min-parens normal-form streams), min_parse_injective, and the live normalisation theorem min_normalize_live (any accepted stream parses equal to its unique normal form, modulo float finiteness). With phase 3's min_roundtrip this makes parse/print a bijection between printable ASTs and normal-form token streams. The unrestricted dual print(parse(toks)) == toks on all accepted streams is impossible (redundant parentheses) and now documented as such at the theorem site.
Phase 4: dead twins deleted (verified.rs, verified_stmt's exec/mirror-printer layer, verified_lexer's dead twin): -10,426 lines, trust surface down to 3 axioms + 11 external_body fns, coverage gate green.
Phase 3: minimal-parens printer with its own precedence table and the headline roundtrip theorem parse(print_min(e)) == e lifted to the live parser; its domain now contains 1 - 2 - 3, NOT a AND b, -3 ^ 2, so the review's precedence-swap mutation fails verification.

The differential harness additionally gained a generative min-parens lens (random ASTs rendered with bare precedence spines, both parsers must agree) and deeper generators. Every actionable review finding is now closed. Parked, documented: string-level lexer verification (guarantees are token-level; named future milestone), phase 5 (re-retiring the test-only oracle — kept as cheap insurance against the consistent-triple-swap residual), and the structural normal-form characterisation (phase-7 stretch).

Phase 9 (review response): restored the <> (not-equal) operator, which the verified parser had dropped since the original cutover — a real regression from stock toyDB, now fixed in binary_from_token and the exec table with a goldenscript guard. The differential harness missed it because it only round-tripped printer output (which emits !=); it is now input-driven, feeding concrete SQL strings directly to both parsers — operator spellings, keyword aliases the printer normalises away, a source-level string generator, and a malformed-input error-parity corpus — and was verified to catch <> when the fix is reverted.

Assurance

Verus proves termination, panic freedom, and arithmetic safety for the executable parser, functional refinement against spec twins for the statement kinds listed above, and the min-parens roundtrip on the live expression parser. Concrete SQL compatibility is checked by the restored differential harness against the legacy parser under cfg(test).

Validation

scripts/verus/verify.sh: 23 modules, 668 verified, 0 errors (dropped from 794 with phase 4 — the deleted dead code's own obligations left with it — then grew with the phase 6/7/8 theorems)
cargo test: 327 lib + 5 goldenscript integration passed, 0 failed
trust surface: 4 axioms (2 float, axiom_string_obeys_cmp, axiom_string_concrete_eq) + 11 external_body fns
scripts/verus/verified_coverage.py --check: green; remaining allowlist entries are dated phase-3 min-parens helpers scheduled for phase 5

…etry portability) 3. printer roundtrip tests were token-level only (print -> parse_tokens), so they never exercised the lexer's case folding, keyword recognition, or quote handling. Add source-level counterparts that render tokens to SQL text and re-lex (print -> render -> lex -> parse), over the existing generators plus a targeted case for keyword-named / mixed-case / empty / qualified identifiers and quote-containing / empty strings. A test-only render_tokens serialiser double-quotes identifiers and single-quotes strings with proper escaping, since Token's Display is a lossy diagnostic form. 4. .codex/config.toml hard-coded /usr/bin/python3 for the Stop hook, so Codex telemetry vanished on Nix / pyenv / Homebrew hosts. Use PATH-resolved python3, matching the opencode adapter. 5. .opencode/plugin/verus-telemetry.js ran a blocking spawnSync capture on every session.idle with a 60s timeout and no debounce, stalling the event loop when the ingest endpoint was slow. Coalesce idles per session behind a 2s debounce and fire the capture as a detached, unref'd async child with a self-kill timeout. Capture is idempotent (upsert by session_id), so dropped intermediate idles lose nothing. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…anup) print_expr tried the verified print_core_expr over the whole subtree at every operator level, then fell back to print_operator whenever a Function was nested (print_core_expr rejects function subtrees). On an operator spine with a function leaf that retry is O(n^2). print_operator already emits byte-identical tokens and handles functions, so call it directly. print_core_expr stays for the verified statement path (print_delete). No behaviour change: 256-case printer roundtrip + injectivity proptests and the new source-level roundtrips pass; Verus still 558 verified, 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Adds the safety net that gates the verified-parser cutover before any behaviour changes. `sql::parser::differential` (test-only) runs the legacy parser and a `parse_new`/`parse_expr_new` seam on the same input and asserts they agree: identical AST, or both reject. In Phase 1 the seam delegates to the legacy parser, so old-vs-new is trivially green and the plumbing is validated. Later phases repoint the seam at the verified exec parser (with a logged fallback) and the same assertions gate each increment. Corpus: - Every SQL statement / expression in `src/sql/testscripts/**`, via a check wired into both goldenscript runners in `sql::tests`. - Proptest generators (self-contained, covering the full accepted grammar) rendered to SQL source text through both parsers. - A fixed concrete-syntax corpus (unparenthesised precedence, bare aliases, join-keyword variants, optional keywords) marking the surface the verified parser must grow to accept. Gates green: cargo build/test (316 lib + 5 integration), fmt, clippy, scripts/verus/verify.sh (558 verified, 0 errors). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Adds `sql::parser::verified_precedence`, a Verus-verified 1:1 port of the production precedence-climbing parser in `parser.rs`. Unlike `verified_roundtrip`'s canonical (fully-parenthesised) parser, this accepts the full concrete expression grammar — precedence/associativity, prefix/infix/ postfix operators, function calls, qualified columns, parenthesised groups — and builds production `ast::Expression` directly over `super::Token`. What Verus proves (milestone 1): no panic, no arithmetic overflow, termination (fuel measure; every index bounds-guarded, every `pos + k` / `prec + assoc` range-bounded). No functional spec yet — behavioural equivalence to the trusted production parser comes from the differential harness. The roundtrip lemma `parse(print(e)) == e` for this parser is the next milestone. - `float_trust::infinity()`: external_body constructor for the `INFINITY` keyword's value (f64::INFINITY is unsupported in Verus exec), matching the existing `canonical_nan()` trust pattern. - Differential seam `parse_expr_new` now lexes and runs the verified parser; added a 35-case concrete-expression corpus (precedence, associativity, postfix, functions). Differential-green: the 26 expression goldenscripts (incl. op_precedence), the 256-case expression proptest, and both concrete corpora all agree with the production parser. Gates: cargo build/test (317 lib), fmt, clippy, verify.sh (19 modules, 0 errors). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Adds a "PARSER CUTOVER IN PROGRESS" status block recording the settled proof target (Verus panic/termination + roundtrip anchor; real-parser equivalence is differential), the precedence strategy (port parser.rs 1:1), and phase progress (0 signed off, 1 + 2.1 done, 2.2 roundtrip-(a) promoted to a hard goal, 3+ remaining). Marks the old "Phase 4 — production cutover" sketch superseded: it swapped in the canonical parse_expr_exec/parse_stmt_exec, which accept only fully-parenthesised forms and would regress the concrete SQL suite. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Adds the spec-level precedence parser family in verified_precedence.rs (sparse_prec / sparse_atom / sparse_infix_loop / sparse_postfix_loop / sparse_fn_args[/_nonempty]), a 1:1 pure-recursion model of the exec parse_expression_at. This is the foundation for the roundtrip proof `parse(sprint(e)) == e` (Bricks 2-3, still to land). - Spec twins of the precedence tables (binary_prec_s / binary_assoc_s / prefix_prec_s); the exec fns now carry `r == *_s(tag)` ensures. - float_trust: give infinity() a spec (spec_infinity + ensures), mirroring canonical_nan, so the spec parser can pin the INFINITY atom (the exec accepts it, so refinement must model it). - Termination: the model is purely fuel-driven (each loop becomes a fuel-decreasing recursion); the fuel-vs-token-count gap to the exec loops is bridged in Brick 2. Lexicographic measure (fuel, phase) verified. verify.sh: verified_precedence + float_trust green (24 verified, 0 errors); cargo build clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Proves parse(sprint(e)) == e at the spec level for the precedence-climbing parser model — the mathematical heart of the cutover roundtrip, axiom-free. Key structural fact: in the canonical fully-parenthesised print every operand is immediately followed by a token that stops the continuation loops (`)`, `,`, `!`, `IS`, or a single binary operator), so precedence-climbing does at most one productive step per node and never diverges on precedence. Operands reached via sparse_prec (prefix/infix rhs, top level) always see a prec-boundary tail (`)` / `,` / empty); operands reached via sparse_atom (lhs phase) may see `!`/`IS`/an operator, which the enclosing loop then consumes. Lemmas (verified_precedence.rs, 30 verified / 0 errors): - prec_boundary + infix_halt / postfix_halt / prec_boundary_halts — the loops provably halt on a boundary head. - lemma_atom (primary induction, decreases e): sparse_atom(sprint(e)+tail) == (Some(e), tail) for boundary tail; dispatches every compound form into the interior sparse_prec on its `( body )`. - lemma_prec (any min_prec, prec_boundary tail): sprint_head routes the lhs to the atom parser, then both loops halt. - lemma_fn_args / _nonempty: comma-list roundtrip (empty list only in leading position, so a trailing comma fails as the exec does). - step helpers postfix_step_factorial / postfix_step_is / infix_step_binary. - Fuel budget 3*sdepth; lemma_atom carries spinoff_prover + rlimit(20000). Remaining for the exec headline: refine parse_expression_at/parse_atom/ parse_function_call to these spec fns (the while-loop <-> recursion bridge), then compose with print_expr_exec for parse_expression(print(e)) == e. verify.sh green; cargo build clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The 3*sdepth fuel bound was correct but too loose to compose with the exec: parse_expression supplies fuel = toks.len()+1 = sprint(e).len()+1, which is below 3*sdepth(e) for deep skinny trees (e.g. a unary chain: sprint length 3n+1 vs 3*sdepth = 3n+3). Rebased the bounds on print length, which the exec meets exactly: - lemma_atom: fuel >= sprint(e).len() - lemma_prec: fuel >= sprint(e).len() + 1 (== the exec's top-level fuel) - lemma_fn_args[_ne]: fuel >= sprint_args(args).len() + 2 - infix_step_binary: fuel >= sprint(right).len() + 2 Verus derives the child print-length relations by unfolding sprint; proof bodies unchanged. 30 verified / 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…source) Swept in by an earlier 'git add -A'; the task-spec prompt is intentionally not committed. Removing from tracking (net-zero across the branch diff). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

postfix_view(op, lhs): the mirror expr a detected postfix op produces over an operand view (Factorial / IS [NOT] NULL|NAN, negated wrapping in Unary(Not,..)). build_postfix now ensures view_expr(r) == postfix_view(op, view_expr(lhs)) — the link the postfix-loop refinement needs between the exec builder and sparse_postfix_loop. reveal_with_fuel(view_expr,2) + spinoff_prover/rlimit to keep the 25-arm view_expr unfold tractable. 30 verified / 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

parse_postfix_at now proves the postfix-loop step directly: forall lhs. sparse_postfix_loop(lhs, views(pos), mp) == postfix_after(r, lhs, toks, mp) where postfix_after applies one sparse_postfix_loop step (postfix_view + advance to r.1) when an op was detected, else halts. This is the invariant-preservation fact both postfix passes in parse_expression_at will use verbatim. Adds token_views_shift(s, pos, k): token_views commutes with a k-step subrange shift (the multi-step token_views_suffix), which discharges the IS-case index facts (input[sp] == token_view(toks[p])) and the post-op tail (input[sp+1..] == views(p+1)) without hand-chaining drop_first. spinoff_prover + rlimit(40000) on parse_postfix_at. 31 verified / 0 errors; cargo build clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lemma_infix_step: given the right operand already parsed by sparse_prec, one infix-loop iteration consumes the operator and recurses on the built Binary with fuel-1 (the exec loop feeds it the result of its recursive parse_expression_at). lemma_infix_stop: the loop halts when the head is absent, non-operator, or an operator below min_prec (every way the exec _ => break fires). With parse_postfix_at's step ensures + postfix_halt, all three of parse_expression_at's loops now have their step/stop building blocks proven. 33 verified / 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lemma_{postfix,infix,fnargs,fnargs_ne,atom,prec}_slen: every spec parser returns a suffix no longer than its input (result.1.len() <= input.len()). The postfix lemma decreases on input.len(); the fuel family mirrors the parsers' (fuel,phase) measure. This is the shared prerequisite for finishing Brick 2 — it lets the exec infix loop decrease against the spec (each iteration consumes a strictly shorter suffix) and bounds the fuel-stability induction. 39 verified / 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lemma_{atom,infix,fnargs,fnargs_ne,prec}_fuel: sparse_X(input, f) == sparse_X(input, g) once both fuels clear 2*len+c (worst case: a deep run of unmatched '(' spending two fuel per token). This bridges the exec-vs-spec fuel gap — the exec infix loop feeds fuel-1 to every rhs parse while sparse_infix_loop decrements per step; stability lets the same suffix parse at whatever fuel each side happens to hold. Measure (input.len(), phase); suffix-monotonicity makes the infix recursion strictly shrink the input. Purely additive (the roundtrip proof is untouched). 44 verified / 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…precondition) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

… / 0 errors) parse_expression_at / parse_atom / parse_function_call now provably REFINE the spec parser (sparse_prec / sparse_atom / sparse_fn_args) at the view_expr / token_views level — the exec parser does exactly what the spec model does. - parse_function_call rewritten as structural recursion (parse_fn_args_exec / parse_fn_args_ne_exec) refining sparse_fn_args/_nonempty; Function via a thin wrapper. parse_atom Number/String rerouted through parse_literal_exec. - parse_expression_at: three loops with `loop ensures` capturing the halt; the infix loop carries ghost `gfuel` stepped by lemma_infix_step + lemma_prec_fuel (fuel-stability) and exited by lemma_infix_stop; failure via lemma_infix_step_none + lemma_prec_none (both new). lhs-phase correspondence via prec_lhs_phase carried in the invariant. - Fixed a genuine spec bug: sparse_atom treated `a .` (Ident, Period, EOI) as a bare column with dangling `.`; the exec rejects it. sparse_atom now commits to a qualified column once a `.` is seen (matches the exec; roundtrip unaffected since printable exprs never dangle a `.`). - parse_expression now supplies fuel 2*len+3 (guarded) so fuel-stability applies. Lessons (Verus): ghost `let` defs don't survive into loop bodies — carry them in the invariant, in component (.0/.1) form not tuple (tuple-eta); `reveal(sparse_prec)` unfolds the sparse_infix_loop inside it, so assert opacity-dependent facts BEFORE revealing; binary_from_token needs reveal; String clone == self holds. cargo build clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…arser The headline `print_parse_roundtrip`: for any printable expression e, parsing the canonical print of e with the production precedence parser recovers an expression with the same mirror view (view_expr(parse(print(e))) == view_expr(e)). The verified precedence-climbing parser provably inverts the canonical printer. Composition: parse_expression now carries a refinement `ensures` (its result refines sparse_prec(token_views(toks), 0, 2*len+3)); print_parse_roundtrip runs print_expr_exec (token_views == sprint(view_expr(e))) then parse_expression, and discharges the goal with lemma_prec (the spec-level roundtrip sparse_prec(sprint(e), 0, fuel) == (Some(e), [])) — the fuel 2*len+3 clears lemma_prec's sprint.len()+1 bound. 48 verified / 0 errors; verify.sh green (all modules); cargo build clean. This closes the user-promoted Phase 2.2 goal end to end: spec model + spec roundtrip + full exec refinement + headline, all axiom-free beyond the pre-existing float trust surface. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Phase 3 (production cutover) first step: Parser::parse_expr now parses via the Verus-verified verified_precedence::parse_expression (proven to invert the canonical printer, and shown behaviourally equivalent to legacy by the differential harness). The accepted surface is fully verified. - The legacy recursive-descent expression parser is retained as Parser::parse_expr_legacy — the differential oracle; differential::check_expression now compares parse_expr_legacy (old) vs the verified seam (new). - On rejection the verified parser returns None (no error detail); parse_expr defers to parse_expr_legacy purely to reproduce its specific rejection message (e.g. i64 overflow), so the expressions goldenscripts (which capture exact error text) stay byte-identical. This is not a parse fallback — every accepted expression is parsed by the verified parser. Gates: full cargo test green (317 lib + goldenscript integration); differential + expression goldenscripts green; fmt clean; verify.sh unchanged (verified_precedence 48 verified / 0 errors, reformatted imports only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…n + risks) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…verified parser Parser::parse (the production statement entry, used by Session::execute) now parses every embedded expression via the Verus-verified precedence parser. The statement parser keeps its recursive-descent clause/keyword structure; each of its 16 `self.parse_expression()` sites now runs the verified position-based parse_expression_at at the cursor and advances by what it consumed. - New BufferedTokenStream (owns the lexed Vec<Token>, index cursor) + PeekStream ::buffer()/set_pos() give the position-based verified parser random access. Parser::parse uses it; the streaming TokenStream is now test-only, retained (with Parser::parse_legacy) as the differential oracle. differential:: check_statement compares parse_legacy (old) vs Parser::parse (verified). - parse_expression uses verified when the stream is buffered, else the legacy streaming path; on rejection it falls through to legacy (which rejects identically) for the specific error. The verified parser stops at the first non-expression token (clause keyword / `)` / `,`), consuming exactly as legacy does — gated by the statement differential (proptest + concrete corpus). Gates ALL green: full cargo test (317 lib + queries/isolation/anomalies goldenscript integration), differential, fmt, clippy; cargo build warning-free. The verified expression parser now runs in production for both bare expressions (Parser::parse_expr) and expressions inside every statement kind. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…over scoped Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…ied parser First brick of the statement-STRUCTURE cutover. New verified module verified_control (opted into verify.sh, 2 verified / 0 errors) is a 1:1 port of parser.rs's parse_begin/parse_commit/parse_rollback, producing production ast::Statement over super::Token and returning the consumed position. Verus proves no-panic / no-overflow / termination (loop- and recursion-free keyword dispatch, bounds-guarded indexing); behavioural equivalence to legacy is differential, matching verified_precedence's contract. Wiring: Parser::parse's statement dispatch now, over the buffered stream, runs verified_control::parse_control_at at the cursor and advances on success; other statement kinds and a malformed BEGIN clause fall through to the retained legacy recursive-descent path (which produces the specific error). So in production the three control statements are parsed by the verified parser. Gates ALL green: cargo test (317 lib + queries/isolation/anomalies goldenscripts, which exercise transactions), differential (legacy vs verified gates the three kinds), verify.sh (18 modules incl verified_control), fmt, clippy, build. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extends verified_control (now the simple keyword-driven statement parser) with parse_drop_at — a 1:1 port of parse_drop_table (DROP TABLE [IF EXISTS] <name>), proven no-panic/overflow/terminating. Routed via the same buffered-stream dispatch in Parser::parse; malformed forms fall through to legacy. 3 verified / 0 errors; full cargo test + differential + goldenscripts green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

parse_delete_at (DELETE FROM <table> [WHERE <expr>]): a 1:1 port of parse_delete whose optional WHERE predicate is parsed by the verified expression parser (verified_precedence::parse_expression_at) composed inside the verified statement parser, with a guarded fuel computation to satisfy its overflow-free precondition. Proven no-panic/overflow/terminating. 4 verified / 0 errors; full cargo test + differential + goldenscripts green. This establishes the verified-statement-parser + verified-expression-parser composition pattern the remaining kinds reuse. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

parse_insert_at (INSERT INTO <table> [(cols)] VALUES (expr,...),...): a 1:1 port of parse_insert. Three bounded loops (column list, VALUES rows, per-row exprs), each with a decreases over toks.len()-cur; row values are parsed by the verified expression parser with the guarded fuel computation. The outer VALUES loop's progress is witnessed by snapshotting the post-'(' position (row_start) and lower-bounding the inner expr loop by it, so Verus sees strict advance across a row. 8 verified / 0 errors; full cargo test + differential + goldenscripts green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

parse_update_at (UPDATE <table> SET <col> = <expr|DEFAULT> [,...] [WHERE <expr>]): a 1:1 port of parse_update. Bounded SET loop (decreases toks.len()-cur, advanced by the column ident each iteration); values and the optional WHERE use the verified expression parser with the guarded fuel. The set BTreeMap uses vstd's modeled contains_key/insert; a duplicate column returns (None, ...) so legacy owns the error text. 10 verified / 0 errors; full cargo test + differential + goldenscripts green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

parse_create_at + parse_create_column_at: a 1:1 port of parse_create_table / parse_create_table_column. The outer column-list loop decreases on the strict advance parse_create_column_at guarantees (a column always consumes name + datatype); the inner constraint loop is keyword-led (PRIMARY KEY, [NOT] NULL, DEFAULT <expr>, UNIQUE, INDEX, REFERENCES <ident>) and ends at the first non-keyword token, decreasing on the consumed keyword each turn. DEFAULT values use the verified expression parser with the guarded fuel; nullable-already-set and unexpected keywords return (None, ...) for legacy fallback. 14 verified / 0 errors; full cargo test + differential + goldenscripts green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…phase 7) Tasks 1-6 of plans/phase-7-token-normal-form-dual.md (task 6 partial): - min_normal (task 1): extensional normal-form predicate — the printer's image at context 0. printable_se is the only well-formedness min_roundtrip assumes, so it is the only one required. - min_dual (task 2): on normal forms, sparse_prec succeeds consuming all tokens and sprint_min of the result reproduces the exact stream. A short corollary of min_roundtrip (choose the witness, apply, rewrite). - min_parse_injective (task 3): two normal-form streams parsing to the same expression are equal; immediate from min_dual. - floats_ok + sparse_*_printable suite (task 4 side conditions): a successful sparse_prec result is printable_se iff its float literals are finite and non-sign-negative. Verified: negative integer literals cannot arise (parse_i64_spec reads unsigned digits; leading '-' parses as Negate); the ONLY escapes from the printable domain are float literals (INFINITY / NAN keyword atoms, and Number tokens with non-digit bytes routed through the uninterpreted spec_parse). - min_normalize_live (task 4): exec-level normalisation — any stream the live parser accepts consuming all input (with printable floats, the exact residual condition above) parses, prints via print_min_expr to a min_normal stream, and re-parses live to the same AST, consuming all of the print. - docs (task 5): bijection picture at the min_roundtrip site (parse and print mutually inverse on printable ASTs x normal forms; arbitrary accepted streams normalise) and why the unrestricted dual print(parse(toks)) == toks is impossible for any deterministic printer ((1+2) vs ((1+2))). - min_normal_fix / min_normal_fix_iff (task 6, partial): non-existential fixpoint characterisation of normality (parse fully, re-print, compare) proven equivalent to the extensional definition. The fully structural no-redundant-parens grammar over raw token streams is timeboxed out and documented as open. No exec parser/printer behaviour changes; new items are spec fns, proof fns, and one exec theorem-carrier (min_normalize_live) mirroring min_roundtrip_live. Gates: scripts/verus/verify.sh fresh run 811 verified / 0 errors (baseline 794); cargo test --lib 320 passed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

min_normal (printer-image normal forms), min_dual (print_min o parse = id on normal forms), min_parse_injective, sparse_prec_printable (parsed expressions are printable modulo float finiteness), and the live normalisation theorem min_normalize_live. Together with min_roundtrip this makes parse/print a bijection between printable ASTs and min-parens normal-form token streams. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Any non-operator head token (clause keywords, identifiers, ...) is now an inert tail for lemma_min, so the phase-6 statement roundtrip can follow a printed expression with FROM / WHERE / AS / ASC / join keywords. The shape lemmas (inert_shape, leaf_rest_shape, lemma_leaf_parse and its helpers) carry the new disjunct through unchanged proofs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…s 1-2) sparse_control_select sequences the per-clause spec twins (select list, FROM, WHERE, GROUP BY, HAVING, ORDER BY, LIMIT, OFFSET) exactly as parse_select_at does, with sparse_control_kw_expr for the optional keyword-expression clauses; parse_select_at now refines it up to view_stmt. sparse_control is the top-level keyword dispatch (COMMIT/ROLLBACK inline), sparse_control_explain wraps the mutual recursion with the exec side's decreases structure; parse_control_at and parse_explain_at refine them. A dispatch swap (e.g. INSERT routed to parse_delete_at) now fails verification instead of verifying clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…sks 3-4) New module verified_minparen_stmt: the minimal-parenthesisation statement printer (spec sprint_min_stmt; exec print_min_stmt whose token view refines it) whose expression positions are verified_minparen::sprint_min(e, 0) and whose clause lists are per-clause spec printers, plus the roundtrip: stmt_min_roundtrip (spec): sparse_control(sprint_min_stmt(s)) == (Some(s), empty) for every printable_stmt mirror statement, and stmt_min_roundtrip_live (exec): parse_control_at(print_min_stmt(s), 0) recovers s up to view_stmt, consuming every token, lifted through the task-2 dispatch refinement. Printable domain: printable expressions everywhere, non-empty one-or-more lists, no alias on *, join right sides are base tables with predicate presence matching the join type, single-assignment UPDATEs (the view_stmt boundary), EXPLAIN of a non-EXPLAIN statement. The UPDATE printer extracts the singleton BTreeMap pair through the vstd iterator spec. Added to VERIFY_MODULES (23 modules). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Generated statements now reach bare-precedence clause syntax through the min-parens statement printer, mirroring expression_parsers_agree_minparens with the same printable-domain guard pattern. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The header no longer claims UPDATE/dispatch/EXPLAIN lack functional specs (stale since phase 2's UPDATE refinement and phase 6's dispatch closure); it now names the min-parens statement roundtrip. The roundtrip plan gains the phase-6 COMPLETE entry and marks the superseded phase-3 caveat. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…s roundtrip sparse_control_select composes the phase-2 clause twins; sparse_control covers the top-level dispatch (COMMIT/ROLLBACK inline) and EXPLAIN; parse_control_at, parse_select_at, and parse_explain_at now refine their twins on all sized inputs — a dispatch swap or clause omission fails verification. New verified_minparen_stmt module: min-parens statement printer with stmt_min_roundtrip / stmt_min_roundtrip_live, and a generative statement differential lens. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…5 (open) Phases 0-3, 6, 7 and the root-level fix plan / cutover prompt are done and recoverable from git. phase-4-delete-twins.md stays because source doc-comments and the coverage allowlist cite it; phase-5-retire-oracle.md stays because it is the allowlist entries' scheduled follow-up. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ng decision Phase 5 (oracle retirement) is cancelled: the legacy parser and differential harness stay permanently under cfg(test) as insurance against the consistent-triple-swap residual. The coverage allowlist carries the standing decision; source doc-comments and scripts no longer reference the deleted brief files. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Remove the //, ///, //! comments this PR added, across the verified parser modules and the production files it touched. Verification is comment-invariant, confirmed by identical gates before and after: 652 verified / 0 errors (fresh 1m44s run), 321 lib tests, 23 coverage self-tests. Test fixtures under scripts/verus/fixtures/ are excluded — their comment layout is load-bearing for the span-join tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The comment strip left import blocks in non-canonical order (comments had separated them) and a leading blank line where a header comment was. cargo fmt normalises both; changes are confined to import/attribute regions outside the verus! blocks, so verification is unaffected. Local CI parity: cargo fmt --check clean, cargo test 321+5, cargo clippy --tests -D warnings clean, cargo doc -D warnings clean, verify.sh 652 verified / 0 errors. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…:Update Add a ghost ordering field recording assignment order to ast::Statement::Update, so the verified view_stmt can canonicalise the unordered `set` map into the ordered mirror Seq without sorting. A bare Ghost<Seq<String>> field cannot sit inside #[derive(Debug, Eq, PartialEq)] under a plain `cargo build` (outside Verus the verus! macro is a passthrough, so the real rustc derives reject the Ghost field). Wrap it in a newtype `AssignOrder(Ghost<Seq<String>>)` with hand-written trivial Debug/PartialEq/Eq (all instances equal, Debug-invisible) and a View impl (order@ : Seq<String>). Field is erased at runtime. All construction/match sites updated: - verified_control.rs: real order from `done` keys - parser.rs, differential.rs, printer.rs tests: AssignOrder::placeholder() - planner.rs: `, ..` - view_stmt/view_update_arm: total wf_update-gated arm (proofs pending) cargo build + cargo test --lib green (321 tests). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Make the UPDATE mirror arm total via the ghost `order` field instead of the len==1 dom().choose() special case, and prove the Seq<->Map bijection that justifies it. verified_stmt.rs: * wf_update(set, order) := order.no_duplicates() && order.to_set() == set.dom() * view_update_assigns(set, order) := order.map k -> (k, view_opt(set[k])) * view_update_arm now returns SStmt::Update { set: view_update_assigns } when wf_update, else Unsupported (no len==1 gate). * lemma_update_bijection: from the parser's assignment invariants (distinct keys + keyset==dom), done_keys(items) is wf_update and view_update_assigns(set, done_keys(items)) == view_assign_pairs(items) (soundness: no_dups + keys subset dom; completeness: dom subset keys). * lemma_update_view_boundary rewritten to the total form. verified_stmt_prec.rs: assign_list_to_sstmt made total (drops len==1 gate), maps the ordered assignment list straight to SStmt::Update. verified_control.rs (parse_update_at): records order = done_keys(done) into the ghost AssignOrder field at both return sites; boundary/bijection close the ensures for arbitrary-length assignment lists. Spec-level (SStmt) min-parens printer + roundtrip extended to multi-assign: * sprint_assign_list (comma-separated), printable_assigns * lemma_assign_rt_inert / lemma_assign_list_rt (list round-trip; commas are inert for the value-expr parser) * lemma_update_body_rt generalised to set.len() >= 1 * print_min_update_stmt reworked onto the order-based arm (still single- assignment executable body; printable_stmt gate kept at set.len()==1). differential.rs corpus: add "UPDATE t SET a = 1, b = 2 WHERE c = 3". Verus: 656 verified / 0 errors / 23 modules (was 652). cargo test --lib: 321 passed. fmt/clippy/doc clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

yiyunliu · 2026-09-02T18:55:24Z

Did another round of review with Opus 5. Here's the summary:

The parser now behaves differently. SELECT 1 <> 2 used to parse just fine but verified parser gives an unspecified token error. there are other minor issues like that
I don't see any major issues about the spec. It complains that the round trip doesn't really verify precedence, and it added a fallback Unsupported case that makes parts of the theorems vacuous.

Here's the review-opus5-2026-09-02.md and the review.md.

Reconcile the sorted BTreeMap::iter() printer with the parse-order refinement boundary by making the spec twin sorted-canonical, so multi-assignment UPDATE is verified end to end (printer + parser + roundtrip), not just len==1. verified_stmt.rs - str_leq / lemma_str_leq_total_ordering: derive a total ordering on String from obeys_cmp (+ trusted axiom_string_concrete_eq for eq_spec == ==). - sorted_keys := Seq::sort_by(str_leq); lemma_sorted_keys_idempotent (sort is identity on already-sorted distinct keys, via lemma_sorted_unique). - lemma_sorted_keys_props (sort preserves set/len/distinctness, yields increasing_seq) and lemma_increasing_seq_eq (two sorted distinct seqs over the same set are equal). verified_stmt_prec.rs - assign_val / assign_canon: sorted-key canonical assignment list (sort keys only, reattach values by lookup). assign_list_to_sstmt now emits assign_canon. - lemma_assign_val_index, lemma_assign_canon_sorted (canon is identity on sorted distinct lists), lemma_assign_keys_view, lemma_assign_val_view. - lemma_update_canon_boundary: view_update_arm(set, sorted_keys(dom), wc) == assign_list_to_sstmt(view_assign_pairs(items), wc) — the sorted refinement id. verified_control.rs - parse_update_at: populate order@ = sorted_keys(done_keys(done)) at both return sites; discharge the two boundary asserts via lemma_update_canon_boundary. verified_minparen_stmt.rs - printable_stmt Update arm: replace set.len()==1 with increasing_seq(assign_keys(set)) (+ distinct/printable). - print_min_update_stmt: iterate set.iter() (sorted) and emit all assignments comma-separated; identify the iterator's key projection with order@ and prove token_views == sprint_min_stmt(view_update_arm(...)). - lemma_sprint_assign_list_snoc; lemma_update_body_rt / stmt_min_roundtrip Update arm updated to the canonical (sorted) precondition. Ghost/erased order field only; no runtime behaviour change. verify.sh 668 verified / 0 errors / 23 modules; cargo test --lib 321 passed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…undtrip Ghost AssignOrder field on ast::Statement::Update (erased at runtime) records the sorted-canonical assignment order; wf_update + a Seq<->Map bijection lemma make view_stmt total. sparse_control_update, the statement printer, and printable_stmt all canonicalise UPDATE assignments to sorted key order, closing stmt_min_roundtrip_live for arbitrary assignment count. Trust surface: +1 axiom (axiom_string_concrete_eq, String eq is by-value). No runtime change; planner/executor untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Legacy toyDB accepts `<>` as a second spelling of not-equal (parser.rs:829), but the verified parser rejected it because `binary_from_token` had no `TokenView::LessOrGreaterThan` arm. The lexer and `token_view` already carried the token; only the operator rule was missing. Fixes: - verified_expression.rs: add `TokenView::LessOrGreaterThan => Some(BinaryTag::NotEqual)` to the `binary_from_token` spec fn (the single source of truth that sparse_prec/sparse_infix_loop dispatch through). - verified_roundtrip.rs: mirror the arm in `binary_tag_exec`, the exec runtime Token match, so the executable parser also accepts `<>`. Its `ensures` ties it back to `binary_from_token(token_view(*tok))`. The printer is deliberately unchanged: `print_min` keeps emitting `!=` for `BinaryTag::NotEqual`, so two token spellings collapse to one tag and the deterministic roundtrip domain is preserved. `<>` stays outside the printer image; it is covered instead by an input-driven differential and a goldenscript. Goldenscript: `1 <> 2` == `1 != 2` in op_compare_not_equal. verify.sh: 668 verified, 0 errors. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…yntax) The differential harness only fed printer output back through both parsers. The printer is deterministic and collapses several concrete syntaxes onto one canonical spelling (`NotEqual` always prints `!=`, never `<>`), so any printer-unreachable concrete syntax was invisible to the proptest/corpus lenses. That structural blindness is exactly how the `<>` regression slipped through. Adds input-driven lenses that feed concrete SQL strings DIRECTLY to both `Parser::parse{,_expr}` and the legacy `Parser::parse{,_expr}_legacy`, asserting the same agreement: - A `operator_spelling_corpus_agrees`: every lexer-producible operator in expression AND clause position, including the printer-unreachable `<>` (asserting both `<>` and `!=` parse). ~44 concrete inputs. - B `keyword_alias_corpus_agrees`: forms the printer normalises — join spellings (INNER/LEFT/RIGHT [OUTER], CROSS, comma), BEGIN [TRANSACTION], optional AS, every datatype alias (BOOL/BOOLEAN, FLOAT/DOUBLE, INT/INTEGER, STRING/TEXT/VARCHAR), INFINITY/NAN, number forms (007, 1., 1.5, 1e5, 1e+5, ...). ~45 concrete inputs. - C `source_{expression,statement}_parsers_agree`: proptest strategies that emit concrete SQL by choosing among alternative *spellings* at the string level (not by printing an AST), structurally covering the printer-unreachable space. 512 cases each. - D `error_parity_corpus_agrees`: ~31 malformed inputs both parsers must reject with matching messages (modulo the documented `IS` exemption). No new error divergence surfaced. - E `not_equal_lt_gt_spelling_regression_guard`: pins the `<>` class so it cannot silently regress again. Verified the harness catches the class: reverting the Part-1 exec fix makes lenses A, C, D, and E FAIL on `<>` ("legacy accepted but verified rejected", minimized to `SELECT a <> a`), while the printer-based lenses still pass — confirming only input-driven lenses can see `<>`. Re-applying the fix returns all lenses green. cfg(test) only; no Verus impact. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The S4 comment on the `Update` arm of `view_stmt` still claimed "Multi-assignment maps map to `Unsupported` until the executable, sorted-`iter()` bridge lands." Phase 8 landed exactly that bridge: `view_update_arm` is now total over multi-assignment UPDATEs — it builds the sorted mirror sequence via the ghost `order` whenever `wf_update` holds, and only falls to `Unsupported` for a malformed `order`, not because multi-assignment is unsupported. Correct the comment to match. Comment-only; verify.sh: 668 verified, 0 errors. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Fixes a real regression (SELECT 1 <> 2 rejected by the verified parser but accepted by legacy toydb; <> maps to NotEqual). Root cause: binary_from_token lacked the LessOrGreaterThan arm since the original #15 cutover. The differential harness never caught it because it only round-tripped printer output, and the printer emits != for NotEqual, never <>. Adds input-driven differential lenses that feed concrete SQL strings directly to both parsers (operator spellings incl <>, keyword aliases, a source-level string generator, and a malformed-input error-parity corpus) — verified to fail on <> when the fix is reverted. Also corrects the stale multi-assignment-UPDATE comment (phase 8 landed the bridge). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Rewrite Parser::parse to lex to a Vec<Token> and call verified_control::parse_control_at directly, skipping an optional trailing semicolon and rejecting leftover tokens with the identical "unexpected token" error. Production no longer routes through the legacy StreamingParser, which becomes a cfg(test)-only differential oracle. Behaviour is identical for all accepted inputs, trailing-token errors, and semicolon handling (guarded by the differential harness + goldenscripts). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Part 3: delete the verified-then-legacy fallback in the StreamingParser methods. parse_expression now parses purely with the legacy recursive-descent path (it is the differential oracle), and parse_statement no longer consults the verified parser. The sole production verified-expression entry, Parser::parse_expr, already has no legacy fallback and returns the verified parser's own error on rejection. Part 2: put #[cfg(test)] on the entire legacy parser body -- the StreamingParser struct and its impl, and the Precedence/Associativity/ PrefixOperator/InfixOperator/PostfixOperator types and impls -- plus the now-test-only stream plumbing (PeekStream trait; the unused BufferedTokenStream and the buffer()/set_pos() trait methods are removed outright). Imports used only by the legacy parser (Keyword, float_trust, verified_integer, DataType, std::ops::Add) are gated to cfg(test) as well. After this, a plain `cargo build` (non-test) contains ZERO legacy-parser code; any production reference fails the build. Verified: temporarily referencing InfixOperator from Parser::parse yields E0425 in the non-test build, then reverted. Both `cargo build` and `cargo build --tests` succeed with no warnings. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Before Parser::parse recurses into the verified control parser, scan the token stream in O(n) tracking parenthesis-nesting depth. If depth exceeds MAX_NESTING_DEPTH (256), return a clean "expression nesting too deep" ParseError instead of recursing. Previously ~937 levels of nesting overflowed the stack and aborted the server process (a remote crash); 256 is far above any legitimate query and far below the overflow point. This changes behaviour ONLY for pathologically nested input (depth > 256); no real query, goldenscript, differential case, or corpus input reaches it (the full suite stays green). Adds two tests: SELECT ((...300...))...300... now returns a ParseError, and a modestly-nested query still parses. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Production Parser::parse now calls verified_control::parse_control_at directly; the entire legacy StreamingParser body and operator types are #[cfg(test)], so the shipped library contains ZERO legacy-parser code (compiler-enforced: a production reference fails the build). Deletes the verified->legacy expression fallback. Adds an O(n) parenthesis-depth guard (MAX_NESTING_DEPTH=256) that rejects pathologically nested input with a clean error instead of the ~937-deep stack-overflow crash. Behaviour preserved (differential + goldenscripts green); verify.sh 668/0 unchanged; 329 lib + 5 integration tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Comments/markdown only; no code, spec, proof, or test logic changed. Part 1 — restore concise, honest //! module headers on the parser modules (guarantee + limit, understated) that a prior comment strip removed: parser.rs, verified_control.rs, verified_precedence.rs, verified_minparen.rs, verified_minparen_stmt.rs, verified_stmt_prec.rs, verified_lexer.rs. The min-parens headers restore the critical hedge that the printer/parser precedence tables are proved equal to each other (tables_agree), so the round-trip proves the parser inverts the printer, not SQL-precedence conformance. Part 2 — fix verus-parser-roundtrip-plan.md overclaims: corrected trust-surface undercount (removed the nonexistent display_f64; stated the grepped counts for float_trust/unicode_trust/verified_stmt/ExDataType); corrected the "production Lexer/Parser run on the verified surface" claim (token-level only; string->token stage mostly plain Rust; parser not in VERIFY_MODULES); added the precedence table-equality hedge to the round-trip framing; brought the phase log current (phases 8/9/10a). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Restores concise, accurate //! headers (guarantee + limit) on the verified modules that the comment strip removed — notably the §2.2 hedge that the min-parens precedence tables are proved equal to each other (so the round-trip proves the parser inverts the printer, not that it implements SQL precedence; conformance rests on the cfg(test) differential + goldenscripts). Corrects verus-parser-roundtrip-plan.md: accurate trust-surface count (4 uninterp + 2 float axioms + 2 String axioms + external_body + ExDataType, not 'three assumptions'), removes the phantom display_f64, fixes the 'lexer runs verified' claim, brings the phase log current (8/9/10a). Comments + markdown only; verify.sh 668/0 and 329+5 tests unaffected. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Precedence conformance is not proven (the min-parens tables are proved equal to each other, not to SQL), so it rests on the differential. This enumerates the precedence relation EXHAUSTIVELY rather than sampling: every ordered pair (256), triple (4096) and quadruple (65,536) of the 16 binary operators, associativity chains, and all prefix/postfix x binary combinations — ~70,000 concrete expressions — each asserting the verified and legacy parsers build the identical AST or reject identically. All agree. Since precedence-climbing parses are determined by pairwise operator decisions, exhaustive pairwise agreement pins the tables to the legacy parser's. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

kiranandcode and others added 30 commits August 30, 2026 08:52

docs: record Phase 2.2 spec-roundtrip milestone in the plan

fb3f1ef

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs: record Brick 2 loop building blocks + the fuel-stability crux

85e7eb7

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs: Brick 2 suffix-mono + fuel-stability done; assembly plan (fuel …

0eabd52

…precondition) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs: mark Phase 2.2 (parse(print(e))==e) COMPLETE

c82e5be

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs: record Phase 3 start (parse_expr cut over; statement-path desig…

647d4e6

…n + risks) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs: statement-path expression cutover done; statement-structure cut…

a17a6cd

…over scoped Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

kiranandcode and others added 16 commits September 2, 2026 11:31

coverage allowlist: dated entry for phase 7's min_normalize_live

60bd1fa

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

coverage allowlist: dated entry for phase 6's stmt_min_roundtrip_live

fe2f54e

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

kiranandcode and others added 13 commits September 2, 2026 15:26

Navigation Menu

Uh oh!

verus: cut production SQL parser over to verified implementation - #18

verus: cut production SQL parser over to verified implementation#18
kiranandcode wants to merge 107 commits into
mainfrom
kg/verified-parser-cutover

kiranandcode commented Aug 30, 2026 •

edited

Loading

Uh oh!

yiyunliu commented Sep 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

kiranandcode commented Aug 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Review response (2026-08-31)

Assurance

Validation

Uh oh!

yiyunliu commented Sep 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

kiranandcode commented Aug 30, 2026 •

edited

Loading