Changeset 2898
 Timestamp:
 Mar 18, 2013, 10:03:37 AM (5 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2891 r2898 14 14 (**************************************************************************) 15 15 16 17 include "joint/StatusSimulationHelper.ma". 16 18 include "ERTL/ERTLtoERTLptrUtils.ma". 17 19 … … 159 161 qed. 160 162 161 include "joint/StatusSimulationHelper.ma".162 163 include alias "basics/lists/listb.ma". 163 164 165 definition state_rel ≝ λprog : ertl_program.λf_lbls. 166 λf_regs : (block → label → list register). 167 λbl,st1,st2.∃f,fn. 168 fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 169 let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in 170 st1 = (sigma_state prog f_lbls f_regs added st2). 171 164 172 lemma make_ERTL_To_ERTLptr_good_state_relation : 165 173 ∀prog : ertl_program. … … 173 181 prog init_regs f_lbls f_regs. 174 182 good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes 175 (λglobals,fn.«translate_data globals fn,(refl …)») 176 (sem_rel … (ERTLptrStatusSimulation prog … good)). 183 (λglobals,fn.«translate_data globals fn,(refl …)») init_regs f_lbls f_regs 184 good (state_rel prog f_lbls f_regs) 185 (sem_rel … (ERTLptrStatusSimulation prog … stack_sizes … good)). 177 186 #prog #stack_sizes 178 187 cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics … … 180 189 #init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good} 181 190 % 182 [#s1 #s2 #f #fn #stmt whd in ⊢ (% → ?); #EQ destruct(EQ) @fetch_stmt_ok_sigma_pc_ok 191 [ #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn whd %{f} %{fn} 192 >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta 193 lapply EQfn >(fetch_ok_sigma_pc_ok … EQfn) #EQfn1 >EQfn1 % 194  #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn @fetch_ok_sigma_pc_ok 195 assumption 196  #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn 197 >(fetch_ok_sigma_last_pop_ok … f fn st2 EQfn) % 198  #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); 199 #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) #EQ destruct(EQ) whd 200 whd in match sigma_state_pc; normalize nodelta >EQfn % 183 201  #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ) 184 lapply(as_label_ok … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %202 lapply(as_label_ok … stack_sizes … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); % 185 203  normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn 186 204 #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt … … 194 212 [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn) 195 213 >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ) 196 whd in ⊢ (% → ?); #EQ destruct(EQ) >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv; 214 whd in ⊢ (% → ?); #EQ destruct(EQ) 215 >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv; 197 216 whd in match sigma_state; normalize nodelta #EQbv 198 217 cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ) 199 218 cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn 200 whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %{(refl …)} 201 % [1,3: %{(refl …)} %] 202 %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)} 203 [@ltrue 3: @lfalse] whd in match fetch_statement; normalize nodelta 204 >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt >m_return_bind 205 normalize nodelta >m_return_bind 206 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 207 >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta 208 [ >(pc_of_label_eq … EQt_fn) >m_return_bind] %{(refl …)} 209 whd whd in match sigma_state_pc; normalize nodelta 210 change with (pc_block (pc … st2)) in match (pc_block ?); 211 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn % 219 whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} % 220 [1,3: % 221 [1,3: % 222 [1,3: %{(refl …)} 223 *: % 224 ] 225 *: % 226 ] 227 *: normalize nodelta 228 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 229 >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta 230 [ >(pc_of_label_eq … EQt_fn) >m_return_bind] 231 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) % 232 ] 233 whd %{f} %{fn} >EQfn %{(refl …)} >(fetch_stmt_ok_sigma_pc_ok … EQfetch) 234 cases st2 * #frms #is #b #regs #m #pc2 #lp2 % 212 235  #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state; 213 236 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind … … 220 243 EQst1_no_pc' #EQst1_no_pc' 221 244 cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc') 222 [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) 223 %{(mk_state_pc ? st2_no_pc' 224 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt) 225 (last_pop … st2))} % 226 [ whd in ⊢ (??%?); >EQst2_no_pc' % 227  whd whd in match sigma_state_pc; normalize nodelta >EQfn % 228 ] 245 [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) %{st2_no_pc'} % 246 [ whd in ⊢ (??%?); >EQst2_no_pc' % 247  whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta 248 >EQfn % 249 ] 229 250  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta 230 251 inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ 
src/ERTLptr/ERTLptrToLTLProof.ma
r2889 r2898 21 21 λprog : ltl_program.λstack_sizes. 22 22 joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes). 23 24 axiom sigma_stored_pc : ertlptr_program → (block → label → list label) →25 program_counter → program_counter.26 27 23 28 24 definition clear_sb_type ≝ label → decision → bool. … … 81 77 ]. 82 78 79 include "joint/StatusSimulationHelper.ma". 80 83 81 definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 84 82 ertlptr_program → (block → label → list label) → … … 92 90 let coloured_graph ≝ build … (\snd y) after in 93 91 mk_state_pc ? (sigma_sb_state prog f_lbls f_regs 94 (to_be_cleared_sb after coloured_graph) st) (pc … st) 95 (sigma_stored_pc prog f_lbls (last_pop … st)) 92 (to_be_cleared_sb after coloured_graph) st) (pc … st) 93 (sigma_stored_pc ERTLptr_semantics LTL_semantics 94 prog f_lbls (last_pop … st)) 96 95  Error e ⇒ dummy_state_pc 97 96 ]. 97 98 definition state_rel : fixpoint_computer → coloured_graph_computer → 99 ertlptr_program → (block → label → list label) → (block → label → list register) → 100 (Σb:block.block_region b = Code) → state ERTL_state → state LTL_LIN_state → Prop ≝ 101 λfix_comp,build,prog,f_lbls,f_regs,bl,st1,st2. 102 ∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 103 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 104 let coloured_graph ≝ build … fn after in 105 (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st1) = 106 (sigma_sb_state prog f_lbls f_regs 107 (to_be_cleared_sb after coloured_graph) st2). 98 108 99 109 axiom write_decision : decision → beval → state LTL_LIN_state → … … 132 142 (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call 133 143 .λs2:Σs:LTL_status ??.as_classifier ? s cl_call 134 .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2)) 144 .pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics 145 prog f_lbls (pc ? s2)) 135 146 (* sim_final ≝ *) ?. 136 147 cases daemon … … 167 178 168 179 169 lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.170 #T #x #y #EQ destruct %171 qed.172 173 180 174 181 axiom pc_block_eq_sigma_commute : ∀fix_comp,colour. … … 186 193 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 187 194 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 188 ∀st1,st2,f,fn ,stmt.189 fetch_ statement ERTLptr_semantics (prog_var_names … prog)(globalenv_noinit … prog)190 (pc … st1) = return 〈f,fn,stmt〉 →195 ∀st1,st2,f,fn. 196 fetch_internal_function ? (globalenv_noinit … prog) 197 (pc_block (pc … st1)) = return 〈f,fn〉 → 191 198 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 192 199 R st1 st2 → 193 200 (pc … st1) = (pc … st2). 194 201 195 202 (* 196 203 axiom change_pc_sigma_commute : ∀fix_comp,colour. 197 204 ∀prog.∀ f_lbls,f_regs.∀f_bl_r. … … 203 210 ∀pc1,pc2.pc1 = pc2 → 204 211 R (set_pc … pc1 st1) (set_pc … pc2 st2). 205 (* 212 206 213 axiom globals_commute : ∀fix_comp,colour. 207 214 ∀prog. 208 215 ∀p_out,m,n. 209 216 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 210 prog_var_names … prog = prog_var_names … p_out. *)217 prog_var_names … prog = prog_var_names … p_out. 211 218 212 219 lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C. 213 220 〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3). 214 221 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] // 215 qed. 222 qed.*) 216 223 217 224 include "joint/semantics_blocks.ma". 218 225 include "ASM/Util.ma". 219 include "joint/StatusSimulationHelper.ma".220 221 226 222 227 axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval. … … 350 355 good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes 351 356 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») 357 init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs) 352 358 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)). 353 359 #fix_comp #colour #prog … … 356 362 #init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good} 357 363 % 358 [ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) % 364 [ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc; 365 whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ; 366 normalize nodelta <(pc_eq_sigma_commute … good … EQfn REL) >EQfn 367 normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn} 368 assumption 369  #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) % 370  #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc; 371 whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ; 372 normalize nodelta <(pc_eq_sigma_commute … good … EQfn REL) >EQfn normalize nodelta 373 #H cases(state_pc_eq … H) * #_ #_ // 374  #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); 375 #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd 376 whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta 377 >EQfn >EQfn normalize nodelta // 359 378  #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) % 360 379  normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse 361 380 #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc; 362 normalize nodelta 363 >EQfetch >m_return_bind normalize nodelta >m_return_bind 381 normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind 364 382 whd in match eval_statement_advance; normalize nodelta 365 383 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); … … 385 403 %{st2_pre_mid_no_pc} 386 404 % 387 [1,3: >map_eval_add_dummy_variance_id @move_spec] 388 % [1,3: % %] %{(mk_state_pc ? st2_pre_mid_no_pc 389 (pc_of_point LTL_semantics (pc_block (pc … st2)) ?) 390 (last_pop … st2))} [@ltrue 3: @lfalse] 391 change with prog_pars_out in match (mk_prog_params ???); % 392 [1,3: whd in match eval_state; whd in match eval_statement_no_pc; 393 whd in match fetch_statement; normalize nodelta 394 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind 395 normalize nodelta >m_return_bind 396 change with prog_pars_out in match (mk_prog_params ???); 397 whd in match eval_statement_advance; normalize nodelta 398 change with (hw_reg_retrieve ??) in match (acca_retrieve ?????); 399 whd in match set_no_pc; normalize nodelta 400 >hw_reg_retrieve_write_decision_hit >m_return_bind 401 cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … good fn … Rst1st2 … EQbv) 405 [1,3: >map_eval_add_dummy_variance_id % 406 [1,3: % 407 [1,3: % 408 [1,3: @move_spec 409 *: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 410 whd in match sigma_sb_state_pc; normalize nodelta >EQfn 411 <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 412 normalize nodelta #EQ cases(state_pc_eq … EQ) * 413 #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn} 414 <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 … 415 (point_of_pc ERTLptr_semantics (pc … st2))) 416 [2,4: @dead_registers_in_dead @acc_is_dead ] 417 assumption 418 ] 419 *: % 420 ] 421 *: % 422 ] 423 *: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????); 424 >hw_reg_retrieve_write_decision_hit >m_return_bind 425 cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … 426 good fn … Rst1st2 … EQbv) 402 427 [2,4: @(all_used_are_live_before … EQstmt) 403 428 [1,3: @set_member_singl *: % ] ] #bv' * #EQbv' #EQbv1 … … 405 430 >EQbv' in EQbool; #EQbool 406 431 >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind 407 normalize nodelta [2: %] whd in match goto; normalize nodelta 408 >(pc_of_label_eq … EQt_fn1) % 409 2,4: whd whd in match sigma_fb_state_pc; normalize nodelta 410 whd in match sigma_sb_state_pc; normalize nodelta 411 change with (pc_block (pc … st1)) in match (pc_block ?); 412 cases(fetch_statement_inv … EQfetch) #EQfn #_ >EQfn 413 normalize nodelta <(pc_eq_sigma_commute … good … EQfetch Rst1st2) 414 change with (pc_block (pc … st1)) in ⊢ (???match (???%) with [_⇒ ?  _ ⇒ ?]); 415 >EQfn normalize nodelta 416 lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 417 whd in match sigma_sb_state_pc; normalize nodelta >EQfn 418 <(pc_eq_sigma_commute … good … EQfetch Rst1st2) >EQfn normalize nodelta 419 #EQ cases(state_pc_eq … EQ) * #EQst1st2 #EQpc #EQlp @eq_f3 420 [3,6: assumption 421 2,5: % 422 *: <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 … 423 (point_of_pc ERTLptr_semantics (pc … st2))) 424 [2,4: @dead_registers_in_dead @acc_is_dead ] 425 assumption 426 ] 432 normalize nodelta 433 [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %] 434 whd in match goto; normalize nodelta 435 >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) % 427 436 ] 428  letin p_in ≝ (mk_prog_params ERTLptr_semantics ??) 437  xxxxxxxxxxxx 438 letin p_in ≝ (mk_prog_params ERTLptr_semantics ??) 429 439 letin p_out ≝ (mk_prog_params LTL_semantics ??) 430 440 letin trans_prog ≝ (b_graph_transform_program ????) 
src/joint/StatusSimulationHelper.ma
r2891 r2898 46 46 qed. 47 47 48 definition joint_state_relation ≝ 49 λP_in,P_out.(Σb:block.block_region b=Code) → state P_in → state P_out → Prop. 50 51 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. 52 53 definition sigma_map ≝ block → label → option label. 54 definition lbl_funct ≝ block → label → (list label). 55 definition regs_funct ≝ block → label → (list register). 56 57 definition get_sigma : ∀p : sem_graph_params. 58 joint_program p → lbl_funct → sigma_map ≝ 59 λp,prog,f_lbls.λbl,searched. 60 let globals ≝ prog_var_names … prog in 61 let ge ≝ globalenv_noinit … prog in 62 ! bl ← code_block_of_block bl ; 63 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl); 64 !〈res,s〉 ← find ?? (joint_if_code ?? fn) 65 (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with 66 [None ⇒ eq_identifier … searched lbl 67 Some x ⇒ eq_identifier … searched (\snd x) 68 ]); 69 return res. 70 71 definition sigma_pc_opt : ∀p_in,p_out : sem_graph_params. 72 joint_program p_in → lbl_funct → 73 program_counter → option program_counter ≝ 74 λp_in,p_out,prog,f_lbls,pc. 75 let sigma ≝ get_sigma p_in prog f_lbls in 76 let ertl_ptr_point ≝ point_of_pc p_out pc in 77 if eqZb (block_id (pc_block pc)) (1) then (* check for dummy exit pc *) 78 return pc 79 else 80 ! point ← sigma (pc_block pc) ertl_ptr_point; 81 return pc_of_point p_in (pc_block pc) point. 82 83 definition sigma_stored_pc ≝ 84 λp_in,p_out,prog,f_lbls,pc. match sigma_pc_opt p_in p_out prog f_lbls pc with 85 [None ⇒ null_pc (pc_offset … pc)  Some x ⇒ x]. 86 48 87 record good_state_relation (P_in : sem_graph_params) 49 88 (P_out : sem_graph_params) (prog : joint_program P_in) 50 89 (stack_sizes : ident → option ℕ) 51 90 (init : ∀globals.joint_closed_internal_function P_in globals 52 →bound_b_graph_translate_data P_in P_out globals) 53 (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) → 54 joint_abstract_status (mk_prog_params P_out 55 (b_graph_transform_program P_in P_out init prog) 56 stack_sizes) 57 → Prop) : Prop ≝ 58 { pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 → 59 fetch_statement ? (prog_var_names … prog) 60 (globalenv_noinit … prog) (pc … st1) = return 〈f,fn,stmt〉 → 61 pc … st1 = pc … st2 62 ; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes). 63 ∀st2 : joint_abstract_status ?. 64 ∀f,fn,stmt. 65 fetch_statement ? (prog_var_names … prog) 66 (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 → 67 R st1 st2 → as_label ? st1 = as_label ? st2 91 →bound_b_graph_translate_data P_in P_out globals) 92 (f_bl_r : block → list register) (f_lbls : lbl_funct) (f_regs : regs_funct) 93 (good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs) 94 (st_no_pc_rel : joint_state_relation P_in P_out) 95 (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝ 96 { fetch_ok_sigma_state_ok : 97 ∀st1,st2,f,fn. st_rel st1 st2 → 98 fetch_internal_function ? (globalenv_noinit … prog) 99 (pc_block (pc … st1)) = return 〈f,fn〉 → 100 st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1) (st_no_pc … st2) 101 ; fetch_ok_pc_ok : 102 ∀st1,st2,f,fn.st_rel st1 st2 → 103 fetch_internal_function ? (globalenv_noinit … prog) 104 (pc_block (pc … st1)) = return 〈f,fn〉 → 105 pc … st1 = pc … st2 106 ; fetch_ok_sigma_last_pop_ok : 107 ∀st1,st2,f,fn.st_rel st1 st2 → 108 fetch_internal_function ? (globalenv_noinit … prog) 109 (pc_block (pc … st1)) = return 〈f,fn〉 → 110 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) 111 ; st_rel_def : 112 ∀st1,st2,pc,lp1,lp2,f,fn. 113 fetch_internal_function ? (globalenv_noinit … prog) 114 (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel (pc_block pc) st1 st2 → 115 lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 → 116 st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) 117 ; as_label_ok : let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 118 ∀st1,st2,f,fn,stmt. 119 fetch_statement ? (prog_var_names … prog) 120 (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 → 121 st_rel st1 st2 → 122 as_label (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 = 123 as_label (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2 68 124 ; cond_commutation : 69 125 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in … … 76 132 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 77 133 st1 = return st1' → 78 Rst1 st2 →134 st_rel st1 st2 → 79 135 ∀t_fn. 80 136 fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) = … … 90 146 (st_no_pc ? st2) 91 147 = return st2_pre_mid_no_pc ∧ 92 let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid) 93 (last_pop … st2) in 148 st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧ 94 149 joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 95 150 ((\snd (\fst blp)) mid) = cl_jump ∧ 96 151 cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 97 152 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧ 98 ∃st2_mid . 99 eval_state P_out (prog_var_names … trans_prog) 100 (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid = 101 return st2_mid ∧ R st1' st2_mid 153 let st2_pre_mid ≝ mk_state_pc P_out st2_pre_mid_no_pc 154 (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in 155 let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in 156 eval_statement_advance P_out (prog_var_names … trans_prog) 157 (ev_genv … (mk_prog_params P_out trans_prog stack_sizes)) f t_fn 158 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2' 102 159 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 103 ) (init ? fn) 160 ) (init ? fn) 104 161 ; seq_commutation : 105 162 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in … … 112 169 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 113 170 st1 = return st1' → 114 Rst1 st2 →171 st_rel st1 st2 → 115 172 ∀t_fn. 116 173 fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) = … … 118 175 bind_new_P' ?? 119 176 (λregs1.λdata.bind_new_P' ?? 120 (λregs2.λblp.177 (λregs2.λblp. 121 178 ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes) 122 179 (globals (mk_prog_params P_out trans_prog stack_sizes))). … … 125 182 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 126 183 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 127 let st2_fin ≝ 128 mk_state_pc ? st2_fin_no_pc 129 (pc_of_point P_out (pc_block(pc … st2)) nxt) 130 (last_pop … st2) in 131 R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq) 132 ) (init ? fn) 184 st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1') st2_fin_no_pc 185 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 186 ) (init ? fn) 133 187 }. 134 188 189 lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params. 190 ∀prog : joint_program P_in. 191 ∀stack_sizes. 192 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 193 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 194 ∀st_no_pc_rel,st_rel. 195 ∀f,fn,stmt,st1,st2. 196 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 197 st_no_pc_rel st_rel → 198 st_rel st1 st2 → 199 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 200 return 〈f,fn,stmt〉 → 201 st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1) (st_no_pc … st2). 202 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel 203 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch 204 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt 205 @(fetch_ok_sigma_state_ok … goodR … EQfn) assumption 206 qed. 207 208 lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params. 209 ∀prog : joint_program P_in. 210 ∀stack_sizes. 211 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 212 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 213 ∀st_no_pc_rel,st_rel. 214 ∀f,fn,stmt,st1,st2. 215 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 216 st_no_pc_rel st_rel → 217 st_rel st1 st2 → 218 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 219 return 〈f,fn,stmt〉 → 220 pc … st1 = pc … st2. 221 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel 222 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch 223 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt 224 @(fetch_ok_pc_ok … goodR … EQfn) assumption 225 qed. 226 227 lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params. 228 ∀prog : joint_program P_in. 229 ∀stack_sizes. 230 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 231 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 232 ∀st_no_pc_rel,st_rel. 233 ∀f,fn,stmt,st1,st2. 234 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 235 st_no_pc_rel st_rel → 236 st_rel st1 st2 → 237 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 238 return 〈f,fn,stmt〉 → 239 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2). 240 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel 241 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch 242 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt 243 @(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption 244 qed. 245 246 (* 247 lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params. 248 ∀prog : joint_program P_in. 249 ∀stack_sizes. 250 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 251 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 252 ∀st_no_pc_rel,st_rel. 253 ∀f,fn,stmt,st1,st2. 254 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 255 st_no_pc_rel st_rel → 256 st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) → 257 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) → 258 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 259 return 〈f,fn,stmt〉 → st_rel st1 st2. 260 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel 261 #st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ) 262 #EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt 263 @(st_rel_def … goodR … EQfn) assumption 264 qed. 265 *) 266 267 135 268 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. 136 269 ∀prog : joint_program P_in. … … 138 271 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 139 272 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 273 ∀st_no_pc_rel,st_rel. 140 274 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 141 275 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 142 276 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 143 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 144 good_state_relation P_in P_out prog stack_sizes init R→277 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 278 st_no_pc_rel st_rel → 145 279 ∀st1,st1' : joint_abstract_status prog_pars_in. 146 280 ∀st2 : joint_abstract_status prog_pars_out. … … 148 282 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog). 149 283 ∀a,ltrue,lfalse. 150 Rst1 st2 →284 st_rel st1 st2 → 151 285 let cond ≝ (COND P_in ? a ltrue) in 152 286 fetch_statement P_in … … … 156 290 st1 = return st1' → 157 291 as_costed (joint_abstract_status prog_pars_in) st1' → 158 ∃ st2'. Rst1' st2' ∧292 ∃ st2'. st_rel st1' st2' ∧ 159 293 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 160 294 bool_to_Prop (taaf_non_empty … taf). 161 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2 162 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed 295 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel 296 #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval 297 @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) 298 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 299 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #bv #EQbv 300 #H @('bind_inversion H) H * #EQbool normalize nodelta whd in ⊢ (??%% → ?); 301 cases(fetch_statement_inv … EQfetch) #EQfn #_ 302 [ >(pc_of_label_eq … EQfn) 303 normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?); 304  whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta 305 ] 306 #EQ destruct(EQ) #n_costed 163 307 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 164 #init_data * #t_fn1 ** >( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch)308 #init_data * #t_fn1 ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 165 309 #EQt_fn1 whd in ⊢ (% → ?); #Hinit 166 * #labs * #regs 167 ** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls * 310 * #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls * 168 311 whd in ⊢ (% → ?); @if_elim 169 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta312 [1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta 170 313 whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 171 * #_ >( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch) whd in match point_of_pc;314 * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; 172 315 normalize nodelta whd in match (point_of_offset ??); <ABS 173 316 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) 174 317 ] 175 #_ <( pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1176 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1318 #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * 319 #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 177 320 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 178 321 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit 179 322 (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1))) 180 323 #EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 181 cases(APP … EQmid) APP 182 #st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST * 183 #st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid} 184 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l 324 cases(APP … EQmid) APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta 325 #EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid 326 [ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue) 327 (last_pop … st2))} 328  %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse) 329 (last_pop … st2))} 330 ] 331 letin st1' ≝ (mk_state_pc P_in ???) 332 letin st2' ≝ (mk_state_pc P_out ???) 333 cut(st_rel st1' st2') 334 [1,3: @(st_rel_def … goodR … f fn ?) 335 [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption 336 2,5: assumption 337 3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption 338 ] 339 ] 340 #H_fin 341 % 342 [1,3: assumption] 343 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l 185 344 lapply(taaf_to_taa ??? 186 345 (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1 187 346 seq_pre_l EQst_pre_mid_no_pc) ?) 188 [ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??); 189 whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind 190 whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta 191 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST * 192 #H @H % 193 ] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I} 194 [ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*) 195  whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta 196 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta 197 assumption 198  assumption 347 [1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??); 348 whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind 349 whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta 350 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST * 351 #H @H % 352 ] 353 #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I} 354 [1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption] 355 cases daemon (*TODO: general lemma!*) 356 2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta 357 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta 358 assumption 359 *: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta 360 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind 361 cases(blm mid1) in CL_JUMP COST Hst2_mid; 362 [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) 363 2,4,6,8: [1,3: #c_id #args #dest *: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ) 364 ] 365 #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta 366 >m_return_bind assumption 199 367 ] 200 368 qed. … … 209 377 *) 210 378 211 lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params. 212 ∀prog : joint_program P_in. 213 ∀stack_sizes. 214 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 215 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 379 lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params. 380 ∀prog : joint_program P_in. 381 ∀stack_sizes. 382 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 383 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 384 ∀st_no_pc_rel,st_rel. 216 385 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 217 386 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 218 387 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 219 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 220 good_state_relation P_in P_out prog stack_sizes init R→388 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 389 st_no_pc_rel st_rel → 221 390 ∀st1,st1' : joint_abstract_status prog_pars_in. 222 391 ∀st2 : joint_abstract_status prog_pars_out. 223 ∀f. 224 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog). 392 ∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog). 225 393 ∀stmt,nxt. 226 Rst1 st2 →394 st_rel st1 st2 → 227 395 let seq ≝ (step_seq P_in ? stmt) in 228 396 fetch_statement P_in … … … 231 399 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 232 400 st1 = return st1' → 233 ∃st2'. Rst1' st2' ∧401 ∃st2'. st_rel st1' st2' ∧ 234 402 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 235 403 if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) 236 404 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 237 405 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 238 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' 239 #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval 406 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel 407 #goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval 408 @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) 409 #H @('bind_inversion H) H #st1_no_pc #H lapply(err_eq_from_io ????? H) H 410 #EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc; 411 whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) 240 412 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 241 #init_data * #t_fn ** >( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch)413 #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 242 414 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim 243 415 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 244 416 whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 245 * #_ >( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch) whd in match point_of_pc;417 * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; 246 418 normalize nodelta whd in match (point_of_offset ??); <ABS 247 419 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) 248 420 ] 249 #_ <( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch) #EQbl250 >( pc_eq_sigma_commute… goodR … Rst1st2 EQfetch) #SBiC421 #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl 422 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC 251 423 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit 252 424 (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) 253 425 #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem 254 426 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} 255 %{Rsem} 427 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 428 #EQfn #_ 429 % 430 [ @(st_rel_def ??????????? goodR … f fn) 431 [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption 432  <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption 433  @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption 434 ] 435 ] 256 436 %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 257 437 SBiC EQst2_fin_no_pc)} 258 438 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 259 439 qed. 440 441 (* 442 lemma eval_cost_ok : 443 ∀ P_in , P_out: sem_graph_params. 444 ∀prog : joint_program P_in. 445 ∀stack_sizes. 446 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 447 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 448 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 449 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 450 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 451 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 452 ∀st1,st1' : joint_abstract_status prog_pars_in. 453 ∀st2 : joint_abstract_status prog_pars_out. 454 ∀f. 455 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt. 456 R st1 st2 → 457 let cost ≝ COST_LABEL P_in ? c in 458 fetch_statement P_in … 459 (globalenv_noinit ? prog) (pc … st1) = 460 return 〈f, fn, sequential ?? cost nxt〉 → 461 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 462 st1 = return st1' → 463 ∃ st2'. R st1' st2' ∧ 464 ∃taf : trace_any_any_free 465 (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) 466 st2 st2'. 467 bool_to_Prop (taaf_non_empty … taf). 468 #P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1' 469 #st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state; 470 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind 471 normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) 472 *)
Note: See TracChangeset
for help on using the changeset viewer.