Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions docs/CLAIMS.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ by its quoted claim, and `tests/test_docs_audit.py` fails if a named row is not

| Claim | Code | Proof |
|---|---|---|
| "A lost reply is `AMBIGUOUS`, never `FAILED`, and a retry against an `AMBIGUOUS` effect is refused — until a human, or a `reconcile` hook, says what happened." | Only `NotExecuted` maps to `FAILED` — `_outcome` — `control.py:1325`; a retry against an `AMBIGUOUS` key is refused by `plan_reservation` — `effect.py:250`; the two things permitted to move the record on and nothing else — `resolve` — `cli/main.py:995` — and `Control._reconciled` — `control.py:2877` | `test_T1_a_lost_response_leaves_the_effect_ambiguous`, `test_T1_a_blind_retry_is_refused_and_never_reaches_the_remote`, `test_T160_there_is_no_reaper`, `test_T13_a_hook_answering_not_executed_moves_the_record_to_failed` |
| "A lost reply is `AMBIGUOUS`, never `FAILED`, and a retry against an `AMBIGUOUS` effect is refused — until a human, or a `reconcile` hook, says what happened." | Only `NotExecuted` maps to `FAILED` — `_outcome` — `control.py:1325`; a retry against an `AMBIGUOUS` key is refused by `plan_reservation` — `effect.py:250`; the two things permitted to move the record on and nothing else — `resolve` — `cli/main.py:1024` — and `Control._reconciled` — `control.py:2877` | `test_T1_a_lost_response_leaves_the_effect_ambiguous`, `test_T1_a_blind_retry_is_refused_and_never_reaches_the_remote`, `test_T160_there_is_no_reaper`, `test_T13_a_hook_answering_not_executed_moves_the_record_to_failed` |
| "The customer is refunded twice, and nothing in the stack noticed." — said of a stack without CTRLRun; the demo runs the same sequence with it, and counts the calls the remote received | `ctrlrun demo` scenario 1, which retries against a fake remote that counts its calls and prints the count | `test_T3_the_fake_remote_is_called_exactly_once`, `test_T1_a_blind_retry_is_refused_and_never_reaches_the_remote` |

## Protect your first action
Expand Down Expand Up @@ -94,14 +94,14 @@ by its quoted claim, and `tests/test_docs_audit.py` fails if a named row is not
| "every principal needs a grant and no grant means denied" | `NO_AUTHORITY` — the fail-closed default of `Authority.evaluate` (`authority.py:86`), reached for reads and for actions with no effect key alike | `test_T67_an_action_the_policy_allows_outright_still_needs_a_grant` |
| "A grant carries no `decision:`" | `_GRANT_KEYS` — `authority.py` — is a closed set that does not contain `decision` | `test_T73b_grant_refuses_what_the_loader_refuses` |
| "combine as the **stricter of the two**" | `Control.evaluate` returns the combined result — `control.py`; a denial on either axis is a denial | `test_T70_the_stricter_of_the_two_wins` |
| "narrow it at runtime with `ctrlrun delegate`" | `Control.delegate` — `control.py:4165`; `Authority.plan_delegation` — `authority.py:1549`; `ctrlrun delegate` — `cli/main.py:1522` | `test_t75_the_delegation_authorizes_an_action_within_its_limits` |
| "narrow it at runtime with `ctrlrun delegate`" | `Control.delegate` — `control.py:4165`; `Authority.plan_delegation` — `authority.py:1549`; `ctrlrun delegate` — `cli/main.py:1551` | `test_t75_the_delegation_authorizes_an_action_within_its_limits` |
| "provably a subset of its parent on every dimension, at creation and again at every evaluation" | `contained_dimension` — `authority.py:986` — runs from `plan_delegation` (`authority.py:1549`) **and** from the chain walk in `Authority.evaluate` (`authority.py:1296`) | `test_t76_each_dimension_violated_alone`, `test_t77b_a_narrowed_parent_narrows_its_children` |
| "provably a subset of its parent on every dimension, at creation and again at every evaluation; a consequence budget is consumed inside the reservation's own transaction, and a rolling window bounds what may start rather than recalling what already did" | Containment as in the row above. The budget: `check_charges` — `state.py:575` — is evaluated inside `reserve_effect`'s own transaction on all three backends, and `_charges_for` — `authority.py:1404` — charges every ancestor in the chain. The window is rolling and bounds the next reserve only: `_spent` sums `[now - window, now]` and nothing reads it again after a reservation is taken | `test_T408_a_charge_and_its_reservation_are_one_transaction`, `test_T409_N_processes_racing_one_budget_spend_at_most_the_limit`, `test_T412b_every_ancestor_is_charged_through_a_real_chain`, `test_T408c_the_rolling_window_forgets` |
| "omitting a dimension the parent constrains is rejected rather than inherited" | `contained_dimension` treats an absent child dimension as unconstrained and therefore wider — `authority.py:986`; the subject half is `_subject_contained` (`authority.py:1065`) | `test_t81_omission_is_not_unlimited`, `test_T73b_a_subject_addressed_to_every_principal_is_refused`, `test_t76_each_dimension_violated_alone` |
| "`ctrlrun revoke` cuts a chain of any depth with one write" | `Control.revoke` — `control.py:4505` — writes one row — `revoke_delegation` — `state.py:841` and visits no children; every evaluation walks to the root | `test_t78_a_revoked_parent_denies_its_grandchild`, `test_put_delegation_is_never_an_upsert` |
| "`mode: observe` … records what *would* have been blocked, without blocking anything" | `_parse_mode` — `policy.py:778`; `Control._observed` — `control.py:1708`; `_WouldHave` — `receipt.py:346`; `ReceiptResult.OBSERVED` — `receipt.py:258` | `test_T82_observe_executes_what_enforce_would_deny`, `test_T83_a_duplicate_is_recorded_and_still_runs` |
| "One top-level line" | `mode:` is refused anywhere but the top level — `reject_nested_mode`, `policy.py:778` | `test_T84_mode_is_refused_anywhere_but_the_top_level` |
| "`ctrlrun stats` gives you the numbers" | `stats` — `cli/main.py:1326`; counted from `would_have.blocked_reason` and nothing else | `test_T86_stats_counts_what_observe_mode_recorded`, `test_T86_stats_reaches_no_network` |
| "`ctrlrun stats` gives you the numbers" | `stats` — `cli/main.py:1355`; counted from `would_have.blocked_reason` and nothing else | `test_T86_stats_counts_what_observe_mode_recorded`, `test_T86_stats_reaches_no_network` |
| "It is not a dry run: it executes" | `_observed` runs the executor on every path, including the ones enforce mode would have refused — `control.py:1708` | `test_T82_observe_executes_what_enforce_would_deny`, `test_T83_an_executor_that_fails_on_a_held_key_still_writes_the_record` |

## Prove it holds in your setup
Expand Down Expand Up @@ -155,7 +155,7 @@ catalogue, `GUARANTEES` (`verify/guarantees.py:55`).
| "It will not *knowingly* execute the same logical effect twice, and will never treat an unknown outcome as a failure." | `plan_reservation` — `effect.py:250` (refuse retry on `AMBIGUOUS`) and `_outcome` — `control.py:2223` (only `NotExecuted` → `FAILED`) | `test_T1_a_blind_retry_is_refused_and_never_reaches_the_remote`, `test_T1_a_lost_response_leaves_the_effect_ambiguous` |
| "a lost connection during `COMMIT` ... are `AMBIGUOUS`" | `_resolve_lost_insert` — `postgres.py:960`; `_resolve_lost_update` — `postgres.py:1586`; only `NotExecuted` maps to `FAILED` — `_outcome` — `control.py:2223` | `test_T155_a_connection_killed_during_commit_is_resolved_by_the_re_read`, `test_T155_no_effect_is_ever_recorded_failed_by_a_lost_commit` |
| "the store re-reads the row to find out which" | The six branches, named and logged — `A2_LANDED` — `postgres.py:154` | `test_T155b_a_landed_commit_on_a_transition_is_seen_as_landed`, `test_T155d_a_commit_the_server_never_received_retries_the_insert` |
| "A crashed worker's effect stays `AMBIGUOUS` until a human runs `ctrlrun resolve` or a `reconcile` hook asks the remote what happened" | An expired lease is `AMBIGUOUS` and nothing sweeps it — `LEASE_EXPIRED` — `effect.py:174`; who resolved it — `resolved_by` — `effect.py:210`; `resolve` — `cli/main.py:995` | `test_T159_ambiguous_survives_a_restart_and_still_refuses_a_blind_retry`, `test_T160_there_is_no_reaper`, `test_T161_a_human_resolution_records_who` |
| "A crashed worker's effect stays `AMBIGUOUS` until a human runs `ctrlrun resolve` or a `reconcile` hook asks the remote what happened" | An expired lease is `AMBIGUOUS` and nothing sweeps it — `LEASE_EXPIRED` — `effect.py:174`; who resolved it — `resolved_by` — `effect.py:210`; `resolve` — `cli/main.py:1024` | `test_T159_ambiguous_survives_a_restart_and_still_refuses_a_blind_retry`, `test_T160_there_is_no_reaper`, `test_T161_a_human_resolution_records_who` |
| "the only thing besides a human permitted to move a record out of `AMBIGUOUS`" | `Control._reconciled` — `control.py:2877`; `RECONCILED_STATES` — `effect.py` | `test_T13_a_hook_answering_not_executed_moves_the_record_to_failed`, `test_T14_a_hook_answering_committed_refuses_the_retry_as_a_duplicate` |
| "and only in the direction its answer points" | `"unknown"` is absent from `RECONCILED_STATES` — `effect.py` | `test_T15_a_hook_that_cannot_answer_leaves_the_record_ambiguous` |
| "Unknown action, missing policy, malformed policy, missing principal, missing or mismatched approval and inconsistent state are all `deny`." | `Policy.evaluate` — `policy.py:657`; `Policy.from_file` — `policy.py:814`; `_refuse_no_principal` — `control.py:4851`; `_authorize_and_reserve` — `state.py:1341` | `test_T6_unknown_action_raises_ActionDenied_with_reason_unknown_action`, `test_malformed_policy_document_is_a_policy_error`, `test_T62_a_declining_provider_with_no_context_is_no_principal`, `test_T2_a_mutated_action_presenting_the_approval_raises_ApprovalMismatch` |
Expand All @@ -173,7 +173,7 @@ catalogue, `GUARANTEES` (`verify/guarantees.py:55`).
| "migrations are automatic at open, forward-only" | `migrate` — `migrations.py:723`, called from both stores' constructors; `HEAD` — `migrations.py:504` | `test_T147_a_v05_database_migrates_and_keeps_every_row`, `test_T150_reopening_does_not_rerun` |
| "An older binary against a newer schema refuses immediately" | `_refuse` — `migrations.py:649`; `SchemaMismatch` — `errors.py` | `test_T148_an_older_binary_refuses_a_newer_database`, `test_T148_no_other_table_is_read_before_the_refusal` |
| "Releases carry PyPI provenance attestations from GitHub Actions" | `.github/workflows/publish.yml` — `pypa/gh-action-pypi-publish` pinned at v1.14.2, which generates and uploads PEP 740 attestations by default since v1.11.0 (its release notes, read 2026-09-06), with no `attestations: false`; the `pypi` job's only permission is `id-token: write` | `test_the_publish_workflow_attests_through_trusted_publishing`, `test_every_action_is_pinned_to_a_commit` |
| "`ctrlrun approve`, `deny`, `resolve`, `inspect`, `receipts` and `stats` work from the shell against any store" | `approve` — `cli/main.py:395`; `receipts` — `cli/main.py:473`; `effects` — `cli/main.py:937`; `resolve` — `cli/main.py:995`; `inspect` — `cli/main.py:1039`; `stats` — `cli/main.py:1074`; every one takes `--store-url` (SPEC-v0.6 §9.4) | `test_T10_resolve_failed_permits_a_retry`, `test_T18_inspect_json_emits_the_inspection_schema`, `test_T86_stats_counts_what_observe_mode_recorded`, `test_verify_chain_reads_a_postgres_store_through_store_url` |
| "`ctrlrun approve`, `deny`, `resolve`, `inspect`, `receipts` and `stats` work from the shell against any store" | `approve` — `cli/main.py:395`; `receipts` — `cli/main.py:473`; `effects` — `cli/main.py:966`; `resolve` — `cli/main.py:1024`; `inspect` — `cli/main.py:1068`; `stats` — `cli/main.py:1355`; every one takes `--store-url` (SPEC-v0.6 §9.4) | `test_T10_resolve_failed_permits_a_retry`, `test_T18_inspect_json_emits_the_inspection_schema`, `test_T86_stats_counts_what_observe_mode_recorded`, `test_verify_chain_reads_a_postgres_store_through_store_url` |
| "`WebhookApprovalProvider` sends an approval request to a webhook, such as Slack, and takes the answer back through the same grant calls" | `WebhookApprovalProvider` — `webhook.py:143` — one signed POST on `APPROVAL_REQUESTED`; the inbound answer lands through `grant_approval` / `deny_approval` like the CLI's | `test_T27_the_outbound_post_carries_a_signature_over_the_exact_bytes_sent`, `test_T27_the_payload_carries_what_the_spec_names` |
| "one OpenTelemetry span per action, one span event per step" | `OTelEventSink` — `otel.py:47` | `test_T29_one_action_produces_one_span_named_for_the_action`, `test_T29_every_event_becomes_a_span_event_named_by_its_type` |
| "argument values stay out of it unless you ask for them" | `OTelEventSink(arguments=...)` — `otel.py:47` | `test_T29_argument_values_are_not_attributes_by_default` |
Expand Down
23 changes: 18 additions & 5 deletions docs/production/retention.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -67,19 +67,32 @@ reviewed, so a person places it and a person ends it.
- **It does not run on a schedule.** Nothing sweeps, nothing reaps, and no hold expires. You run
the command, or your scheduler does.
- **It does not make a checkpoint unforgeable.** Anyone who can insert receipts can write a
checkpoint row. What narrows that is the anchor: a prune must anchor its checkpoint before
deleting, and an erasure with no anchored checkpoint behind it reports `anchor_broken`.
checkpoint row, and anyone who can write that row can write a row in the local `anchors` table
beside it. What narrows both is the provider: a checkpoint supersedes the receipts below it
only when **the provider still returns an anchor**, and only when that anchor's `(seq, hash)`
is the pair the checkpoint claims. A local row the provider does not confirm buys nothing, and
an erasure with no anchored checkpoint behind it reports `anchor_broken`.
- **It does not decide what you may delete.** Retention is not in your policy document,
deliberately: a policy key would make pruning subject to `require_approved_policy`, and a
deployment that had not approved its current policy could then never prune. What authorises a
prune is shell access to the store, which policy does not mediate. Put a human in front of the
command, where you already are for every other destructive operation on your database.

## What the prune itself leaves behind

Two receipts, not one, and they are distinguishable: the first records the request (`--through`,
`--older-than`, `--reason`) as `proposed`, and the second records what became of it as
`completed` or `refused`. A prune that was refused and a prune that succeeded therefore do not
leave the same bytes, which is the only reason the record of a refusal is worth keeping.

**Verified by** `T540` for the chain verifying across the gap, with a naive prefix delete as its
negative control; `T543` for a store that already had a break; `T545` for a hold; `T546b` for the
budget window, where pruning a `COMMITTED` row inside it manufactures authority; `T547b` for a
forged checkpoint with no anchor behind it; and `T549`, which races two prunes in separate OS
processes against a real Postgres server.
budget window, where pruning a `COMMITTED` row inside it manufactures authority; `T550` and
`T559` for a checkpoint the provider does not confirm, including a forged local `anchors` row
that names the checkpoint's own pair; `T552` for a `--through` above the head; `T554` for a
checkpoint asserting a pair that never existed; `T555` for the two receipts; `T551` and `T558`
for the prune holding its lock across every write on SQLite and on Postgres; and `T549`, which
races two prunes in separate OS processes against a real Postgres server.

## Next

Expand Down