Changeset 1936
 Timestamp:
 May 11, 2012, 2:38:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1668 r1936 9 9 10 10 let rec bitvector_elim_prop_internal 11 (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n  m) → Prop ≝ 11 (n: nat) (P: BitVector n → Prop) (m: nat) 12 on m: 13 m ≤ n → BitVector (n  m) → Prop ≝ 12 14 match m return λm. m ≤ n → BitVector (n  m) → Prop with 13 15 [ O ⇒ λprf1. λprefix. P ? 14  S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?) 16  S n' ⇒ λprf2. λprefix. 17 bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …) 15 18 ]. 16 [ applyS prefix 17  letin res ≝ (bit ::: prefix) 18 < (minus_S_S ? ?) 19 > (minus_Sn_m ? ?) 20 [ @ res 21  @ prf2 19 [1: 20 applyS prefix 21 2: 22 letin res ≝ (bit ::: prefix) 23 <minus_S_S 24 >minus_Sn_m 25 [1: 26 @res 27 2: 28 assumption 29 ] 30 3: 31 @le_S_to_le 32 assumption 22 33 ] 23  /2/24 ].25 34 qed. 26 35 … … 29 38 λP: BitVector n → Prop. 30 39 bitvector_elim_prop_internal n P n ? ?. 31 [ @ 32  < 33 @ 40 [ @(le_n ?) 41  <(minus_n_n ?) 42 @[[ ]] 34 43 ] 35 44 qed. … … 40 49 #b #c 41 50 cases b 42 [ normalize // 43  normalize 51 [1: 52 normalize // 53 2: 54 normalize 44 55 cases c 45 [ normalize // 46  normalize // 56 [1: 57 normalize // 58 2: 59 normalize // 47 60 ] 48 61 ] … … 54 67 55 68 let rec bitvector_elim_internal 56 (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n  m) → bool ≝ 69 (n: nat) (P: BitVector n → bool) (m: nat) 70 on m: 71 m ≤ n → BitVector (n  m) → bool ≝ 57 72 match m return λm. m ≤ n → BitVector (n  m) → bool with 58 73 [ O ⇒ λprf1. λprefix. P ? 59 74  S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?) 60 75 ]. 61 [ applyS prefix 62  letin res ≝ (bit ::: prefix) 63 < (minus_S_S ? ?) 64 > (minus_Sn_m ? ?) 65 [ @ res 66  @ prf2 67 ] 68  /2/ 76 [1: 77 applyS prefix 78 2: 79 letin res ≝ (bit ::: prefix) 80 <(minus_S_S ? ?) 81 >(minus_Sn_m ? ?) 82 [1: 83 @res 84 2: 85 @prf2 86 ] 87 3: 88 /2/ 69 89 ]. 70 90 qed. … … 74 94 λP: BitVector n → bool. 75 95 bitvector_elim_internal n P n ? ?. 76 [ @ 77  < 78 @ 96 [ @(le_n ?) 97  <(minus_n_n ?) 98 @[[ ]] 79 99 ] 80 100 qed. 81 101 82 102 lemma super_rewrite2: 83 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 103 ∀A:Type[0]. 104 ∀n, m: nat. 105 ∀v1: Vector A n. 106 ∀v2: Vector A m. 84 107 ∀P: ∀m. Vector A m → Prop. 85 n=m → v1 ≃ v2 → P n v1 → P m v2. 86 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 108 n = m → v1 ≃ v2 → P n v1 → P m v2. 109 #A #n #m #v1 #v2 #P #EQ 110 <EQ in v2; #V #JMEQ 111 >JMEQ // 87 112 qed. 88 113 … … 93 118 ∀v: Vector A n. 94 119 e ::: v = [[ e ]] @@ v. 95 # A # N # E # V 96 elim V 97 [ normalize % 98  # NN # AA # VV # IH 120 #A #n #e #v 121 elim v 122 [1: 123 normalize % 124 2: 125 #NN #AA #VV #IH 99 126 normalize 100 127 % 101 qed. 128 ] 129 qed. 102 130 103 131 lemma vector_cons_append2: … … 110 138 #A #n #m #v #q 111 139 elim v 112 [ #hd % 113  #n' #hd' #tl' #ih #hd' <ih % 140 [1: 141 #hd % 142 2: 143 #n' #hd' #tl' #ih #hd' 144 <ih % 114 145 ] 115 146 qed. … … 125 156 #A #m #n #v #q #prf #hd #E 126 157 @(super_rewrite2 A … E) 127 [ assumption  % ]158 try assumption % 128 159 qed. 129 160 … … 134 165 ∀q: Vector A m. 135 166 ∀r: Vector A o. 136 ((v @@ q) @@ r) 137 ≃ 138 (v @@ (q @@ r)). 167 (v @@ q) @@ r ≃ v @@ (q @@ r). 139 168 #A #n #m #o #v #q #r 140 elim v 141 [ % 142  #n' #hd #tl #ih 143 <(vector_cons_append2 A … hd) 144 @jmeq_cons_vector_monotone 145 // 146 ] 169 elim v try % 170 #n' #hd #tl #ih 171 <(vector_cons_append2 A … hd) 172 @jmeq_cons_vector_monotone 173 try assumption 174 @associative_plus 147 175 qed. 148 176 … … 156 184 ∀r: Vector A o. 157 185 mem A eq ? (p@@(a:::r)) a = true. 158 # A # M # O # EQ # REFLEX # P # A 159 elim P 160 [ normalize 161 > (REFLEX A) 186 #A #m #o #eq #reflex #p #a 187 elim p 188 [1: 162 189 normalize 163 # H 164 % 165  # NN # AA # PP # IH 190 >reflex 191 #H % 192 2: 193 #m' #hd #tl #inductive_hypothesis 166 194 normalize 167 cases (EQ A AA) // 168 @ IH 195 cases (eq ??) normalize nodelta 196 [1: 197 #_ % 198 2: 199 @inductive_hypothesis 200 ] 169 201 ] 170 202 qed. … … 179 211 ∀r: Vector A o. 180 212 mem A eq ? r a = true → mem A eq ? (p @@ r) a = true. 181 # A # M # O # EQ # REFLEX # P # A 182 elim P 183 [ #R #H @H 184  #NN #AA # PP # IH #R #H 213 #A #m #o #eq #reflex #p #a 214 elim p 215 [1: 216 #r #assm assumption 217 2: 218 #m' #hd #tl #inductive_hypothesis #r #assm 185 219 normalize 186 cases (EQ A AA) 187 [ normalize % 188  @ IH @ H 189 ] 220 cases (eq ??) try % 221 @inductive_hypothesis assumption 190 222 ] 191 223 qed. … … 201 233 ∀q: Vector A m. 202 234 bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)). 203 # A # O # N # EQ # REFLEX # H # V 204 elim V 205 [ normalize 206 # M # V % 207  # NN # AA # VV # IH # MM # QQ 235 #A #o #n #eq #reflex #h #v 236 elim v 237 [1: 238 normalize #m #_ @I 239 2: 240 #m' #hd #tl #inductive_hypothesis #m #q 208 241 change with (bool_to_Prop (andb ??)) 209 cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true) 210 [ 211  # HH > HH 212 > (vector_cons_append ? ? AA VV) 242 cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true) 243 [1: 244 @mem_monotonic_wrt_append try assumption 245 @mem_monotonic_wrt_append try assumption 246 normalize >reflex % 247 2: 248 #assm >assm 249 >vector_cons_append 213 250 change with (bool_to_Prop (subvector_with ??????)) 214 @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ?? 215 (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS))) 216 ? 217 (vector_associative_append A ? ? ? QQ [[AA]] VV)) 218 [ >associative_plus // 219  @IH ] 220 ] 221 @(mem_monotonic_wrt_append) 222 [ @ REFLEX 223  @(mem_monotonic_wrt_append) 224 [ @ REFLEX 225  normalize 226 > REFLEX 227 normalize 228 % 229 ] 230 ] 251 @(super_rewrite2 … (vector_associative_append … q [[hd]] tl)) 252 try @associative_plus 253 @inductive_hypothesis 254 ] 255 ] 231 256 qed. 232 257 … … 236 261 ∀v: Vector A n. 237 262 [[ ]] @@ v = v. 238 # A # N # V 239 elim V 240 [ normalize % 241  # NN # HH # VV #H % 242 ] 263 #A #n #v 264 cases v try % 265 #n' #hd #tl % 243 266 qed. 244 267 … … 251 274 ∀v: Vector A o. 252 275 bool_to_Prop (subvector_with A ? ? eq v (h ::: v)). 253 # A # O # EQ # REFLEX # H # V254 > (vector_cons_append A ? H V)255 < (vector_cons_empty A ? ([[H]] @@ V))256 @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H]])276 #A #o #eq #reflex #h #v 277 >(vector_cons_append … h v) 278 <(vector_cons_empty … ([[h]] @@ v)) 279 @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]]) 257 280 qed. 258 281 259 282 lemma eq_a_reflexive: 260 283 ∀a. eq_a a a = true. 261 # A 262 cases A 263 % 284 #a cases a % 264 285 qed. 265 286 … … 270 291 ∀to_search: addressing_mode. 271 292 bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). 272 # M # N # P # Q # TO_SEARCH 273 # H 274 elim Q 275 [ normalize 276 @ H 277  # NN # PP # QQ # IH 278 normalize 279 cases (is_a PP TO_SEARCH) 280 [ normalize 281 % 282  normalize 283 normalize in IH; 284 @ IH 285 ] 286 ] 293 #m #n #p #q #to_search #assm 294 elim q try assumption 295 #n' #hd #tl #inductive_hypothesis 296 normalize 297 cases (is_a ??) try @I 298 >inductive_hypothesis @I 287 299 qed. 288 300 … … 293 305 ∀v: Vector addressing_mode_tag n. 294 306 bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). 295 # TO_SEARCH # HD # N # V296 elim V297 [ # H298 normalize in H;299 cases H300  # NN # HHD # VV # IH # HH301 > vector_cons_append302 > (vector_cons_append ? ? HHD VV)303 @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)304 @ HH307 #to_search #hd #n #v 308 elim v 309 [1: 310 #absurd 311 normalize in absurd; cases absurd 312 2: 313 #n' #hd' #tl #inductive_hypothesis #assm 314 >vector_cons_append >(vector_cons_append … hd' tl) 315 @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) 316 assumption 305 317 ] 306 318 qed. 307 319 308 320 let rec list_addressing_mode_tags_elim 309 (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ 310 match l return λx.match x with [O ⇒ λl: Vector … O. bool  S x' ⇒ λl: Vector addressing_mode_tag (S x'). 311 (l → bool) → bool ] with 321 (n: nat) (l: Vector addressing_mode_tag (S n)) 322 on l: (l → bool) → bool ≝ 323 match l return λx. 324 match x with 325 [ O ⇒ λl: Vector … O. bool 326  S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool 327 ] with 312 328 [ VEmpty ⇒ true 313 329  VCons len hd tl ⇒ λP. … … 341 357 ]. 342 358 try % 343 [ 2: cases (sym_eq ??? prf); @tl 344  generalize in match H; generalize in match tl; cases prf; 345 (* cases prf in tl H; : ??? WAS WORKING BEFORE *) 346 #tl 359 [2: 360 cases (sym_eq ??? prf); assumption 361 1: 362 generalize in match H; generalize in match tl; 363 destruct #tl 347 364 normalize in ⊢ (∀_: %. ?); 348 # H 349 whd 350 normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]); 351 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 365 #H 366 whd normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]); 367 cases (is_a hd (subaddressing_modeel y tl H)) 368 whd try @I normalize nodelta // 369 ] 352 370 qed. 353 371 … … 535 553 lemma eq_addressing_mode_refl: 536 554 ∀a. eq_addressing_mode a a = true. 537 #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl 555 #a 556 cases a try #arg1 try #arg2 557 try @eq_bv_refl try @eq_b_refl 538 558 try normalize % 539 559 qed. 540 560 541 definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ 561 definition eq_sum: 562 ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ 542 563 λlt, rt, leq, req, left, right. 543 564 match left with … … 782 803 eq_sum A B leq req s s = true. 783 804 #A #B #leq #req #s #leq_refl #req_refl 784 cases s whd in ⊢ (? → ??%?); // 805 cases s 806 whd in ⊢ (? → ??%?); 807 assumption 785 808 qed. 786 809 … … 793 816 eq_prod A B leq req s s = true. 794 817 #A #B #leq #req #s #leq_refl #req_refl 795 cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl 818 cases s 819 whd in ⊢ (? → ? → ??%?); 820 #l #r 821 >leq_refl @req_refl 796 822 qed. 797 823 … … 835 861 whd in ⊢ (??%?); 836 862 cases arg1 837 [ #arg1_left normalize nodelta 863 [1: 864 #arg1_left normalize nodelta 838 865 @eq_sum_refl 839 [1: #arg @eq_sum_refl 840 [1: #arg @eq_sum_refl 841 [1: #arg @eq_sum_refl 842 [1: #arg @eq_prod_refl 843 [*: @eq_addressing_mode_refl ] 844 2: #arg @eq_prod_refl 845 [*: #arg @eq_addressing_mode_refl ] 866 [1: 867 #arg @eq_sum_refl 868 [1: 869 #arg @eq_sum_refl 870 [1: 871 #arg @eq_sum_refl 872 [1: 873 #arg @eq_prod_refl 874 [*: 875 @eq_addressing_mode_refl 876 ] 877 2: 878 #arg @eq_prod_refl 879 [*: 880 #arg @eq_addressing_mode_refl 881 ] 846 882 ] 847 2: #arg @eq_prod_refl 848 [*: #arg @eq_addressing_mode_refl ] 883 2: 884 #arg @eq_prod_refl 885 [*: 886 #arg @eq_addressing_mode_refl 887 ] 849 888 ] 850 2: #arg @eq_prod_refl 851 [*: #arg @eq_addressing_mode_refl ] 889 2: 890 #arg @eq_prod_refl 891 [*: 892 #arg @eq_addressing_mode_refl 893 ] 852 894 ] 853 2: #arg @eq_prod_refl 854 [*: #arg @eq_addressing_mode_refl ] 895 2: 896 #arg @eq_prod_refl 897 [*: 898 #arg @eq_addressing_mode_refl 899 ] 855 900 ] 856 2: #arg1_right normalize nodelta 857 @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] 901 2: 902 #arg1_right normalize nodelta 903 @eq_prod_refl 904 [*: 905 #arg @eq_addressing_mode_refl 906 ] 858 907 ] 859 908 *: 860 909 whd in ⊢ (??%?); 861 910 cases arg1 862 [*: #arg1 >eq_sum_refl 863 [1,4: normalize @eq_addressing_mode_refl 864 2,3,5,6: #arg @eq_prod_refl 865 [*: #arg @eq_addressing_mode_refl ] 911 [*: 912 #arg1 >eq_sum_refl 913 [1,4: 914 @eq_addressing_mode_refl 915 2,3,5,6: 916 #arg @eq_prod_refl 917 [*: 918 #arg @eq_addressing_mode_refl 919 ] 866 920 ] 867 921 ] … … 917 971 ∀i. eq_instruction i i = true. 918 972 #i cases i 919 [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl 920 7: #arg1 #arg2 921 whd in ⊢ (??%?); 922 >eq_addressing_mode_refl 923 >eq_addressing_mode_refl 924 % 925 8: #arg @eq_preinstruction_refl 973 [1,2,3,4,5,6: 974 #arg1 @eq_addressing_mode_refl 975 7: 976 #arg1 #arg2 977 whd in ⊢ (??%?); 978 >eq_addressing_mode_refl 979 >eq_addressing_mode_refl % 980 8: 981 #arg @eq_preinstruction_refl 926 982 ] 927 983 qed. 928 984 929 985 let rec vect_member 930 (A: Type[0]) (n: nat) (eq: A → A → bool) 931 (v: Vector A n) (a: A)on v: bool ≝986 (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A) 987 on v: bool ≝ 932 988 match v with 933 989 [ VEmpty ⇒ false 934 990  VCons len hd tl ⇒ 935 eq hd a ∨ (vect_member A ? eq tl a)991 eq hd a ∨ (vect_member A ? eq tl a) 936 992 ]. 937 993 … … 1074 1130 〈[[]], v〉 = split A 0 m v. 1075 1131 #A #m #v 1076 elim v 1077 [ % 1078  #n #hd #tl #ih 1079 normalize in ⊢ (???%); % 1132 cases v try % 1133 #n #hd #tl % 1134 qed. 1135 1136 lemma Vector_O: 1137 ∀A: Type[0]. 1138 ∀v: Vector A 0. 1139 v ≃ VEmpty A. 1140 #A #v 1141 generalize in match (refl … 0); 1142 cases v in ⊢ (??%? → ?%%??); // 1143 #n #hd #tl #absurd 1144 destruct(absurd) 1145 qed. 1146 1147 lemma Vector_Sn: 1148 ∀A: Type[0]. 1149 ∀n: nat. 1150 ∀v: Vector A (S n). 1151 ∃hd: A. ∃tl: Vector A n. 1152 v ≃ VCons A n hd tl. 1153 #A #n #v 1154 generalize in match (refl … (S n)); 1155 cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 1156 [1: 1157 #absurd destruct(absurd) 1158 2: 1159 #m #hd #tl #eq 1160 <(injective_S … eq) 1161 %{hd} %{tl} % 1080 1162 ] 1081 qed.1082 1083 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.1084 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //1085 #n #hd #tl #abs @⊥ destruct (abs)1086 qed.1087 1088 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).1089 ∃hd.∃tl.v ≃ VCons A n hd tl.1090 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));1091 [ #abs @⊥ destruct (abs)1092  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]1093 1163 qed. 1094 1164 … … 1125 1195 #A #n #q #r 1126 1196 generalize in match (Vector_O A q …); 1127 #hyp 1128 >hyp in ⊢ (??%?); 1129 % 1130 qed. 1131 1132 axiom split_succ: 1133 ∀A, m, n. 1197 #hyp >hyp in ⊢ (??%?); % 1198 qed. 1199 1200 lemma tail_head: 1201 ∀a: Type[0]. 1202 ∀m, n: nat. 1203 ∀hd: a. 1204 ∀l: Vector a m. 1205 ∀r: Vector a n. 1206 tail a ? (hd:::(l@@r)) = l@@r. 1207 #a #m #n #hd #l #r 1208 cases l try % 1209 #m' #hd' #tl' % 1210 qed. 1211 1212 lemma head_head': 1213 ∀a: Type[0]. 1214 ∀m: nat. 1215 ∀hd: a. 1216 ∀l: Vector a m. 1217 hd = head' … (hd:::l). 1218 #a #m #hd #l cases l try % 1219 #m' #hd' #tl % 1220 qed. 1221 1222 lemma split_succ: 1223 ∀A: Type[0]. 1224 ∀m, n: nat. 1134 1225 ∀l: Vector A m. 1135 1226 ∀r: Vector A n. … … 1137 1228 ∀hd: A. 1138 1229 v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)). 1139 (*1140 1230 #A #m 1141 1231 elim m 1142 [ #n #l #r #v #hd #equal #hyp 1143 normalize >(Vector_O A l) >equal 1144 >(Vector_O A l) % 1145  #n' #ih #n #l #r #v #hd 1146 #equal #hyp 1147 cases(Vector_Sn A n' l) 1148 #hd' #exists 1149 cases exists #tl #jmeq 1150 >jmeq *) 1232 [1: 1233 #n #l #r #v #hd #eq #hyp 1234 destruct 1235 >(Vector_O … l) % 1236 2: 1237 #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp 1238 destruct 1239 cases (Vector_Sn … l) #hd' #tl' 1240 whd in ⊢ (???%); 1241 >tail_head 1242 <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r)) 1243 [1: 1244 <hyp <head_head' % 1245 2: 1246 elim l normalize // 1247 ] 1248 ] 1249 qed. 1151 1250 1152 1251 lemma split_prod: 1153 ∀A,m,n. 1252 ∀A: Type[0]. 1253 ∀m, n: nat. 1154 1254 ∀p: Vector A (m + n). 1155 1255 ∀v: Vector A m. 1156 1256 ∀q: Vector A n. 1157 1257 p = v@@q → 〈v, q〉 = split A m n p. 1158 #A #m 1159 elim m1160 [#n #p #v #q #hyp1258 #A #m elim m 1259 [1: 1260 #n #p #v #q #hyp 1161 1261 >hyp <(vector_append_zero A n q v) 1162 1262 >(prod_vector_zero_eq_left A …) 1163 1263 @split_zero 1164  #r #ih #n #p #v #q #hyp 1264 2: 1265 #r #ih #n #p #v #q #hyp 1165 1266 >hyp 1166 cases (Vector_Sn A r v) 1167 #hd #exists1168 cases exists1169 #tl #jmeq >jmeq1170 @ split_succ [1: % 2: @ih % ]1267 cases (Vector_Sn A r v) #hd #exists 1268 cases exists #tl #jmeq 1269 >jmeq 1270 @split_succ try % 1271 @ih % 1171 1272 ] 1172 1273 qed. … … 1190 1291 *) 1191 1292 1192 axiom split_elim: 1193 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. 1194 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 1195 (* #A #l #m #v #P #hyp 1196 normalize 1197 <(split_prod A l m v ? ? ?) 1198 *) 1199 1293 lemma split_elim: 1294 ∀A: Type[0]. 1295 ∀l, m: nat. 1296 ∀v: Vector A (l + m). 1297 ∀P: (Vector A l) × (Vector A m) → Prop. 1298 (∀vl: Vector A l. 1299 ∀vm: Vector A m. 1300 v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 1301 cases daemon (* XXX: problem with dependent types *) 1302 qed. 1303 1304 (* XXX: this looks almost certainly wrong *) 1200 1305 example half_add_SO: 1201 1306 ∀pc. … … 1230 1335 *) 1231 1336 1232 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) 1233 (encoding: list Byte) on encoding: Prop ≝ 1337 let rec encoding_check 1338 (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) 1339 (encoding: list Byte) 1340 on encoding: Prop ≝ 1234 1341 match encoding with 1235 1342 [ nil ⇒ final_pc = pc … … 1239 1346 ]. 1240 1347 1241 lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2. 1242 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) → 1243 let intermediate_pc ≝ pc + length … l1 in 1244 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧ 1245 encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. 1246 #code_memory #final_pc #l1 elim l1 1247 [ #pc #l2 whd in ⊢ (????% → ?); #H <plus_n_O whd whd in ⊢ (?%?); /2/ 1248  #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm 1249 #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ] 1348 lemma encoding_check_append: 1349 ∀code_memory: BitVectorTrie Byte 16. 1350 ∀final_pc: nat. 1351 ∀l1: list Byte. 1352 ∀pc: nat. 1353 ∀l2: list Byte. 1354 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) → 1355 let intermediate_pc ≝ pc + length … l1 in 1356 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧ 1357 encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. 1358 #code_memory #final_pc #l1 elim l1 1359 [1: 1360 #pc #l2 1361 whd in ⊢ (????% → ?); #H 1362 <plus_n_O 1363 whd whd in ⊢ (?%?); /2/ 1364 2: 1365 #hd #tl #IH #pc #l2 * #H1 #H2 1366 >half_add_SO in H2; #H2 1367 cases (IH … H2) <plus_n_Sm 1368 #K1 #K2 % [2: @K2 ] whd % // 1369 >half_add_SO @K1 1370 ] 1250 1371 qed. 1251 1372 1252 1373 axiom bitvector_3_elim_prop: 1253 ∀P: BitVector 3 → Prop.1254 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →1255 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →1256 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.1374 ∀P: BitVector 3 → Prop. 1375 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → 1376 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → 1377 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 1257 1378 1258 1379 definition ticks_of_instruction ≝ 1259 λi.1260 let trivial_code_memory ≝ assembly1 i in1261 let trivial_status ≝ load_code_memory trivial_code_memory in1262 \snd (fetch trivial_status (zero ?)).1380 λi. 1381 let trivial_code_memory ≝ assembly1 i in 1382 let trivial_status ≝ load_code_memory trivial_code_memory in 1383 \snd (fetch trivial_status (zero ?)). 1263 1384 1264 1385 lemma fetch_assembly: 1265 ∀pc,i,code_memory,assembled. 1386 ∀pc: nat. 1387 ∀i: instruction. 1388 ∀code_memory: BitVectorTrie Byte 16. 1389 ∀assembled: list Byte. 1266 1390 assembled = assembly1 i → 1267 1391 let len ≝ length … assembled in 1268 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →1269 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in1270 let 〈instr_pc, ticks〉 ≝ fetched in1271 let 〈instr,pc'〉 ≝ instr_pc in1272 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.1273 #pc #i #code_memory #assembled cases i [8: *]1392 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 1393 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in 1394 let 〈instr_pc, ticks〉 ≝ fetched in 1395 let 〈instr,pc'〉 ≝ instr_pc in 1396 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 1397 #pc #i #code_memory #assembled cases i [8: *] 1274 1398 [16,20,29: * * 18,19: * * [1,2,4,5: *] 28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] 1275 1399 [47,48,49: … … 1289 1413 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4 1290 1414 [ whd in match fetch; normalize nodelta <H1 ] cases daemon 1291 (*XXX 1292 1293 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?) 1415 (* 1416 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?) 1294 1417 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3] 1295 1418 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29, 1296 1419 30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66, 1297 1420 69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2] 1298 whd >eq_instruction_refl >H4 @eq_bv_refl*) 1299 qed. 1300 1301 let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝ 1302 match expected with 1421 whd >eq_instruction_refl >H4 @eq_bv_refl 1422 *) (* XXX: not working! *) 1423 qed. 1424 1425 let rec fetch_many 1426 (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word) 1427 (expected: list instruction) 1428 on expected: Prop ≝ 1429 match expected with 1303 1430 [ nil ⇒ eq_bv … pc final_pc = true 1304 1431  cons i tl ⇒ 1305 1306 1307 1432 let fetched ≝ fetch code_memory pc in 1433 let 〈instr_pc, ticks〉 ≝ fetched in 1434 let 〈instr,pc'〉 ≝ instr_pc in 1308 1435 eq_instruction instr i = true ∧ 1309 ticks = (ticks_of_instruction i) ∧ 1310 fetch_many code_memory final_pc pc' tl]. 1311 1312 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. 1313 #A #a #b #EQ destruct // 1436 ticks = (ticks_of_instruction i) ∧ 1437 fetch_many code_memory final_pc pc' tl 1438 ]. 1439 1440 lemma option_destruct_Some: 1441 ∀A: Type[0]. 1442 ∀a, b: A. 1443 Some A a = Some A b → a = b. 1444 #A #a #b #EQ 1445 destruct % 1314 1446 qed. 1315 1447 1316 1448 axiom eq_instruction_to_eq: 1317 ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1318 1449 ∀i1, i2: instruction. 1450 eq_instruction i1 i2 = true → i1 = i2. 1451 1452 (* 1319 1453 lemma fetch_assembly_pseudo': 1320 ∀lookup_labels.∀pol:policy_type lookup_labels.∀ppc,lookup_datalabels. 1321 ∀pi,code_memory,len,assembled,instructions,pc. 1322 let expansion ≝ pol ppc in 1323 instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi → 1324 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi → 1325 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 1326 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 1327 #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 1328 #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2 1329 cases (pair_destruct ?????? EQ2) EQ2; #EQ2a #EQ2b 1330 >EQ2a >EQ2b EQ2a EQ2b; 1454 ∀lookup_labels. 1455 ∀pol: policy_type lookup_labels. 1456 ∀ppc. 1457 ∀lookup_datalabels. 1458 ∀pi. 1459 ∀code_memory. 1460 ∀len. 1461 ∀assembled. 1462 ∀instructions. 1463 ∀pc. 1464 let expansion ≝ pol ppc in 1465 instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi → 1466 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi → 1467 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 1468 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 1469 #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 1470 #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2 1471 cases (pair_destruct ?????? EQ2) EQ2; #EQ2a #EQ2b 1472 >EQ2a >EQ2b EQ2a EQ2b; 1331 1473 generalize in match (pc + flatten … (map … assembly1 instructions)); #final_pc 1332 1474 generalize in match pc; elim instructions 1333 [ #pc whd in ⊢ (% → %); #H >H @eq_bv_refl 1334  #i #tl #IH #pc #H whd cases (encoding_check_append … H); H; #H1 #H2 whd 1475 [1: 1476 #pc whd in ⊢ (% → %); #H >H @eq_bv_refl 1477 2: 1478 #i #tl #IH #pc #H whd cases (encoding_check_append … H); H; #H1 #H2 whd 1335 1479 generalize in match (fetch_assembly pc i code_memory … (refl …) H1); 1336 1480 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %); 1337 1481 cases newi_pc #newi #newpc whd in ⊢ (% → %); #K cases (conjunction_true … K) K; #K1 1338 1482 cases (conjunction_true … K1) K1; #K1 #K2 #K3 % try % 1339 [ @K1  @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2  >(eq_bv_eq … K3) @IH @H2 ] 1340 qed. 1483 [1: 1484 @K1 1485 2: 1486 @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 1487 3: 1488 >(eq_bv_eq … K3) @IH @H2 1489 ] 1490 ] 1491 qed. 1492 *) 1341 1493 1342 1494 axiom bitvector_of_nat_nat_of_bitvector: … … 1346 1498 (* CSC: soo long next one; can we merge with previous one now? *) 1347 1499 lemma fetch_assembly_pseudo: 1348 ∀program: pseudo_assembly_program.1349 ∀pol: policy program.1500 ∀program: pseudo_assembly_program. 1501 ∀pol: policy program. 1350 1502 let lookup_labels ≝ λx:Identifier.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in 1351 1503 ∀ppc.∀code_memory.
Note: See TracChangeset
for help on using the changeset viewer.