Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
9 changes: 8 additions & 1 deletion dag/gunbc/declaration_index_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,11 @@ data declaration_index_seed_growth_justification: SeedGrowthJustification = Seed
decl_name: "declaration_field_names",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "collect_reference_occurrences",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "record_from_module",
Expand Down Expand Up @@ -324,7 +329,7 @@ data declaration_index_seed_growth_justification: SeedGrowthJustification = Seed
],
reason: "WHY RUST IS STILL NEEDED, and it is a REACHABILITY limit rather than a modeling gap: the subject is INGESTION -- the moment a .dag file is read off the filesystem and parsed -- and the only ingestion that executes today is host Rust. A .dag witness cannot reach it: run_required_floor's hermetic envelope refuses host effects during preparation, so a witness whose subject is a filesystem walk is counted executed while its assertion never runs. Asserting the index's behaviour from a mocked file tree would assert the mock, which is the specification-without-execution trap, so the construction and its discriminating evidence both have to live where the walk does.\n\nTHE CONSEQUENCE OF REFUSING IT, stated second because it is not the admitting argument: there is no second executing ingestion to re-home this to, so a refusal would leave both of DESIGN's next-rung triggers -- section 6's module-authorship trigger and section 3's cited-symbol restoration trigger -- undischargeable until v2 is the compiler.\n\nWHAT THE GROWTH BUYS, at identity grain rather than as a category: three walls on one construction, replacing one deleted corpus-walk census and two obligations that had no mechanism at all. It also NETS DOWN inside claim_executor, which loses the --required-cited-symbol mode and its three helper functions.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete all 61 when INGESTION is itself modeled -- when the .dag source walk and the per-module record it derives are expressed as a .dag operation over a typed filesystem transport, the index becomes an ordinary substrate fold and these declarations move to the substrate. A PARTIAL migration IS admissible and is the expected shape: the moment the RECORD DERIVATION is modeled (record_from_module is a pure function of one parse tree and needs no host effect at all), the record builder and every finding function follow it, while the directory walk and the parse-clean plumbing stay behind for as long as the WALK is host-only; delete those on the second step. What does NOT dissolve them is the checks moving to another host entry point, and what does NOT dissolve them is a hermetic witness asserting a fabricated module tree -- that would retire the evidence while retiring nothing it guards.",
trigger: "Delete all 62 when INGESTION is itself modeled -- when the .dag source walk and the per-module record it derives are expressed as a .dag operation over a typed filesystem transport, the index becomes an ordinary substrate fold and these declarations move to the substrate. A PARTIAL migration IS admissible and is the expected shape: the moment the RECORD DERIVATION is modeled (record_from_module is a pure function of one parse tree and needs no host effect at all), the record builder and every finding function follow it, while the directory walk and the parse-clean plumbing stay behind for as long as the WALK is host-only; delete those on the second step. What does NOT dissolve them is the checks moving to another host entry point, and what does NOT dissolve them is a hermetic witness asserting a fabricated module tree -- that would retire the evidence while retiring nothing it guards.",
current_boundary: "src/v1/stage0/src/declaration_index.rs; src/v1/stage0/src/cli_run.rs run_dag_parse_sweep; src/v1/stage0/tests/declaration_index_integrity.rs; src/v1/stage0/src/bin/claim_executor.rs; src/v1/stage0/src/bin/v1_src_dag_parse.rs; dag/gunbc/declaration_index_seed_growth.dag"
}

Expand Down Expand Up @@ -393,3 +398,5 @@ data declaration_index_fixture_exemption_classification_stall: GuaranteeStall =
}

data declaration_index_site_grain_roster_note: String = "THE SUPPRESSION ROSTERS MOVED FROM TARGET GRAIN TO SITE GRAIN (gunbc#9328). Recorded here rather than silently amended, for the reason the two rows above are: the grain of an exemption roster is the whole content of whether it is a contract or a hole, and this carrier had disclosed the previous grain as if it were sound.\n\nWHAT WAS HERE. All three rosters -- PRE_EXISTING_CITATION_DEBT, PLANTED_CONTROL_CITATIONS, FIXTURE_CARRIER_CITATION_EXEMPTIONS -- were keyed (cited module, declaration, field). citation_in_roster read the CITED symbol only, so a row exempted that target corpus-wide and permanently. A patch could author a BRAND NEW dangling DeclarationRef naming any enrolled target, from a module that had never cited it, and the wall stayed silent -- a fail-open inside the mechanism built to refuse exactly that class, and decidable from the patch alone.\n\nOCCUPIED, NOT MERELY REACHABLE, measured over DAG_PARSE_SWEEP_ROOTS: the 70 target-keyed rows covered 87 refusing sites, and seven targets were already cited from more than one module -- gunbc.host_effect host_effect_apply from three, std.bytes builtin_function_registry from three, extdeps.network.mac parse_mac_address from two, four more from two apiece. Every extra site was suppressed by a row authored about a different module.\n\nWHAT LANDED. A row is (citing module, citing declaration, cited module, declaration, field) and exempts THE SITE THAT AUTHORED IT. Both inverse arms read that one identity through a single refusing_sites set, because a suppression arm and a staleness arm keyed differently is the desynchronization this carrier already records once. The rosters are re-derived from the measurement rather than hand-extended: 42 debt, 41 fixture, 4 control, 87 sites, corpus clean.\n\nTHE FIRST DERIVATION WAS TAKEN OVER THE WRONG DENOMINATOR, and it is recorded because it is this carrier's own recurring class arriving a third time. The sweep's roots are src/v1, dag and src/v2; the first measurement used only the last two, so five sites in modules the narrow walk never read were absent from the rosters and the required run refused them. A roster derived from a subset of the subject it governs is not a smaller roster, it is a wrong one.\n\nHAND-ITEM DELTA: +5, enumerated in the roster above rather than counted -- citation_site, refusing_sites and site_owned in declaration_index.rs, and two discriminating tests, a_new_citation_of_an_enrolled_target_from_another_module_still_refuses and a_roster_row_exempts_its_own_citer_and_no_other. No file is added, no impl block is introduced, and every one of the five is citable as a WholeDeclaration. The trigger is unchanged and now names 60: these dissolve with the index, not separately.\n\nRUNG: unchanged at MECHANICALLY PREVENTABLE. This is a repair of an open direction in an existing wall, not a climb -- the invalid state stays writable and safety still depends on the phase executing. The red is authorable and authored at the FIXTURE boundary: both tests above go GREEN under the target-keyed form, which is the state they exist to forbid.\n\nTHE DECLARATION WAS ADDED AFTER REVIEW AND IT IS THE SAME REPAIR ONE LEVEL IN (review 56227). The first cut keyed a row on the citing MODULE, which left two citations of one target inside one module sharing a row -- so a new dangling citation authored BESIDE an enrolled one stayed suppressed. That was DISCLOSED as residue rather than closed, and the objection was that a residue whose closing identity is already available is not a residue. It was available: record_from_module already iterates top-level items, so the enclosing declaration name costs one string at extraction, and it is a NAME reachable from the containment tree rather than the offset DESIGN section 3 forbids. Closed, with a_second_citation_of_an_enrolled_target_in_another_declaration_still_refuses as the discriminating red -- it reports zero findings under the module grain.\n\nWHAT IS NOT REACHED, stated because a closed residue must not be reported as a total one: two citations of one target inside ONE DECLARATION still share a row. Only a position separates those, and a position is what this grain exists not to be, so this is a CEILING rather than a stall. The next rung would be an occurrence ordinal within the declaration -- representable in the record, needed by no measured site today."

data declaration_index_reference_channel_selectivity_note: String = "THE REFERENCE CHANNEL BECAME SELECTIVE BY NODE KIND (gunbc, this change). Recorded here rather than only in the Rust doc comment, because the previous behaviour was DECLARED SOUND on this carrier's own construction -- record_from_module collected every authored name in a module's tree and the field's doc argued the over-collection was harmless -- and a refuted argument has to be retired where it was made.\n\nTHE ARGUMENT AND WHY IT IS WRONG. It read: the over-collection is SYMMETRIC across the two trees v1_compiler.namespace_wave_admission compares, so a spelling that denotes nothing on both sides contributes no delta. A symmetric COLLECTOR does not give a symmetric VERDICT. The supplier set the wall computes for a row is a function of the CORPUS, not of the site, so deleting an unrelated declaration moves it under every site that merely spells the same word -- and a field label spells words.\n\nTHE SPECIMEN, MEASURED RATHER THAN PREDICTED. On gunbc#9106 a witness module deleted a helper fn live_tree_declined_entries and kept twelve RECORD FIELD LABELS of that spelling. Twelve labels, twelve enclosing declarations, twelve NewUnresolvedness rows, one-to-one, against a correct cut. The delta was TRUE about the declaration and FALSE about every site it named: a label binds to nothing and needs no supplier at all.\n\nWHAT LANDED, IN THE SHAPE THE CITED COLLECTOR ON THE SAME WALK ALREADY USED -- decide by node kind, never by name. Two kinds stop being references. First, a record literal's FIELD LABELS: ExprRecordLit's children are its field initializers and nothing else, so the label is decidable from the parent's kind with no guessing, and the initializer's VALUE is still walked because that is where a reference lives. Second, a field projection's MEMBER name: f.widget names a field of a value, not a declaration. The whole dotted spelling is still recorded, which is what module_prefix_of needs to keep a module-qualified reference such as probe.home.widget resolving, and the wall keys on the last segment either way. A name-based suppression list was refused: it would be the same defect one layer up.\n\nWHAT IS NOT REPAIRED, stated because a partial repair reported as a total one is worse than none. A record TYPE declaration's field labels, a named call argument's label, a parameter binder and a coproduct's variant names are STILL collected as references, and each can fabricate the same refusal from a different position. Measured on a fixture rather than assumed: a type declaring a field named tag contributes tag, and a call passing an argument labelled tag contributes tag. They are not swept in here because the parent kinds carrying them also carry children that ARE real references -- a refinement's base type expression is a Connective Conj child with a real type name -- so a parent-kind rule for them cannot be lifted from this one and needs its own fixture. Excluding them by guessing would risk the opposite defect, which is strictly worse: a wall that stops seeing genuine unresolvedness is a decoration.\n\nEVIDENCE, BOTH DIRECTIONS, AT THE FIXTURE BOUNDARY, in the wave wall's own fixture file. RED: deleting_a_declaration_a_record_field_label_merely_spells_carries_no_delta, which reports exactly the specimen's NewUnresolvedness under the previous collector and nothing under this one. GREEN, and this is the half that matters: deleting_a_declaration_a_body_still_references_is_still_unresolvedness and deleting_a_declaration_a_qualified_spelling_reaches_is_still_unresolvedness both require the wall to KEEP refusing a deletion that a real reference reaches, one bare and one dotted. The second is the control on the projection half specifically, because a repair that had dropped the dotted spelling instead of the member name would green the red and silence that arm with it.\n\nRUNG: unchanged at MECHANICALLY PREVENTABLE. This is a repair of a fabricated-refusal direction in an existing wall, not a climb. HAND-ITEM DELTA: plus one, collect_reference_occurrences, enumerated in the roster above; record_from_module's inline walk is replaced by a call to it rather than duplicated, and no other declaration is added. The three test arms live in the wave wall's fixture file, whose carrier gunbc.namespace_wave_admission enumerates lib declarations rather than test arms."
Loading
Loading