Documentation

VCVio.OracleComp.QueryTracking.CountingOracle

Counting Queries Made by a Computation #

This file defines a simulation oracle countingOracle for counting the number of queries made while running the computation. The count is represented by a function from oracle indices to counts, allowing each oracle to be tracked individually.

Tracking individually is not necessary, but gives tighter security bounds in some cases. It also allows for generating things like seed values for a computation more tightly.

source
def QueryImpl.withCounting {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) :
QueryImpl spec (WriterT spec.QueryCount m)
Equations
Instances For
    source
    @[simp]
    theorem QueryImpl.withCounting_apply {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {α : Type u} (so : QueryImpl spec m) (q : spec.OracleQuery α) :
    so.withCounting.impl q = tell (OracleSpec.QueryCount.single q.index) *> liftM (so.impl q)
    source
    def countingOracle {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} :
    QueryImpl spec (WriterT spec.QueryCount (OracleComp spec))

    Oracle for counting the number of queries made by a computation. The count is stored as a function from oracle indices to counts, to give finer grained information about the count.

    Equations
    Instances For
      source
      @[simp]
      theorem countingOracle.impl_apply_eq {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (q : spec.OracleQuery α) :
      countingOracle.impl q = tell (OracleSpec.QueryCount.single q.index) *> liftM q
      source
      @[simp]
      theorem countingOracle.fst_map_run_simulateQ {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      Prod.fst <$> (OracleComp.simulateQ countingOracle oa).run = oa

      countingOracle has no effect on the behavior of the computation itself.

      source
      @[simp]
      theorem countingOracle.run_simulateQ_bind_fst {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α β : Type u} (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
      (do let x ← (OracleComp.simulateQ countingOracle oa).run ob x.1) = oa >>= ob
      source
      @[simp]
      theorem countingOracle.probFailure_run_simulateQ {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] (oa : OracleComp spec α) :
      [⊥|(OracleComp.simulateQ countingOracle oa).run] = [⊥|oa]
      source
      @[simp]
      theorem countingOracle.neverFails_run_simulateQ_iff {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      (OracleComp.simulateQ countingOracle oa).run.neverFails ↔ oa.neverFails
      source
      theorem countingOracle.neverFails_simulateQ {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      oa.neverFails → (OracleComp.simulateQ countingOracle oa).run.neverFails

      Alias of the reverse direction of countingOracle.neverFails_run_simulateQ_iff.