Changeset 940


Ignore:
Timestamp:
Jun 10, 2011, 6:49:00 PM (8 years ago)
Author:
mulligan
Message:

more changes to inc case of main theorem

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r939 r940  
    18021802 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
    18031803qed.
     1804
     1805lemma 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  ]]]]]]]]]]]]]]]]]]]]]]]]]]
     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    ∀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 ]
     1910qed.
     1911
     1912axiom 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 //]
     1924qed.
     1925 
    18041926
    18051927lemma get_arg_8_set_code_memory:
     
    19272049        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
    19282050        [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.