diff --git a/theories/logrel/F_mu_ref_conc/examples/counter.v b/theories/logrel/F_mu_ref_conc/examples/counter.v index 59d5cf0d24b6e27f46645e79d7f3eb6d105ffd36..58eb59066c38fe26e9eec863aa063ebf84176f09 100644 --- a/theories/logrel/F_mu_ref_conc/examples/counter.v +++ b/theories/logrel/F_mu_ref_conc/examples/counter.v @@ -5,36 +5,32 @@ From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary. From iris.program_logic Require Import adequacy. Definition CG_increment (x : expr) : expr := - Rec (Store x.[ren (+ 2)] (BinOp Add (#n 1) (Load x.[ren (+ 2)]))). + Lam (Store x.[ren (+ 1)] (BinOp Add (#n 1) (Load x.[ren (+ 1)]))). Definition CG_locked_increment (x l : expr) : expr := with_lock (CG_increment x) l. Definition CG_locked_incrementV (x l : expr) : val := with_lockV (CG_increment x) l. -Definition counter_read (x : expr) : expr := Rec (Load x.[ren (+2)]). -Definition counter_readV (x : expr) : val := RecV (Load x.[ren (+2)]). +Definition counter_read (x : expr) : expr := Lam (Load x.[ren (+1)]). +Definition counter_readV (x : expr) : val := LamV (Load x.[ren (+1)]). Definition CG_counter_body (x l : expr) : expr := Pair (CG_locked_increment x l) (counter_read x). Definition CG_counter : expr := - App - (Rec $ App (Rec (CG_counter_body (Var 1) (Var 3))) - (Alloc (#n 0))) - newlock. + LetIn newlock (LetIn (Alloc (#n 0)) (CG_counter_body (Var 0) (Var 1))). Definition FG_increment (x : expr) : expr := - Rec $ App - (Rec $ - (* try increment *) - If (CAS x.[ren (+4)] (Var 1) (BinOp Add (#n 1) (Var 1))) - Unit (* increment succeeds we return unit *) - (App (Var 2) (Var 3)) (* increment fails, we try again *)) - (Load x.[ren (+2)]) (* read the counter *). + Rec (LetIn + (Load x.[ren (+2)]) (* read the counter *) + (* try increment *) + (If (CAS x.[ren (+3)] (Var 0) (BinOp Add (#n 1) (Var 0))) + Unit (* increment succeeds we return unit *) + (App (Var 1) (Var 2)) (* increment fails, we try again *))). Definition FG_counter_body (x : expr) : expr := Pair (FG_increment x) (counter_read x). Definition FG_counter : expr := - App (Rec (FG_counter_body (Var 1))) (Alloc (#n 0)). + LetIn (Alloc (#n 0)) (FG_counter_body (Var 0)). Section CG_Counter. Context `{heapIG Σ, cfgSG Σ}. @@ -48,37 +44,38 @@ Section CG_Counter. typed Γ (CG_increment x) (TArrow TUnit TUnit). Proof. intros H1. repeat econstructor. - - eapply (context_weakening [_; _]); eauto. - - eapply (context_weakening [_; _]); eauto. + - eapply (context_weakening [_]); eauto. + - eapply (context_weakening [_]); eauto. Qed. Lemma CG_increment_closed (x : expr) : (∀ f, x.[f] = x) → ∀ f, (CG_increment x).[f] = CG_increment x. Proof. intros Hx f. unfold CG_increment. asimpl. rewrite ?Hx; trivial. Qed. + Hint Rewrite CG_increment_closed : autosubst. + Lemma CG_increment_subst (x : expr) f : (CG_increment x).[f] = CG_increment x.[f]. Proof. unfold CG_increment; asimpl; trivial. Qed. + Hint Rewrite CG_increment_subst : autosubst. + 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)). Proof. iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iMod (step_load _ _ j ((BinOpRCtx _ (#nv _) :: StoreRCtx (LocV _) :: K)) _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - simpl. iFrame "Hspec Hj"; trivial. + { iFrame "Hspec Hj"; trivial. } simpl. - iMod (step_nat_binop _ _ j ((StoreRCtx (LocV _)) :: K) - _ _ _ with "[Hj]") as "Hj"; eauto. + iMod (do_step_pure _ _ _ ((StoreRCtx (LocV _)) :: K) with "[$Hj]") as "Hj"; + eauto. simpl. - iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. - iFrame "Hspec Hj"; trivial. - iModIntro. - iFrame "Hj Hx"; trivial. - Unshelve. all: trivial. + iMod (step_store _ _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto. + iModIntro; iFrame. Qed. Global Opaque CG_increment. @@ -102,14 +99,6 @@ Section CG_Counter. eapply with_lock_type; auto using CG_increment_type. Qed. - Lemma CG_locked_increment_closed (x l : expr) : - (∀ f, x.[f] = x) → (∀ f, l.[f] = l) → - ∀ f, (CG_locked_increment x l).[f] = CG_locked_increment x l. - Proof. - intros H1 H2 f. asimpl. unfold CG_locked_increment. - rewrite with_lock_closed; trivial. apply CG_increment_closed; trivial. - Qed. - Lemma CG_locked_increment_subst (x l : expr) f : (CG_locked_increment x l).[f] = CG_locked_increment x.[f] l.[f]. Proof. @@ -117,6 +106,8 @@ Section CG_Counter. rewrite with_lock_subst CG_increment_subst. asimpl; trivial. Qed. + Hint Rewrite CG_locked_increment_subst : autosubst. + Lemma steps_CG_locked_increment E ρ j K x n l : nclose specN ⊆ E → spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#♭v false) @@ -125,11 +116,10 @@ Section CG_Counter. Proof. iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". iMod (steps_with_lock - _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last done. + _ _ j K _ _ _ _ UnitV UnitV with "[$Hj Hx $Hl]") as "Hj"; eauto. - iIntros (K') "[#Hspec Hxj]". - iApply steps_CG_increment; first done. iFrame. trivial. - - by iFrame "Hspec Hj Hx". - Unshelve. all: trivial. + iApply steps_CG_increment; by try iFrame. + - by iFrame. Qed. Global Opaque CG_locked_increment. @@ -146,17 +136,21 @@ Section CG_Counter. typed Γ x (Tref TNat) → typed Γ (counter_read x) (TArrow TUnit TNat). Proof. intros H1. repeat econstructor. - eapply (context_weakening [_; _]); trivial. + eapply (context_weakening [_]); trivial. Qed. Lemma counter_read_closed (x : expr) : (∀ f, x.[f] = x) → ∀ f, (counter_read x).[f] = counter_read x. Proof. intros H1 f. asimpl. unfold counter_read. by rewrite ?H1. Qed. + Hint Rewrite counter_read_closed : autosubst. + Lemma counter_read_subst (x: expr) f : (counter_read x).[f] = counter_read x.[f]. Proof. unfold counter_read. by asimpl. Qed. + Hint Rewrite counter_read_subst : autosubst. + Lemma steps_counter_read E ρ j K x n : nclose specN ⊆ E → spec_ctx ρ ∗ x ↦ₛ (#nv n) @@ -164,11 +158,10 @@ Section CG_Counter. ={E}=∗ j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n). Proof. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read. - iMod (step_rec _ _ j K _ Unit 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. - { by iFrame "Hspec Hj". } - iModIntro. by iFrame "Hj Hx". + iMod (step_load _ _ j K with "[$Hj Hx]") as "[Hj Hx]"; eauto. + by iFrame. Qed. Opaque counter_read. @@ -183,45 +176,43 @@ Section CG_Counter. eauto using CG_locked_increment_type, counter_read_type. Qed. - Lemma CG_counter_body_closed (x l : expr) : - (∀ f, x.[f] = x) → (∀ f, l.[f] = l) → - ∀ f, (CG_counter_body x l).[f] = CG_counter_body x l. - Proof. - intros H1 H2 f. asimpl. - rewrite CG_locked_increment_closed; trivial. by rewrite counter_read_closed. - Qed. + Lemma CG_counter_body_subst (x l : expr) f : + (CG_counter_body x l).[f] = CG_counter_body x.[f] l.[f]. + Proof. by asimpl. Qed. + + Hint Rewrite CG_counter_body_subst : autosubst. Lemma CG_counter_type Γ : typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)). Proof. econstructor; eauto using newlock_type. - do 2 econstructor; [|do 2 constructor]. - constructor. apply CG_counter_body_type; by constructor. + econstructor; first eauto using typed. + apply CG_counter_body_type; eauto using typed. Qed. Lemma CG_counter_closed f : CG_counter.[f] = CG_counter. - Proof. - asimpl; rewrite CG_locked_increment_subst counter_read_subst; by asimpl. - Qed. + Proof. by asimpl. Qed. + + Hint Rewrite CG_counter_closed : autosubst. (* Fine-grained increment *) Lemma FG_increment_type x Γ : typed Γ x (Tref TNat) → typed Γ (FG_increment x) (TArrow TUnit TUnit). Proof. - intros H1. do 3 econstructor. - do 2 econstructor; eauto using EqTNat. - - eapply (context_weakening [_; _; _; _]); eauto. - - by constructor. - - repeat constructor. - - by constructor. - - by constructor. + intros Hx. do 3 econstructor; eauto using typed. - eapply (context_weakening [_; _]); eauto. + - econstructor; [| |repeat econstructor |]. + + constructor. + + eapply (context_weakening [_; _; _]); eauto. + + repeat constructor. Qed. - Lemma FG_increment_closed (x : expr) : - (∀ f, x.[f] = x) → ∀ f, (FG_increment x).[f] = FG_increment x. - Proof. intros Hx f. asimpl. unfold FG_increment. rewrite ?Hx; trivial. Qed. + Lemma FG_increment_subst (x : expr) f : + (FG_increment x).[f] = FG_increment x.[f]. + Proof. rewrite /FG_increment. by asimpl. Qed. + + Hint Rewrite FG_increment_subst : autosubst. Lemma FG_counter_body_type x Γ : typed Γ x (Tref TNat) → @@ -233,23 +224,23 @@ Section CG_Counter. - apply counter_read_type; trivial. Qed. - Lemma FG_counter_body_closed (x : expr) : - (∀ f, x.[f] = x) → - ∀ f, (FG_counter_body x).[f] = FG_counter_body x. - Proof. - intros H1 f. asimpl. unfold FG_counter_body, FG_increment. - rewrite ?H1. by rewrite counter_read_closed. - Qed. + Lemma FG_counter_body_subst (x : expr) f : + (FG_counter_body x).[f] = FG_counter_body x.[f]. + Proof. rewrite /FG_counter_body /FG_increment. by asimpl. Qed. + + Hint Rewrite FG_counter_body_subst : autosubst. Lemma FG_counter_type Γ : - typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)). + Γ ⊢ₜ FG_counter : (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)). Proof. econstructor; eauto using newlock_type, typed. - constructor. apply FG_counter_body_type; by constructor. + apply FG_counter_body_type; by constructor. Qed. Lemma FG_counter_closed f : FG_counter.[f] = FG_counter. - Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed. + Proof. by asimpl. Qed. + + Hint Rewrite FG_counter_closed : autosubst. Definition counterN : namespace := nroot .@ "counter". @@ -261,20 +252,17 @@ 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 ((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. - iAsimpl. rewrite CG_locked_increment_subst /=. - rewrite counter_read_subst /=. - iMod (step_alloc _ _ j ((AppRCtx (RecV _)) :: K) _ _ _ _ with "[Hj]") + simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iAsimpl. + iMod (step_alloc _ _ j (LetInCtx _ :: K) with "[$Hj]") as (cnt') "[Hj Hcnt']"; eauto. - iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. - iAsimpl. rewrite CG_locked_increment_subst /=. - rewrite counter_read_subst /=. - Unshelve. - all: try match goal with |- to_val _ = _ => auto using to_of_val end. - all: trivial. - iApply (wp_bind (fill [AppRCtx (RecV _)])). + simpl. + iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. + iAsimpl. + iApply (wp_bind (fill [LetInCtx _])). iApply wp_wand_l. iSplitR; [iModIntro; iIntros (v) "Hv"; iExact "Hv"|]. iApply (wp_alloc); trivial; iFrame "#"; iModIntro; iNext; iIntros (cnt) "Hcnt /=". (* establishing the invariant *) @@ -285,7 +273,6 @@ Section CG_Counter. iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; [iNext; iExact "Hinv"|]. (* splitting increment and read *) iApply wp_pure_step_later; trivial. iModIntro. iNext. iAsimpl. - rewrite counter_read_subst /=. iApply wp_value; auto. iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl. rewrite CG_locked_increment_of_val counter_read_of_val. @@ -298,7 +285,7 @@ Section CG_Counter. iLöb as "Hlat". iApply wp_pure_step_later; trivial. iAsimpl. iNext. (* fine-grained reads the counter *) - iApply (wp_bind (fill [AppRCtx (RecV _)])); + iApply (wp_bind (fill [LetInCtx _])); iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. iApply wp_atomic; eauto. iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".