relational_properties.v 29.4 KB
Newer Older
1 2 3 4 5 6 7
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import rules_binary tactics.
From iris.program_logic Require Import ectx_lifting.

(** * Properties of the relational interpretation *)
Section properties.
8
  Context `{logrelG Σ}.
9 10 11 12 13 14 15 16 17 18 19 20 21
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types e : expr.
  Implicit Types Δ : listC D.
  Hint Resolve to_of_val.

  (** * Lemmas to show that binary logical model is closed under
  (forward) reductions. *)

  (* We need this to be able to open and closed invariants in front of logrels *)
  Lemma fupd_logrel Γ E1 E2 e e' τ :
    ((|={E1,E2}=> ({E2,E2;Γ}  e log e' : τ))
     - {E1,E2;Γ}  e log e' : τ)%I.
  Proof.
22
    rewrite bin_log_related_eq.
23 24 25
    iIntros "H".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iMod "H".
26
    iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
27 28
  Qed.

29 30 31 32 33 34 35 36 37 38 39 40
  (* TODO: should there be a corresponding =ElimModal= instance? *)
  Lemma fupd_logrel' Γ E1 E2 e e' τ :
    ((|={E1}=> ({E1,E2;Γ}  e log e' : τ))
     - {E1,E2;Γ}  e log e' : τ)%I.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "H".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iMod "H".
    iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
  Qed.

41 42 43
  Global Instance elim_modal_logrel E1 E2 Γ e e' P τ :
   ElimModal (|={E1,E2}=> P) P
     ({E1,E2;Γ}  e log e' : τ) ({E2,E2;Γ}  e log e' : τ) | 0.
44
  Proof.
45 46 47 48
    iIntros "[HP HI]". iApply fupd_logrel.
    iMod "HP". iApply ("HI" with "HP").
  Qed.
  
49
  Lemma bin_log_related_val Γ E τ e e' v v' :
50 51
    to_val e = Some v 
    to_val e' = Some v' 
52
    ( Δ, |={E}=> interp   τ Δ (v, v'))  {E,E;Γ}  e log e' : τ.
53
  Proof.
54
    rewrite bin_log_related_eq.
55 56
    iIntros (Hv Hv') "IH".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
57 58 59
    replace e with (of_val v); auto using of_to_val.
    replace e' with (of_val v'); auto using of_to_val.    
    rewrite /env_subst !Closed_subst_p_id.
60
    iMod ("IH" $! Δ) as "IH".
61 62 63 64
    iModIntro. iApply wp_value; eauto.
  Qed.

  (** ** Reductions on the left *)
65 66 67
  (** *** Lifting of the pure reductions *)
  Lemma bin_log_pure_l (Γ : stringmap type) (E : coPset) 
    (K' : list ectx_item) (e e' t : expr) (τ : type)
68 69
    (Hclosed : Closed  e)
    (Hclosed' : Closed  e')
70 71
    (Hsafe :  σ, head_reducible e σ) :
    ( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) 
72 73
     ({E,E;Γ}  fill K' e' log t : τ)
     {E,E;Γ}  fill K' e log t : τ.
74
  Proof.
75
    rewrite bin_log_related_eq.
76 77 78 79
    assert (to_val e = None) as Hval.
    { destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
      by eapply val_stuck. }
    iIntros (Hstep) "IH".
80
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
81 82 83 84
    rewrite /env_subst.
    rewrite fill_subst. iModIntro.
    iApply (wp_bind (subst_ctx (fst <$> vvs) K')).
    rewrite Closed_subst_p_id.
85
    iApply wp_lift_pure_det_head_step_no_fork'; eauto. iNext.
86 87 88 89 90 91 92 93
    iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
    rewrite /env_subst fill_subst.
    rewrite Closed_subst_p_id.
    iApply wp_bind_inv. 
    { (* TODO: how to get rid of this? *)
      change lang with (ectx_lang expr). 
      change fill with (ectx_language.fill).
      eapply ectx_lang_ctx. }
94
    iApply fupd_wp. by iApply (fupd_mask_mono E).
95
  Qed.
96

97 98
  Lemma bin_log_pure_masked_l (Γ : stringmap type) (E1 E2 : coPset)
    (K' : list ectx_item) (e e' t : expr) (τ : type)
99 100
    (Hclosed : Closed  e)
    (Hclosed' : Closed  e')
101 102 103 104 105
    (Hsafe :  σ, head_reducible e σ) :
    ( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) 
    {E1,E2;Γ}  fill K' e' log t : τ
     {E1,E2;Γ}  fill K' e log t : τ.
  Proof.
106
    rewrite bin_log_related_eq.
107 108 109 110
    assert (to_val e = None) as Hval.
    { destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
      by eapply val_stuck. }
    iIntros (Hstep) "IH".
111
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
112 113 114 115
    rewrite /env_subst fill_subst. 
    rewrite Closed_subst_p_id.
    iApply (wp_bind (subst_ctx _ K')). 
    iMod ("IH" with "Hs [HΓ] Hj") as "IH"; auto. 
116
    iModIntro.    
117 118 119 120 121 122 123 124 125 126
    iApply wp_lift_pure_det_head_step_no_fork; eauto. iModIntro.
    iNext.
    rewrite /env_subst fill_subst /=. 
    rewrite Closed_subst_p_id.
    iApply wp_bind_inv. 
    { (* TODO: how to get rid of this? *)
      change lang with (ectx_lang expr). 
      change fill with (ectx_language.fill).
      eapply ectx_lang_ctx. }
    done.
127 128
  Qed.
 
129 130 131
  Lemma bin_log_related_fst_l Γ E K v1 v2 e τ :
    ({E,E;Γ}  (fill K (of_val v1)) log e : τ)
    {E,E;Γ}  (fill K (Fst (Pair (of_val v1) (of_val v2)))) log e : τ.
132 133 134 135 136 137 138
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - by inversion H1.
  Qed.

139 140 141
  Lemma bin_log_related_snd_l Γ E K v1 v2 e τ :
    ({E,E;Γ}  (fill K (of_val v2)) log e : τ)
    {E,E;Γ}  (fill K (Snd (Pair (of_val v1) (of_val v2)))) log e : τ.
142 143 144 145 146 147 148
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - by inversion H1.
  Qed.

149
  Lemma bin_log_related_rec_l Γ E K (f x : binder) e e' v t τ
150
   (Hclosed : Closed (x :b: f :b: ) e) :
151
   (to_val e' = Some v) 
152 153
    ({E,E;Γ}  (fill K (subst' f (Rec f x e) (subst' x e' e))) log t : τ)
    {E,E;Γ}  (fill K (App (Rec f x e) e')) log t : τ.
154 155 156
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
157 158 159 160 161 162 163 164 165
    - rewrite /Closed; cbn.
      split_and?; eauto. rewrite -(of_to_val e' v); auto.
      by apply of_val_closed.
    - replace (rec: f x := e)%E with (of_val (rec: f x := e)%V) by (unlock; done).
      replace e' with (of_val v) by (by rewrite (of_to_val e' v)).
      rewrite -subst_p_rec /=.
      eapply subst_p_closes; eauto.
      destruct f, x; cbn-[union]; rewrite ?dom_insert ?dom_singleton ?dom_empty;
        set_solver. (* TODO: kinda slow, dom_insert_binder *)
166 167 168 169 170 171
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

172
  Lemma bin_log_related_tlam_l Γ E K e t τ
173
   (Hclosed : Closed  e) :
174 175
    ({E,E;Γ}  fill K e log t : τ)
    {E,E;Γ}  (fill K (TApp (TLam e))) log t : τ.
176 177 178 179 180 181 182 183 184
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

185
  Lemma bin_log_related_fold_l Γ E K e v t τ :
186
   (to_val e = Some v) 
187 188
    ({E,E;Γ}  fill K e log t : τ)
    {E,E;Γ}  (fill K (Unfold (Fold e))) log t : τ.
189 190 191 192 193 194 195 196 197
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.
  
198
  Lemma bin_log_related_pack_l Γ E K e e' v t τ
199
   (Hclosed' : Closed  e') :
200
   (to_val e = Some v) 
201 202
    ({E,E;Γ}  fill K (App e' e) log t : τ)
    {E,E;Γ}  (fill K (Unpack (Pack e) e')) log t : τ.
203 204 205 206 207 208 209 210 211
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

212
  Lemma bin_log_related_case_inl_l Γ E K e v e1 e2 t τ
213 214
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
215
   (to_val e = Some v) 
216 217
    ({E,E;Γ}  fill K (App e1 e) log t : τ)
    {E,E;Γ}  (fill K (Case (InjL e) e1 e2)) log t : τ.
218 219 220 221 222 223 224 225 226
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

227
  Lemma bin_log_related_case_inr_l Γ E K e v e1 e2 t τ
228 229
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
230
   (to_val e = Some v) 
231 232
    ({E,E;Γ}  fill K (App e2 e) log t : τ)
    {E,E;Γ}  (fill K (Case (InjR e) e1 e2)) log t : τ.
233 234 235 236 237 238 239 240 241
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

242
  Lemma bin_log_related_if_true_l Γ E K e1 e2 t τ
243 244
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
245 246
    ({E,E;Γ}  fill K e1 log t : τ)
    {E,E;Γ}  (fill K (If (# true) e1 e2)) log t : τ.
247 248
  Proof.
    iIntros "Hlog".
249
    iApply (bin_log_pure_l with "Hlog"); auto; intros.
250 251 252 253 254 255
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

256
  Lemma bin_log_related_if_true_masked_l Γ E1 E2 K e1 e2 t τ
257 258
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
259 260
   ({E1,E2;Γ}  fill K e1 log t : τ)
    {E1,E2;Γ}  (fill K (If (# true) e1 e2)) log t : τ.
261 262
  Proof.
    iIntros "Hlog".
263 264 265
    iApply (bin_log_pure_masked_l with "Hlog"); auto.
    - do 3 eexists. econstructor; eauto. 
    - by inversion 1.
266 267
  Qed.

268
  Lemma bin_log_related_if_false_l Γ E K e1 e2 t τ
269 270
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
271 272
    ({E,E;Γ}  fill K e2 log t : τ)
    {E,E;Γ}  (fill K (If (# false) e1 e2)) log t : τ.
273 274
  Proof.
    iIntros "Hlog".
275 276 277 278 279
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
280 281
  Qed.

282
  Lemma bin_log_related_if_false_masked_l Γ E1 E2 K e1 e2 t τ
283 284
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2) : 
285 286 287 288 289 290 291 292 293
   ({E1,E2;Γ}  fill K e2 log t : τ)
    {E1,E2;Γ}  (fill K (If (# false) e1 e2)) log t : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_masked_l with "Hlog"); auto.
    - do 3 eexists. econstructor; eauto. 
    - by inversion 1.
  Qed.
  
294 295 296
  Lemma bin_log_related_binop_l Γ E K op a b t τ :
    ({E,E;Γ}  fill K (of_val (binop_eval op a b)) log t : τ)
    {E,E;Γ}  (fill K (BinOp op (#n a) (#n b))) log t : τ.
297 298 299 300 301 302 303 304 305
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
    - do 3 eexists. econstructor; eauto.
    - match goal with
      | H : head_step _ _ _ _ _ |- _ => inversion H
      end. done.
  Qed.

306
  (** *** Stateful reductions *)
Dan Frumin's avatar
Dan Frumin committed
307 308 309 310 311
  Lemma bin_log_related_wp_l Γ E K e1 e2 τ
   (Hclosed1 : Closed  e1) :
   (WP e1 @ E {{ v,
     {E,E;Γ}  fill K (of_val v) log e2 : τ }})%I -
   {E,E;Γ}  fill K e1 log e2 : τ.
312
  Proof.
313
    rewrite bin_log_related_eq.
Dan Frumin's avatar
Dan Frumin committed
314
    iIntros "He".
315
    iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
316
    rewrite /env_subst fill_subst /=.
Dan Frumin's avatar
Dan Frumin committed
317 318
    rewrite Closed_subst_p_id. iModIntro.
    iApply (wp_bind (subst_ctx _ K)).
319
    iApply (wp_mask_mono E); auto.
320
    iApply (wp_wand with "He").
321
    iIntros (v) "Hv".
322
    iApply fupd_wp. iApply (fupd_mask_mono E); auto.
Dan Frumin's avatar
Dan Frumin committed
323 324 325 326 327 328 329 330 331 332 333 334 335 336
    iMod ("Hv" with "Hs [HΓ] Hj"); auto.
    rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
    done.
  Qed.

  Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
    (Hclosed1 : Closed  e1) :
    (|={E}=> WP e1 @ E {{ Φ }}) -
    ( v, Φ v - {E,E;Γ}  fill K (of_val v) log e2 : τ) -
    {E,E;Γ}  fill K e1 log e2 : τ.
  Proof.
    iIntros "He Hlog".
    iApply bin_log_related_wp_l.
    iMod "He". by iApply (wp_wand with "He").
337 338
  Qed.
    
339
  Lemma bin_log_related_wp_atomic_l Γ (E1 E2 : coPset) K e1 e2 τ
340
   (Hatomic : atomic e1)
341
   (Hclosed1 : Closed  e1) :
342 343 344 345
   (|={E1,E2}=> WP e1 @ E2 {{ v,
     {E2,E1;Γ}  fill K (of_val v) log e2 : τ }})%I -
   {E1,E1;Γ}  fill K e1 log e2 : τ.
  Proof.
346
    rewrite bin_log_related_eq.
347
    iIntros "Hlog".
348 349 350 351 352 353 354
    iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=". iModIntro.
    rewrite /env_subst fill_subst /=.
    rewrite Closed_subst_p_id.
    iApply (wp_bind (subst_ctx _ K)).
    iApply (wp_mask_mono E1); auto.
    iApply wp_atomic; auto.
    iMod "Hlog" as "He". iModIntro.
355
    iApply (wp_wand with "He").
356 357 358 359 360
    iIntros (v) "Hlog".
    iSpecialize ("Hlog" with "Hs [HΓ]"); first by iFrame.
    iSpecialize ("Hlog" with "Hj"). simpl.
    rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
    by iMod "Hlog".
361
  Qed.
362
  
363
  Lemma bin_log_related_step_atomic_l {A} (Φ : A  val  iProp Σ) Γ E1 E2 K e1 e2 τ
364
    (Hatomic : atomic e1)
365 366
    (Hclosed1 : Closed  e1) :
    (|={E1,E2}=>  (a : A), WP e1 @ E2 {{ v, Φ a v }} 
367 368
    ( v, Φ a v - {E2,E1;Γ}  fill K (of_val v) log e2 : τ)) -
    {E1,E1;Γ}  fill K e1 log e2 : τ.
369
  Proof.
370
    iIntros "Hlog".
371 372
    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as (a) "[He Hlog]". iModIntro.
373
    iApply (wp_wand with "He").
374 375
    iIntros (v) "HΦ".
    iApply ("Hlog" with "HΦ").
376 377 378 379 380 381
  Qed.

  (* TODO: how to make eauto do this? *)
  Ltac rewrite_closed :=
    try (let F := fresh in
      intro F); simpl;
382 383 384 385 386 387 388 389 390 391 392 393 394
       repeat match goal with
        | [ |- Closed  _] => rewrite /Closed; cbn
        | [ |- Is_true (is_closed  (of_val ?v))] => eapply of_val_closed
        | [ |- Is_true (is_closed _ _ && is_closed _ _)]
          => split_and?        
        | [Hval : to_val ?e = Some ?v |- context[is_closed  ?e] ] 
          => rewrite -?(of_to_val e v Hval); eauto
        | [Hval : to_val ?e = Some ?v |- Is_true (is_closed  ?e) ]
          => rewrite -?(of_to_val e v Hval); eauto
        | [Hcl : Closed  ?e |- context[env_subst _ ?e]]
          => rewrite /env_subst Closed_subst_p_id
        | [Hcl : Closed  ?e |- context[subst_p _ ?e]]
          => rewrite Closed_subst_p_id
395 396 397
        end;
      try done.

398
  Lemma bin_log_related_fork_l Γ E1 E2 K (e t : expr) (τ : type)
399
   (Hclosed : Closed  e) :
400 401 402
   (|={E1,E2}=>  (WP e {{ _, True }}) 
    {E2,E1;Γ}  fill K (Lit Unit) log t : τ) -
   {E1,E1;Γ}  fill K (Fork e) log t : τ.
403
  Proof.
404 405 406
    iIntros "Hlog".
    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as "[Hsafe Hlog]". iModIntro.
Dan Frumin's avatar
Dan Frumin committed
407
    iApply wp_fork. iNext. by iFrame "Hsafe".
408 409 410
  Qed.

  Lemma bin_log_related_alloc_l Γ E1 E2 K e v t τ
411
    (Heval : to_val e = Some v) :
412 413 414 415 416
    (|={E1,E2}=>  (l : loc), l ↦ᵢ v -
           {E2,E1;Γ}  fill K (Loc l) log t : τ)%I
    - {E1,E1;Γ}  fill K (Alloc e) log t : τ.
  Proof.
    iIntros "Hlog".
Dan Frumin's avatar
Dan Frumin committed
417
    iApply bin_log_related_wp_atomic_l; auto.
418
    iMod "Hlog". iModIntro. 
Dan Frumin's avatar
Dan Frumin committed
419
    iApply (wp_alloc _ _ v); auto.
420 421
  Qed.

422
  Lemma bin_log_related_alloc_l' Γ E K e v t τ
423
    (Heval : to_val e = Some v) :
424 425 426 427 428 429 430
    ( (l : loc), l ↦ᵢ v - {E,E;Γ}  fill K (Loc l) log t : τ)%I
    - {E,E;Γ}  fill K (Alloc e) log t : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_related_alloc_l); auto. assumption.
  Qed.

431
  Lemma bin_log_related_load_l Γ E1 E2 K l t τ :
432 433
    (|={E1,E2}=>  v',
      (l ↦ᵢ v') 
Dan Frumin's avatar
Dan Frumin committed
434
      (l ↦ᵢ v' - ({ E2,E1; Γ }  fill K (of_val v') log t : τ)))%I
435 436 437
    - {E1,E1;Γ}  fill K (Load (Loc l)) log t : τ.
  Proof.
    iIntros "Hlog".
Dan Frumin's avatar
Dan Frumin committed
438
    iApply bin_log_related_wp_atomic_l; auto.
439
    iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
Dan Frumin's avatar
Dan Frumin committed
440
    iApply (wp_load with "Hl"); auto.
441 442
  Qed.

443
  Lemma bin_log_related_load_l' Γ E1 K l v' t τ :
444
     (l ↦ᵢ v') -
Dan Frumin's avatar
Dan Frumin committed
445
     (l ↦ᵢ v' - ({E1,E1;Γ}  fill K (of_val v') log t : τ))
446 447 448 449 450
    - {E1,E1;Γ}  fill K (Load (Loc l)) log t : τ.
  Proof.
    iIntros "Hl Hlog".
    iApply (bin_log_related_load_l); auto.
    iExists v'.
Dan Frumin's avatar
Dan Frumin committed
451
    iModIntro.
452
    by iFrame.
453 454
  Qed.

455
  Lemma bin_log_related_store_l Γ E1 E2 K l e v' t τ :
456 457
    (to_val e = Some v') 
    (|={E1,E2}=>  v,  (l ↦ᵢ v) 
458
      (l ↦ᵢ v' - {E2,E1;Γ}  fill K (Lit Unit) log t : τ))
459 460 461
    - {E1,E1;Γ}  fill K (Store (Loc l) e) log t : τ.
  Proof.
    iIntros (?) "Hlog".
Dan Frumin's avatar
Dan Frumin committed
462 463 464 465
    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
    iApply (wp_store _ _ _ _ v' with "Hl"); auto.
  Qed.    
466

467
  Lemma bin_log_related_store_l' Γ E K l e v v' t τ :
468 469
    (to_val e = Some v') 
     (l ↦ᵢ v) -
470
    (l ↦ᵢ v' - {E,E;Γ}  fill K (Lit Unit) log t : τ)
471 472 473 474 475 476 477
    - {E,E;Γ}  fill K (Store (Loc l) e) log t : τ.
  Proof.
    iIntros (?) "Hl Hlog".
    iApply (bin_log_related_store_l _ _ _ _ l e v'); auto.
    iModIntro. iExists v. iFrame.
  Qed.

478
  Lemma bin_log_related_cas_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
479 480 481
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
    (|={E1,E2}=>  v',  (l ↦ᵢ v')  
Dan Frumin's avatar
Dan Frumin committed
482 483
     (v'  v1 -  (l ↦ᵢ v' - {E2,E1;Γ}  fill K (# false) log t : τ)) 
     (v' = v1 -  (l ↦ᵢ v2 - {E2,E1;Γ}  fill K (# true) log t : τ)))
484 485 486
    - {E1,E1;Γ}  fill K (CAS (Loc l) e1 e2) log t : τ.
  Proof.
    iIntros (??) "Hlog".
Dan Frumin's avatar
Dan Frumin committed
487
    iApply bin_log_related_wp_atomic_l; auto.
488 489 490
    iMod "Hlog" as (v') "[Hl [Hlog_fail Hlog_suc]]". iModIntro. 
    destruct (decide (v' = v1)).
    - (* CAS successful *) subst.      
Dan Frumin's avatar
Dan Frumin committed
491 492
      iApply (wp_cas_suc with "Hl"); eauto.
      iSpecialize ("Hlog_suc" with "[]"); eauto.
493
    - (* CAS failed *)
Dan Frumin's avatar
Dan Frumin committed
494
      iApply (wp_cas_fail with "Hl"); eauto. 
Dan Frumin's avatar
Dan Frumin committed
495
      iSpecialize ("Hlog_fail" with "[]"); eauto.
496 497
  Qed.

498
  Lemma bin_log_related_cas_fail_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
499 500
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
501
    (|={E1,E2}=>  v',  (l ↦ᵢ v')  v'  v1 
502 503 504 505
     (l ↦ᵢ v' - {E2,E1;Γ}  fill K (# false) log t : τ))
    - {E1,E1;Γ}  fill K (CAS (Loc l) e1 e2) log t : τ.
  Proof.
    iIntros (??) "Hlog".
Dan Frumin's avatar
Dan Frumin committed
506
    iApply bin_log_related_wp_atomic_l; auto.
507
    iMod "Hlog" as (v') "[Hl [% Hlog]]". iModIntro. 
Dan Frumin's avatar
Dan Frumin committed
508
    iApply (wp_cas_fail with "Hl"); eauto.
509 510
  Qed.
  
511
  Lemma bin_log_related_cas_fail_l' Γ E K l e1 e2 v1 v2 v' t τ :
512 513
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
514
    (v'  v1) 
515 516 517 518 519 520 521 522 523
     (l ↦ᵢ v') -
    (l ↦ᵢ v' - {E,E;Γ}  fill K (# false) log t : τ)
    - {E,E;Γ}  fill K (CAS (Loc l) e1 e2) log t : τ.
  Proof.
    iIntros (???) "Hl Hlog".
    iApply bin_log_related_cas_fail_l; eauto.
    iModIntro. iExists v'. iFrame "Hl Hlog". eauto.
  Qed.

524
  Lemma bin_log_related_cas_suc_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
525 526 527 528 529 530 531
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
    (|={E1,E2}=>  (l ↦ᵢ v1) 
     (l ↦ᵢ v2 - {E2,E1;Γ}  fill K (# true) log t : τ))
    - {E1,E1;Γ}  fill K (CAS (Loc l) e1 e2) log t : τ.
  Proof.  
    iIntros (??) "Hlog".
Dan Frumin's avatar
Dan Frumin committed
532
    iApply bin_log_related_wp_atomic_l; auto.
533
    iMod "Hlog" as "[Hl Hlog]". iModIntro. 
Dan Frumin's avatar
Dan Frumin committed
534
    iApply (wp_cas_suc with "Hl"); eauto.
535 536
  Qed.

537
  Lemma bin_log_related_cas_suc_l' Γ E K l e1 e2 v1 v2 v' t τ :
538 539 540 541
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
    (v' = v1) 
     (l ↦ᵢ v') -
542 543
    (l ↦ᵢ v2 - {E,E;Γ}  fill K (# true) log t : τ)
    - {E,E;Γ}  fill K (CAS (Loc l) e1 e2) log t : τ.
544 545 546 547 548 549 550 551
  Proof.
    iIntros (???) "Hl Hlog". subst.
    iApply bin_log_related_cas_suc_l; eauto.
    iModIntro. iFrame.
  Qed.
  
  (** ** Reductions on the right *)
  (** Lifting of the pure reductions *)
552 553
  Lemma bin_log_pure_r Γ τ K' E1 E2 e e' t
    (Hspec : nclose specN  E1)
554 555
    (Hclosed1 : Closed  e)
    (Hclosed2 : Closed  e') :
556
    ( σ, head_step e σ e' σ []) 
557 558
    {E1,E2;Γ}  t log fill K' e' : τ
     {E1,E2;Γ}  t log fill K' e : τ.
559
  Proof.
560
    rewrite bin_log_related_eq.
561 562 563
    iIntros (Hstep) "Hlog".
    iIntros (Δ vvs ρ) "#Hs #HΓ".
    iIntros (j K) "Hj /=".
564 565 566 567 568
    rewrite /env_subst fill_subst -fill_app.
    iMod (step_pure _ _ _ _ (subst_p _ e) (env_subst (snd <$> vvs) e') with "[Hs Hj]") as "Hj"; eauto.
    { rewrite /env_subst. rewrite_closed. }
    rewrite fill_app -fill_subst.
    iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.    
569 570
  Qed.

571
  Lemma bin_log_related_rec_r Γ E1 E2 K f x e e' t v' τ
572
   (Hspec : nclose specN  E1)
573
   (Hclosed : Closed (x :b: f :b: ) e) :
574
   (to_val e' = Some v') 
575 576
   {E1,E2;Γ}  t log fill K (subst' f (Rec f x e) (subst' x e' e)) : τ
    {E1,E2;Γ}  t log fill K (App (Rec f x e) e') : τ.
577 578 579
  Proof.
    iIntros (?) "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
580 581 582 583 584 585 586 587
    { rewrite_closed. }
    { replace (rec: f x := e)%E with (of_val (rec: f x := e)%V) by (unlock; done).
      replace e' with (of_val v') by (by rewrite (of_to_val e' v')).
      rewrite -subst_p_rec /=.
      eapply subst_p_closes; eauto.
      destruct f, x; cbn-[union]; rewrite ?dom_insert ?dom_singleton ?dom_empty;
        set_solver. (* TODO: slow af *) }
    { econstructor; eauto. }
588 589
  Qed.

590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610
  Lemma bin_log_related_tlam_r Γ E1 E2 K e t τ
   (Hclosed : Closed  e)
   (Hspec : nclose specN  E1) :
   {E1,E2;Γ}  t log fill K e : τ
    {E1,E2;Γ}  t log fill K (TApp (TLam e)) : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

  Lemma bin_log_related_fold_r Γ E1 E2 K e v t τ
   (Hval : to_val e = Some v)
   (Hspec : nclose specN  E1) :
   {E1,E2;Γ}  t log fill K e : τ
    {E1,E2;Γ}  t log fill K (Unfold (Fold e)) : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.
611
  
612 613 614 615 616 617 618 619 620 621 622 623 624
  Lemma bin_log_related_pack_r Γ E1 E2 K e e' v t τ
   (Hclosed : Closed  e')
   (Hval : to_val e = Some v)
   (Hspec : nclose specN  E1) :
   {E1,E2;Γ}  t log fill K (App e' e) : τ
    {E1,E2;Γ}  t log fill K (Unpack (Pack e) e') : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

  Lemma bin_log_related_fst_r Γ E1 E2 K e v1 v2 τ
625
   (Hspec : nclose specN  E1) :
626 627
   {E1,E2;Γ}  e log (fill K (of_val v1)) : τ
    {E1,E2;Γ}  e log (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
628 629 630 631 632 633
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

634
  Lemma bin_log_related_snd_r Γ E1 E2 K e v1 v2 τ
635
   (Hspec : nclose specN  E1) :
636 637
   {E1,E2;Γ}  e log (fill K (of_val v2)) : τ
    {E1,E2;Γ}  e log (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
638 639 640 641 642 643
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

644
  Lemma bin_log_related_case_inl_r Γ E1 E2 K e v e1 e2 t τ
645 646 647 648 649 650 651 652 653 654 655 656
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2)   
   (Hval : to_val e = Some v)
   (Hspec : nclose specN  E1) :
   {E1,E2;Γ}  t log (fill K (App e1 e)) : τ
    {E1,E2;Γ}  t log (fill K (Case (InjL e) e1 e2)) : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

657
  Lemma bin_log_related_case_inr_r Γ E1 E2 K e v e1 e2 t τ
658 659 660 661 662 663 664 665 666 667 668
   (Hclosed1 : Closed  e1) 
   (Hclosed2 : Closed  e2)   
   (Hval : to_val e = Some v)
   (Hspec : nclose specN  E1) :
   {E1,E2;Γ}  t log (fill K (App e2 e)) : τ
    {E1,E2;Γ}  t log (fill K (Case (InjR e) e1 e2)) : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.
669

670 671
  Lemma bin_log_related_if_true_r Γ K E1 E2 e e1 e2 τ
   (Hspec : nclose specN  E1)
672 673
   (Hclosed1 : Closed  e1)
   (Hclosed2 : Closed  e2) :
674 675
   {E1,E2;Γ}  e log (fill K e1) : τ
    {E1,E2;Γ}  e log (fill K (If (# true) e1 e2)) : τ.
676 677 678 679 680 681
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

682 683
  Lemma bin_log_related_if_false_r Γ K E1 E2 e e1 e2 τ
   (Hspec : nclose specN  E1)
684 685
   (Hclosed1 : Closed  e1)
   (Hclosed2 : Closed  e2) :
686 687
   {E1,E2;Γ}  e log (fill K e2) : τ
    {E1,E2;Γ}  e log (fill K (If (# false) e1 e2)) : τ.
688 689 690 691 692 693
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
    { econstructor; eauto. }
  Qed.

694
  Lemma bin_log_related_binop_r Γ K E1 E2 op a b t τ
695
   (Hspec : nclose specN  E1) :
696 697 698 699 700
   {E1,E2;Γ}  t log fill K (of_val (binop_eval op a b)) : τ
    {E1,E2;Γ}  t log (fill K (BinOp op (#n a) (#n b))) : τ.
  Proof.
    iIntros "Hlog".
    iApply (bin_log_pure_r with "Hlog"); auto; intros.
Dan Frumin's avatar
Dan Frumin committed
701
    { econstructor; eauto. }
702 703
  Qed.
  
704 705
  (** Stateful reductions *)
  Lemma bin_log_related_step_r Φ Γ E1 E2 K' e1 e2 τ
706
    (Hclosed2 : Closed  e2) :
707
    ( ρ j K, spec_ctx ρ - (j  fill K e2 ={E1}=  v, j  fill K (of_val v)
708
                   Φ v)) -
709 710 711
    ( v, Φ v - {E1,E2;Γ}  e1 log fill K' (of_val v) : τ) -
    {E1,E2;Γ}  e1 log fill K' e2 : τ.
  Proof.
712
    rewrite bin_log_related_eq.
713 714
    iIntros "He Hlog".
    iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K) "Hj /=".
715
    rewrite /env_subst fill_subst /= -fill_app.
716
    rewrite_closed.
717 718 719 720 721
    iMod ("He" $! ρ j with "Hs Hj") as (v) "[Hj Hv]".    
    iSpecialize ("Hlog" $! v with "Hv Hs [HΓ]"); first by iFrame.
    rewrite /env_subst fill_app fill_subst.
    rewrite of_val_subst_p /=.
    iSpecialize ("Hlog" with "Hj"); simpl.
722 723 724
    done.
  Qed.

725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742
  Lemma bin_log_related_fork_r Γ E1 E2 K (e t : expr) (τ : type)
   (Hmasked : nclose specN  E1)
   (Hclosed : Closed  e) :
   ( i, i  e -
     {E1,E2;Γ}  t log fill K (Lit Unit) : τ) -
   {E1,E2;Γ}  t log fill K (Fork e) : τ.
  Proof.
    iIntros "Hlog".
    pose (Φ := (fun (v : val) =>  i, i  e  v = #()%V)%I).
    iApply (bin_log_related_step_r Φ with "[]"); cbv[Φ].
    { iIntros (ρ j K') "#Hspec Hj".
      tp_fork j as i "Hi".
      iModIntro. iExists #()%V. iFrame. eauto.
    }
    iIntros (v). iDestruct 1 as (i) "[Hi %]"; subst.
    by iApply "Hlog".
  Qed.

743 744
  Lemma bin_log_related_alloc_r Γ K E1 E2 e v t τ
    (Hmasked : nclose specN  E1)
745
    (Heval : to_val e = Some v) :
746 747 748 749 750 751
    ( (l : loc), l ↦ₛ v - {E1,E2;Γ}  t log fill K (Loc l) : τ)%I
    - {E1,E2;Γ}  t log fill K (Alloc e) : τ.
  Proof.
    iIntros "Hlog".
    pose (Φ := (fun w =>  l, w = (LocV l)  l ↦ₛ v)%I).
    iApply (bin_log_related_step_r Φ with "[]").
752
    { cbv[Φ]. 
753 754
      iIntros (ρ j K') "#Hs Hj /=".
      tp_alloc j as l "Hl". iExists (LocV l).
755
      iFrame. iExists l. eauto. }
756 757 758 759 760 761
    iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
    iApply "Hlog".
    done.
  Qed.

  Lemma bin_log_related_load_r Γ K E1 E2 l v' t τ
762
    (Hmasked : nclose specN  E1) :
763 764 765 766 767 768 769 770 771
    l ↦ₛ v' -
    (l ↦ₛ v' - {E1,E2;Γ}  t log fill K (of_val v') : τ)
    - {E1,E2;Γ}  t log fill K (Load (Loc l)) : τ.
  Proof.
    iIntros "Hl Hlog".
    pose (Φ := (fun w => w = v'⌝  l ↦ₛ v')%I).
    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
    { cbv[Φ].
      iIntros (ρ j K') "#Hs Hj /=". iExists v'.
Dan Frumin's avatar
Dan Frumin committed
772
      tp_load j.
773 774 775 776 777 778
      iFrame. eauto. }
    iIntros (v) "[% Hl]"; subst.
    iApply "Hlog".
    done.
  Qed.

779
  Lemma bin_log_related_store_r Γ K E1 E2 l e v v' t τ 
780
    (Hmasked : nclose specN  E1) :
781 782
    (to_val e = Some v') 
    l ↦ₛ v -
783
    (l ↦ₛ v' - {E1,E2;Γ}  t log fill K (Lit Unit) : τ)
784
    - {E1,E2;Γ}  t log fill K (Store (Loc l) e) : τ.
785 786 787 788 789 790
  Proof.
    iIntros (?) "Hl Hlog".
    pose (Φ := (fun w => w = UnitV  l ↦ₛ v')%I).
    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
    { cbv[Φ].
      iIntros (ρ j K') "#Hs Hj /=". iExists UnitV.
Dan Frumin's avatar
Dan Frumin committed
791
      tp_store j.
792 793 794 795 796 797
      iFrame. eauto. }
    iIntros (w) "[% Hl]"; subst.
    iApply "Hlog".
    done.
  Qed.
  
798
  Lemma bin_log_related_cas_fail_r Γ E1 E2 K l e1 e2 v1 v2 v t τ :
799
    (nclose specN  E1) 
800 801
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
802
    (v  v1) 
803
    l ↦ₛ v -
804 805
    (l ↦ₛ v - {E1,E2;Γ}  t log fill K (# false) : τ)
    - {E1,E2;Γ}  t log fill K (CAS (Loc l) e1 e2) : τ.
806
  Proof.
807
    iIntros (????) "Hl Hlog".
808 809 810 811
    pose (Φ := (fun w => w = BoolV false  l ↦ₛ v)%I).
    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
    { cbv[Φ].
      iIntros (ρ j K') "#Hs Hj /=".
Dan Frumin's avatar
Dan Frumin committed
812
      tp_cas_fail j; auto.
813 814 815 816 817 818 819
      iExists (BoolV false). simpl.
      iFrame. eauto. }
    iIntros (w) "[% Hl]"; subst.
    iApply "Hlog".
    done.
  Qed.

820
  Lemma bin_log_related_cas_suc_r Γ E1 E2 K l e1 e2 v1 v2 v t τ :
821
    (nclose specN  E1)    
822 823 824 825
    (to_val e1 = Some v1) 
    (to_val e2 = Some v2) 
    (v = v1) 
    l ↦ₛ v -
826 827
    (l ↦ₛ v2 - {E1,E2;Γ}  t log fill K (# true) : τ)
    - {E1,E2;Γ}  t log fill K (CAS (Loc l) e1 e2) : τ.
828
  Proof.
829
    iIntros (????) "Hl Hlog".
830 831 832 833
    pose (Φ := (fun w => w = BoolV true  l ↦ₛ v2)%I).
    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
    { cbv[Φ].
      iIntros (ρ j K') "#Hs Hj /=".
Dan Frumin's avatar
Dan Frumin committed
834
      tp_cas_suc j; auto.
835 836 837 838 839 840 841
      iExists (BoolV true). simpl.
      iFrame. eauto. }
    iIntros (w) "[% Hl]"; subst.
    iApply "Hlog".
    done.
  Qed.

842 843
  (* To prevent accidental unfolding by iMod or other tactics *)
  Typeclasses Opaque bin_log_related.
844
End properties.