A ceiling the operator sets, decided on the attempt the store assigned

.github/workflows/ci.yml

@@ -122,10 +122,11 @@ jobs:
           echo "templates: $TEMPLATES ($TEMPLATES_NA not applicable)"
           test "$AUTHORITY" = "verified 13/13"
           # G13 is N/A on SQLite, the action's default store: SQLite has no clock of its own
-          # to diverge from (SPEC-v0.7 §8.9). G16 is graded on both documents (§8.9).
-          test "$AUTHORITY_NA" = "1"
+          # to diverge from; G15 is N/A because neither document declares `max_attempts`.
+          # G16 is graded on both: verify brings its own precondition provider (SPEC-v0.7 §8.9).
+          test "$AUTHORITY_NA" = "2"
           test "$TEMPLATES" = "verified 7/7"
-          test "$TEMPLATES_NA" = "7"
+          test "$TEMPLATES_NA" = "8"
           test -s verify-badge.json
           test -s verify-report.json
           test -s verify-report.xml

CHANGELOG.md

@@ -29,6 +29,35 @@ any change to one appears here.
   Postgres `--store-url` and `N/A` on SQLite, and the catalogue moves to
   `ctrlrun.guarantees/v3`; the store conformance suite gains a `clock` case, `not_applicable`
   on SQLite and the in-memory store because neither has a clock of its own.
+- **The attempt ceiling, `max_attempts`** (SPEC-v0.7 §5, item 4, and the amendment to
+  `docs/SPEC-v0.1.md` §5.4). A new action-entry policy key, an integer of at least 1, bounding
+  the **attempts** that may execute on one effect key, the first included: `max_attempts: 3` is
+  the first attempt and two renewals. It needs `schema: ctrlrun.policy/v5`, a new schema version
+  that is a superset of `v4` as `v4` is of `v3`; `0`, a negative, a `bool`, a float, a string and
+  a mapping are each a `PolicyError` at load, naming the key, the action and the line. The ceiling
+  is inside the policy hash, so a receipt records which one refused an attempt.
+  **An attempt, not an executor invocation**: a `Suspended` executor holds its reservation and
+  every `Control.resume` runs on that same attempt, so an elicitation loop is one dispatch however
+  many rounds it takes. The gateway bounds those with `max_elicitation_rounds`; a direct
+  `Control.resume` caller has no bound, and this adds none.
+  **The decision is taken on the attempt number the store assigned**, after the reservation and
+  before the executor, because two callers that both read attempt *N-1* would both pass a read
+  taken before reserving. Above the ceiling the executor is not called, the record is released as
+  `FAILED` with an error naming the ceiling, `EFFECT_RESERVATION_REFUSED` carries
+  `reason: "attempt_ceiling"` with the attempt and the ceiling, a `blocked` receipt is written,
+  and `ActionDenied(reason="attempt_ceiling")` is raised. The refused attempt number is **spent**:
+  raising `max_attempts` from 2 to 4 after a refusal buys one further dispatch, not two. A read of
+  the record before the approval gate refuses the ordinary sequential case earlier, writing
+  nothing, spending no presented approval and creating no approval request; it refuses only a
+  `FAILED` record and is never the guarantee. **On any other route the approval gate comes
+  first**, so on an `APPROVE` action a human can be asked, and answer, for an attempt that is then
+  refused: a wasted answer, never an execution, and `docs/SPEC-v0.7.md` §5.2 and §5.5 say so
+  rather than closing it. In observe mode the refusal is recorded as `would_have.blocked_reason:
+  "attempt_ceiling"` and the action runs. Verify gains **G15**, and G5 and G14 now select only an
+  action whose ceiling permits a renewal, reporting `N/A` where the ceiling is the only reason
+  they cannot, because each one's control *is* a renewal and `max_attempts: 1` would otherwise
+  report a correct kernel as a failure. No new error type, no new event type, no new `StateStore`
+  method, no new `Control` method, and no CLI change.
 - **The provider idempotency token** (SPEC-v0.7 §4, item 3). `ctrlrun.idempotency_token()`, a new
   zero-argument accessor re-exported at package import, answers inside an executor with the token
   of the attempt it is running: `ctrlrun.effect.idempotency_token_for(effect_key, attempt)`, a
@@ -94,8 +123,15 @@ any change to one appears here.
   no action requires approval. The store conformance suite gains a `precondition-fingerprint` case
   and a broken-store fixture that fails it by name.
 
+
 ### Changed
 
+
+- **An action entry may declare `max_attempts`, and a renewal over `FAILED` can now be bounded.**
+  This is stricter than 0.6.1 only where an operator asks for it: an action that declares no
+  `max_attempts` renews without bound, exactly as before, and every document that loaded at 0.6.1
+  loads unchanged. There is no default ceiling, and no value of the key means "unlimited".
+
 - **`ctrlrun.receipt/v4`**, with `precondition_at_request` and `precondition_at_recheck`, and the
   first receipt-schema bump that does not report older receipts as altered. A receipt read from a
   store is now hashed as the document it was read from (`docs/SPEC-v0.7.md` §6.11, amending
@@ -107,8 +143,9 @@ any change to one appears here.
   own `v1` or `v2` label and keys where 0.6.1 showed `v3`. Upgrade every reader before any writer:
   a `v4` JSONL line handed to 0.6.1 rehashes wrongly.
 - **`ctrlrun verify` prints each distinct note once**, where it printed only the first note in the
-  report, which would have dropped G16's beneath G3's. CI's `verify` job expects `verified 12/12`
-  and `verified 7/7`.
+  report, which would have dropped G16's beneath G3's. CI's `verify` job expects `verified 13/13`
+  with two not applicable, and `verified 7/7` with eight, measured from a run of the merged
+  catalogue rather than carried over from either branch.
 - **A receipt chain reader no longer stops at a row it cannot hash.** A stored document holding a
   value with no canonical form (a float, a lone surrogate) made `verify_chain` raise, so one
   tampered row ended the walk: `ctrlrun receipts --verify-chain` exited with no report and a forged

docs/SPEC-v0.1.md

@@ -336,6 +336,15 @@ When a new action arrives for an `effect_key` that already has a record:
 
 `FAILED` means the executor *proved* nothing happened (§5.5). That is the only state that permits automatic retry.
 
+**Amendment (v0.7, `SPEC-v0.7.md` §5).** The `FAILED` row is bounded where the action's policy entry declares `max_attempts` (`schema: ctrlrun.policy/v5`): at most `max_attempts` attempts execute on one effect key, the first included.
+
+| Existing state | New reservation | Raised |
+|---|---|---|
+| `FAILED` at attempt *n*, and no `max_attempts`, or *n* + 1 ≤ `max_attempts` | allowed: attempt *n* + 1, same key | none |
+| `FAILED` at attempt *n*, and *n* + 1 > `max_attempts` | refused. Where the record is read before the approval gate, nothing is written. Otherwise the store assigns attempt *n* + 1, and the record is released as `FAILED` without the executor being called | `ActionDenied(reason="attempt_ceiling")` |
+
+The decision is taken on the attempt number the store assigned to the reservation, after the reservation and before the executor; a read of the record before the approval gate may refuse the same renewal earlier and is never the only check. The refusal appends `EFFECT_RESERVATION_REFUSED` with `data.reason = "attempt_ceiling"` and writes a `blocked` receipt. `FAILED` is still the only state that permits an automatic retry: the ceiling removes permission from that row and grants none to any other.
+
 ### 5.5 Executor outcome mapping
 
 The wrapped function is the executor. Its result is mapped: