Changeset 2272 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jul 27, 2012, 5:53:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2265 r2272 390 390 qed. 391 391 392 lemma get_index_v_set_index_hit: 393 ∀A: Type[0]. 394 ∀n: nat. 395 ∀v: Vector A n. 396 ∀i: nat. 397 ∀e: A. 398 ∀i_lt_n_proof: i < n. 399 ∀i_lt_n_proof': i < n. 400 get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e. 401 #A #n #v elim v 402 [1: 403 #i #e #i_lt_n_proof 404 cases (lt_to_not_zero … i_lt_n_proof) 405 |2: 406 #n' #hd #tl #inductive_hypothesis #i #e 407 cases i 408 [1: 409 #i_lt_n_proof #i_lt_n_proof' % 410 |2: 411 #i' #i_lt_n_proof' #i_lt_n_proof'' 412 whd in ⊢ (??%?); @inductive_hypothesis 413 ] 414 ] 415 qed. 392 axiom insert_low_internal_ram_of_pseudo_low_internal_ram': 393 ∀M, M', sigma,cm,s,addr,v,v'. 394 (∀addr'. 395 ((false:::addr) = addr' → 396 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = 397 map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧ 398 ((false:::addr) ≠ addr' → 399 let 〈callM, accM〉 ≝ M in 400 let 〈callM', accM'〉 ≝ M' in 401 accM = accM' ∧ 402 assoc_list_lookup … addr' (eq_bv 8) … callM = 403 assoc_list_lookup … addr' (eq_bv 8) … callM')) → 404 insert Byte 7 addr v' 405 (low_internal_ram_of_pseudo_low_internal_ram M' 406 (low_internal_ram pseudo_assembly_program cm s)) = 407 low_internal_ram_of_pseudo_low_internal_ram M 408 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 416 409 417 (*418 410 lemma write_at_stack_pointer_status_of_pseudo_status: 419 411 ∀M, M'. … … 423 415 ∀s, s'. 424 416 ∀new_b, new_b'. 425 M = M' → 426 map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' → 417 map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' → 427 418 status_of_pseudo_status M cm s sigma policy = s' → 428 419 write_at_stack_pointer ?? s' new_b' = 429 status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.420 status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy. 430 421 #M #M' #cm #sigma #policy #s #s' #new_b #new_b' 431 # Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl422 #new_b_refl #s_refl <new_b_refl <s_refl 432 423 whd in match write_at_stack_pointer; normalize nodelta 433 424 @pair_elim #nu #nl #nu_nl_refl normalize nodelta … … 449 440 ] 450 441 |2: 451 cases (get_index_v bool ????) normalize nodelta 452 whd in match status_of_pseudo_status; normalize nodelta 453 whd in match set_low_internal_ram; normalize nodelta 454 @split_eq_status try % 455 [1: 456 @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma) 457 |2: 458 @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma) 442 @if_then_else_status_of_pseudo_status try % 443 [2: 444 @sym_eq <set_low_internal_ram_status_of_pseudo_status 445 [1: 446 @eq_f2 447 [2: 448 @insert_low_internal_ram_of_pseudo_low_internal_ram' 449 @sym_eq 450 [2: 451 <set_low_internal_ram_status_of_pseudo_status 452 [1: 453 @eq_f2 454 [2: 455 @sym_eq 456 >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b') 457 [2: 458 >new_b_refl 459 ] 459 460 ] 460 *) 461 qed. 461 462 462 463 lemma main_lemma_preinstruction: … … 519 520 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 520 521 (get_arg_8 … s false addr2) false in 521 let cy_flag ≝ get_index' ? O 522 let cy_flag ≝ get_index' ? O ? flags in 522 523 let ac_flag ≝ get_index' ? 1 ? flags in 523 524 let ov_flag ≝ get_index' ? 2 ? flags in … … 917 918 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 918 919 whd in match execute_1_preinstruction; normalize nodelta 919 [ 1,2: (* ADD and ADDC *)920 [(*1,2: (* ADD and ADDC *) 920 921 (* XXX: work on the right hand side *) 921 922 (* XXX: switch to the left hand side *) … … 1535 1536 ] 1536 1537 ] 1537 |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1538 |*)12: (* JC *) 1539 >EQP -P normalize nodelta 1540 whd in match expand_pseudo_instruction; normalize nodelta 1541 whd in match expand_relative_jump; normalize nodelta 1542 whd in match expand_relative_jump_internal; normalize nodelta 1543 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1544 inversion sj_possible #sj_possible_refl normalize nodelta 1545 [1: 1546 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1547 whd in maps_assm:(??%%); 1548 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1549 whd in ⊢ (??%?); normalize nodelta 1550 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1551 whd in ⊢ (??%?); 1552 @if_then_else_status_of_pseudo_status 1553 >EQs >EQticks <instr_refl normalize nodelta 1554 [1: 1555 @(get_cy_flag_status_of_pseudo_status M') % 1556 |2: 1557 @sym_eq @set_program_counter_status_of_pseudo_status 1558 [1: 1559 |2: 1560 @sym_eq @set_clock_status_of_pseudo_status try % 1561 whd in match ticks_of0; normalize nodelta 1562 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1563 [1: 1564 @eq_f2 try % 1565 >sigma_increment_commutation 1566 lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta 1567 * #sigma_zero_assm #relevant cases (relevant ppc ?) 1568 [1: 1569 -relevant 1570 [2: 1571 >EQcm assumption 1572 |1: 1573 #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f 1574 >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2 1575 ] 1576 |2: 1577 ] 1578 |2: 1579 >sj_possible_refl % 1580 ] 1581 ] 1582 |3: 1583 ] 1584 ] 1538 1585 cases daemon 1539 |29,30: (* ANL and ORL *) 1586 |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1587 cases daemon 1588 |(*29,30: (* ANL and ORL *) 1540 1589 inversion addr 1541 1590 [1,3: … … 2228 2277 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) 2229 2278 ] 2230 | 42: (* PUSH *)2279 |*)42: (* PUSH *) 2231 2280 >EQP -P normalize nodelta lapply instr_refl 2232 2281 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.