Module PreservationBreadthArrays

Load PreservationHeader.

Ltac forward := constructor; simpl; intros; try discriminate; try omegaContradiction.
Ltac fin := forward; reflexivity.

Lemma goal :forall obj o,
  (Globals.heap (State.global s2)) ! obj = Some o ->
    forall ar cn n,
      valid_array_path hier cn n (Object.class o) (Object.arraysize o) ar ->
      match last ar with
        | None => n = Object.arraysize o /\ cn = Object.class o
        | Some (_, _, fs) => exists n', n = Zpos n' /\ FieldSignature.type fs = FieldSignature.Struct cn n'
      end ->
      forall i1 i2, 0 <= i1 -> i1 < i2 -> i2 < n ->
        constructed_sibling_before (assoc (@pointer_eq_dec _) (obj, (ar, i1, (Class.Inheritance.Repeated, cn :: nil))) (State.construction_states s2)) (assoc (@pointer_eq_dec _) (obj, (ar, i2, (Class.Inheritance.Repeated, cn :: nil))) (State.construction_states s2))
        .

Proof.

inversion Hs1.
inversion step; subst; simpl in *; unfold Globals.update in *; simpl in *; subst; try assumption.

symmetry in H1.
unfold Globals.new in H1.
injection H1; intros until 2; subst; simpl in *.
intros until 1.
destruct (peq obj (Globals.next_object gl)).
subst.
rewrite PTree.gss in H2.
injection H2; intros; subst; simpl in *.
rewrite (construction_states_none _ (Globals.valid_none valid_global (Ple_refl _))).
rewrite (construction_states_none _ (Globals.valid_none valid_global (Ple_refl _))).
fin.
rewrite PTree.gso in H2; eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
  injection e0; intros; subst.
  abstract omegaContradiction.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
apply H17.
assert (n0 = n).
  revert H13 H4.
  destruct (last ar0).
   destruct p.
   destruct p.
   intros; invall; congruence.
  intros; invall; congruence.
subst.
omega.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs) = Some Constructed
).
unfold_ident.
intro.
rewrite H10.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
apply H14.
omega.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
forward.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs) = Some Constructed
).
unfold_ident.
intro.
rewrite H5.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H5; simpl; omega.
unfold_ident_in_all; rewrite H5; simpl; omega.

revert kind.
unfold state_kind_inv.
simpl.
intros; invall; subst.
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, i1, (Class.Inheritance.Repeated, cn :: nil)))
).
destruct k2; try discriminate.
destruct p; try discriminate.
destruct p0; 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, i2, (Class.Inheritance.Repeated, cn :: nil)))
).
destruct k2; try discriminate.
destruct p; try discriminate.
destruct p0; discriminate.
eauto.

generalize (stack _ (or_introl _ (refl_equal _))).
simpl; intros; invall; subst.
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, i1, (Class.Inheritance.Repeated, cn :: nil)))
).
forward.
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, i2, (Class.Inheritance.Repeated, cn :: nil)))
).
destruct k2; try discriminate.
destruct p; try discriminate.
destruct p; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
  injection e0; intro; subst; omegaContradiction.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_none.
eauto.
unfold_ident_in_all; rewrite H9; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs) = Some Constructed
).
unfold_ident.
intro.
rewrite H7.
fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H8; simpl; omega.
unfold_ident_in_all; rewrite H8; simpl; omega.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
  injection e0; intros; subst; omegaContradiction.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
apply H18.
assert (n = x).
  revert H14 H6.
  destruct (last ar0).
   destruct p.
   destruct p.
   intros; invall; congruence.
  intros; invall; congruence.
subst; omega.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs) = Some Constructed
).
unfold_ident.
intro.
rewrite H10.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
apply H15.
omega.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
  injection e0; intros; subst; omegaContradiction.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_destructed.
eauto.
unfold_ident_in_all; rewrite H10; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs)
= Some Constructed
).
unfold_ident.
intro.
rewrite H8.
fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H9; simpl; omega.
unfold_ident_in_all; rewrite H9; simpl; omega.

intros.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
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, i1, (Class.Inheritance.Repeated, cn :: nil)))
).
destruct beta; try discriminate.
destruct p; try discriminate.
destruct p0; 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, i2, (Class.Inheritance.Repeated, cn :: nil)))
).
destruct beta; try discriminate.
destruct p; try discriminate.
destruct p0; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, hp))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn :: nil)))
).
  injection e0; intros; subst; omegaContradiction.
unfold state_kind_inv in kind; simpl in kind; invall; subst.
forward.
eapply constructed_sibling_before_destructed.
eauto.
unfold_ident_in_all; rewrite H6; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, hp))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn :: nil))) cs)
= Some Constructed
).
unfold_ident.
intro.
rewrite H5.
fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H6; simpl; omega.
unfold_ident_in_all; rewrite H6; simpl; omega.

unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, x1 :: nil)))
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
).
injection e; intros; subst.
sdestruct (
pointer_eq_dec (A:=A)
           (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
  injection e0; intros; subst; omegaContradiction.
forward.
eapply constructed_sibling_before_destructed.
eauto.
unfold_ident_in_all; rewrite H1; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, x1 :: nil)))
           (obj0, (ar0, i2, (Class.Inheritance.Repeated, cn0 :: nil)))
).
2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A))
        (obj0, (ar0, i1, (Class.Inheritance.Repeated, cn0 :: nil))) cs) = Some Constructed
).
unfold_ident.
intro.
rewrite H15.
forward.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H1; simpl; omega.
unfold_ident_in_all; rewrite H1; simpl; omega.

Qed.

End Preservation.