Changeset 991 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 17, 2011, 5:17:43 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r989 r991 415 415 λi, j: instruction. 416 416 true.*) 417 axiom eq_instruction: instruction → instruction → bool. 418 axiom eq_instruction_refl: ∀i. eq_instruction i i = true. 417 418 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ 419 λa, b: addressing_mode. 420 match a with 421 [ DIRECT d ⇒ 422 match b with 423 [ DIRECT e ⇒ eq_bv ? d e 424 | _ ⇒ false 425 ] 426 | INDIRECT b' ⇒ 427 match b with 428 [ INDIRECT e ⇒ eq_b b' e 429 | _ ⇒ false 430 ] 431 | EXT_INDIRECT b' ⇒ 432 match b with 433 [ EXT_INDIRECT e ⇒ eq_b b' e 434 | _ ⇒ false 435 ] 436 | REGISTER bv ⇒ 437 match b with 438 [ REGISTER bv' ⇒ eq_bv ? bv bv' 439 | _ ⇒ false 440 ] 441 | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ] 442 | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ] 443 | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ] 444 | DATA b' ⇒ 445 match b with 446 [ DATA e ⇒ eq_bv ? b' e 447 | _ ⇒ false 448 ] 449 | DATA16 w ⇒ 450 match b with 451 [ DATA16 e ⇒ eq_bv ? w e 452 | _ ⇒ false 453 ] 454 | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ] 455 | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ] 456 | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] 457 | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] 458 | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ] 459 | BIT_ADDR b' ⇒ 460 match b with 461 [ BIT_ADDR e ⇒ eq_bv ? b' e 462 | _ ⇒ false 463 ] 464 | N_BIT_ADDR b' ⇒ 465 match b with 466 [ N_BIT_ADDR e ⇒ eq_bv ? b' e 467 | _ ⇒ false 468 ] 469 | RELATIVE n ⇒ 470 match b with 471 [ RELATIVE e ⇒ eq_bv ? n e 472 | _ ⇒ false 473 ] 474 | ADDR11 w ⇒ 475 match b with 476 [ ADDR11 e ⇒ eq_bv ? w e 477 | _ ⇒ false 478 ] 479 | ADDR16 w ⇒ 480 match b with 481 [ ADDR16 e ⇒ eq_bv ? w e 482 | _ ⇒ false 483 ] 484 ]. 485 486 lemma eq_bv_refl: 487 ∀n, b. 488 eq_bv n b b = true. 489 #n #b cases b // 490 qed. 491 492 lemma eq_b_refl: 493 ∀b. 494 eq_b b b = true. 495 #b cases b // 496 qed. 497 498 lemma eq_addressing_mode_refl: 499 ∀a. eq_addressing_mode a a = true. 500 #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl 501 try normalize % 502 qed. 503 504 definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ 505 λlt, rt, leq, req, left, right. 506 match left with 507 [ inl l ⇒ 508 match right with 509 [ inl l' ⇒ leq l l' 510 | _ ⇒ false 511 ] 512 | inr r ⇒ 513 match right with 514 [ inr r' ⇒ req r r' 515 | _ ⇒ false 516 ] 517 ]. 518 519 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ 520 λlt, rt, leq, req, left, right. 521 let 〈l, r〉 ≝ left in 522 let 〈l', r'〉 ≝ right in 523 leq l l' ∧ req r r'. 524 525 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ 526 λi, j. 527 match i with 528 [ ADD arg1 arg2 ⇒ 529 match j with 530 [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 531 | _ ⇒ false 532 ] 533 | ADDC arg1 arg2 ⇒ 534 match j with 535 [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 536 | _ ⇒ false 537 ] 538 | SUBB arg1 arg2 ⇒ 539 match j with 540 [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 541 | _ ⇒ false 542 ] 543 | INC arg ⇒ 544 match j with 545 [ INC arg' ⇒ eq_addressing_mode arg arg' 546 | _ ⇒ false 547 ] 548 | DEC arg ⇒ 549 match j with 550 [ DEC arg' ⇒ eq_addressing_mode arg arg' 551 | _ ⇒ false 552 ] 553 | MUL arg1 arg2 ⇒ 554 match j with 555 [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 556 | _ ⇒ false 557 ] 558 | DIV arg1 arg2 ⇒ 559 match j with 560 [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 561 | _ ⇒ false 562 ] 563 | DA arg ⇒ 564 match j with 565 [ DA arg' ⇒ eq_addressing_mode arg arg' 566 | _ ⇒ false 567 ] 568 | JC arg ⇒ 569 match j with 570 [ JC arg' ⇒ eq_addressing_mode arg arg' 571 | _ ⇒ false 572 ] 573 | JNC arg ⇒ 574 match j with 575 [ JNC arg' ⇒ eq_addressing_mode arg arg' 576 | _ ⇒ false 577 ] 578 | JB arg1 arg2 ⇒ 579 match j with 580 [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 581 | _ ⇒ false 582 ] 583 | JNB arg1 arg2 ⇒ 584 match j with 585 [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 586 | _ ⇒ false 587 ] 588 | JBC arg1 arg2 ⇒ 589 match j with 590 [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 591 | _ ⇒ false 592 ] 593 | JZ arg ⇒ 594 match j with 595 [ JZ arg' ⇒ eq_addressing_mode arg arg' 596 | _ ⇒ false 597 ] 598 | JNZ arg ⇒ 599 match j with 600 [ JNZ arg' ⇒ eq_addressing_mode arg arg' 601 | _ ⇒ false 602 ] 603 | CJNE arg1 arg2 ⇒ 604 match j with 605 [ CJNE arg1' arg2' ⇒ 606 let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in 607 let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in 608 let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 609 arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 610 | _ ⇒ false 611 ] 612 | DJNZ arg1 arg2 ⇒ 613 match j with 614 [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 615 | _ ⇒ false 616 ] 617 | CLR arg ⇒ 618 match j with 619 [ CLR arg' ⇒ eq_addressing_mode arg arg' 620 | _ ⇒ false 621 ] 622 | CPL arg ⇒ 623 match j with 624 [ CPL arg' ⇒ eq_addressing_mode arg arg' 625 | _ ⇒ false 626 ] 627 | RL arg ⇒ 628 match j with 629 [ RL arg' ⇒ eq_addressing_mode arg arg' 630 | _ ⇒ false 631 ] 632 | RLC arg ⇒ 633 match j with 634 [ RLC arg' ⇒ eq_addressing_mode arg arg' 635 | _ ⇒ false 636 ] 637 | RR arg ⇒ 638 match j with 639 [ RR arg' ⇒ eq_addressing_mode arg arg' 640 | _ ⇒ false 641 ] 642 | RRC arg ⇒ 643 match j with 644 [ RRC arg' ⇒ eq_addressing_mode arg arg' 645 | _ ⇒ false 646 ] 647 | SWAP arg ⇒ 648 match j with 649 [ SWAP arg' ⇒ eq_addressing_mode arg arg' 650 | _ ⇒ false 651 ] 652 | SETB arg ⇒ 653 match j with 654 [ SETB arg' ⇒ eq_addressing_mode arg arg' 655 | _ ⇒ false 656 ] 657 | PUSH arg ⇒ 658 match j with 659 [ PUSH arg' ⇒ eq_addressing_mode arg arg' 660 | _ ⇒ false 661 ] 662 | POP arg ⇒ 663 match j with 664 [ POP arg' ⇒ eq_addressing_mode arg arg' 665 | _ ⇒ false 666 ] 667 | XCH arg1 arg2 ⇒ 668 match j with 669 [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 670 | _ ⇒ false 671 ] 672 | XCHD arg1 arg2 ⇒ 673 match j with 674 [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 675 | _ ⇒ false 676 ] 677 | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ] 678 | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ] 679 | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ] 680 | MOVX arg ⇒ 681 match j with 682 [ MOVX arg' ⇒ 683 let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in 684 let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in 685 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 686 sum_eq arg arg' 687 | _ ⇒ false 688 ] 689 | XRL arg ⇒ 690 match j with 691 [ XRL arg' ⇒ 692 let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in 693 let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in 694 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 695 sum_eq arg arg' 696 | _ ⇒ false 697 ] 698 | ORL arg ⇒ 699 match j with 700 [ ORL arg' ⇒ 701 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in 702 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in 703 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in 704 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in 705 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 706 sum_eq arg arg' 707 | _ ⇒ false 708 ] 709 | ANL arg ⇒ 710 match j with 711 [ ANL arg' ⇒ 712 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in 713 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in 714 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in 715 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in 716 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 717 sum_eq arg arg' 718 | _ ⇒ false 719 ] 720 | MOV arg ⇒ 721 match j with 722 [ MOV arg' ⇒ 723 let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in 724 let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in 725 let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in 726 let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in 727 let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in 728 let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in 729 let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in 730 let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in 731 let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in 732 let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in 733 let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in 734 sum_eq_5 arg arg' 735 | _ ⇒ false 736 ] 737 ]. 738 739 lemma eq_sum_refl: 740 ∀A, B: Type[0]. 741 ∀leq, req. 742 ∀s. 743 ∀leq_refl: (∀t. leq t t = true). 744 ∀req_refl: (∀u. req u u = true). 745 eq_sum A B leq req s s = true. 746 #A #B #leq #req #s #leq_refl #req_refl 747 cases s whd in ⊢ (? → ??%?) // 748 qed. 749 750 lemma eq_prod_refl: 751 ∀A, B: Type[0]. 752 ∀leq, req. 753 ∀s. 754 ∀leq_refl: (∀t. leq t t = true). 755 ∀req_refl: (∀u. req u u = true). 756 eq_prod A B leq req s s = true. 757 #A #B #leq #req #s #leq_refl #req_refl 758 cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl 759 qed. 760 761 lemma eq_preinstruction_refl: 762 ∀i. 763 eq_preinstruction i i = true. 764 #i cases i try #arg1 try #arg2 765 try @eq_addressing_mode_refl 766 [1,2,3,4,5,6,7,8,10,16,17,18,19,20: 767 whd in ⊢ (??%?) 768 try % 769 >eq_addressing_mode_refl 770 >eq_addressing_mode_refl % 771 |13,15: 772 whd in ⊢ (??%?) 773 cases arg1 774 [*: 775 #arg1_left normalize nodelta 776 >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] 777 ] 778 |11,12: 779 whd in ⊢ (??%?) 780 cases arg1 781 [1: 782 #arg1_left normalize nodelta 783 >(eq_sum_refl …) 784 [1: % | 2,3: #arg @eq_prod_refl ] 785 @eq_addressing_mode_refl 786 |2: 787 #arg1_left normalize nodelta 788 @eq_prod_refl [*: @eq_addressing_mode_refl ] 789 |3: 790 #arg1_left normalize nodelta 791 >(eq_sum_refl …) [1: % 792 |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ] 793 |4: 794 #arg1_left normalize nodelta 795 @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] 796 ] 797 |14: 798 whd in ⊢ (??%?) 799 cases arg1 800 [ #arg1_left normalize nodelta 801 @eq_sum_refl 802 [1: #arg @eq_sum_refl 803 [1: #arg @eq_sum_refl 804 [1: #arg @eq_sum_refl 805 [1: #arg @eq_prod_refl 806 [*: @eq_addressing_mode_refl ] 807 |2: #arg @eq_prod_refl 808 [*: #arg @eq_addressing_mode_refl ] 809 ] 810 |2: #arg @eq_prod_refl 811 [*: #arg @eq_addressing_mode_refl ] 812 ] 813 |2: #arg @eq_prod_refl 814 [*: #arg @eq_addressing_mode_refl ] 815 ] 816 |2: #arg @eq_prod_refl 817 [*: #arg @eq_addressing_mode_refl ] 818 ] 819 |2: #arg1_right normalize nodelta 820 @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] 821 ] 822 |*: 823 whd in ⊢ (??%?) 824 cases arg1 825 [*: #arg1 >eq_sum_refl 826 [1,4: normalize @eq_addressing_mode_refl 827 |2,3,5,6: #arg @eq_prod_refl 828 [*: #arg @eq_addressing_mode_refl ] 829 ] 830 ] 831 ] 832 qed. 833 834 definition eq_instruction: instruction → instruction → bool ≝ 835 λi, j. 836 match i with 837 [ ACALL arg ⇒ 838 match j with 839 [ ACALL arg' ⇒ eq_addressing_mode arg arg' 840 | _ ⇒ false 841 ] 842 | LCALL arg ⇒ 843 match j with 844 [ LCALL arg' ⇒ eq_addressing_mode arg arg' 845 | _ ⇒ false 846 ] 847 | AJMP arg ⇒ 848 match j with 849 [ AJMP arg' ⇒ eq_addressing_mode arg arg' 850 | _ ⇒ false 851 ] 852 | LJMP arg ⇒ 853 match j with 854 [ LJMP arg' ⇒ eq_addressing_mode arg arg' 855 | _ ⇒ false 856 ] 857 | SJMP arg ⇒ 858 match j with 859 [ SJMP arg' ⇒ eq_addressing_mode arg arg' 860 | _ ⇒ false 861 ] 862 | JMP arg ⇒ 863 match j with 864 [ JMP arg' ⇒ eq_addressing_mode arg arg' 865 | _ ⇒ false 866 ] 867 | MOVC arg1 arg2 ⇒ 868 match j with 869 [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 870 | _ ⇒ false 871 ] 872 | RealInstruction instr ⇒ 873 match j with 874 [ RealInstruction instr' ⇒ eq_preinstruction instr instr' 875 | _ ⇒ false 876 ] 877 ]. 878 879 lemma eq_instruction_refl: 880 ∀i. eq_instruction i i = true. 881 #i cases i 882 [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl 883 |7: #arg1 #arg2 884 whd in ⊢ (??%?) 885 >eq_addressing_mode_refl 886 >eq_addressing_mode_refl 887 % 888 |8: #arg @eq_preinstruction_refl 889 ] 890 qed. 419 891 420 892 let rec vect_member
Note: See TracChangeset
for help on using the changeset viewer.