Changeset 2272 for src/ASM/Test.ma
- Timestamp:
- Jul 27, 2012, 5:53:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2258 r2272 96 96 λM, sigma, v. 97 97 match \snd M with 98 [ data ⇒ v 99 | address upper_lower word ⇒ 100 let mapped ≝ sigma word in 101 let 〈high, low〉 ≝ vsplit bool 8 8 mapped in 98 [ None ⇒ v 99 | Some upper_lower_addr ⇒ 100 let 〈upper_lower, addr〉 ≝ upper_lower_addr in 102 101 if eq_upper_lower upper_lower upper then 103 high 102 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in 103 high 104 104 else 105 low 105 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in 106 low 106 107 ]. 107 108 … … 113 114 λaddress: Byte. 114 115 λvalue: Byte. 115 match assoc_list_lookup ?? address (eq_bv …) (\fst M)with116 match lookup_from_internal_ram … address M with 116 117 [ None ⇒ value 117 118 | Some upper_lower_word ⇒ 118 119 let 〈upper_lower, word〉 ≝ upper_lower_word in 119 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in120 120 if eq_upper_lower upper_lower upper then 121 high 121 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in 122 high 122 123 else 123 low 124 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in 125 low 124 126 ]. 125 127 … … 216 218 qed. 217 219 220 lemma get_index_v_set_index_hit: 221 ∀A: Type[0]. 222 ∀n: nat. 223 ∀v: Vector A n. 224 ∀i: nat. 225 ∀e: A. 226 ∀i_lt_n_proof: i < n. 227 ∀i_lt_n_proof': i < n. 228 get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e. 229 #A #n #v elim v 230 [1: 231 #i #e #i_lt_n_proof 232 cases (lt_to_not_zero … i_lt_n_proof) 233 |2: 234 #n' #hd #tl #inductive_hypothesis #i #e 235 cases i 236 [1: 237 #i_lt_n_proof #i_lt_n_proof' % 238 |2: 239 #i' #i_lt_n_proof' #i_lt_n_proof'' 240 whd in ⊢ (??%?); @inductive_hypothesis 241 ] 242 ] 243 qed. 244 218 245 lemma set_index_status_of_pseudo_status: 219 246 ∀M, code_memory, sigma, policy, s, sfr, v, v'. … … 230 257 whd in match status_of_pseudo_status; normalize nodelta 231 258 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 232 inversion (\snd M) try ( #upper_lower #address) #sndM_refl normalize nodelta259 inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta 233 260 [1: 234 261 <sfr_neq_acc_a_assm cases sfr … … 240 267 % 241 268 |2: 269 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta 242 270 @pair_elim #high #low #high_low_refl normalize nodelta 243 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta 244 <sfr_neq_acc_a_assm cases sfr 271 whd in match set_8051_sfr; normalize nodelta 272 <sfr_neq_acc_a_assm 273 cases sfr in high_low_refl sfr_neq_acc_a_assm; 245 274 [18,37: 275 @pair_elim #high' #low' #high_low_refl' 276 #high_low_refl 246 277 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 247 278 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 248 >sndM_refl normalize nodelta >high_low_refl normalize nodelta279 >sndM_refl normalize nodelta 249 280 >eq_upper_lower_refl normalize nodelta 250 whd in match (set_8051_sfr ?????);251 281 [1: 282 #relevant >relevant 252 283 <set_index_set_index_overwrite in ⊢ (??%?); 253 <set_index_set_index_overwrite in ⊢ (???%); % 284 <set_index_set_index_overwrite in ⊢ (???%); 285 >get_index_v_set_index_hit in high_low_refl'; 286 #assm >assm in relevant; normalize nodelta * % 254 287 |2: 288 #relevant >relevant 255 289 <set_index_set_index_overwrite in ⊢ (??%?); 256 <set_index_set_index_overwrite in ⊢ (???%); % 290 <set_index_set_index_overwrite in ⊢ (???%); 291 >get_index_v_set_index_hit in high_low_refl'; 292 #assm >assm in relevant; normalize nodelta * % 257 293 ] 258 294 ] 259 295 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 260 whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize 261 @nmk #absurd destruct(absurd) 296 #relevant * >get_index_v_set_index_miss 297 try (% #absurd normalize in absurd; destruct(absurd)) 298 >relevant normalize nodelta 299 @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd) 262 300 ] 263 301 qed. 264 302 303 (* 265 304 lemma get_index_v_status_of_pseudo_status: 266 305 ∀M, code_memory, sigma, policy, s, s', sfr. … … 301 340 ] 302 341 qed. 342 *) 303 343 304 344 lemma set_8051_sfr_status_of_pseudo_status: … … 313 353 qed. 314 354 355 (* 315 356 lemma get_8051_sfr_status_of_pseudo_status: 316 357 ∀M, code_memory, sigma, policy, s, s', s'', sfr. … … 324 365 whd in match get_8051_sfr; normalize nodelta 325 366 @get_index_v_status_of_pseudo_status % 326 qed. 367 qed.*) 327 368 328 369 lemma get_8052_sfr_status_of_pseudo_status: … … 424 465 (code_memory_of_pseudo_assembly_program cm sigma policy) 425 466 s' 426 (low_internal_ram_of_pseudo_low_internal_ram M ram)467 (low_internal_ram_of_pseudo_low_internal_ram M sigma ram) 427 468 = status_of_pseudo_status M cm 428 469 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. … … 435 476 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → 436 477 insert Byte 7 addr v' 437 (low_internal_ram_of_pseudo_low_internal_ram M 478 (low_internal_ram_of_pseudo_low_internal_ram M sigma 438 479 (low_internal_ram pseudo_assembly_program cm s)) 439 =low_internal_ram_of_pseudo_low_internal_ram M 480 =low_internal_ram_of_pseudo_low_internal_ram M sigma 440 481 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 441 482 … … 447 488 (code_memory_of_pseudo_assembly_program cm sigma policy) 448 489 (status_of_pseudo_status M cm s sigma policy)) 449 = low_internal_ram_of_pseudo_low_internal_ram M 490 = low_internal_ram_of_pseudo_low_internal_ram M sigma 450 491 (insert Byte 7 addr v 451 492 (low_internal_ram pseudo_assembly_program cm s)). … … 458 499 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' → 459 500 insert Byte 7 addr v' 460 (high_internal_ram_of_pseudo_high_internal_ram M 501 (high_internal_ram_of_pseudo_high_internal_ram M sigma 461 502 (high_internal_ram pseudo_assembly_program cm s)) 462 =high_internal_ram_of_pseudo_high_internal_ram M 503 =high_internal_ram_of_pseudo_high_internal_ram M sigma 463 504 (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)). 464 505 … … 470 511 (code_memory_of_pseudo_assembly_program cm sigma policy) 471 512 (status_of_pseudo_status M cm s sigma policy)) 472 = high_internal_ram_of_pseudo_high_internal_ram M 513 = high_internal_ram_of_pseudo_high_internal_ram M sigma 473 514 (insert Byte 7 addr v 474 515 (high_internal_ram pseudo_assembly_program cm s)). … … 1374 1415 >get_index_v_set_index_miss [2,4: /2/] % 1375 1416 qed. 1417 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 1441 lemma get_arg_8_pseudo_addressing_mode_ok: 1442 ∀M: internal_pseudo_address_map. 1443 ∀cm: pseudo_assembly_program. 1444 ∀ps: PreStatus pseudo_assembly_program cm. 1445 ∀sigma: Word → Word. 1446 ∀policy: Word → bool. 1447 ∀addr1: [[registr; direct]]. 1448 assert_data pseudo_assembly_program M cm ps addr1 = true → 1449 get_arg_8 (BitVectorTrie Byte 16) 1450 (code_memory_of_pseudo_assembly_program cm sigma policy) 1451 (status_of_pseudo_status M cm ps sigma policy) true addr1 = 1452 get_arg_8 pseudo_assembly_program cm ps true addr1. 1453 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1454 #M #cm #ps #sigma #policy #addr1 1455 @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%); 1456 [1: 1457 whd in ⊢ (??%? → ??%?); 1458 whd in match bit_address_of_register; normalize nodelta 1459 @pair_elim #un #ln #un_ln_refl 1460 lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl 1461 @(pair_replace ?????????? un_ln_refl) 1462 [1: 1463 whd in match get_8051_sfr; normalize nodelta 1464 whd in match sfr_8051_index; normalize nodelta 1465 @eq_f <get_index_v_special_function_registers_8051_not_acc_a 1466 try % #absurd destruct(absurd) 1467 |2: 1468 #assembly_mode_ok_refl 1469 >low_internal_ram_of_pseudo_internal_ram_miss 1470 [1: 1471 % 1472 |2: 1473 cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta 1474 [1: 1475 #absurd destruct(absurd) 1476 |2: 1477 * normalize nodelta 1478 [1: 1479 |2: 1480 #_ #absurd destruct(absurd) 1481 ] 1482 #absurd try % @sym_eq assumption 1483 ] 1484 ] 1485 |2: 1486 #addressing_mode_ok_refl whd in ⊢ (??%?); 1487 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (* 1488 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 1489 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta 1490 [1: 1491 whd in ⊢ (??%%); normalize nodelta 1492 cases (eqb ??) normalize nodelta [1: % ] 1493 cases (eqb ??) normalize nodelta [1: % ] 1494 cases (eqb ??) normalize nodelta [1: % ] 1495 cases (eqb ??) normalize nodelta [1: % ] 1496 cases (eqb ??) normalize nodelta [1: 1497 @get_8051_sfr_status_of_pseudo_status 1498 #absurd destruct(absurd) 1499 ] 1500 cases (eqb ??) normalize nodelta [1: 1501 @get_8051_sfr_status_of_pseudo_status 1502 #absurd destruct(absurd) 1503 ] 1504 cases (eqb ??) normalize nodelta [1: 1505 @get_8051_sfr_status_of_pseudo_status 1506 #absurd destruct(absurd) 1507 ] 1508 cases (eqb ??) normalize nodelta [1: 1509 @get_8051_sfr_status_of_pseudo_status 1510 #absurd destruct(absurd) 1511 ] 1512 cases (eqb ??) normalize nodelta [1: 1513 @get_8051_sfr_status_of_pseudo_status 1514 #absurd destruct(absurd) 1515 ] 1516 cases (eqb ??) normalize nodelta [1: % ] 1517 cases (eqb ??) normalize nodelta [1: % ] 1518 cases (eqb ??) normalize nodelta [1: % ] 1519 cases (eqb ??) normalize nodelta [1: % ] 1520 cases (eqb ??) normalize nodelta [1: % ] 1521 cases (eqb ??) normalize nodelta [1: 1522 @get_8051_sfr_status_of_pseudo_status 1523 #absurd destruct(absurd) 1524 ] 1525 cases (eqb ??) normalize nodelta [1: 1526 @get_8051_sfr_status_of_pseudo_status 1527 #absurd destruct(absurd) 1528 ] 1529 cases (eqb ??) normalize nodelta [1: 1530 @get_8051_sfr_status_of_pseudo_status 1531 #absurd destruct(absurd) 1532 ] 1533 cases (eqb ??) normalize nodelta [1: 1534 @get_8051_sfr_status_of_pseudo_status 1535 #absurd destruct(absurd) 1536 ] 1537 cases (eqb ??) normalize nodelta [1: 1538 @get_8051_sfr_status_of_pseudo_status 1539 #absurd destruct(absurd) 1540 ] 1541 cases (eqb ??) normalize nodelta [1: 1542 @get_8051_sfr_status_of_pseudo_status 1543 #absurd destruct(absurd) 1544 ] 1545 cases (eqb ??) normalize nodelta [1: 1546 @get_8051_sfr_status_of_pseudo_status 1547 #absurd destruct(absurd) 1548 ] 1549 cases (eqb ??) normalize nodelta [1: 1550 @get_8051_sfr_status_of_pseudo_status 1551 #absurd destruct(absurd) 1552 ] 1553 cases (eqb ??) normalize nodelta [1: 1554 @get_8051_sfr_status_of_pseudo_status 1555 #absurd destruct(absurd) 1556 ] 1557 cases (eqb ??) normalize nodelta [1: 1558 @get_8051_sfr_status_of_pseudo_status 1559 #absurd destruct(absurd) 1560 ] 1561 inversion (eqb ??) #eqb_refl normalize nodelta [1: 1562 @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl 1563 whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl) 1564 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta 1565 #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_ 1566 #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) % 1567 ] 1568 cases (eqb ??) normalize nodelta [1: 1569 @get_8051_sfr_status_of_pseudo_status 1570 #absurd destruct(absurd) 1571 ] % 1572 |2: 1573 lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant 1574 whd in match status_of_pseudo_status; normalize nodelta 1575 >low_internal_ram_of_pseudo_internal_ram_miss try % 1576 cut(arg = false:::(three_bits@@nl)) 1577 [1: 1578 <get_index_v_refl 1579 cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits) 1580 [1: 1581 cut(ignore = [[get_index_v bool 4 nu 0 ?]]) 1582 [1: 1583 @le_S_S @le_O_n 1584 |2: 1585 cut(ignore = \fst (vsplit bool 1 3 nu)) 1586 [1: 1587 >ignore_three_bits_refl % 1588 |2: 1589 #ignore_refl >ignore_refl 1590 cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl 1591 >nu_refl % 1592 ] 1593 |3: 1594 #ignore_refl >ignore_refl in ignore_three_bits_refl; 1595 #relevant lapply (vsplit_ok ?????? (sym_eq … relevant)) 1596 #nu_refl <nu_refl % 1597 ] 1598 |2: 1599 #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl 1600 @sym_eq @vsplit_ok >nu_nl_refl % 1601 ] 1602 |2: 1603 #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant; 1604 normalize nodelta 1605 [1: 1606 cases (eq_bv ???) normalize #absurd destruct(absurd) 1607 |2: 1608 #_ % 1609 ] 1610 ] 1611 ] 1612 ] *) 1613 qed.
Note: See TracChangeset
for help on using the changeset viewer.