Module Cminorgenproof

Require Import FSets.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Floats.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Csharpminor.
Require Import Cstacked.
Require Import Op.
Require Import Cminor.
Require Import Cminorops.
Require Import Cminorgen.
Require Import Simulations.
Require Import TSOmachine.
Require Import TSOsimulation.
Require Import Memcomp Traces.
Require Import Libtactics.
Require Import Switch.

Open Local Scope error_monad_scope.

Section TRANSLATION.

Variable prog: Csharpminor.program.

Let gce := build_global_compilenv prog.
Let gvare : gvarenv := global_var_env prog.

Variable ge : Cstacked.genv.
Variable tge : Cminor.genv.
Definition genv_rel :=
  Genv.genv_match (fun a b => transl_fundef gce a = OK b) tge ge.
Hypothesis TRANSF: genv_rel.
Hypothesis FINDS:
  forall id, In id (map (fun x => fst (fst x)) (prog_vars prog)) ->
             Genv.find_symbol ge id <> None.
                         

Simulation relations

Inductive match_env_item : ident ->
                           var_info ->
                           option env_item ->
                           option val ->
                           option pointer ->
                           Prop :=
  | match_env_item_local: forall id c v v' anysp
      (LD : Val.lessdef v v'),
      match_env_item id (Var_local c)
                           (Some (Env_local v c))
                           (Some v')
                           anysp
  | match_env_item_scalar: forall id c ofs anyv anyp,
      match_env_item id (Var_stack_scalar c ofs)
                           (Some (Env_stack_scalar c ofs))
                           anyv (Some anyp)
  | match_env_item_array: forall id n anyv anyp,
      match_env_item id (Var_stack_array n)
                           (Some (Env_stack_array n))
                           anyv (Some anyp)
  | match_env_item_global_scalar: forall id c anyv anysp p
      (GVE : gvare ! id = Some (Vscalar c))
      (GVP : Genv.find_symbol ge id = Some p),
      match_env_item id (Var_global_scalar c) None anyv anysp
  | match_env_item_global_array: forall id anyv anysp
      (GVE : match gvare ! id with
                | Some (Vscalar c) => False
                | _ => True
              end),
      match_env_item id Var_global_array None anyv anysp.

Tactic Notation "match_env_item_cases" tactic(first) tactic(c) :=
    first; [
      c "match_env_item_local" |
      c "match_env_item_scalar" |
      c "match_env_item_array" |
      c "match_env_item_global_scalar" |
      c "match_env_item_global_array"].


Definition match_env (cenv : compilenv)
                     (senv : Cstacked.env)
                     (tenv : Cminor.env) : Prop :=
  
  forall i, match_env_item i
                           (cenv !! i)
                           (senv.(csenv_env) ! i)
                           (tenv ! i)
                           senv.(csenv_sp).

Definition match_env_except (cenv : compilenv)
                            (senv : Cstacked.env)
                            (tenv : Cminor.env)
                            (eid : list ident) : Prop :=
  forall i, match_env_item i
                           (cenv !! i)
                           (senv.(csenv_env) ! i)
                           (tenv ! i)
                           senv.(csenv_sp) \/
            In i eid.

Definition get_cenv (k : Cstacked.cont) :=
  match Cstacked.call_cont k with
    | Cstacked.Kcall _ (Internal fd) _ _ => fst (build_compilenv gce fd)
    | _ => gce
  end.

Fixpoint get_cenv_ek (k : Cstacked.expr_cont) :=
  match k with
    | Cstacked.EKunop _ ek => get_cenv_ek ek
    | Cstacked.EKbinop1 _ _ ek => get_cenv_ek ek
    | Cstacked.EKbinop2 _ _ ek => get_cenv_ek ek
    | Cstacked.EKload _ ek => get_cenv_ek ek
    | Cstacked.EKcall _ _ _ k' => get_cenv k'
    | Cstacked.EKargs _ _ _ _ _ k' => get_cenv k'
    | Cstacked.EKatargs _ _ _ _ k' => get_cenv k'
    | Cstacked.EKcond _ _ ek => get_cenv_ek ek
    | Cstacked.EKassign _ k' => get_cenv k'
    | Cstacked.EKthread1 _ k' => get_cenv k'
    | Cstacked.EKthread2 _ k' => get_cenv k'
    | Cstacked.EKcondstmt _ _ k' => get_cenv k'
    | Cstacked.EKswitch _ k' => get_cenv k'
    | Cstacked.EKreturn k' => get_cenv k'
    | Cstacked.EKstoreaddr _ _ k' => get_cenv k'
    | Cstacked.EKstoreval _ _ k' => get_cenv k'
  end.

Definition make_cast_cont (chunk: memory_chunk) (ek: expr_cont) : expr_cont :=
  match chunk with
  | Mint8signed => EKunop Ocast8signed ek
  | Mint8unsigned => EKunop Ocast8unsigned ek
  | Mint16signed => EKunop Ocast16signed ek
  | Mint16unsigned => EKunop Ocast16unsigned ek
  | Mint32 => ek
  | Mfloat32 => EKunop Osingleoffloat ek
  | Mfloat64 => ek
  end.

Inductive match_cont : Cstacked.cont ->
                       Cminor.cont ->
                       exit_env ->
                       Prop :=
  | match_Kstop: forall xenv,
    match_cont Cstacked.Kstop
               Cminor.Kstop
               xenv
  | match_Kseq: forall xenv s ts sk tk
      (TS : transl_stmt (get_cenv sk) xenv s = OK ts)
      (MK : match_cont sk tk xenv),
      match_cont (Cstacked.Kseq s sk)
                 (Cminor.Kseq ts tk)
                 xenv
  | match_Kseq2: forall s1 s2 sk ts1 tk xenv
      (TS : transl_stmt (get_cenv sk) xenv s1 = OK ts1)
      (MK : match_cont (Cstacked.Kseq s2 sk) tk xenv),
      match_cont (Cstacked.Kseq (Csharpminor.Sseq s1 s2) sk)
                 (Cminor.Kseq ts1 tk)
                 xenv
  | match_Kblock: forall sk tk xenv
      (MK : match_cont sk tk xenv),
      match_cont (Cstacked.Kblock sk)
                 (Cminor.Kblock tk)
                 (true :: xenv)
  | match_Kblock2: forall sk tk xenv
      (MK : match_cont sk tk xenv),
      match_cont sk
                 (Cminor.Kblock tk)
                 (false :: xenv)
  | match_Kcall_none: forall fn e sk tfn te tk cenv xenv sz
      (Ecenv : cenv = fst (build_compilenv gce fn))
      (TB : transl_funbody cenv sz fn = OK tfn)
      (MK : match_cont sk tk xenv)
      (ME : match_env (get_cenv sk) e te),
      match_cont (Cstacked.Kcall None (Internal fn) e sk)
                 (Cminor.Kcall None (Internal tfn) e.(csenv_sp) te tk)
                 nil
  | match_Kcall_some: forall id fn e sk tfn s te tk cenv xenv sz
      (Ecenv : cenv = fst (build_compilenv gce fn))
      (TB : transl_funbody cenv sz fn = OK tfn)
      (VS : Cminorgen.var_set (get_cenv sk) id (Evar id) = OK s)
      (ME : match_env (get_cenv sk) e te)
      (MK : match_cont sk tk xenv),
      match_cont (Cstacked.Kcall (Some id) (Internal fn) e sk)
                 (Cminor.Kcall (Some id) (Internal tfn) e.(csenv_sp)
                               te (Cminor.Kseq s tk))
                 nil.

Tactic Notation "match_cont_cases" tactic(first) tactic(c) :=
    first; [
      c "match_Kstop" |
      c "match_Kseq" |
      c "match_Kseq2" |
      c "match_Kblock" |
      c "match_Kblock2" |
      c "match_Kcall_none" |
      c "match_Kcall_some"].

Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env)
                              : lbl_stmt -> cont -> cont -> Prop :=
  | tlsc_default: forall s k ts,
      transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts ->
      transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k))
  | tlsc_case: forall i s ls k ts k',
      transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts ->
      transl_lblstmt_cont cenv xenv ls k k' ->
      transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')).

Inductive cast_chunk_eq : unary_operation ->
                          memory_chunk ->
                          Prop :=
| cast_chunk_eq_8signed:
    cast_chunk_eq Ocast8signed Mint8signed
| cast_chunk_eq_8unsigned:
    cast_chunk_eq Ocast8unsigned Mint8unsigned
| cast_chunk_eq_16signed:
    cast_chunk_eq Ocast16signed Mint16signed
| cast_chunk_eq_16unsigned:
    cast_chunk_eq Ocast16unsigned Mint16unsigned
| cast_chunk_eq_singlefloat:
    cast_chunk_eq Osingleoffloat Mfloat32.

Inductive match_assign_chunk_cont : Cstacked.expr_cont ->
                                    Cminor.expr_cont ->
                                    memory_chunk ->
                                    option pointer ->
                                    list bool ->
                                    Prop :=
| match_assign_chunk_local: forall sk tk xenv osp c ofs sp id
      (CID : (get_cenv sk) !! id = Var_stack_scalar c ofs)
      (SP : osp = Some sp)
      (MK : match_cont sk tk xenv),
  match_assign_chunk_cont (Cstacked.EKassign id sk)
                          (Cminor.EKstoreval c (Vptr (Ptr.add sp (Int.repr ofs))) tk)
                          c osp xenv
| match_assign_chunk_global: forall sk tk xenv c id p osp
       (CID : (get_cenv sk) !! id = Var_global_scalar c)
       (GID : Genv.find_symbol ge id = Some p)
       (MK : match_cont sk tk xenv),
  match_assign_chunk_cont (Cstacked.EKassign id sk)
                          (Cminor.EKstoreval c (Vptr p) tk) c osp xenv
| match_assign_chunk_store: forall sk tk xenv c v v' osp
       (LD : Val.lessdef v v')
       (MK : match_cont sk tk xenv),
  match_assign_chunk_cont (Cstacked.EKstoreval c v sk)
                          (Cminor.EKstoreval c v' tk) c osp xenv.

Inductive match_var_set_cont : Cstacked.cont ->
                               Cminor.cont ->
                               option ident ->
                               list bool ->
                               Prop :=
| match_var_set_cont_none: forall sk tk xenv
    (MK : match_cont sk tk xenv),
      match_var_set_cont sk tk None xenv
| match_var_set_cont_some: forall sk tk id xenv s
    (VS : Cminorgen.var_set (get_cenv sk) id (Evar id) = OK s)
    (MK : match_cont sk tk xenv),
      match_var_set_cont sk (Kseq s tk) (Some id) xenv.
 
Inductive match_expr_cont : Cstacked.expr_cont ->
                            Cminor.expr_cont ->
                            option pointer ->
                            exit_env ->
                            Prop :=
  | match_EKunop : forall op sk tk xenv osp
      (MEK : match_expr_cont sk tk osp xenv),
      match_expr_cont (Cstacked.EKunop op sk)
                      (Cminor.EKunop op tk)
                      osp xenv
  | match_EKbinop1 : forall op sk tk sex tex xenv osp
      (MEK : match_expr_cont sk tk osp xenv)
      (TEX : transl_expr (get_cenv_ek sk) sex = OK tex),
      match_expr_cont (Cstacked.EKbinop1 op sex sk)
                      (Cminor.EKbinop1 op tex tk)
                      osp xenv
  | match_EKbinop2 : forall op sk tk v v' xenv osp
      (MEK : match_expr_cont sk tk osp xenv)
      (LD : Val.lessdef v v'),
      match_expr_cont (Cstacked.EKbinop2 op v sk)
                      (Cminor.EKbinop2 op v' tk)
                      osp xenv
  | match_EKload : forall sk tk xenv c osp
      (MEK : match_expr_cont sk tk osp xenv),
      match_expr_cont (Cstacked.EKload c sk)
                      (Cminor.EKload c tk)
                      osp xenv
  | match_EKcall : forall sk tk xenv oid sg sexs texs osp
      (MEK : match_var_set_cont sk tk oid xenv)
      (TEXL: transl_exprlist (get_cenv sk) sexs = OK texs),
      match_expr_cont (Cstacked.EKcall oid sg sexs sk)
                      (Cminor.EKcall oid sg texs tk)
                      osp xenv
  | match_EKargs : forall sk tk xenv oid sexs texs lv v lv' v' osp sig
      (MEK : match_var_set_cont sk tk oid xenv)
      (TEXL: transl_exprlist (get_cenv sk) sexs = OK texs)
      (LD : Val.lessdef v v')
      (LDV : Val.lessdef_list lv lv'),
      match_expr_cont (Cstacked.EKargs oid v sig sexs lv sk)
                      (Cminor.EKargs oid v' sig texs lv' tk)
                      osp xenv
  | match_EKatargs : forall sk tk xenv oid sexs texs lv lv' osp astmt
      (MEK : match_var_set_cont sk tk oid xenv)
      (TEXL: transl_exprlist (get_cenv sk) sexs = OK texs)
      (LDV : Val.lessdef_list lv lv'),
      match_expr_cont (Cstacked.EKatargs oid astmt sexs lv sk)
                      (Cminor.EKatargs oid astmt texs lv' tk)
                      osp xenv
  | match_EKcond : forall sk tk sex1 sex2 tex1 tex2 xenv osp
      (MEK : match_expr_cont sk tk osp xenv)
      (TEX : transl_expr (get_cenv_ek sk) sex1 = OK tex1)
      (TEX : transl_expr (get_cenv_ek sk) sex2 = OK tex2),
      match_expr_cont (Cstacked.EKcond sex1 sex2 sk)
                      (Cminor.EKcond tex1 tex2 tk)
                      osp xenv
  | match_EKassign: forall sk tk xenv s osp id
      (VS : var_set (get_cenv sk) id (Evar id) = OK s)
      (MEK : match_cont sk tk xenv),
      match_expr_cont (Cstacked.EKassign id sk)
                      (Cminor.EKassign id (Kseq s tk))
                      osp xenv
  | match_EKassign_local : forall sk tk xenv id c osp
      (CID : (get_cenv sk) !! id = Var_local c)
      (MEK : match_cont sk tk xenv),
      match_expr_cont (Cstacked.EKassign id sk)
                      (make_cast_cont c (Cminor.EKassign id tk))
                      osp xenv
  | match_EKassign_chunk : forall sk tk c osp xenv
      (MACK : match_assign_chunk_cont sk tk c osp xenv),
      match_expr_cont sk tk osp xenv
  | match_EKthread1 : forall sk tk xenv sex tex osp
      (MEK : match_cont sk tk xenv)
      (TEX : transl_expr (get_cenv sk) sex = OK tex),
      match_expr_cont (Cstacked.EKthread1 sex sk)
                      (Cminor.EKthread1 tex tk)
                      osp xenv
  | match_EKthread2 : forall sk tk xenv p osp
      (MEK : match_cont sk tk xenv),
      match_expr_cont (Cstacked.EKthread2 p sk)
                      (Cminor.EKthread2 p tk)
                      osp xenv
  | match_EKcondstmt : forall sk tk s1 s2 ts1 ts2 xenv osp
      (MEK : match_cont sk tk xenv)
      (TEX : transl_stmt (get_cenv sk) xenv s1 = OK ts1)
      (TEX : transl_stmt (get_cenv sk) xenv s2 = OK ts2),
      match_expr_cont (Cstacked.EKcondstmt s1 s2 sk)
                      (Cminor.EKcondstmt ts1 ts2 tk)
                      osp xenv
  | match_EKswitch : forall sk tk tk' xenv l tbl osp
      (STBL: switch_table l 0%nat = tbl)
      (MEK : match_cont sk tk xenv)
      (TLS : transl_lblstmt_cont (get_cenv sk) xenv l tk tk'),
      match_expr_cont (Cstacked.EKswitch l sk)
                      (Cminor.EKswitch tbl (length tbl) tk')
                      osp xenv
  | match_EKreturn : forall sk tk xenv osp f
      (CC : Cstacked.get_fundef (Cstacked.call_cont sk) = Some (Internal f))
      (FSIG: sig_res (Csharpminor.fn_sig f) <> None)
      (MEK : match_cont sk tk xenv),
      match_expr_cont (Cstacked.EKreturn sk)
                      (Cminor.EKreturn tk)
                      osp xenv
  | match_EKstoreaddr : forall sk tk xenv c sex tex osp
      (MEK : match_cont sk tk xenv)
      (TEX : transl_expr (get_cenv sk) sex = OK tex),
      match_expr_cont (Cstacked.EKstoreaddr c sex sk)
                      (Cminor.EKstoreaddr c (store_arg c tex) tk)
                      osp xenv
  | match_cast_assign: forall sk tk xenv c cst osp
      (CCE : cast_chunk_eq cst c)
      (MACK: match_assign_chunk_cont sk tk c osp xenv),
      match_expr_cont (Cstacked.EKunop cst sk) tk osp xenv.

Tactic Notation "match_expr_cont_cases" tactic(first) tactic(c) :=
    first; [
      c "match_EKunop" |
      c "match_EKbinop1" |
      c "match_EKbinop2" |
      c "match_EKload" |
      c "match_EKcall" |
      c "match_EKargs" |
      c "match_EKatargs" |
      c "match_EKcond" |
      c "match_EKassign" |
      c "match_EKassign_local" |
      c "match_EKassign_chunk" |
      c "match_EKthread1" |
      c "match_EKthread2" |
      c "match_EKcondstmt" |
      c "match_EKswitch" |
      c "match_EKreturn" |
      c "match_EKstoreaddr" |
      c "match_cast_assign"].

Fixpoint bind_in_env (ids : list ident) (vs : list val)
                     (te : Cminor.env) : Prop :=
  match ids with
    | id :: idr =>
        match vs with
          | v :: vr =>
             bind_in_env idr vr te /\
             match te ! id with
               | Some v' => Val.lessdef v v'
               | None => False
             end
          | nil => bind_in_env idr nil te
        end
    | nil => True
  end.

Inductive match_states : Cstacked.state -> Cminor.state -> Prop :=
  | match_SKexpr: forall sex se sk tex te tk xenv sp
      (TEX : transl_expr (get_cenv_ek sk) sex = OK tex)
      (ME : match_env (get_cenv_ek sk) se te)
      (Esp : sp = se.(csenv_sp))
      (MK : match_expr_cont sk tk se.(csenv_sp) xenv),
      match_states (Cstacked.SKexpr sex se sk)
                   (Cminor.SKexpr tex sp te tk)
  | match_SKexpr_assign: forall sex se sk tex te tk xenv c cst sp
      (TEX : transl_expr (get_cenv_ek sk) sex = OK (Eunop cst tex))
      (ME : match_env (get_cenv_ek sk) se te)
      (CCE : cast_chunk_eq cst c)
      (Esp : sp = se.(csenv_sp))
      (MACK: match_assign_chunk_cont sk tk c se.(csenv_sp) xenv),
      match_states (Cstacked.SKexpr sex se sk)
                   (Cminor.SKexpr tex sp te tk)
  | match_SKval: forall se sk te tk xenv v v' sp
      (ME : match_env (get_cenv_ek sk) se te)
      (LD : Val.lessdef v v')
      (Esp : sp = se.(csenv_sp))
      (MK : match_expr_cont sk tk se.(csenv_sp) xenv),
      match_states (Cstacked.SKval v se sk)
                   (Cminor.SKval v' sp te tk)
  | match_SKval_assign: forall se sk te tk xenv c v v' sp
      (ME : match_env (get_cenv_ek sk) se te)
      (CVC : Val.lessdef (cast_value_to_chunk c v)
                         (cast_value_to_chunk c v'))
      (Esp : sp = se.(csenv_sp))
      (MACK: match_assign_chunk_cont sk tk c sp xenv),
      match_states (Cstacked.SKval v se sk)
                   (Cminor.SKval v' se.(csenv_sp) te tk)
  | match_SKstmt: forall s se sk ts te tk xenv sp
      (TEX : transl_stmt (get_cenv sk) xenv s = OK ts)
      (ME : match_env (get_cenv sk) se te)
      (Esp : sp = se.(csenv_sp))
      (MK : match_cont sk tk xenv),
      match_states (Cstacked.SKstmt s se sk)
                   (Cminor.SKstmt ts sp te tk)
  | match_SKstmt_seq:
      forall s1 s2 sk se ts1 tk sp te xenv
      (TR: transl_stmt (get_cenv sk) xenv s1 = OK ts1)
      (ME : match_env (get_cenv sk) se te)
      (Esp : sp = se.(csenv_sp))
      (MK: match_cont (Cstacked.Kseq s2 sk) tk xenv),
      match_states (Cstacked.SKstmt (Csharpminor.Sseq s1 s2) se sk)
                   (Cminor.SKstmt ts1 sp te tk)
  | match_SKcall_none: forall sk tk xenv args args' e te fn tfn
      (TF : transl_fundef gce fn = OK tfn)
      (LD : Val.lessdef_list args args')
      (ME : match_env (get_cenv sk) e te)
      (MK : match_cont sk tk xenv),
      match_states
        (Cstacked.SKcall args (Cstacked.Kcall None fn e sk))
        (Cminor.SKcall args' (Cminor.Kcall None tfn e.(csenv_sp) te tk))
  | match_SKcall: forall sk tk xenv args args' e te fn tfn s id
      (TF : transl_fundef gce fn = OK tfn)
      (LD : Val.lessdef_list args args')
      (VS : Cminorgen.var_set (get_cenv sk) id (Evar id) = OK s)
      (ME : match_env (get_cenv sk) e te)
      (MK : match_cont sk tk xenv),
      match_states
        (Cstacked.SKcall args (Cstacked.Kcall (Some id) fn e sk))
        (Cminor.SKcall args' (Cminor.Kcall (Some id) tfn e.(csenv_sp)
                               te (Cminor.Kseq s tk)))
  | match_SKexternal: forall sk tk xenv sg oid se te fn ck
      (MK : match_var_set_cont sk tk oid xenv)
      (ME : match_env (get_cenv sk) se te)
      (Eck : ck = Cminor.Kcall oid (External fn) se.(csenv_sp) te tk),
      match_states (Cstacked.SKexternal sg oid se sk)
                   (Cminor.SKexternal sg ck)
  | match_SKexternalReturn: forall sk tk xenv oid se v fn ck te
      (MK : match_var_set_cont sk tk oid xenv)
      (ME : match_env (get_cenv sk) se te)
      (Eck : ck = Cminor.Kcall oid (External fn) se.(csenv_sp) te tk),
      match_states (Cstacked.SKexternalReturn oid v se sk)
                   (Cminor.SKreturn v ck)
  | match_SKreturn: forall sk tk xenv v ov
      (RV : match ov with | Some v' => Val.lessdef v' v
                          | None => v = Vundef end)
      (MK : match_cont sk tk xenv),
      match_states (Cstacked.SKreturn ov sk)
                   (Cminor.SKreturn v tk)
  | match_SKbind: forall pars parids vs te se cenv xenv sk tk fn ts ps sp
      (Ecenv : cenv = get_cenv sk)
      (Eparids : parids = map (@fst _ _) pars)
      (ND : NoDup parids)
      (BIE : bind_in_env parids vs te)
      (ME : match_env cenv se te)
      (Eps : store_parameters cenv pars = OK ps)
      (Ets : transl_stmt cenv xenv fn.(Csharpminor.fn_body) = OK ts)
      (Esp : sp = se.(csenv_sp))
      (MK : match_cont sk tk xenv),
      match_states (Cstacked.SKbind fn vs parids se sk)
                   (Cminor.SKstmt ps sp te (Cminor.Kseq ts tk))
  | match_SKfree_none: forall sp sk tk te xenv f env' k'
      (CC : Cstacked.call_cont sk = Cstacked.Kcall None (Internal f) env' k')
      (FSIG: sig_res (Csharpminor.fn_sig f) = None)
      (MK : match_cont sk tk xenv),
        match_states (Cstacked.SKfree sp None sk)
                   (Cminor.SKstmt (Sreturn None) sp te tk)
  | match_SKfree_some: forall sp sk tk te xenv v v' f env' k' oid
      (CC : Cstacked.call_cont sk = Cstacked.Kcall oid (Internal f) env' k')
      (FSIG: sig_res (Csharpminor.fn_sig f) <> None)
      (LD : Val.lessdef v v')
      (MK : match_cont sk tk xenv),
      match_states (Cstacked.SKfree sp (Some v) sk)
                   (Cminor.SKval v' sp te (Cminor.EKreturn tk)).

Tactic Notation "match_states_cases" tactic(first) tactic(c) :=
    first; [
      c "match_SKexpr" |
      c "match_SKval" |
      c "match_SKstmt" |
      c "match_SKcall" |
      c "match_SKexternal" |
      c "match_SKexternalReturn" |
      c "match_SKreturn" |
      c "match_SKbind" |
      c "match_SKfree_none" |
      c "match_SKfree_some"].


Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat :=
  match s with
  | Csharpminor.Sseq s1 s2 => S (seq_left_depth s1)
  | _ => O
  end.

Definition measure (s : Cstacked.state) : nat :=
  match s with
    | Cstacked.SKbind fn l _ _ _ =>
      (length l + S (S (seq_left_depth fn.(Csharpminor.fn_body)))) %nat
    | Cstacked.SKexpr _ _ (Cstacked.EKassign _ _) => 1%nat
    | Cstacked.SKexpr _ _ (Cstacked.EKstoreval _ _ _) => 1%nat
    | Cstacked.SKval _ _ (Cstacked.EKunop _ _) => 1%nat
    | Cstacked.SKval _ _ (Cstacked.EKreturn _) => 1%nat
    | Cstacked.SKexternalReturn _ _ _ _ => 2%nat
    | Cstacked.SKstmt s _ _ => S (seq_left_depth s)
    | _ => 0%nat
  end.

Definition order := ltof _ measure.

Let slts := (mklts thread_labels (cst_step (ge, gvare))).
Let tlts := (mklts thread_labels (cm_step tge)).

Lemma match_StepSkipBlock:
  forall st env k
    (MS : match_states
           (Cstacked.SKstmt Csharpminor.Sskip env (Cstacked.Kblock k))
           st),
      exists st' : St tlts,
        weakstep tlts st TEtau st' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env k) st'.

Lemma make_cast_taustar_cont:
  forall c x sp te k,
    taustar tlts (SKexpr (make_cast c x) sp te k)
                 (SKexpr x sp te (make_cast_cont c k)).

Lemma cast_val_to_chunk_unop:
  forall op v v' c
    (EU : eval_unop op v = Some v')
    (CCE : cast_chunk_eq op c),
      cast_value_to_chunk c v = cast_value_to_chunk c v'.

Lemma transl_is_store_arg_dest:
  forall {cenv e x} c
    (TEX : transl_expr cenv e = OK x),
      store_arg c x = x \/
      exists s, exists cst, e = Csharpminor.Eunop cst s /\
                cast_chunk_eq cst c.

Lemma step_var_stack_correct:
  forall env id p c v s' k
  (EVR : eval_var_ref (ge, gvare) env id p c)
  (HT : Val.has_type v (type_of_chunk c))
  (MS : match_states (Cstacked.SKexpr (Csharpminor.Evar id) env k) s'),
   exists t' : St tlts,
     weakstep tlts s' (TEmem (MEread p c v)) t' /\
     (forall v' : val,
      Val.lessdef v' v ->
      exists s'' : St slts,
        stepr slts (Cstacked.SKexpr (Csharpminor.Evar id) env k)
          (TEmem (MEread p c v')) s'' /\ match_states s'' t').

Lemma step_addr_correct:
  forall env k s' p id
    (EVA : eval_var_addr (ge, gvare) env id p)
    (MS : match_states (Cstacked.SKexpr (Eaddrof id) env k) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKval (Vptr p) env k) t'.

Lemma step_var_local_correct:
  forall env id v k s'
  (EVL : eval_var_local env id v)
  (MS : match_states (Cstacked.SKexpr (Csharpminor.Evar id) env k) s'),
   exists t',
      weakstep tlts s' TEtau t' /\ match_states (Cstacked.SKval v env k) t'.

Lemma eval_unop_lessdef: forall {op x y x'}
    (EU : eval_unop op x = Some y)
    (LD : Val.lessdef x x'),
      exists y', eval_unop op x' = Some y' /\
                 Val.lessdef y y'.

Lemma eval_binop_lessdef: forall {op x y x' y' z}
    (EU : eval_binop op x y = Some z)
    (LDx : Val.lessdef x x')
    (LDy : Val.lessdef y y'),
      exists z', eval_binop op x' y' = Some z' /\
                 Val.lessdef z z'.

Lemma step_unop_correct:
  forall op v v' env k s'
  (EU : eval_unop op v = Some v')
  (MS : match_states (Cstacked.SKval v env (Cstacked.EKunop op k)) s'),
   order (Cstacked.SKval v' env k)
     (Cstacked.SKval v env (Cstacked.EKunop op k)) /\
   match_states (Cstacked.SKval v' env k) s' \/
   (exists t',
      weakstep tlts s' TEtau t' /\ match_states (Cstacked.SKval v' env k) t').

Lemma step_assign_correct:
  forall id e env k s'
    (MS : match_states (Cstacked.SKstmt (Csharpminor.Sassign id e) env k) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKexpr e env (Cstacked.EKassign id k)) t'.

Lemma step_assign_env_correct:
  forall env id p c k s' v
    (EVR : eval_var_ref (ge, gvare) env id p c)
    (MS : match_states (Cstacked.SKval v env (Cstacked.EKassign id k)) s'),
     exists t' : St tlts,
        exists v' : val,
          Val.lessdef (cast_value_to_chunk c v) v' /\
          weakstep tlts s' (TEmem (MEwrite p c v')) t' /\
          match_states (Cstacked.SKstmt Csharpminor.Sskip env k) t'.

Lemma make_cast_cont_taustar:
  forall c k osp v e,
    exists v',
      taustar tlts (SKval v osp e (make_cast_cont c k))
                   (SKval v' osp e k) /\
      Val.lessdef (Val.load_result c v) v'.

Lemma update_env_match:
  forall cenv env te v v' c id
  (ME : match_env cenv env te)
  (LOC: cenv !! id = Var_local c)
  (LD : Val.lessdef v v'),
    match_env cenv
      (mkcsenv (csenv_sp env) (csenv_env env) ! id <- (Env_local v c))
      te ! id <- v'.

Lemma lessdef_trans:
  forall v1 v2 v3
    (LD1 : Val.lessdef v1 v2)
    (LD2 : Val.lessdef v2 v3),
    Val.lessdef v1 v3.

Lemma step_assign_local_correct:
  forall env id v env' k s'
    (VLS : var_local_store env id v env')
    (MS : match_states (Cstacked.SKval v env (Cstacked.EKassign id k)) s'),
      exists t',
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env' k) t'.

Lemma step_store_correct:
  forall v env c p k s'
    (MS : match_states
         (Cstacked.SKval v env (Cstacked.EKstoreval c (Vptr p) k)) s'),
    exists t', exists v',
        Val.lessdef (cast_value_to_chunk c v) v' /\
        weakstep tlts s' (TEmem (MEwrite p c v')) t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env k) t'.

Lemma step_call_correct:
  forall optid sig e args env k s'
  (MS : match_states
         (Cstacked.SKstmt (Csharpminor.Scall optid sig e args) env k) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states (Cstacked.SKexpr e env (Cstacked.EKcall optid sig args k))
        t'.

Lemma lessdef_list_app:
  forall l1 l1' l2 l2'
    (LD1 : Val.lessdef_list l1 l1')
    (LD2 : Val.lessdef_list l2 l2'),
      Val.lessdef_list (l1 ++ l2) (l1' ++ l2').

Lemma step_call_args_correct:
  forall sig vf fd v e oid vs k s'
  (GFF : Genv.find_funct (Cstacked.ge (ge, gvare)) vf = Some fd)
  (FSIG: Csharpminor.funsig fd = sig)
  (MS : match_states
         (Cstacked.SKval v e (Cstacked.EKargs oid vf sig nil vs k)) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states
        (Cstacked.SKcall (vs ++ v :: nil) (Cstacked.Kcall oid fd e k)) t'.
  
Lemma step_call_args1_correct:
  forall vf e oid sig i is k s'
    (MS : match_states
         (Cstacked.SKval vf e (Cstacked.EKcall oid sig (i :: is) k)) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKexpr i e (Cstacked.EKargs oid vf sig is nil k)) t'.

Lemma step_call_args2_correct:
  forall sig v e oid vf i is vs k s'
    (MS : match_states
           (Cstacked.SKval v e (Cstacked.EKargs oid vf sig (i :: is) vs k)) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states
          (Cstacked.SKexpr i e
             (Cstacked.EKargs oid vf sig is (vs ++ v :: nil) k)) t'.

Lemma step_empty_call_correct:
  forall vf fd e oid sig k s'
  (GFF : Genv.find_funct (Cstacked.ge (ge, gvare)) vf = Some fd)
  (FSIG: Csharpminor.funsig fd = sig)
  (MS : match_states (Cstacked.SKval vf e (Cstacked.EKcall oid sig nil k)) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states (Cstacked.SKcall nil (Cstacked.Kcall oid fd e k)) t'.

Lemma step_exit_seq_correct:
  forall n env s k s'
  (MS : match_states
         (Cstacked.SKstmt (Csharpminor.Sexit n) env (Cstacked.Kseq s k)) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states (Cstacked.SKstmt (Csharpminor.Sexit n) env k) t'.

Lemma step_exit_block_correct:
  forall env k s'
    (MS : match_states
           (Cstacked.SKstmt (Csharpminor.Sexit 0) env (Cstacked.Kblock k)) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env k) t'.

Lemma step_exists_block1_correct:
  forall n env k s'
    (MS : match_states
      (Cstacked.SKstmt (Csharpminor.Sexit (S n)) env (Cstacked.Kblock k)) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKstmt (Csharpminor.Sexit n) env k) t'.

Remark length_switch_table:
  forall sl base1 base2,
  length (switch_table sl base1) = length (switch_table sl base2).

Remark switch_table_shift:
  forall n sl base dfl,
  switch_target n (S dfl) (switch_table sl (S base)) =
  S (switch_target n dfl (switch_table sl base)).

Lemma switch_descent:
  forall {cenv xenv ls body s} k,
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK s ->
  exists k',
  transl_lblstmt_cont cenv xenv ls k k'
  /\ (forall sp e,
      weakstep tlts (SKstmt s sp e k) TEtau (SKstmt body sp e k')).

Lemma step_switch_correct:
  forall e cs env k s'
    (MS : match_states (Cstacked.SKstmt (Csharpminor.Sswitch e cs) env k) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states (Cstacked.SKexpr e env (Cstacked.EKswitch cs k)) t'.

Lemma switch_ascent:
  forall n sp e {cenv xenv k ls k1}
  (TLC : transl_lblstmt_cont cenv xenv ls k k1),
  let tbl := switch_table ls O in
  let ls' := select_switch n ls in
  exists k2,
  taustar tlts (SKstmt (Sexit (switch_target n (length tbl) tbl)) sp e k1)
               (SKstmt (Sexit O) sp e k2)
  /\ transl_lblstmt_cont cenv xenv ls' k k2.

Lemma switch_match_cont:
  forall xenv k tk ls tk',
  match_cont k tk xenv ->
  transl_lblstmt_cont (get_cenv k) xenv ls tk tk' ->
  match_cont (Cstacked.Kseq (seq_of_lbl_stmt ls) k) tk' (false :: switch_env ls xenv).

Lemma transl_lblstmt_suffix:
  forall n cenv xenv ls body ts,
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
  let ls' := select_switch n ls in
  exists body', exists ts',
  transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'.

Lemma switch_match_states:
  forall k e tk te xenv ls tk'
    (ME: match_env (get_cenv k) e te)
    (MK: match_cont k tk xenv)
    (TK: transl_lblstmt_cont (get_cenv k) xenv ls tk tk'),
  exists S,
     weakstep tlts (SKstmt (Sexit O) e.(csenv_sp) te tk') TEtau S
  /\ match_states (Cstacked.SKstmt (seq_of_lbl_stmt ls) e k) S.

Lemma step_select_correct:
  forall n env cs k s'
    (MS : match_states
      (Cstacked.SKval (Vint n) env (Cstacked.EKswitch cs k)) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states
          (Cstacked.SKstmt (seq_of_lbl_stmt (select_switch n cs)) env k) t'.


Section FIND_LABEL.

Variable lbl: label.

Remark find_label_var_set:
  forall cenv id e s k,
  var_set cenv id e = OK s ->
  find_label lbl s k = None.

Lemma transl_lblstmt_find_label_context:
  forall cenv xenv ls body ts tk1 tk2 ts' tk',
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
  transl_lblstmt_cont cenv xenv ls tk1 tk2 ->
  find_label lbl body tk2 = Some (ts', tk') ->
  find_label lbl ts tk1 = Some (ts', tk').

Lemma transl_find_label:
  forall s k xenv ts tk,
  transl_stmt (get_cenv k) xenv s = OK ts ->
  match_cont k tk xenv ->
  match Cstacked.find_label lbl s k with
  | None => find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk', exists xenv',
        find_label lbl ts tk = Some(ts', tk')
     /\ transl_stmt (get_cenv k') xenv' s' = OK ts'
     /\ match_cont k' tk' xenv'
     /\ get_cenv k = get_cenv k'
  end

with transl_lblstmt_find_label:
  forall ls xenv body k ts tk tk1,
  transl_lblstmt (get_cenv k) (switch_env ls xenv) ls body = OK ts ->
  match_cont k tk xenv ->
  transl_lblstmt_cont (get_cenv k) xenv ls tk tk1 ->
  find_label lbl body tk1 = None ->
  match Cstacked.find_label_ls lbl ls k with
  | None => find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk', exists xenv',
        find_label lbl ts tk = Some(ts', tk')
     /\ transl_stmt (get_cenv k') xenv' s' = OK ts'
     /\ match_cont k' tk' xenv'
     /\ get_cenv k = get_cenv k'
  end.

Remark find_label_store_parameters:
  forall cenv vars s k,
  store_parameters cenv vars = OK s -> find_label lbl s k = None.

End FIND_LABEL.

Lemma call_cont_related:
  forall sk tk xenv
    (MK : match_cont sk tk xenv),
      match_cont (Cstacked.call_cont sk) (call_cont tk) nil.

Lemma transl_find_label_body:
  forall {xenv f k tk lbl s' k'}
  (GFD : Cstacked.get_fundef (Cstacked.call_cont k) = (Some (Internal f)))
  (MK : match_cont k tk xenv)
  (FL : Cstacked.find_label lbl f.(Csharpminor.fn_body) (Cstacked.call_cont k) = Some (s', k')),
  exists tf, exists ts', exists tk', exists xenv',
     Cminor.get_fundef (Cminor.call_cont tk) = (Some (Internal tf))
  /\ find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk')
  /\ transl_stmt (get_cenv k') xenv' s' = OK ts'
  /\ match_cont k' tk' xenv'
  /\ get_cenv k = get_cenv k'.

Lemma step_goto_correct:
  forall k k' f lbl s' s'' k'' env
    (CC : Cstacked.call_cont k = k')
    (GFD : Cstacked.get_fundef k' = Some (Internal f))
    (FL : Cstacked.find_label lbl (Csharpminor.fn_body f) k' = Some (s'', k''))
    (MS : match_states (Cstacked.SKstmt (Csharpminor.Sgoto lbl) env k) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKstmt s'' env k'') t'.

Lemma ptree_set_set:
  forall A t id (e e': A),
    (t ! id <- e) ! id <- e' = t ! id <- e'.

Lemma step_return_finish_local_correct:
  forall k id fd env' k' v env'' s'
    (CC : Cstacked.call_cont k = Cstacked.Kcall (Some id) fd env' k')
    (VLS : var_local_store env' id v env'')
    (MS : match_states (Cstacked.SKreturn (Some v) k) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env'' k') t'.

Lemma update_env_match_non_local:
  forall cenv env te v id
  (ME : match_env cenv env te)
  (LOC: match cenv !! id with Var_local _ => False | _ => True end),
    match_env cenv env te ! id <- v.

Lemma step_return_finish_mem_correct:
  forall k id fd env' k' p c s' v
    (CC : Cstacked.call_cont k = Cstacked.Kcall (Some id) fd env' k')
    (EVR : eval_var_ref (ge, gvare) env' id p c)
    (MS : match_states (Cstacked.SKreturn (Some v) k) s'),
      exists t' : St tlts, exists v' : val,
        Val.lessdef (cast_value_to_chunk c v) v' /\
        weakstep tlts s' (TEmem (MEwrite p c v')) t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env' k') t'.

Lemma step_bind_args_stack_correct:
  forall env id c ofs sp v vs args k s' f
    (EG : (csenv_env env) ! id = Some (Env_stack_scalar c ofs))
    (EB : csenv_sp env = Some sp)
    (MS : match_states (SKbind f (v :: vs) (id :: args) env k) s'),
      exists t' : St tlts, exists v' : val,
        Val.lessdef (cast_value_to_chunk c v) v' /\
        weakstep tlts s' (TEmem (MEwrite (sp + Int.repr ofs) c v')) t' /\
        match_states (SKbind f vs args env k) t'.

Lemma bind_in_env_other:
  forall id l vs e v
    (NIN: ~ In id l)
    (BIE: bind_in_env l vs e),
      bind_in_env l vs (e ! id <- v).

Lemma step_bind_args_env_correct:
  forall env id env' v vs args f k s'
    (VLS : var_local_store env id v env')
    (MS : match_states (SKbind f (v :: vs) (id :: args) env k) s'),
      exists t' : St tlts,
        weakstep tlts s' TEtau t' /\ match_states (SKbind f vs args env' k) t'.

Lemma bind_in_env_set_params:
  forall l vs vs'
    (ND : NoDup l)
    (LD : Val.lessdef_list vs vs'),
      bind_in_env l vs (set_params vs' l).

Remark identset_removelist_charact:
  forall l s x, Identset.In x (identset_removelist l s) <-> Identset.In x s /\ ~In x l.

Remark InA_In:
  forall (A: Type) (x: A) (l: list A),
  InA (fun (x y: A) => x = y) x l <-> In x l.

Remark NoDupA_norepet:
  forall (A: Type) (l: list A),
  NoDupA (fun (x y: A) => x = y) l -> NoDup l.

Lemma make_vars_norepet:
  forall fn body,
  NoDup (fn_params_names fn ++ fn_vars_names fn) ->
  NoDup (make_vars (fn_params_names fn) (fn_vars_names fn) body
         ++ fn_params_names fn).

Lemma bind_env_disjoint:
  forall l' l vs e
  (DISJ: list_disjoint l l')
  (BIE : bind_in_env l vs e),
    bind_in_env l vs (set_locals l' e).

Lemma pars_vars_eq_fn_variables:
  forall fn,
    fn_params_names fn ++ fn_vars_names fn =
    map (@fst _ _) (fn_variables fn).

Lemma set_params_defined:
  forall params args id,
  In id params -> (set_params args params)!id <> None.

Lemma set_locals_defined:
  forall e vars id,
  In id vars \/ e!id <> None -> (set_locals vars e)!id <> None.

Lemma set_locals_params_defined:
  forall args params vars id,
  In id (params ++ vars) ->
  (set_locals vars (set_params args params))!id <> None.

Lemma assign_variables_not_in:
  forall {vr v ids ce s ce' s'},
  ~ In v (map (@fst _ _) vr) ->
  assign_variables ids vr (ce, s) = (ce', s') ->
  ce !! v = ce' !! v.

Lemma build_compilenv_not_in:
  forall id f cenv cenv' sz
   (NIN : ~ In id (map (@fst _ _) (fn_variables f)))
   (BCE : build_compilenv cenv f = (cenv', sz)),
     cenv !! id = cenv' !! id.

Lemma assign_variable_agree:
  forall vars n g1 g2 cenv1 cenv2 sz1 sz2 s
   (ND : NoDup (map (@fst _ _) vars))
   (AV1 : assign_variables s vars (g1, n) = (cenv1, sz1))
   (AV2 : assign_variables s vars (g2, n) = (cenv2, sz2)),
     sz1 = sz2 /\
     forall id : ident, In id (map (@fst _ _) vars) -> cenv1 !! id = cenv2 !! id.

Lemma build_compileenv_agree:
  forall {f g1 cenv1 sz1 g2 cenv2 sz2}
  (ND : NoDup (fn_params_names f ++ fn_vars_names f))
  (BCE1 : build_compilenv g1 f = (cenv1, sz1))
  (BCE2 : build_compilenv g2 f = (cenv2, sz2)),
    sz1 = sz2 /\
    forall id (IN : In id (fn_params_names f ++ fn_vars_names f)),
       cenv1 !! id = cenv2 !! id.

Lemma build_env_agree:
  forall {f cenv sz1 g nenv sz2}
  (ND : NoDup (fn_params_names f ++ fn_vars_names f))
  (BEM : build_env f = Some (nenv, sz1))
  (BCE : build_compilenv g f = (cenv, sz2)),
    sz1 = sz2.

Lemma build_envmap_not_in:
  forall {id cenv e vars acc}
   (EM : build_envmap vars cenv acc = Some e)
   (NIN: ~ In id (map (@fst _ _) vars)),
     e ! id = acc ! id.

Lemma match_env_item_build_envmap:
  forall cenv cenv' te e sp id vars acc
  (ND : NoDup (map (@fst _ _) vars))
  (EM : build_envmap vars cenv' acc = Some e)
  (AG : forall id, In id (map (@fst _ _) vars) -> cenv !! id = cenv' !! id)
  (TEU: forall id, In id (map (@fst _ _) vars) -> te ! id <> None)
  (IN : In id (map (@fst _ _) vars))
  (SP : match (cenv !! id) with
          | Var_stack_scalar _ _ => sp <> None
          | Var_stack_array _ => sp <> None
          | _ => True
        end),
    match_env_item id (cenv !! id) (e ! id) (te ! id) sp.

Definition global_match gce gvare :=
  forall id,
    match gce !! id, gvare ! id with
      | Var_global_scalar c, Some (Vscalar c') => c = c'
      | Var_global_array, Some (Varray _) => True
      | Var_global_array, None => True
      | _, _ => False
    end.

Lemma gce_gvare_match: global_match gce gvare.

Lemma global_scalar_impl_find_symb:
  forall id
    (VG: match gce !! id with Var_global_scalar _ => True | _ => False end),
      Genv.find_symbol ge id <> None.

Lemma match_env_gce:
  forall sp te,
    match_env gce (mkcsenv sp (PTree.empty _)) te.

Lemma array_alignment_pos:
  forall sz, array_alignment sz > 0.

Lemma align_size_chunk_le:
  forall n c, n <= align n (size_chunk c).


Lemma assign_variables_mono:
  forall {ids vars ie n ce sz},
    assign_variables ids vars (ie, n) = (ce, sz) ->
    n <= sz.

Lemma build_compilenv_empty:
  forall cenv' id vars s cenv
  (IN : In id (map (@fst _ _) vars))
  (AV : assign_variables s vars (cenv, 0) = (cenv', 0)),
    match (cenv' !! id) with
      | Var_stack_scalar _ _ => False
      | Var_stack_array _ => False
      | _ => True
    end.

Lemma match_env_build_env:
  forall f nenv fsize vs args' cenv sz s osp
    (ND : NoDup (fn_params_names f ++ fn_vars_names f))
    (BE : build_env f = Some (nenv, fsize))
    (LD : Val.lessdef_list vs args')
    (SP : match osp with
            | Some sp => True
            | None => fsize = 0
          end)
    (BCE: build_compilenv gce f = (cenv, sz)),
      match_env cenv (mkcsenv osp nenv)
        (set_locals
           (make_vars (fn_params_names f) (fn_vars_names f) s)
           (set_params args' (fn_params_names f))).

Lemma step_function_internal_with_stack_correct:
  forall ck optid f env k nenv fsize vs sp s'
    (CC : ck = Cstacked.Kcall optid (Internal f) env k)
    (BE : build_env f = Some (nenv, fsize))
    (FNZ : fsize <> 0%Z)
    (ND : NoDup (map (@fst _ _) (fn_variables f)))
    (MS : match_states (Cstacked.SKcall vs ck) s'),
    exists t' : St tlts,

      weakstep tlts s' (TEmem (MEalloc sp (Int.repr fsize) MObjStack)) t' /\
      match_states
        (SKbind f vs (map (@fst _ _) (Csharpminor.fn_params f))
           (mkcsenv (Some sp) nenv) ck) t'.

Lemma step_function_internal_no_stack_correct:
  forall ck optid f env k nenv s' vs
    (CC : ck = Cstacked.Kcall optid (Internal f) env k)
    (BE : build_env f = Some (nenv, 0%Z))
    (ND : NoDup (map (@fst _ _) (fn_variables f)))
    (MS : match_states (Cstacked.SKcall vs ck) s'),
   exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states
        (SKbind f vs (map (@fst _ _) (Csharpminor.fn_params f))
           (mkcsenv None nenv) ck) t'.

Lemma step_stop_correct:
  forall env s'
  (MS : match_states (Cstacked.SKstmt Csharpminor.Sskip env Cstacked.Kstop) s'),
    exists t' : St tlts,
      weakstep tlts s' TEexit t' /\
      match_states (Cstacked.SKstmt Csharpminor.Sskip env Cstacked.Kstop) t'.

Lemma step_next_correct:
  forall env s k s'
  (MS : match_states
         (Cstacked.SKstmt Csharpminor.Sskip env (Cstacked.Kseq s k)) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\ match_states (Cstacked.SKstmt s env k) t'.
    
Lemma step_external_store_mem_correct:
  forall env tgt p c vres k s'
  (EVR : eval_var_ref (ge, gvare) env tgt p c)
  (MS : match_states (SKexternalReturn (Some tgt) vres env k) s'),
    exists t' : St tlts,
      exists v' : val,
        Val.lessdef (cast_value_to_chunk c vres) v' /\
        weakstep tlts s' (TEmem (MEwrite p c v')) t' /\
        match_states (Cstacked.SKstmt Csharpminor.Sskip env k) t'.

Lemma step_external_store_env_correct:
  forall env tgt vres env' k s'
  (VLS : var_local_store env tgt vres env')
  (MS : match_states (SKexternalReturn (Some tgt) vres env k) s'),
    exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states (Cstacked.SKstmt Csharpminor.Sskip env' k) t'.

Lemma atomic_correct:
  forall optid astmt e es env k s'
   (MS : match_states
         (Cstacked.SKstmt (Csharpminor.Satomic optid astmt (e :: es)) env k)
         s'),
   (exists t' : St tlts,
      weakstep tlts s' TEtau t' /\
      match_states
        (Cstacked.SKexpr e env (Cstacked.EKatargs optid astmt es nil k)) t').

Lemma sem_atomic_statement_lessdef:
  forall astmt vs vs' p rmwi
  (SAS: sem_atomic_statement astmt vs = Some (p, rmwi))
  (LD : Val.lessdef_list vs vs'),
   sem_atomic_statement astmt vs' = Some (p, rmwi).

Lemma cminorgen_step_correct:
  forward_sim_with_undefs2 slts tlts match_states order.

Definition bsim_rel := @bsr _ slts tlts match_states.
Definition bsim_order := @bsc _ tlts.

Lemma cst_cm_backward_sim:
  @backward_sim_with_undefs _ slts tlts te_ldo te_ldi
                           bsim_rel bsim_order.

Lemma cshmgen_init:
  forall p vs vs'
    (LD : Val.lessdef_list vs vs'),
    match Cstacked.cst_init (ge, gvare) p vs, cm_init tge p vs' with
      | Some s, Some t => match_states s t
      | None, None => True
      | _, _ => False
    end.

End TRANSLATION.


Definition full_genv_rel (sge : cst_sem.(SEM_GE))
                         (tge : cm_sem.(SEM_GE)) : Prop :=
  exists prog,
    genv_rel prog (fst sge) tge /\
    snd sge = global_var_env prog /\
    forall id, In id (map (fun x => fst (fst x)) (prog_vars prog)) ->
               Genv.find_symbol (fst sge) id <> None.

Definition cst_cm_match_prg (prog : cst_sem.(SEM_PRG))
                            (tprog : cm_sem.(SEM_PRG)) : Prop :=
  transl_program prog = OK tprog.

Definition full_bsim_rel (ge : SEM_GE cst_sem) (tge : SEM_GE cm_sem)
                         (cms : SEM_ST cm_sem) (css : SEM_ST cst_sem) :=
  exists prog,
    snd ge = global_var_env prog /\
    genv_rel prog (fst ge) tge /\
    (forall id, In id (map (fun x => fst (fst x)) (prog_vars prog)) ->
                Genv.find_symbol (fst ge) id <> None) /\
    bsim_rel prog (fst ge) tge cms css.

Theorem cst_cminor_sim :
  Sim.sim tso_mm tso_mm cst_sem cm_sem cst_cm_match_prg.