Ignore:
Timestamp:
Jul 13, 2012, 11:00:04 AM (8 years ago)
Author:
mulligan
Message:

Work from the last week on the new formulation of the main lemma for assembler correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2173 r2181  
    3535    destruct(absurd)
    3636  ]
     37qed.
     38
     39lemma addressing_mode_ok_to_snd_M_data:
     40  ∀M, cm, ps.
     41  ∀addr: [[acc_a]].
     42  addressing_mode_ok pseudo_assembly_program M cm ps addr = true →
     43    \snd M = data.
     44  #M #addr #ps #addr
     45  @(subaddressing_mode_elim … addr)
     46  whd in ⊢ (??%? → ?);
     47  cases (\snd M) normalize nodelta
     48  [2:
     49    * #address #absurd destruct(absurd)
     50  ]
     51  #_ %
     52qed.
     53
     54lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
     55  ∀A, B: Type[0].
     56  ∀e: A.
     57  ∀the_list: list (A × B).
     58  ∀eq_f: A → A → bool.
     59    assoc_list_exists A B e eq_f the_list = true →
     60      ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
     61  #A #B #e #the_list #eq_f elim the_list
     62  [1:
     63    whd in ⊢ (??%? → ?); #absurd destruct(absurd)
     64  |2:
     65    #hd #tl #inductive_hypothesis
     66    whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
     67    cases (eq_f (\fst hd) e) normalize nodelta
     68    [1:
     69      #_ %{(\snd hd)} %
     70    |2:
     71      @inductive_hypothesis
     72    ]
     73  ]
     74qed.
     75
     76lemma assoc_list_exists_false_to_assoc_list_lookup_None:
     77  ∀A, B: Type[0].
     78  ∀e, e': A.
     79  ∀the_list, the_list': list (A × B).
     80  ∀eq_f: A → A → bool.
     81    e = e' →
     82    the_list = the_list' →
     83      assoc_list_exists A B e eq_f the_list = false →
     84        assoc_list_lookup A B e' eq_f the_list' = None ….
     85  #A #B #e #e' #the_list elim the_list
     86  [1:
     87    #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
     88  |2:
     89    #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
     90    whd in ⊢ (??%? → ??%?); <e_refl
     91    cases (eq_f (\fst hd) e) normalize nodelta
     92    [1:
     93      #absurd destruct(absurd)
     94    |2:
     95      >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
     96    ]
     97  ]
     98qed.
     99
     100lemma lookup_low_internal_ram_false:
     101  ∀cm: pseudo_assembly_program.
     102  ∀status.
     103  ∀b: BitVector 7.
     104    lookup … b (low_internal_ram … cm status) (zero 8) = false:::b.
     105  #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter
     106  #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b
     107  cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *)
     108qed.
     109
     110lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
     111  ∀M', cm, status, sigma.
     112  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
     113    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
     114    map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status sigma addr1.
     115  #M' #cm #status #sigma #addr1
     116  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
     117  [1: #_ @I ]
     118  #w whd in ⊢ (??%? → %);
     119  inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
     120  [1:
     121    #absurd destruct(absurd)
     122  |2:
     123    #_
     124    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     125    cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false
     126  ]
     127qed.
     128
     129lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
     130  ∀M', cm.
     131  ∀sigma, status, b.
     132  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
     133    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
     134      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status addr1 b = b.
     135  #M' #cm #sigma #status #b #addr1
     136  @(subaddressing_mode_elim … addr1)
     137  [1:
     138    whd in ⊢ (??%? → ??%?); cases (\snd M')
     139    [1:
     140      normalize nodelta #_ %
     141    |2:
     142      * #address normalize nodelta #absurd destruct(absurd)
     143    ]
     144  |2,4:
     145    #w whd in ⊢ (??%? → ??%?);
     146    inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
     147    [1,3:
     148      #absurd destruct(absurd)
     149    |2,4:
     150      #_ >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     151      normalize nodelta %
     152    ]
     153  |3:
     154    #w whd in ⊢ (??%? → ??%?);
     155    cases daemon (* XXX: ??? *)
     156  |5:
     157    #w #_ %
     158  ]
     159qed.
     160
     161lemma set_flags_status_of_pseudo_status:
     162  ∀M.
     163  ∀sigma.
     164  ∀policy.
     165  ∀code_memory: pseudo_assembly_program.
     166  ∀s: PreStatus ? code_memory.
     167  ∀s'.
     168  ∀b, b': Bit.
     169  ∀opt, opt': option Bit.
     170  ∀c, c': Bit.
     171    b = b' →
     172    opt = opt' →
     173    c = c' →
     174    status_of_pseudo_status M code_memory s sigma policy = s' →
     175      set_flags … s' b opt c =
     176        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
     177  #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
     178  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
     179  whd in match status_of_pseudo_status; normalize nodelta
     180  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     181  cases (\snd M)
     182  [1:
     183    normalize nodelta %
     184  |2:
     185    * #address normalize nodelta
     186    @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     187    whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
     188    @split_eq_status try % whd in match (sfr_8051_index ?);
     189    cases daemon
     190  ]
     191qed.
     192
     193(* XXX: copied from Test.ma *)
     194lemma let_pair_in_status_of_pseudo_status:
     195  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     196    c = c' →
     197    (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
     198    let 〈left, right〉 ≝ c' in (s' left right c') =
     199    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     200  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
     201qed.
     202
     203(* XXX: copied from Test.ma *)
     204lemma let_pair_as_in_status_of_pseudo_status:
     205  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     206    c = c' →
     207    (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →
     208    let 〈left, right〉 as H' ≝ c' in (s' left right H' c') =
     209    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
     210  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
     211  destruct(destruct_refl) /2/
    37212qed.
    38213
     
    10681243  try @split_eq_status try %
    10691244  cases daemon *)
    1070   [42,43,44,45,49,52,56:
     1245  [42,44: (* RL and RR *)
     1246    (* XXX: work on the right hand side *)
     1247    (* XXX: switch to the left hand side *)
     1248    >EQP -P normalize nodelta
     1249    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1250    whd in maps_assm:(??%%);
     1251    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1252    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1253    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1254    whd in ⊢ (??%?);
     1255    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1256    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1257    [2,4:
     1258      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1259      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1260      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1261      %
     1262    ]
     1263    @sym_eq @set_clock_status_of_pseudo_status
     1264    [2,4:
     1265      %
     1266    ]
     1267    @sym_eq @set_program_counter_status_of_pseudo_status %
     1268  |43,45: (* RLC and RRC *)
     1269    (* XXX: work on the right hand side *)
     1270    (* XXX: switch to the left hand side *)
     1271    >EQP -P normalize nodelta
     1272    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1273    whd in maps_assm:(??%%);
     1274    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1275    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1276    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1277    whd in ⊢ (??%?);
     1278    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1279    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1280    [2,4:
     1281      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
     1282      @eq_f2
     1283      [1,3:
     1284        @sym_eq
     1285        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1286        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
     1287      |2,4:
     1288        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
     1289        @sym_eq @set_clock_status_of_pseudo_status %
     1290      ]
     1291    |1,3:
     1292      @sym_eq @set_arg_1_status_of_pseudo_status try %
     1293      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1294      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
     1295    ]
     1296  |1,2: (* ADD and ADDC *)
     1297    (* XXX: work on the right hand side *)
     1298    (* XXX: switch to the left hand side *)
     1299    >EQP -P normalize nodelta
     1300    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1301    whd in maps_assm:(??%%);
     1302    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1303    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1304    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1305    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1306    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1307    whd in ⊢ (??%?);
     1308    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1309    whd in ⊢ (??%?);
     1310    @(pair_replace ?????????? p)
     1311    [2,4:
     1312      @(pair_replace ?????????? p)
     1313      [2,4:
     1314        normalize nodelta
     1315        @set_flags_status_of_pseudo_status try %
     1316        @sym_eq @set_arg_8_status_of_pseudo_status try %
     1317        @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
     1318      |1,3:
     1319        @eq_f3
     1320        [1,2,4,5:
     1321          normalize nodelta
     1322          >EQs >EQticks <instr_refl %
     1323        |3:
     1324          %
     1325        |6:
     1326          normalize nodelta
     1327          @eq_f @eq_f2
     1328          [1:
     1329            >EQs %
     1330          |2:
     1331            >EQticks @eq_f2 <instr_refl try % >EQs %
     1332          ]
     1333        ]
     1334      ]
     1335    |1,3:
     1336      @eq_f3
     1337      [1,2,4,5:
     1338        normalize nodelta
     1339        >EQs >EQticks <instr_refl
     1340        cases daemon (* XXX: matita dies here *)
     1341      |3:
     1342        %
     1343      |6:
     1344        normalize nodelta
     1345        @(get_cy_flag_status_of_pseudo_status … M')
     1346        @sym_eq @set_clock_status_of_pseudo_status
     1347        [1:
     1348          @sym_eq >EQs
     1349          @set_program_counter_status_of_pseudo_status %
     1350        |2:
     1351          >EQticks <instr_refl >EQs %
     1352        ]
     1353      ]
     1354    ]
     1355  |3: (* SUB *)
     1356    (* XXX: work on the right hand side *)
     1357    (* XXX: switch to the left hand side *)
     1358    >EQP -P normalize nodelta
     1359    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1360    whd in maps_assm:(??%%);
     1361    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1362    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1363    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1364    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1365    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1366    whd in ⊢ (??%?);
     1367    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1368    whd in ⊢ (??%?);
     1369    @(pair_replace ?????????? p)
     1370    [1:
     1371      @eq_f3
     1372      normalize nodelta >EQs >EQticks <instr_refl
     1373      [1:
     1374        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
     1375        @(get_arg_8_status_of_pseudo_status cm status … M')
     1376        [1:
     1377          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
     1378        |2:
     1379          >status_refl
     1380          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1)
     1381          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1382          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
     1383          @(subaddressing_mode_elim … addr1)
     1384        |3:
     1385          >status_refl
     1386          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1)
     1387          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1388          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
     1389          @(subaddressing_mode_elim … addr1)
     1390        ]
     1391      |2:
     1392        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
     1393        @(get_arg_8_status_of_pseudo_status cm status … M')
     1394        [1:
     1395          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
     1396        |2:
     1397          >status_refl
     1398          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2)
     1399          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1400          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
     1401          cases daemon (* XXX: ??? *)
     1402        |3:
     1403          >status_refl
     1404          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2)
     1405          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1406          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
     1407          cases daemon (* XXX: ??? *)
     1408        ]
     1409      |3:
     1410        @(get_cy_flag_status_of_pseudo_status … M')
     1411        @sym_eq @set_clock_status_of_pseudo_status
     1412        [1:
     1413          >sigma_increment_commutation
     1414        |2:
     1415          %
     1416        ]
     1417      ]
     1418    |2:
     1419      normalize nodelta
     1420      @(pair_replace ?????????? p)
     1421      [1:
     1422        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
     1423      |2:
     1424        @set_flags_status_of_pseudo_status try %
     1425        @sym_eq @set_arg_8_status_of_pseudo_status
     1426        [1:
     1427          @sym_eq @set_clock_status_of_pseudo_status %
     1428        |2:
     1429          @I
     1430        |3:
     1431          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A)
     1432          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1433          whd in ⊢ (??%?);
     1434          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1435        ]
     1436      ]
     1437    ]
     1438  |4,5,6,7,8,9: (* INC and DEC *)
     1439    (* XXX: work on the right hand side *)
     1440    (* XXX: switch to the left hand side *)
     1441    >EQP -P normalize nodelta
     1442    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1443    whd in maps_assm:(??%%);
     1444    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1445    [2,4,6,8,10,12: normalize nodelta #absurd destruct(absurd) ]
     1446    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1447    whd in ⊢ (??%?);
     1448    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1449    @(subaddressing_mode_elim … addr) try #w whd in ⊢ (??%?); normalize nodelta
     1450    [1:
     1451      @(jmpair_as_replace ?????????? p)
     1452      [1:
     1453        @eq_f2 try % normalize nodelta
     1454        XXX
     1455      |2:
     1456        @(jmpair_as_replace ?????????? p)
     1457      ]
    10711458  |10: (* MUL *)
    1072   (* XXX: work on the right hand side *)
    1073   (* XXX: switch to the left hand side *)
    1074   >EQP -P normalize nodelta
    1075   #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1076   whd in maps_assm:(??%%);
    1077   inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    1078   [2: normalize nodelta #absurd destruct(absurd) ]
    1079   inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    1080   [2: normalize nodelta #absurd destruct(absurd) ]
    1081   normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1082   whd in ⊢ (??%?);
    1083   <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    1084   change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    1085   [2:
    1086     whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
    1087     @sym_eq
    1088     [1:
    1089       @(get_8051_sfr_status_of_pseudo_status … policy)
    1090       cases daemon (* XXX: need a lemma *)
    1091     |2:
    1092       @(get_8051_sfr_status_of_pseudo_status M' … policy)
    1093       @sym_eq @set_clock_status_of_pseudo_status [2: % ]
    1094       @sym_eq @set_program_counter_status_of_pseudo_status %
    1095     ]
    1096   ]
    1097   @sym_eq @set_8051_sfr_status_of_pseudo_status
    1098   [2:
    1099     >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    1100     @eq_f @eq_f2 try % @eq_f2 @eq_f
    1101     @sym_eq
    1102     [1:
    1103       @(get_8051_sfr_status_of_pseudo_status … policy)
    1104       cases daemon (* XXX: needs a lemma *)
    1105     |2:
    1106       @(get_8051_sfr_status_of_pseudo_status M' … policy)
    1107       @sym_eq @set_clock_status_of_pseudo_status [2: % ]
    1108       @sym_eq @set_program_counter_status_of_pseudo_status %
    1109     ]
    1110   ]
    1111   @sym_eq @set_clock_status_of_pseudo_status
    1112   [2:
    1113     @eq_f %
    1114   ]
    1115   @sym_eq @set_program_counter_status_of_pseudo_status %
     1459    (* XXX: work on the right hand side *)
     1460    (* XXX: switch to the left hand side *)
     1461    >EQP -P normalize nodelta
     1462    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1463    whd in maps_assm:(??%%);
     1464    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1465    [2: normalize nodelta #absurd destruct(absurd) ]
     1466    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1467    [2: normalize nodelta #absurd destruct(absurd) ]
     1468    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1469    whd in ⊢ (??%?);
     1470    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1471    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1472    [2:
     1473      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
     1474      @sym_eq
     1475      [1:
     1476        @(get_8051_sfr_status_of_pseudo_status … policy) #_
     1477        @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
     1478      |2:
     1479        @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1480        @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1481        @sym_eq @set_program_counter_status_of_pseudo_status %
     1482      ]
     1483    ]
     1484    @sym_eq @set_8051_sfr_status_of_pseudo_status
     1485    [2:
     1486      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
     1487      @eq_f @eq_f2 try % @eq_f2 @eq_f
     1488      @sym_eq
     1489      [1:
     1490        @(get_8051_sfr_status_of_pseudo_status … policy) #_
     1491        @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
     1492      |2:
     1493        @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1494        @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1495        @sym_eq @set_program_counter_status_of_pseudo_status %
     1496      ]
     1497    ]
     1498    @sym_eq @set_clock_status_of_pseudo_status
     1499    [2:
     1500      @eq_f %
     1501    ]
     1502    @sym_eq @set_program_counter_status_of_pseudo_status %
     1503  |11,12: (* DIV *)
     1504    (* XXX: work on the right hand side *)
     1505    (* XXX: switch to the left hand side *)
     1506    >EQP -P normalize nodelta
     1507    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1508    whd in maps_assm:(??%%);
     1509    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1510    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1511    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1512    [2,4: normalize nodelta #absurd destruct(absurd) ]
     1513    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1514    whd in ⊢ (??%?);
     1515    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1516    whd in ⊢ (??%?);
     1517    @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm #pose_refl @sym_eq
     1518    @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm' #pose_refl'
     1519    cut(nat_of_bitvector_assm = nat_of_bitvector_assm')
     1520    [1,3:
     1521    |2,4:
     1522      #cut_assm <cut_assm cases nat_of_bitvector_assm try #n' normalize nodelta
     1523      @set_flags_status_of_pseudo_status
     1524    ]
     1525   
    11161526   
    11171527  (* XXX: work on the left hand side *)
Note: See TracChangeset for help on using the changeset viewer.