Uniformly bounded source descriptions for polynomial-time compilers

The compiler accepts arbitrary source descriptions. Each description exceeding the supplied binary parameter is replaced by a fixed program before compilation. This leaves every bounded verifier unchanged and gives a uniform polynomial output-size bound in the parameter, including at zero.

@[reducible, inline]

abbrev MIPRE.Introspection.SourceDescriptionCompiler.Input : Type

Equations

• MIPRE.Introspection.SourceDescriptionCompiler.Input = ((MIPRE.Cost.Prog × MIPRE.Cost.Prog) × ℕ)

noncomputable def MIPRE.Introspection.SourceDescriptionCompiler.programSize : Cost.PolyTimeFun Cost.Prog ℕ

Actual program encoding size, computed in binary after a linear-size count.

Equations

• MIPRE.Introspection.SourceDescriptionCompiler.programSize = MIPRE.Cost.PolyTimeFun.unaryToBin.comp (MIPRE.Cost.PolyTimeFun.encodedSizeU MIPRE.Cost.Prog)

@[simp]

theorem MIPRE.Introspection.SourceDescriptionCompiler.programSize_apply (p : Cost.Prog) : programSize.toFun p = Cost.esize p

noncomputable def MIPRE.Introspection.SourceDescriptionCompiler.clampProgram : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

Only an oversized description is replaced. The cutoff stays binary.

Equations

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

@[simp]

theorem MIPRE.Introspection.SourceDescriptionCompiler.clampProgram_apply (p : Cost.Prog) (lam : ℕ) : clampProgram.toFun (p, lam) = if Cost.esize p ≤ lam then p else Cost.Prog.nil

noncomputable def MIPRE.Introspection.SourceDescriptionCompiler.clamp : Cost.PolyTimeFun Input Input

Clamp sampler and decider independently while retaining the parameter.

Equations

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

@[simp]

theorem MIPRE.Introspection.SourceDescriptionCompiler.clamp_apply (S D : Cost.Prog) (lam : ℕ) : clamp.toFun ((S, D), lam) = ((clampProgram.toFun (S, lam), clampProgram.toFun (D, lam)), lam)

theorem MIPRE.Introspection.SourceDescriptionCompiler.clamp_eq_self (S D : Cost.Prog) (lam : ℕ) (hS : Cost.esize S ≤ lam) (hD : Cost.esize D ≤ lam) : clamp.toFun ((S, D), lam) = ((S, D), lam)

theorem MIPRE.Introspection.SourceDescriptionCompiler.clamp_bounded {ℓ lam : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) : clamp.toFun ((V.sampler.prog, V.decider.prog), lam) = ((V.sampler.prog, V.decider.prog), lam)

The verifier's size clause is exactly the preservation premise.

theorem MIPRE.Introspection.SourceDescriptionCompiler.clampProgram_size (p : Cost.Prog) (lam : ℕ) : Cost.esize (clampProgram.toFun (p, lam)) ≤ lam + 5

theorem MIPRE.Introspection.SourceDescriptionCompiler.clamp_size (S D : Cost.Prog) (lam : ℕ) : Cost.esize (clamp.toFun ((S, D), lam)) ≤ 13 * (lam + 1)

The entire clamped compiler input has size linear in λ+1, even at zero.

noncomputable def MIPRE.Introspection.SourceDescriptionCompiler.compiler {β : Type u_1} [Cost.SizedEncoding β] (F : Cost.PolyTimeFun Input β) : Cost.PolyTimeFun Input β

The final transformation is itself a single polynomial-time function.

Equations

• MIPRE.Introspection.SourceDescriptionCompiler.compiler F = F.comp MIPRE.Introspection.SourceDescriptionCompiler.clamp

theorem MIPRE.Introspection.SourceDescriptionCompiler.compiler_size_le_eval {β : Type u_1} [Cost.SizedEncoding β] (F : Cost.PolyTimeFun Input β) (S D : Cost.Prog) (lam : ℕ) : Cost.esize ((compiler F).toFun ((S, D), lam)) ≤ Polynomial.eval (13 * (lam + 1)) F.timeBound

The output polynomial uses only the fixed compiler and the parameter.

theorem MIPRE.Introspection.SourceDescriptionCompiler.exists_compiler_size {β : Type u_1} [Cost.SizedEncoding β] (F : Cost.PolyTimeFun Input β) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (S D : Cost.Prog) (lam : ℕ), Cost.esize ((compiler F).toFun ((S, D), lam)) ≤ C * (lam + 1) ^ C

A single constant absorbs the compiler's coefficient sum and degree. There is no lower-bound assumption on the supplied parameter.