Library M2Fminor_proof
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'.