From 4cf6e6d081573dd1a7fee0d12fdd91961d7e610f Mon Sep 17 00:00:00 2001 From: rohanrkamath Date: Mon, 14 Sep 2026 22:09:49 -0400 Subject: [PATCH] verify: size each vector for the scenario's own spends, try every rule, negate a boolean with a boolean Found by running ctrlrun verify on the payments pack's document: a grant with twelve refunds an hour and a first approve rule on counterparty_new_eq: true graded one guarantee and reported twenty-three not applicable. Three things, each in its own test: - select fitted every candidate to the grant's budgets with PROCESSES * 2 + 2 of room, G4's nine landings doubled, for every guarantee. The room is now the scenario's own: DEFAULT_SPENDS, four, unless the scenario says otherwise; G4 says PROCESSES + 2. - the synthesizer stopped at the first rule of a decision. A budget on amount cannot measure the vector a counterparty_new_eq rule yields, and the next rule was the amount band the budget was written for. select now tries every candidate of a decision, rule by rule, before it concludes nothing binds. - a boolean condition was negated with a string that is neither answer. T413f, T413g and T413k hard-coded eighteen; they now name the number each scenario is sized for. T413h's two-band document is graded honestly under the lower band's own rule, which fits the budget as written, rather than reported not applicable. Signed-off-by: rohanrkamath --- CHANGELOG.md | 20 ++++++ src/ctrlrun/verify/scenarios.py | 115 ++++++++++++++++++++++---------- tests/test_verify_authority.py | 81 ++++++++++++++++++---- 3 files changed, 169 insertions(+), 47 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 36db8ef2..87552537 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,26 @@ any change to one appears here. ## [Unreleased] +### Fixed + +- **`ctrlrun verify` sized every vector for eighteen spends, and a grant with an ordinary + count budget graded nothing.** `select` fitted each candidate to the grant's budgets with + `PROCESSES * 2 + 2` of room, G4's nine landings doubled, for every guarantee. A document whose + grant said twelve refunds an hour, which is what a payments pack writes for a support agent, + reported twenty-three guarantees not applicable, "every action reaching this decision exceeds + a budget on the grant that covers it", about a budget that admitted the action twelve times. + The room is now the scenario's own: `DEFAULT_SPENDS`, four, unless the scenario says + otherwise, and G4 says `PROCESSES + 2`. +- **The synthesizer stopped at the first rule of a decision.** A grant's budget can refuse the + first rule's vector for a reason the second rule's does not share: a document whose first + `approve` rule is `counterparty_new_eq: true` yields a vector with no `amount`, which a budget + on `amount` cannot measure, while the next `approve` rule is the amount band the budget was + written for. `select` now tries every candidate of a decision, rule by rule, before it + concludes nothing binds. +- **A boolean condition was negated with a string.** `X_neq` on `counterparty_new_eq: true` + produced `"ctrlrun-verify"`, neither answer; the vector landed in the next rule by accident of + `eq` and carried a value no document could mean. A boolean is negated with the other boolean. + ## [0.11.0] — Evidence One question: **can the record be trusted after the fact, and kept?** diff --git a/src/ctrlrun/verify/scenarios.py b/src/ctrlrun/verify/scenarios.py index 9a62db11..42e4a794 100644 --- a/src/ctrlrun/verify/scenarios.py +++ b/src/ctrlrun/verify/scenarios.py @@ -143,6 +143,10 @@ #: and named so no reader of the evidence mistakes it for one. APPROVER: Final = "ctrlrun-verify" +#: How many spends of its vector a scenario is sized for unless it says otherwise: a control, +#: the guarded attempt, and a retry or two (SPEC-v0.9 §2). +DEFAULT_SPENDS: Final = 4 + #: SPEC-v0.8 §11.7: the approver identity G18 grades against. Verify builds its own scenarios, #: so it supplies the provider too; what it grades is the kernel's refusal, never whether the #: operator configured one, which is a fact about a constructor call and not about a document. @@ -401,7 +405,13 @@ def _is_int(value: object) -> bool: def _negate_value(operand: object) -> Any: """§3.3's `X_neq` row: a value that is not the operand, in the operand's own shape.""" - if isinstance(operand, int) and not isinstance(operand, bool): + if isinstance(operand, bool): + # Before this, a boolean fell through to the string below, so a rule on + # `counterparty_new_eq: true` was negated with a string that is neither answer. The + # vector still landed in the next rule, by accident of `eq`, and carried a value no + # document could mean. + return not operand + if isinstance(operand, int): return operand + 1 if isinstance(operand, str): return f"{operand}-x" @@ -712,25 +722,44 @@ def authority(self) -> Authority | None: def _synthesize( self, name: str, decision: Decision, mutation: Mapping[str, Any] | None = None ) -> tuple[dict[str, Any], str] | None: - """An argument vector driving `name` to `decision`, and the rule reason it reached. + """The first argument vector driving `name` to `decision`, and the rule reason it + reached; `_synthesized` yields them all.""" + return next(self._synthesized(name, decision, mutation), None) + + def _synthesized( + self, name: str, decision: Decision, mutation: Mapping[str, Any] | None = None + ) -> Iterator[tuple[dict[str, Any], str]]: + """Every argument vector driving `name` to `decision`, rule by rule, with the rule + reason each reached. **The vector is checked before it is used** (§3.3). Having built one, the engine evaluates the action it just constructed and asserts the decision is the one it was aiming for; a vector that lands in a different rule is an internal error, not a FAIL, because it would run, refuse something, and report a guarantee that was never exercised. + + **All of them, not the first.** `select` binds a vector to a grant, and a grant's + budget can refuse the first rule's vector for a reason the second rule's does not + share: a document whose first `approve` rule is `counterparty_new_eq: true` yields a + vector with no `amount`, which a budget on `amount` cannot measure, while its second + `approve` rule is the amount band the budget was written for. Stopping at the first + reported the whole guarantee not applicable, "a budget names a metric the action does + not carry", about a document whose next rule carried it. """ entry: _ActionPolicy | None = self.policy.actions.get(name) if entry is None: - return None + return extras = _placeholders(self.policy, name) if entry.decision is not None: if entry.decision is not decision: - return None + return vector = dict(extras) if mutation: vector.update(mutation) - return self._checked(name, vector, decision, "decision") + checked = self._checked(name, vector, decision, "decision") + if checked is not None: + yield checked + return for index, rule in enumerate(entry.rules): if rule.decision is not decision: continue @@ -740,8 +769,7 @@ def _synthesize( vector.update(mutation) checked = self._checked(name, vector, decision, f"rule[{index}]") if checked is not None: - return checked - return None + yield checked def _checked( self, name: str, vector: dict[str, Any], decision: Decision, expected_reason: str @@ -793,9 +821,17 @@ def select( #: a property of the action rather than of a grant, so `grant_filter` cannot express it. action_filter: Callable[[str], bool] | None = None, mutation: Mapping[str, Any] | None = None, + spends: int = DEFAULT_SPENDS, ) -> _Selection | None: """§3.2 — the first action, sorted by codepoint, that satisfies the requirements. + `spends` is how many times the scenario will spend the vector against the grant's + budgets, and the vector is sized so that many fit (`_fitted_to_budgets`). It is the + scenario's own number: G4 lands `PROCESSES + 1` and says so; everything else lands a + handful. One size for all of them was `PROCESSES * 2 + 2`, and a grant whose count + budget admitted twelve actions an hour, which is an ordinary number for a document to + carry, reported every guarantee not applicable because eighteen did not fit. + Where an `authority:` section exists the principal comes from a grant that actually covers the action (§3.4), because an action nothing authorizes is refused by the authority axis before the policy axis is ever reached (`v0.3 §4.3`), and a scenario @@ -844,24 +880,23 @@ def select( if ceiling_bound is not None and ceiling is not None and ceiling > ceiling_bound: continue for decision in decisions: - synthesized = self._synthesize(name, decision, mutation) - if synthesized is None: - continue - arguments, reason = synthesized - self._declined_on_budget = False - selection = self._bind(name, arguments, decision, reason, grant_filter) - if selection is not None: - return selection - # An action DID reach this decision and no grant covered it. Recorded so the - # caller's N/A reason can say so: a bare `None` here is indistinguishable from - # "no action reaches this decision", and every scenario used to resolve that - # ambiguity by asserting its own hardcoded sentence about the policy. - # - # **Unless a grant did cover it and its budget is what declined.** Recording a - # resource miss there put a sentence in the report that is false of the document: - # the pattern matched perfectly and the budget was the whole reason. - if not self._declined_on_budget: - self._grant_miss = self._resource(name, arguments) + for arguments, reason in self._synthesized(name, decision, mutation): + self._declined_on_budget = False + selection = self._bind(name, arguments, decision, reason, grant_filter, spends) + if selection is not None: + return selection + # An action DID reach this decision and no grant covered it. Recorded so + # the caller's N/A reason can say so: a bare `None` here is + # indistinguishable from "no action reaches this decision", and every + # scenario used to resolve that ambiguity by asserting its own hardcoded + # sentence about the policy. + # + # **Unless a grant did cover it and its budget is what declined.** + # Recording a resource miss there put a sentence in the report that is + # false of the document: the pattern matched perfectly and the budget was + # the whole reason. + if not self._declined_on_budget: + self._grant_miss = self._resource(name, arguments) return None def _bind( @@ -871,6 +906,7 @@ def _bind( decision: Decision, reason: str, grant_filter: Callable[[Grant], bool] | None, + spends: int = DEFAULT_SPENDS, ) -> _Selection | None: resource = self._resource(name, arguments) if self.authority is None: @@ -913,7 +949,9 @@ def _bind( # smaller than the vector `_synthesize` picked refuses that action, and the refusal # reached G1 as an internal error. Verify owns the vector, so verify sizes it. self._unmeasurable = False - fitted = self._fitted_to_budgets(name, arguments, decision, reason, grant, action) + fitted = self._fitted_to_budgets( + name, arguments, decision, reason, grant, action, room=spends + ) if fitted is None: # Recorded, for `unselected`'s reason. A bare `continue` here reported the # *grant* miss below, so a policy whose approve band starts above its grant's @@ -975,10 +1013,11 @@ def _deciding_grant(self, action: Action) -> Grant | None: return grant return None - #: How many spends of the chosen vector a scenario may take. G4's control leg runs - #: `PROCESSES` children on distinct keys and then contends `PROCESSES` more on one key, so - #: nine of them land; the margin above that is for every other scenario that acts twice. - _BUDGET_HEADROOM: Final = reg.PROCESSES * 2 + 2 + #: How many spends of the chosen vector G4 takes: its control leg runs `PROCESSES` + #: children on distinct keys and then contends `PROCESSES` more on one key, so + #: `PROCESSES + 1` land, and one more is margin. Every other scenario passes nothing and + #: gets `DEFAULT_SPENDS`, which is what a scenario that acts a handful of times needs. + G4_SPENDS: Final = reg.PROCESSES + 2 def _fits_budgets(self, grant: Grant, action: Action, *, room: int = 1) -> bool | None: """Whether every budget on this grant admits `room` spends of this action. @@ -1022,7 +1061,12 @@ def _budget_verdict(self, grants: tuple[Grant, ...], action: Action, room: int) return True def _shrunk( - self, arguments: dict[str, Any], grants: tuple[Grant, ...], action: Action, divisor: int + self, + arguments: dict[str, Any], + grants: tuple[Grant, ...], + action: Action, + divisor: int, + room: int, ) -> dict[str, Any] | None: """One vector with **every** over-limit metric brought under its own budget. @@ -1039,7 +1083,7 @@ def _shrunk( value = _metric_value(action, budget.metric, grant.id) except InvalidArgument: return None - if value * self._BUDGET_HEADROOM > budget.limit: + if value * room > budget.limit: tried[budget.metric] = max(1, budget.limit // divisor) return tried if tried != arguments else None @@ -1051,6 +1095,8 @@ def _fitted_to_budgets( reason: str, grant: Grant, action: Action, + *, + room: int = DEFAULT_SPENDS, ) -> tuple[dict[str, Any], Action] | None: """Size verify's own action vector to the budgets that will decide it. @@ -1069,7 +1115,6 @@ def _fitted_to_budgets( """ deciding = self._deciding_grant(action) bound = (grant,) if deciding is None else (grant, deciding) - room = self._BUDGET_HEADROOM verdict = self._budget_verdict(bound, action, room) if verdict is True: return arguments, action @@ -1080,7 +1125,7 @@ def _fitted_to_budgets( self._unmeasurable = True return None for divisor in (room, 8, 4, 2, 1): - tried = self._shrunk(arguments, bound, action, divisor) + tried = self._shrunk(arguments, bound, action, divisor, room) if tried is None: continue rebuilt = replace(action, arguments=tried) @@ -1735,7 +1780,7 @@ def body(detail: dict[str, Any]) -> None: # --- G4: concurrent attempts produce exactly one winner ------------------------------ def g4(self) -> GuaranteeResult: - selection = self.select(needs_effect=True) + selection = self.select(needs_effect=True, spends=self.G4_SPENDS) if selection is None: return self.na( "G4", diff --git a/tests/test_verify_authority.py b/tests/test_verify_authority.py index 3dfd77ab..eee1ebff 100644 --- a/tests/test_verify_authority.py +++ b/tests/test_verify_authority.py @@ -18,7 +18,7 @@ from ctrlrun.authority import DIMENSIONS from ctrlrun.verify import Status, VerifyRefused, run from ctrlrun.verify import guarantees as reg -from ctrlrun.verify.scenarios import EXPIRY_NOT_DECISIVE +from ctrlrun.verify.scenarios import DEFAULT_SPENDS, EXPIRY_NOT_DECISIVE, _negate_value pytestmark = pytest.mark.authority @@ -611,7 +611,7 @@ def test_T413f_a_resized_vector_leaves_room_for_a_scenario_that_acts_more_than_o if result.status is Status.PASS: graded = dict(result.arguments or {}) # Nine spends have to fit inside 900, so a vector of 900, or of 450, would not do. - assert graded["amount"] * 18 <= 900, graded + assert graded["amount"] * (reg.PROCESSES + 1) <= 900, graded FLOORED_RULE = """ @@ -655,26 +655,29 @@ def test_T413g_a_band_whose_floor_leaves_no_headroom_is_N_A_and_never_FAIL(tmp_p assert result.status is not Status.FAIL, result.reason if result.status is Status.PASS: - assert dict(result.arguments or {})["amount"] * 18 <= 900, result.arguments + assert dict(result.arguments or {})["amount"] * (reg.PROCESSES + 1) <= 900, result.arguments def test_T413h_a_resize_never_silently_grades_a_different_rule(tmp_path): """`select`'s contract is the decision **and the rule** it was asked for. - Two bands reach `allow` here. `_synthesize` picks the upper one, and every value small - enough for the budget lands in the lower one, which is a different rule with a different - reason. Checking only the decision would let verify grade a rule nobody selected and report - it under the first band's name. + Two bands reach `allow` here. The upper one is tried first, and every value small enough + for the budget lands in the lower one, which is a different rule with a different reason. + Checking only the decision would let verify resize the upper band's vector below its own + floor and grade it under the upper band's name. - So the honest answer is that no vector fits, and the guarantee is `N/A`. + So a resize that leaves the rule is declined, and the honest answer is the next candidate: + the lower band's own vector, selected under the lower band's name, which fits the budget + as it stands. Where no candidate fits at all the guarantee is `N/A`. """ path = _write(tmp_path, V7 + TIGHT_BUDGET + TWO_ALLOW_BANDS) result = _by_id(run(path, only=("G3",)))["G3"] if result.status is Status.PASS: - assert dict(result.arguments or {})["amount"] >= 1000, ( - f"verify graded a band it was not asked for: {result.arguments}" + graded = dict(result.arguments or {})["amount"] + assert graded <= 999 and graded * DEFAULT_SPENDS <= 900, ( + f"verify graded a vector no rule of the document admits at that size: {graded}" ) else: assert result.status is Status.NOT_APPLICABLE, result.reason @@ -775,8 +778,8 @@ def test_T413k_the_two_metric_vector_is_under_both_budgets(tmp_path): result = _by_id(run(path, only=("G3",)))["G3"] graded = dict(result.arguments or {}) - assert graded["amount"] * 18 <= 100000, graded - assert graded["tip"] * 18 <= 100000, graded + assert graded["amount"] * DEFAULT_SPENDS <= 100000, graded + assert graded["tip"] * DEFAULT_SPENDS <= 100000, graded TASKED_SHADOW = """ @@ -1066,3 +1069,57 @@ def test_T413t_a_v09_guarantee_grades_the_same_alone_as_in_a_full_run(gid, tmp_p f"{gid} alone: {alone.status} ({alone.reason}); in a full run: {together.status} " f"({together.reason})" ) + + +# --- the room a vector is sized for is the scenario's own --------------------------------- + +TWELVE_AN_HOUR = """ +authority: + grants: + - id: support-agent + subject: { agent: "support-agent" } + actions: ["acme.refund"] + resources: ["payment:*"] + environments: ["production"] + budgets: + - {metric: amount, limit: 500000, window: PT24H} + - {metric: count, limit: 12, window: PT1H} +actions: + acme.refund: + effect: "refund:{payment_id}" + resource: "payment:{payment_id}" + rules: + - when: { counterparty_new_eq: true } + decision: approve + - when: { amount_gte: 0, amount_lte: 50000 } + decision: allow + - when: { amount_gte: 0, amount_lte: 500000 } + decision: approve + - decision: deny +""" + + +def test_a_count_budget_of_twelve_an_hour_grades_the_guarantees_that_spend_a_handful(tmp_path): + """The payments pack's own grant: twelve refunds an hour, and every guarantee read N/A. + + One size for every scenario was `PROCESSES * 2 + 2`, eighteen, which no count budget an + operator writes for an agent admits. G1 spends a handful and is sized for that; G4 spends + `PROCESSES + 1` and says so, and is sized for that. + """ + path = _write(tmp_path, V7 + TWELVE_AN_HOUR) + + results = _by_id(run(path, only=("G1", "G3", "G4", "G22"))) + + for gid in ("G1", "G3", "G4", "G22"): + assert results[gid].status is Status.PASS, (gid, results[gid].reason) + assert dict(results["G4"].arguments or {})["amount"] * (reg.PROCESSES + 1) <= 500000 + + +def test_a_boolean_condition_is_negated_with_the_other_boolean(): + """`counterparty_new_eq: true` used to be negated with a string that is neither answer; + the vector landed in the next rule by accident of `eq` and carried a value no document + could mean.""" + assert _negate_value(True) is False + assert _negate_value(False) is True + assert _negate_value(7) == 8 + assert _negate_value("x") == "x-x"