Sweep plan citations onto verified symbols (batch 3)

dag/gunbc/plans/cardinality_refinement.dag

@@ -7,31 +7,30 @@ import gunbc.plans.md_helpers { h2, p, li, ul, ol }
 fn cardinality_refinement_body() -> List<MarkdownBlock> {
   [
     p(text: "**Status:** scoping (Feature-1 from the byte-grounding thread). **DESIGN.md + carriers are authority** (§6 no parallel ledger); each item dissolves into a wired parser/checker change + a green witness when it lands."),
-    p(text: "**Verified against the live tree 2026-06-22.** Line numbers are receipts; re-check before acting."),
+    p(text: "**Verified against the live tree 2026-07-31.** Symbols, not line positions, are receipts; re-check the cited declarations before acting."),
     h2(text: "0. Thesis — cardinality is ONE axis, and it is the *decidable* refinement fragment"),
     p(text: "\"Is it empty\", \"does it have N\", \"did `Int64` overflow\" are the same question — a **cardinality constraint** — answered today by scattered manual `if list_length(..) == 0` / `count` / bound checks. Model cardinality as a refinement **axis** and two things fall out:"),
     ol(items: [
-      li(text: "**Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`admits: fn(B) -> Bool`, `refinement.dag:34`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it."),
+      li(text: "**Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`v2.std.refinement` `Validation.admits: fn(B) -> Bool`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it."),
       li(text: "**Fold-propagation (the payoff).** A catamorphism that carries the cardinality means folding a `List<Bit>` yields its length, adding two bounded `Int64` yields the combined bound (and **overflow is a typed `Rejected`, not a silent wrap**). \"When we fold, it's handled automatically\" — the empty/count/width checks stop being hand-written."),
     ]),
     h2(text: "1. What is ALREADY built (this is wiring, not greenfield)"),
     ul(items: [
-      li(text: "**Value-level refinement substrate — `v2.std.refinement`:** `Validation<B> \{ reason, admits: fn(B)->Bool \}`, `Refined<B> \{ base \}`, and `refine<B>(base, by, at) -> Outcome<Refined<B>>` (`:74`) which checks `admits(base)` and returns `Accepted\{Refined\}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements."),
-      li(text: "**Its own documented gaps:** `🟡 feature:refinement-opaque-carrier / T-25-tail` (`:65`) — bare `Refined \{ base \}` can still bypass `refine`; construction is **not compiler-enforced** yet."),
-      li(text: "**The phantom-width gap — `std.machine_constraints`:** `type MachineWidth<bits>` (`:47`) is a phantom; its TRACKED PARAMETER GAP (`:34-46`) names the exact trigger: *\"substrate grammar for bounded phantom parameters tying `bits` to `Nat`, or a non-phantom `MachineWidth` indexed by an explicit `Nat` carrier.\"* No reflection of `N` to a value."),
-      li(text: "**The structural carriers exist, unchecked — `std.bit`:** `Byte \{ bits: List<Bit> \}` (`bit.dag:25`), header concedes *\"cardinality is not enforced … no lowered field refinement, type-alias `where` is skipped in the handwritten parser.\"*"),
-      li(text: "**A waiting consumer — `std.measure`:** `Refined<Measure<…>, predicate>` is explicitly **deferred** (`measure.dag:8,245`), waiting on exactly this."),
+      li(text: "**Value-level refinement substrate — `v2.std.refinement`:** `Validation`, `Refined`, and `refine` check `Validation.admits` and return `Accepted\{Refined\}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements."),
+      li(text: "**The carrier has not consumed the existing construction wall:** `v2.std.refinement` `Refined` exposes its `base` field and is not marked `sole_constructor`. The compiler already refuses cross-module construction of `sole_constructor` records through `v1.compiler.infer` `type_has_sole_constructor` / `SoleConstructorViolation`; per DESIGN §4b, its completeness for generic refinement carriers, every construction form, and compiler-module exemptions is **unverified**, not absent."),
+      li(text: "**The phantom-width gap — `std.machine_constraints` `MachineWidth`:** the declaration has a type parameter but no value carrier. No reflection of `N` to a value exists."),
+      li(text: "**The structural carrier exists, unchecked — `std.bit` `Byte`:** its `bits: List<Bit>` field carries no cardinality refinement."),
     ]),
     h2(text: "2. The gap, decomposed (each piece → a real surface)"),
     ul(items: [
-      li(text: "[ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Parser: extend the type-RHS path (`parse_type_rhs_after_eq`, named in `machine_constraints.dag:109`) and the record-field path to accept `where <cardinality-pred>`; lex the `where` keyword. Normalize: at the `^dag_surface_type_alias_rhs` hook (`03_normalize.dag:90`) lower `where P` into a `Validation` + a **refined-construction obligation** on the type. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression."),
-      li(text: "[ ] **P2 — compiler-enforced construction (closes T-25-tail).** Checker: at a construction site of a refined type, require the obligation discharged — bare `Byte \{ bits: … \}` outside the sanctioned `refine`/smart-constructor is a located `Rejected`, never silent. This is what turns \"documented intent\" into \"illegal-state-unwritable.\""),
-      li(text: "[ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length<N>` (`== N`), `NonEmpty` (`≥ 1`), `Bounded<Lo,Hi>`, `Width<N>` (the `MachineWidth` bound). All are linear-arithmetic over `list_length` (`types.dag:233`) / magnitude — decidable. `Byte = \{ bits: List<Bit> \} where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.**"),
+      li(text: "[ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Extend `v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr` and the record-field grammar to accept `where <cardinality-pred>`. Register the emitted surface form through `v2.std.compilers.sugar` and lower it through `v2.compiler.normalize` `normalize_sugar_key_optional` into a `Validation` + a **refined-construction obligation**. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression."),
+      li(text: "[ ] **P2 — audit and consume the existing construction wall (closes T-25-tail).** First run discriminating positive/negative probes for `sole_constructor` on generic `Refined<B>`, every record-construction form, and the compiler-module exemptions named by DESIGN §4b. If that audit is complete, mark the canonical refinement carrier and route sanctioned construction through `refine`/its smart constructor; if a probe escapes, extend the existing wall at that measured gap rather than minting a parallel checker. The required outcome is that bare refined construction outside the sanctioned factory produces a located `SoleConstructorViolation`, never silent acceptance."),
+      li(text: "[ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length<N>` (`== N`), `NonEmpty` (`≥ 1`), `Bounded<Lo,Hi>`, `Width<N>` (the `MachineWidth` bound). All are linear-arithmetic over `std.types` `list_length` / magnitude — decidable. `Byte = \{ bits: List<Bit> \} where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.**"),
       li(text: "[ ] **P4 — fold-propagation (the novel, high-value piece).** Extend the catamorphism (`fold_node` / the reduce) so a cardinality fact is COMPUTED through a fold: `Cons/Empty` over a list yields its length; combining two `Bounded` magnitudes yields the combined bound, and a bound exceeding the `Width` is a typed overflow `Rejected`. Connect to the existing cost-through-folds algebra (`induction.dag` PolyCost/exponents) — cardinality is the same shape (a count tracked through a catamorphism) as the cost lens already computes."),
-      li(text: "[ ] **P5 (stretch) — type-level-Nat reflection.** Reflect `MachineWidth<N>`'s `N` to a value (the phantom→value bridge named in `machine_constraints.dag:43-46`), so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal."),
+      li(text: "[ ] **P5 (stretch) — type-level-Nat reflection.** Add the value bridge absent from `std.machine_constraints` `MachineWidth`, so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal."),
     ]),
     h2(text: "3. Where it plugs into the pipeline"),
-    p(text: "`tokenize` (lex `where`) → `parse` (`parse_type_rhs_after_eq`: parse the cardinality pred, attach to the type-decl `Node`) → `normalize` (`dag_surface_type_alias_rhs`: desugar to `Validation` + the construction obligation) → `infer` (`04_infer`: discharge the obligation at construction sites — the decidable cardinality check — and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time)."),
+    p(text: "`tokenize` (lex `where`) → `parse` (`v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr`: attach the cardinality predicate to an emitted surface node) → `normalize` (`v2.compiler.normalize` `normalize_sugar_key_optional`: desugar through the sugar registry to `Validation` + the construction obligation) → `infer` (discharge the obligation at construction sites and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time)."),
     h2(text: "4. The decidability boundary (the one rule that keeps this §4-legal)"),
     p(text: "Two tiers, and the split is the whole discipline:"),
     ul(items: [
@@ -46,13 +45,13 @@ fn cardinality_refinement_body() -> List<MarkdownBlock> {
       li(text: "**Phase-3 — P5 reflection; lift cardinality checks fully static** where the count is known at type level."),
     ]),
     h2(text: "6. What one feature unblocks (the ROI)"),
-    p(text: "Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; `Measure<Q,S>` inhabitance (the deferred `Refined<Measure>`); typed `|>` coercion (the Measure-inhabitance gap blocked it last week); `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings."),
+    p(text: "Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; typed `|>` coercion; `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings."),
     h2(text: "7. Risks / hard parts"),
     ul(items: [
       li(text: "**Decidability discipline** (§4) — the failure mode is P3/P4 quietly admitting a non-cardinality predicate; gate it to the closed vocabulary."),
       li(text: "**Fold-propagation soundness** — the cardinality a fold computes must be *provably* the real one (a fail-closed witness: a fold that miscounts goes RED)."),
-      li(text: "**The parser is handwritten** (`bit.dag` header) — `where` lexing/parsing touches the seed parser (load-bearing; sequence behind the §0 lock-down, not during it)."),
-      li(text: "**P2 is broad** — construction-enforcement touches every construction site of a refined type."),
+      li(text: "**The parser/normalizer path is load-bearing** — `where` must enter through the modeled grammar and sugar registry, sequenced behind the §0 lock-down."),
+      li(text: "**P2 completeness is unverified** — audit the existing `sole_constructor` wall across generic carriers, every construction form, and compiler-module exemptions before declaring the attainable ceiling or extending enforcement."),
     ]),
   ]
 }