simple.v 15.8 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 
Ralf Jung's avatar
Ralf Jung committed
171
  ( fs ft rf es et v c,
Ralf Jung's avatar
Ralf Jung committed
172
    sim_local_funs_lookup fs ft 
Ralf Jung's avatar
Ralf Jung committed
173 174 175
    vrel rf v v 
    subst_l (esf.(fun_args)) [Val v] (esf.(fun_body)) = Some es 
    subst_l (etf.(fun_args)) [Val v] (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].
Ralf Jung's avatar
Ralf Jung committed
186 187
  inversion FREL as [|???? RREL]. specialize (vrel_eq _ _ _ RREL)=>?.
  simplify_eq. eapply HH; done.
188
Qed.
189

Ralf Jung's avatar
Ralf Jung committed
190
Lemma sim_simple_bind fs ft
Ralf Jung's avatar
Ralf Jung committed
191 192
  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
193 194 195 196 197
  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
198
Proof.
199
  intros HH σs σt. apply sim_body_bind.
Ralf Jung's avatar
Ralf Jung committed
200
  eapply sim_local_body_post_mono; last exact: HH.
201
  clear. simpl. intros r n vs σs' vt σ't [<- [<- HH]]. exact: HH.
Ralf Jung's avatar
Ralf Jung committed
202 203
Qed.

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

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

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

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

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

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

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

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

Hai Dang's avatar
Hai Dang committed
320
Lemma sim_simple_retag_ref fs ft r n (ptr: scalar) m ty Φ :
Hai Dang's avatar
Hai Dang committed
321
  (0 < tsize ty)%nat 
Hai Dang's avatar
Hai Dang committed
322
  (if m is Immutable then is_freeze ty else True) 
Hai Dang's avatar
Hai Dang committed
323
  arel r ptr ptr 
Hai Dang's avatar
Hai Dang committed
324 325 326
  ( l told tnew hplt,
    ptr = ScPtr l told 
    let s_new := ScPtr l (Tagged tnew) in
Hai Dang's avatar
Hai Dang committed
327
    let tk := match m with Mutable => tkUnique | Immutable => tkPub end in
Hai Dang's avatar
Hai Dang committed
328
    let s_new := ScPtr l (Tagged tnew) in
Hai Dang's avatar
Hai Dang committed
329
    ( i: nat, (i < tsize ty)%nat  is_Some $ hplt !! (l + i)) 
Hai Dang's avatar
Hai Dang committed
330
    Φ (r  res_tag tnew tk hplt) n (ValR [s_new]) (ValR [s_new])) 
Ralf Jung's avatar
Ralf Jung committed
331
  r ⊨ˢ{n,fs,ft}
Hai Dang's avatar
Hai Dang committed
332
    Retag #[ptr] (RefPtr m) ty Default
Ralf Jung's avatar
Ralf Jung committed
333
  
Hai Dang's avatar
Hai Dang committed
334
    Retag #[ptr] (RefPtr m) ty Default
Ralf Jung's avatar
Ralf Jung committed
335 336
  : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
337 338
  intros ??? HH σs σt.
  apply sim_body_retag_ref_default; eauto.
Hai Dang's avatar
Hai Dang committed
339 340 341
  intros ??????????? HS. do 2 (split; [done|]). eapply HH; eauto.
  intros ??. by apply HS.
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

Hai Dang's avatar
Hai Dang committed
384
Lemma sim_simple_retag_public fs ft r n (rs rt: result) pk T rk Φ :
385
  rrel r rs rt 
Hai Dang's avatar
Hai Dang committed
386 387 388
  ( l old new rt, rs = ValR [ScPtr l old] 
    vrel (r  rt) [ScPtr l new] [ScPtr l new] 
    Φ (r  rt) n (ValR [ScPtr l new]) (ValR [ScPtr l new])) 
Hai Dang's avatar
Hai Dang committed
389
  r ⊨ˢ{n,fs,ft} Retag rs pk T rk  Retag rt pk T rk : Φ.
390
Proof.
Hai Dang's avatar
Hai Dang committed
391 392 393
  intros [Hrel ?]%rrel_with_eq HH σs σt. simplify_eq.
  eapply sim_body_retag_public; eauto.
Qed.
394

Ralf Jung's avatar
Ralf Jung committed
395
(** * Pure *)
396
Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ :
Ralf Jung's avatar
Ralf Jung committed
397
  IntoResult es1 vs1  IntoResult et1 vt1 
398 399 400
  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
401

402
Lemma sim_simple_ref fs ft r n (pl: result) Φ :
Hai Dang's avatar
Hai Dang committed
403
  ( l t T, pl = PlaceR l t T 
404 405 406
    Φ 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
407

408
Lemma sim_simple_deref fs ft r n ef (rf: result) T Φ :
Ralf Jung's avatar
Ralf Jung committed
409
  IntoResult ef rf 
Hai Dang's avatar
Hai Dang committed
410
  ( l t, rf = ValR [ScPtr l t] 
411 412 413
    Φ 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
414

415 416 417
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
418

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

429
Lemma sim_simple_conc fs ft r n (r1 r2: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
430
  ( v1 v2, r1 = ValR v1  r2 = ValR v2 
431 432 433
    Φ 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
434

435
Lemma sim_simple_bin_op fs ft r n op (r1 r2: result) Φ :
Ralf Jung's avatar
Ralf Jung committed
436 437
  ( s1 s2 s mem, r1 = ValR [s1]  r2 = ValR [s2] 
    bin_op_eval mem op s1 s2 s 
438 439 440
    Φ 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
441

442
Lemma sim_simple_case fs ft r n (rc: result) els elt Φ :
Ralf Jung's avatar
Ralf Jung committed
443 444 445 446 447
  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] 
448 449
    r ⊨ˢ{n,fs,ft} es  et : Φ) 
  r ⊨ˢ{n,fs,ft} Case rc els  Case rc elt : Φ.
Ralf Jung's avatar
Ralf Jung committed
450
Proof.
451
  intros ? HH σs σt. apply sim_body_case; first done.
Ralf Jung's avatar
Ralf Jung committed
452 453 454
  intros. eapply HH; eauto.
Qed.

455
End simple.