[F_mu_ref_conc] port FG_ and CG_ to tp tactics

F_mu_ref_conc/examples/stack/CG_stack.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import namespaces.
-From iris_logrel.F_mu_ref_conc Require Import examples.lock.
+From iris_logrel.F_mu_ref_conc Require Import tactics examples.lock.
 Import uPred.
 
+(* Stack τ = μ x. Unit + (τ * x), essentially a type of lists *)
+(* writing nil and cons for "constructors" *)
 Definition CG_StackType τ :=
   TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).
 
 (* Coarse-grained push *)
+(* push s = λ x. s <- fold (injr (x, load st)) *)
+(* push s = λ x. s <- cons (x, load st) *)
 Definition CG_push (st : expr) : expr :=
   Rec (Store
          (st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).
@@ -14,6 +18,10 @@ Definition CG_push (st : expr) : expr :=
 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.
 
+(* pop s = λ x. match (load s) with
+                | nil => InjL ()
+                | cons y ys => s <- ys ;; InjR y 
+                end *)
 Definition CG_pop (st : expr) : expr :=
   Rec (Case (Unfold (Load st.[ren (+ 2)]))
             (InjL Unit)
@@ -26,9 +34,14 @@ Definition CG_pop (st : expr) : expr :=
 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.
 
+(* snap st l = with_lock (λ _, load 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.
 
+(* iter f = λ s. match s with
+                 | nil => Unit
+                 | cons x xs => (f x) ;; iter f xs
+                 end *)
 Definition CG_iter (f : expr) : expr :=
   Rec (Case (Unfold (Var 1))
             Unit
@@ -47,12 +60,18 @@ Definition CG_iterV (f : expr) : val :=
             )
       ).
 
+(* snap_iter st l := λ f. iter f (snap st l #()) *)
 Definition CG_snap_iter (st l : expr) : expr :=
   Rec (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
+
+(* stack_body st l :=
+   ⟨locked_push st l, locked_pop st l, snap_iter st l⟩ *)
 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).
 
+(* stack :=
+   Λα. (λ(l : lock) (s : stack α). stack_body s l) (ref nil) newlock *)
 Definition CG_stack : expr :=
   TLam (App (Rec (App (Rec (CG_stack_body (Var 1) (Var 3)))
                 (Alloc (Fold (InjL Unit))))) newlock).
@@ -83,20 +102,11 @@ Section CG_Stack.
     ⊢ |={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.
-    asimpl.
-    iMod (step_load _ _ j (K ++ [StoreRCtx (LocV _); FoldCtx;
-                                   InjRCtx; PairRCtx _])
-                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
-    { by iFrame. }
-    iModIntro. by iFrame.
-    Unshelve.
-    all: try match goal with |- to_val _ = _ => auto using to_of_val end.
-    simpl; by rewrite ?to_of_val.
+    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.
@@ -138,12 +148,14 @@ Section CG_Stack.
       ∗ 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.
-    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 [Hx Hj]]".
-      iApply steps_CG_push; first done. iFrame "Hspec Hj Hx"; trivial.
-    - iFrame "Hspec Hj Hx"; trivial.
+    iIntros (?) "(#Hspec & Hst & Hl & Hj)".
+    unfold CG_locked_push.
+    (* TODO would be nice to be able to determine that e := Loc l for instance *)
+    iMod (steps_with_lock _ _ j K (CG_push (Loc st)) l _ _ UnitV _ _ _ with "[Hspec Hst Hj Hl]") as "Hj"; last done. 
+    - iIntros (K') "(#Hspec & HQ & Hj)".
+      iApply steps_CG_push; first eauto.
+      iFrame "Hspec Hj". iFrame "HQ".
+    - by iFrame. 
       Unshelve. all: trivial.
   Qed.
 
@@ -180,40 +192,16 @@ 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.
-    asimpl.
-    iMod (step_load _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
-                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    iMod (step_Fold  _ _ j (K ++ [CaseCtx _ _])
-                    _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    asimpl.
-    iMod (step_snd _ _ j (K ++ [AppRCtx (RecV _); StoreRCtx (LocV _)]) _ _ _ _
-                   _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    iMod (step_store _ _ j (K ++ [AppRCtx (RecV _)]) _ _ _ _ _ _
-          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.
-    asimpl.
-    iMod (step_fst _ _ j (K ++ [InjRCtx]) _ _ _ _ _ _
-          with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial. asimpl.
-    rewrite ?fill_app. simpl.
-    iModIntro. iFrame "Hj Hx"; trivial.
-    Unshelve.
-    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
-    all: trivial.
+    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 :
@@ -223,24 +211,11 @@ 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.
-    asimpl.
-    iMod (step_load _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
-                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
-                    _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app. simpl.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    asimpl.
-    iModIntro. iFrame "Hj Hx"; trivial.
-    Unshelve.
-    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
-    all: trivial.
+    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.
@@ -349,15 +324,10 @@ Section CG_Stack.
     iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
           with "[Hj Hx Hl]") as "Hj"; last done; [|by iFrame "Hspec Hx Hl Hj"].
     iIntros (K') "[#Hspec [Hx Hj]]".
-    iMod (step_rec _ _ j K' _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    asimpl.
-    iMod (step_load _ _ j K' _ _ _ _
-          with "[Hj Hx]") as "[Hj Hx]"; eauto.
-    - by iFrame "Hspec Hj Hx".
-    - iModIntro. by iFrame "Hj Hx".
-      Unshelve.
-      all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
-      all: trivial.
+    tp_rec j.
+    tp_load j. tp_normalise j.
+    by iFrame.
+    Unshelve. all: trivial.
   Qed.
 
   Global Opaque CG_snap.
@@ -418,24 +388,15 @@ Section CG_Stack.
              (App (of_val f) (of_val w))).
   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. asimpl.
-    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
-                    _ _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app /=.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. asimpl.
-    iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
+    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.
-    iMod (step_fst _ _ j (K ++ [AppRCtx (RecV _); AppRCtx f]) _ _ _ _
-                   _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app /=.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. simpl.
-    by iModIntro.
-    Unshelve.
-    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
-  Qed.
+    tp_fst j; auto using to_of_val.
+    tp_normalise j.
+    done.
+  Qed. 
 
   Transparent CG_iter.
 
@@ -445,16 +406,10 @@ Section CG_Stack.
       ⊢ |={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. asimpl.
-    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
-                    _ _ _ with "[Hj]") as "Hj"; eauto.
-    rewrite ?fill_app /=.
-    iFrame "Hspec Hj"; trivial.
-    rewrite ?fill_app. asimpl.
-    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.
+    tp_rec j. 
+    tp_fold j.
+    tp_case_inl j. tp_normalise j. 
+    by iFrame.
   Qed.
 
   Global Opaque CG_iter.
@@ -510,6 +465,8 @@ Section CG_Stack.
     by rewrite CG_snap_iter_closed.
   Qed.
 
+  (* CG_stack 
+    : ∀ α. ((α → Unit) * (Unit → Unit + α) * ((α → Unit) → Unit))  *)
   Lemma CG_stack_type Γ :
     typed Γ CG_stack
           (TForall

F_mu_ref_conc/examples/stack/FG_stack.v

 From iris_logrel.F_mu_ref_conc Require Import  typing.
 
+(* stack τ = μ x. ref (Unit + τ * x) *)
 Definition FG_StackType τ :=
   TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
 
+(* push st = λ x.
+   (λ stv. if (CAS(st, stv, ref (cons x stv)))
+           #() 
+           (push st x)) (load st)  *)
 Definition FG_push (st : expr) : expr :=
   Rec (App (Rec
               (* try push *)
@@ -28,6 +33,16 @@ Definition FG_pushV (st : expr) : val :=
            (Load st.[ren (+2)]) (* read the stack pointer *)
        ).
 
+(* pop st = λ (),
+     (λ str. 
+       (λ x. match x with 
+             | nil => InjL #()
+             | cons y ys => 
+               if CAS(st, str, ys)
+                  (InjR y)
+                  (pop st ())) 
+       (load str)) 
+     (load st)*)
 Definition FG_pop (st : expr) : expr :=
   Rec (App (Rec
               (App
@@ -83,6 +98,10 @@ Definition FG_popV (st : expr) : val :=
        (Unfold (Load st.[ren (+ 2)]))
     ).
 
+(* iter f = λ st.
+   case (load st) of
+   | nil => #()
+   | cons y ys => f y ;; iter f ys *)
 Definition FG_iter (f : expr) : expr :=
   Rec
     (Case (Load (Unfold (Var 1)))
@@ -99,12 +118,15 @@ Definition FG_iterV (f : expr) : val :=
                (App f.[ren (+3)] (Fst (Var 0)))
           )
     ).
+(* read_iter st := λf. iter f (load st) *)
 Definition FG_read_iter (st : expr) : expr :=
   Rec (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
 
+(* stack_body st = ⟨ push st, pop st, read_iter st ⟩*)
 Definition FG_stack_body (st : expr) : expr :=
   Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
 
+(* stack = Λα. (λ (s : stack α). stack_body s) (ref (ref nil)) *)
 Definition FG_stack : expr :=
   TLam (App (Rec (FG_stack_body (Var 1)))
                 (Alloc (Fold (Alloc (InjL Unit))))).
@@ -130,6 +152,8 @@ Section FG_stack.
     (* The following assumption is simply ** WRONG ** *)
     (* We assume it though to just be able to prove that the
        stack we are implementing is /type-sane/ so to speak! *)
+    (* EqType (stack τ) would mean that we can compare two stacks for
+       equality, we need this for compare-and-swap *)
     Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
 
     Lemma FG_push_type st Γ τ :