- Timestamp:
- Jul 24, 2012, 2:31:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyStep.ma
r2242 r2243 4 4 include alias "basics/logic.ma". 5 5 6 lemma not_is_jump_to_destination_of_No me:6 lemma not_is_jump_to_destination_of_None: 7 7 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None …. 8 8 * try (#x #y #H) try (#y #H) try #H cases H % 9 qed. 10 11 lemma destination_of_None_to_is_jump_false: 12 ∀instr. destination_of instr = None … → is_jump' instr = false. 13 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs) 14 qed. 15 16 lemma destination_of_Some_to_is_jump_true: 17 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true. 18 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs 19 destruct(abs) 9 20 qed. 10 21 … … 65 76 |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 66 77 #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H; 67 >not_is_jump_to_destination_of_No me in H; normalize nodelta // ]78 >not_is_jump_to_destination_of_None in H; normalize nodelta // ] 68 79 | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]] 69 80 qed. … … 101 112 | @bitvector_of_nat_abs try assumption @lt_O_S ]] 102 113 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ] 103 qed.104 105 lemma destination_of_None_to_is_jump_false:106 ∀instr. destination_of instr = None … → is_jump' instr = false.107 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)108 qed.109 110 lemma destination_of_Some_to_is_jump_true:111 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.112 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs113 destruct(abs)114 114 qed. 115 115 … … 968 968 969 969 lemma jump_expansion_step8: 970 (* 971 program : 972 (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l) 973 labels : 974 (Σlm:label_map 975 .(∀l:identifier ASMTag 976 .occurs_exactly_once ASMTag pseudo_instruction l program 977 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 978 =address_of_word_labels_code_mem program l))*) 979 ∀old_sigma : ppc_pc_map.(* 980 (Σpolicy:ppc_pc_map 981 .not_jump_default program policy 982 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 983 〈O,short_jump〉) 984 =O 985 ∧\fst policy 986 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|)) 987 (\snd policy) 〈O,short_jump〉) 988 ∧sigma_compact_unsafe program labels policy 989 ∧\fst policy≤ 2 \sup 16 )*) 990 ∀prefix : list (option Identifier×pseudo_instruction).(* 991 x : (option Identifier×pseudo_instruction) 992 tl : (list (option Identifier×pseudo_instruction)) 993 prf : (program=prefix@[x]@tl) 994 acc : 995 (Σx0:ℕ×ppc_pc_map 996 .(let 〈added,policy〉 ≝x0 in 997 not_jump_default prefix policy 998 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 999 〈O,short_jump〉) 1000 =O 1001 ∧\fst policy 1002 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 1003 (\snd policy) 〈O,short_jump〉) 1004 ∧jump_increase prefix old_sigma policy 1005 ∧sigma_compact_unsafe prefix labels policy 1006 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 1007 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 1008 ∧out_of_program_none prefix policy 1009 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 1010 (\snd policy) 〈O,short_jump〉) 1011 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 1012 (\snd old_sigma) 〈O,short_jump〉) 1013 +added 1014 ∧sigma_safe prefix labels added old_sigma policy)) 1015 inc_added : ℕ 1016 inc_pc_sigma : ppc_pc_map 1017 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 970 ∀program : list labelled_instruction. 971 ∀labels : label_map. 972 ∀old_sigma : 973 Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst policy≤ 2 \sup 16. 974 ∀prefix : list (option Identifier×pseudo_instruction). 975 ∀x : option Identifier×pseudo_instruction. 976 ∀tl : list (option Identifier×pseudo_instruction). 977 ∀prf : program=prefix@[x]@tl. 978 ∀inc_added : ℕ. 979 ∀inc_pc_sigma : ppc_pc_map. 1018 980 ∀label : option Identifier. 1019 ∀instr : pseudo_instruction.(* 1020 p1 : (x≃〈label,instr〉) 1021 add_instr ≝ 1022 match instr 1023 in pseudo_instruction 1024 return λ_:pseudo_instruction.(option jump_length) 1025 with 1026 [Instruction (i:(preinstruction Identifier))⇒ 1027 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1028 (|prefix|) i 1029 |Comment (_:String)⇒None jump_length 1030 |Cost (_:costlabel)⇒None jump_length 1031 |Jmp (j:Identifier)⇒ 1032 Some jump_length 1033 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 1034 |Call (c:Identifier)⇒ 1035 Some jump_length 1036 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 1037 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1038 inc_pc : ℕ 1039 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 1040 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 1041 old_pc : ℕ 1042 old_length : jump_length 1043 Holdeq : 1044 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) 981 ∀instr : pseudo_instruction. 982 ∀p1 : x≃〈label,instr〉. 983 ∀inc_pc : ℕ. 984 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. 985 ∀old_pc : ℕ. 986 ∀old_length : jump_length. 987 ∀Holdeq : 988 lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) 1045 989 〈O,short_jump〉 1046 =〈old_pc,old_length〉) 1047 Hpolicy : 1048 (not_jump_default prefix 〈inc_pc,inc_sigma〉 1049 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 1050 〈O,short_jump〉) 1051 =O 1052 ∧inc_pc 1053 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 1054 〈O,short_jump〉) 1055 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 1056 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 1057 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 1058 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 1059 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 1060 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 1061 〈O,short_jump〉) 1062 =old_pc+inc_added 1063 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 990 =〈old_pc,old_length〉. 991 ∀Hpolicy1 : inc_pc 992 =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). 993 ∀Hpolicy2: \fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉) 994 =old_pc+inc_added. 1064 995 ∀added : ℕ. 1065 ∀policy : ppc_pc_map.(* 1066 new_length : jump_length 1067 isize : ℕ 1068 Heq1 : 1069 (match 1070 match instr 1071 in pseudo_instruction 1072 return λ_:pseudo_instruction.(option jump_length) 1073 with 1074 [Instruction (i:(preinstruction Identifier))⇒ 1075 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1076 (|prefix|) i 1077 |Comment (_:String)⇒None jump_length 1078 |Cost (_:costlabel)⇒None jump_length 1079 |Jmp (j:Identifier)⇒ 1080 Some jump_length 1081 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 1082 |Call (c:Identifier)⇒ 1083 Some jump_length 1084 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 1085 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1086 in option 1087 return λ_0:(option jump_length).(jump_length×ℕ) 1088 with 996 ∀policy : ppc_pc_map. 997 ∀new_length : jump_length. 998 ∀isize : ℕ. 999 let add_instr ≝ match instr with 1000 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 1001 | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 1002 | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i 1003 | _ ⇒ None ? 1004 ] in 1005 ∀Heq1 : 1006 match add_instr with 1089 1007 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 1090 1008 |Some (pl:jump_length)⇒ 1091 1009 〈max_length old_length pl, 1092 1010 instruction_size_jmplen (max_length old_length pl) instr〉] 1093 =〈new_length,isize〉) 1094 prefix_ok1 : (S (|prefix|)< 2 \sup 16 ) 1095 prefix_ok : (|prefix|< 2 \sup 16 ) 1096 Heq2a : 1097 (match 1098 match instr 1099 in pseudo_instruction 1100 return λ_0:pseudo_instruction.(option jump_length) 1101 with 1102 [Instruction (i:(preinstruction Identifier))⇒ 1103 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1104 (|prefix|) i 1105 |Comment (_0:String)⇒None jump_length 1106 |Cost (_0:costlabel)⇒None jump_length 1107 |Jmp (j:Identifier)⇒ 1108 Some jump_length 1109 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 1110 |Call (c:Identifier)⇒ 1111 Some jump_length 1112 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 1113 |Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 1114 in option 1115 return λ_0:(option jump_length).ℕ 1116 with 1011 =〈new_length,isize〉. 1012 ∀Heq2a : 1013 match add_instr with 1117 1014 [None⇒inc_added 1118 1015 |Some (x0:jump_length)⇒ 1119 1016 inc_added+(isize-instruction_size_jmplen old_length instr)] 1120 =added )1121 Heq2b :1122 (〈inc_pc+isize,1017 =added. 1018 ∀Heq2b : 1019 〈inc_pc+isize, 1123 1020 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 1124 1021 〈inc_pc+isize, … … 1127 1024 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 1128 1025 〈inc_pc,new_length〉 inc_sigma)〉 1129 =policy) 1130 *) 1026 =policy. 1131 1027 \fst (lookup (ℕ×jump_length) 16 1132 1028 (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd policy) … … 1136 1032 〈O,short_jump〉) 1137 1033 +added. 1138 cases daemon(* 1139 <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O 1034 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr 1035 #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added 1036 #policy #new_length #isize #Heq1 #Heq2a #Heq2b 1037 <Heq2b >append_length <plus_n_Sm <plus_n_O 1140 1038 >lookup_insert_hit 1141 <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1; 1142 [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 1143 (* USE: sigma_compact_unsafe (from old_sigma) *) 1144 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1145 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1146 |2,4,6: lapply Holdeq -Holdeq 1147 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1148 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1149 [1,3,5: normalize nodelta #_ #_ #abs cases abs 1150 |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1151 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1152 [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 1153 |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 1154 #H (* USE: fst p = lookup |prefix| *) 1155 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1156 (* USE[pass]: lookup p = lookup old_sigma + added *) 1157 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 1158 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 1159 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second 1160 [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus 1161 >(associative_plus pc) @plus_left_monotone >commutative_plus 1162 @plus_right_monotone @instruction_size_irrelevant @nmk #H @H 1163 |2,4,6: @le_n 1164 ] 1165 ] 1166 ] 1167 ] 1168 |4,5: #x normalize nodelta #p1 #Heq1 1169 (* USE: sigma_compact_unsafe (from old_sigma) *) 1170 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1171 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1172 |2,4: lapply Holdeq -Holdeq 1173 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1174 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1175 [1,3: normalize nodelta #_ #_ #abs cases abs 1176 |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1177 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1178 [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 1179 |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 1180 #H (* USE: fst p = lookup |prefix| *) 1181 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1182 (* USE[pass]: lookup p = lookup old_sigma + added *) 1183 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 1184 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 1185 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus 1186 >(associative_plus pc) @plus_left_monotone >assoc_plus1 1187 >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative 1188 [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second 1189 [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus 1190 @minus_plus_m_m 1191 |2,4: @le_n 1192 ] 1193 |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I 1194 ] 1195 ] 1196 ] 1197 ] 1198 |1: #pi cases pi 1199 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 1200 [1,2,3,6,7,24,25: #x #y 1201 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 1202 normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 1203 (* USE: sigma_compact_unsafe (from old_sigma) *) 1204 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1205 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1206 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1207 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1208 lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1209 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1210 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1211 normalize nodelta #_ #_ #abs cases abs 1212 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1213 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1214 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1215 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1216 normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 1217 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1218 #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 1219 #H (* USE: fst p = lookup |prefix| *) 1220 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1221 (* USE[pass]: lookup p = lookup old_sigma + added *) 1222 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 1223 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 1224 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second 1225 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1226 <minus_n_n >p1 whd in match (nth ????); >associative_plus 1227 >(associative_plus pc) @plus_left_monotone >commutative_plus 1228 @plus_right_monotone @instruction_size_irrelevant @nmk #H @H 1229 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1230 @le_n 1231 ] 1232 ] 1233 ] 1234 ] 1235 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1 1236 (* USE: sigma_compact_unsafe (from old_sigma) *) 1237 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1238 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1239 |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq 1240 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1241 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1242 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs 1243 |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1244 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1245 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj 1246 normalize nodelta #_ #_ #abs cases abs 1247 |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j 1248 #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *) 1249 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1250 (* USE[pass]: lookup p = lookup old_sigma + added *) 1251 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 1252 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 1253 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus 1254 >(associative_plus pc) @plus_left_monotone >assoc_plus1 1255 >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative 1256 [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf 1257 >nth_append_second 1258 [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1 1259 >commutative_plus @minus_plus_m_m 1260 |2,4,6,8,10,12,14,16,18: @le_n 1261 ] 1262 |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1)) 1263 @jump_length_le_max @I 1264 ] 1265 ] 1266 ] 1267 ] 1268 ] 1269 ] *) 1039 <Heq2a cases instr in p1 Heq1; 1040 [1: #pi normalize nodelta whd in match jump_expansion_step_instruction; 1041 normalize nodelta lapply (destination_of_None_to_is_jump_false pi) 1042 lapply (destination_of_Some_to_is_jump_true pi) 1043 cases (destination_of ?) normalize nodelta ] 1044 try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1) 1045 <(proj2 ?? (pair_destruct ?????? Heq1)) 1046 (* USE: sigma_compact_unsafe (from old_sigma) *) 1047 lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?) 1048 [1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 1049 lapply Holdeq -Holdeq 1050 inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) 1051 [1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs] 1052 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) 1053 [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs] 1054 * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta 1055 #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*) 1056 >Hpolicy1 1057 (* USE[pass]: lookup p = lookup old_sigma + added *) 1058 >Hpolicy2 1059 [1,3,4,7: 1060 >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 1061 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 1062 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try % 1063 <minus_n_n >p1 whd in match (nth ????); >associative_plus 1064 >(associative_plus pc) @plus_left_monotone >commutative_plus 1065 @plus_right_monotone @instruction_size_irrelevant try % 1066 whd in match is_jump; normalize nodelta >y % 1067 |2,5,6: 1068 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H 1069 >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ 1070 -Holdeq <(proj1 ?? (pair_destruct ?????? EQ)) 1071 >associative_plus 1072 >(associative_plus pc) @plus_left_monotone >assoc_plus1 1073 >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative 1074 [1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma 1075 >nth_append_second try % 1076 <minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma 1077 >commutative_plus @minus_plus_m_m 1078 |*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try % 1079 whd in match is_jump; normalize nodelta >y %]] 1270 1080 qed. 1271 1081
Note: See TracChangeset
for help on using the changeset viewer.