Expand description
The workspace’s shared resource policy. One resource policy for every public surface.
Several subsystems already impose useful local bounds: the parser’s walk depth, CST extraction depth, expression evaluation steps, morphism search budget, model-check assignment counts. Each is sound on its own, and together they were not a policy: what an input was allowed to cost depended on which door it came through, so the same document could be refused through the CLI and accepted through the C ABI.
Two properties make this a policy rather than another local bound.
A Budget is shared, not per-call. A nested operation draws
from the same allowance as the operation containing it, so a caller
cannot be charged once for a walk and again for each subwalk, and a
document cannot escape a bound by being processed in pieces.
A failure names which resource ran out and what the bound was. “Too deep” without a number tells a caller nothing about what to pass instead.
Structs§
- Budget
- An allowance being drawn down by one operation and everything nested inside it.
- Limit
Exceeded - A bounded resource ran out.
- Resource
Limits - What a single operation is allowed to consume.
Enums§
- Resource
- The resources a bounded operation can exhaust.