import Spec.Prelude

/-!
# Organization —— SaaS tenant root (ADR-0020, ADR-0024)

ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。

本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
writer authority 与 fail-closed resolver 由 ADR-0024 固定。
-/

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

/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
都不允许无关 org 共用 process-global provider 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 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 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

end Spec.System