include "common/Measurable.ma".
include "RTLabs/RTLabs_traces.ma".

definition RTLabs_system : preclassified_system ≝
mk_preclassified_system
  RTLabs_fullexec
  (λ_.RTLabs_cost)
  (λ_. RTLabs_classify) ?.

notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }.
notation "hbox(‘ ident i : t ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in (? : $t)) }.

(* The start and end states are existentially quantified because the states
   need to be extended with the shadow stack of functions.  (I'm not sure that
   was such a great idea now...)  In principle the quantified away part of the
   stack would be important for stack-space correctness, except that the
   structured trace will never touch it, only the suffix of the trace will.
   We could extract the true value from the execution of the prefix anyway. *)

(* XXX: split of observables seem arbitrary *)

theorem measurable_structured_trace : ∀p,m,n,stack_cost,max_stack,obs_pre,obs.
  measurable RTLabs_system p m n stack_cost max_stack →
  observables RTLabs_fullexec p m n = Some ? 〈obs_pre,obs〉 →
  ∃start,end:RTLabs_ext_state (make_global … p).
    state_at … RTLabs_system p m = Some state start →
    state_at … RTLabs_system p n = Some state end →
  ∃tlr:trace_label_return (RTLabs_status (make_global … p)) start end.
    obs = ‘obs’ tlr. 

(* XXX: need some assumption on start to kick off further simulations, presumably
   from the execution of the prefix? *)

(*
  There is no clock in the states of rtlabs, instead it's extracted from the
  whole trace.  Might not match up well with asm?
  
  i.e., do we build the clock into the semantics so that it appears in the
  structured trace (or equiv, use an instrumented semantics), or use the time
  implict from the observables?
*)