include "compiler.ma".

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

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

*)