Oracles Used by a Computation

This file defines a function OracleComp.activeOracles that returns the set of oracle indices that can possibly be called by a computation. Works by just traversing the entire possible execution space, so this really shouldn't be used in practice. However it can be useful in proving certain lemmas about existence of certain reductions.

def OracleComp.activeOracles {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.FiniteRange] [DecidableEq ι] (oa : OracleComp spec α) : Finset ι

Given that the indexing set has decidable equality, return a finite set of all the indices that can ever be used in a query by a computation, by just traversing all possible execution paths.

Equations

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