Skip to content

A ceiling the operator sets, decided on the attempt the store assigned - #145

Merged
arpanghoshal merged 5 commits into
mainfrom
v0.7/4-attempt-ceiling
Sep 11, 2026
Merged

A ceiling the operator sets, decided on the attempt the store assigned#145
arpanghoshal merged 5 commits into
mainfrom
v0.7/4-attempt-ceiling

Conversation

@arpanghoshal

Copy link
Copy Markdown
Member

v0.7 item 4 (SPEC-v0.7 §5, G15), carrying the amendment to SPEC-v0.1 §5.4, the oldest binding rule in the repository.

grep -rn "max_attempt\|attempt >" src/ returned nothing before this branch. plan_reservation did attempt=record.attempt + 1 with no ceiling, so an executor that raises NotExecuted on every call was unlimited provider dispatches, each recorded as an ordinary retry. Every individual renewal is correct, because the executor proved nothing happened. The gap was between "the only automatic retry", which reads as one, and what the code permitted, which was unbounded.

What it does

  • max_attempts, a per-action policy key, integer at least 1. 0, negatives, bools, floats, strings, mappings, lists and null are refused at load, naming the key, the action and the line. Absent means no ceiling: today's behaviour, and G15 is then N/A with a reason true of the operator's document.
  • The decision is taken on the attempt number the store assigned. reserve_effect and consume_approval_and_reserve are frozen and cannot carry a ceiling, so Control compares the returned reservation.attempt before the executor is called. Two callers who both read N-1 cannot both get through. A read before reserving is a fast path that saves the write, never the guarantee, and it refuses only a FAILED record.
  • Above the ceiling: the executor is not called, the evidence is written first (event, then blocked receipt), the record is released FAILED, and ActionDenied(reason="attempt_ceiling") is raised. No new error type, event type, StateStore method, Control method, CLI command or flag.
  • ctrlrun.policy/v5, a superset of v4. The three equality gates became one ordering helper, so the next version needs no fourth edit.
  • G15 in verify, reached through the reconcile route, because a G15 the fast path alone could satisfy would be green with the guarantee deleted.

What the reviews changed

Two blocking findings, and the fix for the first one was three sentences, not code. §5.5 claimed the adapter path was the only route on which a human is asked about an attempt the ceiling will refuse. It is not: on the kernel's own reconcile route a new approval is requested, granted and consumed for an attempt that can never run. Closing it would mean re-reading between the reconcile and the second _take, which would leave the check with no seamless public route, so G15 would grade a guarantee that could not have failed. The honest disposition is to state the cost. §5.5 now says the list is not exhaustive and tells the reader to assume there are others; a test pins the behaviour so the claim cannot drift back.

The second: G15's N/A reason claimed "every declared max_attempts is above verify's bound" while describing only the selectable actions. It is now scoped to what the selection can see, with a test where a deny-only action declares a low ceiling.

A mutation row was deleted, not fixed. The widened except CTRLRunError turned out to catch only to re-raise the same object: deleting the clause entirely left 114/114 green. The reordering is what is load-bearing. The row that claimed to grade the catch had survived a review round by looking like the fix for a real finding, which is a false green in the exact costume CLAUDE.md names.

Stated and open, by decision

The reconcile route costs one wasted human answer, and now three wasted provider calls, and a provider that is down reports precondition_unavailable rather than attempt_ceiling. All three numbers were measured before they were written down, and three tests pin them. The ceiling also bounds attempts, not executor invocations: an executor that keeps suspending gets unlimited invocations within one attempt, and only the gateway bounds elicitation rounds. A refused attempt number is spent, so raising the ceiling from 2 to 4 buys one more dispatch, not two. Each is in §5.5, §5.7 and the CHANGELOG.

Evidence

  • Gate: 3418 passed with Postgres, 3278 passed / 134 skipped without.
  • Mutation table: 29 rows, all red, no survivors and no "patch did not apply". T240 to T245b now run on three backends, Postgres included.
  • T247 can now detect the serialisation it was written to catch: it asserts overlapping execution windows, and is red 3 runs in 3 against the reviewer's own child.wait() mutant. Its property assertion alone was satisfied by six processes running strictly one after another.
  • §7.1 is a 14-row per-entry-point ceiling column, with every "no" written down. CLAUDE.md's entry-point rule exists because Control.delegate was a missing enumeration rather than a missing check, and the two findings above are exactly what a missing enumeration hid.
  • Two independent review rounds, the first blocking on both counts, the second clean.

SPEC-v0.1 §5.4's `FAILED` row permits a renewal and bounds nothing, so an
executor that raises `NotExecuted` on every call is an unlimited number of
provider dispatches, each one individually correct. SPEC-v0.7 §5 bounds it
where the operator asks, and this carries the amendment into SPEC-v0.1 §5.4
itself, beneath the unchanged table.

`max_attempts`, an action-entry policy key, an integer of at least 1, counting
the attempts that may execute on one effect key with the first included. It
needs `schema: ctrlrun.policy/v5`, 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. Absent means no ceiling, which is
0.6.1's behaviour exactly, and there is no default.

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 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. A read 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, so it gets its own test and the check gets
its own deterministic window.

Verify gains G15, graded through the reconcile route where only the check can
refuse. G5 now selects only an action whose ceiling permits a renewal and is
N/A where the ceiling is the only reason it cannot, because G5'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, no CLI change.
Both blocking findings were sentences that were not true, and the fix for each
is words rather than code.

§5.5 claimed the fast path saves a human from being asked, with one stated
exception, and named the wrong one. On the kernel's own primary route, the one
T245 and G15 are built on, a record that is AMBIGUOUS goes through the fast path
correctly and reaches the approval gate BEFORE any reconcile, so a new approval
request is created, a human grants it, and the retry consumes it in the
reservation the check then refuses. §5.5 stops claiming exhaustiveness and lists
the routes it knows as an open list; §5.2 says a new request can be created and
granted on the way to a refusal; a test pins it. Not closed: re-reading the
record between the reconcile and the second take would save the approval and
would leave the check with no seamless public route, so G15 would grade a
guarantee that could not have failed.

G15's above-the-bound N/A reason was false of a document with a low ceiling on
an action verify cannot drive, which is the identical defect §8.9 had already
caught and fixed in the sentence beside it. Reworded to the scope the fallback
selection actually has.

And: the fast path's refusal records the presented approval (v0.6 §7.2.1, as the
DENY path already did); _refuse_ceiling writes the event and the receipt before
attempting the release and catches any store refusal, since InvalidArgument was
escaping with the evidence; T240 to T245b run on Postgres too; T247 asserts that
two children's windows overlap, because every assertion it had was satisfied by
six processes running one after another; §5.5 says the refused attempt number is
spent; §5.7 says the ceiling bounds attempts and not executor invocations;
§7.1 enumerates the ceiling per entry point with the "no" rows written down;
Control.evaluate's docstring says it does not see the ceiling; and G15's title
fits the report table's width, with a test that keeps every title inside it.
…nd G14

main has moved on twice since this branch left it: item 3's provider
idempotency token and item 5's precondition fingerprints, with G14 and G16.

Four merge points, and the two that matter are the ones a textual merge gets
wrong quietly.

The catalogue tuple: items 3, 4 and 5 each appended after G13 on their own
branch, so a merge yields G13/G15/G14/G16 as readily as a conflict, and BY_ID's
insertion order IS the report's order. Reordered by hand to G13, G14, G15, G16,
and a test now asserts the catalogue is in id order, because nothing else would
have noticed: every count still adds up and every id is still present.

ci.yml's AUTHORITY_NA and TEMPLATES_NA are measured from a run of the merged
catalogue rather than taken from either side: examples/authority/payments.yaml
is 13/13 with 2 not applicable (G13, G15), examples/policies/payments.yaml is
7/7 with 8 (G3, G4, G5, G8, G9, G13, G14, G15). Every N/A count in the verify
tests is measured the same way.

And G14 is wired to the mechanism item 4 built for G5, unchanged: SPEC-v0.7
§8.9 amends both, because each one's control is a renewal and a correct kernel
refuses a renewal under max_attempts: 1. One filter and one sentence, not two.
…t were wrong

Nothing blocking, and three of the seven are this specification being wrong
about its own code.

The try/except round one wrapped the release in is an EQUIVALENT MUTANT: the
reviewer deleted it whole and got 114 of 114 green, because it caught only to
re-raise the same object and nothing observes __suppress_context__. Deleted. A
store refusal propagates by not being caught, which is what §5.5's prose said
all along. The mutation table loses the row that claimed to grade it: a red row
for an equivalent mutant is a false green, and that one survived a review round
by looking like the fix for a real finding. What is load-bearing is that the
evidence is written FIRST, which T249 grades and M26 kills.

§5.5's numbered list put the release before the event and the receipt; the code
does the reverse, and the release may not happen at all. Renumbered to the
code's order, step 4 qualified "where the release succeeds", and §5.2 now says
a failed release lands exactly where a crash does: RESERVED under a live lease,
AMBIGUOUS when it lapses, a human resolving an effect that did not run.

And the merge put item 5's precondition provider in front of the ceiling with
no section saying so. Measured: on the reconcile route under max_attempts: 1 a
doomed attempt calls the operator's provider three times before the check
refuses, one on the request pass and two on the retry, because _recheck runs
once per _take and that route takes twice. A provider that raises there makes
the refusal precondition_unavailable rather than attempt_ceiling, writes no
effect record and never runs the reconcile hook, so the operator is told the
wrong reason for an attempt that could never run. The sequential route calls it
zero times. All three numbers are in §5.5 and pinned by three tests.

Four smaller: T248 counts its reconcile hook instead of inferring that the
approval gate ran first; _projection normalises CLOCK_SKEW_DETECTED's volatile
fields instead of dropping the event, so the count still counts; the catalogue
ordering test keeps its place for locality and BY_ID's order, and its docstring
no longer claims to be the only guard, which 2013940's commit message also
claimed and which is untrue: tests/test_verify.py has asserted the same
ordering since before this branch; and the changelog's max_attempts bullet
wraps.
@coderabbitai

coderabbitai Bot commented Sep 11, 2026

Copy link
Copy Markdown

Warning

Review limit reached

Next included review available in 25 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Advanced

Run ID: 6df746fa-189c-4ee4-8c42-5dbd6337435c

📥 Commits

Reviewing files that changed from the base of the PR and between 4b0c72c and 58f3ac1.

📒 Files selected for processing (13)
  • .github/workflows/ci.yml
  • CHANGELOG.md
  • docs/SPEC-v0.1.md
  • docs/SPEC-v0.7.md
  • src/ctrlrun/control.py
  • src/ctrlrun/policy.py
  • src/ctrlrun/receipt.py
  • src/ctrlrun/verify/guarantees.py
  • src/ctrlrun/verify/scenarios.py
  • tests/test_attempt_cap.py
  • tests/test_verify.py
  • tests/test_verify_action.py
  • tests/test_verify_report.py

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@arpanghoshal
arpanghoshal merged commit 2b390ae into main Sep 11, 2026
11 checks passed
@arpanghoshal
arpanghoshal deleted the v0.7/4-attempt-ceiling branch September 11, 2026 20:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant