include "compiler.ma".

include "common/SmallstepExec.ma".
include "Clight/Cexec.ma".
include "ASM/Interpret2.ma".

include "Clight/labelSimulation.ma".

theorem correct :
  ∀input_program.

  not_wrong (exec_inf … clight_fullexec input_program) →
  
  ∀object_code,costlabel_map,labelled,cost_map.
  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
  
  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
  ∧
  True (* TODO *).

#input_program
#NOT_WRONG
#object_code #costlabel_map #labelled #cost_map
#COMPILE
cases (bind_inversion ????? COMPILE) -COMPILE * #labelled' #rtlabs_program * #FRONTEND #COMPILE
cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
whd in COMPILE:(??%%); destruct
cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
cases (bind_inversion ????? FRONTEND) -FRONTEND #rtlabs_program' * #RTLABS #FRONTEND
whd in FRONTEND:(??%%); destruct

%
[ @labelling_sim @NOT_WRONG
| @I
] qed.

(* TODO 

∀input_program.
! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program

exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled

∧

exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
(* Should we be lifting labels in some way here? *)

∧


∀i,f : clight_status.  [i,f labelled, at same level]
i clight~> f →
∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
  clock f - clock i = clock f' - clock i'.


∀s,flat.
let ge ≝ (globalenvs … labelled) in
subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
RTLabs_cost s = true →
∀WR : will_return ge 0 s flat.
let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
let labels_rtlabs ≝ flat_label_trace … flat WR in
∃!initial,final,structured_trace_asm. 
  structured_trace_rtlabs ≈ structured_trace_asm ∧  
  clock … code_memory … final = clock … code_memory … initial +
     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).



What is ≃l?  Must show that "labelled" does everything that 
"input_program" does, without getting lost in some
non-terminating loop part way.

*)