Structures For Tracking a Computation's Oracle Queries

This file defines types like QueryLog and QueryCache for use with simulation oracles and implementation transformers defined in the same directory.

def OracleSpec.QueryCache {ι : Type u} (spec : OracleSpec ι) : Type (max u v)

Type to represent a cache of queries to oracles in spec. Defined to be a function from (indexed) inputs to an optional output.

instance OracleSpec.QueryCache.instEmptyCollection {ι : Type u} {spec : OracleSpec ι} : EmptyCollection spec.QueryCache

def OracleSpec.QueryCache.cacheQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : spec.QueryCache

Add a index + input pair to the cache by updating the function (wrapper around Function.update)

@[reducible]

def OracleSpec.QueryCount (ι : Type u_1) : Type u_1

Simple wrapper in order to introduce the Monoid structure for countingOracle. Marked as reducible and can generally be treated as just a function. idx gives the "index" for a given input

instance OracleSpec.QueryCount.instMonoid {ι : Type u} : Monoid (QueryCount ι)

Pointwise addition as the Monoid operation used for WriterT.

@[simp]

theorem OracleSpec.QueryCount.monoid_mul_def {ι : Type u} (qc qc' : QueryCount ι) : qc * qc' = qc + qc'

@[simp]

theorem OracleSpec.QueryCount.monoid_one_def {ι : Type u} : OfNat.ofNat 1 = 0

def OracleSpec.QueryCount.single {ι : Type u} [DecidableEq ι] (i : ι) : QueryCount ι

@[simp]

theorem OracleSpec.QueryCount.single_le_iff_pos {ι : Type u} [DecidableEq ι] (i : ι) (qc : QueryCount ι) : single i ≤ qc ↔ 0 < qc i

@[reducible]

def OracleSpec.QueryLog {ι : Type u} (spec : OracleSpec ι) : Type (max u v)

Log of queries represented by a list of dependent product's tagging the oracle's index. (t : spec.Domain) × (spec.Range t) is slightly more restricted as it doesn't keep track of query ordering between different oracles.

def OracleSpec.QueryLog.singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : spec.QueryLog

Query log with a single entry.

def OracleSpec.QueryLog.logQuery {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (t : spec.Domain) (u : spec.Range t) : spec.QueryLog

Update a query log by adding a new element to the appropriate list. Note that this requires decidable equality on the indexing set.

instance OracleSpec.QueryLog.instDecidableEqOfDecidableEq {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] : DecidableEq spec.QueryLog

def OracleSpec.QueryLog.getQ {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : List ((t : spec.Domain) × spec.Range t)

Get all the queries with inputs satisfying p

def OracleSpec.QueryLog.countQ {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : ℕ

Count the number of queries with inputs satisfying p.

def OracleSpec.QueryLog.wasQueried {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : spec.Domain) : Bool

Check if an element was ever queried in a log of queries. Relies on decidable equality of the domain types of oracles.

def OracleSpec.QueryLog.fst {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : (spec₁ + spec₂).QueryLog) : spec₁.QueryLog

Get only the portion of the log for queries in spec₁.

def OracleSpec.QueryLog.snd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : (spec₁ + spec₂).QueryLog) : spec₂.QueryLog

Get only the portion of the log for queries in spec₂.

def OracleSpec.QueryLog.inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : spec₁.QueryLog) : (spec₁ + spec₂).QueryLog

View a log for spec₁ as one for spec₁ ++ₒ spec₂ by inclusion.

def OracleSpec.QueryLog.inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : spec₂.QueryLog) : (spec₁ + spec₂).QueryLog

View a log for spec₂ as one for spec₁ ++ₒ spec₂ by inclusion.

instance OracleSpec.QueryLog.instCoeSumHAdd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₁.QueryLog (spec₁ + spec₂).QueryLog

instance OracleSpec.QueryLog.instCoeSumHAdd_1 {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₂.QueryLog (spec₁ + spec₂).QueryLog