prove logical disabling lemma

theories/lang/stbor/stbor_sim.v

@@ -481,7 +481,7 @@ Qed.
 (** * Retagging (SharedRW) extend *)
 
 (** * Logical popping *)
-Lemma pop_prefix_preserve_tail stkparsed stklog1 stklog2 :
+Lemma log_pop_preserve_tail stkparsed stklog1 stklog2 :
   stklog2 `suffix_of` stklog1 →
   stack_sub_tail stklog1 stkparsed →
   stack_sub_tail stklog2 stkparsed.
@@ -506,7 +506,7 @@ Proof.
       apply stack_sub_tail_drop_both. eapply IH. eassumption.
 Qed.
 
-Lemma pop_prefix_preserve stkphys stklog1 stklog2 :
+Lemma log_pop_prefix_preserve stkphys stklog1 stklog2 :
   stklog2 `suffix_of` stklog1 →
   stack_rel_stack stkphys stklog1 →
   stack_rel_stack stkphys stklog2.
@@ -520,12 +520,65 @@ Proof.
     + rewrite -app_comm_cons in Hsuffix. inversion Hsuffix.
       eexists; split; first apply Hparse.
       apply stack_sub_drop_shared.
-      eapply pop_prefix_preserve_tail; last eassumption.
+      eapply log_pop_preserve_tail; last eassumption.
       by exists stkdead.
   - eexists; split; first apply Hparse.
     apply stack_sub_drop_shared.
-    eapply pop_prefix_preserve_tail; last eassumption.
+    eapply log_pop_preserve_tail; last eassumption.
     by exists stkdead.
 Qed.
 
 (** * Logical disabling *)
+Inductive log_disable_item : item → item → Prop :=
+| log_disable_item_disable tg : log_disable_item (ItUnique tg) ItDisabled
+| log_disable_item_keep it : log_disable_item it it.
+
+Definition log_disable (stk1 stk2 : stack) : Prop :=
+  Forall2 log_disable_item stk1 stk2.
+
+Lemma log_disable_cons_inv_l it1 stklog1 stklog2 :
+  log_disable (it1 :: stklog1) stklog2 →
+  ∃ it2 stklog2', log_disable_item it1 it2 ∧ log_disable stklog1 stklog2' ∧ stklog2 = it2 :: stklog2'.
+Proof.
+  intros Hdisable.
+  rewrite /log_disable in Hdisable.
+  eapply Forall2_cons_inv_l. apply Hdisable.
+Qed.
+
+Lemma log_disable_preserve_tail stklog2 stkparsed stklog1 :
+  log_disable stklog1 stklog2 →
+  stack_sub_tail stklog1 stkparsed →
+  stack_sub_tail stklog2 stkparsed.
+Proof.
+  intros Hdisable Hsub.
+  generalize dependent stklog2.
+  induction Hsub as [|? ? ? ? ? IH|? ? ? ? ? Hsubit ? IH|? ? ? ? ? ? ? Hsubit ? IH]; intros stklog2 Hdisable.
+  - inversion Hdisable. apply stack_sub_tail_empty.
+  - apply stack_sub_tail_drop_both. apply IH. apply Hdisable.
+  - apply log_disable_cons_inv_l in Hdisable as (it3 & stklog3 & Hdisableit & Hdisable & ->).
+    apply stack_sub_tail_drop_one.
+    { inversion Hdisableit; subst; last assumption. inversion Hsubit. constructor. }
+    apply IH. assumption.
+  - apply log_disable_cons_inv_l in Hdisable as (it3 & stklog3 & Hdisableit3 & Hdisable & ->).
+    apply log_disable_cons_inv_l in Hdisable as (it4 & stklog4 & Hdisableit4 & Hdisable & ->).
+    inversion Hdisableit3; subst.
+    apply stack_sub_tail_keep; first done.
+    { inversion Hdisableit4; subst; last assumption. inversion Hsubit. constructor. }
+    apply IH. assumption.
+Qed.
+
+Lemma log_disable_preserve stklog2 stkphys stklog1 :
+  log_disable stklog1 stklog2 →
+  stack_rel_stack stkphys stklog1 →
+  stack_rel_stack stkphys stklog2.
+Proof.
+  intros Hdisable (stkparsed & Hparse & Hsub).
+  destruct Hsub.
+  - eexists; split; first apply Hparse.
+    apply log_disable_cons_inv_l in Hdisable as (it3 & stklog3 & Hdisableit3 & Hdisable & ->).
+    inversion Hdisableit3. apply stack_sub_keep_shared; first done.
+    by eapply log_disable_preserve_tail.
+  - eexists; split; first apply Hparse.
+    apply stack_sub_drop_shared.
+    by eapply log_disable_preserve_tail.
+Qed.