(**************************************************************************) (* ___ *) (* ||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/StatusSimulationHelper.ma". include "ERTL/ERTLtoERTLptrUtils.ma". (* lemma get_internal_function_from_ident_ok : ∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals). ∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 → get_internal_function_from_ident p globals ge f= return fn. #p #globals #ge #bl #f #fn #EQf @('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta >(symbol_of_block_rev … EQf2) >m_return_bind cut(code_block_of_block bl = return bl) [ whd in match code_block_of_block; normalize nodelta @match_reg_elim [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl >m_return_bind >EQf % qed. *) (* whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta whd in match sigma_state in ⊢ (???????%%); normalize nodelta cases(st_frms … st) normalize nodelta [ @res_preserve_error1] * #loc_mem #bl #tl inversion(sigma_frames ????) [ #_ normalize nodelta @res_preserve_error1] * #loc_mem1 #bl1 #tl1 whd in match sigma_frames; normalize nodelta inversion(sigma_frames_opt ????) [ #_ normalize nodelta #_ #ABS destruct] #l whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta whd in match (foldr ?????); normalize nodelta inversion(fetch_internal_function ???) [2: #e #_ whd in ⊢ (??%% → ?); #ABS destruct] * #id1 #fn1 #EQfn1 >m_return_bind normalize nodelta #H @('bind_inversion H) -H #l1 change with (sigma_frames_opt ???? = ? → ?) #EQl1 cut (sigma_frames prog f_lbls f_regs tl = l1) [whd in match sigma_frames; normalize nodelta >EQl1 %] #EQl11 cases l [ whd in ⊢ (??%? → ?); #EQ destruct] #x #y whd in ⊢ (??%? → ?); #EQ1 #_ #EQ2 destruct @mfr_bind1 [2: whd in match set_regs; whd in match set_frms; normalize nodelta >EQl1 in ⊢ (???????%?); normalize nodelta cut(sigma_regs prog f_lbls (added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1)) 〈loc_mem,\snd (regs … st)〉 = 〈map RegisterTag beval beval loc_mem (λbv:beval.sigma_beval prog f_lbls bv)∖ added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1), \snd  (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉) [ whd in match sigma_regs; normalize nodelta @eq_f2 [ %] cases(regs ? st) #x #y %] #EQ EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H fetch_internal_function_no_zero [2: %] #EQ destruct ] @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta cases bl1 in EQbl11 EQfn1; #p1 #p2 #EQ destruct lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 % ] qed. *) definition ERTLptrStatusSimulation : ∀ prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀stack_sizes.∀ f_lbls : lbl_funct. ∀ f_regs : regs_funct. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics translate_data prog f_bl_r f_lbls f_regs → status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝ λprog,stack_sizes,f_lbls,f_regs,f_lb_r,good. let trans_prog ≝ ertl_to_ertlptr prog in mk_status_rel ?? (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes .λs2:ERTLptr_status trans_prog stack_sizes .s1=sigma_state_pc prog f_lbls f_regs s2) (* call_rel ≝ *) (λs1:Σs:ERTL_status prog stack_sizes .as_classifier (ERTL_status prog stack_sizes) s cl_call .λs2:Σs:ERTLptr_status trans_prog stack_sizes .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call . pc (mk_prog_params ERTL_semantics prog stack_sizes) s1 =sigma_stored_pc prog f_lbls (pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes) s2)) (* sim_final ≝ *) ?. cases daemon qed. include "joint/semantics_blocks.ma". lemma as_label_ok : ∀ prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀st,fn,id,stmt. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) = return 〈id,fn,stmt〉 → as_label (ERTLptr_status trans_prog stack_sizes) st = as_label (ERTL_status prog stack_sizes) (sigma_state_pc prog f_lbls f_regs st). #prog #f_lbls #f_regs #stack_size #f_lb_r #good #st #fn #id #stmt #EQfetch whd in match as_label; normalize nodelta change with (pc ? ?) in ⊢ (??(??%)(??%)); cases(b_graph_transform_program_fetch_statement … good … EQfetch) #init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_lb_r ?) normalize nodelta [2: #r #tl *] #EQinit destruct(EQinit) * #l_labs * #l_regs ** #_ #_ cases stmt in EQfetch; [ * [ #c | * [ #c_id | #c_ptr ] #c_arg #c_dest | #reg #lbl | #s ] #nxt | #fin | * ] #EQfetch normalize nodelta * #bl * [1,2,3,4,5: >if_merge_right in ⊢ (% → ?); try %] whd in ⊢ (%→?); cases l_regs normalize nodelta [2,4,5,8,10,12: [3: *] #x #y *] [1,2,4,5,6:| #r #tl whd in ⊢ (% → ?); cases tl -tl normalize nodelta [2: #r1 #tl1 *]] #EQ destruct(EQ) [1,2,3,4,6: * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in match map_eval in ⊢ (% → ?); normalize nodelta whd in ⊢ (?????%?? → ?); whd in match (seq_list_in_code ???????) in ⊢ (%→?); * [1,2,3,4: #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%); destruct(EQmid1) * #nxt1 * #EQt_stmt #_ #_ | * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQt_stmt #_ #_ #_ #_ ] | * #pre_l * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ destruct(EQ) whd in EQmid : (???%); destruct(EQmid) #EQ destruct(EQ) whd in ⊢ (% → ?); #EQt_stmt ] whd in ⊢ (??%%); >EQfetch normalize nodelta whd in match fetch_statement; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn; #EQt_fn >EQt_fn >m_return_bind >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_stmt; #EQt_stmt >EQt_stmt % qed. include alias "basics/lists/listb.ma". definition state_rel ≝ λprog : ertl_program.λf_lbls. λf_regs : (block → label → list register). λbl.λ_ : label.λst1,st2.∃f,fn. fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in st1 = (sigma_state prog f_lbls f_regs added st2). lemma make_ERTL_To_ERTLptr_good_state_relation : ∀prog : ertl_program. let p_out ≝ ertl_to_ertlptr prog in ∀stack_sizes. ∃init_regs : block → list register. ∃f_lbls : block → label → list label. ∃f_regs : block → label → list register. ∃good : b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog init_regs f_lbls f_regs. good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes (λglobals,fn.«translate_data globals fn,(refl …)») init_regs f_lbls f_regs good (state_rel prog f_lbls f_regs) (sem_rel … (ERTLptrStatusSimulation prog … stack_sizes … good)). #prog #stack_sizes cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog) #init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good} % [ #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta lapply EQfn >(fetch_ok_sigma_pc_ok … EQfn) #EQfn1 >EQfn1 % | #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn @fetch_ok_sigma_pc_ok assumption | #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn >(fetch_ok_sigma_last_pop_ok … f fn st2 EQfn) % | #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) #EQ destruct(EQ) whd whd in match sigma_state_pc; normalize nodelta >EQfn % | #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ) lapply(as_label_ok … stack_sizes … good st2 … EQfetch) #EQ EQfetch >m_return_bind normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv whd in match set_no_pc; normalize nodelta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn) >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); #EQ destruct(EQ) >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv; whd in match sigma_state; normalize nodelta #EQbv cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ) cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} % [1,3: % [1,3: % [1,3: %{(refl …)} |*: % ] |*: % ] |*: normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta [ >(pc_of_label_eq … EQt_fn) >m_return_bind] >(fetch_stmt_ok_sigma_pc_ok … EQfetch) % ] whd %{f} %{fn} >EQfn %{(refl …)} >(fetch_stmt_ok_sigma_pc_ok … EQfetch) cases st2 * #frms #is #b #regs #m #pc2 #lp2 % | #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc' whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (succ_pc ???); normalize nodelta whd in match (set_no_pc ???); normalize nodelta whd in ⊢ (%→?); #EQ destruct(EQ) whd in match sigma_state_pc in EQst1_no_pc'; normalize nodelta in EQst1_no_pc'; cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc' #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc') -EQst1_no_pc' #EQst1_no_pc' cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc') [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) %{st2_no_pc'} % [ whd in ⊢ (??%?); >EQst2_no_pc' % | whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta >EQfn % ] | #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = return 〈f,fn,stmt1〉) [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) (get_used_registers_from_seq … (functs ERTL) stmt) ?) [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥ cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption ] ] qed. include alias "basics/lists/listb.ma". lemma eval_seq_no_call_ok : ∀prog. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀st2 : state_pc ERTLptr_semantics. let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in ∀st1' : state_pc ERTL_semantics. ∀f,fn,stmt,nxt. fetch_statement ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) (pc … st1) = return 〈f, fn, sequential … (step_seq ERTL … stmt) nxt〉 → eval_state ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → ∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) st2 st2'. if taaf_non_empty … taf then True else (¬as_costed (ERTL_status prog stack_sizes) st1 ∨ ¬as_costed (ERTL_status prog stack_sizes) st1'). #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #stmt #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H)-H #st_no_pc whd in match eval_statement_no_pc; normalize nodelta #EQnopc whd in match eval_statement_advance; normalize nodelta whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch' cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta [2: #r #tl *] #EQ destruct(EQ) * #labs * #regs ******* #EQlabs #EQregs #_ #_ #_ #_ #fresh_regs * #bl * >if_merge_right in ⊢ (% → ?); [2: %] whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs #EQ destruct(EQ) #eval_spec lapply(err_eq_from_io ????? EQnopc) -EQnopc >(fetch_stmt_ok_sigma_state_ok … EQfetch) #EQnopc cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQnopc) [ #stnopc'' * #EQstnopc'' #EQsem % [ % [@stnopc'' | @(succ_pc ERTL_semantics (pc … st2) nxt) | @(last_pop … st2)]] % [ whd in match sigma_state_pc; normalize nodelta @('bind_inversion EQfetch) * #f1 #fn1 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfn1 #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn1 normalize nodelta >EQsem % ] % [ @(produce_trace_any_any_free_coerced) [ @f | @t_fn1 |6: @eval_spec ||| @EQt_fn1] whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?); >EQstnopc'' %] @if_elim [#_ @I] #_ %1 % whd in match as_costed; normalize nodelta * #H @H whd in ⊢ (??%?); >EQfetch % | #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = return 〈f,fn,stmt1〉) [ lapply(fetch_statement_inv … EQfetch') * #EQfn #_ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); #EQregisters #_ #_ #_ #_ #_ #_ >EQregisters cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) (get_used_registers_from_seq … (functs ERTL) stmt) ?) [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥ lapply(fetch_statement_inv … EQfetch') * #_ normalize nodelta #EQstmt cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters whd in ⊢ (% → ?); #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption ] qed. lemma eval_goto_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀st2. let st1 ≝ (sigma_state_pc prog f_lbls f_regs st2) in ∀st1',f,fn,nxt. fetch_statement ERTL_semantics … (globalenv_noinit ? prog) (pc … st1) = return 〈f, fn, final … (GOTO ERTL … nxt)〉 → eval_state ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) st2 st2'. bool_to_Prop (taaf_non_empty … taf). #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match set_no_pc; whd in match goto; normalize nodelta #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #new_pc lapply(fetch_statement_inv … EQfetch) * #EQfn #_ >(pc_of_label_eq … EQfn) whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) % [ % [ @st2 | @(mk_program_counter (pc_block (pc … st2)) (offset_of_point ERTL_semantics nxt)) | @(last_pop … st2)]] % [ >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match sigma_state_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] cases(b_graph_transform_program_fetch_statement … good … EQfetch) #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta [2: #r #tl *] #EQ destruct(EQ) * #labs ** [2: #hd #tl ** #_ #_ ** #pre #inst * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs whd in match translate_fin_step; normalize nodelta * #bl * whd in ⊢ (% → ?); #EQ destruct(EQ) ** [2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid ** whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?) #EQstmt >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQstmt; #EQstmt %{(taaf_step … (taa_base …) …)} [ whd in match as_classifier; normalize nodelta whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >EQstmt % | whd whd in match eval_state; normalize nodelta whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >EQstmt >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1) % ] @I qed. (* lemma list_elim_on_last : ∀A : Type[0].∀ P : (list A) → Prop. ∀ l. P ([ ]) → (∀pre,last. P (pre@[last])) → P l. #A #P #l #H1 #H2 cut(∀A.∀l : list A.l = [ ] ∨ ∃pre,last. l = pre@[last]) [ #A #l elim l [ %1 % | #a #tl * [ #EQ destruct %2 %{([ ])} %{a} %] * #l1 * #a1 #EQ destruct %2 %{(a::l1)} %{a1} %]] #APP1 lapply(APP1 … l) * [ #EQ >EQ assumption] * #pre * #last #EQ >EQ @H2 qed.*) lemma eval_return_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics translate_data prog f_bl_r f_lbls f_regs. ∀st2, st1',f,fn. let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in fetch_statement ERTL_semantics … (globalenv_noinit ? prog) (pc … st1) = return 〈f, fn, final … (RETURN ERTL … )〉 → eval_state ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) st2 = cl_return ∧ ∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ ∃st2_after_ret. ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) (* always empty in this case *) st2_after_ret st2'. (if taaf_non_empty … taf then ¬as_costed (ERTLptr_status trans_prog stack_sizes) st2_after_ret else True) ∧ eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2 = return st2_after_ret ∧ ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes ??? good) st1' st2_after_ret. #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H #st1_tmp whd in ⊢ (??%%→?); #EQ destruct whd in match set_no_pc in ⊢ (%→?); whd in match eval_statement_advance in ⊢ (%→?); whd in match eval_return; normalize nodelta #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H * #n_st #n_pc change with (ertl_pop_frame ? = ? → ?) >(fetch_stmt_ok_sigma_state_ok … EQfetch) #EQpop_frame cases(pop_frame_ok ?????? EQpop_frame) * #t_n_st #t_n_pc * #EQt_pop_frame normalize nodelta inversion (fetch_internal_function ??) normalize nodelta [ * #id1 #fn1 | #err ] normalize nodelta #EQfetch_fn1 #EQ destruct(EQ) #H @('bind_inversion H) -H #next_of_n_pc [2: >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct(EQ)] #EQnext_of_n_pc cases(next_of_call_pc_ok … good … EQnext_of_n_pc) #pc1 * #EQpc1 cut(pc1 = t_n_pc) [ @(sigma_stored_pc_inj prog f_lbls) lapply EQnext_of_n_pc; next_of_call_pc_error [2,4: % %] whd in ⊢ (???% → ?); #EQ destruct| #x #_ #_ % #EQ destruct] #x #EQx #_ lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta inversion (sigma_pc_opt ???) [ #_ >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct] #y #EQy #_ lapply EQpc1 whd in match sigma_stored_pc; normalize nodelta >EQx >EQy normalize nodelta #EQ destruct % ] #EQ destruct(EQ) #EQnxt whd in match next; whd in match set_last_pop; whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(b_graph_transform_program_fetch_statement … good … EQfetch) #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta [2: #r #tl *] #EQ destruct(EQ) * #labs ** [2: #hd #tl ** #_ #_ * #ibl * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs whd in match translate_fin_step; normalize nodelta * #bl * whd in ⊢ (% → ?); #EQ destruct(EQ) ** [2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid ** whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?) #EQstmt % [ whd in match joint_classify; normalize nodelta whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind >EQstmt % | % [ % [ @t_n_st | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc) | @t_n_pc] ] % [ whd in match sigma_state_pc; normalize nodelta lapply(next_of_call_pc_inv … EQnext_of_n_pc) * #id2 * #fn2 * #c_id * #c_arg * #c_dest #EQfetch1 whd in match (succ_pc ???); >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) >EQfetch_fn1 normalize nodelta % ] % [ % [ @t_n_st | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc) | @t_n_pc] ] %{(taaf_base … )} normalize nodelta % [% [@I]] [ whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind >EQstmt >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_return; normalize nodelta change with (ertl_pop_frame ?) in match (pop_frame ????????); >EQt_pop_frame >m_return_bind >EQnxt >m_return_bind whd in match next; whd in match set_pc; whd in match set_last_pop; whd in match succ_pc; normalize nodelta lapply(next_of_call_pc_inv … EQnext_of_n_pc) * #id2 * #fn2 * #c_id * #c_arg * #c_dest #EQfetch1 whd in match (succ_pc ???); >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) % | whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #s1_pre_prf #EQpc_s2_pre whd in ⊢ (% → ?); #EQ1 >EQ1 in EQfetch_call; #EQfetch_call cases(fetch_call_commute … good … EQfetch_call) #calling' * #pc1 * #EQ1 cut(pc … s2_pre = pc1) [ @(sigma_stored_pc_inj prog f_lbls) lapply(EQfetch_call) whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ???) [1,3: #_ >fetch_statement_no_zero [2,4: %] #EQ destruct(EQ)| #x #_ #_ % #EQ destruct] #pc2 #EQpc2 #_ lapply EQ1 whd in match sigma_stored_pc; normalize nodelta >EQpc2 normalize nodelta cases(sigma_pc_opt ???) [2: #x normalize nodelta #EQ >EQ %] normalize nodelta #EQ fetch_statement_no_zero [ #ABS destruct(ABS)] whd in match sigma_stored_pc; normalize nodelta >EQ1 % ] #EQ2 destruct(EQ2) #EQt_fetch_call whd >EQt_fetch_call normalize nodelta % [ >EQ1 in s1_pre_prf; #EQ @(sigma_stored_pc_inj prog f_lbls) lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ???) [1,3: #_ >next_of_call_pc_error [2,4: % %] whd in ⊢ (???% → ?); #EQ destruct] #pc1 #EQpc1 #_ [ % #EQ destruct] lapply EQ whd in match sigma_stored_pc; normalize nodelta >EQpc1 normalize nodelta inversion(sigma_pc_opt ???) [2: #pc2 #_ normalize nodelta #EQ >EQ %] normalize nodelta #ABS #ABS1 lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta >EQpc1 >ABS1 normalize nodelta >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct | whd in match succ_pc; normalize nodelta change with next_of_n_pc in match (point_of_succ ???); change with nxt' in match (point_of_succ ???); lapply EQpc_s2_pre whd in match succ_pc; normalize nodelta change with next_of_n_pc in match (point_of_succ ???); change with nxt' in match (point_of_succ ???); #EQ >EQ cut(pc_block (pc … s1_pre) = pc_block (pc … s2_pre)) [2: #EQ >EQ %] >EQ1 <(pc_block_eq prog f_lbls …) [%] lapply EQfetch_call whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???) [ >fetch_statement_no_zero [2: %] #EQ destruct] #x #_ % #EQ destruct ] ] ] qed. lemma eval_cond_ok : ∀prog. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. ∀st2,st1',f,fn,a,ltrue,lfalse. let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in fetch_statement ERTL_semantics … (globalenv_noinit ? prog) (pc … st1) = return 〈f, fn, sequential … (COND ERTL … a ltrue) lfalse〉 → eval_state ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → as_costed (ERTL_status prog stack_sizes) st1' → ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) st2 st2'. bool_to_Prop (taaf_non_empty … taf). #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #a #ltrue #lfalse #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv >(fetch_stmt_ok_sigma_state_ok … EQfetch) in ⊢ (% → ?); whd in match set_no_pc; normalize nodelta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta lapply(fetch_statement_inv … EQfetch) * #EQfn #_ [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind | whd in match next; normalize nodelta ] whd in match set_pc; normalize nodelta >(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in ⊢ (??%% → ?); #EQ destruct #n_cost %{(mk_state_pc ? (st_no_pc … st2) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) (last_pop … st2))} [ @ltrue |3: @lfalse] % [1,3: whd in match sigma_state_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] cases(b_graph_transform_program_fetch_statement … good … EQfetch) #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta [2,4: #r #tl *] #EQ destruct(EQ) >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs ** [2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs whd in match translate_step; normalize nodelta * #bl * whd in ⊢ (% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) %{(taaf_step_jump … (taa_base …) …) I} [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind >EQcond % |3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc; normalize nodelta whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind >EQcond >m_return_bind normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1 >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool) #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 >(pc_of_label_eq … EQt_fn1) >m_return_bind % |*: lapply n_cost whd in match as_costed; normalize nodelta [ cut((mk_state_pc ERTL_semantics (sigma_state prog f_lbls f_regs (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *) | cut((mk_state_pc ERTL_semantics (sigma_state prog f_lbls f_regs (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) (succ_pc ERTL_semantics (pc ERTLptr_semantics st2) (point_of_succ ERTLptr_semantics (point_of_pc ERTLptr_semantics (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) (point_of_succ ERTLptr_semantics (point_of_pc ERTLptr_semantics (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) (point_of_succ ERTLptr_semantics (point_of_pc ERTLptr_semantics (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *) ] qed. lemma eval_cost_ok : ∀prog. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. ∀st2,st1',f,fn,c,nxt. let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in fetch_statement ERTL_semantics … (globalenv_noinit ? prog) (pc … st1) = return 〈f, fn, sequential … (COST_LABEL ERTL … c) nxt〉 → eval_state ERTL_semantics (prog_var_names (joint_function ERTL_semantics) ℕ prog) (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) st2 st2'. bool_to_Prop (taaf_non_empty … taf). #prog #f_lbls #f_regs #stack_Size #f_bl_r #good #st2 #st1' #f #fn #c #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta >(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match next; whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt) st2)} % [ whd in match sigma_state_pc; normalize nodelta lapply(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) * #EQfn #_ >EQfn %] lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch' cases(b_graph_transform_program_fetch_statement … good … EQfetch') #init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] normalize nodelta #EQ destruct(EQ) * #lbls * #regs ** #_ #_ whd in ⊢ (% → ?); * #bl * >if_merge_right [2: %] whd in ⊢ (% → ?); cases regs [2: #x #y *] normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid : (???%); destruct(EQmid) whd in ⊢ (% → ?); * #nxt1 * #EQstmt #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) %{(taaf_step … (taa_base …) …)} [1,2: whd [ whd in ⊢ (??%?); | whd in match eval_state; ] whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >EQstmt [%] >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind %] @I qed. lemma eval_call_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs,stack_sizes. ∀f_bl_r. ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. ∀st2,st1',f,fn,called,args,dest,nxt. let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in fetch_statement ERTL_semantics … (globalenv_noinit ? prog) (pc … st1) = return 〈f, fn, sequential … (CALL ERTL … called args dest ) nxt〉 → eval_state … (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = return st1' → ∃is_call,st2_pre_call,is_call'. as_call_ident (ERTLptr_status trans_prog stack_sizes) («st2_pre_call,is_call'») = as_call_ident (ERTL_status prog stack_sizes) («st1, is_call») ∧ (pc … st1) = sigma_stored_pc prog f_lbls (pc … st2_pre_call) ∧ ∃taa2 : trace_any_any (ERTLptr_status trans_prog stack_sizes) st2 st2_pre_call. ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ eval_state ERTLptr_semantics … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2_pre_call =return st2'. #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | * #c_ptr1 #c_ptr2 ] #args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_call; normalize nodelta >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H #c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H #EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ) #H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta [3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call; normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?); [2: @ID |4: @PTR] #EQst1'' #H @('bind_inversion H) -H #st1''' whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H #s_size #H lapply(opt_eq_from_res ???? H) -H change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?); whd in ⊢ (???% → ??%% → ?); #EQ #EQ1 destruct(EQ EQ1) lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?); #EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers ******* #EQlabels #EQregisters #_ #_ #_ #_ #fresh_regs normalize nodelta >if_merge_right [2,4: %] whd in match translate_step; normalize nodelta * #bl * cases registers in EQregisters; -registers normalize nodelta [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters [ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta #EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ) * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 #m_fetch_pre whd in ⊢ (% → ?); * #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(pre_l) in m_fetch_pre EQmid1; [* #x * #y ** #ABS destruct(ABS) |4: #lab #tl * #ABS destruct(ABS) | #l1 #tl #m_fetch_pre whd in ⊢ (???% → ?); #EQ destruct(EQ) | * #_ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) ] % [1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %] cases(ertl_save_frame_ok prog f_lbls f_regs ? (added_registers ERTL (prog_var_names … prog) fn1 (f_regs c_bl')) ? st1''' ?) [2: @PTR |3,7: [ %{(mk_state_pc ? (st_no_pc … st2) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) (last_pop … st2))} |%{(st2)} ] @hide_prf whd in match sigma_pc_opt; normalize nodelta @if_elim [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; [1,3: #EQ destruct(EQ) |*: assumption]] #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) ] >m_return_bind % whd in ⊢ (??%? → ?); #ABS destruct(ABS) |6: @ID |4,8: [change with (pc_block (pc … st2)) in match (pc_block ?); >EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?); |>EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?); ] normalize nodelta whd in match (st_no_pc ??); whd in match sigma_stored_pc in ⊢ (??(???(???%?))?); whd in match sigma_pc_opt; normalize nodelta @if_elim [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; [1,3: #EQ destruct(EQ) |*: assumption]] #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) ] >m_return_bind normalize nodelta change with (pc_block (pc … st2)) in match (pc_block ?); >pc_of_point_of_pc assumption ] #st_no_pc_after_call normalize nodelta * [ #H @('bind_inversion H) -H #st_no_pc_pre_call #EQst_no_pc_pre_call whd in match set_no_pc; normalize nodelta] #EQst_no_pc_after_call #EQ destruct(EQ) [ letin pairpc ≝ (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)) %{(mk_state_pc ? (set_regs ERTL_state (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) st_no_pc_pre_call) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) (last_pop … st2))} | %{st2} ] % [1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind %] % [1,3: % [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?); normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);] >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind lapply EQc_bl' whd in match block_of_call; normalize nodelta cases daemon (* CSC: The proof used to be %, why did it change? *) (* This point will be generalized when the call case will be available in StatusSimulationHelper*) (* XXX [cut (block_of_call (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) (globals (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) (ev_genv (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) (inr ident … 〈c_ptr1,c_ptr2〉) (set_regs ERTL_state 〈add RegisterTag beval (\fst  (regs ERTLptr_semantics st2)) r (\snd  (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) mid1))), \snd  (regs ERTLptr_semantics st2)〉 st_no_pc_pre_call) = block_of_call (mk_prog_params ERTL_semantics prog stack_size) (globals (mk_prog_params ERTL_semantics prog stack_size)) (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) (inr ident … 〈c_ptr1,c_ptr2〉) (sigma_state_pc prog f_lbls f_regs st2)) [2: #URCA m_return_bind >m_return_bind whd in match fetch_internal_function; normalize nodelta whd in match fetch_function; normalize nodelta XXX %*) |*: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta @if_elim change with (pc_block(pc … st2)) in match (pc_block ?); [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_ >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption] whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_ [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) ] >m_return_bind >pc_of_point_of_pc % ] |4: %{(taa_base …)} | %{(taaf_to_taa ??? (produce_trace_any_any_free (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) st2 ????? (mk_state_pc ? (set_regs ERTL_state (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) st_no_pc_pre_call) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) (last_pop … st2)) EQcalling' m_fetch_pre ?) ?)} [ @if_elim [2: #_ @I] #_ % whd in ⊢ (% → ?); whd in match (as_label ??); whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQcall >m_return_bind normalize nodelta whd in match cost_label_of_stmt; normalize nodelta * #H @H % | whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); normalize nodelta whd in match (eval_ext_seq ????????); whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; normalize nodelta @('bind_inversion EQfn) * #f2 * #fn2 whd in match fetch_function; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f3 #EQf3 #H @('bind_inversion H) -H #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) >(find_symbol_transf … (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); normalize nodelta whd in match (eval_ext_seq ????????); whd in match acca_arg_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta @('bind_inversion EQst_no_pc_pre_call) #new_st whd in match push in ⊢ (%→ ?); normalize nodelta #H @('bind_inversion H) -H #is1 #EQis1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H @('bind_inversion H) -H #is2 #EQis2 whd in match set_istack; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match push; normalize nodelta >EQis1 >m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); normalize nodelta whd in match (eval_ext_seq ????????); whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; normalize nodelta >(find_symbol_transf … (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); normalize nodelta whd in match (eval_ext_seq ????????); whd in match acca_arg_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta whd in match push; normalize nodelta >EQis2 >m_return_bind normalize nodelta whd in ⊢ (??%?); @eq_f whd in match set_istack; normalize nodelta whd in match reg_store; normalize nodelta >add_idempotent % | cut(∀st,st',kind.ertlptr_save_frame kind it st = return st' → ∃hd,tl.st_frms … st' = return (cons ? hd tl) ∧ \snd hd = pc_block (pc … st)) [ #st * #frms #is #b #regs #m * whd in match ertlptr_save_frame; normalize nodelta [ >m_return_bind | #H @('bind_inversion H) -H #st'' #EQst''] #H @('bind_inversion H) -H #frames #H lapply(opt_eq_from_res ???? H) -H #EQframes whd in ⊢ (??%% → ?); whd in match set_frms; whd in match set_regs; normalize nodelta #EQ destruct(EQ) %{(〈\fst (regs ERTLptr_semantics ?),pc_block (pc … st)〉)} [2,4: %{frames} % [1,3: %] |1,3:] %] ] #save_frame_non_empty cases(save_frame_non_empty … EQst_no_pc_after_call) * #fst_hd #snd_hd * #rest * #EQrest #EQhd ] cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?) [2,4: whd in match fetch_internal_function; normalize nodelta >EQfn1 %] #init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_ [ %{(mk_state_pc ? st_no_pc_after_call (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) c_bl' (joint_if_entry … t_fn1)) (last_pop … st2))} | %{(mk_state_pc ? (set_frms ERTL_state (〈(add ?? (fst_hd) r (\snd pairpc)),snd_hd〉 :: rest) st_no_pc_after_call) (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) c_bl' (joint_if_entry … t_fn1)) (last_pop … st2))} ] % [1,3: whd in match sigma_state_pc; normalize nodelta whd in match pc_of_point in ⊢ (???%); normalize nodelta whd in match fetch_internal_function; normalize nodelta >EQfn1 >m_return_bind normalize nodelta @eq_f3 [1,3,6: % |2,5: >EQentry %] whd in match sigma_state; normalize nodelta cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2. a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → mk_state ERTL_semantics a1 b1 c1 d1 e1 = mk_state ERTL_semantics a2 b2 c2 d2 e2) [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 //] #APP @APP try % whd in match set_frms; normalize nodelta >EQrest whd in match sigma_frames; normalize nodelta >m_return_bind >m_return_bind whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta whd in match (foldr ?????) in ⊢ (???%); normalize nodelta >EQhd >EQfn >m_return_bind normalize nodelta whd in match (foldr ?????); normalize nodelta >EQfn >m_return_bind normalize nodelta change with (sigma_frames_opt prog f_lbls f_regs ?) in match (foldr ?????); change with (sigma_frames_opt prog f_lbls f_regs ?) in match (foldr ?????); cases(sigma_frames_opt ????) [%] #t_rest >m_return_bind >m_return_bind @eq_f @eq_f2 [2: %] @eq_f2 [2: %] change with (pc_block (pc … st2)) in match (pc_block ?); change with (pc_block (pc … st2)) in match (pc_block ?); whd in match sigma_register_env; normalize nodelta >map_add >set_minus_add [%] @list_as_set_mem @in_added_registers [@(point_of_pc ERTL_semantics (pc ERTLptr_semantics st2)) | whd in match code_has_label; whd in match code_has_point; normalize nodelta >EQstmt % | >EQregisters % % ] |*: whd in match fetch_statement; normalize nodelta; >EQcalling' >m_return_bind [2: >point_of_pc_of_point ] >EQcall >m_return_bind normalize nodelta >m_return_bind [2: >EQc_bl' >m_return_bind | whd in match block_of_call; normalize nodelta @('bind_inversion EQst_no_pc_pre_call) #st3 #H @('bind_inversion H) -H #is3 inversion(istack … st2) [2: #bv |3: #bv1 #bv2] #EQis3 whd in match is_push; normalize nodelta whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) #H @('bind_inversion H) -H #is3 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) whd in match set_regs; whd in match dpl_arg_retrieve; normalize nodelta change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); @('bind_inversion EQc_bl') #c_bl'' whd in match dpl_arg_retrieve; normalize nodelta change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); #H @('bind_inversion H) -H #bv_ptr1 whd in match ps_arg_retrieve; normalize nodelta cases (c_ptr1) in EQstmt; [#r_ptr1 | #b_ptr1] #EQstmt normalize nodelta [ whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr1 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] whd in match dph_arg_retrieve; normalize nodelta change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); whd in match ps_arg_retrieve; normalize nodelta cases c_ptr2 in EQstmt; [1,3: #r_ptr2 |*: #b_ptr2] #EQstmt normalize nodelta [1,2: whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta #H @('bind_inversion H) -H #bv_ptr2 #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr2 |*: >m_return_bind ] #H @('bind_inversion H) -H #ptr #EQptr @if_elim #ptr_ok whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H lapply(opt_eq_from_res ???? H) -H #EQptr_code [2,4: >m_return_bind |*: >lookup_add_miss [1,3: >EQbv_ptr1 >m_return_bind |*: % #ABS destruct(ABS) lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; whd in match get_used_registers_from_step; normalize nodelta whd in ⊢ (???% → ?); * // ] ] change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); whd in match ps_arg_retrieve; normalize nodelta [2,4: >m_return_bind |*: whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta >lookup_add_miss [1,3: >EQbv_ptr2 >m_return_bind |*: % #ABS destruct(ABS) lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; whd in match get_used_registers_from_step; normalize nodelta whd in ⊢ (???% → ?); * // #_ * // ] ] >EQptr >m_return_bind @if_elim [2,4,6,8: >ptr_ok *] #_ >m_return_bind >EQptr_code >m_return_bind ] @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQfn2 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn2 >m_return_bind normalize nodelta [ change with (ertlptr_save_frame ? it ?) in match (save_frame ??????); cut(st2 = mk_state_pc ? st2 (pc … st2) (last_pop … st2)) [ cases st2 #H1 #H2 #H3 %] #EQ EQst_no_pc_after_call >m_return_bind |*: change with (ertlptr_save_frame PTR it ?) in match (save_frame ??????); @('bind_inversion EQst_no_pc_after_call) #st4 whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H @('bind_inversion H) -H #frms4 #H lapply(opt_eq_from_res ???? H) -H #EQfrms4 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match ertlptr_save_frame; normalize nodelta >m_return_bind whd in EQrest : (???%); destruct(EQrest) >EQfrms4 >m_return_bind ] change with (stack_size ?) in match (stack_sizes ????); >EQs_size >m_return_bind % ] 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 ertl_to_ertlptr_ok: ∀prog.∀stack_sizes. let trans_prog ≝ ertl_to_ertlptr prog in ex_Type1 … (λR. status_simulation (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). #prog #stack_size cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog) #fregs * #f_lbls * #f_bl_r #good % [@ERTLptrStatusSimulation assumption] whd in match status_simulation; normalize nodelta whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 change with (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) #EQeval @('bind_inversion EQeval) ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch #_ whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct cases stmt in EQfetch; -stmt [ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]] whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *) | (*CALL*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #is_call_st1 cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1' * #st2_pre_call * #is_call_st2_pre_call * * #Hcall #call_rel * #taa * #st2' * #sem_rel #eval_rel %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption] %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption] whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*) | (*COND*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #n_costed cases(eval_cond_ok … good … EQfetch EQeval) [2: @n_costed] #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]] whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (*TODO*) | (*seq*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases (eval_seq_no_call_ok … good … EQfetch EQeval) #st3 * #EQ destruct * #taf #taf_spec %{st3} %{taf} % [% //] whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma about preservation of fetch_statement *) | cases fin_step in EQfetch; [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases (eval_goto_ok … good … EQfetch EQeval) #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta % [% //] whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma about preservation of fetch_statement *) | (*RETURN*) #EQfetch whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases (eval_return_ok … good … EQfetch EQeval) #is_ret * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:] % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)] % [2: assumption] % [2: %] % [2: assumption] % assumption | (*TAILCALL*) * ] ] qed. (* lemma foo : ∀P1_unser,P2_unser: unserialized_params. ∀P1_sem_unser,P2_sem_unser. let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in ∀init,translate_step. ∀translate_fin_step. ∀closed_graph_translate. let translate_internal : ∀globals. joint_closed_internal_function P1_sem globals → joint_closed_internal_function P2_sem globals ≝ λglobals,fun. «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals (init globals) (translate_step globals) (translate_fin_step globals) (pi1 … fun), closed_graph_translate globals fun» in ∀prog. let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in ∀stack_size. ∀sigma_state_pc. (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) → ∀st : state_pc P2_sem. ∀st' : state_pc P1_sem. ∀f. ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)). luniverse_ok … fn → ∀stmt,nxt. ∀P : (state_pc P2_sem) → Prop. (∀pre_Instrs',last_Instrs',dst. ∃st''.∃st'''.∃st''''. repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size) f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧ eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size)) f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧ st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ P st'' (*st' = sigma_state_pc st''*) ∧ let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in let P2_globals ≝ globals P2_prog_params in All (joint_seq … P2_globals) (no_cost_label … P2_globals) (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) → fetch_statement … (prog_var_names (joint_function P1_sem) ℕ prog) (ev_genv (mk_prog_params P1_sem prog stack_size)) (pc … (sigma_state_pc st)) = return 〈f, fn, sequential … (step_seq P1_sem … stmt) nxt〉 → eval_state … (prog_var_names (joint_function P1_sem) ℕ prog) (ev_genv … (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) = return st' → ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*) P st'' ∧ ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''. (if taaf_non_empty … taf then True else (¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨ ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st')) (* the length of taf is the same of the length of ??? *). #P1_unser #P2_unser #P1_sem_unser #P2_sem_unser letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser) letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser) #init #translate_step #translate_fin_step #closed_graph_translate. letin translate_internal ≝ (λglobals,fun. «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals (init globals) (translate_step globals) (translate_fin_step globals) (pi1 … fun), closed_graph_translate globals fun») #prog letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames))) #stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P #Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt cases (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok) #_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *) #MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt) #list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?); @pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code #EQeval cut((list (code_point P2_sem →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)] #pre_Instrs' cut((code_point P2_sem →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)] #last_Instrs' cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *)) #st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED lapply(produce_trace_any_any_free … NO_COSTED … REPEAT) [ cases daemon (* should be @Multi_fetch *) |