Oracle algorithms
Single-oracle computations
AbbreviationThe signature of one oracle#✓fully proved
For types \(X\) and \(Y\), this is the polynomial functor whose operations are the queries \(x \in X\), each answered by an element of \(Y\).
abbrev OracleSig (X : Type u) (Y : Type v) : PFunctor.{u, v} := ⟨X, fun _ => Y⟩Used by 16
AbbreviationAdaptive oracle algorithms#✓fully proved
For a type \(X\) of queries, a type \(Y\) of answers and a type \(\alpha\) of outputs, an adaptive deterministic oracle algorithm is an element of CSLib's free monad over the polynomial functor of one oracle with queries \(X\) and answers \(Y\). It is built inductively: it either stops with an output in \(\alpha\), or asks a query \(x \in X\) and continues with an algorithm that depends on the answer \(y \in Y\).
abbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αabbrev OracleSig (X : Type u) (Y : Type v) : PFunctor.{u, v} := ⟨X, fun _ => Y⟩CSLibExt/Crypto/Framework/Oracle.lean:201
Uses 1 · Used by 25
AbbreviationThe oracle algorithm that stops at once#✓fully proved
For an output \(a \in \alpha\), this is the adaptive oracle algorithm with queries in \(X\) and answers in \(Y\) that asks no query and stops with output \(a\).
abbrev done (a : α) : OracleComp X Y α := .pure aabbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
Uses 2 · Used by 7
AbbreviationQuery step#✓fully proved
For a point \(x \in X\) and a continuation \(k\) assigning an oracle algorithm to each answer \(y \in Y\), the oracle algorithm that first queries \(x\) and then continues with \(k(y)\), where \(y\) is the answer.
abbrev query (x : X) (k : Y → OracleComp X Y α) : OracleComp X Y α := .liftBind x kabbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
Uses 2 · Used by 7
DefinitionRunning an oracle algorithm#✓fully proved
Given a function \(O : X \to Y\), the run of an oracle algorithm with queries in \(X\), answers in \(Y\) and outputs in \(\alpha\) is its output when every query \(x\) is answered by \(O(x)\): an algorithm that stops with output \(a\) runs to \(a\), and one that queries \(x\) and continues with \(k(y)\) on answer \(y\) runs to the run of \(k(O(x))\).
def run (O : X → Y) : OracleComp X Y α → α
| .pure a => a
| .liftBind x k => run O (k (O x))abbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
Uses 2 · Used by 11
DefinitionQueries of an oracle algorithm#✓fully proved
For an oracle algorithm \(c\) and a function \(O : X \to Y\), the queries of \(c\) against \(O\) are the list of the points of \(X\) that \(c\) asks, in order, when every query \(x\) is answered by \(O(x)\): the empty list if \(c\) stops, and otherwise the first query \(x\) followed by the queries of the continuation on the answer \(O(x)\).
def queries (O : X → Y) : OracleComp X Y α → List X
| .pure _ => []
| .liftBind x k => x :: queries O (k (O x))abbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
Uses 2 · Used by 6
TheoremLocality of oracle runs#✓fully proved
Let \(c\) be an oracle algorithm and let \(O, O' : X \to Y\) agree at every query of \(c\) against \(O\). Then \(c\) has the same output against \(O\) as against \(O'\), and the same list of queries against \(O\) as against \(O'\).
theorem run_congr {O O' : X → Y} :
∀ (c : OracleComp X Y α), (∀ x ∈ c.queries O, O x = O' x) →
c.run O = c.run O' ∧ c.queries O = c.queries O'abbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
Uses 4 · Used by 1
TheoremRunning a sequential composition#✓fully proved
Let \(c\) be an oracle algorithm with outputs in \(\alpha\), let \(g\) map each \(a \in \alpha\) to an oracle algorithm with outputs in \(\beta\), and let \(O : X \to Y\). Running against \(O\) the composition that first runs \(c\) and then continues with \(g\) applied to its output gives the output of \(g(a)\) run against \(O\), where \(a\) is the output of \(c\) run against \(O\).
theorem run_bind {β : Type*} (O : X → Y) (g : α → OracleComp X Y β) :
∀ c : OracleComp X Y α, run O (PFunctor.FreeM.bind c g) = (g (c.run O)).run Oabbrev OracleComp (X : Type u) (Y : Type v) (α : Type w) : Type (max u v w) :=
(OracleSig X Y).FreeM αCSLibExt/Crypto/Framework/Oracle.lean:207
def run (O : X → Y) : OracleComp X Y α → α
| .pure a => a
| .liftBind x k => run O (k (O x))CSLibExt/Crypto/Framework/Oracle.lean:221
Uses 3 · Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.