lateearlychoice.v 3.83 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.
Dan Frumin's avatar
Dan Frumin committed
26 27
    wp_rec.
    wp_alloc y as "Hy".
28
    iMod (inv_alloc choiceN _ (y ↦ᵢ #false  y ↦ᵢ #true)%I with "[Hy]") as "#Hinv"; eauto.
Dan Frumin's avatar
Dan Frumin committed
29
    wp_rec.
30 31
    wp_bind (Fork _). iApply wp_fork. iNext.
    iSplitL.
Dan Frumin's avatar
Dan Frumin committed
32
    - iModIntro. wp_rec.
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 40 41
  Lemma rand_l Δ Γ K ρ t τ :
    spec_ctx ρ - ( b : bool, {Δ;Γ}  fill K #b log t : τ) -
    {Δ;Γ}  fill K (rand #()) log t : τ.
42
  Proof.
43
    iIntros  "#Hs Hlog".
44 45
    unfold rand. unlock. simpl.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
46
    rel_alloc_l as y "Hy". simpl.
47
    rel_rec_l.
48
    iMod (inv_alloc choiceN _ ( b : bool, y ↦ᵢ #b)%I with "[Hy]") as "#Hinv".
49
    { iNext. eauto. }
50
    rel_fork_l. iModIntro.
51 52 53 54 55 56 57 58
    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.
59
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
60 61
      rel_load_l_atomic.
      iInv choiceN as (b) "Hy" "Hcl".
62
      iExists #b. iFrame.
Dan Frumin's avatar
Dan Frumin committed
63
      iModIntro. iNext. iIntros "Hy".
64 65 66 67
      iMod ("Hcl" with "[Hy]").
      { iNext. iExists b. iFrame. }
      done. 
  Qed.
68

69
  Lemma rand_r (b : bool) Δ Γ E1 K ρ t τ :
70 71 72
    specN  E1 
    choiceN  E1 
    spec_ctx ρ -
73 74
    {E1;Δ;Γ}  t log fill K #b : τ -
    {E1;Δ;Γ}  t log fill K (rand #()) : τ.
75 76 77 78 79 80 81 82 83
  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.
84
    - tp_store j.
85 86 87 88
      by rel_load_r.
    - by rel_load_r.
  Qed.

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

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

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

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

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

142
End Refinement.