-
Notifications
You must be signed in to change notification settings - Fork 1
/
proof_ms_composition.v
1820 lines (1608 loc) · 110 KB
/
proof_ms_composition.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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
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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
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
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
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
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
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
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From gpfsl.examples Require Import sflib.
From iris.algebra Require Import auth gset gmap agree.
From iris.base_logic Require Import lib.mono_nat.
From iris.proofmode Require Import tactics.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.examples.algebra Require Import mono_list.
From gpfsl.logic Require Import logatom atomics invariants.
From gpfsl.logic Require Import repeat_loop new_delete.
From gpfsl.examples Require Import map_seq loc_helper.
From gpfsl.examples.queue Require Import spec_composition code_ms_tailcas.
From gpfsl.examples.omo Require Import omo omo_preds append_only_loc.
Require Import iris.prelude.options.
#[local] Notation link := 0%nat (only parsing).
#[local] Notation data := 1%nat (only parsing).
#[local] Notation head := 0%nat (only parsing).
#[local] Notation tail := 1%nat (only parsing).
#[local] Notation null := 0%nat (only parsing).
(** Namespace for our internal invariant. See `QueueInternalInv`. *)
Definition msqN (N : namespace) (q: loc) := N .@ q.
Implicit Types
(qu st : queue_state) (node : event_id * Z * view * eView)
(M : eView) (Eh Et El : history loc_event)
(tid : thread_id) (γh γt γs γsh γst γcl γl γsl γm : gname)
(e et : event_id)
(es : list event_id)
(ninfo : event_id * gname * gname * val * loc)
(nidx : nat)
(CL : list (event_id * gname * gname * val * loc)).
(** * Ghost state construction *)
Class msqueueG Σ := MSQueueG {
ms_generalG :> omoGeneralG Σ;
ms_omoG :> omoSpecificG Σ qevent queue_state;
ms_aolocG :> appendOnlyLocG Σ;
ms_enq_list_monoG :> mono_listG (event_id * gname * gname * val * loc) Σ;
}.
Definition msqueueΣ : gFunctors := #[omoGeneralΣ; omoSpecificΣ qevent queue_state; appendOnlyLocΣ; mono_listΣ (event_id * gname * gname * val * loc)].
Global Instance subG_msqueueΣ {Σ} : subG msqueueΣ Σ → msqueueG Σ.
Proof. solve_inG. Qed.
(** * The invariant and local assertions *)
Section msqueue.
Context `{!noprolG Σ, !msqueueG Σ, !atomicG Σ}.
Local Existing Instances ms_omoG ms_aolocG ms_enq_list_monoG.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Local Open Scope nat_scope.
Definition AllTailMsgInner γg γt γcl et : vProp :=
∃ eVt gen enqid γl γsl (v : val) (l : loc) V (eVenq : omo_event qevent),
OmoEinfo γt et eVt ∗
OmoEinfo γg enqid eVenq ∗
⎡mono_list_idx_own γcl gen (enqid, γl, γsl, v, l)⎤ ∗
⌜ loc_event_msg eVt.(type) = (#l, V) ∧ eVenq.(sync) ⊑ V ⌝ ∗
@{V} OmoEview γl {[0]}.
Definition AllTailMsg γg γt γcl es : vProp :=
[∗ list] e ∈ es, AllTailMsgInner γg γt γcl e.
Definition AllHeadMsgInner γg γh γs γcl γm genh eh : vProp :=
∃ deqid eVh enqid γl γsl (v : val) (l : loc) (V : view) st Ml,
OmoEinfo γh eh eVh ∗
OmoCW γg γh deqid eh ∗ CWMonoValid γm deqid ∗
OmoLe γg enqid deqid ∗ (* gen of enq ≤ gen of deq *)
OmoSnap γg γs deqid st ∗
⎡mono_list_idx_own γcl genh (enqid, γl, γsl, v, l)⎤ ∗
⌜ loc_event_msg eVh.(type) = (#l, V) ⌝ ∗
@{V} OmoEview γl Ml ∗
match st with
| [] => emp
| hd :: _ => ∃ enqid' γl' γsl' (v' : val) (l' : loc) el omol',
OmoSnapOmo γl γsl omol' ∗
⎡mono_list_idx_own γcl (genh + 1) (enqid', γl', γsl', v', l')⎤ ∗
⌜ Ml = {[el; 0]} ∧ omo_write_op omol' = [0; el] ⌝
end.
Definition AllHeadMsg γg γh γs γcl γm es : vProp :=
[∗ list] gen↦e ∈ es, AllHeadMsgInner γg γh γs γcl γm gen e.
(* All [Enq] events in [M] are exactly ones in [CL] *)
Definition eView_Enq_exact γg M CL : vProp :=
([∗ list] ninfo ∈ CL, ⌜ ninfo.1.1.1.1 ∈ M ⌝) ∗
([∗ set] e ∈ M,
∃ eV,
OmoEinfo γg e eV ∗
match eV.(type) with
| Enq _ => ⌜ e ∈ CL.*1.*1.*1.*1 ⌝
| _ => True
end).
Definition HeadLastMsg γg γh γs γcl es esh CL : vProp :=
∃ eh deqid st gen CLh (eVh : omo_event loc_event) M',
OmoCW γg γh deqid eh ∗
OmoSnap γg γs deqid st ∗
OmoEinfo γh eh eVh ∗
⎡mono_list_lb_own γcl CLh⎤ ∗ ⌜ (length CLh = length esh + length st)%nat ⌝ ∗
@{(loc_event_msg eVh.(type)).2} OmoEview γg M' ∗
eView_Enq_exact γg M' CLh ∗
OmoUB γg M' deqid ∗
⌜ last esh = Some eh
∧ es !! gen = Some deqid
∧ st.*1.*1.*1 ++ drop (gen + 1) es = drop (length esh) CL.*1.*1.*1.*1 ⌝ ∗
([∗ list] gen↦state ∈ st,
∃ enqid' γl' γsl' (z' : Z) l' eV',
OmoEinfo γg enqid' eV' ∗
⎡mono_list_idx_own γcl (length esh + gen) (enqid', γl', γsl', #z', l')⎤ ∗
⌜ state = (enqid', z', eV'.(sync), eV'.(eview))
∧ eV'.(type) = Enq z'
∧ (z' > 0)%Z ⌝).
Definition NextFieldInfo γg γl γsl γcl es gen : vProp :=
∃ eVl0,
OmoEinfo γl 0 eVl0 ∗ ⌜ (loc_event_msg eVl0.(type)).1 = #0 ⌝ ∗
(⌜ es = [0] ⌝ ∨
(∃ el eVl enqid' γl' γsl' (v' : val) (l' : loc) (eVenq' : omo_event qevent) (V' : view),
⌜ es = [0; el] ∧ el ≠ 0 ∧ loc_event_msg eVl.(type) = (#l', V') ⌝ ∗
meta l' nroot (enqid', γl', γsl', v') ∗
⎡mono_list_idx_own γcl (gen + 1) (enqid', γl', γsl', v', l')⎤ ∗
OmoEinfo γl el eVl ∗
OmoEinfo γg enqid' eVenq' ∗ ⌜ V' = eVenq'.(sync) ⌝ ∗
OmoCW γg γl enqid' el ∗
OmoHb γg γl enqid' el ∗
@{V'} (OmoEview γl {[el; 0]} ∗ OmoEview γl' {[0]}) ∗
(∃ q, @{V'} (l' >> data) ↦{q} v'))).
Definition AllNodesInner γg γcl gen ninfo : vProp :=
∃ enqid eVenq γl γsl v l El omol mol,
⌜ ninfo = (enqid, γl, γsl, v, l) ⌝ ∗
meta l nroot (enqid, γl, γsl, v) ∗
OmoAuth γl γsl (1/2) El omol mol _ ∗
OmoEinfo γg enqid eVenq ∗
(∃ Vbl, @{Vbl} append_only_loc (l >> link) γl ∅ cas_only) ∗
NextFieldInfo γg γl γsl γcl (omo_write_op omol) gen ∗
⌜ ∃ (z : Z), v = #z ∧ eVenq.(type) = Enq z ∧ (z > 0)%Z ⌝.
Definition AllNodes γg γcl CL : vProp :=
[∗ list] gen↦ninfo ∈ CL, AllNodesInner γg γcl gen ninfo.
(* This is used to derive the fact that every non-last node has nonnull value written in next field *)
Definition PrevLinkInfo γg γcl gen ninfo : vProp :=
match gen with
| 0 => emp
| S gen' => ∃ enqid γl γsl v l enqid' γl' γsl' (v' : val) (l' : loc) omol',
⌜ ninfo = (enqid, γl, γsl, v, l) ⌝ ∗
⎡mono_list_idx_own γcl gen' (enqid', γl', γsl', v', l')⎤ ∗
OmoLe γg enqid' enqid ∗
OmoSnapOmo γl' γsl' omol' ∗
⌜ length omol' = 2 ⌝
end.
Definition AllPrevLinks γg γcl CL : vProp :=
[∗ list] gen↦ninfo ∈ CL, PrevLinkInfo γg γcl gen ninfo.
(* Each [enq] event observes all previous [enq] events *)
Definition EnqSeen γg γcl CL : vProp :=
[∗ list] gen↦ninfo ∈ CL,
∃ CL' (eVl : omo_event qevent) M,
⎡mono_list_lb_own γcl CL'⎤ ∗ ⌜ length CL' = (gen + 1)%nat ⌝ ∗
OmoEinfo γg ninfo.1.1.1.1 eVl ∗
OmoUB γg ({[ninfo.1.1.1.1]} ∪ eVl.(eview) ∪ M) ninfo.1.1.1.1 ∗
@{eVl.(sync)} OmoEview γg ({[ninfo.1.1.1.1]} ∪ eVl.(eview) ∪ M) ∗
eView_Enq_exact γg ({[ninfo.1.1.1.1]} ∪ eVl.(eview) ∪ M) CL'.
Definition AllEvents γg γh γcl γm E : vProp :=
[∗ list] e↦eV ∈ E,
match eV.(type) with
| Enq _ => emp
| _ => ∃ e' eh eh',
OmoHb γg γh e eh ∗ OmoEq γg e e' ∗ OmoEq γh eh eh' ∗
OmoCW γg γh e' eh' ∗ CWMonoValid γm e'
end.
Definition QueueInternalInv γg q E : vProp :=
∃ γh γt γs γsh γst γcl γm Eh Et omo omoh omot stlist moh mot CL Mono,
meta q nroot (γh,γt,γsh,γst,γcl,γm) ∗
OmoAuth γg γs (1/2) E omo stlist _ ∗
OmoAuth γh γsh (1/2) Eh omoh moh _ ∗
OmoAuth γt γst (1/2) Et omot mot _ ∗
⎡mono_list_auth_own γcl 1 CL⎤ ∗
(∃ Vbh, @{Vbh} append_only_loc (q >> head) γh ∅ cas_only) ∗
(∃ Vbt, @{Vbt} append_only_loc (q >> tail) γt ∅ cas_only) ∗
AllNodes γg γcl CL ∗ AllPrevLinks γg γcl CL ∗
AllHeadMsg γg γh γs γcl γm (omo_write_op omoh) ∗
HeadLastMsg γg γh γs γcl (omo_write_op omo) (omo_write_op omoh) CL ∗
AllTailMsg γg γt γcl (omo_write_op omot) ∗
CWMono γg γh γm Mono ∗
EnqSeen γg γcl CL ∗
AllEvents γg γh γcl γm E.
Definition QueueInv (γg γs : gname) (q : loc) (E : history qevent) omo stlist : vProp := OmoAuth γg γs (1/2)%Qp E omo stlist _.
Definition InternalInv_inner γg q : vProp := ∃ E, QueueInternalInv γg q E.
Definition InternInv N γg q := inv (msqN N q) (InternalInv_inner γg q).
Definition QueueLocal (N : namespace) γg q M : vProp :=
∃ γh γt γsh γst γcl γm Mh Mt CL,
meta q nroot (γh,γt,γsh,γst,γcl,γm) ∗
InternInv N γg q ∗
OmoEview γg M ∗
OmoEview γh Mh ∗
OmoEview γt Mt ∗
⎡mono_list_lb_own γcl CL⎤ ∗
eView_Enq_exact γg M CL ∗
⌜ CL ≠ [] ⌝.
Local Instance eView_Enq_exact_persistent γg M CL : Persistent (eView_Enq_exact γg M CL).
Proof.
apply @bi.sep_persistent; [apply _|].
apply big_sepS_persistent. intros. apply @bi.exist_persistent. intros.
apply @bi.sep_persistent; [apply _|]. destruct (x0.(type)); apply _.
Qed.
Local Instance eView_Enq_exact_objective γg M CL : Objective (eView_Enq_exact γg M CL).
Proof.
apply sep_objective; try apply _.
apply big_sepS_objective; intros. apply exists_objective; intros.
apply sep_objective; try apply _. destruct (x.(type)); apply _.
Qed.
Local Instance eView_Enq_exact_timeless γg M CL : Timeless (eView_Enq_exact γg M CL).
Proof.
apply @bi.sep_timeless; try apply _.
apply big_sepS_timeless; intros. apply @bi.exist_timeless; intros.
apply @bi.sep_timeless; try apply _. destruct (x0.(type)); apply _.
Qed.
Local Instance PrevLinkInfo_objective γg γcl gen ninfo : Objective (PrevLinkInfo γg γcl gen ninfo).
Proof. destruct gen; apply _. Qed.
Local Instance PrevLinkInfo_persistent γg γcl gen ninfo : Persistent (PrevLinkInfo γg γcl gen ninfo).
Proof. destruct gen; apply _. Qed.
Local Instance PrevLinkInfo_timeless γg γcl gen ninfo : Timeless (PrevLinkInfo γg γcl gen ninfo).
Proof. destruct gen; apply _. Qed.
Local Instance AllHeadMsgInner_persistent γg γh γs γcl γm genh eh : Persistent (AllHeadMsgInner γg γh γs γcl γm genh eh).
Proof.
repeat (apply @bi.exist_persistent; intros).
repeat (apply @bi.sep_persistent; [apply _|]).
destruct x7; apply _.
Qed.
Local Instance AllHeadMsgInner_objective γg γh γs γcl γm genh eh : Objective (AllHeadMsgInner γg γh γs γcl γm genh eh).
Proof.
repeat (apply exists_objective; intros).
repeat (apply sep_objective; try apply _).
destruct x7; apply _.
Qed.
Local Instance AllHeadMsgInner_timeless γg γh γs γcl γm genh eh : Timeless (AllHeadMsgInner γg γh γs γcl γm genh eh).
Proof.
repeat (apply @bi.exist_timeless; intros).
repeat (apply @bi.sep_timeless; try apply _).
destruct x7; apply _.
Qed.
Local Instance QueueInternalInv_objective γg q E : Objective (QueueInternalInv γg q E).
Proof.
repeat (apply exists_objective; intros).
repeat (apply sep_objective; [apply _|]).
apply big_sepL_objective. intros. destruct (x16.(type)); apply _.
Qed.
Local Instance QueueInternalInv_timeless γg q E : Timeless (QueueInternalInv γg q E).
Proof.
repeat (apply @bi.exist_timeless; intros).
repeat (apply @bi.sep_timeless; [apply _|]).
apply big_sepL_timeless. intros. destruct (x16.(type)); apply _.
Qed.
Local Instance AllEvents_persistent γg γh γcl γm E : Persistent (AllEvents γg γh γcl γm E).
Proof. apply big_sepL_persistent. intros. destruct (x.(type)); apply _. Qed.
Local Instance QueueLocal_persistent N γg q M : Persistent (QueueLocal N γg q M) := _.
Lemma NextFieldInfo_dup γg γl γsl γcl es gen :
NextFieldInfo γg γl γsl γcl es gen -∗ NextFieldInfo γg γl γsl γcl es gen ∗ NextFieldInfo γg γl γsl γcl es gen.
Proof.
iDestruct 1 as (eV0) "(#e0✓eV0 & %eV0EV & [%Hes|CASE2])".
- iSplitL; repeat iExists _; iFrame "∗#%".
- iDestruct "CASE2" as (el eVl enqid' γl' γsl' v' l' eVenq' V' EQ) "(#H1 & #H2 & #H3 & #H4 & %H4 & #H5 & #H7 & #H8 & [%q [l'↦1 l'↦2]])".
iSplitL "l'↦1"; iExists eV0; iFrame "#%"; iRight; iExists el,eVl,enqid',γl',γsl',v',l',eVenq';
iExists V'; iFrame "#%"; eauto with iFrame.
Qed.
Lemma gen_le_enq_deq γg γh γs γsh γcl γl γsl γm q Eh v l CL omoh moh gen1 gen2 enqid deqid eh Mono :
CL !! gen1 = Some (enqid, γl, γsl, v, l) →
omo_write_op omoh !! gen2 = Some eh →
gen1 ≤ gen2 →
AllHeadMsg γg γh γs γcl γm (omo_write_op omoh) -∗
OmoCW γg γh deqid eh -∗
CWMonoValid γm deqid -∗
OmoAuth γh γsh q Eh omoh moh _ -∗
CWMono γg γh γm Mono -∗
⎡mono_list_auth_own γcl 1 CL⎤ -∗
OmoLe γg enqid deqid.
Proof.
iIntros "%Hgen1 %Hgen2 %LE".
iInduction LE as [|gen2'] "IH" forall (eh deqid Hgen2); iIntros "AllHeadMsg #deqid↦eh #MONO✓deqid Mh● MONO CL●".
- iDestruct (big_sepL_lookup with "AllHeadMsg") as "Inner"; [exact Hgen2|].
iDestruct "Inner" as (??????????) "(_ & #deqid'↦eh & _ & #enqid≤deqid' & _ & #CL@gen1 & _)".
iDestruct (mono_list_auth_idx_lookup with "CL● CL@gen1") as %Hgen1'.
rewrite Hgen1 in Hgen1'. inversion Hgen1'. subst enqid0 γl0 γsl0 v0 l0. clear Hgen1'.
iDestruct (OmoCW_agree_2 with "deqid↦eh deqid'↦eh") as %[_ <-]. done.
- have [eh' Hgen2'] : is_Some (omo_write_op omoh !! gen2').
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hgen2. lia. }
iDestruct (big_sepL_lookup with "AllHeadMsg") as "#Inner"; [exact Hgen2'|].
iDestruct "Inner" as (deqid' ?????????) "(_ & deqid'↦eh' & #MONO✓deqid' & _ & #CL@gen2' & _)".
iDestruct ("IH" with "[] AllHeadMsg deqid'↦eh' MONO✓deqid' Mh● MONO CL●") as "#enqid≤deqid'"; [done|].
iDestruct (OmoLe_get _ _ _ _ _ _ (wr_event gen2') (wr_event (S gen2')) with "Mh●") as "#eh'≤eh".
{ by rewrite lookup_omo_wr_event. } { by rewrite lookup_omo_wr_event. } { simpl. lia. }
iDestruct (CWMono_acc with "MONO MONO✓deqid' MONO✓deqid deqid'↦eh' deqid↦eh eh'≤eh") as "#deqid'≤deqid".
iDestruct (OmoLe_trans with "enqid≤deqid' deqid'≤deqid") as "#enqid≤deqid". iFrame "#".
Qed.
Lemma gen_le_enq_enq γg γs γcl q (E : history qevent) omo stlist CL eidx1 eidx2 gen1 gen2 enqid1 enqid2 γl1 γl2 γsl1 γsl2 v1 v2 l1 l2 :
CL !! gen1 = Some (enqid1, γl1, γsl1, v1, l1) →
CL !! gen2 = Some (enqid2, γl2, γsl2, v2, l2) →
gen1 ≤ gen2 →
lookup_omo omo eidx1 = Some enqid1 →
lookup_omo omo eidx2 = Some enqid2 →
AllPrevLinks γg γcl CL -∗
OmoAuth γg γs q E omo stlist _ -∗
⎡mono_list_auth_own γcl 1 CL⎤ -∗
⌜ gen_of eidx1 ≤ gen_of eidx2 ⌝.
Proof.
iIntros "%Hgen1 %Hgen2 %LE %Heidx1 %Heidx2 #AllPrevLinks M● CL●".
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iInduction LE as [|gen2'] "IH" forall (eidx2 enqid2 γl2 γsl2 v2 l2 Hgen2 Heidx2).
- rewrite Hgen1 in Hgen2. inversion Hgen2. subst enqid2 γl2 γsl2 v2 l2.
by specialize (lookup_omo_inj _ _ _ _ _ _ OMO_GOOD Heidx1 Heidx2) as <-.
- have [ninfo Hgen2'] : is_Some (CL !! gen2').
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hgen2. lia. }
destruct ninfo as [[[[enqid3 γl3] γsl3] v3] l3].
iDestruct (big_sepL_lookup with "AllPrevLinks") as "Sgen2Info"; [exact Hgen2|].
iDestruct "Sgen2Info" as (??????????) "(%& %EQ & CL@gen2' & enqid3≤enqid2 & _)".
inversion EQ. subst enqid γl γsl v l. clear EQ.
iDestruct (mono_list_auth_idx_lookup with "CL● CL@gen2'") as %Hgen2''.
rewrite Hgen2' in Hgen2''. inversion Hgen2''. subst enqid' γl' γsl' v' l'. clear Hgen2''.
iDestruct (OmoAuth_OmoLe_l with "M● enqid3≤enqid2") as %[eidx3 Heidx3].
iDestruct ("IH" with "[] [] M● CL●") as %LE1; [iPureIntro; exact Hgen2'|iPureIntro; exact Heidx3|].
iDestruct (OmoLe_Le with "M● enqid3≤enqid2") as %LE2; try done. iPureIntro. lia.
Qed.
Lemma eView_Enq_exact_insert_nonenq γg M CL e eV :
(∀ v, eV.(type) ≠ Enq v) →
eView_Enq_exact γg M CL -∗
OmoEinfo γg e eV -∗
eView_Enq_exact γg ({[e]} ∪ M) CL.
Proof.
iIntros "%NEQEnq [#M_CL1 M_CL2] #e✓eV".
destruct (decide (e ∈ M)) as [IN|NIN].
{ replace ({[e]} ∪ M) with M; [|set_solver]. iFrame "∗#". }
iSplitL "M_CL1".
- iApply big_sepL_intro. iIntros "!> % % %".
iDestruct (big_sepL_lookup with "M_CL1") as "%"; [done|]. iPureIntro. set_solver.
- rewrite big_sepS_union; [|set_solver]. iFrame.
rewrite big_sepS_singleton. iExists eV. iFrame "#". destruct (eV.(type)); try done.
by specialize (NEQEnq v).
Qed.
Lemma eView_Enq_exact_union γg γcl M1 M2 CL1 CL2 :
eView_Enq_exact γg M1 CL1 -∗
eView_Enq_exact γg M2 CL2 -∗
⎡mono_list_lb_own γcl CL1⎤ -∗
⎡mono_list_lb_own γcl CL2⎤ -∗
∃ CL, eView_Enq_exact γg (M1 ∪ M2) CL ∗ ⎡mono_list_lb_own γcl CL⎤ ∗ ⌜ (length CL = (length CL1) `max` (length CL2))%nat ⌝.
Proof.
iIntros "#M1_CL1 #M2_CL2 #CL1◯ #CL2◯".
iDestruct (mono_list_lb_valid with "CL1◯ CL2◯") as %[LECL1CL2|LECL2CL1].
- iExists CL2. iFrame "CL2◯". iSplitR; [|by apply prefix_length in LECL1CL2; iPureIntro; lia]. iSplit.
+ rewrite big_sepL_forall. iIntros "%gen %ninfo %Hninfo".
iDestruct "M2_CL2" as "[M2_CL2 _]". iDestruct (big_sepL_lookup with "M2_CL2") as %M2INCL; [done|]. iPureIntro. set_solver.
+ iApply big_sepS_intro. iIntros "%e %eIncl !>". rewrite elem_of_union in eIncl. destruct eIncl as [eIncl|eIncl].
* iDestruct "M1_CL1" as "[_ M1_CL1]". iDestruct (big_sepS_elem_of with "M1_CL1") as (eV) "[e✓eV CASE]"; [done|].
iExists eV. iFrame "e✓eV". destruct (eV.(type)); try done. iDestruct "CASE" as %eInclCL. iPureIntro.
eapply elem_of_prefix; [done|]. do 4 apply fmap_prefix. done.
* iDestruct "M2_CL2" as "[_ M2_CL2]". iDestruct (big_sepS_elem_of with "M2_CL2") as "H"; [done|]. iFrame "H".
- iExists CL1. iFrame "CL1◯". iSplitR; [|by apply prefix_length in LECL2CL1; iPureIntro; lia]. iSplit.
+ rewrite big_sepL_forall. iIntros "%gen %ninfo %Hninfo".
iDestruct "M1_CL1" as "[M1_CL1 _]". iDestruct (big_sepL_lookup with "M1_CL1") as %M2INCL; [done|]. iPureIntro. set_solver.
+ iApply big_sepS_intro. iIntros "%e %eIncl !>". rewrite elem_of_union in eIncl. destruct eIncl as [eIncl|eIncl].
* iDestruct "M1_CL1" as "[_ M1_CL1]". iDestruct (big_sepS_elem_of with "M1_CL1") as "H"; [done|]. iFrame "H".
* iDestruct "M2_CL2" as "[_ M2_CL2]". iDestruct (big_sepS_elem_of with "M2_CL2") as (eV) "[e✓eV CASE]"; [done|].
iExists eV. iFrame "e✓eV". destruct (eV.(type)); try done. iDestruct "CASE" as %eInclCL. iPureIntro.
eapply elem_of_prefix; [done|]. do 4 apply fmap_prefix. done.
Qed.
Local Tactic Notation "simplify_meta6" "with" constr(Hs) :=
iDestruct (meta_agree with Hs) as %[[[[[-> ->]%pair_inj ->]%pair_inj ->]%pair_inj ->]%pair_inj ->]%pair_inj.
Local Tactic Notation "simplify_meta4" "with" constr(Hs) :=
iDestruct (meta_agree with Hs) as %[[[-> ->]%pair_inj ->]%pair_inj ->]%pair_inj.
Lemma QueueInv_Linearizable_instance :
∀ γg γs q E omo stlist, QueueInv γg γs q E omo stlist ⊢ ⌜ Linearizability_omo E omo stlist ⌝.
Proof. intros. iIntros "M●". by iDestruct (OmoAuth_Linearizable with "M●") as %?. Qed.
Lemma QueueInv_OmoAuth_acc_instance :
∀ γg γs q E omo stlist,
QueueInv γg γs q E omo stlist
⊢ OmoAuth γg γs (1/2)%Qp E omo stlist _ ∗ (OmoAuth γg γs (1/2)%Qp E omo stlist _ -∗ QueueInv γg γs q E omo stlist).
Proof. intros. iIntros "M●". iFrame. iIntros "M●". iFrame. Qed.
Lemma QueueLocal_OmoEview_instance :
∀ N γg q M, QueueLocal N γg q M ⊢ OmoEview γg M.
Proof. intros. by iDestruct 1 as (?????????) "(_ & _ & M◯ & _)". Qed.
Lemma new_queue_spec :
new_queue_spec' new_queue QueueLocal QueueInv.
Proof.
iIntros (N tid V0 Φ) "⊒V0 Post". wp_lam.
(* Allocate sentinel node *)
wp_apply wp_new; [done..|].
iIntros (n) "([n†|%] & n↦ & Hmn & _)"; [|done]. rewrite own_loc_na_vec_singleton.
wp_pures. rewrite -[Z.to_nat 0]/(0%nat) shift_0. wp_write.
(* Allocate head/tail location *)
wp_apply wp_new; [done..|].
iIntros (q) "([q†|%] & q↦ & Hmq & _)"; [|done].
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iDestruct "q↦" as "[hd↦ tl↦]".
wp_pures. rewrite -[Z.to_nat 0]/(0%nat) shift_0. wp_write. wp_pures. rewrite -[Z.to_nat 1]/(1%nat). wp_apply wp_fupd. wp_write.
(* Create [append_only_loc] *)
iMod (append_only_loc_cas_only_from_na_rel with "⊒V0 n↦") as (γln γsn Vn eVn0)
"(#⊒Vn & Mn● & [#Mn◯ #⊒Vn@V0] & omon↦ & WCOMMITn & #en0✓eVn0 & [%eVn0EV _])"; [done|].
iMod (append_only_loc_cas_only_from_na_rel with "⊒Vn tl↦")
as (γt γst Vt eVt0) "(#⊒Vt & Mt● & [#Mt◯ #⊒Vn@Vt] & omot↦ & WCOMMITt & #et0✓eVt0 & [%eVt0EV _])"; [done|].
iMod (append_only_loc_cas_only_from_na_rel with "⊒Vt hd↦")
as (γh γsh Vh eVh0) "(#⊒Vh & Mh● & [#Mh◯ #⊒Vt@Vh] & omoh↦ & WCOMMITh & #eh0✓eVh0 & [%eVh0EV %eVh0SYNC])"; [done|].
iAssert (⌜ V0 ⊑ Vn ∧ Vn ⊑ Vt ∧ Vt ⊑ Vh ⌝)%I with "[-]" as %(LeV0Vn & LeVnVt & LeVtVh).
{ rewrite !view_at_unfold !monPred_at_in. iDestruct "⊒Vn@V0" as %?. iDestruct "⊒Vn@Vt" as %?. by iDestruct "⊒Vt@Vh" as %?. }
have LeV0Vt : V0 ⊑ Vt by solve_lat.
set Menq := {[0%nat]}.
set eVenq := mkOmoEvent (Enq 1) Vt Menq.
(* Initial events are two consecutive events: Dummy Enqueue & Dummy Dequeue *)
iMod (@OmoAuth_alloc _ _ _ _ _ eVenq ([] ++ [(0, 1%Z, eVenq.(sync), eVenq.(eview))]) _ _ queue_interpretable with "WCOMMITn")
as (γg γs) "(M● & #M◯1@Vt & #e0↦en0 & #e0✓eVenq & #e0↪st0 & WCOMMIT1)".
{ by eapply queue_step_Enq. } { done. }
iDestruct (OmoHbToken_finish with "M●") as "M●".
set Mdeq := {[1%nat]} ∪ Menq.
set eVdeq := mkOmoEvent (Deq 1) Vh Mdeq.
iDestruct (view_at_mono_2 _ Vh with "M◯1@Vt") as "#M◯1@Vh"; [by subst eVenq|].
iMod (OmoAuth_insert_last with "M● M◯1@Vh WCOMMITh []") as "(M● & #M◯2@Vh & #e1↦eh0 & #e1✓eVdeq & #e1↪st1 & WCOMMIT2)".
{ have ? : step 1%nat eVdeq [(0, 1%Z, eVenq.(sync), eVenq.(eview))] []; [|by iPureIntro; split_and!].
eapply queue_step_Deq; try done. subst eVenq eVdeq Mdeq Menq. simpl. set_solver-. }
iMod (OmoHb_new_1 with "M● e1✓eVdeq eh0✓eVh0") as "[M● #e1⊒eh0]"; [rewrite eVh0SYNC; solve_lat|].
iDestruct (OmoHbToken_finish with "M●") as "M●".
iDestruct (OmoLe_get_append_w with "M● e0✓eVenq") as "#e0≤e1".
iMod (CWMono_new γg γh) as (γm) "MONO".
iMod (CWMono_insert_last_last (wr_event 1) with "MONO M● Mh● e1↦eh0") as "(MONO & #MONO✓e1 & M● & Mh●)"; [done|done|].
set CL := [(0, γln, γsn, #1, n)].
iMod (mono_list_own_alloc CL) as (γcl) "[CL● #CL◯]".
iMod (meta_set _ _ (γh,γt,γsh,γst,γcl,γm) nroot with "Hmq") as "#HM"; [done|].
iMod (meta_set _ _ (0,γln,γsn,#1) nroot with "Hmn") as "#HMn"; [done|].
iAssert (eView_Enq_exact γg Mdeq CL)%I with "[-]" as "#M_CL".
{ subst Mdeq Menq CL. iSplit.
- rewrite big_sepL_singleton. iPureIntro. set_solver-.
- iApply big_sepS_intro. iIntros "%e %eIn". destruct (decide (e = 0)) as [->|NEQ]; iModIntro.
+ iExists eVenq. iFrame "e0✓eVenq". subst eVenq. iPureIntro. set_solver-.
+ have EQ : e = 1 by set_solver. subst e. iExists eVdeq. iFrame "e1✓eVdeq". }
iAssert (OmoUB γg Mdeq 1)%I with "[-]" as "#MAXgen_e1".
{ subst Mdeq Menq. rewrite /OmoUB big_sepS_forall.
iIntros "%e %eIn". destruct (decide (e = 0)) as [->|NEQ]; [done|].
have EQ : e = 1 by set_solver. subst e.
iDestruct (OmoEq_get_from_Einfo with "e1✓eVdeq") as "e1=e1".
iDestruct (OmoLe_get_from_Eq with "e1=e1") as "e1≤e1". done. }
iDestruct "M●" as "[M● M●']".
iMod (inv_alloc (msqN N q) _ (InternalInv_inner γg q) with "[-M●' Post WCOMMIT1 WCOMMIT2]") as "#I".
{ iNext. repeat iExists _. iFrame "HM Mh● MONO". iFrame.
iDestruct (view_at_intro with "omon↦") as (Vbn) "[_ omon↦]".
iDestruct (view_at_intro with "omoh↦") as (Vbh) "[_ omoh↦]".
iDestruct (view_at_intro with "omot↦") as (Vbt) "[_ omot↦]".
iSplitL "omoh↦"; [rewrite shift_0; eauto with iFrame|]. iSplitL "omot↦"; [eauto with iFrame|].
rewrite !omo_append_w_write_op /=. subst CL.
iSplitL; repeat iSplit; try by rewrite big_sepL_nil.
- rewrite /AllNodes big_sepL_singleton. repeat iExists _. iFrame "HMn Mn● e0✓eVenq". iSplitR; [done|].
iSplitL "omon↦"; [rewrite shift_0; eauto with iFrame|]. iSplitL; [|by iPureIntro; exists 1; split_and!].
repeat iExists _. iFrame "en0✓eVn0". iSplitL; [by rewrite eVn0EV|]. iLeft. rewrite omo_append_w_write_op /=. done.
- done.
- iExists 1,eVh0,0,γln,γsn,#1,n,Vh. iExists [],{[0]}.
rewrite (@mono_list_idx_own_get _ _ _ _ _ 0); [|done].
iFrame "#". by rewrite eVh0EV.
- iExists 0,1,[],1,[(0,γln,γsn,#1,n)],eVh0,Mdeq. rewrite eVh0EV. simpl. by iFrame "#".
- iExists eVt0,0,0,γln,γsn,#1,n,Vt. iExists eVenq.
rewrite (@mono_list_idx_own_get _ _ _ _ _ 0); [|done].
iFrame "#". iPureIntro. rewrite eVt0EV. done.
- iExists [(0,γln,γsn,#1,n)],eVenq,{[0]}. subst eVenq. simpl. iFrame "#".
have EQ : {[0]} ∪ Menq ∪ {[0]} = {[0]} by set_solver. rewrite !EQ. clear EQ.
iFrame "#". iSplit; [done|]. iSplit; last iSplit.
+ rewrite /OmoUB big_sepS_singleton.
iDestruct (OmoEq_get_from_Einfo with "e0✓eVenq") as "e0=e0".
by iDestruct (OmoLe_get_from_Eq with "e0=e0") as "e0≤e0".
+ rewrite big_sepL_singleton. set_solver-.
+ rewrite big_sepS_singleton. iExists _. iFrame "e0✓eVenq". iPureIntro. set_solver-.
- by subst eVenq.
- repeat iExists _. iFrame "e1↦eh0 MONO✓e1 e1⊒eh0". by iSplit; [iApply OmoEq_get_from_Einfo|iApply (@OmoEq_get_from_Einfo loc_event)]. }
iDestruct ("Post" $! γg γs q Vt Vh Menq Mdeq with "[M●' WCOMMIT1 WCOMMIT2]") as "HΦ"; [|iModIntro; by iApply "HΦ"].
iFrame "⊒Vh WCOMMIT1 WCOMMIT2 M●'". iSplit; [|done]. repeat iExists _. by iFrame "#".
Qed.
Lemma try_enq_spec :
try_enq_spec' try_enq QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg M V0 v VGTZ. iIntros "#⊒V0 #QueueLocal" (Φ) "AU".
iDestruct "QueueLocal" as (?????? Mh Mt CL0) "(HM & QInv & M◯ & Mh◯ & Mt◯ & CL◯0 & M_CL0 & %CL0NEQ)".
iCombine "M◯ Mh◯" as "MMh◯".
iDestruct (view_at_intro_incl with "MMh◯ ⊒V0") as (V0') "(#⊒V0' & %LEV0V0' & [#M◯@V0' #Mh◯@V0'])".
wp_lam. wp_apply wp_new; [done..|].
iIntros (n) "([n†|%] & n↦ & Hms & _)"; [|done].
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iDestruct "n↦" as "[n↦ n_1↦]".
wp_pures. rewrite -[Z.to_nat 1]/(1%nat). wp_write. wp_pures. rewrite -[Z.to_nat 0]/(0%nat). rewrite shift_0. wp_write.
iLöb as "IH". wp_pures. rewrite -[Z.to_nat 1]/(1%nat). wp_bind (!ᵃᶜ #(q >> tail))%E.
(* Inv access 1 *)
iInv "QInv" as (E1) ">H" "Hclose".
iDestruct "H" as (?? γs1 ???? Eh1 Et1 omo1)
"(%omoh1 & %omot1 & %stlist1 & %moh1 & %mot1 & %CL1 & %Mono1 & HM' & M●1 & Mh●1 & Mt●1 & CL●1 & omoh↦1 & (%Vbt1 & omot↦1) & H)".
iDestruct "H" as "(AllNodes1 & AllPrevLinks & AllHeadMsg1 & HeadLastMsg1 & #AllTailMsg1 & MONO1 & EnqSeen1 & AllEvents1)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (OmoSnapOmo_get with "Mt●1") as "#OMOt1◯".
wp_apply (append_only_loc_acquire_read with "[$Mt●1 $Mt◯ $omot↦1 $⊒V0']"); [solve_ndisj|].
iIntros (et1 gent1 vt1 Vt1 V1 eVt1 eVtn1)
"(Pures & Mt●1 & _ & #MAXgen_et1 & #et1✓eVt1 & #etn1✓eVtn1 & #et1=etn1 & #⊒V1 & #Mt◯1'@V1 & omot↦1)".
iDestruct "Pures" as %(Eqgent1 & eVt1EV & LEV0'Vt1V1 & eVtn1EV & eVtn1SYNC).
iDestruct (big_sepL_lookup with "AllTailMsg1")
as (eVt1' gen1 enqid1 γl1 γsl1 v1 l1 Vt1' eVenq1) "(#et1✓eVt1' & #enqid1✓eVenq1 & #CL@gen1 & [%eVt1'EV %LeSYNCVtl] & #Ml1◯@Vt1)"; [exact Eqgent1|].
iDestruct (OmoEinfo_agree with "et1✓eVt1 et1✓eVt1'") as %<-. rewrite eVt1EV in eVt1'EV. inversion eVt1'EV. subst vt1 Vt1'. clear eVt1'EV.
iMod ("Hclose" with "[-AU n† n↦ n_1↦ Hms]") as "_".
{ repeat iExists _. iFrame "HM". iFrame. rewrite omo_insert_r_write_op. iFrame "AllTailMsg1". eauto with iFrame. }
iModIntro. wp_pures. rewrite -[Z.to_nat 0]/(0%nat). wp_bind (!ᵃᶜ #(l1 >> link))%E.
(* Inv access 2 *)
iInv "QInv" as (E2) ">H" "Hclose".
iDestruct "H" as (?? γs2 ???? Eh2 Et2 omo2)
"(%omoh2 & %omot2 & %stlist2 & %moh2 & %mot2 & %CL2 & %Mono2 & HM' & M●2 & Mh●2 & Mt●2 & CL●2 & omoh↦2 & omot↦2 & H)".
iDestruct "H" as "(AllNodes2 & AllPrevLinks2 & AllHeadMsg2 & HeadLastMsg2 & AllTailMsg2 & MONO2 & EnqSeen2 & AllEvents2)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (mono_list_auth_idx_lookup with "CL●2 CL@gen1") as %HCL2gen1.
iDestruct (big_sepL_lookup_acc with "AllNodes2") as "[Inner Close]"; [exact HCL2gen1|].
iDestruct "Inner" as (? eVenq1' ???? El1 omol1 mol1) "(%EQ & #HMl1 & Ml1● & #enqid1✓eVenq1' & (%Vbl1 & omol1↦) & Fieldl1 & Hgen1)".
inversion EQ. subst enqid γl γsl v0 l. clear EQ.
iDestruct (OmoEinfo_agree with "enqid1✓eVenq1 enqid1✓eVenq1'") as %<-.
have LEVt1V1 : Vt1 ⊑ V1 by solve_lat.
iDestruct (view_at_mono_2 _ V1 with "Ml1◯@Vt1") as "#Ml1◯@V1"; [done|].
iDestruct (view_at_elim with "⊒V1 Ml1◯@V1") as "Ml1◯".
wp_apply (append_only_loc_acquire_read with "[$Ml1● $Ml1◯ $omol1↦ $⊒V1]"); [solve_ndisj|].
iIntros (el2 genl2 vl2 Vl2 V2 eVl2 eVln2)
"(Pures & Ml1● & _ & #MAXgen_el2 & #el2✓eVl2 & #eln2✓eVln2 & #el2=eln2 & #⊒V2 & #Ml1◯'@V2 & omol1↦)".
iDestruct "Pures" as %(Eqgenl2 & eVl2EV & LEV1Vl2V2 & eVln2EV & eVln2SYNC).
destruct genl2; last first.
{ (* Read pointer to next node from next field. Retry *)
iDestruct (NextFieldInfo_dup with "Fieldl1") as "[Fieldl1 Fieldl1']".
iDestruct "Fieldl1" as (eVl0) "(#e0✓eVl0 & %eVl0EV & [%Homol1|CASE2])".
{ rewrite Homol1 in Eqgenl2. inversion Eqgenl2. }
iDestruct "CASE2" as (?? enqid2 γl2 γsl2 v2 l2 eVenq2 ?)
"((%Homol1 & %NZel2 & %eVl2EV') & _ & #CL@Sgen1 & #el2✓eVl2' & #enqid2✓eVenq2 & %EQ & _ & _ & [_ #Ml2◯@Vl2] & _)".
iAssert (⌜ el = el2 ⌝)%I with "[-]" as %->. { rewrite Homol1 /= in Eqgenl2. by destruct genl2; inversion Eqgenl2. }
iDestruct (OmoEinfo_agree with "el2✓eVl2 el2✓eVl2'") as %<-.
rewrite eVl2EV in eVl2EV'. inversion eVl2EV'. subst vl2 V' Vl2. clear eVl2EV'.
iDestruct ("Close" with "[Ml1● omol1↦ Fieldl1' Hgen1]") as "AllNodes2".
{ repeat iExists _. iFrame "HMl1 enqid1✓eVenq1 Ml1●". rewrite omo_insert_r_write_op. iFrame. iSplitR; [done|eauto with iFrame]. }
iMod ("Hclose" with "[-AU n† n↦ n_1↦ Hms]") as "_". { repeat iExists _. iFrame "HM". iFrame. }
iModIntro. wp_pures. rewrite -[Z.to_nat 1]/(1%nat). wp_bind (casʳᵉˡ(_, _, _))%E.
(* Inv access 3 *)
iInv "QInv" as (E3) ">H" "Hclose".
iDestruct "H" as (?? γs3 ???? Eh3 Et3 omo3)
"(%omoh3 & %omot3 & %stlist3 & %moh3 & %mot3 & %CL3 & %Mono3 & HM' & M●3 & Mh●3 & Mt●3 & CL●3 & omoh↦3 & [%Vbt3 omot↦3] & H)".
iDestruct "H" as "(AllNodes3 & AllPrevLinks3 & AllHeadMsg3 & HeadLastMsg3 & #AllTailMsg3 & MONO3 & EnqSeen3 & AllEvents3)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (OmoAuth_OmoSnapOmo with "Mt●3 OMOt1◯") as %[_ LEomot1wr].
iDestruct (OmoAuth_wf with "Mt●3") as %[OMO_GOODt3 _].
wp_apply (append_only_loc_cas_only_cas_live_loc _ _ _ _ _ _ _ ∅ _ _ _ l1 l2 _ ∅
with "[$Mt●3 $Mt◯ $omot↦3 $⊒V2]"); try done; [solve_ndisj|..].
iIntros (b3 et3 gent3 vt3 Vt3 V3 mot3' omot3' eVt3 eVtn3)
"(Pures & #MAXgen_et3 & #et3✓eVt3 & #etn3✓eVtn3 & Mt●3 & #⊒V3 & #Mt◯3@V3 & omot↦3 & CASE)".
iDestruct "Pures" as %(Eqgent3 & eVt3EV & LeV2V3).
iAssert (AllTailMsg γg γt γcl (omo_write_op omot3'))%I with "[-]" as "#AllTailMsg3'".
{ iDestruct "CASE" as "[(Pures & _) | [Pures sVw3]]".
- (* CAS failed, nothing to update *)
iDestruct "Pures" as %(-> & NEq & -> & Homot3' & eVtn3EV & eVtn3SYNC).
subst omot3'. rewrite omo_insert_r_write_op. done.
- (* CAS success *)
iDestruct "Pures" as %(-> & -> & ->).
iDestruct "sVw3" as (Vw3 (Eqmot3' & Homot3' & eVtn3EV & eVtn3SYNC & LeVt3Vw3 & NEqVt3Vw3 & NLeV3Vt3 & NEqV2V3 & LEV3Vw3)) "_".
subst omot3'. rewrite omo_append_w_write_op /AllTailMsg big_sepL_snoc. iFrame "AllTailMsg3".
iExists eVtn3,(gen1 + 1),enqid2,γl2,γsl2,v2,l2,Vw3. iExists eVenq2. iFrame "#". iPureIntro. rewrite eVtn3EV. split; [done|solve_lat]. }
iMod ("Hclose" with "[-AU n† n↦ n_1↦ Hms]") as "_".
{ repeat iExists _. iFrame "HM AllTailMsg3'". iFrame. eauto with iFrame. }
iModIntro. wp_let. wp_let. wp_op. wp_if. iApply ("IH" with "AU n† n↦ n_1↦ Hms"). }
(* Read [None] from next field. Proceed *)
iDestruct (NextFieldInfo_dup with "Fieldl1") as "[Fieldl1 Fieldl1']".
iDestruct "Fieldl1" as (eVl0) "(#e0✓eVl0 & %eVl0EV & CASE)".
iAssert (⌜ el2 = 0 ⌝)%I with "[-]" as %->.
{ iDestruct "CASE" as "[%Homol1|(%&%&%&%&%&%&%&%&%& (%Homol1 & _) & _)]";
rewrite Homol1 in Eqgenl2; by inversion Eqgenl2. }
iDestruct (OmoEinfo_agree with "el2✓eVl2 e0✓eVl0") as %<-.
rewrite eVl2EV in eVl0EV. simpl in eVl0EV. subst vl2.
iDestruct ("Close" with "[Ml1● omol1↦ Fieldl1' Hgen1]") as "AllNodes2".
{ repeat iExists _. iFrame "HMl1 enqid1✓eVenq1 Ml1●". rewrite omo_insert_r_write_op. iFrame. iSplitR; [done|eauto with iFrame]. }
iMod ("Hclose" with "[-AU n† n↦ n_1↦ Hms]") as "_". { repeat iExists _. iFrame "HM". iFrame. }
iClear "IH". iModIntro. wp_pures. rewrite -[Z.to_nat 0]/(0%nat). wp_bind (casʳᵃ(_, _, _))%E.
(* Inv access 3 *)
iInv "QInv" as (E3) ">H" "Hclose".
iDestruct "H" as (?? γs3 ???? Eh3 Et3 omo3)
"(%omoh3 & %omot3 & %stlist3 & %moh3 & %mot3 & %CL3 & %Mono3 & HM' & M●3 & Mh●3 & Mt●3 & CL●3 & omoh↦3 & omot↦3 & H)".
iDestruct "H" as "(AllNodes3 & #AllPrevLinks3 & AllHeadMsg3 & HeadLastMsg3 & #AllTailMsg3 & MONO3 & #EnqSeen3 & AllEvents3)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (mono_list_auth_idx_lookup with "CL●3 CL@gen1") as %HCL3gen1.
iDestruct (big_sepL_lookup_acc with "AllNodes3") as "[Inner Close]"; [exact HCL3gen1|].
iDestruct "Inner" as (? eVenq1' ???? El1' omol1' mol1') "(%EQ & _ & Ml1● & #enqid1✓eVenq1'' & (%Vbl1' & omol1↦) & Fieldl1 & Hgen1)".
inversion EQ. subst enqid γl γsl v0 l. clear EQ.
iDestruct (OmoEinfo_agree with "enqid1✓eVenq1 enqid1✓eVenq1''") as %<-.
iAssert (⌜ if decide (gen1 = (length CL3 - 1)%nat) then length (omo_write_op omol1') = 1
else length (omo_write_op omol1') = 2 ⌝)%I with "[-]" as %Hgen1.
{ iDestruct "Fieldl1" as (eVl0) "(#e0✓eVl0' & %eVl0EV & CASE)".
destruct (decide (gen1 = (length CL3 - 1)%nat)) as [->|NEQ].
- iDestruct "CASE" as "[%Homol1'|(%&%&%&%&%&%&%&%&%& _ & _ & #CL@next & _)]"; [by rewrite Homol1'|].
rewrite (Nat.sub_add 1 (length CL3)); [|by destruct CL3; simpl; try lia].
iDestruct (mono_list_auth_idx_lookup with "CL●3 CL@next") as %HCL3Lookup%lookup_lt_Some. lia.
- have [ninfo Hninfo] : is_Some (CL3 !! (S gen1)).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in HCL3gen1. lia. }
iDestruct (big_sepL_lookup with "AllPrevLinks3") as "PrevLinkInfo"; [exact Hninfo|].
iDestruct "PrevLinkInfo" as (??????????) "(%& _ & CL@gen1' & _ & OMOl'◯ & %LEN)".
iDestruct (mono_list_idx_agree with "CL@gen1 CL@gen1'") as %[[[[<- <-]%pair_inj <-]%pair_inj <-]%pair_inj <-]%pair_inj.
iDestruct "CASE" as "[%Homol1'|(%&%&%&%&%&%&%&%&%& [%Homol1' _] & _ & #CL@next & _)]"; [|by rewrite Homol1'].
iDestruct (OmoAuth_OmoSnapOmo with "Ml1● OMOl'◯") as %[_ LEwr%prefix_length].
rewrite Homol1' -omo_write_op_length LEN /= in LEwr. lia. }
iMod (append_only_loc_cas_only_from_na_rel _ _ ((n >> 1) ↦ #v) with "n_1↦ n↦")
as (γln γsn V2' eVn0) "(#⊒V2' & Mn● & [#Mn◯ n_1↦] & omon↦ & WCOMMITn & #en0✓eVn0 & [%eVn0EV _])"; [done|].
set V2'' := V2 ⊔ V2'.
iCombine "⊒V2 ⊒V2'" as "⊒V2''".
rewrite monPred_in_view_op. replace (V2 ⊔ V2') with V2'' by done.
wp_apply (append_only_loc_cas_only_cas _ _ _ _ _ _ _ ∅ _ _ _ (LitInt 0%Z) n _ ∅
with "[$Ml1● $Ml1◯ $omol1↦ $⊒V2'']"); try done; [solve_ndisj|].
iIntros (b3 el3 genl3 vl3 Vl3 V3 mol3 omol3 eVl3 eVln3)
"(Pures & #MAXgen_el3 & #el3✓eVl3 & #eln3✓eVln3 & Ml1● & #⊒V3 & #Ml1◯3@V3 & omol1↦ & CASE)".
iDestruct "Pures" as %(Eqgenl3 & eVl3EV & LeV2V3).
have LeV1V3 : V1 ⊑ V3 by solve_lat.
have LeV0'V1 : V0' ⊑ V1 by clear -LEV0'Vt1V1; solve_lat.
have LeV0'V3 : V0' ⊑ V3 by solve_lat.
iDestruct (view_at_mono_2 _ V3 with "M◯@V0'") as "#M◯@V3"; [done|].
iDestruct (view_at_mono_2 _ V3 with "Mh◯@V0'") as "#Mh◯@V3"; [done|].
iDestruct (view_at_mono_2 _ V3 with "Mt◯1'@V1") as "#Mt◯1'@V3"; [done|].
iDestruct "CASE" as "[(Pures & _) | [Pures sVw3]]".
{ (* CAS failed *)
iDestruct "Pures" as %(-> & NEq & -> & Homol3 & eVln3EV & eVln3SYNC).
iDestruct ("Close" with "[Ml1● omol1↦ Fieldl1 Hgen1]") as "AllNodes3".
{ repeat iExists _. iFrame "HMl1 Ml1● enqid1✓eVenq1". subst omol3. rewrite omo_insert_r_write_op. iFrame.
iSplitR; [done|eauto with iFrame]. }
iMod ("Hclose" with "[-AU n† omon↦ Mn● WCOMMITn n_1↦ Hms]") as "_".
{ repeat iExists _. iFrame "HM AllTailMsg3 AllPrevLinks3 EnqSeen3". iFrame. }
iMod "AU" as (γs3' E3' omo3' stlist3') "[>M●3 [_ Commit]]".
iMod ("Commit" $! false V3 E3' _ _ M with "[M●3]") as "HΦ".
{ iFrame "⊒V3 M●3". iSplit; [|done]. repeat iExists _. iFrame "HM QInv". by iFrame "#". }
iModIntro. wp_if. iApply wp_hist_inv; [done|]. iIntros "HINV".
iMod (append_only_loc_to_na with "HINV Mn● omon↦") as (???) "[n↦ _]"; [solve_ndisj|].
have LeV2'V3 : V2' ⊑ V3. { clear -LeV2V3. subst V2''. solve_lat. }
iDestruct (view_at_mono_2 _ V3 with "n_1↦") as "n_1↦"; [done|].
iDestruct (view_at_elim with "⊒V3 n_1↦") as "n_1↦".
wp_apply (wp_delete _ tid 2 _ [ v0; #v] with "[$n† n↦ n_1↦]"); [done|done|..].
{ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
iIntros "_". wp_pures. by iApply "HΦ". }
(* CAS success, commit [Enq] *)
iDestruct "Pures" as %(-> & -> & ->).
iDestruct "sVw3" as (Vw3 (Eqmol3 & Homol3 & eVln3EV & eVln3SYNC & LeVl3V3 & NEqVl3V3 & NLeV3Vl3 & NEqV2''V3 & ->))
"(_ & _ & WCOMMIT)".
iDestruct "Fieldl1" as (eVl0) "(#e0✓eVl0' & %eVl0EV & CASE)".
iDestruct (OmoEinfo_agree with "e0✓eVl0 e0✓eVl0'") as %<-.
iDestruct "CASE" as "[%Homol1'|(%&%&%&%&%&%&%&%&%& (%Homol1' & _ & %eVlEV) & _ & _ & #el✓eVl & _)]"; last first.
{ rewrite omo_write_op_length !Homol1' /= in Eqgenl3. inversion Eqgenl3. subst el.
iDestruct (OmoEinfo_agree with "el3✓eVl3 el✓eVl") as %<-.
rewrite eVl3EV in eVlEV. inversion eVlEV. }
destruct (decide (gen1 = (length CL3 - 1)%nat)) as [->|NEQ]; [|rewrite Homol1' /= in Hgen1; lia].
iDestruct (big_sepL_lookup with "EnqSeen3") as "Info"; [exact HCL3gen1|].
iDestruct "Info" as (CLp eVenq1' Mp) "(CLp◯ & %LENeq & enqid1✓eVenq1''' & _ & Mp◯@SYNC & Mp_CLp)".
iDestruct (OmoEinfo_agree with "enqid1✓eVenq1 enqid1✓eVenq1'''") as %<-. simpl.
iDestruct (view_at_mono_2 _ V3 with "Mp◯@SYNC") as "#Mp◯@V3"; [solve_lat|].
iDestruct (OmoEview_union_obj with "M◯@V3 Mp◯@V3") as "M◯'@V3".
iDestruct (eView_Enq_exact_union with "M_CL0 Mp_CLp CL◯0 CLp◯") as (CLp') "(#Mp'_CLp' & #CLp◯' & %LENCLp')".
iAssert (⌜ length CLp' = length CL3 ⌝)%I with "[-]" as %LENCLp''.
{ rewrite Nat.sub_add in LENeq; [|by destruct CL3; simpl; try lia]. rewrite LENeq in LENCLp'.
iDestruct (mono_list_auth_lb_valid with "CL●3 CL◯0") as %[_ LECL3CL0%prefix_length].
iPureIntro. lia. }
have LeV0V3 : V0 ⊑ V3 by solve_lat.
set enqId := length E3.
set M' := {[enqId]} ∪ (M ∪ ({[enqid1]} ∪ eVenq1.(eview) ∪ Mp)).
set egV' := mkOmoEvent (Enq v) V3 M'.
set E3' := E3 ++ [egV'].
have SubE3E3' : E3 ⊑ E3' by apply prefix_app_r.
iMod "AU" as (????) "[>M●3' [_ Commit]]".
iDestruct (OmoAuth_agree with "M●3 M●3'") as %(<- & <- & <- & <-).
iCombine "M●3 M●3'" as "M●3".
iDestruct (OmoAuth_stlist_nonempty with "M●3") as %NEQstlist3.
have [st Hst] : is_Some (last stlist3) by rewrite last_is_Some.
iMod (OmoAuth_insert_last with "M●3 M◯'@V3 WCOMMIT []")
as "(M●3 & #M◯''@V3 & #enqId↦eln3 & #enqId✓egV' & #enqId↪st & WCOMMIT)".
{ have ? : step enqId egV' st (st ++ [(enqId, v, egV'.(sync), egV'.(eview))]); [|by iPureIntro; split_and!].
eapply queue_step_Enq; try done. subst egV' M'. set_solver-. }
iMod (OmoHb_new_1 with "M●3 enqId✓egV' eln3✓eVln3") as "[M●3 #enqId⊒eln3]"; [rewrite eVln3SYNC;solve_lat|].
iDestruct (OmoHbToken_finish with "M●3") as "[M●3 M●3']".
iDestruct (OmoLe_get_append_w with "M●3 enqid1✓eVenq1") as "#enqid1≤enqId".
iMod (meta_set _ _ (enqId,γln,γsn,#v) nroot with "Hms") as "#HMn"; [done|].
iDestruct "HeadLastMsg3" as (eh deqid st' gen CLh eVh M'')
"(#deqid↦eh & #deqid↪st' & #eh✓eVh & #CLh◯ & %LENCLh & #M''◯ & #M''_CLh & #MAXgen_deqid & (%LAST & %Hgen & %Hst'dropdrop) & BIG1)".
iDestruct (mono_list_auth_lb_valid with "CL●3 CLh◯") as %[_ LECLhCL3%prefix_length].
set CL3' := CL3 ++ [(enqId, γln, γsn, #v, n)].
iMod (mono_list_auth_own_update with "CL●3") as "[CL●3 #CL◯3]".
{ have ? : CL3 ⊑ CL3' by apply prefix_app_r. done. }
iDestruct (mono_list_idx_own_get with "CL◯3") as "CL@new"; [by apply lookup_app_1_eq|].
iAssert (⌜ length El1' ≠ 0 ⌝)%I with "[-]" as %NEQlenEl1'.
{ destruct El1'; [|done]. iDestruct (OmoAuth_wf with "Ml1●") as %[OMO_GOOD _].
have EQ1 : lookup_omo omol3 (wr_event 0) = Some 0 by rewrite lookup_omo_wr_event Homol3 omo_append_w_write_op Homol1'.
have EQ2 : lookup_omo omol3 (wr_event 1) = Some 0 by rewrite lookup_omo_wr_event Homol3 omo_append_w_write_op Homol1'.
eapply lookup_omo_inj in EQ2 as INJ; [|exact OMO_GOOD|exact EQ1]. inversion INJ. }
iDestruct "n_1↦" as "[n_1↦ n_1↦']".
iDestruct (OmoSnapOmo_get with "Ml1●") as "#OMOl3◯".
iDestruct ("Close" with "[Ml1● omol1↦ Hgen1 n_1↦']") as "AllNodes3".
{ repeat iExists _. iFrame "HMl1 enqid1✓eVenq1". iFrame. iSplitR; [done|]. iSplitL "omol1↦"; [eauto with iFrame|].
iExists eVl2. iFrame "e0✓eVl0". iSplit; [by rewrite eVl2EV|]. iRight.
iExists (length El1'),eVln3,enqId,γln,γsn,#v,n,egV'. iExists V3. subst omol3. rewrite omo_append_w_write_op.
rewrite (Nat.sub_add 1 (length CL3)); [|by destruct CL3; simpl; try lia].
iDestruct (view_at_mono_2 _ V3 with "Mn◯") as "Mn◯@V3". { clear -LeV2V3. subst V2''. solve_lat. }
iFrame "#". iSplit; last iSplit; try done.
- iPureIntro. split_and!; [|done|by rewrite eVln3EV]. rewrite Homol1'. clear. by simplify_list_eq.
- iExists _. iDestruct (view_at_mono_2 _ V3 with "n_1↦'") as "n_1↦"; [clear -LeV2V3; solve_lat|iFrame]. }
iAssert (AllNodes γg γcl CL3')%I with "[Mn● omon↦ AllNodes3]" as "AllNodes3".
{ subst CL3'. rewrite /AllNodes big_sepL_snoc. iFrame.
repeat iExists _. iFrame "HMn enqId✓egV'". iFrame "Mn●". iSplitR; [done|]. iSplitL.
{ iDestruct (view_at_intro with "omon↦") as (?) "[_ omon↦]". iExists _. rewrite shift_0. iFrame "omon↦". }
iSplit; last first.
{ iPureIntro. exists v. split_and!; try done. lia. }
iExists eVn0. iFrame "en0✓eVn0". iSplit; [by rewrite eVn0EV|]. by iLeft. }
iAssert (AllPrevLinks γg γcl CL3')%I with "[-]" as "#AllPrevLinks3'".
{ subst CL3'. rewrite /AllPrevLinks big_sepL_snoc. iFrame "AllPrevLinks3".
replace (length CL3) with (S (length CL3 - 1)); last first.
{ destruct CL3; [done|]. rewrite cons_length /=. lia. }
replace (S (length CL3 - 1) - 1) with (length CL3 - 1) by lia.
repeat iExists _. iFrame "CL@gen1 enqid1≤enqId OMOl3◯". iSplit; [done|].
iPureIntro. subst omol3. rewrite omo_append_w_length omo_write_op_length Hgen1. lia. }
set omo3' := omo_append_w omo3 enqId [].
iAssert (HeadLastMsg γg γh γs3 γcl (omo_write_op omo3') (omo_write_op omoh3) CL3')%I with "[BIG1 WCOMMITn]" as "HeadLastMsg3".
{ repeat iExists _. iFrame "deqid↦eh deqid↪st' eh✓eVh CLh◯ M''◯ M''_CLh MAXgen_deqid BIG1".
iSplitR; [done|].
have Hgen' : omo_write_op omo3' !! gen = Some deqid.
{ subst omo3'. rewrite omo_append_w_write_op. by apply lookup_app_l_Some. }
iPureIntro. split_and!; try done. subst omo3' CL3'. rewrite omo_append_w_write_op.
rewrite (drop_app_le (omo_write_op omo3)); [|by apply lookup_lt_Some in Hgen; lia].
do 4rewrite -fmap_drop. rewrite drop_app_le; [|lia].
clear -Hst'dropdrop. simplify_list_eq. rewrite -Hst'dropdrop. simplify_list_eq. done. }
iAssert (eView_Enq_exact γg M' CL3')%I with "[-]" as "#M'_CL3'".
{ iDestruct (mono_list_auth_lb_valid with "CL●3 CLp◯'") as %[_ SubCLp'CL3']. iSplit.
- subst CL3'. rewrite big_sepL_forall. iIntros "%i %ninfo %Hi".
destruct (decide (i = length CL3)) as [->|NEQ].
+ rewrite lookup_app_1_eq in Hi. inversion Hi. subst M'. iPureIntro. set_solver-.
+ apply (prefix_lookup_inv CLp') in Hi; [..|done]; last first.
{ rewrite lookup_lt_is_Some LENCLp''. apply lookup_lt_Some in Hi. rewrite app_length /= in Hi. lia. }
iDestruct "Mp'_CLp'" as "[Mp'_CLp' _]". iDestruct (big_sepL_lookup with "Mp'_CLp'") as %INCL; [exact Hi|].
iPureIntro. subst M'. clear -INCL. set_solver.
- iApply big_sepS_intro. iIntros "%e %eIncl". subst M'.
destruct (decide (e = enqId)) as [->|NEQ].
+ iModIntro. iExists egV'. iFrame "enqId✓egV'". subst egV' CL3'. simpl. iPureIntro. rewrite !fmap_app /=. set_solver-.
+ have INCL : e ∈ (M ∪ {[enqid1]} ∪ eVenq1.(eview) ∪ Mp) by clear -eIncl NEQ; set_solver.
iDestruct "Mp'_CLp'" as "[_ Mp'_CLp']". iDestruct (big_sepS_elem_of _ _ e with "Mp'_CLp'") as (eV) "[e✓eV HeV]"; [clear -INCL; set_solver|].
iModIntro. iExists eV. iFrame "e✓eV". destruct (eV.(type)); try done;
iDestruct "HeV" as %HeV; iPureIntro; eapply elem_of_prefix; try done; do 4 apply fmap_prefix; done. }
replace ({[length E3]} ∪ (M ∪ ({[enqid1]} ∪ eVenq1.(eview) ∪ Mp))) with M' by set_solver-.
iAssert (OmoUB γg M' enqId)%I with "[-]" as "#MAXgen_enqId".
{ rewrite /OmoUB (big_sepS_forall _ M'). iIntros "%e %eIncl".
iDestruct (OmoAuth_OmoEview_obj with "M●3 M◯''@V3") as %MIncl.
specialize (MIncl _ eIncl).
iDestruct (OmoEinfo_get' with "M●3") as (eV) "#e✓eV"; [exact MIncl|].
iDestruct (OmoLe_get_append_w with "M●3 e✓eV") as "#e≤enqId". done. }
iDestruct (OmoUB_singleton with "enqId✓egV'") as "MAXenqId".
iDestruct (big_sepS_subseteq _ _ M with "MAXenqId") as "MAXenqId'"; [set_solver-|].
iMod ("Commit" $! true V3 E3' _ _ M' with "[M●3' WCOMMIT]") as "HΦ".
{ iFrame "⊒V3 M●3' WCOMMIT MAXenqId'". iSplit.
- repeat iExists _. iFrame "HM QInv M◯''@V3 Mh◯@V3 Mt◯1'@V3 CL◯3 M'_CL3'". iPureIntro.
unfold not. intros H. apply (f_equal length) in H. subst CL3'. rewrite app_length /= in H. lia.
- iPureIntro. split_and!; try done; [|set_solver-]. by eexists. }
iMod ("Hclose" with "[-HΦ]") as "_".
{ repeat iExists _. iFrame "HM M●3 AllPrevLinks3' AllTailMsg3". iFrame. iNext. iSplitL.
- subst CL3'. rewrite /EnqSeen big_sepL_snoc. iFrame "EnqSeen3". iExists (CL3 ++ [(enqId, γln, γsn, #v, n)]),egV',M'. simpl.
replace ({[enqId]} ∪ M' ∪ M') with M' by set_solver-.
iFrame "CL◯3 enqId✓egV' MAXgen_enqId M◯''@V3 M'_CL3'". iPureIntro. rewrite app_length /=. done.
- rewrite big_sepL_singleton. by subst egV'. }
iModIntro. wp_pures. rewrite -[Z.to_nat 1]/(1%nat). wp_bind (casʳᵉˡ(_, _, _))%E.
(* Inv access 4 *)
iInv "QInv" as (E4) ">H" "Hclose".
iDestruct "H" as (?? γs4 ???? Eh4 Et4 omo4)
"(%omoh4 & %omot4 & %stlist4 & %moh4 & %mot4 & %CL4 & %Mono4 & HM' & M●4 & Mh●4 & Mt●4 & CL●4 & omoh↦4 & [%Vbt4 omot↦4] & H)".
iDestruct "H" as "(AllNodes4 & AllPrevLinks4 & AllHeadMsg4 & HeadLastMsg4 & #AllTailMsg4 & MONO4 & EnqSeen4 & AllEvents4)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (OmoAuth_OmoSnapOmo with "Mt●4 OMOt1◯") as %[_ LEomot1wr].
wp_apply (append_only_loc_cas_only_cas_live_loc _ _ _ _ _ _ _ ∅ _ _ _ l1 n _ ∅
with "[$Mt●4 $Mt◯ $omot↦4 $⊒V3]"); try done; [solve_ndisj|..].
iIntros (b4 et4 gent4 vt4 Vt4 V4 mot4' omot4' eVt4 eVtn4)
"(Pures & #MAXgen_et4 & #et4✓eVt4 & #etn4✓eVtn4 & Mt●4 & #⊒V4 & #Mt◯4@V4 & omot↦4 & CASE)".
iDestruct "Pures" as %(Eqgent4 & eVt4EV & LeV3V4).
iAssert (AllTailMsg γg γt γcl (omo_write_op omot4'))%I with "[-]" as "#AllTailMsg4'".
{ iDestruct "CASE" as "[(Pures & _) | [Pures sVw3]]".
- (* CAS failed, nothing to update *)
iDestruct "Pures" as %(-> & NEq & -> & Homot4' & eVtn4EV & eVtn4SYNC).
subst omot4'. rewrite omo_insert_r_write_op. done.
- (* CAS success *)
iDestruct "Pures" as %(-> & -> & ->).
iDestruct "sVw3" as (Vw4 (Eqmot4' & Homot4' & eVtn4EV & eVtn4SYNC & LeVt4Vw4 & NEqVt4Vw4 & NLeV4Vt4 & NEqV3V4 & LEV4Vw4)) "_".
subst omot4'. rewrite omo_append_w_write_op /AllTailMsg big_sepL_snoc. iFrame "AllTailMsg4".
have LeV2'Vw4 : V2' ⊑ Vw4 by clear -LeV2V3 LeV3V4 LEV4Vw4; solve_lat.
iExists eVtn4,(length CL3),enqId,γln,γsn,#v,n,Vw4. iExists egV'. iFrame "#". iPureIntro. rewrite eVtn4EV. split; [done|].
subst egV'. simpl. clear -LeV3V4 LEV4Vw4. solve_lat. }
iMod ("Hclose" with "[-HΦ]") as "_".
{ repeat iExists _. iFrame "HM AllTailMsg4'". iFrame. eauto with iFrame. }
iModIntro. wp_pures. by iApply "HΦ".
Qed.
Lemma enqueue_spec :
enqueue_spec' enqueue QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg M0 V0 z LTz. iIntros "#⊒V0 #M◯0" (Φ) "AU".
iLöb as "IH". wp_lam.
awp_apply (try_enq_spec with "⊒V0 M◯0"); [eauto..|].
iApply (aacc_aupd with "AU"); [done|].
iIntros (γs E omo stlist) "QInv".
iAaccIntro with "QInv"; [eauto with iFrame|].
iIntros (b V1 E' omo' stlist' M1) "(⊒V1 & QInv & ⊒M1@V1 & CASE) !>".
destruct b.
- iRight. iDestruct "CASE" as "((%HE' & %Homo' & [%st %Hst] & %LeV0V1 & %SubM0M1) & WCOMMIT & MAX)".
iExists V1,st,M1. subst E' omo' stlist'. iFrame. iSplit; [done|]. iIntros "HΦ !> _". wp_pures. by iApply "HΦ".
- iLeft. iDestruct "CASE" as %(-> & -> & -> & ->). iFrame. iIntros "AU !> _". wp_if. by iApply ("IH" with "AU").
Qed.
Lemma try_deq_spec :
try_deq_spec' try_deq QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg M V0. iIntros "#⊒V0 #QueueLocal" (Φ) "AU".
iDestruct "QueueLocal" as (?????? Mh Mt CL0) "(HM & QInv & M◯ & Mh◯ & Mt◯ & CL◯0 & M_CL0 & %CL0NEQ)".
iCombine "M◯ Mt◯" as "MMt◯".
iDestruct (view_at_intro_incl with "MMt◯ ⊒V0") as (V0') "(#⊒V0' & %LEV0V0' & [#M◯' #Mt◯'])".
wp_lam. wp_op. rewrite -[Z.to_nat 0]/(0%nat). wp_bind (!ᵃᶜ #(q >> head))%E.
(* Inv access 1 *)
iInv "QInv" as (E1) ">H" "Hclose".
iDestruct "H" as (?? γs1 ???? Eh1 Et1 omo1)
"(%omoh1 & %omot1 & %stlist1 & %moh1 & %mot1 & %CL1 & %Mono1 & HM' & M●1 & Mh●1 & Mt●1 & CL●1 & (%Vbh1 & omoh↦1) & omot↦1 & H)".
iDestruct "H" as "(AllNodes1 & AllPrevLinks1 & AllHeadMsg1 & H)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (OmoSnapOmo_get with "Mh●1") as "#OMOh1◯".
iDestruct (OmoEview_update with "M●1 M◯ Mh◯") as (Mh') "(M●1 & #Mh◯' & M⊢Mh' & %SubMhMh')".
wp_apply (append_only_loc_acquire_read with "[$Mh●1 $Mh◯' $omoh↦1 $⊒V0']"); [solve_ndisj|].
iIntros (eh1 genh1 vh1 Vh1 V1 eVh1 eVhn1)
"(Pures & Mh●1 & _ & #MAXgen_eh1 & #eh1✓eVh1 & #ehn1✓eVhn1 & #eh1=ehn1 & #⊒V1 & #Mh◯1' & omoh↦1)".
iDestruct "Pures" as %(Eqgenh1 & eVh1EV & LEV0'Vh1V1 & eVhn1EV & eVhn1SYNC).
iDestruct (big_sepL_lookup with "AllHeadMsg1") as "#HMsg_eh1"; [exact Eqgenh1|].
iDestruct "HMsg_eh1" as (deqid1 eVh1' enqid1 γl1 γsl1 vl1 l1 Vh1' st1 ?) "(eh1✓eVh1' & _ & _ & _ & _ & CL@genh1 & %eVh1'EV & _)".
iDestruct (OmoEinfo_agree with "eh1✓eVh1 eh1✓eVh1'") as %<-.
rewrite eVh1EV in eVh1'EV. inversion eVh1'EV. subst vh1 Vh1'. clear eVh1'EV st1 deqid1 Ml. iClear "eh1✓eVh1'".
iMod ("Hclose" with "[-AU M⊢Mh']") as "_".
{ iExists E1. do 7 iExists _. iExists (Eh1 ++ [eVhn1]),_,_,(omo_insert_r omoh1 genh1 (length Eh1)),_,_,_,_. iExists _,_.
rewrite omo_insert_r_write_op. iFrame "H AllHeadMsg1 HM". iFrame "∗". eauto with iFrame. }
iModIntro. wp_pures. rewrite -[Z.to_nat 0]/(0%nat). wp_bind (!ᵃᶜ #(l1 >> 0))%E.
(* Inv access 2 *)
iInv "QInv" as (E2) ">H" "Hclose".
iDestruct "H" as (?? γs2 ???? Eh2 Et2 omo2)
"(%omoh2 & %omot2 & %stlist2 & %moh2 & %mot2 & %CL2 & %Mono2 & HM' & M●2 & Mh●2 & Mt●2 & CL●2 & (%Vbh2 & omoh↦2) & omot↦2 & H)".
iDestruct "H" as "(AllNodes2 & #AllPrevLinks2 & AllHeadMsg2 & H)".
simplify_meta6 with "HM' HM". iClear "HM'".
iDestruct (OmoAuth_OmoSnapOmo with "Mh●2 OMOh1◯") as %[_ LEomoh2wr].
iDestruct (big_sepL_lookup with "AllHeadMsg2") as "#HMsg_eh2"; [by eapply prefix_lookup_Some in Eqgenh1|].
iDestruct "HMsg_eh2" as (deqid1 eVh1' enqid1' γl1' γsl1' vl1' l1' Vh1' st1 Ml1)
"(eh1✓eVh1' & deqid1↦eh1 & MONO✓deqid1 & _ & deqid1↪st1 & CL@genh1' & %eVh1'EV & Ml1◯A & Hst1)".
iDestruct (OmoEinfo_agree with "eh1✓eVh1 eh1✓eVh1'") as %<-.
rewrite eVh1EV in eVh1'EV. inversion eVh1'EV. subst l1' Vh1'. clear eVh1'EV.
iDestruct (mono_list_idx_agree with "CL@genh1 CL@genh1'") as %[[[[<- <-]%pair_inj <-]%pair_inj <-]%pair_inj _]%pair_inj.
iClear "CL@genh1'".
iDestruct (view_at_mono_2 _ V1 with "Ml1◯A") as "#Ml1◯A'"; [solve_lat|].
iDestruct (view_at_elim with "⊒V1 Ml1◯A'") as "#Ml1◯".
iDestruct (mono_list_auth_idx_lookup with "CL●2 CL@genh1") as %HCL2genh1.
iDestruct (big_sepL_lookup_acc with "AllNodes2") as "[AllNodesInner AllNodesClose]"; [exact HCL2genh1|].
iDestruct "AllNodesInner" as (? eVenq1 ???? El1 omol1 mol1) "(%Hninfo & #HMl1 & Ml1● & #enqid1✓eVenq1 & [%Vbl1 omol1↦] & Fieldl1 & Hgenh1)".
inversion Hninfo. subst enqid γl γsl v l. clear Hninfo.
iDestruct (OmoEview_update with "M●2 M◯ Ml1◯") as (Ml1') "(M●2 & #Ml1◯' & M⊢Ml1' & %SubMl1Ml1')".
iDestruct (OmoSnapOmo_get with "Ml1●") as "#OMOl1◯".
wp_apply (append_only_loc_acquire_read with "[$Ml1● $Ml1◯' $omol1↦ $⊒V1]"); [solve_ndisj|].
iIntros (el1 genl1 vl1' Vl1 V2 eVl1 eVl1n)
"(Pures & Ml1● & RCOMMIT & #MAXgen_el1 & #el1✓eVl1 & #el1n✓eVl1n & #el1=el1n & #⊒V2 & #Ml1◯'' & omol1↦)".
iDestruct "Pures" as %(Hgenl1 & eVl1EV & LEV1Vl1'V2 & eVl1nEV & eVl1nSYNC).
destruct genl1.
{ (* Read None value from next field. [EmpDeq] case *)
iAssert (⌜ st1 = [] ∧ vl1' = #0 ∧ el1 = 0 ⌝)%I with "[Ml1● Fieldl1]" as %(-> & -> & ->).
{ iDestruct "Fieldl1" as (eVl0) "(#e0✓eVl0 & %eVl0EV & CASE)".
destruct st1.
- iAssert (⌜ el1 = 0 ⌝)%I with "[CASE]" as %->.
{ by iDestruct "CASE" as "[%Homol1|(%&%&%&%&%&%&%&%&%& [%Homol1 _] & _)]";
rewrite Homol1 in Hgenl1; inversion Hgenl1. }
iDestruct (OmoEinfo_agree with "e0✓eVl0 el1✓eVl1") as %<-.
rewrite eVl1EV /= in eVl0EV. by subst vl1'.
- iDestruct "Hst1" as (???????) "(OMOl1◯' & _ & [-> %Homol1'])".
iDestruct (OmoAuth_OmoSnapOmo with "Ml1● OMOl1◯'") as %[_ LEomol1wr].
iDestruct "CASE" as "[%Homol1|CASE2]".
+ rewrite omo_insert_r_write_op Homol1 Homol1' in LEomol1wr.
apply prefix_length in LEomol1wr. simpl in *. lia.
+ iDestruct "CASE2" as (?????????) "[(%Homol1 & %NEQ & _) _]".
rewrite omo_insert_r_write_op Homol1 Homol1' in LEomol1wr.
rewrite Homol1 /= in Hgenl1. inversion Hgenl1. subst el1. clear Hgenl1.
have EQ : el = el0; [|subst el0].
{ have Lookup : [0; el] !! 1 = Some el by done.
eapply prefix_lookup_Some in Lookup; [|exact LEomol1wr]. by inversion Lookup. }
iDestruct (big_sepS_elem_of _ _ el with "MAXgen_el1") as "#el≤e0"; [set_solver|].
set omol1n := omo_insert_r omol1 0 (length El1).
have Lookup1 : lookup_omo omol1n (wr_event 0) = Some 0 by rewrite lookup_omo_wr_event omo_insert_r_write_op Homol1.
have Lookup2 : lookup_omo omol1n (wr_event 1) = Some el by rewrite lookup_omo_wr_event omo_insert_r_write_op Homol1.
iDestruct (OmoLe_Le with "Ml1● el≤e0") as %LE; [done|done|simpl in *; lia]. }
iAssert (OmoUB γg M deqid1)%I with "[-]" as "#MAXgen_deqid1".
{ iApply big_sepS_forall. iIntros "%e %eM".
iDestruct (OmoAuth_OmoEview with "M●2 M◯") as %MIncl.
specialize (MIncl _ eM) as [eV He].
iDestruct "H" as "(_ & _ & MONO2 & #EnqSeen2 & #AllEvents2)".
iDestruct (big_sepL_lookup with "AllEvents2") as "eInfo"; [exact He|].
destruct (eV.(type)) eqn:HeVev.
- iAssert (∃ gen γl γsl v l, ⌜ CL0 !! gen = Some (e, γl, γsl, v, l) ⌝)%I with "[-]" as (????) "(% & %HCL0gen)".
{ iDestruct "M_CL0" as "[M_CL0 M_CL0']".
iDestruct (big_sepS_elem_of with "M_CL0'") as (eV0) "[e✓eV0 HeV0]"; [exact eM|].
iDestruct (OmoAuth_OmoEinfo with "M●2 e✓eV0") as %He'.