Skip to content

Grammar sync tokens are an enumeration, not a predicate (unblocks the prepare_grammar memo for every language) - #8465

Merged
briansrls merged 9 commits into
mainfrom
session/deep-moth-771
Aug 19, 2026
Merged

briansrls merged 9 commits into
mainfrom
session/deep-moth-771

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 18, 2026 •

Copy link
Copy Markdown
Contributor

Grammar sync tokens were carried as Set<Symbol> — a PointwisePower characteristic function — to hold what every producer in the corpus writes as either nothing or a literal list of keyword classes. A characteristic function is a closure, and one closure anywhere in a value makes the whole value unhashable: the interpreter's content-hash walk has Value::Closure { .. } => EvalRecomputeStep::Bail, and both try_cross_claim_pure_memo and store_cross_claim_pure_memo return early when the key is None.

So prepare_grammar's cross-claim memo could never form its key, never store, and never hit — for every language in the corpus, not only .dag, because grammar_empty_sync_tokens() was Set { member: fn(_) { false } } too. A memo that exists and cannot fire is worse than none: it reads as solved.

What it cost

Measured remotely with claim_batch at a 900s budget, so rows run to completion instead of being interrupted at the 1552ms ceiling:

cost
parse a one-line module 12015ms
parse an empty module (header only) 11706ms
grammar construction 4ms
prepare_grammar ~11.7s of the total

97% of parsing a module was independent of the module being parsed.

The change

GrammarRoot.sync_tokens becomes List<Symbol>. Set is not redefined: std.types grounds Set<element> = PointwisePower<element>, and std.state_durability carries an explicit note that this is "not a license for a Map-as-set or bitset nickname". The characteristic function stays the meaning of a set. What changes is a field that was never a power set — it is six literal keywords.

Blast radius is two producers (grammar_empty_sync_tokens, dag_sync_tokens) and exactly one consumer (parse_sync_step, .member(...) → contains(...)). No call site anywhere needed an arbitrary predicate, so no coproduct-with-an-enumerated-arm is introduced — that would be a variant with no producer.

Receipts

Same instrument, same flags, one dispatch, so before/after are comparable.

Cross-claim memo — one process, one entry group, three consecutive claims:

claim before after
zz_prepare_grammar_only 14407ms 10018ms first claim still pays a full preparation
zz_prepare_then_parse 18815ms 165ms 114×
zz_full_parse_module 19298ms 166ms 116×

Within-claim dedup — dag_arrow_lambda_witness_test:

claim before after
witness_single_param_lambda_parses 12084ms 10527ms first row, pays the preparation
witness_sum_decl_unchanged 12231ms 170ms 72×
witness_pre_repair_grammar_restores_the_RED 50120ms 11276ms 4.4×

The last row deduplicates by content, not by call count, which is the behaviour we want: it builds a modified grammar (one production swapped), so its hash legitimately differs and it must pay a second preparation — exactly one, not four.

What this does NOT establish

  • The floor path is unproven. These receipts are claim_batch, which does not build the floor's per-module scopes. They show the cross-claim memo hits within one process; they do not show pointer stability across those scopes. The floor-side receipt is single_refinement_carrier_emits_no_unsupported_cast moving off its 45941ms on the next main run.
  • This does not retire the over-budget population. The first preparation still costs ~10s, so rows that pay it remain over the 1552ms ceiling. That residue is the cost-shape defect in grammar_has_left_recursion — 38 left-corner closures where one shared relation answers all 38, a fixed 38 rounds with no convergence check, and grammar_lookup_production filtering 38 productions to find 1 — deliberately left to its own PR under DESIGN §6, so the improvement here stays attributable. This PR removes the per-row multiplier; that one removes the constant.

Guarantee

Regression is prevented by construction rather than by a check: with the field typed List<Symbol>, a closure cannot be written there at all, so the memo cannot be silently re-killed the way it was.

gunbc-ci-auto-heal added 8 commits August 18, 2026 21:49
GrammarRoot.sync_tokens carried Set<Symbol>, i.e. a PointwisePower characteristic
function, to hold what every producer in the corpus writes as either nothing or a
literal list of keyword classes. That made the field a closure, and a closure makes
the whole grammar VALUE unhashable: the interpreter's content-hash walk bails on
Value::Closure, so prepare_grammar's cross-claim memo could never form its key,
never store and never hit -- for every language, not only .dag, because
grammar_empty_sync_tokens was a closure too.

Measured consequence before this change (remote, claim_batch, 900s budget so rows
complete instead of being interrupted): parsing an EMPTY module cost 11706ms and a
one-line module 12015ms, of which prepare_grammar was ~11.7s. Three consecutive
claims in ONE process each paid a full preparation.

std.types grounds Set<element> = PointwisePower<element>, so Set is NOT redefined
here: the characteristic function stays the meaning of a set. What changes is the
field, which was never a power set -- it is six literal keywords.
@gunbai-bot gunbai-bot Bot changed the title Main witnesses floor red: retire the budget_refused=102 + stale_quarantine=5 population (brief follows by message) Grammar sync tokens are an enumeration, not a predicate (unblocks the prepare_grammar memo for every language) Aug 18, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 18, 2026 23:11
@briansrls
briansrls merged commit 72676cf into main Aug 19, 2026
1 check passed
@briansrls
briansrls deleted the session/deep-moth-771 branch August 19, 2026 01:01
gunbai-bot Bot pushed a commit that referenced this pull request Aug 19, 2026
…rong

REQUEST_CHANGES on this PR was correct. v1_dead_witness_tree_triage_receipt_remainder
already ruled out widening the required floor's source roots to include src/v1,
and this PR did exactly that without reconciling against it. I missed the
receipt in the same file I reached into.

So I ran the experiment this PR already was. CI run 32219326621, srv1-04, floor
step 05:27:35Z-05:36:41Z.

THE OLD REASON NO LONGER REPRODUCES. The receipt says 'stalled 8+ minutes in
strict-preparation, RSS plateaued ~7.2GB, zero phase progress, killed'.
Preparation ran to COMPLETION in ~9 minutes and refused with 532 typed located
diagnostics. No stall, no kill. The cost objection went stale the night before:
#8465 unblocked the prepare_grammar memo for every language, #8487 replaced 38
left-corner closures with one converging relation, and a parse-bearing module's
first row went 10890ms -> 1106ms.

THE CONCLUSION SURVIVES ANYWAY, for a better reason. Zero of the 532 diagnostics
are in src/v1 -- 525 in src/v2, 7 in dag/test. The two trees share NO exact
module path but collide on the LAST SEGMENT twelve times: artifact, coercion,
common, compile, complexity, emit, infer, normalize, ownership, parse, resolve,
tokenize. v2.compiler.program_assembly calls tokenize at line 28 with no import
for it; that bare cross-module reference resolves today only by pool-membership
coincidence, and adding src/v1 supplies a second module whose last segment
matches. The reference stops resolving. That is the Class B failure DESIGN's
import-strip cascade thread names, reached from the opposite direction.

WHY THE CORRECTION MATTERS MORE THAN THE RULING. Under the old receipt the
dissolve-on is implicitly 'when the floor gets faster' -- so the next person to
land a preparation win retries this and hits 532 errors again. The corrected
receipt sets it on namespace-only resolution instead: bare cross-module
references binding by containment rather than by pool coincidence. Right
trigger, right lane.

The source-root change is REVERTED. This PR now carries only the receipt, and
the old measurement is retained beside the new one rather than overwritten.

Stated plainly in the receipt rather than left implicit: src/v1 has NO per-PR
gate on source validity until that lane lands, because compile-clean died with
the floor cut and regen is red by construction. #8519 is the specimen that
proved a parse error there is invisible.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 19, 2026
…on was wrong (#8520)

* Floor: fold compile_clean_source_roots so src/v1 is in the prepared subject

src/v1's .dag sources had NO per-PR coverage of their source validity. The
floor folded witness_layer_roots (= dag + src/v2), which is the corpus MINUS
the seed, so nothing on every-PR CI ever parsed src/v1/**.dag. A parse error
there was invisible, which is how one landed (#8519, fixed).

What DID cover v1 and no longer does:
  compile-clean  deleted with the 2026-08-15 floor cut
  regen          red by construction since the regen root cut (#8406)

v1's BEHAVIOR is covered -- 253 files under dag/test/claim reach it -- but
through host builtins against the compiled Rust seed, not by resolving v1 .dag
sources. Behavior tested, source validity not.

THE CHANGE IS ONE LINE AND MINTS NOTHING. gunbc.ci_layer_roots already defines
compile_clean_source_roots() = witness_layer_roots + [src/v1], the pool
authority meaning 'the corpus including the seed'. The emitter folds that
instead. Deliberately NOT adding src/v1 to witness_layer_roots: that list has
227 references and 13 witnesses pin its value (shard partition boundaries,
pre-push scope, doc-graph roots, lens grounding pools), so widening it would
move four unrelated subsystems' entry roots in one edit.

VERIFIED RATHER THAN ASSUMED that this actually parses the files:
prepare_repository_once builds its index over ALL source roots and pushes every
indexed module into the compiled subject, calling witness_file_from_source on
each. Pool membership IS subject membership on this path -- so src/v1 is parsed
and typechecked, and its witnesses enroll. I had assumed the opposite first.

RETIRES A SCAFFOLD. src/v1/stage0/src/bin/v1_src_dag_parse.rs is a registered
Scaffold whose dissolve-on reads 'when src/v1 .dag is parsed by the modeled
pipeline'. That is this change. It is also weaker than what it is replaced by:
it read src/v1/*.dag NON-recursively, missing 8 nested files including
src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag and its 7
witnesses, and nothing executed it -- it is built and shipped in the release
bin pack and invoked by no workflow. Its deletion is not bundled here; this
commit only makes it retirable.

Local probe on this tree: 46/46 top-level src/v1 .dag parse clean (#8519 is
already merged as e1da001). Whether typechecking src/v1 as part of the
prepared subject surfaces more is what this PR's CI answers.

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

* Re-measure the src/v1 RESTORE ruling: conclusion stands, reason was wrong

REQUEST_CHANGES on this PR was correct. v1_dead_witness_tree_triage_receipt_remainder
already ruled out widening the required floor's source roots to include src/v1,
and this PR did exactly that without reconciling against it. I missed the
receipt in the same file I reached into.

So I ran the experiment this PR already was. CI run 32219326621, srv1-04, floor
step 05:27:35Z-05:36:41Z.

THE OLD REASON NO LONGER REPRODUCES. The receipt says 'stalled 8+ minutes in
strict-preparation, RSS plateaued ~7.2GB, zero phase progress, killed'.
Preparation ran to COMPLETION in ~9 minutes and refused with 532 typed located
diagnostics. No stall, no kill. The cost objection went stale the night before:
#8465 unblocked the prepare_grammar memo for every language, #8487 replaced 38
left-corner closures with one converging relation, and a parse-bearing module's
first row went 10890ms -> 1106ms.

THE CONCLUSION SURVIVES ANYWAY, for a better reason. Zero of the 532 diagnostics
are in src/v1 -- 525 in src/v2, 7 in dag/test. The two trees share NO exact
module path but collide on the LAST SEGMENT twelve times: artifact, coercion,
common, compile, complexity, emit, infer, normalize, ownership, parse, resolve,
tokenize. v2.compiler.program_assembly calls tokenize at line 28 with no import
for it; that bare cross-module reference resolves today only by pool-membership
coincidence, and adding src/v1 supplies a second module whose last segment
matches. The reference stops resolving. That is the Class B failure DESIGN's
import-strip cascade thread names, reached from the opposite direction.

WHY THE CORRECTION MATTERS MORE THAN THE RULING. Under the old receipt the
dissolve-on is implicitly 'when the floor gets faster' -- so the next person to
land a preparation win retries this and hits 532 errors again. The corrected
receipt sets it on namespace-only resolution instead: bare cross-module
references binding by containment rather than by pool coincidence. Right
trigger, right lane.

The source-root change is REVERTED. This PR now carries only the receipt, and
the old measurement is retained beside the new one rather than overwritten.

Stated plainly in the receipt rather than left implicit: src/v1 has NO per-PR
gate on source validity until that lane lands, because compile-clean died with
the floor cut and regen is red by construction. #8519 is the specimen that
proved a parse error there is invisible.

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

* Correct the other two receipts carrying the same stale RESTORE mechanism

The APPROVE on this PR cited v1_dead_witness_tree_triage_receipt (line 928).
I had corrected v1_dead_witness_tree_triage_receipt_remainder (931). Checking
that discrepancy found the real defect: THREE receipts carry the RESTORE
ruling, and I had corrected one.

  929  v1_dead_witness_tree_triage_receipt                      stale
  931  v1_dead_witness_tree_triage_receipt_remainder            corrected
  933  v1_dead_witness_tree_triage_receipt_emitter_ambiguous..  stale

That is a partial sweep -- the failure I flagged twice today in other diffs and
then committed here. It took a reviewer's mis-citation to surface it.

Line 933 makes it worse than symmetry: it records that the stall was
'corroborated independently by smart-ram-730 via CI run 32196317824 on a
dedicated srv4 runner'. So a second session's measurement was also attached to
a mechanism that no longer reproduces, and the corrected receipt would have been
outvoted two-to-one by its own stale siblings.

FIXED BY CITATION, NOT DUPLICATION. The full corrected measurement stays in
_remainder alone. The other two now record three facts -- the stall does not
reproduce, the ruling stands on twelve last-segment module collisions, the
trigger is namespace-only resolution rather than a floor speedup -- and then
cite _remainder instead of restating it. One authority, two references. Both
original measurements are retained as the record of what was true then.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.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