dcexpr.v 17.2 KB
Newer Older
1
2
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
3
From iris_c.c_translation Require Export translation proofmode.
4

5
Definition known_locs := list cloc.
6

Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
Inductive dloc :=
  | dLoc : nat  dloc
9
  | dLocUnknown : cloc  dloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
13

Global Instance dloc_decision : EqDecision dloc.
Proof. solve_decision. Defined.

14
15
(* This data type is kind of redundant, as long as we don't have symbolic
Booleans and integers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
24
25
26
Inductive dbase_lit : Type :=
  | dLitInt : Z  dbase_lit
  | dLitBool : bool  dbase_lit
  | dLitUnit : dbase_lit
  | dLitUnknown : base_lit  dbase_lit.

Global Instance dlit_decision : EqDecision dbase_lit.
Proof. solve_decision. Defined.

Inductive dval : Type :=
  | dLitV : dbase_lit  dval
27
  | dPairV : dval  dval  dval
28
  | dLocV : dloc  dval
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  | dValUnknown : val  dval.

Global Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.

Inductive doption (A : Type) : Type :=
  | dNone : doption A
  | dSome : A  doption A
  | dUnknown : option A  doption A.

Arguments dNone {_}.
Arguments dSome {_} _.
Arguments dUnknown {_} _.

Global Instance doption_fmap : FMap doption := λ A B f m,
  match m with
  | dNone => dNone
  | dSome x => dSome (f x)
  | dUnknown o => dUnknown (f <$> o)
  end.

50
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  match dl with
52
  | dLoc i => default inhabitant (E !! i)
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
  | dLocUnknown l => l
  end.

56
Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
62
63
  match l with
  | dLitInt x => LitInt x
  | dLitBool b => LitBool b
  | dLitUnit => LitUnit
  | dLitUnknown l => l
  end.

64
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
  match v with
  | dLitV l => LitV (dbase_lit_interp E l)
67
  | dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
68
  | dLocV dl => cloc_to_val (dloc_interp E dl)
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
72
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
  | dValUnknown v => v
  end.

Fixpoint doption_interp {A} (mx : doption A) : option A :=
  match mx with
  | dNone => None
  | dSome x => Some x
  | dUnknown mx => mx
  end.

Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
  match op with
  | PlusOp => dLitInt (n1 + n2)
  | MinusOp => dLitInt (n1 - n2)
  | MultOp => dLitInt (n1 * n2)
  | QuotOp => dLitInt (n1 `quot` n2)
  | RemOp => dLitInt (n1 `rem` n2)
  | AndOp => dLitInt (Z.land n1 n2)
  | OrOp => dLitInt (Z.lor n1 n2)
  | XorOp => dLitInt (Z.lxor n1 n2)
  | ShiftLOp => dLitInt (n1  n2)
  | ShiftROp => dLitInt (n1  n2)
  | LeOp => dLitBool (bool_decide (n1  n2))
  | LtOp => dLitBool (bool_decide (n1 < n2))
  | EqOp => dLitBool (bool_decide (n1 = n2))
  end.

Lemma dbin_op_eval_int_correct E op n1 n2 :
  bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
Proof. by destruct op. Qed.

Definition dbin_op_eval_bool
    (op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
  | AndOp => dSome (dLitBool (b1 && b2))
  | OrOp => dSome (dLitBool (b1 || b2))
  | XorOp => dSome (dLitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => dNone (* Shifts *)
  | LeOp | LtOp => dNone (* InEquality *)
  | EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
  end.

Lemma dbin_op_eval_bool_correct E op b1 b2 w :
  dbin_op_eval_bool op b1 b2 = dSome w 
  bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
Proof. destruct op; simpl; try by inversion 1. Qed.

Definition dbin_op_eval
118
           (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  match dv1,dv2 with
120
  | dPairV _ _, _ | _, dPairV _ _ => dNone
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
  | dValUnknown _, _ | _,dValUnknown _ =>
     dUnknown
      (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
  | dLitV l1, dLitV l2 =>
    if decide (op = EqOp)
    then dSome $ dLitV $ dLitBool
               $ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
    else match l1, l2 with
         | (dLitInt n1), (dLitInt n2) =>
           dSome $ dLitV $ dbin_op_eval_int op n1 n2
         | (dLitBool b1), (dLitBool b2) =>
           dLitV <$> dbin_op_eval_bool op b1 b2
         | dLitUnknown _, _ | _, dLitUnknown _ =>
             dUnknown (dValUnknown <$>
                bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
         | _, _ => dNone
         end
138
  | _, _ => dNone
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
  end.

141
142
143
144
145
146
147
148

Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : doption dval :=
  match op with
  | CBinOp op' => dbin_op_eval E op' dv1 dv2
  | PtrPlusOp | PtrLtOp =>
    dUnknown (dValUnknown <$> cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
152
153
Lemma dbin_op_eval_correct E op dv1 dv2 w :
  doption_interp (dbin_op_eval E op dv1 dv2) = Some w 
  bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
  Some (dval_interp E w).
Proof.
Dan Frumin's avatar
Dan Frumin committed
154
155
  destruct dv1 as [dl1 | |v1|]=> //.
  - destruct dv2 as [dl2 | |v2|]=> //.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
161
    + unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
      { inversion 1. rewrite /bin_op_eval /=.  f_equal. simplify_eq /=.
         do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
      { rewrite /bin_op_eval; intros; destruct dl1, dl2;
          rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
            try (destruct op; done); simpl.
162
163
        - rewrite /bin_op_eval in H0; case_decide; first done.
          destruct b; simplify_eq /=; f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
        - destruct op; simplify_eq /=; try done.
165
166
167
168
        - case_decide; first done. destruct b0; simplify_eq /=; f_equal.
          destruct op; simplify_eq /=; try done.
        - case_decide; first done. destruct b; simplify_eq /=; f_equal.
        - case_decide; first done; destruct b; simplify_eq /=; f_equal;
Robbert Krebbers's avatar
Robbert Krebbers committed
169
            destruct op; simplify_eq /=; try done.
170
171
172
173
        - case_decide; first done; destruct b; simplify_eq /=; f_equal.
        - case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
            destruct op; simplify_eq /=; try done. }
    + simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) _);
174
        try by inversion 1.
175
176
177
  - simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
      try by inversion 1.
  - simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
      try by inversion 1.
Qed.

181
182
183
184
185
186
187
188
189
190
191
Lemma dcbin_op_eval_correct E op dv1 dv2 w :
  doption_interp (dcbin_op_eval E op dv1 dv2) = Some w 
  cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
  Some (dval_interp E w).
Proof.
  destruct op as [op'| |].
  - apply dbin_op_eval_correct.
  - cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
  - cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrLtOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
Qed.

192
193
Definition dun_op_eval
     (E : known_locs) (op : un_op) (dv : dval) : doption dval :=
194
  match dv with
195
  | dPairV _ _ => dNone
196
197
198
199
200
201
  | dValUnknown _ => dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
  | dLitV dl =>
    match op, dl with
    | NegOp, dLitBool b => dSome $ dLitV $ dLitBool (negb b)
    | NegOp, dLitInt n => dSome $ dLitV $ dLitInt (Z.lnot n)
    | MinusUnOp, dLitInt n => dSome $ dLitV $ dLitInt (- n)
202
203
    | _, dLitUnknown l =>
      dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
204
205
    | _,_ => dNone
    end
206
  | dLocV _ => dNone
207
208
209
210
211
212
  end.

Lemma dun_op_eval_correct E op dv w :
  doption_interp (dun_op_eval E op dv) = Some w 
  un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
Dan Frumin's avatar
Dan Frumin committed
213
  destruct dv as [dl | |v|]=> //=; last first.
214
215
216
217
218
219
220
221
  - destruct (un_op_eval op v); simpl; by inversion 1.
  - destruct op.
    + destruct dl; simpl; try by inversion 1.
      destruct b; by inversion 1.
    + destruct dl; simpl; try by inversion 1.
      destruct b; by inversion 1.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
(** DCexpr *)
Inductive dcexpr : Type :=
224
225
226
227
  | dCRet  : dval  dcexpr
  | dCAlloc : dcexpr  dcexpr
  | dCLoad : dcexpr  dcexpr
  | dCStore : dcexpr  dcexpr  dcexpr
228
229
  | dCBinOp : cbin_op  dcexpr  dcexpr  dcexpr
  | dCPreBinOp : cbin_op  dcexpr  dcexpr  dcexpr
230
  | dCUnOp : un_op  dcexpr  dcexpr
231
  | dCSeq : dcexpr  dcexpr  dcexpr
232
  | dCPar : dcexpr  dcexpr  dcexpr
233
  | dCInvoke  (f: val) (de: dcexpr)
234
  | dCUnknown (e : expr) `{!Closed [] e}.
Robbert Krebbers's avatar
Robbert Krebbers committed
235

236
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
240
241
242
  match de with
  | dCRet dv => a_ret (dval_interp E dv)
  | dCAlloc de1 => a_alloc (dcexpr_interp E de1)
  | dCLoad de1 => a_load (dcexpr_interp E de1)
  | dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
  | dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
243
244
  | dCPreBinOp op de1 de2 =>
    a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
245
  | dCUnOp op de => a_un_op op (dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  | dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
247
  | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
248
  | dCInvoke fv de => call (fv, dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250
251
  | dCUnknown e1 => e1
  end.

252
253
(** Well-foundness of dcexpr w.r.t. known_locs *)

254
Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
255
  match dv with
256
  | dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
257
  | dLocV (dLoc i) => bool_decide (is_Some (E !! i))
258
259
260
261
262
263
  | _  => true
  end.

Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
  match de with
  | dCRet dv => dval_wf E dv
264
265
266
  | dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
  | dCStore de1 de2 | dCBinOp _ de1 de2
  | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
267
268
269
270
271
272
273
274
      dcexpr_wf E de1 && dcexpr_wf E de2
  | dCUnknown _ => true
  end.

(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
  dval_wf E dv  E `prefix_of` E'  dval_wf E' dv.
Proof.
275
  induction dv as [d| | |]; try naive_solver.
276
277
278
  destruct d as [i|]; last done; simplify_eq /=.
  intros Hb Hpre. case_bool_decide; last done.
  clear Hb. generalize dependent E. revert E'. induction i as [| i].
279
280
281
282
283
284
  + intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
    destruct E'. by apply prefix_nil_not in Hpre. naive_solver.
  + intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H.
    * by apply prefix_nil_not in Hpre.
    * by apply is_Some_None in H.
    * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
285
286
287
288
289
Qed.

Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
  dcexpr_wf E de  E `prefix_of` E'  dcexpr_wf E' de.
Proof.
Dan Frumin's avatar
Dan Frumin committed
290
  induction de; simplify_eq /=; try eauto; [ apply dval_wf_mono | | | | |];
291
  naive_solver.
292
293
Qed.

294
295
296

Lemma dun_op_eval_dSome_wf E dv u dw:
  dval_wf E dv  dun_op_eval E u dv = dSome dw  dval_wf E dw.
297
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
298
299
300

Lemma dun_op_eval_dUnknown_wf E dv u w:
  dval_wf E dv  dun_op_eval E u dv =  dUnknown (Some w)  dval_wf E w.
301
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
302
303
304
305

Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
  dval_wf E dv1  dval_wf E dv2 
  dbin_op_eval E op dv1 dv2 = dSome dw  dval_wf E dw.
306
Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
307

308
309
310
311
312
Lemma dcbin_op_eval_dSome_wf E dv1 dv2 op dw:
  dval_wf E dv1  dval_wf E dv2 
  dcbin_op_eval E op dv1 dv2 = dSome dw  dval_wf E dw.
Proof. destruct op; first eauto using dbin_op_eval_dSome_wf; naive_solver. Qed.

313
314
(** / Well-foundness of dcexpr w.r.t. known_locs *)

315
316
317
Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
  dval_wf E dv  E `prefix_of` E'  dval_interp E dv = dval_interp E' dv.
Proof.
Dan Frumin's avatar
Dan Frumin committed
318
319
  induction dv as [d|?|?|?]=>//.
  { simpl. intros. f_equal; naive_solver. }
320
321
322
  destruct d as [i|]; last done; simplify_eq /=.
  intros Hb Hpre. case_bool_decide; last done.
  clear Hb. generalize dependent E. revert E'. induction i as [| i].
323
  + intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
324
    destruct E'. by apply prefix_nil_not in Hpre.
325
326
327
328
329
    by apply prefix_cons_inv_1 in Hpre; subst.
  + intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H.
    * by apply prefix_nil_not in Hpre.
    * by apply is_Some_None in H.
    * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
330
331
332
333
334
335
336
337
338
339
340
341
342
Qed.

Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
   dcexpr_wf E de  E `prefix_of` E'  dcexpr_interp E de = dcexpr_interp E' de.
Proof.
  induction de; simplify_eq /=; intros H Hpre;
    try (by rewrite IHde ) ||
        (apply andb_prop_elim in H as [H1 H2];
         rewrite IHde2; [rewrite IHde1; done | done | done ];
           by rewrite (IHde1 H1 Hpre  (dcexpr_interp E de1))) || eauto.
  do 2 f_equal. by apply dval_interp_mono.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
345
Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
Proof. induction de; simpl; solve_closed. Qed.

346
347
(** * Reification of C syntax *)
(** ** LocLookup *)
348
Class LocLookup (E : known_locs) (l : cloc) (i : nat) :=
349
350
351
352
353
354
355
356
357
  loc_lookup : E !! i = Some l.

Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
Proof. done. Qed.

Global Instance loc_lookup_there l l' E i :
  LocLookup E l i  LocLookup (l' :: E) l (S i).
Proof. done. Qed.

358
359
360
(** ** IntoDBaseLit *)
Class IntoDBaseLit (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
  into_dbase_lit : l = dbase_lit_interp E dl.
361

362
363
Global Instance into_dbase_lit_int E i :
  IntoDBaseLit E (LitInt i) (dLitInt i).
364
365
Proof. split; eauto. Qed.

366
367
Global Instance into_dbase_lit_default E l :
  IntoDBaseLit E l (dLitUnknown l) | 1000.
368
369
370
371
372
373
374
Proof. split; eauto. Qed.

(** ** ExprIntoDVal *)
Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
  { expr_into_dval : e = of_val (dval_interp E dv);
    expr_into_dval_wf : dval_wf E dv }.

375
376
377
378
379
380
381
382
383
384
385
Global Instance expr_into_dval_lit E l dl :
  IntoDBaseLit E l dl  ExprIntoDVal E (Lit l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

Global Instance expr_into_dval_loc E l i :
  LocLookup E l i  ExprIntoDVal E (cloc_to_val l) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.

Global Instance expr_into_dval_loc_unknown E l :
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
386

387
(* TODO: use ValToNat for those two instance below *)
388
389
390
391
392
393
394
Global Instance expr_into_dval_cloc_pos E (l : loc) (o : positive) i :
  LocLookup E (l,Pos.to_nat o) i  ExprIntoDVal E (#l,#(Zpos o)) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi -?positive_nat_Z //. Qed.

Global Instance expr_into_dval_cloc_zero E (l : loc) i :
  LocLookup E (l,0%nat) i  ExprIntoDVal E (#l,#0) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.
395
396
397
398
399
400
401
402
403
404

Global Instance expr_into_dval_default E e v :
  IntoVal e v  ExprIntoDVal E e (dValUnknown v) | 1000.
Proof. done. Qed.

(** ** IntoDVal *)
Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
  { into_dval : v = dval_interp E dv;
    into_dval_wf : dval_wf E dv }.

405
406
407
408
409
410
411
412
413
414
415
Global Instance into_dval_lit E l dl :
  IntoDBaseLit E l dl  IntoDVal E (LitV l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

Global Instance into_dval_loc E l i :
  LocLookup E l i  IntoDVal E (cloc_to_val l) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.

Global Instance into_dval_loc_unknown E l :
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
416
417
418
419
420

Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed.

(** ** IntoDCexpr *)
421
Class IntoDCexpr (E: known_locs) (e: expr) (de: dcexpr) :=
422
423
  { into_dcexpr : e = dcexpr_interp E de;
    into_dcexpr_wf : dcexpr_wf E de }.
Robbert Krebbers's avatar
Robbert Krebbers committed
424
425

Global Instance into_dcexpr_ret E v dv:
Robbert Krebbers's avatar
Robbert Krebbers committed
426
  ExprIntoDVal E v dv 
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  IntoDCexpr E (a_ret v) (dCRet dv).
428
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
429
430
431
432

Global Instance into_dcexpr_alloc E e de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_alloc e) (dCAlloc de).
433
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
435
436
437

Global Instance into_dcexpr_load E e de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_load e) (dCLoad de).
438
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
441
442
443

Global Instance into_dcexpr_store E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
444
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
446
447
448
449

Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
450
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
451

Dan Frumin's avatar
Dan Frumin committed
452
453
454
455
456
457
Global Instance into_dcexpr_prebinop E e1 e2 op de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_pre_bin_op op e1 e2) (dCPreBinOp op de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.

458
459
460
Global Instance into_dcexpr_unop E e op de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_un_op op e) (dCUnOp op de).
461
Proof. intros [-> ?]; split; auto. Qed.
462

Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
Robbert Krebbers's avatar
Robbert Krebbers committed
466
  IntoDCexpr E (e1 ; e2) (dCSeq de1 de2).
467
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
468

469
470
471
472
473
474
Global Instance into_dcexpr_par E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (e1 ||| e2) (dCPar de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.

475
476
Global Instance into_dcexpr_invoke E `{Closed [] e1} ef f `{!IntoVal ef f} de1 :
  IntoDCexpr E e1 de1 
477
  IntoDCexpr E (call (ef, e1)) (dCInvoke f de1).
478
479
480
481
482
Proof.
  intros. unfold IntoVal in *. simplify_eq /=.
  split; simpl; auto; f_equal; by inversion H0.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
Global Instance into_dcexpr_unknown E e `{Closed [] e}:
  IntoDCexpr E e (dCUnknown e) | 100.
485
Proof. done. Qed.