The actual compiled introspection decider

Compilation clamps each source description, specializes the fixed prepared kernel using binary metadata, and adds zero-parameter and zero-index branches. The positive branch computes its clock and canonical resources exactly once.

noncomputable def MIPRE.Introspection.DecisionCompiler.positiveCompiler (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun DecisionPreparation.Metadata Cost.Prog

Equations

• MIPRE.Introspection.DecisionCompiler.positiveCompiler c U = MIPRE.Introspection.DecisionPreparation.compiler c (MIPRE.Introspection.DecisionCompiler.untypedKernel U)

noncomputable def MIPRE.Introspection.DecisionCompiler.typedDecider (c : ℕ) (U : Cost.ClockedUniversalMachine) (M : DecisionPreparation.Metadata) : CL.Detyping.TypedDecider DecisionKernel.Label

Equations

• MIPRE.Introspection.DecisionCompiler.typedDecider c U M = { prog := (MIPRE.Introspection.DecisionPreparation.compiler c (MIPRE.Introspection.DecisionKernel.program U)).toFun M, closed := ⋯ }

theorem MIPRE.Introspection.DecisionCompiler.typedDecider_total (c : ℕ) (U : Cost.ClockedUniversalMachine) (M : DecisionPreparation.Metadata) : (typedDecider c U M).Total

theorem MIPRE.Introspection.DecisionCompiler.typedDecider_accepts (c : ℕ) (U : Cost.ClockedUniversalMachine) (M : DecisionPreparation.Metadata) (n : ℕ) (T W : DecisionKernel.Label) (x y a b : Cost.BitStr) : (typedDecider c U M).Accepts n T x W y a b ↔ (DecisionKernel.program U).toFun (DecisionPreparation.kernelInput c M (Cost.encode (n, T, x, W, y, a, b))) = true

noncomputable def MIPRE.Introspection.DecisionCompiler.selectedCompiler (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun DecisionPreparation.Metadata Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.DecisionCompiler.compute (c : ℕ) (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun DecisionPreparation.Metadata Cost.Prog

Both the transformation and its source-description clamp are executable polynomial-time functions on the binary compiler input.

Equations

• MIPRE.Introspection.DecisionCompiler.compute c U = MIPRE.Introspection.SourceDescriptionCompiler.compiler (MIPRE.Introspection.DecisionCompiler.selectedCompiler c U)

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.selectedCompiler_apply (c : ℕ) (U : Cost.ClockedUniversalMachine) (M : DecisionPreparation.Metadata) : (selectedCompiler c U).toFun M = if M.2 = 0 then zeroProg else zeroWrap ((positiveCompiler c U).toFun M)

theorem MIPRE.Introspection.DecisionCompiler.compute_apply (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam : ℕ) : (compute c U).toFun ((S, D), lam) = if lam = 0 then zeroProg else zeroWrap ((positiveCompiler c U).toFun (SourceDescriptionCompiler.clamp.toFun ((S, D), lam)))

theorem MIPRE.Introspection.DecisionCompiler.compute_closed (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam : ℕ) : Cost.Prog.WellScoped 1 ((compute c U).toFun ((S, D), lam))

noncomputable def MIPRE.Introspection.DecisionCompiler.decider (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam : ℕ) : Decider

Equations

• MIPRE.Introspection.DecisionCompiler.decider c U S D lam = { prog := (MIPRE.Introspection.DecisionCompiler.compute c U).toFun ((S, D), lam), closed := ⋯ }

theorem MIPRE.Introspection.DecisionCompiler.positive_runs (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (d : Cost.Data) : ∃ (t : ℕ), (decider c U S D lam).prog.Runs ((Cost.encode n).cons d) (Cost.encode ((untypedKernel U).toFun (DecisionPreparation.kernelInput c (SourceDescriptionCompiler.clamp.toFun ((S, D), lam)) ((Cost.encode n).cons d)))) t

theorem MIPRE.Introspection.DecisionCompiler.zero_runs (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam n : ℕ) (h : lam = 0 ∨ n = 0) (d : Cost.Data) : ∃ (t : ℕ), (decider c U S D lam).prog.Runs ((Cost.encode n).cons d) (Cost.encode (zeroTest.toFun d)) t

theorem MIPRE.Introspection.DecisionCompiler.accepts_positive (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) : (decider c U S D lam).Accepts n x y a b ↔ (untypedKernel U).toFun (DecisionPreparation.kernelInput c (SourceDescriptionCompiler.clamp.toFun ((S, D), lam)) (Cost.encode (n, x, y, a, b))) = true

theorem MIPRE.Introspection.DecisionCompiler.accepts_zero (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam n : ℕ) (h : lam = 0 ∨ n = 0) (x y a b : Cost.BitStr) : (decider c U S D lam).Accepts n x y a b ↔ x = [] ∧ y = [] ∧ List.length a ≤ 2 ∧ List.length b ≤ 2

def MIPRE.Introspection.DecisionCompiler.cutoffAt (c lam n : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.DecisionCompiler.accepts_positive_bounds (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) (h : (decider c U S D lam).Accepts n x y a b) : List.length x = CL.Detyping.graphDim DecisionKernel.Label + (3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n ∧ List.length y = CL.Detyping.graphDim DecisionKernel.Label + (3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n ∧ List.length a ≤ answerBound (SourceCompiler.registerBits c lam n) (SourceCompiler.originalBound lam n) ∧ List.length b ≤ answerBound (SourceCompiler.registerBits c lam n) (SourceCompiler.originalBound lam n)

theorem MIPRE.Introspection.DecisionCompiler.accepts_cutoff (c : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (lam n : ℕ) (x y a b : Cost.BitStr) (h : (decider c U S D lam).Accepts n x y a b) : List.length a ≤ cutoffAt c lam n ∧ List.length b ≤ cutoffAt c lam n

theorem MIPRE.Introspection.DecisionCompiler.cutoffAt_ansBound {c : ℕ} (hc : 1 ≤ c) : ∃ (K : ℕ), ∀ (lam n : ℕ), cutoffAt c lam n ≤ ansBound K lam n

theorem MIPRE.Introspection.DecisionCompiler.compute_size (c : ℕ) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (S D : Cost.Prog) (lam : ℕ), (decider c U S D lam).size ≤ C * (lam + 1) ^ C