source: src/correctness.ma @ 3353

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 ≝ costlabels_of_observables itrace in
  Σ_{l ∈ ctrace}(costmap l).

definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
λC,p,m.
  let g ≝ make_global … (pcs_exec … C) p in
  let C' ≝ pcs_to_cs C g in
  ! s0 ← make_initial_state … p;
  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.

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.

include "ASM/CostsProof.ma".

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
>costlabels_of_observables_append >fold_sum' >commutative_plus @sym_eq @minus_plus_m_m
qed.

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
    (stack_sizes (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
  ∧
   clock ?? (execute (n1 + n2) ? initial_status) =
    plus (clock ?? (execute n1 ? initial_status)) (minus c2 c1).

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/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".
include "ASM/OC_traces_to_exec.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.

record back_end_preconditions (p_rtlabs : RTLabs_program)
(stacksizes : ident → option ℕ) (max_stack : ℕ)
(prefix, subtrace : list intensional_event) (fn : ident)
: Prop ≝ 
{ ra_init : RTLabs_status (make_global p_rtlabs)
; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init
; ra_max :
  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
    (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack
; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs))
    prefix subtrace fn ra_init
}.

lemma front_end_correct :
∀observe, input_program, init_cost, labelled, p_rtlabs.
front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 →
not_wrong … (exec_inf … clight_fullexec input_program) →
sim_with_labels
 (exec_inf … clight_fullexec input_program)
 (exec_inf … clight_fullexec labelled)
∧
  ∀m1,m2,stacksizes,max_stack.
   measurable Clight_pcs labelled m1 m2 stacksizes max_stack →
  ∃prefix, subtrace, fn.
  observables Clight_pcs labelled m1 m2 = return 〈prefix, subtrace〉 ∧
  back_end_preconditions p_rtlabs stacksizes max_stack
    prefix subtrace fn.
#observe #p_in #init_cost' #labelled #p_rtlabs #EQ_front_end
whd in EQ_front_end:(??%?);
letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
inversion (clight_label cl_switch_removed)
#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)
whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)

#NOT_WRONG %
[ cut (cl_labelled = \fst (clight_label cl_switch_removed))
  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
  #E >E
  @switch_and_labelling_sim @NOT_WRONG
]

#m1 #m2 #stacksizes #max_stack #m1_m2_meas
cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
#simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %;
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_s0 * #ra_s1 * #ra_s2 * #fn * #ra_init * #ra_ft * * #ra_ft_fn #ra_ft_obs * #ra_tlr * * #ra_unrepeating #ra_max #ra_obs'
>OBS -ra_meas
%{prefix} %{subtrace} %{fn} %[%]
%{ra_init ra_max}
%{ra_unrepeating ra_ft_obs ra_ft_fn ra_obs'}
qed.

lemma back_end_correct :
∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn.
back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 →
back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn →
init_cost = init_cost' ∧
∀sigma,pol.
ft_and_tlr (ASM_status p_asm sigma pol)
prefix subtrace fn
(initialise_status ? p_asm).
#observe #init_cost #p_rtlabs #p_asm' #init_cost #stack_model #max_stack
#prefix #subtrace #fn
#H @('bind_inversion H) -H
#p_asm
#H lapply (opt_eq_from_res ???? H) -H
#EQ_lin_to_asm
#H lapply (sym_eq ??? H) -H
whd in ⊢ (??%%→?); #EQ destruct(EQ)
letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs)
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_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
letin stack_sizes ≝ (stack_sizes stack_model)
*
#ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%]
#sigma #pol

cases (RTLabsToRTL_ok stack_model init_cost … ra_init_ok)
[2: @(transitive_stack_cost_model_le … (RTLabsToRTL_monotone_stacksizes init_cost …))
   @(transitive_stack_cost_model_le … (RTLToERTL_monotone_stacksizes …))
   @ERTLToLTL_monotone_stacksizes ]
#rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr)
change with (state_pc RTL_semantics_separate) in rtl_init;
change with
  (state_pc RTL_semantics_separate → state_pc RTL_semantics_separate → ?)
#rtl_st2 #rtl_st3 #rtl_ft #rtl_tlr #rtl_unrepeating #rtl_ft_ok
#current_is_fn #rtl_tlr_ok

lapply (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes
  p_rtl fn … rtl_ft rtl_tlr ??? rtl_unrepeating) try assumption
[ whd whd in match extract_call_ud_from_ft; whd in match extract_call_ud_from_tlr;
  normalize nodelta >rtl_ft_ok >rtl_tlr_ok
  <extract_call_ud_from_observables_append assumption
]
>rtl_ft_ok >rtl_tlr_ok #rtl_ft_tlr

cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
#rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl
lapply (status_simulation_produce_ft_and_tlr … simul_rtl rtl_ft_tlr)
-rtl_ft_tlr #rtl_ft_tlr -R_rtl -rtl_st2 -rtl_st3 -R_ra_rtl -ra_init -ra_max

cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok')
#ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr)
-rtl_init -rtl_init' -R_rtl_ertl #ertl_ft_tlr

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
lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr)
-ertl_init -R_ertl_ltl #ltl_ft_tlr

cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
#lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr)
-ltl_init -R_ltl_lin #lin_ft_tlr

cases (LINToASM_ok stack_sizes p_lin p_asm sigma pol EQ_lin_to_asm lin_init lin_init_ok)
#R_lin_asm #simul_lin_asm
@(status_simulation_produce_ft_and_tlr … simul_lin_asm lin_ft_tlr)
qed.

lemma assembler_correct :
∀observe,input_program,output_program,prefix,subtrace,fn.
assembler observe input_program = return output_program →
(∀sigma,pol.ft_and_tlr (ASM_status input_program sigma pol) prefix subtrace fn
  (initialise_status ? input_program)) →
ft_and_tlr (OC_abstract_status output_program)
prefix subtrace fn (initialise_status ? (cm output_program)).
#observe #p_asm #p_oc #prefix #subtrace #fn
#H @('bind_inversion H) -H ** #sigma #pol normalize nodelta #sigma_pol_ok
#H lapply (opt_eq_from_res ???? H) -H #jump_expansion_ok
whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) -H #EQ destruct(EQ)
#H lapply (H sigma pol) -H

cases (assembly_ok p_asm … jump_expansion_ok)
#R_asm_oc #simul_asm_oc
@(status_simulation_produce_ft_and_tlr … simul_asm_oc)
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' #init_cost' #stack_costs #max_stack #EQ_back_end normalize nodelta
#H @('bind_inversion H) -H #p_oc #EQ_assembler
whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG

cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2
%{H1} #m1 #m2 #m1_m2_meas
#c1 #c2 #c1_prf #c2_prf
cases (H2 … m1_m2_meas)
#prefix * #subtrace * #fn * #OBS #back_end_pre >OBS
>(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2

cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ)
#assembler_pre
cases (assembler_correct … EQ_assembler assembler_pre)
#oc_st2 #oc_st3 #oc_ft #oc_tlr #oc_unrepeating #oc_ft_ok #fn_ok #oc_tlr_ok

%{(ft_length … oc_ft)}
%{(tlr_length … oc_tlr)}
%
[ >(OC_traces_to_observables … fn_ok) >oc_ft_ok >oc_tlr_ok %
| >execute_plus >OC_ft_to_execute >OC_tlr_to_execute
  whd in match exec_cost_of_trace; normalize nodelta <oc_tlr_ok 
  >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one}]
  @(compute_max_trace_label_return_cost_ok_with_trace … oc_unrepeating)
]
qed.