source: src/common/Measurable.ma @ 2649

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

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

(* 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_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
}.

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

(* 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.  ∃prefix,suffix,interesting,remainder.
  let C' ≝ pcs_to_cs C (make_global … p) stack_cost in
  let cl_trace ≝ exec_inf … (cs_exec … C') p in
  split_trace … cl_trace m = Some ? 〈prefix,suffix〉 ∧ 
  split_trace … 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 … 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 ?
  ].

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 … trace m with
  [ Some x ⇒
    match \snd x with
    [ e_step _ s _ ⇒ Some ? s
    | e_stop _ _ s ⇒ Some ? s
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].