Documentation

MIPRE.Foundations.CL.ProgBuild

Building programs in polynomial time #

A program is data (Prog.toData), so placing variable subprograms in a fixed context is a polynomial-time function of the subprograms: letF for let e in b, elimF for elim i n c, and from them routeOneCallF for a router with one call to a variable program. These are how a verifier's programs are computed from its input programs when the input programs enter as code rather than as data (the detyping compiler's).

source
noncomputable def MIPRE.CL.ProgBuild.letF :
Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog

(e, b) ↦ let e in b, in polynomial time.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.CL.ProgBuild.letF_apply (e b : Cost.Prog) :
    letF.toFun (e, b) = e.let_ b
    source
    noncomputable def MIPRE.CL.ProgBuild.elimF (i : ℕ) (n : Cost.Prog) :
    Cost.PolyTimeFun Cost.Prog Cost.Prog

    c ↦ elim i n c, in polynomial time.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.CL.ProgBuild.elimF_apply (i : ℕ) (n c : Cost.Prog) :
      (elimF i n).toFun c = Cost.Prog.elim i n c
      source
      noncomputable def MIPRE.CL.ProgBuild.callWithContextF (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) :
      Cost.PolyTimeFun Cost.Prog Cost.Prog

      p ↦ callWithContext p post, in polynomial time.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.CL.ProgBuild.callWithContextF_apply (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (p : Cost.Prog) :
        (callWithContextF post).toFun p = p.callWithContext post
        source
        noncomputable def MIPRE.CL.ProgBuild.routeOneCallF (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) :
        Cost.PolyTimeFun Cost.Prog Cost.Prog

        p ↦ routeOneCall route p post, in polynomial time.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.CL.ProgBuild.routeOneCallF_apply (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (p : Cost.Prog) :
          (routeOneCallF route post).toFun p = Cost.Prog.routeOneCall route p post