- Timestamp:
- Jun 5, 2011, 2:04:22 AM (10 years ago)
- File:
-
- 1 edited
-
src/ASM/AssemblyProof.ma (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r884 r885 443 443 true.*) 444 444 axiom eq_instruction: instruction → instruction → bool. 445 axiom eq_instruction_refl: ∀i. eq_instruction i i = true. 446 445 447 let rec vect_member 446 448 (A: Type[0]) (n: nat) (eq: A → A → bool) … … 717 719 >lookup_insert_hit 718 720 >lookup_insert_hit 719 (* REFL MISSING *) 720 cases daemon 721 @eq_instruction_refl 721 722 |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 722 723 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) … … 726 727 >lookup_insert_miss // 727 728 >lookup_insert_hit 728 generalize in match b1 @(bitvector_elim_complete') 729 @andb_elim' @andb_elim' @andb_elim' whd in ⊢ (??%?) 730 >half_add_SO >lookup_insert_hit normalize 729 >half_add_SO 730 @(bitvector_elim_complete' … b1) @andb_elim' @andb_elim' @andb_elim' 731 whd in ⊢ (??%?) normalize in ⊢ (??(?(???(?))%)?) >lookup_insert_hit 732 normalize 731 733 (* FALSO!!! AJMP vs ACALL *) 732 733 734 whd in ⊢ (??%?) whd in ⊢ (??(match % with [ _ ⇒ % | _ ⇒ ?])?) 735 check andb_elim. 736 (λV.(let 〈instr_pc,ticks〉 ≝ 737 fetch0 738 (insert Byte 16 (bitvector_of_nat 16 (S pc)) b2 739 (insert Byte 16 (bitvector_of_nat 16 pc) 740 (V@@[[true; false; false; false; true]]) (Stub Byte 16))) 741 〈\snd (half_add 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 1)), 742 V@@[[true; false; false; false; true]]〉 in 743 eq_instruction (\fst instr_pc)) 744 (ACALL (ADDR11 (V@@b2)))) ?) 745 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 734 cases daemon 735 | @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 736 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 737 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 738 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 739 >lookup_insert_miss // 740 >lookup_insert_hit 746 741 >half_add_SO 747 748 749 750 751 [2: #addr whd in ⊢ (??%?) 752 753 @ (instruction_elim_complete ) 754 | @ zero 742 whd in ⊢ (??%?) 743 >lookup_insert_hit 744 normalize 745 @eq_instruction_refl 746 | @(list_addressing_mode_tags_elim_prop … arg) whd try % 747 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 748 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 749 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 750 >lookup_insert_hit 751 >half_add_SO 752 normalize 753 @eq_instruction_refl 754 | @(list_addressing_mode_tags_elim_prop … arg) whd try % 755 @(list_addressing_mode_tags_elim_prop … arg2) whd try % 756 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 757 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 758 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 759 >lookup_insert_hit 760 >half_add_SO 761 normalize 762 @eq_instruction_refl 763 | cases arg -i arg; 764 [1,2,3: #arg1 #arg2 765 @(list_addressing_mode_tags_elim_prop … arg1) whd try % 766 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX 767 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 768 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 769 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 770 [1,4,5,8,9,12: >lookup_insert_miss //] 771 >lookup_insert_hit >half_add_SO 772 [1,2,3,4,5,6: whd in ⊢ (??%?) >lookup_insert_hit] 773 normalize 774 @eq_instruction_refl 775 |35,36,37: 776 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 777 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 778 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 779 >lookup_insert_hit >half_add_SO 780 normalize 781 @eq_instruction_refl 782 |6,7,8,23,24,25,26,27: #arg1 try #arg2 783 @(list_addressing_mode_tags_elim_prop … arg1) whd try % 784 try (@(list_addressing_mode_tags_elim_prop … arg2) whd try %) 785 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 786 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 787 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 788 >lookup_insert_hit >half_add_SO 789 normalize 790 @eq_instruction_refl 791 |9,10,14,15,31,32: #arg1 792 @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX 793 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 794 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 795 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 796 >lookup_insert_miss // 797 >lookup_insert_hit 798 >half_add_SO 799 whd in ⊢ (??%?) 800 >lookup_insert_hit 801 normalize 802 @eq_instruction_refl 803 |33,34: #arg1 #arg2 804 @(list_addressing_mode_tags_elim_prop … arg1) whd try % 805 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2 806 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 807 whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?) 808 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 809 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 810 [>lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?) 811 [>lookup_insert_hit] 812 normalize 813 @eq_instruction_refl 814 |4,5,21,22,30: #arg1 815 @(list_addressing_mode_tags_elim_prop … arg1) whd try % try #XX1 816 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 817 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 818 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 819 [1,6,12,15,17: >lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?) 820 [1,2,3,4,5: >lookup_insert_hit] normalize @eq_instruction_refl 821 |11,12,13: #arg1 #arg2 822 @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX1 823 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2 824 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?) 825 whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?) 826 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 827 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 828 >lookup_insert_miss try @not_eqvb_SS 829 >lookup_insert_miss // 830 >lookup_insert_hit 831 >half_add_SO 832 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 833 >half_add_SO 834 >lookup_insert_hit 835 >lookup_insert_miss try @not_eqvb_SS 836 >lookup_insert_hit 837 normalize 838 @eq_instruction_refl 755 839 ] 756 normalize 757 840 qed. 758 841 759 842 (* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset
for help on using the changeset viewer.
