include "compiler.ma".

include "ASM/Interpret2.ma".

include "Clight/Clight_classified_system.ma".

(* From measurable on Clight, we will end up with an RTLabs flat trace where
   we know that there are some m' and n' such that the prefix in Clight matches
   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
   for those n' steps so that we can build a corresponding structured trace.
   
   "Equivalent" here means, in particular, that the observables will be the same,
   and those observables will include the stack space costs.
 *)

definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.

let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
[ nil ⇒ λ_. a
| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
]. 
[ %1 %
| #b #H' @H %2 @H'
] qed.

definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝ 
λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).

lemma Exists_lift : ∀A,P,Q,l.
  (∀x. P x → Q x) →
  Exists A P l →
  Exists A Q l.
#A #P #Q #l elim l
[ //
| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
] qed.

include "RTLabs/MeasurableToStructured.ma".
include "common/ExtraMonads.ma".

definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
λcostmap,itrace.
  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
  Σ_{l ∈ ctrace}(costmap l).

definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝
λC,p,n,costmap.
  ! 〈s,itrace〉 ← exec_steps_with_obs C p n;
  return exec_cost_of_trace costmap itrace.

lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2.
  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
  ∃s1,s2.
    exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧
    exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉.
#pcs #p #m1 #m2 #obs1 #obs2 #OBS
@('bind_inversion OBS) -OBS #s0 #INIT #OBS
@('bind_inversion OBS) -OBS * #tr1 #s1 #EXEC1 #OBS
@('bind_inversion OBS) -OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS
whd in OBS:(??%%); destruct
%{s1} %{s2}
whd in ⊢ (?(??%?)(??%?)); >INIT
whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2)
whd in ⊢ (?(??%?)(??%?));
% [ % | >int_trace_append' @breakup_pair @breakup_pair % ]
qed.

lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ.
  (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)).
#A #l1 elim l1
[ #l2 #f %
| #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH //
] qed.

lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs.
  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
  clock_after pcs p m1 costs = return c1 →
  clock_after pcs p (m1+m2) costs = return c2 →
  c2 - c1 = exec_cost_of_trace costs obs2.
#pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS
cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
>filter_map_append >bigsum_append /2/
qed.

include "common/AssocList.ma".

definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
 λstack_cost,id.
  assoc_list_lookup ?? id (eq_identifier …) stack_cost.

definition simulates ≝ 
  λp: compiler_output.
  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
  ∀m1,m2.
   measurable Clight_pcs (c_labelled_clight … p) m1 m2
    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
  ∀c1,c2.
   clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
   clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 →
  ∃n1,n2.
   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
   observables (OC_preclassified_system (c_labelled_object_code … p))
    (c_labelled_object_code … p) n1 n2
  ∧
   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).

include "Clight/SwitchAndLabel.ma".

include "common/FEMeasurable.ma".
include "Clight/SimplifyCastsMeasurable.ma".
include "Clight/toCminorMeasurable.ma".
include "Cminor/toRTLabsCorrectness.ma".

lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
  measurable pcs p m1 m2 stack_cost max →
  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
#pcs #p #m1 #m2 #stack_cost #max
* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
% [2: % [2:
  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
  whd in ⊢ (??%?); @breakup_pair %
| skip ]| skip ]
qed.

theorem correct :
  ∀observe.
  ∀input_program,output.
  compile observe input_program = return output →
  not_wrong … (exec_inf … clight_fullexec input_program) →
  sim_with_labels
   (exec_inf … clight_fullexec input_program)
   (exec_inf … clight_fullexec (c_labelled_clight … output))
  ∧
  simulates output.
#observe #p_in #out
#H @('bind_inversion H) -H
** #init_cost #labelled #p_rtlabs #EQ_front_end
#H @('bind_inversion H) -H
** #p_asm #stack_costs #globals_size
#H @('bind_inversion H) -H
#p_asm'
#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
#H @('bind_inversion H) -H
#p_loc #EQ_assembler
whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)

whd in EQ_front_end:(??%?);
letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
lapply (refl ? (clight_label cl_switch_removed))
cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
whd in ⊢ (??%? → ?);
letin cl_simplified ≝ (simplify_program ?)
#H @('bind_inversion H) -H #cminor #CMINOR
#H @('bind_inversion H) -H #WCL #_
#H @('bind_inversion H) -H #INJ #_
letin rtlabs ≝ (cminor_to_rtlabs cminor)
#EQ_front_end

#NOT_WRONG %
[ whd in EQ_front_end:(??%%); destruct
  cut (labelled = \fst (clight_label cl_switch_removed))
  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
  #E >E
  @switch_and_labelling_sim @NOT_WRONG
| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
  #El >El
  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
  >OBS -ra_meas
  
  (* So, we have for RTLabs:
     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
     ra_obs'        - the observables from [ra_tlr] are [subtrace]
     ra_max         - the stack bound is respected in [prefix@subtrace]
   *)


(* Old, semiformal cut
cut (∀n,s1,s2,obs1,obs2.
          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
            tlr_observables … tlr (function_of … s1) = obs2 →
            (* maybe instead of function_of the called id can rather be obtained from execution? *)
     ∃m,p,s_fin.
   observables (OC_preclassified_system (c_labelled_object_code … p))
    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
    *)