From a95c50916d8cd65c8a91b55d0823c29fbe0447e8 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Tue, 28 Mar 2017 18:15:56 +0200 Subject: [PATCH] Make the steps_ lemma curried in the stack example --- F_mu_ref_conc/examples/counter.v | 41 ++++---- F_mu_ref_conc/examples/lock.v | 36 +++---- F_mu_ref_conc/examples/stack/CG_stack.v | 114 ++++++++++------------ F_mu_ref_conc/examples/stack/refinement.v | 15 ++- 4 files changed, 97 insertions(+), 109 deletions(-) diff --git a/F_mu_ref_conc/examples/counter.v b/F_mu_ref_conc/examples/counter.v index 9748ace..23b7d44 100644 --- a/F_mu_ref_conc/examples/counter.v +++ b/F_mu_ref_conc/examples/counter.v @@ -62,10 +62,11 @@ Section CG_Counter. Lemma steps_CG_increment E ρ j K x n: nclose specN ⊆ E → - spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit) - ⊢ |={E}=> j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (S n)). + spec_ctx ρ -∗ x ↦ₛ (#nv n) + -∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit) + ={E}=∗ j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (S n)). Proof. - iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment. + iIntros (HNE) "#Hspec Hx Hj". unfold CG_increment. tp_rec j. tp_load j. tp_op j. tp_normalise j. @@ -111,16 +112,15 @@ Section CG_Counter. Lemma steps_CG_locked_increment E ρ j K x n l : nclose specN ⊆ E → - spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) + spec_ctx ρ -∗ x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) ={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". - iMod (steps_with_lock _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last by iFrame. - - iIntros (K') "[#Hspec [Hx Hj]]". - iApply steps_CG_increment; first done. iFrame "Hspec Hj Hx"; trivial. - - by iFrame "Hspec Hj Hx". - Unshelve. all: trivial. + iIntros (HNE) "#Hspec Hx Hl Hj". + iMod (steps_with_lock _ _ _ K _ _ _ _ UnitV UnitV _ _ with "Hspec Hx Hl Hj") as "Hj"; last by iFrame. + { iIntros (K') "#Hspec Hx Hj /=". + iApply (steps_CG_increment E with "Hspec Hx"); auto. } + Unshelve. all: trivial. Qed. Global Opaque CG_locked_increment. @@ -150,11 +150,11 @@ Section CG_Counter. Lemma steps_counter_read E ρ j K x n : nclose specN ⊆ E → - spec_ctx ρ ∗ x ↦ₛ (#nv n) - ∗ j ⤇ fill K (App (counter_read (Loc x)) Unit) + spec_ctx ρ -∗ x ↦ₛ (#nv n) + -∗ j ⤇ fill K (App (counter_read (Loc x)) Unit) ={E}=∗ j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n). Proof. - intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read. + intros HNE. iIntros "#Hspec Hx Hj". unfold counter_read. tp_rec j. tp_load j. tp_normalise j. by iFrame. @@ -250,10 +250,8 @@ Section CG_Counter. iClear "HΓ". cbn -[FG_counter CG_counter]. rewrite ?empty_env_subst /CG_counter /FG_counter. iApply fupd_wp. - iMod (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]") - as (l) "[Hj Hl]"; eauto. - { rewrite fill_app /=. by iFrame. } - rewrite fill_app /=. + tp_bind j newlock. + iMod (steps_newlock with "Hspec Hj") as (l) "[Hj Hl]"; eauto. tp_rec j. asimpl. rewrite CG_locked_increment_subst /=. rewrite counter_read_subst /=. @@ -306,9 +304,7 @@ Section CG_Counter. destruct (decide (n = n')) as [|Hneq]; subst. + (* CAS succeeds *) (* In this case, we perform increment in the coarse-grained one *) - iMod (steps_CG_locked_increment - _ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]". - { iFrame "Hspec Hcnt' Hl Hj"; trivial. } + iMod (steps_CG_locked_increment with "Hspec Hcnt' Hl Hj") as "[Hj [Hcnt' Hl]]"; first by solve_ndisj. iApply (wp_cas_suc with "[Hcnt]"); auto. iNext. iIntros "Hcnt". iMod ("Hclose" with "[Hl Hcnt Hcnt']"). @@ -334,13 +330,12 @@ Section CG_Counter. iNext. iApply wp_atomic; eauto. iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose". - iMod (steps_counter_read with "[$Hspec $Hj $Hcnt']") as "[Hj Hcnt']"; first by solve_ndisj. + iMod (steps_counter_read with "Hspec Hcnt' Hj") as "[Hj Hcnt']"; first by solve_ndisj. iApply (wp_load with "[Hcnt]"); eauto. iNext. iIntros "Hcnt". iMod ("Hclose" with "[Hl Hcnt Hcnt']"). { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". } iExists (#nv _); eauto. - Unshelve. all: solve_ndisj. Qed. End CG_Counter. diff --git a/F_mu_ref_conc/examples/lock.v b/F_mu_ref_conc/examples/lock.v index cbf9b0d..cdb735b 100644 --- a/F_mu_ref_conc/examples/lock.v +++ b/F_mu_ref_conc/examples/lock.v @@ -84,10 +84,10 @@ Section proof. Lemma steps_newlock E ρ j K : nclose specN ⊆ E → - spec_ctx ρ ∗ j ⤇ fill K newlock - ⊢ |={E}=> ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ j ⤇ fill K newlock + ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec Hj]". + iIntros (HNE) "#Hspec Hj". tp_alloc j as l "Hl". tp_normalise j. by iExists _; iFrame. Qed. @@ -96,10 +96,10 @@ Section proof. Lemma steps_acquire E ρ j K l : nclose specN ⊆ E → - spec_ctx ρ ∗ l ↦ₛ (#♭v false) ∗ j ⤇ fill K (App acquire (Loc l)) - ⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#♭v true). + spec_ctx ρ -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App acquire (Loc l)) + ={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ (#♭v true). Proof. - iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire. + iIntros (HNE) "#Hspec Hl Hj". unfold acquire. tp_rec j. tp_cas_suc j. tp_if_true j. tp_normalise j. @@ -110,10 +110,10 @@ Section proof. Lemma steps_release E ρ j K l b: nclose specN ⊆ E → - spec_ctx ρ ∗ l ↦ₛ (#♭v b) ∗ j ⤇ fill K (App release (Loc l)) - ⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (Loc l)) + ={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release. + iIntros (HNE) "#Hspec Hl Hj". unfold release. tp_rec j. tp_store j. tp_normalise j. by iFrame. @@ -124,27 +124,27 @@ Section proof. Lemma steps_with_lock E ρ j K e l P Q v w: nclose specN ⊆ E → (∀ f, e.[f] = e) (* e is a closed term *) → - (∀ K', spec_ctx ρ ∗ P ∗ j ⤇ fill K' (App e (of_val w)) - ⊢ |={E}=> j ⤇ fill K' (of_val v) ∗ Q) → - spec_ctx ρ ∗ P ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w)) - ⊢ |={E}=> j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). + (∀ K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w)) + ={E}=∗ j ⤇ fill K' (of_val v) ∗ Q) → + spec_ctx ρ -∗ P -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w)) + ={E}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]". + iIntros (HNE H1 H2) "#Hspec HP Hl Hj". tp_rec j; eauto using to_of_val. asimpl. rewrite H1. (* TODO: a tp_apply tactic similar to that of iApply *) tp_bind j (App acquire (Loc l)). - iMod (steps_acquire _ _ j with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; eauto. + iMod (steps_acquire _ _ j with "Hspec Hl Hj") as "[Hj Hl]"; eauto. tp_rec j. asimpl. rewrite H1. tp_bind j (App e _). - iMod (H2 with "[$Hspec $Hj $HP]") as "[Hj HQ]". + iMod (H2 with "Hspec HP Hj") as "[Hj HQ]". tp_normalise j. tp_rec j; eauto using to_of_val. asimpl. tp_bind j (App release _). - iMod (steps_release with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; auto. + iMod (steps_release with "Hspec Hl Hj") as "[Hj Hl]"; auto. tp_rec j. tp_normalise j. asimpl. by iFrame. diff --git a/F_mu_ref_conc/examples/stack/CG_stack.v b/F_mu_ref_conc/examples/stack/CG_stack.v index 63d685d..4642a07 100644 --- a/F_mu_ref_conc/examples/stack/CG_stack.v +++ b/F_mu_ref_conc/examples/stack/CG_stack.v @@ -98,10 +98,10 @@ Section CG_Stack. Lemma steps_CG_push E ρ j K st v w : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ v ∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w)) - ⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)). + spec_ctx ρ -∗ st ↦ₛ v -∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w)) + ={E}=∗ j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)). Proof. - intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push. + intros HNE. iIntros "#Hspec Hx Hj". unfold CG_push. tp_rec j; eauto using to_of_val. tp_normalise j. tp_load j. tp_normalise j. @@ -144,19 +144,16 @@ Section CG_Stack. Lemma steps_CG_locked_push E ρ j K st w v l : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w)) - ⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ st ↦ₛ v -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w)) + ={E}=∗ j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false). Proof. - iIntros (?) "(#Hspec & Hst & Hl & Hj)". + iIntros (?) "#Hspec Hst Hl Hj". unfold CG_locked_push. (* TODO would be nice to be able to determine that e := Loc l for instance *) - iMod (steps_with_lock _ _ j K (CG_push (Loc st)) l _ _ UnitV _ _ _ with "[Hspec Hst Hj Hl]") as "Hj"; last done. - - iIntros (K') "(#Hspec & HQ & Hj)". - iApply steps_CG_push; first eauto. - iFrame "Hspec Hj". iFrame "HQ". - - by iFrame. - Unshelve. all: trivial. + iMod (steps_with_lock _ _ _ _ _ _ _ _ UnitV with "Hspec Hst Hl Hj") as "Hj"; auto. + iIntros (K') "#Hspec HQ Hj". + iApply (steps_CG_push with "Hspec HQ"); auto. Qed. Global Opaque CG_locked_push. @@ -187,11 +184,11 @@ Section CG_Stack. Lemma steps_CG_pop_suc E ρ j K st v w : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ - j ⤇ fill K (App (CG_pop (Loc st)) Unit) - ⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v. + spec_ctx ρ -∗ st ↦ₛ FoldV (InjRV (PairV w v)) + -∗ j ⤇ fill K (App (CG_pop (Loc st)) Unit) + ={E}=∗ j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v. Proof. - intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop. + intros HNE. iIntros "#Hspec Hx Hj". unfold CG_pop. tp_rec j. asimpl. tp_load j. tp_normalise j. tp_fold j; simpl; first by rewrite ?to_of_val /=. @@ -206,11 +203,11 @@ Section CG_Stack. Lemma steps_CG_pop_fail E ρ j K st : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ - j ⤇ fill K (App (CG_pop (Loc st)) Unit) - ⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV). + spec_ctx ρ -∗ st ↦ₛ FoldV (InjLV UnitV) + -∗ j ⤇ fill K (App (CG_pop (Loc st)) Unit) + ={E}=∗ j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV). Proof. - iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop. + iIntros (HNE) "#Hspec Hx Hj". unfold CG_pop. tp_rec j. tp_load j. asimpl. tp_normalise j. tp_fold j. @@ -253,32 +250,30 @@ Section CG_Stack. Lemma steps_CG_locked_pop_suc E ρ j K st v w l : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) - ⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ st ↦ₛ FoldV (InjRV (PairV w v)) -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) + ={E}=∗ j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop. - iMod (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _ - with "[Hj Hx Hl]") as "Hj"; last done. - - iIntros (K') "[#Hspec [Hx Hj]]". - iApply steps_CG_pop_suc; first done. iFrame "Hspec Hj Hx"; trivial. - - iFrame "Hspec Hj Hx"; trivial. - Unshelve. all: trivial. + iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. + iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV _ _ + with "Hspec Hx Hl Hj") as "Hj"; auto. + iIntros (K') "#Hspec Hx Hj". + iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial. + Unshelve. all: trivial. Qed. Lemma steps_CG_locked_pop_fail E ρ j K st l : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) - ⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ st ↦ₛ FoldV (InjLV UnitV) -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) + ={E}=∗ j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop. - iMod (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _ - with "[Hj Hx Hl]") as "Hj"; last done. - - iIntros (K') "[#Hspec [Hx Hj]] /=". - iApply steps_CG_pop_fail; first done. iFrame "Hspec Hj Hx"; trivial. - - iFrame "Hspec Hj Hx"; trivial. - Unshelve. all: trivial. + iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. + iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV _ _ + with "Hspec Hx Hl Hj") as "Hj"; auto. + iIntros (K') "#Hspec Hx Hj /=". + iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial. + Unshelve. all: trivial. Qed. Global Opaque CG_locked_pop. @@ -316,14 +311,14 @@ Section CG_Stack. Lemma steps_CG_snap E ρ j K st v l : nclose specN ⊆ E → - spec_ctx ρ ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false) - ∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit) - ⊢ |={E}=> j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). + spec_ctx ρ -∗ st ↦ₛ v -∗ l ↦ₛ (#♭v false) + -∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit) + ={E}=∗ j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). Proof. - iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap. + iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_snap. iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _ - with "[Hj Hx Hl]") as "Hj"; last done; [|by iFrame "Hspec Hx Hl Hj"]. - iIntros (K') "[#Hspec [Hx Hj]]". + with "Hspec Hx Hl Hj") as "Hj"; auto. + iIntros (K') "#Hspec Hx Hj". tp_rec j. tp_load j. tp_normalise j. by iFrame. @@ -377,17 +372,16 @@ Section CG_Stack. Lemma steps_CG_iter E ρ j K f v w : nclose specN ⊆ E → spec_ctx ρ - ∗ j ⤇ fill K (App (CG_iter (of_val f)) - (Fold (InjR (Pair (of_val w) (of_val v))))) - ⊢ |={E}=> - j ⤇ fill K - (App - (Rec - (App ((CG_iter (of_val f)).[ren (+2)]) - (Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)])))) - (App (of_val f) (of_val w))). + -∗ j ⤇ fill K (App (CG_iter (of_val f)) + (Fold (InjR (Pair (of_val w) (of_val v))))) + ={E}=∗ j ⤇ fill K + (App + (Rec + (App ((CG_iter (of_val f)).[ren (+2)]) + (Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)])))) + (App (of_val f) (of_val w))). Proof. - iIntros (HNE) "[#Hspec Hj]". unfold CG_iter. + iIntros (HNE) "#Hspec Hj". unfold CG_iter. tp_rec j; first by (rewrite /= ?to_of_val /=). rewrite -CG_iter_folding. Opaque CG_iter. tp_fold j; first by (rewrite /= ?to_of_val /=). @@ -402,10 +396,10 @@ Section CG_Stack. Lemma steps_CG_iter_end E ρ j K f : nclose specN ⊆ E → - spec_ctx ρ ∗ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit))) - ⊢ |={E}=> j ⤇ fill K Unit. + spec_ctx ρ -∗ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit))) + ={E}=∗ j ⤇ fill K Unit. Proof. - iIntros (HNE) "[#Hspec Hj]". unfold CG_iter. + iIntros (HNE) "#Hspec Hj". unfold CG_iter. tp_rec j. tp_fold j. tp_case_inl j. tp_normalise j. diff --git a/F_mu_ref_conc/examples/stack/refinement.v b/F_mu_ref_conc/examples/stack/refinement.v index 587d901..823293c 100644 --- a/F_mu_ref_conc/examples/stack/refinement.v +++ b/F_mu_ref_conc/examples/stack/refinement.v @@ -63,9 +63,8 @@ Section Stack_refinement. end) with (⊤ ∖ ↑stackN) by reflexivity. replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done). tp_bind j (App (CG_snap _ _) ())%E. - iMod (steps_CG_snap with "[$Hs Hst' Hl Hj]") as "(Hj & Hst' & Hl)"; + iMod (steps_CG_snap with "Hs Hst' Hl Hj") as "(Hj & Hst' & Hl)"; first solve_ndisj. - { iFrame "Hst'". iFrame. } tp_normalise j. close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]". @@ -89,7 +88,7 @@ Section Stack_refinement. iNext. iApply fupd_wp. rewrite CG_iter_of_val /=. - iMod (steps_CG_iter_end with "[$Hs $Hj]") as "Hj"; first solve_ndisj. + iMod (steps_CG_iter_end with "Hs Hj") as "Hj"; first solve_ndisj. iModIntro. iApply wp_value; auto. iExists UnitV. iFrame. eauto. @@ -101,7 +100,7 @@ Section Stack_refinement. iNext. iModIntro. wp_bind (App (of_val f1) _). rewrite CG_iter_of_val. - iMod (steps_CG_iter with "[$Hs $Hj]") as "Hj"; first solve_ndisj. + iMod (steps_CG_iter with "Hs Hj") as "Hj"; first solve_ndisj. rewrite CG_iter_subst. tp_bind j (App (of_val f2) _). iSpecialize ("Hff" $! (y1, y2) with "Hy"). @@ -153,7 +152,7 @@ Section Stack_refinement. iInv stackN as (istk2 v h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose". (* TODO : why can we remove the later here?*) destruct (decide (istk = istk2)) as [Heq|Hneq]; first subst istk. * (* Case CAS succeeds *) - iMod (steps_CG_locked_push _ _ j K st' v2 with "[$Hj $Hs $Hst' $Hl]") as "[Hj [Hst' Hl]]"; first solve_ndisj. + iMod (steps_CG_locked_push _ _ j K st' v2 with "Hs Hst' Hl Hj") as "[Hj [Hst' Hl]]"; first solve_ndisj. iApply (wp_cas_suc with "Hst"); auto. iNext. iIntros "Hst". @@ -196,7 +195,7 @@ Section Stack_refinement. (* Checking whether the stack is empty *) rewrite {2}StackLink_unfold. iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=. - + iMod (steps_CG_locked_pop_fail with "[$Hs $Hst' $Hl $Hj]") + + iMod (steps_CG_locked_pop_fail with "Hs Hst' Hl Hj") as "(Hj & Hstk' & Hl)"; first solve_ndisj. close_sinv "Hclose" "[Hoe Hstk' Hst Hl]". wp_bind (Unfold _). iApply wp_fold; first by auto using to_of_val. iNext. @@ -249,7 +248,7 @@ Section Stack_refinement. iDestruct "HLK'" as (yn1 yn2 zn1 zn2) "[% [% [#Hrel HLK'']]]"; simplify_eq/=. (* Now we have proven that specification can also pop. *) - iMod (steps_CG_locked_pop_suc with "[$Hs $Hst' $Hl $Hj]") + iMod (steps_CG_locked_pop_suc with "Hs Hst' Hl Hj") as "[Hj [Hst' Hl]]"; first solve_ndisj. iMod ("Hclose" with "[-Hj]") as "_". { iNext. @@ -297,7 +296,7 @@ Section Stack_refinement. iApply fupd_wp. tp_tlam j. tp_bind j newlock. - iMod (steps_newlock with "[$Hj]") as (l') "[Hj Hl']"; eauto. + iMod (steps_newlock with "Hspec Hj") as (l') "[Hj Hl']"; eauto. tp_normalise j. tp_rec j. tp_alloc j as stk' "Hstk'". -- GitLab