 Timestamp:
 Jun 13, 2011, 3:28:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r946 r948 2047 2047 qed. 2048 2048 2049 lemma special_function_registers_8051_write_at_stack_pointer: 2050 ∀T,s,x. 2051 special_function_registers_8051 T (write_at_stack_pointer T s x) 2052 = special_function_registers_8051 T s. 2053 #T #s #x whd in ⊢ (??(??%)?) 2054 cases (split ????) #nu #nl normalize nodelta; 2055 cases (get_index_v bool ????) % 2056 qed. 2057 2058 lemma get_8051_sfr_write_at_stack_pointer: 2059 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y. 2060 #T #s #x #y whd in ⊢ (??%%) // 2061 qed. 2062 2063 lemma code_memory_write_at_stack_pointer: 2064 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. 2065 #T #s #x whd in ⊢ (??(??%)?) 2066 cases (split ????) #nu #nl normalize nodelta; 2067 cases (get_index_v bool ????) % 2068 qed. 2069 2070 (* 2071 lemma low_internal_ram_write_at_stack_pointer: 2072 ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s. 2073 #T #s #x whd in ⊢ (??(??%)?) 2074 cases (split ????) #nu #nl normalize nodelta; 2075 cases (get_index_v bool ????) normalize nodelta; // 2076 qed. 2077 2078 lemma high_internal_ram_write_at_stack_pointer: 2079 ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s. 2080 #T #s #x whd in ⊢ (??(??%)?) 2081 cases (split ????) #nu #nl normalize nodelta; 2082 cases (get_index_v bool ????) % 2083 qed. 2084 *) 2085 2086 lemma external_ram_write_at_stack_pointer: 2087 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s. 2088 #T #s #x whd in ⊢ (??(??%)?) 2089 cases (split ????) #nu #nl normalize nodelta; 2090 cases (get_index_v bool ????) % 2091 qed. 2092 2093 lemma special_function_registers_8052_write_at_stack_pointer: 2094 ∀T,s,x. 2095 special_function_registers_8052 T (write_at_stack_pointer T s x) 2096 = special_function_registers_8052 T s. 2097 #T #s #x whd in ⊢ (??(??%)?) 2098 cases (split ????) #nu #nl normalize nodelta; 2099 cases (get_index_v bool ????) % 2100 qed. 2101 2102 lemma p1_latch_write_at_stack_pointer: 2103 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s. 2104 #T #s #x whd in ⊢ (??(??%)?) 2105 cases (split ????) #nu #nl normalize nodelta; 2106 cases (get_index_v bool ????) % 2107 qed. 2108 2109 lemma p3_latch_write_at_stack_pointer: 2110 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s. 2111 #T #s #x whd in ⊢ (??(??%)?) 2112 cases (split ????) #nu #nl normalize nodelta; 2113 cases (get_index_v bool ????) % 2114 qed. 2115 2116 lemma clock_write_at_stack_pointer: 2117 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s. 2118 #T #s #x whd in ⊢ (??(??%)?) 2119 cases (split ????) #nu #nl normalize nodelta; 2120 cases (get_index_v bool ????) % 2121 qed. 2122 2049 2123 lemma eq_rect_Type1_r: 2050 2124 ∀A: Type[1]. … … 2163 2237 #result #flags 2164 2238 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *) 2165 4: (* Jmp *) #label #MAP 2239 5: (* Call *) #label #MAP 2240 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP; 2166 2241 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 2167 [3: (* long *) #H1 #H2 #EQ %[@1] 2242 [ (* short *) #abs @⊥ destruct (abs) 2243 3: (* long *) #H1 #H2 #EQ %[@1] 2168 2244 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2169 2245 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2172 2248 >H2b >(eq_instruction_to_eq … H2a) 2173 2249 generalize in match EQ; EQ; 2250 whd in ⊢ (???% → ??%?); 2251 cases (half_add ???) #carry #new_sp normalize nodelta; 2252 >(eq_bv_to_eq … H2c) 2253 change with 2254 ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) → 2255 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2256 generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc 2257 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; 2258 >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer 2259 cases (half_add ???) #carry' #new_sp' normalize nodelta; 2174 2260 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2175 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX 2176 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP % 2177 1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2178 generalize in match 2179 (refl ? 2180 (sub_16_with_carry 2181 (sigma 〈preamble,instr_list〉 (program_counter … ps)) 2182 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label)) 2183 false)) 2184 cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta; 2185 generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta; 2186 generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; 2187 #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)] 2188 generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2189 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2190 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2191 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2192 >H2b >(eq_instruction_to_eq … H2a) 2193 generalize in match EQ; EQ; 2194 whd in ⊢ (???% → ?); 2195 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2196 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?) 2197 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower))) 2198 cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4 2199 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP 2200 @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label)) 2201 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2261 @split_eq_status;(* whd in ⊢ (??%%)*) 2262 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?) 2263 >code_memory_write_at_stack_pointer % 2264  change with 2265 (low_internal_ram ? 2266 (write_at_stack_pointer ? 2267 (set_8051_sfr ? 2268 (write_at_stack_pointer ? 2269 (set_low_internal_ram ? ps 2270 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps))) 2271 pc_bl) ??) pc_bu) = ?) 2272  2273  >external_ram_write_at_stack_pointer whd in ⊢ (??%?) 2274 >external_ram_write_at_stack_pointer whd in ⊢ (???%) 2275 >external_ram_write_at_stack_pointer whd in ⊢ (???%) 2276 >external_ram_write_at_stack_pointer % 2277  change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?)) 2278 >EQ0 % 2279  >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?) 2280 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%) 2281 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%) 2282 >special_function_registers_8051_write_at_stack_pointer % 2283  >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?) 2284 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%) 2285 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%) 2286 >special_function_registers_8052_write_at_stack_pointer % 2287  >p1_latch_write_at_stack_pointer whd in ⊢ (??%?) 2288 >p1_latch_write_at_stack_pointer whd in ⊢ (???%) 2289 >p1_latch_write_at_stack_pointer whd in ⊢ (???%) 2290 >p1_latch_write_at_stack_pointer % 2291  >p3_latch_write_at_stack_pointer whd in ⊢ (??%?) 2292 >p3_latch_write_at_stack_pointer whd in ⊢ (???%) 2293 >p3_latch_write_at_stack_pointer whd in ⊢ (???%) 2294 >p3_latch_write_at_stack_pointer % 2295  >clock_write_at_stack_pointer whd in ⊢ (??%?) 2296 >clock_write_at_stack_pointer whd in ⊢ (???%) 2297 >clock_write_at_stack_pointer whd in ⊢ (???%) 2298 >clock_write_at_stack_pointer %] 2202 2299  (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2203 2300 generalize in match … … 2232 2329 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2))) 2233 2330 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2234 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP2235 2331 @split_eq_status try % 2236 2332 [ change with (? = sigma ? (address_of_word_labels ps label)) 2237 2333 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2238 2334  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2239 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2240 (* 5: (* Call *) #label 2335 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *) 2336 4: (* Jmp *) #label #MAP 2337 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP MAP; 2241 2338 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 2242 [3 ,6: (* long *) #H1 #H2 #EQ %[1,3:@1]2339 [3: (* long *) #H1 #H2 #EQ %[@1] 2243 2340 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2244 2341 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2247 2344 >H2b >(eq_instruction_to_eq … H2a) 2248 2345 generalize in match EQ; EQ; 2249 [2: whd in ⊢ (???% → ??%?);2250 cases (half_add ???) #carry #new_sp normalize nodelta;2251 >(eq_bv_to_eq … H2c)2252 change with2253 ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) →2254 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)2255 (* MISMATCH ON WHAT IS ON THE STACK!!!! *)2256 (* HOW TO PROVE THIS?? *)2257 ]2258 2346 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2259 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX 2260 [2: %  ] 2261 4: (* short Call *) #abs @⊥ destruct (abs) 2262 1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2347 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 2348 1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2263 2349 generalize in match 2264 2350 (refl ? … … 2315 2401 (half_add 16 (sigma 〈preamble,instr_list〉 newppc) 2316 2402 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2))) 2317 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2403 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2318 2404 @split_eq_status try % 2319 2405 [ change with (? = sigma ? (address_of_word_labels ps label)) 2320 2406 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2321 2407  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2322 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)2408 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2323 2409  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2324 2410 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
Note: See TracChangeset
for help on using the changeset viewer.