Changeset 2024
 Timestamp:
 Jun 7, 2012, 3:20:53 PM (5 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2021 r2024 1517 1517 ∀sigma: Word → Word. 1518 1518 ∀policy: Word → bool. 1519 let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd program) x)in1519 let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd program) x in 1520 1520 ∀ppc. 1521 1521 ∀code_memory. 1522 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in1522 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in 1523 1523 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1524 1524 let pc ≝ sigma ppc in … … 1610 1610 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 1611 1611 let code_memory ≝ load_code_memory assembled in 1612 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x)in1612 let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 1613 1613 ∀ppc. 1614 1614 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in … … 1672 1672 let code_memory ≝ load_code_memory assembled in 1673 1673 let data_labels ≝ construct_datalabels (\fst program) in 1674 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x)in1674 let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 1675 1675 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 1676 1676 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in … … 2347 2347 2348 2348 (*CSC: ???*) 2349 (* XXX: we need a precondition here stating that the PPC is within the 2350 bounds of the instruction list in order for Jaap's specification to 2351 apply. 2352 *) 2349 2353 lemma snd_assembly_1_pseudoinstruction_ok: 2350 2354 ∀program: pseudo_assembly_program. … … 2353 2357 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 2354 2358 ∀ppc: Word. 2359 ∀ppc_in_bounds: nat_of_bitvector 16 ppc ≤ \snd program. 2355 2360 ∀pi. 2356 2361 ∀lookup_labels. 2357 2362 ∀lookup_datalabels. 2358 lookup_labels = (λx. sigma(address_of_word_labels_code_mem (\snd program) x)) →2363 lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) → 2359 2364 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2360 2365 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2361 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels 2366 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2362 2367 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2363 #program #sigma #policy #sigma_policy_specification_witness #ppc #p i2368 #program #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi 2364 2369 #lookup_labels #lookup_datalabels 2365 2370 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl … … 2385 2390 <sigma_newppc_refl 2386 2391 generalize in match fetch_pseudo_refl'; 2392 (* XXX: use ppc_in_bounds to get rid of the cases not_implemented in 2393 fetch_pseudo_instruction, as this is exactly what we need now! 2394 *) 2387 2395 whd in match (fetch_pseudo_instruction ??); 2388 2396 @pair_elim #lbl #instr #nth_refl normalize nodelta 2389 #G cases (pair_destruct_right ?????? G) % 2397 #G cases (pair_destruct_right ?????? G) 2398 lapply (sigma_policy_specification_witness ppc) 2399 >program_refl normalize nodelta #policy_hyp 2400 cases policy_hyp policy_hyp #policy_hyp1 #_ 2401 >policy_hyp1 2402 [1: 2403 policy_hyp1 whd in match instruction_size; normalize nodelta 2404 <pi_refl' >(?: pi' = \fst (fetch_pseudo_instruction (\snd program) ppc)) 2405 [1: >program_refl % ] >fetch_pseudo_refl' % 2406 2: 2407 >program_refl in ppc_in_bounds; #relevant assumption 2408 ] 2390 2409 qed. 2391 2410 
src/ASM/AssemblyProofSplit.ma
r2023 r2024 1394 1394 1395 1395 theorem main_thm: 1396 ∀M. 1397 ∀M'. 1396 ∀M, M': internal_pseudo_address_map. 1398 1397 ∀program: pseudo_assembly_program. 1399 1398 ∀sigma: Word → Word. … … 1408 1407 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 1409 1408 @(pose … (program_counter ?? ps)) #ppc #EQppc 1409 check fetch_assembly_pseudo2 1410 1410 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?; 1411 1411 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta … … 1459 1459 >EQassembled in fetch_many_assm; 1460 1460 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * 1461 #eq_instr #EQticks whd in EQticks:(???%); >EQticks1461 #eq_instr 1462 1462 #fetch_many_assm whd in fetch_many_assm; 1463 1463 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 1464 >(eq_instruction_to_eq … eq_instr) instrwhd in ⊢ (??%?);1464 destruct whd in ⊢ (??%?); 1465 1465 (* XXX: now we start to work on the mk_PreStatus equality *) 1466 1466 (* XXX: lhs *) … … 1470 1470 >set_arg_16_mk_Status_commutation 1471 1471 (* XXX: rhs *) 1472 change with ( ? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)1472 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); 1473 1473 >set_program_counter_mk_Status_commutation 1474 1474 >set_clock_mk_Status_commutation … … 1480 1480 2: 1481 1481 @special_function_registers_8051_set_arg_16 1482 [2: >EQlookup_datalabels%1482 [2: % 1483 1483 1: // 1484 1484 ] 1485 1485 ] 1486 1486 1: (* Instruction *) pi; #instr 1487 @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness 1487 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy 1488 sigma_policy_witness ps ppc EQppc labels costs create_label_cost_refl ? lookup_datalabels) 1489 check (main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness 1488 1490 … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels … 1489 1491 EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
Note: See TracChangeset
for help on using the changeset viewer.