ArkLibFri/ArkLib/OracleReduction/Cast.lean at main · NethermindEth/ArkLibFri · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
/-
Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Quang Dao
-/

import ArkLib.OracleReduction.Security.Basic

/-!
  # Casting for structures of oracle reductions

  We define custom dependent casts (registered as `DepCast` instances) for the following structures:
  - `ProtocolSpec`
  - `(Full)Transcript`
  - `(Oracle)Prover`
  - `(Oracle)Verifier`
  - `(Oracle)Reduction`
-/

/-! ### Casting Protocol Specifications -/

namespace ProtocolSpec

section Cast

variable {m n : ℕ}

/-- Casting a `ProtocolSpec` across an equality of the number of rounds

One should use the type-class function `dcast` instead of this one. -/
protected def cast (h : m = n) (pSpec : ProtocolSpec m) : ProtocolSpec n :=
  pSpec ∘ (Fin.cast h.symm)

@[simp]
theorem cast_id : ProtocolSpec.cast (Eq.refl n) = id := rfl

instance instDepCast : DepCast Nat ProtocolSpec where
  dcast h := ProtocolSpec.cast h
  dcast_id := cast_id

theorem cast_eq_dcast (h : m = n) (pSpec : ProtocolSpec m) :
    dcast h pSpec = ProtocolSpec.cast h pSpec := rfl

end Cast

namespace FullTranscript

/-! ### Casting Full Transcripts -/

section Cast

variable {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n}

/-- Casting a transcript across an equality of `ProtocolSpec`s -/
protected def cast (h : m = n) (hSpec : dcast h pSpec₁ = pSpec₂) (T : FullTranscript pSpec₁) :
    FullTranscript pSpec₂ :=
  fun i => _root_.cast (congrFun (congrArg getType hSpec) i) (T (Fin.cast h.symm i))

@[simp]
theorem cast_id : FullTranscript.cast rfl rfl = (id : pSpec₁.FullTranscript → _) := rfl

instance instDepCast₂ : DepCast₂ Nat ProtocolSpec (fun _ pSpec => FullTranscript pSpec) where
  dcast₂ h h' T := FullTranscript.cast h h' T
  dcast₂_id := cast_id

theorem cast_eq_dcast₂ (h : m = n) (hSpec : dcast h pSpec₁ = pSpec₂) (T : FullTranscript pSpec₁) :
    dcast₂ h hSpec T = FullTranscript.cast h hSpec T := rfl

end Cast

end FullTranscript

end ProtocolSpec

/-! ### Casting Verifiers -/

section Cast

variable {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n}
variable {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type}

/-- To cast the verifier, we only need to cast the transcript. -/
def Verifier.cast
    (h : m = n) (hSpec : dcast h pSpec₁ = pSpec₂)
    (V : Verifier pSpec₁ oSpec StmtIn StmtOut) :
    Verifier pSpec₂ oSpec StmtIn StmtOut where
  verify := fun stmt transcript => V.verify stmt (dcast₂ h.symm (dcast_symm h hSpec) transcript)

@[simp]
def Verifier.cast_id
    (V : Verifier pSpec₁ oSpec StmtIn StmtOut) :
      V.cast rfl rfl = V := by
  ext; simp [Verifier.cast]

instance instDepCast₂Verifier :
    DepCast₂ Nat ProtocolSpec (fun _ pSpec => Verifier pSpec oSpec StmtIn StmtOut) where
  dcast₂ := Verifier.cast
  dcast₂_id := by intros; funext; simp

end Cast