-
Notifications
You must be signed in to change notification settings - Fork 0
/
proof_elim_graph.v
2467 lines (2230 loc) · 112 KB
/
proof_elim_graph.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 iris.bi Require Import lib.fractional.
From iris.algebra Require Import auth gset gmap agree.
From iris.algebra Require Import lib.mono_list.
From iris.proofmode Require Import tactics.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.logic Require Import logatom invariants.
From gpfsl.logic Require Import readonly_ptsto.
From gpfsl.logic Require Import new_delete.
From gpfsl.logic Require Import proofmode.
From gpfsl.examples.stack Require Import spec_graph code_elimination.
From gpfsl.examples.exchanger Require Import spec_graph_piggyback.
Require Import iris.prelude.options.
(* TODO: move *)
Lemma sum_relation_impl {A B} (RA RA' : relation A) (RB RB': relation B) :
∀ ab1 ab2,
(∀ a1 a2, ab1 = inl a1 → ab2 = inl a2 → RA a1 a2 → RA' a1 a2) →
(∀ b1 b2, ab1 = inr b1 → ab2 = inr b2 → RB b1 b2 → RB' b1 b2) →
sum_relation RA RB ab1 ab2 → sum_relation RA' RB' ab1 ab2.
Proof.
intros ab1 ab2 HA HB SR.
inversion SR as [?? HRA|?? HRB]; subst ab1 ab2; constructor; naive_solver.
Qed.
Lemma sum_relation_iff {A B} (RA RA' : relation A) (RB RB': relation B) :
∀ ab1 ab2,
(∀ a1 a2, ab1 = inl a1 → ab2 = inl a2 → RA a1 a2 ↔ RA' a1 a2) →
(∀ b1 b2, ab1 = inr b1 → ab2 = inr b2 → RB b1 b2 ↔ RB' b1 b2) →
sum_relation RA RB ab1 ab2 ↔ sum_relation RA' RB' ab1 ab2.
Proof. intros ab1 ab2 HA HB; split; apply sum_relation_impl; naive_solver. Qed.
(* END move *)
Implicit Types (γ : gname) (s : loc) (N : namespace) (V : view).
Implicit Type T : list (event_id + event_id).
Definition estkN N := N .@ "estk".
(** Filtering exchange events that are to be simulated. *)
(* "Successful" exchanges only include push-pop exchanges, and
exclude accidental push-push or pop-pop exchanges. *)
Definition is_push_xchg (xe : graph_event xchg_event) : Prop :=
match xe.(ge_event) with
| Exchange v1 v2 => 0 < v1 ∧ v2 = 0
end.
Local Instance is_push_xchg_dec :
∀ xe, Decision (is_push_xchg xe).
Proof. intros [[] ? ?]. solve_decision. Defined.
Definition is_pop_xchg (xe : graph_event xchg_event) : Prop :=
match xe.(ge_event) with
| Exchange v1 v2 => v1 = 0 ∧ 0 < v2
end.
Local Instance is_pop_xchg_dec :
∀ xe, Decision (is_pop_xchg xe).
Proof. intros [[] ? ?]. solve_decision. Defined.
Definition is_successful_xchg (xe : graph_event xchg_event) : Prop :=
match xe.(ge_event) with
| Exchange v1 v2 => 0 < v1 ∧ v2 = 0 ∨ v1 = 0 ∧ 0 < v2
end.
Local Instance is_successful_xchg_dec :
∀ xe, Decision (is_successful_xchg xe).
Proof. intros [[] ? ?]. solve_decision. Defined.
Definition is_xchg_event
(P : graph_event xchg_event → Prop) (Ex : event_list xchg_event) e : Prop :=
∃ eV, Ex !! e = Some eV ∧ P eV.
Definition is_successful_xchg_event := is_xchg_event is_successful_xchg.
Definition is_push_xchg_event := is_xchg_event is_push_xchg.
Definition is_pop_xchg_event := is_xchg_event is_pop_xchg.
(* Translating an exchange event to a stack event *)
Definition xchg_2_stk (xe : xchg_event) : sevent :=
match xe with
| Exchange v1 v2 =>
if bool_decide (0 < v1 ∧ v2 = 0) then Push v1
else if bool_decide (v1 = 0 ∧ 0 < v2) then Pop v2
else (* FALSE case, can never happen *) EmpPop
end.
Lemma is_xchg_event_impl (P Q : _ → Prop) E e :
(∀ e, P e → Q e) → is_xchg_event P E e → is_xchg_event Q E e.
Proof. intros HP (eV & Eqe & HPe). exists eV. split; [done|]. by apply HP. Qed.
Lemma is_xchg_event_iff (P Q : _ → Prop) E e :
(∀ e, P e ↔ Q e) → is_xchg_event P E e ↔ is_xchg_event Q E e.
Proof. intros HP. split; apply is_xchg_event_impl => ?; by apply HP. Qed.
Lemma is_push_succ e : is_push_xchg e → is_successful_xchg e.
Proof. rewrite /is_push_xchg /is_successful_xchg. case_match; naive_solver. Qed.
Lemma is_push_xchg_successful Ex e :
is_push_xchg_event Ex e → is_successful_xchg_event Ex e.
Proof. apply is_xchg_event_impl, is_push_succ. Qed.
Lemma is_pop_succ e : is_pop_xchg e → is_successful_xchg e.
Proof. rewrite /is_pop_xchg /is_successful_xchg. case_match; naive_solver. Qed.
Lemma is_pop_xchg_successful Ex e :
is_pop_xchg_event Ex e → is_successful_xchg_event Ex e.
Proof. apply is_xchg_event_impl, is_pop_succ. Qed.
Lemma is_xchg_event_append_not P Ex eV e :
¬ P eV → is_xchg_event P Ex e ↔ is_xchg_event P (Ex ++ [eV]) e.
Proof.
intros UN. apply exist_proper => eV'. split; intros [Eqe SS]; split; auto.
- by apply lookup_app_l_Some.
- apply lookup_app_1 in Eqe as [?|[? <-]]; done.
Qed.
Lemma is_xchg_event_append P Ex eV e :
is_xchg_event P Ex e ∨ e = length Ex ∧ P eV ↔ is_xchg_event P (Ex ++ [eV]) e.
Proof.
split.
- intros [(eV' & Eqe & SS)| [-> ?]].
+ exists eV'. split; [|done]. by apply lookup_app_l_Some.
+ exists eV. split; [|done]. by apply list_lookup_middle.
- intros (eV' & [Eqe|[-> <-]]%lookup_app_1 & SS).
+ left. by exists eV'.
+ by right.
Qed.
Definition stk_props_inj T : Prop :=
∀ ee1 ee2 e, T !! ee1 = Some e → T !! ee2 = Some e → ee1 = ee2.
Definition stk_props_dom_l (Eb : event_list sevent) T : Prop :=
∀ e, inl e ∈ T ↔ (e < length Eb)%nat.
Definition stk_props_dom_r (Ex : event_list xchg_event) T : Prop :=
∀ e, inr e ∈ T ↔ is_successful_xchg_event Ex e.
(** If T contains an exchange event (inr e1), then it must be matched. *)
Definition xchgs_in_pairs (G : graph sevent) T : Prop :=
∀ ee1 e1, T !! ee1 = Some (inr e1) →
∃ ee2 e2, T !! ee2 = Some (inr e2) ∧ ((ee1,ee2) ∈ G.(so) ∨ (ee2,ee1) ∈ G.(so)).
(** Simulating events *)
Definition stk_props_xchg_map (G : graph sevent) (Gx : graph xchg_event) T : Prop :=
∀ e ee eV eVx,
G.(Es) !! e = Some eV → T !! e = Some (inr ee) → Gx.(Es) !! ee = Some eVx →
eV.(ge_event) = xchg_2_stk eVx.(ge_event) ∧
eV.(ge_view).(dv_in) ⊑ eVx.(ge_view).(dv_in) ∧
(∀ v, eV.(ge_event) = Push v → eV.(ge_view).(dv_comm) ⊑ eVx.(ge_view).(dv_in)) ∧
(∀ v, eV.(ge_event) = Pop v → eVx.(ge_view).(dv_comm) ⊑ eV.(ge_view).(dv_comm))
.
Definition stk_props_stk_map (G Gb : graph sevent) T : Prop :=
∀ e ee eV eVb,
G.(Es) !! e = Some eV → T !! e = Some (inl ee) → Gb.(Es) !! ee = Some eVb →
eVb.(ge_event) = eV.(ge_event) ∧
eV.(ge_view).(dv_in) ⊑ eVb.(ge_view).(dv_in) ∧
(∀ v, eV.(ge_event) = Push v → eV.(ge_view).(dv_comm) ⊑ eVb.(ge_view).(dv_comm)) ∧
(∀ v, eV.(ge_event) = Pop v → eVb.(ge_view).(dv_comm) ⊑ eV.(ge_view).(dv_comm))
.
Definition stk_props_so_sim (G Gb : graph sevent) (Gx : graph xchg_event) T : Prop :=
∀ ee1 ee2 e1 e2, T !! ee1 = Some e1 → T !! ee2 = Some e2 →
(ee1, ee2) ∈ G.(so) ↔
sum_relation (λ eb1 eb2, (eb1, eb2) ∈ Gb.(so))
(λ ex1 ex2, (ex1, ex2) ∈ Gx.(so) ∧
is_push_xchg_event Gx.(Es) ex1 ∧
is_pop_xchg_event Gx.(Es) ex2)
e1 e2.
Definition stk_props_stk_logview (E Eb : event_list sevent) T : Prop :=
∀ ee1 ee2 e1 e2, T !! ee1 = Some (inl e1) → T !! ee2 = Some (inl e2) →
∀ eV22 eV2, E !! ee2 = Some eV22 → Eb !! e2 = Some eV2 →
ee1 ∈ eV22.(ge_lview) → e1 ∈ eV2.(ge_lview).
Record StackProps
{G Gb : graph sevent} {Gx : graph xchg_event} {T : list (event_id + event_id)}
{cons : bool} := mkStackProps {
stk_dom_length : (* T maps G to Gb and Ex *) length T = length G.(Es) ;
stk_event_id_map_inj : (* T is injective *) stk_props_inj T ;
stk_event_id_map_dom_l :
(* Left elements in T simulate the base stack events *)
stk_props_dom_l Gb.(Es) T ;
stk_event_id_map_dom_r :
(* Right elements in T simulate the successful exchange events *)
stk_props_dom_r Gx.(Es) T ;
stk_base_stack_map : (* connecting to base stack *) stk_props_stk_map G Gb T ;
stk_xchg_map : (* connecting to exchanger *) stk_props_xchg_map G Gx T ;
stk_xchg_push_pop :
if cons
(* successful matched PUSH-POP exchange events must be consecutive, with
PUSH before POP. *)
then xchgs_in_pairs G T
else (* if cons = false, we are in the middle of an exchange pair *)
∃ Ex xe, Gx.(Es) = Ex ++ [xe] ∧
if (bool_decide (is_push_xchg xe))
then (* and only if in the middle of a PUSH-POP exchange pair, then
(1) the last of T points to the last of Gx, and
(2) the last of T is unmatched in G
(3) the history before that only has matched exchanges *)
∃ Tr, T = Tr ++ [inr (length Ex)] ∧
(∀ id : event_id, (length Tr, id) ∉ G.(so)) ∧
xchgs_in_pairs G Tr
else (* if they are the other pairs (PUSH-PUSH or POP-POP), then
they are not in T anyway. *)
xchgs_in_pairs G T ;
stk_so_sim : (* simulation of so *) stk_props_so_sim G Gb Gx T ;
stk_xchg_consec :
(* exchange event pairs are adjacent *)
∀ ee1 ee2 e1 e2,
T !! ee1 = Some (inr e1) → T !! ee2 = Some (inr e2) →
(ee1, ee2) ∈ G.(so) → ee2 = S ee1 ;
stk_base_stack_logview :
(* eco between elim stack events implies eco between base-stack events *)
stk_props_stk_logview G.(Es) Gb.(Es) T ;
}.
Arguments StackProps : clear implicits.
(** Local observations of M on G simulate the observations of Mb and Mx *)
(* This also requires that M and Mb are included T.
TODO: this seems useful only for Mb, not Mx. *)
Definition ElimStackLocalEvents T (M Mb : logView) : Prop :=
∀ e, e ∈ M →
∃ eo, T !! e = Some eo ∧
match eo with
| inl e' => e' ∈ Mb
| inr e' =>
(* one always observe the pair of exchange events together *)
(* e' ∈ Mx ∧ ∃ e'', e'' ∈ Mx ∧ (e', e'') ∈ Gx.(so) *)
True
end.
(** Quick helper lemmas *)
Lemma StackProps_empty : StackProps ∅ ∅ ∅ [] true.
Proof.
constructor; try done; intros ?; rewrite elem_of_nil /=; [lia|].
rewrite /is_successful_xchg_event /is_xchg_event lookup_nil. naive_solver.
Qed.
Lemma StackProps_is_Some {G Gb Gx T b} ee :
StackProps G Gb Gx T b → is_Some (T !! ee) ↔ is_Some (G.(Es) !! ee).
Proof. intros SP. by rewrite !lookup_lt_is_Some (stk_dom_length SP). Qed.
Lemma StackProps_is_Some_1 {G Gb Gx T b ee e} :
StackProps G Gb Gx T b → T !! ee = Some e → is_Some (G.(Es) !! ee).
Proof. intros SP ?. apply (StackProps_is_Some ee SP). by eexists. Qed.
Lemma StackProps_is_Some_2 {G Gb Gx T b ee eV} :
StackProps G Gb Gx T b → G.(Es) !! ee = Some eV → is_Some (T !! ee).
Proof. intros SP ?. apply (StackProps_is_Some ee SP). by eexists. Qed.
Lemma StackProps_is_Some_so {G Gb Gx T b ee1 ee2} :
StackProps G Gb Gx T b → (ee1, ee2) ∈ G.(so) →
is_Some (T !! ee1) ∧ is_Some (T !! ee2).
Proof.
intros SP Lt%gcons_so_included.
rewrite /= -(stk_dom_length SP) in Lt. by rewrite <-!lookup_lt_is_Some in Lt.
Qed.
Lemma StackProps_Some_so_l {G Gb Gx T b e1 e2} :
StackProps G Gb Gx T b → (e1, e2) ∈ Gb.(so) →
(∃ ee1, T !! ee1 = Some (inl e1)) ∧ (∃ ee2, T !! ee2 = Some (inl e2)).
Proof.
intros SP [?%(stk_event_id_map_dom_l SP)%elem_of_list_lookup
?%(stk_event_id_map_dom_l SP)%elem_of_list_lookup]%gcons_so_included.
done.
Qed.
Lemma StackProps_is_Some_l {G Gb Gx T b} e :
StackProps G Gb Gx T b → (∃ ee, T !! ee = Some (inl e)) ↔ is_Some (Gb.(Es) !! e).
Proof.
intros SP. by rewrite -elem_of_list_lookup (stk_event_id_map_dom_l SP) lookup_lt_is_Some.
Qed.
Lemma StackProps_is_Some_l_1 {G Gb Gx T b ee e} :
StackProps G Gb Gx T b → T !! ee = Some (inl e) → is_Some (Gb.(Es) !! e).
Proof. intros SP ?. apply (StackProps_is_Some_l e SP). by eexists. Qed.
Lemma StackProps_is_Some_l_1_2 {G Gb Gx T b e} :
StackProps G Gb Gx T b → inl e ∈ T → is_Some (Gb.(Es) !! e).
Proof. by intros SP [? ?%(StackProps_is_Some_l_1 SP)]%elem_of_list_lookup. Qed.
Lemma StackProps_is_Some_l_2 {G Gb Gx T b e eV} :
StackProps G Gb Gx T b → Gb.(Es) !! e = Some eV → ∃ ee, T !! ee = Some (inl e).
Proof. intros SP ?. apply (StackProps_is_Some_l e SP). by eexists. Qed.
Lemma StackProps_is_Some_r {G Gb Gx T b} e :
StackProps G Gb Gx T b →
(∃ ee, T !! ee = Some (inr e)) ↔ is_successful_xchg_event Gx.(Es) e.
Proof. intros SP. by rewrite -elem_of_list_lookup (stk_event_id_map_dom_r SP). Qed.
Lemma StackProps_is_Some_r_1 {G Gb Gx T b ee e} :
StackProps G Gb Gx T b → T !! ee = Some (inr e) →
is_successful_xchg_event Gx.(Es) e.
Proof. intros SP ?. apply (StackProps_is_Some_r e SP). by eexists. Qed.
Lemma StackProps_is_Some_r_1_1 {G Gb Gx T b ee e} :
StackProps G Gb Gx T b → T !! ee = Some (inr e) → is_Some (Gx.(Es) !! e).
Proof. intros SP HT. destruct (StackProps_is_Some_r_1 SP HT) as (?&?&?). by eexists. Qed.
Lemma StackProps_is_Some_r_1_2 {G Gb Gx T b e} :
StackProps G Gb Gx T b → inr e ∈ T → is_Some (Gx.(Es) !! e).
Proof. intros SP (?&?&?)%(stk_event_id_map_dom_r SP). by eexists. Qed.
(** For any pair of successful exchanges, one is push iff the other is pop *)
Lemma is_push_pop_xchg_so Gx x1 x2 :
ExchangerConsistent Gx →
(x1, x2) ∈ Gx.(so) →
is_push_xchg_event Gx.(Es) x1 ↔ is_pop_xchg_event Gx.(Es) x2.
Proof.
intros EC InSo. rewrite (xchg_cons_so_com _ EC) in InSo.
destruct (xchg_cons_matches _ EC _ _ InSo) as
(? & eV1 & eV2 & v1 & v2 & Eq1 & Eq2 & Eqev1 & Eqev2 & _).
rewrite /is_push_xchg_event /is_pop_xchg_event /is_xchg_event Eq1 Eq2
/is_push_xchg /is_pop_xchg.
split; intros (? & <-%Some_inj & IS);
[exists eV2|exists eV1]; move : IS; rewrite Eqev1 Eqev2; naive_solver.
Qed.
Lemma StackProps_inj_insert T e :
let T' := T ++ [e] in e ∉ T → stk_props_inj T → stk_props_inj T'.
Proof.
intros T' FR INJ ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1;
[..|done].
- apply (INJ _ _ _ Eq1 Eq2).
- subst ee. exfalso. apply FR. by apply elem_of_list_lookup_2 in Eq1.
- exfalso. apply FR. by apply elem_of_list_lookup_2 in Eq2.
Qed.
Lemma StackProps_dom_l_insert Eb T eV :
let e' := length Eb in let T' := T ++ [inl e'] in
stk_props_dom_l Eb T → stk_props_dom_l (Eb ++ [eV]) T'.
Proof.
intros e' T' DL. intros e.
rewrite elem_of_app elem_of_list_singleton app_length /= DL.
rewrite Nat.add_1_r Nat.lt_succ_r Nat.lt_eq_cases. naive_solver.
Qed.
Lemma StackProps_dom_l_insert_r Eb T e :
let T' := T ++ [inr e] in stk_props_dom_l Eb T → stk_props_dom_l Eb T'.
Proof.
intros T' DL e'. rewrite elem_of_app elem_of_list_singleton DL. naive_solver.
Qed.
Lemma StackProps_dom_r_insert Ex T eV :
let e' := length Ex in let T' := T ++ [inr e'] in
is_successful_xchg eV →
stk_props_dom_r Ex T → stk_props_dom_r (Ex ++ [eV]) T'.
Proof.
intros e' T' SS DR. intros e.
rewrite elem_of_app elem_of_list_singleton DR /is_successful_xchg_event
-is_xchg_event_append. naive_solver.
Qed.
Lemma StackProps_dom_r_insert_l Ex T e :
let T' := T ++ [inl e] in stk_props_dom_r Ex T → stk_props_dom_r Ex T'.
Proof.
intros T' DR e'. rewrite elem_of_app elem_of_list_singleton DR. naive_solver.
Qed.
Lemma StackProps_stk_logview_insert_r E Eb T e eV :
let E' := E ++ [eV] in let T' := T ++ [inr e] in
length T = length E →
stk_props_stk_logview E Eb T → stk_props_stk_logview E' Eb T'.
Proof.
intros E' T' EqL SL ee1 ee2 e1 e2 [Eqee1|[_ ?]]%lookup_app_1; [|done].
intros [Eqee2|[_ ?]]%lookup_app_1; [|done].
intros eV22 eV2 [EqeV2|[-> <-]]%lookup_app_1.
- apply (SL _ _ _ _ Eqee1 Eqee2 _ _ EqeV2).
- exfalso. clear -EqL Eqee2. apply lookup_lt_Some in Eqee2. lia.
Qed.
Lemma StackProps_stk_logview_insert E Eb T eV eVb :
let E' := E ++ [eV] in let Eb' := Eb ++ [eVb] in
let e' := length E in let eb' := length Eb in let T' := T ++ [inl eb'] in
length T = length E →
(∀ e eV, E !! e = Some eV → set_in_bound eV.(ge_lview) E) →
stk_props_dom_l Eb T →
(∀ ee1 e1, T !! ee1 = Some (inl e1) → ee1 ∈ eV.(ge_lview) → e1 ∈ eVb.(ge_lview)) →
(e' ∈ eV.(ge_lview) → eb' ∈ eVb.(ge_lview)) →
stk_props_stk_logview E Eb T → stk_props_stk_logview E' Eb' T'.
Proof.
intros E' Eb' e' eb' T' EqL EGC DL HEEb HEEb' SL.
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite -EqL lookup_app_1_eq in Eqee2. apply Some_inj, inl_inj in Eqee2 as <-.
rewrite lookup_app_1_eq in EqeV2. apply Some_inj in EqeV2 as <-.
apply lookup_app_1 in Eqee1 as [Eqee1|[-> <-%inl_inj]].
- apply (HEEb _ _ Eqee1 IneV22).
- apply HEEb'. by rewrite /e' -EqL. }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 EqL. intros ->. apply lookup_lt_Some in EqeV22. lia. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (EGC _ _ EqeV22), lookup_lt_is_Some in IneV22. intros ->. lia. }
rewrite lookup_app_1_ne in EqeV2; last first.
{ apply elem_of_list_lookup_2, DL in Eqee2. clear -Eqee2. intros ->. lia. }
by apply (SL _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2).
Qed.
(** Simulating unmatched push of base stack *)
Lemma StackProps_unmatched_push {G Gb Gx T u ub} :
StackProps G Gb Gx T true →
T !! u = Some (inl ub) →
unmatched_push G u ↔ unmatched_push Gb ub.
Proof.
intros SP Equ.
destruct (StackProps_is_Some_1 SP Equ) as [eV EqeV].
destruct (StackProps_is_Some_l_1 SP Equ) as [eVb EqeVb].
rewrite /unmatched_push EqeV EqeVb /=.
destruct (stk_base_stack_map SP _ _ _ _ EqeV Equ EqeVb) as [-> _].
apply and_iff_compat_l. split; intros UM pp InSo.
- destruct (StackProps_Some_so_l SP InSo) as [_ [pp2 Eqpp2]].
(* stk_so_sim ELIM : from base stack to elim stack *)
apply (UM pp2), (stk_so_sim SP _ _ _ _ Equ Eqpp2). by constructor.
- destruct (StackProps_is_Some_so SP InSo) as [_ [ee Eqee]].
(* stk_so_sim ELIM : from elim stack to base stack *)
apply (stk_so_sim SP _ _ _ _ Equ Eqee) in InSo.
inversion InSo as [? pb InSo'|]; clear InSo.
by apply (UM pb), InSo'.
Qed.
(** Going from the simulating elim graph to the simulated base stack,
for unmatched push. *)
Lemma StackProps_unmatched_push_1 {G Gb Gx T u} :
StackProps G Gb Gx T true →
StackConsistent G →
unmatched_push G u →
∃ ub, T !! u = Some (inl ub) ∧ unmatched_push Gb ub.
Proof.
intros SP SC UM. set UM' := UM.
(* from u we get ub, a successful, matched exchange event that u simulates *)
destruct UM' as [[vu (eVu & Eqvu & Equ)%list_lookup_fmap_inv'] UM'].
destruct (StackProps_is_Some_2 SP Equ) as [[ub|ub] Equb].
{ exists ub. split; [done|]. by apply (StackProps_unmatched_push SP Equb). }
(* impossible, any events coming from the exchanger must have been matched. *)
exfalso.
(* we get ub2, the one matched with ub, and u2, the one that simulates ub2. *)
(* stk_xchg_push_pop ELIM *)
destruct (stk_xchg_push_pop SP _ _ Equb) as (u2 & ub2 & _ & [InSo|InSo]).
- by apply (UM' u2).
- rewrite (stk_cons_so_com _ SC) in InSo.
apply (stk_cons_matches _ SC) in InSo as (_ & _ & dV & v & _ & EqdV & _ & Eqp & _).
rewrite Equ in EqdV. apply Some_inj in EqdV as <-. by rewrite Eqp in Eqvu.
Qed.
(** Going from the simulated base stack back to the simulating elim stack,
for unmatched push. *)
Lemma StackProps_unmatched_push_2 {G Gb Gx T ub} :
StackProps G Gb Gx T true →
unmatched_push Gb ub →
∃ u, T !! u = Some (inl ub) ∧ unmatched_push G u.
Proof.
intros SP UM. set UM' := UM.
destruct UM' as
[[_ (_ & _ & [u Equ]%(StackProps_is_Some_l_2 SP))%list_lookup_fmap_inv'] _].
exists u. split; [done|]. by apply (StackProps_unmatched_push SP Equ).
Qed.
Lemma StackProps_xchg_map_xchg_insert G Gx T Gx' eVx :
Gx'.(Es) = Gx.(Es) ++ [eVx] →
inr (length Gx.(Es)) ∉ T →
stk_props_xchg_map G Gx T → stk_props_xchg_map G Gx' T.
Proof.
intros EqGx' FRT XM ???? EqG EqT Eqee. apply (XM _ _ _ _ EqG EqT).
(* new event is not in T *)
rewrite EqGx' in Eqee.
apply lookup_app_1 in Eqee as [?|[-> <-]]; [done|].
exfalso. apply FRT. by apply elem_of_list_lookup_2 in EqT.
Qed.
Lemma StackProps_so_sim_xchg_insert G Gb Gx T Gx' eVx ep :
Gx'.(Es) = Gx.(Es) ++ [eVx] →
let e' := length Gx.(Es) in
(Gx'.(so) = Gx.(so) ∨ Gx'.(so) = {[(e', ep); (ep, e')]} ∪ Gx.(so)) →
inr e' ∉ T →
¬ is_push_xchg eVx → ¬ is_pop_xchg eVx →
stk_props_so_sim G Gb Gx T → stk_props_so_sim G Gb Gx' T.
Proof.
intros EqGx' e' Eqso FRT NPU NPO SO.
intros ???? Eq1 Eq2. rewrite (SO _ _ _ _ Eq1 Eq2).
apply sum_relation_iff; [done|]. rewrite EqGx'.
intros x1 x2 -> ->. destruct Eqso as [->| ->].
(* TODO hard to find lemmas *)
- apply and_iff_compat_l, Morphisms_Prop.and_iff_morphism;
by apply is_xchg_event_append_not.
- apply Morphisms_Prop.and_iff_morphism;
[|apply Morphisms_Prop.and_iff_morphism; by apply is_xchg_event_append_not].
split; [set_solver-|].
rewrite 2!elem_of_union 2!elem_of_singleton. clear -FRT Eq1 Eq2.
intros [[[<- <-]%pair_inj|[<- <-]%pair_inj]|Eq']; [..|done];
exfalso; apply FRT; clear FRT; by eapply elem_of_list_lookup_2.
Qed.
Lemma ElimStackLocalEvents_mono {T T' M Mb Mb'} :
ElimStackLocalEvents T M Mb →
T ⊑ T' → Mb ⊆ Mb' →
ElimStackLocalEvents T' M Mb'.
Proof.
intros EL SubT' Subb' e (eo & Eqeo & CASE)%EL.
exists eo. split; [by eapply prefix_lookup_Some|].
destruct eo as [|eo]; [by apply Subb'|done].
Qed.
Section proof.
Context `{!noprolG Σ}.
Context `{!inG Σ (graphR sevent), !inG Σ (graphR xchg_event)}.
Context `{!ro_ptstoG Σ}.
Context `{!inG Σ (mono_listR (leibnizO (event_id + event_id)))}.
Hypothesis (stk : basic_stack_spec Σ).
Hypothesis (ex : exchanger_piggyback_spec Σ).
Notation vProp := (vProp Σ).
Notation try_push' := (spec_graph.try_push stk).
Notation try_pop' := (spec_graph.try_pop stk).
Local Existing Instances
StackInv_Timeless
StackInv_Objective
StackInv_Fractional
StackInv_AsFractional
StackLocal_Persistent
StackLocalLite_Persistent
StackLocalLite_Timeless
ExchangerInv_Timeless
ExchangerInv_Objective
ExchangerInv_Fractional
ExchangerInv_AsFractional
ExchangerLocal_Persistent
ExchangerLocalLite_Persistent
ExchangerLocalLite_Timeless
.
(** * Ghost assertions *)
Definition ge_list_auth γ q T : vProp :=
⎡ own γ (●ML{#q} (T : listO (leibnizO (event_id + event_id)))) ⎤.
Definition ge_list_lb γ T : vProp :=
⎡ own γ (◯ML (T : listO (leibnizO (event_id + event_id)))) ⎤.
Local Instance ge_list_lb_persistent γ T : Persistent (ge_list_lb γ T) := _.
(* Only share the ghost state with the client. *)
Definition StackSharedInv γg (s : loc) (q : Qp) G b γb γx γ Gb Gx T : vProp :=
⌜ StackConsistent G ⌝ ∗ graph_master γg (q/2) G ∗
StackInv stk γb b (q/2)%Qp Gb ∗
ExchangerInv ex γx (q/2)%Qp Gx ∗
ge_list_auth γ (q/2) T.
Definition StackInv' γg (s : loc) q G : vProp :=
∃ (b : loc) (γsb γsx γb γx γ : gname) Gb Gx T,
StackSharedInv γg s q G b γb γx γ Gb Gx T ∗
meta s nroot (γsb,γsx,γb,γx,γ,b).
Global Instance StackInv'_timeless γg s q G : Timeless (StackInv' γg s q G) := _.
Global Instance StackInv'_objective γg s q G : Objective (StackInv' γg s q G) := _.
(* We only need to transfer these things for push events *)
Definition StackViews γb b (G Gb : graph sevent) T : vProp :=
∀ e eV v, ⌜ G.(Es) !! e = Some eV ∧ eV.(ge_event) = Push v ⌝ →
(* the physical view observed the logical view *)
@{eV.(ge_view).(dv_comm)} (SeenLogview G.(Es) eV.(ge_lview) ∗
∃ Mb, StackLocalLite stk γb b Gb Mb ∗ ⌜ ElimStackLocalEvents T eV.(ge_lview) Mb ⌝) .
Definition ElimStackInv_no_exist
γg (s b x : loc) γsb γsx γb γx γ (cons : bool)
(Vbx : view) (G Gb : graph sevent) (Gx : graph xchg_event) T : vProp :=
@{Vbx} (s ro↦{γsb} #b ∗ (s >> 1) ro↦{γsx} #x) ∗
StackSharedInv γg s 1%Qp G b γb γx γ Gb Gx T ∗
StackViews γb b G Gb T ∗
⌜ StackProps G Gb Gx T cons ∧
if cons then eventgraph_consistent Gx ∧ ExchangerConsistent Gx else True ⌝
.
Definition ElimStackInv γg γsb γsx γb γx γ s b x cons : vProp :=
∃ Vbx G Gb Gx T,
ElimStackInv_no_exist γg s b x γsb γsx γb γx γ cons Vbx G Gb Gx T.
Global Instance ElimStackInv_objective γg γsb γsx γb γx γ s b x cons :
Objective (ElimStackInv γg γsb γsx γb γx γ s b x cons) := _.
Global Instance ElimStackInv_timeless γg γsb γsx γb γx γ s b x cons :
Timeless (ElimStackInv γg γsb γsx γb γx γ s b x cons) := _.
Definition StackLocalLite' : StackLocalT Σ :=
(λ γg s G M,
graph_snap γg G M ∗
∃ (b x : loc) (γsb γsx γb γx γ : gname),
meta s nroot (γsb,γsx,γb,γx,γ,b) ∗
s ro⊒{γsb} #b ∗ (s >> 1) ro⊒{γsx} #x ∗
∃ Gb Mb Gx Mx T,
StackLocalLite stk γb b Gb Mb ∗
ExchangerLocalLite ex γx x Gx Mx ∗
(* observing M means Mb and Mx are at least M *)
⌜ ElimStackLocalEvents T M Mb ⌝ ∗
ge_list_lb γ T
)%I.
Global Instance StackLocalLite'_persistent γg s G M :
Persistent (StackLocalLite' γg s G M) := _.
Global Instance StackLocalLite'_timeless γg s G M :
Timeless (StackLocalLite' γg s G M) := _.
Definition StackLocal' N : StackLocalT Σ :=
(λ γg s G M,
graph_snap γg G M ∗
∃ (b x : loc) (γsb γsx γb γx γ : gname),
meta s nroot (γsb,γsx,γb,γx,γ,b) ∗
s ro⊒{γsb} #b ∗ (s >> 1) ro⊒{γsx} #x ∗
∃ Gb Mb Gx Mx T,
StackLocal stk (estkN N) γb b Gb Mb ∗
ExchangerLocal ex (ElimStackInv γg γsb γsx γb γx γ s b x) N γx x Gx Mx ∗
(* observing M means Mb and Mx are at least M *)
⌜ ElimStackLocalEvents T M Mb ⌝ ∗
ge_list_lb γ T ∗
inv (xchgUN N) (ElimStackInv γg γsb γsx γb γx γ s b x true)
)%I.
(* TODO: := _. diverges *)
Global Instance StackLocal'_persistent N γg s G M :
Persistent (StackLocal' N γg s G M).
Proof. apply bi.sep_persistent; apply _. Qed.
(** * Ghost assertions properties *)
#[global] Instance ge_list_auth_fractional γ T :
Fractional (λ q, ge_list_auth γ q T).
Proof.
intros p q. by rewrite -embed_sep -own_op -mono_list_auth_dfrac_op.
Qed.
#[global] Instance ge_list_auth_asfractional γ q T :
AsFractional (ge_list_auth γ q T) (λ q, ge_list_auth γ q T) q.
Proof. constructor; [done|apply _]. Qed.
Lemma ge_list_auth_lb_get γ q T :
ge_list_auth γ q T -∗ ge_list_lb γ T.
Proof. intros. by apply embed_mono, own_mono, mono_list_included. Qed.
Lemma ge_list_lb_mono γ T T' :
T' ⊑ T → ge_list_lb γ T -∗ ge_list_lb γ T'.
Proof. intros. by apply embed_mono, own_mono, mono_list_lb_mono. Qed.
Lemma ge_list_auth_lb_get_mono γ q T T' :
T' ⊑ T → ge_list_auth γ q T -∗ ge_list_lb γ T'.
Proof. intros. etrans; [apply ge_list_auth_lb_get|by apply ge_list_lb_mono]. Qed.
Lemma ge_list_auth_lb_valid γ q T T' :
ge_list_auth γ q T -∗ ge_list_lb γ T' -∗ ⌜ T' ⊑ T ⌝.
Proof.
iIntros "o1 o2".
by iCombine "o1 o2" gives %[_ ?]%mono_list_both_dfrac_valid_L.
Qed.
Lemma ge_list_auth_agree γ q T q' T' :
ge_list_auth γ q T -∗ ge_list_auth γ q' T' -∗ ⌜ T = T' ⌝.
Proof.
iIntros "o1 o2".
by iCombine "o1 o2" gives %[_ ?]%mono_list_auth_dfrac_op_valid_L.
Qed.
Lemma ge_list_alloc T :
⊢ |==> ∃ γ, ge_list_auth γ 1 T ∗ ge_list_lb γ T.
Proof.
iMod (own_alloc (●ML (T : listO (leibnizO (event_id + event_id))))) as (γ) "oT".
{ apply mono_list_auth_valid. }
iIntros "!>". iExists γ.
iDestruct (ge_list_auth_lb_get with "oT") as "#$". by iFrame "oT".
Qed.
Lemma ge_list_auth_update γ T T' :
T ⊑ T' → ge_list_auth γ 1 T ==∗ ge_list_auth γ 1 T'.
Proof.
intros. rewrite -embed_bupd. by apply embed_mono, own_update, mono_list_update.
Qed.
Lemma ge_list_auth_update' γ T T' :
T ⊑ T' → ge_list_auth γ 1 T ==∗ ge_list_auth γ 1 T' ∗ ge_list_lb γ T'.
Proof.
iIntros (SubT) "oT".
iMod (ge_list_auth_update _ _ _ SubT with "oT") as "oT".
iDestruct (ge_list_auth_lb_get with "oT") as "#$". by iFrame "oT".
Qed.
Lemma ElimStackInv_locs_access γg γsb γsx γb γx γ s b x cons :
ElimStackInv γg γsb γsx γb γx γ s b x cons ⊢
∃ Vbx, @{Vbx} (s ro↦{γsb} #b ∗ (s >> 1) ro↦{γsx} #x) ∗
(∀ Vbx', @{Vbx'} (s ro↦{γsb} #b ∗ (s >> 1) ro↦{γsx} #x) -∗
ElimStackInv γg γsb γsx γb γx γ s b x cons).
Proof.
iDestruct 1 as (Vbx G Gb Gx T) "[F R]".
iExists Vbx. iFrame "F". iIntros (Vbx') "F".
iExists Vbx', _, _, _, _. by iFrame.
Qed.
#[global] Instance StackSharedInv_fractional γg s G b γb γx γ Gb Gx T :
Fractional (λ q, StackSharedInv γg s q G b γb γx γ Gb Gx T).
Proof.
intros p q. rewrite {1}/StackSharedInv.
rewrite Qp.div_add_distr.
rewrite graph_master_fractional ge_list_auth_fractional.
rewrite StackInv_Fractional ExchangerInv_Fractional.
rewrite (bi.persistent_sep_dup (⌜_⌝)%I).
iSplit.
- iIntros "([??] & [??] & [??] & [??] & [??])"; eauto with iFrame.
- iIntros "[(?&?&?&?&?) (?&?&?&?&?)]"; eauto with iFrame.
Qed.
#[global] Instance StackSharedInv_asfractional γg s q G b γb γx γ Gb Gx T :
AsFractional (StackSharedInv γg s q G b γb γx γ Gb Gx T)
(λ q, StackSharedInv γg s q G b γb γx γ Gb Gx T) q.
Proof. constructor; [done|apply _]. Qed.
Lemma StackSharedInv_agree γg s q G b γb γx γ Gb Gx T q' G' Gb' Gx' T' :
StackSharedInv γg s q G b γb γx γ Gb Gx T -∗
StackSharedInv γg s q' G' b γb γx γ Gb' Gx' T' -∗
⌜ G' = G ∧ Gb' = Gb ∧ Gx' = Gx ∧ T' = T ⌝.
Proof.
iIntros "(_ & G1 & S1 & E1 & T1) (_ & G2 & S2 & E2 & T2)".
iDestruct (graph_master_agree with "G2 G1") as %?.
iDestruct (StackInv_agree with "S2 S1") as %?.
iDestruct (ExchangerInv_agree with "E2 E1") as %?.
iDestruct (ge_list_auth_agree with "T1 T2") as %?.
done.
Qed.
#[global] Instance StackInv'_fractional γg s G :
Fractional (λ q, StackInv' γg s q G).
Proof.
intros p q. iSplit.
- iDestruct 1 as (?????????) "[S #MT]".
iDestruct (StackSharedInv_fractional with "S") as "[S1 S2]".
iSplitL "S1"; iExists _,_,_,_,_,_; iExists _,_,_; iFrame "MT ∗".
- iIntros "[S1 S2]".
iDestruct "S1" as (?????????) "[S1 #MT1]".
iDestruct "S2" as (?????????) "[S2 #MT2]".
iDestruct (meta_agree with "MT2 MT1") as %?. simplify_eq.
iDestruct (StackSharedInv_agree with "S2 S1") as %(_ & -> & -> & ->).
iExists _,_,_,_,_,_. iExists _,_,_.
iFrame "MT1". iApply StackSharedInv_fractional. by iFrame.
Qed.
#[global] Instance StackInv'_asfractional γg s q G :
AsFractional (StackInv' γg s q G) (λ q, StackInv' γg s q G) q.
Proof. constructor; [done|apply _]. Qed.
Lemma StackInv'_graph_snap_empty γg s q G :
StackInv' γg s q G -∗ graph_snap γg G ∅.
Proof.
iDestruct 1 as (?????????) "[(?&G&?) ?]". iApply (graph_master_snap with "G").
Qed.
Lemma StackSharedInv_StackInv'_combine
γg s G G' b (γsb γsx γb γx γ : gname) Gb Gx T :
meta s nroot (γsb, γsx, γb, γx, γ, b) -∗
StackSharedInv γg s 1 G b γb γx γ Gb Gx T -∗
StackInv' γg s 1 G' -∗
⌜ G' = G ⌝ ∗ StackSharedInv γg s (1 + 1) G b γb γx γ Gb Gx T.
Proof.
iIntros "MT SI SI'". iDestruct "SI'" as (?????????) "[SI' MT']".
iDestruct (meta_agree with "MT' MT") as "% {MT MT'}". simplify_eq.
iDestruct (StackSharedInv_agree with "SI SI'") as %(-> & -> & -> & ->).
iSplit; [done|]. iCombine "SI SI'" as "SI". iFrame.
Qed.
(** * Verifications of Assertions properties *)
Lemma StackInv'_StackConsistent_instance :
∀ γg s q G, StackInv' γg s q G ⊢ ⌜ StackConsistent G ⌝.
Proof. intros. iDestruct 1 as (?????????) "[($&?) ?]". Qed.
Lemma StackInv'_graph_master_acc_instance :
∀ γg s q G, StackInv' γg s q G ⊢
∃ q', graph_master γg q' G ∗ (graph_master γg q' G -∗ StackInv' γg s q G).
Proof.
intros. iDestruct 1 as (?????????) "[(?&?&?) ?]".
iExists _. iFrame. iIntros "?". eauto 10 with iFrame.
Qed.
Lemma StackInv'_graph_snap_instance :
∀ γg s q G G' M',
StackInv' γg s q G -∗ graph_snap γg G' M' -∗ ⌜ G' ⊑ G ⌝.
Proof.
intros. rewrite StackInv'_graph_master_acc_instance.
iDestruct 1 as (q') "[G _]". iApply (graph_master_snap_included with "G").
Qed.
Lemma StackInv'_agree_instance :
∀ γg s q G q' G',
StackInv' γg s q G -∗ StackInv' γg s q' G' -∗ ⌜ G' = G ⌝.
Proof.
iDestruct 1 as (?????????) "[(?&S1&?) ?]".
iDestruct 1 as (?????????) "[(?&S2&?) ?]".
iApply (graph_master_agree with "S2 S1").
Qed.
Lemma StackLocal'_graph_snap_instance N :
∀ γg s G M, StackLocal' N γg s G M ⊢ graph_snap γg G M.
Proof. by iIntros "* [$ _]". Qed.
Lemma StackLocal'_union_instance :
∀ N γg s q G G1 G2 M1 M2,
StackInv' γg s q G -∗ StackLocal' N γg s G1 M1 -∗ StackLocal' N γg s G2 M2 -∗
StackLocal' N γg s G (M1 ∪ M2).
Proof.
intros.
iDestruct 1 as (b γsb γsx γb γx γ Gb Gx T) "[(%SC & G & S & E & T) MT]".
iIntros "[Gs1 SL1]".
iDestruct "SL1" as (???????) "(MT' & s0 & s1 & SL1)".
iDestruct (meta_agree with "MT' MT") as "{MT'} %". simplify_eq.
iIntros "[Gs2 SL2]".
iDestruct "SL2" as (???????) "(MT' & _ & s1' & SL2)".
iDestruct (meta_agree with "MT' MT") as "{MT'} %". simplify_eq.
iDestruct (ROSeen_agree with "s1 s1'") as %?. simplify_eq.
iDestruct "SL1" as (Gb1 Mb1 Gx1 Mx1 T1) "(SL1 & EL1 & %EL1 & LT1 & II)".
iDestruct "SL2" as (Gb2 Mb2 Gx2 Mx2 T2) "(SL2 & EL2 & %EL2 & LT2 & _)".
iDestruct (ge_list_auth_lb_valid with "T LT1") as %LT1.
iDestruct (ge_list_auth_lb_valid with "T LT2") as %LT2.
iDestruct (graph_snap_upgrade with "G Gs1") as "{Gs1} #Gs1".
iDestruct (graph_snap_upgrade with "G Gs2") as "{Gs2} #Gs2".
iDestruct (graph_snap_union with "Gs1 Gs2") as "$".
iExists b, _, γsb, γsx, γb, γx, γ. iFrame "MT s0 s1".
iExists Gb, (Mb1 ∪ Mb2), Gx, (Mx1 ∪ Mx2), T.
iDestruct (ge_list_auth_lb_get with "T") as "$". iFrame "II".
iDestruct (StackLocal_union with "S SL1 SL2") as "$".
iDestruct (ExchangerLocal_union with "E EL1 EL2") as "$".
iPureIntro.
intros e [InM|InM]%elem_of_union.
- apply (ElimStackLocalEvents_mono EL1 LT1); [set_solver|done].
- apply (ElimStackLocalEvents_mono EL2 LT2); [set_solver|done].
Qed.
Lemma StackLocalLite'_from_instance N :
∀ γg s G M, StackLocal' N γg s G M ⊢ StackLocalLite' γg s G M.
Proof.
iIntros "* [$ SL]".
iDestruct "SL" as (???????) "(MT & s0 & s1 & SL)".
iExists _, _, _, _, _, _, _. iFrame "MT s0 s1".
iDestruct "SL" as (?????) "(SL & EL & F & oT & ?)".
iExists _, _, _, _, _. iFrame "F oT".
iDestruct (StackLocalLite_from with "SL") as "$".
iDestruct (ExchangerLocalLite_from with "EL") as "$".
Qed.
Lemma StackLocalLite'_to_instance N :
∀ γg s G' M' G M,
StackLocalLite' γg s G M -∗ StackLocal' N γg s G' M' -∗
StackLocal' N γg s G M.
Proof.
iIntros "* [$ SL] [_ SL']".
iDestruct "SL" as (???????) "(#MT & #s0 & #s1 & SL)".
iExists _, _, _, _, _, _, _. iFrame "MT s0 s1".
iDestruct "SL" as (?????) "(SL & EL & F & oT)".
iExists _, _, _, _, _. iFrame "F oT".
iDestruct "SL'" as (???????) "(MT' & s0' & s1' & SL')".
iDestruct "SL'" as (?????) "(SL' & EL' & _ & _ & II)".
iDestruct (meta_agree with "MT MT'") as %?. simplify_eq.
iDestruct (ROSeen_agree with "s0 s0'") as %?.
iDestruct (ROSeen_agree with "s1 s1'") as %?. simplify_eq.
iFrame "II".
iDestruct (StackLocalLite_to with "SL SL'") as "$".
iDestruct (ExchangerLocalLite_to with "EL EL'") as "$".
Qed.
Lemma StackLocalLite'_graph_snap_instance :
∀ γg s G M, StackLocalLite' γg s G M ⊢ graph_snap γg G M.
Proof. by iIntros "* [$ _]". Qed.
Lemma StackLocalLite'_upgrade_instance :
∀ γg s q G' G M,
StackInv' γg s q G' -∗ StackLocalLite' γg s G M -∗ StackLocalLite' γg s G' M.
Proof.
intros.
iDestruct 1 as (b γsb γsx γb γx γ Gb Gx T) "[(%SC & G & S & E & T) MT]".
iIntros "[Gs SL]".
iDestruct "SL" as (???????) "(MT' & s0 & s1 & SL)".
iDestruct (meta_agree with "MT' MT") as "{MT'} %". simplify_eq.
iDestruct "SL" as (Gb0 Mb Gx0 Mx T0) "(SL & EL & EL0 & LT)".
iDestruct (graph_snap_upgrade with "G Gs") as "#$".
iExists b, _, γsb, γsx, γb, γx, γ. iFrame "MT s0 s1".
iExists Gb0, Mb, Gx0, Mx, T0. by iFrame.
Qed.
(* TODO: general w.r.t StackLocalLite *)
Lemma StackLocal'_upgrade_instance :
∀ N γg s q G' G M,
StackInv' γg s q G' -∗ StackLocal' N γg s G M -∗ StackLocal' N γg s G' M.
Proof.
iIntros "* SI #SL".
iDestruct (StackLocalLite'_from_instance with "SL") as "-#SLL".
iDestruct (StackLocalLite'_upgrade_instance with "SI SLL") as "SLL".
iApply (StackLocalLite'_to_instance with "SLL SL").
Qed.
(** * Verifications of functions *)
Lemma new_stack_spec :
new_stack_spec' (new_estack stk.(new_stack) ex.(new_exchanger))
StackLocal' StackInv'.
Proof.
iIntros (N tid Φ) "T Post". wp_lam.
(* allocate space for pointers *)
wp_apply wp_new; [done..|].
iIntros (s) "([H†|%] & Hs & Hms & Hme & _)"; [|done].
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
iDestruct "Hs" as "[Hbs Hx]".
wp_let.
(* allocate the base stack *)
wp_op. rewrite shift_0.
wp_apply (new_stack_spec with "T").
iIntros (γb b) "[SLs [Is1 Is2]]".
wp_write.
(* allocate the exchanger *)
wp_op.
wp_apply (new_exchanger_spec with "[//]").
iIntros (γx x) "[[Ix1 Ix2] ELx]".
iApply wp_fupd. wp_write.
have SC0 := StackConsistent_empty.
have SP0 := StackProps_empty.
have EG0 := (@eventgraph_consistent_empty sevent).
iMod (graph_master_alloc_empty (eventT:=sevent)) as (γg) "([GM1 GM2] & Gs)".
iDestruct (graph_snap_empty with "Gs") as "#Gn".
iMod (ROPtsTo_from_na with "Hbs") as (γsb) "Hbs".
iDestruct (ROPtsTo_ROSeen with "Hbs") as "#sbs".
iMod (ROPtsTo_from_na with "Hx") as (γsx) "Hx".
iDestruct (ROPtsTo_ROSeen with "Hx") as "#sx".
iCombine "Hbs Hx" as "Hsx".
iDestruct (view_at_intro with "Hsx") as (Vbx) "[sVbx Hsx]".
iMod (ge_list_alloc []) as (γ) "[[oT1 oT2] #oTs]".
iMod (meta_set _ _ (γsb, γsx, γb, γx, γ, b) nroot with "Hms") as "#Hms"; [done|].
(* allocate the extra invariant for the elimination stack *)
iMod (inv_alloc (xchgUN N) _ (ElimStackInv γg γsb γsx γb γx γ s b x true)
with "[Is1 Ix1 GM1 Hsx oT1]") as "#I".
{ iNext. iExists Vbx, ∅, ∅, ∅, []. iFrame. iSplit; [done|]. iSplit; [|done].
by iIntros (???[]). }
iApply ("Post" $! γg). iSplitL "SLs ELx".
(* StackLocal *)
- iFrame "Gn". iExists b, x, γsb, γsx, γb, γx, γ.
iFrame "Hms sbs sx". iExists ∅, ∅, ∅, ∅, []. iFrame "SLs I oTs".
iMod ("ELx" $! _ _ N) as "$". iIntros "!>".
iPureIntro. by intros ??.
- iIntros "!>". iExists b, γsb, γsx, γb, γx, γ. iExists ∅, ∅, ∅. by iFrame "Hms ∗".
Qed.
Lemma try_push_spec :
try_push_spec' (try_push try_push' ex.(exchange)) StackLocal' StackInv'.
Proof.
iIntros (N DISJ s tid γg G1 M V0 v Posv) "#sV0 #[Gs1 SL]".
iIntros (Φ) "AU".
iDestruct "SL" as (b x γsb γsx γb γx γ) "(MT & sbs & sx & SL)".
iDestruct "SL" as (Gb0 Mb0 Gx0 Mx0 T0) "(SLb0 & ELx0 & %EL0 & LT0 & II)".
set E1 := G1.(Es).
(* store our local observations at an old view *)
iCombine "sbs sx Gs1 SLb0 ELx0" as "THUNK".
iDestruct (view_at_intro_incl with "THUNK sV0")
as (V1) "(sV1 & %LeV0 & sbs' & sx' & Gs1' & SLb0' & ELx0') {THUNK}".
wp_lam. wp_op. rewrite shift_0.
(* read base stack pointer *)
wp_bind (!# _)%E.
iInv "II" as ">I" "Close".
iDestruct (ElimStackInv_locs_access with "I") as (Vbx) "[[Hs Hx] Close2]".
iApply (ROSeen_read_non_atomic with "[$sbs $Hs $sV1]"); [solve_ndisj|].
iIntros "!>" (V2) "([_ %LeV1] & #sV2 & Hs)".
iMod ("Close" with "[Hs Hx Close2]") as "_".
{ iNext. iApply "Close2". by iFrame "Hs Hx". } clear Vbx.
iIntros "!>". wp_let.
(* try push on base stack *)
awp_apply (try_push_spec stk with "sV1 SLb0"); [solve_ndisj|done|].
(* open our internal invariant *)
iInv "II" as (Vbx G Gb Gx T) ">(Locs & SI & R)".
(* then the AU *)
iApply (aacc_aupd with "AU"); [solve_ndisj|].
iIntros (G') ">SI'".
iDestruct (StackSharedInv_StackInv'_combine with "MT SI SI'") as "[-> SI]".
iDestruct "SI" as "(%SC & Gm & BI & E & oT)".
rewrite Qp.div_add_distr Qp.half_half.
iAaccIntro with "BI".
{ (* peeking case *)
iIntros "BI !>".
iDestruct "Gm" as "[G1 G2]". iDestruct "BI" as "[B1 B2]".
iDestruct "E" as "[E1 E2]". iDestruct "oT" as "[T1 T2]".
iSplitL "G1 B1 E1 T1".
{ iNext. iExists _,_,_,_,_,_. iExists _,_,_. by iFrame "MT ∗". }
iIntros "$ !> !>". iExists Vbx, G, Gb, Gx, T. by iFrame. }
(* committing case *)
iIntros (b' V3 Gb' psId ps Vps Mb') "(>BI & #sV3 & #SLb' & %CASE)".
destruct CASE as [(-> & -> & ->)|[-> CASE]].
- (* push fails, try to exchange *)
(* but before that, we need to clean up because we're not committing *)
iLeft. iIntros "!>".
iDestruct "Gm" as "[G1 G2]". iDestruct "BI" as "[B1 B2]".
iDestruct "E" as "[E1 E2]". iDestruct "oT" as "[T1 T2]".
iSplitL "G1 B1 E1 T1".
{ iNext. iExists _,_,_,_,_,_. iExists _,_,_. by iFrame "MT ∗". }
iIntros "AU !>". iSplitR "AU".
{ (* close the invariant *) iNext. iExists _, G, Gb, Gx, T. by iFrame. }
iIntros "_ {SLb'}". clear SC Vbx G Gb Gx psId ps Vps T.
wp_if. wp_op.
(* read the exchanger pointer *)
wp_bind (!# _)%E.
iInv "II" as ">I" "Close".
iDestruct (ElimStackInv_locs_access with "I") as (Vbx) "[[Hs Hx] Close2]".
iApply (ROSeen_read_non_atomic with "[$sx $Hx $sV1]"); [solve_ndisj|].
iIntros "!>" (V4) "([_ %LeV14] & #sV4 & Hx)".
iMod ("Close" with "[Hs Hx Close2]") as "_".
{ iNext. iApply "Close2". by iFrame "Hx Hs". } clear Vbx.
iIntros "!>". wp_let.
wp_apply (exchange_spec ex with "sV1 ELx0 II"); [done|lia|..|iApply "AU"].
iIntros "!>" (b1 b2) "AU I".
iAuIntro.
(* open our internal invariant *)