Documentation

VCVio.OracleComp.FinRatPMF

Executable FinRatPMF Semantics for OracleComp #

This file provides a computable oracle evaluator using FinRatPMF.Raw and proves that its denotational semantics agree with the existing evalDist semantics of OracleComp.

source
def FinRatPMF.finRatImpl {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] :
QueryImpl spec Raw

Computable query implementation using the executable FinRatPMF.Raw monad.

Instances For
    source
    @[implicit_reducible]
    def FinRatPMF.finRatImpl.instSpecFintypeOfFinEnum {ι : Type u} {spec : OracleSpec ι} [(t : spec.Domain) → FinEnum (spec.Range t)] :
    spec.Fintype
    Instances For
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.toPMF_apply {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] (t : spec.Domain) :
      (finRatImpl t).toPMF = PMF.uniformOfFintype (spec.Range t)
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.evalDist_apply {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] (t : spec.Domain) :
      evalDist (finRatImpl t) = liftM (PMF.uniformOfFintype (spec.Range t))
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.evalDist_simulateQ {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] {α : Type v} (oa : OracleComp spec α) :
      evalDist (simulateQ finRatImpl oa) = evalDist oa
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.probOutput_simulateQ {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] {α : Type v} (oa : OracleComp spec α) (x : α) :
      Pr[= x | simulateQ finRatImpl oa] = Pr[= x | oa]
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.probEvent_simulateQ {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] {α : Type v} (oa : OracleComp spec α) (p : α → Prop) :
      probEvent (simulateQ finRatImpl oa) p = probEvent oa p
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.support_simulateQ {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] {α : Type v} (oa : OracleComp spec α) :
      support (simulateQ finRatImpl oa) = support oa
      source
      @[simp]
      theorem FinRatPMF.finRatImpl.finSupport_simulateQ {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] [(t : spec.Domain) → FinEnum (spec.Range t)] {α : Type v} [DecidableEq α] (oa : OracleComp spec α) :
      finSupport (simulateQ finRatImpl oa) = finSupport oa

      Demo #

      source
      @[implicit_reducible]
      def FinRatPMF.Demo.instFinEnumBool_vCVio :
      FinEnum Bool
      Instances For
        source
        @[implicit_reducible]
        instance FinRatPMF.Demo.instFinEnumRangeUnitCoinSpec (t : coinSpec.Domain) :
        FinEnum (coinSpec.Range t)
        source
        def FinRatPMF.Demo.xorTwoCoins :
        Raw Bool
        Instances For
          source
          def FinRatPMF.Demo.threeCoinCount :
          Raw ℕ
          Instances For
            source
            def FinRatPMF.Demo.twoCoinQueries :
            OracleComp coinSpec ℕ
            Instances For