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.

This is the specialization of PFunctor.FreeM.IsRollBound to OracleComp spec α = FreeM spec.toPFunctor α: an oracle index t : ι plays the role of a polynomial-functor position, and a query continuation spec t → OracleComp spec α is the FreeM roll continuation. Most structural lemmas defer to their FreeM analogues.

theorem OracleComp.isQueryBound_iff_isRollBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} (oa : OracleComp spec α) (budget : B) (canQuery : ι → B → Prop) (cost : ι → B → B) : oa.IsQueryBound budget canQuery cost ↔ PFunctor.FreeM.IsRollBound oa budget canQuery cost

The bridge to the FreeM-level predicate is Iff.rfl: IsQueryBound is literally PFunctor.FreeM.IsRollBound on the underlying free monad.

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

@[simp]

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 (OracleSpec.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 (OracleSpec.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_iff_of_map_eq {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} {β : Type u} {oa : OracleComp spec α} {ob : OracleComp spec β} {f : α → β} {b : B} (h : f <$> oa = ob) (canQuery : ι → B → Prop) (cost : ι → B → B) : oa.IsQueryBound b canQuery cost ↔ ob.IsQueryBound b canQuery cost

If f <$> oa = ob for any f, the query-bound predicate transfers between them. The standard shape is oa = (simulateQ wrapped mx).run s and ob = simulateQ inner mx (or (simulateQ inner mx).run s'), where wrapped threads bookkeeping (a state, a writer log) that the underlying simulation does not see. The projection equality is supplied by the corresponding QueryImpl.fst_map_run_* lemma (with f = Prod.fst) or by an auxiliary projection identity such as withCachingAux_run_proj_eq (with f = Prod.map id Prod.fst).

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.proj {ι : Type u} {spec : OracleSpec ι} {α : Type u} {B : Type u_1} {B' : Type u_2} (proj : B → B') {oa : OracleComp spec α} {b : B} {canQuery : ι → B → Prop} {cost : ι → B → B} {canQuery' : ι → B' → Prop} {cost' : ι → B' → B'} (h_can : ∀ (t : ι) (b' : B), canQuery t b' → canQuery' t (proj b')) (h_cost : ∀ (t : ι) (b' : B), canQuery t b' → proj (cost t b') = cost' t (proj b')) (h : oa.IsQueryBound b canQuery cost) : oa.IsQueryBound (proj b) canQuery' cost'

Project an IsQueryBound along a budget projection proj : B → B'.

If the source bound at budget b validates queries at every step, the projected bound at proj b is also validated, provided:

• h_can — whenever a step is allowed in the source (canQuery t b'), it is allowed in the projection (canQuery' t (proj b'));
• h_cost — the projection commutes with the cost step on the allowed branch (proj (cost t b') = cost' t (proj b')).

Typical use: extract a single-coordinate query bound (e.g. qS-only) from a multi-coordinate bound (e.g. (qS, qH) from signHashQueryBound) by setting proj := Prod.fst.

theorem OracleComp.isQueryBound_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {B : Type u_1} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {canQuery : ι → B → Prop} {cost : ι → B → B} (combine : B → B → B) {b₁ b₂ : B} (h_can : ∀ (t : ι) (b₁' b₂' b : B), canQuery t b → canQuery t (combine b₁' b) ∧ canQuery t (combine b b₂')) (h_cost : ∀ (t : ι) (b₁' b₂' b : B), canQuery t b → combine b₁' (cost t b) = cost t (combine b₁' b) ∧ cost t (combine b b₂') = combine (cost t b) b₂') (h₁ : oa.IsQueryBound b₁ canQuery cost) (h₂ : ∀ (x : α), (ob x).IsQueryBound b₂ canQuery cost) : (oa >>= ob).IsQueryBound (combine b₁ b₂) canQuery cost

Generic bind composition for IsQueryBound parameterised by an arbitrary budget type B and a binary combine operation on it. The natural-number versions (isTotalQueryBound_bind, isQueryBoundP_bind, isPerIndexQueryBound_bind) are special cases at combine := (· + ·); the vector-budget cmaSignHashQueryBound_bind uses this directly with component-wise +.

The two side conditions are universally quantified so they survive recursion under generalizing b₁:

• h_can — extending any validated budget on either side via combine keeps the query valid;
• h_cost — cost distributes left and right over combine on validated budgets.

theorem OracleComp.isQueryBound_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {B : Type u_1} {og : OracleComp spec (α → β)} {oa : OracleComp spec α} {canQuery : ι → B → Prop} {cost : ι → B → B} (combine : B → B → B) {b₁ b₂ : B} (h_can : ∀ (t : ι) (b₁' b₂' b : B), canQuery t b → canQuery t (combine b₁' b) ∧ canQuery t (combine b b₂')) (h_cost : ∀ (t : ι) (b₁' b₂' b : B), canQuery t b → combine b₁' (cost t b) = cost t (combine b₁' b) ∧ cost t (combine b b₂') = combine (cost t b) b₂') (h₁ : og.IsQueryBound b₁ canQuery cost) (h₂ : oa.IsQueryBound b₂ canQuery cost) : (og <*> oa).IsQueryBound (combine b₁ b₂) canQuery cost

Forward-direction seq analogue of isQueryBound_bind. Reduces to the bind case via seq_eq_bind_map plus isQueryBound_map_iff to discharge the constant continuation.

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.

def OracleComp.IsQueryBoundP {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (p : ι → Prop) [DecidablePred p] (n : ℕ) : Prop

Predicate-targeted query bound: a middle ground between IsQueryBound and IsPerIndexQueryBound / IsTotalQueryBound. IsQueryBoundP oa p n says that oa makes at most n queries to oracle indices satisfying p, with no constraint on the number of queries to indices where p fails.

This is built on the generic IsQueryBound with the validity check ¬ p t ∨ 0 < qb and the cost function that decrements the budget only on p-indices.

theorem OracleComp.isQueryBoundP_def {ι : Type u} {spec : OracleSpec ι} {α : Type u} (p : ι → Prop) [DecidablePred p] (oa : OracleComp spec α) (n : ℕ) : oa.IsQueryBoundP p n ↔ oa.IsQueryBound n (fun (t : ι) (qb : ℕ) => ¬p t ∨ 0 < qb) fun (t : ι) (qb : ℕ) => if p t then qb - 1 else qb

theorem OracleComp.isQueryBoundP_iff_isRollBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} (p : ι → Prop) [DecidablePred p] (oa : OracleComp spec α) (n : ℕ) : oa.IsQueryBoundP p n ↔ PFunctor.FreeM.IsRollBound oa n (fun (t : spec.toPFunctor.A) (qb : ℕ) => ¬p t ∨ 0 < qb) fun (t : spec.toPFunctor.A) (qb : ℕ) => if p t then qb - 1 else qb

IsQueryBoundP is IsRollBound on the underlying FreeM with the predicate-targeted validity and cost.

theorem OracleComp.isQueryBoundP_iff_isQueryBound_if {ι : Type u} {spec : OracleSpec ι} {α : Type u} (p : ι → Prop) [DecidablePred p] (oa : OracleComp spec α) (n : ℕ) : oa.IsQueryBoundP p n ↔ oa.IsQueryBound n (fun (t : ι) (b : ℕ) => if p t then 0 < b else True) fun (t : ι) (b : ℕ) => if p t then b - 1 else b

IsQueryBoundP rephrased with the if … then 0 < b else True validity check. This is the shape that arises naturally in expectedSCost hypotheses, where the gap between the two implementations is paid only on p-queries.

@[simp]

theorem OracleComp.isQueryBoundP_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} (p : ι → Prop) [DecidablePred p] (t : ι) (mx : spec t → OracleComp spec α) (n : ℕ) : (liftM (OracleSpec.query t) >>= mx).IsQueryBoundP p n ↔ (¬p t ∨ 0 < n) ∧ ∀ (u : spec t), (mx u).IsQueryBoundP p (if p t then n - 1 else n)

@[simp]

theorem OracleComp.isQueryBoundP_pure {ι : Type u} {spec : OracleSpec ι} {α : Type u} (p : ι → Prop) [DecidablePred p] (x : α) (n : ℕ) : (pure x).IsQueryBoundP p n

@[simp]

theorem OracleComp.isQueryBoundP_query_iff {ι : Type u} {spec : OracleSpec ι} (p : ι → Prop) [DecidablePred p] (t : spec.Domain) (n : ℕ) : (liftM (OracleSpec.query t)).IsQueryBoundP p n ↔ p t → 0 < n

theorem OracleComp.IsQueryBoundP.proj {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] {B : Type u_1} {oa : OracleComp spec α} {b : B} {canQuery : ι → B → Prop} {cost : ι → B → B} (proj : B → ℕ) (h_can : ∀ (t : ι) (b' : B), canQuery t b' → p t → 0 < proj b') (h_cost : ∀ (t : ι) (b' : B), canQuery t b' → proj (cost t b') = if p t then proj b' - 1 else proj b') (h : oa.IsQueryBound b canQuery cost) : oa.IsQueryBoundP p (proj b)

Projection variant of IsQueryBound.proj that lands directly in IsQueryBoundP. Given a vector-budget bound on oa, project to a scalar budget along proj : B → ℕ and conclude an IsQueryBoundP bound at the projected coordinate. The two side conditions only have to address p-queries: allowed source steps must keep the projected budget positive when p fires (h_can), and the projection must commute with the cost step in the shape that IsQueryBoundP decrements on (h_cost).

Typical use: extract a per-predicate scalar bound (e.g. signing-only qS from a (qS, qH) pair) without spelling out the if … then 0 < b else True boilerplate at the call site.

theorem OracleComp.IsQueryBoundP.mono {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] {oa : OracleComp spec α} {n m : ℕ} (h : oa.IsQueryBoundP p n) (hnm : n ≤ m) : oa.IsQueryBoundP p m

theorem OracleComp.isQueryBoundP_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {p : ι → Prop} [DecidablePred p] {oa : OracleComp spec α} {ob : α → OracleComp spec β} {n m : ℕ} (h : oa.IsQueryBoundP p n) (h' : ∀ x ∈ support oa, (ob x).IsQueryBoundP p m) : (oa >>= ob).IsQueryBoundP p (n + m)

oa >>= ob is p-bounded by n + m when oa is p-bounded by n and every reachable continuation ob x is p-bounded by m.

theorem OracleComp.IsQueryBoundP.simulateQ_run_StateT_of_step {ι : Type u} {spec : OracleSpec ι} {α ι' : Type u} {spec' : OracleSpec ι'} {σ : Type u} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl : QueryImpl spec (StateT σ (OracleComp spec'))} {oa : OracleComp spec α} {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep : ∀ (t : spec.Domain) (s : σ), ((impl t).run s).IsQueryBoundP q (if p t then 1 else 0)) (s : σ) : ((simulateQ impl oa).run s).IsQueryBoundP q n

Transfer a predicate-targeted query bound through a StateT simulation whose handler step consumes at most one target-side predicate query exactly when the source query satisfies the source predicate.

This is the scalar IsQueryBoundP analogue of the more general vector-budget IsQueryBound.simulateQ_run_of_step. It is useful for logging and forwarding handlers whose state updates do not make additional oracle queries.

theorem OracleComp.isQueryBoundP_congr_pred {ι : Type u} {spec : OracleSpec ι} {α : Type u} {oa : OracleComp spec α} {p p' : ι → Prop} [DecidablePred p] [DecidablePred p'] {n : ℕ} (hpp : ∀ (t : ι), p t ↔ p' t) : oa.IsQueryBoundP p n ↔ oa.IsQueryBoundP p' n

Predicate-extensionality: replacing p with an equivalent predicate does not change the bound.

@[simp]

theorem OracleComp.isQueryBoundP_map_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {p : ι → Prop} [DecidablePred p] (oa : OracleComp spec α) (f : α → β) (n : ℕ) : (f <$> oa).IsQueryBoundP p n ↔ oa.IsQueryBoundP p n

theorem OracleComp.isQueryBoundP_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {p : ι → Prop} [DecidablePred p] {og : OracleComp spec (α → β)} {oa : OracleComp spec α} {n m : ℕ} (h : og.IsQueryBoundP p n) (h' : oa.IsQueryBoundP p m) : (og <*> oa).IsQueryBoundP p (n + m)

Forward-direction seq analogue of isQueryBoundP_bind. Reduces to the bind case via seq_eq_bind_map plus isQueryBoundP_map_iff to discharge the constant continuation.

theorem OracleComp.isQueryBoundP_iff_of_map_eq {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] {β : Type u} {oa : OracleComp spec α} {ob : OracleComp spec β} {f : α → β} {n : ℕ} (h : f <$> oa = ob) : oa.IsQueryBoundP p n ↔ ob.IsQueryBoundP p n

Predicate-targeted analogue of isQueryBound_iff_of_map_eq: if f <$> oa = ob for any f, then IsQueryBoundP transfers between them.

theorem OracleComp.IsQueryBoundP.and_isQueryBound_pair {ι : Type u} {spec : OracleSpec ι} {α : Type u} {oa : OracleComp spec α} {p₁ p₂ : ι → Prop} [DecidablePred p₁] [DecidablePred p₂] {n₁ n₂ : ℕ} (h₁ : oa.IsQueryBoundP p₁ n₁) (h₂ : oa.IsQueryBoundP p₂ n₂) : oa.IsQueryBound (n₁, n₂) (fun (t : ι) (b : ℕ × ℕ) => (¬p₁ t ∨ 0 < b.1) ∧ (¬p₂ t ∨ 0 < b.2)) fun (t : ι) (b : ℕ × ℕ) => (if p₁ t then b.1 - 1 else b.1, if p₂ t then b.2 - 1 else b.2)

The conjunction of two scalar IsQueryBoundP bounds combines into a vector-budget IsQueryBound whose canQuery admits a query iff every active predicate has positive budget, and whose cost decrements only the matching coordinates.

This is the canonical bridge from the predicate-targeted scalar API to the vector-budget API: proofs that decompose a multi-oracle adversary into per-oracle counts can use the conjunction form for hypothesis statements while reusing the existing IsQueryBound propagation machinery (such as simulateQ_run_of_step) on the combined bound. The two predicates need not be disjoint — at an overlapping query both coordinates decrement and both must be positive, which exactly tracks the independent per-predicate counts.

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

theorem OracleComp.isPerIndexQueryBound_iff_isRollBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] (oa : OracleComp spec α) (qb : ι → ℕ) : oa.IsPerIndexQueryBound qb ↔ PFunctor.FreeM.IsRollBound oa qb (fun (t : spec.toPFunctor.A) (qb : ι → ℕ) => 0 < qb t) fun (t : spec.toPFunctor.A) (qb : ι → ℕ) => Function.update qb t (qb t - 1)

IsPerIndexQueryBound is IsRollBound on the underlying FreeM with the per-index validity and cost.

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

theorem OracleComp.isPerIndexQueryBound_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type u} [DecidableEq ι] {og : OracleComp spec (α → β)} {oa : OracleComp spec α} {qb₁ qb₂ : ι → ℕ} (h1 : og.IsPerIndexQueryBound qb₁) (h2 : oa.IsPerIndexQueryBound qb₂) : (og <*> oa).IsPerIndexQueryBound (qb₁ + qb₂)

Forward-direction seq analogue of isPerIndexQueryBound_bind. Reduces to the bind case via seq_eq_bind_map plus isPerIndexQueryBound_map_iff to discharge the constant continuation.

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

Per-index analogue of isQueryBound_iff_of_map_eq: if f <$> oa = ob for any f, then IsPerIndexQueryBound transfers between them.

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.

Uniform per-step transfer for simulateQ

If each step impl t makes at most one query of the matching index t (and none of any other), the source's per-index bound transfers across simulateQ. Captures the cachingOracle / seededOracle shape, where each step delegates to a single query t.

theorem OracleComp.IsPerIndexQueryBound.simulateQ_run_of_uniform_step {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] {σ : Type u} {impl : QueryImpl spec (StateT σ (OracleComp spec))} {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep : ∀ (t : spec.Domain) (s : σ), ((impl t).run s).IsPerIndexQueryBound (Function.update 0 t 1)) (s : σ) : ((simulateQ impl oa).run s).IsPerIndexQueryBound qb

theorem OracleComp.IsPerIndexQueryBound.simulateQ_of_uniform_step {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] {impl : QueryImpl spec (OracleComp spec)} {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep : ∀ (t : spec.Domain), (impl t).IsPerIndexQueryBound (Function.update 0 t 1)) : (simulateQ impl oa).IsPerIndexQueryBound qb

Stateless analogue of IsPerIndexQueryBound.simulateQ_run_of_uniform_step: when the simulation target monad is OracleComp spec directly (no StateT layer), each step's single-t-query bound transfers without an external state argument.

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_iff_isRollBound {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (n : ℕ) : oa.IsTotalQueryBound n ↔ PFunctor.FreeM.IsRollBound oa n (fun (x : spec.toPFunctor.A) (b : ℕ) => 0 < b) fun (x : spec.toPFunctor.A) (b : ℕ) => b - 1

IsTotalQueryBound is IsRollBound on the underlying FreeM with a single-counter validity (0 < b) and cost (b - 1), independent of the oracle index.

theorem OracleComp.isTotalQueryBound_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} {t : spec.Domain} {mx : spec.Range t → OracleComp spec α} {n : ℕ} : (liftM (OracleSpec.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₂)

IsTotalQueryBound instantiates the generic vector-budget bind at B := ℕ, combine := (· + ·), with the canQuery / cost obligations both discharged by omega.

theorem OracleComp.isTotalQueryBound_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type u} {og : OracleComp spec (α → β)} {oa : OracleComp spec α} {n₁ n₂ : ℕ} (h1 : og.IsTotalQueryBound n₁) (h2 : oa.IsTotalQueryBound n₂) : (og <*> oa).IsTotalQueryBound (n₁ + n₂)

Forward-direction seq analogue of isTotalQueryBound_bind. Reduces to the bind case via seq_eq_bind_map plus the IsTotalQueryBound-flavoured isQueryBound_map_iff to discharge the constant continuation.

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 (OracleSpec.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 (OracleSpec.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} {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.IsTotalQueryBound.simulateQ_of_step {ι : Type u} {spec : OracleSpec ι} {α ι' : Type u} {spec' : OracleSpec ι'} {impl : QueryImpl spec (OracleComp spec')} {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain), (impl t).IsTotalQueryBound 1) : (simulateQ impl oa).IsTotalQueryBound n

Stateless analogue of IsTotalQueryBound.simulateQ_run_of_step: when the simulation target monad is OracleComp spec' directly (no StateT layer), every per-step bound applies without an external state argument. Captures the liftComp shape, where each source query becomes one query in the larger spec.

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 (OracleSpec.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.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.countingOracle.support_simulate_nonempty {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [spec.Inhabited] (oa : OracleComp spec α) : (support (countingOracle.simulate oa 0)).Nonempty

The counting-oracle simulation of any OracleComp has non-empty support whenever every oracle range is inhabited. Used by the converse direction of isTotalQueryBound_iff_counting_total_le.

theorem OracleComp.isTotalQueryBound_iff_counting_total_le {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [Fintype ι] [spec.Inhabited] {oa : OracleComp spec α} {n : ℕ} : oa.IsTotalQueryBound n ↔ ∀ z ∈ support (countingOracle.simulate oa 0), ∑ i : ι, z.2 i ≤ n

Converse of IsTotalQueryBound.counting_total_le: a counting-oracle bound on every support path implies the structural total query bound. Together they characterize IsTotalQueryBound purely in terms of the counting-oracle support.

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

Conversions and soundness for IsQueryBoundP

theorem OracleComp.IsTotalQueryBound.isQueryBoundP {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) : oa.IsQueryBoundP p n

A total query bound implies a predicate-targeted bound for every predicate p.

theorem OracleComp.isQueryBoundP_true_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (n : ℕ) : oa.IsQueryBoundP (fun (x : ι) => True) n ↔ oa.IsTotalQueryBound n

With the always-true predicate, IsQueryBoundP reduces to IsTotalQueryBound.

@[simp]

theorem OracleComp.isQueryBoundP_false {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (n : ℕ) : oa.IsQueryBoundP (fun (x : ι) => False) n

The always-false predicate places no constraint.

theorem OracleComp.IsPerIndexQueryBound.isQueryBoundP {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] [DecidableEq ι] [Fintype ι] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) : oa.IsQueryBoundP p (∑ i : ι with p i, qb i)

A per-index bound implies a predicate-targeted bound at the sum of the per-index budgets over the indices satisfying p.

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

Soundness: any path of the counting-oracle simulation of a p-bounded computation has sum of per-index counts over p-indices at most n.

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

Residual bound via the counting oracle: after any partial counting-simulation of oa, the continuation ob is p-bounded by n minus the filtered count so far.

theorem OracleComp.isQueryBoundP_iff_counting_filter_le {ι : Type u} {spec : OracleSpec ι} {α : Type u} {p : ι → Prop} [DecidablePred p] [DecidableEq ι] [Fintype ι] [spec.Inhabited] {oa : OracleComp spec α} {n : ℕ} : oa.IsQueryBoundP p n ↔ ∀ z ∈ support (countingOracle.simulate oa 0), ∑ i : ι with p i, z.2 i ≤ n

Predicate-targeted analogue of isTotalQueryBound_iff_counting_total_le: a counting-oracle filtered-sum bound characterizes the structural IsQueryBoundP bound.

theorem OracleComp.IsQueryBoundP.simulateQ_run_of_step {ι : Type u} {spec : OracleSpec ι} {α ι' : Type u} {spec' : OracleSpec ι'} {σ : Type u} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl : QueryImpl spec (StateT σ (OracleComp spec'))} {oa : OracleComp spec α} {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p : ∀ (t : ι), p t → ∀ (s : σ), ((impl t).run s).IsQueryBoundP q 1) (hstep_np : ∀ (t : ι), ¬p t → ∀ (s : σ), ((impl t).run s).IsQueryBoundP q 0) (s : σ) : ((simulateQ impl oa).run s).IsQueryBoundP q n

Transfer a predicate-targeted query bound through simulateQ into a stateful target semantics, provided each simulated source query step is itself q-bounded (by 1 on p-indices, by 0 on ¬ p-indices).

theorem OracleComp.IsQueryBoundP.simulateQ_of_step {ι : Type u} {spec : OracleSpec ι} {α ι' : Type u} {spec' : OracleSpec ι'} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl : QueryImpl spec (OracleComp spec')} {oa : OracleComp spec α} {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p : ∀ (t : ι), p t → (impl t).IsQueryBoundP q 1) (hstep_np : ∀ (t : ι), ¬p t → (impl t).IsQueryBoundP q 0) : (simulateQ impl oa).IsQueryBoundP q n

Stateless analogue of IsQueryBoundP.simulateQ_run_of_step: when the simulation target monad is OracleComp spec' directly (no StateT layer), the per-step bounds apply without an external state argument. Captures the liftComp shape, where each p-step becomes one q-query and each ¬ p-step is q-free.

theorem OracleComp.IsQueryBoundP.simulateQ_run_add_of_step {α ι₁ ι₂ ι' : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec' : OracleSpec ι'} {σ : Type u} {p : ι₁ ⊕ ι₂ → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp spec'))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp spec'))} {oa : OracleComp (spec₁ + spec₂) α} {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p₁ : ∀ (t : ι₁), p (Sum.inl t) → ∀ (s : σ), ((impl₁ t).run s).IsQueryBoundP q 1) (hstep_np₁ : ∀ (t : ι₁), ¬p (Sum.inl t) → ∀ (s : σ), ((impl₁ t).run s).IsQueryBoundP q 0) (hstep_p₂ : ∀ (t : ι₂), p (Sum.inr t) → ∀ (s : σ), ((impl₂ t).run s).IsQueryBoundP q 1) (hstep_np₂ : ∀ (t : ι₂), ¬p (Sum.inr t) → ∀ (s : σ), ((impl₂ t).run s).IsQueryBoundP q 0) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsQueryBoundP q n

Transfer a predicate-targeted bound through simulateQ with a sum-of-implementations impl₁ + impl₂ on a sum source spec spec₁ + spec₂. The source predicate p is split into its .inl and .inr branches, with separate step hypotheses for each impl on its own sub-predicate.

theorem OracleComp.IsQueryBoundP.simulateQ_run_add_inl_of_step {α ι₁ ι₂ ι' : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec' : OracleSpec ι'} {σ : Type u} {p : ι₁ ⊕ ι₂ → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp spec'))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp spec'))} {oa : OracleComp (spec₁ + spec₂) α} {n : ℕ} (hp_inr : ∀ (t : ι₂), ¬p (Sum.inr t)) (h : oa.IsQueryBoundP p n) (hstep_p₁ : ∀ (t : ι₁), p (Sum.inl t) → ∀ (s : σ), ((impl₁ t).run s).IsQueryBoundP q 1) (hstep_np₁ : ∀ (t : ι₁), ¬p (Sum.inl t) → ∀ (s : σ), ((impl₁ t).run s).IsQueryBoundP q 0) (hstep_right : ∀ (t : spec₂.Domain) (s : σ), ((impl₂ t).run s).IsQueryBoundP q 0) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsQueryBoundP q n

Specialization of IsQueryBoundP.simulateQ_run_add_of_step when the source predicate is vacuously false on .inr _ queries: only impl₁ interacts with the predicate, and impl₂ only needs a uniform 0-bound step.

theorem OracleComp.IsQueryBoundP.simulateQ_run_add_inr_of_step {α ι₁ ι₂ ι' : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec' : OracleSpec ι'} {σ : Type u} {p : ι₁ ⊕ ι₂ → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp spec'))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp spec'))} {oa : OracleComp (spec₁ + spec₂) α} {n : ℕ} (hp_inl : ∀ (t : ι₁), ¬p (Sum.inl t)) (h : oa.IsQueryBoundP p n) (hstep_left : ∀ (t : spec₁.Domain) (s : σ), ((impl₁ t).run s).IsQueryBoundP q 0) (hstep_p₂ : ∀ (t : ι₂), p (Sum.inr t) → ∀ (s : σ), ((impl₂ t).run s).IsQueryBoundP q 1) (hstep_np₂ : ∀ (t : ι₂), ¬p (Sum.inr t) → ∀ (s : σ), ((impl₂ t).run s).IsQueryBoundP q 0) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsQueryBoundP q n

Specialization of IsQueryBoundP.simulateQ_run_add_of_step when the source predicate is vacuously false on .inl _ queries: only impl₂ interacts with the predicate, and impl₁ only needs a uniform 0-bound step.

Total-bound sum-handler transfer

IsTotalQueryBound lifts across simulateQ (impl₁ + impl₂) oa whenever each underlying handler makes at most one query per step. The signature mirrors IsQueryBoundP.simulateQ_run_add_of_step without the predicate machinery: every step on either side counts toward the same uniform budget.

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

theorem OracleComp.IsTotalQueryBound.simulateQ_run_add_inl_of_step {α ι₁ ι₂ ι' : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec' : OracleSpec ι'} {σ : Type u} {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp spec'))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp spec'))} {oa : OracleComp (spec₁ + spec₂) α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep₁ : ∀ (t : ι₁) (s : σ), ((impl₁ t).run s).IsTotalQueryBound 1) (hstep₂ : ∀ (t : ι₂) (s : σ), ((impl₂ t).run s).IsTotalQueryBound 0) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsTotalQueryBound n

Specialization of IsTotalQueryBound.simulateQ_run_add_of_step to a left-only interaction: impl₂ only needs a uniform 0-bound step.

theorem OracleComp.IsTotalQueryBound.simulateQ_run_add_inr_of_step {α ι₁ ι₂ ι' : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec' : OracleSpec ι'} {σ : Type u} {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp spec'))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp spec'))} {oa : OracleComp (spec₁ + spec₂) α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep₁ : ∀ (t : ι₁) (s : σ), ((impl₁ t).run s).IsTotalQueryBound 0) (hstep₂ : ∀ (t : ι₂) (s : σ), ((impl₂ t).run s).IsTotalQueryBound 1) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsTotalQueryBound n

Specialization of IsTotalQueryBound.simulateQ_run_add_of_step to a right-only interaction: impl₁ only needs a uniform 0-bound step.

Per-index sum-handler transfer

The per-index analogue of IsTotalQueryBound.simulateQ_run_add_of_step: each side's step is required to make at most one query of its corresponding sum-tagged index in the result spec, mirroring the single-spec simulateQ_run_of_uniform_step.

theorem OracleComp.IsPerIndexQueryBound.simulateQ_run_add_of_uniform_step {α ι₁ ι₂ : Type u} [DecidableEq ι₁] [DecidableEq ι₂] {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type u} {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp (spec₁ + spec₂)))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp (spec₁ + spec₂)))} {oa : OracleComp (spec₁ + spec₂) α} {qb : ι₁ ⊕ ι₂ → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep₁ : ∀ (t : ι₁) (s : σ), ((impl₁ t).run s).IsPerIndexQueryBound (Function.update 0 (Sum.inl t) 1)) (hstep₂ : ∀ (t : ι₂) (s : σ), ((impl₂ t).run s).IsPerIndexQueryBound (Function.update 0 (Sum.inr t) 1)) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsPerIndexQueryBound qb

theorem OracleComp.IsPerIndexQueryBound.simulateQ_run_add_inl_of_uniform_step {α ι₁ ι₂ : Type u} [DecidableEq ι₁] [DecidableEq ι₂] {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type u} {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp (spec₁ + spec₂)))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp (spec₁ + spec₂)))} {oa : OracleComp (spec₁ + spec₂) α} {qb : ι₁ ⊕ ι₂ → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep₁ : ∀ (t : ι₁) (s : σ), ((impl₁ t).run s).IsPerIndexQueryBound (Function.update 0 (Sum.inl t) 1)) (hstep₂ : ∀ (t : ι₂) (s : σ), ((impl₂ t).run s).IsPerIndexQueryBound 0) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsPerIndexQueryBound qb

Specialization of IsPerIndexQueryBound.simulateQ_run_add_of_uniform_step to a left-only interaction: impl₂ only needs a uniform 0-step.

theorem OracleComp.IsPerIndexQueryBound.simulateQ_run_add_inr_of_uniform_step {α ι₁ ι₂ : Type u} [DecidableEq ι₁] [DecidableEq ι₂] {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type u} {impl₁ : QueryImpl spec₁ (StateT σ (OracleComp (spec₁ + spec₂)))} {impl₂ : QueryImpl spec₂ (StateT σ (OracleComp (spec₁ + spec₂)))} {oa : OracleComp (spec₁ + spec₂) α} {qb : ι₁ ⊕ ι₂ → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep₁ : ∀ (t : ι₁) (s : σ), ((impl₁ t).run s).IsPerIndexQueryBound 0) (hstep₂ : ∀ (t : ι₂) (s : σ), ((impl₂ t).run s).IsPerIndexQueryBound (Function.update 0 (Sum.inr t) 1)) (s : σ) : ((simulateQ (impl₁ + impl₂) oa).run s).IsPerIndexQueryBound qb

Specialization of IsPerIndexQueryBound.simulateQ_run_add_of_uniform_step to a right-only interaction: impl₁ only needs a uniform 0-step.

Biconditional transfer under query-count-preserving simulators

loggingOracle, countingOracle, and the withTrace* / withCost / withCounting combinators interpret each source query as exactly one underlying query, threading writer bookkeeping that the underlying simulation does not see. Bounds transfer biconditionally via the fst_map_run_* projection identities and isXQueryBound_iff_of_map_eq.

Cache-hit / seed-hit handlers (cachingOracle, randomOracle, seededOracle) discard queries and so admit only the forward direction — use simulateQ_run_of_step for those.

theorem OracleComp.isTotalQueryBound_run_simulateQ_countingOracle_iff {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (n : ℕ) : (simulateQ OracleSpec.countingOracle oa).run.IsTotalQueryBound n ↔ oa.IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_countingOracle_iff {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (p : ι → Prop) [DecidablePred p] (n : ℕ) : (simulateQ OracleSpec.countingOracle oa).run.IsQueryBoundP p n ↔ oa.IsQueryBoundP p n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withTraceBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ (so.withTraceBefore traceFn) mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withTraceBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ (so.withTraceBefore traceFn) mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withTraceAppend_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ (so.withTraceAppend traceFn) mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withTraceAppend_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ (so.withTraceAppend traceFn) mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withTrace_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ (so.withTrace traceFn) mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withTrace_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ (so.withTrace traceFn) mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withTraceAppendBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ (so.withTraceAppendBefore traceFn) mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withTraceAppendBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ (so.withTraceAppendBefore traceFn) mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withCost_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (costFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ (so.withCost costFn) mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withCost_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (costFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ (so.withCost costFn) mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withCounting_iff {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) {α : Type u} (mx : OracleComp spec α) (n : ℕ) : (simulateQ so.withCounting mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withCounting_iff {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) {α : Type u} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ so.withCounting mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

Per-index analogues

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_countingOracle_iff {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (qb : ι → ℕ) : (simulateQ OracleSpec.countingOracle oa).run.IsPerIndexQueryBound qb ↔ oa.IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withTraceBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ (so.withTraceBefore traceFn) mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withTrace_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ (so.withTrace traceFn) mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withTraceAppendBefore_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ (so.withTraceAppendBefore traceFn) mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withTraceAppend_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ (so.withTraceAppend traceFn) mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withCost_iff {ι : Type u} {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} {ω : Type u} [Monoid ω] (so : QueryImpl spec (OracleComp spec')) (costFn : spec.Domain → ω) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ (so.withCost costFn) mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withCounting_iff {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} [DecidableEq ι'] {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) {α : Type u} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ so.withCounting mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

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.