include "basics/lists/list.ma".
include "common/StructuredTraces.ma".

inductive call_ud : Type [0] ≝ 
  | up: ident → call_ud    (* call *)
  | down: ident → call_ud. (* return *)

record stacksize_info : Type[0] ≝
{ current : ℕ ; maximum : ℕ }.

definition update_stacksize_info :
  (ident → option ℕ) → stacksize_info → list call_ud → stacksize_info ≝ 
  λstacksizes.
  let get_stacksize ≝
    λf.match stacksizes f with
      [ Some n ⇒ n | None ⇒ 0 (* should never happen *) ] in
  let f ≝ λud,acc.
    match ud with
    [ up i ⇒
      let new_stack ≝ get_stacksize i + current acc in
      let new_max ≝ max (maximum acc) new_stack in 
      mk_stacksize_info new_stack new_max
    | down i ⇒
      let new_stack ≝ current acc - get_stacksize i in
      mk_stacksize_info new_stack (maximum acc)
    ] in
  foldr ?? f.

definition extract_call_ud_from_observables :
  list intensional_event → list call_ud ≝
let f ≝ λev.match ev with
[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
foldr ?? (λev.append ? (f ev)) [ ].

definition extract_call_ud_from_tlr :
  ∀S,st1,st2.trace_label_return S st1 st2 → ident → list call_ud ≝
λS,st1,st2,tlr,curr.
  extract_call_ud_from_observables … (observables_trace_label_return … tlr curr).

definition extract_call_ud_from_tll :
  ∀S,fl,st1,st2.trace_label_label fl S st1 st2 → ident → list call_ud ≝
λS,fl,st1,st2,tll,curr.
  extract_call_ud_from_observables … (observables_trace_label_label … tll curr).

lemma tlr_rel_same_stacksize_info :
  ∀stacksizes.
  ∀S1,S2,s1,s1',s2,s2'.
  ∀tlr1 : trace_label_return S1 s1 s1'.
  ∀tlr2 : trace_label_return S2 s2 s2'.
  ∀curr.∀curr_stacksize.
  tlr_rel … tlr1 tlr2 →
  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr1 curr) =
  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr2 curr).
#stacksizes #S1 #S2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
#equiv @eq_f whd in ⊢ (??%%); @eq_f
@tlr_rel_to_traces_same_observables assumption
qed.

lemma tll_rel_same_stacksize_info :
  ∀stacksizes.
  ∀S1,S2,fl1,fl2,s1,s1',s2,s2'.
  ∀tll1 : trace_label_label S1 fl1 s1 s1'.
  ∀tll2 : trace_label_label S2 fl2 s2 s2'.
  ∀curr.∀curr_stacksize.
  tll_rel … tll1 tll2 →
  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll1 curr) =
  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll2 curr).
#stacksizes #S1 #S2 #fl1 #fl2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
#equiv @eq_f whd in ⊢ (??%%); @eq_f
@tll_rel_to_traces_same_observables assumption
qed.