From c958e6ec6030d0c22371c24d387808da597519d0 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 20 Mar 2017 19:57:02 +0100 Subject: [PATCH] [F_mu_ref_conc] simplify the refinement proof for the stack example --- F_mu_ref_conc/examples/stack/refinement.v | 618 +++++++++++---------- F_mu_ref_conc/examples/stack/stack_rules.v | 23 +- F_mu_ref_conc/notation.v | 40 ++ _CoqProject | 1 + 4 files changed, 385 insertions(+), 297 deletions(-) create mode 100644 F_mu_ref_conc/notation.v diff --git a/F_mu_ref_conc/examples/stack/refinement.v b/F_mu_ref_conc/examples/stack/refinement.v index c2fac35..587d901 100644 --- a/F_mu_ref_conc/examples/stack/refinement.v +++ b/F_mu_ref_conc/examples/stack/refinement.v @@ -1,10 +1,9 @@ From iris.algebra Require Import auth. From iris.program_logic Require Import adequacy ectxi_language. -From iris_logrel.F_mu_ref_conc Require Import soundness_binary. +From iris_logrel.F_mu_ref_conc Require Import lang tactics soundness_binary notation. From iris_logrel.F_mu_ref_conc.examples Require Import lock. From iris_logrel.F_mu_ref_conc.examples.stack Require Import CG_stack FG_stack stack_rules. -From iris.proofmode Require Import tactics. Definition stackN : namespace := nroot .@ "stack". @@ -12,7 +11,270 @@ Section Stack_refinement. Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}. Notation D := (prodC valC valC -n> iProp Σ). Implicit Types Δ : listC D. + Import lang. + Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ + := (∃ istk v h, (stack_owns h) + ∗ stk' ↦ₛ v + ∗ stk ↦ᵢ (FoldV (#istk)) + ∗ StackLink τi (#istk, v) + ∗ l' ↦ₛ (#♭v false))%I. + + Ltac close_sinv Hcl asn := + iMod (Hcl with asn) as "_"; + [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro. + + Definition CG_snap_iterV (st l : expr) : val := + RecV (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)). + Definition FG_read_iterV (st : expr) : val := + RecV (App (FG_iter (Var 1)) (Load st.[ren (+2)])). + + + Lemma FG_CG_iter_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}: + spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗ + ⟦ TArrow (TArrow (TVar 0) TUnit) TUnit ⟧ (τi::Δ) (FG_read_iterV (#st)%E, (CG_snap_iterV #st' #l)%E). + Proof. + iIntros "#Hs #Hinv". + iAlways. iIntros ([f1 f2]) "#Hff /=". + iIntros (j K) "Hj /=". + + iApply wp_rec; auto using to_of_val. + iNext. simpl. rewrite FG_iter_subst. simpl. + replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) by (rewrite FG_iter_of_val; done). + wp_bind (Load #st)%E. + iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". + iApply (wp_load with "Hst"). iNext. iIntros "Hst". + tp_rec j; auto using to_of_val. + tp_normalise j. + rewrite CG_iter_subst CG_snap_subst. asimpl. + replace (match @up_close namespace coPset nclose stackN return coPset with + | @exist _ _ t2 _ => + @exist coPset_raw (fun t : coPset_raw => Is_true (coPset_wf t)) + match coPset_opp_raw t2 return coPset_raw with + | coPLeaf b => + match b return coPset_raw with + | true => coPLeaf true + | false => coPLeaf false + end + | coPNode b l0 r => coPNode b l0 r + end + (coPset_intersection_wf (coPLeaf true) + (coPset_opp_raw t2) I (coPset_opp_wf t2)) + 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)"; + first solve_ndisj. + { iFrame "Hst'". iFrame. } + tp_normalise j. + close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]". + + iLöb as "IH" forall (istk v) "HLK". + + iApply wp_rec; auto. iNext. asimpl. + wp_bind (Unfold _). iApply wp_fold; auto. iNext. + iModIntro. wp_bind (Load _). + + clear h. + iInv stackN as (istk2 v' h) "[Hoe [Hst' [Hst [HLK' Hl]]]]" "Hclose". + rewrite StackLink_unfold. + iDestruct "HLK" as (istkl w) "[% [Histk HLK]]". simplify_eq/=. + iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histkl Hoe]". + iApply (wp_load with "Histkl"). iNext. iIntros "Histkl". + iSpecialize ("Hoe" with "Histkl"). + close_sinv "Hclose" "[Hoe Hst Hst' HLK' Hl]". + iDestruct "HLK" as "[[% %]|HLK]"; subst. + + (* the stack is empty *) + iApply wp_case_inl; auto. + iNext. + iApply fupd_wp. + rewrite CG_iter_of_val /=. + iMod (steps_CG_iter_end with "[$Hs $Hj]") as "Hj"; first solve_ndisj. + iModIntro. + iApply wp_value; auto. + iExists UnitV. iFrame. eauto. + + iDestruct "HLK" as (y1 z1 y2 z2) "[% [% [Hy Hsl]]]". subst. + simpl. + iApply wp_case_inr; first by rewrite /= ?to_of_val /=. + iNext. asimpl. + wp_bind (Fst _). iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=). + 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. + rewrite CG_iter_subst. + tp_bind j (App (of_val f2) _). + iSpecialize ("Hff" $! (y1, y2) with "Hy"). + iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl. + iApply (wp_wand with "Hff"). + iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]". + tp_normalise j. asimpl. + iApply fupd_wp. tp_rec j; auto using to_of_val. + asimpl. + rewrite CG_iter_subst. asimpl. + replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) + by (by rewrite CG_iter_of_val). + tp_snd j; auto using to_of_val. + tp_normalise j. + iModIntro. + iPoseProof "Hsl" as "Hsl'". + rewrite {2}StackLink_unfold. + iDestruct "Hsl'" as (zl w') "[% [Hzl Hsl']]". simplify_eq/=. + iSpecialize ("IH" $! zl z2). + iPoseProof (persistentP ((StackLink τi) (#zl, z2)) with "Hsl") as "Hsl_box". + iSpecialize ("IH" with "Hsl_box"). + iSpecialize ("IH" with "Hj"). + iApply wp_rec; auto. iNext. asimpl. + wp_bind (Snd _). iApply wp_snd; auto using to_of_val. + Qed. + + Lemma FG_CG_push_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}: + spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗ + ⟦ TArrow (TVar 0) TUnit ⟧ (τi::Δ) (FG_pushV (#st)%E, (CG_locked_pushV #st' #l)%E). + Proof. + iIntros "#Hs #Hinv". + iAlways. iIntros ([v1 v2]) "#Hvv". + iIntros (j K) "Hj /=". + rewrite CG_locked_push_of_val. + iLöb as "IH". + iApply wp_rec; eauto using to_of_val. iNext. + asimpl. + wp_bind (Load #st)%E. + iApply wp_atomic; eauto. + iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose". + iModIntro. iApply (wp_load _ st 1 (FoldV #istk) with "Hst"). iNext. + iIntros "Hst". + close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". + iApply wp_rec; eauto using to_of_val. iNext. asimpl. + wp_bind (ref (InjR _))%E. + iApply wp_alloc. + { simpl. rewrite ?to_of_val /=. auto. } iNext. iIntros (istk') "Histk'". + wp_bind (CAS _ _ _). clear v h. + 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. + iApply (wp_cas_suc with "Hst"); auto. + iNext. iIntros "Hst". + + iMod (stack_owns_alloc with "[$Hoe $Histk']") as "[Hoe Histk']". + iMod ("Hclose" with "[HLK Hst Hoe Hl Hst' Histk']"). + { iNext. rewrite /sinv. iExists _,_,_. + iFrame. + rewrite (StackLink_unfold _ ((LocV istk'), _)). + iExists _, _. iSplitR; auto. + iFrame "Histk'". + iRight. iExists _, _, _, _. auto. + } + iModIntro. iApply wp_if_true. iNext. + iApply wp_value; eauto. iExists _; iSplitL; auto; simpl. + done. + * (* Case CAS fails *) + iApply (wp_cas_fail with "Hst"); auto. + congruence. iNext. iIntros "Hst". + close_sinv "Hclose" "[HLK Hst Hoe Hl Hst' Histk']". + iApply wp_if_false. iNext. + iApply "IH". iFrame. + Qed. + + Lemma FG_CG_pop_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}: + spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗ + ⟦ TArrow TUnit (TSum TUnit (TVar 0)) ⟧ (τi::Δ) (FG_popV (#st)%E, (CG_locked_popV #st' #l)%E). + Proof. + iIntros "#Hs #Hinv". + iAlways. iIntros ( [v1 v2] ) "[% %]". subst. + iIntros (j K) "Hj /="; simplify_eq/=. + rewrite CG_locked_pop_of_val FG_pop_of_val. + iLöb as "IH". + rewrite {2}(FG_pop_folding). + iApply wp_rec; first by auto using to_of_val. iNext. + rewrite -(FG_pop_folding #st)%E. asimpl. + wp_bind (Load _). + iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". + iApply (wp_load with "Hst"). iNext. iIntros "Hst". + iPoseProof "HLK" as "HLK'". + (* 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]") + 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. + iModIntro. iApply wp_rec; first auto using to_of_val. iNext. asimpl. + clear h. + wp_bind (Load _). iClear "HLK". + iInv stackN as (istk3 w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". + iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]". + iApply (wp_load with "Histk"). iNext. iIntros "Histk". + iSpecialize ("HLoe" with "Histk"). + close_sinv "Hclose" "[HLoe Hst' Hst HLK Hl]". + iApply wp_rec; first by auto. iNext. asimpl. + iApply wp_case_inl; auto. iNext. + iApply wp_value; auto. + iExists (InjLV ())%V. iFrame "Hj". + iLeft. iExists (_,_). iSplit; auto. + + close_sinv "Hclose" "[Hoe Hst' Hst Hl]". + wp_bind (Unfold _). iApply wp_fold; first auto. iNext. + iApply wp_rec; first auto. iNext. asimpl. + wp_bind (Load _). + clear h. + iClear "HLK". + iInv stackN as (istk3 w' h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose". + iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]". + iApply (wp_load with "Histk"). iNext; iIntros "Histk". + iSpecialize ("HLoe" with "Histk"). + close_sinv "Hclose" "[HLoe Hl Hst Hst' HLK]". + iApply wp_rec; first auto using to_of_val. iNext. asimpl. + iDestruct "HLK'" as (y1 z1 y2 z2) "(% & % & Hτ & HLK2)"; subst. + simpl. + iApply wp_case_inr. + { by rewrite /= ?to_of_val /=. } iNext. + asimpl. + wp_bind (Snd _). + iApply wp_snd; try by (rewrite /= to_of_val /=). iNext. + (* now to decide if CAS succeeds or not *) + iClear "HLK2". clear h. iModIntro. + wp_bind (CAS _ _ _). + iInv stackN as (istk w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". + (* deciding whether CAS will succeed or fail *) + destruct (decide (istk = istk2)) as [Heq|Hneq]; subst. + * (* CAS successful *) + iApply (wp_cas_suc with "Hst"); try by (rewrite /= ?to_of_val /=). + iNext. iIntros "Hst". + iPoseProof "HLK" as "HLK'". + rewrite {2}StackLink_unfold. + iDestruct "HLK'" as (? ?) "[% [Hmpt' HLK']]"; simplify_eq/=. + iDestruct (stack_mapstos_agree with "[$Hmpt $Hmpt']") as "%". subst. + iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=. + 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]") + as "[Hj [Hst' Hl]]"; first solve_ndisj. + iMod ("Hclose" with "[-Hj]") as "_". + { iNext. + iPoseProof "HLK''" as "HLK2". + rewrite {2}(StackLink_unfold _ (yn2, zn2)). + iDestruct "HLK2" as (yn2loc ?) "[% _]"; simplify_eq /=. + iExists _,_,_. iFrame. iFrame "HLK''". } + iModIntro. + iApply wp_if_true. iNext. + wp_bind (Fst _). + iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=). iNext. + iModIntro. + iApply wp_value; try by rewrite /= ?to_of_val /=. + iExists (InjRV zn1). iFrame "Hj". + iRight. iExists (_,_). simpl. iSplit; auto. + * (* CAS fails *) + iApply (wp_cas_fail with "Hst"); try by (rewrite /= ?to_of_val /=). + congruence. + iNext. iIntros "Hst". + close_sinv "Hclose" "[-Hj]". + iApply wp_if_false. iNext. + by iApply "IH". + Qed. + + (* ∀ α. (α → Unit) * (Unit → Unit + α) * ((α → Unit) → Unit) *) Lemma FG_CG_counter_refinement : [] ⊨ FG_stack ≤log≤ CG_stack : TForall (TProd (TProd (TArrow (TVar 0) TUnit) @@ -22,36 +284,36 @@ Section Stack_refinement. (* executing the preambles *) iIntros (Δ [|??] ρ ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first. { iDestruct (interp_env_length with "HΓ") as %[=]. } - iClear "HΓ". cbn -[FG_stack CG_stack]. - rewrite ?empty_env_subst /CG_stack /FG_stack. + iClear "HΓ". cbn -[FG_stack CG_stack]. + rewrite ?empty_env_subst /CG_stack /FG_stack. iApply wp_value; eauto. - iExists (TLamV _); iFrame "Hj". - clear j K. iAlways. iIntros (τi) "%". iIntros (j K) "Hj /=". - iMod (step_tlam _ _ j K with "[Hj]") as "Hj"; eauto. - iApply wp_tlam; iNext. - iMod (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) with "[Hj]") - as (l) "[Hj Hl]"; eauto. - { rewrite fill_app; simpl. iFrame "Hspec Hj"; trivial. } - rewrite fill_app; simpl. - iMod (step_rec _ _ j K with "[$Hj]") as "Hj"; eauto. - simpl. - rewrite CG_locked_push_subst CG_locked_pop_subst - CG_iter_subst CG_snap_subst. simpl. asimpl. - iMod (step_alloc _ _ j (K ++ [AppRCtx (RecV _)]) with "[Hj]") - as (stk') "[Hj Hstk']"; [| |rewrite fill_app; simpl; by iFrame|]; auto. - rewrite fill_app; simpl. - iMod (step_rec _ _ j K with "[$Hj]") as "Hj"; eauto. - simpl. + iExists (Λ: _)%V; iFrame "Hj". + fold (interp (TProd (TProd + (TArrow (TVar 0) TUnit) + (TArrow TUnit (TSum TUnit (TVar 0)))) + (TArrow (TArrow (TVar 0) TUnit) TUnit))). + clear j K. iAlways. iIntros (τi) "%". + iIntros (j K) "Hj /=". + iApply fupd_wp. + tp_tlam j. + tp_bind j newlock. + iMod (steps_newlock with "[$Hj]") as (l') "[Hj Hl']"; eauto. + tp_normalise j. + tp_rec j. + tp_alloc j as stk' "Hstk'". rewrite CG_locked_push_subst CG_locked_pop_subst CG_iter_subst CG_snap_subst. simpl. asimpl. - iApply (wp_bind [AppRCtx (RecV _); AllocCtx; FoldCtx]); - iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. - iApply wp_alloc; first done. iNext; iIntros (istk) "Histk". - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. - iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk". - simpl. iApply wp_rec; trivial. iNext. simpl. - rewrite FG_push_subst FG_pop_subst FG_iter_subst. simpl. asimpl. + tp_normalise j. + tp_rec j. + tp_normalise j. rewrite ?CG_locked_push_subst ?CG_locked_pop_subst + ?CG_iter_subst ?CG_snap_subst. simpl. asimpl. + iApply wp_tlam. iNext. + wp_bind (ref (InjL _))%E. iApply wp_alloc; eauto. iNext. iIntros (l) "Hl". + wp_bind (ref _)%E. iApply wp_alloc; eauto. iNext. iIntros (stk) "Hstk". + iApply wp_rec; eauto. iNext. + simpl. rewrite FG_push_subst FG_pop_subst FG_iter_subst /=. + asimpl. + (* establishing the invariant *) iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done. set (istkG := StackG _ _ γ). @@ -59,276 +321,54 @@ Section Stack_refinement. change H1 with (@stack_inG _ istkG). clearbody istkG. clear γ H1. iAssert (@stack_owns _ istkG _ ∅) with "[Hemp]" as "Hoe". - { rewrite /stack_owns big_sepM_empty. iFrame "Hemp"; trivial. } - iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe Hls]". - iAssert (StackLink τi (LocV istk, FoldV (InjLV UnitV))) with "[Hls]" as "HLK". + { rewrite /stack_owns big_sepM_empty. eauto. } + iMod (stack_owns_alloc with "[$Hoe $Hl]") as "[Hoe Hls]". + iAssert (StackLink τi (#l, FoldV (InjLV UnitV))) with "[Hls]" as "HLK". { rewrite StackLink_unfold. iExists _, _. iSplitR; simpl; trivial. iFrame "Hls". iLeft. iSplit; trivial. } - iAssert ((∃ istk v h, (stack_owns h) - ∗ stk' ↦ₛ v - ∗ stk ↦ᵢ (FoldV (LocV istk)) - ∗ StackLink τi (LocV istk, v) - ∗ l ↦ₛ (#♭v false) - )%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv". - { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". } - iMod (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial. - { iNext; iExact "Hinv". } - clear istk. + iAssert (sinv τi stk stk' l') with "[Hoe Hstk Hstk' HLK Hl']" as "Hinv". + { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl' HLK". } + iMod (inv_alloc stackN with "[$Hinv]") as "#Hinv". + clear l. Opaque stack_owns. + (* splitting *) - iApply wp_value; simpl; trivial. + iApply wp_value; first by eauto. iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)). - simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj". + simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj". iExists (_, _), (_, _); iSplit; eauto. iSplit. (* refinement of push and pop *) - iExists (_, _), (_, _); iSplit; eauto. iSplit. - + (* refinement of push *) - iAlways. clear j K. iIntros ( [v1 v2] ) "#Hrel". iIntros (j K) "Hj /=". - rewrite -(FG_push_folding (Loc stk)). - iLöb as "Hlat". - rewrite {2}(FG_push_folding (Loc stk)). - iApply wp_rec; auto using to_of_val. - iNext. - rewrite -(FG_push_folding (Loc stk)). - asimpl. - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. - iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". - iApply (wp_load with "Hstk"). iNext. iIntros "Hstk". - iMod ("Hclose" with "[Hoe Hstk' HLK Hl Hstk]") as "_". - { iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk". } - clear v h. - iApply wp_rec; auto using to_of_val. - iNext. asimpl. - iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _)); - FoldCtx]); - iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - iApply wp_alloc; simpl; trivial; [by rewrite to_of_val|]. - iNext. iIntros (ltmp) "Hltmp". - iApply (wp_bind [IfCtx _ _]); - iApply wp_wand_l; iSplitR; [by iIntros (w) "$"|]. - iInv stackN as (istk2 v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". - (* deciding whether CAS will succeed or fail *) - destruct (decide (istk = istk2)) as [|Hneq]; subst. - * (* CAS succeeds *) - (* In this case, the specification pushes *) - iMod "Hstk'". iMod "Hl". - iMod (steps_CG_locked_push _ _ j K with "[Hj Hl Hstk']") - as "[Hj [Hstk' Hl]]"; first solve_ndisj. - { rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". } - iApply (wp_cas_suc with "Hstk"); auto. - iNext. iIntros "Hstk". - iMod ("Hclose" with ">[-Hj]") as "_". - { iMod (stack_owns_alloc with "[$Hoe $Hltmp]") as "[Hoe Hpt]". - iModIntro. iNext. iExists ltmp, _, _. - iFrame "Hoe Hstk' Hstk Hl". - do 2 rewrite StackLink_unfold. - rewrite -StackLink_unfold. - iExists _, _. iSplit; trivial. - iFrame "Hpt". eauto 10. } - iModIntro. - iApply wp_if_true. iNext; iApply wp_value; trivial. - iExists UnitV; eauto. - * iApply (wp_cas_fail with "Hstk"); auto. congruence. - iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]"). - { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". } - iApply wp_if_false. iNext. by iApply "Hlat". - + (* refinement of pop *) - iAlways. clear j K. iIntros ( [v1 v2] ) "[% %]". - iIntros (j K) "Hj /="; simplify_eq/=. - rewrite -(FG_pop_folding (Loc stk)). - iLöb as "Hlat". - rewrite {2}(FG_pop_folding (Loc stk)). - iApply wp_rec; auto using to_of_val. - iNext. - rewrite -(FG_pop_folding (Loc stk)). - asimpl. - iApply (wp_bind [AppRCtx (RecV _); UnfoldCtx]); - iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. - iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose". - iApply (wp_load with "Hstk"). iNext. iIntros "Hstk". - iPoseProof "HLK" as "HLK'". - (* Checking whether the stack is empty *) - rewrite {2}StackLink_unfold. - iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=. - * (* The stack is empty *) - iMod (steps_CG_locked_pop_fail with "[$Hspec $Hstk' $Hl $Hj]") - as "[Hj [Hstk' Hl]]"; first solve_ndisj. - iMod ("Hclose" with "[-Hj Hmpt]") as "_". - { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". } - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - iApply wp_fold; simpl; auto using to_of_val. - iNext. iModIntro. iApply wp_rec; auto using to_of_val. iNext. asimpl. - clear h. - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - iClear "HLK". - iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". - iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]". - iApply (wp_load with "Histk"). - iNext. iIntros "Histk". iMod ("Hclose" with "[-Hj]") as "_". - { iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl". - by iApply "HLoe". } - iApply wp_rec; simpl; trivial. - iNext. asimpl. - iApply wp_case_inl; trivial. - iNext. iApply wp_value; simpl; trivial. iExists (InjLV UnitV). - iSplit; trivial. iLeft. iExists (_, _); repeat iSplit; simpl; trivial. - * (* The stack is not empty *) - iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_". - { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". } - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. - iApply wp_fold; simpl; auto using to_of_val. - iNext. iApply wp_rec; auto using to_of_val. iNext. asimpl. - clear h. - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. - iClear "HLK". - iInv stackN as (istk3 w' h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". - iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]". - iApply (wp_load with "Histk"). iNext; iIntros "Histk". - iDestruct ("HLoe" with "Histk") as "Hh". - iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_". - { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". } - iApply wp_rec; auto using to_of_val. - iNext. asimpl. - iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl. - iApply wp_case_inr; [simpl; by rewrite ?to_of_val |]. - iNext. - iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _))]); - iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - asimpl. iApply wp_snd; [simpl; by rewrite ?to_of_val | - simpl; by rewrite ?to_of_val |]. - simpl. iNext. iModIntro. - iApply (wp_bind [IfCtx _ _]); - iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - clear istk3 h. asimpl. - iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose". - (* deciding whether CAS will succeed or fail *) - destruct (decide (istk2 = istk3)) as [|Hneq]; subst. - -- (* CAS succeeds *) - (* In this case, the specification pushes *) - iApply (wp_cas_suc with "Hstk"); simpl; auto. by rewrite to_of_val. - iNext. iIntros "Hstk {HLK'}". iPoseProof "HLK" as "HLK'". - rewrite {2}StackLink_unfold. - iDestruct "HLK'" as (istk4 w2) "[% [Hmpt' HLK']]"; simplify_eq/=. - iDestruct (stack_mapstos_agree with "[$Hmpt $Hmpt']") as %?. - iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=. - iDestruct "HLK'" as (yn1 yn2 zn1 zn2) - "[% [% [#Hrel HLK'']]]"; simplify_eq/=. - (* Now we have proven that specification can also pop. *) - rewrite CG_locked_pop_of_val. - iMod (steps_CG_locked_pop_suc with "[$Hspec $Hstk' $Hl $Hj]") - as "[Hj [Hstk' Hl]]"; first solve_ndisj. - iMod ("Hclose" with "[-Hj]") as "_". - { iNext. iIntros "{Hmpt Hmpt' HLK}". rewrite StackLink_unfold. - iDestruct "HLK''" as (istk5 w2) "[% [Hmpt HLK]]"; simplify_eq/=. - iExists istk5, _, _. iFrame "Hoe Hstk' Hstk Hl". - rewrite StackLink_unfold. - iExists _, _; iSplitR; trivial. - by iFrame "HLK". } - iApply wp_if_true. iNext. - iApply (wp_bind [InjRCtx]); iApply wp_wand_l; - iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - iApply wp_fst; [simpl; by rewrite ?to_of_val | - simpl; by rewrite ?to_of_val |]. - iNext. iModIntro. iApply wp_value; simpl. - { by rewrite to_of_val. } - iExists (InjRV _); iFrame "Hj". - iRight. iExists (_, _). iSplit; trivial. - -- (* CAS will fail *) - iApply (wp_cas_fail with "Hstk"); [rewrite /= ?to_of_val //; congruence..|]. - iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]") as "_". - { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". } - iApply wp_if_false. iNext. by iApply "Hlat". - - (* refinement of iter *) - iAlways. clear j K. iIntros ( [f1 f2] ) "/= #Hfs". iIntros (j K) "Hj". - iApply wp_rec; auto using to_of_val. iNext. - iMod (step_rec with "[$Hspec $Hj]") as "Hj"; [by rewrite to_of_val|solve_ndisj|]. - asimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. asimpl. - replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) - by (by rewrite FG_iter_of_val). - replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) - by (by rewrite CG_iter_of_val). - iApply (wp_bind [AppRCtx _]); iApply wp_wand_l; - iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. - iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose". - iMod (steps_CG_snap _ _ _ (K ++ [AppRCtx _]) - with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]"; first solve_ndisj. - { rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". } - iApply (wp_load with "[$Hstk]"). iNext. iIntros "Hstk". - iMod ("Hclose" with "[-Hj]") as "_". - { iNext. iExists _, _, _; by iFrame "Hoe Hstk' Hstk HLK Hl". } - clear h. - rewrite ?fill_app /= -FG_iter_folding. - iLöb as "Hlat" forall (istk3 w) "HLK". - rewrite {2}FG_iter_folding. - iApply wp_rec; simpl; trivial. - rewrite -FG_iter_folding. asimpl. rewrite FG_iter_subst. - iNext. - iApply (wp_bind [CaseCtx _ _; LoadCtx]); iApply wp_wand_l; - iSplitR; [iIntros (v) "Hw"; iExact "Hw"|]. - iApply wp_fold; simpl; trivial. - iNext. iModIntro. simpl. - iApply (wp_bind [CaseCtx _ _]); iApply wp_wand_l; - iSplitR; [iIntros (v) "Hw"; iExact "Hw"|]. - rewrite StackLink_unfold. - iDestruct "HLK" as (istk4 v) "[% [Hmpt HLK]]"; simplify_eq/=. - iInv stackN as (istk5 v' h) "[Hoe [Hstk' [Hstk [HLK' Hl]]]]" "Hclose". - iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]". - iApply (wp_load with "[$Histk]"). iNext. iIntros "Histk". - iDestruct ("HLoe" with "Histk") as "Hh". - iDestruct "HLK" as "[[% %]|HLK'']"; simplify_eq/=. - * rewrite CG_iter_of_val. - iMod (steps_CG_iter_end with "[$Hspec $Hj]") as "Hj"; first solve_ndisj. - iMod ("Hclose" with "[-Hj]"). - { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk Hl". } - iApply wp_case_inl; trivial. - iNext. iApply wp_value; trivial. iExists UnitV; eauto. - * iDestruct "HLK''" as (yn1 yn2 zn1 zn2) - "[% [% [#Hrel HLK'']]]"; simplify_eq/=. - rewrite CG_iter_of_val. - iMod (steps_CG_iter with "[$Hspec $Hj]") as "Hj"; first solve_ndisj. - iMod ("Hclose" with "[-Hj HLK'']"). - { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk Hl". } - simpl. - iApply wp_case_inr; simpl; rewrite ?to_of_val; trivial. - rewrite FG_iter_subst CG_iter_subst. asimpl. - iNext. - iApply (wp_bind [AppRCtx (RecV _); AppRCtx _]); - iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. - iApply wp_fst; simpl; rewrite ?to_of_val; trivial. iNext. iModIntro. - iApply (wp_bind [AppRCtx (RecV _)]); - iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. - rewrite StackLink_unfold. - iDestruct "HLK''" as (istk6 w') "[% HLK]"; simplify_eq/=. - iSpecialize ("Hfs" $! (yn1, zn1) with "Hrel"). - iSpecialize ("Hfs" $! _ (K ++ [AppRCtx (RecV _)])). - rewrite fill_app; simpl. - iApply wp_wand_l; iSplitR "Hj"; [|iApply "Hfs"; by iFrame "Hj"]. - iIntros (u) "/="; iDestruct 1 as (z) "[Hj [% %]]". - rewrite fill_app; simpl. subst. asimpl. - iMod (step_rec with "[$Hspec $Hj]") as "Hj"; [done..|]. - asimpl. rewrite CG_iter_subst. asimpl. - replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) - by (by rewrite CG_iter_of_val). - iMod (step_snd _ _ _ (K ++ [AppRCtx _]) with "[$Hspec Hj]") as "Hj"; - [| | |rewrite fill_app; simpl; by iFrame "Hj"|]; rewrite ?to_of_val; auto. - rewrite fill_app. - iApply wp_rec; simpl; trivial. - iNext. rewrite FG_iter_subst. asimpl. - replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) - by (by rewrite FG_iter_of_val). - iApply (wp_bind [AppRCtx _]); - iApply wp_wand_l; iSplitR; [iIntros (w'') "Hw"; iExact "Hw"|]. - iApply wp_snd; auto using to_of_val. - simpl. iNext. rewrite -FG_iter_folding. - iApply ("Hlat" $! istk6 zn2 with "[HLK] [Hj]"); trivial. - rewrite StackLink_unfold; iAlways; eauto 10. + + simpl. + (* TODO: fold (interp (...)) does not work here *) + replace (□ (∀ vv : prodC valC valC, τi vv + → interp_expr interp_unit (τi :: Δ) + ((of_val + ((RecV + ((rec: if: CAS #stk (Var 1) + (Fold (ref InjR (Var 3, Var 1))) then + () else (Var 2) (Var 3))%E + (! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).1)) + (of_val (vv.1)), + (of_val + ((RecV + ((rec: if: CAS #stk (Var 1) + (Fold (ref InjR (Var 3, Var 1))) then + () else (Var 2) (Var 3))%E + (! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).2)) + (of_val (vv.2)))))%I + with + (interp (TArrow (TVar 0) TUnit) (τi :: Δ) + ((FG_pushV (#stk)%E)%V, + (CG_locked_pushV (#stk')%E (#l')%E))); last first. + { simpl. unlock. (* TODO: WTF???? *) auto. } + iApply (FG_CG_push_refinement with "Hspec Hinv"). + + simpl. + iApply (FG_CG_pop_refinement with "Hspec Hinv"). + - iApply (FG_CG_iter_refinement _ _ _ _ _ Δ with "Hspec Hinv"). + Unshelve. auto. (* TODO why is this goal coming up anyway? *) Qed. End Stack_refinement. diff --git a/F_mu_ref_conc/examples/stack/stack_rules.v b/F_mu_ref_conc/examples/stack/stack_rules.v index 316c589..54fa310 100644 --- a/F_mu_ref_conc/examples/stack/stack_rules.v +++ b/F_mu_ref_conc/examples/stack/stack_rules.v @@ -28,6 +28,10 @@ Section Rules. by iIntros ([=]%auth_own_valid%singleton_valid%dec_agree_op_inv). Qed. + (* stacklink Q := {((Loc l), nil) ∣ l ↦ˢᵗᵏ (InjL #()) } + ∪ {((Loc l), cons y2 z2) ∣ ∃ y1 z1, l ↦ˢᵗᵏ (y1, z1) + ∗ (y1, y2) ∈ Q + ∗ ▷ stacklink Q (z1, z2) }*) Program Definition StackLink_pre (Q : D) : D -n> D := λne P v, (∃ l w, ⌜v.1 = LocV l⌝ ∗ l ↦ˢᵗᵏ w ∗ ((⌜w = InjLV UnitV⌝ ∧ ⌜v.2 = FoldV (InjLV UnitV)⌝) ∨ @@ -46,20 +50,23 @@ Section Rules. ((⌜w = InjLV UnitV⌝ ∧ ⌜v.2 = FoldV (InjLV UnitV)⌝) ∨ (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝ ∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ - ∗ Q (y1, y2) ∗ ▷ @StackLink Q (z1, z2))))%I. + ∗ Q (y1, y2) ∗ ▷ StackLink Q (z1, z2))))%I. Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed. Global Opaque StackLink. (* So that we can only use the unfold above. *) Global Instance StackLink_persistent (Q : D) v `{∀ vw, PersistentP (Q vw)} : PersistentP (StackLink Q v). - Proof. + Proof. iIntros "H". iLöb as "IH" forall (v). rewrite StackLink_unfold. - iDestruct "H" as (l w) "[% [#Hl [#Hr|Hr]]]"; subst. - { iExists l, w; iAlways; eauto. } - iDestruct "Hr" as (y1 z1 y2 z2) "[#H1 [#H2 [#HQ H']]]". - rewrite later_forall. iDestruct ("IH" with "* H'") as "#H''". iClear "H'". - iAlways. eauto 20. + iDestruct "H" as (l w) "[% [#Hl [[% %]|Hr]]]"; subst. + { iExists l, _; iAlways; eauto. } + iDestruct "Hr" as (y1 z1 y2 z2) "[% [% [#HQ Hrec]]]"; subst. + rewrite later_forall. + iSpecialize ("IH" $! (z1, z2)). rewrite later_wand. + iSpecialize ("IH" with "Hrec"). rewrite -always_later. + iDestruct "IH" as "#IH". + iAlways. iExists _,_; eauto 20. Qed. Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) : @@ -79,7 +86,7 @@ Section Rules. stack_owns h ∗ l ↦ᵢ v ==∗ stack_owns (<[l := DecAgree v]> h) ∗ l ↦ˢᵗᵏ v. Proof. iIntros "[[Hown Hall] Hl]". - iDestruct (own_valid with "Hown") as %Hvalid. + iDestruct (own_valid with "Hown") as %Hvalid. destruct (h !! l) as [av|] eqn:?. { iDestruct (big_sepM_lookup with "Hall") as "Hl'"; first done. destruct av as [v'|]; last by iExFalso. diff --git a/F_mu_ref_conc/notation.v b/F_mu_ref_conc/notation.v new file mode 100644 index 0000000..b56690a --- /dev/null +++ b/F_mu_ref_conc/notation.v @@ -0,0 +1,40 @@ +From iris_logrel.F_mu_ref_conc Require Import lang. +From iris.program_logic Require Import language. + +Set Default Proof Using "Type". +Import lang. +Coercion App : expr >-> Funclass. + +(* No scope for the values, does not conflict and scope is often not inferred +properly. *) +Notation "# l" := (LocV l%Z%V) (at level 8, format "# l"). +Notation "# l" := (Loc l%Z%V) (at level 8, format "# l") : expr_scope. + +(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come + first. *) +Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. +Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. +Notation "'case:' e0 'of' 'InjL' => e1 | 'InjR' => e2 'end'" := + (Case e0 e1 e2) + (e0, e1, e2 at level 200) : expr_scope. +Notation "()" := Unit : expr_scope. +Notation "()" := UnitV : val_scope. + +Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. +Notation "'ref' e" := (Alloc e%E) + (at level 30, right associativity) : expr_scope. + +(* The unicode ← is already part of the notation "_ ← _; _" for bind. *) +Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. +Notation "'rec:' e" := (Rec e%E) + (at level 102, e at level 200) : expr_scope. +Notation "'rec:' e" := (locked (RecV e%E)) + (at level 102, e at level 200) : val_scope. +Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) + (at level 200, e1, e2, e3 at level 200) : expr_scope. + +Notation "'Λ:' e" := (TLam e%E) + (at level 102, e at level 200) : expr_scope. +Notation "'Λ:' e" := (TLamV e%E) + (at level 102, e at level 200) : val_scope. + diff --git a/_CoqProject b/_CoqProject index 45bc4eb..da2caa3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -35,6 +35,7 @@ F_mu_ref_conc/soundness_unary.v F_mu_ref_conc/context_refinement.v F_mu_ref_conc/soundness_binary.v F_mu_ref_conc/tactics.v +F_mu_ref_conc/notation.v F_mu_ref_conc/examples/lock.v F_mu_ref_conc/examples/counter.v F_mu_ref_conc/examples/stack/stack_rules.v -- GitLab