Changeset 2181


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

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

Location:
src/ASM
Files:
2 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 *)
  • src/ASM/Test.ma

    r2173 r2181  
    1919    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
    2020  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
     21qed.
     22
     23lemma if_then_else_status_of_pseudo_status_true:
     24  ∀M: internal_pseudo_address_map.
     25  ∀cm: pseudo_assembly_program.
     26  ∀sigma: Word → Word.
     27  ∀policy: Word → bool.
     28  ∀s, s', s'', s'''.
     29  ∀t: bool.
     30    t = true →
     31    status_of_pseudo_status M cm s sigma policy = s' →
     32      if t then
     33        s'
     34      else
     35        s'' =
     36      status_of_pseudo_status M cm (if t then s else s''') sigma policy.
     37  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
     38  >t_refl normalize nodelta >s_refl %
     39qed.
     40
     41lemma if_then_else_status_of_pseudo_status_false:
     42  ∀M: internal_pseudo_address_map.
     43  ∀cm: pseudo_assembly_program.
     44  ∀sigma: Word → Word.
     45  ∀policy: Word → bool.
     46  ∀s, s', s'', s'''.
     47  ∀t: bool.
     48    t = false →
     49    status_of_pseudo_status M cm s sigma policy = s' →
     50      if t then
     51        s''
     52      else
     53        s' =
     54      status_of_pseudo_status M cm (if t then s''' else s) sigma policy.
     55  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
     56  >t_refl normalize nodelta >s_refl %
    2157qed.
    2258
     
    225261
    226262lemma get_index_v_status_of_pseudo_status:
    227   ∀M, code_memory, sigma, policy, s, sfr.
    228     (get_index_v Byte 19
     263  ∀M, code_memory, sigma, policy, s, s', sfr.
     264    map_address_using_internal_pseudo_address_map M sigma sfr
     265      (get_index_v Byte 19
     266        (special_function_registers_8051 pseudo_assembly_program code_memory s)
     267        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
     268    get_index_v Byte 19
    229269      (special_function_registers_8051 (BitVectorTrie Byte 16)
    230270      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    231271      (status_of_pseudo_status M code_memory s sigma policy))
    232       (sfr_8051_index sfr) (sfr8051_index_19 sfr) =
    233     map_address_using_internal_pseudo_address_map M sigma sfr
    234       (get_index_v Byte 19
    235         (special_function_registers_8051 pseudo_assembly_program code_memory s)
    236         (sfr_8051_index sfr) (sfr8051_index_19 sfr))).
    237   #M #code_memory #sigma #policy #s #sfr
     272      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
     273  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
    238274  whd in match status_of_pseudo_status; normalize nodelta
    239275  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     
    275311
    276312lemma get_8051_sfr_status_of_pseudo_status:
    277   ∀M, code_memory, sigma, policy, s, s', sfr.
     313  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    278314    status_of_pseudo_status M code_memory s sigma policy = s' →
    279   (get_8051_sfr (BitVectorTrie Byte 16)
     315    map_address_using_internal_pseudo_address_map M sigma sfr
     316     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
     317  get_8051_sfr (BitVectorTrie Byte 16)
    280318    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    281      s' sfr =
    282   map_address_using_internal_pseudo_address_map M sigma sfr
    283    (get_8051_sfr pseudo_assembly_program code_memory s sfr)).
    284   #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
     319     s' sfr = s''.
     320  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
    285321  whd in match get_8051_sfr; normalize nodelta
    286   @get_index_v_status_of_pseudo_status
     322  @get_index_v_status_of_pseudo_status %
    287323qed.
    288324
     
    444480  bit_address_of_register … cm s r.
    445481 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
    446  >(get_8051_sfr_status_of_pseudo_status … (refl …))
     482 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    447483 @pair_elim #un #ln #_
    448484 @pair_elim #r1 #r0 #_ %
     
    452488  primitive *)
    453489axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
    454  ∀M,sigma,cm,s,addr.
     490 ∀M,sigma,cm,s,s',addr.
     491  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
     492  (lookup Byte 7 addr
     493   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    455494  lookup Byte 7 addr
    456495  (low_internal_ram_of_pseudo_low_internal_ram M
    457496   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
    458   =
    459   map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
    460   (lookup Byte 7 addr
    461    (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
     497  = s'.
    462498
    463499(*CSC: provable using the axiom in AssemblyProof, but this one seems more
    464500  primitive *)
    465501axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
    466  ∀M,sigma,cm,s,addr.
     502 ∀M,sigma,cm,s,s',addr.
     503  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
     504  (lookup Byte 7 addr
     505   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    467506  lookup Byte 7 addr
    468507  (high_internal_ram_of_pseudo_high_internal_ram M
    469508   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
    470   =
    471   map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
    472   (lookup Byte 7 addr
    473    (high_internal_ram pseudo_assembly_program cm s) (zero 8)).
     509  = s'.
    474510
    475511lemma get_register_status_of_pseudo_status:
    476  ∀M,cm,sigma,policy,s,s',r.
     512 ∀M,cm,sigma,policy,s,s',s'',r.
    477513  status_of_pseudo_status M cm s sigma policy = s' →
     514  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
     515   (get_register … cm s r) = s'' →
    478516  get_register …
    479517   (code_memory_of_pseudo_assembly_program cm sigma policy)
    480    s' r =
    481   map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
    482    (get_register … cm s r).
    483  #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta
     518   s' r = s''.
     519 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
     520 whd in match get_register; normalize nodelta
    484521 whd in match status_of_pseudo_status; normalize nodelta
    485522 >bit_address_of_register_status_of_pseudo_status
    486  @lookup_low_internal_ram_of_pseudo_low_internal_ram
     523 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
    487524qed.
    488525
     
    586623qed.
    587624
    588 lemma set_arg_8_status_of_pseudo_status:
     625lemma set_arg_8_status_of_pseudo_status':
    589626  ∀cm.
    590627  ∀ps.
     
    654691    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
    655692  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
    656       >(get_register_status_of_pseudo_status … (refl …))
     693      >(get_register_status_of_pseudo_status … (refl …) (refl …))
    657694      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    658695      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
     
    660697      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
    661698      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    662   |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …))
     699  |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
    663700      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    664701      >EQ1 normalize nodelta
     
    667704  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
    668705  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
    669   |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …))
    670       >(get_8051_sfr_status_of_pseudo_status … (refl …))
     706  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     707      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    671708      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
     709qed.
     710
     711lemma set_arg_8_status_of_pseudo_status:
     712  ∀cm.
     713  ∀ps.
     714  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
     715  ∀value.
     716  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
     717   status_of_pseudo_status M cm ps sigma policy = s' →
     718   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     719   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     720    set_arg_8 (BitVectorTrie Byte 16)
     721      (code_memory_of_pseudo_assembly_program cm sigma policy)
     722      s' addr value' =
     723    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
     724  #cm #ps #addr #value
     725  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
     726  @relevant
    672727qed.
    673728
     
    754809    ∀d: Byte.
    755810    ∀l: bool.
    756     ∀M. ∀sigma. ∀policy. ∀s'.
     811    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
     812      map_address_Byte_using_internal_pseudo_address_map M sigma
     813         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
    757814      (status_of_pseudo_status M code_memory s sigma policy) = s' →
    758815        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    759816          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    760           s' d l =
    761         map_address_Byte_using_internal_pseudo_address_map M sigma
    762          d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
    763  #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
    764  #H @H
     817          s' d l) = s''.
     818 #code #s #d #v
     819 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
     820 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
    765821qed.
    766822
    767823lemma program_counter_status_of_pseudo_status:
    768     ∀M. ∀sigma. ∀policy.
     824    ∀M. ∀sigma: Word → Word. ∀policy.
    769825    ∀code_memory: pseudo_assembly_program.
    770826    ∀s: PreStatus ? code_memory.
    771827    ∀s'.
     828    ∀s''.
     829    sigma (program_counter … s) = s'' →
    772830    (status_of_pseudo_status M code_memory s sigma policy) = s' →
    773831      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    774         s' =
    775         sigma (program_counter … s).
    776   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     832        s' = s''.
     833  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
    777834qed.
    778835
     
    786843  #M #cm #sigma #policy #s #s' #s_refl <s_refl
    787844  whd in match get_cy_flag; normalize nodelta
    788   >get_index_v_status_of_pseudo_status %
    789 qed.
    790 
    791 lemma get_arg_8_status_of_pseudo_status:
     845  >(get_index_v_status_of_pseudo_status … (refl …)) %
     846qed.
     847
     848lemma get_arg_8_status_of_pseudo_status':
    792849  ∀cm.
    793850  ∀ps.
     
    850907  [1:
    851908    #_ >p normalize nodelta >p1 normalize nodelta
    852     @get_bit_addressable_sfr_status_of_pseudo_status %
     909    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
    853910  |2:
    854911    #_>p normalize nodelta >p1 normalize nodelta
    855     @lookup_low_internal_ram_of_pseudo_low_internal_ram
     912    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
    856913  |3,4:
    857     #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
     914    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    858915    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    859916    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
    860917    [1:
    861       >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     918      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
    862919    |2:
    863       >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     920      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
    864921    ]
    865922    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    866923  |5:
    867     #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
     924    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    868925    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    869926    >assoc_list_assm normalize nodelta %
    870927  |6,7,8,9:
    871     #_ /2/
     928    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
    872929  |10:
    873     #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …))
    874     >(get_8051_sfr_status_of_pseudo_status … (refl …))
    875     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     930    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     931    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     932    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    876933    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    877934    >acc_a_assm >p normalize nodelta //
    878935  |11:
    879     * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …))
    880     >(program_counter_status_of_pseudo_status … (refl …))
     936    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     937    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
    881938    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    882939    >sigma_assm >map_acc_a_assm >p normalize nodelta //
    883940  |12:
    884     #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
    885     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     941    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     942    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    886943    >external_ram_status_of_pseudo_status //
    887944  ]
     945qed.
     946
     947lemma get_arg_8_status_of_pseudo_status:
     948  ∀cm.
     949  ∀ps.
     950  ∀l.
     951  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
     952  ∀M. ∀sigma. ∀policy. ∀s', s''.
     953      (status_of_pseudo_status M cm ps sigma policy) = s' →
     954      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
     955      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     956      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     957      s' l addr = s''.
     958  #cm #ps #l #addr
     959  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
     960  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
     961  @relevant assumption
    888962qed.
    889963
     
    10171091  |2,4:
    10181092    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    1019     >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) #map_address_assm
     1093    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
    10201094    >map_address_assm %
    10211095  |3,5:
    10221096    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    10231097    whd in match status_of_pseudo_status; normalize nodelta
    1024     >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     1098    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    10251099    #map_address_assm >map_address_assm %
    10261100  ]
     
    11061180qed.
    11071181
    1108 lemma set_arg_1_status_of_pseudo_status:
     1182lemma set_arg_1_status_of_pseudo_status':
    11091183  ∀cm: pseudo_assembly_program.
    11101184  ∀ps: PreStatus pseudo_assembly_program cm.
    11111185  ∀addr: [[bit_addr; carry]].
    11121186  ∀b: Bit.
    1113     Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'.
     1187    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
     1188      b = b' →
    11141189      status_of_pseudo_status M cm ps sigma policy = s' →
    11151190      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
     
    11181193          (code_memory_of_pseudo_assembly_program cm sigma policy)
    11191194          s' addr b =
    1120         status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
     1195        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
    11211196  whd in match set_arg_1; normalize nodelta
    11221197  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
     
    11571232            [ ]
    11581233      ] (subaddressing_modein … a)) normalize nodelta
    1159   try @modulus_less_than #M #sigma #policy #s' #s_refl <s_refl
     1234  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
    11601235  [1:
    1161     #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
     1236    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    11621237    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11631238    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
    11641239  |2,3:
    1165     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     1240    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    11661241    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11671242    >p normalize nodelta >p1 normalize nodelta
    11681243    #map_bit_address_assm_1 #map_bit_address_assm_2
    11691244    [1:
    1170       >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …))
     1245      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
    11711246      >map_bit_address_assm_1
    11721247      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
    11731248    |2:
    11741249      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
    1175       >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     1250      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    11761251      >map_bit_address_assm_1
    11771252      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
     
    11791254    ]
    11801255  ]
     1256qed.
     1257
     1258lemma set_arg_1_status_of_pseudo_status:
     1259  ∀cm: pseudo_assembly_program.
     1260  ∀ps: PreStatus pseudo_assembly_program cm.
     1261  ∀addr: [[bit_addr; carry]].
     1262  ∀b: Bit.
     1263  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
     1264      b = b' →
     1265      status_of_pseudo_status M cm ps sigma policy = s' →
     1266      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
     1267      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
     1268        set_arg_1 (BitVectorTrie Byte 16)
     1269          (code_memory_of_pseudo_assembly_program cm sigma policy)
     1270          s' addr b =
     1271        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
     1272  #cm #ps #addr #b
     1273  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
     1274  @relevant
    11811275qed.
    11821276
     
    12011295  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
    12021296qed.
     1297
     1298lemma let_pair_in_status_of_pseudo_status:
     1299  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     1300    c = c' →
     1301    (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
     1302    let 〈left, right〉 ≝ c' in s' left right c' =
     1303    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     1304  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
     1305qed.
     1306
     1307lemma let_pair_as_in_status_of_pseudo_status:
     1308  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     1309  ∀c_refl: c = c'.
     1310    (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) →
     1311    let 〈left, right〉 as H ≝ c' in s' left right H c =
     1312    status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy.
     1313  [2: >H' assumption ]
     1314  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s'
     1315  #destruct_assm destruct(destruct_assm) normalize nodelta
     1316  #status_of_pseudo_status_assm >status_of_pseudo_status_assm //
     1317qed.
     1318
     1319lemma if_then_else_status_of_pseudo_status:
     1320  ∀M: internal_pseudo_address_map.
     1321  ∀cm: pseudo_assembly_program.
     1322  ∀sigma: Word → Word.
     1323  ∀policy: Word → bool.
     1324  ∀s, s', s'', s'''.
     1325  ∀t, t': bool.
     1326    t = t' →
     1327    status_of_pseudo_status M cm s sigma policy = s' →
     1328    status_of_pseudo_status M cm s'' sigma policy = s''' →
     1329      if t then
     1330        s'
     1331      else
     1332        s''' =
     1333      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
     1334  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
     1335  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
     1336qed.
Note: See TracChangeset for help on using the changeset viewer.