Binary-uniform compilation of the cross-Introspect component

noncomputable def MIPRE.Introspection.SourceCompiler.parameterStageCompiler (c : ℕ) : Cost.PolyTimeFun ℕ Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.dimensionStageCompiler (k : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.finalStageCompiler (k : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.crossCompiler (c k : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.Prog × Cost.Prog × ℕ) Cost.Prog

One fixed ambient compiler reads both source descriptions and binary lambda.

Equations

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

theorem MIPRE.Introspection.SourceCompiler.crossCompiler_apply (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) : (crossCompiler c k U).toFun (S, D, lam) = crossProg c k lam U S D

theorem MIPRE.Introspection.SourceCompiler.crossCompiler_binary_bounds (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) : Cost.esize (crossProg c k lam U S D) ≤ Polynomial.eval (Cost.esize S + Cost.esize D + 4 * lam.size + 3) (crossCompiler c k U).timeBound ∧ ∃ t ≤ Polynomial.eval (Cost.esize S + Cost.esize D + 4 * lam.size + 3) (crossCompiler c k U).timeBound, (crossCompiler c k U).code.Runs (Cost.encode (S, D, lam)) (Cost.encode (crossProg c k lam U S D)) t