From ece2644a6725c22ad9e6740119ed5ab67f728e33 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 28 May 2018 12:06:06 +0200 Subject: [PATCH] Dynamically add resources to AWP This implements - Composable propositions in flock with `flock_res` - Ability to add resources to AWP "on the fly" --- theories/c_translation/monad.v | 41 ++++-- theories/lib/flock.v | 236 ++++++++++++++++++++++++++++----- 2 files changed, 235 insertions(+), 42 deletions(-) diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v index 928f30e..f8fadfc 100644 --- a/theories/c_translation/monad.v +++ b/theories/c_translation/monad.v @@ -65,9 +65,9 @@ Section a_wp. Definition awp (e : expr) (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := - tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (env : val) (l : val) s, + tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (env : val) (l : val), is_flock amonadN γ l -∗ - flock_res γ s (env_inv env ∗ R) -∗ + flock_res γ (env_inv env ∗ R) -∗ unflocked γ π -∗ WP ev env l {{ v, Φ v ∗ unflocked γ π }} }})%I. @@ -102,6 +102,23 @@ Section a_wp_rules. awp (fill K e) R Φ ⊢ WP e {{ v, awp (fill K (of_val v)) R Φ }}. Proof. by apply: wp_bind_inv. Qed. + Lemma awp_insert_res e Φ R1 R2 : + ▷ R1 -∗ + awp e (R1 ∗ R2) Φ -∗ + awp e R2 Φ. + Proof. + iIntros "HR1 Hawp". rewrite /awp /=. + iApply (wp_wand with "Hawp"). + iIntros (v) "HΦ". + iIntros (γ π env l) "#Hflock Hres Hunfl". + iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1") + as "(#Hres & Hunfl)". + iApply ("HΦ" with "Hflock [Hres] Hunfl"). + rewrite (comm (∗)%I R1 R2). + rewrite (assoc (∗)%I _ R2 R1). + by iFrame "Hres". + Qed. + Lemma awp_wand e (Φ Ψ : val → iProp Σ) R : awp e R Φ -∗ (∀ v, Φ v -∗ Ψ v) -∗ @@ -110,7 +127,7 @@ Section a_wp_rules. iIntros "HAWP Hv". rewrite /awp /=. iApply (wp_wand with "HAWP"). iIntros (v) "HΦ". - iIntros (γ π env l s) "#Hflock #Hres Hunfl". + iIntros (γ π env l) "#Hflock #Hres Hunfl". iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ". iIntros (w) "[HΦ $]". by iApply "Hv". Qed. @@ -130,7 +147,7 @@ Section a_wp_rules. Proof. iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp"). iIntros (v) "HΦ". wp_lam. - iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. iFrame. + iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. iFrame. Qed. Lemma awp_bind (f e : expr) R Φ : @@ -140,7 +157,7 @@ Section a_wp_rules. Proof. iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e. iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam. - iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l). + iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l). iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp"). iIntros (v) "H". by iApply ("H" with "[$]"). @@ -152,14 +169,14 @@ Section a_wp_rules. awp (a_atomic e) R Φ. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam. - iIntros (γ π env l s) "#Hlock1 #Hres Hunfl1". do 2 wp_let. + iIntros (γ π env l) "#Hlock1 #Hres Hunfl1". do 2 wp_let. wp_apply (acquire_cancel_spec with "[$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. - iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]". + iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]". 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 (s') "[#Hres2 Hunfl2]". + with "Hlock2 Hunfl2 [$Henv $HR']") as "[#Hres2 Hunfl2]". 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]". @@ -178,7 +195,7 @@ Section a_wp_rules. awp (a_atomic_env e) R Φ. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam. - iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. + iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_apply (acquire_cancel_spec with "[$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. iDestruct ("Hwp" with "Henv HR") as "Hwp". @@ -199,7 +216,7 @@ Section a_wp_rules. Proof. iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ". rewrite /awp /a_par /=. do 2 wp_lam. - iIntros (γ π env l s) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam. + iIntros (γ π env l) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam. iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I (λ v, Ψ2 v ∗ unflocked _ (π/2))%I with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]"). @@ -228,8 +245,8 @@ 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 (s) "[#Hres Hunfl]". - { iNext. iExists ∅, ∅. iFrame. eauto. } + with "Hlock Hunfl [Henv Hσ $HR]") as "[#Hres Hunfl]". + { 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". diff --git a/theories/lib/flock.v b/theories/lib/flock.v index 747f76f..2338a25 100644 --- a/theories/lib/flock.v +++ b/theories/lib/flock.v @@ -71,7 +71,7 @@ Section flock. Definition to_props_map (f : gmap prop_id (iProp Σ)) : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f. - + Lemma to_props_map_insert f i P : to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f). Proof. by rewrite /to_props_map fmap_insert. Qed. @@ -158,16 +158,28 @@ Section flock. (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) ∗ is_lock (flockN .@ "lock") (flock_lock_name γ) lk (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I. - - Definition flock_res (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ := + + Definition flock_res (γ : flock_name) (R : iProp Σ) : iProp Σ := + (∃ f, ⌜R ≡ all_props f⌝ ∧ own (flock_props_name γ) (◯ to_props_map f))%I. + + Definition flock_res_single (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ := (own (flock_props_name γ) (◯ {[ s := to_agree R ]}))%I. Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk). Proof. apply _. Qed. - Global Instance flock_res_persistent γ s R : Persistent (flock_res γ s R). + Global Instance flock_res_persistent γ R : Persistent (flock_res γ R). Proof. apply _. Qed. + Global Instance flock_res_single_persistent γ s R : Persistent (flock_res_single γ s R). + Proof. apply _. Qed. + + Global Instance flock_res_proper : Proper ((=) ==> (≡) ==> (≡)) flock_res. + Proof. + intros ? γ -> P R HPR. rewrite /flock_res. + apply bi.exist_proper=>f. by rewrite HPR. + Qed. + Definition unflocked (γ : flock_name) (q : frac) : iProp Σ := cinv_own (flock_cinv_name γ) q. @@ -188,15 +200,20 @@ Section flock. AsFractional (unflocked γ π) (unflocked γ) π. Proof. split. done. apply _. Qed. - Lemma flock_res_alloc_unflocked γ lk π R : - is_flock γ lk -∗ unflocked γ π -∗ ▷ R ={⊤}=∗ ∃ s, flock_res γ s R ∗ unflocked γ π. + Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R : + is_flock γ lk -∗ unflocked γ π -∗ ▷ R + ={⊤}=∗ ∃ 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. rewrite {2}/flock_inv. iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)". - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)". - pose (s := (fresh (dom (gset prop_id) (fp ∪ fa)))). + pose (s := (fresh ((dom (gset prop_id) (fp ∪ fa)) ∪ X))). + assert (s ∉ (dom (gset prop_id) (fp ∪ fa))) as Hs. + { intros Hs. + apply (elem_of_union_l s (dom (gset prop_id) (fp ∪ fa)) X) in Hs. + revert Hs. apply is_fresh. } iMod (own_update with "Hauth") as "Hauth". { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp ∪ fa)) {[ s := to_agree R ]}). @@ -204,39 +221,88 @@ Section flock. rewrite to_props_map_insert. apply alloc_local_update; last done. apply (not_elem_of_dom (to_props_map (fp ∪ fa)) s (D:=gset prop_id)). - rewrite to_props_map_dom. - apply is_fresh. } + rewrite to_props_map_dom. done. } iDestruct "Hauth" as "[Hauth Hres]". iExists s. iFrame "Hres Hunfl". - iApply ("Hcl" with "[-]"). - iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2". - rewrite /all_props bi.big_sepM_insert. iFrame. - apply (not_elem_of_dom _ s (D:=gset prop_id)). - assert (s ∉ (dom (gset prop_id) (fp ∪ fa))) as Hs. - { apply is_fresh. } - revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. + iMod ("Hcl" with "[-]") as "_". + { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2". + rewrite /all_props bi.big_sepM_insert. iFrame. + apply (not_elem_of_dom _ s (D:=gset prop_id)). + revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. } + iModIntro. iPureIntro. + clear Hs. intros Hs. + apply (elem_of_union_r s (dom (gset prop_id) (fp ∪ fa)) X) in Hs. + revert Hs. apply is_fresh. - iDestruct "Hrest" as "(>Hactive & Hfa & >%)". simplify_eq/=. rewrite left_id. - pose (s := (fresh (dom (gset prop_id) fa))). + pose (s := (fresh (dom (gset prop_id) fa ∪ X))). + assert (s ∉ (dom (gset prop_id) fa)) as Hs. + { intros Hs. + apply (elem_of_union_l s _ X) in Hs. + revert Hs. apply is_fresh. } iMod (own_update with "Hauth") as "Hauth". { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa)) {[ s := to_agree R ]}). rewrite to_props_map_insert. apply alloc_local_update; last done. apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)). - rewrite to_props_map_dom. - apply is_fresh. } + rewrite to_props_map_dom. done. } iDestruct "Hauth" as "[Hauth Hres]". iExists s. iFrame "Hres Hunfl". iMod (own_update_2 _ _ _ ((● Excl' (<[s:=R]>fa)) ⋅ (◯ Excl' (<[s:=R]>fa))) with "Hactive Hfactive") as "[Hactive Hfactive]". { by apply auth_update, option_local_update, exclusive_local_update. } - iApply ("Hcl" with "[-]"). - iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive". - iSplit; auto. - rewrite /all_props bi.big_sepM_insert. iFrame. - apply (not_elem_of_dom _ s (D:=gset prop_id)). - apply is_fresh. + iMod ("Hcl" with "[-]") as "_". + { iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive". + iSplit; auto. + rewrite /all_props bi.big_sepM_insert. iFrame. + by apply (not_elem_of_dom _ s (D:=gset prop_id)). } + iModIntro. iPureIntro. + clear Hs. intros Hs. + apply (elem_of_union_r s (dom (gset prop_id) fa) X) in Hs. + revert Hs. apply is_fresh. + Qed. + + Lemma flock_res_alloc_unflocked γ lk π R : + is_flock γ lk -∗ unflocked γ π -∗ ▷ R ={⊤}=∗ flock_res γ R ∗ unflocked γ π. + Proof. + iIntros "#Hlk Hunfl HR". + iMod (flock_res_single_alloc_unflocked ∅ with "Hlk Hunfl HR") as (s ?) "[HR $]". + iModIntro. iExists {[s := R]}. + rewrite /flock_res_single /to_props_map map_fmap_singleton. iFrame "HR". + iPureIntro. by rewrite /all_props bi.big_sepM_singleton. + Qed. + + Lemma flock_res_insert_unflocked γ lk π P R : + is_flock γ lk -∗ flock_res γ P -∗ unflocked γ π -∗ ▷ R + ={⊤}=∗ flock_res γ (P∗R) ∗ unflocked γ π. + Proof. + 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 $]". + iModIntro. iExists (<[s := R]>f). + rewrite to_props_map_insert /flock_res_single. + iCombine "HR Hf" as "HR". + (* TODO this should be a lemma, somewhere in std++ *) + rewrite /op /cmra_op /= /ucmra_op /= /gmap_op /=. + assert ((merge op {[s := to_agree R]} (to_props_map f)) + = <[s:=to_agree R]> (to_props_map f)) as Hmerge. + { apply map_eq=>i. rewrite lookup_merge. + destruct (decide (s = i)) as [->|?]. + - rewrite lookup_singleton lookup_insert. + rewrite /to_props_map lookup_fmap. + assert (f !! i = None) as ->. + + by rewrite -(not_elem_of_dom (D:=(gset prop_id))). + + simpl. done. + - rewrite lookup_singleton_ne; auto. + rewrite lookup_insert_ne; auto. + remember (to_props_map f !! i) as o. rewrite -Heqo. + by destruct o. } + rewrite Hmerge. iFrame "HR". + iPureIntro. rewrite /all_props bi.big_sepM_insert; last first. + - by apply (not_elem_of_dom (D:=gset prop_id)). + - rewrite comm Hfeq /all_props. reflexivity. Qed. Lemma newlock_cancel_spec : @@ -263,8 +329,100 @@ Section flock. rewrite /is_flock. by iFrame "Hlock". Qed. - Lemma acquire_cancel_spec γ π lk s R : - {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res γ s R }}} + Lemma flock_res_auth γ R fp : + flock_res γ R -∗ + own (flock_props_name γ) (● to_props_map fp) -∗ + ⌜∃ f', all_props fp ⊣⊢ R ∗ all_props f'⌝. + Proof. + rewrite /flock_res. iDestruct 1 as (f Heq) "#Hf". + iIntros "Hauth". + iDestruct (own_valid_2 with "Hauth Hf") + as %[Hfoo _]%auth_valid_discrete. + iPureIntro. revert Hfoo. simpl. rewrite left_id. + rewrite lookup_included. intros Hffp. + exists (fp ∖ f). rewrite Heq /all_props. revert Hffp. + simple refine (map_ind (fun f => (∀ i, _) → _ ≡ _) _ _ f); simpl. + - (* TODO: this should be somewhere in std++ *) + assert (fp ∖ ∅ = fp) as ->. + { apply map_eq=>i. remember (fp !! i) as XX. destruct XX. + - apply lookup_difference_Some. eauto. + - apply lookup_difference_None. eauto. } + by rewrite bi.big_sepM_empty left_id. + - intros i P f' Hi IH Hffp. rewrite IH; last first. + { intros j. specialize (Hffp j). + destruct (decide (i = j)) as [->|?]. + - rewrite /to_props_map !lookup_fmap Hi. simpl. + apply option_included. eauto. + - revert Hffp. + rewrite /to_props_map !lookup_fmap lookup_insert_ne; auto. } + rewrite bi.big_sepM_insert; last assumption. + specialize (Hffp i). revert Hffp. + rewrite /to_props_map !lookup_fmap lookup_insert; auto. simpl. + rewrite option_included. + intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp. + simplify_eq/=. remember (fp !! i) as XX. + destruct XX as [Q|]; simpl in HQ; last first. + { inversion HQ. } + simplify_eq/=. + assert (P ≡ Q) as HPQ. + { by destruct HeqQ as [?%to_agree_inj |?%to_agree_included]. } + clear HeqQ. + assert (fp = <[i:=Q]>(delete i fp)) as ->. + { by rewrite insert_delete insert_id. } + assert (<[i:=Q]> (delete i fp) ∖ f' = <[i:=Q]>((delete i fp) ∖ f')) as ->. + { apply map_eq=>j. destruct (decide (i = j)) as [->|?]. + - by rewrite lookup_insert lookup_difference_Some lookup_insert. + - rewrite lookup_insert_ne; auto. + unfold difference, map_difference; rewrite !lookup_difference_with. + rewrite lookup_insert_ne; auto. } + rewrite bi.big_sepM_insert; last first. + { apply lookup_difference_None. left. apply lookup_delete. } + assert ((<[i:=Q]> (delete i fp) ∖ <[i:=P]> f') = (delete i fp ∖ f')) as ->. + { apply map_eq=>j. destruct (decide (i = j)) as [->|?]. + - unfold difference, map_difference; rewrite !lookup_difference_with. + by rewrite !lookup_insert lookup_delete Hi. + - unfold difference, map_difference; rewrite !lookup_difference_with. + rewrite !lookup_insert_ne; auto. } + iSplit; rewrite {1}HPQ. iIntros "($ & $ & $)". + iIntros "[[$ $] $]". + Qed. + + Lemma acquire_cancel_spec γ π lk R : + {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res γ R }}} + acquire lk + {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}. + Proof. + iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd. + rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)". + iApply (acquire_spec with "Hlk"). iNext. + iIntros "[Hlocked Hunlk]". + iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done. + rewrite {2}/flock_inv. + iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)". + - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)". + iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2"). + - iDestruct "Hrest" as "(>Hactive & Hfa & >%)". + simplify_eq/=. rewrite left_id. + iMod (own_update_2 with "Hstate Hunlk") as "Hstate". + { apply (auth_update _ _ (Excl' (Locked π)) (Excl' (Locked π))). + apply option_local_update. + by apply exclusive_local_update. } + iDestruct "Hstate" as "[Hstate Hflkd]". + iDestruct "Hunfl" as "[Hunfl Hcown]". + iDestruct (flock_res_auth with "HRres Hauth") as %Hfoo. + destruct Hfoo as [f' Hf']. + iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]") as "_". + { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame. + by rewrite /all_props bi.big_sepM_empty. } + iModIntro. rewrite Hf'. iDestruct "Hfa" as "[HR Hf']". + iApply ("HΦ" $! fa). iFrame. + iApply bi.later_wand. iNext. iIntros "HR". + rewrite Hf'. iFrame. + Qed. + + (* TODO: derive this from acquire_cancel_spec *) + Lemma acquire_single_cancel_spec γ π lk s R : + {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res_single γ s R }}} acquire lk {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}. Proof. @@ -301,7 +459,7 @@ Section flock. iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]"). { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame. by rewrite /all_props bi.big_sepM_empty. } - iModIntro. + iModIntro. iApply ("HΦ" $! fa). rewrite -HReq. iFrame. by iApply bi.later_wand. Qed. @@ -355,8 +513,26 @@ Section flock. rewrite /unflocked. by iSplitL "Hcown". Qed. - Lemma cancel_lock γ lk s R : - is_flock γ lk -∗ flock_res γ s R -∗ unflocked γ 1 ={⊤}=∗ ▷ R. + Lemma cancel_lock γ lk R : + is_flock γ lk -∗ flock_res γ R -∗ unflocked γ 1 ={⊤}=∗ ▷ R. + Proof. + rewrite /is_flock /unflocked. + iDestruct 1 as "(#Hcinv & #Hislock)". + iIntros "#Hres Hcown". + iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto. + iIntros "[Hcown Hstate]". + iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)". + - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)". + iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[]. + - iDestruct "Hrest" as "(>Hactive & Hfa & >%)". + simplify_eq/=. iFrame. rewrite left_id. + iDestruct (flock_res_auth with "Hres Hauth") as %Hfoo. + destruct Hfoo as [f' Hf']. + 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. Proof. rewrite /is_flock /unflocked. iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown". -- GitLab