Documentation

MIPRE.Foundations.Introspection.DynamicParser

Uniform introspection tuple parsing with binary bounds #

One fixed program reads its register length and original-answer cutoff in binary. All format and cutoff specifications are exactly those of the fixed parser, but no parameter value is embedded as a unary program constant.

source
noncomputable def MIPRE.Introspection.DynamicParser.fieldOffset :
Cost.PolyTimeFun ℕ ℕ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.DynamicParser.fieldOffset_apply (Q : ℕ) :
    fieldOffset.toFun Q = 2 * Q + 2
    source
    noncomputable def MIPRE.Introspection.DynamicParser.pairParts :
    Cost.PolyTimeFun (Cost.BitStr × ℕ) (Cost.BitStr × Cost.BitStr)

    Candidate pair fields, using the runtime binary register dimension.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.Introspection.DynamicParser.pairParts_apply (bs : Cost.BitStr) (Q : ℕ) :
      pairParts.toFun (bs, Q) = AnswerParser.pairParts Q bs
      source
      noncomputable def MIPRE.Introspection.DynamicParser.tripleParts :
      Cost.PolyTimeFun (Cost.BitStr × ℕ) (Cost.BitStr × Cost.BitStr × Cost.BitStr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.Introspection.DynamicParser.tripleParts_apply (bs : Cost.BitStr) (Q : ℕ) :
        tripleParts.toFun (bs, Q) = AnswerParser.tripleParts Q bs
        source
        noncomputable def MIPRE.Introspection.DynamicParser.pairCheck :
        Cost.PolyTimeFun (Cost.BitStr × ℕ × ℕ) Bool

        Introspect/Sample validation, uniformly in the binary bounds Q and R.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.Introspection.DynamicParser.pairCheck_apply (bs : Cost.BitStr) (Q R : ℕ) :
          pairCheck.toFun (bs, Q, R) = decide (AnswerParser.pairValid Q R bs)
          source
          noncomputable def MIPRE.Introspection.DynamicParser.tripleCheck (exactLast : Bool) :
          Cost.PolyTimeFun (Cost.BitStr × ℕ × ℕ) Bool

          Read or Hide validation, with all numeric parameters supplied in binary.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.Introspection.DynamicParser.tripleCheck_apply (bs : Cost.BitStr) (Q R : ℕ) (exactLast : Bool) :
            (tripleCheck exactLast).toFun (bs, Q, R) = decide (AnswerParser.tripleValid Q R exactLast bs)
            source
            theorem MIPRE.Introspection.DynamicParser.pairCheck_iff (bs : Cost.BitStr) (Q R : ℕ) :
            pairCheck.toFun (bs, Q, R) = true ↔ ∃ (y : Cost.BitStr) (a : Cost.BitStr), List.length y = Q ∧ List.length a ≤ R ∧ bs = AnswerParser.pairBits y a
            source
            theorem MIPRE.Introspection.DynamicParser.tripleCheck_iff (bs : Cost.BitStr) (Q R : ℕ) (exactLast : Bool) :
            (tripleCheck exactLast).toFun (bs, Q, R) = true ↔ ∃ (y : Cost.BitStr) (yp : Cost.BitStr) (a : Cost.BitStr), List.length y = Q ∧ List.length yp = Q ∧ (if exactLast = true then List.length a = R else List.length a ≤ R) ∧ bs = AnswerParser.tripleBits y yp a
            source
            theorem MIPRE.Introspection.DynamicParser.pairCheck_original_cutoff (bs : Cost.BitStr) (Q R : ℕ) (h : pairCheck.toFun (bs, Q, R) = true) :
            List.length (pairParts.toFun (bs, Q)).2 ≤ R
            source
            theorem MIPRE.Introspection.DynamicParser.readCheck_original_cutoff (bs : Cost.BitStr) (Q R : ℕ) (h : (tripleCheck false).toFun (bs, Q, R) = true) :
            List.length (tripleParts.toFun (bs, Q)).2.2 ≤ R