- Timestamp:
- Jun 27, 2012, 4:23:54 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 10 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] ≝ -
src/ASM/Arithmetic.ma
r2111 r2124 191 191 192 192 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. 193 194 axiom eq_bitvector_of_nat_to_eq: 195 ∀n,n1,n2. 196 n1 < 2^n → n2 < 2^n → 197 bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2. 193 198 194 199 lemma nat_of_bitvector_aux_injective: … … 707 712 add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q). 708 713 714 lemma add_bitvector_of_nat_Sm: 715 ∀n, m: nat. 716 add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = 717 bitvector_of_nat n (S m). 718 #n #m @add_bitvector_of_nat_plus 719 qed. 720 709 721 definition sign_bit : ∀n. BitVector n → bool ≝ 710 722 λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]. … … 729 741 ]. 730 742 743 example sub_minus_one_seven_eight: 744 ∀v: BitVector 7. 745 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 746 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 747 cases daemon. 748 qed. 749 750 axiom sub16_with_carry_overflow: 751 ∀left, right, result: BitVector 16. 752 ∀flags: BitVector 3. 753 ∀upper: BitVector 9. 754 ∀lower: BitVector 7. 755 sub_16_with_carry left right false = 〈result, flags〉 → 756 vsplit bool 9 7 result = 〈upper, lower〉 → 757 get_index_v bool 3 flags 2 ? = true → 758 upper = [[true; true; true; true; true; true; true; true; true]]. 759 // 760 qed. 761 762 axiom sub_16_to_add_16_8_0: 763 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 764 get_index' ? 2 0 flags = false → 765 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 766 v1 = add ? v2 (sign_extension (false:::v3)). 767 768 axiom sub_16_to_add_16_8_1: 769 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 770 get_index' ? 2 0 flags = true → 771 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 772 v1 = add ? v2 (sign_extension (true:::v3)). -
src/ASM/AssemblyProof.ma
r2122 r2124 37 37 qed. 38 38 39 (*CSC: move elsewhere *)40 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝41 λa, b: addressing_mode.42 match a with43 [ DIRECT d ⇒44 match b with45 [ DIRECT e ⇒ eq_bv ? d e46 | _ ⇒ false47 ]48 | INDIRECT b' ⇒49 match b with50 [ INDIRECT e ⇒ eq_b b' e51 | _ ⇒ false52 ]53 | EXT_INDIRECT b' ⇒54 match b with55 [ EXT_INDIRECT e ⇒ eq_b b' e56 | _ ⇒ false57 ]58 | REGISTER bv ⇒59 match b with60 [ REGISTER bv' ⇒ eq_bv ? bv bv'61 | _ ⇒ false62 ]63 | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]64 | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]65 | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]66 | DATA b' ⇒67 match b with68 [ DATA e ⇒ eq_bv ? b' e69 | _ ⇒ false70 ]71 | DATA16 w ⇒72 match b with73 [ DATA16 e ⇒ eq_bv ? w e74 | _ ⇒ false75 ]76 | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]77 | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]78 | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]79 | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]80 | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]81 | BIT_ADDR b' ⇒82 match b with83 [ BIT_ADDR e ⇒ eq_bv ? b' e84 | _ ⇒ false85 ]86 | N_BIT_ADDR b' ⇒87 match b with88 [ N_BIT_ADDR e ⇒ eq_bv ? b' e89 | _ ⇒ false90 ]91 | RELATIVE n ⇒92 match b with93 [ RELATIVE e ⇒ eq_bv ? n e94 | _ ⇒ false95 ]96 | ADDR11 w ⇒97 match b with98 [ ADDR11 e ⇒ eq_bv ? w e99 | _ ⇒ false100 ]101 | ADDR16 w ⇒102 match b with103 [ ADDR16 e ⇒ eq_bv ? w e104 | _ ⇒ false105 ]106 ].107 108 (*CSC: move elsewhere *)109 lemma eq_addressing_mode_refl:110 ∀a. eq_addressing_mode a a = true.111 #a112 cases a try #arg1 try #arg2113 try @eq_bv_refl try @eq_b_refl114 try normalize %115 qed.116 117 (*CSC: move elsewhere *)118 definition eq_sum:119 ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝120 λlt, rt, leq, req, left, right.121 match left with122 [ inl l ⇒123 match right with124 [ inl l' ⇒ leq l l'125 | _ ⇒ false126 ]127 | inr r ⇒128 match right with129 [ inr r' ⇒ req r r'130 | _ ⇒ false131 ]132 ].133 134 (*CSC: move elsewhere *)135 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝136 λlt, rt, leq, req, left, right.137 let 〈l, r〉 ≝ left in138 let 〈l', r'〉 ≝ right in139 leq l l' ∧ req r r'.140 141 (*CSC: move elsewhere *)142 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝143 λi, j.144 match i with145 [ ADD arg1 arg2 ⇒146 match j with147 [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'148 | _ ⇒ false149 ]150 | ADDC arg1 arg2 ⇒151 match j with152 [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'153 | _ ⇒ false154 ]155 | SUBB arg1 arg2 ⇒156 match j with157 [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'158 | _ ⇒ false159 ]160 | INC arg ⇒161 match j with162 [ INC arg' ⇒ eq_addressing_mode arg arg'163 | _ ⇒ false164 ]165 | DEC arg ⇒166 match j with167 [ DEC arg' ⇒ eq_addressing_mode arg arg'168 | _ ⇒ false169 ]170 | MUL arg1 arg2 ⇒171 match j with172 [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'173 | _ ⇒ false174 ]175 | DIV arg1 arg2 ⇒176 match j with177 [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'178 | _ ⇒ false179 ]180 | DA arg ⇒181 match j with182 [ DA arg' ⇒ eq_addressing_mode arg arg'183 | _ ⇒ false184 ]185 | JC arg ⇒186 match j with187 [ JC arg' ⇒ eq_addressing_mode arg arg'188 | _ ⇒ false189 ]190 | JNC arg ⇒191 match j with192 [ JNC arg' ⇒ eq_addressing_mode arg arg'193 | _ ⇒ false194 ]195 | JB arg1 arg2 ⇒196 match j with197 [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'198 | _ ⇒ false199 ]200 | JNB arg1 arg2 ⇒201 match j with202 [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'203 | _ ⇒ false204 ]205 | JBC arg1 arg2 ⇒206 match j with207 [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'208 | _ ⇒ false209 ]210 | JZ arg ⇒211 match j with212 [ JZ arg' ⇒ eq_addressing_mode arg arg'213 | _ ⇒ false214 ]215 | JNZ arg ⇒216 match j with217 [ JNZ arg' ⇒ eq_addressing_mode arg arg'218 | _ ⇒ false219 ]220 | CJNE arg1 arg2 ⇒221 match j with222 [ CJNE arg1' arg2' ⇒223 let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in224 let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in225 let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in226 arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'227 | _ ⇒ false228 ]229 | DJNZ arg1 arg2 ⇒230 match j with231 [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'232 | _ ⇒ false233 ]234 | CLR arg ⇒235 match j with236 [ CLR arg' ⇒ eq_addressing_mode arg arg'237 | _ ⇒ false238 ]239 | CPL arg ⇒240 match j with241 [ CPL arg' ⇒ eq_addressing_mode arg arg'242 | _ ⇒ false243 ]244 | RL arg ⇒245 match j with246 [ RL arg' ⇒ eq_addressing_mode arg arg'247 | _ ⇒ false248 ]249 | RLC arg ⇒250 match j with251 [ RLC arg' ⇒ eq_addressing_mode arg arg'252 | _ ⇒ false253 ]254 | RR arg ⇒255 match j with256 [ RR arg' ⇒ eq_addressing_mode arg arg'257 | _ ⇒ false258 ]259 | RRC arg ⇒260 match j with261 [ RRC arg' ⇒ eq_addressing_mode arg arg'262 | _ ⇒ false263 ]264 | SWAP arg ⇒265 match j with266 [ SWAP arg' ⇒ eq_addressing_mode arg arg'267 | _ ⇒ false268 ]269 | SETB arg ⇒270 match j with271 [ SETB arg' ⇒ eq_addressing_mode arg arg'272 | _ ⇒ false273 ]274 | PUSH arg ⇒275 match j with276 [ PUSH arg' ⇒ eq_addressing_mode arg arg'277 | _ ⇒ false278 ]279 | POP arg ⇒280 match j with281 [ POP arg' ⇒ eq_addressing_mode arg arg'282 | _ ⇒ false283 ]284 | XCH arg1 arg2 ⇒285 match j with286 [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'287 | _ ⇒ false288 ]289 | XCHD arg1 arg2 ⇒290 match j with291 [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'292 | _ ⇒ false293 ]294 | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]295 | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]296 | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]297 | MOVX arg ⇒298 match j with299 [ MOVX arg' ⇒300 let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in301 let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in302 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in303 sum_eq arg arg'304 | _ ⇒ false305 ]306 | XRL arg ⇒307 match j with308 [ XRL arg' ⇒309 let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in310 let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in311 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in312 sum_eq arg arg'313 | _ ⇒ false314 ]315 | ORL arg ⇒316 match j with317 [ ORL arg' ⇒318 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in319 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in320 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in321 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in322 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in323 sum_eq arg arg'324 | _ ⇒ false325 ]326 | ANL arg ⇒327 match j with328 [ ANL arg' ⇒329 let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in330 let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in331 let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in332 let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in333 let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in334 sum_eq arg arg'335 | _ ⇒ false336 ]337 | MOV arg ⇒338 match j with339 [ MOV arg' ⇒340 let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in341 let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in342 let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in343 let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in344 let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in345 let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in346 let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in347 let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in348 let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in349 let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in350 let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in351 sum_eq_5 arg arg'352 | _ ⇒ false353 ]354 ].355 356 (*CSC: move elsewhere *)357 lemma eq_sum_refl:358 ∀A, B: Type[0].359 ∀leq, req.360 ∀s.361 ∀leq_refl: (∀t. leq t t = true).362 ∀req_refl: (∀u. req u u = true).363 eq_sum A B leq req s s = true.364 #A #B #leq #req #s #leq_refl #req_refl365 cases s assumption366 qed.367 368 (*CSC: move elsewhere *)369 lemma eq_prod_refl:370 ∀A, B: Type[0].371 ∀leq, req.372 ∀s.373 ∀leq_refl: (∀t. leq t t = true).374 ∀req_refl: (∀u. req u u = true).375 eq_prod A B leq req s s = true.376 #A #B #leq #req #s #leq_refl #req_refl377 cases s378 whd in ⊢ (? → ? → ??%?);379 #l #r380 >leq_refl @req_refl381 qed.382 383 (*CSC: move elsewhere *)384 lemma eq_preinstruction_refl:385 ∀i.386 eq_preinstruction i i = true.387 #i cases i try #arg1 try #arg2388 try @eq_addressing_mode_refl389 [1,2,3,4,5,6,7,8,10,16,17,18,19,20:390 whd in ⊢ (??%?); try %391 >eq_addressing_mode_refl392 >eq_addressing_mode_refl %393 |13,15:394 whd in ⊢ (??%?);395 cases arg1396 [*:397 #arg1_left normalize nodelta398 >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]399 ]400 |11,12:401 whd in ⊢ (??%?);402 cases arg1403 [1:404 #arg1_left normalize nodelta405 >(eq_sum_refl …)406 [1: % | 2,3: #arg @eq_prod_refl ]407 @eq_addressing_mode_refl408 |2:409 #arg1_left normalize nodelta410 @eq_prod_refl [*: @eq_addressing_mode_refl ]411 |3:412 #arg1_left normalize nodelta413 >(eq_sum_refl …)414 [1:415 %416 |2,3:417 #arg @eq_prod_refl #arg @eq_addressing_mode_refl418 ]419 |4:420 #arg1_left normalize nodelta421 @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]422 ]423 |14:424 whd in ⊢ (??%?);425 cases arg1426 [1:427 #arg1_left normalize nodelta428 @eq_sum_refl429 [1:430 #arg @eq_sum_refl431 [1:432 #arg @eq_sum_refl433 [1:434 #arg @eq_sum_refl435 [1:436 #arg @eq_prod_refl437 [*:438 @eq_addressing_mode_refl439 ]440 |2:441 #arg @eq_prod_refl442 [*:443 #arg @eq_addressing_mode_refl444 ]445 ]446 |2:447 #arg @eq_prod_refl448 [*:449 #arg @eq_addressing_mode_refl450 ]451 ]452 |2:453 #arg @eq_prod_refl454 [*:455 #arg @eq_addressing_mode_refl456 ]457 ]458 |2:459 #arg @eq_prod_refl460 [*:461 #arg @eq_addressing_mode_refl462 ]463 ]464 |2:465 #arg1_right normalize nodelta466 @eq_prod_refl467 [*:468 #arg @eq_addressing_mode_refl469 ]470 ]471 |*:472 whd in ⊢ (??%?);473 cases arg1474 [*:475 #arg1 >eq_sum_refl476 [1,4:477 @eq_addressing_mode_refl478 |2,3,5,6:479 #arg @eq_prod_refl480 [*:481 #arg @eq_addressing_mode_refl482 ]483 ]484 ]485 ]486 qed.487 488 (*CSC: move elsewhere *)489 definition eq_instruction: instruction → instruction → bool ≝490 λi, j.491 match i with492 [ ACALL arg ⇒493 match j with494 [ ACALL arg' ⇒ eq_addressing_mode arg arg'495 | _ ⇒ false496 ]497 | LCALL arg ⇒498 match j with499 [ LCALL arg' ⇒ eq_addressing_mode arg arg'500 | _ ⇒ false501 ]502 | AJMP arg ⇒503 match j with504 [ AJMP arg' ⇒ eq_addressing_mode arg arg'505 | _ ⇒ false506 ]507 | LJMP arg ⇒508 match j with509 [ LJMP arg' ⇒ eq_addressing_mode arg arg'510 | _ ⇒ false511 ]512 | SJMP arg ⇒513 match j with514 [ SJMP arg' ⇒ eq_addressing_mode arg arg'515 | _ ⇒ false516 ]517 | JMP arg ⇒518 match j with519 [ JMP arg' ⇒ eq_addressing_mode arg arg'520 | _ ⇒ false521 ]522 | MOVC arg1 arg2 ⇒523 match j with524 [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'525 | _ ⇒ false526 ]527 | RealInstruction instr ⇒528 match j with529 [ RealInstruction instr' ⇒ eq_preinstruction instr instr'530 | _ ⇒ false531 ]532 ].533 534 (*CSC: move elsewhere *)535 lemma eq_instruction_refl:536 ∀i. eq_instruction i i = true.537 #i cases i [*: #arg1 ]538 try @eq_addressing_mode_refl539 try @eq_preinstruction_refl540 #arg2 whd in ⊢ (??%?);541 >eq_addressing_mode_refl >eq_addressing_mode_refl %542 qed.543 544 (*CSC: in is_a_to_mem_to_is_in use vect_member in place of mem … *)545 definition vect_member ≝546 λA,n,eq,v,a. mem A eq (S n) v a.547 548 (*CSC: move elsewhere*)549 definition is_in_cons_elim:550 ∀len.∀hd,tl.∀m:addressing_mode551 .is_in (S len) (hd:::tl) m →552 (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).553 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;554 cases (is_a hd am) in ISIN; /2/555 qed.556 557 (*CSC: move elsewhere*)558 lemma prod_eq_left:559 ∀A: Type[0].560 ∀p, q, r: A.561 p = q → 〈p, r〉 = 〈q, r〉.562 #A #p #q #r #hyp563 destruct %564 qed.565 566 (*CSC: move elsewhere*)567 lemma prod_eq_right:568 ∀A: Type[0].569 ∀p, q, r: A.570 p = q → 〈r, p〉 = 〈r, q〉.571 #A #p #q #r #hyp572 destruct %573 qed.574 575 39 let rec encoding_check 576 40 (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) … … 583 47 hd = byte ∧ encoding_check code_memory new_pc final_pc tl 584 48 ]. 585 586 (*CSC: move elsewhere *)587 lemma add_bitvector_of_nat_Sm:588 ∀n, m: nat.589 add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =590 bitvector_of_nat n (S m).591 #n #m @add_bitvector_of_nat_plus592 qed.593 49 594 50 lemma encoding_check_append: … … 622 78 ] 623 79 ] 624 qed.625 626 (*CSC: move elsewhere*)627 lemma destruct_bug_fix_1:628 ∀n: nat.629 S n = 0 → False.630 #n #absurd destruct(absurd)631 qed.632 633 (*CSC: move elsewhere*)634 lemma destruct_bug_fix_2:635 ∀m, n: nat.636 S m = S n → m = n.637 #m #n #refl destruct %638 qed.639 640 (*CSC: move elsewhere*)641 definition bitvector_3_cases:642 ∀b: BitVector 3.643 ∃l, c, r: bool.644 b ≃ [[l; c; r]].645 #b646 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))647 [1:648 #absurd @⊥ -b @(destruct_bug_fix_1 2)649 >absurd %650 |2:651 #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}652 cut (n = 2)653 [1:654 @destruct_bug_fix_2655 >size_refl %656 |2:657 #n_refl >n_refl in tl; #V658 @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))659 [1:660 #absurd @⊥ -V @(destruct_bug_fix_1 1)661 >absurd %662 |2:663 #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}664 cut (n' = 1)665 [1:666 @destruct_bug_fix_2 >size_refl' %667 |2:668 #n_refl' >n_refl' in tl'; #V'669 @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))670 [1:671 #absurd @⊥ -V' @(destruct_bug_fix_1 0)672 >absurd %673 |2:674 #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}675 cut (n'' = 0)676 [1:677 @destruct_bug_fix_2 >size_refl'' %678 |2:679 #n_refl'' >n_refl'' in tl''; #tl'''680 >(Vector_O … tl''') %681 ]682 ]683 ]684 ]685 ]686 ]687 qed.688 689 (*CSC: move elsewhere*)690 lemma bitvector_3_elim_prop:691 ∀P: BitVector 3 → Prop.692 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →693 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →694 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.695 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9696 cases (bitvector_3_cases … H9) #l #assm cases assm697 -assm #c #assm cases assm698 -assm #r #assm cases assm destruct699 cases l cases c cases r assumption700 80 qed. 701 81 … … 750 130 fetch_many code_memory final_pc pc' tl) 751 131 ]. 752 753 (*CSC: move elsewhere*)754 lemma option_destruct_Some:755 ∀A: Type[0].756 ∀a, b: A.757 Some A a = Some A b → a = b.758 #A #a #b #EQ759 destruct %760 qed.761 762 (*CSC: move elsewhere*)763 lemma eq_instruction_to_eq:764 ∀i1, i2: instruction.765 eq_instruction i1 i2 = true → i1 ≃ i2.766 #i1 #i2767 cases i1 cases i2 cases daemon (* easy but tedious768 [1,10,19,28,37,46:769 #arg1 #arg2770 whd in match (eq_instruction ??);771 cases arg1 #subaddressing_mode772 cases subaddressing_mode773 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)774 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)775 try (normalize in ⊢ (% → ?); #absurd cases absurd @I)776 #word11 #irrelevant777 cases arg2 #subaddressing_mode778 cases subaddressing_mode779 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)780 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)781 try (normalize in ⊢ (% → ?); #absurd cases absurd @I)782 #word11' #irrelevant normalize nodelta783 #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)784 qed.785 132 786 133 lemma fetch_assembly_pseudo': … … 1429 776 ticks_of0 program sigma policy ppc fetched. 1430 777 1431 (*CSC: move elsewhere*)1432 lemma eq_rect_Type1_r:1433 ∀A: Type[1].1434 ∀a: A.1435 ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.1436 #A #a #P #H #x #p1437 generalize in match H;1438 generalize in match P;1439 cases p //1440 qed.1441 1442 778 (* 1443 779 lemma blah: … … 1569 905 *) 1570 906 1571 (*CSC: move elsewhere*)1572 lemma Some_Some_elim:1573 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.1574 #T #x #y #P #H #K @H @option_destruct_Some //1575 qed.1576 1577 (*CSC: move elsewhere*)1578 lemma pair_destruct_right:1579 ∀A: Type[0].1580 ∀B: Type[0].1581 ∀a, c: A.1582 ∀b, d: B.1583 〈a, b〉 = 〈c, d〉 → b = d.1584 #A #B #a #b #c #d //1585 qed.1586 1587 907 (*CSC: ???*) 1588 908 (* XXX: we need a precondition here stating that the PPC is within the … … 1633 953 @pair_elim #lbl #instr #nth_refl normalize nodelta 1634 954 #G cases (pair_destruct_right ?????? G) % 1635 qed.1636 1637 (*CSC: move elsewhere*)1638 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.1639 /2/1640 955 qed. 1641 956 -
src/ASM/AssemblyProofSplit.ma
r2122 r2124 170 170 qed. 171 171 172 (*CSC: move elsewhere*)173 lemma pair_replace:174 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →175 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').176 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //177 qed.178 179 172 lemma get_arg_8_set_program_counter: 180 173 ∀M: Type[0]. … … 327 320 qed. 328 321 329 (*CSC: move elsewhere*)330 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.331 #P #A #a #abs destruct332 qed.333 334 322 (* 335 323 lemma pi1_let_commute: … … 360 348 include alias "basics/logic.ma". 361 349 include alias "ASM/BitVectorTrie.ma". 362 363 (*CSC: move elsewhere*)364 lemma jmpair_as_replace:365 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.366 ∀EQ:c ≃ 〈a,b〉.367 P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).368 [2:369 >EQc @EQ370 |1:371 #A #B #T #P #a #b372 #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ373 letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]374 change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;375 @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta376 -EQ cases c in f; normalize //377 ]378 qed.379 380 (*CSC: move elsewhere*)381 lemma if_then_else_replace:382 ∀T: Type[0].383 ∀P: T → Prop.384 ∀t1, t2: T.385 ∀c, c', c'': bool.386 c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).387 #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm388 assumption389 qed.390 350 391 351 lemma fetch_many_singleton: … … 398 358 #fetch_many_assm whd in fetch_many_assm; 399 359 cases (eq_bv_eq … fetch_many_assm) assumption 400 qed.401 402 (*CSC: move elsewhere*)403 lemma refl_to_jmrefl:404 ∀a: Type[0].405 ∀l, r: a.406 l = r → l ≃ r.407 #a #l #r #refl destruct %408 360 qed. 409 361 -
src/ASM/BitVector.ma
r2122 r2124 236 236 String. 237 237 238 example sub_minus_one_seven_eight: 239 ∀v: BitVector 7. 240 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 241 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 242 cases daemon. 243 qed. 244 245 axiom sub16_with_carry_overflow: 246 ∀left, right, result: BitVector 16. 247 ∀flags: BitVector 3. 248 ∀upper: BitVector 9. 249 ∀lower: BitVector 7. 250 sub_16_with_carry left right false = 〈result, flags〉 → 251 vsplit bool 9 7 result = 〈upper, lower〉 → 252 get_index_v bool 3 flags 2 ? = true → 253 upper = [[true; true; true; true; true; true; true; true; true]]. 254 // 255 qed. 256 257 axiom sub_16_to_add_16_8_0: 258 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 259 get_index' ? 2 0 flags = false → 260 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 261 v1 = add ? v2 (sign_extension (false:::v3)). 262 263 axiom sub_16_to_add_16_8_1: 264 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 265 get_index' ? 2 0 flags = true → 266 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 267 v1 = add ? v2 (sign_extension (true:::v3)). 238 definition bitvector_3_cases: 239 ∀b: BitVector 3. 240 ∃l, c, r: bool. 241 b ≃ [[l; c; r]]. 242 #b 243 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 244 [1: 245 #absurd @⊥ -b @(destruct_bug_fix_1 2) 246 >absurd % 247 |2: 248 #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} 249 cut (n = 2) 250 [1: 251 @destruct_bug_fix_2 252 >size_refl % 253 |2: 254 #n_refl >n_refl in tl; #V 255 @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) 256 [1: 257 #absurd @⊥ -V @(destruct_bug_fix_1 1) 258 >absurd % 259 |2: 260 #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} 261 cut (n' = 1) 262 [1: 263 @destruct_bug_fix_2 >size_refl' % 264 |2: 265 #n_refl' >n_refl' in tl'; #V' 266 @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) 267 [1: 268 #absurd @⊥ -V' @(destruct_bug_fix_1 0) 269 >absurd % 270 |2: 271 #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} 272 cut (n'' = 0) 273 [1: 274 @destruct_bug_fix_2 >size_refl'' % 275 |2: 276 #n_refl'' >n_refl'' in tl''; #tl''' 277 >(Vector_O … tl''') % 278 ] 279 ] 280 ] 281 ] 282 ] 283 ] 284 qed. 285 286 lemma bitvector_3_elim_prop: 287 ∀P: BitVector 3 → Prop. 288 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → 289 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → 290 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 291 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 292 cases (bitvector_3_cases … H9) #l #assm cases assm 293 -assm #c #assm cases assm 294 -assm #r #assm cases assm destruct 295 cases l cases c cases r assumption 296 qed. -
src/ASM/Fetch.ma
r2119 r2124 17 17 λpc: Word. 18 18 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. 19 20 (*CSC: move elsewhere *)21 axiom eq_bitvector_of_nat_to_eq:22 ∀n,n1,n2.23 n1 < 2^n → n2 < 2^n →24 bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.25 26 discriminator Prod.27 19 28 20 definition load_code_memory0: -
src/ASM/Interpret.ma
r2108 r2124 957 957 qed. 958 958 959 discriminator Prod.960 961 959 definition compute_target_of_unconditional_jump: 962 960 ∀program_counter: Word. -
src/ASM/StatusProofs.ma
r2032 r2124 344 344 program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s. 345 345 346 (* XXX: to be moved elsewhere *)347 346 lemma program_counter_set_arg_8: 348 347 ∀m, cm, s, addr, v. -
src/ASM/Util.ma
r2123 r2124 1478 1478 qed. 1479 1479 1480 (*CSC: just a synonim, get rid of it!*) 1481 lemma Some_eq: 1482 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y ≝ option_destruct_Some. 1483 1480 1484 lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2. 1481 1485 s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2). … … 1483 1487 qed. 1484 1488 1485 lemma Some_eq:1486 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.1487 #T #x #y #H @option_destruct_Some @H1488 qed.1489 1490 1489 lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?. 1491 1490 #A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS') … … 1494 1493 coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝ 1495 1494 not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?. 1495 1496 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 1497 #P #A #a #abs destruct 1498 qed. 1499 1500 discriminator Prod. 1501 1502 lemma pair_replace: 1503 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → 1504 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). 1505 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // 1506 qed. 1507 1508 lemma jmpair_as_replace: 1509 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c. 1510 ∀EQ:c ≃ 〈a,b〉. 1511 P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')). 1512 [2: 1513 >EQc @EQ 1514 |1: 1515 #A #B #T #P #a #b 1516 #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ 1517 letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ] 1518 change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ; 1519 @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta 1520 -EQ cases c in f; normalize // 1521 ] 1522 qed. 1523 1524 lemma if_then_else_replace: 1525 ∀T: Type[0]. 1526 ∀P: T → Prop. 1527 ∀t1, t2: T. 1528 ∀c, c', c'': bool. 1529 c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2). 1530 #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm 1531 assumption 1532 qed. 1533 1534 lemma refl_to_jmrefl: 1535 ∀a: Type[0]. 1536 ∀l, r: a. 1537 l = r → l ≃ r. 1538 #a #l #r #refl destruct % 1539 qed. 1540 1541 lemma prod_eq_left: 1542 ∀A: Type[0]. 1543 ∀p, q, r: A. 1544 p = q → 〈p, r〉 = 〈q, r〉. 1545 #A #p #q #r #hyp 1546 destruct % 1547 qed. 1548 1549 lemma prod_eq_right: 1550 ∀A: Type[0]. 1551 ∀p, q, r: A. 1552 p = q → 〈r, p〉 = 〈r, q〉. 1553 #A #p #q #r #hyp 1554 destruct % 1555 qed. 1556 1557 lemma destruct_bug_fix_1: 1558 ∀n: nat. 1559 S n = 0 → False. 1560 #n #absurd destruct(absurd) 1561 qed. 1562 1563 lemma destruct_bug_fix_2: 1564 ∀m, n: nat. 1565 S m = S n → m = n. 1566 #m #n #refl destruct % 1567 qed. 1568 1569 lemma eq_rect_Type1_r: 1570 ∀A: Type[1]. 1571 ∀a: A. 1572 ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 1573 #A #a #P #H #x #p 1574 generalize in match H; 1575 generalize in match P; 1576 cases p // 1577 qed. 1578 1579 lemma Some_Some_elim: 1580 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P. 1581 #T #x #y #P #H #K @H @option_destruct_Some // 1582 qed. 1583 1584 lemma pair_destruct_right: 1585 ∀A: Type[0]. 1586 ∀B: Type[0]. 1587 ∀a, c: A. 1588 ∀b, d: B. 1589 〈a, b〉 = 〈c, d〉 → b = d. 1590 #A #B #a #b #c #d // 1591 qed. 1592 1593 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. 1594 /2/ 1595 qed. 1596 1597 definition eq_sum: 1598 ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ 1599 λlt, rt, leq, req, left, right. 1600 match left with 1601 [ inl l ⇒ 1602 match right with 1603 [ inl l' ⇒ leq l l' 1604 | _ ⇒ false 1605 ] 1606 | inr r ⇒ 1607 match right with 1608 [ inr r' ⇒ req r r' 1609 | _ ⇒ false 1610 ] 1611 ]. 1612 1613 lemma eq_sum_refl: 1614 ∀A, B: Type[0]. 1615 ∀leq, req. 1616 ∀s. 1617 ∀leq_refl: (∀t. leq t t = true). 1618 ∀req_refl: (∀u. req u u = true). 1619 eq_sum A B leq req s s = true. 1620 #A #B #leq #req #s #leq_refl #req_refl 1621 cases s assumption 1622 qed. 1623 1624 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ 1625 λlt, rt, leq, req, left, right. 1626 let 〈l, r〉 ≝ left in 1627 let 〈l', r'〉 ≝ right in 1628 leq l l' ∧ req r r'. 1629 1630 lemma eq_prod_refl: 1631 ∀A, B: Type[0]. 1632 ∀leq, req. 1633 ∀s. 1634 ∀leq_refl: (∀t. leq t t = true). 1635 ∀req_refl: (∀u. req u u = true). 1636 eq_prod A B leq req s s = true. 1637 #A #B #leq #req #s #leq_refl #req_refl 1638 cases s 1639 whd in ⊢ (? → ? → ??%?); 1640 #l #r 1641 >leq_refl @req_refl 1642 qed. 1496 1643 1497 1644 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. -
src/ASM/Vector.ma
r2122 r2124 223 223 vsplit' A m n v. 224 224 225 lemma vsplit_ok:226 ∀A: Type[0].227 ∀m, n: nat.228 ∀v: Vector A (m + n).229 ∀upper: Vector A m.230 ∀lower: Vector A n.231 〈upper, lower〉 = vsplit A m n v →232 upper @@ lower = v.233 #A #m #n #v #upper #lower234 cases daemon235 qed.236 237 225 lemma vsplit_zero: 238 226 ∀A,m. … … 376 364 377 365 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 366 367 368 lemma vsplit_ok: 369 ∀A: Type[0]. 370 ∀m, n: nat. 371 ∀v: Vector A (m + n). 372 ∀upper: Vector A m. 373 ∀lower: Vector A n. 374 〈upper, lower〉 = vsplit A m n v → 375 upper @@ lower = v. 376 #A #m #n #v #upper #lower 377 cases daemon 378 qed. 378 379 379 380 lemma vector_append_zero:
Note: See TracChangeset
for help on using the changeset viewer.