Bring the site up to the library's v0.7 main: 15 guarantees, the token, the ceiling, preconditions

docs.json

@@ -301,6 +301,7 @@
               "docs/reference/api/conformance-store-run",
               "docs/reference/api/context",
               "docs/reference/api/gateway-serve",
+              "docs/reference/api/idempotency_token",
               "docs/reference/api/jwt_identity-JWTIdentityProvider",
               "docs/reference/api/needs_approval",
               "docs/reference/api/otel-OTelEventSink",

docs.mdx

@@ -219,8 +219,8 @@ the framework's own interrupt, and a framework with no such primitive does not n
 
 {/* generated from the suite, pyproject and the soak (mdx) — run the generator */}
 - **Version 0.6.1**, on [PyPI](https://pypi.org/project/ctrlrun/), Python 3.11 and later.
-- **4,513 tests**, every version specified before it was written and every requirement mutation-tested.
-- **12 guarantees you can check in your own setup**, with `ctrlrun verify` against your policy, on your store's backend, in a scratch store it creates.
+- **4,999 tests**, every version specified before it was written and every requirement mutation-tested.
+- **15 guarantees you can check in your own setup**, with `ctrlrun verify` against your policy, on your store's backend, in a scratch store it creates.
 - **One host: a file.** SQLite, no server, no ops. **Many hosts: Postgres**, the same guarantees, graded by the same suite.
 - **Soaked for 20m 0s on postgres**: 889,735 actions, 0 unattributed ambiguous outcomes, positive control fired. Nothing here establishes what only accumulates over days. [What it does not establish](https://ctrlrun.dev/docs/production/soak).
 - **Each receipt carries the hash of the one before it**, so an alteration is detected and named.

docs/OWASP-AGENTIC-TOP10.md

@@ -75,6 +75,9 @@ mechanism, not the entry.
 | **G10** unknown exception is ambiguous | `NotExecuted` is the only outcome that means "the remote did nothing". Everything else, timeouts included, is `AMBIGUOUS`. | `ASI08:2026` | The mapping from an executor's exception to an outcome is asymmetric on purpose: a timeout is not a failure, so a framework's retry-on-error cannot be the thing that decides whether money moved twice. |
 | **G11** an altered receipt is detected | Each receipt carries the hash of the one before it. Altering, deleting or reordering one breaks the chain, and the break is reported by name — `content_altered`, `hash_missing`, `link_broken`, `missing`, `head_mismatch`, `unchained` — and by `seq`. | `ASI09:2026` (partly) | The evidence an operator reads after an incident is the thing an attacker who got that far has the most reason to edit. This does not stop them: it makes **changing what a receipt says, while keeping the receipts after it**, cost a rewrite of all of them plus the head, rather than one statement. What it does not close is the end of the log — erasing a suffix, or appending to it, each cost two statements and are undetected, because the head is a row in the same database and not an external anchor. v0.6 has no anchor and claims none. It is **not** a signature and says nothing about who wrote the log; somebody who can rewrite every row including the head recomputes the chain and it verifies, and `THREAT_MODEL.md` still lists a malicious administrator as out of scope. |
 | **G13** clock divergence is named | The kernel measures how far this host's clock disagrees with the store's, on a store that has a clock of its own, and reports the divergence as `CLOCK_SKEW_DETECTED` when it passes the configured threshold. It changes no decision: every lease is still compared against the application clock exactly as before. | `ASI08:2026` (partly) | Once the store is shared, each host brings its own clock, and the failure is fail-closed and therefore quiet. A host running ahead sees a live lease as expired and marks `AMBIGUOUS` a record whose real holder is mid-flight and about to succeed; a host running behind refuses for longer than it should. Neither says why. What this closes is the silence, not the skew: an operator reading a receipt learns that two clocks disagreed and by how much, so the response to the first failure is not itself the second one. It does not synchronize anything, and a skew below the threshold is not reported. |
+| **G14** token changes across a renewal | `ctrlrun.idempotency_token()` answers inside an executor with a token derived from `(effect_key, attempt)`: stable within one attempt, including across a resume, and different after a renewal. Send it to a provider as its idempotency key. | `ASI08:2026` (partly) | A provider handed the effect key alone would answer the one retry the kernel permits, permitted *because the executor proved nothing happened*, with the cached failure of the attempt that failed. A token that moves with the attempt keeps a provider's cache from becoming a second source of stale outcomes. What it is for is reconciliation, a deterministic handle to ask a provider what became of an attempt whose outcome is unknown; it does not make a retry safe, and after `AMBIGUOUS` the kernel still refuses one. It is unique only as far as the operator's effect keys are, and nothing here checks two stores sharing a provider account. |
+| **G15** renewal past the ceiling refused | An action entry may declare `max_attempts`; above it the executor is not called, the record is released as `FAILED`, a `blocked` receipt names the ceiling, and `ActionDenied(reason="attempt_ceiling")` is raised. The refused attempt number is spent. | `ASI08:2026` (partly), `ASI10:2026` (partly) | Without a ceiling a renewal after `FAILED` is unbounded, so an agent that keeps proposing an action that keeps failing keeps dispatching, and one human yes on an `APPROVE` action bought unlimited dispatches. The ceiling is the operator's, not the kernel's: an entry that declares none renews exactly as before, and the decision is taken on the attempt number the store assigned, after the reservation, so two callers cannot both pass a read taken before reserving. It bounds attempts on one effect key, not what an agent does across many. |
+| **G16** a moved fingerprint is refused | Under `APPROVE`, a `preconditions=` provider's answer is kept as a `sha256:` fingerprint on the request; on the presenting pass it is computed again, strictly before the store call that consumes the approval, and a difference is refused with `ApprovalMismatch(reason="precondition_changed")`, reserving nothing and leaving the approval granted. | `ASI09:2026` (partly), `ASI01:2026` (partly) | A human's yes was given against the world as it was; this refuses the action where the state the approval depended on has moved since. It **narrows** the window between approval and execution and does not close it: the comparison is a network call outside the atomic reservation write, and a change that lands between the comparison and the reservation is not refused. What the provider looks at is in the operator's code, which verify does not read; verify grades the check with a provider of its own. |
 
 ---
 

docs/cookbook/verify-in-github-actions.mdx

@@ -66,7 +66,6 @@ CTRLRun verify — ctrlrun 0.6.1, catalogue ctrlrun.guarantees/v3
 policy     /home/runner/work/agent/agent/ctrlrun.yaml (ctrlrun.policy/v2, mode: enforce)
 authority  none
 store      sqlite, scratch (created and destroyed for this run)
-
 G1   mutated approval refused         PASS  k8s.delete_namespace
 G2   replayed approval refused        PASS  k8s.delete_namespace
 G3   duplicate effect refused         PASS  k8s.delete_namespace
@@ -79,8 +78,19 @@ G9   delegation cannot escalate       N/A   no authority section
 G10  unknown exception is ambiguous   PASS  k8s.delete_namespace
 G11  an altered receipt is detected   PASS  k8s.delete_namespace
 G13  clock divergence is named        N/A   the store verify was given reads only the application's clock, so there is no second clock to diverge from; pass --store-url postgresql://… to grade this
-
-9/9 declared guarantees pass. 3 not applicable: G8, G9, G13.
+G14  token changes across a renewal   PASS  k8s.delete_namespace (attempt 1 and its renewal carry different tokens)
+G15  renewal past the ceiling refused N/A   no action verify can drive to allow or approve declares both `effect:` and `max_attempts`
+G16  a moved fingerprint is refused   PASS  k8s.delete_namespace
+                                            (verify supplies its own precondition provider; whether
+                                            your @protect declares one is in your code, which verify
+                                            does not read. The gateway and the ACS hook cannot name a
+                                            provider at all, and refuse an approval that carries a
+                                            fingerprint)
+                                            (a token is unique only as far as your effect keys are:
+                                            two stores sharing a provider account must not produce the
+                                            same effect-key string for different effects, and nothing
+                                            here can check that)
+11/11 declared guarantees pass. 4 not applicable: G8, G9, G13, G15.
 ```
 
 The first line is on stderr, from G7's own scenario driving an action with no principal — the
@@ -89,9 +99,9 @@ the first action that fits each scenario in alphabetical order; which one appear
 about it. The `policy` line is the resolved absolute path, so yours will differ.
 
 
-Two guarantees are not applicable because the policy has no `authority:` section; they are
-listed with the reason and excluded from the denominator. Green means nothing that could be
-checked was wrong.
+Four guarantees are not applicable: no `authority:` section (G8, G9), no second clock in a
+scratch store (G13), no `max_attempts` to refuse past (G15). Each is listed with its reason and
+excluded from the denominator. Green means nothing that could be checked was wrong.
 
 ## The receipt
 

docs/guides/verify-in-ci.mdx

@@ -36,7 +36,6 @@ guarantees pass.
     policy     /home/you/agent/ctrlrun.yaml (ctrlrun.policy/v2, mode: enforce)
     authority  none
     store      sqlite, scratch (created and destroyed for this run)
-
     G1   mutated approval refused         PASS  k8s.delete_namespace
     G2   replayed approval refused        PASS  k8s.delete_namespace
     G3   duplicate effect refused         PASS  k8s.delete_namespace
@@ -49,19 +48,30 @@ guarantees pass.
     G10  unknown exception is ambiguous   PASS  k8s.delete_namespace
     G11  an altered receipt is detected   PASS  k8s.delete_namespace
     G13  clock divergence is named        N/A   the store verify was given reads only the application's clock, so there is no second clock to diverge from; pass --store-url postgresql://… to grade this
-
-    9/9 declared guarantees pass. 3 not applicable: G8, G9, G13.
+    G14  token changes across a renewal   PASS  k8s.delete_namespace (attempt 1 and its renewal carry different tokens)
+    G15  renewal past the ceiling refused N/A   no action verify can drive to allow or approve declares both `effect:` and `max_attempts`
+    G16  a moved fingerprint is refused   PASS  k8s.delete_namespace
+                                                (verify supplies its own precondition provider; whether
+                                                your @protect declares one is in your code, which verify
+                                                does not read. The gateway and the ACS hook cannot name a
+                                                provider at all, and refuse an approval that carries a
+                                                fingerprint)
+                                                (a token is unique only as far as your effect keys are:
+                                                two stores sharing a provider account must not produce the
+                                                same effect-key string for different effects, and nothing
+                                                here can check that)
+    11/11 declared guarantees pass. 4 not applicable: G8, G9, G13, G15.
     ```
 
-    Two things about that output. The first line is on **stderr**, from G7's own scenario: it
-    drives an action with no principal and the refusal logs, which is the guarantee passing and
-    not a problem. And every row names `k8s.delete_namespace` rather than the refund — verify
-    exercises one action per guarantee and takes the **first that fits, in alphabetical order**,
-    so which of your actions appears is not a judgement about it.
+    The first line is on **stderr**, from G7's own scenario: an action with no principal is
+    refused and the refusal logs, which is the guarantee passing. Every row names
+    `k8s.delete_namespace` because verify takes the **first action that fits, in alphabetical
+    order**, not because of anything about the refund.
 
-    Two guarantees are not applicable: this policy has no `authority:` section, so nothing
-    about grants can be exercised. They are reported with the reason, excluded from the
-    denominator and listed separately. Never `11/11`, and no flag folds them in.
+    Four guarantees are not applicable: no `authority:` section (G8, G9), no second clock in a
+    scratch store (G13), no `max_attempts` to refuse past (G15). Each is reported with its
+    reason, excluded from the denominator and listed separately. Never `15/15`, and no flag
+    folds them in.
   </Step>
 
   <Step title="Add the action">
@@ -122,10 +132,9 @@ acted is invisible to it. The badge does not mean secure, safe, compliant, certi
 - Exit 2, `mode: observe`: verify refuses an observed configuration, because observe mode
   executes what enforce mode would refuse and nothing can be proved about it.
 - Exit 2, *nothing was checked and nothing is claimed*: **no** guarantee was applicable, so
-  `0/0` — which is never a pass. In practice that means an `actions:` map with nothing in it. A
-  policy with one `allow` action and no `approve` rule, no `effect:` template and no grants is
-  not this case: it exits 0 with `4/4` and seven not applicable, because the fail-closed and
-  unknown-outcome guarantees still have something to exercise.
+  `0/0` — which is never a pass. In practice that means an `actions:` map with nothing in it;
+  a policy with one `allow` action still exercises the fail-closed and unknown-outcome
+  guarantees.
 - Exit 1: a guarantee failed. The report names the scenario and the action; that is a bug
   report, not a configuration problem.
 

docs/production/index.mdx

@@ -28,8 +28,8 @@ need. `test_the_first_line_of_the_section_says_which_store_and_why` asserts the
 
 {/* generated from the suite, pyproject and the soak (full) — run the generator */}
 - **Version 0.6.1**, on [PyPI](https://pypi.org/project/ctrlrun/), Python 3.11 and later.
-- **4,513 tests**, every version specified before it was written and every requirement mutation-tested. [Read more](/docs/how-this-is-built).
-- **12 guarantees you can check in your own setup**, with `ctrlrun verify` against your policy, on your store's backend, in a scratch store it creates. [Read more](/docs/security/verify-guarantees).
+- **4,999 tests**, every version specified before it was written and every requirement mutation-tested. [Read more](/docs/how-this-is-built).
+- **15 guarantees you can check in your own setup**, with `ctrlrun verify` against your policy, on your store's backend, in a scratch store it creates. [Read more](/docs/security/verify-guarantees).
 - **One host: a file.** SQLite, no server, no ops. **Many hosts: Postgres**, the same guarantees, graded by the same suite. [Read more](/docs/production/postgres).
 - **Soaked for 20m 0s on postgres**: 889,735 actions, 0 unattributed ambiguous outcomes, positive control fired. Nothing here establishes what only accumulates over days. [Read more](/docs/production/soak).
 - **Each receipt carries the hash of the one before it**, so an alteration is detected and named. [Read more](/docs/production/receipt-integrity).

docs/reference/api/Approval.mdx

@@ -5,7 +5,7 @@ description: "A human's grant, bound to one `action_hash` (SPEC-v0.1 §4.1)."
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.Approval` — class, defined at `src/ctrlrun/approval.py:111`
+`ctrlrun.Approval` — class, defined at `src/ctrlrun/approval.py:125`
 
 ```python
 from ctrlrun import Approval

docs/reference/api/ApprovalProvider.mdx

@@ -5,7 +5,7 @@ description: "How a human is asked, and how the answer comes back (SPEC-v0.1 §4
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.ApprovalProvider` — class, defined at `src/ctrlrun/approval.py:304`
+`ctrlrun.ApprovalProvider` — class, defined at `src/ctrlrun/approval.py:318`
 
 ```python
 from ctrlrun import ApprovalProvider

docs/reference/api/ApprovalRequest.mdx

@@ -5,7 +5,7 @@ description: "A pending question for a human: may this exact action run? (SPEC-v
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.ApprovalRequest` — class, defined at `src/ctrlrun/approval.py:78`
+`ctrlrun.ApprovalRequest` — class, defined at `src/ctrlrun/approval.py:79`
 
 ```python
 from ctrlrun import ApprovalRequest
@@ -14,7 +14,7 @@ from ctrlrun import ApprovalRequest
 
 ```python
 class ApprovalRequest
-    def __init__(request_id: str, action_hash: str, action: Action, created_at: datetime, expires_at: datetime, policy_hash: str | None = None)
+    def __init__(request_id: str, action_hash: str, action: Action, created_at: datetime, expires_at: datetime, policy_hash: str | None = None, precondition_fingerprint: str | None = None)
 ```
 
 A pending question for a human: may this exact action run? (SPEC-v0.1 §4.1)

docs/reference/api/Condition.mdx

@@ -5,7 +5,7 @@ description: "One `<argument>_<op>: operand` test against an action's arguments
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.Condition` — class, defined at `src/ctrlrun/policy.py:297`
+`ctrlrun.Condition` — class, defined at `src/ctrlrun/policy.py:333`
 
 ```python
 from ctrlrun import Condition

docs/reference/api/Control.mdx

@@ -5,7 +5,7 @@ description: "Policy, state and evidence composed around a single action (SPEC-v
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.Control` — class, defined at `src/ctrlrun/control.py:280`
+`ctrlrun.Control` — class, defined at `src/ctrlrun/control.py:457`
 
 ```python
 from ctrlrun import Control

docs/reference/api/Decision.mdx

@@ -5,7 +5,7 @@ description: "What may happen to an action: exactly three outcomes in v0.1 (SPEC
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.Decision` — class, defined at `src/ctrlrun/policy.py:234`
+`ctrlrun.Decision` — class, defined at `src/ctrlrun/policy.py:270`
 
 ```python
 from ctrlrun import Decision

docs/reference/api/DelegationRecord.mdx

@@ -5,7 +5,7 @@ description: "One row of the `delegations` table (SPEC-v0.3 §5.2)."
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.DelegationRecord` — class, defined at `src/ctrlrun/state.py:372`
+`ctrlrun.DelegationRecord` — class, defined at `src/ctrlrun/state.py:380`
 
 ```python
 from ctrlrun import DelegationRecord

docs/reference/api/EffectRecord.mdx

@@ -5,7 +5,7 @@ description: "What a StateStore holds for one effect key (ARCHITECTURE §5)."
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.EffectRecord` — class, defined at `src/ctrlrun/effect.py:99`
+`ctrlrun.EffectRecord` — class, defined at `src/ctrlrun/effect.py:106`
 
 ```python
 from ctrlrun import EffectRecord

docs/reference/api/EffectState.mdx

@@ -5,7 +5,7 @@ description: "Where a logical effect stands (SPEC-v0.1 §5.2)."
 
 {/* generated by tools/docs_audit/render_api.py from the docstrings — edit the docstring, never this page */}
 
-`ctrlrun.EffectState` — class, defined at `src/ctrlrun/effect.py:74`
+`ctrlrun.EffectState` — class, defined at `src/ctrlrun/effect.py:81`
 
 ```python
 from ctrlrun import EffectState