Changeset 3497
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3496 r3497 876 876 qed. 877 877 878 check labels_pc 879 880 lemma i_act_in_map : ∀p,prog,iact,l1,l2. 881 mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O). 882 #p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr 883 [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???); 884 @mem_append_l2 @IH 885 qed. 886 878 887 lemma static_dynamic : ∀p,p',prog. 879 888 ∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t. … … 905 914 ] 906 915 lapply Hlabelled lapply prf1 prf1 lapply l1 l1 elim t1 st3 907 [ * [3: #st] #l #prf #H1 # H2 #kwhd in ⊢ (??%? → ?);916 [ * [3: #st] #l #prf #H1 #k #_ whd in ⊢ (??%? → ?); 908 917 [3: cases prf 909 918 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?); … … 987 996 [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??); 988 997 >neutral_l assumption 989 3 : >neutral_rlapply(instr_map_ok … good … good_a1)990 [ whd in ⊢ (??%?); @eqb_elim991 [ #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;992 normalize nodelta >EQi in ⊢ (??%?);%993  assumption998 3,6: [ >neutral_r] lapply(instr_map_ok … good … good_a1) 999 [1,7: whd in ⊢ (??%?); @eqb_elim 1000 [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state; 1001 normalize nodelta [ >EQi in ⊢ (??%?);  >EQi in ⊢ (??%?); ] % 1002 2,8: assumption 994 1003 *: 995 1004 ] 996 1005 normalize in ⊢ (% → ?); #H @H 997 998 999 [2: assumption   assumption  assumption  cases daemon (*TODO*) 1000 whd in ⊢ (??%%); 1001 [1,5: inversion H in ⊢ ?; 1002 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 1006 5: whd in match get_pc; normalize nodelta >EQpc >(monotonicity_of_block_cost … EQk') // 1007 *: inversion pre_meas in ⊢ ?; 1008 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1003 1009 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 1004 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1010 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1005 1011 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 1006 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1012 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1007 1013 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 1008 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1014 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1009 1015 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1010 ] // 1011  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 1012 >(rewrite_in_dependent_map … EQx) 1013 1014 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 1015 >neutral_l @opt_safe_elim #elem #EQget 1016 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 1017 #EQ #_ <EQ assumption 1018  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 1019  % 1020  >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1021 >(monotonicity_of_block_cost … EQk') // 1022  @(instr_map_ok … good … EQi … good_a1) /2/ 1023  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1024 #EQ >(rewrite_in_dependent_map … EQ) % 1025 ] 1026 1027 >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % 4: @get_cost_label_append *:] *:] 3:] 1028 xxxxxx 1029 1030 >dependent_map_append 1031 inversion(emits_labels ??) 1032 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels 1033 >rewrite_in_dependent_map #EQlabels 1034 >neutral_r check big_op_associative @IH 1035 >big_op_associative >act_op @IH 1036  #f #EQemits normalize nodelta #H 1037 cases(bind_inversion ????? H) H #k' * #EQk' whd in ⊢ (??%% → ?); 1038 #EQ destruct(EQ) >act_op whd in match (append ???); @IH 1039 ] 1040 [1,5: inversion H in ⊢ ?; 1041 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 1042 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 1043 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1044 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 1045 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1046 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 1047 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1048 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1049 ] // 1050  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 1051 >(rewrite_in_dependent_map … EQx) 1052 1053 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 1054 >neutral_l @opt_safe_elim #elem #EQget 1055 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 1056 #EQ #_ <EQ assumption 1057  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 1058  % 1059  >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1060 >(monotonicity_of_block_cost … EQk') // 1061  @(instr_map_ok … good … EQi … good_a1) /2/ 1062  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1063 #EQ >(rewrite_in_dependent_map … EQ) % 1064 ] 1065 ] 1066 1067 ] 1068 1069 1070 1071 * #i * #EQi inversion(emits_labels …) normalize nodelta 1072 1073 1074 >(act_neutral … a1) in H; 1075 1076 1077 #H #H1 1078 cases st2 in prf; st2 [3: #st2] #prf 1079 lapply(instr_map_ok … good … prf … rel_fin) 1080 1081 lapply prf * 1082 #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 1083 >act_neutral >act_neutral @(instr_map_ok … good … rel_fin) 1084 1085 1086 @opt_safe_elim #k_init 1087 #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct 1088 >act_neutral whd in match (big_op ??); >act_op >act_neutral 1089 1090 1091 #H >act_neutral whd in prf; 1092 1093 cases l in prf H1 H2; 1094 [1,4: #f #lbl 2,5: * [2,4: #lbl] *: * [2,4: #lbl] ] #prf 1095 ** [normalize in ⊢ (% → ?); 1096 ⊢ (??%% → ?); 1097 1098 #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] 1099 cases st st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %] 1100 #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1 1101 #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption 1102  st1 st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); * 1103 [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?); 1104 (* 1105 #EQlabels 1106 #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta 1107 [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st 1108 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1109 #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 1110  ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta 1111 #H cases(bind_inversion ????? H) H * 1112 [ #seq * [#lbl1] 1113  #newpc 1114  #cond #newpc #ltrue #lfalse 1115  #lin #io #lout 1116  #f 1117  1118 ] 1119 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; 1120 normalize nodelta >EQfetch >m_return_bind normalize nodelta 1121 cases(asm_is_io ??) normalize nodelta 1122 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 1123 2,4,8,9,12,14: #H cases(bind_inversion ????? H) H #x * #_ 1124 [3: cases x normalize nodelta 1125 6: #H cases(bind_inversion ????? H) H #y * #_ 1126 ] 1127 ] 1128 whd in ⊢ (??%% → ?); #EQ destruct 1129 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 1130 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 1131 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r 1132 >act_neutral 1133 @(instr_map_ok … good … EQfetch … good_st_a1) /2/ 1134 ]*) 1135  st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 1136 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 1137 whd #costs >dependent_map_append 1138 (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) 1139 #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); H2 1140 normalize nodelta #H cases(bind_inversion ????? H) H #i * #EQi 1141 inversion(emits_labels ??) 1142 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct >big_op_associative >act_op @IH 1143  #f #EQemits normalize nodelta #H 1144 cases(bind_inversion ????? H) H #k' * #EQk' whd in ⊢ (??%% → ?); 1145 #EQ destruct(EQ) >act_op whd in match (append ???); @IH 1146 ] 1147 [1,5: inversion H in ⊢ ?; 1148 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 1149 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 1150 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1151 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 1152 #EQ1 #EQ2 #EQ3 #EQ4 destruct 1153 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 1154 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1155 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1156 ] // 1157  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 1158 >(rewrite_in_dependent_map … EQx) 1159 1160 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 1161 >neutral_l @opt_safe_elim #elem #EQget 1162 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 1163 #EQ #_ <EQ assumption 1164  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 1165  % 1166  >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1167 >(monotonicity_of_block_cost … EQk') // 1168  @(instr_map_ok … good … EQi … good_a1) /2/ 1169  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 1170 #EQ >(rewrite_in_dependent_map … EQ) % 1171 ] 1172 ] 1173 qed. 1174 1175 definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ 1176 λa.match a with 1177 [ call_act f l ⇒ [a_call l] 1178  ret_act opt_l ⇒ match opt_l with [None ⇒ [ ]  Some l ⇒ [a_return_post l]] 1179  cost_act opt_l ⇒ match opt_l with [None ⇒ [ ]  Some l ⇒ [a_non_functional_label l]] 1180 ]. 1181 1182 definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝ 1183 λS,t. 1184 match L_label … t with 1185 [ None ⇒ [i_act] 1186  Some l ⇒ actionlabel_to_costlabel l 1187 ] @ 1188 get_costlabels_of_trace … (trace … t). 1189 1190 lemma i_act_in_map : ∀p,prog. 1191 mem … 〈i_act,O〉 (labels_pc … (instructions p prog) O). 1192 #p *#instr #n #_ generalize in match O in ⊢ (???%); elim instr 1193 [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???); 1194 @mem_append_l2 @IH 1195 qed. 1196 1197 1198 lemma as_execute_labelled_ok : ∀p,p',prog,c,l,st1,st2. 1199 eval_vmstate p p' prog st1 = return 〈l,st2〉 → actionlabel_to_costlabel l = [c] → 1200 ∃n. 1201 mem … 〈c,n〉 (labels_pc … (instructions p prog) O). 1202 #p #p' * #instr #endmain #Hendmain #c #l #st1 #st2 #H2 lapply H2 whd in match eval_vmstate; normalize nodelta 1203 #H cases(bind_inversion ????? H) H #i * #EQfetch #_ 1204 inversion(emits_labels … i) 1205 [ #EQemit cases(step_emit … H2) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel; 1206 normalize nodelta >EQ1 #EQ destruct /2 by ex_intro/ 1207  #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta >(proj1 … (step_non_emit … EQfetch H2 … EQemit)) 1208 #EQ destruct 1209 ] 1210 qed. 1211 1212 1213 (*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*) 1214 theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. 1215 ∀abs_t : abstract_transition_sys (m … p').∀instr_m. 1216 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. 1217 ∀EQmap : static_analisys p ? instr_m mT prog = return map1. 1218 ∀t : measurable_trace (asm_operational_semantics p p' prog). 1219 let start_state ≝ match L_pre_state … t with [None ⇒ L_s1 … t  Some x ⇒ x ] in 1220 ∀a1.rel_galois … good start_state a1 → 1221 ∀abs_trace. 1222 abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → 1223 rel_galois … good (R_s2 … t) (act_abs … abs_t (big_op … abs_trace) a1). 1224 [2: @hide_prf 1225 whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf; 1226 cases(mem_append ???? prf) prf 1227 [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * 1228 #lbl' #pc * #Hmem #EQ destruct 1229 >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) 1230 @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) 1231  inversion(L_label … t) normalize nodelta [ #lbl'] #EQleft 1232 [ * [2: *] #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …))) 1233 @(proj2 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …))) 1234  #H lapply(L_init_ok … t) inversion(L_pre_state … t) [ #_ normalize nodelta * #_ >EQleft #EQ destruct] 1235 #st_pre #EQst_pre normalize nodelta * #l' ** >EQleft #EQ destruct cases l' in H; 1236 [ #x1 #x2  * [#x1]  * [#x1]] whd in ⊢ (% → %→ ?); * [2,4,6: *] #EQ destruct * * #_ 1237 #H cases(as_execute_labelled_ok … H) [3,6,9:% *:] #w #EQw 1238 >(proj1 … (static_analisys_ok … no_dup … EQmap … EQw)) 1239 @(proj2 … (static_analisys_ok … no_dup … EQmap … EQw)) 1240 ] 1241 ] 1242 ] 1243 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace 1244 @(static_dynamic …) 1245 1246 xxxxxx 1247 lapply(static_dynamic … (trace …t) … abs_trace) try // 1248 1249 1016 ] // 1017 ] 1018  whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 cases exe_st1_st3 #EQpc_st3 #EQ destruct 1019 #labels whd in match actionlabel_to_costlabel; normalize nodelta 1020 whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????) 1021 change with ([?]@?) in match ([?]@?); #EQ destruct >big_op_associative >act_op @IH try // 1022 [ inversion pre_meas in ⊢ ?; 1023 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1024 2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 1025 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1026 3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 1027 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1028 4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 1029 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct 1030 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1031 ] // 1032  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap) 1033 [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ] 1034 #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption 1035  lapply(instr_map_ok … good … good_a1) 1036 [1: %  assumption *:] normalize in ⊢ (% → ?); #H @H 1037 ] 1038 ] 1039 qed.
Note: See TracChangeset
for help on using the changeset viewer.