Skip to content
Snippets Groups Projects

Bump Iris with changes in `auth`

Merged Bump Iris with changes in `auth`
hai/auth_frac into master
Merged Hai Dang requested to merge hai/auth_frac into master
Compare
and
19 files
+ 72
− 69
Compare changes
  • Side-by-side
  • Inline
Files
19
theories/hocap/contrib_bag.v
+ 1
− 1
@@ -50,7 +50,7 @@ Section proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd.
iApply (newBag_spec b NB); eauto.
iNext. iIntros (v γb) "[#Hbag Hcntn]".
iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first done.
iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first by apply auth_both_valid.
iMod (inv_alloc NI _ (∃ X, bag_contents b γb X ∗ own γ (●! X))%I with "[Hcntn Hown]") as "#Hinv".
{ iNext. iExists _. iFrame. }
iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".