Documentation

MIPRE.Foundations.CL.Sampler

Samplers #

Blueprint def:sampler (paper linear.tex, Definition def:sampler; ledger node 1.1.3 with def:normal-verifier). A sampler is the half of a normal form verifier that produces the questions: a program of the ambient model (MIPRE.Cost) that, on an index n, presents two conditionally linear functions L^๐– , L^๐–ก on ๐”ฝโ‚‚^{s(n)} โ€” one per player โ€” through a fixed query interface, so that the question distribution of the game at index n is the CL distribution (L^๐–  x, L^๐–ก x), x uniform. The interface is what every transformation of the pipeline (introspection, oracularization, answer reduction) is written against, which is why the blueprint fixes it once and for all. It is the paper's, restricted to field size 2 as the blueprint's normal form verifiers are:

for 1 โ‰ค j โ‰ค โ„“, z, y of length s(n), and โ€” for the last two โ€” u in the image of L^w_{< j}, exactly as the paper quantifies (CLFun.SupportedOn.factorOfPrefix_eval is what makes the answers well defined there). The sampler must moreover halt on every input of the form (n, โ€ฆ); the paper's bounded format checks are what make its running time on index n, the supremum over all such inputs, finite. Sampler.TimeBoundAt n T k is that supremum bounded by T, read as halting within cost T ยท (|d| + 1)^k on every input (n, d): the ambient model has no cursor into its input, and a bound uniform over all inputs is not satisfiable by any program that walks a list of unbounded length (see the module docstring of MIPRE.Foundations.Verifier, which also says why the degree k is needed). Vectors and register subspaces of ๐”ฝโ‚‚^s travel as bit strings of length s (toBits, ofBits, indicatorBits); the paper's binary representation over ๐”ฝ_{2^k} through a self-dual basis is not needed at field size 2.

The CL functions of a sampler are required to be exactly on the whole space (CLFun.ExactlyOn): their factor spaces partition the coordinates, item (2) of lem:cl-kth, which the paper's definition demands of them.

Conventions #

The input of the program is the one value encode (n, q) for q : Sampler.Query, with a query encoded as the tuple (kind, w, j, u, y), missing arguments empty (Sampler.Query.toTuple). Players are MIPRE.Player, Alice first.

source
inductive MIPRE.Player :
Type

The two players of a nonlocal game.

  • alice : Player

    The first player.

  • bob : Player

    The second player.

Instances For
    source
    @[instance_reducible]
    instance MIPRE.instDecidableEqPlayer :
    DecidableEq Player
    Equations
    source
    def MIPRE.Player.toBool :
    Player โ†’ Bool

    Players as bits: Alice is false, Bob is true.

    Equations
    Instances For
      source
      def MIPRE.Player.ofBool :
      Bool โ†’ Player

      The player of a bit.

      Equations
      Instances For
        source
        @[simp]
        theorem MIPRE.Player.ofBool_toBool (w : Player) :
        ofBool w.toBool = w
        source
        @[instance_reducible]
        instance MIPRE.Player.instSizedEncoding :
        Cost.SizedEncoding Player
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[reducible, inline]
        abbrev MIPRE.CL.๐”ฝโ‚‚ :
        Type

        The binary field ๐”ฝโ‚‚: the field size of every sampler of a normal form verifier (blueprint def:sampler).

        Equations
        Instances For

          Vectors of ๐”ฝโ‚‚^s as bit strings #

          source
          def MIPRE.CL.toBits {s : โ„•} (v : Fin s โ†’ ๐”ฝโ‚‚) :
          Cost.BitStr

          The bit string of a vector in ๐”ฝโ‚‚^s: its list of coordinates.

          Equations
          Instances For
            source
            def MIPRE.CL.ofBits (s : โ„•) (l : Cost.BitStr) :
            Fin s โ†’ ๐”ฝโ‚‚

            The vector in ๐”ฝโ‚‚^s read off a bit string; missing bits read as 0, bits beyond s are ignored.

            Equations
            Instances For
              source
              def MIPRE.CL.indicatorBits {s : โ„•} (S : Finset (Fin s)) :
              Cost.BitStr

              The indicator bit string of a set of coordinates: the paper's representation of a register subspace of ๐”ฝโ‚‚^s as a vector in {0,1}^s.

              Equations
              Instances For
                source
                @[simp]
                theorem MIPRE.CL.length_toBits {s : โ„•} (v : Fin s โ†’ ๐”ฝโ‚‚) :
                List.length (toBits v) = s
                source
                @[simp]
                theorem MIPRE.CL.length_indicatorBits {s : โ„•} (S : Finset (Fin s)) :
                List.length (indicatorBits S) = s
                source
                theorem MIPRE.CL.ite_decide_eq_one (a : ๐”ฝโ‚‚) :
                (if decide (a = 1) = true then 1 else 0) = a
                source
                @[simp]
                theorem MIPRE.CL.ofBits_toBits {s : โ„•} (v : Fin s โ†’ ๐”ฝโ‚‚) :
                ofBits s (toBits v) = v
                source
                theorem MIPRE.CL.toBits_ofBits {s : โ„•} {l : Cost.BitStr} (hl : List.length l = s) :
                toBits (ofBits s l) = l

                The query interface #

                source
                inductive MIPRE.CL.Sampler.Query :
                Type

                The queries a sampler answers (def:sampler): the paper's 6-input Turing machine, whose inputs after the index n are a player label w, a query kind, a level j and up to two vectors.

                Instances For
                  source
                  @[instance_reducible]
                  instance MIPRE.CL.Sampler.instDecidableEqQuery :
                  DecidableEq Query
                  Equations
                  source
                  def MIPRE.CL.Sampler.instDecidableEqQuery.decEq (xโœ xโœยน : Query) :
                  Decidable (xโœ = xโœยน)
                  Equations
                  Instances For
                    source
                    def MIPRE.CL.Sampler.Query.toTuple :
                    Query โ†’ โ„• ร— Player ร— โ„• ร— Cost.BitStr ร— Cost.BitStr

                    A query as the tuple (kind, w, j, u, y), missing arguments empty.

                    Equations
                    Instances For
                      source
                      def MIPRE.CL.Sampler.Query.ofTuple :
                      โ„• ร— Player ร— โ„• ร— Cost.BitStr ร— Cost.BitStr โ†’ Option Query

                      Reading a query back from its tuple.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem MIPRE.CL.Sampler.Query.ofTuple_toTuple (q : Query) :
                        ofTuple q.toTuple = some q
                        source
                        @[instance_reducible]
                        instance MIPRE.CL.Sampler.Query.instSizedEncoding :
                        Cost.SizedEncoding Query

                        Queries are data: their tuple, encoded.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        structure MIPRE.CL.Sampler (โ„“ : โ„•) :
                        Type

                        Blueprint def:sampler: an โ„“-level sampler (field size 2). A program of the ambient model which, on index n, presents an โ„“-level CL function on ๐”ฝโ‚‚^{s(n)} for each player through the query interface โ€” dimension, marginals, stage maps and factor spaces (the data of lem:cl-kth) โ€” and halts on every input of the form (n, โ€ฆ). The correctness clauses are imposed exactly where the paper imposes them: well-formed vectors, levels 1 โ‰ค j โ‰ค โ„“, and prefixes u in the image of L^w_{< j}.

                        Instances For
                          source
                          def MIPRE.CL.Sampler.TimeBoundAt {โ„“ : โ„•} (S : Sampler โ„“) (n T k : โ„•) :
                          Prop

                          TIME_๐’ฎ(n) โ‰ค T: the sampler halts within cost T ยท (|d| + 1)^k on every input (n, d), well formed or not โ€” the supremum of def:sampler at index n, bounded by a polynomial in the size of the input with coefficient T and degree k.

                          Equations
                          Instances For
                            source
                            def MIPRE.CL.Sampler.TimeBound {โ„“ : โ„•} (S : Sampler โ„“) (T : โ„• โ†’ โ„•) (k : โ„•) :
                            Prop

                            TIME_๐’ฎ(n) โ‰ค T n for every n, at degree k.

                            Equations
                            Instances For
                              source
                              theorem MIPRE.CL.Sampler.TimeBoundAt.mono {โ„“ : โ„•} {S : Sampler โ„“} {n T k T' k' : โ„•} (h : S.TimeBoundAt n T k) (hT : T โ‰ค T') (hk : k โ‰ค k') :
                              S.TimeBoundAt n T' k'

                              The bound is monotone in both parameters.

                              source
                              def MIPRE.CL.Sampler.size {โ„“ : โ„•} (S : Sampler โ„“) :
                              โ„•

                              The description length |๐’ฎ| of the sampler.

                              Equations
                              Instances For

                                The paper's s(n) โ‰ค TIME_๐’ฎ(n) (a marginal query writes s(n) output cells) does not follow from TimeBoundAt, whose bound grows with the input โ€” the query carrying a vector of length s(n) is itself of size about 3 s(n). Where the pipeline needs it, it is a clause of Verifier.IsBounded.

                                source
                                noncomputable def MIPRE.CL.Sampler.dist {โ„“ : โ„•} (S : Sampler โ„“) (n : โ„•) :
                                (Fin (S.dim n) โ†’ ๐”ฝโ‚‚) โ†’ (Fin (S.dim n) โ†’ ๐”ฝโ‚‚) โ†’ โ„

                                The distribution of the sampler on index n (paper def:sampler-sample): the CL distribution of its two CL functions, (L^๐–  x, L^๐–ก x) for x uniform in ๐”ฝโ‚‚^{s(n)}.

                                Equations
                                Instances For
                                  source
                                  theorem MIPRE.CL.Sampler.dist_nonneg {โ„“ : โ„•} (S : Sampler โ„“) (n : โ„•) (a b : Fin (S.dim n) โ†’ ๐”ฝโ‚‚) :
                                  0 โ‰ค S.dist n a b
                                  source
                                  theorem MIPRE.CL.Sampler.sum_dist {โ„“ : โ„•} (S : Sampler โ„“) (n : โ„•) :
                                  โˆ‘ a : Fin (S.dim n) โ†’ ๐”ฝโ‚‚, โˆ‘ b : Fin (S.dim n) โ†’ ๐”ฝโ‚‚, S.dist n a b = 1