generative.v 10.3 KB
Newer Older
1 2 3 4 5
(** More generative ADT example from "State-Dependent
Represenation Independence" by A. Ahmed, D. Dreyer, A. Rossberg. *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gset frac.
From iris.base_logic.lib Require Import auth.
6 7 8 9 10 11 12 13 14 15 16 17 18
From iris_logrel Require Import logrel examples.counter examples.lock prelude.bij.

(** * 5.2 References for name generation *)

Definition nameGenTy : type := TExists (TProd (TArrow TUnit (TVar 0))
                                              (TArrow (TVar 0) (TArrow (TVar 0) TBool))).

Definition nameGen1 : val :=
  PackV (λ: <>, ref #()
        ,λ: "y" "z", "y" = "z").

Definition nameGen2 : expr :=
  let: "x" := ref #0 in
Dan Frumin's avatar
Dan Frumin committed
19
  Pack (λ: <>, FG_increment "x";; !"x"
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
       ,λ: "y" "z", "y" = "z").

Lemma nameGen1_typed Γ :
  typed Γ nameGen1 nameGenTy.
Proof.
  unlock nameGen1 nameGenTy.
  apply TPack with (Tref TUnit). asimpl.
  solve_typed.
Qed.
Hint Resolve nameGen1_typed : typeable.

Lemma nameGen2_typed Γ :
  typed Γ nameGen2 nameGenTy.
Proof.
  unlock nameGen2 nameGenTy.
  econstructor. 2: solve_typed.
  econstructor. cbn.
  eapply TPack with TNat. asimpl.
  econstructor; solve_typed.
  econstructor. cbn.
  econstructor. cbn. solve_typed.
  econstructor; eauto; solve_typed.
Qed.
Hint Resolve nameGen2_typed : typeable.

Section namegen_refinement.
  Context `{logrelG Σ, PrePBijG loc nat Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).

  Program Definition ngR (γ : gname) : D := λne vv,
    ( (l : loc) (n : nat), vv.1 = #l%V  vv.2 = #n
    inBij γ l n)%I.
  Next Obligation. solve_proper. Qed.

Dan Frumin's avatar
Dan Frumin committed
54
  Instance ngR_persistent γ ww : Persistent (ngR γ ww).
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
  Proof. apply _. Qed.

  Definition ng_Inv (γ : gname) (c : loc) : iProp Σ :=
    ( (n : nat) (L : gset (loc * nat)),
        BIJ γ L  c ↦ₛ #n
       [ set] lk  L, match lk with
                        | (l, k) => l ↦ᵢ #()  k  n
                        end)%I.

  Lemma nameGen_ref1 Γ :
    Γ  nameGen1 log nameGen2 : nameGenTy.
  Proof.
    iIntros (Δ).
    unlock nameGenTy nameGen1 nameGen2.
    rel_alloc_r as c "Hc". rel_let_r.
    iMod alloc_empty_bij as (γ) "HB".
    pose (N:=logrelN.@"ng").
    iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
    { iNext. iExists 0, . iFrame.
      by rewrite big_sepS_empty. }
75
    iApply (bin_log_related_pack (ngR γ)).
76 77 78 79 80 81 82 83 84
    iApply bin_log_related_pair.
    - (* New name *)
      iApply bin_log_related_arrow_val; eauto.
      iAlways.
      iIntros (? ?) "/= [% %]"; simplify_eq.
      rel_seq_l. rel_seq_r.
      rel_alloc_l_atomic.
      iInv N as (n L) "(HB & Hc & HL)" "Hcl".
      iModIntro. iNext. iIntros (l') "Hl'".
85
      rel_apply_r (bin_log_related_FG_increment_r with "Hc").
86 87 88 89
      { solve_ndisj. }
      iIntros "Hc".
      rel_seq_r.
      rel_load_r.
Dan Frumin's avatar
Dan Frumin committed
90
      iAssert (( y, (l', y)  L)  False)%I with "[HL Hl']" as %Hl'.
91 92 93 94 95
      { iIntros (Hy). destruct Hy as [y Hy].
        rewrite (big_sepS_elem_of _ L (l',y) Hy).
        iDestruct "HL" as "[Hl _]".
        iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hfoo.
        compute in Hfoo. eauto. }
Dan Frumin's avatar
Dan Frumin committed
96
      iAssert (( x, (x, S n)  L)  False)%I with "[HL]" as %Hc.
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
      { iIntros (Hx). destruct Hx as [x Hy].
        rewrite (big_sepS_elem_of _ L (x,S n) Hy).
        iDestruct "HL" as "[_ %]". omega. }
      iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto.
      iMod ("Hcl" with "[-]").
      { iNext. iExists _,_; iFrame.
        rewrite big_sepS_insert; last by naive_solver.
        iFrame. iSplit; eauto.
        iApply (big_sepS_mono _ _ L L with "HL"); first reflexivity.
        intros [l x] Hlx. apply uPred.sep_mono_r, uPred.pure_mono. eauto. }
      rel_vals. iModIntro. iAlways.
      iExists _, _; eauto.
    - (* Name comparison *)
      iApply bin_log_related_arrow_val; eauto.
      iAlways.
      iIntros (? ?) "/= #Hv".
      iDestruct "Hv" as (l n) "(% & % & #Hln)". simplify_eq.
      rel_seq_l. rel_seq_r.
      iApply bin_log_related_arrow_val; eauto.
      iAlways.
      iIntros (? ?) "/= #Hv".
      iDestruct "Hv" as (l' n') "(% & % & #Hl'n')". simplify_eq.
      rel_seq_l. rel_seq_r.
      (* we would like to have an atomic version of `rel_op_l`? *)
      rel_bind_l (#l = #l')%E.
      iApply bin_log_related_wp_atomic_l.
      iInv N as (m L) "(>HB & >Hc & HL)" "Hcl".
      iModIntro. wp_op.
      rel_op_r.
      iDestruct (bij_agree with "HB Hln Hl'n'") as %Hag.
      destruct (decide (l = l')) as [->|Hll].
      + assert (n = n') as -> by (apply Hag; auto).
129
        case_decide; last by contradiction.
130 131 132 133 134
        iMod ("Hcl" with "[-]") as "_".
        { iNext. iExists _,_; iFrame. }
        iApply bin_log_related_bool.
      + assert (n  n') as Hnn'.
        { intros Hnn. apply Hll. by apply Hag. }
135
        case_decide; first by contradiction.
136 137 138 139 140 141
        iMod ("Hcl" with "[-]") as "_".
        { iNext. iExists _,_; iFrame. }
        iApply bin_log_related_bool.
  Qed.

End namegen_refinement.
142 143 144 145 146 147 148 149 150 151 152 153 154 155

(** * 5.4 Cell class *)
Definition cellτ : type :=
  TForall (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
                                 (TArrow (TVar 0) (TVar 1)))
                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit)))).
Definition cell1 : val :=
  Λ: Pack (λ: "x", ref "x", λ: "r", !"r", λ: "r" "x", "r" <- "x").
Lemma cell1_typed Γ :
  typed Γ cell1 cellτ.
Proof.
  unfold cellτ. unlock cell1.
  solve_typed.
Qed.
156
Hint Resolve cell1_typed : typeable.
157 158

Definition cell2 : val :=
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
  Λ: Pack ( λ: "x", (ref #false, ref "x", ref "x", newlock #())
         ,  λ: "r", let: "l" := (Snd "r") in
                    acquire "l";;
                    let: "v" :=
                       if: !(Fst (Fst (Fst "r")))
                       then !(Snd (Fst "r"))
                       else !(Snd (Fst (Fst "r"))) in
                    release "l";;
                    "v"
         , λ: "r" "x", let: "l" := (Snd "r") in
                       acquire "l";;
                       (if: !(Fst (Fst (Fst "r")))
                        then (Snd (Fst (Fst "r"))) <- "x";;
                             (Fst (Fst (Fst "r"))) <- #false
                        else (Snd (Fst "r")) <- "x";;
                             (Fst (Fst (Fst "r"))) <- #true);;
175 176 177 178 179 180 181
                       release "l").
Lemma cell2_typed Γ :
  typed Γ cell2 cellτ.
Proof.
  unfold cellτ. unlock cell2.
  solve_typed.
  econstructor.
182
  eapply TPack with (TProd (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))) (Tref TBool)).
183 184 185
  asimpl.
  econstructor; solve_typed.
  econstructor; solve_typed.
186 187 188 189
  econstructor; solve_typed.
  econstructor; solve_typed.
  econstructor; solve_typed.
  econstructor; solve_typed.
190
Qed.
191
Hint Resolve cell2_typed : typeable.
192 193

Section cell_refinement.
194
  Context `{logrelG Σ, lockG Σ}.
195 196
  Notation D := (prodC valC valC -n> iProp Σ).

197
  Definition lockR (R : D) (r1 r2 r3 r : loc) : iProp Σ :=
198
    ( (a b c : val), r ↦ₛ a  r2 ↦ᵢ b  r3 ↦ᵢ c 
199 200
     ( (r1 ↦ᵢ #true   R (c, a))
      (r1 ↦ᵢ #false   R (b, a))))%I.
201

202 203
  Definition cellInt (R : D) (r1 r2 r3 l r : loc) : iProp Σ :=
    ( γ N, is_lock N γ #l (lockR R r1 r2 r3 r))%I.
204

205 206 207
  Program Definition cellR (R : D) : D := λne vv,
    ( r1 r2 r3 l r : loc, vv.1 = (#r1, #r2, #r3, #l)%V  vv.2 = #r
      cellInt R r1 r2 r3 l r)%I.
208 209
  Next Obligation. solve_proper. Qed.

Dan Frumin's avatar
Dan Frumin committed
210
  Instance cellR_persistent R ww : Persistent (cellR R ww).
211 212 213 214 215 216 217 218
  Proof. apply _. Qed.

  Lemma cell2_cell1_refinement Γ :
    Γ  cell2 log cell1 : cellτ.
  Proof.
    iIntros (Δ).
    unlock cell2 cell1 cellτ.
    iApply bin_log_related_tlam; auto.
219
    iIntros (R) "!#".
220
    iApply (bin_log_related_pack (cellR R)).
221 222 223 224 225
    repeat iApply bin_log_related_pair.
    - (* New cell *)
      iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "/= #Hv".
      rel_let_l. rel_let_r.
226
      rel_alloc_r as r "Hr".
227 228 229
      rel_alloc_l as r1 "Hr1".
      rel_alloc_l as r2 "Hr2".
      rel_alloc_l as r3 "Hr3".
230 231 232 233 234 235 236 237
      pose (N:=logrelN.@(r1,r)).
      rel_apply_l (bin_log_related_newlock_l N (lockR R r1 r2 r3 r)%I with "[-]").
      { iExists _,_,_. iFrame.
        iRight. by iFrame. }
      iIntros (lk γl) "#Hlk".
      rel_vals. iModIntro. iAlways.
      iExists _,_,_,_,_. repeat iSplit; eauto.
      iExists _,_. by iFrame.
238 239 240
    - (* Read cell *)
      iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "/=".
241 242 243 244 245 246
      iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq.
      rel_let_l. rel_proj_l. rel_let_l.
      rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk".
      rel_apply_l (bin_log_related_acquire_l with "Hlk"); first auto.
      iIntros "Htok".
      rewrite /lockR. iDestruct 1 as (a b c) "(Hr & Hr2 & Hr3 & Hr1)".
247
      rel_let_l.
248 249 250 251 252
      repeat rel_proj_l.
      rel_let_r. rel_load_r.
      iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]";
        rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l.
      + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto.
253
        { iExists a,b,c; iFrame. iLeft; by iFrame. }
254
        rel_let_l. rel_vals; eauto.
255 256
      + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto.
        { iExists _,_,_; iFrame. iRight; by iFrame. }
257 258 259 260
        rel_let_l. rel_vals; eauto.
    - (* Insert cell *)
      iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "/=".
261
      iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq.
262 263 264
      rel_let_l. rel_let_r.
      iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "/= #Hv".
265 266 267 268 269 270 271 272 273 274 275 276 277 278
      rel_let_l. rel_proj_l. rel_let_l. rel_let_r.
      rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk".
      rel_apply_l (bin_log_related_acquire_l with "Hlk"); first auto.
      iIntros "Htok".
      rewrite /lockR. iDestruct 1 as (a b c) "(Hr & Hr2 & Hr3 & Hr1)".
      rel_let_l.
      repeat rel_proj_l.
      rel_store_r.
      iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]";
        rel_load_l; rel_if_l;
        repeat rel_proj_l; rel_store_l; rel_seq_l;
        repeat rel_proj_l; rel_store_l; rel_seq_l.
      + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto.
        { iExists _,_,_; iFrame. iRight; by iFrame. }
279
        iApply bin_log_related_unit.
280 281
      + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto.
        { iExists _,_,_; iFrame. iLeft; by iFrame. }
282 283 284
        iApply bin_log_related_unit.
    Qed.
End cell_refinement.