Monitoring for budget pressure, prover abuse

[jtoman]

Uses the monitoring feature of Certora/graphcore#24 to add two monitors:

1. A prover monitor, which keeps the state of prover tool calls, and tracks whether the agent is "banging its head" against a set of rules. If so, it uses the new "reminder" channel to emit a "nag", urging the agent to either give up or try something new
2. A budget monitor, which accumulates the total cost of all LLM calls within a given "cost center". If we detect that the task is reaching a budget limit (defined as 80% of the allocated budget) we emit a "wrap it up" message. For verification tasks, we also halt any active feedback agents, and disable all feedback gating (with the idea that it's better to finish under budget with lower quality than blow the budget and return nothing).

Budget cancellation is co-operative, if the agent is overbudget/under budget pressure, it throws a special exception which is interpreted as the appropriate "I give up" type (only for the verification tasks).

As mentioned, there is a per cost center budget and a total "overall run" budget. The sum of cost center budgets does not necessarily have to be the overall budget, in fact, it is expected to be greater. This was chosen over a strict allocation of the total budget to different centers, with some arcane budget rebalancing for unused costs.

As part of this, and as predicted by @shellygr, we have moved the pricing information out of the display subsystem into the llm/ module. We also more accurately track 1hr vs 5m cache costs, as this matters when computing budget pressure.

[jar-ben]

Left some comments. The high-level approaches here look good; I think both the budget constraints and the check for "looping over the same prover input" can be helpful (and I think it would solve the real issue we have seen).

[jar-ben]

Why only timeouts? verified rules, violated rules, sanity failures, .., are also not transient

[jtoman]

that's a great point actually.

[jar-ben]

last_item["spec_digest"] == spec_hash is it possible in the current (or intended future) workflow that the .spec remains the same, but the .conf or .sol files changed? In such situations, a rerun makes sense.

[jtoman]

yeah, this assumes the only thing the agent can change is the spec. That's true currently, but will change. we'll have to digest the conf and/or VFS once those changes land.

[ericeil]

I like the use of context vars for this; it feels like a good fix for "ambient" data that would be a pain to pass around explicitly everywhere. I left some naive comments, but overall the mechanism looks good to me.

[jtoman]

example from a smoketest run