Home

Module PreservationStackKconstrotherBase

Load PreservationHeader.

Lemma goal :
  forall obj ar i h P tinit init body vars k2 current other sf, sf = (StackFrame.Kconstrother obj ar i (h, P) tinit init body vars Constructor.base k2 current other) -> forall (Hin: In sf (State.stack s2)), stackframe_weak_inv prog s2 sf.
Proof.
 inversion Hs1.
 Opaque concat cs_le_dec Zminus.
 inversion step; intros; subst; unfold stackframe_weak_inv in *; simpl in *; unfold Globals.update in *; simpl in *; subst; try exact (stack _ Hin); try exact (stack _ (or_intror _ Hin)); try (destruct Hin as [? | Hin2]; [ discriminate | exact (stack _ Hin2) ]).

symmetry in H1.
destruct Hin as [ | Hin2].
 discriminate.
generalize (stack _ Hin2).
intro; invall; subst.
esplit.
split.
 eassumption.
esplit.
split.
 eapply Globals.valid_pointer_new; simpl; eauto.
eauto 8.

 destruct Hin as [ | Hin2].
  discriminate.
 generalize (stack _ (or_intror _ Hin2)).
 intro; invall; subst.
 rewrite H2.
 rewrite if_some_commut.
 esplit.
 split.
  reflexivity.
 esplit.
 split.
  eassumption.
 esplit.
 split.
  eassumption.
 esplit.
 split.
  eassumption.
 split.
 sdestruct (pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, P)))
 ); trivial.
 destruct k2; invall; subst.
  sdestruct (
    pointer_eq_dec (A:=A)
    (obj,
      (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
    (obj0, (ar0, i0, (h, P ++ current :: nil)))
  ); eauto 10.
 sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
 ).
  discriminate.
 eauto 10.

sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, P)))
).
 apply False_rect.
 injection e; intros; subst.
 generalize (stack _ (or_intror _ Hin)).
 intro; invall; subst.
 revert kind.
 unfold state_kind_inv.
 simpl.
 destruct 1; unfold_ident_in_all; abstract congruence.
generalize (stack _ (or_intror _ Hin)).
intro.
destruct k2.
 sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
                        (obj0, (ar0, i0, (h, P ++ current :: nil)))
 ).
  apply False_rect.
  invall; subst.
  destruct P.
   discriminate.
  destruct P; discriminate.
 assumption.
sdestruct (
 pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 discriminate.
assumption.

destruct Hin as [Heq | Hin2].
 injection Heq.
 intros; subst.
 generalize (StackFrame.Kconstrother_base_inj Heq).
 intro; invall; subst.
 revert kind.
 unfold state_kind_inv.
 simpl.
 intro; invall; subst.
 sdestruct (
pointer_eq_dec (A:=A)
           (obj0,
           (ar0, i0,
           (match k0 with
            | Constructor.direct_non_virtual => h0
            | Constructor.virtual => Class.Inheritance.Shared
            end,
           match k0 with
           | Constructor.direct_non_virtual => P ++ current :: nil
           | Constructor.virtual => current :: nil
           end))) (obj0, (ar0, i0, (h0, P)))
 ).
  apply False_rect.
  destruct k0; invall; subst.
   injection e.
   intro.
   generalize (refl_equal (length P)).
   rewrite <- H10 at 1.
   rewrite app_length.
   simpl.
   intro.
   assert ((length P + 1)%nat = length P) by assumption.
   omegaContradiction.
  discriminate.
esplit.
split.
 eassumption.
esplit.
split.
 eassumption.
esplit.
split.
 eassumption.
esplit.
split.
 eassumption.
split.
 trivial.
destruct k0; invall; subst.
 sdestruct (
 pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, P ++ current :: nil)))
            (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  esplit.
  split.
   eassumption.
  left; trivial.
 abstract congruence.
sdestruct (
   pointer_eq_dec (A:=A)
            (obj0, (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
            (obj0, (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 eauto 8.
 abstract congruence.
generalize (stack _ (or_intror _ Hin2)).
intro.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj,
           (ar, i,
           (match k2 with
            | Constructor.direct_non_virtual => h
            | Constructor.virtual => Class.Inheritance.Shared
            end,
           match k2 with
           | Constructor.direct_non_virtual => p ++ b :: nil
           | Constructor.virtual => b :: nil
           end))) (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 injection e; intros; subst.
 revert kind.
 unfold state_kind_inv.
 simpl.
 intro; invall; subst.
 destruct k2; invall; subst.
  generalize (H14 _ (or_introl _ (refl_equal _))).
  intro; unfold_ident_in_all; abstract congruence.
 generalize (H16 _ (or_introl _ (refl_equal _))).
 intro; unfold_ident_in_all; abstract congruence.
destruct k0.
 sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match k2 with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match k2 with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end))) (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
invall.
eauto 16.
sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match k2 with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match k2 with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
invall; eauto 16.

generalize (stack _ (or_intror _ Hin)).
intro.
sdestruct (
pointer_eq_dec (A:=A)
           (obj,
           (ar, i,
           (match k2 with
            | Constructor.direct_non_virtual => h
            | Constructor.virtual => Class.Inheritance.Shared
            end,
           match k2 with
           | Constructor.direct_non_virtual => p ++ b :: nil
           | Constructor.virtual => b :: nil
           end))) (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 injection e; intros; subst.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl; intro; invall; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 destruct k2; simpl; intro; invall; subst; unfold_ident_in_all; abstract congruence.
destruct k0.
 sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match k2 with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match k2 with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end))) (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
 apply False_rect.
 invall; subst.
 destruct k2.
  injection e; intros; subst.
  generalize (last_complete p b).
  unfold_ident_in_all.
  rewrite H0.
  rewrite last_complete.
  injection 1; intros; subst.
  generalize (app_reg_r H0).
  intro; subst.
  destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
  destruct (H7 _ _ _ _ (refl_equal _)).
  generalize (H9 _ _ _ (refl_equal _)).
  eauto using relptr_gt_irrefl.
 destruct P.
  discriminate.
 destruct P; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match k2 with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match k2 with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
apply False_rect.
 invall; subst.
 destruct k2.
  generalize (stack _ (or_introl _ (refl_equal _))).
  intros; invall; subst.
  destruct p.
   discriminate.
  destruct p; discriminate.
 injection e; intros; subst.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl; intros; invall; subst.
 destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
  destruct (H4 _ _ _ _ (refl_equal _)).
  generalize (H11 _ _ _ (refl_equal _)).
  eauto using relptr_gt_min.

generalize (stack _ Hin).
intro.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 injection e; intros; subst.
 invall; subst.
 destruct (stack_state_wf _ Hin).
 generalize (H2 _ _ _ (refl_equal _)).
 eauto using relptr_gt_irrefl.
destruct k2.
 sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
                        (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
 invall; subst; eauto 16.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
invall; subst; eauto 16.


destruct Hin as [ | Hin2] .
 discriminate.
destruct Hin2 as [ | Hin ].
 discriminate.
generalize (stack _ (Hin)).
intro.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i, (h, P)))
 ).
 apply False_rect.
 revert kind.
 unfold state_kind_inv.
 simpl; injection e; intros; invall; subst.
 assert (0 <= i <= i) by abstract omega.
 generalize (H20 _ H5).
 unfold_ident_in_all; abstract congruence.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A)
                        (obj,
                        (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
                        (obj0, (ar0, i, (h, P ++ current :: nil)))
 ).
  2 : assumption.
 apply False_rect.
 invall; subst.
 destruct P.
  discriminate.
 destruct P; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
                        (obj0,
                        (ar0, i, (Class.Inheritance.Shared, current :: nil)))
).
 discriminate.
assumption.

sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 injection e; intros; subst.
 destruct (stack_state_wf _ Hin).
 generalize (H2 _ _ _ (refl_equal _)).
 eauto using SubobjectOrdering.relptr_gt_irrefl.
generalize (stack _ Hin).
intro; destruct k2.
 sdestruct (
   pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
   (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
 apply False_rect.
 injection e; intros; invall; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 intro; invall; subst; unfold_ident_in_all; destruct H14; abstract congruence.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
apply False_rect.
injection e; intros; invall; subst.
revert kind.
unfold state_kind_inv; simpl.
intro; invall; subst; unfold_ident_in_all; destruct H16; abstract congruence.

destruct Hin as [ | Hin2].
 discriminate.
destruct Hin2 as [ | Hin].
 discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj,
           (ar, i,
           (match beta with
            | Constructor.direct_non_virtual => h
            | Constructor.virtual => Class.Inheritance.Shared
            end,
           match beta with
           | Constructor.direct_non_virtual => p ++ b :: nil
           | Constructor.virtual => b :: nil
           end))) (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 destruct beta.
 injection e; intros; subst.
  destruct (stack_state_wf _ Hin).
  generalize (H _ _ _ (refl_equal _)).
  inversion 1.
   subst.
   rewrite last_complete in H11.
   injection H11; intro; subst.
   unfold state_kind_inv in kind.
   simpl in kind.
   invall; subst.
   inversion H8; subst.
   inversion H25; subst.
   rewrite (path_last H23) in H9.
   injection H9; intros; subst.
   assert (In (Class.Inheritance.Repeated, cn) (Class.super x2)).
    eapply in_map_bases_elim.
    eapply in_rev_elim.
    rewrite H15.
   eauto using in_or_app.
  assert (path (Program.hierarchy prog) cn (p ++ cn :: nil) through h0).
    eapply path_concat.
    eassumption.
    eleft with (lf := cn :: nil) (lt := x1 :: nil).
    reflexivity.
    reflexivity.
    simpl.
    rewrite H10.
    sdestruct (
      In_dec super_eq_dec (Class.Inheritance.Repeated, cn) (Class.super x2)
    ).
    rewrite H1.
    trivial.
   contradiction.
  Transparent concat. simpl.
  rewrite (path_last H23).
  destruct (peq x1 x1); unfold_ident_in_all; abstract congruence.
 generalize (path_concat H26 H12 H13).
 intro.
 generalize (path_last H27).
 rewrite (path_last H23).
 injection 1; intros; subst.
 destruct (Plt_irrefl to').
 eapply Ple_Plt_trans.
 eapply Well_formed_hierarchy.path_le.
  eassumption.
  eexact H12.
 eapply Well_formed_hierarchy.well_founded.
 eassumption.
 2 : eassumption.
 assumption.
generalize (refl_equal (length ar0)).
rewrite H8 at 1.
rewrite app_length.
destruct l.
 abstract congruence.
simpl; intro; omegaContradiction.
injection e; intros; subst.
destruct (stack_state_wf _ Hin _ (refl_equal _)).
invall.
generalize (refl_equal (length ar0)).
rewrite H0 at 1.
destruct x.
 abstract congruence.
rewrite app_length.
simpl; intro; omegaContradiction.
generalize (stack _ Hin).
intro.
destruct k2.
 sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match beta with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match beta with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end))) (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
 apply False_rect.
 revert kind.
 unfold state_kind_inv; simpl.
 injection e;
 invall; intros; destruct beta; invall; subst.
  generalize (last_complete p b).
  rewrite H8.
  rewrite last_complete.
  injection 1; intro; subst.
  generalize (app_reg_r H8).
  intro; unfold_ident_in_all; abstract congruence.
 destruct P.
  discriminate.
 destruct P; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
                        (obj,
                        (ar, i,
                        (match beta with
                         | Constructor.direct_non_virtual => h
                         | Constructor.virtual => Class.Inheritance.Shared
                         end,
                        match beta with
                        | Constructor.direct_non_virtual => p ++ b :: nil
                        | Constructor.virtual => b :: nil
                        end)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
apply False_rect.
revert kind.
unfold state_kind_inv; simpl.
destruct beta; intro.
 clear H.
 invall; subst.
 destruct p.
  discriminate.
 destruct p0; discriminate.
invall; subst.
generalize (H21 _ (or_introl _ (refl_equal _))).
unfold_ident_in_all; destruct H13; abstract congruence.
  
sdestruct (
 (pointer_eq_dec (A:=A) (obj, (ar, i, hp)) (obj0, (ar0, i0, (h, P)))
)).
 apply False_rect.
 injection e; intros; subst.
 destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
 destruct (H _ _ _ _ (refl_equal _)).
 revert kind.
 unfold state_kind_inv; simpl.
 destruct hp'.
 destruct beta; intro; invall; subst.
  generalize (H1 _ _ _ (refl_equal _)).
  inversion 1.
   subst.
   rewrite last_complete in H17.
   injection H17; intro; subst.
   generalize (concat_last (path_nonempty H18) H19).
   rewrite (path_last H18).
   intro.
   generalize (stack _ (or_introl _ (refl_equal _))).
   simpl.
   intro; invall; subst.
   rewrite last_complete in H6.
   injection H6; intros; subst.
   replace x5 with to' in * by abstract congruence.
   apply (Plt_irrefl to').
   eapply Ple_Plt_trans with x1.
   eauto using Well_formed_hierarchy.path_le.
   eapply Well_formed_hierarchy.well_founded.
   eassumption.
   eassumption.
   eapply in_map_bases_elim.
   eapply in_rev_elim.
   rewrite H23.
   eauto using in_or_app.
  generalize (refl_equal (length ar')).
  rewrite H14 at 1.
  rewrite app_length.
  destruct l0.
   congruence.
  simpl; intro; omegaContradiction.
 generalize (H1 _ _ _ (refl_equal _)).
 inversion 1.
  subst.
  injection H17; intros; subst.
  generalize (concat_last (path_nonempty H18) H19).
  rewrite (path_last H18).
  intro.
  generalize (stack _ (or_introl _ (refl_equal _))).
  simpl.
  intro; invall; subst.
  injection H6; intros; subst.
  injection H10; intros; subst.
  apply (Plt_irrefl to').
   eapply Ple_Plt_trans with x1.
   eauto using Well_formed_hierarchy.path_le.
   eapply Well_formed_hierarchy.is_virtual_base_of_lt.
   eassumption.
   eapply vborder_list_virtual_base.
   eassumption.
   eassumption.
   eauto using in_rev_intro, in_or_app.
  generalize (refl_equal (length ar')).
  rewrite H14 at 1.
  rewrite app_length.
  destruct l0.
   congruence.
  simpl; intro; omegaContradiction.
generalize (stack _ (or_intror _ Hin)).
intros.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, hp))
                        (obj0, (ar0, i0, (h, P ++ current :: nil)))
 ).
  2 : assumption.
 apply False_rect.
 injection e; intros; invall; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 destruct beta; intro; invall; subst.
  destruct hp'; invall; subst.
  generalize (last_complete l b).
  rewrite <- H18.
  rewrite last_complete.
  injection 1; intros; subst.
  generalize (app_reg_r H18).
  intro; subst.
  destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
  destruct (H12 _ _ _ _ (refl_equal _)).
  generalize (H16 _ _ _ (refl_equal _)).
  apply relptr_gt_irrefl.
  assumption.
 destruct hp'; invall; subst.
 destruct P.
  discriminate.
 destruct P; discriminate.
sdestruct(
pointer_eq_dec (A:=A) (obj, (ar, i, hp))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
 apply False_rect.
 injection e; intros; invall; subst.
 revert kind.
 unfold state_kind_inv.
 simpl.
 destruct beta; intro; invall; subst.
  destruct hp'; invall; subst.
  generalize (stack _ (or_introl _ (refl_equal _))).
  simpl.
  intros; invall; subst.
  destruct l.
   discriminate.
  destruct l; discriminate.
 destruct hp'; invall; subst.
 injection H18; intros; subst.
 injection H3; intro; subst.
 generalize (stack _ (or_introl _ (refl_equal _))).
 intro; invall; subst.
 destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
 destruct (H10 _ _ _ _ (refl_equal _)).
 generalize (H21 _ _ _ (refl_equal _)).
 eauto using relptr_gt_min.

sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, P)))
).
 apply False_rect.
 injection e; intros; subst.
 destruct (stack_state_wf _ Hin _ (refl_equal _)).
 invall.
 destruct x.
  congruence.
 generalize (refl_equal (length ar0)).
 rewrite H1 at 1.
 rewrite app_length.
 simpl; intro; omegaContradiction.
generalize (stack _ Hin).
intro.
destruct k2.
 sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
                        (obj0, (ar0, i0, (h0, P ++ current :: nil)))
 ).
  2 : assumption.
apply False_rect.
injection e; intros; invall; subst.
destruct (stack_state_wf _ Hin _ (refl_equal _)).
 invall.
 destruct x.
  congruence.
 generalize (refl_equal (length ar0)).
 rewrite H2 at 1.
 rewrite app_length.
 simpl; intro; omegaContradiction.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
                        (obj0,
                        (ar0, i0, (Class.Inheritance.Shared, current :: nil)))
).
 2 : assumption.
apply False_rect.
injection e; intros; invall; subst.
destruct (stack_state_wf _ Hin _ (refl_equal _)).
 invall.
 destruct x.
  congruence.
 generalize (refl_equal (length ar0)).
 rewrite H2 at 1.
 rewrite app_length.
 simpl; intro; omegaContradiction.

Qed.

End Preservation.