From b20ae09efedaf2d30f2bd3f5e0f54d50ce5622f7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 02:47:04 +0000 Subject: [PATCH 1/4] Retire std.string_type String: delete dag/std/string_type.dag (0 importers) Operator-ruled retirement of the duplicate structural declaration (String = FreeMonoid) beside v2.std.text String, after gunbc#12512 deleted its 81 host-text importers. Consumers updated in the same motion: v1.compiler.coercion structural_declaration_modules_for drops the path; the symbol-identity witness drops its sibling citation; the de-fork census moves the String row to resolved via a new ResolvedByDeletingDag arm. Stage0 regenerated to fixed point. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/defork_type_name_census.dag | 16 +++++++--------- dag/std/string_type.dag | 15 --------------- ...host_symbol_identity_binding_witness_test.dag | 5 ++--- src/v1/coercion.dag | 2 +- src/v1/stage0/src/v1_compiler_coercion.rs | 5 +---- 5 files changed, 11 insertions(+), 32 deletions(-) delete mode 100644 dag/std/string_type.dag diff --git a/dag/gunbc/defork_type_name_census.dag b/dag/gunbc/defork_type_name_census.dag index 17a3d236536..34ebbe391b7 100644 --- a/dag/gunbc/defork_type_name_census.dag +++ b/dag/gunbc/defork_type_name_census.dag @@ -111,6 +111,7 @@ type SharedTypeNameRow { type ForkResolution = ResolvedByRenamingV2 { renamed_to: String, citation: String } | ResolvedByDeletingV2 { reason: String } + | ResolvedByDeletingDag { reason: String } | ResolvedByRenamingDag { renamed_to: String, citation: String } | ResolvedByRehomingBothToExtdeps { authority: String, citation: String } @@ -190,15 +191,6 @@ data defork_census_rows: List = [ }, disposition: ForkOpen { reason: "next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`)" } }, - SharedTypeNameRow { - names: ["String"], - reading: AuthoredResolutionReading { - dag_side: "`= FreeMonoid` → `std.algebra` `FreeMonoid`, `std.types` `Char`", - v2_side: "`v2.std.text` `String`: same referents; `v2.std.node` `String`: opaque kernel host text (gunbc#12760), a different type under the same name, bound only where no other String declaration is visible", - class: "the structural pair is one concept, two declarations (duplicate); the v2.std.node host-text String is a distinct concept, not a third copy (gunbc.recurring_failure_mode carrier_by_spelling)" - }, - disposition: ForkAwaitingRuling { question: "seed kernel name — out of scope for the wave" } - }, SharedTypeNameRow { names: ["List"], reading: AuthoredResolutionReading { @@ -274,6 +266,11 @@ data defork_census_rows: List = [ ] data defork_census_resolved: List = [ + ResolvedSharedTypeName { + names: ["String"], + resolution: ResolvedByDeletingDag { reason: "operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling)" }, + change: 0 + }, ResolvedSharedTypeName { names: ["Nat"], resolution: ResolvedByDeletingV2 { reason: "operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance" }, @@ -340,6 +337,7 @@ fn census_resolution_text(r: ForkResolution) -> String { match r { ResolvedByRenamingV2 { renamed_to, citation } => concat(concat(concat("v2 side renamed `", renamed_to), "` — "), citation) ResolvedByDeletingV2 { reason } => concat("v2 side deleted — ", reason) + ResolvedByDeletingDag { reason } => concat("dag side deleted — ", reason) ResolvedByRenamingDag { renamed_to, citation } => concat(concat(concat("dag side renamed `", renamed_to), "` — "), citation) ResolvedByRehomingBothToExtdeps { authority, citation } => concat(concat(concat("both sides deleted; the concept is homed at `", authority), "` — "), citation) } diff --git a/dag/std/string_type.dag b/dag/std/string_type.dag deleted file mode 100644 index b7a4926a573..00000000000 --- a/dag/std/string_type.dag +++ /dev/null @@ -1,15 +0,0 @@ -module std.string_type - -import std.algebra { FreeMonoid } -import std.types { Char } - -// A DECLARED FRONTIER, NOT A CONSUMED TYPE (DESIGN section 3c). This declaration grounds -// String = FreeMonoid -- strings over an alphabet are the free monoid -- per operator Ruling 3 -// (2026-07-15, cited at std.coercion beside grounded_primitive_coproduct_identities). It has no -// importer: the 71 modules that imported it treated the value as host text and now bind the kernel -// String, and its two lexicographic functions were deleted because host String ordering (`<`) is -// already that order (gunbc.rung_drop text_boundary_identity_wall). The open seed kernel-names -// de-fork ruling (String/Bool/Float/List) retires this declaration or promotes it; until then it -// stays, and the structural roster (v1.compiler.coercion structural_declaration_modules_for) keeps -// it a code-point sequence. -type String = FreeMonoid diff --git a/dag/test/claim/self_host_symbol_identity_binding_witness_test.dag b/dag/test/claim/self_host_symbol_identity_binding_witness_test.dag index 66d9aefa43a..d70e6fee848 100644 --- a/dag/test/claim/self_host_symbol_identity_binding_witness_test.dag +++ b/dag/test/claim/self_host_symbol_identity_binding_witness_test.dag @@ -62,14 +62,13 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // THE SAME-SPELLING SIBLINGS, all REAL declarations (the cited-declaration gate refuses a citation // of a declaration that does not exist, so the "another module declaring Symbol" falsifier is -// asked of the declarations the corpus actually has two of): v2.std.text String and std.string_type -// String beside the kernel String row, v2.std.logic Bool beside std.types Bool (which HAS an exact +// asked of the declarations the corpus actually has two of): v2.std.text String beside the kernel +// String row, v2.std.logic Bool beside std.types Bool (which HAS an exact // row), and v2.std.node Hash, declared in Symbol's own module one line below it. None may receive a // binding authored for a different declaration -- module-path and decl-name discrimination both. fn sibling_declarations_without_bindings() -> List { [ decl_ref(module_path: "v2.std.text", decl_name: "String"), - decl_ref(module_path: "std.string_type", decl_name: "String"), decl_ref(module_path: "v2.std.logic", decl_name: "Bool"), decl_ref(module_path: "v2.std.node", decl_name: "Hash") ] diff --git a/src/v1/coercion.dag b/src/v1/coercion.dag index 9c960d693bb..4c266ddf812 100644 --- a/src/v1/coercion.dag +++ b/src/v1/coercion.dag @@ -136,7 +136,7 @@ data type_reference_identity_note: String = "A realization decision is made at R fn structural_declaration_modules_for(dag_name: String) -> List { match dag_name { "Hash" => ["src/v2/std/node.dag"] - "String" => ["src/v2/std/text.dag", "dag/std/string_type.dag"] + "String" => ["src/v2/std/text.dag"] "Bool" => ["src/v2/std/logic.dag"] _ => [] } diff --git a/src/v1/stage0/src/v1_compiler_coercion.rs b/src/v1/stage0/src/v1_compiler_coercion.rs index cb4831838f3..9dda3c52fe7 100644 --- a/src/v1/stage0/src/v1_compiler_coercion.rs +++ b/src/v1/stage0/src/v1_compiler_coercion.rs @@ -168,10 +168,7 @@ pub fn type_reference_identity_note() -> String { pub fn structural_declaration_modules_for(dag_name: String) -> Rc> { match dag_name.clone().as_str() { "Hash" => Rc::new(vec!["src/v2/std/node.dag".to_string()]), - "String" => Rc::new(vec![ - "src/v2/std/text.dag".to_string(), - "dag/std/string_type.dag".to_string(), - ]), + "String" => Rc::new(vec!["src/v2/std/text.dag".to_string()]), "Bool" => Rc::new(vec!["src/v2/std/logic.dag".to_string()]), _ => Rc::new(vec![]), } From 3f60f1d1e6a2b538ae2e3190a53d9008bc53f5fa Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 07:10:09 +0000 Subject: [PATCH 2/4] Delete the two v1 checkpoint claims whose subject was dag/std/string_type.dag Both sent the deleted path through structural_declaration_modules_for and asserted the structural refusal; with the path gone from the roster they have no subject. The v2.std.text sibling claims keep covering the refusal. Co-Authored-By: Claude Opus 5.5 (1M context) --- ...checkpoint_identity_keying_witness_test.rs | 24 ------------------- ...heckpoint_identity_keying_witness_test.dag | 10 -------- 2 files changed, 34 deletions(-) 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 4960b39f4e6..68c6dad6590 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 @@ -113,18 +113,6 @@ pub fn table_present_string_refuses_under_structural_declaration_text() -> bool ) == std::option::Option::None) } -pub fn table_present_string_refuses_under_structural_declaration_string_type() -> bool { - (crate::v1_compiler_emit_rust::rust_scalar_checkpoint_reference_base( - crate::v1_compiler_coercion::type_realization_decision( - RenderTarget::Rust, - "String".to_string(), - Rc::new(TypeDeclarationProvenance::CorpusDeclared { - decl_file: "dag/std/string_type.dag".to_string(), - }), - ), - ) == std::option::Option::None) -} - pub fn table_present_bool_refuses_under_structural_declaration_logic() -> bool { (crate::v1_compiler_emit_rust::rust_scalar_checkpoint_reference_base( crate::v1_compiler_coercion::type_realization_decision( @@ -175,18 +163,6 @@ pub fn literal_suffix_refuses_under_structural_declaration_text() -> bool { ) == std::option::Option::None) } -pub fn literal_suffix_refuses_under_structural_declaration_string_type() -> bool { - (crate::v1_compiler_coercion::literal_suffix( - crate::v1_compiler_coercion::type_realization_decision( - RenderTarget::Rust, - "String".to_string(), - Rc::new(TypeDeclarationProvenance::CorpusDeclared { - decl_file: "dag/std/string_type.dag".to_string(), - }), - ), - ) == std::option::Option::None) -} - pub fn literal_suffix_production_call_site_never_threads_declaration_identity() -> bool { (crate::v1_compiler_coercion::literal_suffix( crate::v1_compiler_coercion::type_realization_decision( 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 eed8c701457..1d91b8ca076 100644 --- a/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag +++ b/src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag @@ -127,11 +127,6 @@ test fn table_present_string_refuses_under_structural_declaration_text() -> Bool == none } -test fn table_present_string_refuses_under_structural_declaration_string_type() -> Bool { - rust_scalar_checkpoint_reference_base(decision: type_realization_decision(target: Rust, dag_name: "String", provenance: CorpusDeclared { decl_file: "dag/std/string_type.dag" })) - == none -} - test fn table_present_bool_refuses_under_structural_declaration_logic() -> Bool { rust_scalar_checkpoint_reference_base(decision: type_realization_decision(target: Rust, dag_name: "Bool", provenance: CorpusDeclared { decl_file: "src/v2/std/logic.dag" })) == none @@ -174,11 +169,6 @@ test fn literal_suffix_refuses_under_structural_declaration_text() -> Bool { == none } -test fn literal_suffix_refuses_under_structural_declaration_string_type() -> Bool { - literal_suffix(decision: type_realization_decision(target: Rust, dag_name: "String", provenance: CorpusDeclared { decl_file: "dag/std/string_type.dag" })) - == none -} - // THE DISCLOSED GAP, EXECUTED RATHER THAN ASSERTED IN PROSE: the real call // site in emit_literal passes decl_file: "" for every String literal, and an // empty decl_file can never satisfy decl_file_declares_structurally (it From 1d673232f50cbce35db2c64a6636bd2cc7ffaf27 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 07:14:55 +0000 Subject: [PATCH 3/4] De-fork census: String row change number 13089 Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/defork_type_name_census.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/defork_type_name_census.dag b/dag/gunbc/defork_type_name_census.dag index 34ebbe391b7..0d301573d10 100644 --- a/dag/gunbc/defork_type_name_census.dag +++ b/dag/gunbc/defork_type_name_census.dag @@ -269,7 +269,7 @@ data defork_census_resolved: List = [ ResolvedSharedTypeName { names: ["String"], resolution: ResolvedByDeletingDag { reason: "operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling)" }, - change: 0 + change: 13089 }, ResolvedSharedTypeName { names: ["Nat"], From 77de1e93df86a4d110092df3497cae3a79030d4e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 08:42:05 +0000 Subject: [PATCH 4/4] Regenerate docs/plans/dag-v2-defork-audit.md (String row resolved) via generated_artifact_gate main_wet Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/plans/dag-v2-defork-audit.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/plans/dag-v2-defork-audit.md b/docs/plans/dag-v2-defork-audit.md index 358be33cf94..2ca50f50fb9 100644 --- a/docs/plans/dag-v2-defork-audit.md +++ b/docs/plans/dag-v2-defork-audit.md @@ -192,12 +192,11 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a ## 2D. The shared type-name census (the one list): the population is derived, the dispositions are authored -**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **23 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`. +**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **22 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`. | name(s) | declared in (derived) | dag/std side (authored reading) | src/v2/std side (authored reading) | class (authored) | disposition | | --- | --- | --- | --- | --- | --- | | `NonNegativeInt`, `PositiveInt` | `dag/std/integer.dag`, `src/v2/std/refinement.dag` | `std.integer` — `= Nat` / `= Nat where gt_zero` (refinement of `std.nat` `Nat`) | `v2.std.refinement` — record `refined: Refined` (smart-constructor over `v2.std.integer` `Int`), consumed by the formatter extdeps | MEANING FORK | OPEN — next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`) | -| `String` | `dag/std/string_type.dag`, `src/v2/std/node.dag`, `src/v2/std/text.dag` | `= FreeMonoid` → `std.algebra` `FreeMonoid`, `std.types` `Char` | `v2.std.text` `String`: same referents; `v2.std.node` `String`: opaque kernel host text (gunbc#12760), a different type under the same name, bound only where no other String declaration is visible | the structural pair is one concept, two declarations (duplicate); the v2.std.node host-text String is a distinct concept, not a third copy (gunbc.recurring_failure_mode carrier_by_spelling) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave | | `List` | `dag/std/types.dag`, `src/v2/std/collection.dag` | `= FreeMonoid` → `std.algebra` `FreeMonoid` | `= std.algebra.FreeMonoid` → same | one concept, two declarations (duplicate) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave | | `Bool` | `dag/std/types.dag`, `src/v2/std/logic.dag` | `std.types` `= True \| False` | `v2.std.logic` `= True \| False` (arms are two more same-name declarations) | one concept, two declarations (duplicate) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave | | `Int`, `UInt` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.nat` `Nat` (via `std.algebra` `GroupCompletion`) | → `v2.std.nat` `Nat` | same concept, divergent referent | NEEDS A DECISION RECORD (integer family) | @@ -211,6 +210,7 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a | name(s) | resolution | change | | --- | --- | --- | +| `String` | dag side deleted — operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling) | #13089 | | `Nat` | v2 side deleted — operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance | #12846 | | `Float` | both sides deleted; the concept is homed at `extdeps.standards.ieee_754_2019 binary64` — IEEE 754-2019 §3.6 (operator ruling relayed 2026-09-28): `std.float` (Float = Float64, uncited) and `v2.std.float` (Float = Binary64) both deleted; kernel Float's meaning is the `std.kernel_type_denotation` row, not a std alias | #12547 | | `ProjectionKind` | v2 side deleted — `v2.std.projection` (compiler lens kinds) had zero importers; `std.planar_projection` keeps the name for drawing views | #12252 |