Actual cross-introspection source compiler

The program computes the canonical register parameters, calls the original sampler's dimension query at 2^n, validates and unpads both Introspect answers, then calls the original decider at 2^n. Both source calls are clocked. It is total on every raw input, for arbitrary source program texts. This is the cross-Introspect edge component, not the remaining typed dispatch.

noncomputable def MIPRE.Introspection.SourceCompiler.parameterStage (c lam : ℕ) : Cost.Prog

Equations

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

theorem MIPRE.Introspection.SourceCompiler.parameterStage_closed (c lam : ℕ) : Cost.Prog.WellScoped 1 (parameterStage c lam)

theorem MIPRE.Introspection.SourceCompiler.parameterStage_runs (c lam : ℕ) (x : Cost.Data) : ∃ (t : ℕ), (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.dimensionRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

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

Equations

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

theorem MIPRE.Introspection.SourceCompiler.dimensionStage_closed (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) : Cost.Prog.WellScoped 1 (dimensionStage k lam U S)

noncomputable def MIPRE.Introspection.SourceCompiler.dimensionResult (k lam : ℕ) (S : Cost.Prog) (n : ℕ) : Cost.Data

Equations

• MIPRE.Introspection.SourceCompiler.dimensionResult k lam S n = MIPRE.Cost.clockedResult S (MIPRE.Cost.encode (2 ^ n, MIPRE.CL.Sampler.Query.dimension)) (MIPRE.Introspection.ansBound k lam n)

theorem MIPRE.Introspection.SourceCompiler.dimensionStage_runs (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S : Cost.Prog) (x bounds : Cost.Data) : ∃ (t : ℕ), (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.originalInput : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.SourceCompiler.originalInput = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.SourceCompiler.returnedDimension : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.SourceCompiler.returnedDimension = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Introspection.SourceCompiler.finalInput : Cost.PolyTimeFun Cost.Data GuardInput

Equations

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

def MIPRE.Introspection.SourceCompiler.Prepared (x : Cost.Data) : Prop

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.Introspection.SourceCompiler.instDecidablePrepared (x : Cost.Data) : Decidable (Prepared x)

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.finalRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

theorem MIPRE.Introspection.SourceCompiler.finalRoute_apply (x : Cost.Data) : finalRoute.toFun x = if Prepared x then (true, (Cost.encode (finalInput.toFun x)).cons Cost.Data.nil) else (false, Cost.encode false)

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

Equations

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

theorem MIPRE.Introspection.SourceCompiler.finalStage_closed (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) : Cost.Prog.WellScoped 1 (finalStage k lam U D)

theorem MIPRE.Introspection.SourceCompiler.finalStage_halts (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : Cost.Halts (finalStage k lam U D) x

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

The actual three-stage cross-Introspect component.

Equations

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

theorem MIPRE.Introspection.SourceCompiler.crossProg_closed (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) : Cost.Prog.WellScoped 1 (crossProg c k lam U S D)

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