Changeset 1561 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 25, 2011, 1:13:15 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1558 r1561 3 3 include "ASM/Status.ma". 4 4 include "common/StructuredTraces.ma". 5 6 definition current_instruction ≝7 λs: Status.8 let pc ≝ program_counter … s in9 \fst (\fst (fetch … (code_memory … s) pc)).10 11 definition ASM_classify: Status → status_class ≝12 λs.13 match current_instruction s with14 [ RealInstruction pre ⇒15 match pre with16 [ RET ⇒ cl_return17  JZ _ ⇒ cl_jump18  JNZ _ ⇒ cl_jump19  JC _ ⇒ cl_jump20  JNC _ ⇒ cl_jump21  JB _ _ ⇒ cl_jump22  JNB _ _ ⇒ cl_jump23  JBC _ _ ⇒ cl_jump24  CJNE _ _ ⇒ cl_jump25  DJNZ _ _ ⇒ cl_jump26  _ ⇒ cl_other27 ]28  ACALL _ ⇒ cl_call29  LCALL _ ⇒ cl_call30  JMP _ ⇒ cl_call31  AJMP _ ⇒ cl_jump32  LJMP _ ⇒ cl_jump33  SJMP _ ⇒ cl_jump34  _ ⇒ cl_other35 ].36 37 definition current_instruction_is_labelled ≝38 λcost_labels: BitVectorTrie costlabel 16.39 λs: Status.40 let pc ≝ program_counter … s in41 match lookup_opt … pc cost_labels with42 [ None ⇒ False43  _ ⇒ True44 ].45 46 definition label_of_current_instruction:47 BitVectorTrie costlabel 16 → Status → list costlabel48 ≝49 λcost_labels,s.50 let pc ≝ program_counter … s in51 match lookup_opt … pc cost_labels with52 [ None ⇒ []53  Some l ⇒ [l]54 ].55 56 definition next_instruction_properly_relates_program_counters ≝57 λbefore: Status.58 λafter : Status.59 let size ≝ current_instruction_cost before in60 let pc_before ≝ program_counter … before in61 let pc_after ≝ program_counter … after in62 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in63 sum = pc_after.64 65 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝66 λcost_labels.67 mk_abstract_status68 Status69 (λs,s'. eject … (execute_1 s) = s')70 (λs,class. ASM_classify s = class)71 (current_instruction_is_labelled cost_labels)72 next_instruction_properly_relates_program_counters.73 5 74 6 (* … … 290 222 include alias "arithmetics/nat.ma". 291 223 292 (* 224 (*Useless now? 293 225 lemma minus_m_n_minus_minus_plus_1: 294 226 ∀m, n: nat. … … 297 229 /3 by lt_plus_to_minus_r, plus_minus/ 298 230 qed. 299 *)300 231 301 232 lemma plus_minus_rearrangement_1: … … 314 245 (m  n) + (n  o) = m  o. 315 246 /2 by plus_minus_rearrangement_1/ 316 qed. 247 qed.*) 317 248 318 249 (* … … 345 276 normalize @compute_max_trace_any_label_cost_is_ok 346 277 2: 347 cases the_trace348 [1:349 #start_status #final_status #is_next #is_not_return #is_costed350 normalize nodelta;351 change with (352 let current_instruction_cost ≝ current_instruction_cost start_status in353 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in354 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in355 call_trace_cost+current_instruction_cost+final_trace_cost356 ) in ⊢ (??%?);357 2:358 #start_status #final_status #is_next #is_return359 3:360 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call361 #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace362 change with (363 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in364 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in365 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in366 call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);367 normalize nodelta;368 >compute_max_trace_label_return_cost_is_ok369 >compute_max_trace_any_label_cost_is_ok370 4:371 ]372 278 3: 373 279 cases the_trace … … 379 285 normalize >compute_max_trace_label_label_cost_is_ok 380 286 >compute_max_trace_label_return_cost_is_ok 381 >plus_minus_rearrangement_1382 [1: %383 2:384 3:385 ]386 287 ] 387 288 ]. … … 536 437 (start_status: Status) (final_status: Status) 537 438 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 538 start_status final_status) on the_trace: list costlabel ≝ 439 start_status final_status) on the_trace: 440 list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝ 539 441 match the_trace with 540 442 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ … … 544 446 [ None ⇒ λabs. ⊥ 545 447  Some l ⇒ λ_. l ] labelled_proof in 546 label::compute_cost_trace_any_label … given_trace448 (dp … label ?)::compute_cost_trace_any_label … given_trace 547 449 ] 548 450 and compute_cost_trace_any_label … … 551 453 (start_status: Status) (final_status: Status) 552 454 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 553 on the_trace: list costlabel≝455 on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝ 554 456 match the_trace with 555 457 [ tal_base_not_return the_status _ _ _ _ ⇒ [] … … 568 470 (start_status: Status) (final_status: Status) 569 471 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 570 on the_trace: list costlabel≝472 on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝ 571 473 match the_trace with 572 474 [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift … … 576 478 labelled_cost @ return_cost 577 479 ]. 578 // 480 [ %{pc} whd in match label; generalize in match labelled_proof; whd in ⊢ (% → ?); 481 cases (lookup_opt costlabel … pc cost_labels) normalize 482 [ #abs cases abs  // ] 483  // ] 579 484 qed. 580 485 … … 595 500 start_status final_status the_trace. 596 501 597 include "arithmetics/bigops.ma". 598 599 lemma foo: 502 (* To be moved elsewhere*) 503 lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m. 504 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) // 505 qed. 506 507 (* Here I would like to use arithmetics/bigops.ma, but it requires the 508 function f to be total on nat, which is not the case here *) 509 let rec bigplus0 (b:nat) (f: ∀n:nat. n < b → nat) (n:nat) on n ≝ 510 match n return λn.n < b → nat with 511 [ O ⇒ λ_. 0 512  S k ⇒ λH. f k ? + bigplus0 b f k ? 513 ]. 514 @(le_S_n_m_to_le_n_m … H) 515 qed. 516 517 definition bigplus ≝ 518 λn,f. 519 match n return λx. x = n → nat with 520 [ O ⇒ λ_. 0 521  S m ⇒ λH. bigplus0 n f m ? ] (refl … n). 522 // 523 qed. 524 525 lemma compute_max_trace_label_return_cost_ok_with_trace: 600 526 ∀cost_labels: BitVectorTrie costlabel 16. 601 ∀cost_ labels_inv: identifier_map CostTag Word.527 ∀cost_map: identifier_map CostTag nat. 602 528 ∀initial,final. 603 529 ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final. 604 let dummy ≝ an_identifier ? one in 530 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 531 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 532 block_cost (code_memory … initial) cost_labels pc 2^16 = 533 lookup_present … k_pres). 605 534 let ctrace ≝ compute_cost_trace_label_return … trace in 606 535 compute_max_trace_label_return_cost … trace = 607 \big [ plus, 0 ]_{ i < ctrace } 608 (block_cost (code_memory … initial) cost_labels 609 (lookup_present … cost_labels_inv (nth i ? ctrace dummy) ?) 2^16). 610 [2: cases daemon (* ALL LABELS MUST BE PRESENT *) 611  #cost_labels #cost_labels_inv #initial #final #trace 612 letin dummy ≝ (an_identifier CostTag one) normalize nodelta 613 whd in match 536 bigplus (ctrace) (λi,H.lookup_present … cost_map (nth_safe ? i ctrace H) ?). 537 [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K 538 lapply (codom_dom … K) #k_pres // 539  #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom normalize nodelta 540 whd in match 614 541 615 542 lemma
Note: See TracChangeset
for help on using the changeset viewer.