Changeset 1650 for src/ASM/ASMCosts.ma
 Timestamp:
 Jan 19, 2012, 4:56:17 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1648 r1650 106 106 cases other 107 107 qed. 108 109 lemma is_in_tl_to_is_in_cons_hd_tl:110 ∀n: nat.111 ∀the_vect: Vector addressing_mode_tag n.112 ∀h: addressing_mode_tag.113 ∀element: addressing_mode.114 is_in n the_vect element → is_in (S n) (h:::the_vect) element.115 #n #the_vect #h #element #assm116 normalize cases (is_a h element) normalize nodelta117 //118 qed.119 120 lemma is_in_singleton_to_is_a:121 ∀tag.122 ∀element.123 is_in … [[tag]] element → is_a tag element.124 #tag #element125 normalize in ⊢ (% → ?);126 cases (is_a tag element)127 [1:128 normalize nodelta #irrelevant129 @I130 2:131 normalize nodelta #absurd132 cases absurd133 ]134 qed.135 108 136 109 lemma is_a_decidable: … … 150 123 qed. 151 124 152 (* 153 lemma is_in_cons_hd_tl_to_is_in_tl: 125 lemma eq_a_elim: 126 ∀tag. 127 ∀hd. 128 ∀P: bool → Prop. 129 (tag = hd → P (true)) → 130 (tag ≠ hd → P (false)) → 131 P (eq_a tag hd). 132 #tag #hd #P 133 cases tag 134 cases hd 135 #true_hyp #false_hyp 136 try @false_hyp 137 try @true_hyp 138 try % 139 #absurd destruct(absurd) 140 qed. 141 142 lemma is_a_true_to_is_in: 154 143 ∀n: nat. 155 ∀the_vect: Vector addressing_mode_tag n. 156 ∀h: addressing_mode_tag. 157 ∀element: addressing_mode. 158 is_in (S n) (h:::the_vect) element → 159 is_in n the_vect element. *) 144 ∀x: addressing_mode. 145 ∀tag: addressing_mode_tag. 146 ∀supervector: Vector addressing_mode_tag n. 147 mem addressing_mode_tag eq_a n supervector tag → 148 is_a tag x = true → 149 is_in … supervector x. 150 #n #x #tag #supervector 151 elim supervector 152 [1: 153 #absurd cases absurd 154 2: 155 #n' #hd #tl #inductive_hypothesis 156 whd in match (mem … eq_a (S n') (hd:::tl) tag); 157 @eq_a_elim normalize nodelta 158 [1: 159 #tag_hd_eq #irrelevant 160 whd in match (is_in (S n') (hd:::tl) x); 161 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta 162 @I 163 2: 164 #tag_hd_neq 165 whd in match (is_in (S n') (hd:::tl) x); 166 change with ( 167 mem … eq_a n' tl tag) 168 in match (fold_right … n' ? false tl); 169 #mem_hyp #is_a_hyp 170 cases(is_a hd x) 171 [1: 172 normalize nodelta // 173 2: 174 normalize nodelta 175 @inductive_hypothesis assumption 176 ] 177 ] 178 ] 179 qed. 160 180 161 181 lemma is_in_subvector_is_in_supervector: … … 166 186 subvector_with … eq_a subvector supervector → 167 187 is_in m subvector element → is_in n supervector element. 168 (*169 188 #m #n #subvector #supervector #element 170 189 elim subvector … … 173 192 cases is_in_proof 174 193 2: 175 #n #hd #tl #inductive_hypothesis 176 cases supervector 194 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof 195 whd in match (is_in … (hd':::tl') element); 196 cases (is_a_decidable hd' element) 177 197 [1: 178 #subvector_with_proof #is_in_proof 179 cases subvector_with_proof 180 2: 181 #n' #hd' #tl' #subvector_with_proof #is_in_proof 182 whd in match (is_in … (hd':::tl') element); 183 cases (is_a_decidable hd' element) 184 [1: 185 #is_a_true >is_a_true normalize nodelta 186 @I 187 2: 188 #is_a_false >is_a_false normalize nodelta 189 @inductive_hypothesis' 190 [2: 191 assumption 192 1: 193 ] 194 ] 195 ] 196 ] 197 qed. 198 3: 199 #n #hd #tl #inductive_hypothesis 200 #subvector_with_proof #is_in_proof 201 @inductive_hypothesis 202 [1: 203 assumption 204 4: 205 ] 206 qed. 207 208 209 210 [1: 211 #n #supervector #subvector_proof #is_in_proof 212 cases is_in_proof 213 2: 214 #m' #hd #tl #inductive_hypothesis #n' #supervector 215 #subvector_proof #is_in_proof 216 generalize in match is_in_proof; 217 cases(is_a_decidable hd element) 218 whd in match (is_in … (hd:::tl) element); 219 [1: 220 #is_a_true >is_a_true normalize nodelta 198 #is_a_true >is_a_true 221 199 #irrelevant 200 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; 201 @(is_a_true_to_is_in … is_a_true) 202 lapply(subvector_with_proof) 203 cases(mem … eq_a n supervector hd') // 222 204 2: 223 205 #is_a_false >is_a_false normalize nodelta … … 225 207 @inductive_hypothesis 226 208 [1: 227 generalize in match subvector_ proof;228 whd in match (subvector_with … eq_a (hd :::tl) supervector);229 cases(mem_decidable n ' supervector hd)209 generalize in match subvector_with_proof; 210 whd in match (subvector_with … eq_a (hd':::tl') supervector); 211 cases(mem_decidable n supervector hd') 230 212 [1: 231 213 #mem_true >mem_true normalize nodelta … … 239 221 ] 240 222 ] 241 242 243 244 245 generalize in match subvector_proof; 246 whd in match (subvector_with … eq_a (hd:::tl) supervector); 247 cases(mem_decidable n' supervector hd) 248 [1: 249 #mem_true >mem_true normalize nodelta 250 #subvector_with_proof 251 @inductive_hypothesis 252 [1: 253 assumption 254 2: 255 generalize in match is_in_proof; 256 whd in match (is_in (S m') (hd:::tl) element); 257 cases(is_a_decidable hd element) 258 [1: 259 #is_a_true >is_a_true normalize nodelta 260 #irrelevant 261 whd whd in match (is_in … tl element); 262 2: 263 #is_a_false >is_a_false normalize nodelta 264 #assm assumption 265 ] 266 ] 267 2: 268 #mem_false >mem_false normalize nodelta 269 #absurd cases absurd 270 ] 271 1: 272 normalize nodelta #subvector_with_assm 273 cases(is_a_decidable hd element) 274 [1: 275 #is_a_hd 276 generalize in match subvector_proof; 277 whd in match (subvector_with … eq_a (hd:::tl) supervector); 278 2: 279 #not_is_a_hd 280 ] 281 ] 282 ] *) 283 cases daemon 223 ] 284 224 qed. 285 225 … … 417 357 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 418 358 419 (*420 lemma subaddressing_mode_elim:421 ∀T:Type[2].422 ∀P1: Word11 → T.423 ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.424 ∀addr: addressing_mode.425 ∀p: is_in 1 [[ addr11 ]] addr.426 ∀Q: addressing_mode → T → Prop.427 (∀w. Q (ADDR11 w) (P1 w)) →428 Q addr (429 match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with430 [ ADDR11 (x:Word11) ⇒ λH:True. P1 x431  ADDR16 _ ⇒ λH:False. P2 H432  DIRECT _ ⇒ λH:False. P3 H433  INDIRECT _ ⇒ λH:False. P4 H434  EXT_INDIRECT _ ⇒ λH:False. P5 H435  ACC_A ⇒ λH:False. P6 H436  REGISTER _ ⇒ λH:False. P7 H437  ACC_B ⇒ λH:False. P8 H438  DPTR ⇒ λH:False. P9 H439  DATA _ ⇒ λH:False. P10 H440  DATA16 _ ⇒ λH:False. P11 H441  ACC_DPTR ⇒ λH:False. P12 H442  ACC_PC ⇒ λH:False. P13 H443  EXT_INDIRECT_DPTR ⇒ λH:False. P14 H444  INDIRECT_DPTR ⇒ λH:False. P15 H445  CARRY ⇒ λH:False. P16 H446  BIT_ADDR _ ⇒ λH:False. P17 H447  N_BIT_ADDR _ ⇒ λH:False. P18 H448  RELATIVE _ ⇒ λH:False. P19 H449 ] p).450 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13451 #P14 #P15 #P16 #P17 #P18 #P19452 * try #x1 try #x2 try #x3 try #x4453 try (@⊥ assumption) normalize @x4454 qed. *)455 456 359 include alias "arithmetics/nat.ma". 457 360 458 let rec block_cost 361 let rec block_cost' 459 362 (code_memory: BitVectorTrie Byte 16) (program_counter: Word) 460 363 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 461 364 (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter) 462 (good_program_witness: good_program code_memory total_program_size) 365 (good_program_witness: good_program code_memory total_program_size) (first_time_around: bool) 463 366 on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝ 464 367 match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with … … 466 369  S program_size' ⇒ λrecursive_case. 467 370 let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in 468 match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with 469 [ None ⇒ 371 let to_continue ≝ 372 match lookup_opt … program_counter' cost_labels with 373 [ None ⇒ true 374  Some _ ⇒ first_time_around 375 ] 376 in 377 if to_continue then 470 378 match instruction return λx. x = instruction → ? with 471 379 [ RealInstruction real_instruction ⇒ λreal_instruction_refl. … … 482 390  DJNZ src_trgt relative ⇒ λinstr. ticks 483 391  _ ⇒ λinstr. 484 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness?392 ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ? 485 393 ] (refl … real_instruction) 486 394  ACALL addr ⇒ λinstr. 487 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness?395 ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ? 488 396  AJMP addr ⇒ λinstr. ticks 489 397  LCALL addr ⇒ λinstr. 490 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness?398 ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ? 491 399  LJMP addr ⇒ λinstr. ticks 492 400  SJMP addr ⇒ λinstr. ticks 493 401  JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) 494 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness?402 ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ? 495 403  MOVC src trgt ⇒ λinstr. 496 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness?404 ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ? 497 405 ] (refl … instruction) 498  Some _ ⇒ ticks499 ]406 else 407 0 500 408 ]. 501 409 [1: … … 635 543 qed. 636 544 545 definition block_cost ≝ 546 λcode_memory: BitVectorTrie Byte 16. 547 λprogram_counter: Word. 548 λtotal_program_size: nat. 549 λcost_labels: BitVectorTrie costlabel 16. 550 λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. 551 λgood_program_witness: good_program code_memory total_program_size. 552 block_cost' code_memory program_counter total_program_size total_program_size cost_labels 553 reachable_program_counter_witness good_program_witness true ?. 554 @le_plus_n_r 555 qed. 556 637 557 lemma fetch_program_counter_n_Sn: 638 558 ∀instruction: instruction. … … 672 592 [ None ⇒ λlookup_refl. cost_mapping 673 593  Some lbl ⇒ λlookup_refl. 674 let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size cost_labels ? good_program_witness ?in594 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 675 595 add … cost_mapping lbl cost 676 596 ] (refl … (lookup_opt … program_counter cost_labels)) … … 680 600 assumption 681 601 2: 682 //683 3:684 602 assumption 685 603 ]
Note: See TracChangeset
for help on using the changeset viewer.