Changeset 1964
 Timestamp:
 May 17, 2012, 12:06:34 PM (8 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1962 r1964 14 14 (program_counter …) 15 15 (λs,class. ASM_classify … s = class) 16 ( current_instruction_label code_memorycost_labels)16 (λpc.lookup_opt ?? pc cost_labels) 17 17 (next_instruction_properly_relates_program_counters code_memory) 18 18 ?. 
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 
src/ASM/Interpret.ma
r1962 r1964 18 18 #a #b 19 19 cases a cases b 20 normalize21 20 #K 22 try %23 cases (eq_true_false K)21 try cases (eq_true_false K) 22 % 24 23 qed. 25 24 
src/ASM/Util.ma
r1937 r1964 1064 1064 2: 1065 1065 #n' #inductive_hypothesis normalize 1066 #absurd @inductive_hypothesis /2 /1066 #absurd @inductive_hypothesis /2 by injective_S/ 1067 1067 ] 1068 1068 qed. … … 1433 1433 #T #x #y #H @option_destruct_Some @H 1434 1434 qed. 1435 1436 lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?. 1437 #A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS') 1438 qed. 1439 1440 coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝ 1441 not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?. 
src/common/StructuredTraces.ma
r1949 r1964 20 20 ; as_pc_of : as_status → as_pc 21 21 ; as_classifier : as_status → status_class → Prop 22 ; as_label : as_status→ option costlabel22 ; as_label_of_pc : as_pc → option costlabel 23 23 ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop 24 24 ; as_final: as_status → Prop 25 25 }. 26 27 definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc … (as_pc_of … s). 26 28 27 29 (* temporary alias for backward compatibility *) … … 435 437 tal_rel … tl1 tal2 (* < this makes it many to many *) 436 438 ]. 439 440 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2). 441 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2). 442 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2). 443 437 444 438 445 let rec flatten_trace_label_label … … 440 447 (start_status: S) (final_status: S) 441 448 (the_trace: trace_label_label S trace_ends_flag start_status final_status) 442 on the_trace: list (Σl: costlabel. ∃ s. as_label S s= Some … l) ≝449 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 443 450 match the_trace with 444 451 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ … … 455 462 (start_status: S) (final_status: S) 456 463 (the_trace: trace_any_label S trace_ends_flag start_status final_status) 457 on the_trace: list (Σl: costlabel. ∃s. as_label … s= Some … l) ≝464 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 458 465 match the_trace with 459 466 [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] … … 473 480 (start_status: S) (final_status: S) 474 481 (the_trace: trace_label_return S start_status final_status) 475 on the_trace: list (Σl: costlabel. ∃s. as_label … s= Some … l) ≝482 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 476 483 match the_trace with 477 484 [ tlr_base before after trace_to_lift ⇒ … … 485 492 cases abs abs #abs @abs % 486 493 1: 487 %{initial} whd in match label; 494 %{(as_pc_of … initial)} whd in match label; 495 change with (as_label ?? = ?) 488 496 generalize in match labelled_proof; whd in ⊢ (% → ?); 489 497 cases (as_label S initial) … … 595 603 qed. 596 604 605 definition as_cost_map ≝ 606 λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. 607 608 definition lift_cost_map_id : 609 ∀S_in, S_out: abstract_status. 610 (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) + 611 ¬(∃pc.as_label_of_pc S_out pc = Some … l)) → 612 (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig. 613 match dec l_sig with 614 [ inl prf ⇒ m «l_sig, prf» 615  inr _ ⇒ 0 (* labels not present in out code get 0 *) 616 ]. 617 618 lemma lift_cost_map_id_eq : 619 ∀S_in, S_out, dec, m, l_in, l_out. 620 pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out. 621 #S_in #S_out #dec #m #l_in * #l_out #prf #EQ 622 whd in match lift_cost_map_id; normalize nodelta 623 cases (dec l_in) normalize nodelta >EQ 624 [2: #H @⊥] /2 by refl, absurd/ 625 qed. 626 627 notation > "Σ_{ ident i ∈ l } f" 628 with precedence 20 629 for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. 630 notation < "Σ_{ ident i ∈ l } f" 631 with precedence 20 632 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 633 634 definition as_cost_of_trace_any_label : 635 ∀S : abstract_status. 636 ∀fl, start, end. 637 as_cost_map S → 638 trace_any_label S fl start end → ℕ ≝ 639 λS,fl,start,end,m,the_trace. 640 Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig). 641 642 definition as_cost_of_trace_label_label : 643 ∀S : abstract_status. 644 ∀fl, start, end. 645 as_cost_map S → 646 trace_label_label S fl start end → ℕ ≝ 647 λS,fl,start,end,m,the_trace. 648 Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig). 649 650 definition as_cost_of_trace_label_return : 651 ∀S : abstract_status. 652 ∀start, end. 653 as_cost_map S → 654 trace_label_return S start end → ℕ ≝ 655 λS,start,end,m,the_trace. 656 Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig). 657 658 lemma lift_cost_map_same_cost : 659 ∀S_in, S_out, dec, m_out, trace_in, trace_out. 660 map … (pi1 ??) trace_in = map … (pi1 ??) trace_out → 661 (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) = 662 (Σ_{ l_sig ∈ trace_out } (m_out l_sig)). 663 #S_in #S_out #dec #m_out #trace_in elim trace_in 664 [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out] 665 normalize in ⊢ (%→?); 666 [2,3: #ABS destruct(ABS) 667 4: #_ % 668 1: 669 #EQ destruct 670 whd in ⊢(??%%); 671 >(lift_cost_map_id_eq … e0) 672 >e0 in e1; normalize in ⊢(%→?); #EQ 673 >(IH … EQ) % 674 ] 675 qed. 676 677 lemma lift_cost_map_same_cost_tal : 678 ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. 679 ∀the_trace_in : trace_any_label S_in f_in start_in end_in. 680 ∀the_trace_out : trace_any_label S_out f_out start_out end_out. 681 tal_rel … the_trace_in the_trace_out → 682 as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 683 as_cost_of_trace_any_label … m_out the_trace_out. 684 #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out 685 #tal_in #tal_out #H_tal 686 @(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal)) 687 qed. 688 689 lemma lift_cost_map_same_cost_tll : 690 ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. 691 ∀the_trace_in : trace_label_label S_in f_in start_in end_in. 692 ∀the_trace_out : trace_label_label S_out f_out start_out end_out. 693 tll_rel … the_trace_in the_trace_out → 694 as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 695 as_cost_of_trace_label_label … m_out the_trace_out. 696 #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out 697 #tll_in #tll_out #H_tll 698 @(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll)) 699 qed. 700 701 lemma lift_cost_map_same_cost_tlr : 702 ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out. 703 ∀the_trace_in : trace_label_return S_in start_in end_in. 704 ∀the_trace_out : trace_label_return S_out start_out end_out. 705 tlr_rel … the_trace_in the_trace_out → 706 as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 707 as_cost_of_trace_label_return … m_out the_trace_out. 708 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out 709 #tlr_in #tlr_out #H_tlr 710 @(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr)) 711 qed.
Note: See TracChangeset
for help on using the changeset viewer.