Changeset 2242
 Timestamp:
 Jul 24, 2012, 1:01:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2241 r2242 918 918 919 919 lemma jump_expansion_step7: 920 (* 921 program : 922 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 923 labels : 924 (Σlm:label_map 925 .(∀l:identifier ASMTag 926 .occurs_exactly_once ASMTag pseudo_instruction l program 927 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 928 =address_of_word_labels_code_mem program l)) 929 old_sigma : 930 (Σpolicy:ppc_pc_map 931 .not_jump_default program policy 932 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 933 〈O,short_jump〉) 934 =O 935 ∧\fst policy 936 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 937 (\snd policy) 〈O,short_jump〉) 938 ∧sigma_compact_unsafe program labels policy 939 ∧\fst policy≤ 2 \sup 16 )*) 940 ∀prefix : list (option Identifier×pseudo_instruction).(* 941 x : (option Identifier×pseudo_instruction) 942 tl : (list (option Identifier×pseudo_instruction)) 943 prf : (program=prefix@[x]@tl) 944 acc : 945 (Σx0:ℕ×ppc_pc_map 946 .(let 〈added,policy〉 ≝x0 in 947 not_jump_default prefix policy 948 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 949 〈O,short_jump〉) 950 =O 951 ∧\fst policy 952 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 953 (\snd policy) 〈O,short_jump〉) 954 ∧jump_increase prefix old_sigma policy 955 ∧sigma_compact_unsafe prefix labels policy 956 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 957 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 958 ∧out_of_program_none prefix policy 959 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 960 (\snd policy) 〈O,short_jump〉) 961 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 962 (\snd old_sigma) 〈O,short_jump〉) 963 +added 964 ∧sigma_safe prefix labels added old_sigma policy)) 965 inc_added : ℕ 966 inc_pc_sigma : ppc_pc_map 967 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 920 ∀old_sigma : ppc_pc_map. 921 ∀prefix : list (option Identifier×pseudo_instruction). 968 922 ∀label : option Identifier. 969 ∀instr : pseudo_instruction.(* 970 p1 : (x≃〈label,instr〉) 971 add_instr ≝ 972 match instr 973 in pseudo_instruction 974 return λ_:pseudo_instruction.(option jump_length) 975 with 976 [Instruction (i:(preinstruction Identifier))⇒ 977 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 978 (prefix) i 979 Comment (_:String)⇒None jump_length 980 Cost (_:costlabel)⇒None jump_length 981 Jmp (j:Identifier)⇒ 982 Some jump_length 983 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 984 Call (c:Identifier)⇒ 985 Some jump_length 986 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 987 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 988 inc_pc : ℕ 989 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 990 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 991 old_pc : ℕ 992 old_length : jump_length 993 Holdeq : 994 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 995 〈O,short_jump〉 996 =〈old_pc,old_length〉) 997 Hpolicy : 998 (not_jump_default prefix 〈inc_pc,inc_sigma〉 999 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 1000 〈O,short_jump〉) 1001 =O 1002 ∧inc_pc 1003 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1004 〈O,short_jump〉) 1005 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 1006 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 1007 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 1008 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 1009 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 1010 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1011 〈O,short_jump〉) 1012 =old_pc+inc_added 1013 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉) 1014 added : ℕ*) 1015 ∀policy : ppc_pc_map.(* 1016 new_length : jump_length 1017 isize : ℕ 1018 Heq1 : 1019 (match 1020 match instr 1021 in pseudo_instruction 1022 return λ_:pseudo_instruction.(option jump_length) 1023 with 1024 [Instruction (i:(preinstruction Identifier))⇒ 1025 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1026 (prefix) i 1027 Comment (_:String)⇒None jump_length 1028 Cost (_:costlabel)⇒None jump_length 1029 Jmp (j:Identifier)⇒ 1030 Some jump_length 1031 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1032 Call (c:Identifier)⇒ 1033 Some jump_length 1034 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1035 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1036 in option 1037 return λ_0:(option jump_length).(jump_length×ℕ) 1038 with 1039 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 1040 Some (pl:jump_length)⇒ 1041 〈max_length old_length pl, 1042 instruction_size_jmplen (max_length old_length pl) instr〉] 1043 =〈new_length,isize〉) 1044 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 1045 prefix_ok : (prefix< 2 \sup 16 ) 1046 Heq2a : 1047 (match 1048 match instr 1049 in pseudo_instruction 1050 return λ_0:pseudo_instruction.(option jump_length) 1051 with 1052 [Instruction (i:(preinstruction Identifier))⇒ 1053 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1054 (prefix) i 1055 Comment (_0:String)⇒None jump_length 1056 Cost (_0:costlabel)⇒None jump_length 1057 Jmp (j:Identifier)⇒ 1058 Some jump_length 1059 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1060 Call (c:Identifier)⇒ 1061 Some jump_length 1062 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1063 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 1064 in option 1065 return λ_0:(option jump_length).ℕ 1066 with 1067 [None⇒inc_added 1068 Some (x0:jump_length)⇒ 1069 inc_added+(isizeinstruction_size_jmplen old_length instr)] 1070 =added) 1071 Heq2b : 1072 (〈inc_pc+isize, 923 ∀instr : pseudo_instruction. 924 ∀inc_pc : ℕ. 925 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. 926 ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉. 927 ∀policy : ppc_pc_map. 928 ∀new_length : jump_length. 929 ∀isize : ℕ. 930 ∀Heq2b : 931 〈inc_pc+isize, 1073 932 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1074 933 〈inc_pc+isize, … … 1077 936 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1078 937 〈inc_pc,new_length〉 inc_sigma)〉 1079 =policy) 1080 *) 938 =policy. 1081 939 out_of_program_none (prefix@[〈label,instr〉]) policy. 1082 cases daemon (* 940 #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length 941 #isize #Heq2b 1083 942 #i #Hi2 >append_length <commutative_plus @conj 1084 [ (* → *) #Hi normalize in Hi; 1085 cases instr in Heq2; normalize nodelta 1086 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 1087 [1,3,5,7,9,11: >lookup_opt_insert_miss 1088 [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *) 1089 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2)) 1090 @le_S_to_le @Hi 1091 2,4,6,8,10,12: @bitvector_of_nat_abs 1092 [1,4,7,10,13,16: @Hi2 1093 2,5,8,11,14,17: @(transitive_lt … Hi2) 1094 3,6,9,12,15,18: @sym_neq @lt_to_not_eq 1095 ] @le_S_to_le @Hi 1096 ] 1097 2,4,6,8,10,12: @bitvector_of_nat_abs 1098 [1,4,7,10,13,16: @Hi2 1099 2,5,8,11,14,17: @(transitive_lt … Hi2) 1100 3,6,9,12,15,18: @sym_neq @lt_to_not_eq 1101 ] @Hi 1102 ] 1103  (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl 1104 elim (decidable_lt i (prefix)) 1105 [ #Hi 943 [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss 944 [ >lookup_opt_insert_miss 945 [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi 946  @bitvector_of_nat_abs try assumption 947 [ @(transitive_lt … Hi2) @le_S_to_le assumption 948  % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i))) 949 @(transitive_le … abs) %2 % ]] 950  @bitvector_of_nat_abs try assumption 951 [ @(transitive_lt … Hi2) assumption 952  % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]] 953  (* ← *) <Heq2b #Hl normalize 954 @(leb_elim (S i) (prefix)) 955 [ #Hi 1106 956 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 1107 957 #Hl2 (* USE[pass]: out_of_program_none ← *) 1108 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)1109 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 958 cases (Hpolicy1 i Hi2) #_ 959 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption 1110 960  #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) 1111 961 [ #Hi3 elim (le_to_or_lt_eq … Hi3) 1112 [ / by /962 [ #X @X 1113 963  #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H) 1114 964 ] 1115 965  #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 1116 >X >eq_bv_refl #H normalize in H; destruct (H) 1117 ] 1118 ] 1119 ]*) 966 >X >eq_bv_refl #H normalize in H; destruct (H)]]] 1120 967 qed. 1121 968
Note: See TracChangeset
for help on using the changeset viewer.