carlos / platform Public

| Round 1 finding | Disposition | |---|---| | A1-1 — termination identity | Partly resolved. Signed instance documents fix account/region/instance verification. They do not authenticate the surrounding legacy label. The first registration still needs an enforced binding between the registering instance and that label; create-only storage prevents replacement, not an incorrect first registration. | | A1-2 — unpopulated generation | Partly resolved. Pinning and baseline creation are specified. The snapshot-only baseline has a replication-position defect: A2-1 below. | | A1-3 — destructive replay | Partly resolved. The no-reinstall boundary addresses ordinary replay. The new participant-replacement transition skips required earlier phases: A2-2. | | A1-4 — file ordering | Resolved. Immutable objects, ordered mutations, tombstones and conditional manifest publication establish the missing ordering. | | A1-5 — installation evidence | Resolved. The completion marker separates installation evidence from authority. | | A1-6 — participant/former rows | Partly resolved. Former-row removal and K11 are explicit, but the new tables omit the relocating source: A2-3. | | A1-7 — timer reconstruction | Partly resolved. Timer rows and catch-up are covered. App-provided routes.next_due remains outside that snapshot; moves §6.2 carries it separately. Replicate and restore that wake state too. | | A1-8 — unit/socket routes | Resolved. Explicitly excluded from relocation. | | A1-9 — multi-box admission | Resolved. Capability checks, the HA floor, executable recovery checks and unstamped-entry handling are specified. | | A1-10 — move target selection | Resolved. K10 binds the chosen target box in the start CAS. | | A1-11 — disappearing termination evidence | Partly resolved. The queue retains delivered events, but delivery is not guaranteed: A2-4. | | A1-12 — Describe permissions | Resolved. Supported region restrictions replace resource-tag authorization. | | A1-13 — citations | Resolved. The three corrections are present. All code citations were checked against d17c843a; references to proposed behavior were assessed as change locations. |

Reviewed spec rev 2 at d17c843a, against claim rev 6.3 (8faa89a4) and moves rev 7.5 (cdc98845). H1–H6 remain fixed. The later moves revision was inspected only to check the dependency defect below.

1. A2-1 — P1 — §5.8 installing; K8: a snapshot-only baseline does not establish the replication position. Location

Problem: The new generation receives a full database snapshot and manifest, without the level-0 state needed to continue replication from that snapshot’s transaction ID. Litestream v0.5.14 derives its remote position from level 0. This is also the defect addressed by the later moves rev 7.6, rather than the cited rev 7.5. Pinned library source.

Failing sequence: B installs a snapshot through transaction N into G′. With fresh replication metadata and no level-0 anchor, its subsequent uploads restart at transaction 1. B then terminates. A cold restore starts from the snapshot at N and skips those lower-numbered uploads, losing writes that had reached storage.

Fix: Require a verified replication-position baseline before installed, including the level-0 anchor used by the corrected moves contract. Update the dependency and K8. Test relocation → write → replicate → terminate → cold restore. The existing library reproducer covers the underlying failure; I inspected it but did not run it.

1. A2-2 — P1 — §5.8 participant-termination exits: early target replacement skips release and pinning. Location

Problem: Every target termination “before installed” resumes at installing using the same pinned set. That includes starting and releasing, when no pinned set exists and the source may still run.

Failing sequence: A→B enters starting; B terminates before A drains. The replacement transition selects C and jumps to installing. There is no recovery set to install. A correct implementation must stop there; proceeding by inventing a recovery set would also bypass A’s required stop evidence.

Fix: Make replacement phase-specific. Before source release, replace the target while preserving the release requirements. After release but before a durable pin, resume pinning. Only reuse an existing pinned set once it has been journaled. Carry these rules, including replacement participants’ execution leases, into K2.

1. A2-3 — P2 — §§5.3 and 5.8: reconciliation drops the current source during relocation. Location

Problem: §5.3 retains an executor’s ready row only when the operation is serving. Otherwise it retains only participants permitted a held row. The relocation table permits a held row only on to, including during starting and releasing.

Failing sequence: A serves a host. Its claim enters relocating/starting, still naming A as executor and permitting A to spawn. A’s next reconciliation matches neither retention case and drops its route. Requests fail before the intended drain, and the source loses registry state needed by the transfer.

Fix: Specify the source row throughout relocation: retain it while ordinary execution is permitted, then hold it before draining. Drop it only after its participant obligations allow removal. Make §5.3, the phase table and K11 agree.

1. A2-4 — P2 — §5.9: queue retention is treated as guaranteed termination capture. Location

Problem: EC2 state-change notifications reach EventBridge on a best-effort basis. Fourteen-day SQS retention protects events that arrive; it cannot recover an event that EC2 never delivered. AWS event reference.

Failing sequence: The sole box terminates, its notification is missed, and the replacement placer starts after DescribeInstances stops returning that instance. This happens within fourteen days, but neither observation method supplies evidence. The stated automatic recovery cannot proceed.

Fix: Explicitly define missing-event recovery immediately, rather than only after fourteen days. Assign durable capture/reconciliation and its availability boundary to spec 3, or state that this case requires operator resolution. Preserve the rule that absence is never fencing evidence.

1. A2-5 — P2 — §5.6: close/rename notifications do not provide the stated continuous-sync interval. Location

Problem: Publication is promised about one second after the last write, but the specified triggers are close and rename. A write to an open file produces a modification event; closing it is a separate event. inotify documentation.

Failing sequence: An app writes and fsyncs an existing file, then keeps its descriptor open without further writes. No close or rename occurs. The box terminates five minutes later, before the ten-minute scan. Continuous mode loses a change made minutes earlier.

Fix: Track modifications and impose a publication deadline independent of close. Specify recursive watch coverage, overflow recovery and how uploads obtain a consistent file image. Keep the periodic scan as repair rather than the normal path for open files.

1. A2-6 — P2 — §§5.6 and 6: create-only permissions conflict with manifest updates. Location

Problem: §6 describes writes to the files namespace as create-only using If-None-Match. §5.6 requires repeated If-Match replacement of manifest.json.

Failing sequence: The first manifest is created successfully. A file changes. Implementing §6’s restriction prevents replacing the existing manifest, so subsequent file and timer updates never become recoverable.

Fix: Separate immutable object/snapshot permissions from mutable manifest permissions. Specify create-only initialization and conditional replacement for manifests, while retaining create-only publication for content objects and box records.

1. A2-7 — P2 — §5.8: a live target with a permanently failing probe has no recovery exit. Location

Problem: After installed, recovery only advances through probing to serving. Replacement is defined only when a participant terminates. There is no bounded failure path for a live target whose probe cannot pass.

Failing sequence: A drains successfully. B installs, but its probe consistently fails because of a target-local launch problem. B remains healthy as a platform box, so it is not terminated. The host stays held indefinitely, and the claim prevents another relocation from starting.

Fix: Define a probe deadline and a journaled recovery or operator-resolution state. Transferring away from a live target must obtain stop evidence and preserve any probe writes from G′. Add that transition to K2; the later failover-loop specification does not supply this missing relocation exit.

Verdict: not ready.