Isolated exec spec: revision 8 after codex round 7
Round 7 findings committed unedited. All accepted: the startup sweep becomes POST /sweep in the control service, keyed on the unit names systemd reports; the downgrade guard checks every row's path shape regardless of flags; unflagging a nested row is refused.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+77
−18
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+43 −18docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R7.md+34 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md| index d7fc0d083..bde92df89 100644 |
| --- a/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| +++ b/docs/superpowers/specs/2026-09-11-isolated-exec-design.md |
| @@ -1,7 +1,7 @@ |
| # Isolated exec — every exec-backed instance in its own namespace |
| -**Date:** 2026-09-11 · **Status:** revision 7, after codex rounds 1 to 6 |
| -(19 + 14 + 7 + 4 + 3 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 8, after codex rounds 1 to 7 |
| +(19 + 14 + 7 + 4 + 3 + 1 + 1 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -848,6 +848,7 @@ itself: |
| | `POST /seed?host=H&memory_max=N` | the same `set-property`; `systemctl start` on `carlos-instance-seed@<esc>.service` (blocking: a oneshot's start job completes when `ExecStart` exits, or fails at `TimeoutStartSec`); the unit is now `active (exited)` or `failed` and **stays loaded** (`RemainAfterExit=yes`, §4.2); `systemctl show -p InvocationID,Result,ExecMainStatus,ExecMainCode`; wait for the cgroup to be empty (§6.5's rule, applied by the service as root); `systemctl stop` (instant for an exited oneshot; clears it) | 200 with `{invocation_id, result, status, code}`, always complete | 150s: 120s seed budget plus `TimeoutStopSec` and slack (R3-5) | |
| | `POST /stop?host=H&role=run\|seed\|sidecar` | `systemctl stop <unit>` (blocking; also cancels a pending start job) | 204 | 30s | |
| | `POST /reset?host=H&role=…` | `systemctl reset-failed <unit>`, tolerating "not loaded" | 204 | 30s | |
| +| `POST /sweep` | `systemctl list-units --all` and `list-jobs` over the three templates' instances; `systemctl stop` each that is not `inactive` or has a job; wait for terminal state and empty cgroup on each | 200 with the list of unit names swept, or 502 naming the unit that would not terminate | 60s | |
| | `GET /ready` | nothing | 204 once the probe verdict (§8.5) is `ready`; 503 with the verdict otherwise | 5s | |
| There is deliberately **no `reset-failed` inside `/start`**: `ResetFailedUnit` |
| @@ -1241,13 +1242,17 @@ half of that for a `systemctl restart carlos-edge` and does not propagate |
| the start. For a crash, or a stop that did not propagate, the agent on |
| start, before anything else: |
| -1. `systemctl list-units --all --plain --no-legend 'carlos-instance*@*' 'carlos-instances-*.slice'` |
| - and `systemctl list-jobs` (both unprivileged); |
| -2. `POST /stop` for every unit that is not `inactive`, whatever its |
| - role, and for every unit with a pending or running job (`stop` cancels |
| - a queued start); |
| -3. wait for each to reach a terminal state **and** for its cgroup to be |
| - empty (§6.5's rule), then remove stale exit records. |
| +1. `POST /sweep` (§5.3). The control service, as root, enumerates every |
| + `carlos-instance@*`, `carlos-instance-seed@*` and |
| + `carlos-instance-sidecar@*` unit and every pending or running job on |
| + them, `systemctl stop`s each (which also cancels a queued start), |
| + waits for each to reach a terminal state **and** for its cgroup to be |
| + empty (§6.5's rule), and returns the list. The sweep is keyed on the |
| + unit names systemd reports, not on hosts, so it covers a unit whose |
| + identifier is hashed and whose registry row is gone: the agent could |
| + not name such a unit through `/stop`, which takes a host (codex |
| + R7-1). |
| +2. The agent removes stale exit records under every run directory. |
| Every instance is therefore asleep, and no job is queued, when the |
| activator's state machine begins, which is the invariant the activator |
| @@ -1491,14 +1496,26 @@ mount would hide. So: |
| - **This release's `carlos system apply` refuses to install a candidate |
| that predates the layout** (its version is below the release that |
| - carries the mount units) unless reversal is **complete**: no |
| - activator-managed row is `nested`, `fenced` or `conflict`, and no |
| - journal exists. `layout_mode` is not consulted, because it records |
| + carries the mount units) unless reversal is **complete**: **no row on |
| + the box, whatever its flags**, has a `DBPath` or `Socket` under |
| + `/data/instances` or `/run/carlos/instances`, no row is `fenced` or |
| + `conflict`, and no journal exists. The check is by path shape and not |
| + by activator eligibility, because a row can leave management while |
| + keeping nested paths: `SetHibernate(false)` (`registry.go:1565`), |
| + including when the reconciler applies a record's flag |
| + (`reconcile.go:828`), does not touch them (codex R7 disposition of |
| + R5-2). `layout_mode` is not consulted either, because it records |
| intent, and a revert refused at quiescence or at the destination check |
| - leaves a nested row under a flat intent (codex R5-2 disposition). The |
| - reason names the rows; the installer is this binary for every |
| - downgrade from here, because a downgrade is an install performed by |
| - the installed binary (§8.1). |
| + leaves a nested row under a flat intent. The reason names the rows; |
| + the installer is this binary for every downgrade from here, because a |
| + downgrade is an install performed by the installed binary (§8.1). |
| +- **Unflagging a nested row is refused.** `carlos route --hibernate=false` |
| + and the reconciler's flag application both refuse to clear `Hibernate` |
| + on a row whose paths are nested, with `layout revert first` as the |
| + reason (the reconciler logs it as it logs shape drift, |
| + `reconcile.go:873-881`), so a nested row is always activator-managed |
| + and the revert pass can always quiesce it. The classification table |
| + (§8.1) therefore never meets a nested row it cannot own. |
| - **The console's rollback door** (`system.go:466`) refuses a channel |
| rollback to a pre-layout release while any box in the fleet reports |
| any `nested`, `fenced` or `conflict` row, or no layout field at all, |
| @@ -1718,8 +1735,11 @@ Unit level, all runnable in CI (no systemd needed): |
| escape function against `systemd-escape` fixtures, and the socket |
| address preflight: a host that fits today's flat paths but whose |
| identifier-keyed paths would exceed 107 bytes cannot exist, pinned by |
| - computing the longest address for a 253-byte host; two hosts colliding |
| - in `InstanceID` classify as `foreign`. |
| + computing the longest address for a 253-byte host; a short host and a |
| + hashed identifier can never be equal (the `_` prefix); two long hosts |
| + colliding in `InstanceID` classify as `conflict` and refuse to wake, |
| + including a host that was already `nested` when the second row |
| + arrived. |
| - `instancefs`: refuses a symlink at every component, refuses `..`, |
| `O_EXCL` temp plus rename, the mountinfo check for all three mounts. |
| - `internal/edge` and `internal/activator` dials, with real socket |
| @@ -1975,3 +1995,8 @@ rollback runs the old binary). |
| R6-1 hashed identifiers carry a `_` prefix no host can have, 64-bit hash; a collision is `conflict`, which refuses to wake and is never the unisolated fallback; the create door refuses a colliding host (§3.1, §8.1); |
| R5-2 the downgrade guards require completed reversal (no `nested`, `fenced` or `conflict` row, no journal), not intent (§8.2); |
| R5-3 the control service builds unit and slice names from `InstanceID(host)` (§5.3). |
| +- **Round 7** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R7.md`, 1 new |
| + finding plus 1 partial, verdict request changes). All accepted: |
| + R7-1 the startup sweep is `POST /sweep`, performed by the control service on the unit names systemd reports, so a hashed identifier without a row is still stopped (§5.3, §6.7); |
| + R5-2 the downgrade guard checks every row's path shape regardless of flags; unflagging a nested row is refused (§8.2); |
| + §10 aligned with the `conflict` rule. |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R7.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R7.md| new file mode 100644 |
| index 000000000..23452e4c3 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R7.md |
| @@ -0,0 +1,34 @@ |
| +| Prior finding | Disposition at `c2d52695` | |
| +|---|---| |
| +| R6-1 | **Resolved at spec level.** Identifier domains are separate; collisions refuse execution as `conflict`. Align §10’s stale `foreign` expectation with that rule. | |
| +| R5-2 | **Partially resolved.** Completed reversal replaces intent checking, but the guard excludes rows that cease to be activator-managed. [`SetHibernate(false)` preserves nested paths](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/registry/registry.go:1565), including when [provisioning invokes it](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/provision/reconcile.go:828). [§8.2 then classifies the row as `external` and skips reversal](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1374), while [the downgrade guard checks only activator-managed rows](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1492). Mount removal can therefore invalidate a still-used nested path. Check mount dependence across **all rows**, regardless of current hibernation eligibility; retain a reversal or refusal requirement for formerly migrated rows. | |
| +| R5-3 | **Resolved.** The control service constructs both unit and slice names from `InstanceID(host)` (§5.3). | |
| +| R2-4 | **Resolved.** Blocking seed execution and `RemainAfterExit=yes` retain identity and results through capture (§§4.2, 5.3, 6.5). [systemd service semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.service.xml). | |
| +| R2-5 | **Resolved.** Completion requires terminal state and cgroup emptiness; uncertain stops retain replication and the lease. | |
| +| R2-7 | **Resolved.** Recovery derives both endpoints from the journal’s direction, completes that transaction, then converges to current intent. | |
| +| R2-9 | **Resolved for the previously reported defects.** Flat minting and explicit reversal remain specified. The remaining downgrade defect is under R5-2. | |
| +| R2-14 | **Resolved at spec level.** The IPv6 exception is explicit, bounded, rechecked and reported. | |
| +| R1-4 | **Resolved.** Completion is independent of log EOF; blocking observations remain outside the activator mutex. | |
| +| R1-5 | **Resolved.** Preparation, execution budget, cancellation, result retention and termination-before-cleanup are specified. | |
| +| R1-8 | **Resolved under the recorded decision.** Shared tier limits remain; per-service OOM families are an explicit difference. | |
| +| R1-12 | **Resolved.** Named consumer fences and bidirectional recovery cover the reported partial-migration failure. | |
| +| R1-13 | **Partially resolved overall.** Reverse recovery is specified; safe downgrade still depends on the incomplete guard under R5-2. | |
| +| R1-15 | **Resolved at spec level.** No unsafe PID-namespace fallback; the behavioural gate and bounded IPv6 exception remain. | |
| +| R1-18 | **Resolved under the recorded ruling.** Remote reporting and layout operations are specified; the `foreign` repair residual remains explicitly accepted. | |
| + |
| +**R7-1 — P2 — §§3.1, 5.3–5.4, 6.7: Retain the authenticated control service, but make orphan-unit cleanup expressible.** |
| + |
| +The [startup sweep](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1244) enumerates systemd units and jobs, then requires `/stop` for every remaining invocation before activation begins. However, [the control protocol](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:859) accepts only a valid full hostname and reconstructs its unit through `InstanceID(host)`. |
| + |
| +For a long hostname, the enumerated unit contains a truncated, hashed identifier. The new `_` prefix deliberately makes that identifier invalid as a hostname. For example, applying the specified algorithm produces: |
| + |
| +```text |
| +host: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa.example.com |
| +iid: _aaaaaaaaaaaaaaaaaaaaaa-aeab2db4d462892c |
| +``` |
| + |
| +Passing that `iid` as `host` fails validation. A registry lookup can recover the hostname while its row exists, but cannot cover an orphaned unit whose row has disappeared. The hash cannot reconstruct the missing hostname. Thus the required sweep cannot stop every discovered unit through its only authorized channel; it must stall startup or abandon its stated completion condition. |
| + |
| +**Correction:** retain §5.4’s process authentication and assign enumeration-and-stop cleanup to the control service, restricted to the three exact templates. Alternatively, provide a stop-only operation accepting a validated instance identifier. Either mechanism must cover units and pending jobs without registry rows and require terminal state plus empty cgroups before completing. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |