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
4 changes: 2 additions & 2 deletions dag/gunbc/declaration_index_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import std.types { String }
import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation }
import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when }

data declaration_index_seed_growth_note: String = "Seed-growth obligation for the ingestion-time per-module declaration index (gunbc#9211). Homed here, beside the obligation it declares, rather than inside gunbc.seed_growth_admission, which owns the ROSTER and the join.\n\nWHAT THE CHANGE IS. v1_compiler.cli_run run_dag_parse_sweep already parses every .dag under DAG_PARSE_SWEEP_ROOTS -- src/v1, dag and src/v2, 3991 files -- once, in parallel, on every required run, and threw every parse tree away. It now builds one ModuleDeclarationRecord per module from that same parse, and three integrity questions are answered from that single keyed index rather than by three corpus-wide walks: import-member claim integrity, the cited-symbol wall, and the lens authorship fact. --required-cited-symbol is DELETED in the same change, so the replacement has one route and not two.\n\nTHE EXHIBITED COST, WHICH IS WHAT ADMITS THIS RATHER THAN THE TWO DESIGN TRIGGERS. v1_maintenance_loaded_index_noun_admission_note states the axis: reachability with exhibited cost, and the argv-fabrication row was refused because it exhibits nothing today. This exhibits, measured on the live tree at 46 sites over 38 distinct targets: authored citations naming declarations that do not exist, unguarded since the operator removed the cited-symbol job on 2026-08-23. And it exhibits a class no mechanism in the repository covers at all: v1's own MissingExport is a function of the COMPILE CLOSURE it is handed, so an ORPHAN module's import claims are checked by nothing -- DESIGN's 2026-08-25 row records gunbc.auth.credentials standing on main with four hard errors for exactly that reason. That premise is MEASURED rather than inferred: orphan_import_claim_is_refused_here_and_nowhere_else holds the identical false claim in a module the resolver sees (MissingExport fires, the index agrees) and in one no closure reaches (the resolver is never asked, the index refuses alone).\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE, ON PRECEDENT RATHER THAN ANALOGY. gunbc.v1_maintenance_standing v1_seed_standing admits by PURPOSE -- does the change serve the v2 self-host program -- and the purpose test reaches the INSTRUMENT that measures that program, not only the program. gunbc.parse_refusal_location_seed_growth admits hand-Rust growth in this same run_dag_parse_sweep on that exact ground: a required-CI phase that cannot locate its own refusals taxes every lane INCLUDING THE SELF-HOST WORK. gunbc.floor_non_verdict_enrollment admits on the same footing: the required floor is the INSTRUMENT that guards that program.\n\nCLASSIFIED AGAINST ALL FIVE REFUSED CLASSES, because a refusal dominates every admission and the nearest one has to be answered rather than skipped. NewLanguageBehavior: no. The compile pipeline is byte-untouched -- no diagnostic is added, moved or removed, and resolve, infer and emit are not edited. NewCompatibilityObligation: no. Nothing is kept working for an old caller; a mode is deleted. NewEscapeHatchOrAdmissionRow: no, and the direction is opposite -- this adds a wall and removes a route. There is no flag, env var or mode that skips it. SeedFeatureCompletion: no. The seed COMPILER gains no capability; it compiles exactly what it compiled before. PublicSurfaceGrowth: this is the nearest, and the test v1_maintenance_rung_note states is a diff over THE EMITTED SEED'S EXPORTED DECLARATIONS. Checked rather than asserted: declaration_index.rs is wired by #[path] mod inside cli_run.rs, exactly as phase_profile.rs and required_regen_host.rs are, so it contributes no pub mod line to the emitted lib.rs -- its SeedRetainedIntrinsicRegistration carries has_pub_mod: false, and the emitted crate's exported surface is unchanged. What grows is the SeedRetained roster, enumerated here.\n\nHAND-ITEM DELTA: +55, all enumerated below rather than counted, and ZERO of them uncitable -- there is not one impl block in either file, which is deliberate: the first draft carried four, and every impl method is uncitable as a DeclarationRef because std.decl_ref offers WholeDeclaration or NamedField and neither names a method on an impl block, so it would have grown the class gunbc.seed_growth_admission reports as seed_growth_uncitable_item_keys. MEASURED FROM THE MERGE BASE 58a15c7eef5702668ae3464be4d9b20c836d3573, not against the moving tip, because a branch delta taken against the tip renders main's own commits as deletions the author did not make. src/v1/stage0/src/cli_run.rs is +70/-10 and adds ZERO declarations -- the change is inside the existing run_dag_parse_sweep plus one #[path] mod line and one returned struct -- so its disposition is ExistingSeedItemModified and listing it would net a modification into an addition census. src/v1/stage0/src/bin/claim_executor.rs and bin/v1_src_dag_parse.rs likewise add no declaration; claim_executor NETS DOWN, deleting three functions with the --required-cited-symbol mode.\n\nRUNG, STATED AT THE HONEST GRAIN AND NOT INFLATED. The class -- an authored claim about another module that names nothing real -- moves from MITIGATABLE (review diligence, which is where DESIGN's 2026-08-23 row left it) to MECHANICALLY PREVENTABLE: a real wall, armed on every required run, whose red is authorable at the FIXTURE boundary and is authored there, in tests/declaration_index_integrity.rs, one planted violation per arm beside a positive control that must stay clean. It is NOT structurally guaranteed and this row does not claim it: the invalid state stays perfectly writable and safety depends on the phase executing. WHAT IS DISCHARGED AND WHAT IS NOT, because the two DESIGN triggers have two halves and only one moves here: the CORPUS-WALK half is discharged FOR THESE THREE QUESTIONS -- one module's facts now come from one module's source at ingestion, and the citation wall no longer reaches decl_facts at all, because --required-cited-symbol and its lens are off the required path entirely. WHAT THAT DOES NOT SAY, corrected before merge because the earlier wording said it and it is not true: decl_facts is NOT unconsulted by the required run. It has live .dag consumers, and several are floor-discovered witness modules -- decl_facts_reflection_witness_test, record_construction_census_witness_test, floor_expected_red_coherence_witness_test and others -- so the corpus walk still executes inside the required floor for their sake. Retiring those consumers is a separate cut with its own subject and its own review surface. The claim this change earns is that THE THREE INTEGRITY QUESTIONS come from one construction instead of three walks, not that the walks are gone. The HAND-RUST half is not: the index is host Rust rather than a modeled ingestion operation, which is why this carrier exists at all.\n\nWHAT THE ARMS DO NOT COVER, named rather than left to be discovered. A citation authored INSIDE a witness or fixture carrier is not enrolled, because a witness proving the resolver refuses an absent module has to author an absent module -- test.claim.annotation_carrier cites extdeps.network.mac parse_mac_addres on purpose, one letter short. The property is read off the module's own path, not from an exemption list, and the population is counted (in_fixtures) rather than dropped. A citation naming a namespace no swept module declares -- v1_compiler.cli_run and its siblings name hand-Rust -- is likewise counted (outside_index) rather than refused, and the line between it and a DELETED .dag module is the namespace root, which is decidable from the index itself. And the field arm resolves against the union over a declaration's subtree, so a field belonging to a different variant of the same coproduct resolves; that weakening is confined to the field arm and its next rung is a lookup that descends the declared TYPE."

Expand Down Expand Up @@ -842,5 +842,5 @@ data declaration_index_fixture_exemption_classification_stall: GuaranteeStall =
"v2.test.lens_cost.valuation unmodelled_effect_specimen",
],
},
next_rung_trigger: "a witness declares each citation it plants to refuse as a typed row beside the citation -- at which point the deliberate half of this roster is DERIVED rather than enrolled, this roster shrinks to the genuinely stale remainder, and that remainder becomes ordinary debt with a terminal state of empty. Until then a new stale citation authored inside a fixture carrier is caught by the wall, but an existing enrolled one is indistinguishable from a control",
next_rung_trigger: climbs_when(capability: "a witness declares each citation it plants to refuse as a typed row beside the citation -- at which point the deliberate half of this roster is DERIVED rather than enrolled, this roster shrinks to the genuinely stale remainder, and that remainder becomes ordinary debt with a terminal state of empty. Until then a new stale citation authored inside a fixture carrier is caught by the wall, but an existing enrolled one is indistinguishable from a control"),
}
121 changes: 118 additions & 3 deletions dag/gunbc/guarantee_stall.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,12 @@ module gunbc.guarantee_stall
import std.types { String, List, Bool, Int }
import v2.std.algebra { fold_list }
import gunbc.guarantee_rung { GuaranteeRung, guarantee_rung_label, guarantee_rung_index }
import gunbc.lifecycle_bounded_referent {
DashboardWorkItemReferent,
dashboard_node_uri_scheme,
dashboard_work_item_referent_uri,
text_spells_a_dashboard_node_uri,
}

// THE CARRIER FOR A DESIGN section 4b(2) STALL, and it is a different fact from a section 4b(3)
// DROP (gunbc.rung_drop) rather than a variant of it. A DROP is an event: something that held a
Expand Down Expand Up @@ -41,6 +47,14 @@ import gunbc.guarantee_rung { GuaranteeRung, guarantee_rung_label, guarantee_run
// writable as it was, and nothing detects one. That is a scope statement, not a climb, and stating
// it here is what keeps a reader from counting this module as coverage it does not provide.
//
// THE SAME SCOPE STATEMENT APPLIES TO THE TRIGGER'S SECOND WALL BELOW, and it is narrower still.
// `stall_trigger_admission` refuses a capability that spells the declared dashboard-node URI
// scheme, which is decidable because that scheme has one owner; it says nothing about a trigger
// that names a lane in words, and nothing about whether an obligation kept an accountable owner
// after that lane ended. Those are the free-prose form and the responsibility-survival trigger of
// `gunbc.recurring_failure_mode.stale_claim_survives_its_own_correct_edit`, and neither is climbed
// here.
//
// THIS MODULE CARRIES THE SHAPE AND THE FOLDS; THE ROWS ARE ONE MODULE EACH under
// gunbc.guarantee_stall.<row>, and gunbc.guarantee_stall.roster is the enumeration. The split is
// the one gunbc#10206 made for gunbc.recurring_failure_mode and it is made here for the same
Expand All @@ -67,13 +81,48 @@ type StallPopulation
= BoundedPopulation { members: List<String> }
| UncountedNotEnumerable { reason: String }

// THE TRIGGER IS TWO FACTS AND WAS ONE FIELD, which is the whole of this carrier's exposure to
// `gunbc.recurring_failure_mode.stale_claim_survives_its_own_correct_edit`. `capability` is the
// OPERATIVE half -- the condition section 4b(2) obliges the row to name, and the only half a later
// reader can re-measure. `awaiting` is the PROVENANCE half: the lifecycle-bounded lanes that were
// asked to deliver it, carried as modeled referents so that a lane closing is a fact a consumer
// can join against rather than a word inside a sentence.
//
// SEPARATING THEM IS WHAT MAKES THE STALE READING UNAVAILABLE. While both halves shared one
// `String`, "node://adhoc-a3b0e05f-374 lands: the wall materializes the operation" reads as a
// trigger whose satisfaction condition is a NODE REACHING DONE -- and three such nodes reached
// done with their conditions unmet, which `gunbc.guarantee_stall.roster` records with its dated
// reading. A row split this way cannot be read that way: the capability stands alone, and the node
// is beside it as who was asked and never as evidence that the climb happened.
//
// WHAT THIS DOES NOT CLAIM. Carrying the referent does not decide whether responsibility for the
// obligation survived that lane's closure; that is the class row's own next trigger, whose subject
// is responsibility survival through a modeled closure transition, and it is a different subject
// from this one. This carrier decides only that the trigger's operative half is stated without
// resting on a lifecycle-bounded referent, and that any referent it does rest on is modeled.
type NextRungTrigger {
capability: String
awaiting: List<DashboardWorkItemReferent>
}

// TWO CONSTRUCTORS BECAUSE THE EMPTY LIST IS THE COMMON AND CORRECT CASE, and spelling `awaiting:
// []` at every row would make the exceptional case indistinguishable from the ordinary one at a
// glance. `climbs_when` is the row that waits on nobody; `climbs_when_awaiting` names the lanes.
fn climbs_when(capability: String) -> NextRungTrigger {
NextRungTrigger { capability: capability, awaiting: [] }
}

fn climbs_when_awaiting(capability: String, awaiting: List<DashboardWorkItemReferent>) -> NextRungTrigger {
NextRungTrigger { capability: capability, awaiting: awaiting }
}

type GuaranteeStall {
subject: String
current: GuaranteeRung
ceiling: GuaranteeRung
blocker: ClimbBlocker
population: StallPopulation
next_rung_trigger: String
next_rung_trigger: NextRungTrigger
}
// A STALL WHOSE CURRENT RUNG EQUALS ITS CEILING IS NOT A STALL. The type cannot forbid writing one
// -- that would need a dependent pair over the two rungs -- so this is validation standing where
Expand Down Expand Up @@ -105,6 +154,18 @@ fn stall_population_render(p: StallPopulation) -> String {
}
}

// THE AWAITED LANES ARE RENDERED FROM THE REFERENTS AND NEVER RE-SPELLED, so the report cannot
// disagree with the field: the URI comes from the referent's own module, which owns the scheme.
// They are rendered AFTER the capability and labelled as who was asked, so a reader is never
// handed a sentence in which a lane's ending looks like the condition.
fn next_rung_trigger_render(t: NextRungTrigger) -> String {
fold_list(
xs: t.awaiting,
empty: t.capability,
cons: fn(acc, r) { concat(acc, concat(" [asked: ", concat(dashboard_work_item_referent_uri(referent: r), "]"))) },
)
}

// ONE RENDERING, for the reason gunbc.rung_drop's renderer already gives: a consumer that spelled
// its own message would be a second authority for the row's own fields and the two would drift.
fn stall_report_message(s: GuaranteeStall) -> String {
Expand All @@ -114,7 +175,7 @@ fn stall_report_message(s: GuaranteeStall) -> String {
concat(", ceiling ", concat(guarantee_rung_label(r: s.ceiling), concat(" (", climb_blocker_label(b: s.blocker)))),
concat(
concat("). Population: ", stall_population_render(p: s.population)),
concat(". Climbs when: ", concat(s.next_rung_trigger, "."))
concat(". Climbs when: ", concat(next_rung_trigger_render(t: s.next_rung_trigger), "."))
)
)
)
Expand All @@ -130,17 +191,71 @@ fn every_stall_is_below_its_ceiling(ss: List<GuaranteeStall>) -> Bool {
)
}

// THE SECOND WALL OVER THE SAME FIELD, AND IT IS A DIFFERENT SUBJECT FROM THE FIRST. 4b(2) asks
// whether a trigger was NAMED; this asks whether what was named is a capability rather than a
// lifecycle-bounded referent's ending. A row can satisfy the first and fail this one, which is the
// state every migrated row here was in.
type TriggerAdmission
= TriggerAdmitted
| TriggerCapabilityEmpty { subject: String }
| TriggerCapabilitySpellsAReferent { subject: String, scheme: String }

fn stall_trigger_admission(s: GuaranteeStall) -> TriggerAdmission {
if s.next_rung_trigger.capability == "" {
TriggerCapabilityEmpty { subject: s.subject }
} else {
if text_spells_a_dashboard_node_uri(text: s.next_rung_trigger.capability) {
TriggerCapabilitySpellsAReferent { subject: s.subject, scheme: dashboard_node_uri_scheme }
} else {
TriggerAdmitted
}
}
}

fn trigger_admission_label(a: TriggerAdmission) -> String {
match a {
TriggerAdmitted => "admitted"
TriggerCapabilityEmpty { subject: subj } => concat("untracked stall, no trigger named: ", subj)
TriggerCapabilitySpellsAReferent { subject: subj, scheme: sch } =>
concat(
concat("trigger rests on a lifecycle-bounded referent spelled into its capability (", sch),
concat("): ", subj),
)
}
}

fn every_stall_trigger_is_admitted(ss: List<GuaranteeStall>) -> Bool {
fold_list(
xs: ss,
empty: true,
cons: fn(acc, s) {
acc && match stall_trigger_admission(s: s) {
TriggerAdmitted => true
TriggerCapabilityEmpty { subject: _ } => false
TriggerCapabilitySpellsAReferent { subject: _, scheme: _ } => false
}
},
)
}

// SECTION 4b(2) IS WHAT THIS ENFORCES: a class below its ceiling must NAME its next-rung trigger,
// so "cannot climb further" stays separable from "unbuilt". An empty trigger is the untracked
// stall that clause forbids, and it becomes decidable here rather than left to review diligence.
fn every_stall_names_a_trigger(ss: List<GuaranteeStall>) -> Bool {
fold_list(
xs: ss,
empty: true,
cons: fn(acc, s) { acc && s.next_rung_trigger != "" },
cons: fn(acc, s) {
acc && match stall_trigger_admission(s: s) {
TriggerCapabilityEmpty { subject: _ } => false
TriggerCapabilitySpellsAReferent { subject: _, scheme: _ } => true
TriggerAdmitted => true
}
},
)
}


// THE QUANTIFIER'S DOMAIN, EXPOSED SO IT CAN BE ASSERTED. Both folds above are universally
// quantified and therefore TRUE on an empty roster, so without this a roster that lost its rows
// would satisfy every check written over it. Counting is what makes emptiness a refusable state
Expand Down
Loading
Loading