Documentation

MIPRE.Foundations.Introspection.TypedPredicate

The parsed typed introspection predicate #

This supplies the actual finite decision predicate, including both orientations of every auxiliary test and the original game test. The Pauli predicate and its X/Z answer projection are supplied by the Pauli test. This semantic layer does not assert the remaining byte parser, answer clock, or program compiler.

source
inductive MIPRE.Introspection.ParsedAnswer (V : Type u_1) (A : Type u_2) (P : Type u_3) :
Type (max (max u_1 u_2) u_3)

The four parsed answer formats. Sample and Introspect share the pair format.

Instances For
    source
    def MIPRE.Introspection.instDecidableEqParsedAnswer.decEq {V✝ : Type u_1} {A✝ : Type u_2} {P✝ : Type u_3} [DecidableEq V✝] [DecidableEq A✝] [DecidableEq P✝] (x✝ x✝¹ : ParsedAnswer V✝ A✝ P✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.Introspection.instDecidableEqParsedAnswer {V✝ : Type u_1} {A✝ : Type u_2} {P✝ : Type u_3} [DecidableEq V✝] [DecidableEq A✝] [DecidableEq P✝] :
      DecidableEq (ParsedAnswer V✝ A✝ P✝)
      Equations
      source
      @[instance_reducible]
      instance MIPRE.Introspection.instFintypeParsedAnswer {V✝ : Type u_1} {A✝ : Type u_2} {P✝ : Type u_3} [Fintype V✝] [Fintype A✝] [Fintype P✝] :
      Fintype (ParsedAnswer V✝ A✝ P✝)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def MIPRE.Introspection.TypedPredicate.fits {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} {ℓ : ℕ} :
      QuestionType PauliType ℓ → ParsedAnswer (ι → F) A PauliAnswer → Bool

      Check the parsed answer constructor against the question type.

      Equations
      Instances For
        source
        noncomputable def MIPRE.Introspection.TypedPredicate.directed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) :
        QuestionType PauliType ℓ → QuestionType PauliType ℓ → ParsedAnswer (ι → F) A PauliAnswer → ParsedAnswer (ι → F) A PauliAnswer → Bool

        One orientation of all sampling/hiding/game comparisons. The caller checks both orientations, as required by the symmetric type graph.

        Equations
        Instances For
          source
          noncomputable def MIPRE.Introspection.TypedPredicate.check {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) :
          Bool

          The actual parsed predicate: format, consistency, Pauli, and both auxiliary orientations.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.Introspection.TypedPredicate.check_formats {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) {t u : QuestionType PauliType ℓ} {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : check L X Z projectPauli D DP t u a b = true) :
            fits t a = true ∧ fits u b = true

            Accepted answers have the correct constructors on both sides.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_consistency {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) {t : QuestionType PauliType ℓ} {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : check L X Z projectPauli D DP t t a b = true) :
            a = b

            Accepted equal-type questions have exactly equal parsed answers.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_sampling {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) {y z : ι → F} {a b : A} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.sample, w)) (ParsedAnswer.pair y a) (ParsedAnswer.pair z b) = true) :
            y = (L w).eval z ∧ a = b

            Accepted introspection/sample answers satisfy the original full CL relation.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_sampling_prefix {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (hL : (L w).SupportedOn Finset.univ) {y z : ι → F} {a b : A} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.sample, w)) (ParsedAnswer.pair y a) (ParsedAnswer.pair z b) = true) (k : ℕ) :
            ((L w).outputPrefix k y, a) = ((CL.CLFun.truncate k (L w)).eval z, b)

            Therefore acceptance enforces every marginal check on the complete answer alphabet.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_reading {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) {y z zp : ι → F} {a b : A} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.pair y a) (ParsedAnswer.read z zp b) = true) :
            y = z ∧ a = b

            The reading edge preserves the introspected question and answer.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_game {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (x y : ι → F) (a b : A) :
            check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, false)) (Sum.inr (AuxType.introspect, true)) (ParsedAnswer.pair x a) (ParsedAnswer.pair y b) = D x y a b

            The cross-introspection edge runs precisely the original decision predicate.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_game_reversed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (x y : ι → F) (a b : A) :
            check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, true)) (Sum.inr (AuxType.introspect, false)) (ParsedAnswer.pair y b) (ParsedAnswer.pair x a) = D x y a b

            Reversing the players on that edge retains the original Alice/Bob argument order.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_directed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) {t u : QuestionType PauliType ℓ} {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : check L X Z projectPauli D DP t u a b = true) :
            directed L X Z projectPauli D t u a b = true

            Acceptance includes the auxiliary check in the displayed player order.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_directed_reversed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) {t u : QuestionType PauliType ℓ} {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : check L X Z projectPauli D DP t u a b = true) :
            directed L X Z projectPauli D u t b a = true

            Acceptance also includes the auxiliary check with the players reversed.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_read {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) {y yp x z zp : ι → F} {a : A} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.hide y yp x) (ParsedAnswer.read z zp a) = true) :
            CLChecks.hidingRead (L w) (y, yp, x) (z, zp, a)

            The last hiding level and Read have the tested common prefix and full dual answer.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_read_reversed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) {y yp x z zp : ι → F} {a : A} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.read, w)) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.read z zp a) (ParsedAnswer.hide y yp x) = true) :
            CLChecks.hidingRead (L w) (y, yp, x) (z, zp, a)

            The reversed Read/hiding edge retains the same earlier-prefix convention.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_next {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) {y yp x z zp t : ι → F} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.hide j, w)) (ParsedAnswer.hide y yp x) (ParsedAnswer.hide z zp t) = true) :
            CLChecks.hidingNext (L w) ↑k (y, yp, x) (z, zp, t)

            Accepted consecutive hiding answers satisfy all four source comparisons.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_next_reversed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) {y yp x z zp t : ι → F} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.hide j, w)) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.hide z zp t) (ParsedAnswer.hide y yp x) = true) :
            CLChecks.hidingNext (L w) ↑k (y, yp, x) (z, zp, t)

            Reversing the players does not change which hiding answer fixes the later register.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_pauli {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) {a : PauliAnswer} {y yp x : ι → F} (h : check L X Z projectPauli D DP (Sum.inl X) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.pauli a) (ParsedAnswer.hide y yp x) = true) :
            CLChecks.hidingPauli (L w) (projectPauli a) (y, yp, x)

            The Pauli-X/hiding-first edge checks the dual first register and the untouched tail.

            source
            theorem MIPRE.Introspection.TypedPredicate.check_hiding_pauli_reversed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) {a : PauliAnswer} {y yp x : ι → F} (h : check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inl X) (ParsedAnswer.hide y yp x) (ParsedAnswer.pauli a) = true) :
            CLChecks.hidingPauli (L w) (projectPauli a) (y, yp, x)

            The reversed first hiding edge has the same dual-map and tail comparisons.