Documentation

MIPRE.Foundations.CL.DetypingProgParse

Total parsing for the detyping sampler #

Raw trees are converted to canonical bit strings and binary naturals before the fixed finite graph computation. Every parser is an actual polynomial-time ambient program, including on malformed encodings.

source
def MIPRE.CL.Detyping.Program.rawList :
Cost.Data → List Cost.Data
Equations
Instances For
    source
    theorem MIPRE.CL.Detyping.Program.encode_rawList (d : Cost.Data) :
    Cost.encode (rawList d) = d
    source
    def MIPRE.CL.Detyping.Program.rawTruth :
    Cost.Data → Bool
    Equations
    Instances For
      source
      noncomputable def MIPRE.CL.Detyping.Program.rawTruthProg :
      Cost.PolyTimeFun Cost.Data Bool
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.CL.Detyping.Program.readBits :
        Cost.PolyTimeFun Cost.Data Cost.BitStr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.CL.Detyping.Program.readBits_encode (l : Cost.BitStr) :
          readBits.toFun (Cost.encode l) = l
          source
          noncomputable def MIPRE.CL.Detyping.Program.readNat :
          Cost.PolyTimeFun Cost.Data ℕ
          Equations
          Instances For
            source
            theorem MIPRE.CL.Detyping.Program.readNat_encode (n : ℕ) :
            readNat.toFun (Cost.encode n) = n
            source
            theorem MIPRE.CL.Detyping.Program.rawTruthProg_encode_bool (b : Bool) :
            rawTruthProg.toFun (Cost.encode b) = b
            source
            noncomputable def MIPRE.CL.Detyping.Program.encoded {α : Type u_1} [Cost.SizedEncoding α] :
            Cost.PolyTimeFun α Cost.Data
            Equations
            Instances For
              source
              @[simp]
              theorem MIPRE.CL.Detyping.Program.encoded_apply {α : Type u_1} [Cost.SizedEncoding α] (a : α) :
              encoded.toFun a = Cost.encode a
              source
              @[reducible, inline]
              abbrev MIPRE.CL.Detyping.Program.Parsed :
              Type
              Equations
              Instances For
                source
                noncomputable def MIPRE.CL.Detyping.Program.parse :
                Cost.PolyTimeFun Cost.Data Parsed
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem MIPRE.CL.Detyping.Program.parse_query (n : ℕ) (q : Sampler.Query) :
                  parse.toFun (Cost.encode (n, q)) = (Cost.encode n, 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
                  @[instance_reducible]
                  instance MIPRE.CL.Detyping.Program.vectorEncoding (d : ℕ) :
                  Cost.SizedEncoding (Fin d → 𝔽₂)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  noncomputable def MIPRE.CL.Detyping.Program.readVector (d : ℕ) :
                  Cost.PolyTimeFun Cost.BitStr (Fin d → 𝔽₂)

                  Reading a fixed number of graph bits is a finite collection of array reads.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem MIPRE.CL.Detyping.Program.readVector_apply (d : ℕ) (l : Cost.BitStr) :
                    (readVector d).toFun l = ofBits d l