Changeset 3535
Legend:
- Unmodified
- Added
- Removed
-
LTS/Final.ma
r3531 r3535 14 14 15 15 include "Simulation.ma". 16 include "Vm.ma". 16 include "Vm.ma". 17 include "Lang_meas.ma". 17 18 18 19 theorem cerco: … … 76 77 #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds 77 78 #R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi' 78 cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi') 79 cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi') 80 [2: #H cases Hclass >H #ABS cases(ABS (refl …)) ] 79 81 #sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas' 80 82 %{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts … … 83 85 qed. 84 86 87 lemma is_permutation_mem : ∀A :DeqSet. 88 ∀l1,l2 : list A.∀x : A.mem … x l1 → 89 is_permutation A l1 l2 → mem … x l2. 90 cases daemon 91 qed. 92 93 definition is_abelian ≝ λM : monoid. 94 ∀x,y : M.op … M x y = op … M y x. 95 96 lemma 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). 99 cases daemon 100 qed. 101 102 lemma 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 ?) → 107 is_permutation B (dependent_map … l1 f) (dependent_map … l2 g). 108 [2: @(is_permutation_mem … perm) //] 109 cases daemon 110 qed. 111 112 theorem final_cerco : 113 (* for all programs in the imperative language (possibly with call non post labelled) *) 114 ∀p,p',prog. 115 no_duplicates_labels … prog → 116 117 (* let t_prog be the same program in which all calls are post-labelled *) 118 let 〈t_prog,m,keep〉 ≝ trans_prog … prog in 119 120 (* Let S1 be the operational semantics of the source code *) 121 let S1 ≝ operational_semantics p p' prog in 122 123 (* Let S2 be the operational semantics of the soource code with call post labelled *) 124 let 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 *) 129 let 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 *) 137 let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧ 138 Srel … 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 *) 144 is_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' 197 lapply(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'' 200 cases(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 ] 211 qed. 212 85 213 (* TODO: 86 1. Monoide di costo: eliminare. 87 2. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita' 88 sull'assembler 214 1. Spostare chop e eliminare suffix. 215 2. La block cost non fallisce in caso di I/O. 89 216 3. Integrare la prima passata di Language nel risultato finale 90 217 5. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato) -
LTS/Language.ma
r3531 r3535 1959 1959 ] |1,4:] 1960 1960 %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct 1961 ]1962 |*: cases daemon1963 ] cases daemon1964 qed.1965 1966 (*1967 1961 | 1968 1962 #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 … … 2012 2006 >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta 2013 2007 >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // 2014 ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen2015 #stack_safety #pre_t' %{abs_top1}2008 ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen 2009 #stack_safety #pre_t' #Hsil %{abs_top1} 2016 2010 %{s2'} %{(t_ind … t')} 2017 2011 [ @hide_prf @(cond_true … EQcode_s1') // 2018 2012 | 2019 ] 2013 ] % [ 2020 2014 % [ % 2021 2015 [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} … … 2030 2024 ]] 2031 2025 %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 ] 2032 2031 | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 2033 2032 #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t … … 2075 2074 >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta 2076 2075 >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // 2077 ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety2078 #pre_t' 2076 ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety 2077 #pre_t' #Hsil 2079 2078 %{abs_top1} %{s2'} %{(t_ind … t')} 2080 2079 [ @hide_prf @(cond_false … EQcode_s1') // 2081 2080 | 2082 ] 2081 ] % [ 2083 2082 % [ % 2084 2083 [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} … … 2092 2091 %{tl1} % // whd in EQk1 : (??%%); destruct // 2093 2092 ] ] 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 ] 2095 2098 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct 2096 2099 #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail … … 2140 2143 % // 2141 2144 ] 2142 #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety2143 #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') // |] % [ 2145 2148 % [ % 2146 2149 [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} … … 2154 2157 %{tl1} % // whd in EQk1 : (??%%); destruct // 2155 2158 ] ] 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 ] 2157 2164 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct 2158 2165 #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail … … 2200 2207 % // % // % // % [2: %] // 2201 2208 ] 2202 #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety2203 #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') // |] % [ 2205 2212 % [ % 2206 2213 [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} … … 2211 2218 cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // 2212 2219 ]] 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 ] 2214 2225 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12 2215 2226 #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre … … 2257 2268 [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) % 2258 2269 ] 2259 #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety2260 #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') // |] % [ 2262 2273 % [ % 2263 2274 [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} … … 2271 2282 %{tl1} % // whd in EQk1 : (??%%); destruct // 2272 2283 ]] 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 ] 2274 2289 | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 2275 2290 #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ) … … 2341 2356 #r_t' #EQcode_s1' 2342 2357 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2343 #EQstore11 #EQio_11 #EQ destruct2358 #EQstore11 #EQio_111 #EQ destruct 2344 2359 cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs) 2345 2360 [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ] 2346 #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety2347 #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')} 2348 2363 [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') // 2349 | ] 2364 | ] % [ 2350 2365 % [ % 2351 2366 [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} … … 2360 2375 % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] 2361 2376 ]] 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 ] 2363 2382 | #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12 2364 2383 [1,2,3,4,5,6,7,9: … … 2437 2456 ] 2438 2457 ] 2439 #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety2440 #pre_t' %{abs_top'''}2458 #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety 2459 #pre_t' #Hsil %{abs_top'''} 2441 2460 %{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/ ] % [ 2443 2462 % [ % 2444 2463 [ % [2: whd in ⊢ (??%%); >EQlen %] … … 2455 2474 ]] 2456 2475 %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 ] 2457 2481 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2458 2482 ] … … 2556 2580 ] 2557 2581 ] 2558 #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety12559 #pre_t1' 2582 #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1 2583 #pre_t1' #Hsil1 2560 2584 whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ] 2561 2585 ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?); … … 2620 2644 abs_tail_cont abs_top'''') 2621 2645 [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')))} 2624 2648 [3: @hide_prf @(call … EQcode_st1' … EQenv_it') // 2625 2649 |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') // 2626 2650 |2,4: skip 2627 ] 2651 ] % [ 2628 2652 % [ % 2629 2653 [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 // … … 2653 2677 ] 2654 2678 ] 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 ] 2684 qed. 2685 2659 2686 2660 2687 lemma silent_in_silent : ∀p,p',prog. -
LTS/Traces.ma
r3531 r3535 274 274 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. 275 275 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 276 definition actionlabel_to_costlabel ≝ 277 λl : ActionLabel.match l with 283 278 [ call_act f c ⇒ [ c ] 284 279 | ret_act x ⇒ match x with … … 290 285 | None ⇒ [] 291 286 ] 292 ] @ tl 287 ]. 288 289 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) 290 (t : raw_trace S st1 st2) on t : list CostLabel ≝ 291 match 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 293 296 ]. 294 297 … … 636 639 637 640 definition 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 ≝ 639 642 λS,si,s1,s3,sn,t. 640 643 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn. -
LTS/Vm.ma
r3524 r3535 685 685 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ 686 686 λ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. 688 688 689 689 definition big_op: ∀M: monoid. list M → M ≝ … … 821 821 normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_ 822 822 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 * 824 825 [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)) 826 828 * 827 829 ] … … 882 884 qed. 883 885 886 (* 884 887 definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ 885 888 λa.match a with … … 888 891 | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]] 889 892 ]. 893 *) 890 894 891 895 lemma get_cost_label_of_trace_tind : ∀S : abstract_status. … … 922 926 (* For every pre_measurable, terminated trace *) 923 927 ∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2. 924 terminated_trace … t → pre_measurable_trace … t →928 terminated_trace … t → 925 929 926 930 (* Let labels be the costlabels observed in the trace (last one excluded) *) … … 951 955 ] 952 956 #p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * 953 #l1 * #prf1 * #EQ destruct #Hlabelled957 #l1 * #prf1 ** #EQ destruct #Hlabelled 954 958 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 955 959 [2: >get_cost_label_append >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled) … … 1200 1204 ] 1201 1205 #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) 1206 cases 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) 1204 1209 #c1 #EQc1 >rewrite_in_dependent_map 1205 [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil ent_ti0) in ⊢ (??%?);1210 [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?); 1206 1211 >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?); 1207 1212 >get_cost_label_of_trace_tind in ⊢ (??%?); 1208 >(get_cost_label_silent_is_empty … sil ent_t3n) in ⊢ (??%?);1213 >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?); 1209 1214 >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?); 1210 1215 whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); … … 1215 1220 >(big_op_associative ? [?]) #a1 >act_op #HR 1216 1221 letin actsl ≝ (dependent_map ????); 1217 @(static_dynamic_inv … EQmap … (t1 2 @ t_ind … prf2 (t_base …)) … actsl… HR)1218 [ / 6width=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) 1220 1225 change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?); 1221 1226 change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?); … … 1224 1229 change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?); 1225 1230 change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?); 1226 <append_associative #H @(sub_trace_premeasurable_l1 … H) 1227 | cases s1 in prf1 t1 2; [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] * 1228 1233 [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %); 1229 1234 #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr -
LTS/costs.ma
r3524 r3535 16 16 17 17 record monoid: Type[1] ≝ 18 { carrier :> Type[0]18 { carrier :> DeqSet 19 19 ; op: carrier → carrier → carrier 20 20 ; e: carrier
Note: See TracChangeset
for help on using the changeset viewer.