 Timestamp:
 Jun 10, 2011, 6:49:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r939 r940 1802 1802 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y % 1803 1803 qed. 1804 1805 lemma set_bit_addressable_sfr_set_code_memory: 1806 ∀T, U: Type[0]. 1807 ∀ps: PreStatus ?. 1808 ∀code_mem. 1809 ∀x. 1810 ∀val. 1811 set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val = 1812 set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem. 1813 #T #U #ps #code_mem #x #val 1814 whd in ⊢ (??%?) 1815 whd in ⊢ (???(???%?)) 1816 cases (eqb ? 128) [ normalize nodelta cases not_implemented 1817  normalize nodelta 1818 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented 1819  normalize nodelta 1820 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented 1821  normalize nodelta 1822 cases (eqb ? 176) [ normalize nodelta % 1823  normalize nodelta 1824 cases (eqb ? 153) [ normalize nodelta % 1825  normalize nodelta 1826 cases (eqb ? 138) [ normalize nodelta % 1827  normalize nodelta 1828 cases (eqb ? 139) [ normalize nodelta % 1829  normalize nodelta 1830 cases (eqb ? 140) [ normalize nodelta % 1831  normalize nodelta 1832 cases (eqb ? 141) [ normalize nodelta % 1833  normalize nodelta 1834 cases (eqb ? 200) [ normalize nodelta % 1835  normalize nodelta 1836 cases (eqb ? 202) [ normalize nodelta % 1837  normalize nodelta 1838 cases (eqb ? 203) [ normalize nodelta % 1839  normalize nodelta 1840 cases (eqb ? 204) [ normalize nodelta % 1841  normalize nodelta 1842 cases (eqb ? 205) [ normalize nodelta % 1843  normalize nodelta 1844 cases (eqb ? 135) [ normalize nodelta % 1845  normalize nodelta 1846 cases (eqb ? 136) [ normalize nodelta % 1847  normalize nodelta 1848 cases (eqb ? 137) [ normalize nodelta % 1849  normalize nodelta 1850 cases (eqb ? 152) [ normalize nodelta % 1851  normalize nodelta 1852 cases (eqb ? 168) [ normalize nodelta % 1853  normalize nodelta 1854 cases (eqb ? 184) [ normalize nodelta % 1855  normalize nodelta 1856 cases (eqb ? 129) [ normalize nodelta % 1857  normalize nodelta 1858 cases (eqb ? 130) [ normalize nodelta % 1859  normalize nodelta 1860 cases (eqb ? 131) [ normalize nodelta % 1861  normalize nodelta 1862 cases (eqb ? 208) [ normalize nodelta % 1863  normalize nodelta 1864 cases (eqb ? 224) [ normalize nodelta % 1865  normalize nodelta 1866 cases (eqb ? 240) [ normalize nodelta % 1867  normalize nodelta 1868 cases not_implemented 1869 ]]]]]]]]]]]]]]]]]]]]]]]]]] 1870 qed. 1871 1872 lemma set_arg_8_set_code_memory: 1873 ∀n:nat. 1874 ∀l:Vector addressing_mode_tag (S n). 1875 ¬(is_in ? l ACC_PC) → 1876 ∀T: Type[0]. 1877 ∀U: Type[0]. 1878 ∀ps: PreStatus ?. 1879 ∀code_mem. 1880 ∀val. 1881 ∀b: l. 1882 set_arg_8 ? (set_code_memory T U ps code_mem) b val = 1883 set_code_memory T U (set_arg_8 ? ps b val) code_mem. 1884 [2,3: cases b; *; normalize //] 1885 #n #l #prf #T #U #ps #code_mem #val * *; 1886 [*: 1887 [1,2,3,4,8,9,15,16,17,18,19: #x] 1888 try #y whd in ⊢ (??(%)?) 1889 whd in ⊢ (???(???(%)?)) 1890 [1,2: 1891 cases (split bool 4 4 ?) 1892 #nu' #nl' 1893 normalize nodelta 1894 cases (split bool 1 3 nu') 1895 #bit1' #ignore' 1896 normalize nodelta 1897 cases (get_index_v bool 4 nu' 1 ?) 1898 [1,2,3,4: 1899 normalize nodelta 1900 try % 1901 try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val)) 1902 try (normalize in ⊢ (???(???%?))) 1903 ] 1904 3,4: % 1905 *: 1906 try normalize nodelta 1907 normalize cases (not_implemented) 1908 ] 1909 ] 1910 qed. 1911 1912 axiom set_arg_8_set_program_counter: 1913 ∀n:nat. 1914 ∀l:Vector addressing_mode_tag (S n). 1915 ¬(is_in ? l ACC_PC) → 1916 ∀T: Type[0]. 1917 ∀ps: PreStatus ?. 1918 ∀pc. 1919 ∀val. 1920 ∀b: l. 1921 set_arg_8 ? (set_program_counter T ps pc) b val = 1922 set_program_counter T (set_arg_8 ? ps b val) pc. 1923 [1,2: cases b; *; normalize //] 1924 qed. 1925 1804 1926 1805 1927 lemma get_arg_8_set_code_memory: … … 1927 2049 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) newppc'; 1928 2050 [5: % 1929 1: 2051 1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program 2052 (set_program_counter pseudo_assembly_program ps newppc) 2053 (\fst (ticks_of0 〈preamble,instr_list〉 2054 (program_counter pseudo_assembly_program ps) 2055 (Instruction (INC Identifier (DIRECT ARG)))) 2056 +clock pseudo_assembly_program 2057 (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG)) 2058 [2,3: // ] 2059 <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://] 2060 whd in ⊢ (??%%) 2061 cases (split bool 4 4 ARG) 2062 #nu' #nl' 2063 normalize nodelta 2064 cases (split bool 1 3 nu') 2065 #bit_1' #ignore' 2066 normalize nodelta 2067 cases (get_index_v bool 4 nu' ? ?) 2068 [ normalize nodelta (* HERE *) whd in ⊢ (??%%) % 2069  2070 ]
Note: See TracChangeset
for help on using the changeset viewer.