← graph

formalize-daemon-planner-replay

Make daemon decisions replayable and formally conformant

Metadata

Statusdone
Agent identity6841f97a7a8e6cbc213051ce0ffb3c85c92c80cb61fd699428ab3fed6cb6ba94
Created2026-08-01T12:58:53.578124157+00:00
Started2026-08-03T10:20:58.572869127+00:00
Completed2026-08-03T11:55:58.692823862+00:00
Tokens631189 in / 2070 out

Description

Extend formal validation from the lifecycle reducer to the correctness-critical daemon decision loop without pretending to verify the operating system or external providers. Refactor the daemon around a small deterministic planner: persisted normalized control state + ordered observations/effect acknowledgements + logical time -> normalized next state + explicit idempotent effects. Process probes, PID topology, filesystem/Git/NFS operations, sockets, timers, Pi/provider calls, and signals remain adapters; their assumptions and evidence quality must be typed inputs, never hidden ambient reads inside the planner.

Add a durable, bounded, redacted decision trace and wg service replay <trace> that reproduces planner states/effects byte-for-byte offline. Production invariant violations must emit a minimal replay bundle before further mutation. Integrate the planner transition schema with formalize-lifecycle-finish-lean4 so Lean proves the safety/convergence properties of daemon choices while Rust conformance replays Lean fixtures. Do not formalize TUI rendering, model output, OS correctness, NFS correctness, or performance. Use runtime guards, fault injection, black-box smoke, and where applicable Loom for adapter/concurrency correctness.

Correctness-critical daemon scope: dispatch/admission and breaker accounting; attempt/process/worktree/session ownership; wrapper/native-child topology; waiting/message consumption; same-session continuation; finish/promotion/cleanup convergence; graph identity and cross-graph isolation; chat-create request reconciliation; archival hold/confirmation; service upgrade/restart migration. A daemon state with unfinished work must always expose exactly one of: runnable action, authenticated live owner, explicit external wait condition, or scheduled convergence action+deadline. “No blockers” with no forward action is an invariant violation.

Adopt a verification pyramid:

  1. Lean invariants and conditional liveness over the pure planner/reducer;
  2. exhaustive bounded enumeration of small state/trace spaces and property-generated traces;
  3. Rust/Lean normalized transition conformance;
  4. Loom/adapter tests for synchronization and CAS linearization where feasible;
  5. candidate-binary crash/fault-injection smokes for real filesystem/process/socket effects;
  6. production runtime invariant monitor + replay capture.

Seed permanent replay fixtures from actual incidents: exited wrapper rejected as stale then stuck NeedsFinalization; reopen before old owner release; park/resume overlap; obsolete daemon chat creation/lost response; target moved during finish; surprise archival backlog; .wg candidate replacement; dead Pi owner retaining session/worktree; abandoned dependency incorrectly satisfying readiness.

Validation

  • Replaying the same trace repeatedly yields identical normalized states/effects and no external side effects; trace schema is versioned and secrets/content are redacted by construction.
  • Every seeded incident reaches a named invariant violation under the historical rule and converges safely under the corrected rule.
  • Kill at each effect issue/ack persistence boundary, restart, and assert exactly-once logical effects (physical retries idempotent), no duplicate spawn/promotion/archive/chat, and no lost WIP.
  • Exhaustive bounded checks cover at least two tasks, two attempts, competing stale/current actors, crashes, reordered duplicate acknowledgements, and target movement.
  • Runtime monitor detects authenticated-live-owner/action/wait/deadline exhaustiveness and writes a usable replay bundle before fail-closed hold.
  • lake build without proof placeholders; Rust conformance/property/Loom tests; candidate-binary owned smoke; cargo fmt --check, cargo check, cargo clippy.

Depends on

Required by

✉ Messages 3 messages (3 unread)

  1. #1isolate-worker-control-plane-filesystem2026-08-02T06:30:43.467961221+00:00read
    Coordination: worker IPC request/effect schema planned as versioned capability tuple (graph_id/task/generation/attempt/fence/lease/agent), typed WorkerOperation and caller request_id. Capability validation and idempotent reply journal should become planner observations/effects rather than ambient filesystem reads when your task starts.
  2. #2isolate-worker-control-plane-filesystem2026-08-02T07:17:59.941053058+00:00delivered
    Final worker broker wire is `worksgood-worker-control-v1`, with attempt tuple validation before any effect and request journal states Pending/Completed(response). Same request_id+token digest+operation replays completed reply; Pending fails closed for reconciliation; conflicting tuple is rejected. This is the seam for future planner observation/effect formalization.
  3. #3formalize-daemon-planner-replay2026-08-02T14:37:34.688621756+00:00read
    Acknowledged worker-control coordination: the design will model broker capability validation and Pending/Completed idempotent request-journal results as typed observations/acknowledgements, never planner filesystem reads.

Log