carlos / platform Public

Clone
git clone https://amadan.net/carlos/platform

Plain git — no account needed to clone.

Download

Download this file

Fleet-internal engines, Plan 1: the simulation — Implementation Plan

> For agentic workers: REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (- [ ]) syntax for tracking.

Goal: A seeded model of spec rev 14's safety rules (invariant I1, the fence, the launch gate, the operator clear, the dedicated engine box, the call path's identity and grants), with a mutation harness proving that every rule is load-bearing, before any production code is written.

Architecture: A test-only package, internal/sim/engines, in the shape of internal/sim/hostlife: a deterministic world driven by a seeded RNG, named protocol rules that a mutation can switch off (ENGINESIM_MUTATE), invariants checked after every step, deterministic witness scenarios (one per Astra finding), and mutate.sh running one prebuilt test binary per rule. It imports nothing from production: it models the spec, so a finding here is a spec defect, fixed in the spec before Plans 2 to 5.

Tech Stack: Go standard library only (math/rand, testing), bash for the harness.

Spec: docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md (rev 14, approved 2026-10-21). Rulings R1 to R4 are in its §2.1.

The series

| Plan | Builds | Depends on | | --- | --- | --- | | 1 (this) | The model and mutation sweep | spec | | 2 | The internal mark: routes.internal, classification before serving, the edge's fence and box-wide epoch, the launch gate on every activator path, the internal refusal (:443, home :80), minted groups, --public, the dedicated-box rule, doc_engine excludes ports, deploy watch tickets | 1 | | 3 | Engine names and grants: console carlos engines, signed control/engines.json, the edge's grant mirror with the durable floor | 2 | | 4 | The call path: arming, the engine socket owner with the peer-cgroup check, the door transition and uid rule, the signed hop caller, engine-box admission (exact route, recheck, per-app cap), the engine transport and limits | 3 | | 5 | Docs, copy review, the rollout survey and runbook | 4 |

Plans 2 to 5 are written after this plan's sweep is green, because a rule the sweep cannot catch, or a violation it finds, changes the spec they implement.

Global Constraints

  • Test-only package: every file ends in _test.go (plus mutate.sh and the expected-outcomes file). No production package imports it; it imports no production package.
  • Deterministic: one seed gives one trace. No wall clock, no goroutines, no map iteration order in a decision (sort keys first).
  • Environment: ENGINESIM_SEEDS (sweep size; gate default 200), ENGINESIM_SEED (one seed, verbose trace), ENGINESIM_MUTATE (one rule or a comma-separated set), ENGINESIM_LIST=1 (print the rules a run would check), ENGINESIM_SCRATCH (default $TMPDIR/enginesim).
  • CPU budget on DOCS-T1: one 3000-seed mutation sweep per revision, serial, nice -n 19; 30k or more only on Paul's say-so. Scratch under $TMPDIR/enginesim, removed once after the sweep, never by pattern.
  • No t.Parallel() in the sweep or witness tests (package-level mutated is written by the harness's environment only, but witnesses read it).
  • Spec values the model uses: mirror poll 30 s, stale bound 10 min, record lifetime 72 h (as ticks: 1 tick = 10 s); fence wait bound 30 s; one internal group per engine box; engine names have no dot.
  • Rule names and invariant ids below are the vocabulary of Plans 2 to 5's test names; keep them exactly.

Review Focus

  1. A witness that passes for the wrong reason. Each witness must also run with no mutation and hold; a witness that violates unmutated is a model bug. (Task 6, TestWitnessesHoldUnmutated.)
  2. Actions the random walk never reaches. A rule guarding an action that no seed fires is untested however green the sweep looks. (Task 6, TestEveryActionFires: each action count > 0 over 200 seeds.)
  3. Residuals generated as if they were violations. The spec's three stated residuals (fresh-box replay, a declaring build with an unwritten manifest running across the upgrade, flat-era tampering) must not be generated by the default world, and a flag must generate each so a test shows it is counted as residual, not violation. (Task 5, TestResidualsAreCountedNotFailed.)
  4. Nondeterminism. A trace that differs between two runs of one seed makes every reported seed unreplayable. (Task 1, TestSeedDeterministic.)
  5. Availability rules invisible to safety invariants. Rules such as static-minted-public and owner-nonempty-unique only protect availability; without a liveness invariant their mutation is never caught. (Task 3, INV-AV.)

---

Task 1: The world, the step loop and the harness

Files:

  • Create: internal/sim/engines/world_test.go, internal/sim/engines/sim_test.go, internal/sim/engines/rules_test.go, internal/sim/engines/invariants_test.go

Interfaces:

  • Produces: - type build struct{ Ver int; Declares, ManifestOK bool } - type proc struct{ ID int; Group string; Ver int; Slice string; Unisolated, OwnPort bool } (Slice is the cgroup the peer check reads: inst:<group>, exec:<host>, unit:<host>) - type row struct{ Host, Kind, Owner, Backend string; Platform, Grant bool; PathTo map[string]string } (Kind is instance|service|static; Backend a socket path or address, "" for static) - type mark int with markNull, markPublic, markInternal - type req struct{ ID, Epoch int; Row, Backend string; Public bool; Caller *caller; Held bool } - type caller struct{ Account, App, Engine string } - type box struct{ ID int; Rows map[string]*row; Mark map[string]mark; Wrote, Fenced, Epoch int; ReloadFails, Armed bool; Live, Good map[string]int; Staged map[string][]int; Procs []*proc; Admitted []*req } - type world struct{ seed int64; rng *rand.Rand; boxes []*box; builds map[int]build; step int; trace, violations, residuals []string; stats map[string]int } - func newWorld(seed int64, verbose bool) *world - func runSeed(seed int64, verbose bool) *world - func (w *world) fail(inv, format string, args ...any) (records a violation once per invariant id) - func on(rule string) bool and var allRules []string (rulestest.go, the hostlife idiom: `ENGINESIMMUTATE read in init) - func (w world) group(b box, host string) string` (a row's group key: its owner for a minted instance row, else its own host)
  • [ ] Step 1: Write the failing tests in sim_test.go: TestSeedDeterministic (two runSeed(7, false) traces are equal), TestEngines (the sweep: ENGINESIM_SEEDS, default 200; one seed with ENGINESIM_SEED; reports violations per invariant with the first seed, hostlife's sweep shape), TestRulesListed (ENGINESIM_LIST=1 prints allRules one per line and runs nothing).
  • [ ] Step 2: Run go test ./internal/sim/engines/ -run 'TestSeedDeterministic|TestEngines|TestRulesListed' -count=1. Expected: FAIL, package has no world.
  • [ ] Step 3: Implement the types above, newWorld (two boxes: box 0 the engine's home, box 1 a calling box; one engine group eng with a minted platform row eng.acct.apps.example; one public app group shop on box 1; builds 1 to 4 with Declares and ManifestOK drawn per world), a step loop of 400 chaos steps then 200 calm steps choosing among registered actions (Tasks 2 to 5 register theirs in an actions slice), and final(). allRules starts empty; each later task appends.
  • [ ] Step 4: Run the same command. Expected: PASS (no actions yet, no violations).
  • [ ] Step 5: Commit enginesim: the world, step loop and sweep (#335 plan 1).

Task 2: The fence and the launch gate (I1)

Files:

  • Create: internal/sim/engines/launch_test.go, internal/sim/engines/edge_test.go
  • Modify: rules_test.go, invariants_test.go

Interfaces:

  • Consumes: Task 1's types, on, fail, group.
  • Produces: - func (w *world) launch(b *box, g string, ver int, path string) bool (path is one of adopt, swap, fallback, recovery, seed, cmd, systemd, socket; returns false when the gate refuses) - func (w *world) writeMark(b *box, g string, m mark) (bumps Wrote) - func (w *world) reload(b *box) (fails when ReloadFails; on success swaps the map, bumps Epoch on any 0→1, cancels every Admitted request with an older epoch, then sets Fenced = Wrote) - func (w *world) fenced(b *box, g string) bool - func (w *world) admitPublic(b *box, host, path string) *req (resolves alias, path map and minted row to the final row; refuses when that row's group is internal or NULL; else appends to Admitted) - func (w *world) deliver(r *req) (a held request resumes; records the process it reaches) - Invariants: INV-P (a public request is delivered to a process whose build declares doc_engine), INV-I1 (a declaring process exists while !fenced). - Rules: set-before-repoint, fence-needs-reload, fence-drains-admitted, fence-box-wide, gate-adopt, gate-swap, gate-fallback, gate-recovery, gate-seed, gate-cmd, gate-waits-when-written, unreadable-declares, live-link-only-adoption, mark-on-final-upstream. - Actions: adopt, reload tick, reload-fails toggle, public request (host, alias or path), hold and resume, wake with recovery or fallback to Good, swap, seed, cmd, systemd restart, socket activation. - Out of the model: deploy watch tickets (spec §5.8). A ticket request is authenticated, not public; Plan 2 tests its scope (GET or HEAD, / or the signed probe path, bound host and version) directly.
  • [ ] Step 1: Write the failing witnesses in witness_test.go (create it with hostlife's witness struct and TestWitnesses), one per rule, each a fixed sequence that violates the named invariant when its rule is off: - wSetBeforeRepoint (R2-1): adopt declaring build over a public route; a public request admitted between repoint and mark → INV-P. - wFenceDrainsAdmitted (R3-1): request admitted at 0, held across the adoption, resumed → INV-P. - wFenceNeedsReload and wGateWaitsWhenWritten (R10-1): reload failing, adoption times out with 1 written, recovery wake picks a declaring Good → INV-I1. - wGateFallback (R9-1): --public (stubbed here as writeMark(0) after stop) then a failed first wake falls back to declaring Good → INV-P. - wGateSwap (R7-1), wGateSeed, wGateCmd, wGateRecovery: a declaring build started by that path under 0 → INV-I1. - wUnreadableDeclares: a build with ManifestOK=false and Declares=true launched under 0 → INV-I1. - wFenceBoxWide (R13-2): a request admitted through a service row that is then deleted, held, resumed after a declaring launch → INV-P. - wMarkOnFinalUpstream (R1-2): a public request via an alias and via a path map to the engine → INV-P. - wLiveLinkOnly (R11): systemd restarts a unit whose live link was moved by something other than adoption → INV-I1.
  • [ ] Step 2: Run ENGINESIM_MUTATE=<rule> go test ./internal/sim/engines/ -run TestWitnesses -count=1 for one rule. Expected: FAIL to compile (no launch, reload).
  • [ ] Step 3: Implement the interfaces above. Each rule guards exactly one step of the mechanism in spec §5.1 ("The invariant", "Setting the mark"), and on(rule) false removes only that step.
  • [ ] Step 4: Run go test ./internal/sim/engines/ -count=1 (unmutated: every witness holds, the sweep is clean) and, for each rule, ENGINESIM_MUTATE=<rule> go test ./internal/sim/engines/ -run TestWitnesses -count=1 (its witness violates). Expected: as stated.
  • [ ] Step 5: Commit enginesim: the fence and the launch gate, I1 (#335 plan 1).

Task 3: Classification, minted groups and the operator clear

Files:

  • Create: internal/sim/engines/classify_test.go
  • Modify: rules_test.go, invariants_test.go, witness_test.go

Interfaces:

  • Consumes: Task 2's launch, writeMark, reload, admitPublic.
  • Produces: - func (w *world) upgrade(b *box) (every instance group to NULL, then classification before listeners: 1 if a grant in the group, the live build declares, or any staged build declares; 0 if the live manifest reads and none holds; else stays NULL) - func (w *world) operatorPublic(b *box, g string) bool (spec §5.1 steps 1 to 4: under the adoption lock, refuse if live declares or a grant remains; stop the group; refuse if any process of the group remains; write 0) - Invariant INV-AV (at the end of the calm phase, every row of a group whose mark is 0 answers a public request; liveness, checked in final() only). - Rules: classify-null-refused, classify-staged, minted-follow-owner, grant-marks-group, static-minted-public, owner-nonempty-unique, public-checks-live, public-stops-group, public-holds-lock. - Actions: upgrade, grant and revoke on any row of a group (minted included), operator clear, add a TCP-backed instance and its minted row, add a static app and its minted row and canary.
  • [ ] Step 1: Write the failing witnesses: wClassifyStaged (R8-1: an awake route repointed without a restart, upgraded → INV-P), wClassifyNullRefused (R2-2), wMintedFollowOwner (R5-1), wGrantMarksGroup (R6-1: grant on the minted row of a non-declaring release → INV-P via the minted host), wStaticMintedPublic (R6-2 → INV-AV), wOwnerNonEmptyUnique (R7-2: two TCP instances of one app → INV-AV with the rule off, ambiguous owner refused with it on), wPublicChecksLive, wPublicStopsGroup (R7-1/R8-2: generation still serving), wPublicHoldsLock (adoption repoints during the clear).
  • [ ] Step 2: Run the witnesses. Expected: FAIL to compile.
  • [ ] Step 3: Implement the interfaces above per spec §5.1 ("Platform-minted rows", "Becoming public is never automatic", "Classification before serving").
  • [ ] Step 4: Run unmutated (all hold, sweep clean) and each rule mutated against its witness (violates).
  • [ ] Step 5: Commit enginesim: classification, minted groups, the operator clear (#335 plan 1).

Task 4: The dedicated engine box and ingress

Files:

  • Create: internal/sim/engines/dedicated_test.go
  • Modify: rules_test.go, witness_test.go

Interfaces:

  • Consumes: Tasks 2 and 3.
  • Produces: - func (w *world) addServiceRow(b *box, host, backend string) (local or, on box 1, aimed at box 0's address) - func (w *world) directConnect(b *box, port string, public bool) *proc (models a connection that bypasses the edge; reaches a process only if the world's ingress precondition flag is violated or a ports listener exists) - Rules: ports-excluded, dedicated-launch-check, dedicated-edge-refusal, ingress-precondition (the world flag; its mutation lets direct connections through, showing the precondition is load-bearing). - Actions: add or delete a service row (local, remote), an engine binding its own port, a release declaring ports with doc_engine.
  • [ ] Step 1: Write the failing witnesses: wPortsExcluded (R11-1), wDedicatedLaunchCheck and wDedicatedEdgeRefusal (R12-2), wIngressPrivate (R13-1: a remote service row aimed at the engine's address with the precondition off → INV-P), wOwnPort (R12-1, same).
  • [ ] Step 2: Run the witnesses. Expected: FAIL to compile.
  • [ ] Step 3: Implement per spec §5.9 and §5.1 "The edge is the only ingress".
  • [ ] Step 4: Run unmutated and mutated as in Task 2.
  • [ ] Step 5: Commit enginesim: the dedicated engine box and ingress (#335 plan 1).

Task 5: Calls, identity, grants and arming

Files:

  • Create: internal/sim/engines/calls_test.go
  • Modify: rules_test.go, invariants_test.go, witness_test.go

Interfaces:

  • Consumes: Tasks 1 to 4.
  • Produces: - type record struct{ Rev, Expires int; Grants map[string]bool } (key account/app/engine) and type mirror struct{ Rec *record; Floor, ReadAt int; Persisted *record; PersistedFloor int }, added to box as Mirror mirror - func (w *world) publish(rev int), func (w *world) replay(rev int) (a bucket writer restores an older signed record), func (w *world) mirrorTick(b *box), func (w *world) restartEdge(b *box) - func (w *world) engineCall(from *box, p *proc, viaDoor bool, uid string, host, engine, path string) - func (w *world) launchUnisolated(b *box, kind string) bool (flat, foreign, worker; refused while armed), func (w *world) arm(b *box) bool, func (w *world) disarm(b *box) - Invariants: INV-G (an engine call reaches an engine route although the newest record the console published does not grant it, beyond the freshness bound, or reaches a route other than the engine's exact route), INV-ID (the caller the engine box records differs from the process's real group), INV-ARM (an unisolated tenant process exists on an armed box while an engine socket is open). - Rules: cgroup-identity, door-uid, hop-caller-signed, engine-box-recheck, exact-route-engine, floor-persisted, stale-clears-grants, armed-refuses-unisolated, arm-checks-box. - Residual flags (off by default, each with a test): freshBoxReplay, unwrittenManifestAcrossUpgrade, flatEraTamper; when on, the world records residual:<name> instead of a violation for the matching sequence.
  • [ ] Step 1: Write the failing witnesses: wCgroupIdentity (R1-1), wDoorUID (R2-3), wHopCallerSigned (a client-set caller header), wEngineBoxRecheck (G4: calling box table stale), wExactRouteEngine (R4-2: path map from engine A's host to engine B), wFloorPersisted (R1-4: revoke, replay older record, restart), wStaleClearsGrants, wArmedRefusesUnisolated (R3-2/R4-1: foreign and worker launches), wArmChecksBox; and TestResidualsAreCountedNotFailed (each flag on: residuals non-empty, violations empty).
  • [ ] Step 2: Run the witnesses. Expected: FAIL to compile.
  • [ ] Step 3: Implement per spec §5.2 to §5.4 and §6.2.
  • [ ] Step 4: Run unmutated and mutated as in Task 2, and the residual test.
  • [ ] Step 5: Commit enginesim: calls, identity, grants and arming (#335 plan 1).

Task 6: The mutation harness and the first sweep

Files:

  • Create: internal/sim/engines/mutate.sh, internal/sim/engines/expected-outcomes.txt
  • Modify: internal/sim/engines/sim_test.go, witness_test.go
  • Modify: docs/superpowers/specs/2026-10-21-fleet-internal-engines-design.md (§8: the sweep result)

Interfaces:

  • Consumes: every rule and witness from Tasks 2 to 5.
  • Produces: mutate.sh <seeds> [rule|rule,rule|@all], hostlife's verdicts (CAUGHT, MISSED, ERROR, EXPECTED-MISS, STALE) with the ENGINESIM_ variables; expected-outcomes.txt in hostlife's format.
  • [ ] Step 1: Write the failing tests: TestWitnessesHoldUnmutated (every witness passes with mutated == ""), TestEveryActionFires (over 200 seeds every registered action's stats count is above zero), TestEveryRuleHasWitness (each name in allRules has a witness or an expected-outcomes.txt line).
  • [ ] Step 2: Run go test ./internal/sim/engines/ -count=1. Expected: FAIL until the harness file and coverage hold.
  • [ ] Step 3: Implement mutate.sh by adapting internal/sim/hostlife/mutate.sh (same build-once, run-per-rule shape, ENGINESIM_ names, scratch $TMPDIR/enginesim), and fill expected-outcomes.txt only for rules a reason makes uncatchable alone.
  • [ ] Step 4: Run the sweep once, serial and niced: go test -c -o "$TMPDIR/enginesim/engines.test" ./internal/sim/engines/ && nice -n 19 internal/sim/engines/mutate.sh 3000. Expected: every rule CAUGHT or EXPECTED-MISS, no MISSED, ERROR or STALE; the unmutated sweep at 3000 seeds has no violation. Remove $TMPDIR/enginesim afterwards.
  • [ ] Step 5: Record the verdict table in spec §8 under "Simulation" (rules, verdicts, first seeds, the date), and if any rule is MISSED or the unmutated sweep fails, stop: write the defect up on #335 and bring it to Paul before Plan 2.
  • [ ] Step 6: Commit enginesim: mutation harness and the first 3000-seed sweep (#335 plan 1).