Changeset 2484 for src/joint/lineariseProof.ma

Timestamp:

Nov 22, 2012, 6:40:31 PM (8 years ago)

Author:

piccolo

Message:

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File:

• src/joint/lineariseProof.ma (modified) (17 diffs)

src/joint/lineariseProof.ma

@@ -120 +120 @@
    ≠ None ….
 
-definition well_formed_status:
- ∀p,p',graph_prog.
+definition sigma_beval_opt :
+ ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
   ((Σi.is_internal_function_of_program … graph_prog i) → 
-    label → option ℕ) →
-  state_pc (make_sem_graph_params p p') → Prop ≝
- λp,p',prog,sigma,st.
- well_formed_pc p p' prog sigma (pc … st) ∧ ?.
-cases daemon (* TODO *)
-qed.
+    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 ….
 
 (* 
@@ -165 +171 @@
 λp,p',graph_prog,sigma,st.opt_safe ….
  
-lemma sigma_pc_of_status_ok:
+lemma sigma_pc_ok:
   ∀p,p',graph_prog.
   ∀sigma.
@@ -174 +180 @@
     #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
 
-definition sigma_state :
- ∀p.
- ∀p':∀F.sem_unserialized_params p F.
- ∀graph_prog.
-  ∀sigma.
-(*   let lin_prog ≝ linearise ? graph_prog in *)
-    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
-     well_formed_status p p' graph_prog sigma s →
-      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
-≝
- λp,p',graph_prog,sigma,s,prf.
- let pc' ≝ sigma_pc … (proj1 … prf) in
- mk_state_pc ? ? pc'.
- cases daemon (* TODO *) qed.
-
-lemma sigma_pc_commute:
- ∀p,p',graph_prog,sigma,st.
- ∀prf : well_formed_status p p' graph_prog sigma st.
- sigma_pc … (pc ? st) (proj1 … prf) =
- pc ? (sigma_state … st prf).
-#p #p' #prog #sigma #st #prf %
-qed.
-
-lemma res_eq_from_opt :
-  ∀A,m,v.res_to_opt A m = return v → m = return v. 
-#A * #x #v normalize #EQ destruct % qed.
-
 definition sigma_function_name :
  ∀p,graph_prog.
@@ -207 +186 @@
   (Σf.is_internal_function_of_program … lin_prog f) ≝
 λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
+
+record good_sigma_state (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_state : state (make_sem_graph_params p p') → Prop
+; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p')
+
+; acca_store_ok :
+  ∀a,bv,bv',st,st',prf1,prf2.
+  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
+  acca_store ?? (p' ?) a bv st = return st' → 
+  acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
+; acca_store_wf :  ∀a,bv,bv',st,st'.
+  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
+  acca_store ?? (p' ?) a bv st = return st' → 
+  well_formed_state st → well_formed_state st'
+
+; acca_retrieve_ok :
+  ∀a,st,bv,prf1,prf2.
+  acca_retrieve ?? (p' ?) st a = return bv → 
+  acca_retrieve ?? (p' ?) (sigma_state st prf1) a =
+  return sigma_beval p p' graph_prog sigma bv prf2
+; 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
+
+}.
+
+(* 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)
+*)
+
+definition well_formed_state_pc :
+ ∀p,p',graph_prog,sigma.
+  good_sigma_state p p' graph_prog sigma → 
+  state_pc (make_sem_graph_params p p') → Prop ≝
+ λp,p',prog,sigma,gss,st.
+ well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st.
+ 
+definition sigma_state_pc :
+ ∀p.
+ ∀p':∀F.sem_unserialized_params p F.
+ ∀graph_prog.
+  ∀sigma.
+(*   let lin_prog ≝ linearise ? graph_prog in *)
+  ∀gss : good_sigma_state 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 gss s →
+      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
+≝
+ λp,p',graph_prog,sigma,gss,s,prf.
+ let pc' ≝ sigma_pc … (proj1 … prf) in
+ let st' ≝ sigma_state … (proj2 … prf) in
+ mk_state_pc ? st' pc'.
+
+(*
+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:
@@ -358 +574 @@
 *)
 
-lemma int_funct_of_block_transf_commute:
+lemma int_funct_of_block_transf:
  ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
   ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
@@ -393 +609 @@
  >(sigma_pblock_eq_lemma … prf) #H
  lapply (opt_eq_from_res ???? H) -H #H
- >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
+ >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
  //
 qed.
@@ -457 +673 @@
 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.
@@ -470 +695 @@
     (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
- (*
+ #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 ????);
@@ -486 +730 @@
  #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
  <sigma_pc_commute >lin_lookup_ok // *)
- cases daemon
-qed.
 
 lemma fetch_statement_sigma_commute:
@@ -516 +758 @@
 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.
@@ -523 +781 @@
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
- ∀sigma.
+ ∀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,good.
+ ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
    mk_status_rel …
     (* sem_rel ≝ *) (λs1,s2.
-     ∃prf: well_formed_status p p' graph_prog sigma s1.
-      s2 = sigma_state … s1 prf)
+     ∃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_status p p' graph_prog sigma s1.
+      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
       pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
     (* sim_final ≝ *) ?.
@@ -544 +802 @@
 #res #_
 #H lapply (res_eq_from_opt ??? H) -H
-#H elim (bind_inversion ????? H)
+cases daemon
+(*#H elim (bind_inversion ????? H) in ⊢ ?;
 * #f #stmt *
-whd in ⊢ (??%?→?);
-cases daemon
+whd in ⊢ (??%?→?);*)
 qed.
-
-(* To be added to common/Globalenvs, it strenghtens
-   find_funct_ptr_transf *)
-(*   
-lemma
-  find_funct_ptr_transf_eq:
-    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
-    ∀b: block.
-    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
-     m_map ???
-      (transf …)
-      (find_funct_ptr ? (globalenv … iV p) b).
- #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
- [ cases daemon (* TODO in Globalenvs.ma *)
- | #f #H >(find_funct_ptr_transf A B … H) // ]
-qed.
-*)
-
-
-(*lemma fetch_function_sigma_commute:
- ∀p,p',graph_prog,sigma,st1.
- ∀prf:well_formed_status ??? sigma st1.
- let lin_prog ≝ linearise ? graph_prog in
-  fetch_function                
-   (lin_prog_params p p' lin_prog)
-   (globals (lin_prog_params p p' lin_prog))
-   (ev_genv (lin_prog_params p p' lin_prog))
-   (pc (lin_prog_params p p' lin_prog)
-    (linearise_status_fun p p' graph_prog sigma st1 prf))
- =
-  m_map …
-   (linearise_int_fun ??)
-   (fetch_function
-    (graph_prog_params p p' graph_prog)
-    (globals (graph_prog_params p p' graph_prog))
-    (ev_genv (graph_prog_params p p' graph_prog))
-    (pc (graph_prog_params p p' graph_prog) st1)).
-#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
-whd in match function_of_block; normalize nodelta
->(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
-cases (find_funct_ptr ???) // * //
-qed.
-*)
 
 lemma IO_bind_inversion:
@@ -603 +818 @@
 ] 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 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_sigma_state … 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'
+  cases daemon (*
+  whd in match eval_seq_no_pc;
+  cases stmt normalize nodelta
+  [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) //
+  | #mv_sig 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 err_eq_from_io : ∀O,I,X,m,v.
-  err_to_io O I X m = return v → m = return v.
-#O #I #X * #x #v normalize #EQ destruct % qed. 
 
 lemma linearise_ok:
@@ -626 +860 @@
   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
@@ -633 +868 @@
  cases (linearise_spec … graph_prog) #sigma #good
  #lin_stack_sizes
- %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
- whd whd in ⊢ (%→%→?);
- change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
- #st1 
- change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
- #st1'
- change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?)
- #st2
- #ex * #wfprf #rel_st1_st2
- whd in ex;
- change with
-  (eval_state
-    (make_sem_graph_params p p')
-    (prog_var_names ?? graph_prog)
-     ?
-    st1 = ?) in ex;
- whd in match eval_state in ex;
- normalize nodelta in ex;
- cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt
- change with (Σi.is_internal_function_of_program … graph_prog i) in fn; *
- change with (globalenv_noinit ? graph_prog) in
-  ⊢ (??(???%?)?→?);
-    match (ge ?? (ev_genv ?)) in ⊢ (%→?);
- st1'
+ #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 [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
->fetch_statement_spec 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
@@ -676 +1069 @@
    letin st2_opt' ≝ (eval_state …
                (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
-               (sigma_state … wf_st1))
+               (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'
@@ -695 +1088 @@
  | ....
 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
+  ]
+]