From e642d877bfad66fc0d1e1beb73a0deb38eb5ebc0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 01:41:33 +0000 Subject: [PATCH 01/10] WIP: get design docs into .dag --- dsl/std/markdown.dag | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dsl/std/markdown.dag b/dsl/std/markdown.dag index 9f48edf8980..3c75f3e3c21 100644 --- a/dsl/std/markdown.dag +++ b/dsl/std/markdown.dag @@ -51,6 +51,7 @@ type MarkdownBlock rows: List, } | BlockquoteBlock { blocks: List } + | ThematicBreak type MarkdownDocument { blocks: List } @@ -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 } } From 7e63efbc8ed73bf15a279d35e0aa15ac5d3fb647 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 01:54:03 +0000 Subject: [PATCH 02/10] WIP: get design docs into .dag --- dsl/extdeps/languages/markdown.dag | 4 ++++ dsl/std/markdown.dag | 6 ++++++ 2 files changed, 10 insertions(+) diff --git a/dsl/extdeps/languages/markdown.dag b/dsl/extdeps/languages/markdown.dag index 9e0dcb2d4eb..52412194026 100644 --- a/dsl/extdeps/languages/markdown.dag +++ b/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 { @@ -268,6 +270,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 } } diff --git a/dsl/std/markdown.dag b/dsl/std/markdown.dag index 3c75f3e3c21..137763f90e7 100644 --- a/dsl/std/markdown.dag +++ b/dsl/std/markdown.dag @@ -334,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: [], + } } } From 562666a28307699ce82e9d6bd19f021627623042 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:05:30 +0000 Subject: [PATCH 03/10] WIP: get design docs into .dag --- dsl/gunbc/design_argument.dag | 61 +++++ dsl/gunbc/design_document.dag | 214 ++++++++++++++++++ dsl/gunbc/generated_artifact.dag | 8 +- .../claim/design_argument_witness_test.dag | 21 +- .../claim/generated_artifact_drift_test.dag | 9 +- 5 files changed, 309 insertions(+), 4 deletions(-) create mode 100644 dsl/gunbc/design_document.dag diff --git a/dsl/gunbc/design_argument.dag b/dsl/gunbc/design_argument.dag index 792fb53f5d9..eac87064eaa 100644 --- a/dsl/gunbc/design_argument.dag +++ b/dsl/gunbc/design_argument.dag @@ -48,3 +48,64 @@ data design_section_1_argument: Argument = Argument { axioms: design_axioms, propositions: design_section_1_propositions } + +// §2–§7: one headline proposition per section, each premised on the sections it is a consequence of. +// This is the document's serial spine (DESIGN preamble: "each later section is a consequence of the ones +// before it (or an independent peer)") made a checked consequence-chain — no orphan, no cycle, every claim +// reachable from A1–A3 via §1. The full prose of each section lives in gunbc.design_document; binding the +// two (render each section FROM its proposition) is the dissolution trigger below. +data design_section_2_to_7_propositions: List = [ + + 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 = + concat(design_section_1_propositions, design_section_2_to_7_propositions) + +// The whole-document argument: A1–A3 + every section's headline claim. The syllogism lens +// (std.syllogism.argument_form_is_valid) checks it is non-vacuous, orphan-free, acyclic, and +// axiom-set-closed — the §1 open-thread "every claim a consequence-chain back to an axiom" turned on +// this document itself (DESIGN §7 recursion). +// +// DISSOLUTION TRIGGER: today the section prose (gunbc.design_document) and these propositions are two +// views of the same claims at different granularity — the proposition is the headline, the document is the +// exposition. Collapse to one authority once design_document renders each section's lead FROM its +// proposition (the document model carrying rich-block claim content), so the headline is single-authored. +data design_argument: Argument = Argument { + axioms: design_axioms, + propositions: design_propositions +} diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag new file mode 100644 index 00000000000..c12ad072da0 --- /dev/null +++ b/dsl/gunbc/design_document.dag @@ -0,0 +1,214 @@ +// gunbc.design_document — DESIGN.md as a .dag projection (DESIGN §7: this document is the first target of +// the recursion — an ordinary substrate fact, generated from its model, drift-gated like ROADMAP.md). +// +// The PROSE is modeled as typed markdown blocks (heading / paragraph / bullet list / thematic break); a +// paragraph carries the raw markdown source as one TextInline (the serializer passes `**bold**`/`code` +// through verbatim — same convention as gunbc.roadmap_authority), unwrapped to a single line. The doc's +// LOGICAL spine (axioms A1–A3 + the §1–§7 consequence-chain) is modeled separately and checked by the +// syllogism lens in gunbc.design_argument; binding the two — render each claim FROM its proposition — is +// the named dissolution trigger (see design_argument.dag). +// +// expected_design_md() is the single generator; gunbc.generated_artifact registers DESIGN.md against it +// and tools.generated_artifact_gate drift-gates it. Do not hand-edit DESIGN.md — regenerate via main_wet. + +module gunbc.design_document + +import std.markdown { + MarkdownDocument, MarkdownBlock, MarkdownListItem, + HeadingBlock, ParagraphBlock, UnorderedListBlock, ThematicBreak, + TextInline, H1, H2, +} +import extdeps.languages.markdown { serialize_markdown_source } + +// ── authoring helpers ────────────────────────────────────────────────────────────────────────────── +// A paragraph / heading carries the exact markdown source line (inline formatting survives as literal +// text through the serializer). Wrapped source lines are joined into one line per block. + +fn h1(text: String) -> MarkdownBlock { HeadingBlock { level: H1, inlines: [TextInline { text: text }] } } +fn h2(text: String) -> MarkdownBlock { HeadingBlock { level: H2, inlines: [TextInline { text: text }] } } +fn p(text: String) -> MarkdownBlock { ParagraphBlock { inlines: [TextInline { text: text }] } } +fn rule() -> MarkdownBlock { ThematicBreak } + +// a bullet item that is a single paragraph +fn li(text: String) -> MarkdownListItem { MarkdownListItem { blocks: [p(text: text)] } } +// a bullet item carrying arbitrary blocks (lead paragraph + nested list + …) +fn li_blocks(blocks: List) -> MarkdownListItem { MarkdownListItem { blocks: blocks } } +fn ul(items: List) -> MarkdownBlock { UnorderedListBlock { items: items } } + +// ── preamble ───────────────────────────────────────────────────────────────────────────────────── +fn preamble_blocks() -> List { + [ + h1(text: "gunbc — Design"), + p(text: "`README.md` and `CLAUDE.md` symlink here — this is the single source of truth. (v1 ships the `gunbc` CLI and is v2's seed · v3 was removed, migrated into v1 · v2 is active.)"), + p(text: "This document is reasoned **serially**: §1 fixes the axioms, and each later section is a consequence of the ones before it (or an independent peer) — never a restatement of it. The principles below apply recursively, including to this document. It is a living draft rebuilt from first principles (the prior ~30k-line doc corpus was bankrupted 2026-06-16; it remains in git history). Examples are verified against the live tree or a git-history receipt; open threads are collected at the end."), + rule(), + ] +} + +// ── §1 — The objective (the axioms) ──────────────────────────────────────────────────────────────── +fn section_1_blocks() -> List { + [ + h2(text: "1. The objective (the axioms)"), + p(text: "The assumptions everything else rests on. Three **axioms** — assumed, not derived:"), + ul(items: [ + li(text: "**A1 — there is a goal.** To *solve a problem* presupposes an agent with a goal to satisfy; with no goal there is nothing to optimize."), + li(text: "**A2 — time is the value.** Every agent intrinsically values time — it is finite and is the substance of acting at all: **time is life**. It is the one value we may assume is *shared*."), + li(text: "**A3 — agreement is temporal.** Intersubjective agreement — two parties holding the same fact — is possible only *across* time, and only on what stays stable under it."), + ]), + p(text: "Three things follow, in order:"), + ul(items: [ + li_blocks(blocks: [ + p(text: "**From A1 and A2 — the solution is minimal, safe, efficient.** A solution is good exactly insofar as it spends less of the only thing valued, time; and time is spent three ways:"), + ul(items: [ + li(text: "**cost** — time to run (cheap to run and to feed);"), + li(text: "**safety** — time to recover from a silent wrong answer, paid later at interest (harm reduction);"), + li(text: "**complexity** — time to change (it stays cheap to maintain)."), + ]), + p(text: "So the three are not preferences layered on — they are A2 applied to A1, and the project optimizes them jointly."), + ]), + li(text: "**From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy."), + li(text: "**At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the universal frameworks and real upstream rather than re-coining them — a nickname is convention standing where physics was available."), + ]), + ] +} + +// ── §2 — Minimize redundancy ─────────────────────────────────────────────────────────────────────── +fn section_2_blocks() -> List { + [ + h2(text: "2. Minimize redundancy (the master move for cost and complexity)"), + p(text: "Redundant work — **duplicated, unnecessary, or irrelevant** — loses on all three of §1's quantities at once: it costs more to run, it widens the surface where harm hides, and it adds complexity to maintain. So a perfectly DRY process is, *by the meaning of redundant*, the minimal/efficient one; minimizing redundancy is therefore the master move for §1's cost and complexity axes (the safety axis is §5). Through §1's time lens this is *why* DRY matters at all: redundant work **defers** cost into the future — it shoves a problem onto a later fixer, or builds a process destined to be thrown out — so DRY is the refusal to spend someone's future time to buy the author's present convenience; it values time **holistically**, across every party and all of it, not just the here-and-now. Redundancy is removed along exactly two directions — not separate \"DRY rules,\" but one move seen two ways:"), + ul(items: [ + li_blocks(blocks: [ + p(text: "**Horizontal — one concept, every scale and breadth.** Model a concept once; derive every use (model-local / derive-global). At the right layer there is nothing fundamentally different between scales, so the *same* concept spans nanosecond memoization and broad infra deployment — the Realization pattern (content-addressed pure-spec → host-effect; one kernel, N handlers)."), + ul(items: [ + li(text: "*e.g.* `dsl/std/integer.dag`: `Int8`…`UInt128` are 10 `Compose>` rows, one axis not 10 types. Realization spans resolve-cost (ns) → sccache → §10 OS provisioning on one content-hash. Cost of *not* doing it: eleven hand-rolled v1 `HashMap` caches, and v2 still recurs (`ParseTable`)."), + ]), + ]), + li_blocks(blocks: [ + p(text: "**Deep — every concept decomposed to grounded atoms.** Nothing is opaque that isn't *genuinely* atomic. The move is `decompress → map → reduce`: reveal the structure the source names, **map** each part onto the concept that already exists (DFS the concept DAG first), **reduce** duplicates. A `String` leaf hiding named parts is anemic modeling."), + ul(items: [ + li(text: "*e.g.* `\"LGA4926\"` → `CpuSocket { package: LandGridArray, contact_count: 4926 }` (the number is a grounded `Int`) and `\"HMA82GR7AFR4N-VK\"` → `DramModuleCatalogRow { chip_width: bit_width(4), rank_count: 1, buffering: Registered }` (the numeric organization axes decoded from the part number ground into existing magnitudes — `chip_width` reuses `BitWidth`, `rank_count` is a cardinal `Int` — not a fresh enum re-inventing bit-width; the categorical axis stays a closed enum); `Cost = Time|Space|Energy` → a record (every cost has all three); still-anemic today: `product.compute_fabric`'s `StorageDevice` has no PCIe-gen/lane-count axis (storage's rank/width). (`GpuFacts.vendor`, once a bare `NonEmptyStr` where `CpuVendor` was a closed enum, is now grounded on the single `Vendor` authority — see §3.)"), + ]), + ]), + ]), + p(text: "The test that an edit actually *reduced* redundancy rather than moving it: **net concepts must not grow by re-invention.** Decomposing a leaf by minting a fresh authority for a concept that already exists is a failed decomposition."), + ] +} + +// ── §3 — Single authority ────────────────────────────────────────────────────────────────────────── +fn section_3_blocks() -> List { + [ + h2(text: "3. Single authority (what keeps §2 from being undone)"), + p(text: "Minimization holds only if each fact lives in exactly one place. The recurring violation is **nicknaming — a second name for one concept** — which duplicates work at the meaning layer and, since we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks (classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep its real names, declare its version, model what the API actually returns), rather than re-coining them. Corollaries: the layer DAG is strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the rename test). A direct consequence for `extdeps/` service operations, three separable facts that must not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract (inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** (which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, `--all-targets`); the tell that (b) has fused is the same operation forked once per transport (GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact rows; corpus RED witnesses execute against live `dsl/extdeps/**` via `filesystem_read` (dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* interface↔realization seam, not only service ops: the cited data behind an agnostic std surface de-fuses exactly as a transport does, and its directional reading is the same — the *dispatch* that selects a realization is itself realization, so it sits peripheral (`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that *matched* over its realizations would have to name them, inverting the import arrow above). What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the `Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion."), + ul(items: [ + li(text: "*e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one \"vendor\" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor` is the §2-horizontal \"one concept, every breadth\"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/{cpu,memory}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` (\"projection only\"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/{ubuntu,windows,macos,os}.dag` (\"dispatch lives in extdeps/, not std/\", promoted from that hub header)."), + ]), + ] +} + +// ── §4 — The closed, grounded substrate ────────────────────────────────────────────────────────────── +fn section_4_blocks() -> List { + [ + h2(text: "4. The closed, grounded substrate (what makes §2–§3 decidable)"), + p(text: "You can unify and decompose *mechanically* only in a closed, grounded system — so the substrate is built for it. A program is a dependency graph over two primitives (`Node` + `Edge`) and a closed vocabulary (6 connectives + 5 behaviors); surface syntax is sugar that adds no power. Execution is **bounded and forward** (cyclic relations via acyclic encodings, never cyclic values; recursion is sugar over `Loop`), so decidability and termination *fall out* rather than being separately proved. **Grounding is intersubjective** — point at a shared framework, not an internal taxonomy — and in a closed system **a heuristic is never necessary**: the richer source always exists or can be written. This is *why* the structure is acyclic — a DAG in the substrate, serial reasoning in this document (recursively, per the preamble): intersubjective agreement holds only **across time** (§1), which demands claims that stay stable under it, so each is written syllogistically — a consequence-chain you can re-interrogate and that never wavers (algebra), never a cycle that could quietly redefine itself."), + p(text: "Because the substrate is closed and grounded, the wins of §2 fall out for free: operations come from *inhabitance* (no per-type ops); and emission, ingestion, and coercion are **one** total decision procedure run in different directions (the epistemic chain *is* the emission algorithm — N models, not N×M adapters; every refusal a located, typed mismatch)."), + ul(items: [ + li(text: "*e.g.* `dsl/std/algebra.dag` derives `Int.add` from `Int` inhabiting a ring (ops aren't listed per type); idempotency dissolved from an `idempotent: Bool` flag into the `EffectShape` variant; termination is *checked, not discovered* — `DescentEvidence = Strict | NonIncreasing | DescentUnknown` inhabits a `BoundedLattice` with bottom = fail-closed."), + li(text: "*e.g.* **one grammar, read in both directions** (§2 horizontal, not an adapter pair): ingest selects a production *forward* to fold surface syntax into a core `Node`; emit (`serialize_target ∘ translate`) selects from the *same* `target_model_edge_translation_rules` rows *backward* — the structural inverse, not a second emitter — so a new target language is rows authored in `extdeps/languages/`, never an edit to the fold (N rows, not N×M parser/emitter pairs). Coercion is that same move turned sideways: whether one model inhabits another is a homomorphism check (`coercion_fold` via `find_witness`), the same epistemic chain the emitter walks. One procedure asked in three directions, not three procedures."), + ]), + ] +} + +// ── §5 — Fail-closed ───────────────────────────────────────────────────────────────────────────────── +fn section_5_blocks() -> List { + [ + h2(text: "5. Fail-closed (§1's safety axis — harm reduction)"), + p(text: "Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded \"forever\" ≠ an \"unknown\" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches \"never\"). The word **\"never\" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — \"done\" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.)"), + ul(items: [ + li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 { x + y }`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types."), + ]), + ] +} + +// ── §6 — How to work ───────────────────────────────────────────────────────────────────────────────── +fn section_6_blocks() -> List { + [ + h2(text: "6. How to work (given §1–§5 — these coexist)"), + ul(items: [ + li(text: "**Model:** DFS the concept DAG before inventing vocabulary; fact-bundle modeling (invent or reuse on proven coincidence, never bare-alias); a finished stage is one fold (any non-fold residue is either a named irreducible kernel or un-migrated modeling — there is no third); model just-in-time and let the mark on the carrier be the authority (no parallel-ledger docs); every scaffold lands with a named dissolution trigger."), + li(text: "**Prioritize holistically, not by the bottleneck:** balance the quantitative and the qualitative — don't anchor on one KPI (you'll hit it at a cost) or on pure taste. Map the cause→effect across sections; a 5ms step doesn't get a pass for not being the 80s one (it might be a 5ns step). Root-cause to the language layer and fix related systems *together* — a local subsystem patch is the forked-logic trap. **Denominate the benefit:** the deliverable is a *displaced cost* (§1's time — a pain someone pays to remove); the lens/substrate is the *mechanism* (the moat), not the product. A lens — or any construction wall — is on-dial exactly insofar as it is the cheapest path to such a pain. Priced in elegance instead, the work is self-referential and unbounded (the purity trap — the economic twin of \"never\" in §5; an extensible substrate's infinite improvability dissolving its own bound)."), + li(text: "**Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie, so an **executable** hygiene check must keep every lens either wired (a discovered fail-closed witness) or deleted — that backstop runs over the corpus and is *not* superseded by the authoring-time construction-justification judgment, which layers on top of it."), + li(text: "*e.g.* one catamorphism `fold_node` is reused by all 7 v2 stages; #4699 dissolved `06_translate` 4,912→3,973 lines (`_go` accumulators 35→0); a 6-line `merge_envs` root fix cut reconcile from 81% of the pipeline to 6% (~2× self-compile) — the symptom recurs wherever the root is unfixed (v2 still hand-rolls `ParseTable` because the Realization carrier is staged, not inhabited)."), + ]), + ] +} + +// ── §7 — Self-hosting ──────────────────────────────────────────────────────────────────────────────── +fn section_7_blocks() -> List { + [ + h2(text: "7. Self-hosting (the principles applied to the compiler itself)"), + p(text: "The compiler is a pure transform and an ordinary substrate fact, analyzable by its own lenses. It is written in itself, self-emits to a bit-identical fixed point (the `.dag` graph is the truth; Rust is one realization, a seed that shrinks to zero), and its tests are data. Its ontology dissolves into `std/` — no dual representation at the compiler/user boundary. This is the recursion: every principle above governs the system that implements them, and this document."), + p(text: "The recursion's payoff is that **language design itself opens up.** It is normally locked — not by lack of will but by cost: a new check means owning a *compiler fork*, and a new language means an *adoption* problem. Both are dissolved here at once: a wall is a **row** (§2, no fork), and because the substrate is medium-agnostic — one grammar read in both directions over many media (§4) — that row applies *on top of an existing language* (no adoption). So language design collapses (compiler-fork × language) → (row + medium): a domain's bug-class can be made extinct in Rust or TypeScript without forking their compilers. It is sound exactly where ingest is `Lossless` and **fail-closed** where it is not (the `DecodeFidelity` boundary, §4) — \"any language, with a typed honesty boundary about where the wall holds,\" not a vibe. This is §1's *reduce convention to necessity* at the meta-level, and the place the purity trap bites hardest: bounded by §5 (\"never\" = decidability) and §6 (priced in displaced cost, not elegance)."), + rule(), + ] +} + +// ── Recurring failure modes ────────────────────────────────────────────────────────────────────────── +fn failure_modes_blocks() -> List { + [ + h2(text: "Recurring failure modes (instances of §3–§5, kept for pattern-matching)"), + p(text: "hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks."), + ] +} + +// ── Open threads ───────────────────────────────────────────────────────────────────────────────────── +fn open_threads_blocks() -> List { + [ + h2(text: "Open threads"), + ul(items: [ + li(text: "model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project)"), + li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), + li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), + li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), + ]), + ] +} + +// ── Building & checks ──────────────────────────────────────────────────────────────────────────────── +fn building_checks_blocks() -> List { + [ + h2(text: "Building & checks"), + ul(items: [ + li(text: "`cargo test --workspace` · `cargo clippy --all-targets -- -D warnings` · `cargo fmt --all --check`"), + li(text: "one-time: `git config core.hooksPath .githooks` (pre-push runs `cargo fmt`)"), + li(text: "CI (`gunbc ci` generates `.github/workflows/ci.yml`; all `v1-compiler` seed bins, no shell gate): **one** composed floor pass — `claim_executor --source-root src/v2 --source-root dsl --plan-entry src/v2/workflow/ci_floor_plan.dag --plan-function gunbc_ci_floor_batches`. The v2 scheduler decides the batches from the single-authority spec (`gunbc.ci_spec`); the only structural fact the plan adds is *compile-clean gates the rest* (batch-1 `dsl_compile_clean_gate` → batch-2 everything else, a dependency edge). Witness **discovery is tree-wide and marker-driven** (roster derived from `gunbc.ci_layer_roots`: `witness_layer_roots = [src/v2, dsl]`, `witness_discovery_scan_dirs = [dsl/test/claim]`): the source-root pass walks every `*_test.dag` under **both** trees and auto-enrolls each `test fn` — fail-closed, a `test fn` in a non-`_test.dag` file is a hygiene violation, so a witness cannot silently hide; the scan-dir pass adds `unified_claim_*` BoolWitnessClaim decls. So a new witness is floor-covered by *naming it* `_test.dag` with a `test fn`, not by hand-enrolling it (`discover_floor_corpus_rows` in `cli_run.rs`). Batch-2 also carries the effectful gates: rust fmt/clippy monolith gate (when a `.rs` changes), emit-host MVP smokes, layering-imports scan + perturb receipts, source-root-ingest, and the `ci.yml` drift+parse gate (ci.yml == `gunbc ci` output). The compile-clean gate is `--target rust` — SCAFFOLD pending the `v1.compiler.dag_collect` identity-key fix that blocks `--target dag`. Parse fallback: hand-written `yaml_check` bin (SCAFFOLD — `src/v1/stage0/src/bin/yaml_check.rs`)."), + ]), + ] +} + +// ── assembled document ─────────────────────────────────────────────────────────────────────────────── +fn design_blocks() -> List { + concat(preamble_blocks(), + concat(section_1_blocks(), + concat(section_2_blocks(), + concat(section_3_blocks(), + concat(section_4_blocks(), + concat(section_5_blocks(), + concat(section_6_blocks(), + concat(section_7_blocks(), + concat(failure_modes_blocks(), + concat(open_threads_blocks(), + building_checks_blocks())))))))))) +} + +fn design_document() -> MarkdownDocument { + MarkdownDocument { blocks: design_blocks() } +} + +fn expected_design_md() -> String { + serialize_markdown_source(doc: design_document()) +} + +fn design_drifted(committed: String) -> Bool { + !(committed == expected_design_md()) +} diff --git a/dsl/gunbc/generated_artifact.dag b/dsl/gunbc/generated_artifact.dag index fa10f06e9a2..2542085f119 100644 --- a/dsl/gunbc/generated_artifact.dag +++ b/dsl/gunbc/generated_artifact.dag @@ -25,12 +25,14 @@ 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 } // Q1 — the closed registry of artifacts gunbc generates from a .dag authority. type GeneratedArtifact = CiYamlArtifact | GitignoreArtifact | RoadmapArtifact + | DesignArtifact // 🟡 §5 COMPLETENESS RESIDUE: the gate folds this LIST. A new variant added to GeneratedArtifact + its // path/generate arms but FORGOTTEN here is silently UNGATED — the "add a row -> auto-gated" promise fails @@ -45,7 +47,8 @@ type GeneratedArtifact data generated_artifact_registry: List = [ CiYamlArtifact, GitignoreArtifact, - RoadmapArtifact + RoadmapArtifact, + DesignArtifact ] // path: where the generated bytes live in the working tree. @@ -54,6 +57,7 @@ fn artifact_path(a: GeneratedArtifact) -> String { CiYamlArtifact => ".github/workflows/ci.yml" GitignoreArtifact => ".gitignore" RoadmapArtifact => "ROADMAP.md" + DesignArtifact => "DESIGN.md" } } @@ -64,6 +68,7 @@ fn artifact_generate(a: GeneratedArtifact) -> String { CiYamlArtifact => expected_ci_yml() GitignoreArtifact => expected_gitignore() RoadmapArtifact => expected_roadmap_md() + DesignArtifact => expected_design_md() } } @@ -96,6 +101,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 } } } diff --git a/dsl/test/claim/design_argument_witness_test.dag b/dsl/test/claim/design_argument_witness_test.dag index 091bdc3f02f..67964e406c4 100644 --- a/dsl/test/claim/design_argument_witness_test.dag +++ b/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,25 @@ test fn design_s1_argument_is_non_vacuous() -> Bool { argument_is_non_vacuous(design_section_1_argument) } +// The whole-document argument (A1–A3 + §1–§7 headline claims) is a valid syllogism: non-vacuous, +// orphan-free, acyclic, axiom-set-closed — every section's claim chains back to an axiom (DESIGN §1 +// open-thread, §7 recursion turned on this document). +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, diff --git a/dsl/test/claim/generated_artifact_drift_test.dag b/dsl/test/claim/generated_artifact_drift_test.dag index 887089ea658..bbc905bca4f 100644 --- a/dsl/test/claim/generated_artifact_drift_test.dag +++ b/dsl/test/claim/generated_artifact_drift_test.dag @@ -17,7 +17,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 @@ -44,9 +44,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") } // (2b) Discriminating: synthetic ignored paths DO classify ignored — the derivation genuinely reads the @@ -66,13 +68,15 @@ fn witness_ignored_paths_excluded() -> Bool { // gunbc.generated_artifact). The named constructors here are authored from the TYPE, a distinct site from // the registry data literal. 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) } // ci.yml carries the extra YAML-parse validation seam (preserved from the old CiYamlGate); the others @@ -80,6 +84,7 @@ fn witness_registry_complete() -> Bool { 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) } From 33a9b821d617c56e00c7221e4348e83a7c64a9ee Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:17:03 +0000 Subject: [PATCH 04/10] WIP: get design docs into .dag --- dsl/gunbc/design_document.dag | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index c12ad072da0..5ba5002e510 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -87,7 +87,7 @@ fn section_2_blocks() -> List { li_blocks(blocks: [ p(text: "**Deep — every concept decomposed to grounded atoms.** Nothing is opaque that isn't *genuinely* atomic. The move is `decompress → map → reduce`: reveal the structure the source names, **map** each part onto the concept that already exists (DFS the concept DAG first), **reduce** duplicates. A `String` leaf hiding named parts is anemic modeling."), ul(items: [ - li(text: "*e.g.* `\"LGA4926\"` → `CpuSocket { package: LandGridArray, contact_count: 4926 }` (the number is a grounded `Int`) and `\"HMA82GR7AFR4N-VK\"` → `DramModuleCatalogRow { chip_width: bit_width(4), rank_count: 1, buffering: Registered }` (the numeric organization axes decoded from the part number ground into existing magnitudes — `chip_width` reuses `BitWidth`, `rank_count` is a cardinal `Int` — not a fresh enum re-inventing bit-width; the categorical axis stays a closed enum); `Cost = Time|Space|Energy` → a record (every cost has all three); still-anemic today: `product.compute_fabric`'s `StorageDevice` has no PCIe-gen/lane-count axis (storage's rank/width). (`GpuFacts.vendor`, once a bare `NonEmptyStr` where `CpuVendor` was a closed enum, is now grounded on the single `Vendor` authority — see §3.)"), + li(text: "*e.g.* `\"LGA4926\"` → `CpuSocket \{ package: LandGridArray, contact_count: 4926 \}` (the number is a grounded `Int`) and `\"HMA82GR7AFR4N-VK\"` → `DramModuleCatalogRow \{ chip_width: bit_width(4), rank_count: 1, buffering: Registered \}` (the numeric organization axes decoded from the part number ground into existing magnitudes — `chip_width` reuses `BitWidth`, `rank_count` is a cardinal `Int` — not a fresh enum re-inventing bit-width; the categorical axis stays a closed enum); `Cost = Time|Space|Energy` → a record (every cost has all three); still-anemic today: `product.compute_fabric`'s `StorageDevice` has no PCIe-gen/lane-count axis (storage's rank/width). (`GpuFacts.vendor`, once a bare `NonEmptyStr` where `CpuVendor` was a closed enum, is now grounded on the single `Vendor` authority — see §3.)"), ]), ]), ]), @@ -101,7 +101,7 @@ fn section_3_blocks() -> List { h2(text: "3. Single authority (what keeps §2 from being undone)"), p(text: "Minimization holds only if each fact lives in exactly one place. The recurring violation is **nicknaming — a second name for one concept** — which duplicates work at the meaning layer and, since we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks (classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep its real names, declare its version, model what the API actually returns), rather than re-coining them. Corollaries: the layer DAG is strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the rename test). A direct consequence for `extdeps/` service operations, three separable facts that must not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract (inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** (which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, `--all-targets`); the tell that (b) has fused is the same operation forked once per transport (GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact rows; corpus RED witnesses execute against live `dsl/extdeps/**` via `filesystem_read` (dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* interface↔realization seam, not only service ops: the cited data behind an agnostic std surface de-fuses exactly as a transport does, and its directional reading is the same — the *dispatch* that selects a realization is itself realization, so it sits peripheral (`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that *matched* over its realizations would have to name them, inverting the import arrow above). What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the `Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion."), ul(items: [ - li(text: "*e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one \"vendor\" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor` is the §2-horizontal \"one concept, every breadth\"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/{cpu,memory}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` (\"projection only\"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/{ubuntu,windows,macos,os}.dag` (\"dispatch lives in extdeps/, not std/\", promoted from that hub header)."), + li(text: "*e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one \"vendor\" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor` is the §2-horizontal \"one concept, every breadth\"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/\{cpu,memory\}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` (\"projection only\"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/\{ubuntu,windows,macos,os\}.dag` (\"dispatch lives in extdeps/, not std/\", promoted from that hub header)."), ]), ] } @@ -125,7 +125,7 @@ fn section_5_blocks() -> List { h2(text: "5. Fail-closed (§1's safety axis — harm reduction)"), p(text: "Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded \"forever\" ≠ an \"unknown\" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches \"never\"). The word **\"never\" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — \"done\" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.)"), ul(items: [ - li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 { x + y }`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types."), + li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 \{ x + y \}`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types."), ]), ] } @@ -168,7 +168,7 @@ fn open_threads_blocks() -> List { ul(items: [ li(text: "model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project)"), li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), - li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), + li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), ]), ] From a36c503ce3699f9b2d4ea04b7722e8784d376fb2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:27:55 +0000 Subject: [PATCH 05/10] WIP: get design docs into .dag --- DESIGN.md | 217 ++++------------------------- dsl/extdeps/languages/markdown.dag | 14 +- 2 files changed, 41 insertions(+), 190 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index f7dc2f9f8fb..6a252d8e26b 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -1,13 +1,8 @@ # gunbc — Design -`README.md` and `CLAUDE.md` symlink here — this is the single source of truth. (v1 ships the `gunbc` -CLI and is v2's seed · v3 was removed, migrated into v1 · v2 is active.) +`README.md` and `CLAUDE.md` symlink here — this is the single source of truth. (v1 ships the `gunbc` CLI and is v2's seed · v3 was removed, migrated into v1 · v2 is active.) -This document is reasoned **serially**: §1 fixes the axioms, and each later section is a consequence of -the ones before it (or an independent peer) — never a restatement of it. The principles below apply recursively, including to -this document. It is a living draft rebuilt from first principles (the prior ~30k-line doc corpus was -bankrupted 2026-06-16; it remains in git history). Examples are verified against the live tree or a -git-history receipt; open threads are collected at the end. +This document is reasoned **serially**: §1 fixes the axioms, and each later section is a consequence of the ones before it (or an independent peer) — never a restatement of it. The principles below apply recursively, including to this document. It is a living draft rebuilt from first principles (the prior ~30k-line doc corpus was bankrupted 2026-06-16; it remains in git history). Examples are verified against the live tree or a git-history receipt; open threads are collected at the end. --- @@ -15,233 +10,77 @@ git-history receipt; open threads are collected at the end. The assumptions everything else rests on. Three **axioms** — assumed, not derived: -- **A1 — there is a goal.** To *solve a problem* presupposes an agent with a goal to satisfy; with no - goal there is nothing to optimize. -- **A2 — time is the value.** Every agent intrinsically values time — it is finite and is the substance - of acting at all: **time is life**. It is the one value we may assume is *shared*. -- **A3 — agreement is temporal.** Intersubjective agreement — two parties holding the same fact — is - possible only *across* time, and only on what stays stable under it. +- **A1 — there is a goal.** To *solve a problem* presupposes an agent with a goal to satisfy; with no goal there is nothing to optimize. +- **A2 — time is the value.** Every agent intrinsically values time — it is finite and is the substance of acting at all: **time is life**. It is the one value we may assume is *shared*. +- **A3 — agreement is temporal.** Intersubjective agreement — two parties holding the same fact — is possible only *across* time, and only on what stays stable under it. Three things follow, in order: -- **From A1 and A2 — the solution is minimal, safe, efficient.** A solution is good exactly insofar as - it spends less of the only thing valued, time; and time is spent three ways: +- **From A1 and A2 — the solution is minimal, safe, efficient.** A solution is good exactly insofar as it spends less of the only thing valued, time; and time is spent three ways: - **cost** — time to run (cheap to run and to feed); - **safety** — time to recover from a silent wrong answer, paid later at interest (harm reduction); - **complexity** — time to change (it stays cheap to maintain). - So the three are not preferences layered on — they are A2 applied to A1, and the project optimizes - them jointly. -- **From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a - fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy. -- **At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, - time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on - grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace - convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the - universal frameworks and real upstream rather than re-coining them — a nickname is convention standing - where physics was available. + So the three are not preferences layered on — they are A2 applied to A1, and the project optimizes them jointly. +- **From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy. +- **At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the universal frameworks and real upstream rather than re-coining them — a nickname is convention standing where physics was available. ## 2. Minimize redundancy (the master move for cost and complexity) -Redundant work — **duplicated, unnecessary, or irrelevant** — loses on all three of §1's quantities at -once: it costs more to run, it widens the surface where harm hides, and it adds complexity to maintain. -So a perfectly DRY process is, *by the meaning of redundant*, the minimal/efficient one; minimizing -redundancy is therefore the master move for §1's cost and complexity axes (the safety axis is §5). -Through §1's time lens this is *why* DRY matters at all: redundant work **defers** cost into the -future — it shoves a problem onto a later fixer, or builds a process destined to be thrown out — so DRY -is the refusal to spend someone's future time to buy the author's present convenience; it values time -**holistically**, across every party and all of it, not just the here-and-now. Redundancy is removed -along exactly two directions — not separate "DRY rules," but one move seen two ways: - -- **Horizontal — one concept, every scale and breadth.** Model a concept once; derive every use - (model-local / derive-global). At the right layer there is nothing fundamentally different between - scales, so the *same* concept spans nanosecond memoization and broad infra deployment — the - Realization pattern (content-addressed pure-spec → host-effect; one kernel, N handlers). +Redundant work — **duplicated, unnecessary, or irrelevant** — loses on all three of §1's quantities at once: it costs more to run, it widens the surface where harm hides, and it adds complexity to maintain. So a perfectly DRY process is, *by the meaning of redundant*, the minimal/efficient one; minimizing redundancy is therefore the master move for §1's cost and complexity axes (the safety axis is §5). Through §1's time lens this is *why* DRY matters at all: redundant work **defers** cost into the future — it shoves a problem onto a later fixer, or builds a process destined to be thrown out — so DRY is the refusal to spend someone's future time to buy the author's present convenience; it values time **holistically**, across every party and all of it, not just the here-and-now. Redundancy is removed along exactly two directions — not separate "DRY rules," but one move seen two ways: + +- **Horizontal — one concept, every scale and breadth.** Model a concept once; derive every use (model-local / derive-global). At the right layer there is nothing fundamentally different between scales, so the *same* concept spans nanosecond memoization and broad infra deployment — the Realization pattern (content-addressed pure-spec → host-effect; one kernel, N handlers). - *e.g.* `dsl/std/integer.dag`: `Int8`…`UInt128` are 10 `Compose>` rows, one axis not 10 types. Realization spans resolve-cost (ns) → sccache → §10 OS provisioning on one content-hash. Cost of *not* doing it: eleven hand-rolled v1 `HashMap` caches, and v2 still recurs (`ParseTable`). -- **Deep — every concept decomposed to grounded atoms.** Nothing is opaque that isn't *genuinely* - atomic. The move is `decompress → map → reduce`: reveal the structure the source names, **map** each - part onto the concept that already exists (DFS the concept DAG first), **reduce** duplicates. A - `String` leaf hiding named parts is anemic modeling. +- **Deep — every concept decomposed to grounded atoms.** Nothing is opaque that isn't *genuinely* atomic. The move is `decompress → map → reduce`: reveal the structure the source names, **map** each part onto the concept that already exists (DFS the concept DAG first), **reduce** duplicates. A `String` leaf hiding named parts is anemic modeling. - *e.g.* `"LGA4926"` → `CpuSocket { package: LandGridArray, contact_count: 4926 }` (the number is a grounded `Int`) and `"HMA82GR7AFR4N-VK"` → `DramModuleCatalogRow { chip_width: bit_width(4), rank_count: 1, buffering: Registered }` (the numeric organization axes decoded from the part number ground into existing magnitudes — `chip_width` reuses `BitWidth`, `rank_count` is a cardinal `Int` — not a fresh enum re-inventing bit-width; the categorical axis stays a closed enum); `Cost = Time|Space|Energy` → a record (every cost has all three); still-anemic today: `product.compute_fabric`'s `StorageDevice` has no PCIe-gen/lane-count axis (storage's rank/width). (`GpuFacts.vendor`, once a bare `NonEmptyStr` where `CpuVendor` was a closed enum, is now grounded on the single `Vendor` authority — see §3.) -The test that an edit actually *reduced* redundancy rather than moving it: **net concepts must not grow -by re-invention.** Decomposing a leaf by minting a fresh authority for a concept that already exists is -a failed decomposition. +The test that an edit actually *reduced* redundancy rather than moving it: **net concepts must not grow by re-invention.** Decomposing a leaf by minting a fresh authority for a concept that already exists is a failed decomposition. ## 3. Single authority (what 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** — which duplicates work at the meaning layer and, since -we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork -always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this -programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks -(classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep -its real names, declare its version, model what the API actually returns), rather than re-coining them. -Corollaries: the layer DAG is -strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, -not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the -rename test). A direct consequence for `extdeps/` service operations, three separable facts that must -not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract -(inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / -SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a -single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname -for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** -(which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* -fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has -leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, -`--all-targets`); the tell that (b) has fused is the same operation forked once per transport -(GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. -Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact -rows; corpus RED witnesses execute against live `dsl/extdeps/**` via `filesystem_read` -(dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* -interface↔realization seam, not only service ops: the cited data behind an agnostic std -surface de-fuses exactly as a transport does, and its directional reading is the same — the -*dispatch* that selects a realization is itself realization, so it sits peripheral -(`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that -*matched* over its realizations would have to name them, inverting the import arrow above). -What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS -taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays -central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the -`Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion. +Minimization holds only if each fact lives in exactly one place. The recurring violation is **nicknaming — a second name for one concept** — which duplicates work at the meaning layer and, since we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks (classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep its real names, declare its version, model what the API actually returns), rather than re-coining them. Corollaries: the layer DAG is strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the rename test). A direct consequence for `extdeps/` service operations, three separable facts that must not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract (inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** (which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, `--all-targets`); the tell that (b) has fused is the same operation forked once per transport (GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact rows; corpus RED witnesses execute against live `dsl/extdeps/**` via `filesystem_read` (dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* interface↔realization seam, not only service ops: the cited data behind an agnostic std surface de-fuses exactly as a transport does, and its directional reading is the same — the *dispatch* that selects a realization is itself realization, so it sits peripheral (`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that *matched* over its realizations would have to name them, inverting the import arrow above). What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the `Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion. - *e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one "vendor" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor` is the §2-horizontal "one concept, every breadth"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/{cpu,memory}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` ("projection only"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/{ubuntu,windows,macos,os}.dag` ("dispatch lives in extdeps/, not std/", promoted from that hub header). ## 4. The closed, grounded substrate (what makes §2–§3 decidable) -You can unify and decompose *mechanically* only in a closed, grounded system — so the substrate is -built for it. A program is a dependency graph over two primitives (`Node` + `Edge`) and a closed -vocabulary (6 connectives + 5 behaviors); surface syntax is sugar that adds no power. Execution is -**bounded and forward** (cyclic relations via acyclic encodings, never cyclic values; recursion is -sugar over `Loop`), so decidability and termination *fall out* rather than being separately proved. -**Grounding is intersubjective** — point at a shared framework, not an internal taxonomy — and in a -closed system **a heuristic is never necessary**: the richer source always exists or can be written. -This is *why* the structure is acyclic — a DAG in the substrate, serial reasoning in this document -(recursively, per the preamble): intersubjective agreement holds only **across time** (§1), which -demands claims that stay stable under it, so each is written syllogistically — a consequence-chain you -can re-interrogate and that never wavers (algebra), never a cycle that could quietly redefine itself. - -Because the substrate is closed and grounded, the wins of §2 fall out for free: operations come from -*inhabitance* (no per-type ops); and emission, ingestion, and coercion are **one** total decision -procedure run in different directions (the epistemic chain *is* the emission algorithm — N models, not -N×M adapters; every refusal a located, typed mismatch). +You can unify and decompose *mechanically* only in a closed, grounded system — so the substrate is built for it. A program is a dependency graph over two primitives (`Node` + `Edge`) and a closed vocabulary (6 connectives + 5 behaviors); surface syntax is sugar that adds no power. Execution is **bounded and forward** (cyclic relations via acyclic encodings, never cyclic values; recursion is sugar over `Loop`), so decidability and termination *fall out* rather than being separately proved. **Grounding is intersubjective** — point at a shared framework, not an internal taxonomy — and in a closed system **a heuristic is never necessary**: the richer source always exists or can be written. This is *why* the structure is acyclic — a DAG in the substrate, serial reasoning in this document (recursively, per the preamble): intersubjective agreement holds only **across time** (§1), which demands claims that stay stable under it, so each is written syllogistically — a consequence-chain you can re-interrogate and that never wavers (algebra), never a cycle that could quietly redefine itself. + +Because the substrate is closed and grounded, the wins of §2 fall out for free: operations come from *inhabitance* (no per-type ops); and emission, ingestion, and coercion are **one** total decision procedure run in different directions (the epistemic chain *is* the emission algorithm — N models, not N×M adapters; every refusal a located, typed mismatch). - *e.g.* `dsl/std/algebra.dag` derives `Int.add` from `Int` inhabiting a ring (ops aren't listed per type); idempotency dissolved from an `idempotent: Bool` flag into the `EffectShape` variant; termination is *checked, not discovered* — `DescentEvidence = Strict | NonIncreasing | DescentUnknown` inhabits a `BoundedLattice` with bottom = fail-closed. - *e.g.* **one grammar, read in both directions** (§2 horizontal, not an adapter pair): ingest selects a production *forward* to fold surface syntax into a core `Node`; emit (`serialize_target ∘ translate`) selects from the *same* `target_model_edge_translation_rules` rows *backward* — the structural inverse, not a second emitter — so a new target language is rows authored in `extdeps/languages/`, never an edit to the fold (N rows, not N×M parser/emitter pairs). Coercion is that same move turned sideways: whether one model inhabits another is a homomorphism check (`coercion_fold` via `find_witness`), the same epistemic chain the emitter walks. One procedure asked in three directions, not three procedures. ## 5. Fail-closed (§1's safety axis — harm reduction) -Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's -safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — -a bridge collapses, it does not warn. Every path succeeds fully or -fails with a typed, located diagnostic; no fabricated plausible output (a bounded "forever" ≠ an -"unknown" error). Relax toward application-layer leniency only under protest, and lean to infra so -others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — -**correctness by construction, not validation.** A check that re-states a constraint the model already -carries is a *second representation* of it (§2/§3): so prefer a single authority from which the -realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, -which concedes the bad state *is* writable. The tell that a check was validation standing where -construction was available: it can be satisfied by editing the *declaration* while the realization still -lies (a key-completeness check went green when the spec was edited while the realizer kept faking the -cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / -necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable -only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and -grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on -its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion` -grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches "never"). The word -**"never" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming -one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is -**specification-without-execution**: a typecheck and -a `.contains()` grep are *not* consumers — "done" means a real consumer **green by execution** plus a -discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, -type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat -your own output as unverified until a consumer runs it green.) +Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded "forever" ≠ an "unknown" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches "never"). The word **"never" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — "done" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.) - *e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 { x + y }`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. ## 6. How to work (given §1–§5 — these coexist) -- **Model:** DFS the concept DAG before inventing vocabulary; fact-bundle modeling (invent or reuse on - proven coincidence, never bare-alias); a finished stage is one fold (any non-fold residue is either a - named irreducible kernel or un-migrated modeling — there is no third); model just-in-time and let the - mark on the carrier be the authority (no parallel-ledger docs); every scaffold lands with a named - dissolution trigger. -- **Prioritize holistically, not by the bottleneck:** balance the quantitative and the qualitative — - don't anchor on one KPI (you'll hit it at a cost) or on pure taste. Map the cause→effect across - sections; a 5ms step doesn't get a pass for not being the 80s one (it might be a 5ns step). - Root-cause to the language layer and fix related systems *together* — a local subsystem patch is the - forked-logic trap. **Denominate the benefit:** the deliverable is a *displaced cost* (§1's time — a - pain someone pays to remove); the lens/substrate is the *mechanism* (the moat), not the product. A - lens — or any construction wall — is on-dial exactly insofar as it is the cheapest path to such a pain. - Priced in elegance instead, the work is self-referential and unbounded (the purity trap — the economic - twin of "never" in §5; an extensible substrate's infinite improvability dissolving its own bound). -- **Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it - concedes the bad state is writable), so make the class unwritable by single authority where you can and - reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure - reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware - the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is - itself a lie, so an **executable** hygiene check must keep every lens either wired (a discovered - fail-closed witness) or deleted — that backstop runs over the corpus and is *not* superseded by the - authoring-time construction-justification judgment, which layers on top of it. +- **Model:** DFS the concept DAG before inventing vocabulary; fact-bundle modeling (invent or reuse on proven coincidence, never bare-alias); a finished stage is one fold (any non-fold residue is either a named irreducible kernel or un-migrated modeling — there is no third); model just-in-time and let the mark on the carrier be the authority (no parallel-ledger docs); every scaffold lands with a named dissolution trigger. +- **Prioritize holistically, not by the bottleneck:** balance the quantitative and the qualitative — don't anchor on one KPI (you'll hit it at a cost) or on pure taste. Map the cause→effect across sections; a 5ms step doesn't get a pass for not being the 80s one (it might be a 5ns step). Root-cause to the language layer and fix related systems *together* — a local subsystem patch is the forked-logic trap. **Denominate the benefit:** the deliverable is a *displaced cost* (§1's time — a pain someone pays to remove); the lens/substrate is the *mechanism* (the moat), not the product. A lens — or any construction wall — is on-dial exactly insofar as it is the cheapest path to such a pain. Priced in elegance instead, the work is self-referential and unbounded (the purity trap — the economic twin of "never" in §5; an extensible substrate's infinite improvability dissolving its own bound). +- **Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie, so an **executable** hygiene check must keep every lens either wired (a discovered fail-closed witness) or deleted — that backstop runs over the corpus and is *not* superseded by the authoring-time construction-justification judgment, which layers on top of it. - *e.g.* one catamorphism `fold_node` is reused by all 7 v2 stages; #4699 dissolved `06_translate` 4,912→3,973 lines (`_go` accumulators 35→0); a 6-line `merge_envs` root fix cut reconcile from 81% of the pipeline to 6% (~2× self-compile) — the symptom recurs wherever the root is unfixed (v2 still hand-rolls `ParseTable` because the Realization carrier is staged, not inhabited). ## 7. Self-hosting (the principles applied to the compiler itself) -The compiler is a pure transform and an ordinary substrate fact, analyzable by its own lenses. It is -written in itself, self-emits to a bit-identical fixed point (the `.dag` graph is the truth; Rust is -one realization, a seed that shrinks to zero), and its tests are data. Its ontology dissolves into -`std/` — no dual representation at the compiler/user boundary. This is the recursion: every principle -above governs the system that implements them, and this document. - -The recursion's payoff is that **language design itself opens up.** It is normally locked — not by lack -of will but by cost: a new check means owning a *compiler fork*, and a new language means an *adoption* -problem. Both are dissolved here at once: a wall is a **row** (§2, no fork), and because the substrate is -medium-agnostic — one grammar read in both directions over many media (§4) — that row applies *on top of -an existing language* (no adoption). So language design collapses (compiler-fork × language) → (row + -medium): a domain's bug-class can be made extinct in Rust or TypeScript without forking their compilers. -It is sound exactly where ingest is `Lossless` and **fail-closed** where it is not (the `DecodeFidelity` -boundary, §4) — "any language, with a typed honesty boundary about where the wall holds," not a vibe. -This is §1's *reduce convention to necessity* at the meta-level, and the place the purity trap bites -hardest: bounded by §5 ("never" = decidability) and §6 (priced in displaced cost, not elegance). +The compiler is a pure transform and an ordinary substrate fact, analyzable by its own lenses. It is written in itself, self-emits to a bit-identical fixed point (the `.dag` graph is the truth; Rust is one realization, a seed that shrinks to zero), and its tests are data. Its ontology dissolves into `std/` — no dual representation at the compiler/user boundary. This is the recursion: every principle above governs the system that implements them, and this document. + +The recursion's payoff is that **language design itself opens up.** It is normally locked — not by lack of will but by cost: a new check means owning a *compiler fork*, and a new language means an *adoption* problem. Both are dissolved here at once: a wall is a **row** (§2, no fork), and because the substrate is medium-agnostic — one grammar read in both directions over many media (§4) — that row applies *on top of an existing language* (no adoption). So language design collapses (compiler-fork × language) → (row + medium): a domain's bug-class can be made extinct in Rust or TypeScript without forking their compilers. It is sound exactly where ingest is `Lossless` and **fail-closed** where it is not (the `DecodeFidelity` boundary, §4) — "any language, with a typed honesty boundary about where the wall holds," not a vibe. This is §1's *reduce convention to necessity* at the meta-level, and the place the purity trap bites hardest: bounded by §5 ("never" = decidability) and §6 (priced in displaced cost, not elegance). --- ## Recurring failure modes (instances of §3–§5, kept for pattern-matching) -hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — -split into named variants) · cache impurity (key on declared-input content; byte-identical -cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by -execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden -string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is -still a violation) · internal review finds missing tests, external review finds missing checks. +hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks. ## Open threads -- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every - claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on - the argument itself; the §7 recursion, with this document as the first target). (operator's next - project) +- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked) -- the model↔realization fork is systemic, and where unfinished it fails open: every primitive is - modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage - is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no - `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` - chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the - *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises - `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native - `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and - `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key - authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; - reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** - (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and - `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is - the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, - so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its - realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded - (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` - `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until - the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). - **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper - root, its own runway). (operator: `==` fail-closed, 2026-06-20) +- the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) ## Building & checks diff --git a/dsl/extdeps/languages/markdown.dag b/dsl/extdeps/languages/markdown.dag index 52412194026..75702e35b2a 100644 --- a/dsl/extdeps/languages/markdown.dag +++ b/dsl/extdeps/languages/markdown.dag @@ -145,7 +145,19 @@ fn md_item(marker: String, blocks: List, 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))) } + // Continuation block of a list item. A nested LIST handles its own indentation (md_nested at + // depth+1) and sits on the next line. A LEAF continuation (a paragraph / code block after a nested + // list) needs a CommonMark loose-list continuation: a blank line then indentation to the item's + // content column (depth+1 list-indents). Without this it renders as a lazy continuation of the + // preceding sub-bullet. Lists keep their existing rendering, so artifacts whose items only carry + // nested lists (ROADMAP.md) are byte-unchanged. + 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)) + _ => 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 } From 3b7631356cb06d636b758f852117b5288a4acfe8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:32:43 +0000 Subject: [PATCH 06/10] Generate DESIGN.md from .dag + enforce the document's syllogism MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit DESIGN.md is now a drift-gated projection of its .dag model (DESIGN §7: the document is the first target of the recursion), the same way ROADMAP.md is: - std.markdown + serializer: add the missing ThematicBreak block (the `---` rules) with arms in all exhaustive match sites; md_item now renders a leaf continuation block (a paragraph after a nested sub-list) as a CommonMark loose-list continuation (blank line + indent), leaving list-continuations — and therefore ROADMAP.md — byte-unchanged. - gunbc.design_document: full DESIGN.md as typed markdown blocks; one TextInline per paragraph carries the raw markdown source (same convention as roadmap_authority). expected_design_md() is the single generator. - gunbc.design_argument: extend the §1 axioms/propositions with §2-§7 headline propositions, each premised on the sections it follows from. The syllogism lens (std.syllogism.argument_form_is_valid) now checks the WHOLE document is non-vacuous, orphan-free, acyclic, and axiom-set-closed — the §1 open-thread. - generated_artifact + universal drift gate + completeness witness: register DesignArtifact -> DESIGN.md -> expected_design_md(); roster bumped to 4. Verified by execution: drift gate ExitSuccess; ROADMAP.md byte-unchanged; all syllogism + completeness witnesses green incl. orphan/cycle/smuggled-axiom/ vacuous negative controls; regenerated DESIGN.md content-identical to the original modulo line-wrapping (paragraphs unwrapped, as in ROADMAP.md). Co-Authored-By: Claude Opus 4.8 --- dsl/gunbc/design_argument.dag | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/dsl/gunbc/design_argument.dag b/dsl/gunbc/design_argument.dag index eac87064eaa..575b2754393 100644 --- a/dsl/gunbc/design_argument.dag +++ b/dsl/gunbc/design_argument.dag @@ -93,8 +93,7 @@ data design_section_2_to_7_propositions: List = [ } ] -data design_propositions: List = - concat(design_section_1_propositions, design_section_2_to_7_propositions) +data design_propositions: List = concat(design_section_1_propositions, design_section_2_to_7_propositions) // The whole-document argument: A1–A3 + every section's headline claim. The syllogism lens // (std.syllogism.argument_form_is_valid) checks it is non-vacuous, orphan-free, acyclic, and From d121095cd6b929d8e35208392b1773574389fe35 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:40:43 +0000 Subject: [PATCH 07/10] WIP: get design docs into .dag --- dsl/extdeps/languages/markdown.dag | 6 --- dsl/gunbc/design_argument.dag | 14 ----- dsl/gunbc/design_document.dag | 54 +++++-------------- .../claim/design_argument_witness_test.dag | 3 -- 4 files changed, 13 insertions(+), 64 deletions(-) diff --git a/dsl/extdeps/languages/markdown.dag b/dsl/extdeps/languages/markdown.dag index 75702e35b2a..881a55e61b7 100644 --- a/dsl/extdeps/languages/markdown.dag +++ b/dsl/extdeps/languages/markdown.dag @@ -145,12 +145,6 @@ fn md_item(marker: String, blocks: List, sp: MarkdownSpellings, d } { idx: 1, out: lead } } else { - // Continuation block of a list item. A nested LIST handles its own indentation (md_nested at - // depth+1) and sits on the next line. A LEAF continuation (a paragraph / code block after a nested - // list) needs a CommonMark loose-list continuation: a blank line then indentation to the item's - // content column (depth+1 list-indents). Without this it renders as a lazy continuation of the - // preceding sub-bullet. Lists keep their existing rendering, so artifacts whose items only carry - // nested lists (ROADMAP.md) are byte-unchanged. 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)) diff --git a/dsl/gunbc/design_argument.dag b/dsl/gunbc/design_argument.dag index 575b2754393..2db0706901e 100644 --- a/dsl/gunbc/design_argument.dag +++ b/dsl/gunbc/design_argument.dag @@ -49,11 +49,6 @@ data design_section_1_argument: Argument = Argument { propositions: design_section_1_propositions } -// §2–§7: one headline proposition per section, each premised on the sections it is a consequence of. -// This is the document's serial spine (DESIGN preamble: "each later section is a consequence of the ones -// before it (or an independent peer)") made a checked consequence-chain — no orphan, no cycle, every claim -// reachable from A1–A3 via §1. The full prose of each section lives in gunbc.design_document; binding the -// two (render each section FROM its proposition) is the dissolution trigger below. data design_section_2_to_7_propositions: List = [ Proposition { @@ -95,15 +90,6 @@ data design_section_2_to_7_propositions: List = [ data design_propositions: List = concat(design_section_1_propositions, design_section_2_to_7_propositions) -// The whole-document argument: A1–A3 + every section's headline claim. The syllogism lens -// (std.syllogism.argument_form_is_valid) checks it is non-vacuous, orphan-free, acyclic, and -// axiom-set-closed — the §1 open-thread "every claim a consequence-chain back to an axiom" turned on -// this document itself (DESIGN §7 recursion). -// -// DISSOLUTION TRIGGER: today the section prose (gunbc.design_document) and these propositions are two -// views of the same claims at different granularity — the proposition is the headline, the document is the -// exposition. Collapse to one authority once design_document renders each section's lead FROM its -// proposition (the document model carrying rich-block claim content), so the headline is single-authored. data design_argument: Argument = Argument { axioms: design_axioms, propositions: design_propositions diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index 5ba5002e510..9c99ec54abb 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -1,15 +1,3 @@ -// gunbc.design_document — DESIGN.md as a .dag projection (DESIGN §7: this document is the first target of -// the recursion — an ordinary substrate fact, generated from its model, drift-gated like ROADMAP.md). -// -// The PROSE is modeled as typed markdown blocks (heading / paragraph / bullet list / thematic break); a -// paragraph carries the raw markdown source as one TextInline (the serializer passes `**bold**`/`code` -// through verbatim — same convention as gunbc.roadmap_authority), unwrapped to a single line. The doc's -// LOGICAL spine (axioms A1–A3 + the §1–§7 consequence-chain) is modeled separately and checked by the -// syllogism lens in gunbc.design_argument; binding the two — render each claim FROM its proposition — is -// the named dissolution trigger (see design_argument.dag). -// -// expected_design_md() is the single generator; gunbc.generated_artifact registers DESIGN.md against it -// and tools.generated_artifact_gate drift-gates it. Do not hand-edit DESIGN.md — regenerate via main_wet. module gunbc.design_document @@ -20,22 +8,15 @@ import std.markdown { } import extdeps.languages.markdown { serialize_markdown_source } -// ── authoring helpers ────────────────────────────────────────────────────────────────────────────── -// A paragraph / heading carries the exact markdown source line (inline formatting survives as literal -// text through the serializer). Wrapped source lines are joined into one line per block. - fn h1(text: String) -> MarkdownBlock { HeadingBlock { level: H1, inlines: [TextInline { text: text }] } } fn h2(text: String) -> MarkdownBlock { HeadingBlock { level: H2, inlines: [TextInline { text: text }] } } fn p(text: String) -> MarkdownBlock { ParagraphBlock { inlines: [TextInline { text: text }] } } fn rule() -> MarkdownBlock { ThematicBreak } -// a bullet item that is a single paragraph fn li(text: String) -> MarkdownListItem { MarkdownListItem { blocks: [p(text: text)] } } -// a bullet item carrying arbitrary blocks (lead paragraph + nested list + …) fn li_blocks(blocks: List) -> MarkdownListItem { MarkdownListItem { blocks: blocks } } fn ul(items: List) -> MarkdownBlock { UnorderedListBlock { items: items } } -// ── preamble ───────────────────────────────────────────────────────────────────────────────────── fn preamble_blocks() -> List { [ h1(text: "gunbc — Design"), @@ -45,7 +26,6 @@ fn preamble_blocks() -> List { ] } -// ── §1 — The objective (the axioms) ──────────────────────────────────────────────────────────────── fn section_1_blocks() -> List { [ h2(text: "1. The objective (the axioms)"), @@ -72,7 +52,6 @@ fn section_1_blocks() -> List { ] } -// ── §2 — Minimize redundancy ─────────────────────────────────────────────────────────────────────── fn section_2_blocks() -> List { [ h2(text: "2. Minimize redundancy (the master move for cost and complexity)"), @@ -95,7 +74,6 @@ fn section_2_blocks() -> List { ] } -// ── §3 — Single authority ────────────────────────────────────────────────────────────────────────── fn section_3_blocks() -> List { [ h2(text: "3. Single authority (what keeps §2 from being undone)"), @@ -106,7 +84,6 @@ fn section_3_blocks() -> List { ] } -// ── §4 — The closed, grounded substrate ────────────────────────────────────────────────────────────── fn section_4_blocks() -> List { [ h2(text: "4. The closed, grounded substrate (what makes §2–§3 decidable)"), @@ -119,7 +96,6 @@ fn section_4_blocks() -> List { ] } -// ── §5 — Fail-closed ───────────────────────────────────────────────────────────────────────────────── fn section_5_blocks() -> List { [ h2(text: "5. Fail-closed (§1's safety axis — harm reduction)"), @@ -130,7 +106,6 @@ fn section_5_blocks() -> List { ] } -// ── §6 — How to work ───────────────────────────────────────────────────────────────────────────────── fn section_6_blocks() -> List { [ h2(text: "6. How to work (given §1–§5 — these coexist)"), @@ -143,7 +118,6 @@ fn section_6_blocks() -> List { ] } -// ── §7 — Self-hosting ──────────────────────────────────────────────────────────────────────────────── fn section_7_blocks() -> List { [ h2(text: "7. Self-hosting (the principles applied to the compiler itself)"), @@ -153,7 +127,6 @@ fn section_7_blocks() -> List { ] } -// ── Recurring failure modes ────────────────────────────────────────────────────────────────────────── fn failure_modes_blocks() -> List { [ h2(text: "Recurring failure modes (instances of §3–§5, kept for pattern-matching)"), @@ -161,7 +134,6 @@ fn failure_modes_blocks() -> List { ] } -// ── Open threads ───────────────────────────────────────────────────────────────────────────────────── fn open_threads_blocks() -> List { [ h2(text: "Open threads"), @@ -174,7 +146,6 @@ fn open_threads_blocks() -> List { ] } -// ── Building & checks ──────────────────────────────────────────────────────────────────────────────── fn building_checks_blocks() -> List { [ h2(text: "Building & checks"), @@ -186,19 +157,20 @@ fn building_checks_blocks() -> List { ] } -// ── assembled document ─────────────────────────────────────────────────────────────────────────────── fn design_blocks() -> List { - concat(preamble_blocks(), - concat(section_1_blocks(), - concat(section_2_blocks(), - concat(section_3_blocks(), - concat(section_4_blocks(), - concat(section_5_blocks(), - concat(section_6_blocks(), - concat(section_7_blocks(), - concat(failure_modes_blocks(), - concat(open_threads_blocks(), - building_checks_blocks())))))))))) + flat_map([ + preamble_blocks(), + section_1_blocks(), + section_2_blocks(), + section_3_blocks(), + section_4_blocks(), + section_5_blocks(), + section_6_blocks(), + section_7_blocks(), + failure_modes_blocks(), + open_threads_blocks(), + building_checks_blocks(), + ], bs => bs) } fn design_document() -> MarkdownDocument { diff --git a/dsl/test/claim/design_argument_witness_test.dag b/dsl/test/claim/design_argument_witness_test.dag index 67964e406c4..8577a13435f 100644 --- a/dsl/test/claim/design_argument_witness_test.dag +++ b/dsl/test/claim/design_argument_witness_test.dag @@ -15,9 +15,6 @@ test fn design_s1_argument_is_non_vacuous() -> Bool { argument_is_non_vacuous(design_section_1_argument) } -// The whole-document argument (A1–A3 + §1–§7 headline claims) is a valid syllogism: non-vacuous, -// orphan-free, acyclic, axiom-set-closed — every section's claim chains back to an axiom (DESIGN §1 -// open-thread, §7 recursion turned on this document). test fn design_full_argument_form_is_valid() -> Bool { argument_form_is_valid(design_argument) } From ba2f715aa4101eaa88c6a262236d78197b976a25 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 03:14:25 +0000 Subject: [PATCH 08/10] Re-home orphaned intent-linearity draft (main #5579 fallout) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main #5579 (DAG comment-wall) stripped the // comment in src/v2/lens/intent_linearity.dag that carried the bind: root for docs/plans/intent-linearity-design-draft.md, orphaning it in the doc-reachability graph — main has been red on doc_graph_has_no_orphan_docs for 5+ consecutive commits, and every PR merging main inherits it. The intent_linearity lens is still live (only its comments were removed), so the draft is re-homed, not deleted: a markdown link from its reachable sibling docs/plans/self-applying-lenses.md (the intent-linearity registry doc, itself ROADMAP-linked). The draft is literally the DESIGN.md articulation of this PR's own open thread ("model §1's axioms in .dag + enforce the syllogism"), so the link is in-theme. Verified: doc_graph_has_no_orphan_docs / no_dangling_links / universe_nonempty all green by execution. Co-Authored-By: Claude Opus 4.8 --- docs/plans/self-applying-lenses.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/self-applying-lenses.md b/docs/plans/self-applying-lenses.md index fe7cd07059a..f3a0abbfc1b 100644 --- a/docs/plans/self-applying-lenses.md +++ b/docs/plans/self-applying-lenses.md @@ -1,6 +1,6 @@ # Self-applying lenses — detect → generalize → emit → write -**Crux (fractal intent-linearity).** A program's *description length should equal its irreducible +**Crux ([fractal intent-linearity](intent-linearity-design-draft.md)).** A program's *description length should equal its irreducible information content* — the minimal generative template plus the genuinely-distinct data — **recursively at every nesting level**. Equivalently: the intent is 1:1 with its own inputs; the description grows *only* with distinct information, never with repetition. This is the decidable, enforceable shadow of From e2e85d9d4f8cb027ceedcd039c3164aa99c07097 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 03:28:12 +0000 Subject: [PATCH 09/10] Resolve merge: fold main's open-thread pointer into the model + regen DESIGN.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main #5584 hand-edited DESIGN.md's first open thread to add a pointer to the intent-linearity draft. Since DESIGN.md is now generated, fold that exact content change into gunbc.design_document and regenerate (not a hand-merge), so the authority stays the .dag model. Verified: regenerated DESIGN.md content == main's content (whitespace-stripped, the only delta is the pointer); drift gate ExitSuccess; syllogism + completeness witnesses green. main also rooted the orphan draft itself (the new DESIGN.md link + its own link in self-applying-lenses.md), so my earlier redundant line-3 link there is reverted — the orphan is now reachable via the DESIGN.md root. Co-Authored-By: Claude Opus 4.8 --- DESIGN.md | 9 +-------- docs/plans/self-applying-lenses.md | 2 +- dsl/gunbc/design_document.dag | 2 +- 3 files changed, 3 insertions(+), 10 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index 3061d4a8fc5..a083ff6f973 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -78,14 +78,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` ## Open threads -<<<<<<< HEAD -- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) -======= -- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every - claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on - the argument itself; the §7 recursion, with this document as the first target). (operator's next - project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md) ->>>>>>> origin/main +- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md) - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked) - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) diff --git a/docs/plans/self-applying-lenses.md b/docs/plans/self-applying-lenses.md index b8ab02312b1..1a6f6f7b522 100644 --- a/docs/plans/self-applying-lenses.md +++ b/docs/plans/self-applying-lenses.md @@ -1,6 +1,6 @@ # Self-applying lenses — detect → generalize → emit → write -**Crux ([fractal intent-linearity](intent-linearity-design-draft.md)).** A program's *description length should equal its irreducible +**Crux (fractal intent-linearity).** A program's *description length should equal its irreducible information content* — the minimal generative template plus the genuinely-distinct data — **recursively at every nesting level**. Equivalently: the intent is 1:1 with its own inputs; the description grows *only* with distinct information, never with repetition. This is the decidable, enforceable shadow of diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index 9c99ec54abb..0cb6f1c7da2 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -138,7 +138,7 @@ fn open_threads_blocks() -> List { [ h2(text: "Open threads"), ul(items: [ - li(text: "model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project)"), + li(text: "model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)"), li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), From a9a5095415707577b0c7ee167b2ae545291be7b0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 03:45:31 +0000 Subject: [PATCH 10/10] WIP: get design docs into .dag --- dsl/extdeps/languages/markdown.dag | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/dsl/extdeps/languages/markdown.dag b/dsl/extdeps/languages/markdown.dag index 881a55e61b7..399df700626 100644 --- a/dsl/extdeps/languages/markdown.dag +++ b/dsl/extdeps/languages/markdown.dag @@ -149,7 +149,12 @@ fn md_item(marker: String, blocks: List, sp: MarkdownSpellings, d 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)) - _ => concat("\n\n", concat(repeat_string(s: sp.list_indent, n: depth + 1), md_block(block: b, sp: sp))) + 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) } }