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} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {m : Type u → Type v} [AlternativeMonad 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} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type u} {m : Type u → Type v} [AlternativeMonad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (q : spec.OracleQuery α) :
          (so'∘ₛso).impl q = OracleComp.simulateQ so' (so.impl q)
          source
          @[simp]
          theorem QueryImpl.simulateQ_compose {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type u} {m : Type u → Type v} [AlternativeMonad m] [LawfulMonad m] [LawfulAlternative m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (oa : OracleComp spec α) :
          OracleComp.simulateQ (so'∘ₛso) oa = OracleComp.simulateQ so' (OracleComp.simulateQ so oa)
          source
          def QueryImpl.equivState {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) :
          QueryImpl spec (StateT τ (OracleComp spec'))

          Substitute an equivalent type for the state of a simulation oracle, by using the equivalence to move back and forth between the states as needed. This can be useful when operations such like simOracle.append add on a state of type Unit. TODO: this should really exist on the StateT level probably instead.

          Equations
            Instances For
              source
              @[simp]
              theorem QueryImpl.equivState_apply {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) (q : spec.OracleQuery α) :
              (so.equivState e).impl q = fun (s : τ) => Prod.map id ⇑e <$> so.impl q (e.symm s)
              source
              @[simp]
              theorem QueryImpl.equivState_subsingleton {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) [Subsingleton σ] (e : σ ≃ σ) :
              so.equivState e = so

              Masking a Subsingleton state has no effect, since the new state elements look the same.

              source
              @[simp]
              theorem QueryImpl.equivState_equivState {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) :
              (so.equivState e).equivState e.symm = so
              source
              def unifOracle {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (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 unifOracle.apply_eq {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} (q : spec.OracleQuery α) :
                  unifOracle.impl q = match α, q with | .(spec.range i), OracleSpec.query i t => $ᵗspec.range i
                  source
                  @[simp]
                  theorem unifOracle.evalDist_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) :
                  (OracleComp.simulateQ unifOracle oa).evalDist = oa.evalDist
                  source
                  @[simp]
                  theorem unifOracle.support_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} (oa : OracleComp spec α) :
                  OracleComp.support (OracleComp.simulateQ unifOracle oa) = oa.support
                  source
                  @[simp]
                  theorem unifOracle.finSupport_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) :
                  OracleComp.finSupport (OracleComp.simulateQ unifOracle oa) = oa.finSupport
                  source
                  @[simp]
                  theorem unifOracle.probOutput_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) :
                  [=x|OracleComp.simulateQ unifOracle oa] = [=x|oa]
                  source
                  @[simp]
                  theorem unifOracle.probEvent_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
                  [p|OracleComp.simulateQ unifOracle oa] = [p|oa]