Changeset 1964 for src/ASM/CostsProof.ma
- Timestamp:
- May 17, 2012, 12:06:34 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1935 r1964 386 386 387 387 definition tech_cost_of_label0: 388 ∀code_memory: BitVectorTrie Byte 16.389 388 ∀cost_labels: BitVectorTrie costlabel 16. 390 389 ∀cost_map: identifier_map CostTag nat. 391 390 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 392 ∀ctrace:list (Σk:costlabel.∃ s: ASM_abstract_status code_memory cost_labels. as_label …s = Some ? k).391 ∀ctrace:list (Σk:costlabel.∃b.lookup_opt … b cost_labels = Some ? k). 393 392 ∀i,p. present … cost_map (nth_safe ? i ctrace p). 394 #co de_memory #cost_labels #cost_map #codom_dom #ctrace #i #p393 #cost_labels #cost_map #codom_dom #ctrace #i #p 395 394 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K 396 395 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres) … … 448 447 449 448 definition tech_cost_of_label: 450 ∀code_memory: BitVectorTrie Byte 16.451 449 ∀cost_labels: BitVectorTrie costlabel 16. 452 450 ∀cost_map: identifier_map CostTag nat. 453 451 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 454 list (Σk:costlabel.∃ s: ASM_abstract_status code_memory cost_labels. as_label …s = Some ? k) →452 list (Σk:costlabel.∃b.lookup_opt … b cost_labels = Some ? k) → 455 453 nat → nat 456 ≝ λco de_memory,cost_labels,cost_map,codom_dom,ctrace,i.454 ≝ λcost_labels,cost_map,codom_dom,ctrace,i. 457 455 ltb_rect ? i (|ctrace|) 458 456 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?) … … 489 487 490 488 lemma tech_cost_of_label_shift: 491 ∀co de_memory,cost_labels,cost_map,codom_dom,l1,l2,i.489 ∀cost_labels,cost_map,codom_dom,l1,l2,i. 492 490 i < |l2| → 493 tech_cost_of_label co de_memory cost_labels cost_map codom_dom l2 i =494 tech_cost_of_label co de_memory cost_labels cost_map codom_dom (l1@l2) (i+|l1|).495 #co de_memory #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H491 tech_cost_of_label cost_labels cost_map codom_dom l2 i = 492 tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|). 493 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H 496 494 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect 497 495 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2 498 496 whd in match ltb; normalize nodelta 499 [1: >le_to_leb_true try assumption applyS le_to_leb_true / /497 [1: >le_to_leb_true try assumption applyS le_to_leb_true / by / 500 498 |4: >not_le_to_leb_false try assumption applyS not_le_to_leb_false 501 499 change with (¬ ? ≤ ?) in K1; applyS K1 502 |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) / / >length_append503 applyS (monotonic_lt_plus_r … (|l1|)) / /500 |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) / by / >length_append 501 applyS (monotonic_lt_plus_r … (|l1|)) / by / 504 502 |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ] 505 503 | #H1 #H2 506 generalize in match (tech_cost_of_label0 ??? ?(l1@l2) ??);504 generalize in match (tech_cost_of_label0 ??? (l1@l2) ??); 507 505 <(shift_nth_safe … H1) #p % 508 | / / ]506 | / by / ] 509 507 qed. 510 508 511 509 lemma tech_cost_of_label_prefix: 512 ∀co de_memory,cost_labels,cost_map,codom_dom,l1,l2,i.510 ∀cost_labels,cost_map,codom_dom,l1,l2,i. 513 511 i < |l1| → 514 tech_cost_of_label co de_memory cost_labels cost_map codom_dom l1 i =515 tech_cost_of_label co de_memory cost_labels cost_map codom_dom (l1@l2) i.516 #co de_memory #cost_labels #cost_map #codom_dom #l1 #l2 #i #H512 tech_cost_of_label cost_labels cost_map codom_dom l1 i = 513 tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) i. 514 #cost_labels #cost_map #codom_dom #l1 #l2 #i #H 517 515 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect 518 516 [1: … … 522 520 |2: 523 521 #K1 #K2 524 generalize in match (tech_cost_of_label0 ??? ?(l1@l2) ??);522 generalize in match (tech_cost_of_label0 ??? (l1@l2) ??); 525 523 <(shift_nth_prefix … l1 i l2 K1 K2) // 526 524 |3: … … 539 537 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 540 538 pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres). 541 let ctrace ≝ as_compute_cost_trace_label_return (ASM_abstract_status cm cost_labels) … trace in539 let ctrace ≝ flatten_trace_label_return (ASM_abstract_status cm cost_labels) … trace in 542 540 compute_trace_label_return_cost_using_paid cm … trace = 543 (Σ_{i < |ctrace|} (tech_cost_of_label c m cost_labels cost_map codom_dom ctrace i))541 (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 544 542 ≝ ? 545 543 and compute_trace_any_label_using_paid_ok_with_trace … … 554 552 on trace: 555 553 ∀unrepeating_witness: tal_unrepeating … trace. 556 let ctrace ≝ as_compute_cost_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in554 let ctrace ≝ flatten_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in 557 555 compute_trace_any_label_cost_using_paid … trace = 558 (Σ_{i < |ctrace|} (tech_cost_of_label c m cost_labels cost_map codom_dom ctrace i))556 (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 559 557 ≝ ? 560 558 and compute_trace_label_label_using_paid_ok_with_trace … … 570 568 on trace: 571 569 ∀unrepeating_witness: tll_unrepeating … trace. 572 let ctrace ≝ as_compute_cost_trace_label_label (ASM_abstract_status cm cost_labels) … trace in570 let ctrace ≝ flatten_trace_label_label (ASM_abstract_status cm cost_labels) … trace in 573 571 compute_trace_label_label_cost_using_paid … trace = 574 (Σ_{i < |ctrace|} (tech_cost_of_label c m cost_labels cost_map codom_dom ctrace i))572 (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 575 573 ≝ ?. 576 574 cases trace normalize nodelta 577 575 [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?); 578 whd in match ( as_compute_cost_trace_label_return ????);576 whd in match (flatten_trace_label_return ????); 579 577 @compute_trace_label_label_using_paid_ok_with_trace 580 578 assumption 581 579 | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom 582 580 whd in ⊢ (??%?); 583 whd in match ( as_compute_cost_trace_label_return ????);581 whd in match (flatten_trace_label_return ????); 584 582 >append_length >bigop_sum_rev >commutative_plus @eq_f2 585 583 [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom) … … 606 604 >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom) 607 605 [1: 608 whd in match ( as_compute_cost_trace_label_label ?????);606 whd in match (flatten_trace_label_label ?????); 609 607 >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2 610 608 [1: 611 609 @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm 612 <(tech_cost_of_label_shift ??? ?[?] ? i) try assumption <(plus_n_O i) %610 <(tech_cost_of_label_shift ??? [?] ? i) try assumption <(plus_n_O i) % 613 611 |2: 614 612 change with (? = lookup_present ? ? ? ? ?) 615 generalize in match (tech_cost_of_label0 ? ? ? ? ? ? ?);613 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 616 614 normalize in match (nth_safe ? ? ? ?); 617 615 whd in costed_assm; lapply costed_assm whd in match (as_label ??); … … 687 685 ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 688 686 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres). 689 let ctrace ≝ as_compute_cost_trace_label_return … trace in687 let ctrace ≝ flatten_trace_label_return … trace in 690 688 clock … code_memory … final = 691 clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label co de_memory cost_labels cost_map codom_dom ctrace i)).689 clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)). 692 690 #code_memory #cost_labels #cost_map 693 691 #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta … … 708 706 ∀unrepeating_witness: tlr_unrepeating … trace. 709 707 let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in 710 let ctrace ≝ as_compute_cost_trace_label_return … trace in711 clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label co de_memory cost_labels cost_map ? ctrace i)).708 let ctrace ≝ flatten_trace_label_return … trace in 709 clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)). 712 710 [1: 713 711 #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
Note: See TracChangeset
for help on using the changeset viewer.