Commit ece2644a by Dan Frumin

### Dynamically add resources to AWP

```This implements
- Composable propositions in flock with `flock_res`
- Ability to add resources to AWP "on the fly"```
parent c24f5451
 ... @@ -65,9 +65,9 @@ Section a_wp. ... @@ -65,9 +65,9 @@ Section a_wp. Definition awp (e : expr) Definition awp (e : expr) (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := (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 -∗ is_flock amonadN γ l -∗ flock_res γ s (env_inv env ∗ R) -∗ flock_res γ (env_inv env ∗ R) -∗ unflocked γ π -∗ unflocked γ π -∗ WP ev env l {{ v, Φ v ∗ unflocked γ π }} WP ev env l {{ v, Φ v ∗ unflocked γ π }} }})%I. }})%I. ... @@ -102,6 +102,23 @@ Section a_wp_rules. ... @@ -102,6 +102,23 @@ Section a_wp_rules. awp (fill K e) R Φ ⊢ WP e {{ v, awp (fill K (of_val v)) R Φ }}. awp (fill K e) R Φ ⊢ WP e {{ v, awp (fill K (of_val v)) R Φ }}. Proof. by apply: wp_bind_inv. Qed. 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 : Lemma awp_wand e (Φ Ψ : val → iProp Σ) R : awp e R Φ -∗ awp e R Φ -∗ (∀ v, Φ v -∗ Ψ v) -∗ (∀ v, Φ v -∗ Ψ v) -∗ ... @@ -110,7 +127,7 @@ Section a_wp_rules. ... @@ -110,7 +127,7 @@ Section a_wp_rules. iIntros "HAWP Hv". rewrite /awp /=. iIntros "HAWP Hv". rewrite /awp /=. iApply (wp_wand with "HAWP"). iApply (wp_wand with "HAWP"). iIntros (v) "HΦ". 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Φ". iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ". iIntros (w) "[HΦ \$]". by iApply "Hv". iIntros (w) "[HΦ \$]". by iApply "Hv". Qed. Qed. ... @@ -130,7 +147,7 @@ Section a_wp_rules. ... @@ -130,7 +147,7 @@ Section a_wp_rules. Proof. Proof. iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp"). iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp"). iIntros (v) "HΦ". wp_lam. 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. Qed. Lemma awp_bind (f e : expr) R Φ : Lemma awp_bind (f e : expr) R Φ : ... @@ -140,7 +157,7 @@ Section a_wp_rules. ... @@ -140,7 +157,7 @@ Section a_wp_rules. Proof. Proof. iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e. 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. 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". iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp"). iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp"). iIntros (v) "H". by iApply ("H" with "[\$]"). iIntros (v) "H". by iApply ("H" with "[\$]"). ... @@ -152,14 +169,14 @@ Section a_wp_rules. ... @@ -152,14 +169,14 @@ Section a_wp_rules. awp (a_atomic e) R Φ. awp (a_atomic e) R Φ. Proof. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam. 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 "[\$]"). wp_apply (acquire_cancel_spec with "[\$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. 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. wp_apply (newlock_cancel_spec amonadN); first done. iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let. iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let. iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R')%I 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' _ _). wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _). iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp". iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp". iIntros (w) "[HR Hunfl2]". iIntros (w) "[HR Hunfl2]". ... @@ -178,7 +195,7 @@ Section a_wp_rules. ... @@ -178,7 +195,7 @@ Section a_wp_rules. awp (a_atomic_env e) R Φ. awp (a_atomic_env e) R Φ. Proof. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam. 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 "[\$]"). wp_apply (acquire_cancel_spec with "[\$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. iIntros (f) "([Henv HR] & Hcl)". wp_seq. iDestruct ("Hwp" with "Henv HR") as "Hwp". iDestruct ("Hwp" with "Henv HR") as "Hwp". ... @@ -199,7 +216,7 @@ Section a_wp_rules. ... @@ -199,7 +216,7 @@ Section a_wp_rules. Proof. Proof. iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ". iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ". rewrite /awp /a_par /=. do 2 wp_lam. 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 iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I (λ v, Ψ2 v ∗ unflocked _ (π/2))%I (λ v, Ψ2 v ∗ unflocked _ (π/2))%I with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]"). with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]"). ... @@ -228,8 +245,8 @@ Section a_wp_run. ... @@ -228,8 +245,8 @@ Section a_wp_run. wp_apply (newlock_cancel_spec amonadN); first done. wp_apply (newlock_cancel_spec amonadN); first done. iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd. iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd. iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R)%I iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R)%I with "Hlock Hunfl [Henv Hσ \$HR]") as (s) "[#Hres Hunfl]". with "Hlock Hunfl [Henv Hσ \$HR]") as "[#Hres Hunfl]". { iNext. iExists ∅, ∅. iFrame. eauto. } { iNext. iExists ∅, ∅. iFrame. eauto. } iSpecialize ("Hwp" \$! amg). iSpecialize ("Hwp" \$! amg). wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp". wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp". iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". ... ...
 ... @@ -71,7 +71,7 @@ Section flock. ... @@ -71,7 +71,7 @@ Section flock. Definition to_props_map (f : gmap prop_id (iProp Σ)) Definition to_props_map (f : gmap prop_id (iProp Σ)) : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <\$> f. : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <\$> f. Lemma to_props_map_insert f i P : Lemma to_props_map_insert f i P : to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f). to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f). Proof. by rewrite /to_props_map fmap_insert. Qed. Proof. by rewrite /to_props_map fmap_insert. Qed. ... @@ -158,16 +158,28 @@ Section flock. ... @@ -158,16 +158,28 @@ Section flock. (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) ∗ (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) ∗ is_lock (flockN .@ "lock") (flock_lock_name γ) lk is_lock (flockN .@ "lock") (flock_lock_name γ) lk (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I. (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. (own (flock_props_name γ) (◯ {[ s := to_agree R ]}))%I. Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk). Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk). Proof. apply _. Qed. 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. 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 Σ := Definition unflocked (γ : flock_name) (q : frac) : iProp Σ := cinv_own (flock_cinv_name γ) q. cinv_own (flock_cinv_name γ) q. ... @@ -188,15 +200,20 @@ Section flock. ... @@ -188,15 +200,20 @@ Section flock. AsFractional (unflocked γ π) (unflocked γ) π. AsFractional (unflocked γ π) (unflocked γ) π. Proof. split. done. apply _. Qed. Proof. split. done. apply _. Qed. Lemma flock_res_alloc_unflocked γ lk π R : Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R : is_flock γ lk -∗ unflocked γ π -∗ ▷ R ={⊤}=∗ ∃ s, flock_res γ s R ∗ unflocked γ π. is_flock γ lk -∗ unflocked γ π -∗ ▷ R ={⊤}=∗ ∃ s, ⌜s ∉ X⌝ ∗ flock_res_single γ s R ∗ unflocked γ π. Proof. Proof. iIntros "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)". iIntros "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)". iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done. iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done. rewrite {2}/flock_inv. rewrite {2}/flock_inv. iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)". iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)". - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)". - 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". iMod (own_update with "Hauth") as "Hauth". { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp ∪ fa)) { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp ∪ fa)) {[ s := to_agree R ]}). {[ s := to_agree R ]}). ... @@ -204,39 +221,88 @@ Section flock. ... @@ -204,39 +221,88 @@ Section flock. rewrite to_props_map_insert. rewrite to_props_map_insert. apply alloc_local_update; last done. apply alloc_local_update; last done. apply (not_elem_of_dom (to_props_map (fp ∪ fa)) s (D:=gset prop_id)). apply (not_elem_of_dom (to_props_map (fp ∪ fa)) s (D:=gset prop_id)). rewrite to_props_map_dom. rewrite to_props_map_dom. done. } apply is_fresh. } iDestruct "Hauth" as "[Hauth Hres]". iDestruct "Hauth" as "[Hauth Hres]". iExists s. iFrame "Hres Hunfl". iExists s. iFrame "Hres Hunfl". iApply ("Hcl" with "[-]"). iMod ("Hcl" with "[-]") as "_". iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2". { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2". rewrite /all_props bi.big_sepM_insert. iFrame. rewrite /all_props bi.big_sepM_insert. iFrame. apply (not_elem_of_dom _ s (D:=gset prop_id)). apply (not_elem_of_dom _ s (D:=gset prop_id)). assert (s ∉ (dom (gset prop_id) (fp ∪ fa))) as Hs. revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. } { apply is_fresh. } iModIntro. iPureIntro. revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. 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 & >%)". - iDestruct "Hrest" as "(>Hactive & Hfa & >%)". simplify_eq/=. rewrite left_id. 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". iMod (own_update with "Hauth") as "Hauth". { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa)) { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa)) {[ s := to_agree R ]}). {[ s := to_agree R ]}). rewrite to_props_map_insert. rewrite to_props_map_insert. apply alloc_local_update; last done. apply alloc_local_update; last done. apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)). apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)). rewrite to_props_map_dom. rewrite to_props_map_dom. done. } apply is_fresh. } iDestruct "Hauth" as "[Hauth Hres]". iDestruct "Hauth" as "[Hauth Hres]". iExists s. iFrame "Hres Hunfl". iExists s. iFrame "Hres Hunfl". iMod (own_update_2 _ _ _ ((● Excl' (<[s:=R]>fa)) ⋅ (◯ Excl' (<[s:=R]>fa))) iMod (own_update_2 _ _ _ ((● Excl' (<[s:=R]>fa)) ⋅ (◯ Excl' (<[s:=R]>fa))) with "Hactive Hfactive") as "[Hactive Hfactive]". with "Hactive Hfactive") as "[Hactive Hfactive]". { by apply auth_update, option_local_update, exclusive_local_update. } { by apply auth_update, option_local_update, exclusive_local_update. } iApply ("Hcl" with "[-]"). iMod ("Hcl" with "[-]") as "_". iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive". { iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive". iSplit; auto. iSplit; auto. rewrite /all_props bi.big_sepM_insert. iFrame. rewrite /all_props bi.big_sepM_insert. iFrame. apply (not_elem_of_dom _ s (D:=gset prop_id)). by apply (not_elem_of_dom _ s (D:=gset prop_id)). } apply is_fresh. 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. Qed. Lemma newlock_cancel_spec : Lemma newlock_cancel_spec : ... @@ -263,8 +329,100 @@ Section flock. ... @@ -263,8 +329,100 @@ Section flock. rewrite /is_flock. by iFrame "Hlock". rewrite /is_flock. by iFrame "Hlock". Qed. Qed. Lemma acquire_cancel_spec γ π lk s R : Lemma flock_res_auth γ R fp : {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res γ s R }}} 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 acquire lk {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}. {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}. Proof. Proof. ... @@ -301,7 +459,7 @@ Section flock. ... @@ -301,7 +459,7 @@ Section flock. iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]"). iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]"). { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame. { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame. by rewrite /all_props bi.big_sepM_empty. } by rewrite /all_props bi.big_sepM_empty. } iModIntro. iModIntro. iApply ("HΦ" \$! fa). rewrite -HReq. iFrame. iApply ("HΦ" \$! fa). rewrite -HReq. iFrame. by iApply bi.later_wand. by iApply bi.later_wand. Qed. Qed. ... @@ -355,8 +513,26 @@ Section flock. ... @@ -355,8 +513,26 @@ Section flock. rewrite /unflocked. by iSplitL "Hcown". rewrite /unflocked. by iSplitL "Hcown". Qed. Qed. Lemma cancel_lock γ lk s R : Lemma cancel_lock γ lk R : is_flock γ lk -∗ flock_res γ s R -∗ unflocked γ 1 ={⊤}=∗ ▷ 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. Proof. rewrite /is_flock /unflocked. rewrite /is_flock /unflocked. iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown". iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown". ... ...
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