Home

Module PreservationBreadthDirectNonVirtual

Load PreservationHeader.

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

Lemma nodup : forall cn c, hier ! cn = Some c ->
        forall l0 b1 l1 l2, map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
          match hb with
            | (Class.Inheritance.Shared, _) => false
            | _ => true
          end
        ) (Class.super c)) = (l0 ++ b1 :: l1 ++ b1 :: l2) -> False.
Proof.
  intros.
  generalize (NoDup_repeated_bases (Well_formed_hierarchy.bases_no_dup hierarchy_wf H)).
  intro.
  eauto using NoDup_elim.
Qed.

Lemma goal : forall obj ar i h p hp,
    valid_pointer hier (Globals.heap (State.global s2)) (Value.subobject obj ar i h p hp) ->
    forall cn, last p = Some cn ->
      forall c, hier ! cn = Some c ->
        forall l0 b1 l1 b2 l2, map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
          match hb with
            | (Class.Inheritance.Shared, _) => false
            | _ => true
          end
        ) (Class.super c)) = (l0 ++ b1 :: l1 ++ b2 :: l2) ->
        constructed_sibling_before (assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p ++ b1 :: nil))) (State.construction_states s2)) (assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p ++ b2 :: nil))) (State.construction_states s2))
        .
Proof.
 inversion Hs1.
 inversion step; subst; simpl in *; unfold Globals.update in *; simpl in *; subst; try assumption.

intros until 1.
symmetry in H1.
unfold Globals.new in H1.
injection H1; intros until 2; subst; simpl in *.
inversion H2; subst; simpl in *.
destruct (peq (obj0) (Globals.next_object gl)).
 rewrite e in H5.
rewrite PTree.gss in H5.
injection H5; 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 H5.
 2 : assumption.
assert (valid_pointer (Program.hierarchy prog) (Globals.heap gl) (Value.subobject (obj0) ar i h p hp0)).
 econstructor; eauto.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b1 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b2 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b1 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b2 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
eauto.

intros.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
 ).
  injection e; intros; subst.
  destruct (list_cons_right_inj H6).
  subst.
  sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
           (obj0, (ar0, i0, (h0, (p0 ++ b2 :: nil))))
  ).
   injection e0; intros.
   destruct (list_cons_right_inj H7).
   subst.
   apply False_rect; eauto using nodup.
  forward.
 eapply breadth_non_virtual_bases.
 eassumption.
 eassumption.
 eassumption.
 eassumption.
 unfold state_kind_inv in kind.
 simpl in kind.
 invall; subst.
 unfold_ident_in_all.
 rewrite (H16 _ (or_introl _ (refl_equal _))).
 simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
destruct (list_cons_right_inj H6).
subst.
cut (
 (assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
        cs) = Some Constructed
).
 unfold_ident.
 intro.
 rewrite H7.
 fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
apply H13.
assert (l0 ++ b1 :: l1 ++ b2 :: l2 = x3 ++ b2 :: q).
 unfold_ident_in_all.
 rewrite <- H14.
 rewrite <- H5.
 replace x2 with c0 by congruence.
 trivial.
 generalize (NoDup_repeated_bases (Well_formed_hierarchy.bases_no_dup hierarchy_wf H4)).
 rewrite H5.
 intro.
 replace (l0 ++ b1 :: l1 ++ b2 :: l2) with ((l0 ++ b1 :: l1) ++ b2 :: l2) in H7, H16.
 generalize (NoDup_uniq H16 H7).
 injection 1; intros; subst.
 eauto using in_or_app.
 rewrite app_ass; reflexivity.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
).
 destruct p0.
   discriminate.
 destruct p0; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 destruct p0.
   discriminate.
 destruct p0; discriminate.
eauto.

intros.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
 ).
  injection e; intros; subst.
  destruct (list_cons_right_inj H3).
  subst.
  sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
           (obj0, (ar0, i0, (h0, (p0 ++ b2 :: nil))))
  ).
   injection e0; intros.
   destruct (list_cons_right_inj H4).
   subst.
   apply False_rect; eauto using nodup.
  forward.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
destruct (list_cons_right_inj H3).
subst.
cut (
 (assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
        cs) = Some Constructed
).
 unfold_ident.
 intro.
 rewrite H4.
 fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H4; simpl; omega.
unfold_ident_in_all; rewrite H4; simpl; omega.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
).
 injection e; intros; subst.
 sdestruct (
 pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
 ).
  injection e0; intro.
  destruct (list_cons_right_inj H5).
  subst.
  apply False_rect; eauto using nodup.
 forward.
 unfold state_kind_inv in kind.
 simpl in kind.
 invall; subst.
 eapply constructed_sibling_before_none.
 eauto.
 unfold_ident_in_all; rewrite H7; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
cut (
  (assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b1 :: 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.


intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i, (h, p ++ b1 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i, (h, p ++ b2 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
).
 injection e; intros; subst.
 sdestruct (
pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
 ).
  injection e0.
  intro.
  destruct (list_cons_right_inj H6).
  subst.
  apply False_rect; eauto using nodup.
 forward.
 unfold state_kind_inv in kind.
 simpl in kind.
 invall; subst.
 eapply constructed_sibling_before_destructed.
 eauto.
 unfold_ident_in_all; rewrite H8; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
cut (
(assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
        cs) = Some Constructed
).
 unfold_ident.
 intro.
 rewrite H6.
 fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H7; simpl; omega.
unfold_ident_in_all; rewrite H7; simpl; omega.

intros.
destruct beta.
 sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
 ).
  injection e; intros; subst.
  destruct (list_cons_right_inj H7).
  subst.
  sdestruct (
 pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
  ).
   injection e0; intro.
   destruct (list_cons_right_inj H8).
   subst.
   apply False_rect; eauto using nodup.
  unfold state_kind_inv in kind.
  simpl in kind.
  invall; subst.
  unfold_ident_in_all.
  forward.
  apply H14.
  assert (l0 ++ b1 :: l1 ++ b2 :: l2 = rev bases ++ b1 :: rev x3).
   replace (rev bases ++ b1 :: rev x3) with (rev (x3 ++ b1 :: bases)).
   rewrite <- H13.
   rewrite rev_involutive.
   rewrite <- H6.
   replace x2 with c0 by congruence.
   trivial.
  rewrite rev_app.
  simpl.
  rewrite app_ass.
  reflexivity.
 generalize (NoDup_repeated_bases (Well_formed_hierarchy.bases_no_dup hierarchy_wf H5)).
 unfold_ident_in_all.
 rewrite H6.
 intro.
 generalize (NoDup_uniq H19 H17).
 injection 1; intros; subst.
 eapply in_rev_elim.
 rewrite <- H21.
 eauto using in_or_app.
 sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
 ).
 2 : eauto.
 injection e; intros; subst.
 destruct (list_cons_right_inj H7).
 subst.
 unfold state_kind_inv in kind.
 simpl in kind.
 invall; subst.
 cut (
 assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
          cs = Some Constructed
 ).
  unfold_ident.
  intro.
  rewrite H8.
  fin.
 apply H16.
 right.
 assert (l0 ++ b1 :: l1 ++ b2 :: l2 = rev bases ++ b2 :: rev x3).
   replace (rev bases ++ b2 :: rev x3) with (rev (x3 ++ b2 :: bases)).
   unfold_ident_in_all.
   rewrite <- H13.
   rewrite rev_involutive.
   rewrite <- H6.
   replace x2 with c0 by congruence.
   trivial.
  rewrite rev_app.
  simpl.
  rewrite app_ass.
  reflexivity.
 generalize (NoDup_repeated_bases (Well_formed_hierarchy.bases_no_dup hierarchy_wf H5)).
 unfold_ident_in_all.
 rewrite H6.
 intro.
 replace (l0 ++ b1 :: l1 ++ b2 :: l2) with ((l0 ++ b1 :: l1) ++ b2 :: l2) in H8, H17.
 generalize (NoDup_uniq H17 H8).
 injection 1; intros; subst.
 eapply in_rev_elim.
 rewrite <- H21.
 eauto using in_or_app.
 rewrite app_ass.
 reflexivity.
sdestruct (pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b1 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
sdestruct (pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b2 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, hp))
           (obj0, (ar0, i0, (h, p ++ b1 :: nil)))
).
 injection e; intros; subst.
 sdestruct (
 pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h, p ++ b1 :: nil)))
           (obj0, (ar0, i0, (h, p ++ b2 :: nil)))
 ).
  apply False_rect.
  injection e0.
  intro.
  destruct (list_cons_right_inj H3).
  subst.
  eauto using nodup.
 unfold state_kind_inv in kind; simpl in kind; invall; subst.
 forward.
 eapply constructed_sibling_before_destructed.
 eauto.
 unfold_ident_in_all; rewrite H4; simpl; omega.
sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, hp))
           (obj0, (ar0, i0, (h, p ++ b2 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
cut (
   (assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h, p ++ b1 :: nil))) cs) = Some Constructed
).
 unfold_ident.
 intro.
 rewrite H3.
 fin.
unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all; rewrite H4; simpl; omega.
unfold_ident_in_all; rewrite H4; 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, i0, (h, p ++ b1 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, x1 :: nil)))
           (obj0, (ar0, i0, (h, p ++ b2 :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
eauto.

Qed.

End Preservation.