amadan
spec: fleet-internal engines rev 11 (Astra R10: I1 on the fenced mark)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+83
−8
docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md+32 −8docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R10.md+51 −0
CI cancelled — superseded by a newer push — run details
CI log
=== gate === cd launchctx && go vet ./... && go test ./... -count=1 ok amadan.net/carlos/platform.git/launchctx 0.011s ? amadan.net/carlos/platform.git/launchctx/controlname [no test files] ? amadan.net/carlos/platform.git/launchctx/wireid [no test files] go vet ./... gofmt -l .: clean go test ./... -count=1 -timeout 30m ok github.com/carlosframework/platform 104.371s ? github.com/carlosframework/platform/cmd/changelog [no test files] ok github.com/carlosframework/platform/cmd/console 3.004s ok github.com/carlosframework/platform/cmd/moveprobe 93.338s ok github.com/carlosframework/platform/cmd/zddprobe 0.719s ok github.com/carlosframework/platform/internal/activator 251.216s ok github.com/carlosframework/platform/internal/agentsock 0.032s ok github.com/carlosframework/platform/internal/alerting 0.004s ok github.com/carlosframework/platform/internal/analytics 0.045s ok github.com/carlosframework/platform/internal/appconfig 2.570s ok github.com/carlosframework/platform/internal/apperr 0.095s ok github.com/carlosframework/platform/internal/applog 0.162s ok github.com/carlosframework/platform/internal/awsinv 0.005s ok github.com/carlosframework/platform/internal/boxchoice 0.005s ok github.com/carlosframework/platform/internal/boxid 0.580s ? github.com/carlosframework/platform/internal/boxid/boxidtest [no test files] ? github.com/carlosframework/platform/internal/boxid/internal/signtest [no test files] ok github.com/carlosframework/platform/internal/boxvolumes 0.010s ok github.com/carlosframework/platform/internal/caps 0.015s ok github.com/carlosframework/platform/internal/certwarm 0.005s ok github.com/carlosframework/platform/internal/cgroup 0.738s ok github.com/carlosframework/platform/internal/changelog 0.367s ok github.com/carlosframework/platform/internal/claimactivation 0.901s ok github.com/carlosframework/platform/internal/clamd 0.060s ? github.com/carlosframework/platform/internal/cliflag [no test files] amadan: job cancelled — a newer push superseded it
diff --git a/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md b/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md| index a906cb5fe..ab44d5940 100644 |
| --- a/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md |
| +++ b/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md |
| @@ -1,9 +1,16 @@ |
| # Fleet-internal engines: a doc engine nobody on the internet can call |
| **Date:** 2026-10-21 |
| -**Revision:** 10. |
| +**Revision:** 11. |
| **Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow). |
| +- **Rev 11** answers Astra round 10 (`CODEX-FINDINGS-ENGINES-R10.md`, |
| + reject, one P1: a mark written but never fenced, after a failed reload |
| + and a timed-out adoption, let a recovery launch start a declaring build |
| + while a public request was admitted). I1 now speaks of the **fenced** |
| + mark, not the registry's, and every declaring launch requires the fence |
| + whether or not it finds `1` already written (R10-1). Marked |
| + **(codex R10-1)**. |
| - **Rev 10** answers Astra round 9 (`CODEX-FINDINGS-ENGINES-R9.md`, reject, |
| one P1: after `--public`, a failed first wake falls back to a declaring |
| `GoodVersion`). Instead of a fourth path-specific rule, §5.1 now states |
| @@ -247,8 +254,15 @@ copying the source's kind and backend but no version, and adoption skips it |
| **The invariant (codex R9-1).** |
| -> **I1.** No process of a build whose manifest declares `doc_engine` runs |
| -> while its group's mark is `0`. |
| +> **I1.** A process of a build whose manifest declares `doc_engine` starts |
| +> only after the edge has **fenced** its group as internal: the edge's |
| +> fenced counter (below) has reached a registry change that set the |
| +> group's mark to `1`, and no later change has cleared it. |
| + |
| +What protects the public is the edge's serving map, not the registry row |
| +(codex R10-1): a `1` written while the edge's `Reload` fails |
| +(`edge.go:925`, `:993`) refuses nobody. So the registry mark is the |
| +intent, and the fence is the fact I1 is about. |
| Rounds 2 to 9 each found one more path by which a declaring build could |
| run under a public mark: adoption's order, requests admitted early, a |
| @@ -260,11 +274,16 @@ activator launch path (an exec child, a nested run or generation unit |
| through the control service, a unit-backed `systemctl start`, a seed, a |
| `carlos run` command, a swap's incoming generation, a wake plan's |
| fallback or recovery build) reads the manifest of the build it is about to |
| -start. If that build declares `doc_engine` and the group's mark is `0`, |
| -the launch first writes `1` and waits for the edge's fence (below), which |
| -cancels every public request admitted under `0`, including the one whose |
| -wake triggered the launch; only then does it start the process. A launch |
| -whose build manifest it cannot read is treated as declaring. Adoption's |
| +start. If that build declares `doc_engine`, the launch writes `1` if it is |
| +not already written, and then **always** waits for the edge's fence to |
| +cover the group's current mark (below), which cancels every public request |
| +admitted before it, including the one whose wake triggered the launch. |
| +Only then does it start the process. A launch that finds `1` written but |
| +not yet fenced (a timed-out adoption, a reload that keeps failing) waits |
| +the same way; if the fence does not arrive within the bound, the launch is |
| +refused, the wake fails, and the request gets the activator's ordinary |
| +wake-failure answer. A launch whose build manifest it cannot read is |
| +treated as declaring. Adoption's |
| set-before is the same gate, reached earlier. |
| `--public` (below) is the only writer of `0`, and it checks I1 directly: |
| @@ -776,6 +795,10 @@ process, real unix sockets and a real cgroup check where the kernel allows |
| fallback to a declaring `GoodVersion` after a failed first wake, a launch |
| of a declaring build under `0` sets `1`, completes the fence, and cancels |
| the public request that caused it before the process starts. |
| +- With the edge's reload held failing: an adoption of a declaring build |
| + times out with `1` written; a later recovery wake that selects a |
| + declaring `GoodVersion` is refused, no declaring process starts, and the |
| + public request gets the wake-failure answer. |
| - Upgrade classification marks a route internal when its live version is |
| non-declaring but another staged version of the app declares. |
| - A TCP-backed instance's minted hostname keeps serving across the upgrade; |
| @@ -885,3 +908,4 @@ it, not only over a private network. |
| | R8-1 upgrade classifies a running declaring build public | Accepted: staged declaring versions classify `1`; residual stated (§5.1) | |
| | R8-2 a sleeping unit-backed route cannot clear | Accepted, with R7-1: no automatic clear; `--public` stops the group and checks cgroups (§5.1) | |
| | R9-1 `--public` then a fallback to a declaring `GoodVersion` | Accepted: invariant I1 enforced at every launch (§5.1) | |
| +| R10-1 a written but unfenced `1` lets a declaring launch through | Accepted: I1 is about the fenced mark; every declaring launch waits for the fence (§5.1) | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R10.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R10.md| new file mode 100644 |
| index 000000000..f734ae53a |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R10.md |
| @@ -0,0 +1,51 @@ |
| +| Previous finding | Round 10 assessment | |
| +|---|---| |
| +| R1-1: flat tenant borrows a nested socket | Fixed by peer-cgroup authentication (§5.4). | |
| +| R1-2: aliases and path routes remain public | Fixed by checking the final upstream (§5.1). | |
| +| R1-3: new box starts public | Reported case fixed by classification before serving (§5.1). | |
| +| R1-4: revoked grants return after restart | Fixed with retained state; fresh-box replay is an explicit residual (§5.3). | |
| +| R1-5: door exceptions fail across routing | Resolved by removing the owner exception and defining the identity transition (§5.4). | |
| +| R1-6: socket lifecycle conflicts | Fixed by instance-level ownership (§5.4). | |
| +| R1-7: transport and body limits | Resolved at spec level (§5.5). | |
| +| R2-1: stamp follows serving | Reported ordering fixed by the admission barrier (§5.1). | |
| +| R2-2: upgrade serves unclassified engines | Reported case fixed by startup classification and refusal of `NULL` (§5.1). | |
| +| R2-3: flat callers borrow door credentials | Fixed by the door’s UID restriction (§§5.4, 6.2). | |
| +| R2-4: deployment verification fails | Fixed by watch tickets (§5.8). | |
| +| R2-5: port-80 refusal cannot work remotely | Resolved by the narrowed contract (§5.1). | |
| +| R3-1: previously admitted requests cross the mark | Fixed when the barrier completes: acknowledgement waits for cancellation and completion (§5.1). | |
| +| R3-2: flat tenant injects into a nested caller | Fixed by excluding unisolated execution while armed; historical compromise is explicitly excluded (§6.2). | |
| +| R3-3: grant-only routes lack watch tickets | Fixed: every deploy target receives a ticket (§5.8). | |
| +| R4-1: foreign instances and workers remain unisolated | Fixed by arming prerequisites and launch refusals (§6.2). | |
| +| R4-2: path routing widens an engine grant | Fixed by exact-host engine dispatch (§5.4). | |
| +| R4-3: watch tickets expire mid-watch | Fixed by renewal (§5.8). | |
| +| R5-1: platform-minted hostnames cannot classify | Fixed by execution-owner inheritance (§5.1). | |
| +| R5-2: arming rejects isolated unit-backed routes | Fixed by distinguishing backing from layout (§6.2). | |
| +| R5-3: home edge lacks the probe path | Fixed by signing the probe path (§5.8). | |
| +| R6-1: minted row’s own grant is ignored | Fixed by aggregating group grants (§5.1). | |
| +| R6-2: static platform domains are refused | Fixed by restricting inheritance to minted instance rows (§5.1). | |
| +| R7-1: clearing exposes a still-serving generation | Fixed by stopping the group and proving its cgroups empty (§5.1). | |
| +| R7-2: TCP-backed minted rows have no owner | Fixed by explicit ownership and unique non-empty backend matching (§5.1). | |
| +| R8-1: upgrade classifies a running declaring build public | Reported case fixed by scanning staged manifests; missing-manifest exposure remains an explicit residual (§5.1). | |
| +| R8-2: sleeping unit-backed route cannot clear | Resolved by operator-controlled stop-and-clear (§5.1). | |
| +| R9-1: recovery launches a declaring `GoodVersion` after clearing | First launch under `0` fixed by the launch gate (§5.1). An already-`1`, unfenced state remains uncovered below. | |
| + |
| +Reviewed `267c0ee6` against locally available amadan `origin/main` at `f550afa2`. The implementation files cited below match that revision. No files changed. |
| + |
| +**1. P1 — A pending internal mark lets a later recovery launch skip the fence while I1 holds (§§5.1, 6.3).** |
| + |
| +The [launch rule](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md:263) requires writing `1` and waiting for the fence **when the group’s mark is `0`**. But `1` does not establish that the fence completed: the [timeout rule](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md:298) deliberately leaves it set after an unsuccessful wait. |
| + |
| +A concrete sequence: |
| + |
| +1. A sleeping nested instance has declaring build A as `GoodVersion`, non-declaring B installed, and an overlap-mode failure record that selects A for recovery. With no grant remaining, `--public` stops the group and clears its mark. |
| +2. Adoption attempts declaring build C. It writes `1`, but the edge’s reload fails. After 30 seconds adoption returns without repointing. The registry says `1`; the serving map still says `0`; B remains installed. |
| +3. While reload remains unsuccessful, a public request passes the old map’s admission check and wakes the instance. Recovery selects A. |
| +4. A’s launch reads its declaring manifest and the already-set mark `1`. The specified conditional does not require this launch to finish the outstanding fence. A starts, and the admitted public request reaches it. |
| + |
| +These are existing execution paths. A failed alias read aborts reload before replacing the serving map ([edge.go:925](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:925), [edge.go:993](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:993)). A blocked installed build selects `GoodVersion` directly ([rollout/wakeplan.go:97](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/rollout/wakeplan.go:97)), and the activator launches that selected build ([activator/wakeplan.go:388](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/wakeplan.go:388)). Once wake succeeds, the waiting request invokes its proxy ([activator.go:5404](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/activator.go:5404)), which selects the actual serving generation ([genproxy.go:255](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/genproxy.go:255)). |
| + |
| +**I1 holds throughout:** A runs only while the registry mark is `1`. Public access nevertheless remains possible because the edge has not fenced that mark. |
| + |
| +**Suggested fix:** Every declaring launch must require acknowledgement of the group’s current internal admission epoch, including when it finds `1` already set. A pending or timed-out transition must remain a launch refusal until its fence completes. Add a test that holds reload unsuccessful, times out adoption, and then requests a recovery wake; no declaring process may start. |
| + |
| +**Overall verdict: reject.** I1 alone permits a declaring process behind an internal registry mark that the serving edge has not yet enforced. |
| \ No newline at end of file |