Documentation

VCVio.OracleComp.SimSemantics.Constructions

Basic Constructions of Simulation Oracles #

This file defines a number of basic simulation oracles, as well as operations to combine them.

source
def QueryImpl.compose {ι : Type u_1} {spec : OracleSpec ι} {ι' : Type} {spec' : OracleSpec ι'} {m : Type u → Type v} [Monad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) :
QueryImpl spec m

Given an implementation of spec in terms of a new set of oracles spec', and an implementation of spec' in terms of arbitrary m, implement spec in terms of m.

Equations
    Instances For
      source
      def QueryImpl.«term_∘ₛ_» :
      Lean.TrailingParserDescr
      Equations
        Instances For
          source
          @[simp]
          theorem QueryImpl.apply_compose {ι : Type u_1} {spec : OracleSpec ι} {ι' : Type} {spec' : OracleSpec ι'} {m : Type u → Type v} [Monad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (t : spec.Domain) :
          (so' ∘ₛ so) t = simulateQ so' (so t)
          source
          @[simp]
          theorem QueryImpl.simulateQ_compose {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} {ι' : Type} {spec' : OracleSpec ι'} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (oa : OracleComp spec α) :
          simulateQ (so' ∘ₛ so) oa = simulateQ so' (simulateQ so oa)
          source
          def uniformSampleImpl {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] :
          QueryImpl spec ProbComp

          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.

          Equations
            Instances For
              source
              @[simp]
              theorem uniformSampleImpl.evalDist_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [(i : ι₀) → SampleableType (spec₀.Range i)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) :
              evalDist (simulateQ uniformSampleImpl oa) = evalDist oa
              source
              @[simp]
              theorem uniformSampleImpl.probOutput_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [(i : ι₀) → SampleableType (spec₀.Range i)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (x : α) :
              Pr[=x | simulateQ uniformSampleImpl oa] = Pr[=x | oa]
              source
              @[simp]
              theorem uniformSampleImpl.probEvent_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [(i : ι₀) → SampleableType (spec₀.Range i)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (p : α → Prop) :
              Pr[p | simulateQ uniformSampleImpl oa] = Pr[p | oa]
              source
              @[simp]
              theorem uniformSampleImpl.support_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [(i : ι₀) → SampleableType (spec₀.Range i)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) :
              support (simulateQ uniformSampleImpl oa) = support oa
              source
              @[simp]
              theorem uniformSampleImpl.finSupport_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [(i : ι₀) → SampleableType (spec₀.Range i)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} [DecidableEq α] (oa : OracleComp spec₀ α) :
              finSupport (simulateQ uniformSampleImpl oa) = finSupport oa