Changeset 2165
- Timestamp:
- Jul 7, 2012, 3:23:57 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2164 r2165 467 467 qed. 468 468 469 lemma external_ram_status_of_pseudo_status: 470 ∀M,cm,s,sigma,policy. 471 external_ram … 472 (code_memory_of_pseudo_assembly_program cm sigma policy) 473 (status_of_pseudo_status M cm s sigma policy) = 474 external_ram … cm s. 475 // 476 qed. 477 478 lemma set_external_ram_status_of_pseudo_status: 479 ∀M,cm,ps,sigma,policy,ram. 480 set_external_ram … 481 (code_memory_of_pseudo_assembly_program cm sigma policy) 482 (status_of_pseudo_status M cm ps sigma policy) 483 ram = 484 status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy. 485 // 486 qed. 487 469 488 definition map_address_mode_using_internal_pseudo_address_map_ok ≝ 470 489 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'. … … 482 501 let register ≝ get_register ?? s [[ false; false; i ]] in 483 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' 484 507 | _ ⇒ v = v']. 485 508 … … 624 647 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 625 648 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta 626 [ 649 [ cases daemon (*CSC*) 627 650 | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2 628 651 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ] 629 qed. 652 |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status 653 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 654 >EQ1 normalize nodelta 655 >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_status 660 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] 661 qed.
Note: See TracChangeset
for help on using the changeset viewer.