source: src/Clight/toCminorMeasurable.ma @ 3063

Last change on this file since 3063 was 3063, checked in by campbell, 6 years ago

Remove measure function from FEMeasurable because we're not using it and
it would need to be generalised for clight to cminor. Sketch out rest
of clight to cminor meas_sim record.

File size: 6.7 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 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 #H186 #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 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 #H303 #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312
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.