Changeset 2267 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jul 26, 2012, 12:05:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2266 r2267 205 205 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 206 206 whd in match (expand_pseudo_instruction ??????); 207 whd in match (ticks_of0 ??????); 208 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 209 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 210 [2: 211 inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 212 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 213 ] 207 whd in match (execute_1_pseudo_instruction0 ?????); 208 inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta 209 inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta 210 @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) carry_new_sp_refl #carry_new_sp_refl 211 @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) pc_bu_bl_refl #pc_bu_bl_refl 212 @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') carry_new_sp_refl' #carry_new_sp_refl' 214 213 #sigma_increment_commutation 215 214 normalize in sigma_increment_commutation:(???(???(??%))); 216 215 (* XXX: we work on the maps *) 217 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 216 whd in ⊢ (??%? → ?); 217 @pair_elim #callM #accM #Mrefl 218 @Some_Some_elim #map_refl_assm <map_refl_assm 218 219 (* XXX: we assume the fetch_many hypothesis *) 219 220 * #fetch_refl #fetch_many_assm … … 227 228 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 228 229 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 229 change with (set_program_counter ???? = 230 status_of_pseudo_status ?? (set_program_counter ????) ??) 231 @set_program_counter_status_of_pseudo_status 232 [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try % 233 [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try % 234 @sigma_increment_commutation 235  @eq_f2 try % @ticks_of_instruction_AJMP ]] 236 whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels; 237 normalize nodelta 238 [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 239 >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl 240 @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl)) 241 [2: >(andb_true_l … mj_possible_refl) % 242  <vsplit_refl @eq_f <EQnewpc % ] 243  >EQlookup_labels >create_label_cost_refl % 244  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 245 >create_label_cost_refl 246 >EQlookup_labels in sjc_refl; #sjc_refl 247 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 248 >(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 249 [2: >(andb_true_l … sj_possible_refl) % 250  >EQnewpc % ]] 251 252 253 254 255 256 257 258 259 260 261 262 263 #arg1 #pi_refl 264 (* XXX: we first work on sigma_increment_commutation *) 265 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 266 whd in match (expand_pseudo_instruction ??????); 267 whd in match (execute_1_pseudo_instruction0 ?????); 268 inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta 269 inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta 270 @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) carry_new_sp_refl #carry_new_sp_refl 271 @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) pc_bu_bl_refl #pc_bu_bl_refl 272 @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') carry_new_sp_refl' #carry_new_sp_refl' 273 #sigma_increment_commutation 274 normalize in sigma_increment_commutation:(???(???(??%))); 275 (* XXX: we work on the maps *) 276 whd in ⊢ (??%? → ?); 277 @pair_elim #callM #accM #Mrefl 278 @Some_Some_elim #map_refl_assm <map_refl_assm 279 (* XXX: we assume the fetch_many hypothesis *) 280 * #fetch_refl #fetch_many_assm 281 (* XXX: we give the existential *) 282 %{1} 283 (* XXX: work on the left hand side of the equality *) 284 whd in ⊢ (??%?); whd in match (program_counter ???); 285 (* XXX: execute fetches some more *) 286 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 287 whd in fetch_many_assm; 288 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 289 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 290 whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …)); 291 normalize in match (length ? (assembly1 …)) in EQnewpc; 292 normalize nodelta 230 whd in ⊢ (??%?); 293 231 [1: 294 232 @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 295 try /demod nohyps/ [1: %] 233 [ @eq_f2 try % 234 cases daemon (*CSC*) 235 ] whd in ⊢ (??%?); 236 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 237 @(pair_replace ????? ?? ??? carry_new_sp_refl') 238 [ @eq_f2 try % 239 cases daemon (*CSC*) 240 ] 241 whd in ⊢ (??%?); 242 @pair_elim #fiv #thr' #fiv_thr_refl' 243 change with (set_program_counter ???? = ?) 244 @set_program_counter_status_of_pseudo_status 245 [2: @sym_eq cases daemon (*@write_at_stack_pointer_status_of_pseudo_status try % 246 [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try % 247 @sigma_increment_commutation 248  @eq_f2 try % @ticks_of_instruction_AJMP ]*)] 249 whd in ajc_refl:(??%?); lapply ajc_refl ajc_refl map_refl_assm Mrefl 250 >EQlookup_labels normalize nodelta 251 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl 252 >fst_5_rest_refl normalize nodelta 253 @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 254 #pair_true_refl destruct(pair_true_refl) 255 <EQnewpc in fst_5_rest_pc_refl; 256 lapply pc_bu_bl_refl' pc_bu_bl_refl' 257 >program_counter_set_8051_sfr >set_clock_set_program_counter 258 >program_counter_set_program_counter #relevant2 259 <(vsplit_ok ?????? (sym_eq … relevant2)) 260 <(vsplit_ok ?????? (sym_eq … fiv_thr_refl')) 261 >(vector_associative_append bool 5 3 8) #relevant3 262 >(? : fiv = fst_5_addr) 263 [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta 264 >create_label_cost_refl % 265 2: 266 cases daemon (*CSC: make a lemma here!*) 267 ] 268  @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 269 [ @eq_f2 try % cases daemon ] 296 270 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 297 271 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 298 try /demod nohyps/ [1: %] 299 @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%); 300 @split_eq_status try /demod nohyps/ try % 301 [1,2: 302 (* XXX: need the commented out axioms from AssemblyProof.ma *) 303 cases daemon 304 3: 305 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta 306 change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 307 #relevant <(relevant arg1) 308 [2: 309 @(is_well_labelled_witness … ppc_in_bounds pi) 310 [1: 311 >fetch_pseudo_refl % 312 2: 313 >pi_refl % 314 ] 315 1: 316 whd in ajc_refl:(??%?); lapply ajc_refl ajc_refl map_refl_assm Mrefl 317 >EQlookup_labels normalize nodelta 318 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl 319 >fst_5_rest_refl normalize nodelta 320 @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 321 #pair_true_refl destruct(pair_true_refl) 322 <EQnewpc in fst_5_rest_pc_refl; 323 lapply pc_bu_bl_refl' pc_bu_bl_refl' 324 >program_counter_set_8051_sfr >set_clock_set_program_counter 325 >program_counter_set_program_counter #relevant2 326 <(vsplit_ok ?????? (sym_eq … relevant2)) 327 <(vsplit_ok ?????? (sym_eq … fiv_thr_refl')) 328 >(vector_associative_append bool 5 3 8) #relevant3 329 >(? : fiv = fst_5_addr) 330 [1: 331 % 332 2: 333 cases daemon 334 ] 335 ] 336 4: 337 >set_program_counter_mk_Status_commutation in ⊢ (???%); 338 >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%); 339 (* XXX: require set_8051_sfr_write_at_stack_pointer and 340 special_function_registers_8051_set_8051_sfr 341 *) 342 cases daemon 343 5,6,7: 344 >set_program_counter_mk_Status_commutation in ⊢ (???%); 345 (* XXX: similar to above but for 8052 346 *) 347 cases daemon 348 8: 349 whd in match (ticks_of_instruction ?); 350 cut(\snd (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2) 351 [1: // 352 2: 353 normalize in match (assembly1 ?); 354 @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) % 355 3: 356 #fetch_2_refl >fetch_2_refl >commutative_plus % 357 ] 358 ] 359 2: 360 @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 361 try /demod nohyps/ [1: %] 362 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 363 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 364 try /demod nohyps/ [1: %] 365 @split_eq_status try /demod nohyps/ try % 272 [ @eq_f2 try % cases daemon ] 273 change with (set_program_counter ???? = ?) 274 @set_program_counter_status_of_pseudo_status 275 [ >EQlookup_labels whd in match address_of_word_labels; normalize nodelta 276 >create_label_cost_refl % ] 277 cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl)) 366 278 [1: 367 cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl)) 368 [1: 369 >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/ 370 >set_clock_set_program_counter >program_counter_set_program_counter 371 >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl)) 372 2: 373 #relevant cases daemon 374 (* XXX: need axioms *) 375 ] 376 2: 377 cases daemon (* XXX: need axioms from assembly.ma *) 378 3: 379 change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 380 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta 381 #relevant <(relevant arg1) 382 [1: 383 >EQlookup_labels % 384 2: 385 @(is_well_labelled_witness … ppc_in_bounds pi) 386 [1: 387 >fetch_pseudo_refl % 388 2: 389 >pi_refl % 390 ] 391 ] 392 4: 393 >set_program_counter_mk_Status_commutation in ⊢ (???%); 394 >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%); 395 (* XXX: require set_8051_sfr_write_at_stack_pointer and 396 special_function_registers_8051_set_8051_sfr 397 *) 398 cases daemon 399 5,6,7: 400 >set_program_counter_mk_Status_commutation in ⊢ (???%); 401 (* XXX: similar to above but for 8052 402 *) 403 cases daemon 404 ] 279 >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) 280 >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl)) 281 >add_commutative 282 >program_counter_set_8051_sfr >set_clock_set_program_counter 283 >program_counter_set_program_counter >add_commutative 284 >program_counter_set_8051_sfr >set_clock_set_program_counter 285 >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl 286 @sym_eq 287 cases daemon 405 288 ] 406 289 ]
Note: See TracChangeset
for help on using the changeset viewer.