Skip to content
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
188b924
WIP: T-30 — generated hollow-alias .dag checker (Node->Outcome fail-c…
briansrls May 19, 2026
ea88f72
T-30: generated substrate-native hollow-alias checker (Node -> Outcom…
briansrls May 19, 2026
8f3765e
T-30: module_no_hollow_alias returns Outcome<Bool> — preserve fail-cl…
briansrls May 19, 2026
d320570
WIP: T-30 — generated hollow-alias .dag checker (Node->Outcome fail-c…
briansrls May 19, 2026
0bc1b82
WIP: T-30 — generated hollow-alias .dag checker (Node->Outcome fail-c…
briansrls May 19, 2026
ed46a3b
T-30: drop carrier_spec_fact ComputationNode variant-abuse; fix chang…
briansrls May 19, 2026
c01b099
WIP: T-30 — generated hollow-alias .dag checker (Node->Outcome fail-c…
briansrls May 19, 2026
6e18dd4
T-30: fact-density discriminator rework — NonZeroNat carrier, well-fo…
briansrls May 19, 2026
bd60903
T-30: sync SourceSpecReadFact ledger row to the NonZeroNat density ca…
briansrls May 19, 2026
beaa52b
Merge remote-tracking branch 'origin/main' into session/bold-bear-747
briansrls May 19, 2026
ef2780a
Merge remote-tracking branch 'origin/main' into session/bold-bear-747
briansrls May 19, 2026
1c42962
Merge remote-tracking branch 'origin/main' into session/bold-bear-747
briansrls May 19, 2026
3f3f47c
Merge remote-tracking branch 'origin/main' into session/bold-bear-747
briansrls May 19, 2026
27f3e4d
WIP: T-30 — generated hollow-alias .dag checker (Node->Outcome fail-c…
briansrls May 19, 2026
168ff08
T-30 (operator RULING-6): complete fact_density std->lens move — dele…
briansrls May 19, 2026
ed5bc02
T-30 (RULING-6): connective_spec_fact refined-alpha — factor connecti…
briansrls May 19, 2026
3d6d2d5
Merge branch 'main' into session/bold-bear-747
briansrls May 19, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions src/v4/DECISIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -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<Symbol>` 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<C>` | 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. |
| `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. |
Expand Down Expand Up @@ -978,6 +979,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<Bool>` (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

Expand Down
9 changes: 7 additions & 2 deletions src/v4/STRUCTURE.md
Original file line number Diff line number Diff line change
Expand Up @@ -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<Bool>`, 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)
Expand Down Expand Up @@ -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
Expand All @@ -147,6 +148,10 @@ checksum **71→72** `.dag`.
`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;

This comment was marked as resolved.

checksum **73→74** `.dag`.

## Scalar/numeric concept decomposition

Expand Down
151 changes: 146 additions & 5 deletions src/v4/std/fact_density.dag
Original file line number Diff line number Diff line change
@@ -1,10 +1,151 @@
// 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 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 }

This comment was marked as resolved.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This finding is a diff-only review artifact — NonZeroNat is declared. src/v4/std/cardinality.dag:17 declares type NonZeroNat { prev: Nat }, and that module's // Owns: header line lists NonZeroNat. cardinality.dag is unchanged by this PR, so it is not in the diff — a reviewer seeing only the diff sees the import v4.std.cardinality { NonZeroNat } but not the declaration, and infers absence.

The generated checker compiles clean: v2-compiler compile --source-root src/v4 --target dag at this head (6e18dd43c) = indexed 74 modules, 0 diagnostics (and an independent --target rust re-verify, also 74 modules / 0 diagnostics). The "cannot compile" claim is contradicted by both compiles.

No code change needed for this thread.

— sent from bold-bear-747



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 }

This comment was marked as resolved.

| NoFact


fn fact_density_nat(children: List<Edge>) -> Nat {
fold(children, init: Zero, f: fn(acc, _) {

This comment was marked as resolved.

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 {

This comment was marked as resolved.

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<Bool> {
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<Node>) -> Outcome<Bool> {

This comment was marked as resolved.

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)
}
})
}
71 changes: 71 additions & 0 deletions src/v4/test/claim/manual/fact_density_anchor.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
// 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.
// 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 }


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 } },
children: []
}


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 },
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
}
]
}


data fact_density_anchor_kernel_ambient_bool: Node = Node {
kind: TypeNode { connective: Atom { identity: fact_density_kernel_ambient_bool } },
children: []
}


fn anchor_hollow_alias_rejected() -> Outcome<Bool> {
hollow_alias_gate(carrier: fact_density_anchor_hollow_alias)
}


fn anchor_fact_bundle_produced() -> Outcome<Bool> {
hollow_alias_gate(carrier: fact_density_anchor_fact_bundle)
}


fn anchor_kernel_ambient_bool_exempt() -> Outcome<Bool> {
hollow_alias_gate(carrier: fact_density_anchor_kernel_ambient_bool)
}
Loading