Bounding Queries Made by a Computation

This file defines a predicate IsQueryBound oa budget canQuery cost parameterized by:

• B — the budget type
• budget : B — the initial budget
• canQuery : ι → B → Prop — whether a query to oracle t is allowed under budget b
• cost : ι → B → B — how the budget is updated after a query to oracle t

The definition is structural via OracleComp.construct: pure satisfies any bound, and query t >>= mx satisfies the bound when canQuery t b holds and each continuation satisfies the bound with the updated budget cost t b.

The classical per-index bound (qb : ι → ℕ, decrement the queried index) is recovered by IsPerIndexQueryBound.

def OracleComp.IsQueryBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} (oa : OracleComp spec α) (budget : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : Prop

Generalized query bound parameterized by a budget type, a validity check, and a cost function. pure satisfies any bound; query t >>= mx satisfies the bound when canQuery t b and every continuation satisfies the bound at cost t b.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OracleComp.isQueryBound_pure {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} (x : α) (b : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : (pure x).IsQueryBound b canQuery cost

theorem OracleComp.isQueryBound_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} (t : ι) (mx : spec t → OracleComp spec α) (b : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : (liftM (query t) >>= mx).IsQueryBound b canQuery cost ↔ canQuery t b ∧ ∀ (u : spec t), (mx u).IsQueryBound (cost t b) canQuery cost

@[simp]

theorem OracleComp.isQueryBound_query_iff {ι : Type u} {spec : OracleSpec ι} {B : Type u_1} (t : ι) (b : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : (liftM (query t)).IsQueryBound b canQuery cost ↔ canQuery t b

@[simp]

theorem OracleComp.isQueryBound_map_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {B : Type u_1} (oa : OracleComp spec α) (f : α → β) (b : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : (f <$> oa).IsQueryBound b canQuery cost ↔ oa.IsQueryBound b canQuery cost

theorem OracleComp.isQueryBound_congr {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} {oa : OracleComp spec α} {b : B} {canQuery₁ canQuery₂ : ι → B → Prop} {cost₁ cost₂ : ι → B → B} (hcan : ∀ (t : ι) (b : B), canQuery₁ t b ↔ canQuery₂ t b) (hcost : ∀ (t : ι) (b : B), cost₁ t b = cost₂ t b) : oa.IsQueryBound b canQuery₁ cost₁ ↔ oa.IsQueryBound b canQuery₂ cost₂

@[reducible, inline]

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

Per-index query bound: qb t gives the maximum number of queries to oracle t. Each query to t decrements qb t by one. Recovers the classical notion.

Equations

• oa.IsPerIndexQueryBound qb = oa.IsQueryBound qb (fun (t : ι) (qb : ι → ℕ) => 0 < qb t) fun (t : ι) (qb : ι → ℕ) => Function.update qb t (qb t - 1)

@[simp]

theorem OracleComp.isPerIndexQueryBound_pure {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] (x : α) (qb : ι → ℕ) : (pure x).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] (t : ι) (mx : spec t → OracleComp spec α) (qb : ι → ℕ) : (liftM (query t) >>= mx).IsPerIndexQueryBound qb ↔ 0 < qb t ∧ ∀ (u : spec t), (mx u).IsPerIndexQueryBound (Function.update qb t (qb t - 1))

@[simp]

theorem OracleComp.isPerIndexQueryBound_query_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (t : ι) (qb : ι → ℕ) : (liftM (query t)).IsPerIndexQueryBound qb ↔ 0 < qb t

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

theorem OracleComp.isPerIndexQueryBound_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] {oa : OracleComp spec α} {ob : α → OracleComp spec β} {qb₁ qb₂ : ι → ℕ} (h1 : oa.IsPerIndexQueryBound qb₁) (h2 : ∀ (x : α), (ob x).IsPerIndexQueryBound qb₂) : (oa >>= ob).IsPerIndexQueryBound (qb₁ + qb₂)

@[simp]

theorem OracleComp.isPerIndexQueryBound_map_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] (oa : OracleComp spec α) (f : α → β) (qb : ι → ℕ) : (f <$> oa).IsPerIndexQueryBound qb ↔ oa.IsPerIndexQueryBound qb

Soundness: structural bound implies dynamic count bound

theorem OracleComp.IsPerIndexQueryBound.counting_bounded {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) {z : α × OracleSpec.QueryCount ι} (hz : z ∈ support (countingOracle.simulate oa 0)) : z.2 ≤ qb

The structural query bound IsPerIndexQueryBound is sound with respect to the dynamic query count produced by countingOracle: if a computation satisfies a per-index query bound, then every execution path's query count is bounded.

Proof strategy: induction on OracleComp, matching the structural IsQueryBound decomposition with the mem_support_simulate_queryBind_iff characterization of counting oracle support.

Worst-case query bounds as a function of input size

def OracleComp.QueryUpperBound {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] (f : α → OracleComp spec β) (size : α → ℕ) (bound : ℕ → ι → ℕ) : Prop

Worst-case per-index query bound as a function of input size: for all inputs x with size x ≤ n, the computation f x makes at most bound n i queries to oracle i.

Equations

• OracleComp.QueryUpperBound f size bound = ∀ (n : ℕ) (x : α), size x ≤ n → (f x).IsPerIndexQueryBound (bound n)

def OracleComp.TotalQueryUpperBound {ι : Type u} {spec : OracleSpec ι} {α β : Type u} (f : α → OracleComp spec β) (size : α → ℕ) (bound : ℕ → ℕ) : Prop

Total query upper bound: there exists a constant k such that for all inputs x with size x ≤ n, the computation f x makes at most k * bound n total queries. Uses the structural IsQueryBound to avoid dependence on oracle responses.

Equations

• OracleComp.TotalQueryUpperBound f size bound = ∃ (k : ℕ), ∀ (n : ℕ) (x : α), size x ≤ n → (f x).IsQueryBound (k * bound n) (fun (x : ι) (b : ℕ) => 0 < b) fun (x : ι) (b : ℕ) => b - 1

def OracleComp.PolyQueryUpperBound {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] (f : α → OracleComp spec β) (size : α → ℕ) : Prop

PolyQueryUpperBound says the per-index query count is polynomially bounded in the input size. This is a non-parameterized version of PolyQueries.

Equations

• OracleComp.PolyQueryUpperBound f size = ∃ (qb : ι → Polynomial ℕ), OracleComp.QueryUpperBound f size fun (n : ℕ) (i : ι) => Polynomial.eval n (qb i)

theorem OracleComp.QueryUpperBound.apply {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] {f : α → OracleComp spec β} {size : α → ℕ} {bound : ℕ → ι → ℕ} (h : QueryUpperBound f size bound) (x : α) : (f x).IsPerIndexQueryBound (bound (size x))

If f has a QueryUpperBound, then each f x satisfies IsPerIndexQueryBound.

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

If oa is a 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).IsPerIndexQueryBound fun (i : ι) => Polynomial.eval n (self.qb i)

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