Changeset 2112
 Timestamp:
 Jun 26, 2012, 11:47:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2111 r2112 3 3 include "ASM/StatusProofs.ma". 4 4 include alias "arithmetics/nat.ma". 5 6 definition bit_elim: ∀P: bool → bool. bool ≝7 λP.8 P true ∧ P false.9 10 let rec bitvector_elim_internal11 (n: nat) (P: BitVector n → bool) (m: nat)12 on m:13 m ≤ n → BitVector (n  m) → bool ≝14 match m return λm. m ≤ n → BitVector (n  m) → bool with15 [ O ⇒ λprf1. λprefix. P ?16  S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)17 ].18 /2/19 qed.20 21 definition bitvector_elim ≝22 λn: nat.23 λP: BitVector n → bool.24 bitvector_elim_internal n P n ? ?.25 try @le_n26 <minus_n_n @[[]]27 qed.28 5 29 6 lemma mem_monotonic_wrt_append: … … 113 90 @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) 114 91 assumption 115 ]116 qed.117 118 let rec list_addressing_mode_tags_elim119 (n: nat) (l: Vector addressing_mode_tag (S n))120 on l: (l → bool) → bool ≝121 match l return λx.122 match x with123 [ O ⇒ λl: Vector … O. bool124  S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool125 ] with126 [ VEmpty ⇒ true127  VCons len hd tl ⇒ λP.128 let process_hd ≝129 match hd return λhd. ∀P: hd:::tl → bool. bool with130 [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))131  indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))132  ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))133  registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))134  acc_a ⇒ λP.P ACC_A135  acc_b ⇒ λP.P ACC_B136  dptr ⇒ λP.P DPTR137  data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))138  data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))139  acc_dptr ⇒ λP.P ACC_DPTR140  acc_pc ⇒ λP.P ACC_PC141  ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR142  indirect_dptr ⇒ λP.P INDIRECT_DPTR143  carry ⇒ λP.P CARRY144  bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))145  n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))146  relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))147  addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))148  addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))149 ]150 in151 andb (process_hd P)152 (match len return λx. x = len → bool with153 [ O ⇒ λprf. true154  S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))155 ].156 try %157 [2:158 cases (sym_eq ??? prf); assumption159 1:160 generalize in match H; generalize in match tl;161 destruct #tl162 normalize in ⊢ (∀_: %. ?);163 #H164 whd normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]);165 cases (is_a hd (subaddressing_modeel y tl H))166 whd try @I normalize nodelta //167 92 ] 168 93 qed. … … 675 600 qed. 676 601 677 let rec vect_member 678 (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A) 679 on v: bool ≝ 680 match v with 681 [ VEmpty ⇒ false 682  VCons len hd tl ⇒ 683 eq hd a ∨ (vect_member A ? eq tl a) 684 ]. 685 686 let rec list_addressing_mode_tags_elim_prop 687 (n: nat) 688 (l: Vector addressing_mode_tag (S n)) 689 on l: 690 ∀P: l → Prop. 691 ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a. 692 ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a. 693 ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a. 694 ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a. 695 ∀x: l. P x ≝ 696 match l return 697 λy. 698 match y with 699 [ O ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True 700  S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop. 701 ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True. 702 ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True. 703 ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True. 704 ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True. 705 ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True. 706 ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True. 707 ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True. 708 ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True. 709 ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True. 710 ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True. 711 ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True. 712 ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True. 713 ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True. 714 ∀carry_a: if vect_member … eq_a l carry then P CARRY else True. 715 ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True. 716 ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True. 717 ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True. 718 ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True. 719 ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True. 720 ∀x:l. P x 721 ] with 722 [ VEmpty ⇒ λAbsurd. ⊥ 723  VCons len hd tl ⇒ λProof. ? 724 ] (refl ? (S n)). cases daemon. qed. (* 725 [ destruct(Absurd) 726  # A1 # A2 # A3 # A4 # A5 # A6 # A7 727 # A8 # A9 # A10 # A11 # A12 # A13 # A14 728 # A15 # A16 # A17 # A18 # A19 # X 729 cases X 730 # SUB cases daemon ] qed. 731 cases SUB 732 [ # BYTE 733 normalize 734 ]. 735 736 737 (* let prepare_hd ≝ 738 match hd with 739 [ direct ⇒ λdirect_prf. ? 740  indirect ⇒ λindirect_prf. ? 741  ext_indirect ⇒ λext_indirect_prf. ? 742  registr ⇒ λregistr_prf. ? 743  acc_a ⇒ λacc_a_prf. ? 744  acc_b ⇒ λacc_b_prf. ? 745  dptr ⇒ λdptr_prf. ? 746  data ⇒ λdata_prf. ? 747  data16 ⇒ λdata16_prf. ? 748  acc_dptr ⇒ λacc_dptr_prf. ? 749  acc_pc ⇒ λacc_pc_prf. ? 750  ext_indirect_dptr ⇒ λext_indirect_prf. ? 751  indirect_dptr ⇒ λindirect_prf. ? 752  carry ⇒ λcarry_prf. ? 753  bit_addr ⇒ λbit_addr_prf. ? 754  n_bit_addr ⇒ λn_bit_addr_prf. ? 755  relative ⇒ λrelative_prf. ? 756  addr11 ⇒ λaddr11_prf. ? 757  addr16 ⇒ λaddr16_prf. ? 758 ] 759 in ? *) 760 ]. 761 [ 1: destruct(absd) 762  2: # A1 # A2 # A3 # A4 # A5 # A6 763 # A7 # A8 # A9 # A10 # A11 # A12 764 # A13 # A14 # A15 # A16 # A17 # A18 765 # A19 * 766 ]. 767 768 769 match l return λx.match x with [O ⇒ λl: Vector … O. bool  S x' ⇒ λl: Vector addressing_mode_tag (S x'). 770 (l → bool) → bool ] with 771 [ VEmpty ⇒ true 772  VCons len hd tl ⇒ λP. 773 let process_hd ≝ 774 match hd return λhd. ∀P: hd:::tl → bool. bool with 775 [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) 776  indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) 777  ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) 778  registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) 779  acc_a ⇒ λP.P ACC_A 780  acc_b ⇒ λP.P ACC_B 781  dptr ⇒ λP.P DPTR 782  data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) 783  data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) 784  acc_dptr ⇒ λP.P ACC_DPTR 785  acc_pc ⇒ λP.P ACC_PC 786  ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR 787  indirect_dptr ⇒ λP.P INDIRECT_DPTR 788  carry ⇒ λP.P CARRY 789  bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) 790  n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) 791  relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) 792  addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) 793  addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) 794 ] 795 in 796 andb (process_hd P) 797 (match len return λx. x = len → bool with 798 [ O ⇒ λprf. true 799  S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) 800 ]. 801 try % 802 [ 2: cases (sym_eq ??? prf); @tl 803  generalize in match H; generalize in match tl; cases prf; 804 (* cases prf in tl H; : ??? WAS WORKING BEFORE *) 805 #tl 806 normalize in ⊢ (∀_: %. ?) 807 # H 808 whd 809 normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]) 810 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 811 qed. 812 *) 602 (*CSC: in is_a_to_mem_to_is_in use vect_member in place of mem … *) 603 definition vect_member ≝ 604 λA,n,eq,v,a. mem A eq (S n) v a. 605 606 definition tech_if_vect_member ≝ 607 λn,l,am,H. 608 bool_inv_rect_Type0 (vect_member … n … eq_a l am) ? H (λ_.True). 609 610 definition is_in_cons_elim: 611 ∀len.∀hd,tl.∀m:addressing_mode 612 .is_in (S len) (hd:::tl) m → 613 (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)). 614 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN; 615 cases (is_a hd am) in ISIN; /2/ 616 qed. 813 617 814 618 definition load_code_memory_aux ≝ … … 960 764 qed. 961 765 962 (*963 lemma vsplit_prod_exists:964 ∀A, m, n.965 ∀p: Vector A (m + n).966 ∃v: Vector A m.967 ∃q: Vector A n.968 〈v, q〉 = vsplit A m n p.969 #A #m #n #p970 elim m971 @ex_intro972 [1:973 2: @ex_intro974 [1:975 2:976 ]977 ]978 *)979 980 766 definition vsplit_elim: 981 767 ∀A: Type[0]. … … 993 779 qed. 994 780 995 (*996 axiom not_eqvb_S:997 ∀pc.998 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).999 1000 axiom not_eqvb_SS:1001 ∀pc.1002 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).1003 1004 axiom bitvector_elim_complete:1005 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.1006 1007 lemma bitvector_elim_complete':1008 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.1009 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv1010 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //1011 qed.1012 *)1013 1014 (*1015 lemma andb_elim':1016 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.1017 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //1018 qed.1019 *)1020 1021 781 let rec encoding_check 1022 782 (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) … … 1030 790 ]. 1031 791 1032 axiom add_commutative: 1033 ∀n: nat. 1034 ∀l, r: BitVector n. 1035 add n l r = add n r l. 1036 1037 axiom add_bitvector_of_nat_Sm: 792 lemma add_bitvector_of_nat_Sm: 1038 793 ∀n, m: nat. 1039 794 add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = 1040 795 bitvector_of_nat n (S m). 796 #n #m @add_bitvector_of_nat_plus 797 qed. 1041 798 1042 799 lemma encoding_check_append: … … 1164 921 [16,20,29: * * 18,19: * * [1,2,4,5: *] 28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] 1165 922 [47,48,49: 1166 *: #arg @( list_addressing_mode_tags_elim_prop … arg) whd try % arg1167 [2,3,5,7,10,12,16,17,18,21,2 5,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,923 *: #arg @(subaddressing_mode_elim … arg) 924 [2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58, 1168 925 59,60,63,64,65,66,67: #ARG]] 1169 926 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52, 1170 56,57,69,70,72 ,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg21171 [1,2,4,7,9,1 0,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,927 56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2) 928 [1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38, 1172 929 39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65, 1173 930 68,69,70,71: #ARG2]] 1174 [1,2,19,20: #arg3 @( list_addressing_mode_tags_elim_prop … arg3) whd try % arg3#ARG3]931 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3] 1175 932 normalize in ⊢ (???% → ?); 1176 933 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E E; [2,4: @(bitvector_3_elim_prop … vl)] … … 1178 935 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2) 1179 936 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4 937 XXX 1180 938 [ whd in match fetch; normalize nodelta <H1 ] cases daemon 1181 939 (*
Note: See TracChangeset
for help on using the changeset viewer.