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
| Finalstate _ ⇒ cl_other
].

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 ∧ f_graph (func h) = f_graph (func f) ]
          | Finalstate r ⇒ stk = [ ]
          | _ ⇒ False
          ]
        | State f fs m ⇒ λH.⊥
        | _ ⇒ λH.⊥
        ] p
      ]).
[ normalize in H; destruct
| 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.

lemma RTLabs_not_cost : ∀ge,s.
  RTLabs_cost s = false →
  ¬ as_costed (RTLabs_status ge) s.
#ge #s #E % whd in ⊢ (% → ?); >E #E' 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.

coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
| nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr').

lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
  not_wrong o i ge s' tr'.
#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
[ #H105 #H106 #H107 #H108 #H109 destruct
| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
] qed.

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 → Type[0] ≝
| 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)
.

(* The way we will use [will_return] won't satisfy Matita's guardedness check,
   so we will measure the length of these termination proofs and use an upper
   bound to show termination of the finite structured trace construction
   functions. *)

let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
match T with
[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
| wr_base _ _ _ _ _ _ ⇒ S O
].

include alias "arithmetics/nat.ma".

(* Specialised to the particular situation it is used in. *)
lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
whd in ⊢ (??(??%) → ?);
>commutative_times
#H lapply (le_plus_b … H)
#H lapply (le_to_leb_true … H)
normalize #E destruct
qed.
   
let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝
match T with
[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
].

(* Inversion lemmas on [will_return] that also note the effect on the length
   of the proof. *)
lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
  RTLabs_classify s = cl_call →
  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
] qed.

lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
  RTLabs_classify s = cl_return →
  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
  match d with
  [ O ⇒ will_return_end … TM = ❬s', trace❭
  | S d' ⇒
      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
  ].
#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
] qed.

lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
#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 % /2/
| #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 % /2/
| #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.

(* When it comes to building bits of nonterminating executions we'll need to be
   able to glue termination proofs together. *)

lemma will_return_prepend : ∀ge,d1,s1,t1.
  ∀T1:will_return ge d1 s1 t1.
  ∀d2,s2,t2.
  will_return ge d2 s2 t2 →
  will_return_end … T1 = ❬s2, t2❭ →
  will_return ge (d1 + S d2) s1 t1.
#ge #d1 #s1 #tr1 #T1 elim T1
[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
  %1 // @(IH … T2) @E
| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
] qed.

discriminator nat.

lemma will_return_remove_call : ∀ge,d1,s1,t1.
  ∀T1:will_return ge d1 s1 t1.
  ∀d2.
  will_return ge (d1 + S d2) s1 t1 →
  ∀s2,t2.
  will_return_end … T1 = ❬s2, t2❭ →
  will_return ge d2 s2 t2.
(* The key part of the proof is to show that the two termination proofs follow
   the same pattern. *)
#ge #d1x #s1x #t1x #T1 elim T1
[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
                   >H21 in CL; * #E destruct
                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
                   >H35 in CL; * #E destruct
                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
                   >H48 in CL; * #E destruct
                 ]
  | @E
  ]
| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
                   >CL in H7; * #E destruct
                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
                   >H35 in CL; #E destruct
                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
                   >H48 in CL; #E destruct
                 ]
  | @E
  ]
| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
                   >CL in H7; * #E destruct
                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
                   >H21 in CL; #E destruct
                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
                   whd in H38:(??%??); destruct //
                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
                   whd in H49:(??%??); @⊥ destruct
                 ]
  | @E
  ]
| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
                 >CL in H7; * #E destruct
               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
                 >H21 in CL; #E destruct
               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
                 whd in H38:(??%??); destruct //
               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
                 whd in H49:(??%??); @⊥ destruct
               ]
] qed.

lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
  ∀T:will_return ge d s t.
  not_wrong io_out io_in ge s t →
  will_return_end … T = ❬s', t'❭ →
  not_wrong io_out io_in ge s' t'.
#ge #d #s #t #s' #t' #T elim T
[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
  [ inversion NW
    [ #H1 #H2 #H3 #H4 #H5 destruct
    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
    ]
  | @E
  ]
| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
  | @E
  ]
| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
  | @E
  ]
| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 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
| Finalstate _ ⇒ True
].

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
| #r #E normalize in E; 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? *)
  @bind_value #v #Ev @bind_ok * #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? *)
  @bind_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
  | normalize #H1 #H2 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 ⊢ (??%? → % → ?);
  @bind_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
  whd in ⊢ (??%? → ?);
  #E' destruct
] qed.


(* The preservation of (most of) the stack is useful to show as_after_return.
   We do this by showing that during the execution of a function the lower stack
   frames never change, and that after returning from the function we preserve
   the identity of the next instruction to execute.
 *)

inductive stack_of_state : list frame → state → Prop ≝
| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
.

inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
| sp_normal : ∀fs,s1,s2.
    stack_of_state fs s1 →
    stack_of_state fs s2 →
    stack_preserved doesnt_end_with_ret s1 s2
| sp_finished : ∀s1,f,f',fs,m.
    next f = next f' →
    frame_rel f f' →
    stack_of_state (f::fs) s1 →
    stack_preserved ends_with_ret s1 (State f' fs m)
| sp_stop : ∀s1,r.
    stack_of_state [ ] s1 →
    stack_preserved ends_with_ret s1 (Finalstate r)
| sp_top : ∀fd,args,dst,m,r.
    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
.

discriminator list.

lemma stack_of_state_eq : ∀fs,fs',s.
  stack_of_state fs s →
  stack_of_state fs' s →
  fs = fs'.
#fs0 #fs0' #s0 *
[ #f #fs #m #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
| #fd #args #dst #f #fs #m #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
| #rtv #dst #fs #m #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
] qed.

lemma stack_preserved_final : ∀e,r,s.
  ¬stack_preserved e (Finalstate r) s.
#e #r #s % #H inversion H
[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
  inversion SOS #a #b #c #d #e #f try #g try #h destruct
| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
  inversion SOS #a #b #c #d #e #f try #g try #h destruct
| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
  inversion SOS #a #b #c #d #e #f try #g try #h destruct
| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
] qed.

lemma stack_preserved_join : ∀e,s1,s2,s3.
  stack_preserved doesnt_end_with_ret s1 s2 →
  stack_preserved e s2 s3 →
  stack_preserved e s1 s3.
#e1 #s1 #s2 #s3 #H1 inversion H1
[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
  #H2 inversion H2
  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
    inversion S2
    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
    ]
  ]
| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
  cases (stack_preserved_final … H) #r #E destruct
| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
  @(absurd … F) //
] qed.

lemma stack_preserved_return : ∀ge,s1,s2,tr.
  RTLabs_classify s1 = cl_return →
  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
  stack_preserved ends_with_ret s1 s2.
#ge *
[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
  cases (lookup_present ??? (next f) (next_ok f)) in E;
  normalize #a try #b try #c try #d try #e try #f try #g destruct
| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
| #res #dst *
  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
    whd in EV:(??%?); destruct @(sp_finished ? f) //
    cases f //
  ]
| #r #s2 #tr #E normalize in E; destruct 
] qed.

lemma stack_preserved_step : ∀ge,s1,s2,tr.
  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
  stack_preserved doesnt_end_with_ret s1 s2.
#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
  normalize in CL; cases CL #E destruct
| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
  #E normalize in E; destruct
| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
] qed.

lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
  RTLabs_classify s1 = cl_call →
  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
  stack_preserved ends_with_ret s2 s3 →
  stack_preserved doesnt_end_with_ret s1 s3.
#ge #s1 #s2 #s3 #tr #CL #EV #SP
cases (rtlabs_call_inv … CL)
#fd * #args * #dst * #stk * #m #E destruct
inversion SP
[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
  inversion (eval_perserves … EV)
  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
    inversion S
    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
    ]
  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
  ]
| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
  inversion (eval_perserves … EV)
  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
    inversion S1
    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
    ]
  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
  ]
| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
] qed. 
  
lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
  ∀CL : RTLabs_classify s1 = cl_call.
  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
  stack_preserved ends_with_ret s2 s3 →
  as_after_return (RTLabs_status ge) «s1,CL» s3.
#ge #s1 #s2 #s3 #tr #CL #EV #S23
cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
inversion S23
[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
  inversion (eval_perserves … EV)
  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
    inversion S
    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
    ]
  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
  ]
| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
  inversion (eval_perserves … EV)
  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
    inversion S1
    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
    ]
  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
  ]
| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 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.  Note that we keep a proof that our upper bound on the length
   of the termination proof is respected. *)
record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
  (start:state) (full:flat_trace io_out io_in ge start)
  (original_terminates: will_return ge depth start full)
  (T:state → Type[0]) (limit:nat) : 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;
  stack_ok : stack_preserved ends start new_state;
  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
               | S d ⇒ ΣTM:will_return ge d new_state remainder.
                         limit > will_return_length … TM ∧
                         will_return_end … original_terminates = will_return_end … TM
               ]
}.

(* The same with a flag indicating whether the function returned, as opposed to
   encountering a label. *)
record sub_trace_result (ge:genv) (depth:nat)
  (start:state) (full:flat_trace io_out io_in ge start)
  (original_terminates: will_return ge depth start full)
  (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
{
  ends : trace_ends_with_ret;
  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
}.

(* We often return the result from a recursive call with an addition to the
   structured trace, so we define a couple of functions to help.  The bound on
   the size of the termination proof might need to be relaxed, too. *)

definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
    will_return_end … TM1 = will_return_end … TM2 →
    T2 (new_state … r) →
    stack_preserved e s2 (new_state … r) →
    trace_result ge d e s2 t2 TM2 T2 l2 ≝
λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
  mk_trace_result ge d e s2 t2 TM2 T2 l2
    (new_state … r)
    (remainder … r)
    (cost_labelled … r)
    trace
    SP
    ?
    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 
                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
. 
cases e in r ⊢ %;
[ <TME -TME * cases d in TM1 TM2 ⊢ %;
  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
    %{TMa} % // @(transitive_le … lGE) @L1
  ]
| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
   * #TMa * #L1 #TME
    %{TMa} % // @(transitive_le … lGE) @L1
] qed.

definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
    will_return_end … TM1 = will_return_end … TM2 →
    T2 (ends … r) (new_state … r) →
    stack_preserved (ends … r) s2 (new_state … r) →
    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
    (ends … r)
    (replace_trace … lGE … r TME trace SP).

(* Small syntax hack to avoid ambiguous input problems. *)
definition myge : nat → nat → Prop ≝ ge.

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)
  (TIME: nat)
  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
              (trace_label_return (RTLabs_status ge) s)
              (will_return_length … TERMINATES) ≝
              
match TIME return λTIME. TIME ≥ ? → ? with
[ O ⇒ λTERMINATES_IN_TIME. ⊥
| S TIME ⇒ λTERMINATES_IN_TIME.

  let r ≝ make_label_label ge depth s
            trace
            ENV_COSTLABELLED
            STATE_COSTLABELLED
            STATEMENT_COSTLABEL
            TERMINATES
            TIME ? in
  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
  [ ends_with_ret ⇒ λr.
      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
  | doesnt_end_with_ret ⇒ λr.
      let r' ≝ make_label_return ge depth (new_state … r)
                 (remainder … r)
                 ENV_COSTLABELLED
                 (cost_labelled … r) ?
                 (pi1 … (terminates … r)) TIME ? 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)

] TERMINATES_IN_TIME


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)
  (TIME: nat)
  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
  on TIME : sub_trace_result ge depth s trace TERMINATES
              (λends. trace_label_label (RTLabs_status ge) ends s)
              (will_return_length … TERMINATES) ≝
              
match TIME return λTIME. TIME ≥ ? → ? with
[ O ⇒ λTERMINATES_IN_TIME. ⊥
| S TIME ⇒ λTERMINATES_IN_TIME.

let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
  replace_sub_trace … r ?
    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)

] TERMINATES_IN_TIME


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)
  (TIME: nat)
  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
  on TIME : sub_trace_result ge depth s trace TERMINATES
              (λends. trace_any_label (RTLabs_status ge) ends s)
              (will_return_length … TERMINATES) ≝

match TIME return λTIME. TIME ≥ ? → ? with
[ O ⇒ λTERMINATES_IN_TIME. ⊥
| S TIME ⇒ λTERMINATES_IN_TIME.

  match trace return λs,trace. well_cost_labelled_state s →
                               ∀TM:will_return ??? trace.
                               myge ? (times 3 (will_return_length ??? trace TM)) →
                               sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
  [ ft_stop st FINAL ⇒
      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥

  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    [ cl_other ⇒ λCL.
        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
        (* We're about to run into a label. *)
        [ true ⇒ λCS.
            mk_sub_trace_result ge depth start ? TERMINATES (λ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 ?? CS) ??)
        (* An ordinary step, keep going. *)
        | false ⇒ λCS.
            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in 
                replace_sub_trace … r ?
                  (tal_step_default (RTLabs_status ge) (ends … r)
                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
        ] (refl ??)
        
    | cl_jump ⇒ λCL.
        mk_sub_trace_result ge depth start ? TERMINATES (λ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 ?? (will_return_call … CL TERMINATES) TIME ? in
        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
        (* We're about to run into a label, use base case for call *)
        [ true ⇒ λCS.
            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
            doesnt_end_with_ret
            (mk_trace_result ge …
              (tal_base_call (RTLabs_status ge) start next (new_state … r)
                ? CL ? (new_trace … r) CS) ??)
        (* otherwise use step case *)
        | false ⇒ λCS.
            let r' ≝ make_any_label ge depth
                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
                       (pi1 … (terminates … r)) TIME ? 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) (RTLabs_not_cost … CS) (new_trace … r')) ?
        ] (refl ??)

    | cl_return ⇒ λCL.
        mk_sub_trace_result ge depth start ? TERMINATES (λ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 TERMINATES_IN_TIME
] TERMINATES_IN_TIME.

[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
| //
| //
| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
| @(stack_preserved_join … (stack_ok … r)) //
| @(trace_label_label_label … (new_trace … r))
| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
  @(transitive_le …  (3*(will_return_length … TERMINATES)))
  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
    @(monotonic_le_times_r 3 … LT)
  | @le_S @le_S @le_n
  ]
| @le_S_S_to_le @TERMINATES_IN_TIME
| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
| @le_n
| //
| @le_S_S_to_le @TERMINATES_IN_TIME
| @(wrl_nonzero … TERMINATES_IN_TIME)
| (* We can't reach the final state because the function terminates with a
     return *)
  inversion TERMINATES
  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
  ]
| @(will_return_return … CL TERMINATES)
| /2 by stack_preserved_return/
| %{tr} @EV
| @(well_cost_labelled_state_step  … EV) //
| whd @(will_return_notfn … TERMINATES) %2 @CL
| @stack_preserved_step /2/
| %{tr} @EV
| %1 whd @CL
| @(well_cost_labelled_jump … EV) //
| @(well_cost_labelled_state_step  … EV) //
| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
    #TMx * #LT' #_ @LT'
  | <EQr cases (will_return_call … CL TERMINATES)
    #TM' * #_ #EQ' @EQ'
  ]
| @(stack_preserved_call … EV (stack_ok … r)) //
| %{tr} @EV
| @RTLabs_after_call //
| @(cost_labelled … r)
| skip
| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
  @(transitive_lt … LT)
  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
| @RTLabs_after_call //
| %{tr} @EV
| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
| @(cost_labelled … r)
| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
  cases (will_return_call … TERMINATES) in GT;
  #X * #Y #_ #Z
  @(transitive_le … (monotonic_lt_times_r 3 … Y))
  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
  | //
  ]
| @(well_cost_labelled_state_step  … EV) //
| @(well_cost_labelled_call … EV) //
| cases (will_return_call … TERMINATES)
  #TM * #GT #_ @le_S_S_to_le
  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
  @(transitive_le … TERMINATES_IN_TIME)
  @(monotonic_le_times_r 3 … GT)
| whd @(will_return_notfn … TERMINATES) %1 @CL
| @(stack_preserved_step … EV) /2/
| %{tr} @EV
| %2 whd @CL
| @(well_cost_labelled_state_step  … EV) //
| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
| @CL
| %{tr} @EV
| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
| @(well_cost_labelled_state_step  … EV) //
| %1 @CL
| cases (will_return_notfn … TERMINATES) #TM * #GT #_
  @le_S_S_to_le
  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
  //
| inversion TERMINATES
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
  ]
] qed.

(* We can initialise TIME with a suitably large value based on the length of the
   termination proof. *)
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 ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
  (2 + 3 * will_return_length … TERMINATES) ?.
@le_n
qed.
  
(* Tail-calls would not be 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.
 *)

inductive inhabited (T:Type[0]) : Prop ≝
| witness : T → inhabited T.

(* We also require that program's traces are soundly labelled: for any state
   in the execution, we can give a distance to a labelled state or termination.
   
   Note that this differs from the syntactic notions in earlier languages
   because it is a global property.  In principle, we would have a loop broken
   only by a call to a function (which necessarily has a label) and no local
   cost label.
 *)

let rec nth_state ge s
  (trace: flat_trace io_out io_in ge s)
  n
  on n : option state ≝
match n with
[ O ⇒ Some ? s
| S n' ⇒
  match trace with
  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
  | _ ⇒ None ?
  ]
].

definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.

lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
  soundly_labelled_trace ge s' trace'.
#ge #s #tr #s' #EV #trace' #H
#n cases (H (S n)) #m #H' %{m} @H'
qed.

(* Define a notion of sound labellings of RTLabs programs. *)

let rec successors (s : statement) : list label ≝
match s with
[ St_skip l ⇒ [l]
| St_cost _ l ⇒ [l]
| St_const _ _ l ⇒ [l]
| St_op1 _ _ _ _ _ l ⇒ [l]
| St_op2 _ _ _ _ l ⇒ [l]
| St_load _ _ _ l ⇒ [l]
| St_store _ _ _ l ⇒ [l]
| St_call_id _ _ _ l ⇒ [l]
| St_call_ptr _ _ _ l ⇒ [l]
(*
| St_tailcall_id _ _ ⇒ [ ]
| St_tailcall_ptr _ _ ⇒ [ ]
*)
| St_cond _ l1 l2 ⇒ [l1; l2]
| St_jumptable _ ls ⇒ ls
| St_return ⇒ [ ]
].

definition actual_successor : state → option label ≝
λs. match s with
[ State f fs m ⇒ Some ? (next f)
| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
| Returnstate _ _ _ _ ⇒ None ?
| Finalstate _ ⇒ None ?
].

lemma nth_opt_Exists : ∀A,n,l,a.
  nth_opt A n l = Some A a →
  Exists A (λa'. a' = a) l.
#A #n elim n
[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
| #m #IH *
  [ #a #E normalize in E; destruct
  | #a #l #a' #E %2 @IH @E
  ]
] qed.

lemma eval_successor : ∀ge,f,fs,m,tr,s'.
  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
  RTLabs_classify s' = cl_return ∨
  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
whd in ⊢ (??%? → ?);
generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] 
  whd in ⊢ (??%? → ?);
  generalize in ⊢ (??(?%)? → ?);
  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
  [ #e #E normalize in E; destruct
  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
  ]
| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
] qed.

definition steps_for_statement : statement → nat ≝
λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).

inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
with bound_on_steps_to_cost1 : label → nat → Prop ≝
| bostc_step : ∀l,n,H.
    let stmt ≝ lookup_present … g l H in
    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
          bound_on_steps_to_cost g l' n) →
    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).

(*
lemma steps_to_label_bound_inv : ∀g,l,n.
  steps_to_label_bound g l n →
  ∀H. let stmt ≝ lookup_present … g l H in
  ∃n'. n = steps_for_statement stmt + n' ∧
  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
        steps_to_label_bound g l' n').
#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
qed.
  *)  

(*
definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.

let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
  soundly_labelled_pc (f_graph fn) (f_entry fn).


definition soundly_labelled_frame : frame → Prop ≝
λf. soundly_labelled_pc (f_graph (func f)) (next f).

definition soundly_labelled_state : state → Prop ≝
λs. match s with
[ State f _ _ ⇒ soundly_labelled_frame f
| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
].
*)
definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).

inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
| sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n
| sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
| sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n)
.

lemma state_bound_on_steps_to_cost_zero : ∀s.
  ¬ state_bound_on_steps_to_cost s O.
#s % #H inversion H
[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
] qed.

lemma eval_steps : ∀ge,f,fs,m,tr,s'.
  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
whd in ⊢ (??%? → ?);
generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] 
  whd in ⊢ (??%? → ?);
  generalize in ⊢ (??(?%)? → ?);
  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
  [ #e #E normalize in E; destruct
  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
  ]
| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
] qed.

lemma bound_after_call : ∀ge,s,s',n.
  state_bound_on_steps_to_cost s (S n) →
  ∀CL:RTLabs_classify s = cl_call.
  as_after_return (RTLabs_status ge) «s, CL» s' →
  RTLabs_cost s' = false →
  state_bound_on_steps_to_cost s' n.
#ge #s #s' #n #H inversion H
[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
  #fn * #args * #dst * #stk * #m' #E destruct
| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
  whd in S; #CL cases s'
  [ #f' #fs' #m' * #N #F #CS
    %1 whd
    inversion S
    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
    | #l #n #B #E1 #E2 #_ destruct <N <F @B
    ]
  | #fd' #args' #dst' #fs' #m' *
  | #rv #dst' #fs' #m' *
  | #r #E normalize in E; destruct
  ]
| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
] qed.

lemma bound_after_step : ∀ge,s,tr,s',n.
  state_bound_on_steps_to_cost s (S n) →
  eval_statement ge s = Value ??? 〈tr, s'〉 →
  RTLabs_cost s' = false →
  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
   state_bound_on_steps_to_cost s' n.
#ge #s #tr #s' #n #BOUND1 inversion BOUND1
[ #f #fs #m #m #FS #E1 #E2 #_ destruct
  #EVAL cases (eval_successor … EVAL)
  [ /3/
  | * #l * #S1 #S2 #NC %2
  (*
    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
    *)
    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
    inversion (eval_perserves … EVAL)
    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
      >(eval_steps … EVAL) in E2; #En normalize in En;
      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
      %1 inversion (IH … S2)
      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
        whd in S1:(??%?); destruct >NC in CSx; *
      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
      ]
    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
      >(eval_steps … EVAL) in E2; #En normalize in En;
      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
      %2 @IH normalize in S1; destruct @S2
    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
      destruct
    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
      normalize in S1; destruct
    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
    ]
  ]
| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
  /3/
| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
  #EVAL #NC %2 inversion (eval_perserves … EVAL)
  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
    %1 whd in FS ⊢ %;
    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
    inversion FS
    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
        >NC in CSx; *
    | #lx #nx #H #E1x #E2x #_ destruct @H
    ]
  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
  ]
] qed.
  
(* When constructing an infinite trace, we need to be able to grab the finite
   portion of the trace for the next [trace_label_diverges] constructor.  We
   use the fact that the trace is soundly labelled to achieve this. *)

inductive finite_prefix (ge:genv) : state → Prop ≝
| fp_tal : ∀s,s'.
           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
           flat_trace io_out io_in ge s' →
           finite_prefix ge s
| fp_tac : ∀s,s'.
           trace_any_call (RTLabs_status ge) s s' →
           flat_trace io_out io_in ge s' →
           finite_prefix ge s
.

definition fp_add_default : ∀ge,s,s'.
  RTLabs_classify s = cl_other →
  finite_prefix ge s' →
  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
  RTLabs_cost s' = false →
  finite_prefix ge s ≝
λge,s,s',OTHER,fp.
match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf 
    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    rem
| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf 
    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
].

definition fp_add_terminating_call : ∀ge,s,s1,s'.
  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
  ∀CALL:RTLabs_classify s = cl_call.
  finite_prefix ge s' →
  trace_label_return (RTLabs_status ge) s1 s' →
  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
  RTLabs_cost s' = false →
  finite_prefix ge s ≝
λge,s,s1,s',EVAL,CALL,fp.
match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with
[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    rem
| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    rem
].

lemma not_return_to_not_final : ∀ge,s,tr,s'.
  eval_statement ge s = Value ??? 〈tr, s'〉 →
  RTLabs_classify s ≠ cl_return →
  RTLabs_is_final s' = None ?.
#ge #s #tr #s' #EV
inversion (eval_perserves … EV) //
#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
@⊥ @(absurd ?? CL) @refl
qed.

definition termination_oracle ≝ ∀ge,depth,s,trace.
  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).

let rec finite_segment ge s n trace
  (ORACLE: termination_oracle)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
  (NOT_UNDEFINED: not_wrong … trace)
  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
  (NOT_FINAL: RTLabs_is_final s = None ?)
  on n : finite_prefix ge s ≝
match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
[ O ⇒ λLABEL_LIMIT. ⊥
| S n' ⇒
    match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → RTLabs_is_final s = None ? → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
    [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥
    | ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT.
        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.
                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
            | false ⇒ λCS.
                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ????? in
                fp_add_default ge ?? CL fs ? CS
            ] (refl ??)
        | cl_jump ⇒ λCL.
            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
        | cl_call ⇒ λCL.
            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
            [ or_introl TERMINATES ⇒
              match TERMINATES with [ witness TERMINATES ⇒ 
                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr)
                | false ⇒ λCS. 
                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ????? in
                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
                ] (refl ??)
              ]
            | or_intror NO_TERMINATION ⇒
                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
            ]
        | cl_return ⇒ λCL. ⊥
        ] (refl ??)
    | ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥
    ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION NOT_FINAL
] LABEL_LIMIT.
[ cases (state_bound_on_steps_to_cost_zero s) /2/
| @(absurd …  NOT_FINAL FINAL)
| @(absurd ?? NO_TERMINATION)
     %{0} % @wr_base //
| @(well_cost_labelled_jump … EV) //
| 5,6,7,8,9,10: /2/
| /2/
| //
| @(not_to_not … NO_TERMINATION) * #depth * #TM1 %{depth} %
  @wr_call //
  @(will_return_prepend … TERMINATES … TM1)
  cases (terminates … tlr) //
| @(will_return_not_wrong … TERMINATES)
  [ @(still_not_wrong … EV) //
  | cases (terminates … tlr) //
  ]
| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
| (* By stack preservation we cannot be in the final state *)
  inversion (stack_ok … tlr)
  [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
  | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
  | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
    cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
    inversion (eval_perserves … EV)
    [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -NOT_UNDEFINED -NO_TERMINATION destruct ]
    #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -NOT_UNDEFINED -NO_TERMINATION destruct
    inversion S
    [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
    (* state_bound_on_steps_to_cost needs to know about the current stack frame,
       so we can use it as a witness that at least one frame exists *)
    inversion LABEL_LIMIT
    #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
  | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
  ]
| @(well_cost_labelled_state_step … EV) //
| @(well_cost_labelled_call … EV) //
| 19,20,21: /2/
| @(well_cost_labelled_state_step … EV) //
| @(not_to_not … NO_TERMINATION)
  * #depth * #TERM %{depth} % @wr_step /2/
| @(still_not_wrong … NOT_UNDEFINED)
| cases (bound_after_step … LABEL_LIMIT EV ?)
  [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // |
    inversion trace'
    [ #s0 #FINAL #E1 #E2 destruct @⊥
      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
      % >CL #E destruct
    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct
      @wr_base //
    | #H99 #H100 #H101 #H102 #H103 destruct
      inversion NOT_UNDEFINED
      [ #H137 #H138 #H139 #H140 #H141 destruct
      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct
        inversion H148
        [ #H153 #H154 #H155 #H156 #H157 destruct
        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
        ]
      ]
    ]
    ]
    | >CL #E destruct
    ]
  | //
  | //
  ]
| @(not_return_to_not_final … EV) >CL % #E destruct
| inversion NOT_UNDEFINED
  [ #H169 #H170 #H171 #H172 #H173 destruct
  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
  ]
] qed.

(*
let corec make_label_diverges 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 *)
  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
  : trace_label_diverges (RTLabs_status ge) s ≝ ?
.
*)