Documentation

Subtract one ExBudget from another. Does not guarantee that the result is positive.

A class for injecting a Builtin into an exBudgetCat. We need it, because the constant application machinery calls spendBudget before reducing a constant application and we want to be general over exBudgetCat there, but still track the built-in functions category, hence the ad hoc polymorphism.

This is used elsewhere to convert cost models into JSON objects where the names of the fields are exactly the same as the names of the builtins.

When we want to just evaluate the program that is intended to run out of budget we use the Restricting mode with this big budget designed to make the CEK machine terminate in a fraction of a second on the reference machine.

When we want to just evaluate the program we use the Restricting mode with an enormous budget, so that evaluation costs of on-chain budgeting are reflected accurately in benchmarks.