source: src/RTLabs/RTLabs_partial_traces.ma @ 2895

(* This deals with the construction of structured traces of finite parts of
   RTLabs program executions.  It will be used as part of the whole compiler's
   intensional correctness proof.
   
   It was originally based on RTLabs/RTLabs_traces.ma, which constructs whole
   execution structured traces, but dealing with the whole program execution
   is unnecessary, it requires classical reasoning for deciding when functions
   terminate and it doesn't fit well with some of the other definitions.
   
   In principle we could clean this up a little by harmonising some of the
   definitions with other parts of the development. *)

include "RTLabs/RTLabs_abstract.ma".
include "RTLabs/CostSpec.ma".
include "RTLabs/CostMisc.ma".
include "common/Executions.ma".
include "utilities/listb_extra.ma".


(* Allow us to move between the different notions of when a state is cost
   labelled. *)

lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
  RTLabs_cost s = true ↔
  as_costed (RTLabs_status ge) s.
cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
#ge * *
[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
  whd in match (as_pc_of ??);
  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
  % cases (lookup_present ?? (f_graph func) ??) normalize
  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
  try (% #E' destruct)
  cases (NONE ?) assumption
| #vf #fd #args #dst #fs #m #stk #mtc %
  [ #E normalize in E; destruct
  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
    #H cases (NONE H)
  ]
| #v #dst #fs #m #stk #mtc %
  [ #E normalize in E; destruct
  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
    #H cases (NONE H)
  ]
| #r #stk #mtc %
  [ #E normalize in E; destruct
  | #E normalize in E; cases (NONE E)
  ]
] qed.

lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
  RTLabs_cost s = false →
  ¬ as_costed (RTLabs_status ge) s.
#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
qed.

inductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
| ft_stop : ∀s. 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.

let rec make_flat_trace ge n s trace s' (EX:exec_steps n … RTLabs_fullexec ge s = return 〈trace,s'〉) on n : flat_trace io_out io_in ge s ≝
match n return λn. exec_steps n ????? = ? → ? with
[ O ⇒ λ_. ft_stop … s
| S m ⇒ λEX'.
  match eval_statement ge s return λx. eval_statement ?? = x → ? with
  [ Value ts ⇒ λEV. ft_step ??? s (\fst ts) (\snd ts) ? (make_flat_trace ge m (\snd ts) (tail … trace) s' ?)
  | _ ⇒ λEV. ⊥
  ] (refl ??)
] EX.
[ cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #_
  change with (eval_statement ??) in ST:(??%?); >EV in ST;
  #ST destruct
| //
| cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #STEPS
  change with (eval_statement ??) in ST:(??%?); >EV in ST;
  #ST destruct
  @STEPS
| cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #_
  change with (eval_statement ??) in ST:(??%?); >EV in ST;
  #ST destruct
] qed.

lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
  ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.
  Σs1. ∃ST,EX'. make_flat_trace ge (S n) s (hd::trace) s' EX = ft_step ??? s (\snd hd) s1 ST (make_flat_trace ge n s1 trace s' EX').
#ge #n #s #hd #trace #s' #EX
lapply (refl ? (eval_statement ge s))
cases (eval_statement ge s) in ⊢ (???% → ?);
[ #o #k | 3: #m ]
[ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct
  change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
] * #tr #s1 #EV
%{s1}
cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
change with (eval_statement ??) in ⊢ (??%? → ?); >EV in ⊢ (% → ?); #E destruct #EX'
%{EV} %{EX'}
whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
>EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
#ST' whd in ⊢ (??%?); %
qed.

let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝
match t with
[ ft_stop _ ⇒ 0
| ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t')
].


(* [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_lower : ∀ge,d,s,t.
  will_return ge d s t →
  ∀d'. d' ≤ d →
  will_return ge d' s t.
#ge #d0 #s0 #t0 #TM elim TM
[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
  [ #LE @wr_base //
  | #d' #LE %3 // @IH /2/
  ]
| #s #tr #s' #EX #tr #CL *
  [ #_ @wr_base //
  | #d' #LE @⊥ /2/
  ]
] 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_preserves … 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 #vf * #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 #vf #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 #N * #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 ∧ 
  (∃r,l1,l2. next_instruction f = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
*
[ #f #fs #m #E
  %{f} %{fs} %{m} %
  [ @refl
  | whd in E:(??%?); cases (next_instruction f) in E ⊢ %;
    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
    (*[ %1*) %{A} %{B} %{C} @refl
(*    | %2 %{A} %{B} @refl
    ]*)
  ]
| normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 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_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
  lapply (Hbody (next fr) (next_ok fr))
  generalize in ⊢ (?(???%) → ?);
  change with (next_instruction fr) in match (lookup_present ?????);
  >Estmt #LP' #WS
  cases (andb_Prop_true … WS) #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_res_value #a cases a [ | #sz #i | #f | | #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 →
  ∃vf,fd,args,dst,stk,m. s = Callstate vf fd args dst stk m.
* [ #f #fs #m whd in ⊢ (??%? → ?);
    cases (next_instruction f) normalize
    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
  | #vf #fd #args #dst #stk #m #E %{vf} %{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)
#vf * #fd * #args * #dst * #stk * #m #E >E in EV WCL;
whd in ⊢ (??%? → % → ?);
cases fd
[ #fn whd in ⊢ (??%? → % → ?);
  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) (*XData*))
  #m' #b whd in ⊢ (??%? → ?); #E' destruct
  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
  @WCL2
| #fn whd in ⊢ (??%? → % → ?);
  @bindIO_value #evargs #Eargs
  whd in ⊢ (??%? → ?);
  #E' destruct
] qed.


(* Extend our information about steps to states extended with the shadow stack. *)

inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (State f' fs m') S M')
| xto_call : ∀ge,f,fs,m,vf,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f'::fs) m) (fn::S) M')
| xfrom_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate vf (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m') S M')
| xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_ext_state ge (State f' fs m) S M')
| xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M')
.

lemma eval_preserves_ext : ∀ge,s,s'.
  as_execute (RTLabs_status ge) s s' →
  state_rel_ext ge s s'.
#ge0 * #s #S #M * #s' #S' #M' * #tr * #EX
generalize in match M'; -M'
generalize in match M; -M
generalize in match EX;
inversion (eval_preserves … EX)
[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %1 //
| #ge #f #fs #m #vf #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %2 //
| #ge #vf #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %3
| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
  cases S [ #EX' * ] #fn #S
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %4
| #ge #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %5 //
| #ge #r #dst #m #E1 #E2 #E3 #E4 destruct
  cases S [ 2: #h #t #EX' * ]
  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
  %6
] 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.
   
   We also show preservation of the shadow stack of function pointers.  As with
   the real stack, we ignore the current function.
 *)

inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M)
| sos_Callstate : ∀vf,fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f::fs) m) (fn::fn'::S) M)
| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m) S M)
.

inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
| sp_normal : ∀fs,S,s1,s2.
    stack_of_state ge fs S s1 →
    stack_of_state ge fs S s2 →
    stack_preserved ge doesnt_end_with_ret s1 s2
| sp_finished : ∀s1,f,f',fs,m,fn,S,M.
    next f = next f' →
    frame_rel f f' →
    stack_of_state ge (f::fs) (fn::S) s1 →
    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M)
| sp_stop : ∀s1,r,M.
    stack_of_state ge [ ] [ ] s1 →
    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
| sp_top : ∀vf,fd,args,dst,m,r,fn,M1,M2.
    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate vf fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
.

discriminator list.

lemma stack_of_state_eq : ∀ge,fs,fs',S,S',s.
  stack_of_state ge fs S s →
  stack_of_state ge fs' S' s →
  fs = fs' ∧ S = S'.
#ge #fs0 #fs0' #S0 #S0' #s0 *
[ #f #fs #m #fn #S #M #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
| #vf #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o try #p destruct /2/
| #rtv #dst #fs #m #S #M #H inversion H
  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
] qed.

lemma stack_preserved_final : ∀ge,e,r,S,M,s.
  ¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s.
#ge #e #r #S #M #s % #H inversion H
[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
  inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m try #o destruct
| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m try #p destruct
| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o try #p destruct
| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
] qed.

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

(* Proof that steps preserve the stack.  For calls we show that a stack
   preservation proof for the called function gives us enough to show
   stack preservation for the caller between the call and the state after
   returning. *)

lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl.
  RTLabs_classify s1 = cl →
  as_execute (RTLabs_status ge) s1 s2 →
  match cl with
  [ cl_call ⇒ ∀s3. stack_preserved ge ends_with_ret s2 s3 →
                   stack_preserved ge doesnt_end_with_ret s1 s3
  | cl_return ⇒ stack_preserved ge ends_with_ret s1 s2
  | _ ⇒ stack_preserved ge doesnt_end_with_ret s1 s2
  ].
#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
| #ge #f #fs #m #vf #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
| #ge #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
  * #s3 #S3 #M3 #SP inversion SP
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
  | #s1 #f #f' #fs' #m3 #fn3 #S3' #M3' #E1 #E2 #SOS #E4 #E5 #E6 #E7 destruct
    @(sp_normal … fs' S3') //
    inversion SOS
    [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct //
    | #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
    | #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
    ]
  | #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
    cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 try #H108 destruct /3/ ]
    * #fn * #E1 #E2 destruct
    @sp_top
  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
  ] 
| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
  whd in match (RTLabs_classify ?); cases (next_instruction f) /2/
| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
  cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
| #ge #r #dst #m #M #M' #E1 #E2 #E3 #E4 destruct whd /2/
] qed.

lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr.
  ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
  as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
#ge #s1 #s2 #tr #EV %{tr} %{EV} %
qed.

lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
  ∀CL : RTLabs_classify s1 = cl_call.
  as_execute (RTLabs_status ge) s1 s2 →
  stack_preserved ge ends_with_ret s2 s3 →
  as_after_return (RTLabs_status ge) «s1,CL» s3.
#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
cases (rtlabs_call_inv … CL) #vf * #fn * #args * #dst * #stk * #m #E destruct
whd
inversion S23
[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
  inversion (eval_preserves_ext … EV)
  [ 3: #gex #vfx #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
    inversion S
    [ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N | inversion F // ] | whd % ]
    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 destruct
    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
    ]
  | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
  ]
| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
  inversion (eval_preserves_ext … EV)
  [ 3: #ge' #vf' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
    inversion S1
    [ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
    | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 try #H123 destruct
    ]
  | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
  ]
| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
] qed.

(* Measure the number of steps in the structured trace so that we know it's the
   same execution that we started with.  TODO: move  *)
let rec length_tlr (S:abstract_status) s1 s2 (tlr:trace_label_return S s1 s2) on tlr : nat ≝
match tlr with
[ tlr_base _ _ tll ⇒ length_tll … tll
| tlr_step _ _ _ tll tlr' ⇒ length_tll … tll + length_tlr … tlr'
]
and length_tll (S:abstract_status) e s1 s2 (tll:trace_label_label S e s1 s2) on tll : nat ≝
match tll with
[ tll_base _ _ _ tal _ ⇒ length_tal … tal
]
and length_tal (AS:abstract_status) e s1 s2 (tal:trace_any_label AS e s1 s2) on tal : nat ≝ 
match tal with
[ tal_base_not_return _ _ _ _ _ ⇒ 1
| tal_base_return _ _ _ _ ⇒ 1
| tal_base_call _ _ _ _ _ _ tlr _ ⇒ S (length_tlr … tlr)
| tal_base_tailcall _ _ _ _ _ tlr ⇒ S (length_tlr … tlr)
| tal_step_call _ _ _ _ _ _ _ _ tlr _ tal' ⇒ S (length_tlr … tlr + length_tal … tal')
| tal_step_default _ _ _ _ _ tal' _ _ ⇒ S (length_tal … tal')
].



(* 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:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
  (original_terminates: will_return ge depth start full)
  (T:RTLabs_ext_state ge → Type[0]) (length:∀s. T s → nat) (limit:nat) : Type[0] ≝
{
  new_state : RTLabs_ext_state ge;
  remainder : flat_trace io_out io_in ge new_state;
  cost_labelled : well_cost_labelled_state new_state;
  new_trace : T new_state;
  tr_length : plus (length … new_trace) (length_flat_trace … remainder) = length_flat_trace … full;
  stack_ok : stack_preserved ge 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.
                         gt 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:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
  (original_terminates: will_return ge depth start full)
  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0])
  (length:∀e,s. T e s → nat)
  (limit:nat) : Type[0] ≝
{
  ends : trace_ends_with_ret;
  trace_res :> trace_result ge depth ends start full original_terminates (T ends) (length 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:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
  ∀r:trace_result ge d e s1 t1 TM1 T1 ln1 l1.
    will_return_end … TM1 = will_return_end … TM2 →
    ∀trace:T2 (new_state … r).
    ln2 (new_state … r) trace + length_flat_trace … (remainder … r) = length_flat_trace … t2 →
    stack_preserved ge e s2 (new_state … r) →
    trace_result ge d e s2 t2 TM2 T2 ln2 l2 ≝
λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
  mk_trace_result ge d e s2 t2 TM2 T2 ln2 l2
    (new_state … r)
    (remainder … r)
    (cost_labelled … r)
    trace
    LN
    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 #LN1 #SP whd in ⊢ (% → %); #TMS @TMS
  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
    %{TMa} % // @(transitive_le … lGE) @L1
  ]
| <TME -TME * #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %);
   * #TMa * #L1 #TME
    %{TMa} % // @(transitive_le … lGE) @L1
] qed.

definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
  ∀r:sub_trace_result ge d s1 t1 TM1 T1 ln1 l1.
    will_return_end … TM1 = will_return_end … TM2 →
    ∀trace:T2 (ends … r) (new_state … r).
    ? (*XXX matita infers this, but won't check it ?! *) + length_flat_trace … (remainder … r) = length_flat_trace ???? t2 →
    stack_preserved ge (ends … r) s2 (new_state … r) →
    sub_trace_result ge d s2 t2 TM2 T2 ln2 l2 ≝ 
λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
  mk_sub_trace_result ge d s2 t2 TM2 T2 ln2 l2
    (ends … r)
    (replace_trace … lGE … r TME trace LN SP).

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

lemma crappyhack : ∀tlr,rem1,tr,tal,rem2:nat.
  tlr+rem1 = tr → tal + rem2 = rem1 → S (tlr + tal) + rem2 = S tr.
#tlr #rem1 #tr #tal #rem2 #E1 #E2 destruct <associative_plus %
qed.

let rec make_label_return ge depth (s:RTLabs_ext_state ge)
  (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)
              (length_tlr (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) (length_tll (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:RTLabs_ext_state ge)
  (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)
              (λends. length_tll (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) ?) ? (stack_ok … r)

] TERMINATES_IN_TIME


and make_any_label ge depth (s0:RTLabs_ext_state ge)
  (trace: flat_trace io_out io_in ge s0)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s0)  (* functions in the state *)
  (TERMINATES: will_return ge depth s0 trace)
  (TIME: nat)
  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
  on TIME : sub_trace_result ge depth s0 trace TERMINATES
              (λends. trace_any_label (RTLabs_status ge) ends s0)
              (λends. length_tal (RTLabs_status ge) ends s0)
              (will_return_length … TERMINATES) ≝

match TIME return λTIME. TIME ≥ ? → ? with
[ O ⇒ λTERMINATES_IN_TIME. ⊥
| S TIME ⇒ λTERMINATES_IN_TIME. 
  match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
                                      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) (λends. length_tal (RTLabs_status ge) ends s) (will_return_length … TM)
  with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
                               well_cost_labelled_state s →
                               ∀TM:will_return ??? trace.
                               myge ? (times 3 (will_return_length ??? trace TM)) →
                               sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (λends. length_tal (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
  [ ft_stop st ⇒
      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥

  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    let next' ≝ next_state ? start' ?? EV in
    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (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 ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (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') (λends. length_tal (RTLabs_status ge) ends start') ?
              doesnt_end_with_ret
              (mk_trace_result ge … next' trace' ?
                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge 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 ? next' CS)) ??
        ] (refl ??)
        
    | cl_jump ⇒ λCL.
        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (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 … 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 ?) (λends. length_tal (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') (λends. length_tal (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) ((proj1 … (RTLabs_costed …)) … 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. length_tal (RTLabs_status ge) ends start') ?
          ends_with_ret
          (mk_trace_result ge ????????
            next'
            trace'
            ?
            (tal_base_return (RTLabs_status ge) start' next' ? CL)
            ?
            ?
            ?)
    | cl_tailcall ⇒ λCL. ⊥
    ] (refl ? (RTLabs_classify start))
    
  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
] TERMINATES_IN_TIME.

[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
| //
| //
| @(tr_length … r)
| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #GT #_ @(le_S_to_le … GT)
| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #_ #EEQ //
| <(tr_length … r) <(tr_length … r') @associative_plus
| @(stack_preserved_join … (stack_ok … r)) //
| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #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
| //
| @(proj1 … (RTLabs_costed …)) //
| @(tr_length … r)
| @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)
| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
| %
| %{tr} %{EV} @refl
| @(well_cost_labelled_state_step  … EV) //
| whd @(will_return_notfn … TERMINATES) %2 @CL
| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
| %
| %{tr} %{EV} %
| %1 whd @CL
| @(proj1 … (RTLabs_costed …)) @(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_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
| whd in ⊢ (???%); <(tr_length … r) %
| %{tr} %{EV} %
| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
| @(cost_labelled … r)
| skip
| cases r #ns #rm #WS #TLR #SP #LN * #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 #LN * #TM * #_ #EQ <EQ
  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
| %{tr} %{EV} %
| @(crappyhack ????? (tr_length … r) (tr_length … r'))
| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
| @(cost_labelled … r)
| cases r #H72 #H73 #H74 #H75 #HX #LN * #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) //
| skip
| 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)
| @(RTLabs_notail … CL)
| whd @(will_return_notfn … TERMINATES) %1 @CL
| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
| %
| %{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 @sym_eq @EQ
| @CL
| %{tr} %{EV} %
| whd in ⊢ (??%%); @eq_f @(tr_length … r)
| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
| @(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)
  //
] 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:RTLabs_ext_state ge)
  (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) (length_tlr (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.
 *)



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

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 ∧ successors (next_instruction f) = [ ]) ∨
  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (next_instruction f)).
#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
whd in ⊢ (??%? → ?);
generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_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_res_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_res_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_res_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_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #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_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 % %
] qed.

(* Establish a link between the number of instructions until the next cost
   label and the number of states. *)


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,H.
    ¬ is_cost_label (lookup_present … g l H) →
    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).

let rec bound_on_steps_succ g l n (H:bound_on_steps_to_cost g l n) on H
 : bound_on_steps_to_cost g l (S n) ≝
match H with
[ bostc_here l n Pr Cs ⇒ ?
| bostc_later l n H' CS B ⇒ ?
] and bound_on_steps1_succ g l n (H:bound_on_steps_to_cost1 g l n) on H
: bound_on_steps_to_cost1 g l (S n) ≝ 
match H with
[ bostc_step l n Pr Sc ⇒ ?
].
[ %1 //
| %2 /2/
| >plus_n_Sm % /3/
] qed.

let rec bound_on_steps_stmt g l n P (H:bound_on_steps_to_cost1 g l (plus (steps_for_statement (lookup_present … g l P)) n))
: bound_on_steps_to_cost1 g l (S (S n)) ≝ ?.
cases (lookup_present ? statement ???) in H; /2/
qed.

let rec bound_on_instrs_to_steps g l n
  (B:bound_on_instrs_to_cost g l n)
on B : bound_on_steps_to_cost1 g l (times n 2) ≝ ?
and bound_on_instrs_to_steps' g l n
  (B:bound_on_instrs_to_cost' g l n)
on B : bound_on_steps_to_cost g l (times n 2) ≝ ?.
[ cases B #l' #n' #H #EX @bound_on_steps_stmt [ @H | % #l'' #SC @bound_on_instrs_to_steps' @EX @SC ]
| cases B
  [ #l' #n' #H #CS %1 //
  | #l' #n' #H #CS #B' %2 [ @H | @CS | @bound_on_instrs_to_steps @B' ]
  ]
] qed.


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 : ∀vf,fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate vf 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 (next_instruction 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 (next_instruction ?)
[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_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_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #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_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
] qed.

lemma bound_after_call : ∀ge.∀s,s':RTLabs_ext_state ge.∀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 #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL -CL inversion H
[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
  #vf * #fn * #args * #dst * #stk * #m' @jmeq_hackT #E destruct
| #vf #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
  whd in S; #CL cases s'
  [ #f' #fs' #m' * * #N #F #STK #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 #H #CS' #B #E1 #E2 #_ destruct <N <F @B
    ]
  | #vf' #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_preserves … 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 #H77 #H78 destruct @H75
      ]
    | #ge0 #f0 #fs' #m0 #vf #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_preserves … 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' #N #F #E1 #E2 #E3 #_ destruct
    %1 whd in FS ⊢ %;
    <N
    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' m')) in CSx:(?%);
        >NC in CSx; *
    | #lx #nx #P #CS #H #E1x #E2x #_ destruct @H
    ]
  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
  ]
] qed.




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

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

lemma steps_from_sound : ∀s.
  RTLabs_cost s = true →
  soundly_labelled_state s →
  ∃n. state_bound_on_steps_to_cost s n.
* [ #f #fs #m #CS | #a #b #c #d #e #f #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
whd in ⊢ (% → ?); * #SLF #_
cases (SLF (next f) (next_ok f)) #n #B1
% [2: % /2/ | skip ]
qed.

lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
  soundly_labelled_ge ge →
  eval_statement ge s = Value ??? 〈tr,s'〉 →
  soundly_labelled_state s →
  soundly_labelled_state s'.
#ge #s #tr #s' #ENV #EV #S
inversion (eval_preserves … EV)
[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct 
  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
| #ge' #f #fs #m #vf #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct 
  whd in S ⊢ %; %
  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
  ]
| #ge' #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
  whd in S ⊢ %; @S
| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct 
  whd in S ⊢ %; cases S //
| #ge' #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
] qed.

lemma soundly_labelled_state_preserved : ∀ge,s,s'.
  stack_preserved ge ends_with_ret s s' →
  soundly_labelled_state s →
  soundly_labelled_state s'.
#ge #s0 #s0' #SP inversion SP
[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
| #s1 #f #f' #fs #m #fn #S #M #N #F #S1 #E1 #E2 #E3 #E4 destruct
  inversion S1
  [ #f1 #fs1 #m1 #fn1 #S1 #M1 #E1 #E2 #E3 #E4 destruct
    * #_ #S whd in S;
    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 
    destruct @S
  | #vf #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 
    destruct @S
  | #rtv #dst #fs1 #m1 #S1 #M1 #E1 #E2 #E3 #E4 destruct #S
    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 
    destruct @S
  ]
| //
| //
] qed.

lemma simplify_cl : ∀ge,s,c.
  as_classifier (RTLabs_status ge) s c →
  RTLabs_classify (Ras_state … s) = c.
#ge * #s #S #M #c #CL
whd in CL; whd in CL:(??%?);
destruct //
qed.
(*
(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
       a trace_label_diverges value, but I only know how to construct those
       using a cofixpoint in Type[0], which means I can't use the termination
       oracle.
*)

let corec make_label_diverges ge (s:RTLabs_ext_state ge)
  (trace: flat_trace io_out io_in ge s)
  (ORACLE: termination_oracle)
  (TRACE_OK: remainder_ok ge s trace)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
  : trace_label_diverges_exists (RTLabs_status ge) s ≝
match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
[ ex_intro n B ⇒
    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
      return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    with
    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
            tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
(*
        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
        [ ex_intro T' _ ⇒
            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
        ]*)
    | fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
            tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
(*
        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
        [ ex_intro T' _ ⇒
            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
        ]*)
    ] STATEMENT_COSTLABEL
].
[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
| @EV
| cases (trace_any_call_call … T) // #CL cases (RTLabs_notail' … CL)
| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') //
  cases (trace_any_call_call … T) #CL
  [ @simplify_cl @CL
  | @⊥ @(RTLabs_notail' … CL)
  ]
] qed.

lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge.
  as_execute (RTLabs_status ge) s1 s2 →
  make_initial_state p = OK ? s1 →
  stack_preserved ge ends_with_ret s2 s' →
  RTLabs_is_final s' ≠ None ?.
#ge #p * #s1 #S1 #M1 * #s2 #S2 #M2 * #s' #S' #M' #EV whd in ⊢ (??%? → ?);
@bind_ok #m #_
@bind_ok #b #_
@bind_ok #f #_
#E destruct
#SP inversion (eval_preserves_ext … EV)
[ 3: #ge' #vf #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
     inversion SP
     [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥
          inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 try #H75 destruct
     ]
| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 try #H113 destruct
] qed.

lemma initial_state_is_call : ∀p,s.
  make_initial_state p = OK ? s →
  RTLabs_classify s = cl_call.
#p #s whd in ⊢ (??%? → ?);
@bind_ok #m #_
@bind_ok #b #_
@bind_ok #f #_
#E destruct
@refl
qed.

let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge)
  (ORACLE: termination_oracle)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
  : ∀trace: flat_trace io_out io_in ge s.
    ∀INITIAL: make_initial_state p = OK state s.
    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
    trace_whole_program_exists (RTLabs_status ge) s ≝ 
match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
                   make_initial_state p = OK ? s →
                   well_cost_labelled_state s →
                   soundly_labelled_state s →
                   trace_whole_program_exists (RTLabs_status ge) s with
[ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace. 
match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
                             make_initial_state p = OK state s →
                             well_cost_labelled_state s →
                             soundly_labelled_state s →
                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with
[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
    let IS_CALL ≝ initial_state_is_call … INITIAL in
    let s' ≝ mk_RTLabs_ext_state ge s stk mtc in
    let next' ≝ next_state ge s' next tr EV in
    match ORACLE ge O next trace' with
    [ or_introl TERMINATES ⇒
        match TERMINATES with
        [ witness TERMINATES ⇒
          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in 
          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (IS_CALL) ? (new_trace … tlr) ?
        ]
    | or_intror NO_TERMINATION ⇒ 
        twp_diverges (RTLabs_status ge) s' next' (IS_CALL) ?
         (make_label_diverges ge next' trace' ORACLE ?
            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
    ]
| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
] mtc0 ].
[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #vf * #fn * #args * #dst * #stk * #m #E destruct
  cases FINAL #E @E @refl
| %{tr} %{EV} %
| @(after_the_initial_call_is_the_final_state … p s' next')
  [ %{tr} %{EV} % | @INITIAL | @(stack_ok … tlr) ]
| @(well_cost_labelled_state_step … EV) //
| @(well_cost_labelled_call … EV) //
| %{tr} %{EV} %
| @(well_cost_labelled_call … EV) //
| % [ @(well_cost_labelled_state_step … EV) //
    | @(soundly_labelled_state_step … EV) //
    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
    ]
] qed.
*)
lemma init_state_is : ∀p,s.
  make_initial_state p = OK ? s →
  𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒
       fs = [ ] ∧
       fid = prog_main … p ∧
       find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧
       find_funct_ptr ? (make_global p) b = Some ? fd
   | _ ⇒ False ].
#p #s
@bind_ok #m #Em
@bind_ok #b #Eb
@bind_ok #f #Ef
#E whd in E:(??%%); destruct
%{b} whd
% [% [%] ] // [ @Eb | @Ef ]
qed.

definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
cases (init_state_is p s I) #b
cases s
[ #f #fs #m *
| #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/
| #rv #rr #fs #m *
| #r *
] qed.

lemma well_cost_labelled_initial : ∀p,s.
  make_initial_state p = OK ? s →
  well_cost_labelled_program p →
  well_cost_labelled_state s ∧ soundly_labelled_state s.
#p #s
@bind_ok #m #Em
@bind_ok #b #Eb
@bind_ok #f #Ef
#E destruct
whd in ⊢ (% → %);
#WCL
@(find_funct_ptr_All ??????? Ef)
@(All_mp … WCL)
* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
qed.

lemma well_cost_labelled_make_global : ∀p.
  well_cost_labelled_program p →
  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
#p whd in ⊢ (% → ?%%);
#WCL %
#b #f #FFP
[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
] @(All_mp … WCL)
* #id * #fn // * /2/
qed.
(*
theorem program_trace_exists :
  termination_oracle →
  ∀p:RTLabs_program.
  well_cost_labelled_program p →
  ∀s:state.
  ∀I: make_initial_state p = OK ? s.
  
  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
  
  ∀NOIO:exec_no_io … plain_trace.
  ∀NW:not_wrong … plain_trace.
  
  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
  
  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).

#ORACLE #p #WCL #s #I
letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
#NOIO #NW
letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
whd 
@(whole_structured_trace_exists (make_global p) p ? ORACLE)
[ @(proj1 … (well_cost_labelled_make_global … WCL))
| @(proj2 … (well_cost_labelled_make_global … WCL))
| @flat_trace
| @I
| @(proj1 ?? (well_cost_labelled_initial … I WCL))
| @(proj2 ?? (well_cost_labelled_initial … I WCL))
] qed.
*)

lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
  as_execute (RTLabs_status ge) s s' →
  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
#ge #s #s' * #tr * #EX #_ %{tr} @EX
qed.

(* as_execute might be in Prop, but because the semantics is deterministic
   we can retrieve the event trace anyway. *)

let rec deprop_execute ge (s,s':state)
  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
[ Value ts ⇒ λY. «fst … ts, ?»
| _ ⇒ λY. ⊥
] X.
[ 1,3: cases Y #x #E destruct
| cases Y #trP #E destruct @refl
] qed.

let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
  (X:as_execute (RTLabs_status ge) s s')
: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
deprop_execute ge s s' ?.
cases X #tr * #EX #_ %{tr} @EX
qed.

(* A non-empty finite section of a flat_trace *)
inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
| pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''.

let rec append_partial_flat_trace o i ge s1 s2 s3
  (tr1:partial_flat_trace o i ge s1 s2)
on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
match tr1 with
[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
].

let rec partial_to_flat_trace o i ge s1 s2
  (tr:partial_flat_trace o i ge s1 s2)
on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
match tr with
[ pft_base s tr s' EX ⇒ ft_step … EX
| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
].

(* Extract a flat trace from a structured one. *)
let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
  (tr:trace_label_return (RTLabs_status ge) s s')
on tr :
  partial_flat_trace io_out io_in ge s s' ≝
match tr with
[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
| tlr_step s1 s2 s3 tll tlr ⇒
  append_partial_flat_trace …
    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
    (flat_trace_of_label_return ge s2 s3 tlr)
]
and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
  (tr:trace_label_label (RTLabs_status ge) ends s s')
on tr :
  partial_flat_trace io_out io_in ge s s' ≝ 
match tr with
[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
]
and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
  (tr:trace_any_label (RTLabs_status ge) ends s s')
on tr :
  partial_flat_trace io_out io_in ge s s' ≝
match tr with
[ tal_base_not_return s1 s2 EX CL CS ⇒
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    pft_base … EX' ]
| tal_base_return s1 s2 EX CL ⇒ 
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    pft_base … EX' ]
| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    pft_step … EX' suffix' ]
| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    pft_step … EX'
      (append_partial_flat_trace …
        (flat_trace_of_label_return ge ?? tlr)
        (flat_trace_of_any_label ge ??? tal))
    ]
| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
    ]
| tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥
].
@(RTLabs_notail' … CL)
qed.

(* We take an extra step so that we can always return a non-empty trace to
   satisfy the guardedness condition in the cofixpoint. *)
let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
  (tr:trace_any_call (RTLabs_status ge) s s')
  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
on tr :
  partial_flat_trace io_out io_in ge s s'' ≝ 
match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒ 
    pft_step … EX'
      (append_partial_flat_trace …
        (flat_trace_of_label_return ge ?? tlr)
        (flat_trace_of_any_call ge … tac EX''))
    ]
| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    pft_step … EX'
     (flat_trace_of_any_call ge … tal EX'')
    ]
] EX''.

let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
  (tr:trace_label_call (RTLabs_status ge) s s')
  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
on tr :
  partial_flat_trace io_out io_in ge s s'' ≝
match tr with
[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
] EX''.




(* We still need to link tal_unrepeating to our definition of cost soundness. *)


(* Extract the "current" function from a state. *)
definition state_fn : ∀ge. RTLabs_status ge → option block ≝
λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
  match Ras_state … s with
  [ Callstate _ _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
  | _ ⇒  Some ? h ] ].

(* Some results to invert the classification of states *)

lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
  as_execute (RTLabs_status ge) s s' →
  RTLabs_classify s = cl →
  match cl with
  [ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
  | cl_return ⇒ ∀fn. P (rapc_ret fn)
  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
  | cl_tailcall ⇒ True
  ] → P (as_pc_of (RTLabs_status ge) s).
#ge #cl #P * *
[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
  cases (next_instruction f) normalize
  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
| #vf #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
| #r #S #M #s' * #tr * #EX normalize in EX; destruct
] qed.

definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL).

lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
  as_execute (RTLabs_status ge) s s' →
  RTLabs_classify s = cl →
  match cl with
  [ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
  | cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
  | cl_tailcall ⇒ False
  ] .
#ge * #s #s' #EX #CL whd
@(declassify_pc … EX CL) whd
[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | @I | #fn #l %{fn} %{l} % ]
qed.

lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
  as_execute (RTLabs_status ge) s s' →
  RTLabs_classify s = cl →
  match cl with
  [ cl_call ⇒ ∃vf,fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate vf fd args dst fs m) S M
  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
  ] .
#ge #cl * * [ #f #fs #m | #vf #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
#S #M * #s' #S' #M' #EX #CL
whd in CL:(??%?);
[ cut (cl = cl_other ∨ cl = cl_jump)
  [ cases (next_instruction f) in CL; 
    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
  * #E >E %{f} %{fs} %{m} %{S} %{M} %
| <CL %{vf} %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
] qed.

lemma State_not_callreturn : ∀f,fs,m,cl.
  RTLabs_classify (State f fs m) = cl →
  match cl with
  [ cl_return ⇒ False
  | cl_call ⇒ False
  | _ ⇒ True
  ].
#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
cases (next_instruction f) //
qed.

(* And some about traces *)

lemma tal_not_final : ∀ge,fl,s1,s2.
  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
  RTLabs_is_final (Ras_state … s1) = None ?.
#ge #flx #s1x #s2x *
[ #s1 #s2 * #tr * #EX #NX #CL #CS
| #s1 #s2 * #tr * #EX #NX #CL
| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
] @(step_not_final … EX)
qed.

(* invert traces ending in a return *)

lemma tal_return : ∀ge,fl,s1,s2.
  as_classifier (RTLabs_status ge) s1 cl_return →
  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
  %{EX} %{CL} % %
| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
  whd in CL CL'; >CL in CL'; #E destruct
| #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL')
| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
  whd in CL CL'; >CL in CL'; #E destruct
| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
  whd in CL CL'; >CL in CL'; #E destruct
] qed.


(* We need to link the pcs, states of the semantics with the labels and graphs
   of the syntax. *)

inductive pc_label : RTLabs_pc → label → Prop ≝
| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.

discriminator option.

lemma pc_label_eq : ∀pc,l1,l2.
  pc_label pc l1 →
  pc_label pc l2 →
  l1 = l2.
#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
qed.

lemma pc_label_call_eq : ∀l,fn,l'.
  pc_label (rapc_call (Some ? l) fn) l' →
  l = l'.
#l #fn #l' #PC inversion PC
#a #b #E1 #E2 #E3 destruct
%
qed.

inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
| gf : ∀b,fn.
    find_funct_ptr … ge b = Some ? (Internal ? fn) →
    graph_fn ge (Some ? b) (f_graph … fn).

lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
  graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
  g = f_graph (func f).
#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
inversion G
#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
%
qed.

lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
  let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
  actual_successor s' = Some ? l →
  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
| #ge' #f' #f'' #m' #vf #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
  >H33 in AS; normalize #AS destruct
| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
] qed.

lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
  as_after_return (RTLabs_status ge) «pre,CL» post →
  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
  match ret with
  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
  | Some retl ⇒
    state_fn … pre = state_fn … post ∧
    pc_label (as_pc_of (RTLabs_status ge) post) retl
  ].
#ge #pre #post #CL #ret #callee #AF 
cases pre in CL AF ⊢ %;
* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??%?);
    cases (next_instruction f) in CL;
    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
  | #vf #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
  | #r #S #M #CL normalize in CL; destruct
  ]
cases post
* [ #postf #postfs #postm * [*] #fn' #S' #M'
  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
  | 2,6: #A #B #C #D #E #F #G #H *
  | 3,7: #A #B #C #D #E #F *
  | #r #S' #M' #AF whd in AF; destruct
  | #r #S' #M'
  ]
#AF #PC normalize in PC; destruct whd
[ cases AF * #A #B #C destruct % [ % | normalize >A // ]
| % #E normalize in E; destruct
] qed.

lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
  actual_successor s = Some ? l →
  pc_label (as_pc_of (RTLabs_status ge) s) l.
#ge * *
[ #f #fs #m * [*] #fn #S #M #l #AS
| #vf #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
| #ret #dst #fs #m #S #M #l #AS
| #r #S #M #l #AS
] whd in AS:(??%?); destruct //
qed.

include alias "utilities/deqsets_extra.ma".

(* Build the tail of the "bad" loop using the reappearance of the original pc,
   ignoring the rest of the trace_any_label once we see that pc. *)

let rec tal_pc_loop_tail ge flX s1X s2X
  (pc:as_pc (RTLabs_status ge)) g l
  (PC0:pc_label pc l)
  (tal: trace_any_label (RTLabs_status ge) flX s1X s2X)
on tal :
  ∀l1.
  pc_label (as_pc_of (RTLabs_status ge) s1X) l1 →
  graph_fn ge (state_fn … s1X) g →
  Not (as_costed (RTLabs_status ge) s1X) →
  pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal →
  bad_label_list g l l1 ≝ ?.
cases tal
[ #s1 #s2 #EX #CL #CS
  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
  >(pc_label_eq … PC0 PC1) %1
| #s1 #s2 #EX #CL
  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
  >(pc_label_eq … PC0 PC1) %1
| #pre #start #final #EX #CL #AF #tlr #CS
  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
  >(pc_label_eq … PC0 PC1) %1
| #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL)
| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
  | #NE #IN
    lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
    [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
      lapply (pc_label_call_eq … PC1) #E destruct
      @(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN)
    | @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct
    ]
  ]
| #fl #pre #init #end #EX #tal' #CL #CS
  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
  | #NE #IN
    cases (declassify_state … EX (simplify_cl … CL))
    #f * #fs * #m * #S * #M #E destruct
    cut (l1 = next f)
    [ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1
      inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct
    cases EX #tr * #EV #NX
    cases (eval_successor … EV)
    [ * #CL' @⊥ cases (tal_return … (CL') tal') #EX' * #CL'' * #E1 #E2 destruct
      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
    | * #l' * #AS #SC
      lapply (graph_fn_state … G) #E destruct
      @(gl_step … l')
      [ @(next_ok f)
      | @Exists_memb @SC
      | @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??))
        @ISL
      | @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS))
        [ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G
        | *: //
        ]
      ]
    ]
  ]
] qed.

(* Combine the above result with the result on bad loops in CostMisc.ma to show
   that the pc of a normal instruction execution state can't be repeated within
   a trace_any_label. *)

lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
  soundly_labelled_state s1 →
  RTLabs_classify s1 = cl_other →
  as_execute (RTLabs_status ge) s1 s2 →
  ¬ as_costed (RTLabs_status ge) s2 →
  ¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal.
#ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL)
#f * #fs * #m * * [* *] #fn #S * * #FFP #M #E destruct
cases EX #tr * #EV #NX
cases (eval_successor … EV)
[ * #CL2 #SC
  cases (tal_return … (CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
  @notb_Prop % whd in match (tal_pc_list ?????); #IN
  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
  #ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct
  normalize #E destruct
| * #l2 * #AS2 #SC1 @notb_Prop % #IN
  (* Two cases: either s1 is a cost label, and it's pc's appearence later on
     is impossible because nothing later in tal can be a cost label; or it
     isn't and we get a loop of successor instruction labels that breaks the
     soundness of the cost labelling. *)
  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
  [ * #H @H
    cases (memb_exists … IN) #left * #right #E
    @(All_split … (tal_tail_not_costed … tal CS2) … E)
  | (* Now show that the loop invalidates soundness. *)
    cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
    [ %1 ] #PC1
    cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
    [ /2/ ] #PC2
    lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN)
    [ <NX <(state_fn_next … EV AS2) % // ]
    cases S1 #SLF #_ cases (SLF (next f) (next_ok f))
    #bound1 #BOUND1 #BLL #CS1
    cases (bound_step1 … BOUND1 … SC1)
    #bound2 #BOUND2 @(absurd … BOUND2)
    @(loop_soundness_contradiction … BLL)
    [ @(next_ok f)
    | @SC1
    | @notb_Prop @(not_to_not … CS1) #CS
      @(proj1 … (RTLabs_costed …)) @CS
    ]
  ]
] qed.

(* We need a similar result for call states.  We'll do this by showing that
   the state following the call state is a normal instruction state and using
   the previous result. *)

lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
  state_fn … s1 = state_fn … s2 →
  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
#ge * #s1 #S1 #M1 #CL1
cases (rtlabs_call_inv … (simplify_cl … CL1)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
* #s2 #S2 #M2 #CL2
cases (rtlabs_call_inv … (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h #i * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h #i * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
whd in ⊢ (% → ?);
[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
    * * #N1 #F1 #STK1
    whd in STK1 ⊢ (% → ?);
    [ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [*] #fn2 * [* #X *] #fn2 #S2' #M2 * * #N2 #F2 #STK2
      normalize in ⊢ (% → % → ?); #E1 #E2
      cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1
      cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2
      whd in ⊢ (??%%); <N2 <N1 destruct >e1 %
    | #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?);
      #X destruct
    ]
| #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M *] #f2 #fs2' cases S2 [*] #fn2 #S2' #M2 * * #N2 #F2 #STK2
  cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1
  normalize in ⊢ (% → ?); #E destruct
| #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ %
] qed.

lemma eq_pc_eq_classify : ∀ge,s1,s2.
  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
  RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
#ge
* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #vf1 #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
* * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
whd in ⊢ (??%% → ?); #E destruct try %
[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
  change with (lookup_present … next2 nok1) in match (next_instruction ?);
  cases (lookup_present … next2 nok1)
  normalize //
| 2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct
| 4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct
] qed.

lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
  state_fn … s1 = state_fn … s2 →
  RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4).
#ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN
@eq_pc_eq_classify
@(pc_after_return_eq … AF1 AF2 PC FN)
qed.

lemma cost_labels_are_other : ∀ge,s.
  as_costed (RTLabs_status ge) s →
  RTLabs_classify (Ras_state … s) = cl_other.
#ge * * [ #f #fs #m #S #M | #vf #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
#CS lapply (proj2 … (RTLabs_costed …) … CS)
whd in ⊢ (??%? → %);
[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
| *: #E destruct
] qed.

lemma eq_pc_cost : ∀ge,s1,s2.
  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
  as_costed (RTLabs_status ge) s1 →
  as_costed (RTLabs_status ge) s2.
#ge
* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #vf1 #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 #S1 #M1 ]
[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
* * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2 | 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 * [2: #fn2 #S2] #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
whd in ⊢ (??%% → ?); #E destruct
#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
qed.

lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal.
  RTLabs_classify (Ras_state … s1) = cl_other →
  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal.
#ge #flX #s1X #s2X *
[ #s1 #s2 #EX *
  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
  | #CL #CS #CL' @eq_true_to_b @memb_hd
  ]
| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
] qed.

lemma state_fn_after_return : ∀ge,pre,post,CL.
  as_after_return (RTLabs_status ge) «pre,CL» post →
  state_fn … pre = state_fn … post.
#ge * #pre #preS #preM * #post #postS #postM #CL #AF
cases (rtlabs_call_inv … (simplify_cl … CL)) #vf * #fd * #args * #dst * #fs * #m #E destruct
cases post in postM AF ⊢ %;
[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
  cases preS in preM AF ⊢ %; [*]
  #fn *
  [ cases fs [ #M * ]
    #f #fs' * #FFP *
  | #fn' #S cases fs [ #M * ]
    #f #fs' #M * * #N #F #PC destruct %
  ]
| #A #B #C #D #E #F #G *
| #A #B #C #D #E *
| #r #M' #AF whd in AF; destruct
  cases preS in preM ⊢ %;
  [ // | #fn * [ // | #fn' #S * #FFP * ] ]
] qed.

lemma state_fn_other : ∀ge,s1,s2.
  RTLabs_classify (Ras_state … s1) = cl_other →
  as_execute (RTLabs_status ge) s1 s2 →
  RTLabs_classify (Ras_state … s2) = cl_return ∨
  state_fn … s1 = state_fn … s2.
#ge #s1 #s2 #CL #EX
cases (declassify_state … EX CL)
#f * #fs * #m * * [**] #fn #S * #M #E destruct
inversion (eval_preserves_ext … EX)
[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct %2 %
| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
| #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
] qed.

(* The main part of the proof is to walk down the trace_any_label and find the
   repeated call state, then show that its successor appears as well. *)

let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
  (AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2)
  (CL2:RTLabs_classify (Ras_state … s2) = cl_other)
  (CS2:Not (as_costed (RTLabs_status ge) s2))
  (EX1:as_execute (RTLabs_status ge) s1 s1') on tal :
  state_fn … s1 = state_fn … s3 →
  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal →
  as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?.
cases tal
[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
  whd in match (tal_pc_list ?????) in IN;
  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
  cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l
  #IN' destruct
| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
  @(declassify_pc_cl … EX2 CL2) whd #fn
  #IN' destruct
| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
  lapply (memb_single … IN) #E
  lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
  @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
| #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL)
| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
  whd in ⊢ (?% → ?); @eqb_elim
  [ #PC #_
    >(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list
    <(classify_after_return_eq … AF1 AF3 PC FN) assumption
  | #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons
    @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN)
    >FN @(state_fn_after_return … AF3)
  ]
| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
  lapply (simplify_cl … CL1) #CL1'
  lapply (simplify_cl … CL3) #CL3'
  @eq_true_to_b @memb_cons
  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
  [ >FN cases (state_fn_other … CL3' EX3)
    [ #CL3'' @⊥
      cases (tal_return … (CL3'') tal3')
      #EX3' * #CL3''' * #E1 #E2 destruct
      whd in IN:(?%); lapply IN @eqb_elim
      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct
      ]
    | //
    ]
  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
    | #NE #IN @IN
    ]
  ]
] qed.

(* Then we can start the proof by finding the original successor state... *)

lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
  as_execute (RTLabs_status ge) s1 s1' →
  as_after_return (RTLabs_status ge) «s1,CL» s2 →
  ¬as_costed (RTLabs_status ge) s2 →
  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal →
  ∃s3,EX,CL',CS,tal'.
    tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
    bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
#ge #s1 #s1' #CL #flX #s2X #s4X *
[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
  whd in match (tal_pc_list ?????) in IN;
  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
  cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l
  #IN' destruct
| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
  @(declassify_pc_cl … EX2 CL2) whd #fn
  #IN' destruct
| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
  cases AF1
| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
  cases AF1
| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
  lapply (simplify_cl … CL) #CL'
  lapply (simplify_cl … CL2) #CL2'
  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
  (* Now that we've inverted the first part of the trace, look for the repeat. *)
  @(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1)
  [ >(state_fn_after_return … AF1)
    cases (state_fn_other … CL2' EX2)
    [ #CL3 @⊥
      cases (tal_return … (CL3) tal3)
      #EX3 * #CL3' * #E1 #E2 destruct
      lapply (simplify_cl … CL3') #CL3''
      whd in IN:(?%); lapply IN @eqb_elim
      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct
      ]
    | //
    ]
  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
    | #NE #IN @IN
    ]
  ]
] qed.

(* And then we get our counterpart to no_loops_in_tal for calls: *)

lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
  ∀tal:trace_any_label (RTLabs_status ge) fl after final.
  as_execute (RTLabs_status ge) pre start →
  as_after_return (RTLabs_status ge) «pre,CL» after →
  ¬as_costed (RTLabs_status ge) after →
  soundly_labelled_state (Ras_state ge after) →
  ¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal.
#ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN
cases (pc_after_call_repeats … EX AF CS IN)
#s * #EX * #CL' * #CSx * #tal' * #E #IN'
@(absurd ? IN')
@Prop_notb
@no_loops_in_tal /2/
qed.

(* Show that if a state is soundly labelled, then so are the states following
   it in a trace. *)

lemma soundly_step : ∀ge,s1,s2.
  soundly_labelled_ge ge →
  as_execute (RTLabs_status ge) s1 s2 →
  soundly_labelled_state (Ras_state … s1) →
  soundly_labelled_state (Ras_state … s2).
#ge #s1 #s2 #GE * #tr * #EX #NX
@(soundly_labelled_state_step … GE … EX)
qed.

let rec tlr_sound ge s1 s2
  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
  (GE:soundly_labelled_ge ge)
on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝ 
match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with
[ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1
| tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in
                            tlr_sound … tlr' GE S2
]
and tll_sound ge fl s1 s2
  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
  (GE:soundly_labelled_ge ge)
on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝ 
match tll with
[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
]
and tal_sound ge fl s1 s2
  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
  (GE:soundly_labelled_ge ge)
on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
match tal with
[ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1
| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
].
@(RTLabs_notail' … CL)
qed.

(* And join everything up to show that soundly labelled states give unrepeating
   traces. *)

let rec tlr_sound_unrepeating ge
  (s1,s2:RTLabs_status ge)
  (GE:soundly_labelled_ge ge)
  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝ 
match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with
[ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1
| tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1))
]
and tll_sound_unrepeating ge fl
  (s1,s2:RTLabs_status ge)
  (GE:soundly_labelled_ge ge)
  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with
[ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal
]
and tal_sound_unrepeating ge fl
  (s1,s2:RTLabs_status ge)
  (GE:soundly_labelled_ge ge)
  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with
[ tal_base_not_return _ _ EX _ _ ⇒ λS1. I
| tal_base_return _ _ EX _ ⇒ λS1. I
| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
    tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
    conj ?? (conj ??? 
     (tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1))))
     (tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1))
| tal_step_default _ pre init end EX tal CL _ ⇒ λS1.
    conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
].
[ @(RTLabs_notail' … CL)
| @(no_repeats_of_calls … EX AF) [ assumption |
  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
| @no_loops_in_tal // @simplify_cl @CL
] qed.