constructive-cryptography/src/Examples/Usability.lean at main · trailofbits/constructive-cryptography · 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
import ConstructiveCryptography.Notation

/-!
# Proof commands on interfaces

The CC notation and proof commands on arbitrary interfaces: normalization of attachment and
parallel composition (`cc_normalize`), non-expansion (`cc_nonexpand`), the triangle
inequality (`cc_triangle`), and exact construction (`cc_construct`).
-/

namespace SystemAlgebra.Usability

open CategoryTheory CategoryTheory.MonoidalCategory
open Interface
open scoped SystemAlgebra

variable {A B C : Interface}

example (α : A ⟶ B) (β : B ⟶ C) (R : TypedSystem C) :
    (α ≫ β) • R = α • (β • R) := by
  cc_normalize

example (R : TypedSystem A) : (𝟙 A • R : TypedSystem A) = R := by
  cc_normalize

example {D : Interface} (α : A ⟶ B) (β : C ⟶ D)
    (R : TypedSystem B) (S : TypedSystem D) :
    (α ⊗ₘ β) • (R ∥ S) = (α • R) ∥ (β • S) := by
  cc_normalize

example {D : Interface} (α : A ⟶ B) (β : C ⟶ D)
    (R : TypedSystem B) (S : TypedSystem D) :
    ((α ⊗ₘ β) • (R ∥ S) : TypedSystem (tensor A C)) = (α • R) ∥ (β • S) := by
  cc_normalize

example {D E : Interface} (γ : E ⟶ tensor A C) (α : A ⟶ B) (β : C ⟶ D)
    (R : TypedSystem B) (S : TypedSystem D) :
    (γ ≫ (α ⊗ₘ β)) • (R ∥ S) = γ • ((α • R) ∥ (β • S)) := by
  cc_normalize

example (α : A ⟶ B) (R S : TypedSystem B) : Δ (α • R) (α • S) ≤ Δ R S := by
  cc_nonexpand

example (R S T : TypedSystem A) : Δ R S ≤ Δ R T + Δ T S := by
  cc_triangle via T
  · exact le_rfl
  · exact le_rfl

example (α : A ⟶ B) (β : A ⟶ B) (R S : TypedSystem B) :
    Δ (α • R) (β • S) ≤ Δ R S + Δ (α • S) (β • S) := by
  cc_triangle via (α • S)
  · cc_nonexpand
  · exact le_rfl

example (R S : TypedSystem A) (T : TypedSystem B) : Δ (R ∥ T) (S ∥ T) ≤ Δ R S := by
  cc_nonexpand

example (R : TypedSystem A) (S T : TypedSystem B) : Δ (R ∥ S) (R ∥ T) ≤ Δ S T := by
  cc_nonexpand

example (R S : TypedSystem A) (T U : TypedSystem B) :
    Δ (R ∥ T) (S ∥ U) ≤ Δ R S + Δ T U := by
  cc_nonexpand

example (R S : TypedSystem A) (h : Δ R S ≤ 0) : Δ R S ≤ 0 := by
  fail_if_success cc_nonexpand
  exact h

/-- trace: [ConstructiveCryptography.ProofAutomation.rule] ConstructiveCryptography.CryptographicAlgebra.distance_parallel_left_le -/
#guard_msgs in
set_option trace.ConstructiveCryptography.ProofAutomation.rule true in
example (R S : TypedSystem A) (T : TypedSystem B) : Δ (R ∥ T) (S ∥ T) ≤ Δ R S := by
  cc_nonexpand

example (α : A ⟶ B) (R : TypedSystem B) :
    ({R} —[α]→ {α • R}) := by
  cc_construct using rfl

end SystemAlgebra.Usability