Library M2Fminor_proof

Semantics preservation of the conversion to Fminor



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 Fminor.
Require Import Integers.
Require Import M2Fminor.
Open Scope nat_scope.

I. Invariants of the simulation scheme

Definition gc_cond (t:Identset.t) (ce:cenv):Prop:=
   forall x , Identset.In x t ->
         PTree.get x (cenv_map ce) <> Some Loc_var.

Definition no_gc_concl (ce:cenv) (e1 e2:env):Prop:=
 forall id , PTree.get id (cenv_map ce) = Some Loc_var ->
                 PTree.get id e1 = PTree.get id e2.

Definition stack_concl (ce:cenv) (sp1 sp2:spenv) :Prop:=
 forall id delta, PTree.get id (cenv_map ce) = Some (Loc_slot delta) ->
                  sp_get delta sp1 = sp_get delta sp2.

Definition sp_height_coherence (ce:cenv) :=
  forall id delta,
       PTree.get id (cenv_map ce) = Some (Loc_slot delta) ->
       lt delta (cenv_height ce) .

Definition sp_norepet (ce:cenv):=
 forall x y delta ,
       PTree.get x (cenv_map ce) = Some (Loc_slot delta) ->
       PTree.get y (cenv_map ce) = Some (Loc_slot delta) ->
       x=y.

Definition lim (ce:cenv) :=
 Zlt (8+(Z_of_nat (cenv_height ce))*4+4)%Z Int.max_signed.

Lemma no_gc_concl_refl:
 forall ce e, no_gc_concl ce e e.

Lemma stack_concl_refl:
 forall ce sp,stack_concl ce sp sp.

Lemma gc_cond_union_left:
 forall ce t1 t2,
      gc_cond (Identset.union t1 t2) ce ->
      gc_cond t1 ce.

Lemma gc_cond_union_right:
 forall ce t1 t2,
      gc_cond (Identset.union t1 t2) ce ->
      gc_cond t2 ce.

Lemma gc_cond_subset:
 forall s1 s2 ce, Identset.Subset s2 s1 ->
                          gc_cond s1 ce -> gc_cond s2 ce.


Ltac monadSimpl1 :=
  match goal with
  | [ |- (bind ?F ?G = Some ?X) -> _ ] =>
      unfold bind at 1;
      generalize (refl_equal F);
      pattern F at -1 in |- *;
      case F;
      [ (let EQ := fresh "EQ" in
           (intro; intro EQ; try monadSimpl1))
      | intro; intro; discriminate ]
  | [ |- (None = Some _) -> _ ] =>
      intro; discriminate
  | [ |- (Some _ = Some _) -> _ ] =>
      let h := fresh "H" in
      (intro h; injection h; intro; clear h)
  | [ |- (_ = Some _) -> _ ] =>
      let EQ := fresh "EQ" in intro EQ
  end.

Ltac monadSimpl :=
  match goal with
  | [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1
  | [ |- (None = Some _) -> _ ] => monadSimpl1
  | [ |- (Some _ = Some _) -> _ ] => monadSimpl1
  | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  | [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  | [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  | [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  | [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
  end.

Ltac monadInv H :=
  generalize H; monadSimpl.

Set of variables properties
Lemma remove_subset:
 forall xl s1 s2,
    Identset.Subset s1 s2 ->
    Identset.Subset (Identset.remove xl s1) (Identset.remove xl s2).

Lemma fold_right_remove_subset:
 forall xl s1 s2,
    Identset.Subset s1 s2 ->
    Identset.Subset (fold_right Identset.remove s1 xl )
                               (fold_right Identset.remove s2 xl ).

Lemma Subset_empty:
 forall s, Identset.Subset Identset.empty s.

Lemma Subset_refl:
 forall s, Identset.Subset s s .

Lemma Subset_union_right:
 forall s1 s2 s3, Identset.Subset s1 s2 ->
                          Identset.Subset s1 (Identset.union s3 s2).

Lemma Subset_union_left:
 forall s1 s2 s3, Identset.Subset s1 s3 ->
                          Identset.Subset s1 (Identset.union s3 s2).

Lemma Subset_union:
 forall s1 s2 s3 s4,
    Identset.Subset s1 s3 -> Identset.Subset s2 s4->
    Identset.Subset (Identset.union s1 s2) (Identset.union s3 s4 ) .

Lemma In_fold_in:
forall xl x s,
 list_norepet xl ->
 Identset.In x s ->
  ((~In x xl) -> Identset.In x (fold_right Identset.remove s xl) ).


Lemma in_in_elt:
 forall x y, Identset.In x y <-> In x (Identset.elements y).


Lemma vars_param_disjoint:
 forall l d , list_disjoint l
      (Identset.elements
         (fold_right Identset.remove d l)).

Lemma fv_roots_subset:
 forall t, Identset.Subset (roots_term t) (fv_term t).

Lemma pat_fv_subset:
 forall pl p n , nth_error pl n = Some p ->
            Identset.Subset (fv_pat p) (fv_plist pl).

Lemma pat_rt_subset:
 forall pl p n , nth_error pl n = Some p ->
            Identset.Subset (roots_case p) (roots_cases pl).

Lemma pat_comp_triggers:
 forall pl p n , nth_error pl n = Some p ->
   comp_triggers_pat p =true ->
   comp_triggers_plist pl = true.

Lemma pat_comp_triggers_false:
 forall pl p n ,
  comp_triggers_plist pl = false ->
  nth_error pl n = Some p ->
   comp_triggers_pat p =false.

IV. Building of invariants for inductive hypothesis
Lemma bind_inv :
  forall x r ce b c (LIM:lim ce),
      bind_var x ce r = Some (b, c) ->
     (lim c) /\
     ( if Identset.mem x r
     then b= SL (cenv_height ce) /\
     c = (mkCenv (PTree.set x (Loc_slot (cenv_height ce)) (cenv_map ce))
                           (cenv_height ce +1))
     else b = VR x /\
     c = (mkCenv (PTree.set x Loc_var (cenv_map ce))
                           (cenv_height ce)
       )) /\
     ((cenv_map ce) ! x = None).

Lemma GCC_let_stack:
 forall r1 t1 r2 t2 b1 b2 id ce ,
   Identset.Subset r1 t1 ->Identset.Subset r2 t2 ->
   (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                            else Identset.remove id r2) ce)->
 (b2 = true -> gc_cond r2
      (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1))).







Lemma GCC_let_var:
 forall r1 t1 r2 t2 b1 b2 id ce ,
     Identset.Subset r1 t1 ->Identset.Subset r2 t2 ->
     Identset.mem id r2 = false->
   (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                            else Identset.remove id r2 ) ce)->
 (b2 = true -> gc_cond r2
      (mkCenv (PTree.set id Loc_var (cenv_map ce))
            (cenv_height ce ))).







Lemma SHC_let_stack:
 forall ce id,
 sp_height_coherence ce->
 sp_height_coherence
    (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
       (cenv_height ce + 1)).




Lemma SHC_let_var:
 forall ce id,
 sp_height_coherence ce->
 sp_height_coherence
    (mkCenv (PTree.set id Loc_var (cenv_map ce))
       (cenv_height ce )).




Lemma SNR_let_stack :
forall ce id,
 sp_norepet ce-> sp_height_coherence ce->
 sp_norepet (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
       (cenv_height ce + 1)).





Lemma SNR_let_var:
forall ce id,
sp_norepet ce-> sp_height_coherence ce->
 sp_norepet (mkCenv (PTree.set id Loc_var (cenv_map ce))
       (cenv_height ce )).




Lemma SC_let_stack:
 forall id cv1 ce sp sp1 spres,
   stack_concl ce sp sp1->
   stack_concl (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1))
            (sp_set (cenv_height ce) cv1 sp1) spres->
   sp_height_coherence ce ->
    (cenv_map ce) ! id = None ->
    stack_concl ce sp spres .

Lemma SC_let_var:
 forall id ce sp sp1 spres,
   stack_concl ce sp sp1->
   stack_concl (mkCenv (PTree.set id Loc_var (cenv_map ce))
            (cenv_height ce )) sp1 spres->
    (cenv_map ce) ! id = None ->
    stack_concl ce sp spres .

Lemma CT_let_stack:
forall ce id b1 b2 e1 eres e0 ,
  (cenv_map ce) ! id = None ->
  (b2 = false -> no_gc_concl (
        mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1)) e1 eres)->
 (b1 = false -> no_gc_concl ce e0 e1)->
 (b1||b2 = false -> no_gc_concl ce e0 eres).

Lemma CT_let_var:
 forall ce id b1 b2 e1 eres e0 v1,
 (cenv_map ce) ! id = None ->
 (b2 = false -> no_gc_concl (
        mkCenv (PTree.set id Loc_var (cenv_map ce))
            (cenv_height ce)) (PTree.set id v1 e1) eres)->
 (b1 = false -> no_gc_concl ce e0 e1)->
 (b1||b2 = false -> no_gc_concl ce e0 eres).

Lemma let_context_out:
forall t2 t1 p c1 id cv1 elet splet ce sp sp1 spres e0 e1 eres
   (L:lim ce) ,
   bind_var id ce (roots_term t2) = Some (p, c1)->
 (match p with
      | VR _ =>
          elet = PTree.set id cv1 e1 /\
          splet = sp1 /\
          c1 = mkCenv (PTree.set id Loc_var (cenv_map ce)) (cenv_height ce)
      | SL _ =>
          elet = e1 /\
          splet = sp_set (cenv_height ce) cv1 sp1 /\
          c1 =
          mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1)
      end) ->
  stack_concl ce sp sp1->
  stack_concl c1 splet spres->
  sp_height_coherence ce ->
  (comp_triggers_gc t2 = false -> no_gc_concl c1 elet eres)->
  (comp_triggers_gc t1 = false -> no_gc_concl ce e0 e1)->
 stack_concl ce sp spres /\
(comp_triggers_gc (Flet id t1 t2) = false -> no_gc_concl ce e0 eres).

Lemma bind_vars_inv:
 forall xl r ce xbl lacc c
      (LIM: lim ce )
     (SF:forall p, In p lacc ->
         match p with | SL d => lt d (cenv_height ce)
                                 | VR id => (cenv_map ce) !id = Some Loc_var
         end),
     list_norepet xl ->list_norepet lacc->
     bind_vars xl ce r lacc = Some (xbl, c) ->
 exists xl', length xl' = length xl /\
                  (forall id, In id xl -> (cenv_map ce)!id = None) /\
                   list_norepet xbl /\
                   (forall id v, (cenv_map ce)!id = Some v ->
                                        (cenv_map c)!id = Some v) /\
                  xbl = lacc++xl' /\ lim c .




Lemma gc_cond_empty:
 forall r, gc_cond r empty_cenv.
Lemma sp_empty_coh_nor:
 sp_height_coherence empty_cenv /\
 sp_norepet empty_cenv.

Lemma GC_empty:
 forall b r , b= true -> gc_cond r empty_cenv.

Lemma match_nth:
forall pl n p ce l,
 nth_error pl n = Some p ->
 germ_patlist pl ce = Some l->
exists cp, nth_error l n = Some cp /\
                 germ_pat p ce = Some cp.

Section COR.

 Variable s: list (ident*funct).
 Variable sc :list (ident*cfunction).

 Hypothesis match_glo:
    forall id d, recup_funct id s=Some d ->
    exists cd, recup_cfunct id sc=Some cd /\
                     germ_cfunction d = Some cd.

V. Correspondence between environments
Inductive match_val: fval->cval->Prop:=
 | mclos: forall id fvl cvl d cd ,
             match_vallist fvl cvl ->
             recup_funct id s = Some d->
             recup_cfunct id sc = Some cd ->
             match_val (fclos id fvl) (cclos id cvl)
 | mconstr: forall n fvl cvl,
             match_vallist fvl cvl->
             match_val (fconstr n fvl) (cconstr n cvl)
with match_vallist:list fval->list cval->Prop:=
 |mnil: match_vallist nil nil
 |mcons: forall fh ft ch ct,
     match_val fh ch ->match_vallist ft ct ->
     match_vallist (fh::ft) (ch::ct).

Definition match_var (id:ident) (v:fval) (info:location)
  (e:env) (sp:spenv) (n:nat):=
 match info with
 | Loc_var => exists cv, PTree.get id e = Some cv /\
                                         match_val v cv
| Loc_slot m => lt m n /\
    exists cv, sp_get m sp = Some cv /\
                                         match_val v cv
end.

Definition fenv:= Mml.env.

Definition var_in_env (t:Identset.t) (ce:cenv) (fe:fenv) (e:env)
 (sp:spenv):Prop:=
    forall id v info, Identset.In id t ->
    PTree.get id fe = Some v ->
    PTree.get id (cenv_map ce) = Some info ->
    match_var id v info e sp (cenv_height ce).

Lemma match_val_nth:
 forall fvl cvl , match_vallist fvl cvl ->
 forall n0 v , nth_error fvl n0 =Some v ->
 exists cv, nth_error cvl n0 = Some cv /\ match_val v cv.

Lemma var_in_env_union_left:
 forall ce t1 t2 fe e sp ,
    var_in_env (Identset.union t1 t2) ce fe e sp ->
    var_in_env t1 ce fe e sp.

Lemma var_in_env_union_right:
 forall ce t1 t2 fe e sp ,
    var_in_env (Identset.union t1 t2) ce fe e sp ->
    var_in_env t2 ce fe e sp.

Lemma var_in_env_subset:
 forall ce s1 s2 fe e sp,
   Identset.Subset s2 s1 ->
   var_in_env s1 ce fe e sp ->
   var_in_env s2 ce fe e sp.

Lemma VIE_let_stack :
 forall r1 t1 r2 t2 b1 b2 id ce e e0 sp v1 cv1 sp1 e1
 (S1:Identset.Subset r1 t1) (S2:Identset.Subset r2 t2),
 var_in_env
        (Identset.union t1 (Identset.remove id t2)) ce e
        e0 sp ->
 (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                            else Identset.remove id r2) ce)->
 (cenv_map ce) ! id = None->
 match_val v1 cv1->
 (b1= false -> no_gc_concl ce e0 e1) ->
 Identset.mem id r2 = true->
  stack_concl ce sp sp1->
    var_in_env t2
           (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
           (cenv_height ce + 1))
            (PTree.set id v1 e) e1 (sp_set (cenv_height ce) cv1 sp1).










Lemma VIE_let_var :
 forall r1 t1 r2 t2 b1 b2 id ce e e0 sp v1 cv1 sp1 e1 ,
   Identset.Subset r1 t1 -> Identset.Subset r2 t2 ->
 var_in_env
        (Identset.union t1 (Identset.remove id t2)) ce e
        e0 sp ->
 (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                                 else Identset.remove id r2 ) ce)->
 (cenv_map ce) ! id = None->
 match_val v1 cv1->
 (b1 = false -> no_gc_concl ce e0 e1) ->
 Identset.mem id r2 = false->
  stack_concl ce sp sp1->
    var_in_env t2
           (mkCenv (PTree.set id Loc_var (cenv_map ce))
           (cenv_height ce ))
            (PTree.set id v1 e) (PTree.set id cv1 e1) sp1.










VI. Let inductive hypothesis invariants
 Lemma let_context_stack:
forall r1 t1 r2 t2 b1 b2 id ce e e0 sp v1 cv1 sp1 e1
  (S1:Identset.Subset r1 t1) (S2:Identset.Subset r2 t2),
   var_in_env
        (Identset.union t1 (Identset.remove id t2)) ce e
        e0 sp ->
   sp_height_coherence ce->
   sp_norepet ce->
   (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                            else Identset.remove id r2) ce)->
   (cenv_map ce) ! id = None->
    (b1 = true -> gc_cond r1 ce) ->
    match_val v1 cv1->
    stack_concl ce sp sp1->
    (b1 = false -> no_gc_concl ce e0 e1) ->
    Identset.mem id r2 = true->
    var_in_env t2
           (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
           (cenv_height ce + 1))
            (PTree.set id v1 e) e1 (sp_set (cenv_height ce) cv1 sp1) /\
     (b2 = true -> gc_cond r2
      (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1)))/\
       sp_height_coherence
    (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
       (cenv_height ce + 1))/\
     sp_norepet (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
       (cenv_height ce + 1)).

Lemma let_context_var:
forall r1 t1 t2 r2 id ce e e0 sp v1 cv1 sp1 e1 b1 b2,
   Identset.Subset r1 t1 -> Identset.Subset r2 t2 ->
   var_in_env
        (Identset.union t1 (Identset.remove id t2)) ce e
        e0 sp ->
   sp_height_coherence ce->
   sp_norepet ce->
   (b1||b2 = true ->
         gc_cond (if b1 then Identset.union r1 (Identset.remove id t2)
                            else Identset.remove id r2 ) ce)->
   (cenv_map ce) ! id = None->
    (b1 = true -> gc_cond r1 ce) ->
    match_val v1 cv1->
    stack_concl ce sp sp1->
    (b1 = false -> no_gc_concl ce e0 e1) ->
    Identset.mem id r2 = false->
    var_in_env t2
           (mkCenv (PTree.set id Loc_var (cenv_map ce))
           (cenv_height ce ))
            (PTree.set id v1 e) (PTree.set id cv1 e1) sp1 /\
     (b2 = true -> gc_cond r2
      (mkCenv (PTree.set id Loc_var (cenv_map ce))
            (cenv_height ce )))/\
       sp_height_coherence
    (mkCenv (PTree.set id Loc_var (cenv_map ce))
       (cenv_height ce )) /\
      sp_norepet (mkCenv (PTree.set id Loc_var (cenv_map ce))
       (cenv_height ce )).

Lemma let_context:
forall t1 t2 id ce e e0 sp v1 cv1 sp1 e1 b c1 (LIM:lim ce),
   var_in_env
        (Identset.union (fv_term t1) (Identset.remove id (fv_term t2))) ce e
        e0 sp ->
   sp_height_coherence ce->
   sp_norepet ce->
   (comp_triggers_gc (Flet id t1 t2) = true ->
         gc_cond (roots_term (Flet id t1 t2)) ce)->
    (comp_triggers_gc t1 = true -> gc_cond (roots_term t1) ce) ->
    match_val v1 cv1->
    stack_concl ce sp sp1->
    (comp_triggers_gc t1 = false -> no_gc_concl ce e0 e1) ->
     bind_var id ce (roots_term t2) = Some (b,c1) ->
   exists elet, exists splet,
   (match b with | SL n =>
   elet = e1 /\ splet = (sp_set (cenv_height ce) cv1 sp1) /\
   c1 = (mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
            (cenv_height ce + 1))
   | _ =>
    elet = (PTree.set id cv1 e1) /\splet = sp1 /\
    c1 = (mkCenv (PTree.set id Loc_var (cenv_map ce)) (cenv_height ce ))
   end) /\ (
   var_in_env (fv_term t2) c1 (PTree.set id v1 e) elet splet /\
   (comp_triggers_gc t2 = true -> gc_cond (roots_term t2) c1) /\
    sp_height_coherence c1 /\
    sp_norepet c1 )/\ lim c1.





VII. Application inductive hypothesis invariants

Lemma var_in_env_sm_dom:
 forall s1 s2 ce fe e sp,
  Identset.Subset s1 s2 -> Identset.Subset s2 s1->
  var_in_env s1 ce fe e sp ->
  var_in_env s2 ce fe e sp.

Lemma add_stack_context:
 forall f r p ce fe e sp fh ch b c1 sp1
 (GC: b = true -> gc_cond r ce)
 (VIE: var_in_env (Identset.remove p f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SN: sp_norepet ce)
 (A: (cenv_map ce) ! p = None)
 (MV: match_val fh ch)
 (MEM: Identset.mem p r = true)
 (EQ1: c1= mkCenv (PTree.set p (Loc_slot (cenv_height ce)) (cenv_map ce))
        (cenv_height ce + 1))
 (EQ2: sp1 = sp_set (cenv_height ce) ch sp ),
  var_in_env f c1 (PTree.set p fh fe) e sp1 /\
   (b=true -> gc_cond r c1) /\
   sp_height_coherence c1 /\
   sp_norepet c1 .











Lemma add_var_context:
 forall f r p ce fe e sp fh ch b c1 e1
 (GC: b = true -> gc_cond r ce)
 (VIE: var_in_env (Identset.remove p f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SN: sp_norepet ce)
 (A: (cenv_map ce) ! p = None)
 (MV: match_val fh ch)
 (MEM: Identset.mem p r = false)
 (EQ1: c1= mkCenv (PTree.set p Loc_var (cenv_map ce))
        (cenv_height ce ))
 (EQ2: e1 = PTree.set p ch e ),
  var_in_env f c1 (PTree.set p fh fe) e1 sp /\
   (b=true -> gc_cond r c1) /\
   sp_height_coherence c1 /\
   sp_norepet c1.











Lemma add_elt_context:
 forall f r p ce fe e sp fh ch b c1 k
 (GC: b = true -> gc_cond r ce) (LI :lim ce)
 (VIE: var_in_env (Identset.remove p f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SN: sp_norepet ce)
 (A: bind_var p ce r = Some (k,c1) )
 (MV: match_val fh ch) ,
  exists e1,exists sp1,
   (if (Identset.mem p r) then
      ( c1 = (mkCenv
                (PTree.set p (Loc_slot (cenv_height ce)) (cenv_map ce))
                 (cenv_height ce +1)) /\e1=e/\sp1= (sp_set (cenv_height ce) ch sp))
      else
      (c1 = (mkCenv (PTree.set p Loc_var (cenv_map ce) )
                               (cenv_height ce)) /\
       e1 = PTree.set p ch e /\ sp1=sp)) /\
   (var_in_env f c1 (PTree.set p fh fe) e1 sp1 /\
   (b=true -> gc_cond r c1) /\
   sp_height_coherence c1 /\
   sp_norepet c1 )/\ lim c1.

Lemma params_context:
 forall fvl cvl , match_vallist fvl cvl ->
 forall f r ce fe e sp ld l l0 c fe1 (b:bool) (LIM:lim ce)
 (LN: list_norepet ld)
 (LN2:list_norepet l)
 (SF:forall p, In p l ->
         match p with | SL d => lt d (cenv_height ce)
                                 | VR id => (cenv_map ce) !id = Some Loc_var
         end)
 (GC: b=true -> gc_cond r ce)
 (VIE : var_in_env (List.fold_right Identset.remove f ld ) ce fe e sp )
 (SET: set_local_par ld fvl fe=Some fe1)
 (BD: bind_vars ld ce r l = Some (l++l0, c) )
  (SH: sp_height_coherence ce) (SN: sp_norepet ce),
 exists e1,exists sp1,
   set_local_pat l0 cvl e sp = Some (e1,sp1) /\
   sp_height_coherence c /\
   sp_norepet c /\ (b=true -> gc_cond r c) /\
   var_in_env f c fe1 e1 sp1 /\
   (b=false -> no_gc_concl ce e e1) /\
   stack_concl ce sp sp1/\ list_norepet (l++l0) /\
   lim c.





Lemma vie_empty:
 forall l , var_in_env l empty_cenv
 (PTree.empty fval) (PTree.empty cval) sp_empty.


Remark lim_empty: lim empty_cenv.

Lemma app_context:
forall vargs cva d l0 c e1 ,
 match_vallist vargs cva->list_norepet (fun_par d) ->
 bind_vars (fun_par d) empty_cenv (roots_term (fun_body d)) nil = Some (l0, c) ->
 set_local_par (fun_par d) vargs (PTree.empty fval) =
     Some e1->
 exists e,exists sp,
   set_local_pat l0 cva (PTree.empty cval) sp_empty = Some (e,sp) /\
   sp_height_coherence c /\
   sp_norepet c /\
  (comp_triggers_gc (fun_body d) = true ->
      gc_cond (roots_term (fun_body d)) c)/\
   var_in_env (fv_term (fun_body d)) c e1 e sp /\
    list_norepet l0 /\ lim c.

VIII. Pattern-matchin inductive hypothesis invariants
Lemma in_peq_list:
 forall l (p:positive) (LN:list_norepet l), In p l \/ ~ In p l.

Lemma plist_nth_gc_vie:
forall pl a ce e e0 sp xl n p (LN:list_norepet xl)
   (SF: forall id, In id xl -> (cenv_map ce) !id =None )
  (VIE : var_in_env (Identset.union (fv_atom a) (fv_plist pl)) ce e e0 sp)
 (NTH: nth_error pl n = Some (FPatc xl p))
 (GCC: comp_triggers_gc (Fmatch a pl) = true ->
      gc_cond (roots_term (Fmatch a pl)) ce ) ,
  (comp_triggers_gc p = true ->
      gc_cond (roots_term p) ce) /\
  var_in_env (List.fold_right Identset.remove (fv_term p) xl) ce e e0 sp.


Lemma bind_varp:
 forall id ce r info e0,
 var_test_prop id -> bind_var id ce r = Some (info,e0) ->
 varp_test_prop info.

Lemma binds_varpl:
   forall id ce r info e0 lk ,
 varpl_test_prop lk ->
 varl_test_prop id -> bind_vars id ce r lk = Some (info,e0) ->
 varpl_test_prop info.

Lemma match_context:
forall vl cva, match_vallist vl cva ->
forall n xl e e1 e0 sp a pl p l0 c ce
   (LIM :lim ce) (VT: varl_test_prop xl)
   (NTH: nth_error pl n = Some (FPatc xl p))
   (SET: set_local_par xl vl e = Some e1)
   ( LN: list_norepet xl )
   (VIE : var_in_env (Identset.union (fv_atom a) (fv_plist pl)) ce e e0 sp)
   (BD: bind_vars xl ce (roots_term p) nil = Some (l0, c))
   (SH: sp_height_coherence ce )
   (SN: sp_norepet ce )
   (GCC: comp_triggers_gc (Fmatch a pl) = true ->
      gc_cond (roots_term (Fmatch a pl)) ce ),
     (forall (id : positive) (v : location),
          (cenv_map ce) ! id = Some v -> (cenv_map c) ! id = Some v)/\
   (exists em, exists spm ,
    set_local_pat l0 cva e0 sp = Some (em,spm) /\
   sp_height_coherence c /\
   sp_norepet c /\ (
  (comp_triggers_gc p) = true ->
      gc_cond (roots_term p) c) /\
   var_in_env (fv_term p) c e1 em spm /\
  ( comp_triggers_gc p=false -> no_gc_concl ce e0 em) /\
   stack_concl ce sp spm /\ list_norepet l0/\lim c) /\ varpl_test_prop l0.

IX. Simulation scheme
Lemma atom_correct:
 forall fe f fv, feval_atom fe f fv ->
 forall ce e sp c
 (G: germ_atom f ce = Some c)
 (VIE: var_in_env (fv_atom f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SNR: sp_norepet ce) ,
 exists cv, ceval_atom e sp c cv/\match_val fv cv.



Lemma atlist_correct:
 forall fe f fv, feval_atlist fe f fv ->
 forall ce e sp c
 (G: germ_atomlist f ce = Some c)
 (VIE: var_in_env (fv_atomlist f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SNR: sp_norepet ce) ,
 exists cv, ceval_atlist e sp c cv/\match_vallist fv cv.

Lemma germ_atom_length:
 forall l ce t, germ_atomlist l ce = Some t ->
                     length l = length t.

Lemma vie_closure:
forall r ce e e0 sp,
  gc_cond r ce -> var_in_env r ce e e0 sp ->
  var_in_env r ce e (@PTree.empty cval) sp.

Lemma fset_correct1:
 forall xl vargs fi fe (LN: list_norepet xl)
  (NG: forall id, In id xl -> PTree.get id fi = None)
  (SEt: set_local_par xl vargs fi = Some fe),
  (forall id v, ~In id xl -> PTree.get id fi = Some v -> PTree.get id fe = Some v).


Lemma fset_correct:
forall xl vargs fi fe (LN: list_norepet xl)
  (NG: forall id, In id xl -> PTree.get id fi = None)
  (SEt: set_local_par xl vargs fi = Some fe),
 (forall (n0 : nat) (id : positive),
  nth_error xl n0 = Some id ->
  exists v0 : fval, fe ! id = Some v0 /\ nth_error vargs n0 = Some v0).


Lemma cset_correct1:
 forall xl vargs fi fe (LN: list_norepet xl)
  (NG: forall id, In id xl -> PTree.get id fi = None)
  (SEt: set_loc_par xl vargs fi = Some fe),
  (forall id v, ~In id xl -> PTree.get id fi = Some v -> PTree.get id fe = Some v).

Lemma cset_correct:
forall xl vargs fi fe (LN: list_norepet xl)
  (NG: forall id, In id xl -> PTree.get id fi = None)
  (SEt: set_loc_par xl vargs fi = Some fe),
 (forall (n0 : nat) (id : positive),
  nth_error xl n0 = Some id ->
  exists v0 : cval, fe ! id = Some v0 /\ nth_error vargs n0 = Some v0).


Lemma set_loc_par_cor:
forall vargs cva ,
  match_vallist vargs cva ->
forall l e e1 c (LN: list_norepet l)
  (NG: forall id, In id l -> PTree.get id e = None)
  (NGC:forall id, In id l -> PTree.get id c = None) ,
  (forall id v, PTree.get id e = Some v ->
                     exists cv, PTree.get id c = Some cv /\ match_val v cv )->
  set_local_par l vargs e = Some e1 ->
  exists ce1 ,
   set_loc_par l cva c = Some ce1 /\
    (forall id v, PTree.get id e1 = Some v ->
                     exists cv, PTree.get id ce1 = Some cv /\ match_val v cv)/\
   (forall (n0 : nat) (id : positive),
    nth_error l n0 = Some id ->
    exists v0 : fval, e1 ! id = Some v0 /\ nth_error vargs n0 = Some v0) /\
    ( forall id : positive,
  In id l ->
  exists v0 : fval,
    exists v' : cval,
      e1 ! id = Some v0 /\ ce1 ! id = Some v' /\ match_val v0 v').



Lemma vie_spec :
 forall e ce,
     (forall id v, PTree.get id e = Some v ->
                     exists cv, PTree.get id ce = Some cv /\ match_val v cv )->
   forall r, var_in_env r empty_cenv e ce sp_empty.

Lemma set_local_inv:
  forall l vl e e1, set_local_par l vl e = Some e1 ->
  length vl = length l.

Fixpoint store_list (l : list (nat*ident))
   (sp:spenv) (e:env) {struct l}:=
 match l with
 | nil => Some sp
 | (n,id)::m =>
       do v<- PTree.get id e ;
       store_list m (sp_set n v sp) e
 end.

Lemma binds_par_inv :
 forall xl ce roots c c1 ce1
    ( LIM:lim ce)
    ( LNc: list_norepet c) ( LNp: list_norepet xl)
    ( NG: forall id, In id xl -> PTree.get id (cenv_map ce) = None)
    ( IN: forall n id, In (n,id) c ->
          ( (Identset.mem id roots =true)/\
           lt n (cenv_height ce) /\
           PTree.get id (cenv_map ce) = Some (Loc_slot n))),
    bind_pars xl ce roots c = Some (c1,ce1) ->
   exists c2, c1 = c++c2 /\
                    (forall n id, In (n,id) c1 ->
                                      ( (Identset.mem id roots =true) /\
                                         ((In (n,id) c) \/In id xl) /\
                                         lt n (cenv_height ce1) /\
                                         PTree.get id (cenv_map ce1) =
                                         Some (Loc_slot n ))) /\
                    list_norepet c1 /\
                    (forall id info , PTree.get id (cenv_map ce) = Some info ->
                                             PTree.get id (cenv_map ce1) = Some info) /\
                    lim ce1 /\
                    (forall id, In id xl -> (Identset.mem id roots =false) ->
                                     PTree.get id (cenv_map ce1) = Some Loc_var) .










Lemma Cpush_list_eval:
 forall l e1 sp1 c sp2 e2 sp3 v
 (ID: forall x id, In (x,id) l -> var_test_prop id) ,
 store_list l sp1 e1 = Some sp2 ->
 ceval_term sc e1 sp2 c e2 sp3 v->
 ceval_term sc e1 sp1 (Cpush_list l c) e2 sp3 v.


Lemma bind_context:
 forall v cv id f ce fe e sp r info ce1 b
 (LIM:lim ce) (VT: var_test_prop id)
 (MV: match_val v cv)
 (GETF: PTree.get id fe = Some v)
 (GETE: PTree.get id e = Some cv)
 (VIE: var_in_env (Identset.remove id f) ce fe e sp)
 (BD: bind_var id ce r = Some (info,ce1))
 (SN: sp_norepet ce) (SH: sp_height_coherence ce)
 (GC: b = true -> gc_cond r ce) ,
 ( lim ce1 /\
       (if Identset.mem id r
        then
         info = SL (cenv_height ce) /\
         ce1 =
         mkCenv (PTree.set id (Loc_slot (cenv_height ce)) (cenv_map ce))
           (cenv_height ce + 1)
        else
         info = VR id /\
         ce1 = mkCenv (PTree.set id Loc_var (cenv_map ce)) (cenv_height ce)) /\
       (cenv_map ce) ! id = None) /\
 (exists sp1,
    var_in_env f ce1 fe e sp1 /\ sp_norepet ce1 /\
    sp_height_coherence ce1 /\
   (b=true -> gc_cond r ce1) /\
   (if Identset.mem id r
        then sp1 = (sp_set (cenv_height ce) cv sp)
         else sp1 =sp))/\ varp_test_prop info.





Lemma binds_context:
 forall vargs cvl, match_vallist vargs cvl ->
  forall xl ce r f c c1 ce1 fe e sp b
  (VT: varl_test_prop xl)
  (ID:( forall x id, In (x,id) c -> var_test_prop id))
 (LEN: length xl = length vargs)
 (LIM : lim ce ) ( LNc: list_norepet c) ( LNp: list_norepet xl)
    ( NG: forall id, In id xl -> PTree.get id (cenv_map ce) = None)
    ( IN: forall n id, In (n,id) c ->
          ( (Identset.mem id r =true)/\
           lt n (cenv_height ce) /\
           PTree.get id (cenv_map ce) = Some (Loc_slot n)))
 (BD: bind_pars xl ce r c = Some (c1,ce1) )
 (NTH: forall n id , nth_error xl n = Some id ->
            exists v, PTree.get id fe = Some v /\
                           nth_error vargs n = Some v)
 (LOC: forall id , In id xl->
                     exists v, exists v' ,
                       PTree.get id fe = Some v/\
                       PTree.get id e = Some v' /\
                       match_val v v')
 (GC: b=true -> gc_cond r ce)
 (VIE : var_in_env (List.fold_right Identset.remove f xl ) ce fe e sp )
 (SH: sp_height_coherence ce) (SN: sp_norepet ce),
 exists l4, exists sp1,
     c1 = c ++ l4 /\
     store_list l4 sp e = Some sp1 /\
   sp_height_coherence ce1 /\
   sp_norepet ce1 /\ (b=true -> gc_cond r ce1) /\
   var_in_env f ce1 fe e sp1 /\
   stack_concl ce sp sp1/\
   lim ce1/\ ( forall x id, In (x,id) c1 -> var_test_prop id).











Lemma gen_patlist_length:
forall pl ce l,
germ_patlist pl ce = Some l -> length l = length pl.

Theorem germ_correct :
 forall (fe:fenv) (f:Fterm) (fv:fval), feval_term s fe f fv ->
forall ce e sp c
 (LIM : lim ce )
 (G: germ f ce = Some c)
 (VIE: var_in_env (fv_term f) ce fe e sp)
 (SH: sp_height_coherence ce)
 (SNR: sp_norepet ce)
 (GCC : comp_triggers_gc f = true ->gc_cond (roots_term f) ce),
 exists cv, exists e1, exists sp1,
   ceval_term sc e sp c e1 sp1 cv/\
   match_val fv cv/\
   stack_concl ce sp sp1 /\
   ( comp_triggers_gc f = false -> no_gc_concl ce e e1).
























End COR.
X. Semantics preservation of the conversion of a program to Fminor
Lemma match_glo:
    forall s sc ,
   germ_cfunctions s = Some sc ->
    (forall id d ,recup_funct id s=Some d ->
    exists cd, recup_cfunct id sc=Some cd /\
                     germ_cfunction d = Some cd) /\
    ((map (fst (A:=ident) (B:=funct))) s ) = ((map (fst (A:=ident) (B:=cfunction))) sc) .


Theorem Fminor_correct:
 forall p cp v
   (TR: germ_cprogram p = Some cp)
   (E : eval_prog p v) ,
  exists v' , ceval_prog cp v' /\
                   match_val (fprog_def p) (cprog_funct cp) v v'.