docs: define platform admin identity boundary

spec/Spec/Prelude.lean

@@ -1,7 +1,7 @@
 /-!
 # Prelude —— System 层共享标识符
 
-平台层反复引用一组标识符(项目、run、session、principal、chat)。其内部表示从未被决策
+平台层反复引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。其内部表示从未被决策
 (UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
 **关系**,却不对标识符表示作承诺。
@@ -33,5 +33,22 @@ structure Identifiers where
       ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
       类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
   ChatId : Type
+  /-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
+  PlatformIdentityId : Type
+  /-- 平台自有飞书应用标识(`OPEN` 表示;ADR-0023,与各 org 客户应用分离)。 -/
+  PlatformFeishuApplicationId : Type
+  /-- 平台应用所验证的外部飞书用户标识(`OPEN` 表示;ADR-0023,其具体 open_id/user_id
+      表示与迁移方式不在本层固定)。 -/
+  PlatformExternalUserId : Type
+  /-- 可撤销 Platform Session 标识(`OPEN` 表示;ADR-0023)。 -/
+  PlatformSessionId : Type
+  /-- Platform Administrator invitation 标识(`OPEN` 表示;ADR-0023)。 -/
+  PlatformInvitationId : Type
+  /-- 一次平台控制面 mutation 标识(`OPEN` 表示;ADR-0023)。 -/
+  PlatformMutationId : Type
+  /-- 独立 Platform Audit Entry 标识(`OPEN` 表示;ADR-0023)。 -/
+  PlatformAuditEntryId : Type
+  /-- 平台离线恢复所声明的 incident 标识(`OPEN` 表示;ADR-0023)。 -/
+  PlatformIncidentId : Type
 
 end Spec.System

spec/Spec/System.lean

@@ -2,6 +2,7 @@ import Spec.System.ProjectGroup
 import Spec.System.Organization
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
+import Spec.System.PlatformAdministration
 import Spec.System.Run
 import Spec.System.Lock
 import Spec.System.Memory
@@ -22,6 +23,8 @@ import Spec.System.Audit
   (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
   平台紧急工作负载制动(ADR-0022)。
+- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
+  保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
@@ -30,7 +33,8 @@ import Spec.System.Audit
 - `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
 - `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
   (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
-- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
+- `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform
+  Audit 由 `PlatformAdministration` 独立钉死。
 
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0022。
+标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0023。
 -/

spec/Spec/System/Audit.lean

@@ -1,7 +1,7 @@
 import Spec.Prelude
 
 /-!
-# Audit —— 审计日志(有意从简)
+# Audit —— Project/Run 审计日志(有意从简)
 
 likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
 但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
@@ -14,7 +14,8 @@ namespace Spec.System
 
 /-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
 关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
-对应 ADR 落定。 -/
+对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见
+`Spec.System.PlatformAdministration`,不复用本结构。 -/
 structure AuditEntry (I : Identifiers) where
   /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
   run : I.RunId

spec/Spec/System/Organization.lean

@@ -10,7 +10,8 @@ ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root
 
 本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
 不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
-provider 细节、平台控制面角色集合仍为 `OPEN`。
+provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
+`Spec.System.PlatformAdministration` 独立决定。
 -/
 
 namespace Spec.System

spec/Spec/System/Permission.lean

@@ -60,7 +60,8 @@ theorem Role.can_mono {r₁ r₂ : Role} {c : Capability}
 
 /-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only
 override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立
-谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/
+谓词;`isAdmin` 由 ADR-0023 的 `Spec.System.PlatformAdministration` 独立判定,
+本层不把平台权力折进 project role。 -/
 def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
 
 end Spec.System

spec/Spec/System/PlatformAdministration.lean

@@ -0,0 +1,221 @@
+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