Simplify stack programs

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.

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 _]));