Documentation

MIPRE.Foundations.Introspection.DecisionPreparationCost

Uniform costs for one shared introspection resource preparation #

source
theorem MIPRE.Introspection.DecisionPreparation.esize_two_pow_le (n : ℕ) :
Cost.esize (2 ^ n) ≤ 4 * n + 5
source
noncomputable def MIPRE.Introspection.DecisionPreparation.boundsMajorant (c v : ℕ) :
ℕ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.DecisionPreparation.boundsCost_le_majorant {c lam n v : ℕ} (hc : 1 ≤ c) (hl : lam ≤ v) (hn : n ≤ v) (hu : lam * n ≤ v) :
    SourceCompiler.boundsCost c lam n ≤ boundsMajorant c v
    source
    theorem MIPRE.Introspection.DecisionPreparation.boundsMajorant_polyBounded (c : ℕ) :
    Cost.PolyBounded (boundsMajorant c)
    source
    noncomputable def MIPRE.Introspection.DecisionPreparation.appendPoly (arg : Cost.PolyTimeFun Cost.Data Cost.Data) (p q : Polynomial ℕ) :
    Polynomial ℕ

    Cost of appending a result, with input and subroutine costs bounded by fixed polynomials of the same resource parameter.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.DecisionPreparation.appendStage_runs_poly (arg : Cost.PolyTimeFun Cost.Data Cost.Data) {code : Cost.Prog} (hcode : Cost.Prog.WellScoped 1 code) (p q : Polynomial ℕ) (v : ℕ) (x r : Cost.Data) (hx : x.size ≤ Polynomial.eval v p) (t : ℕ) (ht : t ≤ Polynomial.eval v q) (hr : code.Runs (arg.toFun x) r t) :
      ∃ time ≤ Polynomial.eval v (appendPoly arg p q), (appendStage arg code).Runs x (x.cons r) time
      source
      noncomputable def MIPRE.Introspection.DecisionPreparation.clockPoly :
      Polynomial ℕ
      Equations
      Instances For
        source
        noncomputable def MIPRE.Introspection.DecisionPreparation.pauliPoly (c : ℕ) :
        Polynomial ℕ
        Equations
        Instances For
          source
          noncomputable def MIPRE.Introspection.DecisionPreparation.boundsPoly (c : ℕ) :
          Polynomial ℕ
          Equations
          Instances For
            source
            noncomputable def MIPRE.Introspection.DecisionPreparation.firstPoly :
            Polynomial ℕ
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MIPRE.Introspection.DecisionPreparation.secondPoly :
              Polynomial ℕ
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def MIPRE.Introspection.DecisionPreparation.thirdPoly (c : ℕ) :
                Polynomial ℕ
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.DecisionPreparation.fourthPoly (c : ℕ) :
                  Polynomial ℕ
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.DecisionPreparation.preparationPoly (c : ℕ) :
                    Polynomial ℕ
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem MIPRE.Introspection.DecisionPreparation.finish_boundsResult (c : ℕ) (z : Cost.Data) :
                      finish.toFun (boundsResult c z) = Cost.encode (resources c z)
                      source
                      theorem MIPRE.Introspection.DecisionPreparation.prog_runs_poly {c v : ℕ} (hc : 1 ≤ c) (z : Cost.Data) (hl : 1 ≤ inputLambda.toFun z) (hn : 1 ≤ inputIndex.toFun z) (hz : z.size ≤ v) (hB : ansBound 5 (inputLambda.toFun z) (inputIndex.toFun z) ≤ v) :
                      ∃ time ≤ Polynomial.eval v (preparationPoly c), (prog c).Runs z (Cost.encode (resources c z)) time

                      All preparation work is polynomial in a common bound for the original input and the one shared clock. The theorem keeps zero parameters separate.

                      source
                      noncomputable def MIPRE.Introspection.DecisionPreparation.kernelPoly (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) :
                      Polynomial ℕ
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def MIPRE.Introspection.DecisionPreparation.compiledPoly (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) :
                        Polynomial ℕ
                        Equations
                        Instances For
                          source
                          theorem MIPRE.Introspection.DecisionPreparation.kernelProg_runs_poly {c v : ℕ} (hc : 1 ≤ c) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) (x : Cost.Data) (hl : 1 ≤ M.2) (hn : 1 ≤ ClockSimulation.indexReader.toFun x) (hz : Cost.esize M + x.size + 1 ≤ v) (hB : ansBound 5 M.2 (ClockSimulation.indexReader.toFun x) ≤ v) :
                          ∃ time ≤ Polynomial.eval v (kernelPoly c kernel), (kernelProg c kernel).Runs ((Cost.encode M).cons x) (Cost.encode (kernel.toFun (kernelInput c M x))) time
                          source
                          theorem MIPRE.Introspection.DecisionPreparation.compiler_runs_poly {c v : ℕ} (hc : 1 ≤ c) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) (x : Cost.Data) (hl : 1 ≤ M.2) (hn : 1 ≤ ClockSimulation.indexReader.toFun x) (hz : Cost.esize M + x.size + 1 ≤ v) (hB : ansBound 5 M.2 (ClockSimulation.indexReader.toFun x) ≤ v) :
                          ∃ time ≤ Polynomial.eval v (compiledPoly c kernel), ((compiler c kernel).toFun M).Runs x (Cost.encode (kernel.toFun (kernelInput c M x))) time

                          The actual binary compiler has only additive metadata-specialization overhead beyond the prepared, fixed polynomial-time kernel.