Documentation

Starlib.OracleReduction.ProtocolSpec.SeqCompose

Sequential Composition of Protocol Specifications #

This file collects all definitions and theorems about sequentially composing ProtocolSpecs and their associated data.

Composition of Two Protocol Specifications #

source
@[reducible, inline]
abbrev ProtocolSpec.cons {n : ℕ} (pSpec : ProtocolSpec n) (dir : Direction) (Message : Type) :
ProtocolSpec (n + 1)

Adding a round with direction dir and type Message to the beginning of a ProtocolSpec

Instances For
    source
    @[reducible, inline]
    abbrev ProtocolSpec.concat {n : ℕ} (pSpec : ProtocolSpec n) (dir : Direction) (Message : Type) :
    ProtocolSpec (n + 1)

    Concatenate a round with direction dir and type Message to the end of a ProtocolSpec

    Instances For
      source
      @[reducible, inline]
      abbrev ProtocolSpec.append {m n : ℕ} (pSpec : ProtocolSpec m) (pSpec' : ProtocolSpec n) :
      ProtocolSpec (m + n)

      Appending two ProtocolSpecs

      Instances For
        source
        def ProtocolSpec.«term_++ₚ_» :
        Lean.TrailingParserDescr

        Appending two ProtocolSpecs

        Instances For
          source
          @[simp]
          theorem ProtocolSpec.append_cast_left {n m : ℕ} {pSpec : ProtocolSpec n} {pSpec' : ProtocolSpec m} (n' : ℕ) (h : n + m = n' + m) :
          dcast h (pSpec ++ₚ pSpec') = dcast ⋯ pSpec ++ₚ pSpec'
          source
          @[simp]
          theorem ProtocolSpec.append_cast_right {n m : ℕ} (pSpec : ProtocolSpec n) (pSpec' : ProtocolSpec m) (m' : ℕ) (h : n + m = n + m') :
          dcast h (pSpec ++ₚ pSpec') = pSpec ++ₚ dcast ⋯ pSpec'
          source
          theorem ProtocolSpec.append_left_injective {m n : ℕ} {pSpec : ProtocolSpec n} :
          Function.Injective fun (x : ProtocolSpec m) => x ++ₚ pSpec
          source
          theorem ProtocolSpec.append_right_injective {m n : ℕ} {pSpec : ProtocolSpec m} :
          Function.Injective pSpec.append
          source
          @[simp]
          theorem ProtocolSpec.append_left_cancel_iff {m n : ℕ} {pSpec : ProtocolSpec n} {p1 p2 : ProtocolSpec m} :
          p1 ++ₚ pSpec = p2 ++ₚ pSpec ↔ p1 = p2
          source
          @[simp]
          theorem ProtocolSpec.append_right_cancel_iff {m n : ℕ} {pSpec : ProtocolSpec m} {p1 p2 : ProtocolSpec n} :
          pSpec ++ₚ p1 = pSpec ++ₚ p2 ↔ p1 = p2
          source
          @[simp]
          theorem ProtocolSpec.snoc_take {n : ℕ} {pSpec : ProtocolSpec n} (k : ℕ) (h : k < n) :
          take k ⋯ pSpec ++ₚ { dir := ![pSpec.dir ⟨k, h⟩], «Type» := ![pSpec.Type ⟨k, h⟩] } = take (k + 1) h pSpec
          source
          @[simp]
          theorem ProtocolSpec.take_append_left {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} :
          take m ⋯ (pSpec₁ ++ₚ pSpec₂) = pSpec₁
          source
          @[simp]
          theorem ProtocolSpec.take_append_left' {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} :
          (pSpec₁ ++ₚ pSpec₂)⟦:m⟧ = pSpec₁
          source
          @[simp]
          theorem ProtocolSpec.rtake_append_right {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} :
          rtake n ⋯ (pSpec₁ ++ₚ pSpec₂) = pSpec₂
          source
          def ProtocolSpec.Transcript.fst {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} {k : Fin (m + n + 1)} (T : Transcript k (pSpec₁ ++ₚ pSpec₂)) :
          Transcript ⟨min (↑k) m, ⋯⟩ pSpec₁

          The first half of a partial transcript for a concatenated protocol, up to round k < m + n + 1.

          This is defined to be the full transcript for the first half if k ≥ m.

          Instances For
            source
            def ProtocolSpec.Transcript.snd {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} {k : Fin (m + n + 1)} (T : Transcript k (pSpec₁ ++ₚ pSpec₂)) :
            Transcript ⟨↑k - m, ⋯⟩ pSpec₂

            The second half of a partial transcript for a concatenated protocol.

            Instances For
              source
              def ProtocolSpec.FullTranscript.append {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.FullTranscript) :
              (pSpec₁ ++ₚ pSpec₂).FullTranscript

              Appending two transcripts for two ProtocolSpecs

              Instances For
                source
                def ProtocolSpec.FullTranscript.«term_++ₜ_» :
                Lean.TrailingParserDescr

                Appending two transcripts for two ProtocolSpecs

                Instances For
                  source
                  def ProtocolSpec.FullTranscript.concat {n : ℕ} {pSpec : ProtocolSpec n} {NextMessage : Type} (T : pSpec.FullTranscript) (dir : Direction) (msg : NextMessage) :
                  (pSpec ++ₚ { dir := !v[dir], «Type» := !v[NextMessage] }).FullTranscript

                  Adding a message with a given direction and type to the end of a Transcript

                  Instances For
                    source
                    @[simp]
                    theorem ProtocolSpec.FullTranscript.take_append_left {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T : pSpec₁.FullTranscript) (T' : pSpec₂.FullTranscript) :
                    take m ⋯ (T ++ₜ T') = FullTranscript.cast ⋯ ⋯ T
                    source
                    @[simp]
                    theorem ProtocolSpec.FullTranscript.rtake_append_right {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T : pSpec₁.FullTranscript) (T' : pSpec₂.FullTranscript) :
                    rtake n ⋯ (T ++ₜ T') = FullTranscript.cast ⋯ ⋯ T'
                    source
                    def ProtocolSpec.FullTranscript.fst {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T : (pSpec₁ ++ₚ pSpec₂).FullTranscript) :
                    pSpec₁.FullTranscript

                    The first half of a transcript for a concatenated protocol

                    Instances For
                      source
                      def ProtocolSpec.FullTranscript.snd {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T : (pSpec₁ ++ₚ pSpec₂).FullTranscript) :
                      pSpec₂.FullTranscript

                      The second half of a transcript for a concatenated protocol

                      Instances For
                        source
                        @[simp]
                        theorem ProtocolSpec.FullTranscript.append_fst {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.FullTranscript) :
                        (T₁ ++ₜ T₂).fst = T₁
                        source
                        @[simp]
                        theorem ProtocolSpec.FullTranscript.append_snd {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.FullTranscript) :
                        (T₁ ++ₜ T₂).snd = T₂
                        source
                        def ProtocolSpec.MessageIdx.inl {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (i : pSpec₁.MessageIdx) :
                        (pSpec₁ ++ₚ pSpec₂).MessageIdx
                        Instances For
                          source
                          def ProtocolSpec.MessageIdx.inr {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (i : pSpec₂.MessageIdx) :
                          (pSpec₁ ++ₚ pSpec₂).MessageIdx
                          Instances For
                            source
                            def ProtocolSpec.MessageIdx.sumEquiv {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} :
                            pSpec₁.MessageIdx ⊕ pSpec₂.MessageIdx ≃ (pSpec₁ ++ₚ pSpec₂).MessageIdx
                            Instances For
                              source
                              @[simp]
                              theorem ProtocolSpec.MessageIdx.sumEquiv_apply {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (a✝ : pSpec₁.MessageIdx ⊕ pSpec₂.MessageIdx) :
                              sumEquiv a✝ = Sum.elim inl inr a✝
                              source
                              @[simp]
                              theorem ProtocolSpec.MessageIdx.sumEquiv_symm_apply {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (x✝ : (pSpec₁ ++ₚ pSpec₂).MessageIdx) :
                              sumEquiv.symm x✝ = if hi : ↑↑x✝ < m then Sum.inl ⟨⟨↑↑x✝, hi⟩, ⋯⟩ else Sum.inr ⟨⟨↑↑x✝ - m, ⋯⟩, ⋯⟩
                              source
                              def ProtocolSpec.ChallengeIdx.inl {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (i : pSpec₁.ChallengeIdx) :
                              (pSpec₁ ++ₚ pSpec₂).ChallengeIdx
                              Instances For
                                source
                                def ProtocolSpec.ChallengeIdx.inr {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (i : pSpec₂.ChallengeIdx) :
                                (pSpec₁ ++ₚ pSpec₂).ChallengeIdx
                                Instances For
                                  source
                                  def ProtocolSpec.ChallengeIdx.sumEquiv {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} :
                                  pSpec₁.ChallengeIdx ⊕ pSpec₂.ChallengeIdx ≃ (pSpec₁ ++ₚ pSpec₂).ChallengeIdx
                                  Instances For
                                    source
                                    @[simp]
                                    theorem ProtocolSpec.ChallengeIdx.sumEquiv_symm_apply {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (x✝ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) :
                                    sumEquiv.symm x✝ = if hi : ↑↑x✝ < m then Sum.inl ⟨⟨↑↑x✝, hi⟩, ⋯⟩ else Sum.inr ⟨⟨↑↑x✝ - m, ⋯⟩, ⋯⟩
                                    source
                                    @[simp]
                                    theorem ProtocolSpec.ChallengeIdx.sumEquiv_apply {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (a✝ : pSpec₁.ChallengeIdx ⊕ pSpec₂.ChallengeIdx) :
                                    sumEquiv a✝ = Sum.elim inl inr a✝
                                    source
                                    @[inline]
                                    def ProtocolSpec.seqCompose {m : ℕ} {n : Fin m → ℕ} (pSpec : (i : Fin m) → ProtocolSpec (n i)) :
                                    ProtocolSpec (Fin.vsum n)

                                    Sequential composition of a family of ProtocolSpecs, indexed by i : Fin m.

                                    Defined for definitional equality, so that:

                                    • seqCompose !v[] = !p[]
                                    • seqCompose !v[pSpec₁] = pSpec₁
                                    • seqCompose !v[pSpec₁, pSpec₂] = pSpec₁ ++ₚ pSpec₂
                                    • seqCompose !v[pSpec₁, pSpec₂, pSpec₃] = pSpec₁ ++ₚ (pSpec₂ ++ₚ pSpec₃)
                                    • and so on.

                                    TODO: add notation ∑ i, pSpec i for seqCompose

                                    Instances For
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_dir {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} :
                                      (seqCompose pSpec).dir = Fin.vflatten fun (i : Fin m) => (pSpec i).dir
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_type {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} :
                                      (seqCompose pSpec).Type = Fin.vflatten fun (i : Fin m) => (pSpec i).Type
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_zero {n : Fin 0 → ℕ} {pSpec : (i : Fin 0) → ProtocolSpec (n i)} :
                                      seqCompose pSpec = !p[]
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_one {n : Fin 1 → ℕ} {pSpec : (i : Fin 1) → ProtocolSpec (n i)} :
                                      seqCompose pSpec = pSpec 0
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_two_eq_append {n : Fin 2 → ℕ} {pSpec : (i : Fin 2) → ProtocolSpec (n i)} :
                                      seqCompose pSpec = pSpec 0 ++ₚ pSpec 1
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_succ_eq_append {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : (i : Fin (m + 1)) → ProtocolSpec (n i)} :
                                      seqCompose pSpec = pSpec 0 ++ₚ seqCompose fun (i : Fin m) => pSpec i.succ
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_succ_dir {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : (i : Fin (m + 1)) → ProtocolSpec (n i)} :
                                      (seqCompose pSpec).dir = Fin.vflatten fun (i : Fin (m + 1)) => (pSpec i).dir
                                      source
                                      @[simp]
                                      theorem ProtocolSpec.seqCompose_succ_type {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : (i : Fin (m + 1)) → ProtocolSpec (n i)} :
                                      (seqCompose pSpec).Type = Fin.vflatten fun (i : Fin (m + 1)) => (pSpec i).Type
                                      source
                                      @[inline]
                                      def ProtocolSpec.FullTranscript.seqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} (T : (i : Fin m) → (pSpec i).FullTranscript) :
                                      (ProtocolSpec.seqCompose pSpec).FullTranscript

                                      Sequential composition of a family of FullTranscripts, indexed by i : Fin m.

                                      Defined for definitional equality, so that the following holds definitionally:

                                      TODO: add notation ∑ i, T i for seqCompose

                                      Instances For
                                        source
                                        @[simp]
                                        theorem ProtocolSpec.FullTranscript.seqCompose_zero {n : Fin 0 → ℕ} {pSpec : (i : Fin 0) → ProtocolSpec (n i)} {T : (i : Fin 0) → (pSpec i).FullTranscript} :
                                        seqCompose T = !h[]
                                        source
                                        @[simp]
                                        theorem ProtocolSpec.FullTranscript.seqCompose_succ_eq_append {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : (i : Fin (m + 1)) → ProtocolSpec (n i)} {T : (i : Fin (m + 1)) → (pSpec i).FullTranscript} :
                                        seqCompose T = T 0 ++ₜ seqCompose fun (i : Fin m) => T i.succ
                                        source
                                        @[simp]
                                        theorem ProtocolSpec.FullTranscript.seqCompose_embedSum {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} {T : (i : Fin m) → (pSpec i).FullTranscript} (i : Fin m) (j : Fin (n i)) :
                                        seqCompose T (i.embedSum j) = cast ⋯ (T i j)
                                        source
                                        @[implicit_reducible, inline]
                                        instance ProtocolSpec.instSampleableTypeChallengeAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} [h₁ : (i : pSpec₁.ChallengeIdx) → SampleableType (pSpec₁.Challenge i)] [h₂ : (i : pSpec₂.ChallengeIdx) → SampleableType (pSpec₂.Challenge i)] (i : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) :
                                        SampleableType ((pSpec₁ ++ₚ pSpec₂).Challenge i)

                                        If two protocols have sampleable challenges, then their concatenation also has sampleable challenges.

                                        source
                                        @[implicit_reducible, inline]
                                        instance ProtocolSpec.instInhabitedChallengeAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} [h₁ : (i : pSpec₁.ChallengeIdx) → Inhabited (pSpec₁.Challenge i)] [h₂ : (i : pSpec₂.ChallengeIdx) → Inhabited (pSpec₂.Challenge i)] (i : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) :
                                        Inhabited ((pSpec₁ ++ₚ pSpec₂).Challenge i)

                                        If two protocols' challenge types are inhabited, then their concatenation's challenge types are also inhabited.

                                        source
                                        @[implicit_reducible, inline]
                                        instance ProtocolSpec.instFintypeChallengeAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} [h₁ : (i : pSpec₁.ChallengeIdx) → Fintype (pSpec₁.Challenge i)] [h₂ : (i : pSpec₂.ChallengeIdx) → Fintype (pSpec₂.Challenge i)] (i : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) :
                                        Fintype ((pSpec₁ ++ₚ pSpec₂).Challenge i)

                                        If two protocols' challenge types are finite, then their concatenation's challenge types are also finite.

                                        source
                                        @[implicit_reducible]
                                        instance ProtocolSpec.instOracleInterfaceMessageAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} [O₁ : (i : pSpec₁.MessageIdx) → OracleInterface (pSpec₁.Message i)] [O₂ : (i : pSpec₂.MessageIdx) → OracleInterface (pSpec₂.Message i)] (i : (pSpec₁ ++ₚ pSpec₂).MessageIdx) :
                                        OracleInterface ((pSpec₁ ++ₚ pSpec₂).Message i)

                                        If two protocols' messages have oracle representations, then their concatenation's messages also have oracle representations.

                                        source
                                        @[implicit_reducible]
                                        instance ProtocolSpec.instOracleInterfaceChallengeAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} (i : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) :
                                        OracleInterface ((pSpec₁ ++ₚ pSpec₂).Challenge i)
                                        source
                                        def ProtocolSpec.sigmaChallengeIdxToSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} (i : Fin m) (j : (pSpec i).ChallengeIdx) :
                                        (seqCompose pSpec).ChallengeIdx
                                        Instances For
                                          source
                                          def ProtocolSpec.seqComposeChallengeIdxToSigma {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} (k : (seqCompose pSpec).ChallengeIdx) :
                                          (i : Fin m) × (pSpec i).ChallengeIdx
                                          Instances For
                                            source
                                            def ProtocolSpec.seqComposeChallengeEquiv {m : ℕ} {n : Fin m → ℕ} (pSpec : (i : Fin m) → ProtocolSpec (n i)) :
                                            (i : Fin m) × (pSpec i).ChallengeIdx ≃ (seqCompose pSpec).ChallengeIdx

                                            The equivalence between the challenge indices of the individual protocols and the challenge indices of the sequential composition.

                                            Instances For
                                              source
                                              def ProtocolSpec.sigmaMessageIdxToSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} (i : Fin m) (j : (pSpec i).MessageIdx) :
                                              (seqCompose pSpec).MessageIdx
                                              Instances For
                                                source
                                                def ProtocolSpec.seqComposeMessageIdxToSigma {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} (k : (seqCompose pSpec).MessageIdx) :
                                                (i : Fin m) × (pSpec i).MessageIdx
                                                Instances For
                                                  source
                                                  def ProtocolSpec.seqComposeMessageEquiv {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} :
                                                  (i : Fin m) × (pSpec i).MessageIdx ≃ (seqCompose pSpec).MessageIdx

                                                  The equivalence between the message indices of the individual protocols and the message indices of the sequential composition.

                                                  Instances For
                                                    source
                                                    @[implicit_reducible]
                                                    instance ProtocolSpec.instSampleableTypeChallengeSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} [inst : (i : Fin m) → (j : (pSpec i).ChallengeIdx) → SampleableType ((pSpec i).Challenge j)] (k : (seqCompose pSpec).ChallengeIdx) :
                                                    SampleableType ((seqCompose pSpec).Challenge k)
                                                    source
                                                    @[implicit_reducible]
                                                    instance ProtocolSpec.instInhabitedChallengeSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} [inst : (i : Fin m) → (j : (pSpec i).ChallengeIdx) → Inhabited ((pSpec i).Challenge j)] (k : (seqCompose pSpec).ChallengeIdx) :
                                                    Inhabited ((seqCompose pSpec).Challenge k)
                                                    source
                                                    @[implicit_reducible]
                                                    instance ProtocolSpec.instFintypeChallengeSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} [inst : (i : Fin m) → (j : (pSpec i).ChallengeIdx) → Fintype ((pSpec i).Challenge j)] (k : (seqCompose pSpec).ChallengeIdx) :
                                                    Fintype ((seqCompose pSpec).Challenge k)
                                                    source
                                                    @[implicit_reducible]
                                                    instance ProtocolSpec.instOracleInterfaceMessageSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : (i : Fin m) → ProtocolSpec (n i)} [Oₘ : (i : Fin m) → (j : (pSpec i).MessageIdx) → OracleInterface ((pSpec i).Message j)] (k : (seqCompose pSpec).MessageIdx) :
                                                    OracleInterface ((seqCompose pSpec).Message k)

                                                    If all protocols' messages have oracle interfaces, then the messages of their sequential composition also have oracle interfaces.