diff --git a/theories/logrel/F_mu_ref_conc/examples/lock.v b/theories/logrel/F_mu_ref_conc/examples/lock.v index 6b93469422a8cfb13806da5199e4c31a7f15c9e6..1235b05d715901fabad1d870cb1773ffdb071d2c 100644 --- a/theories/logrel/F_mu_ref_conc/examples/lock.v +++ b/theories/logrel/F_mu_ref_conc/examples/lock.v @@ -7,20 +7,26 @@ Definition newlock : expr := Alloc (#♭ false). Definition acquire : expr := Rec (If (CAS (Var 1) (#♭ false) (#♭ true)) (Unit) (App (Var 0) (Var 1))). (** [release = λ x. x <- false] *) -Definition release : expr := Rec (Store (Var 1) (#♭ false)). +Definition release : expr := Lam (Store (Var 0) (#♭ false)). (** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *) Definition with_lock (e : expr) (l : expr) : expr := - Rec - (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)]))) - (App e.[ren (+4)] (Var 3)))) - (App acquire l.[ren (+2)]) + Lam + (Seq + (App acquire l.[ren (+1)]) + (LetIn + (App e.[ren (+1)] (Var 0)) + (Seq (App release l.[ren (+2)]) (Var 0)) + ) ). Definition with_lockV (e l : expr) : val := - RecV - (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)]))) - (App e.[ren (+4)] (Var 3)))) - (App acquire l.[ren (+2)]) + LamV + (Seq + (App acquire l.[ren (+1)]) + (LetIn + (App e.[ren (+1)] (Var 0)) + (Seq (App release l.[ren (+2)]) (Var 0)) + ) ). Lemma with_lock_to_val e l : to_val (with_lock e l) = Some (with_lockV e l). @@ -29,6 +35,7 @@ Proof. trivial. Qed. Lemma with_lock_of_val e l : of_val (with_lockV e l) = with_lock e l. Proof. trivial. Qed. +Global Typeclasses Opaque with_lockV. Global Opaque with_lockV. Lemma newlock_closed f : newlock.[f] = newlock. @@ -43,15 +50,10 @@ Lemma release_closed f : release.[f] = release. Proof. by asimpl. Qed. Hint Rewrite release_closed : autosubst. -Lemma with_lock_subst (e l : expr) f : (with_lock e l).[f] = with_lock e.[f] l.[f]. +Lemma with_lock_subst (e l : expr) f : + (with_lock e l).[f] = with_lock e.[f] l.[f]. Proof. unfold with_lock; asimpl; trivial. Qed. -Lemma with_lock_closed e l: - (∀ f : var → expr, e.[f] = e) → - (∀ f : var → expr, l.[f] = l) → - ∀ f, (with_lock e l).[f] = with_lock e l. -Proof. asimpl => H1 H2 f. unfold with_lock. by rewrite ?H1 ?H2. Qed. - Definition LockType := Tref TBool. Lemma newlock_type Γ : typed Γ newlock LockType. @@ -68,18 +70,20 @@ Lemma with_lock_type e l Γ τ τ' : typed Γ l LockType → typed Γ (with_lock e l) (TArrow τ τ'). Proof. - intros H1 H2. do 3 econstructor; eauto. - - repeat (econstructor; eauto using release_type). - + eapply (context_weakening [_; _; _; _; _; _]); eauto. - + eapply (context_weakening [_; _; _; _]); eauto. - - eapply acquire_type. - - eapply (context_weakening [_; _]); eauto. + intros ??. + do 3 econstructor; eauto using acquire_type. + - eapply (context_weakening [_]); eauto. + - econstructor; eauto using typed. + eapply (context_weakening [_]); eauto. + - econstructor; eauto using typed. + econstructor; eauto using release_type. + eapply (context_weakening [_;_]); eauto. Qed. Section proof. Context `{cfgSG Σ}. Context `{heapIG Σ}. - + Lemma steps_newlock E ρ j K : nclose specN ⊆ E → spec_ctx ρ ∗ j ⤇ fill K newlock @@ -89,6 +93,7 @@ Section proof. by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto. Qed. + Global Typeclasses Opaque newlock. Global Opaque newlock. Lemma steps_acquire E ρ j K l : @@ -107,6 +112,7 @@ Section proof. Unshelve. all:trivial. Qed. + Global Typeclasses Opaque acquire. Global Opaque acquire. Lemma steps_release E ρ j K l b: @@ -115,48 +121,45 @@ Section proof. ⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#♭v false). Proof. iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release. - iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done. - iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto. - { by iFrame. } + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto; try done. + iMod (step_store with "[$Hj $Hl]") as "[Hj Hl]"; eauto. by iIntros "!> {$Hj $Hl}". - Unshelve. all: trivial. Qed. + Global Typeclasses Opaque release. Global Opaque release. 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 *) → + (* (∀ 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). Proof. - iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]". - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. rewrite H1. - iMod (steps_acquire _ _ j ((AppRCtx (RecV _)) :: K) - _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto. - { simpl. iFrame "Hspec Hj Hl"; eauto. } - simpl. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. rewrite H1. - iMod (H2 ((AppRCtx (RecV _)) :: K) with "[Hj HP]") as "[Hj HQ]"; eauto. - { simpl. iFrame "Hspec Hj HP"; eauto. } + iIntros (HNE He) "[#Hspec [HP [Hl Hj]]]". + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iAsimpl. + iMod (steps_acquire _ _ j (SeqCtx _ :: K) with "[$Hj Hl]") as "[Hj Hl]"; + auto. simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iMod (He (LetInCtx _ :: K) with "[$Hj HP]") as "[Hj HQ]"; eauto. simpl. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (steps_release _ _ j ((AppRCtx (RecV _)) :: K) _ _ with "[Hj Hl]") + iMod (steps_release _ _ j (SeqCtx _ :: K) _ _ with "[$Hj $Hl]") as "[Hj Hl]"; eauto. - { simpl. by iFrame. } - rewrite ?fill_app /=. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. iModIntro; by iFrame. - Unshelve. - all: try match goal with |- to_val _ = _ => auto using to_of_val end. - trivial. + simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iModIntro; by iFrame. Qed. + Global Typeclasses Opaque with_lock. Global Opaque with_lock. End proof. + +Global Hint Rewrite newlock_closed : autosubst. +Global Hint Rewrite acquire_closed : autosubst. +Global Hint Rewrite release_closed : autosubst. +Global Hint Rewrite with_lock_subst : autosubst. diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v index c14612a8bca1b2b9eef4aef040e6e56ee3d0e5b1..262b047d49173334cf7d43c0a0940098d43679ae 100644 --- a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v +++ b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v @@ -7,33 +7,34 @@ Definition CG_StackType τ := (* Coarse-grained push *) Definition CG_push (st : expr) : expr := - Rec (Store - (st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))). + Lam (Store (st.[ren (+1)]) (Fold (InjR (Pair (Var 0) (Load st.[ren (+ 1)]))))). Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l. Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l. Definition CG_pop (st : expr) : expr := - Rec (Case (Unfold (Load st.[ren (+ 2)])) + Lam (Case (Unfold (Load st.[ren (+ 1)])) (InjL Unit) ( - App (Rec (InjR (Fst (Var 2)))) - (Store st.[ren (+ 3)] (Snd (Var 0))) + Seq + (Store st.[ren (+ 2)] (Snd (Var 0))) + (InjR (Fst (Var 0))) ) ). Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l. Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l. -Definition CG_snap (st l : expr) := with_lock (Rec (Load st.[ren (+2)])) l. -Definition CG_snapV (st l : expr) : val := with_lockV (Rec (Load st.[ren (+2)])) l. +Definition CG_snap (st l : expr) := with_lock (Lam (Load st.[ren (+1)])) l. +Definition CG_snapV (st l : expr) : val := with_lockV (Lam (Load st.[ren (+1)])) l. Definition CG_iter (f : expr) : expr := Rec (Case (Unfold (Var 1)) Unit ( - App (Rec (App (Var 3) (Snd (Var 2)))) - (App f.[ren (+3)] (Fst (Var 0))) + Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) ) ). @@ -41,20 +42,26 @@ Definition CG_iterV (f : expr) : val := RecV (Case (Unfold (Var 1)) Unit ( - App (Rec (App (Var 3) (Snd (Var 2)))) - (App f.[ren (+3)] (Fst (Var 0))) + Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) ) ). Definition CG_snap_iter (st l : expr) : expr := - Rec (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)). + Lam (App (CG_iter (Var 0)) (App (CG_snap st.[ren (+1)] l.[ren (+1)]) Unit)). + Definition CG_stack_body (st l : expr) : expr := Pair (Pair (CG_locked_push st l) (CG_locked_pop st l)) (CG_snap_iter st l). Definition CG_stack : expr := - TLam (App (Rec (App (Rec (CG_stack_body (Var 1) (Var 3))) - (Alloc (Fold (InjL Unit))))) newlock). + TLam ( + LetIn + newlock + (LetIn + (Alloc (Fold (InjL Unit))) + (CG_stack_body (Var 0) (Var 1)))). Section CG_Stack. Context `{heapIG Σ, cfgSG Σ}. @@ -64,37 +71,33 @@ Section CG_Stack. typed Γ (CG_push st) (TArrow τ TUnit). Proof. intros H1. repeat econstructor. - eapply (context_weakening [_; _]); eauto. + eapply (context_weakening [_]); eauto. repeat constructor; asimpl; trivial. - eapply (context_weakening [_; _]); eauto. + eapply (context_weakening [_]); eauto. Qed. - Lemma CG_push_closed (st : expr) : - (∀ f, st.[f] = st) → ∀ f, (CG_push st).[f] = CG_push st. - Proof. intros Hst f. unfold CG_push. asimpl. rewrite ?Hst; trivial. Qed. - Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f]. Proof. unfold CG_push; asimpl; trivial. Qed. + Global Hint Rewrite CG_push_subst : autosubst. + 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. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. iMod (step_load _ _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K) - _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - simpl. iFrame "Hspec Hj"; trivial. simpl. - iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - { by iFrame. } + with "[$Hj $Hx]") as "[Hj Hx]"; eauto. + simpl. + iMod (step_store _ _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto. + { rewrite /= !to_of_val //. } iModIntro. by iFrame. - Unshelve. - all: try match goal with |- to_val _ = _ => auto using to_of_val end. - simpl; by rewrite ?to_of_val. Qed. + Global Typeclasses Opaque CG_push. Global Opaque CG_push. Lemma CG_locked_push_to_val st l : @@ -106,7 +109,6 @@ Section CG_Stack. Proof. trivial. Qed. Global Opaque CG_locked_pushV. - Lemma CG_locked_push_type st l Γ τ : typed Γ st (Tref (CG_StackType τ)) → typed Γ l LockType → @@ -116,17 +118,11 @@ Section CG_Stack. eapply with_lock_type; auto using CG_push_type. Qed. - Lemma CG_locked_push_closed (st l : expr) : - (∀ f, st.[f] = st) → (∀ f, l.[f] = l) → - ∀ f, (CG_locked_push st l).[f] = CG_locked_push st l. - Proof. - intros H1 H2 f. asimpl. unfold CG_locked_push. - rewrite with_lock_closed; trivial. apply CG_push_closed; trivial. - Qed. - Lemma CG_locked_push_subst (st l : expr) f : (CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f]. - Proof. by rewrite with_lock_subst CG_push_subst. Qed. + Proof. by rewrite /CG_locked_push; asimpl. Qed. + + Hint Rewrite CG_locked_push_subst : autosubst. Lemma steps_CG_locked_push E ρ j K st w v l : nclose specN ⊆ E → @@ -135,14 +131,13 @@ Section CG_Stack. ⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false). Proof. intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push. - iMod (steps_with_lock - _ _ j K _ _ _ _ UnitV _ _ _ with "[Hj Hx Hl]") as "Hj"; last done. - - iIntros (K') "[#Hspec Hxj]". - iApply steps_CG_push; first done. iFrame. trivial. - - iFrame "Hspec Hj Hx"; trivial. - Unshelve. all: trivial. + iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]") + as "Hj"; auto. + iIntros (K') "[#Hspec Hxj]". + iApply steps_CG_push; first done. by iFrame. Qed. + Global Typeclasses Opaque CG_locked_push. Global Opaque CG_locked_push. (* Coarse-grained pop *) @@ -152,22 +147,22 @@ Section CG_Stack. Proof. intros H1. econstructor. - eapply (Case_typed _ _ _ _ TUnit); - [| repeat constructor - | repeat econstructor; eapply (context_weakening [_; _; _]); eauto]. - replace (TSum TUnit (TProd τ (CG_StackType τ))) with - ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/]) - by (by asimpl). - repeat econstructor. - eapply (context_weakening [_; _]); eauto. + eapply (Case_typed _ _ _ _ TUnit); eauto using typed. + - replace (TSum TUnit (TProd τ (CG_StackType τ))) with + ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/]) + by (by asimpl). + repeat econstructor. + eapply (context_weakening [_]); eauto. + - econstructor; eauto using typed. + econstructor; eauto using typed. + eapply (context_weakening [_; _]); eauto. Qed. - Lemma CG_pop_closed (st : expr) : - (∀ f, st.[f] = st) → ∀ f, (CG_pop st).[f] = CG_pop st. - Proof. intros Hst f. unfold CG_pop. asimpl. rewrite ?Hst; trivial. Qed. + Lemma CG_pop_subst (st : expr) f : + (CG_pop st).[f] = CG_pop st.[f]. + Proof. by rewrite /CG_pop; asimpl. Qed. - Lemma CG_pop_subst (st : expr) f : (CG_pop st).[f] = CG_pop st.[f]. - Proof. unfold CG_pop; asimpl; trivial. Qed. + Hint Rewrite CG_pop_subst : autosubst. Lemma steps_CG_pop_suc E ρ j K st v w : nclose specN ⊆ E → @@ -176,35 +171,25 @@ Section CG_Stack. ⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v. Proof. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K) - _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - rewrite ?fill_app. simpl. - iFrame "Hspec Hj"; trivial. - rewrite ?fill_app. simpl. - iMod (step_Fold _ _ j (CaseCtx _ _ :: K) - _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (step_load _ _ _ (UnfoldCtx :: CaseCtx _ _ :: K) with "[$Hj $Hx]") + as "[Hj Hx]"; eauto. simpl. - iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. - iMod (step_snd _ _ j (StoreRCtx (LocV _) :: AppRCtx (RecV _) :: K) _ _ _ _ - _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto. simpl. - iMod (step_store _ _ j (AppRCtx (RecV _) :: K) _ _ _ _ _ _ - with "[Hj Hx]") as "[Hj Hx]"; eauto. - rewrite ?fill_app. simpl. - iFrame "Hspec Hj"; trivial. - rewrite ?fill_app. simpl. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_fst _ _ j (InjRCtx :: K) _ _ _ _ _ _ - with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure _ _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K) + with "[$Hj]") as "Hj"; eauto. simpl. - iModIntro. iFrame "Hj Hx"; trivial. - Unshelve. - all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. - all: trivial. + iMod (step_store _ _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]"; + eauto using to_of_val. + simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iMod (do_step_pure _ _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto. + simpl. + by iFrame "Hj Hx". Qed. Lemma steps_CG_pop_fail E ρ j K st : @@ -214,21 +199,17 @@ Section CG_Stack. ⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV). Proof. iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K) - _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - simpl. iFrame "Hspec Hj"; trivial. simpl. - iMod (step_Fold _ _ j (CaseCtx _ _ :: K) - _ _ _ _ with "[Hj]") as "Hj"; eauto. - iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. - iModIntro. iFrame "Hj Hx"; trivial. - Unshelve. - all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. - all: trivial. + _ _ _ with "[$Hj $Hx]") as "[Hj Hx]"; eauto. + iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto. + simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + by iFrame "Hj Hx"; trivial. Qed. + Global Typeclasses Opaque CG_pop. Global Opaque CG_pop. Lemma CG_locked_pop_to_val st l : @@ -250,17 +231,11 @@ Section CG_Stack. eapply with_lock_type; auto using CG_pop_type. Qed. - Lemma CG_locked_pop_closed (st l : expr) : - (∀ f, st.[f] = st) → (∀ f, l.[f] = l) → - ∀ f, (CG_locked_pop st l).[f] = CG_locked_pop st l. - Proof. - intros H1 H2 f. asimpl. unfold CG_locked_pop. - rewrite with_lock_closed; trivial. apply CG_pop_closed; trivial. - Qed. - Lemma CG_locked_pop_subst (st l : expr) f : - (CG_locked_pop st l).[f] = CG_locked_pop st.[f] l.[f]. - Proof. by rewrite with_lock_subst CG_pop_subst. Qed. + (CG_locked_pop st l).[f] = CG_locked_pop st.[f] l.[f]. + Proof. by rewrite /CG_locked_pop; asimpl. Qed. + + Hint Rewrite CG_locked_pop_subst : autosubst. Lemma steps_CG_locked_pop_suc E ρ j K st v w l : nclose specN ⊆ E → @@ -269,12 +244,11 @@ Section CG_Stack. ⊢ |={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 Hxj]". - iApply steps_CG_pop_suc; first done. by iFrame. - - iFrame "Hspec Hj Hx"; trivial. - Unshelve. all: trivial. + iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I + _ (InjRV w) UnitV + with "[$Hj $Hx $Hl]") as "Hj"; eauto. + iIntros (K') "[#Hspec Hxj]". + iApply steps_CG_pop_suc; eauto. Qed. Lemma steps_CG_locked_pop_fail E ρ j K st l : @@ -284,14 +258,14 @@ Section CG_Stack. ⊢ |={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 Hxj] /=". - iApply steps_CG_pop_fail; first done. by iFrame. - - iFrame "Hspec Hj Hx"; trivial. - Unshelve. all: trivial. + iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _ + (InjLV UnitV) UnitV + with "[$Hj $Hx $Hl]") as "Hj"; eauto. + iIntros (K') "[#Hspec Hxj] /=". + iApply steps_CG_pop_fail; eauto. Qed. + Global Typeclasses Opaque CG_locked_pop. Global Opaque CG_locked_pop. Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l). @@ -300,6 +274,7 @@ Section CG_Stack. Lemma CG_snap_of_val st l : of_val (CG_snapV st l) = CG_snap st l. Proof. trivial. Qed. + Global Typeclasses Opaque CG_snapV. Global Opaque CG_snapV. Lemma CG_snap_type st l Γ τ : @@ -309,21 +284,14 @@ Section CG_Stack. Proof. intros H1 H2. repeat econstructor. eapply with_lock_type; trivial. do 2 constructor. - eapply (context_weakening [_; _]); eauto. - Qed. - - Lemma CG_snap_closed (st l : expr) : - (∀ f, st.[f] = st) → (∀ f, l.[f] = l) → - ∀ f, (CG_snap st l).[f] = CG_snap st l. - Proof. - intros H1 H2 f. asimpl. unfold CG_snap. - rewrite with_lock_closed; trivial. - intros f'. by asimpl; rewrite ?H1. + eapply (context_weakening [_]); eauto. Qed. Lemma CG_snap_subst (st l : expr) f : (CG_snap st l).[f] = CG_snap st.[f] l.[f]. - Proof. unfold CG_snap; rewrite ?with_lock_subst. by asimpl. Qed. + Proof. by unfold CG_snap; asimpl. Qed. + + Hint Rewrite CG_snap_subst : autosubst. Lemma steps_CG_snap E ρ j K st v l : nclose specN ⊆ E → @@ -332,20 +300,16 @@ Section CG_Stack. ⊢ |={E}=> j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). Proof. iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap. - iMod (steps_with_lock _ _ j K _ _ (st ↦ₛ v)%I _ v UnitV _ _ - with "[Hj Hx Hl]") as "Hj"; last done; [|iFrame; iFrame "#"]. + iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV + with "[$Hj $Hx $Hl]") as "Hj"; eauto. iIntros (K') "[#Hspec [Hx Hj]]". - iMod (step_rec _ _ j K' _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_load _ _ j K' _ _ _ _ - with "[Hj Hx]") as "[Hj Hx]"; eauto. - - iFrame "#"; iFrame. - - iModIntro. by iFrame "Hj Hx". - Unshelve. - all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. - all: trivial. + iMod (step_load with "[$Hj $Hx]") as "[Hj Hx]"; eauto. + by iFrame. Qed. + Global Typeclasses Opaque CG_snap. Global Opaque CG_snap. (* Coarse-grained iter *) @@ -354,8 +318,9 @@ Section CG_Stack. Rec (Case (Unfold (Var 1)) Unit ( - App (Rec (App (Var 3) (Snd (Var 2)))) - (App f.[ren (+3)] (Fst (Var 0))) + Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) ) ). Proof. trivial. Qed. @@ -364,15 +329,14 @@ Section CG_Stack. typed Γ f (TArrow τ TUnit) → typed Γ (CG_iter f) (TArrow (CG_StackType τ) TUnit). Proof. - intros H1. - econstructor. - eapply (Case_typed _ _ _ _ TUnit); - [| repeat constructor - | repeat econstructor; eapply (context_weakening [_; _; _]); eauto]. + intros ?. econstructor. + eapply (Case_typed _ _ _ _ TUnit); eauto using typed. replace (TSum TUnit (TProd τ (CG_StackType τ))) with ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/]) by (by asimpl). repeat econstructor. + repeat econstructor; simpl; eauto using typed. + eapply (context_weakening [_; _; _]); eauto. Qed. Lemma CG_iter_to_val f : to_val (CG_iter f) = Some (CG_iterV f). @@ -381,14 +345,13 @@ Section CG_Stack. Lemma CG_iter_of_val f : of_val (CG_iterV f) = CG_iter f. Proof. trivial. Qed. + Global Typeclasses Opaque CG_iterV. Global Opaque CG_iterV. - Lemma CG_iter_closed (f : expr) : - (∀ g, f.[g] = f) → ∀ g, (CG_iter f).[g] = CG_iter f. - Proof. intros Hf g. unfold CG_iter. asimpl. rewrite ?Hf; trivial. Qed. - Lemma CG_iter_subst (f : expr) g : (CG_iter f).[g] = CG_iter f.[g]. - Proof. unfold CG_iter; asimpl; trivial. Qed. + Proof. by unfold CG_iter; asimpl. Qed. + + Hint Rewrite CG_iter_subst : autosubst. Lemma steps_CG_iter E ρ j K f v w : nclose specN ⊆ E → @@ -397,44 +360,33 @@ Section CG_Stack. (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))). + (Seq (App (of_val f) (of_val w)) + (App (CG_iter (of_val f)) (Snd (Pair (of_val w) (of_val v))))). Proof. iIntros (HNE) "[#Hspec Hj]". unfold CG_iter. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - rewrite -CG_iter_folding. Opaque CG_iter. iAsimpl. - iMod (step_Fold _ _ j (CaseCtx _ _ :: K) - _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iAsimpl. + iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_fst _ _ j (AppRCtx f :: AppRCtx (RecV _) :: K) _ _ _ _ - _ _ with "[Hj]") as "Hj"; eauto. - Unshelve. - all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. + iMod (do_step_pure _ _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]") + as "Hj"; eauto. 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. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - rewrite -CG_iter_folding. Opaque CG_iter. iAsimpl. - iMod (step_Fold _ _ j (CaseCtx _ _ :: K) - _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto. iAsimpl. - iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. - Unshelve. - all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. Qed. + Global Typeclasses Opaque CG_iter. Global Opaque CG_iter. Lemma CG_snap_iter_type st l Γ τ : @@ -444,23 +396,14 @@ Section CG_Stack. Proof. intros H1 H2; repeat econstructor. - eapply CG_iter_type; by constructor. - - eapply CG_snap_type; by eapply (context_weakening [_;_]). - Qed. - - Lemma CG_snap_iter_closed (st l : expr) : - (∀ f, st.[f] = st) → (∀ f, l.[f] = l) → - ∀ f, (CG_snap_iter st l).[f] = CG_snap_iter st l. - Proof. - intros H1 H2 f. unfold CG_snap_iter. asimpl. rewrite H1 H2. - rewrite CG_snap_closed; auto. + - eapply CG_snap_type; by eapply (context_weakening [_]). Qed. Lemma CG_snap_iter_subst (st l : expr) g : (CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g]. - Proof. - unfold CG_snap_iter; asimpl. - rewrite CG_snap_subst CG_iter_subst. by asimpl. - Qed. + Proof. by unfold CG_snap_iter; asimpl. Qed. + + Hint Rewrite CG_snap_iter_subst : autosubst. Lemma CG_stack_body_type st l Γ τ : typed Γ st (Tref (CG_StackType τ)) → @@ -476,17 +419,15 @@ Section CG_Stack. CG_locked_pop_type, CG_snap_iter_type). Qed. - Opaque CG_snap_iter. - Lemma CG_stack_body_closed (st l : expr) : - (∀ f, st.[f] = st) → (∀ f, l.[f] = l) → - ∀ f, (CG_stack_body st l).[f] = CG_stack_body st l. - Proof. - intros H1 H2 f. unfold CG_stack_body. asimpl. - rewrite CG_locked_push_closed; trivial. - rewrite CG_locked_pop_closed; trivial. - by rewrite CG_snap_iter_closed. - Qed. + Global Typeclasses Opaque CG_snap_iter. + Global Opaque CG_snap_iter. + + Lemma CG_stack_body_subst (st l : expr) f : + (CG_stack_body st l).[f] = CG_stack_body st.[f] l.[f]. + Proof. by unfold CG_stack_body; asimpl. Qed. + + Hint Rewrite CG_stack_body_subst : autosubst. Lemma CG_stack_type Γ : typed Γ CG_stack @@ -499,18 +440,24 @@ Section CG_Stack. (TArrow (TArrow (TVar 0) TUnit) TUnit) )). Proof. - repeat econstructor. - - eapply CG_locked_push_type; constructor; simpl; eauto. - - eapply CG_locked_pop_type; constructor; simpl; eauto. - - eapply CG_snap_iter_type; constructor; by simpl. - - asimpl. repeat constructor. - - eapply newlock_type. + repeat econstructor; + eauto 10 using newlock_type, CG_locked_push_type, CG_locked_pop_type, + CG_snap_iter_type, typed. + asimpl; repeat constructor. Qed. Lemma CG_stack_closed f : CG_stack.[f] = CG_stack. - Proof. - unfold CG_stack. - asimpl; rewrite ?CG_locked_push_subst ?CG_locked_pop_subst. - asimpl. rewrite ?CG_snap_iter_subst. by asimpl. - Qed. + Proof. by unfold CG_stack; asimpl. Qed. + End CG_Stack. + +Global Hint Rewrite CG_push_subst : autosubst. +Global Hint Rewrite CG_locked_push_subst : autosubst. +Global Hint Rewrite CG_locked_pop_subst : autosubst. +Global Hint Rewrite CG_pop_subst : autosubst. +Global Hint Rewrite CG_locked_pop_subst : autosubst. +Global Hint Rewrite CG_snap_subst : autosubst. +Global Hint Rewrite CG_iter_subst : autosubst. +Global Hint Rewrite CG_snap_iter_subst : autosubst. +Global Hint Rewrite CG_stack_body_subst : autosubst. +Global Hint Rewrite CG_stack_closed : autosubst. diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v index 4463e46dcdb3e8ea6b21f69ccfe97d0a1c76537c..d1341e5b35ad6cbb4a2170b46b105e0c26179b5d 100644 --- a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v +++ b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v @@ -1,4 +1,4 @@ -From iris_examples.logrel.F_mu_ref_conc Require Import typing. +From iris_examples.logrel.F_mu_ref_conc Require Import typing. Definition FG_StackType τ := TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))). @@ -7,103 +7,99 @@ Definition FG_Stack_Ref_Type τ := Tref (TSum TUnit (TProd τ (FG_StackType τ))). Definition FG_push (st : expr) : expr := - Rec (App (Rec - (* try push *) - (If (CAS (st.[ren (+4)]) (Var 1) - (Alloc (InjR (Pair (Var 3) (Fold (Var 1))))) - ) - Unit (* push succeeds we return unit *) - (App (Var 2) (Var 3)) (* push fails, we try again *) - ) + Rec + (LetIn + (Load st.[ren (+2)]) + (* try push *) + (If (CAS (st.[ren (+3)]) (Var 0) + (Alloc (InjR (Pair (Var 2) (Fold (Var 0))))) ) - (Load st.[ren (+2)]) (* read the stack pointer *) - ). + Unit (* push succeeds we return unit *) + (App (Var 1) (Var 2)) (* push fails, we try again *) + ) + ). + Definition FG_pushV (st : expr) : val := - RecV (App (Rec - (* try push *) - (If (CAS (st.[ren (+4)]) (Var 1) - (Alloc (InjR (Pair (Var 3) (Fold (Var 1))))) - ) - Unit (* push succeeds we return unit *) - (App (Var 2) (Var 3)) (* push fails, we try again *) - ) + RecV + (LetIn + (Load st.[ren (+2)]) + (* try push *) + (If (CAS (st.[ren (+3)]) (Var 0) + (Alloc (InjR (Pair (Var 2) (Fold (Var 0))))) ) - (Load st.[ren (+2)]) (* read the stack pointer *) - ). + Unit (* push succeeds we return unit *) + (App (Var 1) (Var 2)) (* push fails, we try again *) + ) + ). Definition FG_pop (st : expr) : expr := - Rec (App (Rec - (App - (Rec - ( - Case (Var 1) - (InjL Unit) - ( (* try popping *) - If - (CAS - (st.[ren (+7)]) - (Var 4) - (Unfold (Snd (Var 0))) - ) - (InjR (Fst (Var 0))) (* pop succeeds *) - (App (Var 5) (Var 6)) (* pop fails, we retry*) - ) - ) - ) - ( - (Load (Var 1)) + Rec + (LetIn + (Load st.[ren (+ 2)]) + (LetIn + (Load (Var 0)) + (Case + (Var 0) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+5)]) + (Var 2) + (Unfold (Snd (Var 0))) ) - ) - ) - (Load st.[ren (+ 2)]) - ). + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 3) (Var 4)) (* pop fails, we retry*) + ) + ) + ) + ). + Definition FG_popV (st : expr) : val := RecV - (App - (Rec - ( App - (Rec - ( - Case (Var 1) - (InjL Unit) - ( (* try popping *) - If - (CAS - (st.[ren (+7)]) - (Var 4) - (Unfold (Snd (Var 0))) - ) - (InjR (Fst (Var 0))) (* pop succeeds *) - (App (Var 5) (Var 6)) (* pop fails, we retry*) - ) + (LetIn + (Load st.[ren (+ 2)]) + (LetIn + (Load (Var 0)) + (Case + (Var 0) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+5)]) + (Var 2) + (Unfold (Snd (Var 0))) ) - ) - ( - (Load (Var 1)) - ) + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 3) (Var 4)) (* pop fails, we retry*) + ) ) ) - (Load st.[ren (+ 2)]) ). Definition FG_iter (f : expr) : expr := Rec (Case (Load (Unfold (Var 1))) Unit - (App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *) - (App f.[ren (+3)] (Fst (Var 0))) + (Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) (* recursive_call *) ) ). + Definition FG_iterV (f : expr) : val := RecV (Case (Load (Unfold (Var 1))) Unit - (App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *) - (App f.[ren (+3)] (Fst (Var 0))) + (Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) (* recursive_call *) ) ). + Definition FG_read_iter (st : expr) : expr := - Rec (App (FG_iter (Var 1)) (Fold (Load st.[ren (+2)]))). + Lam (App (FG_iter (Var 0)) (Fold (Load st.[ren (+1)]))). Definition FG_stack_body (st : expr) : expr := Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st). @@ -116,34 +112,19 @@ Section FG_stack. (* Fine-grained push *) Lemma FG_push_folding (st : expr) : FG_push st = - Rec (App (Rec - (* try push *) - (If (CAS (st.[ren (+4)]) (Var 1) - (Alloc (InjR (Pair (Var 3) (Fold (Var 1))))) - ) - Unit (* push succeeds we return unit *) - (App (Var 2) (Var 3)) (* push fails, we try again *) - ) - ) - (Load st.[ren (+2)]) (* read the stack pointer *) - ). + Rec + (LetIn + (Load st.[ren (+2)]) + (* try push *) + (If (CAS (st.[ren (+3)]) (Var 0) + (Alloc (InjR (Pair (Var 2) (Fold (Var 0))))) + ) + Unit (* push succeeds we return unit *) + (App (Var 1) (Var 2)) (* push fails, we try again *) + ) + ). Proof. trivial. Qed. - Section FG_push_type. - Lemma FG_push_type st Γ τ : - typed Γ st (Tref (FG_Stack_Ref_Type τ)) → - typed Γ (FG_push st) (TArrow τ TUnit). - Proof. - intros HTst. - repeat match goal with - |- typed _ _ _ => econstructor; eauto - end; repeat econstructor; eauto. - - eapply (context_weakening [_; _; _; _]); eauto. - - by asimpl. - - eapply (context_weakening [_; _]); eauto. - Qed. - - End FG_push_type. Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st). Proof. trivial. Qed. @@ -151,83 +132,95 @@ Section FG_stack. Lemma FG_push_of_val st : of_val (FG_pushV st) = FG_push st. Proof. trivial. Qed. + Global Typeclasses Opaque FG_pushV. Global Opaque FG_pushV. - Lemma FG_push_closed (st : expr) : - (∀ f, st.[f] = st) → ∀ f, (FG_push st).[f] = FG_push st. - Proof. intros H f. asimpl. unfold FG_push. rewrite ?H; trivial. Qed. + Lemma FG_push_type st Γ τ : + typed Γ st (Tref (FG_Stack_Ref_Type τ)) → + typed Γ (FG_push st) (TArrow τ TUnit). + Proof. + intros ?. + do 2 econstructor. + { econstructor; eapply (context_weakening [_; _]); eauto. } + econstructor; eauto using typed. + econstructor; eauto using typed; repeat econstructor. + - eapply (context_weakening [_; _; _]); eauto. + - by asimpl. + Qed. - Lemma FG_push_subst (st : expr) f : (FG_push st).[f] = FG_push st.[f]. - Proof. unfold FG_push. by asimpl. Qed. + Lemma FG_push_subst (st : expr) f : + (FG_push st).[f] = FG_push st.[f]. + Proof. by rewrite /FG_push; asimpl. Qed. + Hint Rewrite FG_push_subst : autosubst. + + Global Typeclasses Opaque FG_push. Global Opaque FG_push. (* Fine-grained push *) Lemma FG_pop_folding (st : expr) : FG_pop st = - Rec (App (Rec - ( App - (Rec - ( - Case (Var 1) - (InjL Unit) - ( (* try popping *) - If - (CAS - (st.[ren (+7)]) - (Var 4) - (Unfold (Snd (Var 0))) - ) - (InjR (Fst (Var 0))) (* pop succeeds *) - (App (Var 5) (Var 6)) (* pop fails, we retry*) - ) - ) - ) - ( - (Load (Var 1)) - ) - ) - ) - (Load st.[ren (+ 2)]) - ). + Rec + (LetIn + (Load st.[ren (+ 2)]) + (LetIn + (Load (Var 0)) + (Case + (Var 0) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+5)]) + (Var 2) + (Unfold (Snd (Var 0))) + ) + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 3) (Var 4)) (* pop fails, we retry*) + ) + ) + ) + ). Proof. trivial. Qed. - Section FG_pop_type. - - Lemma FG_pop_type st Γ τ : - typed Γ st (Tref (FG_Stack_Ref_Type τ)) → - typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)). - Proof. - replace (FG_Stack_Ref_Type τ) with - (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).[FG_StackType τ/]; - last first. - { by asimpl. } - intros HTst. - repeat match goal with - |- typed _ _ _ => econstructor; eauto - end; repeat econstructor; eauto; last first. - - eapply (context_weakening [_; _]); eauto. - - by asimpl. - - eapply (context_weakening [_; _; _; _; _; _; _]); eauto. - - econstructor. - Qed. - End FG_pop_type. - Lemma FG_pop_to_val st : to_val (FG_pop st) = Some (FG_popV st). Proof. trivial. Qed. - Lemma FG_pop_of_val st : of_val (FG_popV st) = FG_pop st. Proof. trivial. Qed. + Global Typeclasses Opaque FG_popV. Global Opaque FG_popV. - Lemma FG_pop_closed (st : expr) : - (∀ f, st.[f] = st) → ∀ f, (FG_pop st).[f] = FG_pop st. - Proof. intros H f. asimpl. unfold FG_pop. rewrite ?H; trivial. Qed. + Lemma FG_pop_type st Γ τ : + typed Γ st (Tref (FG_Stack_Ref_Type τ)) → + typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)). + Proof. + replace (FG_Stack_Ref_Type τ) with + (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).[FG_StackType τ/]; + last first. + { by asimpl. } + intros ?. + do 2 econstructor. + { econstructor. eapply (context_weakening [_; _]); eauto. } + econstructor. + { repeat econstructor. } + econstructor. + { repeat econstructor. } + { repeat econstructor. } + econstructor. + - econstructor; + [|eapply (context_weakening [_; _; _; _; _]); eauto| |]; + repeat econstructor. + - by repeat econstructor; asimpl. + - repeat econstructor. + Qed. Lemma FG_pop_subst (st : expr) f : (FG_pop st).[f] = FG_pop st.[f]. Proof. unfold FG_pop. by asimpl. Qed. + Hint Rewrite FG_pop_subst : autosubst. + + Global Typeclasses Opaque FG_pop. Global Opaque FG_pop. (* Fine-grained iter *) @@ -236,8 +229,9 @@ Section FG_stack. Rec (Case (Load (Unfold (Var 1))) Unit - (App (Rec (App (Var 3) (Snd (Var 2)))) (* recursive_call *) - (App f.[ren (+3)] (Fst (Var 0))) + (Seq + (App f.[ren (+3)] (Fst (Var 0))) + (App (Var 1) (Snd (Var 0))) (* recursive_call *) ) ). Proof. trivial. Qed. @@ -265,14 +259,12 @@ Section FG_stack. Proof. trivial. Qed. Global Opaque FG_popV. - - Lemma FG_iter_closed (f : expr) : - (∀ g, f.[g] = f) → ∀ g, (FG_iter f).[g] = FG_iter f. - Proof. intros H g. asimpl. unfold FG_iter. rewrite ?H; trivial. Qed. - Lemma FG_iter_subst (f : expr) g : (FG_iter f).[g] = FG_iter f.[g]. Proof. unfold FG_iter. by asimpl. Qed. + Hint Rewrite FG_iter_subst : autosubst. + + Global Typeclasses Opaque FG_iter. Global Opaque FG_iter. Lemma FG_read_iter_type st Γ τ : @@ -282,77 +274,64 @@ Section FG_stack. Proof. intros H1; repeat econstructor. - eapply FG_iter_type; by constructor. - - by eapply (context_weakening [_;_]); asimpl. - Qed. - - Transparent FG_iter. - - Lemma FG_read_iter_closed (st : expr) : - (∀ f, st.[f] = st) → - ∀ f, (FG_read_iter st).[f] = FG_read_iter st. - Proof. - intros H1 f. unfold FG_read_iter, FG_iter. asimpl. - by rewrite ?H1. + - by eapply (context_weakening [_]); asimpl. Qed. Lemma FG_read_iter_subst (st : expr) g : (FG_read_iter st).[g] = FG_read_iter st.[g]. Proof. by unfold FG_read_iter; asimpl. Qed. - Global Opaque FG_iter. + Hint Rewrite FG_read_iter_subst : autosubst. - Section FG_stack_body_type. - - Lemma FG_stack_body_type st Γ τ : - typed Γ st (Tref (FG_Stack_Ref_Type τ)) → - typed Γ (FG_stack_body st) - (TProd - (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ))) - (TArrow (TArrow τ TUnit) TUnit) - ). - Proof. - intros H1. - repeat (econstructor; eauto using FG_push_type, - FG_pop_type, FG_read_iter_type). - Qed. - End FG_stack_body_type. + Global Typeclasses Opaque FG_read_iter. + Global Opaque FG_read_iter. - Opaque FG_read_iter. - - Lemma FG_stack_body_closed (st : expr) : - (∀ f, st.[f] = st) → - ∀ f, (FG_stack_body st).[f] = FG_stack_body st. + Lemma FG_stack_body_type st Γ τ : + typed Γ st (Tref (FG_Stack_Ref_Type τ)) → + typed Γ (FG_stack_body st) + (TProd + (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ))) + (TArrow (TArrow τ TUnit) TUnit) + ). Proof. - intros H1 f. unfold FG_stack_body. asimpl. - rewrite FG_push_closed; trivial. - rewrite FG_pop_closed; trivial. - by rewrite FG_read_iter_closed. + intros H1. + repeat (econstructor; eauto using FG_push_type, + FG_pop_type, FG_read_iter_type). Qed. - Section FG_stack_type. - - Lemma FG_stack_type Γ : - typed Γ FG_stack - (TForall - (TProd - (TProd - (TArrow (TVar 0) TUnit) - (TArrow TUnit (TSum TUnit (TVar 0))) - ) - (TArrow (TArrow (TVar 0) TUnit) TUnit) - )). - Proof. - repeat econstructor. - - eapply FG_push_type; try constructor; simpl; eauto. - - eapply FG_pop_type; try constructor; simpl; eauto. - - eapply FG_read_iter_type; constructor; by simpl. - Qed. - End FG_stack_type. + Opaque FG_read_iter. + + Lemma FG_stack_body_subst (st : expr) f : + (FG_stack_body st).[f] = FG_stack_body st.[f]. + Proof. by unfold FG_stack_body; asimpl. Qed. - Lemma FG_stack_closed f : FG_stack.[f] = FG_stack. + Hint Rewrite FG_stack_body_subst : autosubst. + + Lemma FG_stack_type Γ : + typed Γ FG_stack + (TForall + (TProd + (TProd + (TArrow (TVar 0) TUnit) + (TArrow TUnit (TSum TUnit (TVar 0))) + ) + (TArrow (TArrow (TVar 0) TUnit) TUnit) + )). Proof. - unfold FG_stack. - asimpl; rewrite ?FG_push_subst ?FG_pop_subst. - asimpl. rewrite ?FG_read_iter_subst. by asimpl. + repeat econstructor. + - eapply FG_push_type; try constructor; simpl; eauto. + - eapply FG_pop_type; try constructor; simpl; eauto. + - eapply FG_read_iter_type; constructor; by simpl. Qed. + + Lemma FG_stack_closed f : FG_stack.[f] = FG_stack. + Proof. by unfold FG_stack; asimpl. Qed. + End FG_stack. + +Global Hint Rewrite FG_push_subst : autosubst. +Global Hint Rewrite FG_pop_subst : autosubst. +Global Hint Rewrite FG_iter_subst : autosubst. +Global Hint Rewrite FG_read_iter_subst : autosubst. +Global Hint Rewrite FG_stack_body_subst : autosubst. +Global Hint Rewrite FG_stack_closed : autosubst. diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v index 82f3405b3ca7cc6f67d7d31fa257dae466799782..007a77e24e64ab4ae4c21165237b3d23d203fe10 100644 --- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v +++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v @@ -21,27 +21,23 @@ Section Stack_refinement. Proof. (* executing the preambles *) iIntros (Δ [|??] ρ ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first. - { iDestruct (interp_env_length with "HΓ") as %[=]. } + { iDestruct (interp_env_length with "HΓ") as %[=]. } 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. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iApply wp_pure_step_later; auto. iNext. - iMod (steps_newlock _ _ j (AppRCtx (RecV _) :: K) with "[Hj]") + iMod (steps_newlock _ _ j (LetInCtx _ :: K) with "[$Hj]") as (l) "[Hj Hl]"; eauto. - 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. + iMod (do_step_pure _ _ j K with "[$Hj]") as "Hj"; eauto. simpl. iAsimpl. - iMod (step_alloc _ _ j (AppRCtx (RecV _) :: K) with "[Hj]") - as (stk') "[Hj Hstk']"; [| |simpl; by iFrame|]; auto. - iMod (step_rec _ _ j K with "[$Hj]") as "Hj"; eauto. + iMod (step_alloc _ _ j (LetInCtx _ :: K) with "[$Hj]") + as (stk') "[Hj Hstk']"; eauto. simpl. - rewrite CG_locked_push_subst CG_locked_pop_subst - CG_iter_subst CG_snap_subst. simpl. iAsimpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iAsimpl. iApply (wp_bind (fill [AllocCtx; AppRCtx (RecV _)])); iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. iApply wp_alloc; first done. iNext; iIntros (istk) "Histk". @@ -49,7 +45,7 @@ Section Stack_refinement. iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk". simpl. iApply wp_pure_step_later; trivial. iNext. simpl. - rewrite FG_push_subst FG_pop_subst FG_iter_subst. simpl. iAsimpl. + iAsimpl. (* establishing the invariant *) iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done. set (istkG := StackG _ _ γ). @@ -75,8 +71,11 @@ Section Stack_refinement. Opaque stack_owns. (* splitting *) iApply wp_value; simpl; trivial. - iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)). - simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj". + iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (LamV _)). + simpl. iAsimpl. + rewrite CG_locked_push_of_val CG_locked_pop_of_val. + Transparent CG_snap_iter. + iFrame "Hj". iExists (_, _), (_, _); iSplit; eauto. iSplit. (* refinement of push and pop *) @@ -90,7 +89,7 @@ Section Stack_refinement. iNext. rewrite -(FG_push_folding (Loc stk)). iAsimpl. - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [LetInCtx _])); 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". @@ -140,7 +139,7 @@ Section Stack_refinement. iApply wp_pure_step_later; auto. iNext. rewrite -(FG_pop_folding (Loc stk)). iAsimpl. - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [LetInCtx _])); 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". @@ -149,6 +148,7 @@ Section Stack_refinement. rewrite {2}StackLink_unfold. iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=. * (* The stack is empty *) + rewrite CG_locked_pop_of_val. iMod (steps_CG_locked_pop_fail with "[$Hspec $Hstk' $Hl $Hj]") as "[Hj [Hstk' Hl]]"; first solve_ndisj. iMod ("Hclose" with "[-Hj Hmpt]") as "_". @@ -156,7 +156,7 @@ Section Stack_refinement. iModIntro. iApply wp_pure_step_later; auto. iNext. iAsimpl. clear h. - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [LetInCtx _])); iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|]. iClear "HLK". iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". @@ -176,7 +176,7 @@ Section Stack_refinement. iModIntro. iApply wp_pure_step_later; auto. iNext. iAsimpl. clear h. - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [LetInCtx _])); iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. iClear "HLK". iInv stackN as (istk3 w' h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose". @@ -241,8 +241,8 @@ Section Stack_refinement. - (* refinement of iter *) iAlways. clear j K. iIntros ( [f1 f2] ) "/= #Hfs". iIntros (j K) "Hj". iApply wp_pure_step_later; auto using to_of_val. iNext. - iMod (step_rec with "[$Hspec $Hj]") as "Hj"; [by rewrite to_of_val|solve_ndisj|]. - iAsimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. iAsimpl. + iMod (do_step_pure with "[$Hspec $Hj]") as "Hj"; eauto. + iAsimpl. 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))) @@ -261,7 +261,7 @@ Section Stack_refinement. iLöb as "Hlat" forall (istk3 w) "HLK". rewrite {2}FG_iter_folding. iApply wp_pure_step_later; simpl; trivial. - rewrite -FG_iter_folding. iAsimpl. rewrite FG_iter_subst. + rewrite -FG_iter_folding. iAsimpl. iNext. iApply (wp_bind (fill [LoadCtx; CaseCtx _ _])); iApply wp_wand_l; iSplitR; [iIntros (v) "Hw"; iExact "Hw"|]. @@ -289,29 +289,29 @@ Section Stack_refinement. { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk Hl". } simpl. iApply wp_pure_step_later; simpl; rewrite ?to_of_val; trivial. - rewrite FG_iter_subst CG_iter_subst. iAsimpl. + iAsimpl. iModIntro. iNext. - iApply (wp_bind (fill [AppRCtx _; AppRCtx (RecV _)])); + iApply (wp_bind (fill [AppRCtx _; SeqCtx _])); iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|]. iApply wp_pure_step_later; simpl; rewrite ?to_of_val; trivial. iNext. iApply wp_value. - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [SeqCtx _])); 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" $! _ (AppRCtx (RecV _) :: K)). + iSpecialize ("Hfs" $! _ (SeqCtx _ :: K)). iApply wp_wand_l; iSplitR "Hj"; [|iApply "Hfs"; by iFrame "#"]. iIntros (u) "/="; iDestruct 1 as (z) "[Hj [% %]]". simpl. subst. iAsimpl. - iMod (step_rec with "[$Hspec $Hj]") as "Hj"; [done..|]. - iAsimpl. rewrite CG_iter_subst. iAsimpl. + iMod (do_step_pure with "[$Hspec $Hj]") as "Hj"; [done..|]. + iAsimpl. replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (by rewrite CG_iter_of_val). iMod (step_snd _ _ _ (AppRCtx _ :: K) with "[$Hspec Hj]") as "Hj"; [| | |simpl; by iFrame "Hj"|]; rewrite ?to_of_val; auto. iApply wp_pure_step_later; trivial. - iNext. simpl. rewrite FG_iter_subst. iAsimpl. + iNext. simpl. replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) by (by rewrite FG_iter_of_val). iApply (wp_bind (fill [AppRCtx _]));