diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index dfc55e76ce2..289cd658256 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -111,6 +111,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. | +| `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. | @@ -987,6 +988,36 @@ 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`. +- **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 05edd275314..54ee13abb5f 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 # 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. extdeps/ # external system contracts (23 files) cpp_abi.dag # C++ ABI / target data-model (LP64/LLP64/ILP32/ILP64) @@ -88,6 +87,7 @@ src/v4/ affected_set.dag # incremental re-exec frontier; replaces detect-affected shell (Phase 1.5) affected_set_examples.dag # expected affected-frontier example values 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 @@ -120,6 +120,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 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 diff --git a/src/v4/lens/fact_density.dag b/src/v4/lens/fact_density.dag new file mode 100644 index 00000000000..ca56cea87d3 --- /dev/null +++ b/src/v4/lens/fact_density.dag @@ -0,0 +1,98 @@ +// 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, 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 + +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 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 { + if connective_is_kernel_ambient_atom(c: c) { + KernelAmbientAtom + } else { + 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/std/fact_density.dag b/src/v4/std/fact_density.dag deleted file mode 100644 index 89507fd3bfc..00000000000 --- a/src/v4/std/fact_density.dag +++ /dev/null @@ -1,10 +0,0 @@ -// 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 - -module v4.std.fact_density - -type SourceSpecReadFact 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..b36eb581897 --- /dev/null +++ b/src/v4/test/claim/manual/fact_density_anchor.dag @@ -0,0 +1,71 @@ +// src/v4/test/claim/manual/fact_density_anchor.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.lens.fact_density { + carrier_spec_fact, + SourceSpecReadFact, + fact_density_kernel_ambient_bool +} +import v4.std.node { + Node, + TypeNode, + Atom, + Conj, + Edge, + Named, + Symbol +} + + +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_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_hollow_alias) +} + + +fn anchor_fact_bundle_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_fact_bundle) +} + + +fn anchor_kernel_ambient_bool_read() -> SourceSpecReadFact { + carrier_spec_fact(carrier: fact_density_anchor_kernel_ambient_bool) +}