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 and total query bounds are recovered by IsPerIndexQueryBound and IsTotalQueryBound.

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.

@[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₂

theorem OracleComp.IsQueryBound.simulateQ_run_of_step {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} {ι' : Type u} {spec' : OracleSpec ι'} {σ : Type u} {B' : Type u_2} {canQuery : ι → B → Prop} {cost : ι → B → B} {canQuery' : ι' → B' → Prop} {cost' : ι' → B' → B'} {combine : B' → B' → B'} {mapBudget : B → B'} {stepBudget : ι → B → B'} {impl : QueryImpl spec (StateT σ (OracleComp spec'))} {oa : OracleComp spec α} {budget : B} (h : oa.IsQueryBound budget canQuery cost) (hbind : ∀ {γ δ : Type u} {oa' : OracleComp spec' γ} {ob : γ → OracleComp spec' δ} {b₁ b₂ : B'}, oa'.IsQueryBound b₁ canQuery' cost' → (∀ (x : γ), (ob x).IsQueryBound b₂ canQuery' cost') → (oa' >>= ob).IsQueryBound (combine b₁ b₂) canQuery' cost') (hstep : ∀ (t : ι) (b : B) (s : σ), canQuery t b → ((impl t).run s).IsQueryBound (stepBudget t b) canQuery' cost') (hcombine : ∀ (t : ι) (b : B), canQuery t b → combine (stepBudget t b) (mapBudget (cost t b)) = mapBudget b) (s : σ) : ((simulateQ impl oa).run s).IsQueryBound (mapBudget budget) canQuery' cost'

Transfer a structural query bound through simulateQ into a stateful target semantics, provided each simulated source query has a target-side step bound and the target-side bind rule composes those step budgets with the recursive continuation budget.

@[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.

@[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.

Total query bounds

def OracleComp.IsTotalQueryBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (n : ℕ) : Prop

A total query bound: the computation makes at most n queries total (across all oracle indices).

theorem OracleComp.isTotalQueryBound_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} {t : spec.Domain} {mx : spec.Range t → OracleComp spec α} {n : ℕ} : (liftM (query t) >>= mx).IsTotalQueryBound n ↔ 0 < n ∧ ∀ (u : spec.Range t), (mx u).IsTotalQueryBound (n - 1)

theorem OracleComp.IsTotalQueryBound.mono {ι : Type u} {spec : OracleSpec ι} {α : Type u} {oa : OracleComp spec α} {n₁ n₂ : ℕ} (h : oa.IsTotalQueryBound n₁) (hle : n₁ ≤ n₂) : oa.IsTotalQueryBound n₂

theorem OracleComp.isTotalQueryBound_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {n₁ n₂ : ℕ} (h1 : oa.IsTotalQueryBound n₁) (h2 : ∀ (x : α), (ob x).IsTotalQueryBound n₂) : (oa >>= ob).IsTotalQueryBound (n₁ + n₂)

theorem OracleComp.not_isTotalQueryBound_bind_query_prefix_zero {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {oa : OracleComp spec α} {next : α → spec.Domain} {ob : (x : α) → spec.Range (next x) → OracleComp spec β} : ¬(oa >>= fun (x : α) => liftM (query (next x)) >>= ob x).IsTotalQueryBound 0

theorem OracleComp.IsTotalQueryBound.of_bind_query_prefix {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [spec.Inhabited] {oa : OracleComp spec α} {next : α → spec.Domain} {ob : (x : α) → spec.Range (next x) → OracleComp spec β} {n : ℕ} (h : (oa >>= fun (x : α) => liftM (query (next x)) >>= ob x).IsTotalQueryBound (n + 1)) : oa.IsTotalQueryBound n

If a computation is followed by a continuation that always starts with one query, then a bound on the whole computation by n + 1 yields a bound on the prefix by n.

theorem OracleComp.IsTotalQueryBound.simulateQ_run_of_step {ι : Type u} {spec : OracleSpec ι} {α σ : Type u} {impl : QueryImpl spec (StateT σ (OracleComp spec))} {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain) (s : σ), ((impl t).run s).IsTotalQueryBound 1) (s : σ) : ((simulateQ impl oa).run s).IsTotalQueryBound n

theorem OracleComp.countingOracle.add_single_mem_support_simulate_queryBind {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] {t : spec.Domain} {oa : spec.Range t → OracleComp spec α} {u : spec.Range t} {z : α × OracleSpec.QueryCount ι} (hz : z ∈ support (countingOracle.simulate (oa u) 0)) : (z.1, OracleSpec.QueryCount.single t + z.2) ∈ support (countingOracle.simulate (liftM (query t) >>= oa) 0)

theorem OracleComp.countingOracle.exists_mem_support_simulate_of_mem_support_run_simulateQ_le_cost {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [Fintype ι] {σ : Type u} {impl : QueryImpl spec (StateT σ (OracleComp spec))} (cost : σ → ℕ) (hstep : ∀ (t : spec.Domain) (st : σ), ∀ x ∈ support ((impl t).run st), cost x.2 ≤ cost st + 1) {oa : OracleComp spec α} {st₀ : σ} {z : α × σ} (hz : z ∈ support ((simulateQ impl oa).run st₀)) : ∃ (qc : OracleSpec.QueryCount ι), (z.1, qc) ∈ support (countingOracle.simulate oa 0) ∧ cost z.2 ≤ cost st₀ + ∑ i : ι, qc i

theorem OracleComp.sum_update_pred {ι : Type u} [DecidableEq ι] [Fintype ι] {qc : ι → ℕ} {t : ι} (ht : 0 < qc t) : ∑ i : ι, Function.update qc t (qc t - 1) i = ∑ i : ι, qc i - 1

theorem OracleComp.IsTotalQueryBound.residual_of_mem_support_counting {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] [Fintype ι] {oa : OracleComp spec α} {ob : α → OracleComp spec β} {n : ℕ} (h : (oa >>= ob).IsTotalQueryBound n) {z : α × OracleSpec.QueryCount ι} (hz : z ∈ support (countingOracle.simulate oa 0)) : (ob z.1).IsTotalQueryBound (n - ∑ i : ι, z.2 i)

If oa >>= ob is totally query-bounded by n, then after any support point of the counting run of oa, the continuation ob is bounded by the residual budget.

theorem OracleComp.IsTotalQueryBound.counting_total_le {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [Fintype ι] {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) {z : α × OracleSpec.QueryCount ι} (hz : z ∈ support (countingOracle.simulate oa 0)) : ∑ i : ι, z.2 i ≤ n

Any support point of the counting simulation of a totally query-bounded computation has total query count at most the structural bound.

theorem OracleComp.IsTotalQueryBound.residual_of_mem_support_run_simulateQ_le_cost {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [spec.Fintype] [spec.Inhabited] [Finite ι] {σ : Type u} {impl : QueryImpl spec (StateT σ (OracleComp spec))} (cost : σ → ℕ) (hstep : ∀ (t : spec.Domain) (st : σ), ∀ x ∈ support ((impl t).run st), cost x.2 ≤ cost st + 1) {oa : OracleComp spec α} {ob : α → OracleComp spec β} {n : ℕ} (h : (oa >>= ob).IsTotalQueryBound n) {st₀ : σ} {z : α × σ} (hz : z ∈ support ((simulateQ impl oa).run st₀)) : (ob z.1).IsTotalQueryBound (n - (cost z.2 - cost st₀))

If a stateful simulation has support cost at most one per query step, then any support point of the simulated prefix leaves the continuation bounded by the residual budget measured by that cost. The cost may under-approximate the true query count, so the resulting residual budget is correspondingly weaker but still sound.

theorem OracleComp.IsTotalQueryBound.of_perIndex {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [Fintype ι] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) : oa.IsTotalQueryBound (∑ i : ι, qb i)

Per-index bound implies total bound (sum over indices).

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.

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

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.

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

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.

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

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.

Currently used only in CostModel.lean; retained as scaffolding for future asymptotic analyses.

• 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.