Add push and pop proofs for elim stack

theories/examples/stack/proof_elim_graph.v

@@ -1268,6 +1268,29 @@ Proof.
     wp_if. by iApply "HΦ".
 Qed.
 
+(* TODO : this proof is general w.r.t. to try_push *)
+Lemma push_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
+  push_spec' (push try_push' (exchange ex)) (Eo ∖ ↑N) (StackLocal' N) StackInv'.
+Proof.
+  intros s tid γg G0 M V v Posv.
+  iIntros "#sV #SL" (Φ) "AU".
+  iLöb as "IH".
+
+  wp_rec.
+  awp_apply (try_push_spec with "sV SL"); [done..|].
+  iApply (aacc_aupd with "AU"); [done|].
+  iIntros (G) "QI".
+  iAaccIntro with "QI"; first by eauto with iFrame.
+  iIntros (b V' G' psId ps Vps M') "(QI & sV' & SL' & CASE) !>".
+  iDestruct "CASE" as %[(-> & -> & ->)|[-> F]].
+  - iLeft. iFrame "QI". iIntros "AU !> _".
+    wp_if. by iApply ("IH" with "AU").
+  - iRight.
+    iExists V', G', psId, ps, Vps, M'.
+    iFrame "QI sV' SL'". iSplit; [done|].
+    iIntros "HΦ !> _". wp_if. by iApply "HΦ".
+Qed.
+
 Lemma try_pop_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
   try_pop_spec' (try_pop try_pop' ex.(exchange)) (Eo ∖ ↑N) (StackLocal' N) StackInv'.
 Proof.
@@ -2407,4 +2430,36 @@ Proof.
     wp_if. by iApply "HΦ".
 Qed.
 
+(* TODO : this proof is general w.r.t. to try_pop *)
+Lemma pop_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
+  pop_spec' (pop try_pop' (exchange ex)) (Eo ∖ ↑N) (StackLocal' N) StackInv'.
+Proof.
+  intros s tid γg G0 M V.
+  iIntros "#sV #SL" (Φ) "AU".
+  iLöb as "IH".
+
+  wp_rec.
+  awp_apply (try_pop_spec with "sV SL"); [done..|].
+  iApply (aacc_aupd with "AU"); [done|].
+  iIntros (G) "QI".
+  iAaccIntro with "QI"; first by eauto with iFrame.
+  iIntros (v V' G' psId ppId ps pp Vpp M') "(QI & sV' & Local & F & CASE) !>".
+  iDestruct "CASE" as "[CASE|[CASE|CASE]]".
+  - iLeft. iDestruct "CASE" as %(-> & -> & ->).
+    iFrame "QI". iIntros  "AU !> _".
+    wp_let. wp_op. wp_if. by iApply ("IH" with "AU").
+  - iRight. iClear "IH". iDestruct "CASE" as %[? ?].
+    iExists v, V', G', psId, ppId, ps, pp. iExists Vpp, M'.
+    iFrame "QI sV' Local F". iSplitL.
+    + by iLeft.
+    + iIntros "H !> _". subst v.
+      wp_let. wp_op. wp_if. by iApply "H".
+  - iRight. iClear "IH". iDestruct "CASE" as %[? ?].
+    iExists v, V', G', psId, ppId, ps, pp. iExists Vpp, M'.
+    iFrame "QI sV' Local F". iSplitL.
+    + by iRight.
+    + iIntros "H !> _". wp_let. wp_op. rewrite bool_decide_false; [|lia].
+      wp_if. by iApply "H".
+Qed.
+
 End proof.