Home

# Module PreservationStackWf

Lemma goal : forall sf1 l1 l2, State.stack s2 = l1 ++ sf1 :: l2 -> forall sf2, In sf2 l2 -> ((
forall obj ar i hp, frame_pointer sf1 = Some (obj, ar, i, hp) -> ((
forall ar' i' hp', frame_pointer sf2 = Some (obj, ar', i', hp') -> relptr_gt (ar, i, hp) (ar', i', hp')
) /\
forall ar', frame_array sf2 = Some (obj, ar') -> exists l', ar = ar' ++ l'
)) /\
forall obj ar, frame_array sf1 = Some (obj, ar) -> forall ar', frame_array_weak sf2 = Some (obj, ar') -> exists l', ar = ar' ++ l' /\ l' <> nil
)
.
Proof.
inversion Hs1.
inversion step; subst; simpl in *; try trivial;
intros ? ? ? K;
try (exact (stack_wf _ _ _ (app_cons K _)));
destruct l1 as [ | ? l1']; simpl in K; injection K; intros until 2; subst; simpl; try exact (stack_wf _ _ _ (refl_equal _)); intros ? J; (split; [((intros; discriminate) || (injection 1; intros; subst; eauto; fail)) | (try (intros; discriminate); injection 1; intros; subst; eauto)]) || (try (split; [| ((intros; discriminate) || (injection 1; intros; subst; eauto; fail))])).

destruct (stack_wf _ nil _ (refl_equal _) _ J).
eauto.

refine (_ (stack_wf _ _ _ (app_cons _ _))).
2 : reflexivity.
intro.
destruct (x _ J).
tauto.

injection 1; intros; subst.
destruct (stack_wf _ nil _ (refl_equal _) _ J).
exact (H3 _ _ _ _ (refl_equal _)).

refine (_ (stack_wf _ _ _ (app_cons _ _))).
2 : reflexivity.
intro.
destruct (x _ J).
tauto.

injection 1; intros; subst.
destruct J.
subst.
simpl.
split.
intros; discriminate.
injection 1; intros; subst.
exists nil ; rewrite <- app_nil_end; trivial.
bintro.
generalize (stack_state_wf _ H5 b).
intros.
split.
intros.
generalize (frame_pointer_frame_array_weak H7).
intro.
destruct (H6 H8).
invall; subst.
eright.
reflexivity.
assumption.
intros.
generalize (frame_array_frame_array_weak H7).
intro.
destruct (H6 H8).
invall; eauto.

destruct l1'.
injection H4; intros; subst; simpl.
split.
intros; discriminate.
injection 1; intros; subst.
eauto.
simpl in H4.
injection H4; intros; subst t.
eauto.

injection 1; intros; subst.
assert (
relptr_gt
(ar0, i0,
(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)) (ar0, i0, (h, p))
).
unfold state_kind_inv in kind.
simpl in kind.
destruct beta; invall; subst.
eleft.
eassumption.
eleft with (lt := x1 :: nil) (lf := b :: nil).
reflexivity.
simpl. reflexivity.
simpl.
rewrite H8.
sdestruct (
In_dec super_eq_dec (Class.Inheritance.Repeated, b) (Class.super x2)
).
generalize (Well_formed_hierarchy.complete hierarchy_wf H8 i).
destruct (hier ! b); abstract congruence.
destruct n.
assert (In b (x3 ++ b :: bases)) by eauto using in_or_app.
revert H0.
rewrite <- H9.
intro.
generalize (let (_, h) := In_rev _ _ in h H0).
intros.
destruct (let (h, _) := in_map_iff _ _ _ in h H13).
destruct x.
destruct H15; subst.
generalize (let (h, _) := filter_In _ _ _ in h H16).
destruct 1.
destruct t.
assumption.
discriminate.
simpl.
rewrite H7.
destruct (peq x1 x1).
reflexivity.
destruct n; trivial.
discriminate.
assert (is_virtual_base_of hier b x1).
eapply vborder_list_virtual_base.
eassumption.
eassumption.
eapply In_rev.
rewrite rev_involutive.
eauto using in_or_app.
eleft.
reflexivity.
eright.
eassumption.
eleft with (lt := nil).
reflexivity.
reflexivity.
simpl.
generalize (Well_formed_hierarchy.is_virtual_base_of_defined_base hierarchy_wf H0).
destruct (hier ! b); abstract congruence.
simpl.
trivial.
discriminate.
destruct J.
subst; simpl.
split.
injection 1; intros; subst.
assumption.
destruct beta.
intros; discriminate.
injection 1; intros; subst.
exists nil.
apply app_nil_end.
destruct beta.
destruct (stack_state_wf _ H5).
split; auto.
intros; eauto using relptr_gt_trans.
generalize (stack_state_wf _ H5).
intros.
split.
intros.
destruct (H6 _ (frame_pointer_frame_array_weak H7)).
invall; subst.
eright.
reflexivity.
assumption.
intros.
destruct (H6 _ (frame_array_frame_array_weak H7)).
invall; eauto.

intros.
destruct l1'.
injection H; intros; subst; simpl.
destruct beta.
split; try (intros; discriminate).
injection 1; intros; subst.
eauto.
split.
injection 1; intros; subst.
split.
intros.
destruct (stack_state_wf _ J _ (frame_pointer_frame_array_weak H5)).
invall; subst.
eright.
reflexivity.
assumption.
intros.
destruct (stack_state_wf _ J _ (frame_array_frame_array_weak H5)).
invall; subst.
eauto.
injection 1; intros; subst; eauto.
simpl in H.
injection H; intros; subst t.
assert (In sf1 stk).
subst; eauto using in_or_app.
eauto.

Qed.

End Preservation.