-
Notifications
You must be signed in to change notification settings - Fork 0
/
omo_preds.v
5244 lines (4812 loc) · 284 KB
/
omo_preds.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.algebra Require Import lib.mono_list.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From iris.base_logic.lib Require Import ghost_var ghost_map.
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 stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.omo Require Import omo omo_event omo_history.
Require Import iris.prelude.options.
Ltac encode_agree Hγ :=
match type of Hγ with
| ?γ = ?e =>
match goal with
| H1 : ?γ = ?e, H2 : ?γ = _ |- _ =>
rewrite H1 in H2; apply (inj encode) in H2;
first [ injection H2 as [= <- <- <- <- <- <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <- <-]
| injection H2 as [= <- <- <- <- <-]
| injection H2 as [= <- <- <- <-]
| injection H2 as [= <- <- <-]
| injection H2 as [= <- <-] ]
end
end.
(** Ghost construction for OMO.
`omoGeneralG` is for library-unspecific predicates,
and `omoSpecificG` is for library-specific predicates.
Usage: In order to prove a library L by composing several libraries L1, L2, ..., Ln,
assume the following in the proof context:
1. single `omoGeneralG`
2. multiple `omoSpecificG`'s, each of which corresponds to L, L1, L2, ..., Ln. *)
Class omoGeneralG Σ := OmoGeneralG {
mono_ELG :> mono_listG (gname * option gname * view * eView * Qp * gname) Σ;
mono_WLG :> mono_listG (event_id * gname * Qp) Σ;
mono_RLG :> mono_listG event_id Σ;
mono_GLG :> mono_listG (gname * event_id) Σ;
tok_typeG :> inG Σ (agreeR boolO);
mono_gmapG :> ghost_mapG Σ event_id nat;
gen_gmapG :> ghost_mapG Σ Qp nat;
agree_gnameG :> inG Σ (agreeR gnameO);
}.
Class omoSpecificG Σ (eventT absStateT : Type) := OmoSpecificG {
mono_TLG :> mono_listG eventT Σ;
mono_SLG :> mono_listG absStateT Σ;
mono_EG :> mono_listG (omo_event eventT) Σ;
agree_gvarG :> ghost_varG Σ (gname * history eventT * omoT * list absStateT);
}.
Definition omoGeneralΣ : gFunctors :=
#[mono_listΣ (gname * option gname * view * eView * Qp * gname);
mono_listΣ (event_id * gname * Qp);
mono_listΣ event_id;
mono_listΣ (gname * event_id);
GFunctor (agreeR boolO);
ghost_mapΣ event_id nat;
ghost_mapΣ Qp nat;
GFunctor (agreeR gnameO)].
Definition omoSpecificΣ (eventT absStateT : Type) : gFunctors :=
#[mono_listΣ eventT;
mono_listΣ absStateT;
mono_listΣ (omo_event eventT);
ghost_varΣ (gname * history eventT * omoT * list absStateT)].
Global Instance subG_omoGeneralΣ {Σ} : subG omoGeneralΣ Σ → omoGeneralG Σ.
Proof. solve_inG. Qed.
Global Instance subG_omoSpecificΣ {Σ} eventT absStateT : subG (omoSpecificΣ eventT absStateT) Σ → omoSpecificG Σ eventT absStateT.
Proof. solve_inG. Qed.
(** Definitions of library-unspecific predicates **)
Section omo_general_def.
Context {Σ : gFunctors} `{!omoGeneralG Σ}.
Notation vProp := (vProp Σ).
Implicit Types
(γe γs γtl γel γh γg γwl γrl γgl γsl γq γb γm γn γx : gname)
(q qg : Qp)
(M : eView)
(einfo : (gname * option gname * view * eView * Qp * gname))
(EL : list (gname * option gname * view * eView * Qp * gname)) (* mono_list for all event info excluding event type *)
(WL : list (event_id * gname * Qp)) (* mono_list for γs *)
(RL : list event_id) (* mono_list for each generation *)
(GL : list (gname * event_id)) (* mono_list for commit-with relation or seen_event *)
(QM : gmap Qp nat)
(eidx : event_idx).
Local Open Scope nat_scope.
(* Persistent assertion that gen of `e1` < gen of `e2`. *)
Definition OmoLt_def (γe : gname) (e1 e2 : event_id) : vProp :=
∃ γtl γel γh γg γn einfo1 einfo2,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ (einfo1.1.2 < einfo2.1.2)%Qp ⌝ ∗
⎡mono_list_idx_own γel e1 einfo1⎤ ∗
⎡mono_list_idx_own γel e2 einfo2⎤.
Definition OmoLt_aux : seal (@OmoLt_def). Proof. by eexists. Qed.
Definition OmoLt := unseal (@OmoLt_aux).
Definition OmoLt_eq : @OmoLt = _ := seal_eq _.
(* Persistent assertion that gen of `e1` ≤ gen of `e2` *)
Definition OmoLe_def (γe : gname) (e1 e2 : event_id) : vProp :=
∃ γtl γel γh γg γn einfo1 einfo2,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ (einfo1.1.2 ≤ einfo2.1.2)%Qp ⌝ ∗
⎡mono_list_idx_own γel e1 einfo1⎤ ∗
⎡mono_list_idx_own γel e2 einfo2⎤.
Definition OmoLe_aux : seal (@OmoLe_def). Proof. by eexists. Qed.
Definition OmoLe := unseal (@OmoLe_aux).
Definition OmoLe_eq : @OmoLe = _ := seal_eq _.
(* Persistent assertion that gen of `e1` = gen of `e2` *)
Definition OmoEq_def (γe : gname) (e1 e2 : event_id) : vProp :=
∃ γtl γel γh γg γn einfo1 einfo2,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ (einfo1.1.2 = einfo2.1.2)%Qp ⌝ ∗
⎡mono_list_idx_own γel e1 einfo1⎤ ∗
⎡mono_list_idx_own γel e2 einfo2⎤.
Definition OmoEq_aux : seal (@OmoEq_def). Proof. by eexists. Qed.
Definition OmoEq := unseal (@OmoEq_aux).
Definition OmoEq_eq : @OmoEq = _ := seal_eq _.
(* Persistent assertion that `e'` happens-before `e` *)
Definition OmoHb_def (γe γe' : gname) (e e' : event_id) : vProp :=
∃ γtl γel γh γg γn γtl' γel' γh' γg' γn' einfo einfo' GL,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γe' = encode (γtl',γel',γh',γg',γn') ∧ (γe', e') ∈ GL ∧ einfo'.1.1.1.2 ⊑ einfo.1.1.1.2 ⌝ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗ ⎡mono_list_idx_own γel' e' einfo'⎤ ∗
⎡mono_list_lb_own einfo.2 GL⎤.
Definition OmoHb_aux : seal (@OmoHb_def). Proof. by eexists. Qed.
Definition OmoHb := unseal (@OmoHb_aux).
Definition OmoHb_eq : @OmoHb = _ := seal_eq _.
(* `OmoHb` for set of events *)
Definition OmoHbs_def (γe γe' : gname) (e : event_id) (M : eView) : vProp :=
[∗ set] e' ∈ M, OmoHb γe γe' e e'.
Definition OmoHbs_aux : seal (@OmoHbs_def). Proof. by eexists. Qed.
Definition OmoHbs := unseal (@OmoHbs_aux).
Definition OmoHbs_eq : @OmoHbs = _ := seal_eq _.
(* `gen` is an upper bound of generation of each element in `M` *)
Definition OmoUBgen (omo : omoT) M gen : Prop :=
∀ e, e ∈ M → ∃ eidx, lookup_omo omo eidx = Some e ∧ (gen_of eidx ≤ gen)%nat.
(* generation of `e` is an upper bound of generation of each element in `M` *)
Definition OmoUB γe M e : vProp :=
[∗ set] e' ∈ M, OmoLe γe e' e.
(* Commit-with relation from `e` to `e'` *)
Definition OmoCW_def (γe γe' : gname) (e e' : event_id) : vProp :=
∃ γtl γel γh γg γn γtl' γel' γh' γg' γn' einfo einfo' γgl γb,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γe' = encode (γtl',γel',γh',γg',γn') ⌝ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡mono_list_idx_own γel' e' einfo'⎤ ∗
⎡mono_list_idx_own γgl 0 (γe',e') ⎤ ∗
⎡mono_list_idx_own γgl 1 (γe,e) ⎤ ∗
⌜ einfo.1.1.1.1.2 = Some γgl ∧ einfo'.1.1.1.1.1 = encode (γgl,γb) ⌝.
Definition OmoCW_aux : seal (@OmoCW_def). Proof. by eexists. Qed.
Definition OmoCW := unseal (@OmoCW_aux).
Definition OmoCW_eq : @OmoCW = _ := seal_eq _.
(* Monotonicity of commit-with relations for all relations with starting event e ∈ M *)
Definition CWMono_def (γe γe' γm : gname) M : vProp :=
⎡ghost_map_auth γm 1 (gset_to_gmap 0%nat M)⎤ ∗
([∗ set] e ∈ M, ∃ e', ⎡e ↪[γm]□ 0%nat⎤ ∗ OmoCW γe γe' e e') ∗
□ (∀ e1 e2 e1' e2', ⌜ e1 ∈ M ∧ e2 ∈ M ⌝ -∗
OmoCW γe γe' e1 e1' -∗ OmoCW γe γe' e2 e2' -∗ OmoLe γe' e1' e2' -∗ OmoLe γe e1 e2).
Definition CWMono_aux : seal (@CWMono_def). Proof. by eexists. Qed.
Definition CWMono := unseal (@CWMono_aux).
Definition CWMono_eq : @CWMono = _ := seal_eq _.
(* Persistent snapshot of e ∈ M where M is the one in CWMono *)
Definition CWMonoValid_def γm (e : event_id) : vProp :=
⎡e ↪[γm]□ 0%nat⎤.
Definition CWMonoValid_aux : seal (@CWMonoValid_def). Proof. by eexists. Qed.
Definition CWMonoValid := unseal (@CWMonoValid_aux).
Definition CWMonoValid_eq : @CWMonoValid = _ := seal_eq _.
(* Persistent assertion that ∀ e e' ∈ M, OmoHb e e' -∗ ⌜ e' ∈ M ⌝ *)
Definition HbIncluded_def (γe γe' : gname) (M M' : eView) : vProp :=
∃ γtl γel γh γg γn,
⌜ γe = encode (γtl,γel,γh,γg,γn) ⌝ ∗
[∗ set] e ∈ M,
∃ einfo q GL,
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡mono_list_auth_own einfo.2 q GL⎤ ∗
⌜ (∀ e', (γe', e') ∈ GL → e' ∈ M') ⌝.
Definition HbIncluded_aux : seal (@HbIncluded_def). Proof. by eexists. Qed.
Definition HbIncluded := unseal (@HbIncluded_aux).
Definition HbIncluded_eq : @HbIncluded = _ := seal_eq _.
(* Local observation of events, not objective *)
Definition OmoEview_def (γe : gname) (M : eView) : vProp :=
∃ γtl γel γh γg γn,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ M ≠ ∅ ⌝ ∗
[∗ set] e ∈ M,
∃ einfo,
⎡mono_list_idx_own γel e einfo⎤ ∗
⊒(einfo.1.1.1.2).
Definition OmoEview_aux : seal (@OmoEview_def). Proof. by eexists. Qed.
Definition OmoEview := unseal (@OmoEview_aux).
Definition OmoEview_eq : @OmoEview = _ := seal_eq _.
(* Persistent snapshot of `omo` *)
Definition OmoSnapOmo_def (γe γs : gname) (omo : omoT) : vProp :=
∃ γtl γel γh γg γn γwl γsl γq WL,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γs = encode (γwl,γsl,γq) ⌝ ∗
⎡mono_list_lb_own γwl WL⎤ ∗
([∗ list] ees; winfo ∈ omo; WL,
∃ e es γrl einfo,
⌜ ees = (e, es) ∧ winfo = (e, γrl, einfo.1.2) ⌝ ∗
⎡mono_list_lb_own γrl es⎤ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
[∗ list] e' ∈ es,
∃ einfo',
⎡mono_list_idx_own γel e' einfo'⎤ ∗
⌜ einfo'.1.2 = einfo.1.2 ⌝) ∗
[∗ list] i↦winfo ∈ WL, ⎡winfo.2 ↪[γq]□ i⎤.
Definition OmoSnapOmo_aux : seal (@OmoSnapOmo_def). Proof. by eexists. Qed.
Definition OmoSnapOmo := unseal (@OmoSnapOmo_aux).
Definition OmoSnapOmo_eq : @OmoSnapOmo = _ := seal_eq _.
(* Token for producing read-only events *)
Definition OmoTokenR_def (γe : gname) (e : event_id) : vProp :=
∃ γtl γel γh γg γn einfo γgl γb,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ einfo.1.1.1.1.1 = encode (γgl, γb) ⌝ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡mono_list_auth_own γgl 1 [(γe, e)]⎤ ∗
⎡own γb (to_agree false)⎤.
Definition OmoTokenR_aux : seal (@OmoTokenR_def). Proof. by eexists. Qed.
Definition OmoTokenR := unseal (@OmoTokenR_aux).
Definition OmoTokenR_eq : @OmoTokenR = _ := seal_eq _.
(* Token for producing write events *)
Definition OmoTokenW_def (γe : gname) (e : event_id) : vProp :=
∃ γtl γel γh γg γn einfo γgl γb,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ einfo.1.1.1.1.1 = encode (γgl, γb) ⌝ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡mono_list_auth_own γgl 1 [(γe,e)]⎤ ∗
⎡own γb (to_agree true)⎤.
Definition OmoTokenW_aux : seal (@OmoTokenW_def). Proof. by eexists. Qed.
Definition OmoTokenW := unseal (@OmoTokenW_aux).
Definition OmoTokenW_eq : @OmoTokenW = _ := seal_eq _.
(* Auxilliary predicate for persistently remembering `γx` for `γe` *)
Definition OmoGname_def (γe γx : gname) : vProp :=
∃ γtl γel γh γg γn,
⌜ γe = encode (γtl,γel,γh,γg,γn) ⌝ ∗ ⎡own γn (to_agree γx)⎤.
Definition OmoGname_aux : seal (@OmoGname_def). Proof. by eexists. Qed.
Definition OmoGname := unseal (@OmoGname_aux).
Definition OmoGname_eq : @OmoGname = _ := seal_eq _.
Global Instance OmoLt_persistent γe e1 e2 : Persistent (OmoLt γe e1 e2).
Proof. rewrite OmoLt_eq. apply _. Qed.
Global Instance OmoLt_timeless γe e1 e2 : Timeless (OmoLt γe e1 e2).
Proof. rewrite OmoLt_eq. apply _. Qed.
Global Instance OmoLt_objective γe e1 e2 : Objective (OmoLt γe e1 e2).
Proof. rewrite OmoLt_eq. apply _. Qed.
Global Instance OmoLe_persistent γe e1 e2 : Persistent (OmoLe γe e1 e2).
Proof. rewrite OmoLe_eq. apply _. Qed.
Global Instance OmoLe_timeless γe e1 e2 : Timeless (OmoLe γe e1 e2).
Proof. rewrite OmoLe_eq. apply _. Qed.
Global Instance OmoLe_objective γe e1 e2 : Objective (OmoLe γe e1 e2).
Proof. rewrite OmoLe_eq. apply _. Qed.
Global Instance OmoEq_persistent γe e1 e2 : Persistent (OmoEq γe e1 e2).
Proof. rewrite OmoEq_eq. apply _. Qed.
Global Instance OmoEq_timeless γe e1 e2 : Timeless (OmoEq γe e1 e2).
Proof. rewrite OmoEq_eq. apply _. Qed.
Global Instance OmoEq_objective γe e1 e2 : Objective (OmoEq γe e1 e2).
Proof. rewrite OmoEq_eq. apply _. Qed.
Global Instance OmoHb_persistent γe γe' e e' : Persistent (OmoHb γe γe' e e').
Proof. rewrite OmoHb_eq. apply _. Qed.
Global Instance OmoHb_timeless γe γe' e e' : Timeless (OmoHb γe γe' e e').
Proof. rewrite OmoHb_eq. apply _. Qed.
Global Instance OmoHb_objective γe γe' e e' : Objective (OmoHb γe γe' e e').
Proof. rewrite OmoHb_eq. apply _. Qed.
Global Instance OmoHbs_persistent γe γe' e M : Persistent (OmoHbs γe γe' e M).
Proof. rewrite OmoHbs_eq. apply _. Qed.
Global Instance OmoHbs_timeless γe γe' e M : Timeless (OmoHbs γe γe' e M).
Proof. rewrite OmoHbs_eq. apply _. Qed.
Global Instance OmoHbs_objective γe γe' e M : Objective (OmoHbs γe γe' e M).
Proof. rewrite OmoHbs_eq. apply _. Qed.
Global Instance OmoUB_persistent γe M e : Persistent (OmoUB γe M e) := _.
Global Instance OmoUB_timeless γe M e : Timeless (OmoUB γe M e) := _.
Global Instance OmoUB_objective γe M e : Objective (OmoUB γe M e) := _.
Global Instance OmoCW_persistent γe γe' e e' : Persistent (OmoCW γe γe' e e').
Proof. rewrite OmoCW_eq. apply _. Qed.
Global Instance OmoCW_timeless γe γe' e e' : Timeless (OmoCW γe γe' e e').
Proof. rewrite OmoCW_eq. apply _. Qed.
Global Instance OmoCW_objective γe γe' e e' : Objective (OmoCW γe γe' e e').
Proof. rewrite OmoCW_eq. apply _. Qed.
Global Instance CWMono_timeless γe γe' γm M : Timeless (CWMono γe γe' γm M).
Proof. rewrite CWMono_eq. apply _. Qed.
Global Instance CWMono_objective γe γe' γm M : Objective (CWMono γe γe' γm M).
Proof. rewrite CWMono_eq. apply _. Qed.
Global Instance CWMonoValid_persistent γm e : Persistent (CWMonoValid γm e).
Proof. rewrite CWMonoValid_eq. apply _. Qed.
Global Instance CWMonoValid_timeless γm e : Timeless (CWMonoValid γm e).
Proof. rewrite CWMonoValid_eq. apply _. Qed.
Global Instance CWMonoValid_objective γm e : Objective (CWMonoValid γm e).
Proof. rewrite CWMonoValid_eq. apply _. Qed.
Global Instance HbIncluded_timeless γe γe' M M' : Timeless (HbIncluded γe γe' M M').
Proof. rewrite HbIncluded_eq. apply _. Qed.
Global Instance HbIncluded_objective γe γe' M M' : Objective (HbIncluded γe γe' M M').
Proof. rewrite HbIncluded_eq. apply _. Qed.
Global Instance OmoEview_persistent γe M : Persistent (OmoEview γe M).
Proof. rewrite OmoEview_eq. apply _. Qed.
Global Instance OmoEview_timeless γe M : Timeless (OmoEview γe M).
Proof. rewrite OmoEview_eq. apply _. Qed.
Global Instance OmoSnapOmo_persistent γe γs omo : Persistent (OmoSnapOmo γe γs omo ).
Proof. rewrite OmoSnapOmo_eq. apply _. Qed.
Global Instance OmoSnapOmo_timeless γe γs omo : Timeless (OmoSnapOmo γe γs omo).
Proof. rewrite OmoSnapOmo_eq. apply _. Qed.
Global Instance OmoSnapOmo_objective γe γs omo : Objective (OmoSnapOmo γe γs omo).
Proof. rewrite OmoSnapOmo_eq. apply _. Qed.
Global Instance OmoTokenR_objective γe e : Objective (OmoTokenR γe e).
Proof. rewrite OmoTokenR_eq. apply _. Qed.
Global Instance OmoTokenR_timeless γe e : Timeless (OmoTokenR γe e).
Proof. rewrite OmoTokenR_eq. apply _. Qed.
Global Instance OmoTokenW_objective γe e : Objective (OmoTokenW γe e).
Proof. rewrite OmoTokenW_eq. apply _. Qed.
Global Instance OmoTokenW_timeless γe e : Timeless (OmoTokenW γe e).
Proof. rewrite OmoTokenW_eq. apply _. Qed.
Global Instance OmoGname_persistent γe γx : Persistent (OmoGname γe γx).
Proof. rewrite OmoGname_eq. apply _. Qed.
Global Instance OmoGname_timeless γe γx : Timeless (OmoGname γe γx).
Proof. rewrite OmoGname_eq. apply _. Qed.
Global Instance OmoGname_objective γe γx : Objective (OmoGname γe γx).
Proof. rewrite OmoGname_eq. apply _. Qed.
End omo_general_def.
(** Definitions of library-specific predicates **)
Section omo_specific_def.
Context {eventT absStateT : Type}.
Context {Σ : gFunctors} `{!omoGeneralG Σ, !omoSpecificG Σ eventT absStateT}.
Notation history := (history eventT).
Notation iProp := (iProp Σ).
Notation vProp := (vProp Σ).
Implicit Types
(γe γs γtl γel γh γg γwl γrl γgl γsl γq γb γm γn : gname)
(q qg : Qp)
(E : history)
(M : eView)
(st : absStateT)
(ty : eventT)
(einfo : (gname * option gname * view * eView * Qp * gname))
(TL : list eventT) (* mono_list for type of events *)
(EL : list (gname * option gname * view * eView * Qp * gname)) (* mono_list for all event info excluding event type *)
(WL : list (event_id * gname * Qp)) (* mono_list for γs *)
(RL : list event_id) (* mono_list for each generation *)
(GL : list (gname * event_id)) (* mono_list for commit-with relation or seen_event *)
(SL : list absStateT)
(QM : gmap Qp nat)
(eidx : event_idx).
Local Open Scope nat_scope.
(** Persistent assertion that the resulting abstract state is `st`
when we do interpretation until the occurrence of `e` in linearization order *)
(** Note that this assertion is indeed persistent.
This is possible since `γs` part in `OmoAuth` will be changed when we perform `OmoAuth_insert`.
This behavior models invalidation of old interpretation when we insert a new write event in the middle of the generation. *)
Definition OmoSnap_def (γe γs : gname) (e : event_id) (st : absStateT) : vProp :=
∃ γtl γel γh γg γn γwl γsl γq i einfo,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γs = encode (γwl,γsl,γq) ⌝ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡einfo.1.2 ↪[γq]□ i⎤ ∗
⎡mono_list_idx_own γsl i st⎤.
Definition OmoSnap_aux : seal (@OmoSnap_def). Proof. by eexists. Qed.
Definition OmoSnap := unseal (@OmoSnap_aux).
Definition OmoSnap_eq : @OmoSnap = _ := seal_eq _.
(* Persistent knowledge of omo event `eV` corresponding to event id `e` *)
Definition OmoEinfo_def (γe : gname) (e : event_id) (eV : omo_event eventT) : vProp :=
∃ γtl γel γh γg γn ty einfo,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ eV.(type) = ty ∧ eV.(sync) = einfo.1.1.1.2 ∧ eV.(eview) = einfo.1.1.2 ⌝ ∗
⎡mono_list_idx_own γtl e ty⎤ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
⎡mono_list_idx_own γh e eV⎤ ∗
OmoUB γe ({[e]} ∪ eV.(eview)) e ∗
@{eV.(sync)} OmoEview γe ({[e]} ∪ eV.(eview)).
Definition OmoEinfo_aux : seal (@OmoEinfo_def). Proof. by eexists. Qed.
Definition OmoEinfo := unseal (@OmoEinfo_aux).
Definition OmoEinfo_eq : @OmoEinfo = _ := seal_eq _.
(* ---- Definitions used internally by `OmoAuth` ---- *)
Definition OmoAuth_E_TL_valid E TL : Prop :=
∀ e eV ty,
E !! e = Some eV →
TL !! e = Some ty →
eV.(type) = ty.
Definition OmoAuth_E_EL_valid E EL : Prop :=
∀ e eV einfo,
E !! e = Some eV →
EL !! e = Some einfo →
eV.(sync) = einfo.1.1.1.2 ∧ eV.(eview) = einfo.1.1.2.
Definition OmoAuth_EL_seen_event_valid EL : vProp :=
[∗ list] einfo ∈ EL,
∃ q GL,
⎡mono_list_auth_own einfo.2 q GL⎤ ∗
[∗ list] geinfo ∈ GL,
∃ γe e γtl γel γh γg γn einfo',
⌜ geinfo = (γe, e) ∧ γe = encode(γtl,γel,γh,γg,γn) ∧ einfo'.1.1.1.2 ⊑ einfo.1.1.1.2 ⌝ ∗
⎡mono_list_idx_own γel e einfo'⎤.
Definition OmoAuth_WL_valid γs γel q omo WL : vProp :=
[∗ list] ees; winfo ∈ omo; WL,
∃ e es γrl einfo,
⌜ ees = (e, es) ∧ winfo = (e, γrl, einfo.1.2) ⌝ ∗
⎡mono_list_auth_own γrl q es⎤ ∗
⎡mono_list_idx_own γel e einfo⎤ ∗
[∗ list] e' ∈ es,
∃ einfo',
⎡mono_list_idx_own γel e' einfo'⎤ ∗
⌜ einfo'.1.2 = einfo.1.2 ⌝.
Definition OmoAuth_qg_mono WL : Prop :=
∀ n1 n2 winfo1 winfo2,
WL !! n1 = Some winfo1 →
WL !! n2 = Some winfo2 →
(n1 < n2)%nat →
(winfo1.2 < winfo2.2)%Qp.
Definition OmoAuth_all_elem γe (E : history) : vProp :=
[∗ list] e↦eV ∈ E, OmoEinfo γe e eV.
Definition OmoAuth_QM_valid WL QM : Prop :=
∀ qg i, WL.*2 !! i = Some qg ↔ QM !! qg = Some i.
Definition OmoAuth_qg_keys γq QM : vProp :=
[∗ map] q↦i ∈ QM, ⎡q ↪[γq]□ i⎤.
(* Main definition of `OmoAuth` predicate *)
Definition OmoAuth_def (γe γs : gname) (q : Qp) (E : history) (omo : omoT) (stlist : list absStateT) `{Interpretable eventT absStateT} : vProp :=
∃ γtl γel γh γg γn γwl γsl γq TL EL WL QM,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γs = encode (γwl,γsl,γq) ⌝ ∗
⎡mono_list_auth_own γtl q TL⎤ ∗
⎡mono_list_auth_own γel q EL⎤ ∗
⎡mono_list_auth_own γwl q WL⎤ ∗
⎡mono_list_auth_own γsl q stlist⎤ ∗
⎡ghost_map_auth γq q QM⎤ ∗
⎡mono_list_auth_own γh q E⎤ ∗
⎡ghost_var γg q (γs,E,omo,stlist)⎤∗
OmoAuth_EL_seen_event_valid EL ∗
OmoAuth_WL_valid γs γel q omo WL ∗
OmoAuth_all_elem γe E ∗
OmoAuth_qg_keys γq QM ∗
⌜ (length E = length TL)%nat
∧ (length E = length EL)%nat
∧ OmoAuth_E_TL_valid E TL
∧ OmoAuth_E_EL_valid E EL
∧ OmoAuth_qg_mono WL
∧ OmoAuth_QM_valid WL QM
∧ omo ≠ [] ∧ E ≠ []
∧ history_wf E
∧ lhb E (seq 0 (length E))
∧ Linearizability_omo E omo stlist ⌝.
Definition OmoAuth_aux : seal (@OmoAuth_def). Proof. by eexists. Qed.
Definition OmoAuth := unseal (@OmoAuth_aux).
Definition OmoAuth_eq : @OmoAuth = _ := seal_eq _.
(* Snapshot of history of all events ever committed *)
Definition OmoSnapHistory_def (γe : gname) (E : history) : vProp :=
∃ γtl γel γh γg γn TL EL,
⌜ γe = encode (γtl,γel,γh,γg,γn) ⌝ ∗
⎡mono_list_lb_own γtl TL⎤ ∗
⎡mono_list_lb_own γel EL⎤ ∗
⎡mono_list_lb_own γh E⎤ ∗
⌜ (length E = length TL)%nat
∧ (length E = length EL)%nat
∧ OmoAuth_E_TL_valid E TL
∧ OmoAuth_E_EL_valid E EL ⌝.
Definition OmoSnapHistory_aux : seal (@OmoSnapHistory_def). Proof. by eexists. Qed.
Definition OmoSnapHistory := unseal (@OmoSnapHistory_aux).
Definition OmoSnapHistory_eq : @OmoSnapHistory = _ := seal_eq _.
(* Snapshot of list of abstract state *)
Definition OmoSnapStates_def (γe γs : gname) (omo : omoT) (stlist : list absStateT) : vProp :=
∃ γwl γsl γq,
⌜ γs = encode (γwl,γsl,γq) ∧ length omo = length stlist ⌝ ∗
⎡mono_list_lb_own γsl stlist⎤ ∗
OmoSnapOmo γe γs omo.
Definition OmoSnapStates_aux : seal (@OmoSnapStates_def). Proof. by eexists. Qed.
Definition OmoSnapStates := unseal (@OmoSnapStates_aux).
Definition OmoSnapStates_eq : @OmoSnapStates = _ := seal_eq _.
(** This is a special form of `OmoAuth` that allows us to register `OmoHb` relation.
Whenever `OmoAuth` is updated or initialized, it turns into `OmoHbToken`.
When registration of `OmoHb` relation is finished, use `OmoHbToken_finish` to return it to `OmoAuth`. *)
(** Detailed explanation for `OmoHbToken` and `OmoAuth`:
< When initializing an invariant and creating `OmoAuth` resource >
1. Create `OmoHbToken` resource by allocation rule of `OmoAuth`.
2. Create any number of `OmoHb` relations (if needed).
3. Turn `OmoHbToken` into `OmoAuth` by a rule `OmoHbToken_finish`.
< When inserting a new event into `OmoAuth` and re-establish the invariant >
1. Using a `OmoAuth` resource, perform an insertion rule (e.g. `OmoAuth_insert_ro`, `OmoAuth_insert_last`, `OmoAuth_insert`).
2. Then, take `OmoHbToken` resource.
3. Create any number of `OmoHb` relations (if needed).
4. Turn `OmoHbToken` into `OmoAuth` by the rule `OmoHbToken_finish`.
*)
Definition OmoHbToken_def (γe γs : gname) (E : history) (omo : omoT) (stlist : list absStateT) (e : event_id)
`{Interpretable eventT absStateT} : vProp :=
∃ γtl γel γh γg γn γwl γsl γq TL EL WL QM elast GL,
⌜ γe = encode (γtl,γel,γh,γg,γn) ∧ γs = encode (γwl,γsl,γq) ⌝ ∗
⎡mono_list_auth_own γtl 1 TL⎤ ∗
⎡mono_list_auth_own γel 1 EL⎤ ∗
⎡mono_list_auth_own γwl 1 WL⎤ ∗
⎡mono_list_auth_own γsl 1 stlist⎤ ∗
⎡ghost_map_auth γq 1 QM⎤ ∗
⎡mono_list_auth_own elast.2 1 GL⎤ ∗
⎡mono_list_auth_own γh 1 E⎤ ∗
⎡ghost_var γg 1 (γs,E,omo,stlist)⎤ ∗
OmoAuth_EL_seen_event_valid (take (length EL - 1)%nat EL) ∗
OmoAuth_WL_valid γs γel 1 omo WL ∗
OmoAuth_all_elem γe E ∗
OmoAuth_qg_keys γq QM ∗
([∗ list] geinfo ∈ GL,
∃ γe' e' γtl' γel' γh' γg' γn' einfo',
⌜ geinfo = (γe', e') ∧ γe' = encode (γtl',γel',γh',γg',γn') ∧ einfo'.1.1.1.2 ⊑ elast.1.1.1.2 ⌝ ∗
⎡mono_list_idx_own γel' e' einfo'⎤) ∗
⌜ (length E = length TL)%nat
∧ (length E = length EL)%nat
∧ (e = length EL - 1)%nat
∧ last EL = Some elast
∧ OmoAuth_E_TL_valid E TL
∧ OmoAuth_E_EL_valid E EL
∧ OmoAuth_qg_mono WL
∧ OmoAuth_QM_valid WL QM
∧ E ≠ [] ∧ omo ≠ []
∧ history_wf E
∧ hb_ord E (seq 0 (length E))
∧ Linearizability_omo E omo stlist ⌝.
Definition OmoHbToken_aux : seal (@OmoHbToken_def). Proof. by eexists. Qed.
Definition OmoHbToken := unseal (@OmoHbToken_aux).
Definition OmoHbToken_eq : @OmoHbToken = _ := seal_eq _.
Global Instance OmoSnap_persistent γe γs e st : Persistent (OmoSnap γe γs e st).
Proof. rewrite OmoSnap_eq. apply _. Qed.
Global Instance OmoSnap_timeless γe γs e st : Timeless (OmoSnap γe γs e st).
Proof. rewrite OmoSnap_eq. apply _. Qed.
Global Instance OmoSnap_objective γe γs e st : Objective (OmoSnap γe γs e st).
Proof. rewrite OmoSnap_eq. apply _. Qed.
Global Instance OmoEinfo_persistent γe e eV : Persistent (OmoEinfo γe e eV).
Proof. rewrite OmoEinfo_eq. apply _. Qed.
Global Instance OmoEinfo_timeless γe e eV : Timeless (OmoEinfo γe e eV).
Proof. rewrite OmoEinfo_eq. apply _. Qed.
Global Instance OmoEinfo_objective γe e eV : Objective (OmoEinfo γe e eV).
Proof. rewrite OmoEinfo_eq. apply _. Qed.
Global Instance OmoAuth_timeless γe γs q E omo stlist `{Interpretable eventT absStateT} :
Timeless (OmoAuth γe γs q E omo stlist _).
Proof. rewrite OmoAuth_eq. apply _. Qed.
Global Instance OmoAuth_objective γe γs q E omo stlist `{Interpretable eventT absStateT} :
Objective (OmoAuth γe γs q E omo stlist _).
Proof. rewrite OmoAuth_eq. apply _. Qed.
Global Instance OmoAuth_fractional γe γs E omo stlist `{Interpretable eventT absStateT} :
Fractional (λ q, OmoAuth γe γs q E omo stlist _).
Proof.
intros ??. rewrite OmoAuth_eq. iSplit.
- iIntros "M●". iDestruct "M●" as (??????????)
"(%&%& [%Hγe %Hγs] & [TL● TL●'] & [EL● EL●'] & [WL● WL●'] & [SL● SL●'] & [Hγq Hγq'] & [HL● HL●'] & [Hγg Hγg'] & EL✓ & WL✓ & #ELEMS & #KEYS & Pures)".
iDestruct "Pures" as %(EQlenTL & EQlenEL & E_TL_VALID & E_EL_VALID & MONOqg & QM_VALID & Nomo & NE & HWF & LHB & OMO_GOOD).
iAssert (OmoAuth_EL_seen_event_valid EL ∗ OmoAuth_EL_seen_event_valid EL)%I with "[EL✓]" as "[EL✓ EL✓']".
{ rewrite !/OmoAuth_EL_seen_event_valid. rewrite -big_sepL_sep. iApply (big_sepL_impl with "EL✓"). iModIntro.
iIntros "%i %einfo %Heinfo H". iDestruct "H" as (??) "[[GL● GL●'] #BIG]".
iSplitL "GL●"; repeat iExists _; iFrame "∗#". }
iAssert (OmoAuth_WL_valid γs γel p omo WL ∗ OmoAuth_WL_valid γs γel q omo WL)%I with "[WL✓]" as "[WL✓ WL✓']".
{ rewrite !/OmoAuth_WL_valid. rewrite -big_sepL2_sep. iApply (big_sepL2_impl with "WL✓"). iModIntro.
iIntros "%i %ees %winfo %Hi %Hwinfo H". destruct ees as [e es].
iDestruct "H" as (????) "(%EQ & [RL● RL●'] & #EL & #BIG)". iSplitL "RL●"; repeat iExists _; iFrame "∗#%". }
iSplitL "TL● EL● WL● SL● Hγq HL● Hγg EL✓ WL✓"; repeat iExists _; iFrame "∗#%"; done.
- iIntros "[M● M●']". iDestruct "M●" as (??????????)
"(%&%& [%Hγe %Hγs] & TL● & EL● & WL● & SL● & Hγq & HL● & Hγg & EL✓ & WL✓ & #ELEMS & #KEYS & Pures)".
iDestruct "Pures" as %(EQlenTL & EQlenEL & E_TL_VALID & E_EL_VALID & MONOqg & QM_VALID & Nomo & NE & HWF & LHB & OMO_GOOD).
iDestruct "M●'" as (??????????)
"(%&%& [%Hγe' %Hγs'] & TL●' & EL●' & WL●' & SL●' & Hγq' & HL●' & Hγg' & EL✓' & WL✓' & #ELEMS' & #KEYS' & Pures)".
iDestruct "Pures" as %(EQlenTL' & EQlenEL' & E_TL_VALID' & E_EL_VALID' & MONOqg' & QM_VALID' & Nomo' & NE' & HWF' & LHB' & OMO_GOOD').
encode_agree Hγe. encode_agree Hγs.
iDestruct (mono_list_auth_own_agree with "TL● TL●'") as %[_ <-].
iCombine "TL● TL●'" as "TL●".
iDestruct (mono_list_auth_own_agree with "EL● EL●'") as %[_ <-].
iCombine "EL● EL●'" as "EL●".
iDestruct (mono_list_auth_own_agree with "WL● WL●'") as %[_ <-].
iCombine "WL● WL●'" as "WL●".
iCombine "SL● SL●'" as "SL●".
iDestruct (ghost_map_auth_agree with "Hγq Hγq'") as %<-.
iCombine "Hγq Hγq'" as "Hγq".
iCombine "HL● HL●'" as "HL●".
iCombine "Hγg Hγg'" as "Hγg".
iAssert (OmoAuth_WL_valid γs γel (p + q)%Qp omo WL)%I with "[WL✓ WL✓']" as "WL✓".
{ iCombine "WL✓ WL✓'" as "WL✓". rewrite !/OmoAuth_WL_valid -big_sepL2_sep.
iApply (big_sepL2_impl with "WL✓"). iModIntro. iIntros "%i %ees %winfo %Hi %Hwinfo [H1 H2]". destruct ees as [e es].
iDestruct "H1" as (????) "([%EQ1 %EQ2] & RL● & #EL@e & BIG)".
iDestruct "H2" as (????) "([%EQ1' %EQ2'] & RL●' & #EL@e' & BIG')".
inversion EQ1. subst e0 es0 winfo. inversion EQ1'. inversion EQ2'. subst e1 es1 γrl0.
iExists e,es,γrl,einfo. iCombine "RL● RL●'" as "RL●".
iDestruct (mono_list_idx_agree with "EL@e EL@e'") as %<-. clear EQ1 EQ2' EQ1' H3 H5.
iFrame "∗#%". done. }
repeat iExists _. iFrame "∗#%". done.
Qed.
Global Instance OmoAuth_asfractional γe γs q E omo stlist `{Interpretable eventT absStateT} :
AsFractional (OmoAuth γe γs q E omo stlist _) (λ q, OmoAuth γe γs q E omo stlist _) q.
Proof. constructor; [done|apply _]. Qed.
Global Instance OmoSnapHistory_persistent γe E : Persistent (OmoSnapHistory γe E).
Proof. rewrite OmoSnapHistory_eq. apply _. Qed.
Global Instance OmoSnapHistory_timeless γe E : Timeless (OmoSnapHistory γe E).
Proof. rewrite OmoSnapHistory_eq. apply _. Qed.
Global Instance OmoSnapHistory_objective γe E : Objective (OmoSnapHistory γe E).
Proof. rewrite OmoSnapHistory_eq. apply _. Qed.
Global Instance OmoSnapStates_persistent γe γs omo stlist : Persistent (OmoSnapStates γe γs omo stlist).
Proof. rewrite OmoSnapStates_eq. apply _. Qed.
Global Instance OmoSnapStates_timeless γe γs omo stlist : Timeless (OmoSnapStates γe γs omo stlist).
Proof. rewrite OmoSnapStates_eq. apply _. Qed.
Global Instance OmoSnapStates_objective γe γs omo stlist : Objective (OmoSnapStates γe γs omo stlist).
Proof. rewrite OmoSnapStates_eq. apply _. Qed.
Global Instance OmoHbToken_timeless γe γs E omo stlist e `{Interpretable eventT absStateT} :
Timeless (OmoHbToken γe γs E omo stlist e _).
Proof. rewrite OmoHbToken_eq. apply _. Qed.
Global Instance OmoHbToken_objective γe γs E omo stlist e `{Interpretable eventT absStateT} :
Objective (OmoHbToken γe γs E omo stlist e _).
Proof. rewrite OmoHbToken_eq. apply _. Qed.
End omo_specific_def.
(* Lemmas that involve only omoGeneralG *)
Section omo_general_lemma.
Context {Σ : gFunctors} `{!omoGeneralG Σ}.
Notation vProp := (vProp Σ).
Implicit Types
(γe γs γtl γel γh γg γwl γrl γgl γsl γq γb γm γn γx : gname)
(q qg : Qp)
(M : eView)
(einfo : (gname * option gname * view * eView * Qp * gname))
(EL : list (gname * option gname * view * eView * Qp * gname)) (* mono_list for all event info excluding event type *)
(WL : list (event_id * gname * Qp)) (* mono_list for γs *)
(RL : list event_id) (* mono_list for each generation *)
(GL : list (gname * event_id)) (* mono_list for commit-with relation or seen_event *)
(QM : gmap Qp nat)
(eidx : event_idx).
Local Open Scope nat_scope.
Lemma OmoGname_agree γe γx γx' :
OmoGname γe γx -∗ OmoGname γe γx' -∗ ⌜ γx = γx' ⌝.
Proof.
iIntros "#Hγx #Hγx'". rewrite !OmoGname_eq.
iDestruct "Hγx" as (?????) "[%Hγe Hγx]".
iDestruct "Hγx'" as (?????) "[%Hγe' Hγx']".
encode_agree Hγe.
iDestruct (own_valid_2 with "Hγx Hγx'") as %?%to_agree_op_inv_L. done.
Qed.
Lemma OmoTokenW_contra γe γe' e e' :
OmoTokenW γe' e' -∗ OmoCW γe γe' e e' -∗ False.
Proof.
iIntros "WCOMMIT #e↦e'".
rewrite OmoCW_eq OmoTokenW_eq.
iDestruct "e↦e'" as (??????????) "(%&%&%&%& [%Hγe %Hγe'] & EL@e & EL'@e' & GL@0 & GL@1 & [%Heinfo %Heinfo'])".
iDestruct "WCOMMIT" as (????????) "([%Hγe2 %Heinfo'2] & #EL'@e'2 & GL● & _)".
encode_agree Hγe'. iDestruct (mono_list_idx_agree with "EL'@e' EL'@e'2") as %<-.
encode_agree Heinfo'.
iDestruct (mono_list_auth_idx_lookup with "GL● GL@1") as %?. done.
Qed.
Lemma OmoTokenW_excl γe e :
OmoTokenW γe e -∗ OmoTokenW γe e -∗ False.
Proof.
iIntros "WCOMMIT WCOMMIT'". rewrite OmoTokenW_eq.
iDestruct "WCOMMIT" as (????????) "([%Hγe %Heinfo] & #EL@e & GL● & _)".
iDestruct "WCOMMIT'" as (????????) "([%Hγe' %Heinfo'] & #EL@e' & GL●' & _)".
encode_agree Hγe. iDestruct (mono_list_idx_agree with "EL@e EL@e'") as %<-.
encode_agree Heinfo. iDestruct (mono_list_auth_own_agree with "GL● GL●'") as %[? _]. done.
Qed.
Lemma OmoTokenR_contra γe γe' e e' :
OmoTokenR γe' e' -∗ OmoCW γe γe' e e' -∗ False.
Proof.
iIntros "RCOMMIT #e↦e'".
rewrite OmoCW_eq OmoTokenR_eq.
iDestruct "e↦e'" as (??????????) "(%&%&%&%& [%Hγe %Hγe'] & EL@e & EL'@e' & GL@0 & GL@1 & [%Heinfo %Heinfo'])".
iDestruct "RCOMMIT" as (????????) "([%Hγe2 %Heinfo'2] & #EL'@e'2 & GL● & _)".
encode_agree Hγe'. iDestruct (mono_list_idx_agree with "EL'@e' EL'@e'2") as %<-.
encode_agree Heinfo'.
iDestruct (mono_list_auth_idx_lookup with "GL● GL@1") as %?. done.
Qed.
Lemma OmoTokenR_excl γe e :
OmoTokenR γe e -∗ OmoTokenR γe e -∗ False.
Proof.
iIntros "RCOMMIT RCOMMIT'". rewrite OmoTokenR_eq.
iDestruct "RCOMMIT" as (????????) "([%Hγe %Heinfo] & #EL@e & GL● & _)".
iDestruct "RCOMMIT'" as (????????) "([%Hγe' %Heinfo'] & #EL@e' & GL●' & _)".
encode_agree Hγe. iDestruct (mono_list_idx_agree with "EL@e EL@e'") as %<-.
encode_agree Heinfo. iDestruct (mono_list_auth_own_agree with "GL● GL●'") as %[? _]. done.
Qed.
Lemma OmoTokenWR_excl γe e :
OmoTokenW γe e -∗ OmoTokenR γe e -∗ False.
Proof.
iIntros "WCOMMIT RCOMMIT". rewrite OmoTokenW_eq OmoTokenR_eq.
iDestruct "WCOMMIT" as (????????) "([%Hγe %Heinfo] & #EL@e & GL● & #Hγb)".
iDestruct "RCOMMIT" as (????????) "([%Hγe' %Heinfo'] & #EL@e' & GL●' & #Hγb')".
encode_agree Hγe. iDestruct (mono_list_idx_agree with "EL@e EL@e'") as %<-.
encode_agree Heinfo.
iDestruct (own_valid_2 with "Hγb Hγb'") as %?%to_agree_op_inv_L. done.
Qed.
Lemma OmoEview_nonempty γe M :
OmoEview γe M -∗ ⌜ M ≠ ∅ ⌝.
Proof.
iIntros "#⊒M". rewrite OmoEview_eq.
by iDestruct "⊒M" as (?????) "[[%Hγe %NEmp] BIG]".
Qed.
Lemma OmoEview_nonempty_obj γe M V :
@{V} OmoEview γe M -∗ ⌜ M ≠ ∅ ⌝.
Proof.
iIntros "#⊒M". rewrite OmoEview_eq.
by iDestruct "⊒M" as (?????) "[[%Hγe %NEmp] BIG]".
Qed.
Lemma OmoEview_split γe M1 M2 :
M1 ≠ ∅ → M2 ≠ ∅ →
OmoEview γe M1 ∗ OmoEview γe M2 ⊣⊢ OmoEview γe (M1 ∪ M2).
Proof.
iIntros "%NEmp1 %NEmp2". rewrite OmoEview_eq. iSplit.
- iIntros "[#⊒M1 #⊒M2]".
iDestruct "⊒M1" as (?????) "[[%Hγe _] BIG1]".
iDestruct "⊒M2" as (?????) "[[%Hγe' _] BIG2]". encode_agree Hγe.
iExists γtl,γel,γh,γg,γn. iSplit.
{ iPureIntro. split; [done|]. set_solver. }
iApply big_sepS_forall. iIntros "%e %IN".
have CASE : e ∈ M1 ∨ e ∈ M2 by set_solver.
destruct CASE as [IN'|IN'].
+ by iDestruct (big_sepS_elem_of with "BIG1") as "?".
+ by iDestruct (big_sepS_elem_of with "BIG2") as "?".
- iIntros "#⊒M". iDestruct "⊒M" as (?????) "[[%Hγe _] BIG]". iSplit.
+ iExists γtl,γel,γh,γg,γn. iSplit; [done|]. iApply big_sepS_forall. iIntros "%e %IN".
by iDestruct (big_sepS_elem_of _ _ e with "BIG") as "?"; [set_solver|].
+ iExists γtl,γel,γh,γg,γn. iSplit; [done|]. iApply big_sepS_forall. iIntros "%e %IN".
by iDestruct (big_sepS_elem_of _ _ e with "BIG") as "?"; [set_solver|].
Qed.
Lemma OmoEview_union γe M1 M2 :
OmoEview γe M1 -∗ OmoEview γe M2 -∗
OmoEview γe (M1 ∪ M2).
Proof.
iIntros "#⊒M1 #⊒M2". rewrite OmoEview_eq.
iDestruct "⊒M1" as (?????) "[[%Hγe %NEmp1] BIG1]".
iDestruct "⊒M2" as (?????) "[[%Hγe' %NEmp2] BIG2]". encode_agree Hγe.
iExists γtl,γel,γh,γg,γn. iSplitR.
{ iPureIntro. split; [done|]. set_solver. }
iApply big_sepS_forall. iIntros "%e %IN".
have CASE : e ∈ M1 ∨ e ∈ M2 by set_solver.
destruct CASE as [IN'|IN'].
- by iDestruct (big_sepS_elem_of with "BIG1") as "H".
- by iDestruct (big_sepS_elem_of with "BIG2") as "H".
Qed.
Lemma OmoEview_union_obj γe M1 M2 V :
@{V} OmoEview γe M1 -∗ @{V} OmoEview γe M2 -∗
@{V} OmoEview γe (M1 ∪ M2).
Proof.
iIntros "#⊒M1@V #⊒M2@V". iCombine "⊒M1@V ⊒M2@V" as "RES".
iApply (view_at_mono with "RES"); [done|].
iIntros "[#⊒M1 #⊒M2]". by iApply OmoEview_union.
Qed.
Lemma OmoEview_mono γe M1 M2 :
M2 ⊆ M1 → M2 ≠ ∅ →
OmoEview γe M1 -∗
OmoEview γe M2.
Proof.
iIntros "%SubM2M1 %NEmp #⊒M". rewrite OmoEview_eq.
iDestruct "⊒M" as (?????) "[[%Hγe _] BIG]".
iExists γtl,γel,γh,γg,γn. iSplit; [done|]. iApply big_sepS_forall. iIntros "%e %IN".
iDestruct (big_sepS_elem_of _ _ e with "BIG") as "H"; [set_solver|]. done.
Qed.
Lemma OmoEview_mono_obj γe M1 M2 V :
M2 ⊆ M1 → M2 ≠ ∅ →
@{V} OmoEview γe M1 -∗
@{V} OmoEview γe M2.
Proof.
iIntros "%SubM2M1 %NEmp #⊒M@V". iApply (view_at_mono with "⊒M@V"); [done|].
iIntros "#⊒M". by iApply OmoEview_mono.
Qed.
Lemma OmoEview_latest_elem_obj γe M V :
@{V} OmoEview γe M -∗
∃ e, OmoUB γe M e ∗ ⌜ e ∈ M ⌝.
Proof.
iIntros "#⊒M". rewrite OmoEview_eq.
iDestruct "⊒M" as (?????) "[[%Hγe %NEmp] BIG]".
iInduction M as [|e M NotIn] "IH" using set_ind_L; [done|].
destruct (decide (M = ∅)) as [EQM|Nemp].
{ iExists e. iSplit; [|iPureIntro;set_solver].
have EQ : {[e]} ∪ M = {[e]} by set_solver. rewrite EQ. subst M. clear EQ.
rewrite /OmoUB !big_sepS_singleton OmoLe_eq.
iDestruct "BIG" as (?) "[EL◯ _]". rewrite view_at_objective_iff.
iExists γtl,γel,γh,γg,γn,einfo,einfo. iFrame "EL◯". done. }
rewrite big_sepS_union; [|set_solver]. iDestruct "BIG" as "[BIG1 BIG2]".
iDestruct ("IH" with "[] BIG2") as (e') "[MAX %e'IN]"; [done|].
rewrite big_sepS_singleton. iDestruct "BIG1" as (einfo) "[EL◯ _]".
iAssert (∃ einfo', @{V} ⎡mono_list_idx_own γel e' einfo'⎤)%I with "[]" as (?) "#EL◯'".
{ rewrite -view_at_exist. iApply (view_at_mono with "BIG2"); [done|]. iIntros "BIG".
iDestruct (big_sepS_elem_of with "BIG") as (einfo') "[H _]"; [done|]. iExists einfo'. done. }
rewrite !view_at_objective_iff.
destruct (decide (einfo.1.2 ≤ einfo'.1.2)%Qp) as [LE|LT].
{ iExists e'. iSplit; [|iPureIntro;set_solver]. rewrite /OmoUB big_sepS_union; [|set_solver]. iFrame "MAX".
rewrite big_sepS_singleton OmoLe_eq. iExists γtl,γel,γh,γg,γn,einfo,einfo'. iFrame "EL◯ EL◯'".
iPureIntro. split; [done|]. done. }
rewrite -Qp.lt_nge in LT.
iExists e. iSplit; [|iPureIntro;set_solver]. rewrite /OmoUB big_sepS_union; [|set_solver]. iSplit.
- rewrite big_sepS_singleton OmoLe_eq. iExists γtl,γel,γh,γg,γn,einfo,einfo. iFrame "EL◯". done.
- iApply big_sepS_forall. iIntros "%x %IN". iDestruct (big_sepS_elem_of with "MAX") as "LE"; [exact IN|].
rewrite OmoLe_eq. iDestruct "LE" as (???????) "([%Hγe' %LE] & #EL◯x & #EL◯'')".
encode_agree Hγe. iDestruct (mono_list_idx_agree with "EL◯' EL◯''") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo. iFrame "EL◯x EL◯". iPureIntro. split; [done|].
apply Qp.lt_le_incl. eapply Qp.le_lt_trans; try done.
Qed.
Lemma OmoEview_latest_elem γe M :
OmoEview γe M -∗
∃ e, OmoUB γe M e ∗ ⌜ e ∈ M ⌝.
Proof.
iIntros "#⊒M". iDestruct (view_at_intro with "⊒M") as (V) "[_ ⊒M@V]".
by iApply OmoEview_latest_elem_obj.
Qed.
(* Irreflexitivity of `OmoLt` *)
Lemma OmoLt_irrefl γe e :
OmoLt γe e e -∗ False.
Proof.
iIntros "#e<e". rewrite OmoLt_eq.
iDestruct "e<e" as (???????) "([%Hγe %LT] & #EL@e & #EL@e')".
iDestruct (mono_list_idx_agree with "EL@e EL@e'") as %<-.
have LE : (einfo1.1.2 ≤ einfo1.1.2)%Qp by done.
apply Qp.lt_nge in LT. done.
Qed.
Lemma OmoLt_trans γe e1 e2 e3 :
OmoLt γe e1 e2 -∗
OmoLt γe e2 e3 -∗
OmoLt γe e1 e3.
Proof.
iIntros "#e1<e2 #e2<e3". rewrite OmoLt_eq.
iDestruct "e1<e2" as (???????) "([%Hγe %LT1] & #EL@e1 & #EL@e2)".
iDestruct "e2<e3" as (???????) "([%Hγe' %LT2] & #EL@e2' & #EL@e3)". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2'") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. split; [done|].
transitivity einfo2.1.2; try done.
Qed.
Lemma OmoLe_get_from_Lt γe e1 e2 :
OmoLt γe e1 e2 -∗ OmoLe γe e1 e2.
Proof.
iIntros "#e1<e2". rewrite OmoLe_eq OmoLt_eq.
iDestruct "e1<e2" as (???????) "([%Hγe %LE] & #EL@e1 & #EL@e2)".
iExists γtl,γel,γh,γg,γn,einfo1,einfo2. iFrame "#". iPureIntro. split; [done|].
by apply Qp.lt_le_incl.
Qed.
Lemma OmoLe_get_from_Eq γe e1 e2 :
OmoEq γe e1 e2 -∗ OmoLe γe e1 e2.
Proof.
iIntros "#e1=e2". rewrite OmoLe_eq OmoEq_eq.
iDestruct "e1=e2" as (???????) "([%Hγe %EQ] & #EL@e1 & #EL@e2)".
iExists γtl,γel,γh,γg,γn,einfo1,einfo2. iFrame "#". iPureIntro. rewrite EQ. done.
Qed.
Lemma OmoEq_Le_trans γe e1 e1' e2 :
OmoEq γe e1 e1' -∗
OmoLe γe e1' e2 -∗
OmoLe γe e1 e2.
Proof.
iIntros "#e1=e1' #e1'≤e2". rewrite OmoEq_eq OmoLe_eq.
iDestruct "e1=e1'" as (???????) "([%Hγe %EQ] & #EL@e1 & #EL@e1')".
iDestruct "e1'≤e2" as (???????) "([%Hγe' %LE] & #EL@e1'' & #EL@e2)". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e1' EL@e1''") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. rewrite -EQ in LE. done.
Qed.
Lemma OmoLe_Eq_trans γe e1 e2 e2' :
OmoLe γe e1 e2 -∗
OmoEq γe e2 e2' -∗
OmoLe γe e1 e2'.
Proof.
iIntros "#e1≤e2 #e2=e2'". rewrite OmoEq_eq OmoLe_eq.
iDestruct "e1≤e2" as (???????) "([%Hγe %LE] & #EL@e1 & #EL@e2)".
iDestruct "e2=e2'" as (???????) "([%Hγe' %EQ] & #EL@e2a & #EL@e2')". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2a") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. rewrite EQ in LE. done.
Qed.
Lemma OmoLe_trans γe e1 e2 e3 :
OmoLe γe e1 e2 -∗
OmoLe γe e2 e3 -∗
OmoLe γe e1 e3.
Proof.
iIntros "#e1≤e2 #e2≤e3". rewrite OmoLe_eq.
iDestruct "e1≤e2" as (???????) "([%Hγe %LE1] & #EL@e1 & #EL@e2)".
iDestruct "e2≤e3" as (???????) "([%Hγe' %LE2] & #EL@e2' & #EL@e3)". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2'") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. split; [done|]. transitivity einfo2.1.2; done.
Qed.
Lemma OmoLe_Lt_trans γe e1 e2 e3 :
OmoLe γe e1 e2 -∗
OmoLt γe e2 e3 -∗
OmoLt γe e1 e3.
Proof.
iIntros "#e1≤e2 #e2<e3". rewrite OmoLe_eq OmoLt_eq.
iDestruct "e1≤e2" as (???????) "([%Hγe %LE] & #EL@e1 & #EL@e2)".
iDestruct "e2<e3" as (???????) "([%Hγe' %LT] & #EL@e2' & #EL@e3)". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2'") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. split; [done|].
by eapply Qp.le_lt_trans.
Qed.
Lemma OmoLt_Le_trans γe e1 e2 e3 :
OmoLt γe e1 e2 -∗
OmoLe γe e2 e3 -∗
OmoLt γe e1 e3.
Proof.
iIntros "#e1<e2 #e2≤e3". rewrite OmoLe_eq OmoLt_eq.
iDestruct "e1<e2" as (???????) "([%Hγe %LT] & #EL@e1 & #EL@e2)".
iDestruct "e2≤e3" as (???????) "([%Hγe' %LE] & #EL@e2' & #EL@e3)". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2'") as %<-.
iExists γtl,γel,γh,γg,γn,einfo1,einfo3. iFrame "#". iPureIntro. split; [done|].
by eapply Qp.lt_le_trans.
Qed.
Lemma OmoLe_Lt_contra γe e1 e2 :
OmoLe γe e1 e2 -∗ OmoLt γe e2 e1 -∗ False.
Proof.
iIntros "#e1≤e2 #e2<e1". rewrite OmoLe_eq OmoLt_eq.
iDestruct "e1≤e2" as (???????) "([%Hγe %LE] & #EL@e1 & #EL@e2)".
iDestruct "e2<e1" as (???????) "([%Hγe' %LT] & #EL@e2' & #EL@e1')". encode_agree Hγe.
iDestruct (mono_list_idx_agree with "EL@e1 EL@e1'") as %<-.
iDestruct (mono_list_idx_agree with "EL@e2 EL@e2'") as %<-.
apply Qp.lt_nge in LT. done.
Qed.
Lemma OmoLt_Le_contra γe e1 e2 :
OmoLt γe e1 e2 -∗ OmoLe γe e2 e1 -∗ False.
Proof.
iIntros "#e1<e2 #e2≤e1". by iApply OmoLe_Lt_contra.
Qed.
Lemma OmoEq_get_from_CW γe γe' e e' :
OmoCW γe γe' e e' -∗