The ledger, and the one amendment to a frozen protocol

CHANGELOG.md

@@ -29,6 +29,20 @@ any change to one appears here.
   The task reaches the authority decision and the receipt, and **never the action hash**: a field
   on `Action` would move every hash in existence and invalidate every stored approval.
 
+- **The budget ledger, and one amendment to a frozen protocol** (SPEC-v0.9 §3). `StateStore` has
+  been frozen since v0.6 and gains exactly two things: `charges=` on `reserve_effect` and
+  `consume_approval_and_reserve`, and `consumptions()` to read the ledger back. Migration
+  `0007_budget_ledger`, additive and forward-only.
+
+  **The charge lands inside the transaction that writes the reservation**, on all three backends.
+  Anything else is a check-then-act race: two processes read the same remaining amount and both
+  spend. On Postgres that needs a `SELECT ... FOR UPDATE` on a per-grant anchor row before the sum,
+  because READ COMMITTED does not serialise a sum and an insert. Measured, not chosen: without it,
+  twenty-four processes racing a budget that permits ten spent **2400 against a limit of 1000**,
+  with zero refusals.
+
+  Nothing spends this yet. The consumption, the holds and the releases are the next item.
+
 - **Consequence budgets, in the document** (SPEC-v0.9 §2). A grant may carry `budgets:`, each a
   `metric`, a `limit` and a `window`. They load, validate, render into the policy hash, and
   attenuate down a delegation chain. **Nothing counts yet**: the ledger and the spending are

docs/SPEC-v0.9.md

@@ -693,7 +693,10 @@ governance control gets turned off.
 ### 3.5.1 The migration is named here, as v0.6's and v0.7's were
 
 `migrations.py` currently ends at `0006_verified_approver`. v0.9 adds **`0007_budget_ledger`**: the
-table of §3.2, the unique constraint of §3.4, and the index of §3.5.
+table of §3.2, the unique constraint of §3.4, the index of §3.5, and **on Postgres only, the
+`budget_anchor` table §3.6.1's lock takes** (one row per grant id ever charged, created on demand).
+The anchor is named here because §3.5's growth discussion otherwise misses it: it accumulates a
+permanent row per grant, runtime delegations included, and the kernel deletes none of them.
 
 It is named in the specification rather than left to the item because `v0.6 §3.7` and `v0.7 §6.11`
 both named theirs, with their DDL and their collation, and a migration discovered in a diff is a
@@ -1605,13 +1608,18 @@ One justification per row. Anything not here is a spec amendment before it is co
 | `Grant.budgets` | `constraints` decides one action and cannot count. A `Budget`'s window is a **whole number of seconds**, bounded, because it is stored and hashed as integer seconds: a sub-second window would round to `0` on the way into a delegation row and read back unreadable, dead for ever |
 | `Grant.tasks` | no dimension names a unit of work |
 | `DIMENSIONS` grows from six entries to eight | **an exported public name whose value changes** (`authority.py:126`, `__all__` at `authority.py:1787`). `verify/scenarios.py` iterates it for G9 and prints `len(DIMENSIONS)`, so this is not a private constant. §9.6 has the test |
-| `Charge` | the store needs a value object for what a reservation spends, carrying the whole predicate (§3.3.1) |
+| `Charge` | the store needs a value object for what a reservation spends, carrying the whole predicate (§3.3.1). It refuses a negative or non-integer `amount` or `limit` the way `Budget` does: a negative amount **refunds** the budget, which is the compensation §12 forbids, reachable by anyone calling the store directly |
 | `charges=` on `reserve_effect` and `consume_approval_and_reserve` | §3.3, half of the milestone's amendment to a frozen protocol |
+
+**All four new names live in `ctrlrun.state`**, beside `StateStore` itself, and are imported from
+there rather than from the package root: they are the vocabulary of the store protocol, and a
+third-party backend already imports `StateStore` from that module.
 | `scope=` on `@protect` and `Control.execute` | `preconditions=` answers a different question (§5.2), and §5.2.1 amends `v0.7 §6.9` to add it |
 | `task=` on `@protect` and `Control.execute` | nothing carries a unit of work today, and it cannot go on `Action` without moving every action hash in existence (§6.3.1) |
 | `task=` on `Authority.evaluate` | **amends a signature frozen in `SPEC-v0.3.md` §11**, and §10.3 records the amendment rather than slipping it in. `Authority.evaluate(action, *, now, store)` is frozen there; the task has to reach the decision, and `v0.7 §6.2`'s context variables are request-time stamps in `approval.py`, not inputs to an authority decision |
 | `task=` on `Control.evaluate` | **also amends a frozen signature** (`SPEC-v0.3.md` §11: "its signature and `Evaluation`'s two fields are unchanged"). Required by §6.3.2: without it `Control.evaluate` and `Control.execute` disagree about a task-bound grant, and `ctrlrun.adapter.needs_approval` routes through `evaluate` |
-| `consumptions()` on `StateStore` | §3.3.3: the surfaces and G22 need a read, and `charges=` is write-only |
+| `consumptions()` on `StateStore` | §3.3.3: the surfaces and G22 need a read, and `charges=` is write-only. Rows come back **in insertion order**, which is deterministic and identical across the three backends and is *not* a time ordering: host clock skew, which `v0.7 §3` models, inverts `consumed_at` against the id |
+| `check_charges` | §3.3.1's predicate in one place, so three backends cannot drift on the arithmetic. Public for the same reason `plan_reservation` is: a third-party store decides with it rather than reimplementing it |
 | `Consumption` | what `consumptions()` returns: `grant_id`, `metric`, `amount`, `effect_key`, `attempt`, `consumed_at`, `released_at`. Frozen here because §3.3.3 returns it and §7.2 renders it, and a return type specified nowhere is a spec amendment waiting to happen |
 
 ### 10.1 Schemas

src/ctrlrun/conformance/store/fixtures.py

@@ -30,7 +30,7 @@
 from ...effect import DEFAULT_LEASE, EffectRecord, EffectState, Reservation
 from ...errors import NotExecuted
 from ...receipt import Event
-from ...state import ClockSkew, DelegationRecord, StateStore
+from ...state import Charge, ClockSkew, DelegationRecord, StateStore
 from .backends import SQLiteBackend, StoreBackend
 
 
@@ -87,7 +87,11 @@ class _TwoWinners(_Wrapped):
     """Drops the uniqueness check: every contender reserves."""
 
     def reserve_effect(
-        self, effect_key: str, action_id: str, lease: timedelta = DEFAULT_LEASE
+        self,
+        effect_key: str,
+        action_id: str,
+        lease: timedelta = DEFAULT_LEASE,
+        charges: tuple[Charge, ...] = (),
     ) -> Reservation:
         now = datetime.now(tz=None).astimezone()
         return Reservation(
@@ -100,7 +104,11 @@ class _ReleasesAnExpiredLease(_Wrapped):
     `AMBIGUOUS` and refusing (`v0.1 §5.3 E3`)."""
 
     def reserve_effect(
-        self, effect_key: str, action_id: str, lease: timedelta = DEFAULT_LEASE
+        self,
+        effect_key: str,
+        action_id: str,
+        lease: timedelta = DEFAULT_LEASE,
+        charges: tuple[Charge, ...] = (),
     ) -> Reservation:
         record = self._inner.get_effect(effect_key)
         if record is not None and record.lease_expires_at is not None:
@@ -126,7 +134,11 @@ class _RefusesWithTheWrongError(_Wrapped):
     """
 
     def reserve_effect(
-        self, effect_key: str, action_id: str, lease: timedelta = DEFAULT_LEASE
+        self,
+        effect_key: str,
+        action_id: str,
+        lease: timedelta = DEFAULT_LEASE,
+        charges: tuple[Charge, ...] = (),
     ) -> Reservation:
         try:
             return self._inner.reserve_effect(effect_key, action_id, lease)
@@ -158,9 +170,10 @@ def consume_approval_and_reserve(
         effect_key: str,
         action_id: str,
         lease: timedelta = DEFAULT_LEASE,
+        charges: tuple[Charge, ...] = (),
     ) -> Any:
         approval = self._inner.consume_approval(approval_id, action_hash)
-        reservation = self._inner.reserve_effect(effect_key, action_id, lease)
+        reservation = self._inner.reserve_effect(effect_key, action_id, lease, charges)
         return approval, reservation
 
 
@@ -274,7 +287,11 @@ def __init__(self, inner: StateStore) -> None:
         self._resolvers = {}
 
     def reserve_effect(
-        self, effect_key: str, action_id: str, lease: timedelta = DEFAULT_LEASE
+        self,
+        effect_key: str,
+        action_id: str,
+        lease: timedelta = DEFAULT_LEASE,
+        charges: tuple[Charge, ...] = (),
     ) -> Reservation:
         before = self._inner.get_effect(effect_key)
         reservation = self._inner.reserve_effect(effect_key, action_id, lease)

src/ctrlrun/migrations.py

@@ -332,6 +332,65 @@ def sql(self, dialect: str) -> tuple[str, ...]:
     "ALTER TABLE approvals ADD COLUMN IF NOT EXISTS approvals_required INTEGER",
 )
 
+#: SPEC-v0.9 §3.2, §3.5.1: the budget ledger. One row per consumption, per ancestor charged.
+#:
+#: **The unique constraint is `v0.6 §4.3.2` Table A1 row 2's doing, not tidiness.** A lost
+#: `COMMIT` with no record found retries the insert *once*, and the retried transaction re-inserts
+#: the reservation and its charges together. An unconstrained append would double-charge there,
+#: precisely when an operator's network is already misbehaving.
+#:
+#: **`released_at` is nullable and release is a compare-and-set on it, never a decrement**
+#: (§4.4). Table A2 row 2 re-issues a lost `UPDATE` once, and a decrement is not idempotent under
+#: a re-issue: the second one subtracts again and the operator's budget quietly grows.
+#:
+#: The index is what makes §2.5's rolling sum a range scan. Named here because a ledger without
+#: it is correct and unusable, and "correct and unusable" is how a governance control gets
+#: turned off (§3.5).
+_BUDGET_LEDGER: Final = (
+    """
+    CREATE TABLE budget_ledger (
+        id INTEGER PRIMARY KEY AUTOINCREMENT,
+        grant_id TEXT NOT NULL,
+        metric TEXT NOT NULL,
+        amount INTEGER NOT NULL,
+        effect_key TEXT NOT NULL,
+        attempt INTEGER NOT NULL,
+        consumed_at TEXT NOT NULL,
+        released_at TEXT,
+        UNIQUE (effect_key, attempt, grant_id, metric)
+    )
+    """,
+    "CREATE INDEX ix_budget_ledger_window ON budget_ledger (grant_id, metric, consumed_at)",
+)
+_BUDGET_LEDGER_PG: Final = (
+    """
+    CREATE TABLE IF NOT EXISTS budget_ledger (
+        id BIGSERIAL PRIMARY KEY,
+        grant_id TEXT NOT NULL COLLATE "C",
+        metric TEXT NOT NULL COLLATE "C",
+        amount BIGINT NOT NULL,
+        effect_key TEXT NOT NULL COLLATE "C",
+        attempt INTEGER NOT NULL,
+        consumed_at TIMESTAMPTZ NOT NULL,
+        released_at TIMESTAMPTZ,
+        UNIQUE (effect_key, attempt, grant_id, metric)
+    )
+    """,
+    """
+    CREATE INDEX IF NOT EXISTS ix_budget_ledger_window
+        ON budget_ledger (grant_id, metric, consumed_at)
+    """,
+    # SPEC-v0.9 §3.6, measured rather than chosen: READ COMMITTED does not serialise a sum and an
+    # insert, and the spike overspent 1200 against a limit of 1000 in three runs of four. The
+    # anchor row is what `SELECT ... FOR UPDATE` takes before the sum. **Per grant and not per
+    # store**, so two budgets on two grants do not serialise against each other.
+    """
+    CREATE TABLE IF NOT EXISTS budget_anchor (
+        grant_id TEXT PRIMARY KEY COLLATE "C"
+    )
+    """,
+)
+
 #: The ordered set this binary knows. `NNNN_snake_name`: four digits, zero-padded, so
 #: lexicographic order is application order.
 MIGRATIONS: Final[tuple[Migration, ...]] = (
@@ -349,6 +408,7 @@ def sql(self, dialect: str) -> tuple[str, ...]:
         _VERIFIED_APPROVER,
         postgres=_VERIFIED_APPROVER_PG,
     ),
+    Migration("0007_budget_ledger", _BUDGET_LEDGER, postgres=_BUDGET_LEDGER_PG),
 )
 
 HEAD: Final = MIGRATIONS[-1].id