Changeset 2245
 Timestamp:
 Jul 24, 2012, 4:50:20 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2244 r2245 453 453 454 454 lemma jump_expansion_step6: 455 (* 456 program : 457 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 458 labels : 455 ∀program : list labelled_instruction.(* 456 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l)*) 457 ∀labels : label_map.(* 459 458 (Σlm:label_map 460 459 .(∀l:identifier ASMTag … … 462 461 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 463 462 =address_of_word_labels_code_mem program l))*) 464 ∀old_sigma : ppc_pc_map.(*465 (Σpolicy:ppc_pc_map466 . not_jump_default program policy463 ∀old_sigma : 464 Σpolicy:ppc_pc_map 465 .(*not_jump_default program policy 467 466 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 468 467 〈O,short_jump〉) … … 471 470 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 472 471 (\snd policy) 〈O,short_jump〉) 473 ∧ sigma_compact_unsafe program labels policy474 ∧\fst policy≤ 2 \sup 16 )*)475 ∀prefix : list (option Identifier×pseudo_instruction). (*476 x : (option Identifier×pseudo_instruction)477 tl : (list (option Identifier×pseudo_instruction))478 prf : (program=prefix@[x]@tl)472 ∧*)sigma_compact_unsafe program labels policy 473 (*∧\fst policy≤ 2 \sup 16*). 474 ∀prefix : list (option Identifier×pseudo_instruction). 475 ∀x : option Identifier×pseudo_instruction. 476 ∀tl : list (option Identifier×pseudo_instruction). 477 ∀prf : program=prefix@[x]@tl.(* 479 478 acc : 480 479 (Σx0:ℕ×ppc_pc_map … … 497 496 (\snd old_sigma) 〈O,short_jump〉) 498 497 +added 499 ∧sigma_safe prefix labels added old_sigma policy)) 500 inc_added : ℕ501 inc_pc_sigma : ppc_pc_map498 ∧sigma_safe prefix labels added old_sigma policy))*) 499 ∀inc_added : ℕ. 500 ∀inc_pc_sigma : ppc_pc_map.(* 502 501 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 503 502 ∀label : option Identifier. 504 ∀instr : pseudo_instruction. (*505 p1 : (x≃〈label,instr〉)503 ∀instr : pseudo_instruction. 504 ∀p1 : x≃〈label,instr〉.(* 506 505 add_instr ≝ 507 506 match instr … … 520 519 Some jump_length 521 520 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 522 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 523 inc_pc : ℕ524 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)525 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 526 old_pc : ℕ527 old_length : jump_length528 Holdeq :529 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma)521 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]*) 522 ∀inc_pc : ℕ. 523 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.(* 524 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*) 525 ∀old_pc : ℕ. 526 ∀old_length : jump_length. 527 ∀Holdeq : 528 lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 530 529 〈O,short_jump〉 531 =〈old_pc,old_length〉 )532 Hpolicy :530 =〈old_pc,old_length〉. 531 ∀Hpolicy1 :(* 533 532 (not_jump_default prefix 〈inc_pc,inc_sigma〉 534 533 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma … … 541 540 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 542 541 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 543 ∧( inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)542 ∧( *)inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.(*) 544 543 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 545 544 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma … … 547 546 =old_pc+inc_added 548 547 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 548 ∀Hpolic2: inc_pc 549 =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 〈O,short_jump〉). 549 550 ∀added : ℕ. 550 ∀policy : ppc_pc_map.(* 551 new_length : jump_length 552 isize : ℕ 553 Heq1 : 554 (match 555 match instr 556 in pseudo_instruction 557 return λ_:pseudo_instruction.(option jump_length) 558 with 559 [Instruction (i:(preinstruction Identifier))⇒ 560 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 561 (prefix) i 562 Comment (_:String)⇒None jump_length 563 Cost (_:costlabel)⇒None jump_length 564 Jmp (j:Identifier)⇒ 565 Some jump_length 566 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 567 Call (c:Identifier)⇒ 568 Some jump_length 569 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 570 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 571 in option 572 return λ_0:(option jump_length).(jump_length×ℕ) 573 with 551 ∀policy : ppc_pc_map. 552 ∀new_length : jump_length. 553 ∀isize : ℕ. 554 let add_instr ≝ match instr with 555 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 556  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 557  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i 558  _ ⇒ None ? 559 ] in 560 ∀Heq1 : 561 match add_instr with 574 562 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 575 563 Some (pl:jump_length)⇒ 576 564 〈max_length old_length pl, 577 565 instruction_size_jmplen (max_length old_length pl) instr〉] 578 =〈new_length,isize〉) 579 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 580 prefix_ok : (prefix< 2 \sup 16 ) 581 Heq2a : 582 (match 583 match instr 584 in pseudo_instruction 585 return λ_0:pseudo_instruction.(option jump_length) 586 with 587 [Instruction (i:(preinstruction Identifier))⇒ 588 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 589 (prefix) i 590 Comment (_0:String)⇒None jump_length 591 Cost (_0:costlabel)⇒None jump_length 592 Jmp (j:Identifier)⇒ 593 Some jump_length 594 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 595 Call (c:Identifier)⇒ 596 Some jump_length 597 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 598 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 599 in option 600 return λ_0:(option jump_length).ℕ 601 with 566 =〈new_length,isize〉. 567 ∀prefix_ok1 : S (prefix)< 2 \sup 16. 568 ∀prefix_ok : prefix< 2 \sup 16. 569 ∀Heq2a : 570 match add_instr with 602 571 [None⇒inc_added 603 572 Some (x0:jump_length)⇒ 604 573 inc_added+(isizeinstruction_size_jmplen old_length instr)] 605 =added )606 Heq2b :607 (〈inc_pc+isize,574 =added. 575 ∀Heq2b : 576 〈inc_pc+isize, 608 577 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 609 578 〈inc_pc+isize, … … 612 581 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 613 582 〈inc_pc,new_length〉 inc_sigma)〉 614 =policy) 615 *) 583 =policy. 616 584 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy. 617 cases daemon(* 585 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label 586 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 587 #added #policy #new_length #isize #Heq1 #prefix_ok #prefix_ok1 #Heq2a #Heq2b 618 588 (* USE[pass]: added = 0 → policy_pc_equal *) 619 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 620 <(proj2 ?? (pair_destruct ?????? Heq2)) 621 <(proj1 ?? (pair_destruct ?????? Heq2)) 622 lapply Heq1 Heq1 lapply (refl ? instr) 623 cases instr in ⊢ (???% → % → %); normalize nodelta 589 lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 Heq1 590 inversion instr normalize nodelta 624 591 [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 625 592 #Hi normalize in Hi; 626 593 cases (le_to_or_lt_eq … Hi) Hi #Hi 627 594 [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 628 [1,3,5: < (proj2 ?? (pair_destruct ?????? Heq2))>lookup_insert_miss595 [1,3,5: <Heq2b >lookup_insert_miss 629 596 [1,3,5: >lookup_insert_miss 630 597 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 631 2,4,6: @bitvector_of_nat_abs 632 [3,6,9: @lt_to_not_eq @Hi 633 1,4,7: @(transitive_lt ??? Hi) 634 ] 635 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 636 @le_S_S <plus_n_Sm @le_S @le_plus_n_r 637 ] 638 2,4,6: @bitvector_of_nat_abs 639 [3,6,9: @lt_to_not_eq @le_S @Hi 640 1,4,7: @(transitive_lt … Hi) @le_S_to_le 641 ] 642 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 643 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 644 ] 645 2,4,6: >Hi >lookup_insert_miss 598 *: @bitvector_of_nat_abs try assumption 599 [2,4,6: @lt_to_not_eq @Hi 600 *: @(transitive_lt ??? Hi) assumption ]] 601 *: @bitvector_of_nat_abs try assumption 602 [2,4,6: @lt_to_not_eq @le_S @Hi 603 *: @(transitive_lt … Hi) assumption ]] 604 *: >Hi >lookup_insert_miss 646 605 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 647 606 @sym_eq (* USE: fst p = lookup prefix *) 648 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 649 2,4,6: @bitvector_of_nat_abs 650 [3,6,9: @lt_to_not_eq @le_n 651 1,4,7: @le_S_to_le 652 ] 653 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 654 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 655 ] 656 ] 607 @Hpolicy2 608 *: @bitvector_of_nat_abs try assumption 609 @lt_to_not_eq %]] 657 610 2,4,6: >Hi >lookup_insert_hit 658 611 (* USE fst p = lookup prefix *) 659 > (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))612 >Hpolicy2 660 613 <(Hold Hadded (prefix) (le_n (prefix))) 661 614 (* USE: sigma_compact (from old_sigma) *) 662 lapply (p roj2 ?? (proj1 ?? (pi2 ?? old_sigma))(prefix) ?)615 lapply (pi2 ?? old_sigma (prefix) ?) 663 616 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 664 2,4,6: 665 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 666 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% > %); 617 *: 618 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 667 619 [1,3,5: normalize nodelta #_ #ABS cases ABS 668 2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 669 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 670 [1,3,5: normalize nodelta #Hl #x cases x x #pc #j normalize nodelta #Hl2 #ABS cases ABS 671 2,4,6: normalize nodelta #x cases x x #Spc #Sj #EQS #x cases x x #pc #j #EQ 620 *: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 621 [1,3,5: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS 622 *: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ 672 623 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 673 624 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 674 >prf >p1 >Hins >nth_append_second 675 [2,4,6: @(le_n (prefix)) 676 1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 677 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by / 678 ] 679 ] 680 ] 681 ] 682 ] 625 >prf >p1 >Hins >nth_append_second try % 626 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 627 #H >H @plus_left_monotone @instruction_size_irrelevant % ]]]] 683 628 4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 684 629 #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi #Hi … … 692 637 1,4: @(transitive_lt ??? Hi) 693 638 ] 694 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 695 >append_length @le_plus_n_r 639 assumption 696 640 ] 697 641 2,4: @bitvector_of_nat_abs 698 642 [3,6: @lt_to_not_eq @le_S @Hi 699 1,4: @(transitive_lt ??? Hi) @le_S_to_le 700 ] 701 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 702 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 703 ] 643 1,4: @(transitive_lt ??? Hi) assumption] 644 assumption ] 704 645 2,4: >Hi >lookup_insert_miss 705 646 [1,3: >lookup_insert_hit >(Hold ? (prefix) (le_n (prefix))) 706 647 [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 707 648 (* USE: fst p = lookup prefix *) 708 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 709 2,4: @bitvector_of_nat_abs 710 [3,6: @lt_to_not_eq @le_n 711 1,4: @(transitive_lt ??? (le_S_S … (le_n (prefix)))) 712 ] 713 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 714 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 715 ] 716 ] 649 @Hpolicy2 650 2,4: @bitvector_of_nat_abs try assumption 651 @lt_to_not_eq @le_n]] 717 652 2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1)) 718 653 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 719 654 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1)) 720 @jump_length_le_max / by I/721  2,4: #H (* USE: fst p = lookup prefix *)722 > (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))655 @jump_length_le_max % 656 *: #H (* USE: fst p = lookup prefix *) 657 >Hpolicy2 723 658 <(Hold ? (prefix) (le_n (prefix))) 724 659 [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H 725 >(jump_length_equal_max … H) 726 [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *) 727 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (prefix) ?) 728 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 729 2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 730 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% → %); 731 [1,3: normalize nodelta #_ #_ #ABS cases ABS 732 2,4: normalize nodelta 733 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 734 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 735 [1,3: #_ #x cases x x #pc #j normalize nodelta #_ #_ #ABS cases ABS 736 2,4: #x cases x x #Spc #Sj #EQS #x cases x x #pc #j #EQ 737 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 738 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 739 >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second 740 [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H 741 2,4: @le_n 742 ] 743 ] 744 ] 745 ] 746 2,4: / by I/ 747 ] 748 2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded] 749 ] 750 ] 751 ] 660 >(jump_length_equal_max … H) try % 661 (* USE: sigma_compact_unsafe (from old_sigma) *) 662 lapply (pi2 ?? old_sigma (prefix) ?) 663 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 664 2,4: inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 665 [1,3: normalize nodelta #_ #ABS cases ABS 666 2,4: normalize nodelta 667 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 668 [1,3: #_ * #pc #j normalize nodelta #_ #ABS cases ABS 669 2,4: * #Spc #Sj #EQS #x cases x x #pc #j #EQ 670 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 671 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 672 >EQpair @eq_f >prf >nth_append_second try % 673 <minus_n_n >p1 whd in match (nth ????); >Hins 674 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ' 675 >(proj2 … (pair_destruct … EQ')) % ]]] 676 2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded *: skip]]]] 752 677 1: #pi cases pi normalize nodelta 753 678 [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: … … 914 839 ] 915 840 ] 916 ] *)841 ] 917 842 qed. 918 843 … … 1528 1453  @not_lt_to_le @ltb_false_to_not_lt @p1 1529 1454 ] 1530 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);1531 #inc_pc #inc_sigma #Hips 1455 4: lapply (pi2 ?? acc) >p acc inversion inc_pc_sigma 1456 #inc_pc #inc_sigma #Hips normalize nodelta 1532 1457 inversion (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 1533 1458 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
Note: See TracChangeset
for help on using the changeset viewer.