feat(hub): 事件去重(A-4) + 审计写入路径(A-8)

A-4 FeishuEventReceipt:
- 新增 FeishuEventReceipt 表(eventId @unique),lark ws 至少一次投递的幂等兜底
- MessageReceiveEvent 加 header.event_id 字段
- trigger 入口查重:已存在的 event_id → 跳过(不建第二次 run)
- resetDb 加入 FeishuEventReceipt

A-8 审计写入:
- AuditEntry 加 projectId(权限拒绝/slash 命令等无 run 的审计点可定位)
- 新建 src/audit.ts:writeAudit(prisma, entry) best-effort 写入(吞错,不阻断 trigger)
- trigger 五个审计点:trigger.denied / trigger.role_denied / run.created / run.lock_race / run.finished / run.failed
- 新增 audit unit 测试(3) + trigger 集成测试(去重 + 审计,2)

59 tests 全过。

.gitignore

@@ -11,5 +11,8 @@
 # regenerable, not for VCS. The embedded engine mounts cph-render directly.
 render/vendor/local-packages/
 
+# Node (hub/ TS workspace and any future JS package)
+node_modules/
+
 # OS / editor
 .DS_Store

README.md

@@ -1,74 +1,74 @@
 # curriculum-project-hub
 
-教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件;
-LLM assistant 协助编辑它;一个 rule-based checker 校验其合法性并给出有用的诊断。
+教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
 
-LLM 提效,但判不了一节课合不合法(它不能真去跑 typst、不能可靠地断言数据合不合
-schema);checker 真跑工具、给确定性诊断,补上这块。两者一起才是完整闭环。目标是把教研
-从一次性的文档,变成可累积、可校验、可复用的资产。
+这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
 
-这是一个 monorepo。组织方式本身就表达了一条原则:`spec/` 是上游的语义母本,其余部件是
-向它对齐的实现。
+## 安装 `cph` 命令行
 
-## 安装 `cph`
-
-从源码安装(本仓库根目录):
+当前版本 **0.0.2**。从源码安装(本仓库根目录):
 
 ```sh
 cargo install --path crates/cph-cli --locked
 ```
 
-`render` 包已嵌入二进制,装好后无需任何环境变量、不依赖源码树即可用。开发时可设
-`CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
+`render` 包已嵌入二进制(build.rs 编译期拷入 + `include_dir!`),所以装好后**无需任何环境变量、不依赖源码树**即可用。渲染包按版本解压到 per-user cache(`~/.cache/cph/render-<version>/` 或 macOS `~/Library/Caches/cph/...`);开发时可设 `CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
 
 ```sh
-cph check <工程目录>                              # 校验合法性
+cph --version          # cph 0.0.2
+cph check <工程目录>     # 校验合法性(7 类诊断)
 cph build <工程目录> --target student -o build/student.pdf   # 渲讲义 PDF
-cph completions zsh > ~/.zfunc/_cph               # shell 补全(可选)
 ```
 
-工程文件根放一个 `.cph-version` 文件,声明它面向的 cph 版本;`cph` 加载时比对自身版本,
-不相容则拒绝(版本契约,ADR-0016)。
+**版本契约(ADR-0016):** 教研工程文件根放一个 `.cph-version` 文件,内容为它面向的 cph 版本(如 `0.0.2`)。`cph` 加载时比对自身版本,不相容则报 `E-CPH-VERSION` error 并拒绝(当前判定为版本完全相等;后续可放宽为 semver 区间,只改一处谓词)。`examples/` 与本仓 fixture 已带该文件作为迁移起点;缺文件的工程暂时跳过此检查(OPEN)。
+
+Shell 补全(可选):
+
+```sh
+cph completions zsh > ~/.zfunc/_cph        # 或 bash/fish/powershell/elvish
+```
 
 ## 仓库布局
 
-`spec/` 是 Lean 语义母本(自包含 Lean 工程,见 `spec/README.md`);`crates/` 是实现
-(rule-based checker,向 spec 对齐,见 `crates/README.md`);`render/` 是 typst 渲染包;
-`examples/` 是样例工程文件;`docs/adr/` 是架构决策记录,被 spec 引用。
+```
+README.md          ← 本文件:总览 + 宪法(下面 5 条)
+CLAUDE.md          ← 全局 agent 操作手册(管整个 repo)
+docs/adr/          ← 系统级架构决策记录(跨部件,被 spec 契约引用)
+spec/              ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
+Cargo.toml         ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
+crates/            ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
+  cph-diag / cph-model / cph-schema / cph-typst   ← 可复用基础(模型/校验/typst 引擎)
+  cph-check / cph-cli                             ← checker 本体 + `cph` 命令行
+render/            ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
+examples/          ← 样例工程文件(如 TH-141),流水线的真实输入
+(hub/ exporter/ …) ← 将来的其他部件,平级于 spec/。尚未创建
+```
 
-`spec/` 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。实现部件共用一个
-仓库根的 cargo workspace,使基础 crate 能被未来部件复用。
+`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
+实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被
+未来部件(如 exporter)复用,而非各自重造。
 
 ## 宪法
 
 这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
 
-1. **角色——Lean 是研发侧的上游参照。**
-   `spec/` 用 Lean 写,是开发者和 coding assistant 共用的 spec 工具,用来沉淀产品各部件
-   的语义。它不进产品运行时——运行时那个 checker 用什么技术实现还没定,但它的语义先在
-   `spec/` 里固定下来。
+1. **角色 —— Lean 是研发侧的上游参照。**
+   `spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
 
-2. **对齐机制——Lean 只做上游参照。**
-   不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐
-   spec,靠开发者 review 和 agent 巡逻 diff 这个人肉环节承载。(CI 里的 spec check 只验
-   spec 自身能否 type-check,即契约内部良构,不是 spec↔实现对齐检查。)
+2. **对齐机制 —— Lean 只做上游参照。**
+   不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
+   (CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
 
-3. **资产性——由核对纪律承载,无机器兜底。**
-   这份仓库给的是精确、自洽、机器验过内部良构的语义共识,不是实现正确性的保证。spec 与
-   实现是否一致,没有自动闸门,要靠人工或 coding assistant 不定期(或每次改动后)核对;
-   坚持核对,它就是有用的参照,否则只会变成过期的文档。
+3. **资产性 —— 由 review 纪律承载,无机器兜底。**
+   这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
 
-4. **形态——它是人机共识的契约。**
-   契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——
-   type checker 会逼这份契约在结构上无洞。
+4. **形态 —— 它是人机共识的契约。**
+   契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
 
-5. **深度判据——只收录分歧点。**
-   一条语义该不该写进 Lean,取决于一句话:不写明,开发者与 agent 会不会各自做出不同
-   假设?会,就进契约;显然的东西、纯基础设施、普通 CRUD 字段,不进(写进去只稀释信噪比、
-   增加维护面)。深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量。
-   进了之后钉到多细,见 `spec/README.md` 的取舍判据。
+5. **深度判据 —— 只收录分歧点。**
+   一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
+   深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
 
 ## CI
 
-每次 push / PR 在 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过。这是良构 gate,
-见宪法第 2 条。
+`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。

docs/adr/0017-agent-session-is-provider-bound.md

@@ -0,0 +1,50 @@
+# ADR 0017: AgentSession Is Provider-Bound
+
+## Status
+
+Accepted.
+
+## Context
+
+ADR-0002 says a long-lived `AgentSession` can be reused by many runs, but never
+addressed the provider/model dimension. The agent layer is provider-agnostic
+(ADR-0001..0003 never required Claude specifically; the `@Claude` trigger name
+is a product brand, not a provider commitment). In practice the Hub routes
+model calls through an OpenAI-compatible client (e.g. OpenRouter), so a run may
+target different models — and the motivation for multi-model is **role-based
+routing**: drafting, reviewing, and triage suit different models.
+
+That raises the question ADR-0002 left open: when a teacher switches model
+mid-project, does the `AgentSession` carry live context across the switch, or
+is it bound to a single provider/model?
+
+## Decision
+
+An `AgentSession` is **provider/model-bound**. A model or provider switch
+starts a new `AgentSession`. The `AgentSession` does not carry live context
+across a switch.
+
+Cross-session continuity is not the session's job — it is carried by ADR-0003's
+project memory and anchors, which the Hub reads on demand when seeding a new
+run. This keeps B consistent with ADR-0003 ("the Hub avoids becoming a full
+chat history store"): session continuity and history continuity are the same
+mechanism, both via memory/anchors, never via a live cross-provider session.
+
+Per-run model selection (the run carries its model) is the switching point.
+
+## Consequences
+
+- Switching model mid-project = new session; the new run seeds from project
+  memory/anchors (ADR-0003), not the prior session's live context.
+- The agent layer is provider-agnostic: model calls go through an
+  OpenAI-compatible client, and the tool-calling loop is delegated to the
+  Vercel AI SDK (`generateText` + `tool`). The provider seam is the SDK's
+  `LanguageModel` interface, not a hand-rolled loop; swapping provider is
+  swapping the `createOpenAICompatible` factory, not rewriting the loop. No
+  hard dependency on a single-vendor agent SDK.
+- Role-based model routing (different run kinds default to different models) is
+  a product/admin configuration concern, not a spec invariant.
+- "AgentSession reused by many runs" (ADR-0002) holds *within* one
+  provider/model; it does not span a switch.
+- The `@Claude` trigger name remains the product mention brand regardless of the
+  backing model.

hub/.env.example

@@ -0,0 +1,23 @@
+# Hub runtime configuration. Copy to .env and fill in.
+
+# PostgreSQL connection string. Used by Prisma and the Hub server.
+DATABASE_URL="postgresql://paradigm:paradigm@127.0.0.1:5432/paradigm"
+
+# OpenRouter (or any OpenAI-compatible) API key + base URL.
+# The Hub's agent layer is provider-agnostic (ADR-0017); this points the
+# OpenAI-compatible client at OpenRouter by default.
+OPENROUTER_API_KEY=""
+# Optional: override the base URL (e.g. direct vendor API, local gateway).
+# OPENROUTER_BASE_URL="https://openrouter.ai/api/v1"
+
+# Hub server port. Defaults to 8788.
+PORT=8788
+
+# Feishu (lark) bot credentials. The bot receives @mentions in project groups.
+FEISHU_APP_ID=""
+FEISHU_APP_SECRET=""
+FEISHU_BOT_OPEN_ID=""
+
+# Path to the `cph` binary (the Courseware-side checker, ADR-0016).
+# Defaults to `cph` on PATH if unset.
+# CPH_BIN="/usr/local/bin/cph"

hub/.gitignore

@@ -0,0 +1,6 @@
+node_modules/
+dist/
+*.log
+.env
+.env.*
+!.env.example

hub/deploy/cph-hub.service

@@ -0,0 +1,21 @@
+[Unit]
+Description=Curriculum Project Hub (Feishu agent + cph)
+After=network-online.target postgresql.service
+Wants=network-online.target
+
+[Service]
+Type=simple
+User=__SERVICE_USER__
+WorkingDirectory=__HUB_DIR__
+EnvironmentFile=__ENV_FILE__
+# Run prisma migrations before each start, then launch the Hub.
+ExecStartPre=__NODE_BIN__ __HUB_DIR__/node_modules/prisma/build/index.js migrate deploy --schema __HUB_DIR__/prisma/schema.prisma
+ExecStart=__NODE_BIN__ __HUB_DIR__/dist/server.js
+Restart=on-failure
+RestartSec=5
+# Graceful shutdown: lark ws close + in-flight runs.
+KillSignal=SIGTERM
+TimeoutStopSec=30
+
+[Install]
+WantedBy=multi-user.target

hub/deploy/deploy_platform.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# Deploy the Hub to a host: rsync the repo, install deps, build, restart service.
+#
+# Configure these env vars (e.g. in CI secrets):
+#   PLATFORM_DEPLOY_HOST     required
+#   PLATFORM_DEPLOY_SSH_KEY  required (private key for the deploy user)
+#   PLATFORM_DEPLOY_USER     optional, defaults to deploy
+#   PLATFORM_DEPLOY_PORT     optional, defaults to 22
+#   PLATFORM_DEPLOY_BASE     optional, defaults to /srv/curriculum-project-hub
+#
+# The target host must have Node.js, npm, rsync, PostgreSQL, systemd, and a
+# writable $PLATFORM_DEPLOY_BASE. Use a dedicated `deploy` user that has
+# passwordless sudo for:
+#   systemctl restart cph-hub.service
+#   systemctl is-active --quiet cph-hub.service
+set -euo pipefail
+
+HOST="${PLATFORM_DEPLOY_HOST:?PLATFORM_DEPLOY_HOST required}"
+SSH_KEY="${PLATFORM_DEPLOY_SSH_KEY:?PLATFORM_DEPLOY_SSH_KEY required}"
+DEPLOY_USER="${PLATFORM_DEPLOY_USER:-deploy}"
+PORT="${PLATFORM_DEPLOY_PORT:-22}"
+BASE="${PLATFORM_DEPLOY_BASE:-/srv/curriculum-project-hub}"
+HUB_DIR="$BASE/hub"
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)"
+
+SSH_OPTS=(-i "$SSH_KEY" -p "$PORT" -o StrictHostKeyChecking=accept-new)
+
+# 1. Rsync the hub/ directory (exclude node_modules/dist, they rebuild on host).
+rsync -az --delete \
+  --exclude node_modules --exclude dist --exclude .env \
+  -e "ssh ${SSH_OPTS[*]}" \
+  "$REPO_ROOT/hub/" "$DEPLOY_USER@$HOST:$HUB_DIR/"
+
+# 2. Install deps + build on the host.
+ssh "${SSH_OPTS[@]}" "$DEPLOY_USER@$HOST" "cd '$HUB_DIR' && npm ci && npm run build"
+
+# 3. Ensure the service is installed (idempotent), then restart.
+ssh "${SSH_OPTS[@]}" "$DEPLOY_USER@$HOST" "
+  BASE='$BASE' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/install_service.sh' || true
+  sudo systemctl restart cph-hub.service
+  sleep 2
+  sudo systemctl is-active --quiet cph-hub.service || { echo 'service failed to start'; exit 1; }
+  curl -sf http://127.0.0.1:8788/api/healthz || { echo 'healthz failed'; exit 1; }
+"
+
+echo "Deployed cph-hub to $HOST ($HUB_DIR)"

hub/deploy/install_service.sh

@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# Install the cph-hub systemd service on a host. Idempotent.
+#
+# Prerequisites already on the host: Node.js, npm, PostgreSQL, systemd.
+# The Hub repo is expected at HUB_DIR (default /srv/curriculum-project-hub/hub)
+# with `npm ci` + `npm run build` already run by deploy_platform.sh.
+#
+# Usage:
+#   sudo BASE=/srv/curriculum-project-hub bash deploy/install_service.sh
+set -euo pipefail
+
+BASE="${BASE:-/srv/curriculum-project-hub}"
+HUB_DIR="${HUB_DIR:-$BASE/hub}"
+SERVICE_USER="${SERVICE_USER:-root}"
+HOST="${HOST:-127.0.0.1}"
+PORT="${PORT:-8788}"
+ENV_FILE="${ENV_FILE:-$BASE/.secrets/platform.env}"
+NODE_BIN="${NODE_BIN:-$(command -v node || true)}"
+
+if [ -z "$NODE_BIN" ]; then
+  echo "node must be on PATH, or set NODE_BIN." >&2
+  exit 1
+fi
+if [ ! -d "$HUB_DIR" ]; then
+  echo "HUB_DIR not found: $HUB_DIR (set HUB_DIR or clone the repo there)." >&2
+  exit 1
+fi
+if [ ! -f "$HUB_DIR/dist/server.js" ]; then
+  echo "build missing: run 'npm ci && npm run build' in $HUB_DIR first." >&2
+  exit 1
+fi
+
+# Seed the env file if absent. Secrets stay on the server, never in the repo.
+if [ ! -f "$ENV_FILE" ]; then
+  install -d -m 0700 "$(dirname "$ENV_FILE")"
+  cat >"$ENV_FILE" <<EOF
+NODE_ENV=production
+DATABASE_URL=postgresql://paradigm:change-me@127.0.0.1:5432/paradigm
+OPENROUTER_API_KEY=
+FEISHU_APP_ID=
+FEISHU_APP_SECRET=
+FEISHU_BOT_OPEN_ID=
+PORT=$PORT
+HOST=$HOST
+EOF
+  echo "Seeded $ENV_FILE — edit it to fill in OPENROUTER_API_KEY and Feishu creds, then re-run."
+  exit 0
+fi
+
+# Render the unit with concrete paths.
+UNIT=/etc/systemd/system/cph-hub.service
+sed \
+  -e "s|__SERVICE_USER__|$SERVICE_USER|g" \
+  -e "s|__HUB_DIR__|$HUB_DIR|g" \
+  -e "s|__ENV_FILE__|$ENV_FILE|g" \
+  -e "s|__NODE_BIN__|$NODE_BIN|g" \
+  "$HUB_DIR/deploy/cph-hub.service" >"$UNIT"
+
+systemctl daemon-reload
+systemctl enable cph-hub.service
+echo "Installed cph-hub.service. Start with: systemctl start cph-hub"
+echo "Check health: curl http://127.0.0.1:$PORT/api/healthz"

hub/package.json

@@ -0,0 +1,38 @@
+{
+  "name": "@paradigm/hub",
+  "version": "0.0.0",
+  "private": true,
+  "type": "module",
+  "engines": {
+    "node": ">=20"
+  },
+  "dependencies": {
+    "@ai-sdk/openai-compatible": "^3.0.5",
+    "@fastify/cookie": "^11.0.2",
+    "@larksuiteoapi/node-sdk": "^1.66.1",
+    "@prisma/client": "^6.19.3",
+    "ai": "^7.0.16",
+    "dotenv": "^17.4.2",
+    "fastify": "^5.8.5",
+    "zod": "^4.4.3"
+  },
+  "devDependencies": {
+    "prisma": "^6.19.3",
+    "tsx": "^4.19.0",
+    "typescript": "^5.7.0",
+    "vitest": "^4.1.10"
+  },
+  "description": "Curriculum Project Hub — Feishu-group collaboration + provider-agnostic agent runtime. Aligns to spec/System (ADR-0001..0004, 0017).",
+  "scripts": {
+    "dev": "tsx watch src/server.ts",
+    "build": "tsc -p tsconfig.json",
+    "start": "node dist/server.js",
+    "check": "tsc -p tsconfig.json --noEmit",
+    "prisma:generate": "prisma generate --schema prisma/schema.prisma",
+    "prisma:validate": "DATABASE_URL=${DATABASE_URL:-postgresql://stub:stub@127.0.0.1:5432/stub} prisma validate --schema prisma/schema.prisma",
+    "prisma:migrate": "DATABASE_URL=${DATABASE_URL:-postgresql://paradigm:paradigm@127.0.0.1:5432/paradigm} prisma migrate deploy --schema prisma/schema.prisma",
+    "deploy": "bash deploy/deploy_platform.sh",
+    "test": "vitest run",
+    "test:watch": "vitest"
+  }
+}

hub/prisma/migrations/20260707072854_init/migration.sql

@@ -0,0 +1,271 @@
+-- CreateEnum
+CREATE TYPE "PlatformRole" AS ENUM ('ADMIN', 'TEACHER');
+
+-- CreateEnum
+CREATE TYPE "AgentRunStatus" AS ENUM ('ACTIVE', 'WAITING_FOR_USER', 'COMPLETED', 'FAILED', 'TIMED_OUT', 'CANCELED');
+
+-- CreateEnum
+CREATE TYPE "AgentEntrypoint" AS ENUM ('FEISHU', 'WEB', 'CLI');
+
+-- CreateEnum
+CREATE TYPE "PermissionRole" AS ENUM ('READ', 'EDIT', 'MANAGE');
+
+-- CreateEnum
+CREATE TYPE "PermissionResourceType" AS ENUM ('PROJECT', 'ARTIFACT', 'PROJECT_GROUP');
+
+-- CreateTable
+CREATE TABLE "User" (
+    "id" TEXT NOT NULL,
+    "feishuOpenId" TEXT NOT NULL,
+    "displayName" TEXT NOT NULL,
+    "avatarUrl" TEXT,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+
+    CONSTRAINT "User_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "PlatformRoleAssignment" (
+    "id" TEXT NOT NULL,
+    "userId" TEXT NOT NULL,
+    "role" "PlatformRole" NOT NULL,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "revokedAt" TIMESTAMP(3),
+
+    CONSTRAINT "PlatformRoleAssignment_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "Project" (
+    "id" TEXT NOT NULL,
+    "name" TEXT NOT NULL,
+    "workspaceDir" TEXT NOT NULL,
+    "createdByUserId" TEXT,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+    "archivedAt" TIMESTAMP(3),
+
+    CONSTRAINT "Project_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "ProjectGroupBinding" (
+    "id" TEXT NOT NULL,
+    "projectId" TEXT NOT NULL,
+    "chatId" TEXT NOT NULL,
+    "createdByUserId" TEXT,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+
+    CONSTRAINT "ProjectGroupBinding_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "AgentSession" (
+    "id" TEXT NOT NULL,
+    "projectId" TEXT NOT NULL,
+    "provider" TEXT NOT NULL,
+    "model" TEXT NOT NULL,
+    "title" TEXT,
+    "metadata" JSONB NOT NULL,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+    "archivedAt" TIMESTAMP(3),
+
+    CONSTRAINT "AgentSession_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "AgentRun" (
+    "id" TEXT NOT NULL,
+    "projectId" TEXT NOT NULL,
+    "sessionId" TEXT,
+    "requestedByUserId" TEXT,
+    "entrypoint" "AgentEntrypoint" NOT NULL,
+    "status" "AgentRunStatus" NOT NULL DEFAULT 'ACTIVE',
+    "prompt" TEXT NOT NULL,
+    "model" TEXT NOT NULL,
+    "provider" TEXT NOT NULL,
+    "summary" TEXT,
+    "inputTokens" INTEGER,
+    "outputTokens" INTEGER,
+    "metadata" JSONB NOT NULL,
+    "error" TEXT,
+    "startedAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "finishedAt" TIMESTAMP(3),
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+
+    CONSTRAINT "AgentRun_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "ProjectAgentLock" (
+    "projectId" TEXT NOT NULL,
+    "runId" TEXT NOT NULL,
+    "holderUserId" TEXT,
+    "acquiredAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "expiresAt" TIMESTAMP(3),
+
+    CONSTRAINT "ProjectAgentLock_pkey" PRIMARY KEY ("projectId")
+);
+
+-- CreateTable
+CREATE TABLE "PermissionGrant" (
+    "id" TEXT NOT NULL,
+    "resourceType" "PermissionResourceType" NOT NULL,
+    "resourceId" TEXT NOT NULL,
+    "principal" TEXT NOT NULL,
+    "role" "PermissionRole" NOT NULL,
+    "createdByUserId" TEXT,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "revokedAt" TIMESTAMP(3),
+
+    CONSTRAINT "PermissionGrant_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "PermissionSettings" (
+    "id" TEXT NOT NULL,
+    "resourceType" "PermissionResourceType" NOT NULL,
+    "resourceId" TEXT NOT NULL,
+    "externalShare" TEXT NOT NULL,
+    "comment" TEXT NOT NULL,
+    "copyDownload" TEXT NOT NULL,
+    "collaboratorMgmt" TEXT NOT NULL,
+    "agentTrigger" TEXT NOT NULL,
+    "agentCancel" TEXT NOT NULL,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "updatedAt" TIMESTAMP(3) NOT NULL,
+
+    CONSTRAINT "PermissionSettings_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateTable
+CREATE TABLE "AuditEntry" (
+    "id" TEXT NOT NULL,
+    "runId" TEXT,
+    "actorUserId" TEXT,
+    "action" TEXT NOT NULL,
+    "metadata" JSONB NOT NULL,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+
+    CONSTRAINT "AuditEntry_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateIndex
+CREATE UNIQUE INDEX "User_feishuOpenId_key" ON "User"("feishuOpenId");
+
+-- CreateIndex
+CREATE INDEX "PlatformRoleAssignment_userId_revokedAt_idx" ON "PlatformRoleAssignment"("userId", "revokedAt");
+
+-- CreateIndex
+CREATE INDEX "PlatformRoleAssignment_role_revokedAt_idx" ON "PlatformRoleAssignment"("role", "revokedAt");
+
+-- CreateIndex
+CREATE INDEX "Project_archivedAt_idx" ON "Project"("archivedAt");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "ProjectGroupBinding_projectId_key" ON "ProjectGroupBinding"("projectId");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "ProjectGroupBinding_chatId_key" ON "ProjectGroupBinding"("chatId");
+
+-- CreateIndex
+CREATE INDEX "ProjectGroupBinding_chatId_idx" ON "ProjectGroupBinding"("chatId");
+
+-- CreateIndex
+CREATE INDEX "AgentSession_projectId_archivedAt_idx" ON "AgentSession"("projectId", "archivedAt");
+
+-- CreateIndex
+CREATE INDEX "AgentSession_provider_model_idx" ON "AgentSession"("provider", "model");
+
+-- CreateIndex
+CREATE INDEX "AgentSession_updatedAt_idx" ON "AgentSession"("updatedAt");
+
+-- CreateIndex
+CREATE INDEX "AgentRun_projectId_status_idx" ON "AgentRun"("projectId", "status");
+
+-- CreateIndex
+CREATE INDEX "AgentRun_sessionId_idx" ON "AgentRun"("sessionId");
+
+-- CreateIndex
+CREATE INDEX "AgentRun_requestedByUserId_idx" ON "AgentRun"("requestedByUserId");
+
+-- CreateIndex
+CREATE INDEX "AgentRun_updatedAt_idx" ON "AgentRun"("updatedAt");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "ProjectAgentLock_runId_key" ON "ProjectAgentLock"("runId");
+
+-- CreateIndex
+CREATE INDEX "ProjectAgentLock_expiresAt_idx" ON "ProjectAgentLock"("expiresAt");
+
+-- CreateIndex
+CREATE INDEX "PermissionGrant_resourceType_resourceId_revokedAt_idx" ON "PermissionGrant"("resourceType", "resourceId", "revokedAt");
+
+-- CreateIndex
+CREATE INDEX "PermissionGrant_principal_revokedAt_idx" ON "PermissionGrant"("principal", "revokedAt");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "PermissionGrant_resourceType_resourceId_principal_role_revo_key" ON "PermissionGrant"("resourceType", "resourceId", "principal", "role", "revokedAt");
+
+-- CreateIndex
+CREATE INDEX "PermissionSettings_resourceType_resourceId_idx" ON "PermissionSettings"("resourceType", "resourceId");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "PermissionSettings_resourceType_resourceId_key" ON "PermissionSettings"("resourceType", "resourceId");
+
+-- CreateIndex
+CREATE INDEX "AuditEntry_runId_idx" ON "AuditEntry"("runId");
+
+-- CreateIndex
+CREATE INDEX "AuditEntry_actorUserId_idx" ON "AuditEntry"("actorUserId");
+
+-- CreateIndex
+CREATE INDEX "AuditEntry_createdAt_idx" ON "AuditEntry"("createdAt");
+
+-- AddForeignKey
+ALTER TABLE "PlatformRoleAssignment" ADD CONSTRAINT "PlatformRoleAssignment_userId_fkey" FOREIGN KEY ("userId") REFERENCES "User"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "Project" ADD CONSTRAINT "Project_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "ProjectGroupBinding" ADD CONSTRAINT "ProjectGroupBinding_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "ProjectGroupBinding" ADD CONSTRAINT "ProjectGroupBinding_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "AgentSession" ADD CONSTRAINT "AgentSession_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_sessionId_fkey" FOREIGN KEY ("sessionId") REFERENCES "AgentSession"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "AgentRun" ADD CONSTRAINT "AgentRun_requestedByUserId_fkey" FOREIGN KEY ("requestedByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_runId_fkey" FOREIGN KEY ("runId") REFERENCES "AgentRun"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "ProjectAgentLock" ADD CONSTRAINT "ProjectAgentLock_holderUserId_fkey" FOREIGN KEY ("holderUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "PermissionGrant" ADD CONSTRAINT "PermissionGrant_resourceId_fkey" FOREIGN KEY ("resourceId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "PermissionGrant" ADD CONSTRAINT "PermissionGrant_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "PermissionSettings" ADD CONSTRAINT "PermissionSettings_resourceId_fkey" FOREIGN KEY ("resourceId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "AuditEntry" ADD CONSTRAINT "AuditEntry_actorUserId_fkey" FOREIGN KEY ("actorUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;

hub/prisma/migrations/20260707101108_add_role_trigger_grant/migration.sql

@@ -0,0 +1,27 @@
+-- CreateTable
+CREATE TABLE "RoleTriggerGrant" (
+    "id" TEXT NOT NULL,
+    "projectId" TEXT NOT NULL,
+    "roleId" TEXT NOT NULL,
+    "principal" TEXT NOT NULL,
+    "createdByUserId" TEXT,
+    "createdAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    "revokedAt" TIMESTAMP(3),
+
+    CONSTRAINT "RoleTriggerGrant_pkey" PRIMARY KEY ("id")
+);
+
+-- CreateIndex
+CREATE INDEX "RoleTriggerGrant_projectId_roleId_revokedAt_idx" ON "RoleTriggerGrant"("projectId", "roleId", "revokedAt");
+
+-- CreateIndex
+CREATE INDEX "RoleTriggerGrant_principal_revokedAt_idx" ON "RoleTriggerGrant"("principal", "revokedAt");
+
+-- CreateIndex
+CREATE UNIQUE INDEX "RoleTriggerGrant_projectId_roleId_principal_revokedAt_key" ON "RoleTriggerGrant"("projectId", "roleId", "principal", "revokedAt");
+
+-- AddForeignKey
+ALTER TABLE "RoleTriggerGrant" ADD CONSTRAINT "RoleTriggerGrant_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE CASCADE ON UPDATE CASCADE;
+
+-- AddForeignKey
+ALTER TABLE "RoleTriggerGrant" ADD CONSTRAINT "RoleTriggerGrant_createdByUserId_fkey" FOREIGN KEY ("createdByUserId") REFERENCES "User"("id") ON DELETE SET NULL ON UPDATE CASCADE;

hub/prisma/migrations/20260707200000_dedup_and_audit_project/migration.sql

@@ -0,0 +1,23 @@
+-- FeishuEventReceipt: idempotency for inbound ws events (at-least-once redelivery).
+CREATE TABLE "FeishuEventReceipt" (
+    "id" TEXT NOT NULL,
+    "eventId" TEXT NOT NULL,
+    "eventType" TEXT NOT NULL,
+    "messageId" TEXT,
+    "receivedAt" TIMESTAMP(3) NOT NULL DEFAULT CURRENT_TIMESTAMP,
+
+    CONSTRAINT "FeishuEventReceipt_pkey" PRIMARY KEY ("id")
+);
+
+CREATE UNIQUE INDEX "FeishuEventReceipt_eventId_key" ON "FeishuEventReceipt"("eventId");
+CREATE INDEX "FeishuEventReceipt_eventType_idx" ON "FeishuEventReceipt"("eventType");
+CREATE INDEX "FeishuEventReceipt_messageId_idx" ON "FeishuEventReceipt"("messageId");
+CREATE INDEX "FeishuEventReceipt_receivedAt_idx" ON "FeishuEventReceipt"("receivedAt");
+
+-- AuditEntry: add projectId so audit points before/without a run (permission
+-- denials, slash commands) are locatable to a project.
+ALTER TABLE "AuditEntry" ADD COLUMN "projectId" TEXT;
+
+CREATE INDEX "AuditEntry_projectId_createdAt_idx" ON "AuditEntry"("projectId", "createdAt");
+
+ALTER TABLE "AuditEntry" ADD CONSTRAINT "AuditEntry_projectId_fkey" FOREIGN KEY ("projectId") REFERENCES "Project"("id") ON DELETE SET NULL ON UPDATE CASCADE;

hub/prisma/migrations/migration_lock.toml

@@ -0,0 +1,3 @@
+# Please do not edit this file manually
+# It should be added in your version-control system (e.g., Git)
+provider = "postgresql"

hub/prisma/schema.prisma

@@ -0,0 +1,333 @@
+// Prisma schema for Curriculum Project Hub.
+//
+// Aligns to spec/System (ADR-0001..0004, 0017). Key divergences from the
+// legacy teaching-material-host-service schema, each deliberate:
+//
+//  - No AgentSession.claudeSessionId. ADR-0017: session is provider/model-
+//    bound, not Claude-bound; `provider`+`model` replace it. Switching model
+//    = new session, so the unique constraint is on the session id alone.
+//  - PermissionRole enum = read/edit/manage (ADR-0004 capability lattice),
+//    distinct from platform UserRole (admin/teacher) — legacy conflated them.
+//  - ProjectGroupBinding is project→chat only (ADR-0001 1:1); legacy mixed
+//    user/chat targets into one binding table.
+//  - PermissionGrant + PermissionSettings land (ADR-0004), missing in legacy.
+//  - AgentRunStatus adds WAITING_FOR_USER + TIMED_OUT (spec RunState; enum
+//    completeness OPEN — add states without a schema migration war).
+
+generator client {
+  provider = "prisma-client-js"
+}
+
+datasource db {
+  provider = "postgresql"
+  url      = env("DATABASE_URL")
+}
+
+// --- Platform identity ---------------------------------------------------
+
+/// A Feishu user known to the Hub. principal sub-typology is OPEN (ADR-0004).
+model User {
+  id           String   @id @default(cuid())
+  feishuOpenId String   @unique
+  displayName  String
+  avatarUrl    String?
+  createdAt    DateTime @default(now())
+  updatedAt    DateTime @updatedAt
+
+  platformRoles    PlatformRoleAssignment[]
+  createdProjects  Project[]             @relation("projectCreator")
+  requestedRuns    AgentRun[]            @relation("runRequester")
+  heldLocks        ProjectAgentLock[]   @relation("lockHolder")
+  feishuBindings   ProjectGroupBinding[] @relation("bindingCreator")
+  permissionGrants PermissionGrant[]     @relation("grantCreator")
+  roleTriggerGrants RoleTriggerGrant[]   @relation("roleGrantCreator")
+  auditEntries     AuditEntry[]         @relation("auditActor")
+}
+
+/// Platform-level role (admin/teacher). Distinct from ADR-0004 PermissionRole.
+/// `admin` is the only override path for force-release (spec RequiresAdmin).
+model PlatformRoleAssignment {
+  id        String       @id @default(cuid())
+  userId    String
+  role      PlatformRole
+  createdAt DateTime     @default(now())
+  revokedAt DateTime?
+
+  user User @relation(fields: [userId], references: [id], onDelete: Cascade)
+
+  @@index([userId, revokedAt])
+  @@index([role, revokedAt])
+}
+
+enum PlatformRole {
+  ADMIN
+  TEACHER
+}
+
+// --- Project & Feishu binding (ADR-0001) ---------------------------------
+
+model Project {
+  id              String    @id @default(cuid())
+  name            String
+  workspaceDir    String
+  createdByUserId String?
+  createdAt       DateTime  @default(now())
+  updatedAt       DateTime  @updatedAt
+  archivedAt      DateTime?
+
+  createdBy          User?                 @relation("projectCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
+  groupBinding       ProjectGroupBinding?
+  agentSessions      AgentSession[]
+  agentRuns          AgentRun[]
+  agentLock          ProjectAgentLock?
+  permissionGrants   PermissionGrant[]     @relation("projectGrants")
+  permissionSettings PermissionSettings[] @relation("projectSettings")
+  roleTriggerGrants  RoleTriggerGrant[]   @relation("projectRoleGrants")
+  auditEntries       AuditEntry[]         @relation("projectAudit")
+
+  @@index([archivedAt])
+}
+
+/// ADR-0001: one project ↔ one Feishu chat (1:1). `chatId` is unique ⇒
+/// GroupBinding.WellFormed's injectivity half (no two projects bind one chat).
+/// The "at most one binding per project" half is enforced by the 1:1 relation.
+/// Group dissolution lifecycle is OPEN (ADR-0001 Consequences) — not modeled
+/// here; archival is a future policy, not a current column.
+model ProjectGroupBinding {
+  id              String   @id @default(cuid())
+  projectId       String   @unique
+  chatId          String   @unique
+  createdByUserId String?
+  createdAt       DateTime @default(now())
+  updatedAt       DateTime @updatedAt
+
+  project   Project @relation(fields: [projectId], references: [id], onDelete: Cascade)
+  createdBy User?   @relation("bindingCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
+
+  @@index([chatId])
+}
+
+// --- AgentRun, session, lock (ADR-0002, 0017) -----------------------------
+
+/// ADR-0017: session is provider/model-bound. No claudeSessionId; `provider`
+/// + `model` capture the binding. Same provider+model ⇒ reuse across runs
+/// (ADR-0002); a switch ⇒ new session.
+model AgentSession {
+  id         String    @id @default(cuid())
+  projectId  String
+  provider   String
+  model      String
+  title      String?
+  metadata   Json
+  createdAt  DateTime  @default(now())
+  updatedAt  DateTime  @updatedAt
+  archivedAt DateTime?
+
+  project Project     @relation(fields: [projectId], references: [id], onDelete: Cascade)
+  runs    AgentRun[]
+
+  @@index([projectId, archivedAt])
+  @@index([provider, model])
+  @@index([updatedAt])
+}
+
+/// spec RunState: active/waitingForUser/completed/failed/timedOut/canceled.
+/// Enum completeness OPEN (Run.lean:12) — adding a state is a value add, not a
+/// spec breach. DB mirrors the current enum.
+enum AgentRunStatus {
+  ACTIVE
+  WAITING_FOR_USER
+  COMPLETED
+  FAILED
+  TIMED_OUT
+  CANCELED
+}
+
+enum AgentEntrypoint {
+  FEISHU
+  WEB
+  CLI
+}
+
+model AgentRun {
+  id                String         @id @default(cuid())
+  projectId         String
+  sessionId         String?
+  requestedByUserId String?
+  entrypoint        AgentEntrypoint
+  status            AgentRunStatus @default(ACTIVE)
+  prompt            String
+  model             String
+  provider          String
+  summary           String?
+  inputTokens       Int?
+  outputTokens      Int?
+  metadata          Json
+  error             String?
+  startedAt         DateTime       @default(now())
+  finishedAt        DateTime?
+  updatedAt         DateTime       @updatedAt
+
+  project     Project         @relation(fields: [projectId], references: [id], onDelete: Cascade)
+  session     AgentSession?   @relation(fields: [sessionId], references: [id], onDelete: SetNull)
+  requestedBy User?           @relation("runRequester", fields: [requestedByUserId], references: [id], onDelete: SetNull)
+  projectLock ProjectAgentLock?
+
+  @@index([projectId, status])
+  @@index([sessionId])
+  @@index([requestedByUserId])
+  @@index([updatedAt])
+}
+
+/// ADR-0002: lock owner = run_id (not session/user/chat). `projectId @id` ⇒
+/// at most one lock per project (LockTable exclusivity). `runId @unique` ⇒
+/// a run holds at most one lock. WellFormed (holder is non-terminal) is an
+/// app-level invariant checked on read/write, not a DB constraint.
+model ProjectAgentLock {
+  projectId  String   @id
+  runId      String   @unique
+  holderUserId String?
+  acquiredAt DateTime @default(now())
+  expiresAt  DateTime?
+
+  project Project  @relation(fields: [projectId], references: [id], onDelete: Cascade)
+  run     AgentRun  @relation(fields: [runId], references: [id], onDelete: Cascade)
+  holder  User?     @relation("lockHolder", fields: [holderUserId], references: [id], onDelete: SetNull)
+
+  @@index([expiresAt])
+}
+
+// --- Permission grants & settings (ADR-0004) ----------------------------
+
+/// ADR-0004 PermissionRole: read ⊂ edit ⊂ manage (capability lattice).
+/// Distinct from PlatformRole. Force-release is admin-only, outside this
+/// lattice (spec RequiresAdmin).
+enum PermissionRole {
+  READ
+  EDIT
+  MANAGE
+}
+
+/// ADR-0004 resource_type: project | artifact | project_group. The resource
+/// id's meaning is determined by its type (artifact id semantics align to the
+/// Courseware half; OPEN here).
+enum PermissionResourceType {
+  PROJECT
+  ARTIFACT
+  PROJECT_GROUP
+}
+
+/// ADR-0004 PermissionGrant: resource × principal × role.
+/// `principal` is an opaque string (principal sub-typology OPEN, ADR-0004).
+/// The compound unique covers "one active grant per (resource, principal, role)"
+/// — revoked rows keep `revokedAt` set, so a re-grant after revocation is a new
+/// row, not a conflict.
+model PermissionGrant {
+  id              String               @id @default(cuid())
+  resourceType    PermissionResourceType
+  resourceId      String
+  principal       String
+  role            PermissionRole
+  createdByUserId String?
+  createdAt       DateTime             @default(now())
+  revokedAt       DateTime?
+
+  project   Project? @relation("projectGrants", fields: [resourceId], references: [id], onDelete: Cascade)
+  createdBy User?    @relation("grantCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
+
+  @@unique([resourceType, resourceId, principal, role, revokedAt])
+  @@index([resourceType, resourceId, revokedAt])
+  @@index([principal, revokedAt])
+}
+
+/// ADR-0004 PermissionSettings: six policy knobs, values OPEN. Stored as one
+/// opaque string column each; the enum/value-domain is decided by admin policy,
+/// not by this schema. `resourceType`+`resourceId` identify the resource.
+/// Related to Project only when resourceType=PROJECT (null otherwise).
+model PermissionSettings {
+  id               String               @id @default(cuid())
+  resourceType     PermissionResourceType
+  resourceId       String
+  externalShare    String
+  comment          String
+  copyDownload     String
+  collaboratorMgmt String
+  agentTrigger     String
+  agentCancel      String
+  createdAt        DateTime             @default(now())
+  updatedAt        DateTime             @updatedAt
+
+  project Project? @relation("projectSettings", fields: [resourceId], references: [id], onDelete: Cascade)
+
+  @@unique([resourceType, resourceId])
+  @@index([resourceType, resourceId])
+}
+
+
+/// Per-role agent trigger grant. Orthogonal to ADR-0004's PermissionGrant:
+/// ADR-0004 decides "can trigger an agent at all" (triggerAgent capability,
+/// edit+ role); this table decides "can trigger *which* agent role" (e.g.
+/// /review vs /draft). Two gates in series — both must pass.
+///
+/// `roleId` is an opaque string matching RoleEntry.id (ADR-0017: roles are
+/// data, not a code enum). `principal` mirrors ADR-0004's opaque principal
+/// (sub-typology OPEN). A project-scoped row grants the role on that project;
+/// the compound unique covers "one active grant per (project, principal, role)".
+/// Revocation via `revokedAt`, same pattern as PermissionGrant.
+model RoleTriggerGrant {
+  id              String   @id @default(cuid())
+  projectId       String
+  roleId          String
+  principal       String
+  createdByUserId String?
+  createdAt       DateTime @default(now())
+  revokedAt       DateTime?
+
+  project   Project @relation("projectRoleGrants", fields: [projectId], references: [id], onDelete: Cascade)
+  createdBy User?   @relation("roleGrantCreator", fields: [createdByUserId], references: [id], onDelete: SetNull)
+
+  @@unique([projectId, roleId, principal, revokedAt])
+  @@index([projectId, roleId, revokedAt])
+  @@index([principal, revokedAt])
+}
+
+// --- Audit (ADR Audit, content OPEN) -------------------------------------
+
+/// spec AuditEntry: minimal skeleton — one entry relates to a run. Event type,
+/// actor, timestamp, details are OPEN. This table mirrors that: `runId` is the
+model AuditEntry {
+  id          String   @id @default(cuid())
+  runId       String?
+  projectId   String?
+  actorUserId String?
+  action      String
+  metadata    Json
+  createdAt   DateTime @default(now())
+
+  actor   User?    @relation("auditActor", fields: [actorUserId], references: [id], onDelete: SetNull)
+  project Project? @relation("projectAudit", fields: [projectId], references: [id], onDelete: SetNull)
+
+  @@index([runId])
+  @@index([projectId, createdAt])
+  @@index([actorUserId])
+  @@index([createdAt])
+}
+
+// --- Feishu event dedup --------------------------------------------------
+
+/// Idempotency receipt for inbound Feishu ws events. The lark ws client may
+/// redeliver an event (at-least-once); without dedup a duplicate would spawn a
+/// second AgentRun — the lock would refuse it, but a FAILED run row + a busy
+/// reply would still leak. `eventId @unique` makes the second insert a no-op
+/// signal: the handler checks existence before processing.
+model FeishuEventReceipt {
+  id         String   @id @default(cuid())
+  eventId    String   @unique
+  eventType  String
+  messageId  String?
+  receivedAt DateTime @default(now())
+
+  @@index([eventType])
+  @@index([messageId])
+  @@index([receivedAt])
+}

hub/src/agent/cph.ts

@@ -0,0 +1,105 @@
+/**
+ * `cph` subprocess tools - the Hub<->Courseware coupling point.
+ *
+ * The Hub agent does not parse engineering-file models in-process; it calls the
+ * stable `cph` CLI (ADR-0016 version contract). `cph check` validates a
+ * project; `cph build` renders a target artifact. Version compatibility is the
+ * CLI's responsibility - it refuses incompatible `.cph-version` files with a
+ * `cphVersionMismatch` error diagnostic (ADR-0016); the Hub merely runs the
+ * subprocess and returns its stdout/stderr/exit to the model.
+ *
+ * The `cph` binary path is configurable (env `CPH_BIN`, default `cph` on
+ * PATH). All subprocesses run with `cwd = ctx.workspaceDir` so paths in
+ * diagnostics are relative to the project root.
+ */
+import { execFile } from "node:child_process";
+import { promisify } from "node:util";
+import { tool } from "ai";
+import { z } from "zod";
+import type { ToolContext, ToolDefinition } from "./tools.js";
+
+const execFileAsync = promisify(execFile);
+
+const CPH_BIN = process.env["CPH_BIN"] ?? "cph";
+const DEFAULT_TIMEOUT_MS = 120_000;
+
+interface ExecResult {
+  readonly exitCode: number;
+  readonly stdout: string;
+  readonly stderr: string;
+}
+
+async function runCph(args: readonly string[], workspaceDir: string): Promise<ExecResult> {
+  try {
+    const { stdout, stderr } = await execFileAsync(CPH_BIN, args, {
+      cwd: workspaceDir,
+      timeout: DEFAULT_TIMEOUT_MS,
+      maxBuffer: 10 * 1024 * 1024,
+    });
+    return { exitCode: 0, stdout, stderr };
+  } catch (e) {
+    // execFile rejects on non-zero exit; the error carries stdout/stderr/code.
+    const err = e as NodeJS.ErrnoException & { stdout?: string; stderr?: string; code?: number | string };
+    if (err.code === "ENOENT") {
+      return {
+        exitCode: 127,
+        stdout: "",
+        stderr: `cph binary not found at "${CPH_BIN}" (set CPH_BIN env or install cph on PATH)`,
+      };
+    }
+    return {
+      exitCode: typeof err.code === "number" ? err.code : 1,
+      stdout: err.stdout ?? "",
+      stderr: err.stderr ?? "",
+    };
+  }
+}
+
+/// `cph check <dir>` - validate a curriculum engineering file. Returns the
+/// checker's diagnostics (stdout) for the model to act on. Non-zero exit means
+/// the file has error diagnostics (ADR-0010); the output is still returned,
+/// not thrown - the model needs to see the diagnostics to fix them.
+export function cphCheckTool(ctx: ToolContext): ToolDefinition {
+  return tool({
+    description:
+      "Run `cph check` on the project's curriculum engineering file. Returns diagnostics (7 classes: structure/schema/compile/version...). Non-zero exit means error diagnostics present - read the output to fix them.",
+    inputSchema: z.object({
+      path: z.string().describe("Path to the engineering file dir; defaults to the workspace root.").optional(),
+    }),
+    execute: async (args): Promise<string> => {
+      const target = args.path ?? ".";
+      const res = await runCph(["check", target], ctx.workspaceDir);
+      return JSON.stringify({
+        exitCode: res.exitCode,
+        stdout: res.stdout,
+        stderr: res.stderr,
+      });
+    },
+  });
+}
+
+/// `cph build <dir> --target <T> -o <out>` - render a target artifact. The
+/// target (student/teacher/...) determines the build (ADR-0009). Output path
+/// is relative to the workspace unless absolute.
+export function cphBuildTool(ctx: ToolContext): ToolDefinition {
+  return tool({
+    description:
+      "Run `cph build` to render a curriculum artifact (e.g. student/teacher PDF). Target selects the build; output names the result file.",
+    inputSchema: z.object({
+      target: z.string().describe("Build target, e.g. 'student', 'teacher'."),
+      path: z.string().describe("Path to the engineering file dir; defaults to the workspace root.").optional(),
+      output: z.string().describe("Output file path (relative to workspace or absolute).").optional(),
+    }),
+    execute: async (args): Promise<string> => {
+      const target = args.path ?? ".";
+      const out = args.output ?? `build/${args.target}.pdf`;
+      const res = await runCph(["build", target, "--target", args.target, "-o", out], ctx.workspaceDir);
+      return JSON.stringify({
+        exitCode: res.exitCode,
+        stdout: res.stdout,
+        stderr: res.stderr,
+        output: out,
+      });
+    },
+  });
+}

hub/src/agent/models.ts

@@ -0,0 +1,105 @@
+/**
+ * Per-run model selection & role-based routing.
+ *
+ * ADR-0017 consequence: role-based model routing (different run kinds default
+ * to different models) is a **product/admin configuration** concern, not a spec
+ * invariant. This registry is the seam for that config; the concrete policy
+ * (which models are admin-enabled, which role maps to which default) is `OPEN`
+ * here — decided by admin settings + ADR, not hard-coded.
+ */
+
+/**
+ * A named role preset — the full per-run agent bundle. Roles are **data**, not
+ * a code enum: admin/teachers define them (ADR-0017: role-based routing is
+ * product config, not a spec invariant). `roleId` is an opaque string and
+ * doubles as the slash-command name (`/draft ...`) — the registry holds the
+ * role set, so new roles are added by configuration, not by editing code.
+ *
+ * A role bundles everything that distinguishes one agent persona from another:
+ * model, system prompt, and the tool surface (files / cph / feishu / skills /
+ * mcps). Per-run tool whitelisting is enforced by {@link ToolRegistry.subset};
+ * the model never sees tools outside its role's whitelist, even if it tries to
+ * call them — security does not rely on the system prompt.
+ */
+export interface RoleEntry {
+  readonly id: string;
+  /** Human label for the teacher-side switcher UX. */
+  readonly label: string;
+  /** Default model id for runs under this role, if a routing rule is set. */
+  readonly defaultModel: string | undefined;
+  /**
+   * System prompt seeding the agent's persona/instructions. Prepended to the
+   * run's messages only at session start (resume reads it from the transcript,
+   * see runner.ts). `undefined` ⇒ no system prompt (bare run).
+   */
+  readonly systemPrompt: string | undefined;
+  /**
+   * Tool names this role may use (whitelist). `undefined` ⇒ the full registered
+   * set (back-compat / unrestricted roles). An empty array ⇒ no tools at all.
+   * Names not present in the registry are silently dropped at run setup.
+   */
+  readonly tools: readonly string[] | undefined;
+}
+
+/** A model the admin has enabled for use by the Hub. */
+export interface ModelEntry {
+  readonly id: string;
+  /** Human label for the teacher-side switcher UX. */
+  readonly label: string;
+  /** True when the model is known to support tool use reliably. */
+  readonly toolCapable: boolean;
+}
+
+export interface ModelRegistry {
+  /** All models admin-enabled for this Hub instance. */
+  listModels(): readonly ModelEntry[];
+  /** All role presets currently configured (admin/teacher-defined). */
+  listRoles(): readonly RoleEntry[];
+  /** The role preset with the given id, if any. */
+  role(id: string): RoleEntry | undefined;
+  /** Resolve a model id: explicit request → role default → first enabled. */
+  resolve(requestedModel: string | undefined, roleId: string): string;
+}
+
+/**
+ * A simple in-memory registry. Real wiring reads from admin settings / DB; this
+ * is the skeleton seam. Both the model list and the role set are pluggable data
+ * — adding a role is a config change, not a code change.
+ */
+export class InMemoryModelRegistry implements ModelRegistry {
+  private readonly models: readonly ModelEntry[];
+  private readonly roles: Map<string, RoleEntry>;
+
+  constructor(models: readonly ModelEntry[], roles: readonly RoleEntry[] = []) {
+    this.models = models;
+    this.roles = new Map(roles.map((r) => [r.id, r]));
+  }
+
+  listModels(): readonly ModelEntry[] {
+    return this.models;
+  }
+
+  listRoles(): readonly RoleEntry[] {
+    return [...this.roles.values()];
+  }
+
+  role(id: string): RoleEntry | undefined {
+    return this.roles.get(id);
+  }
+
+  /**
+   * Resolve a model id for a run. Priority: teacher's explicit request → the
+   * role preset's default → the first admin-enabled model. `roleId` is a string
+   * so unknown roles degrade gracefully to the fallback rather than throwing.
+   */
+  resolve(requestedModel: string | undefined, roleId: string): string {
+    if (requestedModel !== undefined && this.models.some((m) => m.id === requestedModel)) {
+      return requestedModel;
+    }
+    const role = this.roles.get(roleId);
+    if (role?.defaultModel !== undefined) return role.defaultModel;
+    const first = this.models[0];
+    if (first === undefined) throw new Error("no models enabled for this Hub");
+    return first.id;
+  }
+}

hub/src/agent/provider.ts

@@ -0,0 +1,18 @@
+/**
+ * OpenRouter model factory.
+ *
+ * ADR-0017: the agent layer keeps role/model resolution separate from provider
+ * construction. A run carries a resolved model id, and switching model still
+ * means a new provider-bound session.
+ */
+import { createOpenAICompatible } from "@ai-sdk/openai-compatible";
+import type { LanguageModel } from "ai";
+
+export function createModelFactory(): (modelId: string) => LanguageModel {
+  const provider = createOpenAICompatible({
+    name: "openrouter",
+    baseURL: process.env.OPENROUTER_BASE_URL ?? "https://openrouter.ai/api/v1",
+    headers: { Authorization: `Bearer ${process.env.OPENROUTER_API_KEY ?? ""}` },
+  });
+  return (modelId: string) => provider(modelId);
+}

hub/src/agent/runner.ts

@@ -0,0 +1,140 @@
+/**
+ * Provider-bound agent runner.
+ *
+ * The AI SDK owns tool-call dispatch and message folding. The Hub owns the
+ * per-run tool context, role/model selection, transcript persistence, and the
+ * ADR-0017 session boundary: a run is bound to one model. Switching model is a
+ * new run + new session; cross-run continuity is carried by project
+ * memory/anchors (ADR-0003), not by this runner.
+ */
+import { generateText, stepCountIs, type LanguageModel, type ModelMessage } from "ai";
+import type { ToolContext, ToolRegistry } from "./tools.js";
+import { readTranscript, appendTranscript } from "./transcript.js";
+
+export type ModelFactory = (modelId: string) => LanguageModel;
+
+/** What the runner needs about the project to seed and bound a run. */
+export interface ProjectContext {
+  readonly projectId: string;
+  /** ADR-0001 binding - the chat this project is bound to. */
+  readonly boundChatId: string;
+  /** Absolute path to the curriculum engineering-file workspace. */
+  readonly workspaceDir: string;
+}
+
+export interface RunRequest {
+  readonly prompt: string;
+  /** Resolved model id (already chosen by the caller per ADR-0017). */
+  readonly model: string;
+  readonly project: ProjectContext;
+  readonly systemPrompt: string | undefined;
+  /** Iteration cap before the run is returned as `length`. Default 25. */
+  readonly maxIterations?: number;
+  /** Per-role tool whitelist (ADR-0017). Undefined means all registered tools. */
+  readonly toolWhitelist?: readonly string[] | undefined;
+  /** Path to the session transcript JSONL. If set, prior messages are loaded
+   *  from it before the run, and new messages are appended after. */
+  readonly transcriptPath?: string;
+}
+
+export type RunStatus = "completed" | "length" | "failed";
+
+export interface RunResult {
+  readonly status: RunStatus;
+  /** Full transcript of the run, for audit (ADR Audit, content OPEN). */
+  readonly messages: readonly ModelMessage[];
+  readonly usage: { inputTokens: number; outputTokens: number };
+  readonly error?: string;
+}
+
+const DEFAULT_MAX_ITERATIONS = 25;
+
+export async function runAgent(
+  modelFactory: ModelFactory,
+  tools: ToolRegistry,
+  req: RunRequest,
+): Promise<RunResult> {
+  const ctx: ToolContext = {
+    runId: cryptoRandomId(),
+    projectId: req.project.projectId,
+    boundChatId: req.project.boundChatId,
+    workspaceDir: req.project.workspaceDir,
+  };
+  const aiTools = tools.build(ctx, req.toolWhitelist);
+
+  // Load prior session messages from transcript (continuity across @bot calls
+  // in the same session). ADR-0003: session messages != group chat history.
+  let messages: ModelMessage[] = req.transcriptPath !== undefined ? await readTranscript(req.transcriptPath) : [];
+  const loadedCount = messages.length;
+  if (req.systemPrompt !== undefined && messages.length === 0) {
+    // System prompt only at the very start of a session; on resume it's
+    // already in the transcript.
+    messages = [{ role: "system", content: req.systemPrompt }];
+  }
+  messages = [...messages, { role: "user", content: req.prompt }];
+
+  const cap = req.maxIterations ?? DEFAULT_MAX_ITERATIONS;
+
+  try {
+    const result = await generateText({
+      model: modelFactory(req.model),
+      messages,
+      allowSystemInMessages: true,
+      tools: aiTools,
+      stopWhen: stepCountIs(cap),
+    });
+    const allMessages: ModelMessage[] = [...messages, ...result.responseMessages];
+    await appendTranscriptIfSet(req, allMessages, loadedCount);
+
+    const stoppedByStepCap = result.finishReason === "tool-calls" && result.steps.length >= cap;
+    const status: RunStatus =
+      result.finishReason === "stop"
+        ? "completed"
+        : result.finishReason === "length" || stoppedByStepCap
+          ? "length"
+          : "failed";
+    const error =
+      status === "failed"
+        ? `finishReason=${result.finishReason}`
+        : stoppedByStepCap
+          ? `exceeded maxIterations=${cap}`
+          : undefined;
+
+    return {
+      status,
+      messages: allMessages,
+      usage: {
+        inputTokens: result.usage.inputTokens ?? 0,
+        outputTokens: result.usage.outputTokens ?? 0,
+      },
+      ...(error !== undefined ? { error } : {}),
+    };
+  } catch (e) {
+    await appendTranscriptIfSet(req, messages, loadedCount);
+    return {
+      status: "failed",
+      messages,
+      usage: { inputTokens: 0, outputTokens: 0 },
+      error: e instanceof Error ? e.message : String(e),
+    };
+  }
+}
+
+/// Append only the messages produced this run (skip the `loadedCount` prior
+/// ones already in the file). Errors are swallowed - a transcript write
+/// failure must not lose the run result.
+async function appendTranscriptIfSet(req: RunRequest, messages: readonly ModelMessage[], loadedCount: number): Promise<void> {
+  if (req.transcriptPath === undefined) return;
+  const newMessages = messages.slice(loadedCount);
+  if (newMessages.length === 0) return;
+  try {
+    await appendTranscript(req.transcriptPath, newMessages);
+  } catch {
+    // Swallow - transcript is best-effort persistence; the run result is
+    // returned regardless. ADR-0002 lock ensures no concurrent writer.
+  }
+}
+
+function cryptoRandomId(): string {
+  return globalThis.crypto.randomUUID();
+}

hub/src/agent/tools.ts

@@ -0,0 +1,114 @@
+/**
+ * Tool registry - the agent's narrow, project-scoped tool surface.
+ *
+ * Unlike a general "Claude Code", the Hub agent operates on a curriculum
+ * engineering-file tree (ADR-0007) and reads Feishu context on demand
+ * (ADR-0003). Its tools are therefore bounded:
+ *
+ * - file-tree read/write against the project workspace dir,
+ * - `cph check` / `cph build` subprocess calls (the Courseware-side checker,
+ *   coupled only via the stable CLI contract ADR-0016),
+ * - Feishu context reads, which must honor ADR-0003's authorization invariant.
+ *
+ * The AI SDK owns tool-call dispatch; this registry owns Hub-specific tool
+ * construction and per-role whitelisting (ADR-0017).
+ */
+import { tool, type Tool } from "ai";
+import { z } from "zod";
+
+/** Per-run execution context closed over by every tool execute function. */
+export interface ToolContext {
+  readonly runId: string;
+  readonly projectId: string;
+  /** ADR-0001: the chat this project is bound to. Feishu reads must stay in it. */
+  readonly boundChatId: string;
+  /** Absolute path to the project's curriculum engineering-file workspace. */
+  readonly workspaceDir: string;
+}
+
+export type ToolDefinition = Tool;
+export type ToolFactory = (ctx: ToolContext) => ToolDefinition;
+
+export class ToolRegistry {
+  private readonly factories = new Map<string, ToolFactory>();
+
+  register(name: string, factory: ToolFactory): void {
+    if (this.factories.has(name)) {
+      throw new Error(`duplicate tool: ${name}`);
+    }
+    this.factories.set(name, factory);
+  }
+
+  /**
+   * Build the AI SDK `tools` record. If `names` is given, include only those
+   * tools (per-role whitelist, ADR-0017). Names not registered are silently
+   * dropped because role config may name tools a Hub instance does not provide.
+   */
+  build(ctx: ToolContext, names: readonly string[] | undefined): Record<string, ToolDefinition> {
+    const built: Record<string, ToolDefinition> = {};
+    const selected = names ?? [...this.factories.keys()];
+    for (const name of selected) {
+      const factory = this.factories.get(name);
+      if (factory !== undefined) {
+        built[name] = factory(ctx);
+      }
+    }
+    return built;
+  }
+}
+
+/**
+ * Thrown when a Feishu context read targets a chat other than the run's project's
+ * bound chat. This is the runtime enforcement of ADR-0003's
+ * `McpReadRequest.Authorized`: "Claude cannot pass arbitrary chat ids".
+ */
+export class UnauthorizedChatRead extends Error {
+  constructor(
+    readonly requestedChatId: string,
+    readonly boundChatId: string,
+  ) {
+    super(
+      `refused Feishu context read: requested chat ${requestedChatId} is not the run's project's bound chat ${boundChatId} (ADR-0003)`,
+    );
+    this.name = "UnauthorizedChatRead";
+  }
+}
+
+/** Schema for the Feishu context read tool's arguments. */
+export interface FeishuContextArgs {
+  readonly chat_id: string;
+  readonly anchor: "trigger_message" | "status_card" | "reply" | "thread";
+  readonly id: string;
+}
+
+/**
+ * Build the Feishu context-read tool factory. The execute closure enforces
+ * ADR-0003's invariant before any API call: the requested `chat_id` must equal
+ * `ctx.boundChatId`.
+ *
+ * The actual Feishu API call (read message / reply chain / thread / recent
+ * group messages) is injected as `read`, so the invariant check is separable
+ * from the transport. In tests `read` can be a stub; in production it wraps
+ * `@larksuiteoapi/node-sdk`.
+ */
+export function feishuContextTool(
+  read: (args: FeishuContextArgs, ctx: ToolContext, rt: unknown) => Promise<string>,
+  rt: unknown,
+): ToolFactory {
+  return (ctx) =>
+    tool({
+      description:
+        "Read on-demand Feishu context (a trigger message, status card, reply, or thread) for the current project's bound chat. The chat id must match the project binding.",
+      inputSchema: z.object({
+        chat_id: z.string().describe("The Feishu chat id to read from."),
+        anchor: z.enum(["trigger_message", "status_card", "reply", "thread"]).describe("Which kind of anchor to read."),
+        id: z.string().describe("The anchor id (message id or run id)."),
+      }),
+      execute: async (args): Promise<string> => {
+        if (args.chat_id !== ctx.boundChatId) {
+          throw new UnauthorizedChatRead(args.chat_id, ctx.boundChatId);
+        }
+        return read(args, ctx, rt);
+      },
+    });
+}

hub/src/agent/transcript.ts

@@ -0,0 +1,64 @@
+/**
+ * Session transcript — append-only JSONL file in the workspace.
+ *
+ * Each line is one AI SDK {@link ModelMessage}, JSON-encoded. The transcript lives at
+ * `workspaceDir/.cph/sessions/<sessionId>.jsonl`, following the same "workspace
+ * is a directory tree" principle as the engineering file itself (ADR-0007).
+ *
+ * This mirrors how Claude Code stores its transcript (a `.jsonl` file per
+ * session). The agent can read its own history via `read_file` — no special
+ * "load history" code path. ADR-0002's lock guarantees one run per project at a
+ * time, so the transcript is never concurrently written.
+ *
+ * ADR-0003: this stores **agent session messages** (prompt + response + tool
+ * calls produced by the Hub), NOT Feishu group chat history. The two are
+ * distinct; storing session messages does not conflict with "the Hub avoids
+ * becoming a full chat history store."
+ */
+import { readFile, mkdir, appendFile } from "node:fs/promises";
+import { join, dirname } from "node:path";
+import type { ModelMessage } from "ai";
+
+/// Subdirectory within a workspace where session transcripts live.
+export const TRANSCRIPT_DIR = ".cph/sessions";
+
+/** Path for a session's transcript file within a workspace. */
+export function transcriptPath(workspaceDir: string, sessionId: string): string {
+  return join(workspaceDir, TRANSCRIPT_DIR, `${sessionId}.jsonl`);
+}
+
+/**
+ * Read prior messages from a transcript file. Returns an empty array if the
+ * file doesn't exist yet (first run in this session). Corrupt lines are
+ * skipped — a partially-written last line (crash mid-append) won't break the
+ * next run.
+ */
+export async function readTranscript(path: string): Promise<ModelMessage[]> {
+  let content: string;
+  try {
+    content = await readFile(path, "utf8");
+  } catch {
+    return [];
+  }
+  const messages: ModelMessage[] = [];
+  for (const line of content.split("\n")) {
+    const trimmed = line.trim();
+    if (trimmed === "") continue;
+    try {
+      messages.push(JSON.parse(trimmed) as ModelMessage);
+    } catch {
+      // Skip corrupt line — likely a partial write from a crash.
+    }
+  }
+  return messages;
+}
+
+/**
+ * Append messages to a transcript file. Creates the parent directory if needed.
+ * Each message is written as one JSON line.
+ */
+export async function appendTranscript(path: string, messages: readonly ModelMessage[]): Promise<void> {
+  await mkdir(dirname(path), { recursive: true });
+  const lines = messages.map((m) => JSON.stringify(m)).join("\n") + "\n";
+  await appendFile(path, lines, "utf8");
+}

hub/src/agent/workspace.ts

@@ -0,0 +1,106 @@
+/**
+ * Workspace file tools - bounded read/write/list against the project's
+ * curriculum engineering-file tree (ADR-0007 directory tree).
+ *
+ * All paths are **confined to `ctx.workspaceDir`**: the handler resolves the
+ * requested relative path against the workspace root and rejects any path that
+ * escapes it (via `..` or absolute paths). This is the agent's only file
+ * surface; the Hub agent is narrower than a general coding agent.
+ */
+import { readFile, writeFile, readdir, mkdir } from "node:fs/promises";
+import { join, resolve, relative, isAbsolute } from "node:path";
+import { tool } from "ai";
+import { z } from "zod";
+import type { ToolContext, ToolDefinition } from "./tools.js";
+
+/** Thrown when a requested path escapes the project workspace root. */
+export class PathEscape extends Error {
+  constructor(readonly requested: string, readonly workspaceDir: string) {
+    super(`path escapes workspace: ${requested} (root ${workspaceDir})`);
+    this.name = "PathEscape";
+  }
+}
+
+/** Resolve a tool-supplied path against the workspace root, rejecting escapes. */
+function confine(requestedPath: string, workspaceDir: string): string {
+  if (isAbsolute(requestedPath)) {
+    // Allow absolute paths only if they're already inside the workspace.
+    const rel = relative(workspaceDir, requestedPath);
+    if (rel.startsWith("..") || rel === "") {
+      throw new PathEscape(requestedPath, workspaceDir);
+    }
+    return requestedPath;
+  }
+  const resolved = resolve(workspaceDir, requestedPath);
+  const rel = relative(workspaceDir, resolved);
+  if (rel.startsWith("..")) {
+    throw new PathEscape(requestedPath, workspaceDir);
+  }
+  return resolved;
+}
+
+export function readFileTool(ctx: ToolContext): ToolDefinition {
+  return tool({
+    description: "Read a file from the project's curriculum engineering-file workspace. Path is relative to the workspace root.",
+    inputSchema: z.object({
+      path: z.string().describe("Relative path within the workspace."),
+    }),
+    execute: async (args): Promise<string> => {
+      try {
+        const full = confine(args.path, ctx.workspaceDir);
+        return await readFile(full, "utf8");
+      } catch (e) {
+        return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
+      }
+    },
+  });
+}
+
+export function writeFileTool(ctx: ToolContext): ToolDefinition {
+  return tool({
+    description:
+      "Write a file in the project's curriculum engineering-file workspace. Path is relative to the workspace root. Creates parent directories.",
+    inputSchema: z.object({
+      path: z.string().describe("Relative path within the workspace."),
+      content: z.string().describe("The full file content to write."),
+    }),
+    execute: async (args): Promise<string> => {
+      try {
+        const full = confine(args.path, ctx.workspaceDir);
+        await mkdir(join(full, ".."), { recursive: true });
+        await writeFile(full, args.content, "utf8");
+        return JSON.stringify({ ok: true, path: args.path, bytes: args.content.length });
+      } catch (e) {
+        return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
+      }
+    },
+  });
+}
+
+interface Entry {
+  readonly name: string;
+  readonly kind: "file" | "dir";
+}
+
+export function listFilesTool(ctx: ToolContext): ToolDefinition {
+  return tool({
+    description: "List files and directories at a path within the workspace. Defaults to the workspace root.",
+    inputSchema: z.object({
+      path: z.string().describe("Relative path within the workspace; defaults to root.").optional(),
+    }),
+    execute: async (args): Promise<string> => {
+      const sub = args.path ?? ".";
+      try {
+        const full = confine(sub, ctx.workspaceDir);
+        const entries = await readdir(full, { withFileTypes: true });
+        const result: Entry[] = entries.map((e) => ({
+          name: e.name,
+          kind: e.isDirectory() ? "dir" : "file",
+        }));
+        return JSON.stringify(result);
+      } catch (e) {
+        return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
+      }
+    },
+  });
+}

hub/src/audit.ts

@@ -0,0 +1,59 @@
+/**
+ * Audit write path — A-8. The `AuditEntry` table existed but had no writer;
+ * callers (trigger path, permission denials, slash commands) had no way to
+ * record what happened. This module is that single write seam.
+ *
+ * ADR reference: spec Audit. The skeleton pins only the `runId` relation;
+ * event type / actor / timestamp / details are content-OPEN. This helper
+ * exposes `action` (event type) + `actorUserId` (actor) + `metadata`
+ * (details) + `projectId` (locates audit points that don't have a run, e.g.
+ * permission denials) + `runId` (loose string ref, not a Prisma relation —
+ * see schema). `createdAt` is `@default(now())` so we don't pass it.
+ *
+ * Best-effort by design: an audit failure must never break the caller's path
+ * (a trigger failing because the audit log is down would be a spec breach —
+ * audit is observability, not control). Errors are swallowed here. There's no
+ * logger in this layer yet; a future logger can be threaded in without
+ * changing the signature.
+ */
+import type { PrismaClient, Prisma } from "@prisma/client";
+
+export interface AuditInput {
+  readonly runId?: string | undefined;
+  readonly projectId?: string | undefined;
+  readonly actorUserId?: string | undefined;
+  readonly action: string;
+  readonly metadata: Record<string, unknown>;
+}
+
+/**
+ * Write one audit entry. Best-effort: any Prisma error is swallowed so the
+ * caller's path (trigger, permission gate, slash command) is unaffected.
+ *
+ * Optional fields are only included when defined — under
+ * `exactOptionalPropertyTypes`, assigning `undefined` to an optional key in a
+ * Prisma `create` payload is a type error (and would also write an explicit
+ * NULL rather than omit the column). Conditional assignment keeps the payload
+ * honest. The data object is typed as `AuditEntryUncheckedCreateInput` (the
+ * direct-FK variant) so it matches one branch of Prisma's `create` input
+ * union exactly — the relation-connect branch has no `projectId`/`runId`
+ * columns and would otherwise reject these fields.
+ */
+export async function writeAudit(
+  prisma: PrismaClient,
+  entry: AuditInput,
+): Promise<void> {
+  const data: Prisma.AuditEntryUncheckedCreateInput = {
+    action: entry.action,
+    metadata: entry.metadata as Prisma.InputJsonValue,
+  };
+  if (entry.runId !== undefined) data.runId = entry.runId;
+  if (entry.projectId !== undefined) data.projectId = entry.projectId;
+  if (entry.actorUserId !== undefined) data.actorUserId = entry.actorUserId;
+
+  try {
+    await prisma.auditEntry.create({ data });
+  } catch {
+    // Swallow: audit is best-effort and must not break the caller's path.
+  }
+}

hub/src/db.ts

@@ -0,0 +1,21 @@
+/**
+ * Prisma client singleton.
+ *
+ * Prisma's client is a connection-pooled datasource; constructing it per-query
+ * exhausts connections. This module exports one shared instance per process.
+ * Hot-reload (tsx watch) can re-import this module — the global guard prevents
+ * a second PrismaClient from being created.
+ */
+import { PrismaClient } from "@prisma/client";
+
+const globalForPrisma = globalThis as unknown as { __hubPrisma?: PrismaClient };
+
+export const prisma: PrismaClient =
+  globalForPrisma.__hubPrisma ??
+  new PrismaClient({
+    log: process.env["HUB_PRISMA_LOG"] !== undefined ? ["query", "error", "warn"] : ["error", "warn"],
+  });
+
+if (process.env["NODE_ENV"] !== "production") {
+  globalForPrisma.__hubPrisma = prisma;
+}

hub/src/feishu/client.ts

@@ -0,0 +1,177 @@
+/**
+ * Feishu lark client + long-connection event dispatcher.
+ *
+ * Uses lark's WebSocket long-connection mode (no public callback endpoint). The
+ * `EventDispatcher` registers `im.message.receive_v1`; the SDK delivers the raw
+ * event to our handler. This version of the SDK does not auto-normalize on the
+ * ws path — `normalize()` is a separate helper — so we work with the raw event
+ * shape directly (it carries chat_id, message_type, content, mentions).
+ *
+ * ADR-0001: the bot operates inside a project's bound group. It does not own
+ * the lock (ADR-0002) and is not the session owner.
+ */
+import * as lark from "@larksuiteoapi/node-sdk";
+import type { FastifyBaseLogger } from "fastify";
+
+export interface FeishuConfig {
+  readonly appId: string;
+  readonly appSecret: string;
+  readonly botOpenId: string;
+}
+
+export interface FeishuRuntime {
+  readonly client: lark.Client;
+  readonly logger: FastifyBaseLogger;
+}
+
+/** Raw `im.message.receive_v1` event payload (subset we use). */
+export interface MessageReceiveEvent {
+  readonly header?: {
+    readonly event_id?: string;
+    readonly event_type?: string;
+  };
+  readonly message: {
+    readonly message_id: string;
+    readonly chat_id: string;
+    readonly chat_type: string;
+    readonly message_type: string;
+    readonly content: string;
+    readonly mentions?: ReadonlyArray<{
+      readonly key: string;
+      readonly id: { readonly open_id?: string };
+      readonly name: string;
+    }>;
+  };
+  readonly sender: {
+    readonly sender_id: { readonly open_id?: string };
+    readonly sender_type: string;
+  };
+}
+
+/** Send a text message to a chat. */
+export async function sendText(rt: FeishuRuntime, chatId: string, text: string): Promise<void> {
+  // SDK exposes im.v1 dynamically at runtime; the generated types are weak
+  // there, so cast through the known shape.
+  const client = rt.client as unknown as {
+    im: { v1: { message: { create: (p: unknown) => Promise<unknown> } } };
+  };
+  await client.im.v1.message.create({
+    params: { receive_id_type: "chat_id" },
+    data: {
+      receive_id: chatId,
+      msg_type: "text",
+      content: JSON.stringify({ text }),
+    },
+  });
+}
+
+/** Send an interactive card to a chat. `card` is the lark card schema object. */
+export async function sendCard(
+  rt: FeishuRuntime,
+  chatId: string,
+  card: unknown,
+): Promise<string | null> {
+  const client = rt.client as unknown as {
+    im: { v1: { message: { create: (p: unknown) => Promise<{ data?: { message_id?: string } }> } } };
+  };
+  const res = await client.im.v1.message.create({
+    params: { receive_id_type: "chat_id" },
+    data: {
+      receive_id: chatId,
+      msg_type: "interactive",
+      content: JSON.stringify(card),
+    },
+  });
+  return res.data?.message_id ?? null;
+}
+
+/** Build a run-status card: status text + model selector + cancel button. */
+export function buildRunStatusCard(opts: {
+  readonly status: string;
+  readonly model: string;
+  readonly models: readonly { readonly id: string; readonly label: string }[];
+  readonly runId: string;
+}): unknown {
+  return {
+    config: { wide_screen_mode: true },
+    header: {
+      title: { tag: "plain_text", content: `@Claude · ${opts.status}` },
+      template: opts.status === "处理完成" ? "green" : opts.status === "处理出错" ? "red" : "blue",
+    },
+    elements: [
+      { tag: "div", text: { tag: "lark_md", content: `**model:** ${opts.model}` } },
+      {
+        tag: "action",
+        actions: [
+          {
+            tag: "select",
+            placeholder: { tag: "plain_text", content: "切换 model" },
+            options: opts.models.map((m) => ({ text: { tag: "plain_text", content: m.label }, value: m.id })),
+            value: opts.model,
+          },
+          {
+            tag: "button",
+            text: { tag: "plain_text", content: "取消" },
+            type: "danger",
+            value: JSON.stringify({ action: "cancel", runId: opts.runId }),
+          },
+        ],
+      },
+    ],
+  };
+}
+
+/**
+ * Start the lark WebSocket client and route `im.message.receive_v1` events to
+ * `onMessage`. The ws connection lives in the background; this resolves the
+ * runtime handle.
+ */
+/** Build a lark Client (HTTP API surface). Used before the ws starts, so tools
+ * that need to call Feishu APIs can hold it from server boot. */
+export function createLarkClient(config: FeishuConfig): lark.Client {
+  return new lark.Client({
+    appId: config.appId,
+    appSecret: config.appSecret,
+    appType: lark.AppType.SelfBuild,
+  });
+}
+
+export interface FeishuListener {
+  readonly runtime: FeishuRuntime;
+  readonly stop: () => Promise<void>;
+}
+
+/** Start the ws listener using an already-built client. Returns the runtime. */
+export function startFeishuListenerWithClient(
+  config: FeishuConfig,
+  client: lark.Client,
+  logger: FastifyBaseLogger,
+  onMessage: (event: MessageReceiveEvent, rt: FeishuRuntime) => Promise<void>,
+): FeishuRuntime {
+  const wsClient = new lark.WSClient({
+    appId: config.appId,
+    appSecret: config.appSecret,
+    domain: lark.Domain.Feishu,
+    loggerLevel: lark.LoggerLevel.info,
+  });
+  const rt: FeishuRuntime = { client, logger };
+  void wsClient.start({
+    eventDispatcher: new lark.EventDispatcher({}).register({
+      "im.message.receive_v1": async (data) => {
+        try {
+          await onMessage(data as MessageReceiveEvent, rt);
+        } catch (e) {
+          logger.error({ err: e }, "feishu message handler threw");
+        }
+      },
+    }),
+  });
+  return rt;
+}
+export function startFeishuListener(
+  config: FeishuConfig,
+  logger: FastifyBaseLogger,
+  onMessage: (event: MessageReceiveEvent, rt: FeishuRuntime) => Promise<void>,
+): FeishuRuntime {
+  return startFeishuListenerWithClient(config, createLarkClient(config), logger, onMessage);
+}

hub/src/feishu/read.ts

@@ -0,0 +1,97 @@
+/**
+ * Feishu context reader — the real implementation behind `feishuContextTool`.
+ *
+ * ADR-0003: Hub stores only anchors, reads Feishu context on demand. The tool
+ * (`feishu_read_context`) is already chat-authorized by `tools.ts` (chat must
+ * match the project binding). Here we actually call lark's `im.v1.message`:
+ *
+ *  - `trigger_message` / `reply`: `message.get` by message_id.
+ *  - `status_card`: the run's status card message — same `message.get` by id.
+ *  - `thread`: lark's thread replies. The SDK exposes `message.list` with a
+ *    `parent_message_id` filter; we map "thread" to that.
+ *
+ * The lark SDK's `im.v1.message` methods are dynamic at runtime (weak types);
+ * we cast through a known request/response shape and return a compact JSON for
+ * the model. All calls use the chat-authorized `client` from the runtime — no
+ * separate credential path, so the ADR-0003 invariant holds end-to-end.
+ */
+import type { FeishuRuntime } from "./client.js";
+import type { FeishuContextArgs } from "../agent/tools.js";
+import type { ToolContext } from "../agent/tools.js";
+
+/** Pragmatic shape of the lark message object we consume. */
+interface LarkMessage {
+  message_id?: string;
+  msg_type?: string;
+  content?: string;
+  create_time?: string;
+  sender?: { id?: string; sender_type?: string };
+  chat_id?: string;
+  parent_message_id?: string;
+  root_id?: string;
+}
+
+interface ImV1Message {
+  get: (p: { path: { message_id: string } }) => Promise<{ data?: { items?: LarkMessage[]; message?: LarkMessage } }>;
+  list: (p: {
+    params: { container_id_type: string; container_id: string; page_size?: number };
+  }) => Promise<{ data?: { items?: LarkMessage[] } }>;
+}
+
+function im(rt: FeishuRuntime): ImV1Message {
+  return (rt.client as unknown as { im: { v1: { message: ImV1Message } } }).im.v1.message;
+}
+
+/** Read on-demand Feishu context for the current run. Entry point for the tool. */
+export async function readFeishuContext(
+  args: FeishuContextArgs,
+  _ctx: ToolContext,
+  rt: unknown,
+): Promise<string> {
+  const runtime = rt as FeishuRuntime;
+  const api = im(runtime);
+  try {
+    switch (args.anchor) {
+      case "trigger_message":
+      case "status_card":
+      case "reply": {
+        // All three are single-message reads by id.
+        const res = await api.get({ path: { message_id: args.id } });
+        const msg = res.data?.message ?? res.data?.items?.[0];
+        if (msg === undefined) return JSON.stringify({ error: "message not found", id: args.id });
+        return JSON.stringify(compact(msg));
+      }
+      case "thread": {
+        // Thread = replies to a parent message. `container_id` is the parent's
+        // message_id; container_id_type=message_id scopes the list to that thread.
+        const res = await api.list({
+          params: {
+            container_id_type: "message_id",
+            container_id: args.id,
+            page_size: 50,
+          },
+        });
+        const items = res.data?.items ?? [];
+        return JSON.stringify(items.map(compact));
+      }
+      default:
+        return JSON.stringify({ error: `unknown anchor type: ${args.anchor as string}` });
+    }
+  } catch (e) {
+    return JSON.stringify({ error: e instanceof Error ? e.message : String(e) });
+  }
+}
+
+/** Project a lark message down to the fields the model actually needs. */
+function compact(m: LarkMessage): Record<string, unknown> {
+  return {
+    message_id: m.message_id,
+    msg_type: m.msg_type,
+    content: m.content,
+    create_time: m.create_time,
+    sender_id: m.sender?.id,
+    parent_message_id: m.parent_message_id,
+    root_id: m.root_id,
+  };
+}
+

hub/src/feishu/trigger.ts

@@ -0,0 +1,361 @@
+/**
+ * Feishu @bot trigger → AgentRun lifecycle.
+ *
+ * The core path (ADR-0001..0003, 0017):
+ *  1. A message mentioning the bot arrives in a project group.
+ *  2. Resolve the chat → project binding (ADR-0001). Unknown chat ⇒ ignored.
+ *  3. Create an AgentRun + AgentSession (provider-bound, ADR-0017).
+ *  4. Acquire the project lock for the run (ADR-0002). If locked, reply busy.
+ *  5. Run the agent loop; the agent reads Feishu context on demand through the
+ *     ADR-0003-authorized tool (chat must match binding).
+ *  6. On finish/fail/timeout: release the lock, post a status card.
+ *
+ * The agent model id comes from the ModelRegistry (ADR-0017 role-based
+ * routing, role-as-data). The trigger does not pick a model directly.
+ */
+import type { PrismaClient } from "@prisma/client";
+import type { FastifyBaseLogger } from "fastify";
+import { sendText, sendCard, buildRunStatusCard, type FeishuRuntime, type MessageReceiveEvent } from "./client.js";
+import type { ToolRegistry } from "../agent/tools.js";
+import type { ModelRegistry } from "../agent/models.js";
+import { runAgent, type ModelFactory, type ProjectContext } from "../agent/runner.js";
+import { acquireLock, currentLockRunId, releaseLock } from "../lock.js";
+import { canTriggerAgent, canTriggerRole } from "../permission.js";
+import { transcriptPath } from "../agent/transcript.js";
+import { writeAudit } from "../audit.js";
+
+interface TriggerDeps {
+  readonly prisma: PrismaClient;
+  readonly modelFactory: ModelFactory;
+  readonly tools: ToolRegistry;
+  readonly models: ModelRegistry;
+  readonly logger: FastifyBaseLogger;
+}
+
+/**
+ * Build the message handler. Returns a function suitable for the lark
+ * `im.message.receive_v1` event. The handler is async and long-running (the
+ * agent run is the long leg); the lock guarantees one run per project at a time.
+ */
+export function makeTriggerHandler(deps: TriggerDeps) {
+  return async (event: MessageReceiveEvent, rt: FeishuRuntime): Promise<void> => {
+    const msg = event.message;
+    const sender = event.sender;
+    void sender; // sender→user mapping is OPEN (principal sub-typology)
+
+    // Dedup: the lark ws client redelivers at-least-once. A duplicate event
+    // would spawn a second AgentRun — the lock would refuse it, but a FAILED
+    // run row + a busy reply would leak. Record the event_id up front; if it
+    // already exists, this is a redelivery → stop.
+    const eventId = event.header?.event_id;
+    if (eventId !== undefined && eventId !== "") {
+      const existing = await deps.prisma.feishuEventReceipt.findUnique({
+        where: { eventId },
+        select: { id: true },
+      });
+      if (existing !== null) {
+        deps.logger.debug({ eventId }, "feishu trigger: duplicate event, skipping");
+        return;
+      }
+      await deps.prisma.feishuEventReceipt.create({
+        data: {
+          eventId,
+          eventType: event.header?.event_type ?? "im.message.receive_v1",
+          messageId: msg.message_id,
+        },
+      });
+    }
+
+    // Only react to text messages in group chats.
+    if (msg.message_type !== "text") return;
+    const chatId = msg.chat_id;
+    if (chatId === "") return;
+
+    // ADR-0001: resolve chat → project. Unknown chat ⇒ not a project group.
+    const binding = await deps.prisma.projectGroupBinding.findUnique({
+      where: { chatId },
+      select: { projectId: true },
+    });
+    if (binding === null) {
+      deps.logger.debug({ chatId }, "feishu trigger: chat not bound to any project");
+      return;
+    }
+    const projectId = binding.projectId;
+    // ADR-0004: triggerAgent requires edit on the project. principal=sender
+ // open_id (sub-typology OPEN — pragmatic choice, see permission.ts).
+    const senderOpenId = event.sender.sender_id.open_id ?? "";
+    if (senderOpenId !== "") {
+      const perm = await canTriggerAgent(deps.prisma, projectId, senderOpenId);
+      if (!perm.allowed) {
+        deps.logger.info({ projectId, senderOpenId, reason: perm.reason }, "feishu trigger: permission denied");
+        await writeAudit(deps.prisma, { projectId, actorUserId: senderOpenId || undefined, action: "trigger.denied", metadata: { reason: perm.reason } });
+        await sendText(rt, chatId, "无权限触发。");
+        return;
+      }
+    }
+
+    const prompt = extractPrompt(msg);
+    if (prompt === null) return;
+
+    // Slash commands: session management, not agent runs. These bypass the
+    // lock — they don't create a run, so they can't conflict with one.
+    if (prompt.startsWith("/")) {
+      const cmd = prompt.split(/\s+/)[0];
+      switch (cmd) {
+        case "/new": {
+          await deps.prisma.agentSession.updateMany({
+            where: { projectId, archivedAt: null },
+            data: { archivedAt: new Date() },
+          });
+          await sendText(rt, chatId, "已开新会话,下次 @bot 将从头开始。");
+          return;
+        }
+        case "/resume": {
+          const latest = await deps.prisma.agentSession.findFirst({
+            where: { projectId, archivedAt: { not: null } },
+            orderBy: { archivedAt: "desc" },
+            select: { id: true },
+          });
+          if (latest === null) {
+            await sendText(rt, chatId, "没有可恢复的会话。");
+            return;
+          }
+          await deps.prisma.agentSession.update({
+            where: { id: latest.id },
+            data: { archivedAt: null },
+          });
+          await sendText(rt, chatId, "已恢复上一个会话。");
+          return;
+        }
+        case "/reset": {
+          await deps.prisma.agentSession.updateMany({
+            where: { projectId, archivedAt: null },
+            data: { archivedAt: new Date() },
+          });
+          await sendText(rt, chatId, "已重置,下次 @bot 将从头开始。");
+          return;
+        }
+        default:
+          break;
+      }
+    }
+
+    // ADR-0002: if locked by another run, reply busy.
+    const existing = await currentLockRunId(deps.prisma, projectId);
+    if (existing !== null) {
+      await sendText(rt, chatId, "项目正在处理中,请稍候。");
+      return;
+    }
+
+    const project = await deps.prisma.project.findUnique({
+      where: { id: projectId },
+      select: { workspaceDir: true },
+    });
+    if (project === null) {
+      deps.logger.error({ projectId }, "feishu trigger: project missing");
+      return;
+    }
+
+    // ADR-0017: role-as-data. Parse a leading `/<role>` command; unknown
+    // slashes are left as literal text (extractRole returns null). Falls back
+    // to "draft" when no role is named — the registry degrades gracefully.
+    const { roleId: parsedRole, prompt: cleanPrompt } = extractRole(prompt, deps.models);
+    const roleId = parsedRole ?? "draft";
+    // Per-role trigger gate (ADR-0017). Orthogonal to ADR-0004's
+    // canTriggerAgent above: that checked "can trigger an agent at all";
+    // this checks "can trigger *this* role". Unconfigured role ⇒ open.
+    if (senderOpenId !== "") {
+      const rolePerm = await canTriggerRole(deps.prisma, projectId, roleId, senderOpenId);
+      if (!rolePerm.allowed) {
+        deps.logger.info({ projectId, roleId, senderOpenId, reason: rolePerm.reason }, "feishu trigger: role permission denied");
+        await writeAudit(deps.prisma, { projectId, actorUserId: senderOpenId || undefined, action: "trigger.role_denied", metadata: { roleId, reason: rolePerm.reason } });
+        await sendText(rt, chatId, `无权限使用角色 ${roleId}。`);
+        return;
+      }
+    }
+    const role = deps.models.role(roleId);
+    const model = deps.models.resolve(undefined, roleId);
+    const providerId = "openrouter";
+    // Per-role bundle (ADR-0017): systemPrompt seeds persona; tools whitelist
+    // is enforced inside runAgent when it builds the SDK tools record. `tools:
+    // undefined` means the full registered set (unrestricted role).
+    const systemPrompt = role?.systemPrompt;
+
+    // ADR-0017: provider+model-bound session. Reuse if one exists for this
+    // (project, provider, model) triple; otherwise create.
+    const existingSession = await deps.prisma.agentSession.findFirst({
+      where: { projectId, provider: providerId, model, archivedAt: null },
+      select: { id: true },
+    });
+    const session =
+      existingSession !== null
+        ? await deps.prisma.agentSession.update({
+            where: { id: existingSession.id },
+            data: { provider: providerId, model, updatedAt: new Date() },
+            select: { id: true },
+          })
+        : await deps.prisma.agentSession.create({
+            data: {
+              projectId,
+              provider: providerId,
+              model,
+              title: cleanPrompt.slice(0, 40) || null,
+              metadata: {},
+            },
+            select: { id: true },
+          });
+
+    const run = await deps.prisma.agentRun.create({
+      data: {
+        projectId,
+        sessionId: session.id,
+        requestedByUserId: null, // sender→user mapping is OPEN (principal sub-typology)
+        entrypoint: "FEISHU",
+        status: "ACTIVE",
+        prompt: cleanPrompt,
+        model,
+        provider: providerId,
+        metadata: { roleId },
+      },
+      select: { id: true },
+    });
+    await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.created", metadata: { roleId, model, prompt: cleanPrompt.slice(0, 200) } });
+
+    // ADR-0002: acquire the project lock for this run.
+    try {
+      await acquireLock(deps.prisma, projectId, run.id, null);
+    } catch {
+      await deps.prisma.agentRun.update({
+        where: { id: run.id },
+        data: { status: "FAILED", error: "lock race", finishedAt: new Date() },
+      });
+      await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.lock_race", metadata: {} });
+      await sendText(rt, chatId, "项目正在处理中,请稍候。");
+      return;
+    }
+
+    await sendText(rt, chatId, `已开始处理(role: ${roleId}, model: ${model})。`);
+
+    const projectCtx: ProjectContext = {
+      projectId,
+      boundChatId: chatId, // ADR-0003: Feishu reads stay in this chat
+      workspaceDir: project.workspaceDir,
+    };
+
+    // Run the agent — fire-and-forget from the ws handler's perspective.
+    // Per-run tools + systemPrompt come from the role bundle (ADR-0017).
+    runAgent(deps.modelFactory, deps.tools, {
+      prompt: cleanPrompt,
+      model,
+      project: projectCtx,
+      systemPrompt,
+      toolWhitelist: role?.tools,
+      transcriptPath: transcriptPath(project.workspaceDir, session.id),
+    })
+      .then(async (result) => {
+        await deps.prisma.agentRun.update({
+          where: { id: run.id },
+          data: {
+            status:
+              result.status === "completed"
+                ? "COMPLETED"
+                : result.status === "length"
+                  ? "TIMED_OUT"
+                  : "FAILED",
+            inputTokens: result.usage.inputTokens,
+            outputTokens: result.usage.outputTokens,
+            error: result.error ?? null,
+            finishedAt: new Date(),
+          },
+        });
+        await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.finished", metadata: { status: result.status, inputTokens: result.usage.inputTokens, outputTokens: result.usage.outputTokens } });
+        await sendCard(rt, chatId, buildRunStatusCard({
+          status: statusReply(result.status),
+          model,
+          models: deps.models.listModels(),
+          runId: run.id,
+        }));
+      })
+      .catch(async (e) => {
+        // The run may have been removed (admin force-delete, or test reset)
+        // between creation and this callback. A P2025 from update is not
+        // actionable here — log and still post the status card.
+        try {
+          await deps.prisma.agentRun.update({
+            where: { id: run.id },
+            data: { status: "FAILED", error: String(e), finishedAt: new Date() },
+          });
+        } catch (updateErr) {
+          deps.logger.warn({ runId: run.id, err: String(updateErr) }, "trigger: could not mark run FAILED (already gone?)");
+        }
+        await writeAudit(deps.prisma, { runId: run.id, projectId, action: "run.failed", metadata: { error: String(e) } });
+        await sendCard(rt, chatId, buildRunStatusCard({
+          status: "处理出错",
+          model,
+          models: deps.models.listModels(),
+          runId: run.id,
+        }));
+      })
+      .finally(async () => {
+        await releaseLock(deps.prisma, run.id);
+      });
+  };
+}
+
+function statusReply(status: "completed" | "length" | "failed"): string {
+  switch (status) {
+    case "completed":
+      return "处理完成。";
+    case "length":
+      return "处理达到步数上限,已停止。";
+    case "failed":
+      return "处理出错。";
+  }
+}
+
+/**
+ * Extract the prompt text from a text message, stripping @mentions.
+ * Returns null if the message is empty after stripping or doesn't mention the bot.
+ * Lark text content is JSON: `{"text":"@_user_1 do something"}`.
+ */
+export function extractPrompt(msg: MessageReceiveEvent["message"]): string | null {
+  // Check for bot mention — mentions[].id.open_id should include the bot.
+  // The dispatcher already routes only message events; we further require
+  // that the bot is among the mentions (if no mentions, it's not @bot).
+  const mentions = msg.mentions;
+  if (mentions === undefined || mentions.length === 0) return null;
+
+  try {
+    const parsed = JSON.parse(msg.content) as { text?: string };
+    const text = parsed.text;
+    if (typeof text !== "string") return null;
+    // Strip @mentions (@_user_1 etc.) and trim; remainder is the prompt.
+    const stripped = text.replace(/@_\w+\s*/g, "").trim();
+    return stripped === "" ? null : stripped;
+  } catch {
+    return null;
+  }
+}
+/**
+ * Parse a leading `/<role>` command from a prompt (e.g. `/draft 帮我写教案`).
+ * Returns the role id and the remaining prompt with the command stripped.
+ * Control commands already handled upstream (`/new`, `/resume`, `/reset`) are
+ * ignored here — they never reach this function.
+ *
+ * Unknown `/foo` that isn't a registered role: returns `null` role and the
+ * original prompt unchanged (the slash is treated as literal text). Role
+ * resolution still happens via the registry's fallback.
+ */
+export function extractRole(
+  prompt: string,
+  registry: { role(id: string): unknown },
+): { roleId: string | null; prompt: string } {
+  const m = /^\/(\S+)\s*/.exec(prompt);
+  if (m === null || m[1] === undefined) return { roleId: null, prompt };
+  const roleId = m[1];
+  if (registry.role(roleId) === undefined) {
+    // Unknown slash command — leave the prompt as-is (no silent role switch).
+    return { roleId: null, prompt };
+  }
+  return { roleId, prompt: prompt.slice(m[0].length) };
+}

hub/src/lock.ts

@@ -0,0 +1,79 @@
+/**
+ * ProjectAgentLock — ADR-0002 invariant enforcement at the DB layer.
+ *
+ * `projectId @id` gives at-most-one lock per project; `runId @unique` gives a
+ * run holds at most one lock. Those are DB-level. The spec's `WellFormed`
+ * invariant ("holder is a non-terminal run") is app-level: it must hold on
+ * every read of the lock table. `assertLockHolderActive` enforces it on the
+ * read path — if a lock exists but its run is terminal, that's a bug (the run
+ * should have released it), surfaced as an error rather than silently trusted.
+ */
+import type { PrismaClient } from "@prisma/client";
+import type { AgentRunStatus } from "@prisma/client";
+
+/// spec RunState.Terminal: completed/failed/timedOut/canceled.
+/// active/waitingForUser are NOT terminal — the lock must still be held.
+const TERMINAL_STATUSES: ReadonlySet<AgentRunStatus> = new Set([
+  "COMPLETED",
+  "FAILED",
+  "TIMED_OUT",
+  "CANCELED",
+]);
+
+export function isTerminal(status: AgentRunStatus): boolean {
+  return TERMINAL_STATUSES.has(status);
+}
+
+/**
+ * Acquire the project lock for a run. Throws if the project is already locked
+ * by another run (ADR-0002 exclusivity). The unique runId constraint means a
+ * run that already holds a lock elsewhere will also fail — that's correct, a
+ * run scopes to one project.
+ */
+export async function acquireLock(
+  prisma: PrismaClient,
+  projectId: string,
+  runId: string,
+  holderUserId: string | null,
+): Promise<void> {
+  await prisma.projectAgentLock.create({
+    data: { projectId, runId, holderUserId },
+  });
+}
+
+/**
+ * Release the lock owned by a run. Idempotent — a no-op if no lock exists.
+ * Called on run completion/failure/timeout/cancellation (ADR-0002).
+ */
+export async function releaseLock(prisma: PrismaClient, runId: string): Promise<void> {
+  await prisma.projectAgentLock.deleteMany({ where: { runId } });
+}
+
+/**
+ * The spec's `LockTable.WellFormed` on a single read: if `projectId` has a
+ * lock owned by `runId`, that run must be non-terminal. Throws if a terminal
+ * run still holds a lock — that's a release-path bug, not a recoverable state.
+ *
+ * Returns the lock's runId if a healthy lock exists, or null if unlocked.
+ */
+export async function currentLockRunId(
+  prisma: PrismaClient,
+  projectId: string,
+): Promise<string | null> {
+  const lock = await prisma.projectAgentLock.findUnique({
+    where: { projectId },
+    select: { runId: true },
+  });
+  if (lock === null) return null;
+
+  const run = await prisma.agentRun.findUnique({
+    where: { id: lock.runId },
+    select: { status: true },
+  });
+  if (run !== null && isTerminal(run.status)) {
+    throw new Error(
+      `lock invariant violated: project ${projectId} locked by terminal run ${lock.runId} (status ${run.status}) — release path bug (ADR-0002 WellFormed)`,
+    );
+  }
+  return lock.runId;
+}

hub/src/permission.ts

@@ -0,0 +1,126 @@
+/**
+ * Permission gate — ADR-0004 in code, project-scope.
+ *
+ * `triggerAgent` requires the `edit` capability (ADR-0004). `edit` is granted
+ * by a `PermissionGrant` with role `edit` or `manage` (manage ⊇ edit, spec
+ * `Role.can_mono`). This module checks that for the run's requester against
+ * the project resource.
+ *
+ * Scope decision (project-wise): the resource is `project`, not
+ * `project_group` — the run and lock scope to the project (ADR-0002), so the
+ * capability is checked against the project. per-artifact permission is `OPEN`
+ * pending a Courseware-side artifact id (ADR-0004 + ADR-0007 mapping).
+ *
+ * principal→user mapping is `OPEN` (ADR-0004 principal sub-typology). Here we
+ * use the sender's Feishu open_id as the principal string literal — a pragmatic
+ * choice for the first cut, not a spec decision. When a real principal model
+ * lands, this is the single seam to change.
+ *
+ * settings.agentTrigger composition is `OPEN` (ADR-0004 separates role-derived
+ * capabilities from settings policy knobs but doesn't pin the composition
+ * rule). This gate implements the role half only; settings composition is
+ * deferred and clearly marked.
+ */
+import type { PrismaClient } from "@prisma/client";
+import type { PermissionRole } from "@prisma/client";
+
+/// The roles that grant `edit` capability (edit itself + manage, by monotonicity).
+const EDIT_OR_HIGHER: ReadonlySet<PermissionRole> = new Set(["EDIT", "MANAGE"]);
+
+export interface PermissionResult {
+  readonly allowed: boolean;
+  readonly reason: string;
+}
+
+/**
+ * Check whether `principal` may trigger an agent run on `projectId`.
+ *
+ * Returns `{allowed, reason}`. On allow, the caller proceeds; on deny, the
+ * caller replies with the reason. Never throws — a DB error is a deny with the
+ * error as reason, so the run is not started on a broken state.
+ */
+export async function canTriggerAgent(
+  prisma: PrismaClient,
+  projectId: string,
+  principal: string,
+): Promise<PermissionResult> {
+  try {
+    // Look for an active (non-revoked) grant on the project resource for this
+    // principal, with a role that grants edit or higher.
+    const grant = await prisma.permissionGrant.findFirst({
+      where: {
+        resourceType: "PROJECT",
+        resourceId: projectId,
+        principal,
+        role: { in: ["EDIT", "MANAGE"] },
+        revokedAt: null,
+      },
+      select: { id: true, role: true },
+    });
+    if (grant !== null) {
+      return { allowed: true, reason: `granted by role ${grant.role}` };
+    }
+    return {
+      allowed: false,
+      reason: `no active edit+ grant for ${principal} on project ${projectId}`,
+    };
+  } catch (e) {
+    return { allowed: false, reason: `permission check failed: ${e instanceof Error ? e.message : String(e)}` };
+  }
+}
+/**
+ * Per-role trigger gate (ADR-0017: roles are product config). Orthogonal to
+ * {@link canTriggerAgent}: that decides "can trigger an agent at all"
+ * (ADR-0004 triggerAgent capability); this decides "can trigger *which* role".
+ * Two gates in series — both must pass.
+ *
+ * Semantics: if **no** `RoleTriggerGrant` row exists for `(projectId, roleId)`
+ * (regardless of principal), the role is unconfigured on this project →
+ * **allow** (back-compat: a project that hasn't configured per-role grants
+ * doesn't get locked down). Once any grant exists for that role on the
+ * project, only principals with an active grant may trigger it. "Grants exist
+ * but this principal has none" → deny (admin explicitly restricted the role).
+ *
+ * `roleId` matches `RoleEntry.id` (the slash-command name). `principal` is the
+ * same opaque string ADR-0004 uses (sender open_id here; principal
+ * sub-typology OPEN).
+ */
+export async function canTriggerRole(
+  prisma: PrismaClient,
+  projectId: string,
+  roleId: string,
+  principal: string,
+): Promise<PermissionResult> {
+  try {
+    // Any grant record (active OR revoked) for this (project, role)? If none,
+    // the role is unconfigured → allow (back-compat: no per-role restriction).
+    // A revoked grant still counts as "configured" — revoking one person must
+    // not silently reopen the role to everyone.
+    const anyGrant = await prisma.roleTriggerGrant.findFirst({
+      where: { projectId, roleId },
+      select: { id: true },
+    });
+    if (anyGrant === null) {
+      return { allowed: true, reason: `role ${roleId} unconfigured on project (open)` };
+    }
+    // Grants exist — this principal must hold one.
+    const grant = await prisma.roleTriggerGrant.findFirst({
+      where: { projectId, roleId, principal, revokedAt: null },
+      select: { id: true },
+    });
+    if (grant !== null) {
+      return { allowed: true, reason: `granted role ${roleId}` };
+    }
+    return {
+      allowed: false,
+      reason: `no active ${roleId} grant for ${principal} on project ${projectId}`,
+    };
+  } catch (e) {
+    return { allowed: false, reason: `role permission check failed: ${e instanceof Error ? e.message : String(e)}` };
+  }
+}
+
+/// Whether a role grants edit capability (edit or manage). Exported for tests.
+export function roleGrantsEdit(role: PermissionRole): boolean {
+  return EDIT_OR_HIGHER.has(role);
+}

hub/src/server.ts

@@ -0,0 +1,107 @@
+/**
+ * Hub entry — Fastify server + Feishu WebSocket listener.
+ *
+ * Wires the full trigger path: lark ws receives `im.message.receive_v1` →
+ * trigger handler resolves chat->project (ADR-0001), creates AgentRun + acquires
+ * the project lock (ADR-0002), runs the AI SDK-backed agent runner
+ * (ADR-0017), and releases the lock on finish. Feishu context reads inside the
+ * loop are ADR-0003-authorized (chat must match binding).
+ *
+ * Env (see .env.example):
+ *  DATABASE_URL, OPENROUTER_API_KEY, FEISHU_APP_ID/SECRET/BOT_OPEN_ID, PORT
+ */
+import "dotenv/config";
+import Fastify from "fastify";
+import { prisma } from "./db.js";
+import { createModelFactory } from "./agent/provider.js";
+import { InMemoryModelRegistry } from "./agent/models.js";
+import { ToolRegistry, feishuContextTool } from "./agent/tools.js";
+import { readFileTool, writeFileTool, listFilesTool } from "./agent/workspace.js";
+import { cphCheckTool, cphBuildTool } from "./agent/cph.js";
+import { createLarkClient, startFeishuListenerWithClient, type FeishuRuntime } from "./feishu/client.js";
+import { readFeishuContext } from "./feishu/read.js";
+import { makeTriggerHandler } from "./feishu/trigger.js";
+
+function requireEnv(name: string): string {
+  const v = process.env[name];
+  if (v === undefined || v === "") {
+    console.error(`[hub] missing required env: ${name}`);
+    process.exit(1);
+  }
+  return v;
+}
+
+async function main(): Promise<void> {
+  const databaseUrl = requireEnv("DATABASE_URL");
+  void databaseUrl; // prisma reads DATABASE_URL from env directly
+  requireEnv("OPENROUTER_API_KEY");
+  const feishuAppId = requireEnv("FEISHU_APP_ID");
+  const feishuAppSecret = requireEnv("FEISHU_APP_SECRET");
+  const feishuBotOpenId = requireEnv("FEISHU_BOT_OPEN_ID");
+  const port = Number(process.env["PORT"] ?? "8788");
+
+  const app = Fastify({ logger: true });
+
+  app.get("/api/healthz", async () => ({ ok: true, ts: Date.now() }));
+
+  // --- Agent seam wiring ---
+  const modelFactory = createModelFactory();
+  const models = new InMemoryModelRegistry(
+    [
+      { id: "z-ai/glm-4.6", label: "GLM-4.6", toolCapable: true },
+      { id: "anthropic/claude-3.5-sonnet", label: "Claude 3.5 Sonnet", toolCapable: true },
+    ],
+    [
+      {
+        id: "draft",
+        label: "草稿",
+        defaultModel: "z-ai/glm-4.6",
+        systemPrompt: undefined,
+        // Drafting needs full workspace + cph access.
+        tools: ["read_file", "write_file", "list_files", "cph_check", "cph_build", "feishu_read_context"],
+      },
+      {
+        id: "review",
+        label: "审校",
+        defaultModel: "anthropic/claude-3.5-sonnet",
+        systemPrompt: undefined,
+        // Review is read-only on artifacts; no write_file, no build.
+        tools: ["read_file", "list_files", "cph_check", "feishu_read_context"],
+      },
+    ],
+  );
+
+  // Build the lark client first — tools that call Feishu APIs hold it from boot.
+  const feishuConfig = { appId: feishuAppId, appSecret: feishuAppSecret, botOpenId: feishuBotOpenId };
+  const larkClient = createLarkClient(feishuConfig);
+  const feishuRt: FeishuRuntime = { client: larkClient, logger: app.log };
+
+  const tools = new ToolRegistry();
+  // ADR-0003: the handler enforces chat==boundChat before any API call;
+  // real read wraps @larksuiteoapi/node-sdk's im.v1.message get/list.
+  tools.register("feishu_read_context", feishuContextTool(readFeishuContext, feishuRt));
+  // Workspace file tools (ADR-0007 directory tree, path-confined).
+  tools.register("read_file", readFileTool);
+  tools.register("write_file", writeFileTool);
+  tools.register("list_files", listFilesTool);
+  // cph CLI tools (ADR-0016 version contract enforced by cph itself).
+  tools.register("cph_check", cphCheckTool);
+  tools.register("cph_build", cphBuildTool);
+
+  // --- Feishu listener (reuses the same lark client) ---
+  const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: app.log });
+  startFeishuListenerWithClient(feishuConfig, larkClient, app.log, trigger);
+
+  app.listen({ port, host: "0.0.0.0" }, (err, address) => {
+    if (err !== null) {
+      app.log.error({ err }, "listen failed");
+      process.exit(1);
+    }
+    app.log.info({ address }, "hub listening");
+  });
+}
+
+main().catch((e) => {
+  console.error("[hub] fatal:", e);
+  process.exit(1);
+});

hub/test/integration/cph.test.ts

@@ -0,0 +1,64 @@
+import { describe, it, expect, beforeEach, afterEach } from "vitest";
+import { cp, mkdtemp, rm } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { ToolRegistry, type ToolContext } from "../../src/agent/tools.js";
+import { cphCheckTool, cphBuildTool } from "../../src/agent/cph.js";
+
+const EXAMPLES_DIR = join(process.cwd(), "..", "examples", "TH-141");
+
+describe("cph subprocess tools (integration, real cph binary)", () => {
+  let ws: string;
+  let tools: ToolRegistry;
+
+  beforeEach(async () => {
+    // Use a writable copy of the real TH-141 example as the workspace.
+    ws = await mkdtemp(join(tmpdir(), "hub-cph-example-"));
+    await cp(EXAMPLES_DIR, ws, { recursive: true });
+    tools = new ToolRegistry();
+    tools.register("cph_check", cphCheckTool);
+    tools.register("cph_build", cphBuildTool);
+  });
+
+  afterEach(async () => {
+    await rm(ws, { recursive: true, force: true });
+  });
+
+  it("cph_check runs on the TH-141 example and returns diagnostics", async () => {
+    const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws };
+    const out = await executeTool(tools, "cph_check", {}, ctx);
+    const result = JSON.parse(out) as { exitCode: number; stdout: string; stderr: string };
+
+    // cph check exits 0 on a legal lesson (no error diagnostics, ADR-0010).
+    // If the example has warnings, exit is still 0.
+    expect(result.exitCode).toBe(0);
+  }, 30000);
+
+  it("cph_build renders the student target PDF", async () => {
+    const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws };
+    const out = await executeTool(tools, "cph_build", { target: "student", output: "build/test-student.pdf" }, ctx);
+    const result = JSON.parse(out) as { exitCode: number; stdout: string; stderr: string; output: string };
+
+    expect(result.exitCode).toBe(0);
+  }, 30000);
+
+  it("cph_check on a temp dir with no engineering file returns non-zero", async () => {
+    const empty = await mkdtemp(join(tmpdir(), "hub-cph-empty-"));
+    try {
+      const ctx = { runId: "r", projectId: "p", boundChatId: "c", workspaceDir: empty };
+      const out = await executeTool(tools, "cph_check", {}, ctx);
+      const result = JSON.parse(out) as { exitCode: number };
+      expect(result.exitCode).not.toBe(0);
+    } finally {
+      await rm(empty, { recursive: true, force: true });
+    }
+  }, 15000);
+});
+
+async function executeTool(tools: ToolRegistry, name: string, args: unknown, ctx: ToolContext): Promise<string> {
+  const def = tools.build(ctx)[name];
+  if (def?.execute === undefined) {
+    throw new Error(`missing executable tool: ${name}`);
+  }
+  return def.execute(args, { toolCallId: "call", messages: [], context: undefined }) as Promise<string>;
+}

hub/test/integration/helpers.ts

@@ -0,0 +1,207 @@
+/**
+ * Test helpers for integration tests.
+ *
+ * Each test gets a clean DB (tables truncated before the test), a mock
+ * FeishuRuntime (sendText/sendCard are no-ops that record calls), and a mock
+ * AI SDK model factory (doGenerate() returns canned responses - no network).
+ */
+import { PrismaClient } from "@prisma/client";
+import type { FastifyBaseLogger } from "fastify";
+import type {
+  LanguageModelV4,
+  LanguageModelV4CallOptions,
+  LanguageModelV4Content,
+  LanguageModelV4GenerateResult,
+  LanguageModelV4StreamResult,
+} from "@ai-sdk/provider";
+import type { FeishuRuntime } from "../../src/feishu/client.js";
+import type { ModelFactory } from "../../src/agent/runner.js";
+
+export const TEST_DATABASE_URL = "postgresql://paradigm:paradigm@127.0.0.1:5432/cph_hub_test";
+
+export const prisma = new PrismaClient({
+  datasources: { db: { url: TEST_DATABASE_URL } },
+});
+
+/** Truncate all tables before each test for isolation. */
+export async function resetDb(): Promise<void> {
+  const tables = [
+    "FeishuEventReceipt",
+    "AuditEntry",
+    "PermissionSettings",
+    "PermissionGrant",
+    "RoleTriggerGrant",
+    "ProjectAgentLock",
+    "AgentRun",
+    "AgentSession",
+    "ProjectGroupBinding",
+    "PlatformRoleAssignment",
+    "User",
+    "Project",
+  ];
+  // Truncate with CASCADE to wipe dependent rows in one shot.
+  await prisma.$executeRawUnsafe(`TRUNCATE TABLE ${tables.map((t) => `"${t}"`).join(", ")} RESTART IDENTITY CASCADE`);
+}
+
+/** A logger that discards everything (tests don't need fastify's pino). */
+export const silentLogger: FastifyBaseLogger = {
+  info() {}, warn() {}, error() {}, debug() {}, fatal() {},
+  child() { return this; },
+  level: "silent",
+} as unknown as FastifyBaseLogger;
+
+/** Records sendText/sendCard calls so tests can assert on them. */
+export interface MockFeishuRuntime extends FeishuRuntime {
+  readonly sentTexts: string[];
+  readonly sentCards: unknown[];
+}
+
+export function mockFeishuRuntime(): MockFeishuRuntime {
+  const sentTexts: string[] = [];
+  const sentCards: unknown[] = [];
+  // Mock the client — sendText/sendCard are in client.ts, not on the runtime
+  // object directly. We patch by providing a runtime whose client is a stub;
+  // the actual send functions cast through shape, so a minimal stub works.
+  const rt: MockFeishuRuntime = {
+    client: {
+      im: {
+        v1: {
+          message: {
+            create: async (p: unknown) => {
+              const payload = p as { data?: { msg_type?: string; content?: string } };
+              if (payload.data?.msg_type === "interactive") {
+                sentCards.push(payload.data.content ? JSON.parse(payload.data.content) : null);
+              } else {
+                try {
+                  const c = JSON.parse(payload.data?.content ?? "{}") as { text?: string };
+                  sentTexts.push(c.text ?? payload.data?.content ?? "");
+                } catch {
+                  sentTexts.push(payload.data?.content ?? "");
+                }
+              }
+              return { data: { message_id: "mock-msg-id" } };
+            },
+          },
+        },
+      },
+    } as unknown as FeishuRuntime["client"],
+    logger: silentLogger,
+    sentTexts,
+    sentCards,
+  };
+  return rt;
+}
+
+export interface MockToolCall {
+  readonly toolCallId: string;
+  readonly toolName: string;
+  readonly input: unknown;
+}
+
+export interface MockModelResponse {
+  readonly text?: string;
+  readonly toolCalls?: readonly MockToolCall[];
+  readonly finishReason?: "stop" | "length" | "content-filter" | "tool-calls" | "error" | "other";
+  readonly inputTokens?: number;
+  readonly outputTokens?: number;
+}
+
+export class MockLanguageModel implements LanguageModelV4 {
+  readonly specificationVersion = "v4";
+  readonly provider = "mock";
+  readonly supportedUrls: Record<string, RegExp[]> = {};
+  readonly calls: LanguageModelV4CallOptions[] = [];
+
+  constructor(
+    readonly modelId: string,
+    private readonly responses: readonly MockModelResponse[] = [{ text: "mock response" }],
+  ) {}
+
+  async doGenerate(options: LanguageModelV4CallOptions): Promise<LanguageModelV4GenerateResult> {
+    this.calls.push(options);
+    const configured = this.responses[this.calls.length - 1];
+    const last = this.responses[this.responses.length - 1];
+    const response =
+      configured ??
+      ((last?.toolCalls?.length ?? 0) > 0
+        ? { text: "mock response" }
+        : last ?? { text: "mock response" });
+    const content: LanguageModelV4Content[] = [];
+    if (response.text !== undefined) {
+      content.push({ type: "text", text: response.text });
+    }
+    for (const call of response.toolCalls ?? []) {
+      content.push({
+        type: "tool-call",
+        toolCallId: call.toolCallId,
+        toolName: call.toolName,
+        input: JSON.stringify(call.input),
+      });
+    }
+    const finishReason = response.finishReason ?? ((response.toolCalls?.length ?? 0) > 0 ? "tool-calls" : "stop");
+    return {
+      content,
+      finishReason: { unified: finishReason, raw: finishReason },
+      usage: {
+        inputTokens: { total: response.inputTokens ?? 10, noCache: undefined, cacheRead: undefined, cacheWrite: undefined },
+        outputTokens: { total: response.outputTokens ?? 5, text: undefined, reasoning: undefined },
+      },
+      response: { id: `mock-${this.calls.length}`, timestamp: new Date(), modelId: this.modelId },
+      warnings: [],
+    };
+  }
+
+  async doStream(_options: LanguageModelV4CallOptions): Promise<LanguageModelV4StreamResult> {
+    throw new Error("MockLanguageModel does not implement streaming");
+  }
+}
+
+export function createMockModelFactory(
+  responses: readonly MockModelResponse[] = [{ text: "mock response" }],
+): { readonly modelFactory: ModelFactory; readonly models: ReadonlyMap<string, MockLanguageModel> } {
+  const models = new Map<string, MockLanguageModel>();
+  return {
+    models,
+    modelFactory: (modelId) => {
+      const model = new MockLanguageModel(modelId, responses);
+      models.set(modelId, model);
+      return model;
+    },
+  };
+}
+
+/** Create a project + binding + user + grant for a test. */
+export async function seedProject(
+  projectId: string,
+  chatId: string,
+  options: { principal?: string; role?: "READ" | "EDIT" | "MANAGE" } = {},
+): Promise<void> {
+  const principal = options.principal ?? "ou_test_user";
+  const role = options.role ?? "EDIT";
+  await prisma.project.create({
+    data: {
+      id: projectId,
+      name: `Test ${projectId}`,
+      workspaceDir: `/tmp/test-${projectId}`,
+    },
+  });
+  await prisma.user.create({
+    data: {
+      id: "u_" + projectId,
+      feishuOpenId: principal,
+      displayName: "Test User",
+      platformRoles: { create: { role: "TEACHER" } },
+      permissionGrants: {
+        create: {
+          resourceType: "PROJECT",
+          resourceId: projectId,
+          principal,
+          role,
+        },
+      },
+    },
+  });
+  await prisma.projectGroupBinding.create({
+    data: { projectId, chatId, createdByUserId: "u_" + projectId },
+  });
+}

hub/test/integration/lock.test.ts

@@ -0,0 +1,85 @@
+import { describe, it, expect, beforeEach, afterAll } from "vitest";
+import { prisma, resetDb } from "./helpers.js";
+import { acquireLock, releaseLock, currentLockRunId, isTerminal } from "../../src/lock.js";
+
+describe("ProjectAgentLock WellFormed (integration, ADR-0002)", () => {
+  beforeEach(async () => {
+    await resetDb();
+  });
+
+  it("acquireLock + currentLockRunId round-trip", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-lock-1", name: "Test", workspaceDir: "/tmp/x" },
+    });
+    const run = await prisma.agentRun.create({
+      data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
+    });
+
+    await acquireLock(prisma, project.id, run.id, null);
+    const holder = await currentLockRunId(prisma, project.id);
+    expect(holder).toBe(run.id);
+
+    await releaseLock(prisma, run.id);
+    const after = await currentLockRunId(prisma, project.id);
+    expect(after).toBeNull();
+  });
+
+  it("acquireLock fails when project already locked (exclusivity)", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-lock-2", name: "Test", workspaceDir: "/tmp/x" },
+    });
+    const run1 = await prisma.agentRun.create({
+      data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
+    });
+    const run2 = await prisma.agentRun.create({
+      data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "y", model: "m", provider: "mock", metadata: {} },
+    });
+
+    await acquireLock(prisma, project.id, run1.id, null);
+    await expect(acquireLock(prisma, project.id, run2.id, null)).rejects.toThrow();
+  });
+
+  it("currentLockRunId throws when a terminal run holds the lock (WellFormed)", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-lock-3", name: "Test", workspaceDir: "/tmp/x" },
+    });
+    // Create a run that is already COMPLETED (terminal), then manually insert a lock.
+    const run = await prisma.agentRun.create({
+      data: { projectId: project.id, entrypoint: "FEISHU", status: "COMPLETED", prompt: "x", model: "m", provider: "mock", metadata: {}, finishedAt: new Date() },
+    });
+    await prisma.projectAgentLock.create({
+      data: { projectId: project.id, runId: run.id },
+    });
+
+    // WellFormed invariant: reading a lock held by a terminal run must throw.
+    await expect(currentLockRunId(prisma, project.id)).rejects.toThrow(/lock invariant violated/);
+  });
+
+  it("releaseLock is idempotent", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-lock-4", name: "Test", workspaceDir: "/tmp/x" },
+    });
+    const run = await prisma.agentRun.create({
+      data: { projectId: project.id, entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
+    });
+
+    await acquireLock(prisma, project.id, run.id, null);
+    await releaseLock(prisma, run.id);
+    // Second release is a no-op.
+    await releaseLock(prisma, run.id);
+    expect(await currentLockRunId(prisma, project.id)).toBeNull();
+  });
+
+  it("isTerminal matches spec RunState.Terminal", () => {
+    expect(isTerminal("ACTIVE")).toBe(false);
+    expect(isTerminal("WAITING_FOR_USER")).toBe(false);
+    expect(isTerminal("COMPLETED")).toBe(true);
+    expect(isTerminal("FAILED")).toBe(true);
+    expect(isTerminal("TIMED_OUT")).toBe(true);
+    expect(isTerminal("CANCELED")).toBe(true);
+  });
+});
+
+afterAll(async () => {
+  await prisma.$disconnect();
+});

hub/test/integration/role-permission.test.ts

@@ -0,0 +1,71 @@
+import { describe, it, expect, beforeEach, afterAll } from "vitest";
+import { prisma, resetDb } from "./helpers.js";
+import { canTriggerRole } from "../../src/permission.js";
+
+describe("canTriggerRole (integration, per-role gate)", () => {
+  beforeEach(async () => {
+    await resetDb();
+  });
+
+  afterAll(async () => {
+    await prisma.$disconnect();
+  });
+
+  it("allows when role is unconfigured on the project (back-compat: open)", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-role-1", name: "T", workspaceDir: "/tmp/x" },
+    });
+    const r = await canTriggerRole(prisma, project.id, "draft", "ou_a");
+    expect(r.allowed).toBe(true);
+  });
+
+  it("allows when principal holds an active grant for the role", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-role-2", name: "T", workspaceDir: "/tmp/x" },
+    });
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: project.id, roleId: "review", principal: "ou_a" },
+    });
+    const r = await canTriggerRole(prisma, project.id, "review", "ou_a");
+    expect(r.allowed).toBe(true);
+  });
+
+  it("denies when grants exist for the role but principal has none", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-role-3", name: "T", workspaceDir: "/tmp/x" },
+    });
+    // Someone else has the role; ou_b does not.
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: project.id, roleId: "review", principal: "ou_a" },
+    });
+    const r = await canTriggerRole(prisma, project.id, "review", "ou_b");
+    expect(r.allowed).toBe(false);
+  });
+
+  it("denies when the principal's grant was revoked", async () => {
+    const project = await prisma.project.create({
+      data: { id: "p-role-4", name: "T", workspaceDir: "/tmp/x" },
+    });
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: project.id, roleId: "review", principal: "ou_a", revokedAt: new Date() },
+    });
+    const r = await canTriggerRole(prisma, project.id, "review", "ou_a");
+    expect(r.allowed).toBe(false);
+  });
+
+  it("scopes grants per-project (grant on p1 does not allow on p2)", async () => {
+    const p1 = await prisma.project.create({ data: { id: "p-role-5a", name: "T", workspaceDir: "/tmp/x" } });
+    const p2 = await prisma.project.create({ data: { id: "p-role-5b", name: "T", workspaceDir: "/tmp/x" } });
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: p1.id, roleId: "review", principal: "ou_a" },
+    });
+    // p2 has the role configured for someone else; ou_a has no grant there.
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: p2.id, roleId: "review", principal: "ou_other" },
+    });
+    const onP1 = await canTriggerRole(prisma, p1.id, "review", "ou_a");
+    expect(onP1.allowed).toBe(true);
+    const onP2 = await canTriggerRole(prisma, p2.id, "review", "ou_a");
+    expect(onP2.allowed).toBe(false);
+  });
+});

hub/test/integration/trigger.test.ts

@@ -0,0 +1,295 @@
+import { describe, it, expect, beforeEach, afterAll, vi } from "vitest";
+import { prisma, resetDb, mockFeishuRuntime, createMockModelFactory, seedProject, silentLogger } from "./helpers.js";
+import { InMemoryModelRegistry } from "../../src/agent/models.js";
+import { ToolRegistry } from "../../src/agent/tools.js";
+import { makeTriggerHandler, extractPrompt } from "../../src/feishu/trigger.js";
+import type { MessageReceiveEvent } from "../../src/feishu/client.js";
+import type { ModelFactory } from "../../src/agent/runner.js";
+
+const bot = { key: "@_user_1", id: { open_id: "ou_bot" }, name: "Bot" };
+
+function makeEvent(chatId: string, text: string, senderOpenId = "ou_test_user", eventId?: string): MessageReceiveEvent {
+  const header = eventId !== undefined ? { event_id: eventId, event_type: "im.message.receive_v1" } : undefined;
+  return {
+    header,
+    message: {
+      message_id: "m_" + Math.random().toString(36).slice(2),
+      chat_id: chatId,
+      chat_type: "group",
+      message_type: "text",
+      content: JSON.stringify({ text }),
+      mentions: [bot],
+    },
+    sender: { sender_id: { open_id: senderOpenId }, sender_type: "user" },
+  };
+}
+
+describe("trigger full lifecycle (integration)", () => {
+  let modelFactory: ModelFactory;
+  let tools: ToolRegistry;
+  let models: InMemoryModelRegistry;
+  let rt: ReturnType<typeof mockFeishuRuntime>;
+
+  beforeEach(async () => {
+    await resetDb();
+    modelFactory = createMockModelFactory().modelFactory;
+    tools = new ToolRegistry();
+    models = new InMemoryModelRegistry(
+      [{ id: "mock-model", label: "Mock", toolCapable: true }],
+      [
+        { id: "draft", label: "草稿", defaultModel: "mock-model", systemPrompt: undefined, tools: undefined },
+        { id: "review", label: "审校", defaultModel: "mock-model", systemPrompt: undefined, tools: ["read_file"] },
+      ],
+    );
+    rt = mockFeishuRuntime();
+  });
+
+  it("creates a run, acquires + releases the lock, sends status card", async () => {
+    await seedProject("proj-1", "chat-1");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-1", "@_user_1 写教案"), rt);
+
+    // Wait for the async run to complete (fire-and-forget in trigger).
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.status).toBe("COMPLETED");
+    });
+
+    // Lock released (no lock row remains).
+    const locks = await prisma.projectAgentLock.findMany();
+    expect(locks).toHaveLength(0);
+
+    // A status card was sent.
+    expect(rt.sentCards.length).toBeGreaterThanOrEqual(1);
+    expect(rt.sentTexts).toContain("已开始处理(role: draft, model: mock-model)。");
+  });
+
+  it("rejects a sender without edit grant (ADR-0004)", async () => {
+    await seedProject("proj-2", "chat-2", { role: "READ" });
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-2", "@_user_1 写教案"), rt);
+
+    expect(rt.sentTexts).toContain("无权限触发。");
+    const runs = await prisma.agentRun.findMany();
+    expect(runs).toHaveLength(0);
+  });
+
+  it("replies busy when project is already locked (ADR-0002)", async () => {
+    await seedProject("proj-3", "chat-3");
+    // Manually create a lock by inserting a run + lock.
+    const existingRun = await prisma.agentRun.create({
+      data: { projectId: "proj-3", entrypoint: "FEISHU", status: "ACTIVE", prompt: "x", model: "m", provider: "mock", metadata: {} },
+    });
+    await prisma.projectAgentLock.create({
+      data: { projectId: "proj-3", runId: existingRun.id },
+    });
+
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+    await trigger(makeEvent("chat-3", "@_user_1 写教案"), rt);
+
+    expect(rt.sentTexts).toContain("项目正在处理中,请稍候。");
+    // No new run created.
+    const runs = await prisma.agentRun.findMany();
+    expect(runs).toHaveLength(1);
+  });
+
+  it("ignores messages from unbound chats (ADR-0001)", async () => {
+    await seedProject("proj-4", "chat-4");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-UNKNOWN", "@_user_1 写教案"), rt);
+
+    expect(rt.sentTexts).toHaveLength(0);
+    expect(rt.sentCards).toHaveLength(0);
+    const runs = await prisma.agentRun.findMany();
+    expect(runs).toHaveLength(0);
+  });
+
+  it("ignores messages without @bot mention", async () => {
+    await seedProject("proj-5", "chat-5");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    const event: MessageReceiveEvent = {
+      message: {
+        message_id: "m_nobot",
+        chat_id: "chat-5",
+        chat_type: "group",
+        message_type: "text",
+        content: JSON.stringify({ text: "hello no bot" }),
+        mentions: undefined,
+      },
+      sender: { sender_id: { open_id: "ou_test_user" }, sender_type: "user" },
+    };
+    await trigger(event, rt);
+
+    expect(rt.sentTexts).toHaveLength(0);
+    const runs = await prisma.agentRun.findMany();
+    expect(runs).toHaveLength(0);
+  });
+
+  it("/new archives current session (no run created)", async () => {
+    await seedProject("proj-6", "chat-6");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    // First @bot creates a session + run.
+    await trigger(makeEvent("chat-6", "@_user_1 写教案"), rt);
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.status).toBe("COMPLETED");
+    });
+
+    // /new archives the session.
+    await trigger(makeEvent("chat-6", "@_user_1 /new"), rt);
+    expect(rt.sentTexts).toContain("已开新会话,下次 @bot 将从头开始。");
+
+    const sessions = await prisma.agentSession.findMany();
+    expect(sessions).toHaveLength(1);
+    expect(sessions[0]?.archivedAt).not.toBeNull();
+    // No new run created for /new.
+    expect(await prisma.agentRun.findMany()).toHaveLength(1);
+  });
+
+  it("/resume un-archives the most recent session", async () => {
+    await seedProject("proj-7", "chat-7");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    // Create + archive a session via /new.
+    await trigger(makeEvent("chat-7", "@_user_1 写教案"), rt);
+    await vi.waitFor(async () => {
+      expect(await prisma.agentRun.findMany()).toHaveLength(1);
+    });
+    await trigger(makeEvent("chat-7", "@_user_1 /new"), rt);
+
+    // /resume un-archives.
+    await trigger(makeEvent("chat-7", "@_user_1 /resume"), rt);
+    expect(rt.sentTexts).toContain("已恢复上一个会话。");
+
+    const sessions = await prisma.agentSession.findMany();
+    expect(sessions).toHaveLength(1);
+    expect(sessions[0]?.archivedAt).toBeNull();
+  });
+
+  it("/reset archives current session", async () => {
+    await seedProject("proj-8", "chat-8");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-8", "@_user_1 写教案"), rt);
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.status).toBe("COMPLETED");
+    });
+
+    await trigger(makeEvent("chat-8", "@_user_1 /reset"), rt);
+    expect(rt.sentTexts).toContain("已重置,下次 @bot 将从头开始。");
+
+    const sessions = await prisma.agentSession.findMany();
+    expect(sessions).toHaveLength(1);
+    expect(sessions[0]?.archivedAt).not.toBeNull();
+  });
+
+  it("unknown slash command falls through to agent", async () => {
+    await seedProject("proj-9", "chat-9");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-9", "@_user_1 /unknown"), rt);
+    // Should create a run (falls through as a normal prompt).
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.prompt).toBe("/unknown");
+    });
+  });
+
+  it("denies /review when sender has no role grant (per-role gate)", async () => {
+    await seedProject("proj-10", "chat-10");
+    // Someone else holds review; ou_test_user does not.
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: "proj-10", roleId: "review", principal: "ou_other" },
+    });
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-10", "@_user_1 /review 看看这节"), rt);
+
+    expect(rt.sentTexts).toContain("无权限使用角色 review。");
+    const runs = await prisma.agentRun.findMany();
+    expect(runs).toHaveLength(0);
+  });
+
+  it("allows /review when sender holds the role grant", async () => {
+    await seedProject("proj-11", "chat-11");
+    await prisma.roleTriggerGrant.create({
+      data: { projectId: "proj-11", roleId: "review", principal: "ou_test_user" },
+    });
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-11", "@_user_1 /review 看看这节"), rt);
+
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.status).toBe("COMPLETED");
+      expect(runs[0]?.metadata).toMatchObject({ roleId: "review" });
+    });
+  });
+
+  it("extractRole: /draft sets roleId=draft, strips command from prompt", async () => {
+    await seedProject("proj-12", "chat-12");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-12", "@_user_1 /draft 写第三单元"), rt);
+
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.prompt).toBe("写第三单元");
+      expect(runs[0]?.metadata).toMatchObject({ roleId: "draft" });
+    });
+  });
+
+  it("dedups a redelivered event by event_id (no second run)", async () => {
+    await seedProject("proj-13", "chat-13");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    // First delivery: processes normally.
+    await trigger(makeEvent("chat-13", "@_user_1 写教案", "ou_test_user", "evt-dedup-1"), rt);
+    await vi.waitFor(async () => {
+      const runs = await prisma.agentRun.findMany();
+      expect(runs).toHaveLength(1);
+      expect(runs[0]?.status).toBe("COMPLETED");
+    });
+
+    // Redelivery of the same event_id: must not create a second run.
+    await trigger(makeEvent("chat-13", "@_user_1 写教案", "ou_test_user", "evt-dedup-1"), rt);
+    const runs2 = await prisma.agentRun.findMany();
+    expect(runs2).toHaveLength(1);
+
+    // Only one event receipt row.
+    const receipts = await prisma.feishuEventReceipt.findMany();
+    expect(receipts).toHaveLength(1);
+    expect(receipts[0]?.eventId).toBe("evt-dedup-1");
+  });
+
+  it("writes audit entries across the run lifecycle", async () => {
+    await seedProject("proj-14", "chat-14");
+    const trigger = makeTriggerHandler({ prisma, modelFactory, tools, models, logger: silentLogger });
+
+    await trigger(makeEvent("chat-14", "@_user_1 写教案"), rt);
+    await vi.waitFor(async () => {
+      const audit = await prisma.auditEntry.findMany();
+      expect(audit.length).toBeGreaterThanOrEqual(2);
+    });
+
+    const audit = await prisma.auditEntry.findMany({ orderBy: { createdAt: "asc" } });
+    expect(audit.some((a) => a.action === "run.created")).toBe(true);
+    expect(audit.some((a) => a.action === "run.finished")).toBe(true);
+  });
+});
+
+afterAll(async () => {
+  await prisma.$disconnect();
+});

hub/test/unit/audit.test.ts

@@ -0,0 +1,73 @@
+import { describe, expect, it, vi } from "vitest";
+import type { PrismaClient } from "@prisma/client";
+import { writeAudit } from "../../src/audit.js";
+
+/// Minimal mock: only the surface `writeAudit` touches. Cast through unknown
+/// so we don't have to implement the rest of the PrismaClient surface — this
+/// is a unit test, not a DB test.
+interface AuditEntryMock {
+  create: ReturnType<typeof vi.fn>;
+}
+function mockPrisma(): PrismaClient & { auditEntry: AuditEntryMock } {
+  return { auditEntry: { create: vi.fn() } } as unknown as PrismaClient & {
+    auditEntry: AuditEntryMock;
+  };
+}
+
+describe("writeAudit (A-8 audit write path)", () => {
+  it("creates a row with all fields set", async () => {
+    const prisma = mockPrisma();
+    prisma.auditEntry.create.mockResolvedValue({ id: "aud-1" });
+
+    await writeAudit(prisma, {
+      runId: "run-1",
+      projectId: "proj-1",
+      actorUserId: "user-1",
+      action: "run.triggered",
+      metadata: { source: "feishu" },
+    });
+
+    expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
+    expect(prisma.auditEntry.create).toHaveBeenCalledWith({
+      data: {
+        runId: "run-1",
+        projectId: "proj-1",
+        actorUserId: "user-1",
+        action: "run.triggered",
+        metadata: { source: "feishu" },
+      },
+    });
+  });
+
+  it("creates a row with only required fields (action + metadata)", async () => {
+    const prisma = mockPrisma();
+    prisma.auditEntry.create.mockResolvedValue({ id: "aud-2" });
+
+    await writeAudit(prisma, {
+      action: "permission.denied",
+      metadata: { reason: "no-edit-role" },
+    });
+
+    expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
+    expect(prisma.auditEntry.create).toHaveBeenCalledWith({
+      data: {
+        action: "permission.denied",
+        metadata: { reason: "no-edit-role" },
+      },
+    });
+  });
+
+  it("swallows a prisma error (best-effort, must not throw)", async () => {
+    const prisma = mockPrisma();
+    prisma.auditEntry.create.mockRejectedValue(new Error("db down"));
+
+    // Must not throw — audit is observability, not control.
+    await expect(
+      writeAudit(prisma, {
+        action: "run.triggered",
+        metadata: {},
+      }),
+    ).resolves.toBeUndefined();
+    expect(prisma.auditEntry.create).toHaveBeenCalledTimes(1);
+  });
+});

hub/test/unit/permission.test.ts

@@ -0,0 +1,16 @@
+import { describe, it, expect } from "vitest";
+import { roleGrantsEdit } from "../../src/permission.js";
+
+describe("roleGrantsEdit (ADR-0004 monotonicity)", () => {
+  it("READ does not grant edit", () => {
+    expect(roleGrantsEdit("READ")).toBe(false);
+  });
+
+  it("EDIT grants edit", () => {
+    expect(roleGrantsEdit("EDIT")).toBe(true);
+  });
+
+  it("MANAGE grants edit (manage ⊇ edit, spec can_mono)", () => {
+    expect(roleGrantsEdit("MANAGE")).toBe(true);
+  });
+});

hub/test/unit/prompt.test.ts

@@ -0,0 +1,75 @@
+import { describe, it, expect } from "vitest";
+import { extractPrompt } from "../../src/feishu/trigger.js";
+import type { MessageReceiveEvent } from "../../src/feishu/client.js";
+
+const bot = { key: "@_user_1", id: { open_id: "ou_bot" }, name: "Bot" };
+
+function msg(text: string, mentions: typeof bot[] | undefined = [bot]): MessageReceiveEvent["message"] {
+  return {
+    message_id: "m",
+    chat_id: "c",
+    chat_type: "group",
+    message_type: "text",
+    content: JSON.stringify({ text }),
+    mentions,
+  };
+}
+
+describe("extractPrompt (@bot mention parsing)", () => {
+  it("extracts the prompt after @bot", () => {
+    expect(extractPrompt(msg("@_user_1 帮我写教案"))).toBe("帮我写教案");
+  });
+
+  it("strips multiple mentions", () => {
+    const other = { key: "@_user_2", id: { open_id: "ou_other" }, name: "Other" };
+    expect(extractPrompt(msg("@_user_1 @_user_2 检查例题2", [bot, other]))).toBe("检查例题2");
+  });
+
+  it("returns null when only @bot with no prompt", () => {
+    expect(extractPrompt(msg("@_user_1"))).toBeNull();
+  });
+
+  it("returns null when @bot followed by whitespace only", () => {
+    expect(extractPrompt(msg("@_user_1   "))).toBeNull();
+  });
+  it("returns null when no mentions", () => {
+    const m: MessageReceiveEvent["message"] = {
+      message_id: "m", chat_id: "c", chat_type: "group",
+      message_type: "text",
+      content: JSON.stringify({ text: "hello" }),
+      mentions: undefined,
+    };
+    expect(extractPrompt(m)).toBeNull();
+  });
+
+  it("returns null for non-text message_type (content still parseable)", () => {
+    const m = msg("{}", [bot]);
+    // message_type check is the caller's job; extractPrompt only parses content.
+    // But with empty text it returns null.
+    expect(extractPrompt({ ...m, content: JSON.stringify({ text: "" }) })).toBeNull();
+  });
+
+  it("returns null when content is not valid JSON", () => {
+    const m: MessageReceiveEvent["message"] = {
+      message_id: "m",
+      chat_id: "c",
+      chat_type: "group",
+      message_type: "text",
+      content: "not json",
+      mentions: [bot],
+    };
+    expect(extractPrompt(m)).toBeNull();
+  });
+
+  it("returns null when JSON has no text field", () => {
+    const m: MessageReceiveEvent["message"] = {
+      message_id: "m",
+      chat_id: "c",
+      chat_type: "group",
+      message_type: "text",
+      content: JSON.stringify({ foo: "bar" }),
+      mentions: [bot],
+    };
+    expect(extractPrompt(m)).toBeNull();
+  });
+});

hub/test/unit/runner.test.ts

@@ -0,0 +1,39 @@
+import { describe, expect, it } from "vitest";
+import { mkdtemp, rm, writeFile } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { runAgent } from "../../src/agent/runner.js";
+import { ToolRegistry } from "../../src/agent/tools.js";
+import { readFileTool } from "../../src/agent/workspace.js";
+import { createMockModelFactory } from "../integration/helpers.js";
+
+describe("runAgent with AI SDK tool loop", () => {
+  it("executes SDK tools and returns the final assistant response", async () => {
+    const ws = await mkdtemp(join(tmpdir(), "hub-runner-"));
+    try {
+      await writeFile(join(ws, "lesson.txt"), "hello lesson", "utf8");
+      const tools = new ToolRegistry();
+      tools.register("read_file", readFileTool);
+      const { modelFactory, models } = createMockModelFactory([
+        {
+          toolCalls: [{ toolCallId: "call-1", toolName: "read_file", input: { path: "lesson.txt" } }],
+        },
+        { text: "done", finishReason: "stop" },
+      ]);
+
+      const result = await runAgent(modelFactory, tools, {
+        prompt: "read lesson.txt",
+        model: "mock-model",
+        project: { projectId: "p", boundChatId: "c", workspaceDir: ws },
+        systemPrompt: "system",
+        maxIterations: 5,
+      });
+
+      expect(result.status).toBe("completed");
+      expect(result.messages.at(-1)).toMatchObject({ role: "assistant" });
+      expect(models.get("mock-model")?.calls).toHaveLength(2);
+    } finally {
+      await rm(ws, { recursive: true, force: true });
+    }
+  });
+});

hub/test/unit/transcript.test.ts

@@ -0,0 +1,60 @@
+import { describe, it, expect, beforeEach, afterEach } from "vitest";
+import { mkdtemp, rm, readFile, writeFile } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { readTranscript, appendTranscript, transcriptPath, TRANSCRIPT_DIR } from "../../src/agent/transcript.js";
+import type { ModelMessage } from "ai";
+
+const sample: ModelMessage = { role: "user", content: "hello" };
+const reply: ModelMessage = { role: "assistant", content: "hi" };
+
+describe("transcript JSONL", () => {
+  let dir: string;
+  let path: string;
+
+  beforeEach(async () => {
+    dir = await mkdtemp(join(tmpdir(), "hub-transcript-"));
+    path = join(dir, "session.jsonl");
+  });
+  afterEach(async () => {
+    await rm(dir, { recursive: true, force: true });
+  });
+
+  it("readTranscript returns empty array for nonexistent file", async () => {
+    expect(await readTranscript(path)).toEqual([]);
+  });
+
+  it("appendTranscript creates parent dirs and writes JSONL", async () => {
+    await appendTranscript(path, [sample]);
+    const content = await readFile(path, "utf8");
+    expect(content.trim()).toBe(JSON.stringify(sample));
+  });
+
+  it("readTranscript reads back appended messages", async () => {
+    await appendTranscript(path, [sample, reply]);
+    const messages = await readTranscript(path);
+    expect(messages).toHaveLength(2);
+    expect(messages[0]).toEqual(sample);
+    expect(messages[1]).toEqual(reply);
+  });
+
+  it("multiple appends accumulate", async () => {
+    await appendTranscript(path, [sample]);
+    await appendTranscript(path, [reply]);
+    const messages = await readTranscript(path);
+    expect(messages).toHaveLength(2);
+  });
+
+  it("skips corrupt lines (partial write recovery)", async () => {
+    await appendTranscript(path, [sample]);
+    // Append a corrupt line (simulating a crash mid-write).
+    await writeFile(path, '{"broken json\n', { flag: "a" });
+    const messages = await readTranscript(path);
+    expect(messages).toHaveLength(1); // only the valid line
+  });
+
+  it("transcriptPath builds the expected path", () => {
+    const p = transcriptPath("/ws", "sess-1");
+    expect(p).toBe(join("/ws", TRANSCRIPT_DIR, "sess-1.jsonl"));
+  });
+});

hub/test/unit/workspace.test.ts

@@ -0,0 +1,88 @@
+import { describe, it, expect, beforeEach } from "vitest";
+import { mkdtemp, writeFile, mkdir } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { ToolRegistry, type ToolContext } from "../../src/agent/tools.js";
+import { readFileTool, writeFileTool, listFilesTool, PathEscape } from "../../src/agent/workspace.js";
+
+describe("workspace path confinement", () => {
+  let ws: string;
+  let tools: ToolRegistry;
+
+  beforeEach(async () => {
+    ws = await mkdtemp(join(tmpdir(), "hub-unit-"));
+    tools = new ToolRegistry();
+    tools.register("read_file", readFileTool);
+    tools.register("write_file", writeFileTool);
+    tools.register("list_files", listFilesTool);
+    await mkdir(join(ws, "sub"));
+    await writeFile(join(ws, "a.txt"), "hello");
+    await writeFile(join(ws, "sub", "b.txt"), "world");
+  });
+
+  const ctx = () => ({ runId: "r", projectId: "p", boundChatId: "c", workspaceDir: ws });
+
+  it("reads a file inside the workspace", async () => {
+    expect(await executeTool(tools, "read_file", { path: "a.txt" }, ctx())).toBe("hello");
+  });
+
+  it("reads nested files", async () => {
+    expect(await executeTool(tools, "read_file", { path: "sub/b.txt" }, ctx())).toBe("world");
+  });
+
+  it("rejects .. escapes as error JSON, not a throw", async () => {
+    const out = await executeTool(tools, "read_file", { path: "../../etc/passwd" }, ctx());
+    expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
+  });
+
+  it("rejects absolute paths outside the workspace", async () => {
+    const out = await executeTool(tools, "read_file", { path: "/etc/passwd" }, ctx());
+    expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
+  });
+
+  it("writes a file and reads it back", async () => {
+    await executeTool(tools, "write_file", { path: "sub/c.txt", content: "new" }, ctx());
+    expect(await executeTool(tools, "read_file", { path: "sub/c.txt" }, ctx())).toBe("new");
+  });
+
+  it("creates parent dirs on write", async () => {
+    await executeTool(tools, "write_file", { path: "deep/nested/d.txt", content: "x" }, ctx());
+    expect(await executeTool(tools, "read_file", { path: "deep/nested/d.txt" }, ctx())).toBe("x");
+  });
+
+  it("lists the workspace root", async () => {
+    const out = await executeTool(tools, "list_files", {}, ctx());
+    const entries = JSON.parse(out) as Array<{ name: string; kind: string }>;
+    expect(entries).toContainEqual({ name: "a.txt", kind: "file" });
+    expect(entries).toContainEqual({ name: "sub", kind: "dir" });
+  });
+
+  it("lists a subdirectory", async () => {
+    const out = await executeTool(tools, "list_files", { path: "sub" }, ctx());
+    const entries = JSON.parse(out) as Array<{ name: string; kind: string }>;
+    expect(entries).toContainEqual({ name: "b.txt", kind: "file" });
+  });
+
+  it("PathEscape is an Error subclass", () => {
+    expect(new PathEscape("../x", "/ws")).toBeInstanceOf(Error);
+    expect(new PathEscape("../x", "/ws").name).toBe("PathEscape");
+  });
+
+  it("read of nonexistent file returns error JSON", async () => {
+    const out = await executeTool(tools, "read_file", { path: "nope.txt" }, ctx());
+    expect((JSON.parse(out) as { error: string }).error).toBeTruthy();
+  });
+
+  it("write with .. escape returns error JSON", async () => {
+    const out = await executeTool(tools, "write_file", { path: "../escape.txt", content: "x" }, ctx());
+    expect((JSON.parse(out) as { error: string }).error).toContain("escapes workspace");
+  });
+});
+
+async function executeTool(tools: ToolRegistry, name: string, args: unknown, ctx: ToolContext): Promise<string> {
+  const def = tools.build(ctx)[name];
+  if (def?.execute === undefined) {
+    throw new Error(`missing executable tool: ${name}`);
+  }
+  return def.execute(args, { toolCallId: "call", messages: [], context: undefined }) as Promise<string>;
+}

hub/tsconfig.json

@@ -0,0 +1,22 @@
+{
+  "compilerOptions": {
+    "target": "ES2022",
+    "lib": ["ES2023"],
+    "module": "NodeNext",
+    "moduleResolution": "NodeNext",
+    "rootDir": "src",
+    "outDir": "dist",
+    "strict": true,
+    "noUncheckedIndexedAccess": true,
+    "exactOptionalPropertyTypes": true,
+    "noImplicitOverride": true,
+    "noFallthroughCasesInSwitch": true,
+    "verbatimModuleSyntax": true,
+    "skipLibCheck": true,
+    "esModuleInterop": true,
+    "forceConsistentCasingInFileNames": true,
+    "declaration": false,
+    "sourceMap": true
+  },
+  "include": ["src/**/*.ts"]
+}

hub/vitest.config.ts

@@ -0,0 +1,12 @@
+import { defineConfig } from "vitest/config";
+
+export default defineConfig({
+  test: {
+    include: ["test/**/*.test.ts"],
+    // Integration tests share one DB; run files sequentially to avoid
+    // concurrent truncate/insert races. Unit tests are fast either way.
+    pool: "forks",
+    fileParallelism: false,
+    env: { NODE_ENV: "test" },
+  },
+});

spec/README.md

@@ -1,74 +1,55 @@
-# spec —— 语义契约
+# spec —— Lean 语义母本
 
-## 这个项目在解决什么
+这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
 
-教研产出现在是一摞一次性的文档:写完就躺着,改一次要同步很多地方,没法校验、
-没法复用、没法追溯。这个项目想把教研产出变成可校验、可复用、能派生多种成品
-(讲义、教案、课件、归档)的工程化文件。
+## 现状
 
-但光有工程文件还不够。它要变成一个能卖钱的产品,还得:
+刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
 
-- 工程文件这种形式,正好适合现在大热的 LLM assistant 来改,从而提效;
-- 但 LLM 判不了一节课合不合法(它不能真去跑 typst 编译器、不能可靠地断言数据合不合
-  schema),所以产品里还有一个 rule-based checker:它真跑工具、给确定性的诊断,补上
-  LLM 判不了的这块。LLM 提效 + checker 兜底,两者一起才是完整的产品闭环。
-- 加上一些提升体验的小功能:飞书/企业微信集成、自动化提醒之类;
-- 如果要做 SaaS,还要有基本的管理概念:权限、LLM API 的配置和用量、费用等。
+## 构建
 
-工程文件是起点,不是终点。
+```sh
+cd spec
+lake build
+```
 
-## spec 是什么
+工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
 
-spec/ 是产品语义的契约,用 Lean 写。它定义产品各部件"是什么意思"。
+## 写作规范
 
-- 它是开发者和 coding assistant 共同的语义依据:两边对某个东西的理解,以这里为准。
-- 它不进产品运行时。运行时真正做校验的那个东西用什么技术实现,还没定;但它的语义,
-  先在这里固定下来。
-- 它精确、自洽,机器能校验它内部结构没有漏洞。它不保证实现一定符合它——
-  实现和它是否一致,没有自动检查,要靠人工或 coding assistant 不定期(或每次改动后)核对。
+### 双半契约:prose + type
 
-## 人机怎么一起干活
+每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:
 
-- 凭语义,不凭经验。这个领域新,coding assistant 在这里没有可靠的既有经验,
-  所以语义以 spec 的注释为准,不要凭训练先验臆测。
-- 契约没写的,就是不存在的。遇到没定的点,提出来让开发者定,不要替它选答案。
-- 改了实现或 spec 之后,两边是否还对得上,要核对一下;这一致性没有自动闸门。
+- **prose 半**给人读——说清"这在领域里是什么、为什么"。
+- **type 半**给机器读、给 type checker 把关——保证结构无洞。
 
-## 怎么往 spec 里写
+agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
 
-### 一条东西要不要进 spec
+### 标签分类法
 
-不写它,开发者和 coding assistant 会不会各自做出不同假设?会,就进;不会
-(显然的事、纯基础设施、普通 CRUD 字段),就不进。
+在 doc 注释里用以下标签标注每条语义的状态:
 
-### 进了之后,钉到多细
+- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
+- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
+- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。
 
-- 现在想清楚的,用 Lean 固定(声明、类型、关系)。
-- 没想清楚的,两三句话 prose 占位,标 `OPEN`。等讨论或业务反馈后再细化,
-  细化结果可以再用 Lean 固定。
-- 不在 Lean 里验证实现真的做了这些事。spec 只讲"要做什么、判什么";实现有没有真做,
-  不形式化证明。
-- 形式化定理:不用写;写了不是坏事,但现在很少有能写的定理。定理本身得是产品语义,
-  不是"实现该满足的性质"。
+### 分歧点测试(写之前先过一遍)
 
-### 写的时候
+新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**
 
-- 每个顶层声明要带 doc 注释,用 `/-- ... -/` 写自然语言,说清这在领域里是什么、为什么。
-  注释是语义的依据,Lean 类型保证结构,两者缺一不可。
-- 在注释里标这条语义的状态:
-  - `PINNED`:已定,契约在此处权威。
-  - `OPEN`:故意没定。不要假设它的解,遇到要提出来讨论。
-  - `ADR-NNNN`:指向 `docs/adr/` 下的决策记录。
-- 不用 `sorry`。没想清楚的,用 `OPEN` 标在注释里,不要用 `sorry` 假装成立——
-  那会让构建通过,却在契约里埋一个谎。
-- 不复述文件系统上能直接看到的东西(目录结构、文件名)。文件系统应当自描述,文档讲 context。
-- 不写变更史(进 git/ADR)。不搬 ADR 内部黑话,要表达就直说。
-  不为设计选择辩护("刻意用 X 而非 Y"),只说是什么。
-- "为什么"的背景考据(如某工具的内部机制)不进 spec,指向 ADR;但产品行为和设计模式要钉。
+- 会 → 它是分歧点,入契约。
+- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
+
+详见根 README 宪法第 5 条。
+
+### 不用 `sorry`
+
+无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
 
 ### 命名
 
-- 模块/命名空间:PascalCase,按分层,如 `Spec.System.Run`。
-- 类型:PascalCase。
-- 谓词(`Prop`):用意图清楚的词,如 `Legal…`、`ValidTransition`、`Can…`。
-- 文件粒度:一个带独立不变式的概念一个文件。
+- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
+- **类型**:PascalCase。
+- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
+- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。

spec/Spec/Courseware.lean

@@ -6,5 +6,16 @@ import Spec.Courseware.Open
 /-!
 # Courseware —— 产品层契约(课程工程文件)
 
-课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。
+护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。按四组组织:
+
+- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子
+  单位 `Element`、单节课 `Lesson`(element 的有序序列)。
+- **`Export`** —— export target = artifact + 有序 typed steps:产物 ADT `Artifact`
+  (`singleFile` / `fileTree`),build 规格 `TargetSpec`(artifact + steps + 覆盖声明
+  `covers`)与 `RenderConfig`。
+- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
+  诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
+  门控。
+- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
+  课程编排 `Course`。
 -/

spec/Spec/Courseware/Check.lean

@@ -2,7 +2,7 @@ import Spec.Courseware.Check.Diagnostic
 import Spec.Courseware.Check.Pipeline
 
 /-!
-# Courseware.Check —— 产品 checker 语义
+# Courseware.Check —— checker 语义
 
 诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处
 ADR-0010。

spec/Spec/Courseware/Check/Diagnostic.lean

@@ -2,39 +2,30 @@ import Spec.Courseware.Model.Lesson
 import Spec.Courseware.Export.Render
 
 /-!
-# Diagnostic —— 产品 checker 的诊断
+# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
 
-这个 codebase 是要拿去卖的产品。LLM 辅助操作提效是它的核心卖点之一——但 LLM 判不了
-一节课合不合法:它不能真的去跑 typst 编译器、不能可靠地断言一段数据合不合 schema、
-也不能可靠地检查文件齐不齐。所以产品里有一个 rule-based checker 来做这件事:它真跑
-工具、给确定性的诊断,补上 LLM 判不了的这块。这个 checker 的语义在这里(ADR-0010,
-经 ADR-0012、ADR-0016 修订)。它对 lesson 提诊断,每条有一个分类(`DiagKind`)和一
-个严重级别(`Severity`)。
-
-注意区分两个"检查":这里的 checker 是**产品功能**——用户把教研工程文件喂给 `cph`,
-检查这个工程文件合不合法。它和"开发时 spec 与实现是否一致"是两回事,后者没有自动
-闸门,靠核对。
-
-本模块钉三件事:严重级别二分;7 类诊断各自的含义和级别;"合法 lesson = 无 error 级
-诊断"这条判定。其中有些诊断是 LLM 判不了、得 checker 真跑工具才能判的(typst 编不编
-得过、数据合不合 schema、content 文件齐不齐)——这些用抽象谓词加 `Oracle` 表示:契约
-说"存在这条诊断、什么意思、什么级别",真值由 checker 给(契约不在 Lean 里内嵌 typst
-编译器去算)。引用解析(`@ref`、相对 import)不单列:它们都是 typst 编译期失败,归
-`typstCompile`(ADR-0012)。版本契约 `cphVersionMismatch`(ADR-0016)是第 7 类。
+产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
+修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
+本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
+error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
+型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
+说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
+编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
+`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。
 -/
 
 namespace Spec.Courseware
 
-/-- 诊断严重级别(ADR-0005)。`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,
-    只是有损)。更细级别(info/hint)未决策,故只二分。 -/
+/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不
+阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/
 inductive Severity where
   | warning
   | error
 
-/-- 诊断分类(ADR-0010,经 ADR-0012 折并为 6 类、ADR-0016 增至 7 类)。按 checker 怎么判分三层:
-    结构型(checker 自己按结构判):`partPathMissing`/`unknownKind`/`cphVersionMismatch`;
-    schema/外部工具型(得真跑工具):`missingContentFile`/`schemaViolation`/`typstCompile`;
-    语义型:`renderIgnored`。 -/
+/-- 诊断**分类**(`PINNED` 7 类, ADR-0010,经 ADR-0012 修订为 6 类,经 ADR-0016 增至 7
+类)。按"谁来判定"分三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`/
+`cphVersionMismatch`;**schema/外部设施型**(靠实现 oracle):
+`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:`renderIgnored`。 -/
 inductive DiagKind where
   /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
   | partPathMissing
@@ -45,19 +36,21 @@ inductive DiagKind where
   /-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/
   | schemaViolation
   /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
-      `import`/`include`。后两者 typst 在编译期检出,故归此类(ADR-0012)。外部工具型。 -/
+      `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期
+      检出,故归此类,ADR-0012)。外部设施型。 -/
   | typstCompile
   /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
   | renderIgnored
-  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。结构型(加载期判)。
-      工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时比对自身版本,不相容
-      即产此类。当前判定为版本完全相等才相容(MVP;后续可放宽为 semver 区间,判定逻辑可
-      逐步改而不动本分类)。`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
+  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
+      判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
+      定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
+      完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
+      `error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
   | cphVersionMismatch
 
-/-- 每类诊断的严重级别(ADR-0010)。六类 `error`(阻断);唯 `renderIgnored` 为 `warning`
-    ——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。钉成全函数使"哪类阻断"成为可
-    引用、可对齐的事实。 -/
+/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
+`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
+钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
 def DiagKind.severity : DiagKind → Severity
   | .partPathMissing    => .error
   | .unknownKind        => .error
@@ -67,51 +60,46 @@ def DiagKind.severity : DiagKind → Severity
   | .renderIgnored      => .warning
   | .cphVersionMismatch => .error
 
-/-- 缺渲染诊断的级别 = warning(ADR-0005/0010,非 error)。具名常量,使"它是 warning"
-    可被实现 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用本定义)。
-    等价于 `DiagKind.renderIgnored.severity`。 -/
+/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量,
+使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用
+本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/
 def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity
 
 variable (P : Primitives)
 
-/-- 缺渲染诊断:lesson 在 target `t` 下存在无法渲染的 element(ADR-0005/0009)。成立 ⟺
-    存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,级别 warning。 -/
+/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`,
+ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,
+级别 warning。 -/
 def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
   ∃ e ∈ l, ¬ c.covers e.kind t
 
 /-!
-## 要真跑工具才能判的诊断:抽象谓词 + Oracle
+## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
 
-诊断分两类(按 checker 怎么判):有些 checker 自己按工程文件结构就能判(part 路径
-在不在、kind 知不知道、某 kind 在某 target 下有没有被覆盖);有些 checker 自己也判
-不了,得真跑外部工具——typst 编不编得过(要跑 typst 编译器)、数据合不合 schema(要
-跑 schema 校验器)、content 文件齐不齐(要看磁盘)。后者就是 `Oracle` 收口的。
-
-`Oracle` 把这些"得 checker 委托外部工具才能判"的事实建成抽象谓词,真值由 checker 给。
-它不是要在 Lean 里实现 checker,而是把"这几件事 checker 自己算不了、得委托出去"显式
-表达、类型化。它只收 Legal 需要的、得委托外部工具的事实;checker 自己能判的(如
-`renderIgnored`)不进 Oracle。
-
-(这两类 checker 都判得了;但 LLM 两类都判不了——这正是产品里要有个 rule-based
-checker 的理由,见本模块顶部。)
+`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
+要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
+给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
+来自模型外"显式化、类型化。
 -/
 
-/-- checker 委托外部工具才能判的那些事实(ADR-0010)。每个字段是一个谓词,真值由
-    checker 提供。checker 自己按结构就能判的诊断(part 路径、未知 kind)不入此 oracle。 -/
+/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
+实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
 structure Oracle (l : Lesson P) (c : RenderConfig P) where
-  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。含引用解析:源能编译即蕴含其
-      `@ref`、相对 import 全部解析(ADR-0012)。 -/
+  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
+      其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
   compiles : P.TargetId → Prop
   /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/
   dataConforms : Prop
   /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/
   contentFilesPresent : Prop
 
-/-- 合法 lesson(ADR-0010)。合法 ⟺ 检查管线产出零条 error 级诊断。展开为:得委托外部
-    工具的判定(经 `Oracle`)全为真,且每个声明的 target 都编译通过。checker 自己按结构
-    能判的诊断(part 路径、未知 kind)在加载期已判;能走到这步谈合法性意味着那些已过,
-    故此处聚焦 schema/外部工具层。`renderIgnored` 是 warning,不进合取(ADR-0005 种子
-    规则)。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
+/-- **合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。
+
+合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真,
+**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步
+谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被
+`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子
+规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
 def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
   o.dataConforms ∧ o.contentFilesPresent ∧
     (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)

spec/Spec/Courseware/Check/Pipeline.lean

@@ -1,24 +1,26 @@
 import Spec.Courseware.Check.Diagnostic
 
 /-!
-# Pipeline —— 检查管线的阶段与序
+# Pipeline —— checker 检查管线的阶段与序(ADR-0010)
 
-checker 的 `check` 按固定顺序跑五个阶段,逐阶段收集诊断;`compile` 阶段有门控。顺序和
-门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示,这是
-有意的)。每阶段的算法不进 Lean(宪法第 5 条深度上限):只钉阶段、序、门控。
+checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
+顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
+显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
+门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
+`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
 -/
 
 namespace Spec.Courseware
 
-/-- 检查管线的阶段(ADR-0010)。
+/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
 
-- `load` —— 解析 manifest + 各 element.toml。含 `.cph-version` 兼容性判定(ADR-0016:
-  工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。硬失败(无法
-  解析 lesson)则停整条管线。
+- `load` —— 解析 manifest + 各 element.toml。**含 `.cph-version` 兼容性判定**
+  (ADR-0016:工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。
+  硬失败(无法解析 lesson)则**停**整条管线。
 - `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。
 - `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。
-- `compile` —— 跑外部工具的阶段(typst 编译)。门控:仅当前序零 error 才跑。
-- `coverage` —— 语义型 warning(`renderIgnored`);不受门控,总跑。 -/
+- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。
+- `coverage` —— 语义型 warning(`renderIgnored`);**不**受门控,总跑。 -/
 inductive Phase where
   | load
   | structural
@@ -27,8 +29,8 @@ inductive Phase where
   | coverage
 deriving DecidableEq
 
-/-- 管线阶段的执行序(ADR-0010)。`order p` 越小越先跑。序是契约:`compile`(3)排在
-    `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
+/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约:
+`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
 def Phase.order : Phase → Nat
   | .load       => 0
   | .structural => 1
@@ -36,14 +38,15 @@ def Phase.order : Phase → Nat
   | .compile    => 3
   | .coverage   => 4
 
-/-- 某阶段是否受"前序零 error"门控(ADR-0010)。唯 `compile` 受门控:藏在结构/schema 错
-    背后的编译错,在前者修好前不显示——有意降噪。 -/
+/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在
+结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/
 def Phase.gated : Phase → Bool
   | .compile => true
   | _        => false
 
-/-- 管线在 `load` 硬失败时停(ADR-0010)。`load` 拿不到可解析 lesson 时,无 lesson 可喂
-    下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` 门控只跳过自己)。 -/
+/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时,
+无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile`
+门控只跳过自己)。 -/
 def Phase.haltsPipelineOnFailure : Phase → Bool
   | .load => true
   | _     => false

spec/Spec/Courseware/Export.lean

@@ -4,5 +4,5 @@ import Spec.Courseware.Export.Render
 /-!
 # Courseware.Export —— export target = artifact + 有序 typed steps
 
-产物 ADT、build 规格与渲染覆盖。决策出处 ADR-0009 / 0011。
+产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。
 -/

spec/Spec/Courseware/Export/Artifact.lean

@@ -1,22 +1,23 @@
 /-!
-# Artifact —— export target 的产物
+# Artifact —— export target 的产物(ADR-0009 / 0011)
 
-一个 export target 是一次 build,产出一个有类型的产物(ADR-0009、ADR-0011)。产物是
-带字段的 ADT:"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)是不好猜的领域
-语义,要写进字段 + doc,而不是抹成两个空构造子。路径、glob 用 `String` 承载并由 doc
-赋义(它们就是文本),不复刻文件系统类型。
+ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
+钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
+是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
+承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
 -/
 
 namespace Spec.Courseware
 
-/-- export 产物(ADR-0011)。产物形状决定 `cph build` 吐文件还是目录、reduce 怎么折叠
-    (`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题计数器能工作的
-    前提;`fileTree` 每 part 落一文件)。后端、格式仍 OPEN(ADR-0009)。 -/
+/-- export 产物(`PINNED` 带字段 ADT, ADR-0011)。产物形状决定 `cph build` 吐文件还是
+目录、reduce 怎么折叠(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题
+计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式仍 OPEN(ADR-0009)。 -/
 inductive Artifact where
   /-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/
   | singleFile (filepath : String)
-  /-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集(第三方平台归档即此)。
-      用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验完整性。 -/
+  /-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive
+      即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验
+      完整性。 -/
   | fileTree (root : String) (outputs : String)
 
 end Spec.Courseware

spec/Spec/Courseware/Export/Render.lean

@@ -2,89 +2,88 @@ import Spec.Courseware.Model.Primitives
 import Spec.Courseware.Export.Artifact
 
 /-!
-# Render —— export target = artifact + 有序 typed steps
+# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
 
-一个 export target 是一次 build,产出一个有类型的 `Artifact`(ADR-0009)。build 的形状
-是:一个 target = `artifact` + 一串有序的 typed step(ADR-0011)。
+ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
+的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
 
-- `typstCompile template` —— 把模板文件(如 `exports/student.typ`)编译成产物。它是
-  typed 而非裸 shell,因为框架要把 manifest 注入模板(经 `--input manifest=…`),裸
-  字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
-- `shell run` —— 逃生口,给难以声明的步骤。
-- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content
-  叶子,ADR-0015)拼成单文件 markdown 产物。typed 而非裸 `cat`:按 manifest `[[parts]]`
-  顺序读取 + 跳过缺失项 + 写到单文件产物路径,框架自己来比裸 shell 稳。
+- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
+  *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
+  裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
+- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
+- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子,
+  ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 +
+  跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。
 
-渲染覆盖:契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用;渲染的
-"how"住模板里(ADR-0011)。
+**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
+契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
 
-shell step 的执行语义(ADR-0013):`shell` 会被执行,语义是把 `run` 交给平台 shell、以
-工程根为工作目录运行,产物由被调外部工具自己写出(框架不装配内容)。三条边界:
-
-1. opt-in:命令执行只在用户显式 build 一个 shell target 时发生,绝不在 `check` 里跑。
-   `check` 只校验结构,不执行外部工具、不验其产物。
-2. 失败归属:shell step 退出非零是一次 build 过程失败,不是 lesson 的合法性缺陷;因此
-   它不进 `Diagnostic` 的 7 类(那 7 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
-   而由 build 执行层报告。诊断分类保持 7 类不变。
-3. 非-typst target 不过 typst 编译:一个只含 `shell` step 的 target(教具包即此)由
+**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
+`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
+内容)。三条边界是真分歧点,故钉契约:
+1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
+   绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
+2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
+   因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
+   而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。
+3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由
    执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。
 
-assembleMarkdown step 的执行语义(ADR-0015):与 `shell` 同属"非-typst target"。框架
-自己读每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物
-是 markdown,不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,
-`check` 不跑;② 装配失败(如写盘失败、引用图缺失)是 build 过程错误,不入 7 类诊断;
-③ 非-typst target,`check` 的 compile 阶段跳过它。
-
-单文件产物(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),每份
-`slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里,
-ADR-0011),按 `[[parts]]` 顺序拼接(分隔符空行)。自包含:装配器扫描产物里的 `![](rel)`
-图引用,把引用到的本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录
-可独立交付;引用图在工程根缺失属 build 过程错误(不入 7 类)。外部 URL(`http(s)://`、
-`data:`)不复制。结构化 FileTree 产物延后(待 parts 树形重组,ADR-0015 OPEN)。
+**assembleMarkdown step 的执行语义(ADR-0015)。** 与 `shell` 同属"非-typst target":框架 own
+读取每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物是 markdown,
+不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,`check` 不跑;② 装配失败
+(如写盘失败、引用图缺失)是 build-过程错误,不入 6 类诊断;③ 非-typst target,`check` 的 compile
+阶段跳过它。**单文件产物**(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),
+每份 `slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, ADR-0011),
+按 `[[parts]]` 顺序拼接(分隔符空行)。**自包含**:装配器扫描产物里的 `![](rel)` 图引用,把引用到的
+本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录可独立交付;引用图在工程根缺失属
+build-过程错误(不入 6 类)。外部 URL(`http(s)://`/`data:`)不复制。结构化 FileTree 产物延后
+(待 parts 树形重组, ADR-0015 OPEN)。
 -/
 
 namespace Spec.Courseware
 
 variable (P : Primitives)
 
-/-- 一个 build step(ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;`steps` 是 list 因为
-    FileTree、第三方 build 会需多步。不把模板内部、shell 命令的解析结构写进来(实现细节,
-    ADR-0011 OPEN)。 -/
+/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
+`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
+解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
 inductive Step where
   /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
       注入这件事裸 shell 写不出。 -/
   | typstCompile (template : String)
-  /-- shell 逃生口:执行命令 `run`(ADR-0013)。以工程根为 cwd 执行,opt-in(只在显式
-      build 该 target 时跑,`check` 不跑),失败属 build 过程错误而非 lesson 诊断。
-      教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
+  /-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根
+      为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误
+      而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
   | shell (run : String)
   /-- 装配 markdown:按 `[[parts]]` 顺序读取每个 element 的 `field`(markdown content 叶子,
-      ADR-0015),注入课程 h1 后拼接成单文件 markdown 产物,并收集 `![](rel)` 引用的本地图
-      进 build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由
-      框架自己来。非-typst target(`check` 不跑,失败属 build 过程错误不入 7 类诊断)。
-      slides 大纲、逐字稿口播即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
-      ADR-0014)。 -/
+      ADR-0015),注入课程 h1 后拼接成**单文件 markdown** 产物,并收集 `![](rel)` 引用的本地图进
+      build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。
+      **已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。
+      slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
+      ADR-0014 R2)。 -/
   | assembleMarkdown (field : String)
 
-/-- 一个 export target 的 build 规格(ADR-0011:artifact + 有序 steps)。 -/
+/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
 structure TargetSpec where
-  /-- 产物(带字段,ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
+  /-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
   artifact : Artifact
-  /-- 有序 build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
+  /-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
   steps : List Step
-  /-- 覆盖声明:`covers k` 表示此 target 渲染 kind `k`。契约只声明"渲染哪些 kind"
-      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现(ADR-0011)。 -/
+  /-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
+      `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
+      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
   covers : P.KindId → Prop
 
-/-- 渲染配置(ADR-0009/0011)。`spec t = none` 表示 target `t` 未声明(不导出);
-    `some s` 给出其 build 规格。 -/
+/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t`
+未声明(不导出);`some s` 给出其 build 规格。 -/
 structure RenderConfig where
   /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
   spec : P.TargetId → Option (TargetSpec P)
 
-/-- kind `k` 在 target `t` 下被渲染(ADR-0009/0011)。成立 ⟺ `t` 已声明
-    (`spec t = some s`)且 `s.covers k`。为假即"此 kind 在此 target 下不被渲染"——
-    checker 据此报 warning(见 `Diagnostic.renderIgnored`)。 -/
+/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立
+⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不
+被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/
 def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
     (k : P.KindId) (t : P.TargetId) : Prop :=
   match c.spec t with

spec/Spec/Courseware/Model.lean

@@ -7,5 +7,7 @@ import Spec.Courseware.Model.Info
 /-!
 # Courseware.Model —— 工程文件的内容模型
 
-基元、富内容、element、lesson、课时元信息。决策出处 ADR-0005 / 0006 / 0008。
+留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
+(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
+决策出处 ADR-0005 / 0006 / 0008。
 -/

spec/Spec/Courseware/Model/Element.lean

@@ -1,23 +1,24 @@
 import Spec.Courseware.Model.Primitives
 
 /-!
-# Element —— 课程内容的最小单位
+# Element —— 课程内容的原子单位
 
-一个 element = 一个 kind 标签 + 符合该 kind schema 的数据(ADR-0005)。
-用依赖结构编码,使"数据必须匹配 kind"成为类型层面的事实,不是运行时校验。
+ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
+依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
 -/
 
 namespace Spec.Courseware
 
 variable (P : Primitives)
 
-/-- 一个 element 实例(ADR-0005)。data 的类型由 kind 决定,所以没法造出数据和 kind
-    不符的 element——schema 合规由类型保证。逐字稿、重点圈划这类跟具体 kind 强相关
-    的字段,落在该 kind 的 ElementData 里,不放在这个通用结构上。 -/
+/-- element 实例(`PINNED`, ADR-0005)。`data : P.ElementData kind` 由 `kind` 决定——
+无法构造数据与 kind 不符的 element,schema 合规由类型系统保证。ADR-0005 的 (a) 类
+字段(逐字稿、重点圈划)落在具体 kind 的 `ElementData` 内,不出现在此通用结构上;
+交互教具等"重型 kind"在此与例题、定理同构,仅 `kind` 不同,重实现在模型之外。 -/
 structure Element where
-  /-- 这个 element 的 kind。 -/
+  /-- 该 element 的 kind。 -/
   kind : P.KindId
-  /-- 符合 kind schema 的数据,类型随 kind 变。 -/
+  /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/
   data : P.ElementData kind
 
 end Spec.Courseware

spec/Spec/Courseware/Model/Info.lean

@@ -1,54 +1,56 @@
 /-!
-# Info —— 课时元信息:canonical 模型 vs 撰写态
+# Info —— 课时元信息:canonical 模型 vs 撰写态(authoring surface)
 
-`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但作者的
-基数是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
-有序列表,不是单值或可选单值。
+`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的
+基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
+**有序列表**,不是单值或可选单值。
 
-另有一条值得钉的模式:on-disk 的撰写态(用户实际填写的形态)是语法糖——单作者可写
-`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态只活在
-加载边界:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端
-始终是 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与
-`RawInfo`(撰写态)两个结构存在的理由。
+另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
+`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
+边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
+`List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
+(撰写态)两个结构存在的理由。
 -/
 
 namespace Spec.Courseware
 
-/-- 作者的撰写态形式(ADR-0008)。on-disk 单作者可写裸字符串、多作者写数组——填写便利,
-    非语义分歧。此 union 只活在加载边界,经 `RawAuthor.normalize` 折叠后不再出现。 -/
+/-- 作者的**撰写态形式**(`PINNED` 仅填写便利, ADR-0008)。on-disk 单作者可写裸
+字符串、多作者写数组——填写便利,非语义分歧。此 union **只活在加载边界**,经
+`RawAuthor.normalize` 折叠后不再出现。 -/
 inductive RawAuthor where
   /-- 单作者裸字符串 `author = "…"`。 -/
   | one (name : String)
   /-- 多作者数组 `author = ["…", "…"]`。 -/
   | many (names : List String)
 
-/-- raw 作者归一化为有序作者列表(ADR-0008)。单作者 ⇒ 单元素列表;数组 ⇒ 原样。
-    这条钉"canonical 接收端始终是 `List String`"。 -/
+/-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
+⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
 def RawAuthor.normalize : RawAuthor → List String
   | .one n => [n]
   | .many ns => ns
 
-/-- 课时元信息的 canonical 模型(ADR-0008)。`authors` 是有序列表:多人署名第一类,
-    空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,不在此承诺更多。这是系统
-    其余部分唯一所见的形态——author 在此已是列表,不再是"字符串或数组"。 -/
+/-- 课时元信息的 **canonical 模型**(`PINNED` author 为列表, ADR-0008)。`authors` 是
+**有序列表**:多人署名第一类,空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,
+不在此承诺更多。这是系统其余部分唯一所见的形态——author 在此**已**是列表,不再是
+"字符串或数组"。 -/
 structure Info where
   /-- 标题(passthrough 元数据)。 -/
   title : String
-  /-- 作者有序列表(空 = 未署名)。canonical 始终是列表。 -/
+  /-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/
   authors : List String
 
-/-- 撰写态的 `[info]`(ADR-0008)。`author` 用 `RawAuthor`(字符串或数组),缺省即未署名。
-    此结构刻画"为便于填写而存在的 raw 形态",不是模型其余部分流通的形式——它经
-    `RawInfo.toInfo` 归一化为 canonical `Info`。 -/
+/-- 撰写态的 `[info]`(`PINNED` 仅填写便利, ADR-0008)。`author` 用 `RawAuthor`
+(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 raw 形态",
+**不**是模型其余部分流通的形式——它经 `RawInfo.toInfo` 归一化为 canonical `Info`。 -/
 structure RawInfo where
   /-- 标题。 -/
   title : String
   /-- 作者 raw 形式(可选;缺省即未署名)。 -/
   author : Option RawAuthor
 
-/-- raw `[info]` 归一化为 canonical `Info`(ADR-0008)。缺省 author ⇒ 空列表,否则按
-    `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,不泄漏进 `Info`——
-    canonical 接收端恒为 `List String`。 -/
+/-- raw `[info]` 归一化为 canonical `Info`(`PINNED` 加载边界归一化, ADR-0008)。缺省
+author ⇒ 空列表,否则按 `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,
+**不**泄漏进 `Info`——canonical 接收端恒为 `List String`。 -/
 def RawInfo.toInfo (r : RawInfo) : Info :=
   { title := r.title
     authors := (r.author.map RawAuthor.normalize).getD [] }

spec/Spec/Courseware/Model/Lesson.lean

@@ -3,14 +3,14 @@ import Spec.Courseware.Model.Element
 /-!
 # Lesson —— 单节课工程文件
 
-一个工程文件 = 一节课,是 element 实例的有序序列(ADR-0005)。课程、单元不是工程文件,
-而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
+ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
+文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
 -/
 
 namespace Spec.Courseware
 
-/-- 一节课(ADR-0005)。用 `List` 因为 element 的次序承载教学语义(先讲定义再举例, ≠ 反过来)。
-    不建模时长——lesson 是内容编排,不是时间轴(ADR-0005)。 -/
+/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲
+定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/
 abbrev Lesson (P : Primitives) := List (Element P)
 
 end Spec.Courseware

spec/Spec/Courseware/Model/Primitives.lean

@@ -1,26 +1,34 @@
 /-!
-# 基元
+# Primitives —— Courseware 契约的留白基元
 
-课程模型要谈"element、lesson、target 之间的关系",但每个基元本身(element kind
-怎么标识、kind 的数据 schema 长什么样、target 怎么标识)的内部表示是实现的事。
-这里把它们收成一组抽象基元,让模型在它们之上参数化。
-
-契约只钉基元之间的关系;基元内部用什么表示,留给实现。
+课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
+schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
+——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
+实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
+是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
+类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
 -/
 
 namespace Spec.Courseware
 
-/-- 课程模型的一组抽象基元:关系已定,内部表示留给实现(ADR-0005、ADR-0006)。 -/
+/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
 structure Primitives where
-  /-- element kind 的标识。kind 是开放宇宙:stdlib 加第三方都可加,不是封闭枚举
-      (ADR-0005)。表示方式留给实现。 -/
+  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
+      类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
+      封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
   KindId : Type
-  /-- 某 kind 的合法数据类型,以 kind 为索引:`ElementData k` 就是"符合 k 的 schema
-      的数据"。schema 用声明式 JSON Schema,带 content 叶子(ADR-0006);JSON Schema
-      的内部结构是实现细节,不进契约,契约只钉"数据要符合 kind 的 schema"这条关系。 -/
+  /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
+      ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
+      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006
+      钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
+      kind schema"这条关系,故此处仍是抽象类型。 -/
   ElementData : KindId → Type
-  /-- export target 的标识。一个 target 是一次 build,产出对 lesson 的一种投影
-      (讲义、教案、PPT、平台归档等),见 Render。 -/
+  /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
+      build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/
   TargetId : Type
 
+-- 注:原 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层 per-target
+-- 载荷,而由 `Render.TargetSpec.steps` 里 `typstCompile` step 引用的**模板文件**承载;
+-- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。
+
 end Spec.Courseware

spec/Spec/Courseware/Model/RichContent.lean

@@ -1,41 +1,44 @@
 /-!
-# 富内容
+# RichContent —— 富内容(ADR-0006 的 prose 母本)
 
-element schema 的叶子可以是 content 类型:一段源文本,按 format 决定语义
-(ADR-0006、ADR-0015)。
+ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
+按其 **format** 决定语义(ADR-0015)。两种 format:
+- **typst** —— 一段 typst 源,语义取该源作为 module 求值后的 body content(讲义/教案面)。
+- **markdown** —— 一段**原样**的 markdown + KaTeX 源,**不经 typst 求值**(slides 大纲面 / 逐字稿口播面;
+  ADR-0015)。直接以 markdown 撰写**绕开** typst→markdown 的公式转换难题(ADR-0014 R2):公式一开始就是
+  KaTeX 源(`$…$`),没有"把 typst 公式转成 md"这一步。
 
-两种 format:
+关键约束(均 ADR-0006,源自 typst 源码事实):**typst** format 的富内容**不可无主**——typst 的源必须有
+`FileId`,否则 span 脱锚、相对 import 报"cannot access file system from here"。故每段 typst 富内容是 World 里
+的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
+的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。
 
-- typst:一段 typst 源,求值后得到讲义/教案用的内容。
-- markdown:一段 markdown + KaTeX 源,原样保留,不经 typst 求值(slides 大纲、
-  逐字稿口播)。直接用 markdown 写,公式一开始就是 KaTeX(`$…$`),绕开了
-  typst→markdown 的公式转换这个难题(ADR-0014)。
-
-约束:typst 内容必须挂在一个虚拟路径上(原因见 ADR-0006 的考据)。markdown 内容
-不经 typst 求值,但同样用虚拟路径定位,供 markdown 装配按序读取。
-
-本模块只钉两条关系:富内容由一个虚拟路径定位、叶子带 format。typst 的 Content/Module
-内部结构、JSON Schema 形状、format 怎么判别,都是实现细节,不进契约。
+本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
+具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
 -/
 
 namespace Spec.Courseware
 
-/-- 富内容在工程文件里的虚拟路径(ADR-0006)。落盘后是真实相对路径(ADR-0007),
-    这层不承诺,所以 opaque。 -/
+/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
+定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
+(ADR-0007),不在本层承诺,故 opaque。 -/
 opaque VPath : Type
 
-/-- 富内容的 format(ADR-0015)。 -/
+/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值;
+markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/
 inductive ContentFormat where
-  /-- typst 源:求值后得到讲义/教案用的内容。 -/
+  /-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/
   | typst
-  /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides、逐字稿)。 -/
+  /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/
   | markdown
 
-/-- 对一段富内容的引用:它挂在一个虚拟路径上(ADR-0006),带一个 format(ADR-0015)。
-    不建模源文本,也不建模求值出的内容——那是实现的事;这里只钉"富内容由虚拟路径定位
-    + 带 format",作为 ElementData 里 content 叶子的语义锚点。 -/
+/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
+**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
+只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
 structure RichContentRef where
+  /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
   vpath : VPath
+  /-- 该富内容的 format(ADR-0015)。 -/
   format : ContentFormat
 
 end Spec.Courseware

spec/Spec/Courseware/Open.lean

@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
 import Spec.Courseware.Open.Course
 
 /-!
-# Courseware.Open —— 留白骨架
+# Courseware.Open —— 留白骨架(核心关系 OPEN)
 
-题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者都是已提出但
-未决策的分歧点,不臆造,待专门 ADR 落定。
+题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
+但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
 -/

spec/Spec/Courseware/Open/Course.lean

@@ -1,10 +1,10 @@
 /-!
-# Course —— 课程编排(OPEN)
+# Course —— 课程编排(骨架,规则 OPEN)
 
-工程文件的粒度是单节课(ADR-0005);course / 单元不是工程文件,而是 lesson 的编排。
-但"编排"的具体规则没定:有序列表,还是带层级(单元 → 课)的树?lesson 被引用还是被
-包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都 OPEN。
+ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的
+**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
+引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
 
-不臆造编排结构——不建 `Course := List Lesson`(那会偷偷承诺"扁平有序、无层级")。课程
-编排待专门 ADR。本文件不引入任何承诺性声明。
+按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
+"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
 -/

spec/Spec/Courseware/Open/QuestionBank.lean

@@ -1,10 +1,10 @@
 /-!
-# QuestionBank —— 题库(OPEN)
+# QuestionBank —— 题库(骨架,核心关系 OPEN)
 
-题库是与工程文件并列的资产:有自身结构的实体,又是最典型的可复用单元,lesson 会引用它。
-但题库与 element 的关系没定,用户也指出"纯引用可能不够"——element 内联题目数据?lesson
-持指向题库条目的引用?两者并存?
+题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最
+典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
+指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
 
-这是 OPEN 分歧点。不替它选解——不建 `QuestionRef` 也不建内联结构,只在此提出。待专门
-ADR 落定后再填。本文件不引入任何承诺性声明。
+这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
+内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
 -/

spec/Spec/Prelude.lean

@@ -1,23 +1,31 @@
 /-!
 # Prelude —— System 层共享标识符
 
-平台层反复引用一组标识符(项目、run、session、principal)。它们的内部表示从未被决策
-(UUID / 复合键、principal 的子类型学),也不是分歧点,所以收成 opaque 载体
-`Identifiers`,System 各模块在它之上参数化——契约谈得了"锁 owner 是哪个 run"这类关系,
-不对标识符表示作承诺。
+平台层反复引用一组标识符(项目、run、session、principal、chat)。其内部表示从未被决策
+(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
+`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
+**关系**,却不对标识符表示作承诺。
 -/
 
 namespace Spec.System
 
-/-- System 层标识符载体:关系已定,各字段表示 OPEN。 -/
+/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/
 structure Identifiers where
-  /-- 课程项目标识(聚合根;表示 OPEN)。 -/
+  /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
   ProjectId : Type
-  /-- 一次 Claude 任务的标识(锁的 owner、审计主体;表示 OPEN)。 -/
+  /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
+  ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
   RunId : Type
-  /-- 长生命周期 Claude 会话标识(跨多 run 复用,ADR-0002;表示 OPEN)。 -/
+  /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
+  session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
+  记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
   SessionId : Type
-  /-- 权限主体标识(表示 OPEN)。 -/
+  /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
+      子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
   Principal : Type
+  /-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
+      ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
+      类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
+  ChatId : Type
 
 end Spec.System

spec/Spec/System.lean

@@ -1,21 +1,26 @@
+import Spec.System.ProjectGroup
 import Spec.System.Run
 import Spec.System.Lock
+import Spec.System.Memory
 import Spec.System.Permission
+import Spec.System.PermissionGrant
+import Spec.System.Audit
 
 /-!
 # System —— Hub 平台层契约
 
-这一层是产品里的协作与执行平台:项目、飞书群、AgentRun、锁、权限、审计。决策出处
-ADR-0001..0004。
+协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
+(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
+**语义分歧点**:
 
-现状:Hub 还没建、没有业务反馈,所以这一层多为 OPEN 占位,只钉少数已定且有语义分量的
-东西(锁 owner = run、持锁者必为非终止 run、角色三级)。其余等 Hub 真建起来、业务反馈
-来了再细化。做 SaaS 要的权限、LLM API 配置和用量、费用等管理概念,将来也落在这层。
+- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
+- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
+- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
+- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
+- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
+- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
+  (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
+- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
 
-- `Run` —— AgentRun 的终止判定(状态集合 OPEN)。
-- `Lock` —— 锁 owner = run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
-- `Permission` —— read ⊂ edit ⊂ manage 角色三级;force-release 在格外。
-- 审计以 run 为主体记录其生命周期事件;审计记录里装什么未定(OPEN)。
-
-标识符见 `Spec.Prelude`。
+标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。
 -/

spec/Spec/System/Audit.lean

@@ -0,0 +1,22 @@
+import Spec.Prelude
+
+/-!
+# Audit —— 审计日志(有意从简)
+
+likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
+但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
+未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
+"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
+契约的一部分:承诺此处尚无答案、勿填)。
+-/
+
+namespace Spec.System
+
+/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
+关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
+对应 ADR 落定。 -/
+structure AuditEntry (I : Identifiers) where
+  /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
+  run : I.RunId
+
+end Spec.System

spec/Spec/System/Lock.lean

@@ -4,29 +4,34 @@ import Spec.System.Run
 /-!
 # Lock —— 项目锁与排他不变式
 
-ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 owner 是当前 AgentRun(不是
-teacher / chat / session)。这条编码进类型,并钉住核心不变式:持锁者必为非终止 run。
+ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
+(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
+likec4 画不出的语义不变式——**持锁者必为非终止 run**。
 -/
 
 namespace Spec.System
 
 variable (I : Identifiers)
 
-/-- 项目级锁(ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型上编码
-    "lock owner = run":锁不可能被 session / teacher 持有。 -/
+/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
+上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
 structure ProjectAgentLock where
-  /-- 作用域:项目级(ADR-0002)。 -/
+  /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
   scope : I.ProjectId
-  /-- 持有者:一个 run(ADR-0002)。 -/
+  /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
   owner : I.RunId
 
-/-- 锁表:每项目当前持锁 run(ADR-0002 排他性)。`ProjectId → Option RunId` 的结构本身
-    即排他——不可能为同一项目登记两个并发 owner。 -/
+/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
+的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
 def LockTable := I.ProjectId → Option I.RunId
 
-/-- 锁表良构:持锁者必为非终止 run(ADR-0002 核心不变式)。"锁在 run 终止时释放"
-    的等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。 -/
-def LockTable.WellFormed (lt : LockTable I) : Prop :=
-  ∀ p r, lt p = some r → ¬ Terminal I r
+/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
+
+"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
+把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
+必须释放"这个约束;它正是契约相对结构图的增量。 -/
+def LockTable.WellFormed
+    (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
+  ∀ p r, lt p = some r → ¬ (statusOf r).Terminal
 
 end Spec.System

spec/Spec/System/Memory.lean

@@ -0,0 +1,51 @@
+import Spec.Prelude
+
+/-!
+# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
+
+ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
+飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
+"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
+按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
+
+"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
+本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+variable (MessageId CardId : Type)
+
+/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
+列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
+而非消息正文。 -/
+inductive Anchor where
+  /-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
+  | triggerMessage : MessageId → Anchor
+  /-- 某 run 的状态卡片(`PINNED` 类别, ADR-0003 "run id and status card id")。 -/
+  | statusCard : I.RunId → CardId → Anchor
+  /-- 回复锚点(`PINNED` 类别, ADR-0003 "reply anchors")。 -/
+  | reply : MessageId → Anchor
+  /-- 线程锚点(`PINNED` 类别, ADR-0003 "thread anchors")。 -/
+  | thread : MessageId → Anchor
+
+/-- MCP 读上下文请求:由某 run 发起、指向某 chat(`PINNED` 关系, ADR-0003 "Claude calls
+MCP tools to read … through Feishu APIs")。 -/
+structure McpReadRequest where
+  /-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
+  run : I.RunId
+  /-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
+  chat : I.ChatId
+
+/-- 请求获授权:其 chat 必须等于该 run 所属 project 的绑定群(`PINNED` 安全不变式,
+ADR-0003 Consequences "MCP tools must authorize by run/project context; Claude cannot
+pass arbitrary chat ids")。`runProject`/`boundChat` 由平台提供(表示 `OPEN`);本谓词只
+钉死"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id 越权读取。 -/
+def McpReadRequest.Authorized
+    (req : McpReadRequest I)
+    (runProject : I.RunId → Option I.ProjectId)
+    (boundChat : I.ProjectId → Option I.ChatId) : Prop :=
+  ∃ p, runProject req.run = some p ∧ boundChat p = some req.chat
+
+end Spec.System

spec/Spec/System/Permission.lean

@@ -1,23 +1,66 @@
 import Spec.Prelude
 
 /-!
-# Permission —— 协作者角色
+# Permission —— 角色、能力与授权
 
-ADR-0004:权限走"飞书云文档式"——grant(resource + principal + role)与 settings 分离;
-role 取自封闭的 read / edit / manage,且 read ⊂ edit ⊂ manage 累积赋能;强制释放锁是
-admin-only,在 role 体系之外。
-
-本模块钉角色三级与累积关系。具体哪些操作归哪级,见 ADR-0004,待业务反馈细化——所以这里
-不钉操作枚举,也不钉"哪个能力要求哪个 role"的映射。
+ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
+分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
+强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
+role 全部能力"的单调性钉死。
 -/
 
 namespace Spec.System
 
-/-- 协作者角色(ADR-0004:read / edit / manage)。read ⊂ edit ⊂ manage,高 role 含低 role
-    全部能力。强制释放锁不在这套体系里,是 admin-only override,由平台另行判定。 -/
+/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/
 inductive Role where
   | read
   | edit
   | manage
 
+/-- 角色赋能层级(`PINNED` 序, ADR-0004 read⊂edit⊂manage 数值化)。仅服务于
+`Role.le` 与能力推导,不对外承诺"层级就是 `Nat`"。 -/
+def Role.level : Role → Nat
+  | .read => 0
+  | .edit => 1
+  | .manage => 2
+
+/-- 角色偏序:`r₁ ≤ r₂` 即 `r₁` 赋能不强于 `r₂`(`PINNED`, ADR-0004)。 -/
+def Role.le (r₁ r₂ : Role) : Prop := r₁.level ≤ r₂.level
+
+/-- 受 role 调控的操作能力(各项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**——
+这是 ADR 当前点名的能力,不保证穷尽,新增产品操作时可能扩)。注意 force-release
+**不在此列**——它是 admin-only override,见 `RequiresAdmin`。 -/
+inductive Capability where
+  | view
+  | discussComment
+  | editArtifact
+  | triggerAgent
+  | answerChoiceCard
+  | manageCollaborators
+  | projectSettings
+  | groupBinding
+  | normalCancel
+
+/-- 某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 能力展开)。授权判定
+`Role.can` 据此定义,"谁能做什么"只有这一处真相。 -/
+def Capability.requiredRole : Capability → Role
+  | .view => .read
+  | .discussComment | .editArtifact | .triggerAgent | .answerChoiceCard => .edit
+  | .manageCollaborators | .projectSettings | .groupBinding | .normalCancel => .manage
+
+/-- 角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。定义为"`c` 的最低角色 ≤ `r`",
+这一处同时编码了 read⊂edit⊂manage 的累积性。 -/
+def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r
+
+/-- **单调性**:`r₁ ≤ r₂` 且 `r₁` 能做 `c` ⇒ `r₂` 也能(`PINNED` 定理, ADR-0004 累积
+赋能的形式化保证)。证明即偏序传递性,得益于 `can` 按"最低角色阈值"定义。 -/
+theorem Role.can_mono {r₁ r₂ : Role} {c : Capability}
+    (h : r₁.le r₂) (hc : r₁.can c) : r₂.can c :=
+  Nat.le_trans hc h
+
+/-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only
+override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立
+谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/
+def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
+
 end Spec.System

spec/Spec/System/PermissionGrant.lean

@@ -0,0 +1,69 @@
+import Spec.Prelude
+import Spec.System.Permission
+
+/-!
+# PermissionGrant —— 授权与设置(ADR-0004)
+
+ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
+(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
+是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
+力格,本模块补"授权如何挂到资源/主体上"。
+
+principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
+层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
+ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
+须 surface,不得默认。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+variable (ArtifactId Policy : Type)
+
+/-- 受权限调控的资源(`PINNED` 三类, ADR-0004 `resource_type: project | artifact |
+project_group`);每类携带其 id,故 resource_id 由 resource_type 决定(结构无洞)。 -/
+inductive Resource where
+  /-- 课程项目(`PINNED` 类别, ADR-0004)。 -/
+  | project : I.ProjectId → Resource
+  /-- 教研产物(`PINNED` 类别, ADR-0004;id 表示 `OPEN`,语义向 Courseware 半边对齐)。 -/
+  | artifact : ArtifactId → Resource
+  /-- 飞书项目群(`PINNED` 类别, ADR-0004 `project_group`;chat 标识见
+  `Identifiers.ChatId`,绑定见 `ProjectGroup`)。 -/
+  | projectGroup : I.ChatId → Resource
+
+/-- 授权项(`PINNED` 结构, ADR-0004 `PermissionGrant`):把一个 role 授予一个 principal 对
+某个 resource。role 取自 `Permission.Role`(read/edit/manage 累积格)。principal 表示
+`OPEN`(子类型学未定,见 `Identifiers.Principal`)。 -/
+structure PermissionGrant where
+  /-- 被授权的资源(`PINNED`, ADR-0004 `resource_id`)。 -/
+  resource : Resource I ArtifactId
+  /-- 被授权的主体(`PINNED` 字段/`OPEN` 表示, ADR-0004 `principal_id`;user/chat/
+  department/user_group/app 子类型学未定)。 -/
+  principal : I.Principal
+  /-- 授予的角色(`PINNED`, ADR-0004 `role`;read⊂edit⊂manage 见 `Permission.Role`)。 -/
+  role : Role
+
+/-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
+控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
+分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
+值域互异"——值域是实现/后续 ADR 的事。 -/
+structure PermissionSettings where
+  /-- 设置所属资源(`PINNED`, ADR-0004)。 -/
+  resource : Resource I ArtifactId
+  /-- 对外分享策略(`PINNED` 旋钮名, ADR-0004 `external_share_policy`;值域 `OPEN`)。 -/
+  externalShare : Policy
+  /-- 评论策略(`PINNED` 旋钮名, ADR-0004 `comment_policy`;值域 `OPEN`)。 -/
+  comment : Policy
+  /-- 复制/下载策略(`PINNED` 旋钮名, ADR-0004 `copy_download_policy`;值域 `OPEN`)。 -/
+  copyDownload : Policy
+  /-- 协作者管理策略(`PINNED` 旋钮名, ADR-0004 `collaborator_management_policy`;
+  值域 `OPEN`)。 -/
+  collaboratorMgmt : Policy
+  /-- agent 触发策略(`PINNED` 旋钮名, ADR-0004 `agent_trigger_policy`;值域 `OPEN`。与
+  `agentCancel` 分立——"谁能触发"≠"谁能取消",ADR-0004 故意拆开)。 -/
+  agentTrigger : Policy
+  /-- agent 取消策略(`PINNED` 旋钮名, ADR-0004 `agent_cancel_policy`;值域 `OPEN`。与
+  `agentTrigger` 分立,见上)。 -/
+  agentCancel : Policy
+
+end Spec.System

spec/Spec/System/ProjectGroup.lean

@@ -0,0 +1,40 @@
+import Spec.Prelude
+
+/-!
+# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
+
+ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
+owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
+处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
+project↔group 的一对一绑定——likec4 画得出"project has group",画不出"恰好一个、且群
+不持锁"。
+
+**群失效态与绑定快照(`OPEN`, ADR-0001 Consequences):** 群解散/归档/不可达时,
+`GroupBinding` 快照应变为 `none`(解绑、允许 rebind)还是保持 `some` 但指向失效 chat
+(悬挂、待管理员干预)未决策。ADR-0001 已点名 "rebinding or group archival needs
+explicit product rules";本模块只刻画健康态 1:1 不变式,不臆造失效态语义。实现遇到
+群解散必须 surface,不得默认任一方。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
+**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
+structure ProjectGroup where
+  /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
+  group";chat 标识见 `Identifiers.ChatId`)。 -/
+  chat : I.ChatId
+
+/-- 项目↔群绑定表(`PINNED` 每项目至多一个群, ADR-0001)。`ProjectId → Option ChatId` 的
+结构本身即"一个 project 至多绑一个群"(由 `Option` 自带);良构补另一半——单射。 -/
+def GroupBinding := I.ProjectId → Option I.ChatId
+
+/-- 绑定良构:**单射**——不同 project 不绑同一 chat(`PINNED` 1:1 的另一半, ADR-0001)。
+"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个 project"。群
+rebinding/archival 是生命周期事件(ADR-0001 Consequences),不在本快照不变式内。 -/
+def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
+  ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
+
+end Spec.System

spec/Spec/System/Run.lean

@@ -1,22 +1,28 @@
-import Spec.Prelude
-
 /-!
-# Run —— AgentRun 的终止判定
+# Run —— AgentRun 状态机
 
-一次 `@Claude` 创建一个 AgentRun(ADR-0001),它在终止时释放项目锁(ADR-0002)。
-
-run 的具体状态集合没定(OPEN):ADR-0001..0003 列了一些状态名,但从未声明"状态恰好
-这些",实现若需新状态(如 pending)要提出来,不要默认已穷尽。所以这里不钉状态枚举,
-只钉一条契约需要的事实:一个 run 是否处于终止态。终止态由实现判定(状态集合本身未定,
-没法在契约里算)。
+一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
+合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
+判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
 -/
 
 namespace Spec.System
 
-variable (I : Identifiers)
+/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`**
+——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认
+本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
+inductive RunState where
+  | active
+  | waitingForUser
+  | completed
+  | failed
+  | timedOut
+  | canceled
 
-/-- run 是否处于终止态(ADR-0002)。真值由实现给——状态集合未定(OPEN),故此处不钉
-    具体状态名,只钉"存在终止与否的判定"。锁在 run 终止时释放(见 `Lock`)。 -/
-opaque Terminal : I.RunId → Prop
+/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled
+时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/
+def RunState.Terminal : RunState → Prop
+  | .completed | .failed | .timedOut | .canceled => True
+  | .active | .waitingForUser => False
 
 end Spec.System