Changeset 2283 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jul 31, 2012, 6:11:27 PM (8 years ago)
- File:
-
- 1 edited
-
src/ASM/AssemblyProofSplit.ma (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2282 r2283 18 18 include alias "ASM/Vector.ma". 19 19 include "ASM/Test.ma". 20 include "ASM/Test2.ma". 20 (*include "ASM/Test2.ma".*) 21 21 22 22 (*CSC: move elsewhere*) … … 90 90 <(eq_bv_eq … relevant) 91 91 >(vsplit_ok … (sym_eq … vsplit_refl)) % 92 qed. 93 94 lemma set_clock_set_clock: 95 ∀M, cm, s, t, t'. 96 set_clock M cm (set_clock … cm s t) t' = set_clock … cm s t'. 97 #M #cm #s #t #t' % 92 98 qed. 93 99 … … 1215 1221 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1216 1222 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1217 @(if_then_else_replace ???????? p) try % normalize nodelta 1218 change with (execute_1 ?? = ?) destruct 1219 whd in ⊢ (??%?); >EQs >EQticks <instr_refl 1220 change with (set_program_counter ???? = ?) 1221 ] 1222 cases daemon 1223 |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1223 change with (execute 1 ?? = ?) 1224 whd in match execute_1; normalize nodelta 1225 whd in match execute_1'; normalize nodelta 1226 <jc_fetch_refl whd in match execute_1_0; normalize nodelta 1227 whd in match execute_1_preinstruction; normalize nodelta 1228 @(if_then_else_replace ???????? p) normalize nodelta 1229 [1: 1230 >EQs 1231 whd in match get_cy_flag; normalize nodelta 1232 >special_function_registers_8051_set_program_counter 1233 <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try % 1234 normalize #absurd destruct(absurd) 1235 |2: 1236 @(if_then_else_replace ???????? p) normalize nodelta try % 1237 change with (execute_1 ?? = ?) 1238 whd in match execute_1; normalize nodelta 1239 whd in match execute_1'; normalize nodelta 1240 >program_counter_set_program_counter 1241 whd in match addr_of_relative; normalize nodelta 1242 >set_clock_set_program_counter >program_counter_set_program_counter 1243 <ljmp_fetch_refl 1244 change with (set_program_counter ???? = ?) 1245 >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter 1246 >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter 1247 >EQs >EQticks <instr_refl 1248 >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%); 1249 @set_program_counter_status_of_pseudo_status 1250 [1: 1251 >program_counter_set_program_counter 1252 whd in match compute_target_of_unconditional_jump; normalize nodelta 1253 >EQaddr_of normalize nodelta >EQlookup_labels % 1254 |2: 1255 >set_clock_set_clock 1256 @set_clock_status_of_pseudo_status try % 1257 /demod nohyps/ 1258 whd in match ticks_of0; normalize nodelta 1259 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1260 [1: 1261 >EQppc % 1262 |2: 1263 >sj_possible_refl % 1264 ] 1265 ] 1266 ] 1267 ] 1268 |13: (* JC *) 1269 >EQP -P normalize nodelta 1270 whd in match assembly_1_pseudoinstruction; normalize nodelta 1271 whd in match expand_pseudo_instruction; normalize nodelta 1272 whd in match expand_relative_jump; normalize nodelta 1273 whd in match expand_relative_jump_internal; normalize nodelta 1274 >EQppc in ⊢ (% → ?); 1275 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1276 inversion sj_possible #sj_possible_refl normalize nodelta 1277 [1: 1278 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1279 whd in maps_assm:(??%%); 1280 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1281 whd in ⊢ (??%?); normalize nodelta 1282 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1283 whd in ⊢ (??%?); 1284 @if_then_else_status_of_pseudo_status 1285 >EQs >EQticks <instr_refl normalize nodelta 1286 [1: 1287 @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) % 1288 |2: 1289 @set_program_counter_status_of_pseudo_status 1290 [1: 1291 >EQaddr_of normalize nodelta 1292 whd in match addr_of_relative; normalize nodelta 1293 @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl)) 1294 [1: 1295 @sym_eq whd in ⊢ (??%?); >EQppc % 1296 |2: 1297 >EQlookup_labels % 1298 |3: 1299 >sj_possible_refl @I 1300 ] 1301 |2: 1302 @set_clock_status_of_pseudo_status try % 1303 whd in match ticks_of0; normalize nodelta 1304 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1305 [1: 1306 >EQppc % 1307 |2: 1308 >sj_possible_refl % 1309 ] 1310 ] 1311 |3: 1312 @set_clock_status_of_pseudo_status try % @eq_f2 try % 1313 whd in match ticks_of0; normalize nodelta 1314 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1315 [1: 1316 >EQppc % 1317 |2: 1318 >sj_possible_refl % 1319 ] 1320 ] 1321 |2: 1322 #sigma_increment_commutation #maps_assm 1323 whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1324 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1325 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1326 change with (execute 1 ?? = ?) 1327 whd in match execute_1; normalize nodelta 1328 whd in match execute_1'; normalize nodelta 1329 <jc_fetch_refl whd in match execute_1_0; normalize nodelta 1330 whd in match execute_1_preinstruction; normalize nodelta 1331 @(if_then_else_replace ???????? p) normalize nodelta 1332 [1: 1333 >EQs 1334 whd in match get_cy_flag; normalize nodelta 1335 >special_function_registers_8051_set_program_counter 1336 <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try % 1337 normalize #absurd destruct(absurd) 1338 |2: 1339 @(if_then_else_replace ???????? p) normalize nodelta try % 1340 change with (execute_1 ?? = ?) 1341 whd in match execute_1; normalize nodelta 1342 whd in match execute_1'; normalize nodelta 1343 1344 >set_clock_set_program_counter 1345 >program_counter_set_program_counter 1346 <sjmp_fetch_refl 1347 change with (set_program_counter ???? = ?) 1348 >set_clock_set_program_counter >set_clock_set_program_counter 1349 >set_program_counter_set_program_counter >set_program_counter_set_program_counter 1350 >EQs >EQticks <instr_refl 1351 >set_clock_set_program_counter >set_clock_set_clock 1352 @set_program_counter_status_of_pseudo_status 1353 [1: 1354 >program_counter_set_program_counter 1355 whd in match compute_target_of_unconditional_jump; normalize nodelta 1356 <(eq_bv_eq … ppc_eq_bv_refl) % 1357 |2: 1358 @set_clock_status_of_pseudo_status try % /demod nohyps/ 1359 whd in match ticks_of0; normalize nodelta 1360 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1361 [1: 1362 >EQppc % 1363 |2: 1364 >sj_possible_refl % 1365 ] 1366 ] 1367 ] 1368 ] 1369 |14: (* JNC *) 1370 >EQP -P normalize nodelta 1371 whd in match assembly_1_pseudoinstruction; normalize nodelta 1372 whd in match expand_pseudo_instruction; normalize nodelta 1373 whd in match expand_relative_jump; normalize nodelta 1374 whd in match expand_relative_jump_internal; normalize nodelta 1375 >EQppc in ⊢ (% → ?); 1376 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1377 inversion sj_possible #sj_possible_refl normalize nodelta 1378 [1: 1379 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1380 whd in maps_assm:(??%%); 1381 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1382 whd in ⊢ (??%?); normalize nodelta 1383 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1384 whd in ⊢ (??%?); 1385 @if_then_else_status_of_pseudo_status 1386 >EQs >EQticks <instr_refl normalize nodelta 1387 [1: 1388 @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) % 1389 |2: 1390 @set_program_counter_status_of_pseudo_status 1391 [1: 1392 >EQaddr_of normalize nodelta 1393 whd in match addr_of_relative; normalize nodelta 1394 @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl)) 1395 [1: 1396 @sym_eq whd in ⊢ (??%?); >EQppc % 1397 |2: 1398 >EQlookup_labels % 1399 |3: 1400 >sj_possible_refl @I 1401 ] 1402 |2: 1403 @set_clock_status_of_pseudo_status try % 1404 whd in match ticks_of0; normalize nodelta 1405 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1406 [1: 1407 >EQppc % 1408 |2: 1409 >sj_possible_refl % 1410 ] 1411 ] 1412 |3: 1413 @set_clock_status_of_pseudo_status try % @eq_f2 try % 1414 whd in match ticks_of0; normalize nodelta 1415 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1416 [1: 1417 >EQppc % 1418 |2: 1419 >sj_possible_refl % 1420 ] 1421 ] 1422 |2: 1423 #sigma_increment_commutation #maps_assm 1424 whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1425 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1426 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1427 change with (execute 1 ?? = ?) 1428 whd in match execute_1; normalize nodelta 1429 whd in match execute_1'; normalize nodelta 1430 <jc_fetch_refl whd in match execute_1_0; normalize nodelta 1431 whd in match execute_1_preinstruction; normalize nodelta 1432 @(if_then_else_replace ???????? p) normalize nodelta 1433 [1: 1434 @eq_f >EQs 1435 whd in match get_cy_flag; normalize nodelta 1436 >special_function_registers_8051_set_program_counter 1437 <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try % 1438 normalize #absurd destruct(absurd) 1439 |2: 1440 @(if_then_else_replace ???????? p) normalize nodelta try % 1441 change with (execute_1 ?? = ?) 1442 whd in match execute_1; normalize nodelta 1443 whd in match execute_1'; normalize nodelta 1444 >program_counter_set_program_counter 1445 whd in match addr_of_relative; normalize nodelta 1446 >set_clock_set_program_counter >program_counter_set_program_counter 1447 <ljmp_fetch_refl 1448 change with (set_program_counter ???? = ?) 1449 >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter 1450 >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter 1451 >EQs >EQticks <instr_refl 1452 >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%); 1453 @set_program_counter_status_of_pseudo_status 1454 [1: 1455 >program_counter_set_program_counter 1456 whd in match compute_target_of_unconditional_jump; normalize nodelta 1457 >EQaddr_of normalize nodelta >EQlookup_labels % 1458 |2: 1459 >set_clock_set_clock 1460 @set_clock_status_of_pseudo_status try % 1461 /demod nohyps/ 1462 whd in match ticks_of0; normalize nodelta 1463 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1464 [1: 1465 >EQppc % 1466 |2: 1467 >sj_possible_refl % 1468 ] 1469 ] 1470 ] 1471 ] 1472 |15: (* JNC *) 1473 >EQP -P normalize nodelta 1474 whd in match assembly_1_pseudoinstruction; normalize nodelta 1475 whd in match expand_pseudo_instruction; normalize nodelta 1476 whd in match expand_relative_jump; normalize nodelta 1477 whd in match expand_relative_jump_internal; normalize nodelta 1478 >EQppc in ⊢ (% → ?); 1479 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1480 inversion sj_possible #sj_possible_refl normalize nodelta 1481 [1: 1482 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1483 whd in maps_assm:(??%%); 1484 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1485 whd in ⊢ (??%?); normalize nodelta 1486 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1487 whd in ⊢ (??%?); 1488 @if_then_else_status_of_pseudo_status 1489 >EQs >EQticks <instr_refl normalize nodelta 1490 [1: 1491 @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) % 1492 |2: 1493 @set_program_counter_status_of_pseudo_status 1494 [1: 1495 >EQaddr_of normalize nodelta 1496 whd in match addr_of_relative; normalize nodelta 1497 @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl)) 1498 [1: 1499 @sym_eq whd in ⊢ (??%?); >EQppc % 1500 |2: 1501 >EQlookup_labels % 1502 |3: 1503 >sj_possible_refl @I 1504 ] 1505 |2: 1506 @set_clock_status_of_pseudo_status try % 1507 whd in match ticks_of0; normalize nodelta 1508 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1509 [1: 1510 >EQppc % 1511 |2: 1512 >sj_possible_refl % 1513 ] 1514 ] 1515 |3: 1516 @set_clock_status_of_pseudo_status try % @eq_f2 try % 1517 whd in match ticks_of0; normalize nodelta 1518 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1519 [1: 1520 >EQppc % 1521 |2: 1522 >sj_possible_refl % 1523 ] 1524 ] 1525 |2: 1526 #sigma_increment_commutation #maps_assm 1527 whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1528 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1529 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1530 change with (execute 1 ?? = ?) 1531 whd in match execute_1; normalize nodelta 1532 whd in match execute_1'; normalize nodelta 1533 <jc_fetch_refl whd in match execute_1_0; normalize nodelta 1534 whd in match execute_1_preinstruction; normalize nodelta 1535 @(if_then_else_replace ???????? p) normalize nodelta 1536 [1: 1537 @eq_f >EQs 1538 whd in match get_cy_flag; normalize nodelta 1539 >special_function_registers_8051_set_program_counter 1540 <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try % 1541 normalize #absurd destruct(absurd) 1542 |2: 1543 @(if_then_else_replace ???????? p) normalize nodelta try % 1544 change with (execute_1 ?? = ?) 1545 whd in match execute_1; normalize nodelta 1546 whd in match execute_1'; normalize nodelta 1547 1548 >set_clock_set_program_counter 1549 >program_counter_set_program_counter 1550 <sjmp_fetch_refl 1551 change with (set_program_counter ???? = ?) 1552 >set_clock_set_program_counter >set_clock_set_program_counter 1553 >set_program_counter_set_program_counter >set_program_counter_set_program_counter 1554 >EQs >EQticks <instr_refl 1555 >set_clock_set_program_counter >set_clock_set_clock 1556 @set_program_counter_status_of_pseudo_status 1557 [1: 1558 >program_counter_set_program_counter 1559 whd in match compute_target_of_unconditional_jump; normalize nodelta 1560 <(eq_bv_eq … ppc_eq_bv_refl) % 1561 |2: 1562 @set_clock_status_of_pseudo_status try % /demod nohyps/ 1563 whd in match ticks_of0; normalize nodelta 1564 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1565 [1: 1566 >EQppc % 1567 |2: 1568 >sj_possible_refl % 1569 ] 1570 ] 1571 ] 1572 ] 1573 |16: (* JB *) 1574 >EQP -P normalize nodelta 1575 whd in match assembly_1_pseudoinstruction; normalize nodelta 1576 whd in match expand_pseudo_instruction; normalize nodelta 1577 whd in match expand_relative_jump; normalize nodelta 1578 whd in match expand_relative_jump_internal; normalize nodelta 1579 >EQppc in ⊢ (% → ?); 1580 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1581 inversion sj_possible #sj_possible_refl normalize nodelta 1582 [1: 1583 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1584 whd in maps_assm:(??%%); 1585 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1586 whd in ⊢ (??%?); normalize nodelta 1587 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1588 whd in ⊢ (??%?); 1589 @if_then_else_status_of_pseudo_status 1590 >EQs >EQticks <instr_refl normalize nodelta 1591 [1: 1592 @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try % 1593 @(subaddressing_mode_elim … addr1) #w whd 1594 |2: 1595 @set_program_counter_status_of_pseudo_status 1596 [1: 1597 >EQaddr_of normalize nodelta 1598 whd in match addr_of_relative; normalize nodelta 1599 @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl)) 1600 [1: 1601 @sym_eq whd in ⊢ (??%?); >EQppc % 1602 |2: 1603 >EQlookup_labels % 1604 |3: 1605 >sj_possible_refl @I 1606 ] 1607 |2: 1608 @set_clock_status_of_pseudo_status try % 1609 whd in match ticks_of0; normalize nodelta 1610 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1611 [1: 1612 >EQppc % 1613 |2: 1614 >sj_possible_refl % 1615 ] 1616 ] 1617 |3: 1618 @set_clock_status_of_pseudo_status try % @eq_f2 try % 1619 whd in match ticks_of0; normalize nodelta 1620 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1621 [1: 1622 >EQppc % 1623 |2: 1624 >sj_possible_refl % 1625 ] 1626 ] 1627 |2: 1628 #sigma_increment_commutation #maps_assm 1629 whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1630 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1631 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1632 change with (execute 1 ?? = ?) 1633 whd in match execute_1; normalize nodelta 1634 whd in match execute_1'; normalize nodelta 1635 <jc_fetch_refl whd in match execute_1_0; normalize nodelta 1636 whd in match execute_1_preinstruction; normalize nodelta 1637 @(if_then_else_replace ???????? p) normalize nodelta 1638 [1: 1639 @eq_f >EQs 1640 whd in match get_cy_flag; normalize nodelta 1641 >special_function_registers_8051_set_program_counter 1642 <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try % 1643 normalize #absurd destruct(absurd) 1644 |2: 1645 @(if_then_else_replace ???????? p) normalize nodelta try % 1646 change with (execute_1 ?? = ?) 1647 whd in match execute_1; normalize nodelta 1648 whd in match execute_1'; normalize nodelta 1649 >program_counter_set_program_counter 1650 whd in match addr_of_relative; normalize nodelta 1651 >set_clock_set_program_counter >program_counter_set_program_counter 1652 <ljmp_fetch_refl 1653 change with (set_program_counter ???? = ?) 1654 >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter 1655 >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter 1656 >EQs >EQticks <instr_refl 1657 >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%); 1658 @set_program_counter_status_of_pseudo_status 1659 [1: 1660 >program_counter_set_program_counter 1661 whd in match compute_target_of_unconditional_jump; normalize nodelta 1662 >EQaddr_of normalize nodelta >EQlookup_labels % 1663 |2: 1664 >set_clock_set_clock 1665 @set_clock_status_of_pseudo_status try % 1666 /demod nohyps/ 1667 whd in match ticks_of0; normalize nodelta 1668 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1669 [1: 1670 >EQppc % 1671 |2: 1672 >sj_possible_refl % 1673 ] 1674 ] 1675 ] 1676 ] 1677 |16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1224 1678 cases daemon 1225 1679 |(*29,30: (* ANL and ORL *)
Note: See TracChangeset
for help on using the changeset viewer.
