ectx_language.v 11 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
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 32 33 34 35 36 37

    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;

38
    mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
39 40
      fill K e1 = fill K' e1' 
      to_val e1 = None 
41
      head_step e1' σ1 κ e2 σ2 efs 
42 43 44 45 46 47 48 49 50
       K'', K' = comp_ectx K K'';
  }.
End ectx_language_mixin.

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

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

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

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

(* From an ectx_language, we can construct a language. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Section ectx_language.
74 75 76 77 78 79
  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 *)
80
  Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
81 82 83 84 85 86 87 88 89 90 91 92
  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.
93
  Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
94 95
    fill K e1 = fill K' e1' 
    to_val e1 = None 
96
    head_step e1' σ1 κ e2 σ2 efs 
97 98
     K'', K' = comp_ectx K K''.
  Proof. apply ectx_language_mixin. Qed.
99

100
  Definition head_reducible (e : expr Λ) (σ : state Λ) :=
101
     κ e' σ' efs, head_step e σ κ e' σ' efs.
Ralf Jung's avatar
Ralf Jung committed
102
  Definition head_reducible_no_obs (e : expr Λ) (σ : state Λ) :=
103
     e' σ' efs, head_step e σ [] e' σ' efs.
104
  Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
105
     κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
106
  Definition head_stuck (e : expr Λ) (σ : state Λ) :=
Glen Mével's avatar
Glen Mével committed
107
    to_val e = None  head_irreducible e σ.
108

109 110
  (* All non-value redexes are at the root.  In other words, all sub-redexes are
     values. *)
111
  Definition sub_redexes_are_values (e : expr Λ) :=
112
     K e', e = fill K e'  to_val e' = None  K = empty_ectx.
113

114
  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
115
      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117
    Ectx_step K e1' e2' :
      e1 = fill K e1'  e2 = fill K e2' 
118
      head_step e1' σ1 κ e2' σ2 efs  prim_step e1 σ1 κ e2 σ2 efs.
119

120 121
  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.
122 123
  Proof. econstructor; eauto. Qed.

124 125 126 127 128
  Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
  Proof.
    split.
    - apply ectx_language_mixin.
    - apply ectx_language_mixin.
129
    - intros ?????? [??? -> -> ?%val_head_stuck].
130 131
      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
  Qed.
132

133
  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
134

Ralf Jung's avatar
Ralf Jung committed
135
  Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
136 137
     σ κ e' σ' efs,
      head_step e σ κ e' σ' efs 
138
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
139

140
  (* Some lemmas about this language *)
141 142 143
  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.

144 145
  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
146 147
  Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.

Ralf Jung's avatar
Ralf Jung committed
148 149 150
  Lemma head_reducible_no_obs_reducible e σ :
    head_reducible_no_obs e σ  head_reducible e σ.
  Proof. intros (?&?&?&?). eexists. eauto. Qed.
151 152 153
  Lemma not_head_reducible e σ : ¬head_reducible e σ  head_irreducible e σ.
  Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.

Dan Frumin's avatar
Dan Frumin committed
154 155 156 157 158 159 160 161 162 163 164 165

  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.
166 167 168 169 170
  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
171
  Lemma head_prim_reducible e σ : head_reducible e σ  reducible e σ.
172
  Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
Dan Frumin's avatar
Dan Frumin committed
173 174 175
  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
Ralf Jung committed
176 177
  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.
178 179 180 181
  Lemma head_prim_irreducible e σ : irreducible e σ  head_irreducible e σ.
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
  Qed.
182
  Lemma head_prim_fill_reducible_no_obs e K σ :
183 184
    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.
185 186

  Lemma prim_head_reducible e σ :
187
    reducible e σ  sub_redexes_are_values e  head_reducible e σ.
188
  Proof.
189
    intros (κ&e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
190
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
191 192 193
    rewrite fill_empty /head_reducible; eauto.
  Qed.
  Lemma prim_head_irreducible e σ :
194
    head_irreducible e σ  sub_redexes_are_values e  irreducible e σ.
195 196 197
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
  Qed.
198

199 200
  Lemma head_stuck_stuck e σ :
    head_stuck e σ  sub_redexes_are_values e  stuck e σ.
201
  Proof.
Glen Mével's avatar
Glen Mével committed
202 203
    intros [] ?. split; first done.
    by apply prim_head_irreducible.
204 205
  Qed.

Ralf Jung's avatar
Ralf Jung committed
206 207
  Lemma ectx_language_atomic a e :
    head_atomic a e  sub_redexes_are_values e  Atomic a e.
208
  Proof.
209
    intros Hatomic_step Hatomic_fill σ κ e' σ' efs [K e1' e2' -> -> Hstep].
210
    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
211 212 213
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
  Qed.

214
  Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs :
215
    head_reducible e1 σ1 
216 217
    prim_step e1 σ1 κ e2 σ2 efs 
    head_step e1 σ1 κ e2 σ2 efs.
218
  Proof.
219 220
    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
221
      as [K' [-> _]%symmetry%ectx_positive];
222
      eauto using fill_empty, fill_not_val, val_head_stuck.
223 224 225
    by rewrite !fill_empty.
  Qed.

226
  (* Every evaluation context is a context. *)
227
  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
228
  Proof.
229
    split; simpl.
230
    - eauto using fill_not_val.
231
    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
232
      by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
233 234
    - 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
235
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
236 237 238
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
239

240
  Record pure_head_step (e1 e2 : expr Λ) := {
241 242
    pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
    pure_head_step_det σ1 κ e2' σ2 efs :
243
      head_step e1 σ1 κ e2' σ2 efs  κ = []  σ2 = σ1  e2' = e2  efs = []
244 245 246
  }.

  Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2  pure_step e1 e2.
Dan Frumin's avatar
Dan Frumin committed
247
  Proof.
248 249
    intros [Hp1 Hp2]. split.
    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
Ralf Jung's avatar
Ralf Jung committed
250
      eexists e2', σ2, efs. by apply head_prim_step.
251
    - intros σ1 κ e2' σ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
Dan Frumin's avatar
Dan Frumin committed
252
  Qed.
253

254 255 256
  Global Instance pure_exec_fill K φ n e1 e2 :
    PureExec φ n e1 e2 
    PureExec φ n (fill K e1) (fill K e2).
257
  Proof. apply: pure_exec_ctx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
End ectx_language.
259

260 261 262
Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.

Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265 266 267 268 269
(* 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. *)
270
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
271 272 273
  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)).