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.
 *)

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 >commutative_plus @sym_eq @minus_plus_m_m
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".

(* atm they are all axioms *)
include "RTLabs/RTLabsExecToTrace.ma".
include "RTLabs/RTLabsToRTLAxiom.ma".
include "RTL/RTL_separate_to_overflow.ma".
include "RTL/RTL_overflow_to_unique.ma".
include "RTL/RTLToERTLAxiom.ma".
include "ERTL/ERTLToLTLAxiom.ma".
include "LTL/LTLToLINAxiom.ma".
include "LIN/LINToASMAxiom.ma".
include "ASM/AssemblyAxiom.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, after the front-end 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]
   *)

  cases (produce_rtlabs_flat_trace … ra_exec_prefix)
  #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
  letin p_rtl ≝ (rtlabs_to_rtl init_cost (cminor_to_rtlabs cminor))
  letin p_ertl ≝ (rtl_to_ertl p_rtl)
  letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
  letin p_lin ≝ (ltl_to_lin p_ltl)
  letin stack_sizes ≝ (lookup_stack_cost (\snd (\fst
    (ertl_to_ltl compute_fixpoint colour_graph p_ertl))))
  cases (RTLabsToRTL_ok stack_sizes init_cost … ra_init_ok)
  [2: cases daemon ]
  #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
  cases (status_simulation_produce_ft_and_tlr … ra_ft ra_tlr simul_ra_rtl)
  change with (state_pc RTL_semantics_separate) in rtl_init;
  change with (state_pc RTL_semantics_separate → ?)
  #rtl_st2 * change with (state_pc RTL_semantics_separate → ?)
  #rtl_st3 * change with (state_pc RTL_semantics_separate → ?)
  #rtl_st4 * #rtl_ft * #rtl_tlr * #rtl_taaf ** #_ -rtl_st4
  #rtl_ft_ok #rtl_tlr_ok
  cases (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
  [2,3: cases daemon (* good stack usage, consequence of ra_max *) ]
  #rtl_ft' * #rtl_tlr' * #rtl_ft_ok' #rtl_tlr_ok'
  cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
  #rtl_ft_ok'' #rtl_tlr_ok''
  cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok'')
  #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
  cases (status_simulation_produce_ft_and_tlr … rtl_ft'' rtl_tlr'' simul_rtl_ertl)
  #ertl_st2 * #ertl_st3 * #ertl_st4 * #ertl_ft * #ertl_tlr * #ertl_taaf ** #_ -ertl_st4
  #ertl_ft_ok #ertl_tlr_ok
  lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
  @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
  #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
  cases (status_simulation_produce_ft_and_tlr … ertl_ft ertl_tlr simul_ertl_ltl)
  #ltl_st2 * #ltl_st3 * #ltl_st4 * #ltl_ft * #ltl_tlr * #ltl_taaf ** #_ -ltl_st4
  #ltl_ft_ok #ltl_tlr_ok
  cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
  #lin_ft_ok #lin_tlr_ok
  @('bind_inversion EQ_assembler) ** #sigma #pol #sigma_pol_ok -EQ_assembler
  #EQ lapply (opt_eq_from_res ???? EQ) #jump_expansion_ok -EQ
  whd in ⊢ (??%%→?); #EQ
  cut (p_loc = assembly p_asm' (λx.sigma x) (λx.pol x))
  [ -EQ_ra_pref_obs -ra_obs' -ra_exec_prefix -ltl_init_ok -jump_expansion_ok
    -rtl_init -rtl_ft'' -ltl_ft -lin_init -ltl_init -ertl_init -rtl_init'
    -El destruct(EQ) % ] #EQ_p_loc -EQ
    
  @@@@
    
  cases (LINToASM_ok stack_sizes p_lin p_asm' sigma pol EQ_lin_to_asm lin_init lin_init_ok)
  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
  #lin_ft_ok #lin_tlr_ok
  
  
  
  
  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
  #rtl_ft_ok'' #rtl_tlr_ok''
  
  
  [2: @rtl_init_ok
  RTL_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
  )
  #aux lapply (aux rtl_init rtl_st2 rtl_st3) -aux #aux
  lapply (aux rtl_ft rtl_tlr) ??)
  cases (RTLToERTL_ok stack_sizes init_cost … ra_init_ok)
  
  [5: 
  cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
    exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →