Changeset 2172 for src/ASM/Status.ma
 Timestamp:
 Jul 10, 2012, 2:39:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r2160 r2172 546 546 set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7). 547 547 548 definition get_bit_addressable_sfr ≝ 549 λM: Type[0]. 550 λcode_memory:M. 551 λs: PreStatus M code_memory. 552 λn: nat. 553 λb: BitVector n. 548 549 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 550 λb: Byte. 551 let address ≝ nat_of_bitvector … b in 552 if (eqb address 128) then None ? 553 else if (eqb address 144) then Some … (inl … SFR_P1) 554 else if (eqb address 160) then None ? 555 else if (eqb address 176) then Some … (inl … SFR_P3) 556 else if (eqb address 153) then Some … (inl … SFR_SBUF) 557 else if (eqb address 138) then Some … (inl … SFR_TL0) 558 else if (eqb address 139) then Some … (inl … SFR_TL1) 559 else if (eqb address 140) then Some … (inl … SFR_TH0) 560 else if (eqb address 141) then Some … (inl … SFR_TH1) 561 else if (eqb address 200) then Some … (inr … SFR_T2CON) 562 else if (eqb address 202) then Some … (inr … SFR_RCAP2L) 563 else if (eqb address 203) then Some … (inr … SFR_RCAP2H) 564 else if (eqb address 204) then Some … (inr … SFR_TL2) 565 else if (eqb address 205) then Some … (inr … SFR_TH2) 566 else if (eqb address 135) then Some … (inl … SFR_PCON) 567 else if (eqb address 136) then Some … (inl … SFR_TCON) 568 else if (eqb address 137) then Some … (inl … SFR_TMOD) 569 else if (eqb address 152) then Some … (inl … SFR_SCON) 570 else if (eqb address 168) then Some … (inl … SFR_IE) 571 else if (eqb address 184) then Some … (inl … SFR_IP) 572 else if (eqb address 129) then Some … (inl … SFR_SP) 573 else if (eqb address 130) then Some … (inl … SFR_DPL) 574 else if (eqb address 131) then Some … (inl … SFR_DPH) 575 else if (eqb address 208) then Some … (inl … SFR_PSW) 576 else if (eqb address 224) then Some … (inl … SFR_ACC_A) 577 else if (eqb address 240) then Some … (inl … SFR_ACC_B) 578 else None ?. 579 580 definition get_bit_addressable_sfr: 581 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝ 582 λM: Type[0]. 583 λcode_memory:M. 584 λs: PreStatus M code_memory. 585 λb: Byte. 554 586 λl: bool. 555 let address ≝ nat_of_bitvector … b in 556 if (eqb address 128) then 557 ? 558 else if (eqb address 144) then 587 match sfr_of_Byte b with 588 [ None ⇒ match not_implemented in False with [ ] 589  Some sfr8051_8052 ⇒ 590 match sfr8051_8052 with 591 [ inl sfr ⇒ 592 match sfr with 593 [ SFR_P1 ⇒ 559 594 if l then 560 (p1_latch ?? s)595 p1_latch … s 561 596 else 562 (get_8051_sfr ?? s SFR_P1) 563 else if (eqb address 160) then 564 ? 565 else if (eqb address 176) then 597 get_8051_sfr … s SFR_P1 598  SFR_P3 ⇒ 566 599 if l then 567 (p3_latch ?? s)600 p3_latch … s 568 601 else 569 (get_8051_sfr ?? s SFR_P3) 570 else if (eqb address 153) then 571 get_8051_sfr ?? s SFR_SBUF 572 else if (eqb address 138) then 573 get_8051_sfr ?? s SFR_TL0 574 else if (eqb address 139) then 575 get_8051_sfr ?? s SFR_TL1 576 else if (eqb address 140) then 577 get_8051_sfr ?? s SFR_TH0 578 else if (eqb address 141) then 579 get_8051_sfr ?? s SFR_TH1 580 else if (eqb address 200) then 581 get_8052_sfr ?? s SFR_T2CON 582 else if (eqb address 202) then 583 get_8052_sfr ?? s SFR_RCAP2L 584 else if (eqb address 203) then 585 get_8052_sfr ?? s SFR_RCAP2H 586 else if (eqb address 204) then 587 get_8052_sfr ?? s SFR_TL2 588 else if (eqb address 205) then 589 get_8052_sfr ?? s SFR_TH2 590 else if (eqb address 135) then 591 get_8051_sfr ?? s SFR_PCON 592 else if (eqb address 136) then 593 get_8051_sfr ?? s SFR_TCON 594 else if (eqb address 137) then 595 get_8051_sfr ?? s SFR_TMOD 596 else if (eqb address 152) then 597 get_8051_sfr ?? s SFR_SCON 598 else if (eqb address 168) then 599 get_8051_sfr ?? s SFR_IE 600 else if (eqb address 184) then 601 get_8051_sfr ?? s SFR_IP 602 else if (eqb address 129) then 603 get_8051_sfr ?? s SFR_SP 604 else if (eqb address 130) then 605 get_8051_sfr ?? s SFR_DPL 606 else if (eqb address 131) then 607 get_8051_sfr ?? s SFR_DPH 608 else if (eqb address 208) then 609 get_8051_sfr ?? s SFR_PSW 610 else if (eqb address 224) then 611 get_8051_sfr ?? s SFR_ACC_A 612 else if (eqb address 240) then 613 get_8051_sfr ?? s SFR_ACC_B 614 else 615 ?. 616 cases not_implemented 617 qed. 618 619 definition set_bit_addressable_sfr': 620 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 621 Σs':PreStatus M code_memory. 622 clock … code_memory s = clock … code_memory s' ∧ 623 program_counter … code_memory s = program_counter … code_memory s' ≝ 602 get_8051_sfr … s SFR_P3 603  _ ⇒ get_8051_sfr … s sfr 604 ] 605  inr sfr ⇒ get_8052_sfr M code_memory s sfr 606 ] 607 ]. 608 609 definition set_bit_addressable_sfr: 610 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝ 624 611 λM: Type[0]. 625 612 λcode_memory:M. … … 627 614 λb: Byte. 628 615 λv: Byte. 629 let address ≝ nat_of_bitvector … b in 630 if (eqb address 128) then 631 match not_implemented in False with [ ] 632 else if (eqb address 144) then 633 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 634 let status_2 ≝ set_p1_latch ?? s v in 635 status_2 636 else if (eqb address 160) then 637 match not_implemented in False with [ ] 638 else if (eqb address 176) then 639 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 640 let status_2 ≝ set_p3_latch ?? s v in 641 status_2 642 else if (eqb address 153) then 643 set_8051_sfr ?? s SFR_SBUF v 644 else if (eqb address 138) then 645 set_8051_sfr ?? s SFR_TL0 v 646 else if (eqb address 139) then 647 set_8051_sfr ?? s SFR_TL1 v 648 else if (eqb address 140) then 649 set_8051_sfr ?? s SFR_TH0 v 650 else if (eqb address 141) then 651 set_8051_sfr ?? s SFR_TH1 v 652 else if (eqb address 200) then 653 set_8052_sfr ?? s SFR_T2CON v 654 else if (eqb address 202) then 655 set_8052_sfr ?? s SFR_RCAP2L v 656 else if (eqb address 203) then 657 set_8052_sfr ?? s SFR_RCAP2H v 658 else if (eqb address 204) then 659 set_8052_sfr ?? s SFR_TL2 v 660 else if (eqb address 205) then 661 set_8052_sfr ?? s SFR_TH2 v 662 else if (eqb address 135) then 663 set_8051_sfr ?? s SFR_PCON v 664 else if (eqb address 136) then 665 set_8051_sfr ?? s SFR_TCON v 666 else if (eqb address 137) then 667 set_8051_sfr ?? s SFR_TMOD v 668 else if (eqb address 152) then 669 set_8051_sfr ?? s SFR_SCON v 670 else if (eqb address 168) then 671 set_8051_sfr ?? s SFR_IE v 672 else if (eqb address 184) then 673 set_8051_sfr ?? s SFR_IP v 674 else if (eqb address 129) then 675 set_8051_sfr ?? s SFR_SP v 676 else if (eqb address 130) then 677 set_8051_sfr ?? s SFR_DPL v 678 else if (eqb address 131) then 679 set_8051_sfr ?? s SFR_DPH v 680 else if (eqb address 208) then 681 set_8051_sfr ?? s SFR_PSW v 682 else if (eqb address 224) then 683 set_8051_sfr ?? s SFR_ACC_A v 684 else if (eqb address 240) then 685 set_8051_sfr ?? s SFR_ACC_B v 686 else 687 match not_implemented in False with [ ]. 688 /2 by refl, pair_destruct/ 689 qed. 690 691 definition set_bit_addressable_sfr: 692 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 693 PreStatus M code_memory ≝ set_bit_addressable_sfr'. 616 match sfr_of_Byte b with 617 [ None ⇒ match not_implemented in False with [ ] 618  Some sfr8051_8052 ⇒ 619 match sfr8051_8052 with 620 [ inl sfr ⇒ 621 match sfr with 622 [ SFR_P1 ⇒ 623 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 624 set_p1_latch ?? s v 625  SFR_P3 ⇒ 626 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 627 set_p3_latch ?? s v 628  _ ⇒ set_8051_sfr ?? s sfr v ] 629  inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. 694 630 695 631 lemma clock_set_bit_addressable_sfr: … … 697 633 clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v). 698 634 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 699 cases (set_bit_addressable_sfr' ?????) #s' * // 635 cases (sfr_of_Byte ?) 636 [1: 637 normalize nodelta cases not_implemented 638 2: 639 * * normalize nodelta % 640 ] 700 641 qed. 701 642 … … 704 645 program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v). 705 646 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 706 cases (set_bit_addressable_sfr' ?????) #s' * // 647 cases (sfr_of_Byte ?) 648 [1: 649 normalize nodelta cases not_implemented 650 2: 651 * * % 652 ] 707 653 qed. 708 654 … … 863 809 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 864 810 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 865 let 〈 carry, address〉 ≝ half_add 16 dptr padded_acc in811 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in 866 812 lookup ? 16 address (external_ram ?? s) (zero 8) 867 813  ACC_PC ⇒ … … 872 818  DIRECT d ⇒ 873 819 λdirect: True. 874 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in 875 let bit_one ≝ get_index_v ? ? nu 0 ? in 876 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 877 match bit_one with 878 [ false ⇒ 879 let address ≝ three_bits @@ nl in 880 lookup ? 7 address (low_internal_ram ?? s) (zero 8) 881  true ⇒ get_bit_addressable_sfr ?? s 8 d l 882 ] 820 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 821 match head' … hd with 822 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l 823  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 824 ] 883 825  INDIRECT i ⇒ 884 826 λindirect: True. 885 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in 886 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 887 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 888 match bit_1 with 889 [ false ⇒ 890 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8) 891  true ⇒ 892 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8) 827 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in 828 match head' … hd with 829 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) 830  false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 893 831 ] 894 832  _ ⇒ λother. 895 833 match other in False with [ ] 896 834 ] (subaddressing_modein … a). 897 [1,2: 898 normalize 899 repeat (@ le_S_S) 900 @ le_O_n 901 ] 902 qed. 903 904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 835 836 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 905 837 acc_a ; acc_b ; ext_indirect ; 906 ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory. 907 clock … code_memory s = clock … code_memory s' ∧ 908 (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧ 909 (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧ 910 program_counter … code_memory s = program_counter … code_memory s' ∧ 911 (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝ 838 ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝ 912 839 λm, cm, s, a, v. 913 840 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 914 841 acc_a ; acc_b ; ext_indirect ; 915 842 ext_indirect_dptr ]] x) → 916 Σs':PreStatus m cm. ? 917 (*CSC: bug here if one specified the two clock above*) 843 PreStatus m cm 918 844 with 919 845 [ DIRECT d ⇒ 920 846 λdirect: True. 921 let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in 922 let bit_one ≝ get_index_v ? ? nu 0 ? in 923 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 924 match bit_one with 925 [ true ⇒ set_bit_addressable_sfr ?? s d v 847 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in 848 match head' … bit_one with 849 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v 926 850  false ⇒ 927 let memory ≝ insert ? 7 (three_bits @@ nl)v (low_internal_ram ?? s) in851 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in 928 852 set_low_internal_ram ?? s memory 929 853 ] … … 931 855 λindirect: True. 932 856 let register ≝ get_register ?? s [[ false; false; i ]] in 933 let 〈nu, nl〉 ≝ vsplit ? 4 4 register in 934 let bit_1 ≝ get_index_v … nu 0 ? in 935 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 936 match bit_1 with 857 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 858 match head' … bit_one with 937 859 [ false ⇒ 938 let memory ≝ insert … (three_bits @@ nl)v (low_internal_ram ?? s) in860 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 939 861 set_low_internal_ram ?? s memory 940 862  true ⇒ 941 let memory ≝ insert … (three_bits @@ nl)v (high_internal_ram ?? s) in863 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 942 864 set_high_internal_ram ?? s memory 943 865 ] … … 960 882 match other in False with [ ] 961 883 ] (subaddressing_modein … a). 962 /6 by conj, False_ind/963 qed.964 965 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝966 set_arg_8'.967 884 968 885 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 969 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 970 cases (set_arg_8' ?????) #s' * * * * // 886 cases daemon 971 887 qed. 972 888 973 889 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). 974 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 975 cases (set_arg_8' ?????) #s' * * * * // 890 cases daemon 976 891 qed. 977 892 … … 979 894 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 980 895 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 981 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 982 * * * * #_ #relevant #_ #_ #_ @relevant @I 896 cases daemon 983 897 qed. 984 898 … … 986 900 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 987 901 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 988 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 989 * * * * #_ #_ #relevant #_ #_ @relevant @I 902 cases daemon 990 903 qed. 991 904 … … 993 906 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 994 907 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 995 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 996 * * * * #_ #_ #_ #_ #relevant @relevant @I 908 cases daemon 997 909 qed. 998 910 … … 1056 968 [ BIT_ADDR b ⇒ 1057 969 λbit_addr: True. 1058 let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in 1059 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1060 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1061 match bit_1 with 1062 [ true ⇒ 1063 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1064 let d ≝ address ÷ 8 in 1065 let m ≝ address mod 8 in 1066 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1067 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1068 get_index_v … sfr m ? 1069  false ⇒ 1070 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1071 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1072 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1073 get_index_v … t (modulus address 8) ? 1074 ] 970 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 971 match head' … bit_1 with 972 [ true ⇒ 973 let address ≝ nat_of_bitvector … seven_bits in 974 let d ≝ address ÷ 8 in 975 let m ≝ address mod 8 in 976 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 977 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 978 get_index_v … sfr m ? 979  false ⇒ 980 let address ≝ nat_of_bitvector … seven_bits in 981 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 982 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 983 get_index_v … t (modulus address 8) ? 984 ] 1075 985  N_BIT_ADDR n ⇒ 1076 986 λn_bit_addr: True. 1077 let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in 1078 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1079 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1080 match bit_1 with 1081 [ true ⇒ 1082 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1083 let d ≝ address ÷ 8 in 1084 let m ≝ address mod 8 in 1085 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1086 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1087 ¬(get_index_v … sfr m ?) 1088  false ⇒ 1089 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1090 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1091 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1092 ¬(get_index_v … trans (modulus address 8) ?) 1093 ] 987 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in 988 match head' … bit_1 with 989 [ true ⇒ 990 let address ≝ nat_of_bitvector … seven_bits in 991 let d ≝ address ÷ 8 in 992 let m ≝ address mod 8 in 993 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 994 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 995 ¬(get_index_v … sfr m ?) 996  false ⇒ 997 let address ≝ nat_of_bitvector … seven_bits in 998 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 999 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1000 ¬(get_index_v … t (modulus address 8) ?) 1001 ] 1094 1002  CARRY ⇒ λcarry: True. get_cy_flag ?? s 1095 1003  _ ⇒ λother. 1096 1004 match other in False with [ ] 1097 1005 ] (subaddressing_modein … a). 1098 [3,6: 1099 normalize 1100 repeat (@ le_S_S) 1101 @ le_O_n 1102 1,2,4,5: 1103 @modulus_less_than 1104 ] 1006 @modulus_less_than 1105 1007 qed. 1106 1008 1107 definition set_arg_1 ': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s'≝1009 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ 1108 1010 λm: Type[0]. 1109 1011 λcm. … … 1111 1013 λa: [[bit_addr; carry]]. 1112 1014 λv: Bit. 1113 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s'with1015 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with 1114 1016 [ BIT_ADDR b ⇒ λbit_addr: True. 1115 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1116 let bit_1 ≝ get_index_v ?? nu 0 ? in 1117 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 1118 match bit_1 return λ_. ? with 1119 [ true ⇒ 1120 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1121 let d ≝ address ÷ 8 in 1122 let m ≝ address mod 8 in 1123 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1124 let sfr ≝ get_bit_addressable_sfr ?? s ? t true in 1125 let new_sfr ≝ set_index … sfr m v ? in 1126 set_bit_addressable_sfr ?? s new_sfr t 1127  false ⇒ 1128 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1129 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1130 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1131 let n_bit ≝ set_index … t (modulus address 8) v ? in 1132 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1133 set_low_internal_ram ?? s memory 1134 ] 1017 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1018 match head' … bit_1 with 1019 [ true ⇒ 1020 let address ≝ nat_of_bitvector … seven_bits in 1021 let d ≝ address ÷ 8 in 1022 let m ≝ address mod 8 in 1023 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1024 let sfr ≝ get_bit_addressable_sfr … s t true in 1025 let new_sfr ≝ set_index … sfr m v ? in 1026 set_bit_addressable_sfr … s new_sfr t 1027  false ⇒ 1028 let address ≝ nat_of_bitvector … seven_bits in 1029 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1030 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1031 let n_bit ≝ set_index … t (modulus address 8) v ? in 1032 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1033 set_low_internal_ram … s memory 1034 ] 1135 1035  CARRY ⇒ 1136 1036 λcarry: True. 1137 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1138 let bit_1 ≝ get_index_v… nu 1 ? in 1139 let bit_2 ≝ get_index_v… nu 2 ? in 1140 let bit_3 ≝ get_index_v… nu 3 ? in 1141 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1037 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1038 let new_psw ≝ v:::seven_bits in 1142 1039 set_8051_sfr ?? s SFR_PSW new_psw 1143 1040  _ ⇒ … … 1146 1043 [ ] 1147 1044 ] (subaddressing_modein … a). 1148 try (repeat @le_S_S @le_O_n) 1149 /by/ 1150 qed. 1151 1152 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'. 1045 @modulus_less_than 1046 qed. 1153 1047 1154 1048 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1155 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi21049 cases daemon 1156 1050 qed. 1157 1051
Note: See TracChangeset
for help on using the changeset viewer.