- Timestamp:
- Jul 19, 2012, 5:33:54 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2212 r2216 295 295 qed. 296 296 297 (*298 297 lemma match_nat_status_of_pseudo_status: 299 298 ∀M, cm, sigma, policy, s, s', s'', s'''. … … 301 300 n = n' → 302 301 status_of_pseudo_status M cm s' sigma policy = s → 303 status_of_pseudo_status M cm s''' sigma policy = s''→304 match n with [ O ⇒ s | S n' ⇒ s'' ] =305 status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' ]) sigma policy.302 (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) → 303 match n with [ O ⇒ s | S n' ⇒ s'' n' ] = 304 status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy. 306 305 #M #cm #sigma #policy #s #s' #s'' #s''' #n #n' 307 #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'308 cases n normalize nodelta try % #n' %306 #n_refl #s_refl #s_refl' <n_refl <s_refl 307 cases n normalize nodelta try % #n' <(s_refl' n') % 309 308 qed. 310 *) 309 310 lemma get_index_v_set_index_hit: 311 ∀A: Type[0]. 312 ∀n: nat. 313 ∀v: Vector A n. 314 ∀i: nat. 315 ∀e: A. 316 ∀i_lt_n_proof: i < n. 317 ∀i_lt_n_proof': i < n. 318 get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e. 319 #A #n #v elim v 320 [1: 321 #i #e #i_lt_n_proof 322 cases (lt_to_not_zero … i_lt_n_proof) 323 |2: 324 #n' #hd #tl #inductive_hypothesis #i #e 325 cases i 326 [1: 327 #i_lt_n_proof #i_lt_n_proof' % 328 |2: 329 #i' #i_lt_n_proof' #i_lt_n_proof'' 330 whd in ⊢ (??%?); @inductive_hypothesis 331 ] 332 ] 333 qed. 311 334 312 335 lemma main_lemma_preinstruction: … … 767 790 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 768 791 whd in match execute_1_preinstruction; normalize nodelta 769 [(* 35: (* XRL *) 770 inversion addr 771 [1: 772 #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl 773 >EQP -P normalize nodelta 774 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 775 whd in maps_assm:(??%%); 776 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 777 [2: normalize nodelta #absurd destruct(absurd) ] 778 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 779 [2: normalize nodelta #absurd destruct(absurd) ] 780 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 781 whd in ⊢ (??%?); 782 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 783 change with (set_arg_8 ????? = ?) 784 @set_arg_8_status_of_pseudo_status try % 785 >EQs >EQticks <instr_refl >addr_refl 786 [1: 787 @sym_eq @set_clock_status_of_pseudo_status 788 [1: 789 @sym_eq @set_program_counter_status_of_pseudo_status % 790 |2: 791 @eq_f2 % 792 ] 793 |2: 794 @(subaddressing_mode_elim … acc_a) @I 795 |3: 796 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 797 [1: 798 @(subaddressing_mode_elim … acc_a) % 799 |4: 800 @eq_f2 801 @(pose … (set_clock ????)) #status #status_refl 802 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 803 [1: 804 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 805 [1: @(subaddressing_mode_elim … acc_a) % |*: % ] 806 |3: 807 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 808 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 809 |2: 810 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 811 [1: @(subaddressing_mode_elim … acc_a) % |2: % ] 812 |4: 813 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 814 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 815 ] 816 |*: 817 % 818 ] 819 ] 820 |2: 821 #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl 822 >EQP -P normalize nodelta 823 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 824 whd in maps_assm:(??%%); 825 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 826 [2: normalize nodelta #absurd destruct(absurd) ] 827 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 828 [2: normalize nodelta #absurd destruct(absurd) ] 829 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 830 whd in ⊢ (??%?); 831 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 832 change with (set_arg_8 ????? = ?) 833 @set_arg_8_status_of_pseudo_status try % 834 >EQs >EQticks <instr_refl >addr_refl 835 [1: 836 @sym_eq @set_clock_status_of_pseudo_status 837 [1: 838 @sym_eq @set_program_counter_status_of_pseudo_status % 839 |2: 840 @eq_f2 % 841 ] 842 |2: 843 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 844 [1: @(subaddressing_mode_elim … direct) #w % ] % 845 |3: 846 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 847 [1: 848 @(subaddressing_mode_elim … direct) #w % 849 |4: 850 @eq_f2 851 @(pose … (set_clock ????)) #status #status_refl 852 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 853 [1: 854 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 855 [1: @(subaddressing_mode_elim … direct) #w % |*: % ] 856 |3: 857 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 858 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 859 |2: 860 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 861 [1: @(subaddressing_mode_elim … direct) #w % |2: % ] 862 |4: 863 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 864 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 865 ] 866 |*: 867 % 868 ] 869 ] 870 ] 871 |33,34: (* ANL and ORL *) 872 inversion addr 873 [1,3: 874 * 875 [1,3: 876 #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl 877 >EQP -P normalize nodelta 878 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 879 whd in maps_assm:(??%%); 880 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 881 [2,4: normalize nodelta #absurd destruct(absurd) ] 882 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 883 [2,4: normalize nodelta #absurd destruct(absurd) ] 884 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 885 whd in ⊢ (??%?); 886 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 887 change with (set_arg_8 ????? = ?) 888 @set_arg_8_status_of_pseudo_status try % 889 >EQs >EQticks <instr_refl >addr_refl 890 [1,4: 891 @sym_eq @set_clock_status_of_pseudo_status 892 [1,3: 893 @sym_eq @set_program_counter_status_of_pseudo_status % 894 |2,4: 895 @eq_f2 % 896 ] 897 |2,5: 898 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 899 [1,3: @(subaddressing_mode_elim … acc_a) % ] % 900 |3,6: 901 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 902 [1,5: 903 @(subaddressing_mode_elim … acc_a) % 904 |4,8: 905 @eq_f2 906 @(pose … (set_clock ????)) #status #status_refl 907 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 908 [1,5: 909 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 910 [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ] 911 |3,7: 912 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 913 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 914 |2,6: 915 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 916 [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ] 917 |4,8: 918 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 919 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 920 ] 921 |*: 922 % 923 ] 924 ] 925 |2,4: 926 #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl 927 >EQP -P normalize nodelta 928 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 929 whd in maps_assm:(??%%); 930 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 931 [2,4: normalize nodelta #absurd destruct(absurd) ] 932 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 933 [2,4: normalize nodelta #absurd destruct(absurd) ] 934 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 935 whd in ⊢ (??%?); 936 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 937 change with (set_arg_8 ????? = ?) 938 @set_arg_8_status_of_pseudo_status try % 939 >EQs >EQticks <instr_refl >addr_refl 940 [1,4: 941 @sym_eq @set_clock_status_of_pseudo_status 942 [1,3: 943 @sym_eq @set_program_counter_status_of_pseudo_status % 944 |2,4: 945 @eq_f2 % 946 ] 947 |2,5: 948 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 949 [1,3: @(subaddressing_mode_elim … direct) #w % ] % 950 |3,6: 951 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 952 [1,5: 953 @(subaddressing_mode_elim … direct) #w % 954 |4,8: 955 @eq_f2 956 @(pose … (set_clock ????)) #status #status_refl 957 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 958 [1,5: 959 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 960 [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ] 961 |3,7: 962 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 963 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 964 |2,6: 965 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 966 [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ] 967 |4,8: 968 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 969 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 970 ] 971 |*: 972 % 973 ] 974 ] 975 ] 976 |2,4: 977 #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl 978 >EQP -P normalize nodelta 979 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 980 whd in maps_assm:(??%%); 981 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 982 [2,4: normalize nodelta #absurd destruct(absurd) ] 983 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 984 [2,4: normalize nodelta #absurd destruct(absurd) ] 985 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 986 whd in ⊢ (??%?); 987 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 988 change with (set_flags ?????? = ?) 989 [1,4: @set_flags_status_of_pseudo_status try % |*: skip ] 990 >EQs >EQticks <instr_refl >addr_refl 991 @sym_eq @set_clock_status_of_pseudo_status % 992 ] 993 |*)4: (* INC *) 994 (* XXX: work on the right hand side *) 995 (* XXX: switch to the left hand side *) 996 >EQs >EQticks <instr_refl >EQP -P normalize nodelta 997 @(subaddressing_mode_elim … addr) normalize nodelta 998 [1: 999 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1000 whd in maps_assm:(??%%); 1001 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1002 [2: normalize nodelta #absurd destruct(absurd) ] 1003 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1004 whd in ⊢ (??%?); 1005 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1006 whd in ⊢ (??%?); 1007 inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta 1008 @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl)) 1009 [1: 1010 @eq_f2 try % 1011 @(pose … (set_clock ????)) #status #status_refl 1012 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1013 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 1014 |2: 1015 @set_arg_8_status_of_pseudo_status try % 1016 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 1017 ] 1018 |2: 1019 |3: 1020 |4: 1021 |5: 1022 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1023 whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1024 whd in ⊢ (??%?); 1025 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1026 whd in ⊢ (??%?); 1027 inversion (half_add ???) #carry #bl #carry_bl_refl normalize nodelta 1028 @(pair_replace ?????????? (refl_to_jmrefl ??? carry_bl_refl)) 1029 [1: 1030 |2: 1031 ] 1032 ] 1033 |5,6,7,8,9: (* INC and DEC *) 1034 cases daemon 1035 |42,44: (* RL and RR *) 1036 (* XXX: work on the right hand side *) 1037 (* XXX: switch to the left hand side *) 1038 >EQP -P normalize nodelta 1039 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1040 whd in maps_assm:(??%%); 1041 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1042 [2,4: normalize nodelta #absurd destruct(absurd) ] 1043 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1044 whd in ⊢ (??%?); 1045 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 1046 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1047 [2,4: 1048 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1049 @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1050 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1051 % 1052 ] 1053 @sym_eq @set_clock_status_of_pseudo_status 1054 [2,4: 1055 % 1056 ] 1057 @sym_eq @set_program_counter_status_of_pseudo_status % 1058 |43,45: (* RLC and RRC *) 1059 (* XXX: work on the right hand side *) 1060 (* XXX: switch to the left hand side *) 1061 >EQP -P normalize nodelta 1062 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1063 whd in maps_assm:(??%%); 1064 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1065 [2,4: normalize nodelta #absurd destruct(absurd) ] 1066 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1067 whd in ⊢ (??%?); 1068 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 1069 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1070 [2,4: 1071 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1072 @eq_f2 1073 [1,3: 1074 @sym_eq 1075 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1076 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1077 |2,4: 1078 @sym_eq @(get_cy_flag_status_of_pseudo_status … M') 1079 @sym_eq @set_clock_status_of_pseudo_status % 1080 ] 1081 |1,3: 1082 @sym_eq @set_arg_1_status_of_pseudo_status try % 1083 @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1084 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1085 ] 1086 |1,2: (* ADD and ADDC *) 792 [(*1,2: (* ADD and ADDC *) 1087 793 (* XXX: work on the right hand side *) 1088 794 (* XXX: switch to the left hand side *) … … 1154 860 |2: 1155 861 >status_refl 1156 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1) 1157 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1158 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1159 @(subaddressing_mode_elim … addr1) 862 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) 863 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1160 864 |3: 1161 865 >status_refl 1162 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1) 1163 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1164 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1165 @(subaddressing_mode_elim … addr1) 866 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) 867 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1166 868 ] 1167 869 |2: … … 1172 874 |2: 1173 875 >status_refl 1174 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2) 1175 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1176 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1177 cases daemon (* XXX: ??? *) 876 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 877 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1178 878 |3: 1179 879 >status_refl 1180 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2) 1181 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1182 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1183 cases daemon (* XXX: ??? *) 880 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 881 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1184 882 ] 1185 883 |3: … … 1205 903 @I 1206 904 |3: 1207 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A) 1208 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1209 whd in ⊢ (??%?); 1210 >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1211 ] 1212 ] 1213 ] 1214 |10: (* MUL *) 905 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) 906 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try % 907 <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) % 908 ] 909 ] 910 ] 911 |4: (* INC *) 912 (* XXX: work on the right hand side *) 913 (* XXX: switch to the left hand side *) 914 >EQs >EQticks <instr_refl >EQP -P normalize nodelta 915 @(subaddressing_mode_elim … addr) normalize nodelta 916 [1: 917 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 918 whd in maps_assm:(??%%); 919 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 920 [2: normalize nodelta #absurd destruct(absurd) ] 921 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 922 whd in ⊢ (??%?); 923 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 924 whd in ⊢ (??%?); 925 inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta 926 @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl)) 927 [1: 928 @eq_f2 try % 929 @(pose … (set_clock ????)) #status #status_refl 930 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 931 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 932 |2: 933 @set_arg_8_status_of_pseudo_status try % 934 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 935 ] 936 |2: 937 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 938 whd in maps_assm:(??%%); 939 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 940 [2: normalize nodelta #absurd destruct(absurd) ] 941 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 942 whd in ⊢ (??%?); 943 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 944 whd in ⊢ (??%?); 945 @let_pair_in_status_of_pseudo_status 946 [1: 947 @eq_f2 try % 948 @(pose … (set_clock ????)) #status #status_refl 949 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 950 >EQs >EQticks 951 [1: 952 @sym_eq @set_clock_status_of_pseudo_status % 953 |2: 954 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 955 |3: 956 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) % 957 ] 958 |2: 959 #carry #result 960 @sym_eq @set_arg_8_status_of_pseudo_status try % 961 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 962 ] 963 |3: 964 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 965 whd in maps_assm:(??%%); 966 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 967 [2: normalize nodelta #absurd destruct(absurd) ] 968 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 969 whd in ⊢ (??%?); 970 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 971 whd in ⊢ (??%?); 972 @let_pair_in_status_of_pseudo_status 973 [1: 974 @eq_f2 try % 975 @(pose … (set_clock ????)) #status #status_refl 976 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 977 >EQs >EQticks 978 [1: 979 @sym_eq @set_clock_status_of_pseudo_status % 980 |2: 981 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 982 |3: 983 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) % 984 ] 985 |2: 986 #carry #result 987 @sym_eq @set_arg_8_status_of_pseudo_status try % 988 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 989 ] 990 |4: 991 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 992 whd in maps_assm:(??%%); 993 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 994 [2: normalize nodelta #absurd destruct(absurd) ] 995 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 996 whd in ⊢ (??%?); 997 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 998 whd in ⊢ (??%?); 999 @let_pair_in_status_of_pseudo_status 1000 [1: 1001 @eq_f2 try % 1002 @(pose … (set_clock ????)) #status #status_refl 1003 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 1004 >EQs >EQticks 1005 [1: 1006 @sym_eq @set_clock_status_of_pseudo_status % 1007 |2: 1008 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % 1009 |3: 1010 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 1011 ] 1012 |2: 1013 #carry #result 1014 @sym_eq @set_arg_8_status_of_pseudo_status try % 1015 [1: 1016 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 1017 |2: 1018 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % 1019 ] 1020 ] 1021 |5: 1022 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1023 whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1024 whd in ⊢ (??%?); 1025 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1026 whd in ⊢ (??%?); 1027 @let_pair_in_status_of_pseudo_status 1028 [1: 1029 @eq_f2 try % 1030 @(pose … (set_clock ????)) #status #status_refl 1031 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl 1032 >EQs >EQticks % 1033 |2: 1034 #carry #bl 1035 @sym_eq @let_pair_in_status_of_pseudo_status 1036 [1: 1037 @eq_f3 try % 1038 @(pose … (set_clock ????)) #status #status_refl 1039 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl 1040 >EQs >EQticks % 1041 |2: 1042 #carry' #bu 1043 @sym_eq @set_8051_sfr_status_of_pseudo_status % 1044 ] 1045 ] 1046 ] 1047 |5: (* DEC *) 1048 >EQs >EQticks <instr_refl >EQP -P normalize nodelta 1049 @(subaddressing_mode_elim … addr) normalize nodelta 1050 [1: 1051 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1052 whd in maps_assm:(??%%); 1053 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1054 [2: normalize nodelta #absurd destruct(absurd) ] 1055 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1056 whd in ⊢ (??%?); 1057 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1058 whd in ⊢ (??%?); 1059 @let_pair_in_status_of_pseudo_status 1060 [1: 1061 @eq_f3 try % 1062 @(pose … (set_clock ????)) #status #status_refl 1063 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 1064 >EQs >EQticks try % 1065 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 1066 |2: 1067 #result #flags 1068 @sym_eq @set_arg_8_status_of_pseudo_status try % 1069 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 1070 ] 1071 |2: 1072 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1073 whd in maps_assm:(??%%); 1074 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1075 [2: normalize nodelta #absurd destruct(absurd) ] 1076 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1077 whd in ⊢ (??%?); 1078 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1079 whd in ⊢ (??%?); 1080 @let_pair_in_status_of_pseudo_status 1081 [1: 1082 @eq_f3 try % 1083 @(pose … (set_clock ????)) #status #status_refl 1084 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 1085 >EQs >EQticks try % 1086 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 1087 |2: 1088 #result #flags 1089 @sym_eq @set_arg_8_status_of_pseudo_status try % 1090 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 1091 ] 1092 |3: 1093 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1094 whd in maps_assm:(??%%); 1095 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1096 [2: normalize nodelta #absurd destruct(absurd) ] 1097 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1098 whd in ⊢ (??%?); 1099 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1100 whd in ⊢ (??%?); 1101 @let_pair_in_status_of_pseudo_status 1102 [1: 1103 @eq_f3 try % 1104 @(pose … (set_clock ????)) #status #status_refl 1105 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 1106 >EQs >EQticks try % 1107 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 1108 |2: 1109 #result #flags 1110 @sym_eq @set_arg_8_status_of_pseudo_status try % 1111 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 1112 ] 1113 |4: 1114 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1115 whd in maps_assm:(??%%); 1116 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1117 [2: normalize nodelta #absurd destruct(absurd) ] 1118 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1119 whd in ⊢ (??%?); 1120 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1121 whd in ⊢ (??%?); 1122 @let_pair_in_status_of_pseudo_status 1123 [1: 1124 @eq_f3 try % 1125 @(pose … (set_clock ????)) #status #status_refl 1126 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 1127 >EQs >EQticks try % 1128 [1: 1129 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % 1130 |2: 1131 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 1132 ] 1133 |2: 1134 #result #flags 1135 @sym_eq @set_arg_8_status_of_pseudo_status try % 1136 [1: 1137 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 1138 |2: 1139 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % 1140 ] 1141 ] 1142 ] 1143 |6: (* MUL *) 1215 1144 (* XXX: work on the right hand side *) 1216 1145 (* XXX: switch to the left hand side *) … … 1254 1183 ] 1255 1184 @sym_eq @set_program_counter_status_of_pseudo_status % 1256 | 11,12: (* DIV *)1185 |7,8: (* DIV *) 1257 1186 (* XXX: work on the right hand side *) 1258 1187 (* XXX: switch to the left hand side *) … … 1268 1197 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 1269 1198 whd in ⊢ (??%?); normalize nodelta 1270 cases daemon (* XXX: need match_nat_replace but is not working! *) 1271 |13: (* DA *) 1199 @(match_nat_status_of_pseudo_status M' cm sigma policy) 1200 [1,4: 1201 @eq_f 1202 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1203 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1204 |2,5: 1205 @sym_eq @set_flags_status_of_pseudo_status % 1206 |3,6: 1207 #n @sym_eq @set_flags_status_of_pseudo_status try % 1208 @sym_eq @set_8051_sfr_status_of_pseudo_status 1209 [1,3: 1210 @sym_eq @set_8051_sfr_status_of_pseudo_status try % 1211 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta 1212 @eq_f @eq_f2 try % @eq_f 1213 @(pose … (set_clock ????)) #status #status_refl 1214 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1215 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1216 |2,4: 1217 whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f 1218 @(pose … (set_clock ????)) #status #status_refl 1219 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1220 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1221 ] 1222 ] 1223 |9: (* DA *) 1272 1224 (* XXX: work on the right hand side *) 1273 1225 (* XXX: switch to the left hand side *) … … 1353 1305 ] 1354 1306 ] 1355 |1 4: (* DA *)1307 |10: (* DA *) 1356 1308 (* XXX: work on the right hand side *) 1357 1309 (* XXX: switch to the left hand side *) … … 1411 1363 ] 1412 1364 ] 1413 |1 5: (* DA *)1365 |11: (* DA *) 1414 1366 (* XXX: work on the right hand side *) 1415 1367 (* XXX: switch to the left hand side *) … … 1456 1408 ] 1457 1409 ] 1458 |36: (* CLR *) 1410 |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1411 cases daemon 1412 |29,30: (* ANL and ORL *) 1413 inversion addr 1414 [1,3: 1415 * 1416 [1,3: 1417 #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl 1418 >EQP -P normalize nodelta 1419 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1420 whd in maps_assm:(??%%); 1421 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1422 [2,4: normalize nodelta #absurd destruct(absurd) ] 1423 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1424 [2,4: normalize nodelta #absurd destruct(absurd) ] 1425 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1426 whd in ⊢ (??%?); 1427 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1428 change with (set_arg_8 ????? = ?) 1429 @set_arg_8_status_of_pseudo_status try % 1430 >EQs >EQticks <instr_refl >addr_refl 1431 [1,4: 1432 @sym_eq @set_clock_status_of_pseudo_status 1433 [1,3: 1434 @sym_eq @set_program_counter_status_of_pseudo_status % 1435 |2,4: 1436 @eq_f2 % 1437 ] 1438 |2,5: 1439 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 1440 [1,3: @(subaddressing_mode_elim … acc_a) % ] % 1441 |3,6: 1442 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 1443 [1,5: 1444 @(subaddressing_mode_elim … acc_a) % 1445 |4,8: 1446 @eq_f2 1447 @(pose … (set_clock ????)) #status #status_refl 1448 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1449 [1,5: 1450 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 1451 [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ] 1452 |3,7: 1453 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1454 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1455 |2,6: 1456 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 1457 [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ] 1458 |4,8: 1459 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1460 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1461 ] 1462 |*: 1463 % 1464 ] 1465 ] 1466 |2,4: 1467 #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl 1468 >EQP -P normalize nodelta 1469 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1470 whd in maps_assm:(??%%); 1471 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1472 [2,4: normalize nodelta #absurd destruct(absurd) ] 1473 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1474 [2,4: normalize nodelta #absurd destruct(absurd) ] 1475 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1476 whd in ⊢ (??%?); 1477 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1478 change with (set_arg_8 ????? = ?) 1479 @set_arg_8_status_of_pseudo_status try % 1480 >EQs >EQticks <instr_refl >addr_refl 1481 [1,4: 1482 @sym_eq @set_clock_status_of_pseudo_status 1483 [1,3: 1484 @sym_eq @set_program_counter_status_of_pseudo_status % 1485 |2,4: 1486 @eq_f2 % 1487 ] 1488 |2,5: 1489 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 1490 [1,3: @(subaddressing_mode_elim … direct) #w % ] % 1491 |3,6: 1492 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 1493 [1,5: 1494 @(subaddressing_mode_elim … direct) #w % 1495 |4,8: 1496 @eq_f2 1497 @(pose … (set_clock ????)) #status #status_refl 1498 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1499 [1,5: 1500 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 1501 [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ] 1502 |3,7: 1503 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1504 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1505 |2,6: 1506 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 1507 [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ] 1508 |4,8: 1509 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1510 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1511 ] 1512 |*: 1513 % 1514 ] 1515 ] 1516 ] 1517 |2,4: 1518 #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl 1519 >EQP -P normalize nodelta 1520 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1521 whd in maps_assm:(??%%); 1522 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1523 [2,4: normalize nodelta #absurd destruct(absurd) ] 1524 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1525 [2,4: normalize nodelta #absurd destruct(absurd) ] 1526 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1527 whd in ⊢ (??%?); 1528 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1529 change with (set_flags ?????? = ?) 1530 [1,4: @set_flags_status_of_pseudo_status try % |*: skip ] 1531 >EQs >EQticks <instr_refl >addr_refl 1532 @sym_eq @set_clock_status_of_pseudo_status % 1533 ] 1534 |31: (* XRL *) 1535 inversion addr 1536 [1: 1537 #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl 1538 >EQP -P normalize nodelta 1539 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1540 whd in maps_assm:(??%%); 1541 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1542 [2: normalize nodelta #absurd destruct(absurd) ] 1543 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1544 [2: normalize nodelta #absurd destruct(absurd) ] 1545 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1546 whd in ⊢ (??%?); 1547 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1548 change with (set_arg_8 ????? = ?) 1549 @set_arg_8_status_of_pseudo_status try % 1550 >EQs >EQticks <instr_refl >addr_refl 1551 [1: 1552 @sym_eq @set_clock_status_of_pseudo_status 1553 [1: 1554 @sym_eq @set_program_counter_status_of_pseudo_status % 1555 |2: 1556 @eq_f2 % 1557 ] 1558 |2: 1559 @(subaddressing_mode_elim … acc_a) @I 1560 |3: 1561 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 1562 [1: 1563 @(subaddressing_mode_elim … acc_a) % 1564 |4: 1565 @eq_f2 1566 @(pose … (set_clock ????)) #status #status_refl 1567 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1568 [1: 1569 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 1570 [1: @(subaddressing_mode_elim … acc_a) % |*: % ] 1571 |3: 1572 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1573 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1574 |2: 1575 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 1576 [1: @(subaddressing_mode_elim … acc_a) % |2: % ] 1577 |4: 1578 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1579 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1580 ] 1581 |*: 1582 % 1583 ] 1584 ] 1585 |2: 1586 #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl 1587 >EQP -P normalize nodelta 1588 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1589 whd in maps_assm:(??%%); 1590 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1591 [2: normalize nodelta #absurd destruct(absurd) ] 1592 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1593 [2: normalize nodelta #absurd destruct(absurd) ] 1594 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1595 whd in ⊢ (??%?); 1596 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1597 change with (set_arg_8 ????? = ?) 1598 @set_arg_8_status_of_pseudo_status try % 1599 >EQs >EQticks <instr_refl >addr_refl 1600 [1: 1601 @sym_eq @set_clock_status_of_pseudo_status 1602 [1: 1603 @sym_eq @set_program_counter_status_of_pseudo_status % 1604 |2: 1605 @eq_f2 % 1606 ] 1607 |2: 1608 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 1609 [1: @(subaddressing_mode_elim … direct) #w % ] % 1610 |3: 1611 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 1612 [1: 1613 @(subaddressing_mode_elim … direct) #w % 1614 |4: 1615 @eq_f2 1616 @(pose … (set_clock ????)) #status #status_refl 1617 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1618 [1: 1619 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 1620 [1: @(subaddressing_mode_elim … direct) #w % |*: % ] 1621 |3: 1622 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1623 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1624 |2: 1625 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 1626 [1: @(subaddressing_mode_elim … direct) #w % |2: % ] 1627 |4: 1628 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1629 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1630 ] 1631 |*: 1632 % 1633 ] 1634 ] 1635 ] 1636 |32: (* CLR *) 1459 1637 >EQP -P normalize nodelta 1460 1638 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1477 1655 [2: <EQaddr % ] % 1478 1656 ] 1479 |3 7: (* CLR *)1657 |33: (* CLR *) 1480 1658 >EQP -P normalize nodelta 1481 1659 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1492 1670 @sym_eq @set_clock_status_of_pseudo_status 1493 1671 >EQs >EQticks <instr_refl % 1494 |3 8: (* CLR *)1672 |34: (* CLR *) 1495 1673 >EQP -P normalize nodelta 1496 1674 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1509 1687 >EQs >EQticks <instr_refl % 1510 1688 |*: 1511 (* XXX: ??? *) 1512 cases daemon 1513 ] 1514 |39: (* CPL *) 1689 cases daemon (* XXX: requires changes to addressing_mode_ok *) 1690 ] 1691 |35: (* CPL *) 1515 1692 >EQP -P normalize nodelta 1516 1693 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1537 1714 [2: <EQaddr % ] % 1538 1715 ] 1539 | 40: (* CPL *)1716 |36: (* CPL *) 1540 1717 >EQP -P normalize nodelta 1541 1718 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1558 1735 >EQs >EQticks <instr_refl <EQaddr % 1559 1736 ] 1560 | 41: (* CPL *)1737 |37: (* CPL *) 1561 1738 >EQP -P normalize nodelta 1562 1739 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1579 1756 @sym_eq @set_clock_status_of_pseudo_status % 1580 1757 |2: 1581 (* XXX: ??? *) 1582 cases daemon 1758 cases daemon (* XXX: require changes to addressing_mode_ok *) 1583 1759 ] 1584 1760 |2: … … 1586 1762 >EQs >EQticks <instr_refl <EQaddr % 1587 1763 |*: 1588 (* XXX: same as above, provable but tedious *) 1589 cases daemon 1590 ] 1591 |33: (* (* ANL *) 1764 cases daemon (* XXX: require changes to addressing_mode_ok *) 1765 ] 1766 |38,40: (* RL and RR *) 1592 1767 (* XXX: work on the right hand side *) 1593 1768 (* XXX: switch to the left hand side *) 1594 >EQP -P normalize nodelta lapply instr_refl 1595 inversion addr 1596 [1: 1597 #addr' #addr_refl' 1598 inversion addr' 1599 #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm 1600 whd in ⊢ (??%? → ?); normalize nodelta cases addr 1601 [1: 1602 #acc_a #others normalize nodelta 1603 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1604 [2: normalize nodelta #absurd destruct(absurd) ] 1605 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1606 [2: normalize nodelta #absurd destruct(absurd) ] 1607 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1608 whd in ⊢ (??%?); 1609 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1610 whd in ⊢ (??%?); normalize nodelta 1611 inversion addr #addr1 #addr2 1612 @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a) 1613 @(subaddressing_mode_elim … addr2) 1614 @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try % 1615 [1: 1616 @sym_eq @set_clock_status_of_pseudo_status 1617 >EQs >EQticks <addr_refl <instr_refl 1618 [1: 1619 @sym_eq @set_program_counter_status_of_pseudo_status % 1620 |2: 1621 @eq_f2 1622 [1: 1623 >addr_refl @(subaddressing_mode_elim … addr1) % 1624 |2: 1625 @(clock_status_of_pseudo_status M') 1626 @sym_eq @set_program_counter_status_of_pseudo_status % 1627 ] 1628 ] 1629 |2: 1630 cases daemon (* XXX: matita dies here *) 1631 ] 1632 |2: 1633 #direct #others 1634 @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta 1635 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1636 [2: normalize nodelta #absurd destruct(absurd) ] 1637 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1638 [2: normalize nodelta #absurd destruct(absurd) ] 1639 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1640 whd in ⊢ (??%?); 1641 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1642 whd in ⊢ (??%?); normalize nodelta 1643 inversion addr #addr1 #addr2 1644 @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2) 1645 [1: #w |2: #w1 #w2 ] #addr_refl normalize nodelta 1646 @set_arg_8_status_of_pseudo_status 1647 ] 1648 |2: 1649 -addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm 1650 whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta 1651 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1 1652 [2: normalize nodelta #absurd destruct(absurd) ] 1653 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1654 [2: normalize nodelta #absurd destruct(absurd) ] 1655 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1656 whd in ⊢ (??%?); 1657 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1658 whd in ⊢ (??%?); normalize nodelta 1659 inversion addr #addr1 #addr2 #addr_refl normalize nodelta 1660 @set_flags_status_of_pseudo_status try % 1661 [1: 1662 @conjunction_split 1663 [1: 1664 @(get_cy_flag_status_of_pseudo_status M') 1665 @sym_eq @set_clock_status_of_pseudo_status 1666 >EQs >EQticks <addr_refl <instr_refl % 1667 |2: 1668 >EQs >EQticks <addr_refl <instr_refl normalize nodelta 1669 (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *) 1670 cases daemon 1671 ] 1672 |2: 1673 @(get_ov_flag_status_of_pseudo_status M') 1674 @sym_eq @set_clock_status_of_pseudo_status 1675 >EQs >EQticks <instr_refl <addr_refl % 1676 |3: 1677 @sym_eq @set_clock_status_of_pseudo_status 1678 >EQs >EQticks <instr_refl <addr_refl % 1679 ] 1680 ] 1769 >EQP -P normalize nodelta 1770 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1771 whd in maps_assm:(??%%); 1772 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1773 [2,4: normalize nodelta #absurd destruct(absurd) ] 1774 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1775 whd in ⊢ (??%?); 1776 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 1777 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1778 [2,4: 1779 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1780 @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1781 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1782 % 1783 ] 1784 @sym_eq @set_clock_status_of_pseudo_status 1785 [2,4: 1786 % 1787 ] 1788 @sym_eq @set_program_counter_status_of_pseudo_status % 1789 |39,41: (* RLC and RRC *) 1790 (* XXX: work on the right hand side *) 1791 (* XXX: switch to the left hand side *) 1792 >EQP -P normalize nodelta 1793 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1794 whd in maps_assm:(??%%); 1795 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1796 [2,4: normalize nodelta #absurd destruct(absurd) ] 1797 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1798 whd in ⊢ (??%?); 1799 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 1800 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1801 [2,4: 1802 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1803 @eq_f2 1804 [1,3: 1805 @sym_eq 1806 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1807 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1808 |2,4: 1809 @sym_eq @(get_cy_flag_status_of_pseudo_status … M') 1810 @sym_eq @set_clock_status_of_pseudo_status % 1811 ] 1812 |1,3: 1813 @sym_eq @set_arg_1_status_of_pseudo_status try % 1814 @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1815 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1816 ] 1817 |*)42: (* SWAP *) 1818 |43: (* MOV *) 1819 |44: (* MOVX *) 1820 |45: (* SETB *) 1821 >EQP -P normalize nodelta 1822 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1681 1823 whd in maps_assm:(??%%); 1682 1824 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 … … 1685 1827 whd in ⊢ (??%?); 1686 1828 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1687 whd in ⊢ (??%?); normalize nodelta *) 1688 |16: (* JC *) 1689 (* XXX: work on the right hand side *) 1690 (* XXX: switch to the left hand side *) 1829 change with (set_arg_1 ????? = ?) 1830 >EQs >EQticks <instr_refl 1831 @set_arg_1_status_of_pseudo_status try % 1832 lapply addressing_mode_ok_assm_1 (* XXX: move into a lemma *) 1833 @(subaddressing_mode_elim … b) 1834 [1,3: 1835 #_ @I 1836 |2,4: 1837 #w cases daemon 1838 (* XXX: need changes to addressing_mode_ok *) 1839 ] 1840 |46: (* PUSH *) 1691 1841 >EQP -P normalize nodelta 1692 #sigma_increment_commutation #maps_assm 1693 whd in match expand_pseudo_instruction; normalize nodelta 1694 whd in match expand_relative_jump; normalize nodelta 1695 whd in match expand_relative_jump_internal; normalize nodelta 1696 @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta 1697 inversion sj_possible #sj_possible_refl 1842 #sigma_increment_commutation whd in ⊢ (??%% → ?); 1843 inversion M #callM #accM #callM_accM_refl normalize nodelta 1844 @(subaddressing_mode_elim … addr) #w normalize nodelta 1845 @Some_Some_elim #Mrefl destruct(Mrefl) 1846 cases daemon (* XXX *) 1847 |47: (* POP *) 1848 |48: (* XCH *) 1849 >EQP -P normalize nodelta 1850 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1851 whd in maps_assm:(??%%); 1852 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1853 [2: normalize nodelta #absurd destruct(absurd) ] 1854 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1855 [2: normalize nodelta #absurd destruct(absurd) ] 1856 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1857 whd in ⊢ (??%?); 1858 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1859 change with (set_arg_8 ????? = ?) 1860 >EQs >EQticks <instr_refl 1861 @set_arg_8_status_of_pseudo_status try % 1698 1862 [1: 1699 #fetch_many_assm %{1} 1700 whd in maps_assm:(??%%); 1701 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1702 whd in ⊢ (??%?); normalize nodelta 1703 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1704 whd in ⊢ (??%?); normalize nodelta 1705 @(if_then_else_replace ???????? p) normalize nodelta 1863 @sym_eq @set_8051_sfr_status_of_pseudo_status try % 1864 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta 1865 @(pose … (set_clock ????)) #status #status_refl 1866 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1706 1867 [1: 1707 >EQs @(get_cy_flag_status_of_pseudo_status M')1708 @sym_eq @set_program_counter_status_of_pseudo_status %1868 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 1869 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1709 1870 |2: 1710 @(if_then_else_replace ???????? p) normalize nodelta try % 1871 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 1872 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1873 ] 1874 |2: 1875 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 1876 [1: 1877 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 1878 |*: 1879 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 1880 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 1881 whd in match sfr_8051_index; normalize nodelta 1882 >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % 1883 ] 1884 |3: 1885 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 1886 [1: 1887 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 1888 |2: 1889 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 1890 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 1891 whd in match sfr_8051_index; normalize nodelta 1892 >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % 1893 |3: 1894 @(pose … (set_clock ????)) #status #status_refl 1895 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1896 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1897 ] 1898 ] 1899 |49: (* XCHD *) 1900 >EQP -P normalize nodelta 1901 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1902 whd in maps_assm:(??%%); 1903 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1904 [2: normalize nodelta #absurd destruct(absurd) ] 1905 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1906 [2: normalize nodelta #absurd destruct(absurd) ] 1907 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1908 whd in ⊢ (??%?); 1909 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1910 whd in ⊢ (??%?); 1911 @(pair_replace ?????????? p) normalize nodelta 1912 >EQs >EQticks <instr_refl 1913 [1: 1914 @eq_f 1915 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1916 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1917 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1918 |2: 1919 @(pair_replace ?????????? p1) normalize nodelta 1920 >EQs >EQticks <instr_refl 1921 [1: 1922 @eq_f 1923 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1924 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1925 [1: 1926 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 1927 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1928 |2: 1929 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 1930 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ] 1931 ] 1932 |2: 1933 @(pair_replace ?????????? p) normalize nodelta 1711 1934 >EQs >EQticks <instr_refl 1712 @set_program_counter_status_of_pseudo_status 1713 [1: 1714 >EQaddr_of normalize nodelta 1715 whd in match addr_of_relative; normalize nodelta 1716 whd in match (program_counter ???); 1717 check address_of_word_labels_code_mem_Some_hit 1718 >EQlookup_labels 1719 1720 >sigma_increment_commutation 1721 whd in match assembly_1_pseudoinstruction; normalize nodelta 1722 whd in match expand_pseudo_instruction; normalize nodelta 1723 whd in match expand_relative_jump; normalize nodelta 1724 whd in match expand_relative_jump_internal; normalize nodelta 1725 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1935 [1: 1936 % 1937 |2: 1938 @(pair_replace ?????????? p1) normalize nodelta 1939 >EQs >EQticks <instr_refl 1726 1940 [1: 1727 >EQppc%1941 % 1728 1942 |2: 1729 >sj_possible_refl normalize nodelta normalize in match (length ??); 1730 lapply sigma_increment_commutation 1731 whd in match assembly_1_pseudoinstruction; normalize nodelta 1732 whd in match (length ??); normalize nodelta 1733 cases daemon 1734 (* XXX: missing invariant? *) 1735 ] 1736 |2: 1737 @sym_eq @set_clock_status_of_pseudo_status try % 1738 @eq_f2 try % whd in ⊢ (??%%); 1739 whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation 1740 whd in match assembly_1_pseudoinstruction; normalize nodelta 1741 whd in match expand_pseudo_instruction; normalize nodelta 1742 whd in match expand_relative_jump; normalize nodelta 1743 whd in match expand_relative_jump_internal; normalize nodelta 1744 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1745 [1: 1746 @eq_f2 try % >EQppc % 1747 |2: 1748 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1943 @set_arg_8_status_of_pseudo_status try % 1749 1944 [1: 1750 @ eq_f2 try % (* XXX: finish, use Jaap's invariant *)1751 cases daemon1945 @sym_eq @set_8051_sfr_status_of_pseudo_status try % 1946 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1752 1947 |2: 1753 #_ >sj_possible_refl % 1948 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 1949 [1: 1950 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 1951 |2: 1952 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 1953 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 1954 whd in match sfr_8051_index; normalize nodelta 1955 >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % 1956 ] 1957 |3: 1958 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 1959 [1: 1960 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 1961 |2: 1962 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 1963 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 1964 whd in match sfr_8051_index; normalize nodelta 1965 >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % 1966 ] 1754 1967 ] 1755 1968 ] 1756 1969 ] 1757 1970 ] 1971 ] 1972 |*)50: (* RET *) 1973 >EQP -P normalize nodelta 1974 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1975 whd in maps_assm:(??%%); normalize nodelta in maps_assm; 1976 lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta 1977 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1 1978 [2: normalize nodelta #absurd destruct(absurd) ] 1979 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2 1980 [2: normalize nodelta #absurd destruct(absurd) ] 1981 normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl) 1982 whd in ⊢ (??%?); 1983 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1984 whd in ⊢ (??%?); 1985 @(pair_replace ?????????? p) normalize nodelta 1986 >EQs >EQticks <instr_refl 1987 [1: 1988 @eq_f3 try % 1989 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1990 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl % 1758 1991 |2: 1759 normalize nodelta >EQppc 1760 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1761 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1762 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1763 #fetch_many_assm whd in fetch_many_assm; %{2} 1764 change with (execute_1 ?? = ?) 1765 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1766 #status_after_1 #EQstatus_after_1 1767 cases daemon (* XXX: ??? *) 1768 ] 1769 ] 1992 @(pair_replace ?????????? p1) normalize nodelta 1993 >EQs >EQticks <instr_refl 1994 [1: 1995 @eq_f3 try % 1996 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1997 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl 1998 [1: 1999 cases daemon 2000 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) 2001 |2: 2002 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 2003 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 2004 whd in match sfr_8051_index; normalize nodelta 2005 >get_index_v_set_index_hit 2006 change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp) 2007 cases daemon 2008 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) 2009 ] 2010 |2: 2011 cases daemon (* XXX *) 2012 ] 2013 ] 2014 |51: (* RETI *) 2015 |52: (* NOP *) 2016 >EQP -P normalize nodelta 2017 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2018 whd in maps_assm:(??%%); 2019 lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl) 2020 whd in ⊢ (??%?); 2021 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 2022 change with (set_clock ???? = ?) 2023 @set_clock_status_of_pseudo_status % 2024 ] 1770 2025 qed. 1771 2026
Note: See TracChangeset
for help on using the changeset viewer.