Commit b0fe9afb authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent c8a2d68b
......@@ -38,11 +38,11 @@ Section auth_excl.
( to_auth_excl x to_auth_excl y) - (x y : iProp Σ).
Proof.
iIntros "Hvalid".
iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
iDestruct "Hy" as ([z|]) "Hy"; last first.
- by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
iDestruct "Hle" as ([z|]) "Hy"; last first.
- by rewrite bi.option_equivI /= excl_equivI.
- iRewrite "Hy" in "Hvalid".
by rewrite left_id uPred.option_validI /= excl_validI /=.
by rewrite uPred.option_validI /= excl_validI /=.
Qed.
Lemma excl_eq γ x y :
......@@ -64,4 +64,4 @@ Section auth_excl.
eapply exclusive_local_update. done. }
by rewrite own_op.
Qed.
End auth_excl.
\ No newline at end of file
End auth_excl.
......@@ -121,10 +121,10 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (lsγ) "[Hls Hls']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (rsγ) "[Hrs Hrs']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. }
iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
{ rewrite /is_list_ref; eauto. }
iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
......
......@@ -185,11 +185,11 @@ Section stype_specs.
Proof.
iIntros "[#Hcctx [Hcol Hcor]]".
iMod (own_alloc ( (to_stype_auth_excl st)
(to_stype_auth_excl st)))
as (lγ) "[Hlsta Hlstf]"; first done.
(to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
{ by apply auth_both_valid_2. }
iMod (own_alloc ( (to_stype_auth_excl (dual_stype st))
(to_stype_auth_excl (dual_stype st))))
as (rγ) "[Hrsta Hrstf]"; first done.
(to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
{ by apply auth_both_valid_2. }
pose (SessionType_name cγ lγ rγ) as stγ.
iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ iNext. rewrite /inv_st. eauto 10 with iFrame. }
......
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