From 188b92415d64214b6cd0a768ff7c3bbae54f6333 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 23:02:47 -0400 Subject: [PATCH 01/12] =?UTF-8?q?WIP:=20T-30=20=E2=80=94=20generated=20hol?= =?UTF-8?q?low-alias=20.dag=20checker=20(Node->Outcome=20fail-closed;=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/std/fact_density.dag | 149 +++++++++++++++++- .../test/claim/manual/fact_density_anchor.dag | 80 ++++++++++ 2 files changed, 224 insertions(+), 5 deletions(-) create mode 100644 src/v4/test/claim/manual/fact_density_anchor.dag diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index 89507fd3bfc..1e658750326 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -1,10 +1,149 @@ // src/v4/std/fact_density.dag -// Scope: P2-staging substrate witness. -// Owns: SourceSpecReadFact -// Consumes: -// Status: drafted. -// Anchor: https://github.com/gunb-ai/gunbc/blob/main/INVARIANTS.md +// Scope: T-30 generated structural hollow-alias checker β€” a pure Node -> Outcome gate that fails closed on a carrier reading zero spec facts. +// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, density_fact, connective_spec_fact, carrier_spec_fact, carrier_is_hollow, fact_density_hollow_alias, hollow_alias_diagnostic, hollow_alias_gate, module_no_hollow_alias. +// Consumes: std node, std diagnostic. +// Status: T-30 generated checker; P2-staging until operator-closure wires pipeline enforcement. +// Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md module v4.std.fact_density + +import v4.std.node { + Node, + Connective, + Atom, + Conj, + Disj, + Arrow, + Cardinality, + Instantiation, + TypeNode, + ComputationNode, + Symbol +} +import v4.std.diagnostic { + Outcome, + Produced, + Rejected, + Diagnostic, + NodeLocus, + Unavailable, + UserInputBoundary +} + + +// Kernel-ambient atom identities (STRUCTURE.md "Kernel-ambient types"): +// String / Int / Bool / Char / List / Map are irreducible substrate atoms β€” +// a carrier aliasing one of them is legitimately atomic, not hollow. +data fact_density_kernel_ambient_string: Symbol = String +data fact_density_kernel_ambient_int: Symbol = Int +data fact_density_kernel_ambient_bool: Symbol = Bool +data fact_density_kernel_ambient_char: Symbol = Char +data fact_density_kernel_ambient_list: Symbol = List +data fact_density_kernel_ambient_map: Symbol = Map + + +fn symbol_is_kernel_ambient(s: Symbol) -> Bool { + s == fact_density_kernel_ambient_string || + s == fact_density_kernel_ambient_int || + s == fact_density_kernel_ambient_bool || + s == fact_density_kernel_ambient_char || + s == fact_density_kernel_ambient_list || + s == fact_density_kernel_ambient_map +} + + +// 🟒 coproduct dissolution β€” what a carrier reads from its source spec. +// NoFact is the hollow alias: a carrier that decomposes into zero spec-read +// facts and is not an exempt kernel-ambient atom. type SourceSpecReadFact + = NamedFieldFacts { density: Int } + | KernelAmbientAtom { atom: Symbol } + | NoFact + + +// Fact-density read: a carrier with >= 1 own fact-edge records that many +// spec-read facts; zero own fact-edges is the hollow shape. +fn density_fact(child_count: Int) -> SourceSpecReadFact { + if child_count == 0 { + NoFact + } else { + NamedFieldFacts { density: child_count } + } +} + + +// A bare alias `type X = Y` lowers to an Atom carrier with zero own +// fact-edges: hollow unless its identity is kernel-ambient. Conj / Disj / +// Arrow / Cardinality / Instantiation carriers read facts iff they carry +// own child edges. +fn connective_spec_fact(c: Connective, child_count: Int) -> SourceSpecReadFact { + match c { + Atom { identity: id } => + if symbol_is_kernel_ambient(s: id) { + KernelAmbientAtom { atom: id } + } else { + density_fact(child_count: child_count) + } + Conj => density_fact(child_count: child_count) + Disj => density_fact(child_count: child_count) + Arrow => density_fact(child_count: child_count) + Cardinality => density_fact(child_count: child_count) + Instantiation => density_fact(child_count: child_count) + } +} + + +// The spec facts a type carrier reads. Computation nodes are not type +// carriers β€” the hollow-alias concept does not apply, so they read a +// non-hollow result by construction. +fn carrier_spec_fact(carrier: Node) -> SourceSpecReadFact { + match carrier.kind { + TypeNode { connective: c } => + connective_spec_fact(c: c, child_count: count(carrier.children)) + ComputationNode { behavior: _ } => + KernelAmbientAtom { atom: fact_density_kernel_ambient_bool } + } +} + + +fn carrier_is_hollow(carrier: Node) -> Bool { + match carrier_spec_fact(carrier: carrier) { + NoFact => true + NamedFieldFacts { density: _ } => false + KernelAmbientAtom { atom: _ } => false + } +} + + +data fact_density_hollow_alias: Symbol = fact_density_hollow_alias + + +fn hollow_alias_diagnostic(carrier: Node) -> Diagnostic { + Diagnostic { + reason: fact_density_hollow_alias, + at: NodeLocus { node: carrier }, + correction: Unavailable { reason: UserInputBoundary } + } +} + + +// The generated T-30 gate: fail-closed structural hollow-alias checker. +// A hollow carrier is Rejected with a diagnostic; every fact-bearing or +// kernel-ambient carrier is Produced. +fn hollow_alias_gate(carrier: Node) -> Outcome { + if carrier_is_hollow(carrier: carrier) { + Rejected { diagnostic: hollow_alias_diagnostic(carrier: carrier) } + } else { + Produced { value: true } + } +} + + +// Whole-module gate: a module is hollow-alias-free iff none of its declared +// carriers is hollow (fail-closed on any hollow carrier). +fn module_no_hollow_alias(declarations: List) -> Bool { + fold(declarations, init: true, f: fn(acc, d) { + acc && !carrier_is_hollow(carrier: d) + }) +} diff --git a/src/v4/test/claim/manual/fact_density_anchor.dag b/src/v4/test/claim/manual/fact_density_anchor.dag new file mode 100644 index 00000000000..85d532aa23e --- /dev/null +++ b/src/v4/test/claim/manual/fact_density_anchor.dag @@ -0,0 +1,80 @@ +// src/v4/test/claim/manual/fact_density_anchor.dag +// Scope: T-30 v2-bootstrap compile anchor β€” exercises the generated hollow-alias gate on a hollow alias, a fact-bundle carrier, and a kernel-ambient atom. +// Owns: fact_density_anchor_int32_symbol, fact_density_anchor_width_field, fact_density_anchor_signedness_field, fact_density_anchor_hollow_alias, fact_density_anchor_fact_bundle, fact_density_anchor_kernel_ambient_bool, anchor_hollow_alias_rejected, anchor_fact_bundle_produced, anchor_kernel_ambient_bool_exempt. +// Consumes: std fact_density, std node, std diagnostic. +// Status: scaffold β€” compile-only until T-22; gate logic pinned here + in std/fact_density.dag. +// Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md + +module v4.test.claim.manual.fact_density_anchor + + +import v4.std.fact_density { + hollow_alias_gate, + fact_density_kernel_ambient_bool +} +import v4.std.node { + Node, + TypeNode, + Atom, + Conj, + Edge, + Named, + Symbol +} +import v4.std.diagnostic { Outcome } + + +// A hollow alias β€” `type RustI32 = Int32`: an Atom carrier whose identity is +// a non-kernel-ambient external primitive and which reads zero own facts. +data fact_density_anchor_int32_symbol: Symbol = Int32 + +data fact_density_anchor_hollow_alias: Node = Node { + kind: TypeNode { connective: Atom { identity: fact_density_anchor_int32_symbol } }, + children: [] +} + + +// A real fact-bundle carrier β€” a Conj carrier with two named spec-read +// fact-edges (width, signedness). +data fact_density_anchor_width_field: Symbol = width +data fact_density_anchor_signedness_field: Symbol = signedness + +data fact_density_anchor_fact_bundle: Node = Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: fact_density_anchor_width_field }, + target: fact_density_anchor_hollow_alias + }, + Edge { + label: Named { name: fact_density_anchor_signedness_field }, + target: fact_density_anchor_hollow_alias + } + ] +} + + +// A kernel-ambient atom β€” `type RustBool = Bool`: an Atom carrier whose +// identity is the kernel-ambient `Bool`. Legitimately atomic, not hollow. +data fact_density_anchor_kernel_ambient_bool: Node = Node { + kind: TypeNode { connective: Atom { identity: fact_density_kernel_ambient_bool } }, + children: [] +} + + +// Acceptance anchor: the hollow alias fails closed (Rejected). +fn anchor_hollow_alias_rejected() -> Outcome { + hollow_alias_gate(carrier: fact_density_anchor_hollow_alias) +} + + +// Acceptance anchor: the fact-bundle carrier passes (Produced). +fn anchor_fact_bundle_produced() -> Outcome { + hollow_alias_gate(carrier: fact_density_anchor_fact_bundle) +} + + +// Acceptance anchor: the kernel-ambient atom is exempt (Produced). +fn anchor_kernel_ambient_bool_exempt() -> Outcome { + hollow_alias_gate(carrier: fact_density_anchor_kernel_ambient_bool) +} From ea88f7233b1feca4814f310702a67127d26f5ab5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 03:15:08 +0000 Subject: [PATCH 02/12] T-30: generated substrate-native hollow-alias checker (Node -> Outcome, fail-closed) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit std/fact_density.dag graduates from a body-less nominal to the generated structural checker `hollow_alias_gate: Node -> Outcome` β€” fails closed on a hollow carrier (zero own fact-edges), exempts kernel-ambient atoms. `SourceSpecReadFact` is now a 3-variant classification coproduct. test/claim/manual/fact_density_anchor.dag exercises the gate on a hollow alias, a fact-bundle carrier, and a kernel-ambient atom. Lands via the v2-bootstrap import path; v2 compile src/v4 = 74 modules, 0 diagnostics. STRUCTURE.md / DECISIONS.md updated. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/DECISIONS.md | 14 +++++++++++ src/v4/STRUCTURE.md | 6 ++++- src/v4/std/fact_density.dag | 23 +++++++++++-------- .../test/claim/manual/fact_density_anchor.dag | 6 ++--- 4 files changed, 36 insertions(+), 13 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 3f3595f7496..20a942fb769 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -965,6 +965,20 @@ language/format targets fan out against the same template. is deferred until `compile_to_dag` can prepend `std/node.dag` without colliding on v3-bootstrap top-level names; dissolution ships in the same change set as that bridge. +- **UPDATE 2026-05-19 (T-30 generated checker landed):** the body-less + nominal is superseded β€” `std/fact_density.dag` now carries the generated + structural checker `hollow_alias_gate: Node -> Outcome` (fail-closed + on a zero-fact carrier; kernel-ambient `Atom` exemption; `SourceSpecReadFact` + is now a 3-variant classification coproduct). It lands via the **v2-bootstrap + import path** (`v2-compiler compile --source-root src/v4` resolves + `import v4.std.node` / `import v4.std.diagnostic`) β€” **not** the + `compile_to_dag` node-prepend bridge, which is therefore not on T-30's + critical path. The kernel-ambient identity symbols are self-referential + `Symbol` constants (the substrate's only Symbol-introduction form); binding + them to the normalizer's interned kernel-ambient type symbols is + operator-closure pipeline wiring (T-30 IMPL+OP). `fact_density.dag` stays + **P2-staging** until that operator-closure wiring lands and retires the + Rust mirror `v4_hollow_alias_gate`. ### Status diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index 1a8cca4ff9c..ee98685e33d 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -32,7 +32,7 @@ src/v4/ collection.dag # bounded containers verification.dag # TestClaim schema + TierΓ—Layer classification (v4-fresh; studied v3/dsl) report.dag # advisory carrier (NOT fail-closed Diagnostic); used by synthesis lens - fact_density.dag # P2-staging only (INVARIANTS Β§P2): T-30 `compile_to_dag` parse witness β€” **not** a landed std primitive until a **generated** `.dag` consumer reads `SourceSpecReadFact`; hollow-alias authority today is the private Rust mirror module `v4_hollow_alias_gate` in `v3-compiler`. See `DECISIONS.md` T-30 encoding note + `TASKS.md` T-30. + fact_density.dag # T-30 generated structural hollow-alias checker β€” pure `hollow_alias_gate: Node -> Outcome`, fail-closed on a zero-fact carrier; consumed (compile-graph) by `test/claim/manual/fact_density_anchor.dag`. P2-staging (INVARIANTS Β§P2) until operator-closure wires pipeline enforcement and retires the Rust mirror `v4_hollow_alias_gate`. See `DECISIONS.md` T-30 encoding note + `TASKS.md` T-30. extdeps/ # external system contracts (23 files) cpp_abi.dag # C++ ABI / target data-model (LP64/LLP64/ILP32/ILP64) @@ -143,6 +143,10 @@ meta-layer cut, operator-ratified. **2026-05-17 (PR #3212):** enumerate C++ ABI / target data-model feeder; checksum **70β†’71** `.dag`. **2026-05-18 (T-30):** add `std/fact_density.dag` P2-staging parse witness; checksum **71β†’72** `.dag`. +**2026-05-19 (T-30):** `std/fact_density.dag` graduates from body-less nominal +to the generated structural hollow-alias checker (`hollow_alias_gate`); add +`test/claim/manual/fact_density_anchor.dag` v2-bootstrap compile anchor; +checksum **73β†’74** `.dag`. **2026-05-18 (PREFIX / T-23 v0):** add `lens/registry.dag` (`LensIdV0` + `LensModulePathV0` registry twin of `docs/briefs/r4-lane-a-lens-interface-freeze-pin.md` Β§3); checksum **72β†’73** `.dag`. **P2-staging** (INVARIANTS Β§P2) until a generated consumer reads the rows β€” paired diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index 1e658750326..7f65a8d3b8e 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -32,15 +32,20 @@ import v4.std.diagnostic { } -// Kernel-ambient atom identities (STRUCTURE.md "Kernel-ambient types"): -// String / Int / Bool / Char / List / Map are irreducible substrate atoms β€” -// a carrier aliasing one of them is legitimately atomic, not hollow. -data fact_density_kernel_ambient_string: Symbol = String -data fact_density_kernel_ambient_int: Symbol = Int -data fact_density_kernel_ambient_bool: Symbol = Bool -data fact_density_kernel_ambient_char: Symbol = Char -data fact_density_kernel_ambient_list: Symbol = List -data fact_density_kernel_ambient_map: Symbol = Map +// Kernel-ambient atom exemption set (STRUCTURE.md "Kernel-ambient types": +// String / Int / Bool / Char / List / Map). A carrier aliasing a +// kernel-ambient atom is legitimately atomic, not hollow β€” the gate exempts +// it. These identity symbols are self-referential Symbol constants (the +// substrate's only Symbol-introduction form); binding them to the +// normalizer's interned kernel-ambient type symbols is operator-closure +// pipeline wiring (T-30 IMPL+OP) β€” that wiring step is not part of this +// checker's definition. +data fact_density_kernel_ambient_string: Symbol = fact_density_kernel_ambient_string +data fact_density_kernel_ambient_int: Symbol = fact_density_kernel_ambient_int +data fact_density_kernel_ambient_bool: Symbol = fact_density_kernel_ambient_bool +data fact_density_kernel_ambient_char: Symbol = fact_density_kernel_ambient_char +data fact_density_kernel_ambient_list: Symbol = fact_density_kernel_ambient_list +data fact_density_kernel_ambient_map: Symbol = fact_density_kernel_ambient_map fn symbol_is_kernel_ambient(s: Symbol) -> Bool { diff --git a/src/v4/test/claim/manual/fact_density_anchor.dag b/src/v4/test/claim/manual/fact_density_anchor.dag index 85d532aa23e..2352b196321 100644 --- a/src/v4/test/claim/manual/fact_density_anchor.dag +++ b/src/v4/test/claim/manual/fact_density_anchor.dag @@ -26,7 +26,7 @@ import v4.std.diagnostic { Outcome } // A hollow alias β€” `type RustI32 = Int32`: an Atom carrier whose identity is // a non-kernel-ambient external primitive and which reads zero own facts. -data fact_density_anchor_int32_symbol: Symbol = Int32 +data fact_density_anchor_int32_symbol: Symbol = fact_density_anchor_int32_symbol data fact_density_anchor_hollow_alias: Node = Node { kind: TypeNode { connective: Atom { identity: fact_density_anchor_int32_symbol } }, @@ -36,8 +36,8 @@ data fact_density_anchor_hollow_alias: Node = Node { // A real fact-bundle carrier β€” a Conj carrier with two named spec-read // fact-edges (width, signedness). -data fact_density_anchor_width_field: Symbol = width -data fact_density_anchor_signedness_field: Symbol = signedness +data fact_density_anchor_width_field: Symbol = fact_density_anchor_width_field +data fact_density_anchor_signedness_field: Symbol = fact_density_anchor_signedness_field data fact_density_anchor_fact_bundle: Node = Node { kind: TypeNode { connective: Conj }, From 8f3765e42b5e2681eec48c9a37f1587bb87f3009 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 03:24:06 +0000 Subject: [PATCH 03/12] =?UTF-8?q?T-30:=20module=5Fno=5Fhollow=5Falias=20re?= =?UTF-8?q?turns=20Outcome=20=E2=80=94=20preserve=20fail-closed=20di?= =?UTF-8?q?agnostic?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses codex REQUEST_CHANGES on #3359: the module-level gate folded carrier_is_hollow into a plain Bool, collapsing a module-level failure to `false` and dropping the typed diagnostic path (INVARIANTS P3 regression). It now folds hollow_alias_gate and carries the first hollow carrier's Rejected { diagnostic } through to the boundary. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/std/fact_density.dag | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index 7f65a8d3b8e..b4c0f27bb44 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -145,10 +145,14 @@ fn hollow_alias_gate(carrier: Node) -> Outcome { } -// Whole-module gate: a module is hollow-alias-free iff none of its declared -// carriers is hollow (fail-closed on any hollow carrier). -fn module_no_hollow_alias(declarations: List) -> Bool { - fold(declarations, init: true, f: fn(acc, d) { - acc && !carrier_is_hollow(carrier: d) +// Whole-module gate: fail-closed on any hollow carrier. Carries the typed +// diagnostic of the first hollow declaration through to the boundary β€” +// never collapses a module-level failure to a bare Bool. +fn module_no_hollow_alias(declarations: List) -> Outcome { + fold(declarations, init: Produced { value: true }, f: fn(acc, d) { + match acc { + Rejected { diagnostic: dg } => Rejected { diagnostic: dg } + Produced { value: _ } => hollow_alias_gate(carrier: d) + } }) } From d320570427c92bbb7a56ae9f219585f7ad0f83a7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 23:38:36 -0400 Subject: [PATCH 04/12] =?UTF-8?q?WIP:=20T-30=20=E2=80=94=20generated=20hol?= =?UTF-8?q?low-alias=20.dag=20checker=20(Node->Outcome=20fail-closed;=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/DECISIONS.md | 1 + src/v4/std/fact_density.dag | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 20a942fb769..78ddddeac11 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -108,6 +108,7 @@ remain boundary indexes until the named substrate support lands. | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | | `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List` over named edges only. The removed path-step sum is not retained; positional addressing is subsumed by replacing the enclosing named subtree until a future ratified extension changes that shape. | | `std/witness.dag` | `Witness` | Green coproduct | Closed fail-closed proof/read carrier: `Holds { value } | Violates { diagnostic }`. Terminal because every read either carries the witnessed value or a diagnostic explaining the failed witness. | +| `std/fact_density.dag` | `SourceSpecReadFact` | Green coproduct | Closed classification of what a T-30 carrier reads from its source spec: `NamedFieldFacts { density: Int }` (β‰₯1 own fact-edge), `KernelAmbientAtom { atom: Symbol }` (exempt irreducible atom), `NoFact` (the hollow alias). Terminal because the three are mutually exclusive β€” a carrier records facts, is an exempt kernel-ambient atom, or records nothing β€” and the fail-closed hollow decision is exactly the `NoFact` arm. Variant-is-data fails: collapsing to a bare `Int` density loses the kernel-ambient-vs-hollow distinction at density 0. Not an algebra carrier; not a dimensional product (exactly one classification holds per carrier); not a parameterized family. | | `extdeps/coordination.dag` | `FrameworkBinding` | Green coproduct | Closed endpoint framework coordinate: an endpoint is either hosted by a named framework or not framework-hosted. Terminal because a bare optional would hide absence, and a flat record would make missing-present combinations representable. | | `extdeps/coordination.dag` | `ExchangePattern` | Green coproduct | Closed messaging-pattern coordinate: request-reply, fire-and-forget, stream, and publish-subscribe are mutually exclusive exchange topologies at the wire-contract layer. Settlement and replica convergence are separate coordinates, so async pubsub and streaming-with-convergence remain representable. | | `extdeps/coordination.dag` | `SettlementGuarantee` | Green coproduct | Closed settlement coordinate: a contract either settles immediately or carries a structural `SettleBound`. Terminal because an optional bound would allow boundedness to be skipped, while making settlement a coordinate avoids compressing it into exchange topology. | diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index b4c0f27bb44..7865427180a 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -58,9 +58,9 @@ fn symbol_is_kernel_ambient(s: Symbol) -> Bool { } -// 🟒 coproduct dissolution β€” what a carrier reads from its source spec. -// NoFact is the hollow alias: a carrier that decomposes into zero spec-read -// facts and is not an exempt kernel-ambient atom. +// 🟒 coproduct dissolution β€” DECISIONS.md classification ledger: SourceSpecReadFact. +// What a carrier reads from its source spec; NoFact is the hollow alias β€” +// a carrier decomposing into zero spec-read facts and not kernel-ambient. type SourceSpecReadFact = NamedFieldFacts { density: Int } | KernelAmbientAtom { atom: Symbol } From 0bc1b82efcb04d3e1a1d4e510ccb33322d05170b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 23:56:27 -0400 Subject: [PATCH 05/12] =?UTF-8?q?WIP:=20T-30=20=E2=80=94=20generated=20hol?= =?UTF-8?q?low-alias=20.dag=20checker=20(Node->Outcome=20fail-closed;=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/std/fact_density.dag | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index 7865427180a..7e0c804b53a 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -1,6 +1,6 @@ // src/v4/std/fact_density.dag // Scope: T-30 generated structural hollow-alias checker β€” a pure Node -> Outcome gate that fails closed on a carrier reading zero spec facts. -// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, density_fact, connective_spec_fact, carrier_spec_fact, carrier_is_hollow, fact_density_hollow_alias, hollow_alias_diagnostic, hollow_alias_gate, module_no_hollow_alias. +// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, density_fact, connective_spec_fact, carrier_is_hollow, fact_density_hollow_alias, hollow_alias_diagnostic, hollow_alias_gate, module_no_hollow_alias. // Consumes: std node, std diagnostic. // Status: T-30 generated checker; P2-staging until operator-closure wires pipeline enforcement. // Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md @@ -99,24 +99,20 @@ fn connective_spec_fact(c: Connective, child_count: Int) -> SourceSpecReadFact { } -// The spec facts a type carrier reads. Computation nodes are not type -// carriers β€” the hollow-alias concept does not apply, so they read a -// non-hollow result by construction. -fn carrier_spec_fact(carrier: Node) -> SourceSpecReadFact { +// A carrier is hollow iff it is a type carrier reading no spec facts. +// `SourceSpecReadFact` classifies only type carriers; computation nodes are +// not type carriers β€” the hollow-alias concept does not apply, so the kind +// match short-circuits them to non-hollow rather than forcing a spec-fact +// classification onto them. +fn carrier_is_hollow(carrier: Node) -> Bool { match carrier.kind { + ComputationNode { behavior: _ } => false TypeNode { connective: c } => - connective_spec_fact(c: c, child_count: count(carrier.children)) - ComputationNode { behavior: _ } => - KernelAmbientAtom { atom: fact_density_kernel_ambient_bool } - } -} - - -fn carrier_is_hollow(carrier: Node) -> Bool { - match carrier_spec_fact(carrier: carrier) { - NoFact => true - NamedFieldFacts { density: _ } => false - KernelAmbientAtom { atom: _ } => false + match connective_spec_fact(c: c, child_count: count(carrier.children)) { + NoFact => true + NamedFieldFacts { density: _ } => false + KernelAmbientAtom { atom: _ } => false + } } } From ed46a3bfe98ca95ed56558c8a7aa6890aec1ccf1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 03:59:52 +0000 Subject: [PATCH 06/12] T-30: drop carrier_spec_fact ComputationNode variant-abuse; fix changelog order MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses claude-opus-4-7 review on #3359: carrier_spec_fact returned KernelAmbientAtom for a ComputationNode β€” variant abuse, since a computation node is not a kernel-ambient atom. carrier_is_hollow now matches Node.kind directly (ComputationNode short-circuits to non-hollow); SourceSpecReadFact classifies only type carriers. STRUCTURE.md changelog entry reordered chronologically. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/STRUCTURE.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index ee98685e33d..3c76ff4e036 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -143,14 +143,14 @@ meta-layer cut, operator-ratified. **2026-05-17 (PR #3212):** enumerate C++ ABI / target data-model feeder; checksum **70β†’71** `.dag`. **2026-05-18 (T-30):** add `std/fact_density.dag` P2-staging parse witness; checksum **71β†’72** `.dag`. -**2026-05-19 (T-30):** `std/fact_density.dag` graduates from body-less nominal -to the generated structural hollow-alias checker (`hollow_alias_gate`); add -`test/claim/manual/fact_density_anchor.dag` v2-bootstrap compile anchor; -checksum **73β†’74** `.dag`. **2026-05-18 (PREFIX / T-23 v0):** add `lens/registry.dag` (`LensIdV0` + `LensModulePathV0` registry twin of `docs/briefs/r4-lane-a-lens-interface-freeze-pin.md` Β§3); checksum **72β†’73** `.dag`. **P2-staging** (INVARIANTS Β§P2) until a generated consumer reads the rows β€” paired `v4_lens_registry_dag_smoke_test.rs` receipt (parse witness only; same discipline as `fact_density.dag`). +**2026-05-19 (T-30):** `std/fact_density.dag` graduates from body-less nominal +to the generated structural hollow-alias checker (`hollow_alias_gate`); add +`test/claim/manual/fact_density_anchor.dag` v2-bootstrap compile anchor; +checksum **73β†’74** `.dag`. ## Scalar/numeric concept decomposition From c01b099b088290296a6f0da5e358c26e9c2ac8e3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 00:11:37 -0400 Subject: [PATCH 07/12] =?UTF-8?q?WIP:=20T-30=20=E2=80=94=20generated=20hol?= =?UTF-8?q?low-alias=20.dag=20checker=20(Node->Outcome=20fail-closed;=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/std/fact_density.dag | 27 ------------------- .../test/claim/manual/fact_density_anchor.dag | 11 +------- 2 files changed, 1 insertion(+), 37 deletions(-) diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index 7e0c804b53a..f731f3bff25 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -32,14 +32,6 @@ import v4.std.diagnostic { } -// Kernel-ambient atom exemption set (STRUCTURE.md "Kernel-ambient types": -// String / Int / Bool / Char / List / Map). A carrier aliasing a -// kernel-ambient atom is legitimately atomic, not hollow β€” the gate exempts -// it. These identity symbols are self-referential Symbol constants (the -// substrate's only Symbol-introduction form); binding them to the -// normalizer's interned kernel-ambient type symbols is operator-closure -// pipeline wiring (T-30 IMPL+OP) β€” that wiring step is not part of this -// checker's definition. data fact_density_kernel_ambient_string: Symbol = fact_density_kernel_ambient_string data fact_density_kernel_ambient_int: Symbol = fact_density_kernel_ambient_int data fact_density_kernel_ambient_bool: Symbol = fact_density_kernel_ambient_bool @@ -59,16 +51,12 @@ fn symbol_is_kernel_ambient(s: Symbol) -> Bool { // 🟒 coproduct dissolution β€” DECISIONS.md classification ledger: SourceSpecReadFact. -// What a carrier reads from its source spec; NoFact is the hollow alias β€” -// a carrier decomposing into zero spec-read facts and not kernel-ambient. type SourceSpecReadFact = NamedFieldFacts { density: Int } | KernelAmbientAtom { atom: Symbol } | NoFact -// Fact-density read: a carrier with >= 1 own fact-edge records that many -// spec-read facts; zero own fact-edges is the hollow shape. fn density_fact(child_count: Int) -> SourceSpecReadFact { if child_count == 0 { NoFact @@ -78,10 +66,6 @@ fn density_fact(child_count: Int) -> SourceSpecReadFact { } -// A bare alias `type X = Y` lowers to an Atom carrier with zero own -// fact-edges: hollow unless its identity is kernel-ambient. Conj / Disj / -// Arrow / Cardinality / Instantiation carriers read facts iff they carry -// own child edges. fn connective_spec_fact(c: Connective, child_count: Int) -> SourceSpecReadFact { match c { Atom { identity: id } => @@ -99,11 +83,6 @@ fn connective_spec_fact(c: Connective, child_count: Int) -> SourceSpecReadFact { } -// A carrier is hollow iff it is a type carrier reading no spec facts. -// `SourceSpecReadFact` classifies only type carriers; computation nodes are -// not type carriers β€” the hollow-alias concept does not apply, so the kind -// match short-circuits them to non-hollow rather than forcing a spec-fact -// classification onto them. fn carrier_is_hollow(carrier: Node) -> Bool { match carrier.kind { ComputationNode { behavior: _ } => false @@ -129,9 +108,6 @@ fn hollow_alias_diagnostic(carrier: Node) -> Diagnostic { } -// The generated T-30 gate: fail-closed structural hollow-alias checker. -// A hollow carrier is Rejected with a diagnostic; every fact-bearing or -// kernel-ambient carrier is Produced. fn hollow_alias_gate(carrier: Node) -> Outcome { if carrier_is_hollow(carrier: carrier) { Rejected { diagnostic: hollow_alias_diagnostic(carrier: carrier) } @@ -141,9 +117,6 @@ fn hollow_alias_gate(carrier: Node) -> Outcome { } -// Whole-module gate: fail-closed on any hollow carrier. Carries the typed -// diagnostic of the first hollow declaration through to the boundary β€” -// never collapses a module-level failure to a bare Bool. fn module_no_hollow_alias(declarations: List) -> Outcome { fold(declarations, init: Produced { value: true }, f: fn(acc, d) { match acc { diff --git a/src/v4/test/claim/manual/fact_density_anchor.dag b/src/v4/test/claim/manual/fact_density_anchor.dag index 2352b196321..2e430520b71 100644 --- a/src/v4/test/claim/manual/fact_density_anchor.dag +++ b/src/v4/test/claim/manual/fact_density_anchor.dag @@ -2,7 +2,7 @@ // Scope: T-30 v2-bootstrap compile anchor β€” exercises the generated hollow-alias gate on a hollow alias, a fact-bundle carrier, and a kernel-ambient atom. // Owns: fact_density_anchor_int32_symbol, fact_density_anchor_width_field, fact_density_anchor_signedness_field, fact_density_anchor_hollow_alias, fact_density_anchor_fact_bundle, fact_density_anchor_kernel_ambient_bool, anchor_hollow_alias_rejected, anchor_fact_bundle_produced, anchor_kernel_ambient_bool_exempt. // Consumes: std fact_density, std node, std diagnostic. -// Status: scaffold β€” compile-only until T-22; gate logic pinned here + in std/fact_density.dag. +// Status: scaffold β€” compile-only until T-22; gate logic pinned in std/fact_density.dag. // Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md module v4.test.claim.manual.fact_density_anchor @@ -24,8 +24,6 @@ import v4.std.node { import v4.std.diagnostic { Outcome } -// A hollow alias β€” `type RustI32 = Int32`: an Atom carrier whose identity is -// a non-kernel-ambient external primitive and which reads zero own facts. data fact_density_anchor_int32_symbol: Symbol = fact_density_anchor_int32_symbol data fact_density_anchor_hollow_alias: Node = Node { @@ -34,8 +32,6 @@ data fact_density_anchor_hollow_alias: Node = Node { } -// A real fact-bundle carrier β€” a Conj carrier with two named spec-read -// fact-edges (width, signedness). data fact_density_anchor_width_field: Symbol = fact_density_anchor_width_field data fact_density_anchor_signedness_field: Symbol = fact_density_anchor_signedness_field @@ -54,27 +50,22 @@ data fact_density_anchor_fact_bundle: Node = Node { } -// A kernel-ambient atom β€” `type RustBool = Bool`: an Atom carrier whose -// identity is the kernel-ambient `Bool`. Legitimately atomic, not hollow. data fact_density_anchor_kernel_ambient_bool: Node = Node { kind: TypeNode { connective: Atom { identity: fact_density_kernel_ambient_bool } }, children: [] } -// Acceptance anchor: the hollow alias fails closed (Rejected). fn anchor_hollow_alias_rejected() -> Outcome { hollow_alias_gate(carrier: fact_density_anchor_hollow_alias) } -// Acceptance anchor: the fact-bundle carrier passes (Produced). fn anchor_fact_bundle_produced() -> Outcome { hollow_alias_gate(carrier: fact_density_anchor_fact_bundle) } -// Acceptance anchor: the kernel-ambient atom is exempt (Produced). fn anchor_kernel_ambient_bool_exempt() -> Outcome { hollow_alias_gate(carrier: fact_density_anchor_kernel_ambient_bool) } From 6e18dd43cb9a1e7d0ac85c6c3b8d69603071e112 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 05:24:27 +0000 Subject: [PATCH 08/12] =?UTF-8?q?T-30:=20fact-density=20discriminator=20re?= =?UTF-8?q?work=20=E2=80=94=20NonZeroNat=20carrier,=20well-formed=20gate,?= =?UTF-8?q?=20file-tree=20enumeration?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Single coherent rework discharging the 3 operator BLOCKING threads on #3359 (operator-ruled fact-density-structural-enforcement direction): - NamedFieldFacts carries NonZeroNat (std/cardinality.dag) instead of raw Int β€” a >=1 fact count is structurally enforced, so it can no longer represent the NoFact zero-state (INVARIANTS P2 illegal-states). - hollow_alias_gate consumes node_well_formed before any children are read; a malformed carrier fails closed with malformed_carrier_diagnostic (INVARIANTS P3). - fact_density_anchor.dag enumerated in the STRUCTURE.md closed file tree; printed total 73 -> 74 .dag files. v2 compile src/v4 = 74 modules, 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/STRUCTURE.md | 3 +- src/v4/std/fact_density.dag | 66 +++++++++++++++++++++++++------------ 2 files changed, 47 insertions(+), 22 deletions(-) diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index 3c76ff4e036..dba847df190 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -119,12 +119,13 @@ src/v4/ nat_law_anchors.dag t19_manual_anchor_manifest.dag # T-19 manifest β€” `T19ManualAnchorKey` membership rows resolve_compile_anchor.dag # resolve + wave-1 canonical `Set` compile anchor (#3225; T-22 defers `v2 run`) + fact_density_anchor.dag # T-30 hollow-alias gate compile anchor (hollow / fact-bundle / kernel-ambient carriers; T-22 defers `v2 run`) boundary/ # boundary-honesty probes english_ingest_fail_closed.dag # T-4.11 β€” fail-closed ingest, no fabrication fixture/ # canonical input programs ``` -**Total: 73 .dag files + 5 docs + 5 .gitkeep = 83 files.** (Per invariant +**Total: 74 .dag files + 5 docs + 5 .gitkeep = 84 files.** (Per invariant #1 the enumeration above β€” not the count β€” is authoritative; the count is a checksum, updated on every operator-ratified file addition/removal. **Reconciliation (2026-05-17, PR #3225 / review #13750):** the prior printed diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag index f731f3bff25..79e7e726aa2 100644 --- a/src/v4/std/fact_density.dag +++ b/src/v4/std/fact_density.dag @@ -1,7 +1,7 @@ // src/v4/std/fact_density.dag -// Scope: T-30 generated structural hollow-alias checker β€” a pure Node -> Outcome gate that fails closed on a carrier reading zero spec facts. -// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, density_fact, connective_spec_fact, carrier_is_hollow, fact_density_hollow_alias, hollow_alias_diagnostic, hollow_alias_gate, module_no_hollow_alias. -// Consumes: std node, std diagnostic. +// Scope: T-30 generated structural hollow-alias checker β€” a pure Node -> Outcome gate that fails closed on a malformed carrier or a carrier reading zero spec facts. +// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, fact_density_nat, classify_density, connective_spec_fact, carrier_is_hollow, fact_density_hollow_alias, fact_density_malformed_carrier, hollow_alias_diagnostic, malformed_carrier_diagnostic, hollow_alias_gate, module_no_hollow_alias. +// Consumes: std node, std diagnostic, std nat, std cardinality. // Status: T-30 generated checker; P2-staging until operator-closure wires pipeline enforcement. // Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md @@ -10,6 +10,7 @@ module v4.std.fact_density import v4.std.node { Node, + Edge, Connective, Atom, Conj, @@ -19,7 +20,8 @@ import v4.std.node { Instantiation, TypeNode, ComputationNode, - Symbol + Symbol, + node_well_formed } import v4.std.diagnostic { Outcome, @@ -30,6 +32,8 @@ import v4.std.diagnostic { Unavailable, UserInputBoundary } +import v4.std.nat { Nat, Zero, Succ } +import v4.std.cardinality { NonZeroNat } data fact_density_kernel_ambient_string: Symbol = fact_density_kernel_ambient_string @@ -52,33 +56,39 @@ fn symbol_is_kernel_ambient(s: Symbol) -> Bool { // 🟒 coproduct dissolution β€” DECISIONS.md classification ledger: SourceSpecReadFact. type SourceSpecReadFact - = NamedFieldFacts { density: Int } + = NamedFieldFacts { density: NonZeroNat } | KernelAmbientAtom { atom: Symbol } | NoFact -fn density_fact(child_count: Int) -> SourceSpecReadFact { - if child_count == 0 { - NoFact - } else { - NamedFieldFacts { density: child_count } +fn fact_density_nat(children: List) -> Nat { + fold(children, init: Zero, f: fn(acc, _) { + Succ { prev: acc } + }) +} + + +fn classify_density(facts: Nat) -> SourceSpecReadFact { + match facts { + Zero => NoFact + Succ { prev: p } => NamedFieldFacts { density: NonZeroNat { prev: p } } } } -fn connective_spec_fact(c: Connective, child_count: Int) -> SourceSpecReadFact { +fn connective_spec_fact(c: Connective, facts: Nat) -> SourceSpecReadFact { match c { Atom { identity: id } => if symbol_is_kernel_ambient(s: id) { KernelAmbientAtom { atom: id } } else { - density_fact(child_count: child_count) + classify_density(facts: facts) } - Conj => density_fact(child_count: child_count) - Disj => density_fact(child_count: child_count) - Arrow => density_fact(child_count: child_count) - Cardinality => density_fact(child_count: child_count) - Instantiation => density_fact(child_count: child_count) + Conj => classify_density(facts: facts) + Disj => classify_density(facts: facts) + Arrow => classify_density(facts: facts) + Cardinality => classify_density(facts: facts) + Instantiation => classify_density(facts: facts) } } @@ -87,7 +97,7 @@ fn carrier_is_hollow(carrier: Node) -> Bool { match carrier.kind { ComputationNode { behavior: _ } => false TypeNode { connective: c } => - match connective_spec_fact(c: c, child_count: count(carrier.children)) { + match connective_spec_fact(c: c, facts: fact_density_nat(children: carrier.children)) { NoFact => true NamedFieldFacts { density: _ } => false KernelAmbientAtom { atom: _ } => false @@ -97,6 +107,7 @@ fn carrier_is_hollow(carrier: Node) -> Bool { data fact_density_hollow_alias: Symbol = fact_density_hollow_alias +data fact_density_malformed_carrier: Symbol = fact_density_malformed_carrier fn hollow_alias_diagnostic(carrier: Node) -> Diagnostic { @@ -108,11 +119,24 @@ fn hollow_alias_diagnostic(carrier: Node) -> Diagnostic { } +fn malformed_carrier_diagnostic(carrier: Node) -> Diagnostic { + Diagnostic { + reason: fact_density_malformed_carrier, + at: NodeLocus { node: carrier }, + correction: Unavailable { reason: UserInputBoundary } + } +} + + fn hollow_alias_gate(carrier: Node) -> Outcome { - if carrier_is_hollow(carrier: carrier) { - Rejected { diagnostic: hollow_alias_diagnostic(carrier: carrier) } + if node_well_formed(n: carrier) { + if carrier_is_hollow(carrier: carrier) { + Rejected { diagnostic: hollow_alias_diagnostic(carrier: carrier) } + } else { + Produced { value: true } + } } else { - Produced { value: true } + Rejected { diagnostic: malformed_carrier_diagnostic(carrier: carrier) } } } From bd60903f4482981d13bb2c176cc6aafc90fc447a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 07:27:14 +0000 Subject: [PATCH 09/12] T-30: sync SourceSpecReadFact ledger row to the NonZeroNat density carrier Addresses operator BLOCKING on #3359 (DECISIONS.md:111): the rework changed NamedFieldFacts to carry NonZeroNat but the classification ledger row still read `density: Int`. Row now names `density: NonZeroNat` and reframes the raw-Int illegal-state as the reason the carrier is structurally nonzero. DECISIONS.md-only; not on the v2 compile graph (checker compile unaffected). Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/DECISIONS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 78ddddeac11..756c7e25ba0 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -108,7 +108,7 @@ remain boundary indexes until the named substrate support lands. | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | | `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List` over named edges only. The removed path-step sum is not retained; positional addressing is subsumed by replacing the enclosing named subtree until a future ratified extension changes that shape. | | `std/witness.dag` | `Witness` | Green coproduct | Closed fail-closed proof/read carrier: `Holds { value } | Violates { diagnostic }`. Terminal because every read either carries the witnessed value or a diagnostic explaining the failed witness. | -| `std/fact_density.dag` | `SourceSpecReadFact` | Green coproduct | Closed classification of what a T-30 carrier reads from its source spec: `NamedFieldFacts { density: Int }` (β‰₯1 own fact-edge), `KernelAmbientAtom { atom: Symbol }` (exempt irreducible atom), `NoFact` (the hollow alias). Terminal because the three are mutually exclusive β€” a carrier records facts, is an exempt kernel-ambient atom, or records nothing β€” and the fail-closed hollow decision is exactly the `NoFact` arm. Variant-is-data fails: collapsing to a bare `Int` density loses the kernel-ambient-vs-hollow distinction at density 0. Not an algebra carrier; not a dimensional product (exactly one classification holds per carrier); not a parameterized family. | +| `std/fact_density.dag` | `SourceSpecReadFact` | Green coproduct | Closed classification of what a T-30 carrier reads from its source spec: `NamedFieldFacts { density: NonZeroNat }` (β‰₯1 own fact-edge), `KernelAmbientAtom { atom: Symbol }` (exempt irreducible atom), `NoFact` (the hollow alias). Terminal because the three are mutually exclusive β€” a carrier records facts, is an exempt kernel-ambient atom, or records nothing β€” and the fail-closed hollow decision is exactly the `NoFact` arm. The density payload is `NonZeroNat` (`std/cardinality.dag`), not a bare `Int`: a raw `Int` admits `0`/negative and could represent the same zero-fact state as `NoFact` (INVARIANTS P2 illegal-states), so the structurally-nonzero carrier makes that overlap unrepresentable. Not an algebra carrier; not a dimensional product (exactly one classification holds per carrier); not a parameterized family. | | `extdeps/coordination.dag` | `FrameworkBinding` | Green coproduct | Closed endpoint framework coordinate: an endpoint is either hosted by a named framework or not framework-hosted. Terminal because a bare optional would hide absence, and a flat record would make missing-present combinations representable. | | `extdeps/coordination.dag` | `ExchangePattern` | Green coproduct | Closed messaging-pattern coordinate: request-reply, fire-and-forget, stream, and publish-subscribe are mutually exclusive exchange topologies at the wire-contract layer. Settlement and replica convergence are separate coordinates, so async pubsub and streaming-with-convergence remain representable. | | `extdeps/coordination.dag` | `SettlementGuarantee` | Green coproduct | Closed settlement coordinate: a contract either settles immediately or carries a structural `SettleBound`. Terminal because an optional bound would allow boundedness to be skipped, while making settlement a coordinate avoids compressing it into exchange topology. | From 27f3e4d403a666ca5a5a2ef0c39d41132d311f5b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 14:24:52 -0400 Subject: [PATCH 10/12] =?UTF-8?q?WIP:=20T-30=20=E2=80=94=20generated=20hol?= =?UTF-8?q?low-alias=20.dag=20checker=20(Node->Outcome=20fail-closed;=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/lens/fact_density.dag | 102 ++++++++++++++++++ .../test/claim/manual/fact_density_anchor.dag | 26 ++--- 2 files changed, 115 insertions(+), 13 deletions(-) create mode 100644 src/v4/lens/fact_density.dag diff --git a/src/v4/lens/fact_density.dag b/src/v4/lens/fact_density.dag new file mode 100644 index 00000000000..c74f4b69bf2 --- /dev/null +++ b/src/v4/lens/fact_density.dag @@ -0,0 +1,102 @@ +// src/v4/lens/fact_density.dag +// Scope: T-30 fact-density lens β€” a pure-advisory read that classifies each type carrier by the spec facts it records, surfacing carriers with empty fact-cardinality. +// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, named_fact_count, density_fact, atom_spec_fact, connective_spec_fact, carrier_spec_fact. +// Consumes: std node, std nat, std cardinality. +// Status: T-30 lens β€” pure-advisory read; enforcement is the downstream apply_lens(Enforce) bridge, not this file. +// Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md + +module v4.lens.fact_density + + +import v4.std.node { + Node, + Edge, + Named, + Positional, + Connective, + Atom, + Conj, + Disj, + Arrow, + Cardinality, + Instantiation, + TypeNode, + ComputationNode, + Symbol +} +import v4.std.nat { Nat, Zero, Succ } +import v4.std.cardinality { NonZeroNat } + + +data fact_density_kernel_ambient_string: Symbol = fact_density_kernel_ambient_string +data fact_density_kernel_ambient_int: Symbol = fact_density_kernel_ambient_int +data fact_density_kernel_ambient_bool: Symbol = fact_density_kernel_ambient_bool +data fact_density_kernel_ambient_char: Symbol = fact_density_kernel_ambient_char +data fact_density_kernel_ambient_list: Symbol = fact_density_kernel_ambient_list +data fact_density_kernel_ambient_map: Symbol = fact_density_kernel_ambient_map + + +fn symbol_is_kernel_ambient(s: Symbol) -> Bool { + s == fact_density_kernel_ambient_string || + s == fact_density_kernel_ambient_int || + s == fact_density_kernel_ambient_bool || + s == fact_density_kernel_ambient_char || + s == fact_density_kernel_ambient_list || + s == fact_density_kernel_ambient_map +} + + +// 🟒 coproduct dissolution β€” DECISIONS.md classification ledger: SourceSpecReadFact. +type SourceSpecReadFact + = NamedFieldFacts { density: NonZeroNat } + | KernelAmbientAtom + | NoFact + | NotATypeCarrier + + +fn named_fact_count(children: List) -> Nat { + fold(children, init: Zero, f: fn(acc, e) { + match e.label { + Named { name: _ } => Succ { prev: acc } + Positional => acc + } + }) +} + + +fn density_fact(named_facts: Nat) -> SourceSpecReadFact { + match named_facts { + Zero => NoFact + Succ { prev: p } => NamedFieldFacts { density: NonZeroNat { prev: p } } + } +} + + +fn atom_spec_fact(id: Symbol, named_facts: Nat) -> SourceSpecReadFact { + if symbol_is_kernel_ambient(s: id) { + KernelAmbientAtom + } else { + density_fact(named_facts: named_facts) + } +} + + +fn connective_spec_fact(c: Connective, named_facts: Nat) -> SourceSpecReadFact { + match c { + Atom { identity: id } => atom_spec_fact(id: id, named_facts: named_facts) + Conj => density_fact(named_facts: named_facts) + Disj => density_fact(named_facts: named_facts) + Arrow => density_fact(named_facts: named_facts) + Cardinality => density_fact(named_facts: named_facts) + Instantiation => density_fact(named_facts: named_facts) + } +} + + +fn carrier_spec_fact(carrier: Node) -> SourceSpecReadFact { + match carrier.kind { + ComputationNode { behavior: _ } => NotATypeCarrier + TypeNode { connective: c } => + connective_spec_fact(c: c, named_facts: named_fact_count(children: carrier.children)) + } +} diff --git a/src/v4/test/claim/manual/fact_density_anchor.dag b/src/v4/test/claim/manual/fact_density_anchor.dag index 2e430520b71..b36eb581897 100644 --- a/src/v4/test/claim/manual/fact_density_anchor.dag +++ b/src/v4/test/claim/manual/fact_density_anchor.dag @@ -1,15 +1,16 @@ // src/v4/test/claim/manual/fact_density_anchor.dag -// Scope: T-30 v2-bootstrap compile anchor β€” exercises the generated hollow-alias gate on a hollow alias, a fact-bundle carrier, and a kernel-ambient atom. -// Owns: fact_density_anchor_int32_symbol, fact_density_anchor_width_field, fact_density_anchor_signedness_field, fact_density_anchor_hollow_alias, fact_density_anchor_fact_bundle, fact_density_anchor_kernel_ambient_bool, anchor_hollow_alias_rejected, anchor_fact_bundle_produced, anchor_kernel_ambient_bool_exempt. -// Consumes: std fact_density, std node, std diagnostic. -// Status: scaffold β€” compile-only until T-22; gate logic pinned in std/fact_density.dag. +// Scope: T-30 v2-bootstrap compile anchor β€” exercises the fact-density lens read on a hollow alias, a fact-bundle carrier, and a kernel-ambient atom. +// Owns: fact_density_anchor_int32_symbol, fact_density_anchor_width_field, fact_density_anchor_signedness_field, fact_density_anchor_hollow_alias, fact_density_anchor_fact_bundle, fact_density_anchor_kernel_ambient_bool, anchor_hollow_alias_read, anchor_fact_bundle_read, anchor_kernel_ambient_bool_read. +// Consumes: lens fact_density, std node. +// Status: scaffold β€” compile-only until T-22; lens read pinned in lens/fact_density.dag. // Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md module v4.test.claim.manual.fact_density_anchor -import v4.std.fact_density { - hollow_alias_gate, +import v4.lens.fact_density { + carrier_spec_fact, + SourceSpecReadFact, fact_density_kernel_ambient_bool } import v4.std.node { @@ -21,7 +22,6 @@ import v4.std.node { Named, Symbol } -import v4.std.diagnostic { Outcome } data fact_density_anchor_int32_symbol: Symbol = fact_density_anchor_int32_symbol @@ -56,16 +56,16 @@ data fact_density_anchor_kernel_ambient_bool: Node = Node { } -fn anchor_hollow_alias_rejected() -> Outcome { - hollow_alias_gate(carrier: fact_density_anchor_hollow_alias) +fn anchor_hollow_alias_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_hollow_alias) } -fn anchor_fact_bundle_produced() -> Outcome { - hollow_alias_gate(carrier: fact_density_anchor_fact_bundle) +fn anchor_fact_bundle_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_fact_bundle) } -fn anchor_kernel_ambient_bool_exempt() -> Outcome { - hollow_alias_gate(carrier: fact_density_anchor_kernel_ambient_bool) +fn anchor_kernel_ambient_bool_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_kernel_ambient_bool) } From 168ff08b4a0ef6354b872e590383e9d2ad9b19fa Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 18:32:20 +0000 Subject: [PATCH 11/12] =?UTF-8?q?T-30=20(operator=20RULING-6):=20complete?= =?UTF-8?q?=20fact=5Fdensity=20std->lens=20move=20=E2=80=94=20delete=20std?= =?UTF-8?q?=20file,=20sync=20docs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Auto-commit 27f3e4d40 added lens/fact_density.dag + reshaped the anchor but left the superseded std/fact_density.dag in place. This deletes it so the branch carries the single lens-only authority; DECISIONS.md ledger row + STRUCTURE.md tree/changelog synced to the lens reshaping. The lens read currently returns SourceSpecReadFact; (iii) apply_lens signature-conformance to Set is pending β€” std/report.dag is body-less scaffold (Report type unlanded, T-17), so `-> Set` cannot yet compile. v2 compile src/v4 = 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/DECISIONS.md | 18 ++++- src/v4/STRUCTURE.md | 11 ++- src/v4/std/fact_density.dag | 151 ------------------------------------ 3 files changed, 25 insertions(+), 155 deletions(-) delete mode 100644 src/v4/std/fact_density.dag diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index a6d0775f783..14587b738d2 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -108,7 +108,7 @@ remain boundary indexes until the named substrate support lands. | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | | `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List` over named edges only. The removed path-step sum is not retained; positional addressing is subsumed by replacing the enclosing named subtree until a future ratified extension changes that shape. | | `std/witness.dag` | `Witness` | Green coproduct | Closed fail-closed proof/read carrier: `Holds { value } | Violates { diagnostic }`. Terminal because every read either carries the witnessed value or a diagnostic explaining the failed witness. | -| `std/fact_density.dag` | `SourceSpecReadFact` | Green coproduct | Closed classification of what a T-30 carrier reads from its source spec: `NamedFieldFacts { density: NonZeroNat }` (β‰₯1 own fact-edge), `KernelAmbientAtom { atom: Symbol }` (exempt irreducible atom), `NoFact` (the hollow alias). Terminal because the three are mutually exclusive β€” a carrier records facts, is an exempt kernel-ambient atom, or records nothing β€” and the fail-closed hollow decision is exactly the `NoFact` arm. The density payload is `NonZeroNat` (`std/cardinality.dag`), not a bare `Int`: a raw `Int` admits `0`/negative and could represent the same zero-fact state as `NoFact` (INVARIANTS P2 illegal-states), so the structurally-nonzero carrier makes that overlap unrepresentable. Not an algebra carrier; not a dimensional product (exactly one classification holds per carrier); not a parameterized family. | +| `lens/fact_density.dag` | `SourceSpecReadFact` | Green coproduct | Closed classification the T-30 fact-density lens reads off a carrier: `NamedFieldFacts { density: NonZeroNat }` (β‰₯1 own NAMED spec-fact-edge), `KernelAmbientAtom` (exempt irreducible kernel-ambient atom β€” nullary, so a non-kernel symbol is structurally unrepresentable), `NoFact` (empty fact-cardinality β€” the surfaced carrier), `NotATypeCarrier` (a computation node, outside the lens's type-carrier domain). Terminal because the four are mutually exclusive and exhaustive over `Node`. The density payload is `NonZeroNat` (`std/cardinality.dag`), not a bare `Int`: a raw `Int` admits `0`/negative and could represent the same zero-fact state as `NoFact` (INVARIANTS P2 illegal-states), so the structurally-nonzero carrier makes that overlap unrepresentable. Only NAMED edges count as spec facts (positional operands of Arrow/Cardinality/Instantiation are composition, not facts). Not an algebra carrier; not a dimensional product (exactly one classification holds per carrier); not a parameterized family. | | `extdeps/coordination.dag` | `FrameworkBinding` | Green coproduct | Closed endpoint framework coordinate: an endpoint is either hosted by a named framework or not framework-hosted. Terminal because a bare optional would hide absence, and a flat record would make missing-present combinations representable. | | `extdeps/coordination.dag` | `ExchangePattern` | Green coproduct | Closed messaging-pattern coordinate: request-reply, fire-and-forget, stream, and publish-subscribe are mutually exclusive exchange topologies at the wire-contract layer. Settlement and replica convergence are separate coordinates, so async pubsub and streaming-with-convergence remain representable. | | `extdeps/coordination.dag` | `SettlementGuarantee` | Green coproduct | Closed settlement coordinate: a contract either settles immediately or carries a structural `SettleBound`. Terminal because an optional bound would allow boundedness to be skipped, while making settlement a coordinate avoids compressing it into exchange topology. | @@ -993,6 +993,22 @@ language/format targets fan out against the same template. operator-closure pipeline wiring (T-30 IMPL+OP). `fact_density.dag` stays **P2-staging** until that operator-closure wiring lands and retires the Rust mirror `v4_hollow_alias_gate`. +- **UPDATE 2026-05-19 (operator RULING-6 β€” fact_density is a LENS):** the + `std/` checker framing above is superseded. `fact_density.dag` moves + `std/` β†’ `lens/` β€” it is a lens, not std-kernel. It is reshaped as the + **pure-advisory** empty-cardinality lens read + `carrier_spec_fact: Node -> SourceSpecReadFact` (surfaces carriers whose + fact-cardinality is empty). The enforcement shape β€” `hollow_alias_gate`, + `Outcome`, `Rejected`, the `*_diagnostic` carriers, + `module_no_hollow_alias` β€” is **removed from the lens**: what to DO about a + flagged carrier (compile error / fail-closed) is the downstream + `apply_lens(_, Enforce)` advisoryβ†’fail-closed bridge, a SEPARATE concern + (RULING-6 hard read/enforcement separation). `SourceSpecReadFact` is now a + 4-variant read result (`NamedFieldFacts`/`KernelAmbientAtom`/`NoFact`/ + `NotATypeCarrier`); `KernelAmbientAtom` is nullary (no raw `Symbol` + payload β€” INVARIANTS P2 illegal-states); only NAMED edges count as spec + facts. `apply_lens` signature-conformance is pending the authoritative + T-23 lens-read contract. ### Status diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index dba847df190..3fc58c256bf 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -16,7 +16,7 @@ src/v4/ TASKS.md # the XL task plan (count drift-proof; see T-15) DECISIONS.md # design-decisions ledger (RATIFIED + record) - std/ # substrate primitives (15 landed + 1 P2-staging witness; see note on `fact_density.dag`) + std/ # substrate primitives (15 landed) node.dag # 6 type connectives + 5 L1 behaviors (substrate root) algebra.dag # Magma/Monoid/BoolAlgebra/FreeMonoid (structures only) cardinality.dag # cardinality refinement, P4 decidability @@ -32,7 +32,6 @@ src/v4/ collection.dag # bounded containers verification.dag # TestClaim schema + TierΓ—Layer classification (v4-fresh; studied v3/dsl) report.dag # advisory carrier (NOT fail-closed Diagnostic); used by synthesis lens - fact_density.dag # T-30 generated structural hollow-alias checker β€” pure `hollow_alias_gate: Node -> Outcome`, fail-closed on a zero-fact carrier; consumed (compile-graph) by `test/claim/manual/fact_density_anchor.dag`. P2-staging (INVARIANTS Β§P2) until operator-closure wires pipeline enforcement and retires the Rust mirror `v4_hollow_alias_gate`. See `DECISIONS.md` T-30 encoding note + `TASKS.md` T-30. extdeps/ # external system contracts (23 files) cpp_abi.dag # C++ ABI / target data-model (LP64/LLP64/ILP32/ILP64) @@ -87,6 +86,7 @@ src/v4/ testgen.dag # producer side β€” reads substrate, emits TestClaim corpus (Phase 1.5) affected_set.dag # incremental re-exec frontier; replaces detect-affected shell (Phase 1.5) application.dag # apply_lens surface β€” opt-in depth + ONLY advisoryβ†’fail-closed bridge + fact_density.dag # T-30 fact-density lens β€” pure-advisory `carrier_spec_fact: Node -> SourceSpecReadFact`; surfaces carriers with empty fact-cardinality. Enforcement is the downstream `apply_lens(Enforce)` bridge, not this file. Compile-graph exercised by `test/claim/manual/fact_density_anchor.dag`. registry.dag # P2-staging only (INVARIANTS Β§P2): PREFIX T-23 v0 `LensIdV0` Γ— `LensModulePathV0` rows β€” **not** landed single authority until a **generated** consumer reads `LensRegistryEntryV0`; `v4_lens_registry_dag_smoke_test.rs` is **parse + inference cleanliness** only (same posture as `fact_density.dag`). Operator pin Β§3 human mirror; amend `.dag` first. workflow/ # meta-process as data (2 files; the v3-derived @@ -119,7 +119,7 @@ src/v4/ nat_law_anchors.dag t19_manual_anchor_manifest.dag # T-19 manifest β€” `T19ManualAnchorKey` membership rows resolve_compile_anchor.dag # resolve + wave-1 canonical `Set` compile anchor (#3225; T-22 defers `v2 run`) - fact_density_anchor.dag # T-30 hollow-alias gate compile anchor (hollow / fact-bundle / kernel-ambient carriers; T-22 defers `v2 run`) + fact_density_anchor.dag # T-30 fact-density lens compile anchor (hollow / fact-bundle / kernel-ambient carriers; T-22 defers `v2 run`) boundary/ # boundary-honesty probes english_ingest_fail_closed.dag # T-4.11 β€” fail-closed ingest, no fabrication fixture/ # canonical input programs @@ -152,6 +152,11 @@ checksum **71β†’72** `.dag`. to the generated structural hollow-alias checker (`hollow_alias_gate`); add `test/claim/manual/fact_density_anchor.dag` v2-bootstrap compile anchor; checksum **73β†’74** `.dag`. +**2026-05-19 (T-30, operator RULING-6):** `fact_density.dag` moves `std/` β†’ `lens/` +β€” it is a lens, not std-kernel β€” reshaped as the pure-advisory empty-cardinality +lens read (`carrier_spec_fact: Node -> SourceSpecReadFact`); the enforcement shape +(`hollow_alias_gate`/`Outcome`/diagnostics) is removed (downstream `apply_lens(Enforce)`). +Net `.dag` count unchanged at **74** (relocation, not addition). ## Scalar/numeric concept decomposition diff --git a/src/v4/std/fact_density.dag b/src/v4/std/fact_density.dag deleted file mode 100644 index 79e7e726aa2..00000000000 --- a/src/v4/std/fact_density.dag +++ /dev/null @@ -1,151 +0,0 @@ -// src/v4/std/fact_density.dag -// Scope: T-30 generated structural hollow-alias checker β€” a pure Node -> Outcome gate that fails closed on a malformed carrier or a carrier reading zero spec facts. -// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, fact_density_nat, classify_density, connective_spec_fact, carrier_is_hollow, fact_density_hollow_alias, fact_density_malformed_carrier, hollow_alias_diagnostic, malformed_carrier_diagnostic, hollow_alias_gate, module_no_hollow_alias. -// Consumes: std node, std diagnostic, std nat, std cardinality. -// Status: T-30 generated checker; P2-staging until operator-closure wires pipeline enforcement. -// Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md - -module v4.std.fact_density - - -import v4.std.node { - Node, - Edge, - Connective, - Atom, - Conj, - Disj, - Arrow, - Cardinality, - Instantiation, - TypeNode, - ComputationNode, - Symbol, - node_well_formed -} -import v4.std.diagnostic { - Outcome, - Produced, - Rejected, - Diagnostic, - NodeLocus, - Unavailable, - UserInputBoundary -} -import v4.std.nat { Nat, Zero, Succ } -import v4.std.cardinality { NonZeroNat } - - -data fact_density_kernel_ambient_string: Symbol = fact_density_kernel_ambient_string -data fact_density_kernel_ambient_int: Symbol = fact_density_kernel_ambient_int -data fact_density_kernel_ambient_bool: Symbol = fact_density_kernel_ambient_bool -data fact_density_kernel_ambient_char: Symbol = fact_density_kernel_ambient_char -data fact_density_kernel_ambient_list: Symbol = fact_density_kernel_ambient_list -data fact_density_kernel_ambient_map: Symbol = fact_density_kernel_ambient_map - - -fn symbol_is_kernel_ambient(s: Symbol) -> Bool { - s == fact_density_kernel_ambient_string || - s == fact_density_kernel_ambient_int || - s == fact_density_kernel_ambient_bool || - s == fact_density_kernel_ambient_char || - s == fact_density_kernel_ambient_list || - s == fact_density_kernel_ambient_map -} - - -// 🟒 coproduct dissolution β€” DECISIONS.md classification ledger: SourceSpecReadFact. -type SourceSpecReadFact - = NamedFieldFacts { density: NonZeroNat } - | KernelAmbientAtom { atom: Symbol } - | NoFact - - -fn fact_density_nat(children: List) -> Nat { - fold(children, init: Zero, f: fn(acc, _) { - Succ { prev: acc } - }) -} - - -fn classify_density(facts: Nat) -> SourceSpecReadFact { - match facts { - Zero => NoFact - Succ { prev: p } => NamedFieldFacts { density: NonZeroNat { prev: p } } - } -} - - -fn connective_spec_fact(c: Connective, facts: Nat) -> SourceSpecReadFact { - match c { - Atom { identity: id } => - if symbol_is_kernel_ambient(s: id) { - KernelAmbientAtom { atom: id } - } else { - classify_density(facts: facts) - } - Conj => classify_density(facts: facts) - Disj => classify_density(facts: facts) - Arrow => classify_density(facts: facts) - Cardinality => classify_density(facts: facts) - Instantiation => classify_density(facts: facts) - } -} - - -fn carrier_is_hollow(carrier: Node) -> Bool { - match carrier.kind { - ComputationNode { behavior: _ } => false - TypeNode { connective: c } => - match connective_spec_fact(c: c, facts: fact_density_nat(children: carrier.children)) { - NoFact => true - NamedFieldFacts { density: _ } => false - KernelAmbientAtom { atom: _ } => false - } - } -} - - -data fact_density_hollow_alias: Symbol = fact_density_hollow_alias -data fact_density_malformed_carrier: Symbol = fact_density_malformed_carrier - - -fn hollow_alias_diagnostic(carrier: Node) -> Diagnostic { - Diagnostic { - reason: fact_density_hollow_alias, - at: NodeLocus { node: carrier }, - correction: Unavailable { reason: UserInputBoundary } - } -} - - -fn malformed_carrier_diagnostic(carrier: Node) -> Diagnostic { - Diagnostic { - reason: fact_density_malformed_carrier, - at: NodeLocus { node: carrier }, - correction: Unavailable { reason: UserInputBoundary } - } -} - - -fn hollow_alias_gate(carrier: Node) -> Outcome { - if node_well_formed(n: carrier) { - if carrier_is_hollow(carrier: carrier) { - Rejected { diagnostic: hollow_alias_diagnostic(carrier: carrier) } - } else { - Produced { value: true } - } - } else { - Rejected { diagnostic: malformed_carrier_diagnostic(carrier: carrier) } - } -} - - -fn module_no_hollow_alias(declarations: List) -> Outcome { - fold(declarations, init: Produced { value: true }, f: fn(acc, d) { - match acc { - Rejected { diagnostic: dg } => Rejected { diagnostic: dg } - Produced { value: _ } => hollow_alias_gate(carrier: d) - } - }) -} From ed5bc022ece3ed1af1a131697fb961eab8c520e5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 18:56:54 +0000 Subject: [PATCH 12/12] =?UTF-8?q?T-30=20(RULING-6):=20connective=5Fspec=5F?= =?UTF-8?q?fact=20refined-alpha=20=E2=80=94=20factor=20connective=5Fis=5Fk?= =?UTF-8?q?ernel=5Fambient=5Fatom?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Practice-10 dissolution of the connective_spec_fact template-hole: the 6-arm Connective dispatch did 2-distinct-RHS work (one outlier kernel-ambient-atom specialization, five identical density routes) β€” a work-vs-shape mismatch. Refined-alpha factors a named Bool predicate connective_is_kernel_ambient_atom (2-arm: Atom+kernel-ambient => true, else false) and connective_spec_fact becomes the binary branch reflecting its real structure. KernelAmbientAtom stays nullary (#A). No new substrate primitive. v2 compile src/v4 = 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/lens/fact_density.dag | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/v4/lens/fact_density.dag b/src/v4/lens/fact_density.dag index c74f4b69bf2..ca56cea87d3 100644 --- a/src/v4/lens/fact_density.dag +++ b/src/v4/lens/fact_density.dag @@ -1,6 +1,6 @@ // src/v4/lens/fact_density.dag // Scope: T-30 fact-density lens β€” a pure-advisory read that classifies each type carrier by the spec facts it records, surfacing carriers with empty fact-cardinality. -// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, named_fact_count, density_fact, atom_spec_fact, connective_spec_fact, carrier_spec_fact. +// Owns: SourceSpecReadFact, fact_density_kernel_ambient_string, fact_density_kernel_ambient_int, fact_density_kernel_ambient_bool, fact_density_kernel_ambient_char, fact_density_kernel_ambient_list, fact_density_kernel_ambient_map, symbol_is_kernel_ambient, named_fact_count, density_fact, connective_is_kernel_ambient_atom, connective_spec_fact, carrier_spec_fact. // Consumes: std node, std nat, std cardinality. // Status: T-30 lens β€” pure-advisory read; enforcement is the downstream apply_lens(Enforce) bridge, not this file. // Anchor: https://github.com/gunb-ai/gunbc/blob/main/src/v4/TASKS.md @@ -72,23 +72,19 @@ fn density_fact(named_facts: Nat) -> SourceSpecReadFact { } -fn atom_spec_fact(id: Symbol, named_facts: Nat) -> SourceSpecReadFact { - if symbol_is_kernel_ambient(s: id) { - KernelAmbientAtom - } else { - density_fact(named_facts: named_facts) +fn connective_is_kernel_ambient_atom(c: Connective) -> Bool { + match c { + Atom { identity: id } => symbol_is_kernel_ambient(s: id) + _ => false } } fn connective_spec_fact(c: Connective, named_facts: Nat) -> SourceSpecReadFact { - match c { - Atom { identity: id } => atom_spec_fact(id: id, named_facts: named_facts) - Conj => density_fact(named_facts: named_facts) - Disj => density_fact(named_facts: named_facts) - Arrow => density_fact(named_facts: named_facts) - Cardinality => density_fact(named_facts: named_facts) - Instantiation => density_fact(named_facts: named_facts) + if connective_is_kernel_ambient_atom(c: c) { + KernelAmbientAtom + } else { + density_fact(named_facts: named_facts) } }