Ignore:
Timestamp:
Jun 9, 2011, 6:40:44 PM (9 years ago)
Author:
mulligan
Message:

added ticks_of function

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r926 r929  
    16021602qed.
    16031603
     1604definition 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 *)
     1814qed.
     1815
    16041816lemma main_thm:
    16051817 ∀ticks_of.
Note: See TracChangeset for help on using the changeset viewer.