amadan
spec: fleet-internal engines rev 13 (Astra R12; Paul's rulings R3 dedicated engine box, R4 review end)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+64
−1
docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md+64 −1
CI cancelled — superseded by a newer push — run details
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 e3de15036..82641b100 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,15 @@ |
| # Fleet-internal engines: a doc engine nobody on the internet can call |
| **Date:** 2026-10-21 |
| -**Revision:** 12. |
| +**Revision:** 13. |
| **Discussion:** amadan carlos/platform #335. Related: #328 (per-app egress allow). |
| +- **Rev 13** answers Astra round 12 (`CODEX-FINDINGS-ENGINES-R12.md`, |
| + reject, two P1s: an engine binding its own high port, and a separate |
| + public route row pointing at the engine's backend) with Paul's ruling R3: |
| + an engine's home box is dedicated, and the platform enforces it (§5.9). |
| + Ruling R4 sets the review end: one more round, then Paul's read. Marked |
| + **(codex R12-n)**. |
| - **Rev 12** answers Astra round 11 (`CODEX-FINDINGS-ENGINES-R11.md`, |
| reject, one P1: a declaring release that also declares `ports` keeps a |
| granted TCP listener the edge never sees). `doc_engine` and `ports` are |
| @@ -159,6 +165,12 @@ address opened in its fence. |
| socket or door first (§7). |
| - **R2. Unit-backed apps are not callers in this spec.** Later, if a caller |
| appears. |
| +- **R3. An engine's home box is dedicated, and the platform enforces it** |
| + (§5.9). Public ingress beyond the edge's own ports is a stated box |
| + precondition, not a platform-installed firewall. |
| +- **R4. Review end:** one Astra round on rev 13, small fixes, then Paul's |
| + read. The plan's first task is a simulation of I1 and §5.9 across every |
| + launch and ingress path. |
| ## 3. What exists today, and what this builds on |
| @@ -663,6 +675,45 @@ everywhere else, where the watch proceeds exactly as today: |
| document: the probe paths are the app's own choice, and Gotenberg's |
| `/health` is a fine probe. |
| +### 5.9 The engine box is dedicated (codex R12-1, R12-2; ruling R3) |
| + |
| +I1 keeps a declaring build from starting before the edge refuses the |
| +public, but the edge is not the only way to a process on its box. Round 12 |
| +found two others: the engine binding a port of its own on every interface |
| +(the template allows it, `carlos-app@.service:21`, `:66`; the capability |
| +validator leaves high ports to the app, `caps/caps.go:401`), and another |
| +route row whose upstream is the engine's backend (`carlos add` with a |
| +`service` kind and an explicit address, `cli.go:126`, `:276`; the edge |
| +proxies by that row's own address, `edge.go:760`, `:889`, `:1790`). The |
| +README already tells operators to run a doc engine on a box of its own. |
| +This spec makes that a rule the box enforces: |
| + |
| +- **One internal group per box, and nothing else that proxies.** On a box |
| + that homes an internal group, every route row whose upstream is a local |
| + process (any `instance`, `service` or sidecar row: a socket path or an |
| + address) must belong to that group. Rows the edge answers without a |
| + local process (`static`, the status host, the tunnel and steering |
| + handlers) are unaffected. |
| +- **The launch gate checks it.** Before it waits for the fence, a declaring |
| + launch confirms the rule holds on the box. If any other proxying row |
| + exists, the launch is refused (the wake fails), and one line per pass |
| + names each offending row. |
| +- **The edge keeps it.** While an internal group is homed on the box, the |
| + edge refuses to serve any proxying row outside the group: it gets the |
| + internal refusal, and the pass logs it with the move or remove command. |
| + A row placed on the box later (provisioning, a move, `carlos add`) is |
| + therefore never served there; the engine keeps running. |
| +- **Ingress precondition, stated (ruling R3).** The engine's box admits |
| + public connections only on the edge's ports (80 and 443, plus whatever the |
| + operator keeps for administration), by its security group or host |
| + firewall. The platform cannot see that boundary from inside the box. The |
| + rollout survey (§7) checks it for every engine box, and the README's |
| + doc-engine preconditions gain it as a third, beside the loopback resolver |
| + and the dedicated box. |
| + |
| +With the box dedicated, a port the engine binds on its own can be reached |
| +only through that firewall, and no other row on the box can point at it. |
| + |
| ## 6. Correctness rules |
| ### 6.1 Identity |
| @@ -750,6 +801,10 @@ so a revoke is in force once either has read it. |
| ## 7. Deploy order and rollout |
| +- **Engine boxes.** For each box that will home an engine: confirm its |
| + public ingress is the edge's ports only (security group or firewall), and |
| + move every other app off it. The launch gate refuses a declaring build on |
| + a box that still has one. |
| - **Survey first.** On dev and the flagship, list every route whose live |
| release declares `doc_engine` or holds the grant, and who calls it. A |
| route with public callers is cut off the moment its home box takes this |
| @@ -834,6 +889,10 @@ process, real unix sockets and a real cgroup check where the kernel allows |
| `ports`; a box with an existing port grant on a route that becomes |
| internal removes the listener before the fence completes, and a direct |
| connection to the port is refused afterwards. |
| +- On a box homing an internal group, a `service` row pointing at the |
| + engine's address, or any other app's instance, gets the internal refusal; |
| + a declaring launch on a box that has one is refused; static and status |
| + rows keep serving. |
| - 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; |
| @@ -898,6 +957,8 @@ it, not only over a private network. |
| 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. |
| +- One internal group per box, enforced: a second engine needs a second |
| + box. |
| - Unclassified routes are refused publicly (fail closed) even though that |
| can make a route with no readable manifest unreachable while the bucket |
| is down. |
| @@ -945,3 +1006,5 @@ it, not only over a private network. |
| | 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) | |
| | R11-1 a granted port bypasses the edge | Accepted: `doc_engine` + `ports` refused at ship; no listener for internal groups (§5.1) | |
| +| R12-1 an engine binds its own public port | Ruling R3: dedicated box; ingress beyond the edge's ports is a stated, surveyed precondition (§5.9) | |
| +| R12-2 a separate service row proxies to the engine | Ruling R3: no proxying row outside the group on an engine's box, enforced by the launch gate and the edge (§5.9) | |