Changeset 2160 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 6, 2012, 5:26:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2143 r2160 360 360 ∀sigma: Word → Word. 361 361 ∀policy: Word → bool. 362 \snd M = (None …)→362 \snd M = data → 363 363 special_function_registers_8051 pseudo_assembly_program cm s = 364 364 special_function_registers_8051 (BitVectorTrie Byte 16) … … 372 372 qed. 373 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: 374 lemma n_lt_19_elim_prop: 375 ∀P: nat → Prop. 376 P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 → 377 P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 → 378 (∀n. n < 19 → P n). 379 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 380 #H15 #H16 #H17 #H18 #H19 #n 381 cases n [1: // ] 382 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 383 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 384 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 385 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 386 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 387 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 388 #n' normalize in ⊢ (% → ?); 389 #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd) 390 cases (lt_to_not_zero … absurd) 391 qed. 392 393 lemma get_index_v_set_index_miss: 394 ∀T: Type[0]. 395 ∀n, i, j: nat. 396 ∀v: Vector T n. 397 ∀b: T. 398 ∀i_proof: i < n. 399 ∀j_proof: j < n. 400 i ≠ j → 401 get_index_v T n (set_index T n v i b i_proof) j j_proof = 402 get_index_v T n v j j_proof. 403 #T #n #i #j #v lapply i lapply j elim v #i #j 404 [1: 405 #b #i_proof 406 cases (lt_to_not_zero … i_proof) 407 2: 408 #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j 409 lapply i_proof lapply i_neq_j cases i' 410 [1: 411 i_neq_j #i_neq_j i_proof #i_proof 412 whd in match (set_index ??????); 413 lapply j_proof lapply i_neq_j cases j' 414 [1: 415 #relevant @⊥ cases relevant relevant #absurd @absurd % 416 2: 417 #j' #_ j_proof #j_proof % 418 ] 419 2: 420 #i' i_neq_j #i_neq_j i_proof #i_proof 421 lapply j_proof lapply i_neq_j cases j' 422 [1: 423 #_ #j_proof % 424 2: 425 #j' #i_neq_j #j_proof 426 @inductive_hypothesis @nmk #relevant 427 cases i_neq_j #absurd @absurd >relevant % 428 ] 429 ] 430 ] 431 qed. 432 433 lemma get_index_v_special_function_registers_8051_not_acc_a: 386 434 ∀M: internal_pseudo_address_map. 387 435 ∀cm: pseudo_assembly_program. 388 ∀ ps.436 ∀s: PreStatus pseudo_assembly_program cm. 389 437 ∀sigma: Word → Word. 390 438 ∀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 439 ∀n: nat. 440 ∀proof: n < 19. 441 n ≠ 17 → 442 (get_index_v Byte 19 443 (special_function_registers_8051 pseudo_assembly_program cm s) n 444 proof = 445 get_index_v Byte 19 446 (special_function_registers_8051 (BitVectorTrie Byte 16) 447 (code_memory_of_pseudo_assembly_program cm sigma policy) 448 (status_of_pseudo_status M cm s sigma policy)) n 449 proof). 450 #M #cm #s #sigma #policy #n #proof lapply proof 451 @(n_lt_19_elim_prop … proof) proof #proof 452 [18: 453 #absurd @⊥ cases absurd absurd #absurd @absurd % 399 454 ] 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 *) 440 441 (* 442 lemma pi1_let_commute: 443 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 444 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t). 445 #A #B #C #P * #a #b * // 446 qed. 447 448 lemma pi1_let_as_commute: 449 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 450 pi1 … (let 〈x1,y1〉 as H ≝ c in t) = 451 (let 〈x1,y1〉 as H ≝ c in pi1 … t). 452 #A #B #C #P * #a #b * // 453 qed. 454 455 lemma tech_pi1_let_as_commute: 456 ∀A,B,C,P. ∀f. ∀c,c':A × B. 457 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c. 458 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c. 459 c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) → 460 pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) = 461 f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)). 462 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/ 463 qed. 464 *) 455 #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 456 whd in match status_of_pseudo_status; normalize nodelta 457 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 458 cases M #left #right cases right normalize nodelta try % 459 right * #address 460 @pair_elim #high #low #high_low_refl normalize nodelta 461 whd in match sfr_8051_index; normalize nodelta 462 >get_index_v_set_index_miss try % 463 #absurd destruct(absurd) 464 qed. 465 465 466 466 include alias "arithmetics/nat.ma". … … 477 477 #fetch_many_assm whd in fetch_many_assm; 478 478 cases (eq_bv_eq … fetch_many_assm) assumption 479 qed. 480 481 (* XXX: this needs an extra invariant relating address and word that we look 482 up! 483 *) 484 definition map_lower_internal_ram_address_using_pseudo_address_map: 485 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ 486 λM: internal_pseudo_address_map. 487 λsigma: Word → Word. 488 λaddress: Byte. 489 λvalue: Byte. 490 match assoc_list_lookup ?? address (eq_bv …) (\fst M) with 491 [ None ⇒ value 492  Some upper_lower_word ⇒ 493 let 〈upper_lower, word〉 ≝ upper_lower_word in 494 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in 495 if eq_upper_lower upper_lower upper then 496 high 497 else 498 low 499 ]. 500 501 lemma get_8051_sfr_status_of_pseudo_status: 502 ∀M. 503 ∀cm, ps, sigma, policy. 504 ∀sfr. 505 (sfr = SFR_ACC_A → \snd M = data) → 506 get_8051_sfr (BitVectorTrie Byte 16) 507 (code_memory_of_pseudo_assembly_program cm sigma policy) 508 (status_of_pseudo_status M cm ps sigma policy) sfr = 509 get_8051_sfr pseudo_assembly_program cm ps sfr. 510 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant 511 [18: 512 >relevant % 513 ] 514 cases sndM try % * #address 515 whd in match get_8051_sfr; 516 whd in match status_of_pseudo_status; normalize nodelta 517 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 518 @pair_elim #upper #lower #upper_lower_refl 519 @get_index_v_set_index_miss @nmk #relevant 520 normalize in relevant; destruct(relevant) 521 qed. 522 523 lemma bitvector_cases_hd_tl: 524 ∀n: nat. 525 ∀w: BitVector (S n). 526 ∃hd: bool. ∃tl: BitVector n. 527 w ≃ hd:::tl. 528 #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant 529 qed. 530 531 lemma external_ram_set_bit_addressable_sfr: 532 ∀M: Type[0]. 533 ∀cm: M. 534 ∀ps. 535 ∀w. 536 ∀result: Byte. 537 external_ram M cm 538 (set_bit_addressable_sfr M cm ps w result) = 539 external_ram M cm ps. 540 #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma! 541 whd in match set_bit_addressable_sfr; normalize nodelta 542 cases (eqb ??) normalize nodelta [1: cases not_implemented ] 543 cases (eqb ??) normalize nodelta [1: % ] 544 cases (eqb ??) normalize nodelta [1: cases not_implemented ] 545 cases (eqb ??) normalize nodelta [1: % ] 546 cases (eqb ??) normalize nodelta [1: % ] 547 cases (eqb ??) normalize nodelta [1: % ] 548 cases (eqb ??) normalize nodelta [1: % ] 549 cases (eqb ??) normalize nodelta [1: % ] 550 cases (eqb ??) normalize nodelta [1: % ] 551 cases (eqb ??) normalize nodelta [1: % ] 552 cases (eqb ??) normalize nodelta [1: % ] 553 cases (eqb ??) normalize nodelta [1: % ] 554 cases (eqb ??) normalize nodelta [1: % ] 555 cases (eqb ??) normalize nodelta [1: % ] 556 cases (eqb ??) normalize nodelta [1: % ] 557 cases (eqb ??) normalize nodelta [1: % ] 558 cases (eqb ??) normalize nodelta [1: % ] 559 cases (eqb ??) normalize nodelta [1: % ] 560 cases (eqb ??) normalize nodelta [1: % ] 561 cases (eqb ??) normalize nodelta [1: % ] 562 cases (eqb ??) normalize nodelta [1: % ] 563 cases (eqb ??) normalize nodelta [1: % ] 564 cases (eqb ??) normalize nodelta [1: % ] 565 cases (eqb ??) normalize nodelta [1: % ] 566 cases (eqb ??) normalize nodelta [1: % ] 567 cases (eqb ??) normalize nodelta [1: % ] 568 cases not_implemented *) 569 qed. 570 571 lemma external_ram_set_arg_8: 572 ∀M: Type[0]. 573 ∀cm: M. 574 ∀ps. 575 ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]]. 576 ∀result. 577 external_ram M cm (set_arg_8 M cm ps addr1 result) = 578 external_ram M cm ps. 579 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 580 #M #cm #ps #addr1 #result 581 @(subaddressing_mode_elim … addr1) try #w try % 582 whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *) 583 [1: 584 cases (vsplit bool ???) #nu #nl normalize nodelta 585 cases (vsplit bool ???) #ignore #three_bits normalize nodelta 586 cases (get_index_v bool ????) normalize nodelta try % 587 @external_ram_set_bit_addressable_sfr 588 2: 589 cases (vsplit bool ???) #nu #nl normalize nodelta 590 cases (vsplit bool ???) #ignore #three_bits normalize nodelta 591 cases (get_index_v bool ????) normalize nodelta % 592 ] 593 qed. 594 595 lemma special_function_registers_8051_set_clock: 596 ∀M: Type[0]. 597 ∀cm: M. 598 ∀ps. 599 ∀t. 600 special_function_registers_8051 M cm (set_clock M cm ps t) = 601 special_function_registers_8051 M cm ps. 602 // 603 qed. 604 605 lemma get_arg_8_pseudo_addressing_mode_ok: 606 ∀M: internal_pseudo_address_map. 607 ∀cm: pseudo_assembly_program. 608 ∀ps: PreStatus pseudo_assembly_program cm. 609 ∀sigma: Word → Word. 610 ∀policy: Word → bool. 611 ∀addr1: [[registr; direct]]. 612 addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true → 613 get_arg_8 (BitVectorTrie Byte 16) 614 (code_memory_of_pseudo_assembly_program cm sigma policy) 615 (status_of_pseudo_status M cm ps sigma policy) true addr1 = 616 get_arg_8 pseudo_assembly_program cm ps true addr1. 617 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 618 #M #cm #ps #sigma #policy #addr1 619 @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%); 620 [1: 621 whd in ⊢ (??%? → ??%?); 622 whd in match bit_address_of_register; normalize nodelta 623 @pair_elim #un #ln #un_ln_refl 624 lapply (refl_to_jmrefl ??? un_ln_refl) un_ln_refl #un_ln_refl 625 @(pair_replace ?????????? un_ln_refl) 626 [1: 627 whd in match get_8051_sfr; normalize nodelta 628 whd in match sfr_8051_index; normalize nodelta 629 @eq_f <get_index_v_special_function_registers_8051_not_acc_a 630 try % #absurd destruct(absurd) 631 2: 632 #assembly_mode_ok_refl 633 >low_internal_ram_of_pseudo_internal_ram_miss 634 [1: 635 % 636 2: 637 cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta 638 #absurd try % @sym_eq assumption 639 ] 640 ] 641 2: 642 #addressing_mode_ok_refl whd in ⊢ (??%?); 643 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 644 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 645 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta 646 [1: 647 whd in ⊢ (??%%); normalize nodelta 648 cases (eqb ??) normalize nodelta [1: % ] 649 cases (eqb ??) normalize nodelta [1: % ] 650 cases (eqb ??) normalize nodelta [1: % ] 651 cases (eqb ??) normalize nodelta [1: % ] 652 cases (eqb ??) normalize nodelta [1: 653 @get_8051_sfr_status_of_pseudo_status 654 #absurd destruct(absurd) 655 ] 656 cases (eqb ??) normalize nodelta [1: 657 @get_8051_sfr_status_of_pseudo_status 658 #absurd destruct(absurd) 659 ] 660 cases (eqb ??) normalize nodelta [1: 661 @get_8051_sfr_status_of_pseudo_status 662 #absurd destruct(absurd) 663 ] 664 cases (eqb ??) normalize nodelta [1: 665 @get_8051_sfr_status_of_pseudo_status 666 #absurd destruct(absurd) 667 ] 668 cases (eqb ??) normalize nodelta [1: 669 @get_8051_sfr_status_of_pseudo_status 670 #absurd destruct(absurd) 671 ] 672 cases (eqb ??) normalize nodelta [1: % ] 673 cases (eqb ??) normalize nodelta [1: % ] 674 cases (eqb ??) normalize nodelta [1: % ] 675 cases (eqb ??) normalize nodelta [1: % ] 676 cases (eqb ??) normalize nodelta [1: % ] 677 cases (eqb ??) normalize nodelta [1: 678 @get_8051_sfr_status_of_pseudo_status 679 #absurd destruct(absurd) 680 ] 681 cases (eqb ??) normalize nodelta [1: 682 @get_8051_sfr_status_of_pseudo_status 683 #absurd destruct(absurd) 684 ] 685 cases (eqb ??) normalize nodelta [1: 686 @get_8051_sfr_status_of_pseudo_status 687 #absurd destruct(absurd) 688 ] 689 cases (eqb ??) normalize nodelta [1: 690 @get_8051_sfr_status_of_pseudo_status 691 #absurd destruct(absurd) 692 ] 693 cases (eqb ??) normalize nodelta [1: 694 @get_8051_sfr_status_of_pseudo_status 695 #absurd destruct(absurd) 696 ] 697 cases (eqb ??) normalize nodelta [1: 698 @get_8051_sfr_status_of_pseudo_status 699 #absurd destruct(absurd) 700 ] 701 cases (eqb ??) normalize nodelta [1: 702 @get_8051_sfr_status_of_pseudo_status 703 #absurd destruct(absurd) 704 ] 705 cases (eqb ??) normalize nodelta [1: 706 @get_8051_sfr_status_of_pseudo_status 707 #absurd destruct(absurd) 708 ] 709 cases (eqb ??) normalize nodelta [1: 710 @get_8051_sfr_status_of_pseudo_status 711 #absurd destruct(absurd) 712 ] 713 cases (eqb ??) normalize nodelta [1: 714 @get_8051_sfr_status_of_pseudo_status 715 #absurd destruct(absurd) 716 ] 717 inversion (eqb ??) #eqb_refl normalize nodelta [1: 718 @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl 719 whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl) 720 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta 721 #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_ 722 #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) % 723 ] 724 cases (eqb ??) normalize nodelta [1: 725 @get_8051_sfr_status_of_pseudo_status 726 #absurd destruct(absurd) 727 ] % 728 2: 729 lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant 730 whd in match status_of_pseudo_status; normalize nodelta 731 >low_internal_ram_of_pseudo_internal_ram_miss try % 732 cut(arg = false:::(three_bits@@nl)) 733 [1: 734 <get_index_v_refl 735 cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits) 736 [1: 737 cut(ignore = [[get_index_v bool 4 nu 0 ?]]) 738 [1: 739 @le_S_S @le_O_n 740 2: 741 cut(ignore = \fst (vsplit bool 1 3 nu)) 742 [1: 743 >ignore_three_bits_refl % 744 2: 745 #ignore_refl >ignore_refl 746 cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl 747 >nu_refl % 748 ] 749 3: 750 #ignore_refl >ignore_refl in ignore_three_bits_refl; 751 #relevant lapply (vsplit_ok ?????? (sym_eq … relevant)) 752 #nu_refl <nu_refl % 753 ] 754 2: 755 #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl 756 @sym_eq @vsplit_ok >nu_nl_refl % 757 ] 758 2: 759 #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant; 760 normalize nodelta 761 [1: 762 cases (eq_bv ???) normalize #absurd destruct(absurd) 763 2: 764 #_ % 765 ] 766 ] 767 ] 768 ] 769 qed. 770 771 lemma special_function_registers_8051_set_program_counter: 772 ∀M: Type[0]. 773 ∀cm: M. 774 ∀ps. 775 ∀pc: Word. 776 special_function_registers_8051 M cm (set_program_counter M cm ps pc) = 777 special_function_registers_8051 M cm ps. 778 // 779 qed. 780 781 lemma special_function_registers_8052_set_program_counter: 782 ∀M: Type[0]. 783 ∀cm: M. 784 ∀ps. 785 ∀pc: Word. 786 special_function_registers_8052 M cm (set_program_counter M cm ps pc) = 787 special_function_registers_8052 M cm ps. 788 // 789 qed. 790 791 lemma set_index_set_index_commutation: 792 ∀A: Type[0]. 793 ∀n: nat. 794 ∀v: Vector A n. 795 ∀m, o: nat. 796 ∀m_lt_proof: m < n. 797 ∀o_lt_proof: o < n. 798 ∀e, f: A. 799 m ≠ o → 800 set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof = 801 set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof. 802 #A #n #v elim v 803 [1: 804 #m #o #m_lt_proof 805 normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof) 806 2: 807 #n' #hd #tl #inductive_hypothesis 808 #m #o 809 cases m cases o 810 [1: 811 #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant 812 @relevant % 813 2,3: 814 #o' normalize // 815 4: 816 #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm 817 normalize @eq_f @inductive_hypothesis @nmk #relevant 818 >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) % 819 ] 820 ] 821 qed. 822 823 lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051: 824 ∀M: internal_pseudo_address_map. 825 ∀cm: pseudo_assembly_program. 826 ∀ps. 827 ∀sigma: Word → Word. 828 ∀policy: Word → bool. 829 ∀sfr. 830 ∀result: Byte. 831 eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false → 832 special_function_registers_8051 (BitVectorTrie Byte 16) 833 (code_memory_of_pseudo_assembly_program cm sigma policy) 834 (set_8051_sfr (BitVectorTrie Byte 16) 835 (code_memory_of_pseudo_assembly_program cm sigma policy) 836 (status_of_pseudo_status M cm ps sigma policy) sfr result) = 837 sfr_8051_of_pseudo_sfr_8051 M 838 (special_function_registers_8051 pseudo_assembly_program cm 839 (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma. 840 #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm 841 whd in match (set_8051_sfr ?????); 842 cases M #callM * try % #upper_lower #address 843 whd in match (special_function_registers_8051 ???); 844 whd in match (sfr_8051_of_pseudo_sfr_8051 ???); 845 @pair_elim #high #low #high_low_refl normalize nodelta 846 cases (eq_upper_lower ??) normalize nodelta 847 whd in match (set_8051_sfr ?????); 848 @set_index_set_index_commutation @nmk #relevant 849 @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm)) 850 qed. 851 852 lemma special_function_registers_8051_set_arg_8: 853 ∀M: internal_pseudo_address_map. 854 ∀cm: pseudo_assembly_program. 855 ∀ps. 856 ∀sigma: Word → Word. 857 ∀policy: Word → bool. 858 ∀addr1: [[ registr; direct ]]. 859 ∀result. 860 addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true → 861 special_function_registers_8051 (BitVectorTrie Byte 16) 862 (code_memory_of_pseudo_assembly_program cm sigma policy) 863 (set_arg_8 (BitVectorTrie Byte 16) 864 (code_memory_of_pseudo_assembly_program cm sigma policy) 865 (status_of_pseudo_status M cm ps sigma policy) addr1 result) = 866 sfr_8051_of_pseudo_sfr_8051 M 867 (special_function_registers_8051 pseudo_assembly_program cm 868 (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma. 869 cases daemon 870 (* 871 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 872 #M #cm #ps #sigma #policy #addr1 #result 873 @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try % 874 whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?); 875 whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?)); 876 cases (vsplit bool ???) #nu #nl normalize nodelta 877 cases (vsplit bool ???) #ignore #three_bits normalize nodelta 878 cases (get_index_v bool ????) normalize nodelta try % 879 whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%); 880 cases (eqb ??) normalize nodelta [1: cases not_implemented ] 881 cases (eqb ??) normalize nodelta [1: % ] 882 cases (eqb ??) normalize nodelta [1: cases not_implemented ] 883 cases (eqb ??) normalize nodelta [1: % ] 884 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 885 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 886 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 887 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 888 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 889 cases (eqb ??) normalize nodelta [1: % ] 890 cases (eqb ??) normalize nodelta [1: % ] 891 cases (eqb ??) normalize nodelta [1: % ] 892 cases (eqb ??) normalize nodelta [1: % ] 893 cases (eqb ??) normalize nodelta [1: % ] 894 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 895 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 896 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 897 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 898 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 899 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 900 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 901 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 902 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 903 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 904 inversion (eqb ??) #eqb_refl normalize nodelta [1: 905 whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl; 906 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta 907 #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm 908 whd in match (status_of_pseudo_status ?????); 909 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 910 >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta % 911 ] 912 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ] 913 cases not_implemented *) 479 914 qed. 480 915 … … 507 942 ∀fetch_pseudo_refl: \fst (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr. 508 943 ∀ticks: nat × nat. 509 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).944 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr). 510 945 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 511 946 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). … … 933 1368 s 934 1369 ] (refl … instr)) 935 try (cases(other))1370 try cases other 936 1371 try assumption (*20s*) 937 1372 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) … … 955 1390 [1,3: 956 1391 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 957 whd in ⊢ (??%?);958 1392 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 959 1393 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1394 whd in ⊢ (??%?); 960 1395 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1396 lapply maps_assm whd in ⊢ (??%? → ?); 1397 inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta 1398 [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl M' 961 1399 (* XXX: work on the left hand side *) 962 1400 @(pair_replace ?????????? p) normalize nodelta 963 1401 [1,3: 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 *) 1402 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) 1403 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1404 >(get_arg_8_set_program_counter … true addr1) 1405 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1406 @get_arg_8_pseudo_addressing_mode_ok assumption 1407 2,4: 1408 >p1 normalize nodelta >EQs 1409 alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)". 1410 >set_program_counter_status_of_pseudo_status 1411 whd in ⊢ (??%%); 1412 @split_eq_status 1413 [1,10: 1414 whd in ⊢ (??%%); >set_arg_8_set_program_counter 1415 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1416 >low_internal_ram_set_program_counter 1417 [1: 1418 >low_internal_ram_set_program_counter 1419 (* XXX: ??? *) 1420 2: 1421 >low_internal_ram_set_clock 1422 (* XXX: ??? *) 989 1423 ] 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 *) 1424 2,11: 1425 whd in ⊢ (??%%); >set_arg_8_set_program_counter 1426 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1427 >high_internal_ram_set_program_counter 1428 [1: 1429 >high_internal_ram_set_program_counter 1430 (* XXX: ??? *) 1431 2: 1432 >high_internal_ram_set_clock 1433 (* XXX: ??? *) 1004 1434 ] 1435 3,12: 1436 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); 1437 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1438 >(external_ram_set_arg_8 ??? addr1) 1439 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 1440 4,13: 1441 whd in ⊢ (??%%); >EQaddr_of normalize nodelta 1442 [1: 1443 >program_counter_set_program_counter 1444 >set_arg_8_set_program_counter 1445 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1446 >set_clock_set_program_counter >program_counter_set_program_counter 1447 change with (add ??? = ?) 1448 (* XXX: ??? *) 1449 2: 1450 >set_arg_8_set_program_counter 1451 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1452 >program_counter_set_program_counter 1453 >set_arg_8_set_program_counter 1454 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1455 >set_clock_set_program_counter >program_counter_set_program_counter 1456 >sigma_increment_commutation <EQppc 1457 whd in match (assembly_1_pseudoinstruction ??????); 1458 whd in match (expand_pseudo_instruction ??????); 1459 (* XXX: ??? *) 1460 ] 1461 5,14: 1462 whd in match (special_function_registers_8051 ???); 1463 [1: 1464 >special_function_registers_8051_set_program_counter 1465 >special_function_registers_8051_set_clock 1466 >set_arg_8_set_program_counter in ⊢ (???%); 1467 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1468 >special_function_registers_8051_set_program_counter 1469 >set_arg_8_set_program_counter 1470 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1471 >special_function_registers_8051_set_program_counter 1472 @special_function_registers_8051_set_arg_8 assumption 1473 2: 1474 >special_function_registers_8051_set_clock 1475 >set_arg_8_set_program_counter 1476 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1477 >set_arg_8_set_program_counter 1478 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1479 >special_function_registers_8051_set_program_counter 1480 >special_function_registers_8051_set_program_counter 1481 @special_function_registers_8051_set_arg_8 assumption 1482 ] 1483 6,15: 1484 whd in match (special_function_registers_8052 ???); 1485 whd in match (special_function_registers_8052 ???) in ⊢ (???%); 1486 [1: 1487 >set_arg_8_set_program_counter 1488 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1489 >set_arg_8_set_program_counter 1490 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1491 >special_function_registers_8052_set_program_counter 1492 >special_function_registers_8052_set_program_counter 1493 @special_function_registers_8052_set_arg_8 assumption 1494 2: 1495 whd in ⊢ (??%%); 1496 >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption 1497 ] 1498 (* XXX: we need special_function_registers_8052_set_arg_8 *) 1499 7,16: 1500 whd in match (p1_latch ???); 1501 whd in match (p1_latch ???) in ⊢ (???%); 1502 (* XXX: we need p1_latch_8052_set_arg_8 *) 1503 8,17: 1504 whd in match (p3_latch ???); 1505 whd in match (p3_latch ???) in ⊢ (???%); 1506 (* XXX: we need p3_latch_8052_set_arg_8 *) 1507 9: 1508 >clock_set_clock 1509 >clock_set_program_counter in ⊢ (???%); >clock_set_clock 1510 >EQticks <instr_refl @eq_f2 1511 [1: 1512 whd in ⊢ (??%%); whd in match (ticks_of0 ??????); 1513 2: 1514 (* XXX: we need clock_set_arg_8 *) 1515 ] 1516 18: 1005 1517 ] 1006 1518 ] … … 1018 1530 7,16,25,34: 1019 1531 8,17,26,35: 1020 whd in ⊢ (??%%); 1532 whd in ⊢ (??%%);maps_assm 1021 1533 1022 1534 9,18,27,36:
Note: See TracChangeset
for help on using the changeset viewer.