Changeset 937


Ignore:
Timestamp:
Jun 10, 2011, 4:48:45 PM (8 years ago)
Author:
mulligan
Message:

resolved conflict in assembly_proof, more lemmas added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r936 r937  
    18031803qed.
    18041804
     1805lemma 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  ]]]]]]]]]]]]]]]]]]]]]]]]]]
     1870qed.
     1871
     1872lemma 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 ]
     1904qed.
     1905
    18051906lemma get_arg_8_set_code_memory:
    18061907 ∀T1,T2,s,code_mem,b,arg.
     
    19132014        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
    19142015        [5: %
    1915         |1:
     2016        |1: <set_arg_8_set_code_memory
Note: See TracChangeset for help on using the changeset viewer.