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.le_length_of_mem_support_generateSeed_of_covers {ι : 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)) (hcover : ∀ (j : ι), 0 < qc j → j ∈ js) : qc i ≤ (seed i).length

If the seed-generation list js contains every oracle family with positive budget, then any seed sampled by generateSeed spec qc js contains at least qc i answers for each oracle i.

This is the support-level coverage property needed by seeded replay arguments: one occurrence of i in js already contributes qc i pre-generated answers to the seed at i, and additional occurrences only increase that supply.

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') : 𝒟[generateSeed spec qc js] = 𝒟[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]

def OracleComp.SeedListCovers {ι : Type} (qb : ι → ℕ) (js : List ι) : Prop

SeedListCovers qb js means that every oracle family with positive query budget appears in the seed-generation list js.

When this holds, any seed sampled from generateSeed spec qb js supplies enough pre-generated answers to cover one full execution of a computation satisfying the structural bound qb.

theorem OracleComp.generateSeed_covers_queryBound {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(t : spec.Domain) → SampleableType (spec.Range t)] (qb : ι → ℕ) (js : List ι) {seed : spec.QuerySeed} (hjs : SeedListCovers qb js) (hseed : seed ∈ support (generateSeed spec qb js)) (t : ι) : qb t ≤ (seed t).length

Any seed sampled from generateSeed spec qb js has at least qb t entries for each oracle t, provided js lists every oracle family with positive budget.

theorem OracleComp.generateSeed_queryCostExactly {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (sampleCost : ι → ℕ) (hSample : ∀ (j : ι), (probCompUnitQueryRun ($ᵗ spec.Range j)).QueryCostExactly (sampleCost j)) : (probCompUnitQueryRun (generateSeed spec qc js)).QueryCostExactly (List.map (fun (j : ι) => qc j * sampleCost j) js).sum

theorem OracleComp.generateSeed_expectedQueryCount_eq {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(t : spec.Domain) → SampleableType (spec.Range t)] (qc : ι → ℕ) (js : List ι) (sampleCost : ι → ℕ) (hSample : ∀ (j : ι), (probCompUnitQueryRun ($ᵗ spec.Range j)).QueryCostExactly (sampleCost j)) : (probCompUnitQueryRun (generateSeed spec qc js)).expectedCostNat = ↑(List.map (fun (j : ι) => qc j * sampleCost j) js).sum

The expected number of uniform-oracle calls made by generateSeed spec qc js equals ∑ j in js, qc j * sampleCost j, i.e. each of the qc j samples at oracle j costs sampleCost j.