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)
:
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.
Instances For
@[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
Instances For
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)