Changeset 2018
 Timestamp:
 Jun 5, 2012, 5:49:09 PM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2017 r2018 860 860 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 861 861 whd in match execute_1_preinstruction; normalize nodelta 862 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 862 [30: (* CJNE *) 863 (* XXX: work on the right hand side *) 864 cases addr1 addr1 #addr1 normalize nodelta 865 cases addr1 addr1 #addr1_l #addr1_r normalize nodelta 866 (* XXX: switch to the left hand side *) 867 >EQP P normalize nodelta 868 #sigma_increment_commutation #maps_assm #fetch_many_assm 869 870 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 871 whd in match (expand_relative_jump ????); 872 <EQppc in fetch_many_assm; 873 @pair_elim #result #flags #sub16_refl 874 @pair_elim #upper #lower #split_refl 875 inversion (eq_bv ???) #upper_split_refl normalize nodelta 876 [1,3: 877 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 878 whd in ⊢ (??%?); 879 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 880 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 881 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl 882 @(if_then_else_replace ???????? eq_bv_refl) 883 [1,3,5,7: 884 cases daemon 885 2,4,6,8: 886 (* XXX: switch to the right hand side *) 887 normalize nodelta >EQs s >EQticks ticks 888 whd in ⊢ (??%%); 889 (* XXX: finally, prove the equality using sigma commutation *) 890 @split_eq_status try % 891 [3,7,11,15: 892 whd in ⊢ (??%?); 893 [1,3: 894 cases daemon 895 2,4: 896 cases daemon 897 ] 898 ] 899 cases daemon (* XXX *) 900 ] 901 2,4: 902 >EQppc 903 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 904 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 905 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 906 #fetch_many_assm whd in fetch_many_assm; %{2} 907 change with (execute_1 ?? = ?) 908 @(pose … (execute_1 ? (status_of_pseudo_status …))) 909 #status_after_1 #EQstatus_after_1 910 <(?: ? = status_after_1) 911 [3,6: 912 >EQstatus_after_1 in ⊢ (???%); 913 whd in ⊢ (???%); 914 [1: <fetch_refl in ⊢ (???%); 915 2: <fetch_refl in ⊢ (???%); 916 ] 917 whd in ⊢ (???%); 918 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 919 whd in ⊢ (???%); 920 whd in match (addr_of_relative ????); 921 change with (add ???) in match (\snd (half_add ???)); 922 >set_clock_set_program_counter in ⊢ (???%); 923 >program_counter_set_program_counter in ⊢ (???%); 924 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 925 [2,4,6,8: 926 >bitvector_of_nat_sign_extension_equivalence 927 [1,3,5,7: 928 >EQintermediate_pc' % 929 *: 930 repeat @le_S_S @le_O_n 931 ] 932 ] 933 [1,3: % ] 934 ] 935 ] 936 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) 937 (* XXX: work on the right hand side *) 938 >p normalize nodelta 939 (* XXX: switch to the left hand side *) 940 instr_refl >EQP P normalize nodelta 941 #sigma_increment_commutation #maps_assm #fetch_many_assm 942 943 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 944 whd in match (expand_relative_jump ????); 945 <EQppc in fetch_many_assm; 946 @pair_elim #result #flags #sub16_refl 947 @pair_elim #upper #lower #split_refl 948 cases (eq_bv ???) normalize nodelta 949 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 950 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 951 whd in ⊢ (??%?); 952 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 953 (* XXX: work on the left hand side *) 954 @(if_then_else_replace ???????? p) normalize nodelta 955 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 956 cases daemon 957 ] 958 (* XXX: switch to the right hand side *) 959 normalize nodelta >EQs s >EQticks ticks 960 whd in ⊢ (??%%); 961 (* XXX: finally, prove the equality using sigma commutation *) 962 @split_eq_status try % 963 cases daemon 964 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 965 >EQppc 966 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 967 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 968 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 969 #fetch_many_assm whd in fetch_many_assm; %{2} 970 change with (execute_1 ?? = ?) 971 @(pose … (execute_1 ? (status_of_pseudo_status …))) 972 #status_after_1 #EQstatus_after_1 973 <(?: ? = status_after_1) 974 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 975 >EQstatus_after_1 in ⊢ (???%); 976 whd in ⊢ (???%); 977 [1: <fetch_refl in ⊢ (???%); 978 2: <fetch_refl in ⊢ (???%); 979 3: <fetch_refl in ⊢ (???%); 980 4: <fetch_refl in ⊢ (???%); 981 5: <fetch_refl in ⊢ (???%); 982 6: <fetch_refl in ⊢ (???%); 983 7: <fetch_refl in ⊢ (???%); 984 8: <fetch_refl in ⊢ (???%); 985 9: <fetch_refl in ⊢ (???%); 986 10: <fetch_refl in ⊢ (???%); 987 11: <fetch_refl in ⊢ (???%); 988 12: <fetch_refl in ⊢ (???%); 989 13: <fetch_refl in ⊢ (???%); 990 14: <fetch_refl in ⊢ (???%); 991 ] 992 whd in ⊢ (???%); 993 @(if_then_else_replace ???????? p) 994 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 995 cases daemon 996 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 997 normalize nodelta 998 whd in match (addr_of_relative ????); 999 >set_clock_mk_Status_commutation 1000 [9,10: 1001 (* XXX: demodulation not working in this case *) 1002 >program_counter_set_arg_1 in ⊢ (???%); 1003 >program_counter_set_program_counter in ⊢ (???%); 1004 *: 1005 /demod/ 1006 ] 1007 whd in ⊢ (???%); 1008 change with (add ???) in match (\snd (half_add ???)); 1009 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1010 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1011 >bitvector_of_nat_sign_extension_equivalence 1012 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1013 >EQintermediate_pc' % 1014 *: 1015 repeat @le_S_S @le_O_n 1016 ] 1017 ] 1018 % 1019 ] 1020 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1021 skip 1022 ] 1023 status_after_1 1024 @(pose … (execute_1 ? (mk_PreStatus …))) 1025 #status_after_1 #EQstatus_after_1 1026 <(?: ? = status_after_1) 1027 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 1028 >EQstatus_after_1 in ⊢ (???%); 1029 whd in ⊢ (???%); 1030 (* XXX: matita bug with patterns across multiple goals *) 1031 [1: <fetch_refl'' in ⊢ (???%); 1032 2: <fetch_refl' in ⊢ (???%); 1033 3: <fetch_refl'' in ⊢ (???%); 1034 4: <fetch_refl' in ⊢ (???%); 1035 5: <fetch_refl'' in ⊢ (???%); 1036 6: <fetch_refl' in ⊢ (???%); 1037 7: <fetch_refl'' in ⊢ (???%); 1038 8: <fetch_refl' in ⊢ (???%); 1039 9: <fetch_refl'' in ⊢ (???%); 1040 10: <fetch_refl' in ⊢ (???%); 1041 11: <fetch_refl'' in ⊢ (???%); 1042 12: <fetch_refl' in ⊢ (???%); 1043 13: <fetch_refl'' in ⊢ (???%); 1044 14: <fetch_refl' in ⊢ (???%); 1045 ] 1046 whd in ⊢ (???%); 1047 [9,10: 1048 *: 1049 /demod/ 1050 ] % 1051 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1052 skip 1053 ] 1054 status_after_1 whd in ⊢ (??%?); 1055 (* XXX: switch to the right hand side *) 1056 normalize nodelta >EQs s >EQticks ticks 1057 whd in ⊢ (??%%); 1058 (* XXX: finally, prove the equality using sigma commutation *) 1059 @split_eq_status try % 1060 [3,11,19,27,36,53,61: 1061 >program_counter_set_program_counter >set_clock_mk_Status_commutation 1062 [5: >program_counter_set_program_counter ] 1063 >EQaddr_of normalize nodelta 1064 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta 1065 >EQcm % 1066 7,15,23,31,45,57,65: 1067 >set_clock_mk_Status_commutation >program_counter_set_program_counter 1068 whd in ⊢ (??%?); normalize nodelta 1069 >EQppc in fetch_many_assm; #fetch_many_assm 1070 [5: 1071 >program_counter_set_arg_1 >program_counter_set_program_counter 1072 ] 1073 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc'' 1074 <bitvector_of_nat_sign_extension_equivalence 1075 [1,3,5,7,9,11,13: 1076 whd in ⊢ (???%); cases (half_add ???) normalize // 1077 2,4,6,8,10,12,14: 1078 @assembly1_lt_128 1079 @le_S_S @le_O_n 1080 ] 1081 *: 1082 cases daemon 1083 ] 1084 ] 1085 4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 863 1086 (* XXX: work on the right hand side *) 864 1087 lapply (subaddressing_modein ???) … … 1058 1281 (* XXX: finally, prove the equality using sigma commutation *) 1059 1282 cases daemon 1060 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)1061 (* XXX: work on the right hand side *)1062 >p normalize nodelta1063 (* XXX: switch to the left hand side *)1064 instr_refl >EQP P normalize nodelta1065 #sigma_increment_commutation #maps_assm #fetch_many_assm1066 1067 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;1068 whd in match (expand_relative_jump ????);1069 <EQppc in fetch_many_assm;1070 @pair_elim #result #flags #sub16_refl1071 @pair_elim #upper #lower #split_refl1072 cases (eq_bv ???) normalize nodelta1073 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:1074 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}1075 whd in ⊢ (??%?);1076 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);1077 (* XXX: work on the left hand side *)1078 @(if_then_else_replace ???????? p) normalize nodelta1079 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:1080 cases daemon1081 ]1082 (* XXX: switch to the right hand side *)1083 normalize nodelta >EQs s >EQticks ticks1084 whd in ⊢ (??%%);1085 (* XXX: finally, prove the equality using sigma commutation *)1086 @split_eq_status try %1087 cases daemon1088 2,4,6,8,10,12,14,16,18,20,22,24,26,28:1089 >EQppc1090 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl1091 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'1092 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''1093 #fetch_many_assm whd in fetch_many_assm; %{2}1094 change with (execute_1 ?? = ?)1095 @(pose … (execute_1 ? (status_of_pseudo_status …)))1096 #status_after_1 #EQstatus_after_11097 <(?: ? = status_after_1)1098 [3,6,9,12,15,18,21,24,27,30,33,36,39,42:1099 >EQstatus_after_1 in ⊢ (???%);1100 whd in ⊢ (???%);1101 [1: <fetch_refl in ⊢ (???%);1102 2: <fetch_refl in ⊢ (???%);1103 3: <fetch_refl in ⊢ (???%);1104 4: <fetch_refl in ⊢ (???%);1105 5: <fetch_refl in ⊢ (???%);1106 6: <fetch_refl in ⊢ (???%);1107 7: <fetch_refl in ⊢ (???%);1108 8: <fetch_refl in ⊢ (???%);1109 9: <fetch_refl in ⊢ (???%);1110 10: <fetch_refl in ⊢ (???%);1111 11: <fetch_refl in ⊢ (???%);1112 12: <fetch_refl in ⊢ (???%);1113 13: <fetch_refl in ⊢ (???%);1114 14: <fetch_refl in ⊢ (???%);1115 ]1116 whd in ⊢ (???%);1117 @(if_then_else_replace ???????? p)1118 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:1119 cases daemon1120 2,4,6,8,10,12,14,16,18,20,22,24,26,28:1121 normalize nodelta1122 whd in match (addr_of_relative ????);1123 >set_clock_mk_Status_commutation1124 [9,10:1125 (* XXX: demodulation not working in this case *)1126 >program_counter_set_arg_1 in ⊢ (???%);1127 >program_counter_set_program_counter in ⊢ (???%);1128 *:1129 /demod/1130 ]1131 whd in ⊢ (???%);1132 change with (add ???) in match (\snd (half_add ???));1133 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')1134 [2,4,6,8,10,12,14,16,18,20,22,24,26,28:1135 >bitvector_of_nat_sign_extension_equivalence1136 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:1137 >EQintermediate_pc' %1138 *:1139 repeat @le_S_S @le_O_n1140 ]1141 ]1142 %1143 ]1144 1,4,7,10,13,16,19,22,25,28,31,34,37,40:1145 skip1146 ]1147 status_after_11148 @(pose … (execute_1 ? (mk_PreStatus …)))1149 #status_after_1 #EQstatus_after_11150 <(?: ? = status_after_1)1151 [3,6,9,12,15,18,21,24,27,30,33,36,39,42:1152 >EQstatus_after_1 in ⊢ (???%);1153 whd in ⊢ (???%);1154 (* XXX: matita bug with patterns across multiple goals *)1155 [1: <fetch_refl'' in ⊢ (???%);1156 2: <fetch_refl' in ⊢ (???%);1157 3: <fetch_refl'' in ⊢ (???%);1158 4: <fetch_refl' in ⊢ (???%);1159 5: <fetch_refl'' in ⊢ (???%);1160 6: <fetch_refl' in ⊢ (???%);1161 7: <fetch_refl'' in ⊢ (???%);1162 8: <fetch_refl' in ⊢ (???%);1163 9: <fetch_refl'' in ⊢ (???%);1164 10: <fetch_refl' in ⊢ (???%);1165 11: <fetch_refl'' in ⊢ (???%);1166 12: <fetch_refl' in ⊢ (???%);1167 13: <fetch_refl'' in ⊢ (???%);1168 14: <fetch_refl' in ⊢ (???%);1169 ]1170 whd in ⊢ (???%);1171 [9,10:1172 *:1173 /demod/1174 ] %1175 1,4,7,10,13,16,19,22,25,28,31,34,37,40:1176 skip1177 ]1178 status_after_1 whd in ⊢ (??%?);1179 (* XXX: switch to the right hand side *)1180 normalize nodelta >EQs s >EQticks ticks1181 whd in ⊢ (??%%);1182 (* XXX: finally, prove the equality using sigma commutation *)1183 @split_eq_status try %1184 [3,11,19,27,36,53,61:1185 >program_counter_set_program_counter >set_clock_mk_Status_commutation1186 [5: >program_counter_set_program_counter ]1187 >EQaddr_of normalize nodelta1188 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta1189 >EQcm %1190 7,15,23,31,45,57,65:1191 >set_clock_mk_Status_commutation >program_counter_set_program_counter1192 whd in ⊢ (??%?); normalize nodelta1193 >EQppc in fetch_many_assm; #fetch_many_assm1194 [5:1195 >program_counter_set_arg_1 >program_counter_set_program_counter1196 ]1197 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''1198 <bitvector_of_nat_sign_extension_equivalence1199 [1,3,5,7,9,11,13:1200 whd in ⊢ (???%); cases (half_add ???) normalize //1201 2,4,6,8,10,12,14:1202 @assembly1_lt_1281203 @le_S_S @le_O_n1204 ]1205 *:1206 cases daemon1207 ]1208 ]1209 30: (* CJNE *)1210 cases addr1 * #addr1_l #addr1_r normalize nodelta1211 (* XXX: work on the right hand side *)1212 (* XXX: switch to the left hand side *)1213 instr_refl >EQP P normalize nodelta1214 #sigma_increment_commutation #maps_assm #fetch_many_assm1215 1216 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;1217 whd in match (expand_relative_jump ????);1218 <EQppc in fetch_many_assm;1219 @pair_elim #result #flags #sub16_refl1220 @pair_elim #upper #lower #split_refl1221 cases (eq_bv ???) normalize nodelta1222 [1,3:1223 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}1224 whd in ⊢ (??%?);1225 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);1226 (* XXX: work on the left hand side *)1227 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta1228 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl1229 @(if_then_else_replace ???????? eq_bv_refl)1230 [1,3,5,7:1231 cases daemon1232 *:1233 (* XXX: switch to the right hand side *)1234 normalize nodelta >EQs s >EQticks ticks1235 whd in ⊢ (??%%);1236 (* XXX: finally, prove the equality using sigma commutation *)1237 @split_eq_status try %1238 cases daemon1239 ]1240 2,4:1241 >EQppc1242 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl1243 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'1244 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''1245 #fetch_many_assm whd in fetch_many_assm; %{2}1246 change with (execute_1 ?? = ?)1247 @(pose … (execute_1 ? (status_of_pseudo_status …)))1248 #status_after_1 #EQstatus_after_11249 <(?: ? = status_after_1)1250 [3,6:1251 >EQstatus_after_1 in ⊢ (???%);1252 whd in ⊢ (???%);1253 [1:1254 <fetch_refl in ⊢ (???%);1255 2:1256 <fetch_refl in ⊢ (???%);1257 ]1258 whd in ⊢ (???%);1259 cases (¬ eq_bv ???) normalize nodelta1260 whd in match (addr_of_relative ????);1261 >set_clock_mk_Status_commutation1262 whd in ⊢ (???%);1263 [9,10:1264 (* XXX: demodulation not working in this case *)1265 >program_counter_set_arg_1 in ⊢ (???%);1266 >program_counter_set_program_counter in ⊢ (???%);1267 *:1268 /demod/1269 ]1270 whd in ⊢ (???%);1271 change with (add ???) in match (\snd (half_add ???));1272 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')1273 [2,4,6,8,10,12,14,16,18,20,22,24,26,28:1274 >bitvector_of_nat_sign_extension_equivalence1275 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:1276 >EQintermediate_pc' %1277 *:1278 repeat @le_S_S @le_O_n1279 ]1280 ]1281 %1282 ]1283 1284 1283 ] 1285 1284 ] 
src/ASM/Policy.ma
r2008 r2018 341 341 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) 342 342 + added in 343 if leb (addr  \fst inc_sigma) 12 6343 if leb (addr  \fst inc_sigma) 129 344 344 then short_jump 345 345 else long_jump 346 346 else 347 347 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in 348 if leb (\fst inc_sigma  addr) 12 9348 if leb (\fst inc_sigma  addr) 125 349 349 then short_jump 350 350 else long_jump.
Note: See TracChangeset
for help on using the changeset viewer.