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.

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

A partial dependent answer table, ordered by extension of cached responses.

• toFn (t : spec.Domain) : Option (spec.Range t)

  Look up the response stored at an oracle index.

@[instance_reducible]

instance OracleSpec.QueryCache.instCoeFunForallOptionRange {ι : Type u} {spec : OracleSpec ι} : CoeFun spec.QueryCache fun (x : spec.QueryCache) => (t : spec.Domain) → Option (spec.Range t)

def OracleSpec.QueryCache.ofFn {ι : Type u} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) : spec.QueryCache

Package a partial dependent answer function as a cache.

@[simp]

theorem OracleSpec.QueryCache.ofFn_apply {ι : Type u} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) (t : spec.Domain) : (ofFn f).toFn t = f t

@[simp]

theorem OracleSpec.QueryCache.toFn_ofFn {ι : Type u} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) : (ofFn f).toFn = f

@[simp]

theorem OracleSpec.QueryCache.ofFn_toFn {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) : ofFn cache.toFn = cache

@[instance_reducible]

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

@[simp]

theorem OracleSpec.QueryCache.empty_apply {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : ∅.toFn t = none

theorem OracleSpec.QueryCache.ext {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} (h : ∀ (t : spec.Domain), c₁.toFn t = c₂.toFn t) : c₁ = c₂

theorem OracleSpec.QueryCache.ext_iff {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} : c₁ = c₂ ↔ ∀ (t : spec.Domain), c₁.toFn t = c₂.toFn t

theorem OracleSpec.QueryCache.toFn_injective {ι : Type u} {spec : OracleSpec ι} : Function.Injective toFn

Cache lookup is injective.

def OracleSpec.QueryCache.equivFn {ι : Type u} {spec : OracleSpec ι} : spec.QueryCache ≃ ((t : spec.Domain) → Option (spec.Range t))

A cache and its dependent optional lookup table contain the same data.

@[instance_reducible]

instance OracleSpec.QueryCache.instInhabited {ι : Type u} {spec : OracleSpec ι} : Inhabited spec.QueryCache

@[instance_reducible]

instance OracleSpec.QueryCache.instDecidableEqOfForallOptionRange {ι : Type u} {spec : OracleSpec ι} [DecidableEq ((t : spec.Domain) → Option (spec.Range t))] : DecidableEq spec.QueryCache

instance OracleSpec.QueryCache.instCountableOfForallOptionRange {ι : Type u} {spec : OracleSpec ι} [Countable ((t : spec.Domain) → Option (spec.Range t))] : Countable spec.QueryCache

instance OracleSpec.QueryCache.instFiniteOfForallOptionRange {ι : Type u} {spec : OracleSpec ι} [Finite ((t : spec.Domain) → Option (spec.Range t))] : Finite spec.QueryCache

@[instance_reducible]

instance OracleSpec.QueryCache.instFintypeOfForallOptionRange {ι : Type u} {spec : OracleSpec ι} [Fintype ((t : spec.Domain) → Option (spec.Range t))] : Fintype spec.QueryCache

Agreement with answer functions

def OracleSpec.QueryCache.AgreesWithFn {ι : Type u} {spec : OracleSpec ι} (f : QueryImpl spec Id) (cache : spec.QueryCache) : Prop

A total answer function agrees with a cache if it returns every cached response.

theorem OracleSpec.QueryCache.exists_agreesWithFn {ι : Type u} {spec : OracleSpec ι} [∀ (t : ι), Nonempty (spec.Range t)] (cache : spec.QueryCache) : ∃ (f : QueryImpl spec Id), AgreesWithFn f cache

Every cache is extended by some total answer function.

Partial Order

A QueryCache carries a natural partial order where c₁ ≤ c₂ means every cached entry in c₁ also appears (with the same value) in c₂. The empty cache is the bottom element.

@[instance_reducible]

instance OracleSpec.QueryCache.instPartialOrder {ι : Type u} {spec : OracleSpec ι} : PartialOrder spec.QueryCache

@[instance_reducible]

instance OracleSpec.QueryCache.instOrderBot {ι : Type u} {spec : OracleSpec ι} : OrderBot spec.QueryCache

@[simp]

theorem OracleSpec.QueryCache.bot_eq_empty {ι : Type u} {spec : OracleSpec ι} : ⊥ = ∅

theorem OracleSpec.QueryCache.le_def {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} : c₁ ≤ c₂ ↔ ∀ ⦃t : ι⦄ ⦃u : spec.Range t⦄, c₁.toFn t = some u → c₂.toFn t = some u

Query membership

def OracleSpec.QueryCache.isCached {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) (t : spec.Domain) : Bool

Check whether a query t has a cached response.

@[simp]

theorem OracleSpec.QueryCache.isCached_empty {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : ∅.isCached t = false

Conversion to a set of query-response pairs

def OracleSpec.QueryCache.toSet {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) : Set ((t : spec.Domain) × spec.Range t)

The set of all (query, response) pairs stored in the cache.

@[simp]

theorem OracleSpec.QueryCache.mem_toSet {ι : Type u} {spec : OracleSpec ι} {cache : spec.QueryCache} {t : spec.Domain} {r : spec.Range t} : ⟨t, r⟩ ∈ cache.toSet ↔ cache.toFn t = some r

@[simp]

theorem OracleSpec.QueryCache.toSet_empty {ι : Type u} {spec : OracleSpec ι} : ∅.toSet = ∅

theorem OracleSpec.QueryCache.toSet_mono {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} (h : c₁ ≤ c₂) : c₁.toSet ⊆ c₂.toSet

noncomputable def OracleSpec.QueryCache.enncard {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) : ENNReal

Number of live entries in a query cache, as an ℝ≥0∞ resource.

@[simp]

theorem OracleSpec.QueryCache.enncard_empty {ι : Type u} {spec : OracleSpec ι} : ∅.enncard = 0

Cache update

theorem OracleSpec.QueryCache.functionUpdate_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : Function.update cache.toFn t (some u) t = some u

theorem OracleSpec.QueryCache.functionUpdate_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t' t : spec.Domain} (u : spec.Range t) (h : t' ≠ t) : Function.update cache.toFn t (some u) t' = cache.toFn t'

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

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

@[simp]

theorem OracleSpec.QueryCache.cacheQuery_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).toFn t = some u

@[simp]

theorem OracleSpec.QueryCache.cacheQuery_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t' t : spec.Domain} (u : spec.Range t) (h : t' ≠ t) : (cache.cacheQuery t u).toFn t' = cache.toFn t'

theorem OracleSpec.QueryCache.agreesWithFn_cacheQuery_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) (f : QueryImpl spec Id) (hcache : cache.toFn t = none) : AgreesWithFn f (cache.cacheQuery t u) ↔ AgreesWithFn f cache ∧ f t = u

An answer function agrees with cache.cacheQuery t u iff it agrees with cache and returns u on t, provided t was not already cached.

theorem OracleSpec.QueryCache.toSet_cacheQuery_subset_insert {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).toSet ⊆ insert ⟨t, u⟩ cache.toSet

theorem OracleSpec.QueryCache.toSet_encard_cacheQuery_le {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).toSet.encard ≤ cache.toSet.encard + 1

theorem OracleSpec.QueryCache.enncard_cacheQuery_le {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).enncard ≤ cache.enncard + 1

theorem OracleSpec.QueryCache.le_cacheQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t : spec.Domain} {u : spec.Range t} (h : cache.toFn t = none) : cache ≤ cache.cacheQuery t u

theorem OracleSpec.QueryCache.cacheQuery_mono {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {c₁ c₂ : spec.QueryCache} (h : c₁ ≤ c₂) (t : spec.Domain) (u : spec.Range t) : c₁.cacheQuery t u ≤ c₂.cacheQuery t u

@[simp]

theorem OracleSpec.QueryCache.isCached_cacheQuery_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).isCached t = true

@[simp]

theorem OracleSpec.QueryCache.isCached_cacheQuery_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t' t : spec.Domain} (u : spec.Range t) (h : t' ≠ t) : (cache.cacheQuery t u).isCached t' = cache.isCached t'

Sum spec projections

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

Project a cache for spec₁ + spec₂ onto spec₁.

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

Project a cache for spec₁ + spec₂ onto spec₂.

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

Embed a cache for spec₁ into one for spec₁ + spec₂.

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

Embed a cache for spec₂ into one for spec₁ + spec₂.

@[simp]

theorem OracleSpec.QueryCache.fst_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) (t : ι₁) : cache.fst.toFn t = cache.toFn (Sum.inl t)

@[simp]

theorem OracleSpec.QueryCache.snd_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) (t : ι₂) : cache.snd.toFn t = cache.toFn (Sum.inr t)

@[simp]

theorem OracleSpec.QueryCache.inl_apply_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) (t : ι₁) : cache.inl.toFn (Sum.inl t) = cache.toFn t

@[simp]

theorem OracleSpec.QueryCache.inl_apply_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) (t : ι₂) : cache.inl.toFn (Sum.inr t) = none

@[simp]

theorem OracleSpec.QueryCache.inr_apply_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) (t : ι₁) : cache.inr.toFn (Sum.inl t) = none

@[simp]

theorem OracleSpec.QueryCache.inr_apply_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) (t : ι₂) : cache.inr.toFn (Sum.inr t) = cache.toFn t

@[simp]

theorem OracleSpec.QueryCache.fst_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) : cache.inl.fst = cache

@[simp]

theorem OracleSpec.QueryCache.snd_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) : cache.inr.snd = cache

@[simp]

theorem OracleSpec.QueryCache.fst_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) : cache.inr.fst = ∅

@[simp]

theorem OracleSpec.QueryCache.snd_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) : cache.inl.snd = ∅

@[simp]

theorem OracleSpec.QueryCache.inl_cacheQuery {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [DecidableEq ι₁] [DecidableEq ι₂] (cache : spec₁.QueryCache) (t : spec₁.Domain) (u : spec₁.Range t) : (cache.cacheQuery t u).inl = cache.inl.cacheQuery (Sum.inl t) u

Embedding a left-component cache commutes with caching a left-component query.

@[simp]

theorem OracleSpec.QueryCache.inr_cacheQuery {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [DecidableEq ι₁] [DecidableEq ι₂] (cache : spec₂.QueryCache) (t : spec₂.Domain) (u : spec₂.Range t) : (cache.cacheQuery t u).inr = cache.inr.cacheQuery (Sum.inr t) u

Embedding a right-component cache commutes with caching a right-component query.

@[simp]

theorem OracleSpec.QueryCache.fst_empty {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : ∅.fst = ∅

@[simp]

theorem OracleSpec.QueryCache.snd_empty {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : ∅.snd = ∅

@[instance_reducible]

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

@[instance_reducible]

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

@[reducible]

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

Per-index natural counts with the ordinary pointwise additive algebra. Additive writer instrumentation uses Multiplicative (QueryCount ι) as its monoidal payload; query counts themselves retain the standard function instances.

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

The query count recording one query at index i and none elsewhere.

@[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.

A QueryLog spec is morally a free monoid on Idx spec.toPFunctor, with identity [] and product (++). By Mathlib reducibility this is exactly FreeMonoid (Idx spec.toPFunctor) = TraceList spec.toPFunctor, so a trace-valued boundary description such as BoundaryAction.emit (in PolyFun/Interaction/UC/OpenProcess.lean) and a per-call QueryLog-valued writer share the same underlying free-monoid carrier.

We do not declare a global Monoid (QueryLog spec) instance: doing so would conflict with the [EmptyCollection ω] [Append ω] → Monad (WriterT ω M) instance Mathlib already provides for WriterT (QueryLog spec) M, which the existing WriterTBridge/mvcgen proof infrastructure relies on. The QueryImpl.withTrace/withLogging API instead uses the Append-based Monad (WriterT _ _) directly via QueryImpl.withTraceAppend.

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_reducible]

instance OracleSpec.QueryLog.instDecidableEqOfRange {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [(t : ι) → DecidableEq (spec.Range t)] : 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

@[simp]

theorem OracleSpec.QueryLog.getQ_nil {ι : Type u} {spec : OracleSpec ι} (p : spec.Domain → Prop) [DecidablePred p] : getQ [] p = []

@[simp]

theorem OracleSpec.QueryLog.getQ_cons {ι : Type u} {spec : OracleSpec ι} (entry : (t : spec.Domain) × spec.Range t) (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : getQ (entry :: log) p = if p entry.fst then entry :: log.getQ p else log.getQ p

@[simp]

theorem OracleSpec.QueryLog.getQ_singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) (p : spec.Domain → Prop) [DecidablePred p] : (singleton t u).getQ p = if p t then [⟨t, u⟩] else []

@[simp]

theorem OracleSpec.QueryLog.getQ_append {ι : Type u} {spec : OracleSpec ι} (log log' : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : (log ++ log').getQ p = log.getQ p ++ log'.getQ 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.

@[simp]

theorem OracleSpec.QueryLog.countQ_cons {ι : Type u} {spec : OracleSpec ι} (entry : (t : spec.Domain) × spec.Range t) (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : countQ (entry :: log) p = if p entry.fst then log.countQ p + 1 else log.countQ p

@[simp]

theorem OracleSpec.QueryLog.countQ_singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) (p : spec.Domain → Prop) [DecidablePred p] : (singleton t u).countQ p = if p t then 1 else 0

@[simp]

theorem OracleSpec.QueryLog.countQ_append {ι : Type u} {spec : OracleSpec ι} (log log' : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : (log ++ log').countQ p = log.countQ p + log'.countQ p

Lookup by oracle occurrence

def OracleSpec.QueryLog.getQueryValue? {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) (n : ℕ) : Option (spec.Range t)

The n-th answer in the log for queries to oracle t, if it exists.

theorem OracleSpec.QueryLog.getQ_logQuery {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (t : ι) (u : spec.Range t) (p : ι → Prop) [DecidablePred p] : (log.logQuery t u).getQ p = log.getQ p ++ if p t then [⟨t, u⟩] else []

Decompose getQ across a logQuery step.

theorem OracleSpec.QueryLog.getQ_getElem?_eq_of_getQueryValue?_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) (n : ℕ) (u : spec.Range t) (h : log.getQueryValue? t n = some u) : (log.getQ fun (x : spec.Domain) => x = t)[n]? = some ⟨t, u⟩

If getQueryValue? log t n = some u, then the n-th t-filtered entry of log is ⟨t, u⟩.

theorem OracleSpec.QueryLog.getQueryValue?_eq_some_of_getQ_getElem? {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) (n : ℕ) (u : spec.Range t) (h : (log.getQ fun (x : spec.Domain) => x = t)[n]? = some ⟨t, u⟩) : log.getQueryValue? t n = some u

Converse: if the n-th t-filtered entry is ⟨t, u⟩, then getQueryValue? log t n = some u.

theorem OracleSpec.QueryLog.getQ_eq_mem {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) {entry : (t' : ι) × spec.Range t'} (h : entry ∈ log.getQ fun (x : spec.Domain) => x = t) : entry.fst = t

Every entry of log.getQ (· = t) has its first component equal to t.

theorem OracleSpec.QueryLog.getQueryValue?_isSome_of_lt {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) (n : ℕ) (h : n < (log.getQ fun (x : spec.Domain) => x = t).length) : (log.getQueryValue? t n).isSome = true

If the t-filtered log has at least n + 1 entries, then the indexed lookup succeeds.

theorem OracleSpec.QueryLog.getQueryValue?_cons_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (entry : (t' : ι) × spec.Range t') (log : spec.QueryLog) (t : ι) (n : ℕ) (h : entry.fst ≠ t) : getQueryValue? (entry :: log) t n = log.getQueryValue? t n

Prepending an entry whose oracle index does not match t leaves the t-indexed view of the log unchanged.

@[simp]

theorem OracleSpec.QueryLog.getQueryValue?_cons_self_zero {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (t : ι) (u : spec.Range t) (log : spec.QueryLog) : getQueryValue? (⟨t, u⟩ :: log) t 0 = some u

The first matching entry is the zeroth indexed query value.

@[simp]

theorem OracleSpec.QueryLog.getQueryValue?_cons_self_succ {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (t : ι) (u : spec.Range t) (log : spec.QueryLog) (n : ℕ) : getQueryValue? (⟨t, u⟩ :: log) t (n + 1) = log.getQueryValue? t n

Prepending a matching entry shifts later indexed lookups by one.

theorem OracleSpec.QueryLog.getQueryValue?_append_self_at_countQ {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (before after : spec.QueryLog) (t : ι) (u : spec.Range t) : (before ++ ⟨t, u⟩ :: after).getQueryValue? t (before.countQ fun (x : spec.Domain) => x = t) = some u

The entry immediately following a prefix is found at the prefix's count of matching oracle queries.

theorem OracleSpec.QueryLog.countQ_eq_occurrences {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) : (log.countQ fun (x : spec.Domain) => x = t) = PFunctor.TraceList.occurrences t (have this := log; this)

Query-log counting is the OracleSpec specialization of PolyFun's generic occurrence count on erased polynomial traces.

theorem OracleSpec.QueryLog.getQueryValue?_eq_getAt? {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : ι) (n : ℕ) : log.getQueryValue? t n = (have this := log; this).getAt? t n

Query-log lookup is the OracleSpec specialization of dependent lookup on PolyFun traces.

def OracleSpec.QueryLog.wasQueried {ι : Type u} {spec : OracleSpec ι} [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.

theorem OracleSpec.QueryLog.getQ_ne_nil_iff_mem_map_fst {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : spec.Domain) : (log.getQ fun (x : spec.Domain) => x = t) ≠ [] ↔ t ∈ List.map (fun (e : (t : spec.Domain) × spec.Range t) => e.fst) log

theorem OracleSpec.QueryLog.wasQueried_eq_decide_mem_map_fst {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (log : spec.QueryLog) (t : spec.Domain) : log.wasQueried t = decide (t ∈ List.map (fun (e : (t : spec.Domain) × spec.Range t) => e.fst) log)

@[simp]

theorem OracleSpec.QueryLog.wasQueried_cons_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {t : spec.Domain} {u : spec.Range t} {log : spec.QueryLog} : wasQueried (⟨t, u⟩ :: log) t = true

@[simp]

theorem OracleSpec.QueryLog.wasQueried_cons_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {t t' : spec.Domain} {u : spec.Range t'} {log : spec.QueryLog} (hne : t' ≠ t) : wasQueried (⟨t', u⟩ :: log) t = log.wasQueried t

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_reducible]

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

@[instance_reducible]

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

@[reducible]

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

A store of pre-generated seed values for oracle queries, indexed by oracle. Maps each oracle index i to a list of outputs List (spec.Range i).

@[instance_reducible]

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

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

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

@[simp]

theorem OracleSpec.QuerySeed.empty_apply {ι : Type u} {spec : OracleSpec ι} (i : ι) : ∅ i = []

theorem OracleSpec.QuerySeed.functionUpdate_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) : Function.update seed i xs i = xs

theorem OracleSpec.QuerySeed.functionUpdate_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) (j : ι) (hj : j ≠ i) : Function.update seed i xs j = seed j

theorem OracleSpec.QuerySeed.functionUpdate_eq_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : Function.update seed i (seed i) = seed

theorem OracleSpec.QuerySeed.functionUpdate_idem {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs ys : List (spec.Range i)) : Function.update (Function.update seed i xs) i ys = Function.update seed i ys

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

Replace the seed values at index i.

@[simp]

theorem OracleSpec.QuerySeed.update_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) : seed.update i xs i = xs

@[simp]

theorem OracleSpec.QuerySeed.update_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) (j : ι) (hj : j ≠ i) : seed.update i xs j = seed j

@[simp]

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

@[simp]

theorem OracleSpec.QuerySeed.update_idem {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs ys : List (spec.Range i)) : (seed.update i xs).update i ys = seed.update i ys

theorem OracleSpec.QuerySeed.update_comm {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i j : ι} (h : i ≠ j) (xs : List (spec.Range i)) (ys : List (spec.Range j)) : (seed.update i xs).update j ys = (seed.update j ys).update i xs

Updates at distinct seed indices commute.

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

Append a list of values to the seed at index i.

@[simp]

theorem OracleSpec.QuerySeed.update_addValues_same {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (us xs : List (spec.Range i)) : (seed.addValues us).update i xs = seed.update i xs

Replacing an index after appending there discards the appended values.

theorem OracleSpec.QuerySeed.update_addValues_comm {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i j : ι} (h : i ≠ j) (us : List (spec.Range i)) (ys : List (spec.Range j)) : (seed.addValues us).update j ys = (seed.update j ys).addValues us

Appending at one seed index commutes with replacing a distinct index.

@[simp]

theorem OracleSpec.QuerySeed.addValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : seed.addValues us i = seed i ++ us

@[simp]

theorem OracleSpec.QuerySeed.addValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) {j : ι} (hj : j ≠ i) : seed.addValues us j = seed j

@[simp]

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

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

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

Prepend a list of values to the seed at index i.

@[simp]

theorem OracleSpec.QuerySeed.prependValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : seed.prependValues us i = us ++ seed i

theorem OracleSpec.QuerySeed.prependValues_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (u : spec.Range i) : seed.prependValues [u] i = u :: seed i

@[simp]

theorem OracleSpec.QuerySeed.prependValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) {j : ι} (hj : j ≠ i) : seed.prependValues us j = seed j

@[simp]

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

theorem OracleSpec.QuerySeed.prependValues_take_drop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : (seed.update i (List.drop n (seed i))).prependValues (List.take n (seed i)) = seed

theorem OracleSpec.QuerySeed.eq_of_prependValues_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed rest : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) {n : ℕ} (hlen : xs.length = n) (h : rest.prependValues xs = seed) : xs = List.take n (seed i) ∧ rest = seed.update i (List.drop n (seed i))

theorem OracleSpec.QuerySeed.eq_of_prependValues_singleton_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed rest : spec.QuerySeed) {i : ι} (u : spec.Range i) (h : rest.prependValues [u] = seed) : u :: rest i = seed i ∧ rest = seed.update i (seed i).tail

@[reducible, inline]

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

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.

@[simp]

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

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_apply_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) (j : ι) (hj : j ≠ i) : seed.takeAtIndex i n j = seed j

@[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.takeAtIndex_addValues_drop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : (seed.takeAtIndex i n).addValues (List.drop n (seed i)) = seed

def OracleSpec.QuerySeed.pop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : Option (spec.Range i × spec.QuerySeed)

Pop one value from index i, returning the consumed value and updated seed when nonempty.

@[simp]

theorem OracleSpec.QuerySeed.pop_eq_none_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.pop i = none ↔ seed i = []

theorem OracleSpec.QuerySeed.pop_eq_some_of_cons {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (us : List (spec.Range i)) (h : seed i = u :: us) : seed.pop i = some (u, seed.update i us)

theorem OracleSpec.QuerySeed.cons_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (rest : spec.QuerySeed) (h : seed.pop i = some (u, rest)) : u :: rest i = seed i

theorem OracleSpec.QuerySeed.rest_eq_update_tail_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (rest : spec.QuerySeed) (h : seed.pop i = some (u, rest)) : rest = seed.update i (seed i).tail

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

Construct a query seed from a list at a single index.

@[simp]

theorem OracleSpec.QuerySeed.ofList_apply_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (xs : List (spec.Range i)) : ofList xs i = xs

@[simp]

theorem OracleSpec.QuerySeed.ofList_apply_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i j : ι} (xs : List (spec.Range i)) (hj : j ≠ i) : ofList xs j = []

theorem OracleSpec.QuerySeed.eq_addValues_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) : seed = seed'.addValues xs ↔ seed' i ++ xs = seed i ∧ ∀ (j : ι), j ≠ i → seed' j = seed j

theorem OracleSpec.QuerySeed.addValues_eq_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) : seed.addValues xs = seed' ↔ seed i ++ xs = seed' i ∧ ∀ (j : ι), j ≠ i → seed j = seed' j

@[simp]

theorem OracleSpec.QuerySeed.pop_prependValues_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i : ι) (u : spec.Range i) : (s'.prependValues [u]).pop i = some (u, s')

theorem OracleSpec.QuerySeed.prependValues_singleton_injective {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (i : ι) : Function.Injective fun (p : spec.Range i × spec.QuerySeed) => p.2.prependValues [p.1]

theorem OracleSpec.QuerySeed.eq_prependValues_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {seed : spec.QuerySeed} {i : ι} {u : spec.Range i} {rest : spec.QuerySeed} (h : seed.pop i = some (u, rest)) : rest.prependValues [u] = seed

theorem OracleSpec.QuerySeed.pop_takeAtIndex_prependValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i₀ : ι) (k : ℕ) {t : ι} (u₀ : spec.Range t) (hti : t ≠ i₀) : ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop t = some (u₀, s'.takeAtIndex i₀ k)

theorem OracleSpec.QuerySeed.pop_takeAtIndex_prependValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i₀ : ι) (u₀ : spec.Range i₀) {k : ℕ} (hk : 0 < k) : ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop i₀ = some (u₀, s'.takeAtIndex i₀ (k - 1))