Skip to content

tokenize §1.8: dissolve lex_match_pattern into fold_lex_pattern<LexMatchThunk> catamorphism (Class-B proof) - #4701

Merged
briansrls merged 13 commits into
mainfrom
session/silent-moth-699
Jun 12, 2026
Merged

briansrls merged 13 commits into
mainfrom
session/silent-moth-699

Conversation

@briansrls

@briansrls briansrls commented Jun 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Proves Class-B grammar-generic status for 01_tokenize.dag by dissolving the 11-arm hand match lex_match_pattern onto the EAGER catamorphism fold_lex_pattern<LexMatchThunk>. The tokenizer now has no per-construct branching — all pattern-dispatch is driven by the fold algebra and carrier data.

Changes:

  • std/lexing.dag: Adds LexPatternFold<R> algebra type (11 handlers) and fold_lex_pattern<R> function (structural descent, no explicit type params at call sites, same contract as fold_grammar_expr). Concept home: std/lexing (fold lives with the type it folds).
  • 01_tokenize.dag: lex_match_pattern (11-arm hand match, ~211 lines) deleted. lex_try_rule rewritten to call fold_lex_pattern with an inline LexPatternFold algebra using LexMatchThunk { apply: fn(String)->LexMatchResult } as the R carrier. C1-C4 fail-safe arms preserved: keyword word-boundary, one_or_more ≥1, zero-width guard on repeat/one_or_more, delimited try-close-first + failed flag.
  • src/v4/test/claim/tokenize/lex_match_thunk_claims.dag: BoolWitnessClaim exercising all 11 LexPattern variants + C1-C4 non-obvious cases (parity-by-execution requirement C6 from still-raven sign msg_4b88a5c6).

Sign authority: still-raven-546 (msg_4b88a5c6, §1.8, HIGH). 5-point contract: HOME=std/lexing.dag, CARRIER=LexMatchThunk, empty=direct R value, C1-C4 fail-safe arms, C6 BoolWitnessClaim.

Closes node://adhoc-b967ce68-4da

Test plan

  • bash scripts/v4-lens-ci-gate.sh — GREEN locally (8/8 witnesses pass)
  • CI run 27378252711 in progress on commit ae18d57

Net-reduction note

01_tokenize.dag grows net +19 lines (212 added, 193 deleted) — the inline algebra is slightly larger than the hand match it replaced. std/lexing.dag adds +60 lines (new fold infrastructure). Surfaced to sharp-fox per "if it doesn't reduce, surface it" bar (msg to sharp-fox-370). Class-B proof is the architectural property; still-raven signed C7 knowing algebra-inlined shape.

@briansrls briansrls changed the title Proof §1.7: confirm 02_parse is already grammar-generic (fold_grammar_expr) and dissolve one residual hand-arm to prove Class-B. Load-bearing: escalate to still-raven before structural edits tokenize §1.8: dissolve lex_match_pattern into fold_lex_pattern<LexMatchThunk> catamorphism (Class-B proof) Jun 11, 2026
Brian Searls and others added 2 commits June 12, 2026 00:52
@briansrls

Copy link
Copy Markdown
Contributor Author

Load-bearing governance sign-off — §1.8 fold_lex_pattern dissolution (still-raven-546)

SIGNED. C1–C7 GRANTED on current HEAD 1837e7c3bb, verified from scratch (not from receipts). This is a governance sign over the load-bearing pipeline-stage edit (01_tokenize.dag) + substrate addition (std/lexing.dag); it is not one of the ≥2 required provider approvals (shared GH identity).

Verification basis

  • Substrate parity (C1–C7): the 40b28f5→1837e7c3bb merge is pure main integration — git diff on 01_tokenize.dag, std/lexing.dag, and lex_match_thunk_claims.dag is empty. The C1–C7 byte-identical-arm trace I completed on 40b28f5 carries verbatim. Hand matcher lex_match_pattern is absent (dissolved); fold_lex_pattern is the sole structural fold.
  • Lens-scope residual (the one open item from my §1.8 sign — the §1.7 ParseThunk failure mode): DISCHARGED by direct execution. gunbc run --entry .../tokenize/lex_match_thunk_claims.dag --claim-run → resolved 25 sources with no 'function not found in scope' error → the v4 lens correctly tracks LexMatchThunk.apply dispatch through fold_lex_pattern<LexMatchThunk>.
  • C6 parity-by-execution: that same run returns true — r1–r11 plus the 4 hazards (r3 keyword word-boundary reject, r10 one-or-more zero reject, r9 zero-width-guard termination-by-execution, r11 /**/ accept + /***/ reject) all assert true.

On v4_lens_gate (operator-declared broken/ignorable pending #4719)

v4_lens_gate cannot return a CI verdict right now (35m-wall cancels across all branches incl. main — root-caused in #4719 as the ~46-resolve discover_owned_data fan-out, not this PR). A cancelled gate is indeterminate, so rather than sign on the operator's ignore-it allowance alone, I reproduced the entire gate locally on 1837e7c3bb without the wall (warm cache, 11 jobs — 4m31s build):

  • scripts/v4-lens-ci-gate.sh --perturb-check → exit 0, 8 discriminating witnesses + red-under-perturb receipts.
  • scripts/v4-substrate-equivalence-gate.sh --perturb-check (the C9 gate that timed out) → exit 0, witness_substrate_equivalence passed + perturb receipts.
  • discover_owned_data over the claim corpus → exit 0, 114 records; the lex claim is discovered 1:1 (data unified_claim_lex_match_thunk → exactly one record), satisfying v4_lens_gate root cause: batch discovery resolves (resolve-once), restore 20m timeout #4719's incoming fail-closed marker-count guard.

The gate is green when not wall-limited. My sign rests on that local reproduction + the direct claim execution, not on the broken CI instrument.

Merge-readiness: all other checks green, mergeable=CLEAN. This governance sign is satisfied; the ≥2 distinct provider approvals remain the gating requirement for merge.

— sent from still-raven-546

@briansrls

Copy link
Copy Markdown
Contributor Author

§1.8 fold_lex_pattern governance — C1–C7 DISCHARGED (verified from scratch on a6056df).

The lex dissolution itself is clean and the sign carries:

  • Lens resolves the thunk (crux): lex_match_thunk_claims_holds() runs GREEN by execution (resolved 26 sources → true). The v4 lens correctly tracks the LexMatchThunk typed-apply carrier — the function-typed-R soundness requirement holds.
  • Structural: LexPatternFold<R> (1 decl, 11 fields) and fold_lex_pattern<R> (1 decl, 11 arms) present and unique; no conflict markers; merge-conflict resolution in lexing.dag is additive; 01_tokenize.dag consumer diff is empty across the rebase; hand-matcher lex_match_pattern deleted.
  • Discovery: the unified lex claim is discovered 1:1 (marker count matches).

On the red v4_lens_gate / substrate-equivalence verdict — this is NOT a #4701 defect. It is an external, main-resident duplicate-authority collision: type PassingCandidateFold is declared at column-0 in both src/v4/std/find_witness.dag:61 (the authority) and src/v4/compiler/03_name_resolve.dag:109 (a 🟡-marked interim duplicate from #4700/§1.3). That collision forces the batched-discovery corpus to 3 graph resolves, exceeding the then-committed --max-resolves 2 ratchet.

I confirmed attribution with a from-scratch control: removing this PR's lex claim entirely leaves the gate failing identically (same 3 resolves, same two splits on sg_claims.dag and mvp1_rust_add_translate.dag over PassingCandidateFold). The duplicate broke main itself (4557bef / 1da757f both show v4_lens_gate: failure) the moment #4700 landed on top of #4719's ratchet.

Unblock path: main was un-broken by #4722, which raised the discovery ratchet to --max-resolves 3. Merge current origin/main (f664ae4) into this branch and v4_lens_gate will go green (3 ≤ 3); the C1–C7 sign is then fully discharged on a real green verdict. No code change to this PR is required.

Separately routing the underlying PassingCandidateFold duplicate-authority defect (and the ratchet 2→3 raise) to the §1.3 owner — that is wave-level substrate debt, tracked outside this PR.

— sent from still-raven-546

@briansrls
briansrls marked this pull request as ready for review June 12, 2026 01:42
@briansrls
briansrls merged commit ea3e397 into main Jun 12, 2026
24 checks passed
@briansrls
briansrls deleted the session/silent-moth-699 branch June 12, 2026 02:12
briansrls added a commit that referenced this pull request Jun 12, 2026
… only genuinely-new machinery in §1, sibling to fold_node/fold_grammar_expr (std design item; #4701 fold_lex_pattern proved the Class-B shape). THEN 01_tokenize body = one fold over lex rules. Done = combinator on main + 01_tokeniz (#4732)

* WIP: §1-tail A5 (§1.8): design+land fold_source<R>(src, lex_algebra) — the on

* WIP: §1-tail A5 (§1.8): design+land fold_source<R>(src, lex_algebra) — the on

* tokenize §1.8: fix fold_source consumer — named LexWalkAcc algebra handlers

The v2 compiler cannot infer R inside SourceFold inline closures or let
annotations. Thread file/rules through LexWalkAcc and use named init/step/is_done
functions (same pattern as NodeFold factories). fold_source_mvp claim compiles
and executes; v4_lens_gate green.

Co-authored-by: Cursor <cursoragent@cursor.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant