Changeset 1650
 Timestamp:
 Jan 19, 2012, 4:56:17 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 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 ] 
src/ASM/CostsProof.ma
r1648 r1650 18 18 definition ASM_classify0: instruction → status_class ≝ 19 19 λi: instruction. 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 20 match i with 21 [ RealInstruction pre ⇒ 22 match pre with 23 [ RET ⇒ cl_return 24  JZ _ ⇒ cl_jump 25  JNZ _ ⇒ cl_jump 26  JC _ ⇒ cl_jump 27  JNC _ ⇒ cl_jump 28  JB _ _ ⇒ cl_jump 29  JNB _ _ ⇒ cl_jump 30  JBC _ _ ⇒ cl_jump 31  CJNE _ _ ⇒ cl_jump 32  DJNZ _ _ ⇒ cl_jump 33  _ ⇒ cl_other 34 ] 35  ACALL _ ⇒ cl_call 36  LCALL _ ⇒ cl_call 37  JMP _ ⇒ cl_call 38  AJMP _ ⇒ cl_jump 39  LJMP _ ⇒ cl_jump 40  SJMP _ ⇒ cl_jump 41  _ ⇒ cl_other 42 ]. 43 43 44 44 definition ASM_classify: Status → status_class ≝ 45 λs: Status. 46 ASM_classify0 (current_instruction s). 45 λs: Status. 46 ASM_classify0 (current_instruction s). 47 48 definition current_instruction_is_labelled ≝ 49 λcost_labels: BitVectorTrie costlabel 16. 50 λs: Status. 51 let pc ≝ program_counter … s in 52 match lookup_opt … pc cost_labels with 53 [ None ⇒ False 54  _ ⇒ True 55 ]. 56 57 definition next_instruction_properly_relates_program_counters ≝ 58 λbefore: Status. 59 λafter : Status. 60 let size ≝ current_instruction_cost before in 61 let pc_before ≝ program_counter … before in 62 let pc_after ≝ program_counter … after in 63 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 64 sum = pc_after. 65 66 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ 67 λcost_labels. 68 mk_abstract_status 69 Status 70 (λs,s'. (execute_1 s) = s') 71 (λs,class. ASM_classify s = class) 72 (current_instruction_is_labelled cost_labels) 73 next_instruction_properly_relates_program_counters. 47 74 48 75 let rec compute_max_trace_label_label_cost … … 92 119 ]. 93 120 94 (*Useless now?95 (* To be moved *)96 lemma pred_minus_1:97 ∀m, n: nat.98 ∀proof: n < m.99 pred (m  n) = m  n  1.100 #m #n101 cases m102 [ #proof103 cases(lt_to_not_zero … proof)104  #m' #proof105 normalize in ⊢ (???%);106 cases n107 [ normalize //108  #n' normalize109 cases(m'  n')110 [ %111  #Sm_n'112 normalize //113 ]114 ]115 ]116 qed.117 118 lemma succ_m_plus_one:119 ∀m: nat.120 S m = m + 1.121 //122 qed.*)123 124 121 include alias "arithmetics/nat.ma". 125 126 (*127 lemma minus_m_n_minus_minus_plus_1:128 ∀m, n: nat.129 ∀proof: n < m.130 m  n = (m  n  1) + 1.131 /3 by lt_plus_to_minus_r, plus_minus/132 qed.133 134 lemma plus_minus_rearrangement_1:135 ∀m, n, o: nat.136 ∀proof_n_m: n ≤ m.137 ∀proof_m_o: m ≤ o.138 (m  n) + (o  m) = o  n.139 #m #n #o #H1 #H2140 lapply (minus_to_plus … H1 (refl …)) #K1 >K1141 lapply (minus_to_plus … H2 (refl …)) #K2 >K2142 /2 by plus_minus/143 qed.144 145 lemma plus_minus_rearrangement_2:146 ∀m, n, o: nat. n ≤ m → o ≤ n →147 (m  n) + (n  o) = m  o.148 /2 by plus_minus_rearrangement_1/149 qed.150 151 lemma m_le_plus_n_m:152 ∀m, n: nat.153 m ≤ n + m.154 #m #n //155 qed.156 157 lemma n_plus_m_le_o_to_m_le_o:158 ∀m, n, o: nat.159 n + m ≤ o → m ≤ o.160 #m #n #o #assm /2 by le_plus_b/161 qed.162 163 lemma m_minus_n_plus_o_m_minus_n_minus_o:164 ∀m, n, o: nat.165 m  (n + o) = m  n  o.166 #m #n #o /2 by /167 qed.168 *)169 122 170 123 let rec compute_max_trace_label_label_cost_is_ok … … 461 414 qed. 462 415 463 (* ??????????????????????? *) 464 axiom block_cost_static_dynamic_ok: 465 ∀cost_labels: BitVectorTrie costlabel 16. 466 ∀trace_ends_flag. 467 ∀start_status: Status. 468 ∀final_status: Status. 469 ∀the_trace: 470 trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 471 start_status final_status. 472 let mem ≝ code_memory … start_status in 473 let pc ≝ program_counter … start_status in 474 let program_size ≝ 2^16 in 475 block_cost mem cost_labels pc program_size = 476 compute_paid_trace_label_label cost_labels trace_ends_flag 477 start_status final_status the_trace. 416 (* XXX: zero in base cases (where the trace is a singleton transition) because 417 we are counting until one from end 418 *) 419 let rec trace_any_label_length 420 (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) 421 (start_status: Status) (final_status: Status) 422 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 423 on the_trace: nat ≝ 424 match the_trace with 425 [ tal_base_not_return the_status _ _ _ _ ⇒ 0 426  tal_base_return the_status _ _ _ ⇒ 0 427  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒ 428 let tail_length ≝ trace_any_label_length … final_trace in 429 let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call)  nat_of_bitvector … (program_counter … pre_fun_call) in 430 pc_difference + tail_length 431  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 432 let tail_length ≝ trace_any_label_length … tail_trace in 433 let pc_difference ≝ nat_of_bitvector … (program_counter … status_init)  nat_of_bitvector … (program_counter … status_pre) in 434 pc_difference + tail_length 435 ]. 436 437 (* XXX: commented out in favour of above 438 let rec trace_label_label_length 439 (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) 440 (start_status: Status) (final_status: Status) 441 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 442 on the_trace: nat ≝ 443 match the_trace with 444 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ? 445 ] 446 and trace_any_label_length 447 (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) 448 (start_status: Status) (final_status: Status) 449 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 450 on the_trace: nat ≝ 451 match the_trace with 452 [ tal_base_not_return the_status _ _ _ _ ⇒ ? 453  tal_base_return the_status _ _ _ ⇒ ? 454  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒ ? 455  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ ? 456 ] 457 and trace_label_return_length 458 (cost_labels: BitVectorTrie costlabel 16) (start_status: Status) (final_status: Status) 459 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 460 on the_trace: nat ≝ 461 match the_trace with 462 [ tlr_base before after trace_to_lift ⇒ ? 463  tlr_step initial labelled final labelled_trace ret_trace ⇒ ? 464 ]. 465 cases daemon 466 qed. 467 *) 468 469 (* Experiments with block_cost first! 470 lemma reachable_program_counter_to_compute_trace_any_label_length_le_program_size: 471 ∀start_status, final_status: Status. 472 ∀code_memory: BitVectorTrie Byte 16. 473 ∀program_size: nat. 474 ∀cost_labels: BitVectorTrie costlabel 16. 475 ∀trace_ends_flag: trace_ends_with_ret. 476 ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 477 let start_program_counter ≝ program_counter … start_status in 478 let final_program_counter ≝ program_counter … final_status in 479 reachable_program_counter code_memory program_size start_program_counter → 480 nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter). 481 cases daemon 482 qed. 483 484 lemma reachable_program_counter_to_compute_trace_label_label_length_le_program_size: 485 ∀start_status, final_status: Status. 486 ∀code_memory: BitVectorTrie Byte 16. 487 ∀program_size: nat. 488 ∀cost_labels: BitVectorTrie costlabel 16. 489 ∀trace_ends_flag: trace_ends_with_ret. 490 ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 491 let start_program_counter ≝ program_counter … start_status in 492 let final_program_counter ≝ program_counter … final_status in 493 reachable_program_counter code_memory program_size start_program_counter → 494 nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter). 495 #start_status #final_status #code_memory #program_size #cost_labels #trace_ends_flag #the_trace 496 cases daemon 497 qed. 498 499 corollary reachable_program_counter_to_compute_trace_length_le_program_size: 500 ∀start_status, final_status: Status. 501 ∀code_memory: BitVectorTrie Byte 16. 502 ∀program_size: nat. 503 ∀cost_labels: BitVectorTrie costlabel 16. 504 ∀trace_ends_flag: trace_ends_with_ret. 505 ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 506 let program_counter ≝ program_counter … start_status in 507 reachable_program_counter code_memory program_size program_counter → 508 trace_length start_status final_status ≤ program_size. 509 cases daemon 510 qed. *) 511 512 include alias "arithmetics/nat.ma". 513 include alias "basics/logic.ma". 514 515 lemma and_intro_right: 516 ∀a, b: Prop. 517 a → (a → b) → a ∧ b. 518 #a #b /3/ 519 qed. 520 521 lemma lt_m_n_to_exists_o_plus_m_n: 522 ∀m, n: nat. 523 m < n → ∃o: nat. m + o = n. 524 #m #n 525 cases m 526 [1: 527 #irrelevant 528 %{n} % 529 2: 530 #m' #lt_hyp 531 %{(n  S m')} 532 >commutative_plus in ⊢ (??%?); 533 <plus_minus_m_m 534 [1: 535 % 536 2: 537 @lt_S_to_lt 538 assumption 539 ] 540 ] 541 qed. 542 543 lemma lt_O_n_to_S_pred_n_n: 544 ∀n: nat. 545 0 < n → S (pred n) = n. 546 #n 547 cases n 548 [1: 549 #absurd 550 cases(lt_to_not_zero 0 0 absurd) 551 2: 552 #n' #lt_hyp % 553 ] 554 qed. 555 556 lemma exists_plus_m_n_to_exists_Sn: 557 ∀m, n: nat. 558 m < n → ∃p: nat. S p = n. 559 #m #n 560 cases m 561 [1: 562 #lt_hyp %{(pred n)} 563 @(lt_O_n_to_S_pred_n_n … lt_hyp) 564 2: 565 #m' #lt_hyp %{(pred n)} 566 @(lt_O_n_to_S_pred_n_n) 567 @(transitive_le … (S m') …) 568 [1: 569 // 570 2: 571 @lt_S_to_lt 572 assumption 573 ] 574 ] 575 qed. 576 577 578 let rec block_cost_trace_any_label_static_dynamic_ok 579 (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 580 (trace_ends_flag: ?) (start_status: Status) (final_status: Status) 581 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 582 on the_trace: 583 let code_memory ≝ code_memory … start_status in 584 let program_counter ≝ program_counter … start_status in 585 ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. 586 ∀good_program_witness: good_program code_memory total_program_size. 587 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 588 block_cost code_memory program_counter total_program_size cost_labels reachable_program_counter_witness good_program_witness = 589 compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ ?. 590 letin code_memory ≝ (code_memory … start_status) 591 letin program_counter ≝ (program_counter … start_status) 592 #reachable_program_counter_witness #good_program_witness 593 generalize in match (refl … final_status); 594 generalize in match (refl … start_status); 595 cases the_trace in ⊢ (???% → ???% → %); 596 [1: 597 #start_status' #final_status' #execute_hyp #classifier_hyp #costed_hyp 598 #start_status_refl #final_status_refl destruct 599 whd in match (trace_any_label_length ? ? ? ? ?); 600 whd in match (compute_paid_trace_any_label ? ? ? ? ?); 601 @and_intro_right 602 [1: 603 generalize in match reachable_program_counter_witness; 604 whd in match (reachable_program_counter code_memory total_program_size program_counter); 605 * #irrelevant #relevant 606 lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant) 607 #hyp assumption 608 2: 609 * #n #trace_length_hyp 610 whd in match block_cost; normalize nodelta 611 generalize in match reachable_program_counter_witness; 612 generalize in match good_program_witness; 613 <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?); (* 614 reachable_program_counter_witness #reachable_program_counter_witness 615 good_program_witness #good_program_witness 616 whd in ⊢ (??%?); @pair_elim *) 617 ] 618 2: 619 #start_status' #final_status' #execute_hyp #classified_hyp 620 #start_status_refl #final_status_refl destruct 621 whd in match (trace_any_label_length ? ? ? ? ?); 622 whd in match (compute_paid_trace_any_label ? ? ? ? ?); 623 @and_intro_right 624 [1: 625 generalize in match reachable_program_counter_witness; 626 whd in match (reachable_program_counter code_memory total_program_size program_counter); 627 * #irrelevant #relevant 628 lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant) 629 #hyp assumption 630 2: 631 * #n #trace_length_hyp 632 whd in match block_cost; normalize nodelta 633 generalize in match reachable_program_counter_witness; 634 generalize in match good_program_witness; 635 <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?); 636 reachable_program_counter_witness #reachable_program_counter_witness 637 good_program_witness #good_program_witness 638 whd in match (0 + S n); whd in ⊢ (??%?); 639 ] 640 3: 641 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 642 #status_final #execute_hyp #classifier_hyp #after_return_hyp 643 #trace_label_return #trace_any_label #start_status_refl #final_status_refl 644 destruct 645 whd in match (trace_any_label_length ? ? ? ? ?); 646 whd in match (compute_paid_trace_any_label ? ? ? ? ?); 647 @and_intro_right 648 [1: 649 2: 650 ] 651 4: 652 #end_flag #status_pre #status_init #status_end #execute_hyp #trace_any_label 653 #classifier_hyp #costed_hyp #start_status_refl #final_status_refl 654 destruct 655 whd in match (trace_any_label_length ? ? ? ? ?); 656 whd in match (compute_paid_trace_any_label ? ? ? ? ?); 657 @and_intro_right 658 [1: 659 2: 660 ] 661 ] 662 ] 663 664 corollary block_cost_trace_label_labelstatic_dynamic_ok: 665 ∀program_size: nat. 666 ∀cost_labels: BitVectorTrie costlabel 16. 667 ∀trace_ends_flag. 668 ∀start_status: Status. 669 ∀final_status: Status. 670 ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 671 let code_memory ≝ code_memory … start_status in 672 let program_counter ≝ program_counter … start_status in 673 ∀reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter. 674 ∀good_program_witness: good_program code_memory program_size. 675 (∃n: nat. trace_length start_status final_status + n = program_size) ∧ 676 block_cost code_memory program_counter program_size program_size cost_labels reachable_program_counter_witness good_program_witness ? = 677 compute_paid_trace_label_label cost_labels trace_ends_flag start_status final_status the_trace. 678 [2: 679 @le_plus_n_r 680 1: 681 #program_size #cost_labels #trace_ends_flag #start_status #final_status 682 #the_trace normalize nodelta 683 #reachable_program_counter_witness #good_program_witness 684 generalize in match start_status; 685 qed. 478 686 479 687 (*
Note: See TracChangeset
for help on using the changeset viewer.