verify: size each vector for the scenario's own spends, try every rule, negate a boolean with a boolean

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.12.0] — Hardening
 
 One question: **is the thing this project says about itself checkable?**

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",

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"