Changeset 2187
 Timestamp:
 Jul 16, 2012, 5:19:06 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2183 r2187 130 130 ∀M', cm. 131 131 ∀sigma, status, b. 132 ∀addr1: [[acc_a; registr; direct; indirect; data ]]. (* XXX: expand as needed *)132 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *) 133 133 addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → 134 134 map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status addr1 b = b. … … 154 154 #w whd in ⊢ (??%? → ??%?); 155 155 cases daemon (* XXX: ??? *) 156 5 :156 5,6: 157 157 #w #_ % 158 158 ] … … 191 191 qed. 192 192 193 lemma get_ac_flag_status_of_pseudo_status: 194 ∀M: internal_pseudo_address_map. 195 ∀sigma: Word → Word. 196 ∀policy: Word → bool. 197 ∀code_memory: pseudo_assembly_program. 198 ∀s: PreStatus ? code_memory. 199 ∀s'. 200 status_of_pseudo_status M code_memory s sigma policy = s' → 201 get_ac_flag ?? s' = get_ac_flag ? code_memory s. 202 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 203 whd in match get_ac_flag; normalize nodelta 204 whd in match status_of_pseudo_status; normalize nodelta 205 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 206 cases (\snd M) try % 207 * normalize nodelta #address 208 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 209 whd in match sfr_8051_index; normalize nodelta 210 >get_index_v_set_index_miss [2,4: /2/] % 211 qed. 212 213 lemma get_cy_flag_status_of_pseudo_status: 214 ∀M: internal_pseudo_address_map. 215 ∀sigma: Word → Word. 216 ∀policy: Word → bool. 217 ∀code_memory: pseudo_assembly_program. 218 ∀s: PreStatus ? code_memory. 219 ∀s'. 220 status_of_pseudo_status M code_memory s sigma policy = s' → 221 get_cy_flag ?? s' = get_cy_flag ? code_memory s. 222 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 223 whd in match get_cy_flag; normalize nodelta 224 whd in match status_of_pseudo_status; normalize nodelta 225 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 226 cases (\snd M) try % 227 * normalize nodelta #address 228 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 229 whd in match sfr_8051_index; normalize nodelta 230 >get_index_v_set_index_miss [2,4: /2/] % 231 qed. 232 233 lemma get_ov_flag_status_of_pseudo_status: 234 ∀M: internal_pseudo_address_map. 235 ∀sigma: Word → Word. 236 ∀policy: Word → bool. 237 ∀code_memory: pseudo_assembly_program. 238 ∀s: PreStatus ? code_memory. 239 ∀s'. 240 status_of_pseudo_status M code_memory s sigma policy = s' → 241 get_ov_flag ?? s' = get_ov_flag ? code_memory s. 242 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl 243 whd in match get_ov_flag; normalize nodelta 244 whd in match status_of_pseudo_status; normalize nodelta 245 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 246 cases (\snd M) try % 247 * normalize nodelta #address 248 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 249 whd in match sfr_8051_index; normalize nodelta 250 >get_index_v_set_index_miss [2,4: /2/] % 251 qed. 252 193 253 lemma match_nat_status_of_pseudo_status: 194 254 ∀M, cm, sigma, policy, s, s', s'', s'''. … … 232 292 match l with [ O ⇒ o  S n ⇒ p ] = match r with [ O ⇒ o'  S n' ⇒ p' ]. 233 293 #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl % 294 qed. 295 296 lemma conjunction_split: 297 ∀l, l', r, r': bool. 298 l = l' → r = r' → (l ∧ r) = (l' ∧ r'). 299 #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl % 234 300 qed. 235 301 … … 873 939 2: 874 940 @set_flags_status_of_pseudo_status try % 875 @sym_eq @ set_arg_8_status_of_pseudo_status941 @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …)) 876 942 [1: 877 943 @sym_eq @set_clock_status_of_pseudo_status % … … 972 1038 2: 973 1039 change with (get_ac_flag ??? = get_ac_flag ???) 974 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 975 cases daemon 1040 @(get_ac_flag_status_of_pseudo_status M') 1041 @sym_eq @set_clock_status_of_pseudo_status 1042 >EQs >EQticks <instr_refl % 976 1043 ] 977 1044 2: … … 993 1060 @set_flags_status_of_pseudo_status try % 994 1061 [1: 995 @eq_f @sym_eq cases daemon 996 (* XXX: get_ac_flag_status_of_pseudo_status *) 1062 @eq_f @(get_ac_flag_status_of_pseudo_status M') 1063 @sym_eq @set_8051_sfr_status_of_pseudo_status 1064 [1: 1065 @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1066 2: 1067 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1068 ] 997 1069 2: 998 @sym_eq cases daemon 999 (* XXX: get_ov_flag_status_of_pseudo_status *) 1070 @(get_ov_flag_status_of_pseudo_status M') 1071 @sym_eq @set_8051_sfr_status_of_pseudo_status 1072 [1: 1073 @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1074 2: 1075 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1076 ] 1000 1077 3: 1001 1078 @sym_eq @set_8051_sfr_status_of_pseudo_status … … 1045 1122 2: 1046 1123 change with (get_ac_flag ??? = get_ac_flag ???) 1047 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 1048 cases daemon 1124 @(get_ac_flag_status_of_pseudo_status M') 1125 @sym_eq @set_clock_status_of_pseudo_status 1126 >EQs >EQticks <instr_refl % 1049 1127 ] 1050 1128 2: … … 1102 1180 2: 1103 1181 change with (get_ac_flag ??? = get_ac_flag ???) 1104 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 1105 cases daemon 1182 @(get_ac_flag_status_of_pseudo_status M') 1183 @sym_eq @set_clock_status_of_pseudo_status 1184 >EQs >EQticks <instr_refl % 1106 1185 ] 1107 1186 2: … … 1117 1196 ] 1118 1197 ] 1198 36: (* CLR *) 1199 >EQP P normalize nodelta 1200 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1201 whd in maps_assm:(??%%); 1202 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1203 [2: normalize nodelta #absurd destruct(absurd) ] 1204 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1205 whd in ⊢ (??%?); 1206 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1207 whd in ⊢ (??%?); normalize nodelta 1208 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1209 normalize nodelta #subaddressing_modein_witness 1210 @set_arg_8_status_of_pseudo_status try % 1211 [1: 1212 @sym_eq @set_clock_status_of_pseudo_status 1213 >EQs >EQticks <instr_refl % 1214 2: 1215 whd in ⊢ (??%?); 1216 >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1) 1217 [2: <EQaddr % ] % 1218 ] 1219 37: (* CLR *) 1220 >EQP P normalize nodelta 1221 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1222 whd in maps_assm:(??%%); 1223 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1224 [2: normalize nodelta #absurd destruct(absurd) ] 1225 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1226 whd in ⊢ (??%?); 1227 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1228 whd in ⊢ (??%?); normalize nodelta 1229 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1230 normalize nodelta #subaddressing_modein_witness 1231 @set_arg_1_status_of_pseudo_status try % 1232 @sym_eq @set_clock_status_of_pseudo_status 1233 >EQs >EQticks <instr_refl % 1234 38: (* CLR *) 1235 >EQP P normalize nodelta 1236 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1237 whd in maps_assm:(??%%); 1238 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1239 [2: normalize nodelta #absurd destruct(absurd) ] 1240 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1241 whd in ⊢ (??%?); 1242 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1243 whd in ⊢ (??%?); normalize nodelta 1244 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1245 normalize nodelta #subaddressing_modein_witness 1246 @set_arg_1_status_of_pseudo_status try % 1247 [1: 1248 @sym_eq @set_clock_status_of_pseudo_status 1249 >EQs >EQticks <instr_refl % 1250 *: 1251 (* XXX: ??? *) 1252 cases daemon 1253 ] 1254 39: (* CPL *) 1255 >EQP P normalize nodelta 1256 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1257 whd in maps_assm:(??%%); 1258 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1259 [2: normalize nodelta #absurd destruct(absurd) ] 1260 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1261 whd in ⊢ (??%?); 1262 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1263 whd in ⊢ (??%?); normalize nodelta 1264 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1265 normalize nodelta #subaddressing_modein_witness 1266 @set_8051_sfr_status_of_pseudo_status 1267 [1: 1268 @sym_eq @set_clock_status_of_pseudo_status 1269 >EQs >EQticks <instr_refl % 1270 2: 1271 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1) 1272 [2: <EQaddr % ] normalize nodelta @eq_f 1273 @sym_eq @(get_8051_sfr_status_of_pseudo_status M') 1274 1275 ] 1276 1277 33: (* (* ANL *) 1278 (* XXX: work on the right hand side *) 1279 (* XXX: switch to the left hand side *) 1280 >EQP P normalize nodelta lapply instr_refl 1281 inversion addr 1282 [1: 1283 #addr' #addr_refl' 1284 inversion addr' 1285 #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm 1286 whd in ⊢ (??%? → ?); normalize nodelta cases addr 1287 [1: 1288 #acc_a #others normalize nodelta 1289 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1290 [2: normalize nodelta #absurd destruct(absurd) ] 1291 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1292 [2: normalize nodelta #absurd destruct(absurd) ] 1293 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1294 whd in ⊢ (??%?); 1295 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1296 whd in ⊢ (??%?); normalize nodelta 1297 inversion addr #addr1 #addr2 1298 @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a) 1299 @(subaddressing_mode_elim … addr2) 1300 @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try % 1301 [1: 1302 @sym_eq @set_clock_status_of_pseudo_status 1303 >EQs >EQticks <addr_refl <instr_refl 1304 [1: 1305 @sym_eq @set_program_counter_status_of_pseudo_status % 1306 2: 1307 @eq_f2 1308 [1: 1309 >addr_refl @(subaddressing_mode_elim … addr1) % 1310 2: 1311 @(clock_status_of_pseudo_status M') 1312 @sym_eq @set_program_counter_status_of_pseudo_status % 1313 ] 1314 ] 1315 2: 1316 cases daemon (* XXX: matita dies here *) 1317 ] 1318 2: 1319 #direct #others 1320 @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta 1321 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1322 [2: normalize nodelta #absurd destruct(absurd) ] 1323 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1324 [2: normalize nodelta #absurd destruct(absurd) ] 1325 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1326 whd in ⊢ (??%?); 1327 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1328 whd in ⊢ (??%?); normalize nodelta 1329 inversion addr #addr1 #addr2 1330 @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2) 1331 [1: #w 2: #w1 #w2 ] #addr_refl normalize nodelta 1332 @set_arg_8_status_of_pseudo_status 1333 ] 1334 2: 1335 addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm 1336 whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta 1337 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1338 [2: normalize nodelta #absurd destruct(absurd) ] 1339 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1340 [2: normalize nodelta #absurd destruct(absurd) ] 1341 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1342 whd in ⊢ (??%?); 1343 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1344 whd in ⊢ (??%?); normalize nodelta 1345 inversion addr #addr1 #addr2 #addr_refl normalize nodelta 1346 @set_flags_status_of_pseudo_status try % 1347 [1: 1348 @conjunction_split 1349 [1: 1350 @(get_cy_flag_status_of_pseudo_status M') 1351 @sym_eq @set_clock_status_of_pseudo_status 1352 >EQs >EQticks <addr_refl <instr_refl % 1353 2: 1354 >EQs >EQticks <addr_refl <instr_refl normalize nodelta 1355 (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *) 1356 cases daemon 1357 ] 1358 2: 1359 @(get_ov_flag_status_of_pseudo_status M') 1360 @sym_eq @set_clock_status_of_pseudo_status 1361 >EQs >EQticks <instr_refl <addr_refl % 1362 3: 1363 @sym_eq @set_clock_status_of_pseudo_status 1364 >EQs >EQticks <instr_refl <addr_refl % 1365 ] 1366 ] 1367 whd in maps_assm:(??%%); 1368 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1369 [2: normalize nodelta #absurd destruct(absurd) ] 1370 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1371 whd in ⊢ (??%?); 1372 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1373 whd in ⊢ (??%?); normalize nodelta 1119 1374 16: (* JC *) 1120 1375 (* XXX: work on the right hand side *) 
src/ASM/Test.ma
r2183 r2187 713 713 ∀cm. 714 714 ∀ps. 715 ∀addr :[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].715 ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 716 716 ∀value. 717 717 ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. 718 addr = addr' → 718 719 status_of_pseudo_status M cm ps sigma policy = s' → 719 720 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → … … 722 723 (code_memory_of_pseudo_assembly_program cm sigma policy) 723 724 s' addr value' = 724 status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.725 #cm #ps #addr # value725 status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy. 726 #cm #ps #addr #addr' #value 726 727 cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant 728 #M #sigma #policy #s' #value' #addr_refl <addr_refl 727 729 @relevant 728 730 qed. … … 1105 1107 ∀cm. 1106 1108 ∀ps. 1107 ∀addr : [[bit_addr; n_bit_addr; carry]].1109 ∀addr, addr': [[bit_addr; n_bit_addr; carry]]. 1108 1110 ∀l. 1109 1111 ∀M. ∀sigma. ∀policy. ∀s'. 1112 addr = addr' → 1110 1113 status_of_pseudo_status M cm ps sigma policy = s' → 1111 1114 map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → 1112 1115 get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 1113 1116 s' addr l = 1114 (get_arg_1 … cm ps addr l).1115 #cm #ps #addr # l1117 (get_arg_1 … cm ps addr' l). 1118 #cm #ps #addr #addr' #l 1116 1119 cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm 1120 #M #sigma #policy #s' #addr_refl <addr_refl 1117 1121 @assm 1118 1122 qed.
Note: See TracChangeset
for help on using the changeset viewer.