Commit 9c4c7f6d authored by Dan Frumin's avatar Dan Frumin

More liberal masks in flock.v

parent b33bd3c2
......@@ -112,7 +112,7 @@ Section a_wp_rules.
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hres Hunfl".
iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1")
as "(#Hres & Hunfl)".
as "(#Hres & Hunfl)"; first done.
iApply ("HΦ" with "Hflock [Hres] Hunfl").
rewrite (comm ()%I R1 R2).
rewrite (assoc ()%I _ R2 R1).
......@@ -176,11 +176,11 @@ Section a_wp_rules.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let.
iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env R')%I
with "Hlock2 Hunfl2 [$Henv $HR']") as "[#Hres2 Hunfl2]".
with "Hlock2 Hunfl2 [$Henv $HR']") as "[#Hres2 Hunfl2]"; first done.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp".
iIntros (w) "[HR Hunfl2]".
iMod (cancel_lock with "Hlock2 Hres2 Hunfl2") as "[Henv HR']".
iMod (cancel_lock with "Hlock2 Hres2 Hunfl2") as "[Henv HR']"; first done.
wp_let.
iDestruct ("HR" with "HR'") as "[HR HΦ]".
wp_apply (release_cancel_spec with "[$Hlock1 Hcl Henv HR]").
......@@ -245,13 +245,14 @@ Section a_wp_run.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env R)%I
with "Hlock Hunfl [Henv Hσ $HR]") as "[#Hres Hunfl]".
with "Hlock Hunfl [Henv Hσ $HR]") as "[#Hres Hunfl]"; first done.
{ iNext. iExists , . iFrame. eauto. }
iSpecialize ("Hwp" $! amg).
wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
iIntros (w) "[HΦ Hunfl]".
iMod (cancel_lock with "Hlock Hres Hunfl") as "[HEnv HR]". by iApply "HΦ".
iMod (cancel_lock with "Hlock Hres Hunfl") as "[HEnv HR]"; first done.
by iApply "HΦ".
Qed.
End a_wp_run.
......
......@@ -224,12 +224,13 @@ Section flock.
AsFractional (unflocked γ π) (unflocked γ) π.
Proof. split. done. apply _. Qed.
Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R :
Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R E :
flockN E
is_flock γ lk - unflocked γ π - R
={}= s, s X flock_res_single γ s R unflocked γ π.
={E}= s, s X flock_res_single γ s R unflocked γ π.
Proof.
iIntros "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
iIntros (?) "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first solve_ndisj.
rewrite {2}/flock_inv.
iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
- iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
......@@ -287,24 +288,28 @@ Section flock.
revert Hs. apply is_fresh.
Qed.
Lemma flock_res_alloc_unflocked γ lk π R :
is_flock γ lk - unflocked γ π - R ={}= flock_res γ R unflocked γ π.
Lemma flock_res_alloc_unflocked γ lk π R E :
flockN E
is_flock γ lk - unflocked γ π - R
={E}= flock_res γ R unflocked γ π.
Proof.
iIntros "#Hlk Hunfl HR".
iMod (flock_res_single_alloc_unflocked with "Hlk Hunfl HR") as (s ?) "[HR $]".
iIntros (?) "#Hlk Hunfl HR".
iMod (flock_res_single_alloc_unflocked with "Hlk Hunfl HR")
as (s ?) "[HR $]"; first done.
iModIntro. iExists {[s := R]}.
rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
iPureIntro. symmetry. apply all_props_singleton.
Qed.
Lemma flock_res_insert_unflocked γ lk π P R :
Lemma flock_res_insert_unflocked γ lk π P R E :
flockN E
is_flock γ lk - flock_res γ P - unflocked γ π - R
={}= flock_res γ (PR) unflocked γ π.
={E}= flock_res γ (PR) unflocked γ π.
Proof.
iIntros "#Hlk #Hres Hunfl HR".
iIntros (?) "#Hlk #Hres Hunfl HR".
iDestruct "Hres" as (f Hfeq) "Hf".
iMod (flock_res_single_alloc_unflocked (dom (gset prop_id) f)
with "Hlk Hunfl HR") as (s Hs) "[HR $]".
with "Hlk Hunfl HR") as (s Hs) "[HR $]"; first done.
iModIntro. iExists (<[s := R]>f).
rewrite to_props_map_insert /flock_res_single.
iCombine "HR Hf" as "HR".
......@@ -507,13 +512,14 @@ Section flock.
rewrite /unflocked. by iSplitL "Hcown".
Qed.
Lemma cancel_lock γ lk R :
is_flock γ lk - flock_res γ R - unflocked γ 1 ={}= R.
Lemma cancel_lock γ lk R E :
flockN E
is_flock γ lk - flock_res γ R - unflocked γ 1 ={E}= R.
Proof.
rewrite /is_flock /unflocked.
rewrite /is_flock /unflocked =>?.
iDestruct 1 as "(#Hcinv & #Hislock)".
iIntros "#Hres Hcown".
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
iIntros "[Hcown Hstate]".
iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
- iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
......@@ -525,13 +531,14 @@ Section flock.
iModIntro. rewrite Hf'. iDestruct "Hfa" as "[$ ?]".
Qed.
Lemma cancel_lock_single γ lk s R :
is_flock γ lk - flock_res_single γ s R - unflocked γ 1 ={}= R.
Lemma cancel_lock_single γ lk s R E :
flockN E
is_flock γ lk - flock_res_single γ s R - unflocked γ 1 ={E}= R.
Proof.
rewrite /is_flock /unflocked.
iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
rewrite /flock_res.
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
iIntros "[Hcown Hstate]".
iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
- iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
......
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