From c5ed10a98ee7f03e2c8bd4cab1d416ed3862693b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 01:09:25 +0000 Subject: [PATCH 1/3] A lexical binding holding a named function now shadows the free function sharing its spelling MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit THE DEFECT. A call site spelling a name held by BOTH a local binding and a module-level free function reached the FREE FUNCTION whenever the local's value was a reference to a named top-level function. Where the two arities differ the call refuses loudly; where they agree it returns a plausible wrong value with no diagnostic at all -- below floor (DESIGN §5), not a naming nuisance. THE AXIS WAS THE VALUE VARIANT, NOT THE BINDING FORM. `eval_call`'s lexical gate matched `Value::Closure` only, so the law held for a local bound to a LAMBDA and failed for a local bound to a NAMED function, which evaluates to `Value::Fn`. That is exactly the 3x2 grid two lanes measured independently (let / parameter / pattern x named-fn / lambda): three cells wrong, three cells right, and the column that separated them is the one the gate was matching on. THE REPAIR. The gate now names the concept -- a lexical binding holding something callable -- instead of one of its representations. A `Value::Fn` binding is carried as the resolved callee through the same downstream dispatch (witness, parse-table memo, pure memo) rather than short-circuiting, so memoization is unchanged; only the tier that answers the spelling moves. The env re-lookup that used to sit BELOW `ctx.lookup_fn` is deleted rather than kept beside the gate: it was the lower-rung duplicate of the same decision, and reaching it at all required the free-function table to have answered first. MEASURED BY EXECUTION, not by typecheck. `v2.test.claim.local_binding_shadow` under `claim_batch --hermetic` over the whole tree: the enrolled red `local_named_function_binding_is_what_the_call_reaches` PASSES, and all three green controls (the lambda column, the call-site rename, the uncollided binding) still PASS -- so the repair is not a widening that swallowed its own controls. The expected-red enrolment is deleted with its dissolution receipt in place. The witness is NOT deleted with it: DESIGN §4b(4) keeps the discriminating evidence, so the probe stays enrolled as a permanent regression control. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01GqJoJVKcVjG7yk9zZ81PSu --- src/v1/stage0/src/v1_interpreter.rs | 72 ++++++++++++++++---------- src/v2/workflow/floor_expected_red.dag | 50 +++++++----------- 2 files changed, 64 insertions(+), 58 deletions(-) diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index b82759a8979..26390288b3c 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -5281,42 +5281,60 @@ fn eval_call(node: &Rc, env: &Rc, ctx: &InterpContext) -> InterpResul .collect::>()?; // A LEXICAL BINDING SHADOWS EVERY NAME-KEYED TIER (nearest-first precedence, the same law - // 04_infer states at call_locals_shadow_note and now applies to the builtin tiers too). A - // parameter or let named `lookup`, `count`, `filter`, ... is a function VALUE, and answering - // its call from the builtin table by spelling calls a different function than the program - // names -- silently, wherever the two arities happen to agree. `ctx.lookup_fn` (module-level - // declarations) deliberately stays BELOW the builtins as before: this moves the lexical tier - // only. - if let Some(closure @ Value::Closure { .. }) = env.lookup(ctx.sym(&func_name)) { - let closure = closure.clone(); - let arg_vals: Vec = args.iter().map(|(_, v)| v.clone()).collect(); - return apply_closure(&closure, &arg_vals, env, ctx); - } + // 04_infer states at call_locals_shadow_note). A parameter or let named `lookup`, `count`, + // `filter`, ... is a function VALUE, and answering its call from the builtin table -- or from + // the module free-function table -- by spelling calls a different function than the program + // names, silently, wherever the two arities happen to agree. + // + // THE GATE IS THE BINDING, NOT THE VALUE'S REPRESENTATION. It formerly matched `Value::Closure` + // only, so the law held for a local bound to a LAMBDA and failed for a local bound to a NAMED + // top-level function -- which evaluates to `Value::Fn` (see the `ItemKind::FuncItem | FnItem` + // arm of `eval_expr`'s identifier path), falls past every tier here, and is answered by + // `ctx.lookup_fn` below at the FREE FUNCTION sharing its spelling. Measured on a complete + // 3x2 grid (let / parameter / pattern x named-fn / lambda) in + // `v2.test.claim.local_binding_shadow`: the three named-fn cells reached the free function, + // the three lambda cells reached the local. The axis was the VALUE VARIANT this gate matched + // on, and the two variants are one concept -- a lexical binding holding something callable -- + // so the gate now names that concept instead of one of its representations. + // + // `ctx.lookup_fn` (module-level declarations) stays BELOW the builtins as before: this widens + // the lexical tier only, and does not reorder anything under it. + let lexically_bound_fn: Option> = match env.lookup(ctx.sym(&func_name)) { + Some(closure @ Value::Closure { .. }) => { + let closure = closure.clone(); + let arg_vals: Vec = args.iter().map(|(_, v)| v.clone()).collect(); + return apply_closure(&closure, &arg_vals, env, ctx); + } + Some(Value::Fn { node: bound_fn }) => Some(bound_fn.clone()), + _ => None, + }; - v1_bridge_family_arms!(v1_bridge_dispatch, func_name, args, node, ctx); + if lexically_bound_fn.is_none() { + v1_bridge_family_arms!(v1_bridge_dispatch, func_name, args, node, ctx); - v1_native_intercept_arms!(v1_native_intercept_dispatch, func_name, args, env, ctx); + v1_native_intercept_arms!(v1_native_intercept_dispatch, func_name, args, env, ctx); - if let Some(result) = eval_builtin(&func_name, &args, ctx)? { - return Ok(result); + if let Some(result) = eval_builtin(&func_name, &args, ctx)? { + return Ok(result); + } } - let fn_node = if let Some(node) = ctx.lookup_fn(&func_name) { - node.clone() - } else { - match env.lookup(ctx.sym(&func_name)) { - Some(Value::Fn { node }) => node.clone(), - Some(closure @ Value::Closure { .. }) => { - let closure = closure.clone(); - let arg_vals: Vec = args.iter().map(|(_, v)| v.clone()).collect(); - return apply_closure(&closure, &arg_vals, env, ctx); - } - _ => { + // Every callable lexical binding was served by the gate above, so this tier reads the module + // free-function table and nothing else. The env re-lookup that used to sit in the `else` arm + // here -- serving `Value::Fn` and `Value::Closure` AFTER `ctx.lookup_fn` had already been + // asked -- is deleted rather than kept beside the gate: it is the lower-rung duplicate of the + // same decision (DESIGN §2/§3), and it is precisely where the shadowing defect landed, + // because reaching it at all required the free-function table to have answered first. + let fn_node = match lexically_bound_fn { + Some(node) => node, + None => match ctx.lookup_fn(&func_name) { + Some(node) => node.clone(), + None => { return Err(InterpError::NoSuchFunction { name: func_name.clone(), }); } - } + }, }; if let Some(result) = try_witness_evaluation_dispatch(ctx, node, &fn_node, &args, env) { diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 735815df85e..bbc15f8e299 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -543,39 +543,27 @@ fn floor_expected_red_chunk_21() -> List { Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_extra_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_missing_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_wrong_argument_type_must_refuse_at_compile", tail: Cons { head: "test.claim.fabric_cell_evidence_algebra_witness.evidence_full_value_is_order_independent", tail: Empty {} } } } } } -// ONE IDENTITY ENROLLED 2026-08-25, and it carries a per-row reason because the nine rows this -// lane just examined do not, and that absence is what let a thrown claim be filed as a semantic -// red for weeks. -// -// THE CLASS: a call site spelling a name held by BOTH a local binding and a module-level free -// function reaches the FREE FUNCTION when the local's value is a reference to a named top-level -// function. Measured on a complete grid by two lanes independently -- let, parameter and pattern -// bindings all behave the same, and a local bound to a LAMBDA reaches the local -- so the binding -// form is not the axis and the value is. The collision is decided at the CALL SITE by the spelling -// used there: the same value handed to a differently-named parameter reaches the local, which is -// why a rename repairs it. -// -// WHY BELOW FLOOR RATHER THAN A NAMING HAZARD: where the shadowing symbol's arity DIFFERS the call -// refuses loudly, and where it AGREES a plausible wrong value is returned with no diagnostic. -// Reproduced twice on live corpus symbols before the fixture existed -- a displaced predicate -// returning a ParagraphBlock, and a fold over three elements answering 3 where the direct fold -// counts 2. -// -// THE ROW ASSERTS THE DESIRED LAW, not today's behaviour, so it reds now and greens on repair. Its -// three conjuncts return Bools and never throw, so this is an OBSERVED semantic red and never -// no-verdict debt. -// -// DISSOLUTION: it FLIPS TO A PERMANENT REGRESSION CONTROL when local bindings win, and is not -// deleted then. DESIGN 4b(4) -- a climb dissolves the lower-rung production machinery and KEEPS -// the discriminating evidence; deleting the probe on repair would recreate -// specification-without-execution one rung up. Its two green controls (the lambda column and the -// call-site rename) are already permanent for the same reason. -fn floor_expected_red_chunk_22() -> List { - Cons { head: "v2.test.claim.local_binding_shadow.local_named_function_binding_is_what_the_call_reaches", tail: Empty {} } -} +// CHUNK 22 IS DELETED, AND THIS IS ITS DISSOLUTION RECEIPT RATHER THAN A GAP. +// +// The identity enrolled here on 2026-08-25 was +// `v2.test.claim.local_binding_shadow.local_named_function_binding_is_what_the_call_reaches`, +// and it asserted the DESIRED law rather than the behaviour of the day: a call site spelling a +// name held by BOTH a local binding and a module-level free function must reach the LOCAL. It +// reached the free function whenever the local's value was a reference to a named top-level +// function -- silently returning a plausible wrong value wherever the two arities agreed. +// +// THE RESOLVER IS REPAIRED, so the row PASSES and its enrolment is deleted. Leaving it here would +// be the roster's stale-quarantine arm firing on a red that no longer exists, which is exactly +// what that arm is for and exactly what an enrolment must not outlive. +// +// THE WITNESS IS NOT DELETED WITH IT. DESIGN 4b(4): a climb dissolves the lower-rung production +// machinery and KEEPS the discriminating evidence, so the probe stays enrolled in the ordinary +// witness roster as a PERMANENT REGRESSION CONTROL, alongside the three green controls it always +// carried (the lambda column, the call-site rename, and the uncollided binding). Deleting the +// probe on repair would recreate specification-without-execution one rung up. fn floor_expected_red_chunks() -> List> { - Cons { head: floor_expected_red_chunk_00(), tail: Cons { head: floor_expected_red_chunk_01(), tail: Cons { head: floor_expected_red_chunk_02(), tail: Cons { head: floor_expected_red_chunk_03(), tail: Cons { head: floor_expected_red_chunk_04(), tail: Cons { head: floor_expected_red_chunk_05(), tail: Cons { head: floor_expected_red_chunk_06(), tail: Cons { head: floor_expected_red_chunk_07(), tail: Cons { head: floor_expected_red_chunk_08(), tail: Cons { head: floor_expected_red_chunk_09(), tail: Cons { head: floor_expected_red_chunk_10(), tail: Cons { head: floor_expected_red_chunk_11(), tail: Cons { head: floor_expected_red_chunk_12(), tail: Cons { head: floor_expected_red_chunk_13(), tail: Cons { head: floor_expected_red_chunk_14(), tail: Cons { head: floor_expected_red_chunk_15(), tail: Cons { head: floor_expected_red_chunk_16(), tail: Cons { head: floor_expected_red_chunk_17(), tail: Cons { head: floor_expected_red_chunk_18(), tail: Cons { head: floor_expected_red_chunk_19(), tail: Cons { head: floor_expected_red_chunk_20(), tail: Cons { head: floor_expected_red_chunk_21(), tail: Cons { head: floor_expected_red_chunk_22(), tail: Empty {}}}}}}}}}}}}}}}}}}}}}}}} + Cons { head: floor_expected_red_chunk_00(), tail: Cons { head: floor_expected_red_chunk_01(), tail: Cons { head: floor_expected_red_chunk_02(), tail: Cons { head: floor_expected_red_chunk_03(), tail: Cons { head: floor_expected_red_chunk_04(), tail: Cons { head: floor_expected_red_chunk_05(), tail: Cons { head: floor_expected_red_chunk_06(), tail: Cons { head: floor_expected_red_chunk_07(), tail: Cons { head: floor_expected_red_chunk_08(), tail: Cons { head: floor_expected_red_chunk_09(), tail: Cons { head: floor_expected_red_chunk_10(), tail: Cons { head: floor_expected_red_chunk_11(), tail: Cons { head: floor_expected_red_chunk_12(), tail: Cons { head: floor_expected_red_chunk_13(), tail: Cons { head: floor_expected_red_chunk_14(), tail: Cons { head: floor_expected_red_chunk_15(), tail: Cons { head: floor_expected_red_chunk_16(), tail: Cons { head: floor_expected_red_chunk_17(), tail: Cons { head: floor_expected_red_chunk_18(), tail: Cons { head: floor_expected_red_chunk_19(), tail: Cons { head: floor_expected_red_chunk_20(), tail: Cons { head: floor_expected_red_chunk_21(), tail: Empty {}}}}}}}}}}}}}}}}}}}}}}} } // Mock-totality's 21 expected-red rows were stale-quarantined by the explicit-import From 4d73a0e2b26397ef46efd952e2ff3e3ea226b63e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 02:58:52 +0000 Subject: [PATCH 2/3] wip: multi-module fixture --- .../v1_interpreter_primitive_surface.dag | 9 + ...ti_module_compile_fixture_witness_test.dag | 215 +++++++++++++++++ dag/tools/multi_module_compile_fixture.dag | 84 +++++++ src/v1/04_method.dag | 3 + src/v1/stage0/src/cli_run.rs | 224 ++++++++++++++++-- src/v1/stage0/src/v1_compiler_infer_method.rs | 14 ++ src/v1/stage0/src/v1_interpreter.rs | 80 +++++++ .../src/v1_interpreter_dispatch_generated.rs | 3 + .../local_binding_shadow_compile_test.dag | 92 +++++++ .../test/claim/local_binding_shadow_peer.dag | 17 ++ .../test/claim/local_binding_shadow_test.dag | 127 +++++++++- src/v2/workflow/floor_expected_red.dag | 36 ++- 12 files changed, 885 insertions(+), 19 deletions(-) create mode 100644 dag/test/claim/multi_module_compile_fixture_witness_test.dag create mode 100644 dag/tools/multi_module_compile_fixture.dag create mode 100644 src/v2/test/claim/local_binding_shadow_compile_test.dag diff --git a/dag/gunbc/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1_interpreter_primitive_surface.dag index 42d2ee338db..9375832bdc0 100644 --- a/dag/gunbc/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1_interpreter_primitive_surface.dag @@ -1048,6 +1048,15 @@ fn v1_interpreter_authored_roster_arms() -> List MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { + sources: [fixture_source("mmfx/peer.dag", peer), fixture_source("mmfx/entry.dag", entry)], + entry: "mmfx/entry.dag" + }) +} + +fn three_module_run() -> MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { + sources: [ + fixture_source("mmfx/peer.dag", peer_source), + fixture_source("mmfx/third.dag", third_source), + fixture_source("mmfx/entry.dag", entry_source) + ], + entry: "mmfx/entry.dag" + }) +} + +fn entry_names_no_supplied_source_run() -> MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { + sources: [fixture_source("mmfx/peer.dag", peer_source)], + entry: "mmfx/absent.dag" + }) +} + +fn empty_manifest_run() -> MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { sources: [], entry: "mmfx/entry.dag" }) +} + +fn duplicate_path_run() -> MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { + sources: [ + fixture_source("mmfx/entry.dag", entry_source), + fixture_source("mmfx/entry.dag", entry_source_perturbed) + ], + entry: "mmfx/entry.dag" + }) +} + +// --------------------------------------------------------------------------- +// Readers. Each MATCHES the coproduct, so no reader can hand a caller a diagnostic list the +// instrument never produced. + +fn completed_with_no_diagnostics(o: MultiModuleCompileFixtureOutcome) -> Bool { + match o { + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => + count(rows) == 0 && count(files) > 0 && n > 0, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false, + FixtureInstrumentRefused { cause: c } => false + } +} + +fn refused_with_class(o: MultiModuleCompileFixtureOutcome, wanted: String) -> Bool { + match o { + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => + fixture_has_class(rows, wanted) && count(fixture_blocking_rows(rows)) > 0, + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false, + FixtureInstrumentRefused { cause: c } => false + } +} + +fn is_instrument_refused(o: MultiModuleCompileFixtureOutcome) -> Bool { + match o { + FixtureInstrumentRefused { cause: c } => count(c as String) > 0, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false, + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false + } +} + +fn module_count_is(o: MultiModuleCompileFixtureOutcome, expected: Int) -> Bool { + match o { + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => n == expected, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => n == expected, + FixtureInstrumentRefused { cause: c } => false + } +} + +fn source_digest_of(o: MultiModuleCompileFixtureOutcome) -> String { + match o { + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => sd as String, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => sd as String, + FixtureInstrumentRefused { cause: c } => "" + } +} + +fn compiler_digest_of(o: MultiModuleCompileFixtureOutcome) -> String { + match o { + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => cd as String, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => cd as String, + FixtureInstrumentRefused { cause: c } => "" + } +} + +// --------------------------------------------------------------------------- +// CONTROL 6, FIRST. Without it every control below can pass vacuously. +// +// Three manifests the instrument cannot form a subject from -- an entry naming no supplied +// source, an empty manifest, and one path carrying two different sets of bytes -- each land in +// FixtureInstrumentRefused with a cause. That variant carries no diagnostic list at all, so +// "could not run" is not merely distinguishable from "ran and found nothing": the second has no +// spelling on this arm. The empty manifest is refused rather than compiled BECAUSE an empty +// subject compiles clean vacuously, which is could-not-measure wearing the subject's verdict. +test fn unreached_compile_cannot_render_as_a_clean_one() -> Bool { + is_instrument_refused(entry_names_no_supplied_source_run()) + && is_instrument_refused(empty_manifest_run()) + && is_instrument_refused(duplicate_path_run()) + && !completed_with_no_diagnostics(entry_names_no_supplied_source_run()) + && !completed_with_no_diagnostics(empty_manifest_run()) +} + +// CONTROL 1. A valid two-module program compiles: no diagnostics of ANY severity, and emitted +// files exist. The zero-of-any-severity form is deliberate -- a blocking-only assertion would go +// green if a landed wall were demoted to advisory. +test fn valid_two_module_program_compiles() -> Bool { + completed_with_no_diagnostics(two_module_run(peer_source, entry_source)) +} + +// CONTROL 2. A deliberately invalid CROSS-MODULE program refuses with the INTENDED diagnostic -- +// the entry imports a symbol its peer does not export, and the compile answers MissingExport. +// Naming the class is what makes this a control rather than a change detector: a probe asserting +// only "something refused" passes on a typo in the fixture source itself. +test fn invalid_cross_module_program_refuses_with_the_intended_diagnostic() -> Bool { + refused_with_class(two_module_run(peer_source, entry_missing_export), "MissingExport") +} + +// CONTROL 3. The module count the instrument reports comes from the RESOLVE stage, not from the +// length of the supplied list, so this is a join between two producers. Both directions are +// asserted: two supplied modules report two, three report three. One row alone would be +// satisfied by a constant. +test fn discovered_module_count_equals_the_supplied_manifest() -> Bool { + module_count_is(two_module_run(peer_source, entry_source), 2) + && module_count_is(three_module_run(), 3) + && !module_count_is(three_module_run(), 2) +} + +// CONTROL 4. No default corpus roots are loaded. The entry imports std.types -- a real corpus +// module, present in every ordinary compile of this repository -- and does not supply it. If any +// module index were consulted the import would bind; it refuses UnresolvedImport instead. +test fn no_default_corpus_roots_are_loaded() -> Bool { + refused_with_class( + two_module_run(peer_source, entry_imports_unsupplied_corpus_module), + "UnresolvedImport" + ) +} + +// CONTROL 5. The other side of control 4: reusing a corpus module SPELLING inside the fixture +// binds the FIXTURE's declaration. The supplied module is spelled std.logic and exports +// mmfx_only_sentinel, which the real std.logic does not have, so this compile can only succeed +// against the authored bytes. +test fn corpus_module_spelling_does_not_bind_the_corpus_declaration() -> Bool { + completed_with_no_diagnostics(two_module_run(corpus_spelled_peer, entry_on_corpus_spelling)) +} + +// CONTROL 7. Both digests travel with every arm that measured something, and the source digest +// DISCRIMINATES: the same manifest twice digests identically, and a one-token edit to a single +// module digests differently. Asserting only that a digest is present would pass over a constant. +// The compiler digest is asserted equal across the two runs and non-empty -- one running binary, +// one identity -- which is what lets a receipt quoting this instrument name the transform that +// produced it. +test fn the_fixtures_source_and_compiler_digests_travel_with_the_result() -> Bool { + let a = two_module_run(peer_source, entry_source) + let b = two_module_run(peer_source, entry_source) + let c = two_module_run(peer_source, entry_source_perturbed) + count(source_digest_of(a)) > 0 + && source_digest_of(a) == source_digest_of(b) + && source_digest_of(a) != source_digest_of(c) + && count(compiler_digest_of(a)) > 0 + && compiler_digest_of(a) == compiler_digest_of(c) +} diff --git a/dag/tools/multi_module_compile_fixture.dag b/dag/tools/multi_module_compile_fixture.dag new file mode 100644 index 00000000000..1805ca86a1e --- /dev/null +++ b/dag/tools/multi_module_compile_fixture.dag @@ -0,0 +1,84 @@ +module tools.multi_module_compile_fixture + +import std.types { String, NonEmptyStr, Bool, Int, List } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensusRow } + +// THE ISOLATED MULTI-MODULE COMPILE FIXTURE. A caller authors a MANIFEST of `.dag` modules and +// an entry among them; the instrument compiles exactly those bytes through the v1 pipeline with +// no module index, no corpus roots, and no filesystem read, and returns what the compile decided. +// +// WHY IT EXISTS BESIDE THE SINGLE-MODULE CENSUS RATHER THAN INSIDE IT. `compile_dag_diagnostic_census` +// resolves its one synthetic module's imports against the live checkout, so the corpus is always +// in the pool and a SECOND module can never be authored. That makes every question whose subject +// is the relationship between two modules unaskable on it: a cross-module name collision, an +// import that must not bind, a spelling held by both a fixture declaration and a corpus one. +// Three consumers hit that wall independently before this instrument existed -- invalid fixtures +// relocated out of the corpus for want of it, an ambiguity arm measured and deleted for want of +// it, and DESIGN naming the missing multi-module compile fixture as the next-rung trigger for the +// acyclicity class, whose own receipt records that the single-module harness returns ParseError +// for the ACYCLIC control as well as the cyclic one and so could never reach the wall. +// +// IT IS AN INSTRUMENT AND NOT A GATE. Its outcome reports what the compile decided; nothing here +// judges acceptance, and no workflow invokes it. Callers judge. + +data multi_module_compile_fixture_isolation_note: String = "CORPUS ISOLATION IS BY CONSTRUCTION, NOT BY A FLAG, and that is the property the whole instrument rests on. The supplied manifest IS the source vector handed to the pipeline: there is no code path in the host realization that consults a module index, so a fixture module may reuse a corpus module's SPELLING and bind its own declaration. THE OPEN QUESTION THIS ANSWERS, recorded because upstream did not know the answer and asked for it either way: under whole-corpus floor preparation the required floor folds every witness through ONE prepared subject, so a name collision between a witness and the corpus is unconditional there. That preparation is a fact about how WITNESSES are compiled, not about this nested compile - the prepared authority is consulted by unrelated censuses and never by compile_to_resolved - so a fixture compiled through this instrument is isolated even when the caller itself was prepared whole-corpus. Control 5 of the witness measures exactly that rather than assuming it." + +data multi_module_compile_fixture_phase_standing_note: String = "PHASE-GRAINED STANDING IS THE POINT OF THE COPRODUCT. FixtureInstrumentRefused is the HARNESS's fault - a ragged manifest, a duplicate path, an entry naming no supplied module, a panic. FixtureCompileRefused is the SUBJECT's fault and carries the compiler's own judgment. FixtureCompileCompleted is the subject passing. Collapsing the first two hands a broken harness the compiler's message, which is the not-applicable-versus-malformed conflation DESIGN records as a recurring failure mode, applied to the instrument itself: one reason symbol over 'the input is wrong' and 'this instrument had nothing to say about it', which have opposite owners and opposite repairs. EXECUTION PROVENANCE IS STRUCTURAL AND NOT A FIELD ANYONE MUST REMEMBER TO READ: FixtureCompileCompleted is constructed at exactly one place in the host, after the emit returned and after the blocking population was counted, so an unreached or killed compile HAS NO SPELLING in which it renders as zero diagnostics. That is the positive-artifact rule moved into the type rather than asserted about it." + +data multi_module_compile_fixture_digest_note: String = "THE TWO DIGESTS TRAVEL WITH THE RESULT so a receipt quoting this instrument names the subject it measured and the compiler that measured it. source_digest is a structural fnv1a64 over the entry spelling and every (path, content) pair in the order supplied - a reordering is a different subject and a whitespace edit is a different subject. compiler_digest is resolved_graph_cache transform_content_digest, the content hash of the running compiler binary, which is already the single authority every identity key in the seed consumes for compiler identity rather than a second executable read. Both are absent from the FixtureInstrumentRefused arm on purpose: that arm reports that no subject was formed, and stamping a digest on it would name a measurement that did not happen." + +data multi_module_compile_fixture_scope_note: String = "SCOPE, stated so a receipt cannot claim coverage it does not have (DESIGN 4b: a class's rung is the MINIMUM across its in-scope paths). This is the v1 pipeline to the RUST render target over an authored multi-module subject. It observes NOTHING about the interpreter's disposition of the same program, nothing about other emission targets, and nothing about corpus-grain prevalence. Unlike the single-module census it does NOT arm with_type_ref_hit_ne_bind_measure: the census arms that bracket to sharpen masked type refs against a corpus pool this instrument does not have, so arming it here would be a knob with no subject. WHAT module_count MEANS: the number of modules the RESOLVE stage produced, read from the resolved graph - not the length of the supplied list. A control comparing it against the manifest is therefore a join between two different producers rather than measure() == measure()." + +type FixtureSource { + path: NonEmptyStr + content: String +} + +type MultiModuleCompileFixture { + sources: List + entry: NonEmptyStr +} + +type MultiModuleCompileFixtureOutcome + = FixtureInstrumentRefused { cause: NonEmptyStr } + | FixtureCompileRefused { + module_count: Int + diagnostics: List + source_digest: NonEmptyStr + compiler_digest: NonEmptyStr + } + | FixtureCompileCompleted { + module_count: Int + emitted_files: List + diagnostics: List + source_digest: NonEmptyStr + compiler_digest: NonEmptyStr + } + +fn fixture_source(path: String, content: String) -> FixtureSource { + FixtureSource { path: path, content: content } +} + +fn compile_fixture(fixture: MultiModuleCompileFixture) -> MultiModuleCompileFixtureOutcome { + compile_dag_multi_module_fixture( + fixture.sources |> map(s => s.path as String), + fixture.sources |> map(s => s.content), + fixture.entry as String + ) +} + +// PURE READS OVER ROWS, never over the outcome -- the same construction gunbc.compile_diagnostic_census +// adopted after an accessor answering [] on the not-runnable arm was found to be the fail-open it +// exists to prevent. The only way to obtain a diagnostic list here is to MATCH the coproduct, so +// reading zero diagnostics out of a refused instrument is structurally unwritable. +fn fixture_blocking_rows(rows: List) -> List { + rows |> filter(r => r.blocking) +} + +fn fixture_rows_of_class(rows: List, wanted: String) -> List { + rows |> filter(r => (r.diagnostic_class as String) == wanted) +} + +fn fixture_has_class(rows: List, wanted: String) -> Bool { + count(fixture_rows_of_class(rows, wanted)) > 0 +} diff --git a/src/v1/04_method.dag b/src/v1/04_method.dag index f38113e6c70..54e5f9f1e32 100644 --- a/src/v1/04_method.dag +++ b/src/v1/04_method.dag @@ -56,6 +56,8 @@ fn builtin_kernel_seed_diagnostics() -> List { data compile_dag_diagnostic_census_row_note: String = "WHY THIS ROW EXISTS, and why it is additive rather than contested (ladder-probe-corpus, operator-amended scope 2026-08-01). Its sibling compile_dag_rust_emit_check compiles a synthetic source and collapses the whole result to a Bool - it counts diagnostics passing compile_clean_diagnostic_is_hard and answers false when that count is nonzero. That discards three facts the guarantee probe corpus must observe: WHICH judgment fired (a probe refusing for any hard reason, a typo included, otherwise reads as the wall firing), whether it BLOCKS (the filter IS the severity predicate, so demoting a landed wall from blocking to advisory turns its RED silently green), and every advisory (so a positive control cannot state zero-diagnostics-of-ANY-severity, the assertion codex review 45357 added after an advisory MethodExistenceUndecided passed unnoticed as a green control). The Stage-0 receipt vocabulary gunbc.guarantee_measurement makes the gap structural rather than stylistic: RefusedTyped and AcceptedCounted both carry a diagnostic class and a count, and neither is inhabitable from a Bool, so without this row that schema is uninhabitable on every v1 path. MEASUREMENT ONLY - the host arm reports what the compile decided and filters nothing; callers filter. Registered as a type variable rather than a kernel record because the result is a COPRODUCT (observed census vs typed not-runnable, the top-as-answer/top-as-ignorance split), following shell_materialize_operation_argv's argv_materialization_result precedent; filesystem_read_result_type's make_kernel_record_type idiom is the right one only for a product. DISSOLUTION, answering the compile_clean_forcecheck objection in place: this registry is itself a flat global map that plan argues is a section-3 fork awaiting the PrimitiveDefinition identity join, and this row inherits that trigger EXACTLY as its sibling does - when the join dissolves the registry, the two migrate together. One additive row is linear cost against that dissolution; the alternative was a schema no v1 probe could inhabit." +data compile_dag_multi_module_fixture_row_note: String = "THE MULTI-MODULE COMPILE FIXTURE, and why it is a row rather than an argument to the census row above. compile_dag_diagnostic_census compiles ONE synthetic module and resolves its imports against build_module_path_index_from_witness_roots, which walks the live checkout - so it cannot express any subject whose content is the RELATIONSHIP BETWEEN TWO MODULES, because the second module cannot be authored and the corpus is always in the pool. This row registers a builtin whose subject is a caller-authored MANIFEST of modules compiled with no module index and no corpus roots at all. Registered as a type variable rather than a kernel record for the same reason its sibling is: the result is a COPRODUCT with three arms whose owners differ - the harness refusing, the subject refusing, and the subject passing. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note PrimitiveDefinition identity-join trigger exactly - do not mint a fresh trigger." + data observe_declared_import_closure_symbol_binding_row_note: String = "CLASS B binding-source observation for declared-import-closure-only compiles (#6985). Production classify_unlisted_import_binding_source already exists in cli_run.rs; this row exposes it through the same builtin-registry pattern as compile_dag_diagnostic_census: coproduct result (observed binding vs not-runnable), registered as type_variable_node(id: declared_import_closure_binding_result) rather than a kernel record. MEASUREMENT ONLY — callers judge ListedImport vs PoolCoincidence vs refusal. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note's PrimitiveDefinition identity-join trigger exactly — one additive row is linear cost against that dissolution; do not mint a fresh trigger." // `emit_map_has` WAS A ROW OF THE REGISTRY BELOW AND HAD NO RUNTIME AT ANY TIER @@ -166,6 +168,7 @@ fn builtin_function_registry() -> Map { let m = map_insert(m, "doc_graph_doc_count", int_type) let m = map_insert(m, "compile_dag_rust_emit_check", bool_type) let m = map_insert(m, "compile_dag_diagnostic_census", type_variable_node(id: "compile_diagnostic_census_result")) + let m = map_insert(m, "compile_dag_multi_module_fixture", type_variable_node(id: "multi_module_compile_fixture_result")) let m = map_insert(m, "observe_declared_import_closure_symbol_binding", type_variable_node(id: "declared_import_closure_binding_result")) let m = map_insert(m, "class_b_import_closure_gate_not_affected_skip", bool_type) let m = map_insert(m, "witness_layer_roots_compile_clean_check", bool_type) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 23b01b18d80..aae9506e9be 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -1914,12 +1914,77 @@ pub fn compile_dag_diagnostic_census(source: &str) -> CompileDiagnosticCensus { ); } }; - // Aggregate on the full key INCLUDING severity: one class can legitimately occur at both - // severities, and folding those together would hide exactly the blocking→advisory demotion - // this surface exists to keep visible. + CompileDiagnosticCensus::Observed(compile_diagnostic_census_rows(&result.diagnostics)) +} + +/// One supplied module of a [`compile_dag_multi_module_fixture`] manifest: the path the compile +/// sees and the exact bytes at it. Both are AUTHORED BY THE FIXTURE — nothing here is read from +/// the checkout, which is the whole reason this instrument can answer a question about name +/// resolution that a corpus-resolved compile cannot. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct MultiModuleFixtureSource { + pub path: String, + pub content: String, +} + +/// Outcome of [`compile_dag_multi_module_fixture`]. THE THREE ARMS HAVE THREE DIFFERENT OWNERS +/// and that is why they are three arms: `InstrumentRefused` is the harness's own fault (a +/// malformed manifest, an entry naming no supplied module, a panic), `CompileRefused` is the +/// SUBJECT's fault and carries the compiler's own judgment, and `CompileCompleted` is the subject +/// passing. Collapsing the first two hands a broken harness the compiler's message — the same +/// not-applicable-versus-malformed conflation DESIGN records as a recurring failure mode, applied +/// to the instrument itself. +/// +/// EXECUTION PROVENANCE IS STRUCTURAL, not a field a caller must remember to read. `Completed` +/// is constructed at exactly one place — after `emit_resolved_for_target` returned and after the +/// blocking population was counted — so an unreached or killed compile has no spelling in which +/// it renders as zero diagnostics. That is the positive-artifact rule moved into the type. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum MultiModuleCompileFixtureOutcome { + InstrumentRefused { + cause: String, + }, + CompileRefused { + module_count: i64, + diagnostics: Vec, + source_digest: String, + compiler_digest: String, + }, + CompileCompleted { + module_count: i64, + emitted_files: Vec, + diagnostics: Vec, + source_digest: String, + compiler_digest: String, + }, +} + +/// Structural digest of the supplied manifest — path and content of every module, in the order +/// the caller supplied them, so a reordering is a different subject and a whitespace edit is a +/// different subject. Same fnv1a64 authority every other identity key in the seed consumes +/// (`v1_rt::atom_identity_hash` / `hash_combine`; `std.content_hash` is the modeled surface). +fn multi_module_fixture_source_digest(sources: &[MultiModuleFixtureSource], entry: &str) -> String { + use crate::v1_rt::{atom_identity_hash, hash_combine}; + let mut h = atom_identity_hash("multi-module-compile-fixture-v1".to_string()); + h = hash_combine(h, atom_identity_hash(entry.to_string())); + for s in sources { + h = hash_combine(h, atom_identity_hash(s.path.clone())); + h = hash_combine(h, atom_identity_hash(s.content.clone())); + } + h +} + +/// Aggregate a compile's diagnostics on the full `(class, name, severity)` key. Severity is part +/// of the key rather than folded away because one class can legitimately occur at both +/// severities, and folding those together would hide exactly the blocking→advisory demotion these +/// surfaces exist to keep visible. ONE fold serves both instruments — the census and the +/// multi-module fixture — so they cannot drift into two diagnostic vocabularies (§3). +fn compile_diagnostic_census_rows( + diagnostics: &im::Vector>, +) -> Vec { let mut order: Vec<(String, String, bool)> = Vec::new(); let mut counts: HashMap<(String, String, bool), i64> = HashMap::new(); - for d in result.diagnostics.iter() { + for d in diagnostics.iter() { let (class, name) = compile_clean_diagnostic_histogram_key(d); let blocking = compile_clean_diagnostic_is_hard(d); let key = (class, name, blocking); @@ -1929,17 +1994,148 @@ pub fn compile_dag_diagnostic_census(source: &str) -> CompileDiagnosticCensus { } *entry += 1; } - CompileDiagnosticCensus::Observed( - order - .into_iter() - .map(|key| CompileDiagnosticCensusRow { - diagnostic_class: key.0.clone(), - subject_name: key.1.clone(), - blocking: key.2, - count: counts.get(&key).copied().unwrap_or(0), + order + .into_iter() + .map(|key| CompileDiagnosticCensusRow { + diagnostic_class: key.0.clone(), + subject_name: key.1.clone(), + blocking: key.2, + count: counts.get(&key).copied().unwrap_or(0), + }) + .collect() +} + +/// Host realization backing the `compile_dag_multi_module_fixture` builtin: compile a +/// CALLER-AUTHORED SET of `.dag` modules through the v1 pipeline to the Rust render target, with +/// NO corpus roots, NO module index, and no filesystem read of any kind. +/// +/// WHY THIS EXISTS BESIDE [`compile_dag_diagnostic_census`] RATHER THAN INSIDE IT. The census +/// takes ONE synthetic module and resolves its imports against +/// [`build_module_path_index_from_witness_roots`], which walks the live checkout. That makes it +/// unable to answer any question whose subject is the RELATIONSHIP BETWEEN TWO MODULES — a +/// cross-module name collision, an import that must not bind, a spelling held by both a local +/// declaration and a corpus one — because the corpus is always in the pool and the second module +/// can never be authored. Three lanes hit that wall independently before this instrument existed: +/// invalid fixtures had to be relocated out of the corpus for want of it, an ambiguity arm was +/// measured and deleted for want of it, and this repository's own DESIGN names the missing +/// multi-module compile fixture as the next-rung trigger for the acyclicity class. +/// +/// CORPUS ISOLATION IS BY CONSTRUCTION, not by a flag. The supplied manifest IS the source vector +/// handed to `compile_to_resolved_with_options`; there is no code path here that consults a module +/// index, so a fixture module may reuse a corpus module's spelling and bind its OWN declaration. +/// That is the property control 5 of the witness pins, and it is what makes the instrument usable +/// for resolution questions at all. +/// +/// SCOPE, stated so a receipt cannot claim coverage it does not have (DESIGN §4b): the v1 pipeline +/// to the Rust render target over an authored multi-module subject. It observes nothing about the +/// interpreter's disposition of the same program, nothing about other emission targets, and +/// nothing about corpus-grain prevalence. Unlike the census it does NOT arm +/// `with_type_ref_hit_ne_bind_measure`: the census arms it to sharpen masked type refs against a +/// corpus pool this instrument does not have, so arming it here would be a knob with no subject. +pub fn compile_dag_multi_module_fixture( + paths: &[String], + contents: &[String], + entry: &str, +) -> MultiModuleCompileFixtureOutcome { + if paths.len() != contents.len() { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: format!( + "compile_dag_multi_module_fixture: manifest is {} paths against {} contents; \ + a source is a (path, content) pair and a ragged manifest names no subject", + paths.len(), + contents.len() + ), + }; + } + if paths.is_empty() { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: "compile_dag_multi_module_fixture: empty manifest — an empty subject compiles \ + clean vacuously, which is could-not-measure wearing the subject's verdict" + .to_string(), + }; + } + let sources: Vec = paths + .iter() + .zip(contents.iter()) + .map(|(p, c)| MultiModuleFixtureSource { + path: p.clone(), + content: c.clone(), + }) + .collect(); + let mut seen: HashSet<&str> = HashSet::new(); + for s in sources.iter() { + if s.path.trim().is_empty() { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: "compile_dag_multi_module_fixture: a supplied source has an empty path" + .to_string(), + }; + } + if !seen.insert(s.path.as_str()) { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: format!( + "compile_dag_multi_module_fixture: path '{}' supplied twice; which bytes are \ + at that path is then undecidable and the digest would name neither", + s.path + ), + }; + } + } + if !sources.iter().any(|s| s.path == entry) { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: format!( + "compile_dag_multi_module_fixture: entry '{entry}' names no supplied source" + ), + }; + } + let source_digest = multi_module_fixture_source_digest(&sources, entry); + let compiler_digest = crate::resolved_graph_cache::transform_content_digest(); + let files: Vec> = sources + .iter() + .map(|s| { + Rc::new(v1_compiler_compile::SourceFile { + path: s.path.clone(), + content: s.content.clone(), }) - .collect(), - ) + }) + .collect(); + let compiled = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + let resolved = v1_compiler_compile::compile_to_resolved(Rc::new(files.into())); + let module_count = match resolved.graph.clone() { + Some(g) => g.modules.len() as i64, + None => 0, + }; + let result = v1_compiler_compile::emit_resolved_for_target( + resolved, + crate::v1_compiler_artifact::RenderTarget::Rust, + ); + (module_count, result) + })); + let (module_count, result) = match compiled { + Ok(r) => r, + Err(_) => { + return MultiModuleCompileFixtureOutcome::InstrumentRefused { + cause: "compile_dag_multi_module_fixture: the compile panicked before producing \ + diagnostics" + .to_string(), + }; + } + }; + let rows = compile_diagnostic_census_rows(&result.diagnostics); + if rows.iter().any(|r| r.blocking) { + return MultiModuleCompileFixtureOutcome::CompileRefused { + module_count, + diagnostics: rows, + source_digest, + compiler_digest, + }; + } + MultiModuleCompileFixtureOutcome::CompileCompleted { + module_count, + emitted_files: result.files.iter().map(|f| f.path.clone()).collect(), + diagnostics: rows, + source_digest, + compiler_digest, + } } /// One symbol's binding observation on a declared-import-closure-only compile. diff --git a/src/v1/stage0/src/v1_compiler_infer_method.rs b/src/v1/stage0/src/v1_compiler_infer_method.rs index 70b29212781..5d7747f9a62 100644 --- a/src/v1/stage0/src/v1_compiler_infer_method.rs +++ b/src/v1/stage0/src/v1_compiler_infer_method.rs @@ -127,6 +127,15 @@ pub fn compile_dag_diagnostic_census_row_note() -> String { CACHED.with(|c: &String| c.clone()) } +pub fn compile_dag_multi_module_fixture_row_note() -> String { + thread_local! { + static CACHED: String = { + "THE MULTI-MODULE COMPILE FIXTURE, and why it is a row rather than an argument to the census row above. compile_dag_diagnostic_census compiles ONE synthetic module and resolves its imports against build_module_path_index_from_witness_roots, which walks the live checkout - so it cannot express any subject whose content is the RELATIONSHIP BETWEEN TWO MODULES, because the second module cannot be authored and the corpus is always in the pool. This row registers a builtin whose subject is a caller-authored MANIFEST of modules compiled with no module index and no corpus roots at all. Registered as a type variable rather than a kernel record for the same reason its sibling is: the result is a COPRODUCT with three arms whose owners differ - the harness refusing, the subject refusing, and the subject passing. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note PrimitiveDefinition identity-join trigger exactly - do not mint a fresh trigger.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn observe_declared_import_closure_symbol_binding_row_note() -> String { thread_local! { static CACHED: String = { @@ -365,6 +374,11 @@ pub fn builtin_function_registry() -> Rc>> { "compile_dag_diagnostic_census".to_string(), type_variable_node("compile_diagnostic_census_result".to_string()), ); + let m = v1_rt::rc_map_insert( + m.clone(), + "compile_dag_multi_module_fixture".to_string(), + type_variable_node("multi_module_compile_fixture_result".to_string()), + ); let m = v1_rt::rc_map_insert( m.clone(), "observe_declared_import_closure_symbol_binding".to_string(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 26390288b3c..de694d0ff62 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -8819,6 +8819,76 @@ fn compile_diagnostic_census_value( } } +/// Projects a host multi-module fixture outcome into the +/// `tools.multi_module_compile_fixture` coproduct. The three arms stay distinct all the way to +/// the substrate: a broken harness must never arrive wearing the compiler's verdict, and a +/// compile that never ran must never arrive as `FixtureCompileCompleted` with an empty diagnostic +/// list (DESIGN §5 — could-not-measure conflated with the subject passing). +fn multi_module_compile_fixture_value( + outcome: crate::cli_run::MultiModuleCompileFixtureOutcome, + ctx: &InterpContext, +) -> Value { + let rows = |rows: Vec| { + list_value( + rows.into_iter() + .map(|r| Value::Record { + type_name: ctx.sym("CompileDiagnosticCensusRow"), + fields: Rc::new(sorted_fields(vec![ + (ctx.sym("diagnostic_class"), str_value(r.diagnostic_class)), + (ctx.sym("subject_name"), str_value(r.subject_name)), + (ctx.sym("blocking"), Value::Bool(r.blocking)), + (ctx.sym("count"), Value::Int(r.count)), + ])), + }) + .collect::>(), + ) + }; + let variant = |name: &str, fields: Vec<(Symbol, Value)>| Value::Variant { + type_name: ctx.sym("MultiModuleCompileFixtureOutcome"), + variant_name: ctx.sym(name), + fields: Rc::new(sorted_fields(fields)), + }; + match outcome { + crate::cli_run::MultiModuleCompileFixtureOutcome::InstrumentRefused { cause } => variant( + "FixtureInstrumentRefused", + vec![(ctx.sym("cause"), str_value(cause))], + ), + crate::cli_run::MultiModuleCompileFixtureOutcome::CompileRefused { + module_count, + diagnostics, + source_digest, + compiler_digest, + } => variant( + "FixtureCompileRefused", + vec![ + (ctx.sym("module_count"), Value::Int(module_count)), + (ctx.sym("diagnostics"), rows(diagnostics)), + (ctx.sym("source_digest"), str_value(source_digest)), + (ctx.sym("compiler_digest"), str_value(compiler_digest)), + ], + ), + crate::cli_run::MultiModuleCompileFixtureOutcome::CompileCompleted { + module_count, + emitted_files, + diagnostics, + source_digest, + compiler_digest, + } => variant( + "FixtureCompileCompleted", + vec![ + (ctx.sym("module_count"), Value::Int(module_count)), + ( + ctx.sym("emitted_files"), + list_value(emitted_files.into_iter().map(str_value).collect::>()), + ), + (ctx.sym("diagnostics"), rows(diagnostics)), + (ctx.sym("source_digest"), str_value(source_digest)), + (ctx.sym("compiler_digest"), str_value(compiler_digest)), + ], + ), + } +} + fn unlisted_import_binding_source_value( source: crate::cli_run::UnlistedImportBindingSource, ctx: &InterpContext, @@ -13852,6 +13922,16 @@ macro_rules! v1_builtin_arms { ))) }, + arm "free_call.compile_dag_multi_module_fixture" { "compile_dag_multi_module_fixture" } => { + let paths = expect_str_list($positional.first().copied(), $name)?; + let contents = expect_str_list($positional.get(1).copied(), $name)?; + let entry = expect_str($positional.get(2).copied(), $name)?; + Ok(Some(multi_module_compile_fixture_value( + crate::cli_run::compile_dag_multi_module_fixture(&paths, &contents, &entry), + $ctx, + ))) + }, + arm "free_call.observe_declared_import_closure_symbol_binding" { "observe_declared_import_closure_symbol_binding" } => { let pool_roots = expect_str_list($positional.first().copied(), $name)?; let entry_path = expect_str($positional.get(1).copied(), $name)?; diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index 28ee9cb01ca..29030b45690 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -93,6 +93,7 @@ pub enum EvalBuiltinArm { FreeCallDocGraphDocCount, FreeCallCompileDagRustEmitCheck, FreeCallCompileDagDiagnosticCensus, + FreeCallCompileDagMultiModuleFixture, FreeCallObserveDeclaredImportClosureSymbolBinding, FreeCallClassBImportClosureGateNotAffectedSkip, FreeCallWitnessLayerRootsCompileCleanCheck, @@ -223,6 +224,7 @@ pub fn lookup_eval_builtin_inner(spelling: &str) -> Option { "doc_graph_doc_count" => Some(EvalBuiltinArm::FreeCallDocGraphDocCount), "compile_dag_rust_emit_check" => Some(EvalBuiltinArm::FreeCallCompileDagRustEmitCheck), "compile_dag_diagnostic_census" => Some(EvalBuiltinArm::FreeCallCompileDagDiagnosticCensus), + "compile_dag_multi_module_fixture" => Some(EvalBuiltinArm::FreeCallCompileDagMultiModuleFixture), "observe_declared_import_closure_symbol_binding" => Some(EvalBuiltinArm::FreeCallObserveDeclaredImportClosureSymbolBinding), "class_b_import_closure_gate_not_affected_skip" => Some(EvalBuiltinArm::FreeCallClassBImportClosureGateNotAffectedSkip), "witness_layer_roots_compile_clean_check" => Some(EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanCheck), @@ -351,6 +353,7 @@ macro_rules! eval_builtin_inner_arm { ("free_call.doc_graph_doc_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallDocGraphDocCount }; ("free_call.compile_dag_rust_emit_check") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallCompileDagRustEmitCheck }; ("free_call.compile_dag_diagnostic_census") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallCompileDagDiagnosticCensus }; + ("free_call.compile_dag_multi_module_fixture") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallCompileDagMultiModuleFixture }; ("free_call.observe_declared_import_closure_symbol_binding") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallObserveDeclaredImportClosureSymbolBinding }; ("free_call.class_b_import_closure_gate_not_affected_skip") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallClassBImportClosureGateNotAffectedSkip }; ("free_call.witness_layer_roots_compile_clean_check") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanCheck }; diff --git a/src/v2/test/claim/local_binding_shadow_compile_test.dag b/src/v2/test/claim/local_binding_shadow_compile_test.dag new file mode 100644 index 00000000000..8941ddf46ca --- /dev/null +++ b/src/v2/test/claim/local_binding_shadow_compile_test.dag @@ -0,0 +1,92 @@ +module v2.test.claim.local_binding_shadow_compile + +import std.types { String, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensusRow } +import tools.multi_module_compile_fixture { + MultiModuleCompileFixture, + MultiModuleCompileFixtureOutcome, + FixtureInstrumentRefused, + FixtureCompileRefused, + FixtureCompileCompleted, + FixtureSource, + fixture_source, + compile_fixture, + fixture_has_class +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE COMPILE HALF OF THE LOCAL-BINDING-SHADOW LAW. Its sibling +// v2.test.claim.local_binding_shadow measures DISPATCH by execution: which function a call site +// actually reaches. This file measures SHAPE: what the compiler's call-shape judgment believes it +// is looking at. The two are one question and were answered differently by the same binding, which +// is the whole reason this file is separate rather than three more arms over there. +// +// ONE BINDING STANDING, AND WHAT IT MEANS HERE. A named-argument call through a function VALUE is +// a blocking refusal by operator ruling -- direct declaration calls keep named arguments, +// function-value calls stay positional-only -- so `CallNamedArgOnFunctionValue` firing is the +// SHAPE tier stating, in the compiler's own vocabulary, that the spelling names a local binding +// and not the module declaration. The discriminating control is the same labeled call with NO +// local binding, which compiles CLEAN because it is a declaration call. So the refusal is a +// property of the BINDING, never of the label. +// +// WHY IT IS AN ISOLATED MULTI-MODULE FIXTURE AND NOT AN IN-CORPUS PAIR. The subject is a name held +// by two modules at once, and the corpus is not a controlled setting for that: under whole-corpus +// floor preparation every witness is folded through one prepared subject, so a third module could +// supply the spelling and neither the red nor the green would be attributable. Every byte compiled +// here is authored below, and nothing outside this file can rename, delete or supply +// `shadow_sentinel` in that compile -- which is also how the "unrelated global renamed or removed" +// arm is answered: by construction, not by sampling one rename. + +data shadow_peer_source: String = "module shadowx.peer\nfn shadow_sentinel(n: Int) -> Int { 900 }\n" + +data entry_local_positional: String = "module shadowx.entry\nimport shadowx.peer { shadow_sentinel }\nfn local_sentinel(n: Int) -> Int { n + 1 }\nfn f() -> Int { let shadow_sentinel = local_sentinel\n shadow_sentinel(1) }\n" + +data entry_local_labeled: String = "module shadowx.entry\nimport shadowx.peer { shadow_sentinel }\nfn local_sentinel(n: Int) -> Int { n + 1 }\nfn f() -> Int { let shadow_sentinel = local_sentinel\n shadow_sentinel(n: 1) }\n" + +data entry_declaration_labeled: String = "module shadowx.entry\nimport shadowx.peer { shadow_sentinel }\nfn f() -> Int { shadow_sentinel(n: 1) }\n" + +fn shadow_compile(entry: String) -> MultiModuleCompileFixtureOutcome { + compile_fixture(MultiModuleCompileFixture { + sources: [ + fixture_source("shadowx/peer.dag", shadow_peer_source), + fixture_source("shadowx/entry.dag", entry) + ], + entry: "shadowx/entry.dag" + }) +} + +fn compiles_clean(o: MultiModuleCompileFixtureOutcome) -> Bool { + match o { + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => count(rows) == 0, + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false, + FixtureInstrumentRefused { cause: c } => false + } +} + +fn refuses_with_class(o: MultiModuleCompileFixtureOutcome, wanted: String) -> Bool { + match o { + FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => fixture_has_class(rows, wanted), + FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false, + FixtureInstrumentRefused { cause: c } => false + } +} + +// THE SHAPE TIER SEES THE LOCAL BINDING. A labeled call through a local that shadows a peer's free +// function refuses CallNamedArgOnFunctionValue -- the compiler naming the callee a function value, +// which only the LOCAL is. The second conjunct is the discriminator and carries the whole claim: +// the identical labeled call with no local binding compiles CLEAN, because it is then a +// declaration call and declaration calls keep their labels. Without it the first conjunct would be +// satisfied by a compiler that refused every labeled call. +test fn the_shape_tier_reads_the_shadowing_local_as_a_function_value() -> Bool { + refuses_with_class(shadow_compile(entry_local_labeled), "CallNamedArgOnFunctionValue") + && compiles_clean(shadow_compile(entry_declaration_labeled)) +} + +// AND THE POSITIONAL FORM IS ADMITTED, which is the precondition for the dispatch half to be +// measurable at all: the sibling witness asserts that this exact program evaluates to the LOCAL's +// answer, and an assertion about a program the compiler refuses would be no verdict. +test fn the_positional_form_of_the_shadowed_call_compiles_clean() -> Bool { + compiles_clean(shadow_compile(entry_local_positional)) +} diff --git a/src/v2/test/claim/local_binding_shadow_peer.dag b/src/v2/test/claim/local_binding_shadow_peer.dag index 69597d63da1..07ff1921221 100644 --- a/src/v2/test/claim/local_binding_shadow_peer.dag +++ b/src/v2/test/claim/local_binding_shadow_peer.dag @@ -17,3 +17,20 @@ import v2.std.logic { Bool } fn shadow_pred(n: Int) -> Bool { true } + +// THE SENTINEL PAIR, and it is a SEPARATE symbol from shadow_pred above rather than a rewrite of +// it. A Bool has two inhabitants, so a Bool-valued displacement can only ever say WHICH of two +// answers came back; an Int sentinel says WHICH FUNCTION ANSWERED. This one returns 900 for every +// input and ignores its argument, so it is total, same-arity, and same param-and-result types as +// the local that displaces it -- every axis held equal except the value returned. A witness +// asserting 2 and receiving 900 has located the producer, not merely disagreed with it. +fn shadow_sentinel(n: Int) -> Int { + 900 +} + +// NOT SHADOWED BY ANYTHING, and named so nothing is tempted to. It exists for the arm that asserts +// the module free function is still reachable when NO local binding competes for its spelling -- +// the direction a repair that simply stopped consulting the free-function table would break. +fn unshadowed_sentinel(n: Int) -> Int { + 700 +} diff --git a/src/v2/test/claim/local_binding_shadow_test.dag b/src/v2/test/claim/local_binding_shadow_test.dag index d6e5f158a4f..a2e53ac88ba 100644 --- a/src/v2/test/claim/local_binding_shadow_test.dag +++ b/src/v2/test/claim/local_binding_shadow_test.dag @@ -1,6 +1,6 @@ module v2.test.claim.local_binding_shadow -import v2.test.claim.local_binding_shadow_peer { shadow_pred } +import v2.test.claim.local_binding_shadow_peer { shadow_pred, shadow_sentinel, unshadowed_sentinel } import v2.std.integer { Int } import v2.std.logic { Bool } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -154,3 +154,128 @@ test fn named_binding_applied_under_another_name_is_unaffected_control() -> Bool test fn uncollided_named_binding_is_unaffected_control() -> Bool { !let_uncollided_named() } + +// =========================================================================================== +// THE PERMANENT ARMS. Everything above measures the defect on a Bool, which was enough to +// establish the law and is NOT enough to keep it. A Bool has two inhabitants, so a displaced call +// and a correct call can agree by coincidence; these arms hold every axis equal except the VALUE +// RETURNED, so a regression names the producer instead of merely disagreeing with it. +// +// EVERY AXIS THE DISPATCH NAMED IS HELD EQUAL between the local and the module function it +// collides with: same arity, same parameter type, same result type, both total. The only +// difference is the sentinel, and the local's sentinel is REQUIRED -- an arm asserting 2 cannot +// be satisfied by the free function, which answers 900 for every input including this one. +// +// THE SHADOWING SYMBOL IS FIXTURE-OWNED, which is how the "unrelated global renamed or removed" +// arm is answered here. That arm exists to catch a repair that works by accident of what else is +// in scope; the construction that forecloses it is that nothing outside this fixture's own two +// files can supply, rename or delete `shadow_sentinel`, so there is no unrelated global whose +// motion could change these results. That is stronger than an A/B over one rename, which only +// samples the globals someone thought to move. + +fn local_sentinel(n: Int) -> Int { + n + 1 +} + +fn sentinel_carrier_named() -> SentinelCarrier { + SentinelCarrier { shadow_sentinel: local_sentinel } +} + +type SentinelCarrier { + shadow_sentinel: fn(Int) -> Int +} + +fn let_sentinel_positional() -> Int { + let shadow_sentinel = local_sentinel + shadow_sentinel(1) +} + +fn param_sentinel(shadow_sentinel: fn(Int) -> Int) -> Int { + shadow_sentinel(1) +} + +fn pattern_sentinel() -> Int { + match sentinel_carrier_named() { + SentinelCarrier { shadow_sentinel: shadow_sentinel } => shadow_sentinel(1) + } +} + +fn no_local_binding_reaches_the_module_function() -> Int { + unshadowed_sentinel(1) +} + +fn no_local_binding_reaches_the_shadowed_module_function() -> Int { + shadow_sentinel(1) +} + +// PERMANENT ARM 1 -- the local callable wins at every binding form. POSITIONAL ONLY, and that is +// a ruled property of the language rather than a gap in this fixture: a named-argument call +// through a function VALUE is a blocking refusal (CallNamedArgOnFunctionValue), operator-required, +// with direct declaration calls keeping named arguments and function-value calls staying +// positional-only. The named spelling is therefore measured where it lives -- at COMPILE, in +// test.claim.local_binding_shadow_compile_witness, which pins that the SHAPE tier and this +// DISPATCH tier consume ONE binding standing: shape sees a function value and refuses the label, +// dispatch sees the same function value and calls the local. Before the repair those two tiers +// disagreed about the same binding, which is what let a labeled call be silently accepted by the +// free function while the shape check was already calling it a function value. +test fn local_callable_wins_over_the_same_named_module_function() -> Bool { + let_sentinel_positional() == 2 + && param_sentinel(shadow_sentinel: local_sentinel) == 2 + && pattern_sentinel() == 2 +} + +// PERMANENT ARM 2 -- the opposite direction, and the one a repair that simply stopped consulting +// the free-function table would break. With NO local binding competing for the spelling, the +// module function is still what the call reaches: 700 from a name nothing shadows, and 900 from +// the very name the arm above displaces. The second conjunct is the load-bearing one -- it proves +// the free-function tier was narrowed rather than removed. +test fn a_module_function_is_still_callable_with_no_local_binding() -> Bool { + no_local_binding_reaches_the_module_function() == 700 + && no_local_binding_reaches_the_shadowed_module_function() == 900 +} + +// PERMANENT ARM 3 -- the sentinel is REQUIRED, not merely observed. Stated as its own row because +// the two arms above would both pass against an interpreter that answered 2 and 900 for reasons +// unrelated to which function ran: this one asserts the free function's answer is ABSENT from the +// shadowed positions and the local's answer is ABSENT from the unshadowed one, so each result is +// evidence about a producer rather than a coincidence of arithmetic. +test fn each_sentinel_is_absent_from_the_other_positions() -> Bool { + let_sentinel_positional() != 900 + && pattern_sentinel() != 900 + && no_local_binding_reaches_the_shadowed_module_function() != 2 +} + +// =========================================================================================== +// THE STILL-OPEN HALF, ENROLLED AS AN EXPECTED RED RATHER THAN LEFT IN PROSE. The repair above +// closed the case where the local binding holds something CALLABLE. Where the local holds a +// NON-CALLABLE value the call still falls through to the module free function and returns its +// answer: `let shadow_sentinel = 5` followed by `shadow_sentinel(1)` evaluates to 900, measured by +// execution. That is the identical below-floor class -- a plausible wrong value, no diagnostic -- +// with the callable half repaired and this half untouched. +// +// AND ITS COMPILE-SIDE TWIN IS ALREADY GREEN, which is what makes this worth a row rather than a +// note. v2.test.claim.local_binding_shadow_compile measures that a labeled call through this exact +// binding refuses CallNamedArgOnFunctionValue -- the SHAPE tier names the callee a function value +// even when the bound value is an Int -- while DISPATCH walks past the binding to the peer. Two +// tiers, one binding, opposite answers. The repair made them agree for callable bindings; they +// still disagree here. +// +// WHY IT IS NOT REPAIRED IN THE SAME CHANGE, stated as a scope decision rather than a discovery +// order. Refusing on ANY lexical binding rather than a callable one widens the gate over every +// spelling in the corpus that shadows a builtin with a non-callable value, and that population is +// not measured. A widening whose blast radius is unmeasured is exactly the shape that swallows its +// own controls, so it is filed here -- one row, one class, an OBSERVED semantic red that returns a +// Bool and never throws -- and repaired against a measured population. +// +// NEXT-RUNG TRIGGER: a census of lexical bindings whose spelling collides with a builtin or +// module free function and whose bound value is not callable. The row retires when that population +// is enumerated and the gate is widened to refuse over it. + +fn noncallable_local_shadow() -> Int { + let shadow_sentinel = 5 + shadow_sentinel(1) +} + +test fn a_noncallable_local_binding_does_not_fall_through_to_the_module_function() -> Bool { + noncallable_local_shadow() != 900 +} diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index bbc15f8e299..91f59210920 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -363,7 +363,7 @@ fn floor_expected_red_chunk_02() -> List { } fn floor_expected_red_chunk_03() -> List { - Cons { head: "test.claim.host_effect_apply_witness.witness_ssh_shell_unreachable_fails_closed", tail: Cons { head: "test.claim.host_phase_status.witness_reconcile_covers_upsert_teardown_and_noop", tail: Cons { head: "test.claim.host_phase_status.witness_remaining_work_counts_every_unfinished_cell", tail: Cons { head: "test.claim.interpreter_replacement_cut_witness_test.interpreter_cut_plan_refuses_with_open_decisions", tail: Cons { head: "test.claim.interpreter_replacement_cut_witness_test.retiring_with_x_needs_no_coverage_authority", tail: Empty {} } } } } } + Cons { head: "test.claim.host_effect_apply_witness.witness_ssh_shell_unreachable_fails_closed", tail: Empty {} } } fn floor_expected_red_chunk_04() -> List { @@ -375,7 +375,7 @@ fn floor_expected_red_chunk_05() -> List { } fn floor_expected_red_chunk_06() -> List { - Cons { head: "test.claim.source_integration_proof_kernel_acceptance.witness_p1_proof_kernel_acceptance_contract_holds", tail: Cons { head: "test.claim.srv3_subsumption.comment_only_drift_is_one_change_not_remove_add", tail: Cons { head: "test.claim.srv3_subsumption.reconcile_would_teardown_only_if_ownership_claimed_it", tail: Cons { head: "test.claim.srv3_subsumption.srv3_and_srv4_disagree_on_convergence", tail: Cons { head: "test.claim.srv3_subsumption.srv3_reconcile_adds_exactly_the_missing_fleet_key", tail: Cons { head: "test.claim.srv3_subsumption.srv3_reconcile_refuses_both_unowned_keys_never_teardown", tail: Cons { head: "test.claim.srv3_subsumption.srv4_reconcile_is_converged_empty_plan", tail: Empty {} } } } } } } } + Cons { head: "test.claim.source_integration_proof_kernel_acceptance.witness_p1_proof_kernel_acceptance_contract_holds", tail: Empty {} } } // SEVENTEEN generated_conformance_floor ROWS LEFT THIS ROSTER BECAUSE THE FIX THIS BRANCH CARRIES @@ -429,7 +429,7 @@ fn floor_expected_red_chunk_07() -> List { } fn floor_expected_red_chunk_08() -> List { - Cons { head: "v2.test.claim.staging.cached_stage_hit_skips_stage", tail: Cons { head: "v2.test.claim.staging.cached_stage_miss_runs_stage", tail: Cons { head: "v2.test.emit.produced_decl_support_preserved.produced_decl_support_survives_augmentation", tail: Cons { head: "v2.test.execution.dag_add_emit_round_trip.dag_add_domain_coerce_accepts_holds", tail: Cons { head: "v2.test.execution.dag_add_emit_round_trip.dag_add_domain_translate_accepts_holds", tail: Empty {} } } } } } + Cons { head: "v2.test.execution.dag_add_emit_round_trip.dag_add_domain_coerce_accepts_holds", tail: Cons { head: "v2.test.execution.dag_add_emit_round_trip.dag_add_domain_translate_accepts_holds", tail: Empty {} } } } fn floor_expected_red_chunk_09() -> List { @@ -539,8 +539,20 @@ fn floor_expected_red_chunk_20() -> List { // // The partition of the 164 and the measurements behind this family are // docs/plans/receipts/floor-runtime-error-partition-2026-08-23/. +// ONE IDENTITY ENROLLED 2026-08-26 with a per-row reason, because a row without one is how a +// thrown claim gets filed as a semantic red. THE CLASS: a lexical binding holding a NON-CALLABLE +// value, called at its own spelling, still falls through to the module free function sharing that +// spelling and returns ITS answer -- a plausible wrong value with no diagnostic. It is the +// unrepaired half of the local-binding-shadow class whose callable half landed the same day; the +// witness's own annotation carries the two-tier disagreement that makes it legible (the compile +// sibling already refuses a labeled call through this exact binding, naming the callee a function +// value, while dispatch walks past it). THE ROW ASSERTS THE DESIRED LAW, so it reds now and greens +// on repair, and its single conjunct returns a Bool and never throws -- an OBSERVED semantic red, +// never no-verdict debt. NEXT-RUNG TRIGGER: the census of non-callable lexical bindings whose +// spelling collides with a builtin or module free function; the gate is widened against a measured +// population, never speculatively. fn floor_expected_red_chunk_21() -> List { - Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_extra_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_missing_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_wrong_argument_type_must_refuse_at_compile", tail: Cons { head: "test.claim.fabric_cell_evidence_algebra_witness.evidence_full_value_is_order_independent", tail: Empty {} } } } } + Cons { head: "v2.test.claim.local_binding_shadow.a_noncallable_local_binding_does_not_fall_through_to_the_module_function", tail:Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_extra_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_missing_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_wrong_argument_type_must_refuse_at_compile", tail: Cons { head: "test.claim.fabric_cell_evidence_algebra_witness.evidence_full_value_is_order_independent", tail: Empty {} } } } } } } // CHUNK 22 IS DELETED, AND THIS IS ITS DISSOLUTION RECEIPT RATHER THAN A GAP. @@ -562,6 +574,22 @@ fn floor_expected_red_chunk_21() -> List { // carried (the lambda column, the call-site rename, and the uncollided binding). Deleting the // probe on repair would recreate specification-without-execution one rung up. +// THIRTEEN FURTHER IDENTITIES RETIRED 2026-08-26 BY ONE REPAIR, and the number is the finding +// rather than the bookkeeping. The local-binding-shadow repair -- a call site spelling a name held +// by both a local binding and a module-level free function now reaches the LOCAL -- was enrolled +// with ONE row of its own. On the first required run after it landed, thirteen OTHER enrolled reds +// across five unrelated modules passed: test.claim.host_phase_status (2), +// test.claim.interpreter_replacement_cut_witness_test (2), test.claim.srv3_subsumption (6), +// v2.test.claim.staging (2) and v2.test.emit.produced_decl_support_preserved (1). None of them was +// authored as a shadow probe and none names the class; they were filed as ordinary reds against +// their own subjects, which is exactly what a SILENT wrong value looks like from the consumer's +// side -- the fold returns a plausible answer, the assertion disagrees with it, and the row gets +// written against the assertion. So this list was carrying thirteen symptoms of one cause, and the +// cause was legible from none of them. +// +// THE ROWS ARE REMOVED AND THE WITNESSES ARE NOT (DESIGN 4b(4)). Every one of those claims stays +// enrolled and now passes, which is what keeps the repair's reach measured rather than asserted: +// if the gate regresses, thirteen independent modules go red before the shadow fixture does. fn floor_expected_red_chunks() -> List> { Cons { head: floor_expected_red_chunk_00(), tail: Cons { head: floor_expected_red_chunk_01(), tail: Cons { head: floor_expected_red_chunk_02(), tail: Cons { head: floor_expected_red_chunk_03(), tail: Cons { head: floor_expected_red_chunk_04(), tail: Cons { head: floor_expected_red_chunk_05(), tail: Cons { head: floor_expected_red_chunk_06(), tail: Cons { head: floor_expected_red_chunk_07(), tail: Cons { head: floor_expected_red_chunk_08(), tail: Cons { head: floor_expected_red_chunk_09(), tail: Cons { head: floor_expected_red_chunk_10(), tail: Cons { head: floor_expected_red_chunk_11(), tail: Cons { head: floor_expected_red_chunk_12(), tail: Cons { head: floor_expected_red_chunk_13(), tail: Cons { head: floor_expected_red_chunk_14(), tail: Cons { head: floor_expected_red_chunk_15(), tail: Cons { head: floor_expected_red_chunk_16(), tail: Cons { head: floor_expected_red_chunk_17(), tail: Cons { head: floor_expected_red_chunk_18(), tail: Cons { head: floor_expected_red_chunk_19(), tail: Cons { head: floor_expected_red_chunk_20(), tail: Cons { head: floor_expected_red_chunk_21(), tail: Empty {}}}}}}}}}}}}}}}}}}}}}}} } From 2bbff5270ae23fbba1b96d82b5de1a8c5e0a28ff Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 04:56:44 +0000 Subject: [PATCH 3/3] Complete the same motion in the paired roster: the non-verdict population is repaid to zero The expected-red removals in this PR orphaned eleven rows in v2.workflow.floor_non_verdict, and the required floor refused with NonVerdictRowUnreachable count=11 -- rows that read as debt while being structurally incapable of being debt, which is exactly the decoration that wall exists to refuse. They are DELETED, not re-enrolled: re-enrolling would restore a falsehood to silence a wall. THE CASCADE WAS LARGER THAN THE REFUSAL NAMED, because gunbc.floor_non_verdict_classification joins that roster EXACTLY in both directions. Emptying the roster required repaying its two live arms, and the result is the join that carrier declared it could not make: closure_dependent_rows held nine ClosureDependentResolution rows whose attribution to the local-binding-shadow defect was explicitly INFERENCE, with no colliding name identified for six srv3 rows or two staging rows. Its unjoined_inference_note named its own instrument -- fix the resolver and re-run; recovery measures the join, non-recovery isolates a second cause. All nine recovered. There is no second cause. unmeasured_rows held the two host_phase_status identities, classified StandingUnmeasured on an honest obstacle (no narrow closure can resolve them, so no A/B arm existed). Both recovered too. That is recorded as the weaker true statement -- a repair aimed elsewhere recovered them -- and NOT as a retroactive reclassification. Both arms stay DECLARED with repayment receipts, following the idiom the file already established for closure_independent_rows: the causes remain constructible, and an emptied arm with its reason recorded is a different fact from an arm that never existed. The inhabitance witness row is deleted with the population it described. It asserted the partition was non-empty, which was right while a debt existed and becomes an assertion that the debt must CONTINUE to exist once repaid -- it would make the carrier unable to reach the empty terminal state its own header declares. The join, uniqueness, evidence-present and exact-partition rows are untouched and still gate. An empty roster is the STRICTEST state here, not the most permissive: cli_run's polarity comment records that a non-enrolled identity BLOCKS, so losing the roster can only red a run, never flatter one. Co-Authored-By: Claude Opus 5 --- .../floor_non_verdict_classification.dag | 76 ++----------------- ...on_verdict_classification_witness_test.dag | 30 ++++++-- src/v2/workflow/floor_non_verdict.dag | 66 ++++++++-------- 3 files changed, 59 insertions(+), 113 deletions(-) diff --git a/dag/gunbc/floor_non_verdict_classification.dag b/dag/gunbc/floor_non_verdict_classification.dag index ec362392e1e..6e11b1eaada 100644 --- a/dag/gunbc/floor_non_verdict_classification.dag +++ b/dag/gunbc/floor_non_verdict_classification.dag @@ -75,81 +75,17 @@ data gating_answer_note: String = "DOES known_red_runtime_errored GATE, AND SHOU data closure_dependent_evidence: String = "PASSES under a narrow claim_batch --hermetic closure; produces no verdict on the floor's whole-corpus subject" -data closure_dependent_rows: List = [ - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "comment_only_drift_is_one_change_not_remove_add"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "reconcile_would_teardown_only_if_ownership_claimed_it"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_and_srv4_disagree_on_convergence"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_reconcile_adds_exactly_the_missing_fleet_key"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_reconcile_refuses_both_unowned_keys_never_teardown"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv4_reconcile_is_converged_empty_plan"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "v2.test.claim.staging", function: "cached_stage_hit_skips_stage"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: "PASSES narrow; on the floor throws `cannot access field 'raw' on Int` -- an error text shared with nothing else in the population and a cause shared with the eight rows above it" - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "v2.test.claim.staging", function: "cached_stage_miss_runs_stage"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: closure_dependent_evidence - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "v2.test.emit.produced_decl_support_preserved", function: "produced_decl_support_survives_augmentation"), - cause: ClosureDependentResolution, - standing: AssertsARedThatDoesNotExist, - measured_evidence: "PASSES narrow; on the floor throws `call contract mismatch calling 'render': missing required argument 'proto'`. Its `render` is PATTERN-BOUND out of ProducedDeclWired and std.layout declares a free `fn render(doc, proto)`, so this row is the shadowing class in its loud, different-arity face" - } -] +data closure_dependent_repaid_note: String = "EMPTY, AND THAT IS A REPAYMENT RECEIPT AND A MEASURED JOIN RATHER THAN A MISSING MEASUREMENT. This list held NINE ClosureDependentResolution / AssertsARedThatDoesNotExist rows -- six test.claim.srv3_subsumption, two v2.test.claim.staging, and v2.test.emit.produced_decl_support_preserved. All nine now ANSWER and PASS on the required floor, so they left this carrier and left floor_expected_red in the same change. THE JOIN THIS CARRIER DECLARED AS INFERENCE IS NOW MEASURED, and that is the substantive result rather than the bookkeeping: unjoined_inference_note stated that closure-dependence was measured for these rows, that the local-binding-shadow defect was measured on its own grid, and that the claim THESE NINE lose their verdict TO THAT DEFECT was inference with no colliding name identified for the six srv3 rows or the two staging rows. It named its own instrument -- fix the resolver and re-run, at which point recovery measures the join and non-recovery isolates a second cause. The resolver is fixed (a lexical binding holding a named top-level function now shadows the free function sharing its spelling; the gate named Value::Closure only and so missed Value::Fn) and ALL NINE RECOVERED. Non-recovery would have isolated a second cause; there is none. The one row that already carried a named colliding symbol, produced_decl_support_preserved, is the confirmation rather than the whole result: its `render` is pattern-bound out of ProducedDeclWired against std.layout's free `fn render(doc, proto)`, the loud different-arity face, and it recovered alongside the eight whose colliding name was never identified. The list stays declared rather than deleted because the CAUSE remains constructible -- a lexical binding holding a NON-CALLABLE value still falls through to a same-named free function, enrolled as its own expected-red row with a census-then-widen trigger -- and an emptied arm with its reason recorded is a different fact from an arm that never existed." + +data closure_dependent_rows: List = [] data closure_independent_repaid_note: String = "EMPTY, AND THAT IS A REPAYMENT RECEIPT RATHER THAN A MISSING MEASUREMENT. This list held the four v2.test.manual.bootstrap_footprint_anchor identities, the only ClosureIndependent / HonestDebtWithStatedTrigger rows in the population. Their cause was a Symbol-declared field holding Int code points: semantic_decl_string_to_bundle_node folded a String into character atoms carrying raw code points, and canonical_hash_of_connective routed that field into content_hash_atom -> atom_identity_hash, which requires a string, so the hash threw before any assertion ran. Repaired at the PRODUCER by giving character atoms a string identity through from_code_point, with code_point as its inverse on the two decoders. All four now ANSWER: three PASS and bootstrap_footprint_canonical_holds FAILS honestly, so the four left this roster and the three passing ones left floor_expected_red in the same change. The list stays declared rather than deleted because the CAUSE remains constructible -- nothing prevents another producer putting a non-Symbol into Atom.identity -- and an emptied arm with its reason recorded is a different fact from an arm that never existed." data closure_independent_rows: List = [] -data unmeasured_rows: List = [ - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.host_phase_status", function: "witness_reconcile_covers_upsert_teardown_and_noop"), - cause: Unmeasured { obstacle: host_phase_unmeasured_note }, - standing: StandingUnmeasured, - measured_evidence: "no small-closure arm exists: claim_batch refuses the narrow run with `no declaration named host_phase_reconcile in this execution's loaded index`" - }, - ClassifiedNonVerdictRow { - identity: non_verdict_row_identity(module_path: "test.claim.host_phase_status", function: "witness_remaining_work_counts_every_unfinished_cell"), - cause: Unmeasured { obstacle: host_phase_unmeasured_note }, - standing: StandingUnmeasured, - measured_evidence: "no small-closure arm exists: claim_batch refuses the narrow run with `no declaration named fleet_subsumption_enrollments in this execution's loaded index`" - } -] +data unmeasured_repaid_note: String = "EMPTY, AND IT WAS REPAID WITHOUT EVER BEING MEASURED, which is a different receipt from the two above and is worth keeping distinct. This list held the two test.claim.host_phase_status identities. They were classified StandingUnmeasured on an honest obstacle: their witness carries ONE import and resolves everything else from the pool, so no narrow closure can even resolve them and there was no small-closure arm to compare against -- host_phase_unmeasured_note records that, and records the refusal to assign them the neighbouring cause merely because they shared an error message. THAT RESTRAINT WAS CORRECT AND IT WAS ALSO NOT NEEDED IN THE END: both now ANSWER and PASS on the required floor after the local-binding-shadow repair, alongside the nine rows that WERE measured as closure-dependent. So the shared cause was real; what was missing was an instrument able to show it, and the repair supplied one that the A/B could not. This is NOT a retroactive classification -- the rows are gone and nothing here claims they were ClosureDependentResolution -- it is the weaker and true statement that a repair aimed elsewhere recovered them too. The list stays declared because the obstacle remains constructible: a witness resolving from the pool rather than from declared imports still has no narrow arm." + +data unmeasured_rows: List = [] data no_classified_non_verdict_rows: List = [] diff --git a/dag/test/claim/floor_non_verdict_classification_witness_test.dag b/dag/test/claim/floor_non_verdict_classification_witness_test.dag index 83d9c90fb2d..158459de68d 100644 --- a/dag/test/claim/floor_non_verdict_classification_witness_test.dag +++ b/dag/test/claim/floor_non_verdict_classification_witness_test.dag @@ -38,15 +38,29 @@ test fn every_classified_non_verdict_row_carries_measured_evidence() -> Bool { every_row_carries_measured_evidence() } +// THE INHABITANCE ROW IS DELETED BECAUSE ITS POPULATION IS REPAID, NOT TO MAKE A TEST AGREE WITH +// BEHAVIOUR. It asserted `stale_enrolment_count() > 0 && unmeasured_count() > 0` -- that neither +// class was empty and neither had swallowed the other -- and it was the right assertion while the +// carrier held a live debt population. Every row is now gone: the nine ClosureDependentResolution +// rows and the two StandingUnmeasured rows all ANSWER and PASS on the required floor after the +// local-binding-shadow repair, and the four ClosureIndependent rows were repaid earlier at their +// own producer. A row asserting that a repaid population is non-empty is not evidence that +// anything works; it is an assertion that the debt must continue to exist, which would make the +// carrier unable to reach the empty terminal state its own header declares. +// +// THE DISTINCTION THIS TURNS ON, stated because the two moves look identical in a diff: editing a +// witness so it agrees with current behaviour is a claim about the world and is forbidden; +// deleting a witness whose SUBJECT no longer exists is dissolution. Nothing here weakens a +// judgment about the classification carrier -- the join, the uniqueness, the evidence-present and +// the exact-partition rows in this file are untouched and still gate, and they are what red if a +// row is added or removed anywhere. What is deleted is a claim about the population's SIZE, which is +// exactly the shape this file already removed once when `row_count() == 15` was found to be a +// change detector. +// +// IT COMES BACK WITH THE DEBT. The carrier keeps both arms declared with their repayment receipts +// precisely because the causes remain constructible; the day a row is authored into either, this +// assertion is the one to restore, and the receipts name what would put it there. test fn standing_partition_is_exact_over_the_population() -> Bool { (stale_enrolment_count() + honest_debt_count() + unmeasured_count()) == classified_non_verdict_row_count() } - -// The result this carrier exists to make unmissable, stated as a partition property rather than -// a literal: SOME rows assert a red that does not exist and SOME were never measured, so neither -// class is empty and neither has swallowed the other. How many are in each is a measurement the -// carrier's rows carry; asserting it here would re-mint the change detector removed above. -test fn both_the_stale_and_the_unmeasured_classes_are_inhabited() -> Bool { - stale_enrolment_count() > 0 && unmeasured_count() > 0 -} diff --git a/src/v2/workflow/floor_non_verdict.dag b/src/v2/workflow/floor_non_verdict.dag index db3eddd0bc6..9ee62091e07 100644 --- a/src/v2/workflow/floor_non_verdict.dag +++ b/src/v2/workflow/floor_non_verdict.dag @@ -100,45 +100,41 @@ import v2.std.text { String } // EMPTY IS THE INTENDED TERMINAL STATE. When every enrolled identity reaches its subject and // answers, this module deletes, and the two collections become ordinary conjuncts over nothing. // -// THE LIVE POPULATION IS 15 IDENTITIES. The original 142-row roster was measured before #9039 +// THE LIVE POPULATION IS ZERO AS OF 2026-08-26, WHICH IS THIS ROSTER'S DECLARED TERMINAL STATE +// AND NOT A HOLE IN IT. Eleven identities stood here -- two test.claim.host_phase_status, six +// test.claim.srv3_subsumption, two v2.test.claim.staging and +// v2.test.emit.produced_decl_support_preserved -- and every one of them now PRODUCES A VERDICT +// and passes, measured by the required floor. They were retired together and by one cause: the +// local-binding-shadow repair, which made a call site spelling a name held by both a local +// binding and a module-level free function reach the LOCAL. The displacement was handing +// `atom_identity_hash` an argument of the wrong type and a record field lookup an Int, so these +// claims THREW before reaching their assertions -- which is exactly the state this roster exists +// to keep from being absorbed, and exactly why eleven of them shared one root nobody could see +// from any individual row. +// +// THE ROWS ARE DELETED AND THE WITNESSES ARE NOT. A non-verdict row admits that an enrolled +// claim stops asserting; it is not an admission about the claim's subject. All eleven remain in +// the ordinary witness roster, now as executing evidence rather than as declared debt. +// +// THE MODULE IS KEPT WITH AN EMPTY ROSTER RATHER THAN DELETED, deliberately: the wall it +// composes into is what refuses a future non-verdict row that is unreachable, and deleting the +// module to celebrate a zero would remove the mechanism along with its current population. Its +// header already names the terminal state; reaching that state is not the same event as +// dissolving the machinery, and conflating them would be the climb that deletes its own +// evidence (DESIGN 4b(4)). +// +// THE PRIOR POPULATION NOTE READ 15 IDENTITIES AND THE ROSTER HELD 11 WHEN THIS EDIT FOUND IT. +// That drift is recorded rather than quietly corrected, because a transcribed count beside a +// list is exactly the second representation that rots without anyone touching either end; the +// count above is derived from the rows this edit removed, and it is zero because the rows are +// gone rather than because anyone counted them. +// +// HISTORICAL: THE LIVE POPULATION WAS 15 IDENTITIES. The original 142-row roster was measured before #9039 // repaired 127 identities, but #9095 authored that stale population after #9039 was already in // its ancestry. The wall then proved those 127 rows unreachable: they were absent from // `floor_expected_red`, so they could never enter either known-red non-verdict arm. Retiring the // exact non-verdict-minus-expected-red set keeps the 15 identities that can classify live debt; // enrolling the other 127 as expected-red instead would fabricate semantic verdicts. fn floor_non_verdict_roster() -> List { - Cons { - head: "test.claim.host_phase_status.witness_reconcile_covers_upsert_teardown_and_noop", - tail: Cons { - head: "test.claim.host_phase_status.witness_remaining_work_counts_every_unfinished_cell", - tail: Cons { - head: "test.claim.srv3_subsumption.comment_only_drift_is_one_change_not_remove_add", - tail: Cons { - head: "test.claim.srv3_subsumption.reconcile_would_teardown_only_if_ownership_claimed_it", - tail: Cons { - head: "test.claim.srv3_subsumption.srv3_and_srv4_disagree_on_convergence", - tail: Cons { - head: "test.claim.srv3_subsumption.srv3_reconcile_adds_exactly_the_missing_fleet_key", - tail: Cons { - head: "test.claim.srv3_subsumption.srv3_reconcile_refuses_both_unowned_keys_never_teardown", - tail: Cons { - head: "test.claim.srv3_subsumption.srv4_reconcile_is_converged_empty_plan", - tail: Cons { - head: "v2.test.claim.staging.cached_stage_hit_skips_stage", - tail: Cons { - head: "v2.test.claim.staging.cached_stage_miss_runs_stage", - tail: Cons { - head: "v2.test.emit.produced_decl_support_preserved.produced_decl_support_survives_augmentation", - tail: Empty {} - } - } - } - } - } - } - } - } - } - } - } + Empty {} }