Changeset 2183
 Timestamp:
 Jul 13, 2012, 5:03:15 PM (5 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2181 r2183 191 191 qed. 192 192 193 lemma match_nat_status_of_pseudo_status: 194 ∀M, cm, sigma, policy, s, s', s'', s'''. 195 ∀n, n': nat. 196 n = n' → 197 status_of_pseudo_status M cm s' sigma policy = s → 198 status_of_pseudo_status M cm s''' sigma policy = s'' → 199 match n with [ O ⇒ s  S n' ⇒ s'' ] = 200 status_of_pseudo_status M cm (match n' with [ O ⇒ s'  S n'' ⇒ s''']) sigma policy. 201 #M #cm #sigma #policy #s #s' #s'' #s''' #n #n' 202 #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl' 203 cases n normalize nodelta try % #n' % 204 qed. 205 193 206 (* XXX: copied from Test.ma *) 194 207 lemma let_pair_in_status_of_pseudo_status: … … 210 223 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl 211 224 destruct(destruct_refl) /2/ 225 qed. 226 227 lemma match_nat_replace: 228 ∀l, o, p, r, o', p': nat. 229 l ≃ r → 230 o ≃ o' → 231 p ≃ p' → 232 match l with [ O ⇒ o  S n ⇒ p ] = match r with [ O ⇒ o'  S n' ⇒ p' ]. 233 #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl % 212 234 qed. 213 235 … … 238 260 ∀fetch_pseudo_refl: \fst (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr. 239 261 ∀ticks: nat × nat. 240 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_ datalabels sigma policy ppc (Instruction instr).262 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr). 241 263 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 242 264 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). … … 669 691 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 670 692 whd in match execute_1_preinstruction; normalize nodelta 671 672 (* [31,32: (* DJNZ *) 673 (* XXX: work on the right hand side *) 674 >p normalize nodelta >p1 normalize nodelta 675 (* XXX: switch to the left hand side *) 676 >EQP P normalize nodelta 677 #sigma_increment_commutation #maps_assm #fetch_many_assm 678 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 679 <EQppc in fetch_many_assm; 680 whd in match (short_jump_cond ??); 681 @pair_elim #sj_possible #disp 682 @pair_elim #result #flags #sub16_refl 683 @pair_elim #upper #lower #vsplit_refl 684 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 685 #sj_possible_pair destruct(sj_possible_pair) 686 >p1 normalize nodelta 687 [1,3: 688 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 689 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 690 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 691 whd in ⊢ (??%?); 692 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 693 lapply maps_assm whd in ⊢ (??%? → ?); 694 inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta 695 [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl M' 696 (* XXX: work on the left hand side *) 697 @(pair_replace ?????????? p) normalize nodelta 698 [1,3: 699 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) 700 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 701 >(get_arg_8_set_program_counter … true addr1) 702 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 703 @get_arg_8_pseudo_addressing_mode_ok assumption 704 2,4: 705 >p1 normalize nodelta >EQs 706 alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)". 707 >set_program_counter_status_of_pseudo_status 708 whd in ⊢ (??%%); 709 @split_eq_status 710 [1,10: 711 whd in ⊢ (??%%); >set_arg_8_set_program_counter 712 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 713 >low_internal_ram_set_program_counter 714 [1: 715 >low_internal_ram_set_program_counter 716 (* XXX: ??? *) 717 2: 718 >low_internal_ram_set_clock 719 (* XXX: ??? *) 720 ] 721 2,11: 722 whd in ⊢ (??%%); >set_arg_8_set_program_counter 723 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 724 >high_internal_ram_set_program_counter 725 [1: 726 >high_internal_ram_set_program_counter 727 (* XXX: ??? *) 728 2: 729 >high_internal_ram_set_clock 730 (* XXX: ??? *) 731 ] 732 3,12: 733 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); 734 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 735 >(external_ram_set_arg_8 ??? addr1) 736 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 737 4,13: 738 whd in ⊢ (??%%); >EQaddr_of normalize nodelta 739 [1: 740 >program_counter_set_program_counter 741 >set_arg_8_set_program_counter 742 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 743 >set_clock_set_program_counter >program_counter_set_program_counter 744 change with (add ??? = ?) 745 (* XXX: ??? *) 746 2: 747 >set_arg_8_set_program_counter 748 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 749 >program_counter_set_program_counter 750 >set_arg_8_set_program_counter 751 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 752 >set_clock_set_program_counter >program_counter_set_program_counter 753 >sigma_increment_commutation <EQppc 754 whd in match (assembly_1_pseudoinstruction ??????); 755 whd in match (expand_pseudo_instruction ??????); 756 (* XXX: ??? *) 757 ] 758 5,14: 759 whd in match (special_function_registers_8051 ???); 760 [1: 761 >special_function_registers_8051_set_program_counter 762 >special_function_registers_8051_set_clock 763 >set_arg_8_set_program_counter in ⊢ (???%); 764 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 765 >special_function_registers_8051_set_program_counter 766 >set_arg_8_set_program_counter 767 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 768 >special_function_registers_8051_set_program_counter 769 @special_function_registers_8051_set_arg_8 assumption 770 2: 771 >special_function_registers_8051_set_clock 772 >set_arg_8_set_program_counter 773 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 774 >set_arg_8_set_program_counter 775 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 776 >special_function_registers_8051_set_program_counter 777 >special_function_registers_8051_set_program_counter 778 @special_function_registers_8051_set_arg_8 assumption 779 ] 780 6,15: 781 whd in match (special_function_registers_8052 ???); 782 whd in match (special_function_registers_8052 ???) in ⊢ (???%); 783 [1: 784 >set_arg_8_set_program_counter 785 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 786 >set_arg_8_set_program_counter 787 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 788 >special_function_registers_8052_set_program_counter 789 >special_function_registers_8052_set_program_counter 790 @special_function_registers_8052_set_arg_8 assumption 791 2: 792 whd in ⊢ (??%%); 793 >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption 794 ] 795 (* XXX: we need special_function_registers_8052_set_arg_8 *) 796 7,16: 797 whd in match (p1_latch ???); 798 whd in match (p1_latch ???) in ⊢ (???%); 799 (* XXX: we need p1_latch_8052_set_arg_8 *) 800 8,17: 801 whd in match (p3_latch ???); 802 whd in match (p3_latch ???) in ⊢ (???%); 803 (* XXX: we need p3_latch_8052_set_arg_8 *) 804 9: 805 >clock_set_clock 806 >clock_set_program_counter in ⊢ (???%); >clock_set_clock 807 >EQticks <instr_refl @eq_f2 808 [1: 809 whd in ⊢ (??%%); whd in match (ticks_of0 ??????); 810 2: 811 (* XXX: we need clock_set_arg_8 *) 812 ] 813 18: 814 ] 815 ] 816 (* XXX: switch to the right hand side *) 817 normalize nodelta >EQs s >EQticks ticks 818 cases (¬ eq_bv ???) normalize nodelta 819 whd in ⊢ (??%%); 820 (* XXX: finally, prove the equality using sigma commutation *) 821 @split_eq_status try % 822 [1,2,3,19,20,21,28,29,30: 823 cases daemon (* XXX: axioms as above *) 824 4,13,22,31: 825 5,14,23,32: 826 6,15,24,33: 827 7,16,25,34: 828 8,17,26,35: 829 whd in ⊢ (??%%);maps_assm 830 831 9,18,27,36: 832 whd in ⊢ (??%%); 833 whd in match (ticks_of_instruction ?); <instr_refl 834 cases daemon (* XXX: daemon in ticks_of0 stopping progression *) 835 ] 836 2,4: 837 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 838 [2, 4: 839 cases daemon (* XXX: !!! *) 840 ] 841 normalize nodelta >EQppc 842 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 843 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 844 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 845 #fetch_many_assm whd in fetch_many_assm; %{2} 846 change with (execute_1 ?? = ?) 847 @(pose … (execute_1 ? (status_of_pseudo_status …))) 848 #status_after_1 #EQstatus_after_1 849 <(?: ? = status_after_1) 850 [3,6: 851 >EQstatus_after_1 in ⊢ (???%); 852 whd in ⊢ (???%); 853 [1: 854 <fetch_refl in ⊢ (???%); 855 2: 856 <fetch_refl in ⊢ (???%); 857 ] 858 whd in ⊢ (???%); 859 @(pair_replace ?????????? p) 860 [1,3: 861 cases daemon 862 2,4: 863 normalize nodelta 864 whd in match (addr_of_relative ????); 865 cases (¬ eq_bv ???) normalize nodelta 866 >set_clock_mk_Status_commutation 867 whd in ⊢ (???%); 868 change with (add ???) in match (\snd (half_add ???)); 869 >set_arg_8_set_program_counter in ⊢ (???%); 870 [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 871 >program_counter_set_program_counter in ⊢ (???%); 872 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 873 [2,4,6,8: 874 >bitvector_of_nat_sign_extension_equivalence 875 [1,3,5,7: 876 >EQintermediate_pc' % 877 *: 878 repeat @le_S_S @le_O_n 879 ] 880 ] 881 [1,3: % ] 882 ] 883 1,4: 884 skip 885 ] 886 [3,4: 887 status_after_1 888 @(pose … (execute_1 ? (mk_PreStatus …))) 889 #status_after_1 #EQstatus_after_1 890 <(?: ? = status_after_1) 891 [3,6: 892 >EQstatus_after_1 in ⊢ (???%); 893 whd in ⊢ (???%); 894 (* XXX: matita bug with patterns across multiple goals *) 895 [1: 896 <fetch_refl'' in ⊢ (???%); 897 2: 898 <fetch_refl'' in ⊢ (???%); 899 ] 900 [2: % 1: whd in ⊢ (???%); % ] 901 1,4: 902 skip 903 ] 904 status_after_1 whd in ⊢ (??%?); 905 (* XXX: switch to the right hand side *) 906 normalize nodelta >EQs s >EQticks ticks 907 normalize nodelta whd in ⊢ (??%%); 908 ] 909 (* XXX: finally, prove the equality using sigma commutation *) 910 @split_eq_status try % 911 whd in ⊢ (??%%); 693 [4,5,6,7,8,9: (* INC and DEC *) 912 694 cases daemon 913 ] 914 30: (* CJNE *) 915 (* XXX: work on the right hand side *) 916 cases addr1 addr1 #addr1 normalize nodelta 917 cases addr1 addr1 #addr1_l #addr1_r normalize nodelta 918 (* XXX: switch to the left hand side *) 919 >EQP P normalize nodelta 920 #sigma_increment_commutation #maps_assm #fetch_many_assm 921 922 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 923 <EQppc in fetch_many_assm; 924 whd in match (short_jump_cond ??); 925 @pair_elim #sj_possible #disp 926 @pair_elim #result #flags #sub16_refl 927 @pair_elim #upper #lower #vsplit_refl 928 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 929 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 930 [1,3: 931 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 932 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 933 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 934 whd in ⊢ (??%?); 935 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 936 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 937 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl 938 @(if_then_else_replace ???????? eq_bv_refl) 939 [1,3,5,7: 940 cases daemon 941 2,4,6,8: 942 (* XXX: switch to the right hand side *) 943 normalize nodelta >EQs s >EQticks ticks 944 whd in ⊢ (??%%); 945 (* XXX: finally, prove the equality using sigma commutation *) 946 @split_eq_status try % 947 [3,7,11,15: 948 whd in ⊢ (??%?); 949 [1,3: 950 cases daemon 951 2,4: 952 cases daemon 953 ] 954 ] 955 cases daemon (* XXX *) 956 ] 957 2,4: 958 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 959 [2, 4: 960 cases daemon (* XXX: !!! *) 961 ] 962 normalize nodelta >EQppc 963 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 964 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 965 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 966 #fetch_many_assm whd in fetch_many_assm; %{2} 967 change with (execute_1 ?? = ?) 968 @(pose … (execute_1 ? (status_of_pseudo_status …))) 969 #status_after_1 #EQstatus_after_1 970 <(?: ? = status_after_1) 971 [2,5: 972 inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta 973 3,6: 974 >EQstatus_after_1 in ⊢ (???%); 975 whd in ⊢ (???%); 976 [1: <fetch_refl in ⊢ (???%); 977 2: <fetch_refl in ⊢ (???%); 978 ] 979 whd in ⊢ (???%); 980 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 981 whd in ⊢ (???%); 982 whd in match (addr_of_relative ????); 983 change with (add ???) in match (\snd (half_add ???)); 984 >set_clock_set_program_counter in ⊢ (???%); 985 >program_counter_set_program_counter in ⊢ (???%); 986 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 987 [2,4,6,8: 988 >bitvector_of_nat_sign_extension_equivalence 989 [1,3,5,7: 990 >EQintermediate_pc' % 991 *: 992 repeat @le_S_S @le_O_n 993 ] 994 1,5: 995 % 996 ] 997 1,4: skip 998 ] 999 [1,2,3,4: 1000 status_after_1 1001 @(pose … (execute_1 ? (mk_PreStatus …))) 1002 #status_after_1 #EQstatus_after_1 1003 <(?: ? = status_after_1) 1004 [3,6,9,12: 1005 >EQstatus_after_1 in ⊢ (???%); 1006 whd in ⊢ (???%); 1007 (* XXX: matita bug with patterns across multiple goals *) 1008 [1: <fetch_refl'' in ⊢ (???%); 1009 2: <fetch_refl'' in ⊢ (???%); 1010 3: <fetch_refl'' in ⊢ (???%); 1011 4: <fetch_refl'' in ⊢ (???%); 1012 ] % 1013 1,4,7,10: 1014 skip 1015 ] 1016 status_after_1 whd in ⊢ (??%?); 1017 (* XXX: switch to the right hand side *) 1018 normalize nodelta >EQs s >EQticks ticks 1019 whd in ⊢ (??%%); 1020 ] 1021 (* XXX: finally, prove the equality using sigma commutation *) 1022 @split_eq_status try % 1023 cases daemon 1024 ] 1025 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) 1026 (* XXX: work on the right hand side *) 1027 >p normalize nodelta 1028 (* XXX: switch to the left hand side *) 1029 >EQP P normalize nodelta 1030 #sigma_increment_commutation #maps_assm #fetch_many_assm 1031 1032 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1033 <EQppc in fetch_many_assm; 1034 whd in match (short_jump_cond ??); 1035 @pair_elim #sj_possible #disp 1036 @pair_elim #result #flags #sub16_refl 1037 @pair_elim #upper #lower #vsplit_refl 1038 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 1039 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 1040 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1041 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1042 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1043 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1044 whd in ⊢ (??%?); 1045 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1046 (* XXX: work on the left hand side *) 1047 @(if_then_else_replace ???????? p) normalize nodelta 1048 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1049 cases daemon 1050 ] 1051 (* XXX: switch to the right hand side *) 1052 normalize nodelta >EQs s >EQticks ticks 1053 whd in ⊢ (??%%); 1054 (* XXX: finally, prove the equality using sigma commutation *) 1055 @split_eq_status try % 1056 cases daemon 1057 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1058 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1059 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1060 cases daemon (* XXX: !!! *) 1061 ] 1062 normalize nodelta >EQppc 1063 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1064 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1065 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1066 #fetch_many_assm whd in fetch_many_assm; %{2} 1067 change with (execute_1 ?? = ?) 1068 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1069 #status_after_1 #EQstatus_after_1 1070 <(?: ? = status_after_1) 1071 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 1072 >EQstatus_after_1 in ⊢ (???%); 1073 whd in ⊢ (???%); 1074 [1: <fetch_refl in ⊢ (???%); 1075 2: <fetch_refl in ⊢ (???%); 1076 3: <fetch_refl in ⊢ (???%); 1077 4: <fetch_refl in ⊢ (???%); 1078 5: <fetch_refl in ⊢ (???%); 1079 6: <fetch_refl in ⊢ (???%); 1080 7: <fetch_refl in ⊢ (???%); 1081 8: <fetch_refl in ⊢ (???%); 1082 9: <fetch_refl in ⊢ (???%); 1083 10: <fetch_refl in ⊢ (???%); 1084 11: <fetch_refl in ⊢ (???%); 1085 12: <fetch_refl in ⊢ (???%); 1086 13: <fetch_refl in ⊢ (???%); 1087 14: <fetch_refl in ⊢ (???%); 1088 ] 1089 whd in ⊢ (???%); 1090 @(if_then_else_replace ???????? p) 1091 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1092 cases daemon 1093 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1094 normalize nodelta 1095 whd in match (addr_of_relative ????); 1096 >set_clock_mk_Status_commutation 1097 [9,10: 1098 (* XXX: demodulation not working in this case *) 1099 >program_counter_set_arg_1 in ⊢ (???%); 1100 >program_counter_set_program_counter in ⊢ (???%); 1101 *: 1102 /demod/ 1103 ] 1104 whd in ⊢ (???%); 1105 change with (add ???) in match (\snd (half_add ???)); 1106 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1107 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1108 >bitvector_of_nat_sign_extension_equivalence 1109 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1110 >EQintermediate_pc' % 1111 *: 1112 repeat @le_S_S @le_O_n 1113 ] 1114 ] 1115 % 1116 ] 1117 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1118 skip 1119 ] 1120 status_after_1 1121 @(pose … (execute_1 ? (mk_PreStatus …))) 1122 #status_after_1 #EQstatus_after_1 1123 <(?: ? = status_after_1) 1124 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 1125 >EQstatus_after_1 in ⊢ (???%); 1126 whd in ⊢ (???%); 1127 (* XXX: matita bug with patterns across multiple goals *) 1128 [1: <fetch_refl'' in ⊢ (???%); 1129 2: <fetch_refl' in ⊢ (???%); 1130 3: <fetch_refl'' in ⊢ (???%); 1131 4: <fetch_refl' in ⊢ (???%); 1132 5: <fetch_refl'' in ⊢ (???%); 1133 6: <fetch_refl' in ⊢ (???%); 1134 7: <fetch_refl'' in ⊢ (???%); 1135 8: <fetch_refl' in ⊢ (???%); 1136 9: <fetch_refl'' in ⊢ (???%); 1137 10: <fetch_refl' in ⊢ (???%); 1138 11: <fetch_refl'' in ⊢ (???%); 1139 12: <fetch_refl' in ⊢ (???%); 1140 13: <fetch_refl'' in ⊢ (???%); 1141 14: <fetch_refl' in ⊢ (???%); 1142 ] 1143 whd in ⊢ (???%); 1144 [9,10: 1145 *: 1146 /demod/ 1147 ] % 1148 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1149 skip 1150 ] 1151 status_after_1 whd in ⊢ (??%?); 1152 (* XXX: switch to the right hand side *) 1153 normalize nodelta >EQs s >EQticks ticks 1154 whd in ⊢ (??%%); 1155 (* XXX: finally, prove the equality using sigma commutation *) 1156 @split_eq_status try % 1157 [3,11,19,27,36,53,61: 1158 >program_counter_set_program_counter >set_clock_mk_Status_commutation 1159 [5: >program_counter_set_program_counter ] 1160 >EQaddr_of normalize nodelta 1161 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta 1162 >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 1163 @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉) 1164 >create_label_cost_refl normalize nodelta #relevant @relevant 1165 whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr)) 1166 try assumption whd in match instruction_has_label; normalize nodelta 1167 <instr_refl normalize nodelta % 1168 7,15,23,31,45,57,65: 1169 >set_clock_mk_Status_commutation >program_counter_set_program_counter 1170 whd in ⊢ (??%?); normalize nodelta 1171 >EQppc in fetch_many_assm; #fetch_many_assm 1172 [5: 1173 >program_counter_set_arg_1 >program_counter_set_program_counter 1174 ] 1175 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc'' 1176 <bitvector_of_nat_sign_extension_equivalence 1177 [1,3,5,7,9,11,13: 1178 whd in ⊢ (???%); cases (half_add ???) normalize // 1179 2,4,6,8,10,12,14: 1180 @assembly1_lt_128 1181 @le_S_S @le_O_n 1182 ] 1183 *: 1184 cases daemon 1185 ] 1186 ] 1187 4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 1188 (* XXX: work on the right hand side *) 1189 lapply (subaddressing_modein ???) 1190 <EQaddr normalize nodelta #irrelevant 1191 try (>p normalize nodelta) 1192 try (>p1 normalize nodelta) 1193 (* XXX: switch to the left hand side *) 1194 >EQP P normalize nodelta 1195 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1196 whd in ⊢ (??%?); 1197 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1198 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1199 (* XXX: work on the left hand side *) 1200 [1,2,3,4,5: 1201 generalize in ⊢ (??(???(?%))?); 1202 6,7,8,9,10,11: 1203 generalize in ⊢ (??(???(?%))?); 1204 12: 1205 generalize in ⊢ (??(???(?%))?); 1206 ] 1207 <EQaddr normalize nodelta #irrelevant 1208 try @(jmpair_as_replace ?????????? p) 1209 [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ] 1210 (* XXX: switch to the right hand side *) 1211 normalize nodelta >EQs s >EQticks ticks 1212 whd in ⊢ (??%%); 1213 (* XXX: finally, prove the equality using sigma commutation *) 1214 try @split_eq_status try % whd in ⊢ (??%%); 1215 cases daemon 1216 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 1217 (* XXX: work on the right hand side *) 1218 >p normalize nodelta 1219 try (>p1 normalize nodelta) 1220 (* XXX: switch to the left hand side *) 1221 instr_refl >EQP P normalize nodelta 1222 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1223 whd in ⊢ (??%?); 1224 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1225 (* XXX: work on the left hand side *) 1226 @(pair_replace ?????????? p) 1227 [1,3,5,7,9,11,13,15,17: 1228 >set_clock_set_program_counter >set_clock_mk_Status_commutation 1229 >set_program_counter_mk_Status_commutation >clock_set_program_counter 1230 cases daemon 1231 14,16,18: 1232 normalize nodelta 1233 @(pair_replace ?????????? p1) 1234 [1,3,5: 1235 >set_clock_mk_Status_commutation 1236 cases daemon 1237 ] 1238 ] 1239 (* XXX: switch to the right hand side *) 1240 normalize nodelta >EQs s >EQticks ticks 1241 whd in ⊢ (??%%); 1242 (* XXX: finally, prove the equality using sigma commutation *) 1243 try @split_eq_status try % 1244 cases daemon *) 1245 [42,44: (* RL and RR *) 695 42,44: (* RL and RR *) 1246 696 (* XXX: work on the right hand side *) 1247 697 (* XXX: switch to the left hand side *) … … 1411 861 @sym_eq @set_clock_status_of_pseudo_status 1412 862 [1: 1413 >sigma_increment_commutation863 @sym_eq @set_program_counter_status_of_pseudo_status % 1414 864 2: 1415 865 % … … 1436 886 ] 1437 887 ] 1438 4,5,6,7,8,9: (* INC and DEC *)1439 (* XXX: work on the right hand side *)1440 (* XXX: switch to the left hand side *)1441 >EQP P normalize nodelta1442 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}1443 whd in maps_assm:(??%%);1444 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm1445 [2,4,6,8,10,12: normalize nodelta #absurd destruct(absurd) ]1446 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)1447 whd in ⊢ (??%?);1448 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm1449 @(subaddressing_mode_elim … addr) try #w whd in ⊢ (??%?); normalize nodelta1450 [1:1451 @(jmpair_as_replace ?????????? p)1452 [1:1453 @eq_f2 try % normalize nodelta1454 XXX1455 2:1456 @(jmpair_as_replace ?????????? p)1457 ]1458 888 10: (* MUL *) 1459 889 (* XXX: work on the right hand side *) … … 1474 904 @sym_eq 1475 905 [1: 1476 @(get_8051_sfr_status_of_pseudo_status … policy) #_ 1477 @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) 906 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 907 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) 908 % 1478 909 2: 1479 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1480 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1481 @sym_eq @set_program_counter_status_of_pseudo_status % 910 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) % 1482 911 ] 1483 912 ] … … 1488 917 @sym_eq 1489 918 [1: 1490 @(get_8051_sfr_status_of_pseudo_status … policy ) #_1491 @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)919 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 920 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1492 921 2: 1493 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1494 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1495 @sym_eq @set_program_counter_status_of_pseudo_status % 922 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) % 1496 923 ] 1497 924 ] … … 1514 941 whd in ⊢ (??%?); 1515 942 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 943 whd in ⊢ (??%?); normalize nodelta 944 cases daemon (* XXX: need match_nat_replace but is not working! *) 945 13: (* DA *) 946 (* XXX: work on the right hand side *) 947 (* XXX: switch to the left hand side *) 948 >EQP P normalize nodelta 949 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 950 whd in maps_assm:(??%%); 951 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 952 [2: normalize nodelta #absurd destruct(absurd) ] 953 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1516 954 whd in ⊢ (??%?); 1517 @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm #pose_refl @sym_eq 1518 @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm' #pose_refl' 1519 cut(nat_of_bitvector_assm = nat_of_bitvector_assm') 1520 [1,3: 1521 2,4: 1522 #cut_assm <cut_assm cases nat_of_bitvector_assm try #n' normalize nodelta 1523 @set_flags_status_of_pseudo_status 1524 ] 1525 1526 955 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 956 whd in ⊢ (??%?); normalize nodelta 957 @(pair_replace ?????????? p) 958 [1: 959 @eq_f normalize nodelta >EQs >EQticks <instr_refl 960 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 961 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 962 2: 963 @(pair_replace ?????????? p) 964 [1: 965 @eq_f normalize nodelta >EQs >EQticks <instr_refl % 966 2: 967 @(if_then_else_replace ???????? p1) normalize nodelta 968 [1: 969 cases (gtb ? 9) 970 [1: 971 % 972 2: 973 change with (get_ac_flag ??? = get_ac_flag ???) 974 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 975 cases daemon 976 ] 977 2: 978 @(if_then_else_replace ???????? p1) normalize nodelta try % 979 @(pair_replace ?????????? p2) 980 [1: 981 @eq_f3 try % normalize nodelta 982 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) 983 whd in ⊢ (??%?); 984 >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 985 2: 986 @(pair_replace ?????????? p2) try % 987 @(pair_replace ?????????? p3) try % 988 @(pair_replace ?????????? p3) try % 989 @(if_then_else_replace ???????? p4) try % normalize nodelta 990 @(if_then_else_replace ???????? p4) try % normalize nodelta 991 @(pair_replace ?????????? p5) try % 992 @(pair_replace ?????????? p5) try % 993 @set_flags_status_of_pseudo_status try % 994 [1: 995 @eq_f @sym_eq cases daemon 996 (* XXX: get_ac_flag_status_of_pseudo_status *) 997 2: 998 @sym_eq cases daemon 999 (* XXX: get_ov_flag_status_of_pseudo_status *) 1000 3: 1001 @sym_eq @set_8051_sfr_status_of_pseudo_status 1002 [1: 1003 @sym_eq @set_clock_status_of_pseudo_status 1004 [1: 1005 >EQs 1006 @sym_eq @set_program_counter_status_of_pseudo_status % 1007 2: 1008 >EQs >EQticks <instr_refl % 1009 ] 1010 2: 1011 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1012 ] 1013 ] 1014 ] 1015 ] 1016 ] 1017 ] 1018 14: (* DA *) 1019 (* XXX: work on the right hand side *) 1020 (* XXX: switch to the left hand side *) 1021 >EQP P normalize nodelta 1022 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1023 whd in maps_assm:(??%%); 1024 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1025 [2: normalize nodelta #absurd destruct(absurd) ] 1026 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1027 whd in ⊢ (??%?); 1028 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1029 whd in ⊢ (??%?); normalize nodelta 1030 @(pair_replace ?????????? p) 1031 [1: 1032 @eq_f normalize nodelta >EQs >EQticks <instr_refl 1033 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1034 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1035 2: 1036 @(pair_replace ?????????? p) 1037 [1: 1038 @eq_f normalize nodelta >EQs >EQticks <instr_refl % 1039 2: 1040 @(if_then_else_replace ???????? p1) normalize nodelta 1041 [1: 1042 cases (gtb ? 9) 1043 [1: 1044 % 1045 2: 1046 change with (get_ac_flag ??? = get_ac_flag ???) 1047 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 1048 cases daemon 1049 ] 1050 2: 1051 @(if_then_else_replace ???????? p1) normalize nodelta try % 1052 @(pair_replace ?????????? p2) 1053 [1: 1054 @eq_f3 try % normalize nodelta 1055 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) 1056 whd in ⊢ (??%?); 1057 >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1058 2: 1059 @(pair_replace ?????????? p2) try % 1060 @(pair_replace ?????????? p3) try % 1061 @(pair_replace ?????????? p3) try % 1062 @(if_then_else_replace ???????? p4) try % normalize nodelta 1063 @(if_then_else_replace ???????? p4) try % normalize nodelta 1064 @set_clock_status_of_pseudo_status 1065 [1: 1066 >EQs 1067 @sym_eq @set_program_counter_status_of_pseudo_status % 1068 2: 1069 >EQs >EQticks <instr_refl % 1070 ] 1071 ] 1072 ] 1073 ] 1074 ] 1075 15: (* DA *) 1076 (* XXX: work on the right hand side *) 1077 (* XXX: switch to the left hand side *) 1078 >EQP P normalize nodelta 1079 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1080 whd in maps_assm:(??%%); 1081 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1082 [2: normalize nodelta #absurd destruct(absurd) ] 1083 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1084 whd in ⊢ (??%?); 1085 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1086 whd in ⊢ (??%?); normalize nodelta 1087 @(pair_replace ?????????? p) 1088 [1: 1089 @eq_f normalize nodelta >EQs >EQticks <instr_refl 1090 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1091 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1092 2: 1093 @(pair_replace ?????????? p) 1094 [1: 1095 @eq_f normalize nodelta >EQs >EQticks <instr_refl % 1096 2: 1097 @(if_then_else_replace ???????? p1) normalize nodelta 1098 [1: 1099 cases (gtb ? 9) 1100 [1: 1101 % 1102 2: 1103 change with (get_ac_flag ??? = get_ac_flag ???) 1104 (* XXX: requires get_ac_flag_status_of_pseudo_status *) 1105 cases daemon 1106 ] 1107 2: 1108 @(if_then_else_replace ???????? p1) normalize nodelta try % 1109 @set_clock_status_of_pseudo_status 1110 [1: 1111 >EQs 1112 @sym_eq @set_program_counter_status_of_pseudo_status % 1113 2: 1114 >EQs >EQticks <instr_refl % 1115 ] 1116 ] 1117 ] 1118 ] 1119 16: (* JC *) 1120 (* XXX: work on the right hand side *) 1121 (* XXX: switch to the left hand side *) 1122 >EQP P normalize nodelta 1123 #sigma_increment_commutation #maps_assm 1124 whd in match expand_pseudo_instruction; normalize nodelta 1125 whd in match expand_relative_jump; normalize nodelta 1126 whd in match expand_relative_jump_internal; normalize nodelta 1127 @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta 1128 inversion sj_possible #sj_possible_refl 1129 [1: 1130 #fetch_many_assm %{1} 1131 whd in maps_assm:(??%%); 1132 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1133 whd in ⊢ (??%?); normalize nodelta 1134 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1135 whd in ⊢ (??%?); normalize nodelta 1136 @(if_then_else_replace ???????? p) normalize nodelta 1137 [1: 1138 >EQs @(get_cy_flag_status_of_pseudo_status M') 1139 @sym_eq @set_program_counter_status_of_pseudo_status % 1140 2: 1141 @(if_then_else_replace ???????? p) normalize nodelta try % 1142 >EQs >EQticks <instr_refl 1143 @set_program_counter_status_of_pseudo_status 1144 [1: 1145 >EQaddr_of normalize nodelta 1146 whd in match addr_of_relative; normalize nodelta 1147 whd in match (program_counter ???); 1148 >sigma_increment_commutation 1149 whd in match assembly_1_pseudoinstruction; normalize nodelta 1150 whd in match expand_pseudo_instruction; normalize nodelta 1151 whd in match expand_relative_jump; normalize nodelta 1152 whd in match expand_relative_jump_internal; normalize nodelta 1153 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1154 [1: 1155 >EQppc % 1156 2: 1157 >sj_possible_refl normalize nodelta normalize in match (length ??); 1158 cases daemon 1159 (* XXX: missing invariant? *) 1160 ] 1161 2: 1162 @sym_eq @set_clock_status_of_pseudo_status try % 1163 @eq_f2 try % whd in ⊢ (??%%); 1164 whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation 1165 whd in match assembly_1_pseudoinstruction; normalize nodelta 1166 whd in match expand_pseudo_instruction; normalize nodelta 1167 whd in match expand_relative_jump; normalize nodelta 1168 whd in match expand_relative_jump_internal; normalize nodelta 1169 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1170 [1: 1171 @eq_f2 try % >EQppc % 1172 2: 1173 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1174 [1: 1175 @eq_f2 try % (* XXX: finish, use Jaap's invariant *) 1176 cases daemon 1177 2: 1178 #_ >sj_possible_refl % 1179 ] 1180 ] 1181 ] 1182 ] 1183 2: 1184 normalize nodelta >EQppc 1185 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1186 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1187 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1188 #fetch_many_assm whd in fetch_many_assm; %{2} 1189 change with (execute_1 ?? = ?) 1190 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1191 #status_after_1 #EQstatus_after_1 1192 cases daemon (* XXX: ??? *) 1193 ] 1194 ] 1195 qed. 1196 1197 (* 1527 1198 (* XXX: work on the left hand side *) 1528 1199 (* XXX: switch to the right hand side *) … … 1638 1309 cases daemon 1639 1310 ] 1640 qed. 1311 *) 1312 1313 1314 (* [31,32: (* DJNZ *) 1315 (* XXX: work on the right hand side *) 1316 >p normalize nodelta >p1 normalize nodelta 1317 (* XXX: switch to the left hand side *) 1318 >EQP P normalize nodelta 1319 #sigma_increment_commutation #maps_assm #fetch_many_assm 1320 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1321 <EQppc in fetch_many_assm; 1322 whd in match (short_jump_cond ??); 1323 @pair_elim #sj_possible #disp 1324 @pair_elim #result #flags #sub16_refl 1325 @pair_elim #upper #lower #vsplit_refl 1326 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 1327 #sj_possible_pair destruct(sj_possible_pair) 1328 >p1 normalize nodelta 1329 [1,3: 1330 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1331 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1332 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1333 whd in ⊢ (??%?); 1334 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1335 lapply maps_assm whd in ⊢ (??%? → ?); 1336 inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta 1337 [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl M' 1338 (* XXX: work on the left hand side *) 1339 @(pair_replace ?????????? p) normalize nodelta 1340 [1,3: 1341 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) 1342 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1343 >(get_arg_8_set_program_counter … true addr1) 1344 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1345 @get_arg_8_pseudo_addressing_mode_ok assumption 1346 2,4: 1347 >p1 normalize nodelta >EQs 1348 alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)". 1349 >set_program_counter_status_of_pseudo_status 1350 whd in ⊢ (??%%); 1351 @split_eq_status 1352 [1,10: 1353 whd in ⊢ (??%%); >set_arg_8_set_program_counter 1354 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1355 >low_internal_ram_set_program_counter 1356 [1: 1357 >low_internal_ram_set_program_counter 1358 (* XXX: ??? *) 1359 2: 1360 >low_internal_ram_set_clock 1361 (* XXX: ??? *) 1362 ] 1363 2,11: 1364 whd in ⊢ (??%%); >set_arg_8_set_program_counter 1365 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1366 >high_internal_ram_set_program_counter 1367 [1: 1368 >high_internal_ram_set_program_counter 1369 (* XXX: ??? *) 1370 2: 1371 >high_internal_ram_set_clock 1372 (* XXX: ??? *) 1373 ] 1374 3,12: 1375 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); 1376 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1377 >(external_ram_set_arg_8 ??? addr1) 1378 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1379 4,13: 1380 whd in ⊢ (??%%); >EQaddr_of normalize nodelta 1381 [1: 1382 >program_counter_set_program_counter 1383 >set_arg_8_set_program_counter 1384 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1385 >set_clock_set_program_counter >program_counter_set_program_counter 1386 change with (add ??? = ?) 1387 (* XXX: ??? *) 1388 2: 1389 >set_arg_8_set_program_counter 1390 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1391 >program_counter_set_program_counter 1392 >set_arg_8_set_program_counter 1393 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1394 >set_clock_set_program_counter >program_counter_set_program_counter 1395 >sigma_increment_commutation <EQppc 1396 whd in match (assembly_1_pseudoinstruction ??????); 1397 whd in match (expand_pseudo_instruction ??????); 1398 (* XXX: ??? *) 1399 ] 1400 5,14: 1401 whd in match (special_function_registers_8051 ???); 1402 [1: 1403 >special_function_registers_8051_set_program_counter 1404 >special_function_registers_8051_set_clock 1405 >set_arg_8_set_program_counter in ⊢ (???%); 1406 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1407 >special_function_registers_8051_set_program_counter 1408 >set_arg_8_set_program_counter 1409 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1410 >special_function_registers_8051_set_program_counter 1411 @special_function_registers_8051_set_arg_8 assumption 1412 2: 1413 >special_function_registers_8051_set_clock 1414 >set_arg_8_set_program_counter 1415 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1416 >set_arg_8_set_program_counter 1417 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1418 >special_function_registers_8051_set_program_counter 1419 >special_function_registers_8051_set_program_counter 1420 @special_function_registers_8051_set_arg_8 assumption 1421 ] 1422 6,15: 1423 whd in match (special_function_registers_8052 ???); 1424 whd in match (special_function_registers_8052 ???) in ⊢ (???%); 1425 [1: 1426 >set_arg_8_set_program_counter 1427 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1428 >set_arg_8_set_program_counter 1429 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1430 >special_function_registers_8052_set_program_counter 1431 >special_function_registers_8052_set_program_counter 1432 @special_function_registers_8052_set_arg_8 assumption 1433 2: 1434 whd in ⊢ (??%%); 1435 >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption 1436 ] 1437 (* XXX: we need special_function_registers_8052_set_arg_8 *) 1438 7,16: 1439 whd in match (p1_latch ???); 1440 whd in match (p1_latch ???) in ⊢ (???%); 1441 (* XXX: we need p1_latch_8052_set_arg_8 *) 1442 8,17: 1443 whd in match (p3_latch ???); 1444 whd in match (p3_latch ???) in ⊢ (???%); 1445 (* XXX: we need p3_latch_8052_set_arg_8 *) 1446 9: 1447 >clock_set_clock 1448 >clock_set_program_counter in ⊢ (???%); >clock_set_clock 1449 >EQticks <instr_refl @eq_f2 1450 [1: 1451 whd in ⊢ (??%%); whd in match (ticks_of0 ??????); 1452 2: 1453 (* XXX: we need clock_set_arg_8 *) 1454 ] 1455 18: 1456 ] 1457 ] 1458 (* XXX: switch to the right hand side *) 1459 normalize nodelta >EQs s >EQticks ticks 1460 cases (¬ eq_bv ???) normalize nodelta 1461 whd in ⊢ (??%%); 1462 (* XXX: finally, prove the equality using sigma commutation *) 1463 @split_eq_status try % 1464 [1,2,3,19,20,21,28,29,30: 1465 cases daemon (* XXX: axioms as above *) 1466 4,13,22,31: 1467 5,14,23,32: 1468 6,15,24,33: 1469 7,16,25,34: 1470 8,17,26,35: 1471 whd in ⊢ (??%%);maps_assm 1472 1473 9,18,27,36: 1474 whd in ⊢ (??%%); 1475 whd in match (ticks_of_instruction ?); <instr_refl 1476 cases daemon (* XXX: daemon in ticks_of0 stopping progression *) 1477 ] 1478 2,4: 1479 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1480 [2, 4: 1481 cases daemon (* XXX: !!! *) 1482 ] 1483 normalize nodelta >EQppc 1484 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1485 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1486 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1487 #fetch_many_assm whd in fetch_many_assm; %{2} 1488 change with (execute_1 ?? = ?) 1489 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1490 #status_after_1 #EQstatus_after_1 1491 <(?: ? = status_after_1) 1492 [3,6: 1493 >EQstatus_after_1 in ⊢ (???%); 1494 whd in ⊢ (???%); 1495 [1: 1496 <fetch_refl in ⊢ (???%); 1497 2: 1498 <fetch_refl in ⊢ (???%); 1499 ] 1500 whd in ⊢ (???%); 1501 @(pair_replace ?????????? p) 1502 [1,3: 1503 cases daemon 1504 2,4: 1505 normalize nodelta 1506 whd in match (addr_of_relative ????); 1507 cases (¬ eq_bv ???) normalize nodelta 1508 >set_clock_mk_Status_commutation 1509 whd in ⊢ (???%); 1510 change with (add ???) in match (\snd (half_add ???)); 1511 >set_arg_8_set_program_counter in ⊢ (???%); 1512 [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1513 >program_counter_set_program_counter in ⊢ (???%); 1514 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1515 [2,4,6,8: 1516 >bitvector_of_nat_sign_extension_equivalence 1517 [1,3,5,7: 1518 >EQintermediate_pc' % 1519 *: 1520 repeat @le_S_S @le_O_n 1521 ] 1522 ] 1523 [1,3: % ] 1524 ] 1525 1,4: 1526 skip 1527 ] 1528 [3,4: 1529 status_after_1 1530 @(pose … (execute_1 ? (mk_PreStatus …))) 1531 #status_after_1 #EQstatus_after_1 1532 <(?: ? = status_after_1) 1533 [3,6: 1534 >EQstatus_after_1 in ⊢ (???%); 1535 whd in ⊢ (???%); 1536 (* XXX: matita bug with patterns across multiple goals *) 1537 [1: 1538 <fetch_refl'' in ⊢ (???%); 1539 2: 1540 <fetch_refl'' in ⊢ (???%); 1541 ] 1542 [2: % 1: whd in ⊢ (???%); % ] 1543 1,4: 1544 skip 1545 ] 1546 status_after_1 whd in ⊢ (??%?); 1547 (* XXX: switch to the right hand side *) 1548 normalize nodelta >EQs s >EQticks ticks 1549 normalize nodelta whd in ⊢ (??%%); 1550 ] 1551 (* XXX: finally, prove the equality using sigma commutation *) 1552 @split_eq_status try % 1553 whd in ⊢ (??%%); 1554 cases daemon 1555 ] 1556 30: (* CJNE *) 1557 (* XXX: work on the right hand side *) 1558 cases addr1 addr1 #addr1 normalize nodelta 1559 cases addr1 addr1 #addr1_l #addr1_r normalize nodelta 1560 (* XXX: switch to the left hand side *) 1561 >EQP P normalize nodelta 1562 #sigma_increment_commutation #maps_assm #fetch_many_assm 1563 1564 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1565 <EQppc in fetch_many_assm; 1566 whd in match (short_jump_cond ??); 1567 @pair_elim #sj_possible #disp 1568 @pair_elim #result #flags #sub16_refl 1569 @pair_elim #upper #lower #vsplit_refl 1570 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 1571 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 1572 [1,3: 1573 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1574 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1575 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1576 whd in ⊢ (??%?); 1577 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1578 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 1579 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl 1580 @(if_then_else_replace ???????? eq_bv_refl) 1581 [1,3,5,7: 1582 cases daemon 1583 2,4,6,8: 1584 (* XXX: switch to the right hand side *) 1585 normalize nodelta >EQs s >EQticks ticks 1586 whd in ⊢ (??%%); 1587 (* XXX: finally, prove the equality using sigma commutation *) 1588 @split_eq_status try % 1589 [3,7,11,15: 1590 whd in ⊢ (??%?); 1591 [1,3: 1592 cases daemon 1593 2,4: 1594 cases daemon 1595 ] 1596 ] 1597 cases daemon (* XXX *) 1598 ] 1599 2,4: 1600 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1601 [2, 4: 1602 cases daemon (* XXX: !!! *) 1603 ] 1604 normalize nodelta >EQppc 1605 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1606 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1607 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1608 #fetch_many_assm whd in fetch_many_assm; %{2} 1609 change with (execute_1 ?? = ?) 1610 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1611 #status_after_1 #EQstatus_after_1 1612 <(?: ? = status_after_1) 1613 [2,5: 1614 inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta 1615 3,6: 1616 >EQstatus_after_1 in ⊢ (???%); 1617 whd in ⊢ (???%); 1618 [1: <fetch_refl in ⊢ (???%); 1619 2: <fetch_refl in ⊢ (???%); 1620 ] 1621 whd in ⊢ (???%); 1622 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 1623 whd in ⊢ (???%); 1624 whd in match (addr_of_relative ????); 1625 change with (add ???) in match (\snd (half_add ???)); 1626 >set_clock_set_program_counter in ⊢ (???%); 1627 >program_counter_set_program_counter in ⊢ (???%); 1628 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1629 [2,4,6,8: 1630 >bitvector_of_nat_sign_extension_equivalence 1631 [1,3,5,7: 1632 >EQintermediate_pc' % 1633 *: 1634 repeat @le_S_S @le_O_n 1635 ] 1636 1,5: 1637 % 1638 ] 1639 1,4: skip 1640 ] 1641 [1,2,3,4: 1642 status_after_1 1643 @(pose … (execute_1 ? (mk_PreStatus …))) 1644 #status_after_1 #EQstatus_after_1 1645 <(?: ? = status_after_1) 1646 [3,6,9,12: 1647 >EQstatus_after_1 in ⊢ (???%); 1648 whd in ⊢ (???%); 1649 (* XXX: matita bug with patterns across multiple goals *) 1650 [1: <fetch_refl'' in ⊢ (???%); 1651 2: <fetch_refl'' in ⊢ (???%); 1652 3: <fetch_refl'' in ⊢ (???%); 1653 4: <fetch_refl'' in ⊢ (???%); 1654 ] % 1655 1,4,7,10: 1656 skip 1657 ] 1658 status_after_1 whd in ⊢ (??%?); 1659 (* XXX: switch to the right hand side *) 1660 normalize nodelta >EQs s >EQticks ticks 1661 whd in ⊢ (??%%); 1662 ] 1663 (* XXX: finally, prove the equality using sigma commutation *) 1664 @split_eq_status try % 1665 cases daemon 1666 ] 1667 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) 1668 (* XXX: work on the right hand side *) 1669 >p normalize nodelta 1670 (* XXX: switch to the left hand side *) 1671 >EQP P normalize nodelta 1672 #sigma_increment_commutation #maps_assm #fetch_many_assm 1673 1674 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1675 <EQppc in fetch_many_assm; 1676 whd in match (short_jump_cond ??); 1677 @pair_elim #sj_possible #disp 1678 @pair_elim #result #flags #sub16_refl 1679 @pair_elim #upper #lower #vsplit_refl 1680 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 1681 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 1682 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1683 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1684 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1685 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1686 whd in ⊢ (??%?); 1687 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1688 (* XXX: work on the left hand side *) 1689 @(if_then_else_replace ???????? p) normalize nodelta 1690 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1691 cases daemon 1692 ] 1693 (* XXX: switch to the right hand side *) 1694 normalize nodelta >EQs s >EQticks ticks 1695 whd in ⊢ (??%%); 1696 (* XXX: finally, prove the equality using sigma commutation *) 1697 @split_eq_status try % 1698 cases daemon 1699 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1700 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1701 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1702 cases daemon (* XXX: !!! *) 1703 ] 1704 normalize nodelta >EQppc 1705 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1706 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1707 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1708 #fetch_many_assm whd in fetch_many_assm; %{2} 1709 change with (execute_1 ?? = ?) 1710 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1711 #status_after_1 #EQstatus_after_1 1712 <(?: ? = status_after_1) 1713 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 1714 >EQstatus_after_1 in ⊢ (???%); 1715 whd in ⊢ (???%); 1716 [1: <fetch_refl in ⊢ (???%); 1717 2: <fetch_refl in ⊢ (???%); 1718 3: <fetch_refl in ⊢ (???%); 1719 4: <fetch_refl in ⊢ (???%); 1720 5: <fetch_refl in ⊢ (???%); 1721 6: <fetch_refl in ⊢ (???%); 1722 7: <fetch_refl in ⊢ (???%); 1723 8: <fetch_refl in ⊢ (???%); 1724 9: <fetch_refl in ⊢ (???%); 1725 10: <fetch_refl in ⊢ (???%); 1726 11: <fetch_refl in ⊢ (???%); 1727 12: <fetch_refl in ⊢ (???%); 1728 13: <fetch_refl in ⊢ (???%); 1729 14: <fetch_refl in ⊢ (???%); 1730 ] 1731 whd in ⊢ (???%); 1732 @(if_then_else_replace ???????? p) 1733 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1734 cases daemon 1735 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1736 normalize nodelta 1737 whd in match (addr_of_relative ????); 1738 >set_clock_mk_Status_commutation 1739 [9,10: 1740 (* XXX: demodulation not working in this case *) 1741 >program_counter_set_arg_1 in ⊢ (???%); 1742 >program_counter_set_program_counter in ⊢ (???%); 1743 *: 1744 /demod/ 1745 ] 1746 whd in ⊢ (???%); 1747 change with (add ???) in match (\snd (half_add ???)); 1748 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1749 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1750 >bitvector_of_nat_sign_extension_equivalence 1751 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1752 >EQintermediate_pc' % 1753 *: 1754 repeat @le_S_S @le_O_n 1755 ] 1756 ] 1757 % 1758 ] 1759 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1760 skip 1761 ] 1762 status_after_1 1763 @(pose … (execute_1 ? (mk_PreStatus …))) 1764 #status_after_1 #EQstatus_after_1 1765 <(?: ? = status_after_1) 1766 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 1767 >EQstatus_after_1 in ⊢ (???%); 1768 whd in ⊢ (???%); 1769 (* XXX: matita bug with patterns across multiple goals *) 1770 [1: <fetch_refl'' in ⊢ (???%); 1771 2: <fetch_refl' in ⊢ (???%); 1772 3: <fetch_refl'' in ⊢ (???%); 1773 4: <fetch_refl' in ⊢ (???%); 1774 5: <fetch_refl'' in ⊢ (???%); 1775 6: <fetch_refl' in ⊢ (???%); 1776 7: <fetch_refl'' in ⊢ (???%); 1777 8: <fetch_refl' in ⊢ (???%); 1778 9: <fetch_refl'' in ⊢ (???%); 1779 10: <fetch_refl' in ⊢ (???%); 1780 11: <fetch_refl'' in ⊢ (???%); 1781 12: <fetch_refl' in ⊢ (???%); 1782 13: <fetch_refl'' in ⊢ (???%); 1783 14: <fetch_refl' in ⊢ (???%); 1784 ] 1785 whd in ⊢ (???%); 1786 [9,10: 1787 *: 1788 /demod/ 1789 ] % 1790 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 1791 skip 1792 ] 1793 status_after_1 whd in ⊢ (??%?); 1794 (* XXX: switch to the right hand side *) 1795 normalize nodelta >EQs s >EQticks ticks 1796 whd in ⊢ (??%%); 1797 (* XXX: finally, prove the equality using sigma commutation *) 1798 @split_eq_status try % 1799 [3,11,19,27,36,53,61: 1800 >program_counter_set_program_counter >set_clock_mk_Status_commutation 1801 [5: >program_counter_set_program_counter ] 1802 >EQaddr_of normalize nodelta 1803 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta 1804 >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 1805 @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉) 1806 >create_label_cost_refl normalize nodelta #relevant @relevant 1807 whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr)) 1808 try assumption whd in match instruction_has_label; normalize nodelta 1809 <instr_refl normalize nodelta % 1810 7,15,23,31,45,57,65: 1811 >set_clock_mk_Status_commutation >program_counter_set_program_counter 1812 whd in ⊢ (??%?); normalize nodelta 1813 >EQppc in fetch_many_assm; #fetch_many_assm 1814 [5: 1815 >program_counter_set_arg_1 >program_counter_set_program_counter 1816 ] 1817 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc'' 1818 <bitvector_of_nat_sign_extension_equivalence 1819 [1,3,5,7,9,11,13: 1820 whd in ⊢ (???%); cases (half_add ???) normalize // 1821 2,4,6,8,10,12,14: 1822 @assembly1_lt_128 1823 @le_S_S @le_O_n 1824 ] 1825 *: 1826 cases daemon 1827 ] 1828 ] 1829 4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 1830 (* XXX: work on the right hand side *) 1831 lapply (subaddressing_modein ???) 1832 <EQaddr normalize nodelta #irrelevant 1833 try (>p normalize nodelta) 1834 try (>p1 normalize nodelta) 1835 (* XXX: switch to the left hand side *) 1836 >EQP P normalize nodelta 1837 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1838 whd in ⊢ (??%?); 1839 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1840 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1841 (* XXX: work on the left hand side *) 1842 [1,2,3,4,5: 1843 generalize in ⊢ (??(???(?%))?); 1844 6,7,8,9,10,11: 1845 generalize in ⊢ (??(???(?%))?); 1846 12: 1847 generalize in ⊢ (??(???(?%))?); 1848 ] 1849 <EQaddr normalize nodelta #irrelevant 1850 try @(jmpair_as_replace ?????????? p) 1851 [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ] 1852 (* XXX: switch to the right hand side *) 1853 normalize nodelta >EQs s >EQticks ticks 1854 whd in ⊢ (??%%); 1855 (* XXX: finally, prove the equality using sigma commutation *) 1856 try @split_eq_status try % whd in ⊢ (??%%); 1857 cases daemon 1858 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 1859 (* XXX: work on the right hand side *) 1860 >p normalize nodelta 1861 try (>p1 normalize nodelta) 1862 (* XXX: switch to the left hand side *) 1863 instr_refl >EQP P normalize nodelta 1864 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1865 whd in ⊢ (??%?); 1866 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1867 (* XXX: work on the left hand side *) 1868 @(pair_replace ?????????? p) 1869 [1,3,5,7,9,11,13,15,17: 1870 >set_clock_set_program_counter >set_clock_mk_Status_commutation 1871 >set_program_counter_mk_Status_commutation >clock_set_program_counter 1872 cases daemon 1873 14,16,18: 1874 normalize nodelta 1875 @(pair_replace ?????????? p1) 1876 [1,3,5: 1877 >set_clock_mk_Status_commutation 1878 cases daemon 1879 ] 1880 ] 1881 (* XXX: switch to the right hand side *) 1882 normalize nodelta >EQs s >EQticks ticks 1883 whd in ⊢ (??%%); 1884 (* XXX: finally, prove the equality using sigma commutation *) 1885 try @split_eq_status try % 1886 cases daemon *) 
src/ASM/Test.ma
r2181 r2183 11 11 ∀policy. 12 12 ∀s, s'. 13 ∀new_ppc. 13 ∀new_ppc, new_ppc'. 14 sigma new_ppc = new_ppc' → 14 15 status_of_pseudo_status M cm s sigma policy = s' → 15 16 set_program_counter (BitVectorTrie Byte 16) 16 17 (code_memory_of_pseudo_assembly_program cm sigma policy) 17 s' 18 (sigma new_ppc) = 18 s' new_ppc' = 19 19 status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. 20 #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // 20 #M #cm #sigma #policy #s #s' #new_ppc #new_ppc' 21 #new_ppc_refl #s_refl <new_ppc_refl <s_refl // 21 22 qed. 22 23
Note: See TracChangeset
for help on using the changeset viewer.