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 u

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

Equations

• spec.QueryCache = ((i : ι) → spec.domain i → Option (spec.range i))

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

Equations

• OracleSpec.QueryCache.instEmptyCollection = { emptyCollection := fun (x : ι) (x_1 : spec.domain x) => none }

def OracleSpec.QueryCache.cacheQuery {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] [DecidableEq ι] (cache : spec.QueryCache) (i : ι) (t : spec.domain i) (u : spec.range i) : spec.QueryCache

Add a index + input pair to the cache by updating the function

Equations

• cache.cacheQuery i t u = Function.update cache i (Function.update (cache i) t (some u))

theorem OracleSpec.QueryCache.cacheQuery_eq_ite_ite {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] [DecidableEq ι] (cache : spec.QueryCache) (i : ι) (t : spec.domain i) (u : spec.range i) : cache.cacheQuery i t u = fun (j : ι) (t' : spec.domain j) => if h : j = i then if h ▸ t' = t then some (⋯ ▸ u) else cache j t' else cache j t'

@[reducible]

def OracleSpec.QueryCount {ι : Type u} (_spec : OracleSpec ι) : Type u

Simple wrapper in order to introduce the Monoid structure for countingOracle. Marked as reducible and can generally be treated as just a function.

Equations

• _spec.QueryCount = (ι → ℕ)

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

Pointwise addition as the Monoid operation used for WriterT.

Equations

• OracleSpec.QueryCount.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

@[simp]

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

@[simp]

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

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

Equations

• OracleSpec.QueryCount.single i = Function.update 0 i 1

@[simp]

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

@[reducible]

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

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

Equations

• spec.QueryLog = List ((i : ι) × spec.domain i × spec.range i)

instance OracleSpec.QueryLog.instAppend {ι : Type u} {spec : OracleSpec ι} : Append spec.QueryLog

Equations

• OracleSpec.QueryLog.instAppend = { append := List.append }

instance OracleSpec.QueryLog.instMonoid {ι : Type u} {spec : OracleSpec ι} : Monoid spec.QueryLog

Dummy Monoid instance to be used with WriterT, actual calls should use append.

Equations

• OracleSpec.QueryLog.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

@[simp]

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

@[simp]

theorem OracleSpec.QueryLog.monoid_one_def {ι : Type u} {spec : OracleSpec ι} : 1 = []

def OracleSpec.QueryLog.singleton {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (q : spec.OracleQuery α) (u : α) : spec.QueryLog

Query log with a single entry.

Equations

• OracleSpec.QueryLog.singleton (OracleSpec.query i t) u_2 = [⟨i, (t, u_2)⟩]

def OracleSpec.QueryLog.logQuery {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (log : spec.QueryLog) (q : spec.OracleQuery α) (u : α) : 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.

Equations

• log.logQuery q u = log ++ OracleSpec.QueryLog.singleton q u

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

Equations

• OracleSpec.QueryLog.instDecidableEqOfDecidableEq = inferInstanceAs (DecidableEq (List ((i : ι) × spec.domain i × spec.range i)))

def OracleSpec.QueryLog.getQ {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (i : ι) : List (spec.domain i × spec.range i)

Get all the queries made to oracle i.

Equations

• One or more equations did not get rendered due to their size.

theorem OracleSpec.QueryLog.getQ_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u_1} (q : spec.OracleQuery α) (u : α) (i : ι) : (singleton q u).getQ i = match α, q, u with | .(spec.range j), query j t, u => if h : j = i then [h ▸ (t, u)] else []

@[simp]

theorem OracleSpec.QueryLog.getQ_singleton_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (i : ι) (t : spec.domain i) (u : spec.range i) : (singleton (query i t) u).getQ i = [(t, u)]

theorem OracleSpec.QueryLog.getQ_singleton_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u_1} {q : spec.OracleQuery α} {u : α} {i : ι} (h : q.index ≠ i) : (singleton q u).getQ i = []

@[simp]

theorem OracleSpec.QueryLog.getQ_cons {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (q : (i : ι) × spec.domain i × spec.range i) (i : ι) : getQ (q :: log) i = if h : q.fst = i then h ▸ (q.snd.1, q.snd.2) :: log.getQ i else log.getQ i

@[simp]

theorem OracleSpec.QueryLog.getQ_append {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log log' : spec.QueryLog) (i : ι) : (log ++ log').getQ i = log.getQ i ++ log'.getQ i

@[simp]

theorem OracleSpec.QueryLog.getQ_logQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u_1} (log : spec.QueryLog) (q : spec.OracleQuery α) (u : α) (i : ι) : (log.logQuery q u).getQ i = log.getQ i ++ (singleton q u).getQ i

def OracleSpec.QueryLog.countQ {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (i : ι) : ℕ

Equations

• log.countQ i = (log.getQ i).length

@[simp]

theorem OracleSpec.QueryLog.countQ_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u_1} (q : spec.OracleQuery α) (u : α) (i : ι) : (singleton q u).countQ i = if q.index = i then 1 else 0

theorem OracleSpec.QueryLog.countQ_singleton_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (i : ι) (t : spec.domain i) (u : spec.range i) : (singleton (query i t) u).countQ i = 1

@[simp]

theorem OracleSpec.QueryLog.countQ_append {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log log' : spec.QueryLog) (i : ι) : (log ++ log').countQ i = log.countQ i + log'.countQ i

@[simp]

theorem OracleSpec.QueryLog.countQ_logQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {α : Type u_1} (log : spec.QueryLog) (q : spec.OracleQuery α) (u : α) (i : ι) : (log.logQuery q u).countQ i = log.countQ i + if q.index = i then 1 else 0

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

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

Equations

• One or more equations did not get rendered due to their size.

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₁.

Equations

• One or more equations did not get rendered due to their size.

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₂.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• log.inl = List.map (fun (x : (i : ι₁) × spec₁.domain i × spec₁.range i) => match x with | ⟨i, (t, u)⟩ => ⟨Sum.inl i, (t, u)⟩) log

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.

Equations

• log.inr = List.map (fun (x : (i : ι₂) × spec₂.domain i × spec₂.range i) => match x with | ⟨i, (t, u)⟩ => ⟨Sum.inr i, (t, u)⟩) log

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

Equations

• OracleSpec.QueryLog.instCoeSumAppend = { coe := OracleSpec.QueryLog.inl }

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

Equations

• OracleSpec.QueryLog.instCoeSumAppend_1 = { coe := OracleSpec.QueryLog.inr }

def OracleSpec.QuerySeed {ι : Type u} (spec : OracleSpec ι) : Type u

Type to represent a store of seed values to use in a computation, represented as a function. Updates to individual seed lists are performed via continuation passing.

Equations

• spec.QuerySeed = ((i : ι) → List (spec.range i))

instance OracleSpec.QuerySeed.instDFunLikeListRange {ι : Type u} {spec : OracleSpec ι} : DFunLike spec.QuerySeed ι fun (i : ι) => List (spec.range i)

Equations

• OracleSpec.QuerySeed.instDFunLikeListRange = { coe := fun (seed : spec.QuerySeed) => seed, coe_injective' := ⋯ }

theorem OracleSpec.QuerySeed.ext {ι : Type u} {spec : OracleSpec ι} (seed₁ seed₂ : spec.QuerySeed) (h : ∀ (i : ι), seed₁ i = seed₂ i) : seed₁ = seed₂

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

Equations

• OracleSpec.QuerySeed.instEmptyCollection = { emptyCollection := fun (x : ι) => [] }

def OracleSpec.QuerySeed.update {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.range i)) : spec.QuerySeed

Equations

• seed.update i xs = Function.update seed i xs

def OracleSpec.QuerySeed.addValues {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (us : List (spec.range i)) (seed : spec.QuerySeed) : spec.QuerySeed

Add a list of values to the query seed.

Equations

• OracleSpec.QuerySeed.addValues us seed = Function.update seed i (seed i ++ us)

@[simp]

theorem OracleSpec.QuerySeed.addValues_apply {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (seed : spec.QuerySeed) (us : List (spec.range i)) (j : ι) : addValues us seed j = Function.update seed i (seed i ++ us) j

@[simp]

theorem OracleSpec.QuerySeed.addValues_nil {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (seed : spec.QuerySeed) : addValues [] seed = seed

@[reducible, inline]

abbrev OracleSpec.QuerySeed.addValue {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.range i) : spec.QuerySeed

Add a single value into the seed, by adding a singleton list

Equations

• seed.addValue i u = OracleSpec.QuerySeed.addValues [u] seed

def OracleSpec.QuerySeed.takeAtIndex {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : spec.QuerySeed

Take only the first n values of the seed at index i.

Equations

• seed.takeAtIndex i n = Function.update seed i (List.take n (seed i))

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_apply {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) (j : ι) : seed.takeAtIndex i n j = Function.update seed i (List.take n (seed i)) j

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_addValues {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (n : ℕ) (xs : List (spec.range i)) : (addValues xs seed).takeAtIndex i n = if n ≤ (seed i).length then seed.takeAtIndex i n else addValues (List.take (n - (seed i).length) xs) seed

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_length {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.takeAtIndex i (seed i).length = seed

theorem OracleSpec.QuerySeed.eq_takeAtIndex_length_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) (i : ι) : seed = seed'.takeAtIndex i (seed i).length ↔ seed' = addValues (List.drop (seed i).length (seed' i)) seed

def OracleSpec.QuerySeed.ofList {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (xs : List (spec.range i)) : spec.QuerySeed

Equations

• OracleSpec.QuerySeed.ofList xs j = if h : i = j then h ▸ xs else []

theorem OracleSpec.QuerySeed.eq_addValues_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.range i)) : seed = addValues xs seed' ↔ seed' = seed.takeAtIndex i (seed' i).length ∧ xs = List.drop (seed' i).length (seed i)

theorem OracleSpec.QuerySeed.addValues_eq_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.range i)) : addValues xs seed = seed' ↔ seed = seed'.takeAtIndex i (seed i).length ∧ xs = List.drop (seed i).length (seed' i)