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

Work from today.

File:
1 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 *)
Note: See TracChangeset for help on using the changeset viewer.