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

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

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

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

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

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

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

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

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

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

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

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

definition sigma_beval_opt :
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ) →
  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).
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ) →
  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_pop_commute :
 ∀p,p',graph_prog,sigma,is,bv,is'.
 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
 is_pop is = return 〈bv, is'〉 →
 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
cases daemon qed.

definition well_formed_mem :
 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
  ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ) →
 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 beloadv_sigma_commute:
∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
beloadv m ptr = return bv → 
∃ prf2.
beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr = 
               return sigma_beval p p' graph_prog sigma bv prf2.
#p #p' #graph_prog #sigma #m #ptr #bv #prf1
whd in match beloadv in ⊢ (%→?); normalize nodelta
whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta
@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
#block_id_ok
@Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
#zh
@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
#zl #EQ whd in EQ : (???%); destruct(EQ)
% [ @(prf1 ?? block_id_ok zh zl) ]
whd in match beloadv; normalize nodelta
whd in match do_if_in_bounds; normalize nodelta
@Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption]
#block_id_lin_ok
@Zleb_elim_Type0 normalize nodelta 
[ 
| * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta

lemma bestorev_sigma_commute :
∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
bestorev m ptr bv = return m' → 
∃prf3.
bestorev (sigma_mem p p' graph_prog sigma m prf1) 
          ptr 
          (sigma_beval p p' graph_prog sigma bv prf2)
=
return (sigma_mem p p' graph_prog sigma m' prf3).
cases daemon qed.

record good_sem_state_sigma
  (p : unserialized_params)
  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    graph_prog i) → 
      label → option ℕ) : 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 : 
  ∀reg,ptr.
  load_sp (make_sem_graph_params p p') reg = return ptr →
  ∃prf.
  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
; 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 : ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ).
 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 : ((Σi.is_internal_function_of_program … graph_prog i) → 
    code_point (mk_graph_params p) → option ℕ).
 ∀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 … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))
  (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))
  (carry … st)
  (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf)))
  (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)).


(*
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 : ((Σi.is_internal_function_of_program … graph_prog i) → 
    label → option ℕ).
∀pc.
∀prf : well_formed_pc p p' graph_prog sigma pc.
program_counter ≝ 
λp,p',graph_prog,sigma,st.opt_safe ….
 
lemma sigma_pc_ok:
  ∀p,p',graph_prog.
  ∀sigma.
   ∀pc.
    ∀prf:well_formed_pc p p' graph_prog sigma pc.
    sigma_pc_opt p p' graph_prog sigma pc =
    Some … (sigma_pc p p' graph_prog sigma pc prf).
    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.

definition 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 (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 pc' ≝ sigma_pc … (proj1 … prf) in
 let st' ≝ sigma_state … (proj2 … prf) in
 mk_state_pc ? st' pc'.

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

lemma 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'.
  cases daemon qed.

(*
inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
 | isMemberHead : ∀ tl.isMember A x (x :: tl) 
 | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
(* 
definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl → 
      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
    @(isMemberTail ? x y l tl l_spec tl_member)
    qed.
  *)             

let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝ 
match l with [ nil ⇒ λprf : l = nil ?.nil ?
             | cons x tl ⇒ λprf : l = cons ? x tl.
              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
             ] (refl …).
@hide_prf
>prf
[ %1
| %2 assumption
] qed. 
              (f x (isMemberHead A x l tl prf)) ::   
              ext_map A B tl (lift_f_tail A B l tl x prf f) ] 
              (refl ? l).
*)

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 ?.∀bv,r,r',prf1,prf1'.
  store … a bv r = return r' → 
  ∃prf2.
  store ??? a
    (sigma_beval p p' graph_prog sigma bv prf1')
    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.

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.∀r,bv,prf1.
  retrieve … r a = return bv → 
  ∃prf2.
  retrieve … (sigma_regs … gsss r prf1) a
     = return sigma_beval p p' graph_prog sigma bv prf2.
  
record good_state_sigma
  (p : unserialized_params)
  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    graph_prog i) → 
      label → option ℕ)
: 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_

}.

lemma store_commute :
  ∀p,p',graph_prog,sigma.
  ∀X : ? → Type[0].
  ∀store.
  ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 
  ∀H : helper_def_store__commute … gsss store.
  ∀a : X p.∀bv,st,st',prf1,prf1'.
  helper_def_store ? store … a bv st = return st' → 
  ∃prf2.
  helper_def_store ? store … a
    (sigma_beval p p' graph_prog sigma bv prf1')
    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
cases daemon 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 .∀st,bv,prf1.
 helper_def_retrieve ? retrieve … st a = return bv →
 ∃prf2.
     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
     return sigma_beval p p' graph_prog sigma bv prf2.
cases daemon 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).*)
  
    
lemma acca_store_commute :
  ∀p,p',graph_prog,sigma.
  ∀gss : good_state_sigma p p' graph_prog sigma.
  ∀a,bv,st,st',prf1,prf1'.
  acca_store ?? (p' ?) a bv st = return st' → 
  ∃prf2.
  acca_store ?? (p' ?) 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,a,bv.?.
* #frms #is #carry #regs #m
* #frms' #is' #carry' #regs' #m'
*** #frms_ok #is_ok #regs_ok #mem_ok
#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
elim (acca_store__commute … gss … EQ1)
[ #prf2 #EQ2
  % [ whd /4 by conj/ ]
  change with (! r ← ? ; ? = ?) >EQ2
  whd in match (sigma_state ???????); normalize nodelta
   >m_return_bind


st,st',prf1,prf2,prf3.?.


#p #p' #
(*
; acca_store_wf :  ∀a,bv,st,st'.
  sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → 
  acca_store ?? (p' ?) a bv st = return st' → 
  well_formed_state st → well_formed_state st'

; acca_retrieve_wf :  ∀a,st,bv.
  acca_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; acca_arg_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  acca_arg_retrieve ?? (p' ?) st a = return bv → 
  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; acca_arg_retrieve_wf :  ∀a,st,bv.
  acca_arg_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; accb_store_ok :
  ∀a,bv,bv',st,st',prf1,prf2.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  accb_store ?? (p' ?) a bv st = return st' → 
  accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
; accb_store_wf :  ∀a,bv,bv',st,st'.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  accb_store ?? (p' ?) a bv st = return st' → 
  well_formed_state st → well_formed_state st'

; accb_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  accb_retrieve ?? (p' ?) st a = return bv → 
  accb_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; accb_retrieve_wf :  ∀a,st,bv.
  accb_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; accb_arg_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  acca_arg_retrieve ?? (p' ?) st a = return bv → 
  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; accb_arg_retrieve_wf :  ∀a,st,bv.
  accb_arg_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?


; dpl_store_ok :
  ∀a,bv,bv',st,st',prf1,prf2.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  dpl_store ?? (p' ?) a bv st = return st' → 
  dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
; dpl_store_wf :  ∀a,bv,bv',st,st'.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  dpl_store ?? (p' ?) a bv st = return st' → 
  well_formed_state st → well_formed_state st'

; dpl_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  dpl_retrieve ?? (p' ?) st a = return bv → 
  dpl_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; dpl_retrieve_wf :  ∀a,st,bv.
  dpl_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; dpl_arg_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  acca_arg_retrieve ?? (p' ?) st a = return bv → 
  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; dpl_arg_retrieve_wf :  ∀a,st,bv.
  dpl_arg_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?


; dph_store_ok :
  ∀a,bv,bv',st,st',prf1,prf2.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  dph_store ?? (p' ?) a bv st = return st' → 
  dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
; dph_store_wf :  ∀a,bv,bv',st,st'.
  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
  dph_store ?? (p' ?) a bv st = return st' → 
  well_formed_state st → well_formed_state st'

; dph_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  dph_retrieve ?? (p' ?) st a = return bv → 
  dph_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; dph_retrieve_wf :  ∀a,st,bv.
  dph_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; dph_arg_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  acca_arg_retrieve ?? (p' ?) st a = return bv → 
  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; dph_arg_retrieve_wf :  ∀a,st,bv.
  dph_arg_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?


; snd_arg_retrieve_ok :
  ∀a,st,bv,prf1,prf2.
  snd_arg_retrieve ?? (p' ?) st a = return bv → 
  snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
  return sigma_beval p p' graph_prog sigma bv prf2
; snd_arg_retrieve_wf :  ∀a,st,bv.
  snd_arg_retrieve ?? (p' ?) st a = return bv → 
  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?

; pair_reg_move_ok :
  ∀mv,st1,st2,prf1,prf2.
  pair_reg_move ?? (p' ?) st1 mv = return st2 → 
  pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv =
    return sigma_state st2 prf2
; pair_reg_move_wf :
  ∀mv,st1,st2.
  pair_reg_move ?? (p' ?) st1 mv = return st2 → 
  well_formed_state st1 → well_formed_state st2

; allocate_locals_ok :
  ∀l,st1,prf1,prf2.
  allocate_locals ?? (p' ?) l (sigma_state st1 prf1) =
    sigma_state (allocate_locals ?? (p' ?) l st1) prf2
; allocate_locals_wf :
  ∀l,st1.
  well_formed_state st1 →
    well_formed_state (allocate_locals ?? (p' ?) l st1)

; save_frame_ok : 
  ∀dest,st1,st2,prf1,prf2.
  save_frame ?? (p' ?) dest st1 = return st2 →
  let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1))
    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 
  save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2
; save_frame_wf : 
  ∀dest,st1,st2.
  save_frame ?? (p' ?) dest st1 = return st2 →
  (well_formed_pc p p' graph_prog sigma (pc … st1) ∧
   well_formed_state st1) → well_formed_state st2

; eval_ext_seq_ok :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀ext,fn,st1,st2,prf1,prf2.
  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    ext fn st1 = return st2 →
  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2
; eval_ext_seq_wf :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀ext,fn,st1,st2.
  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    ext fn st1 = return st2 →
  well_formed_state st1 → well_formed_state st2

; setup_call_ok : 
  ∀ n , parsT, call_args , st1 , st2 , prf1, prf2.
  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
  setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) = 
  return (sigma_state st2 prf2)
; setup_call_wf :
  ∀ n , parsT, call_args , st1 , st2.
  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
  well_formed_state st1 → well_formed_state st2
  
; fetch_external_args_ok : (* 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 st1 prf1) call_args
; fetch_external_args_wf : 
  ∀ex_fun,st1,call_args.
  well_formed_state st1 → ∃ l.
  fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l
  
; set_result_ok :
  ∀ l , call_dest , st1 , st2 , prf1 , prf2 .
  set_result ?? (p' ?) l call_dest st1 = return st2 → 
  set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) = 
  return (sigma_state st2 prf2)
; set_result_wf :
  ∀ l , call_dest , st1 , st2  .
  set_result ?? (p' ?) l call_dest st1 = return st2 → 
  well_formed_state st1 → well_formed_state st2  
  
; read_result_ok :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀call_dest , st1 , prf1, l1.
  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    call_dest st1 = return l1 →
  ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    call_dest (sigma_state st1 prf1) = return opt_safe … prf
; read_result_wf :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀call_dest , st1 , l1.
  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    call_dest st1 = return l1 →
  well_formed_state st1 → 
  m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?
  
; pop_frame_ok :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀ st1 , prf1, curr_id ,st2, prf2.
  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 
            curr_id st1 = return st2 →
 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
 let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in
  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
            (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) =
            return mk_state_pc ? st2' pc' 
; pop_frame_wf :
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
  let stack_sizes' ≝
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
  ∀ st1, curr_id ,st2.
  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 
            curr_id st1 = return st2 → 
  well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧ 
      well_formed_state (st_no_pc ? st2)
}.

(* 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 res_eq_from_opt :
  ∀A,m,v.res_to_opt A m = return v → m = return v. 
#A * #x #v normalize #EQ destruct % 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 bind_opt_inversion:
  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
  (! x ← f ; g x = Some … y) →
  ∃x. (f = Some … x) ∧ (g x = Some … y).
#A #B #f #g #y cases f normalize 
[ #H destruct (H)
| #a #e %{a} /2 by conj/
] qed.

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

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

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

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

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


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

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


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

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


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

.. sigma_int_funct_of_block



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

lemma opt_Exists_elim:
 ∀A:Type[0].∀P:A → Prop.
  ∀o:option A.
   opt_Exists A P o →
    ∃v:A. o = Some … v ∧ P v.
 #A #P * normalize /3/ *
qed.


lemma stmt_at_sigma_commute:
 ∀p,graph_prog,graph_fun,lbl,pt.
 let lin_prog ≝ linearise ? graph_prog in
 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
 ∀sigma.good_sigma p graph_prog sigma →
 sigma graph_fun lbl = return pt →
 ∀stmt.
   stmt_at …
    (joint_if_code ?? (if_of_function ?? graph_fun))  
    lbl = return stmt →
   stmt_at ??
    (joint_if_code ?? (if_of_function ?? lin_fun))
    pt = return (graph_to_lin_statement … stmt).  
 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
#sigma_entry_is_zero #lin_stmt_spec
lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
#EQlookup_stmt1 #H
elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt 
* #EQnth_opt_graph_stmt normalize nodelta
* #optEQlbl_optlbl_graph_stmt #next_spec
whd in match (stmt_at ????) in ⊢ (% → ?);
normalize nodelta
>EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
whd in match (stmt_at ????); > EQnth_opt_graph_stmt 
normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
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 // *)

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

lemma point_of_pc_sigma_commute :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀sigma,pc,fn,n.
  ∀prf : well_formed_pc p p' graph_prog sigma pc.
 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return 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 #fn #n #prf #EQfetch #EQsigma
whd in match sigma_pc; normalize nodelta
@opt_safe_elim #pc' whd in match sigma_pc_opt;
normalize nodelta >EQfetch >m_return_bind >EQsigma
>m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
change with (point_of_offset ??? = ?) @point_of_offset_of_point
qed.

definition linearise_status_rel:
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
 let stack_sizes' ≝
  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    ? graph_prog stack_sizes in
 ∀sigma,gss.
 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) (proj1 … prf))
    (* sim_final ≝ *) ?.
#st1 #st2 * #prf #EQ2
%
whd in ⊢ (%→%);
#H lapply (opt_to_opt_safe … H)
@opt_safe_elim -H
#res #_
#H lapply (res_eq_from_opt ??? H) -H
cases daemon
(*#H elim (bind_inversion ????? H) in ⊢ ?;
* #f #stmt *
whd in ⊢ (??%?→?);*)
qed.

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

lemma 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 eval_seq_no_pc_sigma_commute :
 ∀p,p',graph_prog.
 let lin_prog ≝ linearise p graph_prog in
 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
 let stack_sizes' ≝
  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    ? graph_prog stack_sizes in
 ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
 ∀fn,st,stmt,st'.
 ∀prf : well_formed_state … gss st.∀prf'.
  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
   fn st stmt = return st' →
  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
  return sigma_state … gss st' prf'.
  #p #p' #graph_prog #stack_sizes #sigma #gss
  #fn #st #stmt
  #st' #prf #prf'
  whd in match eval_seq_no_pc;
  cases stmt normalize nodelta
  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //
  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
    >(pair_reg_move_ok ?????????? H) [% | skip]
  | (* POP *)
    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
    * #val #st1 * #vals_spec #H
    cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
    #wf_st1 
    lapply(acca_store_wf ????????? H wf_st1)
    * #_ #sigma_val_spec
    lapply vals_spec -vals_spec
    whd in match pop; normalize nodelta
    #H1 elim (bind_inversion ????? H1) -H1 * #g_bev #g_is * #ispop_spec
    whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*)
    lapply ispop_spec -ispop_spec
    whd in match is_pop; normalize nodelta
    cases (istack ? st) normalize nodelta
    [ #ABS whd in ABS : (???%); destruct(ABS)
    | #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1)
      cases (istack ? (sigma_state … st prf)) normalize nodelta
    
    lapply (acca_store_ok ?????????????? H)

    
     -val_spec * #bv #is * #bv_is_spec
    #EQ whd in EQ : (??%%); destruct(EQ) 
    whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec;
    inversion (istack ? st) in bv_is_spec; 
    [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS)
    | #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ)
    lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H)
 
  @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
    #H
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
 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
 let graph_stack_sizes ≝
  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    ? graph_prog lin_stack_sizes in
 (∀sigma.good_sigma_state p p' graph_prog sigma) →
   ex_Type1 … (λR.
   status_simulation
    (graph_abstract_status p p' graph_prog graph_stack_sizes)
    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
 #p #p' #graph_prog
 cases (linearise_spec … graph_prog) #sigma #good
 #lin_stack_sizes
 #gss lapply (gss sigma) -gss #gss
 %{(linearise_status_rel p p' graph_prog lin_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 ???) ?? = ? → ?)
whd in match eval_state in ⊢ (%→?); normalize nodelta
change with (Σi.is_internal_function_of_program ? graph_prog i) in
match (Sig ??) in ⊢ (%→?);
letin globals ≝ (prog_var_names ?? graph_prog)
change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
  match (fetch_statement ?????) in ⊢ (%→?);
#ex
cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
#EQfetch
cases (bind_inversion ????? EQfetch)
#f_id * #H lapply (opt_eq_from_res ???? H) -H
#EQfunc_of_block
#H elim (bind_inversion ????? H) -H #stmt' *
#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
whd in ⊢ (??%%→?); #EQ destruct(EQ)
#EQeval
cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
#entry_0
#good_local
* * #wf_pc #wf_state #EQst2
generalize in match wf_pc in ⊢ ?;
whd in ⊢ (%→?);
inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
#lin_pc 
whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
elim (good_local … EQsigma) -good_local
#stmt' *
change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
*
#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
letin lin_prog ≝ (linearise … graph_prog) 
lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
destruct(EQst2)
whd in match eval_state in ⊢ (???%→?); normalize nodelta
letin st2 ≝ (sigma_state_pc ????? st1 ?)
>(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
>m_return_bind in ⊢ (%→?);
#ex'
(* resolve classifier *)
whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
>EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
normalize nodelta
cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
[ *
  [ #stmt #nxt
    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
    whd in match eval_statement in ⊢ (%→?); normalize nodelta
    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
    #EQeval_no_pc #EQeval_pc
    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
        >m_return_bind
    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
    [14: #f #args #dest
    | #c
    | #lbl
    | #move_sig
    | #a
    | #a
    | #sy #sy_prf #dpl #dph
    | #op #a #b #arg1 #arg2
    | #op #a #arg
    | #op #a #arg1 #arg2 
    ||
    | #a #dpl #dph
    | #dpl #dph #a
    | #s_ext
    ]
    [ (* CALL *)
    |(*:*)
      normalize nodelta
      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
      whd in match eval_seq_pc; normalize nodelta
      #ex1
      cases next_spec
      [ #EQnext_sigma
        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
        normalize nodelta
        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
        | %
          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
          | whd in match eval_seq_pc in EQeval_pc;
            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
            destruct (EQeval_pc)
            whd in ⊢ (??%%);
            change with (sigma_pc ??????) in match
              (pc ? (sigma_state_pc ???????));
            whd in match (succ_pc ????) in ⊢ (??%%);
            whd in match (point_of_succ ???) in ⊢ (??%%);
            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
            whd in match sigma_pc in ⊢ (???%);
            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
            @opt_safe_elim #pc'
            >EQfunc_of_block >m_return_bind
            whd in match point_of_pc; normalize nodelta
            >point_of_offset_of_point
            >EQnext_sigma whd in ⊢ (??%?→?);
            whd in match pc_of_point; normalize nodelta
            #EQ destruct(EQ)
            >sigma_pblock_eq_lemma %
          ]
        ]
      | -next_spec #next_spec
        %
      
      
        whd in ⊢ (?→???%→?);
        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
  ] #next change with label in next;
| *
  [ #lbl
  | 
  | #fl #f #args
  ]
]
whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
normalize nodelta
whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
whd in match eval_statement in ⊢ (%→?); normalize nodelta
[ >m_return_bind in ⊢ (%→?);
  >m_return_bind in EQeval;



  (* common for all non-call seq *)
  >m_return_bind in ⊢ (%→?);
  whd in ⊢ (??%%→?); #EQ destruct(EQ)
  >m_return_bind in ⊢ (%→?);

  
  #ex1
lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))

whd in match (point_of_pc ???);
whd in match (point_of_succ ???);
whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
#pc' #H
elim (bind_opt_inversion ????? H) #fn * #EQbl
-H #H  
elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
#EQ destruct(EQ)
whd in match (succ_pc ????);
whd in match (point_of_succ ???);
change with (point_of_offset ???) in match (point_of_pc ???);
>point_of_offset_of_point
whd in match sigma_pc; normalize nodelta @opt_safe_elim
#pc' whd in match sigma_pc_opt; normalize nodelta

  
  
        whd in match (succ_pc ????);
                
        change with next in match (offset_of_point ???) in ⊢ (???%);
whd in fetch_statement_spec : (??()%);
cases cl in classified_st1_cl; -cl #classified_st1_cl whd
[4:
 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
 #sigma_entry_is_zero #sigma_spec
 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
 #related_lin_stm_graph_stm
 
 inversion (stmt_implicit_label ???)
 [ whd in match (opt_All ???); #stmt_implicit_spec #_
   letin st2_opt' ≝ (eval_state …
               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
               (sigma_state_pc … wf_st1))
   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
   normalize nodelta in st2_spec'; -st2_opt'
   %{st2'} %{(taaf_step … (taa_base …) …)}
   [ cases daemon (* TODO, together with the previous one? *)
   | @st2_spec' ]
   %[%] [%]
   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
     >m_return_bind
     (* Case analysis over the possible statements *)
     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
     XXXXXXXXXX siamo qua, caso GOTO e RETURN
   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
   ]
 | ....
qed.





[ *
  [ *
    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
    | letin C_POP        ≝ 0 in ⊢ ?; #a
    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2 
    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
    ]
  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
  ] #next change with label in next;
| *
  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
  | letin C_RETURN ≝ 0 in ⊢ ?; 
  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
  ]
]