Changeset 1511 for src/ASM/CostsProof.ma
- Timestamp:
- Nov 16, 2011, 5:35:24 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1509 r1511 55 55 definition current_instruction_cost ≝ 56 56 λs: Status. 57 let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in 58 cost. 57 \snd (fetch (code_memory … s) (program_counter … s)). 59 58 60 59 definition next_instruction_properly_relates_program_counters ≝ … … 64 63 let pc_before ≝ program_counter … before in 65 64 let pc_after ≝ program_counter … after in 66 let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in65 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 67 66 sum = pc_after. 68 67 … … 70 69 λs: Status. 71 70 let pc ≝ program_counter … s in 72 let 〈instruction, new_pc, cost〉 ≝ fetch … (code_memory … s) pc in 73 instruction. 71 \fst (\fst (fetch … (code_memory … s) pc)). 74 72 75 73 definition current_instruction_is_labelled ≝ … … 302 300 qed. 303 301 304 lemma status_execution_progresses_processor_clock: 302 example set_program_counter_ignores_clock: 303 ∀s: Status. 304 ∀pc: Word. 305 clock … (set_program_counter … s pc) = clock … s. 306 #s #pc % 307 qed. 308 309 example set_low_internal_ram_ignores_clock: 310 ∀s: Status. 311 ∀ram: BitVectorTrie Byte 7. 312 clock … (set_low_internal_ram … s ram) = clock … s. 313 #s #ram % 314 qed. 315 316 example set_8051_sfr_ignores_clock: 317 ∀s: Status. 318 ∀sfr: SFR8051. 319 ∀v: Byte. 320 clock … (set_8051_sfr ? s sfr v) = clock … s. 321 #s #sfr #v % 322 qed. 323 324 example clock_set_clock: 325 ∀s: Status. 326 ∀v. 327 clock … (set_clock … s v) = v. 328 #s #v % 329 qed. 330 331 example write_at_stack_pointer_ignores_clock: 332 ∀s: Status. 333 ∀sp: Byte. 334 clock … (write_at_stack_pointer … s sp) = clock … s. 335 #s #sp 336 change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with ( 337 let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in 338 ?); 339 normalize nodelta; 340 cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP)) 341 #nu #nl normalize nodelta; 342 cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) 343 [ normalize nodelta; % 344 | normalize nodelta; % 345 ] 346 qed. 347 348 example status_execution_progresses_processor_clock: 305 349 ∀s: Status. 306 350 clock … s ≤ clock … (execute 1 s). 307 #status 308 cases status 309 #ignore1 #ignore2 #ignore3 #ignore4 #ignore5 #ignore6 #ignore7 #ignore8 310 #ignore9 #clock 311 351 #s 352 change in match (execute 1 s) with (execute_1 s); 353 change in match (execute_1 s) with ( 354 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 355 (program_counter (BitVectorTrie Byte 16) s) 356 in 357 execute_1_0 s instr_pc_ticks); 358 normalize nodelta; 359 whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) 360 (program_counter (BitVectorTrie Byte 16) s))); 361 normalize nodelta; 362 cases (fetch (code_memory (BitVectorTrie Byte 16) s) 363 (program_counter (BitVectorTrie Byte 16) s)) 364 #instruction_pc #ticks 365 normalize nodelta; 366 cases instruction_pc 367 #instruction #pc 368 cases instruction 369 [1: 370 #addr11 cases addr11 #addressing_mode 371 normalize nodelta; cases addressing_mode 372 normalize nodelta; 373 [1,2,3,4,8,9,15,16,17,19: 374 #assm whd in ⊢ (% → ?) 375 #absurd cases(absurd) 376 |5,6,7,10,11,12,13,14: 377 whd in ⊢ (% → ?) 378 #absurd cases(absurd) 379 |18: 380 #addr11 #irrelevant 381 normalize nodelta; 382 >set_program_counter_ignores_clock 383 normalize nodelta; 384 >set_program_counter_ignores_clock 385 >write_at_stack_pointer_ignores_clock 386 >set_8051_sfr_ignores_clock 387 >write_at_stack_pointer_ignores_clock 388 >set_8051_sfr_ignores_clock 389 >clock_set_clock // 390 ] 391 |2: 392 #addr16 cases addr16 #addressing_mode 393 normalize nodelta; cases addressing_mode 394 normalize nodelta; 395 [1,2,3,4,8,9,15,16,17,18: 396 #assm whd in ⊢ (% → ?) 397 #absurd cases(absurd) 398 |5,6,7,10,11,12,13,14: 399 whd in ⊢ (% → ?) 400 #absurd cases(absurd) 401 |19: 402 #addr16 #irrelevant 403 normalize nodelta; 404 >set_program_counter_ignores_clock 405 >write_at_stack_pointer_ignores_clock 406 >set_8051_sfr_ignores_clock 407 >write_at_stack_pointer_ignores_clock 408 >set_8051_sfr_ignores_clock 409 >clock_set_clock 410 >set_program_counter_ignores_clock // 411 ] 412 |3: #addr11 cases addr11 #addressing_mode 413 normalize nodelta; cases addressing_mode 414 normalize nodelta; 415 [1,2,3,4,8,9,15,16,17,19: 416 #assm whd in ⊢ (% → ?) 417 #absurd cases(absurd) 418 |5,6,7,10,11,12,13,14: 419 whd in ⊢ (% → ?) 420 #absurd cases(absurd) 421 |18: 422 #word11 #irrelevant 423 normalize nodelta; 424 >set_program_counter_ignores_clock 425 >clock_set_clock 426 >set_program_counter_ignores_clock // 427 ] 428 |4: #addr16 cases addr16 #addressing_mode 429 normalize nodelta; cases addressing_mode 430 normalize nodelta; 431 [1,2,3,4,8,9,15,16,17,18: 432 #assm whd in ⊢ (% → ?) 433 #absurd cases(absurd) 434 |5,6,7,10,11,12,13,14: 435 whd in ⊢ (% → ?) 436 #absurd cases(absurd) 437 |19: 438 #word #irrelevant 439 normalize nodelta; 440 >set_program_counter_ignores_clock 441 >clock_set_clock 442 >set_program_counter_ignores_clock // 443 ] 444 |5: #relative cases relative #addressing_mode 445 normalize nodelta; cases addressing_mode 446 normalize nodelta; 447 [1,2,3,4,8,9,15,16,18,19: 448 #assm whd in ⊢ (% → ?) 449 #absurd cases(absurd) 450 |5,6,7,10,11,12,13,14: 451 whd in ⊢ (% → ?) 452 #absurd cases(absurd) 453 |17: 454 #byte #irrelevant 455 normalize nodelta; 456 >set_program_counter_ignores_clock 457 >set_program_counter_ignores_clock 458 >clock_set_clock // 459 ] 460 |6: #indirect_dptr cases indirect_dptr #addressing_mode 461 normalize nodelta; cases addressing_mode 462 normalize nodelta; 463 464 465 lemma current_instruction_cost_is_ok: 466 ∀s: Status. 467 current_instruction_cost s = clock … (execute 1 s) - clock … s. 468 #s 469 change in match (execute 1 s) with (execute_1 s); 470 change in match (execute_1 s) with ( 471 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 472 (program_counter (BitVectorTrie Byte 16) s) 473 in 474 execute_1_0 s instr_pc_ticks); 475 change in ⊢ (??%?) with ( 476 \snd (fetch (code_memory … s) (program_counter … s))); 477 normalize nodelta; 312 478 313 479 let rec compute_max_trace_label_label_cost_is_ok … … 348 514 |2: cases the_trace 349 515 [1: #the_status #not_return #not_jump #not_cost 516 change in ⊢ (??%?) with (current_instruction_cost the_status); 517 @current_instruction_cost_is_ok 350 518 |2: #the_status #is_return 519 change in ⊢ (??%?) with (current_instruction_cost the_status); 520 @current_instruction_cost_is_ok 351 521 |3: #the_status #is_jump #is_cost 522 change in ⊢ (??%?) with (current_instruction_cost the_status); 523 @current_instruction_cost_is_ok 352 524 |4: #end_flag #pre_fun_call #after_fun_call #final #is_call 353 #next_intruction_coherence #call_trace #final_trace 525 #next_instruction_coherence #call_trace #final_trace 526 change in ⊢ (??%?) with ( 527 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in 528 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in 529 let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in 530 call_trace_cost + current_instruction_cost + final_trace_cost) 531 normalize nodelta; 532 >current_instruction_cost_is_ok 533 >compute_max_trace_label_return_cost_is_ok 534 >compute_max_trace_label_label_pre_cost_is_ok 535 generalize in match next_instruction_coherence; 536 change in ⊢ (% → ?) with ( 537 let size ≝ current_instruction_cost pre_fun_call in 538 let pc_before ≝ program_counter … pre_fun_call in 539 let pc_after ≝ program_counter … after_fun_call in 540 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 541 sum = pc_after) 542 normalize nodelta; 543 >(plus_minus_rearrangement 544 (clock (BitVectorTrie Byte 16) after_fun_call) 545 (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)) 546 (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?); 354 547 |5: #end_flag #status_pre #status_end #tail_trace #is_not_call 355 548 #is_not_jump #is_not_ret #is_not_labelled 356 @current_instruction_cost 549 change in ⊢ (??%?) with ( 550 let current_instruction_cost ≝ current_instruction_cost status_pre in 551 let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in 552 current_instruction_cost + tail_trace_cost) 553 normalize nodelta; 554 >compute_max_trace_label_label_pre_cost_is_ok 555 >current_instruction_cost_is_ok 357 556 ] 358 557 ]
Note: See TracChangeset
for help on using the changeset viewer.