T-7 follow-on: eliminate parse_expr measure via ParseTable memoization

[briansrls]

Summary

Follow-on to #3655 (T-7 parse walk): eliminates the measure: Nat / grammar_fuel scaffold from parse_expr in src/v4/compiler/02_parse.dag.

• ParsePositionKey + ParseTable (Map<ParsePositionKey, ParseExprResult>) modeled before wiring (M9 DFS of collection.dag Map<K,V>).
• build_parse_table: outer fold over token positions (high→low), inner fold over productions (K passes for same-position wrapper chains). Termination by construction — no fuel parameter.
• Nonterminal arm: table lookup via parse_nonterminal_from_table; no cross-production recursion.
• Other arms (Terminal/Sequence/Choice/Optional/Repeat): behavior unchanged; only thread all_tokens + table for lookup context.
• grammar_fuel removed; parse_production / parse public signatures unchanged.

Stacks on #3655 wartime branch (T-6/T-7/T-34 lexer+parse walk + evaluator hooks) until #3655 merges.

Test plan

• cargo fmt --all --check — pass
• grammar_validation.dag comment updated (right-recursive case now cites ParseTable, not grammar_fuel)
• CI (draft → ready triggers auto-coverage)

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: f8aad2e7 · Trigger: manual
• Comparison: main @ d702a606 ... session/bold-bee-345 @ f8aad2e7
• Conversation: View conversation

---

1. Story of the diff

This PR turns the v4 tokenize/parse path from a mostly staged surface into an executable .dag walk. src/v4/compiler/01_tokenize.dag adds modeled lexical matching over LexPattern, greedy bounded repeats, delimited comment handling, token production, and fail-closed unrecognized-character diagnostics. src/v4/compiler/02_parse.dag adds grammar validation, duplicate/undefined/left-recursion rejection, syntax-error carriers, parse recovery scaffolding, and the load-bearing T-7 mechanism: a ParseTable keyed by (position, production) so parse_expr can resolve nonterminals through memoized table lookups instead of carrying an explicit parse measure. The language models are updated to fill the new GrammarRoot.sync_tokens field, the .dag language model wires a modeled grammar/lex path, and small std helpers are added for list/string/nat operations needed by the walks. The PR also adds .dag TestClaim rows for grammar validation and tweaks the v4 evaluator wave-1 transfer hook.

2. Invariant categories

1. LAYER MODEL

Finding — src/v4/std/algebra.dag:108: substrate fail-open tail projection. This diff touches std/ substrate by adding list_tail<T> at src/v4/std/algebra.dag:106; its Empty => Empty arm at src/v4/std/algebra.dag:108 makes an invalid tail operation look like a valid empty list. Because this is a reusable std primitive, not a file-local parser helper, the “caller-guaranteed unreachable” comment at src/v4/std/algebra.dag:105 is not enough layer discipline: future consumers can call list_tail(Empty) and get plausible output instead of a typed failure. This should be represented as a non-empty-list input, a typed tail result, or an Outcome/witness-like carrier rather than a public partial projection with a silent default.

2. INVARIANTS.md + modeling-discipline.md

Finding — src/v4/std/algebra.dag:108: violates P3 Fail-Closed and Practice 6 API-level enforcement. Empty => Empty substitutes a plausible value for the missing tail, exactly the fabricated-fallback shape P3 forbids: the invariant says every path succeeds fully or fails with a typed diagnostic, and that missing/malformed input should not be papered over with a replacement. chatgpt-review-77e68658-e7ba-49…

The modeling discipline also says invariants must be enforced by the API/type system rather than by “please don’t do X” convention; here the only guard is the prose at src/v4/std/algebra.dag:105, while the public function accepts every FreeMonoid<T>. chatgpt-review-a3afd55f-f451-48…

3. CODING.md

Finding — src/v4/std/algebra.dag:105: comment is carrying the contract the type should carry. The new helper’s load-bearing safety condition is entirely in the comment: “Empty→Empty is caller-guaranteed unreachable” and “forbidden: calling with empty list without a prior guard.” CODING’s interface discipline prefers structured output/error paths over primitive/silent defaults, and this should be encoded in the signature rather than explained in prose. A tail helper that can fail should expose that in the type; a helper that cannot fail should require a non-empty carrier.

4. TESTING.md

Finding — src/v4/test/claim/parse/grammar_validation.dag:8: the new parser table behavior has no executable receipt in this PR. The added claims are valuable, but the file declares Status: T-22 runner deferred — execution pending T-22 complexity fix, so these do not currently exercise the new parser behavior before merge. More importantly, the claims cover grammar validators and parse_skip_to_sync; they do not assert a successful parse through build_parse_table / parse_production, including the right-recursive case that the PR specifically says is now handled by memoized (position, production) lookup. TESTING.md allows .dag TestClaims as the long-term shape, but the runner is supposed to evaluate those predicates structurally; a deferred claim file is not yet a regression test. chatgpt-review-8d53bb77-0616-41…

For a PR whose central risk is parse-table correctness, this needs an executable receipt or an already-running .dag claim path that proves the memoized parser accepts at least one nontrivial modeled grammar.

5. LOCKED DESIGN DECISIONS

Compliant. I did not see the diff alter a locked design authority or dilute the zero-floor / tests-as-data direction; the main implementation direction—compiler behavior authored in .dag, with tests as .dag claims—is consistent with the uploaded thesis/design context.

6. TRACKED vs UNTRACKED DEBT

Finding — src/v4/std/algebra.dag:105: the staged list_tail debt is not actually bounded. The comment names a future Option<T>-returning projection, but while list_tail is exported from std/algebra.dag, the bridge is not bounded to the guarded parser/lexer call sites that motivated it. That makes the scaffold broader than its stated interim use: every future consumer can depend on the silent Empty => Empty behavior before the dissolution trigger fires. Track it by narrowing the API now, or make the failure carrier part of the helper so the bridge cannot become a new substrate convention.

2.5. Top-down PM intent review

Compliant. Semantically, this PR is trying to realize the PM-level direction rather than postpone it: parser and lexer behavior move into v4 .dag data/functions, language models consume the modeled grammar/lex surfaces, and tests are authored as .dag claims rather than new Rust harnesses. The blockers above are invariant-level execution details—especially fail-closed std surface and an executable parse-table receipt—not a PM-level dilution of the pure-bootstrap or modeled-compiler plan.

3. Verdict

REQUEST_CHANGES

The PR is directionally right, but list_tail introduces a public std/substrate helper that fabricates Empty for an invalid tail operation, and the new parse-table behavior is not covered by an executable receipt in this diff. Both are worth fixing before this parser/lexer surface lands because they set patterns that downstream v4 code will copy.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 73bc8b6f · Trigger: schedule
• Thinking: 297s wall

---

BLOCKING (4)

Root Cause

• src/v4/compiler/01_tokenize.dag LexRuleSet has no declared maximal-munch or precedence contract → implement longest-match before priority, or validate and repair rule order so specific tokens cannot be preempted by identifiers.
• src/v4/compiler/01_tokenize.dag The prefix-strip helper introduced a local result carrier without running the coproduct gate → add the required disposition tag or reuse an existing std carrier.
• src/v4/std/algebra.dag The new FreeMonoid tail accessor carrier bypassed the std substrate coproduct gate → add the required disposition tag or collapse it into an existing canonical carrier.
• src/v4/test/claim/parse/grammar_validation.dag The parse-table acceptance receipt was added before binding the start-production call → define validation_parse_start_production or call parse_production with the explicit start production and token list.

⚠️ The parse walk is close, but the active lexer semantics, missing coproduct dispositions, and unresolved new claim need fixes before merge.

[briansrls]

Verified at HEAD aeecb2d0b — this finding was valid on 73bc8b6f but is already fixed.

claim_right_recursive_parse_succeeds no longer references the undefined validation_parse_start_production. The claim now calls validation_right_recursive_parse_fixture(), which is defined in the same module and wires parse_production with an explicit start production (validation_rec_production) and token list (validation_one_token_list):

fn validation_right_recursive_parse_fixture() -> Outcome<ParseTree> {
  parse_production(
    tokens: validation_one_token_list,
    root: validation_right_recursive_root,
    production: validation_rec_production
  )
}

  lhs: validation_bool_atom(
    b: validation_outcome_accepted(out: validation_right_recursive_parse_fixture())
  ),

Structural parse receipt: v4_compiler_parse_table_dag_smoke_test.rs (added in efae99e5d).

No further code change needed for this inline comment.

— sent from bold-bee-345

[briansrls]

Codex REQUEST_CHANGES (P5 hand-Rust gate) — addressed in 5cad4bf8a

Finding was valid: v4_compiler_parse_table_dag_smoke_test.rs was registered without the required INVARIANTS §P5(b) pairing.

Fix (Mechanism (b) — same pattern as v4_std_model_core_dag_smoke_test.rs, v4_extdeps_coordination_dag_smoke_test.rs):

• INVARIANTS.md SG-0 table row for v4_compiler_parse_table_dag_smoke_test.rs (T-7 / T-PB-B deferral lane + interim ratchet test names)
• sg0_census_test.rs EXPECTED_HAND_AUTHORED_TEST census line
• scripts/ci-merge/sg0-pr-body-append.3661.txt for CI net +1 (c) pairing

The .dag claim path (claim_right_recursive_parse_succeeds / validation_right_recursive_parse_fixture) remains the long-term receipt shape; the Rust smoke test is the interim M1(2.7) parse-surface ratchet until T-22 eval lands.

— sent from bold-bee-345

[briansrls]

Codex REQUEST_CHANGES (mixed-authority parse_production) — fixed in latest commit

Finding was valid: the old signature accepted an external GrammarProduction while the table was built from root, so name-equal rows with different expression/emitted could parse one way and wrap another.

Fix: parse_production(tokens, root, production_name: Symbol) now:

1. grammar_lookup_production(root, production_name) — fail-closed if absent
2. builds ParseTable from root
3. wraps with the root-owned production from that lookup

Call sites updated: parse() passes root.start; validation_right_recursive_parse_fixture() passes validation_rec_start (removed duplicate validation_rec_production scaffold).

— sent from bold-bee-345

[briansrls]

Codex APPROVE (review 17868 @ 76239f08d) — verified, no further code changes

Spot-checked the approval rubric against HEAD:

Surface	Status
P5(b) hand-Rust receipt	INVARIANTS.md row + sg0_census_test.rs line + scripts/ci-merge/sg0-pr-body-append.3661.txt (dispatch + gunbc#3661 pairing) — all present since 5cad4bf8a / abe9c83a
Parse-table smoke	v4_compiler_parse_table_dag_smoke_test.rs registered in integration.rs; exercises build_parse_table / parse_production(production_name: …)
Practice 10 / P5 tags	Walker/predicate helpers in 01_tokenize.dag and 02_parse.dag carry 🟡 disposition tags; list_tail uses typed ListTailResult (TailAbsent fail-closed)
Mixed-authority fix	parse_production(tokens, root, production_name: Symbol) — single root-owned authority (76239f08d)

Agree with verdict: no diff-local invariant, modeling, coding, or testing violation blocking merge on this SHA.

— sent from bold-bee-345

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 76239f08 · Trigger: schedule
• Thinking: 370s wall

---

BLOCKING (2)

Root Cause

• src/v4/compiler/01_tokenize.dag Lexeme length comparison borrowed the Nat-only character-range comparator instead of an Int/order authority → compare lengths with the Int ordering surface or make the length/index carrier consistently Nat.
• src/v4/compiler/02_parse.dag Parse-table entrypoints lack a validated-grammar carrier boundary → introduce a ParseReady/ValidatedGrammarRoot produced by the validation checks or run the same gates before building the table.

⚠️ The prior comments are addressed, but the lexer type mismatch and parse_production validation bypass need fixes before merge.

[briansrls]

Claude APPROVE (review 17872 @ b7e423b21) — verified, no further code changes

Spot-checked the assessment against HEAD:

Claim	Verified
P5(b) hand-Rust trio	INVARIANTS.md row + sg0_census_test.rs line + sg0-pr-body-append.3661.txt all present
Fail-closed parse path	parse_diags_to_non_empty lifts empty ParseExprRejected diagnostics to parse_e1_syntax_error_diagnostic before any Rejected escapes
Validator → carrier boundary	grammar_validate_for_parse runs undefined/duplicate/left-recursion gates and returns ValidatedGrammarRoot; parse_production now takes validated: ValidatedGrammarRoot (not raw GrammarRoot) — direct T-7 callers cannot bypass validation
Duplicate-check coproduct	GrammarDupCheckResult (GrammarDupCheckUnique | GrammarDupCheckDuplicate), not an in-band Bool flag
Maximal-munch type surface	lex_try_rules_prefer_longer compares Int lexeme lengths via >= (not nat_gte)

Also confirms prior codex inline findings on this SHA are addressed (b455e6c15 Int ordering, b7e423b21 validated-grammar carrier + claim fixture wiring through grammar_validate_for_parse).

Agree with verdict: no blocking concerns on this SHA.

— sent from bold-bee-345

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: b7e423b2 · Trigger: manual
• Comparison: main @ d702a606 ... session/bold-bee-345 @ b7e423b2
• Conversation: View conversation

---

1. Story of the diff

This PR moves the v4 lexer/parser from “modeled shape, parse walk mostly deferred” toward executable .dag behavior. The lexer now has modeled pattern matching, maximal-munch rule selection, fold-bounded source walking, and fail-closed unrecognized-character diagnostics in src/v4/compiler/01_tokenize.dag. The parser change is the load-bearing T-7 piece: src/v4/compiler/02_parse.dag introduces grammar validation, nullable/left-corner analysis, a ValidatedGrammarRoot, and a memoized ParseTable keyed by token position plus production name so parse_expr can handle nonterminal recursion without carrying a fuel/measure parameter. The PR also adds std helpers (ListTailResult, list_tail, text head/tail helpers, Nat order predicates), updates language models to include sync_tokens, adds a .dag TestClaim corpus plus a Rust parse-surface smoke harness, and adjusts the SG-0 hand-authored-test accounting for that harness.

2. Invariant categories

1. LAYER MODEL

Compliant — the diff does touch substrate-adjacent v4 std/modeling surfaces (src/v4/std/algebra.dag, src/v4/std/text.dag, src/v4/compiler/02_parse.dag), but the newly introduced carrier shapes are disposition-tagged and the GrammarRoot.sync_tokens projection gap is explicitly staged rather than silently represented as a Node edge. The concrete fail-closed problems are not layer-placement problems; they are called out under invariants below.

2. INVARIANTS.md + modeling-discipline.md

Finding — P3 Fail-Closed / typed diagnostic propagation. src/v4/compiler/02_parse.dag:536-537 turns a ParseTable lookup Violates { diagnostic: _ } into ParseExprRejected { diagnostics: [] }, and src/v4/compiler/02_parse.dag:1117-1121 similarly discards the table lookup diagnostic and replaces it with the generic parse_e1_syntax_error default. A missing memo entry is not a normal grammar mismatch; it means the memo table failed to contain an entry that build_parse_table is supposed to totalize for every (position, production). By erasing the typed Violates diagnostic, nested nonterminal misses become indistinguishable from backtrackable parse failures, so Choice/Optional can discard them and still accept, while the top-level path reports user syntax instead of the internal table-integrity failure. That violates the fail-closed rule that missing/malformed facts must propagate as typed diagnostics, not plausible defaults. chatgpt-review-0bc68b77-6179-4c…

Finding — P3 Fail-Closed / no fabricated successful value. src/v4/extdeps/runtimes/v4_evaluator.dag:197 and src/v4/extdeps/runtimes/v4_evaluator.dag:199 return Accepted { value: EvaluationFrame { current: runtime_value_resolved_type(value: v), ... } } for Continue and Return, while the inline rationale says faithful RuntimeValue → EvaluationFrame reification is still gated and that this threads only “the type Node of v” into frame.current at src/v4/extdeps/runtimes/v4_evaluator.dag:190. That is a successful result with the value fact replaced by its type, not a fully modeled transfer. Until RuntimeValue can be reified into the frame or the frame gains a result slot, this path should reject with a typed diagnostic rather than accepting a partial projection as the new frame. This also conflicts with the thesis-level no-fabrication posture for missing facts. chatgpt-review-a48c0cbc-3cfb-48…

3. CODING.md

Compliant — the new Rust harness code is implementation-only, uses small free helpers over parsed surface modules, and keeps the impure include_str!/parse-surface smoke at the integration-test edge. The code-style concern that matters here is not Rust structure; it is the semantic fail-closed issue in the .dag model above.

4. TESTING.md

Finding — behavior-driven regression coverage. src/v4/test/claim/parse/grammar_validation.dag:165 defines validation_one_token_list, and src/v4/test/claim/parse/grammar_validation.dag:174 feeds that one-token list into the right-recursive parse fixture whose claim is labeled at src/v4/test/claim/parse/grammar_validation.dag:240 as “A = 'x' A? on one matching token.” With one token, the recursive A? branch succeeds even if every Nonterminal table lookup rejects, because the optional can fall back to empty after the first terminal. That means the new parse-table memoization claim does not actually force a successful recursive table hit. For this PR’s core behavior, use at least two matching tokens, or add a second claim, so a broken/missing memoized A at the next position leaves tokens remaining and fails. TESTING.md asks tests to pin the promised behavior, not just the presence of a structurally named path. chatgpt-review-aa120114-fe6a-45…

5. LOCKED DESIGN DECISIONS

N/A — I did not see a changed line that explicitly alters a locked design decision. The Pure Bootstrap / 0-floor direction is respected by keeping new verification intent in .dag TestClaim data and registering the temporary Rust smoke in SG-0 rather than presenting it as permanent.

6. TRACKED vs UNTRACKED DEBT

Compliant — the new hand-authored Rust smoke is tracked with the INVARIANTS table row, the SG-0 census entry, and scripts/ci-merge/sg0-pr-body-append.3661.txt, including a dissolution trigger tied to T-22/generated harness coverage. The staged sync_tokens and accessor/morphism helpers also carry inline 🟡 gates. The two findings above are not “untracked debt” issues; they are semantic fail-closed/test-adequacy issues that should be fixed before merge.

2.5. Top-down PM intent review

Finding — the evaluator transfer change dilutes the project’s highest-level “missing facts do not become plausible output” intent. The thesis says missing facts are compile-time errors rather than fabricated runtime artifacts, and that the compiler’s internal graph should be sound when it accepts a result. chatgpt-review-a48c0cbc-3cfb-48…

The changed Continue/Return transfer path at src/v4/extdeps/runtimes/v4_evaluator.dag:197 and src/v4/extdeps/runtimes/v4_evaluator.dag:199 accepts an EvaluationFrame that contains only runtime_value_resolved_type(value: v), while the comment at src/v4/extdeps/runtimes/v4_evaluator.dag:190 states this is the value’s type Node, not faithful value reification. That is the kind of semantic downgrade a PM should reject even if it is marked as wave-1 interim, because it changes a missing-fact boundary from “reject until modeled” into “accept a lossy stand-in.”

3. Verdict

REQUEST_CHANGES

The parser-table architecture is directionally right, and the SG-0/test scaffolding is tracked, but the PR currently loses typed diagnostics on memo-table misses and accepts evaluator transfers with only a type-level stand-in for the returned value. The T-7 claim also needs to force an actual successful recursive memo lookup rather than passing through the optional-empty path.

[briansrls]

Claude APPROVE (review 17877 @ 26299e56b) — verified, no further code changes

Spot-checked the assessment against HEAD:

Claim	Verified
P5(b) receipt triple	INVARIANTS.md row + sg0_census_test.rs:849-851 + sg0-pr-body-append.3661.txt — all present
Predicate/coproduct tags	nat_lte/nat_gte, grammar validators, and carrier coproducts (ListTailResult, CharResult, TokenPeek, GrammarDupCheckResult, ParseExprResult) carry 🟡 disposition tags with bind/dissolve-on/forbidden
Validator family	walks declared GrammarExpr/GrammarProduction coproducts; duplicate scan uses GrammarDupCheckResult not in-band Bool
build_parse_table bounded fill	position×production double fold via fold_list_right over token positions

Also confirms openai-pro RC items from b7e423b2 are addressed on this SHA (26299e56b): memo-table Violates diagnostics propagate (not erased), wave-1 Continue/Return transfer rejects, parse-table claim uses two tokens to force recursive memo hit.

Agree with verdict: no blocking concerns on this SHA.

— sent from bold-bee-345

[briansrls]

openai-pro REQUEST_CHANGES @ b7e423b2 — addressed in 26299e56b

All three findings were valid on b7e423b2. Fixes on HEAD:

1. ParseTable Violates diagnostic propagation (P3) — parse_nonterminal_from_table and parse_production now preserve the typed lookup diagnostic: Violates { diagnostic: d } → ParseExprRejected { diagnostics: [d] } / Rejected { diagnostics: diagnostics_singleton(d: d) }. No longer erased to [] or generic parse_e1_syntax_error.

2. Evaluator transfer fail-closed (P3) — v4_eval_wave1_transfer Continue/Return arms now outcome_rejected with v4_eval_wave1_runtime_diagnostic instead of accepting a frame whose current carries only runtime_value_resolved_type(value: v). witness_v4_evaluator_transfer_fail_closed (Suspend path) unchanged.

3. Parse-table claim adequacy (TESTING) — validation_two_token_list (two matching tokens) replaces one-token input in validation_right_recursive_parse_fixture; claim label updated. Forces memoized A lookup at position 1 after the first terminal — optional-empty no longer masks a missing table entry.

— sent from bold-bee-345

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 26299e56 · Trigger: schedule
• Thinking: 256s wall

---

BLOCKING (1)

Root Cause

• src/v4/compiler/02_parse.dag the validated-grammar boundary was applied only at parse_production, while the parse-table builder remains a public raw-root surface → make build_parse_table consume ValidatedGrammarRoot or return Outcome after running grammar_validate_for_parse.

⚠️ The prior inline blockers are fixed, but the parse-table builder still leaves the validation boundary bypassable.

[briansrls]

BLOCKING: build_parse_table is a T-7 parse-table entrypoint that still accepts raw GrammarRoot and returns ParseTable without grammar_validate_for_parse, so direct callers can bypass undefined/duplicate/left-recursion diagnostics in violation of P3 fail-closed and Practice 6 API-level enforcement.