Changeset 1953
- Timestamp:
- May 16, 2012, 10:29:22 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1952 r1953 1850 1850 λpolicy. 1851 1851 λppc: Word. 1852 λfetched. ?. 1853 cases daemon(* 1852 λfetched. 1854 1853 match fetched with 1855 1854 [ Instruction instr ⇒ 1856 1855 match instr with 1857 [ JC lbl ⇒ 1856 [ JC lbl ⇒ ? (* 1858 1857 match pol lookup_labels ppc with 1859 1858 [ short_jump ⇒ 〈2, 2〉 1860 1859 | medium_jump ⇒ ? 1861 1860 | long_jump ⇒ 〈4, 4〉 1862 ] 1863 | JNC lbl ⇒ 1861 ] *) 1862 | JNC lbl ⇒ ? (* 1864 1863 match pol lookup_labels ppc with 1865 1864 [ short_jump ⇒ 〈2, 2〉 1866 1865 | medium_jump ⇒ ? 1867 1866 | long_jump ⇒ 〈4, 4〉 1868 ] 1869 | JB bit lbl ⇒ 1867 ] *) 1868 | JB bit lbl ⇒ ? (* 1870 1869 match pol lookup_labels ppc with 1871 1870 [ short_jump ⇒ 〈2, 2〉 1872 1871 | medium_jump ⇒ ? 1873 1872 | long_jump ⇒ 〈4, 4〉 1874 ] 1875 | JNB bit lbl ⇒ 1873 ] *) 1874 | JNB bit lbl ⇒ ? (* 1876 1875 match pol lookup_labels ppc with 1877 1876 [ short_jump ⇒ 〈2, 2〉 1878 1877 | medium_jump ⇒ ? 1879 1878 | long_jump ⇒ 〈4, 4〉 1880 ] 1881 | JBC bit lbl ⇒ 1879 ] *) 1880 | JBC bit lbl ⇒ ? (* 1882 1881 match pol lookup_labels ppc with 1883 1882 [ short_jump ⇒ 〈2, 2〉 1884 1883 | medium_jump ⇒ ? 1885 1884 | long_jump ⇒ 〈4, 4〉 1886 ] 1887 | JZ lbl ⇒ 1885 ] *) 1886 | JZ lbl ⇒ ? (* 1888 1887 match pol lookup_labels ppc with 1889 1888 [ short_jump ⇒ 〈2, 2〉 1890 1889 | medium_jump ⇒ ? 1891 1890 | long_jump ⇒ 〈4, 4〉 1892 ] 1893 | JNZ lbl ⇒ 1891 ] *) 1892 | JNZ lbl ⇒ ? (* 1894 1893 match pol lookup_labels ppc with 1895 1894 [ short_jump ⇒ 〈2, 2〉 1896 1895 | medium_jump ⇒ ? 1897 1896 | long_jump ⇒ 〈4, 4〉 1898 ] 1899 | CJNE arg lbl ⇒ 1897 ] *) 1898 | CJNE arg lbl ⇒ ? (* 1900 1899 match pol lookup_labels ppc with 1901 1900 [ short_jump ⇒ 〈2, 2〉 1902 1901 | medium_jump ⇒ ? 1903 1902 | long_jump ⇒ 〈4, 4〉 1904 ] 1905 | DJNZ arg lbl ⇒ 1903 ] *) 1904 | DJNZ arg lbl ⇒ ? (* 1906 1905 match pol lookup_labels ppc with 1907 1906 [ short_jump ⇒ 〈2, 2〉 1908 1907 | medium_jump ⇒ ? 1909 1908 | long_jump ⇒ 〈4, 4〉 1910 ] 1909 ] *) 1911 1910 | ADD arg1 arg2 ⇒ 1912 1911 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in … … 2000 1999 | Mov dptr tgt ⇒ 〈2, 2〉 2001 2000 ]. 2002 cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)2003 *)qed.2001 cases daemon 2002 qed. 2004 2003 2005 2004 definition ticks_of: … … 2032 2031 v = v' ∧ q = q'. 2033 2032 2034 axiomsplit_vector_singleton:2033 lemma split_vector_singleton: 2035 2034 ∀A: Type[0]. 2036 2035 ∀n: nat. … … 2038 2037 ∀rest: Vector A n. 2039 2038 ∀s: Vector A 1. 2040 ∀prf.2041 2039 v = s @@ rest → 2042 ((get_index_v A ? v 0 prf) ::: rest) = v. 2040 ((get_index_v A ? v 0 ?) ::: rest) = v. 2041 [1: 2042 #A #n #v cases daemon (* XXX: !!! *) 2043 |2: 2044 @le_S_S @le_O_n 2045 ] 2046 qed. 2043 2047 2044 2048 example sub_minus_one_seven_eight: … … 2121 2125 2122 2126 axiom low_internal_ram_write_at_stack_pointer: 2123 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2127 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool. 2128 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2124 2129 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 2125 2130 low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 → 2126 2131 sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) → 2127 2132 sp2 = add ? sp1 (bitvector_of_nat 8 1) → 2128 bu@@bl = \fst (sigma (pbu@@pbl)) →2133 bu@@bl = sigma (pbu@@pbl) → 2129 2134 low_internal_ram T1 cm1 2130 2135 (write_at_stack_pointer … … … 2146 2151 pbu)). 2147 2152 2148 axiom high_internal_ram_write_at_stack_pointer: 2149 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2153 lemma high_internal_ram_write_at_stack_pointer: 2154 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool. 2155 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2150 2156 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 2151 2157 high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 → 2152 2158 sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) → 2153 2159 sp2 = add ? sp1 (bitvector_of_nat 8 1) → 2154 bu@@bl = \fst (sigma (pbu@@pbl)) →2160 bu@@bl = sigma (pbu@@pbl) → 2155 2161 high_internal_ram T1 cm1 2156 2162 (write_at_stack_pointer … … … 2171 2177 SFR_SP sp2) 2172 2178 pbu)). 2179 #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2 2180 #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl 2181 cases daemon (* XXX: !!! *) 2182 qed. 2173 2183 2174 2184 lemma Some_Some_elim: … … 2178 2188 2179 2189 (*CSC: ???*) 2180 axiomsnd_assembly_1_pseudoinstruction_ok:2190 lemma snd_assembly_1_pseudoinstruction_ok: 2181 2191 ∀program: pseudo_assembly_program. 2182 2192 ∀sigma: Word → Word. … … 2191 2201 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels pi) in 2192 2202 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2203 #program #sigma #policy #ppc #pi #lookup_labels #lookup_datalabels 2204 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 2205 normalize nodelta cases daemon (* XXX: !!! *) 2206 qed. 2193 2207 2194 2208 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
Note: See TracChangeset
for help on using the changeset viewer.