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

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_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
}.

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

definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).

let rec split_trace FE (g:global io_out io_in FE) (x:execution (state ?? FE g) io_out io_in) (n:nat) on n : option (execution_prefix (state … FE g) × (execution (state ?? FE g) io_out io_in)) ≝
match n with
[ O ⇒ Some ? 〈[ ], x〉
| S n' ⇒
  match x with
  [ e_step tr s x' ⇒
    ! 〈pre,x''〉 ← split_trace FE g x' n';
    Some ? 〈〈tr,s〉::pre,x''〉
    (* Necessary for a measurable trace at the end of the program *)
  | e_stop tr r s ⇒
    match n' with
    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ]
].

(* 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. execution_prefix (cs_state … C) → Prop ≝
λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.

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

definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
λC,x. \fst (measure_stack C x).

definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
λC,x. \snd (measure_stack C x).

(* 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:execution_prefix (cs_state … C)) on trace : bool ≝
match trace with
[ nil ⇒ false
| cons h tl ⇒
  let 〈tr,s〉 ≝ h in
  match cs_classify C s with
  [ cl_call ⇒ will_return_aux C (S depth) tl
  | cl_return ⇒
      match depth with
       (* We need to see the state after the return to build the structured
          trace. *)
      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
      | S d ⇒ will_return_aux C d tl
      ]
  | _ ⇒ will_return_aux C depth tl
  ]
].
definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.

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

(* 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 →
  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
  nat → Prop ≝
λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
  let cl_trace ≝ exec_inf … (cs_exec … C') p in
  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧ 
  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
  trace_is_label_to_return C' interesting ∧
  bool_to_Prop (will_return' C' interesting) ∧
  le (max_stack C' (prefix@interesting)) max_allowed_stack.

(* TODO: probably ought to be elsewhere

   Note that this does not include stack space
 *)

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

definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
λFE,p,m.
  let trace ≝ exec_inf … FE p in
  match split_trace FE ? trace m with
  [ Some x ⇒
    match \snd x with
    [ e_step _ s _ ⇒ Some ? s
    | e_stop _ _ s ⇒ Some ? s
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].