ROADMAP slice-2 step-3a: whole-document projection + pure golden witness

dsl/gunbc/roadmap_document.dag

@@ -0,0 +1,59 @@
+// gunbc/roadmap_document.dag — the WHOLE-document roadmap authority + projection (slice-2 step-3).
+//
+// SCAFFOLD (DESIGN §7 / plan §6 step 2-3): widens the per-section projection (`roadmap_emit`) to the
+// whole ROADMAP — `project_roadmap_to_markdown(authority) -> MarkdownDocument`, the markdown analogue of
+// ci.yml's `project_workflow_to_yaml(ci_workflow)`. The authored `data` authority is the inversion: the
+// `.dag` is the single source, ROADMAP.md is its emitted projection (the structure gate, step-3b, then
+// byte-compares them — the `ci_yaml_gate` shape).
+// dissolution-trigger: authored-now is the INTERMEDIATE (mirrors ci.yml's authored `data ci_workflow`);
+//   the TERMINAL is bridging the structure from `ctrl.process_algebra.ProcessGraph` once v2 self-host
+//   gives in-substrate graph traversal (it is STAGED today, no traversal fns), at which point the
+//   authored `data roadmap_authority` dissolves into a walk over the work graph.
+//
+// O3 DFS (why RoadmapSection is MINTED, not derived from top-level nodes): a ROADMAP `##` section is a
+// SEPARATE presentation axis, not a single work-node + flat subtree — it carries authored intro prose,
+// a plan-doc pointer, and MULTIPLE sub-grouped checkbox lists (`**Audits (done):**`,
+// `**In-scope this window:**`). Its WORK content is the existing `RoadmapNode`/`RoadmapEdge` graph; the
+// section adds the editorial grouping a work-node does not carry. So RoadmapSection earns its keep as
+// the grouping axis — net concepts grow by ONE genuinely-distinct concept, not a re-invention (§2).
+
+module gunbc.roadmap_document
+
+import std.markdown { MarkdownDocument, MarkdownBlock }
+import gunbc.roadmap_model { RoadmapNode, RoadmapEdge }
+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.
+type RoadmapSection {
+  title: String
+  nodes: List<RoadmapNode>
+  edges: List<RoadmapEdge>
+}
+
+// The whole ROADMAP as authority. `preamble` is the document-level authored frame above the first
+// section (the title/intro blocks) — so RoadmapDocument earns its keep over a bare `List<RoadmapSection>`
+// (§2: a 1-field wrapper would not). DISTINCT from `std.markdown.MarkdownDocument`: this is the
+// AUTHORITY (work structure), that is the MEDIUM (rendered blocks) — authority vs medium stays split (§3).
+type RoadmapDocument {
+  preamble: List<MarkdownBlock>
+  sections: List<RoadmapSection>
+}
+
+// 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
+}
+
+// THE whole-document projection (the ci.yml `project_workflow_to_yaml` analogue, markdown medium):
+// preamble blocks, then each section's blocks in order. A pure fold over the authored authority — the
+// checkbox boxes are rendered from each line's binding against `merged` (derived for CompletesIff,
+// authored for HandChecked), exactly as the per-section projection does.
+fn project_roadmap_to_markdown(doc: RoadmapDocument, merged: List<Int>) -> MarkdownDocument {
+  MarkdownDocument {
+    blocks: fold(doc.sections, init: doc.preamble, f: fn(acc, s) {
+      concat(acc, section_blocks(s: s, merged: merged))
+    })
+  }
+}

dsl/test/claim/roadmap_document_test.dag

@@ -0,0 +1,141 @@
+// dsl/test/claim/roadmap_document_test.dag — §5 pure-projection proof for gunbc.roadmap_document.
+//
+// The PURE half of step-3 (O4): proves BY EXECUTION that project_roadmap_to_markdown over a synthetic
+// whole-document authority serializes to the right ROADMAP bytes — preamble first, then each section's
+// H2 + task list in order, with CompletesIff boxes DERIVED from the merged set and HandChecked boxes
+// AUTHORED. Discriminating: flip the merged set and the derived box flips; the effectful drift gate
+// (read the real ROADMAP.md, byte-compare) is the SEPARATE RoadmapGate variant (step-3b), since
+// Filesystem.Read is a host effect and cannot live in a pure witness.
+
+module test.claim.roadmap_document
+
+import extdeps.languages.markdown { serialize_markdown_source }
+import gunbc.roadmap_document { RoadmapDocument, RoadmapSection, project_roadmap_to_markdown }
+import gunbc.roadmap_model { RoadmapNode, RoadmapEdge, PlanDocCarrier, NoCarrier, PlanDoc }
+import gunbc.roadmap_status { RoadmapStatusEntry, CompletesIff, HandChecked }
+import std.markdown { MarkdownBlock, HeadingBlock, ParagraphBlock, TextInline, H1 }
+import ctrl.process_algebra { ProcessNodeId }
+
+data audit_id: ProcessNodeId = "fail-closed-audit"
+data status_id: ProcessNodeId = "pr-checkbox-status"
+data child_id: ProcessNodeId = "host-fed-status-bridge"
+
+// HandChecked line — authored box (no PR derivation).
+fn audit_node() -> RoadmapNode {
+  RoadmapNode {
+    node: audit_id,
+    line: RoadmapStatusEntry { title: "fail-open audit", claimed_done: true, binding: HandChecked },
+    carrier: PlanDoc { path: "docs/plans/fail-closed-lockdown.md" },
+  }
+}
+// CompletesIff line — box DERIVED from the merged set.
+fn status_node() -> RoadmapNode {
+  RoadmapNode {
+    node: status_id,
+    line: RoadmapStatusEntry { title: "PR-checkbox status", claimed_done: false, binding: CompletesIff { prs: [5491] } },
+    carrier: NoCarrier,
+  }
+}
+fn child_node() -> RoadmapNode {
+  RoadmapNode {
+    node: child_id,
+    line: RoadmapStatusEntry { title: "host-fed status bridge", claimed_done: false, binding: HandChecked },
+    carrier: NoCarrier,
+  }
+}
+
+fn lockdown_section() -> RoadmapSection {
+  RoadmapSection { title: "0. Fail-closed lock-down", nodes: [audit_node()], edges: [] }
+}
+fn expansion_section() -> RoadmapSection {
+  RoadmapSection {
+    title: "6. Expansion",
+    nodes: [status_node(), child_node()],
+    edges: [RoadmapEdge { child: child_id, parent: status_id }],
+  }
+}
+
+fn preamble() -> List<MarkdownBlock> {
+  [
+    HeadingBlock { level: H1, inlines: [TextInline { text: "ROADMAP" }] },
+    ParagraphBlock { inlines: [TextInline { text: "Generated from .dag authority — do not hand-edit." }] },
+  ]
+}
+
+fn authority() -> RoadmapDocument {
+  RoadmapDocument { preamble: preamble(), sections: [lockdown_section(), expansion_section()] }
+}
+
+fn emit(merged: List<Int>) -> String {
+  serialize_markdown_source(doc: project_roadmap_to_markdown(doc: authority(), merged: merged))
+}
+
+// The preamble renders first.
+fn witness_preamble_first() -> Bool {
+  let out = emit(merged: [5491])
+  string_contains(s: out, pattern: "# ROADMAP")
+    && string_contains(s: out, pattern: "Generated from .dag authority")
+}
+// Both section H2 headings render, in order.
+fn witness_both_sections() -> Bool {
+  let out = emit(merged: [5491])
+  string_contains(s: out, pattern: "## 0. Fail-closed lock-down")
+    && string_contains(s: out, pattern: "## 6. Expansion")
+}
+// HandChecked authored box + its plan-doc link.
+fn witness_authored_box_and_link() -> Bool {
+  let out = emit(merged: [5491])
+  string_contains(s: out, pattern: "[x] **fail-open audit**")
+    && string_contains(s: out, pattern: "[plan](docs/plans/fail-closed-lockdown.md)")
+}
+// CompletesIff child-bearing node: #5491 merged -> derived [x], nesting its child one indent.
+fn witness_derived_checked_when_merged() -> Bool {
+  string_contains(s: emit(merged: [5491]), pattern: "[x] **PR-checkbox status**")
+}
+// Discriminating: #5491 NOT merged -> SAME line derives [ ] (not authored — claimed_done is false too,
+// but the point is it's DERIVED: a HandChecked false would also be [ ], so pair with the merged case).
+fn witness_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**")
+}
+
+// The literal expected ROADMAP source for the synthetic authority with #5491 merged (independent
+// re-derivation, not via the fold) — the ci.yml `expected_ci_yml` shape over the markdown medium.
+fn expected_roadmap() -> String {
+  join([
+    "# ROADMAP\n",
+    "\n",
+    "Generated from .dag authority — do not hand-edit.\n",
+    "\n",
+    "## 0. Fail-closed lock-down\n",
+    "\n",
+    "- [x] **fail-open audit** [plan](docs/plans/fail-closed-lockdown.md)\n",
+    "\n",
+    "## 6. Expansion\n",
+    "\n",
+    "- [x] **PR-checkbox status**\n",
+    "  - [ ] **host-fed status bridge**\n"
+  ], "")
+}
+
+// Byte-exact: the whole-document projection serializes to the literal expected ROADMAP source.
+fn witness_exact_bytes() -> Bool {
+  emit(merged: [5491]) == expected_roadmap()
+}
+// Drift receipt: the CompletesIff box is genuinely a function of the merged set, not baked into the
+// golden — the clean set MUST match the golden, a perturbed set MUST diverge (so the gate has teeth).
+fn witness_drift_receipt() -> Bool {
+  emit(merged: [5491]) == expected_roadmap()
+    && !(emit(merged: []) == expected_roadmap())
+}
+
+test fn roadmap_document_witnesses() -> Bool {
+  witness_preamble_first()
+    && witness_both_sections()
+    && witness_authored_box_and_link()
+    && witness_derived_checked_when_merged()
+    && witness_derived_unchecked_when_unmerged()
+    && witness_exact_bytes()
+    && witness_drift_receipt()
+}