| 1 | include "Clight/toCminorCorrectness.ma". |
|---|
| 2 | include "common/FEMeasurable.ma". |
|---|
| 3 | include "Clight/Clight_classified_system.ma". |
|---|
| 4 | include "Cminor/Cminor_classified_system.ma". |
|---|
| 5 | |
|---|
| 6 | include "common/ExtraMonads.ma". |
|---|
| 7 | |
|---|
| 8 | axiom clight_cminor_rel_labelled : ∀ge,ge',INV,s,s'. |
|---|
| 9 | clight_cminor_rel ge ge' INV s s' → |
|---|
| 10 | Clight_labelled s = Cminor_labelled s'. |
|---|
| 11 | (* Large inversion required; perhaps better Russell-style |
|---|
| 12 | #Xge #Xge' #XINV #Xs #Xs' * // |
|---|
| 13 | #ge #ge' #INV #cl_s #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #fInv #sInv #kInv #_ #u #Hfrgl #Hfrfn #TrFn #su #su' #lu #lu' #lbls #flag #tI #ts #_ #te #_ #_ #Em #_ #_ #_ #_ #_ #_ #_ #_ |
|---|
| 14 | -TrFn cases cl_s in tI ts ⊢ %; |
|---|
| 15 | [ | #e1 #e2 | #oe #e1 #es | #s1 #s2 | #e1 #s1 #s2 | #e1 #s1 | #e1 #s1 | #s1 #e1 #s2 #s3 | | | #oe | #e1 #ls | #lb #s1 | #lb | #cl #s1 ] |
|---|
| 16 | #tI |
|---|
| 17 | whd in ⊢ (??%? → ?); #E destruct // |
|---|
| 18 | [ @('bind_inversion E) -E #e2' #_ #E |
|---|
| 19 | @('bind_inversion E) -E * [ #id #L | #e' ] #_ #E |
|---|
| 20 | whd in E:(??%?); [@('bind_inversion E) -E #e2'' #_ #E whd in E:(??%%); destruct // |
|---|
| 21 | | cases (type_eq_dec ??) in E; #H #E whd in E:(??%%); destruct // |
|---|
| 22 | ] |
|---|
| 23 | | @('bind_inversion E) -E #x1 #_ #E |
|---|
| 24 | @('bind_inversion E) -E #x2 #_ #E |
|---|
| 25 | @('bind_inversion E) -E #x3 #_ #E |
|---|
| 26 | cases oe in E; [ | #e1 #E @('bind_inversion E) -E * [ #xx ] #x4 #_ ] |
|---|
| 27 | #E whd in E:(??%%); destruct // |
|---|
| 28 | cases (alloc_tmp ???) in E; #x5 #x6 |
|---|
| 29 | *) |
|---|
| 30 | |
|---|
| 31 | definition clight_to_cminor_measurable_sim : meas_sim ≝ |
|---|
| 32 | mk_meas_sim |
|---|
| 33 | Clight_pcs |
|---|
| 34 | Cminor_pcs |
|---|
| 35 | (λp,p'. clight_to_cminor p = OK … p') |
|---|
| 36 | clight_cminor_inv |
|---|
| 37 | clight_cminor_rel |
|---|
| 38 | ? |
|---|
| 39 | ? |
|---|
| 40 | ? |
|---|
| 41 | ? |
|---|
| 42 | ? |
|---|
| 43 | ? |
|---|
| 44 | ? |
|---|
| 45 | ? |
|---|
| 46 | ? |
|---|
| 47 | ? |
|---|
| 48 | ? |
|---|
| 49 | ? |
|---|
| 50 | ? |
|---|
| 51 | ? |
|---|
| 52 | . |
|---|
| 53 | [ (* rel_normal *) |
|---|
| 54 | #ge #ge' #RG #Xs1 #Xs2 * // |
|---|
| 55 | | (* rel_labelled *) |
|---|
| 56 | @clight_cminor_rel_labelled |
|---|
| 57 | | (* rel_classify_call *) |
|---|
| 58 | #ge #ge' #RG #Xs1 #Xs2 * // |
|---|
| 59 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #E |
|---|
| 60 | | #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #E |
|---|
| 61 | | #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #E |
|---|
| 62 | ] whd in E:(??%?); destruct |
|---|
| 63 | | (* rel_classify_return *) |
|---|
| 64 | #ge #ge' #RG #Xs1 #Xs2 * // |
|---|
| 65 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #E |
|---|
| 66 | | #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #E |
|---|
| 67 | | #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #E |
|---|
| 68 | ] whd in E:(??%?); destruct |
|---|
| 69 | | (* rel_callee *) |
|---|
| 70 | #ge #ge' #RG #Xs1 #Xs2 * |
|---|
| 71 | [ #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 * |
|---|
| 72 | | #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 #H255 #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 #H266 * |
|---|
| 73 | | #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 |
|---|
| 74 | | #H314 #H315 #H316 #H317 #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 #H331 #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 #H342 #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 #H356 #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 #H370 #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 * |
|---|
| 75 | ] (* FIXME *) cases daemon |
|---|
| 76 | | (* labelled_normal_1 *) |
|---|
| 77 | #ge * // |
|---|
| 78 | | (* labelled_normal_2 *) |
|---|
| 79 | #ge * // |
|---|
| 80 | | (* notailcalls *) |
|---|
| 81 | #ge * |
|---|
| 82 | [ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ] |
|---|
| 83 | normalize % #E destruct |
|---|
| 84 | | (* sim_normal *) |
|---|
| 85 | #ge #ge' #INV #s1 #s1' #S1 #N1 #NCS1 #s2 #tr #ST |
|---|
| 86 | cases (clight_cminor_normal … S1 N1 NCS1 … ST) |
|---|
| 87 | #m #AF %{m} @(after_n_covariant … AF) |
|---|
| 88 | #tr' #s' * * #TR #R #M % /2/ |
|---|
| 89 | | (* sim_call_nolabel *) |
|---|
| 90 | cases daemon (* |
|---|
| 91 | #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2 |
|---|
| 92 | cases (cast_correction … RG … S1 ST) |
|---|
| 93 | #s2' * #ST' #S2 %{0} whd |
|---|
| 94 | whd in match (is_final … s1'); >(step_not_final … ST') |
|---|
| 95 | whd whd in match (step … Clight_pcs ge' s1'); >ST' |
|---|
| 96 | whd % [ % | assumption ]*) |
|---|
| 97 | | (* sim_call_label *) |
|---|
| 98 | cases daemon (* |
|---|
| 99 | #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #ST1 #CS2 #ST2 |
|---|
| 100 | cases (cast_correction … RG … S1 ST1) |
|---|
| 101 | #s2' * #ST1' #S2 |
|---|
| 102 | cases (cast_correction … RG … S2 ST2) |
|---|
| 103 | #s3' * #ST2' #S3 |
|---|
| 104 | %{1} whd |
|---|
| 105 | whd in match (is_final … s1'); >(step_not_final … ST1') |
|---|
| 106 | whd whd in match (step … Clight_pcs ge' s1'); >ST1' |
|---|
| 107 | whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ] |
|---|
| 108 | whd whd in match (is_final … s2'); >(step_not_final … ST2') |
|---|
| 109 | whd whd in match (step … Clight_pcs ge' s2'); >ST2' |
|---|
| 110 | whd % [ % | assumption ]*) |
|---|
| 111 | | (* sim_return *) |
|---|
| 112 | cases daemon (* |
|---|
| 113 | #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST |
|---|
| 114 | cases (cast_correction … RG … S1 ST) |
|---|
| 115 | #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ] |
|---|
| 116 | whd |
|---|
| 117 | whd in match (is_final … s1'); >(step_not_final … ST') |
|---|
| 118 | whd whd in match (step … Clight_pcs ge' s1'); >ST' |
|---|
| 119 | whd % [ >(return_E0 … ST) // assumption | assumption ]*) |
|---|
| 120 | | (* sim_cost *) |
|---|
| 121 | cases daemon (* |
|---|
| 122 | #ge #ge' #RG #s1 #s1' #s2 #tr #S1 #CS1 #ST |
|---|
| 123 | cases (cast_correction … RG … S1 ST) |
|---|
| 124 | #s2' * #ST' #S2 whd |
|---|
| 125 | whd in match (is_final … s1'); >(step_not_final … ST') |
|---|
| 126 | whd whd in match (step … Clight_pcs ge' s1'); >ST' |
|---|
| 127 | whd % [ % | assumption ]*) |
|---|
| 128 | | (* sim_init *) |
|---|
| 129 | #p1 #p2 #s #COMPILE #INIT |
|---|
| 130 | cases (init_clight_cminor … INIT COMPILE) |
|---|
| 131 | #INV * #s' * #INIT' #S |
|---|
| 132 | %{s'} % [ @INIT' | %{INV} assumption ] |
|---|
| 133 | ] qed. |
|---|
