Changeset 2851 for src/ERTLptr/ERTLptrToLTLProof.ma
 Timestamp:
 Mar 12, 2013, 4:13:21 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2849 r2851 220 220  whd in match next; normalize nodelta 221 221 ] 222 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) EQ st1' #n_cost222 whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) EQ #EQst1' #n_cost 223 223 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 224 224 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta … … 235 235 stacksizes) 236 236 cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧ 237 pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧237 pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧ 238 238 last_pop … st2' = last_pop … st2) 239 239 [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ] … … 257 257 [2,4: cases daemon (*THE EXTENSIONAL PROOF *)] 258 258 #st2_mid #EQst2_mid 259 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_ mid = cl_jump)259 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump) 260 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)} 272 [ @ltrue 3: @lfalse] 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 285 bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 286 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * 287 #nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 288 whd in EQmid1 : (??%%); destruct(EQmid1) 289 %{(taaf_step_jump … (taa_base …) …) I} 290 [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 291 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind 292 >EQcond % 293 3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc; 294 normalize nodelta whd in match fetch_statement; normalize nodelta 295 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind 296 >EQcond >m_return_bind normalize nodelta >m_return_bind 297 whd in match eval_statement_advance; normalize nodelta 298 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 299 cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1 300 >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool) 301 #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta 302 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto; 303 normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 304 >(pc_of_label_eq … EQt_fn1) >m_return_bind % 305 *: lapply n_cost whd in match as_costed; normalize nodelta 306 [ cut((mk_state_pc ERTL_semantics 307 (sigma_state prog f_lbls f_regs 308 (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn 309 (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) 310 (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 311 (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = 312 sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 313 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 314 (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta 315 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] 316 #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 317 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 318 (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *) 319  cut((mk_state_pc ERTL_semantics 320 (sigma_state prog f_lbls f_regs 321 (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn 322 (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) 323 (succ_pc ERTL_semantics (pc ERTLptr_semantics st2) 324 (point_of_succ ERTLptr_semantics 325 (point_of_pc ERTLptr_semantics 326 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 327 (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = 328 sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 329 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) 330 (point_of_succ ERTLptr_semantics 331 (point_of_pc ERTLptr_semantics 332 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 333 (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta 334 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ 335 >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 336 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) 337 (point_of_succ ERTLptr_semantics 338 (point_of_pc ERTLptr_semantics 339 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 340 (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *) 261 * #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 l2 >EQ2 in seq_pre_l EQmid; mid2 #seq_pre_l #EQmid 262 letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)) 263 cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid 264 %{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I} 265 [1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption] 266 cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *) 267 *: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption 341 268 ] 342 qed. *)269 qed. 343 270 344 271
Note: See TracChangeset
for help on using the changeset viewer.