simple.v 15.7 KB
Newer Older
1 2
(** A simpler simulation relation that hides most of the physical state,
except for the call ID stack.
3 4 5
Useful whenever the resources we own are strong enough to carry us from step to step.

When your goal is simple, to make it stateful just do [intros σs σt].
6
To go the other direction, [apply sim_simplify NEW_POST]. Then you will likely
7 8 9
want to clean some stuff from your context.
*)

Ralf Jung's avatar
Ralf Jung committed
10
From stbor.sim Require Export body instance.
11
From stbor.sim Require Import refl_step right_step left_step viewshift.
12

13 14 15 16
Definition sim_simple fs ft r n es et
  (Φ : resUR  nat  result  result  Prop) : Prop :=
   σs σt, r { n , fs , ft } ( es , σs )  ( et , σt ) :
    (λ r n vs' σs' vt' σt', σs'.(scs) = σs.(scs)  σt'.(scs) = σt.(scs)  Φ r n vs' vt').
17

18 19
Notation "r ⊨ˢ{ n , fs , ft } es ≥ et : Φ" :=
  (sim_simple fs ft r n%nat es%E et%E Φ)
20
  (at level 70, es, et at next level,
21
   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' es ']'  '/' ≥  '/  ' '[ ' et ']'  '/' :  Φ ']'").
22

Ralf Jung's avatar
Ralf Jung committed
23
Section simple.
24
Implicit Types Φ: resUR  nat  result  result  Prop.
Ralf Jung's avatar
Ralf Jung committed
25

Ralf Jung's avatar
Ralf Jung committed
26 27
(* TODO: also allow rewriting the postcondition. *)
Global Instance sim_simple_proper fs ft :
28
  Proper (() ==> (=) ==> (=) ==> (=) ==> (=) ==> ())
Ralf Jung's avatar
Ralf Jung committed
29 30
    (sim_simple fs ft).
Proof.
31 32
  intros r1 r2 EQr n ? <- es ? <- et ? <- Φ ? <-.
  split; intros HH σs σt.
Ralf Jung's avatar
Ralf Jung committed
33 34 35 36 37
  - rewrite -EQr. exact: HH.
  - rewrite EQr. exact: HH.
Qed.
Global Instance: Params sim_simple 2.

38
Lemma sim_simplify
39
  (Φnew: resUR  nat  result  result  Prop)
40 41
  (Φ: resUR  nat  result  state  result  state  Prop)
  r n fs ft es σs et σt :
42 43 44 45 46 47 48
  ( r n vs σs' vt σt',
    σs'.(scs) = σs.(scs) 
    σt'.(scs) = σt.(scs) 
    Φnew r n vs vt 
    Φ r n vs σs' vt σt'
  ) 
  r ⊨ˢ{ n , fs , ft } es  et : Φnew 
49 50
  r { n , fs , ft } (es, σs)  (et, σt) : Φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
51
  intros HΦ HH. eapply sim_local_body_post_mono; last exact: HH.
52
  naive_solver.
53
Qed.
54
(*Lemma sim_simplify'
55 56 57 58 59 60 61 62 63 64
  (Φnew: resUR  nat  result  call_id_stack  result  call_id_stack  Prop)
  (Φ: resUR  nat  result  state  result  state  Prop)
  r n fs ft es σs et σt css cst :
  ( r n vs σs vt σt, Φnew r n vs σs.(scs) vt σt.(scs)  Φ r n vs σs vt σt) 
  σs.(scs) = css 
  σt.(scs) = cst 
  r ⊨ˢ{ n , fs , ft } (es, css)  (et, cst) : Φnew 
  r { n , fs , ft } (es, σs)  (et, σt) : Φ.
Proof.
  intros HΦ <-<-. eapply sim_simplify. done.
65
Qed.*)
66

67
Lemma sim_simple_frame_l Φ r rf n fs ft es et :
Ralf Jung's avatar
Ralf Jung committed
68
  r ⊨ˢ{ n , fs , ft }
69 70 71
    es  et
  : (λ r' n' es' et',  (rf  r')  Φ (rf  r') n' es' et') 
  rf  r ⊨ˢ{ n , fs , ft } es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
72
Proof.
73 74
  intros Hold σs σt. eapply sim_body_frame_l.
  eapply sim_local_body_post_mono, Hold. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
75 76
Qed.

77
Lemma sim_simple_frame_r Φ r rf n fs ft es et :
Ralf Jung's avatar
Ralf Jung committed
78
  r ⊨ˢ{ n , fs , ft }
79 80 81
    es  et
  : (λ r' n' es' et',  (r'  rf)  Φ (r'  rf) n' es' et') 
  r  rf ⊨ˢ{ n , fs , ft } es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
82
Proof.
83 84
  intros Hold σs σt. eapply sim_body_frame_r.
  eapply sim_local_body_post_mono, Hold. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
85 86
Qed.

87
Lemma sim_simple_frame_core Φ r n fs ft es et :
Ralf Jung's avatar
Ralf Jung committed
88
  r ⊨ˢ{ n , fs , ft }
89 90 91
    es  et
  : (λ r' n' es' et',  (core r  r')  Φ (core r  r') n' es' et') 
  r ⊨ˢ{ n , fs , ft } es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
92
Proof.
93 94
  intros Hold σs σt. eapply sim_body_frame_core.
  eapply sim_local_body_post_mono, Hold. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
95 96
Qed.

97
Lemma sim_simple_frame_more_core Φ r r' n fs ft es et :
Ralf Jung's avatar
Ralf Jung committed
98
  core r  r' ⊨ˢ{ n , fs , ft }
99 100 101
    es  et
  : (λ r'' n' es' et',  ((core r  core r')  r'')  Φ ((core r  core r')  r'') n' es' et') 
  core r  r' ⊨ˢ{ n , fs , ft } es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
102 103 104 105 106 107 108 109
Proof.
  intros HH. assert (core r  r'  (core r  core r')  (core r  r')) as ->.
  { rewrite {1}cmra_core_dup. rewrite - !assoc. f_equiv.
    rewrite [core r'  _]comm - !assoc. f_equiv.
    rewrite cmra_core_r //. }
  eapply sim_simple_frame_l, HH.
Qed.

110 111 112 113
Lemma sim_simple_post_mono Φ1 Φ2 r n fs ft es et :
  Φ1 <4= Φ2 
  r ⊨ˢ{ n , fs , ft } es  et : Φ1 
  r ⊨ˢ{ n , fs , ft } es  et : Φ2.
Ralf Jung's avatar
Ralf Jung committed
114
Proof.
115
  intros HΦ Hold σs σt. eapply sim_local_body_post_mono, Hold. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
116 117
Qed.

118 119 120
Lemma sim_simple_valid_pre fs ft r n es et Φ :
  (valid r  r ⊨ˢ{n,fs,ft} es  et : Φ) 
  r ⊨ˢ{n,fs,ft} es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
121
Proof.
122 123
  intros Hold σs σt. eapply sim_body_valid=>Hval.
  eapply sim_local_body_post_mono, Hold; naive_solver.
Ralf Jung's avatar
Ralf Jung committed
124 125
Qed.

126
Lemma sim_simple_valid_post fs ft r n es et Φ :
Ralf Jung's avatar
Ralf Jung committed
127
  (r ⊨ˢ{n,fs,ft}
128 129 130
    es  et
  : (λ r' n' es' et', valid r'  Φ r' n' es' et')) 
  r ⊨ˢ{n,fs,ft} es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
131
Proof.
132 133
  intros Hold σs σt. eapply sim_body_valid=>Hval.
  eapply sim_local_body_post_mono, Hold; naive_solver.
Ralf Jung's avatar
Ralf Jung committed
134 135
Qed.

136
Lemma sim_simple_viewshift r2 r1 fs ft n es et Φ :
Ralf Jung's avatar
Ralf Jung committed
137
  r1 |==> r2 
138 139
  r2 ⊨ˢ{n,fs,ft} es  et : Φ 
  r1 ⊨ˢ{n,fs,ft} es  et : Φ.
Ralf Jung's avatar
Ralf Jung committed
140
Proof.
141 142 143 144 145
  intros Hvs Hold σs σt. eapply viewshift_sim_local_body, Hold; naive_solver.
Qed.

(** * Simple proof for a function body. *)
Definition fun_post_simple c (r: resUR) (n: nat) vs vt :=
Hai Dang's avatar
Hai Dang committed
146
  res_cs c   r  rrel r vs vt.
147 148 149 150 151 152 153 154

Lemma sim_fun_simple n (esf etf: function) :
  length (esf.(fun_args)) = length (etf.(fun_args)) 
  ( fs ft rf es et vls vlt c,
    sim_local_funs_lookup fs ft 
    Forall2 (vrel rf) vls vlt 
    subst_l (esf.(fun_args)) (Val <$> vls) (esf.(fun_body)) = Some es 
    subst_l (etf.(fun_args)) (Val <$> vlt) (etf.(fun_body)) = Some et 
Hai Dang's avatar
Hai Dang committed
155
    rf  res_cs c  ⊨ˢ{n,fs,ft} es  et : fun_post_simple c) 
156 157 158 159 160 161 162 163 164 165
  ⊨ᶠ esf  etf.
Proof.
  intros Hl HH fs ft Hlook rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
  apply sim_body_init_call=>/= ?.
  eapply sim_body_valid=>Hval.
  eapply sim_simplify; last exact: HH.
  move=>/= r ? vs' σs' vt' σt' ?? [??].
  split; last done.
  eexists. split; first done.
  eapply res_end_call_sat; done.
Ralf Jung's avatar
Ralf Jung committed
166 167
Qed.

Ralf Jung's avatar
Ralf Jung committed
168
Lemma sim_fun_simple1 n (esf etf: function) :
Ralf Jung's avatar
Ralf Jung committed
169 170
  length (esf.(fun_args)) = 1%nat 
  length (etf.(fun_args)) = 1%nat 
171
  ( fs ft rf es et vs vt c,
Ralf Jung's avatar
Ralf Jung committed
172
    sim_local_funs_lookup fs ft 
173
    vrel rf vs vt 
Ralf Jung's avatar
Ralf Jung committed
174 175
    subst_l (esf.(fun_args)) [Val vs] (esf.(fun_body)) = Some es 
    subst_l (etf.(fun_args)) [Val vt] (etf.(fun_body)) = Some et 
Hai Dang's avatar
Hai Dang committed
176
    rf  res_cs c  ⊨ˢ{n,fs,ft} es  et : fun_post_simple c) 
Ralf Jung's avatar
Ralf Jung committed
177
  ⊨ᶠ esf  etf.
178
Proof.
179 180 181
  intros Hls Hlt HH. eapply sim_fun_simple.
  { rewrite Hls Hlt //. }
  intros ?? rf ?? vls vlt c ? FREL SUBSTs SUBSTt.
182
  move:(subst_l_is_Some_length _ _ _ _ SUBSTs) (subst_l_is_Some_length _ _ _ _ SUBSTt).
183
  rewrite Hls Hlt=>??.
184 185
  destruct vls as [|vs []]; [done| |done].
  destruct vlt as [|vt []]; [done| |done].
186
  inversion FREL as [|???? RREL]. eapply HH; done.
187
Qed.
188

Ralf Jung's avatar
Ralf Jung committed
189
Lemma sim_simple_bind fs ft
Ralf Jung's avatar
Ralf Jung committed
190 191
  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
192 193 194 195 196
  r n Φ :
  r ⊨ˢ{n,fs,ft} es  et
    : (λ r' n' es' et',
        r' ⊨ˢ{n',fs,ft} fill Ks es'  fill Kt et' : Φ) 
  r ⊨ˢ{n,fs,ft} fill Ks es  fill Kt et : Φ.
Ralf Jung's avatar
Ralf Jung committed
197
Proof.
198
  intros HH σs σt. apply sim_body_bind.
Ralf Jung's avatar
Ralf Jung committed
199
  eapply sim_local_body_post_mono; last exact: HH.
200
  clear. simpl. intros r n vs σs' vt σ't [<- [<- HH]]. exact: HH.
Ralf Jung's avatar
Ralf Jung committed
201 202
Qed.

203 204 205
Lemma sim_simple_bind_call r n fs ft es et (fns fnt: result) (pres pret: list result) posts postt Φ :
  r ⊨ˢ{n,fs,ft} es  et
    : (λ r' n' rs' rt',
Ralf Jung's avatar
Ralf Jung committed
206
        r' ⊨ˢ{n',fs,ft}
207
          Call fns ((of_result <$> pres) ++ (of_result rs') :: posts)
Ralf Jung's avatar
Ralf Jung committed
208
        
209
          Call fnt ((of_result <$> pret) ++ (of_result rt') :: postt)
Ralf Jung's avatar
Ralf Jung committed
210 211
        : Φ) 
  r ⊨ˢ{n,fs,ft}
212
    Call fns ((of_result <$> pres) ++ es :: posts)
Ralf Jung's avatar
Ralf Jung committed
213
  
214
    Call fnt ((of_result <$> pret) ++ et :: postt)
Ralf Jung's avatar
Ralf Jung committed
215 216
  : Φ.
Proof.
217
  intros HH σs σt. apply sim_body_bind_call.
Ralf Jung's avatar
Ralf Jung committed
218
  eapply sim_local_body_post_mono; last exact: HH.
219
  clear. simpl. intros r n vs σs' vt σt' [<- [<- HH]]. exact: HH.
Ralf Jung's avatar
Ralf Jung committed
220 221
Qed.

222
Lemma sim_simple_result fs ft r n (vs vt: result) es et Φ :
Ralf Jung's avatar
Ralf Jung committed
223
  IntoResult es vs  IntoResult et vt 
224 225
  Φ r n vs vt 
  r ⊨ˢ{n,fs,ft} es  et : Φ.
226
Proof.
227
  intros ?? HH σs σt. eapply sim_body_result; done.
228 229
Qed.

230
(** * Calls *)
Ralf Jung's avatar
Ralf Jung committed
231 232
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
233
Lemma sim_simple_call n' rls rlt rv fs ft r r' n fe (fi: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
234
  IntoResult fe fi 
235
  sim_local_funs_lookup fs ft 
Ralf Jung's avatar
Ralf Jung committed
236
  r  r'  rv 
Ralf Jung's avatar
Ralf Jung committed
237
  Forall2 (rrel rv) rls rlt 
Hai Dang's avatar
Hai Dang committed
238
  ( rret vs vt vls vlt fid,
Ralf Jung's avatar
Ralf Jung committed
239
    fi = ValR [ScFnPtr fid] 
240 241
    rls = ValR <$> vls  rlt = ValR <$> vlt 
    vrel rret vs vt 
242
    r'  rret ⊨ˢ{n',fs,ft} Val vs  Val vt : Φ) 
Ralf Jung's avatar
Ralf Jung committed
243
  r ⊨ˢ{n,fs,ft}
244
    Call fe (of_result <$> rls)  Call fe (of_result <$> rlt) : Φ.
Ralf Jung's avatar
Ralf Jung committed
245
Proof.
246
  intros <- Hfns Hres Hrel HH σs σt. rewrite Hres.
Ralf Jung's avatar
Ralf Jung committed
247
  apply: sim_body_step_over_call.
Ralf Jung's avatar
Ralf Jung committed
248
  - done.
Hai Dang's avatar
Hai Dang committed
249
  - done.
250 251
  - intros. exists n'. eapply sim_body_res_proper; last exact: HH; try done.
    rewrite STACKS STACKT. done.
Hai Dang's avatar
Hai Dang committed
252
Qed.
Ralf Jung's avatar
Ralf Jung committed
253

254
(** * Memory: local *)
255
Lemma sim_simple_alloc_local fs ft r n T Φ :
256
  ( (l: loc) (tg: nat),
Hai Dang's avatar
Hai Dang committed
257
    let r' := res_loc l (repeat (%S,%S) (tsize T)) tg in
258 259
    Φ (r  r') n (PlaceR l (Tagged tg) T) (PlaceR l (Tagged tg) T)) 
  r ⊨ˢ{n,fs,ft} Alloc T  Alloc T : Φ.
260
Proof.
261
  intros HH σs σt. apply sim_body_alloc_local; eauto.
262 263
Qed.

Hai Dang's avatar
Hai Dang committed
264 265 266 267 268 269 270 271 272
Lemma sim_simple_free_local_1 fs ft r r' n l tg ty v Φ :
  tsize ty = 1%nat 
  r  r'  res_loc l [v] tg 
  Φ r' n (ValR [%S]) (ValR [%S]) 
  r ⊨ˢ{n,fs,ft} Free (Place l (Tagged tg) ty)  Free (Place l (Tagged tg) ty) : Φ.
Proof.
  intros Hty Hres HH σs σt. eapply sim_body_free_unique_local_1; eauto.
Qed.

Hai Dang's avatar
Hai Dang committed
273
Lemma sim_simple_write_local fs ft r r' n l tg ty v v' Φ :
Ralf Jung's avatar
Ralf Jung committed
274
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
275
  r  r'  res_loc l [v'] tg 
Hai Dang's avatar
Hai Dang committed
276
  ( s, v = [s]  Φ (r'  res_loc l [(s,s)] tg) n (ValR [%S]) (ValR [%S])) 
277
  r ⊨ˢ{n,fs,ft}
Hai Dang's avatar
Hai Dang committed
278
    (Place l (Tagged tg) ty <- #v)  (Place l (Tagged tg) ty <- #v)
279
  : Φ.
280
Proof. intros Hty Hres HH σs σt. eapply sim_body_write_local_1; eauto. Qed.
281

Hai Dang's avatar
Hai Dang committed
282
Lemma sim_simple_copy_local_l fs ft r r' n l tg ty ss st et Φ :
283
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
284 285
  r  r'  res_loc l [(ss, st)] tg 
  (r ⊨ˢ{n,fs,ft} #[ss]  et : Φ) 
286
  r ⊨ˢ{n,fs,ft}
287
    Copy (Place l (Tagged tg) ty)  et
288 289
  : Φ.
Proof.
290
  intros ?? Hold σs σt.
Ralf Jung's avatar
Ralf Jung committed
291 292
  eapply sim_body_copy_local_l; eauto.
Qed.
293

Hai Dang's avatar
Hai Dang committed
294
Lemma sim_simple_copy_local_r fs ft r r' n l tg ty ss st es Φ :
295
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
296 297
  r  r'  res_loc l [(ss,st)] tg 
  (r ⊨ˢ{n,fs,ft} es  #[st] : Φ) 
Ralf Jung's avatar
Ralf Jung committed
298
  r ⊨ˢ{S n,fs,ft}
299
    es  Copy (Place l (Tagged tg) ty)
300 301
  : Φ.
Proof.
302
  intros ?? Hold σs σt.
Ralf Jung's avatar
Ralf Jung committed
303 304 305
  eapply sim_body_copy_local_r; eauto.
Qed.

Hai Dang's avatar
Hai Dang committed
306
Lemma sim_simple_copy_local fs ft r r' n l tg ty ss st Φ :
Ralf Jung's avatar
Ralf Jung committed
307
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
308 309
  r  r'  res_loc l [(ss,st)] tg 
  (r ⊨ˢ{n,fs,ft} #[ss]  #[st] : Φ) 
Ralf Jung's avatar
Ralf Jung committed
310
  r ⊨ˢ{S n,fs,ft}
311
    Copy (Place l (Tagged tg) ty)  Copy (Place l (Tagged tg) ty)
Ralf Jung's avatar
Ralf Jung committed
312 313 314 315 316 317
  : Φ.
Proof.
  intros ?? Hcont.
  eapply sim_simple_copy_local_l; [done..|].
  eapply sim_simple_copy_local_r; done.
Qed.
318

319
Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty Φ :
Hai Dang's avatar
Hai Dang committed
320
  (0 < tsize ty)%nat 
Hai Dang's avatar
Hai Dang committed
321
  r  r'  res_loc l [(s,s)] tg 
Ralf Jung's avatar
Ralf Jung committed
322 323
  arel rs s' s 
  r'  r''  rs 
Ralf Jung's avatar
Ralf Jung committed
324
  ( l_inner tg_inner hplt,
Ralf Jung's avatar
Ralf Jung committed
325
    let s_new := ScPtr l_inner (Tagged tg_inner) in
326
(*    let tk := match m with Mutable => tkUnique | Immutable => tkPub end in
Hai Dang's avatar
Hai Dang committed
327
    match m with
Ralf Jung's avatar
Ralf Jung committed
328 329
    | Mutable => is_Some (hplt !! l_inner)
    | Immutable => if is_freeze ty then is_Some (hplt !! l_inner) else True
330 331 332
    end  *)
    let tk := tkUnique in
    is_Some (hplt !! l_inner) 
Hai Dang's avatar
Hai Dang committed
333
    Φ (r''  rs  res_loc l [(s_new,s_new)] tg  res_tag tg_inner tk hplt) n (ValR [%S]) (ValR [%S])) 
Ralf Jung's avatar
Ralf Jung committed
334
  r ⊨ˢ{n,fs,ft}
335
    Retag (Place l (Tagged tg) (Reference (RefPtr Mutable) ty)) Default
Ralf Jung's avatar
Ralf Jung committed
336
  
337
    Retag (Place l (Tagged tg) (Reference (RefPtr Mutable) ty)) Default
Ralf Jung's avatar
Ralf Jung committed
338 339
  : Φ.
Proof.
340
  intros ???? HH σs σt. eapply sim_body_retag_local_mut_ref; eauto.
Hai Dang's avatar
Hai Dang committed
341
Qed.
Ralf Jung's avatar
Ralf Jung committed
342

343
(** * Memory: shared *)
344
Lemma sim_simple_alloc_public fs ft r n T Φ :
345 346
  ( (l: loc) (tg: nat),
    let rt := res_tag tg tkPub  in
347 348
    Φ (r  rt) n (PlaceR l (Tagged tg) T) (PlaceR l (Tagged tg) T)) 
  r ⊨ˢ{n,fs,ft} Alloc T  Alloc T : Φ.
349
Proof.
350
  intros HH σs σt. apply sim_body_alloc_public=>/=; eauto.
Hai Dang's avatar
Hai Dang committed
351
Qed.
352

Hai Dang's avatar
Hai Dang committed
353
Lemma sim_simple_free_public fs ft r es rs et rt n Φ :
Ralf Jung's avatar
Ralf Jung committed
354
  IntoResult es rs  IntoResult et rt 
Hai Dang's avatar
Hai Dang committed
355 356
  rrel r rs rt 
  Φ r n (ValR [%S]) (ValR [%S]) 
Ralf Jung's avatar
Ralf Jung committed
357
  r ⊨ˢ{n,fs,ft} Free es  Free et : Φ.
Hai Dang's avatar
Hai Dang committed
358
Proof.
Hai Dang's avatar
Hai Dang committed
359
  intros <- <- [Hrel <-]%rrel_with_eq HH σs σt. eapply sim_body_free_public; eauto.
Hai Dang's avatar
Hai Dang committed
360 361
Qed.

362
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) Φ :
363 364
  rrel r rs1 rt1 
  rrel r rs2 rt2 
365 366
  Φ r n (ValR [%S]) (ValR [%S]) 
  r ⊨ˢ{n,fs,ft} (rs1 <- rs2)  (rt1 <- rt2) : Φ.
367 368
Proof.
  intros [Hrel1 ?]%rrel_with_eq [Hrel2 ?]%rrel_with_eq. simplify_eq.
369
  intros HH σs σt. eapply sim_body_write_public; eauto.
Hai Dang's avatar
Hai Dang committed
370
Qed.
371

372
Lemma sim_simple_copy_public fs ft r n (rs rt: result) Φ :
373
  rrel r rs rt 
Hai Dang's avatar
Hai Dang committed
374 375 376
  ( r' (v1 v2: value),
    (* this post-condition is weak, we can return related values *)
    vrel r' v1 v2 
377 378
    Φ (r  r') n v1 v2) 
  r ⊨ˢ{n,fs,ft} Copy rs  Copy rt : Φ.
379
Proof.
380
  intros [Hrel <-]%rrel_with_eq HH σs σt.
Hai Dang's avatar
Hai Dang committed
381 382
  eapply sim_body_copy_public; eauto.
Qed.
383

384
Lemma sim_simple_retag_public fs ft r n (rs rt: result) k Φ :
385
  rrel r rs rt 
386 387
  (Φ r n (ValR [%S]) (ValR [%S])) 
  r ⊨ˢ{n,fs,ft} Retag rs k  Retag rt k : Φ.
388 389
Proof.
  intros [Hrel ?]%rrel_with_eq. simplify_eq.
Ralf Jung's avatar
Ralf Jung committed
390
Admitted.
391

Ralf Jung's avatar
Ralf Jung committed
392
(** * Pure *)
393
Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ :
Ralf Jung's avatar
Ralf Jung committed
394
  IntoResult es1 vs1  IntoResult et1 vt1 
395 396 397
  r ⊨ˢ{n,fs,ft} (subst' x es1 es2)  (subst' x et1 et2) : Φ 
  r ⊨ˢ{n,fs,ft} (let: x := es1 in es2)  (let: x := et1 in et2) : Φ.
Proof. intros ?? HH σs σt. apply: sim_body_let. eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
398

399
Lemma sim_simple_ref fs ft r n (pl: result) Φ :
Hai Dang's avatar
Hai Dang committed
400
  ( l t T, pl = PlaceR l t T 
401 402 403
    Φ r n (ValR [ScPtr l t]) (ValR [ScPtr l t])) 
  r ⊨ˢ{n,fs,ft} (& pl)  (& pl) : Φ.
Proof. intros HH σs σt. apply sim_body_ref; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
404

405
Lemma sim_simple_deref fs ft r n ef (rf: result) T Φ :
Ralf Jung's avatar
Ralf Jung committed
406
  IntoResult ef rf 
Hai Dang's avatar
Hai Dang committed
407
  ( l t, rf = ValR [ScPtr l t] 
408 409 410
    Φ r n (PlaceR l t T) (PlaceR l t T)) 
  r ⊨ˢ{n,fs,ft} Deref ef T  Deref ef T : Φ.
Proof. intros <- HH σs σt. apply sim_body_deref; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
411

412 413 414
Lemma sim_simple_var fs ft r n var Φ :
  r ⊨ˢ{n,fs,ft} Var var  Var var : Φ.
Proof. intros σs σt. apply sim_body_var; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
415

416
Lemma sim_simple_proj fs ft r n (v i: expr) (vr ir: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
417
  IntoResult v vr  IntoResult i ir 
Ralf Jung's avatar
Ralf Jung committed
418
  ( vi vv iv, vr = ValR vv  ir = ValR [ScInt iv] 
Ralf Jung's avatar
Ralf Jung committed
419
    vv !! (Z.to_nat iv) = Some vi  0  iv 
420 421
    Φ r n (ValR [vi]) (ValR [vi])) 
  r ⊨ˢ{n,fs,ft} Proj vr ir  Proj vr ir : Φ.
Ralf Jung's avatar
Ralf Jung committed
422
Proof.
423
  intros ?? HH σs σt. apply sim_body_proj; eauto.
Ralf Jung's avatar
Ralf Jung committed
424
Qed.
Ralf Jung's avatar
Ralf Jung committed
425

426
Lemma sim_simple_conc fs ft r n (r1 r2: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
427
  ( v1 v2, r1 = ValR v1  r2 = ValR v2 
428 429 430
    Φ r n (ValR (v1 ++ v2)) (ValR (v1 ++ v2))) 
  r ⊨ˢ{n,fs,ft} Conc r1 r2  Conc r1 r2 : Φ.
Proof. intros HH σs σt. apply sim_body_conc; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
431

432
Lemma sim_simple_bin_op fs ft r n op (r1 r2: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
433 434
  ( s1 s2 s mem, r1 = ValR [s1]  r2 = ValR [s2] 
    bin_op_eval mem op s1 s2 s 
435 436 437
    Φ r n (ValR [s]) (ValR [s])) 
  r ⊨ˢ{n,fs,ft} BinOp op r1 r2  BinOp op r1 r2 : Φ.
Proof. intros HH σs σt. apply sim_body_bin_op; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
438

439
Lemma sim_simple_case fs ft r n (rc: result) els elt Φ :
Ralf Jung's avatar
Ralf Jung committed
440 441 442 443 444
  length els = length elt 
  ( (es et: expr) (i: Z), 0  i 
    els !! (Z.to_nat i) = Some es 
    elt !! (Z.to_nat i) = Some et 
    rc = ValR [ScInt i] 
445 446
    r ⊨ˢ{n,fs,ft} es  et : Φ) 
  r ⊨ˢ{n,fs,ft} Case rc els  Case rc elt : Φ.
Ralf Jung's avatar
Ralf Jung committed
447
Proof.
448
  intros ? HH σs σt. apply sim_body_case; first done.
Ralf Jung's avatar
Ralf Jung committed
449 450 451
  intros. eapply HH; eauto.
Qed.

452
End simple.