- Timestamp:
- Jul 18, 2012, 5:30:26 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2210 r2212 445 445 ] 446 446 | INC addr ⇒ λinstr_refl. 447 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm.? with447 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with 448 448 [ ACC_A ⇒ λacc_a: True. λEQaddr. 449 449 let s' ≝ add_ticks1 s in … … 767 767 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 768 768 whd in match execute_1_preinstruction; normalize nodelta 769 [ 35: (* XRL *)769 [(* 35: (* XRL *) 770 770 inversion addr 771 771 [1: … … 869 869 ] 870 870 ] 871 |4,5,6,7,8,9: (* INC and DEC *) 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 *) 872 1034 cases daemon 873 1035 |42,44: (* RL and RR *) -
src/ASM/Interpret.ma
r2160 r2212 159 159 ] 160 160 | INC addr ⇒ λinstr_refl. 161 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm.? with161 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with 162 162 [ ACC_A ⇒ λacc_a: True. 163 163 let s' ≝ add_ticks1 s in … … 231 231 s 232 232 | CLR addr ⇒ λinstr_refl. 233 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm.? with233 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 234 234 [ ACC_A ⇒ λacc_a: True. 235 235 let s ≝ add_ticks1 s in … … 244 244 ] (subaddressing_modein … addr) 245 245 | CPL addr ⇒ λinstr_refl. 246 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm.? with246 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 247 247 [ ACC_A ⇒ λacc_a: True. 248 248 let s ≝ add_ticks1 s in … … 298 298 set_8051_sfr … s SFR_ACC_A new_acc 299 299 | PUSH addr ⇒ λinstr_refl. 300 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm.? with300 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 301 301 [ DIRECT d ⇒ λdirect: True. 302 302 let s ≝ add_ticks1 s in
Note: See TracChangeset
for help on using the changeset viewer.