-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlattice.v
157 lines (114 loc) · 4.67 KB
/
lattice.v
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
From Coq.ssr Require Import ssreflect.
From stdpp Require Import base prelude list gmap.
Class Lattice (A : Type) := {
lat_equiv :> Equiv A;
lat_equiv_equiv :> Equivalence lat_equiv;
lat_equiv_dec :> RelDecision lat_equiv;
join : A → A → A;
join_proper :> Proper ((≡) ==> (≡) ==> (≡)) join;
join_commutative :> Comm (≡) join;
join_associative :> Assoc (≡) join;
join_idempotent :> IdemP (≡) join;
bot : A;
bot_left_id :> LeftId (≡) bot join;
bot_right_id :> RightId (≡) bot join;
top : A;
top_left_absorb :> LeftAbsorb (≡) top join;
top_right_absorb :> RightAbsorb (≡) top join;
}.
Class SecurityLattice (label : Type) := {
lattice :> Lattice label;
ζ : label; (* attacker/observer *)
}.
Infix "⊔" := join (at level 50) : stdpp_scope.
Notation "⊥" := bot : stdpp_scope.
Notation "⊤" := top : stdpp_scope.
Section Order.
Context `{lattice : Lattice label}.
Implicit Types a b : label.
Definition order a b := a ⊔ b ≡ b.
Global Instance ord_reflexive : Reflexive order.
Proof. by move=> ?; rewrite /order idemp. Qed.
Global Instance ord_antisymmetric : Antisymmetric label (≡) order.
Proof. by rewrite /order => x y Ho1 Ho2; rewrite -Ho1 -{1}Ho2 (comm _ x). Qed.
Global Instance ord_transitive : Transitive order.
Proof. by rewrite /order => ??? Ho1 Ho2; rewrite -Ho2 assoc Ho1. Qed.
Lemma ord_bottom x : order ⊥ x.
Proof. by rewrite /order left_id. Qed.
Lemma ord_top x : order x ⊤.
Proof. by rewrite /order right_absorb. Qed.
Global Instance order_proper : Proper ((≡) ==> (≡) ==> iff) order.
Proof. by intros x y Hxy u v Huv; rewrite /order Hxy Huv. Qed.
Global Instance order_dec : RelDecision order.
Proof. intros x y. by destruct (decide (x ⊔ y ≡ y)); [left|right]. Qed.
End Order.
Notation "a ⊑ b" := (order a b) (at level 70) : stdpp_scope.
Notation "a ⋢ b" := (¬ (order a b)) (at level 70) : stdpp_scope.
Global Hint Extern 3 => apply ord_bottom : core.
Global Hint Extern 6 => rewrite bot_left_id : core.
Global Hint Extern 6 => rewrite bot_right_id : core.
Section Lemmas.
Context `{lattice : Lattice label}.
Implicit Types ℓ : label.
Lemma ord_join_left ℓ1 ℓ2: ℓ1 ⊑ ℓ1 ⊔ ℓ2.
Proof. by rewrite /order assoc idemp. Qed.
Lemma ord_join_right ℓ1 ℓ2: ℓ1 ⊑ ℓ2 ⊔ ℓ1.
Proof. rewrite comm; apply ord_join_left. Qed.
Lemma ord_join_left' ℓ1 ℓ2 ℓ3 : ℓ1 ⊑ ℓ2 → ℓ1 ⊑ ℓ2 ⊔ ℓ3.
Proof. by rewrite /order assoc => ->. Qed.
Lemma ord_join_right' ℓ1 ℓ2 ℓ3 : ℓ1 ⊑ ℓ3 → ℓ1 ⊑ ℓ2 ⊔ ℓ3.
Proof. rewrite comm; apply ord_join_left'. Qed.
Lemma join_ord_inv ℓ1 ℓ2 ℓ3 : ℓ1 ⊔ ℓ2 ⊑ ℓ3 → ℓ1 ⊑ ℓ3 ∧ ℓ2 ⊑ ℓ3.
Proof.
intros.
assert (ℓ1 ⊑ ℓ1 ⊔ ℓ2) by apply ord_join_left.
assert (ℓ2 ⊑ ℓ1 ⊔ ℓ2) by apply ord_join_right.
split; eapply ord_transitive; eauto.
Qed.
Lemma join_ord ℓ1 ℓ2 ℓ3 : ℓ1 ⊑ ℓ3 → ℓ2 ⊑ ℓ3 → ℓ1 ⊔ ℓ2 ⊑ ℓ3.
Proof. rewrite /order -join_associative => + -> //. Qed.
Lemma ord_join_neg_left ℓ1 ℓ2 ℓ3 : ℓ1 ⋢ ℓ3 → ℓ1 ⊔ ℓ2 ⋢ ℓ3.
Proof. move=> ? /join_ord_inv [? ?] //. Qed.
Lemma ord_join_neg_right ℓ1 ℓ2 ℓ3 : ℓ1 ⋢ ℓ3 → ℓ2 ⊔ ℓ1 ⋢ ℓ3.
Proof. rewrite join_commutative. apply ord_join_neg_left. Qed.
Lemma ord_neg_left ℓ1 ℓ2 ℓ3 : ℓ1 ⊑ ℓ2 → ℓ1 ⋢ ℓ3 → ℓ2 ⋢ ℓ3.
Proof.
intros H1 H2. case (bool_decide (ℓ2 ⊑ ℓ3)) eqn:Heq.
- apply bool_decide_eq_true in Heq.
assert (ℓ1 ⊑ ℓ3); first by etransitivity.
contradiction.
- by apply bool_decide_eq_false in Heq.
Qed.
End Lemmas.
(** Example lattices *)
Section TwoPoint.
Inductive tplabel := L | H.
Global Instance tplabel_eq_dec : EqDecision tplabel.
Proof. intros ??; rewrite /Decision; decide equality. Qed.
Implicit Types ℓ : tplabel.
Definition join_tplabel ℓ ℓ' :=
match ℓ with
| L => ℓ'
| H => H
end.
Instance tp_commutative : Comm (=) join_tplabel.
Proof. by do 2 case. Qed.
Instance tp_associative : Assoc (=) join_tplabel.
Proof. by do 3 case. Qed.
Instance tp_idempotent : IdemP (=) join_tplabel.
Proof. by case. Qed.
Instance L_left_id : LeftId (=) L join_tplabel.
Proof. by case. Qed.
Instance L_right_id : RightId (=) L join_tplabel.
Proof. by case. Qed.
Instance H_left_absorb : LeftAbsorb (=) H join_tplabel.
Proof. by case. Qed.
Instance H_right_absorb : RightAbsorb (=) H join_tplabel.
Proof. by case. Qed.
Global Instance tpLattice : Lattice tplabel :=
{
join := join_tplabel;
lat_equiv := (=);
bot := L;
}.
End TwoPoint.