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".

definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
λp,n,costmap.
  ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
  return Σ_{l ∈ ctrace}(costmap l).

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.
   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
   clight_clock_after (c_labelled_clight … p) 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 "common/ExtraMonads.ma".

include "Clight/SwitchAndLabel.ma".

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
| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf

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〉)
    
     
             
             
  
(* start of old simulates  

(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
   according to the [stack_cost] function. *)
axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.


  let cl_trace ≝ exec_inf … clight_fullexec labelled in
  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
  not_wrong ? cl_trace →
  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'

*)

(* 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.
  Clight_labelled i →
  Clight_labelled f →
∀mx,time.
  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
  will_return O O mx time f trace →
  mx < max_allowed_stack →
∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
  time = 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.

*)