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`)。 -/