Changeset 3075
 Timestamp:
 Apr 2, 2013, 7:59:07 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r3066 r3075 3 3 (* ===================================== *) 4 4 5 include "basics/russell.ma". 6 5 7 include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma".*) 6 8 include "ASM/Arithmetic.ma". 7 (*include "ASM/BitVectorTrie.ma".*)8 include "basics/russell.ma".9 9 10 10 definition Time ≝ nat. … … 251 251 qed. 252 252 253 lemma clock_set_8051_sfr: 254 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b. 255 clock … code_memory s = clock … code_memory (set_8051_sfr M code_memory s i b). 256 #M #code_memory #s #i #b // 257 qed. 258 253 259 definition set_8052_sfr ≝ 254 260 λM: Type[0]. … … 282 288 qed. 283 289 290 lemma clock_set_8052_sfr: 291 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b. 292 clock … code_memory s = clock … code_memory (set_8052_sfr M code_memory s i b). 293 #M #code_memory #s #i #b // 294 qed. 295 284 296 definition set_program_counter ≝ 285 297 λM: Type[0]. … … 355 367 old_clock. 356 368 369 definition update_low_internal_ram ≝ 370 λM: Type[0]. 371 λcode_memory:M. 372 λs: PreStatus M code_memory. 373 λaddr,v. 374 let old_low_internal_ram ≝ low_internal_ram ?? s in 375 let new_low_internal_ram ≝ insert ?? addr v old_low_internal_ram in 376 set_low_internal_ram … s new_low_internal_ram. 377 378 lemma clock_set_low_internal_ram: 379 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r. 380 clock … code_memory s = clock … code_memory (set_low_internal_ram M code_memory s r). 381 #M #code_memory #s #r // 382 qed. 383 384 lemma clock_update_low_internal_ram: 385 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v. 386 clock … code_memory s = clock … code_memory (update_low_internal_ram M code_memory s addr v). 387 #M #code_memory #s #addr #v // 388 qed. 389 357 390 definition set_high_internal_ram ≝ 358 391 λM: Type[0]. … … 380 413 old_clock. 381 414 415 definition update_high_internal_ram ≝ 416 λM: Type[0]. 417 λcode_memory:M. 418 λs: PreStatus M code_memory. 419 λaddr,v. 420 let old_high_internal_ram ≝ high_internal_ram ?? s in 421 let new_high_internal_ram ≝ insert ?? addr v old_high_internal_ram in 422 set_high_internal_ram … s new_high_internal_ram. 423 424 lemma clock_set_high_internal_ram: 425 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 7. 426 clock … code_memory s = clock … code_memory (set_high_internal_ram M code_memory s r). 427 #M #code_memory #s #r // 428 qed. 429 430 lemma clock_update_high_internal_ram: 431 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v. 432 clock … code_memory s = clock … code_memory (update_high_internal_ram M code_memory s addr v). 433 #M #code_memory #s #addr #v // 434 qed. 435 382 436 definition set_external_ram ≝ 383 437 λM: Type[0]. … … 404 458 old_clock. 405 459 460 definition update_external_ram ≝ 461 λM: Type[0]. 462 λcode_memory:M. 463 λs: PreStatus M code_memory. 464 λaddr,v. 465 let old_external_ram ≝ external_ram ?? s in 466 let new_external_ram ≝ insert ?? addr v old_external_ram in 467 set_external_ram … s new_external_ram. 468 469 lemma clock_set_external_ram: 470 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 16. 471 clock … code_memory s = clock … code_memory (set_external_ram M code_memory s r). 472 #M #code_memory #s #r // 473 qed. 474 475 lemma clock_update_external_ram: 476 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr: Word. ∀v: Byte. 477 clock … code_memory s = clock … code_memory (update_external_ram M code_memory s addr v). 478 #M #code_memory #s #addr #v // 479 qed. 480 481 definition get_psw_flags ≝ 482 λM: Type[0]. 483 λcode_memory:M. 484 λs: PreStatus M code_memory. 485 λflag. 486 λflag_ok: flag < ?. 487 let psw ≝ get_8051_sfr … s SFR_PSW in 488 get_index_v bool ? psw flag flag_ok. 489 406 490 definition get_cy_flag ≝ 407 491 λM: Type[0]. 408 492 λcode_memory:M. 409 493 λs: PreStatus M code_memory. 410 let sfr ≝ special_function_registers_8051 ?? s in 411 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 412 get_index_v bool 8 psw O ?. 413 normalize 414 @ (le_S_S ? ?) 415 [ @ le_O_n 416  repeat (@ (le_S_S)); 417 // 418 ] 494 get_psw_flags … s 0 ?. // 419 495 qed. 420 496 … … 423 499 λcode_memory:M. 424 500 λs: PreStatus M code_memory. 425 let sfr ≝ special_function_registers_8051 ?? s in 426 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 427 get_index_v bool 8 psw 1 ?. 428 normalize 429 repeat (@ (le_S_S ? ?)) 430 @ le_O_n 501 get_psw_flags … s 1 ?. // 431 502 qed. 432 503 … … 435 506 λcode_memory:M. 436 507 λs: PreStatus M code_memory. 437 let sfr ≝ special_function_registers_8051 ?? s in 438 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 439 get_index_v bool 8 psw 2 ?. 440 normalize 441 repeat (@ (le_S_S ? ?)) 442 @ le_O_n 508 get_psw_flags … s 2 ?. // 443 509 qed. 444 510 … … 447 513 λcode_memory:M. 448 514 λs: PreStatus M code_memory. 449 let sfr ≝ special_function_registers_8051 ?? s in 450 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 451 get_index_v bool 8 psw 3 ?. 452 normalize 453 repeat (@ (le_S_S ? ?)) 454 @ le_O_n 515 get_psw_flags … s 3 ?. // 455 516 qed. 456 517 … … 459 520 λcode_memory:M. 460 521 λs: PreStatus M code_memory. 461 let sfr ≝ special_function_registers_8051 ?? s in 462 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 463 get_index_v bool 8 psw 4 ?. 464 normalize 465 repeat (@ (le_S_S ? ?)) 466 @ le_O_n 522 get_psw_flags … s 4 ?. // 467 523 qed. 468 524 … … 471 527 λcode_memory:M. 472 528 λs: PreStatus M code_memory. 473 let sfr ≝ special_function_registers_8051 ?? s in 474 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 475 get_index_v bool 8 psw 5 ?. 476 normalize 477 repeat (@ (le_S_S ? ?)) 478 @ le_O_n 529 get_psw_flags … s 5 ?. // 479 530 qed. 480 531 … … 483 534 λcode_memory:M. 484 535 λs: PreStatus M code_memory. 485 let sfr ≝ special_function_registers_8051 ?? s in 486 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 487 get_index_v bool 8 psw 6 ?. 488 normalize 489 repeat (@ (le_S_S ? ?)) 490 @ le_O_n 536 get_psw_flags … s 6 ?. // 491 537 qed. 492 538 … … 495 541 λcode_memory:M. 496 542 λs: PreStatus M code_memory. 497 let sfr ≝ special_function_registers_8051 ?? s in 498 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 499 get_index_v bool 8 psw 7 ?. 500 normalize 501 repeat (@ (le_S_S ? ?)) 502 @ le_O_n 543 get_psw_flags … s 7 ?. // 503 544 qed. 504 545 … … 510 551 λac: option Bit. 511 552 λov: Bit. 512 let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in513 let old_cy ≝ get_ index_v ?? sfr_psw O ?in514 let old_ac ≝ get_ index_v ?? sfr_psw 1 ?in515 let old_fo ≝ get_ index_v ?? sfr_psw 2 ?in516 let old_rs1 ≝ get_ index_v ?? sfr_psw 3 ?in517 let old_rs0 ≝ get_ index_v ?? sfr_psw 4 ?in518 let old_ov ≝ get_ index_v ?? sfr_psw 5 ?in519 let old_ud ≝ get_ index_v ?? sfr_psw 6 ?in520 let old_p ≝ get_ index_v ?? sfr_psw 7 ?in553 (*let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in *) 554 let old_cy ≝ get_cy_flag ?? s (* get_index_v ?? sfr_psw O ?*) in 555 let old_ac ≝ get_ac_flag ?? s (* get_index_v ?? sfr_psw 1 ?*) in 556 let old_fo ≝ get_fo_flag ?? s (* get_index_v ?? sfr_psw 2 ?*) in 557 let old_rs1 ≝ get_rs1_flag ?? s (* get_index_v ?? sfr_psw 3 ?*) in 558 let old_rs0 ≝ get_rs0_flag ?? s (* get_index_v ?? sfr_psw 4 ?*) in 559 let old_ov ≝ get_ov_flag ?? s (* get_index_v ?? sfr_psw 5 ?*) in 560 let old_ud ≝ get_ud_flag ?? s (* get_index_v ?? sfr_psw 6 ?*) in 561 let old_p ≝ get_p_flag ?? s (* get_index_v ?? sfr_psw 7 ?*) in 521 562 let new_ac ≝ match ac with [ None ⇒ old_ac  Some j ⇒ j ] in 522 563 set_8051_sfr ?? s SFR_PSW 523 564 [[ cy ; new_ac ; old_fo ; old_rs1 ; 524 565 old_rs0 ; ov ; old_ud ; old_p ]]. 525 [1,2,3,4,5,6,7,8:526 normalize527 repeat (@ le_S_S)528 @ le_O_n529 ]530 qed.531 566 532 567 definition initialise_status ≝ 533 568 λM: Type[0]. 534 569 λcode_mem: M. 535 let status ≝ mk_PreStatus M code_mem 536 (Stub Byte 7) (* Low mem. *)537 (Stub Byte 7) (* High mem. *)538 (Stub Byte 16)(* Ext mem. *)539 (zero 16)(* PC. *)540 (replicate Byte 19 (zero 8))(* 8051 SFR. *)541 (replicate Byte 5 (zero 8))(* 8052 SFR. *)542 (zero 8)(* P1 latch. *)543 (zero 8)(* P3 latch. *)544 O 570 let status ≝ mk_PreStatus M code_mem (* Code mem. *) 571 (Stub …) (* Low mem. *) 572 (Stub …) (* High mem. *) 573 (Stub …) (* Ext mem. *) 574 (zero ?) (* PC. *) 575 (replicate … (zero ?)) (* 8051 SFR. *) 576 (replicate … (zero ?)) (* 8052 SFR. *) 577 (zero ?) (* P1 latch. *) 578 (zero ?) (* P3 latch. *) 579 O (* Clock. *) 545 580 in 546 set_8051_sfr ?? status SFR_SP (bitvector_of_nat 87).581 set_8051_sfr ?? status SFR_SP (bitvector_of_nat ? 7). 547 582 548 549 583 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 550 584 λb: Byte. … … 634 668 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 635 669 cases (sfr_of_Byte ?) 636 [1: 670 [1: 637 671 normalize nodelta cases not_implemented 638 2: 639 * * normalize nodelta%672 2: 673 * * % 640 674 ] 641 675 qed. … … 661 695 let c ≝ get_index_v … r 1 ? in 662 696 let d ≝ get_index_v … r 2 ? in 697 (* JHM: redundant bittwiddling, once you have get_*_flag helpers 663 698 let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 664 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 699 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 700 *) 701 let r1 ≝ get_rs1_flag ?? s in 702 let r0 ≝ get_rs0_flag ?? s in 665 703 let offset ≝ 666 704 if ¬r1 ∧ ¬r0 then … … 674 712 in 675 713 bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). 676 [1,2,3,4,5: 677 normalize 678 repeat (@ le_S_S) 679 @ le_O_n; 680 ] 714 // 681 715 qed. 682 716 … … 687 721 λr: BitVector 3. 688 722 let address ≝ bit_address_of_register … s r in 689 lookup ?? address (low_internal_ram … s) (zero 8).690 723 lookup ?? address (low_internal_ram … s) (zero ?). 724 691 725 definition set_register ≝ 692 726 λM: Type[0]. … … 696 730 λv: Byte. 697 731 let address ≝ bit_address_of_register … s r in 732 (* 698 733 let old_low_internal_ram ≝ low_internal_ram ?? s in 699 734 let new_low_internal_ram ≝ insert … address v old_low_internal_ram in 700 735 set_low_internal_ram … s new_low_internal_ram. 736 *) 737 update_low_internal_ram … s address v. 701 738 702 definition read_from_internal_ram ≝ 739 definition read_from_external_ram ≝ 740 λM: Type[0]. 741 λcode_memory:M. 742 λs: PreStatus M code_memory. 743 λaddr: Word. 744 lookup ?? addr (external_ram … s) (zero ?). 745 746 definition read_from_internal_ram ≝ (* JHM: lots of 7bits+HI/Lo vs. 8bit redundancy throughout *) 703 747 λM: Type[0]. 704 748 λcode_memory:M. … … 712 756 (low_internal_ram ?? s) 713 757 in 714 lookup … seven_bits memory (zero 8).758 lookup … seven_bits memory (zero ?). 715 759 716 760 definition read_at_stack_pointer ≝ … … 718 762 λcode_memory:M. 719 763 λs: PreStatus M code_memory. 720 read_from_internal_ram M code_memorys (get_8051_sfr ?? s SFR_SP).764 read_from_internal_ram … s (get_8051_sfr ?? s SFR_SP). 721 765 722 766 definition write_at_stack_pointer ≝ … … 726 770 λv: Byte. 727 771 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in 728 if head' … 0 bit_one then 772 if head' … bit_one then 773 (* 729 774 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 730 775 set_high_internal_ram ?? s memory 776 *) 777 update_high_internal_ram … s seven_bits v 731 778 else 779 (* 732 780 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 733 781 set_low_internal_ram ?? s memory. 782 *) 783 update_low_internal_ram … s seven_bits v. 734 784 735 785 definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝ … … 763 813  ACC_DPTR ⇒ λ_:True. 764 814 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 765 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in815 let big_acc ≝ (zero ?) @@ (get_8051_sfr … s SFR_ACC_A) in 766 816 add … big_acc dptr 767 817  _ ⇒ Ⓧ … … 784 834 λext_indirect_dptr: True. 785 835 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 786 lookup ? 16 address (external_ram ?? s) (zero 8)836 read_from_external_ram … s address 787 837  EXT_INDIRECT e ⇒ 788 838 λext_indirect: True. 789 839 let address ≝ get_register ?? s [[ false; false; e ]] in 790 let padded_address ≝ pad 8 8address in791 lookup ? 16 padded_address (external_ram ?? s) (zero 8)840 let padded_address ≝ pad 8 ? address in 841 read_from_external_ram … s padded_address 792 842  ACC_DPTR ⇒ 793 843 λacc_dptr: True. 794 844 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 795 let padded_acc ≝ pad 8 8(get_8051_sfr ?? s SFR_ACC_A) in845 let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in 796 846 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in 797 lookup ? 16 address (external_ram ?? s) (zero 8)847 read_from_external_ram … s address 798 848  ACC_PC ⇒ 799 849 λacc_pc: True. 800 let padded_acc ≝ pad 8 8(get_8051_sfr ?? s SFR_ACC_A) in850 let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in 801 851 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in 802 lookup ? 16 address (external_ram ?? s) (zero 8)803  DIRECT d ⇒ 852 read_from_external_ram … s address 853  DIRECT d ⇒ (* JHM: simplify false branch with read_from_internal_ram *) 804 854 λdirect: True. 805 855 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 806 856 match head' … hd with 807 857 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l 808  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 858 (* XXX: get_bit_addressable_sfr m cm s d l *) 859  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?) 860 (* XXX: read_from_internal_ram … s d *) 809 861 ] 810  INDIRECT i ⇒ 862  INDIRECT i ⇒ (* JHM: simplify completely with read_from_internal_ram *) 811 863 λindirect: True. 812 864 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in 813 865 match head' … hd with 814 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)815  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)866 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero ?) 867  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?) 816 868 ] 869 (* XXX: read_from_internal_ram … s (get_register … s [[false;false;i]]) *) 817 870  _ ⇒ λother. 818 871 match other in False with [ ] … … 828 881 PreStatus m cm 829 882 with 830 [ DIRECT d ⇒ 883 [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *) 831 884 λdirect: True. 832 885 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in 833 886 match head' … bit_one with 834 887 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v 835  false ⇒ 836 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in837 set_low_internal_ram ?? s memory 888  false ⇒ update_low_internal_ram … s seven_bits v 889 (*let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in 890 set_low_internal_ram ?? s memory*) 838 891 ] 839  INDIRECT i ⇒ 892  INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *) 840 893 λindirect: True. 841 894 let register ≝ get_register ?? s [[ false; false; i ]] in 842 895 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 843 896 match head' … bit_one with 844 [ false ⇒ 845 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in846 set_low_internal_ram ?? s memory 847  true ⇒ 848 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in849 set_high_internal_ram ?? s memory 897 [ false ⇒ update_low_internal_ram … s seven_bits v 898 (*let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 899 set_low_internal_ram ?? s memory*) 900  true ⇒ update_high_internal_ram … s seven_bits v 901 (*let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 902 set_high_internal_ram ?? s memory*) 850 903 ] 851 904  REGISTER r ⇒ λregister: True. set_register ?? s r v … … 856 909 let address ≝ get_register ?? s [[ false; false; e ]] in 857 910 let padded_address ≝ pad 8 8 address in 858 let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in 911 (* 912 let memory ≝ insert ?? padded_address v (external_ram ?? s) in 859 913 set_external_ram ?? s memory 914 *) 915 update_external_ram … s padded_address v 860 916  EXT_INDIRECT_DPTR ⇒ 861 917 λext_indirect_dptr: True. 862 918 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 863 let memory ≝ insert ? 16 address v (external_ram ?? s) in 919 (* 920 let memory ≝ insert ?? address v (external_ram ?? s) in 864 921 set_external_ram ?? s memory 922 *) 923 update_external_ram … s address v 865 924  _ ⇒ 866 925 λother: False. … … 868 927 ] (subaddressing_modein … a). 869 928 870 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 871 cases daemon 872 qed. 873 929 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v) ≝ 930 λm, cm, s, a, v. 931 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 932 acc_a ; acc_b ; ext_indirect ; 933 ext_indirect_dptr ]] x) → 934 clock … cm s = clock … cm (set_arg_8 … s x v) 935 with 936 [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *) 937 λdirect: True. 938 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in 939 match head' … bit_one with 940 [ true ⇒ ? 941  false ⇒ ? 942 ] 943  INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *) 944 λindirect: True. 945 let register ≝ get_register ?? s [[ false; false; i ]] in 946 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 947 match head' … bit_one with 948 [ false ⇒ ? 949  true ⇒ ? 950 ] 951  REGISTER r ⇒ λregister: True. ? 952  ACC_A ⇒ λacc_a: True. ? 953  ACC_B ⇒ λacc_b: True. ? 954  EXT_INDIRECT e ⇒ 955 λext_indirect: True. 956 let address ≝ get_register ?? s [[ false; false; e ]] in 957 let padded_address ≝ pad 8 8 address in 958 ? 959  EXT_INDIRECT_DPTR ⇒ 960 λext_indirect_dptr: True. 961 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 962 ? 963  _ ⇒ 964 λother: False. 965 match other in False with [ ] 966 ] (subaddressing_modein … a). 967 // 968 whd in match set_arg_8; normalize nodelta 969 (* XXX: nonRussell way 970 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 971 cases x * normalize nodelta 972 [1: #d #ok cases (vsplit ? 1 7 d) normalize nodelta 973 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta 974 [1: @clock_set_bit_addressable_sfr 975 2: @clock_update_low_internal_ram 976 ] 977 2: #i #ok cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta 978 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta 979 [1: @clock_update_high_internal_ram 980 2: @clock_update_low_internal_ram 981 ] 982 3: #b1 #ok @clock_update_external_ram 983 4: #b3 #ok @clock_update_low_internal_ram 984 5,6: #ok @clock_set_8051_sfr 985 12: #ok @clock_update_external_ram 986 ] 987 cases not_implemented (* JHM: there has to be a better way to deal with the absurd branches *) 988 *) 989 [1: (* case DIRECT d *) 990 cases (vsplit ? 1 7 d) normalize nodelta 991 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta // 992 2: (* case DIRECT d; why the repetition? *) 993 cases (vsplit ? 1 7 d) normalize nodelta 994 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta // 995 3: (* case INDIRECT i *) 996 cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta 997 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta // 998 4: (* case INDIRECT i; why the repetition? *) 999 cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta 1000 #bit_one #seven_bits cases (head' … bit_one) normalize nodelta // 1001 ] 1002 qed. 1003 1004 (* XXX: these  like those above  belong in StatusProofs*.ma ??? *) 874 1005 lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v). 1006 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 875 1007 cases daemon 876 1008 qed. … … 954 1086 λbit_addr: True. 955 1087 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 1088 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 956 1089 match head' … bit_1 with 957 1090 [ true ⇒ 958 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in959 1091 let trans ≝ true:::four_bits @@ [[false; false; false]] in 960 1092 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 961 1093 get_index_v … sfr (nat_of_bitvector … three_bits) ? 962 1094  false ⇒ 963 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in964 1095 let address' ≝ [[true; false; false]]@@four_bits in 965 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in1096 let t ≝ lookup ?? address' (low_internal_ram ?? s) (zero ?) in 966 1097 get_index_v … t (nat_of_bitvector … three_bits) ? 967 1098 ] … … 969 1100 λn_bit_addr: True. 970 1101 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in 1102 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 971 1103 match head' … bit_1 with 972 1104 [ true ⇒ 973 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in974 1105 let trans ≝ true:::four_bits @@ [[false; false; false]] in 975 1106 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 976 1107 ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?) 977 1108  false ⇒ 978 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in979 1109 let address' ≝ [[true; false; false]]@@four_bits in 980 1110 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in … … 997 1127 [ BIT_ADDR b ⇒ λbit_addr: True. 998 1128 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in 1129 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 999 1130 match head' … bit_1 with 1000 1131 [ true ⇒ 1001 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in1002 1132 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1003 1133 let sfr ≝ get_bit_addressable_sfr … s trans true in … … 1005 1135 set_bit_addressable_sfr … s new_sfr trans 1006 1136  false ⇒ 1007 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in1008 1137 let address' ≝ [[true; false; false]]@@four_bits in 1009 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in1138 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero ?) in 1010 1139 let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in 1011 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1140 (* 1141 let memory ≝ insert ?? address' n_bit (low_internal_ram ?? s) in 1012 1142 set_low_internal_ram … s memory 1143 *) 1144 update_low_internal_ram … s address' n_bit 1013 1145 ] 1014 1146  CARRY ⇒ … … 1025 1157 qed. 1026 1158 1027 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1028 cases daemon 1029 qed. 1159 (* JHM: Russellstyle works, modulo some oddities...??? *) 1160 lemma clock_set_arg_1: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v) 1161 ≝ 1162 λm: Type[0]. 1163 λcm. 1164 λs: PreStatus m cm. 1165 λa: [[bit_addr; carry]]. 1166 λv: Bit. 1167 match a 1168 return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → 1169 clock m cm s = clock … (set_arg_1 m cm s x v) 1170 with 1171 [ BIT_ADDR b ⇒ λbit_addr: True. 1172 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in 1173 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1174 match head' … bit_1 with 1175 [ true ⇒ 1176 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1177 let sfr ≝ get_bit_addressable_sfr … s trans true in 1178 let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in 1179 ? 1180  false ⇒ 1181 let address' ≝ [[true; false; false]]@@four_bits in 1182 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1183 let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in 1184 ? 1185 ] 1186  CARRY ⇒ 1187 λcarry: True. 1188 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1189 let new_psw ≝ v:::seven_bits in 1190 ? 1191  _ ⇒ 1192 λother: False. 1193 match other in False with 1194 [ ] 1195 ] (subaddressing_modein … a). // 1196 whd in match set_arg_1; normalize nodelta 1197 [1: (* case: CARRY *) 1198 cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW)) 1199 #ignore #seven_bits normalize nodelta @clock_set_8051_sfr 1200 2: (* case: BIT_ADDR *) 1201 cases (vsplit bool 1 7 b) 1202 #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits) 1203 #four_bits #three_bits normalize nodelta cases (head' … bit_1) 1204 [1: @clock_set_bit_addressable_sfr 1205 2: @clock_update_low_internal_ram 1206 ] 1207 3: (* case: BIT_ADDR, again; why? *) 1208 cases (vsplit bool 1 7 b) 1209 #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits) 1210 #four_bits #three_bits normalize nodelta cases (head' … bit_1) 1211 [1: @clock_set_bit_addressable_sfr 1212 2: @clock_update_low_internal_ram 1213 ] 1214 ] 1215 qed. 1216 1217 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1218 (* JHM: boring, nonRussell way 1219 #m #cm #s #x #v whd in match set_arg_1; 1220 cases x * normalize nodelta 1221 [14: #ok cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW)) 1222 #ignore #seven_bits @clock_set_8051_sfr 1223 15: #b #ok cases (vsplit bool 1 7 b) 1224 #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits) 1225 #four_bits #three_bits normalize nodelta cases (head' … bit_1) 1226 [1: @clock_set_bit_addressable_sfr 1227 2: @clock_set_low_internal_ram 1228 ] 1229 ] cases not_implemented (* XXX: there has to be a better way to deal with the absurd branches *) 1230 *) 1231 @clock_set_arg_1 1232 qed. 1233 1030 1234 1031 1235 definition construct_datalabels: list (Identifier × Word) → 1032 1236 identifier_map ASMTag Word ≝ 1033 1237 λthe_preamble. 1034 \fst (foldl ((identifier_map ASMTag Word) × Word)? (λt,preamble.1238 \fst (foldl ?? (λt,preamble. 1035 1239 let 〈datalabels, addr〉 ≝ t in 1036 1240 let 〈name, size〉 ≝ preamble in
Note: See TracChangeset
for help on using the changeset viewer.