Skip to content

Split the checkpoint row's two spelling roles: what a reference renders and what a declaration grounds in #8788

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
briansrls merged 8 commits into from
Aug 21, 2026
Merged

Split the checkpoint row's two spelling roles: what a reference renders and what a declaration grounds in #8788

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
307ebb6
Split the checkpoint row's arity: a reference spelling and a groundin…
Aug 21, 2026
383421e
Merge remote-tracking branch 'origin/main' into session/sharp-carp-19…
Aug 21, 2026
d39ed5d
Narrow the construction claim to the rung the code holds: the shared …
Aug 21, 2026
af48f32
Adopt the regenerated mirrors: the emitter's own bytes, not my hand-w…
Aug 21, 2026
ad5855a
Say "two spelling roles", not "arity": that word already means parame…
Aug 21, 2026
486478b
Absorb main: merge two prose findings about String rather than pickin…
Aug 21, 2026
c35c144
Declare that the split's witness rows are executed but NOT enrolled
Aug 21, 2026
6e8276e
Point the trigger at containment binding, not an envelope widening th…
Aug 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions dag/extdeps/languages/dag/types.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}

data dag_type_checkpoints: List<TypeCheckpoint> = [
{ 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 }
]
16 changes: 8 additions & 8 deletions dag/extdeps/languages/go/types.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}

data go_type_checkpoints: List<TypeCheckpoint> = [
{ 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<InhabitantDecl> = [
Expand Down
16 changes: 8 additions & 8 deletions dag/extdeps/languages/python/types.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}

data python_type_checkpoints: List<TypeCheckpoint> = [
{ 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<InhabitantDecl> = [
Expand Down
20 changes: 10 additions & 10 deletions dag/extdeps/languages/rust/types.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,20 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}

data rust_type_checkpoints: List<TypeCheckpoint> = [
{ 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<u8>", 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<u8>", grounding_type: "Vec<u8>", 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<Fnv1a64Structural>, 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<C> (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<T> in type position and emit `Rc<Witness>` — 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<C> (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<T> in type position and emit `Rc<Witness>` — 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<InhabitantDecl> = [

Expand Down
16 changes: 8 additions & 8 deletions dag/extdeps/languages/typescript/types.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}

data ts_type_checkpoints: List<TypeCheckpoint> = [
{ 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<InhabitantDecl> = [
Expand Down
66 changes: 66 additions & 0 deletions dag/gunbc/empty_decl_file_checkpoint_bypass.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<BypassInstance> = [
{
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")
Loading