Commit a7b129ac authored by Robbert Krebbers's avatar Robbert Krebbers

Allow to use fancy updates in `iProto_le`

parent e6d11e79
...@@ -172,7 +172,7 @@ Section channel. ...@@ -172,7 +172,7 @@ Section channel.
(|={,E}=> vs, (|={,E}=> vs,
chan_own γ s vs chan_own γ s vs
( v vs', vs = v :: vs' - ( v vs', vs = v :: vs' -
chan_own γ s vs' ={E,}= Φ (SOMEV v)))) - chan_own γ s vs' ={E,,}= Φ (SOMEV v)))) -
WP try_recv (side_elim s c2 c1) {{ Φ }}. WP try_recv (side_elim s c2 c1) {{ Φ }}.
Proof. Proof.
iIntros "Hc HΦ". wp_lam; wp_pures. iIntros "Hc HΦ". wp_lam; wp_pures.
...@@ -193,7 +193,7 @@ Section channel. ...@@ -193,7 +193,7 @@ Section channel.
iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv. iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']". iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro. wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_apply (lisnil_spec with "Hll"); iIntros "Hll". iMod "HΦ".
wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=. wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]"). wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
{ iApply (chan_inv_alt s). { iApply (chan_inv_alt s).
...@@ -206,7 +206,7 @@ Section channel. ...@@ -206,7 +206,7 @@ Section channel.
(|={,E}=> vs, (|={,E}=> vs,
chan_own γ s vs chan_own γ s vs
v vs', vs = v :: vs' - v vs', vs = v :: vs' -
chan_own γ s vs' ={E,}= Φ v) - chan_own γ s vs' ={E,,}= Φ v) -
WP recv (side_elim s c2 c1) {{ Φ }}. WP recv (side_elim s c2 c1) {{ Φ }}.
Proof. Proof.
iIntros "#Hc HΦ". iLöb as "IH". wp_lam. iIntros "#Hc HΦ". iLöb as "IH". wp_lam.
...@@ -215,6 +215,7 @@ Section channel. ...@@ -215,6 +215,7 @@ Section channel.
iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH". iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH".
- iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs". - iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs".
iIntros "!> !>" (v vs' ->) "Hvs". iIntros "!> !>" (v vs' ->) "Hvs".
iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures. iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !>". iMod "HΦ".
iIntros "!> !>". by wp_pures.
Qed. Qed.
End channel. End channel.
This diff is collapsed.
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