 Timestamp:
 Dec 15, 2011, 12:02:40 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1587 r1619 3 3 include "ASM/Status.ma". 4 4 include "common/StructuredTraces.ma". 5 include "arithmetics/bigops.ma". 6 include alias "arithmetics/nat.ma". 7 include alias "basics/logic.ma". 5 8 6 9 let rec compute_max_trace_label_label_cost … … 155 158 #start_status #final_status #is_next #is_not_return try (#is_costed) 156 159 change with (current_instruction_cost start_status) in ⊢ (???(?%?)); 157 cases(is_next) 158 cases(execute_1 start_status) 159 whd in match eject; normalize nodelta; 160 #the_status #assm >assm % 160 cases(is_next) @execute_1_ok 161 161 3: 162 162 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call … … 173 173 status_after_fun_call call_trace) 174 174 cases(is_next) in match (clock … status_start_fun_call); 175 cases(execute_1 status_pre_fun_call); 176 #the_status 177 whd in match eject; normalize nodelta; 178 #assm >assm 175 >(execute_1_ok status_pre_fun_call) 179 176 <associative_plus in ⊢ (??%?); 180 177 <commutative_plus in match ( … … 207 204 status_init status_end trace_any_label) 208 205 cases(is_next) in match (clock … status_init); 209 cases(execute_1 status_pre) 210 #the_status whd in match eject; normalize nodelta; 211 #assm >assm <associative_plus in ⊢ (??%?); 212 >commutative_plus in match ( 213 compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label 214 + current_instruction_cost status_pre); 215 % 206 >(execute_1_ok status_pre) 207 >commutative_plus >associative_plus >associative_plus @eq_f 208 @commutative_plus 216 209 ] 217 210 3: … … 391 384 [ None ⇒ λabs. ⊥ 392 385  Some l ⇒ λ_. l ] labelled_proof in 393 ( dp… label ?)::compute_cost_trace_any_label … given_trace386 (mk_Sig … label ?)::compute_cost_trace_any_label … given_trace 394 387 ] 395 388 and compute_cost_trace_any_label … … 452 445 *) 453 446 454 include "arithmetics/bigops.ma".455 456 447 (* This shoudl go in bigops! *) 457 448 theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B. … … 495 486 times ≡ prod ? ? S. 496 487 497 notation "Σ_{ ident i < n } f"488 notation > "Σ_{ ident i < n } f" 498 489 with precedence 20 499 490 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}. 491 492 notation < "Σ_{ ident i < n } f" 493 with precedence 20 494 for @{'bigop $n plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f)}. 500 495 501 496 axiom code_memory_ro_label_label: … … 522 517 % #abs destruct (abs) 523 518 qed. 519 520 include alias "arithmetics/nat.ma". 521 include alias "basics/logic.ma". 524 522 525 523 lemma ltb_rect: … … 596 594 i < l1 → 597 595 tech_cost_of_label cost_labels cost_map codom_dom l2 i = 598 tech_cost_of_label cost_labels cost_mnth_safe ? i ctrace H) ?ap codom_dom (l1@l2) (i+l1). 599 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H 600 cut (ltb i (l2) = ltb (i+l1) (l1@l2)) 601 [ change with (leb ?? = leb ??); @leb_elim 602 [ #H1 change with (i < ?) in H1; >le_to_leb_true [//] change with (? < ?) 603 >append_length >commutative_plus @monotonic_lt_plus_r // 604  #H1 change with (¬ i < ?) in H1; >not_le_to_leb_false [//] 605 >append_length >commutative_plus % #H2 606 change with (? < ?) in H2; @(absurd ?? H1) @(lt_plus_to_lt_r … H2) ] 607  #E whd in match tech_cost_of_label; normalize nodelta 608 @same_ltb_rect [@E] 609 [ #K1 #K2 lapply (shift_nth_safe ? i l1 l2 K1 K2) #H check eq_f 610 lapply (eq_f ?? (lookup_present CostTag nat cost_Map) ?? H) 611 612 613 614 cut (decide_bool (ltb i (l2)) = decide_bool (ltb (i+(l1)) (l1@l2))) 615 whd in match tech_cost_of_label; normalize nodelta 616 596 tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+l1). 597 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H 598 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect 599 [ @(ltb_rect ? i (l2)) @(ltb_rect ? (i+l1) (l1@l2)) #K1 #K2 600 whd in match ltb; normalize nodelta 601 [1: >le_to_leb_true try assumption applyS le_to_leb_true // 602 4: >not_le_to_leb_false try assumption applyS not_le_to_leb_false 603 change with (¬ ? ≤ ?) in K1; applyS K1 604 2: @⊥ @(absurd (i+l1 < l1@l2)) // >length_append 605 applyS (monotonic_lt_plus_r … (l1)) // 606 3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ] 607  #H1 #H2 608 generalize in match (tech_cost_of_label0 ??? (l1@l2) ??); 609 <(shift_nth_safe … H1) #p % 610  // ] 611 qed. 617 612 618 613 let rec compute_max_trace_label_return_cost_ok_with_trace … … 627 622 let ctrace ≝ compute_cost_trace_label_return … trace in 628 623 compute_max_trace_label_return_cost … trace = 629 Σ_{i < ctrace} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)624 (Σ_{i < ctrace} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 630 625 ≝ ?. 631 626 lapply (refl … initial) cases trace in ⊢ (??%? → %); … … 640 635 2: @codom_dom 641 636 4:lapply (code_memory_ro_label_label … tr1) >E #E2 <E2 @dom_codom] 642 @same_bigop [//] #i #H #_ dom_codom 643 generalize in match (compute_cost_trace_label_return cost_labels sl sf tr2); #l1 644 generalize in match (compute_cost_trace_label_label cost_labels doesnt_end_with_ret si sl tr1); 645 646 i < l1 → 647 tech_cost_of_label cost_labels cost_map codom_dom l1 i = 648 tech_cost_of_label cost_labels cost_map codom_dom (l2@l1) (i+l1) 649 650 651 whd in ⊢ (??%%); 637 @same_bigop [//] #i #H #_ dom_codom @tech_cost_of_label_shift 638 652 639  653 640 ]
Note: See TracChangeset
for help on using the changeset viewer.