Changeset 1482 for src/ASM/Assembly.ma
- Timestamp:
- Nov 2, 2011, 2:26:26 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1479 r1482 1121 1121 qed. 1122 1122 1123 axiom fetch_pseudo_instruction_split: 1124 ∀instr_list,ppc. 1125 ∃pre,suff,lbl. 1126 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list. 1127 1128 lemma sigma00_append: 1129 ∀instr_list,jump_expansion,l1,l2,acc. 1130 sigma00 instr_list jump_expansion (l1@l2) acc = 1131 sigma00 instr_list jump_expansion 1132 l2 (sigma00 instr_list jump_expansion l1 acc). 1133 whd in match sigma00; normalize nodelta; 1134 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append 1135 qed. 1136 1137 lemma sigma00_strict: 1138 ∀instr_list,jump_expansion,l,acc. acc = None ? → 1139 sigma00 instr_list jump_expansion l acc = None …. 1140 #instr_list #jump_expansion #l elim l 1141 [ #acc #H >H % 1142 | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ] 1143 qed. 1144 1145 lemma policy_ok_prefix_ok: 1146 ∀program.∀pol:policy program.∀suffix,prefix. 1147 prefix@suffix = \snd program → 1148 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None …. 1149 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%); 1150 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol 1151 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0 1152 normalize nodelta >sigma00_append 1153 cases (sigma00 ?? prefix ?) 1154 [2: #x #_ % #abs destruct(abs) 1155 | * #abs @⊥ @abs >sigma00_strict % ] 1156 qed. 1157 1158 lemma policy_ok_prefix_hd_ok: 1159 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map. 1160 (prefix@[hd])@suffix = \snd program → 1161 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) → 1162 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 1163 let 〈program_counter, sigma_map〉 ≝ pc_map in 1164 let 〈label, i〉 ≝ hd in 1165 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None …. 1166 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2 1167 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix 1168 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?) 1169 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta 1170 @pair_elim' #pc #map #EQ4 normalize nodelta 1171 @pair_elim' #l' #i' #EQ5 normalize nodelta 1172 cases (construct_costs_safe ??????) normalize 1173 [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)] 1174 qed. 1175 1123 1176 definition expand_pseudo_instruction: 1124 1177 ∀program:pseudo_assembly_program.∀pol: policy program. … … 1133 1186 [ None ⇒ let dummy ≝ [ ] in dummy 1134 1187 | Some res ⇒ res ]. 1135 [ cases daemon 1188 [ @⊥ whd in p:(??%??); 1189 generalize in match (sig2 ?? pol) whd in ⊢ (% → ?) 1190 whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????) 1191 generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉))) 1192 cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %] 1193 #res #K 1194 cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1 1195 generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ? 1196 cases daemon (* CSC: XXXXXXXX Ero qui 1197 1198 [3: @policy_ok_prefix_ok ] 1199 | sigma00 program pol pre 1200 1201 1202 1203 QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che 1204 fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc 1205 per concludere construct_costs_safe ≠ None *) 1136 1206 | >p %] 1137 1207 qed. … … 1211 1281 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i). 1212 1282 1283 (* 1284 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A. 1285 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l. 1286 1287 axiom foldl_strong_step: 1288 ∀A:Type[0]. 1289 ∀P: list A → Type[0]. 1290 ∀l: list A. 1291 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 1292 ∀acc: P [ ]. 1293 ∀Q: ∀prefix. P prefix → Prop. 1294 ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl. 1295 ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc). 1296 Q [ ] acc → 1297 Q l (foldl_strong A P l H acc). 1298 (* 1299 #A #P #l #H #acc #Q #HQ #Hacc normalize; 1300 generalize in match 1301 (foldl_strong ? 1302 (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?)) 1303 l ? Hacc) 1304 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ] 1305 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%) 1306 #K 1307 1308 generalize in match 1309 (foldl_strong ? 1310 (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre)))) 1311 [2: @H 1312 *) 1313 1314 axiom foldl_elim: 1315 ∀A:Type[0]. 1316 ∀B: Type[0]. 1317 ∀H: A → B → A. 1318 ∀acc: A. 1319 ∀l: list B. 1320 ∀Q: A → Prop. 1321 (∀acc:A.∀b:B. Q acc → Q (H acc b)) → 1322 Q acc → 1323 Q (foldl A B H acc l). 1324 *) 1325 1213 1326 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. 1214 1327 #A #a #b #EQ destruct // 1215 qed.1216 1217 lemma sigma00_strict:1218 ∀instr_list,jump_expansion,l,acc. acc = None ? →1219 sigma00 instr_list jump_expansion l acc = None ….1220 #instr_list #jump_expansion #l elim l1221 [ #acc #H >H %1222 | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]1223 qed.1224 1225 lemma sigma00_append:1226 ∀instr_list,jump_expansion,l1,l2,acc.1227 sigma00 instr_list jump_expansion (l1@l2) acc =1228 sigma00 instr_list jump_expansion1229 l2 (sigma00 instr_list jump_expansion l1 acc).1230 whd in match sigma00; normalize nodelta;1231 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append1232 qed.1233 1234 lemma policy_ok_prefix_ok:1235 ∀program.∀pol:policy program.∀suffix,prefix.1236 prefix@suffix = \snd program →1237 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….1238 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);1239 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol1240 whd in match policy_ok; whd in match sigma_safe; whd in match sigma01241 normalize nodelta >sigma00_append1242 cases (sigma00 ?? prefix ?)1243 [2: #x #_ % #abs destruct(abs)1244 | * #abs @⊥ @abs >sigma00_strict % ]1245 qed.1246 1247 lemma policy_ok_prefix_hd_ok:1248 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.1249 (prefix@[hd])@suffix = \snd program →1250 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →1251 let 〈ppc,pc_map〉 ≝ ppc_pc_map in1252 let 〈program_counter, sigma_map〉 ≝ pc_map in1253 let 〈label, i〉 ≝ hd in1254 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….1255 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ21256 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix1257 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)1258 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta1259 @pair_elim' #pc #map #EQ4 normalize nodelta1260 @pair_elim' #l' #i' #EQ5 normalize nodelta1261 cases (construct_costs_safe ??????) normalize1262 [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]1263 1328 qed. 1264 1329 … … 1352 1417 [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 1353 1418 <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H] 1354 | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]1419 | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ] 1355 1420 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]] 1356 1421 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
Note: See TracChangeset
for help on using the changeset viewer.