docs: define SaaS capacity controls

spec/Spec/System/Capacity.lean

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

spec/Spec/System/Organization.lean

@@ -9,7 +9,8 @@ ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root
 不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
 
 本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
-不得跨 org。用户身份、外部目录 provider 细节、平台控制面角色集合仍为 `OPEN`。
+不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
+provider 细节、平台控制面角色集合仍为 `OPEN`。
 -/
 
 namespace Spec.System
@@ -48,4 +49,20 @@ def TeamProjectGrantScope.WellScoped
     (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
   ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
 
+/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
+管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
+都不允许无关 org 共用 process-global provider key。模式切换过程仍为 `OPEN`。 -/
+inductive ProviderCredentialMode where
+  | byok
+  | platformManaged
+
+/-- Organization 的 model provider connection(`PINNED`, ADR-0021):connection 必须
+归属一个且仅一个 organization,并明确采用哪一种凭据模式。key/base URL 的加密表示、
+轮换与 resolver 机制由后续 secret-control-plane 决策规定。 -/
+structure OrganizationProviderConnection where
+  /-- connection 所属 organization(`PINNED`, ADR-0021)。 -/
+  organization : I.OrganizationId
+  /-- connection 的凭据归属模式(`PINNED`, ADR-0021)。 -/
+  mode : ProviderCredentialMode
+
 end Spec.System

spec/Spec/System/Run.lean

@@ -8,21 +8,23 @@
 
 namespace Spec.System
 
-/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`**
-——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认
-本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
+/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
+**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
+surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
 inductive RunState where
   | active
   | waitingForUser
   | completed
   | failed
   | timedOut
+  | limitExceeded
   | canceled
 
-/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled
-时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/
+/-- run 处于**终止态**(`PINNED`, ADR-0002, ADR-0022:锁在 completes/fails/
+timesOut/limitExceeded/canceled 时释放)。`active`/`waitingForUser` 非终止——后者仍
+占用项目(锁未释放)。 -/
 def RunState.Terminal : RunState → Prop
-  | .completed | .failed | .timedOut | .canceled => True
+  | .completed | .failed | .timedOut | .limitExceeded | .canceled => True
   | .active | .waitingForUser => False
 
 end Spec.System