Commit c1120a90 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

add a later in texan triples

parent 24b6bc9c
......@@ -104,11 +104,11 @@ Section heap.
Proof. by rewrite heap_mapsto_op_half. Qed.
(** Weakest precondition *)
Lemma wp_alloc E e v Φ :
Lemma wp_alloc E e v :
to_val e = Some v nclose heapN E
heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
{{{ heap_ctx }}} Alloc e @ E {{{ l; LitV (LitLoc l), l v }}}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iIntros (<-%of_to_val ? Φ) "[#Hinv HΦ]". rewrite /heap_ctx.
iMod (auth_empty heap_name) as "Ha".
iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !>".
......@@ -118,12 +118,12 @@ Section heap.
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed.
Lemma wp_load E l q v Φ :
Lemma wp_load E l q v :
nclose heapN E
heap_ctx l {q} v (l {q} v ={E}= Φ v)
WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
{{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E
{{{; v, l {q} v }}}.
Proof.
iIntros (?) "[#Hinv [>Hl HΦ]]".
iIntros (? Φ) "[[#Hinv >Hl] HΦ]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
......@@ -131,12 +131,12 @@ Section heap.
iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v Φ :
Lemma wp_store E l v' e v :
to_val e = Some v nclose heapN E
heap_ctx l v' (l v ={E}= Φ (LitV LitUnit))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
{{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E
{{{; LitV LitUnit, l v }}}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
iIntros (<-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
......@@ -147,12 +147,12 @@ Section heap.
by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E
heap_ctx l {q} v' (l {q} v' ={E}= Φ (LitV (LitBool false)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
{{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{; LitV (LitBool false), l {q} v' }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[[#Hinv >Hl] HΦ]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
......@@ -160,12 +160,12 @@ Section heap.
iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E
heap_ctx l v1 (l v2 ={E}= Φ (LitV (LitBool true)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
{{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{; LitV (LitBool true), l v2 }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
iIntros (<-%of_to_val <-%of_to_val ? Φ) "[[#Hinv >Hl] HΦ]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
......
......@@ -147,7 +147,7 @@ Proof.
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iModIntro. wp_if.
iApply ("IH" with "Hγ [HQR] HΦ"). auto.
iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
......
......@@ -20,7 +20,8 @@ Proof.
intros HN.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
split_and?; simpl.
- iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
- iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); first done.
iSplit; first done. iNext. eauto.
- 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 Q) "!#". by iApply recv_split.
......
......@@ -65,7 +65,7 @@ Section mono_proof.
by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10.
Qed.
......@@ -140,7 +140,7 @@ Section contrib_spec.
iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ l q n :
......
......@@ -19,15 +19,15 @@ Context `{!heapG Σ, !spawnG Σ}.
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ) :
to_val e = Some (f1,f2)%V
(heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iNext. iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
wp_apply join_spec; iFrame "Hl". iNext. iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
......
......@@ -70,7 +70,7 @@ Proof.
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ Hv").
iModIntro. wp_match. iApply ("IH" with "Hγ [Hv]"). auto.
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "Hv".
......
......@@ -76,7 +76,7 @@ Section proof.
iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
iApply try_acquire_spec. iFrame "#". iSplit.
- iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
- wp_if. iApply ("IH" with "HΦ").
- wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
Lemma release_spec γ lk R :
......
......@@ -136,7 +136,7 @@ Section proof.
- wp_cas_fail.
iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
{ iNext. iExists o', n'. by iFrame. }
iModIntro. wp_if. by iApply "IH".
iModIntro. wp_if. by iApply "IH"; auto.
Qed.
Lemma release_spec γ lk R :
......
......@@ -25,7 +25,7 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
(Δ'' |={E}=> Φ (LitV (LitLoc l))))
Δ WP Alloc e @ E {{ Φ }}.
Proof.
intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
......@@ -39,7 +39,8 @@ Lemma tac_wp_load Δ Δ' E i l q v Φ :
(Δ' |={E}=> Φ v)
Δ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
intros. rewrite -wp_fupd -wp_load // -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -53,7 +54,8 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
(Δ'' |={E}=> Φ (LitV LitUnit))
Δ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
intros. rewrite -wp_fupd -wp_store // -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -66,7 +68,8 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
(Δ' |={E}=> Φ (LitV (LitBool false)))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
intros. rewrite -wp_fupd -wp_cas_fail // -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -80,8 +83,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
(Δ'' |={E}=> Φ (LitV (LitBool true)))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros; subst.
rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
intros; subst. rewrite -wp_fupd -wp_cas_suc // -assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......
......@@ -50,16 +50,27 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
(* Texan triples *)
Notation "'{{{' pre } } } e {{{ x .. y ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre ( x, .. ( y, post - ψ (pat)%V) .. )%I) WP e {{ ψ }})
(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 @ E {{{ x .. y ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre ( x, .. ( y, post - ψ (pat)%V) .. )%I) WP e @ E {{ ψ }})
(at level 20, x closed binder, y closed binder,
format "{{{ pre } } } e @ E {{{ x .. y ; pat , post } } }") : C_scope.
Notation "'{{{' pre } } } e {{{ ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre (post - ψ (pat)%V)%I) WP e {{ ψ }})
(pre (post - ψ (pat)%V)%I) WP e {{ ψ }})
(at level 20,
format "{{{ pre } } } e {{{ ; pat , post } } }") : C_scope.
Notation "'{{{' pre } } } e @ E {{{ ; pat , post } } }" :=
( (ψ : _ uPred _),
(pre (post - ψ (pat)%V)%I) WP e @ E {{ ψ }})
(at level 20,
format "{{{ pre } } } e @ E {{{ ; pat , post } } }") : C_scope.
Section wp.
Context `{irisG Λ Σ}.
......
......@@ -30,7 +30,7 @@ Section client.
Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv".
iDestruct 1 as (f) "[Hy #Hf]".
iNext. iDestruct 1 as (f) "[Hy #Hf]".
wp_seq. wp_load.
iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
Qed.
......@@ -39,7 +39,7 @@ Section client.
Proof.
iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let.
iFrame "Hh". iNext. iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "Hy Hs".
- (* The original thread, the sender. *)
......
......@@ -36,7 +36,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
iDestruct 1 as (x) "[#Hγ Hx]".
iNext. iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
iIntros (v) "?"; iExists x; by iSplit.
Qed.
......@@ -77,7 +77,7 @@ Proof.
iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iFrame "Hh". iIntros (l) "[Hr Hs]".
iFrame "Hh". iNext. iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post); iFrame "Hh".
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
......
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