Changeset 924 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 9, 2011, 4:14:54 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r923 r924 1369 1369 bitvector_of_nat n (nat_of_bitvector n v) = v. 1370 1370 1371 axiom assembly_ok_to_expand_pseudo_instruction_ok: 1372 ∀program,assembled,costs. 1373 Some … 〈assembled,costs〉 = assembly program → 1374 ∀ppc. 1375 let code_memory ≝ load_code_memory assembled in 1376 let preamble ≝ \fst program in 1377 let data_labels ≝ construct_datalabels preamble in 1378 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 1379 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1380 let expansion ≝ jump_expansion ppc program in 1381 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1382 ∃instructions. 1383 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi. 1384 1371 1385 lemma fetch_assembly_pseudo2: 1372 1386 ∀program,assembled,costs,labels. 1373 1387 Some … 〈labels,costs〉 = build_maps program → 1374 1388 Some … 〈assembled,costs〉 = assembly program → 1375 ∀ppc ,instructions.1389 ∀ppc. 1376 1390 let code_memory ≝ load_code_memory assembled in 1377 1391 let preamble ≝ \fst program in … … 1381 1395 let expansion ≝ jump_expansion ppc program in 1382 1396 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1383 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi → 1384 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1385 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions 1397 ∃instructions. 1398 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ 1399 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1400 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc 1401 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc) 1386 1402 letin code_memory ≝ (load_code_memory assembled) 1387 1403 letin preamble ≝ (\fst program) … … 1389 1405 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) 1390 1406 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 1391 whd 1407 whd in ⊢ (% → %) 1392 1408 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc) 1393 1409 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc … … 1395 1411 (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi 1396 1412 (load_code_memory assembled)); 1397 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)1398 #H1 #H2 whd #EXPANDwhd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);1413 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND 1414 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 1399 1415 normalize nodelta in EXPAND; (* HERE *) 1400 1416 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1 … … 1404 1420 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2 1405 1421 generalize in match (H1 ?? (refl …) (refl …) ?) -H1; 1406 [ #K3 @K3| @K1 ]1422 [ #K3 % [2: % [% | @K3]] | @K1 ] 1407 1423 qed. 1408 1424 … … 1615 1631 whd in match (\snd 〈final_pc,assembled〉) in H; 1616 1632 -s s'' labels costs final_ppc final_pc; 1633 (* NICE STATEMENT HERE *)
Note: See TracChangeset
for help on using the changeset viewer.