- Timestamp:
- Jun 7, 2011, 5:32:30 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r892 r893 694 694 qed. 695 695 696 (* 696 697 lemma andb_elim': 697 698 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true. 698 699 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize // 699 700 qed. 701 *) 700 702 701 703 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) … … 709 711 710 712 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. 711 712 (*713 lemma test:714 ∀pc,i.715 (let assembled ≝ assembly1 i in716 let code_memory ≝ load_code_memory_aux pc assembled in717 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in718 let 〈instr_pc, ticks〉 ≝ fetched in719 eq_instruction (\fst instr_pc)) i = true.720 *)721 713 722 714 lemma test: … … 754 746 whd >eq_instruction_refl >H4 try @eq_bv_refl 755 747 qed. 756 757 758 |*:759 >eq_instruction_refl >H4 @eq_bv_refl760 qed.761 762 763 whd764 [ @(list_addressing_mode_tags_elim_prop … arg) whd try %765 @(list_addressing_mode_tags_elim_prop … arg2) whd try %766 * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)767 whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 >eq_instruction_refl @eq_bv_refl768 |6: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX769 * #H1 * #H2 #H3 whd in H3; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)770 whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 <H3 >eq_instruction_refl @eq_bv_refl771 |7: @(list_addressing_mode_tags_elim_prop … arg) whd try %772 * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)773 |3,5: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX774 775 @split_elim776 777 778 whd in ⊢ (??%?)779 [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX780 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)781 @split_elim #b1 #b2 #EQ >EQ -EQ;782 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)783 whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)784 >lookup_insert_miss try @not_eqvb_SS785 >lookup_insert_miss //786 >lookup_insert_hit787 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)788 >half_add_SO >half_add_SO789 >lookup_insert_miss try @not_eqvb_S790 >lookup_insert_hit791 >lookup_insert_hit792 @eq_instruction_refl793 |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX794 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)795 @split_elim #b1 #b2 #EQ >EQ -EQ;796 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)797 whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)798 >lookup_insert_miss //799 >lookup_insert_hit800 >half_add_SO801 @(bitvector_elim_complete' … b1) @andb_elim' @andb_elim' @andb_elim'802 whd in ⊢ (??%?) normalize in ⊢ (??(?(???(?))%)?) >lookup_insert_hit803 normalize804 (* FALSO!!! AJMP vs ACALL *)805 cases daemon806 | @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX807 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)808 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)809 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)810 >lookup_insert_miss //811 >lookup_insert_hit812 >half_add_SO813 whd in ⊢ (??%?)814 >lookup_insert_hit815 normalize816 @eq_instruction_refl817 | @(list_addressing_mode_tags_elim_prop … arg) whd try %818 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)819 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)820 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)821 >lookup_insert_hit822 >half_add_SO823 normalize824 @eq_instruction_refl825 | @(list_addressing_mode_tags_elim_prop … arg) whd try %826 @(list_addressing_mode_tags_elim_prop … arg2) whd try %827 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)828 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)829 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)830 >lookup_insert_hit831 >half_add_SO832 normalize833 @eq_instruction_refl834 | cases arg -i arg;835 (*836 16,17,18,19,20,28,19837 *)838 [1,2,3: #arg1 #arg2839 @(list_addressing_mode_tags_elim_prop … arg1) whd try %840 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX841 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)842 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)843 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)844 [1,4,5,8,9,12: >lookup_insert_miss //]845 >lookup_insert_hit >half_add_SO846 [1,2,3,4,5,6: whd in ⊢ (??%?) >lookup_insert_hit]847 normalize848 @eq_instruction_refl849 |35,36,37:850 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)851 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)852 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)853 >lookup_insert_hit >half_add_SO854 normalize855 @eq_instruction_refl856 |6,7,8,23,24,25,26,27: #arg1 try #arg2857 @(list_addressing_mode_tags_elim_prop … arg1) whd try %858 try (@(list_addressing_mode_tags_elim_prop … arg2) whd try %)859 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)860 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)861 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)862 >lookup_insert_hit >half_add_SO863 normalize864 @eq_instruction_refl865 |9,10,14,15,31,32: #arg1866 @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX867 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)868 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)869 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)870 >lookup_insert_miss //871 >lookup_insert_hit872 >half_add_SO873 whd in ⊢ (??%?)874 >lookup_insert_hit875 normalize876 @eq_instruction_refl877 |33,34: #arg1 #arg2878 @(list_addressing_mode_tags_elim_prop … arg1) whd try %879 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2880 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)881 whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)882 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)883 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)884 [>lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)885 [>lookup_insert_hit]886 normalize887 @eq_instruction_refl888 |4,5,21,22,30: #arg1889 @(list_addressing_mode_tags_elim_prop … arg1) whd try % try #XX1890 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)891 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)892 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)893 [1,6,12,15,17: >lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)894 [1,2,3,4,5: >lookup_insert_hit] normalize @eq_instruction_refl895 |11,12,13: #arg1 #arg2896 @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX1897 @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2898 whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)899 whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)900 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)901 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)902 >lookup_insert_miss try @not_eqvb_SS903 >lookup_insert_miss //904 >lookup_insert_hit905 >half_add_SO906 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)907 >half_add_SO908 >lookup_insert_hit909 >lookup_insert_miss //910 >lookup_insert_hit911 normalize912 @eq_instruction_refl913 ]914 qed.915 748 916 749 (* This establishes the correspondence between pseudo program counters and … … 1547 1380 hd = byte ∧ encoding_check' code_memory new_pc tl 1548 1381 ]. 1549 1550 (* prove later *)1551 axiom test:1552 ∀pc: Word.1553 ∀code_memory: BitVectorTrie Byte 16.1554 ∀i: instruction.1555 let assembled ≝ assembly1 i in1556 encoding_check' code_memory pc assembled →1557 let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in1558 let 〈instr, pc〉 ≝ instr_pc in1559 instr = i.1560 1382 1561 1383 lemma main_thm:
Note: See TracChangeset
for help on using the changeset viewer.