ectx_language.v 13.3 KB
Newer Older
1
2
(** An axiomatization of evaluation-context based languages, including a proof
    that this gives rise to a "language" in the Iris sense. *)
3
From iris.algebra Require Export base.
4
From iris.program_logic Require Import language.
5
Set Default Proof Using "Type".
6

Ralf Jung's avatar
Ralf Jung committed
7
(** TAKE CARE: When you define an [ectxLanguage] canonical structure for your
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
language, you need to also define a corresponding [language] canonical
structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
file for doing that. *)

12
Section ectx_language_mixin.
13
  Context {expr val ectx state observation : Type}.
14
15
16
17
18
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
  Context (empty_ectx : ectx).
  Context (comp_ectx : ectx  ectx  ectx).
  Context (fill : ectx  expr  expr).
19
  Context (head_step : expr  state  list observation  expr  state  list expr  Prop).
20
21
22
23

  Record EctxLanguageMixin := {
    mixin_to_of_val v : to_val (of_val v) = Some v;
    mixin_of_to_val e v : to_val e = Some v  of_val v = e;
24
25
    mixin_val_head_stuck e1 σ1 κ e2 σ2 efs :
      head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None;
26
27
28
29
30
31

    mixin_fill_empty e : fill empty_ectx e = e;
    mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
    mixin_fill_inj K : Inj (=) (=) (fill K);
    mixin_fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e);

32
33
34
35
36
    (** Given a head redex [e1_redex] somewhere in a term, and another
        decomposition of the same term into [fill K' e1'] such that [e1'] is not
        a value, then the head redex context is [e1']'s context [K'] filled with
        another context [K''].  In particular, this implies [e1 = fill K''
        e1_redex] by [fill_inj], i.e., [e1]' contains the head redex.)
Ralf Jung's avatar
Ralf Jung committed
37

Ralf Jung's avatar
Ralf Jung committed
38
        This implies there can be only one head redex, see
Ralf Jung's avatar
Ralf Jung committed
39
        [head_redex_unique]. *)
40
41
42
43
44
    mixin_step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
      fill K' e1' = fill K_redex e1_redex 
      to_val e1' = None 
      head_step e1_redex σ1 κ e2 σ2 efs 
       K'', K_redex = comp_ectx K' K'';
Amin Timany's avatar
Amin Timany committed
45

Ralf Jung's avatar
Ralf Jung committed
46
47
48
    (** If [fill K e] takes a head step, then either [e] is a value or [K] is
        the empty evaluation context. In other words, if [e] is not a value
        wrapping it in a context does not add new head redex positions. *)
Amin Timany's avatar
Amin Timany committed
49
50
    mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
      head_step (fill K e) σ1 κ e2 σ2 efs  is_Some (to_val e)  K = empty_ectx;
51
52
53
54
55
56
57
58
  }.
End ectx_language_mixin.

Structure ectxLanguage := EctxLanguage {
  expr : Type;
  val : Type;
  ectx : Type;
  state : Type;
59
  observation : Type;
60

61
62
63
64
65
  of_val : val  expr;
  to_val : expr  option val;
  empty_ectx : ectx;
  comp_ectx : ectx  ectx  ectx;
  fill : ectx  expr  expr;
66
  head_step : expr  state  list observation  expr  state  list expr  Prop;
67

68
69
  ectx_language_mixin :
    EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
70
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72
73
74
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.

75
Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
76
77
Arguments of_val {_} _.
Arguments to_val {_} _.
78
79
Arguments empty_ectx {_}.
Arguments comp_ectx {_} _ _.
80
81
Arguments fill {_} _ _.
Arguments head_step {_} _ _ _ _ _ _.
82
83

(* From an ectx_language, we can construct a language. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Section ectx_language.
85
86
87
88
89
90
  Context {Λ : ectxLanguage}.
  Implicit Types v : val Λ.
  Implicit Types e : expr Λ.
  Implicit Types K : ectx Λ.

  (* Only project stuff out of the mixin that is not also in language *)
91
  Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
92
93
94
95
96
97
98
99
100
  Proof. apply ectx_language_mixin. Qed.
  Lemma fill_empty e : fill empty_ectx e = e.
  Proof. apply ectx_language_mixin. Qed.
  Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
  Proof. apply ectx_language_mixin. Qed.
  Global Instance fill_inj K : Inj (=) (=) (fill K).
  Proof. apply ectx_language_mixin. Qed.
  Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
  Proof. apply ectx_language_mixin. Qed.
101
102
103
104
105
  Lemma step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
      fill K' e1' = fill K_redex e1_redex 
      to_val e1' = None 
      head_step e1_redex σ1 κ e2 σ2 efs 
       K'', K_redex = comp_ectx K' K''.
106
  Proof. apply ectx_language_mixin. Qed.
Amin Timany's avatar
Amin Timany committed
107
108
109
  Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs :
    head_step (fill K e) σ1 κ e2 σ2 efs  is_Some (to_val e)  K = empty_ectx.
  Proof. apply ectx_language_mixin. Qed.
110

111
  Definition head_reducible (e : expr Λ) (σ : state Λ) :=
112
     κ e' σ' efs, head_step e σ κ e' σ' efs.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
113
  Definition head_reducible_no_obs (e : expr Λ) (σ : state Λ) :=
114
     e' σ' efs, head_step e σ [] e' σ' efs.
115
  Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
116
     κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
117
  Definition head_stuck (e : expr Λ) (σ : state Λ) :=
Glen Mével's avatar
Glen Mével committed
118
    to_val e = None  head_irreducible e σ.
119

120
121
  (* All non-value redexes are at the root.  In other words, all sub-redexes are
     values. *)
122
  Definition sub_redexes_are_values (e : expr Λ) :=
123
     K e', e = fill K e'  to_val e' = None  K = empty_ectx.
124

125
  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
126
      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
    Ectx_step K e1' e2' :
      e1 = fill K e1'  e2 = fill K e2' 
129
      head_step e1' σ1 κ e2' σ2 efs  prim_step e1 σ1 κ e2 σ2 efs.
130

131
132
  Lemma Ectx_step' K e1 σ1 κ e2 σ2 efs :
    head_step e1 σ1 κ e2 σ2 efs  prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
133
134
  Proof. econstructor; eauto. Qed.

135
136
137
138
139
  Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
  Proof.
    split.
    - apply ectx_language_mixin.
    - apply ectx_language_mixin.
140
    - intros ?????? [??? -> -> ?%val_head_stuck].
141
142
      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
  Qed.
143

144
  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
145

Ralf Jung's avatar
Ralf Jung committed
146
  Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
147
148
     σ κ e' σ' efs,
      head_step e σ κ e' σ' efs 
Ralf Jung's avatar
Ralf Jung committed
149
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
150

Ralf Jung's avatar
Ralf Jung committed
151
  (** * Some lemmas about this language *)
152
153
154
  Lemma fill_not_val K e : to_val e = None  to_val (fill K e) = None.
  Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.

Ralf Jung's avatar
fix TWP    
Ralf Jung committed
155
156
157
  Lemma head_reducible_no_obs_reducible e σ :
    head_reducible_no_obs e σ  head_reducible e σ.
  Proof. intros (?&?&?&?). eexists. eauto. Qed.
158
159
160
  Lemma not_head_reducible e σ : ¬head_reducible e σ  head_irreducible e σ.
  Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.

Ralf Jung's avatar
Ralf Jung committed
161
162
163
164
165
  (** The decomposition into head redex and context is unique.

      In all sensible instances, [comp_ectx K' empty_ectx] will be the same as
      [K'], so the conclusion is [K = K' ∧ e = e'], but we do not require a law
      to actually prove that so we cannot use that fact here. *)
Ralf Jung's avatar
Ralf Jung committed
166
167
168
169
170
171
172
  Lemma head_redex_unique K K' e e' σ :
    fill K e = fill K' e' 
    head_reducible e σ 
    head_reducible e' σ 
    K = comp_ectx K' empty_ectx  e = e'.
  Proof.
    intros Heq (κ & e2 & σ2 & efs & Hred) (κ' & e2' & σ2' & efs' & Hred').
Ralf Jung's avatar
Ralf Jung committed
173
174
175
176
177
    edestruct (step_by_val K' K e' e) as [K'' HK];
      [by eauto using val_head_stuck..|].
    subst K. move: Heq. rewrite -fill_comp. intros <-%(inj (fill _)).
    destruct (head_ctx_step_val _ _ _ _ _ _ _ Hred') as [[]%not_eq_None_Some|HK''].
    { by eapply val_head_stuck. }
Ralf Jung's avatar
Ralf Jung committed
178
179
180
181
182
183
184
    subst K''. rewrite fill_empty. done.
  Qed.

  Lemma head_prim_step e1 σ1 κ e2 σ2 efs :
    head_step e1 σ1 κ e2 σ2 efs  prim_step e1 σ1 κ e2 σ2 efs.
  Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.

Amin Timany's avatar
Amin Timany committed
185
186
  Lemma head_step_not_stuck e σ κ e' σ' efs : head_step e σ κ e' σ' efs  not_stuck e σ.
  Proof. rewrite /not_stuck /reducible /=. eauto 10 using head_prim_step. Qed.
Dan Frumin's avatar
Dan Frumin committed
187
188
189
190
191
192
193
194
195
196
197
198

  Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs  prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
  Proof.
    destruct 1 as [K' e1' e2' -> ->].
    rewrite !fill_comp. by econstructor.
  Qed.
  Lemma fill_reducible K e σ : reducible e σ  reducible (fill K e) σ.
  Proof.
    intros (κ&e'&σ'&efs&?). exists κ, (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.
199
200
201
202
203
  Lemma fill_reducible_no_obs K e σ : reducible_no_obs e σ  reducible_no_obs (fill K e) σ.
  Proof.
    intros (e'&σ'&efs&?). exists (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  Lemma head_prim_reducible e σ : head_reducible e σ  reducible e σ.
205
  Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
Dan Frumin's avatar
Dan Frumin committed
206
207
208
  Lemma head_prim_fill_reducible e K σ :
    head_reducible e σ  reducible (fill K e) σ.
  Proof. intro. by apply fill_reducible, head_prim_reducible. Qed.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
209
210
  Lemma head_prim_reducible_no_obs e σ : head_reducible_no_obs e σ  reducible_no_obs e σ.
  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
211
212
213
214
  Lemma head_prim_irreducible e σ : irreducible e σ  head_irreducible e σ.
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
  Qed.
215
  Lemma head_prim_fill_reducible_no_obs e K σ :
216
217
    head_reducible_no_obs e σ  reducible_no_obs (fill K e) σ.
  Proof. intro. by apply fill_reducible_no_obs, head_prim_reducible_no_obs. Qed.
218
219

  Lemma prim_head_reducible e σ :
220
    reducible e σ  sub_redexes_are_values e  head_reducible e σ.
221
  Proof.
222
    intros (κ&e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
223
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
224
225
226
    rewrite fill_empty /head_reducible; eauto.
  Qed.
  Lemma prim_head_irreducible e σ :
227
    head_irreducible e σ  sub_redexes_are_values e  irreducible e σ.
228
229
230
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
  Qed.
231

232
233
  Lemma head_stuck_stuck e σ :
    head_stuck e σ  sub_redexes_are_values e  stuck e σ.
234
  Proof.
Glen Mével's avatar
Glen Mével committed
235
236
    intros [] ?. split; first done.
    by apply prim_head_irreducible.
237
238
  Qed.

Ralf Jung's avatar
Ralf Jung committed
239
240
  Lemma ectx_language_atomic a e :
    head_atomic a e  sub_redexes_are_values e  Atomic a e.
241
  Proof.
242
    intros Hatomic_step Hatomic_fill σ κ e' σ' efs [K e1' e2' -> -> Hstep].
243
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
244
245
246
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
  Qed.

Amin Timany's avatar
Amin Timany committed
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
  Lemma head_reducible_prim_step_ctx K e1 σ1 κ e2 σ2 efs :
    head_reducible e1 σ1 
    prim_step (fill K e1) σ1 κ e2 σ2 efs 
     e2', e2 = fill K e2'  head_step e1 σ1 κ e2' σ2 efs.
  Proof.
    intros (κ'&e2''&σ2''&efs''&?HhstepK) [K' e1' e2' HKe1 -> Hstep].
    edestruct (step_by_val K) as [K'' ?];
      eauto using val_head_stuck; simplify_eq/=.
    rewrite -fill_comp in HKe1; simplify_eq.
    exists (fill K'' e2'). rewrite fill_comp; split; first done.
    apply head_ctx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
    { apply val_head_stuck in Hstep; simplify_eq. }
    by rewrite !fill_empty.
  Qed.

262
  Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs :
263
    head_reducible e1 σ1 
264
265
    prim_step e1 σ1 κ e2 σ2 efs 
    head_step e1 σ1 κ e2 σ2 efs.
266
  Proof.
Amin Timany's avatar
Amin Timany committed
267
268
269
270
    intros.
    edestruct (head_reducible_prim_step_ctx empty_ectx) as (?&?&?);
      rewrite ?fill_empty; eauto.
    by simplify_eq; rewrite fill_empty.
271
272
  Qed.

273
  (* Every evaluation context is a context. *)
274
  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
275
  Proof.
276
    split; simpl.
277
    - eauto using fill_not_val.
278
    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
279
      by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
280
281
    - intros e1 σ1 κ e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
      destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
283
284
285
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
286

287
  Record pure_head_step (e1 e2 : expr Λ) := {
288
289
    pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
    pure_head_step_det σ1 κ e2' σ2 efs :
290
      head_step e1 σ1 κ e2' σ2 efs  κ = []  σ2 = σ1  e2' = e2  efs = []
291
292
293
  }.

  Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2  pure_step e1 e2.
Dan Frumin's avatar
Dan Frumin committed
294
  Proof.
295
296
    intros [Hp1 Hp2]. split.
    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
297
      eexists e2', σ2, efs. by apply head_prim_step.
298
    - intros σ1 κ e2' σ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
Dan Frumin's avatar
Dan Frumin committed
299
  Qed.
300

301
302
303
  Global Instance pure_exec_fill K φ n e1 e2 :
    PureExec φ n e1 e2 
    PureExec φ n (fill K e1) (fill K e2).
304
  Proof. apply: pure_exec_ctx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
End ectx_language.
306

307
308
309
Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.

Robbert Krebbers's avatar
Robbert Krebbers committed
310
311
312
313
314
315
316
(* This definition makes sure that the fields of the [language] record do not
refer to the projections of the [ectxLanguage] record but to the actual fields
of the [ectxLanguage] record. This is crucial for canonical structure search to
work.

Note that this trick no longer works when we switch to canonical projections
because then the pattern match [let '...] will be desugared into projections. *)
317
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
318
319
320
  let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
  @Language E V St K of_val to_val _
    (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).