include "Cminor/Cminor_abstract.ma".
include "RTLabs/RTLabs_abstract.ma".
include "Cminor/toRTLabs.ma".

record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ {
}.
axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop.

axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'.
  cminor_rtlabs_rel gc gr INV s s' →
  Cminor_labelled s = RTLabs_cost s'.

(* Conjectured simulation results

   We split these based on the start state:
   
   1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs
      ([n] can be zero if the Cminor program executed an St_skip);
   2. call and return state steps are simulated by a call/return state step (we
      don't add anything extra in this stage, it happens in Clight to Cminor);
      and
   3. lone cost label steps are simulates by a lone cost label step

   Most of the work in this stage is splitting the execution of complex Cminor
   statements into individual RTLabs steps.  This doesn't contradict 2 above -
   the expansion of function parameters, return expressions, etc is done for
   the function call / return *statement*, whereas the call / return *state* is
   a Callstate / Returnstate that is the second half of the operation.

   Note that we'll need something more to show that non-termination is
   preserved (because it isn't obvious that we don't squash a loop to zero
   instructions).  Options are a traditional measure, or using the soundness of
   the cost labelling.

   These should allow us to maintain enough structure to identify the RTLabs
   subtrace corresponding to a measurable Clight/Cminor subtrace.
 *)

definition cminor_normal : Cminor_state → bool ≝
λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

definition rtlabs_normal : RTLabs_state → bool ≝
λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

axiom cminor_measure : Cminor_state → nat.

axiom cminor_rtlabs_normal :
  ∀ge_cm,ge_ra.
  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
  ∀s1,s1',s2,tr.
  cminor_rtlabs_rel … INV s1 s1' →
  cminor_normal s1 →
  ¬ Cminor_labelled s1 →
  step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
  ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
    tr = tr' ∧
    (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧
    cminor_rtlabs_rel … INV s2 s2'
  ).

axiom cminor_rtlabs_call_return :
  ∀ge_cm,ge_ra.
  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
  ∀s1,s1',s2,tr.
  cminor_rtlabs_rel … INV s1 s1' →
  match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
    tr = tr' ∧
    cminor_rtlabs_rel … INV s2 s2'
  ).

axiom cminor_rtlabs_cost :
  ∀ge_cm,ge_ra.
  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
  ∀s1,s1',s2,tr.
  cminor_rtlabs_rel … INV s1 s1' →
  Cminor_labelled s1 →
  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'.
    tr = tr' ∧
    cminor_rtlabs_rel … INV s2 s2'
  ).

axiom cminor_rtlabs_init :
  ∀p,s.
  make_initial_state … Cminor_fullexec p = OK … s →
  let p' ≝ cminor_to_rtlabs p in
  ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p').
  ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧
  cminor_rtlabs_rel … INV s s'.

include "common/FEMeasurable.ma".
include "Cminor/Cminor_classified_system.ma".
include "RTLabs/RTLabs_classified_system.ma".

include "common/ExtraMonads.ma".

lemma Cminor_return_E0 : ∀ge,s,tr,s'.
  step … Cminor_exec ge s = Value … 〈tr,s'〉 →
  Cminor_classify s = cl_return →
  tr = E0.
#ge *
[ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
| #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
| #v #m *
  [ #tr #s' #STEP #_
    cases v in STEP; [ #E whd in E:(??%?); destruct ]
    * [1,3,4: normalize #A try #B destruct ]
    * #v #STEP whd in STEP:(??%?); destruct %
  | cases v
    [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct //
        | normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct
        ]
    | #v' *
      [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct
      | #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct //
      ]
    ]
  ]
| #r #tr #s' #ST #CL normalize in CL; destruct
] qed.

definition cminor_rtlabs_meas_sim : meas_sim ≝
mk_meas_sim
  Cminor_pcs
  RTLabs_pcs
  (λcmp,rap. cminor_to_rtlabs cmp = rap)
  cminor_rtlabs_inv
  cminor_rtlabs_rel
  ? (* rel_normal *)
  ? (* rel_labelled *)
  ? (* rel_classify_call *)
  ? (* rel_classify_return *)
  ? (* rel_callee *)
  ? (* labelled_normal_1 *)
  ? (* labelled_normal_2 *)
  ? (* notailcalls *)
  (λ_.cminor_measure)
  ? (* sim_normal *)
  ? (* sim_call_nolabel *)
  ? (* sim_call_label *)
  ? (* sim_return *)
  ? (* sim_cost *)
  ? (* sim_init *)
.
[ (* rel_normal *)
| (* rel_labelled *)
  @cminor_rtlabs_rel_labelled
| (* rel_classify_call *)
| (* rel_classify_return *)
| (* rel_callee *)
| (* labelled_normal_1 *)
  #g * //
| (* labelled_normal_2 *)
  #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???);
  cases (next_instruction f) //
| (* notailcalls *)
  #g @Cminor_notailcalls
| (* sim_normal *)
  #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP
  cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP)
  #m #AFTER %{m} @(after_n_covariant … AFTER)
  #tr' #s * * #H1 #H2 #H3 /3/
| (* sim_call_nolabel *)
  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0}
  @(cminor_rtlabs_call_return … R1 … STEP)
  change with (Cminor_classify ?) in CL1:(??%?); >CL1 %
| (* sim_call_label *)
  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1}
  lapply (cminor_rtlabs_call_return … R1 … STEP1)
  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
  #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct
  % [ %
  [  %
  |  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2
  ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2)
     #AFTER2 cases (after_1_step … AFTER2)
     #trx * #sx * * #NFx #STEPx * #E #Rx destruct
     whd >NFx whd >STEPx whd /3/
  ]
| (* sim_return *)
  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0}
  lapply (cminor_rtlabs_call_return … R1 … STEP)
  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
  >(Cminor_return_E0 … STEP CL1)
  #AFTER %{(refl ??)} @AFTER
| (* sim_cost *)
  #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP
  @(cminor_rtlabs_cost … R1 … STEP)
  @CS1
| (* sim_init *)
  #p #p' #s #COMPILE destruct #INIT
  cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R
  %{s'} % [ @INIT' | %{INV} @R ]
] cases daemon qed.