Query budgets #
OracleComp.IsCostBounded cost program n says that on every path through the tree of calls of
program, whatever the answers, the calls cost at most n in total, where a call q costs
cost q. This is the library's notion of a query budget; the others are instances of it.
- With unit costs it is
OracleComp.IsQueryBounded program n: at mostncalls on every path, that is, a query tree of depth at mostn. - A cost that is
1on calls of one kind and0on the others counts those calls only, such as the signing calls of a forger, or the external queries of a program with private coins (ProbOracleComp.IsQueryBounded). - A zero budget for the calls outside a predicate
psays that every call satisfiesp(OracleComp.QueriesSatisfy), for example that every request has bounded length.
Budgets are proved and used by induction on the program. They are preserved by sequencing
(IsCostBounded.bind), add over costs (IsCostBounded.add), and compose with handlers whose calls
are budgeted in turn (IsCostBounded.run_interpret). Against every stateful oracle, the calls that
OracleComp.withTranscript records respect the budget (IsCostBounded.transcript_cost_le).
A budget says nothing about running time.
Main definitions #
Cslib.OracleComp.IsCostBounded: calls costing at mostnon every path.Cslib.OracleComp.IsQueryBounded: at mostncalls on every path.Cslib.OracleComp.QueriesSatisfy: every call on every path satisfies a predicate.
Main results #
Cslib.OracleComp.IsCostBounded.bind: budgets add under sequencing.Cslib.OracleComp.IsCostBounded.add: budgets for two costs give a budget for their sum.Cslib.OracleComp.IsCostBounded.run_interpret: the budget of a program run through a stateful handler.Cslib.OracleComp.IsCostBounded.transcript_cost_le: logged calls respect the budget.
The calls of the program cost at most n in total on every path, whatever the answers, where
a call q costs cost q.
- pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {cost : ι → ℕ} (a : α) (n : ℕ) : IsCostBounded cost (Pure.pure a) n
Returning a value makes no call.
- liftBind {ι : Type u} {spec : OracleSpec ι} {α : Type v} {cost : ι → ℕ} (q : ι) (cont : spec q → OracleComp spec α) (n : ℕ) (hcont : ∀ (a : spec q), IsCostBounded cost (cont a) n) : IsCostBounded cost (OracleComp.query q >>= cont) (n + cost q)
A call followed by continuations whose calls each cost at most
n.
Instances For
The program makes at most n oracle calls on every path, whatever the answers.
Instances For
A larger budget is still a budget.
A budget for a call's continuations, from a budget for the call.
One call costs its cost.
Budgets add under sequencing.
Calls that cost nothing fit in a zero budget.
A budget for a cost is one for every smaller cost.
Budgets for two costs give a budget for their sum.
A program whose calls are replaced by programs over another interface, each call q costing
at most cost q there, costs at most n there when its own calls cost at most n.
A program run through a stateful handler, each of whose calls q costs at most cost q on
the target interface, costs at most n there when its own calls cost at most n.
Postprocessing the result makes no call.
Every call satisfies a predicate #
Every call of program, on every path and whatever the answers, satisfies p: the calls
outside p have a zero budget.
Instances For
A call followed by its continuations satisfies p exactly when the call and every
continuation do.
Returning a value makes no call.
A single call satisfies p when its query does.
Sequencing preserves the predicate.
Every program satisfies a predicate that holds for every call.
A weaker predicate is still satisfied.
Postprocessing the result makes no call.
Logged calls respect the budget #
Against every stateful oracle, the calls recorded on a supported run cost at most the budget.
Against every stateful oracle, a supported run records at most n calls.
Against every stateful oracle, every call recorded on a supported run satisfies p.