Documentation

MIPRE.Foundations.Introspection.Types

The introspection question types #

The source's type set consists of the Pauli types and two copies of Introspect, Sample, Read, and Hide₁, ..., Hideℓ. The Pauli type is a parameter so the foundational construction can be instantiated with the concrete Pauli test without importing a Background module.

source
inductive MIPRE.Introspection.AuxType (ℓ : ℕ) :
Type

The additional tests, before specifying the original player's role.

Instances For
    source
    def MIPRE.Introspection.instDecidableEqAuxType.decEq {ℓ✝ : ℕ} (x✝ x✝¹ : AuxType ℓ✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.Introspection.instDecidableEqAuxType {ℓ✝ : ℕ} :
      DecidableEq (AuxType ℓ✝)
      Equations
      source
      @[instance_reducible]
      instance MIPRE.Introspection.instFintypeAuxType {ℓ✝ : ℕ} :
      Fintype (AuxType ℓ✝)
      Equations
      source
      def MIPRE.Introspection.AuxType.equivOption (ℓ : ℕ) :
      AuxType ℓ ≃ Option (Option (Option (Fin ℓ)))

      Three fixed tests followed by the hiding levels.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.AuxType.card (ℓ : ℕ) :
        Fintype.card (AuxType ℓ) = ℓ + 3

        There are exactly ℓ + 3 auxiliary types for either original player.

        source
        def MIPRE.Introspection.AuxType.toNat {ℓ : ℕ} :
        AuxType ℓ → ℕ

        The auxiliary type's binary code, with the three fixed tags first.

        Equations
        Instances For
          source
          def MIPRE.Introspection.AuxType.ofNat (ℓ a✝ : ℕ) :
          Option (AuxType ℓ)

          Out-of-range hiding labels are rejected by the decoder.

          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.Introspection.AuxType.ofNat_toNat {ℓ : ℕ} (t : AuxType ℓ) :
            ofNat ℓ t.toNat = some t
            source
            @[instance_reducible]
            instance MIPRE.Introspection.AuxType.instSizedEncoding {ℓ : ℕ} :
            Cost.SizedEncoding (AuxType ℓ)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            theorem MIPRE.Introspection.AuxType.esize_le {ℓ : ℕ} (t : AuxType ℓ) :
            Cost.esize t ≤ 4 * (ℓ + 3).size + 1

            The tag encoding has logarithmic size in the number of hiding levels.

            source
            @[reducible, inline]
            abbrev MIPRE.Introspection.QuestionType (PauliType : Type u_1) (ℓ : ℕ) :
            Type u_1

            Pauli types together with the introspection tests for the two original players.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev MIPRE.Introspection.QuestionType.pauli {PauliType : Type u_1} {ℓ : ℕ} (p : PauliType) :
              QuestionType PauliType ℓ
              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev MIPRE.Introspection.QuestionType.introspect {PauliType : Type u_1} {ℓ : ℕ} (w : Bool) :
                QuestionType PauliType ℓ
                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev MIPRE.Introspection.QuestionType.sample {PauliType : Type u_1} {ℓ : ℕ} (w : Bool) :
                  QuestionType PauliType ℓ
                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev MIPRE.Introspection.QuestionType.read {PauliType : Type u_1} {ℓ : ℕ} (w : Bool) :
                    QuestionType PauliType ℓ
                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev MIPRE.Introspection.QuestionType.hide {PauliType : Type u_1} {ℓ : ℕ} (w : Bool) (k : Fin ℓ) :
                      QuestionType PauliType ℓ
                      Equations
                      Instances For
                        source
                        theorem MIPRE.Introspection.QuestionType.card {PauliType : Type u_1} [Fintype PauliType] (ℓ : ℕ) :
                        Fintype.card (QuestionType PauliType ℓ) = Fintype.card PauliType + 2 * ℓ + 6

                        Introspection contributes exactly 2ℓ + 6 vertices.

                        source
                        theorem MIPRE.Introspection.QuestionType.card_of_pauli_card {PauliType : Type u_1} [Fintype PauliType] (h : Fintype.card PauliType = 26) (ℓ : ℕ) :
                        Fintype.card (QuestionType PauliType ℓ) = 2 * ℓ + 32

                        The paper's 26 Pauli types give 2ℓ + 32 introspection types.

                        source
                        instance MIPRE.Introspection.QuestionType.instNonempty {PauliType : Type u_1} {ℓ : ℕ} :
                        Nonempty (QuestionType PauliType ℓ)

                        A type exists independently of the Pauli type set and of the number of hiding levels.

                        source
                        def MIPRE.Introspection.QuestionType.toData {PauliType : Type u_1} {ℓ : ℕ} [Cost.SizedEncoding PauliType] :
                        QuestionType PauliType ℓ → Cost.Data

                        A single bit distinguishes Pauli labels from role-tagged auxiliary labels.

                        Equations
                        Instances For
                          source
                          def MIPRE.Introspection.QuestionType.ofData {PauliType : Type u_1} {ℓ : ℕ} [Cost.SizedEncoding PauliType] :
                          Cost.Data → Option (QuestionType PauliType ℓ)
                          Equations
                          Instances For
                            source
                            @[simp]
                            theorem MIPRE.Introspection.QuestionType.ofData_toData {PauliType : Type u_1} {ℓ : ℕ} [Cost.SizedEncoding PauliType] (t : QuestionType PauliType ℓ) :
                            ofData t.toData = some t
                            source
                            @[instance_reducible]
                            instance MIPRE.Introspection.QuestionType.instSizedEncoding {PauliType : Type u_1} {ℓ : ℕ} [Cost.SizedEncoding PauliType] :
                            Cost.SizedEncoding (QuestionType PauliType ℓ)
                            Equations
                            source
                            theorem MIPRE.Introspection.QuestionType.esize_aux_le {PauliType : Type u_1} {ℓ : ℕ} [Cost.SizedEncoding PauliType] (t : AuxType ℓ) (w : Bool) :
                            Cost.esize (Sum.inr (t, w)) ≤ 4 * (ℓ + 3).size + 9

                            The complete encoding of an auxiliary type has logarithmic size in ℓ.