Changeset 1950 for src/ASM/Policy.ma
- Timestamp:
- May 15, 2012, 6:20:31 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r1942 r1950 39 39 40 40 definition is_jump ≝ 41 λx:labelled_instruction. 42 let 〈label,instr〉 ≝ x in 41 λinstr:pseudo_instruction. 43 42 match instr with 44 43 [ Instruction i ⇒ is_jump' i … … 67 66 ]. 68 67 69 (*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝68 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝ 70 69 λprefix.λsigma. 71 70 ∀i:ℕ.i < |prefix| → 72 iff (is_jump (nth i ? prefix 〈None ?, Comment []〉)) 73 (∃x:jump_length. 74 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*) 71 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → 72 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump. 75 73 76 74 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) … … 122 120 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in 123 121 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in 124 opc ≤ pc ∧jmpleq oj j.122 (*opc ≤ pc ∧*) jmpleq oj j. 125 123 126 124 (* Policy safety *) … … 307 305 (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 308 306 0. 309 307 310 308 (* The function that creates the label-to-address map *) 311 309 definition create_label_map: ∀program:list labelled_instruction. 312 310 (Σlabels:label_map. 313 ∀i:ℕ.lt i (|program|) →314 311 ∀l.occurs_exactly_once ?? l program → 315 is_label (nth i ? program 〈None ?, Comment [ ]〉) l →316 lookup ?? labels l = Some ? i312 bitvector_of_nat ? (lookup_def ?? labels l 0) = 313 address_of_word_labels_code_mem program l 317 314 ) ≝ 318 315 λprogram. 319 316 \fst (create_label_cost_map program). 320 # i #Hi #l #Hl1 #Hl2lapply (pi2 ?? (create_label_cost_map program)) @pair_elim321 #labels #costs #EQ normalize nodelta #H @(H i Hi l Hl1 Hl2)317 #l #Hl lapply (pi2 ?? (create_label_cost_map program)) @pair_elim 318 #labels #costs #EQ normalize nodelta #H @(H l Hl) 322 319 qed. 323 320 … … 388 385 389 386 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). 390 # x cases x #l #i cases i387 #i cases i 391 388 [#id cases id 392 389 [1,2,3,6,7,33,34: … … 408 405 qed. 409 406 410 (*lemma jump_not_in_policy: ∀prefix:list labelled_instruction.411 ∀policy:(Σp:ppc_pc_map.412 out_of_program_none prefix p ∧ jump_in_policy prefix p).413 ∀i:ℕ.i < |prefix| →414 iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))415 (\snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) = None ?).416 #prefix #policy #i #Hi @conj417 [ #Hnotjmp lapply (refl ? (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉))418 cases (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) in ⊢ (???% → ?);419 #pc #j cases j420 [ #H >H @refl421 | #x #H >H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))422 >H @(ex_intro ?? x ?) / by /423 ]424 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)425 #H elim H -H; #x #H >H in Hnone; #abs destruct (abs)426 ]427 qed.*)428 429 407 (* The first step of the jump expansion: everything to short. 430 408 * The third condition of the dependent type implies jump_in_policy; … … 438 416 | Some p ⇒ 439 417 And (And (out_of_program_none (pi1 ?? program) p) 440 ( policy_isize_sum (pi1 ?? program) labelsp))418 (jump_not_in_policy (pi1 ?? program) p)) 441 419 (\fst p < 2^16) 442 420 ] ≝ … … 445 423 (λprefix.Σpolicy:ppc_pc_map. 446 424 And (out_of_program_none prefix policy) 447 ( policy_isize_sum prefix labelspolicy))425 (jump_not_in_policy prefix policy)) 448 426 program 449 427 (λprefix.λx.λtl.λprf.λp. … … 560 538 ] 561 539 ] 562 | cases daemon 540 | (* jump_not_in_policy *) #i >append_length <commutative_plus 541 #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 542 [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins cases ins 543 [ #pi cases pi normalize nodelta 544 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 545 [1,2,3,6,7,24,25: #x #y 546 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss 547 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 548 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) 549 |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,54,56: 550 @bitvector_of_nat_abs 551 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 552 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 553 @le_plus_a @Hi 554 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 555 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 556 @le_plus_n_r 557 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 558 @lt_to_not_eq @Hi 559 ] 560 ] 561 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss 562 [1,3,5,7,9,11,13,15,17: 563 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) 564 |2,4,6,8,10,12,14,16,18: 565 @bitvector_of_nat_abs 566 [1,4,7,10,13,16,19,22,25: 567 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 568 @le_plus_a @Hi 569 |2,5,8,11,14,17,20,23,26: 570 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 571 @le_plus_n_r 572 |3,6,9,12,15,18,21,24,27: 573 @lt_to_not_eq @Hi 574 ] 575 ] 576 ] 577 |2,3,4,5,6: #x [5: #y] >lookup_insert_miss 578 [1,3,5,7,9: 579 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) 580 |2,4,6,8,10: 581 @bitvector_of_nat_abs 582 [1,4,7,10,13: 583 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 584 @le_plus_a @Hi 585 |2,5,8,11,14: 586 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 587 @le_plus_n_r 588 |3,6,9,12,15: 589 @lt_to_not_eq @Hi 590 ] 591 ] 592 ] 593 | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 594 cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins cases ins 595 normalize nodelta 596 [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by / 597 |4,5: #x #H @⊥ cases H #H2 @H2 / by I/ 598 |1: #pi cases pi 599 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 600 [1,2,3,6,7,24,25: #x #y 601 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 602 #_ >lookup_insert_hit / by / 603 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 604 #H @⊥ cases H #H2 @H2 / by I/ 605 ] 606 ] 607 ] 563 608 ] 564 609 | @conj 565 610 [ #i #_ #Hi2 / by refl/ 566 | whd in match policy_isize_sum; normalize nodelta 567 cases daemon 611 | #i #H @⊥ @(absurd … H) @not_le_Sn_O 568 612 ] 569 613 ] … … 576 620 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in 577 621 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in 578 pc1 =pc2).622 \snd pc1 = \snd pc2). 579 623 580 624 (*definition nec_plus_ultra ≝ … … 588 632 include alias "basics/logic.ma". 589 633 634 lemma blerpque: ∀a,b,i. 635 is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → 636 (max_length a b) = a. 637 #a #b #i cases i 638 [1: #pi cases pi 639 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 640 [1,2,3,6,7,24,25: #x #y 641 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 642 #H cases H 643 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 644 #_ cases a cases b 645 [1,5,7,8,9: #_ / by refl/ 646 |10,14,16,17,18: #_ / by refl/ 647 |19,23,25,26,27: #_ / by refl/ 648 |28,32,34,35,36: #_ / by refl/ 649 |37,41,43,44,45: #_ / by refl/ 650 |46,50,52,53,54: #_ / by refl/ 651 |55,59,61,62,63: #_ / by refl/ 652 |64,68,70,71,72: #_ / by refl/ 653 |73,77,79,80,81: #_ / by refl/ 654 |2,3,4,6: cases x #a cases a 655 [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb 656 |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb 657 |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb 658 |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb 659 |5,6,7,10,11,12,13,14: #Hb cases Hb 660 |24,25,26,29,30,31,32,33: #Hb cases Hb 661 |43,44,45,48,49,50,51,52: #Hb cases Hb 662 |62,63,64,67,68,69,70,71: #Hb cases Hb 663 |15,34,53,72: #b #Hb #H normalize in H; destruct (H) 664 ] 665 |11,12,13,15: cases x #a cases a 666 [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb 667 |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb 668 |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb 669 |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb 670 |5,6,7,10,11,12,13,14: #Hb cases Hb 671 |24,25,26,29,30,31,32,33: #Hb cases Hb 672 |43,44,45,48,49,50,51,52: #Hb cases Hb 673 |62,63,64,67,68,69,70,71: #Hb cases Hb 674 |15,34,53,72: #b #Hb #H normalize in H; destruct (H) 675 ] 676 |20,21,22,24: cases x #a cases a 677 [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb 678 |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb 679 |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb 680 |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb 681 |5,6,7,10,11,12,13,14: #Hb cases Hb 682 |24,25,26,29,30,31,32,33: #Hb cases Hb 683 |43,44,45,48,49,50,51,52: #Hb cases Hb 684 |62,63,64,67,68,69,70,71: #Hb cases Hb 685 |15,34,53,72: #b #Hb #H normalize in H; destruct (H) 686 ] 687 |29,30,31,33: cases x #a cases a #a1 #a2 688 [1,3,5,7: cases a2 #b cases b 689 [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb 690 |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb 691 |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb 692 |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb 693 |5,6,7,10,11,12,13,14: #Hb cases Hb 694 |24,25,26,29,30,31,32,33: #Hb cases Hb 695 |43,44,45,48,49,50,51,52: #Hb cases Hb 696 |62,63,64,67,68,69,70,71: #Hb cases Hb 697 |1,8: #b #Hb #H normalize in H; destruct (H) 698 |20,27: #b #Hb #H normalize in H; destruct (H) 699 |39,46: #b #Hb #H normalize in H; destruct (H) 700 |58,65: #b #Hb #H normalize in H; destruct (H) 701 ] 702 |2,4,6,8: cases a1 #b cases b 703 [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb 704 |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb 705 |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb 706 |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb 707 |5,6,7,10,11,12,13,14: #Hb cases Hb 708 |24,25,26,29,30,31,32,33: #Hb cases Hb 709 |43,44,45,48,49,50,51,52: #Hb cases Hb 710 |62,63,64,67,68,69,70,71: #Hb cases Hb 711 |2,4: #b #Hb #H normalize in H; destruct (H) 712 |21,23: #b #Hb #H normalize in H; destruct (H) 713 |40,42: #b #Hb #H normalize in H; destruct (H) 714 |59,61: #b #Hb #H normalize in H; destruct (H) 715 ] 716 ] 717 |38,39,40,42: cases x #a cases a 718 [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb 719 |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb 720 |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb 721 |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb 722 |5,6,7,10,11,12,13,14: #Hb cases Hb 723 |24,25,26,29,30,31,32,33: #Hb cases Hb 724 |43,44,45,48,49,50,51,52: #Hb cases Hb 725 |62,63,64,67,68,69,70,71: #Hb cases Hb 726 |1,4: #b #Hb #H normalize in H; destruct (H) 727 |20,23: #b #Hb #H normalize in H; destruct (H) 728 |39,42: #b #Hb #H normalize in H; destruct (H) 729 |58,61: #b #Hb #H normalize in H; destruct (H) 730 ] 731 |47,48,49,51: cases x #a #H normalize in H; destruct (H) 732 |56,57,58,60: cases x #a #H normalize in H; destruct (H) 733 |65,66,67,69: cases x #a #H normalize in H; destruct (H) 734 |74,75,76,78: cases x #a #H normalize in H; destruct (H) 735 ] 736 ] 737 |2,3,6: #x [3: #y] #H cases H 738 |4,5: #id #_ cases a cases b 739 [2,3,4,6,11,12,13,15: normalize #H destruct (H) 740 |1,5,7,8,9,10,14,16,17,18: #H / by refl/ 741 ] 742 ] 743 qed. 744 745 lemma etblorp: ∀a,b,i.is_jump i → 746 instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. 747 #a #b #i cases i 748 [2,3,6: #x [3: #y] #H cases H 749 |4,5: #id #_ cases a cases b / by le_n/ 750 |1: #pi cases pi 751 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 752 [1,2,3,6,7,24,25: #x #y 753 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 754 #H cases H 755 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 756 #_ cases a cases b 757 [2,3: cases x #ad cases ad 758 [15,34: #b #Hb / by le_n/ 759 |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 760 |1,4,5,6,7,8,9: / by le_n/ 761 |11,12: cases x #ad cases ad 762 [15,34: #b #Hb / by le_n/ 763 |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 764 |10,13,14,15,16,17,18: / by le_n/ 765 |20,21: cases x #ad cases ad 766 [15,34: #b #Hb / by le_n/ 767 |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 768 |19,22,23,24,25,26,27: / by le_n/ 769 |29,30: cases x #ad cases ad #a1 #a2 770 [ cases a2 #ad2 cases ad2 771 ] 772 ] 773 ] 774 ] 775 cases daemon (* XXX see if it works first *) 776 qed. 777 778 lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m. 779 #n 780 elim n 781 [ #m #_ @le_O_n 782 | #n' #Hind #m cases m 783 [ #H -n whd in match (minus ??) in H; >H @le_n 784 | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H 785 ] 786 ] 787 qed. 788 789 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0. 790 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r 791 qed. 792 590 793 (* One step in the search for a jump expansion fixpoint. *) 591 794 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). … … 596 799 ∀old_policy:(Σpolicy:ppc_pc_map. 597 800 And (And (out_of_program_none program policy) 598 ( policy_isize_sum program labelspolicy))801 (jump_not_in_policy program policy)) 599 802 (\fst policy < 2^16)). 600 803 (Σx:bool × (option ppc_pc_map). … … 602 805 match y with 603 806 [ None ⇒ (* nec_plus_ultra program old_policy *) True 604 | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program)p)605 ( policy_isize_sum program labelsp))807 | Some p ⇒ And (And (And (And (And (out_of_program_none program p) 808 (jump_not_in_policy program p)) 606 809 (policy_increase program old_policy p)) 607 810 (policy_compact program labels p)) … … 616 819 let 〈added,policy〉 ≝ x in 617 820 And (And (And (And (out_of_program_none prefix policy) 618 ( policy_isize_sum prefix labelspolicy))821 (jump_not_in_policy prefix policy)) 619 822 (policy_increase prefix old_sigma policy)) 620 823 (policy_compact prefix labels policy)) … … 666 869 ] 667 870 | lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 668 cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) 669 #old_pc #old_length #Hpolicy @pair_elim #added #policy normalize nodelta 871 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)) 872 cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %); 873 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta 670 874 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 671 875 @conj [ @conj [ @conj [ @conj … … 681 885 ] 682 886 ] 683 | cases daemon (* XXX *) 887 | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi; 888 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 889 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 890 [ >(nth_append_first ? i prefix ?? Hi) 891 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) 892 | @bitvector_of_nat_abs 893 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 894 @le_plus_a @Hi 895 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 896 @le_plus_n_r 897 | @lt_to_not_eq @Hi 898 ] 899 ] 900 | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit 901 >nth_append_second 902 [ <minus_n_n whd in match (nth ????); cases instr in Heq1; 903 [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/ 904 |2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by / 905 |1: #pi cases pi 906 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 907 [1,2,3,6,7,24,25: #x #y 908 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1 909 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by / 910 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 911 #_ #H @⊥ cases H #H2 @H2 / by I/ 912 ] 913 ] 914 | @le_n 915 ] 916 ] 684 917 ] 685 918 | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 686 cases (le_to_or_lt_eq … Hi) -Hi; #Hi687 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))919 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi 920 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi) 688 921 <(proj2 ?? (pair_destruct ?????? Heq2)) 689 922 @pair_elim #opc #oj #EQ1 >lookup_insert_miss … … 691 924 | @bitvector_of_nat_abs 692 925 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a 693 @ (le_S_S_to_le … Hi)926 @Hi 694 927 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 695 | @lt_to_not_eq @ (le_S_S_to_le … Hi)928 | @lt_to_not_eq @Hi 696 929 ] 697 930 ] 698 | <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) >lookup_insert_hit 699 cases instr in Heq1 Heq2; 700 [2,3,6: #x [3: #y] normalize nodelta #Heq1 #Heq2 <(proj1 ?? (pair_destruct ?????? Heq1)) 701 cases daemon 702 |1,4,5: cases daemon 703 ] 704 ] 705 ] 706 | (* policy_compact *) cases daemon 707 ] 708 | (* added = 0 → policy_equal *) cases daemon 709 ] 931 | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit 932 cases (dec_is_jump instr) 933 [ cases instr in Heq1; normalize nodelta 934 [ #pi cases pi 935 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 936 [1,2,3,6,7,24,25: #x #y 937 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 938 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 939 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 940 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta 941 @jmpleq_max_length 942 ] 943 |2,3,6: #x [3: #y] #_ #Hj cases Hj 944 |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta 945 @jmpleq_max_length 946 ] 947 | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 948 [ #pi cases pi 949 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 950 [1,2,3,6,7,24,25: #x #y 951 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 952 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 953 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 954 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) 955 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 956 >prf >nth_append_second 957 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 958 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 959 |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,54,56: 960 @le_n 961 ] 962 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 963 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 964 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 965 cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) 966 #a #b #H >H normalize nodelta %2 @refl 967 ] 968 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 969 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 970 ] 971 |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 972 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) 973 [1,4,7: >prf >nth_append_second 974 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 975 |2,4,6: @le_n 976 ] 977 |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 978 |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) 979 #a #b #H >H normalize nodelta %2 @refl 980 ] 981 |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 982 ] 983 ] 984 ] 985 ] 986 | (* policy_compact *) (*XXX*) cases daemon 987 ] 988 | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy) 989 lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr) 990 cases instr in ⊢ (???% → % → % → %); normalize nodelta 991 [ #pi cases pi normalize nodelta 992 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 993 [1,2,3,6,7,24,25: #x #y 994 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 995 #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded 996 #i >append_length >commutative_plus #Hi normalize in Hi; 997 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 998 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 999 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 1000 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1001 @(Hold Hadded i Hi) 1002 |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,54,56: 1003 @bitvector_of_nat_abs 1004 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 1005 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 1006 @le_plus_a @Hi 1007 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 1008 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 1009 @le_plus_n_r 1010 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 1011 @lt_to_not_eq @Hi 1012 ] 1013 ] 1014 |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,54,56: 1015 <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 1016 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) 1017 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 1018 >prf >nth_append_second 1019 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1020 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 1021 |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,54,56: 1022 @le_n 1023 ] 1024 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 1025 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1026 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 1027 cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) 1028 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 1029 ] 1030 ] 1031 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold 1032 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 1033 #H #i >append_length >commutative_plus #Hi normalize in Hi; 1034 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 1035 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2)) 1036 >lookup_insert_miss 1037 [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi) 1038 [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 1039 ] 1040 @bitvector_of_nat_abs 1041 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 1042 >append_length >commutative_plus @le_plus_a @Hi 1043 |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 1044 >append_length <plus_n_Sm @le_S_S 1045 |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 1046 ] @le_plus_n_r 1047 |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi 1048 >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 1049 >Holdeq normalize nodelta @sym_eq @blerpque 1050 [3,6,9,12,15,18,21,24,27: 1051 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 1052 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 1053 |2,4,6,8,10,12,14,16,18: #H @H 1054 ] 1055 / by I/ 1056 |2,5,8,11,14,17,20,23,26: / by I/ 1057 ] 1058 ] 1059 ] 1060 |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) 1061 #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 1062 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 1063 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 1064 [1,3,5: @(Hold Hadded i Hi) 1065 |2,4,6: @bitvector_of_nat_abs 1066 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 1067 @le_plus_a @Hi 1068 |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 1069 @le_plus_n_r 1070 |3,6,9: @lt_to_not_eq @Hi 1071 ] 1072 ] 1073 |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 1074 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) 1075 [1,4,7: >prf >nth_append_second 1076 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 1077 |2,4,6: @le_n 1078 ] 1079 |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1080 |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) 1081 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 1082 ] 1083 ] 1084 |4,5: #x #Hins #Heq1 #Heq2 #Hold 1085 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 1086 #H #i >append_length >commutative_plus #Hi normalize in Hi; 1087 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 1088 [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 1089 [1,3: @(Hold ? i Hi) 1090 [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 1091 ] 1092 @bitvector_of_nat_abs 1093 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 1094 >append_length >commutative_plus @le_plus_a @Hi 1095 |2,5: @(transitive_lt … (pi2 ?? program)) >prf 1096 >append_length <plus_n_Sm @le_S_S 1097 |3,6: @lt_to_not_eq @Hi 1098 ] @le_plus_n_r 1099 |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 1100 <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta 1101 @sym_eq @blerpque 1102 [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 1103 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 1104 |2,4: #H @H 1105 ] 1106 / by I/ 1107 |2,5: / by I/ 1108 ] 1109 ] 1110 ] 1111 ] 710 1112 | normalize nodelta @conj [ @conj [ @conj [ @conj 711 1113 [ #i #Hi / by refl/ … … 716 1118 ] 717 1119 qed. 1120 718 1121 719 1122 (* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; … … 1665 2068 qed. 1666 2069 1667 include alias "arithmetics/nat.ma".2070 nclude alias "arithmetics/nat.ma". 1668 2071 include alias "basics/logic.ma". 1669 2072 … … 1672 2075 (* The glue between Policy and Assembly. *) 1673 2076 definition jump_expansion': 1674 1675 2077 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16). 2078 option (Σsigma:Word → Word × bool. 1676 2079 ∀ppc: Word. 1677 2080 let pc ≝ \fst (sigma ppc) in … … 1687 2090 ∨ 1688 2091 (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))). 2092 ≝ λprogram. 2093 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 2094 match policy with 2095 [ None ⇒ None ? 2096 | Some x ⇒ Some ? 2097 «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 2098 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 2099 ]. 1689 2100 cases daemon 1690 2101 qed.
Note: See TracChangeset
for help on using the changeset viewer.