Changeset 929
 Timestamp:
 Jun 9, 2011, 6:40:44 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r926 r929 1602 1602 qed. 1603 1603 1604 definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝ 1605 λprogram: pseudo_assembly_program. 1606 λppc: Word. 1607 let 〈preamble, pseudo〉 ≝ program in 1608 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1609 match fetched with 1610 [ Instruction instr ⇒ 1611 match instr with 1612 [ JC lbl ⇒ 1613 match jump_expansion ppc program with 1614 [ short_jump ⇒ 〈2, 2〉 1615  medium_jump ⇒ ? 1616  long_jump ⇒ 〈4, 4〉 1617 ] 1618  JNC lbl ⇒ 1619 match jump_expansion ppc program with 1620 [ short_jump ⇒ 〈2, 2〉 1621  medium_jump ⇒ ? 1622  long_jump ⇒ 〈4, 4〉 1623 ] 1624  JB bit lbl ⇒ 1625 match jump_expansion ppc program with 1626 [ short_jump ⇒ 〈2, 2〉 1627  medium_jump ⇒ ? 1628  long_jump ⇒ 〈4, 4〉 1629 ] 1630  JNB bit lbl ⇒ 1631 match jump_expansion ppc program with 1632 [ short_jump ⇒ 〈2, 2〉 1633  medium_jump ⇒ ? 1634  long_jump ⇒ 〈4, 4〉 1635 ] 1636  JBC bit lbl ⇒ 1637 match jump_expansion ppc program with 1638 [ short_jump ⇒ 〈2, 2〉 1639  medium_jump ⇒ ? 1640  long_jump ⇒ 〈4, 4〉 1641 ] 1642  JZ lbl ⇒ 1643 match jump_expansion ppc program with 1644 [ short_jump ⇒ 〈2, 2〉 1645  medium_jump ⇒ ? 1646  long_jump ⇒ 〈4, 4〉 1647 ] 1648  JNZ lbl ⇒ 1649 match jump_expansion ppc program with 1650 [ short_jump ⇒ 〈2, 2〉 1651  medium_jump ⇒ ? 1652  long_jump ⇒ 〈4, 4〉 1653 ] 1654  CJNE arg lbl ⇒ 1655 match jump_expansion ppc program with 1656 [ short_jump ⇒ 〈2, 2〉 1657  medium_jump ⇒ ? 1658  long_jump ⇒ 〈4, 4〉 1659 ] 1660  DJNZ arg lbl ⇒ 1661 match jump_expansion ppc program with 1662 [ short_jump ⇒ 〈2, 2〉 1663  medium_jump ⇒ ? 1664  long_jump ⇒ 〈4, 4〉 1665 ] 1666  ADD arg1 arg2 ⇒ 1667 let trivial_code_memory ≝ assembly1 (ADD ? arg1 arg2) in 1668 let trivial_status ≝ load_code_memory trivial_code_memory in 1669 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1670 〈0, ticks〉 1671  ADDC arg1 arg2 ⇒ 1672 let trivial_code_memory ≝ assembly1 (ADDC ? arg1 arg2) in 1673 let trivial_status ≝ load_code_memory trivial_code_memory in 1674 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1675 〈0, ticks〉 1676  SUBB arg1 arg2 ⇒ 1677 let trivial_code_memory ≝ assembly1 (SUBB ? arg1 arg2) in 1678 let trivial_status ≝ load_code_memory trivial_code_memory in 1679 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1680 〈0, ticks〉 1681  INC arg ⇒ 1682 let trivial_code_memory ≝ assembly1 (INC ? arg) in 1683 let trivial_status ≝ load_code_memory trivial_code_memory in 1684 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1685 〈0, ticks〉 1686  DEC arg ⇒ 1687 let trivial_code_memory ≝ assembly1 (DEC ? arg) in 1688 let trivial_status ≝ load_code_memory trivial_code_memory in 1689 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1690 〈0, ticks〉 1691  MUL arg1 arg2 ⇒ 1692 let trivial_code_memory ≝ assembly1 (MUL ? arg1 arg2) in 1693 let trivial_status ≝ load_code_memory trivial_code_memory in 1694 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1695 〈0, ticks〉 1696  DIV arg1 arg2 ⇒ 1697 let trivial_code_memory ≝ assembly1 (DIV ? arg1 arg2) in 1698 let trivial_status ≝ load_code_memory trivial_code_memory in 1699 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1700 〈0, ticks〉 1701  DA arg ⇒ 1702 let trivial_code_memory ≝ assembly1 (DA ? arg) in 1703 let trivial_status ≝ load_code_memory trivial_code_memory in 1704 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1705 〈0, ticks〉 1706  ANL arg ⇒ 1707 let trivial_code_memory ≝ assembly1 (ANL ? arg) in 1708 let trivial_status ≝ load_code_memory trivial_code_memory in 1709 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1710 〈0, ticks〉 1711  ORL arg ⇒ 1712 let trivial_code_memory ≝ assembly1 (ORL ? arg) in 1713 let trivial_status ≝ load_code_memory trivial_code_memory in 1714 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1715 〈0, ticks〉 1716  XRL arg ⇒ 1717 let trivial_code_memory ≝ assembly1 (XRL ? arg) in 1718 let trivial_status ≝ load_code_memory trivial_code_memory in 1719 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1720 〈0, ticks〉 1721  CLR arg ⇒ 1722 let trivial_code_memory ≝ assembly1 (CLR ? arg) in 1723 let trivial_status ≝ load_code_memory trivial_code_memory in 1724 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1725 〈0, ticks〉 1726  CPL arg ⇒ 1727 let trivial_code_memory ≝ assembly1 (CPL ? arg) in 1728 let trivial_status ≝ load_code_memory trivial_code_memory in 1729 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1730 〈0, ticks〉 1731  RL arg ⇒ 1732 let trivial_code_memory ≝ assembly1 (RL ? arg) in 1733 let trivial_status ≝ load_code_memory trivial_code_memory in 1734 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1735 〈0, ticks〉 1736  RLC arg ⇒ 1737 let trivial_code_memory ≝ assembly1 (RLC ? arg) in 1738 let trivial_status ≝ load_code_memory trivial_code_memory in 1739 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1740 〈0, ticks〉 1741  RR arg ⇒ 1742 let trivial_code_memory ≝ assembly1 (RR ? arg) in 1743 let trivial_status ≝ load_code_memory trivial_code_memory in 1744 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1745 〈0, ticks〉 1746  RRC arg ⇒ 1747 let trivial_code_memory ≝ assembly1 (RRC ? arg) in 1748 let trivial_status ≝ load_code_memory trivial_code_memory in 1749 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1750 〈0, ticks〉 1751  SWAP arg ⇒ 1752 let trivial_code_memory ≝ assembly1 (SWAP ? arg) in 1753 let trivial_status ≝ load_code_memory trivial_code_memory in 1754 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1755 〈0, ticks〉 1756  MOV arg ⇒ 1757 let trivial_code_memory ≝ assembly1 (MOV ? arg) in 1758 let trivial_status ≝ load_code_memory trivial_code_memory in 1759 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1760 〈0, ticks〉 1761  MOVX arg ⇒ 1762 let trivial_code_memory ≝ assembly1 (MOVX ? arg) in 1763 let trivial_status ≝ load_code_memory trivial_code_memory in 1764 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1765 〈0, ticks〉 1766  SETB arg ⇒ 1767 let trivial_code_memory ≝ assembly1 (SETB ? arg) in 1768 let trivial_status ≝ load_code_memory trivial_code_memory in 1769 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1770 〈0, ticks〉 1771  PUSH arg ⇒ 1772 let trivial_code_memory ≝ assembly1 (PUSH ? arg) in 1773 let trivial_status ≝ load_code_memory trivial_code_memory in 1774 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1775 〈0, ticks〉 1776  POP arg ⇒ 1777 let trivial_code_memory ≝ assembly1 (POP ? arg) in 1778 let trivial_status ≝ load_code_memory trivial_code_memory in 1779 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1780 〈0, ticks〉 1781  XCH arg1 arg2 ⇒ 1782 let trivial_code_memory ≝ assembly1 (XCH ? arg1 arg2) in 1783 let trivial_status ≝ load_code_memory trivial_code_memory in 1784 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1785 〈0, ticks〉 1786  XCHD arg1 arg2 ⇒ 1787 let trivial_code_memory ≝ assembly1 (XCHD ? arg1 arg2) in 1788 let trivial_status ≝ load_code_memory trivial_code_memory in 1789 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1790 〈0, ticks〉 1791  RET ⇒ 1792 let trivial_code_memory ≝ assembly1 (RET ?) in 1793 let trivial_status ≝ load_code_memory trivial_code_memory in 1794 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1795 〈0, ticks〉 1796  RETI ⇒ 1797 let trivial_code_memory ≝ assembly1 (RETI ?) in 1798 let trivial_status ≝ load_code_memory trivial_code_memory in 1799 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1800 〈0, ticks〉 1801  NOP ⇒ 1802 let trivial_code_memory ≝ assembly1 (NOP ?) in 1803 let trivial_status ≝ load_code_memory trivial_code_memory in 1804 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1805 〈0, ticks〉 1806 ] 1807  Comment comment ⇒ 〈0, 0〉 1808  Cost cost ⇒ 〈0, 0〉 1809  Jmp jmp ⇒ 〈0, 2〉 1810  Call call ⇒ 〈0, 2〉 1811  Mov dptr tgt ⇒ 〈0, 2〉 1812 ]. 1813 cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *) 1814 qed. 1815 1604 1816 lemma main_thm: 1605 1817 ∀ticks_of.
Note: See TracChangeset
for help on using the changeset viewer.