Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
fb40194
Closure front end reads its lexical artifact from pool_acquire
Sep 29, 2026
a9cb98a
One heads reading per file: the pool census projects it instead of re…
Sep 29, 2026
c927086
Heads projection: exhaustive destructuring, no catch-all arms
Sep 29, 2026
8f84d20
Tree census upgrades the memoized raw census instead of rebuilding it
Sep 29, 2026
7ee3a65
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 29, 2026
a88e21b
Heads projection: name Node.declaration (#12612); the parser never wr…
Sep 29, 2026
e404000
WIP: tree census upgrades only the bare fill (seed regen pending)
Sep 29, 2026
304413c
Merge branch 'session/bold-bat-516-heads' into session/bold-bat-516-t…
Sep 29, 2026
8b9d77b
Merge branch 'session/bold-bat-516-heads' into session/bold-bat-516-t…
Sep 29, 2026
8bdf2c3
Regenerate v1_compiler_infer.rs from 04_infer.dag (bare-fill split)
Sep 29, 2026
176f346
WIP: pool fallback census probe
Sep 30, 2026
4d55586
Merge remote-tracking branch 'origin/session/bold-bat-516-typed-censu…
Sep 30, 2026
b7a38df
Merge branch 'session/bold-bat-516-bare-fill' into session/bold-bat-5…
Sep 30, 2026
d7a0c1c
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 30, 2026
fa5bab8
Merge branch 'session/bold-bat-516-typed-census' into session/bold-ba…
Sep 30, 2026
12b4665
Bare loader: no whole-pool census; per-name answer, typed cross-tree …
Sep 30, 2026
831f670
Merge remote-tracking branch 'origin/session/bold-bat-516-bare-fill' …
Sep 30, 2026
4413666
Transitive bare-pick defect: failure-mode row and pinned specimen; ba…
Sep 30, 2026
0322af3
Per-name bare census: prune to the name's declarations; derive the he…
Sep 30, 2026
8038ff8
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 30, 2026
24867b3
Merge remote-tracking branch 'origin/session/bold-bat-516-bare-fill' …
Sep 30, 2026
fac9b9c
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 30, 2026
e0727d7
Retire 12 unimported-bare-provider get pairs as ImportsFixed
Sep 30, 2026
6f57449
Changed-witness sublane: typed DeclinedNoCiWetLane for edited BinWitn…
Sep 30, 2026
c252a1a
Merge remote-tracking branch 'origin/session/bold-bat-516-no-ci-wet-l…
Sep 30, 2026
e217f4d
Adapt the cross-tree refusal to main's (module, is_test_row) provider…
Sep 30, 2026
9d8fd01
DeclinedNoCiWetLane consumes the drop's declared population (review 7…
Sep 30, 2026
432d3cb
Merge remote-tracking branch 'origin/session/bold-bat-516-no-ci-wet-l…
Sep 30, 2026
14c6e2c
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 30, 2026
8cb38e4
Regenerate docs/design-rung-drops.md: the drop row's projection was m…
Sep 30, 2026
a8d55a2
Remove a scratch script committed by mistake
Sep 30, 2026
7a608f8
Regenerate docs/design-rung-drops.md for the population's bare-patter…
Sep 30, 2026
63228fa
Merge remote-tracking branch 'origin/session/bold-bat-516-no-ci-wet-l…
Sep 30, 2026
b3bc7f4
Merge remote-tracking branch 'origin/main' into session/bold-bat-516-…
Sep 30, 2026
2cdadf5
Changed-witness join counts DeclinedNoCiWetLane as a changed-witness …
Sep 30, 2026
ccbeaff
Merge remote-tracking branch 'origin/session/bold-bat-516-wet-decline…
Sep 30, 2026
aa975a6
Execute the changed-witness join by a unit, decide its membership exh…
Sep 30, 2026
425f472
Merge remote-tracking branch 'origin/session/bold-bat-516-wet-decline…
Sep 30, 2026
b110cd6
Failure-mode row: say which evidence the merge path executes (review …
Sep 30, 2026
fd99408
Merge origin/main: keep the extracted changed-witness join beside the…
Oct 1, 2026
67972fd
Merge the #12833 branch (with main): keep bare-scope tests beside the…
Oct 1, 2026
6846561
Merge origin/main (#12833 landed) into the bare-scope branch
Oct 1, 2026
ed02153
Reverse roster joins suppress a changed witness the sublane declined …
Oct 1, 2026
e511353
Every RequiredFloorDisposition consumer decides by an exhaustive matc…
Oct 1, 2026
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
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ data a_new_decision_arm_the_downstream_join_does_not_admit: RecurringFailureMode
"INVALID STATE: a new arm is added to a decision (a disposition variant, a standing, a route outcome), and a DOWNSTREAM exactness check over that decision -- a join that says which decided rows count -- was written against the older set of arms and does not admit the new one. Every piece is individually green: the arm compiles, its row is pushed, its projection prints. But the route that reaches the arm always refuses at the join, so the arm is unreachable in production. HARM: the capability the arm exists for is dead on arrival, and it is discovered only when some later change happens to exercise the route, at which point that unrelated change reds.",
"SPECIMEN (bold-bat-516, 2026-09-30): gunbc#12794 added RequiredFloorDisposition::DeclinedNoCiWetLane to the required floor's changed-witness sublane and pushed a disposition row for each declined selection. The sublane's exactness join built its right-hand side from PlannedAsChangedWitness rows ONLY, so every declined selection refused as ChangedWitnessSublaneJoinInexact selected_without_disposition. It was first observed on gunbc#12741's floor (run 36768985832), the first PR to edit a BinWitnessWet witness after #12794 merged. #12794's only planned route evidence was that later PR's floor, so the defect merged.",
"DISTINGUISHING FACTS: the new arm is a member of an enumeration that some other site FILTERS with an explicit allow-list (a matches! over named arms) rather than an exhaustive match, so adding the variant produced no compile error there; and the change's evidence exercised the arm's own site, not the site that consumes its result.",
"SPECIMEN 2, THE SAME ARM AT THE THIRD AND FOURTH JOIN (gunbc#12741, 2026-10-01): the reverse roster joins (expected-red, route-gap, non-verdict) kept every changed witness on the premise that the changed sublane executes it, so the floor refused the three DeclinedNoCiWetLane identities as stale route-gap rows; and the seed mirror cli_run partition_cost_debt_roster classed DeclinedNoCiWetLane and DeclinedChangedWitnessOutsideDiscovery as DeclaredButNotWithheld through a Some(_) catch-all, contrary to its own authority v2.workflow.required_floor cost_debt_roster_standing (OutsideThisRunsUniverse) -- a refusal waiting for the first rostered wet decline. CENSUS of every consumer of RequiredFloorDisposition and ExpectedRedSuppressionGround, Rust and .dag, at gunbc#12741: every .dag consumer and both generated Rust consumers were already exhaustive; five hand-written seed sites were not -- partition_cost_debt_roster (Some(_)), reconcile_withheld_against_dispositions (matches! DeclinedCostDebt), required_floor_runner enrolment_margin_standing_for (Some(other)), changed_witness_projection_rows (Some(declined)), and the run_required_floor site-projection counters (six matches!, already omitting four arms). All five are converted to exhaustive matches in that change, with a unit red on the restored catch-all (changed_selection_declines_are_outside_this_runs_universe); the reverse joins gained ExpectedRedSuppressionGround::DeclinedNoCiWetLane decided by the exhaustive suppresses_a_changed_witness_enrollment. Residue for these two enumerations after that change: none. The tell, measured: the defect sat only in hand-written seed mirrors of decisions whose .dag authority was already exhaustive.",
"RUNG FOUND AT: mitigatable (the join refused loudly, so nothing passed silently -- the cost was an unreachable capability plus a red on the next consumer). RUNG NOW, FOR THE SPECIMEN'S SITE: structurally guaranteed -- gunbc#12833 extracts the join as cli_run required_floor_runner changed_witness_sublane_join, which decides membership through decides_a_changed_selection, an EXHAUSTIVE match over RequiredFloorDisposition, so a new variant does not compile there until it states whether it counts; changed_witness_sublane_join_tests executes it with a DeclinedNoCiWetLane selection (red on the pre-fix allow-list predicate with the floor's own ChangedWitnessSublaneJoinInexact refusal, green on the fix). WHAT THE MERGE PATH EXECUTES, stated exactly (review 73414): the structural claim rests on the exhaustive match, which the required lint step compiles on every pull request; the unit runs on NO CI path -- the rust-unit-tests lane was deleted by the 2026-09-29 operator ruling and the lint step only compiles it (gunbc.rung_drop rust_unit_tests_off_the_merge_path) -- so its red/green is local supporting evidence and not a merge gate. FOR THE CLASS: mitigatable -- other consumers that select disposition arms by an allow-list matches! remain. CEILING: structurally guaranteed at every such consumer. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: every consumer that decides membership over a closed disposition enumeration does so by an exhaustive match, so adding an arm fails to compile at each one until its membership is stated.",
],

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module gunbc.recurring_failure_mode.a_pool_fallback_provider_shadows_a_builtin

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_pool_fallback_provider_shadows_a_builtin: RecurringFailureMode = RecurringFailureMode {
identity: "a_pool_fallback_provider_shadows_a_builtin" as NonEmptyStr,

receipts: [
"INVALID STATE: a bare reference that names a BUILTIN is resolved by the bare-reference loader to an ordinary pool function that happens to share the name, pulling an unrelated module into the closure. HARM: silent wrong resolution -- the closure depends on a module the author never referenced, so that module's refusals, cost and edits reach a file they do not concern, and nothing reports it.",
"SPECIMEN: dag/test/claim/builtin_get_resolver_test.dag (module test.claim.builtin_get_resolver) calls the builtin get(xs:, index:); the loader's whole-pool fallback in cli_run visit_bare_reference_providers resolved 'get' to fn get in v2.test.manual.fn_as_value (src/v2/test/claim/manual/fn_as_value_test.dag), another source tree. Found by the live fallback census on the resolver-cost lane (bold-bat-516, 2026-09-30): of 624 import-less pool files, 466 demanded the whole-pool fallback census and 13 resolutions in 5 files depended on it; this was the one that was wrong.",
"DISTINGUISHING FACTS: the name is in v1.compiler.infer_method builtin_signature; the file's own source tree does not declare it; some other tree does. The fallback asked the whole pool for the superset instead of asking which kind of name this is -- DESIGN section 5's absorbing fallback, whose answer here was a wrong provider rather than a missing one.",
"RUNG FOUND AT: silent (outside the ladder). RUNG NOW: mechanically preventable -- the whole-pool fallback is deleted; a name the file's tree does not provide is a builtin (no provider), provided only by another tree (typed CrossTreeBareReference refusal naming the qualified spelling to write), or provided nowhere (no provider; the typecheck refuses an undefined name). Receipts: cli_run entry_resolve cross_tree_bare_reference_tests (a_builtin_named_like_another_trees_function_admits, an_unimported_cross_tree_bare_name_refuses) and the live cross_tree_bare_census. CEILING: structurally guaranteed -- a bare reference resolves only within its own source tree or through a written import, so no pool-wide lookup exists to shadow a builtin. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: bare-reference resolution in the v2 demand engine keyed by the reference's own scope (docs/plans/demand-engine-program.md), so the loader route and the typecheck bind a bare name through one authority.",
],

evidence: [],
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module gunbc.recurring_failure_mode.an_import_turns_an_ambiguous_bare_name_into_a_transitive_pick

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data an_import_turns_an_ambiguous_bare_name_into_a_transitive_pick: RecurringFailureMode = RecurringFailureMode {
identity: "an_import_turns_an_ambiguous_bare_name_into_a_transitive_pick" as NonEmptyStr,

receipts: [
"INVALID STATE: adding one import to a .dag file changes how an UNRELATED bare name in that file resolves. Without imports, a bare name two modules of the file's source tree declare refuses as ambiguous; with any import, the same bare name binds silently to whichever declaring module the import CLOSURE happens to reach -- including through the imported module's own imports -- because an import-bearing file's bare names resolve against its closure-scoped census first (closure wins the intersection) and the loader follows no bare references for it. HARM: silent wrong resolution -- a name the author never imported, and that is ambiguous in their tree, is bound to a transitively reachable homonym, and editing an import anywhere upstream can rebind it.",
"SPECIMEN (fixture, measured by bold-bat-516 on 2026-09-30 in the resolver-cost lane): tree ta has ta.dep (fn bar -> 1, fn z), ta.other (fn bar -> 2), ta.lib (import ta.dep { z }). ta.bare_user (no imports) calling bar() refuses: 'ambiguous reference bar: 2 candidates: ta.dep.bar, ta.other.bar'. ta.import_user, identical but with 'import ta.lib { y }', RESOLVES, binding bar to ta.dep.bar. Found while classifying the cliff gunbc#12741 exposed: an import-bearing file loses all its bare pulls (path_y_fidelity_successor_test lost decode_fidelity_from_target's module when an import was added -- that half was loud).",
"DISTINGUISHING FACTS: the file has at least one import; the bare name is not among the imported members; the file's source tree declares it in two or more modules; exactly one of them is in the file's transitive import closure. The same file with its imports removed refuses.",
"RUNG FOUND AT AND CURRENT RUNG: silent wrongness -- below the ladder, not on it -- and LIVE until the cut named below; no mechanism detects or refuses it today. The pinned specimen records the defect as observed, it does not prevent it. CEILING: structurally guaranteed -- a bare name's meaning is a function of the file's own declarations and the names it explicitly imports, never of what an import transitively reaches. WHY IT CANNOT BE CLOSED ALONE (quiet-gull-780, 2026-09-30): the transitive leak currently MASKS consumer-scope re-resolution of foreign field types -- a field whose declared type is foreign to the reading module is re-resolved by bare name in the reader's scope and today finds its type through the transitively flattened bare-name layer -- so removing that layer by itself breaks generation 2. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: one cut in which EVERY foreign-field-type reader reads the field's declaration identity (Node.declaration, the transition quiet-hawk-702 owns) instead of re-resolving it by name, AND the transitive bare-name layer (build_ancestry_precedence ancestry_str_bindings flattening every import's cache) is removed, so bare names start from the kernel plus direct-import selections. A declared-scope bare-name fix without the declaration-identity migration is narrower than this capability and does not retire the row. Until the cut, the mitigation is the CrossTreeBareReference advice in gunbc#12741: write a cross-tree reference qualified rather than adding an import.",
],

evidence: [],
}
7 changes: 5 additions & 2 deletions src/v1/expected_red_roster_join.dag
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,8 @@ type WitnessEvalVerdict
// WHY A SUPPRESSED ROW IS ITS OWN DISPOSITION AND NOT A NotEvaluated REASON. NotEvaluated says
// the identity was ATTEMPTED and produced no verdict -- host tool missing, hermetic route gap,
// budget interrupt. A suppressed row was never attempted at all: the floor removed it from the
// roster BEFORE the fold, because its module is outside the required gate or the cost-debt roster
// withholds it. Same absence of a verdict, different fact and a different remedy -- one needs a
// roster BEFORE the fold, because its module is outside the required gate, the cost-debt roster
// withholds it, or the changed-witness sublane declined it as a declared BinWitnessWet row. Same absence of a verdict, different fact and a different remedy -- one needs a
// route or a budget, the other needs a gate roster edit or a debt to clear -- so collapsing them
// would be the state-space conflation DESIGN section 5 names.
//
Expand All @@ -73,6 +73,7 @@ type WitnessEvalVerdict
type ExpectedRedSuppressionGround
= OutsideRequiredGate
| WithheldCostDebt
| DeclinedNoCiWetLane

type ExpectedRedJoinDisposition
= StillRed
Expand Down Expand Up @@ -133,13 +134,15 @@ fn suppression_ground_label(ground: ExpectedRedSuppressionGround) -> String {
match ground {
OutsideRequiredGate => "suppressed_outside_required_gate"
WithheldCostDebt => "suppressed_withheld_cost_debt"
DeclinedNoCiWetLane => "suppressed_declined_no_ci_wet_lane"
}
}

fn suppression_ground_detail(ground: ExpectedRedSuppressionGround) -> String {
match ground {
OutsideRequiredGate => "enrolled, but its module is outside the required gate and was never loaded, so this run could not attempt it -- dormant, not deleted"
WithheldCostDebt => "enrolled, but the cost-debt roster withholds it from execution in this run -- dormant, not deleted"
DeclinedNoCiWetLane => "enrolled and changed by this run, but its file is a declared BinWitnessWet row no CI lane executes (gunbc.rung_drop edited_bin_witness_wet_rows_not_executed_by_ci), so the changed-witness sublane declined it -- dormant, not deleted"
}
}

Expand Down
Loading