source: src/Clight/SimplifyCastsMeasurable.ma @ 3195

include "Clight/SimplifyCasts.ma".
include "common/FEMeasurable.ma".
include "Clight/Clight_classified_system.ma".

lemma state_cast_labelled : ∀s,s'.
  state_cast s s' →
  Clight_labelled s = Clight_labelled s'.
#Xs #Xs' * // #f * //
qed.

lemma return_E0 : ∀ge,s,tr,s'.
  Clight_classify s = cl_return →
  exec_step ge s = Value … 〈tr,s'〉 →
  tr = E0.
#ge *
[ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ]
#tr #s' #CL whd in CL:(??%?); destruct
whd in ⊢ (??%? → ?);
cases k [ | #s' #k' | #e' #s' #k' | #e' #s' #k' | #e' #s' #s'' #k' | #e' #s' #s'' #k' | #k' | #r' #f' #e' #k' ]
#ST whd in ST:(??%?); destruct
[ cases res in ST; [ | * #i | | #p ] #ST whd in ST:(??%?); destruct %
| cases r' in ST;
  [ #ST whd in ST:(??%?); destruct %
  | * * #b #o #t #ST
    cases (bindIO_inversion ??????? ST)
    #m' * #ST' #E whd in E:(??%%); destruct %
  ]
] qed.

(* Put cast simplification simulation into form that FEMeasurable needs.
   Note that sim_call_label is just sticking together two normal steps - we
   never add extra steps here, so we don't need to worry about moving cost
   labels to the start of the function. *)

definition simplify_measurable_sim : meas_sim ≝
mk_meas_sim
  Clight_pcs
  Clight_pcs
  (λp,p'. simplify_program p = p')
  (λge,ge'. related_globals … simplify_fundef ge ge')
  (λ_,_,_.λs,s'. state_cast s s')
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
  ?
.
[ (* rel_normal *)
  #ge #ge' #RG #Xs1 #Xs2 * //
| (* rel_labelled *)
  #ge #ge' #RG @state_cast_labelled
| (* rel_classify_call *)
  #ge #ge' #RG #Xs1 #Xs2 * //
  [ #f #s #k #k' #e #m #K | #res #k #k' #m #K | #r ]
  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
| (* rel_classify_return *)
  #ge #ge' #RG #Xs1 #Xs2 * //
  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #r ]
  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
| (* rel_callee *)
  #ge #ge' #RG #Xs1 #Xs2 *
  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #res #k #k' #m #K | #r ] *
  * %
| (* 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' #RG #s1 #s1' #S1 #N1 #CS1 #s2 #tr #ST
  cases (cast_correction … RG … S1 ST)
  #s2' * #ST' #S2 %{1} whd
  whd in match (is_final … s1'); >(cl_step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ % | assumption ]
| (* sim_call_nolabel *)
  #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'); >(cl_step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ % | assumption ]
| (* sim_call_label *)
  #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'); >(cl_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'); >(cl_step_not_final … ST2')
  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
  whd % [ % | assumption ]
| (* sim_return *)
  #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'); >(cl_step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ >(return_E0 … ST) // assumption | assumption ]
| (* sim_cost *)
  #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'); >(cl_step_not_final … ST')
  whd whd in match (step … Clight_pcs ge' s1'); >ST'
  whd % [ % | assumption ]
| (* sim_init *)
  #p1 #p2 #s #COMPILE #INIT
  cases (initial_state_casts … INIT)
  #s' * * >COMPILE #INIT' #RG #S
  %{s'} % [ @INIT' | %{RG} assumption ]
] qed.