Repository navigation
T-30 — generated hollow-alias .dag checker (Node->Outcome fail-closed; substrate-native) - #3359
Conversation
…e, fail-closed) std/fact_density.dag graduates from a body-less nominal to the generated structural checker `hollow_alias_gate: Node -> Outcome<Bool>` — 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) <noreply@anthropic.com>
…osed diagnostic 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) <noreply@anthropic.com>
…elog order 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) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c01b099b· Trigger:schedule - Thinking:
517s wall
BLOCKING (3)
Root Cause
src/v4/std/fact_density.dagfact-density uses rawIntinstead of a nonzero cardinality/refinement carrier or removing the redundant density payload → use a structurally nonzero count fromstd/cardinality.dagor make the variant carry no invalid count.src/v4/std/fact_density.dagthe T-30 gate reads raw Node storage shape directly instead of validating through the existingstd/node.dagwell-formedness query → import/usenode_well_formedand reject malformed carriers before density classification.src/v4/STRUCTURE.mdthe new manual anchor was added as a note-only delta → add it undertest/claim/manual/and update the printed total from 73 to 74.dagfiles.
|
|
||
| // 🟢 coproduct dissolution — DECISIONS.md classification ledger: SourceSpecReadFact. | ||
| type SourceSpecReadFact | ||
| = NamedFieldFacts { density: Int } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| match carrier.kind { | ||
| ComputationNode { behavior: _ } => false | ||
| TypeNode { connective: c } => | ||
| match connective_spec_fact(c: c, child_count: count(carrier.children)) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| `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.
This comment was marked as resolved.
Sorry, something went wrong.
…rmed gate, file-tree enumeration 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) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
6e18dd43· Trigger:schedule - Thinking:
234s wall
BLOCKING (2)
Root Cause
src/v4/std/fact_density.dagThe density repair switched to a nonzero refinement carrier without landing the v4 std/cardinality definition in the same PR → add the carrier with its ledger entry or encode the nonzero density using an existing declared v4 Nat shape.src/v4/DECISIONS.mdThe coproduct ledger was not updated atomically with the density carrier change → make DECISIONS.md name the same carrier and remove the stale raw-Int density rationale.
| UserInputBoundary | ||
| } | ||
| import v4.std.nat { Nat, Zero, Succ } | ||
| import v4.std.cardinality { NonZeroNat } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
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
| | `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: 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. | |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…rrier 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) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
bd60903f· Trigger:schedule - Thinking:
418s wall
BLOCKING (3)
Root Cause
src/v4/std/fact_density.dagkernel-ambient identity is modeled as local raw Symbol constants rather than a refined KernelAmbientSymbol or exemption witness → introduce a typed kernel-ambient carrier or make the exemption nullary and have SourceSpecReadFact carry that authority.src/v4/std/fact_density.dagthe gate decomposes SourceSpecReadFact back into an untracked Bool helper instead of consuming the classification directly → inline the match into hollow_alias_gate or add a tracked predicate-dissolution receipt.src/v4/std/fact_density.dagthe module-level gate needs fail-closed traversal but does not consume or name a shared traverse/sequence primitive → bind the missing primitive to an owning task and dissolve-on-arrival, or use the canonical traversal if it already exists.
| // 🟢 coproduct dissolution — DECISIONS.md classification ledger: SourceSpecReadFact. | ||
| type SourceSpecReadFact | ||
| = NamedFieldFacts { density: NonZeroNat } | ||
| | KernelAmbientAtom { atom: Symbol } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| } | ||
|
|
||
|
|
||
| fn carrier_is_hollow(carrier: Node) -> Bool { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| } | ||
|
|
||
|
|
||
| fn module_no_hollow_alias(declarations: List<Node>) -> Outcome<Bool> { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
beaa52bf· Trigger:schedule - Thinking:
219s wall
BLOCKING (1)
Root Cause
src/v4/std/fact_density.dagSourceSpecReadFact uses raw Node child density as its fact witness → count only named source-fact edges or introduce a typed spec-read fact edge/refinement before treating children as evidence.
|
|
||
|
|
||
| fn fact_density_nat(children: List<Edge>) -> Nat { | ||
| fold(children, init: Zero, f: fn(acc, _) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
ef2780ab· Trigger:schedule - Thinking:
295s wall
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1c429626· Trigger:schedule - Thinking:
257s wall
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
3f3f47c0· Trigger:schedule - Thinking:
215s wall
…te std file, sync docs Auto-commit 27f3e4d 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<Report> is pending — std/report.dag is body-less scaffold (Report type unlanded, T-17), so `-> Set<Report>` cannot yet compile. v2 compile src/v4 = 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ve_is_kernel_ambient_atom 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) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
ed5bc022· Trigger:schedule - Thinking:
223s wall
BLOCKING (2)
Root Cause
src/v4/lens/fact_density.dagfact-density is treating EdgeLabel representation as a local authority → import and consume the canonical std/node query, or add the missing query there before the lens reads it.src/v4/lens/fact_density.dagthe kernel-ambient check was factored into a reusable derived predicate without a tracked disposition → either dissolve it into the classifier or add a bounded P10 receipt with owner/lane/trigger.
|
|
||
| fn named_fact_count(children: List<Edge>) -> Nat { | ||
| fold(children, init: Zero, f: fn(acc, e) { | ||
| match e.label { |
There was a problem hiding this comment.
BLOCKING: named_fact_count directly matches EdgeLabel instead of consuming std/node.dag's declared edge_is_named query, so the lens re-derives lower-layer storage shape and violates INVARIANTS P2/L-7 single-authority boundary discipline.
| } | ||
|
|
||
|
|
||
| fn connective_is_kernel_ambient_atom(c: Connective) -> Bool { |
There was a problem hiding this comment.
BLOCKING: connective_is_kernel_ambient_atom is a new Bool predicate over the Connective coproduct with no Practice-10 disposition tag or DECISIONS receipt, violating predicate-dissolution discipline.
Address briansrls inline BLOCKING on #3455:1120 — the original Outlier dissolution path advised "extract a named Bool helper / sibling lens finding (L1.1 territory)," which is EXACTLY the L1.1 predicate-dissolution anti-pattern (Bool-returning fn over a coproduct with literal true/false arms per variant). Corrected dissolution path: - Consume the discriminator structurally via match patterns + guards on the existing coproduct, OR substructure the coproduct so the one-vs-many distinction is a top-level variant. - Function body becomes a 2-arm match: `match x { <Special_pattern> => special; _ => default }` with the discriminator as a sub-pattern or guard. - DO NOT extract a named Bool helper — explicit prohibition with citation to L1.1's signature. Recent precedent updated: PR #3359 connective_spec_fact was resolved via inline match-pattern with guard, NOT a Bool helper. L1.13's "extract a discriminator" reflex must satisfy L1.1 as well as itself — the discriminant is structural (substrate-known from the parsed match), not a hand-rolled helper. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…n; Practice 11's runtime-symptom catcher; 3 real-corpus findings cited) (#3455) * design: L1.13 skeleton-collapse lens — kills parametric-arm duplication via constructor-name template L1.13 catches the runtime symptom of Practice 11 (just landed in #3444) parametric duplication at the match-arm level: matches whose RHSes collapse to K << N distinct skeletons under α-renaming + constructor-name substitution. Distribution-shape classifier: - PureTemplate (K=1): dispatch doing zero work - Outlier (K=2 with 1:N-1): predicate-factor - Categorical (K small, multi-group): push categorization into the coproduct's type definition - Mixed (K close to N): legitimate per-variant dispatch Sibling-of L1.1: where L1.1 catches Bool-returning matches with literal true/false arms, L1.13 catches non-Bool matches with constructor-name templating across arms. Operator-direct 2026-05-21 — first lens shipped under the "every lens demonstrates value at PR time" discipline. Three real-corpus findings cited in PR body (F14 feature_disposition, F15 PR #3452 complexity_bound_from_class, F16 manual_test_claim_for_manual_anchor). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add §5.0 theme + §5.1 acceptance-key registry rows Address briansrls inline BLOCKING on #3455:1085 — L1.13 was added without updating the §5.0 lens→theme catalog or the §5.1 canonical acceptance-key table. Those are single-authority registries downstream consumers (e.g. src/v4/lens/coverage.dag) depend on; adding a lens without the registry rows leaves them orphaned (INVARIANTS P2 violation). Added rows: - §5.0 theme catalog: L1.13 Skeleton-collapse | derive / canonical-home - §5.1 acceptance-key: L1.13 | coverage_defect_skeleton_collapse Theme rationale: 'derive' captures L1.13's core (parametric-arm duplication is hand-rolled derivation of a categorical projection); 'canonical-home' captures the Categorical dissolution (push the categorization into the input coproduct's type definition, its canonical home). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — remove advisory verdict tier; reclassify F16 as borderline Address briansrls inline BLOCKING on #3455:1109 — L1.13's verdict line created an "advisory" tier for fixtures / data tables, contradicting the universal three-disposition rule (🔴/🟡/🟢, "there is no fourth") from §5.0 / Practices 4 + 10. Fixes: 1. Verdict simplified to "hard error (🔴 dissolve-now)" with explicit note that no fourth tier exists. 2. Escape clause expanded to absorb the legitimate exceptions cleanly: - Per-arm distinct literal data (test fixtures, data tables) is Mixed under skeleton extraction → passes naturally as clean 🟢 - Distinct call arguments per arm is also Mixed for the same reason 3. F16 (manual_test_claim_for_manual_anchor) reclassified from "Outlier" to "Borderline case" — under the strict decidability rule the per-arm `claim_<name>` references are distinct free literals (K=N, Mixed). Catching F16 requires either a sub-signature L1.13.b (future) that detects per-arm-named-reference parameterization, or a separate "match-as-typed-table" lens. F16 stays in the doc as a related-pattern example for boundary clarity, NOT as a current L1.13 kill. Net: L1.13 stays clean against the three-disposition rule; F14 + F15 remain valid findings; F16 is honestly documented as out-of-current-scope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 Outlier dissolution — fix L1.1 contradiction Address briansrls inline BLOCKING on #3455:1120 — the original Outlier dissolution path advised "extract a named Bool helper / sibling lens finding (L1.1 territory)," which is EXACTLY the L1.1 predicate-dissolution anti-pattern (Bool-returning fn over a coproduct with literal true/false arms per variant). Corrected dissolution path: - Consume the discriminator structurally via match patterns + guards on the existing coproduct, OR substructure the coproduct so the one-vs-many distinction is a top-level variant. - Function body becomes a 2-arm match: `match x { <Special_pattern> => special; _ => default }` with the discriminator as a sub-pattern or guard. - DO NOT extract a named Bool helper — explicit prohibition with citation to L1.1's signature. Recent precedent updated: PR #3359 connective_spec_fact was resolved via inline match-pattern with guard, NOT a Bool helper. L1.13's "extract a discriminator" reflex must satisfy L1.1 as well as itself — the discriminant is structural (substrate-known from the parsed match), not a hand-rolled helper. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — tighten classifier thresholds, identity source, scope, clearing receipts Address operator discussion review on PR #3455 (6 points). All 6 addressed as fix-forwards: 1. Exact classifier thresholds. Distribution shapes now have precise definitions: - PureTemplate: K=1, histogram=[N] - Outlier: K=2, histogram=[N-1, 1], N≥3 - MultiOutlier (NEW): K≥2 with singletons + non-singletons, N≥4 — covers F14 (1:5:6) and F15 (1:1:7) which were misclassified as Categorical - Categorical: K≥2 with non-singleton-only groups, K≤⌊N/2⌋, N≥4 - Mixed: doesn't meet above thresholds 2. Skeleton substitution precision. The rule now states explicitly: replace EVERY occurrence of the matched-arm constructor identity in the RHS (not just the leading RHS constructor); α-rename pattern-bound names; do NOT collapse unrelated free names, literals, or call arguments. 3. Canonical-identity source. Lens consumes post-resolve/InferredTree canonical identities, not raw source spelling. Qualified names, imports, aliases, renamed bindings resolve to canonical identity before skeleton comparison. 4. Coverage key marked reserved-proposed. §5.1 row for L1.13 now flags "(reserved-proposed — enforcement not active until skeleton extraction + classifier + clearing receipts land)." 5. TotalMap scoping. Moved the substrate-dependency note to scope TotalMap to L1.13.b / future match-as-typed-table lens, NOT base L1.13. Base L1.13 (PureTemplate/Outlier/MultiOutlier/Categorical on F14+F15) has enough substrate today via fold_node + skeleton extraction; does NOT need TotalMap to fire or clear. 6. Clearing receipts explicit per shape. Each distribution shape's dissolution entry now includes a "Clearing receipt" sentence stating what receipt closes the finding. Categorical/MultiOutlier explicitly forbid "category_of(x): Category" hand-rolled projections (would just move the L1.13 violation to a new name). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add Fix-confidence axis per dissolution; cite candidate-state auto-fix flow Address operator framing: "every diagnostic can generate the correct code solution (and eventually apply it) — assuming intent is safely inferable." Each distribution shape now carries an explicit Fix-confidence field stating whether the auto-fix is: - DIRECT — Diff fully specified, no naming decisions: - PureTemplate: replace match with single shared RHS - Outlier: rewrite N-arm match to 2-arm (singleton arm + uniform catch-all) - TEMPLATED — Diff with name-holes reviewer can override: - MultiOutlier: substructure type (singleton variants + wrapping variant + sub-coproduct); default names derived from existing constructors (e.g. F14 "Modeled" + uniform group → "ModeledFeature" + "ModeledKind") - Categorical: same templated-name pattern - STRUCTURAL SKETCH (future sub-signatures only): lens identifies transform kind; concrete Diff requires human design Added top-level framing paragraph citing the §6 (find, transform) convolution view and PR #3364's candidate-state mechanism (candidate_dag = apply_diff(dag, Diff) → gate → commit if green). The fix-confidence axis is what makes L1.13 actionable rather than just diagnostic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — fix F14/F15 classifier inconsistencies; clarify arm-count framing Address cursor REQUEST_CHANGES on #3455: 1. F14 concrete-match label was "Categorical, 1:5:6" — inconsistent with the Kills line + MultiOutlier section + classifier definition. Per the classifier, Categorical requires non-singleton-only groups; 1:5:6 has a singleton (Modeled arm) → MultiOutlier. Fixed: "Categorical, 1:5:6" → "MultiOutlier, 1:5:6" with inline justification referring to the classifier definition. 2. F15 concrete-match label was "Categorical, 1:1:7" — same inconsistency. 1:1:7 has two singletons (Constant, Unknown) → MultiOutlier. Fixed analogously with inline justification. 3. F15 "9 arms to 4" exploratory observation — the clean shape's outer match has 3 arms (ClassConstant, ClassUnknown, `_`); the "4" was counting the inner 2-arm match inside the `_` branch (3 outer + 1 inner-distinct = 4 if flattened, but the structurally meaningful reduction is 9 → 3 at the outer dispatch). Clarified the framing. Root cause of inconsistency: when I introduced MultiOutlier as a distinct shape from Categorical in commit 917942a, I updated the Kills line and the shape's definition but missed updating the F14/F15 concrete-match labels at the bottom of the section. Mechanical consistency restored. P2 (single classifier authority) + P4 (decidability) now hold across classifier definition / Kills / concrete-match labels. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
T-30 — generated substrate-native hollow-alias checker
The structural enforcement tier the D2-reversal root cause named missing: a generated pure v4
.dagfunctionhollow_alias_gate: Node -> Outcome<Bool>that fails closed on a hollow alias — a carrier that reads zero spec facts from its source spec (type RustI32 = Int32and its kind).Builds on the existing P5(b) interim triple (Rust mirror
v4_hollow_alias_gate.rsetc., already on main) — does not duplicate or retire it. Retiring the mirror / wiring pipeline enforcement is the separate operator-closure step (not in this PR).What landed
src/v4/std/fact_density.dag— graduates from body-less nominal to the generated checker:SourceSpecReadFact— 3-variant classification coproduct (NamedFieldFacts/KernelAmbientAtom/NoFact).connective_spec_fact— fact-density read off aNode: own fact-edge count perstd/node.dagConnective.Atomexemption set (STRUCTURE.md "Kernel-ambient types": String/Int/Bool/Char/List/Map).hollow_alias_gate— fail-closedNode -> Outcome<Bool>;module_no_hollow_alias— whole-module fold.src/v4/test/claim/manual/fact_density_anchor.dag— v2-bootstrap compile anchor exercising the gate on the three brief cases.STRUCTURE.md/DECISIONS.md— honest enumeration;fact_density.dagstays P2-staging until operator-closure.Model (TASKS.md:1072-1076)
Node—count(carrier.children); a bare alias /Atomcarrier has zero own fact-edges.Atomwhose identity is kernel-ambient is legitimately atomic, never flagged.Rejected { diagnostic }withreason: fact_density_hollow_alias,NodeLocus,Unavailable.Structural-only read (prongs 2/3 of the Rust mirror are non-structural test-IR — confirmed by the T-4 manager against
std/node.dag).Acceptance criteria (runnable)
Result:
indexed 74 modules,compiled: 0 diagnostics,EXIT=0.The anchor file applies
hollow_alias_gateto three constructed carriers, type-checked by the compile above:anchor_hollow_alias_rejected— Atom carrier, non-kernel-ambient identity, zero facts → Rejected (fails closed).anchor_fact_bundle_produced— Conj carrier with two named fact-edges → Produced.anchor_kernel_ambient_bool_exempt— Atom carrier, kernel-ambient identity → Produced (exempt).The gate's fail-closed logic (
hollow_alias_gate/carrier_is_hollow) is an exhaustive, compiler-verifiedmatch. Runtime evaluation of the anchors is T-22-deferred, consistent with the v4 manual-anchor corpus (connective_anchors.dag).Scope note
Kernel-ambient identity symbols are self-referential
Symbolconstants (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) — not part of this checker's definition.