The fixed-depth polynomial-time Gaussian scan program

The source depth is a compiler constant (seven in introspection). Each stage is a composition of actual polynomial-time programs. A failed stage stops all subsequent source queries. The register width comes from the actual claimed answer, so malformed data never causes a binary-sized allocation.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryScan.Input : Type

Equations

• MIPRE.Introspection.AuxiliaryScan.Input = (MIPRE.Introspection.AuxiliarySource.Context × MIPRE.Cost.BitStr)

def MIPRE.Introspection.AuxiliaryScan.contextAt (ctx : AuxiliarySource.Context) (j : ℕ) (u : Cost.BitStr) : AuxiliarySource.Context

Equations

• MIPRE.Introspection.AuxiliaryScan.contextAt ctx j u = (ctx.1, ctx.2.1, ctx.2.2.1, ctx.2.2.2.1, j, u)

noncomputable def MIPRE.Introspection.AuxiliaryScan.nextContext (k : ℕ) : Cost.PolyTimeFun (Input × State) AuxiliarySource.Context

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryScan.advance (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) : Cost.PolyTimeFun (Input × State) State

Equations

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

theorem MIPRE.Introspection.AuxiliaryScan.advance_apply (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) (ctx : AuxiliarySource.Context) (y : Cost.BitStr) (b : Bool) (u x : Cost.BitStr) : (advance f m k).toFun ((ctx, y), b, u, x) = if b = true then (stage f m).toFun (contextAt ctx (k + 1) u, y, x) else (false, [], [])

noncomputable def MIPRE.Introspection.AuxiliaryScan.zeros : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryScan.zeros = (MIPRE.Cost.PolyTimeFun.const false).map

theorem MIPRE.Introspection.AuxiliaryScan.zeros_toBits {n : ℕ} (y : Fin n → CL.𝔽₂) : zeros.toFun (CL.toBits y) = CL.toBits 0

def MIPRE.Introspection.AuxiliaryScan.program (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) : ℕ → Cost.PolyTimeFun Input State

Equations

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

theorem MIPRE.Introspection.AuxiliaryScan.program_zero (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) (y : Cost.BitStr) : (program f m 0).toFun (ctx, y) = (true, zeros.toFun y, zeros.toFun y)

theorem MIPRE.Introspection.AuxiliaryScan.program_succ (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) (ctx : AuxiliarySource.Context) (y : Cost.BitStr) : (program f m (k + 1)).toFun (ctx, y) = (advance f m k).toFun ((ctx, y), (program f m k).toFun (ctx, y))