Changeset 1014 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 21, 2011, 2:02:37 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r998 r1014 1 1 include "ASM/Assembly.ma". 2 2 include "ASM/Interpret.ma". 3 include "ASM/StatusProofs.ma". 3 4 4 5 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ … … 1227 1228 let pc ≝ ? in 1228 1229 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1229 let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …)(refl …) (refl …) (refl …) in1230 let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in 1230 1231 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in 1231 1232 encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled → … … 1239 1240 letin pc ≝ (sigma program pol ppc) 1240 1241 letin pi ≝ (\fst (fetch_pseudo_instruction (\snd program) ppc)) 1241 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …)(refl …) (refl …) (refl …))1242 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …)) 1242 1243 @pair_elim' #len #assembled #EQ1 #H 1243 1244 generalize in match … … 1259 1260 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 1260 1261 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 1261 ∀ppc,pi,newppc.1262 ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc.1262 ∀ppc. 1263 let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in 1263 1264 ∀len,assembledi. 1264 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) ?→1265 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) → 1265 1266 encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧ 1266 sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 1267 <(pair_destruct_1 ????? prf) % 1268 qed. 1269 1270 (* 1267 sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 1268 1271 1269 axiom assembly_ok_to_expand_pseudo_instruction_ok: 1272 1270 ∀program,pol,assembled,costs. … … 1281 1279 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1282 1280 ∃instructions. 1283 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.1284 *) 1285 1286 lemmafetch_assembly_pseudo2:1287 ∀program,pol, assembled.1281 Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi. 1282 1283 (*CSC: repair me!*) 1284 axiom fetch_assembly_pseudo2: 1285 ∀program,pol,ppc. 1288 1286 let 〈labels,costs〉 ≝ build_maps program pol in 1289 〈assembled,costs〉 = assembly program pol → 1290 ∀ppc,pi,newppc. 1291 let code_memory ≝ load_code_memory assembled in 1292 let preamble ≝ \fst program in 1293 let data_labels ≝ construct_datalabels preamble in 1294 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 1295 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1296 ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc. 1297 let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) pi (refl …) (refl …) ? (refl …) in 1298 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1299 [2: <(pair_destruct_1 ????? prf) %] 1287 let assembled ≝ \fst (assembly program pol) in 1288 let code_memory ≝ load_code_memory assembled in 1289 let data_labels ≝ construct_datalabels (\fst program) in 1290 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 1291 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1292 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1293 let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in 1294 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1295 (* 1300 1296 #program #pol #assembled generalize in match (assembly_ok program pol assembled) 1301 1297 @pair_elim' #labels #costs #BUILD_MAPS … … 1306 1302 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) 1307 1303 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 1308 normalize nodelta #EQ generalize in match (H ASSEMBLY ppc … EQ) -H;1304 normalize nodelta #EQ generalize in match (H ASSEMBLY ppc) -H; 1309 1305 generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta 1310 @pair_elim' #len #assembledi #ASSEMBLE1 1306 @pair_elim' #len #assembledi #ASSEMBLE1 #H1 #H2 1307 generalize in match (H1 ?) [2: cases (H2 len assembledi (refl …)) #H1 #_ @H1] 1308 >bitvector_of_nat_nat_of_bitvector 1309 #K 1310 1311 1311 1312 1312 cases … … 1333 1333 [ #K3 % [2: % [% | @K3]] | @K1 ] 1334 1334 qed. 1335 1336 1335 *) 1336 1337 (* 1337 1338 lemma fetch_assembly_pseudo2: 1338 1339 ∀program,pol,assembled. 1339 1340 let 〈labels,costs〉 ≝ build_maps program pol in 1340 Some …〈assembled,costs〉 = assembly program pol →1341 〈assembled,costs〉 = assembly program pol → 1341 1342 ∀ppc. 1342 1343 let code_memory ≝ load_code_memory assembled in … … 1348 1349 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1349 1350 ∃instructions. 1350 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧1351 Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧ 1351 1352 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1352 1353 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc … … 1360 1361 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1361 1362 generalize in match (fetch_assembly_pseudo program pol ppc 1362 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi1363 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) 1363 1364 (load_code_memory assembled)); 1364 1365 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND … … 1373 1374 [ #K3 % [2: % [% | @K3]] | @K1 ] 1374 1375 qed. 1376 *) 1375 1377 1376 1378 (* OLD? … … 1520 1522 1521 1523 definition status_of_pseudo_status: 1522 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → optionStatus ≝1524 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝ 1523 1525 λM,ps,pol. 1524 1526 let pap ≝ code_memory … ps in 1525 match assembly pap pol with 1526 [ None ⇒ None … 1527 | Some p ⇒ 1528 let cm ≝ load_code_memory (\fst p) in 1529 let pc ≝ sigma pap pol (program_counter ? ps) in 1530 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1531 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in 1532 Some … 1533 (mk_PreStatus (BitVectorTrie Byte 16) 1534 cm 1535 lir 1536 hir 1537 (external_ram … ps) 1538 pc 1539 (special_function_registers_8051 … ps) 1540 (special_function_registers_8052 … ps) 1541 (p1_latch … ps) 1542 (p3_latch … ps) 1543 (clock … ps)) ]. 1527 let p ≝ assembly pap pol in 1528 let cm ≝ load_code_memory (\fst p) in 1529 let pc ≝ sigma pap pol (program_counter ? ps) in 1530 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1531 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in 1532 mk_PreStatus (BitVectorTrie Byte 16) 1533 cm 1534 lir 1535 hir 1536 (external_ram … ps) 1537 pc 1538 (special_function_registers_8051 … ps) 1539 (special_function_registers_8052 … ps) 1540 (p1_latch … ps) 1541 (p3_latch … ps) 1542 (clock … ps). 1544 1543 1545 1544 (* … … 1640 1639 *) 1641 1640 1641 (* DEAD CODE? 1642 1642 lemma status_of_pseudo_status_failure_depends_only_on_code_memory: 1643 1643 ∀M:internal_pseudo_address_map. … … 1657 1657 | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ] 1658 1658 qed. 1659 *) 1659 1660 1660 1661 definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝ … … 1820 1821 ticks_of0 program pol ppc fetched. 1821 1822 1822 lemma get_register_set_program_counter:1823 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.1824 #T #s #pc %1825 qed.1826 1827 lemma get_8051_sfr_set_program_counter:1828 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.1829 #T #s #pc %1830 qed.1831 1832 lemma get_bit_addressable_sfr_set_program_counter:1833 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.1834 #T #s #pc %1835 qed.1836 1837 lemma low_internal_ram_set_program_counter:1838 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.1839 #T #s #pc %1840 qed.1841 1842 lemma get_arg_8_set_program_counter:1843 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →1844 ∀T,s,pc,b.∀arg:l.1845 get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.1846 [2,3: cases arg; *; normalize //]1847 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %1848 qed.1849 1850 lemma set_bit_addressable_sfr_set_code_memory:1851 ∀T, U: Type[0].1852 ∀ps: PreStatus ?.1853 ∀code_mem.1854 ∀x.1855 ∀val.1856 set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =1857 set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.1858 #T #U #ps #code_mem #x #val1859 whd in ⊢ (??%?)1860 whd in ⊢ (???(???%?))1861 cases (eqb ? 128) [ normalize nodelta cases not_implemented1862 | normalize nodelta1863 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented1864 | normalize nodelta1865 cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented1866 | normalize nodelta1867 cases (eqb ? 176) [ normalize nodelta %1868 | normalize nodelta1869 cases (eqb ? 153) [ normalize nodelta %1870 | normalize nodelta1871 cases (eqb ? 138) [ normalize nodelta %1872 | normalize nodelta1873 cases (eqb ? 139) [ normalize nodelta %1874 | normalize nodelta1875 cases (eqb ? 140) [ normalize nodelta %1876 | normalize nodelta1877 cases (eqb ? 141) [ normalize nodelta %1878 | normalize nodelta1879 cases (eqb ? 200) [ normalize nodelta %1880 | normalize nodelta1881 cases (eqb ? 202) [ normalize nodelta %1882 | normalize nodelta1883 cases (eqb ? 203) [ normalize nodelta %1884 | normalize nodelta1885 cases (eqb ? 204) [ normalize nodelta %1886 | normalize nodelta1887 cases (eqb ? 205) [ normalize nodelta %1888 | normalize nodelta1889 cases (eqb ? 135) [ normalize nodelta %1890 | normalize nodelta1891 cases (eqb ? 136) [ normalize nodelta %1892 | normalize nodelta1893 cases (eqb ? 137) [ normalize nodelta %1894 | normalize nodelta1895 cases (eqb ? 152) [ normalize nodelta %1896 | normalize nodelta1897 cases (eqb ? 168) [ normalize nodelta %1898 | normalize nodelta1899 cases (eqb ? 184) [ normalize nodelta %1900 | normalize nodelta1901 cases (eqb ? 129) [ normalize nodelta %1902 | normalize nodelta1903 cases (eqb ? 130) [ normalize nodelta %1904 | normalize nodelta1905 cases (eqb ? 131) [ normalize nodelta %1906 | normalize nodelta1907 cases (eqb ? 208) [ normalize nodelta %1908 | normalize nodelta1909 cases (eqb ? 224) [ normalize nodelta %1910 | normalize nodelta1911 cases (eqb ? 240) [ normalize nodelta %1912 | normalize nodelta1913 cases not_implemented1914 ]]]]]]]]]]]]]]]]]]]]]]]]]]1915 qed.1916 1917 lemma set_arg_8_set_code_memory:1918 ∀n:nat.1919 ∀l:Vector addressing_mode_tag (S n).1920 ¬(is_in ? l ACC_PC) →1921 ∀T: Type[0].1922 ∀U: Type[0].1923 ∀ps: PreStatus ?.1924 ∀code_mem.1925 ∀val.1926 ∀b: l.1927 set_arg_8 ? (set_code_memory T U ps code_mem) b val =1928 set_code_memory T U (set_arg_8 ? ps b val) code_mem.1929 [2,3: cases b; *; normalize //]1930 #n #l #prf #T #U #ps #code_mem #val * *;1931 [*:1932 [1,2,3,4,8,9,15,16,17,18,19: #x]1933 try #y whd in ⊢ (??(%)?)1934 whd in ⊢ (???(???(%)?))1935 [1,2:1936 cases (split bool 4 4 ?)1937 #nu' #nl'1938 normalize nodelta1939 cases (split bool 1 3 nu')1940 #bit1' #ignore'1941 normalize nodelta1942 cases (get_index_v bool 4 nu' 0 ?)1943 [1,2,3,4:1944 normalize nodelta1945 try %1946 try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))1947 try (normalize in ⊢ (???(???%?)))1948 ]1949 |3,4: %1950 |*:1951 try normalize nodelta1952 normalize cases (not_implemented)1953 ]1954 ]1955 1956 1957 qed.1958 1959 axiom set_arg_8_set_program_counter:1960 ∀n:nat.1961 ∀l:Vector addressing_mode_tag (S n).1962 ¬(is_in ? l ACC_PC) →1963 ∀T: Type[0].1964 ∀ps: PreStatus ?.1965 ∀pc.1966 ∀val.1967 ∀b: l.1968 set_arg_8 ? (set_program_counter T ps pc) b val =1969 set_program_counter T (set_arg_8 ? ps b val) pc.1970 [1,2: cases b; *; normalize //]1971 qed.1972 1973 1974 lemma get_arg_8_set_code_memory:1975 ∀T1,T2,s,code_mem,b,arg.1976 get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.1977 #T1 #T2 #s #code_mem #b #arg %1978 qed.1979 1980 lemma set_code_memory_set_flags:1981 ∀T1,T2,s,f1,f2,f3,code_mem.1982 set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =1983 set_flags … (set_code_memory … s code_mem) f1 f2 f3.1984 #T1 #T2 #s #f1 #f2 #f3 #code_mem %1985 qed.1986 1987 lemma set_program_counter_set_flags:1988 ∀T1,s,f1,f2,f3,pc.1989 set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =1990 set_flags … (set_program_counter … s pc) f1 f2 f3.1991 #T1 #s #f1 #f2 #f3 #pc %1992 qed.1993 1994 lemma program_counter_set_flags:1995 ∀T1,s,f1,f2,f3.1996 program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.1997 #T1 #s #f1 #f2 #f3 %1998 qed.1999 2000 lemma special_function_registers_8051_write_at_stack_pointer:2001 ∀T,s,x.2002 special_function_registers_8051 T (write_at_stack_pointer T s x)2003 = special_function_registers_8051 T s.2004 #T #s #x whd in ⊢ (??(??%)?)2005 cases (split ????) #nu #nl normalize nodelta;2006 cases (get_index_v bool ????) %2007 qed.2008 2009 lemma get_8051_sfr_write_at_stack_pointer:2010 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.2011 #T #s #x #y whd in ⊢ (??%%) //2012 qed.2013 2014 lemma code_memory_write_at_stack_pointer:2015 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.2016 #T #s #x whd in ⊢ (??(??%)?)2017 cases (split ????) #nu #nl normalize nodelta;2018 cases (get_index_v bool ????) %2019 qed.2020 2021 axiom low_internal_ram_write_at_stack_pointer:2022 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.2023 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →2024 low_internal_ram ? s2 = low_internal_ram T2 s3 →2025 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →2026 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →2027 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →2028 low_internal_ram T12029 (write_at_stack_pointer ?2030 (set_8051_sfr ?2031 (write_at_stack_pointer ?2032 (set_8051_sfr ?2033 (set_low_internal_ram ? s12034 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))2035 SFR_SP sp1)2036 bl)2037 SFR_SP sp2)2038 bu)2039 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)2040 (low_internal_ram ?2041 (write_at_stack_pointer ?2042 (set_8051_sfr ?2043 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)2044 SFR_SP sp2)2045 pbu)).2046 2047 axiom high_internal_ram_write_at_stack_pointer:2048 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.2049 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →2050 high_internal_ram ? s2 = high_internal_ram T2 s3 →2051 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →2052 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →2053 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →2054 high_internal_ram T12055 (write_at_stack_pointer ?2056 (set_8051_sfr ?2057 (write_at_stack_pointer ?2058 (set_8051_sfr ?2059 (set_high_internal_ram ? s12060 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))2061 SFR_SP sp1)2062 bl)2063 SFR_SP sp2)2064 bu)2065 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)2066 (high_internal_ram ?2067 (write_at_stack_pointer ?2068 (set_8051_sfr ?2069 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)2070 SFR_SP sp2)2071 pbu)).2072 2073 lemma set_program_counter_set_low_internal_ram:2074 ∀T,s,x,y.2075 set_program_counter T (set_low_internal_ram … s x) y =2076 set_low_internal_ram … (set_program_counter … s y) x.2077 //2078 qed.2079 2080 lemma set_clock_set_low_internal_ram:2081 ∀T,s,x,y.2082 set_clock T (set_low_internal_ram … s x) y =2083 set_low_internal_ram … (set_clock … s y) x.2084 //2085 qed.2086 2087 lemma set_program_counter_set_high_internal_ram:2088 ∀T,s,x,y.2089 set_program_counter T (set_high_internal_ram … s x) y =2090 set_high_internal_ram … (set_program_counter … s y) x.2091 //2092 qed.2093 2094 lemma set_clock_set_high_internal_ram:2095 ∀T,s,x,y.2096 set_clock T (set_high_internal_ram … s x) y =2097 set_high_internal_ram … (set_clock … s y) x.2098 //2099 qed.2100 2101 lemma set_low_internal_ram_set_high_internal_ram:2102 ∀T,s,x,y.2103 set_low_internal_ram T (set_high_internal_ram … s x) y =2104 set_high_internal_ram … (set_low_internal_ram … s y) x.2105 //2106 qed.2107 2108 lemma external_ram_write_at_stack_pointer:2109 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.2110 #T #s #x whd in ⊢ (??(??%)?)2111 cases (split ????) #nu #nl normalize nodelta;2112 cases (get_index_v bool ????) %2113 qed.2114 2115 lemma special_function_registers_8052_write_at_stack_pointer:2116 ∀T,s,x.2117 special_function_registers_8052 T (write_at_stack_pointer T s x)2118 = special_function_registers_8052 T s.2119 #T #s #x whd in ⊢ (??(??%)?)2120 cases (split ????) #nu #nl normalize nodelta;2121 cases (get_index_v bool ????) %2122 qed.2123 2124 lemma p1_latch_write_at_stack_pointer:2125 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.2126 #T #s #x whd in ⊢ (??(??%)?)2127 cases (split ????) #nu #nl normalize nodelta;2128 cases (get_index_v bool ????) %2129 qed.2130 2131 lemma p3_latch_write_at_stack_pointer:2132 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.2133 #T #s #x whd in ⊢ (??(??%)?)2134 cases (split ????) #nu #nl normalize nodelta;2135 cases (get_index_v bool ????) %2136 qed.2137 2138 lemma clock_write_at_stack_pointer:2139 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.2140 #T #s #x whd in ⊢ (??(??%)?)2141 cases (split ????) #nu #nl normalize nodelta;2142 cases (get_index_v bool ????) %2143 qed.2144 2145 axiom get_index_v_set_index:2146 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.2147 2148 lemma get_8051_sfr_set_8051_sfr:2149 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.2150 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)2151 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index2152 qed.2153 2154 lemma program_counter_set_8051_sfr:2155 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.2156 //2157 qed.2158 2159 axiom get_arg_8_set_low_internal_ram:2160 ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.2161 2162 1823 lemma eq_rect_Type1_r: 2163 1824 ∀A: Type[1]. … … 2169 1830 cases p 2170 1831 // 2171 qed.2172 2173 lemma split_eq_status:2174 ∀T.2175 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.2176 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.2177 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →2178 mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =2179 mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.2180 //2181 1832 qed. 2182 1833 … … 2277 1928 *) 2278 1929 2279 lemma main_thm: 1930 axiom low_internal_ram_write_at_stack_pointer: 1931 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1932 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 1933 low_internal_ram ? s2 = low_internal_ram T2 s3 → 1934 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 1935 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 1936 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) → 1937 low_internal_ram T1 1938 (write_at_stack_pointer ? 1939 (set_8051_sfr ? 1940 (write_at_stack_pointer ? 1941 (set_8051_sfr ? 1942 (set_low_internal_ram ? s1 1943 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2))) 1944 SFR_SP sp1) 1945 bl) 1946 SFR_SP sp2) 1947 bu) 1948 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M) 1949 (low_internal_ram ? 1950 (write_at_stack_pointer ? 1951 (set_8051_sfr ? 1952 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl) 1953 SFR_SP sp2) 1954 pbu)). 1955 1956 axiom high_internal_ram_write_at_stack_pointer: 1957 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1958 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 1959 high_internal_ram ? s2 = high_internal_ram T2 s3 → 1960 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 1961 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 1962 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) → 1963 high_internal_ram T1 1964 (write_at_stack_pointer ? 1965 (set_8051_sfr ? 1966 (write_at_stack_pointer ? 1967 (set_8051_sfr ? 1968 (set_high_internal_ram ? s1 1969 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2))) 1970 SFR_SP sp1) 1971 bl) 1972 SFR_SP sp2) 1973 bu) 1974 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M) 1975 (high_internal_ram ? 1976 (write_at_stack_pointer ? 1977 (set_8051_sfr ? 1978 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl) 1979 SFR_SP sp2) 1980 pbu)). 1981 1982 lemma main_thm0: 2280 1983 ∀M,M',ps,s,s'',pol. 2281 1984 next_internal_pseudo_address_map M ps = Some … M' → 2282 status_of_pseudo_status M ps pol = Some …s →2283 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some …s'' →1985 status_of_pseudo_status M ps pol = s → 1986 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = s'' → 2284 1987 ∃n. execute n s = s''. 2285 1988 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 2286 1989 #M #M' #ps #s #s'' #pol 2287 1990 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol) 1991 >execute_1_pseudo_instruction_preserves_code_memory 1992 generalize in match (refl … (assembly (code_memory … ps) pol)) 1993 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K; 1994 1995 2288 1996 whd in ⊢ (? → ? → ??%? → ??%? → ?) 2289 1997 >execute_1_pseudo_instruction_preserves_code_memory 2290 1998 generalize in match (refl … (assembly (code_memory … ps) pol)) 1999 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K; 2000 whd in ⊢ (???% → ?) 2001 cases (build_maps (code_memory … ps) pol) 2002 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 2003 cases (code_memory … ps) in pol ⊢ %; 2004 generalize in match pol; -pol; 2005 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%] 2006 #EQ0 #pol normalize nodelta; 2007 2008 2009 2010 lemma main_thm0: 2011 ∀M,M',ps,ps',pol. 2012 next_internal_pseudo_address_map M ps = Some … M' → 2013 ∀H:ps' = execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps. 2014 ∃n. 2015 execute n (status_of_pseudo_status M ps pol) 2016 = status_of_pseudo_status M' ps' ?. 2017 [2: >H >execute_1_pseudo_instruction_preserves_code_memory @pol] 2018 #M #M' #ps #ps' #pol 2019 change with (next_internal_pseudo_address_map0 ???? = ? → ?) 2020 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps)) 2021 @pair_elim' #labels #costs #EQ1 normalize nodelta 2022 whd in match execute_1_pseudo_instruction 2023 @pair_elim' #pi #newppc #EQ2 normalize nodelta 2024 cases pi in EQ2; normalize nodelta 2025 [2: #ARG #MAP #H1 #H2 #EQ >MAP in EQ; 2026 2027 2028 cases (execute_1_pseudo_instruction_preserves_code_memory ??) XX 2029 cases (assembly ??) #assembled #costs normalize nodelta 2030 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta; 2031 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol 2032 #MAP 2033 cases (fetch_pseudo_instruction (\snd code_mem) ppc) 2034 2035 change with 2036 (? → ∃n. 2037 execute n 2038 (set_low_internal_ram ? 2039 (set_high_internal_ram ? 2040 (set_program_counter ? 2041 (set_code_memory ?? ps (load_code_memory ?)) 2042 (sigma ? pol (program_counter ? ps))) 2043 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2044 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2045 = set_low_internal_ram ? 2046 (set_high_internal_ram ? 2047 (set_program_counter ? 2048 (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory ?)) 2049 (sigma ???)) 2050 ?) 2051 ?) 2052 change with (next_internal_pseudo_address_map0 ???? = ? → ?) 2053 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps)) 2054 @pair_elim' #labels #costs #EQ1 normalize nodelta 2055 @pair_elim' #pi #newppc #EQ2 2056 >execute_1_pseudo_instruction_preserves_code_memory 2057 cases (assembly ??) #assembled #costs normalize nodelta 2058 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta; 2059 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol 2060 #MAP 2061 cases (fetch_pseudo_instruction (\snd code_mem) ppc) 2062 2063 2064 (code_memory pseudo_assembly_program ps) 2065 #MAP 2066 2067 2068 2069 whd in ⊢ (? → ? → ??%? → ??%? → ?) 2291 2070 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 2292 2071 cases (build_maps (code_memory … ps) pol) … … 2614 2393 | 2615 2394 ] *) 2395 2396 lemma main_thm: 2397 ∀M,M',ps,pol. 2398 next_internal_pseudo_address_map M ps = Some … M' → 2399 ∃n. 2400 execute n (status_of_pseudo_status M ps pol) 2401 = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?. 2402 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
Note: See TracChangeset
for help on using the changeset viewer.