Changeset 2216 for src


Ignore:
Timestamp:
Jul 19, 2012, 5:33:54 PM (8 years ago)
Author:
mulligan
Message:

More work on the big lemma. Nearly there now.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2212 r2216  
    295295qed.
    296296
    297 (*
    298297lemma match_nat_status_of_pseudo_status:
    299298  ∀M, cm, sigma, policy, s, s', s'', s'''.
    … …  
    301300    n = n' →
    302301    status_of_pseudo_status M cm s' sigma policy = s →
    303     status_of_pseudo_status M cm s''' sigma policy = s'' →
    304       match n with [ O ⇒ s | S n' ⇒ s'' ] =
    305         status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''']) sigma policy.
     302    (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) →
     303      match n with [ O ⇒ s | S n' ⇒ s'' n' ] =
     304        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy.
    306305  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
    307   #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'
    308   cases n normalize nodelta try % #n' %
     306  #n_refl #s_refl #s_refl' <n_refl <s_refl
     307  cases n normalize nodelta try % #n' <(s_refl' n') %
    309308qed.
    310 *)
     309
     310lemma get_index_v_set_index_hit:
     311  ∀A: Type[0].
     312  ∀n: nat.
     313  ∀v: Vector A n.
     314  ∀i: nat.
     315  ∀e: A.
     316  ∀i_lt_n_proof: i < n.
     317  ∀i_lt_n_proof': i < n.
     318    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
     319  #A #n #v elim v
     320  [1:
     321    #i #e #i_lt_n_proof
     322    cases (lt_to_not_zero … i_lt_n_proof)
     323  |2:
     324    #n' #hd #tl #inductive_hypothesis #i #e
     325    cases i
     326    [1:
     327      #i_lt_n_proof #i_lt_n_proof' %
     328    |2:
     329      #i' #i_lt_n_proof' #i_lt_n_proof''
     330      whd in ⊢ (??%?); @inductive_hypothesis
     331    ]
     332  ]
     333qed.
    311334
    312335lemma main_lemma_preinstruction:
    … …  
    767790  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    768791  whd in match execute_1_preinstruction; normalize nodelta
    769   [(* 35: (* XRL *)
    770     inversion addr
    771     [1:
    772       #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
    773       >EQP -P normalize nodelta
    774       #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    775       whd in maps_assm:(??%%);
    776       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    777       [2: normalize nodelta #absurd destruct(absurd) ]
    778       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    779       [2: normalize nodelta #absurd destruct(absurd) ]
    780       normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    781       whd in ⊢ (??%?);
    782       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    783       change with (set_arg_8 ????? = ?)
    784       @set_arg_8_status_of_pseudo_status try %
    785       >EQs >EQticks <instr_refl >addr_refl
    786       [1:
    787         @sym_eq @set_clock_status_of_pseudo_status
    788         [1:
    789           @sym_eq @set_program_counter_status_of_pseudo_status %
    790         |2:
    791           @eq_f2 %
    792         ]
    793       |2:
    794         @(subaddressing_mode_elim … acc_a) @I
    795       |3:
    796         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    797         [1:
    798           @(subaddressing_mode_elim … acc_a) %
    799         |4:
    800           @eq_f2
    801           @(pose … (set_clock ????)) #status #status_refl
    802           @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    803           [1:
    804             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    805             [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
    806           |3:
    807             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    808             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    809           |2:
    810             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    811             [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
    812           |4:
    813             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    814             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    815           ]
    816         |*:
    817           %
    818         ]
    819       ]
    820     |2:
    821       #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
    822       >EQP -P normalize nodelta
    823       #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    824       whd in maps_assm:(??%%);
    825       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    826       [2: normalize nodelta #absurd destruct(absurd) ]
    827       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    828       [2: normalize nodelta #absurd destruct(absurd) ]
    829       normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    830       whd in ⊢ (??%?);
    831       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    832       change with (set_arg_8 ????? = ?)
    833       @set_arg_8_status_of_pseudo_status try %
    834       >EQs >EQticks <instr_refl >addr_refl
    835       [1:
    836         @sym_eq @set_clock_status_of_pseudo_status
    837         [1:
    838           @sym_eq @set_program_counter_status_of_pseudo_status %
    839         |2:
    840           @eq_f2 %
    841         ]
    842       |2:
    843         @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    844         [1: @(subaddressing_mode_elim … direct) #w % ] %
    845       |3:
    846         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    847         [1:
    848           @(subaddressing_mode_elim … direct) #w %
    849         |4:
    850           @eq_f2
    851           @(pose … (set_clock ????)) #status #status_refl
    852           @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    853           [1:
    854             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    855             [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
    856           |3:
    857             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    858             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    859           |2:
    860             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    861             [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
    862           |4:
    863             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    864             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    865           ]
    866         |*:
    867           %
    868         ]
    869       ]
    870     ]
    871   |33,34: (* ANL and ORL *)
    872     inversion addr
    873     [1,3:
    874       *
    875       [1,3:
    876         #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
    877         >EQP -P normalize nodelta
    878         #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    879         whd in maps_assm:(??%%);
    880         inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    881         [2,4: normalize nodelta #absurd destruct(absurd) ]
    882         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    883         [2,4: normalize nodelta #absurd destruct(absurd) ]
    884         normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    885         whd in ⊢ (??%?);
    886         <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    887         change with (set_arg_8 ????? = ?)
    888         @set_arg_8_status_of_pseudo_status try %
    889         >EQs >EQticks <instr_refl >addr_refl
    890         [1,4:
    891           @sym_eq @set_clock_status_of_pseudo_status
    892           [1,3:
    893             @sym_eq @set_program_counter_status_of_pseudo_status %
    894           |2,4:
    895             @eq_f2 %
    896           ]
    897         |2,5:
    898           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    899           [1,3: @(subaddressing_mode_elim … acc_a) % ] %
    900         |3,6:
    901           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    902           [1,5:
    903             @(subaddressing_mode_elim … acc_a) %
    904           |4,8:
    905             @eq_f2
    906             @(pose … (set_clock ????)) #status #status_refl
    907             @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    908             [1,5:
    909               @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    910               [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
    911             |3,7:
    912               @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    913               [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    914             |2,6:
    915               @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    916               [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
    917             |4,8:
    918               @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    919               [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    920             ]
    921           |*:
    922             %
    923           ]
    924         ]
    925       |2,4:
    926         #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
    927         >EQP -P normalize nodelta
    928         #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    929         whd in maps_assm:(??%%);
    930         inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    931         [2,4: normalize nodelta #absurd destruct(absurd) ]
    932         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    933         [2,4: normalize nodelta #absurd destruct(absurd) ]
    934         normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    935         whd in ⊢ (??%?);
    936         <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    937         change with (set_arg_8 ????? = ?)
    938         @set_arg_8_status_of_pseudo_status try %
    939         >EQs >EQticks <instr_refl >addr_refl
    940         [1,4:
    941           @sym_eq @set_clock_status_of_pseudo_status
    942           [1,3:
    943             @sym_eq @set_program_counter_status_of_pseudo_status %
    944           |2,4:
    945             @eq_f2 %
    946           ]
    947         |2,5:
    948           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    949           [1,3: @(subaddressing_mode_elim … direct) #w % ] %
    950         |3,6:
    951           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    952           [1,5:
    953             @(subaddressing_mode_elim … direct) #w %
    954           |4,8:
    955             @eq_f2
    956             @(pose … (set_clock ????)) #status #status_refl
    957             @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    958             [1,5:
    959               @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    960               [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
    961             |3,7:
    962               @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    963               [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    964             |2,6:
    965               @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    966               [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
    967             |4,8:
    968               @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    969               [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    970             ]
    971           |*:
    972             %
    973           ]
    974         ]
    975       ]
    976     |2,4:
    977       #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
    978       >EQP -P normalize nodelta
    979       #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    980       whd in maps_assm:(??%%);
    981       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    982       [2,4: normalize nodelta #absurd destruct(absurd) ]
    983       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    984       [2,4: normalize nodelta #absurd destruct(absurd) ]
    985       normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    986       whd in ⊢ (??%?);
    987       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    988       change with (set_flags ?????? = ?)
    989       [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
    990       >EQs >EQticks <instr_refl >addr_refl
    991       @sym_eq @set_clock_status_of_pseudo_status %
    992     ]
    993   |*)4: (* INC *)
    994     (* XXX: work on the right hand side *)
    995     (* XXX: switch to the left hand side *)
    996     >EQs >EQticks <instr_refl >EQP -P normalize nodelta
    997     @(subaddressing_mode_elim … addr) normalize nodelta
    998     [1:
    999       #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1000       whd in maps_assm:(??%%);
    1001       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1002       [2: normalize nodelta #absurd destruct(absurd) ]
    1003       normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1004       whd in ⊢ (??%?);
    1005       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1006       whd in ⊢ (??%?);
    1007       inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
    1008       @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
    1009       [1:
    1010         @eq_f2 try %
    1011         @(pose … (set_clock ????)) #status #status_refl
    1012         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    1013         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
    1014       |2:
    1015         @set_arg_8_status_of_pseudo_status try %
    1016         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
    1017       ]
    1018     |2:
    1019     |3:
    1020     |4:
    1021     |5:
    1022       #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1023       whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
    1024       whd in ⊢ (??%?);
    1025       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1026       whd in ⊢ (??%?);
    1027       inversion (half_add ???) #carry #bl #carry_bl_refl normalize nodelta
    1028       @(pair_replace ?????????? (refl_to_jmrefl ??? carry_bl_refl))
    1029       [1:
    1030       |2:
    1031       ]
    1032     ]
    1033   |5,6,7,8,9: (* INC and DEC *)
    1034     cases daemon
    1035   |42,44: (* RL and RR *)
    1036     (* XXX: work on the right hand side *)
    1037     (* XXX: switch to the left hand side *)
    1038     >EQP -P normalize nodelta
    1039     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1040     whd in maps_assm:(??%%);
    1041     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
    1042     [2,4: normalize nodelta #absurd destruct(absurd) ]
    1043     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1044     whd in ⊢ (??%?);
    1045     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    1046     change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    1047     [2,4:
    1048       >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
    1049       @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    1050       >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
    1051       %
    1052     ]
    1053     @sym_eq @set_clock_status_of_pseudo_status
    1054     [2,4:
    1055       %
    1056     ]
    1057     @sym_eq @set_program_counter_status_of_pseudo_status %
    1058   |43,45: (* RLC and RRC *)
    1059     (* XXX: work on the right hand side *)
    1060     (* XXX: switch to the left hand side *)
    1061     >EQP -P normalize nodelta
    1062     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1063     whd in maps_assm:(??%%);
    1064     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
    1065     [2,4: normalize nodelta #absurd destruct(absurd) ]
    1066     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1067     whd in ⊢ (??%?);
    1068     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    1069     change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    1070     [2,4:
    1071       >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
    1072       @eq_f2
    1073       [1,3:
    1074         @sym_eq
    1075         @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    1076         >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
    1077       |2,4:
    1078         @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
    1079         @sym_eq @set_clock_status_of_pseudo_status %
    1080       ]
    1081     |1,3:
    1082       @sym_eq @set_arg_1_status_of_pseudo_status try %
    1083       @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    1084       >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
    1085     ]
    1086   |1,2: (* ADD and ADDC *)
     792  [(*1,2: (* ADD and ADDC *)
    1087793    (* XXX: work on the right hand side *)
    1088794    (* XXX: switch to the left hand side *)
    … …  
    1154860        |2:
    1155861          >status_refl
    1156           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1)
    1157           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    1158           lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
    1159           @(subaddressing_mode_elim … addr1)
     862          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
     863          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    1160864        |3:
    1161865          >status_refl
    1162           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1)
    1163           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    1164           lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
    1165           @(subaddressing_mode_elim … addr1)
     866          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
     867          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    1166868        ]
    1167869      |2:
    … …  
    1172874        |2:
    1173875          >status_refl
    1174           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2)
    1175           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    1176           lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
    1177           cases daemon (* XXX: ??? *)
     876          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
     877          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    1178878        |3:
    1179879          >status_refl
    1180           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2)
    1181           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    1182           lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
    1183           cases daemon (* XXX: ??? *)
     880          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
     881          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    1184882        ]
    1185883      |3:
    … …  
    1205903          @I
    1206904        |3:
    1207           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A)
    1208           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    1209           whd in ⊢ (??%?);
    1210           >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    1211         ]
    1212       ]
    1213     ]
    1214   |10: (* MUL *)
     905          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A)
     906          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
     907          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
     908        ]
     909      ]
     910    ]
     911  |4: (* INC *)
     912    (* XXX: work on the right hand side *)
     913    (* XXX: switch to the left hand side *)
     914    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
     915    @(subaddressing_mode_elim … addr) normalize nodelta
     916    [1:
     917      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     918      whd in maps_assm:(??%%);
     919      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     920      [2: normalize nodelta #absurd destruct(absurd) ]
     921      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     922      whd in ⊢ (??%?);
     923      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     924      whd in ⊢ (??%?);
     925      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
     926      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
     927      [1:
     928        @eq_f2 try %
     929        @(pose … (set_clock ????)) #status #status_refl
     930        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     931        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
     932      |2:
     933        @set_arg_8_status_of_pseudo_status try %
     934        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
     935      ]
     936    |2:
     937      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     938      whd in maps_assm:(??%%);
     939      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     940      [2: normalize nodelta #absurd destruct(absurd) ]
     941      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     942      whd in ⊢ (??%?);
     943      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     944      whd in ⊢ (??%?);
     945      @let_pair_in_status_of_pseudo_status
     946      [1:
     947        @eq_f2 try %
     948        @(pose … (set_clock ????)) #status #status_refl
     949        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     950        >EQs >EQticks
     951        [1:
     952          @sym_eq @set_clock_status_of_pseudo_status %
     953        |2:
     954          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
     955        |3:
     956          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
     957        ]
     958      |2:
     959        #carry #result
     960        @sym_eq @set_arg_8_status_of_pseudo_status try %
     961        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
     962      ]
     963    |3:
     964      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     965      whd in maps_assm:(??%%);
     966      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     967      [2: normalize nodelta #absurd destruct(absurd) ]
     968      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     969      whd in ⊢ (??%?);
     970      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     971      whd in ⊢ (??%?);
     972      @let_pair_in_status_of_pseudo_status
     973      [1:
     974        @eq_f2 try %
     975        @(pose … (set_clock ????)) #status #status_refl
     976        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     977        >EQs >EQticks
     978        [1:
     979          @sym_eq @set_clock_status_of_pseudo_status %
     980        |2:
     981          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
     982        |3:
     983          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
     984        ]
     985      |2:
     986        #carry #result
     987        @sym_eq @set_arg_8_status_of_pseudo_status try %
     988        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
     989      ]
     990    |4:
     991      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     992      whd in maps_assm:(??%%);
     993      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     994      [2: normalize nodelta #absurd destruct(absurd) ]
     995      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     996      whd in ⊢ (??%?);
     997      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     998      whd in ⊢ (??%?);
     999      @let_pair_in_status_of_pseudo_status
     1000      [1:
     1001        @eq_f2 try %
     1002        @(pose … (set_clock ????)) #status #status_refl
     1003        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1004        >EQs >EQticks
     1005        [1:
     1006          @sym_eq @set_clock_status_of_pseudo_status %
     1007        |2:
     1008          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1009        |3:
     1010          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1011        ]
     1012      |2:
     1013        #carry #result
     1014        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1015        [1:
     1016          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1017        |2:
     1018          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
     1019        ]
     1020      ]
     1021    |5:
     1022      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1023      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1024      whd in ⊢ (??%?);
     1025      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1026      whd in ⊢ (??%?);
     1027      @let_pair_in_status_of_pseudo_status
     1028      [1:
     1029        @eq_f2 try %
     1030        @(pose … (set_clock ????)) #status #status_refl
     1031        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
     1032        >EQs >EQticks %
     1033      |2:
     1034        #carry #bl
     1035        @sym_eq @let_pair_in_status_of_pseudo_status
     1036        [1:
     1037          @eq_f3 try %
     1038          @(pose … (set_clock ????)) #status #status_refl
     1039          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
     1040          >EQs >EQticks %
     1041        |2:
     1042          #carry' #bu
     1043          @sym_eq @set_8051_sfr_status_of_pseudo_status %
     1044        ]
     1045      ]
     1046    ]
     1047  |5: (* DEC *)
     1048    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
     1049    @(subaddressing_mode_elim … addr) normalize nodelta
     1050    [1:
     1051      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1052      whd in maps_assm:(??%%);
     1053      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1054      [2: normalize nodelta #absurd destruct(absurd) ]
     1055      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1056      whd in ⊢ (??%?);
     1057      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1058      whd in ⊢ (??%?);
     1059      @let_pair_in_status_of_pseudo_status
     1060      [1:
     1061        @eq_f3 try %
     1062        @(pose … (set_clock ????)) #status #status_refl
     1063        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1064        >EQs >EQticks try %
     1065        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
     1066      |2:
     1067        #result #flags
     1068        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1069        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
     1070      ]
     1071    |2:
     1072      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1073      whd in maps_assm:(??%%);
     1074      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1075      [2: normalize nodelta #absurd destruct(absurd) ]
     1076      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1077      whd in ⊢ (??%?);
     1078      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1079      whd in ⊢ (??%?);
     1080      @let_pair_in_status_of_pseudo_status
     1081      [1:
     1082        @eq_f3 try %
     1083        @(pose … (set_clock ????)) #status #status_refl
     1084        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1085        >EQs >EQticks try %
     1086        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
     1087      |2:
     1088        #result #flags
     1089        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1090        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
     1091      ]
     1092    |3:
     1093      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1094      whd in maps_assm:(??%%);
     1095      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1096      [2: normalize nodelta #absurd destruct(absurd) ]
     1097      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1098      whd in ⊢ (??%?);
     1099      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1100      whd in ⊢ (??%?);
     1101      @let_pair_in_status_of_pseudo_status
     1102      [1:
     1103        @eq_f3 try %
     1104        @(pose … (set_clock ????)) #status #status_refl
     1105        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1106        >EQs >EQticks try %
     1107        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
     1108      |2:
     1109        #result #flags
     1110        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1111        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
     1112      ]
     1113    |4:
     1114      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1115      whd in maps_assm:(??%%);
     1116      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1117      [2: normalize nodelta #absurd destruct(absurd) ]
     1118      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1119      whd in ⊢ (??%?);
     1120      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1121      whd in ⊢ (??%?);
     1122      @let_pair_in_status_of_pseudo_status
     1123      [1:
     1124        @eq_f3 try %
     1125        @(pose … (set_clock ????)) #status #status_refl
     1126        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     1127        >EQs >EQticks try %
     1128        [1:
     1129          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1130        |2:
     1131          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1132        ]
     1133      |2:
     1134        #result #flags
     1135        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1136        [1:
     1137          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1138        |2:
     1139          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
     1140        ]
     1141      ]
     1142    ]
     1143  |6: (* MUL *)
    12151144    (* XXX: work on the right hand side *)
    12161145    (* XXX: switch to the left hand side *)
    … …  
    12541183    ]
    12551184    @sym_eq @set_program_counter_status_of_pseudo_status %
    1256   |11,12: (* DIV *)
     1185  |7,8: (* DIV *)
    12571186    (* XXX: work on the right hand side *)
    12581187    (* XXX: switch to the left hand side *)
    … …  
    12681197    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    12691198    whd in ⊢ (??%?); normalize nodelta
    1270     cases daemon (* XXX: need match_nat_replace but is not working! *)
    1271   |13: (* DA *)
     1199    @(match_nat_status_of_pseudo_status M' cm sigma policy)
     1200    [1,4:
     1201      @eq_f
     1202      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1203      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1204    |2,5:
     1205      @sym_eq @set_flags_status_of_pseudo_status %
     1206    |3,6:
     1207      #n @sym_eq @set_flags_status_of_pseudo_status try %
     1208      @sym_eq @set_8051_sfr_status_of_pseudo_status
     1209      [1,3:
     1210        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
     1211        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
     1212        @eq_f @eq_f2 try % @eq_f
     1213        @(pose … (set_clock ????)) #status #status_refl
     1214        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1215        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1216      |2,4:
     1217        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
     1218        @(pose … (set_clock ????)) #status #status_refl
     1219        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1220        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1221      ]
     1222    ]
     1223  |9: (* DA *)
    12721224    (* XXX: work on the right hand side *)
    12731225    (* XXX: switch to the left hand side *)
    … …  
    13531305      ]
    13541306    ]
    1355   |14: (* DA *)
     1307  |10: (* DA *)
    13561308    (* XXX: work on the right hand side *)
    13571309    (* XXX: switch to the left hand side *)
    … …  
    14111363      ]
    14121364    ]
    1413   |15: (* DA *)
     1365  |11: (* DA *)
    14141366    (* XXX: work on the right hand side *)
    14151367    (* XXX: switch to the left hand side *)
    … …  
    14561408      ]
    14571409    ]
    1458   |36: (* CLR *)
     1410  |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1411    cases daemon
     1412  |29,30: (* ANL and ORL *)
     1413    inversion addr
     1414    [1,3:
     1415      *
     1416      [1,3:
     1417        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
     1418        >EQP -P normalize nodelta
     1419        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1420        whd in maps_assm:(??%%);
     1421        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1422        [2,4: normalize nodelta #absurd destruct(absurd) ]
     1423        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1424        [2,4: normalize nodelta #absurd destruct(absurd) ]
     1425        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1426        whd in ⊢ (??%?);
     1427        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1428        change with (set_arg_8 ????? = ?)
     1429        @set_arg_8_status_of_pseudo_status try %
     1430        >EQs >EQticks <instr_refl >addr_refl
     1431        [1,4:
     1432          @sym_eq @set_clock_status_of_pseudo_status
     1433          [1,3:
     1434            @sym_eq @set_program_counter_status_of_pseudo_status %
     1435          |2,4:
     1436            @eq_f2 %
     1437          ]
     1438        |2,5:
     1439          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     1440          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
     1441        |3,6:
     1442          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     1443          [1,5:
     1444            @(subaddressing_mode_elim … acc_a) %
     1445          |4,8:
     1446            @eq_f2
     1447            @(pose … (set_clock ????)) #status #status_refl
     1448            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1449            [1,5:
     1450              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     1451              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
     1452            |3,7:
     1453              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     1454              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1455            |2,6:
     1456              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     1457              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
     1458            |4,8:
     1459              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     1460              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1461            ]
     1462          |*:
     1463            %
     1464          ]
     1465        ]
     1466      |2,4:
     1467        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
     1468        >EQP -P normalize nodelta
     1469        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1470        whd in maps_assm:(??%%);
     1471        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1472        [2,4: normalize nodelta #absurd destruct(absurd) ]
     1473        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1474        [2,4: normalize nodelta #absurd destruct(absurd) ]
     1475        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1476        whd in ⊢ (??%?);
     1477        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1478        change with (set_arg_8 ????? = ?)
     1479        @set_arg_8_status_of_pseudo_status try %
     1480        >EQs >EQticks <instr_refl >addr_refl
     1481        [1,4:
     1482          @sym_eq @set_clock_status_of_pseudo_status
     1483          [1,3:
     1484            @sym_eq @set_program_counter_status_of_pseudo_status %
     1485          |2,4:
     1486            @eq_f2 %
     1487          ]
     1488        |2,5:
     1489          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     1490          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
     1491        |3,6:
     1492          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     1493          [1,5:
     1494            @(subaddressing_mode_elim … direct) #w %
     1495          |4,8:
     1496            @eq_f2
     1497            @(pose … (set_clock ????)) #status #status_refl
     1498            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1499            [1,5:
     1500              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     1501              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
     1502            |3,7:
     1503              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     1504              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1505            |2,6:
     1506              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     1507              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
     1508            |4,8:
     1509              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     1510              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1511            ]
     1512          |*:
     1513            %
     1514          ]
     1515        ]
     1516      ]
     1517    |2,4:
     1518      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
     1519      >EQP -P normalize nodelta
     1520      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1521      whd in maps_assm:(??%%);
     1522      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1523      [2,4: normalize nodelta #absurd destruct(absurd) ]
     1524      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1525      [2,4: normalize nodelta #absurd destruct(absurd) ]
     1526      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1527      whd in ⊢ (??%?);
     1528      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1529      change with (set_flags ?????? = ?)
     1530      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
     1531      >EQs >EQticks <instr_refl >addr_refl
     1532      @sym_eq @set_clock_status_of_pseudo_status %
     1533    ]
     1534  |31: (* XRL *)
     1535    inversion addr
     1536    [1:
     1537      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
     1538      >EQP -P normalize nodelta
     1539      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1540      whd in maps_assm:(??%%);
     1541      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1542      [2: normalize nodelta #absurd destruct(absurd) ]
     1543      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1544      [2: normalize nodelta #absurd destruct(absurd) ]
     1545      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1546      whd in ⊢ (??%?);
     1547      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1548      change with (set_arg_8 ????? = ?)
     1549      @set_arg_8_status_of_pseudo_status try %
     1550      >EQs >EQticks <instr_refl >addr_refl
     1551      [1:
     1552        @sym_eq @set_clock_status_of_pseudo_status
     1553        [1:
     1554          @sym_eq @set_program_counter_status_of_pseudo_status %
     1555        |2:
     1556          @eq_f2 %
     1557        ]
     1558      |2:
     1559        @(subaddressing_mode_elim … acc_a) @I
     1560      |3:
     1561        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     1562        [1:
     1563          @(subaddressing_mode_elim … acc_a) %
     1564        |4:
     1565          @eq_f2
     1566          @(pose … (set_clock ????)) #status #status_refl
     1567          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1568          [1:
     1569            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     1570            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
     1571          |3:
     1572            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     1573            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1574          |2:
     1575            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     1576            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
     1577          |4:
     1578            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     1579            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1580          ]
     1581        |*:
     1582          %
     1583        ]
     1584      ]
     1585    |2:
     1586      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
     1587      >EQP -P normalize nodelta
     1588      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1589      whd in maps_assm:(??%%);
     1590      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1591      [2: normalize nodelta #absurd destruct(absurd) ]
     1592      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1593      [2: normalize nodelta #absurd destruct(absurd) ]
     1594      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1595      whd in ⊢ (??%?);
     1596      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1597      change with (set_arg_8 ????? = ?)
     1598      @set_arg_8_status_of_pseudo_status try %
     1599      >EQs >EQticks <instr_refl >addr_refl
     1600      [1:
     1601        @sym_eq @set_clock_status_of_pseudo_status
     1602        [1:
     1603          @sym_eq @set_program_counter_status_of_pseudo_status %
     1604        |2:
     1605          @eq_f2 %
     1606        ]
     1607      |2:
     1608        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     1609        [1: @(subaddressing_mode_elim … direct) #w % ] %
     1610      |3:
     1611        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     1612        [1:
     1613          @(subaddressing_mode_elim … direct) #w %
     1614        |4:
     1615          @eq_f2
     1616          @(pose … (set_clock ????)) #status #status_refl
     1617          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1618          [1:
     1619            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     1620            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
     1621          |3:
     1622            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     1623            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1624          |2:
     1625            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     1626            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
     1627          |4:
     1628            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     1629            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1630          ]
     1631        |*:
     1632          %
     1633        ]
     1634      ]
     1635    ]
     1636  |32: (* CLR *)
    14591637    >EQP -P normalize nodelta
    14601638    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    14771655      [2: <EQaddr % ] %
    14781656    ]
    1479   |37: (* CLR *)
     1657  |33: (* CLR *)
    14801658    >EQP -P normalize nodelta
    14811659    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    14921670    @sym_eq @set_clock_status_of_pseudo_status
    14931671    >EQs >EQticks <instr_refl %
    1494   |38: (* CLR *)
     1672  |34: (* CLR *)
    14951673    >EQP -P normalize nodelta
    14961674    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    15091687      >EQs >EQticks <instr_refl %
    15101688    |*:
    1511       (* XXX: ??? *)
    1512       cases daemon
    1513     ]
    1514   |39: (* CPL *)
     1689      cases daemon (* XXX: requires changes to addressing_mode_ok *)
     1690    ]
     1691  |35: (* CPL *)
    15151692    >EQP -P normalize nodelta
    15161693    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    15371714      [2: <EQaddr % ] %
    15381715    ]
    1539   |40: (* CPL *)
     1716  |36: (* CPL *)
    15401717    >EQP -P normalize nodelta
    15411718    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    15581735      >EQs >EQticks <instr_refl <EQaddr %
    15591736    ]
    1560   |41: (* CPL *)
     1737  |37: (* CPL *)
    15611738    >EQP -P normalize nodelta
    15621739    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    15791756        @sym_eq @set_clock_status_of_pseudo_status %
    15801757      |2:
    1581         (* XXX: ??? *)
    1582         cases daemon
     1758        cases daemon (* XXX: require changes to addressing_mode_ok *)
    15831759      ]
    15841760    |2:
    … …  
    15861762      >EQs >EQticks <instr_refl <EQaddr %
    15871763    |*:
    1588       (* XXX: same as above, provable but tedious *)
    1589       cases daemon
    1590     ]
    1591   |33: (* (* ANL *)
     1764      cases daemon (* XXX: require changes to addressing_mode_ok *)
     1765    ]
     1766  |38,40: (* RL and RR *)
    15921767    (* XXX: work on the right hand side *)
    15931768    (* XXX: switch to the left hand side *)
    1594     >EQP -P normalize nodelta lapply instr_refl
    1595     inversion addr
    1596     [1:
    1597       #addr' #addr_refl'
    1598       inversion addr'
    1599       #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
    1600       whd in ⊢ (??%? → ?); normalize nodelta cases addr
    1601       [1:
    1602         #acc_a #others normalize nodelta
    1603         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
    1604         [2: normalize nodelta #absurd destruct(absurd) ]
    1605         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    1606         [2: normalize nodelta #absurd destruct(absurd) ]
    1607         normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1608         whd in ⊢ (??%?);
    1609         <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1610         whd in ⊢ (??%?); normalize nodelta
    1611         inversion addr #addr1 #addr2
    1612         @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a)
    1613         @(subaddressing_mode_elim … addr2)
    1614         @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try %
    1615         [1:
    1616           @sym_eq @set_clock_status_of_pseudo_status
    1617           >EQs >EQticks <addr_refl <instr_refl
    1618           [1:
    1619             @sym_eq @set_program_counter_status_of_pseudo_status %
    1620           |2:
    1621             @eq_f2
    1622             [1:
    1623               >addr_refl @(subaddressing_mode_elim … addr1) %
    1624             |2:
    1625               @(clock_status_of_pseudo_status M')
    1626               @sym_eq @set_program_counter_status_of_pseudo_status %
    1627             ]
    1628           ]
    1629         |2:
    1630           cases daemon (* XXX: matita dies here *)
    1631         ]
    1632       |2:
    1633         #direct #others
    1634         @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta
    1635         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
    1636         [2: normalize nodelta #absurd destruct(absurd) ]
    1637         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    1638         [2: normalize nodelta #absurd destruct(absurd) ]
    1639         normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1640         whd in ⊢ (??%?);
    1641         <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1642         whd in ⊢ (??%?); normalize nodelta
    1643         inversion addr #addr1 #addr2
    1644         @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2)
    1645         [1: #w |2: #w1 #w2 ] #addr_refl normalize nodelta
    1646         @set_arg_8_status_of_pseudo_status
    1647       ]
    1648     |2:
    1649       -addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
    1650       whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta
    1651       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
    1652       [2: normalize nodelta #absurd destruct(absurd) ]
    1653       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    1654       [2: normalize nodelta #absurd destruct(absurd) ]
    1655       normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1656       whd in ⊢ (??%?);
    1657       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1658       whd in ⊢ (??%?); normalize nodelta
    1659       inversion addr #addr1 #addr2 #addr_refl normalize nodelta
    1660       @set_flags_status_of_pseudo_status try %
    1661       [1:
    1662         @conjunction_split
    1663         [1:
    1664           @(get_cy_flag_status_of_pseudo_status M')
    1665           @sym_eq @set_clock_status_of_pseudo_status
    1666           >EQs >EQticks <addr_refl <instr_refl %
    1667         |2:
    1668           >EQs >EQticks <addr_refl <instr_refl normalize nodelta
    1669           (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *)
    1670           cases daemon
    1671         ]
    1672       |2:
    1673         @(get_ov_flag_status_of_pseudo_status M')
    1674         @sym_eq @set_clock_status_of_pseudo_status
    1675         >EQs >EQticks <instr_refl <addr_refl %
    1676       |3:
    1677         @sym_eq @set_clock_status_of_pseudo_status
    1678         >EQs >EQticks <instr_refl <addr_refl %
    1679       ]
    1680     ]
     1769    >EQP -P normalize nodelta
     1770    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1771    whd in maps_assm:(??%%);
     1772    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1773    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1774    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1775    whd in ⊢ (??%?);
     1776    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1777    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1778    [2,4:
     1779      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1780      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1781      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1782      %
     1783    ]
     1784    @sym_eq @set_clock_status_of_pseudo_status
     1785    [2,4:
     1786      %
     1787    ]
     1788    @sym_eq @set_program_counter_status_of_pseudo_status %
     1789  |39,41: (* RLC and RRC *)
     1790    (* XXX: work on the right hand side *)
     1791    (* XXX: switch to the left hand side *)
     1792    >EQP -P normalize nodelta
     1793    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1794    whd in maps_assm:(??%%);
     1795    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1796    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1797    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1798    whd in ⊢ (??%?);
     1799    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1800    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1801    [2,4:
     1802      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1803      @eq_f2
     1804      [1,3:
     1805        @sym_eq
     1806        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1807        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
     1808      |2,4:
     1809        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
     1810        @sym_eq @set_clock_status_of_pseudo_status %
     1811      ]
     1812    |1,3:
     1813      @sym_eq @set_arg_1_status_of_pseudo_status try %
     1814      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1815      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
     1816    ]
     1817  |*)42: (* SWAP *)
     1818  |43: (* MOV *)
     1819  |44: (* MOVX *)
     1820  |45: (* SETB *)
     1821    >EQP -P normalize nodelta
     1822    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    16811823    whd in maps_assm:(??%%);
    16821824    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    … …  
    16851827    whd in ⊢ (??%?);
    16861828    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1687     whd in ⊢ (??%?); normalize nodelta *)
    1688   |16: (* JC *)
    1689     (* XXX: work on the right hand side *)
    1690     (* XXX: switch to the left hand side *)
     1829    change with (set_arg_1 ????? = ?)
     1830    >EQs >EQticks <instr_refl
     1831    @set_arg_1_status_of_pseudo_status try %
     1832    lapply addressing_mode_ok_assm_1 (* XXX: move into a lemma *)
     1833    @(subaddressing_mode_elim … b)
     1834    [1,3:
     1835      #_ @I
     1836    |2,4:
     1837      #w cases daemon
     1838      (* XXX: need changes to addressing_mode_ok *)
     1839    ]
     1840  |46: (* PUSH *)
    16911841    >EQP -P normalize nodelta
    1692     #sigma_increment_commutation #maps_assm
    1693     whd in match expand_pseudo_instruction; normalize nodelta
    1694     whd in match expand_relative_jump; normalize nodelta
    1695     whd in match expand_relative_jump_internal; normalize nodelta
    1696     @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta
    1697     inversion sj_possible #sj_possible_refl
     1842    #sigma_increment_commutation whd in ⊢ (??%% → ?);
     1843    inversion M #callM #accM #callM_accM_refl normalize nodelta
     1844    @(subaddressing_mode_elim … addr) #w normalize nodelta
     1845    @Some_Some_elim #Mrefl destruct(Mrefl)
     1846    cases daemon (* XXX *)
     1847  |47: (* POP *)
     1848  |48: (* XCH *)
     1849    >EQP -P normalize nodelta
     1850    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1851    whd in maps_assm:(??%%);
     1852    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1853    [2: normalize nodelta #absurd destruct(absurd) ]
     1854    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1855    [2: normalize nodelta #absurd destruct(absurd) ]
     1856    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1857    whd in ⊢ (??%?);
     1858    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1859    change with (set_arg_8 ????? = ?)
     1860    >EQs >EQticks <instr_refl
     1861    @set_arg_8_status_of_pseudo_status try %
    16981862    [1:
    1699       #fetch_many_assm %{1}
    1700       whd in maps_assm:(??%%);
    1701       lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
    1702       whd in ⊢ (??%?); normalize nodelta
    1703       <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1704       whd in ⊢ (??%?); normalize nodelta
    1705       @(if_then_else_replace ???????? p) normalize nodelta
     1863      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
     1864      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
     1865      @(pose … (set_clock ????)) #status #status_refl
     1866      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    17061867      [1:
    1707         >EQs @(get_cy_flag_status_of_pseudo_status M')
    1708         @sym_eq @set_program_counter_status_of_pseudo_status %
     1868        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
     1869        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    17091870      |2:
    1710         @(if_then_else_replace ???????? p) normalize nodelta try %
     1871        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
     1872        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1873      ]
     1874    |2:
     1875      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
     1876      [1:
     1877        /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     1878      |*:
     1879        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     1880        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     1881        whd in match sfr_8051_index; normalize nodelta
     1882        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
     1883      ]
     1884    |3:
     1885      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
     1886      [1:
     1887        /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     1888      |2:
     1889        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     1890        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     1891        whd in match sfr_8051_index; normalize nodelta
     1892        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
     1893      |3:
     1894        @(pose … (set_clock ????)) #status #status_refl
     1895        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1896        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1897      ]
     1898    ]
     1899  |49: (* XCHD *)
     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    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1906    [2: normalize nodelta #absurd destruct(absurd) ]
     1907    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1908    whd in ⊢ (??%?);
     1909    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1910    whd in ⊢ (??%?);
     1911    @(pair_replace ?????????? p) normalize nodelta
     1912    >EQs >EQticks <instr_refl
     1913    [1:
     1914      @eq_f
     1915      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1916      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     1917      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1918    |2:
     1919      @(pair_replace ?????????? p1) normalize nodelta
     1920      >EQs >EQticks <instr_refl
     1921      [1:
     1922        @eq_f
     1923        @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1924        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1925        [1:
     1926          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
     1927          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1928        |2:
     1929          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
     1930          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1931        ]
     1932      |2:
     1933        @(pair_replace ?????????? p) normalize nodelta
    17111934        >EQs >EQticks <instr_refl
    1712         @set_program_counter_status_of_pseudo_status
    1713         [1:
    1714           >EQaddr_of normalize nodelta
    1715           whd in match addr_of_relative; normalize nodelta
    1716           whd in match (program_counter ???);
    1717           check address_of_word_labels_code_mem_Some_hit
    1718           >EQlookup_labels
    1719          
    1720           >sigma_increment_commutation
    1721           whd in match assembly_1_pseudoinstruction; normalize nodelta
    1722           whd in match expand_pseudo_instruction; normalize nodelta
    1723           whd in match expand_relative_jump; normalize nodelta
    1724           whd in match expand_relative_jump_internal; normalize nodelta
    1725           @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1935        [1:
     1936          %
     1937        |2:
     1938          @(pair_replace ?????????? p1) normalize nodelta
     1939          >EQs >EQticks <instr_refl
    17261940          [1:
    1727             >EQppc %
     1941            %
    17281942          |2:
    1729             >sj_possible_refl normalize nodelta normalize in match (length ??);
    1730             lapply sigma_increment_commutation
    1731             whd in match assembly_1_pseudoinstruction; normalize nodelta
    1732             whd in match (length ??); normalize nodelta
    1733             cases daemon
    1734             (* XXX: missing invariant? *)
    1735           ]
    1736         |2:
    1737           @sym_eq @set_clock_status_of_pseudo_status try %
    1738           @eq_f2 try % whd in ⊢ (??%%);
    1739           whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation
    1740           whd in match assembly_1_pseudoinstruction; normalize nodelta
    1741           whd in match expand_pseudo_instruction; normalize nodelta
    1742           whd in match expand_relative_jump; normalize nodelta
    1743           whd in match expand_relative_jump_internal; normalize nodelta
    1744           @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
    1745           [1:
    1746             @eq_f2 try % >EQppc %
    1747           |2:
    1748             @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1943            @set_arg_8_status_of_pseudo_status try %
    17491944            [1:
    1750               @eq_f2 try % (* XXX: finish, use Jaap's invariant *)
    1751               cases daemon
     1945              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
     1946              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    17521947            |2:
    1753               #_ >sj_possible_refl %
     1948              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
     1949              [1:
     1950                /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     1951              |2:
     1952                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     1953                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     1954                whd in match sfr_8051_index; normalize nodelta
     1955                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
     1956              ]
     1957            |3:
     1958              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
     1959              [1:
     1960                /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     1961              |2:
     1962                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     1963                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     1964                whd in match sfr_8051_index; normalize nodelta
     1965                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
     1966              ]
    17541967            ]
    17551968          ]
    17561969        ]
    17571970      ]
     1971    ]
     1972  |*)50: (* RET *)
     1973    >EQP -P normalize nodelta
     1974    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1975    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
     1976    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
     1977    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
     1978    [2: normalize nodelta #absurd destruct(absurd) ]
     1979    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
     1980    [2: normalize nodelta #absurd destruct(absurd) ]
     1981    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
     1982    whd in ⊢ (??%?);
     1983    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1984    whd in ⊢ (??%?);
     1985    @(pair_replace ?????????? p) normalize nodelta
     1986    >EQs >EQticks <instr_refl
     1987    [1:
     1988      @eq_f3 try %
     1989      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1990      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
    17581991    |2:
    1759       normalize nodelta >EQppc
    1760       * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    1761       * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    1762       * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    1763       #fetch_many_assm whd in fetch_many_assm; %{2}
    1764       change with (execute_1 ?? = ?)
    1765       @(pose … (execute_1 ? (status_of_pseudo_status …)))
    1766       #status_after_1 #EQstatus_after_1
    1767       cases daemon (* XXX: ??? *)
    1768     ]
    1769   ]
     1992      @(pair_replace ?????????? p1) normalize nodelta
     1993      >EQs >EQticks <instr_refl
     1994      [1:
     1995        @eq_f3 try %
     1996        @sym_eq @(pose … (set_clock ????)) #status #status_refl
     1997        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
     1998        [1:
     1999          cases daemon
     2000          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2001        |2:
     2002          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     2003          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     2004          whd in match sfr_8051_index; normalize nodelta
     2005          >get_index_v_set_index_hit
     2006          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
     2007          cases daemon
     2008          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2009        ]
     2010      |2:
     2011        cases daemon (* XXX *)
     2012      ]
     2013    ]
     2014  |51: (* RETI *)
     2015  |52: (* NOP *)
     2016    >EQP -P normalize nodelta
     2017    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2018    whd in maps_assm:(??%%);
     2019    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
     2020    whd in ⊢ (??%?);
     2021    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     2022    change with (set_clock ???? = ?)
     2023    @set_clock_status_of_pseudo_status %
     2024  ]
    17702025qed.
    17712026
Note: See TracChangeset for help on using the changeset viewer.