Enforcement Oracle

Oracle wrapper that enforces a query budget by silently dropping queries beyond the budget. This implements EasyCrypt's Enforce/Bounder pattern.

Main Definitions

• enforceOracle: Oracle that tracks remaining budget via StateT and returns default for queries exceeding the budget.

Main Results

• enforceOracle.fst_map_run_simulateQ: Enforcement is transparent for computations within their query bound.

def enforceOracle {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [spec.Inhabited] : QueryImpl spec (StateT (ι → ℕ) (OracleComp spec))

Enforcement oracle: wraps the original oracle with a per-index budget tracked via StateT. When the remaining budget for the queried oracle is positive, the query is forwarded and the budget decremented. When the budget is exhausted, default is returned silently.

@[simp]

theorem enforceOracle.run_apply {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [spec.Inhabited] (t : ι) (budget : ι → ℕ) : (enforceOracle t).run budget = if 0 < budget t then (fun (x : spec.Range t) => (x, Function.update budget t (budget t - 1))) <$> liftM (OracleQuery.query t) else pure (default, budget)

theorem enforceOracle.fst_map_run_simulateQ {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [spec.Inhabited] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) : Prod.fst <$> (simulateQ enforceOracle oa).run qb = oa

When the computation is within its query bound, enforcement is transparent: the output distribution is identical to running without enforcement.

theorem enforceOracle.probEvent_counting_budget_eq {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [spec.Inhabited] [spec.Fintype] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (p : α → Prop) : (probEvent (countingOracle.simulate oa 0) fun (z : α × OracleSpec.QueryCount ι) => p z.1 ∧ z.2 ≤ qb) = probEvent oa p

For a computation that is structurally within budget, the budget check in the counting semantics is redundant on the support.

theorem enforceOracle.probEvent_counting_budget_eq_enforce {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [spec.Inhabited] [spec.Fintype] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (p : α → Prop) : (probEvent (countingOracle.simulate oa 0) fun (z : α × OracleSpec.QueryCount ι) => p z.1 ∧ z.2 ≤ qb) = probEvent (Prod.fst <$> (simulateQ enforceOracle oa).run qb) p

Penalty characterization under a structural query bound: the probability of an event together with staying within budget under counting equals the event probability under enforcement.

theorem enforceOracle.probEvent_counting_budget_le_enforce {ι : Type u} {spec : OracleSpec ι} {α : Type u} [DecidableEq ι] [spec.Inhabited] [spec.Fintype] {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (p : α → Prop) : (probEvent (countingOracle.simulate oa 0) fun (z : α × OracleSpec.QueryCount ι) => p z.1 ∧ z.2 ≤ qb) ≤ probEvent (Prod.fst <$> (simulateQ enforceOracle oa).run qb) p

EasyCrypt-style penalty inequality, obtained here as an equality under the structural boundedness hypothesis.