Documentation

MIPRE.Foundations.Pipeline.Budget

Resource budgets of a verifier at one index #

The four transformations of chapter 6 of the blueprint (introspection, oracularization, answer reduction, parallel repetition) each take a normal form verifier and return one, and each states its complexity as bounds on the output in terms of bounds on the input: the paper's TIME_𝒮(n), TIME_𝒟(n), the dimension s(n) and the timeout bound B_𝒟(n) of a decider in timeout-counter form. In the ambient cost model these are five numbers per index (MIPRE.Verifier explains the degree): the running-time coefficients of the sampler and the decider, their common degree in the size of the input, a bound on the dimension of the questions, and a length of answers beyond which the decider rejects (Verifier.RejectsLong, the ambient reading of "the decider first parses its answers against B_𝒟(n)"). Budget collects them and Verifier.Within V n R says V respects R at index n.

Nothing here has content: it is the vocabulary in which the hypothesis structures of MIPRE.Foundations.Pipeline state their complexity clauses, so that the composition MIPRE.GapCompression.ofPipeline can chain them.

source
structure MIPRE.Budget :
Type

A resource budget at one index: a bound S on the sampler's running-time coefficient, d on the dimension of its questions, D on the decider's running-time coefficient, k on the degree of both running times in the size of the input, and B on the length of the answers the decider can accept.

  • S : ℕ

    Sampler running-time coefficient (TIME_𝒮(n)).

  • d : ℕ

    Dimension of the questions (s(n)).

  • D : ℕ

    Decider running-time coefficient (TIME_𝒟(n)).

  • k : ℕ

    Degree of both running times in the size of the input.

  • B : ℕ

    Length beyond which the decider rejects an answer (B_𝒟(n)).

Instances For
    source
    def MIPRE.Budget.uniform (z k : ℕ) :
    Budget

    The budget with the same bound z on every quantity, at degree k.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Budget.uniform_S (z k : ℕ) :
      (uniform z k).S = z
      source
      @[simp]
      theorem MIPRE.Budget.uniform_d (z k : ℕ) :
      (uniform z k).d = z
      source
      @[simp]
      theorem MIPRE.Budget.uniform_D (z k : ℕ) :
      (uniform z k).D = z
      source
      @[simp]
      theorem MIPRE.Budget.uniform_k (z k : ℕ) :
      (uniform z k).k = k
      source
      @[simp]
      theorem MIPRE.Budget.uniform_B (z k : ℕ) :
      (uniform z k).B = z
      source
      def MIPRE.Budget.Le (R R' : Budget) :
      Prop

      Pointwise comparison of budgets.

      Equations
      Instances For
        source
        theorem MIPRE.Budget.Le.refl (R : Budget) :
        R.Le R
        source
        def MIPRE.Verifier.Within {ℓ : ℕ} (V : Verifier ℓ) (n : ℕ) (R : Budget) :
        Prop

        V respects the budget R at index n: its sampler runs within R.S at degree R.k, its questions have dimension at most R.d, its decider runs within R.D at degree R.k, and its decider rejects every answer longer than R.B.

        Equations
        Instances For
          source
          theorem MIPRE.Verifier.RejectsLong.mono {ℓ : ℕ} {V : Verifier ℓ} {n T T' : ℕ} (hT : T ≤ T') (h : V.RejectsLong n T) :
          V.RejectsLong n T'
          source
          theorem MIPRE.Verifier.Within.mono {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R R' : Budget} (h : V.Within n R) (hle : R.Le R') :
          V.Within n R'
          source
          theorem MIPRE.Verifier.Within.sampler_time {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R : Budget} (h : V.Within n R) :
          V.sampler.TimeBoundAt n R.S R.k
          source
          theorem MIPRE.Verifier.Within.sampler_dim {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R : Budget} (h : V.Within n R) :
          V.sampler.dim n ≤ R.d
          source
          theorem MIPRE.Verifier.Within.decider_time {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R : Budget} (h : V.Within n R) :
          V.decider.TimeBoundAt n R.D R.k
          source
          theorem MIPRE.Verifier.Within.rejectsLong {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R : Budget} (h : V.Within n R) :
          V.RejectsLong n R.B
          source
          theorem MIPRE.Verifier.Within.val_eq {ℓ : ℕ} {V : Verifier ℓ} (ω : ValueModel) {n : ℕ} {R : Budget} (h : V.Within n R) {T : ℕ} (hT : R.B ≤ T) :
          V.val ω n T = V.val ω n R.B

          A verifier respecting a budget has, at any larger answer bound, the same value in every model as at the budget's answer bound.

          source
          theorem MIPRE.Verifier.Within.valStar_eq {ℓ : ℕ} {V : Verifier ℓ} {n : ℕ} {R : Budget} (h : V.Within n R) {T : ℕ} (hT : R.B ≤ T) :
          V.valStar n T = V.valStar n R.B

          A verifier respecting a budget has, at any larger answer bound, the same value as at the budget's answer bound.