Pre-computing Results of Oracle Queries

This file defines a function QueryImpl.withPregen that modifies a query implementation to take in a list of pre-chosen outputs to use when answering queries.

Note that ordering is subtle, for example so.withCaching.withPregen will first check for seeds and not cache the result if one is found, while so.withPregen.withCaching checks the cache first, and include seed values into the cache after returning them.

def QueryImpl.withPregen {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) : QueryImpl spec (ReaderT spec.QuerySeed m)

Modify a QueryImpl to check for pregenerated responses for oracle queries first

Equations

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

@[simp]

theorem QueryImpl.withPregen_apply {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {m : Type u → Type v} [Monad m] {α : Type u} (so : QueryImpl spec m) (q : spec.OracleQuery α) : so.withPregen.impl q = match α, q with | .(spec.range i), OracleSpec.query i t => do let seed ← read match seed i with | u :: us => ReaderT.adapt (fun (seed : spec.QuerySeed) => seed.update i us) (pure u) | [] => liftM (so.impl (OracleSpec.query i t))

@[reducible, inline]

def seededOracle {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] : QueryImpl spec (ReaderT spec.QuerySeed (OracleComp spec))

Use pregenerated oracle responses for queries.

Equations

• seededOracle = idOracle.withPregen

theorem seededOracle.apply_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u} (q : spec.OracleQuery α) : seededOracle.impl q = match α, q with | .(spec.range i), OracleSpec.query i t => do let seed ← read match seed i with | u :: us => ReaderT.adapt (fun (seed : spec.QuerySeed) => seed.update i us) (pure u) | [] => liftM (OracleSpec.query i t)

@[simp]

theorem seededOracle.probOutput_generateSeed_bind_simulateQ_bind {ι : Type} {spec : OracleSpec ι} {α β : Type} [DecidableEq ι] [(i : ι) → OracleComp.SelectableType (spec.range i)] [unifSpec ⊂ₒ spec] [spec.FiniteRange] (qc : ι → ℕ) (js : List ι) (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : [=y|do let seed ← OracleComp.liftComp (OracleComp.generateSeed spec qc js) spec let x ← (OracleComp.simulateQ seededOracle oa).run seed ob x] = [=y|oa >>= ob]

@[simp]

theorem seededOracle.probOutput_generateSeed_bind_map_simulateQ {ι : Type} {spec : OracleSpec ι} {α β : Type} [DecidableEq ι] [(i : ι) → OracleComp.SelectableType (spec.range i)] [unifSpec ⊂ₒ spec] [spec.FiniteRange] (qc : ι → ℕ) (js : List ι) (oa : OracleComp spec α) (f : α → β) (y : β) : [=y|do let seed ← OracleComp.liftComp (OracleComp.generateSeed spec qc js) spec f <$> (OracleComp.simulateQ seededOracle oa).run seed] = [=y|f <$> oa]