-
Notifications
You must be signed in to change notification settings - Fork 1
/
proof_composition.v
6349 lines (5693 loc) · 446 KB
/
proof_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.algebra Require Import lib.mono_list.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import ghost_var ghost_map.
From iris.bi Require Import fractional.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.examples.algebra Require Import mono_list_list saved_vprop.
From gpfsl.logic Require Import logatom atomics invariants.
From gpfsl.logic Require Import repeat_loop new_delete.
From gpfsl.examples Require Import uniq_token map_seq loc_helper algebra.mono_list.
From gpfsl.examples.omo Require Import omo omo_preds append_only_loc.
From gpfsl.examples.arc Require Import code spec_composition.
Require Import iris.prelude.options.
Local Notation ainfo_type := (Qp * view * (gset event_id) * (gset event_id) * append_only_type)%type.
Class arcG Σ := ArcG {
arc_omoGeneralG :> omoGeneralG Σ;
arc_arcG :> omoSpecificG Σ arc_event arc_state;
arc_aolG :> appendOnlyLocG Σ;
(** Qp: fraction of strong/weak/fake arc
view: lower bound of observation of strong/weak/fake arc
gset event_id: lower bound of eView of strong/weak/fake arc
gset event_id: lower bound of set of observed message of weak counter
append_only_type: current state of append_only_loc of weak counter (meaningful only in [sarc]) *)
arc_ainfoG :> ghost_mapG Σ event_id ainfo_type;
arc_aliveG :> ghost_varG Σ bool;
arc_events :> ghost_varG Σ (gset event_id);
arc_gname :> mono_listG gname Σ;
}.
Definition arcΣ : gFunctors :=
#[omoGeneralΣ;
omoSpecificΣ arc_event arc_state;
appendOnlyLocΣ;
ghost_mapΣ event_id ainfo_type;
ghost_varΣ bool;
ghost_varΣ (gset event_id);
mono_listΣ gname].
Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Proof. solve_inG. Qed.
Section Arc.
Context `{!noprolG Σ, !atomicG Σ, !arcG Σ}.
Local Notation iProp := (iProp Σ).
Local Notation vProp := (vProp Σ).
Local Open Scope nat_scope.
Implicit Types
(γg γn γnl γs γsa γwa γb γm γes γss γew γsw γu γd γl γul : gname) (qs qw qsa qwa : Qp) (alive : bool)
(omo omos omow : omoT) (l : loc) (mos mow : list loc_state)
(stlist : list arc_state) (st stf : arc_state)
(eV : omo_event arc_event) (eVl eVs : omo_event loc_event)
(E : history arc_event) (Es Ew : history loc_event)
(arcs sarc warc : gmap event_id ainfo_type)
(ainfo : ainfo_type)
(sdom wdom adom upds dgds lcks ulcks : gset event_id)
.
Definition arcN (N : namespace) := N .@ "arc".
(* Used by [map_fold] in computing summation of Qp field of [sarc] or [warc] *)
Definition frac_sum := λ (e : event_id) (val : ainfo_type) (q : Qp), (val.1.1.1.1 + q)%Qp.
(* Used by [map_fold] in computing summation of view field of [sarc] or [warc] *)
Definition view_join_total := λ (e : event_id) (val : ainfo_type) (V : view), val.1.1.1.2 ⊔ V.
(* Inexistence of [WeakDrop _ true] or [Unique] that destroys Arc *)
Definition ArcAlive E : Prop :=
Forall (λ eV, match eV.(type) with | WeakDrop _ true | Unique _ => False | _ => True end) E.
(* Every StrongArc object should observe [Clone] event that it has involved in *)
Definition SeenClone E sarc : Prop :=
∀ e e' ainfo eV,
sarc !! e = Some ainfo →
E !! e' = Some eV →
eV.(type) = Clone e →
e' ∈ ainfo.1.1.2.
(* Every WeakArc/FakeArc object should observe [WeakClone] event that it has involved in *)
(* Note: in fact, FakeArc cannot perform WeakClone event, but we can still state this invariant *)
Definition SeenWeakClone E warc : Prop :=
∀ e e' ainfo eV,
warc !! e = Some ainfo →
E !! e' = Some eV →
eV.(type) = WeakClone e →
e' ∈ ainfo.1.1.2.
(* Every [Upgrade] event should be observed by some WeakArc *)
(* Note: [upds] records observation of [Upgrade] event by destroyed WeakArc *)
Definition SeenUpgrade E warc upds : Prop :=
∀ e eV,
E !! e = Some eV →
match eV.(type) with
| Upgrade => e ∈ upds ∨ (∃ e' ainfo, warc !! e' = Some ainfo ∧ e ∈ ainfo.1.1.2)
| _ => True
end.
(* Every [Downgrade] event should be observed by some StrongArc *)
(* Note: [dgds] records observation of [Downgrade] event by destroyed StrongArc *)
Definition SeenDowngrade E sarc dgds : Prop :=
∀ e eV,
E !! e = Some eV →
match eV.(type) with
| Downgrade => e ∈ dgds ∨ (∃ e' ainfo, sarc !! e' = Some ainfo ∧ e ∈ ainfo.1.1.2)
| _ => True
end.
(* Every unlocking message is observed by some StrongArc *)
Definition SeenUnlock sarc lcks ulcks : Prop :=
∀ e, e ∈ ulcks → (e ∈ lcks ∨ (∃ e' ainfo, sarc !! e' = Some ainfo ∧ e ∈ ainfo.1.2)).
Definition ArcsValid E adom : Prop :=
∀ e, e ∈ adom → e < length E.
(* Dropped element should not be contained in [sarc] and [warc] *)
Definition ArcsValid2 E sdom wdom : Prop :=
∀ e eV,
E !! e = Some eV →
match eV.(type) with
| StrongDrop e' _ => e' ∉ sdom
| WeakDrop e' _ => e' ∉ wdom
| _ => True
end.
Definition EventIdValid E : Prop :=
∀ e eV,
E !! e = Some eV →
match eV.(type) with
| Clone e' | WeakClone e' | WeakDrop e' _ | StrongDrop e' _ | UnwrapFail e' => e' < length E
| _ => True
end.
Definition ArcsSeen arcs Vp : Prop :=
∀ e ainfo, arcs !! e = Some ainfo → Vp ⊑ ainfo.1.1.1.2.
(* Whenever FakeArc is absent, StrongArc is also absent *)
Definition StlistValid stlist : Prop :=
Forall (λ st, 0 ∉ st.2.1.1 → st.1.1.1 = ∅) stlist.
Definition AllLockMessageInner γew sarc lcks ew : vProp :=
∃ eVw (z : Z),
OmoEinfo γew ew eVw ∗
⌜ (loc_event_msg eVw.(type)).1 = #z
∧ (z = (-1)%Z → (ew ∈ lcks ∨ (∃ e ainfo, sarc !! e = Some ainfo ∧ ew ∈ ainfo.1.2))) ⌝.
Definition AllLockMessage γew esw sarc lcks : vProp :=
[∗ list] ew ∈ esw, AllLockMessageInner γew sarc lcks ew.
(* Every weak event or strong read-only event observes nearest previous strong write event *)
Definition SeenPrevStrong γg γes ess e : vProp :=
(* Case 1: [e] is located later than last strong event *)
(∃ ef esf esfeq, OmoLe γg ef e ∗ OmoEq γes esf esfeq ∗
OmoCW γg γes ef esf ∗ OmoHb γg γes e esfeq ∗ ⌜ last ess = Some esf ⌝)
(* Case 2: [e] is located between two consecutive strong events [el] and [er] *)
∨ (∃ el er esl esleq esr gen,
OmoLe γg el e ∗ OmoLt γg e er ∗ OmoEq γes esl esleq ∗
OmoCW γg γes el esl ∗ OmoCW γg γes er esr ∗ OmoHb γg γes e esleq ∗
⌜ ess !! gen = Some esl ∧ ess !! (gen + 1)%nat = Some esr ⌝).
Definition AllEvents γg γes γm E ess : vProp :=
[∗ list] e↦eV ∈ E,
match eV.(type) with
| StrongInit | WeakInit | Clone _ | Upgrade | StrongDrop _ _ =>
∃ es, OmoCW γg γes e es ∗ OmoHb γg γes e es ∗ CWMonoValid γm e
| _ => SeenPrevStrong γg γes ess e
end.
Definition AllStrongsInner γg γes γs γss γm gen es : vProp :=
∃ e st eVs,
OmoCW γg γes e es ∗ OmoHb γg γes e es ∗ OmoSnap γg γs e st ∗ OmoEinfo γes es eVs ∗ CWMonoValid γm e ∗
(* every strong counter value matches with set size of abstract state *)
⌜ (loc_event_msg eVs.(type)).1 = #(size st.1.1.1) ⌝ ∗
match gen with
| 0 => emp
| S _ => (* Invariant with previous message *)
∃ omos e' es' eV eVs' st',
OmoSnapOmo γes γss omos ∗ OmoCW γg γes e' es' ∗ OmoEinfo γg e eV ∗ OmoEinfo γes es' eVs' ∗ OmoSnap γg γs e' st' ∗ OmoLt γg e' e ∗
⌜ omo_write_op omos !! (gen - 1) = Some es' ∧ (loc_event_msg eVs'.(type)).1 = #(size st'.1.1.1) ∧ size st'.1.1.1 ≠ 0
∧ ( ( (* Case 1: strong count increases by 1 *)
size st.1.1.1 = ((size st'.1.1.1) + 1)%nat ∧ ((∃ e'', eV.(type) = Clone e'' ∧ e'' ∈ st'.1.1.1) ∨ eV.(type) = Upgrade))
∨ ( (* Case 2: strong count decreases by 1 *)
size st.1.1.1 = ((size st'.1.1.1) - 1)%nat ∧ (∃ e'' b, eV.(type) = StrongDrop e'' b))) ⌝
end.
Definition AllStrongs γg γes γs γss γm ess : vProp :=
[∗ list] gen↦es ∈ ess, AllStrongsInner γg γes γs γss γm gen es.
Definition AllWeaksInner γg γew γsw wdom ulcks gen ew : vProp :=
∃ eVw (v : Z),
OmoEinfo γew ew eVw ∗
⌜ (loc_event_msg eVw.(type)).1 = #v ∧ (-1 ≤ v)%Z ⌝ ∗
match gen with
| 0 => emp
| S _ => (* Invariant with previous message *)
∃ omow ew' eVw' (v' : Z),
OmoSnapOmo γew γsw omow ∗ OmoEinfo γew ew' eVw' ∗
⌜ omo_write_op omow !! (gen - 1) = Some ew' ∧ (loc_event_msg eVw'.(type)).1 = #v' ⌝ ∗
( ( (* Case 1: weak count increases by 1 *)
∃ e eV, OmoCW γg γew e ew ∗ OmoEinfo γg e eV ∗ OmoHb γg γew e ew ∗
⌜ (1 ≤ v')%Z ∧ (v = v' + 1)%Z
(** Corresponding event should be either [Downgrade] or [WeakClone].
Here, if weak counter increases from 1 to 2 and if we know that 0 is alive currently,
then we know it should be cloned from WeakArc with id 0 *)
∧ (eV.(type) = Downgrade ∨ (∃ e', eV.(type) = WeakClone e' ∧ ((v' = 1%Z ∧ 0 ∈ wdom) → e' = 0))) ⌝)
∨ ( (* Case 2: weak counter decreases by 1 *)
⌜ (1 ≤ v')%Z ∧ (v = v' - 1)%Z ⌝)
∨ ( (* Case 3: weak counter gets locked (i.e., 1 -> -1) *)
⌜ v' = 1%Z ∧ v = (-1)%Z ⌝)
∨ ( (* Case 4: weak counter gets unlocked (i.e., -1 -> 1) *)
⌜ v' = (-1)%Z ∧ v = 1%Z ∧ ew ∈ ulcks ⌝))
end.
Definition AllWeaks γg γew γsw wdom ulcks esw : vProp :=
[∗ list] gen↦ew ∈ esw, AllWeaksInner γg γew γsw wdom ulcks gen ew.
Definition ArcInternalInvAlive l γg γs γes γss γew γsw γsa γwa γb γm γu γd γl γul E omo ess esw sarc warc qsa qwa stlist (P1 : Qp → vProp) (P2 : vProp) : vProp :=
∃ Vbs Vbw ty uf stf esf ewf eVsf eVwf (nsf : nat) (zwf : Z) Vsf Vwf Vp q1 q2 qu qd upds dgds lcks ulcks,
AllEvents γg γes γm E ess ∗
AllStrongs γg γes γs γss γm ess ∗
AllWeaks γg γew γsw (dom warc) ulcks esw ∗
@{Vbs} append_only_loc l γes ∅ cas_only ∗
@{Vbw} append_only_loc (l >> 1) γew uf ty ∗
(** [upds]: set of [Upgrade] event observed by destroyed WeakArc
[dgds]: set of [Downgrade] event observed by destroyed StrongArc
[lcks]: set of locking/unlocking message of weak counter observed by destroyed StrongArc
[ulcks]: set of entire unlocking message of weak counter *)
⎡ghost_var γu qu upds⎤ ∗
⎡ghost_var γd qd dgds⎤ ∗
⎡ghost_var γl qd lcks⎤ ∗
⎡ghost_var γul qwa ulcks⎤ ∗
AllLockMessage γew esw sarc lcks ∗
@{Vwf} (OmoEview γg upds ∗ OmoEview γew ulcks) ∗
(* @{Vsf} (OmoEview γg dgds ∗ OmoEview γew lcks) ∗ *)
OmoEinfo γes esf eVsf ∗
OmoEinfo γew ewf eVwf ∗
(* P1 is stored in this invariant whenever strong arc counter is nonzero *)
match nsf with
| 0 => emp
| S _ =>
@{Vp} (P1 q1) ∗ @{Vsf} (P1 q2 ∗ OmoEview γg dgds ∗ OmoEview γew lcks) ∗ (∃ eV0, OmoEinfo γg 0 eV0 ∗ ⌜ eV0.(type) = StrongInit ⌝) ∗
⎡0 ↪[γwa] ((1/2)%Qp, Vp, ∅, ∅, cas_only)⎤ ∗ ⎡ghost_var γb (1/2/2)%Qp true⎤ ∗ ⎡ghost_var γul (1/2)%Qp ulcks⎤ ∗
⌜ qd = 1%Qp ⌝ (* New [Downgrade] event can be inserted only if there exists a strong arc *)
end ∗
(** P2 is stored in this invariant
whenever [fake_arc] has been returned or the Arc has been initialized by [create_weak] *)
match warc !! 0 with
| None => @{Vwf} P2
| _ => emp
end ∗
(* Weak arc counter can be in [swriter] mode iff it is currently locked *)
match ty with
| cas_only =>
( (∃ e, OmoHb γg γew e ewf) ∨ (∃ e ainfo, ⌜ sarc !! e = Some ainfo ∧ ewf ∈ ainfo.1.2 ⌝) ∨ ⌜ nsf = 0 ⌝) ∗
⌜ zwf = Z.of_nat (size stf.2.1.1) ∧ qu = 1%Qp ⌝ (* New [Upgrade] event can only be inserted if current weak counter is unlocked *)
| swriter =>
⌜ zwf = (-1)%Z ∧ size stf.2.1.1 = 1
∧ (∃ e ainfo, e ∈ stf.1.1.1 ∧ sarc !! e = Some ainfo ∧ ainfo.2 = swriter)
∧ qu = (1/2)%Qp ⌝
end ∗
(* Reading last message of strong/weak counter guarantees observing event view in corresponding abstract state *)
@{Vsf} OmoEview γg (stf.1.2) ∗
@{Vwf} OmoEview γg (stf.2.2) ∗
⌜ uf ⊆ {[#(-1)]} ∧ last ess = Some esf ∧ last esw = Some ewf
∧ loc_event_msg eVsf.(type) = (#nsf, Vsf)
∧ loc_event_msg eVwf.(type) = (#zwf, Vwf)
∧ map_fold frac_sum qsa sarc = 1%Qp
∧ map_fold frac_sum qwa warc = 1%Qp
∧ ArcsValid E (dom sarc) ∧ ArcsValid E (dom warc) ∧ ArcsValid2 E (dom sarc) (dom warc)
∧ SeenClone E sarc ∧ SeenWeakClone E warc
∧ omo_write_op omo !! 0 = Some 0
(* [sarc] and [warc] should contain exactly strong/weak arc objects that are alive *)
∧ last stlist = Some stf ∧ dom sarc = stf.1.1.1 ∧ dom warc = stf.2.1.1
∧ qsa = (q1 + q2)%Qp
∧ ArcAlive E ∧ EventIdValid E
(* Collecting all thread views and message view guarantees observing all events *)
∧ Vbs ⊔ Vbw ⊑ (map_fold view_join_total Vp sarc) ⊔ (map_fold view_join_total Vp warc) ⊔ Vsf ⊔ Vwf
(* Reading last message of strong/weak counter guarantees observing physical view in abstract state *)
∧ stf.1.1.2 ⊑ Vsf ∧ stf.2.1.2 ⊑ Vwf
(* Observation of [Upgrade], [Downgrade], and unlocking message *)
∧ SeenUpgrade E warc upds ∧ SeenDowngrade E sarc dgds ∧ SeenUnlock sarc lcks ulcks
(* Vp is observed by all arcs *)
∧ ArcsSeen sarc Vp ∧ ArcsSeen warc Vp
(* Whenever FakeArc is absent, StrongArc is also absent *)
∧ StlistValid stlist
(* If there is no strong arc, all events regarding strong arcs are recorded in weak arcs *)
∧ (if (decide (nsf = 0)) then Vsf ⊑ (map_fold view_join_total Vp warc) ⊔ Vwf else True)
∧ nsf = size stf.1.1.1 ⌝.
Definition ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul : vProp :=
∃ γnl γn, OmoGname γg γnl ∗ ⎡mono_list_idx_own γnl 0 γn⎤ ∗
⌜ γn = encode (γsa,γwa,γb,γm,γes,γss,γew,γsw,γu,γd,γl,γul) ⌝.
Definition ArcInternalInv γg l (P1 : Qp → vProp) (P2 : vProp) : vProp :=
∃ γsa γwa γs γb γm γes γss γew γsw γu γd γl γul sarc warc qsa qwa alive E Es Ew omo omos omow stlist mos mow Mono,
ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul ∗
OmoAuth γg γs (1/2)%Qp E omo stlist _ ∗
OmoAuth γes γss (1/2)%Qp Es omos mos _ ∗
OmoAuth γew γsw (1/2)%Qp Ew omow mow _ ∗
⎡ghost_map_auth γsa 1 sarc⎤ ∗
⎡ghost_map_auth γwa 1 warc⎤ ∗
⎡ghost_var γb (qsa/2 + qwa/2)%Qp alive⎤ ∗
CWMono γg γes γm Mono ∗
(if alive then
ArcInternalInvAlive l γg γs γes γss γew γsw γsa γwa γb γm γu γd γl γul E omo (omo_write_op omos) (omo_write_op omow) sarc warc qsa qwa stlist P1 P2
else emp).
Definition ArcInv γg γs (l : loc) E omo stlist : vProp := OmoAuth γg γs (1/2)%Qp E omo stlist _.
Definition InternInv N γg l P1 P2 : vProp := inv (arcN N) (ArcInternalInv γg l P1 P2).
Definition StrongArc N γg l q P1 P2 M e : vProp :=
∃ γsa γwa γb γm γes γss γew γsw γu γd γl γul Ms Mw eV ainfo,
ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul ∗
InternInv N γg l P1 P2 ∗
OmoEview γg M ∗
OmoEview γes Ms ∗
OmoEview γew Mw ∗
OmoEinfo γg e eV ∗
⊒ainfo.1.1.1.2 ∗
⎡ghost_var γb (ainfo.1.1.1.1/2)%Qp true⎤ ∗ (* Arc is alive *)
⎡e ↪[γsa] ainfo⎤ ∗
⌜ q = ainfo.1.1.1.1 ∧ ainfo.2 = cas_only ∧ e ∈ M ∧ (eV.(type) = StrongInit ∨ (∃ e', eV.(type) = Clone e') ∨ eV.(type) = Upgrade)
∧ ainfo.1.1.2 ⊆ M ∧ ainfo.1.2 ⊆ Mw ⌝
.
Definition WeakArc N γg l P1 P2 M e : vProp :=
∃ γsa γwa γb γm γes γss γew γsw γu γd γl γul Ms Mw eV ainfo ulcks,
ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul ∗
InternInv N γg l P1 P2 ∗
OmoEview γg M ∗
OmoEview γes Ms ∗
OmoEview γew Mw ∗
OmoEinfo γg e eV ∗
⊒ainfo.1.1.1.2 ∗
⎡ghost_var γb (ainfo.1.1.1.1/2)%Qp true⎤ ∗ (* Arc is alive *)
⎡e ↪[γwa] ainfo⎤ ∗
⎡ghost_var γul ainfo.1.1.1.1 ulcks⎤ ∗
(if (decide (e = 0)) then P2 ∗ ⌜ eV.(type) = WeakInit ⌝ else emp) ∗
⌜ ainfo.2 = cas_only ∧ e ∈ M ∧ (eV.(type) = StrongInit ∨ eV.(type) = WeakInit ∨ (∃ e', eV.(type) = WeakClone e') ∨ eV.(type) = Downgrade)
∧ ainfo.1.1.2 ⊆ M ∧ ainfo.1.2 ∪ ulcks ⊆ Mw ⌝
.
Definition FakeArc N γg l P1 P2 M : vProp :=
∃ γsa γwa γb γm γes γss γew γsw γu γd γl γul Ms Mw e eV0 eV ainfo dgds ulcks qd,
ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul ∗
InternInv N γg l P1 P2 ∗
OmoEview γg M ∗
OmoEview γes Ms ∗
OmoEview γew Mw ∗
OmoEinfo γg 0 eV0 ∗
OmoEinfo γg e eV ∗
⊒ainfo.1.1.1.2 ∗
⎡ghost_var γb (ainfo.1.1.1.1/2)%Qp true⎤ ∗ (* Arc is alive *)
⎡0 ↪[γwa] ainfo⎤ ∗
⎡ghost_var γul ainfo.1.1.1.1 ulcks⎤ ∗
⎡ghost_var γd qd dgds⎤ ∗
⌜ ainfo.2 = cas_only ∧ e ∈ M ∧ eV0.(type) = StrongInit ∧ (∃ e', eV.(type) = StrongDrop e' true)
∧ ainfo.1.1.2 ∪ dgds ⊆ M ∧ ainfo.1.2 ∪ ulcks ⊆ Mw ⌝
.
Local Instance AllEvents_timeless γg γes γm E ess : Timeless (AllEvents γg γes γm E ess).
Proof. apply big_sepL_timeless. intros. destruct (x.(type)); apply _. Qed.
Local Instance AllEvents_persistent γg γes γm E ess : Persistent (AllEvents γg γes γm E ess).
Proof. apply big_sepL_persistent. intros. destruct (x.(type)); apply _. Qed.
Local Instance AllEvents_objective γg γes γm E ess : Objective (AllEvents γg γes γm E ess).
Proof. apply big_sepL_objective. intros. destruct (x.(type)); apply _. Qed.
Local Instance AllStrongsInner_timeless γg γes γs γss γm gen es : Timeless (AllStrongsInner γg γes γs γss γm gen es).
Proof. repeat (apply @bi.exist_timeless; intros). destruct gen; apply _. Qed.
Local Instance AllStrongsInner_persistent γg γes γs γss γm gen es : Persistent (AllStrongsInner γg γes γs γss γm gen es).
Proof. repeat (apply @bi.exist_persistent; intros). destruct gen; apply _. Qed.
Local Instance AllStrongsInner_objective γg γes γs γss γm gen es : Objective (AllStrongsInner γg γes γs γss γm gen es).
Proof. repeat (apply exists_objective; intros). destruct gen; apply _. Qed.
Local Instance AllWeaksInner_timeless γg γew γsw wdom ulcks gen ew : Timeless (AllWeaksInner γg γew γsw wdom ulcks gen ew).
Proof. repeat (apply @bi.exist_timeless; intros). destruct gen; apply _. Qed.
Local Instance AllWeaksInner_persistent γg γew γsw wdom ulcks gen ew : Persistent (AllWeaksInner γg γew γsw wdom ulcks gen ew).
Proof. repeat (apply @bi.exist_persistent; intros). destruct gen; apply _. Qed.
Local Instance AllWeaksInner_objective γg γew γsw wdom ulcks gen ew : Objective (AllWeaksInner γg γew γsw wdom ulcks gen ew).
Proof. repeat (apply exists_objective; intros). destruct gen; apply _. Qed.
Local Instance ArcInternalInvAlive_objective l γg γs γes γss γew γsw γsa γwa γb γm γu γd γl γul E omo ess esw sarc warc qsa qwa stlist P1 P2 :
Objective (ArcInternalInvAlive l γg γs γes γss γew γsw γsa γwa γb γm γu γd γl γul E omo ess esw sarc warc qsa qwa stlist P1 P2).
Proof.
repeat (apply exists_objective; intros). repeat (apply sep_objective; try apply _);
[destruct x8; apply _|destruct (warc !! 0); apply _|destruct x1; apply _].
Qed.
Local Instance ArcInternalInv_objective γg l P1 P2 : Objective (ArcInternalInv γg l P1 P2).
Proof. repeat (apply exists_objective; intros). repeat (apply sep_objective; try apply _). destruct x16; apply _. Qed.
Lemma ArcGname_agree γg γsa γsa' γwa γwa' γb γb' γm γm' γes γes' γss γss' γew γew' γsw γsw' γu γu' γd γd' γl γl' γul γul' :
ArcGname γg γsa γwa γb γm γes γss γew γsw γu γd γl γul -∗
ArcGname γg γsa' γwa' γb' γm' γes' γss' γew' γsw' γu' γd' γl' γul' -∗
⌜ γsa = γsa' ∧ γwa = γwa' ∧ γb = γb' ∧ γm = γm' ∧ γes = γes' ∧ γss = γss' ∧ γew = γew' ∧ γsw = γsw' ∧ γu = γu' ∧ γd = γd' ∧ γl = γl' ∧ γul = γul' ⌝.
Proof.
iDestruct 1 as (γnl γn) "(#Hγnl & #Hγn & %Hγn)". iDestruct 1 as (γnl' γn') "(#Hγnl' & #Hγn' & %Hγn')".
iDestruct (OmoGname_agree with "Hγnl Hγnl'") as %<-. iDestruct (mono_list_idx_agree with "Hγn Hγn'") as %<-.
encode_agree Hγn. subst γul'. done.
Qed.
Local Tactic Notation "gname_agree" "with" constr(Hs) :=
iDestruct (ArcGname_agree with Hs) as %(<- & <- & <- & <- & <- & <- & <- & <- & <- & <- & <- & <-).
Lemma dom_same arcs e ainfo ainfo' (arcs' := <[ e := ainfo' ]> (delete e arcs))
(He : arcs !! e = Some ainfo) :
dom arcs = dom arcs'.
Proof.
subst arcs'. rewrite dom_insert_L dom_delete_L. apply elem_of_dom_2 in He. apply set_eq. intros.
split; intros; try set_solver. destruct (decide (x = e)) as [->|NEQ]; try set_solver.
Qed.
Lemma frac_sum_wf arcs :
∀ (j1 j2 : event_id) (z1 z2 : Qp * view * gset event_id * gset event_id * append_only_type) (y : Qp),
j1 ≠ j2
→ arcs !! j1 = Some z1
→ arcs !! j2 = Some z2
→ frac_sum j1 z1 (frac_sum j2 z2 y) = frac_sum j2 z2 (frac_sum j1 z1 y).
Proof. intros. by rewrite /frac_sum Qp.add_assoc (Qp.add_comm z1.1.1.1.1 z2.1.1.1.1) -Qp.add_assoc. Qed.
(* FIXME: A lemma [map_fold_singleton] exists in the latest stdpp, but current version does not include it *)
Lemma map_fold_singleton_frac_sum b i x :
map_fold frac_sum b {[i:=x]} = frac_sum i x b.
Proof. rewrite map_fold_insert_L; [|by apply frac_sum_wf|done]. by rewrite map_fold_empty. Qed.
Lemma map_fold_singleton_view_join_total b i x :
map_fold view_join_total b {[i:=x]} = view_join_total i x b.
Proof. rewrite map_fold_insert_L; [|solve_lat|done]. by rewrite map_fold_empty. Qed.
Lemma map_fold_init_frac_op arcs qb1 qb2 :
map_fold frac_sum (qb1 + qb2)%Qp arcs = (qb1 + map_fold frac_sum qb2 arcs)%Qp.
Proof.
generalize dependent arcs. induction arcs using map_ind; [done|].
do 2 (rewrite map_fold_insert_L; [|by apply frac_sum_wf|done]).
by rewrite IHarcs /frac_sum /= Qp.add_assoc (Qp.add_comm (x.1.1.1.1)) -Qp.add_assoc.
Qed.
Lemma map_fold_init_frac arcs qb :
map_fold frac_sum qb arcs = (qb/2 + map_fold frac_sum (qb/2) arcs)%Qp.
Proof.
have EQ : (qb = qb/2 + qb/2)%Qp by rewrite Qp.add_diag Qp.mul_div_r.
rewrite {1}EQ. apply map_fold_init_frac_op.
Qed.
Lemma EventIdValid_update E eV
(EIDVAL : EventIdValid E)
(NEWVAL : match eV.(type) with
| Clone e' | WeakClone e' | WeakDrop e' _ | StrongDrop e' _ | UnwrapFail e' => e' < length E
| _ => True
end) :
EventIdValid (E ++ [eV]).
Proof.
unfold EventIdValid. intros. destruct (decide (e = length E)) as [->|NEQ].
- rewrite lookup_app_1_eq in H. inversion H. subst eV0.
destruct (eV.(type)); try done; rewrite app_length /=; lia.
- rewrite lookup_app_1_ne in H; [|done]. apply EIDVAL in H.
destruct (eV0.(type)); try done; rewrite app_length /=; lia.
Qed.
Lemma sarc_update_1 sarc e ainfo ainfo' qsa E warc st (sarc' := <[e:=ainfo']> (delete e sarc))
(He : sarc !! e = Some ainfo)
(Hq : ainfo'.1.1.1.1 = ainfo.1.1.1.1)
(Hv : ainfo.1.1.1.2 ⊑ ainfo'.1.1.1.2)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(Hqsa : map_fold frac_sum qsa sarc = 1%Qp)
(VALsarc : ArcsValid E (dom sarc))
(VALsarcwarc : ArcsValid2 E (dom sarc) (dom warc))
(HSeenClone : SeenClone E sarc)
(HDOM : dom sarc = st.1.1.1) :
map_fold frac_sum qsa sarc' = 1%Qp ∧ ArcsValid E (dom sarc') ∧ ArcsValid2 E (dom sarc') (dom warc) ∧ SeenClone E sarc' ∧ dom sarc' = st.1.1.1.
Proof.
subst sarc'. apply (dom_same _ _ _ ainfo') in He as EQdom. rewrite -EQdom. split_and!; try done.
- rewrite map_fold_insert_L; [|by apply frac_sum_wf|by apply lookup_delete].
have EQ : frac_sum e ainfo' (map_fold frac_sum qsa (delete e sarc)) = frac_sum e ainfo (map_fold frac_sum qsa (delete e sarc)).
{ by rewrite /frac_sum Hq. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [done|..|done].
intros. by rewrite /frac_sum Qp.add_assoc (Qp.add_comm z1.1.1.1.1 z2.1.1.1.1) -Qp.add_assoc.
- unfold SeenClone. intros. destruct (decide (e0 = e)) as [->|NEQ].
+ specialize (HSeenClone _ _ _ _ He H0 H1). rewrite lookup_insert in H. inversion H. set_solver.
+ eapply HSeenClone; try done. rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done]. done.
Qed.
Lemma warc_update_1 warc e ainfo ainfo' qwa E sarc st (warc' := <[e:=ainfo']> (delete e warc))
(He : warc !! e = Some ainfo)
(Hq : ainfo'.1.1.1.1 = ainfo.1.1.1.1)
(Hv : ainfo.1.1.1.2 ⊑ ainfo'.1.1.1.2)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(Hqwa : map_fold frac_sum qwa warc = 1%Qp)
(VALwarc : ArcsValid E (dom warc))
(VALsarcwarc : ArcsValid2 E (dom sarc) (dom warc))
(HSeenWeakClone : SeenWeakClone E warc)
(HDOM : dom warc = st.2.1.1) :
map_fold frac_sum qwa warc' = 1%Qp ∧ ArcsValid E (dom warc') ∧ ArcsValid2 E (dom sarc) (dom warc')
∧ SeenWeakClone E warc' ∧ dom warc' = st.2.1.1.
Proof.
subst warc'. apply (dom_same _ _ _ ainfo') in He as EQdom. rewrite -EQdom. split_and!; try done.
- rewrite map_fold_insert_L; [|by apply frac_sum_wf|by apply lookup_delete].
have EQ : frac_sum e ainfo' (map_fold frac_sum qwa (delete e warc)) = frac_sum e ainfo (map_fold frac_sum qwa (delete e warc)).
{ by rewrite /frac_sum Hq. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [done|..|done].
intros. by rewrite /frac_sum Qp.add_assoc (Qp.add_comm z1.1.1.1.1 z2.1.1.1.1) -Qp.add_assoc.
- unfold SeenWeakClone. intros. destruct (decide (e0 = e)) as [->|NEQ].
+ specialize (HSeenWeakClone _ _ _ _ He H0 H1). rewrite lookup_insert in H. inversion H. set_solver.
+ eapply HSeenWeakClone; try done. rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done]. done.
Qed.
Lemma sarc_update_snoc_1 sarc e ainfo ainfo' qsa E eV warc st (sarc' := <[e:=ainfo']> (delete e sarc)) (E' := E ++ [eV])
(He : sarc !! e = Some ainfo)
(Hq : ainfo'.1.1.1.1 = ainfo.1.1.1.1)
(Hv : ainfo.1.1.1.2 ⊑ ainfo'.1.1.1.2)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(Hqsa : map_fold frac_sum qsa sarc = 1%Qp)
(VALsarc : ArcsValid E (dom sarc))
(VALwarc : ArcsValid E (dom warc))
(VALsarcwarc : ArcsValid2 E (dom sarc) (dom warc))
(HSeenClone : SeenClone E sarc)
(HSeenWeakClone : SeenWeakClone E warc)
(HDOM : dom sarc = st.1.1.1)
(HeV : match eV.(type) with
| Clone e' => e = e' ∧ length E ∈ ainfo'.1.1.2
| WeakClone _ => False
| StrongDrop e' _ => e' ∉ dom sarc
| WeakDrop e' _ => e' ∉ dom warc
| _ => True
end) :
map_fold frac_sum qsa sarc' = 1%Qp ∧ ArcsValid E' (dom sarc') ∧ ArcsValid E' (dom warc)
∧ ArcsValid2 E' (dom sarc') (dom warc) ∧ SeenClone E' sarc' ∧ SeenWeakClone E' warc ∧ dom sarc' = st.1.1.1.
Proof.
subst sarc' E'. apply (dom_same _ _ _ ainfo') in He as EQdom. rewrite -EQdom. split_and!; try done.
- rewrite map_fold_insert_L; [|by apply frac_sum_wf|by apply lookup_delete].
have EQ : frac_sum e ainfo' (map_fold frac_sum qsa (delete e sarc)) = frac_sum e ainfo (map_fold frac_sum qsa (delete e sarc)).
{ by rewrite /frac_sum Hq. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [done|..|done].
intros. by rewrite /frac_sum Qp.add_assoc (Qp.add_comm z1.1.1.1.1 z2.1.1.1.1) -Qp.add_assoc.
- unfold ArcsValid. intros. apply VALsarc in H. rewrite app_length /=. lia.
- unfold ArcsValid. intros. apply VALwarc in H. rewrite app_length /=. lia.
- unfold ArcsValid2. intros. destruct (decide (e0 = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H. inversion H. subst eV0. destruct (eV.(type)); try done.
+ rewrite lookup_app_1_ne in H; [|done]. apply VALsarcwarc in H. done.
- unfold SeenClone. intros. destruct (decide (e' = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H0. inversion H0. subst eV0.
rewrite H1 in HeV. destruct HeV as [<- eIN]. rewrite lookup_insert in H. inversion H. subst ainfo0. done.
+ rewrite lookup_app_1_ne in H0; [|done]. destruct (decide (e0 = e)) as [->|NEQ'].
* specialize (HSeenClone _ _ _ _ He H0 H1). rewrite lookup_insert in H. inversion H. set_solver.
* eapply HSeenClone; try done. rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done]. done.
- unfold SeenWeakClone. intros. destruct (decide (e' = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H0. inversion H0. subst eV0. rewrite H1 in HeV. done.
+ rewrite lookup_app_1_ne in H0; [|done]. eapply HSeenWeakClone; try done.
Qed.
Lemma warc_update_snoc_1 warc e ainfo ainfo' qwa E eV sarc sarc' st (warc' := <[e:=ainfo']> (delete e warc)) (E' := E ++ [eV])
(He : warc !! e = Some ainfo)
(Hq : ainfo'.1.1.1.1 = ainfo.1.1.1.1)
(Hv : ainfo.1.1.1.2 ⊑ ainfo'.1.1.1.2)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(Hqsa : map_fold frac_sum qwa warc = 1%Qp)
(VALsarc : ArcsValid E (dom sarc))
(VALwarc : ArcsValid E (dom warc))
(VALsarcwarc : ArcsValid2 E (dom sarc) (dom warc))
(HSeenClone : SeenClone E sarc)
(HSeenWeakClone : SeenWeakClone E warc)
(HDOM : dom warc = st.2.1.1)
(Subsarc : sarc' ⊆ sarc)
(HeV : match eV.(type) with
| Clone _ => False
| WeakClone e' => e = e' ∧ length E ∈ ainfo'.1.1.2
| StrongDrop e' _ => e' ∉ dom sarc'
| WeakDrop e' _ => e' ∉ dom warc
| _ => True
end) :
map_fold frac_sum qwa warc' = 1%Qp ∧ ArcsValid E' (dom sarc') ∧ ArcsValid E' (dom warc')
∧ ArcsValid2 E' (dom sarc') (dom warc') ∧ SeenClone E' sarc' ∧ SeenWeakClone E' warc' ∧ dom warc' = st.2.1.1.
Proof.
apply subseteq_dom in Subsarc as DSubarc.
subst warc' E'. apply (dom_same _ _ _ ainfo') in He as EQdom. rewrite -EQdom. split_and!; try done.
- rewrite map_fold_insert_L; [|by apply frac_sum_wf|by apply lookup_delete].
have EQ : frac_sum e ainfo' (map_fold frac_sum qwa (delete e warc)) = frac_sum e ainfo (map_fold frac_sum qwa (delete e warc)).
{ by rewrite /frac_sum Hq. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [done|..|done].
intros. by rewrite /frac_sum Qp.add_assoc (Qp.add_comm z1.1.1.1.1 z2.1.1.1.1) -Qp.add_assoc.
- unfold ArcsValid. intros. have H' : e0 ∈ dom sarc by set_solver. apply VALsarc in H'. rewrite app_length /=. lia.
- unfold ArcsValid. intros. apply VALwarc in H. rewrite app_length /=. lia.
- unfold ArcsValid2. intros. destruct (decide (e0 = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H. inversion H. subst eV0. destruct (eV.(type)); try done.
+ rewrite lookup_app_1_ne in H; [|done]. apply VALsarcwarc in H. destruct (eV0.(type)); try done; try set_solver.
- unfold SeenClone. intros. destruct (decide (e' = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H0. inversion H0. subst eV0. by rewrite H1 in HeV.
+ rewrite lookup_app_1_ne in H0; [|done]. eapply lookup_weaken in H; [|done]. eapply HSeenClone; try done.
- unfold SeenWeakClone. intros. destruct (decide (e' = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H0. inversion H0. subst eV0. rewrite H1 in HeV.
destruct HeV as [<- IN]. rewrite lookup_insert in H. inversion H. subst ainfo0. set_solver.
+ rewrite lookup_app_1_ne in H0; [|done]. destruct (decide (e0 = e)) as [->|NEQ'].
* rewrite lookup_insert in H. inversion H. subst ainfo0. set_solver.
* rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done]. eapply HSeenWeakClone; try done.
Qed.
Lemma sarc_update_2 sarc e ainfo ainfo' V Vp E dgds lcks lcks' ulcks (sarc' := <[e:=ainfo']> (delete e sarc))
(He : sarc !! e = Some ainfo)
(Hv : ainfo'.1.1.1.2 = ainfo.1.1.1.2 ⊔ V)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(Sublcks : lcks ⊆ lcks')
(HSeenDowngrade : SeenDowngrade E sarc dgds)
(HSeenUnlock : SeenUnlock sarc lcks ulcks)
(LEsarc : ArcsSeen sarc Vp) :
map_fold view_join_total Vp sarc' = map_fold view_join_total Vp sarc ⊔ V ∧ SeenDowngrade E sarc' dgds
∧ SeenUnlock sarc' lcks' ulcks ∧ ArcsSeen sarc' Vp.
Proof.
subst sarc'. split_and!.
- rewrite map_fold_insert_L; [|solve_lat|apply lookup_delete].
have EQ : view_join_total e ainfo' (map_fold view_join_total Vp (delete e sarc)) =
(view_join_total e ainfo (map_fold view_join_total Vp (delete e sarc))) ⊔ V.
{ rewrite /view_join_total Hv /=. solve_lat. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [|solve_lat|done]. solve_lat.
- unfold SeenDowngrade. intros. apply HSeenDowngrade in H. destruct (eV.(type)); try done.
destruct H as [H|H]; [by left|]. right. destruct H as (e' & ainfo'' & He' & IN). destruct (decide (e' = e)) as [->|NEQ].
+ rewrite He in He'. inversion He'. subst ainfo''. exists e,ainfo'. split; [|set_solver].
rewrite lookup_insert. done.
+ exists e',ainfo''. split; [|done]. rewrite lookup_insert_ne; [|done]. rewrite lookup_delete_ne; [|done]. done.
- unfold SeenUnlock. intros. apply HSeenUnlock in H. destruct H as [H|H]; [by left;set_solver|].
destruct H as (e' & ainfo'' & He' & IN). right. destruct (decide (e' = e)) as [->|NEQ].
+ rewrite He in He'. inversion He'. subst ainfo''.
exists e,ainfo'. rewrite lookup_insert. split; [done|]. set_solver.
+ exists e',ainfo''. rewrite lookup_insert_ne; [|done]. rewrite lookup_delete_ne; [|done]. done.
- unfold ArcsSeen. intros. destruct (decide (e0 = e)) as [->|NEQ].
+ rewrite lookup_insert in H. inversion H. subst ainfo0.
apply LEsarc in He. rewrite Hv. solve_lat.
+ rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done].
apply LEsarc in H. done.
Qed.
Lemma warc_update_2 warc e ainfo ainfo' V Vp E upds (warc' := <[e:=ainfo']> (delete e warc))
(He : warc !! e = Some ainfo)
(Hv : ainfo'.1.1.1.2 = ainfo.1.1.1.2 ⊔ V)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HSeenUpgrade : SeenUpgrade E warc upds)
(LEwarc : ArcsSeen warc Vp) :
map_fold view_join_total Vp warc' = map_fold view_join_total Vp warc ⊔ V ∧ SeenUpgrade E warc' upds ∧ ArcsSeen warc' Vp.
Proof.
subst warc'. split_and!.
- rewrite map_fold_insert_L; [|solve_lat|apply lookup_delete].
have EQ : view_join_total e ainfo' (map_fold view_join_total Vp (delete e warc)) =
(view_join_total e ainfo (map_fold view_join_total Vp (delete e warc))) ⊔ V.
{ rewrite /view_join_total Hv /=. solve_lat. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [|solve_lat|done]. solve_lat.
- unfold SeenUpgrade. intros. apply HSeenUpgrade in H. destruct (eV.(type)); try done.
destruct H as [H|H]; [by left|]. right. destruct H as (e' & ainfo'' & He' & IN). destruct (decide (e' = e)) as [->|NEQ].
+ rewrite He in He'. inversion He'. subst ainfo''. exists e,ainfo'. split; [|set_solver].
rewrite lookup_insert. done.
+ exists e',ainfo''. split; [|done]. rewrite lookup_insert_ne; [|done]. rewrite lookup_delete_ne; [|done]. done.
- unfold ArcsSeen. intros. destruct (decide (e0 = e)) as [->|NEQ].
+ rewrite lookup_insert in H. inversion H. subst ainfo0.
apply LEwarc in He. rewrite Hv. solve_lat.
+ rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done].
apply LEwarc in H. done.
Qed.
Lemma sarc_update_snoc_2 sarc e ainfo ainfo' V Vp E eV warc upds dgds dgds' lcks ulcks
(sarc' := <[e:=ainfo']> (delete e sarc))
(E' := E ++ [eV])
(He : sarc !! e = Some ainfo)
(Hv : ainfo'.1.1.1.2 = ainfo.1.1.1.2 ⊔ V)
(HM : ainfo.1.1.2 ⊆ ainfo'.1.1.2)
(HMw : ainfo.1.2 ⊆ ainfo'.1.2)
(HSeenUpgrade : SeenUpgrade E warc upds)
(HSeenDowngrade : SeenDowngrade E sarc dgds)
(HSeenUnlock : SeenUnlock sarc lcks ulcks)
(LEsarc : ArcsSeen sarc Vp)
(Subdgds : dgds ⊆ dgds')
(HeV : match eV.(type) with
| Upgrade => False
| Downgrade => length E ∈ dgds' ∨ length E ∈ ainfo'.1.1.2
| _ => True
end) :
map_fold view_join_total Vp sarc' = map_fold view_join_total Vp sarc ⊔ V
∧ SeenUpgrade E' warc upds ∧ SeenDowngrade E' sarc' dgds' ∧ SeenUnlock sarc' lcks ulcks ∧ ArcsSeen sarc' Vp.
Proof.
subst sarc' E'. split_and!.
- rewrite map_fold_insert_L; [|solve_lat|apply lookup_delete].
have EQ : view_join_total e ainfo' (map_fold view_join_total Vp (delete e sarc)) =
(view_join_total e ainfo (map_fold view_join_total Vp (delete e sarc))) ⊔ V.
{ rewrite /view_join_total Hv /=. solve_lat. }
rewrite EQ. clear EQ. rewrite -map_fold_delete_L; [|solve_lat|done]. solve_lat.
- unfold SeenUpgrade. intros. destruct (decide (e0 = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H. inversion H. subst eV0. destruct (eV.(type)); try done.
+ rewrite lookup_app_1_ne in H; [|done]. apply HSeenUpgrade in H. done.
- unfold SeenDowngrade. intros. destruct (decide (e0 = length E)) as [->|NEQ].
+ rewrite lookup_app_1_eq in H. inversion H. subst eV0. destruct (eV.(type)); try done.
destruct HeV as [IN|IN]; [by left|]. right. exists e,ainfo'. rewrite lookup_insert. done.
+ rewrite lookup_app_1_ne in H; [|done]. apply HSeenDowngrade in H. destruct (eV0.(type)); try done.
destruct H as [IN|IN]; [by left; set_solver|]. right.
destruct IN as (e' & ainfo'' & He' & IN). destruct (decide (e' = e)) as [->|NEQ'].
* rewrite He in He'. inversion He'. subst ainfo''.
exists e,ainfo'. rewrite lookup_insert. split; [done|]. set_solver.
* exists e',ainfo''. rewrite lookup_insert_ne; [|done]. rewrite lookup_delete_ne; [|done]. done.
- unfold SeenUnlock. intros. apply HSeenUnlock in H. destruct H as [H|H]; [by left|]. right.
destruct H as (e' & ainfo'' & He' & IN). destruct (decide (e' = e)) as [->|NEQ].
+ rewrite He in He'. inversion He'. subst ainfo''.
exists e,ainfo'. rewrite lookup_insert. split; [done|]. set_solver.
+ exists e',ainfo''. rewrite lookup_insert_ne; [|done]. rewrite lookup_delete_ne; [|done]. done.
- unfold ArcsSeen. intros. destruct (decide (e0 = e)) as [->|NEQ].
+ rewrite lookup_insert in H. inversion H. subst ainfo0.
apply LEsarc in He. rewrite Hv. solve_lat.
+ rewrite lookup_insert_ne in H; [|done]. rewrite lookup_delete_ne in H; [|done].
apply LEsarc in H. done.
Qed.
Lemma strong_arc_persist e eidx eV E omo stlist sdom wdom
(OMO_GOOD : Linearizability_omo E omo stlist)
(Heidx : lookup_omo omo eidx = Some e)
(He : E !! e = Some eV)
(HeV : (eV.(type) = StrongInit ∨ (∃ e', eV.(type) = Clone e') ∨ eV.(type) = Upgrade))
(eINdom : e ∈ sdom)
(VALsarcwarc : ArcsValid2 E sdom wdom) :
∀ i st, stlist !! i = Some st → gen_of eidx ≤ i → e ∈ st.1.1.1.
Proof.
eapply omo_stlist_length in OMO_GOOD as EQlenST.
destruct eidx.
{ (* [e] cannot be a read-only event since it should be either [StrongInit], [Clone], or [Upgrade] *)
have [st Hst] : is_Some (stlist !! gen).
{ rewrite lookup_lt_is_Some -EQlenST. apply lookup_omo_lt_Some in Heidx. simpl in Heidx. done. }
eapply omo_read_op_step in OMO_GOOD as STEP; [|exact Heidx|done|done].
exfalso. inversion STEP; rewrite EVENT in HeV; des; try done;
destruct st as [[[? ?] ?] [? ?]]; simpl in *; inversion NST; clear -FRESH H4; set_solver. }
intros i st Hst LEi. generalize dependent st. induction LEi as [|i]; intros.
- rewrite lookup_omo_wr_event in Heidx. destruct gen.
+ eapply omo_write_op_init_step in OMO_GOOD as STEP; [|exact Heidx|done|done].
inversion STEP; rewrite EVENT in HeV; des; try done.
+ have [st' Hst'] : is_Some (stlist !! gen).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hst. simpl in Hst. lia. }
replace (S gen) with (gen + 1) in Hst, Heidx by lia.
eapply omo_write_op_step in OMO_GOOD as STEP; try done.
inversion STEP; rewrite EVENT in HeV; des; try done; subst st; set_solver-.
- have [st' Hst'] : is_Some (stlist !! i).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hst. lia. }
apply IHLEi in Hst' as eIN.
have [e' He'] : is_Some (omo_write_op omo !! (S i)).
{ rewrite lookup_lt_is_Some -omo_write_op_length EQlenST. apply lookup_lt_Some in Hst. done. }
rewrite -lookup_omo_wr_event in He'. eapply lookup_omo_event_valid in He' as HeV'; [|done].
rewrite lookup_omo_wr_event in He'. destruct HeV' as [eV' HeV'].
replace (S i) with (i + 1) in He', Hst by lia.
eapply omo_write_op_step in OMO_GOOD as STEP; try done. inversion STEP; try (subst; set_solver +eIN).
+ apply VALsarcwarc in HeV'. rewrite EVENT in HeV'.
have NEQ' : e ≠ e'0 by set_solver +eINdom HeV'. subst st. set_solver +eIN NEQ'.
+ apply VALsarcwarc in HeV'. rewrite EVENT in HeV'.
have NEQ' : e ≠ e'0 by set_solver +eINdom HeV'. rewrite STRONG in eIN. set_solver +eIN NEQ'.
Qed.
Lemma weak_arc_persist e eidx eV E omo stlist sdom wdom
(OMO_GOOD : Linearizability_omo E omo stlist)
(Heidx : lookup_omo omo eidx = Some e)
(He : E !! e = Some eV)
(HeV : (eV.(type) = StrongInit ∨ eV.(type) = WeakInit ∨ (∃ e', eV.(type) = WeakClone e') ∨ eV.(type) = Downgrade))
(eINdom : e ∈ wdom)
(VALsarcwarc : ArcsValid2 E sdom wdom) :
∀ i st, stlist !! i = Some st → gen_of eidx ≤ i → e ∈ st.2.1.1.
Proof.
eapply omo_stlist_length in OMO_GOOD as EQlenST.
destruct eidx.
{ (* [e] cannot be a read-only event since it should be either [WeakInit], [WeakClone], or [Downgrade] *)
have [st Hst] : is_Some (stlist !! gen).
{ rewrite lookup_lt_is_Some -EQlenST. apply lookup_omo_lt_Some in Heidx. simpl in Heidx. done. }
eapply omo_read_op_step in OMO_GOOD as STEP; [|exact Heidx|done|done].
exfalso. inversion STEP; rewrite EVENT in HeV; des; try done;
destruct st as [? [[? ?] ?]]; simpl in *; inversion NST; set_solver +FRESH H4. }
intros i st Hst LEi. generalize dependent st. induction LEi as [|i]; intros.
- rewrite lookup_omo_wr_event in Heidx. destruct gen.
+ eapply omo_write_op_init_step in OMO_GOOD as STEP; [|exact Heidx|done|done].
inversion STEP; rewrite EVENT in HeV; des; try done.
+ have [st' Hst'] : is_Some (stlist !! gen).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hst. simpl in Hst. lia. }
replace (S gen) with (gen + 1) in Hst, Heidx by lia.
eapply omo_write_op_step in OMO_GOOD as STEP; try done.
inversion STEP; rewrite EVENT in HeV; des; try done; subst st; set_solver-.
- have [st' Hst'] : is_Some (stlist !! i).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hst. lia. }
apply IHLEi in Hst' as eIN.
have [e' He'] : is_Some (omo_write_op omo !! (S i)).
{ rewrite lookup_lt_is_Some -omo_write_op_length EQlenST. apply lookup_lt_Some in Hst. done. }
rewrite -lookup_omo_wr_event in He'. eapply lookup_omo_event_valid in He' as HeV'; [|done].
rewrite lookup_omo_wr_event in He'. destruct HeV' as [eV' HeV'].
replace (S i) with (i + 1) in He', Hst by lia.
eapply omo_write_op_step in OMO_GOOD as STEP; try done. inversion STEP; try (subst; set_solver +eIN).
+ apply VALsarcwarc in HeV'. rewrite EVENT in HeV'.
have NEQ' : e ≠ e'0 by set_solver +eINdom HeV'. subst st. set_solver +eIN NEQ'.
+ apply VALsarcwarc in HeV'. rewrite EVENT in HeV'.
have NEQ' : e ≠ e'0 by set_solver +eINdom HeV'. rewrite WEAK in eIN. set_solver +eIN NEQ'.
Qed.
Lemma weak_state_valid E omo stlist i st
(OMO_GOOD : Linearizability_omo E omo stlist)
(Hst : stlist !! i = Some st) :
∀ e, e ∈ st.2.1.1 → e < length E.
Proof.
apply omo_stlist_length in OMO_GOOD as EQlenST.
generalize dependent st. induction i; intros.
- have [ew Hew] : is_Some (omo_write_op omo !! 0).
{ rewrite lookup_lt_is_Some -omo_write_op_length EQlenST. apply lookup_lt_Some in Hst. done. }
rewrite -lookup_omo_wr_event in Hew.
eapply lookup_omo_event_valid in Hew as HeVw; [|done]. destruct HeVw as [eVw HeVw].
rewrite lookup_omo_wr_event in Hew.
eapply omo_write_op_init_step in OMO_GOOD as STEP; try done. apply lookup_lt_Some in HeVw.
inversion STEP; subst st; simpl in *; try done; (have EQ : e = ew by set_solver); subst e; done.
- have [st' Hst'] : is_Some (stlist !! i).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hst. lia. }
have [ew Hew] : is_Some (omo_write_op omo !! (S i)).
{ rewrite lookup_lt_is_Some -omo_write_op_length EQlenST. apply lookup_lt_Some in Hst. done. }
rewrite -lookup_omo_wr_event in Hew.
eapply lookup_omo_event_valid in Hew as HeVw; [|done]. destruct HeVw as [eVw HeVw].
rewrite lookup_omo_wr_event in Hew. replace (S i) with (i + 1) in Hew,Hst by lia.
eapply omo_write_op_step in OMO_GOOD as STEP; try done. apply lookup_lt_Some in HeVw as LTew.
specialize (IHi _ Hst').
inversion STEP; subst; simpl in *; try (by apply IHi);
try ((have [CASE|CASE] : e ∈ st'.2.1.1 ∨ e = ew by set_solver); [by apply IHi|by subst e]).
+ rewrite elem_of_singleton in H. subst e. done.
+ rewrite elem_of_singleton in H. subst e. done.
Qed.
Lemma OmoSnap_update γg γs γs' q E omo stlist pst nst stlist' eV e gen st eidx' (E' := E ++ [eV]) (omo' := omo_insert_w omo (gen + 1) (length E) []) (stlist'' := take (gen + 1) stlist ++ nst :: stlist') :
e ≠ length E →
gen < length omo →
(∀ i stp stn, stlist !! (gen + 1 + i) = Some stp → stlist' !! i = Some stn → stn.1 = stp.1) →
lookup_omo omo' eidx' = Some e →
interp_omo E' ((length E, []) :: drop (gen + 1) omo) pst (nst :: stlist') →
length omo = length stlist →
OmoAuth γg γs' q E' omo' stlist'' _ -∗
OmoSnap γg γs e st -∗
OmoSnapStates γg γs omo stlist -∗
∃ st', OmoSnap γg γs' e st' ∗ ⌜ st.1 = st'.1 ⌝.
Proof.
iIntros "%NEe %LTgen %Hstlist' %Heidx' %Hgengood %EQlenST M● #e↪st #ST◯".
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
apply interp_omo_length in Hgengood as EQlenST'.
have EQlen1 : length (take (gen + 1) (omo_write_op omo)) = gen + 1.
{ rewrite take_length Nat.min_l; [done|]. rewrite -omo_write_op_length. lia. }
destruct (decide (eidx' = wr_event (gen + 1))) as [->|NEQ].
{ subst omo'. rewrite lookup_omo_wr_event omo_insert_w_write_op lookup_app_r in Heidx'; [|lia].
rewrite EQlen1 in Heidx'. replace (gen + 1 - (gen + 1)) with 0 in Heidx' by lia. by inversion Heidx'. }
eapply lookup_omo_before_insert_w in Heidx' as Heidx; [|done|lia].
destruct Heidx as [eidx [Heidx CASE]].
iDestruct (OmoSnapStates_OmoSnap with "ST◯ e↪st") as %Hst; [done|].
have EQlenSgen1 : length (take (gen + 1) stlist) = gen + 1.
{ rewrite take_length Nat.min_l; [done|]. rewrite -EQlenST. apply lookup_omo_lt_Some in Heidx. lia. }
destruct (le_lt_dec (gen + 1) (gen_of eidx')) as [LE|LT].
- rewrite decide_False in CASE; [|lia].
destruct CASE as (LTSgen & EQgen' & EQeidx).
replace (gen_of eidx) with (gen + 1 + (gen_of eidx - 1 - gen)) in Hst by lia.
have [st' Hst'] : is_Some (stlist' !! (gen_of eidx - 1 - gen)).
{ rewrite lookup_lt_is_Some. inversion EQlenST'.
rewrite drop_length. apply lookup_omo_lt_Some in Heidx. lia. }
specialize (Hstlist' _ _ _ Hst Hst').
iDestruct (OmoSnap_get _ _ _ _ _ _ _ eidx' (gen_of eidx') with "M●") as "#e↪st'"; [|done|done|].
{ rewrite lookup_app_r; [|lia]. rewrite EQlenSgen1 lookup_cons.
replace (gen_of eidx' - (gen + 1)) with (S (gen_of eidx - 1 - gen)) by lia. done. }
iExists st'. iFrame "e↪st'". rewrite Hstlist'. done.
- rewrite decide_True in CASE; [|done]. subst eidx'.
iDestruct (OmoSnap_get _ _ _ _ _ _ _ eidx (gen_of eidx) with "M●") as "#e↪st'"; [|done|done|].
{ rewrite lookup_app_l; [|lia]. rewrite lookup_take_Some. done. }
iExists st. iFrame "e↪st'". done.
Qed.
Lemma weak_arc_insert_gen_good E omo stlist eVop gen st (E' := E ++ [eVop]) (opId := length E) (nst := (st.1, (st.2.1.1 ∪ {[opId]}, st.2.1.2, st.2.2)))
(OMO_GOOD : Linearizability_omo E omo stlist)
(Hst : stlist !! gen = Some st)
(STEP : step opId eVop st nst)
(HInitWrite : omo_write_op omo !! 0 = Some 0)
(HAlive : ArcAlive E) :
∃ stlist', interp_omo E' ((opId, []) :: drop (gen + 1) omo) st (nst :: stlist')
∧ (∀ i stp stn, stlist !! (gen + 1 + i)%nat = Some stp → stlist' !! i = Some stn → stn = (stp.1, (stp.2.1.1 ∪ {[opId]}, stp.2.1.2, stp.2.2))).
Proof.
apply omo_stlist_length in OMO_GOOD as EQlenST.
have H : ∀ len, ∃ stlist', interp_omo E' ((opId, []) :: take len (drop (gen + 1) omo)) st (nst :: stlist')
∧ (∀ i stp stn, stlist !! (gen + 1 + i)%nat = Some stp → stlist' !! i = Some stn → stn = (stp.1, (stp.2.1.1 ∪ {[opId]}, stp.2.1.2, stp.2.2))); last first.
{ specialize (H (length (drop (gen + 1) omo))). rewrite take_ge in H; [|done]. done. }
intros. induction len.
- exists []. split; [|done].
rewrite take_0 -(app_nil_l [(opId, [])]) -(app_nil_l [nst]).
apply (interp_omo_snoc _ _ _ eVop _ _ st). split_and!; try done; [by rewrite lookup_app_1_eq|by apply interp_omo_nil].
- destruct IHlen as (stlist' & GEN_GOOD & Hstlist').
destruct (le_lt_dec (length (drop (gen + 1) omo)) len) as [LE|LT].
{ rewrite take_ge in GEN_GOOD; [|done]. rewrite take_ge; [|lia]. by exists stlist'. }
rewrite -lookup_lt_is_Some in LT. destruct LT as [[e' es'] Hlen].
erewrite take_S_r; [|done].
have [stlen Hstlen] : is_Some (stlist !! ((gen + len) + 1)).
{ rewrite lookup_lt_is_Some -EQlenST. apply lookup_lt_Some in Hlen. rewrite drop_length in Hlen. lia. }
set nstlen := (stlen.1, (stlen.2.1.1 ∪ {[opId]}, stlen.2.1.2, stlen.2.2)).
have [stlen' Hstlen'] : is_Some (stlist !! (gen + len)).
{ rewrite lookup_lt_is_Some. apply lookup_lt_Some in Hstlen. lia. }
set nstlen' : arc_state := (stlen'.1, (stlen'.2.1.1 ∪ {[opId]}, stlen'.2.1.2, stlen'.2.2)).
apply interp_omo_length in GEN_GOOD as EQlenST'. simpl in EQlenST'.
inversion EQlenST'. rename H0 into EQlenST''.
rewrite take_length Nat.min_l in EQlenST''; [|by apply lookup_lt_Some in Hlen; lia].
have Hst' : last (nst :: stlist') = Some nstlen'.
{ destruct len.
- destruct stlist'; [|done]. simpl. rewrite Nat.add_0_r Hst in Hstlen'. inversion Hstlen'. subst stlen'. done.
- have [st' Hst'] : is_Some (stlist' !! len) by rewrite lookup_lt_is_Some; lia.
replace (gen + S len) with (gen + 1 + len) in Hstlen' by lia.
specialize (Hstlist' _ _ _ Hstlen' Hst').
rewrite last_cons last_lookup- EQlenST'' /= Hst' Hstlist'. done. }
have He' : lookup_omo omo (wr_event (gen + 1 + len)) = Some e'.
{ rewrite lookup_drop in Hlen. by rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hlen. }
have [eV' HeV'] : is_Some (E !! e') by eapply lookup_omo_event_valid.
apply lookup_lt_Some in HeV' as LTe'.
exists (stlist' ++ [nstlen]). split.
+ replace ((opId, []) :: take len (drop (gen + 1) omo) ++ [(e', es')]) with
(((opId, []) :: take len (drop (gen + 1) omo)) ++ [(e', es')]); [|by clear; simplify_list_eq].
replace (nst :: stlist' ++ [nstlen]) with ((nst :: stlist') ++ [nstlen]); [|by clear; simplify_list_eq].
eapply interp_omo_snoc. split_and!; try done.
* rewrite lookup_app_l; [done|]. done.
* rewrite lookup_omo_wr_event in He'. replace (gen + 1 + len) with ((gen + len) + 1) in He' by lia.
eapply (omo_write_op_step _ _ _ _ _ _ stlen' stlen) in OMO_GOOD as STEP'; try done. inversion STEP'.
-- subst e'. rewrite -!lookup_omo_wr_event in He',HInitWrite.
specialize (lookup_omo_inj _ _ _ _ _ _ OMO_GOOD He' HInitWrite) as H. inversion H. lia.
-- subst e'. rewrite -!lookup_omo_wr_event in He',HInitWrite.
specialize (lookup_omo_inj _ _ _ _ _ _ OMO_GOOD He' HInitWrite) as H. inversion H. lia.
-- eapply arc_step_Clone; try done. subst. done.
-- eapply arc_step_WeakClone; [done|done|..].
++ subst nstlen'. simpl. set_solver +IDVAL.
++ subst nstlen'. simpl. unfold not. intros. have EQ : e' = opId; [set_solver +FRESH H3|rewrite EQ in LTe'; lia].
++ subst nstlen' nstlen. rewrite NST /=.
replace (stlen'.2.1.1 ∪ {[e']} ∪ {[opId]}) with (stlen'.2.1.1 ∪ {[opId]} ∪ {[e']}); [done|set_solver-].
-- eapply arc_step_Downgrade; [done|done|..].
++ subst nstlen'. simpl. unfold not. intros. done.
++ subst nstlen' nstlen. simpl in *. have NEQ : e' ≠ opId by lia. set_solver +FRESH NEQ.
++ subst nstlen' nstlen. rewrite NST /=.
replace (stlen'.2.1.1 ∪ {[e']} ∪ {[opId]}) with (stlen'.2.1.1 ∪ {[opId]} ∪ {[e']}); [done|set_solver-].
-- eapply arc_step_Upgrade; [done|done|done|done|]. subst nstlen nstlen'. rewrite NST /=. done.
-- subst nstlen' nstlen. rewrite H2 /=. by eapply arc_step_UpgradeFail.
-- eapply arc_step_WeakDrop; [done|done|..].
++ subst nstlen'. set_solver +STRICT.
++ subst nstlen nstlen'. rewrite NST /=. destruct (decide (e'0 = opId)) as [->|NEQ].
** specialize (weak_state_valid _ _ _ _ _ OMO_GOOD Hstlen') as VAL.
have IN : opId ∈ stlen'.2.1.1; [set_solver +STRICT|apply VAL in IN; lia].
** replace (stlen'.2.1.1 ∖ {[e'0]} ∪ {[opId]}) with ((stlen'.2.1.1 ∪ {[opId]}) ∖ {[e'0]}); [done|set_solver +NEQ].
-- rewrite /ArcAlive Forall_lookup in HAlive. apply HAlive in HeV'. by rewrite EVENT in HeV'.
-- eapply arc_step_StrongDrop; try done. subst nstlen' nstlen. rewrite NST /=. done.
-- eapply arc_step_StrongDrop_last; try done. subst nstlen nstlen'. rewrite NST /=. done.
-- subst nstlen' nstlen. rewrite H2 /=. eapply arc_step_UnwrapFail; try done.
-- rewrite /ArcAlive Forall_lookup in HAlive. apply HAlive in HeV'. by rewrite EVENT in HeV'.
* rewrite lookup_drop in Hlen.
eapply omo_gen_info in OMO_GOOD as (?&?&?&?&?&?&?&?& RO); [|exact Hlen].
rewrite Forall_lookup. intros. rewrite Forall_lookup in RO. apply RO in H4.
destruct H4 as (eV'' & HeV'' & STEP' & LT).
replace (gen + len + 1) with (gen + 1 + len) in Hstlen by lia.
rewrite Hstlen in H2. inversion H2. subst x1.
exists eV''. split_and!; try done.
{ rewrite lookup_app_l; [done|]. apply lookup_lt_Some in HeV''. done. }
inversion STEP';
try (destruct stlen as [[[? ?] ?] [[? ?] ?]]; simpl in *; inversion NST; set_solver +FRESH H9);
try (destruct stlen as [[[? ?] ?] [[? ?] ?]]; simpl in *; inversion NST; subst; set_solver +H9).
-- eapply arc_step_UpgradeFail; try done.
-- destruct stlen as [[[? ?] ?] [[? ?] ?]]. simpl in *. inversion NST. set_solver +STRICT H9.
-- destruct stlen as [[[? ?] ?] [[? ?] ?]]. simpl in *. inversion NST. subst. set_solver +STRICT H9.
-- eapply arc_step_UnwrapFail; try done.
-- rewrite /ArcAlive Forall_lookup in HAlive. apply HAlive in HeV''. by rewrite EVENT in HeV''.
+ intros. destruct (decide (i = len)) as [->|NEQ].
* rewrite EQlenST'' lookup_app_1_eq in H0. inversion H0. subst stn.
replace (gen + len + 1) with (gen + 1 + len) in Hstlen by lia.