Home
Module PreservationBreadthFields
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,
Class.fields c = (
l0 ++
b1 ::
l1 ++
b1 ::
l2) ->
False.
Proof.
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,
Class.fields c = (
l0 ++
b1 ::
l1 ++
b2 ::
l2) ->
constructed_sibling_before (
assoc aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
b1) (
State.field_construction_states s2)) (
assoc aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
b2) (
State.field_construction_states s2))
.
Proof.
inversion Hs1.
Opaque Zminus.
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_fields_none _ (
Globals.valid_none valid_global (
Ple_refl _))).
rewrite (
construction_states_fields_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.
destruct hp.
simpl.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
t,
l),
fs)
(
obj0,
ar0,
i0, (
h,
p),
b1)
).
injection e;
intros;
subst.
cut (
constructed_sibling_before (
Some StartedConstructing)
(
if aux_constr_state_key_eq_dec (
obj0,
ar0,
i0, (
h,
p),
b1)
(
obj0,
ar0,
i0, (
h,
p),
b2)
then Some StartedConstructing
else
assoc aux_constr_state_key_eq_dec (
obj0,
ar0,
i0, (
h,
p),
b2)
auxcs)
);
eauto.
sdestruct (
aux_constr_state_key_eq_dec (
obj0,
ar0,
i0, (
h,
p),
b1)
(
obj0,
ar0,
i0, (
h,
p),
b2)
).
injection e0;
intros;
subst.
apply False_rect.
eauto using nodup.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
generalize (
H14 _ (
or_introl _ (
refl_equal _))).
simpl.
unfold_ident.
intro.
eapply constructed_sibling_before_none.
eauto.
unfold_ident.
rewrite H5.
simpl;
omega.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
t,
l),
fs)
(
obj0,
ar0,
i0, (
h,
p),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc aux_constr_state_key_eq_dec (
obj0,
ar0,
i0, (
h,
p),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H4.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H10.
replace x2 with c in *
by abstract congruence.
rewrite H9 in H3.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H8).
rewrite H9.
intro.
assert (
x3 ++
b2 ::
q = (
l0 ++
b1 ::
l1) ++
b2 ::
l2).
rewrite H3.
rewrite app_ass.
reflexivity.
generalize (
NoDup_uniq H4 H12).
injection 1;
intros;
subst.
eauto using in_or_app.
simpl.
unfold_ident.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
).
forward.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H5.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H11.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H9).
revert H4.
rewrite H10.
replace (
l0 ++
b1 ::
l1 ++
b2 ::
l2)
with ((
l0 ++
b1 ::
l1) ++
b2 ::
l2).
intros.
generalize (
NoDup_uniq H5 H4).
injection 1;
intros;
subst.
eauto using in_or_app.
rewrite app_ass;
reflexivity.
intros until 1.
assert (
valid_pointer (
Program.hierarchy prog)
(
Globals.heap gl) (
Value.subobject obj0 ar0 i0 h0 p0 hp)
).
assumption.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
).
forward.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H9.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H14.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H13).
revert H8.
rewrite H15.
replace (
l0 ++
b1 ::
l1 ++
b2 ::
l2)
with ((
l0 ++
b1 ::
l1) ++
b2 ::
l2).
intros.
generalize (
NoDup_uniq H9 H8).
injection 1;
intros;
subst.
eauto using in_or_app.
rewrite app_ass;
reflexivity.
simpl.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj',
ar',
i', (
h,
p),
fs)
(
obj0,
ar0,
i, (
h0,
p0),
b1)
).
forward.
sdestruct (
aux_constr_state_key_eq_dec (
obj',
ar',
i', (
h,
p),
fs)
(
obj0,
ar0,
i, (
h0,
p0),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec )
(
obj0,
ar0,
i, (
h0,
p0),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H3.
forward.
generalize (
stack _ (
or_introl _ (
refl_equal _))).
simpl.
intros;
invall;
subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all;
rewrite H10;
simpl;
omega.
unfold_ident_in_all;
rewrite H10;
simpl;
omega.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
).
injection e;
intros;
subst.
sdestruct (
aux_constr_state_key_eq_dec (
obj0,
ar0,
i0, (
h0,
p0),
b1)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
injection e0;
intros;
subst.
apply False_rect.
eauto using nodup.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H11.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H9).
revert H3.
rewrite <- (
rev_involutive (
Class.fields c)).
rewrite H10.
rewrite rev_app.
simpl.
rewrite app_ass.
simpl.
intros.
generalize (
NoDup_uniq H5 H3).
injection 1;
intros;
subst.
apply in_rev_elim.
rewrite H15.
eauto using in_or_app.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H4.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H13.
right.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H8).
revert H3.
replace (
l0 ++
b1 ::
l1 ++
b2 ::
l2)
with ((
l0 ++
b1 ::
l1) ++
b2 ::
l2).
rewrite <- (
rev_involutive (
Class.fields c)).
rewrite H9.
rewrite rev_app.
simpl.
rewrite app_ass.
simpl.
intros.
generalize (
NoDup_uniq H4 H3).
injection 1;
intros;
subst.
apply in_rev_elim.
rewrite H15.
eauto using in_or_app.
rewrite app_ass;
reflexivity.
unfold_ident.
simpl.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
).
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
injection e;
intros;
subst.
injection e0;
intros;
subst.
apply False_rect.
eauto using nodup.
injection e;
intros;
subst.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H11.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H9).
revert H3.
rewrite <- (
rev_involutive (
Class.fields c)).
rewrite H10.
rewrite rev_app.
simpl.
rewrite app_ass.
simpl.
intros.
generalize (
NoDup_uniq H5 H3).
injection 1;
intros;
subst.
apply in_rev_elim.
rewrite H15.
eauto using in_or_app.
sdestruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
p0),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec)
(
obj0,
ar0,
i0, (
h0,
p0),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H4.
forward.
unfold state_kind_inv in kind.
simpl in kind.
invall;
subst.
apply H13.
right.
unfold_ident_in_all.
replace x2 with c in *
by abstract congruence.
generalize (
Well_formed_hierarchy.fields_no_dup hierarchy_wf H8).
revert H3.
replace (
l0 ++
b1 ::
l1 ++
b2 ::
l2)
with ((
l0 ++
b1 ::
l1) ++
b2 ::
l2).
rewrite <- (
rev_involutive (
Class.fields c)).
rewrite H9.
rewrite rev_app.
simpl.
rewrite app_ass.
simpl.
intros.
generalize (
NoDup_uniq H4 H3).
injection 1;
intros;
subst.
apply in_rev_elim.
rewrite H15.
eauto using in_or_app.
rewrite app_ass;
reflexivity.
destruct hp'.
simpl.
intros.
sdestruct (
aux_constr_state_key_eq_dec (
obj',
ar',
i', (
t,
l0),
fs)
(
obj0,
ar0,
i, (
h,
p),
b1)
).
sdestruct (
aux_constr_state_key_eq_dec (
obj',
ar',
i', (
t,
l0),
fs)
(
obj0,
ar0,
i, (
h,
p),
b2)
).
injection e;
intros;
subst.
injection e0;
intros;
subst.
apply False_rect.
eauto using nodup.
injection e;
intros;
subst.
forward.
generalize (
stack _ (
or_introl _ (
refl_equal _))).
simpl.
intros;
invall;
subst.
eapply constructed_sibling_before_destructed.
eauto.
unfold_ident_in_all.
rewrite H11.
simpl;
omega.
sdestruct (
aux_constr_state_key_eq_dec (
obj',
ar',
i', (
t,
l0),
fs)
(
obj0,
ar0,
i, (
h,
p),
b2)
).
2 :
eauto.
injection e;
intros;
subst.
cut (
(
assoc (
aux_constr_state_key_eq_dec )
(
obj0,
ar0,
i, (
h,
p),
b1)
auxcs) =
Some Constructed
).
unfold_ident.
intro.
rewrite H3.
forward.
generalize (
stack _ (
or_introl _ (
refl_equal _))).
simpl.
intros;
invall;
subst.
eapply constructed_sibling_before_constructed.
eauto.
unfold_ident_in_all;
rewrite H10;
simpl;
omega.
unfold_ident_in_all;
rewrite H10;
simpl;
omega.
Qed.
End Preservation.