 Timestamp:
 Jan 13, 2012, 6:11:39 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1642 r1645 205 205  _ ⇒ λother: False. ⊥ 206 206 ] (subaddressing_modein … addr) 207  JMP addr ⇒ True (* XXX: JMP is used for fptrs and unconstrained *) 207  JMP addr ⇒ (* XXX: JMP is used for fptrs and unconstrained *) 208 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ 209 nat_of_bitvector … program_counter' < total_program_size 208 210  MOVC src trgt ⇒ 209 211 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ … … 346 348 qed. 347 349 348 axiom subaddressing_mode_elim': 350 lemma subaddressing_mode_elim': 351 ∀T: Type[2]. 352 ∀n: nat. 353 ∀o: nat. 354 ∀Q: addressing_mode → T → Prop. 355 ∀fixed_v: Vector addressing_mode_tag (n + o). 356 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 357 ∀v1: Vector addressing_mode_tag n. 358 ∀v2: Vector addressing_mode_tag o. 359 ∀fixed_v_proof: fixed_v = v1 @@ v2. 360 ∀subaddressing_mode_proof. 361 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 362 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. 363 #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 364 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof 365 cases daemon 366 qed. 367 368 axiom subaddressing_mode_elim: 349 369 ∀T: Type[2]. 350 370 ∀m: nat. 371 ∀n: nat. 372 ∀Q: addressing_mode → T → Prop. 351 373 ∀fixed_v: Vector addressing_mode_tag m. 352 ∀Q: addressing_mode → T → Prop.353 374 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 354 ∀n: nat.355 375 ∀v: Vector addressing_mode_tag n. 356 376 ∀proof. 357 377 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 358 378 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 359 (* #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v360 elim v361 [ #proof normalize362 363 qed. *)364 379 365 380 (* … … 406 421 n < o → m + n < m + o. 407 422 #m #n #o #assm /2 by monotonic_le_plus_r/ 408 qed. 409 410 (* 411 axiom blah: 412 ∀instruction: instruction. 413 ∀program_counter': Word. 414 ∀ticks, n: nat. 415 ∀code_memory: BitVectorTrie Byte 16. 416 〈instruction,program_counter',ticks〉 = fetch code_memory (fetch_program_counter_n n code_memory (zero 16)) → 417 program_counter' = fetch_program_counter_n (S n) code_memory (zero …). 418 *) 423 qed. 419 424 420 425 let rec block_cost … … 469 474 lapply(good_program_witness program_counter reachable_program_counter_witness) 470 475 <FETCH normalize nodelta <instr normalize nodelta 471 @(subaddressing_mode_elim '… [[addr11]] … [[addr11]]) [1: // ] #new_addr476 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 472 477 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 473 478 cases (split … 3 8 new_addr) #thr #eig normalize nodelta … … 489 494 lapply(good_program_witness program_counter reachable_program_counter_witness) 490 495 <FETCH normalize nodelta <instr normalize nodelta 491 @(subaddressing_mode_elim '… [[addr11]] … [[addr11]]) [1: // ] #new_addr496 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 492 497 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 493 498 cases (split … 3 8 new_addr) #thr #eig normalize nodelta … … 506 511 lapply(good_program_witness program_counter reachable_program_counter_witness) 507 512 <FETCH normalize nodelta <instr normalize nodelta 508 @(subaddressing_mode_elim '… [[addr16]] … [[addr16]]) [1: // ] #new_addr513 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 509 514 * * * * #n' 510 515 #_ #_ #program_counter_lt' #program_counter_lt_tps' … … 524 529 lapply(good_program_witness program_counter reachable_program_counter_witness) 525 530 <FETCH normalize nodelta <instr normalize nodelta 526 @(subaddressing_mode_elim '… [[addr16]] … [[addr16]]) [1: // ] #new_addr531 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 527 532 * * * * #n' 528 533 #_ #_ #program_counter_lt' #program_counter_lt_tps' … … 535 540 assumption 536 541 ] 537 6: 538 cases daemon (* XXX *) 539 7: 540 cases daemon (* XXX *) 541 8: 542 6,8: (* JMP and MOVC *) 542 543 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 543 544 lapply(good_program_witness program_counter reachable_program_counter_witness) … … 556 557 nat_of_bitvector … program_counter') 557 558 assumption 558  9:559 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 560 lapply(good_program_witness program_counter reachable_program_counter_witness) 561 559 7,9: 560 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 561 lapply(good_program_witness program_counter reachable_program_counter_witness) 562 <FETCH normalize nodelta <instr normalize nodelta * 562 563 #program_counter_lt' #program_counter_lt_tps' % 563 [1 :564 [1,3: 564 565 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 565 566 <FETCH normalize nodelta whd in match ltb; normalize nodelta 566 567 >(le_to_leb_true … program_counter_lt') % 567 2 :568 2,4: 568 569 assumption 569 570 ] … … 572 573 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 573 574 lapply(good_program_witness program_counter reachable_program_counter_witness) 574 575 <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * 575 576 #program_counter_lt' #program_counter_lt_tps' % 576 [1: 577 try assumption 578 [*: 577 579 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 578 580 <FETCH normalize nodelta whd in match ltb; normalize nodelta 579 581 >(le_to_leb_true … program_counter_lt') % 580 2:581 assumption582 582 ] 583 583 10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52, … … 601 601 ] 602 602 qed. 603 604 605 606 607 608 609 610 [1: (* ACALL *) 611 generalize in match good_program_witness; 612 whd in match good_program; normalize nodelta 613 cases FETCH normalize nodelta 614 cases instr normalize nodelta 615 @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr 616 cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta 617 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 618 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 619 #assm cases assm #ignore 620 whd in match good_program_counter; normalize nodelta * #n * * 621 #program_counter_eq #program_counter_lt_total_program_size 622 #fetch_n_leq_program_counter 623 @(transitive_le 624 total_program_size 625 ((S program_size') + nat_of_bitvector … program_counter) 626 (program_size' + nat_of_bitvector … program_counter') recursive_case) 627 normalize in match (S program_size' + nat_of_bitvector … program_counter); 628 >plus_n_Sm 629 @monotonic_le_plus_r 630 change with ( 631 nat_of_bitvector … program_counter < 632 nat_of_bitvector … program_counter') 633 >program_counter_eq in FETCH; #hyp 634 >(blah … hyp) 635 <program_counter_eq assumption 636 2: 637 generalize in match good_program_witness; 638 whd in match good_program; normalize nodelta 639 cases FETCH normalize nodelta 640 cases instr normalize nodelta 641 @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr 642 cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta 643 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 644 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 645 #assm cases assm #ignore 646 whd in match good_program_counter; normalize nodelta * #n * * 647 #program_counter_eq #program_counter_lt_total_program_size 648 #fetch_n_leq_program_counter 649 650 whd in match good_program; normalize nodelta 651 @pair_elim #lft #rgt normalize nodelta #fetch_hyp 652 @pair_elim #instruction #program 653 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52, 654 54,56,58,60,62: 655 3: (* LCALL *) 656 generalize in match good_program_witness; 657 whd in match good_program; normalize nodelta 658 cases FETCH normalize nodelta 659 cases instr normalize nodelta 660 @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr 661 * #irrelevant 662 whd in match good_program_counter; normalize nodelta * #n * * 663 #program_counter_eq #program_counter_lt_total_program_size 664 #fetch_n_leq_program_counter 665 @(transitive_le 666 total_program_size 667 ((S program_size') + nat_of_bitvector … program_counter) 668 (program_size' + nat_of_bitvector … program_counter') recursive_case) 669 normalize in match (S program_size' + nat_of_bitvector … program_counter); 670 >plus_n_Sm 671 @monotonic_le_plus_r 672 change with ( 673 nat_of_bitvector … program_counter < 674 nat_of_bitvector … program_counter') 675 >program_counter_eq in FETCH; #hyp 676 >(blah … hyp) 677 <program_counter_eq assumption 678 5,7: (* JMP and MOVC *) 679 generalize in match good_program_witness; 680 whd in match good_program; normalize nodelta 681 cases FETCH normalize nodelta 682 cases instr normalize nodelta 683 9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47, 684 49,51,53,55,57,59,61,63: (* ADD and similar nonbranching instructions *) 685 generalize in match good_program_witness; 686 whd in match good_program; normalize nodelta 687 cases FETCH normalize nodelta 688 <real_instruction_refl <instr normalize nodelta 603 604 axiom fetch_program_counter_n_Sn: 605 ∀instruction: instruction. 606 ∀program_counter, program_counter': Word. 607 ∀ticks, n: nat. 608 ∀code_memory: BitVectorTrie Byte 16. 609 Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → 610 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → 611 Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). 612 613 let rec traverse_code_internal 614 (program: list Byte) (code_memory: BitVectorTrie Byte 16) 615 (cost_labels: BitVectorTrie costlabel 16) (program_counter: Word) 616 (program_size: nat) (reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter) 617 (good_program_witness: good_program code_memory program_size) 618 (n: nat) (fetch_program_counter_proof: Some … program_counter = fetch_program_counter_n n code_memory (zero …)) 619 on program: identifier_map CostTag nat ≝ 620 let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in 621 match program with 622 [ nil ⇒ empty_map … 623  cons hd tl ⇒ 624 match lookup_opt … program_counter cost_labels with 625 [ None ⇒ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ? 626  Some lbl ⇒ 627 let cost ≝ block_cost code_memory program_counter program_size program_size cost_labels ? good_program_witness ? in 628 let cost_mapping ≝ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ? in 629 add … cost_mapping lbl cost 630 ] 631 ]. 632 [6: 633 // 634 2,4: 635 @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n) 636 assumption 637 5: 638 assumption 639 1,3: 640 whd in match reachable_program_counter; normalize nodelta 641 @conj 642 [1,3: 643 %{(S n)} 644 @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n) 645 assumption 646 2,4: 647 cases daemon (* XXX ??? *) 648 ] 689 649 ] 690 whd in match good_program_counter; normalize nodelta * #n * * 691 #program_counter_eq #program_counter_lt_total_program_size 692 #fetch_n_leq_program_counter 693 @(transitive_le 694 total_program_size 695 (S program_size' + nat_of_bitvector … program_counter) 696 (program_size' + nat_of_bitvector … program_counter') 697 recursive_case) 698 normalize in match (S program_size' + nat_of_bitvector … program_counter); 699 >plus_n_Sm 700 @monotonic_le_plus_r 701 change with ( 702 nat_of_bitvector … program_counter < 703 nat_of_bitvector … program_counter') 704 >program_counter_eq in FETCH; #hyp 705 >(blah … hyp) 706 <program_counter_eq assumption 707 qed. 708 709 (* XXX: use memoisation here in the future *) 710 let rec block_cost 711 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 712 (program_counter: Word) (program_size: nat) (total_program_size: nat) 713 (size_invariant: total_program_size ≤ code_memory_size) 714 (pc_invariant: nat_of_bitvector … program_counter < total_program_size) 715 on program_size: total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat ≝ 716 match program_size return λprogram_size: nat. total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat with 717 [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *) 718  S program_size ⇒ λrecursive_case. 719 let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in 720 match lookup_opt … newpc cost_labels return λx: option costlabel. nat with 721 [ None ⇒ 722 let classify ≝ ASM_classify0 instr in 723 match classify return λx. classify = x → ? with 724 [ cl_jump ⇒ λclassify_refl. ticks 725  cl_call ⇒ λclassify_refl. (* ite here *) 726 ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 727  cl_return ⇒ λclassify_refl. ticks 728  cl_other ⇒ λclassify_refl. (* ite here *) 729 ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 730 ] (refl … classify) 731  Some _ ⇒ ticks 732 ] 733 ]. 734 735 let rec traverse_code_internal 736 (program: list Byte) (mem: BitVectorTrie Byte 16) 737 (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) 738 on program: identifier_map CostTag nat ≝ 739 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in 740 match program with 741 [ nil ⇒ empty_map … 742  cons hd tl ⇒ 743 match lookup_opt … pc cost_labels with 744 [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size 745  Some lbl ⇒ 746 let cost ≝ block_cost mem cost_labels pc program_size in 747 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 748 add … cost_mapping lbl cost ]]. 650 qed. 749 651 750 652 definition traverse_code ≝ 751 653 λprogram: list Byte. 752 λ mem: BitVectorTrie Byte 16.654 λcode_memory: BitVectorTrie Byte 16. 753 655 λcost_labels. 754 656 λprogram_size: nat. 755 traverse_code_internal program mem cost_labels (zero …) program_size. 657 λprogram_not_empty_proof: 0 < program_size. 658 λgood_program_witness: good_program code_memory program_size. 659 traverse_code_internal program code_memory cost_labels (zero …) program_size ? good_program_witness. 660 normalize @conj 661 [2: 662 assumption 663 1: 664 %{0} % 665 ] 666 qed. 756 667 757 668 definition compute_costs ≝ … … 759 670 λcost_labels: BitVectorTrie costlabel 16. 760 671 λhas_main: bool. 761 let program_size ≝ program + 1 in 762 let memory ≝ load_code_memory program in 763 traverse_code program memory cost_labels program_size. 672 λgood_program_witness: good_program (load_code_memory program) (program + 1). 673 λprogram_not_empty_proof: 0 < program. 674 let program_size ≝ program + 1 in 675 let code_memory ≝ load_code_memory program in 676 traverse_code program code_memory cost_labels program_size ?. 677 // 678 qed.
Note: See TracChangeset
for help on using the changeset viewer.