From 3f9b60f692e1d4e2e9ae4d38bc6af022a7e8d457 Mon Sep 17 00:00:00 2001 From: Hong Jiarong Date: Mon, 20 Jul 2026 09:07:26 +0000 Subject: [PATCH] chore: remove Lean spec; ADRs are the single source of truth MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The spec/ Lean semantic master had no conformance gate, no codegen, and no CI tie to implementations — alignment was carried entirely by human review, the same mechanism that carries the ADRs. In practice the ADRs plus greppable code comments were already the load-bearing artifacts, so spec/ was the most expensive kind of stale documentation. - delete spec/ and the spec-check CI workflow - README: constitution rewritten around ADRs as decision truth - AGENTS.md/CLAUDE.md: discipline re-anchored (new decisions -> new ADR, never rewrite ADR history; supersede instead) - code comments: re-anchor 'Mirrors Spec.X' invariants to ADR numbers (cph-diag, cph-check, cph-model, hub runner/capacity/org, prisma) - leave ADR bodies and .scratch audit snapshots untouched (history); fix live references in open readiness tickets --- .gitea/workflows/checker-check.yml | 10 +- .gitea/workflows/hub-check.yml | 4 +- .gitea/workflows/spec-check.yml | 20 -- .gitignore | 4 - .../05-define-abuse-capacity-controls.md | 2 +- .../08-prove-production-release-gate.md | 2 +- .../27-reconcile-audit-history-contract.md | 2 +- ...42-decide-platform-admin-identity-audit.md | 4 +- AGENTS.md | 28 +-- CLAUDE.md | 18 +- README.md | 39 ++-- crates/README.md | 5 +- crates/cph-check/src/lib.rs | 20 +- crates/cph-diag/src/lib.rs | 25 +- crates/cph-model/src/lib.rs | 63 ++--- hub/package.json | 2 +- .../migration.sql | 2 +- hub/prisma/schema.prisma | 8 +- hub/src/agent/runner.ts | 6 +- hub/src/capacity/dimensions.ts | 4 +- hub/src/org/capacityPolicy.ts | 6 +- hub/src/org/members.ts | 2 +- spec/.gitignore | 1 - spec/README.md | 55 ----- spec/Spec.lean | 5 - spec/Spec/Courseware.lean | 21 -- spec/Spec/Courseware/Check.lean | 9 - spec/Spec/Courseware/Check/Diagnostic.lean | 107 --------- spec/Spec/Courseware/Check/Pipeline.lean | 54 ----- spec/Spec/Courseware/Export.lean | 8 - spec/Spec/Courseware/Export/Artifact.lean | 23 -- spec/Spec/Courseware/Export/Render.lean | 93 -------- spec/Spec/Courseware/Model.lean | 13 -- spec/Spec/Courseware/Model/Element.lean | 24 -- spec/Spec/Courseware/Model/Info.lean | 58 ----- spec/Spec/Courseware/Model/Lesson.lean | 16 -- spec/Spec/Courseware/Model/Primitives.lean | 34 --- spec/Spec/Courseware/Model/RichContent.lean | 44 ---- spec/Spec/Courseware/Open.lean | 9 - spec/Spec/Courseware/Open/Course.lean | 10 - spec/Spec/Courseware/Open/QuestionBank.lean | 10 - spec/Spec/Prelude.lean | 67 ------ spec/Spec/System.lean | 57 ----- spec/Spec/System/Agent/AgentRole.lean | 60 ----- spec/Spec/System/Agent/AgentSurface.lean | 40 ---- spec/Spec/System/Agent/Capability.lean | 104 --------- spec/Spec/System/Agent/Memory.lean | 48 ---- spec/Spec/System/Agent/Run.lean | 30 --- spec/Spec/System/Agent/Usage.lean | 92 -------- spec/Spec/System/Audit.lean | 20 -- spec/Spec/System/Capacity.lean | 89 ------- spec/Spec/System/Connections.lean | 24 -- spec/Spec/System/Connections/Feishu.lean | 31 --- spec/Spec/System/Connections/Prelude.lean | 15 -- spec/Spec/System/Hierarchy.lean | 46 ---- spec/Spec/System/Lock.lean | 34 --- spec/Spec/System/Organization.lean | 129 ---------- spec/Spec/System/Permission.lean | 66 ------ spec/Spec/System/PermissionGrant.lean | 67 ------ spec/Spec/System/PlatformAdministration.lean | 221 ------------------ spec/Spec/System/ProjectGroup.lean | 75 ------ spec/Spec/System/ProjectWorkspace.lean | 53 ----- spec/Spec/System/User.lean | 12 - spec/lake-manifest.json | 6 - spec/lakefile.toml | 6 - spec/lean-toolchain | 1 - 66 files changed, 109 insertions(+), 2154 deletions(-) delete mode 100644 .gitea/workflows/spec-check.yml delete mode 100644 spec/.gitignore delete mode 100644 spec/README.md delete mode 100644 spec/Spec.lean delete mode 100644 spec/Spec/Courseware.lean delete mode 100644 spec/Spec/Courseware/Check.lean delete mode 100644 spec/Spec/Courseware/Check/Diagnostic.lean delete mode 100644 spec/Spec/Courseware/Check/Pipeline.lean delete mode 100644 spec/Spec/Courseware/Export.lean delete mode 100644 spec/Spec/Courseware/Export/Artifact.lean delete mode 100644 spec/Spec/Courseware/Export/Render.lean delete mode 100644 spec/Spec/Courseware/Model.lean delete mode 100644 spec/Spec/Courseware/Model/Element.lean delete mode 100644 spec/Spec/Courseware/Model/Info.lean delete mode 100644 spec/Spec/Courseware/Model/Lesson.lean delete mode 100644 spec/Spec/Courseware/Model/Primitives.lean delete mode 100644 spec/Spec/Courseware/Model/RichContent.lean delete mode 100644 spec/Spec/Courseware/Open.lean delete mode 100644 spec/Spec/Courseware/Open/Course.lean delete mode 100644 spec/Spec/Courseware/Open/QuestionBank.lean delete mode 100644 spec/Spec/Prelude.lean delete mode 100644 spec/Spec/System.lean delete mode 100644 spec/Spec/System/Agent/AgentRole.lean delete mode 100644 spec/Spec/System/Agent/AgentSurface.lean delete mode 100644 spec/Spec/System/Agent/Capability.lean delete mode 100644 spec/Spec/System/Agent/Memory.lean delete mode 100644 spec/Spec/System/Agent/Run.lean delete mode 100644 spec/Spec/System/Agent/Usage.lean delete mode 100644 spec/Spec/System/Audit.lean delete mode 100644 spec/Spec/System/Capacity.lean delete mode 100644 spec/Spec/System/Connections.lean delete mode 100644 spec/Spec/System/Connections/Feishu.lean delete mode 100644 spec/Spec/System/Connections/Prelude.lean delete mode 100644 spec/Spec/System/Hierarchy.lean delete mode 100644 spec/Spec/System/Lock.lean delete mode 100644 spec/Spec/System/Organization.lean delete mode 100644 spec/Spec/System/Permission.lean delete mode 100644 spec/Spec/System/PermissionGrant.lean delete mode 100644 spec/Spec/System/PlatformAdministration.lean delete mode 100644 spec/Spec/System/ProjectGroup.lean delete mode 100644 spec/Spec/System/ProjectWorkspace.lean delete mode 100644 spec/Spec/System/User.lean delete mode 100644 spec/lake-manifest.json delete mode 100644 spec/lakefile.toml delete mode 100644 spec/lean-toolchain diff --git a/.gitea/workflows/checker-check.yml b/.gitea/workflows/checker-check.yml index 96e027d..d892960 100644 --- a/.gitea/workflows/checker-check.yml +++ b/.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 -# (does it build, pass its tests, satisfy clippy + rustfmt?). It is NOT a -# spec-to-implementation conformance gate — implementations align to the Lean -# contract by human review, not by CI. See the repo README. +# This is an INTERNAL gate on the implementation's own health +# (does it build, pass its tests, satisfy clippy + rustfmt?). There is no +# decision-to-implementation conformance gate — implementations align to the +# ADRs by human review, not by CI. See the repo README. on: push: diff --git a/.gitea/workflows/hub-check.yml b/.gitea/workflows/hub-check.yml index 2549e19..29cdb17 100644 --- a/.gitea/workflows/hub-check.yml +++ b/.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 -# (spec/System implementation). This is an INTERNAL gate on the Hub's own +# The Hub is the Feishu-group collaboration + agent runtime half. +# This is an INTERNAL gate on the Hub's own # health, like checker-check is for the Rust half. on: diff --git a/.gitea/workflows/spec-check.yml b/.gitea/workflows/spec-check.yml deleted file mode 100644 index 8e862dc..0000000 --- a/.gitea/workflows/spec-check.yml +++ /dev/null @@ -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 diff --git a/.gitignore b/.gitignore index f6c770c..08f5590 100644 --- a/.gitignore +++ b/.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 diff --git a/.scratch/saas-production-readiness/issues/05-define-abuse-capacity-controls.md b/.scratch/saas-production-readiness/issues/05-define-abuse-capacity-controls.md index a30b6da..d28d18c 100644 --- a/.scratch/saas-production-readiness/issues/05-define-abuse-capacity-controls.md +++ b/.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: diff --git a/.scratch/saas-production-readiness/issues/08-prove-production-release-gate.md b/.scratch/saas-production-readiness/issues/08-prove-production-release-gate.md index 7603fe4..890e35d 100644 --- a/.scratch/saas-production-readiness/issues/08-prove-production-release-gate.md +++ b/.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? diff --git a/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md b/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md index 4f26fcf..f80dc80 100644 --- a/.scratch/saas-production-readiness/issues/27-reconcile-audit-history-contract.md +++ b/.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 diff --git a/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md b/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md index 017c68f..2ad2f2b 100644 --- a/.scratch/saas-production-readiness/issues/42-decide-platform-admin-identity-audit.md +++ b/.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). -The pinned semantic invariants are in -[`Spec.System.PlatformAdministration`](../../../spec/Spec/System/PlatformAdministration.lean), +[ADR-0023](../../../docs/adr/0023-platform-administrator-identity-and-audit.md), and the canonical terms are in [`CONTEXT.md`](../../../CONTEXT.md). Exact numeric session/invitation/step-up limits and browser mechanics remain diff --git a/AGENTS.md b/AGENTS.md index 5691183..2a53514 100644 --- a/AGENTS.md +++ b/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 语义母本),是产品语义的上游参照。 -- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。 +- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。 - `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 / - `Spec.System.ProjectWorkspace`)。 + 普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。 - 每个 org 自选 BYOK 或平台托管 model provider connection;平台托管也必须是该 org - 独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021 / - `Spec.System.Organization`)。 + 独享的 key/base URL,不得让无关 org 共用 process-global provider key(见 ADR-0021)。 - 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 / - `Spec.System.Capacity`)。 + Agent admission 必须持久、有界、跨 org 公平且显式背压(见 ADR-0022)。 - 平台管理员只通过独立的 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 写操作前与开发者确认(这是开发者的全局偏好)。 diff --git a/CLAUDE.md b/CLAUDE.md index 3fa92d2..fb42274 100644 --- a/CLAUDE.md +++ b/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 语义母本),是产品语义的上游参照。 -- 其余部件(将来的 `spec/` 外文件夹)是**向 `spec/` 对齐的实现**。 +- `docs/adr/` 是系统级决策的唯一权威来源;`CONTEXT.md` 是平台语言词汇表;代码注释把关键不变量锚到 ADR 编号,可 grep。 - `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 / - `Spec.System.ProjectWorkspace`)。 + 普通老师可在飞书群自助建 project 但受 org policy 控制(见 ADR-0021)。 ## 纪律 -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 写操作前与开发者确认(这是开发者的全局偏好)。 diff --git a/README.md b/README.md index 62e6688..02669f1 100644 --- a/README.md +++ b/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 契约引用) -spec/ ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md +docs/adr/ ← 系统级架构决策记录(跨部件,决策的唯一权威来源) +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 是研发侧的上游参照。** - `spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。 +1. **角色 —— ADR 是决策真相。** + 跨部件的语义决策只记录在 `docs/adr/`,一份决策一份 ADR,编号顺延、正文不改写历史。代码里的关键不变量用注释锚到 ADR 编号,保持可 grep。没有第二份权威文档。 -2. **对齐机制 —— Lean 只做上游参照。** - 不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。 - (CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。) +2. **对齐机制 —— 人肉承载,无机器兜底。** + CI 只验各部件自身良构(build / test / clippy),**没有**决策↔实现的一致性 gate。实现对齐 ADR,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。发现漂移,报告它,不要默默让其中一边将就另一边。 -3. **资产性 —— 由 review 纪律承载,无机器兜底。** - 这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。 +3. **形态 —— 自包含。** + 凡 ADR 未明文规定的,开发者与 agent 双方都不该假设;遇到没覆盖的地方,**显式 surface** 出来让开发者决定。 -4. **形态 —— 它是人机共识的契约。** - 契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。 - -5. **深度判据 —— 只收录分歧点。** - 一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。 - 深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。 +4. **深度判据 —— 只收录分歧点。** + 一条语义该不该写进 ADR,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进 ADR;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。 + 深度上限是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。 ## 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。 diff --git a/crates/README.md b/crates/README.md index 11eb86a..237c8a5 100644 --- a/crates/README.md +++ b/crates/README.md @@ -1,7 +1,8 @@ # crates/ -These crates implement the rule-based lesson checker that aligns to the -semantic master in `spec/`: it reads an engineering-file (one lesson, ADR-0005) +These crates implement the rule-based lesson checker whose semantics are +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), diff --git a/crates/cph-check/src/lib.rs b/crates/cph-check/src/lib.rs index 5cf0371..c925c63 100644 --- a/crates/cph-check/src/lib.rs +++ b/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 -/// `Spec.Courseware.renderIgnoredSeverity : Severity := .warning` -/// (`spec/Spec/Courseware/Check/Diagnostic.lean`), itself citing ADR-0005: when a +/// **PINNED to `warning` by 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, -/// alignable fact rather than an inline literal. +/// severity as a const makes "it is a warning, not an error" a greppable +/// 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 - /// implementation of `Spec.Courseware.Legal` (`spec/Spec/Courseware/Check/Diagnostic.lean`): - /// a lesson is *legal* iff its diagnostics contain no error-level diagnostic - /// (warnings are non-blocking — see `Severity` / ADR-0010). There is no CI - /// gate enforcing this alignment (repo constitution); it is kept greppable - /// here so a reviewer can tie the orchestrator's gate to the Lean master. + /// **Legality decision (ADR-0010).** `!has_errors()` decides lesson + /// legality: a lesson is *legal* iff its diagnostics contain no error-level + /// diagnostic (warnings are non-blocking — see `Severity`). There is no CI + /// gate enforcing ADR↔implementation alignment (repo constitution); it is + /// kept greppable here so a reviewer can tie the orchestrator's gate to + /// the ADR. pub fn has_errors(&self) -> bool { self.diagnostics .iter() diff --git a/crates/cph-diag/src/lib.rs b/crates/cph-diag/src/lib.rs index 453588f..4e2bdbf 100644 --- a/crates/cph-diag/src/lib.rs +++ b/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 -/// master (`spec/Spec/Courseware/Check/Diagnostic.lean`), whose definition is -/// exactly: +/// **Pinned by ADR-0005 / ADR-0010: exactly two values.** /// /// ```text -/// inductive Severity where -/// | warning -/// | error +/// warning | error /// ``` /// -/// This two-valued shape is a **contract decision**, not an accident: the Lean -/// module pins `Severity` to exactly `warning | error` and states the finer -/// levels (`info` / `hint` / `note`) are deliberately undecided. We therefore +/// This two-valued shape is a **contract decision**, not an accident: the +/// finer levels (`info` / `hint` / `note`) are deliberately undecided, so we /// 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); -/// it is maintained by review, which is why this correspondence is documented -/// here rather than only in the spec. +/// There is no CI gate enforcing ADR↔implementation alignment (see the repo +/// constitution); it is maintained by review, which is why the decision is +/// 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, } diff --git a/crates/cph-model/src/lib.rs b/crates/cph-model/src/lib.rs index a5aed91..09bc2be 100644 --- a/crates/cph-model/src/lib.rs +++ b/crates/cph-model/src/lib.rs @@ -3,9 +3,7 @@ //! This crate is the **loader**, not the full checker. It reads //! `/manifest.toml` (project / info / ordered `[[parts]]` / declared //! `[targets.*]`) and each part's `//element.toml`, and produces an -//! ordered [`Lesson`] — mirroring the Lean master's `Lesson = List (Element P)` -//! (`spec/Spec/Courseware/Model/Lesson.lean`), where the order of `parts` carries -//! teaching semantics. +//! ordered [`Lesson`], 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/.typ` when no `[[steps]]` are given. pub steps: Vec, /// The **render-coverage declaration**: which element kinds this target - /// renders. Realizes `Spec.Courseware.TargetSpec.covers : KindId → Prop` - /// (`spec/Spec/Courseware/Export/Render.lean`) and ADR-0011's "render - /// coverage is a declaration, not a payload": the contract keeps *which + /// renders. Realizes ADR-0011's "render + /// coverage is a declaration, not a payload": the declaration 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 -/// (`spec/Spec/Courseware/Export/Artifact.lean`), whose definition is exactly: +/// **Pinned by ADR-0011** as an ADT with fields: /// /// ```text -/// inductive Artifact where -/// | singleFile (filepath : String) -/// | fileTree (root : String) (outputs : String) +/// Artifact = singleFile (filepath) | fileTree (root, outputs) /// ``` /// /// 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 -/// alignment (see the repo constitution) — it is maintained by review, which is -/// why the correspondence is documented here. +/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing ADR↔ +/// implementation alignment (see the repo constitution) — it is maintained by +/// 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 - /// `Artifact.fileTree`. + /// A set of files under `root` matching the `outputs` glob. ADR-0011 + /// `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 -/// (`spec/Spec/Courseware/Export/Render.lean`), whose definition is exactly: +/// **Pinned by ADR-0011** as an ADT: /// /// ```text -/// inductive Step where -/// | typstCompile (template : String) -/// | shell (run : String) -/// | assembleMarkdown (field : String) +/// Step = typstCompile (template) | shell (run) | assembleMarkdown (field) /// ``` /// /// 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 - /// `Step.typstCompile`. + /// artifact; the framework injects the manifest. ADR-0011 + /// `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 - /// Lean `Step.assembleMarkdown` (ADR-0015). Not a typst build — the + /// element's `field` markdown content file in `[[parts]]` order. ADR-0011 + /// `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 -/// (`spec/Spec/Courseware/Model/Info.lean`): the *canonical* model whose +/// 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 -/// CI gate enforces this alignment (repo constitution); it is kept greppable. +/// at the load boundary. No +/// 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, } @@ -290,8 +278,7 @@ struct RawProject { name: String, } -/// The authoring-surface `[info]` (mirrors Lean `RawInfo` in -/// `spec/Spec/Courseware/Model/Info.lean`): the raw form that exists for +/// The authoring-surface `[info]`: 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 { match self { diff --git a/hub/package.json b/hub/package.json index 7d33c65..b8df102 100644 --- a/hub/package.json +++ b/hub/package.json @@ -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", diff --git a/hub/prisma/migrations/20260714120000_drop_legacy_platform_role_assignment/migration.sql b/hub/prisma/migrations/20260714120000_drop_legacy_platform_role_assignment/migration.sql index ed23cb6..d005fdb 100644 --- a/hub/prisma/migrations/20260714120000_drop_legacy_platform_role_assignment/migration.sql +++ b/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. diff --git a/hub/prisma/schema.prisma b/hub/prisma/schema.prisma index 0156a8f..9e619ea 100644 --- a/hub/prisma/schema.prisma +++ b/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 -// completeness OPEN — add states without a schema migration war). +// - AgentRunStatus adds WAITING_FOR_USER + TIMED_OUT (the run-state set is +// 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()) diff --git a/hub/src/agent/runner.ts b/hub/src/agent/runner.ts index ba47e96..b8fd0f4 100644 --- a/hub/src/agent/runner.ts +++ b/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` - * (ADR-0018 / `Spec.System.AgentSurface`) without re-implementing the + * provider secrets from Bash. This upholds the workspace-bounded file-op + * 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"; diff --git a/hub/src/capacity/dimensions.ts b/hub/src/capacity/dimensions.ts index 6c774c3..1dde1ce 100644 --- a/hub/src/capacity/dimensions.ts +++ b/hub/src/capacity/dimensions.ts @@ -1,6 +1,6 @@ /** - * ADR-0022 capacity dimensions (spec `Spec.System.Capacity.CapacityDimension`). - * The 23 PINNED dimensions; exact numeric ceilings are `OPEN` and calibrated by + * ADR-0022 capacity dimensions. + * 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. */ diff --git a/hub/src/org/capacityPolicy.ts b/hub/src/org/capacityPolicy.ts index 7815aee..e489255 100644 --- a/hub/src/org/capacityPolicy.ts +++ b/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 - * platform ceiling for that dimension. `LayeredLimit.effective` (min of the two) + * `CapacityDimension`. Enforces the layered-limit invariant: a set limit must be ≤ the + * 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. */ diff --git a/hub/src/org/members.ts b/hub/src/org/members.ts index 2fd7455..b0c2a77 100644 --- a/hub/src/org/members.ts +++ b/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. diff --git a/spec/.gitignore b/spec/.gitignore deleted file mode 100644 index bfb30ec..0000000 --- a/spec/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/.lake diff --git a/spec/README.md b/spec/README.md deleted file mode 100644 index b5e8a3a..0000000 --- a/spec/README.md +++ /dev/null @@ -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…`。 -- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。 diff --git a/spec/Spec.lean b/spec/Spec.lean deleted file mode 100644 index 46dd4a3..0000000 --- a/spec/Spec.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean deleted file mode 100644 index c8c4201..0000000 --- a/spec/Spec/Courseware.lean +++ /dev/null @@ -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`。 --/ diff --git a/spec/Spec/Courseware/Check.lean b/spec/Spec/Courseware/Check.lean deleted file mode 100644 index b326f16..0000000 --- a/spec/Spec/Courseware/Check.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Spec.Courseware.Check.Diagnostic -import Spec.Courseware.Check.Pipeline - -/-! -# Courseware.Check —— checker 语义 - -诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处 -ADR-0010。 --/ diff --git a/spec/Spec/Courseware/Check/Diagnostic.lean b/spec/Spec/Courseware/Check/Diagnostic.lean deleted file mode 100644 index de68494..0000000 --- a/spec/Spec/Courseware/Check/Diagnostic.lean +++ /dev/null @@ -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` 字段缺对应 `.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 diff --git a/spec/Spec/Courseware/Check/Pipeline.lean b/spec/Spec/Courseware/Check/Pipeline.lean deleted file mode 100644 index 2a27b5c..0000000 --- a/spec/Spec/Courseware/Check/Pipeline.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Export.lean b/spec/Spec/Courseware/Export.lean deleted file mode 100644 index 7788bd6..0000000 --- a/spec/Spec/Courseware/Export.lean +++ /dev/null @@ -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。 --/ diff --git a/spec/Spec/Courseware/Export/Artifact.lean b/spec/Spec/Courseware/Export/Artifact.lean deleted file mode 100644 index c30c931..0000000 --- a/spec/Spec/Courseware/Export/Artifact.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Export/Render.lean b/spec/Spec/Courseware/Export/Render.lean deleted file mode 100644 index 576dbe0..0000000 --- a/spec/Spec/Courseware/Export/Render.lean +++ /dev/null @@ -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 的 `.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 diff --git a/spec/Spec/Courseware/Model.lean b/spec/Spec/Courseware/Model.lean deleted file mode 100644 index c1be6be..0000000 --- a/spec/Spec/Courseware/Model.lean +++ /dev/null @@ -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。 --/ diff --git a/spec/Spec/Courseware/Model/Element.lean b/spec/Spec/Courseware/Model/Element.lean deleted file mode 100644 index 92bf401..0000000 --- a/spec/Spec/Courseware/Model/Element.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Model/Info.lean b/spec/Spec/Courseware/Model/Info.lean deleted file mode 100644 index 850f1b4..0000000 --- a/spec/Spec/Courseware/Model/Info.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Model/Lesson.lean b/spec/Spec/Courseware/Model/Lesson.lean deleted file mode 100644 index 3a3145d..0000000 --- a/spec/Spec/Courseware/Model/Lesson.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Model/Primitives.lean b/spec/Spec/Courseware/Model/Primitives.lean deleted file mode 100644 index eff743d..0000000 --- a/spec/Spec/Courseware/Model/Primitives.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Model/RichContent.lean b/spec/Spec/Courseware/Model/RichContent.lean deleted file mode 100644 index 2c9b3ba..0000000 --- a/spec/Spec/Courseware/Model/RichContent.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/Courseware/Open.lean b/spec/Spec/Courseware/Open.lean deleted file mode 100644 index 620c6aa..0000000 --- a/spec/Spec/Courseware/Open.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Spec.Courseware.Open.QuestionBank -import Spec.Courseware.Open.Course - -/-! -# Courseware.Open —— OPEN 骨架(核心关系) - -题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface -但未决策的 OPEN 分歧点,待专门 ADR 落定。 --/ diff --git a/spec/Spec/Courseware/Open/Course.lean b/spec/Spec/Courseware/Open/Course.lean deleted file mode 100644 index aeef406..0000000 --- a/spec/Spec/Courseware/Open/Course.lean +++ /dev/null @@ -1,10 +0,0 @@ -/-! -# Course —— 课程编排(骨架,规则 OPEN) - -ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的 -**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被 -引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。 - -此处不替它选解——不建 `Course := List Lesson`(那会偷偷承诺 -"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。 --/ diff --git a/spec/Spec/Courseware/Open/QuestionBank.lean b/spec/Spec/Courseware/Open/QuestionBank.lean deleted file mode 100644 index 57d629c..0000000 --- a/spec/Spec/Courseware/Open/QuestionBank.lean +++ /dev/null @@ -1,10 +0,0 @@ -/-! -# QuestionBank —— 题库(骨架,核心关系 OPEN) - -题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最 -典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确 -指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存? - -这是一个 `OPEN` 分歧点。此处不替它选解——不建 `QuestionRef` 也不建 -内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。 --/ diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean deleted file mode 100644 index e89b4fa..0000000 --- a/spec/Spec/Prelude.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean deleted file mode 100644 index f92b70a..0000000 --- a/spec/Spec/System.lean +++ /dev/null @@ -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。 --/ diff --git a/spec/Spec/System/Agent/AgentRole.lean b/spec/Spec/System/Agent/AgentRole.lean deleted file mode 100644 index 70aeedd..0000000 --- a/spec/Spec/System/Agent/AgentRole.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Agent/AgentSurface.lean b/spec/Spec/System/Agent/AgentSurface.lean deleted file mode 100644 index 2e4ba9d..0000000 --- a/spec/Spec/System/Agent/AgentSurface.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Agent/Capability.lean b/spec/Spec/System/Agent/Capability.lean deleted file mode 100644 index f89f23e..0000000 --- a/spec/Spec/System/Agent/Capability.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Agent/Memory.lean b/spec/Spec/System/Agent/Memory.lean deleted file mode 100644 index fa9ec14..0000000 --- a/spec/Spec/System/Agent/Memory.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Agent/Run.lean b/spec/Spec/System/Agent/Run.lean deleted file mode 100644 index 46bcb12..0000000 --- a/spec/Spec/System/Agent/Run.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Agent/Usage.lean b/spec/Spec/System/Agent/Usage.lean deleted file mode 100644 index 64ed69a..0000000 --- a/spec/Spec/System/Agent/Usage.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Audit.lean b/spec/Spec/System/Audit.lean deleted file mode 100644 index 54f2dcf..0000000 --- a/spec/Spec/System/Audit.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Capacity.lean b/spec/Spec/System/Capacity.lean deleted file mode 100644 index 0e3452d..0000000 --- a/spec/Spec/System/Capacity.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Connections.lean b/spec/Spec/System/Connections.lean deleted file mode 100644 index f7fd47a..0000000 --- a/spec/Spec/System/Connections.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Connections/Feishu.lean b/spec/Spec/System/Connections/Feishu.lean deleted file mode 100644 index 6df3b94..0000000 --- a/spec/Spec/System/Connections/Feishu.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Connections/Prelude.lean b/spec/Spec/System/Connections/Prelude.lean deleted file mode 100644 index 8e1aab1..0000000 --- a/spec/Spec/System/Connections/Prelude.lean +++ /dev/null @@ -1,15 +0,0 @@ -/-! -# Connections.Prelude —— 连接提供商 - -用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。 -模型 provider connection 是独立概念,见 `Spec.System.Organization`。 --/ - -namespace Spec.System - -/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/ -inductive ConnectionProvider where - /-- 飞书(`PINNED`)。 -/ - | feishu - -end Spec.System diff --git a/spec/Spec/System/Hierarchy.lean b/spec/Spec/System/Hierarchy.lean deleted file mode 100644 index 63f6896..0000000 --- a/spec/Spec/System/Hierarchy.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Lock.lean b/spec/Spec/System/Lock.lean deleted file mode 100644 index a24afea..0000000 --- a/spec/Spec/System/Lock.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Organization.lean b/spec/Spec/System/Organization.lean deleted file mode 100644 index 372fd1f..0000000 --- a/spec/Spec/System/Organization.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/Permission.lean b/spec/Spec/System/Permission.lean deleted file mode 100644 index 4c3fb9e..0000000 --- a/spec/Spec/System/Permission.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/PermissionGrant.lean b/spec/Spec/System/PermissionGrant.lean deleted file mode 100644 index 30d607b..0000000 --- a/spec/Spec/System/PermissionGrant.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/PlatformAdministration.lean b/spec/Spec/System/PlatformAdministration.lean deleted file mode 100644 index 92f83d6..0000000 --- a/spec/Spec/System/PlatformAdministration.lean +++ /dev/null @@ -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 diff --git a/spec/Spec/System/ProjectGroup.lean b/spec/Spec/System/ProjectGroup.lean deleted file mode 100644 index c4cb43e..0000000 --- a/spec/Spec/System/ProjectGroup.lean +++ /dev/null @@ -1,75 +0,0 @@ -import Spec.Prelude - -/-! -# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001/0017) - -一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`, -见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、 -与 agent 生命周期相互独立。 - -**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived -historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。 -群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。 - -**当前角色(`PINNED`, ADR-0017):** active binding 选择一个 Organization-scoped Agent -role;普通群消息在接收时冻结该 role,随后即使群切换角色,已接收工作也不漂移。切换角色 -只改变后续工作路由,不把不同 role 的 provider session 合并。每个 Organization 有一个 -active 默认 role 用于初始化新 binding,role 名称不硬编码。切换共享 role 的 actor 必须同时 -通过 project `agent.trigger` 与目标 role `role.trigger`;不额外要求 project `MANAGE`。 --/ - -namespace Spec.System - -variable (I : Identifiers) - -/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的 -绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/ -structure ProjectGroup where - /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/ - chat : I.ChatId - -/-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。 -`ProjectId → Option ChatId` 的结构本身即"一个 project 至多绑一个 active 群"(由 `Option` -自带);良构补另一半——单射。 -/ -def GroupBinding := I.ProjectId → Option I.ChatId - -/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。 -"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。 -archived historical bindings 不在本快照不变式内。 -/ -def GroupBinding.WellFormed (b : GroupBinding I) : Prop := - ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂ - -/-- 每个 Organization 的 active 默认 Agent role(`PINNED`, ADR-0017)。函数形状钉死每个 -Organization 恰好一个默认值;role 是否 active 及租户归属由 `WellScoped` 约束。 -/ -def OrganizationDefaultRole := I.OrganizationId → I.AgentRoleId - -/-- 默认 role 必须属于作为其 key 的同一个 Organization(`PINNED`, ADR-0017)。 -/ -def OrganizationDefaultRole.WellScoped - (defaults : OrganizationDefaultRole I) - (roleOrg : I.AgentRoleId → Option I.OrganizationId) : Prop := - ∀ o, roleOrg (defaults o) = some o - -/-- Active 项目群选择的 Agent role(`PINNED`, ADR-0017)。role 属于项目 Organization; -具体外键表示是 plumbing,由 `WellScoped` 钉死租户边界。 -/ -structure GroupSelectedRole where - /-- 被选择 role 的项目。 -/ - project : I.ProjectId - /-- 作用于该项目 active 群的动态 Agent role。 -/ - role : I.AgentRoleId - -/-- 群所选 role 必须与 project 同 Organization(`PINNED`, ADR-0017)。 -/ -def GroupSelectedRole.WellScoped - (selection : GroupSelectedRole I) - (projectOrg : I.ProjectId → Option I.OrganizationId) - (roleOrg : I.AgentRoleId → Option I.OrganizationId) : Prop := - ∃ o, projectOrg selection.project = some o ∧ roleOrg selection.role = some o - -/-- 已接收群工作冻结其 role(`PINNED`, ADR-0017):调度时使用 admission 中记录的 role, -而不是重新读取可能已经变化的群当前 role。 -/ -structure GroupRunRoleSnapshot where - /-- 被接收的一次 run。 -/ - run : I.RunId - /-- 接收时冻结的 role。 -/ - role : I.AgentRoleId - -end Spec.System diff --git a/spec/Spec/System/ProjectWorkspace.lean b/spec/Spec/System/ProjectWorkspace.lean deleted file mode 100644 index 1edd89f..0000000 --- a/spec/Spec/System/ProjectWorkspace.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Spec.Prelude - -/-! -# ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021) - -org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前 -不是权限资源。project 仍是授权边界。 - -不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受 -org policy 控制。folder visibility/team policy/继承授权 `OPEN`。 --/ - -namespace Spec.System - -variable (I : Identifiers) - -/-- Project explorer folder 的租户归属(`PINNED`, ADR-0021):folder 是 org 内透明节点。 -/ -structure FolderTenancy where - /-- 被归属的 folder(`PINNED`, ADR-0021)。 -/ - folder : I.FolderId - /-- folder 所属 organization(`PINNED`, ADR-0021)。 -/ - organization : I.OrganizationId - -/-- Project 放入 folder 的作用域(`PINNED`, ADR-0021):project 可以位于某个 folder, -但二者必须同 org。folder 不改变 project 权限。 -/ -structure ProjectFolderPlacement where - /-- 被放置的 project(`PINNED`, ADR-0021)。 -/ - project : I.ProjectId - /-- project 所在 folder(`PINNED`, ADR-0021)。 -/ - folder : I.FolderId - -/-- Project-folder placement 是良构的 iff project 与 folder 解析到同一 organization -(`PINNED`, ADR-0021)。 -/ -def ProjectFolderPlacement.WellScoped - (placement : ProjectFolderPlacement I) - (projectOrg : I.ProjectId → Option I.OrganizationId) - (folderOrg : I.FolderId → Option I.OrganizationId) : Prop := - ∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o - -/-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project -不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/ -structure FolderTransparent where - /-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/ - current : True - -/-- 普通 org member 是否可从 Feishu 群自助创建 project 的 org policy(`PINNED`, ADR-0021)。 -/ -structure MemberProjectCreationPolicy where - /-- policy 所属 organization(`PINNED`, ADR-0021)。 -/ - organization : I.OrganizationId - /-- 为 true 时普通成员可从未绑定飞书群创建 project;owner/admin 可走后台入口。 -/ - membersCanCreateProjects : Bool - -end Spec.System diff --git a/spec/Spec/System/User.lean b/spec/Spec/System/User.lean deleted file mode 100644 index c1f2aa7..0000000 --- a/spec/Spec/System/User.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Spec.Prelude - -/-! -# User —— 用户创建路径 - -用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。 - -用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。 --/ - -namespace Spec.System -end Spec.System diff --git a/spec/lake-manifest.json b/spec/lake-manifest.json deleted file mode 100644 index d041e82..0000000 --- a/spec/lake-manifest.json +++ /dev/null @@ -1,6 +0,0 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [], - "name": "Spec", - "lakeDir": ".lake", - "fixedToolchain": false} diff --git a/spec/lakefile.toml b/spec/lakefile.toml deleted file mode 100644 index 6db46dc..0000000 --- a/spec/lakefile.toml +++ /dev/null @@ -1,6 +0,0 @@ -name = "Spec" -version = "0.1.0" -defaultTargets = ["Spec"] - -[[lean_lib]] -name = "Spec" diff --git a/spec/lean-toolchain b/spec/lean-toolchain deleted file mode 100644 index 18640c8..0000000 --- a/spec/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.31.0