source: src/correctness.ma @ 2475

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

%
[ (* Needs switch removal too, now
     @labelling_sim @NOT_WRONG
   *) cases daemon
| @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).
let rec split_trace (x:execution Clight_state io_out io_in) (n:nat) on n : option (execution_prefix × (execution Clight_state io_out io_in)) ≝
match n with
[ O ⇒ Some ? 〈[ ], x〉
| S n' ⇒
  match x with
  [ e_step tr s x' ⇒
    ! 〈pre,x''〉 ← split_trace x' n';
    Some ? 〈〈tr,s〉::pre,x''〉
  | _ ⇒ None ?
  ]
].

definition trace_labelled : execution_prefix → Prop ≝
λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2).

definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝
λstack_cost. 
  foldl … (λx, trs.
    let 〈current,max_stack〉 ≝ x in
    let 〈tr,s〉 ≝ trs in 
    let new ≝
      match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
      [ cl_call ⇒ λsc. current + sc I
      | cl_return ⇒ λsc. current - sc I
      | _ ⇒ λ_. current
      ] (stack_cost s) in
    〈new, max max_stack new〉) 〈0,0〉.

definition stack_after : Clight_stack_T → execution_prefix → nat ≝
λsc,x. \fst (measure_stack sc x).

definition max_stack :  Clight_stack_T → execution_prefix → nat ≝
λsc,x. \snd (measure_stack sc x).

let rec will_return_aux (depth:nat)
                        (trace:execution_prefix) on trace : bool ≝
match trace with
[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
| cons h tl ⇒
  let 〈tr,s〉 ≝ h in
  match Clight_classify s with
  [ cl_call ⇒ will_return_aux (S depth) tl
  | cl_return ⇒
      match depth with
      [ O ⇒ false
      | S d ⇒ will_return_aux d tl
      ]
  | _ ⇒ will_return_aux depth tl
  ]
].
definition will_return' : execution_prefix → bool ≝ will_return_aux O.

definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
  let cl_trace ≝ exec_inf … clight_fullexec p in
  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
  trace_labelled interesting ∧
  bool_to_Prop (will_return' interesting) ∧
  max_stack stack_cost (prefix@interesting) < 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.
 *)

definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝
λp,m,n.
  let cl_trace ≝ exec_inf … clight_fullexec p in
  match split_trace cl_trace m with
  [ Some x ⇒
    let 〈prefix,suffix〉 ≝ x in
    match split_trace suffix n with
    [ Some y ⇒
      let interesting ≝ \fst y in
      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).

definition in_execution_prefix : execution_prefix → 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.

definition measure_clock : ∀x:execution_prefix. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
λx,costmap. foldl_exists … x
 (λclock,trs,H.
    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
 0.
whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
qed.

definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
λp,n,costmap.
  let x ≝ exec_inf … clight_fullexec p in
  match split_trace x n with
  [ Some traces ⇒
    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
  | None ⇒ None ?
  ].
cases daemon
qed.

axiom initial_8051_status : ∀oc. Status oc.

definition simulates ≝ 
  λstack_cost, stack_bound, labelled, object_code, cost_map.
  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 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = 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 ×
  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled 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 cost_map.
  

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

*)