Changeset 1514
- Timestamp:
- Nov 17, 2011, 5:41:08 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1511 r1514 257 257 qed. 258 258 259 lemma plus_minus_rearrangement :259 lemma plus_minus_rearrangement_1: 260 260 ∀m, n, o: nat. 261 261 ∀proof_n_m: n < m. … … 300 300 qed. 301 301 302 axiom plus_minus_rearrangement_2: 303 ∀m, n, o: nat. 304 (m - n) + (n - o) = m - o. 305 302 306 example set_program_counter_ignores_clock: 303 307 ∀s: Status. … … 461 465 normalize nodelta; cases addressing_mode 462 466 normalize nodelta; 463 467 [1,2,3,4,8,9,15,16,17,18,19: 468 #assm whd in ⊢ (% → ?) 469 #absurd cases(absurd) 470 |5,6,7,10,11,12,14: 471 whd in ⊢ (% → ?) 472 #absurd cases(absurd) 473 |13: 474 #irrelevant 475 normalize nodelta; 476 >set_program_counter_ignores_clock 477 >set_program_counter_ignores_clock 478 >clock_set_clock // 479 ] 480 |8: cases daemon (* XXX: my god *) 481 |7: #acc_a cases acc_a #addressing_mode 482 normalize nodelta; cases addressing_mode 483 normalize nodelta; 484 [1,2,3,4,8,9,15,16,17,18,19: 485 #assm whd in ⊢ (% → ?) 486 #absurd cases(absurd) 487 |6,7,10,11,12,13,14: 488 whd in ⊢ (% → ?) 489 #absurd cases(absurd) 490 |5: 491 #irrelevant #acc_dptr_acc_pc 492 normalize nodelta; 493 cases daemon (* XXX: my god *) 494 ] 495 ] 496 qed. 464 497 465 498 lemma current_instruction_cost_is_ok: … … 476 509 \snd (fetch (code_memory … s) (program_counter … s))); 477 510 normalize nodelta; 511 whd in match ( 512 execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) 513 (program_counter (BitVectorTrie Byte 16) s))); 514 normalize nodelta; 515 cases (fetch (code_memory (BitVectorTrie Byte 16) s) 516 (program_counter (BitVectorTrie Byte 16) s)); 517 #instr_pc #ticks normalize nodelta; 518 cases (\fst instr_pc) 519 [1: 520 #addr11 normalize nodelta; 521 cases addr11 #addressing_mode 522 cases addressing_mode 523 [1,2,3,4,8,9,15,16,17,19: 524 #assm whd in ⊢ (% → ?) 525 #absurd cases(absurd) 526 |5,6,7,10,11,12,13,14: 527 whd in ⊢ (% → ?) 528 #absurd cases(absurd) 529 |18: 530 #word11 #irrelevant normalize nodelta; 531 >set_program_counter_ignores_clock 532 >write_at_stack_pointer_ignores_clock 533 >set_8051_sfr_ignores_clock 534 >write_at_stack_pointer_ignores_clock 535 >set_8051_sfr_ignores_clock 536 >clock_set_clock 537 >set_program_counter_ignores_clock 538 >commutative_plus 539 <plus_minus 540 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 541 % 542 ] 543 |2: 544 #addr16 cases addr16 #addressing_mode 545 normalize nodelta; cases addressing_mode 546 normalize nodelta; 547 [1,2,3,4,8,9,15,16,17,18: 548 #assm whd in ⊢ (% → ?) 549 #absurd cases(absurd) 550 |5,6,7,10,11,12,13,14: 551 whd in ⊢ (% → ?) 552 #absurd cases(absurd) 553 |19: 554 #addr16 #irrelevant 555 normalize nodelta; 556 >set_program_counter_ignores_clock 557 >write_at_stack_pointer_ignores_clock 558 >set_8051_sfr_ignores_clock 559 >write_at_stack_pointer_ignores_clock 560 >set_8051_sfr_ignores_clock 561 >clock_set_clock 562 >set_program_counter_ignores_clock 563 >commutative_plus 564 <plus_minus 565 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 566 % 567 ] 568 |3: 569 #addr11 cases addr11 #addressing_mode 570 normalize nodelta; cases addressing_mode 571 normalize nodelta; 572 [1,2,3,4,8,9,15,16,17,19: 573 #assm whd in ⊢ (% → ?) 574 #absurd cases(absurd) 575 |5,6,7,10,11,12,13,14: 576 whd in ⊢ (% → ?) 577 #absurd cases(absurd) 578 |18: 579 #word11 #irrelevant 580 normalize nodelta; 581 >set_program_counter_ignores_clock 582 >clock_set_clock 583 >set_program_counter_ignores_clock 584 >commutative_plus 585 <plus_minus 586 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 587 % 588 ] 589 |4: 590 #addr16 cases addr16 #addressing_mode 591 normalize nodelta; cases addressing_mode 592 normalize nodelta; 593 [1,2,3,4,8,9,15,16,17,18: 594 #assm whd in ⊢ (% → ?) 595 #absurd cases(absurd) 596 |5,6,7,10,11,12,13,14: 597 whd in ⊢ (% → ?) 598 #absurd cases(absurd) 599 |19: 600 #word #irrelevant 601 normalize nodelta; 602 >set_program_counter_ignores_clock 603 >clock_set_clock 604 >set_program_counter_ignores_clock 605 >commutative_plus 606 <plus_minus 607 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 608 % 609 ] 610 |5: 611 #relative cases relative #addressing_mode 612 normalize nodelta; cases addressing_mode 613 normalize nodelta; 614 [1,2,3,4,8,9,15,16,18,19: 615 #assm whd in ⊢ (% → ?) 616 #absurd cases(absurd) 617 |5,6,7,10,11,12,13,14: 618 whd in ⊢ (% → ?) 619 #absurd cases(absurd) 620 |17: 621 #byte #irrelevant 622 normalize nodelta; 623 >set_program_counter_ignores_clock 624 >set_program_counter_ignores_clock 625 >clock_set_clock 626 >commutative_plus 627 <plus_minus 628 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 629 % 630 ] 631 |6: 632 #indirect_dptr cases indirect_dptr #addressing_mode 633 normalize nodelta; cases addressing_mode 634 normalize nodelta; 635 [1,2,3,4,8,9,15,16,17,18,19: 636 #assm whd in ⊢ (% → ?) 637 #absurd cases(absurd) 638 |5,6,7,10,11,12,14: 639 whd in ⊢ (% → ?) 640 #absurd cases(absurd) 641 |13: 642 #irrelevant 643 normalize nodelta; 644 >set_program_counter_ignores_clock 645 >set_program_counter_ignores_clock 646 >clock_set_clock 647 >commutative_plus 648 <plus_minus 649 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 650 % 651 ] 652 |7: 653 #acc_a cases acc_a #addressing_mode 654 normalize nodelta; cases addressing_mode 655 normalize nodelta; 656 [1,2,3,4,8,9,15,16,17,18,19: 657 #assm whd in ⊢ (% → ?) 658 #absurd cases(absurd) 659 |6,7,10,11,12,13,14: 660 whd in ⊢ (% → ?) 661 #absurd cases(absurd) 662 |5: 663 #irrelevant #acc_dptr_acc_pc 664 normalize nodelta; 665 cases daemon (* XXX: todo *) 666 ] 667 |8: cases daemon (* XXX: todo *) 668 ] 669 qed. 478 670 479 671 let rec compute_max_trace_label_label_cost_is_ok … … 540 732 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 541 733 sum = pc_after) 542 normalize nodelta; 734 normalize nodelta; #relation_pre_after_fun_call 735 >plus_minus_rearrangement_2 in match ( 736 (clock (BitVectorTrie Byte 16) after_fun_call 737 -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call) 738 +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call) 739 -clock (BitVectorTrie Byte 16) pre_fun_call))); 543 740 >(plus_minus_rearrangement 544 741 (clock (BitVectorTrie Byte 16) after_fun_call) -
src/ASM/Interpret.ma
r1511 r1514 582 582 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 583 583 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 584 let 〈carry, new_addr〉 ≝ half_add ? dptr big_accin584 let new_addr ≝ \snd (half_add ? dptr big_acc) in 585 585 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 586 586 set_8051_sfr ? s SFR_ACC_A result 587 587 | ACC_PC ⇒ λacc_pc: True. 588 588 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 589 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in589 let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in 590 590 (* DPM: Under specified: does the carry from PC incrementation affect the *) 591 591 (* addition of the PC with the DPTR? At the moment, no. *) 592 592 let s ≝ set_program_counter ? s inc_pc in 593 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_accin593 let new_addr ≝ \snd (half_add ? inc_pc big_acc) in 594 594 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 595 595 set_8051_sfr ? s SFR_ACC_A result
Note: See TracChangeset
for help on using the changeset viewer.