[stack] Factor out CG stack symbolic execution steps

theories/examples/stack/CG_stack.v

@@ -143,21 +143,6 @@ Section CG_Stack.
 
   Hint Resolve CG_push_type : typeable.
 
-  (* 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. *)
-  (*   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. *)
-
   Lemma CG_locked_push_type Γ τ :
     typed Γ CG_locked_push (TArrow (Tref (CG_StackType τ)) (TArrow LockType (TArrow τ TUnit))).
   Proof.
@@ -167,21 +152,29 @@ Section CG_Stack.
   
   Hint Resolve CG_locked_push_type : typeable.
 
-  (* Lemma steps_CG_locked_push E ρ j K st w v l : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ v -∗ l ↦ₛ (#♭v false) *)
-  (*   -∗ 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. *)
-  (*   iIntros (?) "#Hspec Hst Hl Hj". *)
-  (*   unfold CG_locked_push. *)
-  (*   tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ UnitV) with "Hst Hl" as "[Hst $]"; [auto | | ]. *)
-  (*   - iIntros (K') "#Hspec Hst Hj". *)
-  (*     iApply (steps_CG_push with "Hspec Hst"); auto. *)
-  (*   - by iFrame. *)
-  (* Qed. *)
-
-  (* Global Opaque CG_locked_push. *)
+  Lemma CG_push_r st' (v w : val) l E1 E2 Δ Γ t K τ :
+    nclose logrelN ⊆ E1 →
+    st' ↦ₛ v -∗ l ↦ₛ #false -∗
+    (st' ↦ₛ FoldV (InjRV (w, v)) -∗ l ↦ₛ #false
+     -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ) -∗
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) w) : τ.
+  Proof.
+    iIntros (?)"Hst' Hl Hlog".
+    unlock CG_locked_push CG_push. simpl_subst/=.
+    rel_let_r.
+    rel_apply_r (bin_log_related_acquire_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    rel_seq_r.
+    do 2 rel_let_r.
+    rel_load_r.
+    rel_store_r.
+    rel_seq_r.
+    rel_apply_r (bin_log_related_release_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    iApply ("Hlog" with "Hst' Hl").
+  Qed.
 
   (* Coarse-grained pop *)
   Lemma CG_pop_type Γ τ :
@@ -193,39 +186,6 @@ Section CG_Stack.
   Qed.
 
   Hint Resolve CG_pop_type : typeable.
-  (* Lemma steps_CG_pop_suc E ρ j K st v w : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ FoldV (InjRV (PairV w v)) *)
-  (*   -∗ j ⤇ fill K (App (CG_pop (Loc st)) Unit) *)
-  (*   ={E}=∗ j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v. *)
-  (* Proof. *)
-  (*   intros HNE. iIntros "#Hspec Hx Hj". unfold CG_pop. *)
-  (*   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 : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ FoldV (InjLV UnitV) *)
-  (*   -∗ j ⤇ fill K (App (CG_pop (Loc st)) Unit) *)
-  (*   ={E}=∗ j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV). *)
-  (* Proof. *)
-  (*   iIntros (HNE) "#Hspec Hx Hj". unfold CG_pop. *)
-  (*   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.
 
   Lemma CG_locked_pop_type Γ τ :
@@ -236,33 +196,63 @@ Section CG_Stack.
   Qed.
 
   Hint Resolve CG_locked_pop_type : typeable.
-  (* Lemma steps_CG_locked_pop_suc E ρ j K st v w l : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ FoldV (InjRV (PairV w v)) -∗ l ↦ₛ (#♭v false) *)
-  (*   -∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) *)
-  (*   ={E}=∗ j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). *)
-  (* Proof. *)
-  (*   iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. *)
-  (*   tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV) *)
-  (*            with "Hx Hl" as "[Hx $]"; first auto. *)
-  (*   - iIntros (K') "#Hspec Hx Hj". *)
-  (*     iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial. *)
-  (*   - by iFrame. *)
-  (* Qed. *)
-
-  (* Lemma steps_CG_locked_pop_fail E ρ j K st l : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ FoldV (InjLV UnitV) -∗ l ↦ₛ (#♭v false) *)
-  (*   -∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) *)
-  (*   ={E}=∗ j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false). *)
-  (* Proof. *)
-  (*   iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop. *)
-  (*   tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV) *)
-  (*            with "Hx Hl" as "[Hx Hl]"; first auto. *)
-  (*   - iIntros (K') "#Hspec Hx Hj /=". *)
-  (*     iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial. *)
-  (*   - by iFrame. *)
-  (* Qed. *)
+
+  Lemma CG_pop_suc_r st' l (w v : val) E1 E2 Δ Γ t K τ :
+    nclose logrelN ⊆ E1 →
+    st' ↦ₛ FoldV (InjRV (w, v)) -∗
+    l ↦ₛ #false -∗
+    (st' ↦ₛ v -∗ l ↦ₛ #false
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjR w) : τ) -∗
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #()) : τ.
+  Proof.
+    iIntros (?) "Hst' Hl Hlog".
+    unlock CG_locked_pop CG_pop. simpl_subst/=.
+    rel_seq_r.
+    rel_apply_r (bin_log_related_acquire_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    repeat rel_rec_r.
+    rel_load_r.
+    rel_fold_r.
+    rel_case_r.
+    rel_let_r.
+    rel_proj_r.
+    rel_store_r.
+    rel_seq_r.
+    rel_proj_r.
+    rel_rec_r.
+    rel_apply_r (bin_log_related_release_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    rel_rec_r.
+    iApply ("Hlog" with "Hst' Hl").
+  Qed.
+
+  Lemma CG_pop_fail_r st' l E1 E2 Δ Γ t K τ :
+    nclose logrelN ⊆ E1 →
+    st' ↦ₛ FoldV (InjLV #()) -∗
+    l ↦ₛ #false -∗
+    (st' ↦ₛ FoldV (InjLV #()) -∗ l ↦ₛ #false
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjL #()) : τ) -∗
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #()) : τ.
+  Proof.
+    iIntros (?) "Hst' Hl Hlog".
+    unlock CG_locked_pop CG_pop. simpl_subst/=.
+    rel_seq_r.
+    rel_apply_r (bin_log_related_acquire_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    repeat rel_rec_r.
+    rel_load_r.
+    rel_fold_r.
+    rel_case_r.
+    repeat rel_let_r.
+    rel_apply_r (bin_log_related_release_r with "Hl").
+    { solve_ndisj. }
+    iIntros "Hl /=".
+    rel_rec_r.
+    iApply ("Hlog" with "Hst' Hl").
+  Qed.
 
   Global Opaque CG_locked_pop.
 
@@ -274,36 +264,8 @@ Section CG_Stack.
   Qed.
 
   Hint Resolve CG_snap_type : typeable.
-  (* Lemma steps_CG_snap E ρ j K st v l : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ -∗ st ↦ₛ v -∗ l ↦ₛ (#♭v false) *)
-  (*   -∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit) *)
-  (*   ={E}=∗ j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false). *)
-  (* Proof. *)
-  (*   iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_snap. *)
-  (*   tp_apply j (steps_with_lock _ _ _ _ _ _ _ _ v UnitV) *)
-  (*            with "Hx Hl" as "[Hx $]"; first auto. *)
-  (*   - iIntros (K') "#Hspec Hx Hj". *)
-  (*     tp_rec j. *)
-  (*     tp_load j. tp_normalise j. *)
-  (*     by iFrame. *)
-  (*   - by iFrame. *)
-  (* Qed. *)
-
   Global Opaque CG_snap.
 
-  (* (* Coarse-grained iter *) *)
-  (* Lemma CG_iter_folding (f : expr) : *)
-  (*   CG_iter f = *)
-  (*   Rec (Case (Unfold (Var 1)) *)
-  (*             Unit *)
-  (*             ( *)
-  (*               App (Rec (App (Var 3) (Snd (Var 2)))) *)
-  (*                   (App f.[ren (+3)] (Fst (Var 0))) *)
-  (*             ) *)
-  (*       ). *)
-  (* Proof. trivial. Qed. *)
-
   Lemma CG_iter_type Γ τ :
     typed Γ CG_iter (TArrow (TArrow τ TUnit) (TArrow (CG_StackType τ) TUnit)).
   Proof.
@@ -313,44 +275,6 @@ Section CG_Stack.
   Qed.
 
   Hint Resolve CG_iter_type : typeable.
-
-  (* Lemma steps_CG_iter E ρ j K f v w : *)
-  (*   nclose specN ⊆ E → *)
-  (*   spec_ctx ρ *)
-  (*   -∗ j ⤇ fill K (App (CG_iter (of_val f)) *)
-  (*                      (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))). *)
-  (* Proof. *)
-  (*   iIntros (HNE) "#Hspec Hj". unfold CG_iter. *)
-  (*   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. *)
-  (*   tp_fst j; auto using to_of_val. *)
-  (*   tp_normalise j. *)
-  (*   done. *)
-  (* 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. *)
-  (*   tp_rec j.  *)
-  (*   tp_fold j. *)
-  (*   tp_case_inl j. tp_normalise j.  *)
-  (*   by iFrame. *)
-  (* Qed. *)
-
   Global Opaque CG_iter.
 
   Lemma CG_snap_iter_type Γ τ :

theories/examples/stack/refinement.v

@@ -28,8 +28,6 @@ Section Stack_refinement.
   Proof.
     iIntros "#Hinv #Hvv'" (Δ).
     Transparent FG_push.
-    unfold CG_locked_push. unlock. simpl_subst/=.
-    rel_rec_r.
     unfold FG_push. unlock. simpl_subst/=.
     iLöb as "IH".
     rel_rec_l.
@@ -48,17 +46,9 @@ Section Stack_refinement.
     - (* CAS succeeds *)
       iSplitR; first by iIntros ([]).
       iIntros (?). iNext. iIntros "Hst".
-      rel_apply_r (bin_log_related_acquire_r with "Hl").
+      rel_apply_r (CG_push_r with "Hst' Hl").
       { solve_ndisj. }
-      iIntros "Hl /=". 
-      rel_rec_r.
-      unfold CG_push. unlock. do 2 rel_rec_r.     
-      rel_load_r.
-      rel_store_r.
-      rel_rec_r.
-      rel_apply_r (bin_log_related_release_r with "Hl").
-      { solve_ndisj. }
-      iIntros "Hl /=".
+      iIntros "Hst' Hl".
       iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
       iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
       iModIntro.
@@ -112,22 +102,9 @@ replace ((rec: "pop" "st" <> :=
     iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
     iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
     - (* The stack is empty *)
-      rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
-      rel_rec_r.
-      rel_apply_r (bin_log_related_acquire_r with "Hl").
+      rel_apply_r (CG_pop_fail_r with "Hst' Hl").
       { solve_ndisj. }
-      iIntros "Hl /=".
-      unfold CG_pop. unlock.
-      repeat rel_rec_r.
-      rel_load_r.
-      rel_fold_r.
-      rel_case_r.
-      repeat rel_rec_r.
-      rel_apply_r (bin_log_related_release_r with "Hl").
-      { solve_ndisj. }
-      iIntros "Hl /=".
-      rel_rec_r.
-
+      iIntros "Hst' Hl".
       close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
       rel_load_l_atomic.
       iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
@@ -171,26 +148,9 @@ replace ((rec: "pop" "st" <> :=
         iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
         iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
                               "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
-        rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
-        rel_rec_r.
-        rel_apply_r (bin_log_related_acquire_r with "Hl").
+        rel_apply_r (CG_pop_suc_r with "Hst' Hl").
         { solve_ndisj. }
-        iIntros "Hl /=".
-        unfold CG_pop. unlock.
-        repeat rel_rec_r.
-        rel_load_r.
-        rel_fold_r.
-        rel_case_r.
-        rel_rec_r.
-        rel_proj_r.
-        rel_store_r.
-        rel_rec_r.
-        rel_proj_r.
-        rel_rec_r.
-        rel_apply_r (bin_log_related_release_r with "Hl").
-        { solve_ndisj. }
-        iIntros "Hl /=".
-        rel_rec_r.
+        iIntros "Hst' Hl".
         iMod ("Hclose" with "[-]").
         { iNext. rewrite /sinv.
           rewrite (StackLink_unfold _ (ym2, z2)).