From 04bc3235d650c1b0072c187e033a384617817565 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Tue, 12 Sep 2017 12:49:04 +0200 Subject: [PATCH] [stack] Factor out CG stack symbolic execution steps --- theories/examples/stack/CG_stack.v | 236 +++++++++------------------ theories/examples/stack/refinement.v | 52 +----- 2 files changed, 86 insertions(+), 202 deletions(-) diff --git a/theories/examples/stack/CG_stack.v b/theories/examples/stack/CG_stack.v index 80947be..f8d0b8e 100644 --- a/theories/examples/stack/CG_stack.v +++ b/theories/examples/stack/CG_stack.v @@ -143,21 +143,6 @@ Section CG_Stack. Hint Resolve CG_push_type : typeable. - (* 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)). *) - (* Proof. *) - (* 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. *) - (* tp_store j. simpl. by rewrite ?to_of_val /=. *) - (* tp_normalise j. by iFrame. *) - (* Qed. *) - - (* Global Opaque CG_push. *) - Lemma CG_locked_push_type Γ τ : typed Γ CG_locked_push (TArrow (Tref (CG_StackType τ)) (TArrow LockType (TArrow τ TUnit))). Proof. @@ -167,21 +152,29 @@ Section CG_Stack. Hint Resolve CG_locked_push_type : typeable. - (* 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). *) - (* Proof. *) - (* iIntros (?) "#Hspec Hst Hl Hj". *) - (* unfold CG_locked_push. *) - (* tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ UnitV) with "Hst Hl" as "[Hst $]"; [auto | | ]. *) - (* - iIntros (K') "#Hspec Hst Hj". *) - (* iApply (steps_CG_push with "Hspec Hst"); auto. *) - (* - by iFrame. *) - (* Qed. *) - - (* Global Opaque CG_locked_push. *) + Lemma CG_push_r st' (v w : val) l E1 E2 Δ Γ t K τ : + nclose logrelN ⊆ E1 → + st' ↦ₛ v -∗ l ↦ₛ #false -∗ + (st' ↦ₛ FoldV (InjRV (w, v)) -∗ l ↦ₛ #false + -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ) -∗ + {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) w) : τ. + Proof. + iIntros (?)"Hst' Hl Hlog". + unlock CG_locked_push CG_push. simpl_subst/=. + rel_let_r. + rel_apply_r (bin_log_related_acquire_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + rel_seq_r. + do 2 rel_let_r. + rel_load_r. + rel_store_r. + rel_seq_r. + rel_apply_r (bin_log_related_release_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + iApply ("Hlog" with "Hst' Hl"). + Qed. (* Coarse-grained pop *) Lemma CG_pop_type Γ τ : @@ -193,39 +186,6 @@ Section CG_Stack. Qed. Hint Resolve CG_pop_type : typeable. - (* 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. *) - (* Proof. *) - (* 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 /=. *) - (* tp_normalise j. *) - (* tp_case_inr j; simpl; first by rewrite ?to_of_val. *) - (* tp_snd j; eauto using to_of_val. *) - (* tp_store j; eauto using to_of_val. tp_normalise j. *) - (* tp_rec j. asimpl. *) - (* tp_fst j; eauto using to_of_val. tp_normalise j. *) - (* by iFrame. *) - (* Qed. *) - - (* 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). *) - (* Proof. *) - (* iIntros (HNE) "#Hspec Hx Hj". unfold CG_pop. *) - (* tp_rec j. *) - (* tp_load j. asimpl. tp_normalise j. *) - (* tp_fold j. *) - (* tp_case_inl j. asimpl. tp_normalise j. *) - (* by iFrame. *) - (* Qed. *) - Global Opaque CG_pop. Lemma CG_locked_pop_type Γ τ : @@ -236,33 +196,63 @@ Section CG_Stack. Qed. Hint Resolve CG_locked_pop_type : typeable. - (* 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). *) - (* Proof. *) - (* iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. *) - (* tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV) *) - (* with "Hx Hl" as "[Hx $]"; first auto. *) - (* - iIntros (K') "#Hspec Hx Hj". *) - (* iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial. *) - (* - by iFrame. *) - (* 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). *) - (* Proof. *) - (* iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. *) - (* tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV) *) - (* with "Hx Hl" as "[Hx Hl]"; first auto. *) - (* - iIntros (K') "#Hspec Hx Hj /=". *) - (* iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial. *) - (* - by iFrame. *) - (* Qed. *) + + Lemma CG_pop_suc_r st' l (w v : val) E1 E2 Δ Γ t K τ : + nclose logrelN ⊆ E1 → + st' ↦ₛ FoldV (InjRV (w, v)) -∗ + l ↦ₛ #false -∗ + (st' ↦ₛ v -∗ l ↦ₛ #false + -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjR w) : τ) -∗ + {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #()) : τ. + Proof. + iIntros (?) "Hst' Hl Hlog". + unlock CG_locked_pop CG_pop. simpl_subst/=. + rel_seq_r. + rel_apply_r (bin_log_related_acquire_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + repeat rel_rec_r. + rel_load_r. + rel_fold_r. + rel_case_r. + rel_let_r. + rel_proj_r. + rel_store_r. + rel_seq_r. + rel_proj_r. + rel_rec_r. + rel_apply_r (bin_log_related_release_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + rel_rec_r. + iApply ("Hlog" with "Hst' Hl"). + Qed. + + Lemma CG_pop_fail_r st' l E1 E2 Δ Γ t K τ : + nclose logrelN ⊆ E1 → + st' ↦ₛ FoldV (InjLV #()) -∗ + l ↦ₛ #false -∗ + (st' ↦ₛ FoldV (InjLV #()) -∗ l ↦ₛ #false + -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjL #()) : τ) -∗ + {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #()) : τ. + Proof. + iIntros (?) "Hst' Hl Hlog". + unlock CG_locked_pop CG_pop. simpl_subst/=. + rel_seq_r. + rel_apply_r (bin_log_related_acquire_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + repeat rel_rec_r. + rel_load_r. + rel_fold_r. + rel_case_r. + repeat rel_let_r. + rel_apply_r (bin_log_related_release_r with "Hl"). + { solve_ndisj. } + iIntros "Hl /=". + rel_rec_r. + iApply ("Hlog" with "Hst' Hl"). + Qed. Global Opaque CG_locked_pop. @@ -274,36 +264,8 @@ Section CG_Stack. Qed. Hint Resolve CG_snap_type : typeable. - (* 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). *) - (* Proof. *) - (* iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_snap. *) - (* tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ v UnitV) *) - (* with "Hx Hl" as "[Hx $]"; first auto. *) - (* - iIntros (K') "#Hspec Hx Hj". *) - (* tp_rec j. *) - (* tp_load j. tp_normalise j. *) - (* by iFrame. *) - (* - by iFrame. *) - (* Qed. *) - Global Opaque CG_snap. - (* (* Coarse-grained iter *) *) - (* Lemma CG_iter_folding (f : expr) : *) - (* CG_iter f = *) - (* Rec (Case (Unfold (Var 1)) *) - (* Unit *) - (* ( *) - (* App (Rec (App (Var 3) (Snd (Var 2)))) *) - (* (App f.[ren (+3)] (Fst (Var 0))) *) - (* ) *) - (* ). *) - (* Proof. trivial. Qed. *) - Lemma CG_iter_type Γ τ : typed Γ CG_iter (TArrow (TArrow τ TUnit) (TArrow (CG_StackType τ) TUnit)). Proof. @@ -313,44 +275,6 @@ Section CG_Stack. Qed. Hint Resolve CG_iter_type : typeable. - - (* 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))). *) - (* Proof. *) - (* 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 /=). *) - (* tp_case_inr j; first by (rewrite /= ?to_of_val /=). *) - (* asimpl. *) - (* tp_fst j; auto using to_of_val. *) - (* tp_normalise j. *) - (* done. *) - (* Qed. *) - - (* Transparent CG_iter. *) - - (* 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. *) - (* Proof. *) - (* iIntros (HNE) "#Hspec Hj". unfold CG_iter. *) - (* tp_rec j. *) - (* tp_fold j. *) - (* tp_case_inl j. tp_normalise j. *) - (* by iFrame. *) - (* Qed. *) - Global Opaque CG_iter. Lemma CG_snap_iter_type Γ τ : diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v index adab25b..ed8c61e 100644 --- a/theories/examples/stack/refinement.v +++ b/theories/examples/stack/refinement.v @@ -28,8 +28,6 @@ Section Stack_refinement. Proof. iIntros "#Hinv #Hvv'" (Δ). Transparent FG_push. - unfold CG_locked_push. unlock. simpl_subst/=. - rel_rec_r. unfold FG_push. unlock. simpl_subst/=. iLöb as "IH". rel_rec_l. @@ -48,17 +46,9 @@ Section Stack_refinement. - (* CAS succeeds *) iSplitR; first by iIntros ([]). iIntros (?). iNext. iIntros "Hst". - rel_apply_r (bin_log_related_acquire_r with "Hl"). + rel_apply_r (CG_push_r with "Hst' Hl"). { solve_ndisj. } - iIntros "Hl /=". - rel_rec_r. - unfold CG_push. unlock. do 2 rel_rec_r. - rel_load_r. - rel_store_r. - rel_rec_r. - rel_apply_r (bin_log_related_release_r with "Hl"). - { solve_ndisj. } - iIntros "Hl /=". + iIntros "Hst' Hl". iApply fupd_logrel'. (* TODO iMod should pick this up on its own *) iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]". iModIntro. @@ -112,22 +102,9 @@ replace ((rec: "pop" "st" <> := iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=. iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=. - (* The stack is empty *) - rewrite {2}/CG_locked_pop. unlock. simpl_subst/=. - rel_rec_r. - rel_apply_r (bin_log_related_acquire_r with "Hl"). + rel_apply_r (CG_pop_fail_r with "Hst' Hl"). { solve_ndisj. } - iIntros "Hl /=". - unfold CG_pop. unlock. - repeat rel_rec_r. - rel_load_r. - rel_fold_r. - rel_case_r. - repeat rel_rec_r. - rel_apply_r (bin_log_related_release_r with "Hl"). - { solve_ndisj. } - iIntros "Hl /=". - rel_rec_r. - + iIntros "Hst' Hl". close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'". rel_load_l_atomic. iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". @@ -171,26 +148,9 @@ replace ((rec: "pop" "st" <> := iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=. iDestruct "HLK2" as (ym1 ym2 zm1 zm2) "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=. - rewrite {2}/CG_locked_pop. unlock. simpl_subst/=. - rel_rec_r. - rel_apply_r (bin_log_related_acquire_r with "Hl"). + rel_apply_r (CG_pop_suc_r with "Hst' Hl"). { solve_ndisj. } - iIntros "Hl /=". - unfold CG_pop. unlock. - repeat rel_rec_r. - rel_load_r. - rel_fold_r. - rel_case_r. - rel_rec_r. - rel_proj_r. - rel_store_r. - rel_rec_r. - rel_proj_r. - rel_rec_r. - rel_apply_r (bin_log_related_release_r with "Hl"). - { solve_ndisj. } - iIntros "Hl /=". - rel_rec_r. + iIntros "Hst' Hl". iMod ("Hclose" with "[-]"). { iNext. rewrite /sinv. rewrite (StackLink_unfold _ (ym2, z2)). -- GitLab