Repository navigation
Complete G2 live-read selection and restore affected-set falsifier narrowing - #7997
Merged
Merged
Conversation
INCOMPLETE BY CONSTRUCTION — this is step 2 of a 7-step sequence and must not land alone. The operator ruling is explicit: "Do not land an intermediate state where the .dag law changes but the seed still uses G1." That is exactly this state. No PR is opened for this branch. WHAT THIS CHANGES. live_read_classification_g2_from_facts unconditionally merged the G1 carrier-home result back into G2 via merge_g1_and_g2_carriers, so a "completed" G2 classification inherited every carrier home reachable through the import graph. Wiring that into the seed unchanged would have preserved the falsifier failure verbatim: completed G2 + broad G1 reachability = RuntimeRead on every nonempty diff. A completed G2 result now contains only the carriers of reachable invocations; G1 is fallback evidence for the case where G2 cannot be established, and that case refuses rather than classifying. WHY, measured. The clean-main axis trace isolates one firing axis for the unrelated entry B (affected_set_floor_runner_test.dag): reads_live_tree=false import_closure=false runtime_carrier=TRUE declared_src=Absent effect_reach=false stop_line=false touched_n=1 stopline_n=1 runtime_data_dependency_touched_via_carrier_closure consults touched_paths only as a nonempty guard and then decides from carrier-home reachability alone, so an entry with a 474-module closure is unskippable on any nonempty .dag diff. That is the documented G1-only interim (live-read-witness-classification-design.md P2), not a regression from #7933. REMAINING BEFORE THIS MAY LAND: - delete the now-dead merge_g1_and_g2_carriers / g1_carriers_from_classification - resolve the now-unused carrier_homes parameter (remove, or state its G1 fallback role) - add the LiveReadSelectionProjection classified/refused seam - replace the pinning test g2_union_retains_g1_import_carriers_with_g2_literal_paths with the three completeness controls - produce the manifest from the whole-tree fn_arrow_decl_facts_live context, memoized at declaration grain on the exact MultiEntryIndex subject - replace the seed predicate; wire precompute parity - mutation-prove BOTH shapes red (nonempty-diff guard; G1 union restored) - dispatch the falsifier on the exact recovery SHA Already present and reusable, so not rebuilt: runtime_read_touched_by_path_g2 + filesystem_path_carrier_touched already implement the classified-case fold (LiteralPath -> path match, ParamRef/UnknownPath -> conservative true). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
Contributor
Author
|
…r_homes' role Still step 2 of 7 — see the DO-NOT-MERGE notice on the parent commit and on PR #7997. The seed still decides from the G1-only interim, so this must not land alone. Deletes merge_g1_and_g2_carriers and g1_carriers_from_classification, which the union removal left with no callers. merge_carriers survives — six other users. carrier_homes is RETAINED on live_read_classification_g2_from_facts rather than deleted, with its role stated in g2_carrier_homes_parameter_role_note. A completed G2 answer deliberately does not read it; the classified/refused projection still to land needs it on the other path, where G2 facts are unavailable and carrier-home reachability decides between refusing loudly and refusing at all. Deleting it now and reintroducing it with that seam would be churn; leaving it silently unread would read as an oversight. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…eness controls Steps 3-4 of 7. Still must not land alone — the seed continues to decide from the G1-only interim until the manifest lands. THE PROJECTION. LiveReadClassification answers what an entry reads and has no arm for "we could not establish what this entry reads". That third state is not cosmetic: an unavailable G2 producer that silently answered LocalRead would be observationally identical to the defect this lane repairs, except failing in the opposite and more dangerous direction — under-selection, which presents as a faster green floor rather than as a failure. LiveReadSelectionProjection (Classified | Refused) lives in v2.std.live_read beside the classification it wraps, so no second classification type exists (DESIGN section 3). WHAT COMPLETE MEANS. G2 concludes LocalRead by finding no reachable carrier invocation. That is sound only when the facts contain the bodies where such an invocation would appear. If the import closure reaches a carrier home whose declarations are absent from the supplied fn-arrow facts, "no call found" and "nothing to look at" are indistinguishable, and LocalRead asserts the stronger. So carrier-home reachability decides COVERAGE, never the answer — G1 as evidence, which is the role the completed-G2 recut left it. WHY THE TWO PINNED TESTS WERE REPLACED RATHER THAN REPAIRED, measured. CI on this branch failed exactly 2 of 7563 witnesses, both in this file, both asserting the union. Their subject is entry-closure scoped: this witness does not import the carrier homes its fixture facts name, so fn_arrow_decl_facts_live() returns no declarations for them and no reachable-invocation evidence exists in that context at all. The union was supplying the carriers, so the assertions passed without the evidence ever being available. Remove it and the same subject answers LocalRead — under-selection. Those tests were asserting a conclusion their facts could not support, so they are replaced, not fixed. THE THREE CONTROLS separate what the union test conflated: evidence present + negative -> LocalRead evidence absent -> Refused evidence present + imprecise -> RuntimeRead (unknown argument) Planted FnArrowDecls supply the coverage the live entry-closure cannot, reusing the production_qualification_origin_probe planting idiom, so the complete-facts cases are reachable now rather than blocked behind the whole-tree manifest. Whole-tree compile-clean over the projection alone: exit 0, zero diagnostics. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ted nothing Two operator corrections. Still step 4/7 — the seed decides from the G1-only interim until the manifest lands, so this must not merge. ROOT GRAIN. call_reachable_decls seeds decls_in_module(entry_module) — every function in the entry FILE. One sibling calling a live-read carrier makes every witness in that file inherit it, so their classifications become indistinguishable. Left in place, the manifest this lane is building would have been keyed per declaration while its VALUES were per file: worse than an honestly coarse manifest, because the key implies a precision the value does not have. call_reachable_decls_from_root seeds the exact enrolled function instead. Entry skip is then DERIVED by conjunction over the entry's rows rather than assumed. A CONTROL THAT TESTED NOTHING. decls_matching_callee compares decl.name — the BARE name — against callee atom text. The planted control 3 emitted the callee as "v2.compiler.self_host.carrier_fn" against name "carrier_fn", so string_eq never matched and the planted carrier was not call-reachable at all. The control typechecked and would have reported success while exercising no reachability edge. Spelling corrected to the bare name. That is the second self-certifying control this session — the first asked its question with an all-zero SHA that rev-parse rejected one guard earlier. Both passed the ordinary run and both were exposed only by execution or mutation, not by review or typecheck. Recorded because the pattern, not either instance, is the finding: a control's green says nothing until something proves it can go red. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
briansrls
changed the title
briansrls
marked this pull request as draft
August 7, 2026 18:35
…g a match failure Step 4/7. Still must not merge — the seed decides from the G1-only interim until the manifest lands. EXECUTED RATHER THAN TYPECHECKED, which is the whole point: complete facts, reachable home, no carrier call -> LocalRead true reachable filesystem_read with unknown argument -> RuntimeRead true carrier-home facts missing -> Refused match failure Control 3 only became meaningful with this commit's predecessor: its planted callee was fully qualified while decls_matching_callee compares the BARE decl.name, so the planted carrier was never call-reachable and the control exercised no reachability edge while reporting success. CONTROL 2's MECHANISM IS CORRECT; THE TEST HELPER IS NOT. The projection returned LiveReadSelectionRefused with exactly the authored cause for exactly the right subject, then the helper's match failed to select an arm that syntactically exists for that variant. Both variants are imported and both sibling helpers match the same type successfully — but they only ever take the Classified arm. Control 2 is the only case that reaches Refused at runtime. A value that IS the variant, against a match that HAS an arm for it, failing to match, points at constructor identity across a module boundary: the lens constructs it by bare reference while the test imports it explicitly. That is the ensure_is_converged pool-resolution class one layer over, and it matters beyond this test — the seed manifest decodes these same variants, where the same failure would present as a memo bug rather than a resolution one. Probing before wiring. Two invocation errors of mine are recorded so the receipts are not read as stronger than they are: I first ran controls 2 and 3 under names I had misremembered, and then, seeing the runner refuse, grepped for the invoked names rather than reading the file and wrongly concluded the controls were never written. Both wrong, both mine, both caught by looking at the source. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ing a wildcard match failure Step 4/7. Must not merge — the seed still decides from the G1-only interim. THE ANOMALY THAT MADE THIS DIAGNOSABLE. Control 2's helper failed as a non-exhaustive match on a LiveReadSelectionRefused value. Inverting arm order and adding a `_` wildcard did not fix it — and a wildcard matches anything, so arm selection never ran. The matcher did not accept the scrutinee as an inhabitant of the type being matched. Exactly one declaration of LiveReadSelectionProjection exists in the corpus, so a duplicate type is ruled out; the lens's constructed value and the test's annotated type are nonetheless not one identity. MECHANISM, and it is this repository's documented one. v2.lens.live_read_classification carries ZERO imports and reaches every type by bare cross-module reference. Those resolve by pool-membership coincidence: LiveReadClassification and LocalRead happen to be dragged in by unrelated importers, while a newly added type has no such incidental importer. That is the ensure_is_converged class from earlier today — a bare reference does not select an identity, it hopes one is present — and it is the reason DESIGN blocks further import-stripping. WHY THIS MATTERS BEYOND A TEST HELPER. The seed manifest decodes these same variants. Had the import gone in silently with the manifest, the identical failure would have surfaced inside the memo decode and read as a caching bug rather than a resolution one. Finding it against a three-line helper is the cheap version. Explicit import added; retest running. If control 2 does not green, a single-declaration type failing a wildcard match is a substrate defect rather than this lane's business, and it goes to the operator instead of being worked around. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…te construction from match Step 4/7. Must not merge. RETRACTING 56c8ad2, both halves. Its diagnosis was wrong. It claimed the lens's bare cross-module reference failed to resolve LiveReadSelectionRefused, by analogy to the morning's ensure_is_converged homonym. But controls 1 and 3 pass, and they construct LiveReadSelectionClassified in that same import-less lens and match it in the test. Both constructors resolve. So this is not module resolution, and the analogy was pattern-matching on the day's earlier incident rather than on this evidence. Its edit was harmful. Adding one import to an import-less file switches that file from pool-coincidence resolution to import-scoped visibility, so every remaining bare reference stops resolving — `path_matches_touched` first. Recorded as a finding in its own right: an import-less .dag file cannot be given "just one" import, and any future migration of such a file must import everything it references in the same motion. A near-miss worth recording. `git checkout --` on the lens restored the COMMITTED state, which contained the bad import, so a probe launched right after "reverting" was measuring a tree with an unresolved symbol. Caught by re-counting imports instead of trusting the word revert. Its output would have been noise readable as signal. WHAT IS ACTUALLY ESTABLISHED: two controls green; the refusal mechanism fires with the correct cause and subject; a `_` wildcard fails to match a Refused value; exactly one declaration of the type exists. What is NOT established is why Refused specifically fails to match. The asymmetry between the arms — one carries a concat-built String — is the next candidate, and the running probe constructs Refused inside the test module to separate construction site from match site before any further hypothesis. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…e, not the caller
Step 4/7. Must not merge.
FOUR HYPOTHESES, ALL REFUTED BY EXECUTION:
cross-module constructor identity refuted — construction AND match in the same
module fail identically
arm ordering / missing arm refuted — `_ => true` is present and the match
is still reported non-exhaustive
duplicate type declaration refuted — exactly one declaration corpus-wide
concat-built cause string refuted — a plain literal "locally constructed"
fails the same way
A `_` wildcard matches anything, so a non-exhaustive report against a wildcard
means arm selection never ran: the matcher does not accept the value as an
inhabitant of the type being matched. That is not a property a caller can get
wrong, so this is a substrate question rather than a test-helper one. The probe
added here checks whether the FIRST variant matches where the second does not; if
Classified matches locally and Refused does not, variant registration for a newly
declared coproduct is implicated.
WHAT WILL NOT BE DONE. Control 2 will not be rewritten around the failure. Its job
is to prove that missing G2 facts REFUSE rather than silently answering LocalRead
— the under-selection guard, and the most dangerous direction in this lane. A
version that dodges the matcher would be the fourth self-certifying control of the
session; a red control with a diagnosis is worth more than a green one with a
workaround.
The refusal MECHANISM is unaffected and demonstrably correct: it fires with the
authored cause for the right subject. Only the ability to pattern-match the result
is broken, so the lane is blocked on this alone, not on its design.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ariant constructors
Step 4/7. Must not merge.
A FIFTH HYPOTHESIS, and the first with a controlled contrast already in the file.
Previously refuted, all by execution: cross-module construction, arm ordering,
duplicate declaration, concat-built payload, declaration formatting (the corpus
idiom uses the same `= Variant { .. }` form on the `=` line, and LiveReadCarrier's
first arm matches fine), and stale disk cache (the tier is opt-in via
GUNBC_RESOLVED_GRAPH_CACHE_DIR and is unset).
The "first arm never matches" rule inferred one commit ago was an ARTIFACT of
which values happened to be tested, not a rule. Both arms fail for this type; the
sibling helpers only ever exercised the arm belonging to the other one.
THE CONTRAST. Two coproducts declared in the same module, matched in the same test
by the same interpreter:
LiveReadClassification test imports the TYPE only;
LocalRead / RuntimeRead resolve BARE -> matches
LiveReadSelectionProjection test imports the type AND both variant
constructors explicitly -> fails
Everything else is held fixed. This commit drops the two constructors from the
import list, leaving the type, so they resolve bare like LocalRead does.
If the probes pass, the finding is that explicitly importing a variant constructor
breaks pattern matching on it — a substrate defect with reach well past this lane,
because the more precise-looking import silently yields a match that can never
succeed. It would also be the third time today that explicitness and
resolve-by-coincidence diverge; in the previous two, explicitness was the repair,
and here it may be the fault.
If they still fail, the import is not implicated and there is no working
hypothesis — which is what will be reported, rather than a sixth guess.
Control 2 stays red until it passes for the right reason.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ng and reduce
Step 4/7. Must not merge.
SEVEN HYPOTHESES REFUTED BY EXECUTION, so this stops guessing and reduces instead:
cross-module constructor identity construction AND match in one module fails
arm ordering / missing arm `_ => true` present, still non-exhaustive
duplicate type declaration exactly one declaration corpus-wide
concat-built payload plain literal fails identically
declaration formatting matches the corpus idiom; LiveReadCarrier
uses the same form and matches fine
stale disk cache tier opt-in via unset
GUNBC_RESOLVED_GRAPH_CACHE_DIR
explicit variant imports dropping them from the import list changes
nothing
THE FACT THAT BREAKS EVERY TIDY STORY: projection_classification_is_local matches
this SAME type successfully — controls 1 and 3 depend on it — while three sibling
functions matching the same type fail. "First arm never matches" was inferred
twice and refuted twice by the next data point.
variant_match_minimal_probe_test.dag is the reduction: ten lines, one two-arm
coproduct, matched in both directions, no imports, no lens, no fixtures. It splits
the space decisively. If it fails, a two-arm coproduct match is broken in the
substrate and reproducible in ten lines, which is its own lane and not #7997's
business. If it passes, the fault is specific to LiveReadSelectionProjection or to
that test file, and the repro is the baseline to bisect against.
A ten-line reproduction is worth more than an eighth theory.
Control 2 remains red. It will not be rewritten around the matcher: it is the
under-selection guard — the control proving missing G2 facts REFUSE rather than
silently answering LocalRead — and a green obtained by dodging the failure would
be worth less than nothing.
Steps 5-7 are not blocked by this. The refusal mechanism is proven correct, so
bridge option 3 and the subject-bound completeness receipt can proceed in
parallel.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…card-payload
Step 4/7. Must not merge.
THE REDUCTION ELIMINATED THE SUBSTRATE. variant_match_minimal_probe_test declares
a two-arm coproduct locally and matches it in both directions with wildcard
payloads: both true. So coproduct matching is not broken, and the fault is
specific to this type or this file.
THE FIRST HYPOTHESIS THAT FITS EVERY DATA POINT, not most of them:
type declared payload binding result
local { a: _ } works (minimal repro)
foreign { classification: c } works (controls 1 and 3)
foreign { cause: _ } fails
foreign { classification: _ } fails
Foreign-declared coproduct plus a wildcard payload binding does not match. This
accounts for the fact that defeated every earlier theory: projection_classification_is_local
matches the SAME foreign type successfully, because it binds the payload by name
rather than with `_`. "First arm never matches" fit two points and broke on the
third; "explicit variant imports" fit a surface difference and not the outcome.
variant_match_foreign_probe.dag plus the two probes here are the clean 2x2: same
foreign type, same test module, only the payload binding differs.
If wildcard fails and named passes, the defect is pinned to a one-line difference,
and control 2 gets a fix that is not a dodge — bind the payload by name instead of
`_`, because `_` provably does not work across a module boundary, with the defect
documented separately for whoever owns the compiler. If both pass, something
remains specific to LiveReadSelectionProjection, and the last unexplored axis is
what distinguishes it from LiveReadClassification in the same module.
Eighth hypothesis, which is more than anyone would like. The justification is that
each round has been cheap and strictly eliminative, and the blocked control is the
under-selection guard — the one whose absence lets the floor silently skip
witnesses it should run.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ilure
Step 4/7. Must not merge.
The 2x2 refuted hypothesis 8: a FOREIGN-declared coproduct with WILDCARD payloads
matches fine (both probes true). So neither the declaration site nor the wildcard
binding is the fault, and the elimination table is now:
substrate coproduct matching local repro passes both arms
foreign declaration site foreign probe passes
wildcard payload binding foreign probe passes with { a: _ }
payload type Refused carries String and still fails
constructor imports removing them changed nothing
arm order / duplicate decls /
concat payload / formatting /
disk cache all refuted earlier
ONE VARIABLE REMAINS, and it is the one only half-tested before: the TYPE NAME
being explicitly imported. ForeignTwoArm resolves bare in its probe and matches;
LiveReadSelectionProjection is imported by name and does not. The earlier round
removed only the CONSTRUCTORS from the import list and left the type, so this axis
was never cleared. This commit drops the type too, leaving the file to resolve it
bare exactly as it already resolves LocalRead and RuntimeRead.
If confirmed, control 2's fix is one line and not a dodge — reference the type the
same way the working sibling helpers reference theirs — and the defect is written
up as its own lane, because "an explicit type import silently yields an unmatchable
value" would bite every file the namespace migration touches.
If refuted, this stops. Nine eliminative rounds is enough; the repro artifacts are
committed and the table goes to whoever owns the compiler rather than a tenth
guess.
Either outcome, step 5 starts next: bridge option 3 and the subject-bound
completeness receipt. The matcher question is a side lane; the falsifier stays
dark until the manifest ships, and that is the critical path.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
… result produced Step 4/7. Must not merge. Hypothesis 9 (explicit type import) refuted: dropping LiveReadSelectionProjection from the import list, leaving the file to resolve it bare exactly as it resolves LocalRead, changed nothing. Both Refused cases still fail; control 1 still passes. STOPPING AT NINE WAS THE STATED PLAN AND IS BEING BROKEN DELIBERATELY. The ninth result did not merely refute — it produced a pattern out of data already in hand: function arm order value result projection_classification_is_local Refused, CLASSIFIED Classified pass projection_is_refused v1 REFUSED, Classified Refused fail projection_is_refused v2 CLASSIFIED, wildcard Classified fail Every failure is a value matching the FIRST arm. Every success is a value matching the SECOND. That fits every observation in the investigation, costs one test, and yields a one-line fix if true. Stopping on principle there would have been stubbornness, not discipline. This commit puts Refused in SECOND position with both payloads bound by name and no wildcard, then matches a Refused value. IF CONFIRMED the finding is serious and belongs in its own lane: the first arm of a match over a foreign coproduct never matches, which does not error — it MISROUTES control flow, silently, anywhere it occurs. The local minimal repro passing is consistent with that if locally declared types take a different path, which is exactly what would let such a defect survive undetected. IF REFUTED this stops for real and the elimination table goes to whoever owns the compiler. Either way step 5 begins next: bridge option 3 (dependency_resolution_facts_live -> ModuleDependencyEdge, ModuleImportFact fixture-only) and the subject-bound completeness receipt. The falsifier stays dark until the manifest ships; control 2 can green later once the matcher question has an owner. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
Step 4/7. Must not merge.
Hypothesis 10 (arm position) refuted: LiveReadSelectionRefused fails in SECOND
position too, with both payloads bound by name and no wildcard present. Stopping
here as committed.
TEN ROUNDS, ALL REFUTED BY EXECUTION:
substrate coproduct matching local minimal repro passes both arms
foreign declaration site foreign probe passes
wildcard payload binding foreign probe passes with { a: _ }
payload type Refused carries String and still fails
constructor imports removing them changed nothing
explicit type import removing it changed nothing
arm position Refused fails first AND second
arm order / duplicate decls /
concat payload / formatting /
disk cache refuted earlier
WHAT REMAINS TRUE AND UNEXPLAINED: LiveReadSelectionClassified matches (controls 1
and 3 depend on it); LiveReadSelectionRefused never matches, in any position, with
any binding, imported or bare. Both are arms of one coproduct with a single
declaration, in a module whose OTHER coproduct (LiveReadClassification) matches
both of its arms fine — RuntimeRead is likewise a last variant with a record
payload and it matches.
Two committed artifacts for whoever owns the compiler:
src/v2/test/claim/variant_match_minimal_probe_test.dag local type, passes
src/v2/test/fixture/variant_match_foreign_probe.dag foreign type, passes
Both are green, so they bound the defect from the working side rather than
reproducing it — the reproduction is control 2 itself.
Diagnostic scaffolding removed. The helper is a clean two-arm match and control 2
stays RED, which is the honest state: its mechanism is proven correct (it refuses
with the authored cause for the right subject) and only the ability to
pattern-match the result fails. It is not rewritten around the matcher because it
is the under-selection guard, and a green bought by dodging would be worth less
than nothing.
Step 5 next: bridge option 3 and the subject-bound completeness receipt.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…cy edges
Step 5 of 7 begins. Must not merge: the seed still decides from the G1-only
interim until the manifest and predicate swap land.
live_read_classification_g2_from_edges consumes ModuleDependencyEdge +
ModuleDeclarationFact + FnArrowDecl, keyed by entry PATH, entry module, and the
exact enrolled FUNCTION — so it uses step 4's declaration-grain root rather than
seeding every declaration in the entry file.
WHY ModuleDependencyEdge AND NOT ModuleImportFact (operator ruling). module_graph
declares dependency_resolution_facts_live the single swappable edge producer and
forbids a second one, because the namespace terminal step replaces its BODY when
the import grammar is deleted. Calling import_resolution_facts_live instead would
omit the strict-tier reference-derived edges that producer already unions in, so
the G2 closure would be NARROWER than the selection closure deciding the same
question one axis over — an under-selection source. It would also bind live
classification to a grammar scheduled to disappear, so the namespace swap would
silently narrow G2 rather than leaving it untouched, which is the exact failure
the edge-source-agnostic-by-construction note exists to prevent.
ModuleImportFact stays fixture-facing. It is a hand-authorable {module, imports}
view with NO live producer in the corpus — which is what makes it good for planted
tests and unfit for production: a shape nothing derives cannot be kept honest
against the tree. The seed does not mint it either; asking the host to fabricate
the fact shape would put fact production back in the layer this lane repairs.
TWO MECHANICS WORTH RECORDING. ModuleDeclarationFact {module, path} is the
path/module bridge: dependency_closure works in PATH space while G2 reachability
works in MODULE space, so modules_of_closure_paths translates using the same fact
rows the closure was built from rather than a second mapping. And FreeMonoid<T> IS
the list type — fold_list takes it directly — so no conversion is needed; a
free_monoid_to_list call was written and removed before building.
Next in step 5: the CompleteForSubject{index/tree identity} vs
IncompleteOrUnbound{cause} receipt replacing the one-declaration-per-carrier-home
heuristic, then the declaration-grain manifest and its MultiEntryIndex-bound memo.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…d on a partial one
Step 5 of 7. Must not merge — the seed still decides from the G1-only interim.
5a typechecked clean (whole tree, GATE_EXIT=0).
COMPLETENESS IS NOT INFERABLE FROM THE FACT LIST, which is why the previous
heuristic was wrong in KIND rather than merely weak. It asked whether every
reachable carrier home contributed at least one declaration — that is, it asked
the facts to vouch for their own coverage, which is the question it was trying to
answer. A List<FnArrowDecl> holding one planted declaration is indistinguishable
from a whole-tree projection with one match.
G2FactSubject is therefore CARRIED from the producer:
WholeTreeFactSubject { subject_id } the exact index/tree the facts came from
PartialFactSubject { cause } a fixture, planted list, or narrower context
THE GATE IS DELIBERATELY ASYMMETRIC, and the asymmetry is the entire content of
the type:
partial + RuntimeRead -> classified seeing a call proves a call exists; positive
evidence survives a narrow view
partial + LocalRead -> REFUSED absence of evidence in a partial view is not
evidence of absence
Only the verdict that can license a skip requires the whole-tree subject, so
under-selection is unreachable through this path rather than merely discouraged.
It also makes the memo CHECKABLE rather than only fast: a manifest carries the
subject it was built against, and a lookup whose current index differs refuses
instead of serving a classification derived from another tree. Evidence that
cannot name its subject cannot be checked against it — the same defect class as
this morning's baseline that did not name the commit it compared.
Next: 5c, the declaration-grain manifest and its MultiEntryIndex-bound memo.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…uses on mismatch Step 5 of 7. Must not merge — the seed predicate is not swapped yet. 5a and 5b both typecheck clean on the whole tree (GATE_EXIT=0), so the .dag half of step 5 is complete: production G2 consumes the canonical ModuleDependencyEdge boundary, and the carried G2FactSubject refuses LocalRead on a partial subject while still classifying RuntimeRead. THE MANIFEST NAMES ITS SUBJECT. G2 classification is expensive — it needs fn-arrow facts reflected from a whole-tree resolved context, which is why the design pairs path-intersection with memoization rather than treating the memo as an optimisation. But a memo whose validity is implicit is a cache with no invalidation story: it serves whatever it holds and cannot say which tree the answer came from. subject_id is the content identity of the source population the classifications were derived from, and a lookup whose current index differs REFUSES. No invalidation heuristic is needed because the subject identity IS the validity condition. Same discipline the freeze-gate baseline needed this morning, with a worse failure mode: a stale classification that looks fresh would license a SKIP. BOTH FAILURE PATHS REFUSE RATHER THAN RETURN ABSENCE. Subject mismatch refuses; a missing declaration row refuses. Neither yields a None a caller could read as "nothing known, proceed" — an absent row is a gap in the classification, not evidence of no runtime read. Refused is deliberately not an error channel: it is the state that FORBIDS a skip, so it must survive into the seed rather than being flattened to a bool. ROWS ARE DECLARATION GRAIN. One verdict per entry would make a single live-read witness render every sibling in its file unskippable — the same precision loss the G1 union caused one layer down, and the reason step 4 moved the root off the file. Remaining in 5c: the producer that evaluates the projection against a whole-tree context and fills the manifest, plus the memo field on MultiEntryIndex. Then 5d swaps the seed predicate and 6 gives precompute the same result. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…e context The manifest is built by a single evaluation folding over every request, not one evaluation per declaration: the edge/node/decl closure is derived once and shared. Per-request evaluation would recompute the whole-tree projection for each row, which is the affordability problem the G2 design names when it pairs classification with carrier memoization. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ng consumer Builds the whole-tree manifest in ONE evaluation over the full request set and decodes each row. Every failure arm refuses: a partial manifest would convert the producer's own failure into a skip licence for the rows it dropped, which is the under-selection direction this lane exists to close. Three executing tests: the producer discriminates a carrier-reaching declaration from a pure one against the real tree, and the lookup refuses on both subject mismatch and absent declaration. Also escapes a literal brace in a lens doc string that the module-binding parser read as interpolation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
…ind the root, mint the subject Addresses the review on 351e4d2. Six changes, each closing a hole that made the manifest unable to carry what the selector needs: FULL MIRROR. LiveReadClassification, LiveReadCarrier and PathPattern are mirrored arm for arm instead of collapsing to runtime_read: bool + Vec<String>. That collapse discarded literal-path identity, param-vs-unknown, and scan-vs-reflection — leaving a consumer only 'some runtime read happens', whose one safe reading is 'every nonempty diff touches it', which is the G1 over-selection rebuilt a layer up. touched_by is one total fold over the mirror: literals compare, param/unknown/structural-scan are touched by any nonempty diff as the model's precision frontier, LocalRead never, Refused always. DECODER. Carriers arrive as Value::Variant, and the previous decoder handled only Value::Str and Value::Record with a wildcard empty-vector fallthrough — so every real carrier decoded to an EMPTY carrier list, which reads as 'runtime read, intersecting nothing' and licenses the skip the runtime read forbids. That absorbing arm sat directly beneath a doc-comment claiming fail-closed behaviour, and the old discriminating test passed through it because it compared only the bool. Nine controls now execute the five carrier arms plus the non-variant and unmodelled-variant refusals. ROOT BINDING. entry_path/entry_module/fn_name were three independently writable strings: the closure walked from the path while seeding used the separately supplied module and name. Zero matches seeded an empty walk and classified LocalRead — the strongest answer, licensing a skip; many were silently unioned. bind_g2_root derives the module from the path and refuses zero-or-many at both transitions. SUBJECT. Minted by MultiEntryIndex as an opaque generation, never a caller string; WholeTreeFactSubject is nullary and constructible only where the live whole-tree producers are called. The mismatch control now uses a real second index over identical source roots, which a caller-authored label could not have distinguished. PARTIAL NEVER DECIDES. The asymmetric gate accepted partial RuntimeRead on the reasoning that positive evidence survives a narrow view. Existence survives; the PATH SET does not, and that set is what selection consumes — a partial view of a two-literal closure still says RuntimeRead while exposing one path, so a diff touching the other licenses a skip. Every partial subject refuses, retaining the classification as diagnostic payload. MEMO + DUPLICATE KEYS. One manifest per index, refusals memoized too; a duplicate declaration key refuses rather than letting HashMap::insert discard a classification without saying which. Probe files deleted. Green by execution: 9/9 decoder and selection-fold controls. Producer controls still to re-run serially — four whole-tree indices concurrently OOM-killed the run. STILL OPEN from the review: whole-tree fn-arrow coverage is a construction wall around an unproven premise (recorded in whole_tree_subject_mint_site_law, needs the outside-closure control); the G1 production predicate is still in place; precompute parity, CI enrolment of these controls, and both mutation proofs remain. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs
briansrls
force-pushed
the
claude/falsifier-g2-runtime-read-closure
branch
from
August 8, 2026 05:26
3412fe2 to
7b3b9a9
Compare
briansrls
marked this pull request as ready for review
August 8, 2026 15:45
briansrls
pushed a commit
that referenced
this pull request
Aug 8, 2026
…tion, and a retracted claim reproduced
TWO SELF-INFLICTED, both found by reading `gunbc_ci_selection_control_step_note`
rather than by anything executing.
(1) `stop_line_population_does_not_widen_incident_subject` built its injected
name-status with `\u{0}` — an actual NUL byte. The separator is the literal
four-character sequence `\000`: `floor_diff_observe` splits the injected value on the
STRING "\\000", which is also what the suite's own `injected_name_status_modify`
emits. A NUL would have decoded as one unsplit path, so the control would have
exercised a population it does not name — passing or failing for a reason unrelated
to the stop line. That is the shape of the two controls #7997's body recorded as
testing nothing, reproduced here.
(2) The previous commit's correction to `falsifier_rehomed_bin_wet_rows` said the
suite is "caught within one cadence window rather than at merge". That exact phrasing
was ALREADY RETRACTED in the tree as too strong (`gunbc.ci_workflow`
`gunbc_ci_selection_control_step_note`, review correction 2026-07-30): the falsifier
is queue-not-cancel and the step sits after the prelude and release build, so a
regression landing just after a run passed the control waits for that run's
remainder, plus queued-run startup, plus the next run's prelude and build — a sum
that can exceed one cadence period. The honest statement is that it reds when the
NEXT COMPLETED control runs.
So a commit whose whole subject was correcting a stale citation introduced a claim
the tree had explicitly rejected, into a load-bearing roster, one commit later. It now
uses the words the retraction settled on.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 10, 2026
…roup_by and execute the interpreter-parity controls CI only compiled (#8055) * Consume the G2 live-read manifest at every selection decision; retire the G1 carrier-home predicate #7997 landed the declaration-grain G2 classification, the canonical dependency-edge production, the subject-carrying manifest and its per-index memo — but left the old answer in charge. Every production decision still called `runtime_data_dependency_touched_via_carrier_closure`, whose only use of `touched_paths` was `is_empty()`; it then answered from broad carrier-home reachability with no path intersection at all. So an entry with a wide import closure stayed unskippable on any nonempty `.dag` diff, which is the `2 selected / 1 expected` incident and the `SelectionSuperset` the floor reports. ONE CONTEXT, ONE DECISION. `LiveReadSelectionContext` is built once per index from the COMPLETE discovery roster and answers axis (iv) through `runtime_dependency_touched_for_entry`. An entry is untouched on this axis only when every enrolled declaration is present, classified, and untouched. Producer failure, subject mismatch, absent row, absent entry, and an entry with no enrolled declaration all REFUSE: none falls back to the retired predicate, silently widens to a whole-corpus run, or licenses a skip. A missing classification is not a missing runtime read. FIVE CONSUMERS, NOT FOUR. Beside the four named decisions, `discovery_rows_runtime_dependency_touched_count` fed the precompute's `touched_runtime_dependency_entry_count` through a SECOND carrier fold. That is how a retired predicate survives its replacement — the precompute keeps a copy — so it now counts by calling the same function the per-row path decides with. Parity is construction, not two implementations a later edit can separate. THE COMPLETE-ROSTER REQUIREMENT IS ENFORCED, NOT DOCUMENTED. The memo is index-scoped and request-set insensitive, so a first call carrying a chunk would memoize a partial manifest and every declaration outside it would afterwards refuse. `live_read_manifest` now refuses a later call whose requests its rows do not cover, naming the priming rather than the lookup: `row_for` would also have refused, but its cause reads as a classification gap when the defect is where the manifest was built. Two shapes the code forced, against the plan: - A prebuilt context cannot be handed to a width>1 worker. Each worker calls `build_multi_entry_index` in its own closure and therefore carries its own generation, so the main thread's manifest would refuse on subject mismatch at every lookup — correctly. `run_discovery_rows` takes the complete roster beside its chunk and each worker builds its own context. - The context is built whenever selection is on at all, PredictOnly included. The falsifier runs PredictOnly and counts divergences; predicting from a different predicate than the applied one would make it measure agreement with a retired answer. RETIRED, with zero remaining consumers: the predicate, `LIVE_READ_CARRIER_HOME_MODULES_V0`, `import_closure_module_reaches_carrier_home`, and the const's drift gate. The stale comment citing the removed `merge_g1_and_g2_carriers` as the seed's soundness reason goes with them, as do two further stale citations of the deleted const (in `v2.lens.enforcement.gate_test` prose and the design doc's status line, which still described the G1 interim as the production axis). `lying_substrate_inputs_only_stamp_census` was a real semantic consumer, so rather than delete a merge gate it is re-expressed on the authority that now decides: a SubstrateInputsOnly-stamped declaration classifying RuntimeRead — or refusing — is a lying stamp. Same intent, one authority, no mirrored roster. A COST SHAPE THIS CHANGE ACTIVATES. `live_read_selection_manifest_over` accumulated with `list_snoc_item`, which is `list_append(acc, single)` and rebuilds the whole left list per row — quadratic in the request count. The realized n stopped being small the moment the producer gained a production consumer folding over the complete corpus roster, so it is fixed here per DESIGN section 6's bare-minimum-cost rule. Prepending via `fold_list_right` is O(1) per row and preserves the emitted order (the idiom is copied from `list_append` itself); order is in any case not load-bearing, since the seed decodes rows into a key-addressed map that refuses duplicates. EXECUTING CONTROLS live in `floor_skip_discovery_witness` — CI compiles `v1-compiler-tests --no-run` and does not execute `cli_run.rs` unit tests, so a control placed there would prove nothing. The incident-subject control asserts `selected_entry_groups == 1` of 2, which is the grain the incident was measured in: row totals can read 2/1/1 while both entry groups were selected and resolved. A stop-line-population control separates that axis from axis (iv), and two refusal controls pin `LiveReadEntryAbsent` and `LiveReadContextSubjectMismatch`, each with a positive control beside it so the refusal is a fact about the missing subject rather than about a broken context. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore the stamp census to the floor's declared scan dirs, and state the subject change The rewrite in the previous commit re-expressed `lying_substrate_inputs_only_stamp_census` on the G2 manifest but discovered its roster from `dag/test/claim` alone, which is narrower than the floor's own declared population — a silent scope narrowing inside a change whose whole subject is selection breadth. It now discovers over `gunbc.ci_layer_roots` `witness_discovery_scan_dirs`. The grain change that remains is real and is now stated in the test rather than left to be found: the retired form walked every `*_test.dag` with a parseable disposition because an entry-grain import closure needs no declaration names, while this form is declaration-grain and its subject is the enrolled roster. A `*_test.dag` outside discovery is not covered — it is also not floor-selectable, so it sits outside the population the stamp governs, but the two subjects are not identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a stale justification: the rehomed selection-control row cites per-PR coverage that #7446 removed `falsifier_rehomed_bin_wet_rows` gave two grounds for keeping `floor_skip_discovery_keystone_holds` off the per-PR lane: a measured 289s wall, and that the row was "ALSO a per-PR duplicate: the ci job's own Affected-set selection control step already runs on every PR". The second ground is false. #7446 (Demote the affected-set selection control to the falsifier cadence) moved that step out of `ci.yml` into `falsifier.yml`; `ci.yml` builds, verifies and tars the binary but never invokes it, and `falsifier.yml` runs on `schedule`/`workflow_dispatch`, where the step's own `GITHUB_EVENT_NAME = pull_request` skip branch cannot fire. So the roster row justifies an exclusion by pointing at coverage that stopped existing — a citation that rotted without anyone touching it or the thing it named. The rehome itself stands: the measured wall is its own sufficient ground, and this commit changes no admission decision. What changes is that the row now says what is true, and states the coverage grain plainly — the binary executes on the falsifier cadence only, so this suite (including the affected-set incident controls this branch adds) is caught within one cadence window rather than at merge. Found while establishing where the new controls actually execute, which is a question the stale sentence would have answered wrongly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Assert the unrelated entry skips BEFORE resolving, not merely without running `selected_entry_groups == 1` proves the unrelated entry ran no witness. It does not prove its cold entry resolve was elided: a row skipped as assumed-green AFTER its entry resolved records no `witness_outcome` either, so both states produce the same counter. Eliding that resolve is the entire cost win axis (iv) exists to buy — a resolve-then-skip pays the 474-module closure and reports identically. The control now also asserts the skipped row's provenance is `skip-before-resolve-fast-path`, which is the fact that distinguishes them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix two defects in this branch's own work: a malformed control population, and a retracted claim reproduced TWO SELF-INFLICTED, both found by reading `gunbc_ci_selection_control_step_note` rather than by anything executing. (1) `stop_line_population_does_not_widen_incident_subject` built its injected name-status with `\u{0}` — an actual NUL byte. The separator is the literal four-character sequence `\000`: `floor_diff_observe` splits the injected value on the STRING "\\000", which is also what the suite's own `injected_name_status_modify` emits. A NUL would have decoded as one unsplit path, so the control would have exercised a population it does not name — passing or failing for a reason unrelated to the stop line. That is the shape of the two controls #7997's body recorded as testing nothing, reproduced here. (2) The previous commit's correction to `falsifier_rehomed_bin_wet_rows` said the suite is "caught within one cadence window rather than at merge". That exact phrasing was ALREADY RETRACTED in the tree as too strong (`gunbc.ci_workflow` `gunbc_ci_selection_control_step_note`, review correction 2026-07-30): the falsifier is queue-not-cancel and the step sits after the prelude and release build, so a regression landing just after a run passed the control waits for that run's remainder, plus queued-run startup, plus the next run's prelude and build — a sum that can exceed one cadence period. The honest statement is that it reds when the NEXT COMPLETED control runs. So a commit whose whole subject was correcting a stale citation introduced a claim the tree had explicitly rejected, into a load-bearing roster, one commit later. It now uses the words the retraction settled on. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the producer's fact universe, propagate the modelled refusal, and retract the P3 claim The previous head consumed a manifest whose fact universe was the classification lens's OWN import closure, which makes this branch a widening rather than the repair it was named for. Three coupled fixes, none of which lands alone. FACT UNIVERSE. `fn_arrow_decl_facts_live()` reflects the eval context's modules (`for_each_live_registry_item` iterates `ctx.modules`), and the producer resolved `LIVE_READ_CLASSIFICATION_ENTRY` alone. So every request root outside that closure — nearly every enrolled witness — could not bind: `bind_g2_root` finds the module fact (whole-pool scan) but no fn-arrow declaration, and answers `G2RootUnbound`. The manifest carried a modelled refusal for essentially every declaration. The tree already said this in `production_qualification_origin_probe`: "fn_arrow_decl_facts_live() scope is entry-closure today", and `whole_tree_subject_mint_site_law` flagged the coverage premise as unproven. It is not merely unproven; it is false. The context is now resolved from the INDEX'S OWN sources, so universe identity is structural rather than asserted — the facts cannot describe a different tree than the one the consuming index holds, because they are derived from exactly its files. Deliberately NOT `whole_tree_resolved_ctx`: that helper applies the witness and strict-resolve exclusion sets first, so its universe can omit the very test declarations this manifest must classify, and its name would have read like a receipt while excluding the subject. Sources are sorted so the build is not host-iteration-order dependent. Coverage is checked at identity grain, not by count. `fn_arrow_decl_substrate_is_whole_tree()` projects only `ctx.modules.len()` into a census comparison, and equal counts do not prove equal identities: a context with the right number of modules and a substituted one answers that check and still cannot classify the declaration that went missing. So a resolved-module shortfall refuses by number AND the primary wall is per-root — any request root that fails to bind produces a modelled refusal, which the consumer now propagates. MODELLED REFUSAL PROPAGATES. `touched_by` answers `true` for a `Refused` row, which is right for a path-intersection question and wrong for a consumer to act on: routed through the boolean, an undecidable classification is indistinguishable from a decided "this diff touches a runtime read", so an incomplete producer presents as `SelectionSuperset` — everything ran, slow but apparently valid — instead of "the manifest cannot decide". `runtime_dependency_touched_for_entry` now matches the arm explicitly and returns a typed, located `Err`. The entry still does not skip; it does not skip because the line STOPPED, not because a widened answer looked like a decision. TWO CONTROLS, for the two arms the existing ones did not reach. `live_read_classifies_a_declaration_outside_the_lens_closure` pins the defect directly: a real enrolled witness entry that `v2.lens.live_read_classification` does not import must CLASSIFY, and mutating the producer back to a lens-entry context makes it red. `live_read_present_but_refused_row_propagates_refusal` covers the arm the missing-entry control cannot: a row that is PRESENT and refused must stop the line, where the existing control only exercises a roster-lookup miss. P3 RETRACTED to candidate in the design doc. "P3 landed" was written against the consumption half alone and was wrong for exactly the reason above; producer universe completeness and production consumption are ONE atomic change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bound the fact universe to the request roots' closures, not the whole index The previous commit resolved the index's ENTIRE source population to guarantee every request root could bind. Sound, but it pays a whole-corpus resolve to answer any question — including the two-entry rosters the selection-control suite runs. A producer that costs a corpus resolve to decide a two-entry question is the cost shape this lane exists to remove, reintroduced one layer up, and it would have been measured as a regression in step 6 rather than caught by reading. The universe is now the union of the request roots' own closures from this index's pool, plus the classification lens's closure. Containment is by construction rather than by hope: classifying (E, f) needs E's module and the modules `call_reachable_decls_from_root` walks from it, and both are exactly E's import closure. For the full floor roster this approaches the corpus anyway — correctly, that IS the population being decided — while a scoped roster now pays only for what it asks about. Deduplicated and ordered through a path-keyed BTreeMap, so overlapping closures cost one entry each and the resolve is not a function of host hash-iteration order. A root whose closure cannot be loaded refuses by name rather than resolving a population that silently lacks it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Instrument the manifest build: requests, universe size, wall, CPU, RSS Step 6 of the acceptance sequence needs a measurement, not an argument. This producer resolves the union of the request roots' closures once per index, and that has to be paid back by the entry resolves selection elides; two cost readings on this lane have already been wrong, so the numbers are printed where any run that builds a manifest carries them and a reader can divide them by the resolves saved. CPU is reported beside wall via `getrusage(RUSAGE_SELF)` because the two answer different questions on a shared runner: wall includes time the process spent descheduled behind co-resident jobs, so a wall figure alone cannot separate "this producer is expensive" from "this host was busy", and a cost claim that cannot tell those apart is not a measurement. RSS is labelled as whole-process and therefore an upper bound rather than this producer's attribution — other work shares the process, and quoting it as the producer's own would be the same overclaiming this lane keeps producing. Emitted unconditionally rather than behind a verbose flag: a measurement that only appears when someone thinks to ask for it is not available at the moment a regression lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the producer/decoder representation boundary; measure the union producer The decoder required Value::List while every representation the producer can return is the modeled FreeMonoid chain, so a well-formed manifest reported as a foreign shape. Decoding now accepts the native list and the Empty/Cons chain through the interpreter's own free_monoid_to_vec, inside the active context (the Empty/Cons/head/tail symbols resolve through active_ctx, so a decode outside it reports every variant as foreign). A non-collection value refuses by name rather than decoding to zero rows. The fold was never the functional defect. Both folds return the same modeled collection; execution disproved the earlier attribution, and the note recording that mistake is corrected rather than deleted. Instrumentation added, and it measures the union producer out of the design: one request over a 545-module union costs 179125 ms wall / 178751 ms CPU at 9.4 GiB whole-process RSS. That specimen no longer reproduces the prior SIGKILL -- which is not the same as the OOM class being closed, and the full roster, wider unions and width-N workers remain unproven. fn_arrow_decl_facts_from_sources lands as the replacement's core: the same FnArrowDecl population derived from a parse rather than from the eval context's resolved modules, reusing build_item_info and fn_arrow_decl_record verbatim so it is not a second definition of the fact. Not yet consumed. The foreign-shape control was vacuous -- it rebuilt a well-formed roster and asserted it decoded, which the control above it already proves. It now calls the decoder with a non-collection value and asserts the refusal by cause. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Merge main; land the index-scoped G2 fact substrate with a bidirectional identity join Merges current main (7bcd31d's decl-facts work included) BEFORE binding a declaration key, so the bundle binds to the landed ResolvedDeclarationLocator surface rather than to a key invented against a stale one. That merge changed the plan for the better. decl_facts_corpus_walk already IS a parse-level declaration walk over pool roots with no eval context, so the hand-rolled walk written before the merge was a second definition of a declaration fact. It is deleted. What remains is one projection, push_decl_facts_from_parsed, shared by the corpus walk and the new index-scoped walk; a caller chooses only which modules to visit. Two divergences the live-read consumer requires, each stated where it lives: the corpus walk skips is_test_dag, and enrolled witness declarations are exactly those files, so an unfiltered population is needed -- an empty one would read as "no runtime reads", a silent narrow. And parse_dag_file drops unparseable files to None, which is fine for a census and not for a consumer deciding skips: a dropped module's declarations report as unbound, conflating "no such declaration" with "its module did not parse". parse_dag_source is extracted as the content-taking core (parse_dag_file becomes its filesystem instantiation) and names its refusal. G2FactBundle carries the exact index pool with TWO levels of failure, because collapsing them recreates the union's defect one layer down: the bundle refuses only when the index-wide population itself cannot be observed, while a module that will not parse is a local fact under its own identity. bad A -> A refuses, never bad A -> bundle refuses -> B disappears. Completeness is an identity join in both directions, never a count: a population with one identity missing and one extra has the same size and is a different tree. Foreign facts refuse; unvisited index modules refuse. Visits are reported by the walk rather than inferred from absence, because a module may legitimately parse and declare nothing -- an earlier revision of this join computed that check and then discarded it under a comment claiming it caught a defect it could not catch. Facts are cached RAW. A marshalled Value carries symbols interned in the evaluating context, so caching marshalled rows on the index would hand one context's symbols to another's evaluation. Not yet wired: the union resolver, complete-roster memo guard and stale fold row are still present and still in charge; this commit adds the substrate they will be replaced by. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Index-owned fact cell, declaration-keyed row cache, and zero/one/many request binding Replaces the one-manifest memo's SHAPE, ahead of removing its last consumer. g2_facts is index-owned and request-set INSENSITIVE: the population is the index's, so any roster reads the same facts and no roster can prime it partially. live_read_rows fills incrementally, keyed by ResolvedDeclarationLocator rather than a rendered entry::name string, so two same-named declarations in different modules cannot share a verdict and a miss classifies one declaration instead of poisoning the index. The suite already disproved "complete on first access" as a property an index can have -- the same immutable index is legitimately reused across scenarios with different rosters -- so this is not a convention made easier, it is the convention deleted. Binding is separated from classification. A request names a SPELLING, and a spelling is not an identity: over a whole-tree population it may match nothing or more than one. Folding that into classification would force a verdict out of an ambiguous subject and let "many" become whichever the walk reached first -- a heuristic standing where an identity was owed. All three cardinalities are answered, only exactly-one proceeds, and zero and many refuse with different causes because their remedies differ. An entry whose own module failed to parse refuses under its own key, locally, leaving unrelated entries classifiable. ResolvedDeclarationLocator derives Hash beside its existing Eq so the hash and the equality cannot disagree about which fields decide identity. Not yet wired: nothing consumes these yet. The union resolver and the complete-roster guard are still in charge on the decision path. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cut over to the index-bound producer; delete the union resolver and the complete-roster convention ONE transition, per the ruling: the bridge and its consumer land together, and the machinery they replace is deleted in the same change rather than left beside them. THE PRODUCER. fn_arrow_decl_facts_index_live is a transport, not a second semantic authority: it reads the exact MultiEntryIndex bound to the classification operation, delegates to the shared push_decl_facts_from_parsed projection, reads no files, resolves nothing, walks no closure and decides no classification. It marshals into the CURRENT evaluator context because a marshalled value carries context-interned symbols; what is cached is the parse. With no index bound it REFUSES -- it does not fall back to reflecting the eval context, because the two producers answer about different subjects and substituting one for the other is never a safe default, and an empty population would read as "no runtime reads" and license a skip. It arrives the supported way: .dag declaration, authored roster row, regenerated dispatch (a 3-line diff, generated from the roster rather than hand-edited), interpreter arm. dependency_resolution_facts_live remains the sole edge authority; only the missing fn-arrow projection is supplied. THE LAW CHANGED BECAUSE ITS PREMISE DID. whole_tree_subject_mint_site_law admitted it had not proven the producer covered the consuming index, and it could not: that producer reflects the eval context, so coverage meant evaluating a union of every request root's closure. Measured at 179125 ms wall / 178751 ms CPU for one request, and then it failed outright -- bare names that bind uniquely inside each entry's own import scope stop binding across a union, so Holds, Finding, Exact, Refuse, Blocking and FailClosed went unresolved and ONE shared refusal denied classification to all 133 enrolled entries. That is a property of composition, not a repairable module. Coverage is now established by a bidirectional identity join before any subject is minted, and completeness is per bound request: an unrelated module that fails to extract refuses only the requests whose closure contains it. Reading the subject as "the whole index parsed" would recreate the union's failure in another form. The variant is still spelled WholeTreeFactSubject; the honest name and the deferred rename are stated in the law rather than left to make the prose quietly false. DELETED, not deprecated: the union resolve and its RequestUniverseUnresolved, RequestUniverseIncomplete and RequestRootClosureUnloadable causes; the one-manifest memo, its complete-roster requirement and MemoRequestPopulationIncomplete; the old live_read_selection_manifest_live mint site; and the fold essay whose premise the complete roster was. Only the classification lens's OWN closure is resolved now -- one entry, so a refusal there is about the lens and cannot be caused by an unrelated module. The context becomes a roster-scoped VIEW over the index-owned cache, and re-checks the subject at lookup rather than trusting construction. The memo test asserted Rc::ptr_eq on one manifest -- precisely the property being deleted, since it could only hold if a single object served every request. It is replaced by the incrementality and cache-hit controls: disjoint rosters classify in any order, a repeat ask does not grow cache occupancy, and a distinct index inherits nothing. Occupancy is exposed so a hit is proven by execution rather than inferred from two calls agreeing. STILL OWED, stated rather than implied: the lying_substrate_inputs_only_stamp_census denominator is still narrowed, and the remaining ladder gates (bad-A/good-B isolation, exact-identity refusal, zero/one/many binding, no-union execution proof, the 1-selected/1-skipped incident, both G1 mutations, falsifier_red_control_holds) have not been executed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix build: reattach the producer's doc comment to the function, not to a macro CI builds with RUSTFLAGS=-D warnings; my local checks did not, so an unused-doc-comment error reached the branch that no local run could have caught. The thread_local! block for the bound fact substrate was inserted between build_live_read_selection_manifest's doc comment and the function, leaving the comment attached to a macro invocation. The comment was also stale in the same motion, and rewriting it was the fix rather than moving it: it described a whole-tree manifest built once for the entire request set and a producer whose job was to be handed the full roster. Both premises were deleted by the cutover. It now says what the batching is actually for -- the caller passes exactly its cache misses, one lens resolve and one marshal serve them, and the index keeps the rows -- while retaining the arm that matters, that no failure returns a partial batch, because widening the SKIPPABLE set is the under-selection direction and reads as a faster green. Verified against CI's own flag and bin set rather than my previous weaker local command. Two -D warnings errors remain in p1_cohort_probe.rs; they are pre-existing, untouched by this branch, and that bin is not in ci.yml. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix two source-identity defects the first execution found Nothing had ever executed this path; running it found two real bugs, both of the same family -- an identity compared in the wrong spelling. PATH KEYS. The bundle keyed declarations by MultiEntryIndex.source_files' map key, which is the dotted MODULE PATH (std.machine_shape), not a file path -- `source_files.contains_key(module_path)` elsewhere is the tell I misread. The declaration population must be identified by FILE, because that is what a diff touches and what a discovery row names, so identity now comes from sf.path. Both sides additionally go through the index's own `module_index_path_key`, because a raw string compare against the pool is the source-identity fork DESIGN names on this very index: a caller arriving with an absolute path while the pool holds a relative one gets "no such declaration" about a declaration that is plainly present -- a refusal whose cause is the spelling, not the subject. MODULE PATH ON THE FACT. DeclFactRaw carried only the qualified name, which passes through `decl_logical_qualified_name` and DROPS the `v2.` layer prefix for decl_index consumers. fn-arrow reflection keeps the full path, so reconstructing a module by un-stripping that name produced facts under a name no root can bind. The fact now carries its authored module_path unstripped. MEASURED, first execution of the cutover: requests=1 rows=1 fact_modules=3404 fact_decls=61705 parse_refusals=0 lens_closure_sources=579 lens_modules=579 wall_ms=101506 process_rss_mib=12386 The pool is every .dag file including all 1290 tests, and nothing failed to parse, so the population is complete and no union is formed. But removing the union fixed the SEMANTICS, not the price: 101s for one request, because the classification lens's own closure is 579 modules -- nearly the size of the union deleted. That is a finding, not a fix. STILL RED, stated exactly: the subject declaration still reaches the lens as G2RootUnbound. The population contains its file and its module name is right, so the remaining defect is in the projection rather than the walk. It has not been located, and each observation costs a ten-minute run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the record: c8161f32b4e's module_path claim did not land c8161f32b4e's message states "The fact now carries its authored module_path unstripped." That claim is FALSE. The field was never added, the projection never changed, and `git log -S"pub module_path: String,"` over coproduct_reflection.rs returns nothing for any commit. The edit reported success and the build passed, and I recorded a landed fix from those two signals without re-reading the file -- but the ORIGINAL code compiles fine, so a green build was never evidence the edit applied. That is specification-without-execution with the author as the consumer: the artifact looked finished because nothing ran that could tell the difference. It also means run 4's failure was never evidence against the v2.-stripping hypothesis. The fix was absent, so the run re-tested the unmodified code and the hypothesis stayed untested for two cycles. Applying it for real, and proving it by execution rather than by inspection: - DeclFactRaw carries `module_path`, the module's own AUTHORED path, populated at the single construction site in push_decl_facts_from_parsed. - fn_arrow_decl_rows_from_facts reads that field instead of reconstructing the module by stripping the declaration's name off `qualified_name`. That un-strip could not be correct: `qualified_name` passes through decl_logical_qualified_name, which drops the `v2.` layer for decl_index consumers, so the reconstruction filed every v2-authored fn-arrow row under `test.workflow.x` while the root asks for `v2.test.workflow.x`. Every such root reported G2RootUnbound -- not missing, misfiled. Two probes, both green, both fast (36s against the floor's ten minutes): - the_fact_bundle_contains_an_enrolled_witness_declaration proves the bundle holds the exact declaration CI named and binds it to exactly one identity. This is what rules the host side OUT: the population and the binding were never the defect. - v2_layer_facts_keep_the_authored_module_path_and_drop_it_from_the_qualified_name asserts BOTH directions together, because either alone is satisfied by the defect -- with the un-strip in place `qualified_name` lacked `v2.` exactly as it does now, so only the presence of `v2.` on module_path beside its absence on qualified_name discriminates. It also refuses to pass vacuously: it fails if no v2.-authored fact exists at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Decode the produced manifest inside the active context CarrierListAbsent was never a carrier defect. `free_monoid_to_vec` resolves `Empty`/`Cons`/`head`/`tail` against `active_ctx()` and answers None when there is no active context -- so run outside that scope it cannot tell a cons chain from a foreign shape, and reports the foreign one. The decode ran after the producer call returned, i.e. outside the wrapper. The outer row collection concealed this for three rounds because it arrives as a native `Value::List`, which returns before the symbols are ever consulted. The nested carrier lists are real cons chains and are not so forgiving. So the active context is a property of DECODING a produced value, not of the one call that happened to need it first, and it is now scoped to the whole walk (decode_live_read_manifest_rows). Two diagnostic defects made those three rounds cost what they did, and both are fixed here rather than left as the price of the next one: - The refusal named a cause and no SUBJECT. It saw one projection and could not say which declaration produced it, so analysis could not begin without re-deriving the culprit by hand -- a line that stops without locating is half of what §5 asks for. The key is in scope at the row loop, so attribution belongs there. It named `src/v2/lens/module_graph.dag::module_declaration_facts_live` immediately. - The refusal reported what it EXPECTED and never what it RECEIVED, and fused "field absent" with "field present, wrong shape" into one arm -- two states whose repairs share nothing. Split, with the received shape named: the answer came back `Variant::Cons["head","tail"]`, which is a well-formed cons chain and refuted the representation hypothesis I had just spent a round on. An expectation is not an observation. Green by execution, and the receipts are the evidence rather than a counter: three asks over two indexes print exactly TWO [live-read-rows] lines. The repeat roster prints none, so the per-declaration cache hit is observed, not asserted; the distinct index prints its own, so it classified for itself. Cost, stated plainly and unresolved: 275s per cold classification in an unoptimized build (101s release), lens closure 579 modules. The floor is over budget on CI at 3,300,000 ms for this reason, and this commit does not address it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace the quadratic manifest accumulator, and add the missing O(1) cons STEP 1 of the operator's ordered plan, on the exact head rather than in a PR description. The body claimed the manifest accumulator had been changed to a right fold with constant-time prepend. It had not: at b1976f7 `live_read_selection_manifest_over` still left-folded with `list_snoc_item`, whose body is `list_append(left: xs, right: singleton)` and therefore traverses the accumulated prefix on every row. Why the earlier evidence could not see it: the probe that certified this path used ONE request, where the quadratic term does not exist. The ordinary floor builds from a roster of thousands, and the completion receipt is emitted only after the fold and decode -- so the failure presents as zero receipts and 6 executed discovery rows against main's 4728 in the same window, which reads like a route never entered rather than an accumulator that cannot finish. THE ROOT CAUSE IS A GAP IN THE VOCABULARY, not fifteen careless call sites. `list_snoc_item` existed with NO O(1) counterpart. Writing the cheap form by hand means a `Cons` literal, which typechecks as Coproduct(FreeMonoid) and does NOT unify with a branch typed Container(List, T) through the `List` alias -- proven here by execution, since that is exactly the type error my first attempt produced. So the expensive spelling compiled and the cheap one did not, and the census found sixteen snoc-in-fold sites in ONE lens module. `std.algebra` now carries `list_cons_item` beside `list_snoc_item`, named as an item-level operation so the alias asymmetry cannot resurface per call site. Converted in this pass (prepend + one reverse, order-preserving): the manifest fold, `decls_in_modules` (genuinely quadratic in output, on the hot path), `module_facts_for_path`, `decls_with_qualified_name`, `g1_carriers_from_homes`, `merge_carriers` (seeded on a reversed left so the left side keeps its order), `param_names_of`, `positional_child_targets`, `arg_symbols_from_nodes`. NOT converted, and deliberately so: the `fold_node`-composed pair (`atom_collect_step` / `atom_identities_in_node`) and the remaining dedup accumulators. Prepend-plus-reverse is not obviously order-preserving through a node-fold composition, they are not hot-path quadratic (atoms per node are few), and rewriting them on a guess is how a load-bearing lens acquires a silent semantic change. I therefore did NOT enroll this file in the accumulator-copy roster gate. I wrote that enrolment, ran it, and it FAILED at ceiling 0 -- because the sites above remain. Landing an enrolment I cannot pass would be either a red gate or a false claim, so it is withdrawn until the residue is closed. The lens already decides this exact shape (`red_list_snoc_left_is_suspect`), so the control is available the moment the file is clean; it is owed, not invented. Green by execution: all 20 witnesses in live_read_classification_test pass, so the rewrites preserve classification semantics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Locate the cost (steps 2-3), isolate local refusals, and drop the eager roster STEP 2 -- start and phase receipts. The terminal receipt could not distinguish a route never entered, a route entered and stalled, and a route that returned; it reported only the third. That is why the floor's stall showed NO receipt and I read it as "never ran". Every line now carries one invocation identity (subject + pid + request count, so concurrent workers are separable and a per-process counter cannot collide across them), with an unconditional [live-read-start] before any expensive work and a phase end for each of: fact bundle build, lens closure source load, lens resolve/typecheck, eval context, request marshalling, classification production, decode. IT LOCATED THE COST ON ITS FIRST RUN, and not where step 5 expected: lens_closure_resolve_typecheck ms=40468 modules=579 classification_production ms=207790 <- ONE request decode ms=0 The 579-module closure is 40s. The modeled fold is 208s for a SINGLE request. So the dominant term is fact production plus per-request classification -- the batch-grain indexing work -- not the fixed closure. Recorded here because two cost readings on this lane were already wrong from argument rather than measurement. STEP 3 -- stop classifying rows whose verdict G2 cannot change. Selection is a disjunction of independent do-not-skip axes and every other axis is a fact lookup. A row already forced to run cannot have its verdict changed by a live-read classification, so classifying it is cost paid before the first discovery row executes. Three call sites now consult G2 LAST (semantics identical -- `||` is commutative, ordering only decides what is evaluated), and the context is built over candidates only, counted in a [live-read-candidates] receipt rather than narrowed silently. `entry_blocked_by_cheap_axes` is the one definition of "already decided"; a second copy could drift into classifying needlessly or withholding a classification a consumer then asks for. LOCAL FAILURE ISOLATION. `live_read_rows_for` returned Err for the whole batch on one unbindable request, beneath a comment asserting the refusal was local -- the two disagreed for as long as nothing executed the case. An unbindable request is now a Refused row: the batch keeps classifying, and the floor still refuses to skip, because the consumer already reads Refused as do-not-skip. So isolation costs no fail-closed strength. Not cached -- the durable cache is keyed by resolved declaration identity and an unbindable request has none. The control asserts BOTH halves, since either alone is satisfied by a defect: answering for A would be fail-open, and refusing for A while dropping B is the abort being repaired. Green by execution. Also fixes a second site of the module_path defect: bind_live_read_request still derived the module by un-stripping the qualified name. Same fork as the fn-arrow projection, one call away. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Apply the candidate filter where the run actually builds the context The phase receipts from the previous commit did their job on their first CI run, and what they showed is that my step-3 filter was on a path this run does not take: [live-read-start] requests=8538 phase=fact_bundle_build ms=0 modules=3450 decls=62767 phase=lens_closure_source_load ms=25 sources=587 phase=lens_closure_resolve_typecheck ms=7367 modules=587 phase=eval_context_construction ms=59 phase=request_marshalling ms=5 requests=8538 <no classification_production end> Three things are now located rather than inferred. The stall is in classification_production. The fixed closure is NOT it -- source load plus resolve is 7.4 seconds here, against a 55-minute budget. And 8538 requests entered that fold, so the candidate filter never ran: no [live-read-candidates] line appears anywhere in the log. The site that builds it is `run_discovery_corpus_with_options_inner`, which ran before `run_discovery_rows` and built from the COMPLETE roster under a comment declaring that to be the design: "First consumer of the manifest in the run, and it is handed the COMPLETE roster -- the index-scoped memo it fills is what every later decision reads." That convention outlived its mechanism. It was true of an immutable whole-roster manifest built once; it has been false since the cache became per-declaration and incremental, which disjoint-roster use forced. Nothing downstream needs priming -- a later caller asking about a row this one skipped classifies it then. So the comment was not merely stale prose: it was the live justification for putting every enrolled row into one classification. `live_read_candidate_rows` is now the single definition, used at all three build sites, and the inline copy in `run_discovery_rows` is deleted rather than left to drift from it. The struct doc that chartered the convention says what replaced it and why, and the `LiveReadEntryAbsent` refusal no longer instructs the reader to build from the complete roster -- callers ask about their own demand, so an absent entry means it was not among THIS view's rows, not that a roster was incomplete. This does not fix the quadratic in the fold. It stops feeding it rows whose verdict it cannot change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The short-circuit has to hold at every consumer, not only the predicates The filter worked, and the measurement is unambiguous: [live-read-candidates] roster_rows=8545 candidate_rows=91 excluded=8454 phase=classification_production ms=287414 <- COMPLETED, 91 requests phase=decode rows=91 A 94x reduction in requests, and the classification RETURNS instead of never finishing. Two further facts fall out of the same receipt: the fixed closure is 6639 ms of a 55-minute budget, so step 5 was never the target; and 287 seconds for 91 requests is still ~3.2 s/request, so the quadratic in the fold is untouched and remains the next thing to fix. The run then failed differently, and correctly: AFFECTED-SET REFUSAL cause=LiveReadEntryAbsent entry=dag/test/claim/accelerator_demo_execution_witness_test.dag That is the exact risk excluding rows creates, and it fired at a consumer I did not convert: the first site built the view from candidates and then handed the COMPLETE roster to discovery_rows_runtime_dependency_touched_count beside it, which asks the view about each row. So it asked about rows the view was deliberately not built for. Fixed by passing the candidates there too. The count's meaning narrows, and that is worth stating rather than burying: it is now "among entries whose verdict a live-read answer can still change, how many have a touched runtime dependency". Excluded entries are not uncounted -- they are already forced to run by the axis that excluded them, and counting them here would count one entry under two axes. Every remaining production consumer is guarded: the two entry predicates and the fast-skip predicate all consult G2 last, after the cheap axes have returned early. The one unguarded `row_for` loop is a test that builds its own context from the rows it asks about. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Recut the candidate filter as one typed selection plan Findings 2, 3 and 4 from the review. Finding 1 (precompute iterating the full roster) was already fixed at 36be85d9cbc, before the review landed. THE ROOT DEFECT WAS THE REPRESENTATION, exactly as called. A sparse context gives one representation to two states with opposite remedies: "absent because another axis already decided" is correct and must be silent, while "absent because the classification is missing" must refuse. With only a context every consumer sees LiveReadEntryAbsent for both -- which is why filtering the context alone moved the failure from the stall to a refusal instead of fixing it, and why chasing it consumer-by-consumer would never have terminated. `LiveReadSelectionPlan` carries `AlreadySelected { cause } | NeedsClassification` per entry beside the classifications for the candidates only. `entry_must_run` answers an AlreadySelected entry from its own cause WITHOUT consulting G2, so an excluded row is unqueryable rather than a lookup that happens to refuse. An entry the plan never saw is a real gap and refuses with a distinct cause (LiveReadEntryNotPlanned) -- the plan must not become a way to make every absence silent, which would be the same conflation inverted. FINDING 2 -- post-resolve accounting. resolve_discovery_entry_for_corpus_row short-circuited only on the declared/effect half, so a row excluded for any OTHER cheap reason (ReadsLiveTree, direct touch, edited test fn, import closure, stop line, data-item overlap) still reached G2 after resolve. It now goes through the plan. The runtime axis is not faked false for excluded rows; AlreadySelected answers true, which is the honest do-not-skip verdict rather than a claim about an axis nothing evaluated. FINDING 3 -- the categorization site. eprintln_affected_set_categorization still built directly from the full roster and could independently recreate the 8538-request classification the execution sites had just stopped making, moving the stall to another consumer. It consumes the plan now. measure_selected_entry_closure_overlap is classified deliberately rather than missed: it is an OFFLINE whole-population measurement whose subject IS the full roster, so filtering would change what it measures, and it says so in place. FINDING 4 -- the duplicated chain. entry_qualifies_for_skip_without_resolve and entry_eligible_for_discovery_skip_before_resolve each repeated the disjunction inline; both now call entry_blocked_by_cheap_axes. Two independently writable copies of one rule only have to disagree once to produce either a refusal or the restored cost. The authority returns a typed CheapAxisCause rather than a bool, so the plan can preserve WHY G2 was omitted instead of consumers re-deriving it. Controls, green by execution (465s, serial): - every_cheap_axis_excludes_without_the_classification_being_consulted: one arm per exclusion reason, asserting BOTH the expected cause AND entry_must_run == true. Either alone is satisfied by a defect -- an arm checking only the cause would pass while the entry silently became skippable. - an_unplanned_entry_refuses_rather_than_reading_as_already_selected. - the local-isolation control from the previous commit still passes. The fixture constructor for plans is cfg(test): minting demands without deriving them from the cheap axes is precisely the forgery the plan prevents, and it must not exist on a production route. Not addressed here, and still the dominant term: the per-callee 579 x ~62,000 scan inside every candidate. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Prove zero candidates cost zero classification; group_by is blocked upstream ZERO-CANDIDATE CONTROL (merge bar item). Candidate filtering reduces the number of REQUESTS through the fold; it does not by itself remove the ~7s fixed startup, because a context built unconditionally resolves the ~587-module lens whether it has one candidate or none. "The roster filter appears to work" and "the run stopped paying for the classifier" are different claims and only the second is asserted here. Asserted on a COUNTER, not on stderr: a test that greps its own output proves a line was printed, not that work was skipped. `LIVE_READ_CLASSIFICATION_INVOCATIONS` counts the expensive unit -- one lens resolve plus one modeled fold per `build_live_read_selection_manifest`. It also supplies the width-1/width-2 invocation count the merge bar asks for, which is otherwise unfalsifiable from outside the process. The control also asserts the plan stays USABLE at zero classifications: an excluded entry still answers `entry_must_run == true` from its own cause. Zero classification must not mean zero answers, which is the fail-open direction the filter could have introduced. GROUP_BY: BUILT, MEASURED AGAINST THE SUBSTRATE, REVERTED. The native multiplicity-preserving arm compiles and the roster/regeneration path accepts it, but it is NOT REACHABLE FROM AUTHORED .dag. The witness refuses at typecheck in both spellings: method 'group_by' not found on receiver type 'Container(List,...)' function 'group_by' not found in scope and -- the decisive part -- `index_by` refuses IDENTICALLY, though it is an established interpreter arm. So this is not a missing registration for my new primitive; the whole family is unreachable from authored source and exists only for emitted-Rust/internal paths, which is why no .dag module calls it. Making it usable needs primitive REGISTRATION, and DESIGN already names why that is not a one-line addition: the primitive subject universe is forked across infer_method's builtin registry, std.primitives PrimitiveContract rows, std.algebra templates, the native interpreter arms, and per-target emit handlers (the determinism thread's closed-denominator gap). That is substrate work with its own sequencing, not a lens patch. Landing the arm anyway would be machinery no consumer can reach -- the inert mechanism DESIGN calls coverage by illusion -- so it is reverted rather than left in the tree with a note. The dispatch table is regenerated back to `group_by`-free through the supported path, not hand-edited. The per-callee 579 x ~62,000 scan is therefore still unfixed, and the route to fixing it now has a named upstream blocker rather than an unknown. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist the closure restriction out of the per-callee scan decls_matching_callee called decls_in_modules itself, filtering ~62000 declarations against 587 closure modules once per callee of every reached declaration. Nothing in that filter depends on the callee. The caller now restricts once and threads the restricted list. Same set by construction: filter(filter(xs, in_closure), named) == filter(filter(xs, named), in_closure), so no classification changes. 20 lens witnesses green in 8259ms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Land group_by as a real primitive, and normalize index_by beside it The lens needed a name-keyed declaration index and the substrate had no operation that could build one. index_by is a native HAMT but last-wins, so it drops homonyms; the modeled Map is a closure chain, measured 33x slower than the linear scan it would replace. Neither was reachable from authored .dag in either spelling. One atomic cut, on the shape empty_map already established: a typed public group_by<T,K>(List<T>, fn(T)->K) -> Map<K,List<T>> backed by a private group_by_primitive_delegate intercepted at the collection-native grounding seam, plus the same normalization for index_by. Multiplicity-preserving: every item reaches its key's bucket, buckets keep input order. Surfaces, all in this commit: std.primitives contract (work n x (key_fn_work + expected HAMT insertion), certainty Expected), std.primitive_identity definition/alias/traversal/cost rows, the interpreter roster row and its regenerated dispatch table, the native handler, rc_group_by in runtime_rust.dag and v1_rt.rs, and the rust emit registry row. The grounding seam now threads env, because both grouping delegates apply a caller closure; eval_builtin has no env and the builtin-backed arms keep their own path. A missing native binding refuses rather than falling back - the delegate's body is its own name, so a fallback would be an unbounded self-call. Witnesses green by execution: 6 in test.claim.grouping_primitive_witness (empty, unique key, three equal keys in one bucket, input order, absent key, and index_by keeping the last item). The two multiplicity claims are the discriminating pair a last-wins mutation reds. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the stage0 seed for the group_by emit surface The rust emit registry row and the runtime function both live in .dag authorities that generate seed files; hand-editing v1_rt.rs left the generated emitter and the registry stale, and regen refused with a three-file fixed-point mismatch. Two regen rounds were needed and the reason is the bootstrap order: the first round emits v1_rt.rs with the OLD compiled-in v1_compiler_runtime_rust while writing the new one, so rc_group_by is dropped from v1_rt.rs and added to its emitter in the same pass. Rebuilding and regenerating converges. Also adds a stopped-line audit hook to the live-read producer: with the forensics env var set it dumps per-.dag-fn self time after classification production. It reports and never decides. It is there because the grouped index did NOT move the measured number - classification production is 216427 ms for 2 requests against 207790 ms before - so the dominant term is something other than the per-callee scan and needs a name rather than another guess. Population measured at the seed and now printed with the fact-bundle phase: 61977 declarations, 59218 distinct names, largest bucket 1018. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Stop materializing strings and lists to hash them Forensics on the live-read producer named the dominant term: 73315126 free_monoid_to_vec calls materializing 3251118183 items, every one of them from the single site inside value_hash. Hashing a Value::Str allocated one Value::Int per character and hashing a Value::List cloned every element, walked the clone, and threw it away - and every HAMT key in the interpreter goes through that path. Both arms now hash in place. The result is identical by construction: same 0xF0 tag, same length, same per-element value_hash in the same order, which is exactly what the walk over the materialized vector did. A Cons chain still materializes, because walking it needs the monoid symbols resolved and there is no borrowed view of it. Controls, green by execution: the replaced implementation is kept in the test as the oracle and asserted equal on empty/one-char/path/non-BMP strings and on empty and mixed lists, paired with a discriminating control that distinct strings and permutations still hash apart, so a constant would fail. Measured on the two-request producer: classification production 216427 ms -> 167213 ms. Real, and not the whole term - the remaining cost is still inside the edge producer's two folds and gets measured next rather than guessed at. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the remaining term: ExprCall, at 389 microseconds per evaluation Three forensics-gated counters, each of which answered a question that was otherwise a hypothesis, and one of which REFUTED one of mine. The stack-segment probe: 1089374 probes, 0 under the red zone. stacker never grows a segment on this workload, so the 8 MiB-per-call theory is dead. The zero is kept as the receipt. The node-evaluation counter: 4423731 evaluations for a 173-second phase, which prices ONE evaluation at ~39 microseconds. That is a per-node cost, not a node-count problem - so no amount of work on WHAT the lens computes was ever going to move it. The per-variant profile, using the interpreter's existing GUNBC_INTERP_PROFILE instrument rather than a fourth counter, locates it exactly: ExprCall 434702 evals 169227ms self 389295ns/eval 97.8% ExprRecordLit 793655 evals 1515ms self 1909ns/eval ExprVar 2610850 evals 643ms self 246ns/eval Self time excludes the callee body and the argument nodes, both of which are child evaluations. So 389 microseconds is spent per call in the call machinery itself, and everything this lane touched - the grouped index, the hoist, the accumulator - was optimizing terms three orders of magnitude below it. Reports only; no production behavior changes here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make the hash oracle independent, execute it in CI, and delete the probes Three repairs from review, in the order they depend on each other. THE ORACLE WAS NOT INDEPENDENT. reference_materializing_hash recursed through the PRODUCTION value_hash, so it checked only the outermost string/list layer: a drift appearing solely inside a nested list would have been shared by both sides and stayed green. Since value_hash decides HAMT key identity, that drift changes grouping, lookup and cache behaviour with no type error anywhere. The oracle is now a complete recursive copy of the replaced implementation -- reference_materializing_hash and reference_hash_fields_commutative are mutually recursive and call no production code -- over 24 specimens: empty and ASCII and multi-byte strings, empty list, list of primitives, list containing a list, list of strings, record and variant carrying nested lists, a Map, a Set, and the i64 boundaries. The discriminating half now also asserts the ORACLE separates the same pairs, so a degenerate oracle fails too. THE CONTROLS WERE COMPILED, NOT EXECUTED. The build job runs cargo test --no-run, which proves compilation and runs nothing, so every #[cfg(test)] control in the v1-compiler lib had never executed -- specification without execution. A second build-job step now runs exactly the two named modules: -p v1-compiler --release --lib, two filters, --test-threads=1 because the parity control reads process-global interpreter state. Deliberately NOT the whole lib suite: the heavyweight producer module resolves the live tree and has been observed to exhaust memory as a group, so enrolling everything would trade an unexecuted control for an unreliable job. Two witnesses keep the two claims apart, and the RED half fails if the execution step ever acquires --no-run. THE PROBES ARE DELETED, NOT KEPT. record_node_eval ran on every expression evaluation and record_stack_probe on every dag-fn call and closure application. Both were investigation instruments and both have delivered: 1089374 stack guards with ZERO below the red zone (segment growth refuted), and 4423731 node evaluations pricing one eval at ~39 microseconds. Leaving a call and a branch on the hottest path in the compiler would be permanent residue charged to the cost they were built to measure, so the receipts stay in the commits that took them and the code goes. Green by execution: 5 interpreter controls, 2 step witnesses; ci.yml regenerated. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the measured value_hash A/B receipt (Cut 1 step 5) Both arms unprofiled, same exact classification subject, same binary shape: arm classification_production live-read wall cpu RSS control 218738 ms 313266 ms 312468 ms 7195 MiB candidate 182038 ms 274597 ms 273853 ms 7183 MiB Streaming the hash is 36.7 s (16.8%) cheaper on the classified term and 38.7 s on the whole read, at identical resident cost and identical rows (requests=2 rows=2 in both arms). The fixed prelude reproduced across arms (17.4/17.7 s fact bundle, 36.7/35.7 s source load, 40.4/39.0 s resolve+ typecheck), which is what makes the pair comparable rather than two samples of host noise. The receipt also RETRACTS the earlier 216 -> 167 s reading: those were single runs on a host whose run-to-run variance on this phase is tens of seconds, so only the paired arms above are quotable. classification_production stays far above the fixed lens resolve/typecheck term, so the operator's stop rule does not fire: this repair removed one measured term, it did not move the dominant cost. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Mark the interpreter-parity CI shell transport as a scaffold with a dissolution trigger The compile gate carries ci_v1_compiler_tests_compile_gate_shell_emit_scaffold plus a named dissolve-on trigger, rendered as a comment on its emitted GitHub Actions run:. The interpreter-parity step added a second foreign-executor run: path over the same seam with neither, so a new shell transport landed unmarked and uncounted. Add the sibling pair. The trigger states what the compile gate's does not: this is the SECOND consumer of one seam rather than an independent transport class, so it dissolves with it under shell-to-intent Phase 2, and it joins the srvN STEP 2 population already tracked for the shared EAGAIN retry arm. The marker is emitted, not merely modeled. ci_interpreter_parity_controls_run_script renders the trigger the same way the compile gate does, and two witnesses execute: the carrier is a Scaffold, and the emitted run script actually carries its trigger text. The second is what keeps the disposition from being an inert registration - a row nobody emits would be registration mistaken for enforcement. ci.yml regenerated: one added comment line, no other artifact churn. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Build the live-read selection plan once per index, not once per entry group The floor refused at its 55-minute population budget on 1eb10b48f29 with no witness failing. The log names the cost: [live-read-candidates] printed 719 times, every one reporting the identical roster_rows=8563 candidate_rows=91 excluded_by_cheap_axes=8472. Summed gap preceding those lines is 17.6 minutes of a 70.3-minute job, median 1.41s each. run_discovery_rows is called once per queued entry group inside each worker's loop, and it built LiveReadSelectionPlan over the COMPLETE roster on every call. Roster, index, diff and changed paths are all invariant across the groups one worker processes, so 718 of those 719 builds recomputed an answer that could not differ. The code had already caught this class one call site over: the narration site carries a comment saying "THROUGH THE PLAN, not a second full-roster build -- it could independently recreate the 8538-request classification the execution sites had just stopped making, moving the stall from one consumer to another." The worker-group site is that same mistake, unfixed. The plan is per-INDEX, not per-run: a manifest carries the subject of the index that produced it and each width>1 worker builds its own MultiEntryIndex, so the main thread's plan would refuse on subject mismatch at every lookup, correctly. Per-index is therefore the strongest sharing the subject identity permits. live_read_selection_plan_for_index is the single build site, called where each index is built, and run_discovery_rows now takes the prebuilt plan instead of the roster -- so the per-group rebuild is not merely removed, it is unwritable from there: the roster it would need is out of scope. The rationale comments that documented the removed build move onto the helper rather than being deleted with it. NOT CLAIMED: that this greens the floor. 70.3 - 17.6 leaves ~52.7 minutes against a 55-min…
briansrls
pushed a commit
that referenced
this pull request
Aug 16, 2026
… getting from the pool (#8326) * Unbreak the whole-tree compile: name the import three call sites were getting from the pool v2.lens.live_read_classification carries no import block and calls witness_import_closure at three sites. Those resolved only when some unrelated module elsewhere in the assembled closure had already pulled v2.lens.witness_cost_locality in - the pool-membership coincidence DESIGN records as the import-strip Class B failure. Under a whole-tree compile no module does that, and all three refuse. MEASURED, both directions, at origin/main 87513a53e8: without this change gunbc compile --target dag exit 1, 3 blocking errors with this change gunbc compile --target dag exit 0, 0 blocking errors The call sites are unchanged; this names where the function comes from, from the definer, exactly as v2.lens.effect_reach already does for the same function. Why this stood since 2026-08-08 (#7997): per-PR compile-clean is scoped to the affected import closure, and this module is outside most PRs' closures. The whole-tree baseline is what any PR touching a non-selectable path would have hit. * Import the module_graph functions too: one import block governs the whole module The first commit added one import and broke a green witness. That is the Class B failure inverting, and it is worth stating because it makes the class harder to fix than it looks: while live_read_classification carried NO import block, every bare cross-module reference resolved from the pool. Adding one import made the module import-governed, so path_matches_touched - which had been resolving the same accidental way - stopped resolving, and g2_roster_gate_literal_path_touched_selects failed at runtime. MEASURED, and the split matters: the whole-tree compile reported only witness_import_closure. path_matches_touched resolved at COMPILE time and failed at RUNTIME, so the compile gate could not have caught this and did not. Only executing the witness did. The consequence for the namespace-cut lane: a module with bare references cannot be repaired one import at a time. The first import is the breaking change, and every reference the pool was supplying has to be named in the same commit. All four names this module takes from v2.lens.module_graph are now imported from the definer. live_read_classification_test: 20 of 20 green by execution, including the witness that regressed. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com>
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.
DRAFT — DO NOT MERGE. Steps 1–4 of a 7-step sequence. The seed still decides from the G1-only interim until the manifest lands, so merging this state leaves the
.dagauthority disagreeing with its only consumer, the falsifier red, and its corpus not executing.Retitled from a simplification framing: this is a safety repair, and the previous description claiming downstream classification was maintained is not accurate.
What is broken
The affected-set falsifier's
falsifier-buildjob fails, and while it fails the corpus never runs — so the falsifier provides zero coverage, not merely a red badge.Clean-main axis trace for the unrelated entry B (
affected_set_floor_runner_test.dag) isolates one firing axis:runtime_data_dependency_touched_via_carrier_closureconsultstouched_pathsonly as a nonempty guard, then answers from carrier-home reachability alone. An entry with a 474-module closure is therefore unskippable on any nonempty.dagdiff. This is the documented G1-only interim (live-read-witness-classification-design.mdP2) — not a regression from #7933, whose stop-line channel the trace rules out.Landed so far
LiveReadSelectionProjection(Classified|Refused) inv2.std.live_read. Without a refusal arm, an unavailable G2 producer silently answersLocalRead— under-selection, which presents as a faster green floor rather than a failure, and is strictly worse than the over-selection being repaired.call_reachable_declsseeded every function in the entry file;call_reachable_decls_from_rootseeds the exact enrolled declaration. A manifest keyed per declaration with per-file values would imply precision it lacks.g2_union_retains_g1_import_carriers_with_g2_literal_paths.Two controls that tested nothing
Recorded because the pattern is the finding, not either instance.
The two CI failures on this branch were not collateral damage — they were the union's cover being removed. Both asserted a conclusion their facts could not support: their subject's closure does not contain the carrier homes their fixture facts name, so
fn_arrow_decl_facts_live()returns no declarations for them and no reachability evidence exists in that context. G1 supplied the carriers unconditionally, so they passed without the evidence ever being available.Separately, planted control 3 emitted its callee fully qualified (
v2.compiler.self_host.carrier_fn) whiledecls_matching_calleecompares the baredecl.name. The planted carrier was never call-reachable; the control typechecked and would have reported success while exercising no reachability edge.Both passed ordinary runs. Only execution and mutation exposed them.
Remaining before ready
dependency_resolution_facts_live→ModuleDependencyEdge(+ModuleDeclarationFact,FnArrowDecl) as the live boundary;ModuleImportFactstays fixture-onlyCompleteForSubject{index/tree identity}vsIncompleteOrUnbound{cause}MultiEntryIndex, subject-mismatch refusing2 selected / 1 expectedInfrastructure changes are deliberately excluded from this PR.
🤖 Generated with Claude Code
https://claude.ai/code/session_012DrzU3z7PJzhN5mxvZAfAs