lateearlychoice.v 4.12 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 20 21 22

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

  Definition choice_inv y y' : iProp Σ :=
    ( f, y ↦ᵢ (#v f)  y' ↦ₛ (#v f))%I.

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

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

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

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

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

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

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

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

144
End Refinement.