amadan

carlos / platform Public

spec: deploy credential rev 4, answering Astra round 3

Summary

Replaces invariant I1 with G1 and G2, which claim only what a
content-hash conditional write on one object proves, and one sentence
for what they leave open. The hook runs at three points: the ladder's
pipeline read, between pointer read and write, and on the repeat path. A
no-op is defined as an observation. Adds a randomized interleaving test
with two mutants. Corrects the mixed-version explanation.
Agent notes
Three rounds each found a new ordering of one fault (R2's pipeline rule
spans two objects). Rev 4 stops adding example fixes. Round 3 findings
committed unedited. §16 still needs Paul.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 2af4eba4ac79ce48274260b4f36f7c65afa63dca parent 2d9d528
3 files changed, +250 −114
  • docs/superpowers/specs/2026-10-05-deploy-credential-design.md +175 −114
  • docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md +50 −0
  • docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md +25 −0

CI passed — 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 7f1694a7c..cef4bcf60 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:** 3.
+**Revision:** 4.
- Rev 1 (d30a74c2) went to Astra (via codex). The findings are in
`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R1.md`, unedited. All six were checked
@@ -22,6 +22,18 @@
counterexample, states the guarantee as an invariant (§7.2, I1), and
names the one window it does not close. **That window is a decision for
Paul: §16.**
+- Rev 3 (2d9d528e) went back. The findings are in
+ `CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md`. All four were checked and held.
+ Changes are marked "(codex R3-N)".
+- **Rev 4 stops patching interleavings.** Three rounds each found a new
+ ordering of the same fault: R2's pipeline rule reads one object and
+ writes another, and the store cannot make that atomic. Rev 3's I1(b)
+ said "nothing wrote C", which the store cannot promise either, because
+ an ETag is a hash of the content (codex R3-1). Rev 4 states only what
+ the store does guarantee (§7.2, G1 and G2), says in one sentence what
+ 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.
**Discussion:** carlos/platform#229.
**Code read at:** main `8d8e4bae`. Every line reference below is at that commit.
@@ -255,83 +267,104 @@ principal it refuses, in this order:
5. The rung is not in the credential's rungs.
6. The app has a pipeline and the rung is not `canary`.
-### 7.2 Where it runs, and what is guaranteed (codex 1, codex R2-1, codex R2-2)
+### 7.2 Where it runs, and what is guaranteed (codex 1, R2-1, R2-2, R3-1, R3-2, R3-3)
**The store gives one tool.** Every write in the release store is a
-compare-and-swap on a single object (`internal/release/store.go:33-44`).
+conditional write on a single object: create-only, or replace-only against
+an ETag (`internal/release/store.go:33-44`). An ETag is a hash of the
+object's bytes (`store.go:279`; S3's is too). So a conditional write proves
+one thing: at write time the object's bytes were the bytes the writer
+read. It does not prove nobody wrote the object in between. Two rollbacks
+inside one second can restore a pointer byte for byte, because signing
+truncates `promoted_at` to the second (`release.go:371`) (codex R3-1).
+
There is no lock in the console and no write that spans two objects. A
-pipeline and a channel pointer are two objects, so no ordering of reads
-makes "there is no pipeline" and "write this pointer" one atomic step.
-
-**What went wrong twice.** Rev 1 checked the scope on the handler's
-pipeline read (`apicli.go:772`), and the primitive acted on a second read
-(`release.go:930`). Rev 2 moved the check to that second read and claimed
-the result was always equivalent to "promote, then install the pipeline".
-It is not. Both primitives read the target pointer and its ETag after that
-point (`Signer.Promote`, `release.go:732`; `Signer.Rollback`,
-`release.go:1043`). So a pipeline could be installed, and an owner could
-promote under it, and the `deploy` write could still land on top with the
-owner's version in its history.
-
-**The mechanism.** The authorization runs between the pointer read and the
-pointer write, so the pointer's own compare-and-swap covers it:
-
-1. The primitive reads the target pointer and its ETag, as it does today.
-2. If the caller supplied an authorization hook, the primitive reads the
- pipeline fresh and calls the hook with it.
-3. The primitive signs and writes with that ETag, as it does today. A
- conflict is returned as a conflict. It is not retried inside the
- primitive, because a retry must start again from step 1.
-
-`Signer.Promote` and `Signer.Rollback` both gain the hook, carried from
-`PromoteOptions` for a promote. The console passes `deployScopeAllows`
-bound to the principal, the channel and the hotfix flag. A refusal is a
-typed error the handler maps to §7.3's 403. For any caller that passes no
-hook, both primitives behave exactly as they do today.
-
-`PromoteOnLadder`'s no-op return for a repeat promote (`release.go:887`)
-comes before all of this. When a hook is supplied, the primitive reads the
-pipeline and calls the hook before that return, so a repeat is refused on
-the same terms as a first attempt (codex R2-2).
-
-The handlers also call `deployScopeAllows` on their own read, before the
-rules switch at `apicli.go:803` and before any proposal is created. That
-is the early refusal with a clear message. It is not the authority.
-
-**Invariant I1.** For a write by a `deploy` credential to channel C:
-
-- (a) the pipeline it was authorized against was read after C's pointer
- was read;
-- (b) the write succeeds only if nothing wrote C between that pointer read
- and the write.
-
-What follows from I1:
-
-- A pipeline that existed before the request read C is seen, and the
- request is refused.
-- A `deploy` write never lands on top of a write to C that was made after
- the request read C. That includes every write made under a new pipeline.
- This is Astra's counterexample: the owner's promote changes C's ETag and
- the `deploy` write fails.
-
-**What I1 does not cover.** A pipeline installed inside the window between
-step 2 and step 3, with no write to C in that window. The `deploy` write
-lands on a channel that became a pipeline channel a moment earlier. The
-window is two store round trips. The version that lands was authorized
-when the request read the state, and it replaces only what the request
-itself read.
-
-This is not serializability, and the spec no longer says it is. Another
-operation that reads C inside that window, such as an owner's promote
-that computes a stage from C, sees C as it was before the `deploy` write.
-That is the same thing two concurrent promotes by people see today.
-
-Closing the window needs something the store does not have: a per-app
-lock held across pipeline writes and pointer writes, or a pipeline
-generation stamped into every pointer. §16 puts that choice to Paul.
-
-The rung limit does not depend on any of this. It is enforced by the
-grant (§7.4), which involves one object and has no race.
+pipeline and a channel pointer are two objects. No ordering of reads makes
+"there is no pipeline" and "write this pointer" one atomic step.
+
+**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
+change governs the requests that start after it. The mechanism below makes
+the in-flight case as narrow as one object's conditional write allows, and
+the spec claims nothing beyond that.
+
+**The mechanism.** The console passes an authorization hook,
+`deployScopeAllows` bound to the principal, the channel and the hotfix
+flag. The primitives call it with a pipeline they have just read, at
+three points:
+
+1. **On the ladder's pipeline read** in `PromoteOnLadder`
+ (`release.go:930`), before the order check. This is not the authority.
+ It exists so that a pipeline installed after the handler's read is
+ refused with §7.3's 403, and not with the ladder's 409 about channel
+ order (codex R3-3).
+2. **After the pointer read and before the write**, in `Signer.Promote`
+ (`release.go:732`) and `Signer.Rollback` (`release.go:1043`). The
+ primitive reads the pointer and its ETag as it does today, reads the
+ pipeline fresh, calls the hook, then signs and writes against that
+ ETag. This is the authority for a write.
+3. **On the repeat path.** `PromoteOnLadder` returns a no-op when the
+ channel already points at the requested version (`release.go:887`).
+ With a hook, it reads the pipeline after that pointer read and calls
+ the hook before returning (codex R2-2).
+
+A refusal is a typed error the handler maps to §7.3's 403. A failed
+conditional write is returned as a conflict and is not retried inside the
+primitive, because a retry must start again from the pointer read. A
+caller that passes no hook gets today's behaviour at all three points,
+with no extra read.
+
+The handlers also call `deployScopeAllows` on their own pipeline read,
+before the rules switch at `apicli.go:803`. This is what keeps a `deploy`
+credential off the proposal path: the handler creates a proposal only
+when its own read shows a pipeline that names the channel, and that same
+read refuses a `deploy` credential for any channel but `canary/<name>`.
+
+**What is guaranteed.** For a write by a `deploy` credential to channel C:
+
+- **G1.** It was authorized against a pipeline read made after the read of
+ 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.
+
+From G1: a pipeline that existed before the request read C is seen, and
+the request is refused.
+
+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,
+where an owner promotes B under a new pipeline.
+
+**What is not guaranteed, in one sentence.** A pipeline installed after
+the request's authorization read is not seen, and the write lands if G2
+holds.
+
+That sentence covers every case found so far, and it is the whole of what
+§16 asks Paul to accept or close:
+
+- the pipeline is installed and nothing touches C before the write;
+- the pipeline is installed and C is written and restored to identical
+ bytes, as two rollbacks in one second do (codex R3-1);
+- C has no pointer, a pipeline is installed, and the create-only write
+ lands on a channel that is still empty.
+
+In each, the pointer the `deploy` write replaces is exactly the state the
+request read, and the version was authorized when the request read it.
+This is not serializability and the spec does not claim it. Another
+operation that reads C before the `deploy` write lands sees the earlier
+state, as it would between two people promoting today.
+
+**A no-op is an observation, not a write** (codex R3-2). A repeat promote
+answers "at the moment this request read C, C pointed at this version,
+and the credential was in scope on a pipeline read after that". It makes
+no conditional write, so it detects no later change to C. If an owner
+installs a pipeline and promotes B after the request's reads, the request
+still reports the no-op for A. It has changed nothing, and its answer was
+true when it was read. No conflict is promised for this path.
+
+The rung limit depends on none of this. The grant enforces it (§7.4) on
+one object, with no race.
Everything after the check is unchanged. The ladder order, the audit line
and the serial bump all still run for a `deploy` credential.
@@ -427,12 +460,16 @@ in-instance caller, or choose a second name for the CLI.
## 9. Mixed versions and rollback
-- **Old console, `deploy` token.** `cliRoute` checks `allow.Permits(p.Role)`
- before any handler runs (`authcli.go:411`). An old binary's sets do not
- contain `deploy`, so every door refuses. The plan must pin this with a
- test that resolves a service principal carrying a role the binary does
- not know and asserts a refusal at every registered `cliRoute`. It must
- also confirm the same holds in v0.21.0's `cliRoute` by reading it.
+- **Old console, `deploy` token.** Two checks refuse it, and the first is
+ the one that fires (codex R3-4). `CLIPrincipal` rejects a stored service
+ role it cannot parse (`svcprincipal.go:126`), so `cliRoute` answers as it
+ does for no credential at all, before its role gate. If a role did
+ resolve, `cliRoute` checks `allow.Permits(p.Role)` before any handler
+ runs (`authcli.go:430`), and an old binary's sets do not contain
+ `deploy`. The plan pins both, separately: a stored role the binary does
+ not know is refused as not signed in at every registered `cliRoute`; and
+ a known role outside a door's set is refused by the role gate. It must
+ also confirm both hold in v0.21.0 by reading it.
- **Old console, new column.** An old binary ignores `rungs`. That is safe
only because of the line above: it never lets the credential through.
- **New console, old CLI.** `services create --role deploy` fails in the old
@@ -469,19 +506,37 @@ credentials already are, and the mint line records the rungs.
`canary`, a hotfix, and a non-canary channel on a pipelined app each give
a 403 and write nothing. A pipeline that names `stable` with no passkey
rule still refuses a `deploy` credential.
-- **I1, for promote and for rollback (§7.2).** Each with the store paused
- at the named point:
- - a pipeline installed before the primitive's pointer read is refused;
- - a pipeline installed between the handler's read and the primitive's
- pointer read is refused;
- - Astra's three operations (pipeline installed, an owner promotes B to
- C, the `deploy` write resumes) end in a conflict, C still points at B,
- and B's pointer is untouched;
- - the same races with the requested version already at C's head, so the
- no-op path is covered (codex R2-2);
- - the uncovered window is pinned by a test that states it: a pipeline
- installed between the hook and the write, with no write to C, lands.
- If §16 chooses to close the window, that test flips.
+- **G1 and G2, for promote and for rollback (§7.2).** Each with the store
+ paused at the named point:
+ - a pipeline installed before the primitive's pointer read is refused
+ with §7.3's 403;
+ - a pipeline that excludes the requested rung, installed between the
+ handler's read and the ladder's read, is refused with §7.3's 403 and
+ not the ladder's 409 (codex R3-3);
+ - a pipeline installed and then an owner's promote of B to C, before
+ the `deploy` write: conflict, and C still points at B;
+ - a pipeline installed and then two rollbacks of C that restore its
+ bytes, before the `deploy` write: the write lands. The test names
+ this as the accepted in-flight case (codex R3-1);
+ - a pipeline installed with no write to C, and a first promote onto an
+ empty C: each lands, named the same way.
+ If §16 chooses to close the gap, the three "lands" assertions flip.
+- **No-op (§7.2).** Its own assertions, never a conflict (codex R3-2):
+ refused when a pipeline existed before the pointer read; a successful
+ no-op when the pipeline, or an owner's later promote, arrives after the
+ request's reads.
+- **Randomized interleavings.** One example per round was how three
+ 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.
+- **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.
- **Signer.** A pointer written by a `deploy` promote carries a grant for
exactly the credential's rungs and verifies with `verifyPointer`. With
the scope function stubbed to allow everything, an out-of-rung promote
@@ -494,7 +549,7 @@ credentials already are, and the mint line records the rungs.
- **Mint.** `deploy` with no app, with no rungs, with `stable`, with an
unknown rung; another role with rungs. Each refused through both doors.
- **Read-back.** A `deploy` row with empty rungs is refused at resolve.
-- **Unknown role.** §9's fail-closed test.
+- **Unknown role.** §9's two fail-closed tests.
- **CLI.** Token plus console selects API mode; token with no console
errors; token plus a store variable errors; a bare store variable is
still direct mode.
@@ -534,8 +589,8 @@ credentials already are, and the mint line records the rungs.
- For every caller, the promote handler judges pipeline rules (approvals,
passkey) on its own pipeline read, and `PromoteOnLadder` acts on a second
one. A pipeline changed between the two is judged on the old rules. §7.2
- closes this for `deploy` and leaves it as found for people and for
- `publish`. Closing it for everyone means binding pipeline writes and
+ narrows this for `deploy` to G1 and G2, and leaves it as found for people
+ and for `publish`. Closing it for everyone means binding pipeline writes and
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.
@@ -556,23 +611,29 @@ Every citation was checked at main `8d8e4bae`.
| R2-1 a write can land over an owner's promote made under a new pipeline | P1 | Accepted in part. §7.2: the hook moves between the pointer read and the write, so that counterexample fails on the pointer's compare-and-swap. The serializability claim is withdrawn and replaced by I1. Full serialization is not built; the remaining window is stated and put to Paul in §16. |
| R2-2 the no-op return skips the hook | P2 | Accepted. §7.2. |
| R2-3 ship does not use a signer; wrong citation for the lifetime check | P2 | Accepted. §7.4. |
-
-## 16. For Paul: the one window I1 leaves
-
-A pipeline installed in the two store round trips between a `deploy`
-request's authorization and its write is not seen (§7.2). Two ways to
-treat it:
-
-- **A. Accept it, as written (recommended).** R2 is a rule about which
- channels CI is offered, and the trust boundary is the rung limit, which
- the grant enforces with no race. Hitting the window takes an owner
- installing a pipeline in the same instant CI promotes, and the result is
- what a promote a moment earlier would have produced. The same window
+| R3-1 a restored ETag makes I1(b) false | P1 | Accepted. §7.2: I1 is replaced by G1 and G2, which claim only what a content-hash conditional write proves. The restored-bytes case is named as part of the in-flight gap. |
+| 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. |
+
+## 16. For Paul: requests in flight when a pipeline is installed
+
+§7.2 guarantees G1 and G2 and nothing more: a pipeline installed after a
+`deploy` request's authorization read is not seen, and the request's write
+lands if the pointer is still byte for byte what it read. Two ways to
+treat that:
+
+- **A. Accept it, as written (recommended).** This is how an in-flight
+ request behaves under any authorization system: the policy change
+ governs requests that start after it. R2 is a rule about which channels
+ CI is offered. The trust boundary is the rung limit, which the grant
+ enforces with no race. Reaching the gap takes an owner installing a
+ pipeline while a CI promote is between two store calls, and the result
+ is what a promote a moment earlier would have produced. The same gap
exists today for every person's promote against pipeline rules (§14).
-- **B. Close it for everyone.** Add a per-app lock in the store, or stamp a
- pipeline generation into every pointer, and take it in pipeline writes,
- promotes, rollbacks and proposal execution. That removes the window for
- `deploy`, for `publish` and for people. It is a change to the release
+- **B. Close it for everyone.** Stamp a pipeline generation into every
+ pointer, or add a per-app lock in the store, and take it in pipeline
+ writes, promotes, rollbacks and proposal execution. That removes the gap
+ for `deploy`, for `publish` and for people. It changes the release
store's concurrency model and should be its own spec, which this one
would then depend on.
-
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md
new file mode 100644
index 000000000..09413d0d8
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md
@@ -0,0 +1,50 @@
+Reviewed `2d9d528e`. No files modified; findings are based on source inspection. No tests were run.
+
+1. **R3-1 — P1 — §§7.2, 12, 16: I1(b) is false because an intervening write can restore the original ETag.**
+
+ `DirStore` derives its ETag from the object’s content and compares that hash at replacement time ([store.go:279](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/store.go:279), [store.go:333](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/store.go:333)). It does not prove that nobody wrote the object.
+
+ A concrete interleaving, possible entirely through console operations:
+
+ - `edge` contains a root-signed pointer to A, with history `[B, …]`, no fast-track flag, and `promoted_at` in the current second.
+ - A deploy request reads that pointer and ETag. Its subsequent authorization read sees no pipeline.
+ - An owner installs a pipeline containing `edge`, with no approval or passkey requirement.
+ - The owner rolls `edge` back twice, A → B → A, within that same second.
+ - The deploy request resumes and successfully replaces the pointer using its original ETag.
+
+ Rollback swaps the head and first history entry while preserving the audit ([release.go:1054](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:1054)). Two rollbacks restore those fields exactly. Signing truncates time to seconds and signs the resulting payload deterministically ([release.go:371](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:371)), so the original signed bytes—and content hash—can return.
+
+ This breaks I1(b) for either a waiting `Signer.Promote` or `Signer.Rollback`. It also falls outside the stated exception, which requires **no write to C** during the window. I1(a) still holds.
+
+ **Correction:** State the actual guarantee as matching the observed ETag, and explicitly account for intervening writes that restore it, or introduce a generation mechanism that detects those writes. Add this rollback interleaving to the tests. Create-only writes likewise prove absence at write time, not uninterrupted absence after the read. This is separate from Paul’s decision about accepting the pipeline-install window.
+
+2. **R3-2 — P2 — §§7.2, 12: The no-op path has an additional uncovered outcome and cannot satisfy the repeated conflict test as written.**
+
+ Consider:
+
+ - A repeat deploy promotion reads A at `edge`.
+ - The new no-op hook reads no pipeline and authorizes.
+ - An owner installs a pipeline and promotes B to `edge`.
+ - The deploy request returns successful `noop` for A.
+
+ The existing no-op branch returns without a conditional write or pointer recheck ([release.go:887](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:887)); the handler reports that success ([apicli.go:889](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/console/apicli.go:889)). Adding authorization before the return does not add conflict detection.
+
+ I1 governs writes, so it does not forbid this outcome. The named exception does not describe it either: another writer changed C, and the deploy request writes nothing. Consequently, §12’s instruction to repeat the conflict races with the requested version already at the head needs a different expected result.
+
+ **Correction:** Specify no-op success as an observation of the earlier pointer, with authorization checked separately. Document this outcome and give no-op races their own assertions. Do not promise a conflict unless the mechanism actually detects one.
+
+3. **R3-3 — P2 — §§7.2–7.3, 12: Moving the hook loses the scope-specific refusal before ladder errors.**
+
+ The handler can read no pipeline and pass its early check. An owner then installs a pipeline whose entry is `preview`, excluding `edge`. `PromoteOnLadder` reads that pipeline and rejects the requested `edge` promotion during its order check, before calling `Signer.Promote` and reaching the relocated hook ([release.go:930](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:930), [release.go:951](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:951)).
+
+ The handler consequently returns the existing 409 ladder error ([apicli.go:882](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/console/apicli.go:882)), rather than §7.3’s credential-and-rungs 403. Rev 2’s hook immediately after the ladder’s pipeline read would have produced the specified refusal.
+
+ **Correction:** Retain an early scope check on the ladder’s pipeline read, in addition to the authoritative check after the pointer read. Test this race using a pipeline that excludes the requested rung. Keep both additions conditional on a supplied hook so existing callers retain their behavior.
+
+4. **R3-4 — P2 — §9: The mixed-version explanation cites the wrong location and skips the actual unknown-role refusal.**
+
+ `authcli.go:411` is a comment; the `allow.Permits` check is at [authcli.go:430](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/console/authcli.go:430). More significantly, an unknown stored service role is rejected earlier by `CLIPrincipal` ([svcprincipal.go:126](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/console/svcprincipal.go:126)). `cliRoute` then returns the not-signed-in response before reaching its role gate.
+
+ **Correction:** Cite both checks accurately. Test an unknown stored role through the resolver and registered doors, expecting authentication refusal; test role-set exclusion separately. The fail-closed conclusion remains valid.
+
+**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 55681a302..5a2c8696b 100644
--- a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md
+++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md
@@ -115,3 +115,28 @@ yours to rule on. What is yours:
- Anything rev 3 broke that rev 2 had right, and any wrong citation.
Number findings R3-1 onward. Same severities, same verdict line.
+
+## Round 4
+
+Rev 4 answers your round 3 (`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R3.md`); §15
+lists each disposition. I1 is gone. §7.2 now claims two properties, G1 and
+G2, and one sentence for what they leave open. Whether to close that gap
+is §16, Paul's decision, and not yours to rule on. What is yours:
+
+- **Are G1 and G2 true** of the mechanism as written, for a first promote,
+ a replacing promote, a repeat promote and a rollback, against
+ `DirStore` and `S3Store` as they are? Give an interleaving that breaks
+ either.
+- **Is the open sentence complete?** Give any outcome a `deploy`
+ credential can produce that G1 and G2 do not forbid and that sentence
+ does not describe. A new member of the class the sentence already
+ describes is not a finding; say so if that is all you find.
+- Are the three hook call points consistent with each other and with the
+ handler's own check? Can any path reach a write, a proposal or a
+ success response for a `deploy` credential without the hook having run
+ on a pipeline read at least as recent as the spec says?
+- Is §12's randomized test specified well enough to catch the faults of
+ rounds 1 to 3? Would its two mutants fail it?
+- Anything rev 4 broke, and any wrong citation.
+
+Number findings R4-1 onward. Same severities, same verdict line.