Documentation

MIPRE.Background.Introspection.DecisionCompilerZero

Constant-resource branches of the introspection decider #

At zero parameter or index, the sampler has dimension zero. These branches inspect the answer payload without copying the index or source metadata.

source
noncomputable def MIPRE.Introspection.DecisionCompiler.zeroFields :
Cost.PolyTimeFun Cost.Data (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.DecisionCompiler.zeroTest :
    Cost.PolyTimeFun Cost.Data Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.DecisionCompiler.zeroTest_encode (x y a b : Cost.BitStr) :
      zeroTest.toFun (Cost.encode (x, y, a, b)) = true ↔ x = [] ∧ y = [] ∧ List.length a ≤ 2 ∧ List.length b ≤ 2
      source
      noncomputable def MIPRE.Introspection.DecisionCompiler.zeroProg :
      Cost.Prog

      Ignore the index in place and inspect only the payload.

      Equations
      Instances For
        source
        theorem MIPRE.Introspection.DecisionCompiler.zeroProg_closed :
        Cost.Prog.WellScoped 1 zeroProg
        source
        theorem MIPRE.Introspection.DecisionCompiler.zeroProg_runs (n d : Cost.Data) :
        ∃ t ≤ Polynomial.eval d.size zeroTest.timeBound + d.size + 3, zeroProg.Runs (n.cons d) (Cost.encode (zeroTest.toFun d)) t
        source
        noncomputable def MIPRE.Introspection.DecisionCompiler.zeroWrap (p : Cost.Prog) :
        Cost.Prog

        Test the encoded index before entering a program containing source metadata.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.Introspection.DecisionCompiler.zeroWrap_closed {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) :
          Cost.Prog.WellScoped 1 (zeroWrap p)
          source
          theorem MIPRE.Introspection.DecisionCompiler.zeroWrap_runs_zero (p : Cost.Prog) (d : Cost.Data) :
          ∃ t ≤ Polynomial.eval d.size zeroTest.timeBound + d.size + 4, (zeroWrap p).Runs ((Cost.encode 0).cons d) (Cost.encode (zeroTest.toFun d)) t
          source
          theorem MIPRE.Introspection.DecisionCompiler.zeroWrap_runs_pos {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) {n : ℕ} (hn : 1 ≤ n) (d r : Cost.Data) (t : ℕ) (hr : p.Runs ((Cost.encode n).cons d) r t) :
          (zeroWrap p).Runs ((Cost.encode n).cons d) r (t + ((Cost.encode n).cons d).size + 4)
          source
          noncomputable def MIPRE.Introspection.DecisionCompiler.zeroWrapCompiler :
          Cost.PolyTimeFun Cost.Prog Cost.Prog
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.Introspection.DecisionCompiler.zeroWrapCompiler_apply (p : Cost.Prog) :
            zeroWrapCompiler.toFun p = zeroWrap p
            source
            theorem MIPRE.Introspection.DecisionCompiler.zero_time_bound :
            ∃ (C : ℕ), ∀ (n d : Cost.Data), ∃ t ≤ 2 * (d.size + 1) ^ C, zeroProg.Runs (n.cons d) (Cost.encode (zeroTest.toFun d)) t
            source
            theorem MIPRE.Introspection.DecisionCompiler.zeroWrap_zero_time_bound :
            ∃ (C : ℕ), ∀ (p : Cost.Prog) (d : Cost.Data), ∃ t ≤ 2 * (d.size + 1) ^ C, (zeroWrap p).Runs ((Cost.encode 0).cons d) (Cost.encode (zeroTest.toFun d)) t