 Timestamp:
 Jun 10, 2011, 2:19:09 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r929 r930 1814 1814 qed. 1815 1815 1816 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1817 1818 lemma get_register_set_program_counter: 1819 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s. 1820 #T #s #pc % 1821 qed. 1822 1823 lemma get_8051_sfr_set_program_counter: 1824 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s. 1825 #T #s #pc % 1826 qed. 1827 1828 lemma get_bit_addressable_sfr_set_program_counter: 1829 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s. 1830 #T #s #pc % 1831 qed. 1832 1833 lemma low_internal_ram_set_program_counter: 1834 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s. 1835 #T #s #pc % 1836 qed. 1837 1838 lemma get_arg_8_set_program_counter: 1839 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) → 1840 ∀T,s,pc,b.∀arg:l. 1841 get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg. 1842 [2,3: cases arg; *; normalize //] 1843 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y % 1844 qed. 1845 1846 lemma get_arg_8_set_code_memory: 1847 ∀T1,T2,s,code_mem,b,arg. 1848 get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg. 1849 #T1 #T2 #s #code_mem #b #arg % 1850 qed. 1851 1852 lemma set_code_memory_set_flags: 1853 ∀T1,T2,s,f1,f2,f3,code_mem. 1854 set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem = 1855 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 % 1858 qed. 1859 1860 lemma set_program_counter_set_flags: 1861 ∀T1,s,f1,f2,f3,pc. 1862 set_program_counter T1 (set_flags T1 s f1 f2 f3) pc = 1863 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 % 1866 qed. 1867 1868 lemma program_counter_set_flags: 1869 ∀T1,s,f1,f2,f3. 1870 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 % 1872 qed. 1873 1874 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps. 1875 1816 1876 lemma main_thm: 1817 1877 ∀ticks_of. … … 1830 1890 #abs @⊥ normalize in abs; destruct (abs) ] 1831 1891 * #labels #costs generalize in match (refl … (code_memory … ps)) 1832 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ normalize nodelta;1892 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 1833 1893 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 1834 1894 [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ] … … 1850 1910 #K <K generalize in match K; K; 1851 1911 (* STATEMENT WITH EQUALITY HERE *) 1852 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;1912 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta; 1853 1913 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 1854 1914 #pi #newppc normalize nodelta; * #instructions *; 1855 1915 cases pi normalize nodelta; 1856 [ (* Instruction *) 1857  (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ 1858 whd in ⊢ (???(???(??%))) 1859 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 1860 >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2) 1861 1862  (* Cost *) 1863  (* Jmp *) 1864  (* Call *) 1865  (* Mov *) 1866 ] 1867 qed. 1916 [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0] 1917 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1918 #H2 >(eq_bv_to_eq … H2) >ignore_clock in EQ; #EQ >EQ % 1919 4: (* Jmp *) 1920 5: (* Call *) 1921 6: (* Mov *) 1922  (* Instruction *) pi; * 1923 [1,2: (* ADD, ADDC *) #arg1 #arg2 #H1 #H2 #EQ %[1,3:@1] 1924 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1925 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1926 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1927 * #H2a whd in ⊢ (% → ?) #H2b 1928 >ignore_clock in EQ; 1929 >(eq_instruction_to_eq … H2a) 1930 whd in ⊢ (???% → ??%?); 1931 >ignore_clock 1932 >get_arg_8_set_program_counter [2,4:%] 1933 >get_arg_8_set_program_counter [2,4:%] 1934 >get_arg_8_set_program_counter [2,4:%] 1935 >get_arg_8_set_program_counter [2,4:%] 1936 >get_arg_8_set_code_memory 1937 >get_arg_8_set_program_counter [2,4:%] 1938 >get_arg_8_set_program_counter [2,4:%] 1939 >get_arg_8_set_code_memory 1940 cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags 1941 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2b) newppc'; 1942 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1943 
Note: See TracChangeset
for help on using the changeset viewer.