 Timestamp:
 Oct 19, 2011, 5:10:27 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1404 r1417 773 773 ]. 774 774 775 lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x). 776 #x #y 777 cases y 778 [ // 779  cases x // 780  // 781 ] 782 qed. 783 775 784 definition is_jump' ≝ 776 785 λx:preinstruction Identifier. … … 807 816 (Σpolicy. 808 817 jump_in_policy program policy ∧ 809 (jump_in_policy program policy → True)) ≝ 818 (jump_in_policy program policy → 819 (∀i.i < program → is_jump (nth i ? program 〈None ?, Comment []〉) → 820 jmpleq 821 (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉)) 822 (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉))) 823 ) 824 ) ≝ 810 825 let labels ≝ create_label_trie program old_policy in 811 826 let 〈final_pc, final_policy〉 ≝ … … 813 828 (λprefix.ℕ × Σpolicy. 814 829 jump_in_policy prefix policy ∧ 815 (jump_in_policy prefix policy → True) 830 (jump_in_policy prefix policy → 831 (∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 832 jmpleq 833 (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉)) 834 (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉))) 835 ) 816 836 ) 817 837 program … … 819 839 let 〈pc, policy〉 ≝ acc in 820 840 let 〈label,instr〉 ≝ x in 821 let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (prefix)) policy in841 let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (prefix)) old_policy in 822 842 let add_instr ≝ 823 843 match instr with … … 828 848 ] in 829 849 let 〈new_pc, new_policy〉 ≝ 830 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (prefix)) policy 〈pc, short_jump〉 in850 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (prefix)) old_policy 〈0, short_jump〉 in 831 851 match add_instr with 832 852 [ None ⇒ (* i.e. it's not a jump *) … … 845 865 n #n #Hn 846 866 % [ @h  % [ @n  normalize nodelta cases instr normalize nodelta 847 [2,3: #x cases (lookup ??? policy ?) #y #z @Hn848 6: #x #y cases (lookup ??? policy ?) #w #z @Hn849 1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???)867 [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn 868 6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn 869 1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???) 850 870 [ @Hn 851 871  #z normalize nodelta <Hn @lookup_opt_insert_miss … … 855 875 ] ] 856 876 ] 857 4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn877 4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn 858 878 @lookup_opt_insert_miss @notb_elim >eq_bv_false 859 879 [1,3: // … … 873 893 9,10,14,15: #j normalize nodelta #_ 874 894 % [1,3,5,7: @pc 875 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉))876 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %)895 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 896 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %) 877 897 #x #y #Hl normalize nodelta 878 898 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) … … 881 901 11,12,13,16,17: #x #j normalize nodelta #_ 882 902 % [1,3,5,7,9: @pc 883 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉))884 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %)903 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 904 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %) 885 905 #x #y #Hl normalize nodelta 886 906 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) … … 890 910 4,5: #j normalize nodelta #_ 891 911 % [1,3: @pc 892 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉)912 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 893 913 #x #y normalize nodelta 894 914 % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j)) … … 901 921 ] 902 922 ] 903  // 923  #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 924 [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 925 lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta 926 [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #y #z 927 normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 928 6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #w #z 929 normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 930 1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #x #y 931 cases (jump_expansion_step_instruction ???) 932 [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 933  #z normalize nodelta 934 whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss 935 [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 936  @notb_elim >eq_bv_false [ //  @nmk #H @(absurd (i = (prefix))) 937 [ @(bitvector_of_nat_ok … H) 938  @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 939 ] ] 940 ] 941 ] 942 4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #x #y 943 normalize nodelta >lookup_insert_miss 944 [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 945 2,4: @notb_elim >eq_bv_false [1,3: //  2,4: @nmk #H @(absurd (i = (prefix))) 946 [1,3: @(bitvector_of_nat_ok … H) 947 2,4: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 948 ] ] 949 ] 950 ] 951  #Hi >nth_append_second >(injective_S … Hi) 952 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 953 [2,3: #x #Hj @⊥ @Hj 954 6: #x #y #Hj @⊥ @Hj 955 1: #pi cases pi 956 [35,36,37: #Hj @⊥ @Hj 957 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj 958 1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj 959 9,10,14,15: #j normalize nodelta #_ 960 cases (lookup ???? 〈0,short_jump〉) #x #y 961 whd in match (snd ℕ jump_expansion_policy ?) 962 >lookup_insert_hit normalize @jmpleq_max_length 963 11,12,13,16,17: #z #j normalize nodelta #_ 964 cases (lookup ???? 〈0,short_jump〉) #x #y 965 whd in match (snd ℕ jump_expansion_policy ?) 966 >lookup_insert_hit normalize @jmpleq_max_length 967 ] 968 4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y 969 whd in match (snd ℕ jump_expansion_policy ?) 970 >lookup_insert_hit normalize @jmpleq_max_length 971 ] 972  @le_n 973 ] 974 ] 904 975 ] 905 976  @conj 906 977 [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 907  //978  #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 908 979 ] 909 980 ]
Note: See TracChangeset
for help on using the changeset viewer.