Budget counters not checked at the operation-authorization boundary (§9.6)

[nficano]

Category: spec-conformance Severity: major
Location: src/Arcp.Runtime/Leases/LeaseManager.cs:129-141
Spec: ARCP v1.1 §9.6

What

Spec §9.6 requires the runtime to check all budget counters before authorizing any operation through the lease and to fail with BUDGET_EXHAUSTED if any counter is ≤ 0. AuthorizeOperation — the SDK's single lease-enforcement entry point — checks expiry and pattern only; it never consults the job's BudgetLedger. BudgetLedger.AssertNotExhausted (BudgetLedger.cs:55) exists but is referenced only by unit tests, never on the enforcement path. Budget is therefore enforced reactively (a tool_result error on the cost metric that crosses zero) rather than as a pre-operation gate, so an agent can keep performing lease operations after exhaustion.

Evidence

public void AuthorizeOperation(Lease lease, LeaseConstraints? constraints, string namespaceName, string pattern)
{
    if (constraints?.ExpiresAt is { } exp && _time.GetUtcNow() >= exp)
        throw new LeaseExpiredException($"Lease expired at {exp:O}");

    if (!lease.Capabilities.TryGetValue(namespaceName, out var allowed) || allowed.Count == 0)
        throw new PermissionDeniedException($"No lease for namespace '{namespaceName}'");
    foreach (var pat in allowed)
    {
        if (GlobMatch(pattern, pat)) return;
    }
    throw new PermissionDeniedException($"'{pattern}' is not authorized by lease for '{namespaceName}'");
}

Proposed fix

Thread the job's BudgetLedger into the operation-authorization path and call AssertNotExhausted() (or equivalent) before the pattern check, raising BUDGET_EXHAUSTED when any counter is ≤ 0.

Acceptance criteria

• Once any budget counter reaches ≤ 0, the next lease-authorized operation fails with BUDGET_EXHAUSTED via the enforcement path (not only via a reactive cost-metric tool_result).