Changeset 2755


Ignore:
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:
2 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2553 r2755  
    707707
    708708(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    709 
    710 inductive intensional_event : Type[0] ≝
    711 | IEVcost : costlabel → intensional_event
    712 | IEVcall : ident → intensional_event
    713 | IEVtailcall : ident → ident → intensional_event
    714 | IEVret : ident → intensional_event.
    715 
    716709let rec ft_observables_aux acc S st st' stack
    717710  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
  • src/common/StructuredTraces.ma

    r2553 r2755  
    1 include "basics/types.ma".
     1 include "basics/types.ma".
    22include "basics/bool.ma".
    33include "basics/jmeq.ma".
     
    66include "basics/lists/listb.ma".
    77include "ASM/Util.ma".
     8include "common/IO.ma".
     9include "utilities/hide.ma".
    810
    911inductive status_class: Type[0] ≝
     
    1618record abstract_status : Type[1] ≝
    1719  { as_status :> Type[0]
    18   ; as_execute : as_status → as_status → Prop
     20  ; as_eval : as_status → IO io_out io_in as_status
    1921  ; as_pc : DeqSet
    2022  ; as_pc_of : as_status → as_pc
     
    2224  ; as_label_of_pc : as_pc → option costlabel
    2325  ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
    24   ; as_final: as_status → Prop
     26  ; as_result: as_status → option int
    2527  ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
    2628  ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
     
    2931definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
    3032definition as_call ≝ λS,s,f.as_call_ident S s = f.
     33definition as_final ≝ λS,s.as_result S s ≠ None ?.
     34definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2.
    3135
    3236definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
     
    3741definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
    3842  λa_s,st.as_label ? st ≠ None ?.
    39 
    40 definition as_label_safe : ∀a_s : abstract_status.
    41   (Σs : a_s.as_costed ? s) → costlabel ≝
    42   λa_s,st_sig.opt_safe … (pi2 … st_sig).
    4343
    4444lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
     
    6363
    6464definition as_cost_label ≝
    65   λS : abstract_status. Σl.as_cost_labelled S l.
     65  λS : abstract_status. Σl.as_cost_labelled S l.
     66
     67unification hint 0 ≔ S ⊢ as_cost_label S ≡ Sig costlabel (λl.as_cost_labelled S l).
    6668
    6769definition as_cost_labels ≝
     
    7678definition as_cost_map ≝
    7779  λS : abstract_status. (as_cost_label S) → ℕ.
     80 
     81definition as_label_safe : ∀a_s : abstract_status.
     82  (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
     83  λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
     84@hide_prf
     85@opt_safe_elim #c #EQ %{EQ} qed.
    7886 
    7987definition lift_sigma_map_id :
     
    599607    match tll2 with
    600608    [ tll_base fl2 st2 st2 tal2 G ⇒
    601       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
     609      pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
    602610      tal_rel … tal1 tal2
    603611    ]
     
    726734qed.
    727735
    728 let rec flatten_trace_label_label
     736inductive intensional_event : Type[0] ≝
     737| IEVcost : costlabel → intensional_event
     738| IEVcall : ident → intensional_event
     739| IEVtailcall : ident → ident → intensional_event
     740| IEVret : ident → intensional_event.
     741
     742(* NB: we don't restrict call idents, because it would need some more tinkering
     743   with abstract_status *)
     744definition as_emittable : abstract_status → intensional_event → Prop ≝
     745λS,ev.
     746match ev with
     747[ IEVcost c ⇒ as_cost_labelled S c
     748| _ ⇒ True
     749].
     750 
     751definition as_trace ≝
     752λS : abstract_status.
     753Σl : list intensional_event.All … (as_emittable S) l.
     754
     755unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
     756
     757definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
     758λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
     759
     760definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
     761λA,P,l1,l2.«l1@l2,
     762  cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
     763
     764definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
     765
     766interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
     767interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
     768interpretation "safe nil" 'vnil = (nil_safe ??).
     769
     770definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
     771λS,l.«IEVcost l, pi2 … l».
     772
     773let rec observables_trace_label_label
    729774  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    730775    (start_status: S) (final_status: S)
    731776      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    732         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     777      (curr : ident)
     778        on the_trace: as_trace S ≝
    733779  match the_trace with
    734780  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    735       let label ≝
    736         match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
    737         [ None ⇒ λabs. ⊥
    738         | Some l ⇒ λ_. l
    739         ] labelled_proof
    740       in
    741         (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace
    742   ]
    743 and flatten_trace_any_label
     781      let label ≝ as_label_safe … «?, labelled_proof» in
     782      emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
     783  ]
     784and observables_trace_any_label
    744785  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    745786    (start_status: S) (final_status: S)
    746787      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    747         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     788      (curr : ident)
     789        on the_trace: as_trace S ≝
    748790  match the_trace with
    749   [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    750   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    751       flatten_trace_label_return … call_trace
    752   | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    753       flatten_trace_label_return … call_trace
    754   | tal_base_return the_status _ _ _ ⇒ [ ]
     791  [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
     792  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
     793      let id ≝ as_call_ident ? «?, cl» in
     794      IEVcall id ::: observables_trace_label_return ??? call_trace id
     795  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
     796      let id ≝ as_tailcall_ident ? «?, cl» in
     797      IEVtailcall curr id ::: observables_trace_label_return … call_trace id
     798  | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
    755799  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    756     _ _ _ call_trace _ final_trace ⇒
    757     let call_cost_trace ≝ flatten_trace_label_return … call_trace in
    758     let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
    759         call_cost_trace @ final_cost_trace
     800    _ cl _ call_trace _ final_trace ⇒
     801    let id ≝ as_call_ident ? «?, cl» in
     802    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
     803    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
     804    IEVcall id ::: call_cost_trace @@ final_cost_trace
    760805  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    761       flatten_trace_any_label … tail_trace
    762   ]
    763 and flatten_trace_label_return
     806    observables_trace_any_label … tail_trace curr
     807  ]
     808and observables_trace_label_return
    764809  (S: abstract_status)
    765810    (start_status: S) (final_status: S)
    766811      (the_trace: trace_label_return S start_status final_status)
    767         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     812      (curr : ident)
     813        on the_trace: as_trace S ≝
    768814  match the_trace with
    769815  [ tlr_base before after trace_to_lift ⇒
    770       flatten_trace_label_label … trace_to_lift
     816      observables_trace_label_label … trace_to_lift curr
    771817  | tlr_step initial labelled final labelled_trace ret_trace ⇒
    772     let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in
    773     let return_cost ≝ flatten_trace_label_return … ret_trace in
    774         labelled_cost @ return_cost
    775   ].
    776   [2:
    777     cases abs -abs #abs @abs %
    778   |1:
    779     %{(as_pc_of … initial)} whd in match label;
    780     change with (as_label ?? = ?)
    781     generalize in match labelled_proof; whd in ⊢ (% → ?);
    782     cases (as_label S initial)
    783     [1:
    784       #absurd @⊥ cases absurd -absurd #absurd @absurd %
    785     |2:
    786       #costlabel normalize nodelta #_ %
    787     ]
    788   ]
    789 qed.
     818    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
     819    let return_cost ≝ observables_trace_label_return … ret_trace curr in
     820        labelled_cost @@ return_cost
     821  ]. % qed.
     822 
     823let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
     824match l with
     825[ nil ⇒ [ ]
     826| cons hd tl ⇒
     827  match f hd with
     828  [ Some y ⇒ [ y ]
     829  | None ⇒ [ ]
     830  ] @ filter_map … f tl
     831].
     832
     833lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
     834#X #Y #f #l elim l normalize // qed.
     835
     836lemma filter_map_compose : ∀X,Y,Z,f,g,l.
     837filter_map Y Z f (filter_map X Y g l) =
     838  filter_map X Z (λx.! y ← g x ; f y) l.
     839#X #Y #Z #f #g #l elim l [%]
     840#hd #tl #IH
     841whd in ⊢ (??(????%)%);
     842 cases (g ?) normalize nodelta
     843 [2: #y >m_return_bind whd in ⊢ (??%?); @eq_f2 [ % ]]
     844@IH
     845qed.
     846
     847lemma filter_map_ext_eq : ∀X,Y,f,g,l.
     848  (∀x.f x = g x) → filter_map X Y f l = filter_map X Y g l.
     849#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
     850
     851let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
     852match l return λl.All X P l → list (Σx.P x) with
     853[ nil ⇒ λ_.[ ]
     854| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
     855].
     856
     857definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
     858λA,P,l.list_distribute_sig_aux … l (pi2 … l).
     859
     860let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
     861match l with
     862[ nil ⇒ [[ ]]
     863| cons hd tl ⇒ hd ::: list_factor_sig … tl
     864].
     865
     866definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
     867λS,l.filter_map (Σev.as_emittable S ev) ?
     868  (λev.match ev return λev.as_emittable S ev → option ? with
     869    [ IEVcost c ⇒ λprf.Some ? «c, prf»
     870    | _ ⇒ λ_.None ?
     871    ] (pi2 … ev)) (list_distribute_sig … l).
    790872
    791873(* JHM: base case now passes the termination checker *)
    792 let rec taa_append_tal_same_flatten
     874let rec taa_append_tal_same_observables
    793875  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
    794   ∀tal : trace_any_label S fl st2 st3.
    795     flatten_trace_any_label … (taa @ tal) =
    796       flatten_trace_any_label … tal ≝ ?.
     876  ∀tal : trace_any_label S fl st2 st3.∀curr.
     877    observables_trace_any_label ???? (taa @ tal) curr =
     878      observables_trace_any_label ???? tal curr ≝ ?.
    797879cases taa -st1 -st2
    798 [ #st #tal normalize in ⊢ (??%?); //
    799 | #st_pre #st_init #st2 #H #G #K #taa' #tal
     880[ #st #tal #curr normalize in ⊢ (??%?); //
     881| #st_pre #st_init #st2 #H #G #K #taa' #tal #curr
    800882  whd in match (? @ ?);
    801883  whd in ⊢ (??%?); //
     
    803885qed.
    804886
    805 let rec tal_collapsable_flatten S fl st1 st2 tal
     887let rec tal_collapsable_observables S fl st1 st2 tal
    806888  on tal :
    807   tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝
     889  ∀curr.
     890  tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ] ≝
     891λcurr.
    808892match tal
    809 return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ]
     893return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ]
    810894with
    811895[ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ??
    812896| tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    813     tal_collapsable_flatten ???? tail_trace
     897  tal_collapsable_observables ???? tail_trace curr
    814898| _ ⇒ Ⓧ
    815899].
    816900
    817 let rec tll_rel_to_traces_same_flatten
     901let rec tll_rel_to_traces_same_observables
    818902  (S: abstract_status) (S': abstract_status)
    819903    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
     
    821905      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
    822906        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
     907        (curr : ident)
    823908          on the_trace_l:
    824909            tll_rel … the_trace_l the_trace_r →
    825               map … (pi1 …) (flatten_trace_label_label … the_trace_l) =
    826                 map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝
     910              pi1 … (observables_trace_label_label … the_trace_l curr) =
     911                pi1 … (observables_trace_label_label … the_trace_r curr) ≝
    827912  match the_trace_l with
    828913  [ tll_base fl1 st1 st1' tal1 H ⇒
     
    831916    ]
    832917  ]
    833 and tal_rel_to_traces_same_flatten
     918and tal_rel_to_traces_same_observables
    834919  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
    835920    (trace_ends_flag_r: trace_ends_with_ret)
     
    837922        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
    838923          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
     924          (curr : ident)
    839925          on the_trace_l:
    840926            tal_rel … the_trace_l the_trace_r →
    841               map … (pi1 …) (flatten_trace_any_label … the_trace_l) =
    842                 map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝
     927              pi1 … (observables_trace_any_label … the_trace_l curr) =
     928                pi1 … (observables_trace_any_label … the_trace_r curr) ≝
    843929  match the_trace_l with
    844930  [ tal_base_not_return st1 st1' H G K ⇒ ?
     
    849935  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
    850936  ]
    851 and tlr_rel_to_traces_same_flatten
     937and tlr_rel_to_traces_same_observables
    852938  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
    853939    (start_status_r: S') (final_status_r: S')
    854940      (the_trace_l: trace_label_return S start_status_l final_status_l)
    855941        (the_trace_r: trace_label_return S' start_status_r final_status_r)
     942        (curr : ident)
    856943        on the_trace_l:
    857944          tlr_rel … the_trace_l the_trace_r →
    858             map … (pi1 …) (flatten_trace_label_return … the_trace_l) =
    859               map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝
     945            pi1 … (observables_trace_label_return … the_trace_l curr) =
     946              pi1 … (observables_trace_label_return … the_trace_r curr) ≝
    860947  match the_trace_l with
    861948  [ tlr_base before after tll_l ⇒ ?
    862949  | tlr_step initial labelled final tll_l tlr_l ⇒ ?
    863950  ]. 
    864 [ * whd in match as_label_safe; normalize nodelta
    865   @opt_safe_elim #l1 #EQ1
    866   @opt_safe_elim #l2 #EQ2
    867   #EQ destruct(EQ) #H_tal
    868   change with (? :: ? = ? :: ?) lapply H -H lapply G -G
    869   whd in match as_costed; normalize nodelta
    870   >EQ1 >EQ2 normalize nodelta #_ #_
    871   >(tal_rel_to_traces_same_flatten … H_tal) @refl
     951[ * #EQ #H_tal
     952  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
     953  cases (as_label_safe ??) in EQ; #c1 #H1
     954  cases (as_label_safe ??) #c2 #H2 #EQ destruct %
    872955|2,3,4,5,6,7:
    873956  [1,2,3,4: * #EQ destruct(EQ)]
     
    881964      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
    882965      [| *#tl2] ** #EQ #H_tl #H_tlr
    883     ] >EQ >taa_append_tal_same_flatten
    884   | whd in ⊢ (%→??(????%)?);
    885     @tal_rel_to_traces_same_flatten
    886   ]
     966    ] >EQ >taa_append_tal_same_observables
     967  | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
     968  ]
     969  whd in ⊢ (??%%);
    887970  [1,2: %
    888   |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
    889   |4,6: <map_append
    890     >(tal_collapsable_flatten … H_tl) >append_nil
    891     >(tlr_rel_to_traces_same_flatten … H_tlr) %
    892   |7: <map_append
    893     >(tlr_rel_to_traces_same_flatten … H_tlr)
    894     >(tal_rel_to_traces_same_flatten … H_tl)
    895     @map_append
     971  |3,5: >call >(tlr_rel_to_traces_same_observables … H_tlr) %
     972  |4,6: >call >(tal_collapsable_observables … H_tl) >append_nil
     973    >(tlr_rel_to_traces_same_observables … H_tlr) %
     974  |7: >call
     975    >(tlr_rel_to_traces_same_observables … H_tlr)
     976    >(tal_rel_to_traces_same_observables … H_tl)
     977    %
    896978  ]
    897979|*: cases the_trace_r
    898980  [1,3: #st_before_r #st_after_r #tll_r
    899     [ @tll_rel_to_traces_same_flatten | * ]
     981    [ @tll_rel_to_traces_same_observables | * ]
    900982  |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
    901983    #H_tll #H_tlr
    902     <map_append
    903     >(tll_rel_to_traces_same_flatten … H_tll)
    904     >(tlr_rel_to_traces_same_flatten … H_tlr)
    905     @map_append
     984    whd in ⊢ (??%%);
     985    >(tll_rel_to_traces_same_observables … H_tll)
     986    >(tlr_rel_to_traces_same_observables … H_tlr)
     987    %
    906988  ]
    907989]
     
    910992(* cost maps specifics: summing over flattened traces *)
    911993
    912 lemma lift_cost_map_same_cost_tal :
     994(* lemma lift_cost_map_same_cost_tal :
    913995  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
    914996  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
     
    9351017@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
    9361018qed.
     1019*)
     1020
     1021lemma map_pi1_distribute_sig : ∀A,P,l.
     1022  map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
     1023#A #P * #l elim l -l normalize // qed.
     1024
     1025definition flatten_trace_label_return ≝
     1026  λS,st1,st2.λtlr : trace_label_return S st1 st2.
     1027  (* as cost events do not depend on current function identifier, we
     1028     can use a dummy one *)
     1029  let dummy ≝ an_identifier ? one in
     1030  costlabels_of_observables … (observables_trace_label_return … tlr dummy).
     1031
     1032definition flatten_trace_label_label ≝
     1033  λS,flag,st1,st2.λtll : trace_label_label S flag st1 st2.
     1034  (* as cost events do not depend on current function identifier, we
     1035     can use a dummy one *)
     1036  let dummy ≝ an_identifier ? one in
     1037  costlabels_of_observables … (observables_trace_label_label … tll dummy).
    9371038
    9381039lemma lift_cost_map_same_cost_tlr :
     
    9461047#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    9471048#tlr_in #tlr_out #H_tlr
    948 @(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
    949 qed.
     1049@lift_cost_map_same_cost
     1050whd in match flatten_trace_label_return; normalize nodelta
     1051>map_to_filter_map >map_to_filter_map >filter_map_compose
     1052>filter_map_compose
     1053cut (∀S.∀x: (Σev.as_emittable S ev).
     1054  ! y ←
     1055    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
     1056    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
     1057  Some ? (pi1 ?? y) =
     1058  ! ev ← Some ? (pi1 ?? x) ;
     1059  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
     1060[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
     1061#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
     1062<filter_map_compose <filter_map_compose @eq_f
     1063<map_to_filter_map <map_to_filter_map
     1064>map_pi1_distribute_sig >map_pi1_distribute_sig
     1065@(tlr_rel_to_traces_same_observables … H_tlr) %
     1066qed.
     1067
     1068lemma lift_cost_map_same_cost_tll :
     1069  ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
     1070  ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
     1071  ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
     1072  tll_rel … the_trace_in the_trace_out →
     1073  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
     1074    (lift_cost_map_id … dec m_out l)) =
     1075  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
     1076#S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
     1077#tlr_in #tlr_out #H_tlr
     1078@lift_cost_map_same_cost
     1079whd in match flatten_trace_label_label; normalize nodelta
     1080>map_to_filter_map >map_to_filter_map >filter_map_compose
     1081>filter_map_compose
     1082cut (∀S.∀x: (Σev.as_emittable S ev).
     1083  ! y ←
     1084    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
     1085    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
     1086  Some ? (pi1 ?? y) =
     1087  ! ev ← Some ? (pi1 ?? x) ;
     1088  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
     1089[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
     1090#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
     1091<filter_map_compose <filter_map_compose @eq_f
     1092<map_to_filter_map <map_to_filter_map
     1093>map_pi1_distribute_sig >map_pi1_distribute_sig
     1094@(tll_rel_to_traces_same_observables … H_tlr) %
     1095qed.
  • src/common/stacksize.ma

    r2747 r2755  
    11include "basics/lists/list.ma".
    2 include "joint/joint_semantics.ma".
    3 include "common/Executions.ma".
    42include "common/StructuredTraces.ma".
    53
    6 inductive call_ud (p: params) (globals: list ident): Type [0] ≝
    7   | up: joint_internal_function p globals → call_ud p globals    (* call *)
    8   | down: joint_internal_function p globals → call_ud p globals. (* return *)
    9  
    10 let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
    11   (curr: nat) (max: nat) on fn_list: nat ≝
    12   match fn_list with
    13   [ nil      ⇒ max
    14   | cons h t ⇒ match h with
    15     [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
    16       if leb max new_stack
    17       then max_stacksize … t new_stack new_stack
    18       else max_stacksize … t new_stack max
    19     | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
    20       max_stacksize … t new_stack max
    21     ]
    22   ].
     4inductive call_ud : Type [0] ≝
     5  | up: ident → call_ud    (* call *)
     6  | down: ident → call_ud. (* return *)
    237
    24 let rec extract_list_from_tlr (p: params) (g: list ident)
    25   (lg: ident → joint_internal_function p g) (top_f: ident)
    26   (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
    27   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    28   match tr with
    29   [ tlr_base s1 s2 tll        ⇒
    30     extract_list_from_tll … lg top_f … tll res
    31   | tlr_step s1 s2 s3 tll tlr ⇒
    32     let res' ≝ extract_list_from_tll … lg top_f … tll res in
    33     extract_list_from_tlr … lg top_f … tlr res'
    34   ]
    35 and extract_list_from_tll (p: params) (g: list ident)
    36   (lg: ident → joint_internal_function p g) (top_f: ident)
    37   (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
    38   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    39   match tr with
    40   [ tll_base ends s1 s2 tal co ⇒
    41     extract_list_from_tal … lg top_f … tal res
    42   ]
    43 and extract_list_from_tal (p: params) (g: list ident)
    44   (lg: ident → joint_internal_function p g) (top_f: ident)
    45   (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
    46   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    47   match tr with
    48   [ tal_base_not_return s1 s2 ex cl co ⇒ res
    49   | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
    50   | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒
    51     extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
    52       (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
    53   | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒
    54      extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr
    55       (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res)
    56   | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒
    57     let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
    58       (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
    59     extract_list_from_tal … lg top_f … tal res'
    60   | tal_step_default end s1p s1i s1e ex tal cl co ⇒
    61     extract_list_from_tal … lg top_f … tal res
    62   ].
     8record stacksize_info : Type[0] ≝
     9{ current : ℕ ; maximum : ℕ }.
    6310
    64 let rec tlr_rel_extract_equal (p: params) (g: list ident)
    65   (lg: ident → joint_internal_function p g) (top_f: ident)
    66   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    67   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    68   ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
    69   extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝
    70   match t1 with
    71   [ tlr_base st1 st1' tll1 ⇒ ?
    72   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    73   ]
    74 and tll_rel_extract_equal (p: params) (g: list ident)
    75   (lg: ident → joint_internal_function p g) (top_f: ident)
    76   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    77   t1 ≈ t2 →
    78   ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
    79   extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
    80   match t1 with
    81   [ tll_base ends st1 st1' tal1 co ⇒ ?
    82   ]
    83 and tal_rel_extract_equal (p: params) (g: list ident)
    84   (lg: ident → joint_internal_function p g) (top_f: ident)
    85   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    86   t1 ≈ t2 →
    87   ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
    88   extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
    89   match t1 with
    90   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    91   | tal_base_return st1 st1' ex cl ⇒ ?
    92   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
    93   | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    94   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    95   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    96   ].
    97 [ cases t2
    98   [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
    99   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
    100   ]
    101 | cases t2
    102   [ #st2 #st2' #tll2 normalize #abs cases abs
    103   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    104     >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    105     @(tlr_rel_extract_equal … (proj2 ?? Hsim))
    106   ]
    107 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
    108   @(tal_rel_extract_equal … H2)
    109 | cases t2
    110   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
    111   | #st2 #st2' #ex' #cl' * #abs destruct (abs)
    112   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    113     #taa * #H * #G * #K inversion taa in ⊢ ?;
    114     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    115     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    116       normalize #abs destruct (abs)
    117     ]
    118   | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid *
    119     #taa * #H * #G * #K inversion taa in ⊢ ?;
    120     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    121     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    122       normalize #abs destruct (abs)
    123     ]
    124   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
    125     #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    126     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    127     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    128       normalize #abs destruct (abs)
    129     ]
    130   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    131     * #H * #G * #K inversion taa in ⊢ ?;
    132     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    133     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    134       destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
    135       cases daemon
    136     ]
    137   ]
    138 | cases t2
    139   [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
    140   | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    141   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
    142   | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs)
    143   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    144     normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    145     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    146     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    147       normalize #abs destruct (abs)
    148     ]
    149   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    150     * #taa * #H * #G inversion taa in ⊢ ?;
    151     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    152     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    153       destruct normalize #Hsim destruct (Hsim)
    154       cases daemon (* use Hind again? *) 
    155     ]
    156   ]
    157 | cases t2
    158   [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
    159     * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
    160     [ * * #H3 #H2 #H4 | #H2 ]
    161     inversion taa in ⊢ ?;
    162     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
    163     | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    164       normalize in H3; destruct (H3)
    165     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    166     | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    167       normalize in H1; destruct (H1)
    168     ]
    169   | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
    170   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
    171     * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
    172     [* #tl2]
    173     inversion taa in ⊢ ?;
    174     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    175     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    176       destruct normalize * * #abs destruct (abs)
    177     | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
    178       >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
    179       >ident_eq %
    180     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    181       destruct normalize * #abs destruct (abs)
    182     ]
    183   | (* tail call case *) cases daemon
    184   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
    185     * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
    186     #K * #tlr2' * #L [* #tl2]
    187     inversion taa in ⊢ ?;
    188     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
    189       destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq
    190       (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
    191        * not sure yet *) cases daemon
    192     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    193       destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
    194       >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
    195     ]
    196   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    197     #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
    198     [* #tl2]
    199     inversion taa in ⊢ ?;
    200     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
    201       destruct (H1)
    202     |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    203       destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
    204       >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
    205     ]
    206   ]
    207 | (* tail call case *) cases daemon
    208 | cases t2
    209   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
    210     #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
    211     inversion taa in ⊢ ?;
    212     [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
    213     |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    214       destruct normalize * * #H1 destruct (H1)
    215     ]
    216   | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
    217     * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
    218     inversion taa in ⊢ ?;
    219     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    220     | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    221       normalize * * #abs destruct (abs)
    222     ]
    223   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
    224     #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
    225     [2: * #tl2]
    226     inversion taa in ⊢ ?;
    227     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    228       destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
    229       cases tal1 in H2;
    230       [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
    231       | #ss #sf #ex'' #cl'' normalize #abs cases abs
    232       | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
    233       | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs
    234       | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
    235         normalize #abs cases abs
    236       | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
    237         cases daemon (* use induction here, but no *)
    238       ]
    239     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    240       destruct normalize * * #abs destruct (abs)
    241     ]
    242   | (* tail call case *) cases daemon
    243   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    244     normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
    245     [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
    246     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    247       destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
    248       >(tlr_rel_extract_equal … H3) %
    249     |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    250       destruct normalize * * #abs destruct (abs)
    251     ]
    252   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
    253     #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
    254     [2: * #tl2] inversion taa in ⊢ ?;
    255     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    256     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    257       destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
    258       >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
    259       (* look further here *)
    260     ]
    261   ]
    262 | cases t2
    263   [ #st2 #st2' #ex' #cl' #co'
    264   | #ss #fs #ex' #cl'
    265   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
    266   | #st2p #st2s #st2' #ex' #cl' #tlr2
    267   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    268   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co'
    269   ]
    270   normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    271 ]
    272 (* Another tailcall case escaped *) cases daemon
     11definition update_stacksize_info :
     12  (ident → option ℕ) → stacksize_info → list call_ud → stacksize_info ≝
     13  λstacksizes.
     14  let get_stacksize ≝
     15    λf.match stacksizes f with
     16      [ Some n ⇒ n | None ⇒ 0 (* should never happen *) ] in
     17  let f ≝ λud,acc.
     18    match ud with
     19    [ up i ⇒
     20      let new_stack ≝ get_stacksize i + current acc in
     21      let new_max ≝ max (maximum acc) new_stack in
     22      mk_stacksize_info new_stack new_max
     23    | down i ⇒
     24      let new_stack ≝ current acc - get_stacksize i in
     25      mk_stacksize_info new_stack (maximum acc)
     26    ] in
     27  foldr ?? f.
     28
     29definition extract_call_ud_from_observables :
     30  list intensional_event → list call_ud ≝
     31let f ≝ λev.match ev with
     32[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
     33foldr ?? (λev.append ? (f ev)) [ ].
     34
     35definition extract_call_ud_from_tlr :
     36  ∀S,st1,st2.trace_label_return S st1 st2 → ident → list call_ud ≝
     37λS,st1,st2,tlr,curr.
     38  extract_call_ud_from_observables … (observables_trace_label_return … tlr curr).
     39
     40definition extract_call_ud_from_tll :
     41  ∀S,fl,st1,st2.trace_label_label fl S st1 st2 → ident → list call_ud ≝
     42λS,fl,st1,st2,tll,curr.
     43  extract_call_ud_from_observables … (observables_trace_label_label … tll curr).
     44
     45lemma tlr_rel_same_stacksize_info :
     46  ∀stacksizes.
     47  ∀S1,S2,s1,s1',s2,s2'.
     48  ∀tlr1 : trace_label_return S1 s1 s1'.
     49  ∀tlr2 : trace_label_return S2 s2 s2'.
     50  ∀curr.∀curr_stacksize.
     51  tlr_rel … tlr1 tlr2 →
     52  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr1 curr) =
     53  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr2 curr).
     54#stacksizes #S1 #S2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
     55#equiv @eq_f whd in ⊢ (??%%); @eq_f
     56@tlr_rel_to_traces_same_observables assumption
    27357qed.
    27458
    275 let rec tlr_rel_max_equal (p: params) (g: list ident)
    276   (lg: ident → joint_internal_function p g) (top_f: ident)
    277   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    278   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    279   max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
    280   max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
    281   match t1 with
    282   [ tlr_base st1 st1' tll1 ⇒ ?
    283   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    284   ]
    285 and tll_rel_max_equal (p: params) (g: list ident)
    286   (lg: ident → joint_internal_function p g) (top_f: ident)
    287   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    288   t1 ≈ t2 →
    289   max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
    290   max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
    291   match t1 with
    292   [ tll_base ends st1 st1' tal1 co ⇒ ?
    293   ]
    294 and tal_rel_max_equal (p: params) (g: list ident)
    295   (lg: ident → joint_internal_function p g) (top_f: ident)
    296   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    297   t1 ≈ t2 →
    298   max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
    299   max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    300   match t1 with
    301   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    302   | tal_base_return st1 st1' ex cl ⇒ ?
    303   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
    304   | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    305   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    306   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    307   ].
    308 [1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
    309 |3: #Hsim >(tll_rel_extract_equal … Hsim []) %
    310 |*: #Hsim >(tal_rel_extract_equal … Hsim []) %
    311 ]
     59lemma tll_rel_same_stacksize_info :
     60  ∀stacksizes.
     61  ∀S1,S2,fl1,fl2,s1,s1',s2,s2'.
     62  ∀tll1 : trace_label_label S1 fl1 s1 s1'.
     63  ∀tll2 : trace_label_label S2 fl2 s2 s2'.
     64  ∀curr.∀curr_stacksize.
     65  tll_rel … tll1 tll2 →
     66  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll1 curr) =
     67  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll2 curr).
     68#stacksizes #S1 #S2 #fl1 #fl2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
     69#equiv @eq_f whd in ⊢ (??%%); @eq_f
     70@tll_rel_to_traces_same_observables assumption
    31271qed.
Note: See TracChangeset for help on using the changeset viewer.