ectx_language.v 8.48 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

Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
(* TAKE CARE: When you define an [ectxLanguage] canonical structure for your
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
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
Section ectx_language_mixin.
  Context {expr val ectx state : Type}.
  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).
  Context (head_step : expr  state  expr  state  list expr  Prop).

  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;
    mixin_val_head_stuck e1 σ1 e2 σ2 efs :
      head_step e1 σ1 e2 σ2 efs  to_val e1 = None;

    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);

    (* There are a whole lot of sensible axioms (like associativity, and left and
    right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
    positivity suffices. *)
    mixin_ectx_positive K1 K2 :
      comp_ectx K1 K2 = empty_ectx  K1 = empty_ectx  K2 = empty_ectx;

    mixin_step_by_val K K' e1 e1' σ1 e2 σ2 efs :
      fill K e1 = fill K' e1' 
      to_val e1 = None 
      head_step e1' σ1 e2 σ2 efs 
       K'', K' = comp_ectx K K'';
  }.
End ectx_language_mixin.

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

52
53
54
55
56
  of_val : val  expr;
  to_val : expr  option val;
  empty_ectx : ectx;
  comp_ectx : ectx  ectx  ectx;
  fill : ectx  expr  expr;
57
  head_step : expr  state  expr  state  list expr  Prop;
58

59
60
  ectx_language_mixin :
    EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
61
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
62

63
64
65
66
67
68
69
Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
Arguments of_val {_} _%V.
Arguments to_val {_} _%E.
Arguments empty_ectx {_}.
Arguments comp_ectx {_} _ _.
Arguments fill {_} _ _%E.
Arguments head_step {_} _%E _ _%E _ _.
70
71

(* From an ectx_language, we can construct a language. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Section ectx_language.
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
  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 *)
  Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
  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.
  Lemma ectx_positive K1 K2 :
    comp_ectx K1 K2 = empty_ectx  K1 = empty_ectx  K2 = empty_ectx.
  Proof. apply ectx_language_mixin. Qed.
  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
    fill K e1 = fill K' e1' 
    to_val e1 = None 
    head_step e1' σ1 e2 σ2 efs 
     K'', K' = comp_ectx K K''.
  Proof. apply ectx_language_mixin. Qed.
98

99
  Definition head_reducible (e : expr Λ) (σ : state Λ) :=
100
     e' σ' efs, head_step e σ e' σ' efs.
101
  Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
102
103
     e' σ' efs, ¬head_step e σ e' σ' efs.

104
105
  (* All non-value redexes are at the root.  In other words, all sub-redexes are
     values. *)
106
  Definition sub_redexes_are_values (e : expr Λ) :=
107
     K e', e = fill K e'  to_val e' = None  K = empty_ectx.
108

109
110
  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ)
      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
    Ectx_step K e1' e2' :
      e1 = fill K e1'  e2 = fill K e2' 
113
      head_step e1' σ1 e2' σ2 efs  prim_step e1 σ1 e2 σ2 efs.
114

115
116
117
118
  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.
  Proof. econstructor; eauto. Qed.

119
120
121
122
123
124
125
126
  Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
  Proof.
    split.
    - apply ectx_language_mixin.
    - apply ectx_language_mixin.
    - intros ????? [??? -> -> ?%val_head_stuck].
      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
  Qed.
127

128
  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
129

130
  (* Some lemmas about this language *)
131
132
133
  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.

134
135
  Lemma head_prim_step e1 σ1 e2 σ2 efs :
    head_step e1 σ1 e2 σ2 efs  prim_step e1 σ1 e2 σ2 efs.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
  Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.

138
139
140
  Lemma not_head_reducible e σ : ¬head_reducible e σ  head_irreducible e σ.
  Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
141
  Lemma head_prim_reducible e σ : head_reducible e σ  reducible e σ.
142
  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
143
144
145
146
147
148
  Lemma head_prim_irreducible e σ : irreducible e σ  head_irreducible e σ.
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
  Qed.

  Lemma prim_head_reducible e σ :
149
    reducible e σ  sub_redexes_are_values e  head_reducible e σ.
150
151
  Proof.
    intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
152
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
153
154
155
    rewrite fill_empty /head_reducible; eauto.
  Qed.
  Lemma prim_head_irreducible e σ :
156
    head_irreducible e σ  sub_redexes_are_values e  irreducible e σ.
157
158
159
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
  Qed.
160

161
162
163
164
  Lemma ectx_language_atomic e :
    ( σ e' σ' efs, head_step e σ e' σ' efs  irreducible e' σ') 
    sub_redexes_are_values e 
    Atomic e.
165
166
  Proof.
    intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
167
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
168
169
170
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
  Qed.

171
  Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
172
173
    head_reducible e1 σ1 
    prim_step e1 σ1 e2 σ2 efs 
174
    head_step e1 σ1 e2 σ2 efs.
175
  Proof.
176
177
    intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
    destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'')
Robbert Krebbers's avatar
Robbert Krebbers committed
178
      as [K' [-> _]%symmetry%ectx_positive];
179
      eauto using fill_empty, fill_not_val, val_head_stuck.
180
181
182
    by rewrite !fill_empty.
  Qed.

183
  (* Every evaluation context is a context. *)
184
  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
185
  Proof.
186
    split; simpl.
187
188
189
190
    - eauto using fill_not_val.
    - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
      by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
    - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
191
      destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 efs) as [K' ->]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
193
194
195
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
196

197
  Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
198
199
200
201
    ( σ, P  head_reducible e1 σ) 
    ( σ1 e2' σ2 efs,
      P  head_step e1 σ1 e2' σ2 efs  σ1 = σ2  e2=e2'  efs = []) 
    PureExec P e1 e2.
Dan Frumin's avatar
Dan Frumin committed
202
203
  Proof.
    intros Hp1 Hp2. split.
204
205
206
    - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
      eexists e2', σ2, efs. by apply head_prim_step.
    - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
Dan Frumin's avatar
Dan Frumin committed
207
  Qed.
208
209
210
211
212
213

  Global Instance pure_exec_fill K e1 e2 φ :
    PureExec φ e1 e2 
    PureExec φ (fill K e1) (fill K e2).
  Proof. apply: pure_exec_ctx. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
214
End ectx_language.
215

216
217
218
219
220
221
222
Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.

Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
  let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
  @Language E V St of_val to_val _
    (@ectx_lang_mixin (@EctxLanguage E V C St of_val to_val empty comp fill head mix)).