Library JMLRac_2_Correct
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Correctness Proof of RAC1 <-> RAC2
Sem: st_rac1 ----- Exec p ------> st'_rac1 | | | Corr | Corr | | RAC1: st_rac2 ----- Exec p ------> st'_rac2
Require Export JMLRac2.
Require Export JMLOpSem.
Require Import List.
Require Import MinMax.
Import Dom.
Import Prog.
Import Sem.Notations.
Import Rac1.Notations.
Import Rac2.Notations.
Import Stack.
Module OpRac1 := OperationalSemantics Rac1.
Module OpRac2 := OperationalSemantics Rac2.
Import Rac2.
Import Assignables.
Open Scope rac2_scope.
Theorem rac2_length_assignables_correct:
forall p,
(forall e st st' s,
OpRac2.ExpressionStep p e st st' s ->
(length st@fr@assignables) = (length st'@fr@assignables))
/\
(forall l st st' s,
OpRac2.ListSteps p l st st' s ->
(length st@fr@assignables) = (length st'@fr@assignables))
/\
(forall m b st st' s,
OpRac2.StatementStep p m b st st' s ->
(length st@fr@assignables) = (length st'@fr@assignables))
/\
(forall m b st st' s,
OpRac2.BlockStep p m b st st' s ->
(length st@fr@assignables) = (length st'@fr@assignables)).
Proof.
intro p.
apply OpRac2.mutual_ind; intros; simpl in *; subst; trivial.
simpl.
unfold Assignables.FieldUpdateAction.
case isPivot.
simpl.
rewrite map_length.
rewrite H2.
assumption.
rewrite H2.
assumption.
simpl.
rewrite H1.
rewrite H6.
simpl in H15.
apply eq_add_S.
rewrite H15.
unfold pop.
destruct st_c' @fr @assignables.
discriminate H15.
trivial.
rewrite H1.
assumption.
rewrite H1.
assumption.
Qed.
Theorem rac2_equiv_assignables_correct:
forall p,
(forall e st st' s,
OpRac2.ExpressionStep p e st st' s ->
EquivAssignables p st st')
/\
(forall l st st' s,
OpRac2.ListSteps p l st st' s ->
EquivAssignables p st st')
/\
(forall m b st st' s,
OpRac2.StatementStep p m b st st' s ->
EquivAssignables p st st')
/\
(forall m b st st' s,
OpRac2.BlockStep p m b st st' s ->
EquivAssignables p st st').
Proof.
generalize rac2_length_assignables_correct.
intros.
specialize H with p.
destruct H.
destruct H0.
destruct H1.
apply OpRac2.mutual_ind; intros; simpl in *.
apply EquivAssignables_trans with st1; trivial.
apply EquivAssignables_trans with st2; trivial.
rewrite H14.
apply FieldUpdateAction_Equiv; auto.
rewrite H14.
rewrite <- H13.
simpl.
unfold FieldUpdateAction.
case isPivot.
simpl.
rewrite map_length.
apply le_min_r.
apply le_min_r.
apply H in H5.
rewrite H5.
apply le_min_l.
apply EquivAssignables_trans with st1; trivial.
apply EquivAssignables_trans with st2; trivial.
assert (EquivAssignables p st2 st_c).
unfold NewFrame in H13.
unfold MethodCallAction in H15.
unfold EquivAssignables.
rewrite H13 in H14.
rewrite H14 in H15.
simpl in H15.
rewrite <- H15.
simpl.
unfold level.
simpl.
rewrite nat_compare_n_Sn.
rewrite truncate_same.
apply EquivAssignables_ind_refl.
apply EquivAssignables_trans with st_c'; trivial.
apply EquivAssignables_trans with st_c; trivial.
apply H2 in H18.
rewrite H18.
apply le_min_r.
rewrite <- H21.
apply MethodReturnAction_Equiv with st2; auto.
rewrite <- H21.
unfold MethodReturnAction.
simpl.
unfold pop.
case st_c' @fr @assignables.
auto with *.
intros.
simpl.
auto with *.
apply H0 in H9.
rewrite H9.
apply le_min_l.
apply H in H4.
rewrite H4.
apply le_min_l.
apply EquivAssignables_trans with (st' := st1); trivial.
apply NewObjectAction_Equiv with o; auto.
rewrite H6.
apply EquivAssignables_3 with (Heap.ObjectObject cn um) o.
replace st1 @h with st @h ; trivial.
rewrite <- H5.
trivial.
rewrite H6.
simpl.
apply le_min_r.
rewrite H3.
apply EquivAssignables_refl.
apply EquivAssignables_trans with st1; trivial.
apply H0 in H6.
rewrite H6.
apply le_min_r.
trivial.
apply EquivAssignables_trans with st1; trivial.
apply EquivAssignables_trans with st1 [fr := fr2]; trivial.
unfold EquivAssignables.
rewrite H6.
simpl.
unfold level.
rewrite nat_compare_n_n.
apply EquivAssignables_ind_refl.
rewrite H6.
simpl.
apply le_min_l.
apply H1 in H4.
rewrite H4.
apply le_min_l.
trivial.
Qed.
Theorem rac2_rac1_correct:
forall p,
(forall e st_rac2 st'_rac2 r,
OpRac2.ExpressionStep p e st_rac2 st'_rac2 r ->
forall st_rac1,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac1,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac1.ExpressionStep p e st_rac1 st'_rac1 r)
/\
(forall l st_rac2 st'_rac2 r,
OpRac2.ListSteps p l st_rac2 st'_rac2 r ->
forall st_rac1,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac1,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac1.ListSteps p l st_rac1 st'_rac1 r)
/\
(forall m b st_rac2 st'_rac2 r,
OpRac2.StatementStep p m b st_rac2 st'_rac2 r ->
forall st_rac1,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac1,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac1.StatementStep p m b st_rac1 st'_rac1 r)
/\
(forall m b st_rac2 st'_rac2 r,
OpRac2.BlockStep p m b st_rac2 st'_rac2 r ->
forall st_rac1,
CorrespondingState p st_rac1 st_rac2->
exists st'_rac1,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac1.BlockStep p m b st_rac1 st'_rac1 r).
Proof.
intro p.
apply OpRac2.mutual_ind; intros; simpl in *.
apply H2 in H11.
destruct H11 as[st1_rac1 H11].
destruct H11.
destruct H5 with st1_rac1 as [st2_rac1 H13];trivial.
destruct H13.
set (st'_rac1 := Rac1.Assignables.FieldUpdateAction p loc v st2_rac1).
exists ((st'_rac1[h := Heap.update st2_rac1@h loc v])%rac1).
split.
rewrite H10.
apply FieldUpdateAction_Correct;trivial.
inversion H13.
apply
(OpRac1.assignment_instance_field_ok p e v obj fsig expr target st_rac1
st1_rac1 st2_rac1 st2_rac1[h := Heap.update st2_rac1@h loc v]%rac1
st2_rac1 loc cn um); trivial.
apply
(FieldUpdateCheck_Correct loc p st1_rac1 st1);
trivial.
rewrite H23;trivial.
rewrite H23;trivial.
destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial.
destruct Htmp.
clear H1.
destruct H6 with st1_rac1 as (st2_rac1, Htmp); trivial.
destruct Htmp.
clear H6.
set (fr_c1_rac1 := Rac1.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac1)
in |- *.
set (st3_rac1 := st2_rac1[fr := fr_c1_rac1]%rac1) in |- *.
set (st_c_rac1 := Rac1.Assignables.MethodCallAction p c' m' st3_rac1) in |- *.
destruct H15 with st_c_rac1 as (st_c'_rac1, Htmp).
assert (CorrespondingState p st3_rac1 st3).
unfold st3_rac1 in |- *.
rewrite H10 in |- *.
apply
NewFrame_Correct
with
(m := m')
(param := lv2params m' (Ref this0 :: psv))
(st_rac1 := st2_rac1)
(st_rac2 := st2); trivial.
unfold st_c_rac1 in |- *.
rewrite <- H11.
apply
MethodCallAction_Correct
with (c := c') (m := m') (st_rac1 := st3_rac1) (st_rac2 := st3);
trivial.
destruct Htmp.
set
(st'_rac1 :=
Rac1.Assignables.MethodReturnAction p st_c'_rac1 st2_rac1)
in |- *.
exists st'_rac1.
split.
unfold st'_rac1 in |- *.
rewrite <- H17 in |- *.
generalize rac2_length_assignables_correct.
intros.
specialize H23 with p.
destruct H23.
destruct H24.
destruct H25.
apply
MethodReturnAction_Correct
with
st2_rac1 st_c'_rac1
st2 st_c'; trivial.
assert (EquivAssignables p st2 st_c).
unfold NewFrame in H9.
unfold MethodCallAction in H11.
unfold EquivAssignables.
rewrite H9 in H10.
rewrite H10 in H11.
simpl in H11.
rewrite <- H11.
simpl.
unfold level.
simpl.
rewrite nat_compare_n_Sn.
rewrite truncate_same.
apply EquivAssignables_ind_refl.
apply EquivAssignables_trans with st_c; trivial.
generalize rac2_equiv_assignables_correct.
intros.
specialize H28 with p.
destruct H28.
destruct H29.
destruct H30.
apply H31 in H14.
trivial.
apply H26 in H14.
rewrite H14.
apply le_min_r.
apply H26 in H14.
rewrite <- H14.
rewrite <- H11.
rewrite H10.
rewrite H9.
simpl.
trivial.
apply
(OpRac1.method_vcall_ok p e st_rac1 st1_rac1 st2_rac1 st3_rac1 st_c_rac1
st_c'_rac1 st'_rac1 fr_c1_rac1 msig o cn um this0 ps
psnv psv v cn' m' c' b body); trivial.
destruct H19.
rewrite H30;trivial.
destruct H6.
rewrite H25.
trivial.
set (st1_rac1 := Rac1.Assignables.NewObjectAction p o st_rac1) in |- *.
exists st1_rac1[h := h']%rac1.
split.
rewrite H2 in |- *.
assert (CorrespondingState p st1_rac1 st1).
unfold st1_rac1 in |- *.
rewrite <- H1 in |- *.
apply NewObjectAction_Correct with o st_rac1 st; trivial.
destruct H4.
split;simpl;trivial.
destruct H11.
split.
trivial.
intros.
generalize UnfoldDatagroups_rac_intersect_new.
intros.
specialize H11 with p st_rac2@h (Heap.ObjectObject cn um) st_rac2@fr o h' O.
replace st@h with st_rac2@h in H0.
apply H11 with n in H0.
generalize H0.
specialize e1 with n.
generalize e1.
apply LocSet.eq_trans.
rewrite <- H1.
simpl.
trivial.
apply
OpRac1.new_object_ok
with (st1 := st1_rac1) (h' := h') (cn := cn) (um := um);
trivial.
destruct H3.
rewrite H11; trivial.
exists st_rac1.
rewrite <- H in |- *.
split; trivial.
apply OpRac1.ListSteps_nil; trivial.
destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial.
destruct Htmp.
destruct H3 with st1_rac1 as (st'_rac1, Htmp); trivial.
destruct Htmp.
exists st'_rac1.
split; trivial.
apply OpRac1.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac1);
trivial.
destruct H1 with st_rac1 as (st'_rac1, Htmp); trivial.
destruct Htmp.
exists st'_rac1.
split; trivial.
apply OpRac1.expr_stmt_ok with (v := v) (e := e); trivial.
destruct H2.
destruct H5.
rewrite H6 in |- *; trivial.
destruct H1 with st_rac1 as (st1_rac1, Htmp); trivial.
destruct Htmp.
set (fr2_rac1 := Rac1.State.Frame.set_pc st1_rac1@fr%rac1 pc') in |- *.
destruct H4 with st1_rac1[fr := fr2_rac1]%rac1 as (st'_rac1, Htmp); trivial.
destruct H6.
rewrite H2 in |- *.
unfold fr2_rac1 in |- *.
split; trivial.
destruct Htmp.
exists st'_rac1.
split; trivial.
apply
OpRac1.BlockStep_ok_next
with (pc' := pc') (st1 := st1_rac1) (fr2 := fr2_rac1);
trivial.
destruct H5.
rewrite H11 in |- *.
trivial.
destruct H1 with st_rac1 as (st'_rac1, Htmp); trivial.
destruct Htmp.
exists st'_rac1.
split; trivial.
apply OpRac1.BlockStep_ok_last; trivial.
destruct H2.
rewrite H6 in |- *; trivial.
Qed.
Theorem rac1_rac2_correct:
forall p,
(forall e st_rac1 st'_rac1 r,
OpRac1.ExpressionStep p e st_rac1 st'_rac1 r ->
forall st_rac2,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac2,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac2.ExpressionStep p e st_rac2 st'_rac2 r)
/\
(forall l st_rac1 st'_rac1 r,
OpRac1.ListSteps p l st_rac1 st'_rac1 r ->
forall st_rac2,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac2,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac2.ListSteps p l st_rac2 st'_rac2 r)
/\
(forall m b st_rac1 st'_rac1 r,
OpRac1.StatementStep p m b st_rac1 st'_rac1 r ->
forall st_rac2,
CorrespondingState p st_rac1 st_rac2 ->
exists st'_rac2,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac2.StatementStep p m b st_rac2 st'_rac2 r)
/\
(forall m b st_rac1 st'_rac1 r,
OpRac1.BlockStep p m b st_rac1 st'_rac1 r ->
forall st_rac2,
CorrespondingState p st_rac1 st_rac2->
exists st'_rac2,
CorrespondingState p st'_rac1 st'_rac2 /\
OpRac2.BlockStep p m b st_rac2 st'_rac2 r).
Proof.
intro p.
apply OpRac1.mutual_ind; intros; simpl in *.
apply H2 in H11.
destruct H11 as[st1_rac2 H11].
destruct H11.
destruct H5 with st1_rac2 as [st2_rac2 H13];trivial.
destruct H13.
set (st'_rac2 := FieldUpdateAction p loc v st2_rac2).
exists ((st'_rac2[h := Heap.update st2_rac2@h loc v])).
split.
rewrite H10.
apply FieldUpdateAction_Correct;trivial.
inversion H13.
apply
(OpRac2.assignment_instance_field_ok p e v obj fsig expr target st_rac2
st1_rac2 st2_rac2 st'_rac2[h := Heap.update st2_rac2@h loc v]
st'_rac2 loc cn um); trivial.
apply
(FieldUpdateCheck_Correct loc p st1 st1_rac2);
trivial.
rewrite <- H23;trivial.
rewrite <- H23;trivial.
destruct H1 with st_rac2 as (st1_rac2, Htmp); trivial.
destruct Htmp.
clear H1.
destruct H6 with st1_rac2 as (st2_rac2, Htmp); trivial.
destruct Htmp.
clear H6.
set (fr_c1_rac2 := NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac2)
in |- *.
set (st3_rac2 := st2_rac2[fr := fr_c1_rac2]) in |- *.
set (st_c_rac2 := MethodCallAction p c' m' st3_rac2) in |- *.
destruct H15 with st_c_rac2 as (st_c'_rac2, Htmp).
assert (CorrespondingState p st3 st3_rac2).
unfold st3_rac2 in |- *.
rewrite H10 in |- *.
apply
NewFrame_Correct
with
(m := m')
(param := lv2params m' (Ref this0 :: psv))
(st_rac1 := st2)
(st_rac2 := st2_rac2); trivial.
unfold st_c_rac2 in |- *.
rewrite <- H11.
apply
MethodCallAction_Correct
with (c := c') (m := m') (st_rac1 := st3) (st_rac2 := st3_rac2);
trivial.
destruct Htmp.
set
(st'_rac2 :=
MethodReturnAction p st_c'_rac2 st2_rac2)
in |- *.
exists st'_rac2.
split.
unfold st'_rac2 in |- *.
rewrite <- H17 in |- *.
generalize rac2_length_assignables_correct.
intros.
specialize H23 with p.
destruct H23.
destruct H24.
destruct H25.
apply
MethodReturnAction_Correct
with
st2 st_c'
st2_rac2 st_c'_rac2; trivial.
assert (EquivAssignables p st2_rac2 st_c_rac2).
unfold fr_c1_rac2 in st3_rac2.
unfold st3_rac2 in st_c_rac2.
unfold st_c_rac2.
unfold EquivAssignables.
unfold MethodCallAction.
unfold NewFrame.
simpl.
unfold level.
simpl.
rewrite nat_compare_n_Sn.
rewrite truncate_same.
apply EquivAssignables_ind_refl.
apply EquivAssignables_trans with st_c_rac2; trivial.
generalize rac2_equiv_assignables_correct.
intros.
specialize H28 with p.
destruct H28.
destruct H29.
destruct H30.
apply H31 in H22.
trivial.
apply H26 in H22.
rewrite H22.
apply le_min_r.
apply H26 in H22.
rewrite <- H22.
unfold st_c_rac2.
unfold st3_rac2.
simpl.
trivial.
apply
(OpRac2.method_vcall_ok p e st_rac2 st1_rac2 st2_rac2 st3_rac2 st_c_rac2
st_c'_rac2 st'_rac2 fr_c1_rac2 msig o cn um this0 ps
psnv psv v cn' m' c' b body); trivial.
destruct H19.
rewrite <- H30;trivial.
destruct H6.
rewrite <- H25.
trivial.
set (st1_rac2 := NewObjectAction p o st_rac2) in |- *.
exists st1_rac2[h := h'].
split.
assert (CorrespondingState p st1 st1_rac2).
unfold st1_rac2 in |- *.
rewrite <- H1 in |- *.
apply NewObjectAction_Correct with o st st_rac2; trivial.
rewrite H2.
destruct H4.
split;simpl;trivial.
destruct H11.
split;trivial.
intros.
generalize UnfoldDatagroups_rac_intersect_new.
intros.
specialize H11 with p st_rac0@h (Heap.ObjectObject cn um) st_rac0@fr o h' O.
replace st@h%rac1 with st_rac1@h%rac1 in H0.
rewrite H12 in H0.
apply H11 with n in H0.
generalize H0.
specialize e1 with n.
generalize e1.
apply LocSet.eq_trans.
rewrite <- H1.
simpl.
trivial.
apply
OpRac2.new_object_ok
with (st1 := st1_rac2) (h' := h') (cn := cn) (um := um);
trivial.
destruct H3.
rewrite <- H11; trivial.
exists st_rac2.
rewrite <- H in |- *.
split; trivial.
apply OpRac2.ListSteps_nil; trivial.
destruct H1 with st_rac2 as (st1_rac2, Htmp); trivial.
destruct Htmp.
destruct H3 with st1_rac2 as (st'_rac2, Htmp); trivial.
destruct Htmp.
exists st'_rac2.
split; trivial.
apply OpRac2.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac2);
trivial.
destruct H1 with st_rac2 as (st'_rac2, Htmp); trivial.
destruct Htmp.
exists st'_rac2.
split; trivial.
apply OpRac2.expr_stmt_ok with (v := v) (e := e); trivial.
destruct H2.
destruct H5.
rewrite <- H6 in |- *; trivial.
destruct H1 with st_rac2 as (st1_rac2, Htmp); trivial.
destruct Htmp.
set (fr2_rac2 := Frame.set_pc st1_rac2@fr pc') in |- *.
destruct H4 with st1_rac2[fr := fr2_rac2] as (st'_rac2, Htmp); trivial.
destruct H6.
rewrite H2 in |- *.
unfold fr2_rac2 in |- *.
split; trivial.
destruct Htmp.
exists st'_rac2.
split; trivial.
apply
OpRac2.BlockStep_ok_next
with (pc' := pc') (st1 := st1_rac2) (fr2 := fr2_rac2);
trivial.
destruct H5.
rewrite <- H11 in |- *.
trivial.
destruct H1 with st_rac2 as (st'_rac2, Htmp); trivial.
destruct Htmp.
exists st'_rac2.
split; trivial.
apply OpRac2.BlockStep_ok_last; trivial.
destruct H2.
rewrite <- H6 in |- *; trivial.
Qed.