Commit cd113065 authored by Robbert Krebbers's avatar Robbert Krebbers

Make invariant rules more consistent with Iris.

See discussion at iris!368 (diffs, comment 43824)
parent 7f69e9f4
Pipeline #23935 passed with stage
in 18 minutes and 2 seconds
......@@ -262,7 +262,8 @@ Section proofs.
iMod (fcinv_alloc_strong _ (N .@ "sts"))
as (γinv) "([Hinv_own1 [Hinv_own2 Hinv_own3]] & Hcreate)".
set γs := GNames γx_alive γy_alive x_or_y_commitment γclean γxs γys γinv.
iMod ("Hcreate" $! (messaging_sts γs x_alive y_alive px py) with "[Hx Hy Hnochoice]") as "[Hinv_cancel #Hinv]".
iMod ("Hcreate" $! (messaging_sts γs x_alive y_alive px py)
with "[Hx Hy Hnochoice]") as "[#Hinv Hinv_cancel]".
{ iNext. iLeft; iFrame. }
wp_apply (iron_wp_fork
with "[-Hcancel1 Hcancel2 Hclean Hinv_cancel Hinv_own1]"); last first.
......
......@@ -215,7 +215,7 @@ Section queue_spec.
iMod (own_alloc ( (Excl' l) (Excl' l))) as (γe) "[Hγe Hγe']";
first by apply auth_both_valid.
iMod (fcinv_alloc_named _ N (λ γinv, queue_inv (QueueName γinv γ γd γe) lhptr ltptr)
with "[Hlhptr' Hγ' Hl Hγe]") as (γinv) "([Hγinv Hγinv']&Hγc&#?)".
with "[Hlhptr' Hγ' Hl Hγe]") as (γinv) "(#? & Hγc & [Hγinv Hγinv'])".
{ iIntros "!>" (γinv).
iExists l, l, []. rewrite queue_own_eq /=. iFrame; auto. }
iModIntro. iApply ("HΦ" $! _ (QueueName γinv γ γd γe)). iSplitR.
......@@ -242,23 +242,23 @@ Section queue_spec.
iDestruct "Hh" as (?? ?%eq_sym) "(Hγinv & Hlhptr & Hγd)"; simplify_eq.
iDestruct "Hlhptr" as (l) "Hlhptr".
wp_lam; wp_proj; wp_let. wp_load; wp_let. wp_bind (! _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "[H Hclose]"; first done.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh lt vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt)".
iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %->; simpl.
destruct vs as [|v vs'].
{ iDestruct "Hlist" as ">->".
wp_load. iMod ("Hupd" with "Hvs") as "[Hvs HΦ]".
iMod ("Hclose" with "[Hvs Hlhptr' Hlt Hγe]") as "Hγinv".
iMod ("Hclose" with "[Hvs Hlhptr' Hlt Hγe]") as "_".
{ iExists lt, lt, []. iFrame; auto. }
iModIntro. wp_match. iApply "HΦ". iExists lhptr, ltptr. eauto with iFrame. }
iDestruct "Hlist" as (l') "[>[[Hlh Hlh']|[Hγd' ?]] Hlist]"; last first.
{ iDestruct (own_valid_2 with "Hγd Hγd'") as %[]. }
wp_load.
iMod ("Hclose" with "[Hvs Hlhptr' Hlh' Hγd Hlt Hlist Hγe]") as "Hγinv".
iMod ("Hclose" with "[Hvs Hlhptr' Hlh' Hγd Hlt Hlist Hγe]") as "_".
{ iExists lh, lt, (v :: vs'). iNext. iFrame "Hvs Hlhptr' Hlt Hγe".
iExists l'. auto with iFrame. }
clear vs'. iModIntro. wp_match. wp_proj. wp_let. wp_bind (_ <- _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "[H Hclose]"; first done.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh' lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt)".
iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %?%eq_sym; simplify_eq.
destruct vs as [|v' vs'].
......@@ -270,7 +270,7 @@ Section queue_spec.
iCombine "Hlh Hlh'" as "Hlh"; iCombine "Hlhptr Hlhptr'" as "Hlhptr".
wp_store. iDestruct "Hlhptr" as "[Hlhptr Hlhptr']".
iMod ("Hupd" with "Hvs") as "[Hvs HΦ]".
iMod ("Hclose" with "[Hvs Hlhptr' Hlt Hγe Hlist]") as "Hγinv".
iMod ("Hclose" with "[Hvs Hlhptr' Hlt Hγe Hlist]") as "_".
{ iExists lh', lt', vs'. iNext. iFrame "Hvs Hlhptr' Hlt Hγe".
destruct vs' as [|v'' vs'']=> //=.
iDestruct "Hlist" as (l) "[Hlh Hlist]". auto with iFrame. }
......@@ -291,7 +291,7 @@ Section queue_spec.
"(Hγinv & Hγe' & Hltptr)"; simplify_eq.
do 2 wp_lam. wp_proj; wp_let. wp_load; wp_let.
wp_alloc ltn as "Hltn"; wp_let. wp_bind (_ <- _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "[H Hclose]"; first done.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt')".
iDestruct (own_valid_2 with "Hγe Hγe'")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
......@@ -299,7 +299,7 @@ Section queue_spec.
{ by apply auth_update, option_local_update,
(exclusive_local_update _ (Excl ltn)). }
wp_store. iMod ("Hupd" with "Hvs") as "[Hvs HΦ]".
iMod ("Hclose" with "[Hvs Hlhptr' Hγe Hlist Hlt' Hltn]") as "Hγinv".
iMod ("Hclose" with "[Hvs Hlhptr' Hγe Hlist Hlt' Hltn]") as "_".
{ iNext. iExists lh, ltn, (vs ++ [v]). iFrame "Hvs Hlhptr' Hγe Hltn".
destruct vs as [|v' vs]; simpl.
{ iDestruct "Hlist" as "->". eauto with iFrame. }
......@@ -420,9 +420,9 @@ Section queue_bag_spec.
iApply (new_queue_spec (N .@ "queue") with "[//]"); first solve_ndisj.
iIntros "!>" (q γ) "(#Hq & Hc & Heh & Hdh & Hvs)".
iMod (fcinv_alloc _ (N .@ "inv") ( xs, γ {1/2} xs
[ list] x xs, Ψ x)%I with "[Hvs]") as (γinv) "([Hγinv1 Hγinv2]&Hinvc&Hinv)".
[ list] x xs, Ψ x)%I with "[Hvs]") as (γinv) "(#?&Hinvc&[Hγinv1 Hγinv2])".
{ iExists []; simpl; iFrame; auto. }
iApply ("HΦ" $! (QueueBagName γ γinv)). iModIntro; iFrame; iModIntro; iFrame; auto.
iApply ("HΦ" $! (QueueBagName γ γinv)). iModIntro; iFrame. iSplitL; auto.
Qed.
Lemma bag_insert_spec E q γ v `{ x, Uniform (Ψ x)} :
......@@ -438,11 +438,12 @@ Section queue_bag_spec.
wp_apply (enqueue_spec (N .@ "queue") _ _ _ _ (queue_bag_queue_name γ)
with "[] Henqueue"); eauto; first by solve_ndisj.
iIntros (vs) "Hbag".
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv") as "[H Hclose]"; first by solve_ndisj.
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv")
as "(H & Hown_inv & Hclose)"; first by solve_ndisj.
iDestruct "H" as (xs) "[>Hqueue_contents Hall]".
iDestruct (queue_own_agree with "Hbag Hqueue_contents") as %->.
iMod (queue_own_update_2 _ _ _ (xs ++ [v]) with "Hbag Hqueue_contents") as "[Hqueue_contents Hbag]".
iMod ("Hclose" with "[Hqueue_contents Hall HΨ]") as "Hinv_own".
iMod ("Hclose" with "[Hqueue_contents Hall HΨ]") as "_".
{ iNext. iExists (xs ++ [v]); iFrame. by simpl. }
iIntros "!> {$Hbag} !> Henqueue". iApply "HΦ"; iFrame.
Qed.
......@@ -459,17 +460,18 @@ Section queue_bag_spec.
iIntros (? Φ) "([#Hqueue #Hinv] & Hdequeue & Hown_inv) HΦ".
wp_apply (dequeue_spec (N .@ "queue") with "[] Hdequeue"); eauto; first by solve_ndisj.
iIntros (vs) "Hbag".
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv") as "[H Hclose]"; first by solve_ndisj.
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv")
as "(H & Hinv_own & Hclose)"; first by solve_ndisj.
iDestruct "H" as (xs) "[>Hqueue_contents Hall]".
iDestruct (queue_own_agree with "Hbag Hqueue_contents") as %->.
destruct xs as [|x xs]; simpl.
- iMod ("Hclose" with "[Hqueue_contents]") as "Hinv_own".
- iMod ("Hclose" with "[Hqueue_contents]") as "_".
{ iNext. iExists _; iFrame. by simpl. }
iIntros "!> {$Hbag} !> Hdequeue".
iApply "HΦ"; iLeft; iFrame. by iSplit.
- iDestruct "Hall" as "[HΨ Hall]".
iMod (queue_own_update_2 _ _ _ (xs) with "Hbag Hqueue_contents") as "[Hqueue_contents Hbag]".
iMod ("Hclose" with "[Hqueue_contents Hall]") as "Hinv_own".
iMod ("Hclose" with "[Hqueue_contents Hall]") as "_".
{ iNext. iExists _; iFrame. }
iIntros "!> {$Hbag} !> Hdequeue".
iApply "HΦ"; iRight; iFrame. iExists _; by iSplit.
......
......@@ -38,8 +38,8 @@ Section proof1.
Proof.
iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl"; wp_let.
iMod transfer_alloc as (γ) "(Ht₁ & Hs₁ & Ht₂)".
iMod (fcinv_alloc_strong _ N) as (γinv) "[[Hcown₁ Hcown₂] Halloc]".
iMod ("Halloc" $! (transfer_inv1 γ γinv l) with "[Hs₁ Hl]") as "[Hcancel #Hinv]".
iMod (fcinv_alloc_strong _ N) as (γinv) "[[Hcown₁ Hcown₂] Halloc]".
iMod ("Halloc" $! (transfer_inv1 γ γinv l) with "[Hs₁ Hl]") as "[#? Hcancel]".
{ iNext. iLeft. iFrame. }
wp_apply (iron_wp_fork with "[Ht₁ Hcown₁ HΦ]").
- iNext. do 2 wp_lam. wp_alloc k as "Hk". wp_let.
......@@ -64,7 +64,7 @@ Section proof1.
{ iLeft. iModIntro. do 2 iRight. iFrame; eauto. }
iModIntro. wp_match. wp_apply (iron_wp_free with "[$]").
iIntros "_"; wp_seq.
iMod (fcinv_cancel _ N _ with "Hinv Hcancel [$Hcown₁ $Hcown₂]")
iMod (fcinv_cancel _ N _ with "[$] Hcancel [$Hcown₁ $Hcown₂]")
as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]"; first done.
{ iDestruct (transfer_incompat with "Ht₃ Hs₁") as %[]. }
{ iDestruct (transfer_incompat with "Ht₃ Hs₂") as %[]. }
......@@ -89,7 +89,7 @@ Section proof2.
iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl"; wp_let.
iMod (fcinv_alloc_strong _ N) as (γ) "[Hγ Halloc]".
iEval (rewrite -Qp_three_quarter_quarter) in "Hγ"; iDestruct "Hγ" as "[Hγ Hγ']".
iMod ("Halloc" $! (transfer_inv2 γ l) with "[Hl]") as "[Hγc #?]".
iMod ("Halloc" $! (transfer_inv2 γ l) with "[Hl]") as "[#? Hγc]".
{ iExists NONEV; eauto with iFrame. }
wp_apply (iron_wp_fork with "[Hγ HΦ]").
- iIntros "!>". do 2 wp_lam. wp_alloc k as "Hk". wp_let.
......@@ -107,7 +107,7 @@ Section proof2.
iModIntro. wp_match. iApply ("IH" with "[$] [$]").
+ wp_load. iDestruct "Hinv" as (k') "(->&Hk'&Hγ1) /=".
iMod ("Hclose" with "[Hγc Hγ1 Hγ]") as "_".
{ iRight. iEval (rewrite -{1}Qp_three_quarter_quarter). iFrame. }
{ iRight. iEval (rewrite -{2}Qp_three_quarter_quarter). iFrame. }
iModIntro. wp_match. wp_apply (iron_wp_free with "[$]"); iIntros "_".
wp_seq. wp_apply (iron_wp_free with "[$]"); auto.
Qed.
......
......@@ -40,19 +40,19 @@ Section proof1.
iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl"; wp_let.
iMod transfer_alloc as (γ) "(Ht₁ & Hs₁ & Ht₂)".
iMod (fcinv_alloc _ N (transfer_inv1 γ l) with "[Hs₁ Hl]")
as (γinv) "[[Hcown₁ Hcown₂] [Hcancel #Hinv]]".
as (γinv) "(#Hinv & Hcancel & [Hcown₁ Hcown₂])".
{ iNext. iLeft. iFrame. }
wp_apply (par_spec (λ _, fcinv_own γinv (1 / 2))%I
(λ _, fcinv_own γinv (1 / 2) <affine> t γ )%I with "[Ht₁ Hcown₁] [Ht₂ Hcown₂]").
- do 2 wp_lam. wp_alloc k as "Hk". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & Hclose)"; first done.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & $ & Hclose)"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]".
+ wp_store. iDestruct (transfer_combine with "Ht₁ Hs₁") as "Hs₂".
iApply "Hclose". iNext. iRight. iLeft. eauto with iFrame.
+ iDestruct (transfer_incompat with "Ht₁ Hs₂") as %[].
+ iDestruct (transfer_incompat with "Ht₁ Hs₃") as %[].
- wp_lam. iLöb as "IH"; wp_rec. wp_bind (! _)%E.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & Hclose)"; first done.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & Hγ & Hclose)"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]";
last (iDestruct (transfer_incompat with "Ht₂ Hs₃") as %[]).
+ wp_load. iMod ("Hclose" with "[Hl Hs₁]").
......@@ -90,7 +90,7 @@ Section proof2.
iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl"; wp_let.
iMod (fcinv_alloc_strong _ N) as (γ) "[Hγ Halloc]".
iEval (rewrite -Qp_three_quarter_quarter) in "Hγ"; iDestruct "Hγ" as "[Hγ Hγ']".
iMod ("Halloc" $! (transfer_inv2 γ l) with "[Hl]") as "[Hγc #?]".
iMod ("Halloc" $! (transfer_inv2 γ l) with "[Hl]") as "[#? Hγc]".
{ iExists NONEV; eauto with iFrame. }
wp_apply (par_spec (λ _, emp)%I (λ _, l -)%I with "[Hγ] [Hγc Hγ']").
- do 2 wp_lam. wp_alloc k as "Hk". wp_let.
......@@ -107,7 +107,7 @@ Section proof2.
iModIntro. wp_match. iApply ("IH" with "[$] [$]").
+ wp_load. iDestruct "Hinv" as (k') "(->&Hk'&Hγ1) /=".
iMod ("Hclose" with "[Hγc Hγ1 Hγ]") as "_".
{ iRight. iEval (rewrite -{1}Qp_three_quarter_quarter). iFrame. }
{ iRight. iEval (rewrite -{2}Qp_three_quarter_quarter). iFrame. }
iModIntro. wp_match. wp_apply (iron_wp_free with "[$]"); eauto.
- iIntros (v1 v2) "[_ Hl] !>". iDestruct "Hl" as (v) "Hl".
wp_seq. wp_apply (iron_wp_free with "[$]"); auto.
......
......@@ -40,9 +40,10 @@ Definition lock_inv `{!heapG Σ, !lockG Σ} (γ : gname)
Definition is_lock `{!heapG Σ, !lockG Σ} (N : namespace) (γ : lock_name)
(lk : val) (p : frac) (R : ironProp Σ) : ironProp Σ :=
( l : loc, lk = #l fcinv_own (lock_fcinv_name γ) p
( l : loc, lk = #l
fcinv N (lock_fcinv_name γ) (lock_inv (lock_excl_name γ) l R)
fcinv_cancel_own (lock_fcinv_name γ) p
fcinv N (lock_fcinv_name γ) (lock_inv (lock_excl_name γ) l R))%I.
fcinv_own (lock_fcinv_name γ) p)%I.
Definition locked `{!heapG Σ, !lockG Σ} (γ : lock_name) : ironProp Σ :=
(<affine> own (lock_excl_name γ) (Excl ()) )%I.
......@@ -53,11 +54,11 @@ Section proof.
Global Instance is_lock_fractional γ lk R : Fractional (λ p, is_lock N γ lk p R).
Proof.
intros q1 q2. rewrite /is_lock; iSplit.
- iDestruct 1 as (l ->) "[[H2 H2'] [[H3 H3'] #H4]]".
- iDestruct 1 as (l ->) "(#? & [H2 H2'] & [H3 H3'])".
iSplitL "H2 H3"; iExists _; iFrame; eauto.
- iIntros "[H1 H2]".
iDestruct "H1" as (l ->) "[H1 [H3 #H4]]".
iDestruct "H2" as (l' ->) "[H1' [H3' #H4']]".
iDestruct "H1" as (l ->) "(#? & H3 & H4)".
iDestruct "H2" as (l' ->) "(#? & H3' & H4')".
iExists _; iFrame; eauto.
Qed.
Global Instance is_lock_as_fractional γ lk p R :
......@@ -85,7 +86,7 @@ Section proof.
iIntros (Φ) "HR HΦ". rewrite -iron_wp_fupd /new_lock /=.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (fcinv_alloc _ N (lock_inv γ l R) with "[-HΦ]") as (γinv) "(Hγ & Hγc & #?)".
iMod (fcinv_alloc _ N (lock_inv γ l R) with "[-HΦ]") as (γinv) "(#? & Hγ & Hγc)".
{ iIntros "!>". iExists false. by iFrame. }
iModIntro. iApply ("HΦ" $! #l (LockName γinv γ)). iExists l; iFrame; eauto.
Qed.
......@@ -94,8 +95,8 @@ Section proof.
{{{ is_lock N γ lk p R }}} try_acquire lk
{{{ b, RET #b; is_lock N γ lk p R if b is true then locked γ R else emp }}}.
Proof.
iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (l ->) "(Hγinv & Hγinvc & #?)". wp_lam.
iMod (fcinv_open _ N with "[$] [$]") as "[Hinv Hclose]"; first done.
iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (l ->) "(#? & Hγinvc & Hγinv)". wp_lam.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[>Hl H]".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). iSplit; last done.
......@@ -122,8 +123,8 @@ Section proof.
{{{ RET #(); is_lock N γ lk p R }}}.
Proof.
iIntros (Φ) "(Hlock & Hγ & HR) HΦ".
iDestruct "Hlock" as (l ->) "(Hγinv & Hγinvc & #?)". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "[Hinv Hclose]"; first done.
iDestruct "Hlock" as (l ->) "(#? & Hγinvc & Hγinv)". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[Hl Hinv]".
- wp_store. iMod ("Hclose" with "[HR Hl Hγ]").
{ iNext. iExists false; iFrame. }
......@@ -135,7 +136,7 @@ Section proof.
Lemma free_spec γ lk R `{!Uniform R} :
{{{ is_lock N γ lk 1 R }}} free lk {{{ RET #(); R }}}.
Proof.
iIntros (Φ) "Hlock HΦ". iDestruct "Hlock" as (l ->) "(Hγinv & Hγinvc & #?)".
iIntros (Φ) "Hlock HΦ". iDestruct "Hlock" as (l ->) "(#? & Hγinv & Hγinvc)".
iMod (fcinv_cancel _ N with "[$] [$] [$]") as (b) "[Ht Hinv]"; auto.
iLöb as "IH" forall (b); wp_rec. destruct b.
- wp_load. wp_op. wp_if. by iApply ("IH" with "HΦ Ht").
......
......@@ -99,7 +99,7 @@ Section proof.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc ( None)) as (γ) "Hγ"; first by apply auth_auth_valid.
iMod (fcinv_alloc_named _ N (λ γinv, lock_inv (LockName γinv γ) l R)
with "[-HΦ]") as (γinv) "(Hγ & Hγc & #?)".
with "[-HΦ]") as (γinv) "(#? & Hγc & Hγ)".
{ iIntros "!>" (γinv). iExists false. by iFrame. }
iModIntro. iApply ("HΦ" $! #l (LockName γinv γ)).
iFrame "Hγc". iFrame. iExists l; iFrame; eauto.
......@@ -139,9 +139,9 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & [Hγinv [HC Hγf]] & HR) HΦ".
iDestruct "Hlock" as (l ->) "#?". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "[Hinv Hclose]"; first done.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[Hl Hinv]".
- wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv]".
- wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv']".
iDestruct (own_valid_2 with "Hγ Hγf")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγf") as "Hγ".
......
......@@ -116,7 +116,7 @@ Proof. rewrite fcinv_eq. apply _. Qed.
Lemma fcinv_alloc_strong E N :
(|={E}=> γ, fcinv_own γ 1
P, P ={E}= fcinv_cancel_own γ 1 fcinv N γ P)%I.
P, P ={E}= fcinv N γ P fcinv_cancel_own γ 1)%I.
Proof.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq.
iStartProof (iProp _); iIntros (π1) "Hp".
......@@ -135,7 +135,7 @@ Proof.
iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (F (π1 ? π2 : ufrac))
perm π1 P π2)%I with "[Hγauth Hp HP]"); first by eauto with iFrame.
iModIntro; iSplit; [by rewrite -!cmra_opM_opM_assoc_L /= frac_op' Qp_div_2|].
iExists (Some (π3 / 2)%Qp π2), ε; iSplit; first by rewrite right_id_L.
iExists ε, (Some (π3 / 2)%Qp π2); iSplit; first by rewrite left_id_L.
rewrite Some_op_opM /=. eauto with iFrame.
Qed.
......@@ -143,7 +143,7 @@ Lemma fcinv_open_strong E N γ p P `{!Uniform P} :
N E
fcinv N γ P -
fcinv_own γ p ={E,E∖↑N}=
P fcinv_own γ p ( P fcinv_own γ 1 fcinv_cancel_own γ 1 ={E∖↑N,E}= emp).
P fcinv_own γ p ( P fcinv_cancel_own γ 1 fcinv_own γ 1 ={E∖↑N,E}= emp).
Proof.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _).
iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]"; iIntros (π2) "Hp".
......@@ -171,7 +171,7 @@ Proof.
rewrite -union_difference_L //. iModIntro.
iExists (π6 ? π5), ε; iSplit; first by rewrite left_id_L.
eauto 10 with iFrame.
- iDestruct "Hcancel" as (π7 [π8|] ->) "[[-> Hγinv] Hγ] /="; try done.
- iDestruct "Hcancel" as ([π7|] π8 ->) "[Hγ [-> Hγinv]] /="; try done.
iMod ("Hclose" with "[Hγinv]") as "_"; first by eauto.
rewrite -union_difference_L //. iModIntro.
iDestruct (own_valid_2 with "Hγauth Hγ") as %<-%frac_auth_agreeL.
......@@ -179,7 +179,7 @@ Proof.
Qed.
Lemma fcinv_alloc_named E N Ψ :
( γ, Ψ γ) ={E}= γ, fcinv_own γ 1 fcinv_cancel_own γ 1 fcinv N γ (Ψ γ).
( γ, Ψ γ) ={E}= γ, fcinv N γ (Ψ γ) fcinv_cancel_own γ 1 fcinv_own γ 1.
Proof.
iIntros "HΨ". iMod (fcinv_alloc_strong _ N) as (γ) "[Hγ Halloc]".
iSpecialize ("HΨ" $! γ).
......@@ -187,7 +187,7 @@ Proof.
Qed.
Lemma fcinv_alloc E N P :
P ={E}= γ, fcinv_own γ 1 fcinv_cancel_own γ 1 fcinv N γ P.
P ={E}= γ, fcinv N γ P fcinv_cancel_own γ 1 fcinv_own γ 1.
Proof. iIntros "HP". iApply fcinv_alloc_named; auto. Qed.
Lemma fcinv_cancel E N γ P `{!Uniform P} :
......@@ -204,7 +204,7 @@ Qed.
Lemma fcinv_open E N γ p P `{!Uniform P} :
N E
fcinv N γ P -
fcinv_own γ p ={E,E∖↑N}= P ( P ={E∖↑N,E}= fcinv_own γ p).
fcinv_own γ p ={E,E∖↑N}= P fcinv_own γ p ( P ={E∖↑N,E}= emp).
Proof.
iIntros (?) "#? Hγ".
iMod (fcinv_open_strong with "[$] [$]") as "($ & $ & Hclose)"; 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