docs(hub): document HUB_DEV_LOGIN_BYPASS dev login in database README

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

.gitea/workflows/checker-check.yml

@@ -1,12 +1,12 @@
 name: checker check
 
 # Builds and lints the Rust implementation crates under crates/ (the rule-based
-# checker that "stands in Lean's position" at product runtime).
+# lesson checker).
 #
-# Like spec-check, this is an INTERNAL gate on the implementation's own health
+# This is an INTERNAL gate on the implementation's own health
-# (does it build, pass its tests, satisfy clippy + rustfmt?). It is NOT a
+# (does it build, pass its tests, satisfy clippy + rustfmt?). There is no
-# spec-to-implementation conformance gate — implementations align to the Lean
+# decision-to-implementation conformance gate — implementations align to the
-# contract by human review, not by CI. See the repo README.
+# ADRs by human review, not by CI. See the repo README.
 
 on:
   push:

.gitea/workflows/hub-check.yml

@@ -1,8 +1,8 @@
 name: hub check
 
 # Builds, type-checks, and tests the Hub TS package under hub/.
-# The Hub is the Feishu-group collaboration + agent runtime half
+# The Hub is the Feishu-group collaboration + agent runtime half.
-# (spec/System implementation). This is an INTERNAL gate on the Hub's own
+# This is an INTERNAL gate on the Hub's own
 # health, like checker-check is for the Rust half.
 
 on:

.gitea/workflows/spec-check.yml

@@ -1,20 +0,0 @@
-name: spec check
-
-# Builds the Lean semantic master spec under spec/.
-# This is an INTERNAL well-formedness gate (does the contract type-check?),
-# NOT a spec-to-implementation conformance gate — implementations align to the
-# contract by human review, not by CI. See repo README.
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  spec-check:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
-        with:
-          lake-package-directory: spec

.gitignore

@@ -1,7 +1,3 @@
-# Lean / Lake build artifacts (spec/ has its own .gitignore too)
-.lake/
-**/.lake/
-
 # Rust / Cargo build artifacts (repo-wide cargo workspace at root)
 /target
 **/*.pdf

.scratch/saas-production-readiness/issues/05-define-abuse-capacity-controls.md

@@ -29,7 +29,7 @@ workload brakes.
 
 The full current-state inventory, accepted behavior, and release evidence are
 recorded in [Initial abuse and capacity controls](../assets/initial-abuse-capacity-controls.md),
-with the durable decision in ADR-0022 and `Spec.System.Capacity`. Numerical
+with the durable decision in ADR-0022. Numerical
 ceilings remain open until production-like calibration.
 
 The implementation frontier is:

.scratch/saas-production-readiness/issues/08-prove-production-release-gate.md

@@ -7,6 +7,6 @@ Blocked by: 01, 02, 03, 04, 05, 06, 07, 09, 10, 11, 12, 13, 14, 15, 16, 17, 18,
 ## Question
 
 After the readiness investigations and resulting fixes are resolved, can one
-repeatable release procedure prove build/test/spec health, deploy a clean
+repeatable release procedure prove build/test health, deploy a clean
 production-like environment, exercise critical tenant and agent journeys,
 verify observability and recovery, and either roll forward or roll back safely?

.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md

@@ -8,7 +8,7 @@ Blocked by: 04
 
 Separate or unify run-bound audit entries, pre-run security/permission events,
 structured messages, and operational recovery events without weakening
-`Spec.System.Audit`'s pinned AuditEntry-to-run relation. Decide durability,
+the pinned AuditEntry-to-run relation. Decide durability,
 failure, retention, and query semantics; then enforce referential integrity and
 observable/recoverable writes instead of silently swallowing lost evidence.
 Do not merge these customer Project/Run records with ADR-0023's already-decided

.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md

@@ -40,9 +40,7 @@ an off-host recovery key, an incident and reason, and issues only an expiring
 Emergency Platform Grant.
 
 The complete accepted decision and implementation divergences are in
-[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md).
+[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md),
-The pinned semantic invariants are in
-[`Spec.System.PlatformAdministration`](../../../spec/Spec/System/PlatformAdministration.lean),
 and the canonical terms are in [`CONTEXT.md`](../../../CONTEXT.md).
 
 Exact numeric session/invitation/step-up limits and browser mechanics remain

AGENTS.md

@@ -1,29 +1,25 @@
 # AGENTS.md —— agent 操作手册(全 repo)
 
-本 repo 是 monorepo。先读根 `README.md` 的"宪法"5 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
+本 repo 是 monorepo。先读根 `README.md` 的"宪法"4 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
 
 ## 这个 repo 是什么
 
-- `spec/` 是一份**人机共识的契约**(Lean 语义母本),是产品语义的上游参照。
+- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。
-- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。
 - `hub/` 的平台层按 SaaS 形态演进:`Organization` 是 tenant root;`Project`/`Team`
-  必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020 / `Spec.System.Organization`)。
+  必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020)。
 - org 后台 project explorer 里 `Folder` 是透明组织节点,不是权限资源;project 仍是权限边界。
-  普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021 /
+  普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。
-  `Spec.System.ProjectWorkspace`)。
 - 每个 org 自选 BYOK 或平台托管 model provider connection;平台托管也必须是该 org
-  独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021 /
+  独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021)。
-  `Spec.System.Organization`)。
 - Feishu/provider secret 使用本地版本化 master-key keyring 的信封加密;生产由 systemd
   credential 注入,运行时只允许显式 org/project scope 的 fail-closed resolver,不得回退
   process-global credential;Agent child 只接收 run-scoped loopback proxy capability,
-  不接收 org provider credential(见 ADR-0024 / `Spec.System.Organization`)。
+  不接收 org provider credential(见 ADR-0024)。
 - 生产容量按不可突破的 platform ceiling 与 org 可下调 policy 分层;有效限制取两者较低值。
-  Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022 /
+  Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022)。
-  `Spec.System.Capacity`)。
 - 平台管理员只通过独立的 platform-owned 飞书应用与可撤销 Platform Session 认证,不复用
   客户 `User`/org membership;平台写操作与 append-only audit 同事务,break-glass 只走
-  双因子的离线恢复流程(见 ADR-0023 / `Spec.System.PlatformAdministration`)。
+  双因子的离线恢复流程(见 ADR-0023)。
 - 受控 alpha 暂采用一 Organization 一具名 systemd Silo:独立 database role/database、
   service identity、workspace、keyring 与 Feishu/provider connection；进程必须由
   `HUB_SILO_ORGANIZATION_ID` fail-closed 绑定唯一 org，平台后台不开放。共享 SaaS
@@ -44,12 +40,12 @@
 
 ## 纪律
 
-1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。契约里 prose doc 注释是语义的唯一权威来源;契约没写的,就是没定的。
+1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。ADR 与 `CONTEXT.md` 是语义的唯一权威来源;没写的,就是没定的。
 
-2. **凡契约未写明者,不得假设。** 遇到标了 `OPEN` 的地方,或契约根本没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
+2. **凡 ADR 未写明者,不得假设。** 遇到没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
 
-3. **改 `spec/` 必须保持其 `lake build` 通过。** 在 `spec/` 目录下跑 `lake build`。新增声明必须带 `/-- … -/` doc 注释和恰当标签(`PINNED` / `OPEN` / `ADR-NNNN`)。规范见 `spec/README.md`。不准用 `sorry` 把 build 糊绿。
+3. **新语义决策进 ADR。** 跨部件的语义分歧点按编号顺延新增 `docs/adr/NNNN-*.md`;代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。已有 ADR 正文不改写历史——推翻旧决策就写新 ADR 标记 supersede。
 
-4. **实现向契约对齐;偏离必须 surface。** 没有 CI gate 替你把关 spec↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与契约不一致时,报告它,不要默默让其中一边将就另一边。
+4. **实现向 ADR 对齐;偏离必须 surface。** 没有 CI gate 替你把关 ADR↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与决策不一致时,报告它,不要默默让其中一边将就另一边。
 
 5. **写操作谨慎。** 线上操作、git 写操作前与开发者确认(这是开发者的全局偏好)。

CLAUDE.md

@@ -1,25 +1,23 @@
 # CLAUDE.md —— agent 操作手册(全 repo)
 
-本 repo 是 monorepo。先读根 `README.md` 的"宪法"5 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
+本 repo 是 monorepo。先读根 `README.md` 的"宪法"4 条,那是一切工作的前提。本文件是给在这里干活的 coding agent 的纪律。
 
 ## 这个 repo 是什么
 
-- `spec/` 是一份**人机共识的契约**(Lean 语义母本),是产品语义的上游参照。
+- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。
-- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。
 - `hub/` 的平台层按 SaaS 形态演进:`Organization` 是 tenant root;`Project`/`Team`
-  必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020 / `Spec.System.Organization`)。
+  必须归属 org,TEAM→PROJECT 授权不得跨 org(见 ADR-0020)。
 - org 后台 project explorer 里 `Folder` 是透明组织节点,不是权限资源;project 仍是权限边界。
-  普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021 /
+  普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。
-  `Spec.System.ProjectWorkspace`)。
 
 ## 纪律
 
-1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。契约里 prose doc 注释是语义的唯一权威来源;契约没写的,就是没定的。
+1. **不得用预训练先验脑补本领域。** 这个领域很新,你没有相关先验。ADR 与 `CONTEXT.md` 是语义的唯一权威来源;没写的,就是没定的。
 
-2. **凡契约未写明者,不得假设。** 遇到标了 `OPEN` 的地方,或契约根本没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
+2. **凡 ADR 未写明者,不得假设。** 遇到没覆盖的地方,**显式 surface 出来**让开发者决定,绝不擅自替它选一个解。
 
-3. **改 `spec/` 必须保持其 `lake build` 通过。** 在 `spec/` 目录下跑 `lake build`。新增声明必须带 `/-- … -/` doc 注释和恰当标签(`PINNED` / `OPEN` / `ADR-NNNN`)。规范见 `spec/README.md`。不准用 `sorry` 把 build 糊绿。
+3. **新语义决策进 ADR。** 跨部件的语义分歧点按编号顺延新增 `docs/adr/NNNN-*.md`;代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。已有 ADR 正文不改写历史——推翻旧决策就写新 ADR 标记 supersede。
 
-4. **实现向契约对齐;偏离必须 surface。** 没有 CI gate 替你把关 spec↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与契约不一致时,报告它,不要默默让其中一边将就另一边。
+4. **实现向 ADR 对齐;偏离必须 surface。** 没有 CI gate 替你把关 ADR↔实现的一致性(见宪法第 2 条)——这道对齐靠 review 和你巡逻 diff。发现实现与决策不一致时,报告它,不要默默让其中一边将就另一边。
 
 5. **写操作谨慎。** 线上操作、git 写操作前与开发者确认(这是开发者的全局偏好)。

README.md

@@ -2,7 +2,7 @@
 
 教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
 
-这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
+这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`docs/adr/` 是系统级决策的唯一权威来源,代码注释把关键不变量锚到 ADR 编号,可 grep。**
 
 ## 安装 `cph` 命令行
 
@@ -33,47 +33,40 @@ cph completions zsh > ~/.zfunc/_cph        # 或 bash/fish/powershell/elvish
 ```
 README.md          ← 本文件:总览 + 宪法(下面 5 条)
 CLAUDE.md          ← 全局 agent 操作手册(管整个 repo)
-docs/adr/          ← 系统级架构决策记录(跨部件,被 spec 契约引用)
+docs/adr/          ← 系统级架构决策记录(跨部件,决策的唯一权威来源)
-spec/              ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
+CONTEXT.md         ← 平台语言词汇表(术语与禁用说法)
 Cargo.toml         ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
-crates/            ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
+crates/            ← 实现:rule-based checker(语义由 ADR 锚定)。见 crates/README.md
   cph-diag / cph-model / cph-schema / cph-typst   ← 可复用基础(模型/校验/typst 引擎)
   cph-check / cph-cli                             ← checker 本体 + `cph` 命令行
-render/            ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
+render/            ← typst 渲染包 cph-render(checker 的渲染后端,ADR-0005)
 examples/          ← 样例工程文件(如 TH-141),流水线的真实输入
 hub/              ← SaaS Hub:飞书协作、org 管理、agent runtime 与生产部署
-(exporter/ …)     ← 将来的其他部件,平级于 spec/
+(exporter/ …)     ← 将来的其他部件,平级于 crates/
 ```
 
-`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
 实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被
 未来部件(如 exporter)复用,而非各自重造。
 
 ## 宪法
 
-这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
+这 4 条是本仓库的协作约定,是一切工作的前提。
 
-1. **角色 —— Lean 是研发侧的上游参照。**
+1. **角色 —— ADR 是决策真相。**
-   `spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
+   跨部件的语义决策只记录在 `docs/adr/`,一份决策一份 ADR,编号顺延、正文不改写历史。代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。没有第二份权威文档。
 
-2. **对齐机制 —— Lean 只做上游参照。**
+2. **对齐机制 —— 人肉承载,无机器兜底。**
-   不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
+   CI 只验各部件自身良构(build / test / clippy),**没有**决策↔实现的一致性 gate。实现对齐 ADR,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。发现漂移,报告它,不要默默让其中一边将就另一边。
-   (CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
 
-3. **资产性 —— 由 review 纪律承载,无机器兜底。**
+3. **形态 —— 自包含。**
-   这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
+   凡 ADR 未明文规定的,开发者与 agent 双方都不该假设;遇到没覆盖的地方,**显式 surface** 出来让开发者决定。
 
-4. **形态 —— 它是人机共识的契约。**
+4. **深度判据 —— 只收录分歧点。**
-   契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
+   一条语义该不该写进 ADR,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进 ADR;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
-
+   深度上限是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
-5. **深度判据 —— 只收录分歧点。**
-   一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
-   深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
 
 ## CI
 
-`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。
-
 Rust checker 的本地与 CI 工具链由根 `rust-toolchain.toml` 固定;`.gitea/workflows/checker-check.yml`
 必须安装同一精确版本并执行 `cargo fmt --all --check`、Clippy `-D warnings` 与 workspace
 全测试。升级 Rust 时这两处必须在同一提交更新并通过完整 checker gate。

crates/README.md

@@ -1,7 +1,8 @@
 # crates/
 
-These crates implement the rule-based lesson checker that aligns to the
+These crates implement the rule-based lesson checker whose semantics are
-semantic master in `spec/`: it reads an engineering-file (one lesson, ADR-0005)
+pinned by the ADRs in `docs/adr/`: it reads an engineering-file (one lesson,
+ADR-0005)
 laid out per ADR-0008 (declarative `manifest.toml` + per-element
 `element.toml`), validates structure and content, and emits diagnostics.
 `cph-diag` (the shared diagnostic vocabulary), `cph-model` (the ADR-0008 loader),

crates/cph-check/src/lib.rs

@@ -19,13 +19,11 @@ const DEFAULT_TARGET: &str = "student";
 
 /// Severity of the render-coverage ("element ignored under a target") diagnostic.
 ///
-/// **PINNED to `warning` by the contract.** Mirrors the Lean master's
+/// **PINNED to `warning` by ADR-0005:** when a
-/// `Spec.Courseware.renderIgnoredSeverity : Severity := .warning`
-/// (`spec/Spec/Courseware/Check/Diagnostic.lean`), itself citing ADR-0005: when a
 /// `(kind, target)` pair has no render rule the checker reports that the element
 /// is ignored under that target and **does not block the export**. Naming the
-/// severity as a const makes "it is a warning, not an error" a greppable,
+/// severity as a const makes "it is a warning, not an error" a greppable
-/// alignable fact rather than an inline literal.
+/// fact rather than an inline literal.
 const RENDER_IGNORED_SEVERITY: Severity = Severity::Warning;
 
 /// The result of running [`check`] (or the check phases of [`build`]).
@@ -57,12 +55,12 @@ impl CheckReport {
 
     /// Whether any collected diagnostic is `Error`-severity.
     ///
-    /// **Legality decision (spec alignment).** `!has_errors()` is the
+    /// **Legality decision (ADR-0010).** `!has_errors()` decides lesson
-    /// implementation of `Spec.Courseware.Legal` (`spec/Spec/Courseware/Check/Diagnostic.lean`):
+    /// legality: a lesson is *legal* iff its diagnostics contain no error-level
-    /// a lesson is *legal* iff its diagnostics contain no error-level diagnostic
+    /// diagnostic (warnings are non-blocking — see `Severity`). There is no CI
-    /// (warnings are non-blocking — see `Severity` / ADR-0010). There is no CI
+    /// gate enforcing ADR↔implementation alignment (repo constitution); it is
-    /// gate enforcing this alignment (repo constitution); it is kept greppable
+    /// kept greppable here so a reviewer can tie the orchestrator's gate to
-    /// here so a reviewer can tie the orchestrator's gate to the Lean master.
+    /// the ADR.
     pub fn has_errors(&self) -> bool {
         self.diagnostics
             .iter()

crates/cph-diag/src/lib.rs

@@ -2,7 +2,7 @@
 //!
 //! Every other crate in the workspace depends on these types to report
 //! problems. The vocabulary is intentionally small and stable: a [`Severity`]
-//! (mirroring the Lean master), a closed set of machine-stable [`DiagCode`]s, an
+//! (two-valued, ADR-0010), a closed set of machine-stable [`DiagCode`]s, an
 //! optional [`SourceSpan`] pointing back at the offending source, and a
 //! [`Diagnostic`] tying them together with a human message and a fix hint.
 //!
@@ -17,32 +17,27 @@ use serde::Serialize;
 
 /// Severity of a diagnostic.
 ///
-/// **Mirrors `Spec.Courseware.Diagnostic.Severity`** in the Lean semantic
+/// **Pinned by ADR-0005 / ADR-0010: exactly two values.**
-/// master (`spec/Spec/Courseware/Check/Diagnostic.lean`), whose definition is
-/// exactly:
 ///
 /// ```text
-/// inductive Severity where
+/// warning | error
-///   | warning
-///   | error
 /// ```
 ///
-/// This two-valued shape is a **contract decision**, not an accident: the Lean
+/// This two-valued shape is a **contract decision**, not an accident: the
-/// module pins `Severity` to exactly `warning | error` and states the finer
+/// finer levels (`info` / `hint` / `note`) are deliberately undecided, so we
-/// levels (`info` / `hint` / `note`) are deliberately undecided. We therefore
 /// do **not** add an info/note level here. `error` blocks (the artifact is
 /// invalid); `warning` does not block (the artifact still exports, but with
 /// loss / an ignored element — e.g. ADR-0005's "missing render ⇒ warning").
 ///
-/// There is no CI gate enforcing this alignment (see the repo constitution);
+/// There is no CI gate enforcing ADR↔implementation alignment (see the repo
-/// it is maintained by review, which is why this correspondence is documented
+/// constitution); it is maintained by review, which is why the decision is
-/// here rather than only in the spec.
+/// documented here rather than only in the ADR.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
 pub enum Severity {
     /// Non-blocking: the artifact still exports, but is lossy / has an ignored
-    /// element. Mirrors Lean `Severity.warning`.
+    /// element. ADR-0010 `warning`.
     Warning,
-    /// Blocking: the artifact is invalid. Mirrors Lean `Severity.error`.
+    /// Blocking: the artifact is invalid. ADR-0010 `error`.
     Error,
 }
 

crates/cph-model/src/lib.rs

@@ -3,9 +3,7 @@
 //! This crate is the **loader**, not the full checker. It reads
 //! `<root>/manifest.toml` (project / info / ordered `[[parts]]` / declared
 //! `[targets.*]`) and each part's `<root>/<path>/element.toml`, and produces an
-//! ordered [`Lesson`] — mirroring the Lean master's `Lesson = List (Element P)`
+//! ordered [`Lesson`], where the order of `parts` carries teaching semantics.
-//! (`spec/Spec/Courseware/Model/Lesson.lean`), where the order of `parts` carries
-//! teaching semantics.
 //!
 //! Scope boundaries (deliberately staying in lane):
 //! - It validates **structure** only: manifest shape, element.toml shape, and
@@ -23,7 +21,7 @@ use serde::{Deserialize, Serialize};
 
 /// An ordered, in-memory lesson loaded from an engineering file.
 ///
-/// Mirrors the Lean master's `Lesson = List (Element P)`: `parts` is an ordered
+/// `parts` is an ordered
 /// `Vec`, and that order is the lesson's order (ADR-0008 §"the lesson manifest
 /// is declarative" — the `[[parts]]` array order is the single source of truth).
 #[derive(Debug, Clone, PartialEq, Serialize)]
@@ -86,9 +84,8 @@ pub struct TargetConfig {
     /// with template `exports/<name>.typ` when no `[[steps]]` are given.
     pub steps: Vec<Step>,
     /// The **render-coverage declaration**: which element kinds this target
-    /// renders. Realizes `Spec.Courseware.TargetSpec.covers : KindId → Prop`
+    /// renders. Realizes ADR-0011's "render
-    /// (`spec/Spec/Courseware/Export/Render.lean`) and ADR-0011's "render
+    /// coverage is a declaration, not a payload": the declaration keeps *which
-    /// coverage is a declaration, not a payload": the contract keeps *which
     /// kinds a target renders* (used by the `renderIgnored` seed diagnostic),
     /// while the rendering "how" lives in the template/steps.
     ///
@@ -102,13 +99,10 @@ pub struct TargetConfig {
 
 /// The artifact an export target produces (ADR-0009/0011).
 ///
-/// **Mirrors `Spec.Courseware.Artifact`** in the Lean semantic master
+/// **Pinned by ADR-0011** as an ADT with fields:
-/// (`spec/Spec/Courseware/Export/Artifact.lean`), whose definition is exactly:
 ///
 /// ```text
-/// inductive Artifact where
+/// Artifact = singleFile (filepath) | fileTree (root, outputs)
-///   | singleFile (filepath : String)
-///   | fileTree (root : String) (outputs : String)
 /// ```
 ///
 /// ADR-0011 pinned the artifact as an ADT **with fields**: "what the product
@@ -120,20 +114,20 @@ pub struct TargetConfig {
 /// `"single-file"` → [`Artifact::SingleFile`], `"file-tree"` →
 /// [`Artifact::FileTree`].
 ///
-/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing this
+/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing ADR↔
-/// alignment (see the repo constitution) — it is maintained by review, which is
+/// implementation alignment (see the repo constitution) — it is maintained by
-/// why the correspondence is documented here.
+/// review, which is why the decision is documented here.
 #[derive(Debug, Clone, PartialEq, Eq, Serialize)]
 pub enum Artifact {
     /// One bundled document landing at `filepath` (relative to the engineering
-    /// root). Mirrors Lean `Artifact.singleFile`. The default artifact shape.
+    /// root). ADR-0011 `singleFile`. The default artifact shape.
     SingleFile {
         /// Where the single product is written (relative to the engineering
         /// root), e.g. `build/student.pdf`.
         filepath: PathBuf,
     },
-    /// A set of files under `root` matching the `outputs` glob. Mirrors Lean
+    /// A set of files under `root` matching the `outputs` glob. ADR-0011
-    /// `Artifact.fileTree`.
+    /// `fileTree`.
     FileTree {
         /// The output directory (relative to the engineering root).
         root: PathBuf,
@@ -156,14 +150,10 @@ impl Artifact {
 
 /// One typed build step (ADR-0011).
 ///
-/// **Mirrors `Spec.Courseware.Step`** in the Lean semantic master
+/// **Pinned by ADR-0011** as an ADT:
-/// (`spec/Spec/Courseware/Export/Render.lean`), whose definition is exactly:
 ///
 /// ```text
-/// inductive Step where
+/// Step = typstCompile (template) | shell (run) | assembleMarkdown (field)
-///   | typstCompile (template : String)
-///   | shell (run : String)
-///   | assembleMarkdown (field : String)
 /// ```
 ///
 /// A step is a *typed* operation (extensible): `TypstCompile` compiles a
@@ -183,20 +173,20 @@ impl Artifact {
 #[derive(Debug, Clone, PartialEq, Eq, Serialize)]
 pub enum Step {
     /// Compile a template file (relative to the engineering root) into the
-    /// artifact; the framework injects the manifest. Mirrors Lean
+    /// artifact; the framework injects the manifest. ADR-0011
-    /// `Step.typstCompile`.
+    /// `typstCompile`.
     TypstCompile {
         /// The template file to compile as main, e.g. `exports/student.typ`.
         template: PathBuf,
     },
-    /// Run a shell command — the escape hatch. Mirrors Lean `Step.shell`.
+    /// Run a shell command — the escape hatch. ADR-0011 `shell`.
     Shell {
         /// The command line to run.
         run: String,
     },
     /// Assemble a single-file markdown deliverable by concatenating each
-    /// element's `field` markdown content file in `[[parts]]` order. Mirrors
+    /// element's `field` markdown content file in `[[parts]]` order. ADR-0011
-    /// Lean `Step.assembleMarkdown` (ADR-0015). Not a typst build — the
+    /// `assembleMarkdown` (ADR-0015). Not a typst build — the
     /// framework owns the read/concatenate/write itself.
     AssembleMarkdown {
         /// The per-element markdown content field to assemble (e.g. `slides`,
@@ -226,12 +216,11 @@ pub struct Project {
 
 /// `[info]` table (passed through to render targets verbatim).
 ///
-/// **Mirrors `Spec.Courseware.Info`** in the Lean semantic master
+/// The *canonical* model whose
-/// (`spec/Spec/Courseware/Model/Info.lean`): the *canonical* model whose
 /// `authors` is always a list. The authoring-surface form (string-or-array
 /// `author`) is the separate [`RawInfo`] / [`RawAuthor`], normalized into this
-/// at the load boundary — mirroring the Lean `RawInfo` / `RawAuthor` split. No
+/// at the load boundary. No
-/// CI gate enforces this alignment (repo constitution); it is kept greppable.
+/// CI gate enforces ADR↔implementation alignment (repo constitution); it is kept greppable.
 #[derive(Debug, Clone, PartialEq, Eq, Serialize)]
 pub struct Info {
     /// Lesson title.
@@ -240,7 +229,6 @@ pub struct Info {
     /// so this is a list, not a single name. Empty when `[info]` declares no
     /// `author`. The on-disk `author` accepts either a bare string (one author)
     /// or an array of strings (see [`RawAuthor`]); both load into this `Vec`.
-    /// Mirrors Lean `Info.authors : List String`.
     pub authors: Vec<String>,
 }
 
@@ -290,8 +278,7 @@ struct RawProject {
     name: String,
 }
 
-/// The authoring-surface `[info]` (mirrors Lean `RawInfo` in
+/// The authoring-surface `[info]`: the raw form that exists for
-/// `spec/Spec/Courseware/Model/Info.lean`): the raw form that exists for
 /// fill-in convenience, normalized into the canonical [`Info`] at the load
 /// boundary. Not the form the rest of the model traffics in.
 #[derive(Debug, Deserialize)]
@@ -301,7 +288,7 @@ struct RawInfo {
 }
 
 /// On-disk `author`: either a single name (`author = "…"`) or a list
-/// (`author = ["…", "…"]`). Mirrors Lean `RawAuthor`: a fill-in convenience whose
+/// (`author = ["…", "…"]`). A fill-in convenience whose
 /// string-or-array union lives **only** at the load boundary — [`RawAuthor::into_vec`]
 /// folds it into the canonical [`Info::authors`] `Vec`, after which it never appears.
 #[derive(Debug, Deserialize)]
@@ -312,7 +299,7 @@ enum RawAuthor {
 }
 
 impl RawAuthor {
-    /// Flatten to the ordered author list (Lean `RawAuthor.normalize`): a single
+    /// Flatten to the ordered author list: a single
     /// name becomes a one-element list; a list passes through verbatim.
     fn into_vec(self) -> Vec<String> {
         match self {

docs/para-26071100-feishu-setup.md

@@ -32,7 +32,7 @@ App ID 通常以 `cli_` 开头，可以写入交付单。App Secret 必须通过
 | 接收群聊中 @ 机器人的消息 | `im:message.group_at_msg:readonly` |
 | 以应用身份发送消息 | `im:message:send_as_bot` |
 | 读取触发消息和线程上下文 | `im:message:readonly` |
-| 获取与上传图片或文件 | `im:resource` |
+| 获取消息中的图片/文件，并向飞书上传图片或文件（含 Agent 回答中的图片发送） | `im:resource` |
 | 添加、删除消息表情回复 | `im:message.reactions:write_only` |
 | 获取用户基本信息 | `contact:user.base:readonly` |
 | 获取用户基本资料 | `contact:user.basic_profile:readonly` |
@@ -66,6 +66,9 @@ Educraft 机器人以应用身份调用上述 API，因此这些 scope 全部放
 
 如果 API 调试台提示缺少更细粒度权限，请把错误提示和发生时间截图给部署人员。不要自行开通通讯录全量读取等超出本表的权限。
 
+说明：`im:resource` 既用于下载用户发来的图片/文件，也用于 Agent 回复时把本地或远程图片上传为飞书 `image_key` 后嵌入消息卡片。缺少该权限时，带图回答会发送失败或降级为无图文本。已开通该 scope 的存量应用一般无需新增权限，但若权限尚未随最新版本发布，请创建新版本并审核发布。
+
+
 ## 4. 配置事件与卡片回调
 
 进入“事件与回调”。

hub/.gitignore

@@ -5,6 +5,9 @@ dist/
 .env.*
 !.env.example
 .secrets/
+.dev-keyring.json
+.dev-workspaces/
+.dev-skills/
 admin-web/node_modules/
 admin-web/build/
 admin-web/.svelte-kit/

hub/admin-web/src/lib/components/FolderTree.svelte

@@ -33,7 +33,7 @@
 <div class="space-y-0.5">
 	{#each childProjects as p (p.id)}
 		<a
-			href={`/admin/org/${slug}/projects/${p.id}`}
+			href={`/admin/projects/${p.id}`}
 			class="flex items-center gap-2.5 px-3 py-2.5 text-sm transition hover:bg-surface-100"
 		>
 			<span class="flex h-7 w-7 items-center justify-center border border-primary-200 bg-primary-50 text-primary-700">

hub/admin-web/src/lib/org.ts

@@ -0,0 +1,40 @@
+import type { MeResponse, OrgMembership } from './api';
+
+/** Alpha Silo host prefix: <slug>.educraft[.dev].… */
+export function hostOrgSlug(hostname: string = typeof window !== 'undefined' ? window.location.hostname : ''): string | null {
+	const host = hostname.toLowerCase();
+	const m = host.match(/^([a-z0-9](?:[a-z0-9-]{0,61}[a-z0-9])?)\.educraft(?:-dev)?\./);
+	return m?.[1] ?? null;
+}
+
+export function isOrgAdmin(org: OrgMembership | null | undefined): boolean {
+	if (!org) return false;
+	const role = String(org.role ?? '').toUpperCase();
+	return role === 'OWNER' || role === 'ADMIN';
+}
+
+/**
+ * Resolve the tenancy for this browser session.
+ * Prefers hostname slug (silo), then ?org=, then first admin membership, then first membership.
+ */
+export function resolveOrg(me: MeResponse | null | undefined, search: string = ''): OrgMembership | null {
+	if (!me || me.organizations.length === 0) return null;
+	const host = hostOrgSlug();
+	if (host) {
+		const byHost = me.organizations.find((o) => o.slug === host);
+		if (byHost) return byHost;
+	}
+	const q = new URLSearchParams(search).get('org')?.trim();
+	if (q) {
+		const byQuery = me.organizations.find((o) => o.slug === q);
+		if (byQuery) return byQuery;
+	}
+	const admin = me.organizations.find((o) => isOrgAdmin(o));
+	return admin ?? me.organizations[0] ?? null;
+}
+
+/** SPA paths no longer embed org slug (subdomain carries tenancy). */
+export function adminPath(rest: string = ''): string {
+	const cleaned = rest.replace(/^\/+/, '');
+	return cleaned === '' ? '/admin' : `/admin/${cleaned}`;
+}

hub/admin-web/src/lib/session.ts

@@ -35,12 +35,9 @@ export async function loadSession(): Promise<void> {
 /**
  * Resolve org slug for org-scoped Feishu OAuth (`GET /auth/feishu/:orgSlug`).
  * Unscoped `/auth/feishu` is disabled unless allowLegacyFeishuOAuth is on.
+ * Path no longer carries tenancy: prefer hostname silo slug, then ?org=.
  */
 export function resolveLoginOrgSlug(): string | null {
-	const path = window.location.pathname.split('/').filter(Boolean);
-	if (path[0] === 'admin' && path[1] === 'org' && path[2]) {
-		return decodeURIComponent(path[2]);
-	}
 	const q = new URLSearchParams(window.location.search).get('org');
 	if (q && q.trim() !== '') return q.trim();
 
@@ -48,6 +45,12 @@ export function resolveLoginOrgSlug(): string | null {
 	const host = window.location.hostname.toLowerCase();
 	const m = host.match(/^([a-z0-9](?:[a-z0-9-]{0,61}[a-z0-9])?)\.educraft(?:-dev)?\./);
 	if (m?.[1]) return m[1];
+
+	// Legacy path while old bookmarks still land briefly before redirect.
+	const path = window.location.pathname.split('/').filter(Boolean);
+	if (path[0] === 'admin' && path[1] === 'org' && path[2]) {
+		return decodeURIComponent(path[2]);
+	}
 	return null;
 }
 

hub/admin-web/src/routes/+layout.svelte

@@ -5,6 +5,7 @@
 	import { page } from '$app/state';
 	import { session, loadSession, logout, redirectToLogin } from '$lib/session';
 	import type { OrgMembership } from '$lib/api';
+	import { adminPath, isOrgAdmin, resolveOrg } from '$lib/org';
 	import { orgRoleLabel } from '$lib/format';
 	import Icon from '$lib/components/Icon.svelte';
 	import ToastHost from '$lib/components/ToastHost.svelte';
@@ -32,56 +33,36 @@
 		{ key: 'capabilities', label: '能力', icon: 'provider' as const },
 	];
 
-	function isAdmin(org: OrgMembership): boolean {
-		const role = String(org.role ?? '').toUpperCase();
-		return role === 'OWNER' || role === 'ADMIN';
-	}
-
-	function orgSlugFromPath(): string | null {
-		const parts = page.url.pathname.split('/').filter(Boolean);
-		if (parts[0] === 'admin' && parts[1] === 'org' && parts[2]) {
-			return decodeURIComponent(parts[2]);
-		}
-		return null;
-	}
-
-	function isOnProjectRoute(): boolean {
-		const parts = page.url.pathname.split('/').filter(Boolean);
-		return parts[0] === 'admin' && parts[1] === 'org' && parts[3] === 'projects';
-	}
-
 	function memberships(): OrgMembership[] {
 		return $session.me?.organizations ?? [];
 	}
 
 	function adminOrgs(): OrgMembership[] {
-		return memberships().filter(isAdmin);
+		return memberships().filter((o) => isOrgAdmin(o));
 	}
 
 	function currentOrg(): OrgMembership | null {
-		const slug = orgSlugFromPath();
+		return resolveOrg($session.me, page.url.search);
-		if (!slug) return null;
-		return memberships().find((o) => o.slug === slug) ?? null;
 	}
 
-	function pickHomeOrg(): OrgMembership | null {
+	function isOnProjectRoute(): boolean {
-		const admin = adminOrgs()[0];
+		const parts = page.url.pathname.split('/').filter(Boolean);
-		if (admin) return admin;
+		// /admin/projects or /admin/projects/:id
-		return memberships()[0] ?? null;
+		return parts[0] === 'admin' && parts[1] === 'projects';
 	}
 
 	function activeKey(): string {
 		const parts = page.url.pathname.split('/').filter(Boolean);
-		if (parts[0] !== 'admin' || parts[1] !== 'org' || !parts[2]) return '';
+		if (parts[0] !== 'admin') return '';
-		return parts[3] ?? 'overview';
+		// /admin → overview; /admin/usage → usage; /admin/projects/x → projects
+		return parts[1] ?? 'overview';
 	}
 
 	function navHref(key: string): string {
-		const slug = currentOrg()?.slug ?? pickHomeOrg()?.slug;
+		if (key === 'overview') return adminPath();
-		if (!slug) return '/';
+		return adminPath(key);
-		if (key === 'overview') return `/admin/org/${slug}`;
-		return `/admin/org/${slug}/${key}`;
 	}
+
 	function pageTitle(): string {
 		const key = activeKey();
 		if (key === 'overview' || key === '') return '概览';
@@ -91,7 +72,10 @@
 
 	function switchOrg(nextSlug: string) {
 		if (!nextSlug || nextSlug === currentOrg()?.slug) return;
-		void goto(`/admin/org/${nextSlug}`);
+		// Path is tenancy-free; keep optional ?org= for local multi-membership debugging.
+		const url = new URL(page.url.href);
+		url.searchParams.set('org', nextSlug);
+		void goto(`${url.pathname}${url.search}`, { replaceState: true });
 	}
 
 	function handleLogout(e: Event) {
@@ -114,33 +98,23 @@
 	$effect(() => {
 		if ($session.loading || !$session.me) return;
 
-		const slug = orgSlugFromPath();
+		const path = page.url.pathname;
-		const matched = slug ? memberships().find((o) => o.slug === slug) : null;
+		// Legacy /admin/org/:slug… is handled by admin/org/[...path] page.
 
-		// Org admins: route to their first admin org if none matched as admin.
+		const org = currentOrg();
 		const admins = adminOrgs();
-		if (matched && isAdmin(matched)) {
+
+		if (org && isOrgAdmin(org)) {
 			redirecting = false;
 			return;
 		}
-		if (!matched && admins.length > 0) {
-			const target = `/admin/org/${admins[0].slug}`;
-			if (page.url.pathname !== target && !page.url.pathname.startsWith(`${target}/`)) {
-				redirecting = true;
-				void goto(target, { replaceState: true });
-			}
-			return;
-		}
 
-		// Members (non-admin): project pages are open to project MANAGE holders;
+		// Member only: allow project routes; bounce admin-only surfaces to projects.
-		// the org overview and other admin-only surfaces are not for them.
+		if (org && !isOrgAdmin(org)) {
-		if (matched && !isAdmin(matched)) {
 			redirecting = false;
-			const parts = page.url.pathname.split('/').filter(Boolean);
+			if (!isOnProjectRoute()) {
-			const onOverview = parts.length === 3; // /admin/org/:slug
+				const target = adminPath('projects');
-			if (onOverview) {
+				if (path !== target) {
-				const target = `/admin/org/${matched.slug}/projects`;
-				if (page.url.pathname !== target) {
 					redirecting = true;
 					void goto(target, { replaceState: true });
 				}
@@ -148,12 +122,11 @@
 			return;
 		}
 
-		// No matched org and no admin orgs: route a member to their first org's
+		// No org resolved but user has memberships → land on first org's projects/overview via resolveOrg next tick
-		// projects page so they can reach project MANAGE surfaces.
+		if (!org && memberships().length > 0) {
-		if (!matched && memberships().length > 0) {
+			const home = admins[0] ?? memberships()[0]!;
-			const home = memberships()[0];
+			const target = isOrgAdmin(home) ? adminPath() : adminPath('projects');
-			const target = `/admin/org/${home.slug}/projects`;
+			if (path !== target && !path.startsWith(`${target}/`)) {
-			if (page.url.pathname !== target && !page.url.pathname.startsWith(`${target}/`)) {
 				redirecting = true;
 				void goto(target, { replaceState: true });
 			}
@@ -174,14 +147,14 @@
 					d="M4 12a8 8 0 018-8V0C5.373 0 0 5.373 0 12h4zm2 5.291A7.962 7.962 0 014 12H0c0 3.042 1.135 5.824 3 7.938l3-2.647z"
 				></path>
 			</svg>
-			<p class="text-sm">{redirecting ? '正在进入组织…' : '正在加载会话…'}</p>
+			<p class="text-sm">加载中…</p>
 		</div>
 	</div>
 {:else if $session.error}
 	<div class="saas-status-panel">
 		<div class="saas-status-card">
 			<div
-				class="mx-auto mb-4 flex h-12 w-12 items-center justify-center border border-error-300 bg-error-100 text-error-700 font-bold"
+				class="mx-auto mb-3 flex h-12 w-12 items-center justify-center border border-error-200 bg-error-50 text-error-700"
 			>
 				!
 			</div>
@@ -194,7 +167,7 @@
 	<div class="saas-status-panel">
 		<div class="saas-status-card">
 			<div
-				class="mx-auto mb-5 flex h-12 w-12 items-center justify-center border border-primary-700 bg-primary-600 text-white font-bold"
+				class="mx-auto mb-4 flex h-12 w-12 items-center justify-center border border-primary-700 bg-primary-600 text-sm font-bold text-white"
 			>
 				CPH
 			</div>
@@ -203,7 +176,7 @@
 			<button class="saas-btn-primary w-full" onclick={() => redirectToLogin()}>使用飞书登录</button>
 		</div>
 	</div>
-{:else if currentOrg() && isAdmin(currentOrg()!)}
+{:else if currentOrg() && isOrgAdmin(currentOrg()!)}
 	{@const org = currentOrg()!}
 	{@const me = $session.me!}
 	<div class="saas-shell">
@@ -228,10 +201,11 @@
 				</div>
 				<div class="min-w-0">
 					<div class="truncate text-sm font-semibold text-surface-900">组织后台</div>
-					<div class="truncate text-xs text-surface-600">Curriculum Hub</div>
+					<div class="truncate text-xs text-surface-600">{org.name}</div>
 				</div>
 			</div>
 
+			{#if me.organizations.length > 1}
 				<div class="px-3 pb-3">
 					<div class="mb-1.5 flex items-center gap-1.5 text-xs font-medium text-surface-700">
 						<Icon name="org" class="h-3.5 w-3.5" />
@@ -239,6 +213,7 @@
 					</div>
 					<SelectField items={orgSelectItems(me.organizations)} value={org.slug} onchange={switchOrg} />
 				</div>
+			{/if}
 
 			<nav class="flex-1 space-y-0.5 overflow-y-auto px-2 pb-3">
 				<p class="px-3 pb-1 pt-2 text-[11px] font-semibold uppercase tracking-wider text-surface-600">工作台</p>
@@ -308,13 +283,13 @@
 			</main>
 		</div>
 	</div>
-{:else if currentOrg() && !isAdmin(currentOrg()!) && isOnProjectRoute()}
+{:else if currentOrg() && !isOrgAdmin(currentOrg()!) && isOnProjectRoute()}
 	{@const org = currentOrg()!}
 	{@const me = $session.me!}
 	<div class="saas-shell">
 		<div class="saas-main">
 			<header class="saas-topbar">
-				<a href={`/admin/org/${org.slug}/projects`} class="saas-btn-ghost px-2!" aria-label="返回项目列表">
+				<a href={adminPath('projects')} class="saas-btn-ghost px-2!" aria-label="返回项目列表">
 					<Icon name="menu" class="h-5 w-5" />
 				</a>
 				<div class="min-w-0">
@@ -343,7 +318,7 @@
 			</main>
 		</div>
 	</div>
-{:else if currentOrg() && !isAdmin(currentOrg()!)}
+{:else if currentOrg() && !isOrgAdmin(currentOrg()!)}
 	{@const denied = currentOrg()!}
 	<div class="saas-status-panel">
 		<div class="saas-status-card">
@@ -352,7 +327,7 @@
 				组织 <strong>{denied.name}</strong>（/{denied.slug}）中你的角色是
 				<span class="saas-badge-neutral mx-1">{orgRoleLabel(denied.role)}</span>。普通成员仅可访问自己有授权的项目。
 			</p>
-			<a class="saas-btn-primary" href={`/admin/org/${denied.slug}/projects`}>查看我的项目</a>
+			<a class="saas-btn-primary" href={adminPath('projects')}>查看我的项目</a>
 			{#if memberships().length > 1}
 				<p class="saas-label text-left mb-1.5 mt-3">切换到其他组织</p>
 				<div class="mb-4">
@@ -363,14 +338,14 @@
 		</div>
 	</div>
 {:else if memberships().length > 0}
-	{@const denied = pickHomeOrg()!}
+	{@const denied = resolveOrg($session.me) ?? memberships()[0]!}
 	<div class="saas-status-panel">
 		<div class="saas-status-card">
 			<h2 class="mb-2 text-lg font-semibold">正在跳转…</h2>
 			<p class="mb-5 text-sm text-surface-700">
 				即将进入 <strong>{denied.name}</strong>（/{denied.slug}）的项目。
 			</p>
-			<a class="saas-btn-primary" href={`/admin/org/${denied.slug}/projects`}>立即进入</a>
+			<a class="saas-btn-primary" href={adminPath('projects')}>立即进入</a>
 			<button class="saas-btn-ghost mt-3" onclick={handleLogout}>退出登录</button>
 		</div>
 	</div>

hub/admin-web/src/routes/+page.svelte

@@ -11,7 +11,7 @@
 			return r === 'OWNER' || r === 'ADMIN';
 		});
 		const target = admin ?? me.organizations[0];
-		return target ? `/admin/org/${target.slug}` : null;
+		return target ? `/admin` : null;
 	}
 
 	onMount(() => {

hub/admin-web/src/routes/admin/+page.svelte

@@ -2,6 +2,7 @@
 	import { page } from '$app/state';
 	import { api, type OrgMembership } from '$lib/api';
 	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtCost, fmtNum, orgRoleLabel } from '$lib/format';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import StatCard from '$lib/components/StatCard.svelte';
@@ -10,7 +11,8 @@
 	import SwitchControl from '$lib/components/SwitchControl.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	let orgSlug = $derived(page.params.slug ?? '');
+	const orgFromSession = $derived(resolveOrg($session.me, page.url.search));
+	let orgSlug = $derived(orgFromSession?.slug ?? '');
 	let org = $derived($session.me?.organizations.find((o) => o.slug === orgSlug) as OrgMembership | undefined);
 
 	let settings = $state<{ membersCanCreateProjects: boolean } | null>(null);
@@ -96,7 +98,7 @@
 			<h2 class="saas-section-title">用量概览</h2>
 			<p class="saas-muted">totals 含全部 UsageFact；分账明细见用量页。</p>
 		</div>
-		<a class="saas-btn-secondary py-1.5! text-sm" href={`/admin/org/${orgSlug}/usage`}>完整用量报告</a>
+		<a class="saas-btn-secondary py-1.5! text-sm" href={`/admin/usage`}>完整用量报告</a>
 	</div>
 
 	<div class="mb-6 grid gap-3 sm:grid-cols-2 lg:grid-cols-3">
@@ -115,7 +117,7 @@
 					<h3 class="text-sm font-semibold text-surface-800">消费来源（Top）</h3>
 					<p class="saas-muted text-xs">模型完成 vs 外部能力，按成本降序前 5</p>
 				</div>
-				<a class="text-sm text-primary-700 hover:underline" href={`/admin/org/${orgSlug}/usage`}>查看全部分账</a>
+				<a class="text-sm text-primary-700 hover:underline" href={`/admin/usage`}>查看全部分账</a>
 			</div>
 			<div class="overflow-x-auto">
 				<table class="data-table">
@@ -167,7 +169,7 @@
 						{#each usage.projects as p}
 							<tr>
 								<td class="font-medium">
-									<a class="hover:text-primary-700 hover:underline" href={`/admin/org/${orgSlug}/projects/${p.projectId}`}>
+									<a class="hover:text-primary-700 hover:underline" href={`/admin/projects/${p.projectId}`}>
 										{p.projectName}
 									</a>
 								</td>

hub/admin-web/src/routes/admin/capabilities/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type CapabilityConnection } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtDate } from '$lib/format';
 	import { Label } from 'bits-ui';
 	import PageHeader from '$lib/components/PageHeader.svelte';
@@ -8,7 +10,8 @@
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	const KNOWN_CAPABILITIES = [
 		{ id: 'pdf_to_md_bundle', label: 'PDF → Markdown', description: '将 PDF 转换为带图片的 Markdown bundle（阿里云文档智能，含公式 LaTeX 识别）' },

hub/admin-web/src/routes/admin/capacity/+page.svelte

@@ -1,13 +1,16 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type CapacityDimension, type CapacityDimensionRow, type CapacityPolicyView } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import LoadingState from '$lib/components/LoadingState.svelte';
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
 	import EmptyState from '$lib/components/EmptyState.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	// Friendlier, user-facing labels. No spec jargon (墙钟 → 运行时长, etc.).
 	const DIMENSION_LABELS: Record<CapacityDimension, string> = {

hub/admin-web/src/routes/admin/feishu/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type FeishuApplicationConnection } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtDate } from '$lib/format';
 	import { Label } from 'bits-ui';
 	import PageHeader from '$lib/components/PageHeader.svelte';
@@ -8,7 +10,8 @@
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let connection = $state<FeishuApplicationConnection | null>(null);
 	let loading = $state(true);

hub/admin-web/src/routes/admin/members/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type OrgMember } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtDate } from '$lib/format';
 	import { ORG_ROLES, ORG_ROLE_LABELS, PERMISSION_ROLE_LABELS } from '$lib/constants';
 	import PageHeader from '$lib/components/PageHeader.svelte';
@@ -10,7 +12,8 @@
 	import SelectField from '$lib/components/SelectField.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 	const roleItems = ORG_ROLES.map((r) => ({ value: r, label: ORG_ROLE_LABELS[r] }));
 	const permHint = Object.values(PERMISSION_ROLE_LABELS).join(' / ');
 

hub/admin-web/src/routes/admin/org/[...path]/+page.svelte

@@ -0,0 +1,23 @@
+<script lang="ts">
+	/**
+	 * Legacy bookmarks: /admin/org/:slug[/...] → /admin[/...]
+	 * Tenancy lives on the silo host, not the path.
+	 */
+	import { onMount } from 'svelte';
+	import { goto } from '$app/navigation';
+	import { page } from '$app/state';
+
+	onMount(() => {
+		const raw = page.params.path ?? '';
+		const segments = raw.split('/').filter(Boolean);
+		// Drop the old org slug (first segment) when present.
+		const rest = segments.length > 0 ? segments.slice(1).join('/') : '';
+		const target = rest === '' ? '/admin' : `/admin/${rest}`;
+		const q = page.url.search;
+		void goto(`${target}${q}`, { replaceState: true });
+	});
+</script>
+
+<div class="saas-status-panel">
+	<p class="text-sm text-surface-600">正在重定向到新地址…</p>
+</div>

hub/admin-web/src/routes/admin/projects/+page.svelte

@@ -2,6 +2,7 @@
 	import { page } from '$app/state';
 	import { api, type ExplorerData, type ExplorerFolder, type ExplorerProject, type OrgMembership } from '$lib/api';
 	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import FolderTree from '$lib/components/FolderTree.svelte';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import LoadingState from '$lib/components/LoadingState.svelte';
@@ -13,8 +14,8 @@
 	import { fmtDate } from '$lib/format';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
-	const org = $derived(($session.me?.organizations.find((o) => o.slug === slug) as OrgMembership | undefined) ?? null);
+	const slug = $derived(org?.slug ?? '');
 	const isAdmin = $derived(!!org && (org.role === 'OWNER' || org.role === 'ADMIN'));
 
 	let data = $state<ExplorerData | null>(null);
@@ -87,7 +88,7 @@
 			projectName = '';
 			projectFolder = '';
 			showProjectModal = false;
-			window.location.href = `/admin/org/${slug}/projects/${res.id}`;
+			window.location.href = `/admin/projects/${res.id}`;
 		} catch (err) {
 			toastError(err instanceof Error ? err.message : String(err));
 		}
@@ -207,7 +208,7 @@
 				</thead>
 				<tbody>
 					{#each myProjects as p}
-						<tr class="cursor-pointer" onclick={() => (window.location.href = `/admin/org/${slug}/projects/${p.id}`)}>
+						<tr class="cursor-pointer" onclick={() => (window.location.href = `/admin/projects/${p.id}`)}>
 							<td class="font-medium">{p.name}</td>
 							<td class="font-mono text-xs">{p.binding ? `群 ${p.binding.chatId}` : '—'}</td>
 							<td class="text-surface-700">{fmtDate(p.createdAt)}</td>

hub/admin-web/src/routes/admin/projects/[projectId]/+page.svelte

@@ -9,6 +9,8 @@
 		type ExplorerData,
 		type ProjectUsageReport,
 	} from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import {
 		fmtCost,
 		fmtDate,
@@ -27,7 +29,8 @@
 	import Icon from '$lib/components/Icon.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 	const projectId = $derived(page.params.projectId ?? '');
 	const roleItems = PERMISSION_ROLES.map((r) => ({ value: r, label: PERMISSION_ROLE_LABELS[r] }));
 	const roleChain = `${PERMISSION_ROLE_LABELS.READ} ⊂ ${PERMISSION_ROLE_LABELS.EDIT} ⊂ ${PERMISSION_ROLE_LABELS.MANAGE}`;
@@ -109,7 +112,7 @@
 		if (!confirm(`归档项目 ${proj?.name}?`)) return;
 		try {
 			await api.archiveProject(slug, projectId);
-			window.location.href = `/admin/org/${slug}/projects`;
+			window.location.href = `/admin/projects`;
 		} catch (err) {
 			toastError(err instanceof Error ? err.message : String(err));
 		}
@@ -170,7 +173,7 @@
 {:else if proj}
 	<div class="mb-2">
 		<a
-			href={`/admin/org/${slug}/projects`}
+			href={`/admin/projects`}
 			class="inline-flex items-center gap-1 text-sm text-surface-700 hover:text-primary-600"
 		>
 			<Icon name="arrow-left" class="h-4 w-4" />
@@ -293,7 +296,7 @@
 							{fmtTokens(projectUsage.inputTokens, projectUsage.outputTokens)}
 						</p>
 					</div>
-					<a class="text-sm text-primary-700 hover:underline" href={`/admin/org/${slug}/usage`}>组织报告</a>
+					<a class="text-sm text-primary-700 hover:underline" href={`/admin/usage`}>组织报告</a>
 				</div>
 				{#if projectUsage.breakdown.length === 0}
 					<div class="px-5 py-4 text-sm text-surface-600">尚无 UsageFact。</div>
@@ -368,7 +371,7 @@
 								<td class="text-right">
 									<a
 										class="text-sm text-primary-700 hover:underline"
-										href={`/admin/org/${slug}/sessions/${s.id}`}
+										href={`/admin/sessions/${s.id}`}
 									>
 										详情
 									</a>

hub/admin-web/src/routes/admin/provider/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type ProviderConnectionRow } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtDate, providerModeLabel } from '$lib/format';
 	import { Label } from 'bits-ui';
 	import PageHeader from '$lib/components/PageHeader.svelte';
@@ -8,7 +10,8 @@
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let connections = $state<ProviderConnectionRow[]>([]);
 	let loading = $state(true);

hub/admin-web/src/routes/admin/roles/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type AgentRoleRow, type AgentModelRow, type AgentSkillRow } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import LoadingState from '$lib/components/LoadingState.svelte';
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
@@ -8,7 +10,8 @@
 	import RoleCard from '$lib/components/RoleCard.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let roles = $state<AgentRoleRow[]>([]);
 	let models = $state<AgentModelRow[]>([]);

hub/admin-web/src/routes/admin/sessions/[sessionId]/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type SessionDetail, type SessionRunRow, type UsageFactRow } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import {
 		fmtCost,
 		fmtDate,
@@ -16,7 +18,8 @@
 	import EmptyState from '$lib/components/EmptyState.svelte';
 	import Icon from '$lib/components/Icon.svelte';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 	const sessionId = $derived(page.params.sessionId ?? '');
 
 	let detail = $state<SessionDetail | null>(null);
@@ -92,7 +95,7 @@
 	<div class="mb-2">
 		<a
 			class="inline-flex items-center gap-1 text-sm text-surface-700 hover:text-primary-700"
-			href={`/admin/org/${slug}/projects/${detail.project.id}`}
+			href={`/admin/projects/${detail.project.id}`}
 		>
 			<Icon name="arrow-left" class="h-4 w-4" />
 			返回项目 {detail.project.name}
@@ -113,7 +116,7 @@
 			<div>
 				<dt class="text-surface-600">项目</dt>
 				<dd class="mt-0.5">
-					<a class="text-primary-700 hover:underline" href={`/admin/org/${slug}/projects/${detail.project.id}`}>
+					<a class="text-primary-700 hover:underline" href={`/admin/projects/${detail.project.id}`}>
 						{detail.project.name}
 					</a>
 				</dd>

hub/admin-web/src/routes/admin/skills/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type AgentSkillRow, type SkillFileEntry } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import LoadingState from '$lib/components/LoadingState.svelte';
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
@@ -8,7 +10,8 @@
 	import SkillEditor from '$lib/components/SkillEditor.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let skills = $state<AgentSkillRow[]>([]);
 	let loading = $state(true);

hub/admin-web/src/routes/admin/teams/+page.svelte

@@ -2,6 +2,8 @@
 	import { Collapsible } from 'bits-ui';
 	import { page } from '$app/state';
 	import { api, type TeamRow, type TeamMemberRow } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import { fmtDate } from '$lib/format';
 	import PageHeader from '$lib/components/PageHeader.svelte';
 	import LoadingState from '$lib/components/LoadingState.svelte';
@@ -9,7 +11,8 @@
 	import EmptyState from '$lib/components/EmptyState.svelte';
 	import { toastError, toastSuccess } from '$lib/toast';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let teams = $state<TeamRow[]>([]);
 	let loading = $state(true);

hub/admin-web/src/routes/admin/usage/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
 	import { page } from '$app/state';
 	import { api, type UsageReport, type UsageBreakdownRow } from '$lib/api';
+	import { session } from '$lib/session';
+	import { resolveOrg } from '$lib/org';
 	import {
 		fmtCost,
 		fmtDateOnly,
@@ -15,7 +17,8 @@
 	import ErrorBanner from '$lib/components/ErrorBanner.svelte';
 	import EmptyState from '$lib/components/EmptyState.svelte';
 
-	const slug = $derived(page.params.slug ?? '');
+	const org = $derived(resolveOrg($session.me, page.url.search));
+	const slug = $derived(org?.slug ?? '');
 
 	let usage = $state<UsageReport | null>(null);
 	let loading = $state(true);
@@ -224,7 +227,7 @@
 								<td class="tabular-nums text-surface-600">{fmtTokens(p.inputTokens, p.outputTokens)}</td>
 								<td class="tabular-nums">{fmtCost(p.costUsd)}</td>
 								<td class="text-right">
-									<a class="text-sm text-primary-700 hover:underline" href={`/admin/org/${slug}/projects/${p.projectId}`}>
+									<a class="text-sm text-primary-700 hover:underline" href={`/admin/projects/${p.projectId}`}>
 										查看项目
 									</a>
 								</td>

hub/package-lock.json

@@ -1,12 +1,12 @@
 {
   "name": "@paradigm/hub",
-  "version": "0.0.34",
+  "version": "0.0.36",
   "lockfileVersion": 3,
   "requires": true,
   "packages": {
     "": {
       "name": "@paradigm/hub",
-      "version": "0.0.34",
+      "version": "0.0.36",
       "dependencies": {
         "@alicloud/credentials": "^2.4.5",
         "@alicloud/docmind-api20220711": "^1.4.15",

hub/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@paradigm/hub",
-  "version": "0.0.34",
+  "version": "0.0.36",
   "private": true,
   "type": "module",
   "engines": {
@@ -30,7 +30,7 @@
       "axios": "1.18.1"
     }
   },
-  "description": "Curriculum Project Hub — org-scoped Feishu collaboration and confined Agent runtime. Aligns to spec/System through ADR-0024.",
+  "description": "Curriculum Project Hub — org-scoped Feishu collaboration and confined Agent runtime. Semantics pinned by docs/adr/ (ADR-0001 through ADR-0027).",
   "scripts": {
     "dev": "npm run prisma:migrate && tsx watch src/server.ts",
     "build": "tsc -p tsconfig.json && npm run admin:build",

hub/prisma/migrations/20260714120000_drop_legacy_platform_role_assignment/migration.sql

@@ -1,6 +1,6 @@
 -- ADR-0023 rejected the legacy `PlatformRoleAssignment` / `PlatformRole`{ADMIN,TEACHER}
 -- model: the platform administration control plane is a separate identity/session/
--- audit surface (see `Spec.System.PlatformAdministration`), intentionally not built
+-- audit surface, intentionally not built
 -- in alpha (ADR-0025, `hub/deploy/README.md`). The legacy table has no runtime
 -- reader — no guard, route, or service queries it for an authorization decision —
 -- and ADR-0023 requires it to be migrated/replaced before the platform panel ships.

hub/prisma/schema.prisma

@@ -1,6 +1,6 @@
 // Prisma schema for Curriculum Project Hub.
 //
-// Aligns to spec/System (ADR-0001..0004, 0017). Key divergences from the
+// Aligns to ADR-0001..0004, 0017. Key divergences from the
 // legacy teaching-material-host-service schema, each deliberate:
 //
 //  - AgentSession is provider/model-bound. Provider runtime cursors such as
@@ -11,8 +11,8 @@
 //  - 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
+//  - AgentRunStatus adds WAITING_FOR_USER + TIMED_OUT (the run-state set is
-//    completeness OPEN — add states without a schema migration war).
+//    open — add states without a schema migration war).
 
 generator client {
   provider = "prisma-client-js"
@@ -61,7 +61,7 @@ enum OrganizationStatus {
 }
 
 /// Org-scoped membership role. Distinct from project PermissionRole and from
-/// the platform administrator surface (ADR-0023 / Spec.System.PlatformAdministration),
+/// the platform administrator surface (ADR-0023),
 /// which is a separate control plane not modeled in alpha (ADR-0025).
 model OrganizationMembership {
   id             String                 @id @default(cuid())

hub/src/admin/routes/authRoutes.ts

@@ -432,16 +432,16 @@ async function resolvePostLoginRedirect(
       select: { organization: { select: { slug: true, name: true } } },
     });
     if (intended === null) return "/admin?error=not_an_active_org_member";
-    const orgRoot = `/admin/org/${intended.organization.slug}`;
+    const orgRoot = "/admin";
     // Default / missing returnTo sanitizes to "/admin". Always land in the org
     // admin SPA (not the legacy static "close this tab" complete page).
     if (returnTo === "/admin") {
       return orgRoot;
     }
-    return returnTo === orgRoot || returnTo.startsWith(`${orgRoot}/`) ? returnTo : orgRoot;
+    return normalizeAdminReturnTo(returnTo) ?? orgRoot;
   }
   if (returnTo !== "/admin" && returnTo.startsWith("/admin")) {
-    return returnTo;
+    return normalizeAdminReturnTo(returnTo) ?? "/admin";
   }
   const membership = await prisma.organizationMembership.findFirst({
     where: {
@@ -454,7 +454,7 @@ async function resolvePostLoginRedirect(
     orderBy: { createdAt: "asc" },
   });
   if (membership !== null) {
-    return `/admin/org/${membership.organization.slug}`;
+    return "/admin";
   }
   // Member-only or no org: still land on a shell page (SPA will explain).
   const any = await prisma.organizationMembership.findFirst({
@@ -463,7 +463,7 @@ async function resolvePostLoginRedirect(
     orderBy: { createdAt: "asc" },
   });
   if (any !== null) {
-    return `/admin/org/${any.organization.slug}`;
+    return "/admin/projects";
   }
   return "/admin/login?error=no_organization";
 }
@@ -489,7 +489,18 @@ export function sanitizeReturnTo(raw: string): string {
   if (!raw.startsWith("/admin")) {
     return "/admin";
   }
-  return raw;
+  return normalizeAdminReturnTo(raw) ?? "/admin";
+}
+
+/** Map legacy `/admin/org/:slug[...]` bookmarks onto slugless `/admin[...]` paths. */
+export function normalizeAdminReturnTo(path: string): string | null {
+  if (!path.startsWith("/admin")) return null;
+  const legacy = path.match(/^\/admin\/org\/[^/]+(\/.*)?$/);
+  if (legacy) {
+    const rest = legacy[1] ?? "";
+    return rest === "" ? "/admin" : `/admin${rest}`;
+  }
+  return path;
 }
 
 function trimTrailingSlash(url: string): string {

hub/src/agent/runner.ts

@@ -24,10 +24,10 @@
  * denied by default and re-opened only for the workspace plus named system
  * runtimes, and `failIfUnavailable` hard-fails if the sandbox can't start. The
  * subprocess gets a minimal environment and SDK credential protection removes
- * provider secrets from Bash. This upholds `AgentFileOp.Authorized`
+ * provider secrets from Bash. This upholds the workspace-bounded file-op
- * (ADR-0018 / `Spec.System.AgentSurface`) without re-implementing the
+ * invariant (ADR-0018) without re-implementing the
  * `workspace.ts` `confine()` path validator as a tool wrapper — the OS sandbox
- * is the mechanism, the contract pins the invariant.
+ * is the mechanism, the ADR pins the invariant.
  */
 import { query, type HookCallback, type McpServerConfig, type SDKMessage, type SDKAssistantMessage, type SDKUserMessage, type SDKResultMessage, type SDKPartialAssistantMessage, type SDKSystemMessage } from "@anthropic-ai/claude-agent-sdk";
 import type { PrismaClient } from "@prisma/client";

hub/src/capacity/dimensions.ts

@@ -1,6 +1,6 @@
 /**
- * ADR-0022 capacity dimensions (spec `Spec.System.Capacity.CapacityDimension`).
+ * ADR-0022 capacity dimensions.
- * The 23 PINNED dimensions; exact numeric ceilings are `OPEN` and calibrated by
+ * The 23 pinned dimensions; exact numeric ceilings are open and calibrated by
  * capacity testing. This module is the single source of the dimension set shared
  * by the platform-ceiling config and the org capacity-policy service.
  */

hub/src/database/README.md

@@ -0,0 +1,82 @@
+# src/database/
+
+`/database/*` HTTP 面。代码写在这个目录里，`hub.ts` 通过 `plugin.ts` 挂载它，
+所以服务器启动时能正确识别这些路由。
+
+页面：
+
+- `/database/admin` —— 飞书登录页（唯一登录方式）
+- `/database/dashboard` —— 左菜单 + 右内容的后台，未登录会跳回 `/database/admin`
+
+登录走平台既有的飞书 OAuth：登录页的按钮指向 `/auth/feishu/<orgSlug>`，
+回调由 `src/admin/routes/authRoutes.ts` 处理并种下 session cookie。
+
+## 开发模式：用环境变量开启一键登录
+
+本地开发没有真实飞书 app 时，可以用环境变量开启一键登录，跳过飞书 OAuth，
+直接以现有 OWNER/ADMIN 身份登入后台。**仅限开发，不是生产登录路径。**
+
+### 怎么开
+
+在 `hub/.env` 里设：
+
+```sh
+HUB_DEV_LOGIN_BYPASS="true"
+```
+
+改完重启服务（`npm run dev`，或本地手动 `npx tsx src/server.ts`）。启动日志会
+打印一行 `DEV login bypass enabled: /database/dev-login ...` 作为确认。
+
+开启后：
+
+- `/database/admin` 登录页显示「⚡ 一键登录管理员」按钮
+- 后端注册 `/database/dev-login` 端点：按钮就是打它，它签发一个和飞书 OAuth
+  回调完全一样的 session，然后跳到 `/database/dashboard`
+
+### 怎么关
+
+把值设成 `false`（或 `0` / `no` / `off`），或删掉这一行。关闭后按钮消失、
+`/database/dev-login` 返回 404 —— 按钮和端点同进同退。
+
+### 双重门禁（重要）
+
+真正的开关是两个条件的**与**（判断在 `plugin.ts`）：
+
+```
+allowDevLoginBypass = (NODE_ENV !== "production") && HUB_DEV_LOGIN_BYPASS 为真
+```
+
+即：**只要 `NODE_ENV=production`，无论 `HUB_DEV_LOGIN_BYPASS` 设成什么，一键登录
+都强制关闭。** 生产始终只能走真实飞书 OAuth。
+
+> 提醒：`HUB_DEV_LOGIN_BYPASS` 是敏感开关，别把开着它的 `.env` 带到任何联网 /
+> 共享环境。整个旁路逻辑自包含在本目录（`plugin.ts` + `routes/databaseRoutes.ts`），
+> `src/admin` 的登录路由未受影响。
+
+## 文件
+
+| 文件 | 职责 |
+|------|------|
+| `plugin.ts` | 模块对外入口，`hub.ts` 调 `registerDatabasePlugin()` |
+| `routes/databaseRoutes.ts` | 路由 + 页面渲染，**你主要在这里加内容** |
+
+新增一类端点时：要么直接往 `databaseRoutes.ts` 加 `app.get("/database/...")`，
+要么新建 `routes/xxxRoutes.ts` 并在 `databaseRoutes.ts` 里 `registerXxxRoutes(app, {...})`
+注册一次。
+
+## 约定（与 admin 面一致）
+
+1. 路由用**绝对路径** `"/database/..."`，不用 Fastify prefix —— 每条路由 grep 得到。
+2. **guard 前置、fail closed**：凡碰数据的端点第一行先跑
+   `requireSession` / `requireOrgRole` / `requireProjectPermission`
+   （都在 `../admin/auth/guards.js`）。
+3. **租户隔离**（ADR-0020）：每个 Prisma 查询都 scope 到 `auth.organization.id`，
+   不得跨 org。禁止无鉴权的数据路由。
+4. 数据库通过传入的 `config.prisma` 访问（全进程单例，见 `../db.ts`）；
+   不要在这里 `new PrismaClient()`。
+
+## 为什么代码在 `src/` 下
+
+`tsconfig.json` 固定 `rootDir: "src"` 且 `include: ["src/**/*.ts"]`。只有
+`src/` 下的 `.ts` 会被 `tsc` 编译、被 `tsx watch`（`npm run dev`）加载。放在
+`src/` 之外的目录不会被构建，外部识别不到。

hub/src/database/plugin.ts

@@ -0,0 +1,45 @@
+/**
+ * Registers the `/database/*` HTTP surface onto the Fastify app.
+ *
+ * Single public entry point (mirrors src/admin/plugin.ts). hub.ts calls
+ * registerDatabasePlugin() so the routes are recognized at startup.
+ *
+ * Register AFTER registerAdminPlugin: it relies on the @fastify/cookie parser
+ * and the /auth/feishu/* login routes that the admin plugin adds.
+ *
+ * The dev login bypass is self-contained in THIS module: the flag is read here
+ * (not threaded from hub.ts) and only ever enables the `/database/dev-login`
+ * route below. Double-gated: NODE_ENV must not be production AND
+ * HUB_DEV_LOGIN_BYPASS must be truthy. Production always requires real Feishu
+ * OAuth.
+ */
+import type { FastifyInstance } from "fastify";
+import type { PrismaClient } from "@prisma/client";
+import { registerDatabaseRoutes } from "./routes/databaseRoutes.js";
+
+export interface DatabasePluginConfig {
+  readonly prisma: PrismaClient;
+  readonly sessionSecret: string;
+  readonly siloOrganizationSlug: string;
+}
+
+const FALSY = new Set(["", "0", "false", "no", "off"]);
+
+export async function registerDatabasePlugin(
+  app: FastifyInstance,
+  config: DatabasePluginConfig,
+): Promise<void> {
+  const allowDevLoginBypass =
+    process.env["NODE_ENV"] !== "production" &&
+    !FALSY.has((process.env["HUB_DEV_LOGIN_BYPASS"] ?? "").trim().toLowerCase());
+  if (allowDevLoginBypass) {
+    app.log.warn("DEV login bypass enabled: /database/dev-login mints a session without Feishu OAuth");
+  }
+
+  await registerDatabaseRoutes(app, {
+    prisma: config.prisma,
+    sessionSecret: config.sessionSecret,
+    siloOrganizationSlug: config.siloOrganizationSlug,
+    allowDevLoginBypass,
+  });
+}

hub/src/database/routes/databaseRoutes.ts

@@ -0,0 +1,307 @@
+/**
+ * `/database/*` route aggregator.
+ *
+ * Owns the `/database` HTTP surface (single place new sub-routes get wired in).
+ * Handlers use ABSOLUTE paths (no Fastify prefix) so every route greps as the
+ * literal string it serves.
+ *
+ *   /database/admin      — Feishu-only login page (+ dev one-click button)
+ *   /database/dashboard  — sidebar + content admin shell, session-gated
+ *   /database/dev-login  — DEV ONLY bypass, registered only when the flag is on
+ *
+ * The dev bypass (button + /database/dev-login) is self-contained here and
+ * gated by allowDevLoginBypass (computed in ./plugin.ts from HUB_DEV_LOGIN_BYPASS
+ * + NODE_ENV). Production requires real Feishu OAuth.
+ */
+import type { FastifyInstance } from "fastify";
+import type { PrismaClient } from "@prisma/client";
+import { SESSION_COOKIE_NAME, signSession, verifySession } from "../../admin/auth/session.js";
+
+export interface DatabaseRouteConfig {
+  readonly prisma: PrismaClient;
+  /** HMAC secret for the signed session cookie — reused from the admin plane. */
+  readonly sessionSecret: string;
+  /** Silo Organization slug — builds the org-scoped Feishu login link. */
+  readonly siloOrganizationSlug: string;
+  /** DEV ONLY. Enables the one-click button and the /database/dev-login route. */
+  readonly allowDevLoginBypass: boolean;
+}
+
+export async function registerDatabaseRoutes(
+  app: FastifyInstance,
+  config: DatabaseRouteConfig,
+): Promise<void> {
+  app.get("/database/admin", async (request, reply) => {
+    // Already signed in → straight to the dashboard.
+    if ((await resolveUser(request.cookies[SESSION_COOKIE_NAME], config)) !== null) {
+      return reply.redirect("/database/dashboard");
+    }
+    return reply.type("text/html").send(renderLoginPage(config));
+  });
+
+  app.get("/database/dashboard", async (request, reply) => {
+    const user = await resolveUser(request.cookies[SESSION_COOKIE_NAME], config);
+    if (user === null) return reply.redirect("/database/admin");
+    return reply.type("text/html").send(renderDashboard(user.displayName));
+  });
+
+  // DEV ONLY bypass — self-contained here, registered only when the flag is on
+  // (see ./plugin.ts). Mints a session for an existing OWNER/ADMIN, reusing the
+  // scoped SessionIdentity shape the Feishu OAuth callback produces so the
+  // session guard behaves identically. Never registered in production.
+  if (config.allowDevLoginBypass) {
+    app.get("/database/dev-login", async (_request, reply) => {
+      const membership = await config.prisma.organizationMembership.findFirst({
+        where: {
+          revokedAt: null,
+          role: { in: ["OWNER", "ADMIN"] },
+          organization: { status: "ACTIVE" },
+        },
+        select: { userId: true, organizationId: true },
+        orderBy: { createdAt: "asc" },
+      });
+      if (membership === null) {
+        return reply.status(404).send({ error: { code: "no_admin", message: "no active OWNER/ADMIN to impersonate" } });
+      }
+      const identity = await config.prisma.feishuUserIdentity.findFirst({
+        where: {
+          userId: membership.userId,
+          connection: { organizationId: membership.organizationId, status: "ACTIVE" },
+        },
+        select: { id: true, connectionId: true, connection: { select: { organizationId: true } } },
+      });
+      if (identity === null) {
+        return reply.status(404).send({ error: { code: "no_identity", message: "admin has no active scoped Feishu identity" } });
+      }
+      const token = signSession(
+        {
+          userId: membership.userId,
+          feishuIdentityId: identity.id,
+          feishuConnectionId: identity.connectionId,
+          feishuOrganizationId: identity.connection.organizationId,
+        },
+        config.sessionSecret,
+      );
+      // Local dev is http://127.0.0.1, so secure:false. This route only ever
+      // runs outside production (double-gated in ./plugin.ts).
+      reply.setCookie(SESSION_COOKIE_NAME, token, {
+        path: "/",
+        httpOnly: true,
+        sameSite: "lax",
+        secure: false,
+        maxAge: 7 * 24 * 60 * 60,
+      });
+      reply.log.warn({ userId: membership.userId, orgId: membership.organizationId }, "DEV database login bypass used");
+      return reply.redirect("/database/dashboard");
+    });
+  }
+
+  // Add more /database/* routes here. Guard data routes with requireSession /
+  // requireOrgRole (../../admin/auth/guards.js) and scope every query to the
+  // caller's org (ADR-0020). Access the DB via config.prisma.
+}
+
+/** Verify the session cookie and load the user, or null if not signed in. */
+async function resolveUser(
+  rawCookie: string | undefined,
+  config: DatabaseRouteConfig,
+): Promise<{ displayName: string } | null> {
+  if (rawCookie === undefined || rawCookie === "") return null;
+  const session = verifySession(rawCookie, config.sessionSecret);
+  if (session === null) return null;
+  const user = await config.prisma.user.findUnique({
+    where: { id: session.userId },
+    select: { displayName: true },
+  });
+  return user;
+}
+
+/**
+ * Shared document head: Tailwind CDN + a small design system (fonts, keyframes
+ * for the aurora background, fade-in, shimmer). Both pages import it so the
+ * look stays consistent.
+ */
+function pageHead(title: string): string {
+  return `<head>
+  <meta charset="utf-8"/>
+  <meta name="viewport" content="width=device-width, initial-scale=1"/>
+  <title>${title}</title>
+  <script src="https://cdn.tailwindcss.com"></script>
+  <link rel="preconnect" href="https://fonts.googleapis.com"/>
+  <link href="https://fonts.googleapis.com/css2?family=Inter:wght@400;500;600;700&display=swap" rel="stylesheet"/>
+  <style>
+    :root { font-family: 'Inter', system-ui, sans-serif; }
+    @keyframes aurora {
+      0%   { transform: translate(0,0) scale(1); }
+      33%  { transform: translate(6%, -8%) scale(1.15); }
+      66%  { transform: translate(-8%, 6%) scale(0.9); }
+      100% { transform: translate(0,0) scale(1); }
+    }
+    @keyframes rise {
+      from { opacity: 0; transform: translateY(16px); }
+      to   { opacity: 1; transform: translateY(0); }
+    }
+    @keyframes shimmer {
+      0% { background-position: -200% 0; }
+      100% { background-position: 200% 0; }
+    }
+    .aurora { filter: blur(80px); animation: aurora 18s ease-in-out infinite; }
+    .rise { animation: rise .7s cubic-bezier(.16,1,.3,1) both; }
+    .rise-2 { animation: rise .7s cubic-bezier(.16,1,.3,1) .1s both; }
+    .rise-3 { animation: rise .7s cubic-bezier(.16,1,.3,1) .2s both; }
+    .grad-text {
+      background: linear-gradient(120deg,#7c3aed,#0891b2,#4f46e5);
+      background-size: 200% auto;
+      -webkit-background-clip: text; background-clip: text; color: transparent;
+      animation: shimmer 6s linear infinite;
+    }
+    .glass { background: rgba(255,255,255,.7); backdrop-filter: blur(16px); -webkit-backdrop-filter: blur(16px); }
+    .glow-btn { box-shadow: 0 12px 32px -10px rgba(124,58,237,.45); }
+  </style>
+</head>`;
+}
+
+/** The animated aurora background blobs, shared by both pages (soft pastels on light). */
+const AURORA = `
+  <div class="pointer-events-none fixed inset-0 overflow-hidden">
+    <div class="aurora absolute -left-32 -top-32 h-96 w-96 rounded-full bg-violet-300/50"></div>
+    <div class="aurora absolute right-0 top-1/4 h-96 w-96 rounded-full bg-cyan-300/40" style="animation-delay:-6s"></div>
+    <div class="aurora absolute bottom-0 left-1/3 h-96 w-96 rounded-full bg-indigo-300/40" style="animation-delay:-12s"></div>
+  </div>`;
+
+function renderLoginPage(config: DatabaseRouteConfig): string {
+  const feishuHref = `/auth/feishu/${encodeURIComponent(config.siloOrganizationSlug)}`;
+  const devButton = config.allowDevLoginBypass
+    ? `
+      <div class="relative my-6 rise-3">
+        <div class="absolute inset-0 flex items-center"><div class="w-full border-t border-slate-200"></div></div>
+        <div class="relative flex justify-center"><span class="bg-white/70 px-3 text-[11px] font-medium uppercase tracking-[0.2em] text-slate-400">开发模式</span></div>
+      </div>
+      <a href="/database/dev-login"
+         class="rise-3 group flex w-full items-center justify-center gap-2 rounded-xl border border-amber-300 bg-amber-50 px-4 py-3 text-sm font-semibold text-amber-700 transition hover:border-amber-400 hover:bg-amber-100">
+        <span>⚡</span> 一键登录管理员
+      </a>
+      <p class="rise-3 mt-2 text-center text-xs text-slate-400">仅开发环境可见 · 跳过飞书 OAuth</p>`
+    : "";
+
+  return `<!doctype html>
+<html lang="zh-CN">
+${pageHead("Database Admin · 登录")}
+<body class="relative min-h-screen overflow-hidden bg-gradient-to-br from-slate-50 via-white to-indigo-50 text-slate-800 flex items-center justify-center p-4">
+  ${AURORA}
+  <main class="rise glass relative w-full max-w-sm rounded-3xl border border-white/80 p-8 shadow-2xl shadow-indigo-200/50">
+    <div class="mb-7 text-center">
+      <div class="mx-auto mb-5 flex h-14 w-14 items-center justify-center rounded-2xl bg-gradient-to-br from-violet-500 to-cyan-400 text-2xl font-bold text-white glow-btn">D</div>
+      <h1 class="text-2xl font-bold tracking-tight grad-text">Database Admin</h1>
+      <p class="mt-2 text-sm text-slate-500">使用飞书登录以管理数据库</p>
+    </div>
+
+    <a href="${feishuHref}"
+       class="rise-2 glow-btn group flex w-full items-center justify-center gap-2 rounded-xl bg-gradient-to-r from-violet-500 to-indigo-500 px-4 py-3.5 text-sm font-semibold text-white transition hover:from-violet-400 hover:to-indigo-400">
+      <svg class="h-4 w-4" viewBox="0 0 24 24" fill="currentColor"><path d="M12 2 3 7v10l9 5 9-5V7l-9-5Zm0 2.3 6.5 3.6L12 11.5 5.5 7.9 12 4.3Z"/></svg>
+      使用飞书登录
+    </a>
+    ${devButton}
+  </main>
+</body>
+</html>`;
+}
+
+/** Sidebar nav items. `active` marks the current page. `href` "#" = placeholder. */
+const NAV_ITEMS: ReadonlyArray<{ label: string; icon: string; href: string; active: boolean }> = [
+  { label: "概览", icon: "M4 13h6V4H4v9Zm0 7h6v-5H4v5Zm10 0h6V11h-6v9Zm0-16v5h6V4h-6Z", href: "/database/dashboard", active: true },
+  { label: "数据表", icon: "M4 5h16v4H4V5Zm0 6h16v4H4v-4Zm0 6h16v2H4v-2Z", href: "#", active: false },
+  { label: "查询", icon: "m21 21-4.3-4.3M11 18a7 7 0 1 0 0-14 7 7 0 0 0 0 14Z", href: "#", active: false },
+  { label: "设置", icon: "M12 15a3 3 0 1 0 0-6 3 3 0 0 0 0 6Zm7-3 2 1-2 3-2-1a7 7 0 0 1-2 1l-1 2h-4l-1-2a7 7 0 0 1-2-1l-2 1-2-3 2-1a7 7 0 0 1 0-2l-2-1 2-3 2 1a7 7 0 0 1 2-1l1-2h4l1 2a7 7 0 0 1 2 1l2-1 2 3-2 1a7 7 0 0 1 0 2Z", href: "#", active: false },
+];
+
+function renderDashboard(displayName: string): string {
+  const nav = NAV_ITEMS.map((item) => {
+    const cls = item.active
+      ? "group flex items-center gap-3 rounded-xl bg-gradient-to-r from-violet-500 to-indigo-500 px-3 py-2.5 text-sm font-semibold text-white shadow-lg shadow-indigo-300/50"
+      : "group flex items-center gap-3 rounded-xl px-3 py-2.5 text-sm font-medium text-slate-500 transition hover:bg-slate-100 hover:text-slate-900";
+    return `<a href="${item.href}" class="${cls}">
+            <svg class="h-4 w-4 shrink-0" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="1.8" stroke-linecap="round" stroke-linejoin="round"><path d="${item.icon}"/></svg>
+            ${item.label}
+          </a>`;
+  }).join("\n          ");
+
+  const stats = [
+    { label: "数据表", value: "—", accent: "from-violet-200/60 to-transparent" },
+    { label: "记录数", value: "—", accent: "from-cyan-200/60 to-transparent" },
+    { label: "最近查询", value: "—", accent: "from-indigo-200/60 to-transparent" },
+  ].map((s, i) => `
+        <div class="rise-${i + 1} group relative overflow-hidden rounded-2xl border border-white/80 glass p-5 shadow-lg shadow-slate-200/50 transition hover:-translate-y-0.5 hover:shadow-xl hover:shadow-indigo-200/50">
+          <div class="absolute inset-0 bg-gradient-to-br ${s.accent} opacity-0 transition group-hover:opacity-100"></div>
+          <p class="relative text-sm text-slate-500">${s.label}</p>
+          <p class="relative mt-2 text-3xl font-bold text-slate-900">${s.value}</p>
+        </div>`).join("");
+
+  const initial = escapeHtml(displayName.slice(0, 1) || "U");
+
+  return `<!doctype html>
+<html lang="zh-CN">
+${pageHead("Database Admin · 概览")}
+<body class="relative min-h-screen overflow-hidden bg-gradient-to-br from-slate-50 via-white to-indigo-50 text-slate-700">
+  ${AURORA}
+  <div class="relative flex min-h-screen">
+    <!-- 左侧菜单栏 -->
+    <aside class="flex w-64 shrink-0 flex-col border-r border-slate-200/80 glass">
+      <div class="flex items-center gap-3 px-5 py-6">
+        <div class="flex h-10 w-10 items-center justify-center rounded-xl bg-gradient-to-br from-violet-500 to-cyan-400 text-lg font-bold text-white glow-btn">D</div>
+        <span class="text-base font-bold grad-text">Database Admin</span>
+      </div>
+      <nav class="flex flex-1 flex-col gap-1.5 px-3 py-2">
+          ${nav}
+      </nav>
+      <div class="m-3 flex items-center gap-3 rounded-xl border border-slate-200 bg-white/60 px-3 py-3">
+        <div class="flex h-9 w-9 items-center justify-center rounded-full bg-gradient-to-br from-violet-500 to-indigo-500 text-sm font-semibold text-white">${initial}</div>
+        <div class="min-w-0">
+          <p class="text-[11px] uppercase tracking-wider text-slate-400">已登录</p>
+          <p class="truncate text-sm font-medium text-slate-700">${escapeHtml(displayName)}</p>
+        </div>
+      </div>
+    </aside>
+
+    <!-- 右侧内容 -->
+    <div class="flex flex-1 flex-col">
+      <header class="flex items-center justify-between border-b border-slate-200/80 glass px-8 py-4">
+        <div>
+          <h1 class="text-lg font-bold text-slate-900">概览</h1>
+          <p class="text-xs text-slate-400">欢迎回来，这里是数据库管理台</p>
+        </div>
+        <button id="logout"
+                class="rounded-xl border border-slate-200 bg-white px-4 py-2 text-sm font-medium text-slate-600 transition hover:border-slate-300 hover:bg-slate-50 hover:text-slate-900">
+          退出登录
+        </button>
+      </header>
+
+      <main class="flex-1 p-8">
+        <div class="grid grid-cols-1 gap-5 sm:grid-cols-3">
+          ${stats}
+        </div>
+
+        <div class="rise-3 mt-6 flex h-64 items-center justify-center rounded-2xl border border-dashed border-slate-300 glass text-sm text-slate-400">
+          内容区占位 · 在 src/database/routes/databaseRoutes.ts 里继续搭建
+        </div>
+      </main>
+    </div>
+  </div>
+
+  <script>
+    document.getElementById("logout").addEventListener("click", async () => {
+      await fetch("/auth/logout", { method: "POST" });
+      window.location.href = "/database/admin";
+    });
+  </script>
+</body>
+</html>`;
+}
+
+function escapeHtml(value: string): string {
+  return value
+    .replaceAll("&", "&amp;")
+    .replaceAll("<", "&lt;")
+    .replaceAll(">", "&gt;")
+    .replaceAll('"', "&quot;");
+}

hub/src/deployment/bootstrap-silo.ts

@@ -250,6 +250,7 @@ async function initializeSilo(
       data: {
         organizationId: input.organization.id,
         name: "Inbox",
+        kind: "SYSTEM_INBOX",
         sortKey: "000000",
       },
     });

hub/src/feishu/card/builder.ts

@@ -12,6 +12,7 @@
  */
 
 import type { ToolUseTraceStep } from "./trace-store.js";
+import type { CardContentSegment } from "../outboundImages.js";
 
 // ---------------------------------------------------------------------------
 // Types
@@ -58,6 +59,7 @@ function toolIcon(toolName: string): string {
 export function buildAgentCard(params: {
   phase: CardPhase;
   text: string;
+  contentSegments?: readonly CardContentSegment[] | undefined;
   reasoningText: string | undefined;
   toolUseSteps: ToolUseTraceStep[];
   toolUseElapsedMs: number | undefined;
@@ -65,19 +67,19 @@ export function buildAgentCard(params: {
   interrupted: boolean | undefined;
   runId: string | undefined;
 }): Record<string, unknown> {
-  const { phase, text, reasoningText, toolUseSteps, toolUseElapsedMs, isError, interrupted } = params;
+  const { phase, text, contentSegments, reasoningText, toolUseSteps, toolUseElapsedMs, isError, interrupted } = params;
   const elements: unknown[] = [];
 
   // Tool-use panel (always present if there are steps)
   if (toolUseSteps.length > 0) {
     elements.push(buildToolUsePanel(toolUseSteps, toolUseElapsedMs, phase !== "complete"));
-  } else if (phase === "thinking" || (phase === "streaming" && text === "")) {
+  } else if (phase === "thinking" || (phase === "streaming" && text === "" && (contentSegments === undefined || contentSegments.length === 0))) {
     elements.push(buildPendingToolUsePanel());
   }
 
   // Reasoning panel
   if (reasoningText !== undefined && reasoningText !== "") {
-    if (phase === "streaming" && text === "") {
+    if (phase === "streaming" && text === "" && (contentSegments === undefined || contentSegments.length === 0)) {
       // Still thinking: show reasoning inline
       elements.push({
         tag: "markdown",
@@ -90,12 +92,11 @@ export function buildAgentCard(params: {
     }
   }
 
-  // Main text content
+  // Main answer: either materialized segments (markdown + Feishu-hosted images)
-  if (text !== "") {
+  // or a single markdown block.
-    elements.push({
+  const answerElements = buildAnswerElements(text, contentSegments);
-      tag: "markdown",
+  if (answerElements.length > 0) {
-      content: truncateText(text, MAX_TEXT_LENGTH),
+    elements.push(...answerElements);
-    });
   } else if (phase === "thinking" && toolUseSteps.length === 0 && (reasoningText === undefined || reasoningText === "")) {
     elements.push({
       tag: "markdown",
@@ -401,6 +402,43 @@ function escapeMarkdown(value: string): string {
   return value.replace(/\\/g, "\\\\").replace(/([`*_{}[\]<>])/g, "\\$1");
 }
 
+function buildAnswerElements(
+  text: string,
+  contentSegments: readonly CardContentSegment[] | undefined,
+): unknown[] {
+  if (contentSegments !== undefined && contentSegments.length > 0) {
+    const elements: unknown[] = [];
+    let remaining = MAX_TEXT_LENGTH;
+    for (const segment of contentSegments) {
+      if (segment.type === "image") {
+        elements.push({
+          tag: "img",
+          img_key: segment.imgKey,
+          alt: { tag: "plain_text", content: segment.alt },
+          mode: "fit_horizontal",
+          preview: true,
+        });
+        continue;
+      }
+      if (segment.content === "" || remaining <= 0) continue;
+      const slice = segment.content.length <= remaining
+        ? segment.content
+        : truncateText(segment.content, remaining);
+      remaining -= slice.length;
+      elements.push({
+        tag: "markdown",
+        content: slice,
+      });
+    }
+    return elements;
+  }
+  if (text === "") return [];
+  return [{
+    tag: "markdown",
+    content: truncateText(text, MAX_TEXT_LENGTH),
+  }];
+}
+
 function truncateText(value: string, maxLength: number): string {
   return value.length <= maxLength ? value : `${value.slice(0, maxLength - 3)}...`;
 }

hub/src/feishu/card/streaming-card.ts

@@ -18,10 +18,13 @@
  *   4. onToolEnd(name, id, input, result?, error?) — complete a tool step
  *   5. finish(finalText)    — flush + transition to complete card
  *   6. fail(errorText)      — flush + transition to error card
+ *
+ * On finish, markdown image references (`![](url|path)`) are downloaded /
+ * read, uploaded to Feishu as message images, and embedded as native card
+ * `img` elements so external URLs never hit Feishu content-security checks.
  */
-
 import type { FeishuRuntime, SendMessageOptions } from "../client.js";
-import { sendCard, patchCard, sendText } from "../client.js";
+import { sendCard, patchCard, sendText, sendLongText } from "../client.js";
 import { DEFAULT_MAX_MESSAGE_LENGTH, splitAtBoundary } from "../textStream.js";
 import {
   startToolUseTraceRun,
@@ -31,6 +34,12 @@ import {
   getToolUseTraceSteps,
 } from "./trace-store.js";
 import { buildAgentCard, type CardPhase } from "./builder.js";
+import {
+  type CardContentSegment,
+  maskMarkdownImagesForStreaming,
+  materializeAnswerSegments,
+  sendImageMessage,
+} from "../outboundImages.js";
 
 export interface StreamingCardSink {
   readonly create: (card: Record<string, unknown>) => Promise<string | null>;
@@ -44,6 +53,11 @@ export interface StreamingCardOptions {
   readonly sendOptions?: SendMessageOptions | undefined;
   readonly patchIntervalMs: number | undefined;
   readonly maxMessageLength: number | undefined;
+  /** Project workspace root; required to resolve local image paths. */
+  readonly workspaceRoot?: string | undefined;
+  /** Project workspace directory; required to resolve local image paths. */
+  readonly workspaceDir?: string | undefined;
+  readonly maxImageBytes?: number | undefined;
 }
 
 const DEFAULT_PATCH_INTERVAL_MS = 400;
@@ -65,6 +79,9 @@ export class StreamingAgentCard {
   private readonly sendOptions: SendMessageOptions | undefined;
   private readonly patchIntervalMs: number;
   private readonly maxMessageLength: number;
+  private readonly workspaceRoot: string | undefined;
+  private readonly workspaceDir: string | undefined;
+  private readonly maxImageBytes: number | undefined;
 
   constructor(options: StreamingCardOptions) {
     this.runId = options.runId;
@@ -73,6 +90,9 @@ export class StreamingAgentCard {
     this.sendOptions = options.sendOptions;
     this.patchIntervalMs = options.patchIntervalMs ?? DEFAULT_PATCH_INTERVAL_MS;
     this.maxMessageLength = options.maxMessageLength ?? DEFAULT_MAX_MESSAGE_LENGTH;
+    this.workspaceRoot = options.workspaceRoot;
+    this.workspaceDir = options.workspaceDir;
+    this.maxImageBytes = options.maxImageBytes;
     startToolUseTraceRun(this.runId);
   }
 
@@ -106,23 +126,43 @@ export class StreamingAgentCard {
     recordToolUseEnd({ runId: this.runId, ...params });
     this.scheduleFlush();
   }
-  async finish(fallbackText: string, options: { readonly interrupted?: boolean; readonly footerText?: string | undefined } = {}): Promise<void> {
+
+  async finish(
+    fallbackText: string,
+    options: { readonly interrupted?: boolean; readonly footerText?: string | undefined } = {},
+  ): Promise<void> {
     await this.flushChain;
     this.interrupted = options.interrupted === true;
     const footerText = options.footerText ?? "";
     const fallbackWithFooter = appendFooter(fallbackText, footerText);
     try {
+      let answerText =
+        this.text.length > 0 ? appendFooter(this.text, footerText) : fallbackWithFooter;
+      this.text = answerText;
+
+      const { segments, unresolved } = await materializeAnswerSegments(answerText, {
+        rt: this.rt,
+        workspaceRoot: this.workspaceRoot,
+        workspaceDir: this.workspaceDir,
+        maxImageBytes: this.maxImageBytes,
+      });
+      if (unresolved.length > 0) {
+        this.rt.logger.warn(
+          { runId: this.runId, unresolvedCount: unresolved.length, unresolved: unresolved.slice(0, 5) },
+          "some answer images could not be uploaded to Feishu",
+        );
+      }
+
       let updated = true;
-      if (this.text.length > 0) {
+      if (answerText.length > 0 || segments.length > 0) {
-        this.text = appendFooter(this.text, footerText);
+        updated = await this.flushCard("complete", answerText, false, segments);
-        updated = await this.flushCard("complete", this.text);
-      } else if (this.currentMessageId === null && fallbackWithFooter.length > 0) {
-        // No streaming text was sent. If we never created a card, send one now.
-        this.text = fallbackWithFooter;
-        updated = await this.flushCard("complete", this.text);
       } else if (this.currentMessageId !== null) {
-        // Patch the existing card with the final text.
+        updated = await this.flushCard("complete", "", false, []);
-        updated = await this.flushCard("complete", fallbackWithFooter);
+      }
+
+      if (!updated) {
+        // Card path failed (e.g. residual content policy). Deliver text + standalone images.
+        updated = await this.deliverPlainFallback(segments, answerText);
       }
       if (!updated && this.interrupted) {
         await sendText(this.rt, this.chatId, "\u5DF2\u4E2D\u65AD\u5F53\u524D\u8FD0\u884C\u3002", this.sendOptions);
@@ -166,15 +206,30 @@ export class StreamingAgentCard {
     return this.flushCard(this.currentPhase(), this.text);
   }
 
-  private async flushCard(phase: CardPhase, text: string, isError = false): Promise<boolean> {
+  private async flushCard(
-    const chunks = splitAtBoundary(text, this.maxMessageLength);
+    phase: CardPhase,
-    const firstChunk = chunks[0];
+    text: string,
-    if (firstChunk === undefined) return true;
+    isError = false,
+    contentSegments?: readonly CardContentSegment[],
+  ): Promise<boolean> {
+    // During live streaming, strip image URLs so Feishu never fetches remote
+    // ranks mid-run. Materialized segments are only used on the complete pass.
+    const displayText =
+      phase === "complete" && contentSegments !== undefined
+        ? text
+        : maskMarkdownImagesForStreaming(text);
 
+    const chunks = splitAtBoundary(displayText, this.maxMessageLength);
+    const firstChunk = chunks[0] ?? "";
+    // When we have segments (complete+images), keep first-card complete content
+    // on segments only; overflow text (rare) falls back to plain chunked cards.
     const toolUseSteps = getToolUseTraceSteps(this.runId);
     const card = buildAgentCard({
       phase,
-      text: firstChunk,
+      text: contentSegments !== undefined && contentSegments.length > 0 ? "" : firstChunk,
+      contentSegments: contentSegments !== undefined && contentSegments.length > 0
+        ? contentSegments
+        : undefined,
       reasoningText: this.reasoningText || undefined,
       toolUseSteps,
       toolUseElapsedMs: this.toolUseElapsedMs,
@@ -186,7 +241,9 @@ export class StreamingAgentCard {
     if (this.currentMessageId === null) {
       this.currentMessageId = await sendCard(this.rt, this.chatId, card, this.sendOptions);
       let updated = this.currentMessageId !== null;
-      // Send overflow chunks as new messages (rare for agent output)
+      // Send overflow chunks as new messages (rare for agent output). Segments
+      // already include the whole answer; only plain text overflows.
+      if (contentSegments === undefined || contentSegments.length === 0) {
         for (const chunk of chunks.slice(1)) {
           const overflowCard = buildAgentCard({
             phase,
@@ -202,10 +259,12 @@ export class StreamingAgentCard {
           updated = updated && overflowMessageId !== null;
           this.currentMessageId = overflowMessageId;
         }
+      }
       return updated;
-    } else {
+    }
+
     let updated = await patchCard(this.rt, this.currentMessageId, card);
-      // For overflow, create new messages
+    if (contentSegments === undefined || contentSegments.length === 0) {
       for (const chunk of chunks.slice(1)) {
         const overflowCard = buildAgentCard({
           phase,
@@ -221,8 +280,50 @@ export class StreamingAgentCard {
         updated = updated && overflowMessageId !== null;
         this.currentMessageId = overflowMessageId;
       }
+    }
     return updated;
   }
+
+  private async deliverPlainFallback(
+    segments: readonly CardContentSegment[],
+    answerText: string,
+  ): Promise<boolean> {
+    const textParts: string[] = [];
+    const imageKeys: string[] = [];
+    if (segments.length > 0) {
+      for (const segment of segments) {
+        if (segment.type === "markdown") {
+          if (segment.content.trim() !== "") textParts.push(segment.content);
+        } else {
+          imageKeys.push(segment.imgKey);
+        }
+      }
+    } else if (answerText.trim() !== "") {
+      textParts.push(maskMarkdownImagesForStreaming(answerText));
+    }
+
+    let any = false;
+    if (textParts.length > 0) {
+      const messageId = await sendLongText(
+        this.rt,
+        this.chatId,
+        textParts.join("\n\n"),
+        this.sendOptions,
+      );
+      any = messageId !== null;
+    }
+    for (const imageKey of imageKeys) {
+      try {
+        const messageId = await sendImageMessage(this.rt, this.chatId, imageKey, this.sendOptions);
+        any = any || messageId !== null;
+      } catch (error) {
+        this.rt.logger.warn(
+          { runId: this.runId, err: error instanceof Error ? error.message : String(error) },
+          "standalone image fallback failed",
+        );
+      }
+    }
+    return any;
   }
 
   private currentPhase(): CardPhase {
@@ -235,5 +336,5 @@ export class StreamingAgentCard {
 function appendFooter(text: string, footerText: string): string {
   if (footerText === "") return text;
   if (text === "") return footerText;
-  return `${text.trimEnd()}\n\n${footerText}`;
+  return `${text}\n\n${footerText}`;
 }

hub/src/feishu/client.ts

@@ -316,7 +316,8 @@ export async function sendCard(
       { msgType: "interactive", content: JSON.stringify(card) },
       options,
     );
-  } catch {
+  } catch (e) {
+    rt.logger.warn({ chatId, err: errorText(e) }, "sendCard failed");
     return null;
   }
 }
@@ -334,7 +335,7 @@ export async function patchCard(rt: FeishuRuntime, messageId: string, card: Reco
     });
     return true;
   } catch (e) {
-    rt.logger.warn({ messageId, err: e instanceof Error ? e.message : String(e) }, "patchCard failed");
+    rt.logger.warn({ messageId, err: errorText(e) }, "patchCard failed");
     return false;
   }
 }

hub/src/feishu/outboundImages.ts

@@ -0,0 +1,389 @@
+/**
+ * Resolve markdown image references in agent answers into Feishu-hosted
+ * image_keys so cards can embed them without remote URLs (which trip Feishu
+ * content-security controls).
+ */
+import { isIP } from "node:net";
+import type { FeishuRuntime } from "./client.js";
+import { withRetry } from "./client.js";
+import {
+  WorkspaceFileBoundaryError,
+  readWorkspaceFileNoFollow,
+} from "../security/workspaceFiles.js";
+
+export const FEISHU_MAX_IMAGE_BYTES = 10 * 1024 * 1024;
+export const DEFAULT_MAX_OUTBOUND_IMAGES = 10;
+
+const IMAGE_MARKDOWN_RE = /!\[([^\]\n]*)\]\(([^)\n]+)\)/g;
+const FENCED_CODE_RE = /```[\s\S]*?```/g;
+
+export type CardContentSegment =
+  | { readonly type: "markdown"; readonly content: string }
+  | { readonly type: "image"; readonly imgKey: string; readonly alt: string };
+
+export interface MarkdownImageRef {
+  readonly fullMatch: string;
+  readonly alt: string;
+  readonly src: string;
+  readonly index: number;
+  readonly length: number;
+}
+
+export interface OutboundImageContext {
+  readonly rt: FeishuRuntime;
+  readonly workspaceRoot?: string | undefined;
+  readonly workspaceDir?: string | undefined;
+  readonly maxImageBytes?: number | undefined;
+  readonly maxImages?: number | undefined;
+  readonly fetchImpl?: typeof fetch | undefined;
+}
+
+type ImageCreateResponse = {
+  image_key?: string;
+  data?: { image_key?: string };
+} | null;
+
+type MessageCreateResponse = {
+  message_id?: string;
+  data?: { message_id?: string };
+} | null;
+
+/** Streaming-safe view: drop markdown image URLs so partial cards do not hit Feishu URL checks. */
+export function maskMarkdownImagesForStreaming(text: string): string {
+  return rewriteMarkdownImagesOutsideCode(text, (ref) => {
+    const alt = ref.alt.trim();
+    return alt === "" ? "\u3010\u56fe\u7247\u3011" : alt;
+  });
+}
+
+export function findMarkdownImagesOutsideCode(text: string): MarkdownImageRef[] {
+  const blocked = blockedRanges(text);
+  const refs: MarkdownImageRef[] = [];
+  IMAGE_MARKDOWN_RE.lastIndex = 0;
+  let match: RegExpExecArray | null;
+  while ((match = IMAGE_MARKDOWN_RE.exec(text)) !== null) {
+    const index = match.index;
+    if (blocked.some((range) => index >= range.start && index < range.end)) continue;
+    const fullMatch = match[0];
+    const alt = match[1] ?? "";
+    const rawSrc = (match[2] ?? "").trim();
+    const src = stripUrlTitle(rawSrc);
+    if (src === "") continue;
+    refs.push({ fullMatch, alt, src, index, length: fullMatch.length });
+  }
+  return refs;
+}
+
+/**
+ * Upload reachable markdown images and split the answer into card segments
+ * (markdown + Feishu img elements). Unresolved images become visible alt text.
+ */
+export async function materializeAnswerSegments(
+  text: string,
+  ctx: OutboundImageContext,
+): Promise<{ segments: CardContentSegment[]; unresolved: string[] }> {
+  const refs = findMarkdownImagesOutsideCode(text);
+  if (refs.length === 0) {
+    return {
+      segments: text === "" ? [] : [{ type: "markdown", content: text }],
+      unresolved: [],
+    };
+  }
+
+  const maxImages = ctx.maxImages ?? DEFAULT_MAX_OUTBOUND_IMAGES;
+  const maxBytes = ctx.maxImageBytes ?? FEISHU_MAX_IMAGE_BYTES;
+  const keyBySrc = new Map<string, string>();
+  const unresolved: string[] = [];
+  const uniqueSrcs: string[] = [];
+  for (const ref of refs) {
+    if (!uniqueSrcs.includes(ref.src)) uniqueSrcs.push(ref.src);
+  }
+
+  for (const src of uniqueSrcs.slice(0, maxImages)) {
+    try {
+      const bytes = await resolveOutboundImageBytes(src, ctx, maxBytes);
+      if (bytes === null) {
+        unresolved.push(src);
+        continue;
+      }
+      const imageKey = await uploadMessageImage(ctx.rt, bytes);
+      keyBySrc.set(src, imageKey);
+    } catch (error) {
+      ctx.rt.logger.warn(
+        { src, err: error instanceof Error ? error.message : String(error) },
+        "outbound image materialize failed",
+      );
+      unresolved.push(src);
+    }
+  }
+  for (const src of uniqueSrcs.slice(maxImages)) {
+    unresolved.push(src);
+  }
+
+  const segments: CardContentSegment[] = [];
+  let cursor = 0;
+  for (const ref of refs) {
+    if (ref.index > cursor) {
+      pushMarkdown(segments, text.slice(cursor, ref.index));
+    }
+    const imageKey = keyBySrc.get(ref.src);
+    if (imageKey !== undefined) {
+      segments.push({
+        type: "image",
+        imgKey: imageKey,
+        alt: ref.alt.trim() === "" ? "\u56fe\u7247" : ref.alt.trim(),
+      });
+    } else {
+      const alt = ref.alt.trim();
+      pushMarkdown(segments, alt === "" ? "\u3010\u56fe\u7247\u3011" : alt);
+    }
+    cursor = ref.index + ref.length;
+  }
+  if (cursor < text.length) {
+    pushMarkdown(segments, text.slice(cursor));
+  }
+  return { segments, unresolved };
+}
+
+export async function uploadMessageImage(rt: FeishuRuntime, image: Buffer): Promise<string> {
+  if (image.byteLength === 0) {
+    throw new Error("image is empty");
+  }
+  if (image.byteLength > FEISHU_MAX_IMAGE_BYTES) {
+    throw new Error(`image exceeds Feishu limit of ${FEISHU_MAX_IMAGE_BYTES} bytes`);
+  }
+  const client = rt.client as unknown as {
+    im: { v1: { image: { create: (p: unknown) => Promise<ImageCreateResponse> } } };
+  };
+  const res = await withRetry(async () =>
+    client.im.v1.image.create({
+      data: { image_type: "message", image },
+    }),
+  );
+  const imageKey = res?.image_key ?? res?.data?.image_key;
+  if (imageKey === undefined || imageKey === "") {
+    throw new Error("Feishu image upload response is missing image_key");
+  }
+  return imageKey;
+}
+
+/** Send a standalone image message (fallback if card embed is unavailable). */
+export async function sendImageMessage(
+  rt: FeishuRuntime,
+  chatId: string,
+  imageKey: string,
+  options?: { readonly replyToMessageId?: string | undefined },
+): Promise<string | null> {
+  const client = rt.client as unknown as {
+    im: {
+      v1: {
+        message: {
+          create: (p: unknown) => Promise<MessageCreateResponse>;
+          reply: (p: unknown) => Promise<MessageCreateResponse>;
+        };
+      };
+    };
+  };
+  const replyTo = options?.replyToMessageId;
+  if (replyTo !== undefined && replyTo !== "") {
+    const res = await client.im.v1.message.reply({
+      path: { message_id: replyTo },
+      data: { msg_type: "image", content: JSON.stringify({ image_key: imageKey }) },
+    });
+    return res?.data?.message_id ?? res?.message_id ?? null;
+  }
+  const res = await client.im.v1.message.create({
+    params: { receive_id_type: "chat_id" },
+    data: {
+      receive_id: chatId,
+      msg_type: "image",
+      content: JSON.stringify({ image_key: imageKey }),
+    },
+  });
+  return res?.data?.message_id ?? res?.message_id ?? null;
+}
+
+export async function resolveOutboundImageBytes(
+  src: string,
+  ctx: OutboundImageContext,
+  maxBytes: number,
+): Promise<Buffer | null> {
+  if (isRemoteUrl(src)) {
+    return fetchRemoteImage(src, ctx.fetchImpl ?? fetch, maxBytes);
+  }
+  const root = ctx.workspaceRoot?.trim();
+  const dir = ctx.workspaceDir?.trim();
+  if (root === undefined || root === "" || dir === undefined || dir === "") {
+    return null;
+  }
+  try {
+    const file = await readWorkspaceFileNoFollow(root, dir, src, maxBytes);
+    return file.data;
+  } catch (error) {
+    if (error instanceof WorkspaceFileBoundaryError && error.reason === "not_found") {
+      return null;
+    }
+    throw error;
+  }
+}
+
+function rewriteMarkdownImagesOutsideCode(
+  text: string,
+  replace: (ref: MarkdownImageRef) => string,
+): string {
+  const refs = findMarkdownImagesOutsideCode(text);
+  if (refs.length === 0) return text;
+  let out = "";
+  let cursor = 0;
+  for (const ref of refs) {
+    out += text.slice(cursor, ref.index);
+    out += replace(ref);
+    cursor = ref.index + ref.length;
+  }
+  out += text.slice(cursor);
+  return out;
+}
+
+function pushMarkdown(segments: CardContentSegment[], content: string): void {
+  if (content === "") return;
+  const last = segments[segments.length - 1];
+  if (last !== undefined && last.type === "markdown") {
+    segments[segments.length - 1] = { type: "markdown", content: last.content + content };
+    return;
+  }
+  segments.push({ type: "markdown", content });
+}
+
+function blockedRanges(text: string): Array<{ start: number; end: number }> {
+  const ranges: Array<{ start: number; end: number }> = [];
+  FENCED_CODE_RE.lastIndex = 0;
+  let match: RegExpExecArray | null;
+  while ((match = FENCED_CODE_RE.exec(text)) !== null) {
+    ranges.push({ start: match.index, end: match.index + match[0].length });
+  }
+  return ranges;
+}
+
+function stripUrlTitle(raw: string): string {
+  const trimmed = raw.trim();
+  // Markdown optional title: url "title" or url 'title'
+  const titled = /^(\S+)\s+(".*"|'.*')$/.exec(trimmed);
+  return (titled?.[1] ?? trimmed).trim();
+}
+
+function isRemoteUrl(src: string): boolean {
+  try {
+    const url = new URL(src);
+    return url.protocol === "http:" || url.protocol === "https:";
+  } catch {
+    return false;
+  }
+}
+
+async function fetchRemoteImage(
+  src: string,
+  fetchImpl: typeof fetch,
+  maxBytes: number,
+): Promise<Buffer | null> {
+  let url: URL;
+  try {
+    url = new URL(src);
+  } catch {
+    return null;
+  }
+  if (url.protocol !== "http:" && url.protocol !== "https:") return null;
+  if (!isPublicHttpHost(url.hostname)) return null;
+
+  const controller = new AbortController();
+  const timer = setTimeout(() => controller.abort(), 15_000);
+  try {
+    const response = await fetchImpl(url, {
+      method: "GET",
+      redirect: "manual",
+      signal: controller.signal,
+      headers: { accept: "image/*,*/*;q=0.8" },
+    });
+    // One safe redirect hop to another public http(s) host.
+    if (response.status >= 300 && response.status < 400) {
+      const location = response.headers.get("location");
+      if (location === null || location === "") return null;
+      let redirected: URL;
+      try {
+        redirected = new URL(location, url);
+      } catch {
+        return null;
+      }
+      if (redirected.protocol !== "http:" && redirected.protocol !== "https:") return null;
+      if (!isPublicHttpHost(redirected.hostname)) return null;
+      const second = await fetchImpl(redirected, {
+        method: "GET",
+        redirect: "manual",
+        signal: controller.signal,
+        headers: { accept: "image/*,*/*;q=0.8" },
+      });
+      return readImageBody(second, maxBytes);
+    }
+    return readImageBody(response, maxBytes);
+  } finally {
+    clearTimeout(timer);
+  }
+}
+
+async function readImageBody(response: Response, maxBytes: number): Promise<Buffer | null> {
+  if (!response.ok) return null;
+  const contentType = (response.headers.get("content-type") ?? "").toLowerCase();
+  if (
+    contentType !== "" &&
+    !contentType.startsWith("image/") &&
+    !contentType.includes("octet-stream") &&
+    (contentType.startsWith("text/") || contentType.includes("json") || contentType.includes("html"))
+  ) {
+    return null;
+  }
+  const contentLength = Number(response.headers.get("content-length") ?? "NaN");
+  if (Number.isFinite(contentLength) && contentLength > maxBytes) return null;
+  const buf = Buffer.from(await response.arrayBuffer());
+  if (buf.byteLength === 0 || buf.byteLength > maxBytes) return null;
+  return buf;
+}
+
+function isPublicHttpHost(hostname: string): boolean {
+  const host = hostname.trim().toLowerCase().replace(/\.$/, "");
+  if (host === "" || host === "localhost" || host.endsWith(".localhost") || host.endsWith(".local")) {
+    return false;
+  }
+  if (host === "0.0.0.0" || host === "::" || host === "[::]" || host === "::1" || host === "[::1]") {
+    return false;
+  }
+  const unbracketed = host.startsWith("[") && host.endsWith("]") ? host.slice(1, -1) : host;
+  const ipVersion = isIP(unbracketed);
+  if (ipVersion === 4) return !isPrivateIPv4(unbracketed);
+  if (ipVersion === 6) return !isPrivateIPv6(unbracketed);
+  return true;
+}
+
+function isPrivateIPv4(ip: string): boolean {
+  const parts = ip.split(".").map((part) => Number(part));
+  if (parts.length !== 4 || parts.some((part) => !Number.isInteger(part) || part < 0 || part > 255)) {
+    return true;
+  }
+  const a = parts[0]!;
+  const b = parts[1]!;
+  if (a === 10 || a === 127 || a === 0) return true;
+  if (a === 169 && b === 254) return true;
+  if (a === 172 && b >= 16 && b <= 31) return true;
+  if (a === 192 && b === 168) return true;
+  if (a === 100 && b >= 64 && b <= 127) return true; // CGNAT
+  if (a >= 224) return true; // multicast / reserved
+  return false;
+}
+
+function isPrivateIPv6(ip: string): boolean {
+  const normalized = ip.toLowerCase();
+  if (normalized === "::1") return true;
+  if (normalized.startsWith("fc") || normalized.startsWith("fd")) return true; // unique local
+  if (normalized.startsWith("fe80:")) return true; // link-local
+  const mapped = /^:ffff:(\d+\.\d+\.\d+\.\d+)$/i.exec(normalized);
+  if (mapped?.[1] !== undefined) return isPrivateIPv4(mapped[1]);
+  return false;
+}

hub/src/feishu/trigger.ts

@@ -496,6 +496,9 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
       sendOptions,
       patchIntervalMs: undefined,
       maxMessageLength: undefined,
+      workspaceRoot: projectWorkspaceRoot,
+      workspaceDir: project.workspaceDir,
+      maxImageBytes: deps.resourceLimits?.maxBytesPerFile,
     });
     const fileDeliveryMcpServer = createFileDeliveryMcpServer({
       rt,

hub/src/hub.ts

@@ -1,5 +1,6 @@
 import Fastify from "fastify";
 import { registerAdminPlugin } from "./admin/plugin.js";
+import { registerDatabasePlugin } from "./database/plugin.js";
 import { prisma } from "./db.js";
 import { createLarkClient, startFeishuListenerWithClient } from "./feishu/client.js";
 import { archiveFeishuBindingForLifecycleEvent } from "./feishu/bindingLifecycle.js";
@@ -143,6 +144,14 @@ export async function startHub(): Promise<void> {
     secretEnvelope,
   });
 
+  // `/database/*` surface. Registered after the admin plugin so the
+  // @fastify/cookie parser and /auth/* login routes are already available.
+  await registerDatabasePlugin(app, {
+    prisma,
+    sessionSecret,
+    siloOrganizationSlug: siloOrganization.slug,
+  });
+
   const feishuListenerEnabled = booleanEnv("HUB_FEISHU_LISTENER_ENABLED", true);
   if (feishuListenerEnabled) {
     const feishuConfig = {

hub/src/org/capacityPolicy.ts

@@ -1,9 +1,9 @@
 /**
- * Org capacity policy service (ADR-0022 / spec `Spec.System.Capacity`).
+ * Org capacity policy service (ADR-0022).
  *
  * Stores per-Organization lower `organizationLimit` overrides per
- * `CapacityDimension`. Enforces `LayeredLimit.Valid`: a set limit must be ≤ the
+ * `CapacityDimension`. Enforces the layered-limit invariant: a set limit must be ≤ the
- * platform ceiling for that dimension. `LayeredLimit.effective` (min of the two)
+ * platform ceiling for that dimension. The effective limit (min of the two)
  * is the value capacity admission should use; dimensions with no org override
  * fall back to the platform ceiling.
  */

hub/src/org/members.ts

@@ -1,7 +1,7 @@
 /**
  * Organization membership management for org admin (ADR-0021).
  *
- * Role rules (product pin, not yet in Lean):
+ * Role rules (product pin, not yet recorded in an ADR):
  * 1. Actor must be OWNER or ADMIN (enforced at HTTP layer).
  * 2. Only OWNER can grant/revoke OWNER or modify another OWNER.
  * 3. Cannot revoke or demote the last remaining OWNER.

hub/src/projectOnboarding.ts

@@ -558,6 +558,26 @@ async function ensureInboxFolder(prisma: Prisma.TransactionClient, organizationI
     select: { id: true },
   });
   if (existing !== null) return existing;
+
+  // Bootstrap once created a root "Inbox" without kind=SYSTEM_INBOX. Sibling-name
+  // uniqueness then makes a second create fail. Recover by promoting that row.
+  const legacyRootInbox = await prisma.folder.findFirst({
+    where: {
+      organizationId,
+      parentId: null,
+      name: "Inbox",
+      archivedAt: null,
+    },
+    select: { id: true },
+  });
+  if (legacyRootInbox !== null) {
+    return prisma.folder.update({
+      where: { id: legacyRootInbox.id },
+      data: { kind: "SYSTEM_INBOX" },
+      select: { id: true },
+    });
+  }
+
   return prisma.folder.create({
     data: { organizationId, name: "Inbox", kind: "SYSTEM_INBOX", sortKey: "000000" },
     select: { id: true },

hub/test/integration/admin-auth.test.ts

@@ -170,7 +170,7 @@ describe("admin auth + org API guards", () => {
     try {
       const res = await app.inject({
         method: "GET",
-        url: "/auth/feishu?returnTo=/admin/org/test-default",
+        url: "/auth/feishu?returnTo=/admin",
       });
       expect(res.statusCode).toBe(302);
       const location = res.headers.location;
@@ -233,7 +233,7 @@ describe("admin auth + org API guards", () => {
     try {
       const nonce = "nonce-test-1";
       const state = signOAuthState(
-        { nonce, returnTo: "/admin/org/test-default" },
+        { nonce, returnTo: "/admin" },
         SESSION_SECRET,
       );
       const res = await app.inject({
@@ -242,7 +242,7 @@ describe("admin auth + org API guards", () => {
         headers: { cookie: `${OAUTH_STATE_COOKIE_NAME}=${nonce}` },
       });
       expect(res.statusCode).toBe(302);
-      expect(res.headers.location).toBe("/admin/org/test-default");
+      expect(res.headers.location).toBe("/admin");
       expect(JSON.stringify(res.headers["set-cookie"])).toContain("cph_session=");
 
       const user = await prisma.user.findUnique({ where: { feishuOpenId: "ou_new" } });
@@ -293,7 +293,7 @@ describe("admin auth + org API guards", () => {
     try {
       const start = await app.inject({
         method: "GET",
-        url: "/auth/feishu/test-default?returnTo=/admin/org/test-default/settings",
+        url: "/auth/feishu/test-default?returnTo=/admin/settings",
       });
       expect(start.statusCode).toBe(302);
       const authorize = new URL(String(start.headers.location));
@@ -308,7 +308,7 @@ describe("admin auth + org API guards", () => {
         headers: { cookie: nonceCookie },
       });
       expect(callback.statusCode).toBe(302);
-      expect(callback.headers.location).toBe("/admin/org/test-default/settings");
+      expect(callback.headers.location).toBe("/admin/settings");
       const sessionCookie = cookiePair(callback.headers["set-cookie"], "cph_session");
       const me = await app.inject({ method: "GET", url: "/api/me", headers: { cookie: sessionCookie } });
       expect(me.statusCode).toBe(200);
@@ -346,7 +346,7 @@ describe("admin auth + org API guards", () => {
         headers: { cookie: cookiePair(defaultStart.headers["set-cookie"], OAUTH_STATE_COOKIE_NAME) },
       });
       expect(defaultCallback.statusCode).toBe(302);
-      expect(defaultCallback.headers.location).toBe("/admin/org/test-default");
+      expect(defaultCallback.headers.location).toBe("/admin");
 
       await connections.disable({ organizationId: DEFAULT_ORG_ID, actorUserId: "scoped-owner" });
       const revoked = await app.inject({ method: "GET", url: "/api/me", headers: { cookie: sessionCookie } });

hub/test/integration/project-onboarding.test.ts

@@ -101,6 +101,43 @@ describe("ADR-0021 project onboarding", () => {
     ]));
   });
 
+  it("promotes a legacy root Inbox when Feishu chat creates a project", async () => {
+    await seedUser("u-member", "ou_member", "MEMBER");
+    // Production drift after bootstrap omitted kind=SYSTEM_INBOX. The protect
+    // trigger refuses demotion, so the test plants the legacy shape directly.
+    await prisma.$executeRawUnsafe(`ALTER TABLE "Folder" DISABLE TRIGGER cph_protect_system_inbox`);
+    try {
+      await prisma.folder.updateMany({
+        where: { organizationId: DEFAULT_ORG_ID, kind: "SYSTEM_INBOX", archivedAt: null },
+        data: { kind: "REGULAR" },
+      });
+    } finally {
+      await prisma.$executeRawUnsafe(`ALTER TABLE "Folder" ENABLE TRIGGER cph_protect_system_inbox`);
+    }
+    const legacy = await prisma.folder.findFirstOrThrow({
+      where: { organizationId: DEFAULT_ORG_ID, parentId: null, name: "Inbox", archivedAt: null },
+      select: { id: true, kind: true },
+    });
+    expect(legacy.kind).toBe("REGULAR");
+
+    const result = await createProjectFromFeishuChat(prisma, {
+      organizationId: DEFAULT_ORG_ID,
+      actorFeishuOpenId: "ou_member",
+      chatId: "chat-legacy-inbox",
+      name: "Recovered Inbox Project",
+      workspaceRoot: await tempWorkspaceRoot(),
+    });
+
+    expect(result.folderId).toBe(legacy.id);
+    await expect(prisma.folder.findUniqueOrThrow({
+      where: { id: legacy.id },
+      select: { kind: true },
+    })).resolves.toEqual({ kind: "SYSTEM_INBOX" });
+    expect(await prisma.folder.count({
+      where: { organizationId: DEFAULT_ORG_ID, name: "Inbox", archivedAt: null },
+    })).toBe(1);
+  });
+
   it("blocks ordinary Feishu project creation when the org setting is off", async () => {
     await seedUser("u-member", "ou_member", "MEMBER");
     await setMembersCanCreateProjects(prisma, {

hub/test/integration/silo-bootstrap.test.ts

@@ -62,6 +62,11 @@ describe("Alpha Silo bootstrap", () => {
       { roleId: "draft", label: "草稿", isDefault: true },
       { roleId: "review", label: "审校", isDefault: false },
     ]);
+    await expect(prisma.folder.findMany({
+      where: { organizationId: "org_alpha", archivedAt: null },
+      select: { name: true, kind: true, parentId: true },
+    })).resolves.toEqual([{ name: "Inbox", kind: "SYSTEM_INBOX", parentId: null }]);
+
 
     const persisted = JSON.stringify({
       feishu: await prisma.feishuApplicationCredentialVersion.findMany(),

hub/test/unit/feishu-outbound-images.test.ts

@@ -0,0 +1,163 @@
+import { mkdir, mkdtemp, rm, writeFile } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { afterEach, describe, expect, it, vi } from "vitest";
+import type { FeishuRuntime } from "../../src/feishu/client.js";
+import {
+  findMarkdownImagesOutsideCode,
+  maskMarkdownImagesForStreaming,
+  materializeAnswerSegments,
+  uploadMessageImage,
+} from "../../src/feishu/outboundImages.js";
+import { buildAgentCard } from "../../src/feishu/card/builder.js";
+
+const temps: string[] = [];
+
+afterEach(async () => {
+  await Promise.all(temps.splice(0).map((dir) => rm(dir, { recursive: true, force: true })));
+});
+
+describe("outbound markdown image parsing", () => {
+  it("finds image refs outside fenced code blocks", () => {
+    const text = [
+      "See diagram:",
+      "![plot](https://cdn.example.com/a.png)",
+      "",
+      "```md",
+      "![not-this](https://cdn.example.com/b.png)",
+      "```",
+      "![local](assets/x.png \"title\")",
+    ].join("\n");
+
+    const refs = findMarkdownImagesOutsideCode(text);
+    expect(refs.map((ref) => ref.src)).toEqual([
+      "https://cdn.example.com/a.png",
+      "assets/x.png",
+    ]);
+  });
+
+  it("masks image urls for streaming cards", () => {
+    expect(maskMarkdownImagesForStreaming("before ![alt text](https://x/y.png) after")).toBe(
+      "before alt text after",
+    );
+    expect(maskMarkdownImagesForStreaming("![](https://x/y.png)")).toBe("【图片】");
+  });
+});
+
+describe("materializeAnswerSegments", () => {
+  it("uploads remote and workspace images and builds card segments", async () => {
+    const workspaceRoot = await mkdtemp(join(tmpdir(), "cph-img-root-"));
+    temps.push(workspaceRoot);
+    const workspaceDir = join(workspaceRoot, "project");
+    await mkdir(join(workspaceDir, "assets"), { recursive: true });
+    await writeFile(
+      join(workspaceDir, "assets", "local.png"),
+      Buffer.from([0x89, 0x50, 0x4e, 0x47, 0x0d, 0x0a, 0x1a, 0x0a]),
+    );
+
+    const imageCreate = vi
+      .fn()
+      .mockResolvedValueOnce({ image_key: "img_remote_1" })
+      .mockResolvedValueOnce({ image_key: "img_local_1" });
+    const rt = mockRuntime({ imageCreate });
+
+    const fetchImpl = vi.fn(async () =>
+      new Response(Buffer.from("remote-bytes"), {
+        status: 200,
+        headers: { "content-type": "image/png" },
+      }),
+    );
+
+    const text = "Intro\n\n![remote](https://cdn.example.com/r.png)\n\nAnd local ![local](assets/local.png)\nDone.";
+    const { segments, unresolved } = await materializeAnswerSegments(text, {
+      rt,
+      workspaceRoot,
+      workspaceDir,
+      fetchImpl: fetchImpl as unknown as typeof fetch,
+    });
+
+    expect(unresolved).toEqual([]);
+    expect(imageCreate).toHaveBeenCalledTimes(2);
+    expect(segments).toEqual([
+      { type: "markdown", content: "Intro\n\n" },
+      { type: "image", imgKey: "img_remote_1", alt: "remote" },
+      { type: "markdown", content: "\n\nAnd local " },
+      { type: "image", imgKey: "img_local_1", alt: "local" },
+      { type: "markdown", content: "\nDone." },
+    ]);
+
+    const card = buildAgentCard({
+      phase: "complete",
+      text: "",
+      contentSegments: segments,
+      reasoningText: undefined,
+      toolUseSteps: [],
+      toolUseElapsedMs: undefined,
+      isError: false,
+      interrupted: false,
+      runId: undefined,
+    });
+    expect(card.elements).toEqual(expect.arrayContaining([
+      expect.objectContaining({ tag: "img", img_key: "img_remote_1" }),
+      expect.objectContaining({ tag: "img", img_key: "img_local_1" }),
+      expect.objectContaining({ tag: "markdown", content: "Intro\n\n" }),
+    ]));
+  });
+
+  it("rejects private remote hosts", async () => {
+    const imageCreate = vi.fn();
+    const rt = mockRuntime({ imageCreate });
+    const fetchImpl = vi.fn();
+    const { segments, unresolved } = await materializeAnswerSegments(
+      "![x](http://127.0.0.1/secret.png)",
+      { rt, fetchImpl: fetchImpl as unknown as typeof fetch },
+    );
+    expect(fetchImpl).not.toHaveBeenCalled();
+    expect(imageCreate).not.toHaveBeenCalled();
+    expect(unresolved).toEqual(["http://127.0.0.1/secret.png"]);
+    expect(segments).toEqual([{ type: "markdown", content: "x" }]);
+  });
+});
+
+describe("uploadMessageImage", () => {
+  it("returns image_key from Feishu upload", async () => {
+    const imageCreate = vi.fn(async () => ({ data: { image_key: "img_nested" } }));
+    const rt = mockRuntime({ imageCreate });
+    await expect(uploadMessageImage(rt, Buffer.from("png"))).resolves.toBe("img_nested");
+    expect(imageCreate).toHaveBeenCalledWith({
+      data: { image_type: "message", image: Buffer.from("png") },
+    });
+  });
+});
+
+function mockRuntime(options: {
+  readonly imageCreate?: (payload: unknown) => Promise<unknown>;
+}): FeishuRuntime {
+  return {
+    client: {
+      im: {
+        v1: {
+          image: {
+            create: options.imageCreate ?? vi.fn(),
+          },
+          message: {
+            create: vi.fn(),
+            reply: vi.fn(),
+            patch: vi.fn(),
+          },
+        },
+      },
+    } as unknown as FeishuRuntime["client"],
+    logger: {
+      warn: vi.fn(),
+      error: vi.fn(),
+      info: vi.fn(),
+      debug: vi.fn(),
+      child: vi.fn(),
+      fatal: vi.fn(),
+      trace: vi.fn(),
+      silent: vi.fn(),
+      level: "info",
+    } as unknown as FeishuRuntime["logger"],
+  };
+}

hub/test/unit/session.test.ts

@@ -68,14 +68,14 @@ describe("session cookie signing", () => {
 describe("oauth state signing", () => {
   it("round-trips state with returnTo", () => {
     const token = signOAuthState(
-      { nonce: "abc", returnTo: "/admin/org/acme" },
+      { nonce: "abc", returnTo: "/admin" },
       SECRET,
       600,
       1_700_000_000,
     );
     expect(verifyOAuthState(token, SECRET, 1_700_000_100)).toEqual({
       nonce: "abc",
-      returnTo: "/admin/org/acme",
+      returnTo: "/admin",
       exp: 1_700_000_600,
     });
   });
@@ -83,13 +83,13 @@ describe("oauth state signing", () => {
   it("binds state to an Organization and connection as one inseparable scope", () => {
     const token = signOAuthState({
       nonce: "scoped",
-      returnTo: "/admin/org/acme",
+      returnTo: "/admin",
       organizationId: "org-acme",
       connectionId: "connection-acme",
     }, SECRET, 600, 1_700_000_000);
     expect(verifyOAuthState(token, SECRET, 1_700_000_100)).toEqual({
       nonce: "scoped",
-      returnTo: "/admin/org/acme",
+      returnTo: "/admin",
       organizationId: "org-acme",
       connectionId: "connection-acme",
       exp: 1_700_000_600,
@@ -98,8 +98,11 @@ describe("oauth state signing", () => {
 });
 
 describe("sanitizeReturnTo", () => {
-  it("allows admin paths", () => {
+  it("allows admin paths and rewrites legacy org slug prefixes", () => {
-    expect(sanitizeReturnTo("/admin/org/acme")).toBe("/admin/org/acme");
+    expect(sanitizeReturnTo("/admin")).toBe("/admin");
+    expect(sanitizeReturnTo("/admin/usage")).toBe("/admin/usage");
+    expect(sanitizeReturnTo("/admin/org/acme")).toBe("/admin");
+    expect(sanitizeReturnTo("/admin/org/acme/usage")).toBe("/admin/usage");
   });
 
   it("blocks open redirects", () => {

hub/test/unit/silo-rate-limit.test.ts

@@ -23,6 +23,7 @@ describe("isSiloHttpRateLimitExempt", () => {
     expect(isSiloHttpRateLimitExempt("/favicon.svg")).toBe(true);
     expect(isSiloHttpRateLimitExempt("/robots.txt")).toBe(true);
     expect(isSiloHttpRateLimitExempt("/admin")).toBe(true);
+    expect(isSiloHttpRateLimitExempt("/admin/members")).toBe(true);
     expect(isSiloHttpRateLimitExempt("/admin/org/para-26071100/members")).toBe(true);
   });
 

spec/.gitignore

@@ -1 +0,0 @@
-/.lake

spec/README.md

@@ -1,55 +0,0 @@
-# spec —— Lean 语义母本
-
-这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
-
-## 现状
-
-刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
-
-## 构建
-
-```sh
-cd spec
-lake build
-```
-
-工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
-
-## 写作规范
-
-### 双半契约:prose + type
-
-每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:
-
-- **prose 半**给人读——说清"这在领域里是什么、为什么"。
-- **type 半**给机器读、给 type checker 把关——保证结构无洞。
-
-agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
-
-### 标签分类法
-
-在 doc 注释里用以下标签标注每条语义的状态:
-
-- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
-- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
-- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。
-
-### 分歧点测试(写之前先过一遍)
-
-新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**
-
-- 会 → 它是分歧点,入契约。
-- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
-
-详见根 README 宪法第 5 条。
-
-### 不用 `sorry`
-
-无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
-
-### 命名
-
-- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
-- **类型**:PascalCase。
-- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
-- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。

spec/Spec.lean

@@ -1,5 +0,0 @@
--- This module serves as the root of the `Spec` library.
--- Import modules here that should be built as part of the library.
-import Spec.Prelude
-import Spec.System
-import Spec.Courseware

spec/Spec/Courseware.lean

@@ -1,21 +0,0 @@
-import Spec.Courseware.Model
-import Spec.Courseware.Export
-import Spec.Courseware.Check
-import Spec.Courseware.Open
-
-/-!
-# Courseware —— 产品层契约(课程工程文件)
-
-护城河:课程"工程文件"的语义母本与合法性规则。决策出处 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 骨架(核心关系 OPEN,已 surface):题库 `QuestionBank`、
-  课程编排 `Course`。
--/

spec/Spec/Courseware/Check.lean

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

spec/Spec/Courseware/Check/Diagnostic.lean

@@ -1,107 +0,0 @@
-import Spec.Courseware.Model.Lesson
-import Spec.Courseware.Export.Render
-
-/-!
-# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
-
-产品里"站在 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
-
-/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不
-阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/
-inductive Severity where
-  | warning
-  | error
-
-/-- 诊断**分类**(`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
-  /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/
-  | unknownKind
-  /-- kind schema 要求的某 `content` 字段缺对应 `<field>.typ`。结构/schema 型。 -/
-  | missingContentFile
-  /-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/
-  | schemaViolation
-  /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
-      `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期
-      检出,故归此类,ADR-0012)。外部设施型。 -/
-  | typstCompile
-  /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
-  | renderIgnored
-  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
-      判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
-      定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
-      完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
-      `error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
-  | cphVersionMismatch
-
-/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
-`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
-全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
-def DiagKind.severity : DiagKind → Severity
-  | .partPathMissing    => .error
-  | .unknownKind        => .error
-  | .missingContentFile => .error
-  | .schemaViolation    => .error
-  | .typstCompile       => .error
-  | .renderIgnored      => .warning
-  | .cphVersionMismatch => .error
-
-/-- 缺渲染诊断的级别 = **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(`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
-
-/-!
-## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
-
-`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
-要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
-给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
-来自模型外"显式化、类型化。
--/
-
-/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
-实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
-structure Oracle (l : Lesson P) (c : RenderConfig P) where
-  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
-      其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
-  compiles : P.TargetId → Prop
-  /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/
-  dataConforms : Prop
-  /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/
-  contentFilesPresent : Prop
-
-/-- **合法 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)
-
-end Spec.Courseware

spec/Spec/Courseware/Check/Pipeline.lean

@@ -1,54 +0,0 @@
-import Spec.Courseware.Check.Diagnostic
-
-/-!
-# Pipeline —— checker 检查管线的阶段与序(ADR-0010)
-
-checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
-顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
-显示,这是有意的)。每阶段的**算法**不进 Lean(深度上限:只定**阶段、序、
-门控**)。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
-`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
--/
-
-namespace Spec.Courseware
-
-/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
-
-- `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`);**不**受门控,总跑。 -/
-inductive Phase where
-  | load
-  | structural
-  | schema
-  | compile
-  | coverage
-deriving DecidableEq
-
-/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约:
-`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
-def Phase.order : Phase → Nat
-  | .load       => 0
-  | .structural => 1
-  | .schema     => 2
-  | .compile    => 3
-  | .coverage   => 4
-
-/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在
-结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/
-def Phase.gated : Phase → Bool
-  | .compile => true
-  | _        => false
-
-/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时,
-无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile`
-门控只跳过自己)。 -/
-def Phase.haltsPipelineOnFailure : Phase → Bool
-  | .load => true
-  | _     => false
-
-end Spec.Courseware

spec/Spec/Courseware/Export.lean

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

spec/Spec/Courseware/Export/Artifact.lean

@@ -1,23 +0,0 @@
-/-!
-# Artifact —— export target 的产物(ADR-0009 / 0011)
-
-ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
-固定:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
-是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
-承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
--/
-
-namespace Spec.Courseware
-
-/-- 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** 的文件集(第三方平台 archive
-      即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验
-      完整性。 -/
-  | fileTree (root : String) (outputs : String)
-
-end Spec.Courseware

spec/Spec/Courseware/Export/Render.lean

@@ -1,93 +0,0 @@
-import Spec.Courseware.Model.Primitives
-import Spec.Courseware.Export.Artifact
-
-/-!
-# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 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` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
-- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子,
-  ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 +
-  跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。
-
-**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
-契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
-
-**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":框架 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**(`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-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`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。
-      **已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。
-      slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
-      ADR-0014 R2)。 -/
-  | assembleMarkdown (field : String)
-
-/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
-structure TargetSpec where
-  /-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
-  artifact : Artifact
-  /-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
-  steps : List Step
-  /-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
-      `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
-      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
-  covers : P.KindId → Prop
-
-/-- 渲染配置(`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` 下**被渲染**(`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
-  | none => False
-  | some s => s.covers k
-
-end Spec.Courseware

spec/Spec/Courseware/Model.lean

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

spec/Spec/Courseware/Model/Element.lean

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

spec/Spec/Courseware/Model/Info.lean

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

spec/Spec/Courseware/Model/Lesson.lean

@@ -1,16 +0,0 @@
-import Spec.Courseware.Model.Element
-
-/-!
-# Lesson —— 单节课工程文件
-
-ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
-文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
--/
-
-namespace Spec.Courseware
-
-/-- 一节课(`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,34 +0,0 @@
-/-!
-# Primitives —— Courseware 契约的基元
-
-课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
-schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
-——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
-实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 固定)与其表示进 Lean
-是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
-类型承载。富内容的母本见 `Courseware.RichContent`。
--/
-
-namespace Spec.Courseware
-
-/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
-structure Primitives where
-  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。用抽象
-      类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
-      封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
-  KindId : Type
-  /-- 某 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 标识(`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,44 +0,0 @@
-/-!
-# RichContent —— 富内容(ADR-0006 的母本)
-
-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"这一步。
-
-关键约束(均 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 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
-具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
--/
-
-namespace Spec.Courseware
-
-/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
-定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
-(ADR-0007),不在本层承诺,故 opaque。 -/
-opaque VPath : Type
-
-/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值;
-markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/
-inductive ContentFormat where
-  /-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/
-  | typst
-  /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/
-  | markdown
-
-/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`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

@@ -1,9 +0,0 @@
-import Spec.Courseware.Open.QuestionBank
-import Spec.Courseware.Open.Course
-
-/-!
-# Courseware.Open —— OPEN 骨架(核心关系)
-
-题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
-但未决策的 OPEN 分歧点,待专门 ADR 落定。
--/

spec/Spec/Courseware/Open/Course.lean

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

spec/Spec/Courseware/Open/QuestionBank.lean

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

spec/Spec/Prelude.lean

@@ -1,67 +0,0 @@
-/-!
-# Prelude —— System 层共享标识符
-
-平台层引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。
-其内部表示从未被决策(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque
-载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
-关系,却不对标识符表示作承诺。
--/
-
-namespace Spec.System
-
-/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/
-structure Identifiers where
-  /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
-  ProjectId : Type
-  /-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
-  OrganizationId : Type
-  /-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
-  UserId : Type
-  /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
-  FeishuOpenId : Type
-  /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
-  FeishuUserId : Type
-  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
-  FeishuAppId : Type
-  /-- 飞书 app_secret 信封引用(`OPEN` 表示;ADR-0024)。 -/
-  FeishuAppSecretRef : Type
-  /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
-  TeamId : Type
-  /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/
-  FolderId : Type
-  /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
-  ADR-0017;`@bot` 仅为触发品牌,不承诺 provider)。 -/
-  RunId : Type
-  /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
-  session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
-  记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
-  SessionId : Type
-  /-- Organization-scoped Agent role 标识(`OPEN` 表示, ADR-0017);role 是动态运行配置,
-  不是 slash command 枚举。 -/
-  AgentRoleId : Type
-  /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
-      子类型学未定且非分歧点,故只留 opaque 键)。 -/
-  Principal : Type
-  /-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
-      ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
-      类型——principal 子类型学 OPEN,这里不预设"chat 是 principal 的哪种子型")。 -/
-  ChatId : Type
-  /-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
-  PlatformIdentityId : Type
-  /-- 平台自有飞书应用标识(`OPEN` 表示;ADR-0023,与各 org 客户应用分离)。 -/
-  PlatformFeishuApplicationId : Type
-  /-- 平台应用所验证的外部飞书用户标识(`OPEN` 表示;ADR-0023,其具体 open_id/user_id
-      表示与迁移方式不在本层固定)。 -/
-  PlatformExternalUserId : Type
-  /-- 可撤销 Platform Session 标识(`OPEN` 表示;ADR-0023)。 -/
-  PlatformSessionId : Type
-  /-- Platform Administrator invitation 标识(`OPEN` 表示;ADR-0023)。 -/
-  PlatformInvitationId : Type
-  /-- 一次平台控制面 mutation 标识(`OPEN` 表示;ADR-0023)。 -/
-  PlatformMutationId : Type
-  /-- 独立 Platform Audit Entry 标识(`OPEN` 表示;ADR-0023)。 -/
-  PlatformAuditEntryId : Type
-  /-- 平台离线恢复所声明的 incident 标识(`OPEN` 表示;ADR-0023)。 -/
-  PlatformIncidentId : Type
-
-end Spec.System

spec/Spec/System.lean

@@ -1,57 +0,0 @@
-import Spec.System.Hierarchy
-import Spec.System.ProjectGroup
-import Spec.System.Organization
-import Spec.System.User
-import Spec.System.Connections
-import Spec.System.ProjectWorkspace
-import Spec.System.Capacity
-import Spec.System.PlatformAdministration
-import Spec.System.Agent.Run
-import Spec.System.Agent.AgentRole
-import Spec.System.Agent.Memory
-import Spec.System.Agent.AgentSurface
-import Spec.System.Agent.Usage
-import Spec.System.Agent.Capability
-import Spec.System.Lock
-import Spec.System.Permission
-import Spec.System.PermissionGrant
-import Spec.System.Audit
-/-!
-# System —— Hub 平台层契约
-
-协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
-likec4 已画出结构;这里补语义:
-
-- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
-- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
-- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
-- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
-- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
-  connection secret 信封与 fail-closed resolver(ADR-0024);
-  owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
-- `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
-  (ADR-0021)。
-- `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
-  平台紧急工作负载制动(ADR-0022)。
-- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
-  保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
-- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
-- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
-- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
-- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
-- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
-  Lock 限定并发,Surface 限定波及面。机制 OPEN。
-- `Usage` —— Run 内 append-only 用量计量事实账本(ADR-0026);主模型 completion、
-  外部能力调用、代理网关旁路共用同一账本。fact 不持锁、不跨 run;`costUsd = none`
-  表示未知而非零(ADR-0022)。Run 上的 cost/token 标量是其 rollup cache。
-- `Capability` —— 外部能力(PDF→MD、音视频→文本等)注册与调用(ADR-0027);
-  org-scoped 凭证连接复用 ADR-0024 信封但独立于 model-provider;调用是 Run 内副作用,
-  产物落 workspace,消耗记 UsageFact。capability credential 不进 Agent 进程。
-- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
-- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
-  (ADR-0004);组合规则 OPEN。
-- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
-  `PlatformAdministration` 独立承载。
-
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0027。
--/

spec/Spec/System/Agent/AgentRole.lean

@@ -1,60 +0,0 @@
-import Spec.Prelude
-
-/-!
-# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)
-
-AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
-和 skill 绑定。通过 CLI 管理,不需重启进程生效。
-
-Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
-归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
-仅 label/排序变更不影响会话连续性(ADR-0017)。
-
-Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
-run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
-structure AgentRole where
-  /-- 所属组织(`PINNED`)。 -/
-  organization : I.OrganizationId
-  /-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
-  roleId : String
-  /-- system prompt(`PINNED`)。 -/
-  systemPrompt : String
-  /-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
-  tools : List String
-  /-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
-  defaultModel : String
-
-/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
-structure AgentSkill where
-  /-- 所属组织(`PINNED`)。 -/
-  organization : I.OrganizationId
-  /-- 名称(`PINNED`)。 -/
-  name : String
-  /-- 版本(`PINNED`)。 -/
-  version : String
-  /-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
-  contentDigest : String
-  /-- 描述(`OPEN`)。 -/
-  description : String
-
-/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
-structure AgentRoleSkillBinding where
-  /-- 所属组织(`PINNED`)。 -/
-  organization : I.OrganizationId
-  /-- 绑定的 role(`PINNED`)。 -/
-  roleId : String
-  /-- skill 名称(`PINNED`)。 -/
-  skillName : String
-  /-- skill 版本(`PINNED`)。 -/
-  skillVersion : String
-  /-- 排序(`PINNED`)。 -/
-  sortOrder : Nat
-
-end Spec.System

spec/Spec/System/Agent/AgentSurface.lean

@@ -1,40 +0,0 @@
-import Spec.Prelude
-import Spec.System.Agent.Run
-
-/-!
-# AgentSurface —— Agent 执行面边界(ADR-0018)
-
-Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
-(ADR-0007)。逃逸即越权,拒绝。
-
-与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
-二者都按 run × project 作用域。
-
-shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
-——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers) (Path : Type)
-
-/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
-指向某路径;是否越权由下方 `Authorized` 约束。 -/
-structure AgentFileOp where
-  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
-  run : I.RunId
-  /-- 操作目标路径(`PINNED`, ADR-0018)。 -/
-  path : Path
-
-
-/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
-(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
-(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
-宿主任意文件。 -/
-def AgentFileOp.Authorized
-    (op : AgentFileOp I Path)
-    (runWorkspace : I.RunId → Option Path)
-    (pathWithin : Path → Path → Prop) : Prop :=
-  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
-
-end Spec.System

spec/Spec/System/Agent/Capability.lean

@@ -1,104 +0,0 @@
-import Spec.Prelude
-import Spec.System.Agent.Run
-import Spec.System.Agent.Usage
-
-/-!
-# Capability —— 外部能力注册与调用(ADR-0027)
-
-`AgentRun` 内可能调用**外部能力**:PDF→MD bundle、音视频→文本、OCR 等。这些能力
-不是主 agent loop 的模型 completion,不持项目锁,不占 session 语义(ADR-0026 已拒绝
-nested Run)。它们是 Run 内的副作用:读 workspace 输入、调外部服务、产物落 workspace、
-写一条 `UsageFact`。
-
-本模块 pin 三件事:
-
-1. **ExternalCapability** —— 平台注册的、org 启用的文档/媒体转换服务,由稳定
-   `capabilityId` 标识。
-2. **CapabilityConnection** —— org-scoped 凭证连接,复用 ADR-0024 信封机制但独立于
-   model-provider connection。只有 `active` connection 可被 resolver 使用。
-3. **CapabilityInvocation 良构** —— 调用的输入/输出必须落在 run 的 workspace 内
-   (ADR-0018 `AgentSurface`),且调用产生的消耗必须以 `UsageFact` 记录。
-
-凭证不经 Agent 子进程:Agent 只通过 capability adapter 间接调用,adapter 在 Hub 侧
-解析 org-scoped 凭证并调用外部服务(ADR-0024 resolver boundary)。这与 model-provider
-的 loopback proxy 是不同的机制——capability 调用不走 agent 的网络面,走 Hub 直连。
-
-不变式(`PINNED`, ADR-0027):
-
-- **凭证隔离** —— capability credential 不进 Agent 进程环境;adapter 在 Hub 侧解析。
-- **workspace 边界** —— 输入路径与输出目录都必须落在 run 的 workspace 内(ADR-0018)。
-- **必记 fact** —— 一次成功调用必须产生 ≥1 条 `UsageFact`(`kind = externalCapability`),
-  即使 `costUsd = none`(unknown ≠ 零,ADR-0022/0026)。
-
-`CapabilityInvocation` 作为一等持久记录(status/retries/partial output)在 pilot 不做;
-`UsageFact` 的 `capabilityId + correlationId` 是唯一可追溯痕迹(ADR-0027 Deferred)。
--/
-
-namespace Spec.System.Agent
-
-variable (I : Identifiers) (Path : Type)
-
-/-- 外部能力的输入种类(`PINNED`, ADR-0027)。集合 `OPEN`——新增 kind 须 surface。 -/
-inductive CapabilityInputKind where
-  /-- PDF 文档(`PINNED`)。 -/
-  | pdf
-  /-- 图片(`PINNED`)。 -/
-  | image
-  /-- 音频(`PINNED`)。 -/
-  | audio
-  /-- 视频(`PINNED`)。 -/
-  | video
-
-/-- 外部能力(`PINNED`, ADR-0027)。平台注册的文档/媒体转换服务,由 org 启用。
-
-一个 capability 由稳定 `capabilityId` 标识(如 `pdf_to_md_bundle`),声明接受的输入
-种类与计量单位。org 通过 `CapabilityConnection` 启用它;adapter 是平台侧实现。 -/
-structure ExternalCapability where
-  /-- 稳定能力标识(`PINNED`;如 `pdf_to_md_bundle`、`audio_video_to_text`)。 -/
-  capabilityId : String
-  /-- 接受的输入种类(`PINNED`, ADR-0027)。 -/
-  inputKind : CapabilityInputKind
-  /-- 计量单位(`OPEN`;如 `"pages"`、`"audio_seconds"`)。与 UsageFact.unit 对齐。 -/
-  meteringUnit : String
-
-/-- capability connection 的运行态(`PINNED`, ADR-0024/0027):与 model-provider /
-Feishu connection 同构,只有 `active` 可被 resolver 使用。 -/
-inductive CapabilityConnectionStatus where
-  | draft
-  | active
-  | disabled
-
-/-- Organization 的外部能力凭证连接(`PINNED`, ADR-0027)。复用 ADR-0024 信封机制
-但独立于 model-provider connection:capability 服务(如 MinerU、Whisper)有自己的 auth
-形状与 readiness probe,不走 OpenRouter `/v1/models`。唯一性键为
-`(organization, capabilityId)`。 -/
-structure OrganizationCapabilityConnection where
-  /-- connection 所属 organization(`PINNED`, ADR-0027)。 -/
-  organization : I.OrganizationId
-  /-- 该 connection 启用的 capability(`PINNED`, ADR-0027)。 -/
-  capability : ExternalCapability
-  /-- 运行态(`PINNED`, ADR-0024/0027)。 -/
-  status : CapabilityConnectionStatus
-
-/-- 一次 capability 调用的良构约束(`PINNED`, ADR-0027)。输入路径与输出目录都必须落在
-发起 run 的 workspace 内(ADR-0018 `AgentSurface`);`runWorkspace` 与 `pathWithin`
-由平台提供(表示 `OPEN`)。逃逸即越权,拒绝。 -/
-structure CapabilityInvocation where
-  /-- 发起调用的 run(`PINNED`;调用是 Run 内副作用,不跨 run,ADR-0026/0027)。 -/
-  run : I.RunId
-  /-- 被调用的 capability(`PINNED`)。 -/
-  capability : ExternalCapability
-  /-- 输入路径(workspace 内,`PINNED`, ADR-0018)。 -/
-  inputPath : Path
-  /-- 输出目录(workspace 内,`PINNED`, ADR-0018)。 -/
-  outputDir : Path
-
-/-- capability 调用良构:输入与输出路径都落在 run 的 workspace 内(`PINNED`,
-ADR-0018/0027)。这是 `AgentFileOp.Authorized` 在 capability 调用上的对应物。 -/
-def CapabilityInvocation.Authorized
-    (inv : CapabilityInvocation I Path)
-    (runWorkspace : I.RunId → Option Path)
-    (pathWithin : Path → Path → Prop) : Prop :=
-  ∃ w, runWorkspace inv.run = some w ∧ pathWithin inv.inputPath w ∧ pathWithin inv.outputDir w
-
-end Spec.System.Agent

spec/Spec/System/Agent/Memory.lean

@@ -1,48 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
-
-ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
-飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
-一条安全不变式: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)。"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/Agent/Run.lean

@@ -1,30 +0,0 @@
-/-!
-# Run —— AgentRun 状态机
-
-一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
-转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
-依赖),不定义转移边。
--/
-
-namespace Spec.System
-
-/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
-——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
-见 `RunState.Terminal`。 -/
-inductive RunState where
-  | active
-  | waitingForUser
-  | completed
-  | failed
-  | timedOut
-  | limitExceeded
-  | canceled
-
-/-- run 处于**终止态**(`PINNED`, ADR-0002, ADR-0022:锁在 completes/fails/
-timesOut/limitExceeded/canceled 时释放)。`active`/`waitingForUser` 非终止——后者仍
-占用项目(锁未释放)。 -/
-def RunState.Terminal : RunState → Prop
-  | .completed | .failed | .timedOut | .limitExceeded | .canceled => True
-  | .active | .waitingForUser => False
-
-end Spec.System

spec/Spec/System/Agent/Usage.lean

@@ -1,92 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Usage —— Run 内用量计量事实账本(ADR-0026)
-
-一次 `AgentRun` 内可能产生**多条**可计费消耗:主模型 completion、外部能力调用
-(PDF→MD bundle、音视频转写等)、或代理网关侧旁路调用。这些消耗**不**是子 Run——
-它们不持项目锁、不占 session 语义、不复用 `AgentRun` 状态机。它们是 Run 内的
-append-only **计量事实**(`UsageFact`)。
-
-`AgentRun` 上的 cost/token 标量是 facts 的派生 rollup cache,不是真相来源;真相在
-`UsageFact` 行。这一层抽象让"主模型"与"外部能力"两类消耗共享同一账本,而非给后者
-各开一种特化字段或 nested Run。
-
-核心不变式(`PINNED`, ADR-0022 + ADR-0026):
-
-- **append-only** —— fact 一旦写入只读不更不删;`costUsd` 修正走新 fact,不改旧行。
-- **`costUsd = none` 表示"未知",不是"零成本"** —— ADR-0022:missing provider cost
-  remains unknown rather than zero。聚合时不得把 none 当 0 求和。
-- **fact 不持锁、不跨 run** —— 它是 Run 内的副作用账本,不是又一次 `@bot` 生命周期。
-  外部能力调用亦同:它的语义边界是 `capabilityId` + `correlationId`,不是 `RunId`。
-- **价目回算是派生** —— `costSource = pricebookDerived` 时,`costUsd` 由
-  `occurredAt × (provider, model)` 查价目表派生;provider 实报(`providerReported`)
-  优先于派生。无价目可查时 `costSource = unknown`,`costUsd = none`。
-
-外部能力(capability)注册表、价目表(pricebook)、商业结算均 `OPEN`,pilot 不做
-(ADR-0021 仍 defer commercial billing)。本模块只 pin **账本结构与不变式**。
--/
-
-namespace Spec.System.Agent
-
-variable (I : Identifiers) (Time Cost Quantity : Type)
-
-/-- 计量事实类型(`PINNED`, ADR-0026)。集合完整性 `OPEN`——新增 kind 须 surface,
-不得静默把外部消耗塞进既有 kind。 -/
-inductive UsageFactKind where
-  /-- 主 agent loop 的模型 completion(`PINNED`)。 -/
-  | modelCompletion
-  /-- 外部能力调用(`PINNED`;如 pdf_to_md_bundle、audio_video_to_text)。 -/
-  | externalCapability
-  /-- 代理网关侧旁路调用(`PINNED`;非主 loop 的模型调用,如嵌入工具内的子请求)。 -/
-  | toolProxy
-
-/-- 成本来源(`PINNED`, ADR-0026)。优先级:provider 实报 > 价目派生 > unknown。 -/
-inductive CostSource where
-  /-- provider/gateway 实报(`PINNED`)。 -/
-  | providerReported
-  /-- 用 `occurredAt × (provider, model)` 价目表派生(`PINNED`)。 -/
-  | pricebookDerived
-  /-- 缺失,而非零(`PINNED`;ADR-0022 missing cost ≠ zero)。 -/
-  | unknown
-
-/-- 一次可计费消耗的计量事实(`PINNED`, ADR-0026)。append-only;一次 run ≥0 条。
-
-字段分两组:**归属与时间**(run/occurredAt/kind)用于聚合与价目回算;
-**计量与成本**(tokens/quantity/unit/costUsd/costSource)用于账目本身。
-非 token 计量(页/秒/次)走 `quantity + unit`,与 token 并存而非取代。 -/
-structure UsageFact where
-  /-- 所属 run(`PINNED`;fact 不跨 run,fact 不持锁,ADR-0026)。 -/
-  run : I.RunId
-  /-- 消耗发生时刻(`PINNED`);价目回算依赖此字段而非 run.finishedAt,
-  因为外部能力可能早于 run 结束。 -/
-  occurredAt : Time
-  /-- 事实类型(`PINNED`, ADR-0026)。 -/
-  kind : UsageFactKind
-  /-- provider 标识(`PINNED`;如 openrouter、mineru、openai_whisper)。 -/
-  provider : String
-  /-- 模型标识(`OPEN`;非模型计费可为 none)。 -/
-  model : Option String
-  /-- 输入 tokens(`OPEN`;非 token 计量可为 none)。 -/
-  inputTokens : Option Nat
-  /-- 输出 tokens(`OPEN`)。 -/
-  outputTokens : Option Nat
-  /-- 非 token 计量数值(`OPEN`;如页数、音频秒数)。与 tokens 并存。 -/
-  quantity : Option Quantity
-  /-- 计量单位(`OPEN`;如 "pages"、"audio_seconds"、"invocations")。 -/
-  unit : Option String
-  /-- 成本(`PINNED`;none = 未知,非零,ADR-0022)。 -/
-  costUsd : Option Cost
-  /-- 成本来源(`PINNED`;costUsd ≠ none 时必填,costUsd = none 时为 `unknown`)。 -/
-  costSource : CostSource
-  /-- 外部能力标识(`OPEN`;kind = externalCapability 时填,如 pdf_to_md_bundle)。 -/
-  capabilityId : Option String
-  /-- 外部请求关联 id(`OPEN`;对账/幂等用,不参与聚合)。 -/
-  correlationId : Option String
-
-/-- Fact 的成本是否**已知**(`PINNED`, ADR-0026)。聚合 rollup 时,只对已知成本求和;
-未知成本的 fact 不贡献 0,而是让汇总保持未知(若所有 fact 均未知)或部分未知。 -/
-def UsageFact.HasKnownCost (fact : UsageFact I Time Cost Quantity) : Prop :=
-  fact.costUsd ≠ none
-
-end Spec.System.Agent

spec/Spec/System/Audit.lean

@@ -1,20 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Audit —— Project/Run 审计日志
-
-审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
-且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
-关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
-`Spec.System.PlatformAdministration`,不复用本结构。
--/
-
-namespace Spec.System
-
-/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
-关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
-structure AuditEntry (I : Identifiers) where
-  /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
-  run : I.RunId
-
-end Spec.System

spec/Spec/System/Capacity.lean

@@ -1,89 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Capacity —— SaaS capacity admission and abuse controls (ADR-0022)
-
-初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
-其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
-生产式容量测试校准,保持 `OPEN`。
--/
-
-namespace Spec.System
-
-/-- 首个生产版本必须有硬边界的容量维度(`PINNED`, ADR-0022)。金额与 token 用量是
-统计和软告警,不在本硬限制集合中;各维度的具体数值为 `OPEN`,须由容量测试决定。 -/
-inductive CapacityDimension where
-  | requestRate
-  | requestBodySize
-  | agentConcurrency
-  | admissionQueueLength
-  | admissionQueueWait
-  | fileSize
-  | attachmentCount
-  | archiveExpansion
-  | projectStorage
-  | organizationStorage
-  | memberCount
-  | projectCount
-  | teamCount
-  | folderCount
-  | sessionCount
-  | runWallTime
-  | runTurns
-  | runToolCalls
-  | toolWallTime
-  | runOutputSize
-  | processMemory
-  | processCpu
-  | processCount
-
-/-- 一个容量维度的分层限制(`PINNED`, ADR-0022):platform ceiling 永远存在且不可被
-Organization 突破;Organization policy 可以缺省,也只能配置更低的限制。 -/
-structure LayeredLimit where
-  /-- 由版本化生产部署配置提供的不可突破上限(`PINNED`, ADR-0022)。 -/
-  platformCeiling : Nat
-  /-- Organization 管理员可选的更低策略限制(`PINNED`, ADR-0022)。 -/
-  organizationLimit : Option Nat
-
-/-- 分层限制是良构的 iff Organization policy 未设置或不高于 platform ceiling
-(`PINNED`, ADR-0022)。不允许用 `none` 表示 platform unlimited。 -/
-def LayeredLimit.Valid (limit : LayeredLimit) : Prop :=
-  match limit.organizationLimit with
-  | none => True
-  | some organizationLimit => organizationLimit ≤ limit.platformCeiling
-
-/-- 有效限制(`PINNED`, ADR-0022)取 platform ceiling 与 Organization policy 中较低者;
-Organization policy 缺省时直接采用 platform ceiling,永不退化为 unlimited。 -/
-def LayeredLimit.effective (limit : LayeredLimit) : Nat :=
-  match limit.organizationLimit with
-  | none => limit.platformCeiling
-  | some organizationLimit => min limit.platformCeiling organizationLimit
-
-/-- 已被服务接受的 agent run request 状态(`PINNED`, ADR-0022)。`expired` 和
-`canceled` 都是可审计终态且不得自动执行;`started` 表示已从 admission queue 移交给
-一个 AgentRun。被容量规则拒绝的输入从未被接受,因此不伪装成 queued request。 -/
-inductive RunRequestState where
-  | queued
-  | started
-  | expired
-  | canceled
-
-/-- 平台紧急工作负载制动模式(`PINNED`, ADR-0022)。`drain` 停止新 admission 与队列
-启动但允许当前 run 完成;`stopNow` 还会取消当前 run。它们不等同于删除或封禁 org。 -/
-inductive WorkloadBrakeMode where
-  | open
-  | drain
-  | stopNow
-
-/-- 紧急制动是否允许接收新的 agent 工作(`PINNED`, ADR-0022):只有 `open` 允许。 -/
-def WorkloadBrakeMode.AcceptsNew : WorkloadBrakeMode → Prop
-  | .open => True
-  | .drain | .stopNow => False
-
-/-- 紧急制动是否允许当前 agent run 继续(`PINNED`, ADR-0022):`drain` 允许收尾,
-`stopNow` 要求取消。 -/
-def WorkloadBrakeMode.AllowsActive : WorkloadBrakeMode → Prop
-  | .open | .drain => True
-  | .stopNow => False
-
-end Spec.System

spec/Spec/System/Connections.lean

@@ -1,24 +0,0 @@
-import Spec.System.Connections.Prelude
-import Spec.System.Connections.Feishu
-
-/-!
-# Connections —— 连接绑定与用户信息
-
-组织/用户的外部连接。提供商枚举见 `Connections.Prelude`;
-飞书具体类型见 `Connections.Feishu`。
--/
-
-namespace Spec.System
-
-
-/-- 组织连接绑定(`PINNED`)。 -/
-inductive ConnectionBinding (I : Identifiers) where
-  /-- 飞书(`PINNED`)。 -/
-  | feishu : FeishuAppBinding I → ConnectionBinding I
-
-/-- 用户连接信息(`PINNED`)。 -/
-inductive ConnectionProfile (I : Identifiers) where
-  /-- 飞书(`PINNED`)。 -/
-  | feishu : FeishuProfile I → ConnectionProfile I
-
-end Spec.System

spec/Spec/System/Connections/Feishu.lean

@@ -1,31 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Feishu —— 飞书连接
-
-组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
-structure FeishuAppBinding where
-  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
-  appId : I.FeishuAppId
-  /-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
-  appSecretEnvelope : I.FeishuAppSecretRef
-
-/-- 用户的飞书信息(`PINNED`)。 -/
-structure FeishuProfile where
-  /-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
-  openId : I.FeishuOpenId
-  /-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
-  userId : I.FeishuUserId
-  /-- 显示名(`OPEN`)。 -/
-  name : Option String
-  /-- 头像 URL(`OPEN`)。 -/
-  avatarUrl : Option String
-
-end Spec.System

spec/Spec/System/Connections/Prelude.lean

@@ -1,15 +0,0 @@
-/-!
-# Connections.Prelude —— 连接提供商
-
-用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
-模型 provider connection 是独立概念,见 `Spec.System.Organization`。
--/
-
-namespace Spec.System
-
-/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
-inductive ConnectionProvider where
-  /-- 飞书(`PINNED`)。 -/
-  | feishu
-
-end Spec.System

spec/Spec/System/Hierarchy.lean

@@ -1,46 +0,0 @@
-import Spec.Prelude
-import Spec.System.Connections
-
-/-!
-# Hierarchy —— 主体层级
-
-整个服务中的主体: 平台 → 组织(租户)→ 用户。
-
-- **平台**(Platform): SaaS 提供方实体
-
-- **组织**(Organization): SaaS 租户
-
-- **用户**(User): 租户内的独立实体
-
-**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/
-structure Platform where
-  /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
-  application : I.PlatformFeishuApplicationId
-/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
-外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
-structure Organization where
-  /-- 组织标识(`OPEN` 表示)。 -/
-  id : I.OrganizationId
-  /-- 外部连接(`PINNED`)。 -/
-  connections : List (ConnectionBinding I)
-
-/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/
-structure User where
-  /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
-  id : I.UserId
-  /-- 所属组织(`PINNED`, ADR-0020)。 -/
-  organization : I.OrganizationId
-  /-- 显示名(`PINNED`, 可改)。 -/
-  displayName : String
-  /-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
-  passwordHash : String
-  /-- 外部连接(`PINNED`)。 -/
-  connections : List (ConnectionProfile I)
-
-end Spec.System

spec/Spec/System/Lock.lean

@@ -1,34 +0,0 @@
-import Spec.Prelude
-import Spec.System.Agent.Run
-
-/-!
-# Lock —— 项目锁与排他不变式
-
-ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
-teacher / chat / session)。持锁者必为非终止 run。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
-锁不可能被 session / teacher 持有。 -/
-structure ProjectAgentLock where
-  /-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
-  scope : I.ProjectId
-  /-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
-  owner : I.RunId
-
-/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
-的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
-def LockTable := I.ProjectId → Option I.RunId
-
-/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。
-
-若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
-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/Organization.lean

@@ -1,129 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Organization —— SaaS 租户 (ADR-0020, ADR-0024)
-
-组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
-组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
-`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
-`Spec.System.Agent.AgentRole`。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- 课程项目的租户归属(`PINNED`, ADR-0020):每个 project 必须有一个 organization。 -/
-structure ProjectTenancy where
-  /-- 被归属的课程项目(`PINNED`, ADR-0020)。 -/
-  project : I.ProjectId
-  /-- project 所属 organization(`PINNED`, ADR-0020)。 -/
-  organization : I.OrganizationId
-
-/-- Hub team 的租户归属(`PINNED`, ADR-0020):team 是 org-scoped principal。 -/
-structure TeamTenancy where
-  /-- 被归属的 Hub team(`PINNED`, ADR-0020)。 -/
-  team : I.TeamId
-  /-- team 所属 organization(`PINNED`, ADR-0020)。 -/
-  organization : I.OrganizationId
-
-/-- Team 对 project 的授权作用域(`PINNED`, ADR-0020):`PermissionGrant` 可以把
-TEAM principal 授给 PROJECT resource,但该 grant 必须同 org。role 本身仍由
-`PermissionGrant`/`Permission` 定义,这里仅刻画 tenant well-scopedness。 -/
-structure TeamProjectGrantScope where
-  /-- 被授权的 project(`PINNED`, ADR-0020)。 -/
-  project : I.ProjectId
-  /-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
-  team : I.TeamId
-/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
-(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
-team grant 必须被拒绝。 -/
-def TeamProjectGrantScope.WellScoped
-    (grant : TeamProjectGrantScope I)
-    (projectOrg : I.ProjectId → Option I.OrganizationId)
-    (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
-  ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
-
-/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
-跨 org 共用 process-global key。模式切换 `OPEN`。 -/
-inductive ProviderCredentialMode where
-  | byok
-  | platformManaged
-
-/-- Organization 的 model provider connection(`PINNED`, ADR-0021, ADR-0024):connection
-必须归属一个且仅一个 organization,并明确采用哪一种凭据模式。凭据存为由本地版本化
-master-key keyring 包裹的不可变信封版本;业务代码只能通过显式 organization/project
-作用域的 fail-closed resolver 获得短生命周期明文,不得回退到 process-global key;Agent
-执行环境只获得 run-scoped 本地 proxy capability,不得获得 org provider 明文。 -/
-structure OrganizationProviderConnection where
-  /-- connection 所属 organization(`PINNED`, ADR-0021)。 -/
-  organization : I.OrganizationId
-  /-- connection 的凭据归属模式(`PINNED`, ADR-0021)。 -/
-  mode : ProviderCredentialMode
-
-/-- Organization connection 的运行态(`PINNED`, ADR-0024):只有 `active` connection
-可被 resolver 使用;`draft` 与 `disabled` 都必须 fail closed。 -/
-inductive OrganizationConnectionStatus where
-  | draft
-  | active
-  | disabled
-
-/-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
-同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
-跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
-structure OrganizationSecretBinding
-    (OrganizationId ConnectionId SecretVersionId Purpose : Type) where
-  /-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
-  organization : OrganizationId
-  /-- secret 所属稳定 connection(`PINNED`, ADR-0024)。 -/
-  connection : ConnectionId
-  /-- 不可变 secret version(`PINNED`, ADR-0024)。 -/
-  secretVersion : SecretVersionId
-  /-- payload 的连接类型/用途(`PINNED`, ADR-0024)。 -/
-  purpose : Purpose
-
-/-- 生产 secret resolver 的使用条件(`PINNED`, ADR-0024):connection 与 active secret
-必须属于请求解析出的同一 active organization,connection 必须 active,且信封必须能用其
-记录的本地 KEK 完整认证并解密。缺失/错误 key、损坏密文和任何 scope 不一致都返回失败;
-不得尝试全局环境变量凭据;Agent child 也不得接收该明文。`authenticatedEnvelope` 是
-密码学实现提供的判定。 -/
-def OrganizationSecretResolvable
-    {OrganizationId ConnectionId SecretVersionId Purpose : Type}
-    [BEq OrganizationId]
-    (requestedOrganization : OrganizationId)
-    (binding : OrganizationSecretBinding OrganizationId ConnectionId SecretVersionId Purpose)
-    (organizationActive connectionActive authenticatedEnvelope : Bool) : Bool :=
-  organizationActive && connectionActive &&
-    (binding.organization == requestedOrganization) && authenticatedEnvelope
-
-
-/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
-inductive OrganizationRole where
-  /-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
-  | owner
-  /-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
-  | admin
-  /-- 组织成员(`PINNED`):普通成员。 -/
-  | member
-
-/-- 组织成员关系(`PINNED`)。 -/
-structure OrganizationMembership where
-  /-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
-  user : I.UserId
-  /-- 组织(`PINNED`)。 -/
-  organization : I.OrganizationId
-  /-- 角色(`PINNED`)。 -/
-  role : OrganizationRole
-
-/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
-def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
-  actorRole = .owner
-
-/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
-def LastOwnerProtected
-    (target : OrganizationMembership I)
-    (otherOwnersInOrg : List I.UserId) : Prop :=
-  target.role ≠ .owner ∨
-    ∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
-
-end Spec.System

spec/Spec/System/Permission.lean

@@ -1,66 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Permission —— 角色、能力与授权
-
-ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
-分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
-强制释放锁是 **admin-only**,在 role 体系之外。
--/
-
-namespace Spec.System
-
-/-- 协作者角色(`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` 由 ADR-0023 的 `Spec.System.PlatformAdministration` 独立判定,
-本层不把平台权力折进 project role。 -/
-def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
-
-end Spec.System

spec/Spec/System/PermissionGrant.lean

@@ -1,67 +0,0 @@
-import Spec.Prelude
-import Spec.System.Permission
-
-/-!
-# PermissionGrant —— 授权与设置(ADR-0004)
-
-ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
-(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
-开某类操作"。
-
-principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
-与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
-但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
-organization,见 `Spec.System.Organization`。
--/
-
-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/PlatformAdministration.lean

@@ -1,221 +0,0 @@
-import Spec.Prelude
-
-/-!
-# PlatformAdministration —— 平台管理员身份、会话与审计边界(ADR-0023)
-
-平台控制面可以创建 org、写入连接凭据并制动全平台工作负载,因此不得借用客户
-`User`、`OrganizationMembership` 或 project role。ADR-0023 决定独立平台飞书 issuer、
-单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
-同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。
-
-这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
-字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- 平台管理员的已验证外部身份(`PINNED`, ADR-0023):issuer 必须是专用
-Platform-owned Feishu Application;该身份与客户 `User`/org membership/project grant
-是不同的授权根,即使现实中是同一个人也不自动传播权限。 -/
-structure PlatformIdentity where
-  /-- 平台身份自身标识(`OPEN` 表示,ADR-0023)。 -/
-  id : I.PlatformIdentityId
-  /-- 验证该身份的平台自有飞书应用(`PINNED`, ADR-0023)。 -/
-  application : I.PlatformFeishuApplicationId
-  /-- 在该平台应用作用域内验证的外部飞书用户(`PINNED` 作用域,表示 `OPEN`)。 -/
-  externalUser : I.PlatformExternalUserId
-
-/-- 平台身份来自当前唯一受信 platform-owned app iff identity 的 issuer 与配置的
-平台应用相同(`PINNED`, ADR-0023);不能把客户 org app 的 identity 当平台身份。 -/
-def PlatformIdentity.FromPlatformApplication
-    (identity : PlatformIdentity I)
-    (platformApplication : I.PlatformFeishuApplicationId) : Prop :=
-  identity.application = platformApplication
-
-/-- 初始平台控制面的 standing role(`PINNED` 封闭, ADR-0023):只有一个平级
-administrator;不存在 Platform Owner/Super Admin/Teacher 层级。 -/
-inductive PlatformRole where
-  | administrator
-
-/-- Standing Platform Administrator grant 的生命周期(`PINNED`, ADR-0023)。 -/
-inductive StandingPlatformAdminGrantState where
-  | active
-  | revoked
-
-/-- 一个普通、长期存在的 Platform Administrator grant(`PINNED`, ADR-0023)。 -/
-structure StandingPlatformAdminGrant where
-  /-- 被授予平台管理员权力的独立平台身份(`PINNED`, ADR-0023)。 -/
-  identity : I.PlatformIdentityId
-  /-- standing role;当前封闭集合只有 administrator(`PINNED`, ADR-0023)。 -/
-  role : PlatformRole
-  /-- grant 当前是否仍有效(`PINNED`, ADR-0023)。 -/
-  state : StandingPlatformAdminGrantState
-
-/-- Standing grant 仅在 active 状态有效(`PINNED`, ADR-0023)。 -/
-def StandingPlatformAdminGrant.Active
-    (grant : StandingPlatformAdminGrant I) : Prop :=
-  grant.state = .active
-
-/-- 首位平台管理员 bootstrap 的前置条件(`PINNED`, ADR-0023):只有 standing admin
-集合为空时才允许;bootstrap 身份验证、审计与事务机制见 ADR,具体脚本表示 `OPEN`。 -/
-def CanBootstrapPlatformAdmin
-    (activeStandingAdmins : List I.PlatformIdentityId) : Prop :=
-  activeStandingAdmins = []
-
-/-- 撤销 standing Platform Administrator 的最后管理员保护(`PINNED`, ADR-0023):
-target 必须当前有效,且列表中必须另有一个不同的有效管理员。Emergency grant 不计入
-standing admin 集合,不能用来绕过最后管理员保护。 -/
-def CanRevokePlatformAdmin
-    (activeStandingAdmins : List I.PlatformIdentityId)
-    (target : I.PlatformIdentityId) : Prop :=
-  target ∈ activeStandingAdmins ∧
-    ∃ other, other ∈ activeStandingAdmins ∧ other ≠ target
-
-/-- Platform Administrator invitation 的生命周期(`PINNED`, ADR-0023):accepted/
-expired/revoked 都是终态,所以邀请只能成功领取一次。 -/
-inductive PlatformAdminInvitationState where
-  | pending
-  | accepted
-  | expired
-  | revoked
-
-/-- 一个短期、单次且绑定具体平台飞书账号的管理员邀请(`PINNED`, ADR-0023)。 -/
-structure PlatformAdminInvitation where
-  /-- invitation 标识(`OPEN` 表示,ADR-0023)。 -/
-  id : I.PlatformInvitationId
-  /-- 预期账号必须来自这个平台自有飞书应用(`PINNED`, ADR-0023)。 -/
-  application : I.PlatformFeishuApplicationId
-  /-- 只有这个预期飞书账号可领取;链接本身不是 bearer admin 权力(`PINNED`)。 -/
-  expectedExternalUser : I.PlatformExternalUserId
-  /-- 邀请过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/
-  expiresAt : Nat
-  /-- 邀请当前状态(`PINNED`, ADR-0023)。 -/
-  state : PlatformAdminInvitationState
-
-/-- 邀请可领取 iff 尚 pending、未过期且已验证 identity 与邀请绑定的 app+用户一致
-(`PINNED`, ADR-0023)。 -/
-def PlatformAdminInvitation.CanAccept
-    (invitation : PlatformAdminInvitation I)
-    (identity : PlatformIdentity I)
-    (now : Nat) : Prop :=
-  invitation.state = .pending ∧
-    now < invitation.expiresAt ∧
-    identity.application = invitation.application ∧
-    identity.externalUser = invitation.expectedExternalUser
-
-/-- 邀请状态转换(`PINNED`, ADR-0023):pending 只能结束为 accepted/expired/revoked;
-任何终态都不能回到 pending 或再次 accepted。 -/
-def PlatformAdminInvitation.ValidTransition :
-    PlatformAdminInvitationState → PlatformAdminInvitationState → Prop
-  | .pending, .accepted | .pending, .expired | .pending, .revoked => True
-  | _, _ => False
-
-/-- 服务端 Platform Session 的生命周期(`PINNED`, ADR-0023)。 -/
-inductive PlatformSessionState where
-  | active
-  | revoked
-  | expired
-
-/-- 独立平台会话(`PINNED`, ADR-0023):只绑定 Platform Identity,不携带 org/project
-权力;opaque cookie/token、hash 与 TTL 表示为 `OPEN`。 -/
-structure PlatformSession where
-  /-- 平台会话标识(`OPEN` 表示,ADR-0023)。 -/
-  id : I.PlatformSessionId
-  /-- 会话认证的独立平台身份(`PINNED`, ADR-0023)。 -/
-  identity : I.PlatformIdentityId
-  /-- 服务端可立即撤销/过期的状态(`PINNED`, ADR-0023)。 -/
-  state : PlatformSessionState
-
-/-- 双因子离线恢复授权(`PINNED`, ADR-0023):受控主机权限、主机外 recovery key 与
-已声明 incident 三项都存在才是受支持的 recovery;具体因子实现与保管介质 `OPEN`。 -/
-structure PlatformRecoveryAuthorization where
-  /-- 已验证受控生产主机权限(`PINNED`, ADR-0023)。 -/
-  hostControl : Bool
-  /-- 已验证独立的主机外 recovery key(`PINNED`, ADR-0023)。 -/
-  offlineRecoveryKey : Bool
-  /-- 操作绑定了 incident id 与原因(`PINNED`, ADR-0023)。 -/
-  incidentDeclared : Bool
-
-/-- Recovery authorization 只有三项因子均为真时有效(`PINNED`, ADR-0023)。 -/
-def PlatformRecoveryAuthorization.Valid
-    (authorization : PlatformRecoveryAuthorization) : Prop :=
-  authorization.hostControl = true ∧
-    authorization.offlineRecoveryKey = true ∧
-    authorization.incidentDeclared = true
-
-/-- 只有有效双因子 recovery authorization 才能签发 Emergency Platform Grant
-(`PINNED`, ADR-0023);不存在普通 web session 直接创建 break-glass 权力的路径。 -/
-def CanIssueEmergencyPlatformGrant
-    (authorization : PlatformRecoveryAuthorization) : Prop :=
-  authorization.Valid
-
-/-- 无常驻 break-glass 账号的短期紧急授权(`PINNED`, ADR-0023)。它不属于 standing
-role,必须绑定已声明 incident,自动过期且可在恢复完成时提前关闭。 -/
-structure EmergencyPlatformGrant where
-  /-- 获得临时平台权力的已验证 Platform Identity(`PINNED`, ADR-0023)。 -/
-  identity : I.PlatformIdentityId
-  /-- 触发该授权的 incident(`PINNED`, ADR-0023)。 -/
-  incident : I.PlatformIncidentId
-  /-- 自动过期的逻辑时刻(`PINNED` 有限寿命,数值单位/上限 `OPEN`)。 -/
-  expiresAt : Nat
-  /-- 恢复完成后是否已显式关闭(`PINNED`, ADR-0023)。 -/
-  closed : Bool
-
-/-- Emergency grant 仅在未关闭且未到期时有效(`PINNED`, ADR-0023)。 -/
-def EmergencyPlatformGrant.Active
-    (grant : EmergencyPlatformGrant I) (now : Nat) : Prop :=
-  grant.closed = false ∧ now < grant.expiresAt
-
-/-- 每次平台请求的授权条件(`PINNED`, ADR-0023):session 必须仍为 active,且请求时
-重新解析到 active standing grant 或同 identity 的未关闭、未过期 emergency grant。
-cookie 内曾经出现过 role claim 不能代替这次解析。 -/
-def PlatformSession.Authorized
-    (session : PlatformSession I)
-    (standingGrants : List (StandingPlatformAdminGrant I))
-    (emergencyGrants : List (EmergencyPlatformGrant I))
-    (now : Nat) : Prop :=
-  session.state = .active ∧
-    ((∃ grant, grant ∈ standingGrants ∧
-        grant.identity = session.identity ∧
-        StandingPlatformAdminGrant.Active I grant) ∨
-      ∃ grant, grant ∈ emergencyGrants ∧
-        grant.identity = session.identity ∧
-        EmergencyPlatformGrant.Active I grant now)
-
-/-- 必须做近期 OAuth step-up 的平台敏感操作集合(`PINNED`, ADR-0023;未来新增敏感
-操作时可扩):管理员生命周期、飞书连接、platform-managed provider 凭据、org 生命周期、
-workload brake 与 emergency grant 都不能只凭旧 session。 -/
-inductive PlatformSensitiveAction where
-  | administratorLifecycle
-  | feishuConnection
-  | platformManagedProviderCredential
-  | organizationLifecycle
-  | workloadBrake
-  | emergencyGrant
-
-/-- 敏感操作授权必须提供"近期重新认证"事实(`PINNED`, ADR-0023);具体时间窗 `OPEN`,
-由 browser/session 决策给出受检上限。 -/
-def PlatformSensitiveAction.Authorized
-    (_action : PlatformSensitiveAction)
-    (recentAuthentication : Prop) : Prop :=
-  recentAuthentication
-
-/-- 一个成功平台 mutation 与其独立 Platform Audit Entry 的原子提交事实(`PINNED`,
-ADR-0023):没有 audit entry 就不存在合法成功 commit;具体数据库事务机制 `OPEN`。 -/
-structure PlatformMutationCommit where
-  /-- 成功的平台 mutation(`PINNED`, ADR-0023)。 -/
-  mutation : I.PlatformMutationId
-  /-- 与 mutation 同成同败的 append-only 平台审计条目(`PINNED`, ADR-0023)。 -/
-  auditEntry : I.PlatformAuditEntryId
-
-/-- Organization 管理员可读的平台审计脱敏投影(`PINNED`, ADR-0023):只关联影响该
-Organization 的 entry;完整平台审计和其他 org entry 不经此投影暴露。 -/
-structure OrganizationPlatformAuditProjection where
-  /-- 被投影的平台审计条目(`PINNED`, ADR-0023)。 -/
-  auditEntry : I.PlatformAuditEntryId
-  /-- 唯一可见该投影的受影响 Organization(`PINNED`, ADR-0023)。 -/
-  organization : I.OrganizationId
-
-end Spec.System