Module SimplLocalsproof

Require Import FSets.
Require FSetAVL.
Require Import Coqlib.
Require Import Errors.
Require Import Ordered.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import SimplLocals.
Require Import ExprEval.
Require Import Memory.
Require Import VarSort.
Require Import Psatz.
Require Import ClightRel.
Require Import MemRel Align Tactics ForgetNorm MemReserve.
Require Import BlockAppears InjectWellBehaved.

Opaque Mem.nb_boxes_max.

Module VSF := FSetFacts.Facts(VSet).
Module VSP := FSetProperties.Properties(VSet).

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSF: transf_program prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv 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 m (v: expr_sym) (f: fundef),
  Genv.find_funct m ge v = Some f ->
  exists tf, Genv.find_funct m tge v = Some tf /\ transf_fundef f = OK tf.

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

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



Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (tle: temp_env) (id: ident) : Prop :=
  | match_var_lifted: forall b ty chunk v tv
      (ENV: e!id = Some(b, ty))
      (TENV: te!id = None)
      (LIFTED: VSet.mem id cenv = true)
      (MAPPED: f b = None)
      (MODE: access_mode ty = By_value chunk)
      (LOAD: Mem.load chunk m b 0 = Some v)
      (TLENV: tle!(id) = Some tv)
      (VINJ: expr_inj_se f v tv),
      match_var f cenv e m te tle id
  | match_var_not_lifted: forall b ty b'
      (ENV: e!id = Some(b, ty))
      (TENV: te!id = Some(b', ty))
      (LIFTED: VSet.mem id cenv = false)
      (MAPPED: f b = Some (b',0)),
      match_var f cenv e m te tle id
  | match_var_not_local: forall
      (ENV: e!id = None)
      (TENV: te!id = None)
      (LIFTED: VSet.mem id cenv = false),
      match_var f cenv e m te tle id.



Record match_envs (f: meminj) (cenv: compilenv)
                  (e: env) (le: temp_env) (m tm: mem) (lo hi: block)
                  (te: env) (tle: temp_env) (tlo thi : block) : Prop :=
  mk_match_envs {
    me_vars:
      forall id, match_var f cenv e m te tle id;
    me_temps:
      forall id v,
      le!id = Some v ->
      (exists tv, tle!id = Some tv /\ expr_inj_se f v tv)
      /\ (VSet.mem id cenv = true -> v = Eval Vundef);
    me_bounds:
      forall id b ty, e!id = Some (b,ty) -> Mem.bounds_of_block m b = (0, sizeof ty);
    me_bounds_same:
      forall id b ty b' delta, e!id = Some (b,ty) -> f b = Some (b',delta) -> Mem.bounds_of_block m b = Mem.bounds_of_block tm b';
    me_inj:
      forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2;
    me_range:
      forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi;
    me_trange:
      forall id b ty, te!id = Some(b, ty) -> Ple tlo b /\ Plt b thi;
    me_mapped:
      forall id b' ty,
      te!id = Some(b', ty) -> exists b, f b = Some(b', 0) /\ e!id = Some(b, ty);
    me_flat:
      forall id b' ty b delta,
      te!id = Some(b', ty) -> f b = Some(b', delta) -> e!id = Some(b, ty) /\ delta = 0;
    me_incr:
      Ple lo hi;
    me_tincr:
      Ple tlo thi;
    me_not_dynamic_e: Forall (fun b => ~ Mem.is_dynamic_block m b) (map fst (map fst (blocks_of_env e)));
    me_not_dynamic_te: Forall (fun b => ~ Mem.is_dynamic_block tm b) (map fst (map fst (blocks_of_env te)))
    }.


Lemma assign_loc_bounds:
  forall ty m e1 e2 m'
    (AL: assign_loc ty m e1 e2 m')
    b,
    Mem.bounds_of_block m b = Mem.bounds_of_block m' b.

Lemma assign_loc_mask:
  forall ty m e1 e2 m'
    (AL: assign_loc ty m e1 e2 m')
    b,
    Mem.mask m b = Mem.mask m' b.

Lemma assign_loc_nextblock:
  forall ty m bofs v m',
  assign_loc ty m bofs v m' -> Mem.nextblock m' = Mem.nextblock m.

Lemma assign_loc_mk_block_list:
  forall m m' ty a b
    (AL: assign_loc ty m a b m'),
    Mem.mk_block_list m = Mem.mk_block_list m'.


Lemma assign_loc_nb_extra:
  forall m m' ty a b
    (AL: assign_loc ty m a b m'),
    Mem.nb_extra m = Mem.nb_extra m'.

Lemma assign_loc_size_mem:
  forall m m' ty a b
    (AL: assign_loc ty m a b m'),
    Mem.nb_boxes_used_m m = Mem.nb_boxes_used_m m'.

Lemma in_blocks_of_env:
  forall x e, In x (blocks_of_env e) ->
         exists i t, sizeof t = snd x /\
                snd (fst x) = 0 /\
                e ! i = Some (fst (fst x), t).

Lemma in_blocks_of_env':
  forall e i b t
    (EI: e ! i = Some (b,t)),
    In b (map fst (map fst (blocks_of_env e))).


Lemma in_blocks_of_env_forall:
  forall e i b t
    (EI: e ! i = Some (b,t))
    P (F: Forall P (map fst (map fst (blocks_of_env e)))),
    P b.

Lemma in_forall:
  forall {A: Type} (b: A) l P,
    Forall P l ->
    In b l ->
    P b.

Lemma blocks_of_env_impl:
  forall b e (P: block -> Prop),
    In b (map fst (map fst (blocks_of_env e))) ->
    (forall i b t, e ! i = Some (b,t) -> P b) ->
    P b.

Lemma match_envs_invariant:
  forall f cenv e le m tm lo hi te tle tlo thi f' m' tm'
    (ME: match_envs f cenv e le m tm lo hi te tle tlo thi)
    (LD: forall b chunk v,
        f b = None ->
        Ple lo b /\ Plt b hi ->
        Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v)
    (BOUNDS: forall b, Plt b hi -> ~ Mem.is_dynamic_block m b ->
                  Mem.bounds_of_block m b = Mem.bounds_of_block m' b)
    (BOUNDS': forall b, Plt b thi -> ~ Mem.is_dynamic_block tm b ->
                   Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (INCR: inject_incr f f')
    (INV1: forall b, Ple lo b /\ Plt b hi -> f' b = f b)
    (INV2: forall b b' delta, f' b = Some(b', delta) -> Ple tlo b' /\ Plt b' thi -> f' b = f b)
    (DYNinject: forall b b' delta,
        f b = Some (b',delta) ->
        (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block tm b'))
    (DYNsame: forall b, Plt b hi ->
                   (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b))
    (DYNsame': forall b, Plt b thi ->
                    (Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b)),
    match_envs f' cenv e le m' tm' lo hi te tle tlo thi.

Lemma match_envs_extcall:
  forall f cenv e le m lo hi te tle tlo thi tm f' m' tm'
    (ME: match_envs f cenv e le m tm lo hi te tle tlo thi)
    (UNCH: Mem.unchanged_on (loc_unmapped f) m m')
    (Bnds: forall b, Plt b hi -> ~ Mem.is_dynamic_block m b ->
                Mem.bounds_of_block m b = Mem.bounds_of_block m' b)
    (Bnds':forall b, Plt b thi -> ~ Mem.is_dynamic_block tm b ->
                Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (INCR: inject_incr f f')
    (SEP: inject_separated f f' m tm)
    (PLE1: Ple hi (Mem.nextblock m)) (PLE2: Ple thi (Mem.nextblock tm))
      (DYNinject: forall b b' delta,
        f b = Some (b',delta) ->
        (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block tm b'))
    (DYNsame: forall b, Plt b hi ->
                   (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b))
    (DYNsame': forall b, Plt b thi ->
                    (Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b)),
    match_envs f' cenv e le m' tm' lo hi te tle tlo thi.






Lemma make_cast_correct:
  forall e le m a v1 tto v2,
  eval_expr tge e le m a v1 ->
  sem_cast_expr v1 (typeof a) tto = Some v2 ->
  eval_expr tge e le m (make_cast a tto) v2.

Definition expr_casted (e: expr_sym) (ty: type) :=
  exists e', sem_cast_expr e ty ty = Some e' /\ same_eval e e'.

Lemma expr_casted_load_result:
  forall v ty chunk,
    expr_casted v ty -> access_mode ty = By_value chunk ->
    same_eval (Val.load_result chunk v) v.


Lemma sem_cast_expr_casted:
  forall e ty e'
    (SCE: sem_cast_expr e ty ty = Some e'),
    expr_casted e' ty.

Lemma match_envs_assign_lifted:
  forall f cenv e le m tm lo hi te tle tlo thi b ty v m' id tv
    (MENV: match_envs f cenv e le m tm lo hi te tle tlo thi)
    (EID: e!id = Some(b, ty))
    (SCE: expr_casted v ty)
    (EI: expr_inj_se f v tv)
    (AL: assign_loc ty m (Eval (Vptr b Int.zero)) v m')
    (VMEM: VSet.mem id cenv = true),
  match_envs f cenv e le m' tm lo hi te (PTree.set id tv tle) tlo thi.


Lemma match_envs_set_temp:
  forall f cenv e le m lo hi te tle tlo thi id v tv x tm ,
  match_envs f cenv e le m tm lo hi te tle tlo thi ->
  expr_inj_se f v tv ->
  check_temp cenv id = OK x ->
  match_envs f cenv e (PTree.set id v le) m tm lo hi te (PTree.set id tv tle) tlo thi.

Lemma match_envs_set_opttemp:
  forall f cenv e le m tm lo hi te tle tlo thi optid v tv x,
  match_envs f cenv e le m tm lo hi te tle tlo thi ->
  expr_inj_se f v tv ->
  check_opttemp cenv optid = OK x ->
  match_envs f cenv e (set_opttemp optid v le) m tm lo hi
             te (set_opttemp optid tv tle) tlo thi.


Lemma match_envs_temps_exten:
  forall f cenv e le m tm lo hi te tle tlo thi tle',
  match_envs f cenv e le m tm lo hi te tle tlo thi ->
  (forall id, tle'!id = tle!id) ->
  match_envs f cenv e le m tm lo hi te tle' tlo thi.


Lemma match_envs_change_temp:
  forall f cenv e le m tm lo hi te tle tlo thi id v,
  match_envs f cenv e le m tm lo hi te tle tlo thi ->
  le!id = None -> VSet.mem id cenv = false ->
  match_envs f cenv e le m tm lo hi te (PTree.set id v tle) tlo thi.


Definition cenv_for_gen (atk: VSet.t) (vars: list (ident * type)) : compilenv :=
  List.fold_right (add_local_variable atk) VSet.empty vars.

Remark add_local_variable_charact:
  forall id ty atk cenv id1,
  VSet.In id1 (add_local_variable atk (id, ty) cenv) <->
  VSet.In id1 cenv \/ exists chunk, access_mode ty = By_value chunk /\ id = id1 /\ VSet.mem id atk = false.

Lemma cenv_for_gen_domain:
 forall atk id vars, VSet.In id (cenv_for_gen atk vars) -> In id (var_names vars).

Lemma cenv_for_gen_by_value:
  forall atk id ty vars,
  In (id, ty) vars ->
  list_norepet (var_names vars) ->
  VSet.In id (cenv_for_gen atk vars) ->
  exists chunk, access_mode ty = By_value chunk.

Lemma cenv_for_gen_compat:
  forall atk id vars,
  VSet.In id (cenv_for_gen atk vars) -> VSet.mem id atk = false.


Definition compat_cenv (atk: VSet.t) (cenv: compilenv) : Prop :=
  forall id, VSet.In id atk -> VSet.In id cenv -> False.

Lemma compat_cenv_for:
  forall f, compat_cenv (addr_taken_stmt f.(fn_body)) (cenv_for f).

Lemma compat_cenv_union_l:
  forall atk1 atk2 cenv,
  compat_cenv (VSet.union atk1 atk2) cenv -> compat_cenv atk1 cenv.

Lemma compat_cenv_union_r:
  forall atk1 atk2 cenv,
  compat_cenv (VSet.union atk1 atk2) cenv -> compat_cenv atk2 cenv.

Lemma compat_cenv_empty:
  forall cenv, compat_cenv VSet.empty cenv.

Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.


Lemma alloc_variables_nextblock:
  forall e m vars e' m',
  alloc_variables e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').

Lemma alloc_variables_range:
  forall id b ty e m vars e' m',
  alloc_variables e m vars e' m' ->
  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m').

Lemma alloc_variables_injective:
  forall id1 b1 ty1 id2 b2 ty2 e m vars e' m',
  alloc_variables e m vars e' m' ->
  (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) ->
  (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) ->
  (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2).






Inductive cenv_bound (cenv: compilenv) : list (ident*type) -> Prop :=
| cb_nil: cenv_bound cenv nil
| cb_cons: forall l i ty, cenv_bound cenv l ->
                     (0 < sizeof ty <= 8 \/ VSet.mem i cenv = false) ->
                     cenv_bound cenv ((i,ty)::l).






Lemma alloc_variables_load:
  forall e m vars e' m',
  alloc_variables e m vars e' m' ->
  forall chunk b ofs v,
  Mem.load chunk m b ofs = Some v ->
  Mem.load chunk m' b ofs = Some v.

Lemma sizeof_by_value:
  forall ty chunk,
  access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty.

Definition env_initial_value (e: env) (m: mem) :=
  forall id b ty chunk,
    e!id = Some(b, ty) -> access_mode ty = By_value chunk ->
    exists v, Mem.load chunk m b 0 = Some v /\ same_eval v (Eval Vundef).


Lemma alloc_load:
  forall m hi m' b bt
    (ALLOC: Mem.alloc m 0 hi bt = Some (m', b))
    chunk o (OFS: 0 <= o < hi) (OFS': o + size_chunk chunk <= hi),
    (align_chunk chunk | o) ->
    exists v, Mem.load chunk m' b o = Some v /\ same_eval v (Eval Vundef).

Lemma alloc_variables_initial_value:
  forall e m vars e' m',
  alloc_variables e m vars e' m' ->
  env_initial_value e m ->
  env_initial_value e' m'.

Lemma create_undef_temps_charact:
  forall id ty vars, In (id, ty) vars -> (create_undef_temps vars)!id = Some (Eval Vundef).

Lemma create_undef_temps_inv:
  forall vars id v, (create_undef_temps vars)!id = Some v -> v = (Eval Vundef) /\ In id (var_names vars).

Lemma create_undef_temps_exten:
  forall id l1 l2,
  (In id (var_names l1) <-> In id (var_names l2)) ->
  (create_undef_temps l1)!id = (create_undef_temps l2)!id.

Remark var_names_app:
  forall vars1 vars2, var_names (vars1 ++ vars2) = var_names vars1 ++ var_names vars2.

Remark filter_app:
  forall (A: Type) (f: A -> bool) l1 l2,
  List.filter f (l1 ++ l2) = List.filter f l1 ++ List.filter f l2.

Remark filter_norepet:
  forall (A: Type) (f: A -> bool) l,
  list_norepet l -> list_norepet (List.filter f l).

Remark filter_map:
  forall (A B: Type) (f: A -> B) (pa: A -> bool) (pb: B -> bool),
  (forall a, pb (f a) = pa a) ->
  forall l, List.map f (List.filter pa l) = List.filter pb (List.map f l).

Lemma create_undef_temps_lifted:
  forall id f,
  ~ In id (var_names (fn_params f)) ->
  (create_undef_temps (add_lifted (cenv_for f) (fn_vars f) (fn_temps f))) ! id =
  (create_undef_temps (add_lifted (cenv_for f) (fn_params f ++ fn_vars f) (fn_temps f))) ! id.

Lemma vars_and_temps_properties:
  forall cenv params vars temps,
  list_norepet (var_names params ++ var_names vars) ->
  list_disjoint (var_names params) (var_names temps) ->
  list_norepet (var_names params)
  /\ list_norepet (var_names (remove_lifted cenv (params ++ vars)))
  /\ list_disjoint (var_names params) (var_names (add_lifted cenv vars temps)).

Lemma alloc_variables_in_not_in_vars:
  forall e m1 vars e2 m2
    (AV: alloc_variables e m1 vars e2 m2)
    id0 (N: ~ In id0 (var_names vars)),
    e2 ! id0 = e ! id0.

Lemma alloc_variables_bounds_other:
  forall e m1 vars e2 m2
    (AV : alloc_variables e m1 vars e2 m2)
    (Valid: forall id b ty, e!id = Some (b,ty) -> Mem.valid_block m1 b)
    id0 b ty0 (E : e2 ! id0 = Some (b, ty0))
    (n : In id0 (var_names vars) -> False),
    Mem.bounds_of_block m2 b = Mem.bounds_of_block m1 b.

Lemma alloc_variables_bounds:
  forall e m vars m' e'
    (AV: alloc_variables e m vars e' m')
    (Valid: forall id b ty, e!id = Some (b,ty) -> Mem.valid_block m b)
    id b ty
    (I: In id (var_names vars))
    (E: e' ! id = Some (b,ty)),
    Mem.bounds_of_block m' b = (0, sizeof ty).

Definition free_blocks (m1 m2: mem) (n: nat) :=
  (Mem.nb_boxes_used_m m2 + n <= Mem.nb_boxes_used_m m1)%nat.

Lemma free_blocks_more:
  forall m tm n n' (LE: (n' <= n)%nat)
    (FB: free_blocks m tm n),
    free_blocks m tm n'.

Lemma Sle_le:
  forall (a b: nat),
    (S a <= b)%nat -> (a <= b)%nat.

Lemma box_span_small:
  forall x : Z, 0 < x <= two_power_nat MA ->
           Mem.box_span x = S O.

Lemma free_blocks_alloc:
  forall m tm k bt,
    free_blocks m tm (S k) ->
    exists tm' b,
      Mem.alloc tm 0 8 bt = Some (tm',b) /\
      free_blocks m tm' k.


Lemma free_blocks_reserve_boxes:
  forall k k' m tm,
    free_blocks m tm k ->
    (k' <= k)%nat ->
    exists tm',
      MemReserve.reserve_boxes tm k' = Some tm' /\
      free_blocks m tm' (k - k').

Lemma free_blocks_alloc_bytes_1:
  forall k k' m tm m'
    (FrB: free_blocks m tm k)
    (AB: MemReserve.reserve_boxes m k' = Some m'),
    free_blocks m' tm (k + k').

Ltac genAlloc := Mem.genAlloc.

Lemma alloc_bytes_load:
  forall m n m'
    (AB: MemReserve.reserve_boxes m n = Some m')
    b (PLT: Plt b (Mem.nextblock m))
    chunk o,
    Mem.load chunk m' b o = Mem.load chunk m b o.

Lemma load_valid_block:
  forall m chunk b ofs v,
    Mem.load chunk m b ofs = Some v ->
    Mem.valid_block m b.

Lemma cenv_bound_add:
  forall l e i,
    cenv_bound e l ->
    (forall t, In (i,t) l -> 0 < sizeof t <= 8) ->
    cenv_bound (VSet.add i e) l.

Lemma access_mode_value_s8:
  forall t m,
    access_mode t = By_value m ->
    0 < sizeof t <= 8.

Lemma not_int_mem_false:
  forall b vars i
    (NIN: ~ In i (map fst vars) ),
    VSet.mem i (cenv_for_gen b vars) = false.

Lemma cenv_bound_for_gen:
  forall vars (lnr: list_norepet (map fst vars)) b,
    cenv_bound (cenv_for_gen (addr_taken_stmt b) vars) vars.


Lemma alloc_bytes_in_bound_m:
  forall m
    n m'
    (AB: MemReserve.reserve_boxes m n = Some m')
    b i,
    Mem.in_bound_m i m b <->
    Mem.in_bound_m i m' b.

Lemma size_block_alloc_bytes:
  forall m n m' b
    (AB: MemReserve.reserve_boxes m n = Some m'),
    Mem.size_block m b =
    Mem.size_block m' b.

Definition forb :=
  (fun a: block * Z * Z => (snd (fst a), snd a)).

Require Import Permutation.

Lemma blocks_set_elements_permut:
  forall e id b1 ty
    (nex: e ! id = None)
    (nex': ~ exists id t, e ! id = Some (b1,t))
    (injective: forall id1 id2 b1 b2 ty1 ty2,
        (e ! id1 = Some (b1, ty1) ->
         e ! id2 = Some (b2, ty2) -> id1 <> id2 -> b1 <> b2)),
    Permutation (blocks_of_env (PTree.set id (b1, ty) e))
                ((b1,0,sizeof ty) :: blocks_of_env e ).

Lemma fr_is_map:
  forall {A B} (f: A -> B) l z,
    (fold_right (fun elt acc => f elt :: acc) z l) =
    map f l ++ z.
                            

Lemma blocks_of_env_charact:
  forall vars e' m' e m
    (AV: alloc_variables e m vars e' m')
    (lnr: list_norepet (map fst vars))
    (range: forall id b t, e!id = Some (b,t) -> Plt b (Mem.nextblock m))
    (inj0: forall id1 id2 b1 b2 ty1 ty2, e ! id1 = Some (b1,ty1) -> e!id2 = Some (b2,ty2) ->
                                    id1<>id2 -> b1 <> b2)
    (eid: forall id, ~ In id (map fst vars) -> e ! id = e' ! id)
    (eid': forall id, In id (map fst vars) -> e ! id = None)
  ,
    Permutation (map forb (blocks_of_env e'))
                (fold_right (fun elt acc => (0,sizeof (snd elt))::acc)
                            (map forb (blocks_of_env e)) vars).
      
Lemma filter_rev:
  forall {A} (f: A -> bool) l,
    filter f (rev l) = rev (filter f l).

Lemma align_mul:
  forall x y,
    y > 0 ->
    align (y*x) y = y*x.

Lemma align_eq_8:
  forall z, 0 < z <= 8 ->
       align z (two_power_nat MA) = two_power_nat MA.

Lemma cenv_bound_app:
  forall c l,
    cenv_bound c l <-> Forall (fun x => 0 < sizeof (snd x) <= 8 \/ VSet.mem (fst x) c = false) l.

Lemma Forall_app:
  forall {A} (P: A -> Prop) l1 l2,
    Forall P l1 -> Forall P l2 ->
    Forall P (l1 ++ l2).

Lemma cenv_bound_rev:
  forall c l
    (CB : cenv_bound c l),
    cenv_bound c (rev l).

Opaque align.
Opaque Z.mul Z.add.
Opaque Z.mul Z.of_nat.


Lemma free_blocks_0:
  forall m tm (FrB: free_blocks m tm 0),
    (Mem.nb_boxes_used_m tm <= Mem.nb_boxes_used_m m)%nat.

Lemma free_blocks_0':
  forall m tm,
    (Mem.nb_boxes_used_m tm <= Mem.nb_boxes_used_m m)%nat ->
    free_blocks m tm 0.


Variable ns1 ns2: ident -> nat.
Hypothesis ns1_spec:
  forall f,
    In (Gfun (Internal f)) (map snd (prog_defs prog)) ->
    (ns1 (fn_id f) <=
     ns2 (fn_id f)
     <= ns1 (fn_id f) +
       length
         (filter
            (fun it : VSet.elt * type =>
               VSet.mem (fst it)
                        (cenv_for_gen (addr_taken_stmt (fn_body f))
                                      (varsort (fn_params f ++ fn_vars f))))
            (varsort (fn_params f ++ fn_vars f)))) % nat.


Lemma contra:
  forall A (P Q: A -> Prop),
    (forall x, P x -> Q x) -> (forall x, ~ Q x -> ~ P x).

Lemma assign_loc_inject:
  forall sm ei (wf: wf_inj ei) f ty m locofs v m' tm loc'ofs' v'
    (IWB: inj_well_behaved f m tm)
    (AL: assign_loc ty m locofs v m')
    (EIaddr: ei f (locofs) (loc'ofs'))
    (SI: sep_inj m f locofs)
    (EIval: ei f v v')
    (SI': sep_inj m f v)
    (INJ: Mem.inject sm ei f m tm),
  exists tm',
    assign_loc ty tm loc'ofs' v' tm'
    /\ Mem.inject sm ei f m' tm'
    /\ (forall b chunk v,
          f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v).

Remark bind_parameter_temps_inv:
  forall id params args le le',
  bind_parameter_temps params args le = Some le' ->
  ~In id (var_names params) ->
  le'!id = le!id.

Lemma sem_cast_expr_typ: forall e e' ty,
    sem_cast_expr e' ty ty <> None ->
    sem_cast_expr e ty ty <> None.

Lemma memval_rel_inject:
  forall f a b c
    (MR: memval_rel same_eval a b)
    (MI: memval_inject expr_inj_se f a c),
    memval_inject expr_inj_se f b c.

Lemma dep_store:
  forall chunk m b o e2 m'
    (AL: Mem.store chunk m b o e2 = Some m')
    e b,
    depends_m m e b <-> depends_m m' e b.

Lemma dep_storev:
  forall chunk m e1 e2 m'
    (AL: Mem.storev chunk m e1 e2 = Some m')
    e b,
    depends_m m e b <-> depends_m m' e b.

Lemma dep_storebytes:
  forall m b o e2 m'
    (AL: Mem.storebytes m b o e2 = Some m')
    e b,
    depends_m m e b <-> depends_m m' e b.

Lemma dep_assign_loc:
  forall ty m e1 e2 m'
    (AL: assign_loc ty m e1 e2 m')
    e b,
    depends_m m e b <->
    depends_m m' e b.

Lemma depends_ptr:
       forall m (b b' : block) (i : int),
         depends_m m (Eval (Vptr b i)) b' -> b = b'.

Lemma assign_loc_is_dynamic_block:
  forall t m e f m'
    (AL: assign_loc t m e f m'),
  forall b, Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b.

Theorem store_params_correct:
  forall sm NS j f k cenv le lo hi te tlo thi e m params args m'
    (BP: bind_parameters e m params args m')
    s tm tle1 tle2 targs
    (NOREPET : list_norepet (var_names params))
    (CASTED: list_forall2 expr_casted args (map snd params))
    (VINJ: list_ei expr_inj_se j args targs)
    (SEP: Forall (fun x => sep_inj m j x) args)
    (MENV: match_envs j cenv e le m tm lo hi te tle1 tlo thi)
    (MINJ: Mem.inject sm expr_inj_se j m tm)
    (IWB: inj_well_behaved j m tm)
    (TLE: forall id, ~In id (var_names params) -> tle2!id = tle1!id)
    (LE: forall id, In id (var_names params) -> le!id = None),
  exists tle tm',
    star (fun ge => step2 ge NS) tge (State f (store_params cenv params s) k te tle tm)
         E0 (State f s k te tle tm')
    /\ bind_parameter_temps params targs tle2 = Some tle
    /\ Mem.inject sm expr_inj_se j m' tm'
    /\ match_envs j cenv e le m' tm' lo hi te tle tlo thi
    /\ Mem.nextblock tm' = Mem.nextblock tm
    /\ (forall b, Mem.bounds_of_block tm' b = Mem.bounds_of_block tm b)
    /\ (forall b, Mem.mask tm' b = Mem.mask tm b)
    /\ (forall b, Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b) /\
    Mem.nb_extra tm' = Mem.nb_extra tm.

Lemma bind_parameters_nextblock:
  forall e m params args m',
  bind_parameters e m params args m' -> Mem.nextblock m' = Mem.nextblock m.

Lemma bind_parameters_load:
  forall e chunk b ofs,
  (forall id b' ty, e!id = Some(b', ty) -> b <> b') ->
  forall m params args m',
  bind_parameters e m params args m' ->
  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.


Lemma free_blocks_of_env_perm_1:
  forall m e m' id b ty ofs k p,
  Mem.free_list m (blocks_of_env e) = Some m' ->
  e!id = Some(b, ty) ->
  Mem.perm m' b ofs k p ->
  0 <= ofs < sizeof ty ->
  False.

Lemma free_list_perm':
  forall b lo hi l m m',
  Mem.free_list m l = Some m' ->
  In (b, lo, hi) l ->
  Mem.range_perm m b lo hi Cur Freeable.

Lemma free_blocks_of_env_perm_2:
  forall m e m' id b ty,
  Mem.free_list m (blocks_of_env e) = Some m' ->
  e!id = Some(b, ty) ->
  Mem.range_perm m b 0 (sizeof ty) Cur Freeable.

Fixpoint freelist_no_overlap (l: list (block * Z * Z)) : Prop :=
  match l with
  | nil => True
  | (b, lo, hi) :: l' =>
      freelist_no_overlap l' /\
      (forall b' lo' hi', In (b', lo', hi') l' ->
       b' <> b \/ hi' <= lo \/ hi <= lo')
  end.

Lemma can_free_list:
  forall l m,
    (forall b lo hi, In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable
                                   /\ Mem.bounds_of_block m b = (lo, hi)) ->
  freelist_no_overlap l ->
  exists m', Mem.free_list m l = Some m'.

Lemma blocks_of_env_no_overlap:
  forall sm j cenv e le m lo hi te tle tlo thi tm
    (ME: match_envs j cenv e le m tm lo hi te tle tlo thi )
    (MINJ: Mem.inject sm expr_inj_se j m tm)
    (PERMS: forall id b ty,
        e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ty) Cur Freeable)
    l
    (lnr: list_norepet (List.map fst l))
    (TEID: forall id bty, In (id, bty) l -> te!id = Some bty),
    freelist_no_overlap (List.map block_of_binding l).

Lemma free_list_permut:
  forall l
    (LNR: list_norepet (map fst (map fst l)))
    l' (P: Permutation.Permutation l l')
    m m'
    (FL: Mem.free_list m l = Some m')
    tm (ME: mem_equiv m tm),
  exists tm', Mem.free_list tm l' = Some tm' /\ mem_equiv m' tm'.


Opaque minus.

Lemma filter_Forall:
  forall A f (l: list A)
    (F: Forall (fun x => f x = true) l),
    filter f l = l.

Definition inj (j:meminj) :=
  (fun (elt : block) (acc : list block) =>
                  match j elt with
                  | Some (b', _) => b' :: acc
                  | None => acc
                  end).


Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
  | mk_match_globalenvs
      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).

Lemma match_globalenvs_preserves_globals:
  forall f,
  (exists bound, match_globalenvs f bound) ->
  meminj_preserves_globals ge f.


Section EVAL_EXPR.

Variables e te: env.
Variables le tle: temp_env.
Variables m tm: mem.
Variable f: meminj.
Hypothesis IWB: inj_well_behaved f m tm.

Variable cenv: compilenv.
Variables lo hi tlo thi: block.
Hypothesis MATCH: match_envs f cenv e le m tm lo hi te tle tlo thi.
Variable sm: bool.
Hypothesis MEMINJ: Mem.inject sm expr_inj_se f m tm.
Hypothesis GLOB: exists bound, match_globalenvs f bound.

Lemma typeof_simpl_expr:
  forall a, typeof (simpl_expr cenv a) = typeof a.

Lemma deref_loc_inject:
  forall ty locofs v loc'ofs',
    deref_loc ty m locofs v ->
    sep_inj m f locofs ->
    expr_inj_se f (locofs) (loc'ofs') ->
    exists tv, deref_loc ty tm loc'ofs' tv /\ expr_inj_se f v tv.

Lemma eval_simpl_expr:
  forall a v,
  eval_expr ge e le m a v ->
  compat_cenv (addr_taken_expr a) cenv ->
  exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ expr_inj_se f v tv

with eval_simpl_lvalue:
  forall a bofs,
  eval_lvalue ge e le m a bofs ->
  compat_cenv (addr_taken_expr a) cenv ->
  match a with Evar id ty => VSet.mem id cenv = false | _ => True end ->
  exists b'ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b'ofs' /\ expr_inj_se f (bofs) (b'ofs').

Inductive expr_list_casted : list expr_sym -> typelist -> Prop :=
  expr_list_casted_nil: expr_list_casted nil Tnil
| expr_list_casted_cons:
    forall e el t tl (EC: expr_casted e t)
      (ELC: expr_list_casted el tl),
      expr_list_casted (e::el) (Tcons t tl).
      
Lemma eval_simpl_exprlist:
  forall al tyl vl,
  eval_exprlist ge e le m al tyl vl ->
  compat_cenv (addr_taken_exprlist al) cenv ->
  expr_list_casted vl tyl /\
  exists tvl,
     eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl
  /\ list_ei expr_inj_se f vl tvl.

End EVAL_EXPR.


Definition size_env e :=
  size_list (blocks_of_env e).


Lemma match_cont_sm:
  forall e m m' m'' N,
  Mem.free_list m (blocks_of_env e) = Some m' ->
  release_boxes m' N = Some m'' ->
  (Mem.nb_boxes_used_m m'' =
   Mem.nb_boxes_used_m m - size_env e - N)%nat.



Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> mem -> block -> block -> Prop :=
  | match_Kstop: forall cenv m tm bound tbound hi ,
      match_globalenvs f hi -> Ple hi bound -> Ple hi tbound ->
      match_cont f cenv Kstop Kstop m tm bound tbound
  | match_Kseq: forall cenv s k ts tk m tm bound tbound,
      simpl_stmt cenv s = OK ts ->
      match_cont f cenv k tk m tm bound tbound ->
      compat_cenv (addr_taken_stmt s) cenv ->
      match_cont f cenv (Kseq s k) (Kseq ts tk) m tm bound tbound
  | match_Kloop1: forall cenv s1 s2 k ts1 ts2 tk m tm bound tbound ,
      simpl_stmt cenv s1 = OK ts1 ->
      simpl_stmt cenv s2 = OK ts2 ->
      match_cont f cenv k tk m tm bound tbound ->
      compat_cenv (VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)) cenv ->
      match_cont f cenv (Kloop1 s1 s2 k) (Kloop1 ts1 ts2 tk) m tm bound tbound
  | match_Kloop2: forall cenv s1 s2 k ts1 ts2 tk m tm bound tbound ,
      simpl_stmt cenv s1 = OK ts1 ->
      simpl_stmt cenv s2 = OK ts2 ->
      match_cont f cenv k tk m tm bound tbound ->
      compat_cenv (VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)) cenv ->
      match_cont f cenv (Kloop2 s1 s2 k) (Kloop2 ts1 ts2 tk) m tm bound tbound
  | match_Kswitch: forall cenv k tk m tm bound tbound ,
      match_cont f cenv k tk m tm bound tbound ->
      match_cont f cenv (Kswitch k) (Kswitch tk) m tm bound tbound
  | match_Kcall: forall cenv optid fn e le k tfn te tle tk m tm hi thi lo tlo bound tbound x ,
      transf_function fn = OK tfn ->
      match_envs f (cenv_for fn) e le m tm lo hi te tle tlo thi ->
      match_cont f (cenv_for fn) k tk m tm lo tlo ->
      check_opttemp (cenv_for fn) optid = OK x ->
      Ple hi bound -> Ple thi tbound ->
      (ns1 (fn_id fn) + size_env e >= ns2 (fn_id tfn) + size_env te)%nat ->
      In (Gfun (Internal fn)) (map snd (prog_defs prog)) ->
      match_cont f cenv (Kcall optid fn e le k)
                        (Kcall optid tfn te tle tk) m tm bound tbound .


Lemma match_cont_invariant:
  forall f' m' f cenv k tk m tm tm' bound tbound
    (MC: match_cont f cenv k tk m tm bound tbound)
    (LOAD: forall b chunk v,
        f b = None -> Plt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v)
    (B: forall b, Plt b bound -> ~ Mem.is_dynamic_block m b ->
             Mem.bounds_of_block m b = Mem.bounds_of_block m' b)
    (B': forall b, Plt b tbound -> ~ Mem.is_dynamic_block tm b ->
              Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (INCR: inject_incr f f')
    (INJ1: forall b, Plt b bound -> f' b = f b)
    (INJ2: forall b b' delta, f' b = Some(b', delta) -> Plt b' tbound -> f' b = f b)
    (DYNinject: forall b b' delta,
        f b = Some (b',delta) ->
        (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block tm b'))
    (DYNsame: forall b, Plt b bound ->
                   (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b))
    (DYNsame': forall b, Plt b tbound ->
                    (Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b)),
    match_cont f' cenv k tk m' tm' bound tbound .


Lemma match_cont_assign_loc:
  forall f cenv k tk m bound tbound ty locofs v m' tm tm'
    (MC: match_cont f cenv k tk m tm bound tbound)
    (AL: assign_loc ty m locofs v m')
    (MNaddr: forall b o, Mem.mem_norm m locofs = Vptr b o -> Ple bound b)
    (Bnds: forall b, Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (EQ: Mem.nextblock tm = Mem.nextblock tm')
    (DYNinject: forall b b' delta,
        f b = Some (b',delta) ->
        (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block tm b'))
    (DYNsame': forall b, Plt b tbound ->
                    (Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b)),
    match_cont f cenv k tk m' tm' bound tbound.


Lemma match_cont_extcall:
  forall f cenv k tk m bound tbound tm f' m' tm'
    (MC: match_cont f cenv k tk m tm bound tbound)
    (UNCH: Mem.unchanged_on (loc_unmapped f) m m')
    (Bn: forall b : positive,
        Plt b bound -> ~ Mem.is_dynamic_block m b ->
        Mem.bounds_of_block m b = Mem.bounds_of_block m' b)
    (B': forall b : positive,
        Plt b tbound -> ~ Mem.is_dynamic_block tm b ->
        Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (INCR: inject_incr f f')
    (SEP: inject_separated f f' m tm)
    (PLE1: Ple bound (Mem.nextblock m)) (PLE2: Ple tbound (Mem.nextblock tm))
    (DYNinject: forall b b' delta,
        f b = Some (b',delta) ->
        (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block tm b'))
    (DYNsame: forall b, Plt b bound ->
                   (Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b))
    (DYNsame': forall b, Plt b tbound ->
                    (Mem.is_dynamic_block tm b <-> Mem.is_dynamic_block tm' b)),
  match_cont f' cenv k tk m' tm' bound tbound.


Lemma match_cont_incr_bounds:
  forall f cenv k tk m tm bound tbound,
  match_cont f cenv k tk m tm bound tbound ->
  forall bound' tbound',
    Ple bound bound' -> Ple tbound tbound' ->
  match_cont f cenv k tk m tm bound' tbound'.


Lemma match_cont_change_cenv:
  forall f cenv k tk m tm bound tbound cenv',
  match_cont f cenv k tk m tm bound tbound ->
  is_call_cont k ->
  match_cont f cenv' k tk m tm bound tbound.

Lemma match_cont_is_call_cont:
  forall f cenv k tk m tm bound tbound,
  match_cont f cenv k tk m tm bound tbound ->
  is_call_cont k ->
  is_call_cont tk.

Lemma match_cont_call_cont:
  forall f cenv k tk m tm bound tbound,
  match_cont f cenv k tk m tm bound tbound ->
  forall cenv',
  match_cont f cenv' (call_cont k) (call_cont tk) m tm bound tbound.



Lemma match_cont_free_env':
  forall sm f cenv e le m lo hi te tle tm tlo thi k tk m' tm'
    (IWB: inj_well_behaved f m tm)
    fn
  (MENV: match_envs f cenv e le m tm lo hi te tle tlo thi)
  (MC: match_cont f cenv k tk m tm lo tlo)
  (PLE1: Ple hi (Mem.nextblock m))
  (PLE2: Ple thi (Mem.nextblock tm))
  (FL1: Mem.free_list m (blocks_of_env e) = Some m')
  (FL2: Mem.free_list tm (blocks_of_env te) = Some tm')
  ei (MINJ: Mem.inject sm ei f m tm)
  m2' (MR: MemReserve.release_boxes m' (ns1 (fn_id fn)) = Some m2')
  tm2' (MR': MemReserve.release_boxes tm' (ns2 (fn_id fn)) = Some tm2'),
    match_cont f cenv k tk m2' tm2' (Mem.nextblock m2') (Mem.nextblock tm2').


Lemma match_cont_globalenv:
  forall f cenv k tk m tm bound tbound,
  match_cont f cenv k tk m tm bound tbound ->
  exists bound, match_globalenvs f bound.

Hint Resolve match_cont_globalenv: compat.

Lemma match_cont_find_funct:
  forall sm f cenv k tk m bound tbound vf fd tvf tm
    (IWB: inj_well_behaved f m tm)
    (MC: match_cont f cenv k tk m tm bound tbound)
    (FF: Genv.find_funct m ge vf = Some fd)
    (EI: expr_inj_se f vf tvf)
    (SI: sep_inj m f vf)
    (MINJ: Mem.inject sm expr_inj_se f m tm),
  exists tfd, Genv.find_funct tm tge tvf = Some tfd /\ transf_fundef fd = OK tfd.


Remark is_liftable_var_charact:
  forall cenv a,
  match is_liftable_var cenv a with
  | Some id => exists ty, a = Evar id ty /\ VSet.mem id cenv = true
  | None => match a with Evar id ty => VSet.mem id cenv = false | _ => True end
  end.

Remark simpl_select_switch:
  forall cenv n ls tls,
  simpl_lblstmt cenv ls = OK tls ->
  simpl_lblstmt cenv (select_switch n ls) = OK (select_switch n tls).

Remark simpl_seq_of_labeled_statement:
  forall cenv ls tls,
  simpl_lblstmt cenv ls = OK tls ->
  simpl_stmt cenv (seq_of_labeled_statement ls) = OK (seq_of_labeled_statement tls).

Remark compat_cenv_select_switch:
  forall cenv n ls,
  compat_cenv (addr_taken_lblstmt ls) cenv ->
  compat_cenv (addr_taken_lblstmt (select_switch n ls)) cenv.

Remark addr_taken_seq_of_labeled_statement:
  forall ls, addr_taken_stmt (seq_of_labeled_statement ls) = addr_taken_lblstmt ls.

Section FIND_LABEL.

Variable f: meminj.
Variable cenv: compilenv.
Variables m tm: mem.
Variables bound tbound: block.
Variable lbl: ident.

Lemma simpl_find_label:
  forall s k ts tk,
  simpl_stmt cenv s = OK ts ->
  match_cont f cenv k tk m tm bound tbound ->
  compat_cenv (addr_taken_stmt s) cenv ->
  match find_label lbl s k with
  | None =>
      find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label lbl ts tk = Some(ts', tk')
      /\ compat_cenv (addr_taken_stmt s') cenv
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_cont f cenv k' tk' m tm bound tbound
  end

with simpl_find_label_ls:
  forall ls k tls tk,
  simpl_lblstmt cenv ls = OK tls ->
  match_cont f cenv k tk m tm bound tbound ->
  compat_cenv (addr_taken_lblstmt ls) cenv ->
  match find_label_ls lbl ls k with
  | None =>
      find_label_ls lbl tls tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label_ls lbl tls tk = Some(ts', tk')
      /\ compat_cenv (addr_taken_stmt s') cenv
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_cont f cenv k' tk' m tm bound tbound
  end.


Lemma find_label_store_params:
  forall lbl s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k.

End FIND_LABEL.

Lemma bool_expr_inj:
  forall ei (wf: wf_inj ei) f b b' ty
    (EI: ei f b b'),
    ei f (bool_expr b ty) (bool_expr b' ty).

Lemma sep_inj_bool_expr:
  forall m f v ty
    (SI: sep_inj m f v),
    sep_inj m f (bool_expr v ty).

Lemma expr_casted_list_params:
  forall params vl,
    expr_list_casted vl (type_of_params params) ->
    list_forall2 expr_casted vl (map snd params).

Lemma expr_list_inject_incr:
  forall ei (wf: wf_inj ei) f a b
    (ELI: list_ei ei f a b)
    f' (INCR: inject_incr f f'),
    list_ei ei f' a b.


Lemma filter_permut:
  forall A (f: A -> bool) l l'
    (P: Permutation.Permutation l l'),
    Permutation.Permutation (filter f l) (filter f l').

Lemma add_lifted_permut:
  forall x Y Y' z z', Permutation.Permutation Y Y' ->
                 Permutation.Permutation z z' ->
                 Permutation.Permutation (add_lifted x Y z) (add_lifted x Y' z').

Lemma create_undef_temps_permut:
  forall l1 l2 (P: Permutation.Permutation l1 l2) id,
    (create_undef_temps l1)! id = (create_undef_temps l2)! id.


Lemma add_lifted_set_eq:
  forall s s' (EQ: VSet.Equal s s') l1 l2,
    (add_lifted s l1 l2) = (add_lifted s' l1 l2).

Lemma cenv_for_gen_set_eq:
  forall s l l' (P: Permutation.Permutation l l'),
    VSet.Equal (cenv_for_gen s l) (cenv_for_gen s l').


Lemma sort_remove_lifted:
  forall c l,
    varsort (remove_lifted c l) =
    remove_lifted c (varsort l).

Lemma remove_lifted_eq:
  forall c c' (EQ: VSet.Equal c c') l,
    remove_lifted c l = remove_lifted c' l.


Lemma perm_add_loc_aux:
  forall t l t0 t1 (EQ: (VSet.Equal t0 t1)),
    VSet.Equal (fold_right (add_local_variable t) t0 l)
               (fold_right (add_local_variable t) t1 l).

Lemma perm_add_loc:
  forall t l l' (P: Permutation.Permutation l l')
    t0 t1 (EQ: VSet.Equal t0 t1),
    VSet.Equal (fold_right (add_local_variable t) t0 l)
               (fold_right (add_local_variable t) t1 l').



Lemma cenv_for_cenv_for_gen_eq:
  forall f,
    VSet.Equal (cenv_for f)
               (cenv_for_gen (addr_taken_stmt (fn_body f))
                             (varsort (fn_params f ++ fn_vars f))).

Lemma remove_lifted_app:
  forall f l1 l2,
    remove_lifted f (l1 ++ l2) = remove_lifted f l1 ++ remove_lifted f l2.


Lemma store_params_ext:
  forall cenv cenv' l s (EQ: VSet.Equal cenv cenv'),
    store_params cenv l s = store_params cenv' l s.

Lemma match_envs_cenv_ext:
  forall cenv cenv' f e le m tm lo hi te tle tlo thi
     (EQ: VSet.Equal cenv cenv')
     (ME: match_envs f cenv e le m tm lo hi te tle tlo thi),
    match_envs f cenv' e le m tm lo hi te tle tlo thi.

Lemma av_bounds:
  forall e m vars e' m1
    (AV: alloc_variables e m vars e' m1)
    b (PLT: Plt b (Mem.nextblock m)),
    Mem.bounds_of_block m b = Mem.bounds_of_block m1 b.

Lemma bp_bounds:
  forall m e v vl m1
    (BP: bind_parameters e m v vl m1) b,
    Mem.bounds_of_block m b = Mem.bounds_of_block m1 b.

Lemma free_blocks_alloc_bytes':
  forall k m tm,
    free_blocks m tm k ->
    exists tm',
      MemReserve.reserve_boxes tm k = Some tm' /\
      free_blocks m tm' 0.


Lemma fl_rew:
  forall vars z,
    (fold_left
       (fun (acc : nat) (it : ident * type) => acc + Mem.box_span (sizeof (snd it)))
       vars z =
     fold_left
       (fun (acc : nat) (it : ident * type) => acc + Mem.box_span (sizeof (snd it)))
       vars 0 + z)%nat.

Lemma alloc_variables_size_mem:
  forall vars m e m' e'
    (AV: alloc_variables e m vars e' m'),
    (Mem.nb_boxes_used_m m' = Mem.nb_boxes_used_m m + (fold_left (fun acc it => acc + Mem.box_span (sizeof (snd it))) vars 0))%nat.

Lemma blocks_of_env_norepet:
  forall e
    (Einj: forall i1 b1 t1 i2 b2 t2
             (ei1: e ! i1 = Some (b1, t1))
             (ei2: e ! i2 = Some (b2, t2))
             (idiff: i1 <> i2), b1 <> b2),
    list_norepet (map fst (map fst (blocks_of_env e))).

Lemma match_alloc_variables:
  forall cenv e m vars e' m'
    (AV:alloc_variables e m vars e' m')
    j tm te n
    (FrB: free_blocks m tm n)
    (CB: cenv_bound cenv vars)
    (LNR: list_norepet (var_names vars))
    (MINJ: Mem.inject true expr_inj_se j m tm)
    (IWB: inj_well_behaved j m tm)
    (EVB: forall i b t, e ! i = Some (b,t) -> Mem.valid_block m b)
    (TE: forall i b t, te ! i = Some (b,t) -> ~ In i (var_names vars))
    (INJenv: forall b' i t, te ! i = Some (b',t) -> exists b delta, e ! i = Some (b,t) /\ j b = Some (b',delta)),
  exists j' te' tm',
    alloc_variables te tm (remove_lifted cenv vars) te' tm'
    /\ free_blocks m' tm' (n + length (filter (fun it => VSet.mem (fst it) cenv) vars))
    /\ Mem.inject true expr_inj_se j' m' tm'
    /\ inject_incr j j'
    /\ (forall b, Mem.valid_block m b -> j' b = j b)
    /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b)
    /\ (forall b b' delta, j' b = Some(b', delta) -> ~Mem.valid_block tm b' ->
                     exists id, exists ty, e'!id = Some(b, ty) /\ te'!id = Some(b', ty) /\ delta = 0)
    /\ (forall id ty, In (id, ty) vars ->
                exists b,
                  e'!id = Some(b, ty)
                  /\ if VSet.mem id cenv
                    then te'!id = te!id /\ j' b = None
                    else exists tb, te'!id = Some(tb, ty) /\ j' b = Some(tb, 0))
    /\ (forall id, ~In id (var_names vars) -> e'!id = e!id /\ te'!id = te!id)
    /\ (forall id b ty, ~In id (var_names vars) -> e'!id = Some (b,ty) -> j' b = j b)
    /\ inj_well_behaved j' m' tm'
    /\ (forall b' i t, te' ! i = Some (b',t) -> exists b delta, e' ! i = Some (b,t) /\ j' b = Some (b', delta))
.


Theorem match_envs_alloc_variables:
  forall cenv m vars e m' temps j tm
    (CB: cenv_bound cenv vars)
    (IWB: inj_well_behaved j m tm)
    n (FrB: free_blocks m tm n)
    (AV: alloc_variables empty_env m vars e m')
    nbytes m''
    needed (ORD: (nbytes <= needed)%nat)
    (ORD': (needed <= nbytes +
                     length
                       (filter (fun it : VSet.elt * type => VSet.mem (fst it) cenv)
                               vars))%nat)
    (AB: MemReserve.reserve_boxes m' nbytes = Some m'')
    (LNR: list_norepet (var_names vars))
    (MINJ: Mem.inject true expr_inj_se j m tm)
    (AM: forall id ty, In (id, ty) vars -> VSet.mem id cenv = true ->
                  exists chunk, access_mode ty = By_value chunk)
    (VARIN: forall id, VSet.mem id cenv = true -> In id (var_names vars)),
  exists j' te tm' tm'',
    alloc_variables empty_env tm (remove_lifted cenv vars) te tm'
    /\ MemReserve.reserve_boxes tm' needed = Some tm''
    /\ free_blocks m'' tm'' n
    /\ match_envs j' cenv e (create_undef_temps temps) m'' tm''
                 (Mem.nextblock m) (Mem.nextblock m'')
                 te (create_undef_temps (add_lifted cenv vars temps))
                 (Mem.nextblock tm) (Mem.nextblock tm'')
    /\ Mem.inject true expr_inj_se j' m'' tm''
    /\ inject_incr j j'
    /\ (forall b, Mem.valid_block m b -> j' b = j b)
    /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b)
    /\ inj_well_behaved j' m'' tm''.

Lemma release_inj:
  forall sm j m tm
    ei (INJ: Mem.inject sm ei j m tm)
    n n' (LEextra: (n <= n' <= Mem.nb_extra tm)%nat)
    m' (MR: MemReserve.release_boxes m n = Some m'),
  exists tm',
    MemReserve.release_boxes tm n' = Some tm' /\
    Mem.inject sm ei j m' tm'.

Lemma free_list_preserves:
  forall m m' tm e te (FL: Mem.free_list m (blocks_of_env e) = Some m')
    j
    (IWB: inj_well_behaved j m tm)
    (INJ: Mem.inject true expr_inj_se j m tm)
    cenv le lo hi tle tlo thi
    (MENV : match_envs j cenv e le m tm lo hi te tle tlo thi)
    fn
    (INPROG: In (Gfun (Internal fn)) (map snd (prog_defs prog)))
    (NbExtra2: (ns2 (fn_id fn) <= Mem.nb_extra tm)%nat)
    (NbExtra1: (ns1 (fn_id fn) <= Mem.nb_extra m)%nat)
    m'' (REL: MemReserve.release_boxes m' (ns1 (fn_id fn)) = Some m''),
  exists tm' tm'',
    Mem.free_list tm (blocks_of_env te) = Some tm' /\
    MemReserve.release_boxes tm' (ns2 (fn_id fn)) = Some tm'' /\
    ( forall (FreeOrd: (Mem.nb_boxes_used_m tm - size_env te - ns2 (fn_id fn) <=
                        Mem.nb_boxes_used_m m - size_env e - ns1 (fn_id fn))%nat),
        Mem.inject true expr_inj_se j m'' tm'') /\
    inj_well_behaved j m'' tm''.

Fixpoint match_size_mem (k tk: cont) (m tm: mem) :=
  (Mem.nb_boxes_used_m tm <= Mem.nb_boxes_used_m m)%nat /\
 match k, tk with
   Kcall roi f e le k',
   Kcall troi tf te tle tk' =>
   (
     size_env te <= nb_boxes_static tm /\ ns2 (fn_id tf) <= Mem.nb_extra tm /\
     size_env e <= nb_boxes_static m /\ ns1 (fn_id f) <= Mem.nb_extra m /\
     forall m' tm',
       nb_boxes_static m' = nb_boxes_static m - size_env e ->
       nb_boxes_static tm' = nb_boxes_static tm - size_env te ->
       Mem.nb_extra m' = Mem.nb_extra m - ns1 (fn_id f) ->
       Mem.nb_extra tm' = Mem.nb_extra tm - ns2 (fn_id tf) ->
       forall C C',
       nb_boxes_dynamic m' + C = nb_boxes_dynamic m + C' ->
       nb_boxes_dynamic tm' + C = nb_boxes_dynamic tm + C' ->
       match_size_mem k' tk' m' tm')%nat
 | Kstop, Kstop => True
 | Kseq s1 k', Kseq s2 tk' => match_size_mem k' tk' m tm
 | Kloop1 s1 s2 k', Kloop1 s1' s2' tk' => match_size_mem k' tk' m tm
 | Kloop2 s1 s2 k', Kloop2 s1' s2' tk' => match_size_mem k' tk' m tm
 | Kswitch k', Kswitch tk' => match_size_mem k' tk' m tm
 | _, _ => False
 end.

Lemma match_size_mem_rew (k tk: cont) (m tm: mem) :
  match_size_mem k tk m tm <->
  ((Mem.nb_boxes_used_m tm <= Mem.nb_boxes_used_m m)%nat /\
  match k, tk with
    Kcall roi f e le k',
    Kcall troi tf te tle tk' =>
    (
      size_env te <= nb_boxes_static tm /\ ns2 (fn_id tf) <= Mem.nb_extra tm /\
      size_env e <= nb_boxes_static m /\ ns1 (fn_id f) <= Mem.nb_extra m /\
      forall m' tm',
        nb_boxes_static m' = nb_boxes_static m - size_env e ->
        nb_boxes_static tm' = nb_boxes_static tm - size_env te ->
        Mem.nb_extra m' = Mem.nb_extra m - ns1 (fn_id f) ->
        Mem.nb_extra tm' = Mem.nb_extra tm - ns2 (fn_id tf) ->
        forall C C',
          nb_boxes_dynamic m' + C = nb_boxes_dynamic m + C' ->
          nb_boxes_dynamic tm' + C = nb_boxes_dynamic tm + C' ->
          match_size_mem k' tk' m' tm')%nat
  | Kstop, Kstop => True
  | Kseq s1 k', Kseq s2 tk' => match_size_mem k' tk' m tm
  | Kloop1 s1 s2 k', Kloop1 s1' s2' tk' => match_size_mem k' tk' m tm
  | Kloop2 s1 s2 k', Kloop2 s1' s2' tk' => match_size_mem k' tk' m tm
  | Kswitch k', Kswitch tk' => match_size_mem k' tk' m tm
  | _, _ => False
  end).

Lemma msm_le:
  forall k tk m tm,
    match_size_mem k tk m tm ->
    (Mem.nb_boxes_used_m tm <= Mem.nb_boxes_used_m m)%nat.

Inductive match_states: state -> state -> Prop :=
| match_regular_states:
    forall f s k e le m tf ts tk te tle tm j lo hi tlo thi
      (IWB: inj_well_behaved j m tm)
      (TRF: transf_function f = OK tf)
      (TRS: simpl_stmt (cenv_for f) s = OK ts)
      (MENV: match_envs j (cenv_for f) e le m tm lo hi te tle tlo thi)
      (DIFF: (ns1 (fn_id f) + size_env e >=
              ns2 (fn_id tf) + size_env te)%nat)
      (MCONT: match_cont j (cenv_for f) k tk m tm lo tlo)
      (MSM: match_size_mem (Kcall None f e le k) (Kcall None tf te tle tk) m tm)
      (MINJ: Mem.inject true expr_inj_se j m tm)
      (COMPAT: compat_cenv (addr_taken_stmt s) (cenv_for f))
      (BOUND: Ple hi (Mem.nextblock m))
      (TBOUND: Ple thi (Mem.nextblock tm))
      (Pdefs: In (Gfun (Internal f)) (map snd (prog_defs prog))),
      match_states (State f s k e le m)
                   (State tf ts tk te tle tm)
  | match_call_state:
      forall fd vargs k m tfd tvargs tk tm j targs tres cconv
        (IWB: inj_well_behaved j m tm)
        (TRFD: transf_fundef fd = OK tfd)
        (MCONT: forall cenv, match_cont j cenv k tk m tm (Mem.nextblock m) (Mem.nextblock tm))
        (MSM: match_size_mem k tk m tm)
        (MINJ: Mem.inject true expr_inj_se j m tm)
        (AINJ: list_ei expr_inj_se j vargs tvargs)
        (FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
        (ANORM: expr_list_casted vargs targs)
        (Pdefs: In (Gfun (fd)) (map snd (prog_defs prog))),
      match_states (Callstate fd vargs k m)
                   (Callstate tfd tvargs tk tm)
  | match_return_state:
      forall v k m tv tk tm j
        (IWB: inj_well_behaved j m tm)
        (MCONT: forall cenv, match_cont j cenv k tk m tm (Mem.nextblock m) (Mem.nextblock tm))
        (MSM: match_size_mem k tk m tm)
        (MINJ: Mem.inject true expr_inj_se j m tm)
        (RINJ: expr_inj_se j v tv)
      ,
      match_states (Returnstate v k m)
                   (Returnstate tv tk tm).

Lemma msm_call_cont:
  forall k k' m m' (MSM: match_size_mem k k' m m'),
    match_size_mem (call_cont k) (call_cont k') m m'.

Section GotoMsm.
  
Variable f: meminj.
Variable cenv: compilenv.
Variables m tm: mem.
Variables bound tbound: block.
Variable lbl: ident.

Lemma simpl_find_label_msm:
  forall s k ts tk sm stm,
  simpl_stmt cenv s = OK ts ->
  match_size_mem k tk sm stm ->
  match find_label lbl s k with
  | None =>
      find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label lbl ts tk = Some(ts', tk')
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_size_mem k' tk' sm stm
  end

with simpl_find_label_msm_ls:
  forall ls k tls tk sm stm,
  simpl_lblstmt cenv ls = OK tls ->
  match_size_mem k tk sm stm ->
  match find_label_ls lbl ls k with
  | None =>
      find_label_ls lbl tls tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label_ls lbl tls tk = Some(ts', tk')
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_size_mem k' tk' sm stm
  end.

 
End GotoMsm.

Lemma assign_loc_static_size:
  forall m m' ty a b
    (AL: assign_loc ty m a b m'),
    nb_boxes_static m = nb_boxes_static m'.

Lemma assign_loc_dynamic_size:
  forall m m' ty a b
    (AL: assign_loc ty m a b m'),
    nb_boxes_dynamic m = nb_boxes_dynamic m'.

Opaque match_size_mem.

Lemma alloc_variables_size_mem':
  forall vars m e m' e'
    (AV: alloc_variables e m vars e' m')
    (LNR: list_norepet (map fst vars))
    (IN: forall id, In id (map fst vars) -> e ! id = None)
    (VB: forall id b ty, e ! id = Some (b, ty) -> Mem.valid_block m b)
    (INJ: forall (id1 id2 : positive) (b0 b2 : block) (ty1 ty2 : type),
      e ! id1 = Some (b0, ty1) -> e ! id2 = Some (b2, ty2) -> id1 <> id2 -> b0 <> b2),
    (nb_boxes_static m' = nb_boxes_static m + size_env e' - size_env e)%nat.

Lemma alloc_variables_size_env:
  forall vars m m' e'
    (AV: alloc_variables empty_env m vars e' m')
    (LNR: list_norepet (map fst vars)),
    (nb_boxes_static m' = nb_boxes_static m + size_env e')%nat.

Lemma bind_parameters_mask:
  forall e m params args m' b,
    bind_parameters e m params args m' -> Mem.mask m' b = Mem.mask m b.

Lemma blocks_of_env_charact':
  forall vars e' m' e m
    (AV: alloc_variables e m vars e' m')
    (lnr: list_norepet (map fst vars))
    (range: forall id b t, e!id = Some (b,t) -> Plt b (Mem.nextblock m))
    (inj0: forall id1 id2 b1 b2 ty1 ty2, e ! id1 = Some (b1,ty1) -> e!id2 = Some (b2,ty2) ->
                                    id1<>id2 -> b1 <> b2)
    (eid: forall id, ~ In id (map fst vars) -> e ! id = e' ! id)
    (eid': forall id, In id (map fst vars) -> e ! id = None)
  ,
    Permutation (map size_of_block (blocks_of_env e'))
                (fold_right (fun elt acc => sizeof (snd elt)::acc)
                            (map size_of_block (blocks_of_env e)) vars).


Lemma alloc_variables_lengths':
  forall c l m e m0 tm te tm0
    (CB : cenv_bound c l)
    (AV : alloc_variables empty_env m l e m0)
    (AV' : alloc_variables empty_env tm (remove_lifted c l) te tm0)
    (LNR : list_norepet (map fst l)),
    size_env e =
    ((length (filter (fun it : VSet.elt * type => VSet.mem (fst it) c) l)) + size_env te)%nat.

Lemma bind_parameters_dynamic:
  forall e m v lsv m' (BP:bind_parameters e m v lsv m') b,
    Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b.

Lemma alloc_variables_dynamic:
  forall e m v e' m'
    (AV: alloc_variables e m v e' m')
    b,
    Mem.is_dynamic_block m b <-> Mem.is_dynamic_block m' b.

Lemma filter_app_permut:
  forall {A} (f: A -> bool) l,
    Permutation
      (filter f l ++ filter (fun x => negb (f x)) l)
      l.

Lemma fold_left_plus_length:
  forall l (F: Forall (fun x => x = 1%nat) l),
    fold_left Peano.plus l O = length l.

Lemma bind_parameters_nb_extra:
  forall e m v lsv m' (BP:bind_parameters e m v lsv m'),
    Mem.nb_extra m = Mem.nb_extra m'.


Lemma alloc_variables_nb_dynamic:
  forall e m vars e2 m2 (AV: alloc_variables e m vars e2 m2),
    nb_boxes_dynamic m = nb_boxes_dynamic m2.

  Lemma bp_boxes_static:
    forall e m vars le m',
      bind_parameters e m vars le m' ->
      nb_boxes_static m = nb_boxes_static m'.

  Lemma bp_boxes_dynamic:
    forall e m vars le m',
      bind_parameters e m vars le m' ->
      nb_boxes_dynamic m = nb_boxes_dynamic m'.

    Lemma match_size_mem_same_size:
    forall k tk m tm (MSM: match_size_mem k tk m tm)
      m' tm'
      (stEq: nb_boxes_static m = nb_boxes_static m')
      (stEqt: nb_boxes_static tm = nb_boxes_static tm')
      C C'
      (dynEq: (nb_boxes_dynamic m + C = nb_boxes_dynamic m' + C')%nat)
      (dynEqt: (nb_boxes_dynamic tm + C = nb_boxes_dynamic tm' + C')%nat)
      (exEq: Mem.nb_extra m = Mem.nb_extra m')
      (exEqt: Mem.nb_extra tm = Mem.nb_extra tm'),
      match_size_mem k tk m' tm'.

  Lemma alloc_variables_nb_extra:
  forall e m vars e2 m2 (AV: alloc_variables e m vars e2 m2),
    Mem.nb_extra m = Mem.nb_extra m2.


Lemma step_simulation:
  forall S1 t S2,
    step1 ge ns1 S1 t S2 ->
    forall S1' (MS: match_states S1 S1'),
    exists S2', plus (fun ge => step2 ge ns2) tge S1' t S2' /\ match_states S2 S2'.

Lemma iwb_flat:
  forall m,
    inj_well_behaved (Mem.flat_inj (Mem.nextblock m)) m m.

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

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

Theorem transf_program_correct:
  forall sg, forward_simulation (semantics1 prog ns1 sg) (semantics2 tprog ns2 sg).

End PRESERVATION.