include "RTLabs/semantics.ma".
include "common/StructuredTraces.ma".

discriminator status_class.

(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
       will be added later (LTL → LIN). *)

definition RTLabs_classify : state → status_class ≝
λs. match s with
[ State f _ _ ⇒
    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    [ St_cond _ _ _ ⇒ cl_jump
    | St_jumptable _ _ ⇒ cl_jump
    | _ ⇒ cl_other
    ]
| Callstate _ _ _ _ _ ⇒ cl_call
| Returnstate _ _ _ _ ⇒ cl_return
].

definition is_cost_label : statement → bool ≝
λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].

definition RTLabs_cost : state → bool ≝
λs. match s with
[ State f fs m ⇒
    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
| _ ⇒ false
].

definition RTLabs_status : genv → abstract_status ≝
λge.
  mk_abstract_status
    state
    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    (λs,c. RTLabs_classify s = c)
    (λs. RTLabs_cost s = true)
    (λs,s'. match s with
      [ mk_Sig s p ⇒
        match s return λs. RTLabs_classify s = cl_call → ? with
        [ Callstate fd args dst stk m ⇒
          λ_. match s' with
          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
          | _ ⇒ False
          ]
        | State f fs m ⇒ λH.⊥
        | _ ⇒ λH.⊥
        ] p
      ]).
[ normalize in H; destruct
| whd in H:(??%?);
  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
  normalize try #a try #b try #c try #d try #e try #g try #h destruct
] qed.

(* Before attempting to construct a structured trace, let's show that we can
   form flat traces with evidence that they were constructed from an execution.
   
   For now we don't consider I/O. *)


coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).

(* add I/O? *)
coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.

let corec make_flat_trace ge s
  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
  flat_trace io_out io_in ge s ≝
let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
| e_wrong m ⇒ λE. ft_wrong … s m ?
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
    >(?:is_final ????? = RTLabs_is_final s1) //
    lapply (refl ? (RTLabs_is_final s1))
    cases (RTLabs_is_final s1) in ⊢ (???% → %);
    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
    ]
  | *: #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct @refl
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E
      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
      destruct
      inversion H
      [ #a #b #c #E1 destruct
      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
      | #m #E1 destruct
      ]
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr1 #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct @refl
  ]
| whd in E:(??%?); >E in H; #H
  inversion H
  [ #a #b #c #E destruct
  | #a #b #c #d #E1 destruct
  | #m #E1 destruct
  ]
] qed.

let corec make_whole_flat_trace p s
  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
  (I:make_initial_state ??? p = OK ? s) :
  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
let ge ≝ make_global … p in
let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
| e_wrong m ⇒ λE. ⊥
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ whd in E:(??%?); >exec_inf_aux_unfold in E; 
  whd in ⊢ (??%? → ?);
  >(?:is_final ????? = RTLabs_is_final s) //
  lapply (refl ? (RTLabs_is_final s))
  cases (RTLabs_is_final s) in ⊢ (???% → %);
  [ #_ whd in ⊢ (??%? → ?); #E destruct
  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
  ]
| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
    [ #a #b #c #E1 destruct
    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
      @H1
    | #m #E1 destruct
    ]
  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
] qed.

(* Need a way to choose whether a called function terminates.  Then,
     if the initial function terminates we generate a purely inductive structured trace,
     otherwise we start generating the coinductive one, and on every function call
       use the choice method again to decide whether to step over or keep going.

Not quite what we need - have to decide on seeing each label whether we will see
another or hit a non-terminating call?

Also - need the notion of well-labelled in order to break loops.



outline:

 does function terminate?
 - yes, get (bound on the number of steps until return), generate finite
        structure using bound as termination witness
 - no,  get (¬ bound on steps to return), start building infinite trace out of
        finite steps.  At calls, check for termination, generate appr. form.

generating the finite parts:

We start with the status after the call has been executed; well-labelling tells
us that this is a labelled state.  Now we want to generate a trace_label_return
and also return the remainder of the flat trace.

*)

(* [will_return ge depth s trace] says that after a finite number of steps of
   [trace] from [s] we reach the return state for the current function.  [depth]
   performs the call/return counting necessary for handling deeper function
   calls.  It should be zero at the top level. *)
inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
| wr_step : ∀s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
    will_return ge depth s' trace →
    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
| wr_call : ∀s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_call →
    will_return ge (S depth) s' trace →
    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
| wr_ret : ∀s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_return →
    will_return ge depth s' trace →
    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
    (* Note that we require the ability to make a step after the return (this
       corresponds to somewhere that will be guaranteed to be a label at the
       end of the compilation chain). *)
| wr_base : ∀s,tr,s',EX,trace.
    RTLabs_classify s = cl_return →
    will_return ge O s (ft_step ?? ge s tr s' EX trace)
.

discriminator nat.

lemma will_return_call : ∀ge,depth,s,trace.
  will_return ge depth s trace →
  will_return ge (pred depth) s trace.
#ge #depth #s #trace #H elim H
[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
  cases d in H1 H2 ⊢ %; //
| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
| #s1 #tr #s2 #EX #trc #CL %4 //
] qed. 


lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
  will_return ge d s (ft_step ?? ge s tr s' EX trace) →
  will_return ge d s' trace.
#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct
| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct
| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
] qed.

(* We require that labels appear after branch instructions and at the start of
   functions.  The first is required for preciseness, the latter for soundness.
   We will make a separate requirement for there to be a finite number of steps
   between labels to catch loops for soundness (is this sufficient?). *)

definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
λf,s. match s return λs. labels_present ? s → Prop with
[ St_cond _ l1 l2 ⇒ λH.
    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
| St_jumptable _ ls ⇒ λH.
    (* I did have a dependent version of All here, but it's a pain. *)
    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
| _ ⇒ λ_. True
]. whd in H;
[ @(proj1 … H)
| @(proj2 … H)
] qed.

definition well_cost_labelled_fn : internal_function → Prop ≝
λf. (∀l. ∀H:present … (f_graph f) l.
         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
[ @lookup_lookup_present | cases (f_entry f) // ] qed.

(* We need to ensure that any code we come across is well-cost-labelled.  We may
   get function code from either the global environment or the state. *)

definition well_cost_labelled_ge : genv → Prop ≝
λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.

definition well_cost_labelled_state : state → Prop ≝
λs. match s with
[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
                          All ? (λf. well_cost_labelled_fn (func f)) fs
| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
].

lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
  eval_statement ge s = Value ??? 〈tr,s'〉 →
  well_cost_labelled_ge ge →
  well_cost_labelled_state s →
  well_cost_labelled_state s'.
#ge #s #tr' #s' #EV cases (eval_perserves … EV)
[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
] qed.

lemma rtlabs_jump_inv : ∀s.
  RTLabs_classify s = cl_jump →
  ∃f,fs,m. s = State f fs m ∧ 
  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
*
[ #f #fs #m #E
  %{f} %{fs} %{m} %
  [ @refl
  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
    [ %1 %{A} %{B} %{C} @refl
    | %2 %{A} %{B} @refl
    ]
  ]
| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
| normalize #H8 #H9 #H10 #H11 #H12 destruct
] qed.

lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
  eval_statement ge s = Value ??? 〈tr,s'〉 →
  well_cost_labelled_state s →
  RTLabs_classify s = cl_jump →
  RTLabs_cost s' = true.
#ge #s #tr #s' #EV #H #CL
cases (rtlabs_jump_inv s CL)
#fr * #fs * #m * #Es *
[ * #r * #l1 * #l2 #Estmt
  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
  >Estmt #LP whd in ⊢ (??%? → ?);
  (* replace with lemma on successors? *)
  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
  lapply (Hbody (next fr) (next_ok fr))
  generalize in ⊢ (???% → ?);
  >Estmt #LP'
  whd in ⊢ (% → ?);
  * #H1 #H2 [ @H1 | @H2 ]
| * #r * #ls #Estmt
  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
  >Estmt #LP whd in ⊢ (??%? → ?);
  (* replace with lemma on successors? *)
  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
  [ 2: (* later *)
  | *: #E destruct
  ]
  lapply (Hbody (next fr) (next_ok fr))
  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
  generalize in ⊢ (??(?%)? → ?);
  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
  [ #E1 #E2 whd in E2:(??%?); destruct
  | #l' #E1 #E2 whd in E2:(??%?); destruct
    cases (All_nth ???? CP ? E1)
    #H1 #H2 @H2
  ]
] qed.

lemma rtlabs_call_inv : ∀s.
  RTLabs_classify s = cl_call →
  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
* [ #f #fs #m whd in ⊢ (??%? → ?);
    cases (lookup_present … (next f) (next_ok f)) normalize
    try #A try #B try #C try #D try #E try #F try #G destruct
  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
  | normalize #H411 #H412 #H413 #H414 #H415 destruct
  ] qed.

lemma well_cost_labelled_call : ∀ge,s,tr,s'.
  eval_statement ge s = Value ??? 〈tr,s'〉 →
  well_cost_labelled_state s →
  RTLabs_classify s = cl_call →
  RTLabs_cost s' = true.
#ge #s #tr #s' #EV #WCL #CL
cases (rtlabs_call_inv s CL)
#fd * #args * #dst * #stk * #m #E >E in EV WCL;
whd in ⊢ (??%? → % → ?);
cases fd
[ #fn whd in ⊢ (??%? → % → ?);
  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
  #m' #b whd in ⊢ (??%? → ?); #E' destruct
  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
  @WCL2
| #fn whd in ⊢ (??%? → % → ?);
  @bindIO_value #evargs #Eargs
  @bindIO_value #evres #Eres
  normalize in Eres; destruct
] qed.

(* Don't need to know that labels break loops because we have termination. *)

(* A bit of mucking around with the depth to avoid proving termination after
  termination. *)
record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ {
  new_state : state;
  remainder : flat_trace io_out io_in ge new_state;
  cost_labelled : well_cost_labelled_state new_state;
  new_trace : T new_state;
  terminates : match depth with
               [ O ⇒ True
               | S d ⇒ will_return ge d new_state remainder
               ]
}.

record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
  ends : trace_ends_with_ret;
  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends)
}.

definition replace_sub_trace : ∀ge,trm,T1,T2.
  ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝
λge,trm,T1,T2,r,trace.
  mk_sub_trace_result ge trm T2
    (ends … r)
    (mk_trace_result ge ? (T2 (ends … r))
      (new_state … r)
      (remainder … r)
      (cost_labelled … r)
      trace
      (terminates … r)
    )
.

definition replace_trace : ∀ge,trm,T1,T2.
  ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝
λge,trm,T1,T2,r,trace.
  mk_trace_result ge trm T2
    (new_state … r)
    (remainder … r)
    (cost_labelled … r)
    trace
    (terminates … r)
.

let rec make_label_return ge depth s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
  (TERMINATES: will_return ge depth s trace)
  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝

  let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) → ? with
  [ ends_with_ret ⇒ λr.
      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
  | doesnt_end_with_ret ⇒ λr.
      let r' ≝ make_label_return ge depth (new_state … r)
                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (terminates ??? r) in
        replace_trace … r'
          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
  ] (trace_res … r)

and make_label_label ge depth s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
  (TERMINATES: will_return ge depth s trace)
  : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝
let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
  replace_sub_trace … r
    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)

and make_any_label ge depth s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (TERMINATES: will_return ge depth s trace)
  : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝
match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with
[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    [ cl_other ⇒ λCL.
        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
        [ true ⇒ λCS.
            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
              doesnt_end_with_ret
              (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
        | false ⇒ λCS.
            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in
                replace_sub_trace … r
                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
        ] (refl ??)
    | cl_jump ⇒ λCL.
        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
          doesnt_end_with_ret
          (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 
    | cl_call ⇒ λCL.
        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in
        let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
        replace_sub_trace ???? r'
          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
    | cl_return ⇒ λCL.
        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
          ends_with_ret
          (mk_trace_result ge ??
            next
            trace'
            ?
            (tal_base_return (RTLabs_status ge) start next ? CL)
            ?)
    ] (refl ? (RTLabs_classify start))
| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
] STATE_COSTLABELLED TERMINATES.

[ @(trace_label_label_label … (new_trace … r))
|
| inversion TERMINATES
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct >CL in H7; * #E destruct
  | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 -TERMINATES destruct >CL in H21; #E destruct
  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 -TERMINATES destruct @H36
  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I
  ]
| %{tr} @EV
| @(well_cost_labelled_state_step  … EV) //
| whd @(will_return_notfn … TERMINATES) %2 @CL
| %{tr} @EV
| % whd in ⊢ (% → ?); >CL #E destruct
| @(well_cost_labelled_jump … EV) //
| @(well_cost_labelled_state_step  … EV) //
| (* oh dear *)
| %{tr} @EV
| @(cost_labelled … r)
| @(terminates … r)
| @(well_cost_labelled_state_step  … EV) //
| @(well_cost_labelled_call … EV) //
| inversion TERMINATES
  [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 -TERMINATES destruct >CL in H60; * #E destruct
  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 -TERMINATES destruct @H75
  | #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 -TERMINATES destruct >CL in H88; #E destruct
  | #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 -TERMINATES destruct >CL in H101; #E destruct
  ]
| whd @(will_return_notfn … TERMINATES) %1 @CL
| %{tr} @EV
| % whd in ⊢ (% → ?); >CL #E destruct
| @CS
| @(well_cost_labelled_state_step  … EV) //
| % whd in ⊢ (% → ?); >CS #E destruct
| @CL
| %{tr} @EV
| @(well_cost_labelled_state_step  … EV) //
| @(will_return_notfn … TERMINATES) %1 @CL
| inversion TERMINATES
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct
  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES destruct
  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES destruct
  ]
|


  
(* FIXME: there's trouble at the end of the program because we can't make a step
   away from the final return.
   
   We need to show that the "next pc" is preserved through a function call.
   
   Tail-calls are not handled properly (which means that if we try to show the
   full version with non-termination we'll fail because calls and returns aren't
   balanced.
   
   The guardedness check will reject the recursive definition above; need to
   rearrange things so that this works properly.
 *)