From 38c32311903fd090bac2b28ba768537e51931068 Mon Sep 17 00:00:00 2001 From: sjfhsjfh Date: Sun, 12 Jul 2026 15:54:16 +0800 Subject: [PATCH] refactor(spec): generalize Feishu to Connections MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Connections/Prelude.lean: ConnectionProvider 枚举 (当前仅飞书) - Connections/Feishu.lean: FeishuAppBinding + FeishuProfile - Connections.lean: ConnectionBinding/ConnectionProfile inductive - Organization.feishu → connections: List ConnectionBinding - User.feishu → connections: List ConnectionProfile - 删除 FeishuConnection.lean --- spec/Spec/System.lean | 5 ++-- spec/Spec/System/Connections.lean | 24 +++++++++++++++++++ .../Feishu.lean} | 7 +++--- spec/Spec/System/Connections/Prelude.lean | 15 ++++++++++++ spec/Spec/System/Hierarchy.lean | 15 ++++++------ spec/Spec/System/User.lean | 2 +- 6 files changed, 53 insertions(+), 15 deletions(-) create mode 100644 spec/Spec/System/Connections.lean rename spec/Spec/System/{FeishuConnection.lean => Connections/Feishu.lean} (69%) create mode 100644 spec/Spec/System/Connections/Prelude.lean diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index 9be50a8..3a4db08 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -2,7 +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.Connections import Spec.System.ProjectWorkspace import Spec.System.Capacity import Spec.System.PlatformAdministration @@ -21,7 +21,8 @@ import Spec.System.Audit **语义分歧点**: - `Hierarchy` —— 三层主体:平台 → 组织 → 用户。 -- `User` —— 飞书绑定:登录途径,不是用户本体。 +- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。 +- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。 - `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org; connection secret 信封与 fail-closed resolver(ADR-0024); diff --git a/spec/Spec/System/Connections.lean b/spec/Spec/System/Connections.lean new file mode 100644 index 0000000..f7fd47a --- /dev/null +++ b/spec/Spec/System/Connections.lean @@ -0,0 +1,24 @@ +import Spec.System.Connections.Prelude +import Spec.System.Connections.Feishu + +/-! +# Connections —— 连接绑定与用户信息 + +组织/用户的外部连接。提供商枚举见 `Connections.Prelude`; +飞书具体类型见 `Connections.Feishu`。 +-/ + +namespace Spec.System + + +/-- 组织连接绑定(`PINNED`)。 -/ +inductive ConnectionBinding (I : Identifiers) where + /-- 飞书(`PINNED`)。 -/ + | feishu : FeishuAppBinding I → ConnectionBinding I + +/-- 用户连接信息(`PINNED`)。 -/ +inductive ConnectionProfile (I : Identifiers) where + /-- 飞书(`PINNED`)。 -/ + | feishu : FeishuProfile I → ConnectionProfile I + +end Spec.System diff --git a/spec/Spec/System/FeishuConnection.lean b/spec/Spec/System/Connections/Feishu.lean similarity index 69% rename from spec/Spec/System/FeishuConnection.lean rename to spec/Spec/System/Connections/Feishu.lean index 06d82df..6df3b94 100644 --- a/spec/Spec/System/FeishuConnection.lean +++ b/spec/Spec/System/Connections/Feishu.lean @@ -1,10 +1,9 @@ import Spec.Prelude /-! -# Feishu —— 组织飞书应用绑定与用户飞书信息 +# Feishu —— 飞书连接 -组织绑定一个飞书企业应用(1:1, `Option` 自带)。用户经此应用登录、调飞书 API。 -绑定是组织级;用户通过所属组织隐含获得绑定作用域。 +组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。 -/ namespace Spec.System @@ -18,7 +17,7 @@ structure FeishuAppBinding where /-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/ appSecretEnvelope : I.FeishuAppSecretRef -/-- 用户的飞书信息(`PINNED`)。User 上的可选绑定载荷。 -/ +/-- 用户的飞书信息(`PINNED`)。 -/ structure FeishuProfile where /-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/ openId : I.FeishuOpenId diff --git a/spec/Spec/System/Connections/Prelude.lean b/spec/Spec/System/Connections/Prelude.lean new file mode 100644 index 0000000..8e1aab1 --- /dev/null +++ b/spec/Spec/System/Connections/Prelude.lean @@ -0,0 +1,15 @@ +/-! +# Connections.Prelude —— 连接提供商 + +用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。 +模型 provider connection 是独立概念,见 `Spec.System.Organization`。 +-/ + +namespace Spec.System + +/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/ +inductive ConnectionProvider where + /-- 飞书(`PINNED`)。 -/ + | feishu + +end Spec.System diff --git a/spec/Spec/System/Hierarchy.lean b/spec/Spec/System/Hierarchy.lean index a48a89c..63f6896 100644 --- a/spec/Spec/System/Hierarchy.lean +++ b/spec/Spec/System/Hierarchy.lean @@ -1,6 +1,5 @@ import Spec.Prelude -import Spec.System.User -import Spec.System.FeishuConnection +import Spec.System.Connections /-! # Hierarchy —— 主体层级 @@ -24,14 +23,14 @@ structure Platform where /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/ application : I.PlatformFeishuApplicationId /-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。 -飞书应用绑定 1:1(`Option` 自带),见 `FeishuConnection`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/ +外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/ structure Organization where /-- 组织标识(`OPEN` 表示)。 -/ id : I.OrganizationId - /-- 飞书应用绑定(`PINNED`, 可选;1:1,每 org 至多一个)。 -/ - feishu : Option (FeishuAppBinding I) + /-- 外部连接(`PINNED`)。 -/ + connections : List (ConnectionBinding I) -/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。飞书绑定见 `FeishuConnection`。 -/ +/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/ structure User where /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/ id : I.UserId @@ -41,7 +40,7 @@ structure User where displayName : String /-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/ passwordHash : String - /-- 飞书绑定(`PINNED`, 可选)。 -/ - feishu : Option (FeishuProfile I) + /-- 外部连接(`PINNED`)。 -/ + connections : List (ConnectionProfile I) end Spec.System diff --git a/spec/Spec/System/User.lean b/spec/Spec/System/User.lean index bcba36a..d04b11a 100644 --- a/spec/Spec/System/User.lean +++ b/spec/Spec/System/User.lean @@ -3,7 +3,7 @@ import Spec.Prelude /-! # User —— 用户创建路径 -用户实体见 `Hierarchy.User`;飞书绑定见 `Spec.System.FeishuConnection`。 +用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。 用户创建当前只钉管理员直接创建;飞书自助注册→管理员审批未钉死(`OPEN`)。 -/