Changeset 915
 Timestamp:
 Jun 9, 2011, 11:30:59 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r912 r915 1351 1351 1352 1352 axiom assembly_ok: 1353 ∀program,assembled,costs,labels ,datalabels.1354 Some … 〈labels, datalabels〉 = build_maps program →1353 ∀program,assembled,costs,labels. 1354 Some … 〈labels,costs〉 = build_maps program → 1355 1355 Some … 〈assembled,costs〉 = assembly program → 1356 1356 let code_memory ≝ load_code_memory assembled in 1357 let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in 1357 let preamble ≝ \fst program in 1358 let datalabels ≝ construct_datalabels preamble in 1359 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 1358 1360 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 1359 1361 ∀ppc,len,assembledi. … … 1365 1367 1366 1368 axiom bitvector_of_nat_nat_of_bitvector: 1367 ∀n,v. bitvector_of_nat n (nat_of_bitvector n v) = v. 1369 ∀n,v. 1370 bitvector_of_nat n (nat_of_bitvector n v) = v. 1368 1371 1369 1372 lemma fetch_assembly_pseudo2: 1370 ∀program,assembled,costs,labels ,datalabels.1371 Some … 〈labels, datalabels〉 = build_maps program →1373 ∀program,assembled,costs,labels. 1374 Some … 〈labels,costs〉 = build_maps program → 1372 1375 Some … 〈assembled,costs〉 = assembly program → 1373 let code_memory ≝ load_code_memory assembled in1374 let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in1375 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in1376 1376 ∀ppc,instructions. 1377 let code_memory ≝ load_code_memory assembled in 1378 let preamble ≝ \fst program in 1379 let data_labels ≝ construct_datalabels preamble in 1380 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 1381 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1377 1382 let expansion ≝ jump_expansion_policy program ppc in 1378 1383 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1379 1384 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → 1380 1385 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1381 #program #assembled #costs #labels #datalabels #BUILD_MAPS #ASSEMBLY #ppc #instructions whd 1386 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions 1387 letin code_memory ≝ (load_code_memory assembled) 1388 letin preamble ≝ (\fst program) 1389 letin data_labels ≝ (construct_datalabels preamble) 1390 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) 1391 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 1392 whd 1382 1393 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc) 1383 1394 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1384 1395 generalize in match (fetch_assembly_pseudo program ppc 1385 (λx. lookup ?? x labels (zero ?)) (λx. lookup ?? x datalabels (zero ?)) pi1386 (load_code_memory assembled)) 1396 (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi 1397 (load_code_memory assembled)); 1387 1398 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?) 1388 1399 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
Note: See TracChangeset
for help on using the changeset viewer.