Load PreservationHeader.
Lemma stack_objects_sorted :
sorted (
fun x y =>
Plt y x) (
stack_objects s2).
Proof.
Lemma unconstructed_scalar_fields :
forall obj, (
Globals.heap (
State.global s2)) !
obj =
None ->
forall fs ty,
FieldSignature.type fs =
FieldSignature.Scalar ty ->
forall ar i hp,
Globals.get_field (
Globals.field_values (
State.global s2)) (
obj,
ar,
i,
hp,
fs) =
None.
Proof.
inversion Hs1.
Opaque Globals.get_field Globals.put_field.
inversion step;
subst;
simpl in *;
eauto.
intros.
destruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs) (
obj0,
ar0,
i0,
hp0,
fs0)).
injection e;
intros;
subst.
inversion H0;
abstract congruence.
rewrite (
Globals.get_put_field_other H2 n);
eauto.
injection H1;
intros until 2;
subst;
simpl in *.
intro.
destruct (
peq (
Globals.next_object gl)
obj).
subst.
rewrite PTree.gss.
intro;
discriminate.
rewrite PTree.gso;
eauto.
intros.
destruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs) (
obj0,
ar0,
i0,
hp,
fs0)).
injection e;
intros;
subst.
unfold state_kind_inv in *;
simpl in *;
invall;
subst.
inversion H8;
abstract congruence.
rewrite (
Globals.get_put_field_other H3 n);
eauto.
intros.
destruct (
aux_constr_state_key_eq_dec (
obj,
ar,
i, (
h,
p),
fs) (
obj0,
ar0,
i0,
hp,
fs0)).
injection e;
intros;
subst.
unfold state_kind_inv in *;
simpl in *;
invall;
subst.
inversion H4;
abstract congruence.
eapply trans_equal with (
Globals.get_field (
Globals.field_values gl) (
obj0,
ar0,
i0,
hp,
fs0)).
Transparent Globals.get_field.
simpl.
destruct hp.
rewrite H1.
rewrite (
find_remove_field_other n).
reflexivity.
eauto.
Qed.
Lemma stack_or_deallocated :
forall obj, (
Globals.heap (
State.global s2)) !
obj <>
None ->
In obj (
stack_objects s2) \/
In obj (
State.deallocated_objects s2).
Proof.
inversion Hs1.
inversion step;
subst;
simpl in *;
eauto.
injection H1;
intros until 2;
subst;
simpl in *.
intro.
destruct (
peq obj (
Globals.next_object gl)).
auto.
rewrite PTree.gso;
eauto.
intros;
destruct (
stack_or_deallocated _ H2);
eauto.
intros.
unfold state_kind_inv in *;
simpl in *;
invall;
subst.
destruct (
stack_or_deallocated _ H);
eauto.
destruct H1;
eauto.
Qed.
Lemma deallocated_objects_destructed :
forall obj,
In obj (
State.deallocated_objects s2) ->
forall o, (
Globals.heap (
State.global s2)) !
obj =
Some o ->
forall i, 0 <=
i <
Object.arraysize o ->
assoc (@
pointer_eq_dec _) (
obj, (
nil,
i, (
Class.Inheritance.Repeated,
Object.class o ::
nil))) (
State.construction_states s2) =
Some Destructed.
Proof.
inversion Hs1.
inversion step;
subst;
simpl in *;
eauto.
revert H1.
unfold Globals.new.
injection 1;
intros until 2;
subst;
simpl in *.
intro.
destruct (
peq (
Globals.next_object gl)
obj ).
subst.
generalize (
Globals.valid_none valid_global (
Ple_refl _)).
intros until 2.
generalize (
deallocated_objects_exist _ H3).
intro;
contradiction.
rewrite PTree.gso;
eauto.
intros.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
injection e;
intros;
subst.
generalize (
deallocated_objects_destructed _ H2 _ H3 _ H4).
unfold state_kind_inv in kind;
simpl in *;
invall.
assert (
i0 <=
i0 <
n)
by abstract omega.
generalize (
H13 _ H4).
unfold_ident.
intros;
abstract congruence.
intros.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
injection e;
intros;
subst.
generalize (
deallocated_objects_destructed _ H _ H0 _ H1).
generalize (
stack _ (
or_introl _ (
refl_equal _)));
simpl.
unfold_ident ;
intro;
invall.
destruct H7;
abstract congruence.
intros.
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,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
apply False_rect.
destruct k2;
try discriminate.
unfold state_kind_inv in kind;
simpl in *;
invall.
destruct p.
discriminate.
destruct p0;
discriminate.
intros.
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,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
apply False_rect.
destruct k2;
try discriminate.
generalize (
stack _ (
or_introl _ (
refl_equal _)));
simpl;
intro;
invall.
destruct p.
discriminate.
destruct p;
discriminate.
intros.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
injection e;
intros;
subst.
generalize (
deallocated_objects_destructed _ H1 _ H2 _ H3).
unfold state_kind_inv in kind;
simpl in *;
invall;
subst.
unfold_ident_in_all;
intros;
abstract congruence.
intros.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
j, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
(
nil,
i, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
injection e;
intros;
subst.
apply False_rect.
generalize (
deallocated_objects_destructed _ H4 _ H5 _ H6).
unfold state_kind_inv in kind;
simpl in *;
invall;
subst.
assert (0 <=
i <=
i)
by abstract omega.
generalize (
H12 _ H6).
unfold_ident;
intros;
abstract congruence.
intros.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
injection e;
intros;
subst.
generalize (
deallocated_objects_destructed _ H2 _ H3 _ H4).
unfold state_kind_inv in kind;
simpl in *;
invall;
subst.
unfold_ident_in_all;
intros;
abstract congruence.
intros.
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,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
destruct beta;
try discriminate.
unfold state_kind_inv in kind;
simpl in *;
invall.
destruct p.
discriminate.
destruct p0;
discriminate.
intros.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i,
hp))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
intros.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0,
(
nil,
i0, (
Class.Inheritance.Repeated,
Object.class o ::
nil)))
);
eauto.
destruct 1;
eauto.
subst.
unfold state_kind_inv in kind;
simpl in *;
invall;
subst.
intros.
replace x0 with o in *
by abstract congruence.
apply H6.
abstract omega.
Qed.
Lemma deallocated_objects_not_in_stack :
forall obj,
In obj (
stack_objects s2) ->
In obj (
State.deallocated_objects s2) ->
False.
Proof.
inversion Hs1.
inversion step;
subst;
simpl in *;
eauto.
destruct 1;
eauto.
subst.
intro.
generalize (
deallocated_objects_exist _ H2).
injection H1;
intros;
subst;
simpl in *.
generalize (
Globals.valid_none valid_global (
Ple_refl _)).
assumption.
destruct 2;
eauto.
subst.
inversion stack_objects_no_dup;
subst.
unfold state_kind_inv in *;
simpl in *;
invall;
subst;
contradiction.
Qed.
Lemma deallocated_objects_exist :
forall obj,
In obj (
State.deallocated_objects s2) -> (
Globals.heap (
State.global s2)) !
obj <>
None.
Proof.
inversion Hs1.
inversion step;
subst;
simpl in *;
eauto.
intros.
revert H1.
unfold Globals.new.
injection 1;
intros;
subst;
simpl.
destruct (
peq (
Globals.next_object gl)
obj0 ).
subst;
rewrite PTree.gss;
abstract congruence.
rewrite PTree.gso;
eauto.
destruct 1;
eauto.
subst.
unfold state_kind_inv in *;
simpl in *;
invall;
abstract congruence.
Qed.
Lemma kind_object_in_construction :
forall obj,
kind_object (
State.kind s2) =
Some obj ->
exists l',
stack_objects s2 =
obj ::
l'.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try (intros; discriminate); injection 1; intros; subst; eauto; exact (stack_objects_in_construction nil _ _ (refl_equal _) _ _ (refl_equal _)).
Qed.
Lemma stack_objects_in_construction :
forall l1 sf l2
(
Hstack :
State.stack s2 =
l1 ++
sf ::
l2)
obj ar
(
Hframe :
frame_array_weak sf =
Some (
obj,
ar)),
exists l',
stackframe_objects l2 =
obj ::
l'.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; eauto;
intros until 1; try exact (stack_objects_in_construction _ _ _ (app_cons Hstack _)); destruct l1; injection Hstack; intros; eauto; subst; simpl in *; try (intros; discriminate); injection Hframe; intros; subst; eauto; try exact (stack_objects_in_construction nil _ _ (refl_equal _) _ _ (refl_equal _)); try exact (stack_objects_in_construction (_ :: _) _ _ (refl_equal _) _ _ Hframe).
destruct l1.
injection H4; intros; subst; injection Hframe; intros; subst; eauto.
injection H4; eauto.
destruct l1.
injection H; intros; subst; injection Hframe; intros; subst; eauto.
injection H; eauto.
Qed.
Lemma constructed_stack_objects_no_kind :
forall obj (
Hin :
In obj (
constructed_stack_objects s2)),
kind_object (
State.kind s2) =
Some obj ->
False.
Proof.
generalize (constructed_stack_objects_incl (s := s1)).
intro Hincl.
inversion Hs1.
intros until 1.
inversion step; subst; simpl in *; try (intros; discriminate); injection 1; intros; subst; eauto; try exact (constructed_stack_objects_no_stackframe _ Hin _ (or_introl _ (refl_equal _)) _ (refl_equal _)).
generalize (stack_objects_exist _ (Hincl _ Hin)).
intros.
destruct H3.
eapply Globals.valid_none.
assumption.
revert H1.
unfold Globals.new.
injection 1; intros; subst.
eapply Ple_refl.
inversion stack_objects_no_dup.
subst.
destruct H4.
apply in_or_app.
destruct (in_app_or _ _ _ Hin).
auto.
right.
eapply constructed_stackframe_objects_incl.
assumption.
Qed.
Lemma constructed_stack_objects_no_stackframe :
forall obj,
In obj (
constructed_stack_objects s2) ->
forall sf,
In sf (
State.stack s2) ->
forall ar,
frame_array_weak sf =
Some (
obj,
ar) ->
False.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; eauto.
destruct 2; eauto.
subst; simpl; intro; abstract congruence.
destruct 2; eauto.
subst; simpl; intro; abstract congruence.
destruct 2; eauto.
subst; simpl; intro; abstract congruence.
destruct 1; eauto.
subst; intros.
unfold state_kind_inv in *; simpl in *; invall; subst; simpl in *; invall; subst.
generalize (stack_state_wf _ (or_intror _ H) _ H0).
intros; invall.
destruct ar0; try discriminate.
destruct x0; try discriminate.
destruct H5; trivial.
destruct 2; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2; eauto.
subst; injection 1; intros; subst.
eauto.
destruct 2; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2.
subst; injection 1; intros; subst; eauto.
destruct H5; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2.
subst; injection 1; intros; subst; eauto.
destruct H0; eauto.
subst; injection 1; intros; subst; eauto.
destruct 2; eauto.
subst; simpl; intros; discriminate.
Qed.
Lemma constructed_stack_objects_correct :
forall obj,
In obj (
constructed_stack_objects s2) ->
forall o, (
Globals.heap (
State.global s2)) !
obj =
Some o ->
forall i, 0 <=
i <
Object.arraysize o ->
assoc (@
pointer_eq_dec _) (
obj, (
nil,
i, (
Class.Inheritance.Repeated,
Object.class o ::
nil))) (
State.construction_states s2) =
Some Constructed.
Proof.
generalize (constructed_stack_objects_incl (s := s1)).
intro Hincl.
generalize (fun x H => stack_objects_exist Hs1 (Hincl x H)).
intro Hex.
inversion Hs1.
inversion step; subst; simpl in *; try trivial.
revert H1.
unfold Globals.new.
injection 1; intros until 2; subst; simpl in *.
intro.
destruct (peq (Globals.next_object gl) obj ).
subst.
generalize (Globals.valid_none valid_global (Ple_refl _)).
intros until 2.
generalize (Hex _ H3).
intro; contradiction.
rewrite PTree.gso; eauto.
destruct 1; eauto.
subst.
unfold state_kind_inv in kind; simpl in *; invall; subst; simpl in *; invall; subst.
intros.
replace o with x in * by abstract congruence.
eauto.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
generalize (constructed_stack_objects_correct _ H2 _ H3 _ H4).
unfold state_kind_inv in kind; simpl in *; invall.
assert (i0 <= i0 < n) by abstract omega.
generalize (H13 _ H4).
unfold_ident.
intros; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
intros.
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,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
apply False_rect.
destruct k2; try discriminate.
unfold state_kind_inv in kind; simpl in *; invall.
destruct p.
discriminate.
destruct p0; discriminate.
intros.
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,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
generalize (constructed_stack_objects_correct _ H1 _ H2 _ H3).
unfold state_kind_inv in kind; simpl in *; invall; subst.
unfold_ident_in_all; intros; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
(obj0,
(nil, i, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
apply False_rect.
unfold state_kind_inv in kind; simpl in *; invall; subst.
destruct stk; try contradiction.
destruct t; try contradiction.
simpl in H8.
destruct c0; try contradiction.
invall; subst; simpl in *.
inversion stack_objects_no_dup.
subst.
destruct H18.
apply in_or_app.
destruct (in_app_or _ _ _ H4).
auto.
right.
eapply constructed_stackframe_objects_incl.
assumption.
simpl in H8.
destruct inhpath.
destruct k; try contradiction.
destruct kind; invall; subst.
destruct array; discriminate.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
generalize (constructed_stack_objects_correct _ H2 _ H3 _ H4).
unfold state_kind_inv in kind; simpl in *; invall; subst.
unfold_ident_in_all; intros; abstract congruence.
intros.
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,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
destruct beta; try discriminate.
unfold state_kind_inv in kind; simpl in *; invall.
destruct p.
discriminate.
destruct p0; discriminate.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, hp))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
generalize (constructed_stack_objects_correct _ H _ H0 _ H1).
unfold state_kind_inv in kind; simpl in *; invall; subst.
unfold_ident_in_all; intros; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
(obj0,
(nil, i0, (Class.Inheritance.Repeated, Object.class o :: nil)))
); eauto.
injection e; intros; subst.
generalize (constructed_stack_objects_correct _ H0 _ H1 _ H2).
unfold state_kind_inv in kind; simpl in *; invall.
unfold_ident_in_all; abstract congruence.
intros; eauto.
Qed.
Lemma construction_states_fields_none :
forall obj, (
Globals.heap (
State.global s2)) !
obj =
None ->
forall ar i hp fs,
assoc (
aux_constr_state_key_eq_dec ) (
obj,
ar,
i,
hp,
fs) (
State.field_construction_states s2) =
None.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try trivial.
revert H1.
unfold Globals.new.
injection 1; intros until 2; subst; simpl in *.
intro.
destruct (peq (Globals.next_object gl) obj ).
subst; rewrite PTree.gss; abstract congruence.
rewrite PTree.gso; eauto.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, hp, fs)
(obj0, ar0, i0, hp0, fs0)
); eauto.
destruct hp; unfold state_kind_inv in kind; simpl in *; invall.
inversion H3; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, hp, fs0)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H4; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, hp, fs0)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H7; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', (h, p), fs)
(obj0, ar0, i, hp, fs0)
); eauto.
destruct hp; generalize (stack _ (or_introl _ (refl_equal _))); simpl; intro; invall.
inversion H2; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, hp, fs0)
); eauto.
destruct hp; unfold state_kind_inv in kind; simpl in *; invall.
inversion H3; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, hp, fs0)
); eauto.
destruct hp; unfold state_kind_inv in kind; simpl in *; invall.
inversion H3; abstract congruence.
intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', hp', fs)
(obj0, ar0, i, hp, fs0)
); eauto.
destruct hp'; generalize (stack _ (or_introl _ (refl_equal _))); simpl; intro; invall.
inversion H2; abstract congruence.
Qed.
Lemma stack_objects_no_dup :
NoDup (
stack_objects s2).
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try trivial.
econstructor.
2 : assumption.
intro.
generalize (stack_objects_exist _ H2).
intros.
apply H3.
eapply Globals.valid_none.
assumption.
revert H1.
unfold Globals.new.
injection 1; intros; subst.
apply Ple_refl.
inversion stack_objects_no_dup ; assumption.
Qed.
Lemma stack_objects_exist :
forall obj,
In obj (
stack_objects s2) -> (
Globals.heap (
State.global s2)) !
obj <>
None.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try trivial.
revert H1.
unfold Globals.new.
injection 1; intros; subst; simpl in *.
destruct (peq (Globals.next_object gl) obj0 ).
subst; rewrite PTree.gss; abstract congruence.
destruct H4.
contradiction.
rewrite PTree.gso; eauto.
eauto.
Qed.
Lemma valid_global :
Globals.valid (
State.global s2).
Proof.
inversion Hs1.
inversion valid_global.
constructor.
inversion step; subst; unfold Globals.update in *; simpl in *; try abstract trivial.
eapply Globals.valid_new.
eassumption.
symmetry; eassumption.
Qed.
Lemma valid_object_classes :
forall obj o, (
Globals.heap (
State.global s2)) !
obj =
Some o ->
hier ! (
Object.class o) <>
None.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try abstract trivial.
intros ? ?.
generalize H1.
unfold Globals.new.
injection 1; intros until 2; subst; simpl.
destruct (peq (Globals.next_object gl) obj0).
subst.
rewrite PTree.gss.
injection 1; intros; subst; simpl.
assumption.
rewrite PTree.gso; eauto.
Qed.
Lemma object_arraysizes_nonnegative :
forall obj o, (
Globals.heap (
State.global s2)) !
obj =
Some o -> (0 <=
Object.arraysize o)%
Z.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; trivial.
intros ? ?.
generalize H1.
unfold Globals.new.
injection 1; intros until 2; subst; simpl.
destruct (peq (Globals.next_object gl) obj0).
subst.
rewrite PTree.gss.
injection 1; intros; subst; simpl.
abstract omega.
rewrite PTree.gso; eauto.
Qed.
Lemma stack_state :
forall sf l,
State.stack s2 =
sf ::
l ->
frame_requires_code sf ->
is_code_state (
State.kind s2).
Proof.
inversion Hs1.
inversion step; subst; simpl in *; trivial;
try (injection 1; intros; subst; simpl in *; tauto);
try (intros; subst; refine (_ (stack2 _ nil _ (refl_equal _))); unfold stack2_inv; simpl; tauto).
Qed.
Lemma construction_states_none :
forall obj, (
Globals.heap (
State.global s2)) !
obj =
None ->
forall rptr,
assoc (@
pointer_eq_dec _) (
obj,
rptr) (
State.construction_states s2) =
None.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try trivial.
revert H1.
unfold Globals.new.
injection 1; intros until 2; subst; simpl in *.
intro.
destruct (peq (Globals.next_object gl) obj ).
subst; rewrite PTree.gss; abstract congruence.
rewrite PTree.gso; eauto.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
(obj0, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall; congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
(obj0, rptr)
); eauto.
generalize (stack _ (or_introl _ (refl_equal _))).
simpl; intro; invall; abstract congruence.
intros.
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, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H5; abstract congruence.
intros.
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, rptr)
); eauto.
generalize (stack _ (or_introl _ (refl_equal _))).
simpl; intro; invall.
inversion H2; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p))) (obj0, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H4; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A)
(obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
(obj0, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p))) (obj0, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H5; abstract congruence.
intros.
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, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H6; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, hp)) (obj0, rptr)
); eauto.
destruct hp; unfold state_kind_inv in kind; simpl in *; invall.
inversion H2; abstract congruence.
intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p))) (obj0, rptr)
); eauto.
unfold state_kind_inv in kind; simpl in *; invall.
inversion H3; abstract congruence.
Qed.
End Preservation.