amadan

carlos / platform Public

spec: deploy credential rev 3, answering Astra round 2

Summary

Withdraws rev 2's serializability claim. The authorization hook now runs
between the pointer read and the pointer write in both primitives, so
the pointer's compare-and-swap defeats Astra's three-operation
counterexample. States the guarantee as invariant I1, names the one
window it leaves, and puts closing it to Paul in §16. The no-op path
runs the hook. Ship and lifetime-check claims corrected.
Agent notes
Round 2 findings committed unedited. R2-1 is accepted in part: closing
the window fully needs cross-object atomicity the release store does not
have, which is a separate spec if Paul wants it.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 2d9d528ee87eb8fb9b400dec6f400d1f54c24835 parent 38dfb24
3 files changed, +186 −45
  • docs/superpowers/specs/2026-10-05-deploy-credential-design.md +129 −45
  • docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R2.md +34 −0
  • docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md +23 −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 e27a71607..7f1694a7c 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:** 2.
+**Revision:** 3.
- Rev 1 (d30a74c2) went to Astra (via codex). The findings are in
`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R1.md`, unedited. All six were checked
@@ -12,6 +12,16 @@
flagged that as the trade-off. Rev 2 keeps the box-verified limit: the
console signs a `deploy` credential's pointer with a request-local scoped
key (§7.4, codex 6).
+- Rev 2 (38dfb240) went back. The findings are in
+ `CODEX-FINDINGS-DEPLOY-CREDENTIAL-R2.md`. All three were checked and
+ held. Changes are marked "(codex R2-N)".
+- **Rev 3 withdraws a claim rev 2 made.** Rev 2 said a `deploy` promote
+ racing a pipeline install always ends in a state some serial order
+ produces. Astra gave a three-operation counterexample (codex R2-1). Rev 3
+ reorders the reads so the pointer's own compare-and-swap defeats that
+ 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.**
**Discussion:** carlos/platform#229.
**Code read at:** main `8d8e4bae`. Every line reference below is at that commit.
@@ -245,45 +255,83 @@ 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: on the snapshot that executes (codex 1)
-
-Rev 1 ran the check in the handler, against the handler's own pipeline
-read (`apicli.go:772`). `PromoteOnLadder` reads the pipeline again
-(`release.go:930`) and acts on that second read. A pipeline installed
-between the two would be judged as absent and executed as present, which
-is an outcome no serial order of the two operations produces.
-
-So the authoritative check runs inside the release primitive, on the
-pipeline read the primitive itself uses:
-
-- `release.PromoteOptions` gains an authorization hook that
- `PromoteOnLadder` calls immediately after its own `GetPipeline` and
- before the order check. The console passes
- `deployScopeAllows` bound to the principal, the channel and the hotfix
- flag. A refusal from the hook is returned as a typed error the handler
- maps to §7.3's 403.
-- `Signer.Rollback` (`release.go:1031`) gains the same hook. When it is
- set, the primitive reads the pipeline itself and calls it before it
- signs.
-- The handlers also call `deployScopeAllows` on their own read, before the
- rules switch at `apicli.go:803` and before any proposal is created. This
- is the early refusal that gives CI a clear message. It is not the
- authority.
-
-**The contract.** For a `deploy` credential, the scope decision and the
-pointer write use one pipeline snapshot. A pipeline installed after that
-read and before the write is not seen, and the result is exactly the state
-that "promote, then install the pipeline" produces. Nothing a `deploy`
-credential writes depends on which of the two landed first. If the two
-reads disagree the other way (the handler saw a pipeline and the primitive
-did not), the handler has already refused.
-
-Serializing pipeline writes against every pointer write is not attempted
-here. It is a property of every promote today, and direct-bucket writers
-are outside the console's reach whatever the console locks (§14).
-
-The plan adds a test that installs a pipeline between the handler's read
-and the primitive's read, and asserts the refusal.
+### 7.2 Where it runs, and what is guaranteed (codex 1, codex R2-1, codex R2-2)
+
+**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`).
+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.
Everything after the check is unchanged. The ladder order, the audit line
and the serial bump all still run for a `deploy` credential.
@@ -336,11 +384,13 @@ built (for instance, the console's key is not a root key), the request is
refused. A `deploy` request never falls back to the root signer.
A grant's lifetime is checked against the pointer's own `promoted_at`
-(`release.go:396-441`), so a five-minute grant does not expire a pointer
+(`release.go:480`), so a five-minute grant does not expire a pointer
it has already signed. A pointer dated before its grant was minted is
refused, so the grant is minted before the pointer is stamped.
-Ship is unchanged and uses the console's own signer. It moves no pointer.
+Ship is unchanged. It uploads immutable artifacts and an unsigned
+manifest (`release.Ship`, `release.go:584`, which takes no signer) and
+moves no pointer (codex R2-3).
## 8. The CLI in CI
@@ -419,8 +469,19 @@ 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.
-- **One snapshot.** A pipeline installed between the handler's read and
- the primitive's read is refused, for promote and for rollback (§7.2).
+- **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.
- **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
@@ -475,7 +536,7 @@ credentials already are, and the mint line records the rungs.
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
- pointer writes to one generation, which is its own piece of work.
+ 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.
@@ -492,3 +553,26 @@ Every citation was checked at main `8d8e4bae`.
| R1-4 promote's stable refusal is not unconditional | P2 | Accepted. §1 and §5.2 corrected; the independent refusal is now the grant, §7.4. |
| R1-5 hotfix and fast-track conflated | P2 | Accepted. §7.1 rule 1. |
| R1-6 keep box-verified limits with a request-local scoped signer | P3 | Accepted and adopted. §7.4. |
+| 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
+ 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
+ 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-R2.md b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R2.md
new file mode 100644
index 000000000..bc991d2f1
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-DEPLOY-CREDENTIAL-R2.md
@@ -0,0 +1,34 @@
+Reviewed `38dfb240`. No files modified; findings are based on source inspection, without running tests.
+
+1. **R2-1 — P1 — §7.2: The snapshot check still permits an outcome no serial order produces.**
+
+ The proposed hook runs after the pipeline read at [release.go:930](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:930), but `Signer.Promote` subsequently reads the target pointer and its current ETag at [release.go:732](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:732).
+
+ A concrete interleaving:
+
+ - A deploy credential starts promoting fresh release A to `edge`; both pipeline checks see no pipeline.
+ - An owner installs a pipeline containing `edge`.
+ - After installation completes, the owner promotes fresh release B to `edge`.
+ - The deploy request resumes. A still qualifies for the legacy entry rung. `Signer.Promote` reads B’s pointer and ETag, then successfully writes A with B in its history.
+
+ The final pointer is A. No permitted serial order produces that result: placing the deploy before pipeline installation leaves B last; placing it after installation requires refusal under R2. Pointer CAS does not prevent this because the deploy reads B’s ETag **after** B lands. History and audit also incorporate B at [release.go:745](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:745).
+
+ **Correction:** Bind pipeline authorization and the subsequent pointer reads/write through serialization or equivalent atomic conflict detection across console pipeline and pointer writers. A separate pipeline recheck alone leaves another race. Add the three-operation interleaving above to the tests. Direct-bucket writers being outside console control does not justify this counterexample, which uses only console operations.
+
+2. **R2-2 — P2 — §§7.2, 12: The authoritative hook is bypassed by repeat promotions.**
+
+ `PromoteOnLadder` returns a successful no-op at [release.go:887](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:887), before reaching `GetPipeline` and therefore before the proposed hook.
+
+ If `edge` already points at A, the handler can authorize a repeat promotion while no pipeline exists, an owner can install the pipeline, and the primitive can then return success without performing its authoritative scope check. This writes no pointer, so it is not the escape in R2-1, but it violates the specified refusal contract and leaves the proposed “pipeline installed between reads” test incomplete.
+
+ **Correction:** When an authorization hook is supplied, read the pipeline and invoke the hook before the no-op return. Test the race with the requested version already at the channel head, as well as with a changing head.
+
+3. **R2-3 — P2 — §7.4: The shipping claim and lifetime-check citation are incorrect.**
+
+ “Ship … uses the console’s own signer” is false. The handler calls `release.Ship` without a signing key; [release.go:584](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:584) accepts no signer and stores the manifest as plain JSON at [release.go:618](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:618).
+
+ The lifetime explanation is correct, but its `release.go:396-441` citation does not contain the check against `promoted_at`. That check is at [release.go:480](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/design-deploy-credential/internal/release/release.go:480).
+
+ **Correction:** State that shipping remains unchanged, uploads immutable artifacts and an unsigned manifest, and moves no pointer. Correct the lifetime-check citation.
+
+**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 f382e5900..55681a302 100644
--- a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md
+++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-DEPLOY-CREDENTIAL.md
@@ -92,3 +92,26 @@ lists each disposition. Read rev 2 cold, then check:
- Anything the rev 2 changes broke that rev 1 had right.
Number findings R2-1 onward. Same severities, same verdict line.
+
+## Round 3
+
+Rev 3 answers your round 2 (`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R2.md`); §15
+lists each disposition. R2-1 is accepted in part: the serializability
+claim is withdrawn, the hook moves between the pointer read and the
+pointer write, and §7.2 states invariant I1 and one window it does not
+cover. Whether to close that window is put to Paul in §16 and is not
+yours to rule on. What is yours:
+
+- **Is I1 true** of the mechanism as written, for `Signer.Promote` and
+ `Signer.Rollback` as they are in this worktree? Give an interleaving
+ that breaks (a) or (b) if one exists.
+- **Is the uncovered window stated completely?** Give any outcome a
+ `deploy` credential can produce that is neither forbidden by I1 nor
+ inside the window §7.2 names. Consider first promotes (no pointer, a
+ create-only write), the no-op path, rollback's history, the handler's
+ proposal path, and conflict handling.
+- Does the hook's placement change behaviour for a caller that passes no
+ hook?
+- Anything rev 3 broke that rev 2 had right, and any wrong citation.
+
+Number findings R3-1 onward. Same severities, same verdict line.