Cost Ceilings Read Off the IR: Emission Cardinality Bounds and SLO Gates

Pitch

How many times an agent activation may call its model or tools is a compile-time fact in a capability-typed language, reported with an explicit "unbounded" verdict instead of an optimistic number, and an SLO contract can then be refused or paused against it.

Abstract

Agent frameworks meter cost after the fact: a runaway loop shows up as an invoice. We show that in a language where every effect crosses a declared capability boundary, an upper bound on crossings per activation can be computed from the IR and published as an audit fact next to the capability table. The analysis counts crossings exactly for non-looping bodies, takes the maximum across branches, certifies a finite ceiling for linear self-recursion with a strictly decreasing literal fuel under a dominating base guard, and reports unbounded for everything else, including every branching recursion and every crossing it cannot see through (a first-class emitting arrow, a host extern). An adversarial review caught a recognizer that accepted f(n-1); f(n-1) as linear while it crosses 2^n - 1 times; the repaired recognizer requires at most one recursive call site per path. A typed-model retry budget enters the count as a constant factor N + 1. Declared budget ceilings are checked against the computed bound, and a dedicated ceiling-attenuation check stops a delegated child from holding a wider budget than its parent. On top sits a composition SLO contract with a compile-time gate (declaration against declaration) and an observed half (measurement over the stored trace and, since slice 5, a live producer inside Session; a signed receipt tied to the generation; a rollout gate on the predecessor's receipt). We report what is implemented, what the docs say it does not show, and the evaluation still to run.

Problem and claim

Runtime cost accounting says what an activation spent. It does not say what it can spend, and it cannot refuse a rollout before the spend. Static resource analyses (RAML, gas analyses) bound cost for functional programs or contracts but are not wired to an audit surface, a delegation algebra, or an SLO contract.

The claim has three layers, each with different evidence strength. (1) A crossing-count fold designed to mirror the existing boundary walk line for line, with an honest unbounded verdict; shipped and tested, with soundness argued in the design doc and not proved. (2) Budgets that ride the existing ceiling parameters, checked statically and attenuated on delegation by a dedicated check; shipped. (3) A predicted-versus-observed SLO gate in which the prediction rests on ranked evidence E1 to E4; E1 and E4 are shipped, E2 (refusing an SLO bound over a route the cardinality verdict calls unbounded) and E3 (canary witness) are designed only.

The docs themselves limit the claim. The SLO design note says no arrangement of evidence "proves that a future SLO will hold" and lists exactly what the gate can refuse. This draft keeps that framing.

Contributions

1. A per-capability crossing-count analysis with a named unbounded verdict, joined to the boundary surface, with exact counts for non-looping bodies, max over branches, and counts of the emit step, the req-target emission call and the spawn-handle provision call (src/revl/cardinality.py:1-25, tests/test_cardinality_260.py).
2. A bounded-iteration certifier for linear self-recursion, and the adversarial finding that the first version certified tree recursion as linear; the repaired clause (at most one in-SCC call site per path) with regression tests (docs/design/260-emission-cardinality-bounds.md:3-37, tests/test_cardinality_260.py:372,397).
3. Budget ceilings checked against the computed bound, and a dedicated attenuation check on delegation, with the finding that the existing coverage fold is ceiling-blind (src/revl/lower.py:17931 for the ceiling-blind comment, :17939 for _ceiling_attenuation_check; tests/test_budget_260.py).
4. A typed-model retry budget that multiplies the bound (src/revl/cardinality.py:49-62, tests/test_validated_retry_257s2.py:203).
5. An SLO contract with a closed datum set, a compile-time gate, a measured observed half, signed receipts tied to a generation, and a rollout gate with an evidence ladder (docs/design/473-slo-contracts.md, src/revl/slo.py:1290).
6. An account of four stale premises found when the planned work item met the tree, as a methods lesson.

Related work

Evidence on main

Numbers that exist

• Test counts at the cited commit, from def test_ lines: 22 (tests/test_cardinality_260.py), 16 (tests/test_budget_260.py), 7, 10, 8 (follow-up cardinality files), 20 (tests/test_473_slo_rollout_gate.py), 44 (tests/test_slo_473.py), 26 (tests/test_slo_473_window.py), 19 (tests/test_slo_473_live_producer.py).
• src/revl/slo.py is 2091 lines; src/revl/cardinality.py is 1187 lines.
• The branching counterexample: f(n-1); f(n-1) crosses 2^n - 1 times (design doc, revision paragraph); no experimental count.
• No precision data exists: no figure for how many real components certify bounded versus unbounded across the examples or the agent-loop fixtures. None yet.
• No overhead, no false-refusal rate, no data on how often the SLO gate refuses.

Paper outline

1. Introduction: invoices as the only cost signal; the static alternative.
2. Setting: capability boundary, emissions, the boundary walk.
3. The count analysis: exact, max over branches, unbounded and bounded-symbolic; the soundness tie to the boundary walk.
4. Bounded iteration: the fuel recognizer, the 2^n counterexample, the repair; the agent-loop extensions.
5. Budgets: ceilings on the existing parameter order, static check, the ceiling-blind coverage bug, dedicated attenuation; the retry multiplier.
6. SLO contracts: closed datum set, E1 gate, observed half, receipts, E4 rollout gate; E2 and E3 as the evidence ladder's open rungs.
7. Evaluation: precision study, differential soundness test, replayed breaches.
8. Related work, limits.

Threats to validity and limits

• The SLO design note says E1 "refuses a rollout against a promise nothing currently checks" because the time ceiling has no runtime meter; it is "exactly 'the document contradicts itself' and no more" (docs/design/473-slo-contracts.md, E1).
• max_pending_tasks backed by a per-activation calls ceiling is a unit mismatch, noted in the doc.
• Three of five SLO datums are never gated against a declaration; recovery_time and approval_wait are not measurable today.
• Multi-function and mutual recursion stay unbounded (doc section 5.2, open); symbolic bounds are proof schemas, not numbers.
• Counts are per activation per component, not realm aggregates; a realm-aggregate budget would be a new ceiling kind.
• The analysis trusts the boundary walk; an opaque host body is counted unbounded only if the extern is surfaced.
• "Refused because predicted to breach" means one of three narrow things; this draft does not claim to predict latency.
• No Lean theorem covers src/revl/cardinality.py. The theorems in formal/RevL/Theorems/CapCeilings.lean (attenuation_monotone at :105, lineage_ceiling_le at :121, budget_never_exceeds_root_ceiling at :171) cover the ceiling and attenuation algebra, not the crossing count, and are not evidence for the bound.
• Some design-doc status statements are stale: docs/design/260-emission-cardinality-bounds.md:39 says "design, not implemented", and docs/design/473-slo-contracts.md has a status table (:29-36) saying the rollout gate E4 and the live producer landed while other text says the E4 gate is "the one that does not exist" (:224) and "There is no producer inside Session" (:521). This draft cites the current code.
• No empirical precision or overhead data exists yet; all current evidence is unit tests.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 55 checked, 6 corrected.

Cite this draft

@misc{revlp08,
  author       = {Thomas Moussajee},
  title        = {Cost Ceilings Read Off the IR: Emission Cardinality Bounds and SLO Gates},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P08.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.