vectors.v 13.2 KB
Newer Older
Simon Spies's avatar
Simon Spies committed
1 2 3 4
From iris.heap_lang Require Export lifting metatheory.
From iris.heap_lang Require Import notation proofmode.
From iris_examples.logrel_heaplang Require Import ltyping ltyping_safety.
From iris.algebra Require Import gmap auth agree.
5
From iris_examples.logrel_heaplang.lib Require Import invariants arrays.
Simon Spies's avatar
Simon Spies committed
6 7 8

Set Default Proof Using "Type".

Simon Spies's avatar
nits  
Simon Spies committed
9 10
(* vec = ref array *)
Section Vectors.
Simon Spies's avatar
Simon Spies committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

  (* API *)
  Definition use : val :=
    λ: <> "a" "f" ,
    let: "b" := copy "a" (!"a") in
    let: "v" := ref "b" in "f" #() "v".

  Definition idx : val :=
    λ: <> "v" "i", if: ((#-1) < "i") && ("i" < !(!"v")) then SOME "i" else NONE.

  Definition get : val :=
    λ: <> "v" "i", unsafe_get (!"v") "i".

  Definition set : val :=
    λ: <> "v" "i" "x", (unsafe_set (!"v") "i") "x".
26

Simon Spies's avatar
Simon Spies committed
27 28 29 30 31 32 33
  Definition app : val :=
    λ: <> , rec: "f" "v" "x" :=
      let: "a" := !"v" in
      let: "b" := copy "a" (!"a" + #1) in
      "b" + !"a" + #1 <- "x";;
      if: CAS "v" "a" "b" then #() else "f" "v" "x".

Simon Spies's avatar
nits  
Simon Spies committed
34
  (* History *)
35 36 37 38 39
  Definition Hist := gmap loc nat.
  Definition HistUR  := gmapUR loc (agreeR (leibnizO nat)).
  Definition hist : Hist  HistUR := fmap (λ v: nat, to_agree (v : leibnizO nat)).
  Implicit Types (h : Hist) (a: loc).

Simon Spies's avatar
Simon Spies committed
40 41
  Context `{!heapG Σ,
            !inG Σ (authR mnatUR), (* maximum length *)
42
            !inG Σ (authR HistUR) (* history *)
Simon Spies's avatar
Simon Spies committed
43
           }.
Simon Spies's avatar
nits  
Simon Spies committed
44
  Variable (N: namespace).
Simon Spies's avatar
Simon Spies committed
45 46 47 48

  (* Maximum Length *)
  Global Instance auth_mnat_persistent (n: mnat) γ: Persistent (own γ ( n)).
  Proof.
49
    eapply own_core_persistent, auth_frag_core_id, mnat_core_id.
Simon Spies's avatar
Simon Spies committed
50
  Qed.
51

Simon Spies's avatar
Simon Spies committed
52 53 54 55
  Lemma auth_mnat_alloc (n: mnat) :
    (|==>  γ, own γ ( n)  own γ ( n))%I.
  Proof.
    iMod (own_alloc ( n   n)) as (γ) "[??]". eapply auth_both_valid_2; done.
56
    eauto with iFrame.
Simon Spies's avatar
Simon Spies committed
57 58 59
  Qed.

  Lemma auth_mnat_agree γ (m n : mnat):
Simon Spies's avatar
nits  
Simon Spies committed
60
    own γ ( m) - own γ ( n) - n  m.
Simon Spies's avatar
Simon Spies committed
61
  Proof.
62
    iIntros "Hγ● Hγ◯".
Simon Spies's avatar
Simon Spies committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76
    iDestruct (own_valid_2 with "Hγ● Hγ◯") as "%".
    eapply auth_both_valid in H as [H _].
    iPureIntro. eapply mnat_included in H. lia.
  Qed.

  Lemma auth_mnat_fork γ (n: mnat):
    own γ ( n)  ==  own γ ( n)  own γ ( n).
  Proof.
    iIntros "H".
    iMod (own_update _ _ ( n   n) with "H") as "[$$]"; eauto.
    apply auth_update_alloc. now eapply mnat_local_update.
  Qed.

  Lemma auth_mnat_previous γ (n m: mnat):
Simon Spies's avatar
nits  
Simon Spies committed
77
    n  m  own γ ( m) - own γ ( n).
Simon Spies's avatar
Simon Spies committed
78 79 80
  Proof.
    intros H. eapply own_mono. eapply (auth_frag_mono n m), mnat_included. lia.
  Qed.
81

Simon Spies's avatar
Simon Spies committed
82
  Lemma auth_mnat_update γ (n p: mnat):
Simon Spies's avatar
nits  
Simon Spies committed
83
    n  p  own γ ( n) == own γ ( p).
Simon Spies's avatar
Simon Spies committed
84 85
  Proof.
    iIntros (H) "Hγ●".
86
    iMod (auth_mnat_fork with "Hγ●") as "[Hγ● Hγ◯]"; eauto.
Simon Spies's avatar
Simon Spies committed
87 88 89 90 91 92 93 94
    iMod (own_update_2 _ _ _ ( p   p) with "Hγ● Hγ◯") as "[$ _]"; eauto.
    eapply auth_update, mnat_local_update; lia.
  Qed.

  Section hist.
    (** Conversion to hists and back *)
    Lemma hist_valid h :  hist h.
    Proof. intros l. rewrite lookup_fmap. by case (h !! l). Qed.
95

Simon Spies's avatar
Simon Spies committed
96 97
    Lemma lookup_hist_None h a : h !! a = None  hist h !! a = None.
    Proof. by rewrite /hist lookup_fmap=> ->. Qed.
98

Simon Spies's avatar
Simon Spies committed
99 100 101 102
    Lemma hist_singleton_included h a m :
      {[a := to_agree m]}  hist h  h !! a = Some m.
    Proof.
      rewrite singleton_included=>  -[a' []].
103
      rewrite /hist lookup_fmap fmap_Some_equiv => -[m' [-> H]]. rewrite H.
Simon Spies's avatar
Simon Spies committed
104 105
      move=> /Some_included_total /to_agree_included /leibniz_equiv_iff -> //.
    Qed.
106

Simon Spies's avatar
Simon Spies committed
107
    Lemma hist_insert h a m :
108
      hist (<[a:=m]> h) = <[a:= to_agree (m: leibnizO nat)]> (hist h).
Simon Spies's avatar
Simon Spies committed
109
    Proof. by rewrite /hist fmap_insert. Qed.
110

Simon Spies's avatar
Simon Spies committed
111 112 113 114 115
    Lemma hist_delete a h :
      hist (delete a h) = delete a (hist h).
    Proof. by rewrite /hist fmap_delete. Qed.
  End hist.

116
  Definition hist_all γ h : iProp Σ := (own γ ( (hist h)))%I.
Simon Spies's avatar
Simon Spies committed
117
  Definition hist_entry γ a m : iProp Σ :=
118 119
    (own γ ( {[ a := to_agree (m : leibnizO nat)]}))%I.

Simon Spies's avatar
Simon Spies committed
120 121
  Global Instance hist_persistent a m γ: Persistent (hist_entry γ a m).
  Proof. eapply _. Qed.
122

Simon Spies's avatar
Simon Spies committed
123 124 125
  Lemma hist_alloc: (|==>  γ, hist_all γ )%I.
  Proof.
    iMod (own_alloc ( (hist ))) as (γ) "H".
126
    eapply auth_auth_valid, hist_valid.
Simon Spies's avatar
Simon Spies committed
127 128 129 130
    eauto with iFrame.
  Qed.

  Lemma hist_update γ h a m:
Simon Spies's avatar
nits  
Simon Spies committed
131
    (h !! a = None) 
Simon Spies's avatar
Simon Spies committed
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
    hist_all γ h == hist_all γ (<[a := m]> h)  hist_entry γ a m.
  Proof.
    intros H. iIntros "Hγ●".
    iMod (own_update _ _ _ with "Hγ●") as "H"; eauto.
    2: iModIntro; iDestruct "H" as "[H1 H2]"; iFrame "H1"; eauto.
    rewrite hist_insert. eapply auth_update_alloc.
    eapply alloc_singleton_local_update.
    now eapply lookup_hist_None. done.
  Qed.

  Lemma entry_agree γ a m n: hist_entry γ a m - hist_entry γ a n - m = n.
  Proof.
    apply bi.wand_intro_r.
    rewrite -own_op -auth_frag_op own_valid uPred.discrete_valid.
    f_equiv. rewrite auth_frag_valid /=. rewrite op_singleton singleton_valid.
      by intros ?%agree_op_invL'.
  Qed.
149

Simon Spies's avatar
Simon Spies committed
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
  Lemma hist_agree γ h a m:
    hist_all γ h - hist_entry γ a m - h !! a = Some m.
  Proof.
    iIntros "Hh Ha". rewrite /hist_all /hist_entry.
    iDestruct (own_valid_2 with "Hh Ha") as %H.
    eapply auth_both_valid in H as [H _].
    now eapply hist_singleton_included in H.
  Qed.

  Definition Vec_inv γ1 γ2 (l: loc) : iProp Σ :=
    (  (h: Hist) (a: loc) (m: mnat),
        l  #a 
        own γ1 ( m) 
        hist_all γ2 h 
        hist_entry γ2 a m 
        [ map] a  m  h, array (Z.of_nat m) a)%I.

  Definition Vec γ1 γ2 l := inv N (Vec_inv γ1 γ2 l).
  Definition Idx (γ1: gname) (i: mnat) := own γ1 ( (S i: mnat)).

  Lemma Vec_project_array γ1 γ2 a m l:
171
    hist_entry γ2 a m - Vec γ1 γ2 l - inv N (array m a).
Simon Spies's avatar
Simon Spies committed
172
  Proof.
173 174
    iIntros "#E #V". iApply inv_acc; eauto.
    iNext. iModIntro. iDestruct 1 as (h b n) "(Hl & Hγ1● & Hγ2● & Hγ2◯ & Hst)".
Simon Spies's avatar
Simon Spies committed
175 176 177 178 179 180
    iAssert (h !! a = Some m)%I with "[Hγ2●]" as "#H".
    { iApply (hist_agree with "[Hγ2●]"); eauto. }
    iAssert ((array m a  (array m a - [ map] a  m  h, array (Z.of_nat m) a)))%I
      with "[Hst]" as "(Ha & Hst)".
    { iDestruct "H" as %H1.
      now iApply (big_sepM_lookup_acc with "Hst").  }
181
    iFrame. iIntros "Ha".
Simon Spies's avatar
Simon Spies committed
182 183 184 185 186
    iExists h, b, n. iFrame. now iApply "Hst".
  Qed.

  (* Function Verification *)
  Definition ι γ1 γ2 : val := PairV (#(Z.pos γ1)) (#(Z.pos γ2)).
Simon Spies's avatar
nits  
Simon Spies committed
187
  Definition β γ1 γ2 : lty Σ := Lty (λ v, v = ι γ1 γ2)%I.
Simon Spies's avatar
Simon Spies committed
188
  Definition Index (S: lty Σ) : lty Σ :=
Simon Spies's avatar
nits  
Simon Spies committed
189
    Lty (λ v, (  γ1 γ2 (i: mnat), ( v, S v - β γ1 γ2 v)  v = #i  Idx γ1 i)%I).
Simon Spies's avatar
Simon Spies committed
190
  Definition Vector (S: lty Σ) : lty Σ :=
Simon Spies's avatar
nits  
Simon Spies committed
191
    Lty (λ v, (  γ1 γ2 (l: loc), ( v, S v - β γ1 γ2 v)   v = #l  Vec γ1 γ2 l)%I).
192

Simon Spies's avatar
Simon Spies committed
193
  Lemma typing_use:   use :  T,  Array N  ( S, Vector S  T)  T.
194 195
  Proof. unfold use.
    iIntros (s) "!# #T /=".
Simon Spies's avatar
Simon Spies committed
196
    iApply wp_value.
197
    iIntros (S) "!#". wp_pures.
Simon Spies's avatar
Simon Spies committed
198 199
    iIntros (v1) "!# #Array". wp_pures.
    iIntros (v2) "!# #Cont". wp_pures.
200 201 202
    iDestruct "Array" as (a m) "[Array ->]".
    wp_bind (! #a)%E. iPoseProof (array_length_inv with "Array") as "L".
    iInv "L" as "Ha" "Hclose". wp_load. iMod ("Hclose" with "Ha") as "_".
Simon Spies's avatar
Simon Spies committed
203 204 205 206 207
    iModIntro. wp_apply (copy_spec); eauto with lia.
    iIntros (b) "B". wp_pures.
    wp_bind (ref _)%E. wp_apply wp_fupd. wp_alloc l as "Hl".
    iMod (auth_mnat_alloc m) as (γ1) "[Hγ1● _]".
    iMod (hist_alloc) as (γ2) "Hγ2●".
208
    iMod (hist_update γ2  b m with "[Hγ2●]") as "[Hγ2● #Hγ2◯]"; eauto.
Simon Spies's avatar
Simon Spies committed
209 210 211 212 213 214 215 216 217 218 219 220 221
    iMod (inv_alloc N _ (Vec_inv γ1 γ2 l) with "[Hγ1● Hγ2● Hl B]") as "#I".
    - iNext. iExists {[ b := m ]}, b, m. iFrame. iSplit; eauto.
      now rewrite big_sepM_singleton.
    - iModIntro. wp_pures. iSpecialize ("Cont" $! (β γ1 γ2)).
      wp_bind (v2 _). wp_apply (wp_wand with "Cont").
      iIntros (v) "#H". wp_apply ("H"). iModIntro.
      iExists γ1, γ2, l. repeat iSplit; eauto.
  Qed.

  Lemma typing_idx:   idx : ( S, Vector S  lty_int  Option (Index S)).
  Proof. unfold idx.
    iIntros (s) "!# T /=". iApply wp_value.
    iIntros (S) "!#". wp_pures.
222
    iIntros (v1) "!# #Vec". wp_pures.
Simon Spies's avatar
Simon Spies committed
223
    iIntros (v2) "!# #Int". wp_pures.
224
    iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)".
Simon Spies's avatar
Simon Spies committed
225 226 227 228 229 230 231
    iDestruct "Int" as (n) "->". wp_pures.
    bool_decide H; last (wp_pures; now iLeft).
    wp_pures. wp_bind (! #l)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose".
    wp_load. iMod (auth_mnat_fork with "H2") as "[H2 #Hi]".
    iMod("Hclose" with "[H1 H2 H3 H4]") as "_".
    iNext; iExists h, a, m; iFrame; eauto.
    iModIntro. iPoseProof (Vec_project_array with "Ha V") as "I".
232 233 234
    wp_bind (! _)%E. iPoseProof (array_length_inv with "I") as "L".
    iInv "L" as "H" "Hclose". wp_load. iMod ("Hclose" with "H") as "_".
    iModIntro. wp_pures.
Simon Spies's avatar
Simon Spies committed
235 236 237 238 239
    bool_decide H'; last (wp_pures; now iLeft).
    wp_pures. iRight. iExists #n. iSplit; eauto.
    destruct (Z_to_nat n) as [k ->]; first lia.
    iExists γ1, γ2, k.
    iModIntro. repeat iSplit; eauto.
240
    iApply auth_mnat_previous; eauto. lia.
Simon Spies's avatar
Simon Spies committed
241 242 243 244 245 246
  Qed.

  Lemma typing_get:   get : ( S, Vector S  Index S  lty_int).
  Proof. unfold get.
    iIntros (s) "!# T /=". iApply wp_value.
    iIntros (S) "!#". wp_pures.
247
    iIntros (v1) "!# #Vec". wp_pures.
Simon Spies's avatar
Simon Spies committed
248
    iIntros (v2) "!# #Idx". wp_pures.
249
    iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)".
Simon Spies's avatar
Simon Spies committed
250 251 252
    iDestruct "Idx" as (γ1' γ2' i) "(EQ' & -> & I)".
    iAssert (β γ1 γ2 (ι γ1' γ2'))%I as "%".
    { iApply "EQ". iApply "EQ'". now iPureIntro. }
253
    injection H as -> ->.
Simon Spies's avatar
Simon Spies committed
254 255
    wp_bind (! _)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose".
    wp_load. iDestruct (auth_mnat_agree with "H2 I") as %H.
256
    iMod("Hclose" with "[H1 H2 H3 H4]") as "_".
Simon Spies's avatar
Simon Spies committed
257 258
    iNext; iExists h, a, m; iFrame; eauto.
    iModIntro. wp_apply (unsafe_get_spec); eauto. iSplit.
259
    iApply Vec_project_array; eauto. iPureIntro; lia.
Simon Spies's avatar
Simon Spies committed
260 261 262 263 264 265
  Qed.

  Lemma typing_set:   set : ( S, Vector S  Index S  lty_int  lty_unit).
  Proof. unfold set.
    iIntros (s) "!# T /=". iApply wp_value.
    iIntros (S) "!#". wp_pures.
266
    iIntros (v1) "!# #Vec". wp_pures.
Simon Spies's avatar
Simon Spies committed
267
    iIntros (v2) "!# #Idx". wp_pures.
268 269
    iIntros (v3) "!# #Int". wp_pures.
    iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)".
Simon Spies's avatar
Simon Spies committed
270 271 272 273
    iDestruct "Idx" as (γ1' γ2' i) "(EQ' & -> & I)".
    iDestruct "Int" as (n) "->".
    iAssert (β γ1 γ2 (ι γ1' γ2'))%I as "%".
    { iApply "EQ". iApply "EQ'". now iPureIntro. }
274
    injection H as -> ->.
Simon Spies's avatar
Simon Spies committed
275 276
    wp_bind (! _)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose".
    wp_load. iDestruct (auth_mnat_agree with "H2 I") as %H.
277
    iMod("Hclose" with "[H1 H2 H3 H4]") as "_".
Simon Spies's avatar
Simon Spies committed
278 279
    iNext; iExists h, a, m; iFrame; eauto.
    iModIntro. wp_apply (unsafe_set_spec); eauto. iSplit.
280
    iApply Vec_project_array; eauto. iPureIntro; lia.
Simon Spies's avatar
Simon Spies committed
281 282 283 284 285
  Qed.

  Lemma typing_app:   app : ( S, Vector S  lty_int  lty_unit).
  Proof.
    iIntros (s) "!# #T /=".
286
     unfold app.
Simon Spies's avatar
Simon Spies committed
287 288
    iApply wp_value.
    iIntros (S) "!#". wp_pures.
289
    iIntros (v1) "!# #Vec". wp_pures.
Simon Spies's avatar
Simon Spies committed
290 291
    iIntros (v2) "!# #Int". wp_pures. fold app.
    iLöb as "IH" forall (v1 v2) "Vec Int".
292
    iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & Vec)".
Simon Spies's avatar
Simon Spies committed
293 294 295 296
    iDestruct "Int" as (n) "->".
    wp_bind (! #l)%E.
    iInv "Vec" as (h a m) "(Hl & Hγ1● & Hγ2 & #Ha & Hst)" "Hclose". wp_load.
    iMod ("Hclose" with "[Hl Hγ1● Hγ2 Hst]") as "_". iNext.  iExists h, a, m. iFrame; eauto.
297 298 299
    clear h. iModIntro. iPoseProof (Vec_project_array with "Ha Vec") as "#HA".
    wp_pures. wp_bind (! #a)%E. iPoseProof (array_length_inv with "HA") as "L".
    iInv "L" as "H" "Hclose". wp_load. iMod ("Hclose" with "H") as "_".
Simon Spies's avatar
Simon Spies committed
300 301 302
    iModIntro. wp_pures.
    wp_apply (copy_spec with "[]"); first eauto with lia.
    iIntros (b) "A". wp_pures.
303 304 305 306 307
    wp_bind (! #a)%E. iInv "L" as "Hb" "Hclose". wp_load.
    iMod("Hclose" with "Hb") as "_". iModIntro. wp_pures.
    iPoseProof (array_entry_acc m with "[] A") as "[E A]"; first (iPureIntro; lia).
    iDestruct "E" as (v) "E". wp_store. iSpecialize ("A" with "[E]"); first by iExists _.
    wp_bind (CmpXchg _ _ _).
Simon Spies's avatar
Simon Spies committed
308
    iInv "Vec" as (h a' m') "(Hl & Hγ1● & Hγ2 & #Ha' & Hst)" "Hclose".
309
    wp_cmpxchg as H|H.
Simon Spies's avatar
Simon Spies committed
310 311
    - injection H as ?; subst.
      iPoseProof (entry_agree with "Ha Ha'") as "%"; subst m'.
312 313 314 315 316 317 318
      iMod (auth_mnat_update _ _ (m + 1)%nat with "Hγ1●") as "Hγ1●"; try lia.
      iAssert (h !! b = None)%I with "[A Hst]" as "%".
      { destruct (h !! b) eqn: H; eauto.
        iPoseProof (big_sepM_insert_acc with "Hst") as "[Hst _]"; eauto.
        iPoseProof (array_length_acc with "A") as "[H1 _]".
        iPoseProof (array_length_acc with "Hst") as "[H2 _]".
        iPoseProof (mapsto_valid_2 with "H1 H2") as "%". exfalso.
Simon Spies's avatar
Simon Spies committed
319 320
        destruct (frac.frac_valid' 2%Qp) as [H1 _]. eapply H1 in H0.
        now eapply Qp_not_plus_q_ge_1 in H0. }
321 322
      iMod (hist_update _ _ _ (m + 1)%nat with "Hγ2") as "[Hγ2 #Hb_ent]"; eauto.
      iMod ("Hclose" with "[Hl Hγ1● Hγ2 A Hst]") as "_".
Simon Spies's avatar
Simon Spies committed
323 324 325
      iNext. iExists (<[b:=(m + 1)%nat]> h), b, ((m + 1)%nat). iFrame.
      iSplit; eauto. rewrite big_sepM_insert; eauto; iFrame.
      replace ((m + 1)%nat : Z) with (m + 1) by lia.
326 327
      iFrame. iModIntro. wp_pures. done.
    - iMod ("Hclose" with "[Hl Hγ1● Hγ2 A Hst]") as "_".
Simon Spies's avatar
Simon Spies committed
328 329 330
      iNext. iExists h, a', m'. iFrame; eauto.
      iModIntro. wp_pures.
      iApply "IH". iModIntro. iExists γ1, γ2, l. repeat iSplit; eauto.
331
      iModIntro. iExists n. done.
Simon Spies's avatar
Simon Spies committed
332
  Qed.
333
End Vectors.