Changeset 1909 for src/ASM/Interpret.ma
- Timestamp:
- Apr 27, 2012, 10:59:03 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1710 r1909 144 144 | LCALL _ ⇒ cl_call 145 145 | JMP _ ⇒ cl_call 146 | AJMP _ ⇒ cl_ jump147 | LJMP _ ⇒ cl_ jump148 | SJMP _ ⇒ cl_ jump146 | AJMP _ ⇒ cl_other 147 | LJMP _ ⇒ cl_other 148 | SJMP _ ⇒ cl_other 149 149 | _ ⇒ cl_other 150 150 ]. … … 609 609 discriminator Prod. 610 610 611 definition compute_target_of_unconditional_jump: 612 ∀program_counter: Word. 613 ∀i: instruction. 614 Word ≝ 615 λprogram_counter. 616 λi. 617 match i with 618 [ LJMP addr ⇒ 619 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with 620 [ ADDR16 a ⇒ λaddr16: True. a 621 | _ ⇒ λother: False. ⊥ 622 ] (subaddressing_modein … addr) 623 | SJMP addr ⇒ 624 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 625 [ RELATIVE r ⇒ λrelative: True. 626 let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in 627 new_pc 628 | _ ⇒ λother: False. ⊥ 629 ] (subaddressing_modein … addr) 630 | AJMP addr ⇒ 631 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 632 [ ADDR11 a ⇒ λaddr11: True. 633 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in 634 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 635 let bit ≝ get_index' ? O ? nl in 636 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 637 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 638 let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in 639 new_pc 640 | _ ⇒ λother: False. ⊥ 641 ] (subaddressing_modein … addr) 642 | _ ⇒ zero ? 643 ]. 644 // 645 qed. 646 647 definition is_unconditional_jump: 648 instruction → bool ≝ 649 λi: instruction. 650 match i with 651 [ LJMP _ ⇒ true 652 | SJMP _ ⇒ true 653 | AJMP _ ⇒ true 654 | _ ⇒ false 655 ]. 656 657 let rec member_addressing_mode_tag 658 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) 659 on v: Prop ≝ 660 match v with 661 [ VEmpty ⇒ False 662 | VCons n' hd tl ⇒ 663 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a 664 ]. 665 666 lemma is_a_decidable: 667 ∀hd. 668 ∀element. 669 is_a hd element = true ∨ is_a hd element = false. 670 #hd #element // 671 qed. 672 673 lemma mem_decidable: 674 ∀n: nat. 675 ∀v: Vector addressing_mode_tag n. 676 ∀element: addressing_mode_tag. 677 mem … eq_a n v element = true ∨ 678 mem … eq_a … v element = false. 679 #n #v #element // 680 qed. 681 682 lemma eq_a_elim: 683 ∀tag. 684 ∀hd. 685 ∀P: bool → Prop. 686 (tag = hd → P (true)) → 687 (tag ≠ hd → P (false)) → 688 P (eq_a tag hd). 689 #tag #hd #P 690 cases tag 691 cases hd 692 #true_hyp #false_hyp 693 try @false_hyp 694 try @true_hyp 695 try % 696 #absurd destruct(absurd) 697 qed. 698 699 lemma is_a_true_to_is_in: 700 ∀n: nat. 701 ∀x: addressing_mode. 702 ∀tag: addressing_mode_tag. 703 ∀supervector: Vector addressing_mode_tag n. 704 mem addressing_mode_tag eq_a n supervector tag → 705 is_a tag x = true → 706 is_in … supervector x. 707 #n #x #tag #supervector 708 elim supervector 709 [1: 710 #absurd cases absurd 711 |2: 712 #n' #hd #tl #inductive_hypothesis 713 whd in match (mem … eq_a (S n') (hd:::tl) tag); 714 @eq_a_elim normalize nodelta 715 [1: 716 #tag_hd_eq #irrelevant 717 whd in match (is_in (S n') (hd:::tl) x); 718 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta 719 @I 720 |2: 721 #tag_hd_neq 722 whd in match (is_in (S n') (hd:::tl) x); 723 change with ( 724 mem … eq_a n' tl tag) 725 in match (fold_right … n' ? false tl); 726 #mem_hyp #is_a_hyp 727 cases(is_a hd x) 728 [1: 729 normalize nodelta // 730 |2: 731 normalize nodelta 732 @inductive_hypothesis assumption 733 ] 734 ] 735 ] 736 qed. 737 738 lemma is_in_subvector_is_in_supervector: 739 ∀m, n: nat. 740 ∀subvector: Vector addressing_mode_tag m. 741 ∀supervector: Vector addressing_mode_tag n. 742 ∀element: addressing_mode. 743 subvector_with … eq_a subvector supervector → 744 is_in m subvector element → is_in n supervector element. 745 #m #n #subvector #supervector #element 746 elim subvector 747 [1: 748 #subvector_with_proof #is_in_proof 749 cases is_in_proof 750 |2: 751 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof 752 whd in match (is_in … (hd':::tl') element); 753 cases (is_a_decidable hd' element) 754 [1: 755 #is_a_true >is_a_true 756 #irrelevant 757 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; 758 @(is_a_true_to_is_in … is_a_true) 759 lapply(subvector_with_proof) 760 cases(mem … eq_a n supervector hd') // 761 |2: 762 #is_a_false >is_a_false normalize nodelta 763 #assm 764 @inductive_hypothesis 765 [1: 766 generalize in match subvector_with_proof; 767 whd in match (subvector_with … eq_a (hd':::tl') supervector); 768 cases(mem_decidable n supervector hd') 769 [1: 770 #mem_true >mem_true normalize nodelta 771 #assm assumption 772 |2: 773 #mem_false >mem_false #absurd 774 cases absurd 775 ] 776 |2: 777 assumption 778 ] 779 ] 780 ] 781 qed. 782 783 let rec subaddressing_mode_elim_type 784 (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) 785 (Q: addressing_mode → T → Prop) 786 (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) 787 (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) 788 (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) 789 (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) 790 (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) 791 (p_acc_a: is_in m fixed_v ACC_A → T) 792 (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) 793 (p_acc_b: is_in m fixed_v ACC_B → T) 794 (p_dptr: is_in m fixed_v DPTR → T) 795 (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) 796 (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) 797 (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) 798 (p_acc_pc: is_in m fixed_v ACC_PC → T) 799 (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) 800 (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) 801 (p_carry: is_in m fixed_v CARRY → T) 802 (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) 803 (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) 804 (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) 805 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) 806 on v: Prop ≝ 807 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with 808 [ VEmpty ⇒ λm_refl. λv_refl. 809 ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. 810 Q addr ( 811 match addr return λx: addressing_mode. is_in … fixed_v x → T with 812 [ ADDR11 x ⇒ p_addr11 x 813 | ADDR16 x ⇒ p_addr16 x 814 | DIRECT x ⇒ p_direct x 815 | INDIRECT x ⇒ p_indirect x 816 | EXT_INDIRECT x ⇒ p_ext_indirect x 817 | ACC_A ⇒ p_acc_a 818 | REGISTER x ⇒ p_register x 819 | ACC_B ⇒ p_acc_b 820 | DPTR ⇒ p_dptr 821 | DATA x ⇒ p_data x 822 | DATA16 x ⇒ p_data16 x 823 | ACC_DPTR ⇒ p_acc_dptr 824 | ACC_PC ⇒ p_acc_pc 825 | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr 826 | INDIRECT_DPTR ⇒ p_indirect_dptr 827 | CARRY ⇒ p_carry 828 | BIT_ADDR x ⇒ p_bit_addr x 829 | N_BIT_ADDR x ⇒ p_n_bit_addr x 830 | RELATIVE x ⇒ p_relative x 831 ] p) 832 | VCons n' hd tl ⇒ λm_refl. λv_refl. 833 let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 834 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a 835 p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 836 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry 837 p_bit_addr p_n_bit_addr p_relative n' tl ? 838 in 839 match hd return λa: addressing_mode_tag. a = hd → ? with 840 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call 841 | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call 842 | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call 843 | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call 844 | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call 845 | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call 846 | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call 847 | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call 848 | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call 849 | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call 850 | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call 851 | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call 852 | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call 853 | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call 854 | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call 855 | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call 856 | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call 857 | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call 858 | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call 859 ] (refl … hd) 860 ] (refl … n) (refl_jmeq … v). 861 [20: 862 generalize in match proof; destruct 863 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 864 cases (mem … eq_a m fixed_v hd) normalize nodelta 865 [1: 866 whd in match (subvector_with … eq_a tl fixed_v); 867 #assm assumption 868 |2: 869 normalize in ⊢ (% → ?); 870 #absurd cases absurd 871 ] 872 ] 873 @(is_in_subvector_is_in_supervector … proof) 874 destruct @I 875 qed. 876 877 (* XXX: todo *) 878 lemma subaddressing_mode_elim': 879 ∀T: Type[2]. 880 ∀n: nat. 881 ∀o: nat. 882 ∀v1: Vector addressing_mode_tag n. 883 ∀v2: Vector addressing_mode_tag o. 884 ∀Q: addressing_mode → T → Prop. 885 ∀fixed_v: Vector addressing_mode_tag (n + o). 886 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 887 ∀fixed_v_proof: fixed_v = v1 @@ v2. 888 ∀subaddressing_mode_proof. 889 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 890 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. 891 #T #n #o #v1 #v2 892 elim v1 cases v2 893 [1: 894 #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 895 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 896 #subaddressing_mode_proof destruct normalize 897 #addr #absurd cases absurd 898 |2: 899 #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 900 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 901 destruct normalize in match ([[]]@@hd:::tl); 902 ] 903 cases daemon 904 qed. 905 906 (* XXX: todo *) 907 lemma subaddressing_mode_elim: 908 ∀T: Type[2]. 909 ∀m: nat. 910 ∀n: nat. 911 ∀Q: addressing_mode → T → Prop. 912 ∀fixed_v: Vector addressing_mode_tag m. 913 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 914 ∀v: Vector addressing_mode_tag n. 915 ∀proof. 916 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 917 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 918 #T #m #n #Q #fixed_v 919 elim fixed_v 920 [1: 921 #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 922 #P14 #P15 #P16 #P17 #P18 #P19 #v #proof 923 normalize 924 |2: 925 ] 926 cases daemon 927 qed. 928 611 929 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 612 930 Σs': Status cm. 613 931 And (clock ?? s' = \snd current + clock … s) 614 (ASM_classify0 (\fst (\fst current)) = cl_other → 615 program_counter ? ? s' = \snd (\fst current)) ≝ 932 (if is_unconditional_jump (\fst (\fst current)) then 933 program_counter ? ? s' = 934 compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current)) 935 else 936 (ASM_classify0 (\fst (\fst current)) = cl_other → 937 program_counter ? ? s' = \snd (\fst current))) ≝ 616 938 λcm,s0,instr_pc_ticks. 617 939 let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in … … 651 973 set_program_counter … s new_pc 652 974 | LJMP addr ⇒ λinstr_refl. 975 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 653 976 let s ≝ set_clock ?? s (ticks + clock … s) in 654 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with 655 [ ADDR16 a ⇒ λaddr16: True. 656 set_program_counter … s a 657 | _ ⇒ λother: False. ⊥ 658 ] (subaddressing_modein … addr) 977 set_program_counter … s new_pc 659 978 | SJMP addr ⇒ λinstr_refl. 979 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 660 980 let s ≝ set_clock ?? s (ticks + clock … s) in 661 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 662 [ RELATIVE r ⇒ λrelative: True. 663 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in 664 set_program_counter … s new_pc 665 | _ ⇒ λother: False. ⊥ 666 ] (subaddressing_modein … addr) 981 set_program_counter … s new_pc 667 982 | AJMP addr ⇒ λinstr_refl. 983 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 668 984 let s ≝ set_clock ?? s (ticks + clock … s) in 669 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 670 [ ADDR11 a ⇒ λaddr11: True. 671 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 672 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 673 let bit ≝ get_index' ? O ? nl in 674 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 675 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 676 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in 677 set_program_counter … s new_pc 678 | _ ⇒ λother: False. ⊥ 679 ] (subaddressing_modein … addr) 985 set_program_counter … s new_pc 680 986 | ACALL addr ⇒ λinstr_refl. 681 987 let s ≝ set_clock ?? s (ticks + clock … s) in … … 714 1020 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 715 1021 try // 716 destruct(INSTR_PC) <instr_refl 717 #absurd normalize in absurd; try destruct(absurd) try%1022 destruct(INSTR_PC) <instr_refl whd 1023 try (#absurd normalize in absurd; try destruct(absurd) try %) % 718 1024 |9: 719 1025 cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?? … … 728 1034 destruct(INSTR_PC_TICKS) % 729 1035 |2: 730 #classify_assm -clock_proof >classify_proof -classify_proof 1036 -clock_proof <INSTR_PC_TICKS normalize nodelta 1037 cut(\fst instr_pc = instr ∧ \snd instr_pc = pc) 731 1038 [1: 732 normalize nodelta normalize <INSTR_PC_TICKS 733 destruct(INSTR_PC) % 1039 destruct(INSTR_PC) /2/ 734 1040 |2: 735 <classify_assm <INSTR_PC_TICKS destruct <e0 % 736 ] 1041 * #hyp1 #hyp2 >hyp1 normalize nodelta 1042 <instr_refl normalize nodelta #hyp >classify_proof -classify_proof 1043 try assumption >hyp2 % 737 1044 ] 738 1045 ] … … 745 1052 definition execute_1': ∀cm.∀s:Status cm. 746 1053 Σs':Status cm. 747 And (clock ?? s' = current_instruction_cost cm s + clock … s) 748 (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝ 1054 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1055 And (clock ?? s' = current_instruction_cost cm s + clock … s) 1056 (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then 1057 program_counter ? ? s' = 1058 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1059 else 1060 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1061 program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝ 749 1062 λcm. λs: Status cm. 750 1063 let instr_pc_ticks ≝ fetch cm (program_counter … s) in … … 756 1069 |2: 757 1070 cases(execute_1_0 cm s instr_pc_ticks) 758 #the_status * #_ #classify_assm #classify_assm' 759 lapply(classify_assm ?) 760 [1: 761 change with ( 762 ASM_classify cm s = cl_other 763 ) 764 assumption 765 |2: 766 #program_counter_refl >program_counter_refl % 767 ] 1071 #the_status * #_ #classify_assm 1072 assumption 768 1073 ] 769 1074 qed. … … 772 1077 773 1078 lemma execute_1_ok: ∀cm.∀s. 774 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 775 (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)). 776 #cm #s whd in match execute_1; normalize nodelta @pi2 1079 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1080 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 1081 (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then 1082 program_counter ? cm (execute_1 cm s) = 1083 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1084 else 1085 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1086 (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks))) 1087 (* (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *). 1088 #cm #s normalize nodelta 1089 whd in match execute_1; normalize nodelta @pi2 777 1090 qed-. (*x Andrea: indexing takes ages here *) 778 1091
Note: See TracChangeset
for help on using the changeset viewer.