lateearlychoice.v 4.61 KB
Newer Older
1 2 3 4
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris.base_logic Require Import lib.auth.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
5
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
6 7 8 9 10 11 12 13 14 15 16 17 18 19
From iris.program_logic Require Import adequacy.

From iris_logrel.F_mu_ref_conc Require Import hax.

Definition rand : val := λ: <>,
  let: "y" := (ref (# false))
  in Fork ("y" <- # true);;
     !"y".
Definition lateChoice : val := λ: "x",
  "x" <- #n 0;; rand #().
Definition earlyChoice : val := λ: "x",
  let: "r" := rand #() in "x" <- #n 0;; "r".

Section Refinement.
20
  Context `{logrelG Σ}.
21 22 23 24 25 26 27 28 29 30 31

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

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

  Lemma wp_rand :
    (WP rand #() {{ v, v = #v true  v = #v false}})%I.
  Proof.
    iStartProof.
    unfold rand. unlock.
32
    iApply wp_rec; eauto. iNext. simpl.
33 34
    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.
35
    iApply wp_rec; eauto. iNext. simpl.
36 37
    wp_bind (Fork _). iApply wp_fork. iNext.
    iSplitL.
38
    - iModIntro. iApply wp_rec; eauto. iNext; simpl.
39 40 41 42 43 44 45 46 47 48 49 50
      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.

  Lemma rand_l Γ E1 K ρ t τ :
    choiceN  E1 
    spec_ctx ρ - ( b, {E1,E1;Γ}  fill K (# b) log t : τ)
    - {E1,E1;Γ}  fill K (rand #())%E log t : τ.
  Proof.
    iIntros (?) "#Hs Hlog".
51 52
    unfold rand. unlock. simpl.
    rel_rec_l.
53 54
    rel_bind_l (Alloc _).
    iApply bin_log_related_alloc_l'; first eauto. iIntros (y) "Hy". simpl.
55
    rel_rec_l.
56 57
    iMod (inv_alloc choiceN _ ( b, y ↦ᵢ (#v b))%I with "[Hy]") as "#Hinv".
    { iNext. eauto. }
58
    rel_fork_l. iModIntro.
59 60 61 62 63 64 65 66
    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.
67 68 69
      rel_rec_l.
      rel_load_l under choiceN as "Hy" "Hcl".
        iDestruct "Hy" as (b) "Hy".
Dan Frumin's avatar
Dan Frumin committed
70 71
        iExists (#v b). iFrame.
        iModIntro. iNext. iIntros "Hy".
72 73 74 75
      iMod ("Hcl" with "[Hy]").
      { iNext. iExists b. iFrame. }
      done. 
  Qed.
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96

  Lemma rand_r b Γ E1 E2 K ρ t τ :
    specN  E1 
    choiceN  E1 
    spec_ctx ρ -
    {E1,E2;Γ}  t log fill K (# b) : τ -
    {E1,E2;Γ}  t log fill K (rand #())%E : τ.
  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.
    - iApply fupd_logrel'. tp_store j. iModIntro.
      by rel_load_r.
    - by rel_load_r.
  Qed.

97 98
  Lemma lateChoice_l Γ x v ρ t :
    spec_ctx ρ - x ↦ᵢ v -
99
    (x ↦ᵢ (#nv 0) -  b, Γ  # b log t : TBool) -
100 101 102 103
    Γ  lateChoice #x log t : TBool.
  Proof.  
    iIntros "#Hs Hx Hlog".
    unfold lateChoice. unlock.
104 105 106 107 108 109
    rel_rec_l.
    rel_store_l. simpl.
    rel_rec_l.
    rel_bind_l (rand #())%E.
    iApply (rand_l with "Hs"); eauto. simpl.
    by iApply "Hlog".
110
  Qed.
111
   
112 113 114 115 116
  Lemma prerefinement Γ x x' n ρ :
    (spec_ctx ρ - x ↦ᵢ (#nv n) - x' ↦ₛ (#nv n) -
      Γ  lateChoice #x log earlyChoice #x' : TBool)%I.
  Proof.
    iIntros "#Hspec Hx Hx'".
117 118 119
    iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
    iIntros (b).
    unfold earlyChoice. unlock.
120
    rel_rec_r.
121

122 123
    rel_bind_r (rand #())%E.
    iApply (rand_r b with "Hspec"); eauto. simpl.
124
    rel_rec_r.
125
    rel_store_r. simpl.
126
    rel_rec_r.
127
    rel_vals; eauto.
128 129
  Qed.

130 131 132
  Lemma prerefinement2 Γ x x' n ρ :
    (spec_ctx ρ - x ↦ᵢ (#nv n) - x' ↦ₛ (#nv n) -
      Γ  earlyChoice #x log lateChoice #x' : TBool)%I.
133
  Proof.
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
    iIntros "#Hspec Hx Hx'".
    unfold earlyChoice. unlock.
    rel_rec_l.
    rel_bind_l (rand #())%E.
    iApply (rand_l with "Hspec"); eauto. simpl. iIntros (b).
    rel_rec_l.

    unfold lateChoice. unlock.
    rel_rec_r.
    rel_store_r. simpl.
    rel_rec_r.
    rel_bind_r (rand #())%E.
    iApply (rand_r b with "Hspec"); eauto. simpl.

    rel_store_l. simpl.
    rel_rec_l.
    rel_vals; eauto.
  Qed.
152 153
    
End Refinement.