Repository navigation
Conversation
… + claim-bin cwd fix Reworked to drop the forked complexity machinery. The cost-shape lowering (dag_surface_lower_*) was a second, hand-rolled body producer running beside the compiler's own — a §3/§4 fork: it re-lowered the surface parse tree by hand (one if-arm per production), skipping resolve + normalize + body_producer, and produced a shape that matched neither the real inferred tree nor its own synthetic test subjects. It caught zero real quadratics and generated a cascade of point-fixes (per-form lowering lanes, a lexeme-recovery module, a GeneratedArtifact name collision, missing Branch-descent). All of it is backed out. The general body producer that would replace it — §4's "one grammar read in both directions" (row-driven ingest, the inverse of the row-driven emitter), which also subsumes the pre-existing MVP1 03_body_producer — is left as compiler work, not landed as a fork. Kept: the genuinely fork-free, DESIGN-clean behavioral changes. - 04_infer gains the Loop arm: an iteration-fold body is typed as a per-iteration transform (τ → τ under the measure); divergent and refinement-shaped bodies refuse with the located infer_loop_iteration_type_mismatch. - Measure-derived loop termination (loop_multiplicity over the cited measure_descent_fact_registry, lattice meet + lexicographic strict-dimension proof), grounded on the dag/std/termination.dag single authority. - claim_batch / claim_executor resolve relative path args against the process cwd and refuse (exit 2, located) on missing paths — closes the baked-root mixed-tree fail-open. Verified by execution against the merged base: 8 loop-multiplicity + 5 loop-infer witnesses PASS; roster-shape, generated-artifact drift, and enforcement-consistency + repo-wide-complexity meta-gates PASS. The two new loop tests are CI-enrolled so the kept behavior gates. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
…slice The first real piece of the general body producer that replaces the removed cost-shape fork (and, eventually, the hand-rolled MVP1 loop shapes). A surface fold has no dedicated grammar production — it parses as an ordinary call — so its lowering is a SEMANTIC desugaring keyed on the RESOLVED callee identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. Given a resolved fold call (positional children [callee, collection, init, iteration_body]), fold_call_to_loop lifts the iteration body into the canonical seam Loop bounded by the registered fold-iteration measure, and the kept loop_multiplicity derives PROVEN termination from it — the same real derivation the foundation's loop witnesses use, now reached from a fold-call shape. This pins the seam (M1) and lands the desugaring unit (core of M2), verified by execution: fold_call_lowers_to_terminating_loop (proven termination) + short_fold_call_refuses_no_loop_fabricated (fail-closed red control). It is deliberately resolve-agnostic — it consumes an already-resolved fold-call node — so it is the same desugaring the whole-tree body producer will run on real resolved fold calls once corpus resolution is affordable. Remaining toward catching real quadratics: wire this to real resolved corpus source (M2 full), corpus-scale resolution affordability (M4), re-key the accumulator-copy rule to the seam Loop shape (M3). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
…en class Foundational name-resolution fix. dag_grammar_primary_expr_core stamped the general expression ident head with StampClass, so a general call's callee came out as ^dag_token_ident — the NAME dropped at parse. That made every operation (fold, contains, list_append, ...) unidentifiable in real code and left resolution nothing to bind: a self-inconsistency in the grammar, since qualified names (dag_grammar_qualified_name_expr) already StampLexeme. Switch that one terminal to dag_grammar_terminal_lexeme, identical to how qualified names already carry their name. Now a general call carries its callee name, resolution can bind it (resolve_atom looks up the identity in scope), and consumers read the canonical identity the homogeneous way the R1 lens already does (r1_symbol_of = atom.identity, matched against a symbol-keyed registry). This is the existing identification path, not a new mechanism — and NOT the removed fork's post-hoc lexeme-recovery hack (StampLexeme preserves the name AT parse; the hack recovered it from the token stream after the fact). This unblocks operation-identification in real code — the prerequisite for the complexity feature (and general name resolution broadly). v2 is not in production, so this is the right window for the change. Verified: all 4 v2 language parse tests pass; the whole-tree compile-clean gate, emit-host, source-root-ingest, and self-host gates pass (the content-hash ripple is contained); parse floor witness green (parse perf witness runs the v1 parser, unaffected — a transient timing FAIL re-ran green). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
First check on real source that the StampLexeme grammar fix does its job: a real fold snippet ingested through the census path (tokenize -> parse_module -> normalize, v2.lens.enforcement.cost_coverage) yields a tree in which ^fold (the callee) and ^xs (the collection) appear as atom identities — the names survive, so operation recognition is now possible the homogeneous way the R1 lens reads atom.identity. fold_callee_name_survives_parse is the RED control the pre-fix StampClass regression breaks. CI-enrolled. Grounding note recorded for the next slice: the fold call is NOT shaped as a head-positional callee (that probe failed); it carries the surface call production structure, so the desugaring will navigate it homogeneously via parse_subtree_find_production_captured (the same helper cost_coverage already uses to locate fn bodies) to extract the fn-literal iteration body, then desugar via v2.compiler.fold_lowering. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
Correct fold_call_to_loop to consume the actual surface fold-call subtree
(the primary_expr captured child) rather than a guessed
ComputationNode-with-positional-children shape whose index-3 body slot was
wrong for real folds (fold's iteration body is a NAMED fn-literal arg, not
positional[3]).
The desugaring now identifies the call homogeneously:
- fold_call_head_symbol reads the sequence-left head projection (the callee
^fold), the same way the qualified-name parser reads sequence heads;
- fold_call_iteration_body locates the sole ^dag_surface_fn_literal argument
and lifts its ^dag_surface_fn_body, the same way cost_coverage locates fn
bodies (parse_subtree_find_production_captured).
Keyed on the callee identity (DESIGN §4: fold/recursion is sugar over Loop),
never a lexeme scan. Fail-closed twice: a call whose head is not ^fold
refuses (^fold_lowering_not_a_fold_call); a fold call carrying no fn-literal
iteration body refuses (^fold_lowering_shape_invalid) — never fabricates a
loop.
Verified end-to-end on real source through the census ingest
(tokenize -> parse_module -> normalize): fold(xs, init: 0, f: fn(acc, x) { acc })
lowers to the canonical seam Loop and loop_multiplicity derives PROVEN
termination from the fold-iteration measure. Both fail-closed arms proven
discriminating by perturbation (each red control flips to FAIL when its arm
is defeated).
Consolidate the two probe test files into one end-to-end witness
(fold_lowering_test), folding in the StampLexeme survival checks (^fold/^xs
survive parse) as the grammar red control; drop the now-redundant
fold_real_source_test and update the CI witness roster.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
…l quadratic
Deliver the accumulator-copy lens's first real-source consumer: a surface
projection that reads a parsed fold call and builds R1's fold-step subject
(Instantiation[acc_binder, combiner, call[port0, port1]]), so R1 catches a
real quadratic end-to-end instead of only judging synthetic fixtures.
This is the peer projection of M2's fold_call_to_loop (DESIGN §2 Realization:
one surface fold call, N consumers — the loop projection is for termination,
this one for cost/copy-detection). Both read the SAME located fold call
through the SAME fn-literal locator, now factored out as
v2.compiler.fold_lowering.fold_call_step_fn (§3 single authority for "where
the step function is").
Foundational grammar fix: fn-literal parameters were stamped as the token
class (^dag_token_ident), dropping their names — the same StampLexeme drop
already fixed for call heads. Verified by execution: an unused param vanished
before the fix, survives after. R1 needs the accumulator's name (param 0) to
check whether it lands in the combiner's copied port, so the name must
survive parse.
The distiller (v2.lens.complexity_r1_accumulator_copy.surface_subject) reads
four symbols at the surface/lexeme level: acc_binder = step-fn param 0;
combiner = the head of the call in the step-fn body; port0/port1 = that
call's first two argument values in declared order. Fail-closed at every
step: no step fn / no first param / body not a two-argument call / an
argument not a bare name all REFUSE with a located diagnostic — never
fabricate a subject a fold R1 cannot read as clean.
Proven end-to-end on real source (v2.test.claim.complexity.r1_surface_subject),
through the census ingest: fold(..., fn(acc, x) { list_append(left: acc,
right: x) }) projects Poly(2); the SAME combiner with the accumulator flipped
to the non-copied port (list_append(left: x, right: acc)) is clean —
isolating the copied-port check as the sole difference; an identity-body fold
refuses. Discrimination proven by perturbation: a bogus acc_binder flips the
quadratic to clean (acc_binder is read independently, not circularly).
Surface-level because corpus resolution/body-production is not yet
affordable; a resolved-body read supersedes this once it is, with the seam
(fold_call_step_fn) unchanged. Whole-corpus enrollment (sweep every fold, not
these snippets) remains future work. Full CI floor green (4 batches, 30
witnesses).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
…e refusals
Following the methodology "run the model on the real system and let where it
comes back lacking be the signal it's not done" — challenged the M3 distiller
against the actual corpus suspect shape (src/v2/workflow/glob_discovery_law.dag),
not the textbook snippet the M3 tests were written around.
Finding (verified by execution): the distiller MISSES the real quadratic. The
real suspect is fold_list with the copying list_append(left: acc, right: Cons{..})
buried inside an if-branch and a struct-literal grow-by-one arg. The distiller
reads only "the first call in the step body" — which is the if-CONDITION, a
one-argument call — so it reads the branch condition as the combiner and refuses
(cause: port1_opaque) rather than looking inside the branch. Corpus scale for
context: ~676 fold + ~413 fold_list + ~37 fold_node calls; the textbook direct-
combiner-body shape the distiller handles is the minority.
Captured as a committed coverage-boundary witness
(real_branch_body_quadratic_is_currently_missed): a RED that flips to FAIL the
moment the distiller learns to traverse branches — the flip is the dissolution
trigger to widen it into a positive catch. This is the honest "green on the
textbook shape, not done on real code" marker.
Made the distiller's refusals per-cause (FoldSurfaceRead classification →
no_step_fn / no_accumulator_param / body_not_located / body_head_opaque /
port0_opaque / port1_opaque), so the gap is a typed, located, legible fact
rather than one opaque shape-invalid (DESIGN §5: a refusal must be a typed,
located diagnostic). fold_call_to_r1_subject's public Outcome contract is
unchanged; the M3 tests pass unchanged.
Note: a whole-corpus quantified sweep of the distiller hits the same
affordability wall as M4 (per-file ingest + O(folds×subtree) walks), so
quantifying at scale waits on that infra; the qualitative finding here is
decisive on its own. Full CI floor green (4 batches, 31 witnesses).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
Replace the 230-line surface-navigation distiller (surface_subject.dag) and the bespoke r1_fold_step_subject intermediate with a single linear fold, so the lens is stage1→stage2→… with each stage consuming the previous stage's natural type (a Node), no adapter. Two halves, cleanly split: - COST MODEL (complexity_r1_accumulator_copy.dag) — navigation-free. Owns the copied-port registry lookup and classify_call(at, combiner, port_syms, carriers) → Optional<Finding>. Finding = Poly2Suspect | AnalysisOpaque. - TRAVERSAL (complexity_r1_accumulator_copy/analyze.dag) — the fold. analyze(node, carriers) recurses over the whole tree threading the carrier environment down: at a fold-family call it binds the step-fn's accumulator; at every combiner call it asks classify_call. Because the fold VISITS every node instead of doing targeted "first call in the body" lookup, a copy inside an if/match/let is found by construction. The real glob_discovery_law shape (fold_list, copying list_append(left: acc, ...) inside an if-branch, grow-by-one struct arg) that the bridge MISSED is now CAUGHT — the old coverage-boundary witness flipped from "currently missed" to real_branch_body_quadratic_is_caught. classify_call reads only the copied port, so the old over-strict "both ports must be bare names" gap is gone too. Ports are read as DIRECT args (no descent into an arg's value) so a nested call doesn't shift the copied-port index (map_merge's copied port is index 1). Fail-closed preserved: a known combiner whose copied port is not a bare name is a counted, located AnalysisOpaque finding — "could not tell" stays distinct from "clean" (DESIGN §5). Deletes surface_subject.dag, the r1_fold_step_subject/r1_judge_fold_step judge, and the 5 synthetic red/green fixtures; the registry coverage they gave is consolidated into a direct classify_call unit test (complexity_r1_accumulator_copy_test) covering list_append/list_snoc/map_merge suspects, non-copied-port and unregistered-combiner cleans, and the opaque case. r1_surface_subject_test → r1_fold_analysis_test (drives the fold end-to-end). Remaining (the follow-on "guessing" discussion): three surface reads inside the fold are still syntactic — carrier = positional first param, combiner = lexeme name, carrier-in-copied-port = symbol equality not dataflow — which want to be edge lookups in a resolved/bound tree. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc
…real, resolve loses its vacuity The foundation PR lexeme-stamped identifier REFERENCES (primary_expr_core -> ^x) but binding INTRODUCTIONS (typed params via dag_grammar_binding_name_terminal) still stamped ^dag_token_ident, so resolve's real name lookup rejected the valid bisect module (the rust_tests red: witness_bisect_wave1_parse_module_add_correctness_holds). Root cause, proven by execution: the normalized wave1 tree has NO Arrow nodes (normalize is shape-preserving; Arrows are built only by the post-resolve MVP body producer), so add_arrow_domain_named_params never fires and nothing binds param names. The pre-PR green was VACUOUS: class-stamped refs collapse to ^dag_token_ident, which is grammar-carried and therefore canonical, so resolve on main accepts a module referencing an undefined variable (proven with and without params in scope). Fix (interim, dissolution trigger on the carrier): - dag_grammar_binding_name_terminal ident arm -> StampLexeme (names are identities, consistent with the namespace-only-resolution direction) - dag_fn_decl_param_binding_atoms + dag_param_binding_atom_harvest: harvest exactly the binding-name atoms from the ^dag_surface_param_list capture (preserved qualified_name/module_header subtrees and lex token-class atoms skipped) - resolve: scope_with_fn_decl_params pushes a ScopeFrame at fn_decl production wrappers so param declarations AND body references resolve under it - dissolves into add_arrow_domain_named_params when body-lowering lands fn_decl -> Arrow lowering in normalize (note data row beside the readers) Red controls (new, CI-gated via interpreted_parse_termination_test): witness_bisect_wave1_unbound_reference_rejected + _no_binding_rejected pin the non-vacuous behavior - an unbound body reference must resolve-reject. They go false if the vacuity ever returns. Verified by execution in an isolated worktree: bisect witness green, both new red controls green, fold_lowering 6/6, r1_fold_analysis, budget_roster gate, loop witnesses, truncated-source rejection all green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
|
Closing: the session auto-WIP sweeper pushed my local working branch and auto-opened this draft. The commit it carries is the real fix and has been pushed to its proper home, PR #6373 (claude/complexity-work-status-97zmt9). — sent from eager-ram-612 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
eager-ram-612.Pushing to
pr-6373advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan