prove stack pop; add general stack interface

_CoqProject

@@ -82,3 +82,4 @@ theories/hocap/concurrent_runners.v
 theories/hocap/parfib.v
 
 theories/logatom_stack/stack.v
+theories/logatom_stack/spec.v

theories/logatom_stack/spec.v

+From stdpp Require Import namespaces.
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+Set Default Proof Using "Type".
+
+(** A general logically atomic interface for a stack. *)
+Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
+  (* -- operations -- *)
+  new_stack : val;
+  push : val;
+  pop : val;
+  (* -- other data -- *)
+  name : Type;
+  (* -- predicates -- *)
+  is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
+  stack_content (γs : name) (l : list val) : iProp Σ;
+  (* -- predicate properties -- *)
+  is_stack_persistent N γs v : Persistent (is_stack N γs v);
+  stack_content_timeless γs l : Timeless (stack_content γs l);
+  stack_content_exclusive γs l1 l2 :
+    stack_content γs l1 -∗ stack_content γs l2 -∗ False;
+  (* -- operation specs -- *)
+  new_stack_spec N :
+    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}};
+  push_spec N γs s e v :
+    IntoVal e v →
+    is_stack N γs s -∗
+    <<< ∀ l, stack_content γs l >>>
+      push (s, e) @ ⊤∖↑N
+    <<< stack_content γs (v::l), RET #() >>>;
+  pop_spec N γs s :
+    is_stack N γs s -∗
+    <<< ∀ l, stack_content γs l >>>
+      pop s @ ⊤∖↑N
+    <<< stack_content γs (tail l),
+        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>;
+}.
+Arguments atomic_stack _ {_}.
+
+Existing Instance is_stack_persistent.
+Existing Instance stack_content_timeless.

theories/logatom_stack/stack.v

-From iris.heap_lang Require Export lifting notation.
 From iris.algebra Require Import excl auth list.
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation atomic_heap par.
+From iris.heap_lang Require Import proofmode atomic_heap.
 From iris.bi.lib Require Import fractional.
+From iris_examples.logatom_stack Require Import spec.
 Set Default Proof Using "Type".
 
 (** * Implement a concurrent stack with helping on top of an arbitrary atomic
 heap. *)
-Definition stackN : namespace := nroot .@ "logatom_stack".
-Definition offerN : namespace := nroot .@ "logatom_stack" .@ "offer".
-Definition protoN : namespace := nroot .@ "logatom_stack" .@ "protocol".
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -26,9 +23,12 @@ Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
 Proof. solve_inG. Qed.
 
 Section stack.
-  Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} (N : namespace).
   Notation iProp := (iProp Σ).
 
+  Let offerN := N .@ "offer".
+  Let stackN := N .@ "stack".
+
   Import atomic_heap.notation.
 
   (** Code. A stack is a pair of two pointers-to-option-pointers, one for the
@@ -71,7 +71,7 @@ Section stack.
         (* See if we can change the master head pointer *)
         if: CAS (Fst "stack") (SOME "head_old") (Snd "head_old_data") then
           (* That worked! We are done. Return the value. *)
-          Fst "head_old_data"
+          SOME (Fst "head_old_data")
         else
           (* See if there is an offer on the side-channel *)
           match: !(Snd "stack") with
@@ -82,7 +82,7 @@ Section stack.
             (* Try to accept the offer. *)
             if: CAS (Snd "offer") #0 #1 then
               (* Success! We are done. Return the offered value. *)
-              Fst "offer"
+              SOME (Fst "offer")
             else
               (* Someone else was faster. Just try again. *)
               "pop" "stack"
@@ -94,6 +94,12 @@ Section stack.
     (own γs (◯ Excl' l))%I.
   Global Instance stack_content_timeless γs l : Timeless (stack_content γs l) := _.
 
+  Lemma stack_content_exclusive γs l1 l2 :
+    stack_content γs l1 -∗ stack_content γs l2 -∗ False.
+  Proof.
+    iIntros "Hl1 Hl2". iDestruct (own_valid_2 with "Hl1 Hl2") as %[].
+  Qed.
+
   Definition stack_elem_to_val (stack_rep : option loc) : val :=
     match stack_rep with
     | None => NONEV
@@ -105,8 +111,8 @@ Section stack.
   Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
     match l with
     | nil => ⌜rep = None⌝
-    | v::l => ∃ (ℓ : loc) (rep' : option loc), ⌜rep = Some ℓ⌝ ∗
-                              ℓ ↦ (v, stack_elem_to_val rep') ∗ list_inv l rep'
+    | v::l => ∃ (ℓ : loc) q (rep' : option loc), ⌜rep = Some ℓ⌝ ∗
+                              ℓ ↦{q} (v, stack_elem_to_val rep') ∗ list_inv l rep'
     end%I.
 
   Local Hint Extern 0 (environments.envs_entails _ (list_inv (_::_) _)) => simpl.
@@ -139,10 +145,13 @@ Section stack.
     | Some (v, st_loc) =>
       ∃ P Q γo, inv offerN (offer_inv st_loc γo P Q) ∗
                 (* The persistent part of the Laterable AU *)
-                □ (▷ P -∗ ◇ AU << ∀ l, stack_content γs l >> @ ⊤∖↑stackN, ∅
+                □ (▷ P -∗ ◇ AU << ∀ l, stack_content γs l >> @ ⊤∖↑N, ∅
                                << stack_content γs (v::l), COMM Q >>)
     end%I.
 
+  Local Instance is_offer_persistent γs offer_rep : Persistent (is_offer γs offer_rep).
+  Proof. destruct offer_rep as [[??]|]; apply _. Qed.
+
   Definition offer_to_val (offer_rep : option (val * loc)) : val :=
     match offer_rep with
     | None => NONEV
@@ -157,7 +166,7 @@ Section stack.
   Local Hint Extern 0 (environments.envs_entails _ (stack_inv _ _ _)) => unfold stack_inv.
 
   Definition is_stack (γs : gname) (s : val) : iProp :=
-    (∃ head offer : loc, ⌜s = (#head, #offer)%V⌝ ∗ inv protoN (stack_inv γs head offer))%I.
+    (∃ head offer : loc, ⌜s = (#head, #offer)%V⌝ ∗ inv stackN (stack_inv γs head offer))%I.
   Global Instance is_stack_persistent γs s : Persistent (is_stack γs s) := _.
 
   (** Proofs. *)
@@ -169,24 +178,25 @@ Section stack.
     wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
     { apply auth_valid_discrete_2. split; done. }
-    iMod (inv_alloc protoN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
+    iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
     { iNext. iExists None, None, _. iFrame. done. }
     iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
   Qed.
 
-  Lemma push_spec γs (s v : val) :
+  Lemma push_spec γs s e v :
+    IntoVal e v →
     is_stack γs s -∗
     <<< ∀ l, stack_content γs l >>>
-      push (s, v) @ ⊤∖↑stackN
+      push (s, e) @ ⊤∖↑N
     <<< stack_content γs (v::l), RET #() >>>.
   Proof.
-    iIntros "#Hinv" (Q Φ) "HQ AU".
+    intros <-. iIntros "#Hinv" (Q Φ) "HQ AU".
     iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
     iLöb as "IH".
     wp_let. wp_proj. wp_let. wp_proj. wp_let. wp_proj.
     (* Load the old head. *)
     wp_apply (load_spec with "[HQ AU]"); first by iAccu.
-    iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)".
+    iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)".
     iAaccIntro with "H↦"; first by eauto 10 with iFrame.
     iIntros "?". iSplitL; first by eauto 10 with iFrame.
     iIntros "!> [HQ AU]". clear offer_rep l.
@@ -195,8 +205,8 @@ Section stack.
     wp_let. wp_proj.
     (* CAS to change the head. *)
     wp_apply (cas_spec with "[HQ]"); [by destruct stack_rep|iAccu|].
-    iAuIntro. iInv protoN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
-    iAaccIntro with "H↦"; first eauto 10 with iFrame.
+    iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
+    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
     iIntros "H↦".
     destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as
       [->%stack_elem_to_val_inj|_].
@@ -205,7 +215,7 @@ Section stack.
       iDestruct (own_valid_2 with "Hs● Hl'") as
         %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
-      { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl (v::l))). done. }
+      { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
       iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
       change (InjRV #head_new) with (stack_elem_to_val (Some head_new)).
       iSplitR "HΦ"; first by eauto 12 with iFrame.
@@ -218,7 +228,7 @@ Section stack.
       wp_let. wp_let. wp_proj.
       (* Make the offer *)
       wp_apply (store_spec with "[HQ]"); first by iAccu.
-      iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
+      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
       iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
       iMod (own_alloc (Excl ())) as (γo) "Htok"; first done.
       iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
@@ -231,7 +241,7 @@ Section stack.
       iIntros "!> HQ". wp_let.
       (* Retract the offer. *)
       wp_proj. wp_apply (store_spec with "[HQ]"); first by iAccu.
-      iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
+      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
       iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
       iIntros "?". iSplitR "Htok".
       { iClear "Hoffer". iExists _, None, _. iFrame. done. }
@@ -260,6 +270,112 @@ Section stack.
         iDestruct (own_valid_2 with "Htok Hst") as %[].
   Qed.
 
+  Lemma pop_spec γs (s : val) :
+    is_stack γs s -∗
+    <<< ∀ l, stack_content γs l >>>
+      pop s @ ⊤∖↑N
+    <<< stack_content γs (tail l),
+        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+  Proof.
+    iIntros "#Hinv" (Q Φ) "HQ AU".
+    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
+    iLöb as "IH".
+    wp_let. wp_proj.
+    (* Load the old head *)
+    wp_apply (load_spec with "[HQ]"); first by iAccu.
+    iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
+    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
+    iIntros "?". destruct l as [|v l]; simpl.
+    - (* The list is empty! We are already done, but it's quite some work to
+      prove that. *)
+      iDestruct "Hlist" as ">%". subst stack_rep.
+      iMod "AU" as (l') "[Hl' [_ Hclose]]".
+      iDestruct (own_valid_2 with "Hs● Hl'") as
+        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+      iMod ("Hclose" with "Hl'") as "HΦ".
+      iSplitR "HΦ"; first by eauto 10 with iFrame.
+      iIntros "!> HQ". wp_match. by iApply "HΦ".
+    - (* Non-empty list, let's try to pop. *)
+      iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep.
+      iSplitR "AU Htail"; first by eauto 15 with iFrame.
+      clear offer_rep l.
+      iIntros "!> HQ". wp_match.
+      wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
+      iIntros "Htail". wp_let. wp_proj. wp_proj.
+      (* CAS to change the head *)
+      wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
+      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
+      iAaccIntro with "H↦"; first by eauto 10 with iFrame.
+      iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)).
+      destruct (decide (stack_elem_to_val stack_rep = stack_elem_to_val (Some tail))) as
+        [->%stack_elem_to_val_inj|_].
+      + (* CAS succeeded! It must still be the same head element in the list,
+        and we are done. *)
+        iMod "AU" as (l') "[Hl' [_ Hclose]]".
+        iDestruct (own_valid_2 with "Hs● Hl'") as
+          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        destruct l as [|v' l]; simpl.
+        { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
+        iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
+        iDestruct "Heq" as %[= <-].
+        iDestruct (mapsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj].
+        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
+        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
+        iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}".
+        iSplitR "HΦ"; first by eauto 10 with iFrame.
+        iIntros "!> HQ". clear q' q offer_rep l.
+        wp_if. wp_proj. by iApply "HΦ".
+      + (* CAS failed.  Go on looking for an offer. *)
+        iSplitR "AU"; first by eauto 10 with iFrame.
+        iIntros "!> HQ". wp_if. clear rep stack_rep offer_rep l q tail v.
+        wp_proj.
+        (* Load the offer pointer. *)
+        (* FIXME: [wp_apply (load_spec with "[HQ AU]"); first by iAccu.] here triggers an anomaly. *)
+        wp_apply (load_spec with "[HQ]"); first by iAccu.
+        iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & >Hoff↦ & #Hoff)".
+        iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
+        iIntros "Hoff↦". iSplitR "AU"; first by eauto 10 with iFrame.
+        iIntros "!> HQ". destruct offer_rep as [[v offer_st_loc]|]; last first.
+        { (* No offer, just loop. *) wp_match. iApply ("IH" with "HQ AU"). }
+        clear l stack_rep. wp_match. wp_proj.
+        (* CAS to accept the offer. *)
+        wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. simpl.
+        iAuIntro. iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]".
+        iInv offerN as (offer_st) "[>Hoff↦ Hoff]".
+        iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
+        iIntros "Hoff↦".
+        destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first.
+        { (* CAS failed, we don't do a thing. *)
+          iSplitR "AU"; first by eauto 10 with iFrame.
+          iIntros "!> HQ". wp_if. iApply ("IH" with "HQ AU"). }
+        (* CAS succeeded! We accept and complete the offer. *)
+        destruct offer_st; try done; []. clear Heq.
+        iMod ("AUoff" with "Hoff") as "{AUoff IH} AUoff".
+        iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
+        iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
+        iDestruct (own_valid_2 with "Hs● Hl'") as
+          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
+        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
+        iMod ("Hclose" with "Hl'") as "HQoff".
+        iMod "AU" as (l') "[Hl' [_ Hclose]]".
+        iDestruct (own_valid_2 with "Hs● Hl'") as
+          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
+        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
+        iMod ("Hclose" with "Hl'") as "HΦ".
+        iSplitR "Hoff↦ HQoff HΦ"; first by eauto 10 with iFrame. iSplitR "HΦ".
+        { iIntros "!> !> !>". iExists OfferAccepted. iFrame. }
+        iIntros "!> !> HQ". wp_if. wp_proj. by iApply "HΦ".
+  Qed.
+
 End stack.
 
+Definition elimination_stack `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} :
+  atomic_stack Σ :=
+  {| spec.new_stack_spec := new_stack_spec;
+     spec.push_spec := push_spec;
+     spec.pop_spec := pop_spec;
+     spec.stack_content_exclusive := stack_content_exclusive |}.
+
 Global Typeclasses Opaque stack_content is_stack.