Changeset 2124 for src/ASM/ASM.ma
 Timestamp:
 Jun 27, 2012, 4:23:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2123 r2124 28 28  ADDR11: Word11 → addressing_mode 29 29  ADDR16: Word → addressing_mode. 30 31 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ 32 λa, b: addressing_mode. 33 match a with 34 [ DIRECT d ⇒ 35 match b with 36 [ DIRECT e ⇒ eq_bv ? d e 37  _ ⇒ false 38 ] 39  INDIRECT b' ⇒ 40 match b with 41 [ INDIRECT e ⇒ eq_b b' e 42  _ ⇒ false 43 ] 44  EXT_INDIRECT b' ⇒ 45 match b with 46 [ EXT_INDIRECT e ⇒ eq_b b' e 47  _ ⇒ false 48 ] 49  REGISTER bv ⇒ 50 match b with 51 [ REGISTER bv' ⇒ eq_bv ? bv bv' 52  _ ⇒ false 53 ] 54  ACC_A ⇒ match b with [ ACC_A ⇒ true  _ ⇒ false ] 55  ACC_B ⇒ match b with [ ACC_B ⇒ true  _ ⇒ false ] 56  DPTR ⇒ match b with [ DPTR ⇒ true  _ ⇒ false ] 57  DATA b' ⇒ 58 match b with 59 [ DATA e ⇒ eq_bv ? b' e 60  _ ⇒ false 61 ] 62  DATA16 w ⇒ 63 match b with 64 [ DATA16 e ⇒ eq_bv ? w e 65  _ ⇒ false 66 ] 67  ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true  _ ⇒ false ] 68  ACC_PC ⇒ match b with [ ACC_PC ⇒ true  _ ⇒ false ] 69  EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true  _ ⇒ false ] 70  INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true  _ ⇒ false ] 71  CARRY ⇒ match b with [ CARRY ⇒ true  _ ⇒ false ] 72  BIT_ADDR b' ⇒ 73 match b with 74 [ BIT_ADDR e ⇒ eq_bv ? b' e 75  _ ⇒ false 76 ] 77  N_BIT_ADDR b' ⇒ 78 match b with 79 [ N_BIT_ADDR e ⇒ eq_bv ? b' e 80  _ ⇒ false 81 ] 82  RELATIVE n ⇒ 83 match b with 84 [ RELATIVE e ⇒ eq_bv ? n e 85  _ ⇒ false 86 ] 87  ADDR11 w ⇒ 88 match b with 89 [ ADDR11 e ⇒ eq_bv ? w e 90  _ ⇒ false 91 ] 92  ADDR16 w ⇒ 93 match b with 94 [ ADDR16 e ⇒ eq_bv ? w e 95  _ ⇒ false 96 ] 97 ]. 98 99 lemma eq_addressing_mode_refl: 100 ∀a. eq_addressing_mode a a = true. 101 #a 102 cases a try #arg1 try #arg2 103 try @eq_bv_refl try @eq_b_refl 104 try normalize % 105 qed. 30 106 31 107 (* dpm: renamed register to registr to avoid clash with brian's types *) … … 161 237  VCons m he (tl: Vector addressing_mode_tag m) ⇒ 162 238 is_a he A ∨ is_in ? tl A ]. 239 240 definition is_in_cons_elim: 241 ∀len.∀hd,tl.∀m:addressing_mode 242 .is_in (S len) (hd:::tl) m → 243 (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)). 244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN; 245 cases (is_a hd am) in ISIN; /2/ 246 qed. 163 247 164 248 lemma is_a_to_mem_to_is_in: … … 425 509  NOP: preinstruction A. 426 510 511 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ 512 λi, j. 513 match i with 514 [ ADD arg1 arg2 ⇒ 515 match j with 516 [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 517  _ ⇒ false 518 ] 519  ADDC arg1 arg2 ⇒ 520 match j with 521 [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 522  _ ⇒ false 523 ] 524  SUBB arg1 arg2 ⇒ 525 match j with 526 [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 527  _ ⇒ false 528 ] 529  INC arg ⇒ 530 match j with 531 [ INC arg' ⇒ eq_addressing_mode arg arg' 532  _ ⇒ false 533 ] 534  DEC arg ⇒ 535 match j with 536 [ DEC arg' ⇒ eq_addressing_mode arg arg' 537  _ ⇒ false 538 ] 539  MUL arg1 arg2 ⇒ 540 match j with 541 [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 542  _ ⇒ false 543 ] 544  DIV arg1 arg2 ⇒ 545 match j with 546 [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 547  _ ⇒ false 548 ] 549  DA arg ⇒ 550 match j with 551 [ DA arg' ⇒ eq_addressing_mode arg arg' 552  _ ⇒ false 553 ] 554  JC arg ⇒ 555 match j with 556 [ JC arg' ⇒ eq_addressing_mode arg arg' 557  _ ⇒ false 558 ] 559  JNC arg ⇒ 560 match j with 561 [ JNC arg' ⇒ eq_addressing_mode arg arg' 562  _ ⇒ false 563 ] 564  JB arg1 arg2 ⇒ 565 match j with 566 [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 567  _ ⇒ false 568 ] 569  JNB arg1 arg2 ⇒ 570 match j with 571 [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 572  _ ⇒ false 573 ] 574  JBC arg1 arg2 ⇒ 575 match j with 576 [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 577  _ ⇒ false 578 ] 579  JZ arg ⇒ 580 match j with 581 [ JZ arg' ⇒ eq_addressing_mode arg arg' 582  _ ⇒ false 583 ] 584  JNZ arg ⇒ 585 match j with 586 [ JNZ arg' ⇒ eq_addressing_mode arg arg' 587  _ ⇒ false 588 ] 589  CJNE arg1 arg2 ⇒ 590 match j with 591 [ CJNE arg1' arg2' ⇒ 592 let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in 593 let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in 594 let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 595 arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 596  _ ⇒ false 597 ] 598  DJNZ arg1 arg2 ⇒ 599 match j with 600 [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 601  _ ⇒ false 602 ] 603  CLR arg ⇒ 604 match j with 605 [ CLR arg' ⇒ eq_addressing_mode arg arg' 606  _ ⇒ false 607 ] 608  CPL arg ⇒ 609 match j with 610 [ CPL arg' ⇒ eq_addressing_mode arg arg' 611  _ ⇒ false 612 ] 613  RL arg ⇒ 614 match j with 615 [ RL arg' ⇒ eq_addressing_mode arg arg' 616  _ ⇒ false 617 ] 618  RLC arg ⇒ 619 match j with 620 [ RLC arg' ⇒ eq_addressing_mode arg arg' 621  _ ⇒ false 622 ] 623  RR arg ⇒ 624 match j with 625 [ RR arg' ⇒ eq_addressing_mode arg arg' 626  _ ⇒ false 627 ] 628  RRC arg ⇒ 629 match j with 630 [ RRC arg' ⇒ eq_addressing_mode arg arg' 631  _ ⇒ false 632 ] 633  SWAP arg ⇒ 634 match j with 635 [ SWAP arg' ⇒ eq_addressing_mode arg arg' 636  _ ⇒ false 637 ] 638  SETB arg ⇒ 639 match j with 640 [ SETB arg' ⇒ eq_addressing_mode arg arg' 641  _ ⇒ false 642 ] 643  PUSH arg ⇒ 644 match j with 645 [ PUSH arg' ⇒ eq_addressing_mode arg arg' 646  _ ⇒ false 647 ] 648  POP arg ⇒ 649 match j with 650 [ POP arg' ⇒ eq_addressing_mode arg arg' 651  _ ⇒ false 652 ] 653  XCH arg1 arg2 ⇒ 654 match j with 655 [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 656  _ ⇒ false 657 ] 658  XCHD arg1 arg2 ⇒ 659 match j with 660 [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 661  _ ⇒ false 662 ] 663  RET ⇒ match j with [ RET ⇒ true  _ ⇒ false ] 664  RETI ⇒ match j with [ RETI ⇒ true  _ ⇒ false ] 665  NOP ⇒ match j with [ NOP ⇒ true  _ ⇒ false ] 666  MOVX arg ⇒ 667 match j with 668 [ MOVX arg' ⇒ 669 let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in 670 let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in 671 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 672 sum_eq arg arg' 673  _ ⇒ false 674 ] 675  XRL arg ⇒ 676 match j with 677 [ XRL arg' ⇒ 678 let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in 679 let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in 680 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 681 sum_eq arg arg' 682  _ ⇒ false 683 ] 684  ORL arg ⇒ 685 match j with 686 [ ORL arg' ⇒ 687 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in 688 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in 689 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in 690 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in 691 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 692 sum_eq arg arg' 693  _ ⇒ false 694 ] 695  ANL arg ⇒ 696 match j with 697 [ ANL arg' ⇒ 698 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in 699 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in 700 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in 701 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in 702 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in 703 sum_eq arg arg' 704  _ ⇒ false 705 ] 706  MOV arg ⇒ 707 match j with 708 [ MOV arg' ⇒ 709 let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in 710 let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in 711 let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in 712 let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in 713 let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in 714 let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in 715 let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in 716 let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in 717 let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in 718 let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in 719 let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in 720 sum_eq_5 arg arg' 721  _ ⇒ false 722 ] 723 ]. 724 725 lemma eq_preinstruction_refl: 726 ∀i. 727 eq_preinstruction i i = true. 728 #i cases i try #arg1 try #arg2 729 try @eq_addressing_mode_refl 730 [1,2,3,4,5,6,7,8,10,16,17,18,19,20: 731 whd in ⊢ (??%?); try % 732 >eq_addressing_mode_refl 733 >eq_addressing_mode_refl % 734 13,15: 735 whd in ⊢ (??%?); 736 cases arg1 737 [*: 738 #arg1_left normalize nodelta 739 >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] 740 ] 741 11,12: 742 whd in ⊢ (??%?); 743 cases arg1 744 [1: 745 #arg1_left normalize nodelta 746 >(eq_sum_refl …) 747 [1: %  2,3: #arg @eq_prod_refl ] 748 @eq_addressing_mode_refl 749 2: 750 #arg1_left normalize nodelta 751 @eq_prod_refl [*: @eq_addressing_mode_refl ] 752 3: 753 #arg1_left normalize nodelta 754 >(eq_sum_refl …) 755 [1: 756 % 757 2,3: 758 #arg @eq_prod_refl #arg @eq_addressing_mode_refl 759 ] 760 4: 761 #arg1_left normalize nodelta 762 @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] 763 ] 764 14: 765 whd in ⊢ (??%?); 766 cases arg1 767 [1: 768 #arg1_left normalize nodelta 769 @eq_sum_refl 770 [1: 771 #arg @eq_sum_refl 772 [1: 773 #arg @eq_sum_refl 774 [1: 775 #arg @eq_sum_refl 776 [1: 777 #arg @eq_prod_refl 778 [*: 779 @eq_addressing_mode_refl 780 ] 781 2: 782 #arg @eq_prod_refl 783 [*: 784 #arg @eq_addressing_mode_refl 785 ] 786 ] 787 2: 788 #arg @eq_prod_refl 789 [*: 790 #arg @eq_addressing_mode_refl 791 ] 792 ] 793 2: 794 #arg @eq_prod_refl 795 [*: 796 #arg @eq_addressing_mode_refl 797 ] 798 ] 799 2: 800 #arg @eq_prod_refl 801 [*: 802 #arg @eq_addressing_mode_refl 803 ] 804 ] 805 2: 806 #arg1_right normalize nodelta 807 @eq_prod_refl 808 [*: 809 #arg @eq_addressing_mode_refl 810 ] 811 ] 812 *: 813 whd in ⊢ (??%?); 814 cases arg1 815 [*: 816 #arg1 >eq_sum_refl 817 [1,4: 818 @eq_addressing_mode_refl 819 2,3,5,6: 820 #arg @eq_prod_refl 821 [*: 822 #arg @eq_addressing_mode_refl 823 ] 824 ] 825 ] 826 ] 827 qed. 828 427 829 inductive instruction: Type[0] ≝ 428 830  ACALL: [[addr11]] → instruction … … 437 839 coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ 438 840 RealInstruction on _p: preinstruction ? to instruction. 841 842 definition eq_instruction: instruction → instruction → bool ≝ 843 λi, j. 844 match i with 845 [ ACALL arg ⇒ 846 match j with 847 [ ACALL arg' ⇒ eq_addressing_mode arg arg' 848  _ ⇒ false 849 ] 850  LCALL arg ⇒ 851 match j with 852 [ LCALL arg' ⇒ eq_addressing_mode arg arg' 853  _ ⇒ false 854 ] 855  AJMP arg ⇒ 856 match j with 857 [ AJMP arg' ⇒ eq_addressing_mode arg arg' 858  _ ⇒ false 859 ] 860  LJMP arg ⇒ 861 match j with 862 [ LJMP arg' ⇒ eq_addressing_mode arg arg' 863  _ ⇒ false 864 ] 865  SJMP arg ⇒ 866 match j with 867 [ SJMP arg' ⇒ eq_addressing_mode arg arg' 868  _ ⇒ false 869 ] 870  JMP arg ⇒ 871 match j with 872 [ JMP arg' ⇒ eq_addressing_mode arg arg' 873  _ ⇒ false 874 ] 875  MOVC arg1 arg2 ⇒ 876 match j with 877 [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' 878  _ ⇒ false 879 ] 880  RealInstruction instr ⇒ 881 match j with 882 [ RealInstruction instr' ⇒ eq_preinstruction instr instr' 883  _ ⇒ false 884 ] 885 ]. 886 887 lemma eq_instruction_refl: 888 ∀i. eq_instruction i i = true. 889 #i cases i [*: #arg1 ] 890 try @eq_addressing_mode_refl 891 try @eq_preinstruction_refl 892 #arg2 whd in ⊢ (??%?); 893 >eq_addressing_mode_refl >eq_addressing_mode_refl % 894 qed. 895 896 lemma eq_instruction_to_eq: 897 ∀i1, i2: instruction. 898 eq_instruction i1 i2 = true → i1 ≃ i2. 899 #i1 #i2 900 cases i1 cases i2 cases daemon (* easy but tedious 901 [1,10,19,28,37,46: 902 #arg1 #arg2 903 whd in match (eq_instruction ??); 904 cases arg1 #subaddressing_mode 905 cases subaddressing_mode 906 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) 907 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) 908 try (normalize in ⊢ (% → ?); #absurd cases absurd @I) 909 #word11 #irrelevant 910 cases arg2 #subaddressing_mode 911 cases subaddressing_mode 912 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) 913 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) 914 try (normalize in ⊢ (% → ?); #absurd cases absurd @I) 915 #word11' #irrelevant normalize nodelta 916 #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *) 917 qed. 439 918 440 919 inductive pseudo_instruction: Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.