add some missing rules in history ghost

theories/examples/history/ghost.v

@@ -59,30 +59,22 @@ Definition history_snap γg E M : vProp :=
 
 (* Updates *)
 Lemma ghost_history_update γ E E' (Le: E ⊑ E') :
-  history_gmaster γ 1 E ==∗ history_gmaster γ 1 E' ∗ history_gsnap γ E'.
-Proof.
-  rewrite -own_op. apply own_update.
-  rewrite -mono_list_auth_lb_op. by apply mono_list_update.
-Qed.
+  history_gmaster γ 1 E ==∗ history_gmaster γ 1 E'.
+Proof. by apply own_update, mono_list_update. Qed.
 
-Lemma ghost_history_fork γ f E E' (Le: E' ⊑ E) :
-  history_gmaster γ f E ==∗ history_gmaster γ f E ∗ history_gsnap γ E'.
-Proof.
-  rewrite -own_op. apply own_update.
-  rewrite /ghost_history_master /ghost_history_snap.
-  rewrite mono_list_auth_lb_op.
-  rewrite -(assoc _ (●ML{#f} _)) mono_list_lb_op_r; [|done].
-  by rewrite -mono_list_auth_lb_op.
-Qed.
+Lemma ghost_history_master_snap γ f E :
+  history_gmaster γ f E ⊢ history_gsnap γ E.
+Proof. apply own_mono, mono_list_included. Qed.
+
+Lemma ghost_history_snap_sub γ E G' :
+  E ⊑ G' →
+  history_gsnap γ G' -∗ history_gsnap γ E.
+Proof. intros Le. apply own_mono, mono_list_lb_mono, Le. Qed.
 
 (* Alloc *)
 Lemma ghost_history_alloc E :
-  ⊢ |==> ∃ γ, history_gmaster γ 1 E ∗ history_gsnap γ E.
-Proof.
-  iMod (own_alloc (ghost_history_master 1 E)) as (γ) "Hm".
-  - apply mono_list_auth_valid.
-  - iExists γ. by iMod (ghost_history_update with "Hm") as "$".
-Qed.
+  ⊢ |==> ∃ γ, history_gmaster γ 1 E.
+Proof. apply own_alloc, mono_list_auth_valid. Qed.
 
 (* Agreements *)
 Lemma ghost_history_master_agree γ f1 E1 f2 E2  :
@@ -122,14 +114,16 @@ Lemma history_master_update γ E E' :
   history_master γ 1 E' ∗ history_gsnapv γ E'.
 Proof.
   iIntros (SE EC) "[EM %]".
-  by iMod (ghost_history_update with "EM") as "[$ $]".
+  iMod (ghost_history_update with "EM") as "EM"; [exact SE|].
+  iDestruct (ghost_history_master_snap with "EM") as "#$". by iFrame "EM".
 Qed.
 
 Lemma history_master_alloc_empty :
   ⊢ |==> ∃ γ, history_master γ 1 [] ∗ history_gsnapv γ [].
 Proof.
-  iMod (ghost_history_alloc []) as (γ) "[Em Es]".
-  iIntros "!>". iExists γ. iFrame. by iPureIntro.
+  iMod (ghost_history_alloc []) as (γ) "Em".
+  iIntros "!>". iExists γ. iDestruct (ghost_history_master_snap with "Em") as "#$".
+  iFrame. by iPureIntro.
 Qed.
 
 Lemma history_master_wf γg f E :
@@ -145,12 +139,11 @@ Proof.
 Qed.
 
 Lemma history_master_snap γg f E :
-  history_master γg f E ==∗
-  history_master γg f E ∗ history_snap γg E ∅.
+  history_master γg f E ⊢  history_snap γg E ∅.
 Proof.
   iIntros "[E %EGc]".
-  iMod (ghost_history_fork with "E") as "[$ $]"; first by auto.
-  iIntros "!>". iSplit; [done|]. by rewrite -SeenLogview_empty.
+  iDestruct (ghost_history_master_snap with "E") as "$".
+  by rewrite -SeenLogview_empty.
 Qed.
 
 Lemma history_master_snap_included' γg f E E' M V V' :
@@ -161,12 +154,14 @@ Proof.
   by iDestruct (ghost_history_master_snap_included with "E Es") as %?.
 Qed.
 
-Definition history_master_snap_included γg f E E' M
-  := view_at_wand_lr _ _ _ (history_master_snap_included' γg f E E' M).
-Definition history_master_snap_included_2 γg f E E' M
-  := view_at_wand_l _ _ _ (history_master_snap_included' γg f E E' M).
+Lemma history_master_snap_included γg q E E' M :
+  history_master γg q E -∗ history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+Proof. by apply view_at_wand_lr, history_master_snap_included'. Qed.
+Lemma history_master_snap_included_2 γg q E E' M V' :
+  history_master γg q E -∗ @{V'} history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+Proof. by apply view_at_wand_l, history_master_snap_included'. Qed.
 
-Lemma history_snap_mono_marked γg E M E' M'
+Lemma history_snap_mono γg E M E' M'
   (In1: E' ⊑ E) :
   history_snap γg E M -∗ history_snap γg E' M' -∗
   history_snap γg E M'.
@@ -179,6 +174,22 @@ Lemma history_snap_downclosed γg E M M' :
   M' ⊆ M → history_snap γg E M ⊢ history_snap γg E M'.
 Proof. iIntros (SubM') "[$ SL]". by iApply SeenLogview_downclosed. Qed.
 
+Lemma history_snap_union γg E M M' :
+  history_snap γg E M -∗ history_snap γg E M' -∗ history_snap γg E (M ∪ M').
+Proof. iIntros "[$ S1] [E2 S2]". rewrite -SeenLogview_union'. by iFrame. Qed.
+Lemma history_snap_union' γg E M M' :
+  history_snap γg E M ∗ history_snap γg E M' ⊢ history_snap γg E (M ∪ M').
+Proof. iIntros "[S1 S2]". iApply (history_snap_union with "S1 S2"). Qed.
+
+Lemma history_snap_upgrade γg q E' E M :
+  history_master γg q E' -∗ history_snap γg E M -∗ history_snap γg E' M.
+Proof.
+  iIntros "Em Es".
+  iDestruct (history_master_snap_included with "Em Es") as %SubE.
+  iDestruct (history_master_snap with "Em") as "E0".
+  by iApply (history_snap_mono with "E0 Es").
+Qed.
+
 Lemma history_snap_lookup γg E M e dV :
   ge_view <$> E !! e = Some dV → e ∈ M →
   history_snap γg E M -∗ ⊒(dV.(dv_comm)).

theories/examples/stack/proof_treiber_history.v

@@ -1449,6 +1449,14 @@ Proof.
   intros. iDestruct 1 as (??????????) "[$ ?]". iIntros "$". eauto 11 with iFrame.
 Qed.
 
+Lemma StackInv_history_snap_instance :
+  ∀ γs γg s E E' M',
+    StackInv γs γg s E -∗ history_snap γg E' M' -∗ ⌜ E' ⊑ E ⌝.
+Proof.
+  intros. iDestruct 1 as (??????????) "[E ?]". iIntros "E'".
+  by iDestruct (history_master_snap_included with "E E'") as %?.
+Qed.
+
 Lemma StackLocal_history_snap_instance :
   ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M.
 Proof. intros. iDestruct 1 as (??????) "[$ _]". Qed.
@@ -1535,7 +1543,7 @@ Proof.
     "(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
   simplify_encode.
   (* get snapshot of E1 *)
-  iMod (history_master_snap with "E●1") as "[E●1 #E◯1]".
+  iDestruct (history_master_snap with "E●1") as "#E◯1".
   iDestruct (history_master_snap_included with "E●1 E◯0") as %SubE01.
   iDestruct (emo_auth_lb_valid with "M●1 M◯0") as %(Subesi01 & Subne01 & Subess01).
   (* read *)
@@ -1613,7 +1621,7 @@ Proof.
   iDestruct "CASE" as "[[F ⊒Vr2]|[F sVw2]]".
   { (* fail CAS *)
     iDestruct "F" as %(-> & NEq & ->).
-    iMod (history_master_snap with "E●2") as "[E●2 #E◯2]".
+    iDestruct (history_master_snap with "E●2") as "#E◯2".
     iDestruct (emo_lb_own_get with "M●2") as "#M◯2".
 
     have bLeVV : bool_decide (V ⊑ V) by eapply bool_decide_unpack; eauto.
@@ -1899,7 +1907,7 @@ Proof.
     "(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
   simplify_encode.
   (* get snapshot of E1 *)
-  iMod (history_master_snap with "E●1") as "[E●1 #E◯1]".
+  iDestruct (history_master_snap with "E●1") as "#E◯1".
   (* initial snapshot is included in E1 *)
   iPoseProof "E◯0" as "E◯0'".
   iDestruct "E◯0'" as "[_ PSV]".
@@ -2268,7 +2276,7 @@ Proof.
     (* COMMIT with no change *)
     subst b2 ζn2.
     (* take a snapshot *)
-    iMod (history_master_snap with "E●2") as "[E●2 #E◯2]".
+    iDestruct (history_master_snap with "E●2") as "#E◯2".
     iDestruct (emo_lb_own_get with "M●2") as "#M◯2".
 
     set Vpp := mkDView V V2 V2 bLeVV2.
@@ -2589,6 +2597,8 @@ Program Definition treiber_stack_impl `{!noprolG Σ, !tstackG Σ, !atomicG Σ}
     spec_history.StackInv_Objective := StackInv_objective ;
     spec_history.StackInv_StackLinearizability := StackInv_StackLinearizability_instance ;
     spec_history.StackInv_history_master_acc := StackInv_history_master_acc_instance ;
+    spec_history.StackInv_history_snap := StackInv_history_snap_instance ;
+
     spec_history.StackLocal_history_snap := StackLocal_history_snap_instance ;
     spec_history.StackLocal_Persistent := StackLocal_persistent ;
     spec_history.new_stack_spec := new_stack_spec;

theories/examples/stack/spec_history.v

@@ -211,10 +211,14 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)} := StackSpec {
   StackInv_history_master_acc :
     ∀ γs γg s E, StackInv γs γg s E ⊢ history_master γg 1 E ∗
                                       (history_master γg 1 E -∗ StackInv γs γg s E);
-  StackLocal_history_snap :
-    ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M;
+  StackInv_history_snap :
+    ∀ γs γg s E E' M',
+      StackInv γs γg s E -∗ history_snap γg E' M' -∗ ⌜ E' ⊑ E ⌝;
+
   StackLocal_Persistent :
     ∀ N γs γg s E M, Persistent (StackLocal N γs γg s E M);
+  StackLocal_history_snap :
+    ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M;
 
   (* operations specs *)
   new_stack_spec : new_stack_spec' new_stack StackLocal StackInv;