include "common/Executions.ma".
include "common/StructuredTraces.ma".  (* just for status_class *)

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

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

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〉 ≝
    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) 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 ⊢ (??%?);
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 flatten_append : ∀A,l1,l2.
  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
#A #l1 #l2
elim l1
[ %
| #h #t #IH whd in ⊢ (??%(??%?));
  change with (flatten ??) in match (foldr ?????); >IH
  change with (flatten ??) in match (foldr ?????);
  >associative_append %
] 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_trace_of_trace ???);
  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 ⊢ (??%%); 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.

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 ⊢ (? → ? → ??%%); 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.
  

definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
λcosts,start.
  foldl ?? (λx. λev.
    match ev with
    [ IEVcall id ⇒
        let 〈current_stack,max_stack〉 ≝ x in
        let new_stack ≝ current_stack + costs id in
        〈new_stack, max new_stack max_stack〉
    | IEVret id ⇒
        let 〈current_stack,max_stack〉 ≝ x in
        〈current_stack - costs id, max_stack〉
    | _ ⇒ x
    ]) 〈start,start〉.

definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
λcosts, start, trace. \snd (measure_stack costs start trace).

lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
  (∀acc,el. P acc → P (f acc el)) →
  ∀l,acc. P acc →
  P (foldl A B f acc l).
#A #B #P #f #IH #l elim l
[ //
| #h #t #IH' #acc #H @IH' @IH @H
] qed.
(*
lemma max_stack_step : ∀C,a,m,a',m',tr,s.
  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
  m' = max m a'.
#C #a #m #a' #m' #tr #s
whd in match (measure_stack_aux ???);
generalize in match (cs_stack C s); cases (cs_classify C s) #f
normalize nodelta #E destruct //
qed.

lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
  a1' = a2'.
#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
generalize in match (cs_stack C s); cases (cs_classify C s) #f
normalize nodelta
#E1 #E2 destruct
%
qed.


lemma max_stack_steps : ∀C,trace,a,m.
  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
#C #trace elim trace
[ #a #m >max_n_O %
| * #tr #s #tl #IH #a #m
  whd in match (foldl ?????);
  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
  whd in match (foldl ??? 〈a,O〉 ?);
  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
  >(IH a'') >IH
  >(max_stack_step … M)
  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
] qed.

lemma max_stack_append : ∀C,c1,ex1,ex2.
  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
#C #c1 #ex1 #ex2
whd in match (max_stack ???); whd in match (stack_after ???);
whd in match (max_stack ?? (ex1@ex2));
whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
generalize in match O; generalize in match c1; elim ex1
[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
| * #tr #s #tl #IH #c #m
  whd in match (foldl ?????); whd in ⊢ (???(???%));
  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
  >IH %
] qed.
*)  

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

(* FIXME: this definition is unreasonable because it presumes we can easily
   identify the change in stack usage from return states, but that information
   is rather implicit (we only really record the function called in the
   extended RTLabs states when building the structured traces). *)

definition measurable : ∀C:preclassified_system.
  ∀p:program ?? C. nat → nat →
  (ident → 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 (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.

(* TODO: probably ought to be elsewhere; use exec_steps instead

   Note that this does not include stack space
 *)

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)〉.