Documentation

MIPRE.Background.AnswerReduction.AnswerFormat

The answers of the answer-reduced verifier, as bit strings #

Part of piece AR-3c of planning/answer-reduction.md: Table tpcp of ld_compiler.tex, the answer formats of the eighteen PCP types, as bit strings.

An answer is a tuple of field elements of a length the type prescribes (cnt): one value, or the d + 1 or md + 1 coefficients of one polynomial, for the first five copies; m' + 6 values, or m' + 6 polynomials' coefficients, for the sixth. It is written as the list of the elements' k-bit representations, serialized as the postorder bits of its encoding (enc), the format the oracularized verifier already uses for its answer pairs (pairEnc). Reading an answer back (parse) requires the list to decode, every block to have k bits and the count to be the type's; a failed parse is rejected by the typed predicate, which is the format preamble of fig:decider-pcp with its length bounds.

parse_enc is the round trip for an answer of the right format, and length_enc_le the bound on the length of an honest answer: what completeness needs.

The number of field elements of an answer #

source
def MIPRE.AnswerReduction.cnt (P : SAT.PcpParams) (t : Pcp.PcpTy) :
ℕ

The number of field elements in an answer of the PCP type t (Table tpcp).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def MIPRE.AnswerReduction.elems {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) :
    Ans P E.carrier → List E.carrier

    The field elements of an answer, in order: the values, or the coefficients of each polynomial in turn.

    Equations
    Instances For
      source
      def MIPRE.AnswerReduction.ofElems {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) (t : Pcp.PcpTy) (l : List E.carrier) :
      Ans P E.carrier

      An answer of the type t from a list of field elements.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.AnswerReduction.getD_ofFn {k : ℕ} (E : SAT.BinField k) {n : ℕ} (g : Fin n → E.carrier) (i : Fin n) :
        (List.ofFn g).getD (↑i) 0 = g i
        source
        theorem MIPRE.AnswerReduction.length_elems {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) {t : Pcp.PcpTy} {a : Ans P E.carrier} (h : ansFmt t a = true) :
        (elems E a).length = cnt P t
        source
        theorem MIPRE.AnswerReduction.ofElems_elems {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) {t : Pcp.PcpTy} {a : Ans P E.carrier} (h : ansFmt t a = true) :
        ofElems E t (elems E a) = a

        Reading the elements back gives the answer, for an answer of the right format.

        Bit strings #

        source
        def MIPRE.AnswerReduction.enc {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) (a : Ans P E.carrier) :
        Cost.BitStr

        The honest encoding of an answer: its elements' k-bit blocks, serialized.

        Equations
        Instances For
          source
          def MIPRE.AnswerReduction.parse {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) (t : Pcp.PcpTy) (s : Cost.BitStr) :
          Option (Ans P E.carrier)

          The bounded parse of an answer of the type t: a serialized list of cnt t blocks of k bits.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.AnswerReduction.parse_enc {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) {t : Pcp.PcpTy} {a : Ans P E.carrier} (h : ansFmt t a = true) :
            parse E t (enc E a) = some a

            The round trip: an answer of the right format parses back from its encoding.

            source
            theorem MIPRE.AnswerReduction.ansFmt_of_parse {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) {t : Pcp.PcpTy} {s : Cost.BitStr} {a : Ans P E.carrier} (h : parse E t s = some a) :
            ansFmt t a = true

            An answer parsed at the type t has the right format.

            source
            theorem MIPRE.AnswerReduction.length_enc_le {P : SAT.PcpParams} {k : ℕ} (E : SAT.BinField k) (a : Ans P E.carrier) :
            List.length (enc E a) ≤ 4 * (k * (elems E a).length) + 4 * (elems E a).length + 1