Generate DESIGN.md from .dag + enforce the document's syllogism

dsl/extdeps/languages/markdown.dag

@@ -75,6 +75,7 @@ type MarkdownSpellings {
   blockquote_marker: String
   list_indent: String
   block_separator: String
+  thematic_break: String
 }
 
 data commonmark_gfm_spellings: MarkdownSpellings = {
@@ -102,6 +103,7 @@ data commonmark_gfm_spellings: MarkdownSpellings = {
   blockquote_marker: "> ",
   list_indent: "  ",
   block_separator: "\n\n",
+  thematic_break: "---",
 }
 
 fn md_link_form(text: String, url: String, sp: MarkdownSpellings) -> String {
@@ -143,7 +145,18 @@ fn md_item(marker: String, blocks: List<MarkdownBlock>, sp: MarkdownSpellings, d
       }
       { idx: 1, out: lead }
     } else {
-      { idx: acc.idx + 1, out: concat(acc.out, concat("\n", md_nested(block: b, sp: sp, depth: depth + 1))) }
+      let cont = match b {
+        UnorderedListBlock { items: _ } => concat("\n", md_nested(block: b, sp: sp, depth: depth + 1))
+        OrderedListBlock { items: _ } => concat("\n", md_nested(block: b, sp: sp, depth: depth + 1))
+        TaskListBlock { items: _ } => concat("\n", md_nested(block: b, sp: sp, depth: depth + 1))
+        HeadingBlock { level: _, inlines: _ } => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+        ParagraphBlock { inlines: _ } => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+        CodeBlock { code: _ } => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+        TableBlock { header: _, alignments: _, rows: _ } => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+        BlockquoteBlock { blocks: _ } => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+        ThematicBreak => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp)))
+      }
+      { idx: acc.idx + 1, out: concat(acc.out, cont) }
     }
   }).out
 }
@@ -268,6 +281,8 @@ fn md_block(block: MarkdownBlock, sp: MarkdownSpellings) -> String {
       md_table(header: header, alignments: alignments, rows: rows, sp: sp)
     BlockquoteBlock { blocks } =>
       md_blockquote(blocks: blocks, sp: sp)
+    ThematicBreak =>
+      sp.thematic_break
   }
 }
 

dsl/gunbc/design_argument.dag

@@ -48,3 +48,49 @@ data design_section_1_argument: Argument = Argument {
   axioms: design_axioms,
   propositions: design_section_1_propositions
 }
+
+data design_section_2_to_7_propositions: List<Proposition> = [
+
+  Proposition {
+    id: "s2.minimize-redundancy",
+    statement: "minimize redundancy is the master move for cost and complexity: redundant work loses on all three of §1's quantities at once, so a perfectly DRY process is by meaning the minimal/efficient one",
+    premises: ["s1.minimal-safe-efficient"]
+  },
+
+  Proposition {
+    id: "s3.single-authority",
+    statement: "single authority keeps §2 from being undone: minimization holds only if each fact lives in exactly one place; the recurring violation is nicknaming (a second name for one concept)",
+    premises: ["s2.minimize-redundancy"]
+  },
+
+  Proposition {
+    id: "s4.closed-grounded-substrate",
+    statement: "the closed, grounded substrate makes §2–§3 decidable: you can unify and decompose mechanically only in a closed, grounded system, and grounding is intersubjective",
+    premises: ["s2.minimize-redundancy", "s3.single-authority", "s1.grounding-intersubjective"]
+  },
+
+  Proposition {
+    id: "s5.fail-closed",
+    statement: "fail-closed is §1's safety axis: minimizing cost and complexity is worthless if a wrong thing passes silently; stronger than catching a wrong state is making it unwritable (correctness by construction, not validation)",
+    premises: ["s1.minimal-safe-efficient"]
+  },
+
+  Proposition {
+    id: "s6.how-to-work",
+    statement: "how to work given §1–§5: model by DFS-ing the concept DAG, prioritize holistically and denominate the benefit as displaced cost, and enforce by construction-first then lenses for the unstructurable residue",
+    premises: ["s2.minimize-redundancy", "s3.single-authority", "s4.closed-grounded-substrate", "s5.fail-closed"]
+  },
+
+  Proposition {
+    id: "s7.self-hosting",
+    statement: "self-hosting applies the principles to the compiler itself: it is an ordinary substrate fact written in itself, and because a wall is a row over a medium-agnostic substrate, language design opens up (compiler-fork × language → row + medium)",
+    premises: ["s4.closed-grounded-substrate", "s6.how-to-work", "s1.reduce-to-physics"]
+  }
+]
+
+data design_propositions: List<Proposition> = concat(design_section_1_propositions, design_section_2_to_7_propositions)
+
+data design_argument: Argument = Argument {
+  axioms: design_axioms,
+  propositions: design_propositions
+}

dsl/gunbc/generated_artifact.dag

@@ -5,23 +5,27 @@ import gunbc.ci_yaml_emit { expected_ci_yml }
 import gunbc.ci_yaml_validate { ci_yml_parses }
 import gunbc.gitignore_emit { expected_gitignore, path_is_ignored }
 import gunbc.roadmap_authority { expected_roadmap_md }
+import gunbc.design_document { expected_design_md }
 
 type GeneratedArtifact
   = CiYamlArtifact
   | GitignoreArtifact
   | RoadmapArtifact
+  | DesignArtifact
 
 data generated_artifact_registry: List<GeneratedArtifact> = [
   CiYamlArtifact,
   GitignoreArtifact,
-  RoadmapArtifact
+  RoadmapArtifact,
+  DesignArtifact
 ]
 
 fn artifact_path(a: GeneratedArtifact) -> String {
   match a {
     CiYamlArtifact => ".github/workflows/ci.yml"
     GitignoreArtifact => ".gitignore"
     RoadmapArtifact => "ROADMAP.md"
+    DesignArtifact => "DESIGN.md"
   }
 }
 
@@ -30,6 +34,7 @@ fn artifact_generate(a: GeneratedArtifact) -> String {
     CiYamlArtifact => expected_ci_yml()
     GitignoreArtifact => expected_gitignore()
     RoadmapArtifact => expected_roadmap_md()
+    DesignArtifact => expected_design_md()
   }
 }
 
@@ -53,6 +58,7 @@ fn artifact_eq(a: GeneratedArtifact, b: GeneratedArtifact) -> Bool {
     CiYamlArtifact => match b { CiYamlArtifact => true  _ => false }
     GitignoreArtifact => match b { GitignoreArtifact => true  _ => false }
     RoadmapArtifact => match b { RoadmapArtifact => true  _ => false }
+    DesignArtifact => match b { DesignArtifact => true  _ => false }
   }
 }
 

dsl/std/markdown.dag

@@ -51,6 +51,7 @@ type MarkdownBlock
       rows: List<MarkdownTableRow>,
     }
   | BlockquoteBlock { blocks: List<MarkdownBlock> }
+  | ThematicBreak
 
 type MarkdownDocument { blocks: List<MarkdownBlock> }
 
@@ -156,6 +157,7 @@ fn find_first_rejected_url_in_block(block: MarkdownBlock) -> RejectedUrlScheme?
       }
     BlockquoteBlock { blocks } =>
       find_first_rejected_url_in_blocks(blocks: blocks)
+    ThematicBreak => Absent
   }
 }
 
@@ -332,6 +334,12 @@ fn markdown_block_to_fragment(block: MarkdownBlock) -> Fragment {
         attributes: [],
         children: markdown_blocks_to_fragments(blocks: blocks),
       }
+    ThematicBreak =>
+      Element {
+        tag: "hr",
+        attributes: [],
+        children: [],
+      }
   }
 }
 

dsl/test/claim/design_argument_witness_test.dag

@@ -1,6 +1,6 @@
 module test.claim.design_argument_witness
 
-import gunbc.design_argument { design_section_1_argument, design_axioms }
+import gunbc.design_argument { design_section_1_argument, design_argument, design_axioms }
 import std.syllogism {
   Axiom, NonLogicalAxiom, Proposition, Argument,
   argument_has_no_orphan, argument_is_acyclic,
@@ -15,6 +15,22 @@ test fn design_s1_argument_is_non_vacuous() -> Bool {
   argument_is_non_vacuous(design_section_1_argument)
 }
 
+test fn design_full_argument_form_is_valid() -> Bool {
+  argument_form_is_valid(design_argument)
+}
+
+test fn design_full_argument_has_no_orphan() -> Bool {
+  argument_has_no_orphan(design_argument)
+}
+
+test fn design_full_argument_is_acyclic() -> Bool {
+  argument_is_acyclic(design_argument)
+}
+
+test fn design_full_argument_axiom_set_is_closed() -> Bool {
+  argument_axiom_set_is_closed(design_argument)
+}
+
 fn orphaned_variant() -> Argument {
   Argument {
     axioms: design_axioms,

dsl/test/claim/generated_artifact_drift_test.dag

@@ -2,7 +2,7 @@
 module test.claim.generated_artifact_drift
 
 import gunbc.generated_artifact {
-  GeneratedArtifact, CiYamlArtifact, GitignoreArtifact, RoadmapArtifact,
+  GeneratedArtifact, CiYamlArtifact, GitignoreArtifact, RoadmapArtifact, DesignArtifact,
   generated_artifact_registry,
   committed_generated_artifacts, artifact_path, artifact_generate, artifact_extra_valid,
   artifact_is_committed, registry_contains
@@ -26,9 +26,11 @@ fn witness_all_known_committed() -> Bool {
   artifact_is_committed(a: CiYamlArtifact)
     && artifact_is_committed(a: GitignoreArtifact)
     && artifact_is_committed(a: RoadmapArtifact)
+    && artifact_is_committed(a: DesignArtifact)
     && !path_is_ignored(path: ".github/workflows/ci.yml")
     && !path_is_ignored(path: ".gitignore")
     && !path_is_ignored(path: "ROADMAP.md")
+    && !path_is_ignored(path: "DESIGN.md")
 }
 
 fn witness_ignored_paths_excluded() -> Bool {
@@ -39,18 +41,21 @@ fn witness_ignored_paths_excluded() -> Bool {
 }
 
 fn witness_registry_complete() -> Bool {
-  count(generated_artifact_registry) == 3
+  count(generated_artifact_registry) == 4
     && registry_contains(a: CiYamlArtifact)
     && registry_contains(a: GitignoreArtifact)
     && registry_contains(a: RoadmapArtifact)
+    && registry_contains(a: DesignArtifact)
     && artifact_is_committed(a: CiYamlArtifact)
     && artifact_is_committed(a: GitignoreArtifact)
     && artifact_is_committed(a: RoadmapArtifact)
+    && artifact_is_committed(a: DesignArtifact)
 }
 
 fn witness_extra_validation_wired() -> Bool {
   artifact_extra_valid(a: GitignoreArtifact)
     && artifact_extra_valid(a: RoadmapArtifact)
+    && artifact_extra_valid(a: DesignArtifact)
     && artifact_extra_valid(a: CiYamlArtifact)
 }