Changeset 3535


Ignore:
Timestamp:
Mar 16, 2015, 4:30:28 PM (5 years ago)
Author:
piccolo
Message:

final statement of cerco with the first pass integrated in place

Location:
LTS
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3531 r3535  
    1414
    1515include "Simulation.ma".
    16 include "Vm.ma".   
     16include "Vm.ma".
     17include "Lang_meas.ma".
    1718
    1819theorem cerco:
     
    7677#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
    7778#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
    78 cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
     79cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi')
     80[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
    7981#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
    8082%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
     
    8385qed. 
    8486
     87lemma is_permutation_mem : ∀A :DeqSet.
     88∀l1,l2 : list A.∀x : A.mem … x l1 →
     89is_permutation A l1 l2 → mem … x l2.
     90cases daemon
     91qed.
     92
     93definition is_abelian ≝ λM : monoid.
     94∀x,y : M.op … M x y = op … M y x.
     95
     96lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
     97∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
     98(〚l1〛 a) = (〚l2〛 a).
     99cases daemon
     100qed.
     101
     102lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
     103∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
     104∀perm : is_permutation A l1 l2.
     105(∀a : A.
     106 ∀prf : mem … a l1.f a prf = g a ?) →
     107is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).
     108[2: @(is_permutation_mem … perm) //]
     109cases daemon
     110qed.
     111
     112theorem final_cerco :
     113(* for all programs in the imperative language (possibly with call non post labelled) *)
     114∀p,p',prog.
     115no_duplicates_labels … prog →
     116
     117(* let t_prog be the same program in which all calls are post-labelled *)
     118let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     119
     120(* Let S1 be the operational semantics of the source code  *)
     121let S1 ≝ operational_semantics p p' prog in
     122
     123(* Let S2 be the operational semantics of the soource code with call post labelled  *)
     124let S2 ≝ operational_semantics p p' t_prog in
     125
     126(* for all assmbler programs *)
     127∀p_asm,p_asm',prog_asm.
     128(* Let S3 be the operational semantics of the compiled code  *)
     129let S3 ≝ asm_operational_semantics p_asm p_asm' prog_asm in
     130
     131(* If the simulation conditions between the source with call post-labelled and compiled
     132    code holds (i.e. if the compiler is correct after the first pass) *)
     133∀rel: relations S2 S3. simulation_conditions … rel →
     134
     135(* let REL be semantical relation between the states of the source program and
     136   the states of compiled code *)
     137let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
     138Srel … rel si'' si' in
     139
     140 (* Given an abstract interpretation framework for the compiled code *)
     141∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
     142
     143(* If the abstract instructions monoid is abelian *)
     144is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) → 
     145 
     146 (* If the static analysis does not fail *)
     147∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
     148
     149 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
     150   equivalently, whose state after the initial labelled transition is s1
     151   and whose state after the final labelled transition is s2  *)
     152 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
     153 measurable … s1 s2 … t →
     154
     155 (* For each target non I/O state si' in relation with the source state si *)
     156 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
     157
     158 (* There exists a corresponding target trace starting from si' *)
     159 ∃sn'. ∃t': raw_trace … si' sn'.
     160  REL sn sn' ∧
     161 
     162   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled
     163     (last one excluded), that can be computed from the costlabels observed in the trace of
     164     the source language *)
     165 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
     166 
     167  (*The labels emitted by the trace of the source with all call post-labelled
     168    is a permutation of the labels emitted by the target trace (excluded the last one) *)
     169  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
     170 
     171 (* that has a measurable fragment starting in s1' and ending in s2' *)
     172 ∃s1',s2'. measurable … s1' s2' … t' ∧
     173
     174(* Let abs_actions be the list of statically computed abstract actions
     175   associated to each label in labels. *)
     176 ∀abs_actions.
     177  abs_actions =
     178   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
     179
     180 (* Given an abstract state in relation with the first state of the measurable
     181    fragment *)
     182 ∀a1.R s1' a1 →
     183
     184 (* The final state of the measurable fragment is in relation with the one
     185   obtained by applying every semantics in abs_trace. *)
     186 R s2' (〚abs_actions〛 a1).
     187[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
     188    lapply(is_permutation_mem … prf … perm) -prf #prf
     189    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
     190    #lbl' #pc * #Hmem #EQ destruct
     191    >(proj1 … (static_analisys_ok … EQmap … Hmem))
     192    @(proj2 … (static_analisys_ok … EQmap … Hmem))
     193]
     194#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
     195#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
     196#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
     197lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
     198#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
     199#Hperm * #s1'' * #s2'' #meas_t''
     200cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
     201#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
     202%{sn'} %{t'} %
     203[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
     204 [ @(is_permutation_transitive … Hperm) >EQcost // ]
     205 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
     206 >(action_on_permutation … abelian)
     207 [@Hcerco [% | assumption]
     208 | >EQactions -EQactions @is_permutation_dependent_map //
     209 |
     210 ]
     211qed.
     212
    85213(* TODO:
    86 1. Monoide di costo: eliminare.
    87 2. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita'
    88    sull'assembler
     2141. Spostare chop e eliminare suffix.
     2152. La block cost non fallisce in caso di I/O.
    892163. Integrare la prima passata di Language nel risultato finale
    902175. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
  • LTS/Language.ma

    r3531 r3535  
    19591959          ] |1,4:]
    19601960    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    1961     ]
    1962   |*: cases daemon
    1963   ] cases daemon
    1964 qed.
    1965 
    1966 (*
    19671961  |
    19681962   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     
    20122006        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20132007        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2014     ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
    2015       #stack_safety #pre_t' %{abs_top1}
     2008    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen
     2009      #stack_safety #pre_t' #Hsil %{abs_top1}
    20162010    %{s2'} %{(t_ind … t')}
    20172011    [ @hide_prf @(cond_true … EQcode_s1') //
    20182012    |
    2019     ]
     2013    ] % [
    20202014    % [ %
    20212015    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    20302024    ]]
    20312025    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2026    ]
     2027    #h inversion h in ⊢ ?;
     2028    [#H1 #H2 #H3 #H4 #H5 #H6 destruct
     2029    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct
     2030    ]
    20322031  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    20332032    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    20752074        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20762075        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2077     ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
    2078     #pre_t'
     2076    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety
     2077    #pre_t' #Hsil
    20792078    %{abs_top1} %{s2'} %{(t_ind … t')}
    20802079    [ @hide_prf @(cond_false … EQcode_s1') //
    20812080    |
    2082     ]
     2081    ] % [
    20832082    % [ %
    20842083    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    20922091      %{tl1} % // whd in EQk1 : (??%%); destruct //
    20932092    ] ]
    2094     %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2093    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2094    #h inversion h in ⊢ ?;
     2095    [ #H21 #H22 #H23 #H24 #H25 #H26 destruct
     2096    | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
     2097    ]
    20952098 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    20962099   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    21402143       % //
    21412144   ]
    2142    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2143    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2144    [ @hide_prf @(loop_true … EQcode_s1') // |]
     2145   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2146   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2147   [ @hide_prf @(loop_true … EQcode_s1') // |] % [
    21452148   % [ %
    21462149   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    21542157      %{tl1} % // whd in EQk1 : (??%%); destruct //
    21552158   ] ]
    2156    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2159   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2160   #h inversion h in ⊢ ?;
     2161   [ #H41 #H42 #H43 #H44 #H45 #H46 destruct
     2162   | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
     2163   ]
    21572164 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    21582165   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    22002207        % // % // % // % [2: %] //
    22012208   ]
    2202    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2203    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2204    [ @hide_prf @(loop_false … EQcode_s1') // |]
     2209   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2210   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2211   [ @hide_prf @(loop_false … EQcode_s1') // |] % [
    22052212   % [ %
    22062213   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    22112218     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    22122219   ]]
    2213    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2220   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct]
     2221   #h inversion h in ⊢ ?;
     2222   [ #H61 #H62 #H63 #H64 #H65 #H66 destruct
     2223   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct
     2224   ]
    22142225 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    22152226   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     
    22572268       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    22582269   ]
    2259    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2260    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2261    [ @hide_prf @(io_in … EQcode_s1') // |]
     2270   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2271   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2272   [ @hide_prf @(io_in … EQcode_s1') // |] % [
    22622273   % [ %
    22632274   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    22712282      %{tl1} % // whd in EQk1 : (??%%); destruct //
    22722283   ]]
    2273    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2284   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2285   #h inversion h in ⊢ ?;
     2286   [ #H81 #H82 #H83 #H84 #H85 #H86 destruct
     2287   | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct
     2288   ]
    22742289  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    22752290    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
     
    23412356   #r_t' #EQcode_s1'
    23422357  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    2343   #EQstore11 #EQio_11 #EQ destruct
     2358  #EQstore11 #EQio_111 #EQ destruct
    23442359  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    23452360  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2346   #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2347   #pre_t' %{abs_top1} %{s2'} %{(t_ind … t')}
     2361  #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2362  #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
    23482363  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    2349   | ]
     2364  | ] % [
    23502365  % [ %
    23512366  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    23602375    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    23612376  ]]
    2362   %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2377  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2378  #h inversion h in ⊢ ?;
     2379  [ #H101 #H102 #H103 #H104 #H105 #H106 destruct
     2380  | #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct
     2381  ]
    23632382| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    23642383  [1,2,3,4,5,6,7,9:
     
    24372456            ]
    24382457          ]
    2439           #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
    2440           #pre_t' %{abs_top'''}
     2458          #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety
     2459          #pre_t' #Hsil %{abs_top'''}
    24412460          %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    2442           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
     2461          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [
    24432462          % [ %
    24442463          [ % [2: whd in ⊢ (??%%); >EQlen %]
     
    24552474          ]]
    24562475          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
     2476          ]
     2477          #h inversion h in ⊢ ?;
     2478          [ #H121 #H122 #H123 #H124 #H125 #H126 destruct
     2479          | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct
     2480          ]
    24572481        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    24582482        ]
     
    25562580          ]
    25572581     ]
    2558      #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
    2559      #pre_t1'
     2582     #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2583     #pre_t1' #Hsil1
    25602584     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
    25612585     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     
    26202644             abs_tail_cont abs_top'''')
    26212645     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2622      #abs_top_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
    2623      #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2646     #abs_top_1 * #st5' * #t2' ***** #Hst5_st5' #EQcosts'
     2647     #EQlen'  #stack_safety2 #pre_t2' #Hsil2 %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    26242648     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    26252649     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
    26262650     |2,4: skip
    2627      ]
     2651     ] % [
    26282652     % [ %
    26292653     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
     
    26532677       ]
    26542678     ]
    2655 ]
    2656 qed.
    2657 
    2658 *)
     2679  ] #h inversion h in ⊢ ?;
     2680  [ #H141 #H142 #H143 #H144 #H145 #H146 destruct
     2681  |#H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 destruct
     2682  ]
     2683
     2684qed.
     2685
    26592686
    26602687lemma silent_in_silent : ∀p,p',prog.
  • LTS/Traces.ma

    r3531 r3535  
    274274λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    275275
    276 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
    277 (t : raw_trace S st1 st2) on t : list CostLabel ≝
    278 match t with
    279 [ t_base st ⇒ [ ]
    280 | t_ind st1' st2' st3' l prf t' ⇒
    281     let tl ≝ get_costlabels_of_trace … t' in
    282     match l with
     276definition actionlabel_to_costlabel ≝
     277λl : ActionLabel.match l with
    283278    [ call_act f c ⇒ [ c ]
    284279    | ret_act x ⇒ match x with
     
    290285                  | None ⇒ []
    291286                  ]
    292    ] @ tl
     287   ].
     288
     289let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
     290(t : raw_trace S st1 st2) on t : list CostLabel ≝
     291match t with
     292[ t_base st ⇒ [ ]
     293| t_ind st1' st2' st3' l prf t' ⇒
     294    let tl ≝ get_costlabels_of_trace … t' in
     295    actionlabel_to_costlabel l  @ tl
    293296].
    294297
     
    636639
    637640definition measurable :
    638  ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
     641 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
    639642λS,si,s1,s3,sn,t.
    640643 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
  • LTS/Vm.ma

    r3524 r3535  
    685685definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
    686686λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
    687 ∧ is_costlabelled_act l.
     687∧ is_costlabelled_act l ∧ pre_measurable_trace … t1.
    688688
    689689definition big_op: ∀M: monoid. list M → M ≝
     
    821821      normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
    822822      inversion(emits_labels … i)
    823       [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
     823      [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
     824        normalize nodelta >EQ1 *
    824825        [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
    825       | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
     826      | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta
     827        >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
    826828        *
    827829      ]
     
    882884qed.
    883885
     886(*
    884887definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
    885888λa.match a with
     
    888891| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
    889892].
     893*)
    890894
    891895lemma get_cost_label_of_trace_tind : ∀S : abstract_status.
     
    922926(* For every pre_measurable, terminated trace *)
    923927∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
    924  terminated_trace … t → pre_measurable_trace … t →
     928 terminated_trace … t →
    925929
    926930(* Let labels be the costlabels observed in the trace (last one excluded) *)
     
    951955]
    952956#p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
    953 #l1 * #prf1 * #EQ destruct #Hlabelled
     957#l1 * #prf1 ** #EQ destruct #Hlabelled
    954958>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
    955959[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
     
    12001204]
    12011205#p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
    1202 cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2
    1203 ***** #EQ destruct #Hl1 #Hl2 #_ #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1)
     1206cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2
     1207******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
     1208#acts cases(actionlabel_ok … Hl1)
    12041209#c1 #EQc1 >rewrite_in_dependent_map
    1205 [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?);
     1210[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?);
    12061211     >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
    12071212      >get_cost_label_of_trace_tind in ⊢ (??%?);
    1208      >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
     1213     >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?);
    12091214     >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
    12101215     whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?);
     
    12151220 >(big_op_associative ? [?]) #a1 >act_op #HR
    12161221letin actsl ≝ (dependent_map ????);
    1217 @(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
    1218   [ /6 width=6 by conj, ex_intro/
    1219   | lapply(sub_trace_premeasurable_l2 … premeas)
     1222@(static_dynamic_inv … EQmap … (t13 @ (t_ind … prf2 (t_base …))) … HR)
     1223  [ /7 width=6 by conj, ex_intro/
     1224  (*| lapply(sub_trace_premeasurable_l2 … pre_t13)
    12201225    change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?);
    12211226    change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?);
     
    12241229    change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?);
    12251230    change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?);
    1226     <append_associative #H @(sub_trace_premeasurable_l1 … H)
    1227   | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
     1231    <append_associative #H @(sub_trace_premeasurable_l1 … H) *)
     1232  | cases s1 in prf1 t13; [3: #st1] cases s0 [3,6,9: #st0] *
    12281233    [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
    12291234        #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr
  • LTS/costs.ma

    r3524 r3535  
    1616
    1717record monoid: Type[1] ≝
    18  { carrier :> Type[0]
     18 { carrier :> DeqSet
    1919 ; op: carrier → carrier → carrier
    2020 ; e: carrier
Note: See TracChangeset for help on using the changeset viewer.