-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmetatheory.v
232 lines (213 loc) · 9.72 KB
/
metatheory.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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.
From iris.prelude Require Import options.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
(* Closed expressions and values. *)
Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
match e with
| Val v => is_closed_val v
| Var x => bool_decide (x ∈ X)
| Rec f x e => is_closed_expr (f :b: x :b: X) e
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
is_closed_expr X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
is_closed_expr X e1 && is_closed_expr X e2
| If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
| NewProph => true
end
with is_closed_val (v : val) : bool :=
match v with
| LitV _ => true
| RecV f x e => is_closed_expr (f :b: x :b: []) e
| PairV v1 v2 => is_closed_val v1 && is_closed_val v2
| InjLV v | InjRV v => is_closed_val v
end.
Lemma is_closed_weaken X Y e : is_closed_expr X e → X ⊆ Y → is_closed_expr Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed_expr [] e → is_closed_expr X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x v :
is_closed_val v → is_closed_expr (x :: X) e → is_closed_expr X (subst x v e).
Proof.
intros Hv. revert X.
induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
try match goal with
| H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_subst' X e x v :
is_closed_val v → is_closed_expr (x :b: X) e → is_closed_expr X (subst' x v e).
Proof. destruct x; eauto using is_closed_subst. Qed.
(* Substitution *)
Lemma subst_is_closed X e x es : is_closed_expr X e → x ∉ X → subst x es e = e.
Proof.
revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma subst_is_closed_nil e x v : is_closed_expr [] e → subst x v e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
Lemma subst_subst e x v v' :
subst x v (subst x v' e) = subst x v' e.
Proof.
intros. induction e; simpl; try (f_equal; by auto);
simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x v v' :
subst' x v (subst' x v' e) = subst' x v' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.
Lemma subst_subst_ne e x y v v' :
x ≠ y → subst x v (subst y v' e) = subst y v' (subst x v e).
Proof.
intros. induction e; simpl; try (f_equal; by auto);
simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y v v' :
x ≠ y → subst' x v (subst' y v' e) = subst' y v' (subst' x v e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.
Lemma subst_rec' f y e x v :
x = f ∨ x = y ∨ x = BAnon →
subst' x v (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x v :
(x ≠ f ∨ f = BAnon) → (x ≠ y ∨ y = BAnon) →
subst' x v (Rec f y e) = Rec f y (subst' x v e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma bin_op_eval_closed op v1 v2 v' :
is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
is_closed_val v'.
Proof.
rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
repeat case_match; by naive_solver.
Qed.
Lemma heap_closed_alloc σ l n w :
(0 < n)%Z ∧ (l ≠ null_loc) →
is_closed_val w →
map_Forall (λ _ v, from_option is_closed_val true v) (heap σ) →
(∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
map_Forall (λ _ v, from_option is_closed_val true v)
(heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
Proof.
intros Hn Hw Hσ Hl.
eapply (map_Forall_ind
(λ k v, ((heap_array l (replicate (Z.to_nat n) w) ∪ heap σ)
!! k = Some v))).
- apply map_Forall_empty.
- intros m i x Hi Hix Hkwm Hm.
apply map_Forall_insert_2; auto.
apply lookup_union_Some in Hix; last first.
{ eapply heap_array_map_disjoint;
rewrite replicate_length Z2Nat.id; auto with lia. }
destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
[j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
+ simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
+ apply map_Forall_to_list in Hσ.
by eapply Forall_lookup in Hσ; eauto; simpl in *.
- apply map_Forall_to_list, Forall_forall.
intros [? ?]; apply elem_of_map_to_list.
Qed.
(* The stepping relation preserves closedness *)
Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
is_closed_expr [] e1 →
map_Forall (λ _ v, from_option is_closed_val true v) σ1.(heap) →
head_step e1 σ1 obs e2 σ2 es →
is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
map_Forall (λ _ v, from_option is_closed_val true v) σ2.(heap).
Proof.
intros Cl1 Clσ1 STEP.
induction STEP; simpl in *; split_and!;
try apply map_Forall_insert_2; try by naive_solver.
- subst. repeat apply is_closed_subst'; naive_solver.
- unfold un_op_eval in *. repeat case_match; naive_solver.
- eapply bin_op_eval_closed; eauto; naive_solver.
- by apply heap_closed_alloc.
- select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
- select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
- case_match; try apply map_Forall_insert_2; by naive_solver.
Qed.
Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
match e with
| Val _ => e
| Var y => if vs !! y is Some v then Val v else Var y
| Rec f y e => Rec f y (subst_map (binder_delete y (binder_delete f vs)) e)
| App e1 e2 => App (subst_map vs e1) (subst_map vs e2)
| UnOp op e => UnOp op (subst_map vs e)
| BinOp op e1 e2 => BinOp op (subst_map vs e1) (subst_map vs e2)
| If e0 e1 e2 => If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
| Pair e1 e2 => Pair (subst_map vs e1) (subst_map vs e2)
| Fst e => Fst (subst_map vs e)
| Snd e => Snd (subst_map vs e)
| InjL e => InjL (subst_map vs e)
| InjR e => InjR (subst_map vs e)
| Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
| Fork e => Fork (subst_map vs e)
| AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
| Free e => Free (subst_map vs e)
| Load e => Load (subst_map vs e)
| Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
| CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
| FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
| NewProph => NewProph
| Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
end.
Lemma subst_map_empty e : subst_map ∅ e = e.
Proof.
assert (∀ x, binder_delete x (∅:gmap _ val) = ∅) as Hdel.
{ intros [|x]; by rewrite /= ?delete_empty. }
induction e; simplify_map_eq; rewrite ?Hdel; auto with f_equal.
Qed.
Lemma subst_map_insert x v vs e :
subst_map (<[x:=v]>vs) e = subst x v (subst_map (delete x vs) e).
Proof.
revert vs. induction e=> vs; simplify_map_eq; auto with f_equal.
- match goal with
| |- context [ <[?x:=_]> _ !! ?y ] =>
destruct (decide (x = y)); simplify_map_eq=> //
end. by case (vs !! _); simplify_option_eq.
- destruct (decide _) as [[??]|[<-%dec_stable|[<-%dec_stable ?]]%not_and_l_alt].
+ rewrite !binder_delete_insert // !binder_delete_delete; eauto with f_equal.
+ by rewrite /= delete_insert_delete delete_idemp.
+ by rewrite /= binder_delete_insert // delete_insert_delete
!binder_delete_delete delete_idemp.
Qed.
Lemma subst_map_singleton x v e :
subst_map {[x:=v]} e = subst x v e.
Proof. by rewrite subst_map_insert delete_empty subst_map_empty. Qed.
Lemma subst_map_binder_insert b v vs e :
subst_map (binder_insert b v vs) e =
subst' b v (subst_map (binder_delete b vs) e).
Proof. destruct b; rewrite ?subst_map_insert //. Qed.
Lemma subst_map_binder_insert_empty b v e :
subst_map (binder_insert b v ∅) e = subst' b v e.
Proof. by rewrite subst_map_binder_insert binder_delete_empty subst_map_empty. Qed.
Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e :
subst_map (binder_insert b1 v1 (binder_insert b2 v2 vs)) e =
subst' b2 v2 (subst' b1 v1 (subst_map (binder_delete b2 (binder_delete b1 vs)) e)).
Proof.
destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert.
rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|].
- by rewrite delete_idemp subst_subst delete_insert_delete.
- by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
Qed.
Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e :
subst_map (binder_insert b1 v1 (binder_insert b2 v2 ∅)) e =
subst' b2 v2 (subst' b1 v1 e).
Proof.
by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
Qed.
(* subst_map on closed expressions *)
Lemma subst_map_is_closed X e vs :
is_closed_expr X e →
(∀ x, x ∈ X → vs !! x = None) →
subst_map vs e = e.
Proof.
revert X vs. assert (∀ x x1 x2 X (vs : gmap string val),
(∀ x, x ∈ X → vs !! x = None) →
x ∈ x2 :b: x1 :b: X →
binder_delete x1 (binder_delete x2 vs) !! x = None).
{ intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
induction e=> X vs /= ? HX; repeat case_match; naive_solver eauto with f_equal.
Qed.
Lemma subst_map_is_closed_nil e vs : is_closed_expr [] e → subst_map vs e = e.
Proof. intros. apply subst_map_is_closed with []; set_solver. Qed.