Changeset 2221 for src/ASM/PolicyFront.ma
 Timestamp:
 Jul 20, 2012, 10:46:29 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2213 r2221 302 302 (Σlabels:label_map. 303 303 ∀l.occurs_exactly_once ?? l program → 304 bitvector_of_nat ? (lookup_def ?? labels l 0) = 305 address_of_word_labels_code_mem program l 304 And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 305 address_of_word_labels_code_mem program l) 306 (lookup_def ?? labels l 0 < program) 306 307 ) ≝ 307 308 λprogram. … … 650 651 sigma_compact_unsafe program (create_label_map program) sigma → 651 652 sigma_compact program (create_label_map program) sigma. 652 #program #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi 653 #program cases program program #program #Hprogram #old_sigma #sigma #Hequal 654 #Hsafe #Hcp_unsafe #i #Hi 653 655 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) 654 656 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) … … 669 671 whd in match (expand_pseudo_instruction …); 670 672 normalize nodelta whd in match (append …) in H; 671 cases (nth i ? program 〈None ?,Comment []〉) in H; 673 lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H 674 cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %); 672 675 #lbl #instr cases instr 673 [2,3,6: #x [3: #y] normalize nodelta #H @refl674 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 676 [2,3,6: #x [3: #y] normalize nodelta #H #_ % 677 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq 675 678 lapply (Hj x (refl ? x)) Hj normalize nodelta 676 679 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O … … 678 681 [1,4: whd in match short_jump_cond; normalize nodelta 679 682 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? *) 683 [1,3: cases (create_label_map program) #clm #Hclm 684 @le_S_to_le @(proj2 ?? (Hclm x ?)) 685 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 686 2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 687 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse 688 [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 689 2,5: whd in match fetch_pseudo_instruction; normalize nodelta 690 >nth_safe_nth 691 [1,3: >nat_of_bitvector_bitvector_of_nat_inverse 692 [1,3: >Heq / by refl/ 693 2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 694 ] 695 ] 696 3,6: / by / 697 ] 681 698 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 682 699 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) … … 693 710 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 694 711 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? *) 712 [1,3: cases (create_label_map program) #clm #Hclm 713 @le_S_to_le @(proj2 ?? (Hclm x ?)) 714 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 715 2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 716 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse 717 [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 718 2,5: whd in match fetch_pseudo_instruction; normalize nodelta 719 >nth_safe_nth 720 [1,3: >nat_of_bitvector_bitvector_of_nat_inverse 721 [1,3: >Heq / by refl/ 722 2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 723 ] 724 ] 725 3,6: / by / 726 ] 696 727 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 697 728 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 … … 705 736 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 706 737 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? *) 738 [1,3: cases (create_label_map program) #clm #Hclm 739 @le_S_to_le @(proj2 ?? (Hclm x ?)) 740 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 741 2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 742 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse 743 [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 744 2,5: whd in match fetch_pseudo_instruction; normalize nodelta 745 >nth_safe_nth 746 [1,3: >nat_of_bitvector_bitvector_of_nat_inverse 747 [1,3: >Heq / by refl/ 748 2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 749 ] 750 ] 751 3,6: / by / 752 ] 708 753 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 709 754 cases (vsplit bool 5 11 ?) #addr1 #addr2 … … 720 765 [1,2,3,6,7,24,25: #x #y 721 766 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 722 normalize nodelta #H @refl767 normalize nodelta #H #Heq @refl 723 768 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 724 769 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 725 #Hj lapply (Hj x (refl ? x)) Hj770 #Hj #Heq lapply (Hj x (refl ? x)) Hj 726 771 whd in match expand_relative_jump; normalize nodelta 727 772 whd in match expand_relative_jump_internal; normalize nodelta … … 737 782 [1,3,5,7,9,11,13,15,17: 738 783 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? *) 784 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 785 @le_S_to_le @(proj2 ?? (Hclm x ?)) 786 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 787 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 788 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 789 2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 790 >nth_safe_nth 791 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 792 [1,3,5,7,9,11,13,15,17: >Heq %] 793 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 794 ] 795 ] 796 >Heq / by / 797 ] 740 798 #X >(le_to_leb_true … X) @refl 741 799 ] … … 753 811 [1,3,5,7,9,11,13,15,17: 754 812 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? *) 813 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 814 @le_S_to_le @(proj2 ?? (Hclm x ?)) 815 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 816 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 817 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 818 2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 819 >nth_safe_nth 820 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 821 [1,3,5,7,9,11,13,15,17: >Heq %] 822 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 823 ] 824 ] 825 >Heq / by / 826 ] 756 827 #X >(le_to_leb_true … X) @refl 757 828 ]
Note: See TracChangeset
for help on using the changeset viewer.