Ignore:
Timestamp:
Jul 24, 2012, 6:00:48 PM (8 years ago)
Author:
mulligan
Message:

Work on the MOV instruction from today and bug fixes in set_arg_1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2216 r2247  
    280280qed.
    281281
     282lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
     283  ∀M: internal_pseudo_address_map.
     284  ∀cm: pseudo_assembly_program.
     285  ∀s: PreStatus pseudo_assembly_program cm.
     286  ∀sigma: Word → Word.
     287  ∀addr: [[bit_addr]]. (* XXX: expand as needed *)
     288  ∀f: bool.
     289  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
     290    map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
     291  #M #cm #s #sigma #addr #f
     292  @(subaddressing_mode_elim … addr) #w
     293  whd in ⊢ (??%? → %);
     294  @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     295  cases (head' bool ??) normalize nodelta
     296  [1:
     297    #eq_accumulator_assm whd in ⊢ (??%?);
     298    cases (sfr_of_Byte ?) try %
     299    * * normalize nodelta try %
     300    whd in ⊢ (??%?);
     301    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
     302  |2:
     303    #assoc_list_exists_assm whd in ⊢ (??%?);
     304    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) (not_b_c_to_b_not_c … assoc_list_exists_assm)) %
     305  ]
     306qed.
     307
     308lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
     309  ∀M: internal_pseudo_address_map.
     310  ∀cm: pseudo_assembly_program.
     311  ∀s, s': PreStatus pseudo_assembly_program cm.
     312  ∀sigma: Word → Word.
     313  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
     314  ∀f: bool.
     315  s = s' →
     316  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
     317    map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
     318  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
     319  @(subaddressing_mode_elim … addr) [1: #w ]
     320  whd in ⊢ (??%? → %); [2: #_ @I ]
     321  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     322  cases (head' bool ??) normalize nodelta
     323  [1:
     324    #eq_accumulator_assm whd in ⊢ (??%?);
     325    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
     326    whd in ⊢ (??%?);
     327    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
     328  |2:
     329    #assoc_list_exists_assm whd in ⊢ (??%?);
     330    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
     331    whd in assoc_list_exists_assm:(???%);
     332    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
     333  ]
     334qed.
     335
     336lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
     337  ∀M: internal_pseudo_address_map.
     338  ∀cm: pseudo_assembly_program.
     339  ∀s, s': PreStatus pseudo_assembly_program cm.
     340  ∀sigma: Word → Word.
     341  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
     342  ∀f: bool.
     343  s = s' →
     344  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
     345    map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
     346  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
     347  @(subaddressing_mode_elim … addr) [1: #w ]
     348  whd in ⊢ (??%? → %); [2: #_ @I ]
     349  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     350  cases (head' bool ??) normalize nodelta
     351  [1:
     352    #eq_accumulator_assm whd in ⊢ (??%?);
     353    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
     354    whd in ⊢ (??%?);
     355    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
     356  |2:
     357    #assoc_list_exists_assm whd in ⊢ (??%?);
     358    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
     359    whd in assoc_list_exists_assm:(???%);
     360    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
     361  ]
     362qed.
     363 
    282364lemma match_nat_replace:
    283365  ∀l, o, p, r, o', p': nat.
     
    600682            let s ≝ set_arg_1 … s CARRY new_cy_flag in
    601683              set_8051_sfr … s SFR_ACC_A new_acc
    602         | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     684        | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *)
    603685            let s ≝ add_ticks1 s in
    604686            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     
    18151897      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
    18161898    ]
    1817   |*)42: (* SWAP *)
    1818   |43: (* MOV *)
     1899  |42: (* SWAP *)
     1900    >EQP -P normalize nodelta
     1901    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1902    whd in maps_assm:(??%%);
     1903    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1904    [2: normalize nodelta #absurd destruct(absurd) ]
     1905    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1906    whd in ⊢ (??%?);
     1907    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1908    whd in ⊢ (??%?);
     1909    @(pair_replace ?????????? p)
     1910    [1:
     1911      @eq_f normalize nodelta
     1912      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     1913      @(get_8051_sfr_status_of_pseudo_status … M' … status)
     1914      [1:
     1915        >status_refl -status_refl
     1916        @sym_eq @set_clock_status_of_pseudo_status
     1917        >EQs >EQticks <instr_refl %
     1918      |2:
     1919        whd in ⊢ (??%?);
     1920        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1921      ]
     1922    |2:
     1923      @(pair_replace ?????????? p) normalize nodelta
     1924      [1:
     1925        %
     1926      |2:
     1927        @set_8051_sfr_status_of_pseudo_status
     1928        [1:
     1929          @sym_eq @set_clock_status_of_pseudo_status
     1930          >EQs >EQticks <instr_refl %
     1931        |2:
     1932          whd in ⊢ (??%?);
     1933          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1934        ]
     1935      ]     
     1936    ]
     1937  |*)43: (* MOV *)
     1938    >EQP -P normalize nodelta
     1939    inversion addr
     1940    [1:
     1941      #addr' normalize nodelta
     1942      inversion addr'
     1943      [1:
     1944        #addr'' normalize nodelta
     1945        inversion addr''
     1946        [1:
     1947          #addr''' normalize nodelta
     1948          inversion addr'''
     1949          [1:
     1950            #addr'''' normalize nodelta
     1951            inversion addr''''
     1952            [1:
     1953              normalize nodelta #acc_a_others
     1954              cases acc_a_others #acc_a #others
     1955              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
     1956              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1957              whd in maps_assm:(??%%);
     1958              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1959              [2: normalize nodelta #absurd destruct(absurd) ]
     1960              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1961              [2: normalize nodelta #absurd destruct(absurd) ]
     1962              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1963              whd in ⊢ (??%?);
     1964              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1965              change with (set_arg_8 ????? = ?)
     1966              @set_arg_8_status_of_pseudo_status try %
     1967              [1:
     1968                @sym_eq @set_clock_status_of_pseudo_status
     1969                >EQs >EQticks <instr_refl >addr_refl %
     1970              |2:
     1971                @(subaddressing_mode_elim … acc_a) @I
     1972              |3:
     1973                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     1974                [1: @(subaddressing_mode_elim … acc_a) % ]
     1975                >EQs >EQticks <instr_refl >addr_refl
     1976                [1,2:
     1977                  %
     1978                |3:
     1979                  @(pose … (set_clock ????)) #status #status_refl
     1980                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1981                  [1:
     1982                    @sym_eq @set_clock_status_of_pseudo_status %
     1983                  |2:
     1984                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     1985                    [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1986                  |3:
     1987                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     1988                    [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1989                  ]
     1990                ]
     1991              ]
     1992            |2:
     1993              #others_others' cases others_others' #others #others' normalize nodelta
     1994              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
     1995              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1996              whd in maps_assm:(??%%);
     1997              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1998              [2: normalize nodelta #absurd destruct(absurd) ]
     1999              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2000              [2: normalize nodelta #absurd destruct(absurd) ]
     2001              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2002              whd in ⊢ (??%?);
     2003              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2004              change with (set_arg_8 ????? = ?)
     2005              @set_arg_8_status_of_pseudo_status try %
     2006              >EQs >EQticks <instr_refl >addr_refl try %
     2007              [1:
     2008                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
     2009                [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2010              |2:
     2011                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
     2012                [1:
     2013                  /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2014                |2,3:
     2015                  %
     2016                |4:
     2017                  @(pose … (set_clock ????)) #status #status_refl
     2018                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     2019                  [1:
     2020                    @sym_eq @set_clock_status_of_pseudo_status %
     2021                  |2:
     2022                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
     2023                    [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2024                  |3:
     2025                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
     2026                    [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2027                  ]
     2028                ]
     2029              ]
     2030            ]
     2031          |2:
     2032            #direct_others cases direct_others #direct #others
     2033            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
     2034            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2035            whd in maps_assm:(??%%);
     2036            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2037            [2: normalize nodelta #absurd destruct(absurd) ]
     2038            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2039            [2: normalize nodelta #absurd destruct(absurd) ]
     2040            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2041            whd in ⊢ (??%?);
     2042            <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2043            change with (set_arg_8 ????? = ?)
     2044            @set_arg_8_status_of_pseudo_status try %
     2045            >EQs >EQticks <instr_refl >addr_refl
     2046            [1:
     2047              @sym_eq @set_clock_status_of_pseudo_status %
     2048            |2:
     2049              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     2050              [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2051            |3:
     2052              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     2053              [1:
     2054                /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2055              |2,3:
     2056                %
     2057              |4:
     2058                @(pose … (set_clock ????)) #status #status_refl
     2059                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     2060                [1:
     2061                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     2062                  [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2063                |2:
     2064                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) %
     2065                ]
     2066              ]
     2067            ]
     2068          ]
     2069        |2:
     2070          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
     2071          #addr_refl'' #addr_refl' #addr_refl
     2072          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2073          whd in maps_assm:(??%%);
     2074          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2075          [2: normalize nodelta #absurd destruct(absurd) ]
     2076          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2077          [2: normalize nodelta #absurd destruct(absurd) ]
     2078          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2079          whd in ⊢ (??%?);
     2080          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2081          change with (set_arg_16 ????? = ?)
     2082          @set_arg_16_status_of_pseudo_status
     2083          >EQs >EQticks <instr_refl >addr_refl
     2084          @sym_eq @set_clock_status_of_pseudo_status %
     2085        ]
     2086      |2:
     2087        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
     2088        #addr_refl' #addr_refl
     2089        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2090        whd in maps_assm:(??%%);
     2091        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2092        [2: normalize nodelta #absurd destruct(absurd) ]
     2093        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2094        [2: normalize nodelta #absurd destruct(absurd) ]
     2095        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2096        whd in ⊢ (??%?);
     2097        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2098        change with (set_arg_1 ????? = ?)
     2099        @set_arg_1_status_of_pseudo_status
     2100        >EQs >EQticks <instr_refl >addr_refl try %
     2101        [1:
     2102          @sym_eq @(pose … (set_clock ????)) #status #status_refl
     2103          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     2104          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
     2105        |2,3:
     2106          @(subaddressing_mode_elim … carry) @I
     2107        ]
     2108      ]
     2109    |2:
     2110      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
     2111      #addr_refl
     2112      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2113      whd in maps_assm:(??%%);
     2114      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2115      [2: normalize nodelta #absurd destruct(absurd) ]
     2116      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2117      [2: normalize nodelta #absurd destruct(absurd) ]
     2118      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     2119      whd in ⊢ (??%?);
     2120      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2121      change with (set_arg_1 ????? = ?)
     2122      @set_arg_1_status_of_pseudo_status
     2123      >EQs >EQticks <instr_refl >addr_refl try %
     2124      [1:
     2125        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     2126        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     2127        @(subaddressing_mode_elim … carry) @I
     2128      |2:
     2129        @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps)
     2130        [1:
     2131          normalize nodelta
     2132        |2:
     2133          assumption
     2134        ]
     2135      ]
     2136    ]
    18192137  |44: (* MOVX *)
    18202138  |45: (* SETB *)
Note: See TracChangeset for help on using the changeset viewer.