carlos / platform Public

zdd plan 3: Astra final review r1 (ACCEPT WITH FIXES)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

claude 2 weeks ago a6ba2a095ad7935bcb0fcd12d17c74d50c9c492e parent 5b9055b

1 file changed, +224 −0

docs/superpowers/plans/CODEX-FINDINGS-ZDD-IMPL-3.md +224 −0

diff --git a/docs/superpowers/plans/CODEX-FINDINGS-ZDD-IMPL-3.md b/docs/superpowers/plans/CODEX-FINDINGS-ZDD-IMPL-3.md

new file mode 100644

index 000000000..8d9a73fa5

--- /dev/null

+++ b/docs/superpowers/plans/CODEX-FINDINGS-ZDD-IMPL-3.md

@@ -0,0 +1,224 @@

+**ACCEPT WITH FIXES**

+Reviewed `f36718c5..5992477a` read-only. I did not run builds, tests, or mutants; the execution ledger’s reported passes were not independently reproduced.

+The specified P2-13 contained-start paths appear closed, including handleless starts and failed flat/nested cleanup. The retained-wake Shutdown fix and the flag-off live-leader retention exception are sound. Switch/barrier ordering and pinned-entry installation also look correct. The findings below prevent unconditional acceptance.

+**Findings affecting the dormant branch**

+1. **High — Worker ownership is checked before preparation, not at exec. Fix before merge.**

+ [activator.go:2423](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/activator.go:2423), `workerbuild.go:77`.

+ A respawn passes `ownedLocked`, then stalls in config admission, materialization, or generations-file publication. Its lease fails during that interval. The sweep skips `workerRespawning` entries before checking replication health; the before-exec hook only publishes the build; the final installation checks entry/state/shutdown but not ownership. The replacement can therefore execute and be installed after ownership has been lost.

+ Compose a fresh ownership/context check into the existing before-exec hook, after publication, and recheck ownership before installation. Test lease loss while preparation is deliberately blocked. The current test loses ownership before the initial check and misses this sequence.

+2. **Medium — The simulation can report a false process-after-release violation. Fix before merge.**

+ [swap_sim_test.go:423](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/swap_sim_test.go:423).

+ `die` publishes `p.dead=true`, releases `p.mu`, and only afterward removes the process from `w.running`. A concurrent reaper can observe `Exited()==true`, legitimately release the lease, and have `leaseFreed` report that the same process still runs. Concurrent calls to `die` can expose the same inconsistency.

+ Make process death and removal from the invariant model one atomic transition under consistent locking. Add a controlled death/release interleaving. This is a possible wrong-reason mutant kill; I am not claiming that a recorded run encountered it.

+3. **Medium — A mutation run can pass despite another required run crashing or never running. Fix before merge.**

+ [mutate.sh:164](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/testdata/swapsim/mutate.sh:164).

+ If the sweep reports an invariant violation but the designated witness panics, `CAUGHT` wins before the script examines `crash`. The reverse combination also passes. A `NOT RUN` result likewise does not independently fail the gate when another result supplies a kill.

+ Record execution integrity separately from mutation detection. Panic, timeout, missing execution, and build/setup failure must fail the gate even when another run catches the mutation. Preserve the successful kill as diagnostic evidence.

+4. **Low — Mutation scratch cleanup can delete another run’s files. Fix before merge.**

+ [mutate.sh:54](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/testdata/swapsim/mutate.sh:54).

+ Every invocation uses `$TMPDIR/zdd3-mut` and starts with `rm -rf`. Two runs sharing `TMPDIR` cause the second to delete the first’s tree and logs. This also violates the supplied rule against deleting scratch owned by another session.

+ Allocate a unique directory with `mktemp -d` beneath `$TMPDIR`, and clean only that invocation’s files.

+5. **Low — New generation error detail reaches member events; an added string contains an em dash. Fix before merge.**

+ [backend_exec.go:1282](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/backend_exec.go:1282), `logsink.go:50`, `activator.go:2450`.

+ A contained flat wake fails health, its generation kill fails, and the new `errGenUnproven` detail passes through `memberSafeWakeReason` into the member event. Mapping `errWakeUnproven` does not cover that first failure. This can occur with `a.gens=false` and containment enabled.

+ Map the unproven-start sentinels to existing reviewed wording and keep generation diagnostics in operator logs. Remove the em dash from the added worker-proof log and avoid asserting that a process necessarily remains: missing delegation can also explain failed proof.

+6. **High — Flag-off failed-wake retention still proves only the leader’s exit. Defer as an explicit pre-existing limitation.**

+ [opset.go:247](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/opset.go:247), `opset.go:456`.

+ A flat process forks a descendant, then a failed/fenced wake is retained because its leader survives Stop. Later the leader exits. With no generation containment, the proof accepts the missing generation kill or `errNoGenContainment` and releases the lease while the descendant can remain alive.

+ The live-leader fix improves main and should remain. It does not establish a flag-off process-tree guarantee. Track a separate fix that retains the handle and proves the host cgroup empty on terminal failed-wake cleanup. The simulation currently does not model flag-off descendants, so its passes cannot close this limitation.

+**Findings latent until the flag is on**

+7. **High — A pinned wake never checks the lease it actually acquired. Fix before merge.**

+ [swapadmit.go:88](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/swapadmit.go:88), `swaphold.go:243`, `backend_exec.go:615`.

+ A hold stops the incumbent and acquires its new lease. Renewal then fails during Restore or subsequent preparation. `pinCheck` calls `ownedLocked(..., true)`, which deliberately skips `e.rep`; the local `Lease` exposes no ownership check, although its underlying `lease.Held` has one. Context and fence checks do not establish lease ownership. The staged process can execute before Replicate discovers the failure.

+ Expose the wake-held lease’s liveness and check it at the actual execution boundary. Carry the attempt/revision/fence check through preparation to that boundary too. Classify refusal as NoOwnership/abandonment. This inherits a cold-wake weakness, but the new pinned path expressly promises this check.

+8. **High — Retiring schedule writes have a check/use race. Fix before merge.**

+ [control.go:84](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/schedule/control.go:84), `control.go:148`, `control.go:161`.

+ The old generation starts a PUT and passes `retired()`, then stalls while sending its body. The switch happens; the successor writes the same timer. The old request resumes and overwrites it after retirement. DELETE has the equivalent race between its check and mutation.

+ Serialize the final retirement decision and mutation against the switch with a dedicated write fence; parse request bodies outside it. Keep retirement latched for outstanding handlers after the member leaves the operation set. A second unsynchronized boolean check is insufficient. Cover both flat and nested control listeners.

+9. **High — The closed claims launcher is not refused unconditionally before destructive hold work. Fix before merge.**

+ [swaphold.go:82](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/swaphold.go:82), `swap.go:336`.

+ Set `ClaimRuntime.Generations` and `Pins` true. The guard passes, a hold stops its incumbent, and the permanently closed launcher then refuses the replacement. An overlap likewise reaches the parent raise before refusal. The existing overlap test explicitly permits that raise.

+ On this base, refuse claims-backed swaps before raise/stop regardless of those two booleans. Open that guard only alongside a working isolated launcher and its required lifecycle. Deferring the launcher is reasonable; deferring this guard contradicts the reduced-scope ruling’s “every claims-on swap” guarantee.

+10. **Medium — `pinExec` records entry into StartStaged, not execution. Fix before merge.**

+ [swaphold.go:328](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/swaphold.go:328), `swaphold.go:186`.

+ `pinExec` becomes true before `StartStaged`. A subsequent socket-directory, token, placement, or `cmd.Start` failure returns no process, but `holdResult` reports `SwapDown`. Plan 5 can halt a cohort and hold down a build that never executed.

+ Record execution evidence from the spawn result: a returned process or an unproven-start sentinel. Preserve that evidence on the failed wake before cleanup. Merely checking `hw.next.proc` afterward is insufficient because failed wakes do not install their process there. Test both an ordinary pre-exec failure and a post-exec health failure.

+11. **Medium — Parent-limit repair obligations are discarded on errors. Fix before merge.**

+ [swap.go:408](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/swap.go:408), `opset.go:289`.

+ Two sequences fail:

+ - `RaiseGenParent` writes `memory.max` successfully, then a later cgroup write fails. `raised` is still false, so member cleanup never restores the parent.

+ - The raise succeeds and the last child is proven stopped, but `RestoreGenParent` fails. `leaveSet` logs the error, clears `raised`, and removes the last member, leaving no retry obligation.

+ Mark the parent potentially changed before invoking the raise. Retain and retry failed restoration outside `a.mu`; do not clear the repair state on failure. Test partial raise and transient restore failure separately.

+12. **High — Retained worker processes lose their published build pin. Fix before merge.**

+ [activator.go:1303](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/zdd-3-swap/internal/activator/activator.go:1303), `activator.go:2459`, `generations_file.go:100`.

+ A worker starts and publishes its identity, then its wake fails. Cleanup retains it because termination cannot be proven. `wake` deletes its entry and republishes the generations file, whose snapshot includes entries and pending builds but not `unprovenWakes`. The retained worker’s build disappears from root’s pin set.

+ The shed-respawn path has the same problem: `dropMember` can retain the process, but the caller still drops its pending build pin. Once the live link moves, root can sweep or restage bytes still referenced by that retained process.

+ Transfer the complete staged identity and pin to the retained owner, and remove it only after termination proof. Extend the existing serialized generations writer. This is an integration defect in the already-implemented worker contract, separate from plan 5’s acknowledged instance-pin work.

+**Rulings**

+Line numbers below refer to the [controller ledger](/home/paulca/.cache/zdd-impl/plan3/ledger.md).

+| Line | Judgment |

+|---|---|

+| 46 | **Agree.** Building on plan 2 was appropriate; the required rebase has happened. |

+| 47 | **Disagree.** The supplied machine rules explicitly require the default Go cache and prohibit a fresh task cache; they supersede this earlier cache ruling. |

+| 48, P2-7 | **Agree.** Preserving the third return value, strict gate, settlement, and failure cleanup is necessary. |

+| 49, P2-8 | **Agree.** Strict admission refusals are NoOwnership, not build failures. |

+| 50 | **Agree.** Moving `Gen.Worker` earlier resolves a declaration-order defect. |

+| 51 | **Agree.** Moving `errSwapStopped` earlier likewise changes no contract. |

+| 52, P2-13 | **Agree.** The specified contained and handleless retention paths now preserve the lease until proof; finding 6 is the broader flag-off limitation. |

+| 53 | **Agree as amended by line 78.** Correcting the plan’s cleanup defects is appropriate; retrying a spent lease handle is not. |

+| 54 | **Agree.** Claims-backed successors must never fall through to legacy StartStaged. |

+| 55 | **Agree.** Central classification of unavailable isolation and root staged-path refusal is correct. |

+| 56, P2-9 | **Agree with reduced scope; disagree that its refusal guarantee is implemented.** The closed launcher justifies deferring strict-parent work, but finding 9 remains. |

+| 57 | **Agree.** Valid production-shaped claim fixtures are appropriate. |

+| 58 | **Agree with the rule; implementation incomplete.** Unsupported holds must refuse before stopping, including the both-capabilities-true claims case. |

+| 59 | **Agree.** Installing the pinned entry before waking stop waiters preserves the required ordering. |

+| 60 | **Agree.** `t.TempDir` fixtures are appropriate with disk-backed `TMPDIR`. |

+| 61 | **Agree.** Refusing sidecar execution without ownership is a justified flag-off safety exception. |

+| 62 | **Agree.** The root/nested adaptations preserve validation and protocol behavior; the real-unit checks remain owed. |

+| 63 | **Agree.** Copy review can remain a controller-owned pre-merge gate; its pending status is not itself a finding here. |

+| 64 | **Agree on the worker adaptation.** The new diagnostic still needs the correction in finding 5. |

+| 65 | **Agree on the CPU budget and ninth mutant.** Use the current default-cache rule and fix mutation-run isolation. |

+| 66 | **Agree.** Gate, push, description, and CI belong to the controller after fixes. |

+| 67 | **Agree.** Channel-controlled negative assertions are preferable; the remaining sleep-based cases are triaged below. |

+| 78 | **Agree.** Once process termination is proven, retrying an already-spent release handle cannot improve safety and can permanently block the host. |

+| 80 | **Agree.** A bounded detached release context is a justified dormancy exception. |

+| 81 | **Agree.** A placed flat generation requires child-cgroup proof after failed health; it is not enough to stop its leader. |

+| 82 | **Agree, but incomplete.** Mapping retained-wake refusal is correct; first-failure sentinel text still escapes in finding 5. |

+| 89 | **Agree under the no-new-copy constraint.** Reusing the fence reason is acceptable, though it is not evidence of an actual maintenance fence. |

+| 101 | **Agree.** These refusals must also forbid restoration, so NoOwnership is the right verdict. |

+| 116 | **Agree with the execution-based rule; disagree with “reached StartStaged” as its implementation.** Finding 10. |

+| 117 | **Agree.** Stale/refused pinned attempts should not create new member failure text. |

+| 128 | **Agree as a plan-5 obligation, not a completed fix.** Every planned cold wake must capture its staged identity before arming swaps. |

+| 151 | **Agree.** Keeping typed classification while stripping its wrapper from member text preserves the intended boundary. |

+| 160 | **Agree.** Missing delegation must fail closed; plan 5 must refuse to arm the feature there. |

+| 169 | **Agree.** The restart witness needs a process that outlives cancellation to test the join. |

+| 176 | **Agree.** Reviewing the rebased branch against merged plans 1/2/4 is necessary and was done. |

+| 179 | **Agree.** Unproven termination belongs in the simulation; fix its inconsistent death transition before relying on its evidence. |

+| 180 | **Agree with the ruling; implementation incomplete.** Findings 2–3 undermine the promised distinction between assertion kills and broken runs. |

+| 182 | **Agree with the Shutdown fix.** Its “flag-off unaffected” explanation became false after line 185 and must be updated. |

+| 183 | **Agree.** The generations-on proof backstop makes the isolated ErrStillRunning mutation redundant there; flag-off coverage is the useful witness. |

+| 185 | **Agree.** Retaining a live failed-wake leader is a justified production safety correction; document the resulting flag-off Shutdown wait and the descendant limitation. |

+**Cross-plan consequences**

+- **Plan 5 must consume execution-bound ownership checks**, including the locally held wake lease. Publication hooks must compose with these checks rather than replace them.

+- **Keep one generations-file writer.** Fix retained worker ownership now; extend that same writer to current, spawning, retiring, and retained instance generations before arming swaps.

+- **Capture staged identity for all planned cold wakes and sidecar restarts.** The current live-link fallback remains an explicit pre-arming obligation.

+- **Implement failure recording and held-down admission before another request can wake the live link.** Account for slow hold withdrawal, and do not treat a zero result `Gen` as the failed attempt’s identity.

+- **Wrap hostguard pre-body refusals before classification.** Do not publish `SwapResult.Reason` directly as member text.

+- **Keep claims launch closed until its complete lifecycle lands:** journaled parent ownership, failed-close retention/retry, fallback re-Prepare, and fresh generation identity on retries. Capability booleans alone must not open admission.

+- **Update the index/ledger** with retained-worker pin ownership, parent-repair retry ownership, the execution-evidence contract, and the expanded flag-off Shutdown exception.

+Root validation correctly derives the app from the registry row, rejects symlink traversal, checks the digest and regular-file shape, and refuses before root performs start-side mutations. The validate-then-bind residual remains acceptable only under the stated immutable, root-controlled path assumptions and complete build pinning.

+After these fixes, rerun the corrected simulation and mutation gate. Static inspection found appropriate designated witness targets for M1–M9; it does not establish that the recorded kills were uncontaminated by findings 2–3. The simulation also does not replace worker, sidecar, claims, or schedule-specific witnesses.

+**Deferred-minor triage**

+“Defer to plan 5” below means **required before that plan enables the feature**.

+| Ledger item | Disposition |

+|---|---|

+| T1: staged spawn skips LiveVersion/PurgeHost tests | **Defer.** Add path-specific coverage; do not assert the flat implementation’s guards describe the nested path identically. |

+| T1: GenSwitched stale-real-socket and failure cases | **Defer.** Useful coverage; no additional failing sequence established. |

+| T1: tier ignored without containment | **Defer to arming validation.** Require the containment/delegation prerequisites. |

+| T2: non-worker nil-proc `genTerminated` shortcut | **Defer.** Actual handleless unproven paths use the dedicated proof; preserve that separation. |

+| T2: barrier’s 50 ms negative | **Fix before merge.** Use the existing positive stop-entry signal. |

+| T2: Shutdown waits waking entries before pending-stop polling | **Defer.** Delay, not premature release. |

+| T2: dropped `claimProcess.provenStopped` Stop error | **Defer.** Improve operator diagnostics. |

+| T2: repeated N==0 retained-wake log | **Defer.** Rate-limit without weakening retention. |

+| T2: extra flag-off nested Stop | **Defer; accepted behavior.** It supplies proof after the backend returns an unproven unit. |

+| T2: `errGenUnproven` member text | **Fix before merge.** Finding 5. |

+| T3: replaced-entry, nil-rep, member-current, nil-work coverage | **Defer.** No additional implementation defect established. |

+| T3: `errSwapStopped` classified Proceed | **Resolved.** It now maps to NoOwnership. |

+| T4: partial parent raise | **Fix before merge.** Finding 11, including failed restoration. |

+| T4: raw hostguard pre-body errors | **Defer to plan 5.** Wrap admission errors before classification. |

+| T4: post-switch work error only logged; missing test | **Defer.** A completed switch should stand; add the witness. |

+| T5: sleep triggers in settle tests | **Fix before merge.** Replace available sleep triggers with controlled events. |

+| T5: missing successor-stop/restore/lease assertions and 10-second constant test | **Defer.** Strengthen behavior coverage; the constant itself is correct. |

+| T5: no nil-Proc guard in `observeSettle` | **Defer.** Production successful-start contracts supply a process; future reuse must preserve that contract. |

+| T6: slow successful stop withdraws hold | **Defer to plan 5.** Retry/backoff must avoid repeated stop cycles. |

+| T6: weak claims capability table | **Fix before merge.** Test every flag combination refusing before side effects; finding 9. |

+| T6: missing LayoutConflict row | **Defer.** Add admission coverage. |

+| T6: RF3 50 ms sleep | **Fix before merge.** Use controlled ordering. |

+| T6: failed pinned wake returns zero Gen | **Defer to plan 5.** Use the attempt identity for failure records; do not infer it from zero Gen. |

+| T6: next request wakes live link after SwapDown | **Defer to plan 5.** Held-down admission must precede reopening requests. |

+| T6: early `pinExec` | **Fix before merge.** Finding 10. |

+| T6: pin check precedes preparation/exec | **Fix before merge.** Carry the check to the execution boundary; finding 7. |

+| T7: cold wake lacks staged path for sidecar | **Defer to plan 5.** Capture it before enabling swaps. |

+| T7: KillSidecar does not remove empty role-sidecar cgroup | **Defer.** Bounded empty-directory cleanup. |

+| T7: sticky `sidecarUncertain`, outcome computed before join | **Defer.** Conservative availability behavior, not premature proof. |

+| T7: nested staged sidecar refusal until Task 9 | **Resolved for staged handles.** Cold missing-path handling remains plan 5’s obligation. |

+| T7: stale sweep-retry comment | **Defer.** Correct with nearby maintenance. |

+| T7: bounded negative in sidecar-join test | **Fix before merge.** Tie it to the available lifecycle signal. |

+| T7: KillSidecar proof arm lacks real-cgroup coverage | **Defer to pre-arming dev verification.** |

+| T8: nested control gate untested | **Fix before merge.** Include the nested route in finding 8’s tests. |

+| T9: validate-then-bind residual; optional ownership/mode checks | **Defer hardening.** Immutable root-controlled paths and complete pins remain prerequisites. |

+| T9: ErrStagedExe leaves launch JSON containing environment | **Fix before merge.** Remove the caller-created launch file after a definite pre-start refusal. |

+| T9: stale generation-backend comments | **Defer.** Documentation correction. |

+| T9: HostApp ignores CARLOS_DATA_DIR | **Resolved in the reviewed server wiring.** |

+| T9: OptDir ignores CARLOS_OPT_DIR | **Defer to pre-arming configuration support.** Nondefault paths currently fail closed. |

+| T10: both capability flags allow stopping before closed-launch refusal | **Fix before merge.** Finding 9. |

+| T10: zero Tier, worker generation shape, empty socket producing `.control` | **Defer until isolated launch opens.** Correct all before making these paths executable. |

+| T10: HealthBy caps every retry; reused generation number | **Defer until isolated launch opens.** Specify retry semantics and allocate distinct generation identities. |

+| T10: refusal test does not assert Read was never called | **Defer.** Strengthen the closed-launch witness. |

+| T10: diagnostic Reason might reach members | **Defer to plan 5/6 rendering.** Never display it verbatim. |

+| T11: em dash, overstated proof diagnosis, discarded ownership reason | **Fix before merge.** Preserve the actual refusal reason; findings 1 and 5. |

+| T11: respawn wait bound shorter than worst-case respawn; stale comments | **Defer.** The operation join preserves safety; clarify the timing contract. |

+| T11: unread kill counter, missing heal control, sleep negative | **Fix before merge.** Tie refusal to failed proof and demonstrate recovery after proof succeeds. |

+| T11: missing generations-on shed-path test | **Fix before merge.** Include retained build-pin assertions; finding 12. |

+| T12: 200 ms negative | **Defer.** Retain the positive ordering evidence; improve synchronization when revisiting the fixture. |

+| T12: #231 only indirectly exercised | **Resolved sufficiently.** The reviewed restart witness checks the replacement spawn count. |

+| T12: socket-bind skips | **Defer to a capable test environment.** A skipped witness cannot count as verification there. |

+| T12: `a2` left running | **Defer.** Clean up the fake service fixture; no production process is established by it. |

+| T13: stale Shutdown comment and missing flag-off exception record | **Fix before merge.** Record the bounded flag-off wait. |

+| T13: P2 witness lacks next-wake refusal assertion | **Defer.** Add the assertion; the separate retained-wake witness covers that contract. |

+| T13: P1 witness’s 300 ms budget | **Defer.** Replace timing dependence when strengthening the fixture. |

+| T13: flag-off descendants remain unproven | **Defer explicitly as pre-existing.** Finding 6; do not describe the live-leader fix as full process-tree closure. |

+The pending copy review, two real-control-unit checks, and pre-existing Windows vet failure remain exactly the known items in the brief; none is counted as a new finding.

\ No newline at end of file