amadan
Isolated exec spec: revision 7 after codex round 6
Round 6 findings committed unedited. All accepted: hashed instance identifiers carry a `_` prefix no host can have, so the short and hashed domains cannot meet; a collision is `conflict` and refuses to wake rather than falling back to the unisolated path; downgrade guards require completed reversal; the control service builds unit names from InstanceID.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YZ1ZvWj7naf73GjTX8MBv5
2 files changed,
+86
−23
docs/superpowers/specs/2026-09-11-isolated-exec-design.md+47 −23docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R6.md+39 −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 f864e2afd..d7fc0d083 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 6, after codex rounds 1 to 5 |
| -(19 + 14 + 7 + 4 + 3 findings, all accepted; §13) · **Requested by:** discussion |
| +**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 |
| #126 (Tito, with box evidence), approved in direction by Paul on |
| 2026-09-11 |
| @@ -294,16 +294,27 @@ 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 |
| +and otherwise `_` + the first 22 bytes of the host + `-` + the first 16 |
| +hex digits of `sha256(host)`, which is also 40 bytes. **The two domains |
| +cannot meet** (codex R6-1): no valid host contains `_` |
| +(`controlname` labels are `[a-z0-9-]`), so a hashed identifier is never |
| +equal to any short host, and two hashed identifiers are equal only on a |
| +64-bit hash collision between two long hosts sharing a 22-byte prefix. |
| +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; `_` needs no escaping). 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 nonetheless collide in `InstanceID` |
| +classify as **`conflict`**, which **refuses to wake** with both hosts |
| +named and is never the unisolated fallback: a host that is already |
| +`nested` must never be moved to the `childProc` path by the arrival of |
| +a second row (R6-1). The layout pass skips a `conflict` host, status |
| +reports it, and the console's create-instance door refuses a new host |
| +whose identifier collides with an existing row on the target box. The |
| +pass also 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 |
| @@ -328,7 +339,7 @@ nested path into a row. |
| 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]) |
| + return "_" + host[:22] + "-" + hex.EncodeToString(sum[:8]) // '_' never occurs in a host |
| } |
| func InstanceDir(dataDir, host string) string { |
| return filepath.Join(dataDir, "instances", InstanceID(host)) |
| @@ -851,9 +862,11 @@ the three literals; the memory value must parse as a `Limit` the agent |
| already knows how to produce (`internal/cgroup`, |
| `TierDefault`/`TierChildren`). Anything else is a 400 with no systemctl |
| call. The unit name is |
| -`"carlos-instance" + suffix + "@" + escape(host) + ".service"` and the |
| -slice name `"carlos-instances-" + escape(host) + ".slice"`, built from |
| -the validated pieces, never from the request string. |
| +`"carlos-instance" + suffix + "@" + escape(InstanceID(host)) + ".service"` |
| +and the slice name `"carlos-instances-" + escape(InstanceID(host)) + ".slice"`, |
| +built from the validated host by the same `InstanceID` and escape |
| +functions the agent used to create the directories (§3.1, §4), never |
| +from the request string (codex R5-3 disposition). |
| What this grants the agent: start, stop, reset and tier control of units |
| named `carlos-instance*@<host>` and their host slice. That is exactly |
| @@ -1333,6 +1346,7 @@ The exec backend classifies each activator-managed route on every |
| | `DBPath == DefaultDBPath` (flat), `Socket == DefaultSocket` (flat) | `flat` | today's `childProc`, unchanged, unisolated | |
| | `DBPath == NestedDBPath`, `Socket == NestedSocket` | `nested` | `unitProc` (§6) | |
| | a journal exists in `/data/layout/<host>.json` | `fenced` | refuses to wake; reason from the journal | |
| +| another row on the box has the same `InstanceID` | `conflict` | refuses to wake; both hosts named (§3.1) | |
| | anything else | `foreign` | today's `childProc`; reported for the operator (§8.3) | |
| A fleet rolled to this release behaves byte-for-byte as before until an |
| @@ -1477,14 +1491,18 @@ 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). |
| + 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 |
| + 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). |
| - **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. |
| + any `nested`, `fenced` or `conflict` row, or no layout field at all, |
| + and names the boxes and rows. |
| - 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. |
| @@ -1523,7 +1541,8 @@ to build (R1-18, accepted as the residual). A console-provisioned row |
| `internal/status/snapshot.go` gains a per-route `layout` field with one |
| of `flat`, `nested`, `fenced` (with the journal's phase and reason), |
| -`foreign` (with both values), `external`, and a box-level |
| +`conflict` (with the other host), `foreign` (with both values), |
| +`external`, and a box-level |
| `layout_mode` (`flat`, `nested`, or `none` before any intent). `carlos |
| status`, `carlos instances --layout` and the console's instance page |
| render them; a box that predates the field shows `unknown (box predates |
| @@ -1951,3 +1970,8 @@ rollback runs the old binary). |
| 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). |
| +- **Round 6** (codex, `CODEX-FINDINGS-ISOLATED-EXEC-R6.md`, 1 new |
| + finding plus 2 partials, verdict request changes). All accepted: |
| + 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). |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R6.md b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R6.md| new file mode 100644 |
| index 000000000..d9a4530cf |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ISOLATED-EXEC-R6.md |
| @@ -0,0 +1,39 @@ |
| +| Prior finding | Disposition at `58276fc3` | |
| +|---|---| |
| +| R5-1 | **Resolved.** Custom socket paths remain supported; the reserved-endpoint and peer-address checks remain. Retain the authenticated control service (§5.4). | |
| +| R5-2 | **Partially resolved.** The [downgrade guards](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1478) check `layout_mode` and journals. But `layout_mode` records requested intent, not completed reversal. A revert refused at quiescence or the [destination collision check](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1403), before journal creation, leaves a nested row with flat intent and no journal. Both guards permit downgrade, and [unit removal still unmounts its database](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/host/systemapply.go:522). Require verified completion of reversal, including absence of nested rows, before removing the mounts. | |
| +| R5-3 | **Partially resolved.** Socket paths are bounded, but [§5.3 explicitly constructs unit and slice names using `escape(host)`](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:854), whereas §4 requires `escape(InstanceID(host))`. For hosts longer than 40 bytes, the requested unit’s bind sources differ from the directories preparation created. Use `InstanceID(host)` consistently in both constructions. | |
| +| R2-4 | **Resolved.** Blocking seed execution and `RemainAfterExit=yes` retain the invocation and result until capture (§§4.2, 5.3, 6.5). [systemd service semantics](https://raw.githubusercontent.com/systemd/systemd/v257/man/systemd.service.xml). | |
| +| R2-5 | **Resolved.** Terminal state and cgroup emptiness are required; foreign invocations are stopped; uncertain stops retain replication and the lease. | |
| +| R2-7 | **Resolved.** Both endpoints and artifact sources follow the journal’s own direction. Recovery completes that transaction before converging to current intent (§§3.3, 8.2). | |
| +| R2-9 | **Resolved for the previously reported defects.** Flat minting and explicit reversal remain specified. The remaining mount-removal defect is under R5-2. | |
| +| R2-14 | **Resolved at spec level.** The IPv6 exception remains explicit, bounded, rechecked and reported. | |
| +| R1-4 | **Resolved.** Completion is independent of log EOF, and 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 journal recovery cover the reported partial-migration failure. | |
| +| R1-13 | **Partially resolved overall.** Reverse-journal validation is fixed; safe downgrade still depends on the incomplete prerequisite 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 operations and reporting are specified; the `foreign` repair residual remains explicitly accepted. | |
| + |
| +**R6-1 — P1 — §§3.1, 8.1: An identifier collision switches an already-isolated instance to unisolated execution.** |
| + |
| +The new [collision rule](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:303) classifies both colliding hosts as `foreign`. The [spawn table](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/docs/superpowers/specs/2026-09-11-isolated-exec-design.md:1336) runs `foreign` hosts through the existing unisolated `childProc` path. |
| + |
| +Consequently, adding a colliding row after the first host has migrated causes that existing host’s next wake to run without its isolation namespace. |
| + |
| +This requires no hash search. The short-name and hashed-name branches overlap. Applying the specified function gives: |
| + |
| +```text |
| +H = aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa.example.com |
| +S = aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa-aeab2db4 |
| + |
| +InstanceID(H) = S |
| +InstanceID(S) = S |
| +``` |
| + |
| +Both names pass the repository’s [hostname-shape validator](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/isolated-exec-spec/internal/controlname/names.go:18). I verified the hash and collision against the specified algorithm. |
| + |
| +**Correction:** an identity conflict must refuse execution, particularly for an already-nested row; it must never select the unisolated fallback. Separate the short and hashed identifier domains if retaining the claim that collisions require an unlikely hash collision. Verify adding the second row after the first has migrated. |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |