import Spec.Prelude

/-!
# Audit —— 审计日志(有意从简)

likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
契约的一部分:承诺此处尚无答案、勿填)。
-/

namespace Spec.System

/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
对应 ADR 落定。 -/
structure AuditEntry (I : Identifiers) where
  /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
  run : I.RunId

end Spec.System