The typed oracularized decider

Piece O4 of planning/oracularization.md (issue #189): the decider of the paper's typed oracularized verifier (sec:orac-def, fig:oracle-decider) as a total CL.TypedDecider over the three roles, whose acceptance law is O2's bit-string predicate oraclePred.

The paper runs the input decider in its timeout-counter form, which halts within a bound B_𝒟(n) read off its description, and parses answers against that bound. The ambient model has no such form, and the detyping compiler needs a total typed decider, so the timeout is made explicit: an index routine (OracleDecider.Index) supplies at index n a parse cut B n and a simulation budget K n, and the decider runs an unclocked core under the clocked universal machine for K n steps. Three programs, each fixed, with the input programs as data:

• gameProg j, the game check: on (S̄, D̄, n, z, a₁, a₂), ask the input sampler for the marginals L^𝖠_{≤ j} z and L^𝖡_{≤ j} z and run the input decider on (n, L^𝖠 z, L^𝖡 z, a₁, a₂), all through the universal machine;
• core j, on ((S̄, D̄, B), (n, t, x, u, y, a, b)): parse each answer by its role against B, run the game check for each oracle, and accept iff every check of fig:oracle-decider passes;
• shell j, on ((S̄, D̄, Ī), input): ask the index routine Ī for (K n, B n) and run the core on ((S̄, D̄, B n), input) under the clocked universal machine with budget K n.

The decider is hardcode (shell j) (encode (S̄, D̄, Ī)), so its program is the s-m-n function of the three programs. It halts on every input, whatever the input programs do (oracleDecider_total), and it accepts exactly when the core accepts within the budget (oracleDecider_accepts_iff). The core's acceptance law is oraclePred exactly, with no hypothesis on the input verifier (core_accepts_iff): the input decider need not halt on the inputs it rejects, which is why both directions go through inversion lemmas of the programs. So the decider's acceptance implies oraclePred unconditionally (accepts_sound), and oraclePred implies acceptance once the core's run fits in the budget (accepts_complete) — the role the timeout bound plays in the paper's completeness.

Inverting the routing combinators

theorem MIPRE.Cost.Prog.let_closed_runs {p q : Prog} (hq : WellScoped 1 q) {x v r : Data} {s t : ℕ} (hp : p.Runs x v s) (hq' : q.Runs v r t) : (p.let_ q).Runs x r (s + t + 1)

Sequencing two closed programs.

theorem MIPRE.Cost.Prog.let_closed_inv {p q : Prog} (hq : WellScoped 1 q) {x r : Data} {t : ℕ} (h : (p.let_ q).Runs x r t) : ∃ (v : Data) (s : ℕ) (t' : ℕ), p.Runs x v s ∧ q.Runs v r t'

Inverting the sequence of two closed programs.

theorem MIPRE.Cost.Prog.callWithContext_inv {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) {a ctx r : Data} {t : ℕ} (h : (p.callWithContext post).Runs (a.cons ctx) r t) : ∃ (r' : Data) (t' : ℕ), p.Runs a r' t' ∧ r = post.toFun (ctx, r')

Inverting callWithContext: a run is a run of the callee on the argument, followed by the postprocessor.

theorem MIPRE.Cost.Prog.routeOneCall_indirect_inv (route : PolyTimeFun Data (Bool × Data)) {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) {x a ctx r : Data} {t : ℕ} (hroute : route.toFun x = (true, a.cons ctx)) (h : (routeOneCall route p post).Runs x r t) : ∃ (r' : Data) (t' : ℕ), p.Runs a r' t' ∧ r = post.toFun (ctx, r')

Inverting a routed call: when the router calls, a run is a run of the callee on the argument, followed by the postprocessor.

theorem MIPRE.Cost.Prog.routeOneCall_direct_inv (route : PolyTimeFun Data (Bool × Data)) (p : Prog) (post : PolyTimeFun (Data × Data) Data) {x r₀ r : Data} {t : ℕ} (hroute : route.toFun x = (false, r₀)) (h : (routeOneCall route p post).Runs x r t) : r = r₀

Inverting a routed call when the router answers directly.

The game check

noncomputable def MIPRE.OracleDecider.gS : Cost.PolyTimeFun Cost.Data Cost.Data

The input sampler's program, first field of a game check's input.

Equations

• MIPRE.OracleDecider.gS = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.OracleDecider.gD : Cost.PolyTimeFun Cost.Data Cost.Data

The input decider's program.

Equations

• MIPRE.OracleDecider.gD = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.OracleDecider.gN : Cost.PolyTimeFun Cost.Data Cost.Data

The index.

Equations

• MIPRE.OracleDecider.gN = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.OracleDecider.gZ : Cost.PolyTimeFun Cost.Data Cost.Data

The seed.

Equations

• MIPRE.OracleDecider.gZ = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.OracleDecider.gA : Cost.PolyTimeFun Cost.Data Cost.Data

The pair of answers.

Equations

• MIPRE.OracleDecider.gA = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.OracleDecider.margQuery (w : Player) (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The marginal query (n, w, marginal, j, z) at the game check's seed.

Equations

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

noncomputable def MIPRE.OracleDecider.gRoute₁ (j : ℕ) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

First call: Alice's marginal.

Equations

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

noncomputable def MIPRE.OracleDecider.gRoute₂ (j : ℕ) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Second call: Bob's marginal.

Equations

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

noncomputable def MIPRE.OracleDecider.gRoute₃ : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Third call: the input decider on the two questions and the two answers.

Equations

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

noncomputable def MIPRE.OracleDecider.gStage₁ (j : ℕ) : Cost.Prog

The three stages of the game check.

Equations

• MIPRE.OracleDecider.gStage₁ j = MIPRE.Cost.Prog.routeOneCall (MIPRE.OracleDecider.gRoute₁ j) MIPRE.Cost.selfUniversal.univ MIPRE.Cost.PolyTimeFun.treePair

noncomputable def MIPRE.OracleDecider.gStage₂ (j : ℕ) : Cost.Prog

Equations

• MIPRE.OracleDecider.gStage₂ j = MIPRE.Cost.Prog.routeOneCall (MIPRE.OracleDecider.gRoute₂ j) MIPRE.Cost.selfUniversal.univ MIPRE.Cost.PolyTimeFun.treePair

noncomputable def MIPRE.OracleDecider.gStage₃ : Cost.Prog

Equations

• MIPRE.OracleDecider.gStage₃ = MIPRE.Cost.Prog.routeOneCall MIPRE.OracleDecider.gRoute₃ MIPRE.Cost.selfUniversal.univ MIPRE.CL.Detyping.DeciderProgram.post

noncomputable def MIPRE.OracleDecider.gameProg (j : ℕ) : Cost.Prog

The game check at level j.

Equations

• MIPRE.OracleDecider.gameProg j = (MIPRE.OracleDecider.gStage₁ j).let_ ((MIPRE.OracleDecider.gStage₂ j).let_ MIPRE.OracleDecider.gStage₃)

theorem MIPRE.OracleDecider.gStage₁_closed (j : ℕ) : Cost.Prog.WellScoped 1 (gStage₁ j)

theorem MIPRE.OracleDecider.gStage₂_closed (j : ℕ) : Cost.Prog.WellScoped 1 (gStage₂ j)

theorem MIPRE.OracleDecider.gStage₃_closed : Cost.Prog.WellScoped 1 gStage₃

theorem MIPRE.OracleDecider.gTail_closed (j : ℕ) : Cost.Prog.WellScoped 1 ((gStage₂ j).let_ gStage₃)

theorem MIPRE.OracleDecider.gameProg_closed (j : ℕ) : Cost.Prog.WellScoped 1 (gameProg j)

def MIPRE.OracleDecider.gInput (sp dp : Cost.Prog) (n : ℕ) (z a₁ a₂ : Cost.BitStr) : Cost.Data

The input of a game check.

Equations

• MIPRE.OracleDecider.gInput sp dp n z a₁ a₂ = (MIPRE.Cost.encode sp).cons ((MIPRE.Cost.encode dp).cons (MIPRE.Cost.encode (n, z, a₁, a₂)))

theorem MIPRE.OracleDecider.gRoute₁_apply (j : ℕ) (sp dp : Cost.Prog) (n : ℕ) (z a₁ a₂ : Cost.BitStr) : (gRoute₁ j).toFun (gInput sp dp n z a₁ a₂) = (true, ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.marginal Player.alice j z))).cons (gInput sp dp n z a₁ a₂))

theorem MIPRE.OracleDecider.gRoute₂_apply (j : ℕ) (sp dp : Cost.Prog) (n : ℕ) (z a₁ a₂ : Cost.BitStr) (rA : Cost.Data) : (gRoute₂ j).toFun ((gInput sp dp n z a₁ a₂).cons rA) = (true, ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.marginal Player.bob j z))).cons ((gInput sp dp n z a₁ a₂).cons rA))

theorem MIPRE.OracleDecider.gRoute₃_apply (sp dp : Cost.Prog) (n : ℕ) (z a₁ a₂ : Cost.BitStr) (rA rB : Cost.Data) : gRoute₃.toFun (((gInput sp dp n z a₁ a₂).cons rA).cons rB) = (true, ((Cost.encode dp).cons ((Cost.encode n).cons (rA.cons (rB.cons (Cost.encode (a₁, a₂)))))).cons Cost.Data.nil)

noncomputable def MIPRE.OracleDecider.margBits {ℓ : ℕ} (S : CL.Sampler ℓ) (n j : ℕ) (w : Player) (z : Cost.BitStr) : Cost.BitStr

The question the game check computes for player w from the seed z.

Equations

• MIPRE.OracleDecider.margBits S n j w z = MIPRE.CL.toBits ((MIPRE.CL.CLFun.truncate j (S.cl n w)).eval (MIPRE.CL.ofBits (S.dim n) z))

noncomputable def MIPRE.OracleDecider.gameArg {ℓ : ℕ} (S : CL.Sampler ℓ) (n j : ℕ) (z a₁ a₂ : Cost.BitStr) : Cost.Data

The input decider's input in a game check.

Equations

• MIPRE.OracleDecider.gameArg S n j z a₁ a₂ = MIPRE.Cost.encode (n, MIPRE.OracleDecider.margBits S n j MIPRE.Player.alice z, MIPRE.OracleDecider.margBits S n j MIPRE.Player.bob z, a₁, a₂)

theorem MIPRE.OracleDecider.univ_marginal {ℓ : ℕ} (S : CL.Sampler ℓ) (n j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode S.prog).cons (Cost.encode (n, CL.Sampler.Query.marginal w j z))) (Cost.encode (margBits S n j w z)) t

The two marginal calls, through the universal machine.

theorem MIPRE.OracleDecider.gameProg_runs {ℓ : ℕ} (S : CL.Sampler ℓ) (dp : Cost.Prog) (n j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (z a₁ a₂ : Cost.BitStr) (hz : List.length z = S.dim n) {rD : Cost.Data} {tD : ℕ} (hD : dp.Runs (gameArg S n j z a₁ a₂) rD tD) : ∃ (t : ℕ), (gameProg j).Runs (gInput S.prog dp n z a₁ a₂) (Cost.encode (decide (rD = Cost.encode true))) t

The game check runs the input decider on the two questions and the two answers, and returns whether it accepted.

theorem MIPRE.OracleDecider.univ_marginal_inv {ℓ : ℕ} (S : CL.Sampler ℓ) (n j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) {r : Cost.Data} {t : ℕ} (h : Cost.selfUniversal.univ.Runs ((Cost.encode S.prog).cons (Cost.encode (n, CL.Sampler.Query.marginal w j z))) r t) : r = Cost.encode (margBits S n j w z)

The sampler's run on a marginal query, read back through the universal machine.

theorem MIPRE.OracleDecider.gameProg_inv {ℓ : ℕ} (S : CL.Sampler ℓ) (dp : Cost.Prog) (n j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (z a₁ a₂ : Cost.BitStr) (hz : List.length z = S.dim n) {r : Cost.Data} {t : ℕ} (h : (gameProg j).Runs (gInput S.prog dp n z a₁ a₂) r t) : ∃ (rD : Cost.Data) (tD : ℕ), dp.Runs (gameArg S n j z a₁ a₂) rD tD ∧ r = Cost.encode (decide (rD = Cost.encode true))

Inverting the game check: every run of it is a run of the input decider on the two questions and the two answers, whose verdict it returns.

theorem MIPRE.OracleDecider.gameProg_accepts_iff {ℓ : ℕ} (S : CL.Sampler ℓ) (dp : Cost.Prog) (n j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (z a₁ a₂ : Cost.BitStr) (hz : List.length z = S.dim n) : (∃ (t : ℕ), (gameProg j).Runs (gInput S.prog dp n z a₁ a₂) (Cost.encode true) t) ↔ ∃ (tD : ℕ), dp.Runs (gameArg S n j z a₁ a₂) (Cost.encode true) tD

The game check accepts exactly when the input decider does on the two questions and the two answers.

Parsing an answer by its role

theorem MIPRE.OracleDecider.toBool?_eq_some {d : Cost.Data} {b : Bool} : d.toBool? = some b ↔ d = Cost.Data.ofBool b

theorem MIPRE.OracleDecider.decode_bitStr_eq_some {d : Cost.Data} {x : Cost.BitStr} : Cost.decode d = some x ↔ d = Cost.encode x

A datum decodes to a bit string exactly when it is its encoding.

theorem MIPRE.OracleDecider.toList?_toBool?_eq_some {d : Cost.Data} {x : Cost.BitStr} : Cost.Data.toList? Cost.Data.toBool? d = some x ↔ d = Cost.encode x

theorem MIPRE.OracleDecider.pairDec_eq_some (s a₁ a₂ : Cost.BitStr) : pairDec s = some (a₁, a₂) ↔ Cost.Data.parse s = (Cost.encode a₁).cons (Cost.encode a₂)

An oracle's answer parses to a pair exactly when its postorder parse is the encoding of that pair.

theorem MIPRE.OracleDecider.parseAns_oracle (B : ℕ) (s : Cost.BitStr) : parseAns B Role.oracle s = match pairDec s with | some (a, b) => if h : List.length a ≤ B ∧ List.length b ≤ B then some (OAns.pair ⟨a, ⋯⟩ ⟨b, ⋯⟩) else none | none => none

theorem MIPRE.OracleDecider.parseAns_alice (B : ℕ) (s : Cost.BitStr) : parseAns B Role.alice s = if h : List.length s ≤ B then some (OAns.single ⟨s, h⟩) else none

theorem MIPRE.OracleDecider.parseAns_bob (B : ℕ) (s : Cost.BitStr) : parseAns B Role.bob s = if h : List.length s ≤ B then some (OAns.single ⟨s, h⟩) else none

noncomputable def MIPRE.OracleDecider.parseF : Cost.PolyTimeFun Cost.BitStr Cost.Data

Postorder parsing, as a polynomial-time function (Prog.parseProg).

Equations

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

@[simp]

theorem MIPRE.OracleDecider.parseF_apply (x : Cost.BitStr) : parseF.toFun x = Cost.Data.parse x

noncomputable def MIPRE.OracleDecider.andB {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) : Cost.PolyTimeFun α Bool

a ∧ b on Boolean-valued functions.

Equations

• MIPRE.OracleDecider.andB f g = f.ite g (MIPRE.Cost.PolyTimeFun.const false)

@[simp]

theorem MIPRE.OracleDecider.andB_apply {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) (x : α) : (andB f g).toFun x = (f.toFun x && g.toFun x)

noncomputable def MIPRE.OracleDecider.impB {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) : Cost.PolyTimeFun α Bool

¬ a ∨ b on Boolean-valued functions.

Equations

• MIPRE.OracleDecider.impB f g = f.ite g (MIPRE.Cost.PolyTimeFun.const true)

@[simp]

theorem MIPRE.OracleDecider.impB_apply {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Bool) (x : α) : (impB f g).toFun x = (!f.toFun x || g.toFun x)

noncomputable def MIPRE.OracleDecider.eqD {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Cost.Data) : Cost.PolyTimeFun α Bool

Equality of two raw trees.

Equations

• MIPRE.OracleDecider.eqD f g = MIPRE.Cost.PolyTimeFun.treeEq.ap₂ f g

@[simp]

theorem MIPRE.OracleDecider.eqD_apply {α : Type u_1} [Cost.SizedEncoding α] (f g : Cost.PolyTimeFun α Cost.Data) (x : α) : (eqD f g).toFun x = decide (f.toFun x = g.toFun x)

noncomputable def MIPRE.OracleDecider.isOracle (r : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Bool

Whether a role datum is the oracle's.

Equations

• MIPRE.OracleDecider.isOracle r = MIPRE.OracleDecider.eqD r (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.encode MIPRE.Role.oracle))

noncomputable def MIPRE.OracleDecider.treeOf (s : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.Data

The postorder parse of an answer datum.

Equations

• MIPRE.OracleDecider.treeOf s = MIPRE.OracleDecider.parseF.comp (MIPRE.CL.Detyping.Program.readBits.comp s)

noncomputable def MIPRE.OracleDecider.lenOk (s : Cost.PolyTimeFun Cost.Data Cost.Data) (B : Cost.PolyTimeFun Cost.Data ℕ) : Cost.PolyTimeFun Cost.Data Bool

A bit string datum of length at most the cut.

Equations

• MIPRE.OracleDecider.lenOk s B = MIPRE.Cost.PolyTimeFun.leNat.ap₂ (MIPRE.CL.Detyping.DeciderProgram.lengthNat.comp (MIPRE.CL.Detyping.Program.readBits.comp s)) B

noncomputable def MIPRE.OracleDecider.okAns (r s : Cost.PolyTimeFun Cost.Data Cost.Data) (B : Cost.PolyTimeFun Cost.Data ℕ) : Cost.PolyTimeFun Cost.Data Bool

The bounded parse, as a check: an oracle's answer must parse to the encoding of a pair of strings of length at most the cut, an isolated player's must have length at most the cut.

Equations

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

noncomputable def MIPRE.OracleDecider.reprAns (r s : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.Data

The parsed answer, as a datum: the parse tree of an oracle's answer, an isolated player's answer as it is.

Equations

• MIPRE.OracleDecider.reprAns r s = (MIPRE.OracleDecider.isOracle r).ite (MIPRE.OracleDecider.treeOf s) s

@[simp]

theorem MIPRE.OracleDecider.answers_mk_inj {B : ℕ} {a b : Cost.BitStr} (ha : List.length a ≤ B) (hb : List.length b ≤ B) : ⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b

def MIPRE.OracleDecider.ansData {B : ℕ} : OAns (Verifier.Answers B) → Cost.Data

The datum a parsed answer is represented by.

Equations

• MIPRE.OracleDecider.ansData (MIPRE.OAns.pair a b) = (MIPRE.Cost.encode ↑a).cons (MIPRE.Cost.encode ↑b)
• MIPRE.OracleDecider.ansData (MIPRE.OAns.single a) = MIPRE.Cost.encode ↑a

theorem MIPRE.OracleDecider.ansData_inj {B : ℕ} {r : Role} {U W : OAns (Verifier.Answers B)} (hU : SeededGame.shapeOk r U = true) (hW : SeededGame.shapeOk r W = true) : ansData U = ansData W ↔ U = W

Two answers of the same shape are equal exactly when their data are.

theorem MIPRE.OracleDecider.okAns_spec (r s : Cost.PolyTimeFun Cost.Data Cost.Data) (B : Cost.PolyTimeFun Cost.Data ℕ) (c : Cost.Data) (role : Role) (str : Cost.BitStr) (hr : r.toFun c = Cost.encode role) (hs : s.toFun c = Cost.encode str) : ((okAns r s B).toFun c = true ↔ (parseAns (B.toFun c) role str).isSome = true) ∧ ∀ (U : OAns (Verifier.Answers (B.toFun c))), parseAns (B.toFun c) role str = some U → (reprAns r s).toFun c = ansData U

The parse check is the bounded parse, and the parsed datum represents the parse.

theorem MIPRE.OracleDecider.shapeOk_of_parseAns {B : ℕ} {r : Role} {s : Cost.BitStr} {U : OAns (Verifier.Answers B)} (h : parseAns B r s = some U) : SeededGame.shapeOk r U = true

The bounded parse returns answers of the role's shape.

The core

noncomputable def MIPRE.OracleDecider.cSp : Cost.PolyTimeFun Cost.Data Cost.Data

The fields of the core's input ((S̄, D̄, B), (n, t, x, u, y, a, b)).

Equations

• MIPRE.OracleDecider.cSp = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.OracleDecider.cDp : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.cDp = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeHead)

noncomputable def MIPRE.OracleDecider.cB : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.OracleDecider.cB = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeHead))

noncomputable def MIPRE.OracleDecider.cN : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.cN = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.OracleDecider.cT : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.cT = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.OracleDecider.cX : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.cX = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.OracleDecider.cU : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.OracleDecider.cY : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.OracleDecider.cA : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.OracleDecider.cBb : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

def MIPRE.OracleDecider.cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : Cost.Data

The core's input.

Equations

• MIPRE.OracleDecider.cInput sp dp B n t x u y a b = MIPRE.Cost.encode ((sp, dp, B), n, t, x, u, y, a, b)

@[simp]

theorem MIPRE.OracleDecider.cSp_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cSp.toFun (cInput sp dp B n t x u y a b) = Cost.encode sp

@[simp]

theorem MIPRE.OracleDecider.cDp_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cDp.toFun (cInput sp dp B n t x u y a b) = Cost.encode dp

@[simp]

theorem MIPRE.OracleDecider.cB_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cB.toFun (cInput sp dp B n t x u y a b) = B

@[simp]

theorem MIPRE.OracleDecider.cN_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cN.toFun (cInput sp dp B n t x u y a b) = Cost.encode n

@[simp]

theorem MIPRE.OracleDecider.cT_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cT.toFun (cInput sp dp B n t x u y a b) = Cost.encode t

@[simp]

theorem MIPRE.OracleDecider.cX_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cX.toFun (cInput sp dp B n t x u y a b) = Cost.encode x

@[simp]

theorem MIPRE.OracleDecider.cU_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cU.toFun (cInput sp dp B n t x u y a b) = Cost.encode u

@[simp]

theorem MIPRE.OracleDecider.cY_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cY.toFun (cInput sp dp B n t x u y a b) = Cost.encode y

@[simp]

theorem MIPRE.OracleDecider.cA_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cA.toFun (cInput sp dp B n t x u y a b) = Cost.encode a

@[simp]

theorem MIPRE.OracleDecider.cBb_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : cBb.toFun (cInput sp dp B n t x u y a b) = Cost.encode b

noncomputable def MIPRE.OracleDecider.okA : Cost.PolyTimeFun Cost.Data Bool

The parse checks and the parsed answers of the two players.

Equations

• MIPRE.OracleDecider.okA = MIPRE.OracleDecider.okAns MIPRE.OracleDecider.cT MIPRE.OracleDecider.cA MIPRE.OracleDecider.cB

noncomputable def MIPRE.OracleDecider.okB : Cost.PolyTimeFun Cost.Data Bool

Equations

• MIPRE.OracleDecider.okB = MIPRE.OracleDecider.okAns MIPRE.OracleDecider.cU MIPRE.OracleDecider.cBb MIPRE.OracleDecider.cB

noncomputable def MIPRE.OracleDecider.repA : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.repA = MIPRE.OracleDecider.reprAns MIPRE.OracleDecider.cT MIPRE.OracleDecider.cA

noncomputable def MIPRE.OracleDecider.repB : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.repB = MIPRE.OracleDecider.reprAns MIPRE.OracleDecider.cU MIPRE.OracleDecider.cBb

noncomputable def MIPRE.OracleDecider.sameCheck : Cost.PolyTimeFun Cost.Data Bool

Check 2(a): equal roles force equal answers.

Equations

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

noncomputable def MIPRE.OracleDecider.ovpCheck (r r' rep rep' : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Bool

Check 2(b), for the role r against the role r': an oracle's component for an isolated player's role must be that player's answer.

Equations

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

noncomputable def MIPRE.OracleDecider.localCheck : Cost.PolyTimeFun Cost.Data Bool

The checks that need no call: both parses, check 2(a) and check 2(b) both ways.

Equations

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

theorem MIPRE.OracleDecider.ovpCheck_spec {B : ℕ} (r r' rep rep' : Cost.PolyTimeFun Cost.Data Cost.Data) (c : Cost.Data) (t u : Role) (U W : OAns (Verifier.Answers B)) (hU : SeededGame.shapeOk t U = true) (hW : SeededGame.shapeOk u W = true) (hr : r.toFun c = Cost.encode t) (hr' : r'.toFun c = Cost.encode u) (hrep : rep.toFun c = ansData U) (hrep' : rep'.toFun c = ansData W) {V : Type u_1} (z z' : V) : (ovpCheck r r' rep rep').toFun c = SeededGame.oracleVsPlayer (t, z) (u, z') U W

theorem MIPRE.OracleDecider.sameCheck_spec {B : ℕ} (c : Cost.Data) (t u : Role) (U W : OAns (Verifier.Answers B)) (hU : SeededGame.shapeOk t U = true) (hW : SeededGame.shapeOk u W = true) (ht : cT.toFun c = Cost.encode t) (hu : cU.toFun c = Cost.encode u) (hrA : repA.toFun c = ansData U) (hrB : repB.toFun c = ansData W) : sameCheck.toFun c = if t = u then decide (U = W) else true

theorem MIPRE.OracleDecider.localCheck_spec (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) {V : Type u_1} (z z' : V) : localCheck.toFun (cInput sp dp B n t x u y a b) = true ↔ ∃ (U : OAns (Verifier.Answers B)) (W : OAns (Verifier.Answers B)), parseAns B t a = some U ∧ parseAns B u b = some W ∧ (if t = u then decide (U = W) else true) = true ∧ SeededGame.oracleVsPlayer (t, z) (u, z') U W = true ∧ SeededGame.oracleVsPlayer (u, z') (t, z) W U = true

The local checks are the checks of oaccepts that need no call.

The game checks and the verdict

noncomputable def MIPRE.OracleDecider.gArg (z rep : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.Data

The game check's input for the answer datum rep at the seed z.

Equations

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

noncomputable def MIPRE.OracleDecider.gameRoute (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Route a game check: when cond holds of the core's input (read through view), call the game check on arg; otherwise pass true on. The whole state is the context either way.

Equations

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

noncomputable def MIPRE.OracleDecider.cond₁ : Cost.PolyTimeFun Cost.Data Bool

The game check of each player runs when that player is an oracle whose answer parsed.

Equations

• MIPRE.OracleDecider.cond₁ = MIPRE.OracleDecider.andB (MIPRE.OracleDecider.isOracle MIPRE.OracleDecider.cT) MIPRE.OracleDecider.okA

noncomputable def MIPRE.OracleDecider.cond₂ : Cost.PolyTimeFun Cost.Data Bool

Equations

• MIPRE.OracleDecider.cond₂ = MIPRE.OracleDecider.andB (MIPRE.OracleDecider.isOracle MIPRE.OracleDecider.cU) MIPRE.OracleDecider.okB

noncomputable def MIPRE.OracleDecider.arg₁ : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.arg₁ = MIPRE.OracleDecider.gArg MIPRE.OracleDecider.cX MIPRE.OracleDecider.repA

noncomputable def MIPRE.OracleDecider.arg₂ : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.OracleDecider.arg₂ = MIPRE.OracleDecider.gArg MIPRE.OracleDecider.cY MIPRE.OracleDecider.repB

noncomputable def MIPRE.OracleDecider.gameStage (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.Prog

A routed game check.

Equations

• MIPRE.OracleDecider.gameStage j cond arg view = MIPRE.Cost.Prog.routeOneCall (MIPRE.OracleDecider.gameRoute cond arg view) (MIPRE.OracleDecider.gameProg j) MIPRE.Cost.PolyTimeFun.treePair

theorem MIPRE.OracleDecider.gameStage_closed (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.Prog.WellScoped 1 (gameStage j cond arg view)

noncomputable def MIPRE.OracleDecider.verdict : Cost.PolyTimeFun Cost.Data Bool

The verdict: the local checks passed and both game checks returned true.

Equations

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

noncomputable def MIPRE.OracleDecider.coreTail (j : ℕ) : Cost.Prog

The second game check and the verdict.

Equations

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

theorem MIPRE.OracleDecider.coreTail_closed (j : ℕ) : Cost.Prog.WellScoped 1 (coreTail j)

noncomputable def MIPRE.OracleDecider.core (j : ℕ) : Cost.Prog

The core of the typed oracularized decider.

Equations

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

theorem MIPRE.OracleDecider.gameStage_inv (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) {s r : Cost.Data} {t : ℕ} (h : (gameStage j cond arg view).Runs s r t) : cond.toFun (view.toFun s) = false ∧ r = s.cons (Cost.encode true) ∨ cond.toFun (view.toFun s) = true ∧ ∃ (v : Cost.Data) (tv : ℕ), (gameProg j).Runs (arg.toFun (view.toFun s)) v tv ∧ r = s.cons v

theorem MIPRE.OracleDecider.gameStage_shape (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) {s r : Cost.Data} {t : ℕ} (h : (gameStage j cond arg view).Runs s r t) : ∃ (v : Cost.Data), r = s.cons v

theorem MIPRE.OracleDecider.gameStage_runs_false (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) (s : Cost.Data) (hc : cond.toFun (view.toFun s) = false) : ∃ (t : ℕ), (gameStage j cond arg view).Runs s (s.cons (Cost.encode true)) t

theorem MIPRE.OracleDecider.gameStage_runs_true (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) (s : Cost.Data) (hc : cond.toFun (view.toFun s) = true) {v : Cost.Data} {tv : ℕ} (hv : (gameProg j).Runs (arg.toFun (view.toFun s)) v tv) : ∃ (t : ℕ), (gameStage j cond arg view).Runs s (s.cons v) t

The core's acceptance law

theorem MIPRE.OracleDecider.gameArg_seed {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) (z : V.Questions n) (a₁ a₂ : Cost.BitStr) : gameArg V.sampler n (ℓ + 1) (CL.toBits z) a₁ a₂ = Cost.encode (n, CL.toBits ((V.seeded n B).LA z), CL.toBits ((V.seeded n B).LB z), a₁, a₂)

The input decider's input in the game check at a seed is the query of 𝒱_n's predicate.

theorem MIPRE.OracleDecider.gameProg_accepts_iff_gameCheck {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) (z : V.Questions n) (a₁ a₂ : Verifier.Answers B) : (∃ (t : ℕ), (gameProg (ℓ + 1)).Runs (gInput V.sampler.prog V.decider.prog n (CL.toBits z) ↑a₁ ↑a₂) (Cost.encode true) t) ↔ (V.seeded n B).gameCheck (Role.oracle, z) (OAns.pair a₁ a₂) = true

One game check is the game check of fig:oracle-decider.

theorem MIPRE.OracleDecider.gameStage_sound {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) (s : Cost.Data) (role : Role) (z : V.Questions n) (U : OAns (Verifier.Answers B)) (hU : SeededGame.shapeOk role U = true) (hcond : cond.toFun (view.toFun s) = decide (role = Role.oracle)) (harg : ∀ (a₁ a₂ : Verifier.Answers B), U = OAns.pair a₁ a₂ → arg.toFun (view.toFun s) = gInput V.sampler.prog V.decider.prog n (CL.toBits z) ↑a₁ ↑a₂) {r : Cost.Data} {t : ℕ} (h : (gameStage (ℓ + 1) cond arg view).Runs s r t) : ∃ (v : Cost.Data), r = s.cons v ∧ (v = Cost.encode true → (V.seeded n B).gameCheck (role, z) U = true)

A game-check stage returns true only if the role's game check holds.

theorem MIPRE.OracleDecider.gameStage_complete {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) (s : Cost.Data) (role : Role) (z : V.Questions n) (U : OAns (Verifier.Answers B)) (hU : SeededGame.shapeOk role U = true) (hcond : cond.toFun (view.toFun s) = decide (role = Role.oracle)) (harg : ∀ (a₁ a₂ : Verifier.Answers B), U = OAns.pair a₁ a₂ → arg.toFun (view.toFun s) = gInput V.sampler.prog V.decider.prog n (CL.toBits z) ↑a₁ ↑a₂) (hg : (V.seeded n B).gameCheck (role, z) U = true) : ∃ (t : ℕ), (gameStage (ℓ + 1) cond arg view).Runs s (s.cons (Cost.encode true)) t

A game-check stage returns true when the role's game check holds.

theorem MIPRE.OracleDecider.oraclePred_eq_true_iff {V' : Type u_1} {B : ℕ} (S : SeededGame V' (Verifier.Answers B)) (p q : Role × V') (a b : Cost.BitStr) : oraclePred S p q a b = true ↔ ∃ (U : OAns (Verifier.Answers B)) (W : OAns (Verifier.Answers B)), parseAns B p.1 a = some U ∧ parseAns B q.1 b = some W ∧ S.oaccepts p q U W = true

oraclePred accepts exactly the pairs that parse to answers oaccepts accepts.

theorem MIPRE.OracleDecider.oaccepts_eq_true_iff {V' : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V' A) (p q : Role × V') (U W : OAns A) : S.oaccepts p q U W = true ↔ SeededGame.shapeOk p.1 U = true ∧ SeededGame.shapeOk q.1 W = true ∧ S.gameCheck p U = true ∧ S.gameCheck q W = true ∧ (if p.1 = q.1 then decide (U = W) else true) = true ∧ SeededGame.oracleVsPlayer p q U W = true ∧ SeededGame.oracleVsPlayer q p W U = true

theorem MIPRE.OracleDecider.core_accepts_iff {ℓ : ℕ} (V : Verifier (ℓ + 1)) (B n : ℕ) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) : (∃ (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time) ↔ oraclePred (V.seeded n B) (t, x) (u, y) a b = true

The core's acceptance law is oraclePred, with no hypothesis on the input verifier: the input decider need not halt on the inputs it rejects.

The shell: the index routine and the clock

structure MIPRE.OracleDecider.Index : Type

The index routine of the oracularized decider: at index n, a simulation budget K n, in unary, and a parse cut B n — the explicit form of the paper's timeout bound B_𝒟(n), which plays both roles there.

• cut : ℕ → ℕ

  The parse cut.

• budget : ℕ → ℕ

  The simulation budget.

• prog : Cost.Prog

  The routine.

• runs (n : ℕ) : ∃ (t : ℕ), self.prog.Runs (Cost.encode n) ((Cost.Data.ofNat (self.budget n)).cons (Cost.encode (self.cut n))) t

  On n it returns (K n, B n).

noncomputable def MIPRE.OracleDecider.sIp : Cost.PolyTimeFun Cost.Data Cost.Data

The index routine's program, third of the hardcoded programs.

Equations

• MIPRE.OracleDecider.sIp = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeHead)

noncomputable def MIPRE.OracleDecider.sIndex : Cost.PolyTimeFun Cost.Data ℕ

The index of the typed input.

Equations

• MIPRE.OracleDecider.sIndex = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.OracleDecider.indexRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Call the index routine on the index.

Equations

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

noncomputable def MIPRE.OracleDecider.indexPost (j : ℕ) : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Assemble the clocked simulation's input (K, (core, ((S̄, D̄, B), input))) from the index routine's answer (K, B).

Equations

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

noncomputable def MIPRE.OracleDecider.indexStage (j : ℕ) : Cost.Prog

The index stage.

Equations

• MIPRE.OracleDecider.indexStage j = MIPRE.Cost.Prog.routeOneCall MIPRE.OracleDecider.indexRoute MIPRE.Cost.selfUniversal.univ (MIPRE.OracleDecider.indexPost j)

noncomputable def MIPRE.OracleDecider.shell (j : ℕ) : Cost.Prog

The shell: the index stage, the clocked simulation of the core, and the check of its result.

Equations

• MIPRE.OracleDecider.shell j = (MIPRE.OracleDecider.indexStage j).let_ (MIPRE.Cost.selfClockedUniversal.univT.let_ MIPRE.CL.Detyping.ClockProgram.checkResult.code)

theorem MIPRE.OracleDecider.shellTail_closed : Cost.Prog.WellScoped 1 (Cost.selfClockedUniversal.univT.let_ CL.Detyping.ClockProgram.checkResult.code)

theorem MIPRE.OracleDecider.shell_closed (j : ℕ) : Cost.Prog.WellScoped 1 (shell j)

theorem MIPRE.OracleDecider.shell_runs (j : ℕ) (sp dp : Cost.Prog) (I : Index) (input : Cost.Data) : ∃ (time : ℕ), (shell j).Runs ((Cost.encode (sp, dp, I.prog)).cons input) (Cost.encode (decide (Cost.clockedResult (core j) ((Cost.encode (sp, dp, I.cut (CL.Detyping.Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input)))).cons input) (I.budget (CL.Detyping.Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) = (Cost.encode true).cons (Cost.encode true)))) time

The shell's run on every input with the hardcoded programs: the verdict of the core, clocked at the budget, on the input with the parse cut.

noncomputable def MIPRE.OracleDecider.oracleDecider (j : ℕ) (sp dp : Cost.Prog) (I : Index) : CL.Detyping.TypedDecider Role

The typed oracularized decider, at level j, of the input programs S̄, D̄ with the index routine I.

Equations

• MIPRE.OracleDecider.oracleDecider j sp dp I = { prog := MIPRE.Cost.hardcode (MIPRE.OracleDecider.shell j) (MIPRE.Cost.encode (sp, dp, I.prog)), closed := ⋯ }

theorem MIPRE.OracleDecider.oracleDecider_total (j : ℕ) (sp dp : Cost.Prog) (I : Index) : (oracleDecider j sp dp I).Total

The decider halts on every input, whatever the input programs do.

theorem MIPRE.OracleDecider.oracleDecider_accepts_iff (j : ℕ) (sp dp : Cost.Prog) (I : Index) (n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : (oracleDecider j sp dp I).Accepts n t x u y a b ↔ ∃ time ≤ I.budget n, (core j).Runs (cInput sp dp (I.cut n) n t x u y a b) (Cost.encode true) time

The decider accepts exactly when the core accepts within the budget.

theorem MIPRE.OracleDecider.accepts_sound {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (n : ℕ) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) (h : (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I).Accepts n t (CL.toBits x) u (CL.toBits y) a b) : oraclePred (V.seeded n (I.cut n)) (t, x) (u, y) a b = true

Soundness of the acceptance law: the decider accepts only answers oraclePred accepts, at the index routine's cut, whatever the budget.

theorem MIPRE.OracleDecider.accepts_complete {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (n : ℕ) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) (h : oraclePred (V.seeded n (I.cut n)) (t, x) (u, y) a b = true) (hK : ∀ (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog (I.cut n) n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time → time ≤ I.budget n) : (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I).Accepts n t (CL.toBits x) u (CL.toBits y) a b

Completeness of the acceptance law: the decider accepts the answers oraclePred accepts once the core's accepting run fits in the budget.

noncomputable def MIPRE.OracleDecider.deciderProgFun (j : ℕ) : Cost.PolyTimeFun (Cost.Prog × Cost.Prog × Cost.Prog) Cost.Prog

The decider's program as a polynomial-time function of the three programs: the s-m-n map.

Equations

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

theorem MIPRE.OracleDecider.deciderProgFun_apply (j : ℕ) (sp dp : Cost.Prog) (I : Index) : (deciderProgFun j).toFun (sp, dp, I.prog) = (oracleDecider j sp dp I).prog

The typed predicate of the detyping compiler

The detyping compiler reads a typed decider through typedPredicate, whose typed game over the complete graph on the roles is O2's (oracleSampler_cl). Its acceptance factors through the bounded parse, and it accepts the honest encodings once the core's runs on them fit in the budget: the two forms in which O2's value transfers take a typed predicate.

theorem MIPRE.OracleDecider.typedPredicate_sound {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) (p q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) (a b : Verifier.Answers (C.outer n)) (h : CL.Detyping.DeciderProgram.typedPredicate (oracleSampler V.sampler) (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I) C n p q a b = true) : (V.seeded n (I.cut n)).oaccepts p q ((parseAns (I.cut n) p.1 ↑a).getD default) ((parseAns (I.cut n) q.1 ↑b).getD default) = true

The compiler's typed predicate of the oracularized decider accepts only what oaccepts accepts after the bounded parse.

theorem MIPRE.OracleDecider.typedPredicate_complete {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) (hin : 8 * I.cut n + 3 ≤ C.inner n) (hout : C.inner n ≤ C.outer n) (hK : ∀ (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr), List.length a ≤ C.inner n → List.length b ≤ C.inner n → ∀ (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog (I.cut n) n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time → time ≤ I.budget n) (p q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) (U W : OAns (Verifier.Answers (I.cut n))) (h : (V.seeded n (I.cut n)).oaccepts p q U W = true) : CL.Detyping.DeciderProgram.typedPredicate (oracleSampler V.sampler) (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I) C n p q ⟨encAns U, ⋯⟩ ⟨encAns W, ⋯⟩ = true

The compiler's typed predicate of the oracularized decider accepts the honest encodings of every answer pair oaccepts accepts, when the inner cut holds them and the core's accepting runs fit in the budget.

theorem MIPRE.OracleDecider.valStar_ge_of_typedPredicate {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < quantumValue (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) (CL.Detyping.DeciderProgram.typedPredicate (oracleSampler V.sampler) (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I) C n))) : 1 - 24 * √ε ≤ V.valStar n (I.cut n)

Soundness of the compiled typed game: its quantum value above 1 - ε puts val*(𝒱_n) at the parse cut at least 1 - 24√ε, whatever the budget.

theorem MIPRE.OracleDecider.exists_typedPredicate_perfectPCC {ℓ : ℕ} (V : Verifier (ℓ + 1)) (I : Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) (hin : 8 * I.cut n + 3 ≤ C.inner n) (hout : C.inner n ≤ C.outer n) (hK : ∀ (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr), List.length a ≤ C.inner n → List.length b ≤ C.inner n → ∀ (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog (I.cut n) n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time → time ≤ I.budget n) (hV : V.HasPerfectPCC n (I.cut n)) : ∃ (R : SyncStrategy (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) (CL.Detyping.DeciderProgram.typedPredicate (oracleSampler V.sampler) (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I) C n)).doubled), R.IsPCC ∧ R.value = 1

Completeness of the compiled typed game: a value-1 PCC strategy of 𝒱_n at the parse cut gives one of the doubled typed game, when the inner cut holds every honest encoding and the core's accepting runs fit in the budget.