Query-Bounded Adversary Infrastructure

This file provides infrastructure for modeling adversaries with bounded query access to oracles. This is fundamental to cryptographic security proofs where security bounds depend on the number of oracle queries.

Main definitions

• boundedOracleCall - Single oracle call with query counting
• queryCountPre - Precondition: query count is below bound
• queryCountPost - Postcondition: query count incremented by 1

Main results

• pHoare_bounded_call - pHL rule for a single bounded oracle call
• prEvent_bind_eq - Bad mass of a bind as the expectation of the continuation's bad mass
• prEventComp_bind_step_le - Per-step subadditivity: one step adds at most ε
• prBad_induction - Adaptive union bound: Pr[bad after q calls] ≤ q * ε
• advantage_le_query_bound_derived - Advantage bound ≤ q * ε from per-step freshness

Design

Rather than implementing query-bounded oracles as stateful wrappers (which would require specific location assignments), we provide:

1. Abstract query counting: A precondition/postcondition pair that tracks a query count value through pHL judgments.

2. Inductive probability bounds: Theorems that bound the probability of bad events by q * ε when each query contributes at most ε.

3. Oracle call patterns: Composable patterns for reasoning about sequences of oracle calls.

This approach integrates with the existing pHL rules from Rules.lean and the FEL machinery from Bridge.lean / FailureEvent.lean.

References

• EasyCrypt: phoare with oracle call counting
• Bellare & Rogaway: birthday bound via query counting
• Shoup: "Sequences of Games" (query counting methodology)

Query Counting via pHL Predicates

Instead of tracking query counts in specific heap locations, we parametrize over an abstract "counter" function on the heap. This allows the user to choose their own counter representation.

@[reducible, inline]

abbrev CatCrypt.Unary.QueryCounter : Type

A query counter is a function from heaps to natural numbers. The user defines this based on their specific heap layout.

Equations

• CatCrypt.Unary.QueryCounter = (CatCrypt.Core.Heap → ℕ)

def CatCrypt.Unary.counterAt (count : QueryCounter) (n : ℕ) : UPre

Precondition: the query counter is at value n

Equations

• CatCrypt.Unary.counterAt count n h = (count h = n)

def CatCrypt.Unary.counterBounded (count : QueryCounter) (q : ℕ) : UPre

Precondition: the query counter is at most q

Equations

• CatCrypt.Unary.counterBounded count q h = (count h ≤ q)

def CatCrypt.Unary.counterIncremented (count : QueryCounter) : UPost Unit

Postcondition: the counter was incremented by exactly 1

Equations

• CatCrypt.Unary.counterIncremented count x✝ h' = ∀ (h₀ : CatCrypt.Core.Heap), count h₀ + 1 = count h'

Abstract Bounded Oracle Call

A bounded oracle call is modeled as: check counter, if under budget then call oracle and increment counter, else return default/fail.

noncomputable def CatCrypt.Unary.boundedOracleCall {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (q : ℕ) (oracleCall : Core.SPComp V) [Inhabited V] : Core.SPComp V

A single oracle call that increments a counter.

This represents the pattern:

let n ← get counter_loc
if n < q then
  set counter_loc (n + 1)
  oracle k
else
  fail -- or return default

We model this abstractly: the computation oracleCall k is wrapped with counter tracking.

Equations

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

noncomputable def CatCrypt.Unary.countedOracleCall {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (oracleCall : Core.SPComp V) : Core.SPComp V

A single oracle call that always proceeds (no budget check). Used when the budget is known to be sufficient from context.

Equations

• CatCrypt.Unary.countedOracleCall getCount setCount oracleCall = getCount.bind fun (n : ℕ) => (setCount (n + 1)).bind fun (x : Unit) => oracleCall

pHL Rules for Query Counting

theorem CatCrypt.Unary.pHoare_bounded_call {V : Type u_2} (getCount : Core.SPComp ℕ) (setCount : ℕ → Core.SPComp Unit) (q : ℕ) (oracleCall : Core.SPComp V) [Inhabited V] {P : UPre} {Q : UPost V} (h_get : pHoare P getCount fun (x : ℕ) (h' : Core.Heap) => P h') (h_set : ∀ (m : ℕ), pHoare P (setCount m) fun (x : Unit) (h' : Core.Heap) => P h') (h_oracle : pHoare P oracleCall Q) (h_default : ∀ (h : Core.Heap), P h → Q default h) : pHoare P (boundedOracleCall getCount setCount q oracleCall) Q

pHoare rule for bounded oracle call: if the call computation satisfies a postcondition Q, then the full bounded oracle call also satisfies Q (since it either calls the oracle or returns default).

The user proves pHoare P oracleCall Q and ∀ h, P h → Q default h (the default case satisfies Q too), and gets pHoare P (boundedOracleCall ...) Q.

theorem CatCrypt.Unary.query_count_after_calls {α : Type u_3} (count : QueryCounter) (q : ℕ) (c : Core.SPComp α) (h_init : ∀ (h : Core.Heap), count h = 0 → True) (h_calls : pHoare (counterAt count 0) c fun (x : α) (h' : Core.Heap) => count h' ≤ q) : pHoare (counterAt count 0) c fun (x : α) (h' : Core.Heap) => count h' ≤ q

Key theorem: after q calls to countedOracleCall, the counter has been incremented q times.

This is stated abstractly: if we start with counter = 0 and make exactly q calls, the counter ends at q.

Inductive Probability Bounds

The key result: if each oracle call has at most ε probability of triggering a bad event, and we make at most q calls, then the overall bad probability is at most q * ε.

Rather than proving this inductively over the number of calls (which requires tracking execution traces), we provide it as a composition lemma that the user applies.

theorem CatCrypt.Unary.birthday_bound_pattern (G : Core.SPComp Bool) (h₀ : Core.Heap) (collision : Core.Heap → Prop) (q N : ℕ) (h_bound : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)) : (prEventComp G h₀ fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)

Birthday bound pattern: q queries to a domain of size N gives collision probability at most q * (q-1) / (2 * N).

This is a definitional helper that states the standard birthday bound formula. The actual proof obligation is pushed to the user, who must show the per-query collision probability and compose with the query count.

Composition Patterns

Reusable patterns for composing query-bounded computations.

theorem CatCrypt.Unary.query_bound_seq {α : Type u_3} (count : QueryCounter) (c₁ : Core.SPComp α) (c₂ : α → Core.SPComp Bool) (q₁ q₂ : ℕ) (h₁ : pHoare truePre c₁ fun (x : α) (h' : Core.Heap) => count h' ≤ q₁) (h₂ : ∀ (a : α), pHoare (fun (h : Core.Heap) => count h ≤ q₁) (c₂ a) fun (x : Bool) (h' : Core.Heap) => count h' ≤ q₁ + q₂) : pHoare truePre (c₁.bind c₂) fun (x : Bool) (h' : Core.Heap) => count h' ≤ q₁ + q₂

Sequential composition preserves query bounds.

If c₁ uses at most q₁ queries and c₂ uses at most q₂ queries, then c₁ >> c₂ uses at most q₁ + q₂ queries.

theorem CatCrypt.Unary.query_bound_from_zero (count : QueryCounter) (c : Core.SPComp Bool) (q : ℕ) (h : pHoare (counterAt count 0) c fun (x : Bool) (h' : Core.Heap) => count h' ≤ q) : pHoare (counterAt count 0) c fun (x : Bool) (h' : Core.Heap) => count h' ≤ q

If the counter starts at 0 and the computation makes at most q calls, the count is bounded by q. This is a simple wrapper for readability.

Adaptive q-Query Union Bound

A q-fold loop of oracle calls, where each call adds at most ε to the bad-event probability, has total bad probability at most q * ε.

The loop is repeatStep step q, an unrolled q-fold sequential composition of a single step step : SPComp Unit. The bound is proved by induction on q from a per-step increment hypothesis; that increment is in turn derived from a single-step freshness bound via prEventComp_bind_step_le.

theorem CatCrypt.Unary.sdistr_mass_le_one {β : Type u_4} (d : Prob.SDistr β) : d.mass ≤ 1

The total mass of a sub-distribution is at most one.

noncomputable def CatCrypt.Unary.repeatStep (step : Core.SPComp Unit) : ℕ → Core.SPComp Unit

A q-fold sequential iteration of a single step computation. repeatStep step 0 is the trivial computation; repeatStep step (q+1) runs repeatStep step q and then one more step.

Equations

• CatCrypt.Unary.repeatStep step 0 = CatCrypt.Core.SPComp.pure ()
• CatCrypt.Unary.repeatStep step q.succ = (CatCrypt.Unary.repeatStep step q).bind fun (x : Unit) => step

theorem CatCrypt.Unary.prEvent_pure {δ : Type u_4} (a : δ) (h : Core.Heap) (bad : Core.Heap → Prop) : (prEvent (Prob.SDistr.pure (a, h)) fun (x : δ) (h' : Core.Heap) => bad h') = if bad h then 1 else 0

The bad-event probability of a point mass at (a, h) is the indicator of bad h: 1 if bad h, else 0.

theorem CatCrypt.Unary.prEventComp_pure {α : Type u_3} (a : α) (h₀ : Core.Heap) (bad : Core.Heap → Prop) : (prEventComp (Core.SPComp.pure a) h₀ fun (x : α) (h' : Core.Heap) => bad h') = if bad h₀ then 1 else 0

The bad-event probability of a pure computation from h₀ is the indicator of bad h₀: 1 if bad h₀, else 0.

theorem CatCrypt.Unary.SDistr_bind_apply_some {β : Type u_4} {γ : Type u_5} (d : Prob.SDistr (β × Core.Heap)) (g : β × Core.Heap → Prob.SDistr (γ × Core.Heap)) (b : γ × Core.Heap) : (d.bind g) (some b) = ∑' (a : β × Core.Heap), d (some a) * (g a) (some b)

Pointwise value of a sub-distribution bind at a some outcome: the probability sums, over reachable intermediate outcomes, the intermediate probability times the continuation probability.

theorem CatCrypt.Unary.prEvent_bind_eq {β : Type u_4} {γ : Type u_5} (d : Prob.SDistr (β × Core.Heap)) (g : β × Core.Heap → Prob.SDistr (γ × Core.Heap)) (E : γ → Core.Heap → Prop) : prEvent (d.bind g) E = ∑' (q : β × Core.Heap), d (some q) * prEvent (g q) E

Bad-mass of a sub-distribution bind: the event probability of d.bind g is the d-expectation of the event probability of the continuation g started from each reachable intermediate outcome.

theorem CatCrypt.Unary.prEvent_bind_step_eq_tsum (m step : Core.SPComp Unit) (h₀ : Core.Heap) (bad : Core.Heap → Prop) : (prEventComp (m.bind fun (x : Unit) => step) h₀ fun (x : Unit) (h' : Core.Heap) => bad h') = ∑' (p : Unit × Core.Heap), (m h₀) (some p) * prEvent (step p.2) fun (x : Unit) (h' : Core.Heap) => bad h'

Decomposition of the bad-event mass of a loop step: the bad mass of m.bind (fun _ => step) is the m-expectation of the bad mass of step started from each reachable intermediate heap.

theorem CatCrypt.Unary.prEventComp_bind_step_le (m step : Core.SPComp Unit) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (ε : ENNReal) (h_fresh : ∀ (h₁ : Core.Heap), ¬bad h₁ → (prEvent (step h₁) fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ε) : (prEventComp (m.bind fun (x : Unit) => step) h₀ fun (x : Unit) (h' : Core.Heap) => bad h') ≤ (prEventComp m h₀ fun (x : Unit) (h' : Core.Heap) => bad h') + ε

Per-step subadditivity of bad mass: if from every non-bad reachable heap the single step introduces bad with probability at most ε, then prepending any prefix m adds at most ε to the bad probability.

theorem CatCrypt.Unary.prBad_induction (step : Core.SPComp Unit) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (ε : ENNReal) (h_start : ¬bad h₀) (h_fresh : ∀ (h₁ : Core.Heap), ¬bad h₁ → (prEvent (step h₁) fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ε) (q : ℕ) : (prEventComp (repeatStep step q) h₀ fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ↑q * ε

Adaptive q-query union bound.

A q-fold loop of step, where each single step from a non-bad heap introduces the bad event with probability at most ε, has total bad probability at most q * ε.

Proved by induction on q: the base case is 0 (the initial heap is non-bad); the step case combines the inductive hypothesis with the per-step increment prEventComp_bind_step_le.

theorem CatCrypt.Unary.prBad_of_bounded_count (step : Core.SPComp Unit) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (q : ℕ) (ε : ENNReal) (h_start : ¬bad h₀) (h_fresh : ∀ (h₁ : Core.Heap), ¬bad h₁ → (prEvent (step h₁) fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ε) : (prEventComp (repeatStep step q) h₀ fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ↑q * ε

Adaptive q-query union bound over a loop of counted oracle calls.

If step from any non-bad heap introduces the bad event with probability at most ε, and the initial heap is non-bad, then after q iterations the bad probability is at most q * ε. Derived from the per-step freshness hypothesis by prBad_induction, not assumed.

noncomputable def CatCrypt.Unary.loopGame (step : Core.SPComp Unit) (q : ℕ) (b₀ : Bool) : Core.SPComp Bool

A q-query loop presented as a Bool game: run repeatStep step q, then return the fixed answer b₀. The tail SPComp.pure b₀ leaves the heap unchanged, so it does not affect the bad-event probability.

Equations

• CatCrypt.Unary.loopGame step q b₀ = (CatCrypt.Unary.repeatStep step q).bind fun (x : Unit) => CatCrypt.Core.SPComp.pure b₀

theorem CatCrypt.Unary.prEventComp_loopGame (step : Core.SPComp Unit) (q : ℕ) (b₀ : Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) : (prEventComp (loopGame step q b₀) h₀ fun (x : Bool) (h' : Core.Heap) => bad h') = prEventComp (repeatStep step q) h₀ fun (x : Unit) (h' : Core.Heap) => bad h'

The bad-event probability of loopGame equals that of the underlying loop: the deterministic Bool-returning tail preserves the final heap.

theorem CatCrypt.Unary.advantage_le_query_bound_derived (step : Core.SPComp Unit) (q : ℕ) (b₀ : Bool) (G₁ : Core.SPComp Bool) (bad : Core.Heap → Prop) (ε : ENNReal) (h_start : ¬bad Core.Heap.empty) (h_fresh : ∀ (h₁ : Core.Heap), ¬bad h₁ → (prEvent (step h₁) fun (x : Unit) (h' : Core.Heap) => bad h') ≤ ε) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (loopGame step q b₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll : isLossless (loopGame step q b₀)) : Crypto.Advantage (loopGame step q b₀) G₁ ≤ ↑q * ε

Adaptive q-query union bound as an advantage bound.

For the q-query game loopGame step q b₀, if each step from a non-bad heap introduces the bad event with probability at most ε, and the game agrees with G₁ on all non-bad outcomes (and is lossless), then the advantage is at most q * ε. The bad bound is supplied by prBad_induction, not assumed.

Integration with Failure Event Lemma

Combine query bounds with the FEL to obtain concrete security bounds.

theorem CatCrypt.Unary.advantage_le_query_bound (G₀ G₁ : Core.SPComp Bool) (bad : Core.Heap → Prop) (q : ℕ) (ε : ENNReal) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (h_bad_bound : (prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad h') ≤ ↑q * ε) : Crypto.Advantage G₀ G₁ ≤ ↑q * ε

Combined FEL + query bound: advantage ≤ q * ε.

Given:

• Games agree on non-bad outcomes
• G₀ is lossless
• Bad probability under G₀ is at most q * ε Then advantage is at most q * ε.

theorem CatCrypt.Unary.advantage_le_birthday (G₀ G₁ : Core.SPComp Bool) (collision : Core.Heap → Prop) (q N : ℕ) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬collision h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (h_collision_bound : (prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => collision h') ≤ ↑(q * (q - 1)) / ↑(2 * N)) : Crypto.Advantage G₀ G₁ ≤ ↑(q * (q - 1)) / ↑(2 * N)

Combined FEL + birthday bound: advantage ≤ q²/(2N).

Specialization of advantage_le_query_bound for the common birthday-bound case (e.g., PRF/PRP switching).