amadan
spec: fleet-internal engines rev 10 (Astra R9: invariant I1 at the launch gate)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+90
−3
docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md+45 −3docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R9.md+45 −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 102.496s ? github.com/carlosframework/platform/cmd/changelog [no test files] ok github.com/carlosframework/platform/cmd/console 3.135s ok github.com/carlosframework/platform/cmd/moveprobe 93.282s ok github.com/carlosframework/platform/cmd/zddprobe 0.714s ok github.com/carlosframework/platform/internal/activator 250.668s ok github.com/carlosframework/platform/internal/agentsock 0.022s ok github.com/carlosframework/platform/internal/alerting 0.005s ok github.com/carlosframework/platform/internal/analytics 0.042s ok github.com/carlosframework/platform/internal/appconfig 2.513s ok github.com/carlosframework/platform/internal/apperr 0.092s ok github.com/carlosframework/platform/internal/applog 0.165s ok github.com/carlosframework/platform/internal/awsinv 0.007s ok github.com/carlosframework/platform/internal/boxchoice 0.004s ok github.com/carlosframework/platform/internal/boxid 1.147s ? 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.008s ok github.com/carlosframework/platform/internal/caps 0.013s ok github.com/carlosframework/platform/internal/certwarm 0.003s ok github.com/carlosframework/platform/internal/cgroup 0.720s ok github.com/carlosframework/platform/internal/changelog 0.347s ok github.com/carlosframework/platform/internal/claimactivation 0.854s ok github.com/carlosframework/platform/internal/clamd 0.059s ? 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 b427e4a9d..a906cb5fe 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:** 9. |
| +**Revision:** 10. |
| **Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow). |
| +- **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 |
| + the invariant every path must keep, **I1**, and enforces it at the one |
| + place every path passes through: the launch. A launch of a declaring |
| + build sets the mark and completes the barrier first, cancelling the |
| + public request that caused it (R9-1). Marked **(codex R9-1)**. |
| - **Rev 9** answers Astra round 8 (`CODEX-FINDINGS-ENGINES-R8.md`, reject, |
| a P1 and a P2, both accepted) by changing approach rather than adding a |
| third proof: a route never becomes public automatically. Clearing the |
| @@ -238,6 +245,33 @@ copying the source's kind and backend but no version, and adoption skips it |
| ambiguously, is treated as `NULL` and refused, and logged by name, until |
| the reconciler records its owner. |
| +**The invariant (codex R9-1).** |
| + |
| +> **I1.** No process of a build whose manifest declares `doc_engine` runs |
| +> while its group's mark is `0`. |
| + |
| +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 |
| +pending generation swap, an un-cycled hibernating route, a sleeping unit, |
| +and wake recovery falling back to `GoodVersion` |
| +(`rollout/wakeplan.go:76`, `:111`; `activator/wakeplan.go:448`). So I1 is |
| +enforced where every one of those paths ends: **the launch gate.** Every |
| +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 |
| +set-before is the same gate, reached earlier. |
| + |
| +`--public` (below) is the only writer of `0`, and it checks I1 directly: |
| +the group is stopped and its cgroups empty. Any later declaring launch |
| +re-marks the group through the gate. The one place I1 is not enforced is |
| +stated as a residual under "Classification before serving". |
| + |
| **Setting the mark: the serving barrier (codex R2-1).** Adoption |
| repoints the live symlink (`release/adopt.go:1751`), restarts |
| (`adopt.go:1831`) and records the version afterwards (`adopt.go:2051`), |
| @@ -287,8 +321,10 @@ and the edge serves an in-memory map refreshed on a 2 s registry poll |
| cannot; |
| 4. writes `0` and releases the lock. |
| - Anything that starts afterwards starts from the live version, which step |
| - 1 proved non-declaring and the lock kept there. The route's next request |
| + Whatever starts afterwards passes the launch gate: the live version, |
| + which step 1 proved non-declaring, starts under `0`; a declaring build |
| + chosen by wake recovery (`GoodVersion`) re-marks the group first and the |
| + triggering public request is cancelled (I1). The route's next request |
| wakes it. The cost is a short stop on a rare operation; a log line on the |
| capability pass names every internal route whose live release no longer |
| declares `doc_engine` and holds no grant, with this command. |
| @@ -735,6 +771,11 @@ process, real unix sockets and a real cgroup check where the kernel allows |
| the live manifest declares or a grant remains, stops the group, refuses if |
| a cgroup stays non-empty, and otherwise clears; the next request wakes the |
| non-declaring build. |
| +- I1 per launch path: for each of an exec child, a nested run unit, a |
| + generation swap, a seed, a command, a unit-backed start and a wake plan's |
| + 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. |
| - 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; |
| @@ -843,3 +884,4 @@ it, not only over a private network. |
| | R7-2 TCP-backed minted rows have no owner | Accepted: owner recorded on the row; unique non-empty fallback, TCP included (§5.1) | |
| | 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) | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R9.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R9.md| new file mode 100644 |
| index 000000000..3d0b7862f |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R9.md |
| @@ -0,0 +1,45 @@ |
| +| Previous finding | Round 9 assessment | |
| +|---|---| |
| +| R1-1: flat tenant borrows a nested socket | Fixed by the peer-cgroup check (§5.4). | |
| +| R1-2: aliases and path routes remain public | Fixed by checking the final upstream (§5.1). | |
| +| R1-3: new box starts public | Fixed for the reported missing-mirror case (§5.1). | |
| +| R1-4: revoked grants return after restart | Fixed for retained local state; fresh-box replay remains 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 listener ownership (§5.4). | |
| +| R1-7: transport and body limits | Resolved at spec level (§5.5). | |
| +| R2-1: stamp follows serving | Fixed by the admission barrier (§5.1). | |
| +| R2-2: upgrade serves unclassified engines | Fixed for the reported declaring-live-manifest case (§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: 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 remains 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 the arming prerequisite 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 every four minutes (§5.8). | |
| +| R5-1: platform-minted hostnames cannot classify | Fixed by execution-owner inheritance and explicit ownership (§5.1). | |
| +| R5-2: arming rejects isolated unit-backed routes | Fixed by distinguishing backing from exec layout (§6.2). | |
| +| R5-3: home edge lacks the probe path | Fixed by signing the watcher’s probe path (§5.8). | |
| +| R6-1: minted row’s own grant is ignored | Fixed by aggregating grants across the execution-owner group (§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 for existing processes by stopping the group and proving its cgroups empty (§5.1). A subsequent-start failure follows below. | |
| +| R7-2: TCP-backed minted rows have no owner | Fixed by recorded ownership and unique, non-empty backend matching, including TCP (§5.1). | |
| +| R8-1: upgrade classifies a running declaring build public | Reported case fixed by scanning staged versions; the missing-manifest case remains an explicit residual (§5.1). | |
| +| R8-2: sleeping unit-backed route cannot clear | Resolved by replacing automatic clearing with operator-controlled stop-and-clear (§5.1). | |
| + |
| +Reviewed spec `343f0443` against locally available amadan `origin/main` at `f550afa2`. The implementation files cited below match that revision. No files changed. |
| + |
| +1. **P1 — `--public` can expose a declaring recovery build on the next wake (§§5.1, 6.3).** |
| + |
| + Run a nested instance with generation rollouts enabled. Its healthy build A declares `doc_engine` and is recorded as `GoodVersion`; no group grant remains. Install non-declaring build B, which has not yet passed its first wake. |
| + |
| + Run `carlos route --host <host> --public`. B’s live manifest passes the check, all existing processes stop, the cgroups become empty, and the mark clears. Now send a public request. If B fails its first-wake health check, the activator starts A as its fallback and serves the request through A. The declaring engine is public again. |
| + |
| + Section 5.1’s assertion that everything subsequently starts from the live version is false on main. The wake planner retains `GoodVersion` as a separate staged identity and assigns it as an overlap-mode fallback ([internal/rollout/wakeplan.go:76](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/rollout/wakeplan.go:76), [internal/rollout/wakeplan.go:111](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/rollout/wakeplan.go:111)). After the failed build stops, the activator launches that fallback directly ([internal/activator/wakeplan.go:448](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/wakeplan.go:448)). The edge selects the actual serving generation ([internal/edge/genproxy.go:255](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/genproxy.go:255)). A failure record can also make a later wake choose A immediately, without repointing the live symlink ([internal/rollout/wakeplan.go:57](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/rollout/wakeplan.go:57), [internal/rollout/wakeplan.go:97](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/rollout/wakeplan.go:97)). |
| + |
| + This requires neither an incomplete stop nor a concurrent adoption. The declaring process starts **after** a successful clear, through a path outside the specified adoption barrier. |
| + |
| + **Suggested fix:** Make recovery and fallback activation enforce the internal mark against the build actually selected. A declaring selection must complete the admission barrier before execution, including cancelling the public request that triggered its wake. Alternatively, refuse clearing while a declaring build remains eligible for recovery, and define how the operator safely removes that eligibility. Add a test covering `--public` followed by a failed first wake and fallback to a declaring `GoodVersion`. |
| + |
| +**Overall verdict: reject.** The new clearing operation can succeed and subsequently expose a declaring engine through normal wake recovery. |
| \ No newline at end of file |