 Timestamp:
 Jul 20, 2012, 10:46:29 AM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2199 r2221 624 624 let 〈labels,costs〉 ≝ labels_costs in 625 625 ∀l.occurs_exactly_once ?? l program → 626 bitvector_of_nat ? (lookup_def ?? labels l 0) = 627 address_of_word_labels_code_mem program l 626 And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 627 address_of_word_labels_code_mem program l) 628 (lookup_def ?? labels l 0 < program) 628 629 ) ≝ 629 630 λprogram. … … 633 634 ppc = prefix ∧ 634 635 ∀l.occurs_exactly_once ?? l prefix → 635 bitvector_of_nat ? (lookup_def ?? labels l 0) =636 And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 636 637 address_of_word_labels_code_mem prefix l) 638 (lookup_def ?? labels l 0 < program)) 637 639 program 638 640 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. … … 656 658 >occurs_exactly_once_None in Hocc; @(IH2 lbl) 657 659  #lbl normalize nodelta inversion (eq_identifier ? lbl l) 658 [ #Heq #Hocc >(eq_identifier_eq … Heq) 659 >address_of_word_labels_code_mem_Some_hit 660 [ >IH1 >lookup_def_add_hit % 661  <(eq_identifier_eq … Heq) in Hocc; // 660 [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj 661 [ >address_of_word_labels_code_mem_Some_hit 662 [ >IH1 >lookup_def_add_hit % 663  <(eq_identifier_eq … Heq) in Hocc; // 664 ] 665  >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 662 666 ] 663  #Hneq #Hocc 664 <address_of_word_labels_code_mem_Some_miss 665 [ >lookup_def_add_miss 666 [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq // 667  % @neq_identifier_neq @Hneq 667  #Hneq #Hocc lapply (IH2 lbl ?) 668 [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // 669  #IH3 @conj 670 [ <address_of_word_labels_code_mem_Some_miss 671 [ >lookup_def_add_miss 672 [ @(proj1 ?? IH3) 673  % @neq_identifier_neq @Hneq 674 ] 675  @Hocc 676  >eq_identifier_sym @Hneq 677 ] 678  >lookup_def_add_miss 679 [ @(proj2 ?? IH3) 680  % @neq_identifier_neq @Hneq 681 ] 668 682 ] 669  @Hocc670  >eq_identifier_sym @Hneq671 683 ] 672 684 ] … … 688 700 ∀pseudo_program: pseudo_assembly_program. 689 701 let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in 690 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 691 bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id. 702 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → And 703 (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id) 704 (lookup_def ?? labels id 0 < \snd pseudo_program). 692 705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 693 706 qed. 
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.