Basic Constructions of Simulation Oracles #
This file defines a number of basic simulation oracles, as well as operations to combine them.
def
uniformSampleImpl
{ι : Type u_1}
{spec : OracleSpec ι}
[(i : ι) → SampleableType (spec.Range i)]
:
Simulation oracle for replacing queries with uniform random selection, using unifSpec.
The resulting computation is still identical under evalDist.
The relevant OracleSpec can usually be inferred automatically, so we leave it implicit.