Library FminortoCminor_proof3

Simulation scheme for the generation of Cminor code



Author:Zaynah Dargaye

Created: 29th April 2009

Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Mml.
Require Import Mml_pre.
Require Import FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.
Require Import EqNat.
Require Import Fminor.
Require Import Cminor.
Require Import Op.
Require Import Integers.
Require Import Cmconstr.
Require Import Values.
Require Import Cmconstrproof.
Require Import Mem.
Require Import FminortoCminor.
Require Import Switch.
Require Import FminortoCminor_proof1.
Require Import Fminor_well.
Require Import FminortoCminor_proof2.

I. Intermediate properties
Lemma alloc_success:
 forall m n1 n2,
     exists ma, exists sp , alloc m n1 n2 = (ma,sp).

Lemma nth_pat_gen:
 forall pl n xp id w,
  nth_error pl n = Some xp ->
 nth_error (map (fun x : cpat => gen_pat id x w) pl) n =
 Some (gen_pat id xp w).

Lemma nth_pat_gen_tail:
 forall pl n xp w,
  nth_error pl n = Some xp ->
 nth_error (map (fun x : cpat => gen_pat_tail x w) pl) n =
 Some (gen_pat_tail xp w).

Lemma well_nth:
 forall q pl, well_plist_bound q pl ->
   forall n x (NTH: nth_error pl n = Some x ),
   well_pat_bound q x.

Section COR.

II. Correspondence betwenn global environments
Variable s: list (ident*cfunction).

Variable g:genv.

Variable finit: block_kind.

Hypothesis match_glo:
 forall fid d, recup_cfunct fid s = Some d ->
   exists b, exists f, Genv.find_symbol g fid = Some b/\
                                 Genv.find_funct g (Vptr b Int.zero)= Some f/\
                                 gen_function (fid,d)= (fid,f)/\
                                ( finit b = Some GB)/\
                                well_bound_func d.

III.Correspondence between values

Inductive val_eqv:block_kind->mem->cval->block->Prop:=
 | mconstr:forall f m n vl b cvl ,
           f b = Some HB ->
          (low_bound m b) = 0 ->
          (high_bound m b)= Z_of_nat (S (length vl))*4+4->
          (high_bound m b)< Int.max_signed ->
          loadlist m b 0 (S (length vl)) =
          Some ((Vint (int_of_nat n)):: map (fun x=> Vptr x Int.zero) cvl) ->
         (forall i, In i cvl -> i <b/\ f i = Some HB) ->
          vallist_eqv f m vl cvl ->
          val_eqv f m (cconstr n vl) b
 | mcclos: forall m fid bf vl b cvl d f fk,
           fk b = Some HB ->
          (low_bound m b) = 0 ->
          (high_bound m b)= Z_of_nat (S (length vl))*4+4->
          (high_bound m b) < Int.max_signed ->
          loadlist m b 0 (S (length vl)) =
               Some ((Vptr bf Int.zero):: map (fun x=> Vptr x Int.zero) cvl) ->
          Genv.find_symbol g fid = Some bf ->
          Genv.find_funct g (Vptr bf Int.zero) = Some f ->
          gen_function (fid,d)=(fid,f)->
          fk bf = Some GB ->
          recup_cfunct fid s = Some d->
          (forall i, In i cvl -> i <b/\ fk i = Some HB) ->
          vallist_eqv fk m vl cvl -> well_bound_func d->
          val_eqv fk m (cclos fid vl) b
          
with vallist_eqv : block_kind->mem ->
       list cval -> list block ->Prop:=
 |eqvnil: forall f m ,vallist_eqv f m nil nil
 |eqvcons: forall f m v cv l cl,
       val_eqv f m v cv->vallist_eqv f m l cl->
       vallist_eqv f m (v::l) (cv::cl).

Definition fenv:=Fminor.env.
Scheme val_eqv_ind6 := Minimality for val_eqv Sort Prop
 with vallist_eqv_ind6 := Minimality for vallist_eqv Sort Prop.

Lemma vallist_eqv_length :
 forall f ml cl m ,
    vallist_eqv f m ml cl -> length cl = length ml.

Lemma vallist_eqv_append :
 forall f ml1 ml2 cl1 cl2 m ,
  vallist_eqv f m ml1 cl1 -> vallist_eqv f m ml2 cl2 ->
  vallist_eqv f m (ml1++ml2) (cl1++cl2).

Lemma vallist_eqv_rev :
 forall f ml cl m,
  vallist_eqv f m ml cl ->
  vallist_eqv f m (rev ml) (rev cl).

Lemma vallist_nth:
 forall f m vl cvl, vallist_eqv f m vl cvl ->
  forall n v, nth_error vl n = Some v ->
  exists cv, nth_error cvl n = Some cv /\ val_eqv f m v cv.


Lemma val_eqv_fincr:
 forall f m mv v, val_eqv f m mv v ->
    forall f2 (FI: block_kind_incr f f2),
    val_eqv f2 m mv v.



Lemma val_eqv_valid:
 forall f m cv v, val_eqv f m cv v ->
 valid_block m v.

Lemma val_eqv_kind:
 forall f m cv v, val_eqv f m cv v -> f v = Some HB.

Lemma vallist_eqv_kind:
 forall f m cv v, vallist_eqv f m cv v ->
      (forall x , In x v -> f x = Some HB).

Lemma valid_acc:
forall cvl b m,
 (forall i : block, In i cvl -> i < b) ->
   valid_block m b->
   (forall i: block , In i cvl -> valid_block m i).

Lemma val_eqv_same:
 forall f m v b, val_eqv f m v b ->
 forall sp fa ma (GC: gc_mem m f sp ma fa)
                  (ACC: acc f m sp b ),
   val_eqv fa ma v b.





Lemma vallist_eqv_same:
 forall f m v b, vallist_eqv f m v b ->
 forall sp fa ma (GC: gc_mem m f sp ma fa)
                  (ACC: forall i, In i b -> acc f m sp i ),
   vallist_eqv fa ma v b.

Lemma val_eqv_new:
 forall fa ma fv cv, val_eqv fa ma fv cv ->
 forall sp z0 v m1 ofs
 (VB: fa sp = Some RB)
 (ACC: acc fa ma sp cv)
 (MBK: mem_block_kind ma fa)
 (ID0: fa z0 = Some HB)
 (FRE: fresh_block fa z0)
  (ST: store Mint32 ma z0 ofs v = Some m1) ,
 val_eqv fa m1 fv cv.

Lemma vallist_eqv_new:
 forall fa ma fv cv, vallist_eqv fa ma fv cv ->
 forall z0 v m1 ofs sp
(VB: fa sp = Some RB)
 (ACC: forall i, In i cv -> acc fa ma sp i)
 (MBK: mem_block_kind ma fa)
 (ID0: fa z0 = Some HB)
 (FRE: fresh_block fa z0)
  (ST: store Mint32 ma z0 ofs v = Some m1) ,
      vallist_eqv fa m1 fv cv.

Lemma val_eqv_storelist:
 forall fa ma fv v, val_eqv fa ma fv v->
 forall cv z0 k mf sp
    (ST: storelist ma z0 (Z_of_nat k*4) cv =Some mf)
    (MBK: mem_block_kind ma fa)
    (FRE: fresh_block fa z0) (NEQ:fa z0 = Some HB)
    (VB: fa sp = Some RB) ,
    val_eqv fa mf fv v.




Lemma vallist_eqv_storelist:
 forall fa ma fv v, vallist_eqv fa ma fv v->
 forall sp cv z0 k mf
    (ST: storelist ma z0 (Z_of_nat k*4) cv =Some mf)
    (VE: vallist_eqv fa ma fv v)
    (MBK: mem_block_kind ma fa)
    (FRE: fresh_block fa z0) (NEQ:fa z0 = Some HB)
    (VB: fa sp = Some RB),
    vallist_eqv fa mf fv v.

Lemma match_clos_storelist:
forall ma sp vl z0 fa mf cv fid b f d
    (A: Genv.find_symbol g fid = Some b)
    (B:Genv.find_funct g (Vptr b Int.zero)= Some f)
    (C:gen_function (fid, d) = (fid, f))
    (D: recup_cfunct fid s = Some d)
    (F: fa b = Some GB)
    (E: well_bound_func d)
    (G: fa sp = Some RB)
    (NEQ: fa z0 = Some HB)
    (NV: vallist_eqv fa ma vl cv )
    (STL: storelist ma z0 0 (Vptr b Int.zero ::
    (map (fun x=>Vptr x Int.zero) cv)) = Some mf)
    (LB: low_bound ma z0 = 0)
    (HiB: high_bound ma z0 = Z_of_nat (S (length cv)) * 4 + 4)
    (COND: Z_of_nat (S (length cv)) * 4 + 4 < Int.max_signed)
    (MBK: mem_block_kind ma fa)
    (FRESH: fresh_block fa z0) ,
  val_eqv fa mf (cclos fid vl) z0.



Lemma match_constr_storelist:
forall ma sp vl z0 n mf cv fa
  (NEQ: fa sp = Some RB)
  (G: fa z0 = Some HB)
  (NV: vallist_eqv fa ma vl cv )
  (STL: storelist ma z0 0 (Vint (int_of_nat n) ::
 (map (fun x=>Vptr x Int.zero) cv)) = Some mf)
  (LB: low_bound ma z0 = 0)
  (HiB: high_bound ma z0 = Z_of_nat (S (length cv)) * 4 + 4)
   (VB: valid_block ma z0)
  (COND: Z_of_nat (S (length cv)) * 4 + 4 < Int.max_signed)
  (FRESH: fresh_block fa z0)
  (MBK: mem_block_kind ma fa),
  val_eqv fa mf (cconstr n vl) z0.


Lemma val_eqv_free:
forall f2 m2 v cv,
  val_eqv f2 m2 v cv ->
 forall spnew (EQ:f2 spnew = Some RB),
  val_eqv f2 (free m2 spnew) v cv.


Lemma vallist_eqv_free:
 forall f2 m cv b, vallist_eqv f2 m cv b->
   forall spnew (EQ:f2 spnew = Some RB),
  vallist_eqv f2 (free m spnew) cv b.

Lemma val_eqv_alloc:
 forall f m v cv, val_eqv f m v cv->
 forall n1 n2 ma a
  (NF: f a = None)
  (ALL: alloc m n1 n2 = (ma,a)),
  val_eqv (add_root f a )ma v cv.





Lemma val_eqv_incr:
forall f ml v cv,val_eqv f ml v cv->
 forall sp k cvl ms (MBK: mem_block_kind ml f)
 (ST : store Mint32 ml sp k cvl = Some ms)
 (VB : f sp = Some RB),
 val_eqv f ms v cv.


Lemma vallist_eqv_incr:
forall f ml v cv,vallist_eqv f ml v cv->
 forall sp k cvl ms (MBK: mem_block_kind ml f)
 (ST : store Mint32 ml sp k cvl = Some ms)
 (VB : f sp = Some RB),
 vallist_eqv f ms v cv.

Lemma vallist_in:
  forall f m l1 l2 , vallist_eqv f m l1 l2 ->
    forall x , In x l1 -> exists x2, In x2 l2 /\ val_eqv f m x x2.

IV. Correspondence between local environments
Inductive match_env:mem->block_kind->fenv->env->Prop:=
| me_intro: forall m f fe ce,
 (forall id v, var_test_prop id -> PTree.get id fe =Some v ->
                   exists b, PTree.get id ce = Some (Vptr b Int.zero) /\
                                    val_eqv f m v b) ->
 mem_block_kind m f->
 match_env m f fe ce.

Lemma me_empty:
forall f mf e
 (MBK: mem_block_kind mf f),
 match_env mf f (PTree.empty cval) e.

Lemma me_tmp_st:
 forall m f e ce v,
   match_env m f e ce ->
   match_env m f e (PTree.set tmp_st v ce).

 Lemma me_res:
 forall m f e ce v,
   match_env m f e ce ->
   match_env m f e (PTree.set res v ce).

 Lemma me_roots:
 forall m f e ce v,
   match_env m f e ce ->
   match_env m f e (PTree.set Roots v ce).

Lemma match_env_let:
forall ml f e ce1 v1 cvl id,
    match_env ml f e ce1->val_eqv f ml v1 cvl->
    match_env ml f (PTree.set id v1 e)
          (PTree.set id (Vptr cvl Int.zero) ce1).

Lemma me_store_stack:
 forall ml f e1 cel ms cvl k sp
 (VB: f sp = Some RB)
 (ME: match_env ml f e1 cel)
 (ST:store Mint32 ml sp k cvl = Some ms),
 match_env ms f e1 cel.

Lemma match_env_vundef:
     forall m sp id me e,
 PTree.get id me = None ->
 match_env m sp me e ->
 match_env m sp me (PTree.set id Vundef e) .

Lemma match_env_set_local:
  forall l m sp me e,
 (forall id, In id l -> PTree.get id me = None) ->
 match_env m sp me e ->
 match_env m sp me (set_locals l e) .

Lemma set_correct:
 forall f ms fvl cvl, vallist_eqv f ms fvl cvl ->
  forall l me me' e
   (ME: match_env ms f me e)
   (P1: forall x, In x l -> PTree.get x me = None)
   (P2: list_norepet l)
   (SET:set_loc_par l fvl me= Some me' ),
   match_env ms f me'
      (set_params2 (map (fun x=>Vptr x Int.zero) cvl) l e).

Lemma match_equiv:
 forall m f me e e'
    (ME: match_env m f me e)
    (EQV: env_equiv e e'),
    match_env m f me e'.

Lemma match_env_app:
forall ms f vargs cvl fid vl cva l lx e1 sp
 (MBK: mem_block_kind ms f),
 length l = length (cva::cvl) ->
 vallist_eqv f ms vargs cvl->
  val_eqv f ms (cclos fid vl) cva ->
  varl_test_prop l ->
  list_disjoint lx l ->
  list_norepet l ->
  set_loc_par l (cclos fid vl :: vargs) (PTree.empty cval) =
     Some e1 ->
 match_env ms f e1
   (set_locals lx
         (set_params (Vptr sp Int.zero ::
                                   (map (fun x : block => Vptr x Int.zero) (cva::cvl)))
                                   (Roots::l) )).



Lemma alloc_match_env:
 forall ms me f e ma spa q
 (ME: match_env ms f me e)
 (ALL:alloc ms 0 q=(ma,spa)) ,
  match_env ma (add_root f spa) me e.




V. Correspondence between the root environment and the Cminor stack block

Inductive match_sp:
 mem->block_kind->spenv->block->Prop:=
|ms_intro: forall m f sc sp,
  mem_block_kind m f ->
  f sp = Some RB ->
  (exists sp2, load Mint32 m sp 0 = Some (Vptr sp2 Int.zero) /\
                     f sp2 = Some RB /\ sp2 <sp) ->
  (forall n v, sp_get n sc = Some v ->
 exists b,
   load Mint32 m sp (8+(Z_of_nat n)*4) =Some (Vptr b Int.zero) /\
   val_eqv f m v b ) ->
   match_sp m f sc sp.

Lemma match_sp_empty:
 forall f m sp
 (VB: f sp = Some RB )
 (LD:exists sp2, load Mint32 m sp 0 = Some (Vptr sp2 Int.zero) /\
                     f sp2 = Some RB /\ sp2 <sp)
 (MBK: mem_block_kind m f) ,
 match_sp m f sp_empty sp.

Lemma match_sp_store_stack:
 forall ml s1 sp n v1 cvl ms f
 (MS: match_sp ml f s1 sp)
 (VE: val_eqv f ml v1 cvl)
 (ST:store Mint32 ml sp (8 + Z_of_nat n * 4)
  (Vptr cvl Int.zero) = Some ms),
 match_sp ms f (sp_set n v1 s1) sp .


Lemma match_sp_store_size:
 forall ml f s1 sp cvl ms
 (MS:match_sp ml f s1 sp )
 (ST:store Mint32 ml sp 4
 (Vint (Int.repr (Z_of_nat cvl))) = Some ms),
 match_sp ms f s1 sp .


Lemma match_sp_gc:
 forall m1 f1 s1 sp ma fa
   (CD: high_bound m1 sp < Int.max_signed)
   (SB: match_sp m1 f1 s1 sp)
   (GC: gc_mem m1 f1 sp ma fa),
   match_sp ma fa s1 sp.

Lemma exec_call_msp:
 forall m1 f1 sp ma fa s1 q
    (VB: valid_block m1 sp)
   (LS: lim_stack q)
   (EQ:high_bound m1 sp =8+Z_of_nat q*4+4)
   (GCM: gc_mem m1 f1 sp ma fa )
   (SP: match_sp m1 f1 s1 sp) ,
   match_sp ma fa s1 sp .

VII. Building of contexts correspondences for smart constructors

Lemma exec_Store_stack:
forall ml fl sp e1 cel s1 q n v1 cvl
  (ME: match_env ml fl e1 cel)
 (MS:match_sp ml fl s1 sp )
 (SP: sp_block sp ml q)
 (LS: lim_stack q) (BDT:bound_test n q) (MV: val_eqv fl ml v1 cvl),
exists ms,
 store Mint32 ml sp (8+Z_of_nat n*4) (Vptr cvl Int.zero) = Some ms /\
 exec_stmt g (Vptr sp Int.zero) (PTree.set tmp_st (Vptr cvl Int.zero) cel) ml
    (Store_stack n (Evar tmp_st))
 Eve (PTree.set tmp_st (Vptr cvl Int.zero) cel) ms Out_normal /\
 match_env ms fl e1 (PTree.set tmp_st (Vptr cvl Int.zero) cel)/\
 match_sp ms fl (sp_set n v1 s1) sp /\
 sp_block sp ms q/\ roots_trans ml fl sp ms fl.

Lemma exec_Store_size:
forall ml fl sp e1 cel s1 q z
  (ME: match_env ml fl e1 cel)
 (MS:match_sp ml fl s1 sp )
 (SP: sp_block sp ml q)
 (LS: lim_stack q) ,
exists ms,
 store Mint32 ml sp 4 (Vint (Int.repr (Z_of_nat z))) = Some ms /\
 exec_stmt g (Vptr sp Int.zero) cel ml
    (Store_stsize (Z_of_nat z)) Eve cel ms Out_normal /\
 match_env ms fl e1 cel /\
 match_sp ms fl s1 sp /\
 sp_block sp ms q /\
 roots_trans ml fl sp ms fl.

Axiom exec_alloc_call:
 forall sp ce1 m1 id n f1,
   Z_of_nat n*4+4 <Int.max_signed ->
   mem_block_kind m1 f1 ->
   exists fa, exists ma, exists z,
   exec_stmt g (Vptr sp Int.zero) ce1 m1
                 (alloc_call id n) Eve (PTree.set id (Vptr z Int.zero)
                  (@PTree.empty val))
                  ma Out_normal /\
  (low_bound ma z) = 0 /\
  (high_bound ma z)= Z_of_nat n *4 +4/\
  f1 z = None /\ fa z = Some HB /\ valid_block ma z/\
  gc_mem m1 f1 sp ma fa/\ fresh_block fa z/\
 (forall q, sp_block sp m1 q -> sp_block sp ma q).

Lemma storelist_1:
forall cv s1 q z0 ma fa sp k
 (LB: low_bound ma z0 = 0 )
 (HiB: high_bound ma z0 = (Z_of_nat (k+length cv) )*4 +4)
 (NEW:fa z0 = Some HB)
 (VB: valid_block ma z0)
 (MS:match_sp ma fa s1 sp)
 (SB:sp_block sp ma q) (LS:lim_stack q)
 (FRESH:fresh_block fa z0)
 (MBK:mem_block_kind ma fa),
 exists mf,
 storelist ma z0 (Z_of_nat k*4) cv =Some mf /\
 match_sp mf fa s1 sp /\
 sp_block sp mf q /\
 gc_mem ma fa sp mf fa.


Lemma gen_bind_vars:
forall xl vl cl m1 f1 e ce1 s0 sp q cva n e1 s1
  (NEQ: cva<> sp)
  (VEL: vallist_eqv f1 m1 vl cl )
  (D: (Z_of_nat (length vl)*4)+(Z_of_nat n*4+4) < Int.max_signed)
  (LN : list_norepet xl)
  (VT : varpl_test_prop xl)
  (ME : match_env m1 f1 e ce1)
  (GET: PTree.get res ce1 =Some (Vptr cva Int.zero))
  (MS : match_sp m1 f1 s0 sp)
  (SPB : sp_block sp m1 q)
  (LS: lim_stack q)
  (LPW: list_param_bound q xl)
  (LD : loadlist m1 cva (Z_of_nat n*4+4) (length vl) =
     Some
       (map (fun x : block => Vptr x Int.zero) cl))
  (SET:set_local_pat xl vl e s0 = Some (e1, s1)),
  exists f2,exists m2,exists ce2,
     exec_stmt g (Vptr sp Int.zero) ce1 m1
             (gen_bind_vars (Evar res) (Z_of_nat n*4+4) xl)
    Eve ce2 m2 Out_normal /\
     match_env m2 f2 e1 ce2 /\
     match_sp m2 f2 s1 sp/\
     sp_block sp m2 q/\
     roots_trans m1 f1 sp m2 f2.







VII. Simulation scheme for atoms translation
Lemma gen_atom_correct1:
 forall (fe1:fenv) (se1:spenv) (a:catom) (v:cval),
  ceval_atom fe1 se1 a v ->
  forall sp ce1 m1 f1 q (LS: lim_stack q)
    (ME: match_env m1 f1 fe1 ce1) (MS: match_sp m1 f1 se1 sp )
    (WB: well_atom_bound q a)(SPB: sp_block sp m1 q) ,
  exists cv,
   Eval_expr g (Vptr sp Int.zero) ce1 m1 (gen_atom a) cv
   /\ val_eqv f1 m1 v cv
  /\ valid_block m1 cv
   /\ (forall ma x, f1 x = Some HB ->
              fresh_block f1 x -> mem_incr m1 ma x->
              Eval_expr g (Vptr sp Int.zero) ce1 ma (gen_atom a) cv).





Lemma gen_atom_correct:
 forall (fe1:fenv) (se1:spenv) (a:catom) (v:cval),
  ceval_atom fe1 se1 a v ->
  forall sp ce1 m1 f1 q (LS: lim_stack q)
    (ME: match_env m1 f1 fe1 ce1) (MS: match_sp m1 f1 se1 sp )
    (WB: well_atom_bound q a)(SPB: sp_block sp m1 q) ,
  exists cv,
   Eval_expr g (Vptr sp Int.zero) ce1 m1 (gen_atom a) cv
   /\ val_eqv f1 m1 v cv.




Lemma gen_atlist_correct:
 forall (fe1:fenv) (se1:spenv) (a:list catom) (v:list cval),
  ceval_atlist fe1 se1 a v ->
  forall sp ce1 m1 f1 q (LS: lim_stack q)
    (ME: match_env m1 f1 fe1 ce1) (MS: match_sp m1 f1 se1 sp )
    (WB: well_atomlist_bound q a)(SPB: sp_block sp m1 q) ,
   exists cv,
   Eval_exprlist g (Vptr sp Int.zero) ce1 m1 (gen_atomlist a) cv
   /\ vallist_eqv f1 m1 v cv .


Lemma gen_atlist_correct1:
 forall (fe1:fenv) (se1:spenv) (a:list catom) (v:list cval),
  ceval_atlist fe1 se1 a v ->
  forall sp ce1 m1 f1 q (LS: lim_stack q)
    (ME: match_env m1 f1 fe1 ce1) (MS: match_sp m1 f1 se1 sp )
    (WB: well_atomlist_bound q a)(SPB: sp_block sp m1 q) ,
   exists cv,
   Eval_exprlist g (Vptr sp Int.zero) ce1 m1 (gen_atomlist a) cv
   /\ vallist_eqv f1 m1 v cv
   /\ (forall b, In b cv-> valid_block m1 b)
  /\ (forall ma x, f1 x = Some HB ->
              fresh_block f1 x -> mem_incr m1 ma x->
              Eval_exprlist g (Vptr sp Int.zero) ce1 ma (gen_atomlist a) cv).

VIII. Translation of constructors correctness
Lemma con_correct_inter:
 forall id s1 tl vl z n m1 e1 ce1 sp q f1
(E : ceval_atlist (PTree.empty cval) s1 tl vl)
(D: 8 + Z_of_nat z * 4 + 4 < Int.max_signed)
(F : Z_of_nat (S (length tl)) * 4 + 4 < Int.max_signed)
(ME : match_env m1 f1 e1 ce1)
(MS : match_sp m1 f1 s1 sp)
(SPB : sp_block sp m1 q)
(LS : lim_stack q)
(WB : well_bound q (Ccon n tl z)),
exists f2:block_kind,
exists ce2 : env,
  exists m2 : mem,
    exists cv : block,
      exec_stmt g (Vptr sp Int.zero) ce1 m1
      (mk_constr id n (Z_of_nat z) (S (length tl)) (gen_atomlist tl)) Eve
        (PTree.set id (Vptr cv Int.zero) ce2) m2 Out_normal /\
      match_env m2 f2 (PTree.empty cval) ce2 /\
      match_sp m2 f2 s1 sp /\
      val_eqv f2 m2 (cconstr n vl) cv /\
      sp_block sp m2 q /\ roots_trans m1 f1 sp m2 f2.










VIII. Translation of closures correctness
Lemma clos_correct_inter:
forall id d tl vl z e1 ce1 sp q m1 fid s1 f1
 (A: recup_cfunct fid s = Some d)
(B: ceval_atlist (PTree.empty cval) s1 tl vl)
(C: 8 + Z_of_nat z * 4 + 4 < Int.max_signed)
(D : Z_of_nat (S (length tl)) * 4 + 4 < Int.max_signed)
(ME : match_env m1 f1 e1 ce1)
(MS : match_sp m1 f1 s1 sp)
(SPB : sp_block sp m1 q)
(LS : lim_stack q)
(WB : well_bound q (Cclos fid tl z))
 (FINIT: block_kind_incr finit f1),
exists f2:block_kind,
exists ce2 : PTree.t val,
  exists m2 : mem,
    exists cv : block,
      exec_stmt g (Vptr sp Int.zero) ce1 m1
        (Sseq (Store_stsize (Z_of_nat z))
           (Sseq (alloc_call id (S (length tl)))
              (Sseq (Sstore Mint32 (Evar id) (addrsymbol fid))
                 (gen_fill_block id 4 (gen_atomlist tl))))) Eve
        (PTree.set id (Vptr cv Int.zero) ce2) m2 Out_normal /\
      match_env m2 f2 (PTree.empty cval) ce2 /\
      match_sp m2 f2 s1 sp /\
      val_eqv f2 m2 (cclos fid vl) cv /\
      sp_block sp m2 q /\ roots_trans m1 f1 sp m2 f2.











IX. Simulation schemes for both translations
Definition genCorA (fe1:fenv) (se1:spenv) (c:Cterm)
                               (fe2:fenv) (se2:spenv) (v:cval):=
 forall sp ce1 m1 f1 q
    (ME: match_env m1 f1 fe1 ce1)
    (MS: match_sp m1 f1 se1 sp )
    (SPB: sp_block sp m1 q)
    (LS: lim_stack q) (WB: well_bound q c)
    (FINIT: block_kind_incr finit f1) ,
 forall id,
  exists f2, exists ce2,exists m2,exists cv,
    exec_stmt g (Vptr sp Int.zero) ce1 m1 (gen_term id c)
       Eve (PTree.set id (Vptr cv Int.zero ) ce2) m2 Out_normal /\
    match_env m2 f2 fe2 ce2/\match_sp m2 f2 se2 sp /\
    val_eqv f2 m2 v cv/\sp_block sp m2 q /\
     roots_trans m1 f1 sp m2 f2 .

Definition genCorB (fe1:fenv) (se1:spenv) (c:Cterm)
                               (fe2:fenv) (se2:spenv) (v:cval):=
 forall sp ce1 m1 f1 q
    (ME: match_env m1 f1 fe1 ce1)
    (MS: match_sp m1 f1 se1 sp )
    (SPB: sp_block sp m1 q)
    (LS: lim_stack q) (WB: well_bound q c)
    (FINIT: block_kind_incr finit f1),
 exists ce2,exists m2,exists cv, exists out,
     exec_stmt g (Vptr sp Int.zero) ce1 m1
       (gen_term_tail c) Eve ce2 m2 out /\
    ((exists f2,out = (Out_return (Some (Vptr cv Int.zero)) )/\
     match_env m2 f2 fe2 ce2/\match_sp m2 f2 se2 sp /\
     val_eqv f2 m2 v cv/\ sp_block sp m2 q/\
     roots_trans m1 f1 sp m2 f2)
    \/
     ( exists f2, exists sp_pre,
       load Mint32 m1 sp 0 = Some (Vptr sp_pre Int.zero) /\
       out = Out_tailcall_return (Vptr cv Int.zero)/\
       match_env m2 f2 fe2 ce2/\val_eqv f2 m2 v cv/\
       gc_mem m1 f1 sp_pre m2 f2)
       ).

Definition genCor (fe1:fenv) (se1:spenv) (c:Cterm)
                               (fe2:fenv) (se2:spenv) (v:cval):=
 forall sp ce1 m1 f1 q
    (ME: match_env m1 f1 fe1 ce1)
    (MS: match_sp m1 f1 se1 sp )
    (SPB: sp_block sp m1 q)
    (LS: lim_stack q) (WB: well_bound q c)
    (FINIT: block_kind_incr finit f1) ,
 ( forall id, exists f2,
  exists ce2,exists m2,exists cv,
    exec_stmt g (Vptr sp Int.zero) ce1 m1 (gen_term id c)
       Eve (PTree.set id (Vptr cv Int.zero ) ce2) m2 Out_normal /\
    match_env m2 f2 fe2 ce2/\match_sp m2 f2 se2 sp /\
    val_eqv f2 m2 v cv/\sp_block sp m2 q /\
     roots_trans m1 f1 sp m2 f2)/\
 exists ce2,exists m2,exists cv, exists out,
     exec_stmt g (Vptr sp Int.zero) ce1 m1
       (gen_term_tail c) Eve ce2 m2 out /\
    (
     (exists f2, out = (Out_return (Some (Vptr cv Int.zero)) )/\
     match_env m2 f2 fe2 ce2/\match_sp m2 f2 se2 sp /\
     val_eqv f2 m2 v cv/\ sp_block sp m2 q/\
     roots_trans m1 f1 sp m2 f2)
    \/ ( exists f2, exists sp_pre,
       load Mint32 m1 sp 0 = Some (Vptr sp_pre Int.zero) /\
       out = Out_tailcall_return (Vptr cv Int.zero)/\
       match_env m2 f2 fe2 ce2/\val_eqv f2 m2 v cv/\
       gc_mem m1 f1 sp_pre m2 f2)
       ).

Lemma catom_correct:
forall (e1 : Fminor.env) (s1 : spenv) (a : catom) (va : cval),
        ceval_atom e1 s1 a va ->
         genCor e1 s1 (Catom a) e1 s1 va.

Lemma con_correct:
forall (z : nat) (e1 : Fminor.env) (n : nat) (s1 : spenv)
    (tl : list catom) (vl : list cval),
  ceval_atlist (PTree.empty cval) s1 tl vl ->
  8 + Z_of_nat z * 4 + 4 < Int.max_signed ->
  Z_of_nat (S (length tl)) * 4 + 4 < Int.max_signed ->
  genCor e1 s1 (Ccon n tl z) (PTree.empty cval) s1 (cconstr n vl).






Lemma clos_correct:
forall (z : nat) (e1 : Fminor.env) (s1 : spenv) (fid : ident)
 (d : cfunction) (tl : list catom) (vl : list cval),
   recup_cfunct fid s = Some d ->
   ceval_atlist (PTree.empty cval) s1 tl vl ->
   8 + (Z_of_nat z) * 4 + 4 < Int.max_signed ->
    Z_of_nat (S (length tl)) * 4 +4 < Int.max_signed ->
   genCor e1 s1 (Cclos fid tl z) (PTree.empty cval) s1 (cclos fid vl).






Lemma let_correct:
forall (id : ident) (e : Fminor.env) (s0 : spenv) (t1 : Cterm)
 (v1 : cval) (e1 : Fminor.env) (s1 : spenv) (t2 : Cterm)
 (v2 : cval) (e2 : Fminor.env) (s2 : spenv),
 ceval_term s e s0 t1 e1 s1 v1 ->
 genCor e s0 t1 e1 s1 v1 ->
 var_test_prop id ->
 ceval_term s (PTree.set id v1 e1) s1 t2 e2 s2 v2 ->
 genCor (PTree.set id v1 e1) s1 t2 e2 s2 v2 ->
 genCor e s0 (Clet id t1 t2) e2 s2 v2.
















Lemma push_correct:
forall (n : nat) (t1 : Cterm) (v1 : cval) (t2 : Cterm)
 (e : Fminor.env) (s0 : spenv) (e1 : Fminor.env) (s1 : spenv)
 (e2 : Fminor.env) (s2 : spenv) (v2 : cval),
 ceval_term s e s0 t1 e1 s1 v1 ->
 genCor e s0 t1 e1 s1 v1 ->
 ceval_term s e1 (sp_set n v1 s1) t2 e2 s2 v2 ->
 genCor e1 (sp_set n v1 s1) t2 e2 s2 v2 ->
 genCor e s0 (Cpush n t1 t2) e2 s2 v2.
















Lemma appA_correct:
forall (z : nat) (info : option ident) (t1 : catom)
 (targs : list catom) (fid : ident) (vl : list cval) (d : cfunction)
 (vargs : list cval) (e : Fminor.env) (s0 : spenv)
 (e1 e2 : Fminor.env) (s2 : spenv) (v : cval),
 ceval_atom e s0 t1 (cclos fid vl) ->
 recup_cfunct fid s = Some d ->
 8 + Z_of_nat z * 4 + 4 < Int.max_signed ->
 ceval_atlist e s0 targs vargs ->
 list_norepet (cn_params d) ->
 varl_test_prop (cn_params d) ->
 list_disjoint (Roots::cn_params d) (cn_vars d) ->
 set_loc_par (cn_params d) (cclos fid vl :: vargs) (PTree.empty cval) =
 Some e1 ->
 8 + Z_of_nat (cn_stackspace d) * 4 + 4 < Int.max_signed ->
 ceval_term s e1 sp_empty (cn_body d) e2 s2 v ->
 genCor e1 sp_empty (cn_body d) e2 s2 v ->
 info = None \/ info = Some fid ->
 genCorA e s0 (Capp info t1 targs z) (PTree.empty cval) s0 v.



































Lemma appB_correct:
forall (z : nat) (info : option ident) (t1 : catom)
 (targs : list catom) (fid : ident) (vl : list cval) (d : cfunction)
 (vargs : list cval) (e : Fminor.env) (s0 : spenv)
 (e1 e2 : Fminor.env) (s2 : spenv) (v : cval),
 ceval_atom e s0 t1 (cclos fid vl) ->
 recup_cfunct fid s = Some d ->
 8 + Z_of_nat z * 4 + 4 < Int.max_signed ->
 ceval_atlist e s0 targs vargs ->
 list_norepet (cn_params d) ->
 varl_test_prop (cn_params d) ->
 list_disjoint (Roots::cn_params d) (cn_vars d) ->
 set_loc_par (cn_params d) (cclos fid vl :: vargs) (PTree.empty cval) =
 Some e1 ->
 8 + Z_of_nat (cn_stackspace d) * 4 + 4 < Int.max_signed ->
 ceval_term s e1 sp_empty (cn_body d) e2 s2 v ->
 genCor e1 sp_empty (cn_body d) e2 s2 v ->
 info = None \/ info = Some fid ->
 genCorB e s0 (Capp info t1 targs z) (PTree.empty cval) s0 v.

























Lemma app_correct:
forall (z : nat) (info : option ident) (t1 : catom)
 (targs : list catom) (fid : ident) (vl : list cval) (d : cfunction)
 (vargs : list cval) (e : Fminor.env) (s0 : spenv)
 (e1 e2 : Fminor.env) (s2 : spenv) (v : cval),
 ceval_atom e s0 t1 (cclos fid vl) ->
 recup_cfunct fid s = Some d ->
 8 + Z_of_nat z * 4 + 4 < Int.max_signed ->
 ceval_atlist e s0 targs vargs ->
 list_norepet (cn_params d) ->
 varl_test_prop (cn_params d) ->
 list_disjoint (Roots::cn_params d) (cn_vars d) ->
 set_loc_par (cn_params d) (cclos fid vl :: vargs) (PTree.empty cval) =
 Some e1 ->
 8 + Z_of_nat (cn_stackspace d) * 4 + 4 < Int.max_signed ->
 ceval_term s e1 sp_empty (cn_body d) e2 s2 v ->
 genCor e1 sp_empty (cn_body d) e2 s2 v ->
 info = None \/ info = Some fid ->
 genCor e s0 (Capp info t1 targs z) (PTree.empty cval) s0 v.


Lemma match_correctA:
forall (e : Fminor.env) (s0 : spenv) (a : catom) (n : nat)
 (vl : list cval) (pl : list cpat) (xl : list Param) (p : Cterm)
 (e1 : Fminor.env) (s1 : spenv) (e2 : Fminor.env) (s2 : spenv)
 (v : cval)(Kay:Zlt (Z_of_nat (length pl)) Int.max_signed ),
 ceval_atom e s0 a (cconstr n vl) ->
 nth_error pl n = Some (CPatc xl p) ->
 list_norepet xl ->
 varpl_test_prop xl ->
 set_local_pat xl vl e s0 = Some (e1, s1) ->
 ceval_term s e1 s1 p e2 s2 v ->
 genCor e1 s1 p e2 s2 v -> genCorA e s0 (Cmatch a pl) e2 s2 v.





Lemma match_correctB:
forall (e : Fminor.env) (s0 : spenv) (a : catom) (n : nat)
 (vl : list cval) (pl : list cpat) (xl : list Param) (p : Cterm)
 (e1 : Fminor.env) (s1 : spenv) (e2 : Fminor.env) (s2 : spenv)
 (v : cval)(Kay:Zlt (Z_of_nat (length pl)) Int.max_signed ),
 ceval_atom e s0 a (cconstr n vl) ->
 nth_error pl n = Some (CPatc xl p) ->
 list_norepet xl ->
 varpl_test_prop xl ->
 set_local_pat xl vl e s0 = Some (e1, s1) ->
 ceval_term s e1 s1 p e2 s2 v ->
 genCor e1 s1 p e2 s2 v -> genCorB e s0 (Cmatch a pl) e2 s2 v.






Lemma match_correct:
 forall (e : Fminor.env) (s0 : spenv) (a : catom) (n : nat)
 (vl : list cval) (pl : list cpat) (xl : list Param) (p : Cterm)
 (e1 : Fminor.env) (s1 : spenv) (e2 : Fminor.env) (s2 : spenv)
 (v : cval),
 Zlt (Z_of_nat (length pl)) Int.max_signed ->
 ceval_atom e s0 a (cconstr n vl) ->
 nth_error pl n = Some (CPatc xl p) ->
 list_norepet xl ->
 varpl_test_prop xl ->
 set_local_pat xl vl e s0 = Some (e1, s1) ->
 ceval_term s e1 s1 p e2 s2 v ->
 genCor e1 s1 p e2 s2 v -> genCor e s0 (Cmatch a pl) e2 s2 v.


Theorem gen_cminor_correct:
forall (e : Fminor.env) (s0 : spenv) (c : Cterm) (e0 : Fminor.env)
 (s1 : spenv) (c0 : cval),
ceval_term s e s0 c e0 s1 c0 -> genCor e s0 c e0 s1 c0.

End COR.