source: src/joint/lineariseProof.ma @ 2774

 (**************************************************************************)
(*       ___                                                              *)
(*      ||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".
include "common/ExtraMonads.ma".
(*
!!!SPOSTATO IN extraGlobalenvs.ma!!!!

include alias "common/PositiveMap.ma".

lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
id < (nextfunction ? ge) → 
lookup_opt … id (functions ? ge) = None ? → 
lookup_opt … id (functions … (add_functs F ge l)) = None ?.
#F #ge #l #id whd in match add_functs; normalize nodelta
elim l -l [ #_ normalize //]
* #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
>lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
#f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
| cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
[elim tl [normalize //]
#x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
#H2 lapply(transitive_le … H H2) @lt_to_not_eq
qed.

lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
lookup_opt … id (functions ? (\fst gem)) = None ? → 
lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. 
#F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
** #x1 #x2 #x3 #tl whd in match add_globals;
normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
qed.

  
lemma globalenv_no_minus_one :
 ∀F,V,i,p.
  find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?. 
#F #V #i #p
whd in match find_funct_ptr; normalize nodelta
whd in match globalenv; 
whd in match globalenv_allocmem; normalize nodelta
@add_globals_functions_miss @add_functs_functions_miss normalize //
qed.
*) 

(* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!

lemma fetch_internal_function_no_minus_one :
  ∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
 whd in match fetch_internal_function;
  whd in match fetch_function; normalize nodelta
  >globalenv_no_minus_one
  cases (symbol_for_block ???) normalize //
qed.

*)

(*spostato in ExtraMonads.ma

lemma bind_option_inversion_star:
  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
  (∀x.f = Some … x → g x = Some … y → P) →
  (! x ← f ; g x = Some … y) → P.
#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.

interpretation "option bind inversion" 'bind_inversion =
  (bind_option_inversion_star ???????).

lemma bind_inversion_star : ∀X,Y.∀P : Prop.
∀m : res X.∀f : X → res Y.∀v : Y.
(∀x. m = return x → f x = return v → P) →
! x ← m ; f x = return v → P.
#X #Y #P #m #f #v #H #G
elim (bind_inversion ????? G) #x * @H qed.

interpretation "res bind inversion" 'bind_inversion =
  (bind_inversion_star ???????).

lemma IO_bind_inversion:
  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
  (∀x.f = return x → g x = return y → P) →
  (! x ← f ; g x = return y) → P.
#O #I #A #B #P #f #g #y cases f normalize 
[ #o #f #_ #H destruct
| #a #G #H @(G ? (refl …) H)
| #e #_ #H destruct
] qed.

interpretation "IO bind inversion" 'bind_inversion =
  (IO_bind_inversion ?????????).

record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
  { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
  ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
  ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
      m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
                  m_frel ?? Q G (m_bind … m f) (m_bind … n g)
  ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
  }.

*)

(*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
  λO,I.mk_MonadFunctRel ??
  (λX,Y,F,m,n.∀x.m = return x → n = return F x)
  ???.
[ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) %
| #X #Y #Z #W #F #G *
  [ #o #f | #u | #e ] #n #H #f #g #K #x
  whd in ⊢ (??%%→?); #EQ destruct(EQ)
  >(H ? (refl …)) @K @EQ
| #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H %
]
qed.*)

(* spostato in ExtraMonads.ma
definition res_preserve : MonadFunctRel Res Res ≝
  mk_MonadFunctRel ??
  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
  ???.
[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
| #X #Y #Z #W #P #Q #F #G *
  [ #u | #e ] #n #H #f #g #K #x
  whd in ⊢ (??%%→?); #EQ destruct(EQ)
  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
| #X #Y #P #F #G #H #u #v #K #x #EQ
  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
]
qed.

definition opt_preserve : MonadFunctRel Option Option ≝
  mk_MonadFunctRel ??
  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
  ???.
[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
| #X #Y #Z #W #P #Q #F #G *
  [ | #u ] #n #H #f #g #K #x
  whd in ⊢ (??%%→?); #EQ destruct(EQ)
  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
| #X #Y #P #F #G #H #u #v #K #x #EQ
  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
]
qed.

definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
  λO,I.mk_MonadFunctRel ??
  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
  ???.
[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
| #X #Y #Z #W #P #Q #F #G *
  [ #o #f | #u | #e ] #n #H #f #g #K #x
  whd in ⊢ (??%%→?); #EQ destruct(EQ)
  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
| #X #Y #P #F #G #H #u #v #K #x #EQ
  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
]
qed.

definition preserving ≝
  λM1,M2.λFR : MonadFunctRel M1 M2.
  λX,Y,A,B : Type[0].
  λP : X → Prop.
  λQ : A → Prop.
  λF : ∀x : X.P x → Y.
  λG : ∀a : A.Q a → B.
  λf : X → M1 A.
  λg : Y → M2 B.
  ∀x,prf.
  FR … G
    (f x) (g (F x prf)).

definition preserving2 ≝
  λM1,M2.λFR : MonadFunctRel M1 M2.
  λX,Y,Z,W,A,B : Type[0].
  λP : X → Prop.
  λQ : Y → Prop.
  λR : A → Prop.
  λF : ∀x : X.P x → Z.
  λG : ∀y : Y.Q y → W.
  λH : ∀a : A.R a → B.
  λf : X → Y → M1 A.
  λg : Z → W → M2 B.
  ∀x,y,prf1,prf2.
  FR … H
    (f x y) (g (F x prf1) (G y prf2)).
*)

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).
  (ident → option ℕ) → 
     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).
  (ident → option ℕ) → 
     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_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → 
    label → option ℕ.

definition sigma_pc_opt:
 ∀p,p'.∀graph_prog.
  sigma_map p graph_prog →
   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
  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
    return pc
  else 
    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
    ! lin_point ← sigma fd (point_of_pc pars pc) ;
    return pc_of_point 
    (make_sem_lin_params ? p') (pc_block pc) lin_point.

definition well_formed_pc:
 ∀p,p',graph_prog.
  sigma_map p graph_prog →
   program_counter → Prop
 ≝
 λp,p',prog,sigma,pc.
  sigma_pc_opt p p' prog sigma pc
   ≠ None ….

definition sigma_beval_opt :
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  sigma_map p graph_prog →
  beval → option beval ≝
λp,p',graph_prog,sigma,bv.
match bv with
[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
| _ ⇒ return bv
].

definition sigma_beval :
 ∀p,p',graph_prog,sigma,bv.
 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
 λp,p',graph_prog,sigma,bv.opt_safe ….

definition sigma_is_opt :
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  sigma_map p graph_prog →
  internal_stack → option internal_stack ≝
λp,p',graph_prog,sigma,is.
match is with
[ empty_is ⇒ return empty_is
| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
| both_is bv1 bv2 ⇒
  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
  return both_is bv1' bv2'
].

definition sigma_is :
 ∀p,p',graph_prog,sigma,is.
 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
 λp,p',graph_prog,sigma,is.opt_safe ….
 
lemma sigma_is_empty : ∀p,p',graph_prog,sigma.
  ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is.
#p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta
@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.

(* spostato in ExtraMonads.ma

lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.

lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
∀X,Y,P,F,v,n.
∀prf.n = return F v prf →
FR X Y P F (return v) n.
#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.

lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
*)

lemma sigma_is_pop_commute :
 ∀p,p',graph_prog,sigma,is.
 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
 res_preserve …
  (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧
       sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?)
  (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)
  (is_pop is) (is_pop (sigma_is … prf)).
#p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf
[ @res_preserve_error
|*:
 whd in match sigma_is in ⊢ (?????????%); normalize nodelta
 @opt_safe_elim #is'
  #H @('bind_inversion H) -H #bv1' #EQ1
  [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
 whd in ⊢ (??%%→?); #EQ destruct(EQ)
 @mfr_return_eq
 [1,3: @hide_prf %%
 |*: whd in match sigma_beval; whd in match sigma_is;
  normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''
 ]
 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]
  whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
 [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') %
]
qed.

(* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
  opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v).
#X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ
lapply (H … EQ) cases v [ * ] #y #K @K qed.

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 res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
  res_preserve P u v → IO_preserve O I P u v.
#X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ
lapply (H … EQ) cases v [2: #e * ] #y #K @K qed.

lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
  res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v.
#X #Y #P #e #u #v #H #x #EQ
lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ]
#y #K @K qed.

lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
  IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v.
#X #Y #P #O #I #u #v #H #x #EQ
lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ]
#y #K @K qed. *)

definition well_formed_mem :
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  sigma_map p graph_prog →
 bemem → Prop ≝
λp,p',graph_prog,sigma,m.
∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
  sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. 

definition sigma_mem :
 ∀p,p',graph_prog,sigma,m.
 well_formed_mem p p' graph_prog sigma m →
 bemem ≝
 λp,p',graph_prog,sigma,m,prf.
 mk_mem
  (λb.
    If Zltb (block_id b) (nextblock m) then with prf' do    
      let l ≝ low_bound m b in
      let h ≝ high_bound m b in
      mk_block_contents l h
      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
        sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ?
      else BVundef)
    else empty_block OZ OZ)
  (nextblock m)
  (nextblock_pos m).
@hide_prf
lapply prf'' lapply prf' -prf' -prf''
@Zltb_elim_Type0 [2: #_ * ]
#bid_ok *
@Zleb_elim_Type0 [2: #_ * ]
@Zltb_elim_Type0 [2: #_ #_ * ]
#zh #zl * @(prf … bid_ok zl zh)
qed.

lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.

axiom mem_ext_eq :
  ∀m1,m2 : mem.
  (∀b.let bc1 ≝ blocks m1 b in
      let bc2 ≝ blocks m2 b in
      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
      ∀z.contents bc1 z = contents bc2 z) →
  nextblock m1 = nextblock m2 → m1 = m2.
(* spostato in ExtraMonads.ma

lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
*)

lemma beloadv_sigma_commute:
∀p,p',graph_prog,sigma,ptr.
preserving … opt_preserve …
 (sigma_mem p p' graph_prog sigma)
 (sigma_beval p p' graph_prog sigma)
 (λm.beloadv m ptr)
 (λm.beloadv m ptr).
#p #p' #graph_prog  #sigma #ptr #m #prf #bv
whd in match beloadv;
whd in match do_if_in_bounds;
whd in match sigma_mem;
normalize nodelta
@If_elim #block_ok >block_ok normalize nodelta
[2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
@If_elim #H
[ elim (andb_true … H)
  #H1 #H2
  whd in match sigma_beval; normalize nodelta
  @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
  whd in ⊢ (???%→?); #EQ' destruct
  >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
| elim (andb_false … H) -H #H >H
  [2: >commutative_andb ] normalize nodelta
  whd in ⊢ (???%→?); #ABS destruct(ABS)
]
qed.

include alias "common/GenMem.ma".

lemma bestorev_sigma_commute :
∀p,p',graph_prog,sigma,ptr.
preserving2 ?? opt_preserve …
  (sigma_mem p p' graph_prog sigma)
  (sigma_beval p p' graph_prog sigma)
  (sigma_mem p p' graph_prog sigma)
  (λm.bestorev m ptr)
  (λm.bestorev m ptr).
#p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m'
whd in match bestorev;
whd in match do_if_in_bounds; 
whd in match sigma_mem;
whd in match update_block;
 normalize nodelta
@If_elim #block_ok >block_ok normalize nodelta
[2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
@Zleb_elim_Type0 #H1
[ @Zltb_elim_Type0 #H2 ]
[2,3: #ABS normalize in ABS; destruct(ABS) ]
normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)
%
[2: whd in ⊢ (???%);
  @eq_f
  @mem_ext_eq [2: % ]
  #b @if_elim
  [2: #B
    @If_elim #prf1 @If_elim #prf2
    [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
    whd in match low_bound; whd in match high_bound;
    normalize nodelta
    cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
    [ % #ABS >ABS in B; * ]
    -B #B % [ >B %% ] #z
    @If_elim #prf3  
    @If_elim #prf4
    [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
    whd in match sigma_beval in ⊢ (??%%); normalize nodelta
    @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
    >EQ2 #EQ destruct(EQ) %
  | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]
    #EQ destruct(EQ)
    @If_elim whd in match low_bound; whd in match high_bound;
    normalize nodelta
    [2: >block_ok * #ABS elim (ABS I) ]
    #prf3 % [ >B %% ]
    #z whd in match update; normalize nodelta
    @eqZb_elim normalize nodelta #prf4 
    [2: @If_elim #prf5 @If_elim #prf6
      [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
      normalize nodelta >(eqZb_false … prf4) >EQ2
      #EQ destruct(EQ) %
    | @If_elim #prf5
      [2: >B in prf5; normalize nodelta
        >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
      normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %
    ]
  ]
| whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta
  @eq_block_elim #H normalize nodelta destruct
  #h2 #h3 whd in match update; normalize nodelta
  [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
  @prf1 assumption
]
qed.

record good_sem_state_sigma
  (p : unserialized_params)
  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
  (sigma : sigma_map p graph_prog) : Type[0] ≝
{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
; sigma_empty_frames_commute :
  ∃prf.
  empty_framesT (make_sem_lin_params p p') =
  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf 

; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
; sigma_empty_regsT_commute :
  ∀ptr.∃ prf.
  empty_regsT (make_sem_lin_params p p') ptr =
  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
; sigma_load_sp_commute : 
  preserving … res_preserve …
    (λ_.True)
    …
    sigma_regs
    (λx.λ_.x)
    (load_sp (make_sem_graph_params p p'))
    (load_sp (make_sem_lin_params p p'))
; sigma_save_sp_commute :
  ∀reg,ptr,prf1. ∃prf2.
  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr = 
  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
}.

definition well_formed_state : 
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
 ∀sigma.
 good_sem_state_sigma p p' graph_prog sigma →
 state (make_sem_graph_params p p') → Prop ≝
λp,p',graph_prog,sigma,gsss,st.
well_formed_frames … gsss (st_frms … st) ∧
sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
well_formed_regs … gsss (regs … st) ∧
well_formed_mem p p' graph_prog sigma (m … st).

definition sigma_state : 
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
 ∀sigma.
 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
 ∀st : state (make_sem_graph_params p p').
 well_formed_state … gsss st →
 state (make_sem_lin_params p p') ≝
λp,p',graph_prog,sigma,gsss,st,prf.
mk_state …
  (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?)
  (sigma_is p p' graph_prog sigma (istack … st) ?)
  (carry … st)
  (sigma_regs … gsss (regs … st) ?)
  (sigma_mem p p' graph_prog sigma (m … st) ?).
@hide_prf cases prf ** //
qed.


(*
lemma sigma_is_pop_wf :
 ∀p,p',graph_prog,sigma,is,bv,is'.
 is_pop is = return 〈bv, is'〉 →
 sigma_is_opt p p' graph_prog sigma is ≠ None ? →
 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
 sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
cases daemon 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.
∀pc.
∀prf : well_formed_pc p p' graph_prog sigma pc.
program_counter ≝ 
λp,p',graph_prog,sigma,st.opt_safe ….
 
lemma sigma_pc_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.

lemma sigma_pc_irr :
  ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2.
  pc1 = pc2 →
  sigma_pc p p' graph_prog sigma pc1 prf1 =
  sigma_pc p p' graph_prog sigma pc2 prf2.
#p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2
#EQ destruct(EQ) % qed.

definition well_formed_state_pc :
 ∀p,p',graph_prog,sigma.
  good_sem_state_sigma p p' graph_prog sigma → 
  state_pc (make_sem_graph_params p p') → Prop ≝
 λp,p',prog,sigma,gsss,st.
 well_formed_pc p p' prog sigma (last_pop … st) ∧
 well_formed_pc p p' prog sigma (pc … st) ∧
 well_formed_state … gsss st.
 
definition sigma_state_pc :
 ∀p.
 ∀p':∀F.sem_unserialized_params p F.
 ∀graph_prog.
  ∀sigma.
(*   let lin_prog ≝ linearise ? graph_prog in *)
  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     well_formed_state_pc p p' graph_prog sigma gsss s →
      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
≝
 λp,p',graph_prog,sigma,gsss,s,prf.
 let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in
 let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in
 let st' ≝ sigma_state … (proj2 … prf) in
 mk_state_pc ? st' pc' last_pop'.
(*
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)».
*)

(* spostato in ExtraMonads.ma

lemma m_list_map_All_ok :
  ∀M : MonadProps.∀X,Y,f,l.
  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
  #M #X #Y #f #l elim l -l
  [ * %{[ ]} %
  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
    %{(y :: ys)}
    change with (! y ← ? ;  ? = ?)
    >EQ >m_return_bind
    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
    @m_return_bind
qed.
*)

definition helper_def_store__commute :
  ∀p,p',graph_prog,sigma.
  ∀X : ? → Type[0].
  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
    X p → beval → regsT p' →
    res (regsT p').
  Prop ≝
  λp,p',graph_prog,sigma,X,gsss,store.
  ∀a : X p.preserving2 … res_preserve …
    (sigma_beval p p' graph_prog sigma)
    (sigma_regs … gsss)
    (sigma_regs … gsss)
    (store … a)
    (store … a).
  
definition helper_def_retrieve__commute :
  ∀p,p',graph_prog,sigma.
  ∀X : ? → Type[0].
  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
    regsT p' → X p → res beval.
  Prop ≝
  λp,p',graph_prog,sigma,X,gsss,retrieve.
  ∀a : X p.
  preserving … res_preserve …
    (sigma_regs … gsss)
    (sigma_beval p p' graph_prog sigma)
    (λr.retrieve … r a)
    (λr.retrieve … r a).

record good_state_sigma
  (p : unserialized_params)
  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
  (sigma : sigma_map p graph_prog)
: Type[0] ≝
{ gsss :> good_sem_state_sigma p p' graph_prog sigma 

; acca_store__commute : helper_def_store__commute … gsss acca_store_
; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_
; accb_store_commute : helper_def_store__commute … gsss accb_store_
; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_
; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_
; dpl_store_commute : helper_def_store__commute … gsss dpl_store_
; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_
; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_
; dph_store_commute : helper_def_store__commute … gsss dph_store_
; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_
; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
; pair_reg_move_commute : ∀mv.
  preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss)
    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    (λr.pair_reg_move_ ? ? (p' ?) r mv)
; allocate_locals__commute :
  ∀loc, r1, prf1. ∃ prf2.
  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
; save_frame_commute : 
  ∀dest,fl.
  preserving … res_preserve …
    (sigma_state_pc … gsss)
    (sigma_state … gsss)
    (save_frame ?? (p' ?) fl dest)
    (save_frame ?? (p' ?) fl dest)
; eval_ext_seq_commute :
  let lin_prog ≝ linearise p graph_prog in
  ∀ stack_sizes.
  ∀ext,i,fn.
  preserving … res_preserve …
    (sigma_state … gsss)
    (sigma_state … gsss)
    (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
      ext i fn)
    (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
      ext i (\fst (linearise_int_fun … fn)))
; setup_call_commute :
  ∀ n , parsT, call_args.
  preserving … res_preserve …
    (sigma_state … gsss)
    (sigma_state … gsss)
    (setup_call ?? (p' ?) n parsT call_args)
    (setup_call ?? (p' ?) n parsT call_args)
; fetch_external_args_commute : (* TO BE CHECKED *)
  ∀ex_fun,st1,prf1,call_args.
  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
; set_result_commute :
  ∀ l , call_dest.
  preserving … res_preserve …
    (sigma_state … gsss)
    (sigma_state … gsss)
    (set_result ?? (p' ?) l call_dest)
    (set_result ?? (p' ?) l call_dest)  
; read_result_commute :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes.
  ∀call_dest.
  preserving … res_preserve …
    (sigma_state … gsss)
    (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf)
    (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes))
     call_dest)
    (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     call_dest)
; pop_frame_commute :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes, curr_id , curr_fn.
  preserving … res_preserve …
    (sigma_state … gsss)
    (sigma_state_pc … gsss)
  (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 
            curr_id curr_fn)
  (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
            curr_id (\fst (linearise_int_fun … curr_fn))) 
}.

lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.
well_formed_state p p' graph_prog sigma gss st →
well_formed_regs … gss r →
well_formed_state … gss (set_regs … r st).
#p #p' #graph_prog #sigma #gss #st #r
*** #H1 #H2 #_ #H4 #H3
%{H4} %{H3} %{H2} @H1
qed.

lemma allocate_locals_def :
  ∀p,F,p',loc,locs,st.
  allocate_locals p F p' (loc::locs) st =
  (let st' ≝ allocate_locals p F p' locs st in
   set_regs … (allocate_locals_ p F p' loc (regs … st')) st').
#p #F #p' #loc #locs #st % qed.

lemma allocate_locals_commute :
  ∀p,p',graph_prog,sigma.
  ∀gss : good_state_sigma p p' graph_prog sigma. 
  ∀locs, st1, prf1. ∃ prf2.
  allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) =
  sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2.
#p #p' #gp #sigma #gss #locs elim locs -locs
[ #st1 #prf1 %{prf1} % ]
#loc #tl #IH #st1 #prf1
letin st2 ≝ (sigma_state … st1 prf1)
cases (IH st1 prf1)
letin st1' ≝ (allocate_locals ??? tl st1)
letin st2' ≝ (allocate_locals ??? tl st2)
#prf' #EQ'
cases (allocate_locals__commute … gss loc (regs … st1') ?)
[2: @hide_prf cases prf' ** // ]
#prf'' #EQ''
% [ @hide_prf @wf_set_regs assumption ]
change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1')
  in match (allocate_locals ??? (loc::tl) st1);
change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2')
  in match (allocate_locals ??? (loc::tl) st2);
>EQ' >EQ'' %
qed.

lemma store_commute :
  ∀p,p',graph_prog,sigma.
  ∀X : ? → Type[0].
  ∀store.
  ∀gsss : good_state_sigma p p' graph_prog sigma. 
  ∀H : helper_def_store__commute … gsss store.
  ∀a : X p.
  preserving2 … res_preserve …
    (sigma_beval p p' graph_prog sigma)
    (sigma_state … gsss)
    (sigma_state … gsss)
    (helper_def_store ? store … a)
    (helper_def_store ? store … a).
#p #p' #graph_prog #sigma #X #store #gsss #H #a
#bv #st #prf1 #prf2
@(mfr_bind … (sigma_regs … gsss)) [@H]
#r #prf3 @mfr_return cases st in prf2;
#frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption
qed.

lemma retrieve_commute :
 ∀p,p',graph_prog,sigma.
 ∀X : ? → Type[0].
 ∀retrieve.
 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 
 ∀H : helper_def_retrieve__commute … gsss retrieve.
 ∀a : X p .
 preserving … res_preserve …
    (sigma_state … gsss)
    (sigma_beval p p' graph_prog sigma)
    (λst.helper_def_retrieve ? retrieve … st a)
    (λst.helper_def_retrieve ? retrieve … st a).
#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed.

(*
definition acca_store_commute :
  ∀p,p',graph_prog,sigma.
  ∀gss : good_state_sigma p p' graph_prog sigma. 
  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
  acca_store … a bv st = return st' → 
  ∃prf2.
  acca_store … a
    (sigma_beval p p' graph_prog sigma bv prf1')
    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
 ≝
λp,p',graph_prog,sigma.
λgss : good_state_sigma p p' graph_prog sigma.
store_commute … gss (acca_store__commute … gss).

*)

(* restano:
; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    state st_pars → res (state st_pars)
; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
    res (list val)
; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)

(* from now on, parameters that use the type of functions *)
; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
(* change of pc must be left to *_flow execution *)
; pop_frame: ∀globals.∀ge : genv_gen F globals.
  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
*)

(*
lemma sigma_pc_commute:
 ∀p,p',graph_prog,sigma,gss,st.
 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
 sigma_pc … (pc ? st) (proj1 … prf) =
 pc ? (sigma_state_pc … st prf). // qed.
*)

(*
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 pc_block_sigma_commute : 
∀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; whd in match sigma_pc_opt; normalize nodelta
 @opt_safe_elim #x
 @if_elim #_
 [2: #H @('bind_inversion H) -H * #i #fn #_
   #H @('bind_inversion H) -H #n #_ ]
 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:
 ∀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 
@'bind_inversion #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 symbol_for_block_match:
    ∀M:matching.∀initV,initW.
     (∀v,w. match_var_entry M v w →
      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    ∀MATCH:match_program … M p p'.
    ∀b: block.
    symbol_for_block … (globalenv … initW p') b =
    symbol_for_block … (globalenv … initV p) b.
* #A #B #V #W #match_fn #match_var #initV #initW #H
#p #p' * #Mvars #Mfn #Mmain
#b
whd in match symbol_for_block; normalize nodelta
whd in match globalenv in ⊢ (???%); normalize nodelta
whd in match (globalenv_allocmem ????);
change with (add_globals ?????) in match (foldl ?????);
>(proj1 … (add_globals_match … initW … Mvars))
[ % |*:]
[ * #idr #v * #idr' #w #MVE %
  [ inversion MVE
    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
  | @(H … MVE)
  ]
| @(matching_fns_get_same_blocks … Mfn) 
  #f #g @match_funct_entry_id
]
qed.

lemma symbol_for_block_transf :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl.
 symbol_for_block … (globalenv … init prog_out) bl =
 symbol_for_block … (globalenv … init prog_in) bl.
#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
#v0 #w0 * //
qed.

lemma fetch_function_transf :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl,i,f.
 fetch_function … (globalenv … init prog_in) bl = 
  return 〈i, f〉
→ fetch_function … (globalenv … init prog_out) bl =
  return 〈i, trans … f〉.
#A #B #V #init #prog_in #trans #bl #i #f
 whd in match fetch_function; normalize nodelta
 #H lapply (opt_eq_from_res ???? H) -H
 #H @('bind_inversion H) -H #id #eq_symbol_for_block
 #H @('bind_inversion H) -H #fd #eq_find_funct
 whd in ⊢ (??%?→?); #EQ destruct(EQ)
 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
 >(find_funct_ptr_transf A B …  eq_find_funct) %
qed.

lemma fetch_internal_function_transf :
 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
 ∀bl,i,f.
 fetch_internal_function … (globalenv_noinit … prog_in) bl = 
  return 〈i, f〉
→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
  return 〈i, trans … f〉.
#A #B #prog #trans #bl #i #f
 whd in match fetch_internal_function; normalize nodelta
 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
 whd in ⊢ (??%%→?); #EQ destruct(EQ)
 >(fetch_function_transf … EQfetch) %
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,globals,graph_code,entry,lin_code,lbl,pt,sigma.
 good_local_sigma p globals graph_code entry lin_code sigma →
 code_closed … lin_code →
 sigma lbl = return pt →
 ∀stmt.
   stmt_at … graph_code
    lbl = return stmt →
  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
 match stmt with
 [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') 
 | sequential s' nxt ⇒
             match s' with
             [ step_seq _ ⇒
               (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧
                  ((sigma nxt = Some ? (S pt)) ∨
                   (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧
                    point_of_label … lin_code nxt = sigma nxt) )
             | COND a ltrue ⇒
               (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ 
               sigma nxt = Some ? (S pt)) ∨
               (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧
                point_of_label … lin_code nxt = sigma nxt)
             ]
 | FCOND abs _ _ _ ⇒ Ⓧabs    
 ].  
 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
 ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf
elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec
#All_succs_in #next_spec
#stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ)
% [assumption]
cases stmt in next_spec; -stmt
[ * [ #s | #a #lbl ] #nxt | #s | * ]
normalize nodelta
[ * #H #G %{H}
  cases G -G #G
  [ %1{G} ]
| * [ #H %1{H} ] #G
| //
] %2 %{G}
  lapply (refl …  (point_of_label … lin_code nxt))
  change with (If ? then with prf do ? else ?) in ⊢ (???%→?);
  @If_elim <(lin_code_has_label … (mk_lin_params p))
  [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ]
  * #H cases (H ?) -H
  lapply (lin_code_closed … G) ** [2: #_ * ] //
qed.
 
(*

 >(if_of_function_commute … graph_fun)

check opt_Exists
check linearise_int_fun
check 
 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 // *)

definition good_sigma :
  ∀p.∀graph_prog : joint_program (mk_graph_params p).
  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
    label → option ℕ) → Prop ≝
  λp,graph_prog,sigma.
  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).

lemma pc_of_label_sigma_commute :
  ∀p,p',graph_prog,bl,lbl,i,fn.
  let lin_prog ≝ linearise ? graph_prog in
  ∀sigma.good_sigma p graph_prog sigma →
  fetch_internal_function …
    (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 →
  let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in
  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
    bl lbl =
        return sigma_pc p p' graph_prog sigma pc' prf'.
#p #p' #graph_prog #bl #lbl #i #fn
#sigma #good cases (good fn) -good * #_ #all_labels_in
#good #fetchfn >lin_code_has_label #lbl_in
whd in match pc_of_label; normalize nodelta
> (fetch_internal_function_transf … fetchfn) >m_return_bind
inversion (point_of_label ????)
[ (*
  change with (If ? then with prf do ? else ? = ? → ?)
  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
  %
  [ @hide_prf whd %
  | whd in match sigma_pc; normalize nodelta
    @opt_safe_elim #pc'
  ]
  whd in match sigma_pc_opt; normalize nodelta
  @eqZb_elim #Hbl normalize nodelta
  [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn;
  |*: >fetchfn >m_return_bind
    >point_of_pc_of_point
    >EQsigma
  ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
]
qed.

lemma graph_pc_of_label :
  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
  ∀globals,ge,bl,i_fn,lbl.
  fetch_internal_function ? ge bl = return i_fn →
  pc_of_label pars globals ge bl lbl =
    OK ? (pc_of_point pars bl lbl).
#p #p' #globals #ge #bl #fn #lbl #fetchfn
whd in match pc_of_label; normalize nodelta
>fetchfn %
qed.

lemma point_of_pc_sigma_commute :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀sigma,pc,f,fn,n.
  ∀prf : well_formed_pc p p' graph_prog sigma pc.
 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
whd in match sigma_pc; normalize nodelta
@opt_safe_elim #pc' whd in match sigma_pc_opt;
normalize nodelta @eqZb_elim #Hbl
[ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch;
  whd in ⊢ (???%→?); #ABS destruct(ABS) ]
>EQfetch >m_return_bind >EQsigma
whd in ⊢ (??%%→?); #EQ destruct(EQ)
@point_of_offset_of_point  
qed.

lemma graph_succ_pc :
  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
  ∀pc,lbl.
  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
normalize //
qed.

lemma fetch_statement_sigma_commute:
  ∀p,p',graph_prog,pc,f,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 〈f, fn,stmt〉 →
  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
      pc_of_label (make_sem_lin_params p p') …
          (globalenv_noinit … lin_prog)
          (pc_block pc)
          lbl = return sigma_pc … prf)
    (stmt_explicit_labels … stmt) ∧
  match stmt with
  [  sequential s nxt ⇒
        match s with
        [ step_seq x ⇒ 
          fetch_statement (make_sem_lin_params p p') …
          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
              return 〈f, \fst (linearise_int_fun … fn),
                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
          ∃prf'.
            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 
            let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
            (nxt_pc = sigma_nxt ∨
              (fetch_statement (make_sem_lin_params p p') …
                (globalenv_noinit … lin_prog) nxt_pc =
                return 〈f, \fst (linearise_int_fun … fn),
                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
              (pc_of_label (make_sem_lin_params p p') …
                (globalenv_noinit … lin_prog)
                (pc_block pc)
                nxt = return sigma_nxt)))
        | COND a ltrue ⇒ 
            ∃prf'.
            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 
            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
            (fetch_statement (make_sem_lin_params p p') …
            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 
              return 〈f, \fst (linearise_int_fun … fn), 
                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
             nxt_pc = sigma_nxt)) ∨
            (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf)  
             = 
             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
            pc_of_label (make_sem_lin_params p p') …
                (globalenv_noinit … lin_prog)
                (pc_block pc)
                nxt = return sigma_nxt)
         ]
    | final z ⇒   fetch_statement (make_sem_lin_params p p') … 
                   (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 
                   return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉
    | FCOND abs _ _ _ ⇒ Ⓧabs
  ].
#p #p' #graph_prog #pc #f #fn #stmt #sigma 
#good elim (good fn) * #_ #all_labels_in #good_local #wfprf
#H elim (fetch_statement_inv … H) #fetchfn #graph_stmt 
whd in match well_formed_pc in wfprf; normalize nodelta in wfprf;
inversion(sigma_pc_opt p p' graph_prog sigma pc) 
[#ABS @⊥ >ABS in wfprf; * #H @H %]
#lin_pc
whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta  in ⊢ (%→?);
@eqZb_elim #Hbl
[ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ]
normalize nodelta >fetchfn >m_return_bind
#H @('bind_inversion H) -H
#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt)
[@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 %
[ cases stmt in H2;
  [ * [#s|#a#lbl]#nxt | #s | *]
  normalize nodelta
  [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ]
  cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ)
  #H #_
  [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn)
  |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H
  ]
]
cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
>pc_block_sigma_commute 
>(fetch_internal_function_transf … fetchfn) >m_return_bind
>(point_of_pc_sigma_commute … fetchfn lin_pt_spec)
[ % 
   [ >(proj1 … H3) %
   | % [ @hide_prf %
     | change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?);
       @opt_safe_elim #pc1
     ] whd in match sigma_pc_opt;
        normalize nodelta >(eqZb_false … Hbl) >fetchfn
        >m_return_bind
        >graph_succ_pc >point_of_pc_of_point
        cases(proj2 … H3)
        [1,3: #EQ >EQ
        |*: * cases all_labels_spec #Z #_ #sn
          >(opt_to_opt_safe … Z) #EQpoint_of_label
        ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
        [ %1 
          whd in match (point_of_succ ???) ;
          whd in match point_of_pc; normalize nodelta
          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
          @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind
          >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ)
          whd in match succ_pc; whd in match point_of_pc; normalize nodelta
          >point_of_offset_of_point %
        | %2 whd in match (pc_block ?); >pc_block_sigma_commute
          >(fetch_internal_function_transf … fetchfn) >m_return_bind
          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
          @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta 
          #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind
          whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct
          whd in match point_of_pc; whd in match succ_pc; normalize nodelta
          whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
          whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
          >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta
           >(fetch_internal_function_transf … fetchfn) >m_return_bind
           >EQpoint_of_label %
        ]
   ]
 | % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta
      >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn
      >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta
      whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
      >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_
      >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)]
   cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind 
      [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
       @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2 
       >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind
       >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc;
       normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
       >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ
       whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ
       whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point %
      |%2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label;
       normalize nodelta >(fetch_internal_function_transf … fetchfn)
       >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE
       >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind 
       normalize in ⊢ (??%?);
       whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
       @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?);
       >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc;
       normalize nodelta whd in match point_of_pc; whd in match pc_of_point;
       normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H;
       [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind
       #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta %
      ]
  | >H3 >m_return_bind %
]
qed.

(*
spostato in ExtraMonads.ma

lemma res_eq_from_opt : ∀A,m,a.
res_to_opt A m = return a → m = return a.
#A #m #a  cases m #x normalize #EQ destruct(EQ) %
qed.

lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
#X #Y #P #F #m #n #H #x #EQ
cases (H x ?)
[ #prf #EQ' %{prf} >EQ' %
| cases m in EQ; normalize #x #EQ destruct %
]
qed.
*)
lemma sigma_pc_exit :
  ∀p,p',graph_prog,sigma,pc,prf.
  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
  pc = exit →
  sigma_pc p p' graph_prog sigma pc prf = exit.
#p #p' #graph_prog #sigma #pc #prf
whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
#EQ1 #EQ2 destruct
whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?);
destruct %
qed.

(* this should make things easier for ops using memory (where pc cant happen) *)
definition bv_no_pc : beval → Prop ≝
λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].

lemma bv_pc_other :
  ∀P : beval → Prop.
  (∀pc,p.P (BVpc pc p)) →
  (∀bv.bv_no_pc bv → P bv) →
  ∀bv.P bv.
#P #H1 #H2 * /2/ qed.

lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
  bv_no_pc bv →
  sigma_beval p p' graph_prog sigma bv prf = bv.
#p #p' #graph_prog #sigma *
[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
#prf * whd in match sigma_beval; normalize nodelta
@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
qed.

lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
#p #p' #graph_prog #sigma *
[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
% whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.

lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by.
* [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by
  whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.

lemma sigma_pc_no_exit :
  ∀p,p',graph_prog,sigma,pc,prf.
  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
  pc ≠ exit →
  sigma_pc p p' graph_prog sigma pc prf ≠ exit.
#p #p' #graph_prog #sigma #pc #prf
@(eqZb_elim (block_id (pc_block pc)) (-1))
[ #Hbl
  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
  whd in match sigma_pc_opt; normalize nodelta
  >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ]
#NEQ #_ inversion (sigma_pc ??????)
** #r #id #EQr #off #EQ
lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ'
% #ABS destruct(ABS) cases NEQ #H @H -H
cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') %
qed.

definition linearise_status_rel:
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes.
 ∀sigma. ∀ gss : good_state_sigma p p' graph_prog 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,gss,good.
   mk_status_rel …
    (* sem_rel ≝ *) (λs1,s2.
     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
      s2 = sigma_state_pc … s1 prf)
    (* call_rel ≝ *) (λs1,s2.
      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
      pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf)))
    (* sim_final ≝ *) ?.
#st1 #st2 * #prf #EQ2
% [2: cases daemon]
>EQ2
whd in ⊢ (%→%);
#H lapply (opt_to_opt_safe … H)
@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
#H lapply(res_eq_from_opt ??? H) -H
#H  @('bind_inversion H) -H
** #id #int_f #stmt
#stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec)
cases stmt in stmt_spec; -stmt normalize nodelta
[1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
* normalize nodelta 
[1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
#fetch_graph_spec #_ #fetch_lin_spec
#H >fetch_lin_spec >m_return_bind normalize nodelta
letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes))
letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
cut (preserving … res_preserve …
       (sigma_state … gss)
       (λl.λ_ : True.l)
       (λst.
          do st' ← pop_frame … graph_ge id int_f st;
          if eq_program_counter (pc … st') exit_pc then 
          do vals ← read_result … graph_ge (joint_if_result … int_f) st ;
            Word_of_list_beval vals
          else
            Error ? [ ])
       (λst.
          do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st;
          if eq_program_counter (pc … st') exit_pc then 
          do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ;
            Word_of_list_beval vals
          else
            Error ? [ ]))
[ #st #prf @mfr_bind [3: @pop_frame_commute |*:]
  #st' #prf' @eq_program_counter_elim  
  [ #EQ_pc normalize nodelta
    change with (sigma_pc ??????) in match (pc ??);
    >(sigma_pc_exit … EQ_pc) normalize nodelta
    @mfr_bind [3: @read_result_commute |*:]
    #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv'
    @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
    [
    | * -lbv -lbv' #by1 #lbv #lbv_prf
      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
    [ @opt_safe_elim #lbv' #EQ_lbv'
    |* -lbv #by2 #lbv #lbv_prf
      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
    [ @opt_safe_elim #lbv' #EQ_lbv'
    |* -lbv #by3 #lbv #lbv_prf
      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
    [ @opt_safe_elim #lbv' #EQ_lbv'
    |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ]
      #lbv_prf @mfr_return %
    ]]]]
    cases lbv in EQ_lbv';
    try (#H @res_preserve_error)
    -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1'
    #H @('bind_inversion H) -H #tl' #EQtl'
    whd in ⊢ (??%?→?); #EQ destruct(EQ)
    @(mfr_bind … (λby.λ_:True.by))
    [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1';
      whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    |*: #by1 * @mfr_return_eq
      change with (m_list_map ????? = ?) in EQtl';
      [1,3,5,7: %
      |*: @opt_safe_elim #lbv''
      ] >EQtl' #EQ destruct %
    ]
  | #_ @res_preserve_error
  ]
]
#PRESERVE
cases (PRESERVE … (proj2 … prf) … H) *
#EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS)
qed.

lemma as_label_sigma_commute :
  ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma →
  ∀st,prf.
  as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes)
    (sigma_state_pc p p' graph_prog sigma gss st prf) =
  as_label (graph_abstract_status p p' graph_prog stack_sizes) st.
#p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped
** #prf1 #prf2 #prf3
change with (as_label_of_pc ?? = as_label_of_pc ??)
change with (sigma_pc ??????) in match (as_pc_of ??);
change with pc in match (as_pc_of ??);
whd in match sigma_pc; normalize nodelta
@opt_safe_elim #pc'
whd in match sigma_pc_opt; normalize nodelta
@eqZb_elim #Hbl normalize nodelta
[ whd in ⊢ (??%%→??%%); #EQ destruct(EQ)
  whd in match fetch_statement; normalize nodelta
  >(fetch_internal_function_no_minus_one … graph_prog … Hbl)
  >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) %
| #H @('bind_inversion H) * #i #f -H
  inversion (fetch_internal_function … (pc_block pc))
  [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
  * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ)
  #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
  whd in ⊢ (??%%);
  whd in match fetch_statement; normalize nodelta >EQfetch
  >(fetch_internal_function_transf … graph_prog 
    (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch)
  >m_return_bind >m_return_bind
  cases (good f) * #_ #all_labels_in #spec
  cases (spec … EQsigma) #s ** cases s -s
  [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_
  [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ]
  whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
  >EQstmt_at >EQstmt_at' normalize nodelta %
qed.
  
lemma set_istack_sigma_commute :
∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3.
set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) = 
sigma_state ???? gss (set_istack ? is st) prf3. 
#p #p' #graph_prog #sigma #gss *
#frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed.
(* #st #is #sigmais #prf1 #prf2 #H
whd in match set_istack; normalize nodelta
whd in match sigma_state; normalize nodelta
whd in match sigma_is; normalize nodelta
@opt_safe_elim #x #H1 
cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
#EQ >EQ //
qed.*)

lemma is_push_sigma_commute :
∀ p, p', graph_prog,sigma.
preserving2 … res_preserve …
  (sigma_is p p' graph_prog sigma)
  (sigma_beval p p' graph_prog sigma)  
  (sigma_is p p' graph_prog sigma)
  is_push is_push.
#p #p' #graph_prog #sigma *
[ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is'
whd in ⊢ (??%%→?); #EQ destruct(EQ)
whd in match sigma_beval; normalize nodelta
@opt_safe_elim #val' #EQsigma_val
%
[1,3: @hide_prf %
|*: whd in match sigma_is in ⊢ (???%); normalize nodelta
  @opt_safe_elim #is''
] whd in match sigma_is_opt; normalize nodelta
[2,4:
  inversion (sigma_beval_opt ?????)
  [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1;
    normalize nodelta * #H @H % ]
  #bv1' #EQ_bv1' >m_return_bind ]
>EQsigma_val
whd in ⊢ (??%%→?); #EQ destruct(EQ)
whd in match sigma_is; normalize nodelta 
@opt_safe_elim #is1
whd in match sigma_is_opt; normalize nodelta
[ #H @('bind_inversion H) #bv1''
  >EQ_bv1' #EQ destruct(EQ) ]
whd in ⊢ (??%%→?); #EQ destruct(EQ) %
qed.

lemma Bit_of_val_inv :
  ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v.
#e *
[ #b || #b #ptr #p #o ] #v
whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.

lemma beopaccs_sigma_commute :
∀p,p',graph_prog,sigma,op.
preserving2 … res_preserve …
  (sigma_beval p p' graph_prog sigma)
  (sigma_beval p p' graph_prog sigma)
  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
  (be_opaccs op) (be_opaccs op).
#p #p' #graph_prog #sigma #op
#bv1 #bv2 #prf1 #prf2
@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
[2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
  [2: #by2 * cases (opaccs ????) #by1' #by2'
    @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ)
  ]
]
#v #EQ %{I} 
>sigma_bv_no_pc try assumption
>(Byte_of_val_inv … EQ) %
qed.

lemma beop1_sigma_commute :
∀p,p',graph_prog,sigma,op.
preserving … res_preserve …
  (sigma_beval p p' graph_prog sigma)
  (sigma_beval p p' graph_prog sigma)
  (be_op1 op) (be_op1 op).
#p #p' #graph_prog #sigma #op
#bv #prf
@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
[2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
#v #EQ %{I} >sigma_bv_no_pc try assumption
>(Byte_of_val_inv … EQ) %
qed.


lemma sigma_ptr_commute :
∀ p, p', graph_prog , sigma.
preserving … res_preserve …
  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
  (λx.λ_ : True.x)
  pointer_of_address pointer_of_address.
#p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2
#ptr whd in ⊢ (??%?→?);
cases val1 in prf1;
[|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ]
#prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
cases val2 in prf2 EQ;
[|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ]
#prf2 normalize nodelta #EQ destruct(EQ)
%{I}
>sigma_bv_no_pc [2: %]
>sigma_bv_no_pc [2: %] @EQ
qed.

lemma beop2_sigma_commute :
∀p,p',graph_prog,sigma,carry,op.
preserving2 … res_preserve …
  (sigma_beval p p' graph_prog sigma)
  (sigma_beval p p' graph_prog sigma)
  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉)
  (be_op2 carry op) (be_op2 carry op).
#p #p' #graph_prog #sigma #carry #op
@bv_pc_other
[ #pc1 #p1 #bv2
| #bv1 #bv1_no_pc 
  @bv_pc_other
  [ #pc2 #p2
  | #bv2 #bv2_no_pc
  ]
] #prf1 #prf2
* #res #carry'
[1,2:
  [2: cases bv1 in prf1;
    [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ]
   whd in ⊢ (??%%→?);
  #EQ destruct(EQ) ]
#EQ
cut (bv_no_pc res)
[ -prf1 -prf2
  cases bv1 in bv1_no_pc EQ;
  [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] *
  cases bv2 in bv2_no_pc;
  [3,10,17,24,31,38: #ptr21 #ptr22 #p2
  |4,11,18,25,32,39: #by2
  |5,12,19,26,33,40: #p2
  |6,13,20,27,34,41: #ptr2 #p2
  |7,14,21,28,35,42: #pc2 #p2
  ] *
  cases op
  whd in match be_op2; whd in ⊢ (???%→?);
  normalize nodelta
  #EQ destruct(EQ) try %
  try (whd in EQ : (??%?); destruct(EQ) %)
  lapply EQ -EQ
  [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
  |2,12,13,16,18: @if_elim #_  whd in ⊢ (??%%→?); #EQ destruct(EQ) %
  |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ
    cases (op2 eval bit ???) #res' #bit'
    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
  |17: cases (ptype ptr1) normalize nodelta
    [ @if_elim #_
      [ #H @('bind_inversion H) #bit #EQbit
      cases (op2 eval bit ???) #res' #bit'
      ]
    ]
    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
  |*: whd in ⊢ (??%?→?);
    cases (ptype ?) normalize nodelta
    try (#EQ destruct(EQ) @I)
    cases (part_no ?) normalize nodelta
    try (#n lapply (refl ℕ n) #_)
    try (#EQ destruct(EQ) @I)
    try (#H @('bind_inversion H) -H * #EQbit
         whd in ⊢ (??%%→?);)
    try (#EQ destruct(EQ) @I)
    [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?);
         #EQ destruct(EQ) @I
    |*: cases carry normalize nodelta
      try (#b lapply (refl bool b) #_)
      try (#ptr lapply (refl pointer ptr) #_ #p #o)
      try (#EQ destruct(EQ) @I)
      @if_elim #_
      try (#EQ destruct(EQ) @I)
      @If_elim #prf
      try (#EQ destruct(EQ) @I)
      cases (op2_bytes ?????)
      #res' #bit' whd in ⊢ (??%%→?);
      #EQ destruct(EQ) @I
    ]
  ]
] #res_no_pc
%{(bv_no_pc_wf … res_no_pc)}
>(sigma_bv_no_pc … bv1_no_pc)
>(sigma_bv_no_pc … bv2_no_pc)
>(sigma_bv_no_pc … res_no_pc)
assumption
qed.

definition combine_strong :
  ∀A,B,C,D : Type[0].
  ∀P : A → Prop.∀Q : C → Prop.
  (∀x.P x → B) → (∀x.Q x → D) →
  (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝
λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉.

lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is.
well_formed_state p p' graph_prog sigma gss st →
sigma_is_opt p p' graph_prog sigma is ≠ None ? →
well_formed_state … gss (set_istack … is st).
#p #p' #graph_prog #sigma #gss #st #is
*** #H1 #H2 #H3 #H4 #H5
%{H4} %{H3} %{H5} @H1
qed.

lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m.
well_formed_state p p' graph_prog sigma gss st →
well_formed_mem p p' graph_prog sigma m →
well_formed_state … gss (set_m … m st).
#p #p' #graph_prog #sigma #gss #st #m
*** #H1 #H2 #H3 #H4 #H5
%{H5} %{H3} %{H2} @H1
qed.
(* spostato in ExtraMonads.ma
lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
       opt_preserve X Y P F m n →
       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
#X #Y #P #F #m #n #e1 #e2 #H #v #prf
cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
>EQ %
qed.

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 res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
       res_preserve X Y P F m n →
       io_preserve O I X Y P F m n.
#O #I #X #Y #P #F #m #n #H #v #prf
cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
>EQ %
qed.
*)
lemma eval_seq_no_pc_sigma_commute :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes.
 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
 ∀f,fn,stmt.
 preserving … res_preserve …
   (sigma_state … gss)
   (sigma_state … gss)
   (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
      f fn stmt)
   (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
      f (\fst (linearise_int_fun … fn)) stmt).
  #p #p' #graph_prog #stack_sizes #sigma #gss #f
  #fn #stmt
  whd in match eval_seq_no_pc; 
  cases stmt normalize nodelta
  [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return
  | (* MOVE *) #mv_sig #st #prf'
    @mfr_bind [3: @pair_reg_move_commute |*:]
    #r #prf @mfr_return @wf_set_regs assumption
  | (* POP *)
    #a #st #prf
    @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss)))
    [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2'
      @mfr_return %{prf1'} @wf_set_is assumption
    | * #bv #st' * #prf1' #prf2'
      @mfr_bind [3: @acca_store__commute |*:]
      #r #prf3' @mfr_return @wf_set_regs assumption
    ]
  | (* PUSH *)
     #a #st #prf
     @mfr_bind [3: @acca_arg_retrieve_commute |*:]
     #bv #prf_bv
     @mfr_bind [3: @is_push_sigma_commute |*:]
     #is #prf_is @mfr_return @wf_set_is assumption
  | (*C_ADDRESS*) 
    #sy
    change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) 
    #sy_prf
    change with ((dpl_reg p) → ?) #dpl  
    change with ((dph_reg p) → ?) #dph
    #st #prf
    @(mfr_bind … (sigma_state … gss))
    [ @(mfr_bind … (sigma_regs … gss))
      [2: #r #prf' @mfr_return @wf_set_regs assumption ]
    ]
    @opt_safe_elim #bl #EQbl
    @opt_safe_elim #bl'
    >(find_symbol_transf …
          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?);
    >EQbl in ⊢ (%→?); #EQ destruct(EQ)
    [ @dpl_store_commute
    | #st' #st_prf'
      @mfr_bind [3: @dph_store_commute |*:]
      [2: #r #prf' @mfr_return @wf_set_regs assumption
      ]
    ] @bv_no_pc_wf %
  | (*C_OPACCS*)
    #op #a #b #arg1 #arg2 #st #prf
    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
    #bv1 #bv1_prf
    @mfr_bind [3: @accb_arg_retrieve_commute |*: ]
    #bv2 #bv2_prf
    @mfr_bind [3: @beopaccs_sigma_commute |*: ]
    * #res1 #res2 * #res1_prf #res2_prf
    @(mfr_bind … (sigma_state … gss))
    [ @mfr_bind [3: @acca_store__commute |*: ]
      #r #r_prf @mfr_return @wf_set_regs assumption
    ]
    #st' #st_prf'
    @mfr_bind [3: @accb_store_commute |*: ]
    #r #r_prf @mfr_return @wf_set_regs assumption
  | (*C_OP1*)
    #op #a #arg #st #prf
    @mfr_bind [3: @acca_retrieve_commute |*: ]
    #bv #bv_prf
    @mfr_bind [3: @beop1_sigma_commute |*: ]
    #res #res_prf
    @mfr_bind [3: @acca_store__commute |*: ]
    #r #r_prf @mfr_return @wf_set_regs assumption
  | (*C_OP2*)
    #op #a #arg1 #arg2 #st #prf
    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
    #bv1 #bv1_prf
    @mfr_bind [3: @snd_arg_retrieve_commute |*: ]
    #bv2 #bv2_prf
    @mfr_bind [3: @beop2_sigma_commute |*: ]
    * #res1 #carry' #res1_prf
    @(mfr_bind … (sigma_state … gss))
    [ @mfr_bind [3: @acca_store__commute |*: ]
      #r #r_prf @mfr_return @wf_set_regs assumption
    ]
    #st' #st_prf' @mfr_return
  | (*C_CLEAR_CARRY*)
     #st #prf @mfr_return
  | (*C_SET_CARRY*)
    #st #prf @mfr_return
  | (*C_LOAD*)
    #a #dpl #dph #st #prf
    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
    #bv1 #bv1_prf
    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
    #bv2 #bv2_prf
    @mfr_bind [3: @sigma_ptr_commute |*:]
    [ % assumption ]
    #ptr *
    @mfr_bind
    [3:
     @opt_to_res_preserve @beloadv_sigma_commute
   |*:]
   #res #res_prf
   @mfr_bind [3: @acca_store__commute |*: ]
   #r #r_prf @mfr_return @wf_set_regs assumption
 | (*C_STORE*)
    #dpl #dph #a #st #prf
    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
    #bv1 #bv1_prf
    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
    #bv2 #bv2_prf
    @mfr_bind [3: @sigma_ptr_commute |*:]
    [ % assumption ]
    #ptr *
    @mfr_bind
    [3: @acca_arg_retrieve_commute |*:]
    #res #res_prf
    @mfr_bind
    [3:
     @opt_to_res_preserve @bestorev_sigma_commute
    |*:]
    #mem #wf_mem
    @mfr_return
    @wf_set_m assumption
 | (*CALL*)
     #f #args #dest #st #prf @mfr_return
 |  (*C_EXT*)
    #s_ext #st #prf @eval_ext_seq_commute
 ]
 qed.

lemma eval_seq_no_call_ok :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes.
 ∀sigma.good_sigma p graph_prog sigma → 
 ∀gss : good_state_sigma p p' graph_prog sigma.
 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
 ∀prf : well_formed_state_pc … gss st.
   fetch_statement (make_sem_graph_params p p') …
    (globalenv_noinit ? graph_prog) (pc … st) =
      return 〈f, fn,  sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 →
   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
    return st' →
 ∃prf'.
 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
  (sigma_state_pc … gss st prf)
  (sigma_state_pc … gss st' prf').
 bool_to_Prop (taaf_non_empty … taf).
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
#prf #EQfetch
whd in match eval_state; normalize nodelta >EQfetch
>m_return_bind whd in match eval_statement_no_pc;
whd in match eval_statement_advance; normalize nodelta
@'bind_inversion #st_no_pc' #EQeval
>no_call_advance [2: assumption]
whd in ⊢ (??%%→?); #EQ destruct(EQ)
cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
normalize nodelta #_ * #EQfetch' *
#prf_nxt #nxt_spec
lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval
cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval)
#st_no_pc_prf
#EQeval'
%{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ]
cases nxt_spec -nxt_spec
[ #nxt_spec %{(taaf_step … (taa_base …) …) I}
| * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I}
]
[1,6:
  whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
  whd in match joint_classify_step; normalize nodelta
  >no_call_other try % assumption
|2,5:
  whd whd in match eval_state; normalize nodelta
  change with (sigma_pc ??????) in match (pc ??);
  try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
  whd in match eval_statement_no_pc; normalize nodelta
  try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
  whd in match eval_statement_advance; normalize nodelta
  >no_call_advance try assumption
  whd in match (next ???) in ⊢ (??%?);
  [ >nxt_spec %
  | %
  ]
|3:
  whd whd in ⊢ (??%?); >nxt_spec normalize nodelta %
|4:
  whd whd in match eval_state; normalize nodelta
  >nxt_spec >m_return_bind >m_return_bind
  whd in match eval_statement_advance; normalize nodelta
  whd in match goto; normalize nodelta
  whd in match (pc_block ?); >pc_block_sigma_commute
  >pc_of_label_spec %
|7: %* #H @H -H
  whd in ⊢ (??%?); >nxt_spec %
|8:
]
qed.

lemma block_of_call_sigma_commute : 
∀p,p',graph_prog,sigma.
∀gss : good_state_sigma p p' graph_prog sigma.∀cl.
 preserving … res_preserve …
   (sigma_state p p' graph_prog sigma gss)
   (λx.λ_ : True .x)
   (block_of_call (make_sem_graph_params p p') … 
      (globalenv_noinit ? graph_prog) cl)   
   (block_of_call (make_sem_lin_params p p') … 
      (globalenv_noinit ? (linearise ? graph_prog)) cl).
#p #p' #graph_prog #sigma #gss #cl #st #prf 
@mfr_bind
[3: cases cl
  [ #id normalize nodelta @opt_to_res_preserve
    >(find_symbol_transf …
          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id)
   #s #EQs %{I} >EQs in ⊢ (??%?); %
  | * #dpl #dph normalize nodelta
    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
    #bv1 #bv1_prf
    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
    #bv2 #bv2_prf
    @(mfr_bind … (λptr.λ_:True.ptr))
    [ change with (pointer_of_address 〈?,?〉) in
      match (pointer_of_bevals ?);
      change with (pointer_of_address 〈?,?〉) in
      match (pointer_of_bevals [sigma_beval ??????;?]);
      @sigma_ptr_commute % assumption
    ] #ptr *
    @if_elim #_ [ @mfr_return | @res_preserve_error ] %
 ]
|4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ
|*:
]
qed.

lemma fetch_function_no_minus_one :
  ∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
  whd in match fetch_function; normalize nodelta
  >globalenv_no_minus_one
  cases (symbol_for_block ???) normalize //
qed.

lemma entry_sigma_commute: 
∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma → 
∀bl,f1,fn1.
(fetch_function ? (globalenv_noinit … graph_prog) bl = 
return 〈f1,Internal ? fn1〉) → 
∃prf.
sigma_pc p p' graph_prog sigma 
   (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
      pc_of_point (make_sem_lin_params p p') bl 0.
#p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec
cases (good fn1) * #entry_in #_ #_
       % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ]
       whd in match sigma_pc_opt; normalize nodelta
       >eqZb_false whd in match (pc_block ?);
       [2,4: % #EQbl
        >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec;
        whd in ⊢ (???%→?); #ABS destruct(ABS) ]
       normalize nodelta whd in match fetch_internal_function;
       normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point
       >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) %
qed.

lemma eval_call_ok :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes.
 ∀sigma. good_sigma p graph_prog sigma → 
 ∀gss : good_state_sigma p p' graph_prog sigma.
 ∀st,st',f,fn,called,args,dest,nxt.
 ∀prf : well_formed_state_pc … gss st.
  fetch_statement (make_sem_graph_params p p') …
    (globalenv_noinit ? graph_prog) (pc … st) =
      return 〈f, fn,
        sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 →
   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
    return st' →
(* let st_pc' ≝ mk_state_pc ? st'
  (succ_pc (make_sem_graph_params p p') …
    (pc … st) nxt) in
 ∀prf'.
 fetch_statement (make_sem_lin_params p p') …
   (globalenv_noinit … lin_prog)
     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
 pc_of_label (make_sem_lin_params p p') ?
                (globalenv_noinit ? (linearise p … graph_prog))
                (pc_block (pc … st))
                nxt = return sigma_pc p p' graph_prog sigma
    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*)
  let st2_pre_call ≝ sigma_state_pc … gss st prf in
  ∃is_call, is_call'.
  ∃prf'.
  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
  joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» =
  joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧
  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
    st2_pre_call = return st2_after_call.
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn 
#called #args #dest #nxt #prf #fetch_spec 
cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_
normalize nodelta * #lin_fetch_spec #_
whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec
>m_return_bind >m_return_bind whd in match eval_statement_advance;
whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta
@('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec
@('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H
cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta 
[2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_
  @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
#H lapply (err_eq_from_io ????? H) -H
#H @('bind_inversion H) -H #st_no_pc #save_frame_spec
>m_bind_bind
#H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H
whd in match (stack_sizes ?);
#stack_size_spec
>m_bind_bind
#H @('bind_inversion H) -H #st_no_pc' #set_call_spec
>m_return_bind whd in ⊢ (??%%→?);
whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
%
[  @hide_prf 
  whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind
  normalize nodelta whd in match joint_classify_step; 
  whd in match joint_classify_seq; normalize nodelta
  >bl_spec >m_return_bind >int_f_spec normalize nodelta %
| cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 
            bl_spec)
  * #lin_bl_spec
  generalize in match (fetch_function_transf … graph_prog …
      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
      … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
  #lin_int_f_spec
  %
  [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec
    >m_return_bind normalize nodelta whd in match joint_classify_step; 
    whd in match joint_classify_seq; normalize nodelta
    >lin_bl_spec >m_return_bind
    >lin_int_f_spec %
   | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?;
    [2: @hide_prf cases st in prf; // ]
    #st_no_pc_wf #lin_save_frame_spec
     cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?;
     #st_no_pc_wf' #lin_set_call_spec
     cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf')
     #st_no_pc_wf'' #lin_allocate_locals_spec
     cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec)
     #entry_prf #entry_spec
      % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ]
      % [ whd in match joint_call_ident; normalize nodelta
          >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
          >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
          normalize nodelta
          >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
          whd in match fetch_internal_function; normalize nodelta
          >lin_int_f_spec >int_f_spec %
        | whd in match eval_state; normalize nodelta 
          >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
           whd in match eval_statement_no_pc; normalize nodelta 
           whd in match eval_seq_no_pc; normalize nodelta 
           >m_return_bind in ⊢ (??%?);
           whd in match eval_statement_advance; whd in match eval_seq_advance; 
           whd in match eval_seq_call; normalize nodelta
           >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
           >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
           normalize nodelta
           >lin_save_frame_spec >m_return_bind
           >m_bind_bind whd in match (stack_sizes ?);
           >stack_size_spec >m_return_bind
           >lin_set_call_spec >m_return_bind
           >lin_allocate_locals_spec
           <entry_spec %
         ]
       ]
     ]
qed.          
                
lemma eval_goto_ok :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes.
 ∀sigma.good_sigma p graph_prog sigma → 
 ∀gss : good_state_sigma p p' graph_prog sigma.
 ∀st,st',f,fn,nxt.
 ∀prf : well_formed_state_pc … gss st.
   fetch_statement (make_sem_graph_params p p') …
    (globalenv_noinit ? graph_prog) (pc … st) =
      return 〈f, fn,  final … (GOTO (mk_graph_params p) … nxt)〉 →
   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
    return st' →
 ∃prf'.
 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
  (sigma_state_pc … gss st prf)
  (sigma_state_pc … gss st' prf').
 bool_to_Prop (taaf_non_empty … taf).
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
#nxt #prf #EQfetch
whd in match eval_state; normalize nodelta >EQfetch
>m_return_bind >m_return_bind
whd in match eval_statement_advance; normalize nodelta
whd in match goto; normalize nodelta
#H lapply (err_eq_from_io ????? H) -H
#H @('bind_inversion H) #pc'
@('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
#H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
#EQ destruct(EQ)
>(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
#EQ1 #EQ2 destruct
cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
normalize nodelta ** #prf' #EQpc_of_label' *
#EQfetch'
-H
%
[ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3
  #H4 %{H3} %{H1 H4} ]
%{(taaf_step … (taa_base …) …) I}
[ whd whd in ⊢ (??%?); >EQfetch' %
| whd whd in match eval_state; normalize nodelta
  >EQfetch' >m_return_bind >m_return_bind
  whd in match eval_statement_advance; whd in match goto;
  normalize nodelta >pc_block_sigma_commute >EQpc_of_label'
  >m_return_bind %
]
qed.

lemma eval_cond_ok :
∀p,p',graph_prog.
let lin_prog ≝ linearise p graph_prog in
∀stack_sizes.
∀sigma.good_sigma p graph_prog sigma → 
∀gss : good_state_sigma p p' graph_prog sigma.
∀st,st',f,fn,a,ltrue,lfalse.
∀prf : well_formed_state_pc … gss st.
 fetch_statement (make_sem_graph_params p p') …
  (globalenv_noinit ? graph_prog) (pc … st) =
    return 〈f, fn,  sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 →
 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
  return st' →
as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes))
  st' →
∃prf'.
∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
(sigma_state_pc … gss st prf)
(sigma_state_pc … gss st' prf').
bool_to_Prop (taaf_non_empty … taf).
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
#a #ltrue #lfalse #prf #EQfetch
whd in match eval_state; normalize nodelta >EQfetch
>m_return_bind >m_return_bind
whd in match eval_statement_advance; normalize nodelta
#H @('bind_inversion (err_eq_from_io ????? H))
@bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
#bv #bv_no_pc #EQretrieve
cut
  (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a =
    return sigma_beval p p' graph_prog sigma bv prf')
[ @acca_retrieve_commute assumption ]
* #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve'
-H #H @('bind_inversion H) *
#EQbool normalize nodelta -H
[ whd in match goto; normalize nodelta
  #H @('bind_inversion H) -H #pc'
  @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
  #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
  #EQ destruct(EQ)
  >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
  #EQ1 #EQ2 destruct
| whd in ⊢ (??%%→?);
  #EQ destruct(EQ)
]
#ncost
cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' **
#EQfetch' #nxt_spec
% [1,3,5,7: @hide_prf
  cases st in prf prf' prf'';
  -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5
  %{H3} %{H1} assumption ]
%{(taaf_step_jump … (taa_base …) …) I}
[1,4,7,10: whd
  >(as_label_sigma_commute … good) assumption
|2,5,8,11: whd whd in ⊢ (??%?);
  >EQfetch' %
|*: whd whd in match eval_state; normalize nodelta >EQfetch'
  >m_return_bind >m_return_bind
  whd in match eval_statement_advance; normalize nodelta >EQretrieve'
  >m_return_bind >EQbool >m_return_bind normalize nodelta
  [1,2: whd in match goto; normalize nodelta
    >pc_block_sigma_commute >EQpc_of_label' %
  |3: whd in match next; normalize nodelta >nxt_spec %
  |4: whd in match goto; normalize nodelta
    >pc_block_sigma_commute >nxt_spec %
  ]
]
qed.

lemma eval_return_ok :
∀p,p',graph_prog.
let lin_prog ≝ linearise p graph_prog in
∀stack_sizes.
∀sigma.∀good : good_sigma p graph_prog sigma.
∀gss : good_state_sigma p p' graph_prog sigma.
∀st,st',f,fn.
∀prf : well_formed_state_pc … gss st.
 fetch_statement (make_sem_graph_params p p') …
  (globalenv_noinit ? graph_prog) (pc … st) =
    return 〈f, fn,  final … (RETURN (mk_graph_params p) … )〉 →
 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
  return st' →
joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes)
  (sigma_state_pc … st prf) = Some ? cl_return ∧
∃prf'.
∃st2_after_ret.
∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
st2_after_ret
(sigma_state_pc … gss st' prf').
(if taaf_non_empty … taf then
  ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes))
    st2_after_ret
 else True) ∧
eval_state … (ev_genv …  (lin_prog_params … (linearise … graph_prog) stack_sizes))
  (sigma_state_pc … st prf) =
return st2_after_ret ∧
ret_rel … (linearise_status_rel … gss good) st' st2_after_ret.
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
#prf #EQfetch
whd in match eval_state; normalize nodelta >EQfetch
>m_return_bind >m_return_bind
whd in match eval_statement_advance; normalize nodelta
#H lapply (err_eq_from_io ????? H) -H
#H @('bind_inversion H) -H #st1' #EQpop
cut (∃prf'.
  (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes))
    f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf)))
   = return sigma_state_pc … gss st1' prf')
[ @pop_frame_commute assumption ]
* #prf' #EQpop' >m_bind_bind
#H @('bind_inversion H) ** #call_i #call_fn
* [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta
#EQfetch_ret -H
whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc
cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
#_ normalize nodelta #EQfetch'
cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret)
normalize nodelta
#all_labels_in
* #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label']
% [1,3: whd in match joint_classify; normalize nodelta
  >EQfetch' >m_return_bind % ]
% [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ]
[ % [2: %{(taaf_base …)} |]
  % [ %{I} ]
  [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta
    whd in match eval_return; normalize nodelta
    >EQpop' >m_return_bind
    whd in match next_of_pc; normalize nodelta
    >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta
    >nxt_spec %
  | * #s1_pre #s1_call
    cases (joint_classify_call … s1_call)
    * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl
    * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
    * #s2_pre #s2_call
    whd in ⊢ (%→?); >EQfetch_call * #EQ #_
    * #s1_pre_prf #EQpc_s2_pre
    whd >EQpc_s2_pre
    <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
    >EQfetch_ret' % [ % | >nxt_spec % ]
  ]
| % [2: %{(taaf_step … (taa_base …) …)} |*:]
  [3: % [ % normalize nodelta ]
    [2: >EQfetch' in ⊢ (??%?);
      >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      normalize nodelta
      whd in match eval_return; normalize nodelta
      >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      whd in match next_of_pc; normalize nodelta
      >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      whd in match next; normalize nodelta %
    |1: normalize nodelta %* #H @H -H
      whd in ⊢ (??%?); >nxt_spec %
    |3: * #s1_pre #s1_call
      cases (joint_classify_call … s1_call)
      * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl
      * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
      * #s2_pre #s2_call
      whd in ⊢ (%→?); >EQfetch_call * #EQ #_
      * #s1_pre_prf #EQpc_s2_pre
      whd >EQpc_s2_pre
      <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
      >EQfetch_ret' %%
    ]
  |1: whd whd in ⊢ (??%?); >nxt_spec %
  |2: whd whd in match eval_state; normalize nodelta
    >nxt_spec >m_return_bind >m_return_bind
    whd in match eval_statement_advance; whd in match goto; normalize nodelta
    whd in match (pc_block ?); >pc_block_sigma_commute
    >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); %
  |*:
  ]
]
qed.

 
lemma eval_tailcall_ok :
∀p,p',graph_prog.
let lin_prog ≝ linearise p graph_prog in
∀stack_sizes.
∀sigma.good_sigma p graph_prog sigma → 
∀gss : good_state_sigma p p' graph_prog sigma.
∀st,st',f,fn,fl,called,args.
∀prf : well_formed_state_pc … gss st.
 fetch_statement (make_sem_graph_params p p') …
  (globalenv_noinit ? graph_prog) (pc … st) =
    return 〈f, fn,  final … (TAILCALL (mk_graph_params p) … fl called args)〉 →
 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
  return st' →
  let st2_pre_call ≝ sigma_state_pc … gss st prf in
  ∃is_tailcall, is_tailcall'.
  ∃prf'.
  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
  joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» =
  joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧
  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
    st2_pre_call = return st2_after_call.
#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args 
#prf #fetch_spec 
cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) *
normalize nodelta #lin_fetch_spec
whd in match eval_state; normalize nodelta >fetch_spec
>m_return_bind whd in match eval_statement_no_pc; normalize nodelta
>m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; 
normalize nodelta @('bind_inversion) #bl #bl_spec
lapply (err_eq_from_io ????? bl_spec) -bl_spec
whd in match set_no_pc; normalize nodelta #bl_spec
cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 
            bl_spec) * #lin_bl_spec @('bind_inversion)
* #f1 #fn1 cases fn1 normalize nodelta -fn1
[2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion)
    #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_
    whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
#fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) -fn1_spec #fn1_spec
generalize in match (fetch_function_transf … graph_prog …
      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
      … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
      #lin_fn1_spec
whd in match eval_internal_call; normalize nodelta
#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
#st1 #H @('bind_inversion H) -H #dim_s #dim_s_spec 
#H @('bind_inversion H) -H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?); 
#EQ1 #EQ2 destruct %
[ @hide_prf | % [@hide_prf]]
[1,2: whd in match joint_classify; normalize nodelta [>fetch_spec | >lin_fetch_spec]
      >m_return_bind normalize nodelta whd in match joint_classify_final;
      normalize nodelta [>bl_spec|>lin_bl_spec] >m_return_bind 
      [>fn1_spec|>lin_fn1_spec] % 
| cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec
  cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2) 
  #wf_all_st2 #all_st2_spec 
  cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc
  #pc_spec
  %
  [ @hide_prf % 
    [ % [@(proj1 … (proj1 … prf)) | @(wf_pc)] 
    | @(wf_all_st2) 
    ]
  | %
    [ whd in match joint_tailcall_ident; normalize nodelta
      >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
      >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
      normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
      whd in match fetch_internal_function; normalize nodelta
      >fn1_spec >lin_fn1_spec %
    | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      normalize nodelta >m_return_bind in ⊢ (??%?);
      >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
      >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %]
      >pc_spec %
    ]
  ]
]
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 linearise_ok:
 ∀p,p',graph_prog.
  let lin_prog ≝ linearise ? graph_prog in
 ∀stack_sizes.
 (∀sigma.good_state_sigma p p' graph_prog sigma) →
   ex_Type1 … (λR.
   status_simulation
    (graph_abstract_status p p' graph_prog stack_sizes)
    (lin_abstract_status p p' lin_prog stack_sizes) R).
 #p #p' #graph_prog
 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
 cut (∀fn.good_local_sigma … (sigma fn))
  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
 #good
 #stack_sizes
 #gss lapply (gss sigma) -gss #gss
 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
whd in match graph_abstract_status;
whd in match lin_abstract_status;
whd in match graph_prog_params;
whd in match lin_prog_params;
normalize nodelta
whd
whd in ⊢ (%→%→%→?);
whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
whd in ⊢ (?%→?%→?%→?);
#st1 #st1' #st2
whd in ⊢ (%→?);
change with
  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
#EQeval
@('bind_inversion EQeval)
** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
#_ * #prf #EQst2
cases stmt in EQfetch; -stmt
[ @cond_call_other
  [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ]
normalize nodelta
#EQfetch
change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
[ (* COND *)
  whd in match joint_classify; normalize nodelta;
  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
  normalize nodelta
  #ncost
  cases (eval_cond_ok … good … prf EQfetch EQeval ncost)
  #prf' * #taf #taf_ne
  destruct(EQst2)
  % [2: %{taf} |*:]
  >taf_ne normalize nodelta
  % [ %{I} %{prf'} % ]
  whd >(as_label_sigma_commute … good) %
|  (* CALL *)
  cases (eval_call_ok … good … prf EQfetch EQeval)
  #is_call * #is_call' *
  #prf' * #eq_call #EQeval'
  destruct(EQst2)
  >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
  #ignore %{«?, is_call'»}
  % [ %{eq_call} %{prf} % ]
  % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
  whd >(as_label_sigma_commute … good) %
| (* SEQ *)
  whd in match joint_classify; normalize nodelta;
  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
  normalize nodelta
  whd in match joint_classify_step; normalize nodelta
  >no_call_other [2: assumption ] normalize nodelta
  cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ]
  #prf' * #taf #taf_ne
  destruct(EQst2)
  % [2: %{taf} |*:]
  >taf_ne normalize nodelta % [ %{I} ]
  [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
| (* FIN *) cases s in EQfetch;
  [ (* GOTO *) #lbl #EQfetch
    whd in match joint_classify; normalize nodelta;
    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    normalize nodelta
    cases (eval_goto_ok … good … prf EQfetch EQeval)
    #prf' * #taf #taf_ne
    destruct(EQst2)
    % [2: %{taf} |*:]
    >taf_ne normalize nodelta % [ %{I} ]
    [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
  | (* RETURN *) #EQfetch
    whd in match joint_classify; normalize nodelta;
    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    normalize nodelta
    cases (eval_return_ok … good … prf EQfetch EQeval)
    #is_ret' *
    #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
    destruct(EQst2)
    % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:]
    % [2: whd >(as_label_sigma_commute … good) % ]
    %{ret_prf}
    % [2: %{prf'} % ]
    %{EQeval'}
    %{taf_prf is_ret'}
  | (* TAILCALL *) #fl #called #args #EQfetch
    cases (eval_tailcall_ok … good … prf EQfetch EQeval)
    #is_tailcall * #is_tailcall' *
    #prf' * #eq_call #EQeval'
    destruct(EQst2)
    >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    #ignore %{«?, is_tailcall'»}
    %{eq_call}
    % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
    whd >(as_label_sigma_commute … good) %
  ]
]
qed.