Generating Random Seeds for Oracle Queries

This file defines generateSeed spec qc js, which produces a random QuerySeed for oracle specification spec, seeding qc j values for each oracle j ∈ js.

The definition is recursive on the list js, making it easy to prove properties by induction.

def OracleComp.generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) : List ι → ProbComp spec.QuerySeed

Generate a QuerySeed uniformly at random. For each oracle j ∈ js, generates qc j uniform random values of type spec.Range j using SampleableType.

@[simp]

theorem OracleComp.generateSeed_nil {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) : generateSeed spec qc [] = pure ∅

@[simp]

theorem OracleComp.generateSeed_cons {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (j : ι) (js : List ι) : generateSeed spec qc (j :: js) = do let xs ← replicate (qc j) ($ᵗspec.Range j) let rest ← generateSeed spec qc js pure (rest.prependValues xs)

@[simp]

theorem OracleComp.generateSeed_zero {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (js : List ι) : generateSeed spec 0 js = pure ∅

@[simp]

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

theorem OracleComp.length_eq_of_mem_support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (seed : spec.QuerySeed) (i : ι) (hseed : seed ∈ support (generateSeed spec qc js)) : (seed i).length = qc i * List.count i js

theorem OracleComp.eq_nil_of_mem_support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (seed : spec.QuerySeed) (i : ι) (hseed : seed ∈ support (generateSeed spec qc js)) (hlen0 : qc i * List.count i js = 0) : seed i = []

theorem OracleComp.ne_nil_of_mem_support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (seed : spec.QuerySeed) (i : ι) (hseed : seed ∈ support (generateSeed spec qc js)) (hlenPos : 0 < qc i * List.count i js) : seed i ≠ []

theorem OracleComp.exists_cons_of_mem_support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (seed : spec.QuerySeed) (i : ι) (hseed : seed ∈ support (generateSeed spec qc js)) (hlenPos : 0 < qc i * List.count i js) : ∃ (u : spec.Range i) (us : List (spec.Range i)), seed i = u :: us

theorem OracleComp.tail_length_of_mem_support_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (seed : spec.QuerySeed) (i : ι) (hseed : seed ∈ support (generateSeed spec qc js)) (hlenPos : 0 < qc i * List.count i js) : (seed i).tail.length = qc i * List.count i js - 1

theorem OracleComp.probOutput_pop_none_eq_zero_of_count_pos {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [spec.Fintype] [spec.Inhabited] (i : ι) (hpos : 0 < qc i * List.count i js) : Pr[=none | (fun (seed : spec.QuerySeed) => seed.pop i) <$> generateSeed spec qc js] = 0

theorem OracleComp.probOutput_pop_some_eq_probOutput_prepend {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (i : ι) (u : spec.Range i) (rest : spec.QuerySeed) : Pr[=some (u, rest) | (fun (seed : spec.QuerySeed) => seed.pop i) <$> generateSeed spec qc js] = Pr[=rest.prependValues [u] | generateSeed spec qc js]

@[simp]

theorem OracleComp.finSupport_generateSeed_ne_empty {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [DecidableEq spec.QuerySeed] : finSupport (generateSeed spec qc js) ≠ ∅

theorem OracleComp.probOutput_generateSeed {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [spec.Fintype] (seed : spec.QuerySeed) (h : seed ∈ support (generateSeed spec qc js)) : Pr[=seed | generateSeed spec qc js] = (↑(List.map (fun (j : ι) => Fintype.card (spec.Range j) ^ qc j) js).prod)⁻¹

theorem OracleComp.probOutput_generateSeed' {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [spec.Fintype] [DecidableEq spec.QuerySeed] (seed : spec.QuerySeed) (h : seed ∈ support (generateSeed spec qc js)) : Pr[=seed | generateSeed spec qc js] = 1 / ↑(finSupport (generateSeed spec qc js)).card

theorem OracleComp.evalDist_generateSeed_eq_of_countEq {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [spec.Fintype] [spec.Inhabited] (qc' : ι → ℕ) (js' : List ι) (hcount : ∀ (i : ι), qc i * List.count i js = qc' i * List.count i js') : evalDist (generateSeed spec qc js) = evalDist (generateSeed spec qc' js')

theorem OracleComp.probOutput_generateSeed_prependValues {ι : Type} [DecidableEq ι] (spec : OracleSpec ι) [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) [spec.Fintype] [spec.Inhabited] {t : ι} (u : spec.Range t) (s' : spec.QuerySeed) (hpos : 0 < qc t * List.count t js) : Pr[=s'.prependValues [u] | generateSeed spec qc js] = (↑(Fintype.card (spec.Range t)))⁻¹ * Pr[=s' | generateSeed spec (Function.update (fun (i : ι) => qc i * List.count i js) t (qc t * List.count t js - 1)) js.dedup]