diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index ebe6001..4cf12b9 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -22,8 +22,8 @@ import Spec.System.Audit - `Hierarchy` —— 三层主体:平台 → 组织 → 用户。 - `User` —— 飞书绑定:登录途径,不是用户本体。 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。 -- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org; - connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024);组织级角色格 +- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org; + connection secret 信封与 fail-closed resolver(ADR-0024); owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界 (ADR-0021)。 @@ -36,7 +36,7 @@ import Spec.System.Audit - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。 - `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交—— Lock 限定并发,Surface 限定波及面。机制 OPEN。 -- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。 +- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。 - `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构 (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。 - `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform diff --git a/spec/Spec/System/Hierarchy.lean b/spec/Spec/System/Hierarchy.lean index f6f9f1c..73eaff7 100644 --- a/spec/Spec/System/Hierarchy.lean +++ b/spec/Spec/System/Hierarchy.lean @@ -18,23 +18,17 @@ import Spec.System.User namespace Spec.System variable (I : Identifiers) - -/-- 平台(`PINNED`, SaaS 提供方实体)。平台只有一个,独立于组织(租户)。平台管理 -身份、会话、审计、紧急恢复等由 `PlatformAdministration`(ADR-0023)定义;本 struct 只 -锚定平台在层级中的位置及其飞书应用归属。平台管理员不复用 `User` 或 org membership。 -/ +/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/ structure Platform where - /-- 平台自有的飞书应用(`PINNED`, ADR-0023),用于平台管理员认证;与各 org 客户应用分离。 -/ + /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/ application : I.PlatformFeishuApplicationId - -/-- 组织(`PINNED`, 租户根, ADR-0020)。每个 project/team 必须归属且仅归属一个组织。 -组织级角色格(owner/admin/member)、tenancy 关系、provider connection 凭据模式详见 -`Spec.System.Organization`。 -/ +/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。 +角色/tenancy/凭据见 `Spec.System.Organization`。 -/ structure Organization where - /-- 组织标识(`OPEN` 表示,ADR-0020 tenant root)。 -/ + /-- 组织标识(`OPEN` 表示)。 -/ id : I.OrganizationId -/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织(结构钉死)。飞书身份是绑定 -不是本体,详见 `Spec.System.User`。 -/ +/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。飞书身份是绑定,见 `Spec.System.User`。 -/ structure User where /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/ id : I.UserId diff --git a/spec/Spec/System/Organization.lean b/spec/Spec/System/Organization.lean index 3739f79..972c0a8 100644 --- a/spec/Spec/System/Organization.lean +++ b/spec/Spec/System/Organization.lean @@ -1,9 +1,9 @@ import Spec.Prelude /-! -# Organization —— SaaS tenant root (ADR-0020, ADR-0024) +# Organization —— SaaS 租户 (ADR-0020, ADR-0024) -组织是租户根。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。 +组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。 组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见 `PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。 -/