Changeset 2849
 Timestamp:
 Mar 12, 2013, 1:41:46 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2845 r2849 70 70 ∀ prog : ertlptr_program. 71 71 ∀ f_lbls. ∀ f_regs. ∀f_bl_r. 72 ∀p_out,m,n.73 ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉 →74 let stacksizes ≝ lookup_stack_cost … m in75 72 b_graph_transform_program_props ERTLptr_semantics LTL_semantics 76 73 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 74 let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in 75 let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 76 let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in 77 let stacksizes ≝ lookup_stack_cost … m in 77 78 status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝ 78 λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r,p_out,m,n,EQ. 79 λgood. 79 λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood. 80 80 mk_status_rel ?? 81 (* sem_rel ≝ *) (λs1:ERTLptr_status prog ?. 82 λs2: LTL_status ? ?. 83 sigma_fb_state_pc prog f_lbls f_regs s1 = sigma_sb_state_pc prog f_lbls f_regs s2) 81 (* sem_rel ≝ *) 82 (λs1:ERTLptr_status ? ? 83 .λs2:LTL_status ? ? 84 .sigma_fb_state_pc prog f_lbls f_regs s1 85 =sigma_sb_state_pc prog f_lbls f_regs s2) 84 86 (* call_rel ≝ *) 85 (λs1:Σs .as_classifier … s cl_call.86 λs2:Σs.as_classifier … s cl_call.87 pc … s1 =sigma_stored_pc prog f_lbls (pc … s2))87 (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call 88 .λs2:Σs:LTL_status ??.as_classifier ? s cl_call 89 .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2)) 88 90 (* sim_final ≝ *) ?. 89 91 cases daemon … … 92 94 axiom as_label_ok : 93 95 ∀fix_comp,colour. 94 ∀prog. 95 ∀p_out,m,n. 96 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 97 ∀f_lbls,f_regs. 98 ∀f_bl_r. 96 ∀prog.∀f_lbls,f_regs. ∀f_bl_r. 99 97 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 100 98 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 101 99 ∀st1,st2,fn,id,stmt. 102 let stack_sizes ≝ lookup_stack_cost m in 103 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 104 R st1 st2 → 100 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 101 R st1 st2 → 105 102 fetch_statement ERTLptr_semantics (prog_var_names … prog) 106 103 (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 → 107 as_label (LTL_status p_out stack_sizes) st2 =108 as_label (ERTLptr_status prog stack_sizes) st1. 104 as_label ? st2 = as_label ? st1. 105 109 106 110 107 … … 146 143 147 144 axiom pc_block_eq_sigma_commute : ∀fix_comp,colour. 148 ∀prog. 149 ∀p_out,m,n. 150 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 151 ∀ f_lbls,f_regs. 152 ∀f_bl_r. 145 ∀prog.∀ f_lbls,f_regs.∀f_bl_r. 153 146 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 154 147 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 155 148 ∀st1,st2. 156 let stack_sizes ≝ lookup_stack_cost m in 157 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 149 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 158 150 R st1 st2 → 159 151 pc_block (pc … st1) = pc_block (pc … st2). 160 152 161 axiom change_pc_sigma_commute : ∀fix_comp,colour. 162 ∀prog. 163 ∀p_out,m,n. 164 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 165 ∀ f_lbls,f_regs. 166 ∀f_bl_r. 153 axiom pc_eq_sigma_commute : ∀fix_comp,colour. 154 ∀prog.∀ f_lbls,f_regs.∀f_bl_r. 167 155 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 168 156 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 169 157 ∀st1,st2. 170 let stack_sizes ≝ lookup_stack_cost m in 171 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 158 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 159 R st1 st2 → 160 (pc … st1) = (pc … st2). 161 162 163 axiom change_pc_sigma_commute : ∀fix_comp,colour. 164 ∀prog.∀ f_lbls,f_regs.∀f_bl_r. 165 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 166 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 167 ∀st1,st2. 168 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 172 169 R st1 st2 → 173 170 ∀pc1,pc2.pc1 = pc2 → 174 171 R (set_pc … pc1 st1) (set_pc … pc2 st2). 175 172 (* 176 173 axiom globals_commute : ∀fix_comp,colour. 177 174 ∀prog. 178 175 ∀p_out,m,n. 179 176 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 180 prog_var_names … prog = prog_var_names … p_out. 177 prog_var_names … prog = prog_var_names … p_out.*) 178 179 lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C. 180 〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3). 181 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] // 182 qed. 181 183 182 184 include "joint/semantics_blocks.ma". … … 186 188 ∀fix_comp,colour. 187 189 ∀prog. 188 ∀p_out,m,n. 189 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 190 ∀ f_lbls,f_regs. 191 ∀f_bl_r. 190 ∀ f_lbls,f_regs.∀f_bl_r. 192 191 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 193 192 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 194 193 ∀st1,st2,st1',f,fn,a,ltrue,lfalse. 195 let stack_sizes ≝ lookup_stack_cost m in 196 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 194 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in 197 195 R st1 st2 → 198 196 fetch_statement ERTLptr_semantics … 199 197 (globalenv_noinit ? prog) (pc … st1) = 200 198 return 〈f, fn, sequential … (COND ERTLptr … a ltrue) lfalse〉 → 199 let stacksizes ≝ lookup_stack_cost … 200 (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 201 201 eval_state ERTLptr_semantics 202 202 (prog_var_names … ℕ prog) 203 (ev_genv … (mk_prog_params ERTLptr_semantics prog stack _sizes))203 (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes)) 204 204 st1 = return st1' → 205 as_costed (ERTLptr_status prog stack _sizes) st1' →205 as_costed (ERTLptr_status prog stacksizes) st1' → 206 206 ∃ st2'. R st1' st2' ∧ 207 ∃taf : trace_any_any_free (LTL_status p_out stack_sizes)207 ∃taf : trace_any_any_free (LTL_status ? ?) 208 208 st2 st2'. 209 209 bool_to_Prop (taaf_non_empty … taf). 210 #fix_comp #colour #prog #transf_prog #stack_size #maxstack #EQtransf_prog 211 #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a #ltrue #lfalse 212 #Rst1st2 213 #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind 210 #fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a 211 #ltrue #lfalse #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta 212 >EQfetch >m_return_bind 214 213 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 215 214 whd in match eval_statement_advance; normalize nodelta 216 215 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 217 216 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H 218 #bv >set_no_pc_eta 219 #EQbv #H @('bind_inversion H) H * #EQbool normalize nodelta 220 lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 217 #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) H * #EQbool normalize nodelta 218 lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 221 219 [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind 222 220  whd in match next; normalize nodelta 223 221 ] 224 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) EQ st1' 225 #n_cost 222 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) EQ st1' #n_cost 226 223 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 227 224 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta 228 225 [2,4: #r #tl *] #EQ >EQ init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs ** 229 226 [2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs 230 whd in match translate_step; normalize nodelta * #bl * 231 whd in ⊢ (% → ?); inversion (〈?,?〉) * #blp #blm #bls #EQ #EQbl >EQbl bl 232 letin p≝ (mk_prog_params LTL_semantics (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) (lookup_stack_cost stack_size)) 233 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l 227 whd in match translate_step; normalize nodelta *** #blp #blm #bls * 228 whd in ⊢ (% → ?); #EQbl 229 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 230 #seq_pre_l 231 letin stacksizes ≝ (lookup_stack_cost … 232 (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) 233 letin p≝ (mk_prog_params LTL_semantics 234 (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) 235 stacksizes) 234 236 cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧ 235 237 pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧ 236 238 last_pop … st2' = last_pop … st2) 237 239 [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ] 238 #st2_pre_ cond ** #res_st2_pre_cond #EQpc_st2_pre_cond #EQlast_pop_st2_pre_cond239 >(pc_block_eq_sigma_commute … EQtransf_prog …good … Rst1st2) in EQt_fn1; #EQt_fn1240 241 xxxxxxxxxxxxxxxxxxxxxxxxxxxx 242 240 #st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid 241 >(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1 242 >(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l 243 whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ 244 >EQ in EQmid ⊢ %; nxt1 #EQmid 243 245 lapply(taaf_to_taa ??? 244 (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_cond EQt_fn1 seq_pre_l res_st2_pre_cond) ?) 245 246 @(map_eval ??? mid1) lapply blp whd in match p; normalize nodelta 247 whd in match (globals ?); whd in match prog_var_names; normalize nodelta 248 change with (prog_var_names ??) in match (globals ??); 249 250 lapply(produce_trace_any_any_free p st2 ????? 251 252 253 %{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)} 246 (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1 247 seq_pre_l res_st2_pre_mid) ?) 248 [1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta 249 whd in match (as_label ??); whd in match (as_pc_of ??); 250 whd in match fetch_statement; normalize nodelta * #H @H H >EQt_fn1 251 >m_return_bind whd in match point_of_pc; normalize nodelta 252 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta 253 cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ] 254 #taa_pre_mid whd in ⊢ (% → ?); 255 cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid = 256 return st2_cond ) 257 [2,4: cases daemon (*THE EXTENSIONAL PROOF *)] 258 #st2_mid #EQst2_mid 259 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_mid = cl_jump) 260 [1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?); 261 * #EQ1 #EQ2 destruct(EQ1 EQ2) 262 #seq_post_l 263 lapply(taaf_to_taa ??? 264 (produce_trace_any_any_free p st2_cond f t_fn1 ??? st2_pre_mid EQt_fn1 265 seq_pre_l res_st2_pre_mid) ?) 266 267 268 cases(appoggio ????????? EQbl) * #_ #_ #EQ1 >EQ1 EQ1 269 whd in ⊢ (% → ?); * #EQ2 #EQ3 >EQ3 in seq_pre_l EQcond; mid2 #se_pre_l #EQcond 270 >EQ2 in EQmid1; #EQmid1 l2 271 %{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2_pre_cond)} 254 272 [ @ltrue 3: @lfalse] 255 % [1,3: @(change_pc_sigma_commute … EQtransf_prog … good … Rst1st2) 256 <(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) %] 257 258 259 273 % [1,3: @(change_pc_sigma_commute … good … Rst1st2) % ] 274 %{(taaf_step_jump ? ??? taa_pre_cond ???) I} 275 [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 276 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind 277 cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDENT * #_ #EQ #_ >EQ EQ % *) 278 3,6: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta 279 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind 280 cases(appoggio ????????? EQbl) * #_ #EQ #_ >EQ EQ 281 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 282 whd in match eval_statement_advance; normalize nodelta 283 change with (hw_reg_retrieve ??) in match (acca_retrieve ?????); 284 cases 260 285 bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 261 286 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * … … 322 347 ∀colour : coloured_graph_computer. 323 348 ∀p_in : ertlptr_program. 324 let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in 349 let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in 350 let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in 351 let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in 325 352 (* what should we do with n? *) 326 353 let stacksizes ≝ lookup_stack_cost m in … … 331 358 R. 332 359 #fix_comp #colour #p_in 333 @pair_elim * #p_out #m #n #EQp_out whd334 360 cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics 335 361 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in) 336 362 #fregs * #f_lbls * #f_bl_r #good 337 %{(ERTLptr_to_LTL_StatusSimulation … EQp_out… good)}363 %{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)} 338 364 whd in match status_simulation; normalize nodelta 339 365 whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta … … 367 393  (*COND*) whd in match joint_classify; normalize nodelta >EQfetch 368 394 normalize nodelta #n_costed 369 cases(eval_cond_ok … EQp_out… good … EQst2 … EQfetch EQeval … n_costed)395 cases(eval_cond_ok … good … EQst2 … EQfetch EQeval … n_costed) 370 396 #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@Iassumption]] 371 whd >EQst2' >(as_label_ok fix_comp colour … EQp_out …good … EQst2') [%] cases daemon (*TODO*)397 whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*) 372 398  (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch 373 399 normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.