Library cstepLib

Require Import Coqlib.
Require Import memory.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import language.
Require Import opsem.
Require Import LibTactics.
Require Export lmachLib.
Require Import assertion.
Require Export contLib.

Lemma evaladdr_val_eq : forall e m v t, evaltype e m = Some t -> evaladdr e m = Some v -> evalval (eaddrof e) m = Some v.

Lemma evaltype_GE_eq : forall G E M1 M2 e t1 t2, evaltype e (G, E, M1) = Some t1 -> evaltype e (G,E,M2) = Some t2 -> t1 = t2.

Lemma estepstar_estep_trans : forall c ke m c´ ke´ m´ c´´ ke´´ m´´,
           estepstar c ke m c´ ke´ m´ ->
             estep c´ ke´ m´ c´´ ke´´ m´´ -> estepstar c ke m c´´ ke´´ m´´.

Lemma estepstar_estepstar_trans : forall c ke m c´ ke´ m´ c´´ ke´´ m´´,
            estepstar c ke m c´ ke´ m´ -> estepstar c´ ke´ m´ c´´ ke´´ m´´ ->
                 estepstar c ke m c´´ ke´´ m´´.

Lemma estep_deter : forall c ke m c´ ke´ m´ c´´ ke´´ m´´,
                       estep c ke m c´ ke´ m´ -> estep c ke m c´´ ke´´ m´´ ->
                       c´ = c´´ /\ m´ = m´´/\ ke´=ke´´.

Lemma sstep_idmove_deter : forall p c c´ c´´ ks ks´ ks´´ m m´ ,
                     sstep p c ks m c´ ks´ m
              -> sstep p c ks m c´´ ks´´ m´ -> c´ =c´´/\ ks´ = ks´´ /\ m =m´.

Lemma estepstar_deter: forall c ke m v v´ m´ m´´,
  estepstar c ke m [v] kenil m´ ->
 estepstar c ke m [v´] kenil m´´ -> v = v´/\ m´ = m´´.

Lemma cstep_idmove_deter : forall p C C´ C´´ m m´ ,
         cstep p C m C´ m -> cstep p C m C´´ m´
                -> C´ = C´´ /\ m = m´.

Lemma evalval_evaladdr_imply_estepstar : forall (e:expr) (m : smem),
(forall v ke, evalval e m = Some v ->
  estepstar (cure e) ke m [v]ke m) /\
    (forall v ke, evaladdr e m = Some v ->
          estepstar (cure (eaddrof e)) ke m [v] ke m).

Lemma evalval_imply_estepstar : forall (e:expr) (m : smem) v ke, evalval e m = Some v ->
estepstar (cure e) ke m [v] ke m.

Lemma evaladdr_imply_estepstar : forall (e:expr) (m : smem) v ke, evaladdr e m = Some v ->
estepstar (cure (eaddrof e)) ke m [v] ke m.

Lemma estep_mem_same : forall c ke m c´ ke´ m´, estep c ke m c´ ke´ m´ -> m = m´.

Lemma estepstar_mem_same : forall c ke m c´ ke´ m´, estepstar c ke m c´ ke´ m´ -> m = m´.

Lemma cstep_safe_mono: forall p C m M m´, ~(cstepabt p C m) -> SysmemJoinM m M m´ -> ~(cstepabt p C m´).

Lemma cstep_frame : forall p C m M m´ m´´ C´, ~(cstepabt p C m) -> SysmemJoinM m M m´ -> cstep p C m´ C´ m´´ ->
                                              (exists m1´´, SysmemJoinM m1´´ M m´´ /\ cstep p C m C´ m1´´).
Ltac Some_eq :=
  match goal with
    | |- ?x = ?y =>
    cut (Some x = Some y); [ let H := fresh in intros H; inversion H; auto | idtac ]
    end.

Ltac Tptr_eq :=
  match goal with
    | |- ?x = ?y =>
    cut (Tptr x = Tptr y); [ let H := fresh in intros H; inversion H; auto | idtac ]
    end.

Lemma cstep_idmove_frame :
  forall G E M1 M M2 m´ p C C´ C´´,
    MemMod.join M1 M M2 ->
      cstep p C (G, E, M1) C´ (G, E, M1) ->
        cstep p C (G, E, M2) C´´ m´ ->
          C´´ = C´ /\ m´ = (G, E, M2).

Lemma estepstar_imply_star : forall c c´ ke ke´ m v ,
        estepstar c ke m c´ ke´ m -> estepstar c ke m [v] kenil m ->
        estepstar c´ ke´ m [v] kenil m.

Ltac destru m := (let H := fresh in destruct m as ( H & m)).

Lemma estepv_notabortm : forall m v c ke ,
                         estepstar c ke m [v] kenil m ->
 ~ IsFcall (c,(ke,kstop)) /\
~ IsSwitch (c,(ke,kstop)) /\ ~ IsRet (c,(ke,kstop)) /\ ~ IsRetE (c,(ke,kstop)) /\ ~ IsIRet (c,(ke,kstop)) .