 Timestamp:
 Nov 22, 2011, 7:24:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1527 r1533 555 555 qed. 556 556 557 (*CSC: indexing diverges, why?*) 558 example set_program_counter_ignores_clock: 559 ∀M.∀s: PreStatus M. 560 ∀pc: Word. 561 clock … (set_program_counter … s pc) = clock … s. 562 // 563 qed. 564 565 lemma set_8051_sfr_ignores_clock: 566 ∀M.∀s: PreStatus M. 567 ∀sfr: SFR8051. 568 ∀v: Byte. 569 clock … (set_8051_sfr ? s sfr v) = clock … s. 570 // 571 qed. 572 573 lemma write_at_stack_pointer_ignores_clock: 574 ∀M.∀s: PreStatus M. 575 ∀sp: Byte. 576 clock … (write_at_stack_pointer … s sp) = clock … s. 577 #M #s #sp 578 change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?) 579 in match (write_at_stack_pointer ???); 580 normalize nodelta 581 cases(split bool 4 4 (get_8051_sfr … s SFR_SP)) 582 #nu #nl normalize nodelta; 583 cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) 584 [ normalize nodelta; % 585  normalize nodelta; % 586 ] 587 qed. 588 557 589 definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝ 558 590 λs0,instr_pc_ticks. … … 567 599  _ ⇒ λabsd. ⊥ 568 600 ] (subaddressing_modein … x)) instr s 569  ACALL addr ⇒ ?(*601  ACALL addr ⇒ 570 602 let s ≝ set_clock ? s (ticks + clock ? s) in 571 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ?with603 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 572 604 [ ADDR11 a ⇒ λaddr11: True. 573 605 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 574 606 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 575 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 576 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 607 let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 577 608 let s ≝ write_at_stack_pointer ? s pc_bl in 578 609 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 579 610 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 580 611 let s ≝ write_at_stack_pointer ? s pc_bu in 581 let thr ≝ \fst (split ? 3 8 a) in 582 let eig ≝ \snd (split ? 3 8 a) in 583 let fiv ≝ \fst (split ? 5 3 pc_bu) in 584 let thr' ≝ \snd (split ? 5 3 pc_bu) in 612 let 〈thr,eig〉 ≝ split ? 3 8 a in 613 let 〈fiv,thr'〉 ≝ split ? 5 3 pc_bu in 585 614 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 586 615 set_program_counter ? s new_addr 587 616  _ ⇒ λother: False. ⊥ 588 ] (subaddressing_modein … addr) *)617 ] (subaddressing_modein … addr) 589 618  LCALL addr ⇒ 590 619 let s ≝ set_clock ? s (ticks + clock ? s) in 591 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ?with620 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 592 621 [ ADDR16 a ⇒ λaddr16: True. 593 622 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 594 623 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 595 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 596 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 624 let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 597 625 let s ≝ write_at_stack_pointer ? s pc_bl in 598 626 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in … … 604 632  MOVC addr1 addr2 ⇒ 605 633 let s ≝ set_clock ? s (ticks + clock ? s) in 606 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ?with634 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 607 635 [ ACC_DPTR ⇒ λacc_dptr: True. 608 636 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 631 659  LJMP addr ⇒ 632 660 let s ≝ set_clock ? s (ticks + clock ? s) in 633 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ?with661 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 634 662 [ ADDR16 a ⇒ λaddr16: True. 635 663 set_program_counter ? s a … … 638 666  SJMP addr ⇒ 639 667 let s ≝ set_clock ? s (ticks + clock ? s) in 640 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ?with668 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 641 669 [ RELATIVE r ⇒ λrelative: True. 642 670 let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in … … 646 674  AJMP addr ⇒ 647 675 let s ≝ set_clock ? s (ticks + clock ? s) in 648 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ?with676 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 649 677 [ ADDR11 a ⇒ λaddr11: True. 650 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 651 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 652 let nu ≝ \fst (split ? 4 4 pc_bu) in 653 let nl ≝ \snd (split ? 4 4 pc_bu) in 678 let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 679 let 〈nu,nl〉 ≝ split ? 4 4 pc_bu in 654 680 let bit ≝ get_index' ? O ? nl in 655 let relevant1 ≝ \fst (split ? 3 8 a) in 656 let relevant2 ≝ \snd (split ? 3 8 a) in 681 let 〈relevant1,relevant2〉 ≝ split ? 3 8 a in 657 682 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 658 683 let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in … … 660 685  _ ⇒ λother: False. ⊥ 661 686 ] (subaddressing_modein … addr) 662 ]. 663 try assumption 664 try ( 665 normalize 666 repeat (@ (le_S_S)) 667 @ (le_O_n) 668 ) 669 try ( 670 @ (execute_1_technical … (subaddressing_modein …)) 671 @ I 672 ) 673 try ( 674 normalize 675 @ I 676 ) 677 qed. 678 679 definition execute_1: Status → Status ≝ 687 ]. (*5s*) 688 try assumption (*12s*) 689 [1,2: >set_program_counter_ignores_clock normalize nodelta 690 >write_at_stack_pointer_ignores_clock 691 >set_8051_sfr_ignores_clock 692 >write_at_stack_pointer_ignores_clock 693 >set_8051_sfr_ignores_clock 694 change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/ 695 3,4,5,6: >set_program_counter_ignores_clock normalize nodelta 696 change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/ 697 7,8: >set_8051_sfr_ignores_clock normalize nodelta change with (? ≤ ?+?) 698 >set_program_counter_ignores_clock /by/] 699 qed. 700 701 definition execute_1: ∀s:Status. Σs':Status. clock … s ≤ clock … s' ≝ 680 702 λs: Status. 681 703 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset
for help on using the changeset viewer.