Changeset 988 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 16, 2011, 11:27:48 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r987 r988 1533 1533 1534 1534 axiom low_internal_ram_write_at_stack_pointer: 1535 ∀T1,T2,M,s1,s2,s3.∀p bu,pbl,bu,bl,sp1,sp2:BitVector 8.1535 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1536 1536 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 1537 1537 low_internal_ram ? s2 = low_internal_ram T2 s3 → 1538 1538 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 1539 1539 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 1540 bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →1540 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) → 1541 1541 low_internal_ram T1 1542 1542 (write_at_stack_pointer ? … … 1559 1559 1560 1560 axiom high_internal_ram_write_at_stack_pointer: 1561 ∀T1,T2,M,s1,s2,s3 .∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.1561 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1562 1562 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 1563 1563 high_internal_ram ? s2 = high_internal_ram T2 s3 → 1564 1564 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 1565 1565 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 1566 bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →1566 bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) → 1567 1567 high_internal_ram T1 1568 1568 (write_at_stack_pointer ? … … 1798 1798 1799 1799 lemma main_thm: 1800 ∀M,M',ps,s,s'' .1800 ∀M,M',ps,s,s'',pol. 1801 1801 next_internal_pseudo_address_map M ps = Some … M' → 1802 status_of_pseudo_status M ps = Some … s →1803 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) ) ps)= Some … s'' →1802 status_of_pseudo_status M ps pol = Some … s → 1803 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some … s'' → 1804 1804 ∃n. execute n s = s''. 1805 #M #M' #ps #s #s'' 1806 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1805 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 1806 #M #M' #ps #s #s'' #pol 1807 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol) 1807 1808 whd in ⊢ (? → ? → ??%? → ??%? → ?) 1808 1809 >execute_1_pseudo_instruction_preserves_code_memory 1809 generalize in match (refl … (assembly (code_memory … ps) ))1810 generalize in match (assembly (code_memory … ps) ) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)1811 cases (build_maps (code_memory … ps) )1810 generalize in match (refl … (assembly (code_memory … ps) pol)) 1811 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 1812 cases (build_maps (code_memory … ps) pol) 1812 1813 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 1813 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 1814 generalize in match pol; -pol; 1815 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%] 1816 #EQ0 #pol normalize nodelta; 1814 1817 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta; 1815 1818 [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ] … … 1826 1829 (set_program_counter ? 1827 1830 (set_code_memory ?? ps (load_code_memory assembled)) 1828 (sigma 〈preamble,instr_list〉 (program_counter ? ps)))1831 (sigma 〈preamble,instr_list〉 pol (program_counter ? ps))) 1829 1832 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 1830 1833 (low_internal_ram_of_pseudo_low_internal_ram M ?)) … … 1833 1836 (set_program_counter ? 1834 1837 (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) 1835 (sigma ?? ))1838 (sigma ???)) 1836 1839 ?) 1837 1840 ?) … … 1841 1844 whd in match (\snd 〈preamble,instr_list〉) in MAP; 1842 1845 -s s'' labels costs final_ppc final_pc; 1843 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 ) ps)1846 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps) 1844 1847 (* NICE STATEMENT HERE *) 1845 1848 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps' … … 1871 1874 |5: (* Call *) #label #MAP 1872 1875 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP; 1873 whd in ⊢ (???% → ?) cases ( jump_expansion ??) normalize nodelta;1876 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta; 1874 1877 [ (* short *) #abs @⊥ destruct (abs) 1875 1878 |3: (* long *) #H1 #H2 #EQ %[@1] 1876 1879 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1877 1880 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1878 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1881 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1879 1882 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1880 1883 >H2b >(eq_instruction_to_eq … H2a) … … 1885 1888 change with 1886 1889 ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) → 1887 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)1890 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?) 1888 1891 generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc 1889 generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;1892 generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta; 1890 1893 >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer 1891 1894 >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr … … 1898 1901 >set_clock_set_low_internal_ram 1899 1902 @low_internal_ram_write_at_stack_pointer 1900 [ % | %1903 [ >EQ0 @pol | % | % 1901 1904 | @(pair_destruct_2 … EQ1) 1902 1905 | @(pair_destruct_2 … EQ2) … … 1912 1915 >set_clock_set_high_internal_ram 1913 1916 @high_internal_ram_write_at_stack_pointer 1914 [ % | %1917 [ >EQ0 @pol | % | % 1915 1918 | @(pair_destruct_2 … EQ1) 1916 1919 | @(pair_destruct_2 … EQ2) … … 1926 1929 >external_ram_write_at_stack_pointer whd in ⊢ (???%) 1927 1930 >external_ram_write_at_stack_pointer % 1928 | change with (? = sigma ? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))1931 | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?)) 1929 1932 >EQ0 % 1930 1933 | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?) … … 1986 1989 |4: (* Jmp *) #label #MAP 1987 1990 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP; 1988 whd in ⊢ (???% → ?) cases ( jump_expansion ??) normalize nodelta;1991 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta; 1989 1992 [3: (* long *) #H1 #H2 #EQ %[@1] 1990 1993 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1991 1994 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1992 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1995 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1993 1996 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1994 1997 >H2b >(eq_instruction_to_eq … H2a) … … 2000 2003 (refl ? 2001 2004 (sub_16_with_carry 2002 (sigma 〈preamble,instr_list〉 (program_counter … ps))2003 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))2005 (sigma 〈preamble,instr_list〉 pol (program_counter … ps)) 2006 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label)) 2004 2007 false)) 2005 2008 cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta; … … 2009 2012 generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2010 2013 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2011 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2014 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2012 2015 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2013 2016 >H2b >(eq_instruction_to_eq … H2a) … … 2015 2018 whd in ⊢ (???% → ?); 2016 2019 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) 2017 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ?? ) ? in ?) = ?)2018 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))2020 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?) 2021 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower))) 2019 2022 cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4 2020 @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))2023 @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label)) 2021 2024 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2022 2025 | (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1; 2023 2026 generalize in match 2024 2027 (refl … 2025 (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))2028 (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label)))) 2026 2029 cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1 2027 2030 generalize in match 2028 2031 (refl … 2029 (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))2032 (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps)))) 2030 2033 cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2 2031 2034 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc)) … … 2033 2036 generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?) 2034 2037 change in ⊢ (? →??%?) with (execute_1_0 ??) 2035 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2038 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2036 2039 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2037 2040 >H2b >(eq_instruction_to_eq … H2a) … … 2039 2042 whd in ⊢ (???% → ?); 2040 2043 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?) 2041 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)2042 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))2044 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?) 2045 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) 2043 2046 cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4 2044 2047 generalize in match (refl … (split bool 4 4 pc_bu)) … … 2049 2052 generalize in match 2050 2053 (refl … 2051 (half_add 16 (sigma 〈preamble,instr_list〉 newppc)2054 (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) 2052 2055 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2))) 2053 2056 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2054 2057 @split_eq_status try % 2055 [ change with (? = sigma ? (address_of_word_labels ps label))2058 [ change with (? = sigma ?? (address_of_word_labels ps label)) 2056 2059 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2057 2060 | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
Note: See TracChangeset
for help on using the changeset viewer.