import Spec.Prelude /-! # Audit —— 审计日志(有意从简) likec4 把 `AuditLog` 列为实体:`AgentRun -> AuditLog 'records lifecycle events'`, admin 经控制台审计。但**审计记录里装什么**(事件 schema、保留策略、可查询维度) 在任何 ADR / 散文里都未决策,且大多是 plumbing——按分歧点测试**不入契约**:写明 与否不会让开发者与 agent 各做不同假设。 故本模块**刻意几乎为空**:只固定一条已决策的关系——审计以 run 为主体记录其生命 周期事件——其余 `OPEN`。这里留白本身是契约的一部分(承诺"此处尚无答案,勿填")。 -/ namespace Spec.System /-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4 `records lifecycle events`)。 只承诺"一条审计记录关联到某个 run"。事件类型、时间、actor、详情等字段**未定** (`OPEN`),待出现真实分歧点(如"取消必须记录 actor")时再由对应 ADR 落定。 -/ structure AuditEntry (I : Identifiers) where /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/ run : I.RunId end Spec.System