Commit 3e2fda9e authored by Janno's avatar Janno Committed by Robbert Krebbers
Browse files

Add triple notation for generalized post-condition

parent c476d109
...@@ -91,11 +91,11 @@ Proof. ...@@ -91,11 +91,11 @@ Proof.
Qed. Qed.
(** Actual proofs *) (** Actual proofs *)
Lemma newbarrier_spec (P : iProp Σ) (Φ : val iProp Σ) : Lemma newbarrier_spec (P : iProp Σ) :
heapN N heapN N
heap_ctx ( l, recv l P send l P - Φ #l) WP newbarrier #() {{ Φ }}. {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P send l P }}}.
Proof. Proof.
iIntros (HN) "[#? HΦ]". iIntros (HN Φ) "[#? HΦ]".
rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]"). iApply ("HΦ" with ">[-]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
...@@ -117,14 +117,15 @@ Proof. ...@@ -117,14 +117,15 @@ Proof.
- auto. - auto.
Qed. Qed.
Lemma signal_spec l P (Φ : val iProp Σ) : Lemma signal_spec l P :
send l P P Φ #() WP signal #l {{ Φ }}. {{{ send l P P }}} signal #l {{{; #(), True }}}.
Proof. Proof.
rewrite /signal /send /barrier_ctx /=. rewrite /signal /send /barrier_ctx /=.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let. iIntros (Φ) "((Hs&HP)&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store. iFrame "HΦ". destruct p; [|done]. wp_store.
iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done. iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|].
iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl". iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
...@@ -132,11 +133,11 @@ Proof. ...@@ -132,11 +133,11 @@ Proof.
iNext. iIntros "_"; by iApply "Hr". iNext. iIntros "_"; by iApply "Hr".
Qed. Qed.
Lemma wait_spec l P (Φ : val iProp Σ) : Lemma wait_spec l P:
recv l P (P - Φ #()) WP wait #l {{ Φ }}. {{{ recv l P }}} wait #l {{{ ; #(), P }}}.
Proof. Proof.
rename P into R; rewrite /recv /barrier_ctx. rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros (Φ) "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iLöb as "IH". wp_rec. wp_bind (! _)%E.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
......
...@@ -21,7 +21,7 @@ Proof. ...@@ -21,7 +21,7 @@ Proof.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)). exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
split_and?; simpl. split_and?; simpl.
- iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto. - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
- iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP". - iIntros (l P) "!# [Hl HP]". iApply signal_spec; iFrame "Hl HP"; by eauto.
- iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto. - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
- iIntros (l P Q) "!#". by iApply recv_split. - iIntros (l P Q) "!#". by iApply recv_split.
- apply recv_weaken. - apply recv_weaken.
......
...@@ -50,6 +50,17 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) ...@@ -50,6 +50,17 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200, (at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope. format "'WP' e {{ v , Q } }") : uPred_scope.
Notation "'{{{' pre } } } e {{{ x .. y ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre ( x, .. ( y, post - ψ (pat)%V) .. )%I) WP e {{ ψ }})
(at level 20, x closed binder, y closed binder,
format "{{{ pre } } } e {{{ x .. y ; pat , post } } }") : C_scope.
Notation "'{{{' pre } } } e {{{ ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre (post - ψ (pat)%V)%I) WP e {{ ψ }})
(at level 20,
format "{{{ pre } } } e {{{ ; pat , post } } }") : C_scope.
Section wp. Section wp.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ. Implicit Types P : iProp Σ.
......
...@@ -43,7 +43,7 @@ Section client. ...@@ -43,7 +43,7 @@ Section client.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh". iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "Hy Hs". iSplitL "Hy Hs".
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done]. wp_store. iApply signal_spec; iFrame "Hs"; iSplitL "Hy"; [|by eauto].
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op. iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *) - (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros (_ _) "_ !>"]. iSplitL; [|by iIntros (_ _) "_ !>"].
......
...@@ -85,7 +85,7 @@ Proof. ...@@ -85,7 +85,7 @@ Proof.
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let. iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iMod (own_update with "Hγ") as "Hx". iMod (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). } { by apply (cmra_update_exclusive (Shot x)). }
iApply signal_spec; iFrame "Hs"; iSplit; last done. iApply signal_spec; iFrame "Hs"; iSplitR ""; last auto.
iExists x; auto. iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split. - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iMod (recv_split with "Hr") as "[H1 H2]"; first done. iMod (recv_split with "Hr") as "[H1 H2]"; first done.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment