bounded_queue.v 56.3 KB
Newer Older
Glen Mével's avatar
Glen Mével committed
1
From iris.algebra Require Import excl_auth csum numbers list.
Glen Mével's avatar
Glen Mével committed
2
From iris.base_logic Require Import invariants.
3
4
From cosmo.base Require Import base Zlist lattice_cmra.
From cosmo.program_logic Require Export proofmode atomic.
Glen Mével's avatar
Glen Mével committed
5
6
7
8

Set Default Proof Using "Type".
Open Scope Z.

Glen Mével's avatar
Glen Mével committed
9
(* TODO:
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
10
  - add multiplication, division, modulo to the core language
Glen Mével's avatar
Glen Mével committed
11
12
*)

Glen Mével's avatar
Glen Mével committed
13
14
15
16
(** Implementation **)

Section bounded_queue.

17
Context (capacity : nat) (capacity_min : capacity  1).
Glen Mével's avatar
Glen Mével committed
18

Glen Mével's avatar
Glen Mével committed
19
20
Definition init_array (α : atomicity) : val := λ: "n" "f",
  let: "a" := Alloc α "n" #() in
Glen Mével's avatar
Glen Mével committed
21
22
  (rec: "loop" "i" :=
    if: "n"  "i" then "a" else (
Glen Mével's avatar
Glen Mével committed
23
      Write α "a" "i" ("f" "i") ;;
Glen Mével's avatar
Glen Mével committed
24
25
26
27
28
      "loop" ("i" + #1)
    )
  ) #0.

Axiom modulo : val.
29
Axiom modulo_spec :  `{cosmoG Σ} (n m : Z),
Glen Mével's avatar
Glen Mével committed
30
   (Φ : val  vProp Σ), Φ #(n mod m) - WP modulo #n #m {{ Φ }}.
Glen Mével's avatar
Glen Mével committed
31

32
33
(*
   ICFP21: Below follows the implementation, in our toy deep-embedded language,
34
   of the bounded queue with a circular buffer. It corresponds to Figure 8 of
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
   the paper. capacity is a non-zero integer constant.
   
   It is worth noting that the toy language is untyped. This code, in particular,
   does not typecheck, because it uses the unit value as a dummy element for
   filling cells in the queue, regardless of the intended type for elements of
   the queue. To make it typecheck, assuming it was actual OCaml code, there
   would be a number of options:
    (1) store option values in the queue: that implies a significant overhead
        (when allocating the boxes and when reading these extra indirections);
    (2) when creating the queue, ask the user for an arbitrary inhabitant of the
        element type, just for the sake of using it as a dummy value internally:
        that is odd from the user perspective, and requires storing the dummy as
        an additional field in the data structure);
    (3) use unsafe OCaml features to evade the type system (i.e. Obj.magic).
 *)

Glen Mével's avatar
Glen Mével committed
51
52
Definition make : val := λ: <>,
  let: "elements" := Alloc NonAtomic #capacity #() in
Glen Mével's avatar
Glen Mével committed
53
  let: "statuses" := init_array Atomic #capacity (λ: "i", "i"+"i") in
Glen Mével's avatar
Glen Mével committed
54
55
56
57
58
59
60
61
62
  let: "tail" := ref_at #0 in
  let: "head" := ref_at #0 in
  ("tail", "head", "statuses", "elements").

Definition try_enqueue : val := λ: "q" "x",
  let: ("tail", "head", "statuses", "elements") := "q" in
  let: "h" := !at "head" in
  let: "hmod" := modulo "h" #capacity in
  let: "s" := Read Atomic "statuses" "hmod" in
63
  if: ("s" = "h"+"h") && CAS_ref "head" "h" ("h" + #1) then (
Glen Mével's avatar
Glen Mével committed
64
    Write NonAtomic "elements" "hmod" "x" ;;
65
    Write Atomic "statuses" "hmod" ("s" + #1) ;;
Glen Mével's avatar
Glen Mével committed
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
    #true
  )
  else
    #false.

Definition enqueue : val := rec: "enqueue" "q" "x" :=
  if: try_enqueue "q" "x" then
    #()
  else
    "enqueue" "q" "x".

Definition try_dequeue : val := λ: "q",
  let: ("tail", "head", "statuses", "elements") := "q" in
  let: "t" := !at "tail" in
  let: "tmod" := modulo "t" #capacity in
  let: "s" := Read Atomic "statuses" "tmod" in
82
  if: ("s" = "t"+"t" + #1) && CAS_ref "tail" "t" ("t" + #1) then (
Glen Mével's avatar
Glen Mével committed
83
84
    let: "x" := Read NonAtomic "elements" "tmod" in
    Write NonAtomic "elements" "tmod" #() ;; (* optional, useful for GC *)
85
    Write Atomic "statuses" "tmod" ("t"+"t" + #capacity+#capacity) ;;
Glen Mével's avatar
Glen Mével committed
86
87
88
89
90
91
92
93
94
95
96
97
98
    SOME "x"
  )
  else
    NONEV.

Definition dequeue : val := rec: "dequeue" "q" :=
  match: try_dequeue "q" with
    SOME "x" => "x"
  | NONE     => "dequeue" "q"
  end.

(** Specification **)

99
100
(* ICFP21: Here is the construction of the lattice described by the paper in
   Section 4.3 Monotonicity of statuses. *)
Glen Mével's avatar
Glen Mével committed
101
102
103
104
105
(* Here we define a lattice structure for pairs Z × view, equipped with the
   lexicographic order where the order on views is flipped. This serves to
   express the monotonicity of statuses: the status for a given index only
   grows AND, as long as it has not grown, the view stored in this atomic
   location has not grown either. *)
Glen Mével's avatar
Glen Mével committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
Section lexico.
  Inductive statuspair : Type := StatusPair { statuspair_s : Z ; statuspair_V : view }.
  (** Lattice for statuspair *)
  Definition statuspair_le '(StatusPair s1 V1) '(StatusPair s2 V2) : Prop :=
    s1 < s2  (s1 = s2  V2  V1).
  Program Canonical Structure statuspair_Lat :=
    Make_Lat statuspair (=) statuspair_le
             (λ '(StatusPair s1 V1) '(StatusPair s2 V2),
                if decide (s1 < s2) then StatusPair s2 V2
                else if decide (s2 < s1) then StatusPair s1 V1
                else StatusPair s1 (V1  V2) )
             (λ '(StatusPair s1 V1) '(StatusPair s2 V2),
                if decide (s1 < s2) then StatusPair s1 V1
                else if decide (s2 < s1) then StatusPair s2 V2
                else StatusPair s1 (V1  V2) )
             _ _ _ _ _ _ _ _ _ _ _ _ _.
  Next Obligation. exact (populate $ StatusPair 0 ). Qed.
  Next Obligation.
    exists.
    - intros [s V]. by right.
    - intros [s1 V1][s2 V2][s3 V3] [? | [??]] [? | [??]] ; [left ; lia ..|].
      right. split ; by etrans.
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2] [? | [??]] [? | [??]] ; [exfalso ; lia ..|].
    f_equal ; solve_lat.
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2]. rewrite /sqsubseteq/join/=.
    case_decide ; [by left|]. case_decide ; [by right|]. right. split ; solve_lat.
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2]. rewrite /sqsubseteq/join/=.
    case_decide ; [by right|]. case_decide ; [by left|]. right. split ; [lia|solve_lat].
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2][s3 V3] [? | [??]] [? | [??]].
    all: cbn ; case_decide ; [|case_decide] ; first [by left | by right|idtac].
    all: right ; split ; [done|].
    - exfalso. lia.
    - solve_lat.
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2]. rewrite /sqsubseteq/meet/=.
    case_decide ; [by right|]. case_decide ; [by left|]. right. split ; solve_lat.
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2]. rewrite /sqsubseteq/meet/=.
    case_decide ; [by left|]. case_decide ; [by right|]. right. split ; [lia|solve_lat].
  Qed.
  Next Obligation.
    intros [s1 V1][s2 V2][s3 V3] [? | [??]] [? | [??]].
    all: cbn ; case_decide ; [|case_decide] ; first [by left | by right|idtac].
    all: right ; split ; [done|].
    - exfalso. lia.
    - by apply lat_join_lub.
  Qed.

  Instance statuspair_leibnizequiv : LeibnizEquiv statuspair := λ _ _ H, H.

  Instance statuspair_sqsubseteq_decision : RelDecision (@sqsubseteq statuspair _).
  Proof.
    intros [s1 V1][s2 V2].
    destruct (decide (s1 < s2)) ; first (left ; by left).
    destruct (decide (s2 < s1)) ; first (right ; intros [? | [? _]] ; lia).
    destruct (decide (V2  V1)) ; first (left ; right ; split ; [lia|done]).
    right. by intros [? | [_ ?]].
  Qed.

  Lemma statuspair_le_Z_le (sV1 sV2 : statuspair) :
    sV1  sV2  statuspair_s sV1  statuspair_s sV2.
  Proof. destruct sV1, sV2. intros [? | [? _]] ; cbn ; lia. Qed.
End lexico.

180
181
182
183
(* ICFP21: The typeclass queueG describes which CMRAs we need for specifying
   the data structure. In fact, the Iris framework is parameterized by a single,
   very large product CMRA named Σ, so we require this large product to include
   at least the desired CMRAs. *)
Glen Mével's avatar
Glen Mével committed
184
Class queueG Σ := {
Glen Mével's avatar
Glen Mével committed
185
  (* public state *)
Glen Mével's avatar
Glen Mével committed
186
  queueG_G :> inG Σ (excl_authUR (prodO (prodO
Glen Mével's avatar
Glen Mével committed
187
    (* view of writers *)
Glen Mével's avatar
Glen Mével committed
188
      viewO
Glen Mével's avatar
Glen Mével committed
189
    (* view of readers *)
Glen Mével's avatar
Glen Mével committed
190
      viewO )
Glen Mével's avatar
Glen Mével committed
191
    (* values in the queue, with associated views *)
Glen Mével's avatar
Glen Mével committed
192
193
      (listO valViewO) )
  ) ;
194
  (* tokens for readers (no payload) and writers (a value and a view) *)
195
  queueG_tokensG :> inG Σ (authUR $ listUR $ optionUR $ csumR (exclR unitO) (exclR valViewO)) ;
Glen Mével's avatar
Glen Mével committed
196
  (* monotonicity of statuses *)
Glen Mével's avatar
Glen Mével committed
197
  queueG_mono_statusesG :> inG Σ (listUR $ authUR $ latUR (option_Lat statuspair_Lat)) ;
Glen Mével's avatar
Glen Mével committed
198
199
200
201
}.

Section Spec.

202
  Context `{!cosmoG Σ, !queueG Σ}.
Glen Mével's avatar
Glen Mével committed
203

Glen Mével's avatar
Glen Mével committed
204
  Implicit Types (q : val) (tail head statuses elements : location).
205
  Implicit Types (γ γtoks γmonos : gname) (V Vt Vh : view).
Glen Mével's avatar
Glen Mével committed
206
  Implicit Types (x dummy : val) (xV : val * view) (xVs : list (val * view)).
Glen Mével's avatar
Glen Mével committed
207
  Implicit Types (s : Z) (sV : Z * view) (sVs : list (Z * view)).
Glen Mével's avatar
Glen Mével committed
208
209
210
211
  Implicit Types (t h i tmod hmod imod : Z).

  Open Scope Z.

Glen Mével's avatar
Glen Mével committed
212
213
  Notation "⌊ z ⌋" := (Z.to_nat z).
  Notation "x -- y" := (Z.sub x%Z y%Z) (at level 50, left associativity).
214
  (* NOTE: Coq defines Zlength as a recursive function. *)
Glen Mével's avatar
Glen Mével committed
215
216
  Notation Zlength ls := (Z.of_nat (length ls)) (only parsing).

217
  (* ICFP21: This is the definition of the ghost state representing slot tokens
218
     (Section 4.5 and Figure 9d of the paper).
219
220
221
     Whereas the paper uses finite maps over Z, here we model them using lists.
     There isnt really a technical advantage in doing so, to be honest, and it
     requires careful shifting so that no negative index is involved. *)
222
223
224
225
226
227
  Definition token_read γtoks i : iProp Σ :=
    own γtoks ( {[ i + capacity := Some $ Cinl $ Excl () ]}).
  Definition token_write γtoks i xV : iProp Σ :=
    own γtoks ( {[ i := Some $ Cinr $ Excl xV ]}).
  Definition tokens_auth γtoks t h xVs : iProp Σ :=
    own γtoks ( (
228
229
230
      replicate t None                                      (* 0 .. t          ; length = t   *)
      ++ ((λ xV, Some $ Cinr $ Excl xV) <$> xVs)              (* t .. h          ; length = h-t *)
      ++ replicate t--(h--capacity) (Some $ Cinl $ Excl ()) (* h .. t+capacity ; length = t-(h-capacity) *)
Glen Mével's avatar
Glen Mével committed
231
232
    )).

233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
(* TODO: merge this into Iris *)
  Lemma list_lookup_local_update {A : ucmraT} (l l' : list A) (i : nat) (x x' y y' : A) :
    l !! i  Some x 
    l'  <[i := y]> l 
    (x, x') ~l~> (y, y') 
    (l, {[i := x']})  ~l~>  (l', {[i := y']}).
  Proof. clear.
    move=> Hlookup -> Hxy n lo /= Hvalidl Hdistl.
    rewrite ->(list_dist_lookup (A:=A)) in Hdistl.
    case: (Hxy n (lo = lookup i)) => /= [||Hvalidy Hdisty].
    { by eapply list_lookup_validN_Some, equiv_dist. }
    { specialize (Hdistl i). revert Hdistl.
      rewrite list_lookup_opM list_lookup_singletonM Hlookup.
      case: (lo = lookup i) => [?|] ; intros ?%(inj Some) ; rewrite ?right_id //. }
    assert (i < length l)%nat.
    { destruct (l !! i) eqn:? ; by [eapply lookup_lt_Some | inversion Hlookup]. }
    split.
    { apply list_lookup_validN => j.
      destruct (decide (i = j)) as [<- | Hne].
      - rewrite list_lookup_insert //.
      - rewrite list_lookup_insert_ne //. by apply list_lookup_validN. }
    { apply list_dist_lookup => j.
      specialize (Hdistl j). revert Hdistl. rewrite 2!list_lookup_opM.
      destruct (lt_eq_lt_dec i j) as [[ Hij | <- ]| Hji ].
      - rewrite 2?list_lookup_singletonM_gt // list_lookup_insert_ne //. lia.
      - rewrite 2!list_lookup_singletonM list_lookup_insert // Hdisty.
        by case: (lo = lookup i).
      - rewrite 2?list_lookup_singletonM_lt // list_lookup_insert_ne //. lia. }
  Qed.

(* TODO: merge this into Iris *)
  Lemma list_middle_local_update {A : ucmraT} (l1 l2 : list A) (x x' y y' : A) :
    (x, x') ~l~> (y, y') 
    (l1 ++ x :: l2, {[length l1 := x']})  ~l~>  (l1 ++ y :: l2, {[length l1 := y']}).
  Proof. clear.
    intros ?. eapply list_lookup_local_update ; last done.
    - rewrite lookup_app_r // Nat.sub_diag //=.
    - rewrite insert_app_r_alt // Nat.sub_diag //=.
  Qed.

273
274
275
  (* ICFP21: The lemmas below correspond to properties of the tokens. They are
     more specific than the properties shown in Figure 10c of the paper. *)

276
  Lemma own_token_list_read γtoks t h xVs i :
Glen Mével's avatar
Glen Mével committed
277
278
279
    0  t 
    -capacity  i 
    Z.of_nat $ length xVs = h -- t 
280
281
    tokens_auth γtoks t h xVs -
    token_read γtoks i -
282
    h -- capacity  i < t.
Glen Mével's avatar
Glen Mével committed
283
  Proof. clear.
284
    iIntros (???) "H● H◯". iCombine "H● H◯" as "H". rewrite own_valid.
Glen Mével's avatar
Glen Mével committed
285
286
287
288
289
290
291
292
293
    iDestruct "H" as %Hvalid. iPureIntro.
    apply auth_both_valid_discrete in Hvalid as [Hle Hvalid].
    apply list_singletonM_included in Hle as (otok & Hlookup & Hle).
    apply option_included in Hle as [ |(? & tok & [=<-] & -> & Hle)] ; first discriminate.
    destruct Hle as [ <-%leibniz_equiv | Hle ].
    { apply lookup_app_Some in Hlookup as [Hlookup|[Hineq1 Hlookup]] ; last
      apply lookup_app_Some in Hlookup as [Hlookup|[Hineq2 Hlookup]].
      - by apply lookup_replicate in Hlookup as [[=] _].
      - by apply list_lookup_fmap_inv in Hlookup as (? & [=] & _).
294
      - apply lookup_replicate in Hlookup as [_ Hlookup].
Glen Mével's avatar
Glen Mével committed
295
296
297
298
        rewrite replicate_length fmap_length in Hineq1 Hineq2 Hlookup.
        rewrite (_ : (i + capacity - t - length xVs)%nat
                    = i -- (h -- capacity)) in Hlookup ;
          last lia.
299
        lia. }
Glen Mével's avatar
Glen Mével committed
300
301
302
303
304
305
306
307
308
309
    exfalso.
    apply leibniz_equiv_iff in Hlookup.
    apply csum_included in Hle
      as [   ->
         |[ (? & ? & [=<-] & -> & e' & ->%leibniz_equiv)
          | (? & _ & [=]   & _)
         ]] ;
      [|] ; by destruct (list_lookup_valid_Some _ _ _ Hvalid Hlookup).
  Qed.

310
  Lemma own_token_list_write γtoks t h xVs i xV :
Glen Mével's avatar
Glen Mével committed
311
312
313
    0  t 
    0  i 
    Zlength xVs = h -- t 
314
315
    tokens_auth γtoks t h xVs -
    token_write γtoks i xV -
Glen Mével's avatar
Glen Mével committed
316
317
    t  i < h    xVs !! (i -- t) = Some xV.
  Proof. clear.
318
    iIntros (???) "H● H◯". iCombine "H● H◯" as "H". rewrite own_valid.
Glen Mével's avatar
Glen Mével committed
319
320
321
322
323
324
325
326
327
328
329
330
331
    iDestruct "H" as %Hvalid. iPureIntro.
    apply auth_both_valid_discrete in Hvalid as [Hle Hvalid].
    apply list_singletonM_included in Hle as (otok & Hlookup & Hle).
    apply option_included in Hle as [ |(? & tok & [=<-] & -> & Hle)] ; first discriminate.
    destruct Hle as [ <-%leibniz_equiv | Hle ].
    { apply lookup_app_Some in Hlookup as [Hlookup|[Hineq1 Hlookup]] ; last
      apply lookup_app_Some in Hlookup as [Hlookup|[Hineq2 Hlookup]].
      - by apply lookup_replicate in Hlookup as [[=] _].
      - apply list_lookup_fmap_inv in Hlookup as (_ & [=<-] & Hlookup).
        rewrite replicate_length in Hineq1 Hlookup.
        rewrite (_ : (i - t)%nat = i--t) in Hlookup ; last lia.
        rewrite -list_lookup_Z_to_nat in Hlookup ; last lia.
        split ; last done. apply list_lookup_Z_lt_Some in Hlookup. lia.
332
      - by apply lookup_replicate in Hlookup as [[=] _]. }
Glen Mével's avatar
Glen Mével committed
333
334
335
336
337
338
339
340
341
342
    exfalso.
    apply leibniz_equiv_iff in Hlookup.
    apply csum_included in Hle
      as [   ->
         |[ (? & _ & [=]   & _)
          | (? & ? & [=<-] & -> & e' & ->%leibniz_equiv)
         ]] ;
      [|] ; by destruct (list_lookup_valid_Some _ _ _ Hvalid Hlookup).
  Qed.

343
  Lemma own_token_list_update_to_write γtoks t h xVs xV :
Glen Mével's avatar
Glen Mével committed
344
345
    0  t 
    Zlength xVs = h -- t 
346
347
    tokens_auth γtoks t h xVs -
    token_read γtoks (h--capacity) -
348
349
    |==>
        (*h -- capacity < t
350
351
      *) tokens_auth γtoks t (h+1) (xVs ++ [xV])
       token_write γtoks h xV.
Glen Mével's avatar
Glen Mével committed
352
  Proof. clear.
353
    iIntros (??) "H● H◯".
354
    iDestruct (own_token_list_read with "H● H◯") as "[% %]" ; try lia.
Glen Mével's avatar
Glen Mével committed
355
356
357
    iCombine "H● H◯" as "H". iMod (own_update with "H") as "[$$]" ; last done.
    apply auth_update.
    rewrite (_ : h -- capacity + capacity = h) ; last lia.
358
    rewrite (_ : t--(h--capacity) = S t--((h+1)--capacity)) ; last lia.
Glen Mével's avatar
Glen Mével committed
359
360
361
362
363
364
365
366
367
368
    assert ( t    h )%nat by lia.
    assert (h - t = length xVs)%nat as Hlen by lia.
    eapply list_lookup_local_update.
    { rewrite lookup_app_r replicate_length // Hlen
              lookup_app_r fmap_length // Nat.sub_diag //=. }
    { rewrite fmap_app -app_assoc
              insert_app_r_alt replicate_length // Hlen
              insert_app_r_alt fmap_length // Nat.sub_diag //=. }
    by apply option_local_update, exclusive_local_update.
  Qed.
Glen Mével's avatar
Glen Mével committed
369

370
  Lemma own_token_list_update_to_read γtoks t h xVs xV :
371
    0  t 
372
    h -- capacity  t 
373
    Zlength xVs = h -- t 
374
375
    tokens_auth γtoks t h xVs -
    token_write γtoks t xV -
376
377
    |==>  xVs',
        xVs = xV :: xVs'⌝
378
379
       tokens_auth γtoks (t+1) h xVs'
       token_read γtoks t.
380
381
  Proof. clear.
    iIntros (???) "H● H◯".
382
383
    iDestruct (own_token_list_write with "H● H◯") as "[[% %] #HxVs]" ; try lia.
    rewrite Zminus_diag. iDestruct "HxVs" as %HxVs.
384
385
    destruct xVs as [|? xVs'] ; first discriminate ; injection HxVs as -> ; cbn in *|-.
    iExists xVs'. iSplitR ; first done.
386
    iAssert ( |==> (__)  own γtoks ( {[t := None]}) )%I with "[-]" as ">[$_]" ; last done.
387
388
389
390
391
392
393
394
395
396
    iCombine "H● H◯" as "H". iMod (own_update with "H") as "($&$&$)" ; last done.
    apply auth_update.
    etrans.
    {
      eapply list_lookup_local_update ; [|done|].
      { rewrite lookup_app_r replicate_length ?Nat.sub_diag //=. }
      by apply delete_option_local_update, _.
    }
    {
      rewrite insert_app_r_alt replicate_length // Nat.sub_diag /=.
397
398
      rewrite (_ : t+1--(h--capacity) = S t--(h--capacity)) ?replicate_S_end ; last try lia.
      rewrite cons_middle !app_assoc -replicate_S_end (_ : S t = t+1) ; last lia.
399
400
      set li := (_ ++ _) ++ _.
      rewrite (_ : t+capacity = length li) ; last first.
401
      { rewrite !app_length !replicate_length fmap_length. lia. }
402
403
404
405
406
      rewrite - {1} [ {[t := None]} ] left_id.
      by apply op_local_update_frame, list_alloc_singletonM_local_update.
    }
  Qed.

Glen Mével's avatar
Glen Mével committed
407
408
409
  Definition queueN : namespace :=
    nroot .@ "bounded_queue".

Glen Mével's avatar
Glen Mével committed
410
  Notation seqZ' a b := (seqZ a%Z (b -- a)).
Glen Mével's avatar
Glen Mével committed
411

412
413
  (*
    ICFP21: Here is the internal invariant of the bounded queue as described in
414
    Figure 9e of the paper (queue_proto being called QueueInvInner in the
415
416
417
418
419
420
421
422
423
424
    paper).
    
    Vt and Vh are the head and tail views, respectively (denoted by calligraphic
    letters T and H in the paper).
    xVs is the list of value-view pairs appearing in the public state, denoted
    by (vt, Vt), , (vh, Vh) in the paper.
    sVs in the list of the value-view pairs of the atomic locations in the array
    statuses. It is denoted by (s0, S0), , (s_{C-1}, S_{C-1}) in the paper.
   *)

425
  Definition queue_proto γ γtoks γmonos tail head statuses elements : iProp Σ := (
426
     t h Vt Vh xVs sVs,
427
      (* authority over the public state: *)
Glen Mével's avatar
Glen Mével committed
428
        own γ (E (Vt, Vh, xVs))
429
      (* various arithmetic conditions: *)
Glen Mével's avatar
Glen Mével committed
430
       0  t  h  t + capacity
Glen Mével's avatar
Glen Mével committed
431
       Zlength xVs = h -- t
Glen Mével's avatar
Glen Mével committed
432
       length sVs = capacity
433
      (* authority over the ghost state representing the tokens: *)
434
       tokens_auth γtoks t h xVs
435
      (* authority over the ghost state representing the monotonicity of statuses: *)
Glen Mével's avatar
Glen Mével committed
436
       own (A:=listUR _) γmonos ((λ sV,  to_latT (Some (StatusPair sV.1 sV.2))) <$> sVs)
437
      (* ownership and value of the physical locations tail, head and statuses: *)
Glen Mével's avatar
Glen Mével committed
438
439
       tail at(#t, Vt)
       head at(#h, Vh)
Glen Mével's avatar
Glen Mével committed
440
       statuses *at() ((λ sV, (#sV.1, sV.2)) <$> sVs)
441
442
      (* description of slots: *)
        (* for every i in the range [h-capacity, t): *)
Glen Mével's avatar
Glen Mével committed
443
       ([ list] i  seqZ' (h -- capacity) t,
Glen Mével's avatar
Glen Mével committed
444
445
          let imod := i mod capacity in
          (* cell bearing no value, available for next round: *)
446
            (  dummy V,
447
                sVs !! imod = Some ((2*(i+capacity))%Z, V)
Glen Mével's avatar
Glen Mével committed
448
               (elements.[imod]  dummy) V
449
               token_read γtoks i
Glen Mével's avatar
Glen Mével committed
450
451
452
            )
          (* cell being emptied by a dequeuer: *)
           (  V,
453
                sVs !! imod = Some ((2*i+1)%Z, V)
Glen Mével's avatar
Glen Mével committed
454
(*                0  i *)
Glen Mével's avatar
Glen Mével committed
455
            )
Glen Mével's avatar
Glen Mével committed
456
        )
457
        (* for every i in the range [t, h): *)
Glen Mével's avatar
Glen Mével committed
458
       ([ list] i;xV  seqZ' t h ; xVs,
Glen Mével's avatar
Glen Mével committed
459
          let imod := i mod capacity in
Glen Mével's avatar
Glen Mével committed
460
          (* cell bearing a value: *)
Glen Mével's avatar
Glen Mével committed
461
462
            (  V,
                xV.2  V
463
               sVs !! imod = Some ((2*i+1)%Z, V)
Glen Mével's avatar
Glen Mével committed
464
               (elements.[imod]  xV.1) V
465
               token_write γtoks i xV
Glen Mével's avatar
Glen Mével committed
466
            )
Glen Mével's avatar
Glen Mével committed
467
          (* cell being filled with a value by an enqueuer: *)
Glen Mével's avatar
Glen Mével committed
468
           (  V,
469
                sVs !! imod = Some ((2*i)%Z, V)
Glen Mével's avatar
Glen Mével committed
470
471
            )
        )
472
473
474
475
476
477
478
479
    (* NOTE: additional assertions that we can maintain in the invariant, but
             which are not required by this proof:
       has_length statuses capacity
       has_length elements capacity
       Forall (λ sV, 0  sV.1) sVs
       monotonicity of t
       monotonicity of h
    *)
Glen Mével's avatar
Glen Mével committed
480
481
  )%I.

Glen Mével's avatar
Glen Mével committed
482
  Definition queue_inv q γ : iProp Σ := (
483
     γtoks γmonos tail head statuses elements,
Glen Mével's avatar
Glen Mével committed
484
        q = (#tail, #head, #statuses, #elements)%V
485
       inv queueN (queue_proto γ γtoks γmonos tail head statuses elements)
Glen Mével's avatar
Glen Mével committed
486
487
  )%I.

Glen Mével's avatar
Glen Mével committed
488
  Global Instance queue_inv_persistent q γ : Persistent (queue_inv q γ).
Glen Mével's avatar
Glen Mével committed
489
490
  Proof. by apply _. Qed.

491
  (* ICFP21: this is the predicate IsQueue from the paper, which exposes the
492
     public state of the queue (Figure 9a of the paper). *)
Glen Mével's avatar
Glen Mével committed
493
  Definition is_queue γ Vt Vh xVs : iProp Σ := (
Glen Mével's avatar
Glen Mével committed
494
    own γ (E (Vt, Vh, xVs))
Glen Mével's avatar
Glen Mével committed
495
496
497
498
  )%I.

(*
  Definition Is_queue q Vt Vh xVs : iProp Σ := (
Glen Mével's avatar
Glen Mével committed
499
     (γ : gname),
500
      queue_inv q γ  is_queue γ Vt Vh xVs
Glen Mével's avatar
Glen Mével committed
501
502
503
  )%I.
*)

Glen Mével's avatar
Glen Mével committed
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
  Lemma own_list_auth_update_frag
  {A : latticeT} `{inG Σ (listUR $ authUR $ latUR (option_Lat A))}
  (γ : gname) (xs : list A) (i : nat) (x : A) :
    xs !! i = Some x 
    own (A:= listUR _) γ ((λ (x : A),  to_latT (Some x)) <$> xs) ==
      own (A:= listUR _) γ ((λ (x : A),  to_latT (Some x)) <$> xs)
     own (A:= listUR _) γ {[i :=  to_latT (Some x)]}.
  Proof. clear.
    intros Hi. rewrite -own_op. apply own_update.
    revert xs Hi ; induction i as [|i IH] => xs Hi.
    { destruct xs as [|x0 xs] ; inversion Hi ; subst x0.
      apply cons_update ; last by rewrite right_id.
      apply auth_update_alloc, latT_local_unit_update. reflexivity. }
    { destruct xs as [|x0 xs] ; first discriminate.
      apply cons_update ; first by rewrite right_id. by apply IH. }
  Qed.

  Lemma own_list_auth_both_le
  {A : latticeT} `{inG Σ (listUR $ authUR $ latUR (option_Lat A))}
  (γ : gname) (xs : list A) (i : nat) (x y : A) :
    xs !! i = Some y 
      own (A:= listUR _) γ {[i :=  to_latT (Some x)]}
     own (A:= listUR _) γ ((λ (x : A),  to_latT (Some x)) <$> xs) -
        x  y.
  Proof. clear.
    rewrite -own_op own_valid. iIntros "!% /=".
    revert xs ; induction i as [|i IH] => xs Hi.
    { destruct xs as [|x0 xs] ; inversion Hi ; subst x0. rewrite comm.
      by intros [[?%latT_included _]%auth_both_valid_discrete _]%cons_valid. }
    { destruct xs as [|x0 xs] ; first discriminate. rewrite fmap_cons.
      intros [_ ?]%cons_valid. by apply (IH xs). }
  Qed.

  Lemma seqZ_app (len1 len2 start : Z):
    0  len1 
    0  len2 
    seqZ start (len1 + len2) = seqZ start len1 ++ seqZ (start + len1) len2.
  Proof. clear.
    intros H1 H2. rewrite /seqZ Z2Nat.inj_add// seq_app fmap_app. f_equal.
    rewrite [(0 + _)%nat]comm -fmap_add_seq -list_fmap_compose.
    apply list_fmap_ext ; last done. cbn. lia.
  Qed.

Glen Mével's avatar
Glen Mével committed
547
548
549
550
551
552
  Lemma init_array_atomic_spec (E : coPset) (n : Z) (f : val) (φ : Z  val) V :
    {{{ monPred_in V  0  n
       <pers>  (i : Z) Φ, ( y, y = φ i - Φ y) - WP f #i @ E {{ Φ }}
    }}}
      init_array Atomic #n f @ E
    {{{ arr, RET #arr ;  arr *at() ((λ i, (φ i, V)) <$> seqZ 0 n)  }}}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
553
  Proof using capacity_min.
554
    iIntros (Φ) "(#? & Hn & #Hf) HΦ". iDestruct "Hn" as %Hn.
Glen Mével's avatar
Glen Mével committed
555
556
557
    wp_lam. wp_alloc arr as "Harr". wp_let. wp_closure.
    pose k := 0. rewrite [in #0](_ : 0 = k)//.
    assert (0  k  n) as Hk by lia.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
558
559
    rewrite (_ : replicate _ _ = ((λ i, (φ i, V)) <$> seqZ 0 k) ++ replicate n--k (#(), )) ;
      last (rewrite /k (_ : n-k = n) //; lia).
Glen Mével's avatar
Glen Mével committed
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
    clearbody k. iLöb as "IH" forall (k Hk). wp_pures.
    destruct (bool_decide _) eqn:Hcmp.
    {
      apply bool_decide_eq_true in Hcmp.
      wp_pures. iApply "HΦ". rewrite (_ : k = n) ; last lia.
      rewrite (_ : n - n = 0) ; last lia. rewrite (_ : 0 = 0%nat)//= right_id //.
    }
    {
      apply bool_decide_eq_false in Hcmp.
      wp_pures. wp_apply "Hf" ; iIntros (?->). wp_write_block at V as ??? "_".
      { rewrite app_length fmap_length seqZ_length replicate_length. lia. }
      rewrite (_ : <[_ := _]> _ = ((λ i, (φ i, V)) <$> seqZ 0 (k+1)) ++ replicate n--(k+1) (#(), )) ; last first. {
        rewrite list_insert_Z_to_nat ; last lia.
        rewrite insert_app_r_alt fmap_length seqZ_length ; last lia.
        rewrite Nat.sub_diag (_ : n--k = S n--(k+1)) /= ; last lia.
        rewrite seqZ_app ; [|lia..].
        rewrite /seqZ (_ : 1 = 1%nat)// fmap_app -app_assoc //=.
      }
      wp_op. iApply ("IH" $! (k+1) with "[] HΦ Harr"). iPureIntro. lia.
    }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
580
  Qed.
Glen Mével's avatar
Glen Mével committed
581

582
  (* ICFP21: this is the spec of make, as presented in Figure 5 of the paper,
583
584
585
586
     along with its proof for this particular implementation (recall that
     monPred_in V is what is denoted by V in the paper; P is the embedding
     of an objective assertion P (of type iProp) into general Cosmo assertions
     (of type vProp)). *)
Glen Mével's avatar
Glen Mével committed
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
  Lemma make_spec (E : coPset) V :
    {{{ monPred_in V }}}
      make #() @ E
    {{{ q γ, RET q ; queue_inv q γ⎤  is_queue γ V V [] }}}.
  Proof.
    iIntros (Φ) "#HV HΦ". wp_lam.
    (* allocate locations *)
    wp_alloc elements as "Helements". rewrite Nat2Z.id.
    (* make ownership of elements objective and get the corresponding view: *)
    iDestruct (monPred_in_intro with "Helements") as (Ve) "[ #HVe Helements ]".
    wp_apply init_array_atomic_spec ; last iIntros (statuses) "Hstatuses".
    { iSplit ; last iSplit ; [ iExact "HVe" | iPureIntro ; lia |].
      iIntros "!>" (i Ψ) "HΨ". wp_lam. wp_pures. iApply "HΨ". done. }
    wp_ref tail at V as "Htail". wp_ref head at V as "Hhead".
    (* create ghost variables *)
    iMod (own_alloc (E (V, V, [])  E (V, V, []))) as (γ) "[Hγ● Hγ◯]".
    { by apply auth_both_valid_discrete. }
    epose (tokens := replicate capacity (Some $ Cinl $ Excl ())).
    iMod (own_alloc ( tokens   tokens)) as (γtoks) "[Hγtoks● Hγtoks◯]".
    { apply auth_both_valid_discrete. split ; first done.
      apply list_lookup_valid => ?. destruct (_ !! _) eqn:Hlookup ; last done.
      apply lookup_replicate in Hlookup as [[=->] _]. done. }
    epose (monos := (λ sV,  to_latT (Some (StatusPair sV.1 sV.2))) <$> (
                    (λ i, (i+i, Ve)) <$> seqZ 0 capacity ) ).
    iMod (own_alloc monos) as (γmonos) "Hγmonos●".
    { apply list_lookup_valid => ?. rewrite list_lookup_fmap.
      destruct (_ !! _) => //=. by apply Some_valid, auth_auth_valid. }
    (* create invariant *)
    iMod (inv_alloc _ _ (queue_proto γ γtoks γmonos tail head statuses elements)
          with "[- Hγ◯ HΦ]")  as "#I".
    {
      iIntros "!> !>". iExists 0, 0, V, V, [], _. iFrame "Hγ● Htail Hhead Hγmonos●".
      rewrite -(list_fmap_compose _ _ (seqZ _ _)). iFrame "Hstatuses".
      rewrite /tokens_auth (_ : 0 = 0%nat)// (_ : ⌊ 0 -- (0 -- capacity) ⌋ = capacity) ; last lia. iFrame "Hγtoks●".
      rewrite fmap_length seqZ_length. repeat (iSplit ; first (iPureIntro ; cbn ; lia)).
      rewrite /= right_id.
      rewrite (_ : 0 -- capacity = -capacity) ; last lia.
      rewrite /(seqZ' _ _) big_sepL_fmap (_ :  0 -- (0 -- capacity)  = capacity) ; last lia.
      iDestruct "Helements" as "[_ Helements]". rewrite /tokens.
      iApply big_sepL_mono. { iIntros (?? _) "?". by iLeft. } cbn.
      pose k := capacity.
        rewrite [in replicate capacity](_ : capacity = k)//.
        rewrite [in replicate capacity](_ : capacity = k)//.
        rewrite [in seq 0 capacity](_ : capacity = k)//.
        assert (k  capacity)%nat as Hk by lia.
        clearbody k.
      iInduction k as [|k'] "IH" forall (Hk) ; first done.
      rewrite 2!replicate_S_end.
      iDestruct "Helements" as "[Helements' Helementk]". rewrite replicate_length.
      rewrite (_ : replicate k' (Some $ Cinl $ Excl ()) ++ [ Some $ Cinl $ Excl () ]
                 = replicate k' (Some $ Cinl $ Excl ())  {[ k' := Some $ Cinl $ Excl () ]}
              ) ; last first.
      { apply leibniz_equiv. rewrite -list_singletonM_snoc replicate_length [_  _]comm //. }
      iDestruct "Hγtoks◯" as "[Hγtoks' Hγtokk]".
      rewrite seq_S_end_app.
      iDestruct ("IH" with "[] Helements' Hγtoks'") as "$" ; first (iPureIntro; lia).
      iClear "IH".
      rewrite /= 2!(right_id emp%I) (_ : k' + 0 = k')%nat ; last lia.
      rewrite /token_read.
      rewrite (_ : k' + -capacity + capacity = k') ?Nat2Z.id ; last lia.
      rewrite (_ : (k' + - capacity) mod capacity = k') ; last first.
      { rewrite -Zminus_mod_idemp_r Z.mod_same ?Z.sub_0_r ?Z.mod_small ; lia. }
      iExists _, _. iFrame. iPureIntro.
      rewrite /lookup/list_lookup_Z/=; destruct (bool_decide _) eqn:Hpos;
        last (apply bool_decide_eq_false in Hpos ; lia).
      rewrite list_lookup_fmap lookup_seqZ_lt /= ; first repeat f_equal ; lia.
    }
    (* return, providing the invariant and the representation predicate in the post-condition *)
    wp_pures. iApply "HΦ".
    iFrame "Hγ◯". repeat (iExists _). by iFrame "I".
  Qed.

659
  (* ICFP21: this is the spec of try_enqueue, as presented in Figure 5 of the
660
661
662
663
     paper, along with its proof.
     <<<  x, P >>> e <<< Q, RET v >>> is the notation for a logically atomic
     triple (P,e,Q) with a binder x and returning value v.
     The first condition is about namespaces, it is an Iris technicality. *)
664
  Lemma try_enqueue_spec (E : coPset) q γ x V :
Glen Mével's avatar
Glen Mével committed
665
666
667
668
    E ## queueN 
    queue_inv q γ⎤ -
    monPred_in V -
    <<<  Vt Vh xVs, is_queue γ Vt Vh xVs >>>
Glen Mével's avatar
Glen Mével committed
669
670
671
        try_enqueue q x @ E
    <<<  (b : bool),
      if b
Glen Mével's avatar
Glen Mével committed
672
      then is_queue γ Vt (Vh  V) (xVs ++ [(x,V)])  monPred_in Vh
Glen Mével's avatar
Glen Mével committed
673
      else is_queue γ Vt Vh xVs,
674
          (* NOTE: we can add this, even if useless:  monPred_in Vh *)
Glen Mével's avatar
Glen Mével committed
675
    RET #b >>>.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
676
  Proof using capacity_min.
Glen Mével's avatar
Glen Mével committed
677
    iIntros (HE). iIntros "#Inv #HV" (Φ) "AU".
678
    iDestruct "Inv" as (γtoks γmonos tail head statuses elements ->) "#Inv".
Glen Mével's avatar
Glen Mével committed
679
    wp_lam. repeat first [ wp_proj | wp_let ].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
680

Glen Mével's avatar
Glen Mével committed
681
682
    (* (1) atomic read head *)
    (* --- open invariant *)
Glen Mével's avatar
Glen Mével committed
683
    wp_bind (!at _)%E.
684
    iInv queueN as (t0 h0 Vt0 Vh0 xVs0 sVs0) ">(Hγ● & %Hineq & Hlenx & Hlens & Htoks & Hmonos & Htail & Hhead & InvRest)" "InvClose".
Glen Mével's avatar
Glen Mével committed
685
    (* --- read h from head *)
Glen Mével's avatar
Glen Mével committed
686
    wp_read as "_".
Glen Mével's avatar
Glen Mével committed
687
    assert (0  h0) by lia.
Glen Mével's avatar
Glen Mével committed
688
689
    (* --- close invariant *)
    iMod ("InvClose" with "[-AU]") as "_". { repeat (iExists _). by iFrame. }
690
    clear dependent t0 Vt0 Vh0 xVs0 sVs0.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
691

Glen Mével's avatar
Glen Mével committed
692
693
    (* pure steps *)
    iModIntro. wp_let. wp_apply modulo_spec. wp_let.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
694

Glen Mével's avatar
Glen Mével committed
695
696
697
    (* (2) atomic read statuses.[h % capacity] *)
    (* --- open invariant *)
    wp_bind (Read Atomic _ _)%E.
698
    iInv queueN as (t1 h1 Vt1 Vh1 xVs1 sVs1) ">(Hγ● & %Hineq & %Hlenx & %Hlens & Htoks & Hmonos & Htail & Hhead & Hstatuses & Hfree & Hfill)".
Glen Mével's avatar
Glen Mével committed
699
700
701
702
703
704
705
706
707
    (* --- read s1 from statuses.[h % capacity] *)
    wp_read_block as s1 V1 HsVs1 "HV1".
    { rewrite fmap_length -Hlens. apply Z_mod_lt. lia. }
    (* value s1 is in fact an integer s1' *)
    apply list_lookup_Z_Some_to_nat in HsVs1. rewrite list_lookup_fmap in HsVs1.
    destruct lookup as [[s1' ?]|] eqn:HsVs1' ; last done. injection HsVs1 as <- ->.
    (* --- get monotonicity witness for s1 *)
    iMod ( own_list_auth_update_frag _
        ((λ sV, StatusPair sV.1 sV.2) <$> sVs1)
Glen Mével's avatar
Glen Mével committed
708
        h0 `mod` capacity
Glen Mével's avatar
Glen Mével committed
709
710
711
712
713
714
715
        with "[Hmonos]" )
      as "[Hmonos Hmonos1]" ;
        [|by rewrite -list_fmap_compose|].
    { by rewrite list_lookup_fmap HsVs1'. }
    rewrite -list_fmap_compose.
    (* --- close invariant *)
    iModIntro. iSplitR "AU Hmonos1". { repeat (iExists _). by iFrame. }
716
    cbn. clear dependent t1 h1 Vt1 Vh1 xVs1 sVs1.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
717

718
    (* (3) test whether s1 = 2*h0 *)
Glen Mével's avatar
Glen Mével committed
719
    wp_pures. case_bool_decide ; last first.
720
    (* (3a) case: s1  2*h0: return false *)
Glen Mével's avatar
Glen Mével committed
721
    { iApply wp_fupd. wp_pures. iMod "AU" as (???) "[? [_ H]]". by iApply "H". }
722
    (* (3b) case: s1 = 2*h0: CAS head *)
Glen Mével's avatar
Glen Mével committed
723
    subst s1'. wp_pures.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
724

Glen Mével's avatar
Glen Mével committed
725
726
    (* --- open invariant *)
    wp_bind (CAS_ref _ _ _).
727
    iInv queueN as (t2 h2 Vt2 Vh2 xVs2 sVs2) ">(Hγ● & %Hineq & %Hlenx & %Hlens & Htoks & Hmonos & Htail & Hhead & Hstatuses & Hfree & Hfill)".
Glen Mével's avatar
Glen Mével committed
728
729
730
    (* --- CAS head *)
    wp_cas at (Vh2  V) as "HVh2", Heqh | _ ; last first.
    (* (3b-a) case: h0  h2: CAS fails *)
Glen Mével's avatar
Glen Mével committed
731
    {
Glen Mével's avatar
Glen Mével committed
732
733
734
735
      (* --- close invariant *)
      iModIntro. iSplitR "AU Hmonos1". { repeat (iExists _). by iFrame. }
      (* --- return false *)
      iApply wp_fupd. wp_pures. iMod "AU" as (???) "[? [_ H]]". by iApply "H".
Glen Mével's avatar
Glen Mével committed
736
    }
Glen Mével's avatar
Glen Mével committed
737
738
    (* (3b-b) case: h0 = h2 *)
    injection Heqh as ->.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
739

Glen Mével's avatar
Glen Mével committed
740
    simpl.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
741

Glen Mével's avatar
Glen Mével committed
742
743
    (* --- Eliminate the absurd case where the buffer is full (h0 = t2 + capacity). *)
    destruct (decide (h0 = t2 + capacity)) as [Heq|Hineq2].
Glen Mével's avatar
Glen Mével committed
744
    {
Glen Mével's avatar
Glen Mével committed
745
746
747
748
      assert (length xVs2 > 0) by lia.
      destruct xVs2 as [|[x0 V0] xVs] ; first by exfalso.
      rewrite [seqZ t2 _] seqZ_cons ; last lia.
      rewrite big_sepL2_cons.
Glen Mével's avatar
Glen Mével committed
749
750
      iDestruct "Hfill" as "[Hfillt2 _]".
      iAssert False%I with "[Hmonos1 Hmonos Hfillt2]" as "?" ; last done.
Glen Mével's avatar
Glen Mével committed
751
752
      assert (h0 `mod` capacity = t2 `mod` capacity) as ->.
      { subst h0. by rewrite Zplus_mod Z_mod_same_full [_ + 0] Z.add_0_r Zmod_mod. }
Glen Mével's avatar
Glen Mével committed
753
      iDestruct "Hfillt2" as "[ Hex | Hex ]".
Glen Mével's avatar
Glen Mével committed
754
755
756
757
758
      { iDestruct "Hex" as (? _ HsVs) "_".
        iDestruct (own_list_auth_both_le _ ((λ sV, StatusPair sV.1 sV.2) <$> sVs2) with "[$Hmonos1 Hmonos]") as %Hle ;
          [|by rewrite -list_fmap_compose|].
        - by erewrite list_lookup_fmap, list_lookup_Z_Some_to_nat.
        - exfalso. apply statuspair_le_Z_le in Hle. cbn in Hle. lia. }
Glen Mével's avatar
Glen Mével committed
759
      { iDestruct "Hex" as (?) "%HsVs".
Glen Mével's avatar
Glen Mével committed
760
761
762
763
        iDestruct (own_list_auth_both_le _ ((λ sV, StatusPair sV.1 sV.2) <$> sVs2) with "[$Hmonos1 Hmonos]") as %Hle ;
          [|by rewrite -list_fmap_compose|].
        - by erewrite list_lookup_fmap, list_lookup_Z_Some_to_nat.
        - exfalso. apply statuspair_le_Z_le in Hle. cbn in Hle. lia. }
Glen Mével's avatar
Glen Mével committed
764
    }
Glen Mével's avatar
Glen Mével committed
765
766
    (* --- Now we know that cell number h0 is in the free-list. *)
    assert (h0 < t2 + capacity) by lia.
Glen Mével's avatar
Glen Mével committed
767
768
    rewrite [seqZ' _ t2]seqZ_cons ; last lia.
    (* --- Eliminate the absurd case where cell number h0 is being emptied. *)
Glen Mével's avatar
Glen Mével committed
769
    iDestruct "Hfree" as "[[Hex|Hex] Hfree]" ; last first.
Glen Mével's avatar
Glen Mével committed
770
    { iDestruct "Hex" as (?) "%HsVs".
Glen Mével's avatar
Glen Mével committed
771
      rewrite (_ : (h0 -- capacity) `mod` capacity = h0 `mod` capacity) in HsVs ; last first.
Glen Mével's avatar
Glen Mével committed
772
773
      { rewrite Zminus_mod Z.mod_same ; last lia.
        rewrite Z.sub_0_r Z.mod_mod// ; last lia. }
Glen Mével's avatar
Glen Mével committed
774
775
776
777
778
      iDestruct (own_list_auth_both_le _ ((λ sV, StatusPair sV.1 sV.2) <$> sVs2) with "[$Hmonos1 Hmonos]") as %Hle ;
        [|by rewrite -list_fmap_compose|].
      - by erewrite list_lookup_fmap, list_lookup_Z_Some_to_nat.
      - exfalso. apply statuspair_le_Z_le in Hle. cbn in Hle. lia. }
    (* --- Now we know that cell number h0 is really free. *)
779
    iDestruct "Hex" as (dummy V2) "(HsVs2 & Helement & Hr)".
Glen Mével's avatar
Glen Mével committed
780
781
    rewrite (_ : h0 -- capacity + capacity = h0) ; last lia.
    rewrite (_ : (h0 -- capacity) `mod` capacity = h0 `mod` capacity) ; last first.
Glen Mével's avatar
Glen Mével committed
782
783
784
    { rewrite Zminus_mod Z.mod_same ; last lia.
      rewrite Z.sub_0_r Z.mod_mod// ; last lia. }
    iDestruct "HsVs2" as %HsVs2.
Glen Mével's avatar
Glen Mével committed
785
786
    (* --- The view V2 is in fact V1, it hasnt changed since we read it. *)
    iAssert V2  V1%I with "[Hmonos Hmonos1]" as %HV2.
Glen Mével's avatar
Glen Mével committed
787
    {
Glen Mével's avatar
Glen Mével committed
788
789
790
791
      iDestruct (own_list_auth_both_le _ ((λ sV, StatusPair sV.1 sV.2) <$> sVs2) with "[$Hmonos1 Hmonos]") as %Hle ;
        [|by rewrite -list_fmap_compose|].
      - by erewrite list_lookup_fmap, list_lookup_Z_Some_to_nat.
      - cbn in Hle. destruct Hle as [? | [_ ?]] ; [exfalso ; lia | done].
Glen Mével's avatar
Glen Mével committed
792
    }
Glen Mével's avatar
Glen Mével committed
793
794
795
796
797
798
799
    rewrite [in _ V2] HV2.
    (* --- We commit the atomic Hoare triple. *)
    iMod "AU" as (Vt3 Vh3 xVs3) "[Hγ◯ [_ Hclose]]".
    (* --- Unify Vt3 with Vt2, Vh3 with Vh2, xVs3 with xVs2. *)
    iDestruct (own_valid_2 with "Hγ● Hγ◯") as %[= <- <- <-]%excl_auth_agree_L.
    (* --- Update the public state *)
    iMod (own_update_2 with "Hγ● Hγ◯") as "[Hγ● Hγ◯]" ; first apply excl_auth_update.
800
801
    (* --- Forge a token_write from the token_read from the previous round. *)
    iMod (own_token_list_update_to_write with "Htoks Hr") as "[Htoks Hw]" ; try lia.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
802

Glen Mével's avatar
Glen Mével committed
803
    iMod ("Hclose" $! true with "[$]") as "HΦ".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
804

Glen Mével's avatar
Glen Mével committed
805
806
    (* --- close invariant *)
    iModIntro. iSplitR "Hmonos1 HΦ Hw Helement".
Glen Mével's avatar
Glen Mével committed
807
    {
Glen Mével's avatar
Glen Mével committed
808
      iModIntro. iNext. repeat (iExists _).
Glen Mével's avatar
Glen Mével committed
809
810
      rewrite (_ : Z.succ (h0 - capacity) = (h0+1) - capacity) ; last lia.
      rewrite (_ : Z.pred (t2 - (h0 - capacity)) = t2 - ((h0+1) - capacity)) ; last lia.
811
      iFrame "Hγ● Htoks Hmonos Htail Hhead Hstatuses Hfree".
812
      rewrite app_length /=.
Glen Mével's avatar
Glen Mével committed
813
814
815
      repeat (iSplitL "" ; first (iPureIntro ; eauto with lia)).
      rewrite (_ : h0 + 1 - t2 = (h0 - t2) + 1) ; last lia.
      rewrite seqZ_app ; try lia.
Glen Mével's avatar
Glen Mével committed
816
      iApply (big_sepL2_app with "Hfill").
Glen Mével's avatar
Glen Mével committed
817
      rewrite (_ : t2 + (h0 - t2) = h0) ; last lia.
Glen Mével's avatar
Glen Mével committed
818
819
      rewrite (eq_refl : seqZ h0 1 = [h0]) /= right_id.
      iRight. auto with iFrame.
Glen Mével's avatar
Glen Mével committed
820
    }
821
    iClear "HVh2 Hmonos1". clear dependent t2 Vh2 Vt2 xVs2 sVs2 V2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
822

Glen Mével's avatar
Glen Mével committed
823
    (* (4) non-atomic write to elements.[h0 % capacity] *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
824

Glen Mével's avatar
Glen Mével committed
825
826
827
828
    wp_pures.
    iDestruct (monPred_in_elim with "HV1 Helement") as "Helement" ; iClear (V1) "HV1".
    wp_write.
    iDestruct (monPred_in_intro with "Helement") as (Ve) "[#HVe Helement]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
829

Glen Mével's avatar
Glen Mével committed
830
    (* (5) atomic write to statuses.[h0 % capacity] *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
831

Glen Mével's avatar
Glen Mével committed
832
833
    (* --- open invariant *)
    wp_pures. wp_bind (Write Atomic _ _ _).
834
    iInv queueN as (t3 h3 Vt3 Vh3 xVs3 sVs3) ">(Hγ● & %Hineq & %Hlenx & %Hlens & Htoks & Hmonos & Htail & Hhead & Hstatuses & Hfree & Hfill)".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
835

Glen Mével's avatar
Glen Mével committed
836
837
838
    (* --- perform write *)
    wp_write_block at (V  Ve) as s3 V3 _ "_" ; last clear s3 V3.
    { rewrite fmap_length Hlens. apply Z_mod_lt. lia. }
839
    rewrite (_ : h0+h0 = 2*h0) ; last lia.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
840

Glen Mével's avatar
Glen Mével committed
841
    (* --- close invariant *)
Glen Mével's avatar
Glen Mével committed
842
    iSplitR "HΦ".
Glen Mével's avatar
Glen Mével committed
843
    {
Glen Mével's avatar
Glen Mével committed
844
      rewrite -embed_fupd. iModIntro. repeat (iExists _).
Glen Mével's avatar
Glen Mével committed
845
      assert (0  h0 `mod` capacity). { apply Z_mod_pos. lia. }
846
      iDestruct (own_token_list_write with "Htoks Hw") as "[%Hh0 %HxVs3]" ; [lia .. |].
Glen Mével's avatar
Glen Mével committed
847
      (* frame Hstatuses first (so as to unify the existential list with sVs3) *)
848
      rewrite -(list_fmap_insert_Z _ _ _ (2*h0+1, V  Ve)).
Glen Mével's avatar
Glen Mével committed
849
850
851
      iFrame "Hstatuses".
      (* frame trivial things *)
      rewrite insert_Z_length.
852
      iFrame (Hineq Hlenx Hlens) "Hγ● Htoks Htail Hhead".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
853

854
      iAssert ( V0 : view, sVs3 !! (h0 `mod` capacity) = Some ((2*h0)%Z, V0))%I with "[Hw Hfill]" as (V0) "%HsVs3".
Glen Mével's avatar
Glen Mével committed
855
      {
Glen Mével's avatar
Glen Mével committed
856
        assert (seqZ' t3 h3 !! h0 -- t3 = Some h0) as HseqZ.
Glen Mével's avatar
Glen Mével committed
857
        { apply lookup_seqZ. lia. }
Glen Mével's avatar
Glen Mével committed
858
859
860
861
862
863
864
        apply list_lookup_Z_Some_to_nat in HxVs3.
        iDestruct (big_sepL2_lookup _ _ _ _ _ _ HseqZ HxVs3 with "Hfill") as "[Hfilli|?]" ;
          last done.
        iDestruct "Hfilli" as (?) "(_ & _ & _ & Hw')".
        iCombine "Hw Hw'" as "Hexcl". rewrite list_singletonM_op.
        iDestruct (own_valid with "Hexcl")
          as %[]%auth_frag_valid%list_singletonM_valid.
Glen Mével's avatar
Glen Mével committed
865
      }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
866

Glen Mével's avatar
Glen Mével committed
867
      iSplitL "Hmonos" ; last iSplitL "Hfree".
Glen Mével's avatar
Glen Mével committed
868
869
      {
        (* 1st goal: Hmonos with updated sVs3 *)
Glen Mével's avatar
Glen Mével committed
870
871
872
873
        set f := (λ sV : Z * view,  to_latT (Some $ StatusPair sV.1 sV.2)).
        iMod (own_update with "Hmonos") as "$" ; last done.
        rewrite list_fmap_insert_Z. simpl.
        apply list_lookup_Z_Some_to_nat in HsVs3.
874
        rewrite -(take_drop_middle sVs3 h0 `mod` capacity (2*h0, V0))//.
Glen Mével's avatar
Glen Mével committed
875
876
877
878
879
880
881
        rewrite fmap_app list_insert_Z_to_nat// insert_app_r_alt ; last first.
        { rewrite fmap_length take_length. lia. }
        rewrite [x in <[x := _]>](_ : _ = 0%nat) ; last first.
        { rewrite fmap_length take_length min_l ?Hlens ; first lia.
          pose proof (Z.mod_pos_bound h0 (Z.of_nat capacity)). lia. }
        eapply list_middle_update, auth_update_auth, latT_local_unit_update.
        simpl. left. lia.
Glen Mével's avatar
Glen Mével committed
882
883
      }
      {
Glen Mével's avatar
Glen Mével committed
884
        (* 2nd goal: Hfree *)
Glen Mével's avatar
Glen Mével committed
885
886
887
888
        iModIntro. iNext.
        iApply (big_sepL_mono with "Hfree").
        intros k _ [-> Hk]%lookup_seqZ.
        rewrite /= list_lookup_Z_insert_Z_ne ; first done.
889
        clear -Hineq Hh0 Hk. set h3k := h3 -- capacity + k. intros Heq.
Glen Mével's avatar
Glen Mével committed
890
891
892
        assert ((h0 -- h3k) `mod` capacity = h0 -- h3k) as Heq'.
        { apply Zmod_small. lia. }
        rewrite Zminus_mod Heq Zminus_diag Zmod_0_l in Heq'. lia.
Glen Mével's avatar
Glen Mével committed
893
894
895
      }
      {
        (* 3rd goal: Hfill *)
Glen Mével's avatar
Glen Mével committed
896
        iModIntro. iNext.
Glen Mével's avatar
Glen Mével committed
897
        apply list_lookup_Z_Some_to_nat in HxVs3.
Glen Mével's avatar
Glen Mével committed
898
899
        rewrite -(take_drop_middle xVs3 h0--t3 (x, V))//.
        rewrite -(take_drop_middle (seqZ t3 (h3--t3)) h0--t3 h0) ; last first.
Glen Mével's avatar
Glen Mével committed
900
        { apply lookup_seqZ. lia. }
Glen Mével's avatar
Glen Mével committed
901
902
903
        iDestruct (big_sepL2_app_inv with "Hfill") as "(Hfill1 & Hfilli & Hfill2)".
        { by rewrite 2!take_length seqZ_length -Hlenx Nat2Z.id. }
        iApply (big_sepL2_app with "[Hfill1]").
Glen Mével's avatar
Glen Mével committed
904
        {
Glen Mével's avatar
Glen Mével committed
905
          iApply (big_sepL2_mono with "Hfill1").
Glen Mével's avatar
Glen Mével committed
906
907
          iIntros (k j ? Hj ?) "?".
          rewrite list_lookup_Z_insert_Z_ne//.
Glen Mével's avatar
Glen Mével committed
908
          destruct (decide (k < h0--t3)) ; last first.
Glen Mével's avatar
Glen Mével committed
909
910
911
912
          { rewrite lookup_take_ge in Hj ; [done|lia]. }
          rewrite lookup_take in Hj ; last lia.
          apply lookup_seqZ in Hj.
          intro Hij.
Glen Mével's avatar
Glen Mével committed
913
          assert ((h0 -- j) `mod` capacity = 0) as Hij' by
Glen Mével's avatar
Glen Mével committed
914
915
916
            rewrite Zminus_mod Hij Z.sub_diag//.
          rewrite Zmod_small in Hij' ; lia.
        }
Glen Mével's avatar
Glen Mével committed
917
        iSplitR "Hfill2" ; last first.
Glen Mével's avatar
Glen Mével committed
918
        {
Glen Mével's avatar
Glen Mével committed
919
          iApply (big_sepL2_mono with "Hfill2").
Glen Mével's avatar
Glen Mével committed
920
921
922
923
924
          iIntros (k j ? Hj ?) "?".
          rewrite list_lookup_Z_insert_Z_ne//.
          rewrite lookup_drop in Hj.
          apply lookup_seqZ in Hj.
          intro Hij.
Glen Mével's avatar
Glen Mével committed
925
          assert ((j - h0) `mod` capacity = 0) as Hij' by
Glen Mével's avatar
Glen Mével committed
926
927
928
929
930
931
            rewrite Zminus_mod Hij Z.sub_diag//.
          rewrite Zmod_small in Hij' ; lia.
        }
        rewrite list_lookup_Z_insert_Z ; last first.
        { rewrite Hlens. apply Z_mod_lt. lia. }
        iLeft.
Glen Mével's avatar
Glen Mével committed
932
933
        iDestruct "Hfilli" as "[Hfilli | Hfilli]".
        { iDestruct "Hfilli" as (?) "(_ & _ & _ & Hw')".
Glen Mével's avatar
Glen Mével committed
934
935
          iCombine "Hw Hw'" as "Hexcl". rewrite list_singletonM_op.
          iDestruct (own_valid with "Hexcl")
Glen Mével's avatar
Glen Mével committed
936
            as %[]%auth_frag_valid%list_singletonM_valid. }
Glen Mével's avatar
Glen Mével committed
937
938
        simpl. iExists (V  Ve).
        iFrame "Hw Helement". iPureIntro. split ; [solve_lat | done].
Glen Mével's avatar
Glen Mével committed
939
      }
Glen Mével's avatar
Glen Mével committed
940
    }
941
    clear dependent t3 h3 Vt3 Vh3 xVs3 sVs3.
Glen Mével's avatar
Glen Mével committed
942
    iModIntro.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
943

Glen Mével's avatar
Glen Mével committed
944
945
    (* (6) return true *)
    wp_pures. by iApply "HΦ".
Glen Mével's avatar
Glen Mével committed
946
947
  Qed.

948
  (* ICFP21: this is the spec of try_dequeue, as presented in Figure 5 of the
949
     paper, along with its proof. Same remarks as with try_enqueue. *)