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 : classified_system → Type[0] ≝ λC. list (trace × (cs_state C)).

let rec split_trace C (x:execution (cs_state C) io_out io_in) (n:nat) on n : option (execution_prefix C × (execution (cs_state C) io_out io_in)) ≝
match n with
[ O ⇒ Some ? 〈[ ], x〉
| S n' ⇒
  match x with
  [ e_step tr s x' ⇒
    ! 〈pre,x''〉 ← split_trace C x' n';
    Some ? 〈〈tr,s〉::pre,x''〉
  | _ ⇒ None ?
  ]
].

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

definition measure_stack : ∀C. execution_prefix 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 C → nat ≝
λC,x. \fst (measure_stack C x).

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

let rec will_return_aux C (depth:nat)
                        (trace:execution_prefix C) on trace : bool ≝
match trace with
[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ 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
      [ O ⇒ false
      | S d ⇒ will_return_aux C d tl
      ]
  | _ ⇒ will_return_aux C depth tl
  ]
].
definition will_return' : ∀C. execution_prefix 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
}.

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_labelled C' interesting ∧
  bool_to_Prop (will_return' C' interesting) ∧
  le (max_stack C' (prefix@interesting)) max_allowed_stack.