Changeset 1588 for src/ASM/Status.ma
 Timestamp:
 Dec 6, 2011, 11:21:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1581 r1588 762 762 qed. 763 763 764 definition set_arg_16 : ∀M: Type[0]. PreStatus M → Word → [[ dptr ]] → PreStatus M≝764 definition set_arg_16': ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → Σs':PreStatus M. clock … s = clock … s' ≝ 765 765 λM. 766 766 λs. 767 767 λv. 768 768 λa. 769 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ?with769 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M s = clock M s' with 770 770 [ DPTR ⇒ λ_:True. 771 771 let 〈 bu, bl 〉 ≝ split … 8 8 v in … … 778 778 ] 779 779 ] (subaddressing_modein … a). 780 // 781 qed. 782 783 definition set_arg_16: ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → PreStatus M ≝ 784 set_arg_16'. 785 786 lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x). 787 #M #s #x #v whd in match set_arg_16; normalize nodelta @sig2 788 qed. 789 780 790 781 791 definition get_arg_16: ∀M: Type[0]. PreStatus M → [[ data16 ]] → Word ≝ … … 856 866 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v). 857 867 858 definition set_arg_8 : ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ;868 definition set_arg_8': ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; 859 869 acc_a ; acc_b ; ext_indirect ; 860 870 ext_indirect_dptr ]] → Byte → Σs':PreStatus M. … … 911 921 ] (subaddressing_modein … a). 912 922 // qed. 923 924 definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M ≝ 925 set_arg_8'. 926 927 lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v). 928 #M #s #x #v whd in match set_arg_8; normalize nodelta @sig2 929 qed. 913 930 914 931 theorem modulus_less_than: … … 1020 1037 qed. 1021 1038 1022 (* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn 1023 pointer assertion failure in nCicMetaSubst.ml, line 293. *) 1024 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝ 1039 definition set_arg_1': ∀M: Type[0]. ∀s:PreStatus M. [[bit_addr; carry]] → Bit → Σs':PreStatus M. clock … s = clock … s' ≝ 1025 1040 λm: Type[0]. 1026 1041 λs: PreStatus m. 1027 1042 λa: [[bit_addr; carry]]. 1028 1043 λv: Bit. 1029 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ?with1044 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m s = clock m s' with 1030 1045 [ BIT_ADDR b ⇒ λbit_addr: True. 1031 1046 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in … … 1062 1077 [ ] 1063 1078 ] (subaddressing_modein … a). 1064 [1,2,3,6: 1065 normalize 1066 repeat (@ le_S_S) 1067 @ le_O_n 1068 4,5: 1069 @ modulus_less_than 1070 ] 1079 try (repeat @le_S_S @le_O_n) 1080 /by/ 1081 qed. 1082 1083 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝ set_arg_1'. 1084 1085 lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v). 1086 #M #s #x #v whd in match set_arg_1; normalize nodelta @sig2 1071 1087 qed. 1072 1088
Note: See TracChangeset
for help on using the changeset viewer.