Changeset 2021 for src/ASM/Assembly.ma
 Timestamp:
 Jun 7, 2012, 1:44:18 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2015 r2021 1224 1224 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 1225 1225 qed. 1226 1226 1227 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_safe *) 1228 lemma nth_safe_prepend: 1229 ∀A,l1,l2,j.∀H:j<l2.∀K:l1+j<(l1@l2). 1230 nth_safe A j l2 H =nth_safe A (l1+j) (l1@l2) K. 1231 #A #l1 elim l1 normalize // 1232 qed. 1233 1234 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_prefix *) 1235 lemma shift_nth_prefix: 1236 ∀T,l1,i,l2,K1,K2. 1237 nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2. 1238 #T #l1 elim l1 normalize 1239 [ 1240 #i #l1 #K1 cases(lt_to_not_zero … K1) 1241  1242 #hd #tl #IH #i #l2 1243 cases i 1244 [ 1245 // 1246  1247 #i' #K1 #K2 whd in ⊢ (??%%); 1248 @IH 1249 ] 1250 ] 1251 qed. 1252 1253 lemma nth_cons: 1254 ∀A,hd,tl,l2,j,d. 1255 nth j A (tl@l2) d =nth (1+j) A (hd::tl@l2) d. 1256 // 1257 qed. 1258 1259 (*CSC: move elsewhere *) 1260 lemma fetch_pseudo_instruction_append: 1261 ∀l1,l2,ppc. 1262 let code_newppc ≝ fetch_pseudo_instruction l2 ppc in 1263 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) = 1264 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉. 1265 #l1 elim l1 1266 [ #l2 #ppc >add_commutative <add_zero >add_commutative <add_zero // 1267  #hd #tl #IH #l2 #ppc whd whd in match fetch_pseudo_instruction in ⊢ (??%?); normalize nodelta 1268 (*CSC: FALSE, NEED INVARIANT? *) 1269 > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (hd::tl)) ppc) 1270 = 1 + nat_of_bitvector … (add … (bitvector_of_nat … (tl)) ppc)) [2: cases daemon] 1271 <nth_cons lapply (IH l2 ppc) IH normalize nodelta cases (fetch_pseudo_instruction l2 ppc) 1272 #i #newppc whd in match fetch_pseudo_instruction; normalize nodelta 1273 cases (nth ? labelled_instruction ??) #i' #newppc' normalize nodelta #EQ 1274 destruct EQ change with (add ??? = ?) in e0; 1275 (*CSC: TRUE, NEEDS TRIVIAL ARITHMETICS *) cases daemon 1276 ] 1277 qed. 1278 1227 1279 definition assembly: 1228 1280 ∀p: pseudo_assembly_program. 1229 1281 ∀sigma: Word → Word. 1230 1282 ∀policy: Word → bool. 1231 list Byte × (BitVectorTrie costlabel 16) ≝ 1283 Σres:list Byte × (BitVectorTrie costlabel 16). 1284 let 〈preamble,instr_list〉 ≝ p in 1285 let 〈assembled,costs〉 ≝ res in 1286 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1287 let datalabels ≝ construct_datalabels preamble in 1288 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1289 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1290 ∀ppc. 1291 nat_of_bitvector … ppc < instr_list → 1292 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in 1293 let 〈len,assembledi〉 ≝ 1294 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1295 ∀j:nat. ∀H: j < assembledi. ∀K. 1296 nth_safe ? j assembledi H = 1297 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) 1298 assembled K 1299 ≝ 1232 1300 λp. 1233 1301 λsigma. 1234 1302 λpolicy. 1235 let 〈preamble, instr_list〉≝ p in1303 deplet 〈preamble, instr_list〉 as p_refl ≝ p in 1236 1304 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1237 1305 let datalabels ≝ construct_datalabels preamble in 1238 1306 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1239 1307 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1240 let result ≝1241 pi1 ?? (foldl_strong1308 let 〈ignore,revcode〉 ≝ pi1 … ( 1309 foldl_strong 1242 1310 (option Identifier × pseudo_instruction) 1243 (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))). 1244 let 〈pc,ppc_code〉 ≝ pc_ppc_code in 1311 (λpre. Σppc_code:(Word × (list Byte)). 1245 1312 let 〈ppc,code〉 ≝ ppc_code in 1313 ppc = bitvector_of_nat … (pre) ∧ 1246 1314 ∀ppc'. 1247 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1248 let 〈len,assembledi〉 ≝ 1249 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1250 True) 1315 nat_of_bitvector … ppc' < nat_of_bitvector … ppc → 1316 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1317 let 〈len,assembledi〉 ≝ 1318 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1319 ∀j:nat. ∀H: j < assembledi. ∀K. 1320 nth_safe ? j assembledi H = 1321 nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K) 1251 1322 instr_list 1252 (λprefix,hd,tl,prf,pc_ppc_code. 1253 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 1254 let 〈ppc, code〉 ≝ ppc_code in 1323 (λprefix,hd,tl,prf,ppc_code. 1324 let 〈ppc, code〉 ≝ pi1 … ppc_code in 1255 1325 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in 1256 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in1257 1326 let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in 1258 〈new_p c, 〈new_ppc, (code @ program)〉〉)1259 〈(zero ?), 〈(zero ?), [ ]〉〉)1327 〈new_ppc, (reverse … program @ code)〉) 1328 〈(zero ?), [ ]〉) 1260 1329 in 1261 〈 \snd (\snd result),1330 〈reverse … revcode, 1262 1331 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1263 @pair_elim normalize nodelta #x #y #z 1264 @pair_elim normalize nodelta #w1 #w2 #w3 #w4 1265 @pair_elim // 1332 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 1333 >EQignore_revcode in Hfold; * #_ #Hfold whd >p1 whd #ppc #LTppc @Hfold 1334 (* CSC: ??? *) cases daemon 1335  % // #ppc' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 1336  cases ppc_code in p1; ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; EQppc_code 1337 * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)] 1338 whd #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 1339 cases (le_to_or_lt_eq … LTppc') 1340 [2: #S_S_eq normalize nodelta in S_S_eq; 1341 (*CSC: FALSE, NEEDS INVARIANT *) 1342 cut (ppc' = ppc) [cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' #LTppc 1343 >prf >IH1 in ⊢ match % with [_ ⇒ ?]; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ match % with [_ ⇒ ?]; 1344 @pair_elim #pi' #newppc' >fetch_pseudo_instruction_append #EQpair destruct(EQpair) 1345 >p2 1346 #j #LTj 1347 (* CSC: FALSE, NEEDS INVARIANT *) 1348 >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) = 1349 nat_of_bitvector … (sigma ppc) + j) [2: cases daemon] 1350 >reverse_append >reverse_reverse 1351 (* CSC: TRUE, NEEDS INVARIANT *) 1352 >(? : nat_of_bitvector … (sigma ppc) = reverse … code) [2: cases daemon] 1353 @nth_safe_prepend 1354  #LTppc' lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ] 1355 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1356 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH 1357 change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<assembledi.?) 1358 >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K 1359 >IH 1360 [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon 1361  @shift_nth_prefix 1362 ] 1363 ] 1364 ] 1266 1365 qed. 1267 1366
Note: See TracChangeset
for help on using the changeset viewer.