Library Clight_sim

Require Import sepcomp.core_semantics.
Require Import sepcomp.forward_simulations.
Require Import sepcomp.forward_simulations_lemmas.

Require Import veric.base.
Require Import veric.Clight_lemmas.
Require Import veric.Clight_new.
Require Clight.
Module CC := Clight.

Definition CCstep ge := Clight.step ge Clight.function_entry2.

Lemma cc_step_fun: forall ge s1 s2 s2',
   CCstep ge s1 nil s2 -> CCstep ge s1 nil s2' -> s2=s2'.
Proof.
 intros.
 inv H; inv H0;
 repeat match goal with
  | H: _ \/ _ |- _ => destruct H; try discriminate
  end;
 try contradiction;
  repeat fun_tac; auto; try congruence.
  pose proof (assign_loc_fun H15 H4); subst m'0. auto.
  inversion2 H5 H18.
   pose proof (eval_exprlist_fun H16 H3); subst; auto.
  destruct (Events.external_call_determ _ _ _ _ _ _ _ _ _ _ H14 H2).
  destruct H0; subst; auto.
  inv H1; inv H6.
  inversion2 H9 H4.
  pose proof (alloc_variables_fun H8 H3). inv H4.
  auto.
  destruct (Events.external_call_determ _ _ _ _ _ _ _ _ _ _ H9 H1).
  destruct H0; subst; auto.
Qed.

Fixpoint strip_skip' (k: CC.cont) : CC.cont :=
 match k with
 | CC.Kseq Sskip k' => strip_skip' k'
 | _ => k
 end.

Inductive match_cont: cont -> CC.cont -> Prop :=
  | match_cont_nil: match_cont nil CC.Kstop
  | match_cont_seq: forall s k k',
         match_cont (strip_skip k) (strip_skip' k') ->
          match_cont (Kseq s :: k) (CC.Kseq s k')
  | match_cont_loop1: forall e3 s k k',
         match_cont (strip_skip k) (strip_skip' k') ->
          match_cont (Kseq Scontinue :: Kloop1 s e3 :: k) (CC.Kloop1 s e3 k')
  | match_cont_loop2: forall e3 s k k',
         match_cont (strip_skip k) (strip_skip' k') ->
          match_cont (Kloop2 s e3 :: k) (CC.Kloop2 s e3 k')
  | match_cont_switch: forall k k',
         match_cont (strip_skip k) (strip_skip' k') ->
          match_cont (Kswitch :: k) (CC.Kswitch k')
  | match_cont_call: forall lid fd f ve te k k'
         (CUR: current_function k = Some f),
         match_cont (strip_skip k) (strip_skip' k') ->
          match_cont (Kseq (Sreturn None) :: Kcall lid fd ve te :: k) (CC.Kcall lid f ve te k').


Lemma exec_skips:
 forall {s0 k s k'}
   (H1: match_cont (Kseq s0 :: k) (strip_skip' (CC.Kseq s k')))
   ge f ve te m,
   match s0 with Sskip => False | Scontinue => False | Sloop _ _ => False
            | Sifthenelse _ _ _ => False | Sreturn _ => False
            | _ => True end ->
   exists k2, strip_skip' (CC.Kseq s k') = CC.Kseq s0 k2 /\
     Smallstep.star CCstep ge (CC.State f s k' ve te m) Events.E0
              (CC.State f s0 k2 ve te m).
Proof.
 intros.
 remember (CC.Kseq s k') as k0.
 revert k s k' H1 Heqk0; induction k0; intros; inv Heqk0.
 assert ({s1=Sskip}+{s1<>Sskip}) by (destruct s1; try (left; congruence); right; congruence).
 destruct H0. subst s1.
 destruct k'; try solve [inv H1].
 specialize (IHk0 _ s k' H1 (eq_refl _)).
 destruct IHk0 as [k2 [? ?]].
 exists k2. split; simpl; auto.
 econstructor 2. constructor. eauto. auto.
 inv H1; contradiction. simpl in *. inv H1. contradiction.
  replace (strip_skip' (CC.Kseq s1 k')) with (CC.Kseq s1 k') in *
     by (destruct s1; try congruence; auto).
 inv H1.
 exists k'; split; auto.
 constructor 1.
Qed.

Lemma strip_skip_not:
  forall s k, s<>Sskip -> strip_skip (Kseq s :: k) = (Kseq s :: k).
Proof.
 destruct s; intros; auto. congruence.
Qed.
Lemma strip_skip'_not:
  forall s k, s<>Sskip -> strip_skip' (CC.Kseq s k) = (CC.Kseq s k).
Proof.
 destruct s; intros; auto. congruence.
Qed.

Lemma dec_skip: forall s, {s=Sskip}+{s<>Sskip}.
Proof.
 destruct s; try (left; congruence); right; congruence.
Qed.

Lemma dec_continue: forall s, {s=Scontinue}+{s<>Scontinue}.
Proof.
 destruct s; try (left; congruence); right; congruence.
Qed.

Lemma strip_step:
  forall ge ve te k m st' m',
     cl_step ge (State ve te (strip_skip k)) m st' m' <->
    cl_step ge (State ve te k) m st' m'.
Proof.
intros.
 induction k; intros; split; simpl; intros; try destruct IHk; auto.
 destruct a; try destruct s; auto.
  constructor; auto.
 destruct a; try destruct s; auto.
 inv H. auto.
Qed.

Lemma continue_cont_skip:
  forall k, continue_cont k = continue_cont (strip_skip k).
Proof.
 induction k; simpl; intros; auto.
 destruct a; auto. destruct s; auto.
Qed.

Lemma break_cont_skip:
    forall k, break_cont (strip_skip k) = break_cont k.
Proof. induction k; try destruct a; simpl; auto; destruct s; simpl; auto.
Qed.

Lemma continue_cont_is:
 forall k, match (continue_cont k) with nil => True | Kseq e3 :: Kloop2 s e3' :: _ => e3=e3' | _ => False end.
Proof.
 induction k; simpl; auto; try contradiction.
  destruct a; auto.
Qed.

Inductive step' ge : (corestate * mem) -> Events.trace -> (corestate * mem) -> Prop :=
 mk_step': forall q m q' m', cl_step ge q m q' m' -> step' ge (q,m) Events.E0 (q',m').

Definition ef_exit := EF_external exit_syscall_number (mksignature nil None).

Inductive initial_state (p: program): (corestate * mem) -> Prop :=

  .

Inductive final_state: (corestate * mem) -> int -> Prop :=

 .
Lemma match_cont_strip:
   forall s k k', match_cont (strip_skip k) (strip_skip' k') ->
           match_cont (strip_skip (Kseq s :: k)) (strip_skip' (CC.Kseq s k')).
 Proof.
 intros. destruct (dec_skip s). subst. simpl; auto.
  rewrite strip_skip_not by auto. rewrite strip_skip'_not by auto.
  constructor; auto.
 Qed.

Lemma exec_skips':
  forall ge f s k' s0 k0' ve te m,
        strip_skip' (CC.Kseq s k') = CC.Kseq s0 k0' ->
        Smallstep.star CCstep ge (CC.State f s k' ve te m) Events.E0
                                   (CC.State f s0 k0' ve te m).
Proof.
 intros.
 destruct (dec_skip s). subst. simpl in *.
 induction k'; try solve [inv H].
 destruct (dec_skip s). subst. simpl in *.
 econstructor 2; eauto. constructor. auto. rewrite strip_skip'_not in * by auto.
 inv H. econstructor 2; eauto. constructor. constructor 1. auto.
 rewrite strip_skip'_not in H by auto. inv H. constructor 1.
Qed.

Lemma break_strip:
 forall ge f ve te m k,
     Smallstep.star CCstep ge (CC.State f Sbreak k ve te m) nil (CC.State f Sbreak (strip_skip' k) ve te m).
 Proof. induction k; try solve [constructor 1].
    destruct (dec_skip s). subst. simpl.
     econstructor 2. constructor. eauto. auto.
  rewrite strip_skip'_not; auto. constructor 1.
Qed.

Lemma plus_trans: forall ge s1 s2 s3,
   Smallstep.plus CCstep ge s1 Events.E0 s2 -> Smallstep.plus CCstep ge s2 Events.E0 s3 -> Smallstep.plus CCstep ge s1 Events.E0 s3.
Proof.
 intros. eapply Smallstep.plus_trans; eauto.
Qed.

Lemma star_plus_trans: forall ge s1 s2 s3,
   Smallstep.star CCstep ge s1 Events.E0 s2 -> Smallstep.plus CCstep ge s2 Events.E0 s3 -> Smallstep.plus CCstep ge s1 Events.E0 s3.
Proof.
 intros. eapply Smallstep.star_plus_trans; eauto.
Qed.

Lemma plus_star_trans: forall ge s1 s2 s3,
   Smallstep.plus CCstep ge s1 Events.E0 s2 -> Smallstep.star CCstep ge s2 Events.E0 s3 -> Smallstep.plus CCstep ge s1 Events.E0 s3.
Proof.
 intros. eapply Smallstep.plus_star_trans; eauto.
Qed.

Lemma star_trans: forall ge s1 s2 s3,
   Smallstep.star CCstep ge s1 Events.E0 s2 -> Smallstep.star CCstep ge s2 Events.E0 s3 -> Smallstep.star CCstep ge s1 Events.E0 s3.
Proof.
 intros. eapply Smallstep.star_trans; eauto.
Qed.

Lemma strip_skip'_loop2:
  forall ge f ve te m a3 s k1 k, CC.Kloop2 a3 s k1 = strip_skip' k ->
  Smallstep.star CCstep ge (CC.State f Sskip k ve te m) Events.E0 (CC.State f Sskip (CC.Kloop2 a3 s k1) ve te m).
Proof.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s0). subst. eapply Smallstep.star_trans; try apply IHk; auto. apply Smallstep.star_one. constructor. auto.
 rewrite strip_skip'_not in * by auto.
 rewrite <- H. constructor 1. simpl in H. inv H. constructor 1.
Qed.

Lemma call_strip: forall k, call_cont (strip_skip k) = call_cont k.
Proof.
 induction k; simpl; intros; auto. destruct a; simpl; auto. destruct s; simpl; auto.
Qed.

Lemma strip_call: forall k, strip_skip (call_cont k) = call_cont k.
Proof.
 induction k; simpl; intros; auto. destruct a; simpl; auto.
Qed.

Lemma call_strip': forall k, CC.call_cont (strip_skip' k) = CC.call_cont k.
Proof.
 induction k; simpl; intros; auto. destruct s; simpl; auto.
Qed.

Lemma strip_call': forall k, strip_skip' (CC.call_cont k) = CC.call_cont k.
Proof.
 induction k; simpl; intros; auto.
Qed.

Lemma strip_skip'_loop1:
  forall ge f ve te m a3 s k1 k, CC.Kloop1 a3 s k1 = strip_skip' k ->
  Smallstep.star CCstep ge (CC.State f Sskip k ve te m) Events.E0 (CC.State f Sskip (CC.Kloop1 a3 s k1) ve te m).
Proof.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s0). subst. eapply Smallstep.star_trans; try apply IHk; auto. apply Smallstep.star_one. constructor. auto.
 rewrite strip_skip'_not in * by auto.
 rewrite <- H. constructor 1. simpl in H. inv H. constructor 1.
Qed.

Lemma strip_skip'_call:
  forall ge f ve te m lid f' ve' te' k1 k, CC.Kcall lid f' ve' te' k1 = strip_skip' k ->
  Smallstep.star CCstep ge (CC.State f Sskip k ve te m) Events.E0 (CC.State f Sskip (CC.Kcall lid f' ve' te' k1) ve te m).
Proof.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s). subst. eapply Smallstep.star_trans; try apply IHk; auto. apply Smallstep.star_one. constructor. auto.
 rewrite strip_skip'_not in * by auto.
 rewrite <- H. constructor 1. simpl in H. inv H. constructor 1.
Qed.

Lemma match_cont_call_strip:
 forall k k',
    call_cont k <> nil ->
    match_cont (strip_skip k) (strip_skip' k') ->
   match_cont (Kseq (Sreturn None) :: call_cont k) (CC.call_cont k').
Proof.
 intros.
 rewrite <- call_strip in *. rewrite <- call_strip'.
 forget (strip_skip k) as k1. forget (strip_skip' k') as k1'.
 revert H; induction H0; simpl; intros; try rewrite call_strip in *; try rewrite call_strip' in *; auto.
 congruence.
 constructor; auto.
Qed.

Lemma match_cont_strip1:
  forall k k', match_cont k k' -> match_cont (strip_skip k) (strip_skip' k').
 Proof. induction 1; try solve [constructor; auto].
 apply match_cont_strip. auto.
Qed.

Lemma match_find_label_None:
  forall lbl s1 k0 k0', match_cont (strip_skip k0) (strip_skip' k0') ->
     find_label lbl s1 k0 = None -> CC.find_label lbl s1 k0' = None
 with match_find_ls_None:
   forall lbl ls k0 k0', match_cont (strip_skip k0) (strip_skip' k0') ->
     find_label_ls lbl ls k0 = None -> CC.find_label_ls lbl ls k0' = None.
Proof. induction s1; intros; simpl in *; auto.
 revert H0; case_eq (find_label lbl s1_1 (Kseq s1_2 :: k0)); intros. inv H1.
 erewrite IHs1_1; eauto. apply match_cont_strip. auto.
 revert H0; case_eq (find_label lbl s1_1 k0); intros. inv H1.
 erewrite IHs1_1; eauto.
 revert H0; case_eq (find_label lbl s1_1 (Kseq Scontinue :: Kloop1 s1_1 s1_2 :: k0)); intros. inv H1.
 erewrite IHs1_1; eauto. erewrite IHs1_2; eauto. simpl. constructor. auto.
 simpl. constructor; auto.
 eapply match_find_ls_None; eauto. constructor. auto.
 if_tac. subst. inv H0. eapply match_find_label_None; eauto.
 induction ls; intros; simpl in *.
 eapply match_find_label_None; eauto.
 revert H0; case_eq (find_label lbl s (Kseq (seq_of_labeled_statement ls) :: k0)); intros.
 inv H1.
 erewrite match_find_label_None; eauto. apply match_cont_strip. auto.
Qed.

Lemma match_find_label: forall lbl k' s1 k0 k0',
     match_cont (strip_skip k0) (strip_skip' k0') ->
     (find_label lbl s1 k0 = Some k' ->
      exists s2 : statement, exists k2' : CC.cont,
       CC.find_label lbl s1 k0' = Some (s2, k2') /\
       match_cont k' (CC.Kseq s2 k2'))
 with match_find_label_ls: forall lbl k' s1 k0 k0',
     match_cont (strip_skip k0) (strip_skip' k0') ->
     (find_label_ls lbl s1 k0 = Some k' ->
      exists s2 : statement, exists k2' : CC.cont,
       CC.find_label_ls lbl s1 k0' = Some (s2, k2') /\
       match_cont k' (CC.Kseq s2 k2')).
Proof.
 induction s1; intros; simpl in *; intuition; try discriminate.
 revert H0; case_eq (find_label lbl s1_1 (Kseq s1_2 :: k0)); intros.
 inv H1.
 destruct (IHs1_1 (Kseq s1_2 :: k0) (CC.Kseq s1_2 k0')) as [s2 [k2' [? ?]]]; clear IHs1_1.
 apply match_cont_strip. auto. auto.
 exists s2; exists k2'; split; auto. rewrite H1; auto.
  destruct (IHs1_2 k0 k0') as [s2 [k2' [? ?]]]; clear IHs1_1 IHs1_2; auto.
 exists s2, k2'; split; auto.
 erewrite match_find_label_None; eauto.
  apply match_cont_strip. auto.
 revert H0; case_eq (find_label lbl s1_1 k0); intros. inv H1.
 destruct (IHs1_1 k0 k0') as [s2 [k2' [? ?]]]; clear IHs1_1; auto.
 exists s2, k2'; split; auto.
 rewrite H1. auto.
  destruct (IHs1_2 k0 k0') as [s2 [k2' [? ?]]]; clear IHs1_1 IHs1_2; auto.
 exists s2, k2'; split; auto.
 erewrite match_find_label_None; eauto.
 revert H0; case_eq (find_label lbl s1_1 (Kseq Scontinue :: Kloop1 s1_1 s1_2 :: k0)); intros.
 inv H1.
 destruct (IHs1_1 (Kseq Scontinue :: Kloop1 s1_1 s1_2 :: k0) (CC.Kloop1 s1_1 s1_2 k0')) as [s2 [k2' [? ?]]]; clear IHs1_1; auto.
 simpl. constructor; auto.
 exists s2, k2'; split; auto. rewrite H1. auto.
 destruct (IHs1_2 (Kloop2 s1_1 s1_2 :: k0) (CC.Kloop2 s1_1 s1_2 k0')) as [s2 [k2' [? ?]]]; clear IHs1_1; auto.
 constructor; auto.
 exists s2, k2'; split; auto.
 erewrite match_find_label_None; eauto. simpl. constructor; auto.
 destruct (match_find_label_ls lbl k' l (Kswitch :: k0) (CC.Kswitch k0')) as [s2 [k2' [? ?]]]; auto.
 constructor; auto.
 exists s2, k2'; split; auto.
 if_tac. subst l.
 exists s1, k0'; split; auto. inv H0; constructor; auto.
 destruct (IHs1 k0 k0') as [s2 [k2' [? ?]]]; auto.
 exists s2, k2'; split; auto.

 induction s1; intros. simpl in *.
 eauto.
 simpl in *.
 revert H0; case_eq (find_label lbl s (Kseq (seq_of_labeled_statement s1) :: k0)); intros.
 inv H1.
destruct (match_find_label lbl k' s (Kseq (seq_of_labeled_statement s1) :: k0) (CC.Kseq (seq_of_labeled_statement s1) k0')) as [s2 [k2' [? ?]]]; auto.
apply match_cont_strip. auto.
 exists s2, k2'; split; auto.
 rewrite H1. auto.
 erewrite match_find_label_None; eauto.
apply match_cont_strip. auto.
Qed.

Lemma current_function_strip: forall k, current_function (strip_skip k) = current_function k.
Proof.
 induction k; try destruct a; try destruct s; simpl; auto.
Qed.

 Lemma current_function_call_cont:
   forall k, current_function (call_cont k) = current_function k.
 Proof. induction k; try destruct a; simpl; auto. Qed.

 Lemma current_function_find_label:
  forall lbl f s k k', current_function k = Some f ->
              find_label lbl s k = Some k' ->
              current_function k' = Some f
 with current_function_find_label_ls:
  forall lbl f s k k', current_function k = Some f ->
              find_label_ls lbl s k = Some k' ->
              current_function k' = Some f.
 Proof.
   induction s; simpl; intros; try discriminate.
   revert H0; case_eq (find_label lbl s1 (Kseq s2 :: k)); intros. inv H1.
   eapply IHs1; [ | eauto]. simpl; auto.
   eapply IHs2; [ | eauto]. simpl; auto.
 revert H0; case_eq (find_label lbl s1 k); intros. inv H1.
   eapply IHs1; [ | eauto]. simpl; auto.
   eapply IHs2; [ | eauto]. simpl; auto.
 revert H0; case_eq (find_label lbl s1 (Kseq Scontinue :: Kloop1 s1 s2 :: k)); intros. inv H1.
   eapply IHs1; [ | eauto]. simpl; auto.
   eapply IHs2; [ | eauto]. simpl; auto.
  eapply current_function_find_label_ls; [ | eauto]. simpl; auto.
  if_tac in H0. inv H0. simpl. auto.
   eapply IHs; [ | eauto]. simpl; auto.
   induction s; simpl; intros; try discriminate.
  eapply current_function_find_label; [ | eauto]. simpl; auto.
  revert H0; case_eq (find_label lbl s (Kseq (seq_of_labeled_statement s0) :: k)); intros.
 inv H1.
  eapply current_function_find_label; [ | eauto]. simpl; auto.
   eapply IHs; [ | eauto]. simpl; auto.
 Qed.

Lemma step_continue_strip:
  forall ge f k ve te m,
           Smallstep.star CCstep ge (CC.State f Scontinue k ve te m) Events.E0
               (CC.State f Scontinue (strip_skip' k) ve te m).
Proof.
intros.
induction k; simpl; try constructor 1.
destruct (dec_skip s).
subst.
eapply Smallstep.star_trans.
  apply Smallstep.star_one. apply CC.step_continue_seq.
  apply IHk.
auto.
destruct s; try congruence; constructor 1.
Qed.

Inductive CC_core : Type :=
    CC_core_State : function ->
            statement -> CC.cont -> env -> temp_env -> CC_core
  | CC_core_Callstate : fundef -> list val -> CC.cont -> CC_core
  | CC_core_Returnstate : val -> CC.cont -> CC_core.

Definition CC_core_to_CC_state (c:CC_core) (m:mem) : CC.state :=
  match c with
     CC_core_State f st k e te => CC.State f st k e te m
  | CC_core_Callstate fd args k => CC.Callstate fd args k m
  | CC_core_Returnstate v k => CC.Returnstate v k m
 end.
Definition CC_state_to_CC_core (c:CC.state): CC_core * mem :=
  match c with
     CC.State f st k e te m => (CC_core_State f st k e te, m)
  | CC.Callstate fd args k m => (CC_core_Callstate fd args k, m)
  | CC.Returnstate v k m => (CC_core_Returnstate v k, m)
 end.

Lemma CC_core_CC_state_1: forall c m,
   CC_state_to_CC_core (CC_core_to_CC_state c m) = (c,m).
  Proof. intros. destruct c; auto. Qed.

Lemma CC_core_CC_state_2: forall s c m,
   CC_state_to_CC_core s = (c,m) -> s= CC_core_to_CC_state c m.
  Proof. intros. destruct s; simpl in *.
      destruct c; simpl in *; inv H; trivial.
      destruct c; simpl in *; inv H; trivial.
      destruct c; simpl in *; inv H; trivial.
  Qed.

Lemma CC_core_CC_state_3: forall s c m,
   s= CC_core_to_CC_state c m -> CC_state_to_CC_core s = (c,m).
  Proof. intros. subst. apply CC_core_CC_state_1. Qed.

Lemma CC_core_CC_state_4: forall s, exists c, exists m, s = CC_core_to_CC_state c m.
  Proof. intros. destruct s.
             exists (CC_core_State f s k e le). exists m; reflexivity.
             exists (CC_core_Callstate fd args k). exists m; reflexivity.
             exists (CC_core_Returnstate res k). exists m; reflexivity.
  Qed.

Lemma CC_core_to_CC_state_inj: forall c m c' m',
     CC_core_to_CC_state c m = CC_core_to_CC_state c' m' -> (c',m')=(c,m).
  Proof. intros.
       apply CC_core_CC_state_3 in H. rewrite CC_core_CC_state_1 in H. inv H. trivial.
  Qed.

Inductive match_states: forall (qm: corestate) (st: CC_core), Prop :=
 | match_states_seq: forall f ve te s k k'
      (CUR: current_function k = Some f),
      match_cont (strip_skip k) (strip_skip' (CC.Kseq s k')) ->
      match_states (State ve te k) (CC_core_State f s k' ve te)
 | match_states_ext: forall k f ef tyargs tyres args lid ve te k'
      (CUR: current_function k = Some f),
      match_cont (strip_skip k) (strip_skip' k') ->
      match_states (ExtCall ef (signature_of_type tyargs tyres) args lid ve te k)
           (CC_core_Callstate (External ef tyargs tyres) args (CC.Kcall lid f ve te k')).

Lemma Clightnew_Clight_sim_eq_noOrder_SSplusConclusion:
forall p (c1 : corestate) (m : mem) (c1' : corestate) (m' : mem),
corestep cl_core_sem (Genv.globalenv p) c1 m c1' m' ->
forall (c2 : CC_core),
 match_states c1 c2 ->
exists c2' : CC_core,
    Smallstep.plus CCstep (Genv.globalenv p) (CC_core_to_CC_state c2 m) Events.E0 (CC_core_to_CC_state c2' m') /\
    match_states c1' c2'.
Proof.
intros.
forget (Genv.globalenv p) as ge. clear p.
simpl in H.
revert c2 H0. induction H; intros.

Focus 1. inv H4.
simpl strip_skip in H9.
destruct (exec_skips H9 ge f ve te m) as [k2 [? ?]]; auto.
exists (CC_core_State f Sskip k2 ve te); split.
    eapply Smallstep.star_plus_trans. eassumption.
          apply Smallstep.plus_one. econstructor; eauto. reflexivity.
    constructor. apply CUR. rewrite H4 in H9. inv H9. simpl in *. apply H7.

Focus 1. inv H0.
destruct (exec_skips H5 ge f ve te m) as [k2 [? ?]]; auto.
exists (CC_core_State f Sskip k2 ve (PTree.set id v te)); split.
  eapply Smallstep.star_plus_trans. eassumption. apply Smallstep.plus_one. econstructor; eauto. auto.
  rewrite H0 in H5. inv H5; constructor; auto.

Focus 1. inv H7.
 destruct (exec_skips H12 ge f0 ve te m) as [k2 [? ?]]; auto.
 rewrite H7 in *. inv H12. simpl in CUR.
  exists (CC_core_State f (fn_body f) (CC.Kcall optid f0 ve te k2) ve' le').
  split.
eapply star_plus_trans. apply H8.
               eapply Smallstep.plus_two. econstructor; eauto.
              econstructor; eauto.
               apply list_norepet_app in H4. destruct H4 as [? [? ?]].
               econstructor; auto. reflexivity.
constructor.
              auto.
             apply match_cont_strip. simpl. constructor; auto.

Focus 1. inv H3.
 destruct (exec_skips H8 ge f ve te m) as [k2 [? ?]]; auto.
 rewrite H3 in *. inv H8. simpl in CUR.
  exists (CC_core_Callstate (External ef tyargs tyres) vargs (CC.Kcall optid f ve te k2)).
  split.
eapply star_plus_trans. eassumption. eapply Smallstep.plus_one. econstructor; eauto.
econstructor; eauto.

Focus 1.  inv H0.
 destruct (exec_skips H5 ge f ve te m) as [k2 [? ?]]; auto.
 rewrite H0 in *. inv H5.
 destruct (IHcl_step (CC_core_State f s1 (CC.Kseq s2 k2) ve te))
                as [st2 [? ?]]; clear IHcl_step.
 repeat constructor; auto.
 apply match_cont_strip. apply match_cont_strip. auto.
 exists st2; split; auto.
 eapply star_plus_trans; [ eassumption | ].
 eapply plus_trans. apply Smallstep.plus_one. constructor. eassumption.

 Focus 1.  inv H0.
 simpl strip_skip in H5.
 remember (strip_skip k) as k0.
 destruct k0.
 elimtype False; clear - H Heqk0.
 revert H; induction k; intros. inv H.
 forget (a::k) as k'; clear - Heqk0 H.
 remember (State ve te k') as s.
 revert ve te k' Heqs Heqk0; induction H; intros; inv Heqs; simpl in *; try congruence.
 eapply IHcl_step. reflexivity. auto.
 remember (strip_skip' (CC.Kseq s k')) as k0'.
 destruct k0'; inv H5;
  try solve [rewrite <- strip_step in H; rewrite <- Heqk0 in H; inv H].
 assert (s0<>Sskip).
 clear- Heqk0; intro; subst.
 revert Heqk0; induction k; simpl; intros. inv Heqk0. destruct a; try solve [inv Heqk0]; auto. destruct s; inv Heqk0; auto.
 destruct (IHcl_step (CC_core_State f s k' ve te))
                 as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. rewrite <- Heqk0. rewrite <- Heqk0'.
 constructor 2; auto.
 exists st2; split; auto.

  destruct (IHcl_step (CC_core_State f Sskip (CC.Kloop1 s0 s1 k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. simpl. rewrite <- Heqk0. constructor. auto.
  exists st2; split; auto.
 inv H0. destruct t1; inv H5. simpl in H0. subst t2.
 eapply plus_star_trans; try apply H4.
 clear - H3 Heqk0'.
 destruct s; inv Heqk0'.
 rewrite H0 in H3.
 eapply star_plus_trans; [ | apply Smallstep.plus_one; eauto ].
 rewrite <- H0;
 apply strip_skip'_loop1; auto.

 destruct (IHcl_step (CC_core_State f Sskip (CC.Kloop2 s0 s1 k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 destruct (dec_skip s). subst.
 econstructor; eauto. rewrite <- Heqk0. constructor. auto.
 rewrite strip_skip'_not in Heqk0' by auto. inv Heqk0'.
  exists st2; split; auto.
  destruct s; inv Heqk0'.
 eapply star_plus_trans; try apply H0.
 clear - H4; revert H4; induction k'; intros; inv H4.
 destruct (dec_skip s). subst.
 specialize (IHk' H0). econstructor 2. constructor. apply IHk'. auto.
 replace (CC.Kloop2 s0 s1 k0') with (CC.Kseq s k') by (destruct s; auto; congruence).
 constructor 1.
 constructor 1.

 destruct s; inv Heqk0'.
 destruct (IHcl_step (CC_core_State f Sskip (CC.Kcall o f0 e t k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. rewrite <- Heqk0. constructor; auto.
  exists st2; split; auto.
  inv H0. destruct t1; inv H6. simpl in H0; subst t2.
 eapply plus_star_trans; [ | apply H5].
 inv H4.
 eapply star_plus_trans; [eapply strip_skip'_call; eauto | ].
 apply Smallstep.plus_one. constructor; auto.

 Focus 1.  inv H0.
 simpl strip_skip in H5.
 inv H5.
 Focus 1.  change (CC.Kseq Scontinue k'0 = strip_skip' (CC.Kseq s k')) in H3.
 symmetry in H3.
 rewrite continue_cont_skip in *.
 simpl in CUR.
 rewrite <- current_function_strip in CUR.
forget (strip_skip k) as k0. clear k. rename k0 into k.

 generalize (continue_cont_is k); case_eq (continue_cont k); intros; try contradiction.
 rewrite H0 in H; inv H.
 destruct c; try contradiction. destruct l; try contradiction. destruct c; try contradiction.
 subst s0.

 assert (Smallstep.star CCstep ge (CC.State f s k' ve te m) Events.E0
                             (CC.State f Scontinue k'0 ve te m)).
 clear - H3.
 destruct (dec_skip s). subst. simpl in H3.
 eapply exec_skips'; auto.
 rewrite strip_skip'_not in H3 by auto. inv H3. constructor.
 assert (Smallstep.star CCstep ge (CC.State f Scontinue k'0 ve te m) Events.E0
                                 (CC.State f Scontinue (strip_skip' k'0) ve te m)).
clear.
  induction k'0; try solve [constructor 1].
 destruct (dec_skip s). subst. simpl in *. econstructor 2. constructor. eassumption. auto.
  rewrite strip_skip'_not; auto. constructor 1.
 generalize (Smallstep.star_trans H2 H4 (eq_refl _)); clear H2 H4; intro.
 clear H3.
 forget (strip_skip' k'0) as k0'; clear k'0.
 assert (precontinue_cont k = Kloop1 s1 s2 :: l).
 revert H0; clear; induction k; simpl; try congruence. destruct a; try congruence; auto.
 assert (exists k1',
               Smallstep.star CCstep ge (CC.State f Scontinue k0' ve te m)
                  (Events.Eapp Events.E0 Events.E0)
                    (CC.State f Scontinue k1' ve te m) /\
               match_cont (Kseq Scontinue :: Kloop1 s1 s2 :: l) k1').
 clear - H1 H0.
 revert H0; induction H1; simpl; intros; try congruence.
 destruct IHmatch_cont as [k1' [? ?]].
 rewrite <- continue_cont_skip; auto.
 econstructor. split; [ | eassumption].
 eapply star_trans; try apply H.
 clear.
 eapply star_trans. apply Smallstep.star_one.
 apply CC.step_continue_seq.
 apply step_continue_strip.
 inv H0.
 econstructor; split. constructor 1. constructor. auto.
 destruct IHmatch_cont as [k1' [? ?]].
 rewrite <- continue_cont_skip; auto.
 econstructor. split; [ | eassumption].
 eapply star_trans; try apply H.
 eapply star_trans. apply Smallstep.star_one.
 apply CC.step_continue_switch.
 apply step_continue_strip.

 destruct H4 as [k1' [? ?]].
 generalize (Smallstep.star_trans H2 H4 (eq_refl _)); clear H2 H4; intro H2.
 rewrite H0 in *.
 assert (CUR': current_function l = Some f).
   clear - CUR H0. revert CUR H0; induction k; simpl; intros. inv CUR.
   destruct a; try discriminate; auto. inv H0. auto.
 clear H1 CUR k H0 H3.
 inv H5. inv H4. simpl in *.
 destruct (IHcl_step (CC_core_State f s2 (CC.Kloop2 s1 s2 k'0) ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. apply match_cont_strip. constructor. auto.
 exists st2; split; auto.
 eapply star_plus_trans; [apply H2 | ].
 eapply star_plus_trans; [ | apply H0].
 apply Smallstep.star_one. constructor. auto.

Focus 1.    change (CC.Kloop1 s0 e3 k'0 = strip_skip' (CC.Kseq s k')) in H1.
 destruct (dec_skip s); [ | destruct s; try congruence; inv H1].
 subst s.
 simpl in H.
 simpl in H1.
 simpl in *.
 assert (Smallstep.star CCstep ge (CC.State f Sskip k' ve te m) Events.E0
                   (CC.State f Sskip (CC.Kloop1 s0 e3 k'0) ve te m)).
 rewrite H1; clear.
 induction k'; intros; try solve [constructor 1].
  destruct (dec_skip s). subst. simpl in *. econstructor 2. constructor.
  apply IHk'. auto.
 rewrite strip_skip'_not; auto. constructor 1.
 forget (CC.State f Sskip k' ve te m) as st1.
 clear k' H1.
 assert (Smallstep.plus CCstep ge st1 Events.E0
                  (CC.State f e3 (CC.Kloop2 s0 e3 k'0) ve te m)).
 eapply Smallstep.star_plus_trans; try apply H0.
 econstructor. constructor. auto. constructor 1. reflexivity. auto.
 clear H0.
 destruct (IHcl_step (CC_core_State f e3 (CC.Kloop2 s0 e3 k'0) ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. apply match_cont_strip; constructor; auto.
 exists st2; split; auto.
 eapply plus_trans; eauto.

 Focus 1.
 inv H0. simpl strip_skip in H5.
 destruct (dec_skip s).
 subst. simpl strip_skip' in *.
 assert (exists k1', strip_skip' k' = CC.Kseq Sbreak k1').
     revert H5; clear. remember (strip_skip' k') as k0'.
     revert k' Heqk0'; induction k0'; intros; try solve [inv H5].
        inv H5. eauto.
 destruct H0 as [k1' H0].
 assert (Smallstep.star CCstep ge (CC.State f Sskip k' ve te m) Events.E0
                           (CC.State f Sbreak k1' ve te m)).
       revert k1' H0; clear; induction k'; intros; try solve [inv H0].
        destruct (dec_skip s). subst. simpl in *. specialize (IHk' _ H0).
            econstructor 2. constructor. eassumption. auto.
      rewrite strip_skip'_not in H0 by auto. inv H0.
         econstructor 2. constructor. constructor 1. auto.
 simpl.
 forget (CC.State f Sskip k' ve te m) as st1.
 rewrite H0 in *.
 clear k' H0.
 inv H5.
 rewrite <- break_cont_skip in *.
 simpl in CUR. rewrite <- current_function_strip in CUR.
 forget (strip_skip k) as k0.
 assert (Smallstep.star CCstep ge st1 Events.E0 (CC.State f Sbreak (strip_skip' k1') ve te m)).
      eapply Smallstep.star_trans; try apply H1; auto.
      2: instantiate (1:=Events.E0); auto.
      clear.
      induction k1'; try destruct s; try solve [constructor 1].
         simpl. econstructor 2; eauto. constructor. auto.
 forget (strip_skip' k1') as k0'. clear k1' H1.
 assert (X:exists k1',
             Smallstep.plus CCstep ge (CC.State f Sbreak k0' ve te m) Events.E0
                       (CC.State f Sskip k1' ve te m)
               /\ match_cont (strip_skip (break_cont k0)) (strip_skip' k1')).
       clear - H H2.
       revert H; induction H2; intros; try solve [inv H].
            rewrite break_cont_skip in *. simpl in H.
               destruct (IHmatch_cont H) as [k1' [? ?]]; clear IHmatch_cont. simpl.
               exists k1'; split; auto.
               eapply Smallstep.star_plus_trans; try eassumption. 2: instantiate (1:=Events.E0); auto.
               econstructor 2. constructor. 2: instantiate (1:=Events.E0); auto.
              apply break_strip.

            simpl in *. exists k'; split. econstructor.
                 eapply CC.step_break_loop1. constructor 1. auto.
                 auto.

            simpl in *. exists k'; split.
                  econstructor. eapply CC.step_skip_break_switch. auto.
                  constructor 1; auto.
                  auto.
                  auto.

 destruct X as [k1' [? ?]].
 destruct (IHcl_step (CC_core_State f Sskip k1' ve te))
                      as [st2 [? ?]]; clear IHcl_step.
       constructor; auto.
       clear - H CUR.
       revert CUR; induction k0; intros. inv CUR.
       destruct a; simpl in *; auto. inv H. inv H.
 exists st2; split; auto.
 eapply star_plus_trans; try apply H5.
      eapply star_trans; try apply H0.
      apply Smallstep.plus_star; apply H1.
      auto.

 rewrite strip_skip'_not in H5 by auto.
 inv H5. clear n.
 admit.
 Focus 1.  inv H1. simpl strip_skip in H6.
 inv H6.
 change (CC.Kseq (Sifthenelse a s1 s2) k'0 = strip_skip' (CC.Kseq s k')) in H4.
 assert (Smallstep.star CCstep ge (CC.State f s k' ve te m) nil (CC.State f (Sifthenelse a s1 s2) k'0 ve te m)).
     clear - H4.
     revert H4; induction k'; intros; try solve [ destruct s; inv H4; constructor 1].
     destruct (dec_skip s). subst s.
     destruct (dec_skip s0). subst s0. simpl in *.
     eapply Smallstep.star_trans; try apply IHk'; eauto. apply Smallstep.star_one. constructor. auto.
      change (strip_skip' (CC.Kseq Sskip (CC.Kseq s0 k'))) with
               (strip_skip' (CC.Kseq s0 k')) in H4.
      rewrite strip_skip'_not in H4 by auto.
      inv H4. apply Smallstep.star_one. constructor. rewrite strip_skip'_not in * by auto.
      inv H4. constructor 1.
 exists (CC_core_State f (if b then s1 else s2) k'0 ve te); split; auto.
 eapply star_plus_trans; try apply H1.
 apply Smallstep.plus_one. econstructor; eauto. auto. constructor; auto.
 apply match_cont_strip; auto.

 Focus 1.  inv H0. inv H4.
 change (CC.Kseq (Sloop s1 s2) k'0 = strip_skip' (CC.Kseq s k')) in H2.
 generalize (exec_skips' ge f _ _ _ _ ve te m (@eq_sym _ _ _ H2)); intro.
 exists ( (CC_core_State f s1 (CC.Kloop1 s1 s2 k'0) ve te)); split.
 eapply star_plus_trans; try apply H.
 apply Smallstep.plus_one. eapply CC.step_loop; eauto.
 constructor; auto. apply match_cont_strip; constructor; auto.

 Focus 1.   inv H0. inv H4.
 destruct s0; inv H3.
 generalize (strip_skip'_loop2 ge f ve te m _ _ _ _ H1); intro.
 exists (CC_core_State f s (CC.Kloop1 s a3 k'0) ve te); split.
eapply star_plus_trans; try apply H.
               econstructor.
                            eapply CC.step_skip_loop2; eauto.
                            apply Smallstep.star_one. eapply CC.step_loop; eauto.
                            auto.
constructor; auto. apply match_cont_strip. constructor. auto.

 Focus 1.  inv H3.
  remember (strip_skip' (CC.Kseq s k'0)) as k3. simpl in CUR, H8.
 inv H8.
 generalize (exec_skips' ge f0 _ _ _ _ ve te m (@eq_sym _ _ _ H4)); intro H99.
 assert (f0=f).
   simpl in CUR; clear - CUR H.
   revert H CUR; induction k; intros. inv H. simpl in *. destruct a; auto. inv CUR; auto. inv H; auto.
 subst f.
 generalize (match_cont_call_strip k k'1); intro.
 spec H3; [congruence |]. spec H3; [auto |].
 generalize H3; rewrite H; intro.
 inv H5.
elimtype False; clear - H10.
         revert H10; induction k'1; simpl; intros; congruence.
destruct optexp; [destruct H1 as [v [? ?]] | ]; (destruct optid; destruct H2 as [H2 H2'];
               try solve [contradiction H2; auto]; subst te'' ).
                eexists (CC_core_State f Sskip k'2 ve' (PTree.set i v' te')).
                split.
                     apply (star_plus_trans _ _ _ _ H99).                      eapply plus_trans with (s2:=CC.Returnstate v' (CC.call_cont k'1) m').
                                         eapply Smallstep.plus_one. simpl. econstructor; eauto.
                                         eapply Smallstep.plus_one. simpl. rewrite <- H13.
                                         eapply CC.step_returnstate.
                    constructor; auto.
                eexists (CC_core_State f Sskip k'2 ve' te').
                split.
                     eapply (star_plus_trans _ _ _ _ H99).                           eapply plus_trans with (s2:=CC.Returnstate v' (CC.call_cont k'1) m').
                                         eapply Smallstep.plus_one. simpl. econstructor; eauto.
                                         eapply Smallstep.plus_one. simpl. rewrite <- H13. eapply CC.step_returnstate.
                    constructor; auto.
                eexists (CC_core_State f Sskip k'2 ve' te').
                split.
                     eapply (star_plus_trans _ _ _ _ H99).                           eapply plus_trans with (s2:=CC.Returnstate Vundef (CC.call_cont k'1) m').
                                         eapply Smallstep.plus_one. simpl. econstructor; eauto.
                                         eapply Smallstep.plus_one. simpl. rewrite <- H13. eapply CC.step_returnstate.
                    constructor; auto.

 destruct optid. destruct H2. congruence.
 destruct H2; subst te''.
 simpl in H. inv H. simpl in CUR. symmetry in CUR; inv CUR.
 destruct s; inv H4.
 assert (Smallstep.star CCstep ge (CC.State f Sskip k'0 ve te m) nil
                         (CC.State f Sskip (CC.Kcall None f1 ve' te' k'1) ve te m)).
     clear H1; rename H3 into H1.
     clear - H1.
     revert H1; induction k'0; intros; try solve [inv H1].
           destruct (dec_skip s). subst s. simpl in H1.
               eapply star_trans; try apply IHk'0; auto. apply Smallstep.star_one. constructor; auto.
          rewrite strip_skip'_not in H1 by auto. rewrite <- H1. constructor 1.
          simpl in H1. inv H1. constructor 1.
 (econstructor; split; [eapply star_plus_trans; [ apply H | eapply Smallstep.plus_two ] | ]).
     eapply CC.step_skip_call; simpl; eauto.
     assert (X: CCstep ge (CC.Returnstate Vundef (CC.Kcall None f1 ve' te' k'1) m')
                                      Events.E0
                                     (CC_core_to_CC_state (CC_core_State f1 Sskip k'1 ve' te') m')).
            econstructor; eauto.
       apply X.
    auto.
    econstructor; eauto.

 Focus 1.  inv H0. simpl strip_skip in H5.
 remember (CC.Kseq s k') as k0'.
 inv H5.
 evar (c2': CC_core).
 exists c2'; split.
     Focus 2. constructor; eauto. apply match_cont_strip. simpl.
                    instantiate (1:= CC.Kswitch k'0). constructor. auto.
     generalize (exec_skips' ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
        eapply star_plus_trans; try apply H99.
        unfold c2'. apply Smallstep.plus_one. simpl. constructor; auto.

 Focus 1.  inv H0. remember (CC.Kseq s0 k') as k0'. inv H5.
 destruct (IHcl_step (CC_core_State f s k'0 ve te)) as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. apply match_cont_strip. auto.
 exists st2; split; auto.
   eapply star_plus_trans; try eassumption.
   generalize (exec_skips' ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
     eapply star_trans; try apply H99.
     apply Smallstep.star_one. constructor.

 Focus 1.  inv H0. remember (CC.Kseq s k'0) as k0'. inv H5.
  generalize (match_cont_call_strip k k'1); intro.
 spec H0.
 clear - CUR. apply (call_cont_nonnil _ _ CUR).
 specialize (H0 H1).
  rewrite <- strip_call' in H0.
 change (Kseq (Sreturn None) :: call_cont k) with (strip_skip (Kseq (Sreturn None) :: call_cont k)) in H0.
 destruct (match_find_label _ _ _ _ _ H0 H) as [s2 [k2' [? ?]]].
 exists (CC_core_State f s2 k2' ve te); split.
    simpl in CUR0. inversion2 CUR CUR0.
     generalize (exec_skips' ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
     eapply star_plus_trans; try apply H99.
         apply Smallstep.plus_one. constructor; auto.
         constructor; auto.
   clear - CUR H. forget (fn_body f) as s.
       rewrite <- current_function_call_cont in CUR.
       change (current_function (Kseq (Sreturn None) :: call_cont k) = Some f) in CUR.
        forget (Kseq (Sreturn None) :: call_cont k) as k0. clear - CUR H.
        eapply current_function_find_label; eauto.
 apply match_cont_strip1. auto.
Qed.

Definition CC_at_external (c: CC_core) : option (external_function * signature * list val) :=
  match c with
  | CC_core_State _ _ _ _ _ => None
  | CC_core_Callstate fd args k =>
    match fd with
      Internal _ => None
      | External ef tps tp =>
          match tp with
          | Tvoid => Some (ef, mksignature (typlist_of_typelist tps) None, args)
          | _ => Some (ef, mksignature (typlist_of_typelist tps) (Some (typ_of_type tp)), args)
          end
    end
  | CC_core_Returnstate _ _ => None
 end.
Parameter mkAfterExtCore: external_function -> typelist -> type -> val -> list val -> CC.cont -> option CC_core.

Definition CC_after_external (rv: option val) (c: CC_core) : option CC_core :=
  match rv, c with
   | Some v, CC_core_Callstate fd vargs k =>
                     match fd with
                         Internal _ => None
                       | External ef tps tp => mkAfterExtCore ef tps tp v vargs k
                     end

  | _, _ => None
  end.

Parameter main_function:function. Parameter myStatement:statement.
Definition CC_initial_core (ge: genv) (v: val) (args: list val) : option CC_core :=
  let tl := typed_params 2%positive (length args)
   in Some (CC_core_State main_function myStatement
                           (CC.Kseq (Scall None
                                  (Etempvar 1%positive (Tfunction (type_of_params tl) Tvoid))
                                  (map (fun x => Etempvar (fst x) (snd x)) tl))
                              (CC.Kseq (Sloop Sskip Sskip) CC.Kstop))
                          empty_env (temp_bindings 1%positive (v::args))).

Definition CC_step (ge: Genv.t fundef type) (q:CC_core) (m:mem) (q': CC_core) (m': mem) : Prop :=
  match q with
      CC_core_Callstate (External _ _ _ ) _ _ => False
   | _ => CCstep ge (CC_core_to_CC_state q m) (Events.E0)(CC_core_to_CC_state q' m')
  end.

Lemma CC_corestep_not_at_external: forall (ge : Genv.t fundef type) (m : mem) (q : CC_core) (m' : mem)
  (q' : CC_core), CC_step ge q m q' m' -> CC_at_external q = None.
  Proof. intros.
     destruct q; simpl in *; trivial.
       destruct f; trivial. contradiction.
  Qed.

Definition CC_safely_halted (q:CC_core) : option val := None.
Lemma CC_corestep_not_halted :
       forall ge m q m' q', CC_step ge q m q' m' -> CC_safely_halted q = None.
  Proof. intros; trivial. Qed.

 Lemma CC_at_external_halted_excl :
       forall q, CC_at_external q = None \/ CC_safely_halted q = None.
   Proof. intros. right; trivial. Qed.

Definition CC_core_sem : CoreSemantics (Genv.t fundef type) CC_core mem (list (ident * globdef fundef type)).
 apply (Build_CoreSemantics _ _ _ _ cl_init_mem
                CC_initial_core CC_at_external CC_after_external CC_safely_halted CC_step).
       apply CC_corestep_not_at_external.
       apply CC_corestep_not_halted.
       apply CC_at_external_halted_excl.
       admit.
  Defined.

Lemma CC_step_to_CCstep: forall ge q m q' m',
   CC_step ge q m q' m' -> CCstep ge (CC_core_to_CC_state q m) nil (CC_core_to_CC_state q' m').
  Proof. intros.
       destruct q; simpl in *. apply H.
          destruct f; try contradiction. apply H.
        apply H.
  Qed.

Definition isExternalCallState (c:CC.state) :=
  match c with CC.Callstate (External _ _ _ ) _ _ _ => True
                      | _ => False
  end.

Lemma CCstep_to_CC_step_1: forall ge c m c' m',
              CCstep ge (CC_core_to_CC_state c m) Events.E0 (CC_core_to_CC_state c' m') ->
              CC_at_external c = None -> CC_step ge c m c' m'.
   Proof. intros.
      destruct c; try apply H.
      destruct f; try apply H.
      destruct t0; try solve [inv H0].
   Qed.

  Lemma CC_atExternal_isExternal: forall s,
         (exists z, CC_at_external (fst (CC_state_to_CC_core s)) = Some z) = isExternalCallState s.
  Proof. intros. apply prop_ext.
     destruct s; simpl.
        split; intros; try contradiction. destruct H. inv H.
        destruct fd; simpl; intros.
        split; try contradiction.
        intros [z H1]. congruence.
        destruct t0; split; auto; intros; try solve[eexists; eauto].
        split; try solve[intros;elimtype False; auto|intros [? ?]; congruence].
  Qed.

Lemma step_to_CC_step: forall ge s s' (H:CCstep ge s Events.E0 s') (Hs: ~ isExternalCallState s),
       exists c, exists m, exists c', exists m',
                  s = CC_core_to_CC_state c m /\ s' = CC_core_to_CC_state c' m' /\
                  CC_step ge c m c' m'.
  Proof. intros.
       destruct (CC_core_CC_state_4 s) as [c [m Hcm]]; subst.
       destruct (CC_core_CC_state_4 s') as [c' [m' Hcm']]; subst.
       eexists. exists m. eexists. exists m'. split. reflexivity. split. reflexivity.
        apply CCstep_to_CC_step_1. apply H.
        remember (CC_at_external c) as b.
          destruct b; trivial; apply eq_sym in Heqb.
            exfalso. apply Hs. clear Hs.
            rewrite <- CC_atExternal_isExternal. exists p.
                 rewrite (CC_core_CC_state_3 _ c m); auto.
  Qed.

Lemma CC_step_to_step: forall ge c m c' m', CC_step ge c m c' m' ->
   CCstep ge (CC_core_to_CC_state c m) Events.E0 (CC_core_to_CC_state c' m').
  Proof. intros.
      destruct c; try apply H.
      destruct f; try contradiction. apply H.
  Qed.

Lemma CC_step_fun: forall ge m q m1 q1 m2 q2,
    CC_step ge q m q1 m1 ->
    CC_step ge q m q2 m2 ->
    (q1,m1)=(q2,m2).
Proof.
intros. apply CC_step_to_step in H. apply CC_step_to_step in H0.
  assert (Z:= cc_step_fun _ _ _ _ H H0).
  destruct q1; destruct q2; inv Z; trivial.
Qed.

Lemma exec_skips_CC:
 forall {s0 k s k'}
   (H1: match_cont (Kseq s0 :: k) (strip_skip' (CC.Kseq s k')))
   ge f ve te m,
   match s0 with Sskip => False | Scontinue => False | Sloop _ _ => False
            | Sifthenelse _ _ _ => False | Sreturn _ => False
            | _ => True end ->
   exists k2, strip_skip' (CC.Kseq s k') = CC.Kseq s0 k2 /\
     corestep_star CC_core_sem ge (CC_core_State f s k' ve te) m
              (CC_core_State f s0 k2 ve te) m.
Proof.
 intros.

 remember (CC.Kseq s k') as k0.
 revert k s k' H1 Heqk0; induction k0; intros; inv Heqk0.
 assert ({s1=Sskip}+{s1<>Sskip}) by (destruct s1; try (left; congruence); right; congruence).
 destruct H0.
subst s1.
      destruct k'; try solve [inv H1].
specialize (IHk0 _ s k' H1 (eq_refl _)).
                   destruct IHk0 as [k2 [? ?]].
                   exists k2. split; simpl; auto.
                   clear - H2. destruct H2 as [n Hn]. exists (S n). simpl.
                     eexists. eexists. split. Focus 2. apply Hn.
                                                          constructor.
inv H1; contradiction.
simpl in H1. inv H1. contradiction.
   replace (strip_skip' (CC.Kseq s1 k')) with (CC.Kseq s1 k') in *
       by (destruct s1; try congruence; auto).
  clear - H H1.
   inv H1. exists k'; split; auto. exists O. reflexivity.
Qed.

Lemma exec_skips'_CC:
  forall ge f s k' s0 k0' ve te m,
        strip_skip' (CC.Kseq s k') = CC.Kseq s0 k0' ->
        corestep_star CC_core_sem ge (CC_core_State f s k' ve te) m
                                   (CC_core_State f s0 k0' ve te) m.
Proof.
 intros.
 destruct (dec_skip s). subst. simpl in *.
 induction k'; try solve [inv H].
 destruct (dec_skip s). subst. simpl in *.
  eapply corestep_star_trans.
             Focus 2. apply IHk'. apply H.
       apply corestep_star_one. simpl. econstructor.
 rewrite strip_skip'_not in * by auto.
 inv H. apply corestep_star_one. simpl. econstructor.
 rewrite strip_skip'_not in H by auto. inv H. exists O. simpl. reflexivity.
Qed.

Lemma strip_skip'_loop1_CC:
  forall ge f ve te m a3 s k1 k, CC.Kloop1 s a3 k1 = strip_skip' k ->
  corestep_star CC_core_sem ge (CC_core_State f Sskip k ve te) m
                                                         (CC_core_State f Sskip (CC.Kloop1 s a3 k1) ve te) m.
Proof.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s0). subst. simpl in H.
     eapply corestep_star_trans; try apply (IHk H).
       apply corestep_star_one. simpl. constructor.
 rewrite strip_skip'_not in * by auto.
 rewrite <- H. apply corestep_star_zero.
 simpl in H. inv H. apply corestep_star_zero.
Qed.

Lemma strip_skip'_call_CC:
  forall ge f ve te m lid f' ve' te' k1 k, CC.Kcall lid f' ve' te' k1 = strip_skip' k ->
  corestep_star CC_core_sem ge (CC_core_State f Sskip k ve te) m
                                                          (CC_core_State f Sskip (CC.Kcall lid f' ve' te' k1) ve te) m.
Proof.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s). subst. simpl in H.
     eapply corestep_star_trans; try apply (IHk H).
       apply corestep_star_one. simpl. constructor.
 rewrite strip_skip'_not in * by auto.
 rewrite <- H. apply corestep_star_zero.
 simpl in H. inv H. apply corestep_star_zero.
Qed.

Lemma step_continue_strip_CC:
  forall ge f k ve te m,
           corestep_star CC_core_sem ge (CC_core_State f Scontinue k ve te) m
               (CC_core_State f Scontinue (strip_skip' k) ve te) m.
Proof.
intros.
induction k; simpl; try apply corestep_star_zero.
destruct (dec_skip s).
   subst.
   eapply corestep_star_trans.
         apply corestep_star_one.
            assert (ZZ: corestep CC_core_sem ge (CC_core_State f Scontinue (CC.Kseq Sskip k) ve te) m (CC_core_State f Scontinue k ve te) m).
                    simpl. apply (CC.step_continue_seq ge function_entry2 f Sskip k ve te m).
            apply ZZ.
         assumption.
destruct s; try congruence; apply corestep_star_zero.
Qed.

Lemma step_continue_seq_CC: forall ge f s k e le m,
       corestep CC_core_sem ge (CC_core_State f Scontinue (CC.Kseq s k) e le) m
                                                      (CC_core_State f Scontinue k e le) m.
  Proof. intros.
    assert (Z:CCstep ge (CC.State f Scontinue (CC.Kseq s k) e le m) Events.E0 (CC.State f Scontinue k e le m) ).
           apply CC.step_continue_seq.
    apply step_to_CC_step in Z.
                     destruct Z as [cc [mm [cc' [mm' [Heq1 [Heq2 Hstep]]]]]].
                         apply CC_core_CC_state_3 in Heq1. apply CC_core_CC_state_3 in Heq2. simpl in *.
                     inv Heq1. inv Heq2. apply Hstep.
                     auto.
  Qed.

Lemma step_continue_switch_CC: forall ge f k e le m,
              corestep CC_core_sem ge (CC_core_State f Scontinue (CC.Kswitch k) e le) m
                                                             (CC_core_State f Scontinue k e le) m.
  Proof. intros.
    assert (Z:CCstep ge (CC.State f Scontinue (CC.Kswitch k) e le m) Events.E0 (CC.State f Scontinue k e le m) ).
           apply CC.step_continue_switch.
    apply step_to_CC_step in Z.
                     destruct Z as [cc [mm [cc' [mm' [Heq1 [Heq2 Hstep]]]]]].
                         apply CC_core_CC_state_3 in Heq1. apply CC_core_CC_state_3 in Heq2. simpl in *.
                     inv Heq1. inv Heq2. apply Hstep.
                     auto.
  Qed.

Lemma break_strip_CC: forall ge f ve te m k,
       corestep_star CC_core_sem ge (CC_core_State f Sbreak k ve te) m
                               (CC_core_State f Sbreak (strip_skip' k) ve te) m.
 Proof. induction k; try solve [apply corestep_star_zero].
    destruct (dec_skip s).
subst. simpl.
         eapply corestep_star_trans; try eassumption. eapply corestep_star_one. constructor.
  rewrite strip_skip'_not; auto. apply corestep_star_zero.
Qed.

Lemma strip_skip'_loop2_CC:
  forall ge f ve te m a3 s k1 k, CC.Kloop2 s a3 k1 = strip_skip' k ->
  corestep_star CC_core_sem ge (CC_core_State f Sskip k ve te) m
                     (CC_core_State f Sskip (CC.Kloop2 s a3 k1) ve te) m.
Proof. intros.
 induction k; intros; try solve [inv H].
 destruct (dec_skip s0).
subst. eapply corestep_star_trans; try apply IHk; auto. apply corestep_star_one. constructor.
rewrite strip_skip'_not in * by auto.
         rewrite <- H. apply corestep_star_zero.

 simpl in H. inv H. apply corestep_star_zero.
Qed.

Lemma Clightnew_Clight_sim_eq_noOrder:
forall p (c1 : corestate) (m : mem) (c1' : corestate) (m' : mem),
corestep cl_core_sem (Genv.globalenv p) c1 m c1' m' ->
forall (c2 : CC_core),
 match_states c1 c2 ->
exists c2' : CC_core,
    corestep_plus CC_core_sem (Genv.globalenv p) c2 m c2' m' /\
    match_states c1' c2'.
Proof.
intros.
forget (Genv.globalenv p) as ge. clear p.
simpl in H.
revert c2 H0. induction H; intros.

Focus 1. inv H4.
simpl strip_skip in H9.
destruct (exec_skips_CC H9 ge f ve te m) as [k2 [? ?]]; auto.
exists (CC_core_State f Sskip k2 ve te); split.
       eapply corestep_star_plus_trans. eassumption.
              eapply corestep_plus_one. econstructor; eauto.
constructor; auto.
rewrite H4 in H9. inv H9; auto.

Focus 1. inv H0.
destruct (exec_skips_CC H5 ge f ve te m) as [k2 [? ?]]; auto.
exists (CC_core_State f Sskip k2 ve (PTree.set id v te)); split.
  eapply corestep_star_plus_trans. eassumption. apply corestep_plus_one. econstructor; eauto.
  rewrite H0 in H5. inv H5; constructor; auto.

Focus 1. inv H7.
 destruct (exec_skips_CC H12 ge f0 ve te m) as [k2 [? ?]]; auto.
 rewrite H7 in *. inv H12. simpl in CUR.
  exists (CC_core_State f (fn_body f) (CC.Kcall optid f0 ve te k2) ve' le').
  split.
eapply corestep_star_plus_trans. apply H8.
               apply corestep_plus_two with (c':=CC_core_Callstate (Internal f) vargs (CC.Kcall optid f0 ve te k2))(m':=m).
                     simpl. econstructor; eauto.
              econstructor; eauto.
simpl. apply list_norepet_app in H4; destruct H4 as [? [? ?]].
             econstructor; eauto. econstructor; eauto.
             apply match_cont_strip. simpl. constructor; auto.

Focus 1. inv H3.
 destruct (exec_skips_CC H8 ge f ve te m) as [k2 [? ?]]; auto.
 rewrite H3 in *. inv H8. simpl in CUR.
  exists (CC_core_Callstate (External ef tyargs tyres) vargs (CC.Kcall optid f ve te k2)).
  split.
eapply corestep_star_plus_trans. eassumption. eapply corestep_plus_one. econstructor; eauto.
econstructor; eauto.

Focus 1.  inv H0.
 destruct (exec_skips_CC H5 ge f ve te m) as [k2 [? ?]]; auto.
 rewrite H0 in *. inv H5.
 destruct (IHcl_step (CC_core_State f s1 (CC.Kseq s2 k2) ve te))
                as [st2 [? ?]]; clear IHcl_step.
 repeat constructor; auto.
 apply match_cont_strip. apply match_cont_strip. auto.
 exists st2; split; auto.
 eapply corestep_star_plus_trans; [ eassumption | ]. simpl.
 apply corestep_plus_trans with (c2:=CC_core_State f s1 (CC.Kseq s2 k2) ve te)(m2:=m).
              apply corestep_plus_one. simpl. econstructor. eassumption.

 Focus 1.  inv H0.
 simpl strip_skip in H5.
 remember (strip_skip k) as k0.
 destruct k0.
 elimtype False; clear - H Heqk0.
 revert H; induction k; intros. inv H.
 forget (a::k) as k'; clear - Heqk0 H.
 remember (State ve te k') as s.
 revert ve te k' Heqs Heqk0; induction H; intros; inv Heqs; simpl in *; try congruence.
 eapply IHcl_step. reflexivity. auto.
 remember (strip_skip' (CC.Kseq s k')) as k0'.
 destruct k0'; inv H5;
  try solve [rewrite <- strip_step in H; rewrite <- Heqk0 in H; inv H].
 assert (s0<>Sskip).
 clear- Heqk0; intro; subst.
 revert Heqk0; induction k; simpl; intros. inv Heqk0. destruct a; try solve [inv Heqk0]; auto. destruct s; inv Heqk0; auto.
 destruct (IHcl_step (CC_core_State f s k' ve te))
                 as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. rewrite <- Heqk0. rewrite <- Heqk0'.
 constructor 2; auto.
 exists st2; split; auto.

  destruct (IHcl_step (CC_core_State f Sskip (CC.Kloop1 s0 s1 k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. simpl. rewrite <- Heqk0. constructor. auto.
  exists st2; split; auto.
  apply corestep_plus_split in H0. destruct H0 as [cc [mm [Hstep Hstar]]].
      eapply corestep_plus_star_trans; try apply Hstar.
          clear - Hstep Heqk0'.
             destruct s; inv Heqk0'.
             eapply corestep_star_plus_trans.
                    apply (strip_skip'_loop1_CC _ _ _ _ _ _ _ _ _ H0).
                    eapply corestep_plus_one. apply Hstep.

 destruct (IHcl_step (CC_core_State f Sskip (CC.Kloop2 s0 s1 k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 destruct (dec_skip s). subst.
 econstructor; eauto. rewrite <- Heqk0. constructor. auto.
 rewrite strip_skip'_not in Heqk0' by auto. inv Heqk0'.
  exists st2; split; auto.
  destruct s; inv Heqk0'.
  eapply corestep_star_plus_trans; try apply H0.
  clear - H4; revert H4; induction k'; intros; inv H4.
  destruct (dec_skip s). subst.
  specialize (IHk' H0).
       eapply corestep_star_trans; try apply IHk'. apply corestep_star_one. constructor.
 replace (CC.Kloop2 s0 s1 k0') with (CC.Kseq s k') by (destruct s; auto; congruence).
    apply corestep_star_zero.
 apply corestep_star_zero.

 destruct s; inv Heqk0'.
 destruct (IHcl_step (CC_core_State f Sskip (CC.Kcall o f0 e t k0') ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. rewrite <- Heqk0. constructor; auto.
  exists st2; split; auto.
  apply corestep_plus_split in H0. destruct H0 as [cc [mm [Hstep Hstar]]].
      eapply corestep_plus_star_trans; try apply Hstar.
          clear - Hstep H2.
             eapply corestep_star_plus_trans.
                    eapply (strip_skip'_call_CC _ _ _ _ _ _ _ _ _ _ _ H2); try apply Hstep.
                    eapply corestep_plus_one. apply Hstep.

 Focus 1.  inv H0.
 simpl strip_skip in H5.
 inv H5.
 Focus 1.  change (CC.Kseq Scontinue k'0 = strip_skip' (CC.Kseq s k')) in H3.
 symmetry in H3.
 rewrite continue_cont_skip in *.
 simpl in CUR.
 rewrite <- current_function_strip in CUR.
 forget (strip_skip k) as k0. clear k. rename k0 into k.

 generalize (continue_cont_is k); case_eq (continue_cont k); intros; try contradiction.
 rewrite H0 in H; inv H.
 destruct c; try contradiction. destruct l; try contradiction. destruct c; try contradiction.
 subst s0.

 assert (X1: corestep_star CC_core_sem ge (CC_core_State f s k' ve te) m
                             (CC_core_State f Scontinue k'0 ve te) m).
     clear - H3.
     destruct (dec_skip s).
subst. simpl in H3.
           eapply exec_skips'_CC; auto.
           rewrite strip_skip'_not in H3 by auto. inv H3. simpl. apply corestep_star_zero.
 assert (X2: corestep_star CC_core_sem ge (CC_core_State f Scontinue k'0 ve te) m
                                       (CC_core_State f Scontinue (strip_skip' k'0) ve te) m).
      clear.
      induction k'0; try solve [apply corestep_star_zero].
      destruct (dec_skip s).
subst. simpl in *.
                            eapply corestep_star_trans; try apply IHk'0. clear IHk'0.
                            apply corestep_star_one. constructor.
           rewrite strip_skip'_not; auto. apply corestep_star_zero.
 generalize (corestep_star_trans _ _ _ _ _ _ _ _ X1 X2); clear X1 X2; intro.
 clear H3.
 forget (strip_skip' k'0) as k0'; clear k'0.
 assert (precontinue_cont k = Kloop1 s1 s2 :: l).
 revert H0; clear; induction k; simpl; try congruence. destruct a; try congruence; auto.
 assert (exists k1',
               corestep_star CC_core_sem ge (CC_core_State f Scontinue k0' ve te) m
                    (CC_core_State f Scontinue k1' ve te) m /\
               match_cont (Kseq Scontinue :: Kloop1 s1 s2 :: l) k1').
     clear - H1 H0.
     revert H0; induction H1; simpl; intros; try congruence.
        destruct IHmatch_cont as [k1' [? ?]].
           rewrite <- continue_cont_skip; auto.
        econstructor. split; [ | eassumption].
           eapply corestep_star_trans; try apply H.
             clear.
             eapply corestep_star_trans.
                 eapply corestep_star_one. apply step_continue_seq_CC.
                 apply step_continue_strip_CC.
      inv H0. econstructor; split. apply corestep_star_zero. constructor. auto.
      destruct IHmatch_cont as [k1' [? ?]].
          rewrite <- continue_cont_skip; auto.
          econstructor. split; [ | eassumption].
             eapply corestep_star_trans; try apply H.
              eapply corestep_star_trans.
                 eapply corestep_star_one. apply step_continue_switch_CC.
                 apply step_continue_strip_CC.
 destruct H4 as [k1' [StepStar Mtch]].
 generalize (corestep_star_trans _ _ _ _ _ _ _ _ H2 StepStar); clear H2 StepStar; intro H2.
 rewrite H0 in *.
 assert (CUR': current_function l = Some f).
   clear - CUR H0. revert CUR H0; induction k; simpl; intros. inv CUR.
   destruct a; try discriminate; auto. inv H0. auto.
 clear H1 CUR k H0 H3.
 inv Mtch.
     inv H4. simpl in *.
    destruct (IHcl_step (CC_core_State f s2 (CC.Kloop2 s1 s2 k'0) ve te))
                      as [st2 [? ?]]; clear IHcl_step.
    constructor; auto. apply match_cont_strip. constructor. auto.
    exists st2; split; auto.
    eapply corestep_star_plus_trans; [apply H2 | ].
    eapply corestep_star_plus_trans; [ | apply H0].
    eapply corestep_star_one. constructor. auto.

Focus 1.
   change (CC.Kloop1 s0 e3 k'0 = strip_skip' (CC.Kseq s k')) in H1.
 destruct (dec_skip s); [ | destruct s; try congruence; inv H1].
 subst s.
 simpl in H.
 simpl in H1.
 simpl in *.
 assert (X1: corestep_star CC_core_sem ge (CC_core_State f Sskip k' ve te) m
                   (CC_core_State f Sskip (CC.Kloop1 s0 e3 k'0) ve te) m).
     rewrite H1; clear.
     induction k'; intros; try solve [apply corestep_star_zero].
     destruct (dec_skip s).
subst. simpl in *. eapply corestep_star_trans; try apply IHk'.
                                        apply corestep_star_one. simpl. econstructor.
rewrite strip_skip'_not; auto. apply corestep_star_zero.
 forget (CC_core_State f Sskip k' ve te) as st1.
 clear k' H1.
 assert (X2: corestep_star CC_core_sem ge st1
                  m (CC_core_State f e3 (CC.Kloop2 s0 e3 k'0) ve te) m).
     eapply corestep_star_trans; try apply X1.
     eapply corestep_star_one. constructor. auto.
 clear X1.
 destruct (IHcl_step (CC_core_State f e3 (CC.Kloop2 s0 e3 k'0) ve te))
                      as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. apply match_cont_strip; constructor; auto.
 exists st2; split; auto.
 eapply corestep_star_plus_trans; eauto.

 Focus 1.
 inv H0. simpl strip_skip in H5.
 destruct (dec_skip s).
      subst. simpl strip_skip' in *.
      assert (exists k1', strip_skip' k' = CC.Kseq Sbreak k1').
           revert H5; clear. remember (strip_skip' k') as k0'.
           revert k' Heqk0'; induction k0'; intros; try solve [inv H5].
           inv H5. eauto.
      destruct H0 as [k1' H0].
      assert (X: corestep_star CC_core_sem ge (CC_core_State f Sskip k' ve te) m
                           (CC_core_State f Sbreak k1' ve te) m).
          revert k1' H0; clear; induction k'; intros; try solve [inv H0].
          destruct (dec_skip s).
subst. simpl in *. specialize (IHk' _ H0).
                  eapply corestep_star_trans; try apply IHk'. apply corestep_star_one. constructor.
rewrite strip_skip'_not in H0 by auto. inv H0.
                          apply corestep_star_one. constructor.
      simpl.
      forget (CC_core_State f Sskip k' ve te) as st1.
      rewrite H0 in *.
      clear k' H0.
      inv H5.
      rewrite <- break_cont_skip in *.
      simpl in CUR. rewrite <- current_function_strip in CUR.
      forget (strip_skip k) as k0.
      assert (Y: corestep_star CC_core_sem ge st1 m (CC_core_State f Sbreak (strip_skip' k1') ve te) m).
          eapply corestep_star_trans; try apply X; auto.
          clear.
          induction k1'; try destruct s; try solve [apply corestep_star_zero].
          simpl. eapply corestep_star_trans; eauto. apply corestep_star_one. constructor.
      forget (strip_skip' k1') as k0'. clear k1' X.

      assert (X: exists k1',
             corestep_plus CC_core_sem ge (CC_core_State f Sbreak k0' ve te) m
                       (CC_core_State f Sskip k1' ve te) m
             /\ match_cont (strip_skip (break_cont k0)) (strip_skip' k1')).
          clear - H H1.
          revert H; induction H1; intros; try solve [inv H].
              rewrite break_cont_skip in *. simpl in H.
              destruct (IHmatch_cont H) as [k1' [? ?]]; clear IHmatch_cont. simpl.
              exists k1'; split; auto.
              eapply corestep_star_plus_trans; try eassumption.
                   eapply corestep_star_trans with (c2:=CC_core_State f Sbreak k' ve te)(m2:=m).
                        apply corestep_star_one. simpl. constructor.
                        apply break_strip_CC.
simpl in *. exists k'; split.
               apply corestep_plus_one. simpl. eapply CC.step_break_loop1.
                auto.
simpl in *. exists k'; split.
                eapply corestep_plus_one. simpl. eapply CC.step_skip_break_switch. auto.
                assumption.
       destruct X as [k1' [? ?]].
       destruct (IHcl_step (CC_core_State f Sskip k1' ve te))
                      as [st2 [? ?]]; clear IHcl_step.
         constructor; auto.
            clear - H CUR. revert CUR; induction k0; intros. inv CUR.
            destruct a; simpl in *; auto. inv H. inv H.
       exists st2; split; auto.
       eapply corestep_star_plus_trans; try apply Y.
       eapply corestep_plus_trans. apply H0. apply H3.
     rewrite strip_skip'_not in H5 by auto.
     inv H5. clear n.
     admit.
 Focus 1.  inv H1. simpl strip_skip in H6.
 inv H6.
 change (CC.Kseq (Sifthenelse a s1 s2) k'0 = strip_skip' (CC.Kseq s k')) in H4.
 assert (X: corestep_star CC_core_sem ge (CC_core_State f s k' ve te) m (CC_core_State f (Sifthenelse a s1 s2) k'0 ve te) m).
     clear - H4.
     revert H4; induction k'; intros; try solve [ destruct s; inv H4; apply corestep_star_zero].
     destruct (dec_skip s).
subst s.
          destruct (dec_skip s0).
subst s0. simpl in *.
               eapply corestep_star_trans; try apply IHk'; eauto. apply corestep_star_one. constructor.
change (strip_skip' (CC.Kseq Sskip (CC.Kseq s0 k'))) with
               (strip_skip' (CC.Kseq s0 k')) in H4.
               rewrite strip_skip'_not in H4 by auto.
               inv H4. apply corestep_star_one. constructor.
rewrite strip_skip'_not in * by auto.
          inv H4. apply corestep_star_zero.
 exists (CC_core_State f (if b then s1 else s2) k'0 ve te); split; auto.
   eapply corestep_star_plus_trans; try apply X.
      apply corestep_plus_one. econstructor; eauto.
 constructor; auto. apply match_cont_strip; auto.

 Focus 1.  inv H0. inv H4.
 change (CC.Kseq (Sloop s1 s2) k'0 = strip_skip' (CC.Kseq s k')) in H2.
  generalize (exec_skips'_CC ge f _ _ _ _ ve te m (@eq_sym _ _ _ H2)); intro.
 exists ( (CC_core_State f s1 (CC.Kloop1 s1 s2 k'0) ve te)); split.
 eapply corestep_star_plus_trans; try apply H.
  apply corestep_plus_one. simpl. eapply CC.step_loop; eauto.
constructor; auto. apply match_cont_strip; constructor; auto.

 Focus 1.   inv H0. inv H4.
 destruct s0; inv H3.
 generalize (strip_skip'_loop2_CC ge f ve te m _ _ _ _ H1); intro.
 exists (CC_core_State f s (CC.Kloop1 s a3 k'0) ve te); split.
 eapply corestep_star_plus_trans; try apply H.
 eapply corestep_plus_star_trans with (c2:=CC_core_State f (Sloop s a3) k'0 ve te)(m2:=m).
 apply corestep_plus_one. simpl. eapply CC.step_skip_loop2; eauto.
 apply corestep_star_one. simpl. eapply CC.step_loop; eauto.
  constructor; auto. apply match_cont_strip. constructor. auto.

 Focus 1.  inv H3.
  remember (strip_skip' (CC.Kseq s k'0)) as k3. simpl in CUR, H8.
 inv H8.
 generalize (exec_skips'_CC ge f0 _ _ _ _ ve te m (@eq_sym _ _ _ H4)); intro H99.
 assert (f0=f).
   simpl in CUR; clear - CUR H.
   revert H CUR; induction k; intros. inv H. simpl in *. destruct a; auto. inv CUR; auto. inv H; auto.
 subst f.
 generalize (match_cont_call_strip k k'1); intro.
 spec H3; [congruence |]. spec H3; [auto |].
 generalize H3; rewrite H; intro.
 inv H5.
elimtype False; clear - H10.
         revert H10; induction k'1; simpl; intros; congruence.
destruct optexp; [destruct H1 as [v [? ?]] | ]; (destruct optid; destruct H2 as [H2 H2'];
               try solve [contradiction H2; auto]; subst te'' );
               try (eapply corestep_star_trans; split; [eapply corestep_star_plus_trans; [ apply H99 | eapply corestep_plus_two ] | ]).
                eexists (CC_core_State f Sskip k'2 ve' (PTree.set i v' te')).
                split.
                     eapply (corestep_star_plus_trans _ _ _ _ _ _ _ _ H99).                           eapply corestep_plus_trans with (c2:=CC_core_Returnstate v' (CC.call_cont k'1))(m2:=m').
                                         eapply corestep_plus_one. simpl. econstructor; eauto.
                                         eapply corestep_plus_one. simpl. rewrite <- H13. eapply CC.step_returnstate.
                    constructor; auto.
                eexists (CC_core_State f Sskip k'2 ve' te').
                split.
                     eapply (corestep_star_plus_trans _ _ _ _ _ _ _ _ H99).                           eapply corestep_plus_trans with (c2:=CC_core_Returnstate v' (CC.call_cont k'1))(m2:=m').
                                         eapply corestep_plus_one. simpl. econstructor; eauto.
                                         eapply corestep_plus_one. simpl. rewrite <- H13. eapply CC.step_returnstate.
                    constructor; auto.
                eexists (CC_core_State f Sskip k'2 ve' te').
                split.
                     eapply (corestep_star_plus_trans _ _ _ _ _ _ _ _ H99).                           eapply corestep_plus_trans with (c2:=CC_core_Returnstate Vundef (CC.call_cont k'1))(m2:=m').
                                         eapply corestep_plus_one. simpl. econstructor; eauto.
                                         eapply corestep_plus_one. simpl. rewrite <- H13. eapply CC.step_returnstate.
                    constructor; auto.

 destruct optid. destruct H2. congruence.
 destruct H2; subst te''.
 simpl in H. inv H. simpl in CUR. symmetry in CUR; inv CUR.
 destruct s; inv H4.
 assert (corestep_star CC_core_sem ge (CC_core_State f Sskip k'0 ve te) m
                         (CC_core_State f Sskip (CC.Kcall None f1 ve' te' k'1) ve te) m).
     clear H1; rename H3 into H1.
     clear - H1.
     revert H1; induction k'0; intros; try solve [inv H1].
           destruct (dec_skip s).
subst s. simpl in H1.
               eapply corestep_star_trans; try apply IHk'0; auto. apply corestep_star_one. constructor; auto.
              rewrite strip_skip'_not in H1 by auto. rewrite <- H1. apply corestep_star_zero.
          simpl in H1. inv H1. apply corestep_star_zero.
 eexists (CC_core_State f1 Sskip k'1 ve' te').
     split. eapply corestep_star_plus_trans. apply H. clear H.
              eapply corestep_plus_trans with (c2:=CC_core_Returnstate Vundef (CC.Kcall None f1 ve' te' k'1))(m2:=m').
                  eapply corestep_plus_one. simpl. eapply CC.step_skip_call; simpl; eauto.
                  eapply corestep_plus_one. simpl. econstructor; eauto.
     econstructor; eauto.

 Focus 1.  inv H0. simpl strip_skip in H5.
 remember (CC.Kseq s k') as k0'.
 inv H5.
 evar (c2': CC_core).
 exists c2'; split.
     Focus 2. constructor; eauto. apply match_cont_strip. simpl.
                    instantiate (1:= CC.Kswitch k'0). constructor. auto.
     generalize (exec_skips'_CC ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
        eapply corestep_star_plus_trans; try apply H99.
        unfold c2'. apply corestep_plus_one. simpl. constructor; auto.

 Focus 1.  inv H0. remember (CC.Kseq s0 k') as k0'. inv H5.
 destruct (IHcl_step (CC_core_State f s k'0 ve te)) as [st2 [? ?]]; clear IHcl_step.
 constructor; auto. apply match_cont_strip. auto.
 exists st2; split; auto.
   eapply corestep_star_plus_trans; try eassumption.
   generalize (exec_skips'_CC ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
     eapply corestep_star_trans; try apply H99.
     apply corestep_star_one. constructor.

 Focus 1.  inv H0. remember (CC.Kseq s k'0) as k0'. inv H5.
  generalize (match_cont_call_strip k k'1); intro.
 spec H0.
 clear - CUR. apply (call_cont_nonnil _ _ CUR).
 specialize (H0 H1).
  rewrite <- strip_call' in H0.
 change (Kseq (Sreturn None) :: call_cont k) with (strip_skip (Kseq (Sreturn None) :: call_cont k)) in H0.
 destruct (match_find_label _ _ _ _ _ H0 H) as [s2 [k2' [? ?]]].
 exists (CC_core_State f s2 k2' ve te); split.
    simpl in CUR0. inversion2 CUR CUR0.
     generalize (exec_skips'_CC ge f _ _ _ _ ve te m (@eq_sym _ _ _ H3)); intro H99.
     eapply corestep_star_plus_trans; try apply H99.
         apply corestep_plus_one. constructor; auto.
         constructor; auto.
   clear - CUR H. forget (fn_body f) as s.
       rewrite <- current_function_call_cont in CUR.
       change (current_function (Kseq (Sreturn None) :: call_cont k) = Some f) in CUR.
        forget (Kseq (Sreturn None) :: call_cont k) as k0. clear - CUR H.
        eapply current_function_find_label; eauto.
 apply match_cont_strip1. auto.
Qed.

Definition MS (_:corestate)(c: corestate) (C: CC_core): Prop := match_states c C.

Lemma Clightnew_Clight_sim_eq: forall p ExternIdents entrypoints
               (ext_ok : CompilerCorrectness.entryPts_ok p p ExternIdents entrypoints)
,
              Forward_simulation_eq.Forward_simulation_equals _ _ _ cl_core_sem CC_core_sem (Genv.globalenv p) (Genv.globalenv p) entrypoints.
Proof.
  intros.
  pose (bogus_measure := (fun x: corestate => O)).
  eapply eq_simulation_plus with (match_cores:=MS); try apply bogus_measure; unfold MS.
      intros. unfold cl_core_sem, CC_core_sem; simpl.
      unfold cl_initial_core, CC_initial_core; simpl.
     eexists. eexists. split. reflexivity. split. reflexivity.
       assert (v1=v2). unfold CompilerCorrectness.entryPts_ok in ext_ok. admit.        subst.
       econstructor. simpl. admit.
       simpl. assert (myStatement = Sskip). admit.
          rewrite H1. econstructor. simpl. constructor. simpl. constructor.
      intros. unfold cl_core_sem in H0. simpl in H0. unfold cl_safely_halted in H0. inv H0.
     intros. inv H. simpl in *. inv H2. simpl in *. inv H0.
          split. unfold CC_at_external. destruct tyres;auto.
          admit.          intros. inv H; simpl in *.
          admit. admit.
  Qed.

Require Import sepcomp.forward_simulations.

Theorem Clightnew_Clight_sim: forall p ExternIdents entrypoints
         (ext_ok: CompilerCorrectness.entryPts_ok p p ExternIdents entrypoints)
        (IniHyp: forall x, Genv.init_mem p = Some x <-> initial_mem CC_core_sem (Genv.globalenv p) x p.(prog_defs)),
        CompilerCorrectness.core_correctness
             (fun F C V Sem P => (forall x, Genv.init_mem P = Some x <-> initial_mem Sem (Genv.globalenv P) x P.(prog_defs)))
              ExternIdents _ _ _ _ _ _ cl_core_sem CC_core_sem p p.
Proof.
intros.
econstructor.
  simpl. intros. exists m1; auto.
  apply ext_ok.
  eapply Clightnew_Clight_sim_eq; eauto.
  trivial.
  unfold CompilerCorrectness.GenvHyp; auto.
  apply IniHyp.
  apply IniHyp.
Qed.