diff --git a/dsl/gunbc/roadmap_emit.dag b/dsl/gunbc/roadmap_emit.dag new file mode 100644 index 00000000000..45c0abd5050 --- /dev/null +++ b/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) -> Bool { + entry_is_done(entry: rn.line, merged: merged) +} + +// === Inline content — bold title + optional plan-doc link ==================== + +fn carrier_inlines(carrier: PlanDocCarrier) -> List { + match carrier { + NoCarrier => [] + PlanDoc { path } => [ + TextInline { text: " " }, + LinkInline { inlines: [TextInline { text: "plan" }], url: path }, + ] + } +} + +fn node_inlines(rn: RoadmapNode) -> List { + 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, edges: List, parent: ProcessNodeId) -> List { + 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) -> 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, edges: List, merged: List, 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, edges: List, merged: List) -> 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())) }, + ] + } +} diff --git a/dsl/gunbc/roadmap_status.dag b/dsl/gunbc/roadmap_status.dag index 0f00a7962b3..13a3f1678de 100644 --- a/dsl/gunbc/roadmap_status.dag +++ b/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) -> List { 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, merged: List) -> 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, merged: List) -> 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) -> 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) -> 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 diff --git a/dsl/test/claim/roadmap_emit_test.dag b/dsl/test/claim/roadmap_emit_test.dag new file mode 100644 index 00000000000..84218668f0d --- /dev/null +++ b/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 { [parent_node(), child_node()] } +fn edges() -> List { [RoadmapEdge { child: child_id, parent: parent_id }] } + +fn emit(merged: List) -> 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() +} diff --git a/dsl/test/claim/roadmap_model_test.dag b/dsl/test/claim/roadmap_model_test.dag index 963188dfbea..457b4dfa5d0 100644 --- a/dsl/test/claim/roadmap_model_test.dag +++ b/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 = [ 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])) diff --git a/dsl/test/claim/roadmap_status_test.dag b/dsl/test/claim/roadmap_status_test.dag index eb1f2d0fe3e..4d7823072f9 100644 --- a/dsl/test/claim/roadmap_status_test.dag +++ b/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])) }