dcexpr.v 31.9 KB
Newer Older
1 2
From iris_c.c_translation Require Export translation.
Local Open Scope Z_scope.
3

4
Definition known_locs := list cloc.
5

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Inductive Z_or_nat :=
  | IntZ : Z  Z_or_nat
  | IntNat : nat  Z_or_nat.
Record dint := dInt { dint_known : Z; dint_unknown : option Z_or_nat }.

Instance Z_or_nat_eq_dec : EqDecision Z_or_nat.
Proof. solve_decision. Defined.
Instance dint_eq_dec : EqDecision dint.
Proof. solve_decision. Defined.

Inductive dbase_loc :=
  | dLocKnown : nat  dbase_loc
  | dLocUnknown : cloc  dbase_loc.

Instance dbase_loc_eq_dec : EqDecision dbase_loc.
Proof. solve_decision. Defined.

Record dloc := dLoc { dloc_base : dbase_loc; dloc_offset : dint }.
Robbert Krebbers's avatar
Robbert Krebbers committed
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Instance dloc_eq_dec : EqDecision dloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
Proof. solve_decision. Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30
Inductive dbool :=
  | dBoolKnown : bool  dbool
  | dBoolUnknown : bool  dbool.
Dan Frumin's avatar
Dan Frumin committed
31

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Instance dbool_eq_dec : EqDecision dbool.
Dan Frumin's avatar
Dan Frumin committed
33 34
Proof. solve_decision. Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Inductive dbase_lit : Type :=
Dan Frumin's avatar
Dan Frumin committed
36
  | dLitInt : dint  dbase_lit
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  | dLitBool : dbool  dbase_lit
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40
  | dLitUnit : dbase_lit
  | dLitUnknown : base_lit  dbase_lit.

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Instance dbase_lit_eq_dec : EqDecision dbase_lit.
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45
Proof. solve_decision. Defined.

Inductive dval : Type :=
  | dLitV : dbase_lit  dval
46
  | dPairV : dval  dval  dval
47
  | dLocV : dloc  dval
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  | dNone : dval
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50
  | dValUnknown : val  dval.

Robbert Krebbers's avatar
Robbert Krebbers committed
51
Instance dval_eq_dec : EqDecision dval.
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
Proof. solve_decision. Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62 63 64 65
Inductive dexpr : Type :=
  | dEVal : dval  dexpr
  | dEVar : string  dexpr
  | dEPair : dexpr  dexpr  dexpr
  | dEFst : dexpr  dexpr
  | dESnd : dexpr  dexpr
  | dENone : dexpr
  | dEUnknown : expr  dexpr.

Inductive dcexpr : Type :=
  | dCRet : dexpr  dcexpr
  | dCSeqBind : binder  dcexpr  dcexpr  dcexpr
66
  | dCMutBind : binder  dcexpr  dcexpr  dcexpr
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
  | dCAlloc : dcexpr  dcexpr  dcexpr
  | dCLoad : dcexpr  dcexpr
  | dCStore : dcexpr  dcexpr  dcexpr
  | dCBinOp : cbin_op  dcexpr  dcexpr  dcexpr
  | dCPreBinOp : cbin_op  dcexpr  dcexpr  dcexpr
  | dCUnOp : un_op  dcexpr  dcexpr
  | dCPar : dcexpr  dcexpr  dcexpr
  | dCWhile : dcexpr  dcexpr  dcexpr
  | dCWhileV : dcexpr  dcexpr  dcexpr
  | dCCall : val  dcexpr  dcexpr
  | dCUnknown : expr  dcexpr.

Fixpoint dcexpr_size (de : dcexpr) : nat :=
  match de with
  | dCRet _ | dCUnknown _ => 1
82
  | dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 |dCAlloc de1 de2 | dCStore de1 de2
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88 89 90 91 92 93 94 95
     | dCBinOp _ de1 de2 | dCPreBinOp _ de1 de2 | dCPar de1 de2
     | dCWhile de1 de2 | dCWhileV de1 de2 => S (dcexpr_size de1 + dcexpr_size de2)
  | dCLoad de | dCUnOp _ de | dCCall _ de => S (dcexpr_size de)
  end.

Definition dloc_of_dval (dv : dval) : option dloc :=
  match dv with dLocV dl => Some dl | _ => None end.
Definition dint_of_dval (dv : dval) : option dint :=
  match dv with  dLitV (dLitInt di) => Some di | _ => None end.
Definition dknown_bool_of_dval (dv : dval) : option bool :=
  match dv with dLitV (dLitBool (dBoolKnown b)) => Some b | _ => None end.

Definition dloc_var_of_dloc (dl : dloc) : option nat :=
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  match dl with
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
  | dLoc (dLocKnown i) (dInt 0 None) => Some i
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101
Definition dloc_var_of_dval (dv : dval) : option nat :=
  dl  dloc_of_dval dv; dloc_var_of_dloc dl.
Robbert Krebbers's avatar
Robbert Krebbers committed
102

Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
Definition nat_of_dint (di : dint) : option (nat * option nat) :=
  match di with
  | dInt i None => guard (0  i); Some (Z.to_nat i, None) 
  | dInt i (Some (IntNat j)) => guard (0  i); Some (Z.to_nat i, Some j)
  | _ => None
  end.
Definition succ_nat_of_dint (di : dint) : option dint :=
  ''(i,mj)  nat_of_dint di;
  match i with O => None | S i => Some (dInt i (IntNat <$> mj)) end.

Definition nat_of_dval (dv : dval) : option (nat * option nat) :=
  dl  dint_of_dval dv; nat_of_dint dl.
Definition succ_nat_of_dval (dv : dval) : option dint :=
  dl  dint_of_dval dv; succ_nat_of_dint dl.

(** Well-formedness *)
Definition dloc_var_wf (E : known_locs) (i : nat) : bool :=
  bool_decide (is_Some (E !! i)).

Definition dbase_loc_wf (E : known_locs) (dl : dbase_loc) : bool :=
  match dl with dLocKnown i => dloc_var_wf E i | _  => true end.

Definition dloc_wf (E : known_locs) (dl : dloc) : bool :=
  dbase_loc_wf E (dloc_base dl).

Fixpoint dval_wf (E : known_locs) (dv : dval) : bool :=
  match dv with
  | dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
  | dLocV dl => dloc_wf E dl
  | _  => true
  end.

Fixpoint dexpr_wf (E : known_locs) (de : dexpr) : bool :=
  match de with
  | dEVal dv => dval_wf E dv
  | dEVar _ | dEUnknown _ | dENone => true
  | dEFst de | dESnd de => dexpr_wf E de
  | dEPair de1 de2 => dexpr_wf E de1 && dexpr_wf E de2
  end.

Fixpoint dcexpr_wf (E : known_locs) (de : dcexpr) : bool :=
  match de with
  | dCRet de => dexpr_wf E de
146
  | dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
  | dCLoad de1 | dCUnOp _ de1 | dCCall _ de1 => dcexpr_wf E de1
  | dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
  | dCPreBinOp _ de1 de2 | dCWhile de1 de2 | dCWhileV de1 de2 | dCPar de1 de2 =>
     dcexpr_wf E de1 && dcexpr_wf E de2
  | dCUnknown e => true
  end.

(** Interpretation *)
Definition Z_or_nat_interp (x : Z_or_nat) : Z :=
  match x with IntZ x => x | IntNat x => x end.
Arguments Z_or_nat_interp !_ /.

(* Defined in such a way that the interpretation is normalized. The lemma
[dint_interp_alt] proves correspondence to an alternative definition that is
better for proofs. *)
Definition dint_interp' (di : dint) : option Z :=
Dan Frumin's avatar
Dan Frumin committed
163
  match di with
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
  | dInt 0 None => None
  | dInt (Zpos p) None => Some (Z.of_nat (Pos.to_nat p))
  | dInt x None => Some x
  | dInt 0 (Some y) => Some (Z_or_nat_interp y)
  | dInt (Zpos p) (Some (IntNat n)) => Some (Z.of_nat (Pos.to_nat p + n))
  | dInt x (Some y) => Some (x + Z_or_nat_interp y)
  end.
Arguments dint_interp' !_ / : simpl nomatch.
Arguments Pos.to_nat !_ /.

Definition dint_interp (di : dint) : Z :=
  default 0 (dint_interp' di).
Arguments dint_interp !_ / : simpl nomatch.

Lemma dint_interp_alt di :
  dint_interp di = dint_known di + from_option Z_or_nat_interp 0 (dint_unknown di).
Proof. destruct di as [[] [[]|]]=> //=; lia. Qed.

Definition dloc_var_interp (E : known_locs) (i : nat) : cloc :=
  default inhabitant (E !! i).
Arguments dloc_var_interp !_ !_ /.

Definition dbase_loc_interp (E : known_locs) (dl : dbase_loc) : cloc :=
  match dl with
  | dLocKnown i => dloc_var_interp E i
  | dLocUnknown cl => cl
  end.
Arguments dbase_loc_interp _ !_ / : simpl nomatch.

Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
  match dl with
  | dLoc i dj => 
     match dint_interp' dj with
     | Some j => dbase_loc_interp E i + j
     | None => dbase_loc_interp E i
     end
  end.
Arguments dloc_interp _ !_ / : simpl nomatch.
Lemma dloc_interp_alt E dl :
  dloc_interp E dl = dbase_loc_interp E (dloc_base dl) + dint_interp (dloc_offset dl).
Proof. destruct dl as [? [[] [[]|]]]=> //=. Qed.

Definition dbool_interp (db : dbool) : bool :=
  match db with
  | dBoolKnown b => b
  | dBoolUnknown b => b
Dan Frumin's avatar
Dan Frumin committed
210
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
Arguments dbool_interp !_ /.
Dan Frumin's avatar
Dan Frumin committed
212

213
Definition dbase_lit_interp (l : dbase_lit) : base_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  match l with
Dan Frumin's avatar
Dan Frumin committed
215
  | dLitInt x => LitInt (dint_interp x)
Robbert Krebbers's avatar
Robbert Krebbers committed
216
  | dLitBool b => LitBool (dbool_interp b)
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218 219
  | dLitUnit => LitUnit
  | dLitUnknown l => l
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
Arguments dbase_lit_interp !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  match v with
224
  | dLitV l => LitV (dbase_lit_interp l)
225
  | dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
226
  | dLocV dl => cloc_to_val (dloc_interp E dl)
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  | dNone => NONEV
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229
  | dValUnknown v => v
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Arguments dval_interp _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
231

Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236 237 238 239 240
Fixpoint dexpr_interp (E : known_locs) (de : dexpr) : expr :=
  match de with
  | dEVal dv => dval_interp E dv
  | dEVar x => Var x
  | 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)
  | dENone => NONE
  | dEUnknown e => e
Dan Frumin's avatar
Dan Frumin committed
241 242
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
243 244 245 246
Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr :=
  match de with
  | dCRet de => a_ret (dexpr_interp E de)
  | dCSeqBind x de1 de2 => x ←ᶜ (dcexpr_interp E de1) ; (dcexpr_interp E de2)
247
  | dCMutBind x de1 de2 => x mut (dcexpr_interp E de1) ; (dcexpr_interp E de2)
Robbert Krebbers's avatar
Robbert Krebbers committed
248 249 250 251 252 253 254 255 256
  | dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2)
  | 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)
  | dCPreBinOp op de1 de2 => a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
  | dCUnOp op de => a_un_op op (dcexpr_interp E de)
  | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
  | dCWhile de1 de2 => while (dcexpr_interp E de1) { dcexpr_interp E de2 }
  | dCWhileV de1 de2 => whileV (dcexpr_interp E de1) { dcexpr_interp E de2 }
257
  | dCCall fv de => call fv (dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259
  | dCUnknown e1 => e1
  end.
Dan Frumin's avatar
Dan Frumin committed
260

Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 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 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
(* Operations *)
Definition dbool_and (db1 db2 : dbool) : dbool :=
  match db1, db2 with
  | dBoolKnown false, _ => dBoolKnown false
  | dBoolKnown true, _ => db2
  | dBoolUnknown _, dBoolKnown false => dBoolKnown false
  | dBoolUnknown _, dBoolKnown true => db1
  | dBoolUnknown b1, dBoolUnknown b2 => dBoolUnknown (b1 && b2)
  end.
Arguments dbool_and !_ _ / : simpl nomatch.

Definition dbool_or (db1 db2 : dbool) : dbool :=
  match db1, db2 with
  | dBoolKnown true, _ => dBoolKnown true
  | dBoolKnown false, _ => db2
  | dBoolUnknown _, dBoolKnown true => dBoolKnown true
  | dBoolUnknown _, dBoolKnown false => db1
  | dBoolUnknown b1, dBoolUnknown b2 => dBoolUnknown (b1 || b2)
  end.
Arguments dbool_or !_ _ / : simpl nomatch.

Definition dbool_xor (db1 db2 : dbool) : dbool :=
  match db1, db2 with
  | dBoolKnown b1, dBoolKnown b2 => dBoolKnown (xorb b1 b2)
  | dBoolKnown b1, dBoolUnknown b2 => dBoolUnknown (xorb b1 b2)
  | dBoolUnknown b1, (dBoolKnown b2 | dBoolUnknown b2) => dBoolUnknown (xorb b1 b2)
  end.
Arguments dbool_xor !_ _ / : simpl nomatch.

Definition dbool_eq (db1 db2 : dbool) : dbool :=
  match db1, db2 with
  | dBoolKnown b1, dBoolKnown b2 => dBoolKnown (bool_decide (b1 = b2))
  | dBoolKnown b1, dBoolUnknown b2 => dBoolUnknown (bool_decide (b1 = b2))
  | dBoolUnknown b1, (dBoolKnown b2 | dBoolUnknown b2) => dBoolUnknown (bool_decide (b1 = b2))
  end.
Arguments dbool_eq !_ _ / : simpl nomatch.

Definition dbool_neg (db : dbool) : dbool :=
  match db with
  | dBoolKnown b => dBoolKnown (negb b)
  | dBoolUnknown b => dBoolUnknown (negb b)
  end.
Arguments dbool_neg !_ /.

Definition dint_plus (di1 di2 : dint) : dint :=
  match di1, di2 with
  | dInt x1 None, dInt x2 None => dInt (x1 + x2) None
  | dInt x1 (Some y1), dInt x2 None => dInt (x1 + x2) (Some y1)
  | dInt x1 None, dInt x2 (Some y2) => dInt (x1 + x2) (Some y2)
  | dInt x1 (Some (IntNat y1)), dInt x2 (Some (IntNat y2)) =>
     dInt (x1 + x2) (Some (IntNat (y1 + y2)))
  | dInt x1 (Some y1), dInt x2 (Some y2) =>
     dInt (x1 + x2) (Some (IntZ (Z_or_nat_interp y1 + Z_or_nat_interp y2)))
  end.
Arguments dint_plus !_ !_ / : simpl nomatch.

Definition dint_minus (di1 di2 : dint) : dint :=
  match di1, di2 with
  | dInt x1 None, dInt x2 None => dInt (x1 - x2) None
  | dInt x1 (Some y1), dInt x2 None => dInt (x1 - x2) (Some y1)
  | dInt x1 None, dInt x2 (Some y2) =>
     dInt (x1 - x2) (Some (IntZ (-Z_or_nat_interp y2)))
  | dInt x1 (Some y1), dInt x2 (Some y2) =>
     dInt (x1 - x2) (Some (IntZ (Z_or_nat_interp y1 - Z_or_nat_interp y2)))
  end.
Arguments dint_minus !_ !_ / : simpl nomatch.

Definition dint_opp (di : dint) : dint :=
  match di with
  | dInt x None => dInt (-x) None
  | dInt x (Some y) => dInt (-x) (Some (IntZ (-Z_or_nat_interp y)))
  end.
Arguments dint_opp !_ / : simpl nomatch.

Definition dint_lt (di1 di2 : dint) : dbool :=
  match di1, di2 with
  | dInt x1 None, dInt x2 None => dBoolKnown (bool_decide (x1 < x2))
  | dInt x1 None, dInt x2 (Some (IntNat _)) =>
     if bool_decide (x1 < x2) then dBoolKnown true
     else dBoolUnknown (bool_decide (dint_interp di1 < dint_interp di2))
  | _, _ => dBoolUnknown (bool_decide (dint_interp di1 < dint_interp di2))
  end.
Arguments dint_lt !_ !_ / : simpl nomatch.

Definition dint_le (di1 di2 : dint) : dbool :=
  match di1, di2 with
  | dInt x1 None, dInt x2 None => dBoolKnown (bool_decide (x1  x2))
  | _, _ => dBoolUnknown (bool_decide (dint_interp di1  dint_interp di2))
  end.
Arguments dint_le !_ !_ / : simpl nomatch.

Definition dint_eq (di1 di2 : dint) : dbool :=
  match di1, di2 with
  | dInt x1 None, dInt x2 None => dBoolKnown (bool_decide (x1 = x2))
  | _, _ => dBoolUnknown (bool_decide (dint_interp di1 = dint_interp di2))
  end.
Arguments dint_eq !_ !_ / : simpl nomatch.

Definition dbase_loc_strong_eq (dl1 dl2 : dbase_loc) : bool :=
  match dl1, dl2 with
  | dLocKnown i1, dLocKnown i2 => bool_decide (i1 = i2)
  | _, _ => false
  end.
Arguments dbase_loc_strong_eq !_ !_ / : simpl nomatch.

Definition dloc_plus (dl : dloc) (dj : dint) : dloc :=
  match dl with
  | dLoc dl di => dLoc dl (dint_plus di dj)
  end.
Arguments dloc_plus !_ !_ / : simpl nomatch.

Definition dloc_eq (E : known_locs) (dl1 dl2 : dloc) : dbool :=
  if dbase_loc_strong_eq (dloc_base dl1) (dloc_base dl2)
  then dint_eq (dloc_offset dl1) (dloc_offset dl2)
  else dBoolUnknown (bool_decide (dloc_interp E dl1 = dloc_interp E dl2)).
Arguments dloc_eq _ !_ !_ / : simpl nomatch.

Definition dloc_lt (E : known_locs) (dl1 dl2 : dloc) : dbool :=
  if dbase_loc_strong_eq (dloc_base dl1) (dloc_base dl2)
  then dint_lt (dloc_offset dl1) (dloc_offset dl2)
  else dBoolUnknown (cloc_lt (dloc_interp E dl1) (dloc_interp E dl2)).
Arguments dloc_lt _ !_ !_ / : simpl nomatch.

Definition dbin_op_eval_bool (op : bin_op) (db1 db2 : dbool) : option dbase_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
385
  match op with
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387 388 389 390 391 392 393 394
  | AndOp => Some $ dLitBool $ dbool_and db1 db2
  | OrOp => Some $ dLitBool $ dbool_or db1 db2
  | XorOp => Some $ dLitBool $ dbool_xor db1 db2
  | EqOp => Some $ dLitBool $ dbool_eq db1 db2
  | _ => None
  end.
Arguments dbin_op_eval_bool !_ _ _ /.

Definition dbin_op_eval_int (op : bin_op) (di1 di2 : dint) : dbase_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  match op with
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  | PlusOp => dLitInt $ dint_plus di1 di2
  | MinusOp => dLitInt $ dint_minus di1 di2
  | EqOp => dLitBool $ dint_eq di1 di2
  | LtOp => dLitBool $ dint_lt di1 di2
  | LeOp => dLitBool $ dint_le di1 di2
  | _ => dLitUnknown $ bin_op_eval_int op (dint_interp di1) (dint_interp di2)
         (* Do better in case both operands are known *)
  end.
Arguments dbin_op_eval_int !_ _ _ /.

Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool :=
  match dl1, dl2 with
  | dLitInt di1, dLitInt di2 => dint_eq di1 di2
  | dLitBool db1, dLitBool db2 => dbool_eq db1 db2
  | dLitUnit, dLitUnit => dBoolKnown true
  | dLitInt _, (dLitUnit | dLitBool _)
     | dLitBool _, (dLitInt _ | dLitUnit)
     | dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *)
  | _, _ => dBoolUnknown (bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2))
  end.
Arguments dbase_lit_eq !_ !_ / : simpl nomatch.

Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool :=
  match dv1, dv2 with
  | dLitV dl1, dLitV dl2 => dbase_lit_eq dl1 dl2
  | dNone, dNone => dBoolKnown true
  | dPairV dv1 dv1', dPairV dv2 dv2' => dbool_and (dval_eq E dv1 dv2) (dval_eq E dv1' dv2')
  | dLocV dl1, dLocV dl2 => dloc_eq E dl1 dl2
  | dLitV _, (dNone | dPairV _ _ | dLocV _)
     | dNone, (dLitV _ | dPairV _ _ | dLocV _)
     | dPairV _ _, (dNone | dLitV _ | dLocV _)
     | dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *)
  | _, _ => dBoolUnknown (bool_decide (dval_interp E dv1 = dval_interp E dv2))
  end.
Arguments dval_eq _ !_ !_ / : simpl nomatch.

Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
  if decide (op = EqOp) then Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2 else
  match dv1, dv2 with
  | dLitV (dLitInt di1), dLitV (dLitInt di2) => Some $ dLitV $ dbin_op_eval_int op di1 di2
  | dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2
437
  | _, _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
438
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
439
Arguments dbin_op_eval _ !_ _ _ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
440

Robbert Krebbers's avatar
Robbert Krebbers committed
441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
Definition dcbin_op_eval (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) : option dval :=
  match op with
  | CBinOp op' => dbin_op_eval E op' dv1 dv2
  | PtrPlusOp =>
     dl  dloc_of_dval dv1;
     di  dint_of_dval dv2;
     Some $ dLocV $ dloc_plus dl di
  | PtrLtOp =>
     dl1  dloc_of_dval dv1;
     dl2  dloc_of_dval dv2;
     Some $ dLitV $ dLitBool $ dloc_lt E dl1 dl2
  end.
Arguments dcbin_op_eval _ !_ !_ !_ / : simpl nomatch.

Definition dun_op_eval (E : known_locs) (op : un_op) (dv : dval) : option dval :=
  match op, dv with
  | NegOp, dLitV (dLitBool db) => Some $ dLitV $ dLitBool $ dbool_neg db
  | MinusUnOp, dLitV (dLitInt di) => Some $ dLitV $ dLitInt $ dint_opp di
  | _, _ => None
460
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
461
Arguments dun_op_eval _ !_ !_ / : simpl nomatch.
462

Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465 466 467 468 469 470
(** Correctness proofs *)
Lemma dloc_of_dval_Some dv dl : dloc_of_dval dv = Some dl  dv = dLocV dl.
Proof. intros. by destruct dv; simplify_eq/=. Qed.
Lemma dint_of_dval_Some dv di : dint_of_dval dv = Some di  dv = dLitV (dLitInt di).
Proof. intros. by destruct dv as [[]| | | |]; simplify_eq/=. Qed.

Lemma dknown_bool_of_dval_Some dv b :
  dknown_bool_of_dval dv = Some b  dv = dLitV (dLitBool (dBoolKnown b)).
471
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
  rewrite /dknown_bool_of_dval. intros; by repeat (simplify_eq/= || case_match).
473
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
474 475 476
Lemma dknown_bool_of_dval_correct E dv b :
  dknown_bool_of_dval dv = Some b  dval_interp E dv = #b.
Proof. by intros ->%dknown_bool_of_dval_Some. Qed.
477

Robbert Krebbers's avatar
Robbert Krebbers committed
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501
Lemma dloc_var_of_dloc_Some dl i :
  dloc_var_of_dloc dl = Some i  dl = dLoc (dLocKnown i) (dInt 0 None).
Proof.
  rewrite /dloc_var_of_dloc. intros; by repeat (simplify_eq/= || case_match).
Qed.
Lemma dloc_var_of_dval_Some dv i :
  dloc_var_of_dval dv = Some i  dv = dLocV (dLoc (dLocKnown i) (dInt 0 None)).
Proof. by intros (dl&->%dloc_of_dval_Some&->%dloc_var_of_dloc_Some)%bind_Some. Qed.
Lemma dloc_var_of_dval_wf E dv i :
  dloc_var_of_dval dv = Some i  dval_wf E dv  dloc_var_wf E i.
Proof. by intros ->%dloc_var_of_dval_Some. Qed.
Lemma dloc_var_of_dval_correct E dv i :
  dloc_var_of_dval dv = Some i  dval_interp E dv = cloc_to_val (dloc_var_interp E i).
Proof. by intros ->%dloc_var_of_dval_Some. Qed.

Lemma nat_of_dint_Some di i mj :
  nat_of_dint di = Some (i,mj)  di = dInt i (IntNat <$> mj).
Proof.
  destruct di as [i' [[j|]|]]; intros;
    repeat (simplify_eq/= || case_option_guard); by rewrite Z2Nat.id.
Qed.
Lemma nat_of_dval_Some dv i mj :
  nat_of_dval dv = Some (i,mj)  dv = dLitV (dLitInt (dInt i (IntNat <$> mj))).
Proof. by intros (di&->%dint_of_dval_Some&->%nat_of_dint_Some)%bind_Some. Qed.
502

Robbert Krebbers's avatar
Robbert Krebbers committed
503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
Lemma succ_nat_of_dint_Some di dj :
  succ_nat_of_dint di = Some dj 
  dint_interp di = S (Z.to_nat (dint_interp dj)).
Proof.
  intros ([[|i] [j|]] & ->%nat_of_dint_Some & [= <-])%bind_Some;
    rewrite !dint_interp_alt /=.
  - rewrite -Z2Nat.inj_succ; last by lia. rewrite Z2Nat.id; lia.
  - rewrite -Z2Nat.inj_succ; last by lia. rewrite Z2Nat.id; lia.
Qed.
Lemma succ_nat_of_dval_Some E dv di :
  succ_nat_of_dval dv = Some di 
  dval_interp E dv = #(S (Z.to_nat (dint_interp di))).
Proof. by intros (dl&->%dint_of_dval_Some&<-%succ_nat_of_dint_Some)%bind_Some. Qed.

Lemma dbool_and_correct db1 db2 :
  dbool_interp (dbool_and db1 db2) = dbool_interp db1 && dbool_interp db2.
Proof. by destruct db1 as [[]|[]], db2 as [[]|[]]. Qed.
Lemma dbool_or_correct db1 db2 :
  dbool_interp (dbool_or db1 db2) = dbool_interp db1 || dbool_interp db2.
Proof. by destruct db1 as [[]|[]], db2 as [[]|[]]. Qed.
Lemma dbool_xor_correct db1 db2 :
  dbool_interp (dbool_xor db1 db2) = xorb (dbool_interp db1) (dbool_interp db2).
Proof. by destruct db1 as [[]|[]], db2 as [[]|[]]. Qed.
Lemma dbool_eq_correct db1 db2 :
  dbool_interp (dbool_eq db1 db2) = bool_decide (dbool_interp db1 = dbool_interp db2).
Proof. by destruct db1 as [[]|[]], db2 as [[]|[]]. Qed.
Lemma dbool_neg_correct db :
  dbool_interp (dbool_neg db) = negb (dbool_interp db).
Proof. by destruct db as [[]|[]]. Qed.

Lemma dint_plus_correct di1 di2 :
  dint_interp (dint_plus di1 di2) = dint_interp di1 + dint_interp di2.
Proof.
  rewrite !dint_interp_alt. destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; lia.
Qed.
Lemma dint_minus_correct di1 di2 :
  dint_interp (dint_minus di1 di2) = dint_interp di1 - dint_interp di2.
Proof.
  rewrite !dint_interp_alt. destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; lia.
Qed.
Lemma dint_opp_correct di :
  dint_interp (dint_opp di) = -dint_interp di.
Proof. rewrite !dint_interp_alt. destruct di as [? [[]|]]; simpl; lia. Qed.
Lemma dint_lt_correct di1 di2 :
  dbool_interp (dint_lt di1 di2) = bool_decide (dint_interp di1 < dint_interp di2).
Proof.
  rewrite /dint_lt !dint_interp_alt.
  destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; repeat case_bool_decide; auto with lia.
Qed.
Lemma dint_le_correct di1 di2 :
  dbool_interp (dint_le di1 di2) = bool_decide (dint_interp di1  dint_interp di2).
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
555 556 557 558 559
  rewrite /dint_le !dint_interp_alt.
  destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; repeat case_bool_decide; auto with lia.
Qed.
Lemma dint_eq_correct di1 di2 :
  dbool_interp (dint_eq di1 di2) = bool_decide (dint_interp di1 = dint_interp di2).
560
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
561 562
  rewrite /dint_eq !dint_interp_alt.
  destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; repeat case_bool_decide; auto with lia.
563 564
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
Lemma dbase_loc_strong_eq_correct E dl1 dl2 :
  dbase_loc_strong_eq dl1 dl2 = true  dbase_loc_interp E dl1 = dbase_loc_interp E dl2.
Proof. intros; destruct dl1, dl2; by simplify_option_eq. Qed.
Lemma dloc_plus_correct E dl di :
  dloc_interp E (dloc_plus dl di) = dloc_interp E dl + dint_interp di.
Proof.
  rewrite !dloc_interp_alt. by destruct dl as [dl dj]; rewrite /= dint_plus_correct cloc_plus_plus.
Qed.
Lemma dloc_lt_correct E dl1 dl2 :
  dbool_interp (dloc_lt E dl1 dl2) = cloc_lt (dloc_interp E dl1) (dloc_interp E dl2).
Proof.
  unfold dloc_lt. destruct (dbase_loc_strong_eq _ _) eqn:H; last done.
  rewrite dint_lt_correct /cloc_lt !dloc_interp_alt /=.
  apply (dbase_loc_strong_eq_correct E) in H as ->.
  repeat case_bool_decide; naive_solver eauto with lia.
Qed.
Lemma dloc_eq_correct E dl1 dl2 :
  dbool_interp (dloc_eq E dl1 dl2) = bool_decide (dloc_interp E dl1 = dloc_interp E dl2).
Proof.
  unfold dloc_eq. destruct (dbase_loc_strong_eq _ _) eqn:H; last done.
  rewrite dint_eq_correct !dloc_interp_alt /=.
  apply (dbase_loc_strong_eq_correct E) in H as ->.
  apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.

Lemma dbin_op_eval_int_correct op di1 di2 :
  dbase_lit_interp (dbin_op_eval_int op di1 di2) =
  bin_op_eval_int op (dint_interp di1) (dint_interp di2).
Proof.
  destruct op; f_equal/=; auto using dint_plus_correct, dint_minus_correct,
    dint_eq_correct, dint_lt_correct, dint_le_correct.
Qed.

Lemma dbin_op_eval_bool_correct op db1 db2 dl :
  dbin_op_eval_bool op db1 db2 = Some dl 
  bin_op_eval_bool op (dbool_interp db1) (dbool_interp db2) = Some (dbase_lit_interp dl).
Proof.
  destruct op; intros; simplify_eq/=; do 2 f_equal/=;
    auto using dbool_and_correct, dbool_or_correct,
    dbool_xor_correct, dbool_eq_correct.
Qed.

Lemma dbase_lit_eq_correct dl1 dl2 :
  dbool_interp (dbase_lit_eq dl1 dl2) =
  bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2).
Proof.
  destruct dl1, dl2=> //=.
  - rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence.
  - rewrite dbool_eq_correct. apply bool_decide_iff. naive_solver congruence.
Qed.

Lemma dval_eq_correct E dv1 dv2 :
  dbool_interp (dval_eq E dv1 dv2) =
  bool_decide (dval_interp E dv1 = dval_interp E dv2).
Proof.
  revert dv1. induction dv2; intros []=> //=; try by rewrite cloc_to_val_eq.
  - rewrite dbase_lit_eq_correct. apply bool_decide_iff. naive_solver congruence.
  - rewrite dbool_and_correct. rewrite IHdv2_1 IHdv2_2.
    repeat case_bool_decide; intuition congruence.
  - rewrite dloc_eq_correct.
    apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.

Lemma dbin_op_eval_correct E op dv1 dv2 dw :
  dbin_op_eval E op dv1 dv2 = Some dw 
  bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw).
Proof.
  rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)); simplify_eq/=.
  { by rewrite dval_eq_correct. }
  destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq.
  - by rewrite dbin_op_eval_int_correct.
  - by erewrite dbin_op_eval_bool_correct by done.
Qed.

Lemma dcbin_op_eval_correct op E dv1 dv2 dw :
  dcbin_op_eval E op dv1 dv2 = Some dw 
  cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw).
Proof.
  rewrite /dcbin_op_eval; destruct op; intros; simplify_option_eq;
    repeat match goal with
    | H : dloc_of_dval _ = _ |- _ => apply dloc_of_dval_Some in H as ->
    | H : dint_of_dval _ = _ |- _ => apply dint_of_dval_Some in H as ->
    end; simpl.
  - by apply dbin_op_eval_correct.
  - by rewrite cloc_of_to_val /= dloc_plus_correct.
  - by rewrite !cloc_of_to_val /= dloc_lt_correct.
Qed.
652 653

Lemma dun_op_eval_correct E op dv w :
654
  dun_op_eval E op dv = Some w 
655 656
  un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
657 658 659
  intros; destruct op, dv as [[]| | | |]; simplify_eq/=.
  - by rewrite dbool_neg_correct.
  - by rewrite dint_opp_correct.
660 661
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
662 663 664 665 666 667 668
(** Well-formedness w.r.t. known_locs *)
Lemma dloc_var_wf_mono E E' i :
  dloc_var_wf E i  E `prefix_of` E'  dloc_var_wf E' i.
Proof.
  rewrite /dloc_var_wf !bool_decide_spec.
  intros [v ?] [E'' ->]. exists v; by apply lookup_app_l_Some.
Qed.
669

Robbert Krebbers's avatar
Robbert Krebbers committed
670 671 672
Lemma dbase_loc_wf_mono E E' dl :
  dbase_loc_wf E dl  E `prefix_of` E'  dbase_loc_wf E' dl.
Proof. destruct dl; simpl; eauto using dloc_var_wf_mono. Qed.
673

Robbert Krebbers's avatar
Robbert Krebbers committed
674 675 676
Lemma dloc_wf_mono E E' dl :
  dloc_wf E dl  E `prefix_of` E'  dloc_wf E' dl.
Proof. apply dbase_loc_wf_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
677

Robbert Krebbers's avatar
Robbert Krebbers committed
678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749
Lemma dval_wf_mono E E' dv :
  dval_wf E dv  E `prefix_of` E'  dval_wf E' dv.
Proof. induction dv; naive_solver eauto using dloc_wf_mono. Qed.

Lemma dexpr_wf_mono E E' de :
  dexpr_wf E de  E `prefix_of` E'  dexpr_wf E' de.
Proof. induction de; naive_solver eauto using dval_wf_mono. Qed.

Lemma dcexpr_wf_mono E E' de :
  dcexpr_wf E de  E `prefix_of` E'  dcexpr_wf E' de.
Proof. induction de; naive_solver eauto using dexpr_wf_mono. Qed.

Lemma dloc_of_dval_Some_wf E dv dl :
  dval_wf E dv  dloc_of_dval dv = Some dl  dloc_wf E dl.
Proof. destruct dv; naive_solver. Qed.

Lemma dloc_plus_wf E dl di : dloc_wf E dl  dloc_wf E (dloc_plus dl di).
Proof. by destruct dl. Qed.

Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
  dbin_op_eval E op dv1 dv2 = Some dw 
  dval_wf E dv1  dval_wf E dv2  dval_wf E dw.
Proof.
  rewrite /dbin_op_eval; intros; simplify_option_eq; auto.
  destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
Qed.

Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
  dcbin_op_eval E op dv1 dv2 = Some dw 
  dval_wf E dv1  dval_wf E dv2  dval_wf E dw.
Proof.
  rewrite /dcbin_op_eval. intros; destruct op; simplify_option_eq;
    eauto using dloc_plus_wf, dloc_of_dval_Some_wf, dbin_op_eval_Some_wf.
Qed.

Lemma dun_op_eval_Some_wf E dv op dw:
  dun_op_eval E op dv = Some dw  dval_wf E dv  dval_wf E dw.
Proof. destruct op, dv as [[]| | | |]; naive_solver. Qed.

Lemma dloc_var_interp_mono E E' dl :
  dloc_var_wf E dl  E `prefix_of` E' 
  dloc_var_interp E dl = dloc_var_interp E' dl.
Proof.
  rewrite /dloc_var_wf /dloc_var_interp !bool_decide_spec.
  intros [v ?] [E'' ->]. rewrite lookup_app_l; eauto using lookup_lt_is_Some_1.
Qed.

Lemma dbase_loc_interp_mono E E' dl :
  dbase_loc_wf E dl  E `prefix_of` E' 
  dbase_loc_interp E dl = dbase_loc_interp E' dl.
Proof. destruct dl; simpl; eauto using dloc_var_interp_mono. Qed.

Lemma dloc_interp_mono E E' dl :
  dloc_wf E dl  E `prefix_of` E' 
  dloc_interp E dl = dloc_interp E' dl.
Proof.
  rewrite !dloc_interp_alt=> ??. destruct dl as [dl i].
  f_equal. by apply dbase_loc_interp_mono.
Qed.

Lemma dval_interp_mono E E' dv :
  dval_wf E dv  E `prefix_of` E'  dval_interp E dv = dval_interp E' dv.
Proof. induction dv; naive_solver eauto using dloc_interp_mono with f_equal. Qed.

Lemma dexpr_interp_mono E E' de :
   dexpr_wf E de  E `prefix_of` E'  dexpr_interp E de = dexpr_interp E' de.
Proof. induction de; naive_solver eauto using dval_interp_mono with f_equal. Qed.

Lemma dcexpr_interp_mono E E' de :
  dcexpr_wf E de  E `prefix_of` E' 
  dcexpr_interp E de = dcexpr_interp E' de.
Proof. induction de; try naive_solver eauto 10 using dexpr_interp_mono with f_equal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
750

Dan Frumin's avatar
Dan Frumin committed
751
(** ** Substitution *)
Robbert Krebbers's avatar
Robbert Krebbers committed
752
Fixpoint de_subst (E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
Dan Frumin's avatar
Dan Frumin committed
753
  match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
754 755
  | dEVal dv => dEVal dv
  | dEVar y  => if decide (x = y) then dEVal dv else de
Dan Frumin's avatar
Dan Frumin committed
756 757 758
  | 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)
Robbert Krebbers's avatar
Robbert Krebbers committed
759 760
  | dENone => dENone
  | dEUnknown e => dEUnknown (subst x (dval_interp E dv) e)
Dan Frumin's avatar
Dan Frumin committed
761 762
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
763
Fixpoint dce_subst (E: known_locs) (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
Dan Frumin's avatar
Dan Frumin committed
764 765
  match dce with
  | dCRet de1 => dCRet (de_subst E x dv de1)
Robbert Krebbers's avatar
Robbert Krebbers committed
766 767 768 769
  | dCSeqBind y de1 de2 =>
    if decide (BNamed x = y)
    then dCSeqBind y (dce_subst E x dv de1) de2
    else dCSeqBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
770 771 772 773
  | dCMutBind y de1 de2 =>
    if decide (BNamed x = y)
    then dCMutBind y (dce_subst E x dv de1) de2
    else dCMutBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
Dan Frumin's avatar
Dan Frumin committed
774 775 776 777
  | 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 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
778
     dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
Dan Frumin's avatar
Dan Frumin committed
779
  | dCPreBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
780
     dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
Dan Frumin's avatar
Dan Frumin committed
781 782
  | dCUnOp op de1 =>  dCUnOp op (dce_subst E x dv de1)
  | dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
Robbert Krebbers's avatar
Robbert Krebbers committed
783 784 785 786
  | dCWhile de1 de2 => dCWhile (dce_subst E x dv de1) (dce_subst E x dv de2)
  | dCWhileV de1 de2 => dCWhileV de1 de2
  | dCCall v de1 => dCCall v (dce_subst E x dv de1)
  | dCUnknown e => dCUnknown (subst x (dval_interp E dv) e)
Dan Frumin's avatar
Dan Frumin committed
787 788
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
789 790 791 792 793 794
Definition dce_subst' (E: known_locs) (mx: binder) (dv : dval) (dce : dcexpr) : dcexpr :=
  match mx with BAnon => dce | BNamed x => dce_subst E x dv dce end.

Lemma dexpr_interp_subst 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 /=; repeat case_match; auto with f_equal. Qed.
Dan Frumin's avatar
Dan Frumin committed
795

Robbert Krebbers's avatar
Robbert Krebbers committed
796 797
Lemma dcexpr_interp_subst E x de dv :
  dcexpr_interp E (dce_subst E x dv de) = subst x (dval_interp E dv) (dcexpr_interp E de).
Dan Frumin's avatar
Dan Frumin committed
798
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
799
  induction de; repeat (simplify_eq /= || case_decide);
Robbert Krebbers's avatar
Robbert Krebbers committed
800
    naive_solver eauto 10 using dexpr_interp_subst with f_equal.
Dan Frumin's avatar
Dan Frumin committed
801 802
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
803 804 805
Lemma dcexpr_interp_subst' E mx de dv :
  dcexpr_interp E (dce_subst' E mx dv de) = subst' mx (dval_interp E dv) (dcexpr_interp E de).
Proof. destruct mx; simpl; auto using dcexpr_interp_subst. Qed.
Dan Frumin's avatar
Dan Frumin committed
806

807 808
Lemma de_subst_wf E x dv1 de2 :
  dval_wf E dv1  dexpr_wf E de2  dexpr_wf E (de_subst E x dv1 de2).
Dan Frumin's avatar
Dan Frumin committed
809
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
810
  induction de2; intros; repeat (simplify_eq /= || case_decide); naive_solver.
Dan Frumin's avatar
Dan Frumin committed
811 812
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
813 814
Lemma dce_subst_wf E x dv1 de2 :
  dval_wf E dv1  dcexpr_wf E de2  dcexpr_wf E (dce_subst E x dv1 de2).
Dan Frumin's avatar
Dan Frumin committed
815
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
816 817
  induction de2; intros; repeat (simplify_eq /= || case_decide);
    naive_solver auto using de_subst_wf.
Dan Frumin's avatar
Dan Frumin committed
818 819
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
820 821 822
Lemma dce_subst_wf' E mx dv1 de2 :
  dval_wf E dv1  dcexpr_wf E de2  dcexpr_wf E (dce_subst' E mx dv1 de2).
Proof. destruct mx; simpl; auto using dce_subst_wf. Qed.
823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843

Lemma de_subst_mono E E' x dv1 de2 :
  dval_wf E dv1  dexpr_wf E de2  E `prefix_of` E' 
  de_subst E x dv1 de2 = de_subst E' x dv1 de2.
Proof.
  induction de2; intros; repeat (simplify_eq /= || case_decide);
    naive_solver eauto using dval_interp_mono with f_equal.
Qed.

Lemma dce_subst_mono E E' x dv1 de2 :
  dval_wf E dv1  dcexpr_wf E de2  E `prefix_of` E' 
  dce_subst E x dv1 de2 = dce_subst E' x dv1 de2.
Proof.
  induction de2; intros; repeat (simplify_eq /= || case_decide);
    naive_solver eauto using de_subst_mono, dval_interp_mono with f_equal.
Qed.

Lemma dce_subst_mono' E E' mx dv1 de2 :
  dval_wf E dv1  dcexpr_wf E de2  E `prefix_of` E' 
  dce_subst' E mx dv1 de2 = dce_subst' E' mx dv1 de2.
Proof. destruct mx; simpl; auto using dce_subst_mono. Qed.