source: src/correctness.ma @ 2396

include "compiler.ma".

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

include "Clight/labelSimulation.ma".

theorem correct :
  ∀input_program.
  
  ∀object_code,costlabel_map,labelled,cost_map.
  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →

  not_wrong … (exec_inf … clight_fullexec input_program) →
  
  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
  ∧
  True (* TODO *).

#input_program
#object_code #costlabel_map #labelled #cost_map
#COMPILE
#NOT_WRONG
cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #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
whd in FRONTEND:(??%%); destruct

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


include "Clight/abstract.ma".

definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.

definition execution_prefix : Type[0] ≝ list (trace × Clight_state).
axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)).
axiom stack_after : execution_prefix → nat.

(* TODO: cost labels *)

let rec will_return_aux (stack_cost:Clight_stack_T) (depth:nat) (current_stack:nat)
                        (max_stack:nat) (trace:execution_prefix) on trace : option nat ≝
match trace with
[ nil ⇒ match depth with [ O ⇒ Some ? max_stack | _ ⇒ None ? ]
| cons h tl ⇒
  let 〈tr,s〉 ≝ h in
  match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
  [ cl_call ⇒ λsc.
      let new_stack ≝ current_stack + sc I in
      will_return_aux stack_cost (S depth) new_stack (max max_stack new_stack) tl
  | cl_return ⇒ λsc.
      match depth with
      [ O ⇒ None ?
      | S d ⇒ will_return_aux stack_cost d (current_stack - sc I) max_stack tl
      ]
  | _ ⇒ λ_. will_return_aux stack_cost depth current_stack max_stack tl
  ] (stack_cost s)
].
definition will_return' : Clight_stack_T → nat → execution_prefix → option nat ≝
λstack_cost,current_stack,trace. will_return_aux stack_cost O current_stack current_stack trace.

definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder,max_stack.
  let cl_trace ≝ exec_inf … clight_fullexec p in
  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
  will_return' stack_cost (stack_after prefix) interesting = Some ? max_stack ∧
  max_stack < max_allowed_stack.

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

axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
axiom clight_clock_after : clight_program → nat → option nat.
axiom initial_8051_status : ∀oc. Status oc.

definition simulates ≝ 
  λstack_cost, stack_bound, labelled, object_code.
  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
  ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
  ∀c1,c2. clight_clock_after labelled m1 = Some ? c1 → clight_clock_after labelled m2 = Some ? c2 →
  ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).

axiom compile' : clight_program → res (object_code × costlabel_map × clight_program
 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).

theorem correct' :
  ∀input_program.

  not_wrong … (exec_inf … clight_fullexec input_program) →
  
  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
  compile' input_program = OK ? 〈〈〈〈object_code,costlabel_map〉,labelled〉,cost_map〉,stack_cost,stack_bound〉 →
  
  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
  ∧

  simulates stack_cost stack_bound labelled object_code.
  

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

*)