Changeset 2160 for src/ASM/Status.ma
 Timestamp:
 Jul 6, 2012, 5:26:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r2139 r2160 617 617 qed. 618 618 619 definition set_bit_addressable_sfr ≝ 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' ≝ 620 624 λM: Type[0]. 621 625 λcode_memory:M. … … 625 629 let address ≝ nat_of_bitvector … b in 626 630 if (eqb address 128) then 627 ?631 match not_implemented in False with [ ] 628 632 else if (eqb address 144) then 629 633 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in … … 631 635 status_2 632 636 else if (eqb address 160) then 633 ?637 match not_implemented in False with [ ] 634 638 else if (eqb address 176) then 635 639 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in … … 681 685 set_8051_sfr ?? s SFR_ACC_B v 682 686 else 683 ?. 684 cases not_implemented 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'. 694 695 lemma clock_set_bit_addressable_sfr: 696 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte. 697 clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v). 698 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 699 cases (set_bit_addressable_sfr' ?????) #s' * // 700 qed. 701 702 lemma program_counter_set_bit_addressable_sfr: 703 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte. 704 program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v). 705 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 706 cases (set_bit_addressable_sfr' ?????) #s' * // 685 707 qed. 686 708 … … 880 902 qed. 881 903 882 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v). 883 884 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; 904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 885 905 acc_a ; acc_b ; ext_indirect ; 886 ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory. 887 clock … code_memory s = clock … code_memory s' ≝ 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') ≝ 888 912 λm, cm, s, a, v. 889 913 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 890 914 acc_a ; acc_b ; ext_indirect ; 891 915 ext_indirect_dptr ]] x) → 892 Σs':PreStatus m cm. clock m cm s = clock m cm s'916 Σs':PreStatus m cm. ? 893 917 (*CSC: bug here if one specified the two clock above*) 894 918 with … … 936 960 match other in False with [ ] 937 961 ] (subaddressing_modein … a). 938 // qed. 962 /6 by conj, False_ind/ 963 qed. 939 964 940 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 ≝ 941 966 set_arg_8'. 942 967 943 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 944 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2 968 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' * * * * // 971 qed. 972 973 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' * * * * // 976 qed. 977 978 lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v). 979 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 980 #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 983 qed. 984 985 lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v). 986 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 987 #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 990 qed. 991 992 lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v). 993 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 994 #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 945 997 qed. 946 998
Note: See TracChangeset
for help on using the changeset viewer.