chore: Merge origin/main: hub v0.0.23-v0.0.25 into main with spec-rewrite

spec/Spec/Prelude.lean

@@ -36,6 +36,9 @@ structure Identifiers where
   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

spec/Spec/System/ProjectGroup.lean

@@ -1,7 +1,7 @@
 import Spec.Prelude
 
 /-!
-# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
+# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001/0017)
 
 一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
 见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
@@ -10,6 +10,12 @@ import Spec.Prelude
 **绑定历史(`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
@@ -33,4 +39,37 @@ 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