Counting Queries Made by a Computation

This file defines a simulation oracle countingOracle spec for counting the number of queries made while running the computation. The count is represented by a type queryCount spec, which

def OracleComp.generateSeedT {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) (activeOracles : List ι) : StateT spec.QuerySeed ProbComp Unit

Equations

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

def OracleComp.generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) (js : List ι) : ProbComp spec.QuerySeed

Generate a QuerySeed uniformly at random for some set of oracles spec : OracleSpec ι, with qc i : ℕ values seeded for each index i ∈ js. Note that js is allowed to contain duplicates, but usually wouldn't in practice.

Equations

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

def OracleComp.generateSingleSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) (i : ι) [SelectableType (spec.range i)] (n : ℕ) : ProbComp spec.QuerySeed

Equations

• OracleComp.generateSingleSeed spec i n = OracleSpec.QuerySeed.ofList <$> OracleComp.replicate n ($ᵗspec.range i)

@[simp]

theorem OracleComp.generateSeed_nil {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) : generateSeed spec qc [] = pure ∅

@[simp]

theorem OracleComp.generateSeed_cons {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) (j : ι) (js : List ι) : generateSeed spec qc (j :: js) = do let _ ← replicate (qc j) ($ᵗspec.range j) generateSeed spec qc js

@[simp]

theorem OracleComp.generateSeed_zero {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (js : List ι) : generateSeed spec 0 js = pure ∅

@[simp]

theorem OracleComp.support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) (js : List ι) : support (generateSeed spec qc js) = {seed : spec.QuerySeed | ∀ (i : ι), (seed i).length = qc i * List.count i js}

theorem OracleComp.probOutput_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(i : ι) → SelectableType (spec.range i)] (qc : ι → ℕ) (js : List ι) [spec.FiniteRange] (seed : spec.QuerySeed) (h : seed ∈ support (generateSeed spec qc js)) : [=seed|generateSeed spec qc js] = 1 / ↑(List.map (fun (j : ι) => Fintype.card (spec.range j) ^ qc j) js).prod