amadan
Isolated exec spec: revision 6 after codex round 5
Round 5 findings committed unedited. All accepted: InstanceID bounded to 40 bytes keys every directory, socket and unit name so no unix address exceeds 107 bytes; seed unit RemainAfterExit=yes retains its result; only the control endpoint is refused by path; system apply and the console rollback door refuse a pre-layout release while any box is nested; recovery endpoints follow the journal's own direction.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+200
−67
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+144 −67docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R5.md+56 −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 9a6d2066e..f864e2afd 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 5, after codex rounds 1 to 4 |
| -(19 + 14 + 7 + 4 findings, all accepted; §13) · **Requested by:** discussion |
| +**Date:** 2026-09-11 · **Status:** revision 6, after codex rounds 1 to 5 |
| +(19 + 14 + 7 + 4 + 3 findings, all accepted; §13) · **Requested by:** discussion |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -264,7 +264,7 @@ scoped to the three instance templates and does not extend to |
| ``` |
| /data/.instances/ the RAW directory: 0700 carlos:carlos; opened by the layout pass only (§3.2, §8.2) |
| /data/instances/ nosymfollow bind mount OF /data/.instances (§3.2); the view everything else uses |
| -/data/instances/<host>/ 0700 carlos:carlos, created by the agent |
| +/data/instances/<iid>/ 0700 carlos:carlos, created by the agent |
| <host>.db the database (+ -wal, -shm) |
| .activator-<host>.db-litestream/ the in-process replicator's shadow |
| <host>.env admin token (EnsureAdminToken, unchanged) |
| @@ -277,18 +277,35 @@ scoped to the three instance templates and does not extend to |
| /data/layout/ 0700 carlos:carlos |
| <host>.json the migration journal for a host in flight (§8.2) |
| /run/carlos/instances/ bind mount of itself, nosymfollow; 2750 carlos:carlos-sockets |
| -/run/carlos/instances/<host>/ 2750 carlos:carlos-sockets, created by the agent |
| +/run/carlos/instances/<iid>/ 2750 carlos:carlos-sockets, created by the agent |
| app.sock the instance's listener (rt.Socket); 0660 after health, as today |
| app.sock.control the agent's control listener (rt.Socket + ".control"); 0600 |
| exit.<role>.<invocation>.json the unit's advisory exit record (§6.5); tenant-writable, and treated so |
| /run/carlos/logs/ bind mount of itself, nosymfollow; 0700 carlos:carlos; NOT bound into any namespace |
| - <host>.run.sock the agent's log listener for the instance (§6.4) |
| - <host>.seed.sock ... for the seed |
| - <host>.sidecar.sock ... for the sidecar |
| + <iid>.run.sock the agent's log listener for the instance (§6.4) |
| + <iid>.seed.sock ... for the seed |
| + <iid>.sidecar.sock ... for the sidecar |
| /run/carlos-control/ 0750 root:carlos; NOT under /run/carlos, NOT in any namespace |
| control.sock the root channel (§5); SocketUser=carlos, 0600 |
| ``` |
| +**`<iid>` is the instance identifier, bounded to 40 bytes** (codex |
| +R5-3). A host may be 253 bytes (`controlname.ValidHostShape`), and a |
| +unix socket address holds 107 bytes of path, so a directory named after |
| +the host cannot carry `app.sock.control` for every valid host. |
| +`provision.InstanceID(host)` is the host itself when `len(host) <= 40`, |
| +and otherwise the first 31 bytes of the host, a `-`, and the first 8 hex |
| +digits of `sha256(host)`; it is the directory name under `/data/instances` |
| +and `/run/carlos/instances`, the log socket prefix, and, escaped, the |
| +unit instance and slice suffix (§4). File names *inside* the directory |
| +keep the full host (a file name may be 255 bytes). The longest address |
| +this produces, `/run/carlos/instances/<40>/app.sock.control`, is 79 |
| +bytes. Two rows on one box whose hosts collide in `InstanceID` (a |
| +truncation collision, astronomically unlikely and checked anyway) refuse |
| +to classify as anything but `foreign` with both hosts named, and the |
| +layout pass preflights every socket address it is about to commit |
| +against 107 bytes before it moves a file. |
| + |
| The socket tree keeps the #103 contract: `/run/carlos/instances` and |
| each host's run directory are `2750 carlos:carlos-sockets` (setgid, so |
| the socket an instance binds inherits the group, exactly as |
| @@ -308,20 +325,25 @@ flat paths, and the layout pass is the only thing that ever writes a |
| nested path into a row. |
| ```go |
| +func InstanceID(host string) string { // ≤ 40 bytes; see §3.1 |
| + if len(host) <= 40 { return host } |
| + sum := sha256.Sum256([]byte(host)) |
| + return host[:31] + "-" + hex.EncodeToString(sum[:4]) |
| +} |
| func InstanceDir(dataDir, host string) string { |
| - return filepath.Join(dataDir, "instances", host) |
| + return filepath.Join(dataDir, "instances", InstanceID(host)) |
| } |
| func NestedDBPath(dataDir, host string) string { |
| return filepath.Join(InstanceDir(dataDir, host), host+".db") |
| } |
| func InstanceRunDir(host string) string { |
| - return filepath.Join(SocketDir, "instances", host) |
| + return filepath.Join(SocketDir, "instances", InstanceID(host)) |
| } |
| func NestedSocket(host string) string { |
| return filepath.Join(InstanceRunDir(host), "app.sock") |
| } |
| func LogSocket(host, role string) string { |
| - return filepath.Join(SocketDir, "logs", host+"."+role+".sock") |
| + return filepath.Join(SocketDir, "logs", InstanceID(host)+"."+role+".sock") |
| } |
| // DefaultDBPath and DefaultSocket keep their flat meaning for this |
| // release; the next release, which drops the flat spawn path, points |
| @@ -483,11 +505,14 @@ file list or a phase from there. In particular: |
| - the migration journal lives in `/data/layout/<host>.json`, outside |
| every tenant mount, and every source and destination path in it is |
| *derived from the host name and the registry row* by the §3.1 helpers |
| - at plan time. On recovery the pass **recomputes** the plan from the row |
| - and honours the journal only if its paths equal the recomputation and |
| - its direction equals the fleet's recorded intent (`control/layout.json`, |
| - a bucket object no tenant can write, §8.2). During the transition a |
| - flat tenant can write `/data/layout` (same uid); a journal it forges can |
| + at plan time. On recovery the pass **recomputes** both endpoints for |
| + the journal's own direction and honours the journal only if its paths |
| + equal the recomputation and the row stands at one of them (§8.2); a |
| + journal that passes is completed to its own end and the host is then |
| + converged to the fleet's recorded intent (`control/layout.json`, a |
| + bucket object no tenant can write) before it is released. During the |
| + transition a flat tenant can write `/data/layout` (same uid); a journal |
| + it forges can |
| therefore cause the agent to do exactly what the next layout pass would |
| do for that host anyway, and nothing else (R3-1); |
| - the launch file is agent-written and then read by the trampoline |
| @@ -515,14 +540,17 @@ the existing nineteen are (`bootstrap.go:33-34`, `systemapply.go:339-398`): |
| §8.5, and the two control units of §5.2. Nothing enables the templates; |
| an instance unit exists only while the agent has started it. |
| -**Instance names are escaped hosts.** The unit instance is |
| -`systemd-escape(host)`: for a valid host (`[a-z0-9.-]`) that only turns |
| -`-` into `\x2d`. `%I` (unescaped) is used wherever the host is a path |
| -component; `%i` (escaped) wherever it is part of a unit name, which is |
| -what lets a per-host slice be spelled in the template (R1-8). The agent |
| -and the control service share one Go escape function (a copy of |
| -systemd's rules for this character set, pinned by a test against |
| -`systemd-escape` output for the hosts in the fixture set). |
| +**Instance names are escaped instance identifiers.** The unit instance |
| +is `systemd-escape(InstanceID(host))` (§3.1): for a valid identifier |
| +(`[a-z0-9.-]`) that only turns `-` into `\x2d`. `%I` (unescaped) is used |
| +wherever the identifier is a path component; `%i` (escaped) wherever it |
| +is part of a unit name, which is what lets a per-host slice be spelled |
| +in the template (R1-8). The agent and the control service share one Go |
| +escape function (a copy of systemd's rules for this character set, |
| +pinned by a test against `systemd-escape` output for the hosts in the |
| +fixture set). The templates never need the full host: every path they |
| +name is keyed by `<iid>`, and the trampoline learns the host from the |
| +launch file (§6.2). |
| ### 4.1 `carlos-instance@.service` |
| @@ -659,7 +687,7 @@ Differences: |
| | | seed | sidecar | |
| |---|---|---| |
| -| `Type=` | `oneshot` | `simple` | |
| +| `Type=` | `oneshot` with `RemainAfterExit=yes`: after `ExecStart` exits the unit stays `active (exited)` or `failed`, loaded, with its `InvocationID`, `Result` and `ExecMainStatus` retained until the control service stops it, so the seed's result can never be garbage-collected before it is read (codex R2-4, R5 disposition) | `simple` | |
| | `ExecStart=` | `/opt/carlos/carlos instance-exec seed %I` | `/opt/carlos/carlos instance-exec sidecar %I` | |
| | `ExecStopPost=` | `/opt/carlos/carlos instance-exit seed %I` | `/opt/carlos/carlos instance-exit sidecar %I` | |
| | `StandardOutput=` | `file:/run/carlos/logs/%I.seed.sock` | `file:/run/carlos/logs/%I.sidecar.sock` | |
| @@ -806,7 +834,7 @@ itself: |
| | Verb | What it runs | Returns | Agent deadline | |
| |---|---|---|---| |
| | `POST /start?host=H&role=run\|sidecar&memory_max=N` | `systemctl set-property --runtime carlos-instances-<esc>.slice MemoryMax=N MemoryHigh=0.9N MemorySwapMax=N`; `systemctl start <unit>` (blocking: the start job completes) | 200 with `{invocation_id}` from `systemctl show -p InvocationID <unit>`, read immediately after the start returns; or 502 with systemctl's stderr | 30s | |
| -| `POST /seed?host=H&memory_max=N` | the same `set-property`; `systemctl start --no-block` on `carlos-instance-seed@<esc>.service`; **immediately** `systemctl show -p InvocationID` (the unit is `activating` and has one); then wait until the unit is terminal and its cgroup empty (§6.5's rule, applied by the service as root), then `systemctl show -p Result,ExecMainStatus,ExecMainCode` | 200 with `{invocation_id, result, status, code}`; `result` is `unknown` if the unit unloaded before the final `show` | 150s: 120s seed budget plus `TimeoutStopSec` and slack (R3-5) | |
| +| `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 | |
| | `GET /ready` | nothing | 204 once the probe verdict (§8.5) is `ready`; 503 with the verdict otherwise | 5s | |
| @@ -877,10 +905,12 @@ can is **systemd's own record of which process is the agent**: |
| pass that check. It does not get that far, because of two checks on |
| **every unix dial the edge and the agent make** (`edge.go:2000-2014`'s |
| `unixProxy`, the activator's health and control dials, §6.1): |
| - 1. **the path is allowed before the dial**: it must be under |
| - `/run/carlos/` (flat sockets, `instances/`, `apps/`), so a registry |
| - row pointing at `/run/carlos-control/control.sock` is refused |
| - before `connect()`; |
| + 1. **the reserved endpoint is refused before the dial**: a path under |
| + `/run/carlos-control/` is never dialled as an upstream, so a |
| + registry row pointing at `control.sock` is refused before |
| + `connect()`. Nothing else is refused by path: a route whose |
| + operator stamped `--socket /run/titogo/example.sock` keeps working |
| + exactly as today (codex R5-1); |
| 2. **the listener answers to the path that was dialled**: after |
| `connect()` and before a byte is sent, `getpeername()` on the |
| connected socket returns the address the *listener* bound, which is |
| @@ -948,16 +978,20 @@ child; return a `unitProc` carrying the invocation id. |
| ```json |
| { |
| "schema": 1, |
| - "argv": ["/opt/carlos/live/<host>", "--socket", "/run/carlos/instances/<host>/app.sock", "--db", "/data/instances/<host>/<host>.db"], |
| + "host": "<host>", |
| + "argv": ["/opt/carlos/live/<host>", "--socket", "/run/carlos/instances/<iid>/app.sock", "--db", "/data/instances/<iid>/<host>.db"], |
| "env": ["PATH=...", "CARLOS_ADMIN_TOKEN=...", "CARLOS_CONTROL_SOCKET=...", "..."] |
| } |
| ``` |
| -`carlos instance-exec <role> <host>` runs as `ExecStart`, inside the |
| -namespace, as `carlos`. It reads `/data/instances/<host>/launch.<role>.json` |
| +`carlos instance-exec <role> <iid>` runs as `ExecStart`, inside the |
| +namespace, as `carlos`. It reads `/data/instances/<iid>/launch.<role>.json` |
| through `instancefs`, refuses a schema it does not know, refuses an |
| -`argv[0]` that is not `/opt/carlos/live/<host>` (defence in depth: the |
| -file is agent-written; the check is one line), and calls |
| +`argv[0]` that is not directly under `/opt/carlos/live/` or that does |
| +not equal `/opt/carlos/live/` plus the file's own `host` (defence in |
| +depth: the file is agent-written; the prefix check is the one that |
| +holds even against a rewritten file, since only the platform's live |
| +links live there), and calls |
| `syscall.Exec(argv[0], argv, env)`. It never parses env syntax: the |
| agent's `childEnv` (`backend_exec.go:802-814`) composes the list exactly |
| as it does today, including the agent-owned removal of tenant-supplied |
| @@ -1131,16 +1165,11 @@ agent owns these units and any other invocation is an anomaly to end, |
| not to adopt; the invocation id decides the event line's wording and |
| nothing about whether a writer is gone. |
| -**The seed's status is the one place a record is more than wording.** |
| -`/seed` returns systemd's `result`/`status` when the unit was still |
| -loaded at the final `show`, and `unknown` otherwise (§5.3). In the |
| -`unknown` case the agent reads the seed's exit record and takes its |
| -status. That record is tenant-writable, but a seed is the tenant's own |
| -code seeding the tenant's own database: a forged "success" leaves the |
| -tenant with whatever database its seed produced, and a forged "failure" |
| -deletes the tenant's own fresh database and restores nothing. The only |
| -party a seed record can deceive is its author, so it is allowed to |
| -decide the seed's outcome and nothing else. |
| +**The seed's outcome comes from systemd, always.** The seed unit |
| +carries `RemainAfterExit=yes` (§4.2), so it stays loaded, with its |
| +`Result` and `ExecMainStatus`, until the control service reads them and |
| +stops it (§5.3). `/seed` therefore always returns a complete result and |
| +the seed's exit record is, like every other record, wording only. |
| `sweepOnce`'s existing dead-child check (`activator.go:1105-1122`) sees a |
| flag, never a blocking call. `Restart=no` in the template is what makes |
| @@ -1405,10 +1434,12 @@ needed) and, per host in scope, in this order: |
| **Recovery is the journal, and it is exact, and it is checked** (R2-7, |
| R3-1, R4 disposition). On agent start and at the top of every layout |
| pass, for each journal, the check is against **both endpoints**, because |
| -the row is at `from` before step 8 and at `to` after it: the journal's |
| -`to` must equal the destination the §3.1 helpers derive for that host |
| -in the journal's own `mode`, its `from` must be the host-named flat |
| -paths of step 3, and the row must currently equal either `from` or `to`. |
| +the row is at `from` before step 8 and at `to` after it, and it is |
| +derived from **the journal's own direction** (codex R5 disposition): for |
| +`mode: nested`, `from` must be the host-named flat paths of step 3 and |
| +`to` the nested paths the §3.1 helpers derive; for `mode: flat` the two |
| +are swapped, artifact sources included. The row must currently equal |
| +either `from` or `to`. |
| A journal that fails any of those is refused (`layout: <host>: journal |
| does not match row; not acting`), the host stays `fenced`, and status |
| says so. **A journal that passes is completed to its own endpoint even |
| @@ -1435,16 +1466,42 @@ same fence, the same preflight in reverse. It exists so that a fleet |
| can be taken back to a layout the previous release serves **before** |
| that release is installed: the operator's rollback order is `layout |
| revert` (this release, verified `flat` in status) then `system rollback`. |
| -A `system rollback` or a failed-gate rollback that happens while hosts |
| -are `nested` lands the old binary on rows it honours (`rt.DBPath`, |
| -`rt.Socket`; `backend_exec.go:220-225, 557-562`). On the same boot the |
| -nested run directories still exist, so the old binary can bind the |
| -nested socket and serve the nested database while minting flat env |
| -files; after a reboot the run directories are gone and those hosts fail |
| -to bind, loudly and losslessly. Either way the database has one history, |
| -the nested one, and the revert's step 5 handles the stray env files when |
| -the new binary is back. The layout is never two databases: the fence |
| -and the destination check see to that. |
| +**That order is enforced, not advised** (codex R5-2). A downgrade |
| +removes this release's unit files: `installUnits` runs `systemctl |
| +disable --now` on every unit the candidate lacks (`systemapply.go:522`), |
| +so the bind mounts go with the binary, `/data/instances/<iid>/` becomes |
| +an empty mountpoint directory, and the old backend, honouring the nested |
| +`rt.DBPath` (`backend_exec.go:220-225`), would find no database and |
| +restore a second copy into the uncovered directory, which the next |
| +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) while the box's `layout_mode` is `nested` or |
| + any journal exists, with `layout revert first` as the reason; the |
| + installer is this binary for every downgrade from here, because a |
| + downgrade is an install performed by the installed binary (§8.1). |
| +- **The console's rollback door** (`system.go:466`) refuses a channel |
| + rollback to a pre-layout release while any box in the fleet reports |
| + `layout_mode: nested`, `fenced` rows, or no layout field at all, and |
| + names the boxes. |
| +- A failed-gate rollback of the upgrade *to* this release runs the old |
| + binary, but at that moment nothing is nested (§8.1). A failed-gate |
| + rollback of a later upgrade runs this binary, which knows the layout. |
| +- **Recovery for a layout that was unmounted anyway** (an operator |
| + removing units by hand): at start the control service (root) |
| + inspects the underlying mountpoint directories in a private mount |
| + namespace (`unshare -m`, `umount` the bind there, list) and, if |
| + `/data/instances` or `/run/carlos/instances` holds anything under the |
| + mount, records the verdict `mountpoint held files while unmounted` |
| + and `GET /ready` refuses nested wakes until an operator has moved or |
| + removed them; the layout pass's destination check (step 5) then sees |
| + whatever was moved into the raw directory. Nothing is chosen |
| + silently; the databases are never two. |
| + |
| +The database therefore has one history in every path that is allowed |
| +to happen, and the two paths that are not allowed are refused with the |
| +revert named as the fix. |
| ### 8.3 `foreign` rows |
| @@ -1636,26 +1693,39 @@ sentinel `.path` units name fixed files under `/data`, never a host. |
| Unit level, all runnable in CI (no systemd needed): |
| -- `internal/provision`: `InstanceDir`, the nested helpers, the flat |
| - defaults unchanged, `LogSocket`, the escape function against |
| - `systemd-escape` fixtures. |
| +- `internal/provision`: `InstanceID` (identity below 41 bytes, |
| + truncation plus hash above, never longer than 40, stable), the nested |
| + helpers keyed by it, the flat defaults unchanged, `LogSocket`, the |
| + 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`. |
| - `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 |
| - pairs: a path outside `/run/carlos/` is refused before `connect()`; a |
| - symlink under `/run/carlos` to another listener yields a `getpeername` |
| + pairs: a path under `/run/carlos-control/` is refused before |
| + `connect()`; a custom path elsewhere (`/run/titogo/example.sock`) is |
| + dialled as today; a symlink to another listener yields a `getpeername` |
| mismatch and is closed before a byte is sent; a listener created by |
| another process and passed over (the `carlos-app@.socket` shape) is |
| accepted when its bound path is the one dialled. |
| +- `internal/host/systemapply`: a pre-layout candidate is refused while |
| + `layout_mode` is `nested` or a journal exists, and installed when the |
| + box is `flat`; the control service's start-time inspection of an |
| + underlying mountpoint that holds files (with a fake namespace runner). |
| +- `internal/console`: the rollback door refuses a pre-layout release |
| + while any box reports `nested`, `fenced` or no layout field, naming |
| + them. |
| - `instance-control`: a connection whose peer pid is not the edge's |
| `MainPID`, or whose uid is not `carlos`, is closed without a response; |
| every 400 (bad host, bad role, bad limit); the unit and slice names it |
| builds for a host with a dash; `set-property` (three properties) → |
| `start` ordering with no `reset-failed`; `/reset` tolerating "not |
| - loaded"; `/seed` starting `--no-block`, reading the invocation id |
| - while `activating`, waiting for terminal state plus empty cgroup, and |
| - returning `unknown` when the unit unloaded first; `/ready` from the |
| - probe verdict; with a fake `systemctl` runner and a fake peer. |
| + loaded"; `/seed` reading a retained result from an `active (exited)` |
| + and from a `failed` oneshot, waiting for the empty cgroup, then |
| + stopping it; `/ready` from the probe verdict; with a fake `systemctl` |
| + runner and a fake peer. |
| - `internal/activator`: classification of the four row shapes; |
| `prepare` mints the token for seed and run, writes `launch.<role>.json` |
| with the deduplicated env and the exact argv (the existing |
| @@ -1874,3 +1944,10 @@ rollback runs the old binary). |
| R2-7 journals validated against both endpoints and completed to their own end before convergence (§8.2); |
| R2-14 `v6: unverified` bounded by the five-minute re-run and reported in status (§8.5); |
| R1-18 the `foreign` residual accepted with its reason (§8.3). |
| +- **Round 5** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R5.md`, 3 new |
| + findings plus 2 partials, verdict request changes). All accepted: |
| + R5-1 only the control endpoint is refused by path; custom sockets elsewhere dial as today (§5.4); |
| + R5-2 `system apply` and the console's rollback door refuse a pre-layout release while any box is nested; underlying mountpoints inspected at start (§8.2); |
| + R5-3 `InstanceID`, bounded to 40 bytes, keys every directory, socket and unit name; addresses preflighted against 107 bytes (§3.1, §4, §6.2); |
| + R2-4 the seed unit carries `RemainAfterExit=yes`, so its result is retained until read; the record is wording again (§4.2, §5.3, §6.5); |
| + R2-7 recovery endpoints derived from the journal's own direction; §3.3 reconciled with §8.2 (§3.3, §8.2). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R5.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R5.md| new file mode 100644 |
| index 000000000..7aeede7cf |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R5.md |
| @@ -0,0 +1,56 @@ |
| +| Prior finding | Disposition at `0236be94` | |
| +|---|---| |
| +| R4-1 | **Resolved for the reported failure.** Removing the root-peer rejection preserves systemd-created application listeners. The replacement path restriction introduces R5-1 below. | |
| +| R4-2 | **Resolved.** The raw directory and confined directory-fd renames provide endpoints on one mount. The changed storage location introduces the downgrade defect in R5-2. | |
| +| R4-3 | **Resolved.** Custom paths are excluded from migration; the remaining forward sources follow their existing file contracts. | |
| +| R4-4 | **Resolved.** The probe no longer requires a forbidden netlink route query. | |
| +| R2-4 | **Partially resolved.** The seed-record outcome rule is now explicit. However, [`start --no-block` followed by `show`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:809) does not retain invocation identity. `--no-block` only enqueues the job: the subsequent query can precede activation or follow completion and unloading. “Immediately” supplies no synchronization. Retain the unit through completion and result capture, or provide equivalent request-to-invocation correlation. [systemctl semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemctl.xml), [unit garbage collection](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.unit.xml). | |
| +| R2-5 | **Resolved.** Foreign invocations are stopped, and completion still requires terminal state and an empty cgroup. Unproven stops retain replication and the lease. | |
| +| R2-7 | **Partially resolved.** Forward recovery now recognizes both row endpoints and changed fleet intent. But the [new validation](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1405) requires `from` to be flat even for a reverse journal. A legitimate nested→flat transaction therefore fails validation. Derive **both** endpoints from the journal’s direction, including artifact sources. Also reconcile §3.3’s remaining requirement that journal direction equal current fleet intent with §8.2’s explicit opposite rule. | |
| +| R2-9 | **Resolved for the original first-upgrade defect.** Flat minting preserves compatibility before migration. The newly introduced mount-removal defect is R5-2. | |
| +| R2-14 | **Resolved at spec level.** IPv6 evidence remains explicitly unverified when unavailable; the exception has a five-minute bound, rechecks and status reporting. | |
| +| R1-4 | **Resolved.** Completion is independent of log EOF, blocking observations stay outside the mutex, and the foreign-invocation completion exception is removed. | |
| +| R1-5 | **Partially resolved.** Preparation, execution budget, cancellation and termination-before-cleanup are specified. Seed invocation correlation remains defective under R2-4. | |
| +| R1-8 | **Resolved.** Shared tier limits and the deliberate per-service OOM-family difference are specified. | |
| +| R1-12 | **Partially resolved.** Consumer fences are specified; reverse-journal recovery remains defective under R2-7. | |
| +| R1-13 | **Partially resolved.** Explicit reversal and collision refusal replace the original history-selection defect, but reverse validation remains inconsistent under R2-7. | |
| +| R1-15 | **Resolved at spec level.** There is no unsafe PID-namespace fallback; the probe and bounded IPv6 exception are specified. | |
| +| R1-18 | **Resolved under the recorded ruling.** Remote reporting and layout operations are specified. The box-local `foreign` repair residual is explicitly accepted. | |
| + |
| +**R5-1 — P2 — §§5.4, 6.1, 8.3: Retain the authenticated control service, but preserve supported custom socket paths.** |
| + |
| +The new rule rejects every application dial outside `/run/carlos/`. An existing route with `Socket=/run/titogo/example.sock` therefore loses public traffic and health checks on upgrade, even though §8.3 promises that `foreign` routes keep running unchanged. |
| + |
| +The existing CLI accepts an explicit socket pathname, and the edge uses it without this directory restriction. The reviewed Tito precedent itself binds beneath `/run/titogo`. |
| + |
| +Evidence: [new dial restriction](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:878), [compatibility promise](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1451), [CLI socket input](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/cli.go:76), [edge dispatch](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/edge/edge.go:536). |
| + |
| +**Correction:** retain process authentication and the actual-peer-address check. Reserve and reject the broker endpoint explicitly while permitting existing ordinary upstream paths. Verify a legitimate custom socket outside `/run/carlos/` alongside direct and symlinked attempts to proxy to the broker. |
| + |
| +**R5-2 — P2 — §§3.2, 8.2, 9: Removing the new bind mounts invalidates the downgrade recovery claim.** |
| + |
| +This revision stores the database physically under `/data/.instances` and exposes it through `/data/instances`. An ordinary downgrade to a pre-layout release removes the new mount units: `installUnits` executes `systemctl disable --now` for every removed unit before deleting its file. |
| + |
| +Consequently, the old backend’s nested `DBPath` no longer reaches the database. The same change removes the nested runtime-directory view immediately, rather than only after reboot as §8.2 claims. |
| + |
| +There is also a second-copy path: the old backend sees the database as absent and invokes restore. Litestream creates missing parent directories, so it can restore into the uncovered `/data/instances/<host>/` while the original remains under `/data/.instances/<host>/`. Reinstalling the bind mount hides that restored copy from the specified collision check. |
| + |
| +Evidence: [new mount source](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:380), [downgrade claim](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1438), [removed-unit handling](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/systemapply.go:522), [missing-database handling](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/activator/backend_exec.go:220), [restore directory creation](/home/paulca/go/pkg/mod/github.com/benbjohnson/litestream@v0.5.14/replica.go:654). |
| + |
| +**Correction:** make completed reversal a checked prerequisite for removing these mounts and starting a pre-layout binary. Define recovery for an already-unmounted layout, including checking the uncovered mountpoint before remounting. Verify through the actual updater’s unit-removal path. |
| + |
| +**R5-3 — P1 — §§3.1, 6.1, 8.2: The longer socket paths make previously working hosts unwakeable after migration.** |
| + |
| +For a valid 80-byte hostname, the current application socket is 97 bytes and its control socket is 105 bytes. The proposed paths become: |
| + |
| +- Application: `/run/carlos/instances/<host>/app.sock` — **111 bytes**. |
| +- Control: the same path plus `.control` — **119 bytes**. |
| +- Sidecar log: `/run/carlos/logs/<host>.sidecar.sock` — **110 bytes**. |
| + |
| +Linux’s Unix socket address has a 108-byte pathname field; Go requires room for the terminating NUL. These new addresses cannot bind. Migration nevertheless accepts the flat row and commits the nested paths, after which the application cannot wake. |
| + |
| +Evidence: [runtime layout](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:279), [existing hostname validation](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/controlname/names.go:18), [Go’s address-length rejection](/usr/local/go/src/syscall/syscall_linux.go:547), [Linux Unix socket limits](https://man7.org/linux/man-pages/man7/unix.7.html). |
| + |
| +**Correction:** specify a bounded per-host runtime identifier consistently across socket paths, unit bind paths and log endpoints. Preflight every resulting Unix socket address before moving files. Include a hostname that fits the current application and control sockets but exceeds the proposed limits. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |