Module ControlFlowGraphFlatteningproof

Require Import Clight.
Require Import AST.
Require Import Integers.
Require Import Ctypes.
Require Import Maps.
Require Import Cop.
Require Import Coqlib.
Require Import Smallstep.
Require Import Errors.
Require Import Globalenvs.
Require Import Values.
Require Import Memory.
Require Import Events.

Require Import ControlFlowGraphFlattening.
Open Scope error_monad_scope.


Definition tint := Tint I32 Unsigned noattr.

Section Utils.

Variable phi: Z -> Int.int.

Inductive not_in_expr (id: ident): expr -> Prop :=
  | not_in_int:
      forall i t,
        not_in_expr id (Econst_int i t)
  | not_in_float:
      forall f t,
        not_in_expr id (Econst_float f t)
  | not_in_single:
      forall s t,
        not_in_expr id (Econst_single s t)
  | not_in_long:
      forall l t,
        not_in_expr id (Econst_long l t)
  | not_in_var:
      forall v t,
        id <> v ->
        not_in_expr id (Evar v t)
  | not_in_tempvar:
      forall v t,
        id <> v ->
        not_in_expr id (Etempvar v t)
  | not_in_deref:
      forall e t,
      not_in_expr id e ->
      not_in_expr id (Ederef e t)
  | not_in_addrof:
      forall e t,
      not_in_expr id e ->
      not_in_expr id (Eaddrof e t)
  | not_in_unop:
      forall op e t,
      not_in_expr id e ->
      not_in_expr id (Eunop op e t)
  | not_in_binop:
      forall op e1 e2 t,
      not_in_expr id e1 ->
      not_in_expr id e2 ->
      not_in_expr id (Ebinop op e1 e2 t)
  | not_in_cast:
      forall e t,
        not_in_expr id e ->
        not_in_expr id (Ecast e t)
  | not_in_field:
      forall e f t,
        not_in_expr id e ->
        id <> f ->
        not_in_expr id (Efield e f t)
  | not_in_sizeof:
      forall t1 t2,
        not_in_expr id (Esizeof t1 t2)
  | not_in_alignof:
      forall t1 t2,
        not_in_expr id (Ealignof t1 t2).

Inductive not_in_stmt (id: ident): statement -> Prop :=
  | not_in_skip: not_in_stmt id Sskip
  | not_in_assign:
      forall e1 e2,
        not_in_expr id e1 ->
        not_in_expr id e2 ->
        not_in_stmt id (Sassign e1 e2)
  | not_in_set:
      forall i e,
        i <> id ->
        not_in_expr id e ->
        not_in_stmt id (Sset i e)
  | not_in_call_some:
      forall v e el,
        v <> id ->
        not_in_expr id e ->
        (forall e', In e' el -> not_in_expr id e') ->
        not_in_stmt id (Scall (Some v) e el)
  | not_in_call_none:
      forall e el,
        not_in_expr id e ->
        (forall e', In e' el -> not_in_expr id e') ->
        not_in_stmt id (Scall None e el)
  | not_in_builtin_some:
      forall v ef tl el,
        v <> id ->
        (forall e, In e el -> not_in_expr id e) ->
        not_in_stmt id (Sbuiltin (Some v) ef tl el)
  | not_in_builtin_none:
      forall ef tl el,
        (forall e, In e el -> not_in_expr id e) ->
        not_in_stmt id (Sbuiltin None ef tl el)
  | not_in_sequence:
      forall s1 s2,
        not_in_stmt id s1 ->
        not_in_stmt id s2 ->
        not_in_stmt id (Ssequence s1 s2)
  | not_in_ifthenelse:
      forall e s1 s2,
        not_in_expr id e ->
        not_in_stmt id s1 ->
        not_in_stmt id s2 ->
        not_in_stmt id (Sifthenelse e s1 s2)
  | not_in_loop:
      forall s1 s2,
        not_in_stmt id s1 ->
        not_in_stmt id s2 ->
        not_in_stmt id (Sloop s1 s2)
  | not_in_break:
      not_in_stmt id Sbreak
  | not_in_continue:
      not_in_stmt id Scontinue
  | not_in_return_some:
      forall e,
        not_in_expr id e ->
        not_in_stmt id (Sreturn (Some e))
  | not_in_return_none:
      not_in_stmt id (Sreturn None)
  | not_in_switch:
      forall e ls,
        not_in_expr id e ->
        not_in_lstmt id ls ->
        not_in_stmt id (Sswitch e ls)
  | not_in_label:
      forall l s,
        not_in_stmt id s ->
        not_in_stmt id (Slabel l s)
  | not_in_goto_some:
      forall l,
      not_in_stmt id (Sgoto l)
with not_in_lstmt (id: ident): labeled_statements -> Prop :=
     | not_in_nil:
         not_in_lstmt id LSnil
     | not_in_cons:
         forall l s ls,
           not_in_stmt id s ->
           not_in_lstmt id ls ->
           not_in_lstmt id (LScons l s ls).

Lemma ple_max_ident:
  forall e id,
    Ple id (max_ident_in_expr e id).

Lemma max_ident_in_expr_monotone:
  forall e id1 id2,
    Ple id1 id2 ->
    Ple (max_ident_in_expr e id1) (max_ident_in_expr e id2).

Lemma ple_fold_max_ident:
  forall l i,
    Ple i (fold_right max_ident_in_expr i l).

Lemma max_ident_in_expr_fold_monotone:
  forall l id1 id2,
    Ple id1 id2 ->
    Ple (fold_right max_ident_in_expr id1 l) (fold_right max_ident_in_expr id2 l).

Theorem not_in_expr_trans:
  forall e id,
    Plt (max_ident_in_expr e 1%positive) id ->
    not_in_expr id e.

Theorem not_in_expr_trans_fold:
  forall l i id,
    Plt (fold_right max_ident_in_expr i l) id ->
    forall e, In e l -> not_in_expr id e.

Lemma ple_max_ident_stmt:
  forall s id,
    Ple id (max_ident_in_stmt s id)
with ple_max_ident_lstmt:
       forall ls id,
         Ple id (max_ident_in_lstmt ls id).

Lemma max_ident_in_stmt_monotone:
  forall s id1 id2,
    Ple id1 id2 ->
    Ple (max_ident_in_stmt s id1) (max_ident_in_stmt s id2)
with max_ident_in_lstmt_monotone:
       forall ls id1 id2,
         Ple id1 id2 ->
         Ple (max_ident_in_lstmt ls id1) (max_ident_in_lstmt ls id2).

Theorem max_ident_not_in_stmt:
  forall s id,
    Plt (max_ident_in_stmt s 1%positive) id ->
    not_in_stmt id s
with max_ident_not_in_lstmt:
       forall ls id,
         Plt (max_ident_in_lstmt ls 1%positive) id ->
         not_in_lstmt id ls.

Lemma find_label_not_in:
  forall s k s' k' lbl id,
    not_in_stmt id s ->
    find_label lbl s k = Some (s', k') ->
    not_in_stmt id s'
with find_label_ls_not_in:
       forall ls k s' k' lbl id,
         not_in_lstmt id ls ->
         find_label_ls lbl ls k = Some (s', k') ->
         not_in_stmt id s'.

Lemma max_list_is_max:
  forall l x,
    In x l -> Ple x (fold_right (fun x y => if plt x y then y else x) (1%positive) l).

Theorem new_ident_not_in_body:
  forall f,
    not_in_stmt (new_ident_for_function f) (fn_body f).

Theorem new_ident_no_repet:
  forall f x,
    In x (var_names (fn_vars f) ++ var_names (fn_params f) ++ var_names (fn_temps f)) -> Plt x (new_ident_for_function f).

Inductive not_in_cont (id: ident): cont -> Prop :=
| not_in_Kstop: not_in_cont id Kstop
| not_in_Kseq: forall s k,
                not_in_stmt id s ->
                not_in_cont id k ->
                not_in_cont id (Kseq s k)
| not_in_Kloop1: forall s1 s2 k,
                  not_in_stmt id s1 ->
                  not_in_stmt id s2 ->
                  not_in_cont id k ->
                  not_in_cont id (Kloop1 s1 s2 k)
| not_in_Kloop2: forall s1 s2 k,
                  not_in_stmt id s1 ->
                  not_in_stmt id s2 ->
                  not_in_cont id k ->
                  not_in_cont id (Kloop2 s1 s2 k)
| not_in_Kswitch: forall k,
                   not_in_cont id k ->
                   not_in_cont id (Kswitch k)
| not_in_Kcall_some: forall f e le k id',
                       id' <> new_ident_for_function f ->
                       not_in_cont (new_ident_for_function f) k ->
                       not_in_cont id (Kcall (Some id') f e le k)
| not_in_Kcall_none: forall f e le k,
                       not_in_cont (new_ident_for_function f) k ->
                       not_in_cont id (Kcall None f e le k).

Theorem not_in_cont_call_cont:
  forall id k,
    not_in_cont id k ->
    forall id', not_in_cont id' (call_cont k).

Lemma sizeof_stmt_pos:
  forall s, sizeof_stmt s > 0.

Inductive no_switch_label_goto_in_stmt: statement -> Prop :=
| no_switch_label_goto_in_skip: no_switch_label_goto_in_stmt Sskip
| no_switch_label_goto_in_assign: forall e1 e2, no_switch_label_goto_in_stmt (Sassign e1 e2)
| no_switch_label_goto_in_set: forall id e, no_switch_label_goto_in_stmt (Sset id e)
| no_switch_label_goto_in_call: forall optid f args, no_switch_label_goto_in_stmt (Scall optid f args)
| no_switch_label_goto_in_builtin: forall optid ef tyl args, no_switch_label_goto_in_stmt (Sbuiltin optid ef tyl args)
| no_switch_label_goto_in_sequence: forall s1 s2, no_switch_label_goto_in_stmt s1 -> no_switch_label_goto_in_stmt s2 -> no_switch_label_goto_in_stmt (Ssequence s1 s2)
| no_switch_label_goto_in_ifthenelse: forall e s1 s2, no_switch_label_goto_in_stmt s1 -> no_switch_label_goto_in_stmt s2 -> no_switch_label_goto_in_stmt (Sifthenelse e s1 s2)
| no_switch_label_goto_in_loop: forall s1 s2, no_switch_label_goto_in_stmt s1 -> no_switch_label_goto_in_stmt s2 -> no_switch_label_goto_in_stmt (Sloop s1 s2)
| no_switch_label_goto_in_break: no_switch_label_goto_in_stmt Sbreak
| no_switch_label_goto_in_continue: no_switch_label_goto_in_stmt Scontinue
| no_switch_label_goto_in_return: forall e, no_switch_label_goto_in_stmt (Sreturn e).

Lemma no_switch_label_goto_loop1:
  forall id_t s counter k to_continue to_break ls,
    flatten_loop1 phi id_t s counter k to_continue to_break = OK ls ->
    no_switch_label_goto_in_stmt s
with no_switch_label_goto_loop2:
       forall id_t s counter k to_break ls,
         flatten_loop2 phi id_t s counter k to_break = OK ls ->
         no_switch_label_goto_in_stmt s.

Lemma no_switch_label_goto_stmt:
  forall id_t s counter k ls,
    flatten phi id_t s counter k = OK ls ->
    no_switch_label_goto_in_stmt s.

Lemma no_switch_label_goto_body:
  forall id_t s s',
    obf_body phi id_t s = OK s' ->
    no_switch_label_goto_in_stmt s.

Theorem no_switch_label_goto_function:
  forall f f',
    transf_function phi f = OK f' ->
    no_switch_label_goto_in_stmt (fn_body f).

Inductive no_switch_label_goto_in_cont: cont -> Prop :=
| no_switch_label_goto_in_stop: no_switch_label_goto_in_cont Kstop
| no_switch_label_goto_in_seq: forall s k, no_switch_label_goto_in_stmt s -> no_switch_label_goto_in_cont k -> no_switch_label_goto_in_cont (Kseq s k)
| no_switch_label_goto_in_loop1: forall s1 s2 k, no_switch_label_goto_in_stmt s1 -> no_switch_label_goto_in_stmt s2 -> no_switch_label_goto_in_cont k -> no_switch_label_goto_in_cont (Kloop1 s1 s2 k)
| no_switch_label_goto_in_loop2: forall s1 s2 k, no_switch_label_goto_in_stmt s1 -> no_switch_label_goto_in_stmt s2 -> no_switch_label_goto_in_cont k -> no_switch_label_goto_in_cont (Kloop2 s1 s2 k)
| no_switch_label_goto_in_Kcall: forall optid f e le k, no_switch_label_goto_in_stmt (fn_body f) -> no_switch_label_goto_in_cont k -> no_switch_label_goto_in_cont (Kcall optid f e le k).

End Utils.

Section PRESERVATION.

Variable phi: Z -> Int.int.

Variable phi_injective:
  forall x y,
    0 <= x <= Int.max_unsigned ->
    0 <= y <= Int.max_unsigned ->
    phi x = phi y ->
    x = y.

Variable prog: Clight.program.
Variable tprog: Clight.program.
Hypothesis TRANSF: transf_program phi prog = OK tprog.
Let ge := Clight.globalenv prog.
Let tge := Clight.globalenv tprog.

Lemma comp_env_preserved:
  Clight.genv_cenv tge = Clight.genv_cenv ge.

Lemma transf_programs:
  AST.transform_partial_program (transf_fundef phi) (program_of_program prog) = OK (program_of_program tprog).

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.

Lemma functions_translated:
  forall (v: val) (f: Clight.fundef),
    Genv.find_funct ge v = Some f ->
    exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef phi f = OK tf.

Lemma function_ptr_translated:
  forall (b: block) (f: Clight.fundef),
    Genv.find_funct_ptr ge b = Some f ->
    exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef phi f = OK tf.

Lemma type_of_fundef_preserved:
  forall fd tfd,
    transf_fundef phi fd = OK tfd -> type_of_fundef tfd = type_of_fundef fd.

Section EXPR_PRESERVATION.


Variable (id: ident).
Variable (e: env).
Variables (le tle: temp_env).
Variable (m: mem).
Hypothesis LENV: forall id', id' <> id -> le!id' = tle!id'.

Theorem eval_expr_preserved:
  forall a v,
    eval_expr ge e le m a v ->
    not_in_expr id a ->
    eval_expr tge e tle m a v
with eval_lvalue_preserved:
       forall a loc ofs,
         eval_lvalue ge e le m a loc ofs ->
         not_in_expr id a ->
         eval_lvalue tge e tle m a loc ofs.

Theorem eval_exprlist_preserved:
  forall al tyl v,
    eval_exprlist ge e le m al tyl v ->
    (forall a, In a al -> not_in_expr id a) ->
    eval_exprlist tge e tle m al tyl v.

End EXPR_PRESERVATION.

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

Inductive match_stmt_cont_in_loop1: statement -> labeled_statements -> (ident * type) -> list Z -> Z -> Z -> list Z -> list Z -> cont -> Prop :=
| match_skip_cont_seq_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' s k,
                                  (exists s1 s2 k', context (Kseq s k) = Kloop1 s1 s2 k') ->
                                  0 < n <= Int.max_unsigned ->
                                  (select_switch_case (Int.unsigned (phi n)) ls =
                                   Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                   exists m, match_stmt_cont_in_loop1 s ls id_t start next_instr m to_continue to_break k) \/
                                  match_stmt_cont_in_loop1 s ls id_t start n next_instr to_continue to_break k ->
                                  match_stmt_cont_in_loop1 Sskip ls id_t start n next_instr to_continue to_break (Kseq s k)
| match_skip_cont_loop1_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' s1 s2 k,
                                    0 < n <= Int.max_unsigned ->
                                    (select_switch_case (Int.unsigned (phi n)) ls =
                                     Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                     exists m, match_stmt_cont_in_loop2 s2 ls id_t start next_instr m to_continue to_break (Kloop2 s1 s2 k)) \/
                                    match_stmt_cont_in_loop2 s2 ls id_t start n next_instr to_continue to_break (Kloop2 s1 s2 k) ->
                                    match_stmt_cont_in_loop1 Sskip ls id_t start n next_instr to_continue to_break (Kloop1 s1 s2 k)
| match_assign_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' e1 e2 k,
                                (exists s1 s2 k', context k = Kloop1 s1 s2 k') ->
                                0 < n <= Int.max_unsigned ->
                                select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sassign e1 e2) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                (exists m, match_stmt_cont_in_loop1 Sskip ls id_t start next_instr m to_continue to_break k) ->
                                match_stmt_cont_in_loop1 (Sassign e1 e2) ls id_t start n next_instr to_continue to_break k
| match_set_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' id e k,
                             (exists s1 s2 k', context k = Kloop1 s1 s2 k') ->
                             0 < n <= Int.max_unsigned ->
                             select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset id e) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                             (exists m, match_stmt_cont_in_loop1 Sskip ls id_t start next_instr m to_continue to_break k) ->
                             match_stmt_cont_in_loop1 (Sset id e) ls id_t start n next_instr to_continue to_break k
| match_call_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' optid a al k,
                              (exists s1 s2 k', context k = Kloop1 s1 s2 k') ->
                              0 < n <= Int.max_unsigned ->
                              select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Scall optid a al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                              (exists m, match_stmt_cont_in_loop1 Sskip ls id_t start next_instr m to_continue to_break k) ->
                              match_stmt_cont_in_loop1 (Scall optid a al) ls id_t start n next_instr to_continue to_break k
| match_builtin_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' optid ef tyargs al k,
                                 (exists s1 s2 k', context k = Kloop1 s1 s2 k') ->
                                 0 < n <= Int.max_unsigned ->
                                 select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sbuiltin optid ef tyargs al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                 (exists m, match_stmt_cont_in_loop1 Sskip ls id_t start next_instr m to_continue to_break k) ->
                                 match_stmt_cont_in_loop1 (Sbuiltin optid ef tyargs al) ls id_t start n next_instr to_continue to_break k
| match_sequence_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break s1 s2 k,
                                  (exists s s' k', context k = Kloop1 s s' k') ->
                                  0 < n <= Int.max_unsigned ->
                                  match_stmt_cont_in_loop1 s1 ls id_t start (n) (n + sizeof_stmt s1) to_continue to_break (Kseq s2 k) ->
                                  match_stmt_cont_in_loop1 s2 ls id_t start (n + sizeof_stmt s1) next_instr to_continue to_break k ->
                                  match_stmt_cont_in_loop1 (Ssequence s1 s2) ls id_t start n next_instr to_continue to_break k
| match_ifthenelse_cont_in_loop1: forall start id_t ls ls' n next_instr to_continue to_break b s1 s2 k,
                                    (exists s s' k', context k = Kloop1 s s' k') ->
                                    0 < n <= Int.max_unsigned ->
                                    select_switch_case (Int.unsigned (phi n)) ls =
                                    Some (LScons (Some (Int.unsigned (phi n))) (Sifthenelse b (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1 + sizeof_stmt s1)) (snd id_t))) Sbreak)) ls') ->
                                    match_stmt_cont_in_loop1 s1 ls id_t start (n + 1) next_instr to_continue to_break k ->
                                    match_stmt_cont_in_loop1 s2 ls id_t start (n + 1 + sizeof_stmt s1) next_instr to_continue to_break k ->
                                    match_stmt_cont_in_loop1 (Sifthenelse b s1 s2) ls id_t start n next_instr to_continue to_break k
| match_loop_cont_in_loop1: forall start id_t ls ls' n next_instr to_continue to_break s1 s2 k,
                              (exists s s' k', context k = Kloop1 s s' k') ->
                              0 < n <= Int.max_unsigned ->
                              select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) ls') ->
                              match_stmt_cont_in_loop1 s1 ls id_t (n::start) (n + 1) (n + 1 + sizeof_stmt s1) ((n + 1 + sizeof_stmt s1)::to_continue) (next_instr::to_break) (Kloop1 s1 s2 k) ->
                              match_stmt_cont_in_loop2 s2 ls id_t (n::start) (n + 1 + sizeof_stmt s1) n ((n + 1 + sizeof_stmt s1)::to_continue) (next_instr::to_break) (Kloop2 s1 s2 k) ->
                              match_stmt_cont_in_loop1 (Sloop s1 s2) ls id_t start n next_instr to_continue to_break k
| match_break_cont_seq_in_loop1: forall start id_t ls n next_instr to_continue to_break s k,
                                   (exists s1 s2 k', context (Kseq s k) = Kloop1 s1 s2 k') ->
                                   match_stmt_cont_in_loop1 Sbreak ls id_t start n next_instr to_continue to_break k ->
                                   match_stmt_cont_in_loop1 Sbreak ls id_t start n next_instr to_continue to_break (Kseq s k)
| match_break_cont_loop1_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' s1 s2 k start' p q,
                                    0 < n <= Int.max_unsigned ->
                                    select_switch_case (Int.unsigned (phi n)) ls =
                                    Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_break) (snd id_t))) Sbreak) ls') ->
                                    ((is_call_cont (context k) /\ exists m, match_stmt_cont Sskip ls id_t to_break m k /\ start' = nil /\ p = nil /\ q = nil) \/
                                    (exists s s' k', context k = Kloop1 s s' k' /\ exists m, match_stmt_cont_in_loop1 Sskip ls id_t start' to_break m p q k) \/
                                    (exists s s' k', context k = Kloop2 s s' k' /\ exists m, match_stmt_cont_in_loop2 Sskip ls id_t start' to_break m p q k)) ->
                                    match_stmt_cont_in_loop1 Sbreak ls id_t (start::start') n next_instr (to_continue::p) (to_break::q) (Kloop1 s1 s2 k)
| match_continue_cont_seq_in_loop1: forall start id_t ls n next_instr to_continue to_break s k,
                                      (exists s1 s2 k', context (Kseq s k) = Kloop1 s1 s2 k') ->
                                      match_stmt_cont_in_loop1 Scontinue ls id_t start n next_instr to_continue to_break k ->
                                      match_stmt_cont_in_loop1 Scontinue ls id_t start n next_instr to_continue to_break (Kseq s k)
| match_continue_cont_loop1_in_loop1: forall start id_t ls n next_instr to_continue to_continue' to_break ls' s1 s2 k,
                                        0 < n <= Int.max_unsigned ->
                                        select_switch_case (Int.unsigned (phi n)) ls =
                                        Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_continue) (snd id_t))) Sbreak) ls') ->
                                        (exists m, match_stmt_cont_in_loop2 s2 ls id_t start to_continue m (to_continue::to_continue') to_break (Kloop2 s1 s2 k)) ->
                                        match_stmt_cont_in_loop1 Scontinue ls id_t start n next_instr (to_continue::to_continue') to_break (Kloop1 s1 s2 k)
| match_return_cont_in_loop1: forall start id_t ls n next_instr to_continue to_break ls' v k,
                                (exists s1 s2 k', context k = Kloop1 s1 s2 k') ->
                                0 < n <= Int.max_unsigned ->
                                select_switch_case (Int.unsigned (phi n)) ls =
                                Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sreturn v) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                match_stmt_cont_in_loop1 (Sreturn v) ls id_t start n next_instr to_continue to_break k
with match_stmt_cont_in_loop2: statement -> labeled_statements -> ident * type -> list Z -> Z -> Z -> list Z -> list Z -> cont -> Prop :=
| match_skip_cont_seq_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' s k,
                                  (exists s1 s2 k', context (Kseq s k) = Kloop2 s1 s2 k') ->
                                  0 < n <= Int.max_unsigned ->
                                  (select_switch_case (Int.unsigned (phi n)) ls =
                                   Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                   exists m, match_stmt_cont_in_loop2 s ls id_t start next_instr m to_continue to_break k) \/
                                  match_stmt_cont_in_loop2 s ls id_t start n next_instr to_continue to_break k ->
                                  match_stmt_cont_in_loop2 Sskip ls id_t start n next_instr to_continue to_break (Kseq s k)
| match_skip_cont_loop2_in_loop2: forall start start' id_t ls n next_instr to_continue to_break ls' s1 s2 k,
                                    0 < n <= Int.max_unsigned ->
                                    (select_switch_case (Int.unsigned (phi n)) ls =
                                     Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                     next_instr = start /\
                                     (exists ls'',
                                        select_switch_case (Int.unsigned (phi next_instr)) ls =
                                        Some (LScons (Some (Int.unsigned (phi next_instr))) (Ssequence (Sset (fst id_t) (Econst_int (phi (start + 1)) (snd id_t))) Sbreak) ls'')) \/
                                    (n = start /\
                                     select_switch_case (Int.unsigned (phi n)) ls =
                                     Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi (start + 1)) (snd id_t))) Sbreak) ls'))) ->
                                    match_stmt_cont_in_loop2 Sskip ls id_t (start::start') n next_instr to_continue to_break (Kloop2 s1 s2 k)
| match_assign_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' e1 e2 k,
                                (exists s1 s2 k', context k = Kloop2 s1 s2 k') ->
                                0 < n <= Int.max_unsigned ->
                                select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sassign e1 e2) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                (exists m, match_stmt_cont_in_loop2 Sskip ls id_t start next_instr m to_continue to_break k) ->
                                match_stmt_cont_in_loop2 (Sassign e1 e2) ls id_t start n next_instr to_continue to_break k
| match_set_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' id e k,
                             (exists s1 s2 k', context k = Kloop2 s1 s2 k') ->
                             0 < n <= Int.max_unsigned ->
                             select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset id e) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                             (exists m, match_stmt_cont_in_loop2 Sskip ls id_t start next_instr m to_continue to_break k) ->
                             match_stmt_cont_in_loop2 (Sset id e) ls id_t start n next_instr to_continue to_break k
| match_call_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' optid a al k,
                              (exists s1 s2 k', context k = Kloop2 s1 s2 k') ->
                              0 < n <= Int.max_unsigned ->
                              select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Scall optid a al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                              (exists m, match_stmt_cont_in_loop2 Sskip ls id_t start next_instr m to_continue to_break k) ->
                              match_stmt_cont_in_loop2 (Scall optid a al) ls id_t start n next_instr to_continue to_break k
| match_builtin_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' optid ef tyargs al k,
                                 (exists s1 s2 k', context k = Kloop2 s1 s2 k') ->
                                 0 < n <= Int.max_unsigned ->
                                 select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sbuiltin optid ef tyargs al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                 (exists m, match_stmt_cont_in_loop2 Sskip ls id_t start next_instr m to_continue to_break k) ->
                                 match_stmt_cont_in_loop2 (Sbuiltin optid ef tyargs al) ls id_t start n next_instr to_continue to_break k
| match_sequence_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break s1 s2 k,
                             (exists s s' k', context k = Kloop2 s s' k') ->
                             0 < n <= Int.max_unsigned ->
                             match_stmt_cont_in_loop2 s1 ls id_t start (n) (n + sizeof_stmt s1) to_continue to_break (Kseq s2 k) ->
                             match_stmt_cont_in_loop2 s2 ls id_t start (n + sizeof_stmt s1) next_instr to_continue to_break k ->
                             match_stmt_cont_in_loop2 (Ssequence s1 s2) ls id_t start n next_instr to_continue to_break k
| match_ifthenelse_cont_in_loop2: forall start id_t ls ls' n next_instr to_continue to_break b s1 s2 k,
                                    (exists s s' k', context k = Kloop2 s s' k') ->
                                    0 < n <= Int.max_unsigned ->
                                    select_switch_case (Int.unsigned (phi n)) ls =
                                    Some (LScons (Some (Int.unsigned (phi n))) (Sifthenelse b (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1 + sizeof_stmt s1)) (snd id_t))) Sbreak)) ls') ->
                                    match_stmt_cont_in_loop2 s1 ls id_t start (n + 1) next_instr to_continue to_break k ->
                                    match_stmt_cont_in_loop2 s2 ls id_t start (n + 1 + sizeof_stmt s1) next_instr to_continue to_break k ->
                                    match_stmt_cont_in_loop2 (Sifthenelse b s1 s2) ls id_t start n next_instr to_continue to_break k
| match_loop_cont_in_loop2: forall start id_t ls ls' n next_instr to_continue to_break s1 s2 k,
                              (exists s s' k', context k = Kloop2 s s' k') ->
                              0 < n <= Int.max_unsigned ->
                              select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) ls') ->
                              match_stmt_cont_in_loop1 s1 ls id_t (n::start) (n + 1) (n + 1 + sizeof_stmt s1) ((n + 1 + sizeof_stmt s1)::to_continue) (next_instr::to_break) (Kloop1 s1 s2 k) ->
                              match_stmt_cont_in_loop2 s2 ls id_t (n::start) (n + 1 + sizeof_stmt s1) n ((n + 1 + sizeof_stmt s1)::to_continue) (next_instr::to_break) (Kloop2 s1 s2 k) ->
                              match_stmt_cont_in_loop2 (Sloop s1 s2) ls id_t start n next_instr to_continue to_break k
| match_break_cont_seq_in_loop2: forall start id_t ls n next_instr to_continue to_break s k,
                                   (exists s1 s2 k', context (Kseq s k) = Kloop2 s1 s2 k') ->
                                   match_stmt_cont_in_loop2 Sbreak ls id_t start n next_instr to_continue to_break k ->
                                   match_stmt_cont_in_loop2 Sbreak ls id_t start n next_instr to_continue to_break (Kseq s k)
| match_break_cont_loop2_in_loop2: forall start start' id_t ls n next_instr to_continue to_break ls' s1 s2 k p q,
                                    0 < n <= Int.max_unsigned ->
                                    select_switch_case (Int.unsigned (phi n)) ls =
                                    Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_break) (snd id_t))) Sbreak) ls') ->
                                    ((is_call_cont (context k) /\ exists m, match_stmt_cont Sskip ls id_t to_break m k /\ start' = nil /\ p = nil /\ q = nil) \/
                                    (exists s s' k', context k = Kloop1 s s' k' /\ exists m, match_stmt_cont_in_loop1 Sskip ls id_t start' to_break m p q k) \/
                                    (exists s s' k', context k = Kloop2 s s' k' /\ exists m, match_stmt_cont_in_loop2 Sskip ls id_t start' to_break m p q k)) ->
                                    match_stmt_cont_in_loop2 Sbreak ls id_t (start::start') n next_instr (to_continue::p) (to_break::q) (Kloop2 s1 s2 k)
| match_return_cont_in_loop2: forall start id_t ls n next_instr to_continue to_break ls' v k,
                                (exists s1 s2 k', context k = Kloop2 s1 s2 k') ->
                                0 < n <= Int.max_unsigned ->
                                select_switch_case (Int.unsigned (phi n)) ls =
                                Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sreturn v) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                                match_stmt_cont_in_loop2 (Sreturn v) ls id_t start n next_instr to_continue to_break k
with match_stmt_cont: statement -> labeled_statements -> ident * type -> Z -> Z -> cont -> Prop :=
| match_skip_cont_seq: forall id_t ls n next_instr ls' s k,
                                  is_call_cont (context (Kseq s k)) ->
                                  0 < n <= Int.max_unsigned ->
                                  (select_switch_case (Int.unsigned (phi n)) ls =
                                   Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                   exists m, match_stmt_cont s ls id_t next_instr m k) \/
                                  match_stmt_cont s ls id_t n next_instr k ->
                                  match_stmt_cont Sskip ls id_t n next_instr (Kseq s k)
| match_skip_cont_call_cont: forall id_t ls n next_instr ls' k,
                               is_call_cont k ->
                               ((select_switch_case (Int.unsigned (phi n)) ls =
                                Some (LScons (Some (Int.unsigned (phi n))) (Ssequence Sskip (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') /\
                                 0 < n <= Int.max_unsigned /\
                                 next_instr = 0 /\
                                 select_switch (Int.unsigned (phi next_instr)) ls = LSnil) \/
                                n = 0 /\
                                select_switch (Int.unsigned (phi n)) ls = LSnil) ->
                               match_stmt_cont Sskip ls id_t n next_instr k
| match_assign_cont: forall id_t ls n next_instr ls' e1 e2 k,
                       is_call_cont (context k) ->
                       0 < n <= Int.max_unsigned ->
                       select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sassign e1 e2) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                       (exists m, match_stmt_cont Sskip ls id_t next_instr m k) ->
                       match_stmt_cont (Sassign e1 e2) ls id_t n next_instr k
| match_set_cont: forall id_t ls n next_instr ls' id e k,
                    is_call_cont (context k) ->
                    0 < n <= Int.max_unsigned ->
                    select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset id e) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                    (exists m, match_stmt_cont Sskip ls id_t next_instr m k) ->
                    match_stmt_cont (Sset id e) ls id_t n next_instr k
| match_scall_cont: forall id_t ls n next_instr ls' optid a al k,
                     is_call_cont (context k) ->
                     0 < n <= Int.max_unsigned ->
                     select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Scall optid a al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                     (exists m, match_stmt_cont Sskip ls id_t next_instr m k) ->
                     match_stmt_cont (Scall optid a al) ls id_t n next_instr k
| match_builtin_cont: forall id_t ls n next_instr ls' optid ef tyargs al k,
                        is_call_cont (context k) ->
                        0 < n <= Int.max_unsigned ->
                        select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sbuiltin optid ef tyargs al) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                        (exists m, match_stmt_cont Sskip ls id_t next_instr m k) ->
                        match_stmt_cont (Sbuiltin optid ef tyargs al) ls id_t n next_instr k
| match_sequence_cont: forall id_t ls n next_instr s1 s2 k,
                         is_call_cont (context k) ->
                         0 < n <= Int.max_unsigned ->
                         match_stmt_cont s1 ls id_t (n) (n + sizeof_stmt s1) (Kseq s2 k) ->
                         match_stmt_cont s2 ls id_t (n + sizeof_stmt s1) next_instr k ->
                         match_stmt_cont (Ssequence s1 s2) ls id_t n next_instr k
| match_ifthenelse_cont: forall id_t ls ls' n next_instr b s1 s2 k,
                           is_call_cont (context k) ->
                           0 < n <= Int.max_unsigned ->
                           select_switch_case (Int.unsigned (phi n)) ls =
                           Some (LScons (Some (Int.unsigned (phi n))) (Sifthenelse b (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1 + sizeof_stmt s1)) (snd id_t))) Sbreak)) ls') ->
                           match_stmt_cont s1 ls id_t (n + 1) next_instr k ->
                           match_stmt_cont s2 ls id_t (n + 1 + sizeof_stmt s1) next_instr k ->
                           match_stmt_cont (Sifthenelse b s1 s2) ls id_t n next_instr k
| match_loop_cont: forall id_t ls ls' n next_instr s1 s2 k,
                     is_call_cont (context k) ->
                     0 < n <= Int.max_unsigned ->
                     select_switch_case (Int.unsigned (phi n)) ls = Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sset (fst id_t) (Econst_int (phi (n + 1)) (snd id_t))) Sbreak) ls') ->
                     match_stmt_cont_in_loop1 s1 ls id_t (n::nil) (n + 1) (n + 1 + sizeof_stmt s1) ((n + 1 + sizeof_stmt s1)::nil) (next_instr::nil) (Kloop1 s1 s2 k) ->
                     match_stmt_cont_in_loop2 s2 ls id_t (n::nil) (n + 1 + sizeof_stmt s1) n ((n + 1 + sizeof_stmt s1)::nil) (next_instr::nil) (Kloop2 s1 s2 k) ->
                     match_stmt_cont (Sloop s1 s2) ls id_t n next_instr k
| match_return_cont: forall id_t ls n next_instr ls' v k,
                       is_call_cont (context k) ->
                       0 < n <= Int.max_unsigned ->
                       select_switch_case (Int.unsigned (phi n)) ls =
                       Some (LScons (Some (Int.unsigned (phi n))) (Ssequence (Sreturn v) (Ssequence (Sset (fst id_t) (Econst_int (phi next_instr) (snd id_t))) Sbreak)) ls') ->
                       match_stmt_cont (Sreturn v) ls id_t n next_instr k.

Lemma is_call_cont_context:
  forall k,
    is_call_cont (context k) ->
    is_call_cont k \/ exists s k', k = Kseq s k'.

Lemma select_switch_case_app_right:
  forall ls1 ls2 pc,
    select_switch_case pc ls1 = None ->
    select_switch_case pc (app_lstmt ls1 ls2) = select_switch_case pc ls2.

Lemma select_switch_nil_select_switch_case:
  forall pc ls,
    select_switch pc ls = LSnil ->
    select_switch_case pc ls = None.

Lemma select_switch_default_app_right:
  forall ls1 ls2,
    select_switch_default ls1 = LSnil ->
    select_switch_default (app_lstmt ls1 ls2) = select_switch_default ls2.

Lemma select_switch_app_right:
  forall ls1 ls2 pc,
    select_switch pc ls1 = LSnil ->
    select_switch pc (app_lstmt ls1 ls2) = select_switch pc ls2.

Lemma app_lstmt_assoc:
  forall ls1 ls2 ls3,
    app_lstmt (app_lstmt ls1 ls2) ls3 = app_lstmt ls1 (app_lstmt ls2 ls3).

Lemma select_switch_case_not_nil:
  forall n ls,
    select_switch_case n ls <> Some LSnil.

Lemma select_switch_app_nil:
  forall n ls1 ls2,
    select_switch n (app_lstmt ls1 ls2) = LSnil ->
    select_switch n ls1 = LSnil /\ select_switch n ls2 = LSnil.

Lemma phi_injection:
  forall n m,
    0 <= n <= Int.max_unsigned ->
    0 <= m <= Int.max_unsigned ->
    Int.unsigned (phi n) = Int.unsigned (phi m) ->
    n = m.

Lemma select_switch_in_loop1_flatten:
  forall s id_t n m k l ls pc,
    0 <= n ->
    (n + sizeof_stmt s) <= Int.max_unsigned ->
    0 <= pc <= Int.max_unsigned ->
    flatten_loop1 phi id_t s n m k l = OK ls ->
    (select_switch (Int.unsigned (phi pc)) ls = LSnil <-> pc < n \/ n + sizeof_stmt s <= pc)
with select_switch_in_loop2_flatten:
  forall s id_t n m k ls pc,
    0 <= n ->
    (n + sizeof_stmt s) <= Int.max_unsigned ->
    0 <= pc <= Int.max_unsigned ->
    flatten_loop2 phi id_t s n m k = OK ls ->
    (select_switch (Int.unsigned (phi pc)) ls = LSnil <-> pc < n \/ n + sizeof_stmt s <= pc).

Lemma select_switch_flatten:
  forall s id_t n m ls pc,
    0 <= n ->
    (n + sizeof_stmt s) <= Int.max_unsigned ->
    0 <= pc <= Int.max_unsigned ->
    flatten phi id_t s n m = OK ls ->
    (select_switch (Int.unsigned (phi pc)) ls = LSnil <-> pc < n \/ n + sizeof_stmt s <= pc).

Lemma lscons_app_lstmt:
  forall o s ls,
    LScons o s ls = app_lstmt (LScons o s LSnil) ls.

Lemma app_lstmt_lscons:
  forall o s ls1 ls2,
    LScons o s (app_lstmt ls1 ls2) = app_lstmt (LScons o s ls1) ls2.

Lemma app_lstmt_lsnil:
  forall ls,
    app_lstmt ls LSnil = ls.

Lemma context_loop1:
  forall k s1 s2 k',
    context k = Kloop1 s1 s2 k' ->
    k = Kloop1 s1 s2 k' \/ exists s'' k'', k = Kseq s'' k''.

Lemma context_loop2:
  forall k s1 s2 k',
    context k = Kloop2 s1 s2 k' ->
    k = Kloop2 s1 s2 k' \/ exists s'' k'', k = Kseq s'' k''.

Lemma break_continue_seq_match_stmt_cont_in_loop1:
  forall k s s1 s2 k' start pc next_instr to_continue to_break ls id_t,
    context k = Kloop1 s1 s2 k' ->
    s = Sbreak \/ s = Scontinue ->
    (match_stmt_cont_in_loop1 s ls id_t start pc next_instr to_continue to_break (Kloop1 s1 s2 k') <->
    match_stmt_cont_in_loop1 s ls id_t start pc next_instr to_continue to_break k).

Lemma break_seq_match_stmt_cont_in_loop2:
  forall k s1 s2 k' start pc next_instr to_continue to_break ls id_t,
    context k = Kloop2 s1 s2 k' ->
    (match_stmt_cont_in_loop2 Sbreak ls id_t start pc next_instr to_continue to_break (Kloop2 s1 s2 k') <->
    match_stmt_cont_in_loop2 Sbreak ls id_t start pc next_instr to_continue to_break k).

Lemma break_loop1_loop2:
  forall s1 s2 k ls id_t start pc next_instr to_continue to_break,
    match_stmt_cont_in_loop1 Sbreak ls id_t start pc next_instr to_continue to_break (Kloop1 s1 s2 k) <-> match_stmt_cont_in_loop2 Sbreak ls id_t start pc next_instr to_continue to_break (Kloop2 s1 s2 k).

Lemma match_stmt_cont_in_loop1_pos:
  forall s ls id_t start pc next_instr to_continue to_break k,
    match_stmt_cont_in_loop1 s ls id_t start pc next_instr to_continue to_break k ->
    0 < pc <= Int.max_unsigned
with match_stmt_cont_in_loop2_pos:
       forall s ls id_t start pc next_instr to_continue to_break k,
         match_stmt_cont_in_loop2 s ls id_t start pc next_instr to_continue to_break k ->
         0 < pc <= Int.max_unsigned.

Fixpoint match_stmt_cont_flatten s { struct s } :
  forall k ls ls1 ls2 pc next_instr id_t,
    is_call_cont (context k) ->
    flatten phi id_t s pc next_instr = OK ls ->
    (forall s' k', k = Kseq s' k' ->
                   exists next_instr',
                     0 < next_instr <= Int.max_unsigned /\
                     match_stmt_cont s' (app_lstmt ls1 (app_lstmt ls ls2)) id_t next_instr next_instr' k') ->
    (is_call_cont k -> next_instr = 0 /\ select_switch (Int.unsigned (phi next_instr)) (app_lstmt ls1 (app_lstmt ls ls2)) = LSnil) ->
    (next_instr < pc \/ next_instr >= pc + sizeof_stmt s) ->
    (forall n, pc <= n <= Int.max_unsigned -> select_switch (Int.unsigned (phi n)) ls1 = LSnil) ->
    0 < pc ->
    pc + sizeof_stmt s <= Int.max_unsigned ->
    match_stmt_cont s (app_lstmt ls1 (app_lstmt ls ls2)) id_t pc next_instr k
with match_stmt_cont_in_loop1_flatten_loop1 s { struct s } :
  forall k ls ls1 ls2 start start' pc next_instr to_continue to_continue' to_break to_break' id_t,
    (exists s1 s2 k', context k = Kloop1 s1 s2 k' /\
    (forall counter ls' next,
       0 < counter <= Int.max_unsigned ->
       select_switch_case (Int.unsigned (phi counter)) (app_lstmt ls1 (app_lstmt ls ls2)) =
       Some (LScons (Some (Int.unsigned (phi counter))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_break) (snd id_t))) Sbreak) ls') -> match_stmt_cont_in_loop1 Sbreak (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') counter next (to_continue::to_continue') (to_break::to_break') (Kloop1 s1 s2 k')) /\
    (forall counter ls' next,
      0 < counter <= Int.max_unsigned ->
      select_switch_case (Int.unsigned (phi counter)) (app_lstmt ls1 (app_lstmt ls ls2)) =
      Some (LScons (Some (Int.unsigned (phi counter))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_continue) (snd id_t))) Sbreak) ls') -> match_stmt_cont_in_loop1 Scontinue (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') counter next (to_continue::to_continue') (to_break::to_break') (Kloop1 s1 s2 k'))) ->
    flatten_loop1 phi id_t s pc next_instr to_continue to_break = OK ls ->
    (forall s' k', k = Kseq s' k' ->
                   ((exists next_instr',
                     match_stmt_cont_in_loop1 s' (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') next_instr next_instr' (to_continue::to_continue') (to_break::to_break') k'))) ->
    (forall s1' s2' k', k = Kloop1 s1' s2' k' ->
                        (next_instr = to_continue) /\
                        (exists ls',
                           (next_instr = start + 1 + sizeof_stmt s1') /\
                           (0 < start /\ start + 1 + sizeof_stmt s1' + sizeof_stmt s2' <= Int.max_unsigned) /\
                           match_stmt_cont_in_loop2 s2' (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') next_instr start (to_continue::to_continue') (to_break::to_break') (Kloop2 s1' s2' k') /\
                           select_switch_case (Int.unsigned (phi start)) (app_lstmt ls1 (app_lstmt ls ls2)) = Some (LScons (Some (Int.unsigned (phi start))) (Ssequence (Sset (fst id_t) (Econst_int (phi (start + 1)) (snd id_t))) Sbreak) ls')) /\
                        ((is_call_cont (context k') /\ start' = nil /\ to_continue' = nil /\ to_break' = nil /\ exists next_instr', match_stmt_cont Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t to_break next_instr' k') \/
                         (exists s1'' s2'' k'', context k' = Kloop1 s1'' s2'' k'' /\ exists next_instr', match_stmt_cont_in_loop1 Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t start' to_break next_instr' to_continue' to_break' k') \/
                         (exists s1'' s2'' k'', context k' = Kloop2 s1'' s2'' k'' /\ exists next_instr', match_stmt_cont_in_loop2 Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t start' to_break next_instr' to_continue' to_break' k'))) ->
    (next_instr < pc \/ next_instr >= pc + sizeof_stmt s) ->
    (forall n, pc <= n <= Int.max_unsigned -> select_switch (Int.unsigned (phi n)) ls1 = LSnil) ->
    0 < pc ->
    pc + sizeof_stmt s <= Int.max_unsigned ->
    match_stmt_cont_in_loop1 s (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') pc next_instr (to_continue::to_continue') (to_break::to_break') k
with match_stmt_cont_in_loop2_flatten_loop2 s { struct s } :
       forall k ls ls1 ls2 start start' pc next_instr to_continue to_continue' to_break to_break' id_t,
         (exists s1 s2 k', context k = Kloop2 s1 s2 k' /\
         (forall counter ls' next,
            0 < counter <= Int.max_unsigned ->
            select_switch_case (Int.unsigned (phi counter)) (app_lstmt ls1 (app_lstmt ls ls2)) =
            Some (LScons (Some (Int.unsigned (phi counter))) (Ssequence (Sset (fst id_t) (Econst_int (phi to_break) (snd id_t))) Sbreak) ls') -> match_stmt_cont_in_loop2 Sbreak (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') counter next (to_continue::to_continue') (to_break::to_break') (Kloop2 s1 s2 k'))) ->
         flatten_loop2 phi id_t s pc next_instr to_break = OK ls ->
         (forall s' k', k = Kseq s' k' ->
                        ((exists next_instr',
                          match_stmt_cont_in_loop2 s' (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') next_instr next_instr' (to_continue::to_continue') (to_break::to_break') k'))) ->
         (forall s1' s2' k', k = Kloop2 s1' s2' k' ->
                             (exists ls',
                                next_instr = start /\
                                (0 < start /\ start + 1 + sizeof_stmt s1' + sizeof_stmt s2' <= Int.max_unsigned) /\
                                select_switch_case (Int.unsigned (phi next_instr)) (app_lstmt ls1 (app_lstmt ls ls2)) = Some (LScons (Some (Int.unsigned (phi next_instr))) (Ssequence (Sset (fst id_t) (Econst_int (phi (start + 1)) (snd id_t))) Sbreak) ls')) /\
                             ((is_call_cont (context k') /\ start' = nil /\ to_continue' = nil /\ to_break' = nil /\ exists next_instr', match_stmt_cont Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t to_break next_instr' k') \/
                             (exists s1'' s2'' k'', context k' = Kloop1 s1'' s2'' k'' /\ exists next_instr', match_stmt_cont_in_loop1 Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t start' to_break next_instr' to_continue' to_break' k') \/
                             (exists s1'' s2'' k'', context k' = Kloop2 s1'' s2'' k'' /\ exists next_instr', match_stmt_cont_in_loop2 Sskip (app_lstmt ls1 (app_lstmt ls ls2)) id_t start' to_break next_instr' to_continue' to_break' k'))) ->
         (next_instr < pc \/ next_instr >= pc + sizeof_stmt s) ->
         (forall n, pc <= n <= Int.max_unsigned -> select_switch (Int.unsigned (phi n)) ls1 = LSnil) ->
         0 < pc ->
         pc + sizeof_stmt s <= Int.max_unsigned ->
         match_stmt_cont_in_loop2 s (app_lstmt ls1 (app_lstmt ls ls2)) id_t (start::start') pc next_instr (to_continue::to_continue') (to_break::to_break') k.


Fixpoint num_stmt (s: statement): nat :=
  match s with
    | Ssequence s1 s2 => S (S (num_stmt s1 + num_stmt s2))
    | _ => O
  end.

Fixpoint num_cont (k: cont): nat :=
  match k with
    | Kseq s k => S (num_cont k + num_stmt s)
    | Kstop | Kcall _ _ _ _ _ | Kswitch _ => O
    | Kloop1 _ s2 k => S (S (num_cont k) + num_stmt s2)
    | Kloop2 _ _ k => S (num_cont k)
  end.

Definition measure (st: Clight.state): nat :=
  match st with
    | State _ s k _ _ _ => (num_stmt s + num_cont k)%nat
    | _ => 0%nat
  end.

Inductive match_loop (ls: labeled_statements) (id_t: ident * type): list Z -> list Z -> list Z -> cont -> Prop :=
| match_loop_cont_loop1: forall start start' to_continue to_continue' to_break to_break' s1 s2 k,
                           0 < start <= Int.max_unsigned ->
                           start + 1 + sizeof_stmt s1 = to_continue ->
                           match_stmt_cont_in_loop1 s1 ls id_t (start::start') (start + 1) (start + 1 + sizeof_stmt s1) (to_continue::to_continue') (to_break::to_break') (Kloop1 s1 s2 k) ->
                           match_stmt_cont_in_loop2 s2 ls id_t (start::start') (start + 1 + sizeof_stmt s1) start (to_continue::to_continue') (to_break::to_break') (Kloop2 s1 s2 k) ->
                           match_loop ls id_t start' to_continue' to_break' k ->
                           match_loop ls id_t (start::start') (to_continue::to_continue') (to_break::to_break') (Kloop1 s1 s2 k)
| match_loop_cont_loop2: forall start start' to_continue to_continue' to_break to_break' s1 s2 k,
                           0 < start <= Int.max_unsigned ->
                           start + 1 + sizeof_stmt s1 = to_continue ->
                           match_stmt_cont_in_loop1 s1 ls id_t (start::start') (start + 1) (start + 1 + sizeof_stmt s1) (to_continue::to_continue') (to_break::to_break') (Kloop1 s1 s2 k) ->
                           match_stmt_cont_in_loop2 s2 ls id_t (start::start') (start + 1 + sizeof_stmt s1) start (to_continue::to_continue') (to_break::to_break') (Kloop2 s1 s2 k) ->
                           match_loop ls id_t start' to_continue' to_break' k ->
                           match_loop ls id_t (start::start') (to_continue::to_continue') (to_break::to_break') (Kloop2 s1 s2 k)
| match_loop_cont_call: forall optid f e le k,
                          match_loop ls id_t nil nil nil (Kcall optid f e le k)
| match_loop_cont_stop: match_loop ls id_t nil nil nil Kstop
| match_loop_cont_seq: forall start to_continue to_break s k,
                         match_loop ls id_t start to_continue to_break (context (Kseq s k)) ->
                         match_loop ls id_t start to_continue to_break (Kseq s k).

Lemma match_loop_context:
  forall ls id_t start continue break k,
    match_loop ls id_t start continue break k <->
    match_loop ls id_t start continue break (context k).

Lemma match_loop_call_cont_context:
  forall ls id_t k,
    is_call_cont (context k) ->
    match_loop ls id_t nil nil nil (context k).

Lemma match_loop_loop1_context:
  forall ls id_t start continue break k s1 s2 k',
    context k = Kloop1 s1 s2 k' ->
    match_loop ls id_t start continue break k ->
    exists to_start to_start' to_continue to_continue' to_break to_break',
      start = to_start::to_start' /\ continue = to_continue::to_continue' /\ break = to_break::to_break'.

Lemma match_loop_loop2_context:
  forall ls id_t start continue break k s1 s2 k',
    context k = Kloop2 s1 s2 k' ->
    match_loop ls id_t start continue break k ->
    exists to_start to_start' to_continue to_continue' to_break to_break',
      start = to_start::to_start' /\ continue = to_continue::to_continue' /\ break = to_break::to_break'.

Lemma match_loop_call_cont_context_charact:
  forall ls id_t start to_continue to_break k,
    is_call_cont (context k) ->
    match_loop ls id_t start to_continue to_break k ->
    start = nil /\ to_continue = nil /\ to_break = nil.

Lemma context_charact:
  forall k,
    is_call_cont (context k) \/
    (exists s1 s2 k', context k = Kloop1 s1 s2 k') \/
    (exists s1 s2 k', context k = Kloop2 s1 s2 k') \/
    (exists k', context k = Kswitch k').

Lemma no_switch_context:
  forall k k',
    no_switch_label_goto_in_cont k ->
    context k <> Kswitch k'.

Lemma no_switch_label_goto_in_cont_call_cont:
  forall k,
    no_switch_label_goto_in_cont k ->
    no_switch_label_goto_in_cont (call_cont k).

Inductive match_call_cont: cont -> cont -> Prop :=
| match_call_cont_stop: forall k tk,
                          call_cont k = Kstop ->
                          call_cont tk = Kstop ->
                          match_call_cont k tk
| match_call_cont_call: forall k tk optid f tf e le tle k' tk' ls,
                          call_cont k = Kcall optid f e le k' ->
                          call_cont tk = Kcall optid tf e tle tk' ->
                          transf_function phi f = OK tf ->
                          flatten phi (new_ident_for_function f, tint) (fn_body f) 1 0 = OK ls ->
                          (forall id, id <> new_ident_for_function f -> le!id = tle!id) ->
                          (exists next_instr ls' tk'',
                            tk' = Kseq
     (Ssequence
        (Sset (new_ident_for_function f)
           (Econst_int (phi next_instr) tint)) Sbreak)
     (Kseq (seq_of_labeled_statement ls')
        (Kswitch
           (Kloop1
              (Ssequence
                 (Sifthenelse
                    (Ebinop One (Etempvar (new_ident_for_function f) tint)
                       (Econst_int (phi 0) tint) tint) Sskip Sbreak)
                 (Sswitch (Etempvar (new_ident_for_function f) tint) ls))
              Sskip tk''))) /\
                            (is_call_cont tk'') /\
                            ((is_call_cont (context k') /\ exists next_instr', match_stmt_cont Sskip ls (new_ident_for_function f, tint) next_instr next_instr' k') \/
                             (exists s1 s2 k'', context k' = Kloop1 s1 s2 k'' /\
                                                exists start start' next_instr' to_continue to_continue' to_break to_break',
                               match_stmt_cont_in_loop1 Sskip ls (new_ident_for_function f, tint) (start::start') next_instr next_instr' (to_continue::to_continue') (to_break::to_break') k' /\
                               match_loop ls (new_ident_for_function f, tint) (start::start') (to_continue::to_continue') (to_break::to_break') k') \/
                             (exists s1 s2 k'', context k' = Kloop2 s1 s2 k'' /\
                                                exists start start' next_instr' to_continue to_continue' to_break to_break',
                               match_stmt_cont_in_loop2 Sskip ls (new_ident_for_function f, tint) (start::start') next_instr next_instr' (to_continue::to_continue') (to_break::to_break') k' /\
                               match_loop ls (new_ident_for_function f, tint) (start::start') (to_continue::to_continue') (to_break::to_break') k'))) ->
                          match_call_cont k' tk' ->
                          match_call_cont k tk.

Lemma match_call_cont_seq:
  forall k tk, match_call_cont k tk ->
  forall s, match_call_cont (Kseq s k) tk.

Lemma match_call_cont_seq_bis:
  forall k tk,
    match_call_cont k tk ->
    forall s, match_call_cont k (Kseq s tk).

Lemma match_call_cont_loop1:
  forall k tk,
    match_call_cont k tk ->
    forall s1 s2, match_call_cont (Kloop1 s1 s2 k) tk.

Lemma match_call_cont_loop1_bis:
  forall k tk,
    match_call_cont k tk ->
    forall s1 s2, match_call_cont k (Kloop1 s1 s2 tk).

Lemma match_call_cont_loop2:
  forall k tk,
    match_call_cont k tk ->
    forall s1 s2, match_call_cont (Kloop2 s1 s2 k) tk.

Lemma match_call_cont_loop2_bis:
  forall k tk,
    match_call_cont k tk ->
    forall s1 s2, match_call_cont k (Kloop2 s1 s2 tk).

Lemma match_call_cont_switch_bis:
  forall k tk,
    match_call_cont k tk ->
    match_call_cont k (Kswitch tk).

Lemma match_call_cont_call_cont:
  forall k tk,
    match_call_cont k tk ->
    match_call_cont (call_cont k) (call_cont tk).

Inductive match_states: Clight.state -> Clight.state -> Prop :=
| match_regular_states:
    forall f s k e le m tf tk tle ls n
           (TRF: transf_function phi f = OK tf)
           (TENV: forall id, id <> new_ident_for_function f ->
                             le!id = tle!id)
           (NSTMT: not_in_stmt (new_ident_for_function f) s)
           (NCONT: not_in_cont (new_ident_for_function f) k)
           (NSLG: no_switch_label_goto_in_stmt s)
           (NSLGK: no_switch_label_goto_in_cont k)
           (LS: flatten phi (new_ident_for_function f, tint) (fn_body f) 1 0 = OK ls)
           (PC: tle!(new_ident_for_function f) = Some (Vint (phi n)))
           (MSTMT: (is_call_cont (context k) /\ exists next_instr, match_stmt_cont s ls (new_ident_for_function f, tint) n next_instr k) \/
           (exists s1 s2 k', context k = Kloop1 s1 s2 k' /\
                             exists start start' next_instr to_continue to_continue' to_break to_break',
                               match_stmt_cont_in_loop1 s ls (new_ident_for_function f, tint) (start::start') n next_instr (to_continue::to_continue') (to_break::to_break') k /\
                               match_loop ls (new_ident_for_function f, tint) (start::start') (to_continue::to_continue') (to_break::to_break') k) \/
           (exists s1 s2 k', context k = Kloop2 s1 s2 k' /\
                             exists start start' next_instr to_continue to_continue' to_break to_break',
                               match_stmt_cont_in_loop2 s ls (new_ident_for_function f, tint) (start::start') n next_instr (to_continue::to_continue') (to_break::to_break') k /\
                               match_loop ls (new_ident_for_function f, tint) (start::start') (to_continue::to_continue') (to_break::to_break') k))
           (MCONT: match_call_cont k tk)
           (CCONT: is_call_cont tk),
      match_states
        (State f s k e le m)
        (State tf
               (Sloop (Ssequence
                         (Sifthenelse
                            (Ebinop One
                                    (Etempvar (new_ident_for_function f) tint)
                                    (Econst_int (phi 0) tint) tint)
                            Sskip
                            Sbreak)
                         (Sswitch (Etempvar (new_ident_for_function f) tint) ls)) Sskip)
               tk e tle m)
| match_call_states:
    forall fd tfd args k tk m
           (TRFD: transf_fundef phi fd = OK tfd)
           (MCONT: match_call_cont k tk)
           (NCONT: forall id, not_in_cont id k)
           (NSLGK: no_switch_label_goto_in_cont k)
           (CCONT: is_call_cont k)
           (TCONT: is_call_cont tk),
      match_states (Callstate fd args k m) (Callstate tfd args tk m)
| match_return_states:
    forall v k tk m
           (MCONT: match_call_cont k tk)
           (NCONT: forall id, not_in_cont id k)
           (NSLGK: no_switch_label_goto_in_cont k)
           (CCONT: is_call_cont k)
           (TCONT: is_call_cont tk),
      match_states (Returnstate v k m) (Returnstate v tk m).

Lemma is_call_cont_call_cont:
  forall k,
    is_call_cont (call_cont k).

Lemma alloc_variables_preserved:
  forall e m l e' m',
    alloc_variables ge e m l e' m' ->
    alloc_variables tge e m l e' m'.

Lemma bind_parameters_preserved:
  forall e m params args m',
    bind_parameters ge e m params args m' ->
    bind_parameters tge e m params args m'.

Theorem simulation:
  forall S1 t S2, step1 ge S1 t S2 ->
                  forall S1' (MS: match_states S1 S1'),
                  exists S2',
                    (plus step1 tge S1' t S2' \/
                     (star step1 tge S1' t S2' /\ measure S2 < measure S1)%nat)
                    /\ match_states S2 S2'.

Lemma initial_states_simulation:
  forall S, Clight.initial_state prog S ->
            exists R, Clight.initial_state tprog R /\ match_states S R.

Lemma final_states_simulation:
  forall S R r,
  match_states S R -> Clight.final_state S r -> Clight.final_state R r.

Theorem transf_program_correct:
  forward_simulation (Clight.semantics1 prog) (Clight.semantics1 tprog).

End PRESERVATION.

Section PRESERVATION_IDENT.


Definition phi_ident := Int.repr.

Variable prog: Clight.program.
Variable tprog: Clight.program.
Hypothesis TRANSF: transf_program phi_ident prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Theorem phi_ident_injective:
  forall x y,
    0 <= x <= Int.max_unsigned ->
    0 <= y <= Int.max_unsigned ->
    phi_ident x = phi_ident y ->
    x = y.

Theorem transf_program_correct_ident:
  forward_simulation (Clight.semantics1 prog) (Clight.semantics1 tprog).

End PRESERVATION_IDENT.

Section PRESERVATION_INV.

Definition phi_inv x := Int.repr (Int.max_unsigned - x).

Variable prog: Clight.program.
Variable tprog: Clight.program.
Hypothesis TRANSF: transf_program phi_inv prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Theorem phi_inv_injective:
  forall x y,
    0 <= x <= Int.max_unsigned ->
    0 <= y <= Int.max_unsigned ->
    phi_inv x = phi_inv y ->
    x = y.

Theorem transf_program_correct_inv:
  forward_simulation (Clight.semantics1 prog) (Clight.semantics1 tprog).

End PRESERVATION_INV.