# Changeset 3398

Ignore:
Timestamp:
Nov 21, 2013, 8:56:45 PM (8 years ago)
Message:

state relation with stack relation uptaded

File:
1 edited

Unmodified
Added
Removed
• ## LTS/Language.ma

 r3397 ∀l1,l2 : list (ActionLabel × (Instructions p)). associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → option (Prop × (list CostLabel)) ≝ λp,cont1,cont2,m,abs,keep. foldr2 ??? 〈True,abs〉 cont1 cont2 list (list CostLabel) →  option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ λp,cont1,cont2,m,keep,abs_top,abs_tail. foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 (λx,y,z. match call_post_clean p (\snd z) m keep (\snd x) with [ None ⇒ 〈False,nil ?〉 let 〈cond,abs_top',abs_tail'〉 ≝ x in match call_post_clean p (\snd z) m keep abs_top' with [ None ⇒ 〈False,nil ?,nil ?〉 | Some w ⇒ match \fst z with [ ret_act opt_x ⇒ match ret_costed_abs keep opt_x with [ Some lbl ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧ get_element … m lbl = lbl :: (\fst w),(nil ?)〉 [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 | None ⇒ 〈\fst y = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 ] | cost_act opt_x ⇒ match opt_x with [ None ⇒ 〈\fst y = \fst z ∧ \fst x ∧ \snd w = \snd y,\fst w〉 | Some xx ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧ get_element … m xx = xx :: (\fst w),(nil ?)〉] | _ ⇒ (* dummy *) 〈False,nil ?〉]]). [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). (* in input : abs_top is the list of labels to be propageted to the deepest level of the call stack abs_tail are the lists of labels to be propagated to the levels "below" the deepest level in output : abs_top is the list of labels to be propageted from the current level of the call stack abs_tail are the lists of labels to be propagated from the levels "below" the current level *) definition state_rel : ∀p. associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → relation (state p) ≝ λp,m,l,keep,st1,st2. match check_continuations ? (cont ? st1) (cont … st2) m (nil ?) keep with [ Some x ⇒ let 〈prf1,l'〉 ≝ x in prf1 ∧ call_post_clean … (code … st2) m keep l' = return 〈l,(code … st1)〉 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) → relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. match check_continuations ? (cont ? st1) (cont … st2) m keep (nil ?) (nil ?) with [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' | None ⇒ False ]. lemma correctness : ∀p,p',prog. let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀s1,s2,s1' : state p.∀l. ∀s1,s2,s1' : state p.∀abs_top,abs_tail. ∀t : raw_trace (operational_semantics … p' prog) s1 s2. state_rel … m l keep s1 s1' → ∃l'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. state_rel  … m l' keep s2 s2' ∧ l @ (map_labels_on_trace m (get_costlabels_of_trace … t)) = (get_costlabels_of_trace … t') @ l' ∧ len … t = len … t'. state_rel … m keep abs_top abs_tail s1 s1' → ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. state_rel  … m keep abs_top' abs_tail' s2 s2' ∧ (foldr … (append …) (nil ?) (rev … abs_tail')) @ abs_top' @ (map_labels_on_trace m (get_costlabels_of_trace … t)) = (get_costlabels_of_trace … t') @ abs_top @ (foldr … (append …) (nil ?) abs_tail) ∧ len … t = len … t'. xxxxxx #p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans #s1 #s2 #s1' #l #t lapply l -l lapply s1' -s1' elim t whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ **** ] normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????); inversion(check_continuations ??????) [ #_ *] * #H1 #l2 #EQHl2 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ **** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta cases l1' (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta [1,4: [ #x #y ] (*#_ #_ #_ #H*) **** | #x cases (ret_costed_abs ??) normalize nodelta [|#c] *****[|*] #EQ @⊥ >EQ in Hl1; cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) **** | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] *****[|*] #EQ @⊥ >EQ in Hl1; normalize * /2/ ] * [ (*#Hio11 #_ #EQcont11 #H*) normalize nodelta ***** #EQ destruct(EQ) [ #EQconts1' normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1') [ #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …) [2: whd whd in match check_continuations; normalize nodelta >EQHl2 [2: whd whd in match check_continuations; normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????);  >EQHl2 normalize nodelta % // % // % // @EQcode_c_st12 ] #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'} whd in match (get_costlabels_of_trace ????); whd in match (get_costlabels_of_trace ????); >EQcosts % | #lbl #Hiost11 #_ #EQcontst11 #H normalize nodelta ****** #EQ destruct(EQ) | #lbl #EQconts1' normalize nodelta ****** #EQ destruct(EQ) #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1') [ #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …) [2: whd whd in match check_continuations; normalize nodelta >EQHl2 [2: whd whd in match check_continuations; normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????);  >EQHl2 normalize nodelta % // % // % // @EQcode_c_st12 ] #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'} cases daemon (*TODO*) | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta % // % // % [ % // % //]  >EQcode12
Note: See TracChangeset for help on using the changeset viewer.