Documentation

MIPRE.Foundations.SAT.PcpFormat

Executable specification and view checks for the classical PCP #

source
noncomputable def MIPRE.SAT.andProg :
Cost.PolyTimeFun (Bool × Bool) Bool
Equations
Instances For
    source
    theorem MIPRE.SAT.fold_and (l : List Bool) (a : Bool) :
    List.foldl (fun (b c : Bool) => b && c) a l = (a && l.all id)
    source
    theorem MIPRE.SAT.esize_bool_le (b : Bool) :
    Cost.esize b ≤ 3
    source
    noncomputable def MIPRE.SAT.allBoolProg :
    Cost.PolyTimeFun (List Bool) Bool

    Test all supplied bits without interpreting their number as a binary magnitude.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.SAT.allBoolProg_apply (l : List Bool) :
      allBoolProg.toFun l = l.all id
      source
      noncomputable def MIPRE.SAT.widthsProg :
      Cost.PolyTimeFun (ℕ × List Cost.BitStr) Bool

      Check a list of coefficient widths against a binary-specified field degree.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.SAT.widthsProg_apply (p : ℕ × List Cost.BitStr) :
        widthsProg.toFun p = p.2.all fun (b : Cost.BitStr) => decide (List.length b = p.1)
        source
        theorem MIPRE.SAT.widthsProg_true_iff (p : ℕ × List Cost.BitStr) :
        widthsProg.toFun p = true ↔ ∀ b ∈ p.2, List.length b = p.1
        source
        def MIPRE.SAT.validBool (p : DescInput) :
        Bool

        The five finite conditions making a decider specification valid.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.SAT.validProg :
          Cost.PolyTimeFun DescInput Bool

          Uniform specification checking, including the actual encoded program size.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.SAT.validProg_apply (p : DescInput) :
            validProg.toFun p = validBool p
            source
            theorem MIPRE.SAT.validProg_true_iff (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) :
            validProg.toFun ((D, n, T, Q, σ), x, y) = true ↔ Valid D n T Q σ x y
            source
            noncomputable def MIPRE.SAT.viewFormatProg :
            Cost.PolyTimeFun ((ℕ × ℕ) × List Cost.BitStr × List Cost.BitStr) Bool

            Check both coordinate-list lengths and every field coefficient width. The first input pair supplies the binary degree and outer dimension.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MIPRE.SAT.viewFormatProg_true_iff (P : PcpParams) (z ev : List Cost.BitStr) :
              viewFormatProg.toFun ((P.k, P.m'), z, ev) = true ↔ ViewFormat P z ev