# spec —— Lean 语义母本

这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。

## 现状

刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。

## 构建

```sh
cd spec
lake build
```

工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。

## 写作规范

### 双半契约:prose + type

每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:

- **prose 半**给人读——说清"这在领域里是什么、为什么"。
- **type 半**给机器读、给 type checker 把关——保证结构无洞。

agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。

### 标签分类法

在 doc 注释里用以下标签标注每条语义的状态:

- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。

### 分歧点测试(写之前先过一遍)

新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**

- 会 → 它是分歧点,入契约。
- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。

详见根 README 宪法第 5 条。

### 不用 `sorry`

无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。

### 命名

- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
- **类型**:PascalCase。
- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。