Changeset 2273 for src/ASM/Test.ma
- Timestamp:
- Jul 30, 2012, 12:46:19 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2272 r2273 301 301 qed. 302 302 303 (*304 303 lemma get_index_v_status_of_pseudo_status: 305 304 ∀M, code_memory, sigma, policy, s, s', sfr. … … 316 315 whd in match status_of_pseudo_status; normalize nodelta 317 316 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 318 inversion (\snd M) try ( #upper_lower #address) #sndM_refl normalize nodelta317 inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta 319 318 [1: 320 319 cases sfr … … 326 325 % 327 326 |2: 327 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta 328 328 @pair_elim #high #low #high_low_refl normalize nodelta 329 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta330 329 cases sfr 331 330 [18,37: … … 340 339 ] 341 340 qed. 342 *)343 341 344 342 lemma set_8051_sfr_status_of_pseudo_status: … … 350 348 (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy. 351 349 #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok 352 <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/ 353 qed. 354 355 (* 350 <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/ 351 qed. 352 353 (*lemma get_8051_sfr_status_of_pseudo_status: 354 ∀M. 355 ∀cm, ps, sigma, policy. 356 ∀sfr. 357 (sfr = SFR_ACC_A → \snd M = None …) → 358 get_8051_sfr (BitVectorTrie Byte 16) 359 (code_memory_of_pseudo_assembly_program cm sigma policy) 360 (status_of_pseudo_status M cm ps sigma policy) sfr = 361 get_8051_sfr pseudo_assembly_program cm ps sfr. 362 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant 363 [18: >relevant % ] 364 cases sndM try % * #address 365 whd in match get_8051_sfr; 366 whd in match status_of_pseudo_status; normalize nodelta 367 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address 368 cases (eq_upper_lower ??) normalize nodelta 369 @pair_elim #upper #lower #upper_lower_refl 370 @get_index_v_set_index_miss @nmk #relevant 371 normalize in relevant; destruct(relevant) 372 qed.*) 373 356 374 lemma get_8051_sfr_status_of_pseudo_status: 357 375 ∀M, code_memory, sigma, policy, s, s', s'', sfr. … … 365 383 whd in match get_8051_sfr; normalize nodelta 366 384 @get_index_v_status_of_pseudo_status % 367 qed. *)385 qed. 368 386 369 387 lemma get_8052_sfr_status_of_pseudo_status: … … 537 555 (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 538 556 lookup Byte 7 addr 539 (low_internal_ram_of_pseudo_low_internal_ram M 557 (low_internal_ram_of_pseudo_low_internal_ram M sigma 540 558 (low_internal_ram pseudo_assembly_program cm s)) (zero 8) 541 559 = s'. … … 549 567 (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 550 568 lookup Byte 7 addr 551 (high_internal_ram_of_pseudo_high_internal_ram M 569 (high_internal_ram_of_pseudo_high_internal_ram M sigma 552 570 (high_internal_ram pseudo_assembly_program cm s)) (zero 8) 553 571 = s'. … … 606 624 definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ 607 625 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr. 626 let 〈low,high,accA〉 ≝ M in 608 627 match addr with 609 628 [ INDIRECT i ⇒ 610 assoc_list_lookup ??611 ( false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M)= None …629 lookup_opt … 630 (bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None … 612 631 | EXT_INDIRECT e ⇒ 613 assoc_list_lookup ??614 ( false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M)= None …632 lookup_opt … 633 (bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None … 615 634 | ACC_DPTR ⇒ 616 635 (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer … … 697 716 set_low_internal_ram ?? s memory 698 717 ] 718 699 719 | INDIRECT i ⇒ 700 720 λindirect: True. … … 734 754 [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status 735 755 | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 736 |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; 756 |3,4: cases M * -M #low #high #accA normalize nodelta 757 #EQ1 #EQ2 change with (get_register ????) in match register in p; 737 758 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 738 759 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 760 whd in match (lookup_from_internal_ram ??); 739 761 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta 740 762 [ >(insert_high_internal_ram_status_of_pseudo_status … v) 741 763 | >(insert_low_internal_ram_status_of_pseudo_status … v) ] 742 764 // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 743 |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 765 |5: cases M * -M #low #high #accA normalize nodelta 766 #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 744 767 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 768 whd in match lookup_from_internal_ram; normalize nodelta 745 769 >EQ1 normalize nodelta 746 770 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status … … 957 981 #_>p normalize nodelta >p1 normalize nodelta 958 982 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) % 959 |3,4: 983 |3,4: cases M -M * #low #high #accA 960 984 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 961 985 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 986 whd in match lookup_from_internal_ram; normalize nodelta 962 987 >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta 963 988 [1: 964 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)989 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma) 965 990 |2: 966 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)991 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma) 967 992 ] 968 993 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 969 |5: 994 |5: cases M -M * #low #high #accA 970 995 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 971 996 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 997 whd in match lookup_from_internal_ram; normalize nodelta 972 998 >assoc_list_assm normalize nodelta % 973 999 |6,7,8,9: 974 1000 #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/ 975 |10: 1001 |10: cases M -M * #low #high #accA 976 1002 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 977 1003 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) … … 979 1005 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 980 1006 >acc_a_assm >p normalize nodelta // 981 |11: 1007 |11: cases M -M * #low #high #accA 982 1008 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 983 1009 >(program_counter_status_of_pseudo_status … (refl …) (refl …)) … … 1048 1074 match head' … bit_1 with 1049 1075 [ true ⇒ 1050 let address ≝ nat_of_bitvector … seven_bits in 1051 let d ≝ address ÷ 8 in 1052 let m ≝ address mod 8 in 1053 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1076 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1077 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1054 1078 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1055 1079 | false ⇒ 1056 let address ≝ nat_of_bitvector …seven_bits in1057 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1080 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1081 let address' ≝ [[true; false; false]]@@four_bits in 1058 1082 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1059 1083 map_internal_ram_address_using_pseudo_address_map M sigma 1060 1084 (false:::address') t = t 1061 1085 ] … … 1064 1088 match head' … bit_1 with 1065 1089 [ true ⇒ 1066 let address ≝ nat_of_bitvector … seven_bits in 1067 let d ≝ address ÷ 8 in 1068 let m ≝ address mod 8 in 1069 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1090 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1091 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1070 1092 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1071 1093 | false ⇒ 1072 let address ≝ nat_of_bitvector …seven_bits in1073 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1094 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1095 let address' ≝ [[true; false; false]]@@four_bits in 1074 1096 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1075 1097 map_internal_ram_address_using_pseudo_address_map M sigma 1076 1098 (false:::address') t = t 1077 1099 ] … … 1100 1122 match head' … bit_1 with 1101 1123 [ true ⇒ 1102 let address ≝ nat_of_bitvector … seven_bits in 1103 let d ≝ address ÷ 8 in 1104 let m ≝ address mod 8 in 1105 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1124 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1125 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1106 1126 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1107 get_index_v … sfr m?1127 get_index_v … sfr (nat_of_bitvector … three_bits) ? 1108 1128 | false ⇒ 1109 let address ≝ nat_of_bitvector …seven_bits in1110 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1129 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1130 let address' ≝ [[true; false; false]]@@four_bits in 1111 1131 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1112 get_index_v … t ( modulus address 8) ?1132 get_index_v … t (nat_of_bitvector … three_bits) ? 1113 1133 ] 1114 1134 | N_BIT_ADDR n ⇒ … … 1117 1137 match head' … bit_1 with 1118 1138 [ true ⇒ 1119 let address ≝ nat_of_bitvector … seven_bits in 1120 let d ≝ address ÷ 8 in 1121 let m ≝ address mod 8 in 1122 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1139 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1140 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1123 1141 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1124 ¬(get_index_v … sfr m?)1142 ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?) 1125 1143 | false ⇒ 1126 let address ≝ nat_of_bitvector …seven_bits in1127 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1144 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1145 let address' ≝ [[true; false; false]]@@four_bits in 1128 1146 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1129 ¬(get_index_v … t ( modulus address 8) ?)1147 ¬(get_index_v … t (nat_of_bitvector … three_bits) ?) 1130 1148 ] 1131 1149 | CARRY ⇒ λcarry: True. get_cy_flag ?? s … … 1133 1151 match other in False with [ ] 1134 1152 ] (subaddressing_modein … a)) normalize nodelta 1135 try @modulus_less_than1153 [4,5,8,9: //] 1136 1154 #M #sigma #policy #s' #s_refl <s_refl 1137 1155 [1: 1138 1156 #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) % 1139 1157 |2,4: 1140 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1158 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2 1159 normalize nodelta 1141 1160 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm 1142 1161 >map_address_assm % 1143 1162 |3,5: 1144 1163 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1145 whd in match status_of_pseudo_status; normalize nodelta 1164 whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta 1146 1165 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1147 1166 #map_address_assm >map_address_assm % … … 1167 1186 qed. 1168 1187 1188 (*CSC: daemon 1169 1189 definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ 1170 1190 λM: internal_pseudo_address_map. … … 1321 1341 cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant 1322 1342 @relevant 1323 qed. 1343 qed.*) 1324 1344 1325 1345 lemma clock_status_of_pseudo_status: … … 1344 1364 qed. 1345 1365 1366 (*CSC: daemon 1346 1367 lemma set_flags_status_of_pseudo_status: 1347 1368 ∀M. … … 1367 1388 [1: 1368 1389 normalize nodelta % 1369 |2: 1370 * #address normalize nodelta 1390 |2: ** #address normalize nodelta 1371 1391 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1372 1392 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta … … 1374 1394 cases daemon 1375 1395 ] 1376 qed. 1396 qed.*) 1377 1397 1378 1398 lemma get_ac_flag_status_of_pseudo_status: … … 1389 1409 whd in match status_of_pseudo_status; normalize nodelta 1390 1410 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1391 cases (\snd M) try % 1392 * normalize nodelta#address1411 cases (\snd M) try % normalize nodelta ** normalize nodelta 1412 #address 1393 1413 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1394 1414 whd in match sfr_8051_index; normalize nodelta … … 1410 1430 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1411 1431 cases (\snd M) try % 1412 * normalize nodelta #address1432 ** normalize nodelta #address 1413 1433 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1414 1434 whd in match sfr_8051_index; normalize nodelta … … 1416 1436 qed. 1417 1437 1418 lemma get_8051_sfr_status_of_pseudo_status: 1419 ∀M. 1420 ∀cm, ps, sigma, policy. 1421 ∀sfr. 1422 (sfr = SFR_ACC_A → \snd M = None …) → 1423 get_8051_sfr (BitVectorTrie Byte 16) 1424 (code_memory_of_pseudo_assembly_program cm sigma policy) 1425 (status_of_pseudo_status M cm ps sigma policy) sfr = 1426 get_8051_sfr pseudo_assembly_program cm ps sfr. 1427 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant 1428 [18: 1429 >relevant % 1430 ] 1431 cases sndM try % * #address 1432 whd in match get_8051_sfr; 1433 whd in match status_of_pseudo_status; normalize nodelta 1434 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address 1435 cases (eq_upper_lower ??) normalize nodelta 1436 @pair_elim #upper #lower #upper_lower_refl 1437 @get_index_v_set_index_miss @nmk #relevant 1438 normalize in relevant; destruct(relevant) 1439 qed. 1440 1438 (*CSC: useless? 1441 1439 lemma get_arg_8_pseudo_addressing_mode_ok: 1442 1440 ∀M: internal_pseudo_address_map. … … 1485 1483 |2: 1486 1484 #addressing_mode_ok_refl whd in ⊢ (??%?); 1487 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*1485 @pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX cases daemon (* 1488 1486 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 1489 1487 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta … … 1610 1608 ] 1611 1609 ] 1612 ] *) 1613 qed. 1610 ] 1611 qed.*)*) 1612 1613 lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map: 1614 ∀M, cm, ps, sigma, x. 1615 ∀addr1: [[acc_a]]. 1616 assert_data pseudo_assembly_program M cm ps addr1=true → 1617 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x. 1618 #M #cm #ps #sigma #x #addr1 1619 @(subaddressing_mode_elim … addr1) 1620 whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//] 1621 * #upper_lower #address normalize nodelta #absurd destruct(absurd) 1622 qed. 1623 1624 lemma addressing_mode_ok_to_snd_M_data: 1625 ∀M, cm, ps. 1626 ∀addr: [[acc_a]]. 1627 assert_data pseudo_assembly_program M cm ps addr = true → 1628 \snd M = None …. 1629 #M #cm #ps #addr 1630 @(subaddressing_mode_elim … addr) 1631 whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta 1632 [ #_ % 1633 | #addr #abs destruct(abs) ] 1634 qed. 1635 1636 (*(*CSC: move elsewhere*) 1637 lemma assoc_list_exists_true_to_assoc_list_lookup_Some: 1638 ∀A, B: Type[0]. 1639 ∀e: A. 1640 ∀the_list: list (A × B). 1641 ∀eq_f: A → A → bool. 1642 assoc_list_exists A B e eq_f the_list = true → 1643 ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'. 1644 #A #B #e #the_list #eq_f elim the_list 1645 [1: 1646 whd in ⊢ (??%? → ?); #absurd destruct(absurd) 1647 |2: 1648 #hd #tl #inductive_hypothesis 1649 whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????); 1650 cases (eq_f (\fst hd) e) normalize nodelta 1651 [1: 1652 #_ %{(\snd hd)} % 1653 |2: 1654 @inductive_hypothesis 1655 ] 1656 ] 1657 qed. 1658 1659 (*CSC: move elsewhere*) 1660 lemma assoc_list_exists_false_to_assoc_list_lookup_None: 1661 ∀A, B: Type[0]. 1662 ∀e, e': A. 1663 ∀the_list, the_list': list (A × B). 1664 ∀eq_f: A → A → bool. 1665 e = e' → 1666 the_list = the_list' → 1667 assoc_list_exists A B e eq_f the_list = false → 1668 assoc_list_lookup A B e' eq_f the_list' = None …. 1669 #A #B #e #e' #the_list elim the_list 1670 [1: 1671 #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ % 1672 |2: 1673 #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl 1674 whd in ⊢ (??%? → ??%?); <e_refl 1675 cases (eq_f (\fst hd) e) normalize nodelta 1676 [1: 1677 #absurd destruct(absurd) 1678 |2: 1679 >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption 1680 ] 1681 ] 1682 qed.*) 1683 1684 lemma sfr_psw_eq_to_bit_address_of_register_eq: 1685 ∀A: Type[0]. 1686 ∀code_memory: A. 1687 ∀status, status', register_address. 1688 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1689 bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address. 1690 #A #code_memory #status #status' #register_address #sfr_psw_refl 1691 whd in match bit_address_of_register; normalize nodelta 1692 <sfr_psw_refl % 1693 qed. 1694 1695 lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq: 1696 ∀A: Type[0]. 1697 ∀code_memory: A. 1698 ∀status, status', register_address. 1699 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1700 low_internal_ram A code_memory status = low_internal_ram A code_memory status' → 1701 get_register A code_memory status register_address = get_register A code_memory status' register_address. 1702 #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl 1703 whd in match get_register; normalize nodelta <low_internal_ram_refl 1704 >(sfr_psw_eq_to_bit_address_of_register_eq … status status') // 1705 qed. 1706 1707 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: 1708 ∀M, cm, status, status', sigma. 1709 ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 1710 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1711 assert_data pseudo_assembly_program M cm status addr1 = true → 1712 map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1. 1713 * * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl 1714 @(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w 1715 whd in ⊢ (??%? → %); whd in match (data_or_address ?????); 1716 whd in match exists; normalize nodelta 1717 <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption 1718 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) 1719 qed. 1720 1721 lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map: 1722 ∀M. 1723 ∀sigma. 1724 ∀sfr8051. 1725 ∀b. 1726 sfr8051 ≠ SFR_ACC_A → 1727 map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b. 1728 #M #sigma * #b 1729 [18: 1730 #relevant cases (absurd … (refl ??) relevant) 1731 ] 1732 #_ % 1733 qed. 1734 1735 lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map: 1736 ∀M. 1737 ∀sigma: Word → Word. 1738 ∀w: BitVector 8. 1739 ∀b. 1740 w ≠ bitvector_of_nat … 224 → 1741 map_address_Byte_using_internal_pseudo_address_map M sigma w b = b. 1742 #M #sigma #w #b #w_neq_assm 1743 whd in ⊢ (??%?); inversion (sfr_of_Byte ?) 1744 [1: 1745 #sfr_of_Byte_refl % 1746 |2: 1747 * #sfr8051 #sfr_of_Byte_refl normalize nodelta try % 1748 @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map % 1749 #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl 1750 @(absurd ?? w_neq_assm) 1751 lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma 1752 whd in match sfr_of_Byte; normalize nodelta 1753 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1754 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1755 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1756 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1757 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1758 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1759 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1760 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1761 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1762 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1763 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1764 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1765 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1766 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1767 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1768 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1769 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1770 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1771 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1772 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1773 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1774 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1775 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1776 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1777 @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ] 1778 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1779 #absurd destruct(absurd) 1780 qed. 1781 1782 (*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map: 1783 ∀M, sigma, w, b. 1784 assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst M) = false → 1785 map_internal_ram_address_using_pseudo_address_map M sigma w b = b. 1786 #M #sigma #w #b #assoc_list_exists_assm 1787 whd in ⊢ (??%?); 1788 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) % 1789 qed.*) 1790 1791 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2: 1792 ∀M', cm. 1793 ∀sigma, status, status', b, b'. 1794 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 1795 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1796 low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' → 1797 b = b' → 1798 assert_data pseudo_assembly_program M' cm status addr1 = true → 1799 map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'. 1800 #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl 1801 @(subaddressing_mode_elim … addr1) 1802 [1: 1803 whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high * 1804 [1: 1805 normalize nodelta #_ % 1806 |2: 1807 * #upper_lower #address normalize nodelta #absurd destruct(absurd) 1808 ] 1809 |2: cases M' -M' * #low #high #accA 1810 #w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??); 1811 <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl) 1812 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) 1813 |4: cases M' -M' * #low #high #accA 1814 #w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram; 1815 whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta 1816 whd in match get_register; normalize nodelta 1817 <(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl) 1818 cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)] 1819 <low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta 1820 cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta 1821 #x try % #abs destruct(abs) 1822 |3: cases M' -M' * #low #high #accA 1823 #w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta 1824 @vsplit_elim #hd #tl #w_refl normalize nodelta 1825 lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd)) 1826 cases (head' bool ??) normalize nodelta 1827 [2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????); 1828 whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????); 1829 normalize nodelta // #x #abs destruct(abs) ] #EQhd 1830 >w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta 1831 [1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_ 1832 normalize in eq_bv_refl; >eq_bv_refl % 1833 |2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ] 1834 |5,6,7,8: 1835 #w try #w' % 1836 ] 1837 qed. 1838 1839 (*CSC: move elsewhere*) 1840 lemma bv_append_eq_to_eq: 1841 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m. 1842 v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4. 1843 #A #n #v1 elim v1 1844 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %% 1845 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2 1846 #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ] 1847 qed. 1848 1849 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get: 1850 ∀M: internal_pseudo_address_map. 1851 ∀cm: pseudo_assembly_program. 1852 ∀s: PreStatus pseudo_assembly_program cm. 1853 ∀sigma: Word → Word. 1854 ∀addr: [[bit_addr]]. (* XXX: expand as needed *) 1855 ∀f: bool. 1856 assert_data pseudo_assembly_program M cm s addr = true → 1857 map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f. 1858 ** #low #high #accA #cm #s #sigma #addr #f 1859 @(subaddressing_mode_elim … addr) #w 1860 whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta 1861 @vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1862 @vsplit_elim #four #three #four_three_refl normalize nodelta 1863 cases (head' bool ??) normalize nodelta 1864 [1: @eq_bv_elim normalize nodelta 1865 [1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour % 1866 |2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map 1867 try % normalize #EQ @(absurd ?? NEQ) 1868 cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1 1869 cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ] 1870 |2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 1871 whd in match lookup_from_internal_ram; normalize nodelta 1872 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ] 1873 qed. 1874 1875 (* 1876 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1: 1877 ∀M: internal_pseudo_address_map. 1878 ∀cm: pseudo_assembly_program. 1879 ∀s, s': PreStatus pseudo_assembly_program cm. 1880 ∀sigma: Word → Word. 1881 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) 1882 ∀f: bool. 1883 s = s' → 1884 addressing_mode_ok pseudo_assembly_program M cm s addr = true → 1885 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f. 1886 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl 1887 @(subaddressing_mode_elim … addr) [1: #w ] 1888 whd in ⊢ (??%? → %); [2: #_ @I ] 1889 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1890 cases (head' bool ??) normalize nodelta 1891 [1: 1892 #eq_accumulator_assm whd in ⊢ (??%?); 1893 cases (sfr_of_Byte ?) try % * * try % normalize nodelta 1894 whd in ⊢ (??%?); 1895 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % 1896 |2: 1897 #assoc_list_exists_assm whd in ⊢ (??%?); 1898 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm 1899 whd in assoc_list_exists_assm:(???%); 1900 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % 1901 ] 1902 qed. 1903 1904 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2: 1905 ∀M: internal_pseudo_address_map. 1906 ∀cm: pseudo_assembly_program. 1907 ∀s, s': PreStatus pseudo_assembly_program cm. 1908 ∀sigma: Word → Word. 1909 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) 1910 ∀f: bool. 1911 s = s' → 1912 addressing_mode_ok pseudo_assembly_program M cm s addr = true → 1913 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f. 1914 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl 1915 @(subaddressing_mode_elim … addr) [1: #w ] 1916 whd in ⊢ (??%? → %); [2: #_ @I ] 1917 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1918 cases (head' bool ??) normalize nodelta 1919 [1: 1920 #eq_accumulator_assm whd in ⊢ (??%?); 1921 cases (sfr_of_Byte ?) try % * * try % normalize nodelta 1922 whd in ⊢ (??%?); 1923 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % 1924 |2: 1925 #assoc_list_exists_assm whd in ⊢ (??%?); 1926 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm 1927 whd in assoc_list_exists_assm:(???%); 1928 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % 1929 ] 1930 qed.*) 1931 1932 (* 1933 axiom insert_low_internal_ram_of_pseudo_low_internal_ram': 1934 ∀M, M', sigma,cm,s,addr,v,v'. 1935 (∀addr'. 1936 ((false:::addr) = addr' → 1937 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = 1938 map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧ 1939 ((false:::addr) ≠ addr' → 1940 let 〈callM, accM〉 ≝ M in 1941 let 〈callM', accM'〉 ≝ M' in 1942 accM = accM' ∧ 1943 assoc_list_lookup … addr' (eq_bv 8) … callM = 1944 assoc_list_lookup … addr' (eq_bv 8) … callM')) → 1945 insert Byte 7 addr v' 1946 (low_internal_ram_of_pseudo_low_internal_ram M' 1947 (low_internal_ram pseudo_assembly_program cm s)) = 1948 low_internal_ram_of_pseudo_low_internal_ram M 1949 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 1950 *) 1951 1952 (* 1953 lemma write_at_stack_pointer_status_of_pseudo_status: 1954 ∀M, M'. 1955 ∀cm. 1956 ∀sigma. 1957 ∀policy. 1958 ∀s, s'. 1959 ∀new_b, new_b'. 1960 map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' → 1961 status_of_pseudo_status M cm s sigma policy = s' → 1962 write_at_stack_pointer ?? s' new_b' = 1963 status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy. 1964 #M #M' #cm #sigma #policy #s #s' #new_b #new_b' 1965 #new_b_refl #s_refl <new_b_refl <s_refl 1966 whd in match write_at_stack_pointer; normalize nodelta 1967 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 1968 @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl)) 1969 [1: 1970 @eq_f 1971 whd in match get_8051_sfr; normalize nodelta 1972 whd in match sfr_8051_index; normalize nodelta 1973 whd in match status_of_pseudo_status; normalize nodelta 1974 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1975 cases (\snd M) [2: * #address ] normalize nodelta 1976 [1,2: 1977 cases (vsplit bool ???) #high #low normalize nodelta 1978 whd in match sfr_8051_index; normalize nodelta 1979 >get_index_v_set_index_miss % 1980 #absurd destruct(absurd) 1981 |3: 1982 % 1983 ] 1984 |2: 1985 @if_then_else_status_of_pseudo_status try % 1986 [2: 1987 @sym_eq <set_low_internal_ram_status_of_pseudo_status 1988 [1: 1989 @eq_f2 1990 [2: 1991 @insert_low_internal_ram_of_pseudo_low_internal_ram' 1992 @sym_eq 1993 [2: 1994 <set_low_internal_ram_status_of_pseudo_status 1995 [1: 1996 @eq_f2 1997 [2: 1998 @sym_eq 1999 >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b') 2000 [2: 2001 >new_b_refl 2002 ] 2003 ] 2004 qed.*)
Note: See TracChangeset
for help on using the changeset viewer.