Changeset 2143 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 2, 2012, 11:37:34 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2140 r2143 175 175 ∀s: PreStatus M cm. 176 176 ∀flag: bool. 177 ∀addr .177 ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]]. 178 178 ∀pc: Word. 179 179 get_arg_8 M cm (set_program_counter M cm s pc) flag addr = 180 180 get_arg_8 M cm s flag addr. 181 [2,3: 182 cases addr #subaddressing_mode 183 cases subaddressing_mode 184 try (#addr1 whd in ⊢ (% → %);) 185 whd in ⊢ (% → %); // 186 ] 181 187 #M #cm #s #flag #addr #pc 182 188 whd in match get_arg_8; normalize nodelta 183 189 cases addr * 184 try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I)185 190 try (#addr1 #absurd normalize in absurd; cases absurd @I) 186 191 try (#absurd normalize in absurd; cases absurd @I) 187 192 try (#addr1 #addr2) try #addr1 188 normalize nodelta try % 189 cases daemon (* XXX: rewrite not working but provable *) 193 normalize nodelta % 190 194 qed. 191 195 … … 319 323 #M #cm #s #pc #pc' % 320 324 qed. 325 326 (* XXX: move elsewhere *) 327 lemma bitvector_8_cases: 328 ∀w: BitVector 8. 329 ∃b0,b1,b2,b3,b4,b5,b6,b7: bool. 330 w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]]. 331 #w repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} w lapply w0 w0 #w) 332 >(BitVector_O … w) % 333 qed. 334 335 (* XXX: not true 336 lemma p3_latch_set_arg_8: 337 ∀M: Type[0]. 338 ∀cm: M. 339 ∀s: PreStatus M cm. 340 ∀args. 341 ∀v: Byte. 342 p3_latch M cm (set_arg_8 M cm s args v) = 343 p3_latch M cm s. 344 #M #cm #s #args #v 345 @(subaddressing_mode_elim … args) 346 try #w try % 347 whd in match set_arg_8; normalize nodelta 348 whd in match set_arg_8'; normalize nodelta 349 inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta 350 inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta 351 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try % 352 whd in match set_bit_addressable_sfr; normalize nodelta 353 @(bitvector_8_elim_prop … w) 354 *) 355 356 lemma status_of_pseudo_status_does_not_change_8051_sfrs: 357 ∀M: internal_pseudo_address_map. 358 ∀cm: pseudo_assembly_program. 359 ∀s: PreStatus pseudo_assembly_program cm. 360 ∀sigma: Word → Word. 361 ∀policy: Word → bool. 362 \snd M = (None …) → 363 special_function_registers_8051 pseudo_assembly_program cm s = 364 special_function_registers_8051 (BitVectorTrie Byte 16) 365 (code_memory_of_pseudo_assembly_program cm sigma policy) 366 (status_of_pseudo_status M cm s sigma policy). 367 #M #cm #s #sigma #policy #None_proof cases s 368 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 369 whd in match status_of_pseudo_status; normalize nodelta 370 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 371 >None_proof % 372 qed. 373 374 lemma special_function_registers_8051_set_program_counter: 375 ∀cm: pseudo_assembly_program. 376 ∀ps: PreStatus pseudo_assembly_program cm. 377 ∀v: Word. 378 special_function_registers_8051 pseudo_assembly_program cm 379 (set_program_counter pseudo_assembly_program cm ps v) = 380 special_function_registers_8051 pseudo_assembly_program cm ps. 381 #cm #ps #v % 382 qed. 383 384 (* 385 lemma get_arg_8_status_of_pseudo_status: 386 ∀M: internal_pseudo_address_map. 387 ∀cm: pseudo_assembly_program. 388 ∀ps. 389 ∀sigma: Word → Word. 390 ∀policy: Word → bool. 391 ∀b: bool. 392 ∀addr1: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect_dptr]]. 393 get_arg_8 (BitVectorTrie Byte 16) 394 (code_memory_of_pseudo_assembly_program cm sigma policy) 395 (status_of_pseudo_status M cm ps sigma policy) b addr1 = 396 get_arg_8 pseudo_assembly_program cm ps b addr1. 397 [2,3: 398 @(subaddressing_mode_elim … addr1) try #w @I 399 ] 400 #M #cm #ps #sigma #policy #b #addr1 401 @(subaddressing_mode_elim … addr1) 402 try #w 403 [1: 404 whd in ⊢ (??%%); 405 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 406 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 407 cases (get_index_v bool ????) normalize nodelta try % 408 cases daemon (* XXX: require axioms from Assembly.ma *) 409 2: 410 whd in ⊢ (??%%); 411 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 412 lapply (refl_to_jmrefl ??? nu_nl_refl) nu_nl_refl #nu_nl_refl 413 @(pair_replace ?????????? nu_nl_refl) [1: cases daemon (* XXX: !! *) ] 414 @pair_elim #bit_one_v #three_bits #bit_one_v_three_bits_refl normalize nodelta 415 cases (get_index_v bool ????) normalize nodelta 416 cases daemon (* XXX: same as above *) 417 3: 418 whd in ⊢ (??%%); @(bitvector_3_elim_prop … w) 419 whd in match bit_address_of_register; normalize nodelta 420 @pair_elim #un #ln #un_ln_refl 421 cases (¬get_index_v bool ???? ∧ ¬get_index_v bool ????) normalize nodelta 422 [1,3,5,7,9,11,13,15: 423 cases daemon (* XXX: same as above *) 424 *: 425 cases (¬get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta 426 [1,3,5,7,9,11,13,15: 427 cases daemon (* XXX: same as above *) 428 *: 429 cases (get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta 430 cases daemon (* XXX: same as above *) 431 ] 432 ] 433 4,5: 434 whd in ⊢ (??%%); <status_of_pseudo_status_does_not_change_8051_sfrs % 435 6,7,8: 436 % 437 ] 438 qed. 439 *) 321 440 322 441 (* … … 823 942 >p normalize nodelta >p1 normalize nodelta 824 943 (* XXX: switch to the left hand side *) 825 instr_refl>EQP P normalize nodelta944 >EQP P normalize nodelta 826 945 #sigma_increment_commutation #maps_assm #fetch_many_assm 827 946 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; … … 843 962 @(pair_replace ?????????? p) normalize nodelta 844 963 [1,3: 845 >get_arg_8_set_program_counter 846 cases daemon 964 >(get_arg_8_set_program_counter … true addr1) in ⊢ (??%?); 965 [2,4: (* /2 by _/ *) cases daemon ] @eq_f3 [2,3,5,6: % ] 966 whd in ⊢ (??%?); @(subaddressing_mode_elim … addr1) 967 #arg normalize nodelta whd in ⊢ (???%); 968 [1,3: 969 whd in match get_register; normalize nodelta 970 @(bitvector_3_elim_prop … arg) 971 whd in match bit_address_of_register; normalize nodelta 972 @pair_elim #un #ln #un_ln_refl 973 lapply (refl_to_jmrefl ??? un_ln_refl) un_ln_refl #un_ln_refl 974 @(pair_replace ?????????? un_ln_refl) 975 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31: 976 whd in match get_8051_sfr; normalize nodelta 977 whd in match sfr_8051_index; normalize nodelta 978 @eq_f <status_of_pseudo_status_does_not_change_8051_sfrs 979 >EQs 980 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31: 981 /demod nohyps/ % 982 *: 983 cases daemon 984 ] 985 *: 986 >low_internal_ram_of_pseudo_internal_ram_miss 987 cases daemon 988 (* XXX: require axioms about low_internal_ram_of_pseudo_low_internal_ram *) 989 ] 990 2,4: 991 @pair_elim #nu #nl #nu_nl_refl 992 lapply (refl_to_jmrefl ??? nu_nl_refl) nu_nl_refl #nu_nl_refl 993 @pair_elim #ignore #three_bits #ignore_three_bits_refl 994 lapply (refl_to_jmrefl ??? ignore_three_bits_refl) ignore_three_bits_refl #ignore_three_bits_refl 995 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta 996 [1,3: 997 @(pair_replace ?????????? ignore_three_bits_refl) try % 998 >get_index_v_refl normalize nodelta >EQs % 999 2,4: 1000 @(pair_replace ?????????? ignore_three_bits_refl) try % 1001 >get_index_v_refl normalize nodelta >EQs 1002 cases daemon 1003 (* XXX: require axioms about low_internal_ram as above *) 1004 ] 1005 ] 847 1006 ] 848 1007 (* XXX: switch to the right hand side *) … … 852 1011 (* XXX: finally, prove the equality using sigma commutation *) 853 1012 @split_eq_status try % 854 cases daemon 1013 [1,2,3,19,20,21,28,29,30: 1014 cases daemon (* XXX: axioms as above *) 1015 4,13,22,31: 1016 5,14,23,32: 1017 6,15,24,33: 1018 7,16,25,34: 1019 8,17,26,35: 1020 whd in ⊢ (??%%); 1021 1022 9,18,27,36: 1023 whd in ⊢ (??%%); 1024 whd in match (ticks_of_instruction ?); <instr_refl 1025 cases daemon (* XXX: daemon in ticks_of0 stopping progression *) 1026 ] 855 1027 2,4: 856 1028 >(? : eq_v bool 9 eq_b upper (zero 9) = false)
Note: See TracChangeset
for help on using the changeset viewer.