include "Clight/toCminorCorrectness.ma".
include "common/FEMeasurable.ma".
include "Clight/Clight_classified_system.ma".
include "Cminor/Cminor_classified_system.ma".

include "common/ExtraMonads.ma".

axiom clight_cminor_rel_labelled : ∀ge,ge',INV,s,s'.
  clight_cminor_rel ge ge' INV s s' →
  Clight_labelled s = Cminor_labelled s'.
  (* Large inversion required; perhaps better Russell-style
#Xge #Xge' #XINV #Xs #Xs' * //
#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 #_ #_ #_ #_ #_ #_ #_ #_
-TrFn cases cl_s in tI ts ⊢ %;
[ | #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 ]
#tI
whd in ⊢ (??%? → ?); #E destruct //
[ @('bind_inversion E) -E #e2' #_ #E
  @('bind_inversion E) -E * [ #id #L | #e' ] #_ #E
  whd in E:(??%?); [@('bind_inversion E) -E #e2'' #_ #E whd in E:(??%%); destruct //
  | cases (type_eq_dec ??) in E; #H #E whd in E:(??%%); destruct //
  ]
| @('bind_inversion E) -E #x1 #_ #E
  @('bind_inversion E) -E #x2 #_ #E
  @('bind_inversion E) -E #x3 #_ #E
  cases oe in E; [ | #e1 #E @('bind_inversion E) -E * [ #xx ] #x4 #_ ]
  #E whd in E:(??%%); destruct //
  cases (alloc_tmp ???) in E; #x5 #x6
*)

definition clight_to_cminor_measurable_sim : meas_sim ≝
mk_meas_sim
  Clight_pcs
  Cminor_pcs
  (λp,p'. clight_to_cminor p = OK … p')
  clight_cminor_inv
  clight_cminor_rel
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
.
[ (* rel_normal *)
  #ge #ge' #RG #Xs1 #Xs2 * //
| (* rel_labelled *)
  @clight_cminor_rel_labelled
| (* rel_classify_call *)
  #ge #ge' #RG #Xs1 #Xs2 * //
  [ #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
  | #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
  | #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
  ] whd in E:(??%?); destruct
| (* rel_classify_return *)
  #ge #ge' #RG #Xs1 #Xs2 * //
  [ #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
  | #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
  | #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
  ] whd in E:(??%?); destruct
| (* rel_callee *)
  #ge #ge' #RG #Xs1 #Xs2 *
  [ #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 *
  | #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 *
  | #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 
  | #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 *
  ] (* FIXME *) cases daemon
| (* labelled_normal_1 *)
  #ge * //
| (* labelled_normal_2 *)
  #ge * //
| (* notailcalls *)
  #ge *
  [ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ]
  normalize % #E destruct
| (* sim_normal *)
  #ge #ge' #INV #s1 #s1' #S1 #N1 #NCS1 #s2 #tr #ST
  cases (clight_cminor_normal … S1 N1 NCS1 … ST)
  #m #AF %{m} @(after_n_covariant … AF)
  #tr' #s' * * #TR #R #M % /2/
| (* sim_call_nolabel *)
  cases daemon (*
  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2
  cases (cast_correction … RG … S1 ST)
  #s2' * #ST' #S2 %{0} whd
  whd in match (is_final … s1'); >(step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ % | assumption ]*)
| (* sim_call_label *)
  cases daemon (*
  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #ST1 #CS2 #ST2
  cases (cast_correction … RG … S1 ST1)
  #s2' * #ST1' #S2
  cases (cast_correction … RG … S2 ST2)
  #s3' * #ST2' #S3
  %{1} whd
  whd in match (is_final … s1'); >(step_not_final … ST1')
  whd whd in match (step … Clight_pcs ge' s1'); >ST1'
  whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ] 
  whd whd in match (is_final … s2'); >(step_not_final … ST2')
  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
  whd % [ % | assumption ]*)
| (* sim_return *)
  cases daemon (*
  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST
  cases (cast_correction … RG … S1 ST)
  #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ]
  whd
  whd in match (is_final … s1'); >(step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ >(return_E0 … ST) // assumption | assumption ]*)
| (* sim_cost *)
  cases daemon (*
  #ge #ge' #RG #s1 #s1' #s2 #tr #S1 #CS1 #ST
  cases (cast_correction … RG … S1 ST)
  #s2' * #ST' #S2 whd
  whd in match (is_final … s1'); >(step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ % | assumption ]*)
| (* sim_init *)
  #p1 #p2 #s #COMPILE #INIT
  cases (init_clight_cminor … INIT COMPILE)
  #INV * #s' * #INIT' #S
  %{s'} % [ @INIT' | %{INV} assumption ]
] qed.