Cost Models for Oracle Computations

This file defines a general cost model for oracle computations, parametric over any AddCommMonoid cost type. This supports natural numbers, extended non-negative reals, per-oracle cost vectors, and custom multi-dimensional cost structures.

Uses AddWriterT (defined in ToMathlib.Control.WriterT) for additive cost accumulation.

Main Definitions

• instrumentedRun oa cm: oa interpreted in the canonical free runtime with additive cost tracking.
• addCostOracle costFn: the corresponding one-query instrumented oracle implementation.
• CostModel spec ω: Assigns cost queryCost t : ω to each oracle query t.
• costDist oa cm: Joint distribution of (output, totalCost).
• expectedCost oa cm val: Expected total cost E[val(cost)], computed via wp.
• WorstCaseCostBound, ExpectedCostBound: Cost bound predicates.
• WorstCasePolyTime, ExpectedPolyTime: Asymptotic polynomial-time predicates for computation families indexed by a security parameter.

Key Results

• fst_map_costDist: Cost instrumentation doesn't change the output distribution.
• expectedCost_pure: Expected cost of a pure computation is 0.
• probEvent_cost_gt_le_expectedCost_div: Markov's inequality for cost distributions.
• WorstCasePolyTime.toExpectedPolyTime: Strict polynomial time implies expected polynomial time.

Cost Model, Cost Oracle, Cost Distribution

All definitions below operate at Type (= Type 0), matching wp, support, and Pr[ ...] which are defined for {α : Type} in the program logic.

def addCostOracle {ι : Type} {spec : OracleSpec ι} {ω : Type} [AddCommMonoid ω] (costFn : spec.Domain → ω) : QueryImpl spec (AddWriterT ω (OracleComp spec))

Oracle that tracks additive cost. Wraps costOracle with Multiplicative to get additive accumulation through the existing WriterT infrastructure.

@[simp]

theorem fst_map_run_simulateQ_addCostOracle {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] (costFn : spec.Domain → ω) (oa : OracleComp spec α) : Prod.fst <$> WriterT.run (simulateQ (addCostOracle costFn) oa) = oa

structure CostModel {ι : Type} (spec : OracleSpec ι) (ω : Type) [AddCommMonoid ω] : Type

A cost model assigns a cost in ω to each oracle query. The cost type ω can be ℕ, ℝ≥0∞, ι → ℕ (per-oracle), or any AddCommMonoid.

• queryCost : spec.Domain → ω

def CostModel.zero {ι : Type} {spec : OracleSpec ι} {ω : Type} [AddCommMonoid ω] : CostModel spec ω

The zero cost model: every query is free.

@[reducible, inline]

abbrev instrumentedRun {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] (oa : OracleComp spec α) (cm : CostModel spec ω) : AddWriterT ω (OracleComp spec) α

Run oa in the canonical free OracleComp runtime instrumented by cm's additive query-cost function. This is the semantic core of CostModel.

def costDist {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] (oa : OracleComp spec α) (cm : CostModel spec ω) : OracleComp spec (α × Multiplicative ω)

The joint distribution of (output, totalCost) obtained by running oa with additive cost tracking. Cost accumulates via + through AddWriterT.

Since Multiplicative ω and ω are definitionally equal, the second component of the product can be used directly as ω.

@[simp]

theorem fst_map_costDist {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] (oa : OracleComp spec α) (cm : CostModel spec ω) : Prod.fst <$> costDist oa cm = oa

Cost instrumentation does not change the output distribution.

theorem AddWriterT.expectedCost_eq_wp_run {ι : Type} {spec : OracleSpec ι} {α ω : Type} [spec.Fintype] [spec.Inhabited] [AddMonoid ω] (oa : AddWriterT ω (OracleComp spec) α) (val : ω → ENNReal) : oa.expectedCost val = OracleComp.ProgramLogic.wp (WriterT.run oa) fun (z : α × Multiplicative ω) => val (Multiplicative.toAdd z.2)

For OracleComp, AddWriterT.expectedCost is the weakest-precondition expectation of the run semantics projected to the additive cost component.

Expected Cost

noncomputable def expectedCost {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) : ENNReal

The expected total cost of oa under cost model cm, valued by val : ω → ℝ≥0∞. Computed as E[val(cost)] = ∑ (x, c), Pr[= (x, c) | costDist] * val(c).

The valuation val maps the abstract cost type to ℝ≥0∞ for expectation computation. For ω = ℕ, use (↑·). For ω = ℝ≥0∞, use id. For multi-dimensional cost, choose which dimension to analyze.

@[reducible, inline]

noncomputable abbrev expectedCostNat {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ℕ) : ENNReal

Convenience: expected cost for ℕ-valued cost models.

theorem expectedCost_eq_wp_costDist {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) : expectedCost oa cm val = OracleComp.ProgramLogic.wp (costDist oa cm) fun (z : α × Multiplicative ω) => val z.2

The CostModel.expectedCost facade agrees definitionally with the weakest-precondition expectation of the instrumented costDist.

@[simp]

theorem expectedCost_pure {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (x : α) (cm : CostModel spec ω) (val : ω → ENNReal) (hval : val 0 = 0) : expectedCost (pure x) cm val = 0

theorem expectedCost_le_of_support_bound {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) (c : ENNReal) (h : ∀ z ∈ support (costDist oa cm), val z.2 ≤ c) : expectedCost oa cm val ≤ c

If val z.2 ≤ c for all z in the support of costDist, then expectedCost ≤ c. This is the key bridge from worst-case (support) bounds to expected bounds.

Worst-Case Cost Bounds

def WorstCaseCostBound {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [Preorder ω] (oa : OracleComp spec α) (cm : CostModel spec ω) (bound : ω) : Prop

Every execution path of oa under cm has total cost at most bound.

Currently unused outside this file; retained as scaffolding for future asymptotic analyses.

theorem worstCaseCostBound_iff_support_bound {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [Preorder ω] (oa : OracleComp spec α) (cm : CostModel spec ω) (bound : ω) : WorstCaseCostBound oa cm bound ↔ ∀ z ∈ support (costDist oa cm), z.2 ≤ bound

WorstCaseCostBound is equivalently a support bound over the old costDist view.

Cost Bounds

def ExpectedCostBound {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) (bound : ENNReal) : Prop

The expected cost of oa under cm (valued by val) is at most bound.

Currently unused outside this file; retained as scaffolding for future asymptotic analyses.

theorem WorstCaseCostBound.toExpectedCostBound {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] [Preorder ω] {oa : OracleComp spec α} {cm : CostModel spec ω} {bound : ω} (hstrict : WorstCaseCostBound oa cm bound) {val : ω → ENNReal} (hval_mono : Monotone val) : ExpectedCostBound oa cm val (val bound)

A strict cost bound implies an expected cost bound, provided the valuation val is monotone with respect to ≤ on ω.

theorem probEvent_cost_gt_mul_le_expectedCost {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) (t : ENNReal) : (probEvent (costDist oa cm) fun (z : α × Multiplicative ω) => t < val z.2) * t ≤ expectedCost oa cm val

Markov's inequality for cost distributions (multiplication form). The probability that the valued cost exceeds t, times t, is at most expectedCost.

theorem probEvent_cost_gt_le_expectedCost_div {ι : Type} {spec : OracleSpec ι} {α ω : Type} [AddCommMonoid ω] [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (cm : CostModel spec ω) (val : ω → ENNReal) (t : ENNReal) (ht : 0 < t) (ht' : t ≠ ⊤) : (probEvent (costDist oa cm) fun (z : α × Multiplicative ω) => t < val z.2) ≤ expectedCost oa cm val / t

Markov's inequality for cost distributions (division form).

Standard Cost Models

def CostModel.unit {ι : Type} {spec : OracleSpec ι} : CostModel spec ℕ

Unit cost model: every oracle query costs 1. Total cost under this model equals total query count.

theorem WorstCaseCostBound.toIsPerIndexQueryBound_unit {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [spec.Inhabited] {oa : OracleComp spec α} {bound : ℕ} (h : WorstCaseCostBound oa CostModel.unit bound) : oa.IsPerIndexQueryBound fun (x : ι) => bound

A strict bound under the unit cost model yields a uniform per-index query bound: if every execution uses at most bound total unit-cost steps, then each oracle index is queried at most bound times.

theorem IsPerIndexQueryBound.toWorstCaseCostBound_unit_sum {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [Fintype ι] [spec.Inhabited] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) : WorstCaseCostBound oa CostModel.unit (∑ i : ι, qb i)

If main makes at most qb i queries to each oracle i, then its total query count (under the unit cost model) is at most ∑ i, qb i on every execution path.

theorem IsPerIndexQueryBound.toExpectedCostBound_unit_sum {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [Fintype ι] [spec.Fintype] [spec.Inhabited] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) : ExpectedCostBound oa CostModel.unit (fun (n : ℕ) => ↑n) (∑ i : ι, ↑(qb i))

Corollary: the expected total query count is also at most ∑ i, qb i. Follows from the worst-case bound toWorstCaseCostBound_unit_sum.

@[reducible, inline]

abbrev OracleComp.probCompUnitQueryRun {β : Type} (oa : ProbComp β) : AddWriterT ℕ ProbComp β

Run a ProbComp with unit-cost instrumentation: each call to the uniform-selection oracle is counted as cost 1.