- Timestamp:
- Jul 27, 2012, 5:53:25 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2256 r2272 335 335 qed. 336 336 337 inductive accumulator_address_map_entry: Type[0] ≝ 338 | data: accumulator_address_map_entry 339 | address: upper_lower → Word → accumulator_address_map_entry. 337 (* XXX: if upper then the byte in the entry is the least significant byte of the address and 338 the byte in the status is the most significant, otherwise if lower then the 339 other way around 340 *) 341 definition address_entry ≝ upper_lower × Byte. 340 342 341 343 definition eq_accumulator_address_map_entry: 342 accumulator_address_map_entry → accumulator_address_map_entry → bool ≝343 λleft : accumulator_address_map_entry.344 λright : accumulator_address_map_entry.344 option address_entry → option address_entry → bool ≝ 345 λleft. 346 λright. 345 347 match left with 346 [ data⇒348 [ None ⇒ 347 349 match right with 348 [ data⇒ true350 [ None ⇒ true 349 351 | _ ⇒ false 350 352 ] 351 | address upper_lower word ⇒ 353 | Some upper_lower_addr ⇒ 354 let 〈upper_lower, addr〉 ≝ upper_lower_addr in 352 355 match right with 353 [ address upper_lower' word' ⇒ 354 eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word' 356 [ Some upper_lower_addr' ⇒ 357 let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in 358 eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr' 355 359 | _ ⇒ false 356 360 ] … … 358 362 359 363 lemma eq_accumulator_address_map_entry_true_to_eq: 360 ∀left: accumulator_address_map_entry.361 ∀right: accumulator_address_map_entry.364 ∀left: option address_entry. 365 ∀right: option address_entry. 362 366 eq_accumulator_address_map_entry left right = true → left = right. 363 367 #left #right cases left cases right … … 365 369 #_ % 366 370 |2,3: 367 #upper_lower#word normalize #absurd destruct(absurd)371 * * #word normalize #absurd destruct(absurd) 368 372 |4: 369 #upper_lower #word #upper_lower' #word' normalize 370 cases upper_lower' normalize nodelta 371 cases upper_lower normalize 373 * * #word * * #word' 372 374 [2,3: 373 #absurd destruct(absurd)375 #absurd normalize in absurd; destruct(absurd) 374 376 ] 375 change with (eq_bv 16 ?? = true → ?) 376 #relevant lapply (eq_bv_eq … relevant) 377 #word_refl >word_refl % 377 normalize change with (eq_bv 8 ?? = true → ?) 378 #relevant >(eq_bv_eq … relevant) % 378 379 ] 379 380 qed. … … 403 404 404 405 lemma eq_accumulator_address_map_entry_false_to_neq: 405 ∀left: accumulator_address_map_entry.406 ∀right: accumulator_address_map_entry.406 ∀left: option address_entry. 407 ∀right: option address_entry. 407 408 eq_accumulator_address_map_entry left right = false → left ≠ right. 408 409 #left #right cases left cases right … … 410 411 normalize #absurd destruct(absurd) 411 412 |2,3: 412 #upper_lower #word normalize #_ 413 @nmk #absurd destruct(absurd) 413 * * #word normalize #_ % #absurd destruct(absurd) 414 414 |4: 415 #upper_lower #word #upper_lower' #word' normalize 416 cases upper_lower' normalize nodelta 417 cases upper_lower normalize nodelta 415 * * #word * * #word' normalize 418 416 [2,3: 419 #_ @nmk#absurd destruct(absurd)417 #_ % #absurd destruct(absurd) 420 418 ] 421 419 change with (eq_bv ??? = false → ?) 422 #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)423 #word_neq_assm @nmk#address_eq_assm cases word_neq_assm420 #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm) 421 #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm 424 422 #word_eq_assm @word_eq_assm destruct(address_eq_assm) % 425 423 ] 426 qed. 424 qed. 427 425 428 426 (* XXX: changed this type. Bool specifies whether byte is first or second … … 431 429 A. 432 430 *) 433 definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry. 431 definition internal_pseudo_address_map ≝ 432 (* low, high, acc *) 433 (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry). 434 434 435 435 include alias "ASM/BitVectorTrie.ma". … … 437 437 include "common/AssocList.ma". 438 438 439 axiom low_internal_ram_of_pseudo_low_internal_ram: 440 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 441 442 axiom high_internal_ram_of_pseudo_high_internal_ram: 443 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 444 439 axiom bvt_map2: 440 ∀A, B, C: Type[0]. 441 ∀n: nat. 442 ∀bvt_1: BitVectorTrie A n. 443 ∀bvt_2: BitVectorTrie B n. 444 ∀f: ∀a: option A. ∀b: option B. option C. 445 BitVectorTrie C n. 446 447 axiom is_in_domain: 448 ∀A: Type[0]. 449 ∀n: nat. 450 ∀bvt: BitVectorTrie A n. 451 ∀b: BitVector n. 452 Prop. 453 454 axiom bvt_map2_function_extensionality: 455 ∀A, B, C: Type[0]. 456 ∀n: nat. 457 ∀bvt_1: BitVectorTrie A n. 458 ∀bvt_2, bvt_2': BitVectorTrie B n. 459 ∀f: ∀a: option A. ∀b: option B. option C. 460 (∀addr. 461 is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr → 462 f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) → 463 bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f. 464 465 definition internal_ram_of_pseudo_internal_ram: 466 ∀sigma: Word → Word. 467 ∀ram: BitVectorTrie Byte 7. 468 ∀map: BitVectorTrie address_entry 7. 469 BitVectorTrie Byte 7 ≝ 470 λsigma, ram, map. 471 bvt_map2 ??? ? ram map (λv. λul_addr. 472 match 473 match ul_addr with 474 [ None ⇒ v 475 | Some ul_addr' ⇒ 476 let 〈ul, addr〉 ≝ ul_addr' in 477 let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in 478 match ul with 479 [ upper ⇒ 480 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in 481 Some … high 482 | lower ⇒ 483 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in 484 Some … low 485 ] 486 ] with 487 [ None ⇒ None … 488 | Some v ⇒ 489 if eq_bv … v (zero …) then 490 None … 491 else 492 Some … v 493 ]). 494 495 definition low_internal_ram_of_pseudo_low_internal_ram: 496 ∀M: internal_pseudo_address_map. 497 ∀sigma: Word → Word. 498 ∀ram: BitVectorTrie Byte 7. 499 BitVectorTrie Byte 7 ≝ 500 λM, sigma, ram. 501 let 〈low, high, accA〉 ≝ M in 502 internal_ram_of_pseudo_internal_ram sigma ram low. 503 504 definition high_internal_ram_of_pseudo_high_internal_ram: 505 ∀M: internal_pseudo_address_map. 506 ∀sigma: Word → Word. 507 ∀ram: BitVectorTrie Byte 7. 508 BitVectorTrie Byte 7 ≝ 509 λM, sigma, ram. 510 let 〈low, high, accA〉 ≝ M in 511 internal_ram_of_pseudo_internal_ram sigma ram high. 512 513 (* 445 514 axiom low_internal_ram_of_pseudo_internal_ram_hit: 446 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.447 assoc_list_lookup?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 →448 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in515 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7. 516 lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 → 517 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in 449 518 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in 450 519 let bl ≝ lookup ? 7 addr ram (zero 8) in 451 520 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in 452 let 〈plower, phigher〉 ≝ vsplit ? 8 8 ( \fst (sigma points_to)) in521 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in 453 522 if eq_upper_lower upper_lower upper then 454 523 (pbl = higher) ∧ (bl = phigher) 455 524 else 456 525 (pbl = lower) ∧ (bl = plower). 526 *) 457 527 458 528 (* changed from add to sub *) 459 529 axiom low_internal_ram_of_pseudo_internal_ram_miss: 460 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 461 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 462 assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false → 463 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?). 464 465 definition addressing_mode_ok ≝ 530 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 531 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in 532 lookup_opt … addr (\fst (\fst M)) = None … → 533 lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?). 534 535 definition exists: 536 ∀A: Type[0]. 537 ∀n: nat. 538 ∀v: BitVector n. 539 ∀bvt: BitVectorTrie A n. 540 bool ≝ 541 λA, n, v, bvt. 542 match lookup_opt … v bvt with 543 [ None ⇒ false 544 | _ ⇒ true 545 ]. 546 547 definition data_or_address ≝ 466 548 λT. 467 549 λM: internal_pseudo_address_map. … … 469 551 λs: PreStatus T cm. 470 552 λaddr: addressing_mode. 471 match addr with 553 let 〈low, high, accA〉 ≝ M in 554 match addr return λx. option (option address_entry) with 472 555 [ DIRECT d ⇒ 473 if eq_bv … d (bitvector_of_nat … 224) then 474 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data 475 else 476 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 556 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 557 match head' … hd with 558 [ true ⇒ 559 if eq_bv … d (bitvector_of_nat … 224) then 560 Some … accA 561 else 562 Some … (None …) 563 | false ⇒ Some … (lookup_opt … seven_bits low) 564 ] 477 565 | INDIRECT i ⇒ 478 566 let d ≝ get_register … s [[false;false;i]] in 479 567 let address ≝ bit_address_of_register … s [[false;false;i]] in 480 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧ 481 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 568 if ¬exists … address low then 569 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 570 if head' … 0 bit_one then 571 Some … (lookup_opt … seven_bits high) 572 else 573 Some … (lookup_opt … seven_bits low) 574 else 575 None ? 482 576 | EXT_INDIRECT e ⇒ 483 577 let address ≝ bit_address_of_register … s [[false;false;e]] in 484 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 578 if ¬exists … address low then 579 Some … (None …) 580 else 581 None ? 485 582 | REGISTER r ⇒ 486 583 let address ≝ bit_address_of_register … s r in 487 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 488 | ACC_A ⇒ 489 match \snd M with 490 [ data ⇒ true 491 | _ ⇒ false 492 ] 493 | ACC_B ⇒ true 494 | DPTR ⇒ true 495 | DATA _ ⇒ true 496 | DATA16 _ ⇒ true 497 | ACC_DPTR ⇒ true 498 | ACC_PC ⇒ true 499 | EXT_INDIRECT_DPTR ⇒ true 500 | INDIRECT_DPTR ⇒ true 501 | CARRY ⇒ true 584 Some … (lookup_opt … address low) 585 | ACC_A ⇒ Some … accA 586 | ACC_B ⇒ Some … (None …) 587 | DPTR ⇒ Some … (None …) 588 | DATA _ ⇒ Some … (None …) 589 | DATA16 _ ⇒ Some … (None …) 590 | ACC_DPTR ⇒ Some … (None …) 591 | ACC_PC ⇒ Some … (None …) 592 | EXT_INDIRECT_DPTR ⇒ Some … (None …) 593 | INDIRECT_DPTR ⇒ Some … (None …) 594 | CARRY ⇒ Some … (None …) 502 595 | BIT_ADDR b ⇒ 503 596 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in 597 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 504 598 if head' bool 0 bit_one then 505 eq_accumulator_address_map_entry (\snd M) data 599 if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *) 600 Some … accA 601 else 602 Some … (None …) 506 603 else 507 let address ≝ nat_of_bitvector 7 seven_bits in 508 let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in 509 ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M) 510 | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *) 511 | RELATIVE _ ⇒ true 512 | ADDR11 _ ⇒ true 513 | ADDR16 _ ⇒ true 604 let address' ≝ [[true; false; false]]@@four_bits in 605 Some … (lookup_opt … address' low) 606 | N_BIT_ADDR b ⇒ 607 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in 608 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 609 if head' bool 0 bit_one then 610 if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *) 611 Some … accA 612 else 613 Some … (None …) 614 else 615 let address' ≝ [[true; false; false]]@@four_bits in 616 Some … (lookup_opt … address' low) 617 | RELATIVE _ ⇒ Some … (None …) 618 | ADDR11 _ ⇒ Some … (None …) 619 | ADDR16 _ ⇒ Some … (None …) 514 620 ]. 621 622 definition assert_data ≝ 623 λT. 624 λM: internal_pseudo_address_map. 625 λcm. 626 λs: PreStatus T cm. 627 λaddr: addressing_mode. 628 match data_or_address T M cm s addr with 629 [ None ⇒ false 630 | Some s ⇒ 631 match s with 632 [ None ⇒ true 633 | _ ⇒ false 634 ] 635 ]. 636 637 definition insert_into_internal_ram: 638 ∀addr: Byte. 639 ∀v: address_entry. 640 ∀M: internal_pseudo_address_map. 641 internal_pseudo_address_map ≝ 642 λaddr, v, M. 643 let 〈low, high, accA〉 ≝ M in 644 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 645 if head' … bit_one then 646 〈insert … seven_bits v low, high, accA〉 647 else 648 〈low, insert … seven_bits v high, accA〉. 649 650 axiom delete: 651 ∀A: Type[0]. 652 ∀n: nat. 653 ∀b: BitVector n. 654 BitVectorTrie A n → BitVectorTrie A n. 655 656 definition delete_from_internal_ram: 657 ∀addr: Byte. 658 ∀M: internal_pseudo_address_map. 659 internal_pseudo_address_map ≝ 660 λaddr, M. 661 let 〈low, high, accA〉 ≝ M in 662 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 663 if head' … bit_one then 664 〈delete … seven_bits low, high, accA〉 665 else 666 〈low, delete … seven_bits high, accA〉. 667 668 definition overwrite_or_delete_from_internal_ram: 669 ∀addr: Byte. 670 ∀v: option address_entry. 671 ∀M: internal_pseudo_address_map. 672 internal_pseudo_address_map ≝ 673 λaddr, v, M. 674 let 〈low, high, accA〉 ≝ M in 675 match v with 676 [ None ⇒ delete_from_internal_ram addr M 677 | Some v' ⇒ insert_into_internal_ram addr v' M 678 ]. 679 680 definition lookup_from_internal_ram: 681 ∀addr: Byte. 682 ∀M: internal_pseudo_address_map. 683 option address_entry ≝ 684 λaddr, M. 685 let 〈low, high, accA〉 ≝ M in 686 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 687 if head' … bit_one then 688 lookup_opt … seven_bits high 689 else 690 lookup_opt … seven_bits low. 515 691 516 692 definition next_internal_pseudo_address_map0 ≝ … … 521 697 λM: internal_pseudo_address_map. 522 698 λs: PreStatus T cm. 699 let 〈low, high, accA〉 ≝ M in 523 700 match fetched with 524 701 [ Comment _ ⇒ Some ? M … … 527 704 | Call a ⇒ 528 705 let a' ≝ addr_of a s in 529 let 〈 callM, accM〉 ≝ Min530 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::531 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉706 let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in 707 Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉 708 (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M)) 532 709 | Mov _ _ ⇒ Some … M 533 710 | Instruction instr ⇒ 534 711 match instr return λx. option internal_pseudo_address_map with 535 712 [ ADD addr1 addr2 ⇒ 536 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then713 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 537 714 Some ? M 538 715 else 539 716 None ? 540 717 | ADDC addr1 addr2 ⇒ 541 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then718 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 542 719 Some ? M 543 720 else 544 721 None ? 545 722 | SUBB addr1 addr2 ⇒ 546 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then723 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 547 724 Some ? M 548 725 else 549 726 None ? 550 727 | INC addr1 ⇒ 551 if a ddressing_mode_okT M ? s addr1 then728 if assert_data T M ? s addr1 then 552 729 Some ? M 553 730 else 554 731 None ? 555 732 | DEC addr1 ⇒ 556 if a ddressing_mode_okT M … s addr1 then733 if assert_data T M … s addr1 then 557 734 Some ? M 558 735 else 559 736 None ? 560 737 | MUL addr1 addr2 ⇒ 561 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then738 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 562 739 Some ? M 563 740 else 564 741 None ? 565 742 | DIV addr1 addr2 ⇒ 566 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then743 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 567 744 Some ? M 568 745 else 569 746 None ? 570 747 | DA addr1 ⇒ 571 if a ddressing_mode_okT M … s addr1 then748 if assert_data T M … s addr1 then 572 749 Some ? M 573 750 else … … 584 761 [ inl l ⇒ 585 762 let 〈left, right〉 ≝ l in 586 if a ddressing_mode_ok T M … s left ∧ addressing_mode_okT M … s right then763 if assert_data T M … s left ∧ assert_data T M … s right then 587 764 Some ? M 588 else if ¬(a ddressing_mode_ok T M … s left) ∧ ¬(addressing_mode_okT M … s right) then765 else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then 589 766 Some ? M 590 767 else … … 592 769 | inr r ⇒ 593 770 let 〈left, right〉 ≝ r in 594 if a ddressing_mode_ok T M … s left ∧ addressing_mode_okT M … s right then771 if assert_data T M … s left ∧ assert_data T M … s right then 595 772 Some ? M 596 else if ¬(a ddressing_mode_ok T M … s left) ∧ ¬(addressing_mode_okT M … s right) then773 else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then 597 774 Some ? M 598 775 else … … 600 777 ] 601 778 | DJNZ addr1 addr2 ⇒ 602 if a ddressing_mode_okT M … s addr1 then779 if assert_data T M … s addr1 then 603 780 Some ? M 604 781 else 605 782 None ? 606 783 | CLR addr1 ⇒ 607 if a ddressing_mode_okT M … s addr1 then784 if assert_data T M … s addr1 then 608 785 Some ? M 609 786 else 610 787 None ? 611 788 | CPL addr1 ⇒ 612 if a ddressing_mode_okT M … s addr1 then789 if assert_data T M … s addr1 then 613 790 Some ? M 614 791 else 615 792 None ? 616 793 | RL addr1 ⇒ 617 if a ddressing_mode_okT M … s addr1 then794 if assert_data T M … s addr1 then 618 795 Some ? M 619 796 else 620 797 None ? 621 798 | RLC addr1 ⇒ 622 if a ddressing_mode_okT M … s addr1 then799 if assert_data T M … s addr1 then 623 800 Some ? M 624 801 else 625 802 None ? 626 803 | RR addr1 ⇒ 627 if a ddressing_mode_okT M … s addr1 then804 if assert_data T M … s addr1 then 628 805 Some ? M 629 806 else 630 807 None ? 631 808 | RRC addr1 ⇒ 632 if a ddressing_mode_okT M … s addr1 then809 if assert_data T M … s addr1 then 633 810 Some ? M 634 811 else 635 812 None ? 636 813 | SWAP addr1 ⇒ 637 if a ddressing_mode_okT M … s addr1 then814 if assert_data T M … s addr1 then 638 815 Some ? M 639 816 else 640 817 None ? 641 818 | SETB addr1 ⇒ 642 if a ddressing_mode_okT M … s addr1 then819 if assert_data T M … s addr1 then 643 820 Some ? M 644 821 else … … 646 823 (* XXX: need to track addresses pushed and popped off the stack? *) 647 824 | PUSH addr1 ⇒ 648 let 〈callM, accM〉 ≝ M in649 825 match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 650 826 [ DIRECT d ⇒ λproof. 651 let extended ≝ pad 8 8 d in 652 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉 827 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 828 if head' … bit_one then 829 if eq_bv … seven_bits (bitvector_of_nat … 224) then 830 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M) 831 else 832 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 833 else 834 match lookup_from_internal_ram … d M with 835 [ None ⇒ 836 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 837 | Some ul_addr ⇒ 838 Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M) 839 ] 653 840 | _ ⇒ λother: False. ⊥ 654 841 ] (subaddressing_modein … addr1) 655 | POP addr1 ⇒ Some … M 842 | POP addr1 ⇒ 843 let sp ≝ get_8051_sfr ?? s SFR_SP in 844 match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 845 [ DIRECT d ⇒ λproof. 846 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 847 if head' … bit_one then 848 if eq_bv … d (bitvector_of_nat … 224) then 849 Some … 〈low, high, lookup_from_internal_ram … sp M〉 850 else 851 match lookup_from_internal_ram sp M with 852 [ None ⇒ Some ? M 853 | _ ⇒ None ? 854 ] 855 else 856 Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M) 857 | _ ⇒ λother: False. ⊥ 858 ] (subaddressing_modein … addr1) 656 859 | XCH addr1 addr2 ⇒ 657 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then860 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 658 861 Some ? M 659 862 else 660 863 None ? 661 864 | XCHD addr1 addr2 ⇒ 662 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then865 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 663 866 Some ? M 664 867 else 665 868 None ? 666 869 | RET ⇒ 667 let 〈callM, accM〉 ≝ M in 668 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 669 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 670 if sp_plus_1 ∧ sp_plus_2 then 671 Some … M 672 else 673 None ? 870 let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in 871 let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in 872 match lookup_from_internal_ram sp_minus_1 M with 873 [ None ⇒ None … 874 | Some low_addr_high ⇒ 875 match lookup_from_internal_ram sp_minus_2 M with 876 [ None ⇒ None … 877 | Some high_addr_low ⇒ 878 let 〈low, addr_high〉 ≝ low_addr_high in 879 let 〈high, addr_low〉 ≝ high_addr_low in 880 let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in 881 let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in 882 if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then 883 Some ? M 884 else 885 None ? 886 ] 887 ] 674 888 | RETI ⇒ 675 let 〈callM, accM〉 ≝ M in 676 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 677 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 678 if sp_plus_1 ∧ sp_plus_2 then 679 Some … M 680 else 681 None ? 889 let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in 890 let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in 891 match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with 892 [ None ⇒ None … 893 | Some low_addr_high ⇒ 894 match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with 895 [ None ⇒ None … 896 | Some high_addr_low ⇒ 897 let 〈low, addr_high〉 ≝ low_addr_high in 898 let 〈high, addr_low〉 ≝ high_addr_low in 899 let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in 900 let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in 901 if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then 902 Some ? M 903 else 904 None ? 905 ] 906 ] 682 907 | NOP ⇒ Some … M 683 908 | MOVX addr1 ⇒ 684 909 match addr1 with 685 910 [ inl l ⇒ 686 let 〈acc_a, others〉 ≝ l in 687 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 688 let others_ok ≝ addressing_mode_ok T M … s others in 689 if acc_a_ok ∧ others_ok then 690 Some ? M 691 else 692 None ? 911 Some ? 〈low, high, None …〉 693 912 | inr r ⇒ 694 913 let 〈others, acc_a〉 ≝ r in 695 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 696 let others_ok ≝ addressing_mode_ok T M … s others in 697 if others_ok ∧ acc_a_ok then 914 if assert_data T M … s acc_a then 698 915 Some ? M 699 916 else … … 704 921 [ inl l ⇒ 705 922 let 〈acc_a, others〉 ≝ l in 706 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in707 let others_ok ≝ a ddressing_mode_okT M … s others in923 let acc_a_ok ≝ assert_data T M … s acc_a in 924 let others_ok ≝ assert_data T M … s others in 708 925 if acc_a_ok ∧ others_ok then 709 926 Some ? M … … 712 929 | inr r ⇒ 713 930 let 〈direct, others〉 ≝ r in 714 let direct_ok ≝ a ddressing_mode_okT M … s direct in715 let others_ok ≝ a ddressing_mode_okT M … s others in931 let direct_ok ≝ assert_data T M … s direct in 932 let others_ok ≝ assert_data T M … s others in 716 933 if direct_ok ∧ others_ok then 717 934 Some ? M … … 725 942 [ inl l ⇒ 726 943 let 〈acc_a, others〉 ≝ l in 727 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in728 let others_ok ≝ a ddressing_mode_okT M … s others in944 let acc_a_ok ≝ assert_data T M … s acc_a in 945 let others_ok ≝ assert_data T M … s others in 729 946 if acc_a_ok ∧ others_ok then 730 947 Some ? M … … 733 950 | inr r ⇒ 734 951 let 〈direct, others〉 ≝ r in 735 let direct_ok ≝ a ddressing_mode_okT M … s direct in736 let others_ok ≝ a ddressing_mode_okT M … s others in952 let direct_ok ≝ assert_data T M … s direct in 953 let others_ok ≝ assert_data T M … s others in 737 954 if direct_ok ∧ others_ok then 738 955 Some ? M … … 742 959 | inr r ⇒ 743 960 let 〈carry, others〉 ≝ r in 744 let carry_ok ≝ a ddressing_mode_okT M … s carry in745 let others_ok ≝ a ddressing_mode_okT M … s others in961 let carry_ok ≝ assert_data T M … s carry in 962 let others_ok ≝ assert_data T M … s others in 746 963 if carry_ok ∧ others_ok then 747 964 Some ? M … … 755 972 [ inl l ⇒ 756 973 let 〈acc_a, others〉 ≝ l in 757 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in758 let others_ok ≝ a ddressing_mode_okT M … s others in974 let acc_a_ok ≝ assert_data T M … s acc_a in 975 let others_ok ≝ assert_data T M … s others in 759 976 if acc_a_ok ∧ others_ok then 760 977 Some ? M … … 763 980 | inr r ⇒ 764 981 let 〈direct, others〉 ≝ r in 765 let direct_ok ≝ a ddressing_mode_okT M … s direct in766 let others_ok ≝ a ddressing_mode_okT M … s others in982 let direct_ok ≝ assert_data T M … s direct in 983 let others_ok ≝ assert_data T M … s others in 767 984 if direct_ok ∧ others_ok then 768 985 Some ? M … … 772 989 | inr r ⇒ 773 990 let 〈carry, others〉 ≝ r in 774 let carry_ok ≝ a ddressing_mode_okT M … s carry in775 let others_ok ≝ a ddressing_mode_okT M … s others in991 let carry_ok ≝ assert_data T M … s carry in 992 let others_ok ≝ assert_data T M … s others in 776 993 if carry_ok ∧ others_ok then 777 994 Some ? M … … 780 997 ] 781 998 | MOV addr1 ⇒ 999 (* XXX: wrong *) 782 1000 match addr1 with 783 1001 [ inl l ⇒ … … 791 1009 [ inl l'''' ⇒ 792 1010 let 〈acc_a, others〉 ≝ l'''' in 793 if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then 794 Some ? M 795 else 796 None ? 1011 match data_or_address T M … s others with 1012 [ None ⇒ None ? 1013 | Some s ⇒ 1014 Some … 〈low, high, s〉 1015 ] 797 1016 | inr r ⇒ 798 1017 let 〈others, others'〉 ≝ r in 799 if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then 800 Some ? M 801 else 802 None ? 1018 let address ≝ 1019 match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with 1020 [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r 1021 | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]] 1022 | _ ⇒ λother: False. ⊥ 1023 ] (subaddressing_modein … others) 1024 in 1025 match data_or_address T M … s others' with 1026 [ None ⇒ None ? 1027 | Some s ⇒ 1028 Some … (overwrite_or_delete_from_internal_ram address s M) 1029 ] 803 1030 ] 804 1031 | inr r ⇒ 805 let 〈direct, others〉 ≝ r in 806 if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then 807 Some ? M 808 else 809 None ? 1032 let 〈direct', others〉 ≝ r in 1033 match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 1034 [ DIRECT d ⇒ λproof. 1035 match data_or_address T M … s others with 1036 [ None ⇒ None ? 1037 | Some s' ⇒ 1038 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 1039 if head' … bit_one then 1040 if eq_bv … d (bitvector_of_nat … 224) then 1041 Some … 〈low, high, s'〉 1042 else 1043 match s' with 1044 [ None ⇒ Some ? M 1045 | Some s'' ⇒ None ? 1046 ] 1047 else 1048 Some … (overwrite_or_delete_from_internal_ram d s' M) 1049 ] 1050 | _ ⇒ λother: False. ⊥ 1051 ] (subaddressing_modein … direct') 810 1052 ] 811 | inr r ⇒ 812 let 〈dptr, data_16〉 ≝ r in 813 if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then 814 Some ? M 815 else 816 None ? 1053 | inr r ⇒ Some … M 817 1054 ] 818 1055 | inr r ⇒ 819 1056 let 〈carry, bit_addr〉 ≝ r in 820 if a ddressing_mode_ok T M … s carry ∧ addressing_mode_okT M … s bit_addr then1057 if assert_data T M … s bit_addr then 821 1058 Some ? M 822 1059 else … … 825 1062 | inr r ⇒ 826 1063 let 〈bit_addr, carry〉 ≝ r in 827 if a ddressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carrythen1064 if assert_data T M … s bit_addr then 828 1065 Some ? M 829 1066 else … … 858 1095 λsigma: Word → Word. 859 1096 match \snd M with 860 [ data⇒ sfrs861 | address upper_loweraddress ⇒1097 [ None ⇒ sfrs 1098 | Some upper_lower_address ⇒ 862 1099 let index ≝ sfr_8051_index SFR_ACC_A in 863 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in 1100 let acc_a ≝ get_index_v … sfrs index ? in 1101 let 〈upper_lower, address〉 ≝ upper_lower_address in 864 1102 if eq_upper_lower upper_lower upper then 865 set_index Byte 19 sfrs index high ? 1103 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in 1104 set_index Byte 19 sfrs index high ? 866 1105 else 867 set_index Byte 19 sfrs index low ? 1106 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in 1107 set_index Byte 19 sfrs index low ? 868 1108 ]. 869 1109 // … … 881 1121 let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in 882 1122 let pc ≝ sigma (program_counter … ps) in 883 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in884 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in1123 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in 1124 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in 885 1125 mk_PreStatus (BitVectorTrie Byte 16) 886 1126 cm … … 1206 1446 ∀arg: Byte. 1207 1447 ∀b: bool. 1208 a ddressing_mode_okm s (DIRECT arg) = true →1448 assert_data m s (DIRECT arg) = true → 1209 1449 get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) = 1210 1450 get_arg_8 ? s b (DIRECT arg). … … 1265 1505 get_arg_8 (internal_ram ...) (DIRECT arg) 1266 1506 1267 ((if a ddressing_mode_ok M ps ACC_A∧addressing_mode_okM ps (DIRECT ARG2)1507 ((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 1268 1508 then Some internal_pseudo_address_map M 1269 1509 else None internal_pseudo_address_map ) -
src/ASM/AssemblyProofSplit.ma
r2265 r2272 390 390 qed. 391 391 392 lemma get_index_v_set_index_hit: 393 ∀A: Type[0]. 394 ∀n: nat. 395 ∀v: Vector A n. 396 ∀i: nat. 397 ∀e: A. 398 ∀i_lt_n_proof: i < n. 399 ∀i_lt_n_proof': i < n. 400 get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e. 401 #A #n #v elim v 402 [1: 403 #i #e #i_lt_n_proof 404 cases (lt_to_not_zero … i_lt_n_proof) 405 |2: 406 #n' #hd #tl #inductive_hypothesis #i #e 407 cases i 408 [1: 409 #i_lt_n_proof #i_lt_n_proof' % 410 |2: 411 #i' #i_lt_n_proof' #i_lt_n_proof'' 412 whd in ⊢ (??%?); @inductive_hypothesis 413 ] 414 ] 415 qed. 392 axiom insert_low_internal_ram_of_pseudo_low_internal_ram': 393 ∀M, M', sigma,cm,s,addr,v,v'. 394 (∀addr'. 395 ((false:::addr) = addr' → 396 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = 397 map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧ 398 ((false:::addr) ≠ addr' → 399 let 〈callM, accM〉 ≝ M in 400 let 〈callM', accM'〉 ≝ M' in 401 accM = accM' ∧ 402 assoc_list_lookup … addr' (eq_bv 8) … callM = 403 assoc_list_lookup … addr' (eq_bv 8) … callM')) → 404 insert Byte 7 addr v' 405 (low_internal_ram_of_pseudo_low_internal_ram M' 406 (low_internal_ram pseudo_assembly_program cm s)) = 407 low_internal_ram_of_pseudo_low_internal_ram M 408 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 416 409 417 (*418 410 lemma write_at_stack_pointer_status_of_pseudo_status: 419 411 ∀M, M'. … … 423 415 ∀s, s'. 424 416 ∀new_b, new_b'. 425 M = M' → 426 map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' → 417 map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' → 427 418 status_of_pseudo_status M cm s sigma policy = s' → 428 419 write_at_stack_pointer ?? s' new_b' = 429 status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.420 status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy. 430 421 #M #M' #cm #sigma #policy #s #s' #new_b #new_b' 431 # Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl422 #new_b_refl #s_refl <new_b_refl <s_refl 432 423 whd in match write_at_stack_pointer; normalize nodelta 433 424 @pair_elim #nu #nl #nu_nl_refl normalize nodelta … … 449 440 ] 450 441 |2: 451 cases (get_index_v bool ????) normalize nodelta 452 whd in match status_of_pseudo_status; normalize nodelta 453 whd in match set_low_internal_ram; normalize nodelta 454 @split_eq_status try % 455 [1: 456 @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma) 457 |2: 458 @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma) 442 @if_then_else_status_of_pseudo_status try % 443 [2: 444 @sym_eq <set_low_internal_ram_status_of_pseudo_status 445 [1: 446 @eq_f2 447 [2: 448 @insert_low_internal_ram_of_pseudo_low_internal_ram' 449 @sym_eq 450 [2: 451 <set_low_internal_ram_status_of_pseudo_status 452 [1: 453 @eq_f2 454 [2: 455 @sym_eq 456 >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b') 457 [2: 458 >new_b_refl 459 ] 459 460 ] 460 *) 461 qed. 461 462 462 463 lemma main_lemma_preinstruction: … … 519 520 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 520 521 (get_arg_8 … s false addr2) false in 521 let cy_flag ≝ get_index' ? O 522 let cy_flag ≝ get_index' ? O ? flags in 522 523 let ac_flag ≝ get_index' ? 1 ? flags in 523 524 let ov_flag ≝ get_index' ? 2 ? flags in … … 917 918 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 918 919 whd in match execute_1_preinstruction; normalize nodelta 919 [ 1,2: (* ADD and ADDC *)920 [(*1,2: (* ADD and ADDC *) 920 921 (* XXX: work on the right hand side *) 921 922 (* XXX: switch to the left hand side *) … … 1535 1536 ] 1536 1537 ] 1537 |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1538 |*)12: (* JC *) 1539 >EQP -P normalize nodelta 1540 whd in match expand_pseudo_instruction; normalize nodelta 1541 whd in match expand_relative_jump; normalize nodelta 1542 whd in match expand_relative_jump_internal; normalize nodelta 1543 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1544 inversion sj_possible #sj_possible_refl normalize nodelta 1545 [1: 1546 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1547 whd in maps_assm:(??%%); 1548 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1549 whd in ⊢ (??%?); normalize nodelta 1550 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1551 whd in ⊢ (??%?); 1552 @if_then_else_status_of_pseudo_status 1553 >EQs >EQticks <instr_refl normalize nodelta 1554 [1: 1555 @(get_cy_flag_status_of_pseudo_status M') % 1556 |2: 1557 @sym_eq @set_program_counter_status_of_pseudo_status 1558 [1: 1559 |2: 1560 @sym_eq @set_clock_status_of_pseudo_status try % 1561 whd in match ticks_of0; normalize nodelta 1562 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1563 [1: 1564 @eq_f2 try % 1565 >sigma_increment_commutation 1566 lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta 1567 * #sigma_zero_assm #relevant cases (relevant ppc ?) 1568 [1: 1569 -relevant 1570 [2: 1571 >EQcm assumption 1572 |1: 1573 #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f 1574 >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2 1575 ] 1576 |2: 1577 ] 1578 |2: 1579 >sj_possible_refl % 1580 ] 1581 ] 1582 |3: 1583 ] 1584 ] 1538 1585 cases daemon 1539 |29,30: (* ANL and ORL *) 1586 |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1587 cases daemon 1588 |(*29,30: (* ANL and ORL *) 1540 1589 inversion addr 1541 1590 [1,3: … … 2228 2277 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) 2229 2278 ] 2230 | 42: (* PUSH *)2279 |*)42: (* PUSH *) 2231 2280 >EQP -P normalize nodelta lapply instr_refl 2232 2281 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta -
src/ASM/Interpret.ma
r2264 r2272 727 727 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 728 728 let s ≝ set_8051_sfr … s SFR_SP new_sp in 729 write_at_stack_pointer … s d729 write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d)) 730 730 | _ ⇒ λother: False. ⊥ 731 731 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) -
src/ASM/Status.ma
r2270 r2272 700 700 set_low_internal_ram … s new_low_internal_ram. 701 701 702 definition read_at_stack_pointer ≝ 703 λM: Type[0]. 704 λcode_memory:M. 705 λs: PreStatus M code_memory. 706 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in 707 let m ≝ get_index_v ?? nu O ? in 708 let r1 ≝ get_index_v ?? nu 1 ? in 709 let r2 ≝ get_index_v ?? nu 2 ? in 710 let r3 ≝ get_index_v ?? nu 3 ? in 711 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 702 definition read_from_internal_ram ≝ 703 λM: Type[0]. 704 λcode_memory:M. 705 λs: PreStatus M code_memory. 706 λaddr: Byte. 707 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 712 708 let memory ≝ 713 if mthen709 if head' … bit_one then 714 710 (low_internal_ram ?? s) 715 711 else 716 712 (high_internal_ram ?? s) 717 713 in 718 lookup … address memory (zero 8).719 [1,2,3,4: 720 normalize 721 repeat (@ le_S_S)722 @ le_O_n723 ]724 qed.714 lookup … seven_bits memory (zero 8). 715 716 definition read_at_stack_pointer ≝ 717 λM: Type[0]. 718 λcode_memory:M. 719 λs: PreStatus M code_memory. 720 read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP). 725 721 726 722 definition write_at_stack_pointer ≝ … … 729 725 λs: PreStatus M code_memory. 730 726 λv: Byte. 731 let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in 732 let bit_zero ≝ get_index_v ?? nu O ? in 733 let bit_1 ≝ get_index_v ?? nu 1 ? in 734 let bit_2 ≝ get_index_v ?? nu 2 ? in 735 let bit_3 ≝ get_index_v ?? nu 3 ? in 736 if bit_zero then 737 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 738 v (high_internal_ram ?? s) in 727 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in 728 if head' … 0 bit_one then 729 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 739 730 set_high_internal_ram ?? s memory 740 731 else 741 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 742 v (low_internal_ram ?? s) in 732 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 743 733 set_low_internal_ram ?? s memory. 744 [1,2,3,4:745 normalize746 repeat (@ le_S_S)747 @ le_O_n748 ]749 qed.750 734 751 735 definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝ … … 971 955 match head' … bit_1 with 972 956 [ true ⇒ 973 let address ≝ nat_of_bitvector … seven_bits in 974 let d ≝ address ÷ 8 in 975 let m ≝ address mod 8 in 976 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 957 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 958 let trans ≝ true:::four_bits @@ [[false; false; false]] in 977 959 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 978 get_index_v … sfr m?960 get_index_v … sfr (nat_of_bitvector … three_bits) ? 979 961 | false ⇒ 980 let address ≝ nat_of_bitvector …seven_bits in981 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in962 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 963 let address' ≝ [[true; false; false]]@@four_bits in 982 964 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 983 get_index_v … t ( modulus address 8) ?965 get_index_v … t (nat_of_bitvector … three_bits) ? 984 966 ] 985 967 | N_BIT_ADDR n ⇒ … … 988 970 match head' … bit_1 with 989 971 [ true ⇒ 990 let address ≝ nat_of_bitvector … seven_bits in 991 let d ≝ address ÷ 8 in 992 let m ≝ address mod 8 in 993 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 972 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 973 let trans ≝ true:::four_bits @@ [[false; false; false]] in 994 974 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 995 ¬(get_index_v … sfr m?)975 ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?) 996 976 | false ⇒ 997 let address ≝ nat_of_bitvector …seven_bits in998 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in977 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 978 let address' ≝ [[true; false; false]]@@four_bits in 999 979 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1000 ¬(get_index_v … t ( modulus address 8) ?)980 ¬(get_index_v … t (nat_of_bitvector … three_bits) ?) 1001 981 ] 1002 982 | CARRY ⇒ λcarry: True. get_cy_flag ?? s … … 1004 984 match other in False with [ ] 1005 985 ] (subaddressing_modein … a). 1006 @modulus_less_than986 // 1007 987 qed. 1008 988 … … 1018 998 match head' … bit_1 with 1019 999 [ true ⇒ 1020 let address ≝ nat_of_bitvector … seven_bits in 1021 let d ≝ address ÷ 8 in 1022 let m ≝ address mod 8 in 1023 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1024 let sfr ≝ get_bit_addressable_sfr … s t true in 1025 let new_sfr ≝ set_index … sfr m v ? in 1026 set_bit_addressable_sfr … s new_sfr t 1000 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1001 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1002 let sfr ≝ get_bit_addressable_sfr … s trans true in 1003 let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in 1004 set_bit_addressable_sfr … s new_sfr trans 1027 1005 | false ⇒ 1028 let address ≝ nat_of_bitvector …seven_bits in1029 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1006 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1007 let address' ≝ [[true; false; false]]@@four_bits in 1030 1008 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1031 let n_bit ≝ set_index … t ( modulus address 8) v ? in1009 let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in 1032 1010 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1033 1011 set_low_internal_ram … s memory … … 1043 1021 [ ] 1044 1022 ] (subaddressing_modein … a). 1045 @modulus_less_than1023 // 1046 1024 qed. 1047 1025 -
src/ASM/StatusProofs.ma
r2172 r2272 27 27 #m #s #v 28 28 whd in match write_at_stack_pointer; normalize nodelta 29 cases(vsplit … 4 4 ?) #nu #nlnormalize nodelta30 cases (get_index_v … 4 nu 0 ?)//29 cases(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta 30 cases (head' bool ??) normalize nodelta // 31 31 qed. 32 32 … … 236 236 = special_function_registers_8051 T cm s. 237 237 #T #cm #s #x whd in ⊢ (??(???%)?); 238 cases (vsplit ????) # nu #nl normalize nodelta;239 cases (get_index_v bool ????)%238 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 239 cases (head' bool ??) normalize nodelta % 240 240 qed. 241 241 … … 297 297 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. 298 298 #T #cm #s #x whd in ⊢ (??(???%)?); 299 cases (vsplit ????) # nu #nl normalize nodelta;300 cases ( get_index_v bool ????) %299 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 300 cases (head' bool ??) % 301 301 qed. 302 302 … … 306 306 = special_function_registers_8052 T cm s. 307 307 #T #cm #s #x whd in ⊢ (??(???%)?); 308 cases (vsplit ????) # nu #nl normalize nodelta;309 cases ( get_index_v bool ????) %308 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 309 cases (head' bool ??) % 310 310 qed. 311 311 … … 313 313 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. 314 314 #T #cm #s #x whd in ⊢ (??(???%)?); 315 cases (vsplit ????) # nu #nl normalize nodelta;316 cases ( get_index_v bool ????) %315 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 316 cases (head' bool ??) % 317 317 qed. 318 318 … … 320 320 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. 321 321 #T #cm #s #x whd in ⊢ (??(???%)?); 322 cases (vsplit ????) # nu #nl normalize nodelta;323 cases ( get_index_v bool ????) %322 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 323 cases (head' bool ??) % 324 324 qed. 325 325 … … 412 412 #m #cm #s #v 413 413 whd in match write_at_stack_pointer; normalize nodelta 414 cases (vsplit bool 4 4 ?) #nu #nlnormalize nodelta415 cases (get_index_v bool 4 nu ??) normalize nodelta /demod/%414 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 415 cases (head' bool ??) % 416 416 qed. 417 417 -
src/ASM/StatusProofsSplit.ma
r2172 r2272 81 81 ∀cm: M. 82 82 ∀s: PreStatus M cm. 83 ∀sfr: SFR8051.84 83 ∀pc: Word. 85 84 get_8051_sfr M cm (set_program_counter M cm s pc) = 86 85 get_8051_sfr M cm s. 87 #M #cm #s # sfr #pc %86 #M #cm #s #pc % 88 87 qed. 89 88 … … 360 359 ∀sigma: Word → Word. 361 360 ∀policy: Word → bool. 362 \snd M = data→361 \snd M = None … → 363 362 special_function_registers_8051 pseudo_assembly_program cm s = 364 363 special_function_registers_8051 (BitVectorTrie Byte 16) … … 457 456 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 458 457 cases M #left #right cases right normalize nodelta try % 459 -right * #address458 -right * * #address normalize nodelta 460 459 @pair_elim #high #low #high_low_refl normalize nodelta 461 460 whd in match sfr_8051_index; normalize nodelta … … 469 468 include alias "ASM/BitVectorTrie.ma". 470 469 *) 471 472 lemma get_8051_sfr_status_of_pseudo_status:473 ∀M.474 ∀cm, ps, sigma, policy.475 ∀sfr.476 (sfr = SFR_ACC_A → \snd M = data) →477 get_8051_sfr (BitVectorTrie Byte 16)478 (code_memory_of_pseudo_assembly_program cm sigma policy)479 (status_of_pseudo_status M cm ps sigma policy) sfr =480 get_8051_sfr pseudo_assembly_program cm ps sfr.481 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant482 [18:483 >relevant %484 ]485 cases sndM try % * #address486 whd in match get_8051_sfr;487 whd in match status_of_pseudo_status; normalize nodelta488 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta489 @pair_elim #upper #lower #upper_lower_refl490 @get_index_v_set_index_miss @nmk #relevant491 normalize in relevant; destruct(relevant)492 qed.493 470 494 471 lemma bitvector_cases_hd_tl: … … 572 549 special_function_registers_8051 M cm ps. 573 550 // 574 qed.575 576 lemma get_arg_8_pseudo_addressing_mode_ok:577 ∀M: internal_pseudo_address_map.578 ∀cm: pseudo_assembly_program.579 ∀ps: PreStatus pseudo_assembly_program cm.580 ∀sigma: Word → Word.581 ∀policy: Word → bool.582 ∀addr1: [[registr; direct]].583 addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →584 get_arg_8 (BitVectorTrie Byte 16)585 (code_memory_of_pseudo_assembly_program cm sigma policy)586 (status_of_pseudo_status M cm ps sigma policy) true addr1 =587 get_arg_8 pseudo_assembly_program cm ps true addr1.588 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]589 #M #cm #ps #sigma #policy #addr1590 @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);591 [1:592 whd in ⊢ (??%? → ??%?);593 whd in match bit_address_of_register; normalize nodelta594 @pair_elim #un #ln #un_ln_refl595 lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl596 @(pair_replace ?????????? un_ln_refl)597 [1:598 whd in match get_8051_sfr; normalize nodelta599 whd in match sfr_8051_index; normalize nodelta600 @eq_f <get_index_v_special_function_registers_8051_not_acc_a601 try % #absurd destruct(absurd)602 |2:603 #assembly_mode_ok_refl604 >low_internal_ram_of_pseudo_internal_ram_miss605 [1:606 %607 |2:608 cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta609 #absurd try % @sym_eq assumption610 ]611 ]612 |2:613 #addressing_mode_ok_refl whd in ⊢ (??%?);614 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*615 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta616 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta617 [1:618 whd in ⊢ (??%%); normalize nodelta619 cases (eqb ??) normalize nodelta [1: % ]620 cases (eqb ??) normalize nodelta [1: % ]621 cases (eqb ??) normalize nodelta [1: % ]622 cases (eqb ??) normalize nodelta [1: % ]623 cases (eqb ??) normalize nodelta [1:624 @get_8051_sfr_status_of_pseudo_status625 #absurd destruct(absurd)626 ]627 cases (eqb ??) normalize nodelta [1:628 @get_8051_sfr_status_of_pseudo_status629 #absurd destruct(absurd)630 ]631 cases (eqb ??) normalize nodelta [1:632 @get_8051_sfr_status_of_pseudo_status633 #absurd destruct(absurd)634 ]635 cases (eqb ??) normalize nodelta [1:636 @get_8051_sfr_status_of_pseudo_status637 #absurd destruct(absurd)638 ]639 cases (eqb ??) normalize nodelta [1:640 @get_8051_sfr_status_of_pseudo_status641 #absurd destruct(absurd)642 ]643 cases (eqb ??) normalize nodelta [1: % ]644 cases (eqb ??) normalize nodelta [1: % ]645 cases (eqb ??) normalize nodelta [1: % ]646 cases (eqb ??) normalize nodelta [1: % ]647 cases (eqb ??) normalize nodelta [1: % ]648 cases (eqb ??) normalize nodelta [1:649 @get_8051_sfr_status_of_pseudo_status650 #absurd destruct(absurd)651 ]652 cases (eqb ??) normalize nodelta [1:653 @get_8051_sfr_status_of_pseudo_status654 #absurd destruct(absurd)655 ]656 cases (eqb ??) normalize nodelta [1:657 @get_8051_sfr_status_of_pseudo_status658 #absurd destruct(absurd)659 ]660 cases (eqb ??) normalize nodelta [1:661 @get_8051_sfr_status_of_pseudo_status662 #absurd destruct(absurd)663 ]664 cases (eqb ??) normalize nodelta [1:665 @get_8051_sfr_status_of_pseudo_status666 #absurd destruct(absurd)667 ]668 cases (eqb ??) normalize nodelta [1:669 @get_8051_sfr_status_of_pseudo_status670 #absurd destruct(absurd)671 ]672 cases (eqb ??) normalize nodelta [1:673 @get_8051_sfr_status_of_pseudo_status674 #absurd destruct(absurd)675 ]676 cases (eqb ??) normalize nodelta [1:677 @get_8051_sfr_status_of_pseudo_status678 #absurd destruct(absurd)679 ]680 cases (eqb ??) normalize nodelta [1:681 @get_8051_sfr_status_of_pseudo_status682 #absurd destruct(absurd)683 ]684 cases (eqb ??) normalize nodelta [1:685 @get_8051_sfr_status_of_pseudo_status686 #absurd destruct(absurd)687 ]688 inversion (eqb ??) #eqb_refl normalize nodelta [1:689 @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl690 whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)691 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta692 #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_693 #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %694 ]695 cases (eqb ??) normalize nodelta [1:696 @get_8051_sfr_status_of_pseudo_status697 #absurd destruct(absurd)698 ] %699 |2:700 lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant701 whd in match status_of_pseudo_status; normalize nodelta702 >low_internal_ram_of_pseudo_internal_ram_miss try %703 cut(arg = false:::(three_bits@@nl))704 [1:705 <get_index_v_refl706 cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)707 [1:708 cut(ignore = [[get_index_v bool 4 nu 0 ?]])709 [1:710 @le_S_S @le_O_n711 |2:712 cut(ignore = \fst (vsplit bool 1 3 nu))713 [1:714 >ignore_three_bits_refl %715 |2:716 #ignore_refl >ignore_refl717 cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl718 >nu_refl %719 ]720 |3:721 #ignore_refl >ignore_refl in ignore_three_bits_refl;722 #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))723 #nu_refl <nu_refl %724 ]725 |2:726 #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl727 @sym_eq @vsplit_ok >nu_nl_refl %728 ]729 |2:730 #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;731 normalize nodelta732 [1:733 cases (eq_bv ???) normalize #absurd destruct(absurd)734 |2:735 #_ %736 ]737 ]738 ]739 ] *)740 551 qed. 741 552 … … 811 622 #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm 812 623 whd in match (set_8051_sfr ?????); 813 cases M #callM * try % #upper_lower #address624 cases M * #low #high * try % * * 814 625 whd in match (special_function_registers_8051 ???); 815 whd in match (sfr_8051_of_pseudo_sfr_8051 ???); 626 whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta 816 627 @pair_elim #high #low #high_low_refl normalize nodelta 817 628 cases (eq_upper_lower ??) normalize nodelta -
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.