language.v 6.8 KB
Newer Older
1
From iris.algebra Require Export ofe.
2
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
3

4
5
6
7
8
9
10
11
12
13
14
15
16
Section language_mixin.
  Context {expr val state : Type}.
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
  Context (prim_step : expr  state  expr  state  list expr  Prop).

  Record LanguageMixin := {
    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_stuck e σ e' σ' efs : prim_step e σ e' σ' efs  to_val e = None
  }.
End language_mixin.

17
18
19
20
21
22
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
  of_val : val  expr;
  to_val : expr  option val;
23
  prim_step : expr  state  expr  state  list expr  Prop;
24
  language_mixin : LanguageMixin of_val to_val prim_step
Ralf Jung's avatar
Ralf Jung committed
25
}.
Janno's avatar
Janno committed
26
27
28
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr.
29
Bind Scope val_scope with val.
30
31

Arguments Language {_ _ _ _ _ _} _.
32
33
34
35
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.

36
37
38
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
39
40

Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Ralf Jung's avatar
Ralf Jung committed
41

42
Class LanguageCtx {Λ : language} (K : expr Λ  expr Λ) := {
43
44
45
46
47
48
49
50
51
52
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
  fill_step e1 σ1 e2 σ2 efs :
    prim_step e1 σ1 e2 σ2 efs 
    prim_step (K e1) σ1 (K e2) σ2 efs;
  fill_step_inv e1' σ1 e2 σ2 efs :
    to_val e1' = None  prim_step (K e1') σ1 e2 σ2 efs 
     e2', e2 = K e2'  prim_step e1' σ1 e2' σ2 efs
}.

53
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
Proof. constructor; naive_solver. Qed.

Ralf Jung's avatar
Ralf Jung committed
56
Inductive atomicity := StronglyAtomic | WeaklyAtomic.
57

58
Section language.
59
60
  Context {Λ : language}.
  Implicit Types v : val Λ.
61
62
63
64
65
66
67
68
  Implicit Types e : expr Λ.

  Lemma to_of_val v : to_val (of_val v) = Some v.
  Proof. apply language_mixin. Qed.
  Lemma of_to_val e v : to_val e = Some v  of_val v = e.
  Proof. apply language_mixin. Qed.
  Lemma val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs  to_val e = None.
  Proof. apply language_mixin. Qed.
Ralf Jung's avatar
Ralf Jung committed
69

70
  Definition reducible (e : expr Λ) (σ : state Λ) :=
71
     e' σ' efs, prim_step e σ e' σ' efs.
72
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
73
     e' σ' efs, ¬prim_step e σ e' σ' efs.
74
75
  Definition stuck (e : expr Λ) (σ : state Λ) :=
    to_val e = None  irreducible e σ.
76

Ralf Jung's avatar
Ralf Jung committed
77
  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
Ralf Jung's avatar
Ralf Jung committed
78
79
80
81
     invariants when WP ensures safety, i.e., programs never can get stuck.  We
     have an example in lambdaRust of an expression that is atomic in this
     sense, but not in the stronger sense defined below, and we have to be able
     to open invariants around that expression.  See `CasStuckS` in
82
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
83

Ralf Jung's avatar
Ralf Jung committed
84
     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
Ralf Jung's avatar
Ralf Jung committed
85
86
87
88
     safety, we need a stronger form of atomicity.  With the above definition,
     in case `e` reduces to a stuck non-value, there is no proof that the
     invariants have been established again. *)
  Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
89
90
    atomic σ e' σ' efs :
      prim_step e σ e' σ' efs 
Ralf Jung's avatar
Ralf Jung committed
91
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
92

93
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
94
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
95
       ρ1 = (t1 ++ e1 :: t2, σ1) 
96
97
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
       prim_step e1 σ1 e2 σ2 efs 
98
99
       step ρ1 ρ2.

Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
102
103
104

  Lemma not_reducible e σ : ¬reducible e σ  irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
105
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
106
  Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
107
108
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
109
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
110
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Ralf Jung's avatar
Ralf Jung committed
111

112
113
114
  Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e  Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
115

116
117
118
119
120
121
122
123
124
  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
  Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  irreducible e σ  irreducible (K e) σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
125
126
127
128
129
130
131
132
133
134

  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1  t1'  step (t1,σ1) (t2,σ2)   t2', t2  t2'  step (t1',σ1) (t2',σ2).
  Proof.
    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff ()).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
135
136
137
138
139
140
141
142

  Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
    pure_exec_safe σ :
      P  reducible e1 σ;
    pure_exec_puredet σ1 e2' σ2 efs :
      P  prim_step e1 σ1 e2' σ2 efs  σ1 = σ2  e2 = e2'  efs = [];
  }.

143
  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
Dan Frumin's avatar
Dan Frumin committed
144
145
146
    (P  PureExec True e1 e2) 
    PureExec P e1 e2.
  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
147

148
149
  (* We do not make this an instance because it is awfully general. *)
  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
150
151
152
153
    PureExec φ e1 e2 
    PureExec φ (K e1) (K e2).
  Proof.
    intros [Hred Hstep]. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
157
158
    - unfold reducible in *. naive_solver eauto using fill_step.
    - intros σ1 e2' σ2 efs ? Hpstep.
      destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
      + edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
159
160
  Qed.

161
162
163
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
    into_val : to_val e = Some v.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
167
168
169
170
171
172

  Class AsVal (e : expr Λ) := as_val : is_Some (to_val e).
  (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
  efficiently since no witness has to be computed. *)
  Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
  Proof.
    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
    rewrite /AsVal /= to_of_val; eauto.
  Qed.
173
End language.