carlos / platform Public

spec: fleet-internal engines rev 9 (Astra R8 answered: no automatic clear; operator --public)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev 343f0443d08175bf340fd4a0bcfdfd250e7eff1c parent 9306d7a
2 files changed, +128 −42
  • docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md +77 −42
  • docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R8.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	103.030s
?   	github.com/carlosframework/platform/cmd/changelog	[no test files]
ok  	github.com/carlosframework/platform/cmd/console	3.115s
ok  	github.com/carlosframework/platform/cmd/moveprobe	92.302s
ok  	github.com/carlosframework/platform/cmd/zddprobe	0.717s
ok  	github.com/carlosframework/platform/internal/activator	250.734s
ok  	github.com/carlosframework/platform/internal/agentsock	0.019s
ok  	github.com/carlosframework/platform/internal/alerting	0.006s
ok  	github.com/carlosframework/platform/internal/analytics	0.018s
ok  	github.com/carlosframework/platform/internal/appconfig	2.481s
ok  	github.com/carlosframework/platform/internal/apperr	0.092s
ok  	github.com/carlosframework/platform/internal/applog	0.158s
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.641s
?   	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.012s
ok  	github.com/carlosframework/platform/internal/certwarm	0.003s
ok  	github.com/carlosframework/platform/internal/cgroup	0.711s
ok  	github.com/carlosframework/platform/internal/changelog	0.344s
ok  	github.com/carlosframework/platform/internal/claimactivation	0.847s
ok  	github.com/carlosframework/platform/internal/clamd	0.055s
?   	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 86d2fe1eb..b427e4a9d 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:** 8.
+**Revision:** 9.
**Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow).
+- **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
+ mark is an operator verb that stops the group under the adoption lock and
+ checks its cgroups are empty (R7-1, R8-1, R8-2). Upgrade classification
+ also marks a route internal when any staged version of its app declares
+ `doc_engine`. Marked **(codex R8-n)**.
- **Rev 8** answers Astra round 7 (`CODEX-FINDINGS-ENGINES-R7.md`, reject,
a P1 and a P2, both accepted). Clearing the mark waits for proof that no
process of a declaring build is left, not for adoption's return, which
@@ -231,7 +238,7 @@ 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.
-**Set before, clear after: the serving barrier (codex R2-1).** Adoption
+**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`),
and the edge serves an in-memory map refreshed on a 2 s registry poll
@@ -259,42 +266,62 @@ and the edge serves an in-memory map refreshed on a 2 s registry poll
stays `1`, and the next pass retries. The old, non-engine release is
refused publicly for that interval, which costs availability, never
exposure.
-- **Becoming public** (the incoming release does not declare `doc_engine`,
- the route is `1`, and no row of its group holds the grant): the mark is
- cleared only once the execution layer **confirms that no process of a
- declaring build remains** for the group **(codex R7-1)**. Adoption's
- return proves nothing: with generation rollouts armed, the restart
- callback only schedules the swap (`host/agent.go:4309`,
- `rollout/manager.go:483`) while the declaring generation keeps serving
- (`edge/genproxy.go:255`). The proof per backing:
- - a nested or exec instance: the activator reports the serving
- generation's build as the non-declaring version and no retiring
- generation of a declaring build still has a process (after the swap,
- `activator/swap.go:638`, and the retiring member's exit), or the
- instance is asleep with its live version non-declaring;
- - a unit-backed route: the unit's current main process was started from
- the non-declaring version after the repoint.
-
- Until that proof, the mark stays `1`, through a queued, failed or
- abandoned replacement and through a rollback. The capability pass checks
- for the proof each pass, and the activator signals it at the swap's end
- so the clear is prompt.
-- **Rollback** is an adoption like any other: to a declaring release, set
- before; away from one, clear after.
+- **Becoming public is never automatic (codex R7-1, R8-1, R8-2).** No
+ adoption, revoke, rollback or pass ever writes `0` over `1`. Rounds 6 to
+ 8 each found a new interleaving in which an automatic clear raced a
+ process of the declaring build that was still running (a generation
+ swap still pending, an awake hibernating unit adopted without a restart,
+ a sleeping unit with no main process to vouch for). So clearing is an
+ operator act whose preconditions are checked, not inferred:
+
+ carlos route --host <host> --public
+
+ On the box, holding the adoption lock (so the live version cannot move
+ under it), it:
+ 1. refuses unless the live release's manifest is readable and does not
+ declare `doc_engine`, and no row of the group holds the grant;
+ 2. stops the whole group (every unit and generation of the owner, through
+ the activator and the control service);
+ 3. confirms every cgroup of the group is empty (`carlos-instances-<iid>.slice`,
+ `carlos-app@<host>.service`, `carlos-exec@<host>`), and refuses if it
+ 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
+ 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.
+- **Rollback** to a declaring release is an adoption like any other: set
+ before. Rollback away from one leaves the mark set.
- The same barrier applies to a grant: `carlos route --grant doc-engine`
writes `1` and returns once the edge has loaded it (or says it timed out).
-**Classification before serving (codex R2-2).** The new column arrives
+**Classification before serving (codex R2-2, R8-1).** The new column arrives
`NULL` for every existing route. Before the upgraded agent opens any edge
-listener, it classifies every `NULL` instance route from the staged
-manifest of its live version (`release.ReadStagedManifest`), and if the
-sibling is missing, from the release's signed manifest in the bucket, as
-adoption's back-fill does. A route it still cannot classify stays `NULL`,
-is refused publicly, and is named in a log line every pass until the
-capability pass classifies it. This can make a route with no readable
-manifest unreachable until the bucket answers; that is the fail-closed
-choice. A route the agent creates later (provisioning, a move) is
-classified by its first adoption, which runs before the route is served.
+listener, it classifies every `NULL` instance route (minted rows follow their
+owner):
+
+- `1` if any row of the group holds the grant, or the live version's
+ manifest declares `doc_engine`, or **the manifest of any other version of
+ the app staged on the box declares it**. The last clause covers a box
+ whose live symlink has moved off a declaring build that is still running
+ (an awake hibernating route is repointed without a restart,
+ `release/adopt.go:1174`).
+- `0` only if the live manifest is readable, none of the above holds.
+- Otherwise (the live manifest is unreadable from the staged sibling and
+ from the bucket, as adoption's back-fill reads it) the route stays `NULL`,
+ is refused publicly, and is named in a log line every pass until the
+ capability pass classifies it. That is the fail-closed choice.
+
+A route that turns out `1` only because an old staged version declared is
+cleared with `--public` like any other. **Residual, stated:** a declaring
+version whose staged manifest failed to write, still running across the
+upgrade after the live symlink moved to a non-declaring version, would be
+classified `0`; it needs a sibling write failure on a doc-engine release
+and a pending, un-cycled switch away from it at the moment of the upgrade.
+A route the agent creates later (provisioning, a move) is classified by its
+first adoption, which runs before the route is served.
**What the edge does with it** (`ServeHTTP`):
@@ -618,10 +645,10 @@ key are operator steps in the runbook, not part of this build.
### 6.3 The public never reaches an internal route
- The mark lives in the box's own registry and survives restarts. It is set
- before a declaring release can serve and cleared only after a
- non-declaring one is live, with the edge's loaded state as the barrier;
- an unclassified route is refused (§5.1). No bucket read happens at serve
- time.
+ before a declaring release can serve, with the edge's fenced state as the
+ barrier, and cleared only by the operator's `--public`, which stops the
+ group first; an unclassified route is refused (§5.1). No bucket read
+ happens at serve time.
- The check runs on the final upstream's route, after every re-resolution,
before every dispatch branch (§5.1).
- Old non-home boxes backhaul public requests as ordinary hops; the home box
@@ -703,9 +730,13 @@ process, real unix sockets and a real cgroup check where the kernel allows
admits engine calls exactly as the owner does; a minted hostname of a
public route keeps working across the upgrade; a static platform domain
and a static canary keep serving.
-- With generation rollouts armed, deploying a non-declaring release over a
- declaring one keeps the route internal until the retiring generation has
- exited; a failed swap leaves it internal.
+- Deploying a non-declaring release over a declaring one, with and without
+ generation rollouts, leaves the route internal; `--public` refuses while
+ 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.
+- 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;
two TCP instances of one app with an unrecorded owner are refused until
the reconciler records it.
@@ -766,6 +797,8 @@ it, not only over a private network.
under their own uid use the door, enabled by the operator.
- Engine sockets only on boxes an operator armed; an armed box refuses
flat, foreign and worker launches rather than closing sockets afterwards.
+- A route never becomes public automatically; `carlos route --public` is
+ the only way back, and it stops the group.
- Unclassified routes are refused publicly (fail closed) even though that
can make a route with no readable manifest unreachable while the bucket
is down.
@@ -806,5 +839,7 @@ it, not only over a private network.
| R5-3 no source for the probe path | Accepted: the ticket signs the watcher's probe path (§5.8) |
| R6-1 grant on a minted row ignored | Accepted: grants anywhere in the group mark the group (§5.1) |
| R6-2 static platform domains refused | Accepted: inheritance only for minted instance rows (§5.1) |
-| R7-1 clear-after reopens a still-serving engine under rollouts | Accepted: clear only on proof no declaring process remains (§5.1) |
+| R7-1 clear-after reopens a still-serving engine under rollouts | Accepted in rev 8, superseded in rev 9 by the operator clear (§5.1) |
| 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) |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R8.md b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R8.md
new file mode 100644
index 000000000..45cf00923
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-ENGINES-R8.md
@@ -0,0 +1,51 @@
+| Previous finding | Round 8 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). A separate upgrade-classification gap follows below. |
+| R1-4: revoked grants return after restart | Fixed for retained local state; fresh-box replay remains explicitly accepted (§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). Divergence between installed and running builds remains uncovered below. |
+| 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 the expanded ownership mechanism (§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 the reported rollout: clearing waits for activation and declaring generations’ exit (§5.1). |
+| R7-2: TCP-backed minted rows have no owner | Fixed by recorded ownership and unique, non-empty backend matching, including TCP (§5.1). |
+
+Reviewed spec `9306d7a5` against locally available amadan `origin/main` at `aaa6a949`. The implementation files cited below match that revision. No files changed.
+
+1. **P1 — First-upgrade classification bypasses the new activation proof (§§5.1, 6.3).**
+
+ Run an awake, unit-backed route with hibernation enabled. Its running build A declares `doc_engine`, but the route holds no `doc-engine` grant. On the old platform build, the root adoption pass installs non-declaring build B and repoints the live symlink. Before the agent cycles A, the agent crashes. Start the upgraded agent.
+
+ The new column is `NULL`. The startup rule classifies it from B’s live manifest and writes `0`, although A still runs. Public requests can consequently reach the declaring build. The new proof requirement applies to clearing an existing `1`; the initial `NULL`→`0` classification does not require it.
+
+ This installed/running divergence exists on main: root adoption passes a nil restart callback for hibernating routes, including awake ones ([internal/release/adopt.go:1174](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/adopt.go:1174)). The manifest loader follows the live symlink ([internal/host/caps_pass.go:111](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/host/caps_pass.go:111)). A fresh agent can encounter an already-running unit, and `UnitBackend.Start` issues `systemctl start`, which leaves that process running; it also reads the version from the symlink ([internal/activator/backend_unit.go:134](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_unit.go:134)).
+
+ **Suggested fix:** Require activation evidence before classifying an existing `NULL` route as public, just as for clearing `1`. A non-declaring installed manifest alone is insufficient. Keep the route refused until the execution layer proves that no declaring build remains, or proves it stopped with a non-declaring next-start version.
+
+2. **P2 — A sleeping unit-backed route cannot complete the transition back to public (§5.1).**
+
+ On an upgraded box, let an internal, unit-backed engine hibernate. It has no remaining group grant. Promote a non-declaring release without running a deployment watch.
+
+ Adoption repoints the sleeping route without waking it. The new clearing rule nevertheless requires the unit’s **current main process** to have started from the new version. There is no main process. The mark therefore stays `1`, and public requests are refused before they can wake the non-declaring release. Unlike the nested/exec rule immediately above it, the unit-backed rule has no stopped-instance alternative.
+
+ Adoption deliberately preserves sleep ([internal/release/adopt.go:1176](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/release/adopt.go:1176)). Unit-backed tenants have no scheduled wake and sleep until a request ([internal/activator/backend_unit.go:174](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/activator/backend_unit.go:174)); request-driven wake happens in the dispatch branch that §5.1 places after the refusal ([internal/edge/edge.go:1767](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-fleet-internal-engines/internal/edge/edge.go:1767)). The route needs an additional authenticated wake or operator intervention to escape this state.
+
+ **Suggested fix:** Add a unit-backed stopped-state proof: the unit has no remaining processes, its next-start version is non-declaring, and no group grant remains. Permit clearing on that proof without waking it.
+
+**Overall verdict: reject.** Initial classification can still expose a declaring process during upgrade. The new clearing rule also strands sleeping unit-backed routes.
\ No newline at end of file