source: src/joint/lineariseProof.ma @ 2481

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "joint/linearise.ma".
include "common/StatusSimulation.ma".   
include "joint/Traces.ma".
include "joint/semanticsUtils.ma".

definition graph_prog_params ≝
λp,p',prog,stack_sizes.
mk_prog_params (make_sem_graph_params p p') prog stack_sizes.

definition graph_abstract_status:
 ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    ∀prog : joint_program (mk_graph_params p).
  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
     abstract_status
 ≝
 λp,p',prog,stack_sizes.
 joint_abstract_status (graph_prog_params ? p' prog stack_sizes).

definition lin_prog_params ≝
λp,p',prog,stack_sizes.
mk_prog_params (make_sem_lin_params p p') prog stack_sizes.

definition lin_abstract_status:
 ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    ∀prog : joint_program (mk_lin_params p).
  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
     abstract_status
 ≝
 λp,p',prog,stack_sizes.
 joint_abstract_status (lin_prog_params ? p' prog stack_sizes).

(*
axiom P :
  ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop.

check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x)
(* 
unification hint 0 ≔ p, prog, stack_sizes ;
pars ≟ mk_prog_params p prog stack_sizes ,
pars' ≟ make_global pars,
A ≟ λvars.joint_closed_internal_function p vars,
B ≟ ℕ
⊢
A (prog_var_names (λvars.fundef (A vars)) B prog) ≡
joint_closed_internal_function pars' (globals pars').
*)
axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop.
(*axiom Q : ∀A,B,init,prog.
 T … (globalenv (λvars:list ident.fundef (A vars)) B
  init prog) → Prop.

lemma pippo :
  ∀p,p',prog,stack_sizes.
  let pars ≝ graph_prog_params p p' prog stack_sizes in
  let ge ≝ ev_genv pars in T ?? prog ge → Prop.
  
  #H1 #H2 #H3 #H4
   #H5
  whd in match (ev_genv ?) in H5;               
  whd in match (globalenv_noinit) in H5; normalize nodelta in H5;
  whd in match (prog ?) in H5;
  whd in match (joint_function ?) in H5;
  @(Q … H5)
 λx:T ??? ge.Q ???? x)
*)
axiom Q : ∀A,B,init,prog,i.
is_internal_function
 (A
  (prog_var_names (λvars:list ident.fundef (A vars)) B
   prog))
 (globalenv (λvars:list ident.fundef (A vars)) B
  init prog)
 i → Prop.

check
  (λp,p',prog,stack_sizes,i.
  let pars ≝ graph_prog_params p p' prog stack_sizes in
  let ge ≝ ev_genv pars in
 λx:is_internal_function (joint_closed_internal_function pars (globals pars))
  ge i.Q ??? prog ? x)
*)

definition sigma_pc_opt:
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ) →
   program_counter → option program_counter
 ≝
  λp,p',prog,sigma,pc.
  let pars ≝ make_sem_graph_params p p' in
  let ge ≝ globalenv_noinit … prog in
  ! f ← int_funct_of_block ? ge (pc_block pc) ;
  ! lin_point ← sigma f (point_of_pc ? pars pc) ;
  return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.

definition well_formed_pc:
 ∀p,p',graph_prog.
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    label → option ℕ) →
   program_counter → Prop
 ≝
 λp,p',prog,sigma,pc.
  sigma_pc_opt p p' prog sigma pc
   ≠ None ….

definition well_formed_status:
 ∀p,p',graph_prog.
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    label → option ℕ) →
  state_pc (make_sem_graph_params p p') → Prop ≝
 λp,p',prog,sigma,st.
 well_formed_pc p p' prog sigma (pc … st) ∧ ?.
cases daemon (* TODO *)
qed.

(* 
lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
[ #p #s #st #prf
  whd in match sigma_pc_of_status; normalize nodelta
  @opt_safe_elim
  #n
  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
        (ev_genv p) (pblock (pc p st))))
  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
  [ #_ #ABS normalize in ABS; destruct(ABS) ]
  #f #EQ >m_return_bind
*)


(*
lemma wf_status_to_wf_pc : 
∀p,p',graph_prog,stack_sizes.
∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ).
∀st.
well_formed_status p p' graph_prog stack_sizes sigma st →
well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
qed.
 *)
 definition sigma_pc :
∀p,p',graph_prog.
∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
    label → option ℕ).
∀pc.
∀prf : well_formed_pc p p' graph_prog sigma pc.
program_counter ≝ 
λp,p',graph_prog,sigma,st.opt_safe ….
 
lemma sigma_pc_of_status_ok:
  ∀p,p',graph_prog.
  ∀sigma.
   ∀pc.
    ∀prf:well_formed_pc p p' graph_prog sigma pc.
    sigma_pc_opt p p' graph_prog sigma pc =
    Some … (sigma_pc p p' graph_prog sigma pc prf).
    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.

definition sigma_state :
 ∀p.
 ∀p':∀F.sem_unserialized_params p F.
 ∀graph_prog.
  ∀sigma.
(*   let lin_prog ≝ linearise ? graph_prog in *)
    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     well_formed_status p p' graph_prog sigma s →
      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
≝
 λp,p',graph_prog,sigma,s,prf.
 let pc' ≝ sigma_pc … (proj1 … prf) in
 mk_state_pc ? ? pc'.
 cases daemon (* TODO *) qed.

lemma sigma_pc_commute:
 ∀p,p',graph_prog,sigma,st.
 ∀prf : well_formed_status p p' graph_prog sigma st.
 sigma_pc … (pc ? st) (proj1 … prf) =
 pc ? (sigma_state … st prf).
#p #p' #prog #sigma #st #prf %
qed.

lemma res_eq_from_opt :
  ∀A,m,v.res_to_opt A m = return v → m = return v. 
#A * #x #v normalize #EQ destruct % qed.

definition sigma_function_name :
 ∀p,graph_prog.
 let lin_prog ≝ linearise p graph_prog in
  (Σf.is_internal_function_of_program … graph_prog f) →
  (Σf.is_internal_function_of_program … lin_prog f) ≝
λp,graph_prog,f.«f, if_propagate … (pi2 … f)».

lemma if_of_function_commute:
 ∀p.
 ∀graph_prog : joint_program (mk_graph_params p).
 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
 let graph_fd ≝ if_of_function … graph_fun in
 let lin_fun ≝ sigma_function_name … graph_fun in
 let lin_fd ≝ if_of_function … lin_fun in
 lin_fd = \fst (linearise_int_fun ?? graph_fd).
 #p #graph_prog #graph_fun whd
 @prog_if_of_function_transform % qed.

lemma bind_opt_inversion:
  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
  (! x ← f ; g x = Some … y) →
  ∃x. (f = Some … x) ∧ (g x = Some … y).
#A #B #f #g #y cases f normalize 
[ #H destruct (H)
| #a #e %{a} /2 by conj/
] qed.

lemma sigma_pblock_eq_lemma : 
∀p,p',graph_prog.
let lin_prog ≝ linearise p graph_prog in
∀sigma,pc.
∀prf : well_formed_pc p p' graph_prog sigma pc.
 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
 pc_block pc.
 #p #p' #graph_prog #sigma #pc #prf
 whd in match sigma_pc; normalize nodelta
 @opt_safe_elim #x #x_spec
 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
qed.

(*
lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
(! x ← m ; g x) ≠ None ? → m ≠ None ?.
#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize  
[ #abs elim abs -abs #abs @abs %
| #abs elim abs -abs #abs #v @abs %
]
qed.

lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. 
∀ b : B .∀ f : A → B. ∀g : B → option C.
g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
#A #B #C #m #x #b  #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption
qed.
*)

lemma funct_of_block_transf :
∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
funct_of_block … (globalenv_noinit … progr) bl = return f →
funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
#A #B #progr #transf #bl #f #prf whd
whd in match funct_of_block in ⊢ (%→?); normalize nodelta
cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
  ∀o.∀prf : Q o.
  ∀f1,f2.
  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) 
  [ #A #B #Q #P * /2/ ] #aux
@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
#fd #EQfind whd in ⊢ (??%%→?);
generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
whd in match funct_of_block; normalize nodelta
@aux [ # fd' ]
[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
#prf' cases daemon qed.

lemma description_of_function_transf :
∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
∀transf : ∀vars. A vars → B vars.
let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
∀f_out,prf.
description_of_function …
  (globalenv_noinit … progr') f_out =
transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
  «pi1 … f_out, prf»).
#A #B #progr #transf #f_out #prf
whd in match description_of_function in ⊢ (???%);
normalize nodelta
cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
  ∀o.∀prf : Q o.
  ∀f1,f2.
  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) 
  [ #A #B #Q #P * /2/ ] #aux
@aux
[ #fd' ] * #fd #EQ destruct (EQ)
inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
#bl #EQfind >m_return_bind #EQfindf
whd in match description_of_function; normalize nodelta
@aux
[ #fdo' ] * #fdo #EQ destruct (EQ)
>find_symbol_transf >EQfind >m_return_bind
>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
qed.


lemma match_int_fun :
∀A,B : Type[0].∀P : B → Prop.
∀Q : fundef A → Prop.
∀m : fundef A.
∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
∀f2 : ∀fd.Q (External … fd) → B.
∀prf : Q m.
(∀fd,prf.P (f1 fd prf)) → 
(∀fd,prf.P (f2 fd prf)) → 
P (match m
return λx.Q x → ?
with
[ Internal fd ⇒ f1 fd
| External fd ⇒ f2 fd
] prf).
#A #B #P #Q * // qed.
(*)
 lemma match_int_fun :
∀A,B : Type[0].∀P : B → Prop.
∀m : fundef A.
∀f1 : ∀fd.m = Internal … fd → B.
∀f2 : ∀fd.m = External … fd → B.
(∀fd,prf.P (f1 fd prf)) → 
(∀fd,prf.P (f2 fd prf)) → 
P (match m
return λx.m = x → ?
with
[ Internal fd ⇒ f1 fd
| External fd ⇒ f2 fd
] (refl …)).
#A #B #P * // qed. 
*)
(*
lemma prova :
∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
∀ f,g,prf1.
match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
External fn ⇒ λprf.None ? ] (refl ? M) = return f →  
∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
#H1 #H2 #H3 #H4 #H5 #H6
@match_int_fun
#fd #EQ #EQ' whd in EQ' : (??%%); destruct
%[|%[| % ]] qed.
*)

lemma int_funct_of_block_transf_commute:
 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
#A #B #progr #transf #bl #f #prf
whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta 
#H
elim (bind_opt_inversion ??? ?? H) -H #x
* #x_spec
@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
whd in match int_funct_of_block; normalize nodelta
>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
>m_return_bind
@match_int_fun #fd' #prf' [ % ]
@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
>(description_of_function_transf) [2: @x_prf ]
>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.


lemma fetch_function_sigma_commute :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀sigma,pc_st,f.
  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
 fetch_function … (globalenv_noinit … graph_prog) pc_st = 
  return f
→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
  return sigma_function_name … f.
 #p #p' #graph_prog #sigma #st #f #prf
 whd in match fetch_function; normalize nodelta
 >(sigma_pblock_eq_lemma … prf) #H
 lapply (opt_eq_from_res ???? H) -H #H
 >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
 //
qed.
 
(*
#H elim (bind_opt_inversion ????? H) -H
#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
@match_opt_prf_elim
 #H #H1  whd in H : (??%?); 
cases (   find_funct_ptr
   (fundef
    (joint_closed_internal_function
     (graph_prog_params p p' graph_prog
      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
       (linearise_int_fun p) graph_prog stack_sizes))
     (globals
      (graph_prog_params p p' graph_prog
       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
        (linearise_int_fun p) graph_prog stack_sizes)))))
   (ev_genv
    (graph_prog_params p p' graph_prog
     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
      (linearise_int_fun p) graph_prog stack_sizes)))
   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
 

normalize nodelta
#H #H1
cases (   find_funct_ptr
   (fundef
    (joint_closed_internal_function
     (graph_prog_params p p' graph_prog
      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
       (linearise_int_fun p) graph_prog stack_sizes))
     (globals
      (graph_prog_params p p' graph_prog
       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
        (linearise_int_fun p) graph_prog stack_sizes)))))
   (ev_genv
    (graph_prog_params p p' graph_prog
     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
      (linearise_int_fun p) graph_prog stack_sizes)))
   (pblock (pc (make_sem_graph_params p p') st))) in H;


check find_funct_ptr_transf
whd in match int_funct_of_block; normalize nodelta
#H elim (bind_inversion ????? H)

.. sigma_int_funct_of_block



whd in match int_funct_of_block; normalize nodelta
elim (bind_inversion ????? H)
whd in match int_funct_of_block; normalize nodelta
#H elim (bind_inversion ????? H) -H #fn *
#H lapply (opt_eq_from_res ???? H) -H
#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
destruct //
cases daemon
qed. *)

lemma stmt_at_sigma_commute:
 ∀p,graph_prog,graph_fun,lbl,pt.
 let lin_prog ≝ linearise ? graph_prog in
 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
 ∀sigma.good_sigma p graph_prog sigma →
 sigma graph_fun lbl = return pt →
 ∀stmt.
   stmt_at …
    (joint_if_code ?? (if_of_function ?? graph_fun))  
    lbl = return stmt →
   stmt_at ??
    (joint_if_code ?? (if_of_function ?? lin_fun))
    pt = return (graph_to_lin_statement … stmt).  
 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf
 (*
 whd in match (stmt_at ????);
 whd in match (stmt_at ????);
 cases (linearise_code_spec … p' graph_prog graph_fun
         (joint_if_entry … graph_fun))
 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
 lapply (sigma_spec
         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
 <sigma_pc_commute >lin_lookup_ok // *)
 cases daemon
qed.

lemma fetch_statement_sigma_commute:
  ∀p,p',graph_prog,pc,fn,stmt.
  let lin_prog ≝ linearise ? graph_prog in
  ∀sigma.good_sigma p graph_prog sigma →
  ∀prf : well_formed_pc p p' graph_prog sigma pc.
  fetch_statement ? (make_sem_graph_params p p') …
    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
  fetch_statement ? (make_sem_lin_params p p') …
    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf 
 whd in match fetch_statement; normalize nodelta #H
 cases (bind_inversion ????? H) #id * -H #fetchfn
 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
 #H cases (bind_inversion ????? H) #fstmt * -H #H
 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
 >(stmt_at_sigma_commute … good … H) [%]
 whd in match sigma_pc; normalize nodelta
 @opt_safe_elim #pc' #H
 cases (bind_opt_inversion ????? H)
 #i * #EQ1 -H #H
 cases (bind_opt_inversion ????? H)
 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
qed.

definition linearise_status_rel:
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
 let stack_sizes' ≝
  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    ? graph_prog stack_sizes in
 ∀sigma.
 good_sigma p graph_prog sigma →
   status_rel
    (graph_abstract_status p p' graph_prog stack_sizes')
    (lin_abstract_status p p' lin_prog stack_sizes)
 ≝ λp,p',graph_prog,stack_sizes,sigma,good.
   mk_status_rel …
    (* sem_rel ≝ *) (λs1,s2.
     ∃prf: well_formed_status p p' graph_prog sigma s1.
      s2 = sigma_state … s1 prf)
    (* call_rel ≝ *) (λs1,s2.
      ∃prf:well_formed_status p p' graph_prog sigma s1.
      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
    (* sim_final ≝ *) ?.
#st1 #st2 * #prf #EQ2
%
whd in ⊢ (%→%);
#H lapply (opt_to_opt_safe … H)
@opt_safe_elim -H
#res #_
#H lapply (res_eq_from_opt ??? H) -H
#H elim (bind_inversion ????? H)
* #f #stmt *
whd in ⊢ (??%?→?);
cases daemon
qed.

(* To be added to common/Globalenvs, it strenghtens
   find_funct_ptr_transf *)
(*   
lemma
  find_funct_ptr_transf_eq:
    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
    ∀b: block.
    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
     m_map ???
      (transf …)
      (find_funct_ptr ? (globalenv … iV p) b).
 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
 [ cases daemon (* TODO in Globalenvs.ma *)
 | #f #H >(find_funct_ptr_transf A B … H) // ]
qed.
*)


(*lemma fetch_function_sigma_commute:
 ∀p,p',graph_prog,sigma,st1.
 ∀prf:well_formed_status ??? sigma st1.
 let lin_prog ≝ linearise ? graph_prog in
  fetch_function                
   (lin_prog_params p p' lin_prog)
   (globals (lin_prog_params p p' lin_prog))
   (ev_genv (lin_prog_params p p' lin_prog))
   (pc (lin_prog_params p p' lin_prog)
    (linearise_status_fun p p' graph_prog sigma st1 prf))
 =
  m_map …
   (linearise_int_fun ??)
   (fetch_function
    (graph_prog_params p p' graph_prog)
    (globals (graph_prog_params p p' graph_prog))
    (ev_genv (graph_prog_params p p' graph_prog))
    (pc (graph_prog_params p p' graph_prog) st1)).
#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
whd in match function_of_block; normalize nodelta
>(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
cases (find_funct_ptr ???) // * //
qed.
*)

lemma IO_bind_inversion:
  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
  (! x ← f ; g x = return y) →
  ∃x. (f = return x) ∧ (g x = return y).
#O #I #A #B #f #g #y cases f normalize 
[ #o #f #H destruct
| #a #e %{a} /2 by conj/
| #m #H destruct (H)
] qed.

lemma opt_Exists_elim:
 ∀A:Type[0].∀P:A → Prop.
  ∀o:option A.
   opt_Exists A P o →
    ∃v:A. o = Some … v ∧ P v.
 #A #P * normalize /3/ *
qed.
        
inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)

lemma err_eq_from_io : ∀O,I,X,m,v.
  err_to_io O I X m = return v → m = return v.
#O #I #X * #x #v normalize #EQ destruct % qed. 

lemma linearise_ok:
 ∀p,p',graph_prog.
  let lin_prog ≝ linearise ? graph_prog in
 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
 let graph_stack_sizes ≝
  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    ? graph_prog lin_stack_sizes in
   ex_Type1 … (λR.
   status_simulation
    (graph_abstract_status p p' graph_prog graph_stack_sizes)
    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
 #p #p' #graph_prog
 cases (linearise_spec … graph_prog) #sigma #good
 #lin_stack_sizes
 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
 whd whd in ⊢ (%→%→?);
 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
 #st1 
 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
 #st1'
 change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?)
 #st2
 #ex * #wfprf #rel_st1_st2
 whd in ex;
 change with
  (eval_state
    (make_sem_graph_params p p')
    (prog_var_names ?? graph_prog)
     ?
    st1 = ?) in ex;
 whd in match eval_state in ex;
 normalize nodelta in ex;
 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt
 change with (Σi.is_internal_function_of_program … graph_prog i) in fn; *
 change with (globalenv_noinit ? graph_prog) in
  ⊢ (??(???%?)?→?);
    match (ge ?? (ev_genv ?)) in ⊢ (%→?);
 st1'
whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
>fetch_statement_spec in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
whd in fetch_statement_spec : (??()%);
cases cl in classified_st1_cl; -cl #classified_st1_cl whd
[4:
 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
 #sigma_entry_is_zero #sigma_spec
 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
 #related_lin_stm_graph_stm
 
 inversion (stmt_implicit_label ???)
 [ whd in match (opt_All ???); #stmt_implicit_spec #_
   letin st2_opt' ≝ (eval_state …
               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
               (sigma_state … wf_st1))
   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
   normalize nodelta in st2_spec'; -st2_opt'
   %{st2'} %{(taaf_step … (taa_base …) …)}
   [ cases daemon (* TODO, together with the previous one? *)
   | @st2_spec' ]
   %[%] [%]
   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
     >m_return_bind
     (* Case analysis over the possible statements *)
     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
     XXXXXXXXXX siamo qua, caso GOTO e RETURN
   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
   ]
 | ....
qed.