feat(spec): backfill Export terminology + diagnostics/legality/pipeline (ADR-0009/0010)

Lift the business decisions the MVP made into the Lean master, per constitution
rule 5. lake build green (20 jobs), no sorry.

- Artifact.lean: `inductive Artifact | singleFile | fileTree` — product shape is
  part of a target's value (ADR-0009); it determines the assemble/reduce step.
- Render.lean reworked target-centric (ADR-0009, amends ADR-0005's matrix):
  `TargetSpec` carries `artifact` + a per-kind `renders` map (field visibility
  lives in this map); `RenderConfig.spec : TargetId → Option TargetSpec`; `covers`
  rewritten (target must exist AND its map covers the kind) — semantics continuous
  with ADR-0005 so renderIgnored still typechecks. `BuildStepForm` (declarative |
  shell) is a structural anchor for the build form (shell hatch = ADR-0005's
  medium-only category b) without replicating the schema.
- Diagnostic.lean extended: `DiagKind` (7 classes) + `DiagKind.severity` (six
  error, renderIgnored warning); `Oracle` makes external-facility verdicts
  (compiles/refsResolve/dataConforms/contentFilesPresent) an explicit
  implementation boundary; `Legal` = no error-level diagnostic (backfills
  ADR-0005's deferred full-legality), with renderIgnored deliberately excluded
  (it's a warning).
- Pipeline.lean: the 5 phases (load→structural→schema→compile→coverage) as
  structure — order + the compile gate (compile runs only on zero prior errors) +
  load halts the pipeline. Algorithms stay out of Lean (depth ceiling).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

spec/Spec/Courseware/Diagnostic.lean

@@ -2,44 +2,143 @@ import Spec.Courseware.Lesson
 import Spec.Courseware.Render
 
 /-!
-# Diagnostic —— checker 诊断(种子)
+# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
 
-产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀。它对 lesson 提诊断,
-每条诊断有**严重级别**。本模块固定级别类型,并落第一条规则——ADR-0005 钉死的"缺
-渲染 ⇒ warning"。完整的"合法 lesson"判定仍 OPEN,本模块只是它的起点。
+产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀(ADR-0010)。它对 lesson
+提诊断,每条诊断有**分类**(`DiagKind`)与**严重级别**(`Severity`)。本模块:
+
+1. 钉级别类型(二分,ADR-0005)。
+2. 钉 7 类诊断各自的含义与级别(ADR-0010),并把"**合法 lesson = 无 error 级诊断**"
+   建成判定——这是 ADR-0005 deferred 的"完整合法判定"的回填。
+3. 对**模型外设施**型诊断(typst 能否编过、引用悬否、数据合 schema 否),用**抽象谓词 +
+   显式实现边界**表示:契约说"存在这样一条诊断、它什么意思、什么级别",但其**真值由
+   实现(checker)提供**,不在 Lean 内计算——保持契约诚实(不内嵌 typst 编译器)。
 -/
 
 namespace Spec.Courseware
 
 /--
-诊断的严重级别(`PINNED` 二分, ADR-0005 区分 warning 与阻断)。
+诊断的严重级别(`PINNED` 二分, ADR-0005)。
 
-`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。
-ADR-0005 已用到这个区分:缺渲染是 warning 而非 error。更细的级别(info/hint)未
-决策,故只二分。
+`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。更细的
+级别(info/hint)未决策,故只二分。
 -/
 inductive Severity where
   | warning
   | error
 
+/--
+诊断的**分类**(`PINNED` 7 类, ADR-0010)。每类含义见下;级别见 `DiagKind.severity`。
+
+按"谁来判定"分三层(ADR-0010 的边界):
+- **结构型**(模型自身可判):`partPathMissing` / `unknownKind`。
+- **schema / 外部设施型**(判定靠实现 oracle):`missingContentFile` / `schemaViolation`
+  / `danglingReference` / `typstCompile`。
+- **语义型**(coverage 规则):`renderIgnored`。
+-/
+inductive DiagKind where
+  /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
+  | partPathMissing
+  /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/
+  | unknownKind
+  /-- kind schema 要求的某 `content` 字段缺对应 `<field>.typ`。结构/schema 型。 -/
+  | missingContentFile
+  /-- 实例数据不合其 kind 的 JSON Schema(标量类型错/缺必填/多余键);亦作 manifest/
+      element.toml 畸形的兜底。schema / 外部设施型。 -/
+  | schemaViolation
+  /-- 引用不解析:越界的相对 import,或悬空的交叉引用。外部设施型。 -/
+  | danglingReference
+  /-- 拼装出的 typst 源编译失败(语法错、`@ref` 未解析…)。外部设施型。 -/
+  | typstCompile
+  /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被该 target 忽略。语义型。 -/
+  | renderIgnored
+
+/--
+每类诊断的**严重级别**(`PINNED`, ADR-0010)。
+
+六类为 `error`(阻断);**唯 `renderIgnored` 为 `warning`**——即 ADR-0005 的种子规则
+"缺渲染 ⇒ warning,不阻断导出"。把级别钉成一个全函数,使"哪类阻断、哪类不阻断"成为
+契约里可引用、可对齐的事实(实现侧 `DiagCode` 的级别据此对齐)。
+-/
+def DiagKind.severity : DiagKind → Severity
+  | .partPathMissing   => .error
+  | .unknownKind       => .error
+  | .missingContentFile => .error
+  | .schemaViolation   => .error
+  | .danglingReference => .error
+  | .typstCompile      => .error
+  | .renderIgnored     => .warning
+
+/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。
+
+保留为具名常量,使"它是 warning 不是 error"可被实现侧 grep 对齐(实现里同名常量
+`RENDER_IGNORED_SEVERITY` 引用本定义)。等价于 `DiagKind.severity .renderIgnored`。 -/
+def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity
+
 variable (P : Primitives)
 
 /--
-**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005)。
+**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005/0009)。
 
-成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则。这条对应 checker 的第一条
-诊断;其级别由下面的 `renderIgnoredSeverity` 钉死为 **warning**。
+成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则(`covers` 为假,见 `Render`)。这条
+是 checker 的**语义型**诊断,级别由 `renderIgnoredSeverity` 钉为 warning。`covers` 已随
+ADR-0009 下沉到 target 的 build 规格,但本判定式不变。
 -/
 def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
   ∃ e ∈ l, ¬ c.covers e.kind t
 
-/--
-缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005,**非 error**)。
+/-!
+## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
 
-ADR-0005 明确:某 (kind, target) 无渲染规则时,checker 报 warning 说该 element 在
-该 target 被忽略,**不阻断导出**。把这条决策固定为一个常量,使"它是 warning 不是
-error"成为契约里可被引用、可被对齐的事实,而不是散落在 prose 里的口头约定。
+`typstCompile` / `danglingReference` / `schemaViolation`(的 schema-合规面)断言的是
+**模型自身无法判定**的事实——要跑 typst 编译器、要跑 schema 校验器。契约因此把它们建成
+**抽象谓词**,真值由一个**实现提供的 oracle** 给出。Lean 只说"这条诊断存在、什么意思、
+什么级别",**不**在 Lean 内计算其真假。
+
+下面用一个 `Oracle` 结构收口这些实现侧判定。它**不是**要在 Lean 里实现 checker,而是
+把"这些事实来自模型外"这件事显式化、类型化:谁想谈论一节 lesson 合不合法,就得先有一个
+oracle 提供这些外部判定。
 -/
-def renderIgnoredSeverity : Severity := .warning
+
+/--
+**实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。
+
+收口那些"模型外设施"才能回答的判定。每个字段是一个谓词,**真值由实现(checker)提供**:
+
+- `compiles` —— 该 lesson 在 target `t` 下拼装出的 typst 源能否编译通过(否 ⇒ `typstCompile`)。
+- `refsResolve` —— 该 lesson 的引用(相对 import / 交叉引用)是否全部解析(否 ⇒ `danglingReference`)。
+- `dataConforms` —— 每个 element 的数据是否合其 kind schema(否 ⇒ `schemaViolation`)。
+- `contentFilesPresent` —— schema 要求的 `content` 文件是否齐备(否 ⇒ `missingContentFile`)。
+
+把它们作为参数,正是"显式实现边界":契约能据此**定义**合法性,却不假装自己能算出这些
+外部事实。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。
+-/
+structure Oracle (l : Lesson P) (c : RenderConfig P) where
+  /-- target `t` 下拼装源可编译。 -/
+  compiles : P.TargetId → Prop
+  /-- 引用全部解析。 -/
+  refsResolve : Prop
+  /-- 每个 element 数据合 schema。 -/
+  dataConforms : Prop
+  /-- schema 要求的 content 文件齐备。 -/
+  contentFilesPresent : Prop
+
+/--
+**合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。
+
+一节 lesson 合法 ⟺ 检查管线产出**零条 error 级诊断**。warning(如 `renderIgnored`)
+不影响合法性——带 warning 的 lesson 仍合法、仍可(有损)导出。
+
+这里把"无 error 级诊断"展开为:模型外设施判定(经 `Oracle`)全部为真,**且**每个声明的
+target 都编译通过。结构型诊断(part 路径、未知 kind、kind 不一致)由 `cph-model` 在加载
+期判定;能走到这一步谈合法性,意味着已加载成功,故此处聚焦 schema/外部设施层。注意
+`renderIgnored` 是 warning,**不**进合法性合取——这正是 ADR-0005 种子规则的体现。
+
+`targets` 是该工程文件声明的 target 列表(`RenderConfig.spec t` 非 `none` 者);为保持
+本层抽象、不绑定 `TargetId` 的可枚举性,这里用"对所有满足前提的 t"的全称式表达。
+-/
+def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
+  o.refsResolve ∧ o.dataConforms ∧ o.contentFilesPresent ∧
+    (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)
 
 end Spec.Courseware