Library JMLRac_3_Correct

Correctness Proof of RAC2 <-> RAC3


 

Sem:  st_rac2 ----- Exec p ------> st'_rac2
        |                           |
        | Corr                      | Corr
        |                           |
RAC1: st_rac3 ----- Exec p ------> st'_rac3


 

Require Export JMLRac3.
Require Export JMLOpSem.

Import Dom.
Import Prog.
Import Sem.Notations.
Import Rac1.Notations.
Import Rac2.Notations.
Import Rac3.Notations.

Module OpRac2 := OperationalSemantics Rac2.
Module OpRac3 := OperationalSemantics Rac3.

Import Rac3.
Import Assignables.

Open Scope rac3_scope.

Theorem rac3_rac2_correct:
forall p,
  (forall e st_rac3 st'_rac3 r,
  OpRac3.ExpressionStep p e st_rac3 st'_rac3 r ->
  forall st_rac2,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac2,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac2.ExpressionStep p e st_rac2 st'_rac2 r)
/\
  (forall l st_rac3 st'_rac3 r,
  OpRac3.ListSteps p l st_rac3 st'_rac3 r ->
  forall st_rac2,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac2,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac2.ListSteps p l st_rac2 st'_rac2 r)
/\
  (forall m b st_rac3 st'_rac3 r,
  OpRac3.StatementStep p m b st_rac3 st'_rac3 r ->
  forall st_rac2,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac2,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac2.StatementStep p m b st_rac2 st'_rac2 r)
/\
  (forall m b st_rac3 st'_rac3 r,
  OpRac3.BlockStep p m b st_rac3 st'_rac3 r ->
  forall st_rac2,
  CorrespondingState p st_rac2 st_rac3->
  exists st'_rac2,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac2.BlockStep p m b st_rac2 st'_rac2 r).
Proof.

intro p.
apply OpRac3.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 (st3_rac2 := Rac2.Assignables.FieldUpdateAction p loc v st2_rac2).
exists ((st3_rac2[h := Heap.update st2_rac2@h loc v])%rac2).
split.
rewrite H10.
apply FieldUpdateAction_Correct with cn um obj fsig;trivial.
inversion H13.
  apply
   (OpRac2.assignment_instance_field_ok p e v obj fsig expr target st_rac2
      st1_rac2 st2_rac2 st3_rac2[h := Heap.update st2_rac2@h loc v]%rac2
      st3_rac2 loc cn um); trivial.

   apply
    (FieldUpdateCheck_Correct loc p st1_rac2 st1);
    trivial.

rewrite H16;trivial.

rewrite H16;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 := Rac2.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac2)
  in |- *.
 set (st3_rac2 := st2_rac2[fr := fr_c1_rac2]%rac2) in |- *.
 set (st_c_rac2 := Rac2.Assignables.MethodCallAction p c' m' st3_rac2) in |- *.
 destruct H15 with st_c_rac2 as (st_c'_rac2, Htmp).
  assert (CorrespondingState p st3_rac2 st3).

   unfold st3_rac2 in |- *.
   rewrite H10 in |- *.

   apply
    NewFrame_Correct
     with
       (m := m')
       (param := lv2params m' (Ref this0 :: psv))
       (st_rac2 := st2_rac2)
       (st_rac3 := st2); trivial.

   unfold st_c_rac2 in |- *.
   rewrite <- H11.
    apply
     MethodCallAction_Correct
      with (c := c') (m := m') (st_rac2 := st3_rac2) (st_rac3 := st3);
     trivial.

  destruct Htmp.

  set
   (st'_rac2 :=
    Rac2.Assignables.MethodReturnAction p st_c'_rac2 st2_rac2)
   in |- *.
  exists st'_rac2.
  split.
   unfold st'_rac2 in |- *.
   rewrite <- H17 in |- *.

    apply
     MethodReturnAction_Correct
      with
        st2_rac2 st_c'_rac2
        st2 st_c'; 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.
    inversion H19.
    rewrite H24;trivial.

    inversion H6.
    inversion H23.
    rewrite H31.
    trivial.


 set (st1_rac2 := Rac2.Assignables.NewObjectAction p o st_rac2) in |- *.
 exists st1_rac2[h := h']%rac2.
 split.
  rewrite H2 in |- *.
  assert (CorrespondingState p st1_rac2 st1).
   unfold st1_rac2 in |- *.
   rewrite <- H1 in |- *.
   apply NewObjectAction_Correct with o st_rac2 st; trivial.
   replace st@h with st1@h in H0.

   destruct H4.
   split;simpl;trivial.

  rewrite <- CorrectBacklinks_new with cn um o;trivial.

  destruct H1.
  unfold NewObjectAction.
  simpl.
  trivial.

  apply
   OpRac2.new_object_ok
    with (st1 := st1_rac2) (h' := h') (cn := cn) (um := um);
   trivial.
  destruct H3.
  rewrite H4; 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 H2.
 rewrite H8 in |- *; trivial.


 destruct H1 with st_rac2 as (st1_rac2, Htmp); trivial.
 destruct Htmp.
 set (fr2_rac2 := Rac2.State.Frame.set_pc st1_rac2@fr%rac2 pc') in |- *.
 destruct H4 with st1_rac2[fr := fr2_rac2]%rac2 as (st'_rac2, Htmp); trivial.
  destruct H6.
  rewrite H2 in |- *.
  unfold fr2_rac2 in |- *.
  split; trivial.

  inversion H6.
  split;simpl;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.
  destruct H5.
  rewrite H13 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.
 destruct H2.
 rewrite H8 in |- *; trivial.
Qed.

Open Scope rac2_scope.

Theorem rac2_rac3_correct:
forall p,
  (forall e st_rac2 st'_rac2 r,
  OpRac2.ExpressionStep p e st_rac2 st'_rac2 r ->
  forall st_rac3,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac3,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac3.ExpressionStep p e st_rac3 st'_rac3 r)
/\
  (forall l st_rac2 st'_rac2 r,
  OpRac2.ListSteps p l st_rac2 st'_rac2 r ->
  forall st_rac3,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac3,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac3.ListSteps p l st_rac3 st'_rac3 r)
/\
  (forall m b st_rac2 st'_rac2 r,
  OpRac2.StatementStep p m b st_rac2 st'_rac2 r ->
  forall st_rac3,
  CorrespondingState p st_rac2 st_rac3 ->
  exists st'_rac3,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac3.StatementStep p m b st_rac3 st'_rac3 r)
/\
  (forall m b st_rac2 st'_rac2 r,
  OpRac2.BlockStep p m b st_rac2 st'_rac2 r ->
  forall st_rac3,
  CorrespondingState p st_rac2 st_rac3->
  exists st'_rac3,
  CorrespondingState p st'_rac2 st'_rac3 /\
  OpRac3.BlockStep p m b st_rac3 st'_rac3 r).
Proof.
intro p.
apply OpRac2.mutual_ind; intros; simpl in *.


apply H2 in H11.
destruct H11 as[st1_rac3 H11].
destruct H11.
destruct H5 with st1_rac3 as [st2_rac3 H13];trivial.
destruct H13.
set (st3_rac3 := Rac3.Assignables.FieldUpdateAction p loc v st2_rac3).
exists ((st3_rac3[h := Heap.update st2_rac3@h loc v])%rac3).
split.
rewrite H10.
destruct H13.
apply FieldUpdateAction_Correct with cn um obj fsig;trivial.
rewrite <- H15;trivial.
rewrite <- H15;trivial.
split;trivial.
inversion H13.
  apply
   (OpRac3.assignment_instance_field_ok p e v obj fsig expr target st_rac3
      st1_rac3 st2_rac3 st3_rac3[h := Heap.update st2_rac3@h loc v]%rac3
      st3_rac3 loc cn um); trivial.

   apply
    (FieldUpdateCheck_Correct loc p st1 st1_rac3);
    trivial.

rewrite <- H16;trivial.

rewrite <- H16;trivial.



 destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial.
 destruct Htmp.
 clear H1.
 destruct H6 with st1_rac3 as (st2_rac3, Htmp); trivial.
 destruct Htmp.
 clear H6.
 set (fr_c1_rac3 := Rac3.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac3)
  in |- *.
 set (st3_rac3 := st2_rac3[fr := fr_c1_rac3]%rac3) in |- *.
 set (st_c_rac3 := Rac3.Assignables.MethodCallAction p c' m' st3_rac3) in |- *.
 destruct H15 with st_c_rac3 as (st_c'_rac3, Htmp).
  assert (CorrespondingState p st3 st3_rac3).

   unfold st3_rac3 in |- *.
   rewrite H10 in |- *.

   apply
    NewFrame_Correct
     with
       (m := m')
       (param := lv2params m' (Ref this0 :: psv))
       (st_rac2 := st2)
       (st_rac3 := st2_rac3); trivial.

   unfold st_c_rac3 in |- *.
   rewrite <- H11.
    apply
     MethodCallAction_Correct
      with (c := c') (m := m') (st_rac2 := st3) (st_rac3 := st3_rac3);
     trivial.

  destruct Htmp.

  set
   (st'_rac3 :=
    Rac3.Assignables.MethodReturnAction p st_c'_rac3 st2_rac3)
   in |- *.
  exists st'_rac3.
  split.
   unfold st'_rac3 in |- *.
   rewrite <- H17 in |- *.

    apply
     MethodReturnAction_Correct
      with
        st2 st_c'
        st2_rac3 st_c'_rac3; trivial.

   apply
     (OpRac3.method_vcall_ok p e st_rac3 st1_rac3 st2_rac3 st3_rac3 st_c_rac3
       st_c'_rac3 st'_rac3 fr_c1_rac3 msig o cn um this0 ps
       psnv psv v cn' m' c' b body); trivial.
    inversion H19.
    rewrite <- H24;trivial.

    inversion H6.
    inversion H23.
    rewrite <- H31.
    trivial.


 set (st1_rac3 := Rac3.Assignables.NewObjectAction p o st_rac3) in |- *.
 exists st1_rac3[h := h']%rac3.
 split.
  rewrite H2 in |- *.
  assert (CorrespondingState p st1 st1_rac3).
   unfold st1_rac3 in |- *.
   rewrite <- H1 in |- *.
   apply NewObjectAction_Correct with o st st_rac3; trivial.
   replace st@h with st1@h in H0.

   destruct H4.
   split;simpl;trivial.

  rewrite <- CorrectBacklinks_new with cn um o;trivial.
  rewrite <- H5;trivial.

  destruct H1.
  unfold Rac2.Assignables.NewObjectAction.
  simpl.
  trivial.

  apply
   OpRac3.new_object_ok
    with (st1 := st1_rac3) (h' := h') (cn := cn) (um := um);
   trivial.
  destruct H3.
  rewrite <- H4; trivial.


 exists st_rac3.
 rewrite <- H in |- *.
 split; trivial.
 apply OpRac3.ListSteps_nil; trivial.


 destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial.
 destruct Htmp.
 destruct H3 with st1_rac3 as (st'_rac3, Htmp); trivial.
 destruct Htmp.
 exists st'_rac3.
 split; trivial.
 apply OpRac3.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac3);
  trivial.


 destruct H1 with st_rac3 as (st'_rac3, Htmp); trivial.
 destruct Htmp.
 exists st'_rac3.
 split; trivial.
 apply OpRac3.expr_stmt_ok with (v := v) (e := e); trivial.
 destruct H2.
 destruct H2.
 rewrite <- H8 in |- *; trivial.


 destruct H1 with st_rac3 as (st1_rac3, Htmp); trivial.
 destruct Htmp.
 set (fr2_rac3 := Rac3.State.Frame.set_pc st1_rac3@fr%rac3 pc') in |- *.
 destruct H4 with st1_rac3[fr := fr2_rac3]%rac3 as (st'_rac3, Htmp); trivial.
  destruct H6.
  rewrite H2 in |- *.
  unfold fr2_rac3 in |- *.
  split; trivial.

  inversion H6.
  split;simpl;trivial.

  destruct Htmp.
  exists st'_rac3.
  split; trivial.
  apply
   OpRac3.BlockStep_ok_next
    with (pc' := pc') (st1 := st1_rac3) (fr2 := fr2_rac3);
   trivial.
  destruct H5.
  destruct H5.
  rewrite <- H13 in |- *.
  trivial.


 destruct H1 with st_rac3 as (st'_rac3, Htmp); trivial.
 destruct Htmp.
 exists st'_rac3.
 split; trivial.
 apply OpRac3.BlockStep_ok_last; trivial.
 destruct H2.
 destruct H2.
 rewrite <- H8 in |- *; trivial.
Qed.