(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "common/StructuredTraces.ma".

(* We work with two relations on states in parallel, as well as two derived ones.
   sem_rel is the classic semantic relation between states, keeping track of
   memory and how program counters are mapped between languages.
   call_rel keeps track of what pcs corresponding calls have and just that:
   this is different than corresponance between program counters in sem_rel when
   CALL f ↦ instr* CALL f instr* *)

record status_rel 
  (S1 : abstract_status)
  (S2 : abstract_status)
  : Type[1] ≝ 
  { sem_rel :2> S1 → S2 → Prop
  (* this is kept separate, as not necessarily carrier will
     synchronise on calls. It should state the minimal properties
     necessary for as_after_return (typically just the program counter)
     maybe what function is called too? *)
  ; call_rel : (Σs.as_classifier S1 s cl_call) →
               (Σs.as_classifier S2 s cl_call) → Prop
  }.

(* The two derived relations are
   label_rel which tells that the two states are colabelled
   ret_rel which tells that two return states are in relation: the idea is that
   it happens when "going back" through as_after_return on one side we get
   a pair of call_rel related states, then we enjoy as_after_return also on the
   other. Roughly call_rel will store just enough information so that we can
   advance locally on a return step and build structured traces any way *)

(* if we later generalise, we should move this inside status_rel *)
definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.

definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
  λs1_ret,s2_ret.
  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
                 call_rel ?? R s1_pre s2_pre →
                 as_after_return S2 s2_pre s2_ret.

(* the base property we ask for simulation to work depends on the status_class
   S will mark semantic relation, C call relation, L label relation, R return relation *)

record status_simulation
  (S1, S2 : abstract_status)
  (sim_status_rel : status_rel S1 S2) : Prop ≝
{ one_step_sim :5>
    ∀st1,st1',st2.as_execute S1 st1 st1' →
    sim_status_rel st1 st2 →
      match as_classify … st1 with
      [ cl_call ⇒ ∀prf.
        (* 
             st1' ------------S----------\
              ↑ \                         \
             st1 \--L--\                   \
              | \       \                   \
              S  \-C-\  st2_after_call →taa→ st2'
              |       \     ↑
             st2 →taa→ st2_pre_call
        *)
        ∃st2_pre_call.
        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
        ∃st2_after_call,st2'.
        ∃taa2 : trace_any_any … st2 st2_pre_call.
        ∃taa2' : trace_any_any … st2_after_call st2'.
        as_execute … st2_pre_call st2_after_call ∧
        sim_status_rel st1' st2' ∧
        label_rel … st1' st2_after_call
      | cl_tailcall ⇒ ∀prf.
        (* 
             st1' ------------S----------\
              ↑ \                         \
             st1 \--L--\                   \
              |         \                   \
              S         st2_after_call →taa→ st2'
              |             ↑
             st2 →taa→ st2_pre_call
        *)
        ∃st2_pre_call.
        as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
        ∃st2_after_call,st2'.
        ∃taa2 : trace_any_any … st2 st2_pre_call.
        ∃taa2' : trace_any_any … st2_after_call st2'.
        as_execute … st2_pre_call st2_after_call ∧
        sim_status_rel st1' st2' ∧
        label_rel … st1' st2_after_call
      | cl_return ⇒
        (* 
             st1
            / ↓
           | st1'----------S,L------------\
           S   \                           \
            \   \-----R-------\            |      
             \                 |           |
             st2 →taa→ st2_ret |           |
                          ↓   /            |
                     st2_after_ret →taaf→ st2'

           we also ask that st2_after_ret be not labelled if the taaf tail is
           not empty
        *)
        ∃st2_ret,st2_after_ret,st2'.
        ∃taa2 : trace_any_any … st2 st2_ret.
        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
        as_classifier … st2_ret cl_return ∧
        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
        ret_rel … sim_status_rel st1' st2_after_ret ∧
        label_rel … st1' st2'
      | cl_other ⇒
          (*          
          st1 → st1'
            |      \
            S      S,L
            |        \
           st2 →taaf→ st2'
           
           the taaf can be empty (e.g. tunneling) but we ask it must not be the
           case when both st1 and st1' are labelled (we would be able to collapse
           labels otherwise)
         *)
        ∃st2'.
        ∃taa2 : trace_any_any_free … st2 st2'.
        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
        sim_status_rel st1' st2' ∧
        label_rel … st1' st2'
      | cl_jump ⇒
        (* just like cl_other, but with a hypothesis more *)
        as_costed … st1' →
        ∃st2'.
        ∃taa2 : trace_any_any_free … st2 st2'.
        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
        sim_status_rel st1' st2' ∧
        label_rel … st1' st2'
    ]
; sim_final :
  ∀st1,st2,res.as_result S1 st1 = Some ? res → sim_status_rel st1 st2 →
  as_result S2 st2 = Some ? res
}.

record status_simulation_with_init (S1,S2 : abstract_status)
  (R : status_rel S1 S2)
  (init1 : S1) (init2 : S2) : Prop ≝
{ sim_init : R init1 init2
; sim_init_labels : label_rel … init1 init2
; sim_step_final :> status_simulation S1 S2 R
}.

(* some useful lemmas *)

let rec taa_append_tal_rel S1 fl1 st1 st1'
  (tal1 : trace_any_label S1 fl1 st1 st1')
  S2 st2 st2mid fl2 st2'
  (taa2 : trace_any_any S2 st2 st2mid)
  (tal2 : trace_any_label S2 fl2 st2mid st2')
  on tal1 :
  tal_rel … tal1 tal2 →
  tal_rel … tal1 (taa2 @ tal2) ≝
match tal1 return λfl1,st1,st1',tal1.? with
  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
  | tal_base_return st1 st1' _ _ ⇒ ?
  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
  ].
[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ 
| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
  ]
| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
  ]
| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
]
destruct
<associative_taa_append_tal
  [1,2,3,4,5:%{(refl …)}] %{st2mid}
  [1,2:|*: %{G2} %{EQcall} ]
  %{(taa_append_taa … taa2 taa2')}
  [1,2: %{H2} %{G2} [%{K2}] %
  |5: %{st2mid'} %{H2} %{tlr2} % //
  |*: %{st2mid'} %{H2}
    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
  ]
qed.

(*
check trace_any_label_label
let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
  on tal : as_costed … st2 ≝
  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
  | tal_base_return _ _ _ _ ⇒ λprf.⊥
  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
  ] (refl …).
[ destruct
|*: >prf %
]
qed.
*)

lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
  if taa_non_empty … taa then ¬as_costed … s2 else True.
#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
[ #s1 %
| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
  [ #s2 #H #K #_ assumption
  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
  ]
]
qed.

let rec tal_collapsable_to_rel S fl st1 st2
  (tal : trace_any_label S fl st1 st2) on tal :
  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
  with
  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
  | tal_base_not_return _ st2' _ _ K ⇒ ?
  | _ ⇒ Ⓧ
  ].
* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
qed.

let rec tal_collapsable_eq_flag S fl st1 st2
  (tal : trace_any_label S fl st1 st2) on tal :
  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
  with
  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
  | _ ⇒ Ⓧ
  ].

let rec tal_collapsable_split S fl st1 st2
  (tal : trace_any_label S fl st1 st2) on tal :
  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
  with
  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
  | tal_base_not_return st1' st2' H I J ⇒ ?
  | _ ⇒ Ⓧ
  ].
[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
| #coll
  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
  #EQ >EQ %
]
qed.

lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
elim (tal_collapsable_split … coll) lapply tal
 >(tal_collapsable_eq_flag … coll) -tal #tal
#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
%[|%[|%[|%[|%[| % ]]]]]
qed.

lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
[ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
/2 by taa_append_tal_rel/
qed.

(* little helpers *)
lemma if_else_True : ∀b,P.P → if b then P else True.
* // qed-.
lemma if_then_True : ∀b,P.P → if b then True else P.
* // qed-.

include alias "basics/logic.ma".

let rec status_simulation_produce_tlr S1 S2 R
(* we start from this situation
     st1 →→→→tlr→→→→ st1'
      | \
      L  \---S--\
      |          \
   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
                        by the preceding call)
   
   and we produce
     st1 →→→→tlr→→→→ st1'
             \\      /  \
             //     R    \-L,S-\
             \\     |           \
   st2_lab →tlr→ st2_mid →taaf→ st2'
*) 
  st1 st1' st2_lab st2
  (tlr1 : trace_label_return S1 st1 st1')
  (taa2_pre : trace_any_any S2 st2_lab st2)
  (sim_execute : status_simulation S1 S2 R)
  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
  ∃st2_mid.∃st2'.
  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
  ∃taa2 : trace_any_any_free … st2_mid st2'.
  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
  tlr_rel … tlr1 tlr2 ≝
 match tlr1 with
 [ tlr_base st1 st1' tll1 ⇒ ?
 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
 ]
and status_simulation_produce_tll S1 S2 R
(* we start from this situation
     st1 →→→→tll→→→ st1'
      | \
      L  \---S--\
      |          \
   st2_lab →taa→ st2
   
   and if the tll is a returning one we produce a diagram like the one for tlr,
   otherwise a simpler:
     st1 →→→→tll→→→→ st1'
             \\       |
             //      L,S
             \\       |
   st2_lab →→→tll→→→ st2'
*)
  fl st1 st1' st2_lab st2
  (tll1 : trace_label_label S1 fl st1 st1')
  (taa2_pre : trace_any_any S2 st2_lab st2)
  (sim_execute : status_simulation S1 S2 R)
   on tll1 : R st1 st2 → label_rel … st1 st2_lab → 
    match fl with
    [ ends_with_ret ⇒
      ∃st2_mid.∃st2'.
      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
      ∃taa2 : trace_any_any_free … st2_mid st2'.
      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
      tll_rel … tll1 tll2
    | doesnt_end_with_ret ⇒
      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
    ] ≝
  match tll1 with
  [ tll_base fl1' rst1 rst1' tal1 H ⇒ ?
  ]
and status_simulation_produce_tal S1 S2 R
(* we start from this situation
     st1 →→tal→→ st1'
      |
      S
      |
     st2
   
   and if the tal is a returning one we produce a diagram like the one for tlr,
   otherwise we allow for two possibilities:
   either

     st1 →→tal→→ st1'
            \\    |
            //   L,S
            \\    |
     st2 →→tal→→ st2'

   or we do not advance from st2:

     st1 →→tal→→ st1'  collapsable, and st1 uncosted
                /
         /-L,S-/
        /
     st2
*)
  fl st1 st1' st2
  (tal1 : trace_any_label S1 fl st1 st1')
  (sim_execute : status_simulation S1 S2 R)
   on tal1 : R st1 st2 →
    match fl with
    [ ends_with_ret ⇒
      ∃st2_mid.∃st2'.
      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
      ∃taa2 : trace_any_any_free … st2_mid st2'.
      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
      tal_rel … tal1 tal2
    | doesnt_end_with_ret ⇒
      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
      (* empty *)
      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
    ] ≝
  match tal1 with
  [ tal_base_not_return st1' st1'' H G K ⇒ ?
  | tal_base_return st1' st1'' H G ⇒ ?
  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
  | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ?
  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
  ].
#st1_R_st2
[1,2,3: #st1_L_st2_lab ]
[ (* tlr_base *)
  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
  #st2_mid * #st2' * #tll2 #H
  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
| (* tlr_step *)
  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
  #st2_mid * #tll2 ** #H1 #H2 #H3
  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
  %{H4} %{H3 H5}
| (* tll_base *)
  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
  cases fl1' in tal1; normalize nodelta #tal1 *
  [3: * #_ #ABS elim (absurd … H ABS) ]
  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
  [1,3: whd <st1_L_st2_lab assumption
  |*: [%{taa2} ] %{H1} %
    [1,3: change with (opt_safe ??? = opt_safe ???)
      @opt_safe_elim #a #EQ1
      @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
    |*: @taa_append_tal_rel assumption
    ] 
  ]
| (* tal_base_non_return *) whd
  cases G -G #G
  lapply (sim_execute … H st1_R_st2)
  (* without try it fails... why? *)
  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
  [ #H lapply (H K) -H ] *
  #st2' ** -st2 -st2'
  [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *)
    ** whd in ⊢ (%→?); *
    [1,3: #ncost #R' #L' %2 /4 by conj/
    |*: * #ABS elim (ABS K)
    ]
  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ]
    *** #st1_R_st2' #st1_L_st2' %1
    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
    % /2 by conj/
    % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
  ]
| (* tal_base_return *) whd
  lapply (sim_execute … H st1_R_st2)
  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
  ***** #ncost #J2 #K2
  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
  % [ /4 by conj/ ]
  %[ % | %[|%[|%[|%[| % ]]]]]]]
| (* tal_base_call *) whd
  lapply (sim_execute … H st1_R_st2)
  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
  #H elim (H G) -H
  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
  #st1_R_st2_mid #st1_L_st2_after_call
  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
  [ #st2' #tlr2 *****
  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
    #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
  ]
  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
  %{st2'}
  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    [3: % [ % assumption ]
      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
    ]
  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
    [2: %1{J2} |6: %2{J2}
    |4,8: % try (% assumption)
      % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
        % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
      ]]]]]]]]]]
    ]
  ]
  [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption
  |*: whd <st1_L_st2' assumption
  ]
| (* tal_base_tailcall *) whd
  lapply (sim_execute … H st1_R_st2)
  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
  #H elim (H G) -H
  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
  #st1_R_st2_mid #st1_L_st2_after_call
  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
  #st2_after_ret * #st2' * #tlr2 * #taa2''
  * #props #S
  %{st2_after_ret} %{st2'}
  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
  %{taa2''}
  %{props}
  % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
| (* tal_step_call *)
  lapply (sim_execute … H st1_R_st2)
  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
  #H elim (H G) -H
  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
  #st1_R_st2_mid #st1_L_st2_after_call
  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
  #st2_after_ret * #st2' * #tlr2 * #taa2''
  ****
  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
  cases fl1' in tl1; #tl1 *
  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    [4: %{taa2'''} % [ /4 by conj/ ]
      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
    ]]]
  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    [4: % [ /2 by conj/ ]
      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
    ]]
  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
      [3: % [ /2 by conj/ ]
      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
      [2: %1{J2'} |6: %2{J2'}
      |4,8: % [1,3: /2 by conj/]
        %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
          %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
        ]]]]]]]]]]
      ]]
    ]
  ]
  [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption
  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
    [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
    |*: normalize nodelta //
    ]
  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
  |*: whd <st1_L_st2'' @(trace_any_label_label … tl1)
  ]
| (* step_default *)
  lapply (sim_execute … H st1_R_st2)
  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
  cases fl1' in tl1; #tl1 *
  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
      [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
    ]]
  | *#st2' *#tal2 *#H #G %1
    %[| %{(taaf_append_tal … taa2 ? tal2)}
      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
    ]
  | (* can't happen *)
    *** #_ #L' elim (absurd ?? K)
    whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1)
  ]
  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
]
qed.

definition is_cl_jump : ∀S : abstract_status.S → bool ≝
λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].

definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.

(* finite flat traces, with recursive structure right to left. The list of
   identifiers represents the call stack *)
inductive flat_trace (S : abstract_status) (start : S) : S → Type[0] ≝
| ft_start : flat_trace S start start
| ft_advance :
  ∀st1,st2.flat_trace S start st1 → as_execute S st1 st2 →
  enforce_costedness … st1 st2 → flat_trace S start st2.

(*
  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
  flat_trace S start st2 stack
| ft_advance_call :
  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
  ∀prf : as_classifier ? st1 cl_call.
  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
| ft_advance_tailcall :
  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
  ∀prf : as_classifier ? st1 cl_tailcall.
  flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
| ft_advance_ret :
  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
  as_classifier ? st1 cl_return →
  flat_trace S start st2 stack.
*)

let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
  (taa : trace_any_any S st2 st3)
on taa : flat_trace S st1 st3 ≝
match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
[ taa_base s ⇒ λacc.acc
| taa_step st1 st2 st3 H G _ tl ⇒
  λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
] ft.
@hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.

lemma ft_extend_extend_taa : ∀S,st1,st2,st3,st4,ft,taa1,taa2.
  ft_extend_taa S st1 st3 st4 (ft_extend_taa … st2 … ft taa1) taa2 =
  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
#S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
/2/
qed.

definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
  λtaaf : trace_any_any_free S st2 st3.
  match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
  [ taaf_base s ⇒ λft.ft
  | taaf_step s1 s2 s3 pre H G ⇒
    λft.ft_advance … (ft_extend_taa … ft pre) H ?
  | taaf_step_jump s1 s2 s3 pre H G K ⇒
    λft.ft_advance … (ft_extend_taa … ft pre) H ?
  ] ft.
@hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.

definition option_to_list : ∀A.option A → list A ≝ λA,x.
  match x with
  [ Some x ⇒ [x]
  | None ⇒ [ ]
  ].

(*
let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
match ft with
[ ft_start ⇒ [ ]
| ft_advance st1_mid st1' pre1 _ _ ⇒
  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
  [ cl_call ⇒ λprf.
    let id ≝ as_call_ident ? «st1_mid, prf» in
    id :: ft_stack … pre1
  | cl_tailcall ⇒ λprf.
    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    match ft_stack … pre1 with
    [ nil ⇒ (* should never happen in correct programs *)
      [id]
    | cons _ stack' ⇒
      id :: stack'
    ]
  | cl_return ⇒ λ_.
    match ft_stack … pre1 with
    [ nil ⇒ (* should never happen in correct programs *)
      [ ]
    | cons _ stack' ⇒ stack'
    ]
  | _ ⇒ λ_.ft_stack … pre1
  ] (refl …)
].
*)

(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
(* inefficient, but used only in correctness proofs *)
let rec ft_stack_observables S st st'
  (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
match ft with
[ ft_start ⇒ 〈[ ], [ ]〉
| ft_advance st1_mid st1' pre1 _ _ ⇒
  let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
  [ cl_call ⇒ λprf.
    let id ≝ as_call_ident ? «st1_mid, prf» in
    let tr' ≝ tr @ add @ [IEVcall id] in
    〈id :: stack, tr'〉
  | cl_tailcall ⇒ λprf.
    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    match stack with
    [ nil ⇒ (* should never happen in correct programs *)
      〈[ ], tr @ add〉
    | cons f stack' ⇒
      let tr' ≝ tr @ add @ [IEVtailcall f id] in
      〈id :: stack', tr'〉
    ]
  | cl_return ⇒ λ_.
    match stack with
    [ nil ⇒ (* should never happen in correct programs *)
      〈[ ], tr @ add〉
    | cons f stack' ⇒
      let tr' ≝ tr @ add @ [IEVret f] in
      〈stack', tr'〉
    ]
  | _ ⇒ λ_.〈stack, tr @ add〉
  ] (refl …)
].

definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).

definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
λS,st1,st2,ft.
match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].

lemma status_class_dep_match_elim :
∀A : Type[0].∀P : A → Prop.
∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
(∀prf : cl = cl_call.P (c_call prf)) →
(∀prf : cl = cl_return.P (c_return prf)) →
(∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
(∀prf : cl = cl_other.P (c_other prf)) →
(∀prf : cl = cl_jump.P (c_jump prf)) →
P (match cl return λx.cl = x → ? with
   [ cl_call ⇒ c_call
   | cl_return ⇒ c_return
   | cl_tailcall ⇒ c_tailcall
   | cl_other ⇒ c_other
   | cl_jump ⇒ c_jump
   ] (refl …)).
#A #P * normalize // qed.

lemma status_class_dep_match_rewrite :
∀A : Type[0].
∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
∀cl'.
∀prf : cl = cl'.
match cl return λx.cl = x → A with
 [ cl_call ⇒ c_call
 | cl_return ⇒ c_return
 | cl_tailcall ⇒ c_tailcall
 | cl_other ⇒ c_other
 | cl_jump ⇒ c_jump
 ] (refl …) =
match cl' return λx.cl = x → A with
 [ cl_call ⇒ c_call
 | cl_return ⇒ c_return
 | cl_tailcall ⇒ c_tailcall
 | cl_other ⇒ c_other
 | cl_jump ⇒ c_jump
 ] prf.
#A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.

lemma pair_elim' :
  ∀A,B,C : Type[0].∀T : A → B → C.∀t : A × B.
  ∀P : (A×B) → C → Prop.
  P 〈\fst t, \snd t〉 (T (\fst t) (\snd t)) →
  P t (let 〈a, b〉 ≝ t in T a b).
#A #B #C #T * // qed.

lemma ft_extend_taa_obs : ∀S,st1,st2,st3,ft,taa.
  ft_stack_observables … (ft_extend_taa S st1 st2 st3 ft taa) =
    〈ft_stack … ft, ft_observables … ft @
    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
#S #st1 #st2 #st3 #ft #taa lapply ft elim taa -st2 -st3
[ #st2 #ft >append_nil @eq_pair_fst_snd ]
#st2 #st3 #st4 #H #K #G #taa #IH #ft
whd in ⊢ (??(????%)?); >IH normalize nodelta
-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
[ #st3 #H #G
| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
  >(not_costed_no_label … G)
]
>append_nil whd in ⊢ (??(???%%)(????(??%?)));
whd in match (ft_stack_observables ????) ;
@(pair_elim' … (ft_stack_observables … ft))
>(status_class_dep_match_rewrite … K) %
qed.

lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
  ∀ft : flat_trace S st1 st2.
  ∀taa : trace_any_any S st2 st3.
  ∀H : as_execute S st3 st4.∀G.
  ft_stack_observables … (ft_advance … (ft_extend_taa … ft taa) H G) =
  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
   match as_classify … st3 return λx.as_classifier … st3 x → ? with
    [ cl_call ⇒ λprf.
      let id ≝ as_call_ident ? «st3, prf» in
      let tr' ≝ tr @ add @ [IEVcall id] in
      〈id :: ft_stack … ft, tr'〉
    | cl_tailcall ⇒ λprf.
      let id ≝ as_tailcall_ident ? «st3, prf» in
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVtailcall f id] in
        〈id :: stack', tr'〉
      ]
    | cl_return ⇒ λ_.
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVret f] in
        〈stack', tr'〉
      ]
    | _ ⇒ λ_.〈stack, tr @ add〉
    ] (refl …)).
#S #st1 #st2 #st3 #st4 #ft #taa #H #G normalize nodelta
whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
@status_class_dep_match_elim #prf
@status_class_dep_match_elim #prf'
try(@⊥ >prf in prf'; #prf' -prf destruct @False)
>ft_extend_taa_obs whd in match ft_stack; whd in match ft_observables; normalize nodelta
[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
@eq_f >associative_append @eq_f
lapply prf lapply prf' lapply (taa_end_not_costed … taa)
cases taa -st3 -st2 normalize nodelta
[1,3,5,7,9,11,13: #st2 * #prf #prf' % ]
#st2 #st2' #st3 #H' #G' #K' #taa' #K #prf #prf'
>(not_costed_no_label … K) try % >append_nil %
qed.

lemma ft_extend_taaf_obs : ∀S,st1,st2,st3,ft,taaf.
  ft_stack_observables … (ft_extend_taaf S st1 st2 st3 ft taaf) =
    〈ft_stack … ft,
     ft_observables … ft @
      if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
#S #st1 #st2 #st3 #ft #taa lapply ft cases taa -st2 -st3
[ #st2 #ft >append_nil @eq_pair_fst_snd ]
#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
whd in match ft_extend_taaf; normalize nodelta
>ft_extend_taa_advance_obs @pair_elim'
>(status_class_dep_match_rewrite … G) %
qed.

(*
lemma ft_extend_taaf_advance_obs : ∀S,st1,st2,st3,st4.
  ∀ft : flat_trace S st1 st2.
  ∀taaf : trace_any_any_free S st2 st3.
  ∀H : as_execute S st3 st4.∀G.
  ft_stack_observables … (ft_advance … (ft_extend_taaf … ft taaf) H G) =
  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
   match as_classify … st3 return λx.as_classifier … st3 x → ? with
    [ cl_call ⇒ λprf.
      let id ≝ as_call_ident ? «st3, prf» in
      let tr' ≝ tr @ add @ [IEVcall id] in
      〈id :: ft_stack … ft, tr'〉
    | cl_tailcall ⇒ λprf.
      let id ≝ as_tailcall_ident ? «st3, prf» in
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVtailcall f id] in
        〈id :: stack', tr'〉
      ]
    | cl_return ⇒ λ_.
      match stack with
      [ nil ⇒ (* should never happen in correct programs *)
        〈[ ], tr @ add〉
      | cons f stack' ⇒
        let tr' ≝ tr @ add @ [IEVret f] in
        〈stack', tr'〉
      ]
    | _ ⇒ λ_.〈stack, tr @ add〉
    ] (refl …)).
#S #st1 #st2 #st3 #st4 #ft #taaf lapply ft cases taaf
whd in match ft_extend_taaf; normalize nodelta
[ #st #ft #H #G whd in ⊢ (??%?); @pair_elim' normalize nodelta % ]
#st2 #st2' #st3 #taa' #H' #G' [2: #K' ] #ft #H #G
whd in ⊢ (??%?); >ft_extend_taa_advance_obs normalize nodelta
@(pair_elim' … (ft_stack_observables … ft)) normalize nodelta
>(status_class_dep_match_rewrite … G') normalize nodelta
@status_class_dep_match_elim #prf
@status_class_dep_match_elim #prf'
try(@⊥ >prf in prf'; #prf' -prf destruct @False)
[ >associative_append 
whd in match ft_stack; whd in match ft_observables; normalize nodelta
[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
@eq_f >associative_append @eq_f
lapply prf lapply prf' lapply G
cases taaf -st3 -st2 normalize nodelta
[1,4,7,10,13,16,19: #st2 #_ #prf #prf' % ]

>(not_costed_no_label … K) try % >append_nil %
qed.
*)

(* little helper to avoid splitting equal cases *)
lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.

lemma enforce_costedness_ok : ∀S,s1,s2.enforce_costedness S s1 s2 →
as_classifier S s1 cl_jump → as_costed … s2.
#S #s1 #s2 whd in ⊢ (%→%→?); whd in match (is_cl_jump ??); #H #G >G in H; #K @K qed.

let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa :
  trace_any_any_free S st1 st2 ≝
match taa return λst1,st2,taa.trace_any_any_free S st1 st2 with
[ taa_base s ⇒ taaf_base … s
| taa_step s1 s2 s3 ex cl ncost tl ⇒
  taaf_cons … ex cl (taa_to_taaf … tl) ?
]. @if_else_True assumption qed.

definition taa_append_taaf : ∀S,st1,st2,st3.
  trace_any_any S st1 st2 → trace_any_any_free S st2 st3 →
  trace_any_any_free S st1 st3 ≝
λS,st1,st2,st3,taa,taaf.
match taaf return λst2,st3,taaf.trace_any_any S st1 st2 → trace_any_any_free S st1 st3 with
[ taaf_base s ⇒ taa_to_taaf …
| taaf_step s1 s2 s3 taa' ex cl ⇒
  λtaa.taaf_step … (taa_append_taa … taa taa') ex cl
| taaf_step_jump s1 s2 s3 taa' ex cl K ⇒
  λtaa.taaf_step_jump … (taa_append_taa … taa taa') ex cl K
] taa.

lemma taa_to_taaf_non_empty : ∀S,st1,st2,taa.
taaf_non_empty … (taa_to_taaf S st1 st2 taa) = taa_non_empty … taa.
#S #st1 #st2 #taa elim taa -st1 -st2
[ #s % | #s1 #s2 #s3 #ex #cl #ncost #tl #IH
  change with (taaf_cons ????????) in match (taa_to_taaf ????);
  >taaf_cons_non_empty %
qed.

lemma taa_append_taaf_non_empty : ∀S,st1,st2,st3,taa,taaf.
taaf_non_empty … (taa_append_taaf S st1 st2 st3 taa taaf) =
(taa_non_empty … taa ∨ taaf_non_empty … taaf).
#S #st1 #st2 #st3 #taa #taaf lapply taa cases taaf -st2 -st3
[ #s #taa whd in match (taa_append_taaf ??????); >taa_to_taaf_non_empty
  >commutative_orb %
|*: #s1 #s2 #s3 #taa' #ex #cl [2: #K] #taa >commutative_orb %
]
qed.

lemma taa_empty_to_eq : ∀S,st1,st2,taa.
¬(bool_to_Prop (taa_non_empty S st1 st2 taa)) → st1 = st2.
#S #st1 #st2 * // #s1 #s2 #s3 #ex #cl #K #tl * #ABS cases (ABS ?) % qed.

lemma taaf_empty_to_eq : ∀S,st1,st2,taaf.
¬(bool_to_Prop (taaf_non_empty S st1 st2 taaf)) → st1 = st2.
#S #st1 #st2 * // #s1 #s2 #s3 #pre #ex #cl [2: #K ] * #ABS cases (ABS ?) % qed.

theorem status_simulation_produce_ft :
(* from

  st1 →→→ft→→→ st1'
   |
  R,L
   |
  st2

  we produce
  
  st1 →→→ft→→→ st1'-------\
         //      \         \
         \\       L         S
         //       |          \
  st2 →→→ft→→→ st2_lab →taa→ st2'
  
  so that from any tlr or tll following st1' we can produce the corresponding
  structured trace from st2_lab using the previous result
*)
  ∀S1,S2.
  ∀R.
  ∀st1,st1',st2.∀ft1 : flat_trace S1 st1 st1'.
  status_simulation S1 S2 R → R st1 st2 → label_rel … st1 st2 →
  ∃st2_lab,st2'.
  ∃ft2 : flat_trace S2 st2 st2_lab.
  ∃taa : trace_any_any S2 st2_lab st2'.
  R st1' st2' ∧ label_rel … st1' st2_lab ∧ ft_stack_observables … ft1 = ft_stack_observables … ft2.
#S1 #S2 #R #st1 #st1' #st2 #ft1 #sim_execute #H #G elim ft1 -st1'
[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % ]
#st1_mid #st1' #ft1 #ex #ncost_st1'
(* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #G' #L' #S
inversion (as_classify … st1_mid) #cl
[2,5: (* other/jump *)
  lapply (sim_execute … ex G')
  try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
  [ #H lapply (H (enforce_costedness_ok ??? ncost_st1' (jmeq_to_eq … cl))) -H ] *
  #st2' *#taaf ** #ncost #H'' #G''
  %{st2'} %{st2'}
  %[1,3:
    @(ft_extend_taaf … (taa_append_taaf … taa taaf))
    assumption]
  %{(taa_base …)}
  % [1,3: %{H'' G''} ]
  >ft_extend_taaf_obs >taa_append_taaf_non_empty
  whd in match ft_observables; whd in match ft_stack; normalize nodelta
  <S whd in ⊢ (??%?); @pair_elim' normalize nodelta
  >(status_class_dep_match_rewrite … cl) normalize nodelta @eq_f @eq_f
  cases (true_or_false_Prop taa) #Htaa >Htaa
  [2,4: lapply (taa_empty_to_eq … Htaa) #EQ destruct
    cases (true_or_false_Prop (taaf_non_empty … taaf)) #Htaaf
    >Htaaf in ncost ⊢ %;
    [1,3: #_ |*: * #ncost lapply (taaf_empty_to_eq … Htaaf) #EQ destruct ]
  ]
  normalize nodelta in ncost ⊢ %; // >not_costed_no_label //
  whd in ⊢ (?%); >L' <G'' assumption
|4: (* tailcall *)
  lapply (sim_execute … ex G')
  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
  * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
  * #taa2 * #taa2' ** #ex' #H'' #G''
  %{st2_after_call} %{st2'}
  %[@(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
    @(ft_extend_taa … (taa_append_taa … taa taa2))
    assumption]
  %{taa2'}
  % [ %{H'' G''} ]
  >ft_extend_taa_advance_obs
  whd in ⊢ (??%?); @pair_elim' @pair_elim'
  >(status_class_dep_match_rewrite … cl)
  >(status_class_dep_match_rewrite … cl') normalize nodelta
  >S <EQcall >L' %
|1: (* ret *)
  lapply (sim_execute … ex G')
  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
  #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
  ***** #ncost #cl' #ex' #H'' #_ #G'' %{st2'} %{st2'}
  %[@(ft_extend_taaf … taa2')
    @(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
    @(ft_extend_taa … (taa_append_taa … taa taa2))
    assumption]
  %{(taa_base …)}
  % [ %{H'' G''} ]
  >ft_extend_taaf_obs whd in match ft_observables; whd in match ft_stack; normalize nodelta
  >ft_extend_taa_advance_obs
  whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
  >(status_class_dep_match_rewrite … cl)
  >(status_class_dep_match_rewrite … cl') normalize nodelta
  >S cases (\fst (ft_stack_observables … ft2)) [2: #f #stack']
  normalize nodelta @eq_f >L' >associative_append @eq_f
  cases (true_or_false_Prop (taaf_non_empty … taa2')) #H
  >H in ncost ⊢ %; normalize nodelta [1,3: #ncost |*: lapply (taaf_empty_to_eq … H) #EQ destruct #_ ]
  // >(not_costed_no_label … st2_after_ret) // >append_nil %
|3: (* call *)
  lapply (sim_execute … ex G')
  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
  * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
  * #taa2 * #taa2' ** #ex' #H'' #G''
  %{st2_after_call} %{st2'}
  %[@(ft_advance … ex' ?) [2: @hide_prf  normalize >cl' % ]
    @(ft_extend_taa … (taa_append_taa … taa taa2))
    assumption]
  %{taa2'}
  % [ %{H'' G''} ]
  >ft_extend_taa_advance_obs @pair_elim' >(status_class_dep_match_rewrite … cl') normalize nodelta
  whd in ⊢ (??%?); @pair_elim' >(status_class_dep_match_rewrite … cl) normalize nodelta
  >S <EQcall >L' %
]
qed.

theorem status_simulation_produce_ft_and_tlr :
∀S1,S2.
∀R.
∀st1,st1',st1'',st2.
∀ft1 : flat_trace S1 st1 st1'.
∀tlr1 : trace_label_return S1 st1' st1''.
status_simulation_with_init S1 S2 R st1 st2 →
∃st2',st2'',st2'''.
∃ft2 : flat_trace S2 st2 st2'.
∃tlr2 : trace_label_return S2 st2' st2''.
∃taaf : trace_any_any_free S2 st2'' st2'''.
(∀x.as_result … st1'' = Some ? x → as_result … st2''' = Some ? x) ∧
ft_observables … ft1 = ft_observables … ft2 ∧
tlr_rel … tlr1 tlr2.
#S1 #S2 #R #st1 #st1' #st1'' #st2 #ft1 #tlr1 * #S #L #simul
cases (status_simulation_produce_ft … ft1 simul S L)
#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ1
cases (status_simulation_produce_tlr … tlr1 taa2 simul S' L')
#st2'' * #st2''' * #tlr2 * #taa2' **** #_ #S'' #_ #_ #EQ2
%{st2'} %{st2''} %{st2'''} %{ft2} %{tlr2} %{taa2'} %{EQ2} %
[ #res #EQ @(sim_final … simul … EQ S'')
| whd in ⊢ (??%%); @eq_f assumption
]
qed.