forked from EduCraft/curriculum-project-hub
sjfhsjfh
3ebe4b754d
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
130 lines
5.9 KiB
Lean4
130 lines
5.9 KiB
Lean4
import Spec.Prelude
|
||
|
||
/-!
|
||
# Organization —— SaaS 租户 (ADR-0020, ADR-0024)
|
||
|
||
组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
|
||
组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
|
||
`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
|
||
`Spec.System.Agent.AgentRole`。
|
||
-/
|
||
|
||
namespace Spec.System
|
||
|
||
variable (I : Identifiers)
|
||
|
||
/-- 课程项目的租户归属(`PINNED`, ADR-0020):每个 project 必须有一个 organization。 -/
|
||
structure ProjectTenancy where
|
||
/-- 被归属的课程项目(`PINNED`, ADR-0020)。 -/
|
||
project : I.ProjectId
|
||
/-- project 所属 organization(`PINNED`, ADR-0020)。 -/
|
||
organization : I.OrganizationId
|
||
|
||
/-- Hub team 的租户归属(`PINNED`, ADR-0020):team 是 org-scoped principal。 -/
|
||
structure TeamTenancy where
|
||
/-- 被归属的 Hub team(`PINNED`, ADR-0020)。 -/
|
||
team : I.TeamId
|
||
/-- team 所属 organization(`PINNED`, ADR-0020)。 -/
|
||
organization : I.OrganizationId
|
||
|
||
/-- Team 对 project 的授权作用域(`PINNED`, ADR-0020):`PermissionGrant` 可以把
|
||
TEAM principal 授给 PROJECT resource,但该 grant 必须同 org。role 本身仍由
|
||
`PermissionGrant`/`Permission` 定义,这里仅刻画 tenant well-scopedness。 -/
|
||
structure TeamProjectGrantScope where
|
||
/-- 被授权的 project(`PINNED`, ADR-0020)。 -/
|
||
project : I.ProjectId
|
||
/-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
|
||
team : I.TeamId
|
||
/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
|
||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
|
||
team grant 必须被拒绝。 -/
|
||
def TeamProjectGrantScope.WellScoped
|
||
(grant : TeamProjectGrantScope I)
|
||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||
(teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
|
||
∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
|
||
|
||
/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
|
||
跨 org 共用 process-global key。模式切换 `OPEN`。 -/
|
||
inductive ProviderCredentialMode where
|
||
| byok
|
||
| platformManaged
|
||
|
||
/-- 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 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 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
|
||
|
||
|
||
/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
|
||
inductive OrganizationRole where
|
||
/-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
|
||
| owner
|
||
/-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
|
||
| admin
|
||
/-- 组织成员(`PINNED`):普通成员。 -/
|
||
| member
|
||
|
||
/-- 组织成员关系(`PINNED`)。 -/
|
||
structure OrganizationMembership where
|
||
/-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
|
||
user : I.UserId
|
||
/-- 组织(`PINNED`)。 -/
|
||
organization : I.OrganizationId
|
||
/-- 角色(`PINNED`)。 -/
|
||
role : OrganizationRole
|
||
|
||
/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
|
||
def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
|
||
actorRole = .owner
|
||
|
||
/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
|
||
def LastOwnerProtected
|
||
(target : OrganizationMembership I)
|
||
(otherOwnersInOrg : List I.UserId) : Prop :=
|
||
target.role ≠ .owner ∨
|
||
∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
|
||
|
||
end Spec.System
|