Documentation

MIPRE.Foundations.Introspection.TypeGraph

The introspection type graph #

The graph of introspection.tex, Figure fig:type-graph-intro: the Pauli subgraph, two chains from Pauli-X through hiding levels to Read, two chains from Pauli-Z through Sample and Introspect to Read, the cross-introspection edge, and a loop at every vertex. The construction uses only the Pauli graph and its two distinguished vertices; no rigidity conclusion is assumed.

source
def MIPRE.Introspection.TypeGraph.oriented {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) :
QuestionType PauliType ℓ → QuestionType PauliType ℓ → Bool

One orientation of each edge drawn in the source figure.

Equations
Instances For
    source
    def MIPRE.Introspection.TypeGraph.adj {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t u : QuestionType PauliType ℓ) :
    Bool

    The graph is undirected and has a self-loop at every type.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MIPRE.Introspection.TypeGraph.Adj {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t u : QuestionType PauliType ℓ) :
      Prop

      Propositional adjacency, for the graph sampler and finite detyping theorem.

      Equations
      Instances For
        source
        theorem MIPRE.Introspection.TypeGraph.adj_symm {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t u : QuestionType PauliType ℓ) :
        adj E X Z t u = adj E X Z u t
        source
        theorem MIPRE.Introspection.TypeGraph.symmetric {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t u : QuestionType PauliType ℓ) :
        Adj E X Z t u → Adj E X Z u t

        Adjacency has the exact symmetry needed by graph detyping.

        source
        @[simp]
        theorem MIPRE.Introspection.TypeGraph.adj_self {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t : QuestionType PauliType ℓ) :
        adj E X Z t t = true
        source
        theorem MIPRE.Introspection.TypeGraph.adj_pauli {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (hE : ∀ (p q : PauliType), E p q = E q p) (hloop : ∀ (p : PauliType), E p p = true) (p q : PauliType) :
        adj E X Z (QuestionType.pauli p) (QuestionType.pauli q) = E p q

        A symmetric reflexive Pauli graph is embedded without adding any Pauli edge.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_pauliX_hide_first {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (hℓ : 0 < ℓ) (w : Bool) :
        adj E X Z (QuestionType.pauli X) (QuestionType.hide w ⟨0, hℓ⟩) = true

        The Pauli-X vertex starts both hiding chains.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_hide_next {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w : Bool) (k k' : Fin ℓ) (h : ↑k + 1 = ↑k') :
        adj E X Z (QuestionType.hide w k) (QuestionType.hide w k') = true

        Consecutive hiding levels for one original player are connected.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_hide_read {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w : Bool) (k : Fin ℓ) (h : ↑k + 1 = ℓ) :
        adj E X Z (QuestionType.hide w k) (QuestionType.read w) = true

        The last hiding level connects to that player's Read type.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_pauliZ_sample {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w : Bool) :
        adj E X Z (QuestionType.pauli Z) (QuestionType.sample w) = true

        Pauli-Z connects to each Sample type.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_sample_introspect {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w : Bool) :
        adj E X Z (QuestionType.sample w) (QuestionType.introspect w) = true

        Each Sample type is checked against the corresponding introspection.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_introspect_read {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w : Bool) :
        adj E X Z (QuestionType.introspect w) (QuestionType.read w) = true

        Each Read type is checked against the corresponding introspection.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_cross_introspect {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) :
        adj E X Z (QuestionType.introspect false) (QuestionType.introspect true) = true

        The cross-introspection edge is where the original verifier is tested.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_different_roles_iff {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (t u : AuxType ℓ) (w w' : Bool) (hw : w ≠ w') :
        adj E X Z (Sum.inr (t, w)) (Sum.inr (u, w')) = true ↔ t = AuxType.introspect ∧ u = AuxType.introspect

        The only edge between different original-player roles is cross-introspection.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_pauli_aux_iff {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z p : PauliType) (t : AuxType ℓ) (w : Bool) :
        adj E X Z (QuestionType.pauli p) (Sum.inr (t, w)) = true ↔ (p = X ∧ ∃ (k : Fin ℓ), t = AuxType.hide k ∧ ↑k = 0) ∨ p = Z ∧ t = AuxType.sample

        There are exactly two kinds of edges from the Pauli graph into the auxiliary tests.

        source
        theorem MIPRE.Introspection.TypeGraph.adj_hide_hide_iff {PauliType : Type u_1} [DecidableEq PauliType] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (w w' : Bool) (k k' : Fin ℓ) :
        adj E X Z (QuestionType.hide w k) (QuestionType.hide w' k') = true ↔ w = w' ∧ (k = k' ∨ ↑k + 1 = ↑k' ∨ ↑k' + 1 = ↑k)

        Within the hiding tests the graph has precisely same-role consecutive edges and loops.

        source
        def MIPRE.Introspection.TypeGraph.edges {PauliType : Type u_1} [DecidableEq PauliType] [Fintype PauliType] (E : PauliType → PauliType → Bool) (X Z : PauliType) (ℓ : ℕ) :
        Finset (QuestionType PauliType ℓ × QuestionType PauliType ℓ)

        The actual ordered edge set used by the typed game's distribution.

        Equations
        Instances For
          source
          theorem MIPRE.Introspection.TypeGraph.edges_nonempty {PauliType : Type u_1} [DecidableEq PauliType] [Fintype PauliType] (E : PauliType → PauliType → Bool) (X Z : PauliType) (ℓ : ℕ) :
          (edges E X Z ℓ).Nonempty

          Every introspection graph is nonempty, even with no hiding levels.

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

          In particular, the source's 26-type Pauli test gives the factor 16^(2ℓ + 32).