prove retag (unique/sharedro)

theories/lang/stbor/stbor_sim.v

@@ -4,7 +4,7 @@ From lrust.lang Require Export lang_base.
 From lrust.lang.stbor Require Export stbor_semantics.
 Set Default Proof Using "Type".
 
-(** Simulation relation *)
+(** * Simulation relation *)
 Inductive stack_is_tail_item : item → Prop :=
 | stack_is_tail_item_unique tg : stack_is_tail_item (ItUnique tg)
 | stack_is_tail_item_disabled : stack_is_tail_item ItDisabled.
@@ -60,7 +60,7 @@ Inductive stack_sub : stack → stack → Prop :=
 Definition stack_rel_stack (stkphys stklog : stack) : Prop :=
   ∃ stkparsed, stack_parse stkphys stkparsed ∧ stack_sub stklog stkparsed.
 
-(** Access predicates *)
+(** * Access predicates *)
 Inductive stack_log_grants_write (tg : tag) : stack → Prop :=
 | stack_log_grants_write_here it stk :
     item_grants_write tg it →
@@ -75,7 +75,9 @@ Inductive stack_log_grants_read (tg : tag) : stack → Prop :=
     stack_log_grants_read tg stk →
     stack_log_grants_read tg (it :: stk).
 
-(** Writing *)
+Definition stack_log_no_sharedro (stklog : stack) : Prop := ¬ ∃ tgs stklog', stklog = ItSharedRO tgs :: stklog'.
+
+(** * Writing *)
 Lemma stack_sub_write_skip_sharedro tg tgs stklog stkparsed :
   stack_log_grants_write tg stklog →
   stack_sub stklog (ItSharedRO tgs :: stkparsed) →
@@ -129,11 +131,11 @@ Proof.
   - apply stack_sub_drop_shared. apply Hsub.
 Qed.
 
-Lemma write_single_preserve tg stklog stkphys1 stkphys2 :
+Lemma write_single_preserve' tg stklog stkphys1 stkphys2 :
   write_single tg stkphys1 = Some stkphys2 →
   stack_log_grants_write tg stklog →
   stack_rel_stack stkphys1 stklog →
-  stack_rel_stack stkphys2 stklog.
+  ∃ stkparsed, stack_parse_tail stkphys2 stkparsed ∧ stack_sub_tail stklog stkparsed.
 Proof.
   intros Hwrite Hgrants Hrel.
   destruct Hrel as (stkparsed & Hparse & Hsub).
@@ -144,26 +146,87 @@ Proof.
       case_decide as Hgrants';
       rewrite -/write_single in Hwrite;
       first inversion Hgrants'.
-    eapply stack_rel_from_tail; by eapply write_single_preserve_tail.
+    by eapply write_single_preserve_tail.
   - (* No SharedRO on top *)
     eapply stack_sub_write_skip_sharedro in Hsub; last done.
-    eapply stack_rel_from_tail; by eapply write_single_preserve_tail.
+    by eapply write_single_preserve_tail.
+Qed.
+
+Lemma write_single_preserve tg stklog stkphys1 stkphys2 :
+  write_single tg stkphys1 = Some stkphys2 →
+  stack_log_grants_write tg stklog →
+  stack_rel_stack stkphys1 stklog →
+  stack_rel_stack stkphys2 stklog.
+Proof.
+  intros Hwrite Hgrants Hrel.
+  eapply stack_rel_from_tail; by eapply write_single_preserve'.
+Qed.
+
+(** * Reading *)
+
+(** ** Inversion lemmas about semantics *)
+Lemma read_single_sharedrw_inv tg tgs stkphys1 stkphys2 :
+  read_single tg (ItSharedRW tgs :: stkphys1) = Some stkphys2 →
+  (item_grants_read tg (ItSharedRW tgs) ∧ stkphys2 = ItSharedRW tgs :: stkphys1) ∨
+  (∃ stkphys2', ¬ item_grants_read tg (ItSharedRW tgs) ∧ stkphys2 = ItSharedRW tgs :: stkphys2' ∧ read_single tg stkphys1 = Some stkphys2').
+Proof.
+  intros Hread.
+  rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
+  - left. inversion Hread; split; done.
+  - right. apply fmap_Some_1 in Hread as (stkphys2' & Hread' & Heq).
+    rewrite /read_traverse_item decide_True in Heq; last constructor.
+    exists stkphys2'; split; last split; assumption.
+Qed.
+
+Lemma stack_is_tail_item_traverse it stk :
+  stack_is_tail_item it → read_traverse_item it stk = ItDisabled :: stk.
+Proof.
+  inversion 1.
+  - by rewrite /read_traverse_item decide_False; last inversion 1.
+  - by rewrite /read_traverse_item decide_True; last constructor.
 Qed.
 
-(** Reading *)
-Lemma stack_log_grants_not_sharedro tg tgs1 tgs2 :
+Lemma read_single_unique_inv tg it stkphys1 stkphys2 :
+  stack_is_tail_item it →
+  read_single tg (it :: stkphys1) = Some stkphys2 →
+  (item_grants_read tg it ∧ stkphys2 = it :: stkphys1) ∨
+  (∃ stkphys2', ¬ item_grants_read tg it ∧ stkphys2 = ItDisabled :: stkphys2' ∧ read_single tg stkphys1 = Some stkphys2').
+Proof.
+  intros Htailit Hread.
+  rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
+  - left. inversion Hread; split; done.
+  - right. apply fmap_Some_1 in Hread as (stkphys2' & Hread' & Heq).
+    rewrite stack_is_tail_item_traverse in Heq; last assumption.
+    exists stkphys2'; split; last split; assumption.
+Qed.
+
+Lemma read_single_sharedro_inv tg tgs stkphys1 stkphys2 :
+  read_single tg (ItSharedRO tgs :: stkphys1) = Some stkphys2 →
+  (item_grants_read tg (ItSharedRO tgs) ∧ stkphys2 = ItSharedRO tgs :: stkphys1) ∨
+  (∃ stkphys2', ¬ item_grants_read tg (ItSharedRO tgs) ∧ stkphys2 = ItSharedRO tgs :: stkphys2' ∧ read_single tg stkphys1 = Some stkphys2').
+Proof.
+  intros Hread.
+  rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
+  - left. by inversion Hread.
+  - right. apply fmap_Some_1 in Hread as (stkphys2' & Hread & Heq).
+    rewrite /read_traverse_item decide_True in Heq; last constructor.
+    rewrite Heq. by exists stkphys2'.
+Qed.
+
+(** ** Properties of access predicates *)
+Lemma item_grants_read_not_sharedro tg tgs1 tgs2 :
   tgs1 ⊆ tgs2 →
   ¬ item_grants_read tg (ItSharedRO tgs2) →
   ¬ item_grants_read tg (ItSharedRO tgs1).
 Proof. intros Hsub Hit2 Hit1. apply Hit2. constructor. inversion Hit1. set_solver. Qed.
 
-Lemma stack_log_grants_not_sharedrw tg tgs1 tgs2 :
+Lemma item_grants_read_not_sharedrw tg tgs1 tgs2 :
   tgs1 ⊆ tgs2 →
   ¬ item_grants_read tg (ItSharedRW tgs2) →
   ¬ item_grants_read tg (ItSharedRW tgs1).
 Proof. intros Hsub Hit2 Hit1. apply Hit2. constructor. inversion Hit1. set_solver. Qed.
 
-Lemma stack_log_grants_not_subitem tg it1 it2 :
+Lemma item_grants_read_not_unique tg it1 it2 :
   stack_sub_unique it1 it2 →
   ¬ item_grants_read tg it2 →
   ¬ item_grants_read tg it1.
@@ -189,7 +252,7 @@ Lemma stack_log_grants_is_disabled_1 tg it1 it2 stklog :
 Proof.
   intros Hit Hsubit Hgrants.
   inversion Hgrants as [|? ? Hskip].
-  { exfalso. by eapply stack_log_grants_not_subitem. }
+  { exfalso. by eapply item_grants_read_not_unique. }
   inversion Hsubit; [done|done|].
   subst. inversion Hskip.
 Qed.
@@ -204,11 +267,29 @@ Lemma stack_log_grants_is_disabled_2 tg tgs tgs' it1 it2 stklog :
 Proof.
   intros Hit1 Hit2 Htgs Hsubit Hgrants.
   inversion Hgrants.
-  { exfalso. by eapply stack_log_grants_not_sharedrw. }
+  { exfalso. by eapply item_grants_read_not_sharedrw. }
   by eapply stack_log_grants_is_disabled_1.
 Qed.
 
-Lemma stack_log_grants_drop_both tg tgs it stklog stkparsed :
+Lemma stack_log_grants_split_sharedro tg tgs stklog stkparsed :
+  ¬ item_grants_read tg (ItSharedRO tgs) →
+  stack_log_grants_read tg stklog →
+  stack_sub stklog (ItSharedRO tgs :: stkparsed) →
+  ∃ stklog',
+    stack_log_grants_read tg stklog' ∧
+    stack_sub_tail stklog' stkparsed ∧
+    (∀ stkparsed', stack_sub_tail stklog' stkparsed' → stack_sub stklog (ItSharedRO tgs :: stkparsed')).
+Proof.
+  intros Hit Hgrants Hsub.
+  inversion Hsub; subst.
+  - apply stack_log_grants_drop_not_matching in Hgrants; last by eapply item_grants_read_not_sharedro.
+    eexists; split; last split; [eassumption|eassumption|].
+    intros stkparsed' Hsub'. by apply stack_sub_keep_shared.
+  - eexists; split; last split; [eassumption|eassumption|].
+    intros stkparsed' Hsub'. by apply stack_sub_drop_shared.
+Qed.
+
+Lemma stack_log_grants_split_sharedrw tg tgs it stklog stkparsed :
   ¬ item_grants_read tg (ItSharedRW tgs) →
   ¬ item_grants_read tg it →
   stack_log_grants_read tg stklog →
@@ -222,61 +303,25 @@ Proof.
   inversion Hsub.
   - exists stklog; split; last split; [assumption|assumption|].
     intros stkparsed' Hsub'. apply stack_sub_tail_drop_both. assumption.
-  - subst.
-    assert (Hdisabled: it1 = ItDisabled).
+  - subst. assert (Hdisabled: it1 = ItDisabled).
     { by eapply stack_log_grants_is_disabled_1; first apply Hit2. }
     rewrite Hdisabled.
-    apply stack_log_grants_drop_not_matching in Hgrants; last by eapply stack_log_grants_not_subitem.
+    apply stack_log_grants_drop_not_matching in Hgrants; last by eapply item_grants_read_not_unique.
     clear Hsub. eexists; split; last split; [eassumption|eassumption|].
     intros stkparsed' Hsub'. apply stack_sub_tail_drop_one; last assumption.
     constructor.
-  - subst.
-    assert (Hdisabled: it1 = ItDisabled).
+  - subst. assert (Hdisabled: it1 = ItDisabled).
     { eapply stack_log_grants_is_disabled_2; eauto. }
     rewrite Hdisabled.
     apply stack_log_grants_drop_not_matching in Hgrants; last first.
-    { by eapply stack_log_grants_not_sharedrw. }
+    { by eapply item_grants_read_not_sharedrw. }
     apply stack_log_grants_drop_not_matching in Hgrants; last first.
-    { by eapply stack_log_grants_not_subitem. }
+    { by eapply item_grants_read_not_unique. }
     clear Hsub. eexists; split; last split; [eassumption|eassumption|].
     intros stkparsed' Hsub'. apply stack_sub_tail_keep; [assumption|constructor|assumption].
 Qed.
 
-Lemma read_single_sharedrw_inv tg tgs it stkphys1 stkphys2 :
-  read_single tg (ItSharedRW tgs :: it :: stkphys1) = Some stkphys2 →
-  (item_grants_read tg (ItSharedRW tgs) ∧ stkphys2 = ItSharedRW tgs :: it :: stkphys1) ∨
-  (∃ stkphys2', ¬ item_grants_read tg (ItSharedRW tgs) ∧ stkphys2 = ItSharedRW tgs :: stkphys2' ∧ read_single tg (it :: stkphys1) = Some stkphys2').
-Proof.
-  intros Hread.
-  rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
-  - left. inversion Hread; split; done.
-  - right. apply fmap_Some_1 in Hread as (stkphys2' & Hread' & Heq).
-    rewrite /read_traverse_item decide_True in Heq; last constructor.
-    exists stkphys2'; split; last split; assumption.
-Qed.
-
-Lemma stack_is_tail_item_traverse it stk :
-  stack_is_tail_item it → read_traverse_item it stk = ItDisabled :: stk.
-Proof.
-  inversion 1.
-  - by rewrite /read_traverse_item decide_False; last inversion 1.
-  - by rewrite /read_traverse_item decide_True; last constructor.
-Qed.
-
-Lemma read_single_unique_inv tg it stkphys1 stkphys2 :
-  stack_is_tail_item it →
-  read_single tg (it :: stkphys1) = Some stkphys2 →
-  (item_grants_read tg it ∧ stkphys2 = it :: stkphys1) ∨
-  (∃ stkphys2', ¬ item_grants_read tg it ∧ stkphys2 = ItDisabled :: stkphys2' ∧ read_single tg stkphys1 = Some stkphys2').
-Proof.
-  intros Htailit Hread.
-  rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
-  - left. inversion Hread; split; done.
-  - right. apply fmap_Some_1 in Hread as (stkphys2' & Hread' & Heq).
-    rewrite stack_is_tail_item_traverse in Heq; last assumption.
-    exists stkphys2'; split; last split; assumption.
-Qed.
-
+(** ** Preservation properties *)
 Lemma read_single_preserve_tail tg stklog stkphys1 stkphys2 stkparsed1 :
   read_single tg stkphys1 = Some stkphys2 →
   stack_log_grants_read tg stklog →
@@ -294,7 +339,7 @@ Proof.
     { rewrite Heq. eexists. split; last eassumption. by apply stack_parse_tail_shared. }
     apply read_single_unique_inv in Hread' as [[Hit3 Heq3]|(stkphys3 & Hit3 & Heq3 & Hread3)]; last assumption.
     { subst. eexists. split; last eassumption. by apply stack_parse_tail_shared. }
-    eapply stack_log_grants_drop_both in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [|eassumption..].
+    eapply stack_log_grants_split_sharedrw in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [|eassumption..].
     clear Hgrants. subst.
     edestruct IH as (stkparsed4 & Hparse4 & Hsub4); [eassumption..|].
     eexists; split; last first.
@@ -303,7 +348,7 @@ Proof.
   - (* No SharedRW on top *)
     apply read_single_unique_inv in Hread as [[Hit3 Heq3]|(stkphys2' & Hit & Heq & Hread')]; last assumption.
     { subst. eexists. split; last eassumption. by apply stack_parse_tail_noshared. }
-    eapply stack_log_grants_drop_both in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [| |eassumption..]; last first.
+    eapply stack_log_grants_split_sharedrw in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [| |eassumption..]; last first.
     { inversion 1. set_solver. }
     clear Hgrants. subst.
     edestruct IH as (stkparsed4 & Hparse4 & Hsub4); [eassumption..|].
@@ -323,210 +368,123 @@ Proof.
   destruct stkphys1 as [|it stkphys1]; first inversion Hread.
   inversion Hparse; subst.
   - (* SharedRO on top *)
-    rewrite /read_single in Hread; case_decide as Hit; rewrite -/read_single in Hread.
-    { inversion Hread; eexists _; split; eassumption. }
-    destruct (read_single _ _) as [stknew|] eqn:Hread'; last inversion Hread.
-    rewrite /read_traverse_item /= in Hread. rewrite decide_True in Hread; last constructor.
-    inversion Hread.
-    inversion Hsub; subst.
-    (* Is the SharedRO part of the logical stack? *)
-    + apply stack_log_grants_drop_not_matching in Hgrants; last by eapply stack_log_grants_not_sharedro.
-      edestruct read_single_preserve_tail as (stkparsed2 & Hparse' & Hsub'); [eassumption..|].
-      eexists; split; constructor; eassumption.
-    + edestruct read_single_preserve_tail as (stkparsed2 & Hparse' & Hsub'); [eassumption..|].
-      eexists; split; constructor; eassumption.
+    apply read_single_sharedro_inv in Hread as [[Hit ->]|(stkphys3 & Hit3 & -> & Hread)]; first by eexists.
+    eapply stack_log_grants_split_sharedro in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [|eassumption..].
+    edestruct read_single_preserve_tail as (stkparsed2 & Hparse2 & Hsub2); [eassumption..|].
+    eexists. split; last eauto.
+    apply stack_parse_shared. apply Hparse2.
   - (* No SharedRO on top *)
-    inversion Hsub; subst.
-    (* Is the (empty) SharedRO part of the logical stack? *)
-    + apply stack_log_grants_drop_not_matching in Hgrants; last (inversion 1; set_solver).
-      edestruct read_single_preserve_tail as (stkparsed2 & Hparse' & Hsub'); [eassumption..|].
-      eexists; split; constructor; eassumption.
-    + edestruct read_single_preserve_tail as (stkparsed2 & Hparse' & Hsub'); [eassumption..|].
-      eexists; split; constructor; eassumption.
+    eapply stack_log_grants_split_sharedro in Hsub as (stklog' & Hgrants' & Hsub' & Hback); [| |eassumption]; last first.
+    { inversion 1. set_solver. }
+    edestruct read_single_preserve_tail as (stkparsed2 & Hparse2 & Hsub2); [eassumption..|].
+    eexists. split; last eauto.
+    apply stack_parse_noshared. apply Hparse2.
+Qed.
+
+(** * Retagging (Unique) *)
+Lemma retag_unique_single_preserve tgold tgnew stkphys1 stkphys2 stklog :
+  retag_unique_single tgold tgnew stkphys1 = Some stkphys2 →
+  stack_log_grants_write tgold stklog →
+  stack_rel_stack stkphys1 stklog →
+  stack_rel_stack stkphys2 stklog.
+Proof.
+  intros Hretag Hgrants Hrel.
+  rewrite /retag_unique_single /= in Hretag.
+  apply bind_Some in Hretag as (stkphys3 & Hwrite & Heq).
+  inversion Heq.
+  edestruct write_single_preserve' as (stkphys4 & Hparse4 & Hsub4); [eassumption..|].
+  eexists; split; last first.
+  - apply stack_sub_drop_shared. apply stack_sub_tail_drop_both. apply Hsub4.
+  - apply stack_parse_noshared. apply stack_parse_tail_noshared; first constructor. apply Hparse4.
+Qed.
+
+(** * Retagging (SharedRO) initial *)
+Lemma retag_sharedro_single_initial_preserve stklog stkphys :
+  stack_log_no_sharedro stklog →
+  stack_rel_stack stkphys stklog →
+  stack_rel_stack stkphys (ItSharedRO ∅ :: stklog).
+Proof.
+  intros Hnoshared Hrel.
+  destruct Hrel as (stkparsed & Hparse & Hsub).
+  inversion Hparse; subst.
+  - eexists; split.
+    + apply stack_parse_shared; eassumption.
+    + destruct Hsub.
+      { exfalso. apply Hnoshared; eauto. }
+      apply stack_sub_keep_shared; first set_solver.
+      assumption.
+  - eexists; split.
+    + apply Hparse.
+    + apply stack_sub_keep_shared; first set_solver.
+      inversion Hsub; subst.
+      { exfalso. apply Hnoshared; eauto. }
+      assumption.
 Qed.
 
-(* (** Retagging (Unique) *) *)
-(* Lemma stack_write_single_no_sharedro_tail tg stkphys1 stkphys2 : *)
-(*   stack_is_tail stkphys1 → *)
-(*   write_single tg stkphys1 = Some stkphys2 → *)
-(*   stack_is_tail stkphys2. *)
-(* Proof. *)
-(*   intros Htail Hwrite. *)
-(*   induction Htail as [|it stkphys1 Hit Htail IH]; first inversion Hwrite. *)
-(*   rewrite /write_single in Hwrite; case_decide; rewrite -/write_single in Hwrite. *)
-(*   - inversion Hwrite. apply Forall_cons; split; done. *)
-(*   - apply IH. apply Hwrite. *)
-(* Qed. *)
-
-(* Lemma stack_write_single_no_sharedro tg stkphys1 stkphys2 stklog : *)
-(*   stack_rel_stack stkphys1 stklog → *)
-(*   write_single tg stkphys1 = Some stkphys2 → *)
-(*   stack_is_tail stkphys2. *)
-(* Proof. *)
-(*   intros Hrel Hwrite. *)
-(*   destruct Hrel as (stkp & Hrel & Hsub). *)
-(*   destruct Hrel. *)
-(*   - rewrite /write_single in Hwrite; case_decide; rewrite -/write_single in Hwrite; first contradiction. *)
-(*     apply stack_write_single_no_sharedro_tail in Hwrite; done. *)
-(*   - apply stack_write_single_no_sharedro_tail in Hwrite; done. *)
-(* Qed. *)
-
-(* Lemma stack_log_grants_write_sub stklog stkphys tg : *)
-(*   stack_log_grants_write stklog tg → *)
-(*   stack_rel_stack stkphys stklog → *)
-(*   stklog `sublist_of` stkphys. *)
-(* Proof. *)
-(*   intros Hgrants Hrel. *)
-(*   destruct Hrel as (stkp & Hrel & Hsub). *)
-(*   destruct Hrel. *)
-(*   - apply sublist_cons_r in Hsub as [Hsub|(stklog'&Heq&Hsub)]. *)
-(*     + by apply sublist_cons. *)
-(*     + rewrite Heq in Hgrants. inversion Hgrants. *)
-(*       contradiction. *)
-(*   - apply sublist_cons_r in Hsub as [Hsub|(stklog'&Heq&Hsub)]. *)
-(*     + apply Hsub. *)
-(*     + rewrite Heq in Hgrants. inversion Hgrants. *)
-(*       contradiction. *)
-(* Qed. *)
-
-(* Lemma stack_retag_unique_single_preserve tgnew tgold stkphys1 stkphys2 stklog  : *)
-(*   retag_unique_single tgold tgnew stkphys1 = Some stkphys2 → *)
-(*   stack_log_grants_write stklog tgold → *)
-(*   stack_rel_stack stkphys1 stklog → *)
-(*   stack_rel_stack stkphys2 (ItUnique tgnew :: stklog). *)
-(* Proof. *)
-(*   intros Hretag Hgrants Hrel. *)
-(*   rewrite /retag_unique_single in Hretag. *)
-(*   destruct (write_single tgold stkphys1) as [stkphys3|] eqn:Hwrite; inversion Hretag. *)
-(*   assert (stack_is_tail stkphys3) as Htail. *)
-(*   { eapply stack_write_single_no_sharedro; done. } *)
-(*   eapply stack_write_single_preserve in Hwrite; try done. *)
-(*   exists (ItSharedRO ∅ :: ItUnique tgnew :: stkphys3); split; first constructor. *)
-(*   { apply Forall_cons; split; last done; constructor. } *)
-(*   eapply stack_log_grants_write_sub in Hwrite; last done. *)
-(*   apply sublist_cons, sublist_skip, Hwrite. *)
-(* Qed. *)
-
-(* Lemma stack_retag_unique_single_step tgold tgnew stkphys1 stklog : *)
-(*   stack_log_grants_write stklog tgold → *)
-(*   stack_rel_stack stkphys1 stklog → *)
-(*   ∃ stkphys2, retag_unique_single tgold tgnew stkphys1 = Some stkphys2. *)
-(* Proof. *)
-(*   intros Hgrants Hrel. *)
-(*   edestruct stack_write_single_step as (stkphys3 & Hwrite); try done. *)
-(*   exists (ItUnique tgnew :: stkphys3). *)
-(*   by rewrite /retag_unique_single Hwrite. *)
-(* Qed. *)
-
-(* (** Retagging (SharedRO) *) *)
-(* Lemma push_sharedro_subseteq tgsnew stk : *)
-(*   ∃ tgs' stkrest, push_sharedro tgsnew stk = ItSharedRO tgs' :: stkrest ∧ tgsnew ⊆ tgs'. *)
-(* Proof. *)
-(*   destruct stk as [|[tgit|tgsit|tgsit] stk]. *)
-(*   - by exists tgsnew, []. *)
-(*   - by exists tgsnew, (ItUnique tgit :: stk). *)
-(*   - by exists tgsnew, (ItSharedRW tgsit :: stk). *)
-(*   - by exists (tgsnew ∪ tgsit), stk; split; last set_solver. *)
-(* Qed. *)
-
-(* Lemma stack_is_tail_push_sharedro tgsnew stk : *)
-(*   stack_is_tail stk → *)
-(*   push_sharedro tgsnew stk = ItSharedRO tgsnew :: stk. *)
-(* Proof. by intros [|? ? [|]]. Qed. *)
-
-(* Lemma stack_is_tail_sublist stk1 stk2 : *)
-(*   stk1 `sublist_of` stk2 → *)
-(*   stack_is_tail stk2 → *)
-(*   stack_is_tail stk1. *)
-(* Proof. *)
-(*   intros Hsub. rewrite /stack_is_tail Forall_forall. *)
-(*   intros Htail. *)
-(*   apply Forall_forall. *)
-(*   intros it Helem. *)
-(*   apply Htail. *)
-(*   by eapply sublist_submseteq, elem_of_submseteq in Hsub; last done. *)
-(* Qed. *)
-
-(* Lemma stack_rel_stack_push_sharedro_empty stkphys stklog : *)
-(*   stack_rel_stack stkphys stklog → *)
-(*   stack_rel_stack stkphys (push_sharedro ∅ stklog). *)
-(* Proof. *)
-(*   intros Hrel. *)
-(*   destruct Hrel as (stkp & [|] & Hsub); apply sublist_cons_r in Hsub as [Hsub|(stklog'&Heq&Hsub)]. *)
-(*   - assert (stack_is_tail stklog) by by eapply stack_is_tail_sublist. *)
-(*     rewrite (stack_is_tail_push_sharedro ∅ stklog); last done. *)
-(*     exists (ItSharedRO ∅ :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - rewrite Heq. *)
-(*     exists (ItSharedRO (∅ ∪ tgs') :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - assert (stack_is_tail stklog) by by eapply stack_is_tail_sublist. *)
-(*     rewrite (stack_is_tail_push_sharedro ∅ stklog); last done. *)
-(*     exists (ItSharedRO ∅ :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - rewrite Heq. *)
-(*     exists (ItSharedRO ∅ :: stk); split; first (constructor; set_solver). *)
-(*     assert (Heq2 : (∅ : gset tag) ∪ ∅ = ∅) by set_solver. *)
-(*     simpl. rewrite Heq2. by apply sublist_skip. *)
-(* Qed. *)
-
-(* Lemma stack_rel_stack_push_sharedro tgsnew stkphys stklog : *)
-(*   stack_rel_stack stkphys stklog → *)
-(*   stack_rel_stack (push_sharedro tgsnew stkphys) (push_sharedro tgsnew stklog). *)
-(* Proof. *)
-(*   intros Hrel. *)
-(*   destruct Hrel as (stkp & [|] & Hsub); apply sublist_cons_r in Hsub as [Hsub|(stklog'&Heq&Hsub)]. *)
-(*   - assert (stack_is_tail stklog) by by eapply stack_is_tail_sublist. *)
-(*     rewrite (stack_is_tail_push_sharedro tgsnew stklog); last done. *)
-(*     exists (ItSharedRO tgsnew :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - rewrite Heq. *)
-(*     exists (ItSharedRO (tgsnew ∪ tgs') :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - assert (stack_is_tail stklog) by by eapply stack_is_tail_sublist. *)
-(*     rewrite (stack_is_tail_push_sharedro tgsnew stklog); last done. *)
-(*     rewrite (stack_is_tail_push_sharedro tgsnew stk); last done. *)
-(*     exists (ItSharedRO tgsnew :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(*   - rewrite Heq. *)
-(*     rewrite (stack_is_tail_push_sharedro tgsnew stk); last done. *)
-(*     exists (ItSharedRO (tgsnew ∪ ∅) :: stk); split; first (constructor; set_solver). *)
-(*     by apply sublist_skip. *)
-(* Qed. *)
-
-(* Lemma stack_retag_sharedro_single_preserve tgold tgsnew stkphys1 stkphys2 stklog : *)
-(*   retag_sharedro_single tgold tgsnew stkphys1 = Some stkphys2 → *)
-(*   stack_log_grants_read stklog tgold → *)
-(*   stack_rel_stack stkphys1 stklog → *)
-(*   stack_rel_stack stkphys2 (push_sharedro tgsnew stklog). *)
-(* Proof. *)
-(*   intros Hretag Hgrants Hrel. *)
-(*   rewrite /retag_sharedro_single in Hretag. *)
-(*   destruct (read_single tgold stkphys1) as [stkphys3|] eqn:Hread; inversion Hretag. *)
-(*   eapply stack_read_single_preserve in Hread; try done. *)
-(*   apply stack_rel_stack_push_sharedro. apply Hread. *)
-(* Qed. *)
-
-(* Lemma stack_retag_sharedro_single_step tgsnew tgold stklog stkphys1 : *)
-(*   stack_log_grants_read stklog tgold → *)
-(*   stack_rel_stack stkphys1 stklog → *)
-(*   ∃ stkphys2, retag_sharedro_single tgold tgsnew stkphys1 = Some stkphys2. *)
-(* Proof. *)
-(*   intros Hgrants Hrel. *)
-(*   edestruct stack_read_single_step as [stkphys3 Hread]; try done. *)
-(*   exists (push_sharedro tgsnew stkphys3). *)
-(*   by rewrite /retag_sharedro_single Hread. *)
-(* Qed. *)
-
-(* (** Logical removal *) *)
-(* Lemma stack_remove_preserve stklog1 stklog2 stkphys : *)
-(*   stklog2 `sublist_of` stklog1 → *)
-(*   stack_rel_stack stkphys stklog1 → *)
-(*   stack_rel_stack stkphys stklog2. *)
-(* Proof. *)
-(*   intros Hsub (stkp & Hrel & Hsub'). *)
-(*   exists stkp; split; first done. *)
-(*   by transitivity stklog1. *)
-(* Qed. *)
-
-(* (** Retagging (SharedRW) *) *)
+(** * Retagging (SharedRO) extend *)
+Lemma retag_sharedro_single_inv tgold tgsnew stkphys1 stkphys2 :
+  retag_sharedro_single tgold tgsnew stkphys1 = Some stkphys2 →
+  ∃ stkphys2', stkphys2 = merge_push (ItSharedRO tgsnew) stkphys2' ∧ read_single tgold stkphys1 = Some stkphys2'.
+Proof.
+  intros Hretag.
+  rewrite /retag_sharedro_single in Hretag.
+  apply bind_Some in Hretag as (stkphys2' & Hread & Heq2').
+  inversion Heq2'.
+  eexists; split; done.
+Qed.
+
+Lemma merge_push_tail tgs stkphys stkparsed :
+  stack_parse_tail stkphys stkparsed →
+  merge_push (ItSharedRO tgs) stkphys = ItSharedRO tgs :: stkphys.
+Proof.
+  intros Hparse.
+  destruct Hparse as [| |? ? ? Htailit]; try done.
+  inversion Htailit; done.
+Qed.
+
+Lemma stack_sub_tail_no_sharedro stklog stkparsed :
+  stack_sub_tail stklog stkparsed → ¬ ∃ tgs stklog', stklog = ItSharedRO tgs :: stklog'.
+Proof.
+  intros Hsub.
+  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? Hsubit|z w x y p].
+  - intros (? & ? & Heq). inversion Heq.
+  - apply IH.
+  - intros (? & ? & Heq). inversion Hsubit; subst; inversion Heq.
+  - intros (? & ? & Heq). inversion Heq.
+Qed.
+
+Lemma retag_sharedro_single_extend_preserve tgsnew tgold tgs stkphys1 stkphys2 stklog :
+  retag_sharedro_single tgold tgsnew stkphys1 = Some stkphys2 →
+  stack_log_grants_read tgold (ItSharedRO tgs :: stklog) →
+  stack_rel_stack stkphys1 (ItSharedRO tgs :: stklog) →
+  stack_rel_stack stkphys2 (ItSharedRO (tgsnew ∪ tgs) :: stklog).
+Proof.
+  intros Hretag Hgrants Hrel.
+  apply retag_sharedro_single_inv in Hretag as (stkphys2' & Heq & Hread).
+  edestruct read_single_preserve as (stkparsed3 & Hparse3 & Hsub3); [done..|].
+  inversion Hsub3; subst; last first.
+  { exfalso. eapply stack_sub_tail_no_sharedro; [eassumption|eauto]. }
+  inversion Hparse3; subst.
+  - eexists; split.
+    + by apply stack_parse_shared.
+    + by apply stack_sub_keep_shared; first set_solver.
+  - assert (Heq1: tgs = ∅) by set_solver.
+    assert (Heq2: tgsnew ∪ ∅ = tgsnew) by set_solver.
+    rewrite Heq1 Heq2.
+    erewrite merge_push_tail; last done.
+    eexists; split.
+    + by apply stack_parse_shared.
+    + by apply stack_sub_keep_shared; first set_solver.
+Qed.
+
+(** * Retagging (SharedRW) initial *)
+(** * Retagging (SharedRW) extend *)
+
+(** * Logical popping *)
+Lemma pop_prefix_preserve stkphys stklog1 stklog2 :
+  stklog2 `suffix_of` stklog1 →
+  stack_rel_stack stkphys stklog1 →
+  stack_rel_stack stkphys stklog2.
+Proof. Admitted.
+
+(** * Logical disabling *)