From 39bd2c9ff7b75c57b1d75b7df40158eea07bd5ce Mon Sep 17 00:00:00 2001
From: sjfhsjfh <sjfhsjfh@qq.com>
Date: Sun, 12 Jul 2026 09:29:41 +0800
Subject: [PATCH] feat(spec): pin org-feishu app binding to 1:1
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- FeishuConnection.lean: FeishuAppBinding (appId + appSecretEnvelope)
- Organization.feishu: Option FeishuAppBinding (Option 自带 1:1)
- 删除 FeishuConnectionId (不再需要游离类型)
- FeishuProfile 删除 connection 字段 (由 org 隐含)
---
 spec/Spec/Prelude.lean                 |  6 ++++--
 spec/Spec/System.lean                  |  1 +
 spec/Spec/System/FeishuConnection.lean | 21 +++++++++++++++++++++
 spec/Spec/System/Hierarchy.lean        |  5 ++++-
 spec/Spec/System/User.lean             |  2 --
 5 files changed, 30 insertions(+), 5 deletions(-)
 create mode 100644 spec/Spec/System/FeishuConnection.lean

diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean
index 5c5323f..85342b3 100644
--- a/spec/Spec/Prelude.lean
+++ b/spec/Spec/Prelude.lean
@@ -21,8 +21,10 @@ structure Identifiers where
   FeishuOpenId : Type
   /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
   FeishuUserId : Type
-  /-- 组织飞书应用连接标识(`OPEN` 表示;org-scoped)。 -/
-  FeishuConnectionId : 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 透明组织节点,非权限资源)。 -/
diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean
index 4cf12b9..9be50a8 100644
--- a/spec/Spec/System.lean
+++ b/spec/Spec/System.lean
@@ -2,6 +2,7 @@ import Spec.System.Hierarchy
 import Spec.System.ProjectGroup
 import Spec.System.Organization
 import Spec.System.User
+import Spec.System.FeishuConnection
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
 import Spec.System.PlatformAdministration
diff --git a/spec/Spec/System/FeishuConnection.lean b/spec/Spec/System/FeishuConnection.lean
new file mode 100644
index 0000000..0b2f1d6
--- /dev/null
+++ b/spec/Spec/System/FeishuConnection.lean
@@ -0,0 +1,21 @@
+import Spec.Prelude
+
+/-!
+# FeishuConnection —— 组织飞书应用绑定
+
+一个组织绑定一个飞书企业应用(1:1, `Option` 结构自带)。用户经此应用登录、调飞书 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
+
+end Spec.System
diff --git a/spec/Spec/System/Hierarchy.lean b/spec/Spec/System/Hierarchy.lean
index 73eaff7..c327a75 100644
--- a/spec/Spec/System/Hierarchy.lean
+++ b/spec/Spec/System/Hierarchy.lean
@@ -1,5 +1,6 @@
 import Spec.Prelude
 import Spec.System.User
+import Spec.System.FeishuConnection
 
 /-!
 # Hierarchy —— 主体层级
@@ -23,10 +24,12 @@ structure Platform where
   /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
   application : I.PlatformFeishuApplicationId
 /-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
-角色/tenancy/凭据见 `Spec.System.Organization`。 -/
+飞书应用绑定 1:1(`Option` 自带),见 `FeishuConnection`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
 structure Organization where
   /-- 组织标识(`OPEN` 表示)。 -/
   id : I.OrganizationId
+  /-- 飞书应用绑定(`PINNED`, 可选;1:1,每 org 至多一个)。 -/
+  feishu : Option (FeishuAppBinding I)
 
 /-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。飞书身份是绑定,见 `Spec.System.User`。 -/
 structure User where
diff --git a/spec/Spec/System/User.lean b/spec/Spec/System/User.lean
index 127fcaa..fb6d603 100644
--- a/spec/Spec/System/User.lean
+++ b/spec/Spec/System/User.lean
@@ -17,8 +17,6 @@ structure FeishuProfile where
   openId : I.FeishuOpenId
   /-- 租户内身份(`OPEN` 表示);换应用不变,比 open_id 稳定。 -/
   userId : I.FeishuUserId
-  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped)。 -/
-  connection : I.FeishuConnectionId
   /-- 飞书显示名(`OPEN`)。 -/
   name : Option String
   /-- 飞书头像 URL(`OPEN`)。 -/