 Timestamp:
 Jun 7, 2012, 4:37:42 PM (9 years ago)
 Location:
 src/ASM
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2024 r2026 1393 1393 qed. 1394 1394 1395 theorem main_thm:1396 ∀M, M': internal_pseudo_address_map.1397 ∀program: pseudo_assembly_program.1398 ∀sigma: Word → Word.1399 ∀policy: Word → bool.1400 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.1401 ∀ps: PseudoStatus program.1402 next_internal_pseudo_address_map M program ps = Some … M' →1403 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =1404 status_of_pseudo_status M' …1405 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.1406 #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps1407 change with (next_internal_pseudo_address_map0 ????? = ? → ?)1408 @(pose … (program_counter ?? ps)) #ppc #EQppc1409 check fetch_assembly_pseudo21410 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;1411 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta1412 @pair_elim #assembled #costs' #assembly_refl normalize nodelta1413 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled1414 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta1415 @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels1416 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels1417 whd in match execute_1_pseudo_instruction; normalize nodelta1418 whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta1419 lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc1420 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)1421 [1: >fetch_pseudo_refl % ]1422 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;1423 generalize in match assm1; assm1 assm2 assm31424 normalize nodelta1425 cases pi1426 [2,3:1427 #arg1428 (* XXX: we first work on sigma_increment_commutation *)1429 #sigma_increment_commutation1430 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;1431 (* XXX: we work on the maps *)1432 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm1433 (* XXX: we assume the fetch_many hypothesis *)1434 #fetch_many_assm1435 (* XXX: we give the existential *)1436 %{0}1437 whd in match (execute_1_pseudo_instruction0 ?????);1438 (* XXX: work on the left hand side of the equality *)1439 whd in ⊢ (??%?);1440 @split_eq_status //1441 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]1442 6: (* Mov *)1443 #arg1 #arg21444 (* XXX: we first work on sigma_increment_commutation *)1445 #sigma_increment_commutation1446 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;1447 (* XXX: we work on the maps *)1448 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm1449 (* XXX: we assume the fetch_many hypothesis *)1450 #fetch_many_assm1451 (* XXX: we give the existential *)1452 %{1}1453 whd in match (execute_1_pseudo_instruction0 ?????);1454 (* XXX: work on the left hand side of the equality *)1455 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc1456 (* XXX: execute fetches some more *)1457 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta1458 whd in fetch_many_assm;1459 >EQassembled in fetch_many_assm;1460 cases (fetch ??) * #instr #newpc #ticks normalize nodelta *1461 #eq_instr1462 #fetch_many_assm whd in fetch_many_assm;1463 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc1464 destruct whd in ⊢ (??%?);1465 (* XXX: now we start to work on the mk_PreStatus equality *)1466 (* XXX: lhs *)1467 change with (set_arg_16 ????? = ?)1468 >set_program_counter_mk_Status_commutation1469 >set_clock_mk_Status_commutation1470 >set_arg_16_mk_Status_commutation1471 (* XXX: rhs *)1472 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);1473 >set_program_counter_mk_Status_commutation1474 >set_clock_mk_Status_commutation1475 >set_arg_16_mk_Status_commutation in ⊢ (???%);1476 (* here we are *)1477 @split_eq_status //1478 [1:1479 assumption1480 2:1481 @special_function_registers_8051_set_arg_161482 [2: %1483 1: //1484 ]1485 ]1486 1: (* Instruction *) pi; #instr1487 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy1488 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_witness1490 … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …1491 EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))1492 4,5: cases daemon1493 ]1494 qed.1495 1395 (* 1496 1396 *
Note: See TracChangeset
for help on using the changeset viewer.