Changeset 3398 for LTS/Language.ma
 Timestamp:
 Nov 21, 2013, 8:56:45 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3397 r3398 515 515 ∀l1,l2 : list (ActionLabel × (Instructions p)). 516 516 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → 517 option (Prop × (list CostLabel)) ≝518 λp,cont1,cont2,m, abs,keep.519 foldr2 ??? 〈True,abs 〉 cont1 cont2517 list (list CostLabel) → option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ 518 λp,cont1,cont2,m,keep,abs_top,abs_tail. 519 foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 520 520 (λx,y,z. 521 match call_post_clean p (\snd z) m keep (\snd x) with 522 [ None ⇒ 〈False,nil ?〉 521 let 〈cond,abs_top',abs_tail'〉 ≝ x in 522 match call_post_clean p (\snd z) m keep abs_top' with 523 [ None ⇒ 〈False,nil ?,nil ?〉 523 524  Some w ⇒ 524 525 match \fst z with 525 526 [ ret_act opt_x ⇒ 526 527 match ret_costed_abs keep opt_x with 527 [ Some lbl ⇒ 〈\fst y = \fst z ∧ \fst x∧ \snd w = \snd y ∧528 get_element … m lbl = lbl :: (\fst w),(nil ?) 〉528 [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ 529 get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 529 530  None ⇒ 530 〈\fst y = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉531 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 531 532 ] 532 533  cost_act opt_x ⇒ 533 534 match opt_x with 534 [ None ⇒ 〈\fst y = \fst z ∧ \fst x ∧ \snd w = \snd y,\fst w〉 535  Some xx ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧ 536 get_element … m xx = xx :: (\fst w),(nil ?)〉] 537  _ ⇒ (* dummy *) 〈False,nil ?〉]]). 535 [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 536  Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ 537 get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] 538  _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). 539 (* in input : 540 abs_top is the list of labels to be propageted to the deepest level of the call stack 541 abs_tail are the lists of labels to be propagated to the levels "below" the deepest level 542 in output : 543 abs_top is the list of labels to be propageted from the current level of the call stack 544 abs_tail are the lists of labels to be propagated from the levels "below" the current level 545 *) 546 538 547 539 548 definition state_rel : ∀p. 540 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → 541 relation (state p) ≝ λp,m, l,keep,st1,st2.542 match check_continuations ? (cont ? st1) (cont … st2) m (nil ?) keepwith543 [ Some x ⇒ let 〈prf1, l'〉 ≝ x in544 prf1 ∧ call_post_clean … (code … st2) m keep l' = return 〈l,(code … st1)〉545 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 549 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) → 550 relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. 551 match check_continuations ? (cont ? st1) (cont … st2) m keep (nil ?) (nil ?) with 552 [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in 553 prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 554 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' 546 555  None ⇒ False 547 556 ]. … … 652 661 lemma correctness : ∀p,p',prog. 653 662 let 〈t_prog,m,keep〉 ≝ trans_prog … prog in 654 ∀s1,s2,s1' : state p.∀ l.663 ∀s1,s2,s1' : state p.∀abs_top,abs_tail. 655 664 ∀t : raw_trace (operational_semantics … p' prog) s1 s2. 656 state_rel … m l keep s1 s1' → 657 ∃l'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. 658 state_rel … m l' keep s2 s2' ∧ 659 l @ (map_labels_on_trace m (get_costlabels_of_trace … t)) = 660 (get_costlabels_of_trace … t') @ l' 661 ∧ len … t = len … t'. 665 state_rel … m keep abs_top abs_tail s1 s1' → 666 ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. 667 state_rel … m keep abs_top' abs_tail' s2 s2' ∧ 668 (foldr … (append …) (nil ?) (rev … abs_tail')) @ abs_top' @ 669 (map_labels_on_trace m (get_costlabels_of_trace … t)) = 670 (get_costlabels_of_trace … t') @ abs_top @ (foldr … (append …) (nil ?) abs_tail) ∧ 671 len … t = len … t'. 672 xxxxxx 662 673 #p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans 663 674 #s1 #s2 #s1' #l #t lapply l l lapply s1' s1' elim t … … 669 680 whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); 670 681 inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' 671 normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2672 >m_return_bind normalize nodelta673 inversion (call_post_clean ?????) [ #_ **** ]682 normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????); 683 inversion(check_continuations ??????) [ #_ *] * #H1 #l2 #EQHl2 684 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ **** ] 674 685 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 675 cases l1' (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta676 [1,4: [ #x #y ] (*#_ #_ #_ #H*) ****677  #x cases (ret_costed_abs ??) normalize nodelta [#c] *****[*] #EQ @⊥ >EQ in Hl1;686 cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta 687 [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) **** 688  #x #_ cases (ret_costed_abs ??) normalize nodelta [#c] *****[*] #EQ @⊥ >EQ in Hl1; 678 689 normalize * /2/ ] * 679 [ (*#Hio11 #_ #EQcont11 #H*)normalize nodelta ***** #EQ destruct(EQ)690 [ #EQconts1' normalize nodelta ***** #EQ destruct(EQ) 680 691 #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1') 681 692 [ … … 692 703 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 693 704 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …) 694 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 705 [2: whd whd in match check_continuations; normalize nodelta 706 change with (check_continuations ??????) in match (foldr2 ???????); >EQHl2 695 707 normalize nodelta % // % // % // @EQcode_c_st12 ] 696 708 #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'} … … 701 713 whd in match (get_costlabels_of_trace ????); 702 714 whd in match (get_costlabels_of_trace ????); >EQcosts % 703  #lbl # Hiost11 #_ #EQcontst11 #Hnormalize nodelta ****** #EQ destruct(EQ)715  #lbl #EQconts1' normalize nodelta ****** #EQ destruct(EQ) 704 716 #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1') 705 717 [ … … 714 726 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio 715 727 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …) 716 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 728 [2: whd whd in match check_continuations; normalize nodelta 729 change with (check_continuations ??????) in match (foldr2 ???????); >EQHl2 717 730 normalize nodelta % // % // % // @EQcode_c_st12 ] 718 731 #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'} … … 766 779 cases daemon (*TODO*) 767 780  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) 768 whd in match ret_costed_abs; normalize nodelta 781 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta 782 % // % // % [ % // % //] >EQcode12 <EQtrans 769 783 * [ #_ #l3' 770 784 cases(bind_inversion ????? H) in ⊢ ?;
Note: See TracChangeset
for help on using the changeset viewer.