Changeset 2755

Timestamp:

Mar 1, 2013, 11:06:29 AM (7 years ago)

Author:

tranquil

Message:

• changed primitives of abstract status (with stuf that is probably already there in all of its implementations): this temporarily breaks current as creations
• generalised stacksize file and consequently moved it to common

Location:

src/common

Files:

• StatusSimulation.ma (modified) (1 diff)
• StructuredTraces.ma (modified) (19 diffs)
• stacksize.ma (moved) (moved from src/joint/stacksize.ma) (1 diff)

src/common/StatusSimulation.ma

@@ -707 +707 @@
 
 (* the observables of a flat trace (for the moment, only labels, calls and returns) *)
-
-inductive intensional_event : Type[0] ≝
-| IEVcost : costlabel → intensional_event
-| IEVcall : ident → intensional_event
-| IEVtailcall : ident → ident → intensional_event
-| IEVret : ident → intensional_event.
-
 let rec ft_observables_aux acc S st st' stack
   (ft : flat_trace S st st' stack) on ft : list intensional_event ≝

src/common/StructuredTraces.ma

@@ -1 @@
-include "basics/types.ma".
+ include "basics/types.ma".
 include "basics/bool.ma".
 include "basics/jmeq.ma".
@@ -6 +6 @@
 include "basics/lists/listb.ma".
 include "ASM/Util.ma".
+include "common/IO.ma".
+include "utilities/hide.ma".
 
 inductive status_class: Type[0] ≝
@@ -16 +18 @@
 record abstract_status : Type[1] ≝
   { as_status :> Type[0]
-  ; as_execute : as_status → as_status → Prop
+  ; as_eval : as_status → IO io_out io_in as_status
   ; as_pc : DeqSet
   ; as_pc_of : as_status → as_pc
@@ -22 +24 @@
   ; as_label_of_pc : as_pc → option costlabel
   ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
-  ; as_final: as_status → Prop
+  ; as_result: as_status → option int
   ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
   ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
@@ -29 +31 @@
 definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
 definition as_call ≝ λS,s,f.as_call_ident S s = f.
+definition as_final ≝ λS,s.as_result S s ≠ None ?.
+definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2.
 
 definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
@@ -37 +41 @@
 definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
   λa_s,st.as_label ? st ≠ None ?.
-
-definition as_label_safe : ∀a_s : abstract_status.
-  (Σs : a_s.as_costed ? s) → costlabel ≝
-  λa_s,st_sig.opt_safe … (pi2 … st_sig).
 
 lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
@@ -63 +63 @@
 
 definition as_cost_label ≝
-  λS : abstract_status. Σl.as_cost_labelled S l. 
+  λS : abstract_status. Σl.as_cost_labelled S l.
+
+unification hint 0 ≔ S ⊢ as_cost_label S ≡ Sig costlabel (λl.as_cost_labelled S l). 
 
 definition as_cost_labels ≝
@@ -76 +78 @@
 definition as_cost_map ≝
   λS : abstract_status. (as_cost_label S) → ℕ.
+  
+definition as_label_safe : ∀a_s : abstract_status.
+  (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
+  λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
+@hide_prf
+@opt_safe_elim #c #EQ %{EQ} qed.
   
 definition lift_sigma_map_id :
@@ -599 +607 @@
     match tll2 with
     [ tll_base fl2 st2 st2 tal2 G ⇒
-      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
+      pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
       tal_rel … tal1 tal2
     ]
@@ -726 +734 @@
 qed.
 
-let rec flatten_trace_label_label
+inductive intensional_event : Type[0] ≝
+| IEVcost : costlabel → intensional_event
+| IEVcall : ident → intensional_event
+| IEVtailcall : ident → ident → intensional_event
+| IEVret : ident → intensional_event.
+
+(* NB: we don't restrict call idents, because it would need some more tinkering
+   with abstract_status *)
+definition as_emittable : abstract_status → intensional_event → Prop ≝
+λS,ev.
+match ev with
+[ IEVcost c ⇒ as_cost_labelled S c
+| _ ⇒ True
+].
+ 
+definition as_trace ≝
+λS : abstract_status.
+Σl : list intensional_event.All … (as_emittable S) l.
+
+unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
+
+definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
+λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
+
+definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
+λA,P,l1,l2.«l1@l2,
+  cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
+
+definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
+
+interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
+interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
+interpretation "safe nil" 'vnil = (nil_safe ??).
+
+definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
+λS,l.«IEVcost l, pi2 … l».
+
+let rec observables_trace_label_label
   (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     (start_status: S) (final_status: S)
       (the_trace: trace_label_label S trace_ends_flag start_status final_status)
-        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
+      (curr : ident)
+        on the_trace: as_trace S ≝
   match the_trace with
   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
-      let label ≝
-        match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
-        [ None ⇒ λabs. ⊥
-        | Some l ⇒ λ_. l
-        ] labelled_proof
-      in
-        (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace
-  ]
-and flatten_trace_any_label
+      let label ≝ as_label_safe … «?, labelled_proof» in
+      emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
+  ]
+and observables_trace_any_label
   (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     (start_status: S) (final_status: S)
       (the_trace: trace_any_label S trace_ends_flag start_status final_status)
-        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
+      (curr : ident)
+        on the_trace: as_trace S ≝
   match the_trace with
-  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
-  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
-      flatten_trace_label_return … call_trace
-  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
-      flatten_trace_label_return … call_trace
-  | tal_base_return the_status _ _ _ ⇒ [ ]
+  [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
+  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
+      let id ≝ as_call_ident ? «?, cl» in
+      IEVcall id ::: observables_trace_label_return ??? call_trace id
+  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
+      let id ≝ as_tailcall_ident ? «?, cl» in
+      IEVtailcall curr id ::: observables_trace_label_return … call_trace id
+  | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
-    _ _ _ call_trace _ final_trace ⇒
-    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
-    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
-        call_cost_trace @ final_cost_trace
+    _ cl _ call_trace _ final_trace ⇒
+    let id ≝ as_call_ident ? «?, cl» in
+    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
+    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
+    IEVcall id ::: call_cost_trace @@ final_cost_trace
   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
-      flatten_trace_any_label … tail_trace
-  ]
-and flatten_trace_label_return
+    observables_trace_any_label … tail_trace curr
+  ]
+and observables_trace_label_return
   (S: abstract_status)
     (start_status: S) (final_status: S)
       (the_trace: trace_label_return S start_status final_status)
-        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
+      (curr : ident)
+        on the_trace: as_trace S ≝
   match the_trace with
   [ tlr_base before after trace_to_lift ⇒
-      flatten_trace_label_label … trace_to_lift
+      observables_trace_label_label … trace_to_lift curr
   | tlr_step initial labelled final labelled_trace ret_trace ⇒
-    let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in
-    let return_cost ≝ flatten_trace_label_return … ret_trace in
-        labelled_cost @ return_cost
-  ].
-  [2:
-    cases abs -abs #abs @abs %
-  |1:
-    %{(as_pc_of … initial)} whd in match label;
-    change with (as_label ?? = ?)
-    generalize in match labelled_proof; whd in ⊢ (% → ?);
-    cases (as_label S initial)
-    [1:
-      #absurd @⊥ cases absurd -absurd #absurd @absurd %
-    |2:
-      #costlabel normalize nodelta #_ %
-    ]
-  ]
-qed.
+    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
+    let return_cost ≝ observables_trace_label_return … ret_trace curr in
+        labelled_cost @@ return_cost
+  ]. % qed.
+  
+let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
+match l with
+[ nil ⇒ [ ]
+| cons hd tl ⇒
+  match f hd with
+  [ Some y ⇒ [ y ]
+  | None ⇒ [ ]
+  ] @ filter_map … f tl
+].
+
+lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
+#X #Y #f #l elim l normalize // qed.
+
+lemma filter_map_compose : ∀X,Y,Z,f,g,l.
+filter_map Y Z f (filter_map X Y g l) =
+  filter_map X Z (λx.! y ← g x ; f y) l.
+#X #Y #Z #f #g #l elim l [%]
+#hd #tl #IH
+whd in ⊢ (??(????%)%);
+ cases (g ?) normalize nodelta
+ [2: #y >m_return_bind whd in ⊢ (??%?); @eq_f2 [ % ]]
+@IH
+qed.
+
+lemma filter_map_ext_eq : ∀X,Y,f,g,l.
+  (∀x.f x = g x) → filter_map X Y f l = filter_map X Y g l.
+#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
+
+let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
+match l return λl.All X P l → list (Σx.P x) with
+[ nil ⇒ λ_.[ ]
+| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
+].
+
+definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
+λA,P,l.list_distribute_sig_aux … l (pi2 … l).
+
+let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
+match l with
+[ nil ⇒ [[ ]]
+| cons hd tl ⇒ hd ::: list_factor_sig … tl
+].
+
+definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
+λS,l.filter_map (Σev.as_emittable S ev) ?
+  (λev.match ev return λev.as_emittable S ev → option ? with
+    [ IEVcost c ⇒ λprf.Some ? «c, prf»
+    | _ ⇒ λ_.None ?
+    ] (pi2 … ev)) (list_distribute_sig … l).
 
 (* JHM: base case now passes the termination checker *)
-let rec taa_append_tal_same_flatten
+let rec taa_append_tal_same_observables
   S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
-  ∀tal : trace_any_label S fl st2 st3.
-    flatten_trace_any_label … (taa @ tal) =
-      flatten_trace_any_label … tal ≝ ?.
+  ∀tal : trace_any_label S fl st2 st3.∀curr.
+    observables_trace_any_label ???? (taa @ tal) curr =
+      observables_trace_any_label ???? tal curr ≝ ?.
 cases taa -st1 -st2
-[ #st #tal normalize in ⊢ (??%?); //
-| #st_pre #st_init #st2 #H #G #K #taa' #tal
+[ #st #tal #curr normalize in ⊢ (??%?); //
+| #st_pre #st_init #st2 #H #G #K #taa' #tal #curr
   whd in match (? @ ?);
   whd in ⊢ (??%?); //
@@ -803 +885 @@
 qed.
 
-let rec tal_collapsable_flatten S fl st1 st2 tal
+let rec tal_collapsable_observables S fl st1 st2 tal
   on tal :
-  tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝
+  ∀curr.
+  tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ] ≝
+λcurr.
 match tal
-return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ]
+return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ]
 with
 [ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ??
 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
-    tal_collapsable_flatten ???? tail_trace
+  tal_collapsable_observables ???? tail_trace curr
 | _ ⇒ Ⓧ
 ].
 
-let rec tll_rel_to_traces_same_flatten
+let rec tll_rel_to_traces_same_observables
   (S: abstract_status) (S': abstract_status)
     (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
@@ -821 +905 @@
       (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
         (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
+        (curr : ident)
           on the_trace_l:
             tll_rel … the_trace_l the_trace_r →
-              map … (pi1 …) (flatten_trace_label_label … the_trace_l) =
-                map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝
+              pi1 … (observables_trace_label_label … the_trace_l curr) =
+                pi1 … (observables_trace_label_label … the_trace_r curr) ≝
   match the_trace_l with
   [ tll_base fl1 st1 st1' tal1 H ⇒
@@ -831 +916 @@
     ]
   ]
-and tal_rel_to_traces_same_flatten
+and tal_rel_to_traces_same_observables
   (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
     (trace_ends_flag_r: trace_ends_with_ret)
@@ -837 +922 @@
         (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
           (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
+          (curr : ident)
           on the_trace_l:
             tal_rel … the_trace_l the_trace_r →
-              map … (pi1 …) (flatten_trace_any_label … the_trace_l) =
-                map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝
+              pi1 … (observables_trace_any_label … the_trace_l curr) =
+                pi1 … (observables_trace_any_label … the_trace_r curr) ≝
   match the_trace_l with
   [ tal_base_not_return st1 st1' H G K ⇒ ?
@@ -849 +935 @@
   | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
   ]
-and tlr_rel_to_traces_same_flatten
+and tlr_rel_to_traces_same_observables
   (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
     (start_status_r: S') (final_status_r: S')
       (the_trace_l: trace_label_return S start_status_l final_status_l)
         (the_trace_r: trace_label_return S' start_status_r final_status_r)
+        (curr : ident)
         on the_trace_l:
           tlr_rel … the_trace_l the_trace_r →
-            map … (pi1 …) (flatten_trace_label_return … the_trace_l) =
-              map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝
+            pi1 … (observables_trace_label_return … the_trace_l curr) =
+              pi1 … (observables_trace_label_return … the_trace_r curr) ≝
   match the_trace_l with
   [ tlr_base before after tll_l ⇒ ?
   | tlr_step initial labelled final tll_l tlr_l ⇒ ?
   ].  
-[ * whd in match as_label_safe; normalize nodelta
-  @opt_safe_elim #l1 #EQ1
-  @opt_safe_elim #l2 #EQ2
-  #EQ destruct(EQ) #H_tal
-  change with (? :: ? = ? :: ?) lapply H -H lapply G -G
-  whd in match as_costed; normalize nodelta
-  >EQ1 >EQ2 normalize nodelta #_ #_
-  >(tal_rel_to_traces_same_flatten … H_tal) @refl
+[ * #EQ #H_tal
+  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
+  cases (as_label_safe ??) in EQ; #c1 #H1
+  cases (as_label_safe ??) #c2 #H2 #EQ destruct %
 |2,3,4,5,6,7: 
   [1,2,3,4: * #EQ destruct(EQ)]
@@ -881 +964 @@
       [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
       [| *#tl2] ** #EQ #H_tl #H_tlr
-    ] >EQ >taa_append_tal_same_flatten
-  | whd in ⊢ (%→??(????%)?);
-    @tal_rel_to_traces_same_flatten
-  ]
+    ] >EQ >taa_append_tal_same_observables
+  | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
+  ]
+  whd in ⊢ (??%%);
   [1,2: %
-  |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
-  |4,6: <map_append
-    >(tal_collapsable_flatten … H_tl) >append_nil
-    >(tlr_rel_to_traces_same_flatten … H_tlr) %
-  |7: <map_append
-    >(tlr_rel_to_traces_same_flatten … H_tlr)
-    >(tal_rel_to_traces_same_flatten … H_tl)
-    @map_append
+  |3,5: >call >(tlr_rel_to_traces_same_observables … H_tlr) %
+  |4,6: >call >(tal_collapsable_observables … H_tl) >append_nil
+    >(tlr_rel_to_traces_same_observables … H_tlr) %
+  |7: >call
+    >(tlr_rel_to_traces_same_observables … H_tlr)
+    >(tal_rel_to_traces_same_observables … H_tl)
+    %
   ]
 |*: cases the_trace_r
   [1,3: #st_before_r #st_after_r #tll_r
-    [ @tll_rel_to_traces_same_flatten | * ]
+    [ @tll_rel_to_traces_same_observables | * ]
   |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
     #H_tll #H_tlr
-    <map_append
-    >(tll_rel_to_traces_same_flatten … H_tll)
-    >(tlr_rel_to_traces_same_flatten … H_tlr)
-    @map_append
+    whd in ⊢ (??%%);
+    >(tll_rel_to_traces_same_observables … H_tll)
+    >(tlr_rel_to_traces_same_observables … H_tlr)
+    %
   ]
 ]
@@ -910 +992 @@
 (* cost maps specifics: summing over flattened traces *)
 
-lemma lift_cost_map_same_cost_tal :
+(* lemma lift_cost_map_same_cost_tal :
   ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
   ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
@@ -935 +1017 @@
 @(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
 qed.
+*)
+
+lemma map_pi1_distribute_sig : ∀A,P,l.
+  map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
+#A #P * #l elim l -l normalize // qed.
+
+definition flatten_trace_label_return ≝
+  λS,st1,st2.λtlr : trace_label_return S st1 st2.
+  (* as cost events do not depend on current function identifier, we
+     can use a dummy one *)
+  let dummy ≝ an_identifier ? one in
+  costlabels_of_observables … (observables_trace_label_return … tlr dummy).
+
+definition flatten_trace_label_label ≝
+  λS,flag,st1,st2.λtll : trace_label_label S flag st1 st2.
+  (* as cost events do not depend on current function identifier, we
+     can use a dummy one *)
+  let dummy ≝ an_identifier ? one in
+  costlabels_of_observables … (observables_trace_label_label … tll dummy).
 
 lemma lift_cost_map_same_cost_tlr :
@@ -946 +1047 @@
 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
 #tlr_in #tlr_out #H_tlr
-@(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
-qed.
+@lift_cost_map_same_cost
+whd in match flatten_trace_label_return; normalize nodelta
+>map_to_filter_map >map_to_filter_map >filter_map_compose
+>filter_map_compose
+cut (∀S.∀x: (Σev.as_emittable S ev).
+  ! y ←
+    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
+    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
+  Some ? (pi1 ?? y) =
+  ! ev ← Some ? (pi1 ?? x) ;
+  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
+[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
+#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
+<filter_map_compose <filter_map_compose @eq_f
+<map_to_filter_map <map_to_filter_map
+>map_pi1_distribute_sig >map_pi1_distribute_sig
+@(tlr_rel_to_traces_same_observables … H_tlr) %
+qed.
+
+lemma lift_cost_map_same_cost_tll :
+  ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
+  ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
+  ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
+  tll_rel … the_trace_in the_trace_out →
+  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
+    (lift_cost_map_id … dec m_out l)) =
+  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
+#S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
+#tlr_in #tlr_out #H_tlr
+@lift_cost_map_same_cost
+whd in match flatten_trace_label_label; normalize nodelta
+>map_to_filter_map >map_to_filter_map >filter_map_compose
+>filter_map_compose
+cut (∀S.∀x: (Σev.as_emittable S ev).
+  ! y ←
+    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
+    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
+  Some ? (pi1 ?? y) =
+  ! ev ← Some ? (pi1 ?? x) ;
+  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
+[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
+#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
+<filter_map_compose <filter_map_compose @eq_f
+<map_to_filter_map <map_to_filter_map
+>map_pi1_distribute_sig >map_pi1_distribute_sig
+@(tll_rel_to_traces_same_observables … H_tlr) %
+qed.

src/common/stacksize.ma

@@ -1 +1 @@
 include "basics/lists/list.ma".
-include "joint/joint_semantics.ma".
-include "common/Executions.ma".
 include "common/StructuredTraces.ma".
 
-inductive call_ud (p: params) (globals: list ident): Type [0] ≝ 
-  | up: joint_internal_function p globals → call_ud p globals    (* call *)
-  | down: joint_internal_function p globals → call_ud p globals. (* return *)
-  
-let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
-  (curr: nat) (max: nat) on fn_list: nat ≝ 
-  match fn_list with
-  [ nil      ⇒ max
-  | cons h t ⇒ match h with
-    [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
-      if leb max new_stack
-      then max_stacksize … t new_stack new_stack
-      else max_stacksize … t new_stack max
-    | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
-      max_stacksize … t new_stack max
-    ] 
-  ].
+inductive call_ud : Type [0] ≝ 
+  | up: ident → call_ud    (* call *)
+  | down: ident → call_ud. (* return *)
 
-let rec extract_list_from_tlr (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
-  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
-  match tr with
-  [ tlr_base s1 s2 tll        ⇒ 
-    extract_list_from_tll … lg top_f … tll res
-  | tlr_step s1 s2 s3 tll tlr ⇒ 
-    let res' ≝ extract_list_from_tll … lg top_f … tll res in
-    extract_list_from_tlr … lg top_f … tlr res'
-  ]
-and extract_list_from_tll (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
-  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
-  match tr with
-  [ tll_base ends s1 s2 tal co ⇒ 
-    extract_list_from_tal … lg top_f … tal res
-  ]
-and extract_list_from_tal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
-  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 
-  match tr with
-  [ tal_base_not_return s1 s2 ex cl co ⇒ res
-  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
-  | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒
-    extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
-      (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
-  | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒
-     extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr
-      (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res)
-  | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 
-    let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
-      (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
-    extract_list_from_tal … lg top_f … tal res'
-  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
-    extract_list_from_tal … lg top_f … tal res
-  ].
+record stacksize_info : Type[0] ≝
+{ current : ℕ ; maximum : ℕ }.
 
-let rec tlr_rel_extract_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
-  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
-  ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
-  extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ 
-  match t1 with
-  [ tlr_base st1 st1' tll1 ⇒ ?
-  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
-  ]
-and tll_rel_extract_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
-  extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
-  match t1 with
-  [ tll_base ends st1 st1' tal1 co ⇒ ?
-  ]
-and tal_rel_extract_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
-  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
-  match t1 with
-  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
-  | tal_base_return st1 st1' ex cl ⇒ ?
-  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
-  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
-  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
-  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
-  ].
-[ cases t2
-  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
-  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
-  ]
-| cases t2
-  [ #st2 #st2' #tll2 normalize #abs cases abs
-  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
-    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
-    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
-  ]
-| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
-  @(tal_rel_extract_equal … H2)
-| cases t2 
-  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
-  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
-  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
-    #taa * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid *
-    #taa * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
-    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
-    * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 
-      destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
-      cases daemon
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
-  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
-  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
-  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs) 
-  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
-    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
-    * #taa * #H * #G inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize #Hsim destruct (Hsim)
-      cases daemon (* use Hind again? *)  
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
-    * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
-    [ * * #H3 #H2 #H4 | #H2 ]
-    inversion taa in ⊢ ?;
-    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
-    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize in H3; destruct (H3)
-    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
-    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize in H1; destruct (H1)
-    ]
-  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
-  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
-    * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
-    [* #tl2]
-    inversion taa in ⊢ ?;
-    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #abs destruct (abs)
-    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
-      >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
-      >ident_eq %
-    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * #abs destruct (abs)
-    ]
-  | (* tail call case *) cases daemon
-  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
-    * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
-    #K * #tlr2' * #L [* #tl2] 
-    inversion taa in ⊢ ?;
-    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
-      destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq 
-      (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
-       * not sure yet *) cases daemon
-    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
-      >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
-    #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
-    [* #tl2]
-    inversion taa in ⊢ ?;
-    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
-      destruct (H1)
-    |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
-      >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
-    ]
-  ]
-| (* tail call case *) cases daemon 
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
-    #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
-    inversion taa in ⊢ ?;
-    [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
-    |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #H1 destruct (H1)
-    ]
-  | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
-    * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
-    inversion taa in ⊢ ?;
-    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize * * #abs destruct (abs)
-    ]
-  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
-    #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
-    [2: * #tl2]
-    inversion taa in ⊢ ?;
-    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 
-      destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
-      cases tal1 in H2;
-      [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
-      | #ss #sf #ex'' #cl'' normalize #abs cases abs
-      | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
-      | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs
-      | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
-        normalize #abs cases abs
-      | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
-        cases daemon (* use induction here, but no *)
-      ]
-    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #abs destruct (abs)
-    ]
-  | (* tail call case *) cases daemon
-  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
-    normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
-    [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
-    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
-      destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
-      >(tlr_rel_extract_equal … H3) %
-    |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
-    #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
-    [2: * #tl2] inversion taa in ⊢ ?;
-    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
-      >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
-      (* look further here *)
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co'
-  | #ss #fs #ex' #cl'
-  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
-  | #st2p #st2s #st2' #ex' #cl' #tlr2
-  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' 
-  ]
-  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 
-]
-(* Another tailcall case escaped *) cases daemon
+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.
 
-let rec tlr_rel_max_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
-  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
-  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tlr_base st1 st1' tll1 ⇒ ?
-  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
-  ]
-and tll_rel_max_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tll_base ends st1 st1' tal1 co ⇒ ?
-  ]
-and tal_rel_max_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
-  | tal_base_return st1 st1' ex cl ⇒ ?
-  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
-  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
-  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
-  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
-  ].
-[1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
-|3: #Hsim >(tll_rel_extract_equal … Hsim []) %
-|*: #Hsim >(tal_rel_extract_equal … Hsim []) %
-]
+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.