Commit df4574f2 authored by Robbert Krebbers's avatar Robbert Krebbers

Iris Proofmode.

parent 631c8260
......@@ -79,7 +79,6 @@ program_logic/saved_one_shot.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
program_logic/tactics.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......@@ -96,7 +95,20 @@ heap_lang/lib/barrier/specification.v
heap_lang/lib/barrier/protocol.v
heap_lang/lib/barrier/proof.v
heap_lang/lib/barrier/client.v
heap_lang/proofmode.v
tests/heap_lang.v
tests/program_logic.v
tests/one_shot.v
tests/joining_existentials.v
tests/proofmode.v
proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/environments.v
proofmode/intro_patterns.v
proofmode/spec_patterns.v
proofmode/tactics.v
proofmode/notation.v
proofmode/invariants.v
proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/sts.v
......@@ -974,19 +974,6 @@ Lemma later_wand P Q : ▷ (P -★ Q) ⊢ (▷ P -★ ▷ Q).
Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
Lemma later_iff P Q : (P Q) ( P Q).
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
Lemma löb_strong P Q : (P Q) Q P Q.
Proof.
intros Hlöb. apply impl_entails. rewrite -(löb (P Q)).
apply entails_impl, impl_intro_l. rewrite -{2}Hlöb.
apply and_intro; first by eauto.
by rewrite {1}(later_intro P) later_impl impl_elim_r.
Qed.
Lemma löb_strong_sep P Q : (P (P - Q)) Q P Q.
Proof.
move/wand_intro_l=>Hlöb. apply impl_entails.
rewrite -[(_ _)%I]always_elim. apply löb_strong.
by rewrite left_id -always_wand_impl -always_later Hlöb.
Qed.
(* Own *)
Lemma ownM_op (a1 a2 : M) :
......
......@@ -248,50 +248,3 @@ Ltac strip_later :=
intros_revert ltac:(
etrans; [apply: strip_later_r|];
etrans; [|apply: strip_later_l]; apply later_mono).
(** Transforms a goal of the form ..., ?0... ?1 ?2
into True ..., ?0... ?1 ?2, applies tac, and
the moves all the assumptions back. *)
(* TODO: this name may be a big too general *)
Ltac revert_all :=
lazymatch goal with
| |- _, _ =>
let H := fresh in intro H; revert_all;
(* TODO: Really, we should distinguish based on whether this is a
dependent function type or not. Right now, we distinguish based
on the sort of the argument, which is suboptimal. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- _ _ => apply impl_entails
end.
(** This starts on a goal of the form ..., ?0... ?1 ?2.
It applies löb where all the Coq assumptions have been turned into logical
assumptions, then moves all the Coq assumptions back out to the context,
applies [tac] on the goal (now of the form _ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started,
but with an additional assumption -ed to the context *)
Ltac löb tac :=
revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
apply: always_intro;
(* Now introduce again all the things that we reverted, and at the bottom,
do the work *)
let rec go :=
lazymatch goal with
| |- _ ( _, _) =>
apply forall_intro; let H := fresh in intro H; go; revert H
| |- _ ( _ _) =>
apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the from löb_strong and the we added. *)
| |- ?R (?L _) => apply impl_intro_l;
trans (L R)%I;
[eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]
end
in go.
From iris.heap_lang.lib.barrier Require Import proof.
From iris.heap_lang Require Import par.
From iris.program_logic Require Import auth sts saved_prop hoare ownership.
From iris.heap_lang Require Import proofmode.
Import uPred.
Definition worker (n : Z) : val :=
......@@ -15,63 +16,44 @@ Section client.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition y_inv q y : iProp :=
( f : val, y {q} f n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
Definition y_inv (q : Qp) (l : loc) : iProp :=
( f : val, l {q} f n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
Lemma y_inv_split q y :
y_inv q y (y_inv (q/2) y y_inv (q/2) y).
Lemma y_inv_split q l : y_inv q l (y_inv (q/2) l y_inv (q/2) l).
Proof.
rewrite /y_inv. apply exist_elim=>f.
rewrite -!(exist_intro f). rewrite heap_mapsto_op_split.
ecancel [y {_} _; y {_} _]%I. by rewrite [X in X _]always_sep_dup.
iIntros "Hl"; iDestruct "Hl" as {f} "[[Hl1 Hl2] #Hf]".
iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
Qed.
Lemma worker_safe q (n : Z) (b y : loc) :
(heap_ctx heapN recv heapN N b (y_inv q y))
WP worker n (%b) (%y) {{ λ _, True }}.
WP worker n (%b) (%y) {{ λ _, True }}.
Proof.
rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
rewrite comm. apply sep_mono_r. apply wand_intro_l.
rewrite sep_exist_r. apply exist_elim=>f. wp_seq.
(* TODO these parenthesis are rather surprising. *)
(ewp apply: (wp_load heapN _ _ q f)); eauto with I.
strip_later. (* hu, shouldn't it do that? *)
rewrite -assoc. apply sep_mono_r. apply wand_intro_l.
rewrite always_elim (forall_elim n) sep_elim_r sep_elim_l.
apply wp_mono=>?. eauto with I.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv".
iIntros "Hy"; iDestruct "Hy" as {f} "[Hy #Hf]".
wp_seq. wp_load.
iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"].
Qed.
Lemma client_safe :
heapN N heap_ctx heapN WP client {{ λ _, True }}.
Lemma client_safe : heapN N heap_ctx heapN WP client {{ λ _, True }}.
Proof.
intros ?. rewrite /client.
(ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y.
apply wand_intro_l. wp_let.
ewp eapply (newbarrier_spec heapN N (y_inv 1 y)); last done.
rewrite comm. rewrite {1}[heap_ctx _]always_sep_dup -!assoc.
apply sep_mono_r. apply forall_intro=>b. apply wand_intro_l.
wp_let. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
rewrite 2!{1}[heap_ctx _]always_sep_dup !assoc [(_ heap_ctx _)%I]comm.
ecancel [heap_ctx _]. sep_split right: []; last first.
{ do 2 apply forall_intro=>_. apply wand_intro_l.
eauto using later_intro with I. }
sep_split left: [send heapN _ _ _; heap_ctx _; y _]%I.
iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done.
iFrame "Hh". iIntros {l} "[Hr Hs]". wp_let.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs".
- (* The original thread, the sender. *)
(ewp eapply wp_store); eauto with I. strip_later.
ecancel [y _]%I. apply wand_intro_l.
wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", '"z" + #42)%V).
apply sep_intro_True_r; first done. apply: always_intro.
apply forall_intro=>n. wp_let. wp_op. by apply const_intro.
wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
rewrite recv_mono; last exact: y_inv_split.
rewrite (recv_split _ _ ) // pvs_frame_r. apply wp_strip_pvs.
(ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
do 2 rewrite {1}[heap_ctx _]always_sep_dup.
ecancel [heap_ctx _]. rewrite !assoc. sep_split right: []; last first.
{ do 2 apply forall_intro=>_. apply wand_intro_l.
eauto using later_intro with I. }
sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm.
iSplitL; [|iIntros {_ _} "_"; by iNext].
iDestruct recv_weaken "[] Hr" as "Hr".
{ iIntros "?". by iApply y_inv_split "-". }
iPvs recv_split "Hr" as "[H1 H2]"; first done.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|iIntros {_ _} "_"; by iNext]];
iApply worker_safe; by iSplit.
Qed.
End client.
......@@ -81,11 +63,9 @@ Section ClosedProofs.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
Proof.
apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last done.
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
(* This, too, should be automated. *)
by apply ndot_ne_disjoint.
iIntros "! Hσ".
iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
Qed.
Print Assumptions client_safe_closed.
......
From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import sts saved_prop tactics.
From iris.heap_lang Require Export heap wp_tactics.
From iris.program_logic Require Import saved_prop.
From iris.heap_lang Require Import proofmode.
From iris.proofmode Require Import sts.
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.heap_lang.lib.barrier Require Import protocol.
Import uPred.
......@@ -22,6 +23,7 @@ Proof. destruct H as (?&?&?). split; apply _. Qed.
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
Context (heapN N : namespace).
Implicit Types I : gset gname.
Local Notation iProp := (iPropG heap_lang Σ).
Definition ress (P : iProp) (I : gset gname) : iProp :=
......@@ -30,11 +32,11 @@ Definition ress (P : iProp) (I : gset gname) : iProp :=
Coercion state_to_val (s : state) : val :=
match s with State Low _ => #0 | State High _ => #1 end.
Arguments state_to_val !_ /.
Arguments state_to_val !_ / : simpl nomatch.
Definition state_to_prop (s : state) (P : iProp) : iProp :=
match s with State Low _ => P | State High _ => True%I end.
Arguments state_to_val !_ /.
Arguments state_to_prop !_ _ / : simpl nomatch.
Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
(l s ress (state_to_prop s P) (state_I s))%I.
......@@ -54,12 +56,8 @@ Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
PersistentP (barrier_ctx γ l P).
Proof. apply _. Qed.
(* TODO: Figure out if this has a "Global" or "Local" effect.
We want it to be Global. *)
Typeclasses Opaque barrier_ctx send recv.
Implicit Types I : gset gname.
(** Setoids *)
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed.
......@@ -79,33 +77,19 @@ Proof. solve_proper. Qed.
(** Helper lemmas *)
Lemma ress_split i i1 i2 Q R1 R2 P I :
i I i1 I i2 I i1 i2
(saved_prop_own i2 R2
saved_prop_own i1 R1 saved_prop_own i Q
(saved_prop_own i Q saved_prop_own i1 R1 saved_prop_own i2 R2
(Q - R1 R2) ress P I)
ress P ({[i1]} ({[i2]} (I {[i]}))).
Proof.
intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))).
rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //.
do 4 (rewrite big_sepS_insert; last set_solver).
rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert.
set savedQ := _ i Q. set savedΨ := _ i (Ψ _).
sep_split left: [savedQ; savedΨ; Q - _; (_ - Π★{set I} _)]%I.
- rewrite !assoc saved_prop_agree /=. strip_later.
apply wand_intro_l. to_front [P; P - _]%I. rewrite wand_elim_r.
rewrite (big_sepS_delete _ I i) //.
sep_split right: [Π★{set _} _]%I.
+ rewrite !assoc.
eapply wand_apply_r'; first done.
apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); last by eauto with I.
rewrite eq_sym. eauto with I.
+ apply big_sepS_mono; [done|] => j.
rewrite elem_of_difference not_elem_of_singleton=> -[??].
by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
- rewrite !assoc [(saved_prop_own i2 _ _)%I]comm; apply sep_mono_r.
apply big_sepS_mono; [done|]=> j.
rewrite elem_of_difference not_elem_of_singleton=> -[??].
by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP".
iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
iDestruct "HQR" "HΨ" as "[HR1 HR2]".
rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
- rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
Qed.
(** Actual proofs *)
......@@ -114,176 +98,110 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
(heap_ctx heapN l, recv l P send l P - Φ (%l))
WP newbarrier #() {{ Φ }}.
Proof.
intros HN. rewrite /newbarrier. wp_seq.
rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
rewrite !assoc. rewrite- pvs_wand_r; apply sep_mono_l.
(* The core of this proof: Allocating the STS and the saved prop. *)
eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ P).
rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
apply exist_elim=>i.
trans (pvs (heap_ctx heapN
(barrier_inv l P (State Low {[ i ]})) saved_prop_own i P)).
- rewrite -pvs_intro. cancel [heap_ctx heapN].
rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i P].
rewrite /barrier_inv /ress -later_intro. cancel [l #0]%I.
rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I ()%I).
by rewrite !big_sepS_singleton /= wand_diag -later_intro.
- rewrite (sts_alloc (barrier_inv l P) N); last by eauto.
rewrite !pvs_frame_r !pvs_frame_l.
rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l.
apply exist_elim=>γ.
rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
rewrite always_and_sep_l wand_diag later_True right_id.
rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
rewrite /barrier_ctx const_equiv // left_id.
ecancel_pvs [saved_prop_own i _; heap_ctx _; heap_ctx _;
sts_ctx _ _ _; sts_ctx _ _ _].
rewrite (sts_own_weaken _ _ (i_states i low_states) _
({[ Change i ]} {[ Send ]})).
+ apply pvs_mono.
rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
set_solver.
+ intros []; set_solver.
iIntros {HN} "[#? HΦ]".
rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iApply "HΦ".
iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
"-" as {γ'} "[#? Hγ']"; eauto.
{ iNext. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=.
iSplit; [|done]. by iNext; iIntros "?". }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ auto using sts.closed_op, i_states_closed, low_states_closed.
+ iApply sts_own_weaken "Hγ'";
auto using sts.closed_op, i_states_closed, low_states_closed;
set_solver. }
iPvsIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. iNext; by iIntros "?".
- iExists γ'. by iSplit.
Qed.
Lemma signal_spec l P (Φ : val iProp) :
(send l P P Φ #()) WP signal (%l) {{ Φ }}.
Proof.
rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
(* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
eauto with I ndisj.
ecancel [sts_ownS γ _ _].
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
eapply wp_store with (v' := #0); eauto with I ndisj.
strip_later. cancel [l #0]%I.
apply wand_intro_l. rewrite -(exist_intro (State High I)).
rewrite -(exist_intro ). rewrite const_equiv /=; last by eauto using signal_step.
rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
sep_split right: [Φ _]; last first.
{ apply wand_intro_l. eauto with I. }
(* Now we come to the core of the proof: Updating from waiting to ress. *)
rewrite /ress sep_exist_r. apply exist_mono=>{Φ} Φ.
ecancel [Π★{set I} (λ _, saved_prop_own _ _)]%I. strip_later.
rewrite wand_True. eapply wand_apply_l'; eauto with I.
rewrite /signal /send /barrier_ctx.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_store. destruct p; [|done].
iExists (State High I), ( : set token).
iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by iIntros "?"].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
iNext; iIntros "_"; by iApply "Hr".
Qed.
Lemma wait_spec l P (Φ : val iProp) :
(recv l P (P - Φ #())) WP wait (%l) {{ Φ }}.
Proof.
rename P into R. wp_rec.
rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
apply exist_elim=>i. rewrite -!(assoc ()%I). apply const_elim_sep_l=>?.
wp_focus (! _)%E.
(* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
eauto with I ndisj.
ecancel [sts_ownS γ _ _].
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs.
rewrite {1}/barrier_inv =>/=. rewrite later_sep.
eapply wp_load; eauto with I ndisj.
ecancel [ l {_} _]%I. strip_later.
apply wand_intro_l. destruct p.
{ (* a Low state. The comparison fails, and we recurse. *)
rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
rewrite [( sts.steps _ _ )%I]const_equiv /=; last by apply rtc_refl.
rewrite left_id -[( barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
wp_op; first done. intros _. wp_if. rewrite !assoc.
rewrite -always_wand_impl always_elim.
rewrite -{2}pvs_wp. rewrite -pvs_wand_r; apply sep_mono_l.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
rewrite const_equiv // left_id -later_intro.
ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q - _; R - _; sts_ctx _ _ _]%I.
apply sts_own_weaken; eauto using i_states_closed. }
(* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
rewrite [(_ (_ _ ))%I]sep_elim_l.
rewrite -(exist_intro (State High (I {[ i ]}))) -(exist_intro ).
change (i I) in Hs.
rewrite const_equiv /=; last by eauto using wait_step.
rewrite left_id -[( barrier_inv _ _ _)%I]later_intro {2}/barrier_inv.
rewrite -!assoc. apply sep_mono_r. rewrite /ress.
rewrite !sep_exist_r. apply exist_mono=>Ψ.
rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep.
ecancel [ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
apply wand_intro_l. set savedΨ := _ i (Ψ _). set savedQ := _ i Q.
to_front [savedΨ; savedQ]. rewrite saved_prop_agree /=.
wp_op; [|done]=> _. wp_if. rewrite -pvs_intro. rewrite !assoc. eapply wand_apply_r'; first done.
eapply wand_apply_r'; first done.
apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb "Hγ HQR HΦ" as "IH". wp_rec. wp_focus (! _)%E.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_load. destruct p.
- (* a Low state. The comparison fails, and we recurse. *)
iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
{ iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
iIntros "Hγ".
iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
{ iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iExists (State High (I {[ i ]})), ( : set token).
iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i Π★{set (I {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
iExists Ψ; iFrame "Hsp". iNext; by iIntros "_".
+ iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
Lemma recv_split E l P1 P2 :
nclose N E
recv l (P1 P2) |={E}=> recv l P1 recv l P2.
nclose N E recv l (P1 P2) |={E}=> recv l P1 recv l P2.
Proof.
rename P1 into R1. rename P2 into R2. intros HN.
rewrite {1}/recv /barrier_ctx.
apply exist_elim=>γ. rewrite sep_exist_r. apply exist_elim=>P.
apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc ()%I).
apply const_elim_sep_l=>?. rewrite -pvs_trans'.
(* I think some evars here are better than repeating *everything* *)
eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
eauto with I ndisj.
ecancel [sts_ownS γ _ _].
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs. rewrite /pvs_fsa.
eapply sep_elim_True_l.
{ eapply saved_prop_alloc_strong with (x := R1) (G := I). }
rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r.
apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc.
apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l.
{ eapply saved_prop_alloc_strong with (x := R2) (G := I {[ i1 ]}). }
rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r.
apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc.
apply const_elim_sep_l=>Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2.
destruct Hi2 as [Hi2 Hi12]. change (i I) in Hs.
(* Update to new state. *)
rewrite -(exist_intro (State p ({[i1]} ({[i2]} (I {[i]}))))).
rewrite -(exist_intro ({[Change i1 ]} {[ Change i2 ]})).
rewrite [( sts.steps _ _)%I]const_equiv; last by eauto using split_step.
rewrite left_id {1 3}/barrier_inv.
(* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *)
rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
rewrite {1}[saved_prop_own i1 _]always_sep_dup.
rewrite {1}[saved_prop_own i2 _]always_sep_dup !later_sep.
rewrite -![( saved_prop_own _ _)%I]later_intro.
ecancel [ l _; saved_prop_own i1 _; saved_prop_own i2 _ ;
ress _ _ ; (Q - _) ; saved_prop_own i _]%I.
apply wand_intro_l. rewrite !assoc. rewrite /recv.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
rewrite /barrier_ctx const_equiv // left_id.
ecancel_pvs [saved_prop_own i1 _; saved_prop_own i2 _; heap_ctx _; heap_ctx _;
sts_ctx _ _ _; sts_ctx _ _ _].
rewrite !wand_diag later_True !right_id.
rewrite -sts_ownS_op; eauto using i_states_closed.
- apply sts_own_weaken;
eauto using sts.closed_op, i_states_closed. set_solver.
- set_solver.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros {?} "Hr"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iApply pvs_trans'.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
iPvs (saved_prop_alloc_strong _ (R1: %CF iProp) I) as {i1} "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]}))
as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1]} ({[i2]} (I {[i]})))).
iExists ({[Change i1 ]} {[ Change i2 ]}).
iSplit; [by eauto using split_step|iSplitL].
- iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
- iIntros "Hγ".
iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
set_solver. }
iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
by iNext; iIntros "?".
+ iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
by iNext; iIntros "?".
Qed.