Changeset 936 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 10, 2011, 4:20:47 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r935 r936 834 834 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 835 835 836 definition ticks_of_instruction ≝ 837 λi. 838 let trivial_code_memory ≝ assembly1 i in 839 let trivial_status ≝ load_code_memory trivial_code_memory in 840 \snd (fetch trivial_status (zero ?)). 841 836 842 axiom fetch_assembly: 837 843 ∀pc,i,code_memory,assembled. … … 842 848 let 〈instr_pc, ticks〉 ≝ fetched in 843 849 let 〈instr,pc'〉 ≝ instr_pc in 844 (eq_instruction instr i ∧ eq _bv … pc' (bitvector_of_nat … (pc + len))) = true.850 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 845 851 (* #pc #i #code_memory #assembled cases i [8: *] 846 852 [16,20,29: * * 18,19: * * [1,2,4,5: *] 28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] … … 876 882 let 〈instr_pc, ticks〉 ≝ fetched in 877 883 let 〈instr,pc'〉 ≝ instr_pc in 878 eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl]. 884 eq_instruction instr i = true ∧ 885 ticks = (ticks_of_instruction i) ∧ 886 fetch_many code_memory final_pc pc' tl]. 879 887 880 888 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. … … 887 895 888 896 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2. 897 898 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 889 899 890 900 lemma fetch_assembly_pseudo: … … 906 916 generalize in match (fetch_assembly pc i code_memory … (refl …) H1) 907 917 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) 908 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) K; #K1 #K2 % // 909 >(eq_bv_to_eq … K2) @IH @H2 ] 918 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) K; #K1 919 cases (conjunction_true … K1) K1; #K1 #K2 #K3 % try % // 920 [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) //  >(eq_bv_to_eq … K3) @IH @H2 ] 910 921 qed. 911 922 … … 1602 1613 qed. 1603 1614 1604 definition ticks_of : pseudo_assembly_program → Word→ nat × nat ≝1615 definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝ 1605 1616 λprogram: pseudo_assembly_program. 1606 1617 λppc: Word. 1607 let 〈preamble, pseudo〉 ≝ program in 1608 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1618 λfetched. 1609 1619 match fetched with 1610 1620 [ Instruction instr ⇒ … … 1664 1674  long_jump ⇒ 〈4, 4〉 1665 1675 ] 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〉 1676  ADD arg1 arg2 ⇒ 1677 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in 1678 〈ticks, ticks〉 1671 1679  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〉 1680 let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in 1681 〈ticks, ticks〉 1676 1682  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〉 1683 let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in 1684 〈ticks, ticks〉 1681 1685  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 let ticks ≝ ticks_of_instruction (INC ? arg) in 1687 〈ticks, ticks〉 1686 1688  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〉 1689 let ticks ≝ ticks_of_instruction (DEC ? arg) in 1690 〈ticks, ticks〉 1691 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〉 1692 let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in 1693 〈ticks, ticks〉 1696 1694  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〉 1695 let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in 1696 〈ticks, ticks〉 1701 1697  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〉 1698 let ticks ≝ ticks_of_instruction (DA ? arg) in 1699 〈ticks, ticks〉 1706 1700  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〉 1701 let ticks ≝ ticks_of_instruction (ANL ? arg) in 1702 〈ticks, ticks〉 1711 1703  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〉 1704 let ticks ≝ ticks_of_instruction (ORL ? arg) in 1705 〈ticks, ticks〉 1716 1706  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〉 1707 let ticks ≝ ticks_of_instruction (XRL ? arg) in 1708 〈ticks, ticks〉 1721 1709  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〉 1710 let ticks ≝ ticks_of_instruction (CLR ? arg) in 1711 〈ticks, ticks〉 1726 1712  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〉 1713 let ticks ≝ ticks_of_instruction (CPL ? arg) in 1714 〈ticks, ticks〉 1731 1715  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〉 1716 let ticks ≝ ticks_of_instruction (RL ? arg) in 1717 〈ticks, ticks〉 1736 1718  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〉 1719 let ticks ≝ ticks_of_instruction (RLC ? arg) in 1720 〈ticks, ticks〉 1741 1721  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〉 1722 let ticks ≝ ticks_of_instruction (RR ? arg) in 1723 〈ticks, ticks〉 1746 1724  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〉 1725 let ticks ≝ ticks_of_instruction (RRC ? arg) in 1726 〈ticks, ticks〉 1751 1727  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〉 1728 let ticks ≝ ticks_of_instruction (SWAP ? arg) in 1729 〈ticks, ticks〉 1756 1730  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〉 1731 let ticks ≝ ticks_of_instruction (MOV ? arg) in 1732 〈ticks, ticks〉 1761 1733  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〉 1734 let ticks ≝ ticks_of_instruction (MOVX ? arg) in 1735 〈ticks, ticks〉 1766 1736  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〉 1737 let ticks ≝ ticks_of_instruction (SETB ? arg) in 1738 〈ticks, ticks〉 1771 1739  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〉 1740 let ticks ≝ ticks_of_instruction (PUSH ? arg) in 1741 〈ticks, ticks〉 1776 1742  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〉 1743 let ticks ≝ ticks_of_instruction (POP ? arg) in 1744 〈ticks, ticks〉 1781 1745  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〉 1746 let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in 1747 〈ticks, ticks〉 1786 1748  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〉 1749 let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in 1750 〈ticks, ticks〉 1791 1751  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〉 1752 let ticks ≝ ticks_of_instruction (RET ?) in 1753 〈ticks, ticks〉 1796 1754  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〉 1755 let ticks ≝ ticks_of_instruction (RETI ?) in 1756 〈ticks, ticks〉 1801 1757  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〉 1758 let ticks ≝ ticks_of_instruction (NOP ?) in 1759 〈ticks, ticks〉 1806 1760 ] 1807 1761  Comment comment ⇒ 〈0, 0〉 … … 1814 1768 qed. 1815 1769 1816 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1770 definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝ 1771 λprogram: pseudo_assembly_program. 1772 λppc: Word. 1773 let 〈preamble, pseudo〉 ≝ program in 1774 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1775 ticks_of0 program ppc fetched. 1817 1776 1818 1777 lemma get_register_set_program_counter: … … 1844 1803 qed. 1845 1804 1846 lemma set_arg_8_set_program_counter:1847 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →1848 ∀T,s.∀pc:Word.∀b:l.1849 set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b.1850 [2,3: cases b; *; normalize //]1851 #n #l #prf #T #s #pc #b * *;1852 qed.1853 1854 1805 lemma get_arg_8_set_code_memory: 1855 1806 ∀T1,T2,s,code_mem,b,arg. … … 1877 1828 #T1 #s #f1 #f2 #f3 % 1878 1829 qed. 1879 1880 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.1881 1830 1882 1831 lemma eq_rect_Type1_r: … … 1892 1841 1893 1842 lemma main_thm: 1894 ∀ticks_of.1895 1843 ∀ps,s,s''. 1896 1844 status_of_pseudo_status ps = Some … s → 1897 status_of_pseudo_status (execute_1_pseudo_instruction ticks_ofps) = Some … s'' →1845 status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' → 1898 1846 ∃n. execute n s = s''. 1899 # ticks_of #ps #s #s''1847 #ps #s #s'' 1900 1848 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1901 1849 whd in ⊢ (? → ??%? → ??%? → ?) … … 1917 1865 (∃n. 1918 1866 execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1919 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_ofps) (load_code_memory assembled)) ?)1867 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?) 1920 1868 whd in match (\snd 〈preamble,instr_list〉) in H; 1921 1869 whd in match (\fst 〈preamble,instr_list〉) in H; 1922 1870 whd in match (\snd 〈final_pc,assembled〉) in H; 1923 1871 s s'' labels costs final_ppc final_pc; 1924 letin ps' ≝ (execute_1_pseudo_instruction ticks_ofps)1872 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps) 1925 1873 (* NICE STATEMENT HERE *) 1926 1874 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; ps'; #ps' 1927 1875 #K <K generalize in match K; K; 1928 1876 (* STATEMENT WITH EQUALITY HERE *) 1929 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta; 1877 whd in ⊢ (???(?%?) → ?) 1878 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) H; >EQ0 normalize nodelta; 1930 1879 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 1931 1880 #pi #newppc normalize nodelta; * #instructions *; … … 1933 1882 [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0] 1934 1883 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1935 #H2 >(eq_bv_to_eq … H2) > ignore_clock in EQ; #EQ >EQ %1884 #H2 >(eq_bv_to_eq … H2) >EQ % 1936 1885 4: (* Jmp *) 1937 1886 5: (* Call *) … … 1942 1891 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1943 1892 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1944 * #H2a whd in ⊢ (% → ?) #H2b 1945 >ignore_clock in EQ; 1946 >(eq_instruction_to_eq … H2a) 1947 whd in ⊢ (???% → ??%?); 1948 >ignore_clock 1893 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1894 >H2b >(eq_instruction_to_eq … H2a) 1895 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); 1949 1896 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; 1950 1897 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 … … 1952 1899 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 1953 1900 #result #flags 1954 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2 b) newppc';%1901 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % 1955 1902  (* INC *) #arg1 #H1 #H2 #EQ %[@1] 1956 1903 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1957 1904 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1958 1905 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1959 * #H2a whd in ⊢ (% → ?) #H2b 1960 >ignore_clock in EQ; 1961 >(eq_instruction_to_eq … H2a) 1962 whd in ⊢ (???% → ??%?); 1963 >ignore_clock 1906 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1907 >H2b >(eq_instruction_to_eq … H2a) 1908 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); 1964 1909 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; normalize nodelta; [1,2,3: #ARG] 1965 1910 [1,2,3,4: cases (half_add ???) #carry #result 1966 1911  cases (half_add ???) #carry #bl normalize nodelta; 1967 1912 cases (full_add ????) #carry' #bu normalize nodelta ] 1968 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2 b) newppc';1913 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) newppc'; 1969 1914 [5: % 1970 1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1971 1972 XXX 1973 % 1974 1915 1:
Note: See TracChangeset
for help on using the changeset viewer.