Changeset 2898 for src/joint/StatusSimulationHelper.ma
 Timestamp:
 Mar 18, 2013, 10:03:37 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.