Ignore:
Timestamp:
Jun 10, 2011, 6:42:41 PM (9 years ago)
Author:
sacerdot
Message:

Long Jmp case finished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r938 r939  
    18031803qed.
    18041804
    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 
    19061805lemma get_arg_8_set_code_memory:
    19071806 ∀T1,T2,s,code_mem,b,arg.
     
    19981897       | (* short *)
    19991898       | (* medium *)
    2000        ] *)
     1899       ]
    20011900  |5: (* Call *)
    20021901  |6: (* Mov *)
     
    20281927        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
    20291928        [5: %
    2030         |1: <set_arg_8_set_code_memory
     1929        |1:
Note: See TracChangeset for help on using the changeset viewer.