Changeset 991
 Timestamp:
 Jun 17, 2011, 5:17:43 PM (8 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.