Composed execution cost of the actual source component

This accounts for parameter generation, the clocked sampler dimension query, format checks, source-question unpadding, and the clocked original decider. The bound applies to all raw inputs and arbitrary source program texts.

def MIPRE.Introspection.SourceCompiler.callCost (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (x a ctx : Cost.Data) (T : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.call_runs_cost (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (x a ctx r : Cost.Data) (T t : ℕ) (ht : t ≤ T) (hroute : route.toFun x = (true, a.cons ctx)) (hr : p.Runs a r t) : ∃ time ≤ callCost route post x a ctx T, (Cost.Prog.routeOneCall route p post).Runs x (post.toFun (ctx, r)) time

noncomputable def MIPRE.Introspection.SourceCompiler.conditionalCost (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (x a : Cost.Data) (T : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.conditionalCost route x a T = MIPRE.Introspection.SourceCompiler.callCost route MIPRE.Cost.PolyTimeFun.snd x a MIPRE.Cost.Data.nil T + 5

theorem MIPRE.Introspection.SourceCompiler.conditional_haltsWithin (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (x a : Cost.Data) (T : ℕ) (ready : Prop) [Decidable ready] (hroute : route.toFun x = if ready then (true, a.cons Cost.Data.nil) else (false, Cost.encode false)) (hr : Cost.HaltsWithin p a T) : Cost.HaltsWithin (Cost.Prog.routeOneCall route p Cost.PolyTimeFun.snd) x (conditionalCost route x a T)

noncomputable def MIPRE.Introspection.SourceCompiler.projectedCost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.projectedProg_haltsWithin (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : Cost.HaltsWithin (projectedProg (ClockSimulation.decider k lam U D).prog) x (projectedCost k lam U D x)

noncomputable def MIPRE.Introspection.SourceCompiler.finalCost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.finalStage_haltsWithin (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : Cost.HaltsWithin (finalStage k lam U D) x (finalCost k lam U D x)

noncomputable def MIPRE.Introspection.SourceCompiler.rawSimulationCost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.rawSimulation_runs_cost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x : Cost.Data) : ∃ time ≤ rawSimulationCost k lam U S x, (ClockSimulation.prog k lam U S).Runs x (Cost.clockedResult S (ClockSimulation.reindexed x) (ansBound k lam (ClockSimulation.indexReader.toFun x))) time

noncomputable def MIPRE.Introspection.SourceCompiler.parameterCost (c lam : ℕ) (x : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.parameterStage_runs_cost (c lam : ℕ) (x : Cost.Data) : ∃ t ≤ parameterCost c lam x, (parameterStage c lam).Runs x (x.cons (Cost.encode (registerBits c lam (ClockSimulation.indexReader.toFun x), originalBound lam (ClockSimulation.indexReader.toFun x)))) t

noncomputable def MIPRE.Introspection.SourceCompiler.dimensionCost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x bounds : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.dimensionStage_runs_cost (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x bounds : Cost.Data) : ∃ t ≤ dimensionCost k lam U S x bounds, (dimensionStage k lam U S).Runs (x.cons bounds) ((x.cons bounds).cons (dimensionResult k lam S (ClockSimulation.indexReader.toFun x))) t

noncomputable def MIPRE.Introspection.SourceCompiler.crossCost (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (x : Cost.Data) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.crossProg_haltsWithin (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (x : Cost.Data) : Cost.HaltsWithin (crossProg c k lam U S D) x (crossCost c k lam U S D x)

A compositional cost bound for every raw input, without source halting assumptions.