Changeset 937
 Timestamp:
 Jun 10, 2011, 4:48:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r936 r937 1803 1803 qed. 1804 1804 1805 lemma set_bit_addressable_sfr_set_code_memory: 1806 ∀T: Type[0]. 1807 ∀ps: PreStatus T. 1808 ∀code_mem. 1809 ∀x. 1810 ∀val. 1811 set_bit_addressable_sfr T (set_code_memory T T ps code_mem) x val = 1812 set_code_memory T T (set_bit_addressable_sfr T ps x val) code_mem. 1813 #T #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 ∀ps: PreStatus T. 1878 ∀code_mem. 1879 ∀val. 1880 ∀b: l. 1881 set_arg_8 T (set_code_memory … ps code_mem) b val = 1882 set_code_memory … (set_arg_8 T ps b val) code_mem. 1883 [2,3: cases b; *; normalize //] 1884 #n #l #prf #T #ps #code_mem #val * *; 1885 [*: [1,2,3,4,8,9,15,16,17,18,19: #x] 1886 try #y whd in ⊢ (??(%)?) 1887 whd in ⊢ (???(???(%)?)) 1888 [1,2: 1889 cases (split bool 4 4 ?) 1890 #nu' #nl' 1891 normalize nodelta 1892 cases (split bool 1 3 nu') 1893 #bit1' #ignore' 1894 normalize nodelta 1895 cases (get_index_v bool 4 nu' 1 ?) 1896 [*:try (normalize nodelta %) 1897 try % 1898 try (@(set_bit_addressable_sfr_set_code_memory T ps code_mem x val)) 1899 ] 1900 3,4: % 1901 *: normalize cases (not_implemented) 1902 ] 1903 ] 1904 qed. 1905 1805 1906 lemma get_arg_8_set_code_memory: 1806 1907 ∀T1,T2,s,code_mem,b,arg. … … 1913 2014 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) newppc'; 1914 2015 [5: % 1915 1: 2016 1: <set_arg_8_set_code_memory
Note: See TracChangeset
for help on using the changeset viewer.