Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
23263e2
WIP: bare-name ambiguity wall -- third resolution tier and the refusal
Sep 12, 2026
fd0e916
Give the fixture instrument a claim scope, so the wall's RED is autho…
Sep 12, 2026
11c4112
Use the ungated scope builder: claim_scope_for_without_memos is cfg(t…
Sep 12, 2026
c8322f3
Put each fixture source literal on its own declaration line
Sep 12, 2026
7842dca
Split the wall out: land the claim-scope instrument and its controls …
Sep 12, 2026
e6b56b7
Stop a harness budget refusal from wearing a scope refusal's name
Sep 12, 2026
ba83aad
Let a fixture subject build its scope without taking a floor memo slot
Sep 12, 2026
e445a81
Move the third resolution tier out: it ships where its controls are
Sep 12, 2026
4421cda
Put two relocated rationale receipts back on the symbols they describe
Sep 12, 2026
17f03f6
Stop claiming a call the code cannot make, and delete the reader noth…
Sep 12, 2026
861abdc
Merge main and retire the gunbc#11137 row its trigger came due on
Sep 12, 2026
2b751a9
Stop ScopeAccepted claiming a guarantee this branch does not make
Sep 12, 2026
2fa2d01
Merge main: the #11137 retirement landed there, so drop this branch's…
Sep 12, 2026
971a2ef
Drop a receipt that narrated someone else's deletion and deleted a re…
Sep 12, 2026
be9ae74
Brand the refusal cause NonEmptyStr, and coerce where split reads it
Sep 12, 2026
cf67459
Use the corpus containment authority, and declare the frontier properly
Sep 12, 2026
eb017be
Merge main; rebuild the dispatch projection rather than text-merging it
Sep 12, 2026
58a47bc
Pay the seed-growth receipt for the fixture claim-scope instrument
Sep 13, 2026
9664efc
Narrow the slot-competition commentary to what is actually established
Sep 13, 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
56 changes: 56 additions & 0 deletions dag/gunbc/claim_scope_fixture_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
module gunbc.claim_scope_fixture_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the hand Rust added by giving the fixture instrument a claim scope.
// Authored because gunbc.seed_growth_admission seed_growth_forward_freeze_policy_note makes
// unenumerated hand growth in src/v1 a stop-line, and this change adds four hand items across
// three modules of the seed. Requested by review 64893 on gunbc#11143, which read the change's
// section 3c frontier as answered and the SEED-SIDE receipt as missing -- correctly: the two are
// different questions, and answering "who consumes this .dag type" says nothing about "why is
// this Rust".
//
// WHAT THE CHANGE IS. `claim_scope_for` is where the corpus's bare-name ambiguity census is
// computed, and it is a seed function. The instrument that already exists for multi-module
// fixtures, `compile_dag_multi_module_fixture`, stops at `compile_to_resolved` and never builds a
// scope -- so a wall living in `claim_scope_for` had a positive control that could run and a
// discriminating RED that could not be authored anywhere. This change adds the scope-building
// counterpart of that instrument.
//
// WHY IT IS RUST AND NOT .dag, which is the question this receipt exists to answer honestly. The
// SUBJECT is a seed function. `claim_scope_for` and the `PreparedRepository` it reads are host
// structures with no substrate representation, and a .dag-side re-derivation of the ambiguity
// population would be a SECOND detector beside the census -- free to drift from the one the floor
// prints and the wall refuses on, which is the fork DESIGN section 3 exists to refuse. The
// instrument therefore calls the same `claim_scope_for_with_memos` the floor's own entry point
// calls; it is one detector observed from a fixture, not a copy of one. This is the same boundary
// gunbc.census_memo_seed_growth records one seam over: an instrument about a host builtin is
// co-located with the builtin.
//
// WHAT IS NOT NETTED, and it is named rather than counted against the additions because
// seed_growth_deletions_offset_nothing executes that rule. `claim_scope_for_with_memos` gains a
// `reference_index` parameter and `reference_closure_index` loses its build body to the lifted
// function -- both ExistingSeedItemModified under gunbc.seed_growth_admission
// SeedGrowthChangeDisposition, keeping their names and their behaviour for every production
// caller, which pass `None`. The three generated rows (the dispatch arm, its macro arm and the
// lookup entry in v1_interpreter_dispatch_generated.rs) are projections of
// gunbc.v1.v1_interpreter_primitive_surface and are exempt by generation authority, not by this
// author's say-so.
//
// HAND-ITEM DELTA is derived from the diff by gunbc.rust_item_host_observation and is deliberately
// not restated here: an authored copy of a fact the diff owns is the second representation
// seed_growth_forward_freeze_policy_note measured going wrong on gunbc#9095.
data claim_scope_fixture_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "ClaimScopeFixtureOutcome", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "build_reference_closure_index", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.emit_host", decl_name: "claim_scope_dag_multi_module_fixture", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "claim_scope_fixture_value", field: WholeDeclaration }
],
reason: "A wall in claim_scope_for could not have a discriminating RED without a way to hand the seed a multi-module subject and ask it to build a scope. DESIGN section 4b names exactly this shape: a state unrepresentable in the ACCEPTED corpus may still be representable as SOURCE HANDED TO THE COMPILER BY A FIXTURE, and where that is so, declining the evidence is specification-without-execution. It is measured rather than argued here -- authoring the fixture found a real defect in the resolution tier it controls, one that needs a coproduct-returning function and a contested arm name in one scope and so could not surface from the corpus at all.\n\nWHAT EACH ITEM IS FOR. claim_scope_dag_multi_module_fixture is the instrument: it compiles a caller-authored manifest with no corpus roots and calls the SAME claim_scope_for_with_memos the floor calls. ClaimScopeFixtureOutcome is its typed outcome, and its four arms exist to keep three failures apart that a Bool conflates -- the harness could not measure, the manifest did not compile, the scope refused -- because a control satisfied by ANY refusal goes green on a cause it never observed. claim_scope_fixture_value projects that outcome into the interpreter's value space. build_reference_closure_index is the cache's own body, lifted so a caller can build an index WITHOUT registering it.\n\nTHE LIFT IS A CONTRACT CHANGE, NOT A CAP RAISE, and that was the reviewed alternative. reference_closure_index memoizes per subject in a thread_local bounded by FLOOR_PREPARED_SUBJECTS_PER_PROCESS, and the floor already holds both slots -- so a fixture going through the cache is the third subject and is refused for a reason that says nothing about its manifest. Measured on this branch before the split: the POSITIVE control returned false while the NEGATIVE one passed, thread- and order-dependent, because the memo is thread-local and the floor evaluates claims across workers. Raising the bound so a test instrument fits is the instrument dictating production limits; the fixture builds its own index and occupies no slot.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete all four when claim scope construction is a MODELED operation rather than a seed function -- at which point a fixture subject is an ordinary value in the substrate, the instrument is a .dag fold over it, and a host builtin standing beside it is the duplicated authority this receipt's own single-authority argument refuses. That is the same trigger the sibling fixture instrument carries, and the two migrate together or not at all: leaving one hand-rolled beside a modeled sibling is the fork, not the fix.",
current_boundary: "Confined to one builtin reachable only from .dag, and it decides nothing about the corpus. The instrument reads no corpus root and consults no module index, so its subject is entirely the calling test's manifest; it registers nothing in the per-subject memo, so no floor subject is evicted and no slot is spent; and it returns a projection of what claim_scope_for said rather than a judgment of its own. The only production code it shares is the detector itself, which is the point: a second detector here would be free to drift from the census the floor prints. It changes no verdict for any existing caller -- both production callers of claim_scope_for_with_memos pass None for the new parameter, so the cache path they observe is the body it always ran."
}
79 changes: 79 additions & 0 deletions dag/gunbc/instruments/multi_module_compile_fixture.dag
Original file line number Diff line number Diff line change
Expand Up @@ -236,3 +236,82 @@ fn resolved_rust_fn_lookup(
fn resolved_rust_fn_has_parameter(signature: ResolvedRustFnSignature, parameter_name: String) -> Bool {
signature.ordered_parameter_names |> any(n => n == parameter_name)
}

// BUILDING A CLAIM SCOPE OVER THE SAME MANIFEST, which is a different question from compiling it.
//
// `compile_fixture` above stops at `compile_to_resolved`. The bare-name-ambiguity refusal lives
// in `claim_scope_for` -- the scope builder the required floor calls once per claim module, and
// the same call whose `ambiguous_reads` vector the floor's census lines are printed from. So a
// control written over `compile_fixture` cannot see that refusal at all, and the refusal's
// discriminating RED is not authorable in the CORPUS either: a module carrying a deliberately
// ambiguous read would refuse the whole floor rather than sit in it as a probe. DESIGN section 4b
// answers exactly that shape -- a state unrepresentable in the accepted corpus may still be
// representable as source handed to the compiler by a fixture, and declining to enrol it there is
// specification-without-execution.
//
// ONE DETECTOR, NOT TWO. The host builtin behind this calls `claim_scope_for_with_memos`, the
// same function the floor's own entry point calls. It does not re-derive the ambiguity
// population, so the refusal a control observes IS the refusal the corpus floor raises, from one
// computation. A second copy here -- even a faithful one -- would be the second authority the
// census exists to prevent, and would be free to drift from it silently. What differs from the
// floor's call is the memo arguments, which is a caching decision rather than a semantic one.
//
// THE ENTRY IS A MODULE PATH, not a file path, because that is what `claim_scope_for` is keyed on.
// `cause` is `NonEmptyStr`, matching `MultiModuleCompileFixtureOutcome`'s arm one screen up
// rather than weakening to bare `String` for the same fact. Every producer builds a non-empty
// literal, so the brand costs nothing and makes an empty cause unwritable instead of merely
// unwritten -- §5's construction over validation, applied to a refusal whose whole value is the
// text it carries.
type ClaimScopeFixtureOutcome
= ClaimScopeInstrumentRefused { cause: NonEmptyStr }
| ClaimScopeCompileRefused { blocking_count: Int }
| ClaimScopeRefused { cause: NonEmptyStr }
| ClaimScopeAccepted { module_count: Int }

fn claim_scope_fixture(fixture: MultiModuleCompileFixture, entry_module_path: String) -> ClaimScopeFixtureOutcome {
claim_scope_dag_multi_module_fixture(
fixture.sources |> map(s => s.path as String),
fixture.sources |> map(s => s.content),
entry_module_path
)
}

// AND WHICH REFUSAL IT WAS -- the only refusal reader this instrument offers, deliberately.
//
// A reader that answered "did the scope builder refuse" would say nothing about WHY, and a probe
// satisfied by ANY refusal goes green the day an unrelated one starts firing first, and would
// then be cited as coverage for a cause it never observed. One was written here and deleted
// rather than shipped beside this: two readers, one of them strictly weaker, is an invitation to
// reach for the weaker.
//
// So this reader matches the arm AND requires the cause to name the expected refusal: a red has
// to be the red the caller meant.
//
// Containment through `string_contains`, the corpus authority for this predicate (declared at
// `std.methods` `string_contains_method`, and what the sibling instruments in this directory
// already call). An earlier revision hand-rolled it as `split(..) |> count > 1` and defended that
// as "the idiom the corpus already uses" -- true of the weaker idiom only, and §2's re-invention:
// net concepts must not grow when an authority exists. `cause` is coerced to `String` at the call
// because the `NonEmptyStr` brand establishes no method surface of its own; the brand is worth
// keeping on the FIELD, where it makes an empty cause unwritable, and costs one ascription here.
fn claim_scope_refusal_names(o: ClaimScopeFixtureOutcome, cause_marker: String) -> Bool {
match o {
ClaimScopeRefused { cause: c } => string_contains(s: c as String, pattern: cause_marker)
ClaimScopeAccepted { module_count: n } => false
ClaimScopeCompileRefused { blocking_count: n } => false
ClaimScopeInstrumentRefused { cause: c } => false
}
}

// ACCEPTANCE IS SILENT ABOUT AMBIGUITY. The scope builder COLLECTS ambiguous bare-name reads onto
// the accepted scope; it does not refuse on them. So this reader answers "the entry resolved and
// the scope built", and NOT "the scope is unambiguous" -- a row asserting it establishes nothing
// about that class, and must not be cited as coverage for a refusal that is not in this change.
fn claim_scope_was_accepted(o: ClaimScopeFixtureOutcome) -> Bool {
match o {
ClaimScopeAccepted { module_count: n } => true
ClaimScopeRefused { cause: c } => false
ClaimScopeCompileRefused { blocking_count: n } => false
ClaimScopeInstrumentRefused { cause: c } => false
}
}
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
module gunbc.seed_growth_admission

import gunbc.claim_scope_fixture_seed_growth { claim_scope_fixture_seed_growth_justification }
import gunbc.anonymous_record_resolution_seed_growth { anonymous_record_resolution_seed_growth_justification }
import gunbc.closure_edge_demand_seed_growth { closure_edge_demand_seed_growth_justification }
import gunbc.reference_closure_binder_seed_growth { reference_closure_binder_seed_growth_justification }
Expand Down Expand Up @@ -210,6 +211,7 @@ data seed_growth_admission_g0_population_note: String = "G0 CENSUS HOST: gunbc.r

fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
[
claim_scope_fixture_seed_growth_justification,
anonymous_record_resolution_seed_growth_justification,
floor_non_verdict_seed_growth_justification,
floor_route_gap_seed_growth_justification,
Expand Down
4 changes: 4 additions & 0 deletions dag/gunbc/v1/v1_interpreter_opaque_host_call.dag
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,10 @@ fn v1_interpreter_nested_compile_reaches() -> List<NestedCompileReach> {
arm_identity: "free_call.compile_dag_multi_module_fixture",
nested_compile_entry: "cli_run.emit_host.compile_dag_multi_module_fixture",
},
NestedCompileReach {
arm_identity: "free_call.claim_scope_dag_multi_module_fixture",
nested_compile_entry: "cli_run.emit_host.claim_scope_dag_multi_module_fixture",
},
NestedCompileReach {
arm_identity: "free_call.observe_declared_import_closure_symbol_binding",
nested_compile_entry: "cli_run.observe_declared_import_closure_symbol_binding",
Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/v1/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1222,6 +1222,15 @@ fn v1_interpreter_authored_roster_arms() -> List<InterpreterPrimitiveDispatchArm
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.claim_scope_dag_multi_module_fixture" },
form: FreeCall,
authored_spelling: "claim_scope_dag_multi_module_fixture",
realization_module: "v1_interpreter",
dispatch_symbol: "eval_builtin_inner",
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.compile_dag_reference_occurrence_binding_census" },
form: FreeCall,
Expand Down
Loading
Loading