Bounding Queries Made by a Computation

This file defines a predicate IsQueryBound oa qb to say that a computation with oracles spec never makes a larger number of queries than is given by a bound qb : spec.ι → ℕ. This is useful for showing that some simulated computation is polynomial time, and in things like seeding query values for a computation.

We also define a function minimalQueryBound oa that returns the smallest such count. Calculating this is generally expensive, and so it shouldn't be used in actual algorithms, but it can be useful in some proofs that only care about the existence of a bound.

def OracleComp.IsQueryBound {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (qb : ι → ℕ) : Prop

Predicate expressing that qb is a bound on the number of queries made by oa. In particular any simulation with a countingOracle produces counts that are smaller.

Equations

• oa.IsQueryBound qb = ∀ qc ∈ (Prod.snd <$> (OracleComp.simulateQ countingOracle oa).run).support, qc ≤ qb

theorem OracleComp.isQueryBound_def {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (qb : spec.QueryCount) : oa.IsQueryBound qb ↔ ∀ qc ∈ (Prod.snd <$> (simulateQ countingOracle oa).run).support, qc ≤ qb

theorem OracleComp.isQueryBound_mono {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} {oa : OracleComp spec α} (qb : ι → ℕ) {qb' : ι → ℕ} (h' : oa.IsQueryBound qb) (h : qb ≤ qb') : oa.IsQueryBound qb'

theorem OracleComp.isQueryBound_iff_probEvent {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] {oa : OracleComp spec α} {qb : ι → ℕ} : oa.IsQueryBound qb ↔ [fun (x : ι → ℕ) => x ≤ qb|Prod.snd <$> (simulateQ countingOracle oa).run <|> pure 0] = 1

@[simp]

theorem OracleComp.isQueryBound_pure {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (a : α) (qb : ι → ℕ) : (pure a).IsQueryBound qb

@[simp]

theorem OracleComp.isQueryBound_failure {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (qb : ι → ℕ) : failure.IsQueryBound qb

@[simp]

theorem OracleComp.isQueryBound_query_iff_pos {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} [Nonempty α] (q : spec.OracleQuery α) (qb : ι → ℕ) : (liftM q).IsQueryBound qb ↔ 0 < qb q.index

structure OracleComp.PolyQueries {ι : Type} [DecidableEq ι] {spec : ℕ → OracleSpec ι} {α β : ℕ → Type} (oa : (n : ℕ) → α n → OracleComp (spec n) (β n)) : Type

If oa is an computation indexed by a security parameter, then PolyQueries oa means that for each oracle index there is a polynomial function qb of the security parameter, such that the number of queries to that oracle is bounded by the corresponding polynomial.

• qb : ι → Polynomial ℕ

  qb i is a polynomial bound on the queries made to oracle i.

• qb_isQueryBound (n : ℕ) (x : α n) : (oa n x).IsQueryBound fun (i : ι) => Polynomial.eval n (self.qb i)

  The bound is actually a bound on the number of queries made.