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
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
module gunbc.recurring_failure_mode.bare_reference_channel_declines_a_pull_in_silence

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

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

receipts: [
"bare reference channel declines a pull in silence: the loader's bare-reference channel decides, per NAME, whether to pull the module that declares it. Every arm that declines is a bare `continue` -- no diagnostic, no count, no record carried past the loader -- so a module whose type reference was declined is simply not compile-clean. It then drops out of the compiled closure into the NAME CENSUS ONLY, the item registry is built over REALIZED modules only, and the first LOUD symptom is `ResolvedCalleeRegistryRowAbsent` (`effect summary incomplete`) raised once per CALLING witness, modules away from the file that carries the defect. DESIGN section 5's absorbing fallback: a precise, located fact (this reference names a module nothing pulled) replaced by a wider, quieter state, with the locating signal destroyed.",

"THE RULE, DERIVED FROM THE LOADER AND NAMED AT ITS OWNING SYMBOLS. There are TWO gates, in this order. GATE ONE, `v1_compiler.cli_run` `build_both_closure_edge_index`: the bare half runs only when `source_declares_import_lines(&source.content)` is FALSE. A single `import` line anywhere in a file turns the ENTIRE bare channel off for that file, for every name in it. GATE TWO, `v1_compiler.cli_run` `visit_bare_reference_providers`: inside the channel a name is pulled only if the census answers `GlobalBareUniqueBinding` (or `closure_bare_disposition` answers `UniqueOnChain`) AND its local `pullable` predicate holds -- the reference is in call position, OR the declaration has params, OR it carries a `type_annotation`, OR its `connective` is not `NoConnective`. Names that are self-declared, explicitly imported, substrate vocabulary (`std_types::kernel_type_set` / `container_type_arity`) or a `test fn`/`test data` row are skipped earlier. `AmbiguousOnChain` is the ONE arm that refuses loudly; every other decline is silent.",

"WHAT THAT MEANS FOR A NULLARY TYPE ALIAS, which is the shape that bit. the branded alias `type ProcessNodeId = NonEmptyStr where brand(...)` has no params, no type_annotation and `NoConnective`, so referencing it in TYPE POSITION satisfies no arm of `pullable` and its module is not pulled. A coproduct (`Disj`) or a record type IS pulled from the same position, because its connective is not `NoConnective`.",

"THE STANDING FACT ABOUT IMPORT LISTS IS HALF TRUE AND THE HALF THAT IS FALSE IS THE DANGEROUS ONE. A `.dag` import list does NOT bind at NAME RESOLUTION -- a name absent from the braces still resolves through the corpus-wide bare census (`v1_compiler.infer_env` `global_bare_fallback_invariant`), which is why an unlisted use is an ADVISORY and not an error. It DOES bind at the LOADER: gate one means the first `import` line an author adds silently switches off bare pulling for every OTHER name in that file. So a partially-imported file is strictly more dangerous than a zero-import one, and 'it has an import header' is not a safety property.",

"THE DISCRIMINATING SET, hermetic: FOUR ENTRIES over seven modules in one source root, at `fixtures/bare_reference_channel/`. One compile each, same invocation, only the entry varying: `gunbc compile --output-dir <tmp> --source-root fixtures/bare_reference_channel --entry fixtures/bare_reference_channel/<name>.dag --target rust`. (1) `bare_record_consumer` -- no imports, bare reference to a RECORD type -- PULLS: the compile is clean and the reference is reported only as an `unlisted import use` advisory. (2) `bare_alias_consumer` -- no imports, bare reference to `type BrcAliasId = Int` -- DOES NOT PULL: the compile REFUSES with `unresolved type BrcAliasId` and the alias home is absent from the resolved closure. The pair differs in exactly the `pullable` condition. (3) `imported_record_consumer` -- the SAME bare reference as (1) plus one unrelated `import` line -- DOES NOT PULL: refuses with `unresolved type BrcRecordId`. The pair (1)/(3) differs in exactly gate one. (4) `transitive_alias_consumer` -- no imports, a bare CALL into a module that imports the alias home -- pulls the CALLEE, and the alias arrives as a passenger of its import closure, so the same alias reference that refuses in (2) compiles clean here. With `GUNBC_BARE_PULL_TRACE=1` a pulled name prints one `[bare-pull]` line naming the census state and a declined name prints nothing, which is the silence this row is about.",

"THE HYPOTHESIS THIS ROW REPLACES, AND WHY IT LOOKED FALSIFIED. gunbc#11940 proposed that alias-shaped references are not pullable and then falsified it on `test.claim.extdeps_version_base`, which reaches `extdeps.version` through the same alias shape and compiles clean. The alias half was RIGHT; the counterexample resolves for a different reason. That witness also bare-references `min_coreutils_version`, a `data` declaration WITH a type annotation, so `pullable` holds, `extdeps.tools.gnu_coreutils` is pulled, and `extdeps.version` arrives as a PASSENGER of that module's import closure. Reproduced hermetically by entry (4) `transitive_alias_consumer`: a bare CALL to a function in a module that imports the alias home resolves the alias, while (2) identical alias reference still refuses. Whether a bare reference resolves is therefore not a property of the reference; it is a property of what ELSE the file happened to name.",

"THE SET IS A DECLARED FRONTIER AND NOT A CONSUMED ONE, stated rather than left to be noticed (DESIGN section 3c). Nothing in the corpus runs these four compiles today: this row is their only reference, so the results above are read by a human running the invocation and by nobody else, and they are recorded as OUTCOMES (pulls / refuses, and which diagnostic) rather than as counts, because a transcribed figure with no producer rots (DESIGN section 6). THE NAMED CONSUMER: an instrument target under `gunbc test //gunbc/instruments:<label>` -- a `gunbc.instrument_targets` label with a `gunbc.target_binding` producer -- that runs the four entries and asserts, per entry, PULLED versus DECLINED plus the refusal identity, so a loader change that moves either gate turns that target red instead of leaving a stale sentence here. ITS TRIGGER: the same loader-side decline record the next-rung trigger below already names -- once a decline is a value rather than a `continue`, the instrument observes it directly instead of inferring it from whether a downstream type resolved, and building the instrument before that carrier exists would wall the SYMPTOM and not the decision. Until it lands the set is evidence a reader re-runs, which is weaker than an enrolled control and is said here in those words.",
"RUNG FOUND AT: 1, mitigatable, and only for the eventual symptom. The unresolved type is reported where it sits, so the file's own compile is loud; what is silent is the DECLINE (no arm of the loader records it) and the DEMOTION (`[census] N indexed modules outside the compile-clean closure enter the name census only` is a COUNT with no identities and no causes). Under a floor run that count is the whole record, and the located reading arrives 13 modules away wearing an effect-modelling error's name.",

"ATTAINABLE CEILING: 3, structurally guaranteed, and it is NOT reachable in the change that authored this row. The condition is decidable -- at the decline the loader holds the file, the name, the declaring module and the reason -- but nothing carries a declined name past the loader, so the resolver that later reports `unresolved type 'X'` cannot say declared by module M, which this file bare channel declined, with the arm named, and the registry-row consumer cannot say callee module M is census-only. The missing thing is a CARRIER, not a check.",

"NEXT-RUNG TRIGGER, at capability grain: a per-file record of every bare-channel decline (name, declining arm, declaring module when the census named one) produced by the loader and CONSUMED by the two downstream reporters -- the unresolved-name diagnostic and the callee-registry join -- sufficient for each to name the unpulled module at the site that failed. A trigger naming only the loader-side record would be satisfied while both distant symptoms stayed unlocated, which is the grain mismatch DESIGN section 4b(3) warns about.",

"THE DEEPER READING, kept separate because it is a proposal and not a measurement: `pullable` is a HEURISTIC standing where a decidable fact was available. The kind of the declaration the census resolved to is known exactly; the predicate instead asks four proxy questions about the node's shape and declines on all-no. DESIGN section 4 rules that in a closed system a heuristic is never necessary, and section 5 names the confidence threshold that selects such an arm as the tell that LOCATES anemic modelling. The principled repair is to pull the declarer of any bare name the census resolved, whatever its shape, and to price the resulting closure growth rather than guess at it -- which is a measured change to closure size across the corpus, not an edit that can ride in on this row.",

"REVIEW TELL: a module with NO import header at all is not tidy, it is on the bare channel; a module with ONE import line has the channel off and is relying on that list being complete. An `unlisted import use` advisory is the loader telling you a name resolved through the census -- for a coproduct or record it also pulled, for an alias it did not. And an `effect summary incomplete` error over a callee whose own module is reported unresolved elsewhere in the SAME run is this class, not an effect-modelling gap.",
],

evidence: [],
}
3 changes: 3 additions & 0 deletions fixtures/bare_reference_channel/alias_home.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module probe.brc.alias_home

type BrcAliasId = Int
3 changes: 3 additions & 0 deletions fixtures/bare_reference_channel/bare_alias_consumer.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module probe.brc.bare_alias_consumer

type BrcAliasCarrier { id: BrcAliasId }
3 changes: 3 additions & 0 deletions fixtures/bare_reference_channel/bare_record_consumer.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module probe.brc.bare_record_consumer

type BrcRecordCarrier { id: BrcRecordId }
5 changes: 5 additions & 0 deletions fixtures/bare_reference_channel/imported_record_consumer.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module probe.brc.imported_record_consumer

import probe.brc.alias_home { BrcAliasId }

type BrcImportedCarrier { id: BrcRecordId }
5 changes: 5 additions & 0 deletions fixtures/bare_reference_channel/passenger_home.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module probe.brc.passenger_home

import probe.brc.alias_home { BrcAliasId }

fn brc_alias_identity(id: BrcAliasId) -> BrcAliasId { id }
3 changes: 3 additions & 0 deletions fixtures/bare_reference_channel/record_home.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module probe.brc.record_home

type BrcRecordId { tag: Int }
3 changes: 3 additions & 0 deletions fixtures/bare_reference_channel/transitive_alias_consumer.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module probe.brc.transitive_alias_consumer

fn brc_transitive(id: BrcAliasId) -> BrcAliasId { brc_alias_identity(id: id) }