dcexpr.v 27 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

7
(* RK: We should also record an offset for unknown locations, ideally. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
8
Inductive dloc :=
9
  | dLoc : nat  nat  dloc (* index * offset *)
10
  | dLocUnknown : cloc  dloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

Robbert Krebbers's avatar
Robbert Krebbers committed
12
Global Instance dloc_eq_dec : EqDecision dloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
Proof. solve_decision. Defined.

Dan Frumin's avatar
Dan Frumin committed
15 16 17 18 19 20 21 22 23
(* Symbolic integers *)
(* TODO: these should account for known non-natural integers as well *)
Inductive dint : Type :=
| dNat : nat  dint
| dIntUnknown : Z  dint.

Global Instance dint_decision : EqDecision dint.
Proof. solve_decision. Defined.

24 25
(* 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
26
Inductive dbase_lit : Type :=
Dan Frumin's avatar
Dan Frumin committed
27
  | dLitInt : dint  dbase_lit
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30 31
  | dLitBool : bool  dbase_lit
  | dLitUnit : dbase_lit
  | dLitUnknown : base_lit  dbase_lit.

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Global Instance dbase_lit_eq_dec : EqDecision dbase_lit.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36
Proof. solve_decision. Defined.

Inductive dval : Type :=
  | dLitV : dbase_lit  dval
37
  | dPairV : dval  dval  dval
38
  | dLocV : dloc  dval
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
  | dValUnknown : val  dval.

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Global Instance dval_eq_dec : EqDecision dval.
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
Proof. solve_decision. Defined.

44
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  match dl with
46
  | dLoc i j => cloc_plus (default inhabitant (E !! i)) j
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49
  | dLocUnknown l => l
  end.

Dan Frumin's avatar
Dan Frumin committed
50 51 52 53 54 55 56
Definition dint_interp (di : dint) : Z :=
  match di with
  | dNat n => Z.of_nat n
  (* | dInt z => z *)
  | dIntUnknown z => z
  end.

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

65
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  match v with
67
  | dLitV l => LitV (dbase_lit_interp l)
68
  | dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
69
  | dLocV dl => cloc_to_val (dloc_interp E dl)
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72
  | dValUnknown v => v
  end.

Dan Frumin's avatar
Dan Frumin committed
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
Definition dval_to_nat (dv : dval) : option nat :=
  match dv with
  | dLitV (dLitInt (dNat n)) => Some n
  | _ => None
  end.

Lemma dval_to_nat_correct E dv n :
  dval_to_nat dv = Some n 
  dval_interp E dv = #n.
Proof.
  intros Hv.
  destruct dv; try inversion Hv.
  case_match; simplify_eq/=.
  case_match; simplify_eq/=.
  done.
Qed.

(* TODO: beter heuristics here for operations like sub and div *) 
Definition dbin_op_eval_nat (op : bin_op) (n1 n2 : nat) : dbase_lit :=
  match op with
  | PlusOp => dLitInt $ dNat $ (n1 + n2)%nat
  | MinusOp => dLitInt $ dIntUnknown $ Z.of_nat n1 - Z.of_nat n2
  | MultOp => dLitInt $ dNat $ (n1 * n2)%nat
  | QuotOp => dLitInt $ dIntUnknown $ Z.of_nat n1 `quot` Z.of_nat n2
  | RemOp => dLitInt $ dIntUnknown $ Z.of_nat n1 `rem` Z.of_nat n2
  | AndOp => dLitInt $ dNat $ Nat.land n1 n2
  | OrOp => dLitInt $ dNat $ Nat.lor n1 n2
  | XorOp => dLitInt $ dNat $ Nat.lxor n1 n2
  | ShiftLOp => dLitInt $ dIntUnknown $ Z.of_nat n1  Z.of_nat n2
  | ShiftROp => dLitInt $ dIntUnknown $ Z.of_nat n1  Z.of_nat n2
  | LeOp => dLitBool (bool_decide (n1  n2))
  | LtOp => dLitBool (bool_decide (n1 < n2))
  | EqOp => dLitBool (bool_decide (n1 = n2))
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
108 109
Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
  match op with
Dan Frumin's avatar
Dan Frumin committed
110 111 112 113 114 115 116 117 118 119
  | PlusOp => dLitInt $ dIntUnknown $ n1 + n2
  | MinusOp => dLitInt $ dIntUnknown $ n1 - n2
  | MultOp => dLitInt $ dIntUnknown $ n1 * n2
  | QuotOp => dLitInt $ dIntUnknown $ n1 `quot` n2
  | RemOp => dLitInt $ dIntUnknown $ n1 `rem` n2
  | AndOp => dLitInt $ dIntUnknown $ Z.land n1 n2
  | OrOp => dLitInt $ dIntUnknown $ Z.lor n1 n2
  | XorOp => dLitInt $ dIntUnknown $ Z.lxor n1 n2
  | ShiftLOp => dLitInt $ dIntUnknown $ n1  n2
  | ShiftROp => dLitInt $ dIntUnknown $ n1  n2
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124
  | LeOp => dLitBool (bool_decide (n1  n2))
  | LtOp => dLitBool (bool_decide (n1 < n2))
  | EqOp => dLitBool (bool_decide (n1 = n2))
  end.

125 126
Lemma dbin_op_eval_int_correct op n1 n2 :
  bin_op_eval_int op n1 n2 = dbase_lit_interp (dbin_op_eval_int op n1 n2).
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129
Proof. by destruct op. Qed.

Definition dbin_op_eval_bool
130
    (op : bin_op) (b1 b2 : bool) : option dbase_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  match op with
132 133 134 135 136 137 138
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
  | AndOp => Some (dLitBool (b1 && b2))
  | OrOp => Some (dLitBool (b1 || b2))
  | XorOp => Some (dLitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => None (* Shifts *)
  | LeOp | LtOp => None (* InEquality *)
  | EqOp => Some (dLitBool (bool_decide (b1 = b2)))
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
  end.

141
Lemma dbin_op_eval_bool_correct op b1 b2 w :
142
  dbin_op_eval_bool op b1 b2 = Some w 
143
  bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp w).
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
Proof. destruct op; simpl; try by inversion 1. Qed.

146
(* DF: why are we not allowing the `dLocV _, dLocV _` case? *)
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Definition dbin_op_eval
148
           (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151
  match dv1,dv2 with
  | dLitV l1, dLitV l2 =>
    if decide (op = EqOp)
152
    then Some $ dLitV $ dLitBool
153
              $ bool_decide (dbase_lit_interp l1 = dbase_lit_interp l2)
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    else match l1, l2 with
Dan Frumin's avatar
Dan Frumin committed
155 156 157 158
         | dLitInt (dNat n1), dLitInt (dNat n2) =>
           Some $ dLitV $ dbin_op_eval_nat op n1 n2
         | dLitInt z1, dLitInt z2 =>
           Some $ dLitV $ dbin_op_eval_int op (dint_interp z1) (dint_interp z2)
159 160
         | dLitBool b1, dLitBool b2 => dLitV <$> dbin_op_eval_bool op b1 b2
         | _, _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
161
         end
162
  | _, _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164
  end.

165
Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : option dval :=
166
  match dv1,dv2 with
Dan Frumin's avatar
Dan Frumin committed
167 168 169
  | dLocV (dLoc i j), dLitV (dLitInt (dNat o)) =>
    (* TODO: here we need to additionaly check wether the argument 
       is a natural number *)
170
    match offset_of_val (LitV (LitInt o)) with
171
    | None => None
172
    | Some k => Some $ dLocV $ dLoc i (j + k)
173
    end
174
  | _,_ => None
175 176 177
  end.

Lemma dptr_plus_eval_correct E dv1 dv2 w :
178 179
  dptr_plus_eval E dv1 dv2 = Some w 
  cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E w).
180
Proof.
181
  destruct dv1 as [?|??|[??|]|u1],dv2 as [[]|??|?|u2]; try naive_solver.
Dan Frumin's avatar
Dan Frumin committed
182 183 184 185 186 187
  rewrite /cbin_op_eval /=.
  destruct d; last by inversion 1.
  case_option_guard; inversion 1. 
  rewrite cloc_of_to_val /=. 
  case_option_guard; last contradiction. simpl.
  rewrite cloc_plus_plus //.
188
Qed.
189

190
Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : option dval :=
191 192
  match op with
  | CBinOp op' => dbin_op_eval E op' dv1 dv2
193
  | PtrPlusOp => dptr_plus_eval E dv1 dv2
194
  | PtrLtOp => None
195 196
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
197
Lemma dbin_op_eval_correct E op dv1 dv2 w :
198
  dbin_op_eval E op dv1 dv2 = Some w 
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200 201
  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
202
  destruct dv1 as [dl1 | |v1|]=> //.
203 204 205 206
  destruct dv2 as [dl2 | |v2|]=> //.
  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. }
Dan Frumin's avatar
Dan Frumin committed
207 208 209 210 211 212 213 214 215
  { destruct dl1 as [[d1| ]| | |], dl2 as [[d2| ]| | | ], op;
      simpl; intros; simplify_eq/=; auto.
    by rewrite Nat2Z.inj_add.
    by rewrite Nat2Z.inj_mul.
    admit. (* Z.land vs Nat.land *)
    admit. (* lor *)
    admit. (* xor *)
  }
Admitted.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217
Lemma dcbin_op_eval_correct E op dv1 dv2 w :
218
  dcbin_op_eval E op dv1 dv2 = Some w 
219 220 221
  cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
  Some (dval_interp E w).
Proof.
222
  destruct op as [op'| |]=> //.
223
  - apply dbin_op_eval_correct.
224
  - apply dptr_plus_eval_correct.
225 226
Qed.

227
Definition dun_op_eval
228
     (E : known_locs) (op : un_op) (dv : dval) : option dval :=
229 230 231
  match dv with
  | dLitV dl =>
    match op, dl with
232
    | NegOp, dLitBool b => Some $ dLitV $ dLitBool (negb b)
Dan Frumin's avatar
Dan Frumin committed
233 234
    | NegOp, dLitInt (dIntUnknown n) => Some $ dLitV $ dLitInt $ dIntUnknown (Z.lnot n)
    | MinusUnOp, dLitInt (dIntUnknown n) => Some $ dLitV $ dLitInt $ dIntUnknown (- n)
235
    | _,_ => None
236
    end
237
  | _ => None
238 239 240
  end.

Lemma dun_op_eval_correct E op dv w :
241
  dun_op_eval E op dv = Some w 
242 243
  un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
244
  destruct dv as [dl | |v|]=> //=.
Dan Frumin's avatar
Dan Frumin committed
245
  destruct op, dl as [[?| ]| | |]; intros; simplify_eq/=; auto.
246 247
Qed.

248 249 250
(** Dexpr *)
Inductive dexpr : Type :=
  | dEVal : dval  dexpr
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
251
  | dEVar : string  dexpr
252 253 254
  | dEPair : dexpr  dexpr  dexpr
  | dEFst : dexpr  dexpr
  | dESnd : dexpr  dexpr
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  | dEUnknown (e : W.expr) : dexpr.
256 257 258 259

Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
  match de with
  | dEVal dv => dval_interp E dv
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
260
  | dEVar x => Var x
261 262 263
  | dEPair de1 de2 => (dexpr_interp E de1, dexpr_interp E de2)
  | dEFst de => Fst (dexpr_interp E de)
  | dESnd de => Snd (dexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
264
  | dEUnknown e => W.to_expr e
265 266
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
267 268
(** DCexpr *)
Inductive dcexpr : Type :=
269
  | dCRet : dexpr  dcexpr
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
270
  | dCBind : string  dcexpr  dcexpr  dcexpr
271
  | dCAlloc : dcexpr  dcexpr  dcexpr
272 273
  | dCLoad : dcexpr  dcexpr
  | dCStore : dcexpr  dcexpr  dcexpr
274 275
  | dCBinOp : cbin_op  dcexpr  dcexpr  dcexpr
  | dCPreBinOp : cbin_op  dcexpr  dcexpr  dcexpr
276
  | dCUnOp : un_op  dcexpr  dcexpr
277
  | dCSeq : dcexpr  dcexpr  dcexpr
278
  | dCPar : dcexpr  dcexpr  dcexpr
279
  | dCInvoke  (f: val) (de: dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  | dCUnknown (e : W.expr).
Robbert Krebbers's avatar
Robbert Krebbers committed
281

282
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  match de with
284
  | dCRet de => a_ret (dexpr_interp E de)
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
285
  | dCBind x de1 de2 => x ←ᶜ (dcexpr_interp E de1) ;; (dcexpr_interp E de2)
286
  | dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2)
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289
  | 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)
290 291
  | dCPreBinOp op de1 de2 =>
    a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
292
  | dCUnOp op de => a_un_op op (dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
293
  | dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
294
  | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
295
  | dCInvoke fv de => call (fv, dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  | dCUnknown e1 => W.to_expr e1
Robbert Krebbers's avatar
Robbert Krebbers committed
297 298
  end.

Dan Frumin's avatar
Dan Frumin committed
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 329 330 331 332 333 334 335 336 337 338 339 340
(** ** Substitution *)
Fixpoint de_subst
         (E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
  match de with
  | dEVal _ => de
  | dEVar y  =>  if decide (x = y) then dEVal dv else de
  | dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
  | dEFst de1 => dEFst (de_subst E x dv de1)
  | dESnd de1 => dESnd (de_subst E x dv de1)
  | dEUnknown we =>
    dEUnknown (W.subst x
                       (W.Val (dval_interp E dv)
                              (of_val (dval_interp E dv))
                              (to_of_val _ )) we)
  end.


Fixpoint dce_subst (E: known_locs)
         (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
  match dce with
  | dCRet de1 => dCRet (de_subst E x dv de1)
  | dCBind y de1 de2 =>
    if decide (x = y)
    then dCBind y (dce_subst E x dv de1) de2
    else dCBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCLoad de1 =>  dCLoad (dce_subst E x dv de1)
  | dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCBinOp op de1 de2 =>
    dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCPreBinOp op de1 de2 =>
    dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCUnOp op de1 =>  dCUnOp op (dce_subst E x dv de1)
  | dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
  | dCUnknown we => dCUnknown (W.subst x (W.Val (dval_interp E dv)
                                                (of_val (dval_interp E dv))
                                                (to_of_val _ )) we)
  end.


Robbert Krebbers's avatar
Robbert Krebbers committed
341
(** Well-formedness of dcexpr w.r.t. known_locs *)
Dan Frumin's avatar
Dan Frumin committed
342
Definition dloc_wf (E: known_locs) (dl : dloc) : bool :=
Léon Gondelman's avatar
Léon Gondelman committed
343 344 345 346 347
  match dl with
  | dLoc i _ => bool_decide (is_Some (E !! i))
  | _  => true
  end.

348
Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
349
  match dv with
350
  | dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
351
  | dLocV (dLoc i _) => bool_decide (is_Some (E !! i))
352 353 354
  | _  => true
  end.

Léon Gondelman 's avatar
Léon Gondelman committed
355
Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
356 357
  match de with
  | dEVal dv => dval_wf E dv
Léon Gondelman 's avatar
Léon Gondelman committed
358 359 360
  | dEVar x  => bool_decide (x  X)
  | dEFst de | dESnd de => dexpr_wf X E de
  | dEPair de1 de2 => dexpr_wf X E de1 && dexpr_wf X E de2
Robbert Krebbers's avatar
Robbert Krebbers committed
361
  | dEUnknown e => W.is_closed X e
362 363
  end.

Léon Gondelman 's avatar
Léon Gondelman committed
364
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
365
  match de with
Léon Gondelman 's avatar
Léon Gondelman committed
366
  | dCRet de => dexpr_wf X E de
367
  | dCBind x de1 de2 => dcexpr_wf X E de1 && dcexpr_wf (x :: X) E de2
Léon Gondelman 's avatar
Léon Gondelman committed
368
  | dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf X E de1
369
  | dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
370
  | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
Léon Gondelman 's avatar
Léon Gondelman committed
371
      dcexpr_wf X E de1 && dcexpr_wf X E de2
Robbert Krebbers's avatar
Robbert Krebbers committed
372
  | dCUnknown e => W.is_closed X e
373 374
  end.

Dan Frumin's avatar
Dan Frumin committed
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442
(** Substitution  properties *)
(* We need to be able to simplify subst in the following lemma *)
Arguments subst _ _ !_ /.

Lemma de_subst_subst_comm E x de dv :
  (dexpr_interp E (de_subst E x dv de)) =
  subst x (dval_interp E dv) (dexpr_interp E de).
Proof.
  induction de; simplify_eq /=.
  - by simpl_subst.
  - by destruct (decide (x = s)).
  - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                end; by simpl_subst).
  - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                end; by simpl_subst).
  - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                end; by simpl_subst).
  - by rewrite! W.to_expr_subst.
Qed.

Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
  dcexpr_interp E (dce_subst E x dv de) =
  (subst x (dval_interp E dv) (dcexpr_interp E de))%E.
Proof.
  induction de; simplify_eq /=; simpl_subst;
    try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                end; by simpl_subst).
  - by rewrite de_subst_subst_comm.
  - destruct (decide (x = s)); simplify_eq /=; rewrite IHde1.
    + rewrite decide_False; naive_solver.
    + rewrite IHde2 decide_True; naive_solver.
Qed.

(* Turn the simplification in subst OFF again *)
Arguments subst : simpl never.

Lemma de_subst_dexpr_wf X E s dv1 de2 :
  dval_wf E dv1 
  dexpr_wf (s::X) E de2 
  dexpr_wf X E (de_subst E s dv1 de2).
Proof.
  revert X. induction de2; intros X Hdv1 Hwf2;
  simplify_eq/=; try naive_solver.
  - case_match; eauto. simpl.
    apply bool_decide_pack.
    apply bool_decide_unpack in Hwf2.
    set_solver.
  - apply W.is_closed_correct in Hwf2.
    admit.
Admitted.

Lemma dce_subst_dcexpr_wf X E s dv1 de2 :
  dval_wf E dv1 
  dcexpr_wf (s::X) E de2 
  dcexpr_wf X E (dce_subst E s dv1 de2).
Proof.
  revert X. induction de2; intros X Hdv1 Hwf2; 
              simplify_eq/=; try naive_solver.
  - by apply de_subst_dexpr_wf.
  - destruct_and!. case_match; simpl; split_and; eauto.
    + subst.
      (* use H0 *)
      admit.
    + eapply IHde2_2; eauto.
      admit.
  - apply W.is_closed_correct in Hwf2.
    admit. (* Need W.is_closed_correct in the opposite direction *)
Admitted.
Léon Gondelman 's avatar
Léon Gondelman committed
443

444 445 446 447
(*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.
448
  induction dv as [d| | |]; try naive_solver.
449 450 451
  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].
452 453 454 455 456 457
  + 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.
458 459
Qed.

Léon Gondelman 's avatar
Léon Gondelman committed
460 461 462

Lemma dexpr_wf_mono (X: list string) (E E': known_locs) (de: dexpr) :
  dexpr_wf X E de  E `prefix_of` E'  dexpr_wf X E' de.
463 464
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.

Léon Gondelman 's avatar
Léon Gondelman committed
465 466
Lemma dcexpr_wf_mono (X: list string) (E E': known_locs) (de: dcexpr) :
  dcexpr_wf X E de  E `prefix_of` E'  dcexpr_wf X E' de.
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
467
Proof.
Léon Gondelman 's avatar
Léon Gondelman committed
468
  revert X.
Léon Gondelman 's avatar
wip  
Léon Gondelman committed
469 470 471
  induction de; intros X; simplify_eq /=; [try apply dexpr_wf_mono|..];
  naive_solver.
Qed.
472 473


474 475
Lemma dun_op_eval_Some_wf E dv u dw:
  dval_wf E dv  dun_op_eval E u dv = Some dw  dval_wf E dw.
476
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
477

478
Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
479
  dval_wf E dv1  dval_wf E dv2 
480
  dbin_op_eval E op dv1 dv2 = Some dw  dval_wf E dw.
481
Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
482

483
Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
484
  dval_wf E dv1  dval_wf E dv2 
485
  dcbin_op_eval E op dv1 dv2 = Some dw  dval_wf E dw.
486
Proof.
487
  destruct op; first eauto using dbin_op_eval_Some_wf; try naive_solver.
488 489
  simpl. unfold dptr_plus_eval. repeat case_match; naive_solver.
Qed.
490

Robbert Krebbers's avatar
Robbert Krebbers committed
491
(** / Well-formedness of dcexpr w.r.t. known_locs *)
492

Léon Gondelman's avatar
Léon Gondelman committed
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511
Lemma dloc_interp_mono (E E': known_locs) (i j: nat) :
  dloc_wf E (dLoc i j)  E `prefix_of` E' 
  dloc_interp E (dLoc i j) = dloc_interp E' (dLoc i j).
Proof.
  revert E E'. induction i as [| i].
  - intros E E' Hwf Hpre; destruct E, E'; try (inversion Hpre ; done).
    apply prefix_cons_inv_1 in Hpre. by rewrite Hpre.
  - intros E E' Hwf Hpre; destruct E, E'; try (inversion Hpre ; done).
    specialize (prefix_cons_inv_1 c c0 E E' Hpre) as ->.
    assert ( dloc_interp (c0 :: E) (dLoc (S i) j) =
             dloc_interp (E) (dLoc i j)) by
        naive_solver. rewrite H.
    assert ( dloc_interp (c0 :: E') (dLoc (S i) j) =
             dloc_interp (E') (dLoc i j)) by
        naive_solver. rewrite H0.
    apply prefix_cons_inv_2 in Hpre.
    apply IHi; last done. destruct E; naive_solver.
Qed.

512 513 514
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
515 516
  induction dv as [d|?|?|?]=>//.
  { simpl. intros. f_equal; naive_solver. }
517 518 519
  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].
520
  + intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
521
    destruct E'. by apply prefix_nil_not in Hpre.
522 523 524 525 526
    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.
527 528
Qed.

Léon Gondelman 's avatar
Léon Gondelman committed
529 530 531

Lemma dexpr_interp_mono (X: list string) (E E': known_locs) (de: dexpr) :
   dexpr_wf X E de  E `prefix_of` E'  dexpr_interp E de = dexpr_interp E' de.
532 533 534 535 536 537 538 539 540
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.
  by rewrite (dval_interp_mono E E').
Qed.

Léon Gondelman 's avatar
Léon Gondelman committed
541
Lemma dcexpr_interp_mono (X: list string) (E E': known_locs) (de: dcexpr) :
Dan Frumin's avatar
Dan Frumin committed
542 543
  dcexpr_wf X E de  E `prefix_of` E' 
  dcexpr_interp E de = dcexpr_interp E' de.
544
Proof.
Dan Frumin's avatar
Dan Frumin committed
545 546 547 548 549 550 551 552
  revert X.
  induction de; simplify_eq /=; intros X H Hpre; eauto;
    destruct_and?;
    try by rewrite (IHde X)
       || (rewrite (IHde2 X) // (IHde1 X) //).
  - by rewrite (dexpr_interp_mono X E E').
  - rewrite (IHde1 X) //.
    by erewrite (IHde2 (_::X)).
553 554
Qed.

555 556 557
Global Instance dexpr_closed X E de :
  dexpr_wf X E de 
  Closed X (dexpr_interp E de).
558
Proof.
559 560 561 562
  revert X. induction de; simpl; intros; unfold Closed; simpl; eauto using is_closed_of_val;
              try by apply IHde.
  destruct_and!. by split_and; [apply IHde1 | apply IHde2].
  by apply W.is_closed_correct.
563 564
Qed.

565 566
Global Instance dcexpr_closed X E de :
  dcexpr_wf X E de 
567
  Closed X (dcexpr_interp E de).
568
Proof.
569 570 571 572 573 574 575 576
  revert X. induction de; intros; unfold Closed in *; simplify_eq /=;
   try (destruct_and!; split_and; first split_and; [ apply is_closed_of_val | by apply IHde2 | by apply IHde1]);
   try (destruct_and!; split_and; first split_and; [ apply is_closed_of_val | by apply IHde1 | by apply IHde2]).
  - split_and; eauto using is_closed_of_val. by apply dexpr_closed.
  - split_and;  [ apply is_closed_of_val | by apply IHde].
  - split_and;  [ apply is_closed_of_val | by apply IHde].
  - split_and; first split_and; [ apply is_closed_of_val | apply is_closed_of_val | by apply  IHde].
  - by apply W.is_closed_correct.
577
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
578

579 580
(** * Reification of C syntax *)
(** ** LocLookup *)
581
Class LocLookup (E : known_locs) (l : cloc) (i : nat) :=
582 583 584 585 586 587 588 589 590
  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.

591 592 593 594 595 596 597 598 599 600 601
Class IntoCLocPlus (l : cloc) (k : cloc) (j : nat) :=
  into_cloc_plus : l = cloc_plus k j.

Global Instance into_cloc_plus_here l : IntoCLocPlus l l 0 | 100.
Proof. by rewrite /IntoCLocPlus cloc_plus_0. Qed.

Global Instance into_cloc_plus_plus l l' i j :
  IntoCLocPlus l l' i 
  IntoCLocPlus (cloc_plus l j) l' (i + j).
Proof. rewrite /IntoCLocPlus=> ->. by rewrite cloc_plus_plus. Qed.

Dan Frumin's avatar
Dan Frumin committed
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622
(** ** IntoDInt *)
Class IntoDInt (i : Z) (l : dint) :=
  into_dint : i = dint_interp l.

Global Instance intodint_zero : IntoDInt 0 (dNat 0).
Proof. done. Qed.

Global Instance intodint_pos (o : positive) :
  IntoDInt (Z.pos o) (dNat (Pos.to_nat o)).
Proof. rewrite /IntoDInt. by rewrite -positive_nat_Z. Qed.

(* DF: This is here to reify unknown naturals, ie meta-variables which
   value is unknown, but we do know that they are natural numbers *)
Global Instance intodint_of_nat (n : nat) :
  IntoDInt (Z.of_nat n) (dNat n).
Proof. done. Qed.

Global Instance intodint_unknown (i : Z) :
  IntoDInt i (dIntUnknown i) | 100.
Proof. done. Qed.

623
(** ** IntoDBaseLit *)
624 625
Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) :=
  into_dbase_lit : l = dbase_lit_interp dl.
626

Dan Frumin's avatar
Dan Frumin committed
627 628 629 630
Global Instance into_dbase_lit_dint i l :
  IntoDInt i l 
  IntoDBaseLit (LitInt i) (dLitInt l).
Proof. intros ->. split; eauto. Qed.
631

632 633
Global Instance into_dbase_lit_default l :
  IntoDBaseLit l (dLitUnknown l) | 1000.
634 635 636 637 638 639 640
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 }.

641
Global Instance expr_into_dval_lit E l dl :
642
  IntoDBaseLit l dl  ExprIntoDVal E (Lit l) (dLitV dl).
643 644
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

645 646 647 648
Global Instance expr_into_dval_loc E l k i j :
  IntoCLocPlus l k j 
  LocLookup E k i  ExprIntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1.
Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //. Qed.
649 650

Global Instance expr_into_dval_loc_unknown E l :
651
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 100.
652
Proof. done. Qed.
653 654 655 656 657 658 659 660 661 662

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 }.

663
Global Instance into_dval_lit E l dl :
664
  IntoDBaseLit l dl  IntoDVal E (LitV l) (dLitV dl).
665 666
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

667 668 669 670
Global Instance into_dval_loc E l k i j :
  IntoCLocPlus l k j 
  LocLookup E k i  IntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1.
Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //. Qed.
671 672 673 674

Global Instance into_dval_loc_unknown E l :
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
675 676 677 678

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

679 680
(** ** IntoDExpr *)
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
681
  into_dexpr : e = dexpr_interp E de.
682 683 684 685

Global Instance into_dexpr_val E e dv :
  ExprIntoDVal E e dv 
  IntoDExpr E e (dEVal dv) | 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Proof. by intros [-> ?]. Qed.
687

Léon Gondelman 's avatar
Léon Gondelman committed
688 689
Global Instance into_dexpr_var E x :
  IntoDExpr E (Var x) (dEVar x) | 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
690
Proof. done. Qed.
691 692 693 694

Global Instance into_dexpr_pair E e1 e2 de1 de2 :
  IntoDExpr E e1 de1  IntoDExpr E e2 de2 
  IntoDExpr E (Pair e1 e2) (dEPair de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
695
Proof. by rewrite /IntoDExpr=> -> ->. Qed.
696 697 698 699

Global Instance into_dexpr_fst E e de:
  IntoDExpr E e de 
  IntoDExpr E (Fst e) (dEFst de).
Robbert Krebbers's avatar
Robbert Krebbers committed
700
Proof. by rewrite /IntoDExpr=> ->. Qed.
701 702 703 704

Global Instance into_dexpr_snd E e de:
  IntoDExpr E e de 
  IntoDExpr E (Snd e) (dESnd de).
Robbert Krebbers's avatar
Robbert Krebbers committed
705
Proof. by rewrite /IntoDExpr=> ->. Qed.
706

Robbert Krebbers's avatar
Robbert Krebbers committed
707 708 709 710
Lemma into_dexpr_unknown {E e} de :
  e = W.to_expr de 
  IntoDExpr E e (dEUnknown de).
Proof. by intros ->. Qed.
711

Robbert Krebbers's avatar
Robbert Krebbers committed
712 713 714
Hint Extern 100 (IntoDExpr _ ?e _) =>
  let e' := W.of_expr e in
  apply (into_dexpr_unknown e'); reflexivity : typeclass_instances.
715 716 717

(** ** IntoDCExpr *)
Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
718
  into_dcexpr : e = dcexpr_interp E de.
Robbert Krebbers's avatar
Robbert Krebbers committed
719

720 721 722
Global Instance into_dcexpr_ret E e de:
  IntoDExpr E e de 
  IntoDCExpr E (a_ret e) (dCRet de).
Robbert Krebbers's avatar
Robbert Krebbers committed
723
Proof. by rewrite /IntoDExpr=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
724

Léon Gondelman 's avatar
Léon Gondelman committed
725 726 727 728
Global Instance into_dcexpr_bind E x e1 e2 de1 de2:
  IntoDCExpr E e1 de1 
  IntoDCExpr E e2 de2 
  IntoDCExpr E (BNamed x ←ᶜ e1 ;; e2) (dCBind x de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
729
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
730

731
Global Instance into_dcexpr_alloc E e1 e2 de1 de2 :
732 733
  IntoDCExpr E e1 de1  IntoDCExpr E e2 de2 
  IntoDCExpr E (a_alloc e1 e2) (dCAlloc de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
734
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
735 736

Global Instance into_dcexpr_load E e de:
737 738
  IntoDCExpr E e de 
  IntoDCExpr E (a_load e) (dCLoad de).
Robbert Krebbers's avatar
Robbert Krebbers committed
739
Proof. by rewrite /IntoDCExpr=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
740 741

Global Instance into_dcexpr_store E e1 e2 de1 de2:
742 743 744
  IntoDCExpr E e1 de1 
  IntoDCExpr E e2 de2 
  IntoDCExpr E (a_store e1 e2) (dCStore de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
745
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
746 747

Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
748 749 750
  IntoDCExpr E e1 de1 
  IntoDCExpr E e2 de2 
  IntoDCExpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
751
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
752

Dan Frumin's avatar
Dan Frumin committed
753
Global Instance into_dcexpr_prebinop E e1 e2 op de1 de2:
754 755 756
  IntoDCExpr E e1 de1 
  IntoDCExpr E e2 de2 
  IntoDCExpr E (a_pre_bin_op op e1 e2) (dCPreBinOp op de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
757
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Dan Frumin's avatar
Dan Frumin committed
758

759
Global Instance into_dcexpr_unop E e op de:
760 761
  IntoDCExpr E e de 
  IntoDCExpr E (a_un_op op e) (dCUnOp op de).
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Proof. by rewrite /IntoDCExpr=> ->. Qed.
763

Robbert Krebbers's avatar
Robbert Krebbers committed
764
Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
765 766 767
  IntoDCExpr E e1 de1 
  IntoDCExpr E e2 de2 
  IntoDCExpr E (e1 ; e2) (dCSeq de1 de2).
Robbert Krebbers's avatar
Robbert Krebbers committed
768
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
769

770
Global Instance into_dcexpr_par E e1 e2 de1 de2:
771 772 773
  IntoDCExpr