concurrent stacks: add some comments

theories/concurrent_stacks/concurrent_stack1.v

@@ -7,6 +7,8 @@ From iris.algebra Require Import agree list.
 From iris.heap_lang Require Import assert proofmode notation.
 Set Default Proof Using "Type".
 
+(** Stack 1: No helping, bag spec. *)
+
 Definition mk_stack : val :=
   λ: "_",
   let: "r" := ref NONEV in
@@ -65,6 +67,7 @@ Section stacks.
       iSplitL; try iApply is_stack_unfold; iRight; auto.
   Qed.
 
+  (* Per-element invariant (i.e., bag spec). *)
   Theorem stack_works P Φ :
     (∀ (f₁ f₂ : val),
             (∀ (v : val), □ WP f₁ #() {{ v, P v  ∨ v ≡ #-1 }})

theories/concurrent_stacks/concurrent_stack2.v

@@ -3,6 +3,8 @@ From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
 Set Default Proof Using "Type".
 
+(** Stack 2: With helping, bag spec. *)
+
 Definition mk_offer : val :=
   λ: "v", ("v", ref #0).
 Definition revoke_offer : val :=
@@ -262,6 +264,7 @@ Section stack_works.
       iSplitL; try iApply is_stack_unfold; iRight; auto.
   Qed.
 
+  (* Per-element invariant (i.e., bag spec). *)
   Theorem stack_works {channelG0 : channelG Σ} P Φ :
     (∀ (f₁ f₂ : val),
             (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v')  ∨ v ≡ NONEV }})

theories/concurrent_stacks/concurrent_stack3.v

@@ -3,6 +3,8 @@ From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
 Set Default Proof Using "Type".
 
+(** Stack 3: No helping, view-shift spec. *)
+
 Definition mk_stack : val :=
   λ: "_",
   let: "r" := ref NONEV in
@@ -83,12 +85,16 @@ Section stack_works.
       injection H; intros; subst; auto.
   Qed.
 
+  (* Whole-stack invariant (P). However:
+     - The resources for the successful and failing pop must be disjoint.
+       Instead, there should be a normal conjunction between them.
+     Open question: How does this relate to a logically atomic spec? *)
   Theorem stack_works P Q Q' Q'' Φ :
     (∀ (f₁ f₂ : val) ι,
-        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) -∗
+        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) -∗ (* pop *)
             (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗
             WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
-         -∗ (∀ (v : val),
+         -∗ (∀ (v : val), (* push *)
                □ ((∀ vs, P vs ={⊤∖↑ι}=∗ P (v :: vs) ∗ Q'') -∗
                   WP f₂ v {{ v, Q'' }}))
          -∗ Φ (f₁, f₂)%V)%I

theories/concurrent_stacks/concurrent_stack4.v

@@ -2,6 +2,8 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
 
+(** Stack 4: With helping, (weak) view-shift spec. *)
+
 Definition mk_offer : val :=
   λ: "v", ("v", ref #0).
 Definition revoke_offer : val :=
@@ -139,6 +141,11 @@ Section stack_works.
       injection H; intros; subst; auto.
   Qed.
 
+  (* View-shift based hole-stack invariant (P). However:
+     - The resources for the successful and failing pop must be disjoint.
+       Instead, there should be a normal conjunction between them.
+     - The updating view shifts have the empty mask.
+     Open question: How does this relate to a logically atomic spec? *)
   Theorem stack_works {channelG0 : channelG Σ} P Q Q' Q'' Φ :
     (∀ (f₁ f₂ : val),
         (□((∀ v vs, P (v :: vs) ==∗ Q v ∗ P vs) -∗