lateearlychoice.v 4.04 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris_logrel Require Export logrel.
3 4

Definition rand : val := λ: <>,
5 6
  let: "y" := ref #false
  in Fork ("y" <- #true);;
7
     !"y".
8

9
Definition lateChoice : val := λ: "x",
10
  "x" <- #0;; rand #().
11
Definition earlyChoice : val := λ: "x",
12
  let: "r" := rand #() in "x" <- #0;; "r".
13 14

Section Refinement.
15
  Context `{logrelG Σ}.
16 17 18 19

  Definition choiceN : namespace := nroot .@ "choice".

  Definition choice_inv y y' : iProp Σ :=
20
    ( f : bool, y ↦ᵢ #f  y' ↦ₛ #f)%I.
21 22

  Lemma wp_rand :
23
    (WP rand #() {{ v, v = #true  v = #false}})%I.
24 25
  Proof.
    unfold rand. unlock.
26
    iApply wp_rec; eauto. iNext. simpl.
27
    wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy".
28
    iMod (inv_alloc choiceN _ (y ↦ᵢ #false  y ↦ᵢ #true)%I with "[Hy]") as "#Hinv"; eauto.
29
    iApply wp_rec; eauto. iNext. simpl.
30 31
    wp_bind (Fork _). iApply wp_fork. iNext.
    iSplitL.
32
    - iModIntro. iApply wp_rec; eauto. iNext; simpl.
33 34 35 36 37 38
      iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_load with "Hy"); eauto; iNext;
        iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
    - iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_store with "Hy"); eauto; iNext;
        iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
  Qed.

39
  Lemma rand_l Δ Γ E1 K ρ t τ :
40
    choiceN  E1 
41 42
    spec_ctx ρ - ( b : bool, {E1,E1;Δ;Γ}  fill K #b log t : τ) -
    {E1,E1;Δ;Γ}  fill K (rand #()) log t : τ.
43 44
  Proof.
    iIntros (?) "#Hs Hlog".
45 46
    unfold rand. unlock. simpl.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
47
    rel_alloc_l as y "Hy". simpl.
48
    rel_rec_l.
49
    iMod (inv_alloc choiceN _ ( b : bool, y ↦ᵢ #b)%I with "[Hy]") as "#Hinv".
50
    { iNext. eauto. }
51
    rel_fork_l. iModIntro.
52 53 54 55 56 57 58 59
    iSplitR.
    - iNext.
      iInv choiceN as (b) "Hy" "Hcl".
      iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
      iMod ("Hcl" with "[Hy]").
      { iNext. iExists true. by iFrame. }
      done.
    - simpl.
60
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
61 62
      rel_load_l_atomic.
      iInv choiceN as (b) "Hy" "Hcl".
63
      iExists #b. iFrame.
Dan Frumin's avatar
Dan Frumin committed
64
      iModIntro. iNext. iIntros "Hy".
65 66 67 68
      iMod ("Hcl" with "[Hy]").
      { iNext. iExists b. iFrame. }
      done. 
  Qed.
69

70
  Lemma rand_r (b : bool) Δ Γ E1 E2 K ρ t τ :
71 72 73
    specN  E1 
    choiceN  E1 
    spec_ctx ρ -
74
    {E1,E2;Δ;Γ}  t log fill K #b : τ -
75
    {E1,E2;Δ;Γ}  t log fill K (rand #()) : τ.
76 77 78 79 80 81 82 83 84
  Proof.
    iIntros (??) "#Hs Hlog".
    unfold rand. unlock.
    rel_rec_r.
    rel_alloc_r as y "Hy".
    rel_rec_r.
    rel_fork_r as j "Hj".
    rel_rec_r.
    destruct b.
Dan Frumin's avatar
Dan Frumin committed
85
    - tp_store j.
86 87 88 89
      by rel_load_r.
    - by rel_load_r.
  Qed.

90
  Lemma lateChoice_l Δ Γ x v ρ t :
91
    spec_ctx ρ - x ↦ᵢ v -
92
    (x ↦ᵢ #0 -  b : bool, {,;Δ;Γ}  #b log t : TBool) -
93 94
    {,;Δ;Γ}  lateChoice #x log t : TBool.
  Proof.
95 96
    iIntros "#Hs Hx Hlog".
    unfold lateChoice. unlock.
97 98 99
    rel_rec_l.
    rel_store_l. simpl.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
100
    rel_apply_l (rand_l with "Hs"); eauto.
101
    by iApply "Hlog".
102
  Qed.
103
   
104
  Lemma prerefinement Δ Γ x x' n ρ :
105 106
    spec_ctx ρ - x ↦ᵢ #n - x' ↦ₛ #n -
    {,;Δ;Γ}  lateChoice #x log earlyChoice #x' : TBool.
107 108
  Proof.
    iIntros "#Hspec Hx Hx'".
109 110 111
    iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
    iIntros (b).
    unfold earlyChoice. unlock.
112
    rel_rec_r.
113

Dan Frumin's avatar
Dan Frumin committed
114
    rel_apply_r (rand_r b with "Hspec"); eauto.
115
    rel_rec_r.
116
    rel_store_r. simpl.
117
    rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
118
    rel_vals; eauto.
119 120
  Qed.

121
  Lemma prerefinement2 Δ Γ x x' n ρ :
122 123
    spec_ctx ρ - x ↦ᵢ #n - x' ↦ₛ #n -
    {,;Δ;Γ}  earlyChoice #x log lateChoice #x' : TBool.
124
  Proof.
125 126 127
    iIntros "#Hspec Hx Hx'".
    unfold earlyChoice. unlock.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
128 129
    rel_apply_l (rand_l with "Hspec"); eauto.
    iIntros (b).
130 131 132 133 134 135
    rel_rec_l.

    unfold lateChoice. unlock.
    rel_rec_r.
    rel_store_r. simpl.
    rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
136
    rel_apply_r (rand_r b with "Hspec"); eauto.
137 138 139

    rel_store_l. simpl.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
140
    rel_vals; eauto.
141
  Qed.
Dan Frumin's avatar
Dan Frumin committed
142

143
End Refinement.