 Timestamp:
 Jul 18, 2012, 5:57:26 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2211 r2213 644 644 qed. 645 645 646 lemma label_in_program: ∀program:(Σl.S (l) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm.647 ∀l.occurs_exactly_once ?? l program →648 bitvector_of_nat ? (lookup_def ?? lm l 0) =649 address_of_word_labels_code_mem program l).∀x.650 occurs_exactly_once ?? x program →651 lookup_def ASMTag ℕ labels x O≤program.652 #program cases program program #program #Hprogram #labels #x cases labels653 labels #labels #H lapply (H x) H654 generalize in match (lookup_def … labels x 0);655 whd in match address_of_word_labels_code_mem;656 whd in match index_of; normalize nodelta elim program in Hprogram;657 [ #Hprogram #n cases not_implemented658  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv659 whd in match (occurs_exactly_once ????) in Hocc;660 whd in match (index_of_internal ????) in Hbv;661 lapply (refl ? (instruction_matches_identifier … x h))662 lapply Hocc; lapply Hbv; Hocc Hbv663 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);664 normalize nodelta #Hbv #Hocc #EQ665 [ >(bitvector_of_nat_ok 16 n 0)666 [ @le_O_n667  >(eq_eq_bv … Hbv) @I668  / by /669  cases daemon670 ]671  cases n in Hbv;672 [ #_ @le_O_n673  n #n #Hbv @le_S_S @(Hind … Hocc)674 [ @conj675 [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n676  cases daemon (* axiomatize this *)677 ]678  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)679 [ >Hbv >eq_bv_refl @I680  @(transitive_lt … (proj1 ?? Hprogram)) cases daemon681  cases daemon682  #H >(index_of_label_from_internal … Hocc)683 <plus_O_n >(index_of_label_from_internal … Hocc) in H;684 #H >(injective_S … H) <plus_O_n @refl685 ]686 ]687 ]688 ]689 ]690 qed.691 692 646 lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (l)) < 2^16 ∧ is_well_labelled_p l). 693 ∀ labels.∀old_sigma.∀sigma.647 ∀old_sigma.∀sigma. 694 648 sigma_pc_equal program old_sigma sigma → 695 sigma_safe program labels0 old_sigma sigma →696 sigma_compact_unsafe program labelssigma →697 sigma_compact program labelssigma.698 #program # labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi649 sigma_safe program (create_label_map program) 0 old_sigma sigma → 650 sigma_compact_unsafe program (create_label_map program) sigma → 651 sigma_compact program (create_label_map program) sigma. 652 #program #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi 699 653 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) 700 654 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) … … 723 677 cases x2 normalize nodelta 724 678 [1,4: whd in match short_jump_cond; normalize nodelta 725 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 726 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 727 normalize nodelta 728 >(Hequal (lookup_def ?? labels x 0) ?) 729 [2,4,6,8: @(label_in_program program labels x) 730 cases daemon (* XXX this has to come from somewhere else *) 731 ] 732 <plus_n_O 679 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 680 [1,3: cases daemon (* XXX should this be a property of create_label_map? *) 681 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 733 682 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 734 683 #result #flags normalize nodelta 735 684 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 736 685 cases (get_index' bool 2 0 flags) normalize nodelta 737 [ 5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/738 1,2 ,3,4: cases (eq_bv 9 upper ?)739 [2,4 ,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3)740 1,3 ,5,7: #_ normalize nodelta @refl686 [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 687 1,2: cases (eq_bv 9 upper ?) 688 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) 689 1,3: #_ normalize nodelta @refl 741 690 ] 742 691 ] 692 ] 743 693 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 744 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 745 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 746 normalize nodelta 747 (* USE: added = 0 → policy_pc_equal (from fold) *) 748 >(Hequal (lookup_def ?? labels x 0) ?) 749 [2,4,6,8: @(label_in_program program labels x) 750 cases daemon (* XXX this has to come from somewhere else *)] 751 <plus_n_O 694 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 695 [1,3: cases daemon (* XXX should this be a property of create_label_map? *) 696 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 752 697 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 753 698 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta … … 757 702 cases (get_index' bool 2 0 flags) normalize nodelta 758 703 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 704 ] 759 705 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 760 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 761 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 762 normalize nodelta 763 (* USE: added = 0 → policy_pc_equal (from fold) *) 764 >(Hequal (lookup_def ?? labels x 0) ?) 765 [2,4,6,8: @(label_in_program program labels x) 766 cases daemon (* XXX this has to come from somewhere else *)] 767 <plus_n_O normalize nodelta 706 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 707 [1,3: cases daemon (* XXX should this be a property of create_label_map? *) 708 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 768 709 cases (vsplit bool 5 11 ?) #addr1 #addr2 769 710 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta … … 773 714 cases (get_index' bool 2 0 flags) normalize nodelta 774 715 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 716 ] 775 717 ] 776 718 1: #pi cases pi … … 787 729 whd in match expand_relative_jump_internal_unsafe; 788 730 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 789 <(plus_n_Sm i 0) <plus_n_O 790 cases daemon (* XXX this needs subadressing mode magic, see above *) 731 <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta 732 [1,4,7,10,13,16,19,22,25: 733 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 734 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 735 #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2 736 @(pair_replace ?????????? (eq_to_jmeq … H)) 737 [1,3,5,7,9,11,13,15,17: 738 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 739 [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *) 740 #X >(le_to_leb_true … X) @refl 741 ] 742 >(proj1 ?? H2) try (@refl) normalize nodelta 743 [1,2,3,5: @(subaddressing_mode_elim … y) #w % 744  cases y * #sth #sth2 @(subaddressing_mode_elim … sth) 745 @(subaddressing_mode_elim … sth2) #x [3,4: #x2] % 746 ] 747 2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/ 748 ] 749 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 750 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 751 #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 752 @(pair_replace ?????????? (eq_to_jmeq … H)) 753 [1,3,5,7,9,11,13,15,17: 754 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 755 [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *) 756 #X >(le_to_leb_true … X) @refl 757 ] 758 #H2 >H2 try (@refl) normalize nodelta 759 [1,2,3,5: @(subaddressing_mode_elim … y) #w % 760  cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w 761 [1,2: %] whd in match (map ????); whd in match (flatten ??); 762 whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%); 763 >length_append >length_append @eq_f2 % 764 ] 765 ] 791 766 ] 792 767 ] 793 768 ] 794 769 ] 795 ]796 770 qed. 797 771
Note: See TracChangeset
for help on using the changeset viewer.