 Timestamp:
 Jun 13, 2011, 11:37:46 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r945 r946 2068 2068 qed. 2069 2069 2070 (* 2070 2071 lemma blah: 2071 2072 ∀p: pseudo_instruction. … … 2085 2086 else None internal_pseudo_address_map ) 2086 2087 =Some internal_pseudo_address_map M') 2088 *) 2087 2089 2088 2090 lemma main_thm: … … 2161 2163 #result #flags 2162 2164 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *) 2163 (* 4,5: (* Jmp, Call *) #label 2165 4: (* Jmp *) #label #MAP 2166 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 2167 [3: (* long *) #H1 #H2 #EQ %[@1] 2168 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2169 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2170 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2171 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2172 >H2b >(eq_instruction_to_eq … H2a) 2173 generalize in match EQ; EQ; 2174 #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 *) 2202  (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2203 generalize in match 2204 (refl … 2205 (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label)))) 2206 cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1 2207 generalize in match 2208 (refl … 2209 (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps)))) 2210 cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2 2211 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc)) 2212 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)] 2213 generalize in match (option_destruct_Some ??? TEQ) TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?) 2214 change in ⊢ (? →??%?) with (execute_1_0 ??) 2215 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2216 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2217 >H2b >(eq_instruction_to_eq … H2a) 2218 generalize in match EQ; EQ; 2219 whd in ⊢ (???% → ?); 2220 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?) 2221 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2222 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc))) 2223 cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4 2224 generalize in match (refl … (split bool 4 4 pc_bu)) 2225 cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5 2226 generalize in match (refl … (split bool 3 8 rest_addr)) 2227 cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6 2228 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?) 2229 generalize in match 2230 (refl … 2231 (half_add 16 (sigma 〈preamble,instr_list〉 newppc) 2232 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2))) 2233 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7 2234 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP 2235 @split_eq_status try % 2236 [ change with (? = sigma ? (address_of_word_labels ps label)) 2237 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2238  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2239 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2240 (* 5: (* Call *) #label 2164 2241 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 2165 2242 [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1] … … 2243 2320 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2244 2321  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2245 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2246 (*5: (* Call *)*) *) 2322 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *) 2247 2323  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2248 2324 [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.