ROADMAP transcription: author roadmap_authority as the .dag source + fold 6 status corrections

dsl/gunbc/roadmap_document.dag

@@ -20,16 +20,17 @@
 module gunbc.roadmap_document
 
 import std.markdown { MarkdownDocument, MarkdownBlock }
-import gunbc.roadmap_model { RoadmapNode, RoadmapEdge }
+import gunbc.roadmap_model { RoadmapNode, RoadmapEdge, SectionElement }
 import gunbc.roadmap_emit { project_roadmap_section }
 
-// One ROADMAP section: an editorial title (the `##` heading) over a work-node forest. The forest is the
-// EXISTING line model (nodes + their parent/child edges) — reused whole, not re-coined. This is the
-// grouping axis the work graph itself does not carry.
+// One ROADMAP section: an editorial title (the `##` heading) over an ORDERED element sequence
+// (`SectionElement` = authored intro prose | a labelled checkbox sub-group). This subsumes the
+// slice-2 single-list section (`nodes`+`edges`) — that flat list is now one `Group` element with an
+// empty label, no fork (§3) — and carries the real ROADMAP's frame faithfully: intro prose + the
+// `◆ Milestones` spine fenced as `Prose`, the `**…:**` sub-groups as `Group`s, all in document order.
 type RoadmapSection {
   title: String
-  nodes: List<RoadmapNode>
-  edges: List<RoadmapEdge>
+  elements: List<SectionElement>
 }
 
 // The whole ROADMAP as authority. `preamble` is the document-level authored frame above the first
@@ -43,7 +44,7 @@ type RoadmapDocument {
 
 // The medium blocks for one section: delegate to the per-section projection (step-2), take its blocks.
 fn section_blocks(s: RoadmapSection, merged: List<Int>) -> List<MarkdownBlock> {
-  project_roadmap_section(title: s.title, nodes: s.nodes, edges: s.edges, merged: merged).blocks
+  project_roadmap_section(title: s.title, elements: s.elements, merged: merged).blocks
 }
 
 // THE whole-document projection (the ci.yml `project_workflow_to_yaml` analogue, markdown medium):

dsl/gunbc/roadmap_emit.dag

@@ -24,6 +24,7 @@ import std.markdown {
 import gunbc.roadmap_model {
   RoadmapNode, RoadmapEdge, PlanDocCarrier, NoCarrier, PlanDoc,
   RoadmapParent, TopLevel, UnderParent, roadmap_parent, is_top_level,
+  SectionElement, Prose, Group, SectionProse, SectionGroup,
 }
 // Completion is a Bool here (§2: roadmap_status carries no 2-variant enum restating it). The ONLY
 // checkbox-state type in the project is std.markdown's GFM glyph `CheckboxState = Checked | Unchecked`;
@@ -60,23 +61,34 @@ fn carrier_inlines(carrier: PlanDocCarrier) -> List<MarkdownInline> {
   }
 }
 
+// The `(#ref)` annotation, EMITTED FROM THE BINDING (plan TASK-2 emit-refs-from-binding, §3 single
+// authority): a DerivableLine's `prs` is the one source of both the derived box AND its rendered refs,
+// so the `(#5445/#5453)` annotation is generated here, never hand-kept in prose. An empty binding emits
+// no annotation. Mentions keep their refs in AuthoredLine prose (no binding to emit from).
+fn refs_text(prs: List<Int>) -> String {
+  fold(prs, init: "", f: (acc, p) =>
+    if acc == "" { concat("#", to_string(p)) } else { concat(acc, concat("/#", to_string(p))) })
+}
+fn refs_inlines(prs: List<Int>) -> List<MarkdownInline> {
+  if count(prs) == 0 { [] } else { [TextInline { text: concat(" (", concat(refs_text(prs: prs), ")")) }] }
+}
+// The fenced prose tail of a DerivableLine (verbatim, refs-free — the refs emit from `prs` above). A
+// leading space separates it from the title/refs; empty renders nothing.
+fn desc_inlines(description: String) -> List<MarkdownInline> {
+  if description == "" { [] } else { [TextInline { text: concat(" ", description) }] }
+}
+
 // Render the line body by arm (the fold's payoff): a DerivableLine is a BOLD title (emit applies the
-// markup) plus an optional fenced description tail; an AuthoredLine is its `content` String emitted
-// VERBATIM as a single text inline (the §5 DecodeFidelity fence — any bold/refs/links live in the
-// String, so opaque prose round-trips byte-exact). The `(#ref)` annotation from `prs` is deferred to
-// the emit-refs increment; this increment renders the structural title + carrier only.
+// markup) + its `(#ref)` annotation derived from `prs` + an optional fenced description tail; an
+// AuthoredLine is its `content` String emitted VERBATIM as a single text inline (the §5 DecodeFidelity
+// fence — any bold/refs/links live in the String, so opaque prose round-trips byte-exact).
 fn line_inlines(line: RoadmapItem) -> List<MarkdownInline> {
   match line {
-    DerivableLine { prs: _, title, description } =>
-      if description == "" {
-        [StrongInline { inlines: [TextInline { text: title }] }]
-      } else {
-        [
-          StrongInline { inlines: [TextInline { text: title }] },
-          TextInline { text: " " },
-          TextInline { text: description },
-        ]
-      }
+    DerivableLine { prs, title, description } =>
+      concat(
+        concat([StrongInline { inlines: [TextInline { text: title }] }], refs_inlines(prs: prs)),
+        desc_inlines(description: description),
+      )
     AuthoredLine { done: _, content } => [TextInline { text: content }]
   }
 }
@@ -127,14 +139,39 @@ fn task_item_for(rn: RoadmapNode, nodes: List<RoadmapNode>, edges: List<RoadmapE
 
 // === The section projection ==================================================
 
-// One ROADMAP section: an H2 heading + a task list of its top-level nodes (each nesting its children
-// as the indentation = dependency forest). The whole-document projection maps this over sections.
-fn project_roadmap_section(title: String, nodes: List<RoadmapNode>, edges: List<RoadmapEdge>, merged: List<Int>) -> MarkdownDocument {
-  let tops = nodes |> filter(n => is_top_level(edges: edges, node: n.node))
-  MarkdownDocument {
-    blocks: [
-      HeadingBlock { level: H2, inlines: [TextInline { text: title }] },
-      TaskListBlock { items: tops |> map(n => task_item_for(rn: n, nodes: nodes, edges: edges, merged: merged, fuel: roadmap_max_depth())) },
+// One checkbox sub-group's blocks: an optional `**{label}:**` heading-paragraph (the UNIFORM frame the
+// projection owns — §3 single authority, see roadmap_model.SectionGroup) followed by a task list of its
+// top-level nodes (each nesting its children as the indentation = dependency forest). An empty label
+// emits the bare list with no preceding label paragraph.
+fn group_blocks(g: SectionGroup, merged: List<Int>) -> List<MarkdownBlock> {
+  let tops = g.nodes |> filter(n => is_top_level(edges: g.edges, node: n.node))
+  let list = TaskListBlock { items: tops |> map(n => task_item_for(rn: n, nodes: g.nodes, edges: g.edges, merged: merged, fuel: roadmap_max_depth())) }
+  if g.label == "" {
+    [list]
+  } else {
+    [
+      ParagraphBlock { inlines: [StrongInline { inlines: [TextInline { text: concat(g.label, ":") }] }] },
+      list,
     ]
   }
 }
+
+// One section element's blocks: authored prose emitted VERBATIM as a single-TextInline paragraph (the
+// §5 fence — markup inside the String passes through untouched), or a checkbox sub-group.
+fn element_blocks(e: SectionElement, merged: List<Int>) -> List<MarkdownBlock> {
+  match e {
+    Prose { prose } => [ParagraphBlock { inlines: [TextInline { text: prose.content }] }]
+    Group { group } => group_blocks(g: group, merged: merged)
+  }
+}
+
+// One ROADMAP section: an H2 heading + its ordered element sequence (intro prose, the `◆ Milestones`
+// spine, then one-or-more labelled checkbox sub-groups — interleaved IN DOCUMENT ORDER). A pure fold
+// over `elements` preserving order; the whole-document projection maps this over sections.
+fn project_roadmap_section(title: String, elements: List<SectionElement>, merged: List<Int>) -> MarkdownDocument {
+  MarkdownDocument {
+    blocks: fold(elements,
+      init: [HeadingBlock { level: H2, inlines: [TextInline { text: title }] }],
+      f: fn(acc, e) { concat(acc, element_blocks(e: e, merged: merged)) })
+  }
+}

dsl/gunbc/roadmap_model.dag

@@ -60,6 +60,38 @@ type RoadmapEdge {
   parent: ProcessNodeId
 }
 
+// === Section content: the frame-is-the-win element sequence ==================
+//
+// A real ROADMAP `##` section is NOT a single flat checkbox list (what the slice-2 RoadmapSection
+// assumed): it interleaves authored INTRO prose (the section rationale, the `◆ Milestones` spine, a
+// `→ [plan](…)` pointer) with one-or-MORE labelled checkbox SUB-GROUPS (`**Audits (done):**`,
+// `**In-scope this window:**`). `SectionElement` is that ordered sequence — the frame-is-the-win
+// faithful model of the section: model the FRAME (sub-group boxes + their bindings), FENCE the prose.
+//
+// - `SectionProse` carries authored prose VERBATIM (the §5 DecodeFidelity fence): an opaque String
+//   emitted as a paragraph, ALL markup (bold/links/refs/code-spans) living inside it. It is NOT modelled
+//   into medium constructs — fake-modelling prose is the forbidden over-reach (plan §5).
+// - `SectionGroup` is one checkbox list: an authored `label` + its node/edge forest (the EXISTING line
+//   model, reused whole). The label is SEMANTIC TEXT, not literal markup: every real sub-group renders as
+//   the UNIFORM `**{label}:**` frame, so the bold+colon is a rendering convention the projection owns
+//   (single authority, §3) — not the `**…:**` repeated in every String. An empty `label` is the bare
+//   unlabelled `[ ]`-list that opens a section (no label paragraph emitted).
+type SectionProse { content: String }
+type SectionGroup { label: String, nodes: List<RoadmapNode>, edges: List<RoadmapEdge> }
+
+// The ordered content of a section: authored prose, or a checkbox sub-group. A closed sum so the
+// emitter dispatches the two renderings (a verbatim paragraph vs a task list) — no Optional straddle.
+type SectionElement
+  = Prose { prose: SectionProse }
+  | Group { group: SectionGroup }
+
+// Typed constructors so an element literal in list position carries its declared SectionElement type
+// (a bare inline payload arm is read as a Product, cf. roadmap_parent above).
+fn section_prose(content: String) -> SectionElement { Prose { prose: SectionProse { content: content } } }
+fn section_group(label: String, nodes: List<RoadmapNode>, edges: List<RoadmapEdge>) -> SectionElement {
+  Group { group: SectionGroup { label: label, nodes: nodes, edges: edges } }
+}
+
 // === Dependency projection: the indentation edge ============================
 
 // Where a roadmap line sits in the forest. A closed domain sum, NOT `ProcessNodeId?` — the Optional

dsl/test/claim/roadmap_authority_test.dag

@@ -0,0 +1,154 @@
+// dsl/test/claim/roadmap_authority_test.dag — §5 by-execution proof for gunbc.roadmap_authority.
+//
+// Proves the REAL-ROADMAP transcription projects faithfully: the whole document emits, the FRAME is
+// modelled (sections + nested checkbox forests + sub-group labels + plan pointers), the 6 STATUS
+// CORRECTIONS are authored to MERGED REALITY, refs emit FROM THE BINDING, and warm-lark-306's two
+// invariants hold — (a) authored prose emits BYTE-VERBATIM including its internal markup (the §5 fence),
+// (b) a section is an ORDERED element sequence (intro prose → ◆ Milestones → sub-groups, in order).
+// Discriminating: a perturbed merged set flips a DERIVED box (the binding has teeth), prose markup is
+// asserted byte-exact (a mangle goes red), and a reversed-order adjacency is asserted ABSENT.
+//
+// The effectful drift gate (read the committed ROADMAP.md, byte-compare) is the SEPARATE RoadmapGate
+// variant, deferred until the file is fully emittable (warm-lark-306) — Filesystem.Read is a host effect
+// and cannot live in a pure witness.
+
+module test.claim.roadmap_authority
+
+import extdeps.languages.markdown { serialize_markdown_source }
+import gunbc.roadmap_document { project_roadmap_to_markdown }
+import gunbc.roadmap_authority { roadmap_authority }
+
+// The merged-PR set = current MAIN reality (the PRs that have actually landed; step-3b #5529 is NOT in
+// it — the inversion sub-rows are authored to what merged, not to the incoming PR).
+fn merged() -> List<Int> {
+  [5428, 5445, 5453, 5433, 5476, 5473, 5456, 5470, 5478, 5421, 5425, 5236,
+   5437, 5434, 5441, 5449, 5471, 5430, 5481, 5491, 5508, 5520, 5525, 5527]
+}
+
+fn emit_with(m: List<Int>) -> String {
+  serialize_markdown_source(doc: project_roadmap_to_markdown(doc: roadmap_authority(), merged: m))
+}
+fn out() -> String { emit_with(m: merged()) }
+
+// === Frame: all sections + the preamble project =============================
+
+fn witness_frame_all_sections() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "# gunbc — Roadmap")
+    && string_contains(s: o, pattern: "## 0. Fail-closed lock-down")
+    && string_contains(s: o, pattern: "## 1. CI under control")
+    && string_contains(s: o, pattern: "## 2. Minimal work")
+    && string_contains(s: o, pattern: "## 3. Complexity budget gate")
+    && string_contains(s: o, pattern: "## 4. Testgen as the bug-class oracle")
+    && string_contains(s: o, pattern: "## 5. Self-host v2")
+    && string_contains(s: o, pattern: "## 6. idea → idea compiler")
+    && string_contains(s: o, pattern: "## 7. HTML / React rendering")
+    && string_contains(s: o, pattern: "## 8. Session dashboard on `.dag` (SHELVED)")
+}
+
+// Sub-group labels render as the uniform `**{label}:**` frame (projection-owned, single authority).
+fn witness_subgroup_labels() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "**Audits (done):**")
+    && string_contains(s: o, pattern: "**In-scope this window:**")
+    && string_contains(s: o, pattern: "**Fenced OUT (after stability):**")
+    && string_contains(s: o, pattern: "**Meta — lock down the reasoning (§7 recursion):**")
+}
+
+// === emit-refs-from-binding (plan TASK-2, §3 single authority) ===============
+
+// A DerivableLine's `(#ref)` is GENERATED from `prs` — single (#N) and multi (#N/#M). The numeric-tower
+// row binds [5428]; the realization-vocab row binds [5445, 5453] → `(#5445/#5453)`.
+fn witness_emit_refs_from_binding() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "**numeric-tower grounding** (#5428)")
+    && string_contains(s: o, pattern: "**realization-vocabulary containment guard** (#5445/#5453)")
+}
+
+// === The 6 status corrections (authored to MERGED REALITY) ===================
+
+// C1 — MEASURE ROWS (bright-stag-194): missing from the committed ROADMAP; #5470/#5478 merged → DERIVED
+// `[x]`, the FLOOR + demand-CEIL families, refs from the binding.
+fn witness_c1_measure_rows() -> Bool {
+  string_contains(s: out(),
+    pattern: "- [x] **Section 1 spawn-width foundation — std.measure expressibility** (#5470/#5478)")
+}
+// C2 — ROUND-TRIP LAW (bright-stag + quick-seal-137): its OWN `[x]` row bound to #5525/#5527 (two media),
+// DISTINCT from the medium-axis checkmark — no overclaim that the medium checkmark = round-trip-complete.
+fn witness_c2_roundtrip_law() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "- [x] **round-trip law (ingest∘emit = id, DecodeFidelity-bounded)** (#5525/#5527)")
+    && string_contains(s: o, pattern: "- [x] **medium axis** —")
+    && string_contains(s: o, pattern: "per-medium round-trips are v1-seed interim")
+}
+// C3 — INVERSION SUB-ROWS (warm-lark-306): slice-1/slice-2/step-3a landed → DERIVED `[x]` bound to
+// #5491/#5508/#5520 (step-3b #5529 intentionally NOT in the set — authored to merged reality).
+fn witness_c3_inversion_subrows() -> Bool {
+  string_contains(s: out(),
+    pattern: "- [x] **PR→checkbox status + section-emit + projection layer** (#5491/#5508/#5520)")
+}
+// C4 — SELF-HOST PATH-A no-overclaim (bright-stag): #5481 landed (in the spine) but §7 regen-fixpoint is
+// DEFERRED and src/v1 is NOT yet deletable — the milestone must NOT read as "self-host done".
+fn witness_c4_selfhost_no_overclaim() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "class-3 corpus-coherence + cargo-green seed ✓ (#5481)")
+    && string_contains(s: o, pattern: "§7 regen-fixpoint deferred, #5514; src/v1 NOT yet deletable")
+    && string_contains(s: o, pattern: "**TERMINAL: `src/v1` deleted**")
+}
+// C5 — edge-(b) / .dag→rust coverage wall (bright-stag): SCOPED / pending operator greenlight, NOT
+// greenlit — no status change, the rust-gate coverage row stays `[ ]`.
+fn witness_c5_rust_gate_not_greenlit() -> Bool {
+  string_contains(s: out(), pattern: "- [ ] **rust-gate coverage** (shared §1)")
+}
+
+// === Invariant (a): authored prose emits BYTE-VERBATIM including its markup (the §5 fence) ===
+
+// The §2 ◆ Milestones spine is authored prose; its internal markup (bold, the ✓ glyph, and a `(#5425)`
+// that is PROSE — not a binding) passes through UNTOUCHED. A mangled fence (stripped bold/glyph, or a
+// (#5425) "helpfully" re-emitted) makes this go red.
+fn witness_a_prose_verbatim() -> Bool {
+  string_contains(s: out(),
+    pattern: "**◆ Milestones:** key-by-construction ✓ (#5425) → **▸ warm==cold purity proven (616/616, #5429)**")
+}
+
+// === Invariant (b): the section is an ORDERED element sequence ===============
+
+// §0 in document order: intro prose → window note → ◆ Milestones spine → Audits sub-group. The exact
+// `tail\n\nhead` adjacencies hold ONLY if order is preserved (a reorder breaks every one of them).
+fn witness_b_ordered_interleaving() -> Bool {
+  let o = out()
+  string_contains(s: o, pattern: "([DESIGN §5](DESIGN.md)).\n\nThis window = a few days of STABILITY")
+    && string_contains(s: o, pattern: "[fork plan](docs/plans/model-realization-fork.md) §3).\n\n**◆ Milestones:** fail-open audited")
+    && string_contains(s: o, pattern: "`Value::Null` split *(deep root)*\n\n**Audits (done):**")
+}
+// Discriminating negative: if the element order were lost (sub-group hoisted before the prose), the
+// Audits label would sit immediately before the window prose — assert that adjacency is ABSENT.
+fn witness_b_order_discriminator() -> Bool {
+  !string_contains(s: out(), pattern: "**Audits (done):**\n\nThis window = a few days of STABILITY")
+}
+
+// === Discriminating: the DERIVED box is a function of the merged set =========
+
+// numeric-tower (#5428) and measure (#5470/#5478) are DERIVED `[x]` when merged; drop those PRs and the
+// SAME lines derive `[ ]` (the box is computed from the binding, not baked) — the inversion has teeth.
+fn witness_derivation_has_teeth() -> Bool {
+  let dropped = emit_with(m: [5445, 5453, 5433, 5476, 5473, 5456, 5421, 5425])
+  string_contains(s: dropped, pattern: "- [ ] **numeric-tower grounding** (#5428)")
+    && string_contains(s: dropped, pattern: "- [ ] **Section 1 spawn-width foundation — std.measure expressibility** (#5470/#5478)")
+    && !string_contains(s: dropped, pattern: "- [x] **numeric-tower grounding** (#5428)")
+}
+
+test fn roadmap_authority_witnesses() -> Bool {
+  witness_frame_all_sections()
+    && witness_subgroup_labels()
+    && witness_emit_refs_from_binding()
+    && witness_c1_measure_rows()
+    && witness_c2_roundtrip_law()
+    && witness_c3_inversion_subrows()
+    && witness_c4_selfhost_no_overclaim()
+    && witness_c5_rust_gate_not_greenlit()
+    && witness_a_prose_verbatim()
+    && witness_b_ordered_interleaving()
+    && witness_b_order_discriminator()
+    && witness_derivation_has_teeth()
+}