 Timestamp:
 Mar 1, 2013, 11:06:29 AM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
 1 moved
Legend:
 Unmodified
 Added
 Removed

src/common/StatusSimulation.ma
r2553 r2755 707 707 708 708 (* 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_event712  IEVcall : ident → intensional_event713  IEVtailcall : ident → ident → intensional_event714  IEVret : ident → intensional_event.715 716 709 let rec ft_observables_aux acc S st st' stack 717 710 (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". 2 2 include "basics/bool.ma". 3 3 include "basics/jmeq.ma". … … 6 6 include "basics/lists/listb.ma". 7 7 include "ASM/Util.ma". 8 include "common/IO.ma". 9 include "utilities/hide.ma". 8 10 9 11 inductive status_class: Type[0] ≝ … … 16 18 record abstract_status : Type[1] ≝ 17 19 { as_status :> Type[0] 18 ; as_e xecute : as_status → as_status → Prop20 ; as_eval : as_status → IO io_out io_in as_status 19 21 ; as_pc : DeqSet 20 22 ; as_pc_of : as_status → as_pc … … 22 24 ; as_label_of_pc : as_pc → option costlabel 23 25 ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop 24 ; as_ final: as_status → Prop26 ; as_result: as_status → option int 25 27 ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident 26 28 ; 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. 30 32 definition as_call ≝ λS,s,f.as_call_ident S s = f. 33 definition as_final ≝ λS,s.as_result S s ≠ None ?. 34 definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2. 31 35 32 36 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 ≝ 38 42 λ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).43 43 44 44 lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s). … … 63 63 64 64 definition as_cost_label ≝ 65 λS : abstract_status. Σl.as_cost_labelled S l. 65 λS : abstract_status. Σl.as_cost_labelled S l. 66 67 unification hint 0 ≔ S ⊢ as_cost_label S ≡ Sig costlabel (λl.as_cost_labelled S l). 66 68 67 69 definition as_cost_labels ≝ … … 76 78 definition as_cost_map ≝ 77 79 λS : abstract_status. (as_cost_label S) → ℕ. 80 81 definition 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. 78 86 79 87 definition lift_sigma_map_id : … … 599 607 match tll2 with 600 608 [ 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»)) ∧ 602 610 tal_rel … tal1 tal2 603 611 ] … … 726 734 qed. 727 735 728 let rec flatten_trace_label_label 736 inductive 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 *) 744 definition as_emittable : abstract_status → intensional_event → Prop ≝ 745 λS,ev. 746 match ev with 747 [ IEVcost c ⇒ as_cost_labelled S c 748  _ ⇒ True 749 ]. 750 751 definition as_trace ≝ 752 λS : abstract_status. 753 Σl : list intensional_event.All … (as_emittable S) l. 754 755 unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l). 756 757 definition 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 760 definition 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 764 definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I». 765 766 interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl). 767 interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2). 768 interpretation "safe nil" 'vnil = (nil_safe ??). 769 770 definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝ 771 λS,l.«IEVcost l, pi2 … l». 772 773 let rec observables_trace_label_label 729 774 (S: abstract_status) (trace_ends_flag: trace_ends_with_ret) 730 775 (start_status: S) (final_status: S) 731 776 (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 ≝ 733 779 match the_trace with 734 780 [ 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 ] 784 and observables_trace_any_label 744 785 (S: abstract_status) (trace_ends_flag: trace_ends_with_ret) 745 786 (start_status: S) (final_status: S) 746 787 (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 ≝ 748 790 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]] 755 799  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 760 805  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 761 flatten_trace_any_label … tail_trace762 ] 763 and flatten_trace_label_return806 observables_trace_any_label … tail_trace curr 807 ] 808 and observables_trace_label_return 764 809 (S: abstract_status) 765 810 (start_status: S) (final_status: S) 766 811 (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 ≝ 768 814 match the_trace with 769 815 [ tlr_base before after trace_to_lift ⇒ 770 flatten_trace_label_label … trace_to_lift816 observables_trace_label_label … trace_to_lift curr 771 817  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 823 let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝ 824 match 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 833 lemma 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 836 lemma filter_map_compose : ∀X,Y,Z,f,g,l. 837 filter_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 841 whd in ⊢ (??(????%)%); 842 cases (g ?) normalize nodelta 843 [2: #y >m_return_bind whd in ⊢ (??%?); @eq_f2 [ % ]] 844 @IH 845 qed. 846 847 lemma 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 851 let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝ 852 match 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 857 definition 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 860 let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝ 861 match l with 862 [ nil ⇒ [[ ]] 863  cons hd tl ⇒ hd ::: list_factor_sig … tl 864 ]. 865 866 definition 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). 790 872 791 873 (* JHM: base case now passes the termination checker *) 792 let rec taa_append_tal_same_ flatten874 let rec taa_append_tal_same_observables 793 875 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 ≝ ?. 797 879 cases 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 800 882 whd in match (? @ ?); 801 883 whd in ⊢ (??%?); // … … 803 885 qed. 804 886 805 let rec tal_collapsable_ flattenS fl st1 st2 tal887 let rec tal_collapsable_observables S fl st1 st2 tal 806 888 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. 808 892 match tal 809 return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal= [ ]893 return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ] 810 894 with 811 895 [ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ?? 812 896  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 813 tal_collapsable_flatten ???? tail_trace897 tal_collapsable_observables ???? tail_trace curr 814 898  _ ⇒ Ⓧ 815 899 ]. 816 900 817 let rec tll_rel_to_traces_same_ flatten901 let rec tll_rel_to_traces_same_observables 818 902 (S: abstract_status) (S': abstract_status) 819 903 (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) 822 906 (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r) 907 (curr : ident) 823 908 on the_trace_l: 824 909 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) ≝ 827 912 match the_trace_l with 828 913 [ tll_base fl1 st1 st1' tal1 H ⇒ … … 831 916 ] 832 917 ] 833 and tal_rel_to_traces_same_ flatten918 and tal_rel_to_traces_same_observables 834 919 (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret) 835 920 (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) 838 923 (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r) 924 (curr : ident) 839 925 on the_trace_l: 840 926 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) ≝ 843 929 match the_trace_l with 844 930 [ tal_base_not_return st1 st1' H G K ⇒ ? … … 849 935  tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ? 850 936 ] 851 and tlr_rel_to_traces_same_ flatten937 and tlr_rel_to_traces_same_observables 852 938 (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S) 853 939 (start_status_r: S') (final_status_r: S') 854 940 (the_trace_l: trace_label_return S start_status_l final_status_l) 855 941 (the_trace_r: trace_label_return S' start_status_r final_status_r) 942 (curr : ident) 856 943 on the_trace_l: 857 944 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) ≝ 860 947 match the_trace_l with 861 948 [ tlr_base before after tll_l ⇒ ? 862 949  tlr_step initial labelled final tll_l tlr_l ⇒ ? 863 950 ]. 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 % 872 955 2,3,4,5,6,7: 873 956 [1,2,3,4: * #EQ destruct(EQ)] … … 881 964 [*#fl_EQ destruct(fl_EQ) * #st2_mid ] *#K' *#tlr2 *#L' 882 965 [ *#tl2] ** #EQ #H_tl #H_tlr 883 ] >EQ >taa_append_tal_same_ flatten884  whd in ⊢ (%→??(??? ?%)?);885 @tal_rel_to_traces_same_flatten886 ]966 ] >EQ >taa_append_tal_same_observables 967  whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables 968 ] 969 whd in ⊢ (??%%); 887 970 [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 % 896 978 ] 897 979 *: cases the_trace_r 898 980 [1,3: #st_before_r #st_after_r #tll_r 899 [ @tll_rel_to_traces_same_ flatten * ]981 [ @tll_rel_to_traces_same_observables  * ] 900 982 *: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r * 901 983 #H_tll #H_tlr 902 <map_append903 >(tll_rel_to_traces_same_ flatten… H_tll)904 >(tlr_rel_to_traces_same_ flatten… H_tlr)905 @map_append984 whd in ⊢ (??%%); 985 >(tll_rel_to_traces_same_observables … H_tll) 986 >(tlr_rel_to_traces_same_observables … H_tlr) 987 % 906 988 ] 907 989 ] … … 910 992 (* cost maps specifics: summing over flattened traces *) 911 993 912 lemma lift_cost_map_same_cost_tal :994 (* lemma lift_cost_map_same_cost_tal : 913 995 ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. 914 996 ∀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)) 936 1018 qed. 1019 *) 1020 1021 lemma 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 1025 definition 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 1032 definition 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). 937 1038 938 1039 lemma lift_cost_map_same_cost_tlr : … … 946 1047 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out 947 1048 #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 1050 whd in match flatten_trace_label_return; normalize nodelta 1051 >map_to_filter_map >map_to_filter_map >filter_map_compose 1052 >filter_map_compose 1053 cut (∀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) % 1066 qed. 1067 1068 lemma 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 1079 whd in match flatten_trace_label_label; normalize nodelta 1080 >map_to_filter_map >map_to_filter_map >filter_map_compose 1081 >filter_map_compose 1082 cut (∀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) % 1095 qed. 
src/common/stacksize.ma
r2747 r2755 1 1 include "basics/lists/list.ma". 2 include "joint/joint_semantics.ma".3 include "common/Executions.ma".4 2 include "common/StructuredTraces.ma". 5 3 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 ]. 4 inductive call_ud : Type [0] ≝ 5  up: ident → call_ud (* call *) 6  down: ident → call_ud. (* return *) 23 7 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 ]. 8 record stacksize_info : Type[0] ≝ 9 { current : ℕ ; maximum : ℕ }. 63 10 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 11 definition 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 29 definition extract_call_ud_from_observables : 30 list intensional_event → list call_ud ≝ 31 let f ≝ λev.match ev with 32 [ IEVcall i ⇒ [up i]  IEVtailcall i j ⇒ [down i; up j]  IEVret i ⇒ [down i]  _ ⇒ [ ]] in 33 foldr ?? (λev.append ? (f ev)) [ ]. 34 35 definition 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 40 definition 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 45 lemma 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 273 57 qed. 274 58 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 ] 59 lemma 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 312 71 qed.
Note: See TracChangeset
for help on using the changeset viewer.