← graph

design-atomic-graph-work-save

Design atomic GraphSave and WorkSave protocol

Metadata

Statusdone
Agent identity603daf069cd2ae4a26357aa66e8c6124154b648711a0816ffd8b660ee3b23815
Created2026-08-02T15:13:34.086245311+00:00
Started2026-08-03T09:56:28.024816163+00:00
Completed2026-08-03T10:07:57.855255874+00:00
Tagslifecycle, design, graphsave, worksave
Tokens18826786 in / 45812 out

Description

Design the complete GraphSave + WorkSave protocol that makes WG task completion truthful, durable, crash-replayable, and dependency-safe. This is a design/audit task, not the implementation task. It may run in parallel with the currently active formalize-lifecycle-finish-lean4 finalization, but MUST NOT edit that worktree, its branch, or correctness-critical runtime code. Inspect the preserved branch wg/agent-956/formalize-lifecycle-finish-lean4 at 9774eed0 read-only via Git, and treat the current self-hosting incidents as primary evidence.

Incidents to explain precisely:

  • formalize-lifecycle-finish-lean4 became graph done while finalization remained RepairNeeded, its candidate was stale, and no merge/promotion/cleanup receipt existed.
  • That false done made formalize-daemon-planner-replay dependency-satisfied and allowed dispatch.
  • brokered DoneHandoff lost authenticated worktree context, so terminal state could be recorded without checkpointing/promoting retained work; 9774eed0 is a narrow repair, not assumed complete.
  • reset/reopen retained the branch/worktree but launched a new session rather than proving exact-session continuation.
  • after the prematurely dispatched planner worker exited, its graph state remained in-progress despite a dead process and clean worktree.

Produce docs/design-atomic-graph-work-save.md containing:

  1. A single normative invariant: dependency-satisfying Done iff the exact attempt's durable WorkSave receipt, accepted immutable candidate, required validation/FLIP receipt, task-owned Land/Deliver/Report receipt, exact promotion/output receipt, and cleanup commit all exist and agree on task/generation/attempt/fence/candidate/base.
  2. An authoritative state machine / write-ahead SaveTransaction with explicit phases, allowed transitions, idempotency keys, CAS/revision rules, and fail-closed behavior. Graph status must be a projection of evidence, not independent mutable authority.
  3. Exact authority rules for worker, broker, daemon convergence, evaluator, promoter, cleanup, operator reset/retry, and dependency readers.
  4. A complete mutation/read inventory across commands and service code: every path that writes terminal status, changes generation/attempt ownership, captures or deletes worktrees, creates candidates, promotes output, satisfies dependencies, archives, resets, retries, or migrates old records.
  5. Crash cuts and replay actions after every durable boundary, including lost IPC responses and daemon/binary skew.
  6. Legacy migration/quarantine: old Done records lacking evidence must become non-dependency-satisfying NeedsReconciliation, never silently blessed or erased.
  7. A phased implementation DAG with explicit file ownership so independent adapter tasks can fan out after a shared kernel lands. Separate kernel/schema, WorkSave capture, terminal command adapters, daemon convergence, dependency/archive/reset readers, migration, formal/Rust traces, adversarial smokes, and final synthesis/canary.
  8. Rollout, compatibility/versioning, rollback, observability, and operator repair commands.
  9. A traceability matrix mapping each invariant to runtime guard, pure reducer rule, Lean theorem, Rust conformance trace, fault-injection test, and smoke scenario.

Also produce docs/plans/atomic-graph-work-save-dag.json as a machine-readable proposed task DAG. It must name each bounded task, dependencies, owned files/modules, non-goals, and validation commands. Do not create or dispatch the implementation tasks yet; the chat/operator will review the design first.

Non-goals: no filesystem/XDG sandbox project, provider work, broad TUI redesign, historical worktree cleanup, or rewriting the completed Lean program. Do not claim Lean verifies OS/Git/storage adapters; state environmental assumptions explicitly.

Validation

  • docs/design-atomic-graph-work-save.md and docs/plans/atomic-graph-work-save-dag.json exist and agree.
  • The mutation/read inventory names concrete functions/files and is checked against repository-wide searches; include the search commands used.
  • The DAG has one shared kernel gate before parallel runtime adapters and one final synthesis/canary gate after them; no two parallel tasks own the same correctness-critical files.
  • The design includes executable acceptance traces for false-Done dependency dispatch, brokered lost-worktree handoff, crash at every transaction phase, dead-worker convergence, target movement, reset/retry, lost response, and legacy Done migration.
  • The design explains why 9774eed0 is necessary but insufficient.
  • No production Rust, Lean source, existing fixtures, graph state, or other agent worktree is modified by this task.
  • python3 -m json.tool docs/plans/atomic-graph-work-save-dag.json >/dev/null passes.

Depends on

Required by

Log