Changeset 2247


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

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

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r2209 r2247  
    464464
    465465definition addressing_mode_ok ≝
    466  λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
    467   λaddr:addressing_mode.
    468    match addr with
     466  λT.
     467  λM: internal_pseudo_address_map.
     468  λcm.
     469  λs: PreStatus T cm.
     470  λaddr: addressing_mode.
     471  match addr with
    469472    [ DIRECT d ⇒
    470473        if eq_bv … d (bitvector_of_nat … 224) then
    … …  
    481484        let address ≝ bit_address_of_register … s r in
    482485          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
    483     | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
     486    | ACC_A ⇒
     487      match \snd M with
     488      [ data ⇒ true
     489      | _ ⇒ false
     490      ]
    484491    | ACC_B ⇒ true
    485492    | DPTR ⇒ true
    … …  
    491498    | INDIRECT_DPTR ⇒ true
    492499    | CARRY ⇒ true
    493     | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    494     | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     500    | BIT_ADDR b ⇒
     501      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
     502        if head' bool 0 bit_one then
     503          eq_accumulator_address_map_entry (\snd M) data
     504        else
     505          let address ≝ nat_of_bitvector 7 seven_bits in 
     506          let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in
     507            ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M)
     508    | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *)
    495509    | RELATIVE _ ⇒ true
    496510    | ADDR11 _ ⇒ true
    … …  
    650664      | RET ⇒
    651665        let 〈callM, accM〉 ≝ M in
    652         let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    653         let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     666        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     667        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    654668          if sp_plus_1 ∧ sp_plus_2 then
    655669            Some … M
    … …  
    658672      | RETI ⇒
    659673        let 〈callM, accM〉 ≝ M in
    660         let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    661         let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     674        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     675        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    662676          if sp_plus_1 ∧ sp_plus_2 then
    663677            Some … M
    … …  
    745759            None ?
    746760        ]
    747       | MOV addr1 ⇒ Some … M
     761      | MOV addr1 ⇒
     762        match addr1 with
     763        [ inl l ⇒
     764          match l with
     765          [ inl l' ⇒
     766            match l' with
     767            [ inl l'' ⇒
     768              match l'' with
     769              [ inl l''' ⇒
     770                match l''' with
     771                [ inl l'''' ⇒
     772                  let 〈acc_a, others〉 ≝ l'''' in
     773                  if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then
     774                    Some ? M
     775                  else
     776                    None ?
     777                | inr r ⇒
     778                  let 〈others, others'〉 ≝ r in
     779                  if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then
     780                    Some ? M
     781                  else
     782                    None ?
     783                ]
     784              | inr r ⇒
     785                let 〈direct, others〉 ≝ r in
     786                if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then
     787                  Some ? M
     788                else
     789                  None ?
     790              ]
     791            | inr r ⇒
     792              let 〈dptr, data_16〉 ≝ r in
     793              if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then
     794                Some ? M
     795              else
     796                None ?
     797            ]
     798          | inr r ⇒
     799            let 〈carry, bit_addr〉 ≝ r in
     800            if addressing_mode_ok T M … s carry ∧ addressing_mode_ok T M … s bit_addr then
     801              Some ? M
     802            else
     803              None ?
     804          ]
     805        | inr r ⇒
     806          let 〈bit_addr, carry〉 ≝ r in
     807          if addressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carry then
     808            Some ? M
     809          else
     810            None ?
     811        ]
    748812      ]
    749813    ].

  • 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 *)

  • src/ASM/Status.ma

    r2172 r2247  
    10151015    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
    10161016      [ BIT_ADDR b ⇒ λbit_addr: True.
    1017         let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1017        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    10181018        match head' … bit_1 with
    10191019        [ true ⇒

  • src/ASM/Test.ma

    r2207 r2247  
    11331133  match addr with
    11341134  [ BIT_ADDR b ⇒
    1135     let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1135    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    11361136    match head' … bit_1 with
    11371137    [ true ⇒
    … …  
    11621162  match addr with
    11631163  [ BIT_ADDR b ⇒
    1164     let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1164    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    11651165    match head' … bit_1 with
    11661166    [ true ⇒
    … …  
    12111211    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
    12121212      [ BIT_ADDR b ⇒ λbit_addr: True.
    1213         let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1213        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    12141214        match head' … bit_1 with
    12151215        [ true ⇒
    … …  
    12451245    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
    12461246  |2,3:
    1247     >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    1248     whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    12491247    >p normalize nodelta >p1 normalize nodelta
    12501248    #map_bit_address_assm_1 #map_bit_address_assm_2
Note: See TracChangeset for help on using the changeset viewer.