A ceiling the operator sets, decided on the attempt the store assigned - #145
Merged
Conversation
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.
|
Warning Review limit reachedNext included review available in 25 minutes. View limit detailsLimit 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. Review configuration: ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Advanced Run ID: 📒 Files selected for processing (13)
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. Comment |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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_reservationdidattempt=record.attempt + 1with no ceiling, so an executor that raisesNotExecutedon 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 thenN/Awith a reason true of the operator's document.reserve_effectandconsume_approval_and_reserveare frozen and cannot carry a ceiling, soControlcompares the returnedreservation.attemptbefore the executor is called. Two callers who both readN-1cannot both get through. A read before reserving is a fast path that saves the write, never the guarantee, and it refuses only aFAILEDrecord.blockedreceipt), the record is releasedFAILED, andActionDenied(reason="attempt_ceiling")is raised. No new error type, event type,StateStoremethod,Controlmethod, 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.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/Areason claimed "every declaredmax_attemptsis 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 CTRLRunErrorturned 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 costumeCLAUDE.mdnames.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_unavailablerather thanattempt_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
child.wait()mutant. Its property assertion alone was satisfied by six processes running strictly one after another.CLAUDE.md's entry-point rule exists becauseControl.delegatewas a missing enumeration rather than a missing check, and the two findings above are exactly what a missing enumeration hid.