Changeset 1526 for src/ASM/Status.ma
 Timestamp:
 Nov 22, 2011, 10:43:47 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1522 r1526 6 6 include "ASM/Arithmetic.ma". 7 7 include "ASM/BitVectorTrie.ma". 8 include "ASM/JMCoercions.ma". 8 9 9 10 definition Time ≝ nat. … … 853 854 qed. 854 855 855 definition set_arg_8: ∀M: Type[0]. PreStatus M → [[ direct ; indirect ; registr ; 856 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v). 857 858 definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; 856 859 acc_a ; acc_b ; ext_indirect ; 857 ext_indirect_dptr ]] → Byte → PreStatus M ≝ 860 ext_indirect_dptr ]] → Byte → Σs':PreStatus M. 861 clock … s = clock … s' ≝ 858 862 λm, s, a, v. 859 863 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 860 864 acc_a ; acc_b ; ext_indirect ; 861 ext_indirect_dptr ]] x) → ? with 865 ext_indirect_dptr ]] x) → 866 Σs':PreStatus m. ?(*clock … s*) = ?(*clock … s'*) 867 (*CSC: bug here if one specified the two clock above*) 868 with 862 869 [ DIRECT d ⇒ 863 870 λdirect: True. … … 899 906 let memory ≝ insert ? 16 address v (external_ram ? s) in 900 907 set_external_ram ? s memory 901  _ ⇒ 908  _ ⇒ 902 909 λother: False. 903 910 match other in False with [ ] 904 911 ] (subaddressing_modein … a). 905 [1,2,3,4: 906 normalize 907 repeat (@ le_S_S) 908 @ le_O_n 909 ] 910 qed. 912 // qed. 911 913 912 914 theorem modulus_less_than: … … 1024 1026 [ BIT_ADDR b ⇒ λbit_addr: True. 1025 1027 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1026 let bit_1 ≝ get_index_v …nu 0 ? in1028 let bit_1 ≝ get_index_v ?? nu 0 ? in 1027 1029 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 1028 1030 match bit_1 with
Note: See TracChangeset
for help on using the changeset viewer.