amadan
spec: region HA spec 1 rev 5.1, Astra round 2 findings (unedited)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+77
−0
docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-REV5-2.md+77 −0
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-REV5-2.md b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-REV5-2.md| new file mode 100644 |
| index 000000000..c28fc03e8 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-REV5-2.md |
| @@ -0,0 +1,77 @@ |
| +| Prior finding | Disposition | Answer in rev 5.1 | |
| +|---|---|---| |
| +| B1-1 | **Resolved** | §5.8 selects each probe’s database predecessor through `genselect.Select`; L9 limits `released` to the matching source session. | |
| +| B1-2 | **Partly resolved** | §5.8 requires replacement-local installation, but subsequent probe stamps invalidate its receipt without a safe replay rule. Finding 5 below. | |
| +| B1-3 | **Partly resolved** | §5.9 adds holds and removed-volume accounting, but release can precede completion of authorized mutations. Finding 2. | |
| +| B1-4 | **Partly resolved** | §6 protects direct tag changes and disables unattested fencing. Another volume-replacement API remains unguarded, and the attestation conflicts with Auto Scaling’s permissions. Findings 1 and 3. | |
| +| B1-5 | **Resolved** | §5.10 retains exclusion for `lost`, unreadable records and unfinished cleanup until D6 clearing. | |
| +| B1-6 | **Resolved** | §5.8 defines source-loss conversion from both `starting` and `releasing`, preserving the target’s acknowledgement requirement. | |
| +| B1-7 | **Resolved** | §5.9/L5 binds console enrollment to compute and excludes fenced consoles. H18/L20 scopes stale-report acceptance to box-started relocation with matching floor enforcement. | |
| +| B1-8 | **Partly resolved** | §5.1/L19 supplies a cross-region confirmer, but its eligibility condition remains circular after the last box dies. Finding 6. | |
| +| B1-9 | **Resolved** | Active code citations were refreshed; historical disposition anchors are identified as historical. | |
| + |
| +Reviewed `fdc0fe07` against claim `98b45332`, moves `a4711728`—the latest committed spec in the supplied worktree—and code at `origin/main` `09814f7f`. H1–H18 and claim R6 are treated as fixed. |
| + |
| +1. **P1 — Root-volume replacement bypasses the destroyed-disk guard.** |
| + |
| + **Section:** [§6, lines 1200–1211](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:1200), with §5.9’s removed-volume detection. |
| + |
| + The deny covers `ModifyInstanceAttribute`, `AttachVolume` and `DetachVolume`, but not `CreateReplaceRootVolumeTask`. That separate API replaces a running instance’s root disk and can retain the original volume. Its authorization does not require the three denied actions. [AWS API contract](https://docs.aws.amazon.com/AWSEC2/latest/APIReference/API_CreateReplaceRootVolumeTask.html), [EC2 authorization reference](https://docs.aws.amazon.com/service-authorization/latest/reference/list_ec2.html). |
| + |
| + **Failing sequence:** A valid record lists root volume V with `DeleteOnTermination: true`. A principal permitted to replace root volumes replaces V while retaining it, without creating a hold. The instance terminates before the next volume observation. The old record still satisfies the two-hour bound; no removal was recorded; the fence discharges local retirement although V survives. |
| + |
| + **Suggested fix:** Include root-volume replacement in the protected mutation paths and the hold workflow. Test this exact sequence, including preservation of the old volume, rather than testing only the three enumerated APIs. |
| + |
| +2. **P1 — Releasing a hold does not close the authority to mutate volumes.** |
| + |
| + **Section:** [§5.9, lines 969–987](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:969), §6. |
| + |
| + Release requires an all-true observation after the hold, but no durable completion state for the change, no reconciliation of outstanding requests, and no closure of the role session. Requiring a session tag establishes neither an existing hold nor its continuing applicability; tags are caller-supplied session attributes. [AWS session-tag contract](https://docs.aws.amazon.com/IAM/latest/UserGuide/id_session-tags.html). |
| + |
| + **Failing sequence:** Change H creates its hold and obtains credentials. A concurrent release sees an all-true record written after H and releases it. Another all-true record arrives after release. The still-authorized change process then detaches a volume, or completes an outstanding detach. Termination before the next sweep produces a qualifying fence despite the surviving disk. |
| + |
| + **Suggested fix:** Give changes a durable closing protocol. Bind mutation authority to the exact enrollment and hold; prevent further requests and account for outstanding mutations before release. Require the validating observation after that barrier, not merely after the hold’s creation. |
| + |
| +3. **P1 — The required guard attestation cannot pass for the specified Auto Scaling deployment.** |
| + |
| + **Section:** [§6, lines 1217–1228](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:1217), §8’s rollout gate. |
| + |
| + The attestation requires verification that no service-linked role can modify running instances’ volumes. Auto Scaling’s service-linked role has unrestricted `ec2:ModifyInstanceAttribute` and `ec2:CreateReplaceRootVolumeTask`, as well as tag mutation permissions. SCPs do not restrict service-linked roles, and Auto Scaling’s role permissions cannot be edited. [Managed policy](https://docs.aws.amazon.com/aws-managed-policy/latest/reference/AutoScalingServiceRolePolicy.html), [role restrictions](https://docs.aws.amazon.com/autoscaling/ec2/userguide/autoscaling-service-linked-role.html). |
| + |
| + **Failing sequence:** Spec 4 creates an Auto Scaling group and its required service-linked role. The attestation workflow examines that role and cannot establish §6’s condition. Consequently, automatic fencing and the multi-box gate remain disabled. |
| + |
| + **Suggested fix:** Specify an attainable proof covering service-mediated mutations: identify the service workflows and initiating APIs that can change disks or protected tags, and constrain or hold-gate them. Include Auto Scaling’s actual managed policy in the guard validation. A blanket assertion that no such service-linked permission exists cannot authorize this design. |
| + |
| +4. **P1 — Database-baseline selection can discard files already published by an unfinished session.** |
| + |
| + **Section:** [§5.6, lines 567–579](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:567), §5.8’s pinned recovery set. |
| + |
| + Files are selected from the same generation as the database baseline. However, the two publishers can make independent progress. `genselect.Select` examines database-generation prefixes; files under `files/<generation>/` do not make that database generation nonempty. |
| + |
| + **Failing sequence:** P is published. A later probe admits Q, copies P’s files manifest, and starts the app. Q successfully publishes a changed file and its manifest while its first database upload is delayed. The target terminates. Selection correctly falls back through the unfinished database run to P, but §5.8 consequently pins P’s older files manifest too. Q’s acknowledged file update is omitted and can later be retired. |
| + |
| + **Suggested fix:** Define files-manifest selection independently across the admitted predecessor chain, journal its exact identity alongside the database pin, and protect its referenced objects through publication and retirement. Test a durable files update followed by termination before the session’s first database upload. |
| + |
| +5. **P2 — Probe retries invalidate the local-install receipt without defining safe recovery.** |
| + |
| + **Section:** [§5.8, lines 753–788](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:753), replay rules at lines 829–835. |
| + |
| + A receipt counts only for its recorded `holder.stamp`. Later probe admissions deliberately change that stamp. Replay nevertheless calls for local installation when there is no valid receipt, and that installation applies P’s files and wake state. |
| + |
| + **Failing sequence:** The target installs P and records receipt S. A second admission creates Q with stamp S2, publishes Q, and changes files. The agent crashes during probing. Receipt S no longer qualifies. Recovery has no specified way to validate installation at S2 except remaking it from P, which can revert files and timers; P may also already be queued for retirement. |
| + |
| + **Suggested fix:** Separate initial installation provenance from subsequent writer stamps. Explicitly preserve or advance that provenance across admissions. Once probing has admitted a writer, recovery must not reapply the original prepared files; any reconstruction must use the current recovery lineage. |
| + |
| +6. **P2 — H17’s bootstrap condition still excludes an emptied region whose dead box remains enrolled.** |
| + |
| + **Section:** [§5.1, lines 322–351](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:322), §5.9 lines 1085–1088, §7. |
| + |
| + Cross-region confirmation requires zero `active` roster entries in the target region. Termination does not itself change that roster state: the console retires the entry only after a regional worker writes its fence. |
| + |
| + **Failing sequence:** A region’s sole active box A terminates before another worker fences it. Auto Scaling launches B. A remains `active`, so the cross-region confirmer and console refuse H17 confirmation. B cannot enroll and become the regional worker that fences A. The console cannot retire A through the specified fence path. |
| + |
| + **Suggested fix:** Define a bootstrap-specific empty-region check using positive terminal-state evidence for the remaining enrollments, as part of H17 confirmation. Permit the replacement’s enrollment before local disk fencing; leave the termination fence and host relocation to the newly enrolled regional worker. Do not substitute heartbeat expiry for that evidence. |
| + |
| +No files were changed or tests run. |
| + |
| +**Verdict: not ready for plan.** |
| \ No newline at end of file |