Query Cost Accounting

This file defines the HasQuery-level accounting surface for direct-style query programs. A direct-style program is evaluated against a concrete QueryImpl, and query-cost statements are phrased by running that implementation through the writer-cost instrumentation from WriterCost.lean.

@[reducible, inline]

abbrev HasQuery.Program {ι : Type} (spec : OracleSpec ι) (m : Type → Type u_2) (α : Type) : Type u_2

A direct-style computation parameterized by an oracle-query capability.

def HasQuery.Program.eval {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} (oa : Program spec m α) (impl : QueryImpl spec m) : m α

Evaluate a direct-style query program against a concrete implementation.

def HasQuery.Program.withAddCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Program spec (AddWriterT ω m) α) (impl : QueryImpl spec m) (costFn : spec.Domain → ω) : AddWriterT ω m α

Evaluate a direct-style query program against an additive-cost instrumentation of impl.

def HasQuery.Program.withUnitCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : Program spec (AddWriterT ℕ m) α) (impl : QueryImpl spec m) : AddWriterT ℕ m α

Evaluate a direct-style query program against the unit-cost instrumentation of impl.

theorem HasQuery.hasCost_withAddCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] {ω : Type} [AddMonoid ω] (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (t : spec.Domain) : (Program.withAddCost (fun [HasQuery spec (AddWriterT ω m)] => query t) runtime costFn).HasCost (costFn t)

theorem HasQuery.queryBoundedAboveBy_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryImpl spec m) (t : spec.Domain) : (Program.withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryBoundedAboveBy 1

theorem HasQuery.queryBoundedBelowBy_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryImpl spec m) (t : spec.Domain) : (Program.withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryBoundedBelowBy 1

theorem HasQuery.queryCostExactly_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryImpl spec m) (t : spec.Domain) : (Program.withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryCostExactly 1

@[reducible, inline]

abbrev HasQuery.Computation {ι : Type} (spec : OracleSpec ι) (m : Type → Type u_2) (α : Type) : Type u_2

A computation generic over a HasQuery spec m capability.

def HasQuery.UsesCostAs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (f : α → ω) : Prop

Running oa in the additive-cost instrumentation of runtime yields an output-dependent cost described by f.

def HasQuery.UsesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs constant cost w.

def HasQuery.UsesCostAtMost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalSet m] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs cost at most w on every execution path. This is a semantic support bound, not merely an output-indexed cost description.

def HasQuery.UsesCostAtLeast {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalSet m] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs cost at least w on every execution path.

theorem HasQuery.usesCostAtMost_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {w b : ω} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hwb : w ≤ b) : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn b

theorem HasQuery.usesCostAtLeast_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {w b : ω} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hbw : b ≤ w) : UsesCostAtLeast (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn b

theorem HasQuery.usesCostAtMost_query_of_le {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (t : spec.Domain) {b : ω} (ht : costFn t ≤ b) : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => query t) runtime costFn b

def HasQuery.UsesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1.

def HasQuery.UsesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSet m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1, with an upper bound.

def HasQuery.UsesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSet m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1, with a lower bound.

theorem HasQuery.usesAtMostQueries_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n b : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hnb : n ≤ b) : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime b

theorem HasQuery.usesAtLeastQueries_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n b : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hbn : b ≤ n) : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime b

noncomputable def HasQuery.expectedQueryCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) (val : ω → ENNReal) : ENNReal

The expected weighted query cost of oa, instantiated in runtime and instrumented by costFn.

This is the primary expectation notion for generic HasQuery computations. It is computed from the additive cost marginal in the base monad's subdistribution semantics, valued by val.

The unit-cost query-counting notion [HasQuery.expectedQueries] is a specialization of this definition with costFn := fun _ ↦ 1 and val := fun n ↦ (n : ENNReal).

def HasQuery.queryCostDist {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryImpl spec m) (costFn : spec.Domain → ω) : m ω

The marginal distribution of weighted query costs induced by running oa in runtime with query-cost function costFn.

@[reducible, inline]

abbrev HasQuery.queryCountDist {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) : m ℕ

The marginal distribution of the unit-cost query count induced by running oa in runtime.

@[reducible, inline]

noncomputable abbrev HasQuery.expectedQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) : ENNReal

Expected number of oracle queries made by oa when run in runtime, counting each query with unit additive cost.

theorem HasQuery.expectedQueries_eq_tsum_tail_probs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ∑' (i : ℕ), probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c

Tail-sum formula for the expected number of oracle queries made by oa in runtime:

E[number of queries] = ∑ i, Pr[i < number of queries].

This is the generic HasQuery version of [AddWriterT.expectedCostNat_eq_tsum_tail_probs].

theorem HasQuery.expectedQueries_le_tsum_of_tail_probs_le {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryImpl spec m) {a : ℕ → ENNReal} (h : ∀ (i : ℕ), (probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c) ≤ a i) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime ≤ ∑' (i : ℕ), a i

Tail domination bounds expected query count.

If Pr[i < number of queries] ≤ a i for every i, then ExpectedQueries[ oa in runtime ] ≤ ∑ i, a i.

theorem HasQuery.expectedQueries_eq_sum_tail_probs_of_usesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n : ℕ} (h : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ∑ i ∈ Finset.range n, probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c

Finite tail-sum formula for expected query count under a pathwise upper bound.

If oa uses at most n oracle queries in every execution, then its expected query count is the finite sum of the probabilities that the query count exceeds i, for i < n.

theorem HasQuery.expectedQueryCost_le_of_usesCostAtMost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val ≤ val w

theorem HasQuery.expectedQueryCost_eq_tsum_outputs_of_usesCostAs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {f : α → ω} {val : ω → ENNReal} (h : UsesCostAs (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn f) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val = ∑' (a : α), Pr[= a | (Program.withAddCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn).outputs] * val (f a)

theorem HasQuery.expectedQueries_le_of_usesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n : ℕ} (h : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime ≤ ↑n

theorem HasQuery.expectedQueryCost_ge_of_usesCostAtLeast {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostAtLeast (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : val w ≤ expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val

theorem HasQuery.expectedQueryCost_eq_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryImpl spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val = val w

theorem HasQuery.expectedQueries_ge_of_usesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n : ℕ} (h : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : ↑n ≤ expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime

theorem HasQuery.expectedQueries_eq_of_usesAtMostQueries_of_usesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n : ℕ} (hUpper : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hLower : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ↑n

theorem HasQuery.expectedQueries_eq_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryImpl spec m} {n : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ↑n

def HasQuery.«termQueries[_In_]=_» : Lean.ParserDescr

Queries[ oa in runtime ] = n means that the generic HasQuery computation oa makes exactly n oracle queries when instantiated in runtime and instrumented with unit additive cost per query.

The computation oa is written in direct HasQuery style. The notation elaborates it against the unit-cost analysis monad induced by runtime, so statements can usually be written without explicit monad annotations such as m := AddWriterT ℕ m.

def HasQuery.«termQueries[_In_]≤_» : Lean.ParserDescr

Queries[ oa in runtime ] ≤ n means that every execution path of oa makes at most n oracle queries when run in the unit-cost instrumentation of runtime.

This packages the common cryptographic statement “the construction uses at most n queries” on top of [HasQuery.UsesAtMostQueries].

def HasQuery.«termQueries[_In_]≥_» : Lean.ParserDescr

Queries[ oa in runtime ] ≥ n means that every execution of oa in the unit-cost instrumentation of runtime incurs at least n query-cost units.

This is less common than the exact and upper-bound forms, but it is useful for statements saying that a construction must query the oracle at least a certain number of times.

def HasQuery.«termQueryCost[_In_]=_» : Lean.ParserDescr

QueryCost[ oa in runtime ] = n is the unit-cost specialization of weighted query cost: each oracle query contributes additive cost 1, so the total query cost is just the number of queries made by oa.

def HasQuery.«termQueryCost[_In_By_]=_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] = w means that oa, instantiated in runtime and instrumented so that each query t contributes cost costFn t, has constant total query cost w.

Use this when the cost model is not unit cost, for example when different query families or different query shapes carry different weights.

def HasQuery.«termQueryCost[_In_]≤_» : Lean.ParserDescr

QueryCost[ oa in runtime ] ≤ n is the unit-cost specialization of pathwise query-cost upper bounds. It says that every execution of oa makes at most n oracle queries.

def HasQuery.«termQueryCost[_In_By_]≤_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] ≤ w means that every execution path of oa has total query cost bounded above by w under the weighting function costFn.

This is the weighted analogue of [Queries[ oa in runtime ] ≤ n].

def HasQuery.«termQueryCost[_In_]≥_» : Lean.ParserDescr

QueryCost[ oa in runtime ] ≥ n is the unit-cost specialization of pathwise query-cost lower bounds. It says that every execution of oa makes at least n oracle queries.

def HasQuery.«termQueryCost[_In_By_]≥_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] ≥ w means that every execution path of oa has total query cost bounded below by w under the weighting function costFn.

This is the weighted analogue of [Queries[ oa in runtime ] ≥ n].

def HasQuery.«termExpectedQueryCost[_In_]» : Lean.ParserDescr

ExpectedQueryCost[ oa in runtime ] is the expected number of oracle queries made by oa when run in runtime, viewed as the unit-cost specialization of weighted expected query cost.

def HasQuery.«termExpectedQueryCost[_In_By_Via_]» : Lean.ParserDescr

ExpectedQueryCost[ oa in runtime by costFn via val ] is the expected weighted query cost of oa when instantiated in runtime.

Each query t contributes additive cost costFn t, and the total cost is then valued by val : ω → ENNReal before taking expectation. This is the primary expected-cost term for generic HasQuery constructions.

def HasQuery.«termExpectedQueries[_In_]» : Lean.ParserDescr

ExpectedQueries[ oa in runtime ] is the expected number of oracle queries made by oa when run in runtime, with each query carrying unit additive cost.

The result is an ℝ≥0∞ expectation, so it can be compared directly against natural-number bounds such as ExpectedQueries[ oa in runtime ] ≤ n.

This is the unit-cost specialization of [ExpectedQueryCost[ oa in runtime by costFn via val ]], with costFn := fun _ ↦ 1 and val := fun n ↦ (n : ENNReal).