source: src/common/Measurable.ma @ 2989

include "common/Executions.ma".
include "common/stacksize.ma".

(* A small-step executable semantics, together with some kind of global
   environment, notion of cost labelled state, classification function and
   stack costs. *)

record classified_system : Type[2] ≝ {
  cs_exec :> fullexec io_out io_in;
  cs_global : global … cs_exec;
  cs_labelled : state … cs_exec cs_global → bool;
  cs_classify : state … cs_exec cs_global → status_class;
  cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True | _ ⇒ False ] → ident
}.

definition cs_state : classified_system → Type[0] ≝
λC. state … C (cs_global … C).

(* Ideally we would also allow measurable traces to be from one cost label to
   another (in the same function call), but due to time constraints we'll stick
   to ending measurable traces at the end of the function only.
 *)

definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.

(* Construction of the trace of intensional events.

   It might be possible to merge these with the plain events, but for now we
   combine those with call/return information taken from the states.
   
   The build_* results help with the proof that measurable subtraces are
   preserved in the front-end. *)

definition intensional_event_of_event : event → list intensional_event ≝
λev. match ev with
[ EVcost l ⇒ [ IEVcost l ]
| EVextcall _ _ _ ⇒ [ ]  (* No equivalent, but there shouldn't be any for now *)
].

definition intensional_events_of_events : trace → list intensional_event ≝
λtr. flatten ? (map ?? intensional_event_of_event tr).

definition intensional_state_change ≝
λC,callstack,s.
    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
    | _ ⇒ λ_. 〈callstack, [ ]〉
    ] (cs_callee C s).

let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
match trace with
[ nil ⇒ 〈callstack, [ ]〉
| cons str tl ⇒
  let 〈s,tr〉 ≝ str in 
  let 〈callstack, call_event〉 ≝ intensional_state_change C callstack s in
  let other_events ≝ intensional_events_of_events tr in
  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
    〈callstack, call_event@other_events@rem〉
].

definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

lemma normal_state_inv : ∀C,s.
  normal_state C s →
  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
qed.

lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
  normal_state C s →
  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
      〈stk', (intensional_events_of_events tr)@tl〉).
#C #callstack #s #tr #trace #NORMAL
whd in ⊢ (??%?); whd in match (intensional_state_change ???);
generalize in match (cs_callee C s);
cases (normal_state_inv … NORMAL)
#CL >CL normalize nodelta #_
cases (intensional_trace_of_trace C callstack trace)
#callstack' #tl normalize nodelta
%
qed.


lemma int_events_append : ∀tr1,tr2.
  intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2).
#tr1 #tr2
change with (flatten ??) in ⊢ (??%(??%%));
<map_append >flatten_append %
qed.


lemma int_trace_irr : ∀C,callstack,s,trace.
  normal_state C s →
  intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace.
#C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL)
cases (intensional_trace_of_trace ???) //
qed.

lemma int_trace_append : ∀C,callstack,s,t1,t2,trace.
  normal_state C s →
  intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace).
#C #callstack #s #t1 #t2 #trace #NORMAL
>(int_trace_of_normal … NORMAL)
>(int_trace_of_normal … NORMAL)
>(int_trace_of_normal … NORMAL)
cases (intensional_trace_of_trace ???) #callstack' #trace'
normalize nodelta
>int_events_append
>associative_append %
qed.

lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'.
  normal_state C s →
  all … (λstr. normal_state C' (\fst str)) trace →
  intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' →
  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
#C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL'
>(int_trace_of_normal … NORMAL)
cases (intensional_trace_of_trace C callstack rem) #callstack' #trace'
#REM whd in ⊢ (??%?);
elim trace in NORMAL' ⊢ %;
[ #_ @REM
| * #s' #tr' #tl #IH #NORMAL'
  cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl
  >int_trace_of_normal
  [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%);
    >int_events_append >associative_append %
  | @NORMALs
  ]
] qed.

lemma int_trace_append' : ∀C,t1,t2,callstack.
  intensional_trace_of_trace C callstack (t1@t2) =
    (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in
     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in
     〈cs'', t1'@t2'〉).
#C #t1 #t2 elim t1
[ #callstack whd in match ([ ]@t2); whd in ⊢ (???%);
  cases (intensional_trace_of_trace ???) #cs' #trace' %
| * #s #tr #tl #IH
  #callstack
  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
  generalize in match (cs_callee C s);
  cases (cs_classify C s)
  normalize nodelta #callee
  [ cases callstack [2: #cshd #cdtl] normalize nodelta ]
  >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl'
  normalize nodelta
  cases (intensional_trace_of_trace C ? t2) #cs'' #tl''
  normalize nodelta >associative_append >associative_append
  %
] qed.

lemma int_trace_normal_cs : ∀C,callstack,trace.
  all ? (λstr. normal_state C (\fst str)) trace →
  callstack = \fst (intensional_trace_of_trace C callstack trace).
#C #callstack #trace elim trace
[ //
| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
  >(int_trace_of_normal … N1)
  >(IH Ntl) in ⊢ (??%?);
  cases (intensional_trace_of_trace ???) /2/
] qed.

lemma int_trace_append_normal : ∀C,t1,t2,callstack.
  all ? (λstr. normal_state C (\fst str)) t1 →
  intensional_trace_of_trace C callstack (t1@t2) =
    (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in
     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in
     〈cs'', t1'@t2'〉).
#C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack)
lapply (int_trace_normal_cs C callstack t1 NORMAL)
cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct //
qed.

lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'.
  cs_classify C s = cl_return →
  cs_classify C' s' = cl_return →
  all ? (λstr. normal_state C' (\fst str)) trace' →
  intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' →
  let trace ≝ 〈s',tr〉::trace' in
  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
whd
whd in ⊢ (??%%);
whd in match (intensional_state_change ???);
whd in match (intensional_state_change C' ??);
normalize nodelta
generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
>CL >CL' normalize nodelta #_ #_
cases callstack in E ⊢ %; [2: #stkhd #stktl]
normalize nodelta
cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta
>(int_trace_append_normal … NORMAL) normalize nodelta
cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
destruct @eq_f @eq_f
whd in match (gather_trace ??); >int_events_append
>associative_append @eq_f 
elim trace in NORMAL ⊢ %;
[ 1,3: #_ %
| 2,4:
  * #s1 #tr1 #tl #IH
  #N cases (andb_Prop_true … N) #N1 #Ntl
  whd in match (gather_trace ??); >int_events_append
  >associative_append >(IH Ntl)
  >(int_trace_of_normal … N1)
  cases (intensional_trace_of_trace ?? tl)
  #cs' #tl' >associative_append %
] qed.

(* I had a little trouble doing this directly. *)
lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
  (∀f. P f (f H)) →
  P (cs_callee C s) (cs_callee C s H).
#C #s #H #P #f @f
qed.

lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
  all ? (λstr. normal_state C' (\fst str)) trace' →
  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
  cs_callee C s H = cs_callee C' s' H' →
  let trace ≝ 〈s',tr〉::trace' in
  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
whd in ⊢ (? → ? → %);
whd in ⊢ (? → ? → ??%%);
whd in match (intensional_state_change ???);
whd in match (intensional_state_change C' ??);
normalize nodelta
@generalize_callee
@generalize_callee
cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
>(int_trace_append_normal … NORMAL) normalize nodelta
cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
destruct @eq_f @eq_f
whd in match (gather_trace ??); >int_events_append
>associative_append @eq_f 
elim trace in NORMAL ⊢ %;
[ 1,3: #_ %
| 2,4:
  * #s1 #tr1 #tl #IH
  #N cases (andb_Prop_true … N) #N1 #Ntl
  whd in match (gather_trace ??); >int_events_append
  >associative_append >(IH Ntl)
  >(int_trace_of_normal … N1)
  cases (intensional_trace_of_trace ?? tl)
  #cs' #tl' >associative_append %
] qed.

(* Measuring stack usage.  The intensional_event to cost part is handled by a
   common function with the structured traces version in common/stacksize.ma. *)  

definition measure_stack : (ident → option nat) → stacksize_info → list intensional_event → stacksize_info ≝
λcosts,start,ev.
  update_stacksize_info costs start (extract_call_ud_from_observables ev).


(* Check that the trace ends with the return from the starting function and one
   further state. *)

let rec will_return_aux C (depth:nat)
                        (trace:list (cs_state … C × trace)) on trace : bool ≝
match trace with
[ nil ⇒ false
| cons h tl ⇒
  let 〈s,tr〉 ≝ h in
  match cs_classify C s with
  [ cl_call ⇒ will_return_aux C (S depth) tl
  | cl_return ⇒
      match depth with
       (* The state after the return will appear in the structured trace, but
          not here because it is the second part of the pair returned by
          exec_steps. *)
      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
      | S d ⇒ will_return_aux C d tl
      ]
  | _ ⇒ will_return_aux C depth tl
  ]
].
definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.

(* Like classified_system, but we don't fix the global environment so that we
   talk about the program separately. *)

record preclassified_system : Type[2] ≝ {
  pcs_exec :> fullexec io_out io_in;
  pcs_labelled : ∀g. state … pcs_exec g → bool;
  pcs_classify : ∀g. state … pcs_exec g → status_class;
  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
}.

definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
λC,g.
  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).



definition measurable : ∀C:preclassified_system.
  ∀p:program ?? C. nat → nat →
  (ident → option nat) (* stack cost *) →
  nat → Prop ≝
λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
  let g ≝ make_global … (pcs_exec … C) p in
  let C' ≝ pcs_to_cs C g in
  make_initial_state … p = OK ? s0 ∧
  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
  trace_is_label_to_return C' interesting ∧
  bool_to_Prop (will_return' C' interesting) ∧
  le (maximum (measure_stack stack_cost (mk_stacksize_info 0 0) (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting))))) max_allowed_stack.



definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
λC,p,m,n.
  let g ≝ make_global … (pcs_exec … C) p in
  let C' ≝ pcs_to_cs C g in
  ! s0 ← make_initial_state … p;
  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.

(* CSC: Main debug function for the extracted code.
   It returns the list of all observed states and their observables,
   the last state and the reason for stopping execution. If the last
   state is final, it also returns the exit value. *)
let rec observe_all_in_measurable (n:nat) (fx:classified_system)
 (observe: intensional_event → unit) (callstack: list ident)
 (s:state … fx (cs_global fx)) :
 list intensional_event × (res int) ≝
match n with
[ O ⇒
  let res ≝
   match is_final … fx (cs_global … fx) s with
   [ Some r ⇒ OK … r
   | None ⇒ Error … (msg NotTerminated) ]
  in
   〈[ ],res〉
| S m ⇒
  match is_final … fx (cs_global … fx) s with
  [ Some r ⇒ 〈[ ],OK … r〉
  | None ⇒
    match step … fx (cs_global … fx) s with
    [ Value trs ⇒
        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
        let 〈callstack,callevent〉 ≝
         match cs_classify fx s
         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
                 list ident × (list intensional_event)
         with
         [ cl_call ⇒
            λcallee. let id ≝ callee I in
            〈id::callstack,[IEVcall id]〉
         | cl_return ⇒ λ_.
            match callstack with
            [ nil ⇒ 〈[ ],[ ]〉
            | cons id tl ⇒ 〈tl,[IEVret id]〉]
         | _ ⇒ λ_. 〈callstack, [ ]〉
         ] (cs_callee fx s) in
        let events ≝ costevents@callevent in
        let dummy : list unit ≝ map ?? observe events in
        let 〈tl,res〉 ≝
         observe_all_in_measurable m fx observe callstack (\snd trs) in
         〈events@tl,res〉
    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
    | Wrong m ⇒ 〈[ ],Error … m〉
    ]
  ]
].