ectx_language.v 6.44 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
7
8

(* We need to make thos arguments indices that we want canonical structure
   inference to use a keys. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Class EctxLanguage (expr val ectx state : Type) := {
10
11
12
13
14
  of_val : val  expr;
  to_val : expr  option val;
  empty_ectx : ectx;
  comp_ectx : ectx  ectx  ectx;
  fill : ectx  expr  expr;
15
  head_step : expr  state  expr  state  list expr  Prop;
16
17
18

  to_of_val v : to_val (of_val v) = Some v;
  of_to_val e v : to_val e = Some v  of_val v = e;
19
  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None;
20
21
22

  fill_empty e : fill empty_ectx e = e;
  fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  fill_inj K :> Inj (=) (=) (fill K);
24
25
  fill_not_val K e : to_val e = None  to_val (fill K e) = None;

Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
  (* 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. *)
29
  ectx_positive K1 K2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
30
    comp_ectx K1 K2 = empty_ectx  K1 = empty_ectx  K2 = empty_ectx;
31

32
  step_by_val K K' e1 e1' σ1 e2 σ2 efs :
33
34
    fill K e1 = fill K' e1' 
    to_val e1 = None 
35
    head_step e1' σ1 e2 σ2 efs 
36
37
    exists K'', K' = comp_ectx K K'';
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

39
40
Arguments of_val {_ _ _ _ _} _%V.
Arguments to_val {_ _ _ _ _} _%E.
41
42
Arguments empty_ectx {_ _ _ _ _}.
Arguments comp_ectx {_ _ _ _ _} _ _.
43
44
Arguments fill {_ _ _ _ _} _ _%E.
Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
45
46
47
48
49
50
51

Arguments to_of_val {_ _ _ _ _} _.
Arguments of_to_val {_ _ _ _ _} _ _ _.
Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
Arguments fill_empty {_ _ _ _ _} _.
Arguments fill_comp {_ _ _ _ _} _ _ _.
Arguments fill_not_val {_ _ _ _ _} _ _ _.
52
Arguments ectx_positive {_ _ _ _ _} _ _ _.
53
54
55
Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.

(* From an ectx_language, we can construct a language. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
Section ectx_language.
  Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
58
59
  Implicit Types (e : expr) (K : ectx).

60
  Definition head_reducible (e : expr) (σ : state) :=
61
     e' σ' efs, head_step e σ e' σ' efs.
62
63
64
65
66
  Definition head_irreducible (e : expr) (σ : state) :=
     e' σ' efs, ¬head_step e σ e' σ' efs.

  Definition sub_values (e : expr) :=
     K e', e = fill K e'  to_val e' = None  K = empty_ectx.
67

68
  Inductive prim_step (e1 : expr) (σ1 : state)
69
      (e2 : expr) (σ2 : state) (efs : list expr) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
    Ectx_step K e1' e2' :
      e1 = fill K e1'  e2 = fill K e2' 
72
      head_step e1' σ1 e2' σ2 efs  prim_step e1 σ1 e2 σ2 efs.
73

74
75
76
77
  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.

78
79
  Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
    prim_step e1 σ1 e2 σ2 efs  to_val e1 = None.
80
81
82
83
84
  Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.

  Canonical Structure ectx_lang : language := {|
    language.expr := expr; language.val := val; language.state := state;
    language.of_val := of_val; language.to_val := to_val;
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    language.prim_step := prim_step;
86
    language.to_of_val := to_of_val; language.of_to_val := of_to_val;
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    language.val_stuck := val_prim_stuck;
88
89
  |}.

90
  (* Some lemmas about this language *)
91
92
  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
93
94
  Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.

95
96
97
  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
98
  Lemma head_prim_reducible e σ : head_reducible e σ  reducible e σ.
99
  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
  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 σ :
    reducible e σ  sub_values e  head_reducible e σ.
  Proof.
    intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
    rewrite fill_empty /head_reducible; eauto.
  Qed.
  Lemma prim_head_irreducible e σ :
    head_irreducible e σ  sub_values e  irreducible e σ.
  Proof.
    rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
  Qed.
117

Robbert Krebbers's avatar
Robbert Krebbers committed
118
  Lemma ectx_language_atomic e :
119
    ( σ e' σ' efs, head_step e σ e' σ' efs  irreducible e' σ') 
120
    sub_values e 
Robbert Krebbers's avatar
Robbert Krebbers committed
121
    Atomic e.
122
  Proof.
123
    intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
126
127
  Qed.

128
  Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
129
130
    head_reducible e1 σ1 
    prim_step e1 σ1 e2 σ2 efs 
131
    head_step e1 σ1 e2 σ2 efs.
132
  Proof.
133
134
    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
135
      as [K' [-> _]%symmetry%ectx_positive];
136
137
138
139
      eauto using fill_empty, fill_not_val, val_stuck.
    by rewrite !fill_empty.
  Qed.

140
141
142
143
144
145
146
147
  (* Every evaluation context is a context. *)
  Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K).
  Proof.
    split.
    - 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].
148
      destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 efs) as [K' ->]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
150
151
152
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
153

154
  Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
155
156
157
158
    ( σ, 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
159
160
  Proof.
    intros Hp1 Hp2. split.
161
162
163
    - 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
164
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
End ectx_language.
166

167
Arguments ectx_lang _ {_ _ _ _}.