language.v 13.5 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
Section language_mixin.
5
  Context {expr val state observation : Type}.
6
7
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
Ralf Jung's avatar
Ralf Jung committed
8
9
10
  (** We annotate the reduction relation with observations [κ], which we will
     use in the definition of weakest preconditions to predict future
     observations and assert correctness of the predictions. *)
11
  Context (prim_step : expr  state  list observation  expr  state  list expr  Prop).
12
13
14
15

  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;
16
    mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None
17
18
19
  }.
End language_mixin.

20
21
22
23
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
24
  observation : Type;
25
26
  of_val : val  expr;
  to_val : expr  option val;
27
  prim_step : expr  state  list observation  expr  state  list expr  Prop;
28
  language_mixin : LanguageMixin of_val to_val prim_step
Ralf Jung's avatar
Ralf Jung committed
29
}.
Ralf Jung's avatar
Ralf Jung committed
30
31

Declare Scope expr_scope.
Janno's avatar
Janno committed
32
33
Delimit Scope expr_scope with E.
Bind Scope expr_scope with expr.
Ralf Jung's avatar
Ralf Jung committed
34
35
36

Declare Scope val_scope.
Delimit Scope val_scope with V.
37
Bind Scope val_scope with val.
38

39
Arguments Language {_ _ _ _ _ _ _} _.
40
41
Arguments of_val {_} _.
Arguments to_val {_} _.
42
Arguments prim_step {_} _ _ _ _ _ _.
43

44
45
46
Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
Canonical Structure exprO Λ := leibnizO (expr Λ).
47
48

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

50
Class LanguageCtx {Λ : language} (K : expr Λ  expr Λ) := {
51
52
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
53
54
55
56
57
58
  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
59
60
}.

61
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
Proof. constructor; naive_solver. Qed.

Ralf Jung's avatar
Ralf Jung committed
64
Inductive atomicity := StronglyAtomic | WeaklyAtomic.
65

66
Section language.
67
68
  Context {Λ : language}.
  Implicit Types v : val Λ.
69
70
71
72
73
74
  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.
75
  Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs  to_val e = None.
76
  Proof. apply language_mixin. Qed.
Ralf Jung's avatar
Ralf Jung committed
77

78
  Definition reducible (e : expr Λ) (σ : state Λ) :=
79
     κ e' σ' efs, prim_step e σ κ e' σ' efs.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
80
81
  (* Total WP only permits reductions without observations *)
  Definition reducible_no_obs (e : expr Λ) (σ : state Λ) :=
82
     e' σ' efs, prim_step e σ [] e' σ' efs.
83
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
84
     κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
85
86
  Definition stuck (e : expr Λ) (σ : state Λ) :=
    to_val e = None  irreducible e σ.
Amin Timany's avatar
Amin Timany committed
87
88
  Definition not_stuck (e : expr Λ) (σ : state Λ) :=
    is_Some (to_val e)  reducible e σ.
89

Ralf Jung's avatar
Ralf Jung committed
90
  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
Ralf Jung's avatar
Ralf Jung committed
91
92
93
94
     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
95
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
96

Ralf Jung's avatar
Ralf Jung committed
97
     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
Ralf Jung's avatar
Ralf Jung committed
98
99
100
101
     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 :=
102
103
    atomic σ e' κ σ' efs :
      prim_step e σ κ e' σ' efs 
Ralf Jung's avatar
Ralf Jung committed
104
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
105

106
  Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
107
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
108
       ρ1 = (t1 ++ e1 :: t2, σ1) 
109
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
110
111
       prim_step e1 σ1 κ e2 σ2 efs 
       step ρ1 κ ρ2.
Tej Chajed's avatar
Tej Chajed committed
112
  Hint Constructors step : core.
113

114
  Inductive nsteps : nat  cfg Λ  list (observation Λ)  cfg Λ  Prop :=
Ralf Jung's avatar
Ralf Jung committed
115
116
117
118
119
    | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
    | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 
       nsteps n ρ2 κs ρ3 
120
       nsteps (S n) ρ1 (κ ++ κs) ρ3.
Tej Chajed's avatar
Tej Chajed committed
121
  Hint Constructors nsteps : core.
122

Ralf Jung's avatar
Ralf Jung committed
123
  Definition erased_step (ρ1 ρ2 : cfg Λ) :=  κ, step ρ1 κ ρ2.
124

125
126
  (** [rtc erased_step] and [nsteps] encode the same thing, just packaged
      in a different way. *)
127
  Lemma erased_steps_nsteps ρ1 ρ2 :
128
    rtc erased_step ρ1 ρ2   n κs, nsteps n ρ1 κs ρ2.
129
  Proof.
130
    split.
131
132
133
    - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
    - intros (n & κs & Hsteps). unfold erased_step.
      induction Hsteps; eauto using rtc_refl, rtc_l.
134
  Qed.
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
138
139
140

  Lemma not_reducible e σ : ¬reducible e σ  irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
141
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
142
  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
143
144
  Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ  reducible e σ.
  Proof. intros (?&?&?&?); eexists; eauto. Qed.
145
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
146
  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
147
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
148
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Amin Timany's avatar
Amin Timany committed
149
150
151
152
153
  Lemma not_not_stuck e σ : ¬not_stuck e σ  stuck e σ.
  Proof.
    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
    destruct (decide (to_val e = None)); naive_solver.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
154

155
156
157
  Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e  Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
158

159
  Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
160
161
162
    reducible e σ  reducible (K e) σ.
  Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.
  Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
163
164
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
165
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
166
167
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
168
  Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
169
170
171
    reducible_no_obs e σ  reducible_no_obs (K e) σ.
  Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.
  Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ :
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
172
173
174
175
176
    to_val e = None  reducible_no_obs (K e) σ  reducible_no_obs e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
177
  Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
178
    to_val e = None  irreducible e σ  irreducible (K e) σ.
179
180
181
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.
  Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ :
    irreducible (K e) σ  irreducible e σ.
182
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
183

184
  Lemma not_stuck_fill_inv K `{!@LanguageCtx Λ K} e σ :
185
186
187
188
    not_stuck (K e) σ  not_stuck e σ.
  Proof.
    rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
    - auto using fill_not_val.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    - destruct (decide (to_val e = None)); eauto using reducible_fill_inv.
190
191
  Qed.

Hai Dang's avatar
Hai Dang committed
192
193
  Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
    stuck e σ  stuck (K e) σ.
194
  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed.
Hai Dang's avatar
Hai Dang committed
195

196
197
  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).
198
199
200
201
202
203
204
  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
205

Amin Timany's avatar
Amin Timany committed
206
207
208
209
210
211
212
213
214
215
216
217
  Lemma step_insert i t2 σ2 e κ e' σ3 efs :
    t2 !! i = Some e 
    prim_step e σ2 κ e' σ3 efs 
    step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
  Proof.
    intros.
    edestruct (elem_of_list_split_length t2) as (t21&t22&?&?);
      first (by eauto using elem_of_list_lookup_2); simplify_eq.
    econstructor; eauto.
    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
  Qed.

218
219
220
  Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1  t1'  erased_step (t1,σ1) (t2,σ2)   t2', t2  t2'  erased_step (t1',σ1) (t2',σ2).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
221
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
Ralf Jung's avatar
Ralf Jung committed
222
     (* FIXME: [naive_solver] should be able to handle this *)
223
224
  Qed.

225
  Record pure_step (e1 e2 : expr Λ) := {
226
227
    pure_step_safe σ1 : reducible_no_obs e1 σ1;
    pure_step_det σ1 κ e2' σ2 efs :
228
      prim_step e1 σ1 κ e2' σ2 efs  κ = []  σ2 = σ1  e2' = e2  efs = []
Dan Frumin's avatar
Dan Frumin committed
229
230
  }.

Amin Timany's avatar
Amin Timany committed
231
232
  Notation pure_steps_tp := (Forall2 (rtc pure_step)).

233
234
235
  (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
  succeeding when it did not actually do anything. *)
  Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
236
    pure_exec : φ  relations.nsteps pure_step n e1 e2.
237

238
  Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
239
240
    pure_step e1 e2 
    pure_step (K e1) (K e2).
241
242
  Proof.
    intros [Hred Hstep]. split.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
243
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
244
    - intros σ1 κ e2' σ2 efs Hpstep.
245
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
246
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
247
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
248
249
  Qed.

250
  Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
251
252
    relations.nsteps pure_step n e1 e2 
    relations.nsteps pure_step n (K e1) (K e2).
Amin Timany's avatar
Amin Timany committed
253
254
255
256
257
258
  Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.

  Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    rtc pure_step e1 e2  rtc pure_step (K e1) (K e2).
  Proof. eauto using rtc_congruence, pure_step_ctx. Qed.

259
  (* We do not make this an instance because it is awfully general. *)
260
  Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
261
262
263
264
    PureExec φ n e1 e2 
    PureExec φ n (K e1) (K e2).
  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.

265
266
  (* This is a family of frequent assumptions for PureExec *)
  Class IntoVal (e : expr Λ) (v : val Λ) :=
267
    into_val : of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
268

269
  Class AsVal (e : expr Λ) := as_val :  v, of_val v = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
271
272
273
274
  (* 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.
275
    rewrite /AsVal /=; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
  Qed.
Amin Timany's avatar
Amin Timany committed
277

Ralf Jung's avatar
Ralf Jung committed
278
279
280
  Lemma as_val_is_Some e :
    ( v, of_val v = e)  is_Some (to_val e).
  Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
Amin Timany's avatar
Amin Timany committed
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328

  Lemma prim_step_not_stuck e σ κ e' σ' efs :
    prim_step e σ κ e' σ' efs  not_stuck e σ.
  Proof. rewrite /not_stuck /reducible. eauto 10. Qed.

  Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e :
    rtc pure_step (of_val v) e  to_val e = Some v.
  Proof.
    intros ?; rewrite <- to_of_val.
    f_equal; symmetry; eapply rtc_nf; first done.
    intros [e' [Hstep _]].
    destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
    by rewrite to_of_val in Hval.
  Qed.

  (** Let thread pools [t1] and [t3] be such that each thread in [t1] makes
   (zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
   let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
   step to thread pool [t2] and state [σ2]. In this situation, either the step
   from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
   or, there is an [i] such that [i]th thread does not participate in the
   pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
   the [i]th thread starting from [t1]. *)
  Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 :
    erased_step (t1, σ1) (t2, σ2) 
    pure_steps_tp t1 t3 
    (σ1 = σ2  pure_steps_tp t2 t3) 
    ( i e efs e' κ,
      t1 !! i = Some e  t3 !! i = Some e 
      t2 = <[i:=e']>t1 ++ efs 
      prim_step e σ1 κ e' σ2 efs).
  Proof.
    intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
    apply Forall2_app_inv_l in Hps
      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
    - right.
      exists (length t11), e, efs, e', κ; split_and!; last done.
      + by rewrite lookup_app_r // Nat.sub_diag.
      + apply Forall2_length in Hpsteps.
        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
    - edestruct Hprs as (?&?&?&?); first done; simplify_eq.
      left; split; first done.
      rewrite right_id_L.
      eauto using Forall2_app.
  Qed.

329
End language.
Amin Timany's avatar
Amin Timany committed
330
331

Notation pure_steps_tp := (Forall2 (rtc pure_step)).