Changeset 1042 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 25, 2011, 2:30:07 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1041 r1042 1268 1268 sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 1269 1269 1270 axiom assembly_ok_to_expand_pseudo_instruction_ok:1271 ∀program,pol,assembled,costs.1272 〈assembled,costs〉 = assembly program pol →1273 ∀ppc.1274 let code_memory ≝ load_code_memory assembled in1275 let preamble ≝ \fst program in1276 let data_labels ≝ construct_datalabels preamble in1277 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in1278 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in1279 let expansion ≝ pol ppc in1280 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in1281 ∃instructions.1282 Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.1283 1284 1270 lemma fetch_assembly_pseudo2: 1285 1271 ∀program,pol,ppc. … … 1994 1980 whd in ⊢ (??(match ?%? with [_ ⇒ ?])?) 1995 1981 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 1996 1997 1998 1999 lemma main_thm0: 2000 ∀M,M',ps,ps',pol. 2001 next_internal_pseudo_address_map M ps = Some … M' → 2002 ∀H:ps' = execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps. 2003 ∃n. 2004 execute n (status_of_pseudo_status M ps pol) 2005 = status_of_pseudo_status M' ps' ?. 2006 [2: >H >execute_1_pseudo_instruction_preserves_code_memory @pol] 2007 #M #M' #ps #ps' #pol 2008 change with (next_internal_pseudo_address_map0 ???? = ? → ?) 2009 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps)) 2010 @pair_elim' #labels #costs #EQ1 normalize nodelta 2011 whd in match execute_1_pseudo_instruction 2012 @pair_elim' #pi #newppc #EQ2 normalize nodelta 2013 cases pi in EQ2; normalize nodelta 2014 [2: #ARG #MAP #H1 #H2 #EQ >MAP in EQ; 2015 2016 2017 cases (execute_1_pseudo_instruction_preserves_code_memory ??) XX 2018 cases (assembly ??) #assembled #costs normalize nodelta 2019 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta; 2020 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol 2021 #MAP 2022 cases (fetch_pseudo_instruction (\snd code_mem) ppc) 2023 2024 change with 2025 (? → ∃n. 2026 execute n 2027 (set_low_internal_ram ? 2028 (set_high_internal_ram ? 2029 (set_program_counter ? 2030 (set_code_memory ?? ps (load_code_memory ?)) 2031 (sigma ? pol (program_counter ? ps))) 2032 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2033 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2034 = set_low_internal_ram ? 2035 (set_high_internal_ram ? 2036 (set_program_counter ? 2037 (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory ?)) 2038 (sigma ???)) 2039 ?) 2040 ?) 2041 change with (next_internal_pseudo_address_map0 ???? = ? → ?) 2042 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps)) 2043 @pair_elim' #labels #costs #EQ1 normalize nodelta 2044 @pair_elim' #pi #newppc #EQ2 2045 >execute_1_pseudo_instruction_preserves_code_memory 2046 cases (assembly ??) #assembled #costs normalize nodelta 2047 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta; 2048 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol 2049 #MAP 2050 cases (fetch_pseudo_instruction (\snd code_mem) ppc) 2051 2052 2053 (code_memory pseudo_assembly_program ps) 2054 #MAP 2055 2056 2057 2058 whd in ⊢ (? → ? → ??%? → ??%? → ?) 2059 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 2060 cases (build_maps (code_memory … ps) pol) 2061 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 2062 generalize in match pol; pol; 2063 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%] 2064 #EQ0 #pol normalize nodelta; 2065 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 2066 [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ] 2067 * #final_ppc * #final_pc #assembled #EQ >EQ EQ ASS; normalize nodelta; 2068 #H generalize in match (H ? (refl …)) H; #H; 2069 #MAP 2070 #H1 generalize in match (option_destruct_Some ??? H1) H1; #H1 <H1 H1; 2071 #H2 generalize in match (option_destruct_Some ??? H2) H2; #H2 <H2 H2; 2072 change with 2073 (∃n. 2074 execute n 2075 (set_low_internal_ram ? 2076 (set_high_internal_ram ? 2077 (set_program_counter ? 2078 (set_code_memory ?? ps (load_code_memory assembled)) 2079 (sigma 〈preamble,instr_list〉 pol (program_counter ? ps))) 2080 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2081 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2082 = set_low_internal_ram ? 2083 (set_high_internal_ram ? 2084 (set_program_counter ? 2085 (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) 2086 (sigma ???)) 2087 ?) 2088 ?) 2089 whd in match (\snd 〈preamble,instr_list〉) in H; 2090 whd in match (\fst 〈preamble,instr_list〉) in H; 2091 whd in match (\snd 〈final_pc,assembled〉) in H; 2092 whd in match (\snd 〈preamble,instr_list〉) in MAP; 2093 s s'' labels costs final_ppc final_pc; 2094 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps) 2095 (* NICE STATEMENT HERE *) 2096 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; ps'; #ps' 2097 #K <K generalize in match K; K; 2098 (* STATEMENT WITH EQUALITY HERE *) 2099 whd in ⊢ (???(?%?) → ?) 2100 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) H; >EQ0 normalize nodelta; 2101 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ % 2102 #pi #newppc normalize nodelta; #MAP * #instructions *; 2103 cases pi in MAP; normalize nodelta; 2104 [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0] 2105 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP M'; 2106 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2107 #H2 >(eq_bv_eq … H2) >EQ % 2108 (* 6: (* Mov *) #arg1 #arg2 1982 6: (* Mov *) #arg1 #arg2 2109 1983 #H1 #H2 #EQ %[@1] 2110 1984 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) … … 2119 1993 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2120 1994 #result #flags 2121 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)2122 (*5: (* Call *) #label #MAP1995 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % 1996 5: (* Call *) #label #MAP 2123 1997 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP; 2124 1998 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta; … … 2308 2182  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2309 2183 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2310 *) (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta;2184  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2311 2185 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1] 2312 2186 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) … … 2318 2192 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; 2319 2193 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 2320 normalize nodelta; #MAP; (*2194 normalize nodelta; #MAP; 2321 2195 [1: change in ⊢ (? → %) with 2322 2196 ((let 〈result,flags〉 ≝ … … 2330 2204 change in ⊢ (???% → ?) with 2331 2205 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?) 2332 >get_arg_8_set_clock *)2206 >get_arg_8_set_clock 2333 2207 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ? 2334 2208 [2,4: #abs @⊥ normalize in abs; destruct (abs) … … 2349 2223 #result #flags 2350 2224 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % 2351 (* (* INC *) #arg1 #H1 #H2 #EQ %[@1]2225  (* INC *) #arg1 #H1 #H2 #EQ %[@1] 2352 2226 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2353 2227 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2381 2255 [ normalize nodelta (* HERE *) whd in ⊢ (??%%) % 2382 2256  2383 ] *) 2384 2385 lemma main_thm: 2386 ∀M,M',ps,pol. 2387 next_internal_pseudo_address_map M ps = Some … M' → 2388 ∃n. 2389 execute n (status_of_pseudo_status M ps pol) 2390 = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?. 2391 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 2257 ] 2258 cases daemon (* EASY CASES TO BE COMPLETED *) 2259 qed.
Note: See TracChangeset
for help on using the changeset viewer.