Work 控制面四层平面与形式化安全不变式 (C0 / W0 / O1 / E0)

Work 控制面四层平面与形式化安全不变式 (C0 / W0 / O1 / E0) 由 Archify 生成的工作流图。 01 / C0 命令 / W0 编排平面 EX / O1 尝试 / E0 效应平面 C0 准入与 W0 锁 O1 尝试与回执结算 E0 效应与终态 SingleCurrentWork & RevisionMonotonic OneSendPerAttempt & FallbackOnlyAfterProof C0 准入冻结 · bindAdmittedWork · C0 命令 / W0 编排平面 › SingleCurrentWork & RevisionMonotonic › C0 准入与 W0 锁 · 效应冻结 C0 准入冻结 bindAdmittedWork 效应冻结 W0 Root 行锁 · control_revision · C0 命令 / W0 编排平面 › SingleCurrentWork & RevisionMonotonic › C0 准入与 W0 锁 W0 Root 行锁 control_revision W0 匹配唤醒 · MatchingWait · C0 命令 / W0 编排平面 › SingleCurrentWork & RevisionMonotonic › O1 尝试与回执结算 W0 匹配唤醒 MatchingWait C0 显式 Stop · requestWorkStop · C0 命令 / W0 编排平面 › SingleCurrentWork & RevisionMonotonic › E0 效应与终态 C0 显式 Stop requestWorkStop W0 终态收口 · finishCarrier · C0 命令 / W0 编排平面 › SingleCurrentWork & RevisionMonotonic › E0 效应与终态 · 不可逆终态 W0 终态收口 finishCarrier 不可逆终态 O1 领取围栏 · attempt_token · O1 尝试 / E0 效应平面 › OneSendPerAttempt & FallbackOnlyAfterProof › C0 准入与 W0 锁 O1 领取围栏 attempt_token O1 单次派发 · admitAttempt · O1 尝试 / E0 效应平面 › OneSendPerAttempt & FallbackOnlyAfterProof › O1 尝试与回执结算 O1 单次派发 admitAttempt 未发出证明回退 · not_dispatched · O1 尝试 / E0 效应平面 › OneSendPerAttempt & FallbackOnlyAfterProof › O1 尝试与回执结算 未发出证明回退 not_dispatched E0 效应账本 · markExecuting · O1 尝试 / E0 效应平面 › OneSendPerAttempt & FallbackOnlyAfterProof › E0 效应与终态 · ActiveRun CAS E0 效应账本 markExecuting ActiveRun CAS rootRunId 挂起与恢复 检查停止意图 完成或取消 签发租约 CAS 写账本 证明未发出 OneSend NoWriteAfterStop 图例 Agent 逻辑 策略 上下文 / 追踪 云服务

C0 命令与 W0 编排不变式

  • • SingleCurrentWork：同一会话至多 1 个活跃前台 Work
  • • RevisionMonotonic：control_revision 严格单调递增
  • • ReplyRequiresMatchingWait：迟到或错绑定回执不唤醒

O1 尝试与回退证明不变式

  • • StaleWorkerCannotCommit：过期租约写被栅栏拒绝
  • • OneSendPerAttempt：单次尝试绝不重复下发请求
  • • FallbackOnlyAfterProof：仅未发出证明可触发回退

E0 外部效应与终态不变式

  • • CommittedWriteBlocksRerun：已提交外部写阻断重跑
  • • NoLateActivationAfterTerminal：终态后拒绝迟到激活
  • • NoWriteAfterStop：Stop 生效后禁止推进外部写入