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 ≝ λacc,ud.
    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
  foldl ?? f.

lemma foldr_append : ∀A,B,f,b,l1,l2.
foldr A B f b (l1@l2) = foldr A B f (foldr A B f b l2) l1.
#A #B #f #b #l1 elim l1 -l1 [#l2 %]
#hd #tl #IH #l2 whd in ⊢ (??%%); >IH %
qed.

lemma foldl_append : ∀A,B,f,b,l1,l2.
foldl A B f b (l1@l2) = foldl A B f (foldl A B f b l1) l2.
#A #B #f #b #l1 lapply b -b elim l1 -l1 [#b #l2 %]
#hd #tl #IH #b #l2 whd in ⊢ (??%(????%?)); >IH %
qed.

lemma update_stacksize_info_append :
∀ss,info,l1,l2.
update_stacksize_info ss info (l1 @ l2) =
update_stacksize_info ss (update_stacksize_info ss info l1) l2.
#ss #info @foldl_append qed.

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)) [ ].

lemma extract_call_ud_from_observables_append :
∀l1,l2.extract_call_ud_from_observables (l1@l2) =
  extract_call_ud_from_observables l1 @ extract_call_ud_from_observables l2.
#l1 elim l1 -l1 [ #l2 % ]
#hd #tl #IH #l2 whd in ⊢ (??%(??%?)); >associative_append @eq_f @IH qed.

lemma update_stacksize_info_max_monotone :
∀ss,info,l.maximum info ≤ maximum (update_stacksize_info ss info l).
#ss #info #l lapply info elim l -l [ #info % ]
* #id #tl #IH #info
whd in match (update_stacksize_info ???); normalize nodelta
change with (update_stacksize_info ???) in ⊢ (??(?%));
@(transitive_le ???? (IH …))
[ whd in ⊢ (??%); @(leb_elim (?:ℕ)) #H ] //
qed.

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.