Changeset 1975
 Timestamp:
 May 21, 2012, 5:48:43 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1972 r1975 1380 1380 assm #c #assm cases assm 1381 1381 assm #r #assm cases assm destruct 1382 cases l cases c cases r //1382 cases l cases c cases r assumption 1383 1383 qed. 1384 1384 … … 1451 1451 qed. 1452 1452 1453 axiomeq_instruction_to_eq:1453 lemma eq_instruction_to_eq: 1454 1454 ∀i1, i2: instruction. 1455 1455 eq_instruction i1 i2 = true → i1 ≃ i2. 1456 #i1 #i2 1457 cases i1 cases i2 cases daemon (* 1458 [1,10,19,28,37,46: 1459 #arg1 #arg2 1460 whd in match (eq_instruction ??); 1461 cases arg1 #subaddressing_mode 1462 cases subaddressing_mode 1463 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) 1464 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) 1465 try (normalize in ⊢ (% → ?); #absurd cases absurd @I) 1466 #word11 #irrelevant 1467 cases arg2 #subaddressing_mode 1468 cases subaddressing_mode 1469 try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) 1470 try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) 1471 try (normalize in ⊢ (% → ?); #absurd cases absurd @I) 1472 #word11' #irrelevant normalize nodelta 1473 #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *) 1474 qed. 1456 1475 1457 1476 lemma fetch_assembly_pseudo': 
src/ASM/AssemblyProofSplit.ma
r1971 r1975 66 66 qed. 67 67 68 lemma get_8051_sfr_set_clock: 69 ∀M: Type[0]. 70 ∀cm: M. 71 ∀s: PreStatus M cm. 72 ∀sfr: SFR8051. 73 ∀t: Time. 74 get_8051_sfr M cm (set_clock M cm s t) sfr = 75 get_8051_sfr M cm s sfr. 76 #M #cm #s #sfr #t % 77 qed. 68 78 69 79 lemma special_function_registers_8051_set_arg_16: … … 102 112 #A #B #C #P * #a #b * // 103 113 qed. 104 *)105 114 106 115 lemma tech_pi1_let_as_commute: … … 113 122 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/ 114 123 qed. 124 *) 115 125 116 126 include alias "arithmetics/nat.ma". … … 119 129 120 130 lemma pair_replace: 121 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c =c'→ c ≃ 〈a,b〉 →131 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → 122 132 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). 123 133 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // 134 qed. 135 136 lemma pair_as_replace: 137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c' → T. ∀EQc: c'= c. 138 c ≃ 〈a,b〉 → 139 P (let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H). 140 [2: 141 >EQc assumption 142 1: 143 #A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct // 144 ] 145 qed. 146 147 lemma if_then_else_replace: 148 ∀T: Type[0]. 149 ∀P: T → Prop. 150 ∀t1, t2: T. 151 ∀c, c', c'': bool. 152 c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2). 153 #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm 154 assumption 124 155 qed. 125 156 … … 159 190 ∀P. 160 191 ∀EQP: 161 P = (λs. ∃n:ℕ162 .execute n192 P = (λs. 193 execute (expand_relative_jump lookup_labels sigma ppc instr) 163 194 (code_memory_of_pseudo_assembly_program cm sigma 164 195 policy) … … 271 302 ] 272 303  INC addr ⇒ λinstr_refl. 273 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with274 [ ACC_A ⇒ λacc_a: True. 304 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with 305 [ ACC_A ⇒ λacc_a: True. λEQaddr. 275 306 let s' ≝ add_ticks1 s in 276 307 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 277 308 set_arg_8 … s' ACC_A result 278  REGISTER r ⇒ λregister: True. 309  REGISTER r ⇒ λregister: True. λEQaddr. 279 310 let s' ≝ add_ticks1 s in 280 311 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 281 312 set_arg_8 … s' (REGISTER r) result 282  DIRECT d ⇒ λdirect: True. 313  DIRECT d ⇒ λdirect: True. λEQaddr. 283 314 let s' ≝ add_ticks1 s in 284 315 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 285 316 set_arg_8 … s' (DIRECT d) result 286  INDIRECT i ⇒ λindirect: True. 317  INDIRECT i ⇒ λindirect: True. λEQaddr. 287 318 let s' ≝ add_ticks1 s in 288 319 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 289 320 set_arg_8 … s' (INDIRECT i) result 290  DPTR ⇒ λdptr: True. 321  DPTR ⇒ λdptr: True. λEQaddr. 291 322 let s' ≝ add_ticks1 s in 292 323 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in … … 295 326 set_8051_sfr … s' SFR_DPH bu 296 327  _ ⇒ λother: False. ⊥ 297 ] (subaddressing_modein … addr) 328 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 298 329  NOP ⇒ λinstr_refl. 299 330 let s ≝ add_ticks2 s in … … 343 374 s 344 375  CLR addr ⇒ λinstr_refl. 345 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with346 [ ACC_A ⇒ λacc_a: True. 376 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with 377 [ ACC_A ⇒ λacc_a: True. λEQaddr. 347 378 let s ≝ add_ticks1 s in 348 379 set_arg_8 … s ACC_A (zero 8) 349  CARRY ⇒ λcarry: True. 380  CARRY ⇒ λcarry: True. λEQaddr. 350 381 let s ≝ add_ticks1 s in 351 382 set_arg_1 … s CARRY false 352  BIT_ADDR b ⇒ λbit_addr: True. 383  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 353 384 let s ≝ add_ticks1 s in 354 385 set_arg_1 … s (BIT_ADDR b) false 355 386  _ ⇒ λother: False. ⊥ 356 ] (subaddressing_modein … addr) 387 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 357 388  CPL addr ⇒ λinstr_refl. 358 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with359 [ ACC_A ⇒ λacc_a: True. 389 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with 390 [ ACC_A ⇒ λacc_a: True. λEQaddr. 360 391 let s ≝ add_ticks1 s in 361 392 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 362 393 let new_acc ≝ negation_bv ? old_acc in 363 394 set_8051_sfr … s SFR_ACC_A new_acc 364  CARRY ⇒ λcarry: True. 395  CARRY ⇒ λcarry: True. λEQaddr. 365 396 let s ≝ add_ticks1 s in 366 397 let old_cy_flag ≝ get_arg_1 … s CARRY true in 367 398 let new_cy_flag ≝ ¬old_cy_flag in 368 399 set_arg_1 … s CARRY new_cy_flag 369  BIT_ADDR b ⇒ λbit_addr: True. 400  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 370 401 let s ≝ add_ticks1 s in 371 402 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in … … 373 404 set_arg_1 … s (BIT_ADDR b) new_bit 374 405  _ ⇒ λother: False. ? 375 ] (subaddressing_modein … addr) 406 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 376 407  SETB b ⇒ λinstr_refl. 377 408 let s ≝ add_ticks1 s in … … 410 441 set_8051_sfr … s SFR_ACC_A new_acc 411 442  PUSH addr ⇒ λinstr_refl. 412 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with413 [ DIRECT d ⇒ λdirect: True. 443 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with 444 [ DIRECT d ⇒ λdirect: True. λEQaddr. 414 445 let s ≝ add_ticks1 s in 415 446 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in … … 417 448 write_at_stack_pointer … s d 418 449  _ ⇒ λother: False. ⊥ 419 ] (subaddressing_modein … addr) 450 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 420 451  POP addr ⇒ λinstr_refl. 421 452 let s ≝ add_ticks1 s in … … 596 627 ) (*66s*) 597 628 whd in match execute_1_preinstruction; normalize nodelta 598 [1: (* ADD *) 599 >p normalize nodelta 600 >EQP %{1} 601 whd in ⊢ (??%?); 602 (* work on fetch_many *) 629 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 630 lapply (subaddressing_modein ???) 631 <EQaddr normalize nodelta #irrelevant 632 try (>p normalize nodelta) 633 try (>p1 normalize nodelta) 634 (* XXX: start work on the left hand side *) 635 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 636 (* XXX: work on fetch_many *) 603 637 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 604 638 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 605 639 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 606 <EQppc 607 cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 640 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 608 641 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 609 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc642 >(eq_bv_eq … fetch_many_assm) newpc 610 643 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 644 (* XXX: work on sigma commutation *) 645 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 646 (* XXX: work on ticks (of all kinds) *) 647 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 648 (* XXX: work on both sides *) 649 [1,2,3,4,5: 650 generalize in ⊢ (??(???(?%))?); 651 6,7,8,9,10,11: 652 generalize in ⊢ (??(???(?%))?); 653 12: 654 generalize in ⊢ (??(???(?%))?); 655 ] 656 <EQaddr normalize nodelta #irrelevant 657 [1: 658 @(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p) 659 660 (* XXX: removes status 's' *) 661 normalize nodelta >EQs s ticks 662 whd in ⊢ (??%%); 663 (* XXX: simplify the left hand side *) 664 665 (* XXX: work on both sides *) 666 1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI *) 667 (* XXX: simplify the right hand side *) 668 >p normalize nodelta 669 try (>p1 normalize nodelta) 670 (* XXX: start work on the left hand side *) 671 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 672 (* XXX: work on fetch_many *) 673 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 674 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 675 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 676 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 677 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 678 >(eq_bv_eq … fetch_many_assm) newpc 679 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 680 (* XXX: work on sigma commutation *) 681 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 682 (* XXX: work on ticks (of all kinds) *) 683 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 684 (* XXX: simplify the left hand side *) 611 685 @(pair_replace ?????????? p) 612 [2: normalize nodelta >EQs s >EQticks' ticks' 613 <instr_refl in EQticks; #EQticks >EQticks ticks 614 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 615 whd in ⊢ (??%%); 616 @split_eq_status 617 try % 618 [3: whd in ⊢ (??%%); >EQnewpc >sigma_increment_commutation % 619 2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation 686 [1,3,5,7,9,11,13,15: 687 cases daemon 688 12,14,16: 689 normalize nodelta 690 @(pair_replace ?????????? p1) 691 [1,3,5: 692 cases daemon 693 ] 694 ] 695 (* XXX: removes status 's' *) 696 normalize nodelta >EQs s ticks 697 whd in ⊢ (??%%); 698 (* XXX: work on both sides *) 699 cases daemon (* 700 @split_eq_status try % 701 [*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation 620 702 whd in match (set_flags ??????); 621 703 (* CSC: TO BE COMPLETED *) 622 ] 623  (*>get_arg_8_ok_set_clock*) (*CSC: to be done *) 624 ] 625 626 ] cases daemon 704 ] *) 705 10,42,43,44,45,49,52,56: (* MUL *) 706 (* XXX: simplify the right hand side *) 707 (* XXX: start work on the left hand side *) 708 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 709 (* XXX: work on fetch_many *) 710 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 711 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 712 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 713 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 714 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 715 >(eq_bv_eq … fetch_many_assm) newpc 716 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 717 (* XXX: work on sigma commutation *) 718 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 719 (* XXX: work on ticks (of all kinds) *) 720 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 721 (* XXX: removes status 's' *) 722 normalize nodelta >EQs s ticks 723 whd in ⊢ (??%%); 724 (* XXX: work on both sides *) 725 (* @split_eq_status try % *) 726 cases daemon 727 11,12: (* DIV *) 728 normalize nodelta in p; 729 >p normalize nodelta 730 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 731 (* XXX: work on fetch_many *) 732 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 733 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 734 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 735 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 736 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 737 >(eq_bv_eq … fetch_many_assm) newpc 738 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 739 (* XXX: work on sigma commutation *) 740 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 741 (* XXX: work on ticks (of all kinds) *) 742 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 743 (* XXX: work on both sides *) 744 @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl 745 >(?: pose_assm = 0) 746 [2,4: 747 <p >pose_refl 748 cases daemon 749 1,3: 750 (* XXX: removes status 's' *) 751 normalize nodelta >EQs s ticks 752 whd in ⊢ (??%%); 753 (* XXX: work on both sides *) 754 @split_eq_status try % 755 cases daemon 756 ] 757 13,14,15: (* DA *) 758 >p normalize nodelta 759 >p1 normalize nodelta 760 try (>p2 normalize nodelta 761 try (>p3 normalize nodelta 762 try (>p4 normalize nodelta 763 try (>p5 normalize nodelta)))) 764 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 765 (* XXX: work on fetch_many *) 766 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 767 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 768 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 769 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 770 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 771 >(eq_bv_eq … fetch_many_assm) newpc 772 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 773 (* XXX: work on sigma commutation *) 774 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 775 (* XXX: work on ticks (of all kinds) *) 776 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 777 (* XXX: work on both sides *) 778 @(pair_replace ?????????? p) 779 [1,3,5: 780 cases daemon 781 2,4,6: 782 @(if_then_else_replace ???????? p1) 783 [1,3,5: 784 cases daemon 785 2,4: 786 normalize nodelta 787 @(pair_replace ?????????? p2) 788 [1,3: 789 cases daemon 790 2,4: 791 normalize nodelta >p3 normalize nodelta 792 >p4 normalize nodelta try >p5 793 ] 794 ] 795 (* XXX: removes status 's' *) 796 normalize nodelta >EQs s ticks 797 whd in ⊢ (??%%); 798 (* XXX: work on both sides *) 799 @split_eq_status try % 800 cases daemon 801 ] 802 33,34,35: (* ANL, ORL, XRL *) 803 (* XXX: simplify the right hand side *) 804 [1,2,3: 805 inversion addr #addr' #EQaddr normalize nodelta 806 [1,3: 807 inversion addr' #addr'' #EQaddr' normalize nodelta 808 ] 809 ] 810 @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta 811 (* XXX: start work on the left hand side *) 812 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 813 (* XXX: work on fetch_many *) 814 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 815 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 816 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 817 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 818 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 819 >(eq_bv_eq … fetch_many_assm) newpc 820 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 821 (* XXX: work on sigma commutation *) 822 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 823 (* XXX: work on ticks (of all kinds) *) 824 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 825 (* XXX: simplify the left hand side *) 826 >EQaddr normalize nodelta try (>EQaddr' normalize nodelta) 827 >lft_rgt_refl normalize nodelta 828 (* XXX: removes status 's' *) 829 normalize nodelta >EQs s ticks 830 whd in ⊢ (??%%); 831 (* XXX: work on both sides *) 832 cases daemon 833  627 834 qed. 628 835 (*
Note: See TracChangeset
for help on using the changeset viewer.