Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
f10d962
Resource requirements are part of the call contract: the typecheck re…
Sep 22, 2026
1dd3770
Regenerate the stage0 mirrors for the resource-requirement call contr…
Sep 22, 2026
a98ba70
The indexed fn binding carries its uses clause; test roots are admitt…
Sep 22, 2026
6a50d30
Regenerate the stage0 mirrors at the fixed point (second generation e…
Sep 22, 2026
9bf3e08
Merge origin/main into the call-contract lane (union the failure-mode…
Sep 22, 2026
47d42d4
Review 69961: the unestablished-resource arm rendered panic!, and the…
Sep 22, 2026
21330ab
Review 69984: nothing here holds the test-root fork as declared debt,…
Sep 22, 2026
ec7780e
Merge origin/main and regenerate the mirrors from the merged base
Sep 22, 2026
3967e0b
The resource-requirement frontier's 69 rows, discovered by whole-corp…
Sep 22, 2026
300e08d
Canonicalise the resource key on its resolved declaration, and file t…
Sep 22, 2026
fb48be3
The 69 rows re-derived with canonical resource keys
Sep 22, 2026
e4a423b
Merge origin/main: regenerate every mirror, restore the hand-authored…
Sep 22, 2026
4eaad7d
The regenerated emitter mirror grew a field; the hand-authored bin mu…
Sep 22, 2026
355e821
Review 70193: an identified callee whose declaration cannot be read r…
Sep 22, 2026
a3402f1
Merge origin/main; consolidate the ledger row into the one #12055 landed
Sep 22, 2026
b809006
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 23, 2026
5128b43
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 23, 2026
c7d277c
Regenerate the five mirrors the merge driver refused, from the merged…
Sep 23, 2026
30551ac
Author the Network requirement on three callers main landed after the…
Sep 23, 2026
23bc3e1
Frontier-row mismatch diagnostics print the declared and observed cou…
Sep 23, 2026
0e861de
Regenerate v1_std_core.rs for the frontier-count render (fixed point …
Sep 23, 2026
6edf832
Re-derive the resource frontier from the whole-corpus census: 37 diss…
Sep 23, 2026
3632e8a
Regenerate v1_compiler_infer.rs for the re-derived frontier (fixed po…
Sep 23, 2026
180e60c
Author the second ring of propagated resource requirements the verifi…
Sep 23, 2026
bb43b81
A kernel-owned resource has the kernel's identity at the requirement …
Sep 23, 2026
5da26f7
Admit the third propagation ring as frontier rows, and file the maske…
Sep 23, 2026
f1394ce
Regenerate v1_compiler_infer.rs for the kernel-wins resource identity…
Sep 23, 2026
86c4beb
Withdraw the kernel-wins identity repair: the fixture refuted it
Sep 23, 2026
1f472f4
Admit the one site the resource-identity fork refuses as a frontier r…
Sep 23, 2026
574a543
Regenerate v1_compiler_infer.rs: the refuted identity repair withdraw…
Sep 23, 2026
2b38caa
Review 70620: the comparator note and the witness receipt state what …
Sep 23, 2026
fd4878d
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 23, 2026
1739120
Delete the five Filesystem rows #12125 dissolved: their callees no lo…
Sep 23, 2026
8803c75
Repair the frontier list's separators: row deletion left runs of comm…
Sep 23, 2026
9db2241
Regenerate emit_rust and infer mirrors on the merged base with the 38…
Sep 23, 2026
6e69eb4
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 23, 2026
afcba0f
Shrink to the emitter-side repair: D13 owns whether a caller establis…
Sep 23, 2026
9db55f8
Review 70670: the kept fold matches by DeclarationRef, so mixed spell…
Sep 23, 2026
6c1d50d
Regenerate v1_compiler_infer.rs and v1_std_core.rs from the shrunk au…
Sep 23, 2026
7b8adaa
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 23, 2026
836e8d9
Regenerate the four mirrors the merge driver refused, from the merged…
Sep 23, 2026
c5895c9
Merge remote-tracking branch 'origin/main' into session/smart-tern-891
Sep 24, 2026
49841fe
Regenerate the mirrors the merge with #12034/#12070 refused (stable a…
Sep 24, 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
@@ -0,0 +1,28 @@
module gunbc.recurring_failure_mode.a_sibling_refusal_masks_a_ratchet_rows_observation

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

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

receipts: [
"**an equality ratchet row reads observed=0 and is deleted as dissolved, while the debt it counts is still present: a SIBLING refusal on the same caller fired first and the row's own requirement was never evaluated.** The deletion looks like the ratchet working in the shrinking direction, so nothing flags it.",

"SPECIMEN, gunbc#12047, 2026-09-23. The whole-corpus census re-deriving the resource-requirement frontier gunbc#12047 carried (withdrawn in that PR when D13 was ruled the authority) read 0 for the Filesystem row on gunbc.instruments.github_app_acquire census_app_acquisition_receipt_for, and the row was deleted with 36 others. The caller also carried an unestablished NETWORK requirement, refused first. Once Network was authored, the next census refused the same caller for Filesystem: the debt had never dissolved.",

"CORRECTION, AND WHICH PART EACH CAUSE PRODUCED. The ring-3 census then refused that caller for Filesystem EVEN AFTER it declared `uses ... fs: std.resources.Filesystem`, which masking cannot explain. A two-module fixture located a second cause in the requirement join itself: v1.compiler.infer resource_declaration_identity compared the node each side's spelling resolved to, and a bare `Filesystem` resolves to the kernel-minted node while `std.resources.Filesystem` resolves to the corpus declaration, so a qualified callee refused every caller. The callee here, gunbc.github_app_acquisition census_app_acquisition_standing, spells its requirement qualified. So the specimen is two defects: the MASKING (the Network refusal hid the Filesystem evaluation in census 1, a real instance of this class) and the IDENTITY FORK (the Filesystem refusal persisted in census 3 because the join could not see the caller's binding), REPAIRED ON gunbc#12047 after a first attempt was refuted. The kernel-wins precedence predicate (overlay_skips_kernel_name) did NOT fix it -- Filesystem is not in std.types kernel_type_set -- and the fixture refuted that attempt, which was withdrawn. The stand-in was minted by v1.compiler.infer nominal_ref_node (via local_binding_for_item / nominal_type_ref); neat-lynx-128 located it and built the repair (parked as #12174), which #12047 carries: the stand-in now carries its declaration's spans and the join compares DeclarationRef. Measured by neat-lynx-128 over per-module compiles of the frontier's caller modules, 8 Filesystem frontier rows observed 0 once the join compared DeclarationRef: those were false refusals from the caller-environment re-lookup, not debt.",

"A SECOND, RELATED SHAPE, from the same re-derivation: authoring a `uses` clause on a caller moves the requirement to that caller's callers, and one census reports only the ring it can see. Closing the propagation took one whole-corpus run per ring (three runs of about 20 minutes and 16 GiB each), where a derivation of the requirement's closure over the call graph would have answered in one.",

"RECOGNITION RULE. Any ratchet whose observation for one key is produced only when no other refusal on the same subject fires first. Ask: is observed=0 a reading of the key, or the absence of a reading? A deletion is safe only when the subject carries no other unestablished requirement at the same boundary.",

"RUNG FOUND AT: SILENT WRONGNESS (a debt row deleted while its debt stood; caught only because a later run re-evaluated the caller). RUNG NOW: MITIGATABLE, because the re-derivation re-runs after authoring. ATTAINABLE CEILING: MECHANICALLY PREVENTABLE, since both halves are decidable. NEXT TRIGGER: a census that evaluates every requirement of a caller independently of its siblings' refusals and reports observed per key as a reading, not an absence. For the second shape, the trigger is a resource-requirement closure derived over the call graph, sufficient to name every caller a new `uses` clause will reach before the edit lands.",
],

evidence: [
DeclarationRef { module_path: "v1.compiler.infer", decl_name: "established_resource_binding", field: WholeDeclaration },
DeclarationRef { module_path: "gunbc.emit_stage_blocking_population_census", decl_name: "census_run_invocation", field: WholeDeclaration },
],
}
Original file line number Diff line number Diff line change
Expand Up @@ -271,6 +271,7 @@ data accepted_source_emits_uncompilable_target: RecurringFailureMode = Recurring

"THREE THINGS THE ABOVE KEEPS APART, because collapsing them is how a refresh cadence gets mistaken for a wall. (1) OBSERVATION: an on-demand run exposes a failure -- what the instrument does when someone invokes it. (2) REGRESSION PROTECTION: an applicable REQUIRED acceptance consumer stops the failure landing unnoticed -- which needs a phase that emits a closure AND COMPILES it, with the target compiler's refusal reaching the lane, not merely a phase that emits. (3) FRONTIER TRUTH: a standing derived from evidence applicable to the claimed subject and contract. gunbc.compiler_frontend_program_status reported SelfHostCorpusEmitsCleanly as Clear across the 2026-09-20/21 window while the capability was down, which is DESIGN section 4b(1) rung inflation -- but the repair for (3) is NOT a refresh cadence: a recent receipt can describe the wrong subject, and an older receipt stays applicable while its relevant inputs are demonstrably unchanged. Applicability, not recency, is what (3) needs.",

"OCCURRENCE, 2026-09-22 (smart-tern-891, template-to-.dag call contract lane, gunbc#12047). A declaration `fn reads(path: String) -> String uses fs: Filesystem` called from `fn plain(path: String) -> String { reads(path: path) }` was accepted with zero blocking diagnostics and emitted `reads(path.clone(), &fs).await?` inside a synchronous fn that binds no `fs`: v1.compiler.emit_rust emit_typed_call appended the CALLEE's resource binding name unconditionally. Arity agreed; the argument named nothing in the caller's scope. REPAIRED AT THE EMITTER, AT RUNG 2 AND NO HIGHER: emit_typed_call now asks v1.compiler.infer established_resource_binding for the CALLER's binding of each requirement, matched by resolved resource declaration, and renders a located compile_error! where there is none, so the target compiler refuses the artifact instead of accepting a call to an unbound identifier. THE ARTIFACT IS STILL WRITTEN: nothing refuses before publishing. Executing evidence: test.claim.resource_requirement_call_admission_witness (two reds that agree on arity and render the located refusal, one with no resource and one with the WRONG resource; a positive control whose caller binds the resource under a different name and emits `&filesystem`; a boundary control). A TYPECHECK WALL WAS BUILT AND WITHDRAWN, and the reason is the next trigger: it required every caller to AUTHOR a `uses` clause, which is the E1b migration DESIGN D13 superseded (dag/gunbc/plans/demand_engine_program.dag) -- under D13 a transparent function's dependency demand is DERIVED, not authored, and #12125 deleted 174 authored rows as restatements. NEXT-RUNG TRIGGER, A CAPABILITY: D13's DependencyDemand carrier, derived per resource DECLARATION (and logical subject) and carrying a binding identity the emitter can pass -- sufficient that a call whose caller's derived demand does not cover its callee's requirement refuses at the typecheck, before emission, and that a derived caller receives a binding rather than the compile_error! arm. IDENTITY BY DECLARATION, NOT BY NODE: a first version of the kept fold compared resolved NODES, and a bare resource name resolved to a kernel-spanned stand-in (v1.compiler.infer nominal_ref_node) while `std.resources.X` resolved to the declaration, so a caller and callee that spelled one resource differently rendered compile_error! where main had compiled (review 70670). The fold now reads the DeclarationRef off the node resolution selected in the declaring module (v1.compiler.infer resource_declaration_identity over v1.compiler.infer_env declaration_ref_of_type_node), and the stand-in carries its declaration's spans; the repair was built by neat-lynx-128 (parked as #12174) and is witnessed by the spelling-fork pair in test.claim.resource_requirement_call_admission_witness.",
],


Expand Down
117 changes: 117 additions & 0 deletions dag/test/claim/resource_requirement_call_admission_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
module test.claim.resource_requirement_call_admission_witness

import std.types { String, Bool }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly


// A RESOURCE ARGUMENT AT A CALL SITE IS THE CALLER'S BINDING, OR A LOCATED REFUSAL -- NEVER THE
// CALLEE'S SPELLING. The subject is v1.compiler.emit_rust emit_typed_call, which asks
// v1.compiler.infer established_resource_binding for the caller's binding of each resource the
// callee requires. Before it, the emitter appended the CALLEE's binding name: the emitted call agreed
// with the declaration on arity while its argument named nothing in the caller's scope (measured
// 2026-09-22: `reads(path.clone(), &fs).await?` inside a synchronous fn that binds no `fs`).
//
// RUNG, STATED HONESTLY: MECHANICALLY PREVENTABLE (2). An unestablished requirement renders a
// located compile_error!, so the target compiler refuses the artifact -- but the artifact is still
// WRITTEN, and nothing refuses before publishing. The typecheck wall that would have refused
// earlier was withdrawn because whether a caller ESTABLISHES a resource is owned by D13's derived
// DependencyDemand, which does not exist yet; its return is the next-rung trigger on
// gunbc.recurring_failure_mode accepted_source_emits_uncompilable_target.

// THE CALLEE, shared by every row: one parameter, one resource requirement.
data callee_source: String = "fn reads(path: String) -> String uses fs: Filesystem {\n filesystem_read(path)\n}\n"

// RED 1: arity agrees, no resource established. The pre-repair emitter published this.
data red_plain_caller_source: String = "module probe_resource_plain_caller\nimport std.types { String }\nimport std.resources { Filesystem }\nfn reads(path: String) -> String uses fs: Filesystem {\n filesystem_read(path)\n}\nfn plain(path: String) -> String {\n reads(path: path)\n}\n"

// RED 2: arity agrees, the caller establishes a resource -- the WRONG one. A wall that only asked
// "does the caller have any `uses`" admits this; the declaration-identity comparison refuses it.
data red_wrong_resource_caller_source: String = "module probe_resource_wrong_caller\nimport std.types { String }\nimport std.resources { Filesystem, Network }\nfn reads(path: String) -> String uses fs: Filesystem {\n filesystem_read(path)\n}\nfn networked(path: String) -> String uses net: Network {\n reads(path: path)\n}\n"

// GREEN CONTROL: the caller establishes the same resource under a DIFFERENT binding name and spells
// the type by its qualified path. Name comparison would refuse this; declaration comparison admits it.
data green_renamed_binding_caller_source: String = "module probe_resource_renamed_caller\nimport std.types { String }\nimport std.resources { Filesystem }\nfn reads(path: String) -> String uses fs: Filesystem {\n filesystem_read(path)\n}\nfn forwards(path: String) -> String uses filesystem: std.resources.Filesystem {\n reads(path: path)\n}\n"

// BOUNDARY CONTROL: a callee with no requirement is callable from a plain fn, so the wall is
// about the requirement and not about calls in general.
data green_no_requirement_source: String = "module probe_resource_no_requirement\nimport std.types { String }\nfn plain_reads(path: String) -> String {\n path\n}\nfn plain(path: String) -> String {\n plain_reads(path: path)\n}\n"

test fn a_plain_callers_emitted_call_is_a_located_refusal_not_the_callees_spelling() -> Bool {
compile_dag_rust_emit_check(
red_plain_caller_source,
"src/probe_resource_plain_caller.rs",
["compile_error!(", "requires resource fs that the calling declaration does not establish"],
["&fs)"]
)
}

test fn a_wrong_resource_callers_emitted_call_is_a_located_refusal_by_declaration_identity() -> Bool {
compile_dag_rust_emit_check(
red_wrong_resource_caller_source,
"src/probe_resource_wrong_caller.rs",
["compile_error!(", "requires resource fs that the calling declaration does not establish"],
["&fs)"]
)
}

// POSITIVE CONTROL: the caller establishes the same resource under a DIFFERENT binding name, and
// the emitted call carries the CALLER's binding.
test fn the_emitted_call_passes_the_callers_binding_not_the_callees_spelling() -> Bool {
compile_dag_rust_emit_check(
green_renamed_binding_caller_source,
"src/probe_resource_renamed_caller.rs",
["reads(path.clone(), &filesystem).await?", "filesystem: &Filesystem"],
["&fs)", "compile_error!("]
)
}

// BOUNDARY CONTROL: a callee with no requirement emits an ordinary call, so the arm is about the
// requirement and not about calls in general.
test fn a_callee_without_a_requirement_emits_an_ordinary_call() -> Bool {
compile_dag_rust_emit_check(
green_no_requirement_source,
"src/probe_resource_no_requirement.rs",
["plain_reads("],
["compile_error!("]
)
}

// THE SPELLING-FORK PAIR (review 70670; the repair ported from neat-lynx-128's parked #12174). The
// callee spells its requirement QUALIFIED and the caller spells it BARE, under the same binding name.
// On main the emitter passed the callee's name and this compiled; with the join comparing resolved
// NODES it rendered compile_error!, because a bare name resolved to a kernel-spanned stand-in and the
// qualified one to the declaration. Identity is now the DeclarationRef recovered from the resolved
// node. The bare/bare row must stay admitted, and a qualified callee whose caller establishes a
// DIFFERENT resource must still refuse -- identity, not spelling-blindness, is what admits the pair.
data green_qualified_callee_bare_caller_source: String = "module probe_resource_spelling_fork\nimport std.types { String }\nimport std.resources { Filesystem }\nfn reads(path: String) -> String uses fs: std.resources.Filesystem {\n filesystem_read(path)\n}\nfn forwards(path: String) -> String uses fs: Filesystem {\n reads(path: path)\n}\n"
data green_bare_callee_bare_caller_source: String = "module probe_resource_bare_bare\nimport std.types { String }\nimport std.resources { Filesystem }\nfn reads(path: String) -> String uses fs: Filesystem {\n filesystem_read(path)\n}\nfn forwards(path: String) -> String uses fs: Filesystem {\n reads(path: path)\n}\n"
data red_qualified_callee_other_bare_resource_source: String = "module probe_resource_spelling_fork_wrong\nimport std.types { String }\nimport std.resources { Network }\nfn reads(path: String) -> String uses fs: std.resources.Filesystem {\n filesystem_read(path)\n}\nfn networked(path: String) -> String uses net: Network {\n reads(path: path)\n}\n"

test fn a_bare_caller_passes_its_binding_to_a_qualified_callee() -> Bool {
compile_dag_rust_emit_check(
green_qualified_callee_bare_caller_source,
"src/probe_resource_spelling_fork.rs",
["reads(path.clone(), &fs).await?"],
["compile_error!("]
)
}

test fn a_bare_caller_passes_its_binding_to_a_bare_callee() -> Bool {
compile_dag_rust_emit_check(
green_bare_callee_bare_caller_source,
"src/probe_resource_bare_bare.rs",
["reads(path.clone(), &fs).await?"],
["compile_error!("]
)
}

test fn a_caller_of_a_different_resource_still_refuses_a_qualified_callee() -> Bool {
compile_dag_rust_emit_check(
red_qualified_callee_other_bare_resource_source,
"src/probe_resource_spelling_fork_wrong.rs",
["compile_error!(", "requires resource fs that the calling declaration does not establish"],
["&fs)"]
)
}
4 changes: 2 additions & 2 deletions src/v1/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -710,8 +710,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
MethodExistenceFrontierAdmitted { method: m, receiver_type: t, trigger: tr, span: _ } => concat("method '", m, "' on receiver type '", t, "' is admitted by a declared unresolved-method frontier row; dissolves on: ", tr)
AlgebraApplicationEvidenceUnavailable { receiver_type: t, argument_index: i, span: _ } => concat("algebra receiver application evidence unavailable for '", t, "' at argument ", to_string(value: i), ": structural members are not type arguments")
ReceiverTypeUnestablished { method: _, span: _ } => "the receiver's own type was never established, so nothing is known about the method's existence here; this is an upstream type-propagation deficit, not a fact about the method"
FrontierOccurrenceBudgetExceeded { method: m, receiver_type: t, declared: _, observed: _, span: _ } =>
concat(concat(concat("the declared frontier row for '", m), concat("' on receiver type '", t)), "' no longer matches what this module contains: its declared occurrence count and the count observed here differ, and both numbers are carried on this diagnostic. If MORE were observed, a new unresolved call has appeared and the receiver's type should be established rather than the count raised. If FEWER were observed, the deficit has partly dissolved and the row must be lowered or deleted so the ratchet keeps its new ground. The count is an equality, not a ceiling, in both directions.")
FrontierOccurrenceBudgetExceeded { method: m, receiver_type: t, declared: d, observed: o, span: _ } =>
concat(concat(concat("the declared frontier row for '", m), concat("' on receiver type '", t)), concat(concat("' no longer matches what this module contains: the row declares ", to_string(value: d)), concat(" occurrence(s) and ", to_string(value: o))), " were observed here. If MORE were observed, a new unresolved call has appeared and the receiver's type should be established rather than the count raised. If FEWER were observed, the deficit has partly dissolved and the row must be lowered or deleted so the ratchet keeps its new ground. The count is an equality, not a ceiling, in both directions.")
TestCodeReferenced { referrer: r, target: t, span: _ } => concat("'", r, "' references test code '", t, "': a `test` declaration is entered only by the witness runner, so no declaration may call, name or import it. Move shared logic into an ordinary fn, or delete a test that only re-asserts other tests")
TestCodeReferenceAdmitted { referrer: r, target: t, span: _ } => concat("'", r, "' references test code '", t, "'; admitted by the declared test-reference debt ledger (v1.compiler.compile test_reference_debt), which may only shrink")
TestCodeReferenceRowOrphaned { referrer: r, span: _ } => concat("the test-reference debt row for '", r, "' names a module that no longer exists in the corpus: it is neither compiled here nor in the loaded name census. A row that can never be observed again must be deleted, not left to persist")
Expand Down
Loading