carlos / platform Public

A, B and C are not ready to support Phase 1 implementation planning. The revisions resolve many round-1 findings, but several remaining safety and recovery gaps are hidden by stronger or more atomic behavior in the model.

I read AGENTS.md first and reviewed the requested revisions with three independent GPT-6 reviewers; Opus was unavailable. The worktree matches B at 4ec3282b and C at 7a3e94e7. Nothing was changed.

Both requested test commands failed before compilation:

go test ./internal/sim/hostlife/ -count=1
HOSTLIFE_SEEDS=30000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1

go: creating work dir: mkdir /home/paulca/.cache/tmp/go-build…: read-only file system

The conclusions below are therefore static-review findings, not reproduced failing seeds. I inspected mutate.sh but could not independently confirm its published counts.

1. Round-1 dispositions

“Resolved” means the specific contract or modeled behavior is addressed—not that implementation correctness is established. Model dispositions include fidelity to the specified behavior.

| Finding | Spec | Model | Why | |---|---|---|---| | D1: box/phase admission | Resolved | Resolved | A C4 and B §19.1 require exact executor and phase; model implements these, although role and executor checks are combined. | | D2: revision versus generation | Resolved | Resolved | Claim revision is separate from installed operation/incarnation identity. | | D3: reconstructible stop evidence | Resolved | Partly | A §6.1/B §5.3 require containment and draining; model atomically removes known processes without spawn-in-flight, descriptor or cleanup-failure states. | | D4: staging permissions/exclusion | Partly | Partly | Shared lease and version seal address the original race; timing proof remains incomplete, and model lease acquisition does not exclude workers of the same operation. | | D5: retirement-event identity | Resolved | Resolved | Separate retirement IDs prevent initial-target, failed-target, source and staging manifests colliding. | | D6: independent execution fencing | Resolved | Partly | Compute fencing replaces lease expiry; model represents verification as a Destroyed Boolean, omitting cloud-identity/proof handling. | | D7: transitions and recovery writer | Partly | Partly | B §7.5 lets the source complete target handoff; K4 still reserves that transition to the receiving participant. Model also uses a different claim/record ordering. | | D8: obligations block release | Resolved | Resolved | Operation-owned obligations block serving release; all obligations block free. | | I-7: local retirement inventory | Resolved | Partly | A §6.3 names flat siblings and nested state; model clears aggregate fields without path-level retirement or durability steps. | | N1: late storage completion | Partly | Partly | Version deletes are sound; source-version copies do not fence destinations, and request completion within H is assumed by the model. | | N2: delayed staging rounds | Partly | Partly | Forward seals address content corruption; cleanup depends on timing assumptions. Return-lane paused signers are not modeled. | | N3: declare-lost double writer | Resolved | Partly | Compute fencing and quarantine address the original failure; external fencing verification remains abstract. | | N4: cross-object transaction gaps | Partly | Partly | Durable intent helps, but late create publication is unspecified and the model collapses/reverses B’s record/claim transactions. | | N5: incomplete legacy discovery | Partly | Partly | Remote replica acknowledgements set complete=true without discovering historical local files; the model never seeds that local residue. | | N6: parking live coordination locks | Resolved | Resolved | Live locks are excluded from manifests, emptiness checks and subsequent retirement scans. | | N7: same-operation manifest collision | Resolved | Resolved | Per-retirement destinations address the collision. | | N8: stale config/adoption writers | Partly | Partly | An in-process guard cannot cover separate root commands; model lacks operation and config-version identity for delayed writes. | | N9: purge teardown ordering | Partly | Partly | Reservation precedes teardown, but reservation checking and create admission are not serialized across objects. | | N10: stalled door reads | Partly | Partly | Version handles protect a stalled open; authorization-to-version-selection remains a separate unprotected interval. | | N11: pre-flip recovery rechecks its writes | Resolved | Resolved | Durable recovery phases prohibit baseline verification after entering probing. | | N12: automatic old-binary restoration | Resolved | Partly | Automatic recovery and rollout ordering are covered in prose; model uses a Boolean floor rather than enrollment and executable activation paths. | | N13: abort actor lacks permissions | Resolved | Resolved | Target-region actor owns staging retirement; M17 remains push-only. | | N14: timer runner’s prune | Resolved | Resolved | Canonical digests exclude completed history while preserving active timer state. | | N15: cut budget | Partly | Partly | Deadline now bounds commit, not the promised stop-to-open interval; T11 also budgets one settle despite permitting retries. |

For N5 specifically, A §9’s new completion rule defeats its own fallback: once foreign bucket obligations finish, §5.2 no longer requires every box to acknowledge. An old box’s database, key or sibling env files can remain unretired when the host becomes free.

2. Model fidelity

| Abstraction | Fault it can hide | Concrete model change | |---|---|---| | Permissions checked on modeled mutations; reads/listings access maps directly | A worker depends on a read or listing its credentials cannot perform | Route Get, Head, ListVersions, control-bucket access and copy-source reads through principal-aware APIs. | | Exact base-version pointer plus historical LTX selection | Actual prefix restore selects a stale current object after a late destination write | Represent real replica keys, regional generation markers and the actual restore-selection algorithm. | | Every request completes by issue + H | An accepted request completes after retirement has acknowledged | Separate signing, server acceptance, timeout and completion; allow completion beyond H unless an enforced bound exists. | | Check/sign and check/local-write are atomic | A process pauses after authorization or lease validation, then acts after revocation | Split these into independently scheduled events, including independent root processes. | | Replica “lease acquisition” is unconditional PUT; staging lease accepts the same op | Two same-operation workers execute conflicting work simultaneously | Give each worker a lease identity and model conditional acquire, renewal, expiry and release. | | Claim transitions followed immediately by fixRecord | Crashes between B’s record-first transition and claim update are missed | Model both objects, conditional writes, ambiguous responses and recovery in B’s specified order. | | Atomic localPark | Crash between rename, journal, directory fsync and acknowledgement loses replay information | Represent individual artifacts and durability barriers; inject crashes between them. | | Complete map listings | A failed/truncated/paginated inventory is treated as complete | Model pages, continuation tokens, failures after successful pages, and mutations between pages. | | Fixed clock skew; one global time | Clock steps or pause margins invalidate signing horizons and cross-box deadlines | Separate service time, wall time and monotonic time; exercise clock adjustment and post-check pauses. | | Old executable is a Boolean fault | Old console, stale enrollment report or pre-floor updater bypasses the floor | Model enrollment and distinct console, agent and boot-updater versions and activation decisions. | | Config is an incarnation integer; first failed probe never creates a process | Same-incarnation config changes and writes before first readiness failure disappear | Track bundle/release/environment versions; separate spawn from readiness success/failure. |

Two additional scope gaps matter:

• One host prevents testing purge’s multi-host enumeration and admission protocol.
• Return staging bypasses the forward path’s lease and stalled-signer machinery at moves_test.go:808, and uses now + H rather than the forward staging horizon.

The time scaling also reverses an important relationship: model H=60 is shorter than cutBudget=320; production H exceeds fifteen minutes while the default cut budget is 120 seconds. Successful schedules in one configuration cannot establish the other’s timing behavior.

Mutation results: useful, but not trustworthy as protocol-wide proof.

• 37 caught alone: plausible evidence that these switches affect this model. The counts are unverified here, and some detections are non-convergence rather than the claimed safety failure.
• 9 with partners: useful interaction evidence, but additional failing seeds do not by themselves establish which guard prevented which fault. Preserve and compare minimized traces.
• 2 liveness-only: supported only within the represented state space. In particular, configuration is too coarse to establish a general claim about real config failures.
• The admission/hold/start-check triple: materially misleading. Its third fence is stronger than B specifies; finding R2-8 below explains why.
• restore-lineage-filter: correctly described as adding no detection beyond its partner. That is unproven protection, not proof of redundancy.
• readiness-quiet: its unreachability is credible under the encoded ordering: acknowledgements already wait for the horizon and conflicting obligations block new operations. It does not validate the horizon itself.
• Harness classification: build failures and timeouts can be counted as CAUGHT; finding R2-10 below prevents accepting the summary without underlying logs.

3. New failure traces and model defects

These include failures in the proposed round-1 remedies. They do not reopen M1–M18.

R2-1 — P1: storage fencing remains incomplete at the destination and completion boundary. A C3/§6.2a; B §§6.4, 7.6, 15.

A copy naming an exact source version still creates a new destination version. Consider an accepted install-copy request whose client times out: a retry succeeds, the operation advances, and the earlier request completes after retirement or namespace reuse. The source-version condition does not protect the destination.

The proposed horizon does not yet exclude that schedule. The 14/16-minute experiment tests whether S3 accepts an old signature, not how long an already accepted operation may continue. AWS also distinguishes copy acceptance from completion and provides separate destination conditions. AWS CopyObject documentation.

The model assumes completion within H, then further protects restore with exact BaseVer and historical lineage selection at protocol_test.go:178. B specifies neither that persistent restore pointer nor that selection algorithm.

Fix: define destination-side fencing or immutable generation identities and the corresponding restore contract. If correctness still depends on H, establish an enforceable server-completion bound covering every request type; client timeout is insufficient. Model destination writes after publication and retirement.

R2-2 — P1: purge can miss a creator already past its reservation check. A §§5.1–5.3; console_test.go:76.

A creator reads “no purge reservation” and pauses. Purge reserves the app, enumerates its hosts and claims them. The creator then claims a previously unused hostname and publishes its record while purge tears down stores or deletes the app prefix.

The reservation check and host CAS concern different objects. The model performs both atomically inside userCreate.

Fix: register in-flight creators through an app-level admission protocol. Purge must close admission and drain or reconcile those creators before fixing its host set and beginning teardown. Test at least two hosts.

R2-3 — P1: the local host guard excludes only threads in one process. A §6.4; background_test.go:222.

Release adoption and config work also run through separate root commands: carlos-adopt.service:17 and carlos-config-sync.service:25.

One process can validate, pause, then write an old env file or release pointer after another process retires or holds the host. An in-process mutex cannot serialize them. A’s cached-admission wording further conflicts with C4.

Fix: use a guard shared by all relevant OS processes, with fresh durable incarnation/operation checks under it. Include the selected config/release identity. Model independent processes and pauses between validation and the filesystem mutation.

R2-4 — P1: pinning the door’s read leaves authorization-to-version-selection exposed. A §6.5; console_test.go:436.

The console authorizes a listing for incarnation A, then pauses before resolving object versions. The host is deleted and recreated for B. The listing resumes and signs a handle for B’s current version. Opening that exact version preserves the wrong authorization decision.

The model selects versions atomically with authorization and filters on an incarnation tag that ordinary legacy LTX objects need not have.

Fix: bind authorization and version selection to the same holder/operation observation—for example, validate the claim around selection and reject if it changed. Sign the selected identity and authorization scope. Inject the pause before version selection, not only before object open.

R2-5 — P1: a config update can make automatic rollback permanently fail. B §§7.6–7.8, 9.1.

Admission pins bundle V1. A normal config/secrets update publishes V2 after the cut. Target configured rejects the changed ETag and starts rollback. Source recovery also renders current configuration, but every recovery probe must satisfy the pinned V1 inputs. Each retry encounters the same mismatch.

No specified mechanism preserves/render-selects V1, serializes its publication, or authorizes a recovery-specific replacement. Model assignments such as moves_test.go:892 cannot represent V1 versus V2.

Fix: choose one complete policy for updates during a move and for recovery: durable pinned inputs, serialized publication, or explicitly validated recovery inputs. Test a change after admission and after a writable probe.

R2-6 — P2: A’s park manifest cannot replay its stated deletion set. A §6.2 steps 2–7; protocol_test.go:379.

A selects/copies current versions and records those copies, then requires deleting noncurrent snapshot versions too. After a crash, retry knows only the manifest’s recorded versions. Historical data behind a delete marker is particularly ambiguous.

B §6.4 and the model instead snapshot every version; the model archives every non-marker version. They validate a different algorithm.

Fix: persist separate archive and deletion sets, including the policy for delete markers, or explicitly adopt all-version archiving in A. Test crashes after manifest publication with several historical versions and a marker at the head.

R2-7 — P2: create recovery can free the claim before record publication completes. A §5.1 step 5 and §8; console_test.go:498.

Recovery observes an absent record and frees the creating claim. An earlier submitted record PUT completes afterward. Admission refuses the orphan, but the record also blocks ordinary recreation; A supplies no explicit replay rule for removing it safely.

The model’s record creation is synchronous, and its recovery pass contains additional orphan deletion absent from A’s operation table.

Fix: specify publication/cancellation recovery, including conditional orphan cleanup or roll-forward from durable intent. Model late control-bucket writes and ambiguous responses.

R2-8 — P2: the advertised third admission fence does not exist in B’s start check. B §§5.1, 14.2.5; background_test.go:77.

After target commit, before source retirement, the source’s old DB marker, files marker and source-region bucket marker still agree. That satisfies B’s specified start check.

The model instead compares the source with the globally committed target lineage, updated at moves_test.go:658.

Thus, with only exec-admission and hold-op-open removed, a delayed open can make the source ready and let it wake beside the target under B’s rules. The model invents a third barrier and requires the triple mutation.

Fix: model regional generation markers faithfully and run the pair against this exact schedule. Correct the redundancy claim, or explicitly add a global committed-generation check to the protocol. The unmutated admission/open protections still prevent this trace.

R2-9 — P2: the final cold-restore check repairs storage before checking it. sim_test.go:290.

Before cold restore, the checker directly writes the complete surviving local DB into the bucket. A missing or stale replica can therefore pass because the checker just supplied the missing data.

Moreover, write-loss checks run only for the final holder. A bad move followed by deletion/recreation can escape that final assertion.

Fix: check storage at explicit promised durability boundaries without modifying it. Check each terminal operation before a later deletion can erase the evidence. Exercise cold restart with local state unavailable after a completed checkpoint.

R2-10 — P2: mutation infrastructure errors count as detections. mutate.sh:40.

Any nonzero Go exit becomes CAUGHT, including compilation failure, read-only cache failure and timeout. MISSED also does not make the sweep fail.

Fix: count only a parsed invariant violation with a reproducible seed as detection. Classify infrastructure failures as errors, preserve logs, and fail the sweep on errors. Declare expected redundant/liveness-only outcomes separately.

There are no additional material P3 findings.

4. Verdicts

| Artifact | Ready for Phase 1 planning? | Reason | |---|---|---| | A — claim rev 3.1 | No | Purge/create admission, cross-process local exclusion, authorization/version selection, legacy local coverage and storage-completion guarantees remain incomplete. | | B — move rev 5 | No | Inherits A’s blockers; config-update recovery is incomplete; record/claim ordering and handoff authority remain inconsistent; the cut promise still differs from the enforced deadline. | | C — model | No, as the planning gate | Useful for finding faults, but stronger restore/admission behavior, atomic transaction boundaries and a repairing final oracle prevent its green results from validating the specified protocol. |

The next round should begin with deterministic regressions for these traces, faithful record/claim and regional-marker behavior, and a corrected mutation harness. Then rerun the seed sweep. Increasing seed counts alone will not exercise states the model cannot represent.

---

FIRST PROMPT: Joint independent, read-only round-2 review of the two specs and executable model.

WHAT: Assess prior fixes, model fidelity, new faults and Phase 1 readiness.

STATUS: Review complete. All three verdicts are not ready. Go execution was sandbox-blocked.

NEEDED: Nothing for this review.

RECOMMENDED: Resolve the protocol gaps and model mismatches, then rerun deterministic regressions and mutations.

SESSION: Safe to close. No files changed; nothing remains running.