source: src/Clight/toCminorMeasurable.ma @ 3367

Last change on this file since 3367 was 3178, checked in by campbell, 7 years ago

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File size: 6.5 KB
Line 
1include "Clight/toCminorCorrectness.ma".
2include "common/FEMeasurable.ma".
3include "Clight/Clight_classified_system.ma".
4include "Cminor/Cminor_classified_system.ma".
5
6include "common/ExtraMonads.ma".
7
8axiom 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
17whd 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
31definition clight_to_cminor_measurable_sim : meas_sim ≝
32mk_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.
Note: See TracBrowser for help on using the repository browser.