Add StackLocalLite for elim stack

theories/examples/stack/proof_elim_graph.v

@@ -2,6 +2,7 @@ From stdpp Require Import list.
 From iris.algebra Require Import auth gset gmap agree.
 From iris.proofmode Require Import tactics.
 
+From gpfsl.base_logic Require Import meta_data.
 From gpfsl.logic Require Import logatom invariants.
 From gpfsl.logic Require Import readonly_ptsto.
 From gpfsl.logic Require Import new_delete.
@@ -403,6 +404,8 @@ Local Existing Instances
   ExchangerInv_Objective
   ExchangerInv_Fractional
   ExchangerLocal_Persistent
+  ExchangerLocalLite_Persistent
+  ExchangerLocalLite_Timeless
   .
 
 (* Only share the ghost state with the client. *)
@@ -447,11 +450,32 @@ Global Instance ElimStackInv_objective γg γsb γsx γb γx γ s b x cons :
 Global Instance ElimStackInv_timeless γg γsb γsx γb γx γ s b x cons :
   Timeless (ElimStackInv γg γsb γsx γb γx γ s b x cons) := _.
 
+Definition StackLocalLite' N : StackLocalT Σ :=
+  (λ γg s G M,
+    graph_snap γg G M ∗
+    ∃ (b x : loc) (γsb γsx γb γx γ : gname),
+    meta s N (γsb,γsx,γb,γx,γ) ∗
+    s ro⊒{γsb} #b ∗ (s >> 1) ro⊒{γsx} #x ∗
+    ∃ Gb Mb Gx Mx T,
+    StackLocalLite stk γb b Gb Mb ∗
+    ExchangerLocalLite ex γx x Gx Mx ∗
+    (* observing M means Mb and Mx are at least M *)
+    ⌜ ElimStackLocalEvents T M Mb ⌝ ∗
+    ge_list_lb γ T
+  )%I.
+
+Global Instance StackLocalLite'_persistent N γg s G M :
+  Persistent (StackLocalLite' N γg s G M) := _.
+Global Instance StackLocalLite'_timeless N γg s G M :
+  Timeless (StackLocalLite' N γg s G M) := _.
+
 Definition StackLocal' N : StackLocalT Σ :=
   (λ γg s G M,
     graph_snap γg G M ∗
-    ∃ (b x : loc) γsb γsx γb γx γ Gb Mb Gx Mx T,
+    ∃ (b x : loc) (γsb γsx γb γx γ : gname),
+    meta s N (γsb,γsx,γb,γx,γ) ∗
     s ro⊒{γsb} #b ∗ (s >> 1) ro⊒{γsx} #x ∗
+    ∃ Gb Mb Gx Mx T,
     StackLocal stk γb b Gb Mb ∗
     ExchangerLocal ex N (ElimStackInv γg γsb γsx γb γx γ s b x) γx x Gx Mx ∗
     (* observing M means Mb and Mx are at least M *)
@@ -460,8 +484,10 @@ Definition StackLocal' N : StackLocalT Σ :=
     inv N (ElimStackInv γg γsb γsx γb γx γ s b x true)
   )%I.
 
+(* TODO: := _. diverges *)
 Global Instance StackLocal'_persistent N γg s G M :
-  Persistent (StackLocal' N γg s G M) := _.
+  Persistent (StackLocal' N γg s G M).
+Proof. apply bi.sep_persistent; apply _. Qed.
 
 Lemma ElimStackInv_locs_access γg γsb γsx γb γx γ s b x cons :
   ElimStackInv γg γsb γsx γb γx γ s b x cons ⊢
@@ -478,20 +504,6 @@ Lemma StackInv'_agree γg s G G' :
   StackInv' γg s G -∗ StackInv' γg s G' -∗ ⌜ G' = G ⌝.
 Proof. iIntros "[_ S1] [_ S2]". iApply (graph_master_agree with "S2 S1"). Qed.
 
-Lemma StackInv'_BasicStackConsistent_instance :
-  ∀ γg s G, StackInv' γg s G ⊢ ⌜ BasicStackConsistent G ⌝.
-Proof. by iIntros "* [$ _]". Qed.
-
-Lemma StackInv'_graph_master_acc_instance :
-  ∀ γg s G, StackInv' γg s G ⊢
-    graph_master γg (1/2) G ∗
-    (graph_master γg (1/2) G -∗ StackInv' γg s G).
-Proof. by iIntros "* [$ $] $". Qed.
-
-Lemma StackLocal'_graph_snap_instance N :
-  ∀ γg s G M, StackLocal' N γg s G M ⊢ graph_snap γg G M.
-Proof. by iIntros "* [$ _]". Qed.
-
 Lemma StackInv'_update γg s (G G' : graph sevent) :
   G ⊑ G' →
   eventgraph_consistent G' → BasicStackConsistent G' →
@@ -550,6 +562,55 @@ Proof.
   iDestruct (ge_list_auth_lb_get with "oT") as "#$". by iFrame "oT".
 Qed.
 
+(** * Verifications of Assertions properties *)
+Lemma StackInv'_BasicStackConsistent_instance :
+  ∀ γg s G, StackInv' γg s G ⊢ ⌜ BasicStackConsistent G ⌝.
+Proof. by iIntros "* [$ _]". Qed.
+
+Lemma StackInv'_graph_master_acc_instance :
+  ∀ γg s G, StackInv' γg s G ⊢
+    graph_master γg (1/2) G ∗
+    (graph_master γg (1/2) G -∗ StackInv' γg s G).
+Proof. by iIntros "* [$ $] $". Qed.
+
+Lemma StackLocal'_graph_snap_instance N :
+  ∀ γg s G M, StackLocal' N γg s G M ⊢ graph_snap γg G M.
+Proof. by iIntros "* [$ _]". Qed.
+
+Lemma StackLocalLite'_from_instance N :
+  ∀ γg s G M, StackLocal' N γg s G M ⊢ StackLocalLite' N γg s G M.
+Proof.
+  iIntros "* [$ SL]".
+  iDestruct "SL" as (???????) "(MT & s0 & s1 & SL)".
+  iExists _, _, _, _, _, _, _. iFrame "MT s0 s1".
+  iDestruct "SL" as (?????) "(SL & EL & F & oT & ?)".
+  iExists _, _, _, _, _. iFrame "F oT".
+  iDestruct (StackLocalLite_from with "SL") as "$".
+  iDestruct (ExchangerLocalLite_from with "EL") as "$".
+Qed.
+Lemma StackLocalLite_to_instance N :
+  ∀ γg s G' M' G M,
+    StackLocalLite' N γg s G M -∗ StackLocal' N γg s G' M' -∗
+    StackLocal' N γg s G M.
+Proof.
+  iIntros "* [$ SL] [_ SL']".
+  iDestruct "SL" as (???????) "(#MT & #s0 & #s1 & SL)".
+  iExists _, _, _, _, _, _, _. iFrame "MT s0 s1".
+  iDestruct "SL" as (?????) "(SL & EL & F & oT)".
+  iExists _, _, _, _, _. iFrame "F oT".
+  iDestruct "SL'" as (???????) "(MT' & s0' & s1' & SL')".
+  iDestruct "SL'" as (?????) "(SL' & EL' & _ & _ & II)".
+  iDestruct (meta_agree with "MT MT'") as %?. simplify_eq.
+  iDestruct (ROSeen_agree with "s0 s0'") as %?.
+  iDestruct (ROSeen_agree with "s1 s1'") as %?. simplify_eq.
+  iFrame "II".
+  iDestruct (StackLocalLite_to with "SL SL'") as "$".
+  iDestruct (ExchangerLocalLite_to with "EL EL'") as "$".
+Qed.
+
+Lemma StackLocalLite'_graph_snap_instance N :
+  ∀ γg s G M, StackLocalLite' N γg s G M ⊢ graph_snap γg G M.
+Proof. by iIntros "* [$ _]". Qed.
 
 (** * Verifications of functions *)
 Lemma new_stack_spec N :