 Timestamp:
 Jun 9, 2011, 1:22:15 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r906 r908 1364 1364 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len). 1365 1365 1366 axiom bitvector_of_nat_nat_of_bitvector: 1367 ∀n,v. bitvector_of_nat n (nat_of_bitvector n v) = v. 1368 1369 lemma fetch_assembly_pseudo2: 1370 ∀program,assembled,costs,labels,datalabels. 1371 Some … 〈labels,datalabels〉 = build_maps program → 1372 Some … 〈assembled,costs〉 = assembly program → 1373 let code_memory ≝ load_code_memory assembled in 1374 let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in 1375 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 1376 ∀ppc,instructions. 1377 let expansion ≝ jump_expansion_policy program ppc in 1378 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1379 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → 1380 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1381 #program #assembled #costs #labels #datalabels #BUILD_MAPS #ASSEMBLY #ppc #instructions whd 1382 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc) 1383 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1384 generalize in match (fetch_assembly_pseudo program ppc 1385 (λx. lookup ?? x labels (zero ?)) (λx. lookup ?? x datalabels (zero ?)) pi 1386 (load_code_memory assembled)) 1387 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?) 1388 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 1389 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) 1390 #H1 #H2 1391 cases (H2 ?? (refl …)) H2; #K1 #K2 >K2 1392 generalize in match (H1 ??? (nat_of_bitvector … (sigma program ppc)) (refl …) (refl …) ?) H1; 1393 [ #K3 >bitvector_of_nat_nat_of_bitvector in K3; #R @R 1394  >bitvector_of_nat_nat_of_bitvector @K1 ] 1395 qed. 1396 1366 1397 (* OLD? 1367 1398 definition assembly_specification:
Note: See TracChangeset
for help on using the changeset viewer.