amadan
spec: deploy credential rev 5.1, ruling R5
Human
Prompt
recommendation sounds good
From this commit's own message. The prompt ledger has no entries for it — which is what a squashed, rebased or amended commit looks like, and what every commit looks like in a repo without a ledger.
Summary
Records Paul's ruling on §16 as R5: a deploy request in flight when a pipeline is installed may complete within G1 and G2. The gap is accepted and not closed by this spec.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+26
−22
docs/superpowers/specs/2026-10-05-deploy-credential-design.md+26 −22
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 edc4fd18d..591e3336b 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:** 5. |
| +**Revision:** 5.1. |
| - Rev 1 (d30a74c2) went to Astra (via codex). The findings are in |
| `CODEX-FINDINGS-DEPLOY-CREDENTIAL-R1.md`, unedited. All six were checked |
| @@ -43,7 +43,9 @@ |
| and corrects the test's oracle. Changes are marked "(codex R4-N)". |
| - Rev 5 (e764b20c) went back. Astra's round 5 |
| (`CODEX-FINDINGS-DEPLOY-CREDENTIAL-R5.md`) found nothing at P1 or P2 and |
| - accepted. Rev 5 is unchanged by it. §16 is still open for Paul. |
| + accepted. Rev 5 is unchanged by it. |
| +- **Rev 5.1 records Paul's ruling on §16 as R5** (2026-10-05): the |
| + in-flight gap is accepted. Nothing else changes. |
| **Discussion:** carlos/platform#229. |
| **Code read at:** main `8d8e4bae`. Every line reference below is at that commit. |
| @@ -149,6 +151,9 @@ is a separate spec. Neither is part of this one. |
| bumps the serial makes the bypass more attractive. Polling every followed |
| channel pointer multiplies the one serial read per 2-second tick that the |
| serial exists to protect. |
| +- **R5.** A `deploy` request in flight when a pipeline is installed may |
| + complete, within G1 and G2 (§7.2, §16). The gap is accepted and is not |
| + closed by this spec. |
| ## 4. The shape, in one paragraph |
| @@ -373,7 +378,7 @@ 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: |
| +R5 accepts (§16): |
| - the pipeline is installed and nothing touches C before the write; |
| - the pipeline is installed and C is written and restored to identical |
| @@ -552,7 +557,7 @@ credentials already are, and the mint line records the rungs. |
| 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. |
| + These three pin R5. If the gap is ever closed, they 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 |
| @@ -668,24 +673,23 @@ Every citation was checked at main `8d8e4bae`. |
| | 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 |
| +## 16. Requests in flight when a pipeline is installed (R5) |
| §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.** 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. |
| +lands if the pointer is still byte for byte what it read. |
| + |
| +**Ruled (R5, Paul, 2026-10-05): accepted.** 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). |
| + |
| +**Not chosen.** Closing 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 changes the |
| +release store's concurrency model. If it is ever wanted it is its own |
| +spec. |