Changeset 2024 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jun 7, 2012, 3:20:53 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
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.