Changeset 2259 for src/ASM


Ignore:
Timestamp:
Jul 25, 2012, 4:37:34 PM (8 years ago)
Author:
mulligan
Message:

For Claudio

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2258 r2259  
    414414  ]
    415415qed.
     416
     417(*
     418lemma write_at_stack_pointer_status_of_pseudo_status:
     419  ∀M, M'.
     420  ∀cm.
     421  ∀sigma.
     422  ∀policy.
     423  ∀s, s'.
     424  ∀new_b, new_b'.
     425    M = M' →
     426    map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' →
     427    status_of_pseudo_status M cm s sigma policy = s' →
     428    write_at_stack_pointer ?? s' new_b' =
     429    status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.
     430  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
     431  #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl
     432  whd in match write_at_stack_pointer; normalize nodelta
     433  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     434  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
     435  [1:
     436    @eq_f
     437    whd in match get_8051_sfr; normalize nodelta
     438    whd in match sfr_8051_index; normalize nodelta
     439    whd in match status_of_pseudo_status; normalize nodelta
     440    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     441    cases (\snd M) [2: * #address ] normalize nodelta
     442    [1,2:
     443      cases (vsplit bool ???) #high #low normalize nodelta
     444      whd in match sfr_8051_index; normalize nodelta
     445      >get_index_v_set_index_miss %
     446      #absurd destruct(absurd)
     447    |3:
     448      %
     449    ]
     450  |2:
     451    cases (get_index_v bool ????) normalize nodelta
     452    whd in match status_of_pseudo_status; normalize nodelta
     453    whd in match set_low_internal_ram; normalize nodelta
     454    @split_eq_status try %
     455    [1:
     456      @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     457    |2:
     458      @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     459  ]
     460*)
    416461
    417462lemma main_lemma_preinstruction:
    … …  
    622667                s
    623668        | CLR addr ⇒ λinstr_refl.
    624           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     669          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
    625670            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
    626671              let s ≝ add_ticks1 s in
    … …  
    635680            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
    636681        | CPL addr ⇒ λinstr_refl.
    637           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     682          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
    638683            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
    639684                let s ≝ add_ticks1 s in
    … …  
    689734              set_8051_sfr … s SFR_ACC_A new_acc
    690735        | PUSH addr ⇒ λinstr_refl.
    691             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
     736            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with
    692737              [ DIRECT d ⇒ λdirect: True. λEQaddr.
    693738                let s ≝ add_ticks1 s in
    … …  
    906951          @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    907952        ]
    908       |3: %
     953      |3:
     954        %
    909955      |6:
    910956        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
    … …  
    917963      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    918964    ]
    919   |3: (* SUB *)
     965  |3: (* SUBB *)
    920966    (* XXX: work on the right hand side *)
    921967    (* XXX: switch to the left hand side *)
    … …  
    17171763    ]
    17181764  |32: (* CLR *)
    1719     >EQP -P normalize nodelta
     1765    >EQP -P normalize nodelta lapply instr_refl
     1766    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
    17201767    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    17211768    whd in maps_assm:(??%%);
    1722     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1723     [2: normalize nodelta #absurd destruct(absurd) ]
    1724     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1725     whd in ⊢ (??%?);
    1726     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1727     whd in ⊢ (??%?); normalize nodelta
    1728     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1729     normalize nodelta #subaddressing_modein_witness
    1730     @set_arg_8_status_of_pseudo_status try %
    1731     [1:
    1732       @sym_eq @set_clock_status_of_pseudo_status
    1733       >EQs >EQticks <instr_refl %
    1734     |2:
     1769    [1,2:
     1770      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1771      [2,4: normalize nodelta #absurd destruct(absurd) ]
     1772      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    17351773      whd in ⊢ (??%?);
    1736       >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
    1737       [2: <EQaddr % ] %
    1738     ]
    1739   |33: (* CLR *)
    1740     >EQP -P normalize nodelta
     1774      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1775      [1:
     1776        >EQs >EQticks <instr_refl
     1777        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
     1778        @set_arg_1_status_of_pseudo_status try %
     1779        [1:
     1780          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
     1781        |2:
     1782          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
     1783        ]         
     1784      |2:
     1785        >EQs >EQticks <instr_refl
     1786        change with (set_arg_8 ??? ACC_A ? = ?) try %
     1787        @set_arg_8_status_of_pseudo_status try %
     1788        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
     1789      ]
     1790    |3:
     1791      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1792      whd in ⊢ (??%?);
     1793      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1794      >EQs >EQticks <instr_refl
     1795      change with (set_arg_1 ??? CARRY ? = ?) try %
     1796      @set_arg_1_status_of_pseudo_status %
     1797    ]
     1798  |33: (* CPL *)
     1799    >EQP -P normalize nodelta lapply instr_refl
     1800    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
    17411801    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    17421802    whd in maps_assm:(??%%);
    1743     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1744     [2: normalize nodelta #absurd destruct(absurd) ]
    1745     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1746     whd in ⊢ (??%?);
    1747     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1748     whd in ⊢ (??%?); normalize nodelta
    1749     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1750     normalize nodelta #subaddressing_modein_witness
    1751     @set_arg_1_status_of_pseudo_status try %
    1752     @sym_eq @set_clock_status_of_pseudo_status
    1753     >EQs >EQticks <instr_refl %
    1754   |34: (* CLR *)
    1755     >EQP -P normalize nodelta
    1756     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1757     whd in maps_assm:(??%%);
    1758     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1759     [2: normalize nodelta #absurd destruct(absurd) ]
    1760     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1761     whd in ⊢ (??%?);
    1762     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1763     whd in ⊢ (??%?); normalize nodelta
    1764     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1765     normalize nodelta #subaddressing_modein_witness
    1766     @set_arg_1_status_of_pseudo_status try %
    1767     [1:
    1768       @sym_eq @set_clock_status_of_pseudo_status
    1769       >EQs >EQticks <instr_refl %
    1770     |*:
    1771       cases daemon (* XXX: requires changes to addressing_mode_ok *)
    1772     ]
    1773   |35: (* CPL *)
    1774     >EQP -P normalize nodelta
    1775     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1776     whd in maps_assm:(??%%);
    1777     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1778     [2: normalize nodelta #absurd destruct(absurd) ]
    1779     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1780     whd in ⊢ (??%?);
    1781     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1782     whd in ⊢ (??%?); normalize nodelta
    1783     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1784     normalize nodelta #subaddressing_modein_witness
    1785     @set_8051_sfr_status_of_pseudo_status
    1786     [1:
    1787       @sym_eq @set_clock_status_of_pseudo_status
    1788       >EQs >EQticks <instr_refl %
    1789     |2:
    1790       whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
    1791       [2: <EQaddr % ] normalize nodelta @eq_f
    1792       @(pose … (set_clock ????)) #status #status_refl
    1793       @sym_eq @(get_8051_sfr_status_of_pseudo_status M' … status) >status_refl
    1794       >EQs >EQticks <instr_refl try %
    1795       whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addr addressing_mode_ok_assm_1)
    1796       [2: <EQaddr % ] %
    1797     ]
    1798   |36: (* CPL *)
    1799     >EQP -P normalize nodelta
    1800     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1801     whd in maps_assm:(??%%);
    1802     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1803     [2: normalize nodelta #absurd destruct(absurd) ]
    1804     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1805     whd in ⊢ (??%?);
    1806     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1807     whd in ⊢ (??%?); normalize nodelta
    1808     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1809     normalize nodelta #subaddressing_modein_witness
    1810     @set_arg_1_status_of_pseudo_status try %
    1811     [1:
    1812       @eq_f @(get_arg_1_status_of_pseudo_status … M') try %
    1813       @sym_eq @set_clock_status_of_pseudo_status
    1814       >EQs >EQticks <instr_refl <EQaddr %
    1815     |2:
    1816       @sym_eq @set_clock_status_of_pseudo_status
    1817       >EQs >EQticks <instr_refl <EQaddr %
    1818     ]
    1819   |37: (* CPL *)
    1820     >EQP -P normalize nodelta
    1821     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1822     whd in maps_assm:(??%%);
    1823     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1824     [2: normalize nodelta #absurd destruct(absurd) ]
    1825     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1826     whd in ⊢ (??%?);
    1827     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1828     whd in ⊢ (??%?); normalize nodelta
    1829     generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    1830     normalize nodelta #subaddressing_modein_witness
    1831     @set_arg_1_status_of_pseudo_status
    1832     [1:
     1803    [1,2:
     1804      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1805      [2,4: normalize nodelta #absurd destruct(absurd) ]
     1806      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1807      whd in ⊢ (??%?);
     1808      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1809      [1:
     1810        >EQs >EQticks <instr_refl
     1811        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
     1812        @set_arg_1_status_of_pseudo_status
     1813        [1:
     1814          @eq_f
     1815          @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1816          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1817          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
     1818        |2:
     1819          %
     1820        |3:
     1821          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) %
     1822        |4:
     1823          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) %
     1824        ]       
     1825      |2:
     1826        >EQs >EQticks <instr_refl
     1827        change with (set_8051_sfr ????? = ?)
     1828        @set_8051_sfr_status_of_pseudo_status try %
     1829        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
     1830        normalize nodelta @eq_f
     1831        @(pose … (set_clock ????)) #status #status_refl
     1832        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1833        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
     1834      ]
     1835    |3:
     1836      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1837      whd in ⊢ (??%?);
     1838      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1839      >EQs >EQticks <instr_refl
     1840      change with (set_arg_1 ??? CARRY ? = ?) try %
     1841      @set_arg_1_status_of_pseudo_status try %
    18331842      @eq_f
    1834       @(pose … (set_clock ????)) #status #status_refl
    1835       @(get_arg_1_status_of_pseudo_status … M' … status) try % >status_refl
    1836       >EQs >EQticks <instr_refl <EQaddr
    1837       [1:
    1838         @sym_eq @set_clock_status_of_pseudo_status %
    1839       |2:
    1840         cases daemon (* XXX: require changes to addressing_mode_ok *)
    1841       ]
    1842     |2:
    1843       @sym_eq @set_clock_status_of_pseudo_status
    1844       >EQs >EQticks <instr_refl <EQaddr %
    1845     |*:
    1846       cases daemon (* XXX: require changes to addressing_mode_ok *)
    1847     ]
    1848   |38,40: (* RL and RR *)
     1843      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1844      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
     1845    ]
     1846  |34,36: (* RL and RR *)
    18491847    (* XXX: work on the right hand side *)
    18501848    (* XXX: switch to the left hand side *)
    … …  
    18691867    ]
    18701868    @sym_eq @set_program_counter_status_of_pseudo_status %
    1871   |39,41: (* RLC and RRC *)
     1869  |35,37: (* RLC and RRC *)
    18721870    (* XXX: work on the right hand side *)
    18731871    (* XXX: switch to the left hand side *)
    … …  
    18971895      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
    18981896    ]
    1899   |42: (* SWAP *)
     1897  |38: (* SWAP *)
    19001898    >EQP -P normalize nodelta
    19011899    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    19351933      ]     
    19361934    ]
    1937   |43: (* MOV *)
     1935  |39: (* MOV *)
    19381936    >EQP -P normalize nodelta
    19391937    inversion addr
    … …  
    20622060                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20632061                |2:
    2064                   @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) %
     2062                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     2063                  [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    20652064                ]
    20662065              ]
    … …  
    21282127      |2:
    21292128        >EQs >EQticks <instr_refl >addr_refl %
    2130       |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *)
     2129      |3,4:
    21312130        @(pose … (set_clock ????)) #status #status_refl
    21322131        [1:
    … …  
    21402139      ]
    21412140    ]
    2142   |44: (* MOVX *)
     2141  |40: (* MOVX *)
    21432142    >EQP -P normalize nodelta
    21442143    inversion addr
    … …  
    22132212      ]
    22142213    ]
    2215   |*)45: (* SETB *)
     2214  |41: (* SETB *)
    22162215    >EQs >EQticks <instr_refl
    22172216    >EQP -P normalize nodelta
    … …  
    22302229      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    22312230    ]
    2232   |46: (* PUSH *)
     2231  |*)42: (* PUSH *)
     2232    >EQP -P normalize nodelta lapply instr_refl
     2233    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
     2234    #sigma_increment_commutation
     2235    whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
     2236    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
     2237    whd in ⊢ (??%?);
     2238    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2239    whd in ⊢ (??%?);
     2240    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
     2241    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
     2242    [1:
     2243      @eq_f2 try %
     2244      @(pose … (set_clock ????)) #status #status_refl
     2245      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
     2246      @sym_eq @set_clock_status_of_pseudo_status
     2247      >EQs >EQticks <instr_refl %
     2248    |2:
     2249      >EQs >EQticks <instr_refl
     2250      XXX
     2251    ]
     2252  |46: (* RET *)
    22332253    >EQP -P normalize nodelta
    2234     #sigma_increment_commutation whd in ⊢ (??%% → ?);
    2235     inversion M #callM #accM #callM_accM_refl normalize nodelta
    2236     @(subaddressing_mode_elim … addr) #w normalize nodelta
    2237     @Some_Some_elim #Mrefl destruct(Mrefl)
    2238     cases daemon (* XXX *)
     2254    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2255    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
     2256    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
     2257    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
     2258    [2: normalize nodelta #absurd destruct(absurd) ]
     2259    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
     2260    [2: normalize nodelta #absurd destruct(absurd) ]
     2261    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
     2262    whd in ⊢ (??%?);
     2263    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2264    whd in ⊢ (??%?);
     2265    @(pair_replace ?????????? p) normalize nodelta
     2266    >EQs >EQticks <instr_refl
     2267    [1:
     2268      @eq_f3 try %
     2269      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     2270      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
     2271    |2:
     2272      @(pair_replace ?????????? p1) normalize nodelta
     2273      >EQs >EQticks <instr_refl
     2274      [1:
     2275        @eq_f3 try %
     2276        @sym_eq @(pose … (set_clock ????)) #status #status_refl
     2277        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
     2278        [1:
     2279          cases daemon
     2280          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2281        |2:
     2282          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     2283          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     2284          whd in match sfr_8051_index; normalize nodelta
     2285          >get_index_v_set_index_hit
     2286          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
     2287          cases daemon
     2288          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2289        ]
     2290      |2:
     2291        cases daemon (* XXX *)
     2292      ]
     2293    ]
    22392294  |47: (* POP *)
    22402295  |48: (* XCH *)
    … …  
    23632418    ]
    23642419  |50: (* RET *)
    2365     >EQP -P normalize nodelta
    2366     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    2367     whd in maps_assm:(??%%); normalize nodelta in maps_assm;
    2368     lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
    2369     inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
    2370     [2: normalize nodelta #absurd destruct(absurd) ]
    2371     inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
    2372     [2: normalize nodelta #absurd destruct(absurd) ]
    2373     normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
    2374     whd in ⊢ (??%?);
    2375     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    2376     whd in ⊢ (??%?);
    2377     @(pair_replace ?????????? p) normalize nodelta
    2378     >EQs >EQticks <instr_refl
    2379     [1:
    2380       @eq_f3 try %
    2381       @sym_eq @(pose … (set_clock ????)) #status #status_refl
    2382       @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
    2383     |2:
    2384       @(pair_replace ?????????? p1) normalize nodelta
    2385       >EQs >EQticks <instr_refl
    2386       [1:
    2387         @eq_f3 try %
    2388         @sym_eq @(pose … (set_clock ????)) #status #status_refl
    2389         @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
    2390         [1:
    2391           cases daemon
    2392           (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
    2393         |2:
    2394           whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    2395           whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
    2396           whd in match sfr_8051_index; normalize nodelta
    2397           >get_index_v_set_index_hit
    2398           change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
    2399           cases daemon
    2400           (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
    2401         ]
    2402       |2:
    2403         cases daemon (* XXX *)
    2404       ]
    2405     ]
    24062420  |51: (* RETI *)
    24072421  |52: (* NOP *)
Note: See TracChangeset for help on using the changeset viewer.