Changeset 1971 for src/ASM/Interpret.ma
 Timestamp:
 May 20, 2012, 10:34:31 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1969 r1971 112 112 include alias "ASM/BitVectorTrie.ma". 113 113 114 definition execute_1_preinstruction ':114 definition execute_1_preinstruction: 115 115 ∀ticks: nat × nat. 116 116 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a. 117 ∀s: PreStatus m cm. 118 Σs': PreStatus m cm. 119 And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 120 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝ 117 ∀s: PreStatus m cm. PreStatus m cm ≝ 121 118 λticks: nat × nat. 122 119 λa, m: Type[0]. λcm. … … 126 123 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 127 124 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 128 match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. 129 And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 130 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with 125 match instr in preinstruction return λx. x = instr → PreStatus m cm with 131 126 [ ADD addr1 addr2 ⇒ λinstr_refl. 132 127 let s ≝ add_ticks1 s in … … 533 528 @I 534 529 ) (*66s*) 530 qed. 531 532 definition execute_1_preinstruction_ok': 533 ∀ticks: nat × nat. 534 ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a. 535 ∀s: PreStatus m cm. 536 Σs': PreStatus m cm. 537 (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in 538 (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 539 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝ 540 λticks: nat × nat. 541 λa, m: Type[0]. λcm. 542 λaddr_of: a → PreStatus m cm → Word. 543 λinstr: preinstruction a. 544 λs: PreStatus m cm. 545 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 546 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 547 match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. 548 ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 549 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with 550 [ ADD addr1 addr2 ⇒ λinstr_refl. 551 let s ≝ add_ticks1 s in 552 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 553 (get_arg_8 … s false addr2) false in 554 let cy_flag ≝ get_index' ? O ? flags in 555 let ac_flag ≝ get_index' ? 1 ? flags in 556 let ov_flag ≝ get_index' ? 2 ? flags in 557 let s ≝ set_arg_8 … s ACC_A result in 558 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 559  ADDC addr1 addr2 ⇒ λinstr_refl. 560 let s ≝ add_ticks1 s in 561 let old_cy_flag ≝ get_cy_flag ?? s in 562 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 563 (get_arg_8 … s false addr2) old_cy_flag in 564 let cy_flag ≝ get_index' ? O ? flags in 565 let ac_flag ≝ get_index' ? 1 ? flags in 566 let ov_flag ≝ get_index' ? 2 ? flags in 567 let s ≝ set_arg_8 … s ACC_A result in 568 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 569  SUBB addr1 addr2 ⇒ λinstr_refl. 570 let s ≝ add_ticks1 s in 571 let old_cy_flag ≝ get_cy_flag ?? s in 572 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 573 (get_arg_8 … s false addr2) old_cy_flag in 574 let cy_flag ≝ get_index' ? O ? flags in 575 let ac_flag ≝ get_index' ? 1 ? flags in 576 let ov_flag ≝ get_index' ? 2 ? flags in 577 let s ≝ set_arg_8 … s ACC_A result in 578 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 579  ANL addr ⇒ λinstr_refl. 580 let s ≝ add_ticks1 s in 581 match addr with 582 [ inl l ⇒ 583 match l with 584 [ inl l' ⇒ 585 let 〈addr1, addr2〉 ≝ l' in 586 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 587 set_arg_8 … s addr1 and_val 588  inr r ⇒ 589 let 〈addr1, addr2〉 ≝ r in 590 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 591 set_arg_8 … s addr1 and_val 592 ] 593  inr r ⇒ 594 let 〈addr1, addr2〉 ≝ r in 595 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 596 set_flags … s and_val (None ?) (get_ov_flag ?? s) 597 ] 598  ORL addr ⇒ λinstr_refl. 599 let s ≝ add_ticks1 s in 600 match addr with 601 [ inl l ⇒ 602 match l with 603 [ inl l' ⇒ 604 let 〈addr1, addr2〉 ≝ l' in 605 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 606 set_arg_8 … s addr1 or_val 607  inr r ⇒ 608 let 〈addr1, addr2〉 ≝ r in 609 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 610 set_arg_8 … s addr1 or_val 611 ] 612  inr r ⇒ 613 let 〈addr1, addr2〉 ≝ r in 614 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 615 set_flags … s or_val (None ?) (get_ov_flag … s) 616 ] 617  XRL addr ⇒ λinstr_refl. 618 let s ≝ add_ticks1 s in 619 match addr with 620 [ inl l' ⇒ 621 let 〈addr1, addr2〉 ≝ l' in 622 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 623 set_arg_8 … s addr1 xor_val 624  inr r ⇒ 625 let 〈addr1, addr2〉 ≝ r in 626 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 627 set_arg_8 … s addr1 xor_val 628 ] 629  INC addr ⇒ λinstr_refl. 630 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with 631 [ ACC_A ⇒ λacc_a: True. λEQaddr. 632 let s' ≝ add_ticks1 s in 633 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 634 set_arg_8 … s' ACC_A result 635  REGISTER r ⇒ λregister: True. λEQaddr. 636 let s' ≝ add_ticks1 s in 637 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 638 set_arg_8 … s' (REGISTER r) result 639  DIRECT d ⇒ λdirect: True. λEQaddr. 640 let s' ≝ add_ticks1 s in 641 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 642 set_arg_8 … s' (DIRECT d) result 643  INDIRECT i ⇒ λindirect: True. λEQaddr. 644 let s' ≝ add_ticks1 s in 645 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 646 set_arg_8 … s' (INDIRECT i) result 647  DPTR ⇒ λdptr: True. λEQaddr. 648 let s' ≝ add_ticks1 s in 649 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 650 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 651 let s ≝ set_8051_sfr … s' SFR_DPL bl in 652 set_8051_sfr … s' SFR_DPH bu 653  _ ⇒ λother: False. ⊥ 654 ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr)) 655  NOP ⇒ λinstr_refl. 656 let s ≝ add_ticks2 s in 657 s 658  DEC addr ⇒ λinstr_refl. 659 let s ≝ add_ticks1 s in 660 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 661 set_arg_8 … s addr result 662  MUL addr1 addr2 ⇒ λinstr_refl. 663 let s ≝ add_ticks1 s in 664 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 665 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 666 let product ≝ acc_a_nat * acc_b_nat in 667 let ov_flag ≝ product ≥ 256 in 668 let low ≝ bitvector_of_nat 8 (product mod 256) in 669 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 670 let s ≝ set_8051_sfr … s SFR_ACC_A low in 671 set_8051_sfr … s SFR_ACC_B high 672  DIV addr1 addr2 ⇒ λinstr_refl. 673 let s ≝ add_ticks1 s in 674 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 675 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 676 match acc_b_nat with 677 [ O ⇒ set_flags … s false (None Bit) true 678  S o ⇒ 679 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 680 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 681 let s ≝ set_8051_sfr … s SFR_ACC_A q in 682 let s ≝ set_8051_sfr … s SFR_ACC_B r in 683 set_flags … s false (None Bit) false 684 ] 685  DA addr ⇒ λinstr_refl. 686 let s ≝ add_ticks1 s in 687 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 688 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 689 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 690 let cy_flag ≝ get_index' ? O ? flags in 691 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in 692 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 693 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 694 let new_acc ≝ nu @@ acc_nl' in 695 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 696 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 697 else 698 s 699 else 700 s 701  CLR addr ⇒ λinstr_refl. 702 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with 703 [ ACC_A ⇒ λacc_a: True. λEQaddr. 704 let s ≝ add_ticks1 s in 705 set_arg_8 … s ACC_A (zero 8) 706  CARRY ⇒ λcarry: True. λEQaddr. 707 let s ≝ add_ticks1 s in 708 set_arg_1 … s CARRY false 709  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 710 let s ≝ add_ticks1 s in 711 set_arg_1 … s (BIT_ADDR b) false 712  _ ⇒ λother: False. ⊥ 713 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 714  CPL addr ⇒ λinstr_refl. 715 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with 716 [ ACC_A ⇒ λacc_a: True. λEQaddr. 717 let s ≝ add_ticks1 s in 718 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 719 let new_acc ≝ negation_bv ? old_acc in 720 set_8051_sfr … s SFR_ACC_A new_acc 721  CARRY ⇒ λcarry: True. λEQaddr. 722 let s ≝ add_ticks1 s in 723 let old_cy_flag ≝ get_arg_1 … s CARRY true in 724 let new_cy_flag ≝ ¬old_cy_flag in 725 set_arg_1 … s CARRY new_cy_flag 726  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 727 let s ≝ add_ticks1 s in 728 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 729 let new_bit ≝ ¬old_bit in 730 set_arg_1 … s (BIT_ADDR b) new_bit 731  _ ⇒ λother: False. ? 732 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 733  SETB b ⇒ λinstr_refl. 734 let s ≝ add_ticks1 s in 735 set_arg_1 … s b false 736  RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 737 let s ≝ add_ticks1 s in 738 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 739 let new_acc ≝ rotate_left … 1 old_acc in 740 set_8051_sfr … s SFR_ACC_A new_acc 741  RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 742 let s ≝ add_ticks1 s in 743 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 744 let new_acc ≝ rotate_right … 1 old_acc in 745 set_8051_sfr … s SFR_ACC_A new_acc 746  RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 747 let s ≝ add_ticks1 s in 748 let old_cy_flag ≝ get_cy_flag ?? s in 749 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 750 let new_cy_flag ≝ get_index' ? O ? old_acc in 751 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 752 let s ≝ set_arg_1 … s CARRY new_cy_flag in 753 set_8051_sfr … s SFR_ACC_A new_acc 754  RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 755 let s ≝ add_ticks1 s in 756 let old_cy_flag ≝ get_cy_flag ?? s in 757 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 758 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 759 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 760 let s ≝ set_arg_1 … s CARRY new_cy_flag in 761 set_8051_sfr … s SFR_ACC_A new_acc 762  SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 763 let s ≝ add_ticks1 s in 764 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 765 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 766 let new_acc ≝ nl @@ nu in 767 set_8051_sfr … s SFR_ACC_A new_acc 768  PUSH addr ⇒ λinstr_refl. 769 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with 770 [ DIRECT d ⇒ λdirect: True. λEQaddr. 771 let s ≝ add_ticks1 s in 772 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 773 let s ≝ set_8051_sfr … s SFR_SP new_sp in 774 write_at_stack_pointer … s d 775  _ ⇒ λother: False. ⊥ 776 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 777  POP addr ⇒ λinstr_refl. 778 let s ≝ add_ticks1 s in 779 let contents ≝ read_at_stack_pointer ?? s in 780 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 781 let s ≝ set_8051_sfr … s SFR_SP new_sp in 782 set_arg_8 … s addr contents 783  XCH addr1 addr2 ⇒ λinstr_refl. 784 let s ≝ add_ticks1 s in 785 let old_addr ≝ get_arg_8 … s false addr2 in 786 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 787 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 788 set_arg_8 … s addr2 old_acc 789  XCHD addr1 addr2 ⇒ λinstr_refl. 790 let s ≝ add_ticks1 s in 791 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 792 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 793 let new_acc ≝ acc_nu @@ arg_nl in 794 let new_arg ≝ arg_nu @@ acc_nl in 795 let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in 796 set_arg_8 … s addr2 new_arg 797  RET ⇒ λinstr_refl. 798 let s ≝ add_ticks1 s in 799 let high_bits ≝ read_at_stack_pointer ?? s in 800 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 801 let s ≝ set_8051_sfr … s SFR_SP new_sp in 802 let low_bits ≝ read_at_stack_pointer ?? s in 803 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 804 let s ≝ set_8051_sfr … s SFR_SP new_sp in 805 let new_pc ≝ high_bits @@ low_bits in 806 set_program_counter … s new_pc 807  RETI ⇒ λinstr_refl. 808 let s ≝ add_ticks1 s in 809 let high_bits ≝ read_at_stack_pointer ?? s in 810 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 811 let s ≝ set_8051_sfr … s SFR_SP new_sp in 812 let low_bits ≝ read_at_stack_pointer ?? s in 813 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 814 let s ≝ set_8051_sfr … s SFR_SP new_sp in 815 let new_pc ≝ high_bits @@ low_bits in 816 set_program_counter … s new_pc 817  MOVX addr ⇒ λinstr_refl. 818 let s ≝ add_ticks1 s in 819 (* DPM: only copies  doesn't affect I/O *) 820 match addr with 821 [ inl l ⇒ 822 let 〈addr1, addr2〉 ≝ l in 823 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 824  inr r ⇒ 825 let 〈addr1, addr2〉 ≝ r in 826 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 827 ] 828  MOV addr ⇒ λinstr_refl. 829 let s ≝ add_ticks1 s in 830 match addr with 831 [ inl l ⇒ 832 match l with 833 [ inl l' ⇒ 834 match l' with 835 [ inl l'' ⇒ 836 match l'' with 837 [ inl l''' ⇒ 838 match l''' with 839 [ inl l'''' ⇒ 840 let 〈addr1, addr2〉 ≝ l'''' in 841 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 842  inr r'''' ⇒ 843 let 〈addr1, addr2〉 ≝ r'''' in 844 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 845 ] 846  inr r''' ⇒ 847 let 〈addr1, addr2〉 ≝ r''' in 848 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 849 ] 850  inr r'' ⇒ 851 let 〈addr1, addr2〉 ≝ r'' in 852 set_arg_16 … s (get_arg_16 … s addr2) addr1 853 ] 854  inr r ⇒ 855 let 〈addr1, addr2〉 ≝ r in 856 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 857 ] 858  inr r ⇒ 859 let 〈addr1, addr2〉 ≝ r in 860 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 861 ] 862  JC addr ⇒ λinstr_refl. 863 if get_cy_flag ?? s then 864 let s ≝ add_ticks1 s in 865 set_program_counter … s (addr_of addr s) 866 else 867 let s ≝ add_ticks2 s in 868 s 869  JNC addr ⇒ λinstr_refl. 870 if ¬(get_cy_flag ?? s) then 871 let s ≝ add_ticks1 s in 872 set_program_counter … s (addr_of addr s) 873 else 874 let s ≝ add_ticks2 s in 875 s 876  JB addr1 addr2 ⇒ λinstr_refl. 877 if get_arg_1 … s addr1 false then 878 let s ≝ add_ticks1 s in 879 set_program_counter … s (addr_of addr2 s) 880 else 881 let s ≝ add_ticks2 s in 882 s 883  JNB addr1 addr2 ⇒ λinstr_refl. 884 if ¬(get_arg_1 … s addr1 false) then 885 let s ≝ add_ticks1 s in 886 set_program_counter … s (addr_of addr2 s) 887 else 888 let s ≝ add_ticks2 s in 889 s 890  JBC addr1 addr2 ⇒ λinstr_refl. 891 let s ≝ set_arg_1 … s addr1 false in 892 if get_arg_1 … s addr1 false then 893 let s ≝ add_ticks1 s in 894 set_program_counter … s (addr_of addr2 s) 895 else 896 let s ≝ add_ticks2 s in 897 s 898  JZ addr ⇒ λinstr_refl. 899 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 900 let s ≝ add_ticks1 s in 901 set_program_counter … s (addr_of addr s) 902 else 903 let s ≝ add_ticks2 s in 904 s 905  JNZ addr ⇒ λinstr_refl. 906 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 907 let s ≝ add_ticks1 s in 908 set_program_counter … s (addr_of addr s) 909 else 910 let s ≝ add_ticks2 s in 911 s 912  CJNE addr1 addr2 ⇒ λinstr_refl. 913 match addr1 with 914 [ inl l ⇒ 915 let 〈addr1, addr2'〉 ≝ l in 916 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 917 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 918 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 919 let s ≝ add_ticks1 s in 920 let s ≝ set_program_counter … s (addr_of addr2 s) in 921 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 922 else 923 let s ≝ add_ticks2 s in 924 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 925  inr r' ⇒ 926 let 〈addr1, addr2'〉 ≝ r' in 927 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 928 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 929 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 930 let s ≝ add_ticks1 s in 931 let s ≝ set_program_counter … s (addr_of addr2 s) in 932 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 933 else 934 let s ≝ add_ticks2 s in 935 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 936 ] 937  DJNZ addr1 addr2 ⇒ λinstr_refl. 938 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 939 let s ≝ set_arg_8 … s addr1 result in 940 if ¬(eq_bv ? result (zero 8)) then 941 let s ≝ add_ticks1 s in 942 set_program_counter … s (addr_of addr2 s) 943 else 944 let s ≝ add_ticks2 s in 945 s 946 ] (refl … instr). 947 try (cases(other)) 948 try assumption (*20s*) 949 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 950 try ( 951 @(execute_1_technical … (subaddressing_modein …)) 952 @I 953 ) (*66s*) 954 whd in match execute_1_preinstruction; 535 955 normalize nodelta % 536 try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) 537 try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd)) 956 [21,22,23,24: (* DIV *) 957 normalize nodelta in p; 958 7,8,9,10,11,12,13,14,15,16, (* INC *) 959 71,72,73,74,75,76, (* CLR *) 960 77,78,79,80,81,82, (* CPL *) 961 99,100: (* PUSH *) 962 lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b 963 93,94: (* MOV *) 964 cases addr * normalize nodelta 965 [1,2,4,5: * normalize nodelta 966 [1,2,4,5: * normalize nodelta 967 [1,2,4,5: * normalize nodelta 968 [1,2,4,5: * normalize nodelta ]]]] 969 #arg1 #arg2 970 65,66, (* ANL *) 971 67,68, (* ORL *) 972 95,96: (* MOVX*) 973 cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta 974 59,60: (* CJNE *) 975 cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta 976 cases (¬(eq_bv ???)) normalize nodelta 977 69,70: (* XRL *) 978 cases addr normalize nodelta * #addr1 #addr2 normalize nodelta 979 ] 980 try (>p normalize nodelta 981 try (>p1 normalize nodelta 982 try (>p2 normalize nodelta 983 try (>p3 normalize nodelta 984 try (>p4 normalize nodelta 985 try (>p5 normalize nodelta)))))) 986 try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) 987 try (change with (cl_return = cl_other → ?) #absurd destruct(absurd)) 538 988 try (@or_introl //) 539 989 try (@or_intror //) 540 #_ /demod/ % 541 qed. 542 543 definition execute_1_preinstruction: 544 ∀ticks: nat × nat. 545 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 546 PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'. 547 990 try (#_ /demod/ %) 991 try (#_ //) 992 [ <set_arg_8_ok @or_introl // 993 *: <set_arg_1_ok @or_introl // ] 994 qed. 995 548 996 lemma execute_1_preinstruction_ok: 549 997 ∀ticks,a,m,cm,f,i,s. … … 551 999 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧ 552 1000 (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s). 553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi21001 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) // 554 1002 qed. 555 1003
Note: See TracChangeset
for help on using the changeset viewer.