Executable detyping of the decision predicate

The compiler first queries the supplied typed sampler for its dimension, then runs the supplied cutoff routine, and finally applies the graph router. Both the original answers and the original index are retained. The cutoff routine is an actual program: its bounds need not be polynomial in the binary index.

structure MIPRE.CL.Detyping.TypedDecider (T : Type u_1) [Cost.SizedEncoding T] : Type

A typed decider uses the source's seven-field input convention.

• prog : Cost.Prog
• closed : Cost.Prog.WellScoped 1 self.prog

def MIPRE.CL.Detyping.TypedDecider.Accepts {T : Type u_1} [Cost.SizedEncoding T] (D : TypedDecider T) (n : ℕ) (u : T) (x : Cost.BitStr) (v : T) (y a b : Cost.BitStr) : Prop

Equations

• D.Accepts n u x v y a b = ∃ (time : ℕ), D.prog.Runs (MIPRE.Cost.encode (n, u, x, v, y, a, b)) (MIPRE.Cost.encode true) time

def MIPRE.CL.Detyping.TypedDecider.Total {T : Type u_1} [Cost.SizedEncoding T] (D : TypedDecider T) : Prop

Equations

• D.Total = ∀ (n : ℕ) (d : MIPRE.Cost.Data), MIPRE.Cost.Halts D.prog ((MIPRE.Cost.encode n).cons d)

structure MIPRE.CL.Detyping.CutoffProgram : Type

An executable pair of answer bounds. The inner bound is the source typed game's cutoff for its entire answer; the outer bound applies even on nonedge views.

• inner : ℕ → ℕ
• outer : ℕ → ℕ
• prog : Cost.Prog
• closed : Cost.Prog.WellScoped 1 self.prog
• runs (n : ℕ) : ∃ (time : ℕ), self.prog.Runs (Cost.encode n) (Cost.encode (self.inner n, self.outer n)) time

noncomputable def MIPRE.CL.Detyping.DeciderProgram.pairPost : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

• MIPRE.CL.Detyping.DeciderProgram.pairPost = MIPRE.Cost.PolyTimeFun.treePair

noncomputable def MIPRE.CL.Detyping.DeciderProgram.dimensionRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.cutoffRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.dimensionStage {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) : Cost.Prog

Equations

• MIPRE.CL.Detyping.DeciderProgram.dimensionStage S = MIPRE.Cost.Prog.routeOneCall MIPRE.CL.Detyping.DeciderProgram.dimensionRoute S.prog MIPRE.CL.Detyping.DeciderProgram.pairPost

noncomputable def MIPRE.CL.Detyping.DeciderProgram.cutoffStage (C : CutoffProgram) : Cost.Prog

Equations

• MIPRE.CL.Detyping.DeciderProgram.cutoffStage C = MIPRE.Cost.Prog.routeOneCall MIPRE.CL.Detyping.DeciderProgram.cutoffRoute C.prog MIPRE.CL.Detyping.DeciderProgram.pairPost

noncomputable def MIPRE.CL.Detyping.DeciderProgram.decisionStage {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) : Cost.Prog

Equations

• MIPRE.CL.Detyping.DeciderProgram.decisionStage E D = MIPRE.Cost.Prog.routeOneCall (MIPRE.CL.Detyping.DeciderProgram.route E) D.prog MIPRE.CL.Detyping.DeciderProgram.post

theorem MIPRE.CL.Detyping.DeciderProgram.dimensionStage_closed {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) : Cost.Prog.WellScoped 1 (dimensionStage S)

theorem MIPRE.CL.Detyping.DeciderProgram.cutoffStage_closed (C : CutoffProgram) : Cost.Prog.WellScoped 1 (cutoffStage C)

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_closed {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) : Cost.Prog.WellScoped 1 (decisionStage E D)

noncomputable def MIPRE.CL.Detyping.DeciderProgram.prog {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) : Cost.Prog

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.prog_closed {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) : Cost.Prog.WellScoped 1 (prog E S D C)

theorem MIPRE.CL.Detyping.DeciderProgram.dimensionStage_runs {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (input : Cost.Data) : ∃ (time : ℕ), (dimensionStage S).Runs input (input.cons (Cost.encode (S.dim (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))))) time

theorem MIPRE.CL.Detyping.DeciderProgram.cutoffStage_runs (C : CutoffProgram) (input : Cost.Data) (s : ℕ) : ∃ (time : ℕ), (cutoffStage C).Runs (input.cons (Cost.encode s)) (context input s (C.inner (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.outer (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input)))) time

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_direct {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (c r : Cost.Data) (h : (route E).toFun c = (false, r)) : ∃ (time : ℕ), (decisionStage E D).Runs c r time

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_indirect {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (c arg ctx r : Cost.Data) (time : ℕ) (h : (route E).toFun c = (true, arg.cons ctx)) (hr : D.prog.Runs arg r time) : ∃ (time : ℕ), (decisionStage E D).Runs c (post.toFun (ctx, r)) time

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_halts {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (hD : D.Total) (c : Cost.Data) : Cost.Halts (decisionStage E D) c

theorem MIPRE.CL.Detyping.DeciderProgram.prog_runs {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (input r : Cost.Data) (time : ℕ) (h : (decisionStage E D).Runs (context input (S.dim (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.inner (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.outer (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input)))) r time) : ∃ (t : ℕ), (prog E S D C).Runs input r t

Prefixing the two executable index routines to any decision-stage run.

theorem MIPRE.CL.Detyping.DeciderProgram.prog_halts {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hD : D.Total) (input : Cost.Data) : Cost.Halts (prog E S D C) input

The compiled program halts on every raw data tree, including malformed indices.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.decider {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) : Decider

A genuine ambient decider, built from executable source programs.

Equations

• MIPRE.CL.Detyping.DeciderProgram.decider E S D C = { prog := MIPRE.CL.Detyping.DeciderProgram.prog E S D C, closed := ⋯ }