feat: secure organization provider credentials

spec/Spec/System.lean

@@ -18,7 +18,8 @@ import Spec.System.Audit
 **语义分歧点**:
 
 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
-- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org。
+- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
+  connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024)。
 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
   (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
@@ -36,5 +37,5 @@ import Spec.System.Audit
 - `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform
   Audit 由 `PlatformAdministration` 独立钉死。
 
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0023。
+标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0024。
 -/

spec/Spec/System/Organization.lean

@@ -1,7 +1,7 @@
 import Spec.Prelude
 
 /-!
-# Organization —— SaaS tenant root (ADR-0020)
+# Organization —— SaaS tenant root (ADR-0020, ADR-0024)
 
 ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
 `Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
@@ -11,7 +11,8 @@ ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root
 本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
 不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
 provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
-`Spec.System.PlatformAdministration` 独立决定。
+`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
+writer authority 与 fail-closed resolver 由 ADR-0024 固定。
 -/
 
 namespace Spec.System
@@ -57,13 +58,50 @@ inductive ProviderCredentialMode where
   | byok
   | platformManaged
 
-/-- Organization 的 model provider connection(`PINNED`, ADR-0021):connection 必须
-归属一个且仅一个 organization,并明确采用哪一种凭据模式。key/base URL 的加密表示、
-轮换与 resolver 机制由后续 secret-control-plane 决策规定。 -/
+/-- 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 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 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
+
 end Spec.System