Changeset 3493
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3492 r3493 1 include "costs.ma".1 include "costs.ma". 2 2 include "basics/lists/list.ma". 3 3 include "../src/utilities/option.ma". … … 460 460 definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. 461 461 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p)) 462 (λs.match s with [ STATE st ⇒ ! x ← fetch_state p p' prog st; Some ? (Some ? x) 462 (λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then 463 Some ? (None ?) 464 else ! x ← fetch_state p p' prog st; Some ? (Some ? x) 463 465  INITIAL ⇒ Some ? (None ?) 464 466  FINAL ⇒ None ? ]) instr_m. … … 856 858 qed. 857 859 860 definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ 861 λa.match a with 862 [ call_act f l ⇒ [a_call l] 863  ret_act opt_l ⇒ match opt_l with [None ⇒ [ ]  Some l ⇒ [a_return_post l]] 864  cost_act opt_l ⇒ match opt_l with [None ⇒ [ ]  Some l ⇒ [a_non_functional_label l]] 865 ]. 866 867 lemma get_cost_label_of_trace_tind : ∀S : abstract_status. 868 ∀st1,st2,st3 : S.∀l,prf,t. 869 get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) = 870 actionlabel_to_costlabel l @ get_costlabels_of_trace … t. 871 #S #st1 #st2 #st3 * // qed. 872 873 lemma actionlabel_ok : ∀l : ActionLabel. 874 (is_costlabelled_act l ∨ is_labelled_ret_act l) → ∃c.actionlabel_to_costlabel l = [c]. 875 * /2 by refl, ex_intro/ 876 [ * /2/ ** #x #EQ destruct  * /2/ ** #x #EQ destruct] 877 qed. 878 858 879 lemma static_dynamic : ∀p,p',prog. 859 880 ∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t. … … 880 901 ] 881 902 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct 882 lapply prf1 prf1 lapply l1 l1 elim t1 st3 883 [ * [3: #st] #l #prf * #H1 #H2 #k #_ whd in ⊢ (??%? → ?); 903 * #Hlabelled 904 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 905 [2: >get_cost_label_append >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled) 906 #c #EQc >EQc // 907 ] 908 lapply Hlabelled lapply prf1 prf1 lapply l1 l1 elim t1 st3 909 [ * [3: #st] #l #prf #H1 #H2 #k #_ whd in ⊢ (??%? → ?); 884 910 [3: cases prf 885 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in match (get_costlabels_of_trace ????); 886 whd in match (get_costlabels_of_trace ????); 911 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?); 887 912 lapply(instr_map_ok … good … prf … rel_fin) [ %] cases st2 in prf; st2 [3: #st2] * 888 #EQpc #EQ destruct #H whd in ⊢ (??%% → ?); whd in match (dependent_map ????); 889 #EQ destruct >act_neutral >act_neutral normalize in H; 913 #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H; 890 914 <(act_neutral ?? (act_abs ? abs_t) a1) @H 891 915  @eqb_elim normalize nodelta 892 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels 916 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?); 917 #EQ destruct >act_neutral >act_neutral whd in prf; cases st2 in prf; st2 [3: #st2] 918 normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct 919 #EQ destruct whd in EQc : (??%%); destruct 920 lapply(instr_map_ok … good … good_st_a1) 921 [5: @(FINAL …) 922 2: whd % [ >EQpc @eqb_elim // * #ABS @⊥ @ABS %] % 923  whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption 924 ] 925 #_ normalize nodelta %    whd in ⊢ (% → ?); >act_neutral // 926 ] 927  #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; st2 [3: #st2] #prf 928 normalize nodelta [2:* 3: * #ABS @⊥ lapply ABS ABS @eqb_elim 929 [#EQ #_ @(absurd ? EQ Hpc)  #_ #EQ destruct ] ] * #INUTILE #H4 930 #H cases(bind_inversion ????? H) H * 931 [ #seq * [#lbl1] 932  #newpc 933  #cond #newpc #ltrue #lfalse 934  #lin #io #lout 935  #f 936  937 ] 938 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; 939 normalize nodelta >EQfetch >m_return_bind normalize nodelta 940 cases(asm_is_io ??) normalize nodelta 941 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 942 2,4,8,9,12,14: #H cases(bind_inversion ????? H) H #x * #_ 943 [3: cases x normalize nodelta 944 6: #H cases(bind_inversion ????? H) H #y * #_ 945 ] 946 ] 947 whd in ⊢ (??%% → ?); #EQ destruct 948 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 949 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 950 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r 951 >act_neutral 952 lapply(instr_map_ok … good … good_st_a1) 953 [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta 954 [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state; 955 normalize nodelta 956 [ >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?); 957  >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?);  >EQfetch in ⊢ (??%?); 958  >EQfetch in ⊢ (??%?); ] % 959 3,9,15,21,27,33,39: skip *: try assumption // ] 960 ] 961 ] 962  st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 st3 963 [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl tl lapply(refl ? (FINAL p p')) 964 generalize in match (FINAL ??) in ⊢ (??%? → %); #st5 #EQst5 #tl lapply EQst5 965 lapply exe lapply st2 st2 EQst5 elim tl 966 [ #st #st5 #ABS #EQ destruct cases ABS 967  #s1 #s2 #s3 #l2 #H3 #tl1 #IH #s4 #_ #EQ destruct cases H3 968 ] 969 ] 970 #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #l1_lab1 #k #pre_meas whd in ⊢ (??%? → ?); 971 >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind 3,6: ] 972 >dependent_map_append 973 [ @eqb_elim [ #ABS @⊥ cases exe_st1_st3 >ABS @eqb_elim [ #_ #EQ destruct  * #ABS1 @⊥ @ABS1 %] ] 974 #Hpc normalize nodelta #H cases(bind_inversion ????? H) H #i * #EQi 975 inversion(emits_labels ??) 976 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels 977 cases(step_emit … EQi … EQemits) 978 [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) 2,3:] #c * #EQc #Hc 979 whd in match actionlabel_to_costlabel; normalize nodelta 980 >rewrite_in_dependent_map [2: @EQc 3:] whd in match (dependent_map ????); 981 @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????) 982 #EQ destruct >big_op_associative >act_op @IH 983  #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) H #k' * #EQk' whd in ⊢ (??%% → ?); 984 #EQ destruct(EQ) #a1 #good_a1 #labels cases(step_non_emit … EQi… EQemits) 985 [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) 2,3:] #EQl #EQpc 986 >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????); 987 #EQlabels >act_op @IH 988 ] 989 [2: assumption   assumption  assumption  cases daemon (*TODO*) 990 whd in ⊢ (??%%); 991 [1,5: inversion H in ⊢ ?; 992 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 993 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 994 #EQ1 #EQ2 #EQ3 #EQ4 destruct 995 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 996 #EQ1 #EQ2 #EQ3 #EQ4 destruct 997 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 998 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 999 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1000 ] // 1001  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 1002 >(rewrite_in_dependent_map … EQx) 1003 1004 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 1005 >neutral_l @opt_safe_elim #elem #EQget 1006 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 1007 #EQ #_ <EQ assumption 1008  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 1009  % 1010  >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1011 >(monotonicity_of_block_cost … EQk') // 1012  @(instr_map_ok … good … EQi … good_a1) /2/ 1013  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1014 #EQ >(rewrite_in_dependent_map … EQ) % 1015 ] 893 1016 >(rewrite_in_dependent_map ??? []) 894 1017 [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral 895 1018 lapply (instr_map_ok … good … prf …) 896 1019 897 >(act_neutral ?? (act_abs ? abs_t) a1)) 898 change 899 with (get_costlabels_of_trace ??? (?@?)) 900 in match (get_costlabels_of_trace ????); 901 cases l 1020 >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % 4: @get_cost_label_append *:] *:] 3:] 1021 xxxxxx 902 1022 903 >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append skip]3:skip] 904 cases daemon 905  cases daemon ]] 906  st1 #st1 #st3 #st4 #l whd in ⊢ (% → ?); 1023 >dependent_map_append 1024 inversion(emits_labels ??) 1025 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels 1026 >rewrite_in_dependent_map #EQlabels 1027 >neutral_r check big_op_associative @IH 1028 >big_op_associative >act_op @IH 1029  #f #EQemits normalize nodelta #H 1030 cases(bind_inversion ????? H) H #k' * #EQk' whd in ⊢ (??%% → ?); 1031 #EQ destruct(EQ) >act_op whd in match (append ???); @IH 1032 ] 1033 [1,5: inversion H in ⊢ ?; 1034 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 1035 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 1036 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1037 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 1038 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1039 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 1040 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1041 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1042 ] // 1043  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 1044 >(rewrite_in_dependent_map … EQx) 1045 1046 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 1047 >neutral_l @opt_safe_elim #elem #EQget 1048 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 1049 #EQ #_ <EQ assumption 1050  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 1051  % 1052  >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1053 >(monotonicity_of_block_cost … EQk') // 1054  @(instr_map_ok … good … EQi … good_a1) /2/ 1055  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1056 #EQ >(rewrite_in_dependent_map … EQ) % 1057 ] 1058 ] 1059 1060 ] 1061 1062 1063 1064 * #i * #EQi inversion(emits_labels …) normalize nodelta 1065 1066 1067 >(act_neutral … a1) in H; 1068 1069 1070 #H #H1 1071 cases st2 in prf; st2 [3: #st2] #prf 1072 lapply(instr_map_ok … good … prf … rel_fin) 1073 1074 lapply prf * 1075 #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 1076 >act_neutral >act_neutral @(instr_map_ok … good … rel_fin) 1077 1078 1079 @opt_safe_elim #k_init 1080 #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct 1081 >act_neutral whd in match (big_op ??); >act_op >act_neutral 1082 1083 1084 #H >act_neutral whd in prf; 1085 1086 cases l in prf H1 H2; 1087 [1,4: #f #lbl 2,5: * [2,4: #lbl] *: * [2,4: #lbl] ] #prf 1088 ** [normalize in ⊢ (% → ?); 1089 ⊢ (??%% → ?); 907 1090 908 1091 * #H3 #H4
Note: See TracChangeset
for help on using the changeset viewer.