The executable typed introspection sampler router

Dimension queries and Pauli queries call the supplied sampler once. Auxiliary queries write the zero vector or the appropriate factor indicator, using the length of the supplied vector. This total router needs no decoding of the ambient dimension and does not depend on the number of hiding types.

def MIPRE.Introspection.SamplerProgram.auxResult (p : CL.Detyping.Program.Parsed) : Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.SamplerProgram.aux : Cost.PolyTimeFun CL.Detyping.Program.Parsed Cost.BitStr

Equations

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

theorem MIPRE.Introspection.SamplerProgram.aux_apply (p : CL.Detyping.Program.Parsed) : aux.toFun p = auxResult p

noncomputable def MIPRE.Introspection.SamplerProgram.routeResult (x : Cost.Data) : Bool × Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.SamplerProgram.route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

theorem MIPRE.Introspection.SamplerProgram.route_apply (x : Cost.Data) : route.toFun x = routeResult x

theorem MIPRE.Introspection.SamplerProgram.route_dimension {P : Type u_1} [Cost.SizedEncoding P] (n : ℕ) : route.toFun (Cost.encode (n, CL.TypedSampler.Query.dimension)) = CL.Detyping.Program.callResult ((Cost.encode n).cons Cost.Data.nil) Cost.Data.nil

theorem MIPRE.Introspection.SamplerProgram.route_pauli {P : Type u_1} [Cost.SizedEncoding P] (ℓ n : ℕ) (p : P) (q : CL.Sampler.Query) : route.toFun (Cost.encode (n, CL.TypedSampler.Query.atType (QuestionType.pauli p) q)) = CL.Detyping.Program.callResult (Cost.encode (n, CL.TypedSampler.Query.atType p q)) Cost.Data.nil

theorem MIPRE.Introspection.SamplerProgram.route_aux {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} (n : ℕ) (t : AuxType ℓ) (role : Bool) (q : CL.Sampler.Query) : route.toFun (Cost.encode (n, CL.TypedSampler.Query.atType (Sum.inr (t, role)) q)) = CL.Detyping.Program.directResult (auxResult (Cost.encode n, q.toTuple.1, q.toTuple.2.1.toBool, q.toTuple.2.2.1, q.toTuple.2.2.2.1, q.toTuple.2.2.2.2))

theorem MIPRE.Introspection.SamplerProgram.route_preserves (n : ℕ) (q a : Cost.Data) (h : route.toFun ((Cost.encode n).cons q) = (true, a)) : ∃ (d : Cost.Data) (ctx : Cost.Data), a = ((Cost.encode n).cons d).cons ctx

noncomputable def MIPRE.Introspection.SamplerProgram.post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

• MIPRE.Introspection.SamplerProgram.post = MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.SamplerProgram.prog {P : Type u_1} [Cost.SizedEncoding P] (S : CL.TypedSampler 3 P) : Cost.Prog

Equations

• MIPRE.Introspection.SamplerProgram.prog S = MIPRE.Cost.Prog.routeOneCall MIPRE.Introspection.SamplerProgram.route S.prog MIPRE.Introspection.SamplerProgram.post

theorem MIPRE.Introspection.SamplerProgram.prog_closed {P : Type u_1} [Cost.SizedEncoding P] (S : CL.TypedSampler 3 P) : Cost.Prog.WellScoped 1 (prog S)

theorem MIPRE.Introspection.SamplerProgram.prog_halts {P : Type u_1} [Cost.SizedEncoding P] (S : CL.TypedSampler 3 P) (n : ℕ) (d : Cost.Data) : Cost.Halts (prog S) ((Cost.encode n).cons d)

theorem MIPRE.Introspection.SamplerProgram.prog_run_call {P : Type u_1} [Cost.SizedEncoding P] (S : CL.TypedSampler 3 P) (x a r : Cost.Data) (time : ℕ) (h : route.toFun x = CL.Detyping.Program.callResult a Cost.Data.nil) (hr : S.prog.Runs a r time) : ∃ (t : ℕ), (prog S).Runs x r t

theorem MIPRE.Introspection.SamplerProgram.prog_run_direct {P : Type u_1} [Cost.SizedEncoding P] (S : CL.TypedSampler 3 P) (x : Cost.Data) (out : Cost.BitStr) (h : route.toFun x = CL.Detyping.Program.directResult out) : ∃ (t : ℕ), (prog S).Runs x (Cost.encode out) t