prove retag(sharedrw) preservation lemma

theories/lang/stbor/stbor_sim.v

@@ -38,10 +38,10 @@ Inductive stack_sub_tail : stack → stack → Prop :=
 | stack_sub_tail_drop_both stk1 it1 it2 stk2 :
     stack_sub_tail stk1 stk2 →
     stack_sub_tail stk1 (it1 :: it2 :: stk2)
-| stack_sub_tail_drop_one it1 stk1 it' it2 stk2 :
+| stack_sub_tail_drop_one it1 stk1 tgs2 it2 stk2 :
     stack_sub_unique it1 it2 →
     stack_sub_tail stk1 stk2 →
-    stack_sub_tail (it1 :: stk1) (it' :: it2 :: stk2)
+    stack_sub_tail (it1 :: stk1) (ItSharedRW tgs2 :: it2 :: stk2)
 | stack_sub_tail_keep tgs1 it1 stk1 tgs2 it2 stk2 :
     tgs1 ⊆ tgs2 →
     stack_sub_unique it1 it2 →
@@ -77,6 +77,14 @@ Inductive stack_log_grants_read (tg : tag) : stack → Prop :=
 
 Definition stack_log_no_sharedro (stklog : stack) : Prop := ¬ ∃ tgs stklog', stklog = ItSharedRO tgs :: stklog'.
 
+Inductive stack_log_grants_retag_sharedrw (tg : tag) : stack → Prop :=
+| stack_log_grants_retag_sharedrw_found tgs it stklog :
+    tg ∈ tgs ∨ item_grants_write tg it →
+    stack_log_grants_retag_sharedrw tg (ItSharedRW tgs :: it :: stklog)
+| stack_log_grants_retag_sharedrw_continue it stklog :
+    stack_log_grants_retag_sharedrw tg stklog →
+    stack_log_grants_retag_sharedrw tg (it :: stklog).
+
 (** * Writing *)
 Lemma stack_sub_write_skip_sharedro tg tgs stklog stkparsed :
   stack_log_grants_write tg stklog →
@@ -478,7 +486,367 @@ Proof.
 Qed.
 
 (** * Retagging (SharedRW) initial *)
+Inductive retag_sharedrw_initial : stack → stack → Prop :=
+| retag_sharedrw_initial_nil : retag_sharedrw_initial [] []
+| retag_sharedrw_initial_sharedrw tgs it stklog stklog' :
+    retag_sharedrw_initial stklog stklog' →
+    retag_sharedrw_initial (ItSharedRW tgs :: it :: stklog) (ItSharedRW tgs :: it :: stklog')
+| retag_sharedrw_initial_unique it stklog stklog' :
+    stack_is_tail_item it →
+    retag_sharedrw_initial stklog stklog' →
+    retag_sharedrw_initial (it :: stklog) (it :: stklog')
+| retag_sharedrw_initial_unique_push it stklog stklog' :
+    stack_is_tail_item it →
+    retag_sharedrw_initial stklog stklog' →
+    retag_sharedrw_initial (it :: stklog) (ItSharedRW ∅ :: it :: stklog')
+| retag_sharedrw_initial_sharedro tgs stklog stklog' :
+    retag_sharedrw_initial stklog stklog' →
+    retag_sharedrw_initial (ItSharedRO tgs :: stklog) (ItSharedRO tgs :: stklog').
+
+Lemma stack_sub_unique_is_tail_item it1 it2 :
+  stack_sub_unique it1 it2 → stack_is_tail_item it1.
+Proof. intros Hsub. inversion Hsub; constructor. Qed.
+
+Lemma retag_sharedrw_initial_inv_tail_item it stklog1 stklog2 :
+  stack_is_tail_item it →
+  retag_sharedrw_initial (it :: stklog1) stklog2 →
+  ∃ stklog3, retag_sharedrw_initial stklog1 stklog3 ∧ (stklog2 = ItSharedRW ∅ :: it :: stklog3 ∨ stklog2 = it :: stklog3).
+Proof.
+  intros Htailit Hretag.
+  inversion Hretag; subst.
+  - inversion Htailit.
+  - eexists; split; first eassumption.
+    by right.
+  - eexists; split; first eassumption.
+    by left.
+  - inversion Htailit.
+Qed.
+
+Lemma retag_sharedrw_initial_inv_sharedrw tgs it stklog1 stklog2 :
+  retag_sharedrw_initial (ItSharedRW tgs :: it :: stklog1) stklog2 →
+  ∃ stklog3, stklog2 = ItSharedRW tgs :: it :: stklog3 ∧ retag_sharedrw_initial stklog1 stklog3.
+Proof.
+  inversion 1 as [| |? ? ? Htailit|? ? ? Htailit|].
+  - by eexists; split; last eassumption.
+  - inversion Htailit.
+  - inversion Htailit.
+Qed.
+
+Lemma retag_sharedrw_initial_inv_sharedro tgs stklog1 stklog2 :
+  retag_sharedrw_initial (ItSharedRO tgs :: stklog1) stklog2 →
+  ∃ stklog3, stklog2 = ItSharedRO tgs :: stklog3 ∧ retag_sharedrw_initial stklog1 stklog3.
+Proof.
+  inversion 1 as [| |? ? ? Htailit|? ? ? Htailit|].
+  - inversion Htailit.
+  - inversion Htailit.
+  - by eexists; split; last eassumption.
+Qed.
+
+Lemma retag_sharedrw_single_initial_tail stkparsed stklog1 stklog2 :
+  retag_sharedrw_initial stklog1 stklog2 →
+  stack_sub_tail stklog1 stkparsed →
+  stack_sub_tail stklog2 stkparsed.
+Proof.
+  intros Hretag Hsub.
+  generalize dependent stklog2.
+  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? ? ? IH|? ? ? ? ? ? ? ? ? IH]; intros stklog2 Hretag.
+  - inversion Hretag. apply stack_sub_tail_empty.
+  - apply stack_sub_tail_drop_both. apply IH.
+    apply Hretag.
+  - apply retag_sharedrw_initial_inv_tail_item in Hretag as (stklog3 & Hretag & [Heq|Heq]); last first.
+    + by eapply stack_sub_unique_is_tail_item.
+    + rewrite Heq. apply stack_sub_tail_drop_one; first done.
+      by apply IH.
+    + rewrite Heq. eapply stack_sub_tail_keep; [set_solver|done|].
+      by apply IH.
+  - apply retag_sharedrw_initial_inv_sharedrw in Hretag as (stklog3 & -> & Hretag).
+    apply stack_sub_tail_keep; [done..|].
+    by apply IH.
+Qed.
+
+Lemma retag_sharedrw_single_initial stkphys stklog1 stklog2 :
+  retag_sharedrw_initial stklog1 stklog2 →
+  stack_rel_stack stkphys stklog1 →
+  stack_rel_stack stkphys stklog2.
+Proof.
+  intros Hretag (stkparsed & Hparse & Hsub).
+  eexists; split; first apply Hparse.
+  destruct Hsub.
+  - apply retag_sharedrw_initial_inv_sharedro in Hretag as (stklog3 & -> & Hretag).
+    apply stack_sub_keep_shared; first done.
+    by eapply retag_sharedrw_single_initial_tail.
+  - apply stack_sub_drop_shared.
+    by eapply retag_sharedrw_single_initial_tail.
+Qed.
+
 (** * Retagging (SharedRW) extend *)
+Lemma retag_sharedrw_single_inv tgold tgsnew stkphys1 stkphys2 :
+  retag_sharedrw_single tgold tgsnew stkphys1 = Some stkphys2 →
+  ∃ stkphys2',
+    write_single tgold stkphys1 = Some stkphys2' ∧
+    retag_sharedrw_single' tgold tgsnew stkphys1 = stkphys2.
+Proof.
+  intros Hretag.
+  rewrite /retag_sharedrw_single in Hretag.
+  apply bind_Some in Hretag as (stkphys2' & Hwrite & Hretag).
+  inversion Hretag. eauto.
+Qed.
+
+Lemma merge_push_tail_item_l it stk :
+  stack_is_tail_item it →
+  merge_push it stk = it :: stk.
+Proof. by inversion 1. Qed.
+
+Lemma merge_push_tail_item_r it2 it1 stk :
+  stack_is_tail_item it2 →
+  merge_push it1 (it2 :: stk) = it1 :: it2 :: stk.
+Proof. destruct it1; by inversion 1. Qed.
+
+Lemma merge_push_merge_sharedrw tgs1 tgs2 stk :
+  merge_push (ItSharedRW tgs1) (merge_push (ItSharedRW tgs2) stk) = merge_push (ItSharedRW (tgs1 ∪ tgs2)) stk.
+Proof.
+  destruct stk as [|[] stk]; try done.
+  simpl. f_equal. f_equal. set_solver.
+Qed.
+
+Definition item_either_grants_write (tgold : tag) (tgsrw : gset tag) (ituniq : item) : Prop :=
+  item_grants_write tgold (ItSharedRW tgsrw) ∨ item_grants_write tgold ituniq.
+
+Lemma retag_sharedrw_single'_inv_sharedrw tgold tgsnew tgs it stkphys1 stkphys2 :
+  stack_is_tail_item it →
+  retag_sharedrw_single' tgold tgsnew (ItSharedRW tgs :: it :: stkphys1) = stkphys2 →
+  ∃ stkphys2',
+    retag_sharedrw_single' tgold tgsnew stkphys1 = stkphys2' ∧
+    ((item_either_grants_write tgold tgs it ∧ stkphys2 = ItSharedRW (tgsnew ∪ tgs) :: it :: stkphys2') ∨
+     (¬ item_either_grants_write tgold tgs it ∧ stkphys2 = ItSharedRW tgs :: it :: stkphys2')).
+Proof.
+  intros Htailit Hretag.
+  rewrite /retag_sharedrw_single' in Hretag; case_decide as Hit1; rewrite -/retag_sharedrw_single' in Hretag; case_decide as Hit2.
+  - rewrite !merge_push_merge_sharedrw (merge_push_tail_item_l it) in Hretag; last done.
+    rewrite (merge_push_tail_item_r it) in Hretag; last done.
+    rewrite -Hretag. set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    left; split; first by left. f_equal. f_equal. set_solver.
+  - rewrite !merge_push_merge_sharedrw (merge_push_tail_item_l it) in Hretag; last done.
+    rewrite (merge_push_tail_item_r it) in Hretag; last done.
+    rewrite -Hretag. set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    left; split; first by left. done.
+  - rewrite !merge_push_merge_sharedrw (merge_push_tail_item_l it) in Hretag; last done.
+    rewrite (merge_push_tail_item_r it) in Hretag; last done.
+    rewrite -Hretag. set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    left; split; first by right. f_equal. f_equal. set_solver.
+  - rewrite (merge_push_tail_item_l it) in Hretag; last done.
+    rewrite (merge_push_tail_item_r it) in Hretag; last done.
+    rewrite -Hretag. set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    right; split; last done. intros Heither.
+    rewrite /item_either_grants_write in Heither. tauto.
+Qed.
+
+Lemma retag_sharedrw_single'_inv_unique it tgold tgsnew stkphys1 stkphys2 :
+  stack_is_tail_item it →
+  retag_sharedrw_single' tgold tgsnew (it :: stkphys1) = stkphys2 →
+  ∃ stkphys2',
+    retag_sharedrw_single' tgold tgsnew stkphys1 = stkphys2' ∧
+    ((item_grants_write tgold it ∧ stkphys2 = ItSharedRW tgsnew :: it :: stkphys2') ∨
+     (¬ item_grants_write tgold it ∧ stkphys2 = it :: stkphys2')).
+Proof.
+  intros Htailit Hretag.
+  rewrite /retag_sharedrw_single' in Hretag; case_decide; rewrite -/retag_sharedrw_single' in Hretag.
+  - rewrite (merge_push_tail_item_l it) in Hretag; last done.
+    rewrite (merge_push_tail_item_r it) in Hretag; last done.
+    set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    left; by split.
+  - rewrite (merge_push_tail_item_l it) in Hretag; last done.
+    set (stkphys2' := retag_sharedrw_single' _ _ _).
+    exists stkphys2'; split; first done.
+    right; by split.
+Qed.
+
+Inductive retag_sharedrw_extend (tgold : tag) (tgsnew : gset tag) : stack → stack → Prop :=
+| retag_sharedrw_extend_nil : retag_sharedrw_extend tgold tgsnew [] []
+| retag_sharedrw_extend_continue it stklog1 stklog2 :
+    retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+    retag_sharedrw_extend tgold tgsnew (it :: stklog1) (it :: stklog2)
+| retag_sharedrw_extend_found tgs it stklog1 stklog2 :
+    item_grants_write tgold (ItSharedRW tgs) ∨ item_grants_write tgold it →
+    retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+    retag_sharedrw_extend tgold tgsnew (ItSharedRW tgs :: it :: stklog1) (ItSharedRW (tgsnew ∪ tgs) :: it :: stklog2).
+
+Lemma retag_sharedrw_extend_inv_tail_item tgold tgsnew it stklog1 stklog2 :
+  stack_is_tail_item it →
+  retag_sharedrw_extend tgold tgsnew (it :: stklog1) stklog2 →
+  ∃ stklog3, stklog2 = it :: stklog3 ∧ retag_sharedrw_extend tgold tgsnew stklog1 stklog3.
+Proof.
+  intros Htailit Hretag.
+  inversion Hretag; last first.
+  { subst. inversion Htailit. }
+  eexists; split; done.
+Qed.
+
+(* TODO: Get rid of this horrible duplication... *)
+Lemma stack_sub_tail_split_sharedrw1 stklog1 stklog2 tgold tgs tgsnew it stkparsed :
+  retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+  stack_sub_tail stklog1 (ItSharedRW tgs :: it :: stkparsed) →
+  ∃ stklog1' stklog2',
+    retag_sharedrw_extend tgold tgsnew stklog1' stklog2' ∧
+    stack_sub_tail stklog1' stkparsed ∧
+    (∀ stkparsed', stack_sub_tail stklog2' stkparsed' → stack_sub_tail stklog2 (ItSharedRW (tgsnew ∪ tgs) :: it :: stkparsed')).
+Proof.
+  intros Hretagl Hsub.
+  inversion Hsub as [| |? ? ? ? ? Hsubit|]; subst.
+  - do 2 eexists; split; last split; [done..|].
+    intros stkparsed' Hsub'. by apply stack_sub_tail_drop_both.
+  - inversion Hretagl; subst; last inversion Hsubit. clear Hretagl.
+    do 2 eexists; split; last split; [done..|].
+    intros stkparsed' Hsub'. by apply stack_sub_tail_drop_one.
+  - inversion Hretagl as [|? ? ? Hretagl'|]; last first.
+    + do 2 eexists; split; last split; [done..|].
+      intros stkparsed' Hsub'. apply stack_sub_tail_keep; [set_solver|done..].
+    + apply retag_sharedrw_extend_inv_tail_item in Hretagl' as (stklog3 & -> & Hretagl'); last first.
+      { by eapply stack_sub_unique_is_tail_item. }
+      subst. do 2 eexists; split; last split; [done..|].
+      intros stkparsed' Hsub'. apply stack_sub_tail_keep; [set_solver|done..].
+Qed.
+
+Lemma stack_sub_unique_item_grants tg it1 it2 :
+  stack_sub_unique it1 it2 → item_grants_write tg it1 → item_grants_write tg it2.
+Proof.
+  intros Hsub Hgrants.
+  inversion Hsub; subst; inversion Hgrants; subst.
+  assumption.
+Qed.
+
+Lemma stack_sub_tail_split_sharedrw2 stklog1 stklog2 tgold tgs tgsnew it stkparsed :
+  ¬ item_either_grants_write tgold tgs it →
+  retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+  stack_sub_tail stklog1 (ItSharedRW tgs :: it :: stkparsed) →
+  ∃ stklog1' stklog2',
+    retag_sharedrw_extend tgold tgsnew stklog1' stklog2' ∧
+    stack_sub_tail stklog1' stkparsed ∧
+    (∀ stkparsed', stack_sub_tail stklog2' stkparsed' → stack_sub_tail stklog2 (ItSharedRW tgs :: it :: stkparsed')).
+Proof.
+  intros Hit Hretagl Hsub.
+  inversion Hsub as [| |? ? ? ? ? Hsubit|]; subst.
+  - do 2 eexists; split; last split; [done..|].
+    intros stkparsed' Hsub'. by apply stack_sub_tail_drop_both.
+  - inversion Hretagl; subst; last inversion Hsubit. clear Hretagl.
+    do 2 eexists; split; last split; [done..|].
+    intros stkparsed' Hsub'. by apply stack_sub_tail_drop_one.
+  - inversion Hretagl as [|? ? ? Hretagl'|? ? ? ? Hgrants]; last first.
+    + exfalso. apply Hit. rewrite /item_either_grants_write.
+      destruct Hgrants as [Hgrants|Hgrants].
+      * left. constructor. inversion Hgrants. set_solver.
+      * right. by eapply stack_sub_unique_item_grants.
+    + apply retag_sharedrw_extend_inv_tail_item in Hretagl' as (stklog3 & -> & Hretagl'); last first.
+      { by eapply stack_sub_unique_is_tail_item. }
+      subst. do 2 eexists; split; last split; [done..|].
+      intros stkparsed' Hsub'. apply stack_sub_tail_keep; [set_solver|done..].
+Qed.
+
+Lemma retag_sharedrw_single_extend_tail tgold tgsnew stkphys1 stkphys2 stkparsed1 stklog1 stklog2 :
+  retag_sharedrw_single' tgold tgsnew stkphys1 = stkphys2 →
+  retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+  stack_parse_tail stkphys1 stkparsed1 →
+  stack_sub_tail stklog1 stkparsed1 →
+  ∃ stkparsed2, stack_parse_tail stkphys2 stkparsed2 ∧ stack_sub_tail stklog2 stkparsed2.
+Proof.
+  intros Hretagp Hretagl Hparse Hsub.
+  generalize dependent stklog2.
+  generalize dependent stklog1.
+  generalize dependent stkphys2.
+  induction Hparse as [|tgs it stk stk' Htailit Hparse IH|it stk stk' Htailit Hparse IH];
+    intros stkphys2 Hretagp stklog1 Hsub stklog2 Hretagl.
+  - simpl in Hretagp. rewrite -Hretagp. exists []; split; first apply stack_parse_tail_empty.
+    inversion Hsub in Hretagl. inversion Hretagl. apply stack_sub_tail_empty.
+  - apply retag_sharedrw_single'_inv_sharedrw in Hretagp as (stkphys2' & Hretagp & [[Heither Heq]|[Heither Heq]]); last done.
+    + eapply stack_sub_tail_split_sharedrw1 in Hsub as (? & ? & ? & ? & Hback); last done.
+      clear Hretagl.
+      edestruct IH as (? & ? & ?); [eassumption..|].
+      rewrite Heq. eexists; split; first by apply stack_parse_tail_shared.
+      by apply Hback.
+    + eapply stack_sub_tail_split_sharedrw2 in Hsub as (? & ? & ? & ? & Hback); [|done..].
+      clear Hretagl.
+      edestruct IH as (? & ? & ?); [eassumption..|].
+      rewrite Heq. eexists; split; first by apply stack_parse_tail_shared.
+      by apply Hback.
+  - apply retag_sharedrw_single'_inv_unique in Hretagp as (stkphys2' & Hretagp & [[Heither Heq]|[Heither Heq]]); last done.
+    + eapply stack_sub_tail_split_sharedrw1 in Hsub as (? & ? & ? & ? & Hback); last done.
+      clear Hretagl.
+      edestruct IH as (? & ? & ?); [eassumption..|].
+      rewrite Heq. eexists; split; first by apply stack_parse_tail_shared.
+      assert (tgsnew = tgsnew ∪ ∅) as -> by set_solver.
+      by apply Hback.
+    + eapply stack_sub_tail_split_sharedrw2 in Hsub as (? & ? & ? & ? & Hback); last done; last first.
+      { intros Hgrants. apply Heither. destruct Hgrants as [Hgrants|Hgrants]; last assumption.
+        inversion Hgrants. set_solver. }
+      clear Hretagl.
+      edestruct IH as (? & ? & ?); [eassumption..|].
+      rewrite Heq. eexists; split; first by apply stack_parse_tail_noshared.
+      by apply Hback.
+Qed.
+
+Lemma merge_push_sharedro_tail tgs stkphys stkparsed :
+  stack_parse_tail stkphys stkparsed →
+  merge_push (ItSharedRO tgs) stkphys = ItSharedRO tgs :: stkphys.
+Proof.
+  intros Hparse. inversion Hparse; [done..|].
+  by rewrite (merge_push_tail_item_r it); last done.
+Qed.
+
+Lemma retag_sharedrw_single'_inv_sharedro tgs tgold tgsnew stkphys1 stkphys2 :
+  retag_sharedrw_single' tgold tgsnew (ItSharedRO tgs :: stkphys1) = stkphys2 →
+  ∃ stkphys2',
+    retag_sharedrw_single' tgold tgsnew stkphys1 = stkphys2' ∧
+    stkphys2 = merge_push (ItSharedRO tgs) stkphys2'.
+Proof.
+  intros Hretag.
+  rewrite /retag_sharedrw_single' in Hretag; case_decide as Hit; rewrite -/retag_sharedrw_single' in Hretag.
+  { inversion Hit. }
+  eexists; split; last first.
+  - symmetry in Hretag. rewrite Hretag. done.
+  - done.
+Qed.
+
+Lemma retag_sharedrw_extend_inv_sharedro tgold tgsnew tgs stklog1 stklog2 :
+  retag_sharedrw_extend tgold tgsnew (ItSharedRO tgs :: stklog1) stklog2 →
+  ∃ stklog3, stklog2 = ItSharedRO tgs :: stklog3 ∧ retag_sharedrw_extend tgold tgsnew stklog1 stklog3.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma retag_sharedrw_single_extend tgold tgsnew stkphys1 stkphys2 stklog1 stklog2 :
+  retag_sharedrw_single tgold tgsnew stkphys1 = Some stkphys2 →
+  retag_sharedrw_extend tgold tgsnew stklog1 stklog2 →
+  stack_rel_stack stkphys1 stklog1 →
+  stack_rel_stack stkphys2 stklog2.
+Proof.
+  intros Hretagp Hretagl (stkparsed1 & Hparse1 & Hsub1).
+  apply retag_sharedrw_single_inv in Hretagp as (stkphys2' & Hwrite & Hretagp).
+  inversion Hparse1; subst stkphys1 stkparsed1; inversion Hsub1.
+  - apply retag_sharedrw_single'_inv_sharedro in Hretagp as (stkphys3 & Heq3 & Hretagp).
+    subst. apply retag_sharedrw_extend_inv_sharedro in Hretagl as (stklog3 & Heql3 & Hretagl).
+    edestruct retag_sharedrw_single_extend_tail as (stkparsed4 & Hparse4 & Hsub4); [done..|].
+    erewrite merge_push_sharedro_tail; last done.
+    eexists; split; first by apply stack_parse_shared.
+    rewrite Heql3. by apply stack_sub_keep_shared.
+  - apply retag_sharedrw_single'_inv_sharedro in Hretagp as (stkphys3 & Heq3 & Hretagp).
+    subst.
+    edestruct retag_sharedrw_single_extend_tail as (stkparsed4 & Hparse4 & Hsub4); [done..|].
+    erewrite merge_push_sharedro_tail; last done.
+    eexists; split; first by apply stack_parse_shared.
+    by apply stack_sub_drop_shared.
+  - subst.
+    apply retag_sharedrw_extend_inv_sharedro in Hretagl as (stklog3 & Heql3 & Hretagl).
+    edestruct retag_sharedrw_single_extend_tail as (stkparsed4 & Hparse4 & Hsub4); [done..|].
+    eexists; split; first by apply stack_parse_noshared.
+    rewrite Heql3. by apply stack_sub_keep_shared.
+  - subst.
+    edestruct retag_sharedrw_single_extend_tail as (stkparsed4 & Hparse4 & Hsub4); [done..|].
+    eexists; split; first by apply stack_parse_noshared.
+    by apply stack_sub_drop_shared.
+Qed.
 
 (** * Logical popping *)
 Lemma log_pop_preserve_tail stkparsed stklog1 stklog2 :