- Timestamp:
- Jul 8, 2012, 3:59:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2165 r2166 486 486 qed. 487 487 488 definition map_address_mode_using_internal_pseudo_address_map_ok ≝ 489 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'. 488 definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ 489 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr. 490 match addr with 491 [ INDIRECT i ⇒ 492 assoc_list_lookup ?? 493 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … 494 | EXT_INDIRECT e ⇒ 495 assoc_list_lookup ?? 496 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … 497 | _ ⇒ True ]. 498 499 definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝ 500 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v. 490 501 match addr with 491 502 [ DIRECT d ⇒ … … 495 506 map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v 496 507 | false ⇒ 497 map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v'508 map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] 498 509 | INDIRECT i ⇒ 499 assoc_list_lookup ??500 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧501 510 let register ≝ get_register ?? s [[ false; false; i ]] in 502 map_internal_ram_address_using_pseudo_address_map M sigma register v = v' 503 | EXT_INDIRECT e ⇒ 504 assoc_list_lookup ?? 505 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧ 506 v = v' 507 | _ ⇒ v = v']. 511 map_internal_ram_address_using_pseudo_address_map M sigma register v 512 | ACC_A ⇒ 513 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v 514 | _ ⇒ v ]. 508 515 509 516 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; … … 584 591 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 585 592 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. 586 map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' → 593 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr → 594 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → 587 595 set_arg_8 (BitVectorTrie Byte 16) 588 596 (code_memory_of_pseudo_assembly_program cm sigma policy) … … 638 646 match other in False with [ ] 639 647 ] (subaddressing_modein … a)) normalize nodelta 640 #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta 648 #M #sigma #policy #v' 649 whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta 650 whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta 641 651 [1,2: 642 652 <vsplit_refl normalize nodelta >p normalize nodelta 643 [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status644 | # v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]645 |3,4: *#EQ1 #EQ2 change with (get_register ????) in match register in p;653 [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status 654 | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 655 |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; 646 656 >get_register_status_of_pseudo_status 647 657 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta … … 650 660 | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2 651 661 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ] 652 |5: *#EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status662 |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status 653 663 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 654 664 >EQ1 normalize nodelta 655 665 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status 656 |6: # EQ <EQ cases daemon (*CSC*)657 |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*)658 |8: # EQ <EQ @set_8051_sfr_status_of_pseudo_status %659 |9: # EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status666 |6: #_ #EQ <EQ cases daemon (*CSC*) 667 |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/ 668 |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status % 669 |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status 660 670 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] 661 671 qed.
Note: See TracChangeset
for help on using the changeset viewer.