diff --git a/dag/extdeps/languages/dag/types.dag b/dag/extdeps/languages/dag/types.dag index 5e8e0a6cb02..cd38208e5ed 100644 --- a/dag/extdeps/languages/dag/types.dag +++ b/dag/extdeps/languages/dag/types.dag @@ -13,8 +13,8 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } data dag_type_checkpoints: List = [ - { dag_name: "Int", target_type: "Int", default_expr: "0", is_copy: none, literal_suffix: none }, - { dag_name: "Float", target_type: "Float", default_expr: "0.0", is_copy: none, literal_suffix: none }, - { dag_name: "Bool", target_type: "Bool", default_expr: "false", is_copy: none, literal_suffix: none }, - { dag_name: "String", target_type: "String", default_expr: "\"\"", is_copy: none, literal_suffix: none } + { dag_name: "Int", target_type: "Int", grounding_type: "Int", default_expr: "0", is_copy: none, literal_suffix: none }, + { dag_name: "Float", target_type: "Float", grounding_type: "Float", default_expr: "0.0", is_copy: none, literal_suffix: none }, + { dag_name: "Bool", target_type: "Bool", grounding_type: "Bool", default_expr: "false", is_copy: none, literal_suffix: none }, + { dag_name: "String", target_type: "String", grounding_type: "String", default_expr: "\"\"", is_copy: none, literal_suffix: none } ] diff --git a/dag/extdeps/languages/go/types.dag b/dag/extdeps/languages/go/types.dag index ea23ed3917c..6dccdd47017 100644 --- a/dag/extdeps/languages/go/types.dag +++ b/dag/extdeps/languages/go/types.dag @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } data go_type_checkpoints: List = [ - { dag_name: "Int", target_type: "int64", default_expr: "0", is_copy: none, literal_suffix: none }, - { dag_name: "Float", target_type: "float64", default_expr: "0.0", is_copy: none, literal_suffix: none }, - { dag_name: "Bool", target_type: "bool", default_expr: "false", is_copy: none, literal_suffix: none }, - { dag_name: "Unit", target_type: "struct{}", default_expr: "struct{}{}", is_copy: none, literal_suffix: none }, - { dag_name: "String", target_type: "string", default_expr: "\"\"", is_copy: none, literal_suffix: none }, - { dag_name: "Bytes", target_type: "[]byte", default_expr: "nil", is_copy: none, literal_suffix: none }, - { dag_name: "Secret", target_type: "string", default_expr: "\"\"", is_copy: none, literal_suffix: none }, - { dag_name: "Json", target_type: "interface{}", default_expr: "nil", is_copy: none, literal_suffix: none } + { dag_name: "Int", target_type: "int64", grounding_type: "int64", default_expr: "0", is_copy: none, literal_suffix: none }, + { dag_name: "Float", target_type: "float64", grounding_type: "float64", default_expr: "0.0", is_copy: none, literal_suffix: none }, + { dag_name: "Bool", target_type: "bool", grounding_type: "bool", default_expr: "false", is_copy: none, literal_suffix: none }, + { dag_name: "Unit", target_type: "struct{}", grounding_type: "struct{}", default_expr: "struct{}{}", is_copy: none, literal_suffix: none }, + { dag_name: "String", target_type: "string", grounding_type: "string", default_expr: "\"\"", is_copy: none, literal_suffix: none }, + { dag_name: "Bytes", target_type: "[]byte", grounding_type: "[]byte", default_expr: "nil", is_copy: none, literal_suffix: none }, + { dag_name: "Secret", target_type: "string", grounding_type: "string", default_expr: "\"\"", is_copy: none, literal_suffix: none }, + { dag_name: "Json", target_type: "interface{}", grounding_type: "interface{}", default_expr: "nil", is_copy: none, literal_suffix: none } ] data go_algebra_inhabitants: List = [ diff --git a/dag/extdeps/languages/python/types.dag b/dag/extdeps/languages/python/types.dag index a19e45da30d..1656c9b54c0 100644 --- a/dag/extdeps/languages/python/types.dag +++ b/dag/extdeps/languages/python/types.dag @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } data python_type_checkpoints: List = [ - { dag_name: "Int", target_type: "int", default_expr: "0", is_copy: none, literal_suffix: none }, - { dag_name: "Float", target_type: "float", default_expr: "0.0", is_copy: none, literal_suffix: none }, - { dag_name: "Bool", target_type: "bool", default_expr: "False", is_copy: none, literal_suffix: none }, - { dag_name: "Unit", target_type: "None", default_expr: "None", is_copy: none, literal_suffix: none }, - { dag_name: "String", target_type: "str", default_expr: "\"\"", is_copy: none, literal_suffix: none }, - { dag_name: "Bytes", target_type: "bytes", default_expr: "b\"\"", is_copy: none, literal_suffix: none }, - { dag_name: "Secret", target_type: "str", default_expr: "\"\"", is_copy: none, literal_suffix: none }, - { dag_name: "Json", target_type: "dict", default_expr: "{}", is_copy: none, literal_suffix: none } + { dag_name: "Int", target_type: "int", grounding_type: "int", default_expr: "0", is_copy: none, literal_suffix: none }, + { dag_name: "Float", target_type: "float", grounding_type: "float", default_expr: "0.0", is_copy: none, literal_suffix: none }, + { dag_name: "Bool", target_type: "bool", grounding_type: "bool", default_expr: "False", is_copy: none, literal_suffix: none }, + { dag_name: "Unit", target_type: "None", grounding_type: "None", default_expr: "None", is_copy: none, literal_suffix: none }, + { dag_name: "String", target_type: "str", grounding_type: "str", default_expr: "\"\"", is_copy: none, literal_suffix: none }, + { dag_name: "Bytes", target_type: "bytes", grounding_type: "bytes", default_expr: "b\"\"", is_copy: none, literal_suffix: none }, + { dag_name: "Secret", target_type: "str", grounding_type: "str", default_expr: "\"\"", is_copy: none, literal_suffix: none }, + { dag_name: "Json", target_type: "dict", grounding_type: "dict", default_expr: "{}", is_copy: none, literal_suffix: none } ] data python_algebra_inhabitants: List = [ diff --git a/dag/extdeps/languages/rust/types.dag b/dag/extdeps/languages/rust/types.dag index e72f6f748ee..02b95d4031d 100644 --- a/dag/extdeps/languages/rust/types.dag +++ b/dag/extdeps/languages/rust/types.dag @@ -16,20 +16,20 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } data rust_type_checkpoints: List = [ - { dag_name: "Int", target_type: "i64", default_expr: "0", is_copy: true, literal_suffix: none }, - { dag_name: "Float", target_type: "f64", default_expr: "0.0", is_copy: true, literal_suffix: none }, - { dag_name: "Bool", target_type: "bool", default_expr: "false", is_copy: true, literal_suffix: none }, - { dag_name: "Symbol", target_type: "String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, - { dag_name: "Unit", target_type: "()", default_expr: "()", is_copy: true, literal_suffix: none }, - { dag_name: "String", target_type: "String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, - { dag_name: "Bytes", target_type: "Vec", default_expr: "Vec::new()", is_copy: false, literal_suffix: none }, - { dag_name: "Secret", target_type: "String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, - { dag_name: "Json", target_type: "serde_json::Value", default_expr: "serde_json::Value::Null", is_copy: false, literal_suffix: none } + { dag_name: "Int", target_type: "i64", grounding_type: "i64", default_expr: "0", is_copy: true, literal_suffix: none }, + { dag_name: "Float", target_type: "f64", grounding_type: "f64", default_expr: "0.0", is_copy: true, literal_suffix: none }, + { dag_name: "Bool", target_type: "bool", grounding_type: "bool", default_expr: "false", is_copy: true, literal_suffix: none }, + { dag_name: "Symbol", target_type: "String", grounding_type: "String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, + { dag_name: "Unit", target_type: "()", grounding_type: "()", default_expr: "()", is_copy: true, literal_suffix: none }, + { dag_name: "String", target_type: "String", grounding_type: "std::string::String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, + { dag_name: "Bytes", target_type: "Vec", grounding_type: "Vec", default_expr: "Vec::new()", is_copy: false, literal_suffix: none }, + { dag_name: "Secret", target_type: "String", grounding_type: "String", default_expr: "String::new()", is_copy: false, literal_suffix: ".to_string()" }, + { dag_name: "Json", target_type: "serde_json::Value", grounding_type: "serde_json::Value", default_expr: "serde_json::Value::Null", is_copy: false, literal_suffix: none } ] data rust_checkpoint_hash_row_retired_note: String = "The Hash row is RETIRED, not rebound, and the distinction is the rule it follows: a target row survives only where some exact source declaration genuinely realizes that way. A census of every `type Hash` declaration in the corpus finds exactly ONE -- v2.std.node.Hash = Fnv1a64Structural (src/v2/std/node.dag) -- and it must NOT realize as v1_rt::Hash. Every remaining occurrence of that spelling in the seed is inside a STRING LITERAL in v1.runtime_rust, which is generated v1_rt.rs text rather than a .dag type reference, so no declaration is left for the row to bind. WHAT THE ROW COST WHILE IT STOOD, measured rather than predicted: Fnv1a64Structural's public record constructors are deleted precisely so the `where lower_hex_16` refinement IS its construction wall (std.content_hash content_hash_family_constructor_note), and this row rendered that carrier away as a bare String alias, taking the wall with it -- a DESIGN 4b construction rung demoted with no diagnostic anywhere. The live specimen is the emitted 05_eval closure: v2_std_node.rs carried `pub type Hash = v1_rt::Hash` while functions in the SAME file returned Rc, and the two disagreed at 70 distinct E0308 sites. checkpoint_table_bypasses_identity_note recorded this class from declarations at both ends and stated that no live site had been produced by anyone; that emission is the site. Retiring the row is INDEPENDENT of keying the remaining rows on declaration identity: those rows still bypass identity, still answer one spelling for two declarations, and the emitter's type renderer carries no module plumbing to key them on -- see checkpoint_table_bypasses_identity_note for that residue, which this change does not close." -data rust_checkpoint_scalar_arity_note: String = "A TypeCheckpoint row states one thing: how a target SPELLS a dag type whose Rust arity is zero. It cannot express arity, so membership of this table IS the emitter's arity-0 claim — v1.compiler.05_emit_rust rust_scalar_checkpoint_render_base reads it, and rust_render_checkpoint_scalar_bare strips every type argument from any leaf it matches (the E0109 wall, rust_checkpoint_scalar_phantom_params_note). Witness/witness rows were removed here 2026-08-16: Witness is the generic enum v2.std.witness.Witness (src/v2/std/witness.dag), arity 1 by its single authority std.types container_type_arity, so the rows made the emitter drop the argument of every Witness in type position and emit `Rc` — rustc E0107 'missing generics for enum Witness', 4 sites in the 06_translate closure alone (docs/probes/root_d_generic_arity_2026-08-16.md). Nothing else was lost with them: coerce_primitive_type renders the bare leaf name 'Witness' through qualified_last_segment either way, and is_copy's Absent arm and Present\{false\} arm are the same decision at every consumer. A generic type may not be added to this table; its spelling is not the missing fact, its arity is." +data rust_checkpoint_scalar_arity_note: String = "A TypeCheckpoint row states one thing: how a target SPELLS a dag type whose Rust arity is zero. It cannot express arity, so membership of this table IS the emitter's arity-0 claim — v1.compiler.05_emit_rust rust_scalar_checkpoint_reference_base reads it, and rust_render_checkpoint_scalar_bare strips every type argument from any leaf it matches (the E0109 wall, rust_checkpoint_scalar_phantom_params_note). Witness/witness rows were removed here 2026-08-16: Witness is the generic enum v2.std.witness.Witness (src/v2/std/witness.dag), arity 1 by its single authority std.types container_type_arity, so the rows made the emitter drop the argument of every Witness in type position and emit `Rc` — rustc E0107 'missing generics for enum Witness', 4 sites in the 06_translate closure alone (docs/probes/root_d_generic_arity_2026-08-16.md). Nothing else was lost with them: coerce_primitive_type renders the bare leaf name 'Witness' through qualified_last_segment either way, and is_copy's Absent arm and Present\{false\} arm are the same decision at every consumer. A generic type may not be added to this table; its spelling is not the missing fact, its arity is." data rust_algebra_inhabitants: List = [ diff --git a/dag/extdeps/languages/typescript/types.dag b/dag/extdeps/languages/typescript/types.dag index 1cf520b2bf8..78b75907838 100644 --- a/dag/extdeps/languages/typescript/types.dag +++ b/dag/extdeps/languages/typescript/types.dag @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } data ts_type_checkpoints: List = [ - { dag_name: "Int", target_type: "number", default_expr: "0", is_copy: true, literal_suffix: none }, - { dag_name: "Float", target_type: "number", default_expr: "0.0", is_copy: true, literal_suffix: none }, - { dag_name: "Bool", target_type: "boolean", default_expr: "false", is_copy: true, literal_suffix: none }, - { dag_name: "Unit", target_type: "undefined", default_expr: "undefined", is_copy: true, literal_suffix: none }, - { dag_name: "String", target_type: "string", default_expr: "\"\"", is_copy: false, literal_suffix: none }, - { dag_name: "Bytes", target_type: "Uint8Array", default_expr: "new Uint8Array()", is_copy: false, literal_suffix: none }, - { dag_name: "Secret", target_type: "string", default_expr: "\"\"", is_copy: false, literal_suffix: none }, - { dag_name: "Json", target_type: "unknown", default_expr: "null", is_copy: false, literal_suffix: none } + { dag_name: "Int", target_type: "number", grounding_type: "number", default_expr: "0", is_copy: true, literal_suffix: none }, + { dag_name: "Float", target_type: "number", grounding_type: "number", default_expr: "0.0", is_copy: true, literal_suffix: none }, + { dag_name: "Bool", target_type: "boolean", grounding_type: "boolean", default_expr: "false", is_copy: true, literal_suffix: none }, + { dag_name: "Unit", target_type: "undefined", grounding_type: "undefined", default_expr: "undefined", is_copy: true, literal_suffix: none }, + { dag_name: "String", target_type: "string", grounding_type: "string", default_expr: "\"\"", is_copy: false, literal_suffix: none }, + { dag_name: "Bytes", target_type: "Uint8Array", grounding_type: "Uint8Array", default_expr: "new Uint8Array()", is_copy: false, literal_suffix: none }, + { dag_name: "Secret", target_type: "string", grounding_type: "string", default_expr: "\"\"", is_copy: false, literal_suffix: none }, + { dag_name: "Json", target_type: "unknown", grounding_type: "unknown", default_expr: "null", is_copy: false, literal_suffix: none } ] data ts_algebra_inhabitants: List = [ diff --git a/dag/gunbc/empty_decl_file_checkpoint_bypass.dag b/dag/gunbc/empty_decl_file_checkpoint_bypass.dag new file mode 100644 index 00000000000..ac0d2f19144 --- /dev/null +++ b/dag/gunbc/empty_decl_file_checkpoint_bypass.dag @@ -0,0 +1,66 @@ +module gunbc.empty_decl_file_checkpoint_bypass + +import std.types { List, String } +import std.decl_ref { DeclarationRef, decl_ref } +import std.dissolution { DissolutionCondition, unbound_dissolution } + +// WHEN A SITE REACHES EMISSION WITH NO DECLARATION IDENTITY, THE IDENTITY-KEYED ROSTER IS NOT +// CONSULTED AT ALL. +// +// v1.compiler.coercion lookup_checkpoint answers straight from the bare-name table when decl_file +// is the empty string: decl_file_declares_structurally returns false before it reaches +// structural_declaration_modules_for, so the roster that exists precisely to say "this declaration +// is structural, refuse the table's spelling" never runs. Every consequence the roster was built to +// prevent is therefore live for any site whose declaration identity was not threaded to the call. +// +// THIS IS NOT THE ARITY DEFECT THE SPLIT CLOSED, AND THE TWO ARE DELIBERATELY NOT FILED TOGETHER. +// The split (TypeCheckpoint's reference_ / grounding_ spellings) governs what a row may SAY once +// identity is known. This bypass governs whether identity is CONSULTED. A correct answer to the +// first question is delivered to the wrong decision whenever the second fails, so closing one does +// nothing for the other. +// +// A KNOWN INSTANCE, kept because it is the one that was measured rather than reasoned: +// v1.compiler.05_emit emit_literal passes decl_file "" for every String literal, so literal_suffix +// at production sites answers from the table for every literal regardless of which module the +// surrounding reference resolves to. That instance already executes as a row in +// v1.tests.claim.checkpoint_identity_keying_witness_test +// (literal_suffix_production_call_site_never_threads_declaration_identity). + +type BypassInstance { + caller: DeclarationRef + position: String + evidence: DeclarationRef +} + +data empty_decl_file_bypass_instances: List = [ + { + caller: decl_ref(module_path: "v1.compiler.05_emit", decl_name: "emit_literal"), + position: "String literal rendering: decl_file is passed as the empty string unconditionally", + evidence: decl_ref(module_path: "v1.tests.claim.checkpoint_identity_keying_witness_test", decl_name: "literal_suffix_production_call_site_never_threads_declaration_identity"), + }, +] + +// THE POPULATION IS UNCOUNTED AND NO ESTIMATE IS OFFERED. +// +// One instance is listed because it was executed, not because a census found one. No sweep of +// lookup_checkpoint's transitive call sites for a hardcoded or unthreaded decl_file has been run. +// The list above is therefore a LOWER BOUND of one, and a reader must not take it as the extent of +// the class -- an unmeasured population stated as a small number is the fabricated-plausible-output +// failure applied to a ceiling disclosure. +type PopulationBasis + = UncountedNoSweepRun { named_instances_are: String } + | SweptCallSites { sweep: String } + +data empty_decl_file_bypass_population: PopulationBasis = UncountedNoSweepRun { + named_instances_are: "instances that surfaced while measuring something else; the sweep over lookup_checkpoint's transitive call sites has not been run", +} + +// RUNG. The class sits at MITIGATABLE: nothing refuses when identity is missing -- the table answers +// and emission proceeds with plausible output. The next rung is a REFUSAL at lookup_checkpoint when +// decl_file is empty, which is decidable today and blocked only on the call sites that would then +// refuse being made to thread identity first. That ordering is the whole of the work: the refusal is +// one arm, the threading is the population above, and the refusal cannot land before the population +// is known or it converts an uncounted silence into an uncounted red. +data empty_decl_file_bypass_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: lookup_checkpoint refuses rather than answering from the bare-name table when decl_file is empty, and every production call site threads a resolved declaration file, established by execution against a discriminating red at a site that previously answered from the table. Not satisfied by threading identity at the listed instance alone while the population remains UncountedNoSweepRun -- the sweep is the precondition for the refusal, not a follow-up to it.") + +data empty_decl_file_bypass_surfaced_by: DeclarationRef = decl_ref(module_path: "v1.compiler.emit_rust", decl_name: "checkpoint_table_bypasses_identity_note") diff --git a/dag/std/coercion.dag b/dag/std/coercion.dag index 838f3081d51..643490fad4c 100644 --- a/dag/std/coercion.dag +++ b/dag/std/coercion.dag @@ -3,11 +3,52 @@ module std.coercion type TypeCheckpoint { dag_name: String target_type: String + grounding_type: String default_expr: String? is_copy: Bool? literal_suffix: String? } +// WHY A CHECKPOINT CARRIES TWO SPELLINGS, AND WHY THE SECOND IS NOT A REFINEMENT OF THE FIRST. +// +// A checkpoint is asked two different questions by two different consumers, and one field could only +// ever answer one of them: +// +// target_type -- REFERENCE position. What does the target render where a program MENTIONS this +// type? In Rust, the dag name String renders as the bare `String`, which is +// correct and idiomatic wherever a type is mentioned. +// grounding_type -- DECLARATION right-hand side. What host type is a declaration of this name +// GROUNDED IN? Here the bare spelling is not merely unidiomatic, it is wrong: +// `pub type String = String;` is self-referential, and the alias being defined +// shadows the very name its right-hand side is trying to reach. The grounding +// spelling is `std::string::String`, which no alias can shadow. +// +// The two coincide for most rows -- i64, bool and () are unshadowable spellings -- and where they +// coincide the row says so explicitly rather than defaulting, because a default is a rule and a rule +// is what this split exists to remove. +// +// WHAT THIS REPLACES, so the shape is not re-collapsed later. One field answering both questions is +// a TWO-ROLE defect, not a wrong value: whichever spelling the field carries, one consumer is wrong. +// (The word ARITY is deliberately avoided: in this area it already means type-parameter count -- +// v1.compiler.emit_rust carries AliasDeclArityVerdict and a scalar declared-arity guard -- so naming +// this defect that way would collide with a live, different meaning a few declarations away.) +// The cost while it stood was a compensating fork at the consumer -- v1.compiler.emit_rust's type +// alias arm special-cased `item_text == "String"` and emitted the grounded line by hand, ahead of and +// bypassing the identity-keyed authority every other consumer already routed through. So the +// declaration site could not honour declaration identity even after the reference side did, and one +// emitted file disagreed with itself. Splitting the field deletes that arm rather than guarding it: +// the next name whose reference spelling collides with its own declaration cannot reach the +// ambiguity, because there is no longer a single field for it to be ambiguous in (DESIGN section 4b +// -- construction, not a wall over a state that stays writable). +// +// ON THE NAME `target_type`, WHICH IS NARROWER THAN IT READS. It now means the REFERENCE-position +// spelling and nothing broader -- it is not the general answer to "what is this type in the target", +// because that question no longer has a single answer here. The name survives only because renaming +// it to reference_type reaches every target table; it is the same one-name-two-meanings shape this +// split removed from the field's VALUE, still standing in its NAME. A reader must not take +// target_type for the universal spelling, and a new consumer must decide which of the two questions +// it is asking rather than reaching for the familiar name. + // TypeCheckpoint (above) is cited to the target LANGUAGE reference and states how a spelling // renders. TypeRealizationDecision is the gunbc-corpus fact answering which of a named // declaration's possible renderings actually applies at a given reference, keyed on declaration diff --git a/dag/test/claim/checkpoint_identity_keying_witness_test.dag b/dag/test/claim/checkpoint_identity_keying_witness_test.dag index e6e43e024b2..f92cb397117 100644 --- a/dag/test/claim/checkpoint_identity_keying_witness_test.dag +++ b/dag/test/claim/checkpoint_identity_keying_witness_test.dag @@ -6,7 +6,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Executing floor migration of src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag // (that file cannot execute -- src/v1 is not a --source-root in any workflow, so its -// `import v1.compiler.emit_rust { rust_scalar_checkpoint_render_base }` is structurally +// `import v1.compiler.emit_rust { rust_scalar_checkpoint_reference_base }` is structurally // unresolvable under the required floor; see checkpoint_table_bypasses_identity_note in // src/v1/05_emit_rust.dag for the mechanism this reproduces black-box). // @@ -18,7 +18,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // (dag_name, decl_file) pair without ever importing v1.compiler.* directly. // // ONE of the SEVEN keying/residue rows from the original oracle executes here, -// CONFIRMED BY REAL EXECUTION (not by reading rust_scalar_checkpoint_render_base's return +// CONFIRMED BY REAL EXECUTION (not by reading rust_scalar_checkpoint_reference_base's return // value, which this black-box surface never observes directly -- it observes the emitted // field's Rust rendering, one layer downstream): // - table_absent_name_realizes_natively_for_the_std_declaration (Nat, dag/std/nat.dag): @@ -26,7 +26,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // -- realizing natively means importing the shared std_nat alias module, NOT inlining // the literal "i64". Confirmed by direct capture of the emitted file: the substring // "i64" does not occur anywhere in it. The original oracle's `must_contain: ["i64"]` -// was authored against rust_scalar_checkpoint_render_base's own return value and does +// was authored against rust_scalar_checkpoint_reference_base's own return value and does // not hold for this file's black-box observation surface; asserting on "std_nat" instead // is the correct discriminator for THIS surface, not a weakened claim. // @@ -69,7 +69,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // the wrong reason and mislead a future reader into re-diagnosing checkpoint identity // keying instead of this namespace-resolution gap -- so, per the same discipline as the // empty-decl_file row, it is recorded here as an honest gap rather than migrated. -data checkpoint_identity_keying_migration_note: String = "Migrated from src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag per the src-v1-outside-every-workflow-source-root gap: that file's rows are real assertions about rust_scalar_checkpoint_render_base but cannot execute in CI. Of its seven rows, exactly ONE executes here as real evidence, via compile_dag_rust_emit_check's transitive-import mechanism, which gives a fixture field reference the SAME resolved decl_file as the real declaration it imports -- CORRECTED BY REAL EXECUTION (2026-08-19) from an earlier draft of this file that asserted must_contain: [\"i64\"] for the native-Nat row without having executed it: the real emitted field renders as `pub field: Nat` behind a `crate::std_nat` type-alias import, and the literal substring \"i64\" does not appear in that file at all, because this black-box surface observes the emitter's field rendering one layer downstream of rust_scalar_checkpoint_render_base's own return value, where a native realization imports the shared alias module rather than inlining the scalar name.\n\nThe remaining SIX rows are honest, permanently-excluded gaps, each confirmed by real execution rather than assumed, none of them deferred to a later commit or PR:\n - table_present_name_renders_from_the_table (Int, dag/std/integer.dag): EXECUTED at authorship time (bare \"i64\" rendering, confirmed true), then REMOVED from the executing set on 2026-08-19 for real, measured cost -- see checkpoint_identity_keying_int_table_present_cost_note below for the full account. This is a cost gap, not a correctness gap: the assertion is not in doubt, only its right to run in the fast lane.\n - unknown_declaration_identity_refuses_rather_than_guessing (empty decl_file): unreachable from any ordinary parsed source reference, since every reachable reference carries a real ident_span; the empty-identity arm has no construction path through this surface.\n - same_spelling_different_declaration_does_not_realize_natively (cross-decl, v2.std.nat.Nat): hard-fails to compile, hard_diagnostics=9, every diagnostic located in src/v2/std/node.dag and none related to Nat/coercion/checkpoint -- v2.std.node references std.occurrence_identity by bare qualified name with no explicit import, and this surface's import-closure-based dependency discovery never follows that namespace-only reference to load dag/std/occurrence_identity.dag.\n - residue_table_present_int_bypasses_identity (Int under a src/v2 decl path): the same import-closure-vs-namespace-only-resolution gap, reached through a different corpus path -- v2.std.integer.dag itself references v2.std.nat.Nat by bare qualified name with no explicit import (UnlistedImportUse), and its transitive closure also reaches dag/std/measure.dag's 45+ pre-existing UnlistedImportUse diagnostics, none related to Int, Nat, coercion, or checkpoint rendering. hard_diagnostics is nonzero purely from this unrelated closure; the target file is never emitted and checkpoint identity keying is never exercised for this fixture.\n - residue_table_present_string_bypasses_identity: RETIRED at the source level, not reproduced here -- structural_declaration_modules_for (v1.compiler.coercion) now enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which DO declare String (type String = FreeMonoid), correcting an earlier draft of this note that claimed no such v2 declaration path existed. The legacy oracle's residue row is replaced by two CLOSED rows (table_present_string_refuses_under_structural_declaration_text / _string_type asserting == none), mirroring table_present_hash_refuses_under_structural_declaration; like that Hash row, the String closure is evidenced by the legacy oracle's authored assertion plus the coercion.dag source, not by this black-box surface, and is not migrated here for the same reason.\n - table_present_hash_refuses_under_structural_declaration (the CLOSED Hash row): not reproduced here either -- the legacy oracle's own note records this row as already CLOSED (structural_declaration_modules_for enrolls Hash), so it needs no black-box migration; the closure is evidenced by the legacy oracle's authored assertion plus the coercion.dag source, not by this surface.\n\nFive of the six gaps are structural properties of the compile_dag_rust_emit_check witness-authoring surface itself (import-closure dependency discovery vs. namespace-only resolution) or of unclaimed scope (String), NOT checkpoint-identity-keying defects; the sixth (table_present_name_renders_from_the_table) is a real-cost gap, also not a checkpoint-identity-keying defect. NONE are in T7's scope to repair. No test fn for any of the six is included in the executing set, to avoid a red whose real cause is unrelated to what the row's name claims to test." +data checkpoint_identity_keying_migration_note: String = "Migrated from src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag per the src-v1-outside-every-workflow-source-root gap: that file's rows are real assertions about rust_scalar_checkpoint_reference_base but cannot execute in CI. Of its seven rows, exactly ONE executes here as real evidence, via compile_dag_rust_emit_check's transitive-import mechanism, which gives a fixture field reference the SAME resolved decl_file as the real declaration it imports -- CORRECTED BY REAL EXECUTION (2026-08-19) from an earlier draft of this file that asserted must_contain: [\"i64\"] for the native-Nat row without having executed it: the real emitted field renders as `pub field: Nat` behind a `crate::std_nat` type-alias import, and the literal substring \"i64\" does not appear in that file at all, because this black-box surface observes the emitter's field rendering one layer downstream of rust_scalar_checkpoint_reference_base's own return value, where a native realization imports the shared alias module rather than inlining the scalar name.\n\nThe remaining SIX rows are honest, permanently-excluded gaps, each confirmed by real execution rather than assumed, none of them deferred to a later commit or PR:\n - table_present_name_renders_from_the_table (Int, dag/std/integer.dag): EXECUTED at authorship time (bare \"i64\" rendering, confirmed true), then REMOVED from the executing set on 2026-08-19 for real, measured cost -- see checkpoint_identity_keying_int_table_present_cost_note below for the full account. This is a cost gap, not a correctness gap: the assertion is not in doubt, only its right to run in the fast lane.\n - unknown_declaration_identity_refuses_rather_than_guessing (empty decl_file): unreachable from any ordinary parsed source reference, since every reachable reference carries a real ident_span; the empty-identity arm has no construction path through this surface.\n - same_spelling_different_declaration_does_not_realize_natively (cross-decl, v2.std.nat.Nat): hard-fails to compile, hard_diagnostics=9, every diagnostic located in src/v2/std/node.dag and none related to Nat/coercion/checkpoint -- v2.std.node references std.occurrence_identity by bare qualified name with no explicit import, and this surface's import-closure-based dependency discovery never follows that namespace-only reference to load dag/std/occurrence_identity.dag.\n - residue_table_present_int_bypasses_identity (Int under a src/v2 decl path): the same import-closure-vs-namespace-only-resolution gap, reached through a different corpus path -- v2.std.integer.dag itself references v2.std.nat.Nat by bare qualified name with no explicit import (UnlistedImportUse), and its transitive closure also reaches dag/std/measure.dag's 45+ pre-existing UnlistedImportUse diagnostics, none related to Int, Nat, coercion, or checkpoint rendering. hard_diagnostics is nonzero purely from this unrelated closure; the target file is never emitted and checkpoint identity keying is never exercised for this fixture.\n - residue_table_present_string_bypasses_identity: RETIRED at the source level, not reproduced here -- structural_declaration_modules_for (v1.compiler.coercion) now enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which DO declare String (type String = FreeMonoid), correcting an earlier draft of this note that claimed no such v2 declaration path existed. The legacy oracle's residue row is replaced by two CLOSED rows (table_present_string_refuses_under_structural_declaration_text / _string_type asserting == none), mirroring table_present_hash_refuses_under_structural_declaration; like that Hash row, the String closure is evidenced by the legacy oracle's authored assertion plus the coercion.dag source, not by this black-box surface, and is not migrated here for the same reason.\n - table_present_hash_refuses_under_structural_declaration (the CLOSED Hash row): not reproduced here either -- the legacy oracle's own note records this row as already CLOSED (structural_declaration_modules_for enrolls Hash), so it needs no black-box migration; the closure is evidenced by the legacy oracle's authored assertion plus the coercion.dag source, not by this surface.\n\nFive of the six gaps are structural properties of the compile_dag_rust_emit_check witness-authoring surface itself (import-closure dependency discovery vs. namespace-only resolution) or of unclaimed scope (String), NOT checkpoint-identity-keying defects; the sixth (table_present_name_renders_from_the_table) is a real-cost gap, also not a checkpoint-identity-keying defect. NONE are in T7's scope to repair. No test fn for any of the six is included in the executing set, to avoid a red whose real cause is unrelated to what the row's name claims to test." // checkpoint_identity_keying_int_table_present_cost_note: table_present_name_renders_from_the_table // (Int, dag/std/integer.dag) was authored and confirmed executing (bare "i64" rendering) before diff --git a/dag/test/claim/hash_checkpoint_retired_witness_test.dag b/dag/test/claim/hash_checkpoint_retired_witness_test.dag index b2fc88ec74c..17e18d5fc68 100644 --- a/dag/test/claim/hash_checkpoint_retired_witness_test.dag +++ b/dag/test/claim/hash_checkpoint_retired_witness_test.dag @@ -8,7 +8,7 @@ data hash_checkpoint_retired_witness_note: String = "PERMANENT REGRESSION CONTRO WHY THIS LIVES HERE RATHER THAN BESIDE THE EMITTER. The predecessor assertions lived in src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag, and that tree DOES NOT EXECUTE: the required floor runs claim_executor with source roots dag and src/v2 only, src/v1 appears in no workflow, and a run log carrying 619 v2.test rows carries zero v1.tests rows. Seventeen witness files and 127 test fns sit there unexecuted. So the earlier repair -- which moved these assertions OUT of a generated #[cfg(test)] block that CI never compiles -- landed them somewhere CI never discovers, repeating the class it was written to correct one layer over. A control that does not execute is specification without execution, whatever its name says. -WHY BEHAVIOURAL RATHER THAN A DIRECT CALL. Asserting rust_scalar_checkpoint_render_base returns none proves the lookup answers nothing; it does not prove the EMITTER stops writing v1_rt::Hash. This compiles a module and reads the emitted bytes, so it fails if any path -- checkpoint, alias renderer, or a future re-binding -- puts that spelling back. The bare spelling is the load-bearing input because the retired table was keyed on it, so the fixture declares its own Hash rather than importing v2.std.node: compile_dag_rust_emit_check compiles a virtual single-module source through the witness-root index, where importing v2.std.node refuses with hard diagnostics and would make this claim unrunnable rather than red. That is the same construction, and the same reason, as the sibling root_d_checkpoint_scalar_declared_arity_witness. +WHY BEHAVIOURAL RATHER THAN A DIRECT CALL. Asserting rust_scalar_checkpoint_reference_base returns none proves the lookup answers nothing; it does not prove the EMITTER stops writing v1_rt::Hash. This compiles a module and reads the emitted bytes, so it fails if any path -- checkpoint, alias renderer, or a future re-binding -- puts that spelling back. The bare spelling is the load-bearing input because the retired table was keyed on it, so the fixture declares its own Hash rather than importing v2.std.node: compile_dag_rust_emit_check compiles a virtual single-module source through the witness-root index, where importing v2.std.node refuses with hard diagnostics and would make this claim unrunnable rather than red. That is the same construction, and the same reason, as the sibling root_d_checkpoint_scalar_declared_arity_witness. Dissolve-on: when lookup_checkpoint is re-keyed from a bare String to a resolved declaration identity, the spelling stops being the key and this fixture imports the authority instead." diff --git a/dag/tools/self_host_std_bridge_shims/v2_std_integer.rs b/dag/tools/self_host_std_bridge_shims/v2_std_integer.rs index 1c7e9cc3c2f..dd46ee67bcd 100644 --- a/dag/tools/self_host_std_bridge_shims/v2_std_integer.rs +++ b/dag/tools/self_host_std_bridge_shims/v2_std_integer.rs @@ -15,7 +15,7 @@ // REPRESENTATION DIVERGENCE (deliberate, and narrow): its one consumer today is the // 03_normalize row, whose narrow lib re-exports `Int` without using it in a typed position, so // the checkpoint -// scalar rendering (rust_scalar_checkpoint_render_base, Int -> i64) is sufficient here and +// scalar rendering (rust_scalar_checkpoint_reference_base, Int -> i64) is sufficient here and // keeps the bridge free of the Nat coproduct. If a consumer ever uses Int in a typed position // this alias is wrong and must be grounded on the real GroupCompletion pair construction. // diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index c13c2c0b806..7b8b9160336 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -322,10 +322,6 @@ fn render_rust_text_carrier(shared_types: Set) -> String { render_rust_shared_type_if_needed(type_name: "String", rendered: "String", shared_types: shared_types) } -fn rust_string_grounded_type_alias_decl_line() -> String { - concat(rust_visibility_prefix(), rust_items().type_alias_keyword, " String = std::string::String;") -} - fn emit_rust_host_to_dag_string_via_seam(host_expr: String) -> String { host_expr } @@ -453,11 +449,53 @@ data reference_use_lines_representation_invariant_note: String = "Use-lines are data numeric_realization_relocation_note: String = "RELOCATED to v1.compiler.coercion (smart-ram-730, adhoc-2ea6fb98-a3f, 2026-08-21, review 54335): numeric_realization_identity_note, numeric_realization_roster_extension_note, numeric_realization_declaring_modules, decl_file_realizes_natively and rust_seed_host_numeric_alias moved there in full, completing the relocation checkpoint_table_bypasses_identity_note's structural_declaration_modules_for precedent already established for the negative-form (structural) half of this same two-authority shape -- this was the positive-form (native) half, still sitting in this module and reached back into by v1.compiler.coercion type_realization_decision, an import cycle DESIGN section 3 forbids (emit_rust already imports FROM coercion; coercion calling back into emit_rust closes the cycle). This module now imports only rust_seed_host_numeric_alias back from v1.compiler.coercion, exactly as it already imports lookup_checkpoint from there -- one direction, no cycle; numeric_realization_declaring_modules and decl_file_realizes_natively have no consumer left in this module, since rust_seed_host_numeric_alias was their only caller here and it moved with them. Agreed with swift-moth-294 (msg_502982ac, 2026-08-21) and sequenced behind gunbc#8716 (merged 2026-08-21T06:19:19Z), which is why the move landed now rather than when first proposed." -data checkpoint_table_bypasses_identity_note: String = "CEILING, STATED BECAUSE THE CODE DELIVERS LESS THAN THE DELETION OF RustCorpusRepr SUGGESTS. lookup_checkpoint is keyed on the BARE dag_name and is consulted BEFORE the identity-keyed arm, so any name carrying a checkpoint row in extdeps/languages/rust/types.dag bypasses declaration keying entirely. Nat carries no row and therefore discriminates correctly -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag refuses. Names WITH a row do not. This is not a regression introduced here: the table was already bare-name keyed and the global corpus mode was hiding the question. It is the honest rung. The class is MECHANICALLY PREVENTABLE rather than structurally impossible, and its executing evidence is v1.tests.claim.checkpoint_identity_keying_witness_test, which asserts the CURRENT bypassing answers on purpose so the gap is counted instead of assumed closed. THAT CITATION WAS FALSE WHEN THIS NOTE FIRST LANDED AND IS REPAIRED RATHER THAN SOFTENED. It named the residue block generated by v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into a module declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate -- while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package consuming v1-compiler as an ordinary dependency, so cfg(test) is never set for it and the block is not compiled, let alone executed. Measured rather than reasoned: that step's binary enumerates 30 tests and none is this one, against a positive control confirming the enumeration is non-empty. So a ceiling disclosure cited evidence that had never run -- DESIGN section 4b(1) rung honesty violated in the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The assertions were re-authored as an enrolled .dag witness and now execute (seven rows PASS, including the discriminating row where two declarations share the spelling Nat and answer differently); the superseded generated-Rust block is deleted rather than left standing as a second, silent copy. POPULATION (census by vivid-wren-870, who owns the rows): SEVEN of the table's names are also declared under src/v2 -- Int, Float, Bool, Symbol, Unit, String, Hash; Bytes, Secret and Json are not. That is a LOWER BOUND obtained by grepping line-start `type ` declarations under src/v2; it does not find names introduced any other way, and it says NOTHING about how many sites bite in any real closure. Three of the seven are the same shape as Int in that the v2 declaration is a genuinely different STRUCTURE rather than a spelling coincidence -- Int is GroupCompletion, String is FreeMonoid, Bool is a two-variant coproduct. Symbol and Unit are bodyless and may be declared-abstract rather than competing realizations, so their bypass may be harmless. Hash is the one that costs a GUARANTEE rather than merely a representation, and it belongs with the same-shape three rather than apart from them: the row targets v1_rt::Hash, which is `pub type Hash = String` in the seed, against a v2 declaration of Fnv1a64Structural -- a single-field record whose digest field is `String where lower_hex_16`. std.content_hash content_hash_family_constructor_note states the public forgeable record constructors are DELETED and that the where-refinement IS the construction wall, so realizing that type as a bare String alias renders away the carrier the wall is attached to. A name-keyed spelling row can therefore silently drop a §4b construction rung. Established from declarations at both ends (vivid-wren-870, re-read here); NO live site is claimed, because no closure reaching a v2-declared Hash through lookup_checkpoint has been emitted by either of us. NEXT-RUNG TRIGGER -- AND THE OBVIOUS SHAPE IS THE WRONG ONE. An earlier revision of this note named `the checkpoint rows gain a declaring-module column`. vivid-wren-870 refused that shape with an argument this note adopts: a TypeCheckpoint row is cited to the Rust reference and states how RUST spells a type, whereas which dag module declares Int is a gunbc-corpus fact, so a declaring-module column puts corpus data inside an extdeps upstream authority -- a layer inversion, and the same class as a row being asked a question its cited authority cannot answer. The expected terminal shape is TWO authorities rather than one wider one: extdeps keeps Rust type -> spelling, a corpus-side binding says this dag declaration realizes as that Rust type, and lookup_checkpoint keys on the second. That also lets the seven differ from each other, which one column keyed on a single module cannot express. Recorded as a proposal from the rows owner, not as a decision, and unbuilt at the time of writing. When it lands the residue assertions flip to None and the flip is the dissolution signal, not a regression. LANDED FOR HASH (this PR, T7): the second authority is v1.compiler.coercion structural_declaration_modules_for, a corpus-side row roster keyed on the dag_name and enumerating the modules whose declaration of that name is structural rather than native -- \"Hash\" => [\"src/v2/std/node.dag\"] is its one row. lookup_checkpoint (v1.compiler.coercion) now consults it before the bare-name table: when decl_file_declares_structurally holds, lookup_checkpoint refuses (none) rather than answering from the table, and every consumer that already carried a correct identity-arm fallback -- coerce_primitive_type, is_copy, literal_suffix, and the direct callers of lookup_checkpoint itself -- inherits the refusal once decl_file is threaded to the call, which it now is at every production call site across v1.compiler.emit_rust and v1.compiler.emit. table_present_hash_refuses_under_structural_declaration in the witness below is the flip this note predicted; it is no longer residue. LANDED FOR STRING (session merry-lark-67, per smart-ram-730's dispatch): structural_declaration_modules_for gained a second row, \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"] -- both declare `type String = FreeMonoid`, the structural free-monoid-over-Char carrier, never a host string, so a reference resolving to either module now refuses the bare-name table's `String`/`.to_string()` spelling instead of silently rendering it. residue_table_present_string_bypasses_identity in the legacy oracle (src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag) is retired for the same reason table_present_hash_refuses_under_structural_declaration closed for Hash, and is replaced there by table_present_string_refuses_under_structural_declaration_text / _string_type rather than repaired back to a passing bypass -- the flip is the dissolution signal, not a regression. LANDED FOR BOOL (session merry-lark-67, corpus-wide histogram from smart-ram-730; corrected same session, commit 127ad848070, per review 54257): structural_declaration_modules_for gained a third row, \"Bool\" => [\"src/v2/std/logic.dag\"] -- the initial enrollment mirrored String's two-row shape onto Bool and also listed dag/std/types.dag, but that module is the ordinary corpus-wide native Bool prelude (imported by 300+ dag/test/claim modules with no bit/width/encoding modeling riding on it), directly analogous to dag/std/integer.dag for Int, which sits in the POSITIVE numeric_realization_declaring_modules roster, never the negative structural one. Only src/v2/std/logic.dag's Bool is genuinely structural, carrying BoolWidthFact/BoolEncodingFact/BooleanAlgebra modeling over the two-variant coproduct; a reference resolving to it refuses the bare-name table's `bool`/`false` spelling instead of silently rendering it, while a reference resolving to dag/std/types.dag renders natively as designed. The over-broad row caused required-floor to refuse native bool rendering for 5 unrelated fixtures (e0308_mechanical_trio_test, optional_carrier_signature_test) and caused required-regen to see drift across the self-hosted std_*.rs mirrors; both are the fabricated-plausible-ceiling failure this note elsewhere criticizes, disclosed and repaired here rather than left standing. Bool never had a residue row in the legacy oracle to flip; it lands directly as one CLOSED row, table_present_bool_refuses_under_structural_declaration_logic, alongside table_present_bool_renders_natively_for_the_corpus_prelude confirming dag/std/types.dag's native rendering. KNOWN GAP THIS ROW DOES NOT CLOSE, FOUND WHILE MEASURING IT: emit_typed_item's type-alias arm special-cases `item_text == \"String\"` UNCONDITIONALLY -- rust_string_grounded_type_alias_decl_line emits `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file, never consulting rust_scalar_checkpoint_render_base or this roster at all. So the module that declares `type String = FreeMonoid` keeps emitting itself as a host-String alias even after this row makes every REFERENCE to it refuse the bare-name table; the declaration and its own references can now disagree in the SAME emitted file. This is not fixed here -- it is a separate emit_rust mechanism, unconditional on decl_file, that this row's PR does not touch -- and is recorded as the next-rung trigger for String's declaration-site emission specifically, distinct from the reference-site gate this note otherwise describes. REACHABILITY CORRECTION (royal-dove-436, adhoc-c735d227-60b, 2026-08-21, measured on the 03_ingest closure): TWO CLAIMS ABOVE ARE FALSE FOR STRING AND ARE CORRECTED HERE RATHER THAN SOFTENED -- the LANDED FOR STRING clause's 'a reference resolving to either module now refuses the bare-name table's String/.to_string() spelling instead of silently rendering it', and the KNOWN GAP clause's 'even after this row makes every REFERENCE to it refuse the bare-name table'. The row does not make every reference refuse, because a String-spelled reference in TYPE position never reaches lookup_checkpoint at all. SIX type renderers in this module -- render_rust_type, render_rust_type_without_applied_binding, render_rust_applied_type, render_rust_type_with_applied_binding, render_rust_decl_type and render_rust_fn_sig_type -- each RETURN ON THEIR FIRST LINE (verified: the call is the statement immediately following each fn's own declaration) via is_host_text_carrier_type, rendering the literal \"String\" unconditionally on decl_file, ahead of every checkpoint or roster consultation; and is_host_text_carrier_type accepts the spelling String outright, so no path through those six can reach type_realization_decision's Unrealized-via-structural-gate arm for it. THE ROW IS THEREFORE PRESENT, CORRECT, AND UNREACHABLE FOR THE TEXT CARRIER IN TYPE POSITION -- an unreachable wall rather than a missing one, which is DESIGN section 6's coverage-by-illusion and a section 4b rung this note previously reported as held. This is a REACHABILITY claim about String's reference-site gate; it does NOT touch the Hash clause above, whose 'NO live site is claimed' is scoped to a v2-declared Hash reaching lookup_checkpoint and is unaffected, and it is a DIFFERENT mechanism from the declaration-site alias line the KNOWN GAP clause otherwise describes. SUPPORTING EVIDENCE, cited as a population rather than as the basis of the claim: 34 live E0308 sites in the 03_ingest closure pair a String-declared field or parameter against a FreeMonoid-realized value, every one of them a type position that rendered the native spelling while the roster says the declaration is structural (docs/probes/t2_t3_realization_route_2026-08-21.md, per-site TSV beside it). ESTABLISHED HOW, because the distinction decides what would falsify this: the reachability claim is decidable from the five renderers' control flow, which is how it was established -- NOT by a discriminating execution, and it says nothing about a sixth renderer that may handle some type position without that preamble. NEXT-RUNG TRIGGER: the short-circuit family is deleted so the existing authority becomes reachable, per docs/plans/carrier-realization-arbiter-repair-design.md, which also counts the decl_file == \"\" residue this module contributes (four sites) that the DECLARED RESIDUE note in v1.compiler.coercion says is uncounted. That design leaves the structural-vs-native direction to its owner and proposes an emit-only blast-radius measurement, not a merge, as the next step -- deliberately, because the over-broad Bool row recorded above is what picking a direction without that measurement already cost once. Int, Float, Symbol remain open -- they have no row in structural_declaration_modules_for -- and are the population the next instance of this class (a name question answered by authored spelling instead of declaration identity) inherits, per the class-level framing this ceiling was folded into. The roster is deliberately a single generic, identity-keyed mechanism with one row rather than a Hash-specific special case, so a future row for Int or String is an addition to this same authority, not a new mechanism. MEASURED CONSEQUENCE AT ARTIFACT GRAIN, added after this note first landed: the bypass is observable in the emitted FILE SET, not only in the emitter's answer. In a two-arm emission of one v2-only closure the file v2_std_integer.rs is present before the cut and ABSENT after it. That module declares exactly one item, the v2-declared structural Int, and its only type-position consumer was a single generated re-export line in std_algebra.rs; with Int reaching the bare-name checkpoint the re-export is no longer generated, nothing references the module, and it is not emitted. Every other hunk in that file is an offset shift from the deleted line -- the Int string literals are unchanged and the i64 count in the file is identical across arms, so nothing became native that was structural. AND THE DROP IS THE MINORITY CASE -- THE WRONG REALIZATION IS EMITTED, NOT AVOIDED. Across eleven emitted closures measured by smart-ibex-716 (corpus a6bceb6903, binaries a6bceb6903 and ad05a2f2d5), the module disappears in only 2; in the other 9 it SURVIVES with its content changed, from pub type Int = GroupCompletion> to pub type Int = i64. So the native realization of the v2-declared Peano-completion type is already present in the emitted artifact. What is absent is only a consumer: the same census found ZERO type-position uses of the v2 Int in any of the eleven -- every qualified occurrence sits on a use line, and the only bare occurrences surviving a use-line exclusion were four string literals inside prose, one of them a parser test fixture. Two false positives were found and discarded on the way to that zero, both by pulling the specimen rather than trusting the count. The residue is therefore NOT a dead re-export being dropped, which was this note's first reading and is corrected here; it is a wrong realization sitting inert with no diagnostic attached, so the day any declaration binds a bare Int in one of those closures it binds i64 silently. THE HAZARD TRIGGER IS THEREFORE A TYPE POSITION APPEARING, not the re-export returning. This is recorded because a module leaving OR silently changing an alias target is the kind of consequence a content-only diff of one closure reads as offset noise: the instruments that name it are a file-set diff and a cross-closure alias-target read, and neither was in this PR's original receipt." +data checkpoint_table_bypasses_identity_note: String = "CEILING, STATED BECAUSE THE CODE DELIVERS LESS THAN THE DELETION OF RustCorpusRepr SUGGESTS. lookup_checkpoint is keyed on the BARE dag_name and is consulted BEFORE the identity-keyed arm, so any name carrying a checkpoint row in extdeps/languages/rust/types.dag bypasses declaration keying entirely. Nat carries no row and therefore discriminates correctly -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag refuses. Names WITH a row do not. This is not a regression introduced here: the table was already bare-name keyed and the global corpus mode was hiding the question. It is the honest rung. The class is MECHANICALLY PREVENTABLE rather than structurally impossible, and its executing evidence is v1.tests.claim.checkpoint_identity_keying_witness_test, which asserts the CURRENT bypassing answers on purpose so the gap is counted instead of assumed closed. THAT CITATION WAS FALSE WHEN THIS NOTE FIRST LANDED AND IS REPAIRED RATHER THAN SOFTENED. It named the residue block generated by v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into a module declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate -- while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package consuming v1-compiler as an ordinary dependency, so cfg(test) is never set for it and the block is not compiled, let alone executed. Measured rather than reasoned: that step's binary enumerates 30 tests and none is this one, against a positive control confirming the enumeration is non-empty. So a ceiling disclosure cited evidence that had never run -- DESIGN section 4b(1) rung honesty violated in the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The assertions were re-authored as an enrolled .dag witness and now execute (seven rows PASS, including the discriminating row where two declarations share the spelling Nat and answer differently); the superseded generated-Rust block is deleted rather than left standing as a second, silent copy. POPULATION (census by vivid-wren-870, who owns the rows): SEVEN of the table's names are also declared under src/v2 -- Int, Float, Bool, Symbol, Unit, String, Hash; Bytes, Secret and Json are not. That is a LOWER BOUND obtained by grepping line-start `type ` declarations under src/v2; it does not find names introduced any other way, and it says NOTHING about how many sites bite in any real closure. Three of the seven are the same shape as Int in that the v2 declaration is a genuinely different STRUCTURE rather than a spelling coincidence -- Int is GroupCompletion, String is FreeMonoid, Bool is a two-variant coproduct. Symbol and Unit are bodyless and may be declared-abstract rather than competing realizations, so their bypass may be harmless. Hash is the one that costs a GUARANTEE rather than merely a representation, and it belongs with the same-shape three rather than apart from them: the row targets v1_rt::Hash, which is `pub type Hash = String` in the seed, against a v2 declaration of Fnv1a64Structural -- a single-field record whose digest field is `String where lower_hex_16`. std.content_hash content_hash_family_constructor_note states the public forgeable record constructors are DELETED and that the where-refinement IS the construction wall, so realizing that type as a bare String alias renders away the carrier the wall is attached to. A name-keyed spelling row can therefore silently drop a §4b construction rung. Established from declarations at both ends (vivid-wren-870, re-read here); NO live site is claimed, because no closure reaching a v2-declared Hash through lookup_checkpoint has been emitted by either of us. NEXT-RUNG TRIGGER -- AND THE OBVIOUS SHAPE IS THE WRONG ONE. An earlier revision of this note named `the checkpoint rows gain a declaring-module column`. vivid-wren-870 refused that shape with an argument this note adopts: a TypeCheckpoint row is cited to the Rust reference and states how RUST spells a type, whereas which dag module declares Int is a gunbc-corpus fact, so a declaring-module column puts corpus data inside an extdeps upstream authority -- a layer inversion, and the same class as a row being asked a question its cited authority cannot answer. The expected terminal shape is TWO authorities rather than one wider one: extdeps keeps Rust type -> spelling, a corpus-side binding says this dag declaration realizes as that Rust type, and lookup_checkpoint keys on the second. That also lets the seven differ from each other, which one column keyed on a single module cannot express. Recorded as a proposal from the rows owner, not as a decision, and unbuilt at the time of writing. When it lands the residue assertions flip to None and the flip is the dissolution signal, not a regression. LANDED FOR HASH (this PR, T7): the second authority is v1.compiler.coercion structural_declaration_modules_for, a corpus-side row roster keyed on the dag_name and enumerating the modules whose declaration of that name is structural rather than native -- \"Hash\" => [\"src/v2/std/node.dag\"] is its one row. lookup_checkpoint (v1.compiler.coercion) now consults it before the bare-name table: when decl_file_declares_structurally holds, lookup_checkpoint refuses (none) rather than answering from the table, and every consumer that already carried a correct identity-arm fallback -- coerce_primitive_type, is_copy, literal_suffix, and the direct callers of lookup_checkpoint itself -- inherits the refusal once decl_file is threaded to the call, which it now is at every production call site across v1.compiler.emit_rust and v1.compiler.emit. table_present_hash_refuses_under_structural_declaration in the witness below is the flip this note predicted; it is no longer residue. LANDED FOR STRING (session merry-lark-67, per smart-ram-730's dispatch): structural_declaration_modules_for gained a second row, \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"] -- both declare `type String = FreeMonoid`, the structural free-monoid-over-Char carrier, never a host string, so a reference resolving to either module now refuses the bare-name table's `String`/`.to_string()` spelling instead of silently rendering it. residue_table_present_string_bypasses_identity in the legacy oracle (src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag) is retired for the same reason table_present_hash_refuses_under_structural_declaration closed for Hash, and is replaced there by table_present_string_refuses_under_structural_declaration_text / _string_type rather than repaired back to a passing bypass -- the flip is the dissolution signal, not a regression. LANDED FOR BOOL (session merry-lark-67, corpus-wide histogram from smart-ram-730; corrected same session, commit 127ad848070, per review 54257): structural_declaration_modules_for gained a third row, \"Bool\" => [\"src/v2/std/logic.dag\"] -- the initial enrollment mirrored String's two-row shape onto Bool and also listed dag/std/types.dag, but that module is the ordinary corpus-wide native Bool prelude (imported by 300+ dag/test/claim modules with no bit/width/encoding modeling riding on it), directly analogous to dag/std/integer.dag for Int, which sits in the POSITIVE numeric_realization_declaring_modules roster, never the negative structural one. Only src/v2/std/logic.dag's Bool is genuinely structural, carrying BoolWidthFact/BoolEncodingFact/BooleanAlgebra modeling over the two-variant coproduct; a reference resolving to it refuses the bare-name table's `bool`/`false` spelling instead of silently rendering it, while a reference resolving to dag/std/types.dag renders natively as designed. The over-broad row caused required-floor to refuse native bool rendering for 5 unrelated fixtures (e0308_mechanical_trio_test, optional_carrier_signature_test) and caused required-regen to see drift across the self-hosted std_*.rs mirrors; both are the fabricated-plausible-ceiling failure this note elsewhere criticizes, disclosed and repaired here rather than left standing. Bool never had a residue row in the legacy oracle to flip; it lands directly as one CLOSED row, table_present_bool_refuses_under_structural_declaration_logic, alongside table_present_bool_renders_natively_for_the_corpus_prelude confirming dag/std/types.dag's native rendering. KNOWN GAP THIS ROW DOES NOT CLOSE, FOUND WHILE MEASURING IT: emit_typed_item's type-alias arm special-cases `item_text == \"String\"` UNCONDITIONALLY -- rust_string_grounded_type_alias_decl_line emits `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file, never consulting rust_scalar_checkpoint_render_base or this roster at all. So the module that declares `type String = FreeMonoid` keeps emitting itself as a host-String alias even after this row makes every REFERENCE to it refuse the bare-name table; the declaration and its own references can now disagree in the SAME emitted file. THAT KNOWN GAP IS NOW CLOSED, AND THE ROOT WAS NOT WHERE THIS NOTE PUT IT. The gap as recorded: emit_typed_item's type-alias arm special-cased `item_text == \"String\"` UNCONDITIONALLY, emitting `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file and never consulting the identity-keyed authority every REFERENCE already routed through, so one emitted file could disagree with itself. This note framed that as a second bare-name bypass to be deleted. IT WAS NOT. The arm was COMPENSATING, and deleting it alone would have emitted `pub type String = String;` -- self-referential, because the checkpoint's target_type for String is the bare spelling `String` and the declaration site uses target_type as the alias's right-hand side. The real defect was that ONE FIELD CARRIED TWO SPELLING ROLES (the word arity is avoided here on purpose -- in this module it already means type-parameter count, see AliasDeclArityVerdict and rust_checkpoint_scalar_declared_arity_guard_note): one field answering two questions -- what a REFERENCE renders (bare `String`, correct and idiomatic) and what a DECLARATION is GROUNDED IN (`std::string::String`, the spelling no alias can shadow). Whichever spelling one field carried, one consumer was wrong, and the arm was the visible cost of making it try. std.coercion TypeCheckpoint now carries both spellings as separate fields; rust_scalar_checkpoint_reference_base and rust_scalar_checkpoint_grounding_base are two named entry points over one shared identity-keyed body, so every PRODUCTION caller states which question it asks by visibly naming it rather than by passing an argument. That is mechanically preventable, NOT structurally impossible: the shared body stays reachable and carries the discriminator, .dag has no function-privacy concept to hide it behind (the emitted emitter carries 665 pub fn and zero non-pub), and the next-rung trigger is a module-private function boundary in the language. The standing evidence for the narrower claim is that the shared body's only direct callers are the two wrappers; the three reference callers read the reference spelling, the single declaration-RHS caller reads grounding, and the arm is DELETED rather than guarded. WHAT THIS STILL DOES NOT CLOSE, stated so the ceiling is not read as retired: lookup_checkpoint's FIRST arm answers straight from the bare-name table when decl_file is the empty string, consulting no roster at all, so every site reaching emission with UNKNOWN declaration identity still realizes from the table exactly as this note describes. That bypass is live, its population is UNCOUNTED, and no estimate is offered here. It is a separate defect from the two-role split -- the split governs what a row can SAY once identity is known; the bypass governs whether identity is consulted at all -- and it is filed as its own row rather than folded into this one. HOW THIS CLOSURE AND THE REACHABILITY CORRECTION BELOW RELATE, because each narrows the other and reading either alone overstates it: the two-role split is what makes the DECLARATION site able to consult the identity-keyed authority at all, and royal-dove-436's finding is that the REFERENCE site for a String-spelled type never reaches lookup_checkpoint in the first place. So for String specifically the split repairs a position that was answering wrongly, while the position this note elsewhere calls gated is not yet reached -- the declaration half is closed and the reference half is unreachable, which is one authority with two different reasons its consumers do not see it, not one gap. Neither finding weakens the other and neither is the whole story for String; the split is stated here as closing the arm it deletes, never as making every String position identity-keyed. REACHABILITY CORRECTION (royal-dove-436, adhoc-c735d227-60b, 2026-08-21, measured on the 03_ingest closure): TWO CLAIMS ABOVE ARE FALSE FOR STRING AND ARE CORRECTED HERE RATHER THAN SOFTENED -- the LANDED FOR STRING clause's 'a reference resolving to either module now refuses the bare-name table's String/.to_string() spelling instead of silently rendering it', and the KNOWN GAP clause's 'even after this row makes every REFERENCE to it refuse the bare-name table'. The row does not make every reference refuse, because a String-spelled reference in TYPE position never reaches lookup_checkpoint at all. SIX type renderers in this module -- render_rust_type, render_rust_type_without_applied_binding, render_rust_applied_type, render_rust_type_with_applied_binding, render_rust_decl_type and render_rust_fn_sig_type -- each RETURN ON THEIR FIRST LINE (verified: the call is the statement immediately following each fn's own declaration) via is_host_text_carrier_type, rendering the literal \"String\" unconditionally on decl_file, ahead of every checkpoint or roster consultation; and is_host_text_carrier_type accepts the spelling String outright, so no path through those six can reach type_realization_decision's Unrealized-via-structural-gate arm for it. THE ROW IS THEREFORE PRESENT, CORRECT, AND UNREACHABLE FOR THE TEXT CARRIER IN TYPE POSITION -- an unreachable wall rather than a missing one, which is DESIGN section 6's coverage-by-illusion and a section 4b rung this note previously reported as held. This is a REACHABILITY claim about String's reference-site gate; it does NOT touch the Hash clause above, whose 'NO live site is claimed' is scoped to a v2-declared Hash reaching lookup_checkpoint and is unaffected, and it is a DIFFERENT mechanism from the declaration-site alias line the KNOWN GAP clause otherwise describes. SUPPORTING EVIDENCE, cited as a population rather than as the basis of the claim: 34 live E0308 sites in the 03_ingest closure pair a String-declared field or parameter against a FreeMonoid-realized value, every one of them a type position that rendered the native spelling while the roster says the declaration is structural (docs/probes/t2_t3_realization_route_2026-08-21.md, per-site TSV beside it). ESTABLISHED HOW, because the distinction decides what would falsify this: the reachability claim is decidable from the five renderers' control flow, which is how it was established -- NOT by a discriminating execution, and it says nothing about a sixth renderer that may handle some type position without that preamble. NEXT-RUNG TRIGGER: the short-circuit family is deleted so the existing authority becomes reachable, per docs/plans/carrier-realization-arbiter-repair-design.md, which also counts the decl_file == \"\" residue this module contributes (four sites) that the DECLARED RESIDUE note in v1.compiler.coercion says is uncounted. That design leaves the structural-vs-native direction to its owner and proposes an emit-only blast-radius measurement, not a merge, as the next step -- deliberately, because the over-broad Bool row recorded above is what picking a direction without that measurement already cost once. Int, Float, Symbol remain open -- they have no row in structural_declaration_modules_for -- and are the population the next instance of this class (a name question answered by authored spelling instead of declaration identity) inherits, per the class-level framing this ceiling was folded into. The roster is deliberately a single generic, identity-keyed mechanism with one row rather than a Hash-specific special case, so a future row for Int or String is an addition to this same authority, not a new mechanism. MEASURED CONSEQUENCE AT ARTIFACT GRAIN, added after this note first landed: the bypass is observable in the emitted FILE SET, not only in the emitter's answer. In a two-arm emission of one v2-only closure the file v2_std_integer.rs is present before the cut and ABSENT after it. That module declares exactly one item, the v2-declared structural Int, and its only type-position consumer was a single generated re-export line in std_algebra.rs; with Int reaching the bare-name checkpoint the re-export is no longer generated, nothing references the module, and it is not emitted. Every other hunk in that file is an offset shift from the deleted line -- the Int string literals are unchanged and the i64 count in the file is identical across arms, so nothing became native that was structural. AND THE DROP IS THE MINORITY CASE -- THE WRONG REALIZATION IS EMITTED, NOT AVOIDED. Across eleven emitted closures measured by smart-ibex-716 (corpus a6bceb6903, binaries a6bceb6903 and ad05a2f2d5), the module disappears in only 2; in the other 9 it SURVIVES with its content changed, from pub type Int = GroupCompletion> to pub type Int = i64. So the native realization of the v2-declared Peano-completion type is already present in the emitted artifact. What is absent is only a consumer: the same census found ZERO type-position uses of the v2 Int in any of the eleven -- every qualified occurrence sits on a use line, and the only bare occurrences surviving a use-line exclusion were four string literals inside prose, one of them a parser test fixture. Two false positives were found and discarded on the way to that zero, both by pulling the specimen rather than trusting the count. The residue is therefore NOT a dead re-export being dropped, which was this note's first reading and is corrected here; it is a wrong realization sitting inert with no diagnostic attached, so the day any declaration binds a bare Int in one of those closures it binds i64 silently. THE HAZARD TRIGGER IS THEREFORE A TYPE POSITION APPEARING, not the re-export returning. This is recorded because a module leaving OR silently changing an alias target is the kind of consequence a content-only diff of one closure reads as offset noise: the instruments that name it are a file-set diff and a cross-closure alias-target read, and neither was in this PR's original receipt." -fn rust_scalar_checkpoint_render_base(dag_name: String, decl_file: String) -> String? { +// TWO ENTRY POINTS OVER ONE BODY, because a checkpoint answers two questions and the caller must +// state which one it is asking. The shared body below decides WHETHER a checkpoint governs this +// declaration -- identity-keyed, one authority, unchanged. What the two surfaces select is WHICH +// SPELLING the answering row hands back. +// +// WHY NOT ONE FUNCTION WITH A POSITION ARGUMENT: an argument is a discriminator the caller can get +// wrong, and nothing stops the next caller passing the one that compiles rather than the one that is +// true. Naming the question makes selecting the wrong spelling require visibly calling the wrong +// function. Same reason the row carries two fields rather than one field and a rule (std.coercion +// TypeCheckpoint). +// +// THE RUNG IS MECHANICALLY PREVENTABLE, NOT STRUCTURALLY IMPOSSIBLE, AND AN EARLIER REVISION OF +// THIS ANNOTATION CLAIMED OTHERWISE. It said the discrimination lives in the structure rather than +// in author care, and that a new caller must say which position it is in before it can compile at +// all. Neither holds. rust_scalar_checkpoint_spelling below is reachable and carries the grounding +// Bool -- exactly the discriminator these two surfaces exist to remove -- so a caller CAN still +// select the wrong spelling by calling the shared body directly, and nothing refuses it. What the +// two entry points buy is that every PRODUCTION caller goes through a question-named surface, which +// is a fact about the current call graph rather than a property of the API. +// +// THE EVIDENCE FOR THE NARROWER CLAIM, so it is checkable rather than merely modest: the only +// direct callers of rust_scalar_checkpoint_spelling are these two wrappers, in this authority and +// in the emitted seed alike. A third direct caller appearing is the regression this annotation +// exists to make visible. +// +// WHY IT IS A CEILING RATHER THAN A DEFECT LEFT UNFIXED: .dag has no function-privacy concept, so +// the shared body cannot be made unreachable however it is written -- measured on the emitted +// emitter, which carries 665 `pub fn` and zero non-pub functions, against a parser with no privacy +// keyword to reach for. NEXT-RUNG TRIGGER: a module-private function boundary in the language. When +// it exists this body becomes private, the wrong selection becomes unrepresentable outside the +// module, and the class climbs without any change to the two surfaces. +fn rust_scalar_checkpoint_reference_base(dag_name: String, decl_file: String) -> String? { + rust_scalar_checkpoint_spelling(dag_name: dag_name, decl_file: decl_file, grounding: false) +} + +// DECLARATION right-hand side. The alias being defined shadows its own name, so this position needs +// the spelling no alias can reach -- see std.coercion TypeCheckpoint for why the bare one is wrong +// here rather than merely unidiomatic. +fn rust_scalar_checkpoint_grounding_base(dag_name: String, decl_file: String) -> String? { + rust_scalar_checkpoint_spelling(dag_name: dag_name, decl_file: decl_file, grounding: true) +} + +fn rust_scalar_checkpoint_spelling(dag_name: String, decl_file: String, grounding: Bool) -> String? { match lookup_checkpoint(target: Rust, dag_name: dag_name, decl_file: decl_file) { - Present { value: cp } => Present { value: cp.target_type } + Present { value: cp } => Present { value: if grounding { cp.grounding_type } else { cp.target_type } } Absent => match rust_seed_host_numeric_alias(name: dag_name, decl_file: decl_file) { Present { value: host } => Present { value: host } @@ -479,7 +517,7 @@ data rust_checkpoint_scalar_phantom_params_note: String = "Construction wall for // `Rc * i64`, an operator refusal that neither position produces alone. // // Scope is the same as the parameter-side guard and deliberately no wider: only the numeric -// authority suppresses the wrap. rust_scalar_checkpoint_render_base also answers for +// authority suppresses the wrap. rust_scalar_checkpoint_reference_base also answers for // lookup_checkpoint rows that are NOT machine scalars (String is the live one), and those may // legitimately be shared, so widening this to every checkpoint row is a separate cut. fn rust_render_checkpoint_scalar_bare(n: Node, source_indices: Map, shared_types: Set) -> String? { @@ -490,7 +528,7 @@ fn rust_render_checkpoint_scalar_bare(n: Node, source_indices: Map Present { value: numeric } Absent => - match rust_scalar_checkpoint_render_base(dag_name: leaf, decl_file: type_reference_decl_file(n: n)) { + match rust_scalar_checkpoint_reference_base(dag_name: leaf, decl_file: type_reference_decl_file(n: n)) { Present { value: scalar } => if set_contains(shared_types, leaf) && !rust_type_is_rc_wrapped(type_name: scalar) { Present { value: wrap_shared_type(target: Rust, inner: scalar) } @@ -875,7 +913,7 @@ fn render_rust_applied_type(n: Node, generic_param_names: List, shared_t } } else { - match rust_scalar_checkpoint_render_base(dag_name: base_name, decl_file: type_reference_decl_file(n: n)) { + match rust_scalar_checkpoint_reference_base(dag_name: base_name, decl_file: type_reference_decl_file(n: n)) { Present { value: scalar } => scalar Absent => match closed_alias_peel_verdict(env: env, n: n) { @@ -1290,7 +1328,7 @@ fn render_rust_alias_rhs_type(n: Node, generic_param_names: List, shared } } else if n.connective == NoConnective && n.children |> count > 0 { let leaf = qualified_last_segment(name: name) - let numeric_host_alias = match rust_scalar_checkpoint_render_base(dag_name: leaf, decl_file: type_reference_decl_file(n: n)) { + let numeric_host_alias = match rust_scalar_checkpoint_reference_base(dag_name: leaf, decl_file: type_reference_decl_file(n: n)) { Present { value: scalar } => Present { value: scalar } Absent => rust_seed_host_numeric_alias(name: leaf, decl_file: type_reference_decl_file(n: n)) } @@ -5041,16 +5079,14 @@ fn emit_typed_item(item: Node, module_name: String, registry: Map count) == 0 && rust_opaque_kernel_alias_type_eligible(name: item_text) { + if (item.params |> count) == 0 && rust_opaque_kernel_alias_type_eligible(name: item_text) { rust_opaque_kernel_alias_type_decl(name: item_text) } else if (item.params |> count) == 0 && rust_nominal_identity_carrier_type_eligible(type_name: item_text) { rust_nominal_identity_carrier_def(name: item_text) } else if is_zero_param_self_referential_opaque_decl(item: item, source_indices: env.source_indices) { emit_zero_param_phantom_opaque_struct(item: item, map_key_required: set_contains(emit_info.map_key_required_type_names, item_text), source_indices: env.source_indices) } else { - match rust_scalar_checkpoint_render_base(dag_name: item_text, decl_file: decl_identity_file(item: item)) { + match rust_scalar_checkpoint_grounding_base(dag_name: item_text, decl_file: decl_identity_file(item: item)) { Present { value: host } => concat(rust_visibility_prefix(), rust_items().type_alias_keyword, " ", item_text, " = ", host, ";") Absent => diff --git a/src/v1/coercion.dag b/src/v1/coercion.dag index 33b6fc6c3da..82ebfc23428 100644 --- a/src/v1/coercion.dag +++ b/src/v1/coercion.dag @@ -232,7 +232,7 @@ fn type_realization_decision( Absent => let native = if (target == Rust) { rust_seed_host_numeric_alias(name: dag_name, decl_file: decl_file) } else { none } match native { - Present { value: host } => Realized { checkpoint: TypeCheckpoint { dag_name: dag_name, target_type: host, default_expr: none, is_copy: none, literal_suffix: none } } + Present { value: host } => Realized { checkpoint: TypeCheckpoint { dag_name: dag_name, target_type: host, grounding_type: host, default_expr: none, is_copy: none, literal_suffix: none } } Absent => Unrealized } } diff --git a/src/v1/stage0/src/extdeps_languages_dag_types.rs b/src/v1/stage0/src/extdeps_languages_dag_types.rs index 7b095a1bc84..043777cafa9 100644 --- a/src/v1/stage0/src/extdeps_languages_dag_types.rs +++ b/src/v1/stage0/src/extdeps_languages_dag_types.rs @@ -29,7 +29,7 @@ pub fn extdeps_external_authority_anchor() -> Rc { pub fn dag_type_checkpoints() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "Int", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "Float", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "Bool", "default_expr": "false", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "String", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}])) + serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "Int", "grounding_type": "Int", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "Float", "grounding_type": "Float", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "Bool", "grounding_type": "Bool", "default_expr": "false", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "String", "grounding_type": "String", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/extdeps_languages_go_types.rs b/src/v1/stage0/src/extdeps_languages_go_types.rs index 0f2581c526f..bf1e28f3762 100644 --- a/src/v1/stage0/src/extdeps_languages_go_types.rs +++ b/src/v1/stage0/src/extdeps_languages_go_types.rs @@ -29,7 +29,7 @@ pub fn extdeps_external_authority_anchor() -> Rc { pub fn go_type_checkpoints() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "int64", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "float64", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "default_expr": "false", "is_copy": null, "literal_suffix": null}, {"dag_name": "Unit", "target_type": "struct{}", "default_expr": "struct{}{}", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "string", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bytes", "target_type": "[]byte", "default_expr": "nil", "is_copy": null, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "string", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Json", "target_type": "interface{}", "default_expr": "nil", "is_copy": null, "literal_suffix": null}])) + serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "int64", "grounding_type": "int64", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "float64", "grounding_type": "float64", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "grounding_type": "bool", "default_expr": "false", "is_copy": null, "literal_suffix": null}, {"dag_name": "Unit", "target_type": "struct{}", "grounding_type": "struct{}", "default_expr": "struct{}{}", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "string", "grounding_type": "string", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bytes", "target_type": "[]byte", "grounding_type": "[]byte", "default_expr": "nil", "is_copy": null, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "string", "grounding_type": "string", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Json", "target_type": "interface{}", "grounding_type": "interface{}", "default_expr": "nil", "is_copy": null, "literal_suffix": null}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/extdeps_languages_python_types.rs b/src/v1/stage0/src/extdeps_languages_python_types.rs index 25132e23d71..68f032bde82 100644 --- a/src/v1/stage0/src/extdeps_languages_python_types.rs +++ b/src/v1/stage0/src/extdeps_languages_python_types.rs @@ -30,7 +30,7 @@ pub fn extdeps_external_authority_anchor() -> Rc { pub fn python_type_checkpoints() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "int", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "float", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "default_expr": "False", "is_copy": null, "literal_suffix": null}, {"dag_name": "Unit", "target_type": "None", "default_expr": "None", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "str", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bytes", "target_type": "bytes", "default_expr": "b\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "str", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Json", "target_type": "dict", "default_expr": "{}", "is_copy": null, "literal_suffix": null}])) + serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "int", "grounding_type": "int", "default_expr": "0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Float", "target_type": "float", "grounding_type": "float", "default_expr": "0.0", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "grounding_type": "bool", "default_expr": "False", "is_copy": null, "literal_suffix": null}, {"dag_name": "Unit", "target_type": "None", "grounding_type": "None", "default_expr": "None", "is_copy": null, "literal_suffix": null}, {"dag_name": "String", "target_type": "str", "grounding_type": "str", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Bytes", "target_type": "bytes", "grounding_type": "bytes", "default_expr": "b\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "str", "grounding_type": "str", "default_expr": "\"\"", "is_copy": null, "literal_suffix": null}, {"dag_name": "Json", "target_type": "dict", "grounding_type": "dict", "default_expr": "{}", "is_copy": null, "literal_suffix": null}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/extdeps_languages_rust_types.rs b/src/v1/stage0/src/extdeps_languages_rust_types.rs index 9818bffd16d..d6e173a741f 100644 --- a/src/v1/stage0/src/extdeps_languages_rust_types.rs +++ b/src/v1/stage0/src/extdeps_languages_rust_types.rs @@ -34,7 +34,7 @@ pub fn extdeps_external_authority_anchor() -> Rc { pub fn rust_type_checkpoints() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "i64", "default_expr": "0", "is_copy": true, "literal_suffix": null}, {"dag_name": "Float", "target_type": "f64", "default_expr": "0.0", "is_copy": true, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "default_expr": "false", "is_copy": true, "literal_suffix": null}, {"dag_name": "Symbol", "target_type": "String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Unit", "target_type": "()", "default_expr": "()", "is_copy": true, "literal_suffix": null}, {"dag_name": "String", "target_type": "String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Bytes", "target_type": "Vec", "default_expr": "Vec::new()", "is_copy": false, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Json", "target_type": "serde_json::Value", "default_expr": "serde_json::Value::Null", "is_copy": false, "literal_suffix": null}])) + serde_json::from_value(serde_json::json!([{"dag_name": "Int", "target_type": "i64", "grounding_type": "i64", "default_expr": "0", "is_copy": true, "literal_suffix": null}, {"dag_name": "Float", "target_type": "f64", "grounding_type": "f64", "default_expr": "0.0", "is_copy": true, "literal_suffix": null}, {"dag_name": "Bool", "target_type": "bool", "grounding_type": "bool", "default_expr": "false", "is_copy": true, "literal_suffix": null}, {"dag_name": "Symbol", "target_type": "String", "grounding_type": "String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Unit", "target_type": "()", "grounding_type": "()", "default_expr": "()", "is_copy": true, "literal_suffix": null}, {"dag_name": "String", "target_type": "String", "grounding_type": "std::string::String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Bytes", "target_type": "Vec", "grounding_type": "Vec", "default_expr": "Vec::new()", "is_copy": false, "literal_suffix": null}, {"dag_name": "Secret", "target_type": "String", "grounding_type": "String", "default_expr": "String::new()", "is_copy": false, "literal_suffix": ".to_string()"}, {"dag_name": "Json", "target_type": "serde_json::Value", "grounding_type": "serde_json::Value", "default_expr": "serde_json::Value::Null", "is_copy": false, "literal_suffix": null}])) .expect("valid data definition") }; } @@ -53,7 +53,7 @@ pub fn rust_checkpoint_hash_row_retired_note() -> String { pub fn rust_checkpoint_scalar_arity_note() -> String { thread_local! { static CACHED: String = { - "A TypeCheckpoint row states one thing: how a target SPELLS a dag type whose Rust arity is zero. It cannot express arity, so membership of this table IS the emitter's arity-0 claim — v1.compiler.05_emit_rust rust_scalar_checkpoint_render_base reads it, and rust_render_checkpoint_scalar_bare strips every type argument from any leaf it matches (the E0109 wall, rust_checkpoint_scalar_phantom_params_note). Witness/witness rows were removed here 2026-08-16: Witness is the generic enum v2.std.witness.Witness (src/v2/std/witness.dag), arity 1 by its single authority std.types container_type_arity, so the rows made the emitter drop the argument of every Witness in type position and emit `Rc` — rustc E0107 'missing generics for enum Witness', 4 sites in the 06_translate closure alone (docs/probes/root_d_generic_arity_2026-08-16.md). Nothing else was lost with them: coerce_primitive_type renders the bare leaf name 'Witness' through qualified_last_segment either way, and is_copy's Absent arm and Present{false} arm are the same decision at every consumer. A generic type may not be added to this table; its spelling is not the missing fact, its arity is.".to_string() + "A TypeCheckpoint row states one thing: how a target SPELLS a dag type whose Rust arity is zero. It cannot express arity, so membership of this table IS the emitter's arity-0 claim — v1.compiler.05_emit_rust rust_scalar_checkpoint_reference_base reads it, and rust_render_checkpoint_scalar_bare strips every type argument from any leaf it matches (the E0109 wall, rust_checkpoint_scalar_phantom_params_note). Witness/witness rows were removed here 2026-08-16: Witness is the generic enum v2.std.witness.Witness (src/v2/std/witness.dag), arity 1 by its single authority std.types container_type_arity, so the rows made the emitter drop the argument of every Witness in type position and emit `Rc` — rustc E0107 'missing generics for enum Witness', 4 sites in the 06_translate closure alone (docs/probes/root_d_generic_arity_2026-08-16.md). Nothing else was lost with them: coerce_primitive_type renders the bare leaf name 'Witness' through qualified_last_segment either way, and is_copy's Absent arm and Present{false} arm are the same decision at every consumer. A generic type may not be added to this table; its spelling is not the missing fact, its arity is.".to_string() }; } CACHED.with(|c: &String| c.clone()) diff --git a/src/v1/stage0/src/std_coercion.rs b/src/v1/stage0/src/std_coercion.rs index 363232b275a..1137d2263b7 100644 --- a/src/v1/stage0/src/std_coercion.rs +++ b/src/v1/stage0/src/std_coercion.rs @@ -13,6 +13,7 @@ use std::rc::Rc; pub struct TypeCheckpoint { pub dag_name: String, pub target_type: String, + pub grounding_type: String, pub default_expr: Option, pub is_copy: Option, pub literal_suffix: Option, diff --git a/src/v1/stage0/src/v1_compiler_coercion.rs b/src/v1/stage0/src/v1_compiler_coercion.rs index f4f390d0eaf..4846ae7b835 100644 --- a/src/v1/stage0/src/v1_compiler_coercion.rs +++ b/src/v1/stage0/src/v1_compiler_coercion.rs @@ -276,6 +276,7 @@ pub fn type_realization_decision( checkpoint: Rc::new(TypeCheckpoint { dag_name: dag_name.clone(), target_type: host.clone(), + grounding_type: host.clone(), default_expr: None, is_copy: None, literal_suffix: None, diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index c5ca6d834b9..8e5ed30b61b 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -572,16 +572,6 @@ pub fn render_rust_text_carrier(shared_types: Rc>) -> String { ) } -pub fn rust_string_grounded_type_alias_decl_line() -> String { - v1_rt::concat( - v1_rt::concat( - rust_visibility_prefix(), - rust_items().type_alias_keyword.clone(), - ), - " String = std::string::String;".to_string(), - ) -} - pub fn emit_rust_host_to_dag_string_via_seam(host_expr: String) -> String { host_expr } @@ -754,15 +744,37 @@ pub fn numeric_realization_relocation_note() -> String { pub fn checkpoint_table_bypasses_identity_note() -> String { thread_local! { static CACHED: String = { - "CEILING, STATED BECAUSE THE CODE DELIVERS LESS THAN THE DELETION OF RustCorpusRepr SUGGESTS. lookup_checkpoint is keyed on the BARE dag_name and is consulted BEFORE the identity-keyed arm, so any name carrying a checkpoint row in extdeps/languages/rust/types.dag bypasses declaration keying entirely. Nat carries no row and therefore discriminates correctly -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag refuses. Names WITH a row do not. This is not a regression introduced here: the table was already bare-name keyed and the global corpus mode was hiding the question. It is the honest rung. The class is MECHANICALLY PREVENTABLE rather than structurally impossible, and its executing evidence is v1.tests.claim.checkpoint_identity_keying_witness_test, which asserts the CURRENT bypassing answers on purpose so the gap is counted instead of assumed closed. THAT CITATION WAS FALSE WHEN THIS NOTE FIRST LANDED AND IS REPAIRED RATHER THAN SOFTENED. It named the residue block generated by v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into a module declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate -- while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package consuming v1-compiler as an ordinary dependency, so cfg(test) is never set for it and the block is not compiled, let alone executed. Measured rather than reasoned: that step's binary enumerates 30 tests and none is this one, against a positive control confirming the enumeration is non-empty. So a ceiling disclosure cited evidence that had never run -- DESIGN section 4b(1) rung honesty violated in the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The assertions were re-authored as an enrolled .dag witness and now execute (seven rows PASS, including the discriminating row where two declarations share the spelling Nat and answer differently); the superseded generated-Rust block is deleted rather than left standing as a second, silent copy. POPULATION (census by vivid-wren-870, who owns the rows): SEVEN of the table's names are also declared under src/v2 -- Int, Float, Bool, Symbol, Unit, String, Hash; Bytes, Secret and Json are not. That is a LOWER BOUND obtained by grepping line-start `type ` declarations under src/v2; it does not find names introduced any other way, and it says NOTHING about how many sites bite in any real closure. Three of the seven are the same shape as Int in that the v2 declaration is a genuinely different STRUCTURE rather than a spelling coincidence -- Int is GroupCompletion, String is FreeMonoid, Bool is a two-variant coproduct. Symbol and Unit are bodyless and may be declared-abstract rather than competing realizations, so their bypass may be harmless. Hash is the one that costs a GUARANTEE rather than merely a representation, and it belongs with the same-shape three rather than apart from them: the row targets v1_rt::Hash, which is `pub type Hash = String` in the seed, against a v2 declaration of Fnv1a64Structural -- a single-field record whose digest field is `String where lower_hex_16`. std.content_hash content_hash_family_constructor_note states the public forgeable record constructors are DELETED and that the where-refinement IS the construction wall, so realizing that type as a bare String alias renders away the carrier the wall is attached to. A name-keyed spelling row can therefore silently drop a §4b construction rung. Established from declarations at both ends (vivid-wren-870, re-read here); NO live site is claimed, because no closure reaching a v2-declared Hash through lookup_checkpoint has been emitted by either of us. NEXT-RUNG TRIGGER -- AND THE OBVIOUS SHAPE IS THE WRONG ONE. An earlier revision of this note named `the checkpoint rows gain a declaring-module column`. vivid-wren-870 refused that shape with an argument this note adopts: a TypeCheckpoint row is cited to the Rust reference and states how RUST spells a type, whereas which dag module declares Int is a gunbc-corpus fact, so a declaring-module column puts corpus data inside an extdeps upstream authority -- a layer inversion, and the same class as a row being asked a question its cited authority cannot answer. The expected terminal shape is TWO authorities rather than one wider one: extdeps keeps Rust type -> spelling, a corpus-side binding says this dag declaration realizes as that Rust type, and lookup_checkpoint keys on the second. That also lets the seven differ from each other, which one column keyed on a single module cannot express. Recorded as a proposal from the rows owner, not as a decision, and unbuilt at the time of writing. When it lands the residue assertions flip to None and the flip is the dissolution signal, not a regression. LANDED FOR HASH (this PR, T7): the second authority is v1.compiler.coercion structural_declaration_modules_for, a corpus-side row roster keyed on the dag_name and enumerating the modules whose declaration of that name is structural rather than native -- \"Hash\" => [\"src/v2/std/node.dag\"] is its one row. lookup_checkpoint (v1.compiler.coercion) now consults it before the bare-name table: when decl_file_declares_structurally holds, lookup_checkpoint refuses (none) rather than answering from the table, and every consumer that already carried a correct identity-arm fallback -- coerce_primitive_type, is_copy, literal_suffix, and the direct callers of lookup_checkpoint itself -- inherits the refusal once decl_file is threaded to the call, which it now is at every production call site across v1.compiler.emit_rust and v1.compiler.emit. table_present_hash_refuses_under_structural_declaration in the witness below is the flip this note predicted; it is no longer residue. LANDED FOR STRING (session merry-lark-67, per smart-ram-730's dispatch): structural_declaration_modules_for gained a second row, \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"] -- both declare `type String = FreeMonoid`, the structural free-monoid-over-Char carrier, never a host string, so a reference resolving to either module now refuses the bare-name table's `String`/`.to_string()` spelling instead of silently rendering it. residue_table_present_string_bypasses_identity in the legacy oracle (src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag) is retired for the same reason table_present_hash_refuses_under_structural_declaration closed for Hash, and is replaced there by table_present_string_refuses_under_structural_declaration_text / _string_type rather than repaired back to a passing bypass -- the flip is the dissolution signal, not a regression. LANDED FOR BOOL (session merry-lark-67, corpus-wide histogram from smart-ram-730; corrected same session, commit 127ad848070, per review 54257): structural_declaration_modules_for gained a third row, \"Bool\" => [\"src/v2/std/logic.dag\"] -- the initial enrollment mirrored String's two-row shape onto Bool and also listed dag/std/types.dag, but that module is the ordinary corpus-wide native Bool prelude (imported by 300+ dag/test/claim modules with no bit/width/encoding modeling riding on it), directly analogous to dag/std/integer.dag for Int, which sits in the POSITIVE numeric_realization_declaring_modules roster, never the negative structural one. Only src/v2/std/logic.dag's Bool is genuinely structural, carrying BoolWidthFact/BoolEncodingFact/BooleanAlgebra modeling over the two-variant coproduct; a reference resolving to it refuses the bare-name table's `bool`/`false` spelling instead of silently rendering it, while a reference resolving to dag/std/types.dag renders natively as designed. The over-broad row caused required-floor to refuse native bool rendering for 5 unrelated fixtures (e0308_mechanical_trio_test, optional_carrier_signature_test) and caused required-regen to see drift across the self-hosted std_*.rs mirrors; both are the fabricated-plausible-ceiling failure this note elsewhere criticizes, disclosed and repaired here rather than left standing. Bool never had a residue row in the legacy oracle to flip; it lands directly as one CLOSED row, table_present_bool_refuses_under_structural_declaration_logic, alongside table_present_bool_renders_natively_for_the_corpus_prelude confirming dag/std/types.dag's native rendering. KNOWN GAP THIS ROW DOES NOT CLOSE, FOUND WHILE MEASURING IT: emit_typed_item's type-alias arm special-cases `item_text == \"String\"` UNCONDITIONALLY -- rust_string_grounded_type_alias_decl_line emits `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file, never consulting rust_scalar_checkpoint_render_base or this roster at all. So the module that declares `type String = FreeMonoid` keeps emitting itself as a host-String alias even after this row makes every REFERENCE to it refuse the bare-name table; the declaration and its own references can now disagree in the SAME emitted file. This is not fixed here -- it is a separate emit_rust mechanism, unconditional on decl_file, that this row's PR does not touch -- and is recorded as the next-rung trigger for String's declaration-site emission specifically, distinct from the reference-site gate this note otherwise describes. REACHABILITY CORRECTION (royal-dove-436, adhoc-c735d227-60b, 2026-08-21, measured on the 03_ingest closure): TWO CLAIMS ABOVE ARE FALSE FOR STRING AND ARE CORRECTED HERE RATHER THAN SOFTENED -- the LANDED FOR STRING clause's 'a reference resolving to either module now refuses the bare-name table's String/.to_string() spelling instead of silently rendering it', and the KNOWN GAP clause's 'even after this row makes every REFERENCE to it refuse the bare-name table'. The row does not make every reference refuse, because a String-spelled reference in TYPE position never reaches lookup_checkpoint at all. SIX type renderers in this module -- render_rust_type, render_rust_type_without_applied_binding, render_rust_applied_type, render_rust_type_with_applied_binding, render_rust_decl_type and render_rust_fn_sig_type -- each RETURN ON THEIR FIRST LINE (verified: the call is the statement immediately following each fn's own declaration) via is_host_text_carrier_type, rendering the literal \"String\" unconditionally on decl_file, ahead of every checkpoint or roster consultation; and is_host_text_carrier_type accepts the spelling String outright, so no path through those six can reach type_realization_decision's Unrealized-via-structural-gate arm for it. THE ROW IS THEREFORE PRESENT, CORRECT, AND UNREACHABLE FOR THE TEXT CARRIER IN TYPE POSITION -- an unreachable wall rather than a missing one, which is DESIGN section 6's coverage-by-illusion and a section 4b rung this note previously reported as held. This is a REACHABILITY claim about String's reference-site gate; it does NOT touch the Hash clause above, whose 'NO live site is claimed' is scoped to a v2-declared Hash reaching lookup_checkpoint and is unaffected, and it is a DIFFERENT mechanism from the declaration-site alias line the KNOWN GAP clause otherwise describes. SUPPORTING EVIDENCE, cited as a population rather than as the basis of the claim: 34 live E0308 sites in the 03_ingest closure pair a String-declared field or parameter against a FreeMonoid-realized value, every one of them a type position that rendered the native spelling while the roster says the declaration is structural (docs/probes/t2_t3_realization_route_2026-08-21.md, per-site TSV beside it). ESTABLISHED HOW, because the distinction decides what would falsify this: the reachability claim is decidable from the five renderers' control flow, which is how it was established -- NOT by a discriminating execution, and it says nothing about a sixth renderer that may handle some type position without that preamble. NEXT-RUNG TRIGGER: the short-circuit family is deleted so the existing authority becomes reachable, per docs/plans/carrier-realization-arbiter-repair-design.md, which also counts the decl_file == \"\" residue this module contributes (four sites) that the DECLARED RESIDUE note in v1.compiler.coercion says is uncounted. That design leaves the structural-vs-native direction to its owner and proposes an emit-only blast-radius measurement, not a merge, as the next step -- deliberately, because the over-broad Bool row recorded above is what picking a direction without that measurement already cost once. Int, Float, Symbol remain open -- they have no row in structural_declaration_modules_for -- and are the population the next instance of this class (a name question answered by authored spelling instead of declaration identity) inherits, per the class-level framing this ceiling was folded into. The roster is deliberately a single generic, identity-keyed mechanism with one row rather than a Hash-specific special case, so a future row for Int or String is an addition to this same authority, not a new mechanism. MEASURED CONSEQUENCE AT ARTIFACT GRAIN, added after this note first landed: the bypass is observable in the emitted FILE SET, not only in the emitter's answer. In a two-arm emission of one v2-only closure the file v2_std_integer.rs is present before the cut and ABSENT after it. That module declares exactly one item, the v2-declared structural Int, and its only type-position consumer was a single generated re-export line in std_algebra.rs; with Int reaching the bare-name checkpoint the re-export is no longer generated, nothing references the module, and it is not emitted. Every other hunk in that file is an offset shift from the deleted line -- the Int string literals are unchanged and the i64 count in the file is identical across arms, so nothing became native that was structural. AND THE DROP IS THE MINORITY CASE -- THE WRONG REALIZATION IS EMITTED, NOT AVOIDED. Across eleven emitted closures measured by smart-ibex-716 (corpus a6bceb6903, binaries a6bceb6903 and ad05a2f2d5), the module disappears in only 2; in the other 9 it SURVIVES with its content changed, from pub type Int = GroupCompletion> to pub type Int = i64. So the native realization of the v2-declared Peano-completion type is already present in the emitted artifact. What is absent is only a consumer: the same census found ZERO type-position uses of the v2 Int in any of the eleven -- every qualified occurrence sits on a use line, and the only bare occurrences surviving a use-line exclusion were four string literals inside prose, one of them a parser test fixture. Two false positives were found and discarded on the way to that zero, both by pulling the specimen rather than trusting the count. The residue is therefore NOT a dead re-export being dropped, which was this note's first reading and is corrected here; it is a wrong realization sitting inert with no diagnostic attached, so the day any declaration binds a bare Int in one of those closures it binds i64 silently. THE HAZARD TRIGGER IS THEREFORE A TYPE POSITION APPEARING, not the re-export returning. This is recorded because a module leaving OR silently changing an alias target is the kind of consequence a content-only diff of one closure reads as offset noise: the instruments that name it are a file-set diff and a cross-closure alias-target read, and neither was in this PR's original receipt.".to_string() + "CEILING, STATED BECAUSE THE CODE DELIVERS LESS THAN THE DELETION OF RustCorpusRepr SUGGESTS. lookup_checkpoint is keyed on the BARE dag_name and is consulted BEFORE the identity-keyed arm, so any name carrying a checkpoint row in extdeps/languages/rust/types.dag bypasses declaration keying entirely. Nat carries no row and therefore discriminates correctly -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag refuses. Names WITH a row do not. This is not a regression introduced here: the table was already bare-name keyed and the global corpus mode was hiding the question. It is the honest rung. The class is MECHANICALLY PREVENTABLE rather than structurally impossible, and its executing evidence is v1.tests.claim.checkpoint_identity_keying_witness_test, which asserts the CURRENT bypassing answers on purpose so the gap is counted instead of assumed closed. THAT CITATION WAS FALSE WHEN THIS NOTE FIRST LANDED AND IS REPAIRED RATHER THAN SOFTENED. It named the residue block generated by v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into a module declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate -- while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package consuming v1-compiler as an ordinary dependency, so cfg(test) is never set for it and the block is not compiled, let alone executed. Measured rather than reasoned: that step's binary enumerates 30 tests and none is this one, against a positive control confirming the enumeration is non-empty. So a ceiling disclosure cited evidence that had never run -- DESIGN section 4b(1) rung honesty violated in the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The assertions were re-authored as an enrolled .dag witness and now execute (seven rows PASS, including the discriminating row where two declarations share the spelling Nat and answer differently); the superseded generated-Rust block is deleted rather than left standing as a second, silent copy. POPULATION (census by vivid-wren-870, who owns the rows): SEVEN of the table's names are also declared under src/v2 -- Int, Float, Bool, Symbol, Unit, String, Hash; Bytes, Secret and Json are not. That is a LOWER BOUND obtained by grepping line-start `type ` declarations under src/v2; it does not find names introduced any other way, and it says NOTHING about how many sites bite in any real closure. Three of the seven are the same shape as Int in that the v2 declaration is a genuinely different STRUCTURE rather than a spelling coincidence -- Int is GroupCompletion, String is FreeMonoid, Bool is a two-variant coproduct. Symbol and Unit are bodyless and may be declared-abstract rather than competing realizations, so their bypass may be harmless. Hash is the one that costs a GUARANTEE rather than merely a representation, and it belongs with the same-shape three rather than apart from them: the row targets v1_rt::Hash, which is `pub type Hash = String` in the seed, against a v2 declaration of Fnv1a64Structural -- a single-field record whose digest field is `String where lower_hex_16`. std.content_hash content_hash_family_constructor_note states the public forgeable record constructors are DELETED and that the where-refinement IS the construction wall, so realizing that type as a bare String alias renders away the carrier the wall is attached to. A name-keyed spelling row can therefore silently drop a §4b construction rung. Established from declarations at both ends (vivid-wren-870, re-read here); NO live site is claimed, because no closure reaching a v2-declared Hash through lookup_checkpoint has been emitted by either of us. NEXT-RUNG TRIGGER -- AND THE OBVIOUS SHAPE IS THE WRONG ONE. An earlier revision of this note named `the checkpoint rows gain a declaring-module column`. vivid-wren-870 refused that shape with an argument this note adopts: a TypeCheckpoint row is cited to the Rust reference and states how RUST spells a type, whereas which dag module declares Int is a gunbc-corpus fact, so a declaring-module column puts corpus data inside an extdeps upstream authority -- a layer inversion, and the same class as a row being asked a question its cited authority cannot answer. The expected terminal shape is TWO authorities rather than one wider one: extdeps keeps Rust type -> spelling, a corpus-side binding says this dag declaration realizes as that Rust type, and lookup_checkpoint keys on the second. That also lets the seven differ from each other, which one column keyed on a single module cannot express. Recorded as a proposal from the rows owner, not as a decision, and unbuilt at the time of writing. When it lands the residue assertions flip to None and the flip is the dissolution signal, not a regression. LANDED FOR HASH (this PR, T7): the second authority is v1.compiler.coercion structural_declaration_modules_for, a corpus-side row roster keyed on the dag_name and enumerating the modules whose declaration of that name is structural rather than native -- \"Hash\" => [\"src/v2/std/node.dag\"] is its one row. lookup_checkpoint (v1.compiler.coercion) now consults it before the bare-name table: when decl_file_declares_structurally holds, lookup_checkpoint refuses (none) rather than answering from the table, and every consumer that already carried a correct identity-arm fallback -- coerce_primitive_type, is_copy, literal_suffix, and the direct callers of lookup_checkpoint itself -- inherits the refusal once decl_file is threaded to the call, which it now is at every production call site across v1.compiler.emit_rust and v1.compiler.emit. table_present_hash_refuses_under_structural_declaration in the witness below is the flip this note predicted; it is no longer residue. LANDED FOR STRING (session merry-lark-67, per smart-ram-730's dispatch): structural_declaration_modules_for gained a second row, \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"] -- both declare `type String = FreeMonoid`, the structural free-monoid-over-Char carrier, never a host string, so a reference resolving to either module now refuses the bare-name table's `String`/`.to_string()` spelling instead of silently rendering it. residue_table_present_string_bypasses_identity in the legacy oracle (src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag) is retired for the same reason table_present_hash_refuses_under_structural_declaration closed for Hash, and is replaced there by table_present_string_refuses_under_structural_declaration_text / _string_type rather than repaired back to a passing bypass -- the flip is the dissolution signal, not a regression. LANDED FOR BOOL (session merry-lark-67, corpus-wide histogram from smart-ram-730; corrected same session, commit 127ad848070, per review 54257): structural_declaration_modules_for gained a third row, \"Bool\" => [\"src/v2/std/logic.dag\"] -- the initial enrollment mirrored String's two-row shape onto Bool and also listed dag/std/types.dag, but that module is the ordinary corpus-wide native Bool prelude (imported by 300+ dag/test/claim modules with no bit/width/encoding modeling riding on it), directly analogous to dag/std/integer.dag for Int, which sits in the POSITIVE numeric_realization_declaring_modules roster, never the negative structural one. Only src/v2/std/logic.dag's Bool is genuinely structural, carrying BoolWidthFact/BoolEncodingFact/BooleanAlgebra modeling over the two-variant coproduct; a reference resolving to it refuses the bare-name table's `bool`/`false` spelling instead of silently rendering it, while a reference resolving to dag/std/types.dag renders natively as designed. The over-broad row caused required-floor to refuse native bool rendering for 5 unrelated fixtures (e0308_mechanical_trio_test, optional_carrier_signature_test) and caused required-regen to see drift across the self-hosted std_*.rs mirrors; both are the fabricated-plausible-ceiling failure this note elsewhere criticizes, disclosed and repaired here rather than left standing. Bool never had a residue row in the legacy oracle to flip; it lands directly as one CLOSED row, table_present_bool_refuses_under_structural_declaration_logic, alongside table_present_bool_renders_natively_for_the_corpus_prelude confirming dag/std/types.dag's native rendering. KNOWN GAP THIS ROW DOES NOT CLOSE, FOUND WHILE MEASURING IT: emit_typed_item's type-alias arm special-cases `item_text == \"String\"` UNCONDITIONALLY -- rust_string_grounded_type_alias_decl_line emits `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file, never consulting rust_scalar_checkpoint_render_base or this roster at all. So the module that declares `type String = FreeMonoid` keeps emitting itself as a host-String alias even after this row makes every REFERENCE to it refuse the bare-name table; the declaration and its own references can now disagree in the SAME emitted file. THAT KNOWN GAP IS NOW CLOSED, AND THE ROOT WAS NOT WHERE THIS NOTE PUT IT. The gap as recorded: emit_typed_item's type-alias arm special-cased `item_text == \"String\"` UNCONDITIONALLY, emitting `pub type String = std::string::String;` at the DECLARATION site regardless of decl_file and never consulting the identity-keyed authority every REFERENCE already routed through, so one emitted file could disagree with itself. This note framed that as a second bare-name bypass to be deleted. IT WAS NOT. The arm was COMPENSATING, and deleting it alone would have emitted `pub type String = String;` -- self-referential, because the checkpoint's target_type for String is the bare spelling `String` and the declaration site uses target_type as the alias's right-hand side. The real defect was that ONE FIELD CARRIED TWO SPELLING ROLES (the word arity is avoided here on purpose -- in this module it already means type-parameter count, see AliasDeclArityVerdict and rust_checkpoint_scalar_declared_arity_guard_note): one field answering two questions -- what a REFERENCE renders (bare `String`, correct and idiomatic) and what a DECLARATION is GROUNDED IN (`std::string::String`, the spelling no alias can shadow). Whichever spelling one field carried, one consumer was wrong, and the arm was the visible cost of making it try. std.coercion TypeCheckpoint now carries both spellings as separate fields; rust_scalar_checkpoint_reference_base and rust_scalar_checkpoint_grounding_base are two named entry points over one shared identity-keyed body, so every PRODUCTION caller states which question it asks by visibly naming it rather than by passing an argument. That is mechanically preventable, NOT structurally impossible: the shared body stays reachable and carries the discriminator, .dag has no function-privacy concept to hide it behind (the emitted emitter carries 665 pub fn and zero non-pub), and the next-rung trigger is a module-private function boundary in the language. The standing evidence for the narrower claim is that the shared body's only direct callers are the two wrappers; the three reference callers read the reference spelling, the single declaration-RHS caller reads grounding, and the arm is DELETED rather than guarded. WHAT THIS STILL DOES NOT CLOSE, stated so the ceiling is not read as retired: lookup_checkpoint's FIRST arm answers straight from the bare-name table when decl_file is the empty string, consulting no roster at all, so every site reaching emission with UNKNOWN declaration identity still realizes from the table exactly as this note describes. That bypass is live, its population is UNCOUNTED, and no estimate is offered here. It is a separate defect from the two-role split -- the split governs what a row can SAY once identity is known; the bypass governs whether identity is consulted at all -- and it is filed as its own row rather than folded into this one. HOW THIS CLOSURE AND THE REACHABILITY CORRECTION BELOW RELATE, because each narrows the other and reading either alone overstates it: the two-role split is what makes the DECLARATION site able to consult the identity-keyed authority at all, and royal-dove-436's finding is that the REFERENCE site for a String-spelled type never reaches lookup_checkpoint in the first place. So for String specifically the split repairs a position that was answering wrongly, while the position this note elsewhere calls gated is not yet reached -- the declaration half is closed and the reference half is unreachable, which is one authority with two different reasons its consumers do not see it, not one gap. Neither finding weakens the other and neither is the whole story for String; the split is stated here as closing the arm it deletes, never as making every String position identity-keyed. REACHABILITY CORRECTION (royal-dove-436, adhoc-c735d227-60b, 2026-08-21, measured on the 03_ingest closure): TWO CLAIMS ABOVE ARE FALSE FOR STRING AND ARE CORRECTED HERE RATHER THAN SOFTENED -- the LANDED FOR STRING clause's 'a reference resolving to either module now refuses the bare-name table's String/.to_string() spelling instead of silently rendering it', and the KNOWN GAP clause's 'even after this row makes every REFERENCE to it refuse the bare-name table'. The row does not make every reference refuse, because a String-spelled reference in TYPE position never reaches lookup_checkpoint at all. SIX type renderers in this module -- render_rust_type, render_rust_type_without_applied_binding, render_rust_applied_type, render_rust_type_with_applied_binding, render_rust_decl_type and render_rust_fn_sig_type -- each RETURN ON THEIR FIRST LINE (verified: the call is the statement immediately following each fn's own declaration) via is_host_text_carrier_type, rendering the literal \"String\" unconditionally on decl_file, ahead of every checkpoint or roster consultation; and is_host_text_carrier_type accepts the spelling String outright, so no path through those six can reach type_realization_decision's Unrealized-via-structural-gate arm for it. THE ROW IS THEREFORE PRESENT, CORRECT, AND UNREACHABLE FOR THE TEXT CARRIER IN TYPE POSITION -- an unreachable wall rather than a missing one, which is DESIGN section 6's coverage-by-illusion and a section 4b rung this note previously reported as held. This is a REACHABILITY claim about String's reference-site gate; it does NOT touch the Hash clause above, whose 'NO live site is claimed' is scoped to a v2-declared Hash reaching lookup_checkpoint and is unaffected, and it is a DIFFERENT mechanism from the declaration-site alias line the KNOWN GAP clause otherwise describes. SUPPORTING EVIDENCE, cited as a population rather than as the basis of the claim: 34 live E0308 sites in the 03_ingest closure pair a String-declared field or parameter against a FreeMonoid-realized value, every one of them a type position that rendered the native spelling while the roster says the declaration is structural (docs/probes/t2_t3_realization_route_2026-08-21.md, per-site TSV beside it). ESTABLISHED HOW, because the distinction decides what would falsify this: the reachability claim is decidable from the five renderers' control flow, which is how it was established -- NOT by a discriminating execution, and it says nothing about a sixth renderer that may handle some type position without that preamble. NEXT-RUNG TRIGGER: the short-circuit family is deleted so the existing authority becomes reachable, per docs/plans/carrier-realization-arbiter-repair-design.md, which also counts the decl_file == \"\" residue this module contributes (four sites) that the DECLARED RESIDUE note in v1.compiler.coercion says is uncounted. That design leaves the structural-vs-native direction to its owner and proposes an emit-only blast-radius measurement, not a merge, as the next step -- deliberately, because the over-broad Bool row recorded above is what picking a direction without that measurement already cost once. Int, Float, Symbol remain open -- they have no row in structural_declaration_modules_for -- and are the population the next instance of this class (a name question answered by authored spelling instead of declaration identity) inherits, per the class-level framing this ceiling was folded into. The roster is deliberately a single generic, identity-keyed mechanism with one row rather than a Hash-specific special case, so a future row for Int or String is an addition to this same authority, not a new mechanism. MEASURED CONSEQUENCE AT ARTIFACT GRAIN, added after this note first landed: the bypass is observable in the emitted FILE SET, not only in the emitter's answer. In a two-arm emission of one v2-only closure the file v2_std_integer.rs is present before the cut and ABSENT after it. That module declares exactly one item, the v2-declared structural Int, and its only type-position consumer was a single generated re-export line in std_algebra.rs; with Int reaching the bare-name checkpoint the re-export is no longer generated, nothing references the module, and it is not emitted. Every other hunk in that file is an offset shift from the deleted line -- the Int string literals are unchanged and the i64 count in the file is identical across arms, so nothing became native that was structural. AND THE DROP IS THE MINORITY CASE -- THE WRONG REALIZATION IS EMITTED, NOT AVOIDED. Across eleven emitted closures measured by smart-ibex-716 (corpus a6bceb6903, binaries a6bceb6903 and ad05a2f2d5), the module disappears in only 2; in the other 9 it SURVIVES with its content changed, from pub type Int = GroupCompletion> to pub type Int = i64. So the native realization of the v2-declared Peano-completion type is already present in the emitted artifact. What is absent is only a consumer: the same census found ZERO type-position uses of the v2 Int in any of the eleven -- every qualified occurrence sits on a use line, and the only bare occurrences surviving a use-line exclusion were four string literals inside prose, one of them a parser test fixture. Two false positives were found and discarded on the way to that zero, both by pulling the specimen rather than trusting the count. The residue is therefore NOT a dead re-export being dropped, which was this note's first reading and is corrected here; it is a wrong realization sitting inert with no diagnostic attached, so the day any declaration binds a bare Int in one of those closures it binds i64 silently. THE HAZARD TRIGGER IS THEREFORE A TYPE POSITION APPEARING, not the re-export returning. This is recorded because a module leaving OR silently changing an alias target is the kind of consequence a content-only diff of one closure reads as offset noise: the instruments that name it are a file-set diff and a cross-closure alias-target read, and neither was in this PR's original receipt.".to_string() }; } CACHED.with(|c: &String| c.clone()) } -pub fn rust_scalar_checkpoint_render_base(dag_name: String, decl_file: String) -> Option { +pub fn rust_scalar_checkpoint_reference_base( + dag_name: String, + decl_file: String, +) -> Option { + rust_scalar_checkpoint_spelling(dag_name.clone(), decl_file.clone(), false) +} + +pub fn rust_scalar_checkpoint_grounding_base( + dag_name: String, + decl_file: String, +) -> Option { + rust_scalar_checkpoint_spelling(dag_name.clone(), decl_file.clone(), true) +} + +pub fn rust_scalar_checkpoint_spelling( + dag_name: String, + decl_file: String, + grounding: bool, +) -> Option { match lookup_checkpoint(RenderTarget::Rust, dag_name.clone(), decl_file.clone()) { - Some(cp) => Some(cp.target_type.clone()), + Some(cp) => Some(if grounding.clone() { + cp.grounding_type.clone() + } else { + cp.target_type.clone() + }), None => match rust_seed_host_numeric_alias(dag_name.clone(), decl_file.clone()) { Some(host) => Some(host.clone()), None => None, @@ -803,7 +815,7 @@ pub fn rust_render_checkpoint_scalar_bare( } match rust_seed_host_numeric_alias(leaf.clone(), type_reference_decl_file(n.clone())) { Some(numeric) => Some(numeric.clone()), - None => match rust_scalar_checkpoint_render_base( + None => match rust_scalar_checkpoint_reference_base( leaf.clone(), type_reference_decl_file(n.clone()), ) { @@ -1621,7 +1633,7 @@ pub fn render_rust_applied_type( } } } else { - match rust_scalar_checkpoint_render_base( + match rust_scalar_checkpoint_reference_base( base_name.clone(), type_reference_decl_file(n.clone()), ) { @@ -2542,7 +2554,7 @@ pub fn render_rust_alias_rhs_type( { { let leaf = qualified_last_segment(name.clone()); - let numeric_host_alias = match rust_scalar_checkpoint_render_base( + let numeric_host_alias = match rust_scalar_checkpoint_reference_base( leaf.clone(), type_reference_decl_file(n.clone()), ) { @@ -12194,88 +12206,84 @@ pub fn emit_typed_item( ) } else { if is_type_alias_item(item.clone(), env.source_indices.clone()) { - if (item_text.clone() == "String".to_string()) { - rust_string_grounded_type_alias_decl_line() + if (((item.params.clone().len() as i64) == 0) + && rust_opaque_kernel_alias_type_eligible(item_text.clone())) + { + rust_opaque_kernel_alias_type_decl(item_text.clone()) } else { if (((item.params.clone().len() as i64) == 0) - && rust_opaque_kernel_alias_type_eligible(item_text.clone())) + && rust_nominal_identity_carrier_type_eligible(item_text.clone())) { - rust_opaque_kernel_alias_type_decl(item_text.clone()) + rust_nominal_identity_carrier_def(item_text.clone()) } else { - if (((item.params.clone().len() as i64) == 0) - && rust_nominal_identity_carrier_type_eligible(item_text.clone())) - { - rust_nominal_identity_carrier_def(item_text.clone()) - } else { - if is_zero_param_self_referential_opaque_decl( + if is_zero_param_self_referential_opaque_decl( + item.clone(), + env.source_indices.clone(), + ) { + emit_zero_param_phantom_opaque_struct( item.clone(), + v1_rt::set_contains( + &emit_info.map_key_required_type_names.clone(), + item_text.clone(), + ), env.source_indices.clone(), + ) + } else { + match rust_scalar_checkpoint_grounding_base( + item_text.clone(), + decl_identity_file(item.clone()), ) { - emit_zero_param_phantom_opaque_struct( - item.clone(), - v1_rt::set_contains( - &emit_info.map_key_required_type_names.clone(), - item_text.clone(), - ), - env.source_indices.clone(), - ) - } else { - match rust_scalar_checkpoint_render_base( - item_text.clone(), - decl_identity_file(item.clone()), - ) { - Some(host) => v1_rt::concat( + Some(host) => v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - rust_visibility_prefix(), - rust_items().type_alias_keyword.clone(), - ), - " ".to_string(), + rust_visibility_prefix(), + rust_items().type_alias_keyword.clone(), ), - item_text.clone(), + " ".to_string(), ), - " = ".to_string(), + item_text.clone(), ), - host.clone(), + " = ".to_string(), ), - ";".to_string(), + host.clone(), ), - None => v1_rt::concat( + ";".to_string(), + ), + None => v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - rust_visibility_prefix(), - rust_items().type_alias_keyword.clone(), - ), - " ".to_string(), + rust_visibility_prefix(), + rust_items().type_alias_keyword.clone(), ), - item_text.clone(), + " ".to_string(), ), - " = ".to_string(), - ), - render_rust_alias_rhs_type( - resolved_type(item.clone()), - Rc::new(vec![]), - shared_types.clone(), - env.source_indices.clone(), - scope.clone(), - imports.clone(), - registry.clone(), - module_name.clone(), - export_sets.clone(), - typed_modules.clone(), - module_index.clone(), - emit_info.variant_to_enum.clone(), + item_text.clone(), ), + " = ".to_string(), + ), + render_rust_alias_rhs_type( + resolved_type(item.clone()), + Rc::new(vec![]), + shared_types.clone(), + env.source_indices.clone(), + scope.clone(), + imports.clone(), + registry.clone(), + module_name.clone(), + export_sets.clone(), + typed_modules.clone(), + module_index.clone(), + emit_info.variant_to_enum.clone(), ), - ";".to_string(), ), - } + ";".to_string(), + ), } } } diff --git a/src/v1/stage0/src/v1_tests_claim_checkpoint_identity_keying_witness_test.rs b/src/v1/stage0/src/v1_tests_claim_checkpoint_identity_keying_witness_test.rs index 562ec5d800c..6f44f0a602d 100644 --- a/src/v1/stage0/src/v1_tests_claim_checkpoint_identity_keying_witness_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_checkpoint_identity_keying_witness_test.rs @@ -4,7 +4,9 @@ pub use crate::v1_compiler_artifact::RenderTarget; use crate::v1_compiler_artifact::RenderTarget::Rust; pub use crate::v1_compiler_coercion::literal_suffix; -pub use crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base; +pub use crate::v1_compiler_emit_rust::{ + rust_scalar_checkpoint_grounding_base, rust_scalar_checkpoint_reference_base, +}; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; use crate::NonEmptyBTreeSet; @@ -15,63 +17,63 @@ use std::rc::Rc; pub fn checkpoint_identity_keying_witness_note() -> String { thread_local! { static CACHED: String = { - "EXECUTING evidence for the declaration-identity keying of Rust primitive realization, and for the checkpoint-table bypass that keying does NOT close.\n\nWHY THIS FILE EXISTS RATHER THAN THE ROWS IT REPLACES. The same assertions were authored as generated Rust in v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into src/v1/stage0/src/compiler_tests.rs. That module is declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate, while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package that consumes v1-compiler as an ordinary dependency -- so cfg(test) is never set for it and the module is not compiled, let alone run. Measured by execution rather than by reading: the binary that step builds enumerates 30 tests and none of them is this one, against a positive control confirming the enumeration is non-empty. The assertions were therefore authored, plausible, type-correct and NEVER EXECUTED, and v1.compiler.emit_rust checkpoint_table_bypasses_identity_note nonetheless cited them as the class's executing evidence. That is rung inflation in the disclosure of a ceiling -- the DESIGN section 4b(1) failure applied to the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The claim is repaired by making it TRUE here rather than by softening the sentence.\n\nWHAT DISCRIMINATES. rust_scalar_checkpoint_render_base takes a bare type name and the resolved declaration's ident_span file. The first four rows are the keying itself: a name with a table row renders from the table; a name WITHOUT one (Nat) reaches the identity arm and answers differently for two declarations that share a spelling -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag does not, and an EMPTY decl_file (identity unknown at the site) refuses rather than guessing. Those four cannot be satisfied together by any constant, by a disabled mechanism, or by a rule keyed on the name alone, which is precisely the property the deleted global corpus mode lacked.\n\nTHE RESIDUE ROWS ASSERT THE CURRENT BYPASSING ANSWERS ON PURPOSE. The table is keyed on the bare name and consulted BEFORE identity, so a table-present name bypasses declaration keying entirely: Int under a src/v2 path still renders i64 even though that declaration is GroupCompletion and not a machine integer. They are counted here rather than assumed closed. They FLIP to Absent when a name gets its own row in v1.compiler.coercion structural_declaration_modules_for, and that flip is the dissolution signal, NOT a regression -- do not make them pass again. Hash already made that flip: lookup_checkpoint (v1.compiler.coercion) now refuses before the bare-name table is consulted whenever decl_file names a module enrolled in structural_declaration_modules_for, and \"src/v2/std/node.dag\" is that module's one enrolled row, so table_present_hash_refuses_under_structural_declaration below is CLOSED rather than residue. String made the same flip in a later change: structural_declaration_modules_for now also enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which declare the structural FreeMonoid carrier rather than a host string, so table_present_string_refuses_under_structural_declaration_text and its _string_type sibling below are CLOSED and residue_table_present_string_bypasses_identity is retired rather than repaired back to passing. Bool was added in the same change -- structural_declaration_modules_for now also enrolls \"Bool\" => [\"src/v2/std/logic.dag\"], whose `type Bool = True | False` sits beside a BooleanAlgebra instance modeling machine-bool bit/width/encoding facts and so cannot shortcut to the primitive it derives, so table_present_bool_refuses_under_structural_declaration_logic below is CLOSED. dag/std/types.dag is NOT enrolled (see RE-GROUNDING NOTE 2): its `type Bool = True | False` is the ordinary corpus-wide prelude Bool, the genuine native declaring module parallel to dag/std/integer.dag for Int, so table_present_bool_renders_natively_for_the_corpus_prelude below asserts the positive answer instead. No residue_table_present_bool row ever existed in this file to retire. Int remains open -- it has no row yet -- and is exactly the residue population the next instance of this class inherits.\n\nWHERE THIS EXECUTES, STATED PRECISELY BECAUSE THE PREVIOUS CLAIM'S WHOLE DEFECT WAS AN IMPRECISE ONE. The row is enrolled in gunbc.ci_layer_roots v1_claim_scoped_witness_entries, consumed by v1_claim_scoped_witness_batch, whose source-root envelope is dag plus src/v1 -- the envelope this file needs, since it imports v1.compiler.emit_rust. The entry carries the empty function name, so it expands to every test fn here rather than pinning a roster of them. That batch runs SelectionApplied, so this witness executes on changes that affect it and emits a ScopedWitnessSelectionSkipped receipt with provenance otherwise; it is NOT claimed to run on every PR. That is the correct scope rather than a concession: evidence guarding a decision inside emit_rust should execute when emit_rust changes, and a provenance failure refuses loudly instead of widening. Note also what the enrollment is NOT: witness_discovery_scan_dirs is the owned-data-decl scope, not the witness scope, so membership there would neither add nor remove execution here. The assertions were additionally run directly during authoring -- all fourteen PASS -- but direct execution is evidence the assertions HOLD, never evidence that CI runs them, and conflating those two is the same class of error this file exists to repair.\n\nRE-GROUNDING NOTE (smart-ram-730 blocker, session merry-lark-67): the ORIGINAL String residue row here queried decl_file \"src/v2/std/string.dag\", a path that does not exist anywhere in the corpus -- its predicted flip to `none` was therefore structurally unreachable regardless of whether structural_declaration_modules_for was correct, and the row measured nothing. It is replaced, not repaired, by the two CLOSED rows above keyed on the REAL declarations (src/v2/std/text.dag, dag/std/string_type.dag), each asserting the strong `== none` shape the Hash flip already established rather than the weaker `!= none` the broken row used. Two further specimens close the packet: a positive control (literal_suffix_positive_control_symbol_not_enrolled) proving the gate is not a blanket refusal, since without one every refusal row below would be satisfied vacuously by a mechanism that refuses unconditionally; and literal_suffix -- a DIFFERENT consumer of lookup_checkpoint than rust_scalar_checkpoint_render_base, with its own return shape and its own production call site -- is exercised separately rather than inferred from the type-alias rows, and that direct execution surfaced a genuine, distinct disclosure: the literal-rendering call site in v1.compiler.05_emit emit_literal never threads a real decl_file (LitStr passes the empty string), so literal_suffix at PRODUCTION sites cannot be gated by this roster however correctly the roster and lookup_checkpoint discriminate when a real decl_file is supplied. That is measured directly below, not assumed from the declaration-site gap this note's sibling (checkpoint_table_bypasses_identity_note) already names.\n\nRE-GROUNDING NOTE 2 (CI blocker, session merry-lark-67, PR #8708 @ c084813): the ORIGINAL Bool enrollment listed BOTH src/v2/std/logic.dag AND dag/std/types.dag, mirroring String's two-row shape without checking whether either declaration was actually the genuine native one -- unlike String's two rows (text.dag, string_type.dag), neither of which is imported as the corpus's everyday String, dag/std/types.dag IS the corpus's everyday Bool: import std.types { Bool } appears in 300+ dag/test/claim modules. Enrolling it made lookup_checkpoint refuse native `bool` for every one of them, which the required-floor CI phase caught as five genuine (non-KNOWN-RED) failures in optional_carrier_signature_test.dag and e0308_mechanical_trio_test.dag -- fixtures that use `flag: Bool` as an incidental parameter and assert nothing about Bool's own realization, so the breakage was pure collateral, not a caught defect in those fixtures. The correction follows the numeric_realization_declaring_modules precedent (v1.compiler.emit_rust numeric_realization_roster_extension_note): a name belongs in the NEGATIVE structural roster only when none of its dag declarations is genuinely native, the way Hash's is purely coincidental spelling; a declaration that IS the grounded native one -- dag/std/integer.dag for Int, dag/std/types.dag for Bool -- must keep rendering from the table. dag/std/types.dag is removed from Bool's row; src/v2/std/logic.dag stays, since its BooleanAlgebra/BoolWidthFact/BoolEncodingFact modeling is a genuine structural encoding of what a bool bit-pattern is, not the everyday corpus type.\n\ndissolve-on: a corpus-side declaration-to-Rust-type binding supersedes the bare-name row, at which point the residue rows flip and this note's second half retires with them. The extdeps table keeps Rust-type-to-spelling (which is what its cited authority can answer); which dag declaration realizes as which Rust type is a gunbc-corpus fact and does not belong in an upstream row.".to_string() + "EXECUTING evidence for the declaration-identity keying of Rust primitive realization, and for the checkpoint-table bypass that keying does NOT close.\n\nWHY THIS FILE EXISTS RATHER THAN THE ROWS IT REPLACES. The same assertions were authored as generated Rust in v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into src/v1/stage0/src/compiler_tests.rs. That module is declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate, while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package that consumes v1-compiler as an ordinary dependency -- so cfg(test) is never set for it and the module is not compiled, let alone run. Measured by execution rather than by reading: the binary that step builds enumerates 30 tests and none of them is this one, against a positive control confirming the enumeration is non-empty. The assertions were therefore authored, plausible, type-correct and NEVER EXECUTED, and v1.compiler.emit_rust checkpoint_table_bypasses_identity_note nonetheless cited them as the class's executing evidence. That is rung inflation in the disclosure of a ceiling -- the DESIGN section 4b(1) failure applied to the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The claim is repaired by making it TRUE here rather than by softening the sentence.\n\nWHAT DISCRIMINATES. rust_scalar_checkpoint_reference_base takes a bare type name and the resolved declaration's ident_span file. The first four rows are the keying itself: a name with a table row renders from the table; a name WITHOUT one (Nat) reaches the identity arm and answers differently for two declarations that share a spelling -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag does not, and an EMPTY decl_file (identity unknown at the site) refuses rather than guessing. Those four cannot be satisfied together by any constant, by a disabled mechanism, or by a rule keyed on the name alone, which is precisely the property the deleted global corpus mode lacked.\n\nTHE RESIDUE ROWS ASSERT THE CURRENT BYPASSING ANSWERS ON PURPOSE. The table is keyed on the bare name and consulted BEFORE identity, so a table-present name bypasses declaration keying entirely: Int under a src/v2 path still renders i64 even though that declaration is GroupCompletion and not a machine integer. They are counted here rather than assumed closed. They FLIP to Absent when a name gets its own row in v1.compiler.coercion structural_declaration_modules_for, and that flip is the dissolution signal, NOT a regression -- do not make them pass again. Hash already made that flip: lookup_checkpoint (v1.compiler.coercion) now refuses before the bare-name table is consulted whenever decl_file names a module enrolled in structural_declaration_modules_for, and \"src/v2/std/node.dag\" is that module's one enrolled row, so table_present_hash_refuses_under_structural_declaration below is CLOSED rather than residue. String made the same flip in a later change: structural_declaration_modules_for now also enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which declare the structural FreeMonoid carrier rather than a host string, so table_present_string_refuses_under_structural_declaration_text and its _string_type sibling below are CLOSED and residue_table_present_string_bypasses_identity is retired rather than repaired back to passing. Bool was added in the same change -- structural_declaration_modules_for now also enrolls \"Bool\" => [\"src/v2/std/logic.dag\"], whose `type Bool = True | False` sits beside a BooleanAlgebra instance modeling machine-bool bit/width/encoding facts and so cannot shortcut to the primitive it derives, so table_present_bool_refuses_under_structural_declaration_logic below is CLOSED. dag/std/types.dag is NOT enrolled (see RE-GROUNDING NOTE 2): its `type Bool = True | False` is the ordinary corpus-wide prelude Bool, the genuine native declaring module parallel to dag/std/integer.dag for Int, so table_present_bool_renders_natively_for_the_corpus_prelude below asserts the positive answer instead. No residue_table_present_bool row ever existed in this file to retire. Int remains open -- it has no row yet -- and is exactly the residue population the next instance of this class inherits.\n\nWHERE THIS EXECUTES, STATED PRECISELY BECAUSE THE PREVIOUS CLAIM'S WHOLE DEFECT WAS AN IMPRECISE ONE. The row is enrolled in gunbc.ci_layer_roots v1_claim_scoped_witness_entries, consumed by v1_claim_scoped_witness_batch, whose source-root envelope is dag plus src/v1 -- the envelope this file needs, since it imports v1.compiler.emit_rust. The entry carries the empty function name, so it expands to every test fn here rather than pinning a roster of them. That batch runs SelectionApplied, so this witness executes on changes that affect it and emits a ScopedWitnessSelectionSkipped receipt with provenance otherwise; it is NOT claimed to run on every PR. That is the correct scope rather than a concession: evidence guarding a decision inside emit_rust should execute when emit_rust changes, and a provenance failure refuses loudly instead of widening. Note also what the enrollment is NOT: witness_discovery_scan_dirs is the owned-data-decl scope, not the witness scope, so membership there would neither add nor remove execution here. The assertions were additionally run directly during authoring -- all fourteen PASS -- but direct execution is evidence the assertions HOLD, never evidence that CI runs them, and conflating those two is the same class of error this file exists to repair.\n\nRE-GROUNDING NOTE (smart-ram-730 blocker, session merry-lark-67): the ORIGINAL String residue row here queried decl_file \"src/v2/std/string.dag\", a path that does not exist anywhere in the corpus -- its predicted flip to `none` was therefore structurally unreachable regardless of whether structural_declaration_modules_for was correct, and the row measured nothing. It is replaced, not repaired, by the two CLOSED rows above keyed on the REAL declarations (src/v2/std/text.dag, dag/std/string_type.dag), each asserting the strong `== none` shape the Hash flip already established rather than the weaker `!= none` the broken row used. Two further specimens close the packet: a positive control (literal_suffix_positive_control_symbol_not_enrolled) proving the gate is not a blanket refusal, since without one every refusal row below would be satisfied vacuously by a mechanism that refuses unconditionally; and literal_suffix -- a DIFFERENT consumer of lookup_checkpoint than rust_scalar_checkpoint_reference_base, with its own return shape and its own production call site -- is exercised separately rather than inferred from the type-alias rows, and that direct execution surfaced a genuine, distinct disclosure: the literal-rendering call site in v1.compiler.05_emit emit_literal never threads a real decl_file (LitStr passes the empty string), so literal_suffix at PRODUCTION sites cannot be gated by this roster however correctly the roster and lookup_checkpoint discriminate when a real decl_file is supplied. That is measured directly below, not assumed from the declaration-site gap this note's sibling (checkpoint_table_bypasses_identity_note) already names.\n\nRE-GROUNDING NOTE 2 (CI blocker, session merry-lark-67, PR #8708 @ c084813): the ORIGINAL Bool enrollment listed BOTH src/v2/std/logic.dag AND dag/std/types.dag, mirroring String's two-row shape without checking whether either declaration was actually the genuine native one -- unlike String's two rows (text.dag, string_type.dag), neither of which is imported as the corpus's everyday String, dag/std/types.dag IS the corpus's everyday Bool: import std.types { Bool } appears in 300+ dag/test/claim modules. Enrolling it made lookup_checkpoint refuse native `bool` for every one of them, which the required-floor CI phase caught as five genuine (non-KNOWN-RED) failures in optional_carrier_signature_test.dag and e0308_mechanical_trio_test.dag -- fixtures that use `flag: Bool` as an incidental parameter and assert nothing about Bool's own realization, so the breakage was pure collateral, not a caught defect in those fixtures. The correction follows the numeric_realization_declaring_modules precedent (v1.compiler.emit_rust numeric_realization_roster_extension_note): a name belongs in the NEGATIVE structural roster only when none of its dag declarations is genuinely native, the way Hash's is purely coincidental spelling; a declaration that IS the grounded native one -- dag/std/integer.dag for Int, dag/std/types.dag for Bool -- must keep rendering from the table. dag/std/types.dag is removed from Bool's row; src/v2/std/logic.dag stays, since its BooleanAlgebra/BoolWidthFact/BoolEncodingFact modeling is a genuine structural encoding of what a bool bit-pattern is, not the everyday corpus type.\n\ndissolve-on: a corpus-side declaration-to-Rust-type binding supersedes the bare-name row, at which point the residue rows flip and this note's second half retires with them. The extdeps table keeps Rust-type-to-spelling (which is what its cited authority can answer); which dag declaration realizes as which Rust type is a gunbc-corpus fact and does not belong in an upstream row.".to_string() }; } CACHED.with(|c: &String| c.clone()) } pub fn table_present_name_renders_from_the_table() -> bool { - (rust_scalar_checkpoint_render_base("Int".to_string(), "dag/std/integer.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Int".to_string(), "dag/std/integer.dag".to_string()) .as_deref() == Some("i64".to_string()).as_deref()) } pub fn table_absent_name_realizes_natively_for_the_std_declaration() -> bool { - (rust_scalar_checkpoint_render_base("Nat".to_string(), "dag/std/nat.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Nat".to_string(), "dag/std/nat.dag".to_string()) .as_deref() == Some("i64".to_string()).as_deref()) } pub fn same_spelling_different_declaration_does_not_realize_natively() -> bool { - (rust_scalar_checkpoint_render_base("Nat".to_string(), "src/v2/std/nat.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Nat".to_string(), "src/v2/std/nat.dag".to_string()) == None) } pub fn unknown_declaration_identity_refuses_rather_than_guessing() -> bool { - (rust_scalar_checkpoint_render_base("Nat".to_string(), "".to_string()) == None) + (rust_scalar_checkpoint_reference_base("Nat".to_string(), "".to_string()) == None) } pub fn residue_table_present_int_bypasses_identity() -> bool { - (rust_scalar_checkpoint_render_base("Int".to_string(), "src/v2/std/integer.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Int".to_string(), "src/v2/std/integer.dag".to_string()) .as_deref() == Some("i64".to_string()).as_deref()) } pub fn table_present_hash_refuses_under_structural_declaration() -> bool { - (rust_scalar_checkpoint_render_base("Hash".to_string(), "src/v2/std/node.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Hash".to_string(), "src/v2/std/node.dag".to_string()) == None) } pub fn table_present_string_refuses_under_structural_declaration_text() -> bool { - (rust_scalar_checkpoint_render_base("String".to_string(), "src/v2/std/text.dag".to_string()) + (rust_scalar_checkpoint_reference_base("String".to_string(), "src/v2/std/text.dag".to_string()) == None) } pub fn table_present_string_refuses_under_structural_declaration_string_type() -> bool { - (rust_scalar_checkpoint_render_base( + (rust_scalar_checkpoint_reference_base( "String".to_string(), "dag/std/string_type.dag".to_string(), ) == None) } pub fn table_present_bool_refuses_under_structural_declaration_logic() -> bool { - (rust_scalar_checkpoint_render_base("Bool".to_string(), "src/v2/std/logic.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Bool".to_string(), "src/v2/std/logic.dag".to_string()) == None) } pub fn table_present_bool_renders_natively_for_the_corpus_prelude() -> bool { - (rust_scalar_checkpoint_render_base("Bool".to_string(), "dag/std/types.dag".to_string()) + (rust_scalar_checkpoint_reference_base("Bool".to_string(), "dag/std/types.dag".to_string()) .as_deref() == Some("bool".to_string()).as_deref()) } @@ -101,3 +103,21 @@ pub fn literal_suffix_production_call_site_never_threads_declaration_identity() (literal_suffix(RenderTarget::Rust, "String".to_string(), "".to_string()).as_deref() == Some(".to_string()".to_string()).as_deref()) } + +pub fn reference_position_renders_the_bare_spelling() -> bool { + (rust_scalar_checkpoint_reference_base("String".to_string(), "dag/std/types.dag".to_string()) + .as_deref() + == Some("String".to_string()).as_deref()) +} + +pub fn declaration_position_renders_the_grounding_spelling() -> bool { + (rust_scalar_checkpoint_grounding_base("String".to_string(), "dag/std/types.dag".to_string()) + .as_deref() + == Some("std::string::String".to_string()).as_deref()) +} + +pub fn numeric_name_grounds_in_its_own_reference_spelling() -> bool { + (rust_scalar_checkpoint_grounding_base("Int".to_string(), "dag/std/integer.dag".to_string()) + .as_deref() + == Some("i64".to_string()).as_deref()) +} diff --git a/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag b/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag index 01ddf7f9b37..22f6b1a36ca 100644 --- a/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag +++ b/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag @@ -1,10 +1,10 @@ module v1.tests.claim.checkpoint_identity_keying_witness_test -import v1.compiler.emit_rust { rust_scalar_checkpoint_render_base } +import v1.compiler.emit_rust { rust_scalar_checkpoint_reference_base, rust_scalar_checkpoint_grounding_base } import v1.compiler.coercion { literal_suffix } import v1.compiler.artifact { Rust } -data checkpoint_identity_keying_witness_note: String = "EXECUTING evidence for the declaration-identity keying of Rust primitive realization, and for the checkpoint-table bypass that keying does NOT close.\n\nWHY THIS FILE EXISTS RATHER THAN THE ROWS IT REPLACES. The same assertions were authored as generated Rust in v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into src/v1/stage0/src/compiler_tests.rs. That module is declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate, while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package that consumes v1-compiler as an ordinary dependency -- so cfg(test) is never set for it and the module is not compiled, let alone run. Measured by execution rather than by reading: the binary that step builds enumerates 30 tests and none of them is this one, against a positive control confirming the enumeration is non-empty. The assertions were therefore authored, plausible, type-correct and NEVER EXECUTED, and v1.compiler.emit_rust checkpoint_table_bypasses_identity_note nonetheless cited them as the class's executing evidence. That is rung inflation in the disclosure of a ceiling -- the DESIGN section 4b(1) failure applied to the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The claim is repaired by making it TRUE here rather than by softening the sentence.\n\nWHAT DISCRIMINATES. rust_scalar_checkpoint_render_base takes a bare type name and the resolved declaration's ident_span file. The first four rows are the keying itself: a name with a table row renders from the table; a name WITHOUT one (Nat) reaches the identity arm and answers differently for two declarations that share a spelling -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag does not, and an EMPTY decl_file (identity unknown at the site) refuses rather than guessing. Those four cannot be satisfied together by any constant, by a disabled mechanism, or by a rule keyed on the name alone, which is precisely the property the deleted global corpus mode lacked.\n\nTHE RESIDUE ROWS ASSERT THE CURRENT BYPASSING ANSWERS ON PURPOSE. The table is keyed on the bare name and consulted BEFORE identity, so a table-present name bypasses declaration keying entirely: Int under a src/v2 path still renders i64 even though that declaration is GroupCompletion and not a machine integer. They are counted here rather than assumed closed. They FLIP to Absent when a name gets its own row in v1.compiler.coercion structural_declaration_modules_for, and that flip is the dissolution signal, NOT a regression -- do not make them pass again. Hash already made that flip: lookup_checkpoint (v1.compiler.coercion) now refuses before the bare-name table is consulted whenever decl_file names a module enrolled in structural_declaration_modules_for, and \"src/v2/std/node.dag\" is that module's one enrolled row, so table_present_hash_refuses_under_structural_declaration below is CLOSED rather than residue. String made the same flip in a later change: structural_declaration_modules_for now also enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which declare the structural FreeMonoid carrier rather than a host string, so table_present_string_refuses_under_structural_declaration_text and its _string_type sibling below are CLOSED and residue_table_present_string_bypasses_identity is retired rather than repaired back to passing. Bool was added in the same change -- structural_declaration_modules_for now also enrolls \"Bool\" => [\"src/v2/std/logic.dag\"], whose `type Bool = True | False` sits beside a BooleanAlgebra instance modeling machine-bool bit/width/encoding facts and so cannot shortcut to the primitive it derives, so table_present_bool_refuses_under_structural_declaration_logic below is CLOSED. dag/std/types.dag is NOT enrolled (see RE-GROUNDING NOTE 2): its `type Bool = True | False` is the ordinary corpus-wide prelude Bool, the genuine native declaring module parallel to dag/std/integer.dag for Int, so table_present_bool_renders_natively_for_the_corpus_prelude below asserts the positive answer instead. No residue_table_present_bool row ever existed in this file to retire. Int remains open -- it has no row yet -- and is exactly the residue population the next instance of this class inherits.\n\nWHERE THIS EXECUTES, STATED PRECISELY BECAUSE THE PREVIOUS CLAIM'S WHOLE DEFECT WAS AN IMPRECISE ONE. The row is enrolled in gunbc.ci_layer_roots v1_claim_scoped_witness_entries, consumed by v1_claim_scoped_witness_batch, whose source-root envelope is dag plus src/v1 -- the envelope this file needs, since it imports v1.compiler.emit_rust. The entry carries the empty function name, so it expands to every test fn here rather than pinning a roster of them. That batch runs SelectionApplied, so this witness executes on changes that affect it and emits a ScopedWitnessSelectionSkipped receipt with provenance otherwise; it is NOT claimed to run on every PR. That is the correct scope rather than a concession: evidence guarding a decision inside emit_rust should execute when emit_rust changes, and a provenance failure refuses loudly instead of widening. Note also what the enrollment is NOT: witness_discovery_scan_dirs is the owned-data-decl scope, not the witness scope, so membership there would neither add nor remove execution here. The assertions were additionally run directly during authoring -- all fourteen PASS -- but direct execution is evidence the assertions HOLD, never evidence that CI runs them, and conflating those two is the same class of error this file exists to repair.\n\nRE-GROUNDING NOTE (smart-ram-730 blocker, session merry-lark-67): the ORIGINAL String residue row here queried decl_file \"src/v2/std/string.dag\", a path that does not exist anywhere in the corpus -- its predicted flip to `none` was therefore structurally unreachable regardless of whether structural_declaration_modules_for was correct, and the row measured nothing. It is replaced, not repaired, by the two CLOSED rows above keyed on the REAL declarations (src/v2/std/text.dag, dag/std/string_type.dag), each asserting the strong `== none` shape the Hash flip already established rather than the weaker `!= none` the broken row used. Two further specimens close the packet: a positive control (literal_suffix_positive_control_symbol_not_enrolled) proving the gate is not a blanket refusal, since without one every refusal row below would be satisfied vacuously by a mechanism that refuses unconditionally; and literal_suffix -- a DIFFERENT consumer of lookup_checkpoint than rust_scalar_checkpoint_render_base, with its own return shape and its own production call site -- is exercised separately rather than inferred from the type-alias rows, and that direct execution surfaced a genuine, distinct disclosure: the literal-rendering call site in v1.compiler.05_emit emit_literal never threads a real decl_file (LitStr passes the empty string), so literal_suffix at PRODUCTION sites cannot be gated by this roster however correctly the roster and lookup_checkpoint discriminate when a real decl_file is supplied. That is measured directly below, not assumed from the declaration-site gap this note's sibling (checkpoint_table_bypasses_identity_note) already names.\n\nRE-GROUNDING NOTE 2 (CI blocker, session merry-lark-67, PR #8708 @ c084813): the ORIGINAL Bool enrollment listed BOTH src/v2/std/logic.dag AND dag/std/types.dag, mirroring String's two-row shape without checking whether either declaration was actually the genuine native one -- unlike String's two rows (text.dag, string_type.dag), neither of which is imported as the corpus's everyday String, dag/std/types.dag IS the corpus's everyday Bool: import std.types { Bool } appears in 300+ dag/test/claim modules. Enrolling it made lookup_checkpoint refuse native `bool` for every one of them, which the required-floor CI phase caught as five genuine (non-KNOWN-RED) failures in optional_carrier_signature_test.dag and e0308_mechanical_trio_test.dag -- fixtures that use `flag: Bool` as an incidental parameter and assert nothing about Bool's own realization, so the breakage was pure collateral, not a caught defect in those fixtures. The correction follows the numeric_realization_declaring_modules precedent (v1.compiler.emit_rust numeric_realization_roster_extension_note): a name belongs in the NEGATIVE structural roster only when none of its dag declarations is genuinely native, the way Hash's is purely coincidental spelling; a declaration that IS the grounded native one -- dag/std/integer.dag for Int, dag/std/types.dag for Bool -- must keep rendering from the table. dag/std/types.dag is removed from Bool's row; src/v2/std/logic.dag stays, since its BooleanAlgebra/BoolWidthFact/BoolEncodingFact modeling is a genuine structural encoding of what a bool bit-pattern is, not the everyday corpus type.\n\ndissolve-on: a corpus-side declaration-to-Rust-type binding supersedes the bare-name row, at which point the residue rows flip and this note's second half retires with them. The extdeps table keeps Rust-type-to-spelling (which is what its cited authority can answer); which dag declaration realizes as which Rust type is a gunbc-corpus fact and does not belong in an upstream row." +data checkpoint_identity_keying_witness_note: String = "EXECUTING evidence for the declaration-identity keying of Rust primitive realization, and for the checkpoint-table bypass that keying does NOT close.\n\nWHY THIS FILE EXISTS RATHER THAN THE ROWS IT REPLACES. The same assertions were authored as generated Rust in v1.compiler.compiler_tests_rust ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test, which emits into src/v1/stage0/src/compiler_tests.rs. That module is declared `#[cfg(test)] mod compiler_tests;` inside the v1-compiler crate, while the only test step CI runs is `cargo test -p v1-compiler-tests`, a SEPARATE package that consumes v1-compiler as an ordinary dependency -- so cfg(test) is never set for it and the module is not compiled, let alone run. Measured by execution rather than by reading: the binary that step builds enumerates 30 tests and none of them is this one, against a positive control confirming the enumeration is non-empty. The assertions were therefore authored, plausible, type-correct and NEVER EXECUTED, and v1.compiler.emit_rust checkpoint_table_bypasses_identity_note nonetheless cited them as the class's executing evidence. That is rung inflation in the disclosure of a ceiling -- the DESIGN section 4b(1) failure applied to the compiler's own self-description, which is worse than sitting low because an inflated class never ranks for climbing. The claim is repaired by making it TRUE here rather than by softening the sentence.\n\nWHAT DISCRIMINATES. rust_scalar_checkpoint_reference_base takes a bare type name and the resolved declaration's ident_span file. The first four rows are the keying itself: a name with a table row renders from the table; a name WITHOUT one (Nat) reaches the identity arm and answers differently for two declarations that share a spelling -- dag/std/nat.dag realizes natively, src/v2/std/nat.dag does not, and an EMPTY decl_file (identity unknown at the site) refuses rather than guessing. Those four cannot be satisfied together by any constant, by a disabled mechanism, or by a rule keyed on the name alone, which is precisely the property the deleted global corpus mode lacked.\n\nTHE RESIDUE ROWS ASSERT THE CURRENT BYPASSING ANSWERS ON PURPOSE. The table is keyed on the bare name and consulted BEFORE identity, so a table-present name bypasses declaration keying entirely: Int under a src/v2 path still renders i64 even though that declaration is GroupCompletion and not a machine integer. They are counted here rather than assumed closed. They FLIP to Absent when a name gets its own row in v1.compiler.coercion structural_declaration_modules_for, and that flip is the dissolution signal, NOT a regression -- do not make them pass again. Hash already made that flip: lookup_checkpoint (v1.compiler.coercion) now refuses before the bare-name table is consulted whenever decl_file names a module enrolled in structural_declaration_modules_for, and \"src/v2/std/node.dag\" is that module's one enrolled row, so table_present_hash_refuses_under_structural_declaration below is CLOSED rather than residue. String made the same flip in a later change: structural_declaration_modules_for now also enrolls \"String\" => [\"src/v2/std/text.dag\", \"dag/std/string_type.dag\"], both of which declare the structural FreeMonoid carrier rather than a host string, so table_present_string_refuses_under_structural_declaration_text and its _string_type sibling below are CLOSED and residue_table_present_string_bypasses_identity is retired rather than repaired back to passing. Bool was added in the same change -- structural_declaration_modules_for now also enrolls \"Bool\" => [\"src/v2/std/logic.dag\"], whose `type Bool = True | False` sits beside a BooleanAlgebra instance modeling machine-bool bit/width/encoding facts and so cannot shortcut to the primitive it derives, so table_present_bool_refuses_under_structural_declaration_logic below is CLOSED. dag/std/types.dag is NOT enrolled (see RE-GROUNDING NOTE 2): its `type Bool = True | False` is the ordinary corpus-wide prelude Bool, the genuine native declaring module parallel to dag/std/integer.dag for Int, so table_present_bool_renders_natively_for_the_corpus_prelude below asserts the positive answer instead. No residue_table_present_bool row ever existed in this file to retire. Int remains open -- it has no row yet -- and is exactly the residue population the next instance of this class inherits.\n\nWHERE THIS EXECUTES, STATED PRECISELY BECAUSE THE PREVIOUS CLAIM'S WHOLE DEFECT WAS AN IMPRECISE ONE. The row is enrolled in gunbc.ci_layer_roots v1_claim_scoped_witness_entries, consumed by v1_claim_scoped_witness_batch, whose source-root envelope is dag plus src/v1 -- the envelope this file needs, since it imports v1.compiler.emit_rust. The entry carries the empty function name, so it expands to every test fn here rather than pinning a roster of them. That batch runs SelectionApplied, so this witness executes on changes that affect it and emits a ScopedWitnessSelectionSkipped receipt with provenance otherwise; it is NOT claimed to run on every PR. That is the correct scope rather than a concession: evidence guarding a decision inside emit_rust should execute when emit_rust changes, and a provenance failure refuses loudly instead of widening. Note also what the enrollment is NOT: witness_discovery_scan_dirs is the owned-data-decl scope, not the witness scope, so membership there would neither add nor remove execution here. The assertions were additionally run directly during authoring -- all fourteen PASS -- but direct execution is evidence the assertions HOLD, never evidence that CI runs them, and conflating those two is the same class of error this file exists to repair.\n\nRE-GROUNDING NOTE (smart-ram-730 blocker, session merry-lark-67): the ORIGINAL String residue row here queried decl_file \"src/v2/std/string.dag\", a path that does not exist anywhere in the corpus -- its predicted flip to `none` was therefore structurally unreachable regardless of whether structural_declaration_modules_for was correct, and the row measured nothing. It is replaced, not repaired, by the two CLOSED rows above keyed on the REAL declarations (src/v2/std/text.dag, dag/std/string_type.dag), each asserting the strong `== none` shape the Hash flip already established rather than the weaker `!= none` the broken row used. Two further specimens close the packet: a positive control (literal_suffix_positive_control_symbol_not_enrolled) proving the gate is not a blanket refusal, since without one every refusal row below would be satisfied vacuously by a mechanism that refuses unconditionally; and literal_suffix -- a DIFFERENT consumer of lookup_checkpoint than rust_scalar_checkpoint_reference_base, with its own return shape and its own production call site -- is exercised separately rather than inferred from the type-alias rows, and that direct execution surfaced a genuine, distinct disclosure: the literal-rendering call site in v1.compiler.05_emit emit_literal never threads a real decl_file (LitStr passes the empty string), so literal_suffix at PRODUCTION sites cannot be gated by this roster however correctly the roster and lookup_checkpoint discriminate when a real decl_file is supplied. That is measured directly below, not assumed from the declaration-site gap this note's sibling (checkpoint_table_bypasses_identity_note) already names.\n\nRE-GROUNDING NOTE 2 (CI blocker, session merry-lark-67, PR #8708 @ c084813): the ORIGINAL Bool enrollment listed BOTH src/v2/std/logic.dag AND dag/std/types.dag, mirroring String's two-row shape without checking whether either declaration was actually the genuine native one -- unlike String's two rows (text.dag, string_type.dag), neither of which is imported as the corpus's everyday String, dag/std/types.dag IS the corpus's everyday Bool: import std.types { Bool } appears in 300+ dag/test/claim modules. Enrolling it made lookup_checkpoint refuse native `bool` for every one of them, which the required-floor CI phase caught as five genuine (non-KNOWN-RED) failures in optional_carrier_signature_test.dag and e0308_mechanical_trio_test.dag -- fixtures that use `flag: Bool` as an incidental parameter and assert nothing about Bool's own realization, so the breakage was pure collateral, not a caught defect in those fixtures. The correction follows the numeric_realization_declaring_modules precedent (v1.compiler.emit_rust numeric_realization_roster_extension_note): a name belongs in the NEGATIVE structural roster only when none of its dag declarations is genuinely native, the way Hash's is purely coincidental spelling; a declaration that IS the grounded native one -- dag/std/integer.dag for Int, dag/std/types.dag for Bool -- must keep rendering from the table. dag/std/types.dag is removed from Bool's row; src/v2/std/logic.dag stays, since its BooleanAlgebra/BoolWidthFact/BoolEncodingFact modeling is a genuine structural encoding of what a bool bit-pattern is, not the everyday corpus type.\n\ndissolve-on: a corpus-side declaration-to-Rust-type binding supersedes the bare-name row, at which point the residue rows flip and this note's second half retires with them. The extdeps table keeps Rust-type-to-spelling (which is what its cited authority can answer); which dag declaration realizes as which Rust type is a gunbc-corpus fact and does not belong in an upstream row." // --------------------------------------------------------------------------- // The keying itself. Four answers, one function, three distinct outcomes. @@ -12,14 +12,14 @@ data checkpoint_identity_keying_witness_note: String = "EXECUTING evidence for t // A table-present name renders from the table. test fn table_present_name_renders_from_the_table() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Int", decl_file: "dag/std/integer.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Int", decl_file: "dag/std/integer.dag") == Present { value: "i64" } } // A table-ABSENT name reaches the identity arm and realizes natively for the // std declaration. test fn table_absent_name_realizes_natively_for_the_std_declaration() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Nat", decl_file: "dag/std/nat.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Nat", decl_file: "dag/std/nat.dag") == Present { value: "i64" } } @@ -28,14 +28,14 @@ test fn table_absent_name_realizes_natively_for_the_std_declaration() -> Bool { // integer. A rule keyed on the name alone cannot pass this and the previous row // together -- which is exactly what the deleted global corpus mode could not do. test fn same_spelling_different_declaration_does_not_realize_natively() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Nat", decl_file: "src/v2/std/nat.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Nat", decl_file: "src/v2/std/nat.dag") == none } // Identity UNKNOWN at the site refuses rather than guessing. The empty decl_file // is not a third realization, it is the absence of the fact the decision needs. test fn unknown_declaration_identity_refuses_rather_than_guessing() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Nat", decl_file: "") + rust_scalar_checkpoint_reference_base(dag_name: "Nat", decl_file: "") == none } @@ -48,7 +48,7 @@ test fn unknown_declaration_identity_refuses_rather_than_guessing() -> Bool { // --------------------------------------------------------------------------- test fn residue_table_present_int_bypasses_identity() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Int", decl_file: "src/v2/std/integer.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Int", decl_file: "src/v2/std/integer.dag") == Present { value: "i64" } } @@ -90,27 +90,27 @@ test fn residue_table_present_int_bypasses_identity() -> Bool { // --------------------------------------------------------------------------- test fn table_present_hash_refuses_under_structural_declaration() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Hash", decl_file: "src/v2/std/node.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Hash", decl_file: "src/v2/std/node.dag") == none } test fn table_present_string_refuses_under_structural_declaration_text() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "String", decl_file: "src/v2/std/text.dag") + rust_scalar_checkpoint_reference_base(dag_name: "String", decl_file: "src/v2/std/text.dag") == none } test fn table_present_string_refuses_under_structural_declaration_string_type() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "String", decl_file: "dag/std/string_type.dag") + rust_scalar_checkpoint_reference_base(dag_name: "String", decl_file: "dag/std/string_type.dag") == none } test fn table_present_bool_refuses_under_structural_declaration_logic() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Bool", decl_file: "src/v2/std/logic.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Bool", decl_file: "src/v2/std/logic.dag") == none } test fn table_present_bool_renders_natively_for_the_corpus_prelude() -> Bool { - rust_scalar_checkpoint_render_base(dag_name: "Bool", decl_file: "dag/std/types.dag") + rust_scalar_checkpoint_reference_base(dag_name: "Bool", decl_file: "dag/std/types.dag") == Present { value: "bool" } } @@ -139,7 +139,7 @@ test fn literal_suffix_positive_control_symbol_not_enrolled() -> Bool { } // literal_suffix refuses for String under EITHER real structural declaration, -// exactly like rust_scalar_checkpoint_render_base above -- the same gate, a +// exactly like rust_scalar_checkpoint_reference_base above -- the same gate, a // different consumer, its own executed specimen per declaration identity. test fn literal_suffix_refuses_under_structural_declaration_text() -> Bool { literal_suffix(target: Rust, dag_name: "String", decl_file: "src/v2/std/text.dag") @@ -170,3 +170,82 @@ test fn literal_suffix_production_call_site_never_threads_declaration_identity() literal_suffix(target: Rust, dag_name: "String", decl_file: "") == Present { value: ".to_string()" } } + +// --------------------------------------------------------------------------- +// WHERE THE THREE ROWS BELOW EXECUTE, AND WHERE THEY DO NOT. They were run +// directly during authoring -- green, plus a discriminating RED that fails at +// the grounding assertion specifically while both reference assertions pass -- +// and that is evidence the assertions HOLD. It is NOT evidence that CI runs +// them, and conflating the two is the error the note at the top of this file +// exists to repair. +// +// They are NOT ENROLLED. The required-CI invocation is +// `claim_executor --required-ci --source-root dag --source-root src/v2`, and +// this file lives under src/v1, which is outside that envelope -- the same +// reason the migration note above gives for the rows it could not carry across. +// So the standing evidence for the two-role split is on-demand, not executing, +// and DESIGN section 4b(4) -- the discriminating RED remains enrolled as the +// evidence that the higher rung stays real -- does not hold for these rows yet. +// +// AND THE MECHANISM IS NOT MERELY AN ENVELOPE THAT NEVER INCLUDED THEM. The +// consumer that DID run v1 claim entries -- the scoped witness batch, the only +// ScopedWitnessBatch instance that ever existed, under a dag plus src/v1 envelope +// -- was DELETED 2026-08-15 (gunbc.ci_layer_roots +// v1_claim_scoped_witness_batch_deleted_note, which also carries triage receipts +// for seventeen other v1 witness files retired for this same root). These rows +// are therefore enrolled against a consumer that no longer exists, which is a +// worse state than being outside a live envelope: nothing refuses, because +// nothing is asking. +// +// This is declared rather than left to be rediscovered, per 4b(2)'s no-untracked- +// stall rule. NEXT-RUNG TRIGGER, AND THE OBVIOUS ONE IS RULED OUT: it is NOT +// "widen the required-CI envelope to include src/v1". That restore was measured +// and refused, and the reason was re-measured 2026-08-19 when the original went +// stale -- the blocker is no longer cost (preparation completes in ~9 minutes) +// but NAME RESOLUTION: src/v1 and src/v2 share no exact module path yet collide +// on the LAST SEGMENT in twelve places (artifact, coercion, common, compile, +// complexity, emit, infer, normalize, ownership, parse, resolve, tokenize), so +// admitting src/v1 supplies a second module whose last segment matches and bare +// cross-module references that resolve today by pool-membership coincidence stop +// resolving. The damage is in what is ALREADY there, not in what is admitted: +// of 532 typed diagnostics, 525 were in src/v2 and 7 in dag/test -- ZERO in +// src/v1. The real trigger is therefore bare cross-module references binding BY +// CONTAINMENT rather than by pool coincidence, whose current vehicle is the +// namespace cut (gunbc#8282, crisp-crab-430) -- explicitly not the floor getting +// faster and not the envelope widening. +// +// Re-homing is not free and is not done here: the rows +// import v1.compiler.emit_rust directly, and the dag/ sibling of this file can +// only observe the emitter black-box through compile_dag_rust_emit_check, which +// is a weaker instrument -- it sees rendered output, not the function's answer. +// Moving them there would silently downgrade what they discriminate. +// +// --------------------------------------------------------------------------- +// THE TWO-ROLE SPLIT, EXECUTED. One TypeCheckpoint row was answering two +// questions -- what a REFERENCE renders and what a DECLARATION's right-hand +// side is GROUNDED IN -- and for String those answers differ: a reference +// renders the bare `String`, while the declaration `pub type String = String;` +// is self-referential and does not compile. The two rows below are the pair +// that no single field can satisfy: they call the same identity-keyed body +// with the same name and the same decl_file and require different answers. +// If the split is ever collapsed back to one field, exactly one of them goes +// red, whichever field survives. +// --------------------------------------------------------------------------- + +test fn reference_position_renders_the_bare_spelling() -> Bool { + rust_scalar_checkpoint_reference_base(dag_name: "String", decl_file: "dag/std/types.dag") + == Present { value: "String" } +} + +test fn declaration_position_renders_the_grounding_spelling() -> Bool { + rust_scalar_checkpoint_grounding_base(dag_name: "String", decl_file: "dag/std/types.dag") + == Present { value: "std::string::String" } +} + +// The split does not fork the NUMERIC names: their grounding spelling is their +// reference spelling, and stating that by execution keeps the new field from +// being read as a second authority that could drift row by row. +test fn numeric_name_grounds_in_its_own_reference_spelling() -> Bool { + rust_scalar_checkpoint_grounding_base(dag_name: "Int", decl_file: "dag/std/integer.dag") + == Present { value: "i64" } +}