source: src/RTLabs/Traces.ma @ 1595

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
      [ dp 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. 

(*
(* If we'll return then we must return from calls. *)
lemma will_return_call : ∀ge,depth,s,trace.
  will_return ge (S depth) s trace →
  will_return ge depth s trace.
#ge #depth #s #trace #H elim H in ⊢ ?;
[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
| #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/
| #H215 #H216 #H217 #H218 #H219 #H220 #H221
  inversion H221
  [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct
  | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct
  | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct
  | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct
] qed. check will_return_call.
| #H130 #H131 #H132 #H133 #H134 #H135
  inversion H
  [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct
    cases H196 #E destruct
  

let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace)
  on H : will_return ge depth s trace ≝
match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with
[ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ?
| wr_call s tr s' d EX trace CL H' ⇒ λE. ?
| wr_ret s tr s' d EX trace CL H' ⇒ λE. ?
| wr_base s tr s' EX trace CL ⇒ λE. ?
] (refl ? (S depth)).
[ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H')
  @(will_return_call … H'')
| *: cases daemon ] qed.
| %2 /2/
| destruct cases d in H' ⊢ %;
  [ #H' @wr_base //
  | #d' #H' %3 /2/
  ]
| destruct
] qed.

(* If we'll return then we must return from calls. *)
lemma will_return_call : ∀ge,depth,s,trace.
  will_return ge (S depth) s trace →
  will_return ge depth s trace.
#ge #depth #s #trace #H lapply (refl ? (S depth))
generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %);
[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/
| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3
  
discriminator nat.



(* Find time until a nested call completes. *)
lemma nth_is_return_down : ∀ge,n,depth,s,trace.
  nth_is_return ge n (S depth) s trace →
  ∃m. nth_is_return ge m depth s trace.
#ge #n elim n
(* It's impossible to run out of time... *)
[ #depth #s #trace #H inversion H
  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
  ]
| #n' #IH #depth #s #trace #H inversion H
  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (IH depth s1' trace1 ?)
    [ #m' #H' %{(S m')} %1 //
    | //
    ]
  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (IH (S depth) s1' trace1 ?)
    [ #m' #H' %{(S m')} %2 //
    | //
    ]
  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (depth1) in H2 ⊢ %;
    [ #H2 %{O} %4 //
    | #depth' #H2 cases (IH depth' s1' trace1 ?)
      [ #m' #H' %{(S m')} %3 //
      | //
      ]
    ]
  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
  ]
] qed.

lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
  RTLabs_classify s = cl_call →
  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
  ∃m. nth_is_return ge m O s' trace.
#ge #n #s #tr #s' #EX #trace #CLASS #H 
inversion H
[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
  -H2 destruct >H1 in CLASS; #E destruct
| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
  @nth_is_return_down //
| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
  -H2 destruct
| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
] qed.

lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
  nth_is_return ge (pred n) O s' trace.
#ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
| #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
] qed.
*)

lemma will_return_notfn : ∀ge,s,tr,s',EX,trace.
  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
  will_return ge O s (ft_step ?? ge s tr s' EX trace) →
  will_return ge O s' trace.
#ge #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
| #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
| #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. *)

record trace_result (ge:genv) (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
}.

record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
  ends : trace_ends_with_ret;
  trace_res :> trace_result ge (T ends);
  terminates :
    (* We handle returns specially *)
    match ends with
    [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res)
    | ends_with_ret ⇒ True
    ]
}.

definition replace_sub_trace : ∀ge,T1,T2.
  ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝
λge,T1,T2,r,trace.
  mk_sub_trace_result ge 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,T1,T2.
  ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝
λge,T1,T2,r,trace.
  mk_trace_result ge T2
    (new_state … r)
    (remainder … r)
    (cost_labelled … r)
    trace
.

let rec make_label_return ge 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 O s trace)
  : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝

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

and make_label_label ge 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 O s trace)
  : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
let r ≝ make_any_label ge 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 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 O s trace)
  : sub_trace_result ge (λ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 (λ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 (λ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 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 (λ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 next trace' ENV_COSTLABELLED ??? in
        let r' ≝ make_any_label ge (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 (λ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 … tll)
|
| %{tr} @EV
| @(well_cost_labelled_state_step  … EV) //
| @I
| %{tr} @EV
| % whd in ⊢ (% → ?); >CL #E destruct
| @(well_cost_labelled_jump … EV) //
| @(well_cost_labelled_state_step  … EV) //
| @(will_return_notfn … TERMINATES) %2 @CL
| (* oh dear *)
| %{tr} @EV
| @(cost_labelled … r)
|
|
| 

 @(well_cost_labelled_state_step  … EV) //
| % whd in ⊢ (% → ?); >CL #E destruct
| @CS
| @(nth_is_return_notfn … TERMINATES) %1 @CL
| % whd in ⊢ (% → ?); >CS #E destruct
| @CL
| %{tr} @EV
| @(well_cost_labelled_state_step  … EV) //
| @(nth_is_return_notfn … TERMINATES) %1 @CL
| inversion TERMINATES
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
  ]
|


  
(* FIXME: there's trouble at the end of the program because we can't make a step
   away from the final return. *)