| 1 | Reviewed `2af4eba4`. No files modified; no tests run. |
| 2 | |
| 3 | 1. **R4-1 — P1 — §7.2: G2 does not hold across `DirStore` handles sharing a directory.** |
| 4 | |
| 5 | The mutex belongs to each `DirStore` instance, despite the comment calling it process-wide ([store.go:258](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/store.go:258)). The comparison and filesystem replacement are separate operations ([store.go:323](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/store.go:323), [store.go:345](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/store.go:345)). |
| 6 | |
| 7 | A concrete interleaving with two handles on the same directory: |
| 8 | |
| 9 | - Deploy reads pointer A, then reads no pipeline and passes authorization. |
| 10 | - Its `Put` checks A’s ETag successfully, then pauses before writing the temporary file. |
| 11 | - Through the second handle, an owner installs a pipeline and promotes B. Both operations finish. |
| 12 | - Deploy resumes, writes its temporary file and renames it over B. It returns success. |
| 13 | |
| 14 | G1 holds, but G2 fails: the pointer being replaced contains B, not the bytes deploy read. No restoration of A is needed. The same race permits a first promote to overwrite a newly created pointer and a rollback to overwrite an intervening promotion. A repeat promote writes nothing and is unaffected. |
| 15 | |
| 16 | This is a supported configuration concern: both the console and direct CLI independently construct directory stores ([console/main.go:482](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/cmd/console/main.go:482), [cli.go:1948](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/cli.go:1948)). |
| 17 | |
| 18 | **Correction:** Qualify G2’s backend assumptions explicitly. For directory storage, either enforce that every writer shares one handle or provide coordination across handles/processes around the comparison and replacement. Include this interleaving in backend verification; a randomized test using one shared handle cannot expose it. This concerns single-object conditional writes, separately from Paul’s cross-object decision in §16. |
| 19 | |
| 20 | 2. **R4-2 — P2 — §§7.2, 12: The randomized oracle rejects a write that satisfies G1 and G2.** |
| 21 | |
| 22 | §7.2 infers that a pipeline existing before the pointer read must be seen and cause refusal. §12 repeats that assertion while explicitly scheduling **pipeline removal** ([spec:332](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/docs/superpowers/specs/2026-10-05-deploy-credential-design.md:332), [spec:528](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/docs/superpowers/specs/2026-10-05-deploy-credential-design.md:528)). |
| 23 | |
| 24 | Consider an in-scope `edge` promotion: |
| 25 | |
| 26 | - The handler and ladder read no pipeline. |
| 27 | - An owner installs a pipeline naming `edge`. |
| 28 | - `Signer.Promote` reads C’s pointer. |
| 29 | - The pipeline is removed. |
| 30 | - The authoritative hook reads no pipeline, authorizes, and the unchanged pointer permits the write. |
| 31 | |
| 32 | `GetPipeline` returns nil for the removed object ([pipeline.go:205](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/pipeline.go:205)). Both guarantees hold, yet §12 requires failure because the pipeline existed at the pointer read. Rollback has the same counterexample. |
| 33 | |
| 34 | **Correction:** Base authorization assertions on the pipeline actually returned to the authoritative hook. Qualify the earlier-pipeline inference with continued presence through that read and the non-canary restriction. Record pointer-read, authorization-read and write events independently. |
| 35 | |
| 36 | With that correction, moving the authoritative hook before the pointer read violates G1; an unconditional write violates G2 when another writer changes C between read and write. Require reproducible schedules demonstrating each mutant’s failure. As written, failures cannot establish mutation sensitivity because the correct mechanism also fails the oracle. |
| 37 | |
| 38 | The three hook placements otherwise cover first, replacing and repeat promotes, rollback, and the handler’s proposal gate. I found no additional authorization-gap outcome outside the class already described; another ordering within that class is not a finding. S3’s conditional-write mechanism supports the stated comparison, unlike the multi-handle directory case. [AWS conditional-write documentation](https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html) |
| 39 | |
| 40 | **Verdict: request changes.** |
amadan