Changeset 3398 for LTS/Language.ma


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

state relation with stack relation uptaded

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3397 r3398  
    515515∀l1,l2 : list (ActionLabel × (Instructions p)).
    516516associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
    517 option (Prop × (list CostLabel)) ≝
    518 λp,cont1,cont2,m,abs,keep.
    519 foldr2 ??? 〈True,abs〉 cont1 cont2
     517list (list CostLabel) →  option (Prop × (list CostLabel) × (list (list CostLabel))) ≝
     518λp,cont1,cont2,m,keep,abs_top,abs_tail.
     519foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2
    520520 (λ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 ?〉
    523524   | Some w ⇒
    524525      match \fst z with
    525526       [ ret_act opt_x ⇒
    526527           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'
    529530           | 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'
    531532           ]
    532533       | cost_act opt_x ⇒
    533534           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       
    538547
    539548definition 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 ?) keep with
    543 [ Some x ⇒ let 〈prf1,l'〉 ≝ x in
    544            prf1 ∧ call_post_clean … (code … st2) m keep l' = return 〈l,(code … st1)〉
    545            ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2
     549associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) →
     550relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
     551match 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'
    546555| None ⇒ False
    547556].
     
    652661lemma correctness : ∀p,p',prog.
    653662let 〈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.
    655664∀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'.
     665state_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'.
     667state_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'.
     672xxxxxx
    662673#p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans
    663674#s1 #s2 #s1' #l #t lapply l -l lapply s1' -s1' elim t
     
    669680  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
    670681  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
    671   normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2
    672   >m_return_bind normalize nodelta
    673   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 ?????) [ #_ **** ]
    674685  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
    675   cases l1' (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
    676   [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;
    678689    normalize * /2/ ] *
    679   [ (*#Hio11 #_ #EQcont11 #H*) normalize nodelta ***** #EQ destruct(EQ)
     690  [ #EQconts1' normalize nodelta ***** #EQ destruct(EQ)
    680691    #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1')
    681692    [
     
    692703    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11
    693704    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
    695707        normalize nodelta % // % // % // @EQcode_c_st12 ]
    696708    #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'}
     
    701713    whd in match (get_costlabels_of_trace ????);
    702714    whd in match (get_costlabels_of_trace ????); >EQcosts %
    703   | #lbl #Hiost11 #_ #EQcontst11 #H normalize nodelta ****** #EQ destruct(EQ)
     715  | #lbl #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
    704716    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1')
    705717    [
     
    714726    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio
    715727    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
    717730        normalize nodelta % // % // % // @EQcode_c_st12 ]
    718731    #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'}
     
    766779          cases daemon (*TODO*)
    767780        | 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
    769783           * [ #_ #l3'
    770784    cases(bind_inversion ????? H) in ⊢ ?;
Note: See TracChangeset for help on using the changeset viewer.