Changeset 2017
 Timestamp:
 Jun 4, 2012, 5:38:43 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1985 r2017 77 77 qed. 78 78 79 lemma get_8051_sfr_set_program_counter: 80 ∀M: Type[0]. 81 ∀cm: M. 82 ∀s: PreStatus M cm. 83 ∀sfr: SFR8051. 84 ∀pc: Word. 85 get_8051_sfr M cm (set_program_counter M cm s pc) = 86 get_8051_sfr M cm s. 87 #M #cm #s #sfr #pc % 88 qed. 89 79 90 lemma special_function_registers_8051_set_arg_16: 80 91 ∀M, M': Type[0]. … … 119 130 qed. 120 131 132 lemma get_ov_flag_set_program_counter: 133 ∀M: Type[0]. 134 ∀cm: M. 135 ∀s: PreStatus M cm. 136 ∀pc: Word. 137 get_ov_flag M cm (set_program_counter M cm s pc) = 138 get_ov_flag M cm s. 139 #M #cm #s #pc % 140 qed. 141 142 lemma external_ram_set_program_counter: 143 ∀M: Type[0]. 144 ∀cm: M. 145 ∀s: PreStatus M cm. 146 ∀pc: Word. 147 external_ram M cm (set_program_counter M cm s pc) = 148 external_ram M cm s. 149 #M #cm #s #pc % 150 qed. 151 152 lemma low_internal_ram_set_program_counter: 153 ∀M: Type[0]. 154 ∀cm: M. 155 ∀s: PreStatus M cm. 156 ∀pc: Word. 157 low_internal_ram M cm (set_program_counter M cm s pc) = 158 low_internal_ram M cm s. 159 #M #cm #s #pc % 160 qed. 161 162 lemma high_internal_ram_set_program_counter: 163 ∀M: Type[0]. 164 ∀cm: M. 165 ∀s: PreStatus M cm. 166 ∀pc: Word. 167 high_internal_ram M cm (set_program_counter M cm s pc) = 168 high_internal_ram M cm s. 169 #M #cm #s #pc % 170 qed. 171 172 lemma get_arg_8_set_program_counter: 173 ∀M: Type[0]. 174 ∀cm: M. 175 ∀s: PreStatus M cm. 176 ∀flag: bool. 177 ∀addr. 178 ∀pc: Word. 179 get_arg_8 M cm (set_program_counter M cm s pc) flag addr = 180 get_arg_8 M cm s flag addr. 181 #M #cm #s #flag #addr #pc 182 whd in match get_arg_8; normalize nodelta 183 cases addr * 184 try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I) 185 try (#addr1 #absurd normalize in absurd; cases absurd @I) 186 try (#absurd normalize in absurd; cases absurd @I) 187 try (#addr1 #addr2) try #addr1 188 normalize nodelta try % 189 >external_ram_set_program_counter 190 >program_counter_set_program_counter 191 cases daemon (* XXX: rewrite not working but provable *) 192 qed. 193 194 lemma external_ram_set_flags: 195 ∀M: Type[0]. 196 ∀cm: M. 197 ∀s: PreStatus M cm. 198 ∀opt: option Bit. 199 ∀bit1, bit2: Bit. 200 external_ram M cm (set_flags M cm s bit1 opt bit2) = 201 external_ram M cm s. 202 #M #cm #s #opt #bit1 #bit2 % 203 qed. 204 205 lemma low_internal_ram_set_flags: 206 ∀M: Type[0]. 207 ∀cm: M. 208 ∀s: PreStatus M cm. 209 ∀opt: option Bit. 210 ∀bit1, bit2: Bit. 211 low_internal_ram M cm (set_flags M cm s bit1 opt bit2) = 212 low_internal_ram M cm s. 213 #M #cm #s #opt #bit1 #bit2 % 214 qed. 215 216 lemma high_internal_ram_set_flags: 217 ∀M: Type[0]. 218 ∀cm: M. 219 ∀s: PreStatus M cm. 220 ∀opt: option Bit. 221 ∀bit1, bit2: Bit. 222 high_internal_ram M cm (set_flags M cm s bit1 opt bit2) = 223 high_internal_ram M cm s. 224 #M #cm #s #opt #bit1 #bit2 % 225 qed. 226 227 lemma low_internal_ram_set_clock: 228 ∀M: Type[0]. 229 ∀cm: M. 230 ∀s: PreStatus M cm. 231 ∀t: Time. 232 low_internal_ram M cm (set_clock M cm s t) = 233 low_internal_ram M cm s. 234 #M #cm #s #t % 235 qed. 236 237 lemma high_internal_ram_set_clock: 238 ∀M: Type[0]. 239 ∀cm: M. 240 ∀s: PreStatus M cm. 241 ∀t: Time. 242 high_internal_ram M cm (set_clock M cm s t) = 243 high_internal_ram M cm s. 244 #M #cm #s #t % 245 qed. 246 247 lemma external_ram_set_clock: 248 ∀M: Type[0]. 249 ∀cm: M. 250 ∀s: PreStatus M cm. 251 ∀t: Time. 252 external_ram M cm (set_clock M cm s t) = 253 external_ram M cm s. 254 #M #cm #s #t % 255 qed. 256 257 lemma set_8051_sfr_set_program_counter: 258 ∀M: Type[0]. 259 ∀cm: M. 260 ∀s: PreStatus M cm. 261 ∀pc: Word. 262 ∀sfr: SFR8051. 263 ∀v: Byte. 264 set_8051_sfr M cm (set_program_counter M cm s pc) sfr v = 265 set_program_counter M cm (set_8051_sfr M cm s sfr v) pc. 266 #M #cm #s #pc #sfr #v % 267 qed. 268 269 lemma low_internal_ram_set_8051_sfr: 270 ∀M: Type[0]. 271 ∀cm: M. 272 ∀s: PreStatus M cm. 273 ∀sfr: SFR8051. 274 ∀v: Byte. 275 low_internal_ram M cm (set_8051_sfr M cm s sfr v) = 276 low_internal_ram M cm s. 277 #M #cm #s #sfr #v % 278 qed. 279 280 lemma high_internal_ram_set_8051_sfr: 281 ∀M: Type[0]. 282 ∀cm: M. 283 ∀s: PreStatus M cm. 284 ∀sfr: SFR8051. 285 ∀v: Byte. 286 high_internal_ram M cm (set_8051_sfr M cm s sfr v) = 287 high_internal_ram M cm s. 288 #M #cm #s #sfr #v % 289 qed. 290 291 lemma external_ram_set_8051_sfr: 292 ∀M: Type[0]. 293 ∀cm: M. 294 ∀s: PreStatus M cm. 295 ∀sfr: SFR8051. 296 ∀v: Byte. 297 external_ram M cm (set_8051_sfr M cm s sfr v) = 298 external_ram M cm s. 299 #M #cm #s #sfr #v % 300 qed. 301 302 lemma get_arg_8_set_clock: 303 ∀M: Type[0]. 304 ∀cm: M. 305 ∀s: PreStatus M cm. 306 ∀addr. 307 ∀t: Time. 308 get_arg_8 M cm (set_clock M cm s t) addr = 309 get_arg_8 M cm s addr. 310 #M #cm #s #addr #t % 311 qed. 312 121 313 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 122 314 #P #A #a #abs destruct … … 194 386 cases (eq_bv_eq … fetch_many_assm) assumption 195 387 qed. 388 389 lemma refl_to_jmrefl: 390 ∀a: Type[0]. 391 ∀l, r: a. 392 l = r → l ≃ r. 393 #a #l #r #refl destruct % 394 qed. 395 396 include alias "ASM/Vector.ma". 196 397 197 398 lemma main_lemma_preinstruction: … … 654 855 s 655 856 ] (refl … instr)) 656 try (cases(other)) 657 try assumption (*20s*) 658 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 659 try ( 660 @(execute_1_technical … (subaddressing_modein …)) 661 @I 662 ) (*66s*) 663 whd in match execute_1_preinstruction; normalize nodelta 664 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 857 try (cases(other)) 858 try assumption (*20s*) 859 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 860 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 861 whd in match execute_1_preinstruction; normalize nodelta 862 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 665 863 (* XXX: work on the right hand side *) 666 864 lapply (subaddressing_modein ???) … … 669 867 try (>p1 normalize nodelta) 670 868 (* XXX: switch to the left hand side *) 671 instr_refl>EQP P normalize nodelta869 >EQP P normalize nodelta 672 870 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 673 871 whd in ⊢ (??%?); … … 688 886 whd in ⊢ (??%%); 689 887 (* XXX: finally, prove the equality using sigma commutation *) 690 cases daemon 691 (* XXX: work on both sides *) 692 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 888 try @split_eq_status try % whd in ⊢ (??%%); 889 [1: 890 >low_internal_ram_set_8051_sfr >low_internal_ram_set_clock 891 >low_internal_ram_set_program_counter @eq_f2 try % 892 whd in maps_assm:(??%?); destruct % 893 2: 894 >high_internal_ram_set_8051_sfr >high_internal_ram_set_clock 895 >high_internal_ram_set_program_counter @eq_f2 try % 896 whd in maps_assm:(??%?); destruct % 897 3: 898 >clock_set_program_counter >clock_set_program_counter <instr_refl % 899 4,6: 900 >set_clock_set_program_counter >get_arg_8_set_program_counter 901 >clock_set_program_counter >set_clock_mk_Status_commutation 902 >set_clock_mk_Status_commutation >clock_set_program_counter <instr_refl 903 8: 904 cases daemon 905 ] 906 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 693 907 (* XXX: work on the right hand side *) 694 908 >p normalize nodelta … … 702 916 @(pair_replace ?????????? p) 703 917 [1,3,5,7,9,11,13,15,17: 918 >set_clock_set_program_counter >set_clock_mk_Status_commutation 919 >set_program_counter_mk_Status_commutation >clock_set_program_counter 704 920 cases daemon 705 921 14,16,18: 706 922 normalize nodelta 707 923 @(pair_replace ?????????? p1) 708 [1,3,5: 709 cases daemon 710 ] 924 [1,3,5: 925 >set_clock_mk_Status_commutation 926 cases daemon 927 ] 711 928 ] 712 929 (* XXX: switch to the right hand side *) … … 714 931 whd in ⊢ (??%%); 715 932 (* XXX: finally, prove the equality using sigma commutation *) 933 try @split_eq_status try % 934 >set_clock_mk_Status_commutation 716 935 cases daemon (* 717 936 @split_eq_status try % … … 720 939 (* CSC: TO BE COMPLETED *) 721 940 ] *) 722 10,42,43,44,45,49,52,56: (* MUL *)941 10,42,43,44,45,49,52,56: (* MUL *) 723 942 (* XXX: work on the right hand side *) 724 943 (* XXX: switch to the left hand side *) … … 733 952 (* XXX: finally, prove the equality using sigma commutation *) 734 953 cases daemon 735 11,12: (* DIV *)954 11,12: (* DIV *) 736 955 (* XXX: work on the right hand side *) 737 956 normalize nodelta in p; … … 755 974 cases daemon 756 975 ] 757 13,14,15: (* DA *)976 13,14,15: (* DA *) 758 977 (* XXX: work on the right hand side *) 759 978 >p normalize nodelta … … 771 990 @(pair_replace ?????????? p) 772 991 [1,3,5: 992 /demod/ 773 993 cases daemon 774 994 2,4,6: … … 793 1013 cases daemon 794 1014 ] 795 33,34,35,48: (* ANL, ORL, XRL, MOVX *)1015 33,34,35,48: (* ANL, ORL, XRL, MOVX *) 796 1016 (* XXX: work on the right hand side *) 797 1017 cases addr #addr' normalize nodelta … … 811 1031 (* XXX: finally, prove the equality using sigma commutation *) 812 1032 cases daemon 813 47: (* MOV *)1033 47: (* MOV *) 814 1034 (* XXX: work on the right hand side *) 815 1035 cases addr addr #addr normalize nodelta … … 838 1058 (* XXX: finally, prove the equality using sigma commutation *) 839 1059 cases daemon 840 17,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *)1060 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) 841 1061 (* XXX: work on the right hand side *) 842 1062 >p normalize nodelta … … 851 1071 @pair_elim #upper #lower #split_refl 852 1072 cases (eq_bv ???) normalize nodelta 853 [1,3,5,7,9,11,13,15 :1073 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 854 1074 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 855 1075 whd in ⊢ (??%?); … … 857 1077 (* XXX: work on the left hand side *) 858 1078 @(if_then_else_replace ???????? p) normalize nodelta 859 [1,3,5,7,9,11,13,15 :1079 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 860 1080 cases daemon 861 1081 ] … … 866 1086 @split_eq_status try % 867 1087 cases daemon 868 2,4,6,8,10,12,14,16 :1088 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 869 1089 >EQppc 870 1090 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl … … 876 1096 #status_after_1 #EQstatus_after_1 877 1097 <(?: ? = status_after_1) 878 [3,6,9,12,15,18,21,24 :1098 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 879 1099 >EQstatus_after_1 in ⊢ (???%); 880 1100 whd in ⊢ (???%); … … 887 1107 7: <fetch_refl in ⊢ (???%); 888 1108 8: <fetch_refl in ⊢ (???%); 1109 9: <fetch_refl in ⊢ (???%); 1110 10: <fetch_refl in ⊢ (???%); 1111 11: <fetch_refl in ⊢ (???%); 1112 12: <fetch_refl in ⊢ (???%); 1113 13: <fetch_refl in ⊢ (???%); 1114 14: <fetch_refl in ⊢ (???%); 889 1115 ] 890 1116 whd in ⊢ (???%); 891 1117 @(if_then_else_replace ???????? p) 892 [1,3,5,7,9,11,13,15 :1118 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 893 1119 cases daemon 894 2,4,6,8,10,12,14,16 :1120 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 895 1121 normalize nodelta 896 1122 whd in match (addr_of_relative ????); 897 1123 >set_clock_mk_Status_commutation 898 [ 6:1124 [9,10: 899 1125 (* XXX: demodulation not working in this case *) 900 1126 >program_counter_set_arg_1 in ⊢ (???%); … … 906 1132 change with (add ???) in match (\snd (half_add ???)); 907 1133 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 908 [2,4,6,8,10,12,14,16 :1134 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 909 1135 >bitvector_of_nat_sign_extension_equivalence 910 [1,3,5,7,9,11,13,15 :1136 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 911 1137 >EQintermediate_pc' % 912 1138 *: … … 916 1142 % 917 1143 ] 918 1,4,7,10,13,16,19,22 :1144 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 919 1145 skip 920 1146 ] … … 923 1149 #status_after_1 #EQstatus_after_1 924 1150 <(?: ? = status_after_1) 925 [3,6,9,12,15,18,21,24 :1151 [3,6,9,12,15,18,21,24,27,30,33,36,39,42: 926 1152 >EQstatus_after_1 in ⊢ (???%); 927 1153 whd in ⊢ (???%); … … 930 1156 2: <fetch_refl' in ⊢ (???%); 931 1157 3: <fetch_refl'' in ⊢ (???%); 932 4: <fetch_refl' 'in ⊢ (???%);1158 4: <fetch_refl' in ⊢ (???%); 933 1159 5: <fetch_refl'' in ⊢ (???%); 934 6: <fetch_refl' 'in ⊢ (???%);1160 6: <fetch_refl' in ⊢ (???%); 935 1161 7: <fetch_refl'' in ⊢ (???%); 936 8: <fetch_refl'' in ⊢ (???%); 1162 8: <fetch_refl' in ⊢ (???%); 1163 9: <fetch_refl'' in ⊢ (???%); 1164 10: <fetch_refl' in ⊢ (???%); 1165 11: <fetch_refl'' in ⊢ (???%); 1166 12: <fetch_refl' in ⊢ (???%); 1167 13: <fetch_refl'' in ⊢ (???%); 1168 14: <fetch_refl' in ⊢ (???%); 937 1169 ] 938 1170 whd in ⊢ (???%); 939 [ 6:1171 [9,10: 940 1172 *: 941 1173 /demod/ 942 1174 ] % 943 1,4,7,10,13,16,19,22 :1175 1,4,7,10,13,16,19,22,25,28,31,34,37,40: 944 1176 skip 945 1177 ] … … 950 1182 (* XXX: finally, prove the equality using sigma commutation *) 951 1183 @split_eq_status try % 952 [3,11,1 5,19,24,32,36:1184 [3,11,19,27,36,53,61: 953 1185 >program_counter_set_program_counter >set_clock_mk_Status_commutation 954 1186 [5: >program_counter_set_program_counter ] … … 956 1188 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta 957 1189 >EQcm % 958 7 :1190 7,15,23,31,45,57,65: 959 1191 >set_clock_mk_Status_commutation >program_counter_set_program_counter 960 1192 whd in ⊢ (??%?); normalize nodelta 961 1193 >EQppc in fetch_many_assm; #fetch_many_assm 1194 [5: 1195 >program_counter_set_arg_1 >program_counter_set_program_counter 1196 ] 962 1197 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc'' 963 1198 <bitvector_of_nat_sign_extension_equivalence 964 [1 :1199 [1,3,5,7,9,11,13: 965 1200 whd in ⊢ (???%); cases (half_add ???) normalize // 966 2 :1201 2,4,6,8,10,12,14: 967 1202 @assembly1_lt_128 1203 @le_S_S @le_O_n 968 1204 ] 969 1205 *: … … 971 1207 ] 972 1208 ] 1209 30: (* CJNE *) 1210 cases addr1 * #addr1_l #addr1_r normalize nodelta 1211 (* XXX: work on the right hand side *) 1212 (* XXX: switch to the left hand side *) 1213 instr_refl >EQP P normalize nodelta 1214 #sigma_increment_commutation #maps_assm #fetch_many_assm 1215 1216 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1217 whd in match (expand_relative_jump ????); 1218 <EQppc in fetch_many_assm; 1219 @pair_elim #result #flags #sub16_refl 1220 @pair_elim #upper #lower #split_refl 1221 cases (eq_bv ???) normalize nodelta 1222 [1,3: 1223 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1224 whd in ⊢ (??%?); 1225 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1226 (* XXX: work on the left hand side *) 1227 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta 1228 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl 1229 @(if_then_else_replace ???????? eq_bv_refl) 1230 [1,3,5,7: 1231 cases daemon 1232 *: 1233 (* XXX: switch to the right hand side *) 1234 normalize nodelta >EQs s >EQticks ticks 1235 whd in ⊢ (??%%); 1236 (* XXX: finally, prove the equality using sigma commutation *) 1237 @split_eq_status try % 1238 cases daemon 1239 ] 1240 2,4: 1241 >EQppc 1242 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1243 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 1244 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 1245 #fetch_many_assm whd in fetch_many_assm; %{2} 1246 change with (execute_1 ?? = ?) 1247 @(pose … (execute_1 ? (status_of_pseudo_status …))) 1248 #status_after_1 #EQstatus_after_1 1249 <(?: ? = status_after_1) 1250 [3,6: 1251 >EQstatus_after_1 in ⊢ (???%); 1252 whd in ⊢ (???%); 1253 [1: 1254 <fetch_refl in ⊢ (???%); 1255 2: 1256 <fetch_refl in ⊢ (???%); 1257 ] 1258 whd in ⊢ (???%); 1259 cases (¬ eq_bv ???) normalize nodelta 1260 whd in match (addr_of_relative ????); 1261 >set_clock_mk_Status_commutation 1262 whd in ⊢ (???%); 1263 [9,10: 1264 (* XXX: demodulation not working in this case *) 1265 >program_counter_set_arg_1 in ⊢ (???%); 1266 >program_counter_set_program_counter in ⊢ (???%); 1267 *: 1268 /demod/ 1269 ] 1270 whd in ⊢ (???%); 1271 change with (add ???) in match (\snd (half_add ???)); 1272 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 1273 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1274 >bitvector_of_nat_sign_extension_equivalence 1275 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1276 >EQintermediate_pc' % 1277 *: 1278 repeat @le_S_S @le_O_n 1279 ] 1280 ] 1281 % 1282 ] 1283 1284 ] 973 1285 ] 1286 cases daemon (* XXX: CJNE and DJNZ cases *) 974 1287 qed. 975 1288 (* … … 1080 1393 whd in fetch_many_assm; 1081 1394 >EQassembled in fetch_many_assm; 1082 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *1395 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * 1083 1396 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 1084 1397 #fetch_many_assm whd in fetch_many_assm;
Note: See TracChangeset
for help on using the changeset viewer.