Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2528 r2529  
    2626  (∀F.sem_unserialized_params p F) →
    2727    ∀prog : joint_program (mk_graph_params p).
    28   ((Σi.is_internal_function_of_program … prog i) → ℕ) →
     28  (ident → option ℕ) →
    2929     abstract_status
    3030 ≝
     
    4040  (∀F.sem_unserialized_params p F) →
    4141    ∀prog : joint_program (mk_lin_params p).
    42   ((Σi.is_internal_function_of_program … prog i) → ℕ) →
     42  (ident → option ℕ) →
    4343     abstract_status
    4444 ≝
     
    9797*)
    9898
     99definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
     100  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) →
     101    label → option ℕ.
     102   
    99103definition sigma_pc_opt:
    100  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    101   ((Σi.is_internal_function_of_program … graph_prog i) →
    102     code_point (mk_graph_params p) → option ℕ) →
     104 ∀p,p'.∀graph_prog.
     105  sigma_map p graph_prog →
    103106   program_counter → option program_counter
    104107 ≝
     
    106109  let pars ≝ make_sem_graph_params p p' in
    107110  let ge ≝ globalenv_noinit … prog in
    108   ! f ← int_funct_of_block ? ge (pc_block pc) ;
    109   ! lin_point ← sigma f (point_of_pc ? pars pc) ;
    110   return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
     111  ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
     112  ! lin_point ← sigma fd (point_of_pc pars pc) ;
     113  return pc_of_point
     114  (make_sem_lin_params ? p') (pc_block pc) lin_point.
    111115
    112116definition well_formed_pc:
    113117 ∀p,p',graph_prog.
    114   ((Σi.is_internal_function_of_program … graph_prog i) →
    115     label → option ℕ) →
     118  sigma_map p graph_prog →
    116119   program_counter → Prop
    117120 ≝
     
    122125definition sigma_beval_opt :
    123126 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    124   ((Σi.is_internal_function_of_program … graph_prog i) →
    125     code_point (mk_graph_params p) → option ℕ) →
     127  sigma_map p graph_prog →
    126128  beval → option beval ≝
    127129λp,p',graph_prog,sigma,bv.
     
    138140definition sigma_is_opt :
    139141 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    140   ((Σi.is_internal_function_of_program … graph_prog i) →
    141     code_point (mk_graph_params p) → option ℕ) →
     142  sigma_map p graph_prog →
    142143  internal_stack → option internal_stack ≝
    143144λp,p',graph_prog,sigma,is.
     
    167168definition well_formed_mem :
    168169 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    169   ((Σi.is_internal_function_of_program … graph_prog i) →
    170     code_point (mk_graph_params p) → option ℕ) →
     170  sigma_map p graph_prog →
    171171 bemem → Prop ≝
    172172λp,p',graph_prog,sigma,m.
     
    311311  (p : unserialized_params)
    312312  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    313  (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    314     graph_prog i) →
    315       label → option ℕ) : Type[0] ≝
     313  (sigma : sigma_map p graph_prog) : Type[0] ≝
    316314{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
    317315; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
     
    340338definition well_formed_state :
    341339 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    342  ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    343     code_point (mk_graph_params p) → option ℕ).
     340 ∀sigma.
    344341 good_sem_state_sigma p p' graph_prog sigma →
    345342 state (make_sem_graph_params p p') → Prop ≝
     
    352349definition sigma_state :
    353350 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    354  ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    355     code_point (mk_graph_params p) → option ℕ).
     351 ∀sigma.
    356352 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    357353 ∀st : state (make_sem_graph_params p p').
     
    409405definition sigma_pc :
    410406∀p,p',graph_prog.
    411 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    412     label → option ℕ).
     407∀sigma.
    413408∀pc.
    414409∀prf : well_formed_pc p p' graph_prog sigma pc.
     
    447442 let st' ≝ sigma_state … (proj2 … prf) in
    448443 mk_state_pc ? st' pc'.
    449 
     444(*
    450445definition sigma_function_name :
    451446 ∀p,graph_prog.
     
    454449  (Σf.is_internal_function_of_program … lin_prog f) ≝
    455450λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    456 
     451*)
    457452lemma m_list_map_All_ok :
    458453  ∀M : MonadProps.∀X,Y,f,l.
     
    520515  (p : unserialized_params)
    521516  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    522  (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    523     graph_prog i) →
    524       label → option ℕ)
     517  (sigma : sigma_map p graph_prog)
    525518: Type[0] ≝
    526519{ gsss :> good_sem_state_sigma p p' graph_prog sigma
     
    557550; eval_ext_seq_commute :
    558551  let lin_prog ≝ linearise p graph_prog in
    559   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    560   let stack_sizes' ≝
    561    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    562      ? graph_prog stack_sizes in
    563   ∀ext,fn,st1,st2,prf1.
    564   eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    565     ext fn st1 = return st2 →
     552  ∀stack_sizes.
     553  ∀ext,i,fn,st1,st2,prf1.
     554  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     555    ext i fn st1 = return st2 →
    566556  ∃prf2.
    567557  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    568     ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     558    ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    569559   return sigma_state p p' graph_prog sigma gsss st2 prf2
    570560; setup_call_commute :
     
    586576; read_result_commute :
    587577  let lin_prog ≝ linearise p graph_prog in
    588   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    589   let stack_sizes' ≝
    590    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    591      ? graph_prog stack_sizes in
     578  ∀stack_sizes.
    592579  ∀call_dest , st1 , prf1, l1.
    593   read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     580  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    594581    call_dest st1 = return l1 →
    595582  ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
     
    598585; pop_frame_commute :
    599586  let lin_prog ≝ linearise p graph_prog in
    600   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    601   let stack_sizes' ≝
    602    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    603      ? graph_prog stack_sizes in
    604   ∀ st1 , prf1, curr_id ,st2.
    605   pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    606             curr_id st1 = return st2 →
     587  ∀stack_sizes.
     588  ∀ st1 , prf1, curr_id , curr_fn ,st2.
     589  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     590            curr_id curr_fn st1 = return st2 →
    607591 ∃prf2.
    608592 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
    609593 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
    610594  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    611             (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     595            curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    612596            return mk_state_pc ? st2' pc'
    613597}.
     
    672656λgss : good_state_sigma p p' graph_prog sigma.
    673657store_commute … gss (acca_store__commute … gss).
    674  
    675    
    676 lemma acca_store_commute :
    677   ∀p,p',graph_prog,sigma.
    678   ∀gss : good_state_sigma p p' graph_prog sigma.
    679   ∀a,bv,st,st',prf1,prf1'.
    680   acca_store ?? (p' ?) a bv st = return st' →
    681   ∃prf2.
    682   acca_store ?? (p' ?) a
    683     (sigma_beval p p' graph_prog sigma bv prf1')
    684     (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
    685 λp,p',graph_prog,sigma,gss,a,bv.?.
    686 * #frms #is #carry #regs #m
    687 * #frms' #is' #carry' #regs' #m'
    688 *** #frms_ok #is_ok #regs_ok #mem_ok
    689 #bv_ok #EQ1 elim (bind_inversion ????? EQ1)
    690 #regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    691 elim (acca_store__commute … gss … EQ1)
    692 [ #prf2 #EQ2
    693   % [ whd /4 by conj/ ]
    694   change with (! r ← ? ; ? = ?) >EQ2
    695   whd in match (sigma_state ???????); normalize nodelta
    696    >m_return_bind
    697 
    698 
    699 st,st',prf1,prf2,prf3.?.
    700 
    701 
    702 #p #p' #
     658
    703659*)
    704660
     
    729685#A * #x #v normalize #EQ destruct % qed.
    730686
     687(*
    731688lemma if_of_function_commute:
    732689 ∀p.
     
    739696 #p #graph_prog #graph_fun whd
    740697 @prog_if_of_function_transform % qed.
    741 
    742 lemma bind_opt_inversion:
    743   ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
    744   (! x ← f ; g x = Some … y) →
    745   ∃x. (f = Some … x) ∧ (g x = Some … y).
    746 #A #B #f #g #y cases f normalize
    747 [ #H destruct (H)
    748 | #a #e %{a} /2 by conj/
    749 ] qed.
     698*)
     699lemma bind_option_inversion_star:
     700  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     701  (∀x.f = Some … x → g x = Some … y → P) →
     702  (! x ← f ; g x = Some … y) → P.
     703#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
     704
     705interpretation "option bind inversion" 'bind_inversion =
     706  (bind_option_inversion_star ???????).
    750707
    751708lemma sigma_pblock_eq_lemma :
     
    758715 #p #p' #graph_prog #sigma #pc #prf
    759716 whd in match sigma_pc; normalize nodelta
    760  @opt_safe_elim #x #x_spec
    761  whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
    762  normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
    763  #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
     717 @opt_safe_elim #x @'bind_inversion * #i #fn #_
     718 @'bind_inversion #n #_ whd in ⊢ (??%?→?);
     719 #EQ destruct %
    764720qed.
    765721
     
    780736*)
    781737
     738(*
    782739lemma funct_of_block_transf :
    783740∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
     
    887844#A #B #progr #transf #bl #f #prf
    888845whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
    889 #H
    890 elim (bind_opt_inversion ??? ?? H) -H #x
    891 * #x_spec
     846@'bind_inversion #x #x_spec
    892847@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
    893848#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
     
    899854>(description_of_function_transf) [2: @x_prf ]
    900855>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
    901 
    902 
    903 lemma fetch_function_sigma_commute :
    904  ∀p,p',graph_prog.
    905  let lin_prog ≝ linearise p graph_prog in
    906  ∀sigma,pc_st,f.
    907   ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
    908  fetch_function … (globalenv_noinit … graph_prog) pc_st =
    909   return f
    910 → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
    911   return sigma_function_name … f.
    912  #p #p' #graph_prog #sigma #st #f #prf
     856*)
     857
     858axiom symbol_for_block_transf :
     859 ∀A,B,V,init.∀prog_in : program A V.
     860 ∀trans : ∀vars.A vars → B vars.
     861 let prog_out ≝ transform_program … prog_in trans in
     862 ∀bl, i.
     863 symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
     864 symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
     865
     866lemma fetch_function_transf :
     867 ∀A,B,V,init.∀prog_in : program A V.
     868 ∀trans : ∀vars.A vars → B vars.
     869 let prog_out ≝ transform_program … prog_in trans in
     870 ∀bl,i,f.
     871 fetch_function … (globalenv … init prog_in) bl =
     872  return 〈i, f〉
     873→ fetch_function … (globalenv … init prog_out) bl =
     874  return 〈i, trans … f〉.
     875#A #B #V #init #prog_in #trans #bl #i #f
    913876 whd in match fetch_function; normalize nodelta
    914  >(sigma_pblock_eq_lemma … prf) #H
    915  lapply (opt_eq_from_res ???? H) -H #H
    916  >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
    917  //
     877 #H lapply (opt_eq_from_res ???? H) -H
     878 @'bind_inversion #id #eq_symbol_for_block
     879 @'bind_inversion #fd #eq_find_funct
     880 whd in ⊢ (??%?→?); #EQ destruct(EQ)
     881 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
     882 >(find_funct_ptr_transf A B …  eq_find_funct) >m_return_bind %
     883qed.
     884
     885lemma bind_inversion_star : ∀X,Y.∀P : Prop.
     886∀m : res X.∀f : X → res Y.∀v : Y.
     887(∀x. m = return x → f x = return v → P) →
     888! x ← m ; f x = return v → P.
     889#X #Y #P #m #f #v #H #G
     890elim (bind_inversion ????? G) #x * @H qed.
     891
     892interpretation "res bind inversion" 'bind_inversion =
     893  (bind_inversion_star ???????).
     894
     895lemma fetch_internal_function_transf :
     896 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     897 ∀trans : ∀vars.A vars → B vars.
     898 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
     899 ∀bl,i,f.
     900 fetch_internal_function … (globalenv_noinit … prog_in) bl =
     901  return 〈i, f〉
     902→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
     903  return 〈i, trans … f〉.
     904#A #B #prog #trans #bl #i #f
     905 whd in match fetch_internal_function; normalize nodelta
     906 @'bind_inversion * #id * #fd normalize nodelta #EQfetch
     907 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     908 >(fetch_function_transf … EQfetch) %
    918909qed.
    919910 
     
    978969qed. *)
    979970
    980 lemma opt_Exists_elim:
    981  ∀A:Type[0].∀P:A → Prop.
    982   ∀o:option A.
    983    opt_Exists A P o →
    984     ∃v:A. o = Some … v ∧ P v.
    985  #A #P * normalize /3/ *
    986 qed.
    987 
    988 
    989971lemma stmt_at_sigma_commute:
    990  ∀p,graph_prog,graph_fun,lbl,pt.
    991  let lin_prog ≝ linearise ? graph_prog in
    992  let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
    993  ∀sigma.good_sigma p graph_prog sigma →
    994  sigma graph_fun lbl = return pt →
     972 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
     973 good_local_sigma p globals graph_code entry lin_code sigma →
     974 sigma lbl = return pt →
    995975 ∀stmt.
    996    stmt_at …
    997     (joint_if_code ?? (if_of_function ?? graph_fun)) 
     976   stmt_at … graph_code
    998977    lbl = return stmt →
    999    stmt_at ??
    1000     (joint_if_code ?? (if_of_function ?? lin_fun))
    1001     pt = return (graph_to_lin_statement … stmt). 
    1002  #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
    1003 cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
    1004 #sigma_entry_is_zero #lin_stmt_spec
    1005 lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
    1006 #EQlookup_stmt1 #H
    1007 elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
    1008 * #EQnth_opt_graph_stmt normalize nodelta
    1009 * #optEQlbl_optlbl_graph_stmt #next_spec
    1010 whd in match (stmt_at ????) in ⊢ (% → ?);
    1011 normalize nodelta
    1012 >EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
    1013 whd in match (stmt_at ????); > EQnth_opt_graph_stmt
    1014 normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
    1015 qed.
     978 stmt_at ?? lin_code
     979  pt = return graph_to_lin_statement … stmt ∧
     980  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
     981 match stmt with
     982 [ final stmt ⇒ True
     983 | sequential stmt nxt ⇒
     984   (sigma nxt = Some ? (S pt) ∨
     985    (stmt_at ?? lin_code
     986     (S pt) = return final (mk_lin_params p) … (GOTO … nxt)))
     987 ]. 
     988 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
     989 * #_ #lin_stmt_spec #prf
     990elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at
     991#All_succs_in #next_spec
     992#EQstmt_at_graph_stmt
     993#stmt >EQstmt_at
     994whd in ⊢ (??%%→?); #EQ destruct(EQ)
     995% [ % assumption ]
     996cases stmt in next_spec; -stmt normalize nodelta [2: // ]
     997#stmt #nxt
     998whd in match opt_All;
     999whd in match stmt_implicit_label;
     1000normalize nodelta //
     1001qed.
     1002 
    10161003(*
    10171004
     
    10361023 <sigma_pc_commute >lin_lookup_ok // *)
    10371024
    1038 lemma fetch_statement_sigma_commute:
    1039   ∀p,p',graph_prog,pc,fn,stmt.
     1025definition good_sigma :
     1026  ∀p.∀graph_prog : joint_program (mk_graph_params p).
     1027  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
     1028    label → option ℕ) → Prop ≝
     1029  λp,graph_prog,sigma.
     1030  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
     1031  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
     1032    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).
     1033
     1034lemma pc_of_label_sigma_commute :
     1035  ∀p,p',graph_prog,pc,lbl,i,fn.
    10401036  let lin_prog ≝ linearise ? graph_prog in
    10411037  ∀sigma.good_sigma p graph_prog sigma →
    10421038  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1043   fetch_statement ? (make_sem_graph_params p p') …
    1044     (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
    1045   fetch_statement ? (make_sem_lin_params p p') …
     1039  fetch_internal_function …
     1040    (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 →
     1041  let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in
     1042  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
     1043  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1044    (pc_block (sigma_pc … pc prf)) lbl =
     1045        return sigma_pc p p' graph_prog sigma pc' prf'.
     1046#p #p' #graph_prog #pc #lbl #i #fn
     1047#sigma #good cases (good fn) -good * #_ #all_labels_in
     1048#good #prf #fetchfn >lin_code_has_label #lbl_in
     1049whd in match pc_of_label; normalize nodelta
     1050>sigma_pblock_eq_lemma
     1051> (fetch_internal_function_transf … fetchfn) >m_return_bind
     1052inversion (point_of_label ????)
     1053[ (*
     1054  change with (If ? then with prf do ? else ? = ? → ?)
     1055  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
     1056  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
     1057| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
     1058  %
     1059  [ @hide_prf whd %
     1060  | whd in match sigma_pc; normalize nodelta
     1061    @opt_safe_elim #pc'
     1062  ]
     1063  whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
     1064  >point_of_pc_of_point
     1065  >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) %
     1066]
     1067qed.
     1068
     1069lemma graph_pc_of_label :
     1070  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
     1071  ∀globals,ge,bl,i_fn,lbl.
     1072  fetch_internal_function ? ge bl = return i_fn →
     1073  pc_of_label pars globals ge bl lbl =
     1074    OK ? (pc_of_point pars bl lbl).
     1075#p #p' #globals #ge #bl #fn #lbl #fetchfn
     1076whd in match pc_of_label; normalize nodelta
     1077>fetchfn %
     1078qed.
     1079
     1080lemma graph_succ_pc :
     1081  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
     1082  ∀pc,lbl.
     1083  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
     1084normalize //
     1085qed.
     1086
     1087lemma fetch_statement_sigma_commute:
     1088  ∀p,p',graph_prog,pc,f,fn,stmt.
     1089  let lin_prog ≝ linearise ? graph_prog in
     1090  ∀sigma.good_sigma p graph_prog sigma →
     1091  ∀prf : well_formed_pc p p' graph_prog sigma pc.
     1092  fetch_statement (make_sem_graph_params p p') …
     1093    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
     1094  fetch_statement (make_sem_lin_params p p') …
    10461095    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    1047     return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
    1048  #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
    1049  whd in match fetch_statement; normalize nodelta #H
    1050  cases (bind_inversion ????? H) #id * -H #fetchfn
    1051  >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
    1052  #H cases (bind_inversion ????? H) #fstmt * -H #H
    1053  lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
    1054  >(stmt_at_sigma_commute … good … H) [%]
    1055  whd in match sigma_pc; normalize nodelta
    1056  @opt_safe_elim #pc' #H
    1057  cases (bind_opt_inversion ????? H)
    1058  #i * #EQ1 -H #H
    1059  cases (bind_opt_inversion ????? H)
    1060  #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
    1061  whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
    1062  lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
    1063 qed.
     1096  return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧
     1097  All ? (λlbl.well_formed_pc p p' graph_prog sigma
     1098      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
     1099    (stmt_explicit_labels … stmt) ∧
     1100  match stmt with
     1101  [ sequential stmt nxt ⇒
     1102    ∃prf'.
     1103    let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1104    let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1105    (nxt_pc = sigma_nxt ∨
     1106     fetch_statement (make_sem_lin_params p p') …
     1107      (globalenv_noinit … lin_prog) nxt_pc =
     1108      return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     1109  | final stmt ⇒ True
     1110  ].
     1111#p #p' #graph_prog #pc #f #fn #stmt #sigma #good
     1112elim (good fn) * #_ #all_labels_in #good_local #wfprf
     1113#H
     1114elim (fetch_statement_inv … H)
     1115#fetchfn #graph_stmt
     1116whd in match fetch_statement; normalize nodelta
     1117>sigma_pblock_eq_lemma
     1118>(fetch_internal_function_transf … fetchfn) >m_return_bind
     1119whd in match sigma_pc; normalize nodelta @opt_safe_elim
     1120#lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta
     1121>fetchfn in ⊢ (%→?); >m_return_bind
     1122inversion (sigma ??)
     1123[ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     1124#lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1125cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) *
     1126#H1 #H2 #H3 % [ % ]
     1127[ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1128  >H1 %
     1129| @(All_mp … (All_append_r … H2)) #lbl #prf'
     1130 whd whd in match sigma_pc_opt; normalize nodelta
     1131 >fetchfn >m_return_bind >point_of_pc_of_point
     1132 >(opt_to_opt_safe … prf') % normalize
     1133 #ABS destruct(ABS)
     1134| cases stmt in H2 H3; normalize nodelta [2: // ]
     1135  -stmt #stmt #nxt * #next_in #_ #nxt_spec
     1136  % 
     1137  [ @hide_prf whd %
     1138  | @opt_safe_elim #pc'
     1139  ]
     1140  >graph_succ_pc whd in ⊢ (??%?→?);
     1141  >fetchfn normalize nodelta >point_of_pc_of_point
     1142  >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1143  cases nxt_spec
     1144  [ #EQsigma_nxt %1
     1145    whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta
     1146    >point_of_offset_of_point lapply next_in >EQsigma_nxt #N %
     1147  | #EQstmt_at_nxt %2
     1148    whd in match (succ_pc ???);
     1149    >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1150    whd in match point_of_pc;
     1151    normalize nodelta >point_of_offset_of_point >point_of_offset_of_point
     1152    whd in match (point_of_succ ???);
     1153    >EQstmt_at_nxt %
     1154  ]
     1155]
     1156qed. 
    10641157
    10651158lemma point_of_pc_sigma_commute :
    10661159 ∀p,p',graph_prog.
    10671160 let lin_prog ≝ linearise p graph_prog in
    1068  ∀sigma,pc,fn,n.
     1161 ∀sigma,pc,f,fn,n.
    10691162  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1070  int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn
    1071  sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
    1072  point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
    1073 #p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
     1163 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉
     1164 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
     1165 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     1166#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
    10741167whd in match sigma_pc; normalize nodelta
    10751168@opt_safe_elim #pc' whd in match sigma_pc_opt;
    10761169normalize nodelta >EQfetch >m_return_bind >EQsigma
    1077 >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1078 change with (point_of_offset ??? = ?) @point_of_offset_of_point
     1170whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1171@point_of_offset_of_point
    10791172qed.
    10801173
     
    10821175 ∀p,p',graph_prog.
    10831176 let lin_prog ≝ linearise p graph_prog in
    1084  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1085  let stack_sizes' ≝
    1086   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1087     ? graph_prog stack_sizes in
     1177 ∀stack_sizes.
    10881178 ∀sigma,gss.
    10891179 good_sigma p graph_prog sigma →
    10901180   status_rel
    1091     (graph_abstract_status p p' graph_prog stack_sizes')
     1181    (graph_abstract_status p p' graph_prog stack_sizes)
    10921182    (lin_abstract_status p p' lin_prog stack_sizes)
    10931183 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
     
    11141204
    11151205lemma IO_bind_inversion:
    1116   ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    1117   (! x ← f ; g x = return y) →
    1118   ∃x. (f = return x) ∧ (g x = return y).
    1119 #O #I #A #B #f #g #y cases f normalize
    1120 [ #o #f #H destruct
    1121 | #a #e %{a} /2 by conj/
    1122 | #m #H destruct (H)
     1206  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     1207  (∀x.f = return x → g x = return y → P) →
     1208  (! x ← f ; g x = return y) → P.
     1209#O #I #A #B #P #f #g #y cases f normalize
     1210[ #o #f #_ #H destruct
     1211| #a #G #H @(G ? (refl …) H)
     1212| #e #_ #H destruct
    11231213] qed.
     1214
     1215interpretation "IO bind inversion" 'bind_inversion =
     1216  (IO_bind_inversion ?????????).
    11241217
    11251218lemma err_eq_from_io : ∀O,I,X,m,v.
     
    11441237cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
    11451238#EQ >EQ //
     1239qed.
     1240
     1241(* this should make things easier for ops using memory (where pc cant happen) *)
     1242definition bv_no_pc : beval → Prop ≝
     1243λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
     1244
     1245lemma bv_pc_other :
     1246  ∀P : beval → Prop.
     1247  (∀pc,p.P (BVpc pc p)) →
     1248  (∀bv.bv_no_pc bv → P bv) →
     1249  ∀bv.P bv.
     1250#P #H1 #H2 * /2/ qed.
     1251
     1252lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
     1253  bv_no_pc bv →
     1254  sigma_beval p p' graph_prog sigma bv prf = bv.
     1255#p #p' #graph_prog #sigma *
     1256[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     1257#prf * whd in match sigma_beval; normalize nodelta
     1258@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
    11461259qed.
    11471260
     
    12541367 ∀p,p',graph_prog.
    12551368 let lin_prog ≝ linearise p graph_prog in
    1256  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1257  let stack_sizes' ≝
    1258   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1259     ? graph_prog stack_sizes in
    1260  ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
    1261  ∀fn,st,stmt,st'.
     1369 ∀stack_sizes.
     1370 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1371 ∀f,fn,st,stmt,st'.
    12621372 ∀prf : well_formed_state … gss st.
    1263   eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
    1264    fn st stmt = return st' →
     1373  eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1374   f fn stmt st = return st' →
    12651375  ∃prf'.
    1266   eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    1267     (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
     1376  eval_seq_no_pc (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1377    f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
    12681378  return sigma_state … gss st' prf'.
    12691379  #p #p' #graph_prog #stack_sizes #sigma #gss
     
    13931503          inversion(sigma_beval_opt ???? y)
    13941504          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
     1505         xxxxxxxxxxxxxxxxxx
     1506       
     1507 qed.       
     1508
     1509lemma eval_statement_no_pc_sigma_commute :
     1510 ∀p,p',graph_prog.
     1511 let lin_prog ≝ linearise p graph_prog in
     1512 ∀stack_sizes.
     1513 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1514 ∀f,fn,st,stmt,st'.
     1515 ∀prf : well_formed_state … gss st.
     1516  eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1517   f fn stmt st = return st' →
     1518  ∃prf'.
     1519  eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1520    f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
     1521       (sigma_state … gss st prf) =
     1522  return sigma_state … gss st' prf'.
     1523  #p #p' #graph_prog #stack_sizes #sigma #gss
     1524  #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
     1525  #st' #prf
     1526  whd in match eval_statement_no_pc; normalize nodelta
     1527  [ @eval_seq_no_pc_sigma_commute
     1528  |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     1529  | (* tailcall, follow proof of CALL in previous lemma *)
     1530    cases daemon
     1531  ]
     1532qed.
     1533
     1534=======
    13951535           whd in match sigma_is_opt; >H normalize nodelta >ABS
    13961536           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
     
    15811721  | (*C_OP1*)
    15821722   
     1723>>>>>>> .r2528
    15831724inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    15841725    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     
    15881729 ∀p,p',graph_prog.
    15891730  let lin_prog ≝ linearise ? graph_prog in
    1590  ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1591  let graph_stack_sizes ≝
    1592   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1593     ? graph_prog lin_stack_sizes in
    1594  (∀sigma.good_sigma_state p p' graph_prog sigma) →
     1731 ∀stack_sizes.
     1732 (∀sigma.good_state_sigma p p' graph_prog sigma) →
    15951733   ex_Type1 … (λR.
    15961734   status_simulation
    1597     (graph_abstract_status p p' graph_prog graph_stack_sizes)
    1598     (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
     1735    (graph_abstract_status p p' graph_prog stack_sizes)
     1736    (lin_abstract_status p p' lin_prog stack_sizes) R).
    15991737 #p #p' #graph_prog
    1600  cases (linearise_spec … graph_prog) #sigma #good
    1601  #lin_stack_sizes
     1738 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
     1739 cut (∀fn.good_local_sigma … (sigma fn))
     1740  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
     1741 #good
     1742 #stack_sizes
    16021743 #gss lapply (gss sigma) -gss #gss
    1603  %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
     1744 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
    16041745whd in match graph_abstract_status;
    16051746whd in match lin_abstract_status;
     
    16161757  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
    16171758whd in match eval_state in ⊢ (%→?); normalize nodelta
    1618 change with (Σi.is_internal_function_of_program ? graph_prog i) in
    1619 match (Sig ??) in ⊢ (%→?);
    1620 letin globals ≝ (prog_var_names ?? graph_prog)
    1621 change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
    1622   match (fetch_statement ?????) in ⊢ (%→?);
    1623 #ex
    1624 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
    1625 #EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
    1626 #EQfetch
    1627 cases (bind_inversion ????? EQfetch)
    1628 #f_id * #H lapply (opt_eq_from_res ???? H) -H
    1629 #EQfunc_of_block
    1630 #H elim (bind_inversion ????? H) -H #stmt' *
    1631 #H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
    1632 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    1633 #EQeval
    1634 cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
    1635 letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
    1636 #entry_0
    1637 #good_local
    1638 * * #wf_pc #wf_state #EQst2
     1759@'bind_inversion
     1760** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt
     1761cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_
     1762@'bind_inversion
     1763#st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance
     1764* #wf_prf #st2_EQ
     1765
     1766cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
     1767* #EQfetch_stmt' #all_labels_in
     1768
     1769letin lin_prog ≝ (linearise … graph_prog)
     1770lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
     1771whd in match eval_state in ⊢ (???%→?);
     1772>st2_EQ in ⊢ (???%→?); normalize nodelta
     1773>EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?);
     1774cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
     1775#wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
     1776
     1777whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1778>EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1779normalize nodelta
     1780
     1781cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement;
     1782normalize nodelta
     1783[ whd in match joint_classify_step; @cond_call_other
     1784  [ (* COND *) #a #lbltrue #nxt
     1785    #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta
     1786    #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other
     1787    [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
     1788    #bv #bv_no_pc #EQretrieve
     1789    cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve)
     1790    #ignore >(sigma_bv_no_pc … bv_no_pc)
     1791    change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?)
     1792    #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?);
     1793    #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv
     1794    >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta
     1795    [ whd in match goto; normalize nodelta
     1796      >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?);
     1797      #EQ destruct(EQ) #ex_advance #ex_advance'
     1798      % [2: %{(tal_base_not_return …)} [3: @ex_advance'
     1799  | (* CALL *) #f #args #dest #nxt
     1800  | (* other *) #stmt #no_call #nxt
     1801  ] normalize nodelta
     1802  [ #ex
     1803    #ex_advance #ex_advance'
     1804  | whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1805    #H @('bind_inversion H) -H #called_block
     1806    #H lapply (err_eq_from_io ????? H) -H #EQcalled_block
     1807    #H @('bind_inversion H) -H * #called * #called_fn
     1808    #H lapply (err_eq_from_io ????? H) -H #EQcalled
     1809    normalize nodelta
     1810    [ #H lapply (err_eq_from_io ????? H) -H ]
     1811    #H @('bind_inversion H) -H
     1812     | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ]
     1813    #ex_advance #ex_advance'
     1814    whd in match joint_classify_seq; normalize nodelta
     1815    >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1816   
     1817    cut (∀p,p',graph_prog,sigma,gss,st,f,bl.
     1818        ∀prf : well_formed_state p p' graph_prog sigma gss st.
     1819        block_of_call (make_sem_graph_params p p') ?
     1820          (globalenv_noinit ? graph_prog) st f = return bl →
     1821        block_of_call (make_sem_lin_params p p') ?
     1822          (globalenv_noinit ? (linearise … graph_prog))
     1823          (sigma_state … st prf) f = return bl)
     1824      [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute
     1825      whd in match eval_seq_advance; normalize nodelta
     1826      >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?);
     1827      >m_return_bind in ⊢ (???%→?);
     1828      >(fetch_function_transf … EQcalled :
     1829        fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?);
     1830      >m_return_bind in ⊢ (???%→?);
     1831      whd in match (transf_fundef); normalize nodelta
     1832       
     1833       
     1834      #block_of_call_sigma_commute
     1835    @match_int_fun #called_descr #EQcalled_descr
     1836    [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ]
     1837    #ex_advance
     1838    cut
     1839      (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ.
     1840      ∀trans : ∀vars.A vars → B vars.
     1841      let prog_out : program (λvars.fundef (B vars)) ℕ ≝
     1842        transform_program ??? prog (λvars.transf_fundef … (trans vars)) in
     1843      ∀i.is_function … (globalenv_noinit … prog) i →
     1844       is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ]
     1845    #f_propagate
     1846    letin sigma_function ≝ (λA,B,prog,trans.
     1847      λf : Σi.is_function ? (globalenv_noinit ? prog) i.
     1848      «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *)
     1849    cut (∀p,p',graph_prog.
     1850      let lin_prog ≝ linearise ? graph_prog in
     1851      ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
     1852      ∀f,st,fn.
     1853      ∀prf : well_formed_state … gss st.
     1854      function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog)
     1855        st f = return fn →
     1856      function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1857        (sigma_state … gss st prf) f = return sigma_function … fn)
     1858        [1,3: (* TODO lemma *) cases daemon ]
     1859    #function_of_call_sigma_commute
     1860    whd in match joint_classify_step; whd in match joint_classify_seq;
     1861    normalize nodelta #next_spec
     1862    >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?);
     1863    >m_return_bind in ⊢ (%→?);
     1864    @match_int_fun
     1865    [2,3: #EQdescr' lapply EQdescr'
     1866      >description_of_function_transf in EQdescr';
     1867     
     1868   
     1869    whd in match sigma_beval; normalize nodelta
     1870    cases bv
     1871    [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ]
     1872    whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?);
     1873    [7: #ignore #_
     1874    #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve
     1875    whd in match (bool_of_beval ?) in ⊢ (% → ?);
     1876    3: >no_call_advance [2: @no_call]
     1877 
     1878
     1879
    16391880generalize in match wf_pc in ⊢ ?;
    16401881whd in ⊢ (%→?);
     
    16561897*
    16571898#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
    1658 letin lin_prog ≝ (linearise … graph_prog)
    1659 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
    16601899destruct(EQst2)
    16611900whd in match eval_state in ⊢ (???%→?); normalize nodelta
    1662 letin st2 ≝ (sigma_state_pc ????? st1 ?)
    1663 >(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
    1664 >m_return_bind in ⊢ (%→?);
    1665 #ex'
    16661901(* resolve classifier *)
    1667 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    1668 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    1669 normalize nodelta
    1670 cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
    16711902[ *
    16721903  [ #stmt #nxt
Note: See TracChangeset for help on using the changeset viewer.