/-!
# Prelude —— System 层共享标识符

平台层(`Spec.System`)反复引用一组**标识符**(项目、run、session、principal)。
它们在 likec4 / ADR 里只作为引用键出现,**内部表示从未被决策**(是 UUID 还是
复合键、principal 怎么分类),也不构成语义分歧点。

故把它们收口成一个 opaque 载体 `Identifiers`,System 各模块在其上参数化。这样
契约谈得了"锁的 owner 是哪个 run""grant 授给哪个 principal"这类**关系**,却
不对标识符的表示作任何承诺。
-/

namespace Spec.System

/--
System 层标识符载体(`OPEN` 表示,关系结构 `PINNED`)。

每个字段是一个 opaque 类型:契约只用它做引用键,绝不假设其内部表示。System 各
模块 `variable (I : Identifiers)` 后即可引用 `I.ProjectId` 等。
-/
structure Identifiers where
  /-- 课程项目的标识(`OPEN` 表示;聚合根,见 likec4 `Project`)。 -/
  ProjectId : Type
  /-- 一次 Claude 处理任务的标识(`OPEN` 表示;锁的 owner、审计主体,见 `AgentRun`)。 -/
  RunId : Type
  /-- 长生命周期 Claude 会话的标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/
  SessionId : Type
  /--
  权限主体的标识(`OPEN` 表示及其**子类型学**)。

  ADR-0004 列出 principal 可以是 user / feishu_chat / department / user_group /
  app。这套子类型学本身**未定且非本层分歧点**(纯 plumbing),故此处只留 opaque
  键,不展开为 `inductive`。
  -/
  Principal : Type

end Spec.System