Documentation

MIPRE.TM.CookLevin.PcpPrepare

Preparing the exact circuit from a PCP view #

The point list supplies the unary output budget. Thus constructing the circuit is globally polynomial in the actual verifier input, even when the binary parameter values would demand a much larger correctly formatted view.

source
noncomputable def MIPRE.TM.CookLevin.Pad.inputCountU :
Cost.PolyTimeFun ParamInput Cost.Unary

Number of input coordinates, in unary, without expanding a binary gate count.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.TM.CookLevin.Pad.inputCountU_length (p : ParamInput) :
    List.length (inputCountU.toFun p) = 5 * innerDim p.2.1 p.2.2.2 + 5
    source
    noncomputable def MIPRE.TM.CookLevin.Pad.gateBudgetProg :
    Cost.PolyTimeFun SAT.PcpInput Cost.Unary

    The point's gate-coordinate tail determines the circuit-printing budget.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.TM.CookLevin.Pad.gateBudgetProg_length (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) :
      List.length (gateBudgetProg.toFun (SAT.pcpInput D n T Q σ x y z ev)) = z.length - (5 * innerDim T σ + 5)
      source
      theorem MIPRE.TM.CookLevin.Pad.gateBudgetProg_exact (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) (hf : SAT.ViewFormat (pcpParams n T Q σ) z ev) :
      List.length (gateBudgetProg.toFun (SAT.pcpInput D n T Q σ x y z ev)) = gateCount n T Q σ
      source
      noncomputable def MIPRE.TM.CookLevin.Pad.pcpCircuitProg :
      Cost.PolyTimeFun SAT.PcpInput SAT.Circuit

      The verifier's uniform circuit constructor, using the supplied view budget.

      Equations
      Instances For
        source
        theorem MIPRE.TM.CookLevin.Pad.pcpCircuitProg_apply (p : SAT.PcpInput) :
        pcpCircuitProg.toFun p = describeExact.toFun (p.1, gateBudgetProg.toFun p)
        source
        theorem MIPRE.TM.CookLevin.Pad.pcpCircuitProg_eq_fixed (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) (hf : SAT.ViewFormat (pcpParams n T Q σ) z ev) :
        pcpCircuitProg.toFun (SAT.pcpInput D n T Q σ x y z ev) = describeExact.toFun (((D, n, T, Q, σ), x, y), Cost.unary (gateCount n T Q σ))

        For a correctly formatted view, the constructor is independent of the coordinate values and equals the fixed exact-size describer for the specification.

        source
        theorem MIPRE.TM.CookLevin.Pad.fieldDegreeU_apply (p : ParamInput) :
        fieldDegreeU.toFun p = Cost.unary (pcpParams p.1 p.2.1 p.2.2.1 p.2.2.2).k