- Timestamp:
- Jun 10, 2011, 1:15:11 PM (10 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r934 r935 1844 1844 qed. 1845 1845 1846 lemma set_arg_8_set_program_counter: 1847 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) → 1848 ∀T,s.∀pc:Word.∀b:l. 1849 set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b. 1850 [2,3: cases b; *; normalize //] 1851 #n #l #prf #T #s #pc #b * *; 1852 qed. 1853 1846 1854 lemma get_arg_8_set_code_memory: 1847 1855 ∀T1,T2,s,code_mem,b,arg. … … 1854 1862 set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem = 1855 1863 set_flags … (set_code_memory … s code_mem) f1 f2 f3. 1856 #T1 #T2 #s #f1 #f2 #f3 #code_mem whd in ⊢ (??(???%?)%) 1857 cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl % 1864 #T1 #T2 #s #f1 #f2 #f3 #code_mem % 1858 1865 qed. 1859 1866 … … 1862 1869 set_program_counter T1 (set_flags T1 s f1 f2 f3) pc = 1863 1870 set_flags … (set_program_counter … s pc) f1 f2 f3. 1864 #T1 #s #f1 #f2 #f3 #pc whd in ⊢ (??(??%?)%) 1865 cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl % 1871 #T1 #s #f1 #f2 #f3 #pc % 1866 1872 qed. 1867 1873 … … 1869 1875 ∀T1,s,f1,f2,f3. 1870 1876 program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s. 1871 #T1 #s #f1 #f2 #f3 whd in ⊢ (??(??%)?) cases (split ????) #nu #nl%1877 #T1 #s #f1 #f2 #f3 % 1872 1878 qed. 1873 1879 1874 1880 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps. 1881 1882 lemma eq_rect_Type1_r: 1883 ∀A: Type[1]. 1884 ∀a:A. 1885 ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 1886 #A #a #P #H #x #p 1887 generalize in match H 1888 generalize in match P 1889 cases p 1890 // 1891 qed. 1875 1892 1876 1893 lemma main_thm: … … 1935 1952 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 1936 1953 #result #flags 1937 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; 1938 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1954 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; % 1939 1955 | (* INC *) #arg1 #H1 #H2 #EQ %[@1] 1940 1956 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) … … 1952 1968 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; 1953 1969 [5: % 1954 | 1970 |1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1955 1971 1956 1972 XXX 1957 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags%1973 % 1958 1974 -
src/ASM/Status.ma
r911 r935 498 498 λac: option Bit. 499 499 λov: Bit. 500 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in 501 let old_cy ≝ get_index_v… nu O ? in 502 let old_ac ≝ get_index_v… nu 1 ? in 503 let old_fo ≝ get_index_v… nu 2 ? in 504 let old_rs1 ≝ get_index_v… nu 3 ? in 505 let old_rs0 ≝ get_index_v… nl O ? in 506 let old_ov ≝ get_index_v… nl 1 ? in 507 let old_ud ≝ get_index_v… nl 2 ? in 508 let old_p ≝ get_index_v… nl 3 ? in 500 let old_cy ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) O ? in 501 let old_ac ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 1 ? in 502 let old_fo ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 2 ? in 503 let old_rs1 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 3 ? in 504 let old_rs0 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 4 ? in 505 let old_ov ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 5 ? in 506 let old_ud ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 6 ? in 507 let old_p ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 7 ? in 509 508 let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in 510 509 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
Note: See TracChangeset
for help on using the changeset viewer.