-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAuthority.v
150 lines (133 loc) · 4.41 KB
/
Authority.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
(* Celsius project *)
(* Clément Blaudeau - Lamp@EPFL & Inria 2020-2022 *)
(* ------------------------------------------------------------------------ *)
(* This files describes the semantic authority that our calculus enjoys. It is not used for
soundness *)
From Celsius Require Export Semantics.
Implicit Type (σ: Store) (ρ ω: Env) (l: Loc).
(* ------------------------------------------------------------------------ *)
(** ** Definition *)
Definition authority σ σ' :=
forall l C ω, getObj σ l = Some(C, ω) -> exists ω', getObj σ' l = Some(C, ω') /\ dom ω >= dom ω'.
Global Instance notation_authority_store : notation_authority Store :=
{ authority_ := authority }.
Local Hint Unfold notation_authority_store: notations.
Local Hint Unfold authority : aty.
(* ------------------------------------------------------------------------ *)
(** ** Basic results *)
(** The relation is trivially reflexive and transitive *)
Lemma aty_refl: forall σ,
σ ▷ σ.
Proof.
intros ? ? ; eauto with aty.
Qed.
Global Hint Resolve aty_refl: aty.
Lemma aty_trans : forall σ1 σ2 σ3,
σ1 ▷ σ2 ->
σ2 ▷ σ3 ->
σ1 ▷ σ3.
Proof.
intros. intros ?; intros.
specialize (H l C ω); steps.
specialize (H0 l C ω'); steps; eauto with aty lia.
Qed.
Global Hint Resolve aty_trans: aty.
Ltac aty_trans :=
repeat match goal with
| H:_ |- ?σ ▷ ?σ => apply aty_refl
| H: ?σ1 ▷ ?σ2 |- ?σ1 ▷ ?σ3 => apply aty_trans with σ2 ; [ assumption | ]
| H: ?σ2 ▷ ?σ3 |- ?σ1 ▷ ?σ3 => apply aty_trans with σ2 ; [ | assumption ]
end.
Global Hint Extern 1 => aty_trans: aty.
(** We have a result on the store sizes *)
Lemma aty_domains:
forall σ σ',
σ ▷ σ' -> dom σ <= dom σ'.
Proof.
intros.
destruct σ eqn:Σ; simpl; [lia |].
destruct o as [C ω].
specialize (H (dom s)).
destruct (getObj ((C, ω)::s) (dom s)) eqn: H__e.
- destruct o as [D ω'].
apply H in H__e; steps.
apply getObj_dom in H1; auto.
- unfold getObj in H__e.
apply nth_error_None in H__e.
simpl in H__e; lia.
Qed.
Global Hint Resolve aty_domains: aty.
(* ------------------------------------------------------------------------ *)
(** ** Authority theorem *)
(** We start with two technical results on authority for assignment (update) and fresh
location *)
Lemma aty_assignment :
forall σ l C ω ω',
getObj σ l = Some (C, ω) ->
length ω >= length ω' ->
σ ▷ [l ↦ (C, ω')]σ.
Proof.
intros. introv ?.
lets: getObj_dom H.
destruct_eq (l = l0); subst;
updates; eauto with lia.
Qed.
Global Hint Resolve aty_assignment: aty.
Lemma aty_freshness :
forall σ c ρ,
σ ▷ (σ ++ [(c, ρ)]).
Proof.
intros. introv ?.
lets: getObj_dom H.
exists ω; steps;
try rewrite getObj_last2;
eauto with updates.
Qed.
Global Hint Resolve aty_freshness: aty.
(** Then we have the main result *)
Theorem aty_theorem:
(forall e σ ρ ψ v σ',
⟦e⟧ (σ, ρ, ψ) --> (v, σ') -> σ ▷ σ') /\
(forall el σ ρ ψ vl σ',
⟦_ el _⟧p (σ, ρ, ψ) --> (vl, σ') -> σ ▷ σ') /\
(forall C ψ x ρ σ σ',
initP C ψ x ρ σ σ' ->
[ψ ↦ (C,[])]σ ▷ [ψ ↦ (C, [])]σ').
Proof with (updates; cross_rewrites; eauto 3 with aty updates lia).
eapply evalP_multi_ind;
unfold assign; intros;
repeat destruct_match; eval_dom;
flatten; aty_trans; try discriminate ...
- (* e_new *)
intros l D ?ω H__get; steps.
specialize (IH__init l D ω).
lets: getObj_dom H__get...
repeat rewrite getObj_update_diff in IH__init...
rewrite getObj_last2 in IH__init...
- (* init_cons *)
lets: assign_new_dom H__assign.
intros l ?D ?ω H__obj...
destruct (getObj σ I) as [[?D ?ω]|] eqn:H2.
+ lets: IH__e I H2; steps.
rewrite /assign_new H4 in H__assign...
destruct_if_eqb; inverts H__assign;
destruct_eq (I = l); subst...
+ destruct_eq (I = l); subst...
destruct (getObj σ1 I) as [[?D ?ω]|] eqn:H4;
rewrite /assign_new H4 in H__assign;
try destruct_if_eqb; inverts H__assign...
Qed.
Corollary aty_theorem_expr:
forall e σ ρ ψ v σ',
⟦e⟧ (σ, ρ, ψ) --> (v, σ') -> σ ▷ σ'.
Proof.
apply aty_theorem.
Qed.
Global Hint Resolve aty_theorem: aty.
Corollary aty_theorem_list:
forall el σ ρ ψ vl σ',
⟦_ el _⟧p (σ, ρ, ψ) --> (vl, σ') -> σ ▷ σ'.
Proof.
apply aty_theorem.
Qed.
Global Hint Resolve aty_theorem_list: aty.