Changeset 2143
 Timestamp:
 Jul 2, 2012, 11:37:34 AM (5 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2139 r2143 403 403 qed. 404 404 405 (* XXX: move back into ASM.ma *) 406 lemma subvector_with_to_subvector_with_tl: 407 ∀n: nat. 408 ∀m: nat. 409 ∀v. 410 ∀fixed_v. 411 ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v). 412 ∀n': nat. 413 ∀hd: addressing_mode_tag. 414 ∀tl: Vector addressing_mode_tag n'. 415 ∀m_refl: S n'=n. 416 ∀v_refl: v≃hd:::tl. 417 subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v. 418 #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl 419 generalize in match proof; destruct 420 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 421 cases (mem … eq_a ? fixed_v hd) normalize nodelta 422 [1: 423 whd in match (subvector_with … eq_a tl fixed_v); 424 #assm assumption 425 2: 426 normalize in ⊢ (% → ?); 427 #absurd cases absurd 428 ] 429 qed. 405 430 406 431 let rec subaddressing_mode_elim_type … … 437 462 ] (refl … n) (refl_jmeq … v). 438 463 [20: 439 generalize in match proof; destruct 440 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 441 cases (mem … eq_a ? fixed_v hd) normalize nodelta 442 [1: 443 whd in match (subvector_with … eq_a tl fixed_v); 444 #assm assumption 445 2: 446 normalize in ⊢ (% → ?); 447 #absurd cases absurd 448 ] 464 @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl) 449 465 ] 450 466 @(is_in_subvector_is_in_supervector … proof) … … 460 476 (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → 461 477 subaddressing_mode_elim_type n v addr Q m w H. 462 #n #v #addr #Q #m #w elim w 463 [ /2/ 464  #n' #hd #tl #IH cases hd #H 465 #INV whd #PO @IH #xaddr cases xaddr * 466 try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV 467 @ALREADYSEEN ] 478 #n #v #addr #Q #m #w elim w 479 [1: 480 /2/ 481 2: 482 #n' #hd #tl #IH cases hd #H 483 #INV whd #PO @IH #xaddr cases xaddr * 484 try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV 485 @ALREADYSEEN 486 ] 468 487 qed. 469 488 … … 474 493 ∀Q: v → Prop. 475 494 subaddressing_mode_elim_type n v addr Q (S n) v ?. 476 [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // 477  @subvector_with_refl @eq_a_reflexive 478 ] 495 [1: 496 #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // 497 2: 498 @subvector_with_refl @eq_a_reflexive 499 ] 479 500 qed. 480 501 
src/ASM/AssemblyProof.ma
r2142 r2143 340 340 qed. 341 341 342 lemma m_lt_1_to_m_refl_0: 343 ∀m: nat. 344 m < 1 → m = 0. 345 #m cases m try (#irrelevant %) 346 #m' whd in ⊢ (% → ?); #relevant 347 lapply (le_S_S_to_le … relevant) 348 change with (? < ? → ?) relevant #relevant 349 cases (lt_to_not_zero … relevant) 350 qed. 351 342 352 (*CSC: move elsewhere*) 343 353 axiom lt_to_lt_nat_of_bitvector_add: 344 ∀n,v,m1,m2.345 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →346 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <347 nat_of_bitvector n (add n v (bitvector_of_nat n m2)).354 ∀n,v,m1,m2. 355 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 356 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) < 357 nat_of_bitvector n (add n v (bitvector_of_nat n m2)). 348 358 349 359 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) … … 645 655 (external_ram … ps) 646 656 pc 647 (s pecial_function_registers_8051 … ps)657 (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma) 648 658 (special_function_registers_8052 … ps) 649 659 (p1_latch … ps) … … 764 774 *) 765 775 776 (* XXX: check values returned for conditional jumps below! *) 766 777 definition ticks_of0: 767 778 ∀p:pseudo_assembly_program. … … 775 786 [ Instruction instr ⇒ 776 787 match instr with 777 [ JC lbl ⇒ ? (* 778 match pol lookup_labels ppc with 779 [ short_jump ⇒ 〈2, 2〉 780  absolute_jump ⇒ ? 781  long_jump ⇒ 〈4, 4〉 782 ] *) 783  JNC lbl ⇒ ? (* 784 match pol lookup_labels ppc with 785 [ short_jump ⇒ 〈2, 2〉 786  absolute_jump ⇒ ? 787  long_jump ⇒ 〈4, 4〉 788 ] *) 789  JB bit lbl ⇒ ? (* 790 match pol lookup_labels ppc with 791 [ short_jump ⇒ 〈2, 2〉 792  absolute_jump ⇒ ? 793  long_jump ⇒ 〈4, 4〉 794 ] *) 795  JNB bit lbl ⇒ ? (* 796 match pol lookup_labels ppc with 797 [ short_jump ⇒ 〈2, 2〉 798  absolute_jump ⇒ ? 799  long_jump ⇒ 〈4, 4〉 800 ] *) 801  JBC bit lbl ⇒ ? (* 802 match pol lookup_labels ppc with 803 [ short_jump ⇒ 〈2, 2〉 804  absolute_jump ⇒ ? 805  long_jump ⇒ 〈4, 4〉 806 ] *) 807  JZ lbl ⇒ ? (* 808 match pol lookup_labels ppc with 809 [ short_jump ⇒ 〈2, 2〉 810  absolute_jump ⇒ ? 811  long_jump ⇒ 〈4, 4〉 812 ] *) 813  JNZ lbl ⇒ ? (* 814 match pol lookup_labels ppc with 815 [ short_jump ⇒ 〈2, 2〉 816  absolute_jump ⇒ ? 817  long_jump ⇒ 〈4, 4〉 818 ] *) 819  CJNE arg lbl ⇒ ? (* 820 match pol lookup_labels ppc with 821 [ short_jump ⇒ 〈2, 2〉 822  absolute_jump ⇒ ? 823  long_jump ⇒ 〈4, 4〉 824 ] *) 825  DJNZ arg lbl ⇒ ? (* 826 match pol lookup_labels ppc with 827 [ short_jump ⇒ 〈2, 2〉 828  absolute_jump ⇒ ? 829  long_jump ⇒ 〈4, 4〉 830 ] *) 788 [ JC lbl ⇒ 789 if policy ppc then 790 〈4, 4〉 791 else 792 〈2, 2〉 793  JNC lbl ⇒ 794 if policy ppc then 795 〈4, 4〉 796 else 797 〈2, 2〉 798  JB bit lbl ⇒ 799 if policy ppc then 800 〈4, 4〉 801 else 802 〈2, 2〉 803  JNB bit lbl ⇒ 804 if policy ppc then 805 〈4, 4〉 806 else 807 〈2, 2〉 808  JBC bit lbl ⇒ 809 if policy ppc then 810 〈4, 4〉 811 else 812 〈2, 2〉 813  JZ lbl ⇒ 814 if policy ppc then 815 〈4, 4〉 816 else 817 〈2, 2〉 818  JNZ lbl ⇒ 819 if policy ppc then 820 〈4, 4〉 821 else 822 〈2, 2〉 823  CJNE arg lbl ⇒ 824 if policy ppc then 825 〈4, 4〉 826 else 827 〈2, 2〉 828  DJNZ arg lbl ⇒ 829 if policy ppc then 830 〈4, 4〉 831 else 832 〈2, 2〉 831 833  ADD arg1 arg2 ⇒ 832 834 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in … … 916 918  Comment comment ⇒ 〈0, 0〉 917 919  Cost cost ⇒ 〈0, 0〉 918  Jmp jmp ⇒ 〈2, 2〉 919  Call call ⇒ 〈2, 2〉 920  Jmp jmp ⇒ 921 if policy ppc then 922 〈4, 4〉 923 else 924 〈2, 2〉 925  Call call ⇒ 926 if policy ppc then 927 〈4, 4〉 928 else 929 〈2, 2〉 920 930  Mov dptr tgt ⇒ 〈2, 2〉 921 931 ]. 922 cases daemon923 qed.924 932 925 933 definition ticks_of: 
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.