-
Notifications
You must be signed in to change notification settings - Fork 1
/
crash_borrow.v
1083 lines (1008 loc) · 39.9 KB
/
crash_borrow.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.algebra Require Import gmap auth agree gset coPset excl csum.
From Perennial.program_logic Require Import language staged_invariant.
(* From Perennial.goose_lang Require Import crash_modality lifting wpr_lifting. *)
(* From Perennial.goose_lang Require Import wpc_proofmode. *)
From iris.proofmode Require Import tactics.
From Perennial.base_logic.lib Require Import saved_prop frac_coPset.
From Perennial.Helpers Require Import Qextra.
(* From Perennial.program_logic Require Import language. *)
From self.lang Require Import lang.
From self.base Require Import post_crash_modality primitive_laws wpr_lifting.
From self.base Require Import cred_frag.
From self.base Require Import primitive_laws.
From Perennial.program_logic Require Import language.
Section frac_coPset_prop.
Context {Σ : gFunctors}.
Context {Hin: inG Σ (frac_coPsetR)}.
Lemma ownfCP_inf_le1 γ (q : Qp) (E : coPset) :
ownfCP_inf γ q E -∗ ⌜ q ≤ 1 ⌝%Qp.
Proof.
iDestruct 1 as "(%Hinf&Hown)".
iDestruct (own_valid with "Hown") as %Hval.
iPureIntro.
destruct Hval as (Hval&Hdom).
specialize (Hval (coPpick E)).
rewrite /= decide_True in Hval => //=.
apply coPpick_elem_of.
intros ?. apply set_not_infinite_finite in Hinf; eauto.
Qed.
Lemma ownfCP_disj1 γ q1 D E :
ownfCP γ q1 D ∗ ownfCP_inf γ 1 E -∗ ⌜ E ## D ⌝.
Proof.
iIntros. iDestruct (ownfCP_disj with "[$]") as %Hcases. iPureIntro.
destruct Hcases as [Hdisj|Hbad]; auto. exfalso.
move: Hbad. rewrite frac_valid Qp.le_ngt => Hnlt. apply Hnlt.
apply Qp.lt_add_r.
Qed.
Lemma ownfCP_disj_gt2 γ q D E :
(/2 < q)%Qp →
ownfCP γ q D ∗ ownfCP_inf γ q E -∗ ⌜ E ## D ⌝.
Proof.
iIntros. iDestruct (ownfCP_disj with "[$]") as %Hcases. iPureIntro.
destruct Hcases as [Hdisj|Hbad]; auto. exfalso.
move: Hbad. rewrite frac_valid Qp.le_ngt => Hnlt. apply Hnlt.
rewrite -Qp.inv_half_half.
apply Qp.add_lt_mono; auto.
Qed.
End frac_coPset_prop.
Section crash_borrow_def.
(* Context `{ext:ffi_syntax}. *)
(* Context `{ffi_sem: ffi_semantics}. *)
(* Context `{!ffi_interp ffi}. *)
(* Context `{!heapGS Σ}. *)
Context `{!stagedG Σ}.
Context `{nvmBaseFixedG Σ, !extraStateInterp Σ, nvmBaseDeltaG}.
Global Instance later_tokG_heap : later_tokG (nvmBase_irisGS).
Proof.
refine {| later_tok := cred_frag 1 |};
rewrite /step_count_next.
- iIntros (g ns mj D κ) "(Hg&Hfrag)".
iDestruct "Hg" as "(Hffi&Hinv&Hcred&Htok)".
iMod (cred_interp_decr with "[$]") as (ns' ->) "(Hauth&Hfrag)".
iExists ns'. iModIntro; iSplit; first done.
iFrame. iDestruct "Hauth" as "($&_)".
- iIntros (g ns mj D κ) "Hg".
iDestruct "Hg" as "(Hffi&(Hcred&H0)& h & tok)".
iMod (cred_interp_incr with "[$]") as "(Hauth&Hfrag)".
iFrame. eauto.
- intros n1 n2 Hlt => /=.
transitivity (3 ^ (1 + (n1 + 1)))%nat; last first.
{ apply Nat.pow_le_mono_r; lia. }
rewrite [a in _ _ a]Nat.pow_add_r.
rewrite [a in _ _ a]/=.
transitivity (2 + 3^(n1 + 1) + 3^(n1 + 1))%nat; first by lia.
rewrite Nat.add_0_r -Nat.add_assoc.
apply Nat.add_le_mono_r.
clear.
transitivity (2 ^ 1)%nat; first by auto.
etransitivity; last eapply (Nat.pow_le_mono_r _ 1); try (simpl; lia).
- intros n1 n2 Hlt => /=. lia.
- intros n1 n2 Hlt => /=. lia.
- intros n1 => /=. lia.
Defined.
Global Instance pri_invG_heap : pri_invG (nvmBase_irisGS).
Proof.
refine {| pri_inv_tok := λ q E, pinv_tok_inf q E |}; rewrite /pinv_tok_inf.
- iIntros (??) "($&?)".
- iIntros (???) "H". by rewrite ownfCP_inf_op_plus.
- iIntros (???). rewrite ownfCP_inf_op_plus. by iIntros "$ $".
- iIntros (q E) "H". by iApply (ownfCP_inf_le1).
- intros (**). iIntros "(? & ? & ? & ?)". eauto.
- iIntros (??????) "%Hlt Hg". iDestruct "Hg" as "(?&?&%Hle2&Hp)".
iDestruct (ownfCP_op_plus with "Hp") as "(Hp1&$)".
iFrame. iSplit.
{ iPureIntro. split; auto. transitivity (q1 + q2)%Qp; last by naive_solver.
apply Qp.le_add_r. }
iIntros (???) "Hg". iDestruct "Hg" as "(?&?&%Hle2'&Hp)".
iFrame. iSplit; first auto.
iApply ownfCP_op_plus. iFrame.
- iIntros (?????) "%Hlt (Hg&Hp')". iDestruct "Hg" as "(?&?&%Hle2&Hp)".
iFrame. iDestruct "Hp'" as "(%Hinf&Hp')".
iDestruct (ownfCP_op_plus with "[$Hp' $Hp]") as "Hp".
iDestruct (ownfCP_inf_le1 with "[$Hp //]") as %Hle3.
iFrame. iPureIntro.
split; auto. transitivity q2; first naive_solver.
apply Qp.lt_add_r.
- iIntros (g ns q D κ) "Hg".
iMod (ownfCP_inf_init (coPset_name credit_cr_names)) as (E) "H".
iDestruct "Hg" as "($&$&$&Hp)".
iDestruct "H" as "(%Hinf&H)".
iExists E.
iDestruct (ownfCP_disj1 with "[$Hp H]") as %Hdisj.
{ iFrame; eauto. }
iFrame. eauto.
- iIntros (E g ns q D κ) "(Hp&Hg)".
iDestruct "Hg" as "($&$&%Hle&Hp')".
iFrame "%".
iDestruct (ownfCP_disj_gt2 with "[$Hp $Hp']") as %Hdisj; first naive_solver.
iDestruct "Hp" as "(Hinf&Hp)".
iModIntro. iApply ownfCP_op_union; auto.
iFrame.
- iIntros (E g ns q D κ) "((%Hdisj&%Hinf)&Hg)".
iDestruct "Hg" as "($&$&$&Hp)".
iDestruct (ownfCP_op_union with "Hp") as "($&$)"; auto.
- iIntros (g ns q1 q2 D κ E) "(Hg&Hp')".
iDestruct "Hg" as "(?&?&%Hle&Hp)".
iApply (ownfCP_disj with "[$]").
Qed.
Definition pre_borrow : iProp Σ :=
(later_tok ∗ later_tok ∗ later_tok ∗ later_tok).
Definition pre_borrowN (n: nat) := Nat.iter n (λ P, pre_borrow ∗ P)%I True%I.
Global Instance pre_borrowN_timeless n :
Timeless (pre_borrowN n).
Proof. induction n; apply _. Qed.
Lemma cred_frag_to_pre_borrowN n :
cred_frag (n * 4) -∗ pre_borrowN n.
Proof.
induction n.
- rewrite //=. eauto.
- replace (S n * 4) with (4 + (n * 4)) by auto.
iIntros "H". iDestruct (cred_frag_split with "H") as "(H&IH)".
iDestruct (IHn with "IH") as "IH". simpl. iFrame.
replace 4 with (1 + 1 + 1 + 1) by auto.
repeat (iDestruct (cred_frag_split with "H") as "(H&?)").
rewrite /pre_borrow.
rewrite /later_tok.
simpl.
iFrame.
Qed.
Lemma pre_borrowN_split n1 n2 :
pre_borrowN (n1 + n2) -∗ pre_borrowN n1 ∗ pre_borrowN n2.
Proof.
rewrite /pre_borrowN Nat.iter_add.
induction n1 => //=.
- iIntros "$".
- iIntros "($&H)". by iApply IHn1.
Qed.
Lemma pre_borrowN_to_cred_frag n :
pre_borrowN (S n) -∗ cred_frag ((S n) * 4).
Proof.
induction n.
- rewrite //=.
replace 4 with (1 + 1 + 1 + 1) by auto.
iIntros "((?&?&?&?)&_)".
repeat (iApply cred_frag_join; iFrame).
- iIntros "H". iDestruct (pre_borrowN_split 1 with "H") as "(H&Hrest)".
iDestruct (IHn with "Hrest") as "IH".
replace (S (S n) * 4) with (4 + (S n * 4)) by lia.
iApply cred_frag_join; iFrame.
replace 4 with (1 + 1 + 1 + 1) by auto.
iDestruct "H" as "((?&?&?&?)&_)".
repeat (iApply cred_frag_join; iFrame).
Qed.
Lemma pre_borrowN_global_interp_le n1 g n2 mj E κs :
pre_borrowN n1 -∗ global_state_interp g n2 mj E κs -∗
⌜ 4 * n1 <= n2 ⌝.
Proof.
destruct n1; first by (iIntros; iPureIntro; lia).
iIntros "Hpre Hg".
iDestruct "Hg" as "(?&?&?&?)".
iDestruct (pre_borrowN_to_cred_frag with "Hpre") as "Hcred_frag".
iDestruct (cred_interp_invert with "[$]") as (?) "%Heq". subst.
iPureIntro; lia.
Qed.
Lemma pre_borrowN_big_sepM `{Countable K} {A} n (m : gmap K A) :
size m = n →
pre_borrowN n -∗ [∗ map] _ ↦ _ ∈ m, pre_borrow.
Proof.
iInduction m as [| x m] "IH" using map_ind forall (n).
- iIntros (_) "_". rewrite //=.
- iIntros (Hsize) "H".
rewrite big_sepM_insert //.
rewrite map_size_insert_None // in Hsize.
inversion Hsize; subst.
iDestruct (pre_borrowN_split 1 with "H") as "(($&_)&H)".
iApply "IH"; eauto.
Qed.
Definition crash_borrow Ps Pc : iProp Σ :=
(∃ Ps' Pc', □ (Ps -∗ Pc) ∗
▷ (Ps' -∗ Ps) ∗
▷ □ (Pc -∗ Pc') ∗
staged_value_idle ⊤ Ps' True%I Pc' ∗ later_tok ∗ later_tok).
Global Instance crash_borrow_proper Rc :
Proper ((⊣⊢) ==> (⊣⊢)) (λ R, crash_borrow R Rc).
Proof. intros ?? eq. rewrite /crash_borrow. setoid_rewrite eq. done. Qed.
Lemma crash_borrow_init_cancel P Pc :
pre_borrow -∗ P -∗ □ (P -∗ Pc) -∗ init_cancel (crash_borrow P Pc) Pc.
Proof.
iIntros "H HP #Hwand".
iDestruct "H" as "(Hlt1&H)".
iDestruct "H" as "(Hlt2&Hlt3)".
iDestruct (staged_value_init_cancel P Pc with "[$]") as "H".
iApply (init_cancel_wand with "H [-] []").
{ iIntros "H". iExists _, _. iFrame "# ∗". iSplitL; eauto. }
eauto.
Qed.
Lemma big_sepM_crash_borrow_init_cancel `{Countable A} {B} (P: A → B → iProp Σ) Q m:
([∗ map] _ ↦ _ ∈ m, pre_borrow) -∗
([∗ map] a ↦ obj ∈ m, Q a obj) -∗
([∗ map] a ↦ obj ∈ m, □ (Q a obj -∗ P a obj)) -∗
init_cancel ([∗ map] a ↦ obj ∈ m, crash_borrow (Q a obj) (P a obj)) ([∗ map] a ↦ obj ∈ m, P a obj).
Proof.
iIntros "Hpres HQs #Hstatuses".
iInduction m as [|i x m] "IH" using map_ind.
{ iApply init_cancel_intro; rewrite !big_sepM_empty; eauto. }
iDestruct (big_sepM_insert with "Hpres") as "[Hpre Hpres]";
first by assumption.
iDestruct (big_sepM_insert with "HQs") as "[HQ HQs]";
first by assumption.
iDestruct (big_sepM_insert with "Hstatuses") as "[Hstatus Hstatuses']";
first by assumption.
iDestruct ("IH" with "Hstatuses' Hpres HQs") as "Hcancel".
iDestruct (crash_borrow_init_cancel with "Hpre HQ Hstatus")
as "Hcrash".
iDestruct (init_cancel_sep with "Hcrash Hcancel") as "Hcancel".
iApply (init_cancel_wand with "Hcancel"); iIntros "H"; iApply big_sepM_insert; eauto.
Qed.
Lemma wpc_crash_borrow_inits s e Φ Φc P Pc :
pre_borrow -∗
P -∗
□ (P -∗ Pc) -∗
(crash_borrow P Pc -∗ WPC e @ s; ⊤ {{ Φ }} {{ Pc -∗ Φc }}) -∗
WPC e @ s; ⊤ {{ Φ }} {{ Φc }}.
Proof.
iIntros "H HP #Hwand Hwpc".
iDestruct (crash_borrow_init_cancel with "[$] HP [$]") as "Hcb".
iApply (init_cancel_elim with "[$]"). eauto.
Qed.
Lemma wpc_borrow_inv s E e Φ Φc :
(crash_borrow_ginv -∗ WPC e @ s; E {{ Φ }} {{ Φc }}) -∗
WPC e @ s; E {{ Φ }} {{ Φc }}.
Proof.
iIntros "H".
rewrite wpc_unfold.
iIntros (mj). rewrite /wpc_pre.
iSplit; last first.
{ iIntros (????) "Hg HC".
iAssert (crash_borrow_ginv) with "[Hg]" as "#Hinv".
{ iDestruct "Hg" as "(#Hinv&_)". eauto. }
iDestruct ("H" with "[$]") as "H".
iDestruct ("H" $! _) as "(_&H)".
iApply ("H" with "[$]"); eauto. }
destruct (to_val _).
- iIntros (?????) "Hg HNC".
iAssert (crash_borrow_ginv) with "[Hg]" as "#Hinv".
{ iDestruct "Hg" as "(#Hinv&_)". eauto. }
iDestruct ("H" with "[$]") as "H".
iDestruct ("H" $! _) as "(H&_)".
iApply ("H" with "[$]"); eauto.
- iIntros (????????) "Hσ Hg HNC".
iAssert (crash_borrow_ginv) with "[Hg]" as "#Hinv".
{ iDestruct "Hg" as "(#Hinv&_)". eauto. }
iDestruct ("H" with "[$]") as "H".
iDestruct ("H" $! _) as "(H&_)".
iApply ("H" with "[$] [$]"); eauto.
Qed.
(* Lemma wpc_crash_borrow_generate_pre s k (e : thread_state) Φ Φc : *)
(* language.to_val *)
(* language.language *)
Lemma wpc_crash_borrow_generate_pre s e Φ Φc :
to_val e = None →
WPC e @ s; (⊤ ∖ (↑borrowN : coPset))
{{ v, pre_borrow -∗ Φ v }} {{ Φc }} -∗
WPC e @ s; ⊤ {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnv) "Hwpc".
iApply wpc_borrow_inv.
iIntros "#Hinv". rewrite wpc_eq. iIntros (mj).
iSpecialize ("Hwpc" $! mj).
rewrite ?wpc0_unfold.
iSplit; last first.
{ iIntros. iDestruct "Hwpc" as "(_&H)".
iSpecialize ("H" with "[$] [$] [$]").
iApply (step_fupd2N_inner_wand with "H"); auto. }
rewrite Hnv.
iIntros (q σ g1 ns D κ κs nt) "Hσ Hg HNC cred".
iInv "Hinv" as ">H" "Hclo".
rewrite /crash_borrow_ginv_number.
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt1&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt2&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt3&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt4&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt5&H)".
iDestruct ("Hwpc") as "(Hwpc&_)".
rewrite Hnv.
iMod (later_tok_decr with "[$]") as (ns' Heq) "Hg".
iMod ("Hwpc" with "[$] [$] [$] [cred]") as "Hwpc".
{ iApply lc_weaken; last done.
assert (Hlt: ns' < ns) by lia.
apply num_laters_per_step_lt in Hlt. lia. }
iModIntro.
iApply (step_fupd_extra.step_fupd2N_le (S (num_laters_per_step ns')) (num_laters_per_step ns) with "[-]").
{ assert (Hlt: ns' < ns) by lia.
apply num_laters_per_step_lt in Hlt. lia.
}
iApply (step_fupd2N_wand with "Hwpc").
iIntros "($&H)".
iIntros. iMod ("H" with "[//]") as "(Hσ&Hg&Hwp&$)".
iFrame.
iMod (later_tok_incrN 10 with "[$]") as "(Hg&Htoks)".
iMod (global_state_interp_le _ ((step_count_next ns)) _ _ with "Hg") as "Hg".
{ by apply step_count_next_add. }
iFrame.
iMod ("Hclo" with "[Htoks]").
{ iNext.
repeat (iDestruct "Htoks" as "(?&Htoks)").
repeat (rewrite -(cred_frag_join (S 0)); iFrame). }
iModIntro.
iApply (wpc0_strong_mono with "Hwp"); auto.
{ destruct (to_val e2); eauto. }
iSplit; last eauto.
iIntros (?) "H". iModIntro.
iApply "H". iFrame.
Qed.
(*
Lemma wp_crash_borrow_generate_pre s e Φ :
language.to_val e = None →
WP e @ s; (⊤ ∖ (↑borrowN : coPset))
{{ v, pre_borrow -∗ Φ v }} -∗
WP e @ s; ⊤ {{ Φ }}.
Proof.
iIntros (?) "H".
iApply (wpc_wp _ 0 _ _ _ True%I).
iApply wpc_crash_borrow_generate_pre; auto.
iApply (wp_wpc). iApply "H".
Qed.
*)
Lemma wpc_crash_borrow_init_ctx'' s e Φ Φc P Pc K `{!LanguageCtx K} :
to_val e = None →
P -∗
□ (P -∗ Pc) -∗
(∀ mj, wpc_crash_modality ⊤ mj Φc) ∧ (crash_borrow P Pc -∗
WPC e @ s; (⊤ ∖ (↑borrowN : coPset))
{{ λ v, WPC K (of_val v) @ s; ⊤ {{ Φ }} {{ Φc }} }}
{{ Φc }}) -∗
WPC K e @ s; ⊤ {{ Φ }} {{ Φc ∗ Pc }}.
Proof.
iIntros (Hnv) "HP #Hwand Hwpc".
iApply wpc_borrow_inv.
iIntros "#Hinv". rewrite wpc_eq. iIntros (mj).
iApply wpc0_bind.
rewrite Hnv.
rewrite wpc0_unfold.
iSplit; last first.
{ iIntros. iDestruct "Hwpc" as "(H&_)".
iSpecialize ("H" $! mj).
rewrite /wpc_crash_modality.
iSpecialize ("H" with "[$] [$] [$]").
iApply (step_fupd2N_inner_wand with "H"); auto.
iIntros "($&$)". iApply "Hwand". iFrame.
}
rewrite Hnv.
iIntros (q σ g1 ns D κ κs nt) "Hσ Hg HNC Hlc".
iInv "Hinv" as ">H" "Hclo".
rewrite /crash_borrow_ginv_number.
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt1&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt2&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt3&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt4&H)".
iDestruct (cred_frag_split 1 _ with "H") as "(Hlt5&_)".
iDestruct "Hwpc" as "(_&Hwpc)".
iMod (pri_inv_tok_alloc with "[$]") as (Einv Hdisj) "(Hitok&Hg)".
iDestruct (pri_inv_tok_global_valid with "[$]") as %(Hgt&Hle).
(* Create the invariant *)
iMod (saved_prop_alloc P) as (γprop) "#Hsaved".
{ apply dfrac_valid_discarded. }
iMod (saved_prop_alloc True%I) as (γprop') "#Hsaved'".
{ apply dfrac_valid_discarded. }
iMod (own_alloc (● (Excl' (γprop, γprop')) ⋅ ◯ (Excl' (γprop, γprop')))) as (γ) "[H1 H2]".
{ apply auth_both_valid_2; [econstructor | reflexivity]. }
iMod (pending_alloc) as (γ') "Hpending".
iMod (own_alloc (● (Excl' idle) ⋅ ◯ (Excl' idle))) as (γstatus) "[Hstat1 Hstat2]".
{ apply auth_both_valid_2; [econstructor | reflexivity]. }
iDestruct (pri_inv_tok_infinite with "Hitok") as %Hinf.
destruct (Qp_plus_inv_2_gt_1_split mj) as (mj_ikeep&mj_ishare&Heq_mj&Hinvalid); first auto.
iEval (rewrite -Qp.inv_half_half) in "Hitok".
iDestruct (pri_inv_tok_split with "Hitok") as "(Hitok_u&Hitok_i)".
iEval (rewrite -Heq_mj) in "Hitok_i".
iDestruct (pri_inv_tok_split with "Hitok_i") as "(Hitok_ikeep&Hitok_ishare)".
iMod (pri_inv_alloc Einv _ _ (staged_inv_inner ⊤ Einv mj mj_ishare γ γ' γstatus Pc) with "[HP H1 Hitok_ishare Hstat1]") as
"#Hpri_inv"; auto.
{ iNext. rewrite staged_inv_inner_unfold. iExists _, _, idle, P, True%I. iFrame "∗ #".
iLeft. iSplit; first iFrame. iIntros "HC". iDestruct ("Hwand" with "[$]") as "$"; eauto.
}
iAssert (crash_borrow P Pc)%I with "[Hlt1 Hlt2 Hlt5 H2 Hstat2 Hitok_u]" as "Hborrow".
{
iFrame "# ∗". iExists P, Pc.
iSplitR; first eauto.
iSplitR; first eauto.
iExists _, _, _, _, _, _. iFrame "∗". iFrame "Hsaved Hsaved'".
iExists _, _. iFrame "Hpri_inv". eauto.
}
iAssert (staged_inv_cancel ⊤ mj Pc)%I with "[Hitok_ikeep Hpending Hlt3]" as "Hcancel".
{
iExists _, _, _, _, _, _, _. iFrame "%". iFrame. eauto.
}
iSpecialize ("Hwpc" with "[$]").
iSpecialize ("Hwpc" $! mj).
rewrite wpc0_unfold.
iDestruct ("Hwpc") as "(Hwpc&_)".
rewrite Hnv.
iMod (later_tok_decr with "[$]") as (ns' Heq) "Hg".
iMod ("Hwpc" with "[$] [$] [$] [Hlc]") as "Hwpc".
{ iApply (lc_weaken with "Hlc").
apply num_laters_per_step_lt in Heq. lia. }
iModIntro.
iApply (step_fupd_extra.step_fupd2N_le (S (num_laters_per_step ns')) (num_laters_per_step ns) with "[-]").
{ assert (Hlt: ns' < ns) by lia.
apply num_laters_per_step_lt in Hlt. lia.
}
iApply (step_fupd2N_wand with "Hwpc").
iIntros "($&H)".
iIntros. iMod ("H" with "[//]") as "(Hσ&Hg&Hwp&$)".
iFrame.
iMod (later_tok_incrN 10 with "[$]") as "(Hg&Htoks)".
iMod (global_state_interp_le _ ((step_count_next ns)) _ _ with "Hg") as "Hg".
{ by apply step_count_next_add. }
iFrame.
iMod ("Hclo" with "[Htoks]").
{ iNext.
repeat (iDestruct "Htoks" as "(?&Htoks)").
repeat (rewrite -(cred_frag_join (S 0)); iFrame). }
iModIntro.
iApply (wpc0_staged_inv_cancel with "[$]").
{ destruct (to_val e2); eauto. }
{ auto. }
iApply (wpc0_strong_mono with "Hwp"); auto.
{ destruct (to_val e2); eauto. }
iSplit; last first.
{ iIntros "H !>"; eauto. }
iIntros (v) "Hwpc". iModIntro. iIntros "Hcancel".
iApply (wpc0_staged_inv_cancel with "[$]").
{ destruct (to_val (K _)); eauto. }
{ auto. }
iApply (wpc0_strong_mono with "Hwpc"); auto.
{ destruct (to_val (K _)); auto. }
Qed.
Lemma wpc_crash_borrow_init_ctx' s e Φ Φc P Pc K `{!LanguageCtx K} :
to_val e = None →
P -∗
□ (P -∗ Pc) -∗
Φc ∧ (crash_borrow P Pc -∗
WPC e @ s; (⊤ ∖ (↑borrowN : coPset))
{{ λ v, WPC K (of_val v) @ s; ⊤ {{ Φ }} {{ Φc }} }}
{{ Φc }}) -∗
WPC K e @ s; ⊤ {{ Φ }} {{ Φc ∗ Pc }}.
Proof.
iIntros (Hnv) "HP HPC Hwpc".
iApply (wpc_crash_borrow_init_ctx'' with "HP HPC"); auto.
iSplit.
- iIntros. iApply wpc_crash_modality_intro.
iDestruct "Hwpc" as "[Hwpc _]". eauto.
- iDestruct "Hwpc" as "[_ Hwpc]". eauto.
Qed.
(*
Lemma wpc_crash_borrow_init_ctx s k e Φ Φc P Pc K `{!LanguageCtx K} :
language.to_val e = None →
P -∗
□ (P -∗ Pc) -∗
(Pc -∗ Φc) ∧ (crash_borrow P Pc -∗
WPC e @ s; k; (⊤ ∖ (↑borrowN : coPset))
{{ λ v, WPC K (of_val v) @ s; k ; ⊤ {{ Φ }} {{ Pc -∗ Φc }} }}
{{ Pc -∗ Φc }}) -∗
WPC K e @ s; k; ⊤ {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnv) "HP HPC Hwpc".
iPoseProof (wpc_crash_borrow_init_ctx'' _ _ e Φ (Pc -∗ Φc) with "HP HPC [Hwpc]") as "H"; auto.
{ iSplit.
- iIntros. iApply wpc_crash_modality_intro. iLeft in "Hwpc". eauto.
- iRight in "Hwpc". eauto. }
iApply (wpc_mono with "H"); auto.
iIntros "(H1&HP)". iApply "H1". eauto.
Qed.
*)
Lemma crash_borrow_later_conseq P Pc P' Pc' :
□ (P' -∗ Pc') -∗
▷ (P -∗ P') -∗
▷ □ (Pc' -∗ Pc) -∗
crash_borrow P Pc -∗ crash_borrow P' Pc'.
Proof.
iIntros "#Hw1' Hw2' #Hw3'".
iIntros "Hborrow".
iDestruct "Hborrow" as (P0 Pc0) "(#Hw1&Hw2&#H3&Hinv&Htok&Htok')".
rewrite /crash_borrow.
iExists P0, Pc0. iSplit; first eauto. iFrame "Hinv Htok Htok'".
iSplitL "Hw2 Hw2'".
- iNext. iIntros. iApply "Hw2'". iApply "Hw2". done.
- iNext. iIntros. iModIntro. iIntros. iApply "H3". iApply "Hw3'". done.
Qed.
Lemma crash_borrow_conseq P Pc P' Pc' :
□ (P' -∗ Pc') -∗
(P -∗ P') -∗
□ (Pc' -∗ Pc) -∗
crash_borrow P Pc -∗ crash_borrow P' Pc'.
Proof.
iIntros "#Hw1' Hw2' #Hw3'".
iIntros "Hborrow".
iDestruct "Hborrow" as (P0 Pc0) "(#Hw1&Hw2&#H3&Hinv&Htok&Htok')".
rewrite /crash_borrow.
iExists P0, Pc0. iSplit; first eauto. iFrame "Hinv Htok Htok'".
iSplitL "Hw2 Hw2'".
- iNext. iIntros. iApply "Hw2'". iApply "Hw2". done.
- iNext. iIntros. iModIntro. iIntros. iApply "H3". iApply "Hw3'". done.
Qed.
(*
Lemma wpc_crash_borrow_split' k E e Φ Φc P Pc P1 P2 Pc1 Pc2 :
language.to_val e = None →
▷ crash_borrow P Pc -∗
▷▷ (P -∗ P1 ∗ P2) -∗
▷▷ □ (P1 -∗ Pc1) -∗
▷▷ □ (P2 -∗ Pc2) -∗
▷▷ (Pc1 ∗ Pc2 -∗ Pc) -∗
WPC e @ NotStuck; k; E {{ λ v, (crash_borrow P1 Pc1 ∗ crash_borrow P2 Pc2) -∗ (Φc ∧ Φ v) }} {{ Φc }} -∗
WPC e @ NotStuck; k; E {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnval) "Hborrow Hshift #Hwand1 #Hwand2 Hwandc Hwpc".
iDestruct "Hborrow" as (??) "(#Hw1&Hw2&Hw3&Hinv&>Htok&>Htok')".
iApply (wpc_later_tok_use2 with "[$]"); first done.
iNext. iNext.
iApply (wpc_staged_inv_inuse); first done.
iFrame "Hinv".
iSplit.
{ iIntros. rewrite wpc_unfold. iDestruct ("Hwpc" $! _) as "(_&Hwpc)".
iApply (wpc_crash_modality_wand with "Hwpc").
iIntros "$". eauto. }
iIntros "HP".
iDestruct ("Hshift" with "[HP Hw2]") as "(HP1&HP2)".
{ iApply "Hw2". eauto. }
iIntros (mj Hlt).
iApply wpc_fupd2.
iApply (wpc_pri_inv_tok_res).
iIntros (E1') "Hitok1".
iApply (wpc_pri_inv_tok_res).
iIntros (E2') "Hitok2".
iApply (wpc_later_tok_invest with "[$]"); first done.
rewrite wpc_eq. iIntros (mj').
iApply (wpc0_strong_mono with "Hwpc"); auto.
iSplit; last first.
{ iIntros "$ !>". iSplitR; first eauto. iApply "Hw3". iApply "Hwandc". iSplitL "HP1".
- iApply "Hwand1". eauto.
- iApply "Hwand2". eauto.
}
iIntros (v) "Hc !> Htok".
(* create staged inv for first crash borrow *)
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iMod (staged_inv_create _ _ P1 Pc1 ⊤ _ mj with "[$] [$] Hitok1 [$] [$]") as "(Hval1&Hcancel1)".
{ auto. }
(* create staged inv for second crash borrow *)
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iMod (staged_inv_create _ _ P2 Pc2 ⊤ _ mj with "[$] [$] Hitok2 [$] [$]") as "(Hval2&Hcancel2)".
{ auto. }
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iDestruct ("Htok") as "(Htok3&Htok)".
iDestruct ("Htok") as "(Htok4&Htok)".
iSpecialize ("Hc" with "[Htok1 Htok2 Htok3 Htok4 Hval1 Hval2]").
{ iSplitL "Htok1 Htok2 Hval1".
- iExists P1, Pc1. iFrame "Hval1". iFrame "#". iFrame. iSplitL; eauto.
- iExists P2, Pc2. iFrame "Hval2". iFrame "#". iFrame. iSplitL; eauto.
}
iDestruct (staged_inv_cancel_wpc_crash_modality with "Hcancel1") as "Hcancel1".
iDestruct (staged_inv_cancel_wpc_crash_modality with "Hcancel2") as "Hcancel2".
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct (wpc_crash_modality_combine with "[$] [$] [$]") as "Hcombined".
iModIntro. iSplitR "Hc".
{
iApply (wpc_crash_modality_wand with "Hcombined").
iIntros "(?&?) !>". iApply "Hw3". iApply "Hwandc". by iFrame.
}
iSplit.
- iDestruct "Hc" as "(Hc&_)".
iApply (wpc_crash_modality_intro). auto.
- iDestruct "Hc" as "(_&$)". eauto.
Qed.
Lemma wpc_crash_borrow_split k E e Φ Φc P Pc P1 P2 Pc1 Pc2 :
language.to_val e = None →
▷ crash_borrow P Pc -∗
▷ (P -∗ P1 ∗ P2) -∗
▷ □ (P1 -∗ Pc1) -∗
▷ □ (P2 -∗ Pc2) -∗
▷ (Pc1 ∗ Pc2 -∗ Pc) -∗
WPC e @ NotStuck; k; E {{ λ v, (crash_borrow P1 Pc1 ∗ crash_borrow P2 Pc2) -∗ (Φc ∧ Φ v) }} {{ Φc }} -∗
WPC e @ NotStuck; k; E {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnval) "Hborrow Hshift #Hwand1 #Hwand2 Hwandc Hwpc".
iApply (wpc_crash_borrow_split' with "[$] [$] [$] [$] [$]"); eauto.
Qed.
Lemma wpc_crash_borrow_combine' k E e Φ Φc P Pc P1 P2 Pc1 Pc2 :
language.to_val e = None →
▷ crash_borrow P1 Pc1 -∗
▷ crash_borrow P2 Pc2 -∗
▷▷ □ (P -∗ Pc) -∗
▷▷ (Pc -∗ (Pc1 ∗ Pc2)) -∗
▷▷ (P1 ∗ P2 ==∗ P) -∗
WPC e @ NotStuck; k; E {{ λ v, (crash_borrow P Pc) -∗ (Φc ∧ Φ v) }} {{ Φc }} -∗
WPC e @ NotStuck; k; E {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnval) "Hborrow1 Hborrow2 #Hc Hwandc12 HwandP Hwpc".
iDestruct "Hborrow1" as (??) "(#Hw1&Hw2&Hw3&Hinv1&Htok1&>Htok2)".
iApply (wpc_later_tok_use2 with "[$]"); first done.
iNext.
iNext.
iApply (wpc_staged_inv_inuse2); first done.
iFrame "Htok1 Hinv1".
iSplit.
{ iIntros. rewrite wpc_unfold. iDestruct ("Hwpc" $! _) as "(_&Hwpc)".
iApply (wpc_crash_modality_wand with "Hwpc").
iIntros "$". eauto. }
iIntros "HP1". iIntros (mj_wp1 Hlt1).
iDestruct "Hborrow2" as (??) "(#Hw1'&Hw2'&Hw3'&Hinv2&Htok2&_)".
iApply (wpc_staged_inv_inuse); first done.
iFrame "Hinv2".
iSplit.
{ iIntros. rewrite wpc_unfold. iDestruct ("Hwpc" $! _) as "(_&Hwpc)".
iApply (wpc_crash_modality_wand with "Hwpc").
iIntros "HΦc".
iModIntro. iFrame. iSplitR; first eauto.
iApply wpc_crash_modality_intro. iApply "Hw3". iApply "Hw1". iApply "Hw2". iFrame. }
iIntros "HP2". iIntros (mj_wp2 Hlt2).
iApply wpc_fupd2.
iApply (wpc_later_tok_invest with "[$]"); first done.
iApply (wpc_pri_inv_tok_res).
iIntros (Enew) "Hitok_new".
iApply (wpc_pri_inv_tok_res).
iIntros (Esplit) "Hitok_split".
rewrite wpc_eq. iIntros (mj').
iApply (wpc0_strong_mono with "Hwpc"); auto.
iSplit; last first.
{ iIntros "$ !>". iSplitL "HP1 Hw3 Hw2".
- iSplitR; first eauto. iApply wpc_crash_modality_intro. iApply "Hw3". iApply "Hw1". iApply "Hw2". eauto.
- iApply "Hw3'". iApply "Hw1'". iApply "Hw2'". eauto.
}
iIntros (v) "Hc' !> Htok".
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iMod ("HwandP" with "[HP1 HP2 Hw2 Hw2']") as "HP".
{ iSplitL "HP1 Hw2".
- iApply "Hw2". eauto.
- iApply "Hw2'". eauto. }
assert (∃ mj0, /2 < mj0 ∧ mj0 < mj_wp1 `min` mj_wp2)%Qp as (mj0&Hmj0).
{
apply Qp.lt_densely_ordered.
apply Qp.min_glb1_lt; auto.
}
iMod (staged_inv_create _ _ P Pc ⊤ _ mj0 with "[$] [$] Hitok_new [$] [$]") as "(Hval&Hcancel)".
{ naive_solver. }
iDestruct (staged_inv_cancel_wpc_crash_modality with "Hcancel") as "Hcancel".
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iAssert (wpc_crash_modality ⊤ mj0 (Pc1 ∗ Pc2))%I with "[Hwandc12 Hcancel]" as "Hcancel".
{ iApply (wpc_crash_modality_wand with "Hcancel"). iIntros "? !>".
by iApply "Hwandc12". }
iDestruct (wpc_crash_modality_split _ _ _ (mj_wp1 `min` mj_wp2) with "[$] [$] [$] [$]") as "Hcancel".
{ auto. }
iMod (fupd2_mask_subseteq ∅ ∅) as "Hclo"; try set_solver+.
iMod "Hcancel" as "(Hcancel1&Hcancel2)".
iMod "Hclo" as "_". iModIntro.
iSplitL "Hcancel2 Hw3'".
{ iApply (wpc_crash_modality_strong_wand with "Hcancel2"); auto; last first.
{ iIntros. iModIntro. iApply "Hw3'". iFrame. }
split.
- apply Qp.min_glb1_lt; auto.
- apply Qp.le_min_r.
}
iDestruct ("Htok") as "(Htok1&Htok)".
iDestruct ("Htok") as "(Htok2&Htok)".
iSpecialize ("Hc'" with "[Hval Htok1 Htok2]").
{ iExists _, _. iFrame "Hval Htok1 #".
iFrame. iSplitL; eauto. }
iSplit.
{ iApply wpc_crash_modality_intro.
iDestruct "Hc'" as "($&_)".
iSplitR; first eauto.
iApply (wpc_crash_modality_strong_wand with "Hcancel1"); auto.
{ split.
- apply Qp.min_glb1_lt; auto.
- apply Qp.le_min_l.
}
{ iIntros. iModIntro. iApply "Hw3". iFrame. }
}
iSplitL "Hcancel1 Hw3".
{ iApply (wpc_crash_modality_strong_wand with "Hcancel1"); auto.
{ split.
- apply Qp.min_glb1_lt; auto.
- apply Qp.le_min_l.
}
{ iIntros. iModIntro. iApply "Hw3". iFrame. }
}
iSplit.
- iDestruct "Hc'" as "(Hc'&_)". iApply wpc_crash_modality_intro. auto.
- iDestruct "Hc'" as "(_&$)". eauto.
Qed.
Lemma wpc_crash_borrow_combine k E e Φ Φc P Pc P1 P2 Pc1 Pc2 :
language.to_val e = None →
▷ crash_borrow P1 Pc1 -∗
▷ crash_borrow P2 Pc2 -∗
▷ □ (P -∗ Pc) -∗
▷ (Pc -∗ (Pc1 ∗ Pc2)) -∗
▷ (P1 ∗ P2 ==∗ P) -∗
WPC e @ NotStuck; k; E {{ λ v, (crash_borrow P Pc) -∗ (Φc ∧ Φ v) }} {{ Φc }} -∗
WPC e @ NotStuck; k; E {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnval) "Hborrow1 Hborrow2 #Hc Hwandc12 HwandP Hwpc".
iApply (wpc_crash_borrow_combine' with "[$Hborrow1] [$Hborrow2] [$] [$Hwandc12] [$HwandP]"); eauto.
Qed.
*)
Lemma wpc_crash_borrow_open_modify_fupd E1 e Φ Φc P Pc:
to_val e = None →
crash_borrow P Pc -∗
(Φc ∧ (P -∗ WPC e @ E1
{{λ v, |={E1, ∅}=> ∃ P', P' ∗ □ (P' -∗ Pc) ∗ (crash_borrow P' Pc ={∅, E1}=∗ (Φc ∧ Φ v))}}
{{ Φc ∗ Pc }})) -∗
WPC e @ E1 {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnv) "H1 Hwp".
iDestruct "H1" as (??) "(#Hw1 & Hw2 & #Hw3 & Hval & Hltok1 & Hltok2)".
iApply (wpc_staged_inv with "[$Hval Hwp Hltok1 Hltok2 Hw2]").
{ auto. }
iSplit.
{ iDestruct "Hwp" as "($ & _)". }
iIntros "HP".
iApply (wpc_later_tok_use2 with "[$]"); first done.
iNext. iNext.
iDestruct "Hwp" as "(_ & Hwp)".
iSpecialize ("Hwp" with "[HP Hw2]").
{ iApply "Hw2". eauto. }
iApply (wpc_strong_mono with "Hwp"); auto.
{ iSplit; last first.
{ iIntros "($&?) !> _". iApply "Hw3". eauto. }
iIntros (?) "Hw".
iModIntro.
iIntros "Hltok2".
iMod "Hw" as (P') "(HP & #Hwand & H)". iModIntro.
iExists (P' ∧ Pc')%I. iSplitL "HP Hw3".
{ iSplit; iFrame. iApply "Hw3". iApply "Hwand". eauto. }
iSplitL "".
{ iIntros "(_&$)". eauto. }
iIntros "Hs".
iMod ("H" with "[Hs Hltok1 Hltok2]").
{ iExists _, _. iFrame "Hs # ∗". iNext. iIntros "($&_)". }
eauto. }
Qed.
Lemma wpc_crash_borrow_open_modify E1 e Φ Φc P Pc:
to_val e = None →
crash_borrow P Pc -∗
(Φc ∧ (P -∗ WPC e @ E1
{{λ v, ∃ P', P' ∗ □ (P' -∗ Pc) ∗ (crash_borrow P' Pc -∗ (Φc ∧ Φ v))}}
{{ Φc ∗ Pc }})) -∗
WPC e @ E1 {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnv) "H1 Hwp".
iApply (wpc_crash_borrow_open_modify_fupd with "[$]"); first done.
iSplit.
{ iDestruct "Hwp" as "($&_)". }
iIntros "HP". iDestruct "Hwp" as "[_ Hwp]".
iSpecialize ("Hwp" with "[$]").
iApply (wpc_mono with "Hwp"); last done.
iIntros (?) "H". iDestruct "H" as (P') "(HP&HPc&Hclo)".
iApply (fupd_mask_weaken ∅); first set_solver+.
iIntros "H". iModIntro. iExists P'; iFrame. iIntros "Hcb".
iMod "H". iApply "Hclo". eauto.
Qed.
Lemma crash_borrow_crash_wand P Pc:
crash_borrow P Pc -∗ □ (P -∗ Pc).
Proof. iDestruct 1 as (??) "($&_)". Qed.
(*
Lemma crash_borrow_wpc_nval' E Pc P P' R :
crash_borrow P Pc -∗
▷ (P -∗ wp_nval E (□ (P' -∗ Pc) ∗ P' ∗ R)) -∗
wpc_nval E (R ∗ crash_borrow P' Pc).
Proof.
iIntros "Hborrow Hwand".
iDestruct "Hborrow" as (??) "(#Hw1&Hw2&#Hw3&Hval&Hltok1&Hltok2)".
iApply (wp_nval_wpc_nval with "[$]"). iNext.
iApply (wp_nval_strong_mono with "[-Hltok1]").
{ iApply (staged_inv_wp_nval _ _ _ P' (□ (P' -∗ Pc) ∗ R) with "[$Hval]"); auto.
iNext. iIntros "HPs'". iDestruct ("Hw2" with "[$]") as "HP".
iDestruct ("Hwand" with "[$]") as "H".
iApply (wp_nval_strong_mono with "H").
iIntros "(#Hshift&$&$)".
iModIntro. iFrame "#".
{ iModIntro. iIntros "?". iApply "Hw3". iApply "Hshift". iFrame. }
}
iIntros "((#Hw4&HR)&Hval)".
iModIntro. iIntros "Hltok2".
iDestruct "Hval" as (??????) "(?&?&?&?&?&?&?)".
iFrame "HR".
iExists P', Pc'.
iFrame "#".
iSplitR; first eauto.
iFrame.
iExists _, _, _, _, _, _. iFrame "∗".
Qed.
Lemma crash_borrow_wpc_nval E Pc P P' R :
crash_borrow P Pc -∗
▷ (P -∗ |NC={E}=> □ (P' -∗ Pc) ∗ P' ∗ R) -∗
wpc_nval E (R ∗ crash_borrow P' Pc).
Proof.
iIntros "Hborrow Hwand".
iApply (crash_borrow_wpc_nval' with "[$]"). iNext. iIntros "HP".
iApply (ncfupd_wp_nval). iMod ("Hwand" with "[$]") as "(#Hwand&HP'&HR)".
iModIntro. iApply wp_nval_intro.
iFrame. eauto.
Qed.
Lemma crash_borrow_wp_nval E Pc P P' R :
crash_borrow P Pc -∗
▷ (P -∗ wp_nval E (□ (P' -∗ Pc) ∗ P' ∗ R)) -∗
wp_nval E (R ∗ crash_borrow P' Pc).
Proof.
iIntros "Hborrow Hwand".
iDestruct "Hborrow" as (??) "(#Hw1&Hw2&#Hw3&Hval&Hltok1&Hltok2)".
iApply (wp_nval_strong_mono with "[-Hltok2 Hltok1]").
{ iApply (staged_inv_wp_nval _ _ _ P' (□ (P' -∗ Pc) ∗ R) with "[$Hval]"); auto.
iNext. iIntros "HPs'". iDestruct ("Hw2" with "[$]") as "HP".
iDestruct ("Hwand" with "[$]") as "H".
iApply (wp_nval_strong_mono with "H").
iIntros "(#Hshift&$&$)".
iModIntro. iFrame "#".
{ iModIntro. iIntros "?". iApply "Hw3". iApply "Hshift". iFrame. }
}
iIntros "((#Hw4&HR)&Hval)".
iModIntro.
iDestruct "Hval" as (??????) "(?&?&?&?&?&?&?)".
iFrame "HR".
iExists P', Pc'.
iFrame "#".
iSplitR; first eauto.
iFrame.
iExists _, _, _, _, _, _. iFrame "∗".
Qed.
Lemma crash_borrow_wp_nval_sepM `{Countable A} {B} E (P: A → B → iProp Σ) Q Q' R m:
([∗ map] i ↦ x ∈ m, crash_borrow (Q i x) (P i x)) -∗
(([∗ map] i ↦ x ∈ m, Q i x) -∗
wp_nval E (□ ([∗ map] i ↦ x ∈ m, ((Q' i x) -∗ (P i x))) ∗
([∗ map] i ↦ x ∈ m, (Q' i x)) ∗ R)) -∗
wp_nval E (R ∗ ([∗ map] i ↦ x ∈ m, crash_borrow (Q' i x) (P i x))).
Proof.
revert R.
induction m as [|i x m] using map_ind.
{
iIntros (?) "_ Hrestore".
iDestruct ("Hrestore" with "[]") as "H";
first by (iApply big_sepM_empty; trivial).
iApply (wp_nval_strong_mono with "H"). iIntros "(_&_&R)". iModIntro.
rewrite big_sepM_empty; trivial. iFrame.
}
iIntros (?) "Hcrash_invs Hrestores".
iDestruct (big_sepM_insert with "Hcrash_invs")
as "[Hcrash_inv Hcrash_invs]";
first by assumption.
iDestruct (IHm (crash_borrow (Q' i x) (P i x) ∗ R)%I with "Hcrash_invs [Hrestores Hcrash_inv]") as "H".
{
iIntros "HQs".
iDestruct (
crash_borrow_wp_nval _ _ _ _
(
([∗ map] i↦x ∈ m, Q' i x) ∗
□ ([∗ map] i↦x ∈ m, (Q' i x -∗ P i x)) ∗
R
)%I
with "Hcrash_inv [Hrestores HQs]"
) as "H".
{
iNext.
iIntros "HQ".
iDestruct ("Hrestores" with "[HQs HQ]") as "H".
{
iApply big_sepM_insert; first by assumption.
iFrame.
}
iApply (wp_nval_strong_mono with "H").
iIntros "(#Hstatuses&HQ's&HR)".
iDestruct (big_sepM_insert with "HQ's")
as "[HQ' HQ's]";
first by assumption. iModIntro.
iDestruct (big_sepM_insert with "Hstatuses")
as "[Hstatus Hstatuses']";
first by assumption.
iFrame "∗ #".
trivial.
}
iApply (wp_nval_strong_mono with "H"). iIntros "((?&?&?)&?)".
iFrame.
trivial.
}
iApply (wp_nval_strong_mono with "H").
iIntros "((?&?)&?)".
iModIntro.
iFrame.
iApply big_sepM_insert; first by assumption.
iFrame.
Qed.
*)
Lemma wpc_crash_borrow_open E1 e Φ Φc P Pc:
to_val e = None →
crash_borrow P Pc -∗
(Φc ∧ (P -∗ WPC e @ E1
{{λ v, P ∗ (crash_borrow P Pc -∗ (Φc ∧ Φ v))}}
{{ Φc ∗ Pc }})) -∗
WPC e @ E1 {{ Φ }} {{ Φc }}.
Proof.
iIntros (Hnv) "H1 Hwp".
iDestruct (crash_borrow_crash_wand with "[$]") as "#Hw".
iApply (wpc_crash_borrow_open_modify with "[$] [Hwp]"); auto.
iSplit; first by iDestruct "Hwp" as "($&_)".
iIntros "HP".
iDestruct "Hwp" as "(_&Hwp)".
iSpecialize ("Hwp" with "[$]").
iApply (wpc_strong_mono with "Hwp"); auto.