Executable source queries and matrix reconstruction

The clock is supplied once as unary data. Matrix reconstruction queries the linear map on the standard basis and transposes those columns. All operations are polynomial in the explicit clock, source text, and register length. Correctness is used only after the prefix scan establishes the source interface's attained-prefix premise.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliarySource.Context : Type

Equations

• MIPRE.Introspection.AuxiliarySource.Context = (MIPRE.Cost.Unary × MIPRE.Cost.Prog × ℕ × Bool × ℕ × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Introspection.AuxiliarySource.budget : Cost.PolyTimeFun Context Cost.Unary

Equations

• MIPRE.Introspection.AuxiliarySource.budget = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.AuxiliarySource.source : Cost.PolyTimeFun Context Cost.Prog

Equations

• MIPRE.Introspection.AuxiliarySource.source = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliarySource.index : Cost.PolyTimeFun Context ℕ

Equations

• MIPRE.Introspection.AuxiliarySource.index = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Introspection.AuxiliarySource.player : Cost.PolyTimeFun Context Bool

Equations

• MIPRE.Introspection.AuxiliarySource.player = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Introspection.AuxiliarySource.level : Cost.PolyTimeFun Context ℕ

Equations

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

noncomputable def MIPRE.Introspection.AuxiliarySource.inputPrefix : Cost.PolyTimeFun Context Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.AuxiliarySource.queryInput (kind : ℕ) : Cost.PolyTimeFun (Cost.BitStr × Context) Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.AuxiliarySource.query (U : Cost.ClockedUniversalMachine) (kind : ℕ) : Cost.PolyTimeFun (Cost.BitStr × Context) Cost.Data

Equations

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

theorem MIPRE.Introspection.AuxiliarySource.query_apply (U : Cost.ClockedUniversalMachine) (kind : ℕ) (y : Cost.BitStr) (b : Cost.Unary) (S : Cost.Prog) (n : ℕ) (w : Bool) (j : ℕ) (u : Cost.BitStr) : (query U kind).toFun (y, b, S, n, w, j, u) = Cost.clockedResult S (Cost.encode (n, kind, Player.ofBool w, j, u, y)) (List.length b)

noncomputable def MIPRE.Introspection.AuxiliarySource.linear (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.BitStr × Context) Cost.BitStr

Read a returned bit string; malformed results also terminate.

Equations

• MIPRE.Introspection.AuxiliarySource.linear U = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Introspection.AuxiliarySource.query U 2))

noncomputable def MIPRE.Introspection.AuxiliarySource.factor (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Context Cost.BitStr

Equations

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

theorem MIPRE.Introspection.AuxiliarySource.linear_correct (U : Cost.ClockedUniversalMachine) (y v : Cost.BitStr) (b : Cost.Unary) (S : Cost.Prog) (n : ℕ) (w : Bool) (j : ℕ) (u : Cost.BitStr) (h : Cost.clockedResult S (Cost.encode (n, CL.Sampler.Query.linear (Player.ofBool w) j u y)) (List.length b) = (Cost.encode true).cons (Cost.encode v)) : (linear U).toFun (y, b, S, n, w, j, u) = v

theorem MIPRE.Introspection.AuxiliarySource.factor_correct (U : Cost.ClockedUniversalMachine) (v : Cost.BitStr) (b : Cost.Unary) (S : Cost.Prog) (n : ℕ) (w : Bool) (j : ℕ) (u : Cost.BitStr) (h : Cost.clockedResult S (Cost.encode (n, CL.Sampler.Query.factor (Player.ofBool w) j u)) (List.length b) = (Cost.encode true).cons (Cost.encode v)) : (factor U).toFun (b, S, n, w, j, u) = v

noncomputable def MIPRE.Introspection.AuxiliarySource.matrix (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Context (List Cost.BitStr)

Collect the matrix using a polynomial number of source calls.

Equations

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