ROADMAP slice-2 step-2: emit a section from the work-DAG model + §2 delete redundant box enum

dsl/gunbc/roadmap_emit.dag

@@ -0,0 +1,117 @@
+// gunbc/roadmap_emit.dag — project the roadmap work-model to Markdown (slice-2 step 2).
+//
+// SCAFFOLD (DESIGN §7 self-host / plan §6): the ROADMAP-specific projection in the SAME shape as
+// ci.yml's `expected_ci_yml = serialize_yaml(project_workflow_to_yaml(...))` — here
+// `expected_roadmap_md = serialize_markdown_source(project_roadmap_to_markdown(...))`, a dsl
+// serializer fold on the v1 seed. The generic Markdown medium is deep-newt's
+// `std.markdown` + `extdeps.languages.markdown.serialize_markdown_source` (row-driven). This module
+// owns ONLY the roadmap→Markdown projection; the medium is not re-modeled here.
+// dissolution-trigger: the eventual v2 Markdown TargetModel (one grammar both ways, §4) supersedes
+//   the dsl serializer fold — at which point `project_roadmap_to_markdown` emits v2 Nodes and this
+//   composition retires, exactly as `serialize_yaml`/`ci_yaml_emit` will.
+//
+// The checkbox cell is where the DONE-authority decision lands (plan §6.1): a CompletesIff line's box
+// is DERIVED from the merged-PR set (the inversion — generated, not hand-toggled); a HandChecked
+// line's box is the AUTHORED one (honest un-derivable residue). So the generated ROADMAP cannot carry
+// a stale checkbox on a PR-bound line.
+
+module gunbc.roadmap_emit
+
+import std.markdown {
+  MarkdownDocument, MarkdownBlock, MarkdownInline, HeadingBlock, ParagraphBlock, TaskListBlock,
+  MarkdownTaskItem, StrongInline, TextInline, LinkInline, H2, Checked, Unchecked,
+}
+import gunbc.roadmap_model {
+  RoadmapNode, RoadmapEdge, PlanDocCarrier, NoCarrier, PlanDoc,
+  RoadmapParent, TopLevel, UnderParent, roadmap_parent, is_top_level,
+}
+// 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`;
+// this module maps the Bool onto that glyph in `task_item_with` below. The completion concept (Bool,
+// roadmap_status) and the render-glyph concept (std.markdown.CheckboxState) stay distinct (§3).
+import gunbc.roadmap_status { entry_is_done }
+import ctrl.process_algebra { ProcessNodeId }
+
+// Bounded nesting depth — the roadmap forest is shallow (sections → items → sub-items). Explicit fuel
+// gives the recursion its strict-descent evidence (DESIGN §4 bounded-and-forward); a tree deeper than
+// this truncates, which is loud (a missing deep item is visible drift), not silent corruption.
+fn roadmap_max_depth() -> Int { 8 }
+
+// === The checkbox cell — DONE-authority (plan §6.1) ==========================
+
+// Whether a line's box SHOULD read done — the DONE-authority decision (plan §6.1), delegated whole to
+// `roadmap_status.entry_is_done` (CompletesIff → derived from the merged set; HandChecked → authored).
+// Kept as a Bool so the markdown glyph lands in `MarkdownTaskItem.state` field position below.
+fn node_is_done(rn: RoadmapNode, merged: List<Int>) -> Bool {
+  entry_is_done(entry: rn.line, merged: merged)
+}
+
+// === Inline content — bold title + optional plan-doc link ====================
+
+fn carrier_inlines(carrier: PlanDocCarrier) -> List<MarkdownInline> {
+  match carrier {
+    NoCarrier => []
+    PlanDoc { path } => [
+      TextInline { text: " " },
+      LinkInline { inlines: [TextInline { text: "plan" }], url: path },
+    ]
+  }
+}
+
+fn node_inlines(rn: RoadmapNode) -> List<MarkdownInline> {
+  concat(
+    [StrongInline { inlines: [TextInline { text: rn.line.title }] }],
+    carrier_inlines(carrier: rn.carrier),
+  )
+}
+
+// === The forest projection ===================================================
+
+// Direct children of `parent`: nodes whose decomposition parent is `parent`.
+fn children_of(nodes: List<RoadmapNode>, edges: List<RoadmapEdge>, parent: ProcessNodeId) -> List<RoadmapNode> {
+  nodes |> filter(n => match roadmap_parent(edges: edges, node: n.node) {
+    UnderParent { parent: p } => p == parent
+    TopLevel => false
+  })
+}
+
+// Build a task item from its done-flag + blocks. The glyph (`Checked`/`Unchecked`) sits DIRECTLY in
+// `state:` field position in each branch — a bare nullary markdown constructor only resolves where its
+// type (`MarkdownTaskItem.state`) is the expected type pushed onto it; it does NOT resolve through an
+// `if`/match-arm into the field, nor inside a match-arm body (read there as a variable). Both branches
+// build the same record type, so they unify cleanly.
+fn task_item_with(done: Bool, blocks: List<MarkdownBlock>) -> MarkdownTaskItem {
+  if done {
+    MarkdownTaskItem { state: Checked, blocks: blocks }
+  } else {
+    MarkdownTaskItem { state: Unchecked, blocks: blocks }
+  }
+}
+
+// Map a roadmap node to a task item, nesting its children one indent level (fuel-bounded, §4). The
+// status box is the DONE-authority decision (plan §6.1): CompletesIff → derived from the merged set,
+// HandChecked → authored.
+fn task_item_for(rn: RoadmapNode, nodes: List<RoadmapNode>, edges: List<RoadmapEdge>, merged: List<Int>, fuel: Int) -> MarkdownTaskItem {
+  let para = ParagraphBlock { inlines: node_inlines(rn: rn) }
+  let kids = if fuel > 0 { children_of(nodes: nodes, edges: edges, parent: rn.node) } else { [] }
+  let blocks = if count(kids) > 0 {
+    [para, TaskListBlock { items: kids |> map(k => task_item_for(rn: k, nodes: nodes, edges: edges, merged: merged, fuel: fuel - 1)) }]
+  } else {
+    [para]
+  }
+  task_item_with(done: node_is_done(rn: rn, merged: merged), blocks: blocks)
+}
+
+// === 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())) },
+    ]
+  }
+}

dsl/gunbc/roadmap_status.dag

@@ -28,10 +28,6 @@ module gunbc.roadmap_status
 
 import extdeps.github.pulls { PullRequest }
 
-// The committed checkbox a ROADMAP line asserts. Legend: `[x]` done · `[ ]` todo — markdown carries
-// no third state, so a two-variant closed sum.
-type CheckboxState = Done | Todo
-
 // The §5 boundary between a checkbox that can be DERIVED and one that must stay hand-checked.
 type CompletionBinding
   // Explicit "this line is done IFF every one of these PRs merges" — the work-DAG authority edge.
@@ -42,10 +38,14 @@ type CompletionBinding
   // The honest un-derivable residue — hand-checked, NEVER gated.
   | HandChecked
 
-// A roadmap line's status surface: its title, the box it commits, and its completion binding.
+// A roadmap line's status surface: its title, whether the committed box reads done, and its completion
+// binding. The box is a plain Bool — markdown carries no third checkbox state, so completion is exactly
+// 2-valued; the GFM render-glyph (`std.markdown.CheckboxState = Checked | Unchecked`) is a SEPARATE
+// medium concept the emit projection maps this Bool onto (§2: don't restate a Bool as a 2-variant enum;
+// §3: completion ≠ glyph).
 type RoadmapStatusEntry {
   title: String
-  claimed: CheckboxState
+  claimed_done: Bool
   binding: CompletionBinding
 }
 
@@ -67,16 +67,25 @@ fn merged_pr_numbers(prs: List<PullRequest>) -> List<Int> {
   prs |> filter(pr => pr_merged(pr: pr)) |> map(pr => pr.number)
 }
 
-// === Derivation: the checkbox an explicitly-bound line SHOULD show ===========
+// === Derivation: whether an explicitly-bound line SHOULD read done ============
+
+// Done iff the binding is non-empty and EVERY bound PR merged — THE completion authority, a plain Bool
+// (no 2-variant enum restating it, §2). Single authority for the predicate, so the drift gate and the
+// emit projection both reuse it. Defined over the PR list of a CompletesIff binding only — a HandChecked
+// line has no derived box. An empty binding is not derivably-done (no merge evidence) → false,
+// fail-closed.
+fn prs_all_merged(prs: List<Int>, merged: List<Int>) -> Bool {
+  count(prs) > 0 && all(prs, r => merged |> any(m => m == r))
+}
 
-// Done iff the binding is non-empty and EVERY bound PR merged. Defined over the PR list of a
-// CompletesIff binding only — a HandChecked line has no derived box at all (it is residue, below).
-// An empty binding is not derivably-done (no merge evidence) → Todo, fail-closed.
-fn derive_checkbox(prs: List<Int>, merged: List<Int>) -> CheckboxState {
-  if count(prs) > 0 && all(prs, r => merged |> any(m => m == r)) {
-    Done
-  } else {
-    Todo
+// The done-ness an entry's box SHOULD show: DERIVED (every bound PR merged) for a CompletesIff binding
+// — the inversion; the AUTHORED box for a HandChecked line — honest residue (§5 DecodeFidelity). THE
+// completion authority the emitted checkbox glyph maps from (a Bool — the emit projection turns it into
+// `std.markdown.CheckboxState`, which it alone names).
+fn entry_is_done(entry: RoadmapStatusEntry, merged: List<Int>) -> Bool {
+  match entry.binding {
+    CompletesIff { prs } => prs_all_merged(prs: prs, merged: merged)
+    HandChecked => entry.claimed_done
   }
 }
 
@@ -92,7 +101,7 @@ fn status_drift(entry: RoadmapStatusEntry, merged: List<Int>) -> DriftVerdict {
   match entry.binding {
     HandChecked => Underivable
     CompletesIff { prs } =>
-      if entry.claimed == derive_checkbox(prs: prs, merged: merged) {
+      if entry.claimed_done == prs_all_merged(prs: prs, merged: merged) {
         Clean
       } else {
         Drifted

dsl/test/claim/roadmap_emit_test.dag

@@ -0,0 +1,71 @@
+// dsl/test/claim/roadmap_emit_test.dag — §5 proof for gunbc.roadmap_emit (slice-2 step 2).
+//
+// Proves BY EXECUTION that project_roadmap_to_markdown ∘ serialize_markdown_source produces the right
+// ROADMAP bytes: a CompletesIff line whose PR merged renders `- [x]` (DERIVED, the inversion), a
+// HandChecked line renders its AUTHORED box, a child node nests one indent level, and a plan-doc
+// carrier renders as a link. Discriminating: flip the merged set and the derived `[x]` becomes `[ ]`.
+
+module test.claim.roadmap_emit
+
+import extdeps.languages.markdown { serialize_markdown_source }
+import gunbc.roadmap_emit { project_roadmap_section }
+import gunbc.roadmap_model { RoadmapNode, RoadmapEdge, PlanDocCarrier, NoCarrier, PlanDoc }
+import gunbc.roadmap_status { RoadmapStatusEntry, CompletesIff, HandChecked }
+import ctrl.process_algebra { ProcessNodeId }
+
+data parent_id: ProcessNodeId = "invert-hand-maintained"
+data child_id: ProcessNodeId = "pr-checkbox-status"
+
+fn parent_node() -> RoadmapNode {
+  RoadmapNode {
+    node: parent_id,
+    line: RoadmapStatusEntry { title: "invert hand-maintained", claimed_done: false, binding: HandChecked },
+    carrier: PlanDoc { path: "docs/plans/invert-hand-maintained.md" },
+  }
+}
+
+// CompletesIff #5491 — box DERIVED from the merged set.
+fn child_node() -> RoadmapNode {
+  RoadmapNode {
+    node: child_id,
+    line: RoadmapStatusEntry { title: "PR-checkbox status", claimed_done: false, binding: CompletesIff { prs: [5491] } },
+    carrier: NoCarrier,
+  }
+}
+
+fn nodes() -> List<RoadmapNode> { [parent_node(), child_node()] }
+fn edges() -> List<RoadmapEdge> { [RoadmapEdge { child: child_id, parent: parent_id }] }
+
+fn emit(merged: List<Int>) -> String {
+  serialize_markdown_source(doc: project_roadmap_section(
+    title: "6. Expansion", nodes: nodes(), edges: edges(), merged: merged,
+  ))
+}
+
+// The H2 heading renders.
+fn witness_heading() -> Bool {
+  string_contains(s: emit(merged: [5491]), pattern: "## 6. Expansion")
+}
+// The HandChecked parent renders its AUTHORED [ ] box + the plan-doc link.
+fn witness_parent_authored_box_and_link() -> Bool {
+  let out = emit(merged: [5491])
+  string_contains(s: out, pattern: "- [ ] **invert hand-maintained**")
+    && string_contains(s: out, pattern: "[plan](docs/plans/invert-hand-maintained.md)")
+}
+// The CompletesIff child whose PR #5491 IS merged renders a DERIVED `[x]`, nested one indent.
+fn witness_child_derived_checked_when_merged() -> Bool {
+  string_contains(s: emit(merged: [5491]), pattern: "[x] **PR-checkbox status**")
+}
+// Discriminating: when #5491 is NOT in the merged set, the SAME child derives `[ ]` (not hand-set).
+fn witness_child_derived_unchecked_when_unmerged() -> Bool {
+  let out = emit(merged: [])
+  string_contains(s: out, pattern: "[ ] **PR-checkbox status**")
+    && !string_contains(s: out, pattern: "[x] **PR-checkbox status**")
+}
+
+test fn roadmap_emit_witnesses() -> Bool {
+  witness_heading()
+    && witness_parent_authored_box_and_link()
+    && witness_child_derived_checked_when_merged()
+    && witness_child_derived_unchecked_when_unmerged()
+}

dsl/test/claim/roadmap_model_test.dag

@@ -16,7 +16,7 @@ module test.claim.roadmap_model
 
 import ctrl.process_algebra { ProcessNodeId }
 import gunbc.roadmap_status {
-  RoadmapStatusEntry, Todo, Done, CompletesIff, HandChecked,
+  RoadmapStatusEntry, CompletesIff, HandChecked,
   DriftVerdict, Drifted, Clean, Underivable,
 }
 import gunbc.roadmap_model {
@@ -71,7 +71,7 @@ data existing_docs: List<String> = [
 fn node_with_carrier(c: PlanDocCarrier) -> RoadmapNode {
   RoadmapNode {
     node: child_node,
-    line: RoadmapStatusEntry { title: "PR→checkbox status", claimed: Todo, binding: HandChecked },
+    line: RoadmapStatusEntry { title: "PR→checkbox status", claimed_done: false, binding: HandChecked },
     carrier: c,
   }
 }
@@ -102,7 +102,7 @@ fn witness_no_carrier_clean() -> Bool {
 fn witness_node_status_drifts() -> Bool {
   let rn = RoadmapNode {
     node: child_node,
-    line: RoadmapStatusEntry { title: "stale", claimed: Todo, binding: CompletesIff { prs: [5491] } },
+    line: RoadmapStatusEntry { title: "stale", claimed_done: false, binding: CompletesIff { prs: [5491] } },
     carrier: NoCarrier,
   }
   verdict_is_drifted(v: node_status_drift(rn: rn, merged: [5491]))
@@ -111,7 +111,7 @@ fn witness_node_status_drifts() -> Bool {
 fn witness_node_handchecked_underivable() -> Bool {
   let rn = RoadmapNode {
     node: child_node,
-    line: RoadmapStatusEntry { title: "partial evidence", claimed: Todo, binding: HandChecked },
+    line: RoadmapStatusEntry { title: "partial evidence", claimed_done: false, binding: HandChecked },
     carrier: NoCarrier,
   }
   verdict_is_underivable(v: node_status_drift(rn: rn, merged: [5491]))

dsl/test/claim/roadmap_status_test.dag

@@ -20,11 +20,10 @@ module test.claim.roadmap_status
 import extdeps.github.pulls { PullRequest, PullRequestRef, Open }
 import extdeps.github.github { GitHubUser, User }
 import gunbc.roadmap_status {
-  CheckboxState, Done, Todo,
   CompletionBinding, CompletesIff, HandChecked,
   RoadmapStatusEntry,
   DriftVerdict, Drifted, Clean, Underivable,
-  pr_merged, merged_pr_numbers, derive_checkbox,
+  pr_merged, merged_pr_numbers, prs_all_merged,
   status_drift, entry_drifted,
 }
 
@@ -93,23 +92,19 @@ fn witness_merged_numbers_projection() -> Bool {
   count(nums) == 1 && (nums |> any(n => n == 5445))
 }
 
-// === Derivation: derive_checkbox ==============================================
+// === Derivation: prs_all_merged ===============================================
 
-fn checkbox_is_done(c: CheckboxState) -> Bool {
-  match c { Done => true  Todo => false }
-}
-
-// All bound PRs merged -> Done.
+// All bound PRs merged -> done.
 fn witness_all_merged_derives_done() -> Bool {
-  checkbox_is_done(c: derive_checkbox(prs: [5445], merged: [5445]))
+  prs_all_merged(prs: [5445], merged: [5445])
 }
-// A single unmerged bound PR -> Todo (not yet landed).
+// A single unmerged bound PR -> not done (not yet landed).
 fn witness_one_unmerged_derives_todo() -> Bool {
-  !checkbox_is_done(c: derive_checkbox(prs: [5445, 9999], merged: [5445]))
+  !prs_all_merged(prs: [5445, 9999], merged: [5445])
 }
-// An empty binding -> Todo (no merge evidence; fail-closed).
+// An empty binding -> not done (no merge evidence; fail-closed).
 fn witness_empty_binding_derives_todo() -> Bool {
-  !checkbox_is_done(c: derive_checkbox(prs: [], merged: [5445]))
+  !prs_all_merged(prs: [], merged: [5445])
 }
 
 // === Drift verdict: only an explicit CompletesIff binding can drift ===========
@@ -121,7 +116,7 @@ fn witness_empty_binding_derives_todo() -> Bool {
 fn witness_partial_evidence_merged_mention_stays_green() -> Bool {
   let entry = RoadmapStatusEntry {
     title: "rust-gate coverage — cites merged #5445 as partial evidence, not done",
-    claimed: Todo,
+    claimed_done: false,
     binding: HandChecked,
   }
   is_underivable(v: status_drift(entry: entry, merged: [5445]))
@@ -130,41 +125,41 @@ fn witness_partial_evidence_merged_mention_stays_green() -> Bool {
 
 // A HandChecked `[x]` is also out of the gate's reach (operator's call, no binding to check).
 fn witness_handchecked_done_underivable() -> Bool {
-  let entry = RoadmapStatusEntry { title: "audit done, no PR", claimed: Done, binding: HandChecked }
+  let entry = RoadmapStatusEntry { title: "audit done, no PR", claimed_done: true, binding: HandChecked }
   is_underivable(v: status_drift(entry: entry, merged: []))
 }
 
 // The genuine stale-checkbox: a line EXPLICITLY bound to complete iff #5445 merges, #5445 merged,
 // box still `[ ]` -> Drifted (the #5445/#5453 realization-vocab-guard case the plan cites).
 fn witness_completesiff_merged_box_todo_drifts() -> Bool {
-  let entry = RoadmapStatusEntry { title: "bound + stale", claimed: Todo, binding: completes_iff(prs: [5445]) }
+  let entry = RoadmapStatusEntry { title: "bound + stale", claimed_done: false, binding: completes_iff(prs: [5445]) }
   is_drifted(v: status_drift(entry: entry, merged: [5445])) && entry_drifted(entry: entry, merged: [5445])
 }
 // Premature `[x]`: bound to complete iff #9999 merges, #9999 unmerged -> Drifted.
 fn witness_completesiff_unmerged_box_done_drifts() -> Bool {
-  let entry = RoadmapStatusEntry { title: "bound + premature", claimed: Done, binding: completes_iff(prs: [9999]) }
+  let entry = RoadmapStatusEntry { title: "bound + premature", claimed_done: true, binding: completes_iff(prs: [9999]) }
   is_drifted(v: status_drift(entry: entry, merged: [5445]))
 }
 // Correctly-marked `[x]` on a satisfied binding -> Clean.
 fn witness_completesiff_merged_box_done_clean() -> Bool {
-  let entry = RoadmapStatusEntry { title: "bound + honest done", claimed: Done, binding: completes_iff(prs: [5445]) }
+  let entry = RoadmapStatusEntry { title: "bound + honest done", claimed_done: true, binding: completes_iff(prs: [5445]) }
   is_clean(v: status_drift(entry: entry, merged: [5445])) && !entry_drifted(entry: entry, merged: [5445])
 }
 // Correctly-marked `[ ]` on an unsatisfied binding -> Clean.
 fn witness_completesiff_unmerged_box_todo_clean() -> Bool {
-  let entry = RoadmapStatusEntry { title: "bound + honest todo", claimed: Todo, binding: completes_iff(prs: [9999]) }
+  let entry = RoadmapStatusEntry { title: "bound + honest todo", claimed_done: false, binding: completes_iff(prs: [9999]) }
   is_clean(v: status_drift(entry: entry, merged: [5445]))
 }
 // Multi-PR binding, one ref still unmerged, box `[ ]` -> Clean (not all landed).
 fn witness_completesiff_partial_multi_todo_clean() -> Bool {
-  let entry = RoadmapStatusEntry { title: "bound + multi partial", claimed: Todo, binding: completes_iff(prs: [5445, 9999]) }
+  let entry = RoadmapStatusEntry { title: "bound + multi partial", claimed_done: false, binding: completes_iff(prs: [5445, 9999]) }
   is_clean(v: status_drift(entry: entry, merged: [5445]))
 }
 
 // The host/gate edge: bound to complete iff #5445 merges; the live PR set has #5445 merged; box
 // `[ ]` -> drift.
 fn entry_against_prs_drifts() -> Bool {
-  let entry = RoadmapStatusEntry { title: "live-edge stale", claimed: Todo, binding: completes_iff(prs: [5445]) }
+  let entry = RoadmapStatusEntry { title: "live-edge stale", claimed_done: false, binding: completes_iff(prs: [5445]) }
   entry_drifted(entry: entry, merged: merged_pr_numbers(prs: [pr_5445, pr_open_9999]))
 }