amadan
spec: deploy credential rev 5, answering Astra round 4
Summary
States G2 per backend: it holds against every writer on S3, and only among writers sharing one handle on a directory store, which is that store's existing, documented limit. Restates the G1 inference and the randomized test's oracle on the pipeline the authorization read actually returned, with recorded events and replayable mutant failures.
Agent notes
Round 4 found no outcome outside the class the open sentence describes and judged the three hook call points sufficient. Findings committed unedited. §16 still needs Paul.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
3 files changed,
+113
−9
docs/superpowers/specs/2026-10-05-deploy-credential-design.md+58 −9docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md+40 −0docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md+15 −0
CI cancelled — superseded by a newer push — run details
diff --git a/docs/superpowers/specs/2026-10-05-deploy-credential-design.md b/docs/superpowers/specs/2026-10-05-deploy-credential-design.md| index cef4bcf60..2cdee8de3 100644 |
| --- a/docs/superpowers/specs/2026-10-05-deploy-credential-design.md |
| +++ b/docs/superpowers/specs/2026-10-05-deploy-credential-design.md |
| @@ -1,7 +1,7 @@ |
| # A deploy credential for CI: promote through the console, limited to rungs |
| **Date:** 2026-10-05 |
| -**Revision:** 4. |
| +**Revision:** 5. |
| - Rev 1 (d30a74c2) went to Astra (via codex). The findings are in |
| `CODEX-FINDINGS-DEPLOY-CREDENTIAL-R1.md`, unedited. All six were checked |
| @@ -34,6 +34,13 @@ |
| that leaves open, and requires a randomized interleaving test of exactly |
| those two properties (§12). §16's decision is unchanged in substance and |
| is now stated in those terms. |
| +- Rev 4 (2af4eba4) went back. The findings are in |
| + `CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md`. Astra found no outcome outside |
| + the class §7.2's open sentence describes, and found the three hook call |
| + points sufficient. Two findings remained and both held: G2 assumed more |
| + of the directory store than it provides, and §12's randomized test |
| + asserted something G1 and G2 do not imply. Rev 5 qualifies G2 by backend |
| + and corrects the test's oracle. Changes are marked "(codex R4-N)". |
| **Discussion:** carlos/platform#229. |
| **Code read at:** main `8d8e4bae`. Every line reference below is at that commit. |
| @@ -282,6 +289,23 @@ There is no lock in the console and no write that spans two objects. A |
| pipeline and a channel pointer are two objects. No ordering of reads makes |
| "there is no pipeline" and "write this pointer" one atomic step. |
| +**The two backends differ, and G2 below is only as good as the backend** |
| +(codex R4-1). |
| + |
| +- `S3Store` sends the condition with the write (`store.go:613-628`), and S3 |
| + evaluates it atomically. G2 holds against every writer. |
| +- `DirStore` compares and then renames under a mutex that belongs to one |
| + handle (`store.go:258-262`, `:316-348`). Its own comment calls this |
| + "single-process fidelity, which is what the tests and a one-box |
| + deployment need" (`store.go:254-257`). Two handles on one directory, |
| + such as a console and a direct-mode CLI (`cmd/console/main.go:482`, |
| + `cli.go:1948`), can both pass the comparison and the later rename wins. |
| + On a directory store G2 holds only among writers that share one handle. |
| + |
| +That is an existing limit of every conditional write on a directory |
| +store, for every caller. This spec does not change it and does not depend |
| +on a directory store being safe across processes (§14). |
| + |
| **What a `deploy` request therefore is.** It is authorized against the |
| pipeline it read, and it may complete after a pipeline is installed. That |
| is what an in-flight request is under any authorization system: a policy |
| @@ -327,10 +351,15 @@ read refuses a `deploy` credential for any channel but `canary/<name>`. |
| C's pointer. |
| - **G2.** It lands only if C's pointer, at write time, is byte for byte |
| what the request read. For a first promote, it lands only if C has no |
| - pointer at write time. |
| + pointer at write time. This holds to the extent the backend's |
| + conditional write does, as set out above. |
| -From G1: a pipeline that existed before the request read C is seen, and |
| -the request is refused. |
| +From G1: a pipeline that existed before the request read C, and still |
| +exists when the authorization read is made, is seen. A `deploy` request |
| +for any channel but `canary/<name>` is then refused. A pipeline that was |
| +installed and removed again before the authorization read is not seen, |
| +and nothing requires it to be: the request is judged on the pipeline the |
| +authorization read returned (codex R4-2). |
| From G2: a write to C that leaves it different from what the request read |
| defeats the `deploy` write. That covers Astra's round 2 counterexample, |
| @@ -529,11 +558,25 @@ credentials already are, and the mint line records the rungs. |
| rounds went. The plan adds a test that runs random schedules of `deploy` |
| promote, `deploy` rollback, owner promote, owner rollback, pipeline |
| install and pipeline removal against a store that can pause between any |
| - two of a request's steps, over many seeds. It asserts G1 and G2 for |
| - every `deploy` write that landed, and that no `deploy` write landed when |
| - a pipeline naming the channel existed before its pointer read. A mutant |
| - with the hook moved before the pointer read, and one with the write made |
| - unconditional, must each fail it. |
| + two of a request's steps, over many seeds. |
| + - It records three events for every `deploy` request, independently: the |
| + pointer read (with the bytes read), the authorization read (with the |
| + pipeline returned), and the write (with the bytes replaced). |
| + - The oracle is G1 and G2 and nothing else (codex R4-2). G1: the |
| + authorization read came after the pointer read, and the pipeline it |
| + returned permits the request under §7.1. G2: the bytes replaced equal |
| + the bytes read. It does not assert anything about a pipeline that |
| + existed at some other moment, since a pipeline can be removed again |
| + before the authorization read. |
| + - Two mutants must each fail it, on a schedule the test prints so the |
| + failure can be replayed: the authoritative hook moved before the |
| + pointer read (breaks G1), and the write made unconditional (breaks G2 |
| + when another writer changes C between the read and the write). |
| + - It runs on one shared store handle, which is where G2 holds for a |
| + directory store. It therefore cannot show the two-handle directory |
| + race (codex R4-1), and does not claim to. The S3 path's conditional |
| + write is covered by the existing store tests |
| + (`internal/release/store_test.go`, `store_rgw_test.go`). |
| - **No hook, no change.** A caller that passes no hook makes the same |
| store calls in the same order as before, for promote, repeat promote |
| and rollback. |
| @@ -594,6 +637,10 @@ credentials already are, and the mint line records the rungs. |
| pointer writes to one generation, which is its own piece of work (§16). |
| - A pipeline may name `stable` with no passkey rule, and promote then |
| applies only that channel's rules (§1). Existing behaviour, unchanged. |
| +- A directory store's conditional write is not safe across handles or |
| + processes (§7.2, codex R4-1). It affects every conditional write on a |
| + directory-backed deployment, whoever makes it. Fixing it, with a file |
| + lock or by refusing a second writer, is separate work. |
| ## 15. Review dispositions |
| @@ -615,6 +662,8 @@ Every citation was checked at main `8d8e4bae`. |
| | R3-2 the no-op path detects no conflict | P2 | Accepted. §7.2 and §12: a no-op is an observation, with its own assertions. | |
| | R3-3 the relocated hook loses the scope refusal to a ladder error | P2 | Accepted. §7.2: the hook is also called on the ladder's pipeline read. | |
| | R3-4 wrong location and missing first refusal in §9 | P2 | Accepted. §9. | |
| +| R4-1 G2 fails across two `DirStore` handles on one directory | P1 | Accepted as a qualification. §7.2 states G2 per backend. The directory store's cross-handle limit is existing, documented in the store, and recorded in §14 as separate work. | |
| +| R4-2 the randomized test's oracle rejects a write that satisfies G1 and G2 | P2 | Accepted. §7.2's inference and §12's oracle are restated on the pipeline the authorization read returned. Mutants must fail on a printed, replayable schedule. | |
| ## 16. For Paul: requests in flight when a pipeline is installed |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md| new file mode 100644 |
| index 000000000..bb8e8a7d1 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md |
| @@ -0,0 +1,40 @@ |
| +Reviewed `2af4eba4`. No files modified; no tests run. |
| + |
| +1. **R4-1 — P1 — §7.2: G2 does not hold across `DirStore` handles sharing a directory.** |
| + |
| + 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)). |
| + |
| + A concrete interleaving with two handles on the same directory: |
| + |
| + - Deploy reads pointer A, then reads no pipeline and passes authorization. |
| + - Its `Put` checks A’s ETag successfully, then pauses before writing the temporary file. |
| + - Through the second handle, an owner installs a pipeline and promotes B. Both operations finish. |
| + - Deploy resumes, writes its temporary file and renames it over B. It returns success. |
| + |
| + 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. |
| + |
| + 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)). |
| + |
| + **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. |
| + |
| +2. **R4-2 — P2 — §§7.2, 12: The randomized oracle rejects a write that satisfies G1 and G2.** |
| + |
| + §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)). |
| + |
| + Consider an in-scope `edge` promotion: |
| + |
| + - The handler and ladder read no pipeline. |
| + - An owner installs a pipeline naming `edge`. |
| + - `Signer.Promote` reads C’s pointer. |
| + - The pipeline is removed. |
| + - The authoritative hook reads no pipeline, authorizes, and the unchanged pointer permits the write. |
| + |
| + `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. |
| + |
| + **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. |
| + |
| + 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. |
| + |
| +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) |
| + |
| +**Verdict: request changes.** |
| \ No newline at end of file |
diff --git a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md| index 5a2c8696b..93e595a33 100644 |
| --- a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md |
| +++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md |
| @@ -140,3 +140,18 @@ is §16, Paul's decision, and not yours to rule on. What is yours: |
| - Anything rev 4 broke, and any wrong citation. |
| Number findings R4-1 onward. Same severities, same verdict line. |
| + |
| +## Round 5 |
| + |
| +Rev 5 answers your round 4 (`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R4.md`); §15 |
| +lists each disposition. G2 is now stated per backend, and §12's randomized |
| +test asserts G1 and G2 only, on recorded events. The directory store's |
| +cross-handle limit is recorded in §14 as existing and separate; §16 is |
| +still Paul's. |
| + |
| +Check that the two round 4 fixes close what you found, that the oracle as |
| +now written is implied by G1 and G2 and that both mutants fail it, and |
| +that rev 5 broke nothing and cites correctly. If you have no finding at P1 |
| +or P2, say so and give the verdict. |
| + |
| +Number findings R5-1 onward. Same severities, same verdict line. |