 Timestamp:
 Jul 31, 2012, 6:11:27 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
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 *) 
src/ASM/Interpret.ma
r2280 r2283 162 162 [ ACC_A ⇒ λacc_a: True. 163 163 let s' ≝ add_ticks1 s in 164 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in164 let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 165 165 set_arg_8 … s' ACC_A result 166 166  REGISTER r ⇒ λregister: True. 167 167 let s' ≝ add_ticks1 s in 168 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in168 let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 169 169 set_arg_8 … s' (REGISTER r) result 170 170  DIRECT d ⇒ λdirect: True. 171 171 let s' ≝ add_ticks1 s in 172 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in172 let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 173 173 set_arg_8 … s' (DIRECT d) result 174 174  INDIRECT i ⇒ λindirect: True. 175 175 let s' ≝ add_ticks1 s in 176 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in176 let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 177 177 set_arg_8 … s' (INDIRECT i) result 178 178  DPTR ⇒ λdptr: True. 179 179 let s' ≝ add_ticks1 s in 180 let 〈 carry, bl 〉 ≝ half_add ?(get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in181 let 〈 carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in180 let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 181 let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 182 182 let s ≝ set_8051_sfr … s' SFR_DPL bl in 183 183 set_8051_sfr … s' SFR_DPH bu … … 222 222 let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in 223 223 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 224 let 〈 carry, nu 〉 ≝ half_add ?acc_nu' (bitvector_of_nat 4 6) in224 let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in 225 225 let new_acc ≝ nu @@ acc_nl' in 226 226 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in … … 582 582 [ ACC_A ⇒ λacc_a: True. λEQaddr. 583 583 let s' ≝ add_ticks1 s in 584 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in584 let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 585 585 set_arg_8 … s' ACC_A result 586 586  REGISTER r ⇒ λregister: True. λEQaddr. 587 587 let s' ≝ add_ticks1 s in 588 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in588 let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 589 589 set_arg_8 … s' (REGISTER r) result 590 590  DIRECT d ⇒ λdirect: True. λEQaddr. 591 591 let s' ≝ add_ticks1 s in 592 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in592 let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 593 593 set_arg_8 … s' (DIRECT d) result 594 594  INDIRECT i ⇒ λindirect: True. λEQaddr. 595 595 let s' ≝ add_ticks1 s in 596 let 〈 carry, result 〉 ≝ half_add ?(get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in596 let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 597 597 set_arg_8 … s' (INDIRECT i) result 598 598  DPTR ⇒ λdptr: True. λEQaddr. 599 599 let s' ≝ add_ticks1 s in 600 let 〈 carry, bl 〉 ≝ half_add ?(get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in601 let 〈 carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in600 let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 601 let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 602 602 let s ≝ set_8051_sfr … s' SFR_DPL bl in 603 603 set_8051_sfr … s' SFR_DPH bu … … 642 642 let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in 643 643 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 644 let 〈 carry, nu 〉 ≝ half_add ?acc_nu' (bitvector_of_nat 4 6) in644 let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in 645 645 let new_acc ≝ nu @@ acc_nl' in 646 646 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in … … 721 721 [ DIRECT d ⇒ λdirect: True. λEQaddr. 722 722 let s ≝ add_ticks1 s in 723 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in723 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 724 724 let s ≝ set_8051_sfr … s SFR_SP new_sp in 725 725 write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d)) … … 969 969 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 970 970 [ RELATIVE r ⇒ λrelative: True. 971 let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in 972 new_pc 971 add … program_counter (sign_extension r) 973 972  _ ⇒ λother: False. ⊥ 974 973 ] (subaddressing_modein … addr) … … 1034 1033 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 1035 1034 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 1036 let 〈carry, new_addr〉 ≝ half_add ?dptr big_acc in1035 let new_addr ≝ add … dptr big_acc in 1037 1036 let result ≝ lookup ? ? new_addr cm (zero ?) in 1038 1037 set_8051_sfr … s SFR_ACC_A result … … 1041 1040 (* DPM: Under specified: does the carry from PC incrementation affect the *) 1042 1041 (* addition of the PC with the DPTR? At the moment, no. *) 1043 let 〈carry, new_addr〉 ≝ half_add ?(program_counter … s) big_acc in1042 let new_addr ≝ add … (program_counter … s) big_acc in 1044 1043 let result ≝ lookup ? ? new_addr cm (zero ?) in 1045 1044 set_8051_sfr … s SFR_ACC_A result … … 1050 1049 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 1051 1050 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 1052 let 〈carry, jmp_addr〉 ≝ half_add ?big_acc dptr in1053 let 〈carry, new_pc〉 ≝ half_add ?(program_counter … s) jmp_addr in1051 let jmp_addr ≝ add … big_acc dptr in 1052 let new_pc ≝ add … (program_counter … s) jmp_addr in 1054 1053 set_program_counter … s new_pc 1055 1054  LJMP addr ⇒ λinstr_refl. … … 1069 1068 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 1070 1069 [ ADDR11 a ⇒ λaddr11: True. 1071 «let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1070 «let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1072 1071 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1073 1072 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1074 1073 let s ≝ write_at_stack_pointer … s pc_bl in 1075 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1074 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1076 1075 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1077 1076 let s ≝ write_at_stack_pointer … s pc_bu in … … 1087 1086 [ ADDR16 a ⇒ λaddr16: True. 1088 1087 « 1089 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1088 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1090 1089 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1091 1090 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1092 1091 let s ≝ write_at_stack_pointer … s pc_bl in 1093 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1092 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1094 1093 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1095 1094 let s ≝ write_at_stack_pointer … s pc_bu in … … 1105 1104 try (#absurd normalize in absurd; try destruct(absurd) try %) 1106 1105 @pair_elim #carry #new_sp #carry_new_sp_refl 1107 @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl1108 @pair_elim #carry' #new_sp' #carry_new_sp_refl'1109 1106 [2: 1110 1107 /demod nohyps/ % … … 1196 1193 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 1197 1194 let a ≝ address_of_word_labels (\snd cm) call in 1198 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1195 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1199 1196 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1200 1197 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1201 1198 let s ≝ write_at_stack_pointer … s pc_bl in 1202 let 〈carry, new_sp〉 ≝ half_add ?(get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in1199 let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1203 1200 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1204 1201 let s ≝ write_at_stack_pointer … s pc_bu in
Note: See TracChangeset
for help on using the changeset viewer.