Improve counter

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".