Changeset 2938 for src/ERTLptr/ERTLptrToLTLProof.ma
 Timestamp:
 Mar 22, 2013, 2:11:59 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2930 r2938 102 102 103 103 definition state_rel : fixpoint_computer → coloured_graph_computer → 104 ertlptr_program → (Σb:block.block_region b = Code) → label →105 state ERTL_state → state LTL_LIN_state → Prop ≝104 ertlptr_program → 105 (Σb:block.block_region b = Code) → label → state ERTL_state → state LTL_LIN_state → Prop ≝ 106 106 λfix_comp,build,prog,bl,pc,st1,st2. 107 107 ∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ … … 349 349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 350 350 ∀r: register. 351 let live ≝ 352 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in 351 let live ≝ 352 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 353 in 353 354 set_member (identifier RegisterTag) (eq_identifier RegisterTag) r 354 (\fst (live l)) = false →355 (\fst (livebefore … fn l live)) = false → 355 356 sigma_fb_state prog 356 357 (to_be_cleared_fb live l) … … 363 364 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 364 365 ∀r: Register. 365 let live ≝ 366 let live ≝ 366 367 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 367 368 in 368 set_member Register eq_Register r (\snd (live l)) = false →369 set_member Register eq_Register r (\snd (livebefore … fn l live)) = false → 369 370 sigma_fb_state prog 370 371 (to_be_cleared_fb live l) … … 377 378 axiom sigma_fb_state_insensitive_to_dead_carry: 378 379 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 379 let live ≝ 380 let live ≝ 380 381 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 381 382 in 382 set_member Register eq_Register RegisterCarry (\snd (live l)) = false →383 set_member Register eq_Register RegisterCarry (\snd (livebefore … fn l live)) = false → 383 384 sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) = 384 385 sigma_fb_state prog (to_be_cleared_fb live l) st. … … 386 387 lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false. 387 388 ** normalize #abs destruct /2/ 389 qed. 390 391 lemma eta_set_carry: 392 ∀P,st. set_carry P (carry P st) st = st. 393 #P * // 394 qed. 395 396 lemma set_carry_set_regs_commute: 397 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st). 398 #P * // 399 qed. 400 401 lemma eliminable_step_to_eq_livebefore_liveafter: 402 ∀fix_comp,colour,prog,fn. 403 let p_in ≝ 404 mk_prog_params ERTLptr_semantics prog 405 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 406 ∀st1: joint_abstract_status p_in. 407 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next. 408 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in 409 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) → 410 let liveafter ≝ analyse_liveness fix_comp (globals p_in) fn in 411 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true → 412 livebefore … fn pt liveafter = liveafter pt. 413 #fix_comp #colour #prog #fn #st1 #stms #next #stmt_at #Helim 414 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at; 415 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I) 416 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?); 417 whd in match eliminable; normalize nodelta >Helim % 388 418 qed. 389 419 … … 398 428 ∀st1 : joint_abstract_status p_in. 399 429 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in 400 ∀st1_no_pc,stms. 430 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next. 431 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) → 401 432 ∀Heval_seq_no_pc: 402 433 eval_seq_no_pc ERTLptr_semantics … … 423 454 (st_no_pc … st1)). 424 455 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn 425 #st1 #st1' * 456 #st1 #st1' #stms #next #stmt_at #Heval #Helim 457 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim) 458 #EQ_livebefore_after next 459 cases stms in Heval Helim; 426 460 try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim) 427 461 try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim) … … 466 500 whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) X 467 501 try (cases (split_orb_false … Helim) Helim #Helim1 #Helim2) 468 try (@sigma_fb_state_insensitive_to_dead_reg assumption)469 try (@sigma_fb_state_insensitive_to_dead_Reg assumption)470 try (@sigma_fb_state_insensitive_to_dead_carry assumption)502 try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption) 503 try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption) 504 try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption) 471 505 [1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ] 472 506 [1,2,3: 473 >sigma_fb_state_insensitive_to_dead_carry try assumption 474 @sigma_fb_state_insensitive_to_dead_reg assumption 475 4,5,6: (* BUG! *) 476 7: >sigma_fb_state_insensitive_to_dead_reg try assumption 507 >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption) 508 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 509 4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta 510 [2: #error #abs destruct (abs) ] 511 #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ 512 whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry 513 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 514 5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta 515 try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres 516 try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta 517 try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres 518 try (destruct (Hvres) @I) 519 [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I) 520 cases andb normalize nodelta #Hvres 521 9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres; 522 normalize nodelta try (#abs destruct(abs) @I) #Hvres ] 523 whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry 524 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 525 7: cases (split_orb_false … Helim1) Helim1 #Helim1 #Helim3 526 >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 527 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 528 8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 529 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ] 530 qed. 477 531 478 532 lemma make_ERTLptr_To_LTL_good_state_relation : … … 490 544 good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes 491 545 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») 492 init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)546 init_regs f_lbls f_regs good (state_rel fix_comp colour prog) 493 547 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)). 494 548 #fix_comp #colour #prog
Note: See TracChangeset
for help on using the changeset viewer.