Documentation

MIPRE.Background.QLD.SamplerQueryProgram

The actual uniform Pauli query router #

Every input tree is parsed by total programs. Dimension, marginal, linear and factor queries use the uniform programs on the supplied parameters; the type table is the fixed twenty-six-element table only.

source
noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.dimensionProg :
Cost.PolyTimeFun Introspection.PauliStageProgram.Parameters ℕ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.QLD.PauliCL.SamplerProgram.dimensionProg_apply (p : Introspection.PauliStageProgram.Parameters) :
    dimensionProg.toFun p = (3 * List.length p.2.2 + 3) * List.length p.1
    source
    @[reducible, inline]
    abbrev MIPRE.QLD.PauliCL.SamplerProgram.RawInput :
    Type
    Equations
    Instances For
      source
      noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.parsed :
      Cost.PolyTimeFun RawInput CL.Detyping.Program.Parsed
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.tag :
        Cost.PolyTimeFun RawInput Introspection.PauliStageProgram.Tag
        Equations
        Instances For
          source
          noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.level :
          Cost.PolyTimeFun RawInput ℕ
          Equations
          Instances For
            source
            noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.inputU :
            Cost.PolyTimeFun RawInput Cost.BitStr
            Equations
            Instances For
              source
              noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.inputY :
              Cost.PolyTimeFun RawInput Cost.BitStr
              Equations
              Instances For
                source
                noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.marginalInput :
                Cost.PolyTimeFun RawInput Introspection.PauliStageProgram.BinaryInput
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.linearInput :
                  Cost.PolyTimeFun RawInput Introspection.PauliStageProgram.BinaryInput
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MIPRE.QLD.PauliCL.SamplerProgram.query :
                    Cost.PolyTimeFun RawInput Cost.Data
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.parsed_atType (p : Introspection.PauliStageProgram.Parameters) (T : Ty) (q : CL.Sampler.Query) :
                      parsed.toFun (p, Cost.encode (CL.TypedSampler.Query.atType T q)) = (Cost.encode 0, q.toTuple.1, q.toTuple.2.1.toBool, q.toTuple.2.2.1, q.toTuple.2.2.2.1, q.toTuple.2.2.2.2)
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.tag_atType (p : Introspection.PauliStageProgram.Parameters) (T : Ty) (q : CL.Sampler.Query) :
                      tag.toFun (p, Cost.encode (CL.TypedSampler.Query.atType T q)) = programTag T
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.query_dimension (p : Introspection.PauliStageProgram.Parameters) :
                      query.toFun (p, Cost.encode CL.TypedSampler.Query.dimension) = Cost.encode ((3 * List.length p.2.2 + 3) * List.length p.1)
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.query_marginal (p : Introspection.PauliStageProgram.Parameters) (w : Player) (T : Ty) (r : ℕ) (z : Cost.BitStr) :
                      query.toFun (p, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.marginal w r z))) = Cost.encode (Introspection.PauliStageProgram.marginalBits.toFun (p, programTag T, r, z, z))
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.query_linear (p : Introspection.PauliStageProgram.Parameters) (w : Player) (T : Ty) (r : ℕ) (u y : Cost.BitStr) :
                      query.toFun (p, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.linear w r u y))) = Cost.encode (Introspection.PauliStageProgram.linearBits.toFun (p, programTag T, r, u, y))
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.query_factor (p : Introspection.PauliStageProgram.Parameters) (w : Player) (T : Ty) (r : ℕ) (u : Cost.BitStr) :
                      query.toFun (p, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.factor w r u))) = Cost.encode (Introspection.PauliStageProgram.factorBits.toFun (p, r))
                      source
                      theorem MIPRE.QLD.PauliCL.SamplerProgram.query_runs (p : Introspection.PauliStageProgram.Parameters) (d : Cost.Data) :
                      ∃ t ≤ Polynomial.eval (Cost.esize (p, d)) query.timeBound, query.code.Runs (Cost.encode (p, d)) (query.toFun (p, d)) t