 Timestamp:
 Jun 10, 2011, 6:42:41 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r938 r939 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 #val1814 whd in ⊢ (??%?)1815 whd in ⊢ (???(???%?))1816 cases (eqb ? 128) [ normalize nodelta cases not_implemented1817  normalize nodelta1818 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented1819  normalize nodelta1820 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented1821  normalize nodelta1822 cases (eqb ? 176) [ normalize nodelta %1823  normalize nodelta1824 cases (eqb ? 153) [ normalize nodelta %1825  normalize nodelta1826 cases (eqb ? 138) [ normalize nodelta %1827  normalize nodelta1828 cases (eqb ? 139) [ normalize nodelta %1829  normalize nodelta1830 cases (eqb ? 140) [ normalize nodelta %1831  normalize nodelta1832 cases (eqb ? 141) [ normalize nodelta %1833  normalize nodelta1834 cases (eqb ? 200) [ normalize nodelta %1835  normalize nodelta1836 cases (eqb ? 202) [ normalize nodelta %1837  normalize nodelta1838 cases (eqb ? 203) [ normalize nodelta %1839  normalize nodelta1840 cases (eqb ? 204) [ normalize nodelta %1841  normalize nodelta1842 cases (eqb ? 205) [ normalize nodelta %1843  normalize nodelta1844 cases (eqb ? 135) [ normalize nodelta %1845  normalize nodelta1846 cases (eqb ? 136) [ normalize nodelta %1847  normalize nodelta1848 cases (eqb ? 137) [ normalize nodelta %1849  normalize nodelta1850 cases (eqb ? 152) [ normalize nodelta %1851  normalize nodelta1852 cases (eqb ? 168) [ normalize nodelta %1853  normalize nodelta1854 cases (eqb ? 184) [ normalize nodelta %1855  normalize nodelta1856 cases (eqb ? 129) [ normalize nodelta %1857  normalize nodelta1858 cases (eqb ? 130) [ normalize nodelta %1859  normalize nodelta1860 cases (eqb ? 131) [ normalize nodelta %1861  normalize nodelta1862 cases (eqb ? 208) [ normalize nodelta %1863  normalize nodelta1864 cases (eqb ? 224) [ normalize nodelta %1865  normalize nodelta1866 cases (eqb ? 240) [ normalize nodelta %1867  normalize nodelta1868 cases not_implemented1869 ]]]]]]]]]]]]]]]]]]]]]]]]]]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 nodelta1892 cases (split bool 1 3 nu')1893 #bit1' #ignore'1894 normalize nodelta1895 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 1906 1805 lemma get_arg_8_set_code_memory: 1907 1806 ∀T1,T2,s,code_mem,b,arg. … … 1998 1897  (* short *) 1999 1898  (* medium *) 2000 ] *)1899 ] 2001 1900 5: (* Call *) 2002 1901 6: (* Mov *) … … 2028 1927 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) newppc'; 2029 1928 [5: % 2030 1: <set_arg_8_set_code_memory1929 1:
Note: See TracChangeset
for help on using the changeset viewer.