Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 26 additions & 4 deletions dag/gunbc/keyed_declaration_read_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -53,13 +53,35 @@ import std.decl_ref { DeclarationRef, WholeDeclaration }
// projects std.primitive_projection. Each was edited by hand in the same change as its authority
// because the seed cannot build the emitter that regenerates it without them -- the ordinary
// stage0 bootstrap seam, not new hand growth.
// A THIRD ITEM JOINED THIS RECEIPT LATER (gunbc#11291), and it is enumerated here rather than in a
// parallel justification because it is the same seam narrowed along a different key.
// eval_type_declarer_qualified_names is the BARE-NAME sibling of eval_decl_facts_at: same census,
// same decl_facts_for_roots_shared memo, same pool-root line-stop, same canonical order inherited
// rather than chosen. It exists because the keyed read already here CANNOT express its question --
// decl_facts_at keys on a QUALIFIED name and a bare spelling has no module -- so the only substrate
// answer was to fold the whole declaration corpus once per call, measured at ~3.6s against ~1ms for
// the keyed read and sharing at no grain, four calls in one claim frame costing four times one.
// That is recorded as a third specimen on
// gunbc.recurring_failure_mode.shared_precondition_re_derived_once_per_claim_frame.
//
// ITS CORRECTNESS CONTENT IS THE SAME ONE THE ROW ABOVE NAMES, which is why it belongs beside it:
// it returns the MATCHING SET -- every qualified name declaring that bare spelling as a type -- and
// never a first hit, because multiplicity is the whole answer. A host that chose among candidates
// would be the bare-name identity defect its consumer exists to remove, one layer below the one
// being removed. Its consumer is v2.std.node_reflection type_declarer_names, reached by both guarded
// routes -- resolve_type_node and resolve_type_node_at -- each of which refuses typed and
// located on multiplicity and names its candidates from what this returns.
//
// It marshals no declaration nodes, which is where the population read's cost actually lived; it is
// therefore cheaper than eval_decl_facts_at rather than merely narrower.
data keyed_declaration_read_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.coproduct_reflection", decl_name: "eval_decl_facts_at", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.entry_resolve", decl_name: "module_declaration_fact_at", field: WholeDeclaration }
DeclarationRef { module_path: "v1_compiler.cli_run.entry_resolve", decl_name: "module_declaration_fact_at", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.coproduct_reflection", decl_name: "eval_type_declarer_qualified_names", field: WholeDeclaration }
],
reason: "A keyed read of a host census is a property of the host that holds it. Both items are the keyed projection of a population read that already exists beside them, and each is its own item because each answers for a different census: eval_decl_facts_at over the declaration facts, module_declaration_fact_at over the module-path index.\n\nTHE RETURN SHAPE IS THE CORRECTNESS CONTENT. eval_decl_facts_at returns the MATCHING SET rather than a bool or a first hit, because multiplicity is what DeclarationRefAmbiguous is derived from -- two rows under one logical qualified name is an ambiguous citation, and a keyed read that collapsed it would silently RESOLVE one. That is not a cost defect, it is a wrong answer, and it is the reason this item is enumerated rather than treated as an inlined filter. module_declaration_fact_at returns an Option because the two questions a keyed caller asks -- is this module declared, and at which path -- are one lookup, and answering only the first would send the second back through the population read.\n\nEXECUTING EVIDENCE, not a shape argument: test.claim.decl_ref_keyed_read_agreement_witness_test asks one reference BOTH ways over one pool and requires the two feeds to land on the same arm AND names which arm, across all five, with the ambiguous arm reached at multiplicity two from a real duplicate-qualified-name fixture pool rather than a synthesized fact list.\n\nENUMERATED RATHER THAN COUNTED. Both are free functions, so the citable count and the real count are both two; nothing lands in seed_growth_uncitable_item_keys. The interpreter arms and the modified existing items are disclosed in this file's header instead.",
reason: "A keyed read of a host census is a property of the host that holds it. Both items are the keyed projection of a population read that already exists beside them, and each is its own item because each answers for a different census: eval_decl_facts_at over the declaration facts, module_declaration_fact_at over the module-path index.\n\nTHE RETURN SHAPE IS THE CORRECTNESS CONTENT. eval_decl_facts_at returns the MATCHING SET rather than a bool or a first hit, because multiplicity is what DeclarationRefAmbiguous is derived from -- two rows under one logical qualified name is an ambiguous citation, and a keyed read that collapsed it would silently RESOLVE one. That is not a cost defect, it is a wrong answer, and it is the reason this item is enumerated rather than treated as an inlined filter. module_declaration_fact_at returns an Option because the two questions a keyed caller asks -- is this module declared, and at which path -- are one lookup, and answering only the first would send the second back through the population read.\n\nEXECUTING EVIDENCE, not a shape argument: test.claim.decl_ref_keyed_read_agreement_witness_test asks one reference BOTH ways over one pool and requires the two feeds to land on the same arm AND names which arm, across all five, with the ambiguous arm reached at multiplicity two from a real duplicate-qualified-name fixture pool rather than a synthesized fact list.\n\nENUMERATED RATHER THAN COUNTED. All three are free functions, so the citable count and the real count are both three; nothing lands in seed_growth_uncitable_item_keys. The interpreter arms and the modified existing items are disclosed in this file's header instead.\n\nTHE THIRD ITEM, eval_type_declarer_qualified_names, is the bare-name sibling of eval_decl_facts_at over the SAME census and the same memo, added because a qualified key cannot express bare-name multiplicity. It carries the same return-shape law for the same reason: it answers with every qualified name declaring the spelling as a type, so its consumer can refuse on multiplicity and name its candidates, and the host never picks among them. The header records the measurement that admitted it.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete both when the declaration census is a MODELED operation over a modeled prepared inventory rather than a host walk -- at which point a keyed read of it is an ordinary modeled query over a modeled collection and needs no host producer at all. This receipt dissolves with gunbc.decl_facts_shared_memo_seed_growth and gunbc.census_memo_seed_growth and not before: they are one seam, and retiring the memo while its keyed reader stayed hand-written would leave the reader keyed on a population nothing models.",
current_boundary: "Two pure functions of their declared arguments, each reading one already-built artifact and holding nothing. eval_decl_facts_at consults decl_facts_for_roots_shared -- the same census, the same canonical key over the pool-root multiset, the same shared-artifact fill accounting -- and filters DeclFactRaw rows on exact qualified_name equality, which is the law v2.std.decl_facts_skeleton decl_facts_matching_qualified_name already carries on the interpreted side; it therefore inherits the population read's CanonicalOrder rather than choosing one, because a filter cannot reorder what it does not rebuild. module_declaration_fact_at reads build_module_path_index, which was already process-cached before this change. Neither adds state, and neither can answer where the population read refuses: the pool-root defect line-stop fires first in both, against the DECLARED roots, because an empty keyed answer is exactly what a genuine miss looks like and the two must stay distinguishable. What they do NOT bound is the demand: a fold over N citations makes N keyed calls, so the census provider must retain across them, which is why claim_batch registers the census for its invocation and why gunbc run -- whose dispatch diverges and so cannot clear -- is deliberately left unregistered with no keyed consumer reached through it."
trigger: "Delete all three when the declaration census is a MODELED operation over a modeled prepared inventory rather than a host walk -- at which point a keyed read of it is an ordinary modeled query over a modeled collection and needs no host producer at all. This receipt dissolves with gunbc.decl_facts_shared_memo_seed_growth and gunbc.census_memo_seed_growth and not before: they are one seam, and retiring the memo while its keyed reader stayed hand-written would leave the reader keyed on a population nothing models.",
current_boundary: "Three pure functions of their declared arguments, each reading one already-built artifact and holding nothing. eval_decl_facts_at consults decl_facts_for_roots_shared -- the same census, the same canonical key over the pool-root multiset, the same shared-artifact fill accounting -- and filters DeclFactRaw rows on exact qualified_name equality, which is the law v2.std.decl_facts_skeleton decl_facts_matching_qualified_name already carries on the interpreted side; it therefore inherits the population read's CanonicalOrder rather than choosing one, because a filter cannot reorder what it does not rebuild. module_declaration_fact_at reads build_module_path_index, which was already process-cached before this change. Neither adds state, and neither can answer where the population read refuses: the pool-root defect line-stop fires first in both, against the DECLARED roots, because an empty keyed answer is exactly what a genuine miss looks like and the two must stay distinguishable. What they do NOT bound is the demand: a fold over N citations makes N keyed calls, so the census provider must retain across them, which is why claim_batch registers the census for its invocation and why gunbc run -- whose dispatch diverges and so cannot clear -- is deliberately left unregistered with no keyed consumer reached through it.\n\neval_type_declarer_qualified_names sits inside every sentence above with one narrowing and one widening. It consults the same decl_facts_for_roots_shared census under the same canonical key and the same pool-root line-stop, and it filters DeclFactRaw on exact bare-name equality AND TypeItem kind rather than on qualified_name -- a different key over the same rows, not a different census. The widening is that it does NOT reach eval_decl_facts_rows at all: it marshals no declaration nodes and returns only qualified-name strings, so it is strictly cheaper than the row it is keyed beside and cannot inherit a marshalling defect from it. The narrowing is that it answers for TYPE declarations only, because that is the question its consumer asks; a caller wanting another kind would need its own key rather than a widened arm here."
}
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ data host_seam_self_call_diverges_when_its_arm_is_absent: RecurringFailureMode =
"WHY THE COMPARISON COULD NOT SEE IT, recorded because the next investigator will reach for the same instrument: two heads with one binary separates 'this head regressed' from 'nothing' only if the binary is sound. Where the binary carries the defect, the honest control needs a second ARTIFACT, not a second head. Three lanes matching one signature in two days was already the stronger inference and was available before the false report. ",

"UNCERTAINTIES CARRIED, ONE OF THEM NOW DISCHARGED AND SAID SO HERE RATHER THAN LEFT STANDING BESIDE ITS ANSWER. This row used to carry, as its first uncertainty, that the specimen execution was a lane report and that no pre-#11121 binary had been run against it: the two-binary discrimination above did exactly that run, on a corpus head held fixed, so that uncertainty is closed and the mechanism no longer rests on a source reading alone. What remains uncertain is unchanged. The emitted-path claims are taken from `symbol_lexeme_seam_disposition_note`, the identity-form realization now in `v1_compiler.v1_rt`, and the resolver's stated suppression behaviour, not from an emission run performed for this row; that the two UNROSTERED self-call sites are absent from the emitted seed is a read of `src/v1` at f9d37e43a1, and whether an emission run that reached them would confirm a compiled self-call was not established by execution here. The denominator is a regex over first-expression self-application; a self-call reached through a `let` or a nested expression would be missed by the search and is not claimed absent.",
"ONE OF THE THIRTEEN IS GONE RATHER THAN CLIMBED, recorded by another lane (gunbc#11291) so the denominator above is not read as still current. `v2.std.node_reflection` resolve_type_node was one of the two self-call declarations this row names as having an interpreter arm and NO projection row -- the state it calls PROSPECTIVE exposure. It was not given a projection row and it did not climb: it was DELETED, together with its roster arm, its interpreter family arm, and the host functions beneath it (eval_resolve_type_node and the type_item_by_name scan), because a scope-carrying replacement left it with no consumer. So the count this row states is correct as OBSERVED on 2026-09-12 at f9d37e43a1 and is one lower afterwards, and the remaining member of that pair is `v2.std.data_index` data_init_decl_facts_live alone. The row is not re-swept here, because a lane that deletes one member is not thereby entitled to restate another lane's census.",

],

evidence: [
Expand All @@ -45,7 +47,6 @@ data host_seam_self_call_diverges_when_its_arm_is_absent: RecurringFailureMode =
DeclarationRef { module_path: "std.primitive_projection", decl_name: "primitive_projection_roster", field: WholeDeclaration },
DeclarationRef { module_path: "std.primitive_projection", decl_name: "symbol_lexeme_seam_disposition_note", field: WholeDeclaration },
DeclarationRef { module_path: "gunbc.v1_interpreter_primitive_surface", decl_name: "v1_interpreter_primitive_arms", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.node_reflection", decl_name: "resolve_type_node", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.data_index", decl_name: "data_init_decl_facts_live", field: WholeDeclaration },
DeclarationRef { module_path: "gunbc.recurring_failure_mode.dispatch_correctness_resting_on_arm_order", decl_name: "dispatch_correctness_resting_on_arm_order", field: WholeDeclaration },
DeclarationRef { module_path: "gunbc.recurring_failure_mode.unresolved_callee_conflated_with_dispatched_elsewhere", decl_name: "unresolved_callee_conflated_with_dispatched_elsewhere", field: WholeDeclaration },
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,14 @@ data interpreted_run_accepts_what_the_floors_resolve_refuses: RecurringFailureMo

"SPECIMEN, gunbc#11026, 2026-09-11, both observations first-hand. `dag/std` distinguishes `List` from `FreeMonoid`: `[]` with `concat([x], acc)` builds the first, `Empty` with `Cons` the second, and a new module mixed them. `claim_batch --entry` over that tree resolved the entry -- reported 168 modules, 6554 resolved items -- and ran eight witnesses to PASS, including the discriminating ones. The required floor refused the SAME tree at `modules_resolved=110` with `dag/std/algebra.dag:367: variant 'Empty' not found in type 'List'`. Both readings are receipts; what is missing is the fact that explains the difference.",

"SECOND SPECIMEN, gunbc#11291, 2026-09-13, both observations first-hand -- and it carries a MEASURED mechanism for ITS OWN instance, which the first specimen still lacks. An indented `//` inside a declaration body: `claim_batch --entry` ran the claim and reported PASS, while required-witnesses-floor refused the identical bytes with `required-ci: parse FAIL ... source annotation sits inside a declaration body. Only module-item grain is modeled`. The author had a green execution receipt from a real consumer for source the merge path refuses, which is this row's shape exactly.",

"ITS MECHANISM IS NOT POPULATION, AND THAT IS THE POINT OF RECORDING IT. The first specimen's open question is whether the disagreement comes from the runner or from resolving under a larger module set, and the isolating experiment this row prescribes is to compare the same entry under both. Run for this instance, the answer is NEITHER: a six-line single module, one indented annotation, ONE locally built binary, compiled two ways. `gunbc compile --source-root <dir>` REFUSES it typed and located at `5:3`; `claim_batch --source-root dag --source-root src/v2 --entry <file>` ACCEPTS it and greens the claim. Same bytes, same binary, same declaration, no population difference available to explain it -- so for this instance the difference is in WHICH ROUTE RUNS THE CHECK, not in what the checks would say. The `AnnotationAttachmentRefusal` `BodyGrainNotModeled` arm is reached on the compile and emit path (`v1_compiler.cli_run.compile_clean`); the claim route resolves and evaluates without reaching it.",

"WHAT THIS DOES AND DOES NOT SETTLE, because the two specimens share a shape and that is not evidence they share a cause. It settles that AT LEAST ONE member of this class is a route that does not run a check rather than two checks disagreeing -- which is a strictly worse failure than a gate mismatch, since no amount of strictness on the claim route's own gate would have caught it. It does NOT explain the first specimen: that one refused with `VariantNotFound` under the floor's resolve, a diagnostic the claim route DOES compute, so its disagreement cannot be this mechanism and the population experiment remains unrun for it. Identical symptom, two candidate causes, one now measured.",

"THE PRACTICAL RULE THIS SPECIMEN ADDS: a local `claim_batch` green is not evidence about ANY refusal that lives on the compile or emit path, including the DESIGN section 4c annotation-grain refusals. For those classes the cheap local route is structurally silent rather than merely differently gated, so the check before pushing is a compile of the touched root, not a claim run over it.",

"WHAT WOULD ISOLATE IT, stated so the next occurrence produces the answer instead of another anecdote: the two runs differ in the POPULATION they resolve (an entry closure versus the floor's module set) and in nothing else that has been checked, so the discriminating experiment is to resolve the same entry under both populations and compare the diagnostic sets. If the entry closure alone refuses, the difference is in the runner; if it accepts while the larger set refuses, the difference is in how a declaration is typed when more modules are present, which is a different and more interesting class. Until that is run, no mechanism belongs in this row.",

"DISTINGUISHING FACTS, available before any push and independent of the cause: a change lands in a layer whose idioms the author inferred from a NEIGHBOURING layer, the local run is green first try, and no floor result exists yet. The boundary against neighbours: this is NOT [[accepted_source_emits_uncompilable_target]], where the refusing party is a TARGET compiler outside this repository and the emission is the subject; both answers here are our own, about the same source, at the same stage. It is NOT [[realization_arms_diverge_on_whether_the_program_refuses]] either -- that class is two realizations of an ALREADY ACCEPTED program disagreeing at evaluation time, where here the disagreement is about acceptance itself and never reaches evaluation on the refusing side.",
Expand Down
Loading
Loading