(**************************************************************************) (* ___ *) (* ||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/StatusSimulationUtils.ma". lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel. ∀f,fn,stmt,st1,st2. good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → st_rel st1 st2 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f,fn,stmt〉 → st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2). #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt @(fetch_ok_sigma_state_ok … goodR … EQfn) assumption qed. lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. ∀f,fn,stmt,st1,st2. good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel→ st_rel st1 st2 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f,fn,stmt〉 → pc … st1 = pc … st2. #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt @(fetch_ok_pc_ok … goodR … EQfn) assumption qed. lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. ∀f,fn,stmt,st1,st2. good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → st_rel st1 st2 → fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = return 〈f,fn,stmt〉 → (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs (last_pop … st2). #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt @(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption qed. lemma as_label_ok_non_entry : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st2,f,fn,stmt. fetch_statement … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 → block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn → as_label (joint_status P_in prog stack_sizes) st1 = as_label (joint_status P_out trans_prog stack_sizes) st2. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st2 #f #fn #stmt #EQfetch * #Hbl #Rst1st2 * #Hentry whd in ⊢ (??%%); >EQfetch normalize nodelta lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) [2: @eqZb_elim [1: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn #Hdata #H whd in match fetch_statement; normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >EQt_fn >m_return_bind cases stmt in EQfetch H; [ * [ #c | #id #args #dest | #r #lb | #seq] #nxt | * [ #lb | | #has #id #args ] | * ] #EQfetch normalize nodelta * #bl [1,2,3,4: @eq_identifier_elim [1,3,5,7: #EQ @⊥ @Hentry >EQ % |*: #_ cut(∀b.andb b false = false) [1,3,5,7: * %] #EQ >EQ -EQ normalize nodelta ] ] * [ >(f_step_on_cost … data) whd in ⊢ (% → ?); cases(f_regs ??) [2: # x #y *] normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQcost change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2) >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQcost; #EQcost >EQcost % ] #Hregs * [1,2,3: * [2,4,6: #hd #tl * #mid1 * #mid2 * #l2 *** #EQmid1 cases(\fst (\fst bl)) [1,3,5: whd in ⊢ (% → ?); * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?); * #mid3 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ #_ >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % ] * #mid1 * #mid2 * #l2 *** #_ cases bl in Hregs; ** [2,4,6: #x #y #z #w #_ whd in ⊢ (% → ?); * #a * #b ** #EQ destruct(EQ)] #instr #post #Hregs whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ #_ >EQ inversion(instr ?) [2,3,4,6,7,8,10,11,12: [1,4,7: #id1 #arg1 #dest1 |2,5,8: #r1 #lb1 |*: #seq] #EQ1 >EQ1 %] #c1 #EQc1 lapply(bind_new_bind_new_instantiates … Hregs (cost_in_f_step … data … c1) … (jmeq_to_eq ??? EQc1)) #EQ destruct(EQ) |*: * [2,4,6: #hd #tl * #mid ** #_ cases (\fst bl) [1,3,5: * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?); * #mid1 * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % |*: * #mid ** #_ cases bl in Hregs; * [2,4,6: #x #y #z #_ * #w * #a ** #EQ destruct] #instr #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) #EQ >EQ % ] ] qed. lemma eval_goto_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀lbl. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → let goto ≝ (GOTO P_in lbl) in fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final … goto〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #lbl * #Hbl #Rst1st2 #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 whd in match goto; normalize nodelta >pc_of_label_eq [2: @(proj1 … (fetch_statement_inv … EQfetch)) |*: ] >m_return_bind whd in match set_no_pc; whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs * #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good … EQfetch Rst1st2 …))) [2: % assumption |4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption |3: ] #st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel %{(mk_state_pc ? st2_fin (pc_of_point p_out (pc_block (pc … st2)) lbl) (last_pop … st2))} cut(? : Prop) [3: #Rst1st2' %{Rst1st2'} | | <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) @(st_rel_def … good) [3: @(proj1 … (fetch_statement_inv … EQfetch)) |1,2: |5: @(fetch_stmt_ok_sigma_last_pop_ok … good … Rst1st2 EQfetch) | assumption ] ] >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQl1; #EQl1 lapply(taaf_to_taa … (produce_trace_any_any_free … st2 … … EQl1 … EQst2_fin) ?) [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQfin % | <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn % ] #taa %{(taaf_step … taa …)} [3: %{I} |*: whd [ whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind >point_of_pc_of_point >EQfin [%] >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match goto; normalize nodelta >pc_of_label_eq [2: whd in match (pc_block ?); >EQt_fn in ⊢ (??%?); % |3:] % ] cases(fetch_stmt_ok_succ_ok … lbl … EQfetch) [4: %|3: % % |*:] #stmt' #EQstmt' @(as_label_ok_non_entry … good) [4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt' |1,2,3: | <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) % assumption | <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (?%?); assumption | <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #EQ destruct(EQ) @H % ] qed. lemma eval_goto_premain_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀lbl. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → let goto ≝ (GOTO P_in lbl) in fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final … goto〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_sizes #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #lbl #EQbl #Rst1st2 #EQfetch #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %{st2'} % [assumption] %{(taaf_step … (taa_base …)…)} [ whd change with (joint_classify ???) in ⊢ (??%?); EQfetch % | assumption ] %{I} assumption qed. lemma eval_tailcall_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀has_tail,id,arg. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃is_tail,st2_pre_call,t_is_tail. as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧ ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes) st2_pre_call = return st2_after_call ∧ st_rel st1' st2' ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2_after_call. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #has_tail #id #arg * #Hbl #Rst1st2 #EQfetch whd in match eval_state in ⊢ (% → ?); 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_tailcall; normalize nodelta >set_no_pc_eta #H @('bind_inversion H) -H #bl #EQbl lapply(err_eq_from_io ????? EQbl) -EQbl #EQbl #H @('bind_inversion H) -H * #id1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta [2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_ #H @('bind_inversion H) -H #w whd in ⊢ (??%%→ ?); #ABS destruct(ABS) ] whd in match (stack_sizes ????); #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize_f #H lapply(opt_eq_from_res ???? H) -H #EQssize_f #H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????); #H @('bind_inversion H) -H #ssize_f1 #H lapply(opt_eq_from_res ???? H) -H #EQssize_f1 #H @('bind_inversion H) -H #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) % [@hide_prf whd in ⊢ (??%?); >EQfetch %] lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs * #l1 * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQmid cut(? : Prop) [3: #EQint_fn1 lapply(b_graph_transform_program_fetch_internal_function … good bl id1 fn1) @eqZb_elim [ #ABS cases(block_of_call_no_minus_one … EQbl) >ABS #H @⊥ @H % ] #_ normalize nodelta #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1 cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' ?????? Hdata (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 … EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption] #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H) -H #st2' * #EQst2' #fin_sem_rel |2: whd in match fetch_internal_function; normalize nodelta >EQfn1 % | ] %{(mk_state_pc ? st2_pre (pc_of_point p_out (pc_block … (pc … st2)) mid) (last_pop … st2))} % [ @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid % ] % [ whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); >EQt_fn in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); >EQmid in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta >EQbl >EQt_bl >m_return_bind >m_return_bind >EQt_fn1 >EQint_fn1 % ] %{(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after) (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))} %{(mk_state_pc ? st2' (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))} >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre %{(taaf_to_taa … (produce_trace_any_any_free … st2 … EQt_fn … EQpre EQst2_pre) …)} [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid % ] cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1) * #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_ cases(added_prologue … data1) in EQst2'; [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta * whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2: #x #y #_ #_ *] #EQregs #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2) #EQentry >EQentry %{(taa_base …)} | #hd #tl #EQst2' * normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQnop change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #star * #_ whd in ⊢ (% → ?); * #l3 * #mid3 * #mid4 * #l4 *** #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl4 letin trans_prog ≝ (b_graph_transform_program ????) lapply(taaf_to_taa … (produce_trace_any_any_free … (mk_prog_params p_out trans_prog stack_size) (mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after) (pc_of_point p_out bl mid4) (last_pop … st2)) … EQt_fn1 … EQst2') ?) [4: >point_of_pc_of_point in ⊢ (????%???); assumption | @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQnop % |*:] #taa %{(taa_step … taa)} [ % * #H @H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point cases EQl4 #mid5 * #rest ** #EQ destruct(EQ) * #nxt3 * #EQ #_ #_ >EQ % |2,3: whd [ whd in ⊢ (??%?); | whd in match eval_state; ] whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [2: %] >m_return_bind % ] ] % [2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta >EQint_fn1 >EQt_fn1 >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >point_of_offset_of_point >EQin >m_return_bind normalize nodelta >EQt_cost >m_return_bind normalize nodelta [ %] whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%); whd in match (get_first_costlabel_next ???); generalize in match (refl ??); >EQin in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?)))); #EQcost' normalize nodelta % ] % [1,3: whd in match eval_state; whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1) * #id2 * #fn2 normalize nodelta #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) >EQ -EQ >m_return_bind normalize nodelta whd in match (stack_sizes ????); >EQssize_f >m_return_bind whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????); >EQssize_f1 >m_return_bind >EQst2_after >m_return_bind [2: %] whd in match set_no_pc; normalize nodelta >EQentry % |*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn1 |1,2,5,6:] @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption ] qed. lemma eval_tailcall_premain_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀has_tail,id,arg. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃is_tail,st2_pre_call,t_is_tail. as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧ ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes) st2_pre_call = return st2_after_call ∧ st_rel st1' st2' ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2_after_call. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #has #id #arg #EQbl #Rst1st2 #EQfetch #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab % [ @hide_prf whd in ⊢ (??%?); >EQfetch %] %{st2} % [ @hide_prf change with (joint_classify ???) in ⊢ (??%?); EQfetch %] % [ letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog) cut(∃f',fn',has',id',arg'. fetch_statement p_out … (joint_globalenv p_out trans_prog stack_size) (pc … st2) = return 〈f',fn',final ?? (TAILCALL p_out has' id' arg')〉) [ lapply Hclass whd in ⊢ (??%? → ?); >EQfetch whd in match joint_classify_final; normalize nodelta whd in match joint_classify; normalize nodelta inversion (fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct(EQ)] ** #f' #fn' * [ * [ #c | #c_id #arg #dest | #r #lbl | #seq ] #nxt | * [ #lbl | | #has' #id' #arg' ] | *] #EQt_fetch normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) %{f'} %{fn'} %{has'} %{id'} %{arg'} % ] * #f' * #fn' * #has' * #id' * #arg' #EQt_fetch @('bind_inversion EQeval) #x >EQfetch in ⊢ (% → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta #H @('bind_inversion H) -H #bl #H lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] #H lapply(err_eq_from_io ????? H) -H #H@('bind_inversion H) -H #f_ssize #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize #H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H #f1_ssize #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf1_ssize #H @('bind_inversion H) -H #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQst2') #x >EQt_fetch in ⊢ (% → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta #H @('bind_inversion H) -H #bl' #H lapply(err_eq_from_io ????? H) -H #EQbl' #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) -H #EQfn1' normalize nodelta [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #f_ssize' #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize' #H @('bind_inversion H) -H #st2_fin whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H #f1_ssize' #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf1_ssize' #H @('bind_inversion H) -H #st2_setup #EQst2_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ])); normalize nodelta >EQt_fetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?); normalize nodelta >EQbl >EQbl' >m_return_bind >m_return_bind whd in match fetch_internal_function; normalize nodelta lapply(fetch_ok_pc_ok … good … Rst1st2' ?) [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); % |*: ] whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ) >EQfn1 >EQfn1' >m_return_bind >m_return_bind normalize nodelta lapply EQfn1 whd in match fetch_function; normalize nodelta @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption] #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta #H lapply(opt_eq_from_res ???? H) -H whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta whd in match transform_joint_program; normalize nodelta >(symbol_for_block_transf ??? (λx.x) prog (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?); >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) % ] %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [2: assumption] %{EQst2' Rst1st2'} qed. lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀a,ltrue,lfalse. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → let cond ≝ (COND P_in ? a ltrue) in fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential … cond lfalse〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → as_costed (joint_abstract_status prog_pars_in) st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 #EQfetch #EQeval @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?); cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt [ >(pc_of_label_eq … EQfn) normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?); | whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta ] #EQ destruct(EQ) #n_costed lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?) [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #init_data * #t_fn1 ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta *** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim [1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *] whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??); EQ #EQ1 destruct(EQ1) ] #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1))) [2,4: % assumption] #EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc * normalize nodelta #Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' [ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue) (last_pop … st2))} | %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse) (last_pop … st2))} ] letin st1' ≝ (mk_state_pc P_in ???) letin st2' ≝ (mk_state_pc P_out ???) cut(st_rel st1' st2') [1,3: @(st_rel_def … goodR … f fn ?) [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption |2,5: assumption |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption ] ] #H_fin % [1,3: assumption] >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l lapply(taaf_to_taa ??? (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1 seq_pre_l EQst_pre_mid_no_pc) ?) [1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond * #H @H % ] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???)} [1,5: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?) [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt' whd <(as_label_ok_non_entry … goodR … EQstmt' ? H_fin) [1,4: assumption |2,5: cases(entry_unused … (pi2 ?? fn) … EQstmt) [ whd in match stmt_forall_labels; whd in match stmt_labels; normalize nodelta #H cases(append_All … H) #_ whd in match stmt_explicit_labels; whd in match step_labels; normalize nodelta * whd in match (point_of_label ????); * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 % | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1'; #H2 @H1

point_of_offset_of_point % ] |*: % assumption ] |2,6: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta >EQt_cond % |3,7: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind >rel_v_v' >m_return_bind normalize nodelta [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)] >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) % |*: %{I} cases(fetch_stmt_ok_succ_ok … (pc … st1') … EQfetch) [4,8: % |3: whd in match stmt_labels; normalize nodelta @Exists_append2 whd in match stmt_explicit_labels; whd in match step_labels; normalize nodelta %1 // |7: @Exists_append1 %1 % |2,6: ] #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) [4,11: @EQstmt' |1,2,3,8,9,10: |5,12: % assumption |6,13: assumption |*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) [ * #_ ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H

point_of_pc_of_point % | ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H

point_of_pc_of_point % ] ] ] qed. lemma eval_cond_premain_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f : ident. ∀fn : joint_closed_internal_function P_in ?. ∀a,ltrue,lfalse. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → let cond ≝ (COND P_in ? a ltrue) in fetch_statement P_in ? (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential … cond lfalse〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → as_costed (joint_abstract_status prog_pars_in) st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #EQbl #Rst1st2 #EQfetch #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab whd in ⊢ (% → ?); * #ncost %{st2'} %{Rst1st2'} %{(taaf_step_jump … (taa_base …) …)} [ whd EQfetch % | assumption ] %{I} assumption qed. lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f.∀fn : joint_closed_internal_function P_in ?. ∀stmt,nxt. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → let seq ≝ (step_seq P_in ? stmt) in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential ?? seq nxt〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1') ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel #goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H #EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?) [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQt_fn #Hinit normalize nodelta * #bl * @if_elim [ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??); EQ #EQ1 destruct(EQ1) ] #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) [2: % assumption] #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQfn #_ cut(? : Prop) [3: #Hfin % [@Hfin] |1: | @(st_rel_def ?????????? goodR … f fn) [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption ] ] %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn SBiC EQst2_fin_no_pc)} % [ @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch % ] cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4: % |3: % % |2:] #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) [4: <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt' |1,2,3: | % <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) assumption | assumption | cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H

point_of_offset_of_point % ] qed. lemma general_eval_seq_no_call_premain_ok :∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f.∀fn : joint_closed_internal_function P_in ?. ∀stmt,nxt. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → let seq ≝ (step_seq P_in ? stmt) in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential ?? seq nxt〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → ∃st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #stmt #nxt #EQbl #Rst1st2 #EQfetch #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)} [ whd change with (joint_classify ???) in ⊢ (??%?); EQfetch % | assumption ] %{I} assumption qed. lemma general_eval_cost_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f. ∀fn : joint_closed_internal_function P_in ?.∀c,nxt. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → let cost ≝ COST_LABEL P_in ? c in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential ?? cost nxt〉 → eval_state P_in … (ev_genv … prog_pars_in) st1 = return st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta #EQfetch whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} cut(? : Prop) [3: #Hfin % [@Hfin] | | cases(fetch_statement_inv … EQfetch) #EQfn #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match (succ_pc ???); whd in match (point_of_succ ???); >set_no_pc_eta @(st_rel_def … prog … stack_size … goodR (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:] [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption] @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch) | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch) ] ] lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?) [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQt_fn #Hinit normalize nodelta * #bl * @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_ >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2) | #EQentry #_ >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2) ] %{(taaf_step … (taa_base …) …)} [3,6,9: %{I} |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >EQt_stmt >m_return_bind % ] cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4,8,12: % |2,6,10: |3,7,11: % %] #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) [4,11,18: @EQstmt' |1,2,3,8,9,10,15,16,17: |5,12,19: % assumption |6,13,20: assumption |*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H

point_of_offset_of_point % ] qed. lemma general_eval_cost_premain_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel → ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f. ∀fn : joint_closed_internal_function P_in ?.∀c,nxt. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → let cost ≝ COST_LABEL P_in ? c in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential ?? cost nxt〉 → eval_state P_in … (ev_genv … prog_pars_in) st1 = return st1' → ∃ st2'. st_rel st1' st2' ∧ ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2 st2'. bool_to_Prop (taaf_non_empty … taf) ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #c #nxt #EQbl #Rst1st2 #EQfetch #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)} [ whd change with (joint_classify ???) in ⊢ (??%?); EQfetch % | assumption ] %{I} assumption qed. lemma next_of_call_pc_inv : ∀pars.∀prog. ∀stack_size. ∀pc,nxt. next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc = return nxt → ∃id,fn,c_id,c_args,c_dest. fetch_statement pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc = return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉. #pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta #H @('bind_inversion H) -H ** #id #fn * [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ] #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption qed. lemma stored_pc_inj : ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? → block_id (pc_block pc) ≠ OZ → sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc = sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → pc = pc'. #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H *#H1 whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1 normalize nodelta inversion(sigma_pc_opt ?????????) [ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1 whd in match sigma_pc_opt; normalize nodelta @if_elim [ #Hbl whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(Hbl) -Hbl @eqZb_elim [whd in ⊢ (??%% → ?); #EQ destruct(EQ)] @eqZb_elim [#ABS >ABS in H1; #H @⊥ @H %] @⊥ @H1 %] #Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label; normalize nodelta >code_block_of_block_eq >m_return_bind >fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] >(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 % ] #pc2 #EQpc2 normalize nodelta #EQ destruct(EQ) @(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …) [ assumption] >EQpc1 >EQpc2 % qed. lemma eval_return_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_sizes. ∀ f_lbls,f_regs.∀f_bl_r.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in ∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs st_no_pc_rel st_rel. ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f. ∀fn : joint_closed_internal_function P_in ?. block_id … (pc_block (pc … st1)) ≠ -1 → st_rel st1 st2 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn,final P_in ? (RETURN …)〉 → eval_state P_in … (ev_genv … prog_pars_in) st1 = return st1' → ∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out. ∃taa2 : trace_any_any … st2 st2_ret. ∃taa2' : trace_any_any_free … st2_after_ret st2'. (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ as_classifier … st2_ret cl_return ∧ as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧ ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2'. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #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_return; normalize nodelta #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize #H lapply(opt_eq_from_res ???? H) -H change with (stack_size f) in ⊢ (??%? → ?); #EQssize #H @('bind_inversion H) -H * #st_pop #pc_pop #EQpop #H @('bind_inversion H) -H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next; whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ) lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall … Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop ** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta [ * #sem_rel #EQt_next %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))} %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop) (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)} %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop) (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)} %{((taaf_to_taa … (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))} [ @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt % ] %{(taaf_base …)} cut(? : Prop) [3: #Hfin % [ % [ % [ % [%{I} ] whd [whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%] >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 whd in match (stack_sizes ????); >EQssize >m_return_bind >EQt_pop >m_return_bind >EQt_next >m_return_bind % | @Hfin ] | whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i #calling * #id1 * #arg1 * #dest1 * #nxt' #EQfetch_call * #s2_pre #s2_call whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQ destruct(EQ) whd in ⊢ (??%% → ?); whd in match (point_of_succ ???); whd in match (point_of_succ ???); #EQ cut(next_of_call =nxt') [ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) cases next_of_call in e0; #x normalize nodelta whd in match (offset_of_point ??); cases nxt' #y normalize nodelta #EQ1 destruct(EQ1) % ] -EQ #EQ destruct(EQ) whd in ⊢ (% → ?); fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % | % #ABS cases(next_of_call_pc_inv … EQt_next) #x * #y * #z * #w * #a whd in match fetch_statement; normalize nodelta >fetch_internal_function_no_zero [whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] assumption ] #EQ2 destruct(EQ2) whd cases(next_of_call_pc_inv … EQt_next) #id'' * #fn'' * #c_id'' * #c_args'' * #c_dest'' #EQ3 >EQ3 normalize nodelta % [%] % ] ] |2: whd in match succ_pc; normalize nodelta whd in match (point_of_succ ???); destruct(EQt_pc_pop) lapply(proj1 ?? (fetch_statement_inv … EQcall)) fetch_internal_function_no_zero [ #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >H %] #Hbl_pcpop #sem_rel #EQ @(st_rel_def … good … sem_rel … ) [3: @EQ |1,2:] % | ] cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:] #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc_pop)) (neg one)) [ #Hbl @(as_label_premain_ok ?????????? good) [assumption | assumption ] | #Hbl_pc_pop @(as_label_ok_non_entry … good) [4: @EQstmt' |1,2,3: | assumption | assumption | cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall))) * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #H1 @H

fetch_internal_function_no_zero [#EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS %] #pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????) [ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %] #EQ destruct(EQ) ] #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1 * #pre * #post @eq_identifier_elim [ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c ABS #EQ destruct(EQ) ] #_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta *** cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1) (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1)) #id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1) (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) H)) -H #st2' * #EQst2' #fin_sem_rel %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))} %{(next p_out nxt1 (set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))} %{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)} %{((taaf_to_taa … (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))} [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??); whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ] letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog) lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????) [11: * #taaf * #_ #prf %{taaf} |3: change with (pc_block pc1) in match (pc_block ?); @(proj1 … (fetch_statement_inv … EQt_call)) |2: whd in match next; whd in match succ_pc; whd in match set_pc; whd in match point_of_pc; normalize nodelta whd in match pc_of_point; normalize nodelta >point_of_offset_of_point in ⊢ (????%???); whd in match (point_of_succ ???); @EQpost_c |1: assumption |*: ] cut(? : Prop) [3: #Hfin % [ % [ % [2: @Hfin | % [ % [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *] #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) * #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??); whd in match (as_pc_of ??); whd in match (point_of_succ ???); change with (pc_block pc1) in match (pc_block ?); whd in match fetch_statement; normalize nodelta >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt; normalize nodelta * #H @H % ] ] whd [ whd in match (as_classify ??); | whd in match eval_state; normalize nodelta] whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%] >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 whd in match (stack_sizes ????); >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc; normalize nodelta >EQt_call >m_return_bind % ] ] ] | | whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct] whd in match (point_of_succ ???); @(st_rel_def … good) [3: change with (pc_block pc1) in match (pc_block ?); lapply(proj1 ?? (fetch_statement_inv … EQcall)) EQpc2 % #EQ destruct] #H @H |1,2: | EQpc2 % #EQ destruct] #H @H | % ] ] [ 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 * #EQpc1_pc_s1_pre #EQsucc_pc whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call cases(fetch_statement_sigma_stored_pc … good … EQfetch_call) [2: EQpc1_pc_s1_pre assumption ] #data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored lapply(stored_pc_inj … (sym_eq ??? EQstored)) [2: % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % | % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero [2: ABS1 >fetch_internal_function_no_zero [2: %] ] whd in ⊢ (??%% → ?); #EQ destruct ] #EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim [ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct] #_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ -EQ normalize nodelta *** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta cut(? : Prop) [3: whd in match (last_pop ??); #H %{H} |2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … ) [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % |3: >EQpc1_pc_s1_pre assumption | % #ABS cases(fetch_statement_inv … EQt_call) >fetch_internal_function_no_zero [2: assumption] #EQ destruct ] |] destruct(H) cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ] cut(nxt' = next_of_call) [ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta whd in match (point_of_succ ???); whd in match (point_of_succ ???); whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y whd in match (offset_of_point ??); whd in match (offset_of_point ??); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) % ] #EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call; whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) % ] cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:] #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc1)) (neg one)) [ #Hbl @(as_label_premain_ok ?????????? good) [ change with (pc_block (sigma_stored_pc ?????????)) in match (pc_block ?); fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % | assumption ] | #Hbl_pc_pop @(as_label_ok_non_entry … good) [4: @EQstmt' |1,2,3: | assumption | assumption | cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall))) * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #H1 @H

EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind #H @('bind_inversion H) -H #bl >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta [2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_ #H @('bind_inversion H) -H #w whd in ⊢ (??%% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save #EQst1_save #H @('bind_inversion H) -H #st1_no_pc' whd in match eval_internal_call; normalize nodelta change with (stack_size ?) in match (stack_sizes ????); #H @('bind_inversion H) -H #ssize #H lapply(opt_eq_from_res ???? H) -H #EQssize #H @('bind_inversion H) -H #st1_no_pc'' #EQst1_no_pc'' whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) % [@hide_prf whd in ⊢ (??%?); >EQfetch %] cases(fetch_statement_sigma_stored_pc … good … Hbl EQfetch) #data * #EQdata normalize nodelta *** #pre #instr #post * #Hregs * #pc' * #EQpc' * #t_fn * #nxt' * #l1 * #l2 @eq_identifier_elim [ #EQentry cases(fetch_statement_inv … EQfetch) #_ >EQentry normalize nodelta cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #ABS destruct(ABS) ] #_ cut(∀b.andb b false = false) [* %] #EQ ** >EQ -EQ normalize nodelta * #EQt_call #EQpre #EQpost #_ lapply(b_graph_transform_program_fetch_internal_function … good … bl f1 fn1) @eqZb_elim [ normalize nodelta #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) >ABS #H @H %] #_ normalize nodelta #H cut(? : Prop) [3: #EQint_fn cases(H EQint_fn) -H |2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %|*:] #data1 * #t_fn1 ** #EQt_fn1 #Hdata1 #good1 cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs) (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata) (call_is_call … good … )) … (point_of_pc p_out pc')) [4: @(proj1 … (fetch_statement_inv … EQfetch)) |*:] #id' * #args' * #dest' #EQinstr cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs) (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata) (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize … EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr) #st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after #Hprologue %{(mk_state_pc ? st2_pre pc' (last_pop … st2))} % [ @hide_prf whd in ⊢ (??%?); >EQt_call >EQinstr %] % [ % [2: @sym_eq assumption] whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?); >EQt_call in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ])); normalize nodelta >EQbl >m_return_bind >EQint_fn normalize nodelta >EQinstr normalize nodelta >EQt_bl >m_return_bind >EQt_fn1 % ] %{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after) (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))} cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2' #fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta >(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %] #_ cases(added_prologue … data1) in EQst2'; normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) | #hd #tl #EQst2' ] * whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4: #x #y #_ #_ *] #EQf_regs #EQ [2: whd in EQ : (???%);] destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * [ #EQnop | #EQt_cost ] change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) [ * #star_lab * #Hstar_lab * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1' whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl2 | #EQentry ] whd in EQmid1 : (??%%); destruct(EQmid1) %{(mk_state_pc ? ? (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))} [ @st2' |3: @(increment_stack_usage p_out ssize st2_after)] >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre lapply(taaf_to_taa … (produce_trace_any_any_free … st2 f t_fn … EQpre … EQst2_pre) ?) [3,6: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) fetch_internal_function_no_zero [1,3: #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %] >(pc_of_point_of_pc … pc') #taa1 %{taa1} |1,4: @if_elim #_ [2,4: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) fetch_internal_function_no_zero [1,3: #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %] >(pc_of_point_of_pc … pc') whd in match (as_pc_of ??); >EQt_call >EQinstr % |2,5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) fetch_internal_function_no_zero [1,3: #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %] @(proj1 … (fetch_statement_inv … EQt_call)) ] -taa1 [ letin trans_prog ≝ (b_graph_transform_program ????) lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) (mk_state_pc ? (increment_stack_usage p_out ssize st2_after) (pc_of_point p_out bl mid2) (last_pop … st2)) … EQst2') [ >point_of_pc_of_point in ⊢ (????%???); @EQl2 | change with bl in match (pc_block ?); assumption |*: ] #taaf %{(taaf_to_taa … (taa_append_taaf … (taa_step … (taa_base …) …) taaf) ?)} [1,2: [ @if_elim #_ [2: @I] ] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point [ >EQnop %] cases EQl2 #mid * #rest ** #EQ destruct(EQ) * #nxt2 * #EQmid2 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ >EQmid2 % |3,4: whd [ whd in ⊢ (??%?); | whd in match eval_state; ] whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [%] >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind % ] | >EQentry %{(taa_base …)} ] % [2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta >EQint_fn >EQt_fn1 >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >point_of_offset_of_point >EQcost >m_return_bind normalize nodelta >EQt_cost >m_return_bind [2: %] normalize nodelta whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%); whd in match (get_first_costlabel_next ???); generalize in match (refl ??); >EQcost in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?)))); #EQcost' normalize nodelta % ] % [1,3: whd in match eval_state; normalize nodelta >EQt_call >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >EQinstr normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_call; normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQ normalize nodelta whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) >EQ -EQ >m_return_bind normalize nodelta >EQst2_save >m_return_bind whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????); >EQssize >m_return_bind >EQst2_after >m_return_bind [%] >EQentry % |*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn |1,2,5,6:] @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption ] qed. lemma eval_call_premain_ok : ∀ P_in , P_out: sem_graph_params. ∀prog : joint_program P_in. ∀stack_size. ∀ f_lbls,f_regs.∀init_regs.∀init. ∀st_no_pc_rel,st_rel. let prog_pars_in ≝ mk_prog_params P_in prog stack_size in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in ∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs st_no_pc_rel st_rel. ∀st1,st1' : joint_abstract_status prog_pars_in. ∀st2 : joint_abstract_status prog_pars_out. ∀f. ∀fn : joint_closed_internal_function P_in ?. ∀id,arg,dest,nxt. block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → fetch_statement P_in … (joint_globalenv P_in prog stack_size) (pc … st1) = return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 → eval_state P_in … (ev_genv … prog_pars_in) st1 = return st1' → ∃is_call,st2_pre_call,t_is_call. as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» = as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧ (pc … st1) = sigma_stored_pc P_in P_out prog stack_size init init_regs f_lbls f_regs (pc … st2_pre_call) ∧ ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call = return st2_after_call ∧ st_rel st1' st2' ∧ as_label (joint_abstract_status prog_pars_in) st1' = as_label (joint_abstract_status prog_pars_out) st2_after_call. #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel #good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #EQbl #Rst1st2 #EQfetch #EQeval % [ whd in ⊢ (??%?); >EQfetch %] %{st2} cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab % [ change with (joint_classify ???) in ⊢ (??%?); EQfetch %] % [ % [2: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQbl % ] | %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [%{EQst2' Rst1st2'}] assumption ] whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta lapply Hclass whd in ⊢ (??%% → ?); >EQfetch in ⊢ (% → ?); whd in match joint_classify_step; normalize nodelta inversion(fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct] ** #f' #fn' * [ * [ #c | #id' #arg' #dest' | #r #lbl | #seq ] #nxt | * [ #lb || #h #id' #arg'] | *] #EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct normalize nodelta @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) 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 #H @('bind_inversion H) -H #bl #H lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save #_ #H @('bind_inversion H) -H #st1_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQbl >m_return_bind whd in match fetch_internal_function; normalize nodelta >EQfn1 >m_return_bind normalize nodelta @('bind_inversion EQst2') #x >EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) 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 #H @('bind_inversion H) -H #bl' >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H #EQbl' #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) -H #EQfn1' normalize nodelta [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st2_save #_ #H @('bind_inversion H) -H #st2_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQbl' >m_return_bind >EQfn1' >m_return_bind normalize nodelta lapply(fetch_ok_pc_ok … good … Rst1st2' ?) [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); % |*: ] whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ) lapply EQfn1 whd in match fetch_function; normalize nodelta @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption] #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta #H lapply(opt_eq_from_res ???? H) -H whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta whd in match transform_joint_program; normalize nodelta >(symbol_for_block_transf ??? (λx.x) prog (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?); >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) % qed. lemma pair_dep_match_elim : ∀A,B,C : Type[0].∀P : C → Prop.∀t:A×B. ∀c. (∀x,y,prf.P (c x y prf)) → P (let 〈x,y〉 as prf ≝ t in c x y prf). #A #B #C #P * // qed. theorem joint_correctness : ∀p_in,p_out : sem_graph_params. ∀prog : joint_program p_in.∀stack_size : ident → option ℕ. ∀init : (∀globals.joint_closed_internal_function p_in globals → bound_b_graph_translate_data p_in p_out globals). ∀init_regs : block → list register.∀f_lbls : lbl_funct_type. ∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out. ∀st_rel : joint_state_pc_relation p_in p_out. good_state_relation p_in p_out prog stack_size init init_regs f_lbls f_regs st_no_pc_rel st_rel → good_init_relation p_in p_out prog stack_size init st_no_pc_rel → let trans_prog ≝ b_graph_transform_program … init prog in ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → ∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ ∃[1] R. status_simulation_with_init (joint_abstract_status (mk_prog_params p_in prog stack_size)) (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) R init_in init_out. #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #st_no_pc_rel #st_rel #good #good_init #init_in whd in match make_initial_state; normalize nodelta #H @('bind_inversion H) -H #init_m #EQinit_m @pair_dep_match_elim #m #bl #prf whd in ⊢ (??%% → ?); #EQ destruct(EQ) letin trans_prog ≝ (b_graph_transform_program ????) letin globals_size ≝ (globals_stacksize … trans_prog) letin spp ≝ («mk_pointer bl (mk_offset (bitvector_of_Z 16 (-S (globals_size)))), pi2 … bl») letin st ≝ (mk_state p_out (* frames ≝ *)(Some ? (empty_framesT …)) (* internal_stack ≝ *) empty_is (* carry ≝ *)(BBbit false) (* regs ≝ *)(empty_regsT … spp) (* mem ≝ *)m (* stack_usage ≝ *)0) %{(mk_state_pc ? (set_sp … spp st) init_pc (null_pc one))} >init_mem_transf >EQinit_m >m_return_bind @pair_dep_match_elim #m1 #bl1 #prf' lapply prf lapply prf' lapply prf' EQ % | * #x * #EQ #EQ1 >EQ normalize nodelta >EQ1 % ] ] #x cases(cost_label_of_stmt ???) normalize nodelta [ * [ * #e' #EQ >EQ % | * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %] | #c * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 % ] ] % [ #st1 #st1' #st2 whd in ⊢ (% → ?); #EQeval @('bind_inversion EQeval) ** #f #fn #stmt #H lapply(err_eq_from_io ????? H) -H cases stmt -stmt [ * [ #c | #id #arg #dest | #r #lb | #seq ] #nxt | #fin | * ] #EQfetch #_ whd in ⊢ (% → ?); #Rst1st2 change with (joint_classify ???) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); [ whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(general_eval_cost_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) | cases(general_eval_cost_ok … good … Hbl Rst1st2 EQfetch EQeval) ] #st2' * #Rst1st2' * #taaf * #H #H1 %{st2'} %{taaf} >H % [1,3: %{I} assumption] assumption | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #prf cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(eval_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) | cases(eval_call_ok … good … Hbl Rst1st2 EQfetch EQeval) ] #prf' * #st2_pre * #prf'' ** #EQ #EQ1 * #st2_after * #st2' * #taa * #taa1 ** #EQ2 #H #EQ3 %{st2_pre} [1,3: assumption] % [1,3: % [1,3: >EQ % |*: assumption ] ] %{st2_after} %{st2'} %{taa} %{taa1} % [1,3: %{EQ2 H}] assumption | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #ncost cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(eval_cond_premain_ok … good … Hbl Rst1st2 EQfetch EQeval ncost) | cases(eval_cond_ok … good … Hbl Rst1st2 EQfetch EQeval ncost) ] #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I} assumption] assumption | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(general_eval_seq_no_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) | cases(general_eval_seq_no_call_ok … good … Hbl Rst1st2 EQfetch EQeval) ] #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} % [ >H1 %{I H} |3: %{H1 H} ] assumption ] | @(as_result_ok … good) ] cases fin in EQfetch; -fin [ #lb #EQfetch whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(eval_goto_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) | cases(eval_goto_ok … good … Hbl Rst1st2 EQfetch EQeval) ] #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I H}] assumption | #EQfetch whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ @⊥ @(pre_main_no_return … good … Hbl … EQfetch) ] cases(eval_return_ok … good … Hbl Rst1st2 EQfetch EQeval) #st2_pre * #st2_after * #st2' * #taa * #taaf ***** #H #H1 #H2 #H3 #H4 #H5 %{st2_pre} %{st2_after} %{st2'} %{taa} %{taaf} % [2: assumption] % [2: assumption] % [2: assumption] % [2: assumption] %{H H1} | #has #id #arg #EQfetch whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl [ cases(eval_tailcall_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) | cases(eval_tailcall_ok … good … Hbl Rst1st2 EQfetch EQeval) ] #prf * #st2_pre * #t_is_call * #H * #st2_after * #st2' * #taa1 * #taa2 ** #H1 #H2 #H3 #prf' %{st2_pre} [1,3: assumption] %{H} %{st2_after} %{st2'} %{taa1} %{taa2} % [2,4: assumption] %{H1 H2} ] qed.