Documentation

Starlib.OracleReduction.ProtocolSpec.Cast

Casting for ProtocolSpec and related structures #

We define custom dependent casts (registered as DCast instances) for the following structures:

We also show basic properties about these casts.

Casting Protocol Specifications #

source
def ProtocolSpec.cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) (pSpec : ProtocolSpec n₁) :
ProtocolSpec n₂

Casting a ProtocolSpec across an equality of the number of rounds

One should use the type-class function dcast instead of this one.

Instances For
    source
    @[simp]
    theorem ProtocolSpec.cast_id {n₁ : ℕ} :
    ProtocolSpec.cast ⋯ = id
    source
    @[implicit_reducible]
    instance ProtocolSpec.instDCast :
    DCast ℕ ProtocolSpec
    source
    theorem ProtocolSpec.cast_eq_dcast {n₁ n₂ : ℕ} {h : n₁ = n₂} {pSpec : ProtocolSpec n₁} :
    ProtocolSpec.cast h pSpec = dcast h pSpec

    Casting (Partial) Transcripts #

    source
    @[simp]
    theorem ProtocolSpec.cast_dir_idx {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : Fin n₁} :
    pSpec₂.dir (Fin.cast hn i) = pSpec₁.dir i
    source
    theorem ProtocolSpec.cast_Type_idx {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : Fin n₁} :
    pSpec₂.Type (Fin.cast hn i) = pSpec₁.Type i
    source
    @[simp]
    theorem ProtocolSpec.cast_dir_idx_symm {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : Fin n₂} :
    pSpec₁.dir (Fin.cast ⋯ i) = pSpec₂.dir i
    source
    theorem ProtocolSpec.cast_Type_idx_symm {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : Fin n₂} :
    pSpec₁.Type (Fin.cast ⋯ i) = pSpec₂.Type i
    source
    theorem ProtocolSpec.cast_symm {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) :
    ProtocolSpec.cast ⋯ pSpec₂ = pSpec₁
    source
    def ProtocolSpec.MessageIdx.cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) (i : pSpec₁.MessageIdx) :
    pSpec₂.MessageIdx

    Casting a message index across an equality of ProtocolSpecs.

    Instances For
      source
      @[simp]
      theorem ProtocolSpec.MessageIdx.cast_id {n₁ : ℕ} {pSpec₁ : ProtocolSpec n₁} :
      MessageIdx.cast ⋯ ⋯ = id
      source
      theorem ProtocolSpec.MessageIdx.cast_injective {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) :
      Function.Injective (MessageIdx.cast hn hSpec)
      source
      @[implicit_reducible]
      instance ProtocolSpec.MessageIdx.instDCast₂ :
      DCast₂ ℕ ProtocolSpec fun (x : ℕ) (pSpec : ProtocolSpec x) => pSpec.MessageIdx
      source
      theorem ProtocolSpec.MessageIdx.cast_eq_dcast₂ {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} {hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂} {i : pSpec₁.MessageIdx} :
      MessageIdx.cast hn hSpec i = dcast₂ hn hSpec i
      source
      @[simp]
      theorem ProtocolSpec.Message.cast_idx_symm {n₁ n₂ : ℕ} {hn : n₁ = n₂} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : pSpec₂.MessageIdx} :
      pSpec₁.Message (MessageIdx.cast ⋯ ⋯ i) = pSpec₂.Message i
      source
      theorem ProtocolSpec.Message.cast_idx {n₁ n₂ : ℕ} {hn : n₁ = n₂} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : pSpec₁.MessageIdx} :
      pSpec₂.Message (MessageIdx.cast hn hSpec i) = pSpec₁.Message i
      source
      def ProtocolSpec.ChallengeIdx.cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) (i : pSpec₁.ChallengeIdx) :
      pSpec₂.ChallengeIdx

      Casting a challenge index across an equality of ProtocolSpecs.

      Instances For
        source
        @[simp]
        theorem ProtocolSpec.ChallengeIdx.cast_id {n₁ : ℕ} {pSpec₁ : ProtocolSpec n₁} :
        ChallengeIdx.cast ⋯ ⋯ = id
        source
        theorem ProtocolSpec.ChallengeIdx.cast_injective {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) :
        Function.Injective (ChallengeIdx.cast hn hSpec)
        source
        @[implicit_reducible]
        instance ProtocolSpec.ChallengeIdx.instDCast₂ :
        DCast₂ ℕ ProtocolSpec fun (x : ℕ) (pSpec : ProtocolSpec x) => pSpec.ChallengeIdx
        source
        theorem ProtocolSpec.ChallengeIdx.cast_eq_dcast₂ {n₁ n₂ : ℕ} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {hn : n₁ = n₂} {hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂} {i : pSpec₁.ChallengeIdx} :
        ChallengeIdx.cast hn hSpec i = dcast₂ hn hSpec i
        source
        @[simp]
        theorem ProtocolSpec.Challenge.cast_idx {n₁ n₂ : ℕ} {hn : n₁ = n₂} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : pSpec₁.ChallengeIdx} :
        pSpec₂.Challenge (ChallengeIdx.cast hn hSpec i) = pSpec₁.Challenge i
        source
        @[simp]
        theorem ProtocolSpec.Challenge.cast_idx_symm {n₁ n₂ : ℕ} {hn : n₁ = n₂} {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {i : pSpec₂.ChallengeIdx} :
        pSpec₁.Challenge (ChallengeIdx.cast ⋯ ⋯ i) = pSpec₂.Challenge i
        source
        def ProtocolSpec.Transcript.cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {k : Fin (n₁ + 1)} {l : Fin (n₂ + 1)} (hIdx : ↑k = ↑l) (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) (T : Transcript k pSpec₁) :
        Transcript l pSpec₂

        Casting two partial transcripts across an equality of ProtocolSpecs, where the cutoff indices are equal.

        Instances For
          source
          @[simp]
          theorem ProtocolSpec.Transcript.cast_id {n₁ : ℕ} {pSpec₁ : ProtocolSpec n₁} {k : Fin (n₁ + 1)} :
          Transcript.cast ⋯ ⋯ ⋯ = id
          source
          @[implicit_reducible]
          instance ProtocolSpec.Transcript.instDCast₃ :
          DCast₃ ℕ (fun (n : ℕ) => Fin (n + 1)) (fun (n : ℕ) (x : Fin (n + 1)) => ProtocolSpec n) fun (x : ℕ) (k : Fin (x + 1)) (pSpec : ProtocolSpec x) => Transcript k pSpec

          Casting Full Transcripts #

          source
          def ProtocolSpec.FullTranscript.cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) (T : pSpec₁.FullTranscript) :
          pSpec₂.FullTranscript

          Casting a transcript across an equality of ProtocolSpecs.

          Internally invoke Transcript.cast with the last indices.

          Instances For
            source
            @[simp]
            theorem ProtocolSpec.FullTranscript.cast_id {n₁ : ℕ} {pSpec₁ : ProtocolSpec n₁} :
            FullTranscript.cast ⋯ ⋯ = id
            source
            @[implicit_reducible]
            instance ProtocolSpec.FullTranscript.instDCast₂ :
            DCast₂ ℕ ProtocolSpec fun (x : ℕ) (pSpec : ProtocolSpec x) => pSpec.FullTranscript
            source
            theorem ProtocolSpec.FullTranscript.cast_eq_dcast₂ {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} (hSpec : ProtocolSpec.cast hn pSpec₁ = pSpec₂) {T : pSpec₁.FullTranscript} :
            dcast₂ hn hSpec T = FullTranscript.cast hn hSpec T
            source
            theorem ProtocolSpec.challengeOracleInterface_cast {n₁ n₂ : ℕ} (hn : n₁ = n₂) {pSpec₁ : ProtocolSpec n₁} {pSpec₂ : ProtocolSpec n₂} {h : n₁ = n₂} {hSpec : ProtocolSpec.cast h pSpec₁ = pSpec₂} {i : pSpec₁.ChallengeIdx} :
            challengeOracleInterface i = dcast ⋯ (challengeOracleInterface (ChallengeIdx.cast hn hSpec i))