Changeset 2283 for src/ASM


Ignore:
Timestamp:
Jul 31, 2012, 6:11:27 PM (8 years ago)
Author:
mulligan
Message:

Work from today.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2282 r2283  
    1818include alias "ASM/Vector.ma".
    1919include "ASM/Test.ma".
    20 include "ASM/Test2.ma".
     20(*include "ASM/Test2.ma".*)
    2121
    2222(*CSC: move elsewhere*)
    … …  
    9090  <(eq_bv_eq … relevant)
    9191  >(vsplit_ok … (sym_eq … vsplit_refl)) %
     92qed.
     93
     94lemma 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' %
    9298qed.
    9399
    … …  
    12151221      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
    12161222      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 *)
    12241678    cases daemon
    12251679  |(*29,30: (* ANL and ORL *)

  • src/ASM/Interpret.ma

    r2280 r2283  
    162162              [ ACC_A ⇒ λacc_a: True.
    163163                let s' ≝ add_ticks1 s in
    164                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     164                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
    165165                 set_arg_8 … s' ACC_A result
    166166              | REGISTER r ⇒ λregister: True.
    167167                let s' ≝ add_ticks1 s in
    168                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     168                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    169169                 set_arg_8 … s' (REGISTER r) result
    170170              | DIRECT d ⇒ λdirect: True.
    171171                let s' ≝ add_ticks1 s in
    172                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     172                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    173173                 set_arg_8 … s' (DIRECT d) result
    174174              | INDIRECT i ⇒ λindirect: True.
    175175                let s' ≝ add_ticks1 s in
    176                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     176                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    177177                 set_arg_8 … s' (INDIRECT i) result
    178178              | DPTR ⇒ λdptr: True.
    179179                let s' ≝ add_ticks1 s in
    180                 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
     180                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
    182182                let s ≝ set_8051_sfr … s' SFR_DPL bl in
    183183                 set_8051_sfr … s' SFR_DPH bu
    … …  
    222222                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    223223                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    224                     let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     224                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
    225225                    let new_acc ≝ nu @@ acc_nl' in
    226226                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
    … …  
    582582              [ ACC_A ⇒ λacc_a: True. λEQaddr.
    583583                let s' ≝ add_ticks1 s in
    584                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     584                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
    585585                 set_arg_8 … s' ACC_A result
    586586              | REGISTER r ⇒ λregister: True. λEQaddr.
    587587                let s' ≝ add_ticks1 s in
    588                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     588                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    589589                 set_arg_8 … s' (REGISTER r) result
    590590              | DIRECT d ⇒ λdirect: True. λEQaddr.
    591591                let s' ≝ add_ticks1 s in
    592                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     592                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    593593                 set_arg_8 … s' (DIRECT d) result
    594594              | INDIRECT i ⇒ λindirect: True. λEQaddr.
    595595                let s' ≝ add_ticks1 s in
    596                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     596                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    597597                 set_arg_8 … s' (INDIRECT i) result
    598598              | DPTR ⇒ λdptr: True. λEQaddr.
    599599                let s' ≝ add_ticks1 s in
    600                 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
     600                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
    602602                let s ≝ set_8051_sfr … s' SFR_DPL bl in
    603603                 set_8051_sfr … s' SFR_DPH bu
    … …  
    642642                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    643643                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    644                     let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     644                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
    645645                    let new_acc ≝ nu @@ acc_nl' in
    646646                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
    … …  
    721721              [ DIRECT d ⇒ λdirect: True. λEQaddr.
    722722                let s ≝ add_ticks1 s in
    723                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     723                let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    724724                let s ≝ set_8051_sfr … s SFR_SP new_sp in
    725725                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
    … …  
    969969        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
    970970        [ 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)
    973972        | _ ⇒ λother: False. ⊥
    974973        ] (subaddressing_modein … addr)
    … …  
    10341033              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    10351034              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 in
     1035              let new_addr ≝ add … dptr big_acc in
    10371036              let result ≝ lookup ? ? new_addr cm (zero ?) in
    10381037                set_8051_sfr … s SFR_ACC_A result
    … …  
    10411040              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    10421041              (*      addition of the PC with the DPTR? At the moment, no.              *)
    1043               let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
     1042              let new_addr ≝ add … (program_counter … s) big_acc in
    10441043              let result ≝ lookup ? ? new_addr cm (zero ?) in
    10451044                set_8051_sfr … s SFR_ACC_A result
    … …  
    10501049          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    10511050          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    1052           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    1053           let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
     1051          let jmp_addr ≝ add … big_acc dptr in
     1052          let new_pc ≝ add … (program_counter … s) jmp_addr in
    10541053            set_program_counter … s new_pc
    10551054      | LJMP addr ⇒ λinstr_refl.
    … …  
    10691068          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    10701069            [ ADDR11 a ⇒ λaddr11: True.
    1071               «let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1070              «let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10721071              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10731072              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    10741073              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) in
     1074              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10761075              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10771076              let s ≝ write_at_stack_pointer … s pc_bu in
    … …  
    10871086            [ ADDR16 a ⇒ λaddr16: True.
    10881087              «
    1089               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1088              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10901089              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10911090              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    10921091              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) in
     1092              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10941093              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10951094              let s ≝ write_at_stack_pointer … s pc_bu in
    … …  
    11051104    try (#absurd normalize in absurd; try destruct(absurd) try %)
    11061105    @pair_elim #carry #new_sp #carry_new_sp_refl
    1107     @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl
    1108     @pair_elim #carry' #new_sp' #carry_new_sp_refl'
    11091106    [2:
    11101107      /demod nohyps/ %
    … …  
    11961193      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    11971194      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) in
     1195      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    11991196      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    12001197      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    12011198      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) in
     1199      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12031200      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    12041201      let s ≝ write_at_stack_pointer … s pc_bu in
Note: See TracChangeset for help on using the changeset viewer.