amadan
Astra joint round 2 findings (claim bf61e6a9 + moves rev 5 4ec3282b + model 7a3e94e7), unedited
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+208
−0
docs/superpowers/specs/CODEX-FINDINGS-JOINT-R2.md+208 −0
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R2.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R2.md| new file mode 100644 |
| index 000000000..e411ff3e7 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R2.md |
| @@ -0,0 +1,208 @@ |
| +**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: |
| + |
| +```text |
| +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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](https://docs.aws.amazon.com/AmazonS3/latest/API/API_CopyObject.html). |
| + |
| +The model assumes completion within `H`, then further protects restore with exact `BaseVer` and historical lineage selection at [protocol_test.go:178](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:222).** |
| + |
| +Release adoption and config work also run through separate root commands: [carlos-adopt.service:17](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/units/carlos-adopt.service:17) and [carlos-config-sync.service:25](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/units/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/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. |
| \ No newline at end of file |