DESIGN.md recut: rules kept, rulings typed, half the words

dag/gunbc/contributor_onboarding_path.dag

@@ -750,6 +750,40 @@ fn onboarding_bus_factor_blocks() -> List<MarkdownBlock> {
   ]
 }
 
+// OPERATOR FACTS DESIGN.md USED TO CARRY. They change with tooling rather than with the design, so
+// they live with the walked path that exercises them; DESIGN.md's Building & checks keeps only the
+// CI contract and links here.
+type OnboardingReference {
+  topic: NonEmptyStr
+  fact: NonEmptyStr
+}
+
+data onboarding_reference: List<OnboardingReference> = [
+  OnboardingReference {
+    topic: "Two CLIs" as NonEmptyStr,
+    fact: "`gunbc` is the seed's CLI (`std.compiler_entry` `RetainedHostCliKernel`, host Rust in `v1_compiler.cli_run`), unreachable from a self-emitted binary. The v2 door is `v2.cli.compile_cli` (`std.compiler_entry` `NativeCliDriver`): `.dag` decides parsing, refusals, output and exit, and its rendered main only performs the host reads and writes (`gunbc.source_root_read`)." as NonEmptyStr,
+  },
+  OnboardingReference {
+    topic: "Local checks" as NonEmptyStr,
+    fact: "`cargo fmt --all --check` runs in the generated pre-commit hook (`gunbc.githooks_pre_commit_emit`). `cargo clippy --all-targets -- -D warnings` (`gunbc.repo_self_build` `repo_self_clippy_command`, the only command compiling the integration-test and example targets) and `cargo test --release -p v1-compiler --lib` (`repo_self_test_command`) are local only and block nothing." as NonEmptyStr,
+  },
+  OnboardingReference {
+    topic: "Hooks" as NonEmptyStr,
+    fact: "`git config core.hooksPath .githooks`; the generated hooks converge the rest from `gunbc.repo_local_git_config`, including a merge driver that refuses a both-sides change to a generated path and prints the regeneration recipe." as NonEmptyStr,
+  },
+  OnboardingReference {
+    topic: "Regenerating projections" as NonEmptyStr,
+    fact: "`tools.generated_artifact_gate` `main_wet` rewrites the committed generated artifacts from their authorities, `main` verifies them; `tools.docs_projection_gate` `regen` renders the on-demand ledger views." as NonEmptyStr,
+  },
+]
+
+fn onboarding_reference_blocks() -> List<MarkdownBlock> {
+  [
+    h2(text: "Reference: CLIs, local checks and regeneration"),
+    ul(items: map(onboarding_reference, r => li(text: join(["**", (r.topic as String), ".** ", (r.fact as String)], "")))),
+  ]
+}
+
 fn onboarding_reading_blocks() -> List<MarkdownBlock> {
   [
     h2(text: "Reading DESIGN.md in an order"),
@@ -778,6 +812,7 @@ fn onboarding_document() -> MarkdownDocument {
         onboarding_step_blocks(),
         onboarding_obstacle_blocks(),
         onboarding_bus_factor_blocks(),
+        onboarding_reference_blocks(),
         onboarding_checks_blocks(),
         onboarding_reading_blocks(),
       ],

dag/gunbc/design_ruling.dag

@@ -0,0 +1,150 @@
+module gunbc.design_ruling
+
+import std.types { String }
+import std.decl_ref { DeclarationRef, decl_ref }
+import std.markdown { MarkdownDocument, MarkdownBlock, HeadingBlock, TextInline, H1 }
+import gunbc.plans.md_helpers { h2, p, hr }
+import extdeps.languages.markdown { serialize_markdown_source }
+
+// THE DATED OPERATOR RULINGS DESIGN.md STATES, HELD AS ROWS RATHER THAN NARRATED INLINE.
+//
+// gunbc.design_document carries reasoning; a ruling is a HISTORY fact -- when, in which section, and
+// on whose words -- and it grows by one row per decision while the sections are fixed by section 1.
+// The RULE has exactly one home, the document: a row carries no copy of it, so the two cannot drift.
+// A row's `reference` is its own declaration as a DeclarationRef; the document cites a ruling by
+// passing the row (an import, so a renamed or deleted row fails to resolve), and
+// gunbc.documentary_refs takes its ruling references from design_rulings(), so that one roster is
+// the population the citation resolver, the render witness and the view below all read.
+//
+// One row per ruling, each its own declaration, so a citation names one ruling and two lanes adding
+// two rulings touch two declarations. The on-demand view is
+// `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/design_ruling.dag --function expected_design_rulings_md`;
+// it is not committed, for the same contention reason as the failure-mode ledger.
+
+type DesignRuling {
+  reference: DeclarationRef
+  decided: String
+  section: String
+  provenance: String
+}
+
+data conformance_needs_attention: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "conformance_needs_attention"),
+  decided: "2026-09-06",
+  section: "3b",
+  provenance: "Operator: \"it needs more attention than it has received because it is incredibly important\". The same day the operator named the climb the printing-press direction: derive the touched domains at plan admission, before any worker runs.",
+}
+
+data consumption_interrogated_separately: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "consumption_interrogated_separately"),
+  decided: "2026-09-06",
+  section: "3c",
+  provenance: "Operator: adding dangling modeling is interrogated separately, and the consumption must be understood well.",
+}
+
+data authorization_pattern_is_a_selection: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "authorization_pattern_is_a_selection"),
+  decided: "2026-09-19",
+  section: "3b",
+  provenance: "Added to the conformance domain row on that date; the census gunbc.auth.privileged_effect_census classifies every site by executing the selection.",
+}
+
+data coercion_is_the_implicit_safe_subset: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "coercion_is_the_implicit_safe_subset"),
+  decided: "2026-09-26",
+  section: "4",
+  provenance: "Operator ruling.",
+}
+
+data text_crossings_go_through_the_unfold: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "text_crossings_go_through_the_unfold"),
+  decided: "2026-09-27",
+  section: "4",
+  provenance: "Operator ruling revising XL-0T to option B; Ruling 3 (String is FreeMonoid<Char>) stands. Its first execution falsified the withdrawn leaf-name identity wall.",
+}
+
+data epistemic_humility_is_symmetric: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "epistemic_humility_is_symmetric"),
+  decided: "2026-09-10",
+  section: "4d",
+  provenance: "Operator ruling; receipts gunbc-private #54 (over-assertion) and gunbc#10954 (over-prohibition).",
+}
+
+data chain_re_derivation: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "chain_re_derivation"),
+  decided: "2026-09-15",
+  section: "6b",
+  provenance: "Operator ruling, stated separately because the opposite is the default habit. Specimens: #11401 (resolve rebuilt corpus-wide state per module; repaired upstream with one shared ResolutionContext per native ingest in v2.compiler.compile), #11422 (every ordered Choice is owed one prepared plan, so per-token dispatch was the wrong link, not a slow one), #11444 (the emitter tail-call lowering is_tco_identity_passthrough was itself the earliest unjustified boundary, so the local repair was right).",
+}
+
+data v2_better_than_the_seed: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "v2_better_than_the_seed"),
+  decided: "2026-10-02",
+  section: "7",
+  provenance: "Operator ruling; neither a byte-identical fixed point nor behavioural equivalence to the seed is the goal.",
+}
+
+data instrument_is_a_row_not_a_flag: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "instrument_is_a_row_not_a_flag"),
+  decided: "2026-09-16",
+  section: "Building & checks",
+  provenance: "Operator ruling; `--self-host` was withdrawn in the change that added //gunbc/instruments:self-host.",
+}
+
+data job_roster_closed_to_growth: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "job_roster_closed_to_growth"),
+  decided: "2026-09-04",
+  section: "Building & checks",
+  provenance: "Operator ruling cutting three of seven jobs. On 2026-09-15 the same reasoning cut the push-on-main trigger: the merge queue's required run already proves the landing sha.",
+}
+
+data v1_withdrawn_one_required_job: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "v1_withdrawn_one_required_job"),
+  decided: "2026-10-09",
+  section: "Building & checks",
+  provenance: "Operator ruling (the v1 withdrawal, gunbc#13658 and gunbc#13641). The lanes floor, generated, rust-unit-tests and seed were deleted; the loss is gunbc.rung_drop v1_required_lanes_withdrawn.",
+}
+
+data memory_envelope_is_part_of_the_verdict: DesignRuling = DesignRuling {
+  reference: decl_ref(module_path: "gunbc.design_ruling", decl_name: "memory_envelope_is_part_of_the_verdict"),
+  decided: "2026-10-09",
+  section: "Building & checks",
+  provenance: "Operator ruling issued with the v1 withdrawal.",
+}
+
+fn design_rulings() -> List<DesignRuling> {
+  [
+    job_roster_closed_to_growth,
+    conformance_needs_attention,
+    consumption_interrogated_separately,
+    epistemic_humility_is_symmetric,
+    chain_re_derivation,
+    instrument_is_a_row_not_a_flag,
+    authorization_pattern_is_a_selection,
+    coercion_is_the_implicit_safe_subset,
+    text_crossings_go_through_the_unfold,
+    v2_better_than_the_seed,
+    v1_withdrawn_one_required_job,
+    memory_envelope_is_part_of_the_verdict,
+  ]
+}
+
+fn ruling_blocks(r: DesignRuling) -> List<MarkdownBlock> {
+  [
+    h2(text: concat(r.reference.decl_name as String, " — ", r.decided, " — §", r.section)),
+    p(text: r.provenance),
+  ]
+}
+
+fn expected_design_rulings_md() -> String {
+  serialize_markdown_source(doc: MarkdownDocument {
+    blocks: concat(
+      [
+        HeadingBlock { level: H1, inlines: [TextInline { text: "gunbc — design rulings" }] },
+        p(text: "Generated on demand from `gunbc.design_ruling`. `DESIGN.md` states each rule and cites its row; a row carries only the date, the section and the provenance, never a second copy of the rule."),
+        hr(),
+      ],
+      flat_map(design_rulings(), r => ruling_blocks(r: r)),
+    ),
+  })
+}

dag/gunbc/doc_graph_roots.dag

@@ -549,16 +549,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
     ],
     dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the work this document plans lands and its subject next_spawnable describes shipped behavior rather than a planned change; the row deletes with the document. Registered at subject grain: the systems bound here are the ones whose movement would make this document's purpose false, not every system its prose mentions.") },
   },
-  HandAuthoredDocBind {
-    home: PlanDoc,
-    slug: "s2-v2-self-emit-brief",
-    primary_work: DeclarationRef { module_path: "v2.std.node", decl_name: "Symbol", field: WholeDeclaration },
-    additional_works: [
-      DeclarationRef { module_path: "std.algebra", decl_name: "FreeMonoid", field: WholeDeclaration },
-      DeclarationRef { module_path: "std.optional", decl_name: "Optional", field: WholeDeclaration },
-    ],
-    dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the work this document plans lands and its subject Symbol describes shipped behavior rather than a planned change; the row deletes with the document. Registered at subject grain: the systems bound here are the ones whose movement would make this document's purpose false, not every system its prose mentions.") },
-  },
+
   HandAuthoredDocBind {
     home: PlanDoc,
     slug: "s2-v2-self-emit-direction",

dag/gunbc/documentary_refs.dag

@@ -2,6 +2,7 @@ module gunbc.documentary_refs
 
 import std.types { String }
 import std.decl_ref { DeclarationRef, decl_ref }
+import gunbc.design_ruling { design_rulings }
 
 // THE SYSTEMS A GENERATED DOCUMENT NAMES, CARRIED AS TYPED REFERENCES RATHER THAN SPELLED IN PROSE.
 // gunbc.doc_graph_roots already does exactly this for HAND-AUTHORED documents: HandAuthoredDocBind
@@ -47,5 +48,8 @@ fn documentary_ref_symbol_text(reference: DeclarationRef) -> String {
 }
 
 fn generated_document_declaration_refs() -> List<DeclarationRef> {
-  [v1_maintenance_standing_ref, required_gate_subjects_ref]
+  concat(
+    [v1_maintenance_standing_ref, required_gate_subjects_ref],
+    map(design_rulings(), r => r.reference),
+  )
 }

dag/gunbc/roadmap/roadmap_review_criteria.dag

@@ -3,7 +3,7 @@ module gunbc.roadmap.roadmap_review_criteria
 import std.types { String, Bool, List }
 import std.syllogism { Proposition }
 import std.decl_ref { DeclarationRef, declaration_ref_display_key }
-import gunbc.design_argument { design_propositions, design_rows, DesignRow, PropositionReview, DefectReview, ConformanceReview, PropositionReviewDisposition, ReviewableOnChange, NotReviewableOnChange, ReviewAnswerAlgebra, YesIsADefect, ConformanceThreeValued, ConformanceDomain, conformance_home_list }
+import gunbc.design_argument { design_propositions, design_rows, DesignRow, PropositionReview, DefectReview, ConformanceReview, PropositionReviewDisposition, ReviewableOnChange, NotReviewableOnChange, ReviewAnswerAlgebra, YesIsADefect, ConformanceThreeValued, ConformanceDomain, conformance_domain_homes }
 
 // ONE CRITERION PER DESIGN PROPOSITION, ONE REVIEWER PER CRITERION. A review that asks "is this
 // change good" is one judgment over every concern at once, and its verdict cannot say which concern
@@ -60,7 +60,7 @@ fn conformance_criterion_from_domain(domain: ConformanceDomain, proposition_id:
     question: domain.question,
     tells: domain.tells,
     answer: ConformanceThreeValued,
-    homes: conformance_home_list(h: domain.homes),
+    homes: conformance_domain_homes(d: domain),
   }
 }
 

dag/std/algebra.dag

@@ -906,6 +906,10 @@ fn kernel_carrier_admits_numeral(name: String) -> Bool {
         spelling.text == name && carrier_spelling_row_present(m: spelling.method_surface))))
 }
 
+// Whether distinct keys of a finite map are decidably distinct: consumed by the map-literal
+// duplicate-key check (docs/plans/map-literal-introduction-design.md). The admission is
+// instantiation-blind at this rung -- an opaque brand or a type parameter admits unjudged -- and its
+// next-rung trigger is instantiation-grain admission (v1 infer equality_admission_wall_note).
 fn algebra_profile_equality_extensional(profile: AlgebraProfile) -> Bool {
   match algebra_profile_support(profile: profile) {
     FiniteSupport => true

dag/test/claim/documentary_refs_witness_test.dag

@@ -3,16 +3,15 @@ module test.claim.documentary_refs_witness
 import std.types { Bool, String }
 import std.decl_ref { DeclarationRef, WholeDeclaration }
 import v2.lens.module_graph { ModuleDeclarationFact }
-import v2.std.decl_index { DeclFact, FnItem, TypeItem }
+import v2.std.decl_index { DeclFact, FnItem, TypeItem, decl_facts_at }
 import v2.lens.enforcement.receipts { enforcement_red_probe_body_leaf }
 import v2.std.decl_ref_resolution { cited_declaration_ref_refusal_count }
 import gunbc.documentary_refs {
   documentary_ref_symbol_text,
   generated_document_declaration_refs,
-  v1_maintenance_standing_ref,
-  required_gate_subjects_ref,
 }
 import gunbc.design_document { expected_design_md }
+import gunbc.design_ruling { design_rulings }
 
 // THE PERTURBATIONS ARE THE POINT, AND EACH RUNS AGAINST THE SAME RESOLVER PRODUCTION USES.
 // cited_declaration_ref_refusal_count is v2.std.decl_ref_resolution's own counter -- the one the
@@ -29,6 +28,7 @@ fn fixture_modules() -> List<ModuleDeclarationFact> {
     ModuleDeclarationFact { module: "gunbc.roadmap_authority", path: "dag/gunbc/roadmap/roadmap_authority.dag" },
     ModuleDeclarationFact { module: "gunbc.v1_maintenance_standing", path: "dag/gunbc/v1/v1_maintenance_standing.dag" },
     ModuleDeclarationFact { module: "gunbc.emitted_subject_build_gate", path: "dag/gunbc/emitted_subject_build_gate.dag" },
+    ModuleDeclarationFact { module: "gunbc.design_ruling", path: "dag/gunbc/design_ruling.dag" },
   ]
 }
 
@@ -46,7 +46,7 @@ fn fixture_fact(qualified_name: String, name: String, path: String) -> DeclFact
 // generated_document_declaration_refs(). This is the
 // control that proves the refusals below are caused by the perturbation rather than by a fixture
 // that never resolved anything.
-fn intact_facts() -> List<DeclFact> {
+fn fixed_facts() -> List<DeclFact> {
   [
     fixture_fact(
       qualified_name: "gunbc.v1_maintenance_standing.v1_seed_standing",
@@ -61,6 +61,20 @@ fn intact_facts() -> List<DeclFact> {
   ]
 }
 
+// The ruling rows' facts come from the same roster the document's references do, so a ruling
+// added to gunbc.design_ruling design_rulings() is resolved and render-checked with no edit here.
+fn ruling_facts() -> List<DeclFact> {
+  map(design_rulings(), r => fixture_fact(
+    qualified_name: concat("gunbc.design_ruling.", r.reference.decl_name as String),
+    name: r.reference.decl_name as String,
+    path: "dag/gunbc/design_ruling.dag",
+  ))
+}
+
+fn intact_facts() -> List<DeclFact> {
+  concat(fixed_facts(), ruling_facts())
+}
+
 fn refusals_against(facts: List<DeclFact>) -> Int {
   cited_declaration_ref_refusal_count(
     refs: generated_document_declaration_refs(),
@@ -118,12 +132,23 @@ test fn documentary_refs_ambiguous_system_refuses() -> Bool {
 // typed reference sitting beside a paragraph that independently spells the same name is two
 // representations of one fact -- the rename would move the row and leave the sentence, and the
 // enrolled population would resolve while the document lied. This claim asserts the rendered symbol
-// text of each row appears in the generated document, so the row and the printed name cannot
-// diverge.
+// text of EVERY row appears in the generated document, so the row and the printed name cannot
+// diverge, and a row no paragraph renders is a red rather than an orphan.
 
 test fn documentary_refs_generated_document_renders_the_rows() -> Bool {
   let md = expected_design_md()
-  string_contains(s: md, pattern: documentary_ref_symbol_text(reference: v1_maintenance_standing_ref))
-    && string_contains(s: md, pattern: documentary_ref_symbol_text(reference: required_gate_subjects_ref))
+  all(generated_document_declaration_refs(), r => string_contains(s: md, pattern: documentary_ref_symbol_text(reference: r)))
 }
 
+
+// THE INHABITANCE HALF. The fixture above derives the ruling facts from the rows' own references, so
+// it proves the resolver's behaviour, not that a row's reference names the row: a row whose
+// decl_name drifted from its declaration would plant its own matching fact and stay green. This
+// claim reads the live declaration pool, keyed, so each ruling reference must name exactly one real
+// declaration.
+test fn documentary_refs_ruling_references_name_live_declarations() -> Bool {
+  all(design_rulings(), r => length(xs: decl_facts_at(
+    pool_roots: ["dag"],
+    qualified_name: concat("gunbc.design_ruling.", r.reference.decl_name as String),
+  )) == 1)
+}