Changeset 2160
 Timestamp:
 Jul 6, 2012, 5:26:21 PM (8 years ago)
 Location:
 src/ASM
 Files:

 1 added
 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2157 r2160 384 384 qed. 385 385 386 inductive upper_lower: Type[0] ≝ 387  upper: upper_lower 388  lower: upper_lower. 389 390 definition eq_upper_lower: 391 upper_lower → upper_lower → bool ≝ 392 λleft: upper_lower. 393 λright: upper_lower. 394 match left with 395 [ upper ⇒ 396 match right with 397 [ upper ⇒ true 398  _ ⇒ false 399 ] 400  lower ⇒ 401 match right with 402 [ lower ⇒ true 403  _ ⇒ false 404 ] 405 ]. 406 407 lemma eq_upper_lower_true_to_eq: 408 ∀left: upper_lower. 409 ∀right: upper_lower. 410 eq_upper_lower left right = true → left = right. 411 * * normalize try (#_ %) 412 #absurd destruct(absurd) 413 qed. 414 415 lemma eq_upper_lower_false_to_neq: 416 ∀left: upper_lower. 417 ∀right: upper_lower. 418 eq_upper_lower left right = false → left ≠ right. 419 * * normalize try (#absurd destruct(absurd)) 420 @nmk #absurd destruct(absurd) 421 qed. 422 423 inductive accumulator_address_map_entry: Type[0] ≝ 424  data: accumulator_address_map_entry 425  address: upper_lower → Word → accumulator_address_map_entry. 426 427 definition eq_accumulator_address_map_entry: 428 accumulator_address_map_entry → accumulator_address_map_entry → bool ≝ 429 λleft: accumulator_address_map_entry. 430 λright: accumulator_address_map_entry. 431 match left with 432 [ data ⇒ 433 match right with 434 [ data ⇒ true 435  _ ⇒ false 436 ] 437  address upper_lower word ⇒ 438 match right with 439 [ address upper_lower' word' ⇒ 440 eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word' 441  _ ⇒ false 442 ] 443 ]. 444 445 lemma eq_accumulator_address_map_entry_true_to_eq: 446 ∀left: accumulator_address_map_entry. 447 ∀right: accumulator_address_map_entry. 448 eq_accumulator_address_map_entry left right = true → left = right. 449 #left #right cases left cases right 450 [1: 451 #_ % 452 2,3: 453 #upper_lower #word normalize #absurd destruct(absurd) 454 4: 455 #upper_lower #word #upper_lower' #word' normalize 456 cases upper_lower' normalize nodelta 457 cases upper_lower normalize 458 [2,3: 459 #absurd destruct(absurd) 460 ] 461 change with (eq_bv 16 ?? = true → ?) 462 #relevant lapply (eq_bv_eq … relevant) 463 #word_refl >word_refl % 464 ] 465 qed. 466 467 lemma eq_bv_false_to_neq: 468 ∀n: nat. 469 ∀left, right: BitVector n. 470 eq_bv n left right = false → left ≠ right. 471 #n #left elim left 472 [1: 473 #right >(BitVector_O … right) normalize #absurd destruct(absurd) 474 2: 475 #n' #hd #tl #inductive_hypothesis #right 476 cases (BitVector_Sn … right) #hd' * #tl' #right_refl 477 >right_refl normalize 478 cases hd normalize nodelta 479 cases hd' normalize nodelta 480 [2,3: 481 #_ @nmk #absurd destruct(absurd) 482 ] 483 change with (eq_bv ??? = false → ?) 484 #relevant lapply (inductive_hypothesis … relevant) 485 #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm 486 #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) % 487 ] 488 qed. 489 490 lemma eq_accumulator_address_map_entry_false_to_neq: 491 ∀left: accumulator_address_map_entry. 492 ∀right: accumulator_address_map_entry. 493 eq_accumulator_address_map_entry left right = false → left ≠ right. 494 #left #right cases left cases right 495 [1: 496 normalize #absurd destruct(absurd) 497 2,3: 498 #upper_lower #word normalize #_ 499 @nmk #absurd destruct(absurd) 500 4: 501 #upper_lower #word #upper_lower' #word' normalize 502 cases upper_lower' normalize nodelta 503 cases upper_lower normalize nodelta 504 [2,3: 505 #_ @nmk #absurd destruct(absurd) 506 ] 507 change with (eq_bv ??? = false → ?) 508 #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm) 509 #word_neq_assm @nmk #address_eq_assm cases word_neq_assm 510 #word_eq_assm @word_eq_assm destruct(address_eq_assm) % 511 ] 512 qed. 513 386 514 (* XXX: changed this type. Bool specifies whether byte is first or second 387 515 component of an address, and the Word is the pseudoaddress that it … … 389 517 A. 390 518 *) 391 definition internal_pseudo_address_map ≝ list ( (BitVector 8) × (bool × Word)) × (option (bool × Word)).519 definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry. 392 520 393 521 include alias "ASM/BitVectorTrie.ma". … … 402 530 403 531 axiom low_internal_ram_of_pseudo_internal_ram_hit: 404 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀ high: bool. ∀points_to: Word. ∀addr:BitVector 7.405 assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)→532 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7. 533 assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 → 406 534 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 407 535 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in … … 409 537 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in 410 538 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in 411 if highthen539 if eq_upper_lower upper_lower upper then 412 540 (pbl = higher) ∧ (bl = phigher) 413 541 else … … 426 554 match addr with 427 555 [ DIRECT d ⇒ 428 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 429 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 556 if eq_bv … d (bitvector_of_nat … 224) then 557 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data 558 else 559 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 430 560  INDIRECT i ⇒ 431 561 let d ≝ get_register … s [[false;false;i]] in 432 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 433 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 562 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) 434 563  EXT_INDIRECT _ ⇒ true 435  REGISTER _ ⇒ true 436  ACC_A ⇒ match \snd M with [ None ⇒ true  _ ⇒ false ] 564  REGISTER r ⇒ 565 let address ≝ bit_address_of_register … s r in 566 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 567  ACC_A ⇒ match \snd M with [ data ⇒ true  _ ⇒ false ] 437 568  ACC_B ⇒ true 438 569  DPTR ⇒ true … … 448 579  RELATIVE _ ⇒ true 449 580  ADDR11 _ ⇒ true 450  ADDR16 _ ⇒ true ]. 581  ADDR16 _ ⇒ true 582 ]. 451 583 452 584 definition next_internal_pseudo_address_map0 ≝ … … 464 596 let a' ≝ addr_of a s in 465 597 let 〈callM, accM〉 ≝ M in 466 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈 false, a'〉〉::467 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈 true, a'〉〉::callM, accM〉598 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉:: 599 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉 468 600  Mov _ _ ⇒ Some … M 469 601  Instruction instr ⇒ 470 match instr with 471 [ ADD addr1 addr2 ⇒ 472 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 602 match instr return λx. option internal_pseudo_address_map with 603 [ ADD addr1 addr2 ⇒ 604 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 605 Some ? M 606 else 607 None ? 608  ADDC addr1 addr2 ⇒ 609 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 610 Some ? M 611 else 612 None ? 613  SUBB addr1 addr2 ⇒ 614 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 615 Some ? M 616 else 617 None ? 618  INC addr1 ⇒ 619 if addressing_mode_ok T M ? s addr1 then 620 Some ? M 621 else 622 None ? 623  DEC addr1 ⇒ 624 if addressing_mode_ok T M … s addr1 then 625 Some ? M 626 else 627 None ? 628  MUL addr1 addr2 ⇒ 629 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 630 Some ? M 631 else 632 None ? 633  DIV addr1 addr2 ⇒ 634 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 635 Some ? M 636 else 637 None ? 638  DA addr1 ⇒ 639 if addressing_mode_ok T M … s addr1 then 640 Some ? M 641 else 642 None ? 643  JC addr1 ⇒ Some ? M 644  JNC addr1 ⇒ Some ? M 645  JB addr1 addr2 ⇒ Some ? M 646  JNB addr1 addr2 ⇒ Some ? M 647  JBC addr1 addr2 ⇒ Some ? M 648  JZ addr1 ⇒ Some ? M 649  JNZ addr1 ⇒ Some ? M 650  CJNE addr1 addr2 ⇒ 651 match addr1 with 652 [ inl l ⇒ 653 let 〈left, right〉 ≝ l in 654 if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then 655 Some ? M 656 else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then 657 Some ? M 658 else 659 None ? 660  inr r ⇒ 661 let 〈left, right〉 ≝ r in 662 if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then 663 Some ? M 664 else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then 665 Some ? M 666 else 667 None ? 668 ] 669  DJNZ addr1 addr2 ⇒ 670 if addressing_mode_ok T M … s addr1 then 671 Some ? M 672 else 673 None ? 674  CLR addr1 ⇒ 675 if addressing_mode_ok T M … s addr1 then 676 Some ? M 677 else 678 None ? 679  CPL addr1 ⇒ 680 if addressing_mode_ok T M … s addr1 then 681 Some ? M 682 else 683 None ? 684  RL addr1 ⇒ 685 if addressing_mode_ok T M … s addr1 then 686 Some ? M 687 else 688 None ? 689  RLC addr1 ⇒ 690 if addressing_mode_ok T M … s addr1 then 691 Some ? M 692 else 693 None ? 694  RR addr1 ⇒ 695 if addressing_mode_ok T M … s addr1 then 696 Some ? M 697 else 698 None ? 699  RRC addr1 ⇒ 700 if addressing_mode_ok T M … s addr1 then 701 Some ? M 702 else 703 None ? 704  SWAP addr1 ⇒ 705 if addressing_mode_ok T M … s addr1 then 706 Some ? M 707 else 708 None ? 709  SETB addr1 ⇒ 710 if addressing_mode_ok T M … s addr1 then 711 Some ? M 712 else 713 None ? 714 (* XXX: need to track addresses pushed and popped off the stack? *) 715  PUSH addr1 ⇒ 716 let 〈callM, accM〉 ≝ M in 717 match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 718 [ DIRECT d ⇒ λproof. 719 let extended ≝ pad 8 8 d in 720 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉 721  _ ⇒ λother: False. ⊥ 722 ] (subaddressing_modein … addr1) 723  POP addr1 ⇒ Some … M 724  XCH addr1 addr2 ⇒ 725 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 726 Some ? M 727 else 728 None ? 729  XCHD addr1 addr2 ⇒ 730 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 731 Some ? M 732 else 733 None ? 734  RET ⇒ 735 let 〈callM, accM〉 ≝ M in 736 let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 737 let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 738 if sp_plus_1 ∧ sp_plus_2 then 739 Some … M 740 else 741 None ? 742  RETI ⇒ 743 let 〈callM, accM〉 ≝ M in 744 let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 745 let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 746 if sp_plus_1 ∧ sp_plus_2 then 747 Some … M 748 else 749 None ? 750  NOP ⇒ Some … M 751  MOVX addr1 ⇒ Some … M 752  XRL addr1 ⇒ 753 match addr1 with 754 [ inl l ⇒ 755 let 〈acc_a, others〉 ≝ l in 756 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 757 let others_ok ≝ addressing_mode_ok T M … s others in 758 if acc_a_ok ∧ others_ok then 473 759 Some ? M 474 760 else 475 761 None ? 476  ADDC addr1 addr2 ⇒ 477 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 762  inr r ⇒ 763 let 〈direct, others〉 ≝ r in 764 let direct_ok ≝ addressing_mode_ok T M … s direct in 765 let others_ok ≝ addressing_mode_ok T M … s others in 766 if direct_ok ∧ others_ok then 478 767 Some ? M 479 768 else 480 769 None ? 481  SUBB addr1 addr2 ⇒ 482 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 770 ] 771  ORL addr1 ⇒ 772 match addr1 with 773 [ inl l ⇒ 774 match l with 775 [ inl l ⇒ 776 let 〈acc_a, others〉 ≝ l in 777 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 778 let others_ok ≝ addressing_mode_ok T M … s others in 779 if acc_a_ok ∧ others_ok then 780 Some ? M 781 else 782 None ? 783  inr r ⇒ 784 let 〈direct, others〉 ≝ r in 785 let direct_ok ≝ addressing_mode_ok T M … s direct in 786 let others_ok ≝ addressing_mode_ok T M … s others in 787 if direct_ok ∧ others_ok then 788 Some ? M 789 else 790 None ? 791 ] 792  inr r ⇒ 793 let 〈carry, others〉 ≝ r in 794 let carry_ok ≝ addressing_mode_ok T M … s carry in 795 let others_ok ≝ addressing_mode_ok T M … s others in 796 if carry_ok ∧ others_ok then 483 797 Some ? M 484 else 485 None ? 486  _ ⇒ (* TO BE COMPLETED *) Some ? M ]]. 798 else 799 None ? 800 ] 801  ANL addr1 ⇒ 802 match addr1 with 803 [ inl l ⇒ 804 match l with 805 [ inl l ⇒ 806 let 〈acc_a, others〉 ≝ l in 807 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 808 let others_ok ≝ addressing_mode_ok T M … s others in 809 if acc_a_ok ∧ others_ok then 810 Some ? M 811 else 812 None ? 813  inr r ⇒ 814 let 〈direct, others〉 ≝ r in 815 let direct_ok ≝ addressing_mode_ok T M … s direct in 816 let others_ok ≝ addressing_mode_ok T M … s others in 817 if direct_ok ∧ others_ok then 818 Some ? M 819 else 820 None ? 821 ] 822  inr r ⇒ 823 let 〈carry, others〉 ≝ r in 824 let carry_ok ≝ addressing_mode_ok T M … s carry in 825 let others_ok ≝ addressing_mode_ok T M … s others in 826 if carry_ok ∧ others_ok then 827 Some ? M 828 else 829 None ? 830 ] 831  MOV addr1 ⇒ Some … M 832 ] 833 ]. 834 cases other 835 qed. 487 836 488 837 definition next_internal_pseudo_address_map ≝ … … 509 858 λsigma: Word → Word. 510 859 match \snd M with 511 [ None ⇒ sfrs 512  Some s ⇒ 513 let 〈high, address〉 ≝ s in 860 [ data ⇒ sfrs 861  address upper_lower address ⇒ 514 862 let index ≝ sfr_8051_index SFR_ACC_A in 515 let 〈 upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in516 if highthen517 set_index Byte 19 sfrs index upper?863 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in 864 if eq_upper_lower upper_lower upper then 865 set_index Byte 19 sfrs index high ? 518 866 else 519 set_index Byte 19 sfrs index low er?867 set_index Byte 19 sfrs index low ? 520 868 ]. 521 869 // … … 640 988 *) 641 989 642 (* XXX: check values returned for conditional jumps below! *) 990 (* XXX: check values returned for conditional jumps below! They are wrong, 991 find correct values *) 643 992 definition ticks_of0: 644 993 ∀p:pseudo_assembly_program. 645 ( Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝994 (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝ 646 995 λprogram: pseudo_assembly_program. 996 λlookup_labels: Identifier → Word. 647 997 λsigma. 648 998 λpolicy. … … 653 1003 match instr with 654 1004 [ JC lbl ⇒ 655 if policy ppc then 656 〈4, 4〉 657 else 658 〈2, 2〉 1005 let lookup_address ≝ sigma (lookup_labels lbl) in 1006 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1007 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1008 if sj_possible then 1009 〈2, 2〉 1010 else 1011 〈4, 4〉 659 1012  JNC lbl ⇒ 660 if policy ppc then 661 〈4, 4〉 662 else 663 〈2, 2〉 1013 let lookup_address ≝ sigma (lookup_labels lbl) in 1014 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1015 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1016 if sj_possible then 1017 〈2, 2〉 1018 else 1019 〈4, 4〉 664 1020  JB bit lbl ⇒ 665 if policy ppc then 666 〈4, 4〉 667 else 668 〈2, 2〉 1021 let lookup_address ≝ sigma (lookup_labels lbl) in 1022 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1023 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1024 if sj_possible then 1025 〈2, 2〉 1026 else 1027 〈4, 4〉 669 1028  JNB bit lbl ⇒ 670 if policy ppc then 671 〈4, 4〉 672 else 673 〈2, 2〉 1029 let lookup_address ≝ sigma (lookup_labels lbl) in 1030 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1031 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1032 if sj_possible then 1033 〈2, 2〉 1034 else 1035 〈4, 4〉 674 1036  JBC bit lbl ⇒ 675 if policy ppc then 676 〈4, 4〉 677 else 678 〈2, 2〉 1037 let lookup_address ≝ sigma (lookup_labels lbl) in 1038 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1039 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1040 if sj_possible then 1041 〈2, 2〉 1042 else 1043 〈4, 4〉 679 1044  JZ lbl ⇒ 680 if policy ppc then 681 〈4, 4〉 682 else 683 〈2, 2〉 1045 let lookup_address ≝ sigma (lookup_labels lbl) in 1046 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1047 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1048 if sj_possible then 1049 〈2, 2〉 1050 else 1051 〈4, 4〉 684 1052  JNZ lbl ⇒ 685 if policy ppc then 686 〈4, 4〉 687 else 688 〈2, 2〉 1053 let lookup_address ≝ sigma (lookup_labels lbl) in 1054 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1055 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1056 if sj_possible then 1057 〈2, 2〉 1058 else 1059 〈4, 4〉 689 1060  CJNE arg lbl ⇒ 690 if policy ppc then 691 〈4, 4〉 692 else 693 〈2, 2〉 1061 let lookup_address ≝ sigma (lookup_labels lbl) in 1062 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1063 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1064 if sj_possible then 1065 〈2, 2〉 1066 else 1067 〈4, 4〉 694 1068  DJNZ arg lbl ⇒ 695 if policy ppc then 696 〈4, 4〉 697 else 698 〈2, 2〉 1069 let lookup_address ≝ sigma (lookup_labels lbl) in 1070 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1071 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1072 if sj_possible then 1073 〈2, 2〉 1074 else 1075 〈4, 4〉 699 1076  ADD arg1 arg2 ⇒ 700 1077 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in … … 785 1162  Cost cost ⇒ 〈0, 0〉 786 1163  Jmp jmp ⇒ 787 if policy ppc then 788 〈4, 4〉 1164 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1165 let do_a_long ≝ policy ppc in 1166 let lookup_address ≝ sigma (lookup_labels jmp) in 1167 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 1168 if sj_possible ∧ ¬ do_a_long then 1169 〈2, 2〉 (* XXX: SJMP *) 1170 else 1171 let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in 1172 if mj_possible ∧ ¬ do_a_long then 1173 〈2, 2〉 (* XXX: AJMP *) 1174 else 1175 〈2, 2〉 (* XXX: LJMP *) 1176  Call call ⇒ 1177 (* XXX: collapse the branches as they are identical? *) 1178 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 1179 let lookup_address ≝ sigma (lookup_labels call) in 1180 let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in 1181 let do_a_long ≝ policy ppc in 1182 if mj_possible ∧ ¬ do_a_long then 1183 〈2, 2〉 (* ACALL *) 789 1184 else 790 〈2, 2〉 791  Call call ⇒ 792 if policy ppc then 793 〈4, 4〉 794 else 795 〈2, 2〉 1185 〈2, 2〉 (* LCALL *) 796 1186  Mov dptr tgt ⇒ 〈2, 2〉 797 1187 ]. … … 799 1189 definition ticks_of: 800 1190 ∀p:pseudo_assembly_program. 801 ( Word → Word) → (Word → bool) → ∀ppc:Word.1191 (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word. 802 1192 nat_of_bitvector … ppc < \snd p → nat × nat ≝ 803 1193 λprogram: pseudo_assembly_program. 1194 λlookup_labels. 804 1195 λsigma. 805 1196 λpolicy. … … 807 1198 let pseudo ≝ \snd program in 808 1199 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in 809 ticks_of0 program sigma policy ppc fetched.1200 ticks_of0 program lookup_labels sigma policy ppc fetched. 810 1201 811 1202 (* 
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: 
src/ASM/Interpret.ma
r2130 r2160 944 944 try (@or_intror //) 945 945 try #_ 946 try /demod nohyps by clock_set_clock,clock_set_8051_sfr, set_arg_8_ok,set_arg_1_ok,946 try /demod nohyps by clock_set_clock,clock_set_8051_sfr,clock_set_arg_8,set_arg_1_ok, 947 947 program_counter_set_8051_sfr,program_counter_set_arg_1/ 948 948 try (% @I) try (@or_introl % @I) try (@or_intror % @I) // 
src/ASM/Status.ma
r2139 r2160 617 617 qed. 618 618 619 definition set_bit_addressable_sfr ≝ 619 definition set_bit_addressable_sfr': 620 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 621 Σs':PreStatus M code_memory. 622 clock … code_memory s = clock … code_memory s' ∧ 623 program_counter … code_memory s = program_counter … code_memory s' ≝ 620 624 λM: Type[0]. 621 625 λcode_memory:M. … … 625 629 let address ≝ nat_of_bitvector … b in 626 630 if (eqb address 128) then 627 ?631 match not_implemented in False with [ ] 628 632 else if (eqb address 144) then 629 633 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in … … 631 635 status_2 632 636 else if (eqb address 160) then 633 ?637 match not_implemented in False with [ ] 634 638 else if (eqb address 176) then 635 639 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in … … 681 685 set_8051_sfr ?? s SFR_ACC_B v 682 686 else 683 ?. 684 cases not_implemented 687 match not_implemented in False with [ ]. 688 /2 by refl, pair_destruct/ 689 qed. 690 691 definition set_bit_addressable_sfr: 692 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 693 PreStatus M code_memory ≝ set_bit_addressable_sfr'. 694 695 lemma clock_set_bit_addressable_sfr: 696 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte. 697 clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v). 698 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 699 cases (set_bit_addressable_sfr' ?????) #s' * // 700 qed. 701 702 lemma program_counter_set_bit_addressable_sfr: 703 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte. 704 program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v). 705 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 706 cases (set_bit_addressable_sfr' ?????) #s' * // 685 707 qed. 686 708 … … 880 902 qed. 881 903 882 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v). 883 884 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; 904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 885 905 acc_a ; acc_b ; ext_indirect ; 886 ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory. 887 clock … code_memory s = clock … code_memory s' ≝ 906 ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory. 907 clock … code_memory s = clock … code_memory s' ∧ 908 (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧ 909 (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧ 910 program_counter … code_memory s = program_counter … code_memory s' ∧ 911 (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝ 888 912 λm, cm, s, a, v. 889 913 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 890 914 acc_a ; acc_b ; ext_indirect ; 891 915 ext_indirect_dptr ]] x) → 892 Σs':PreStatus m cm. clock m cm s = clock m cm s'916 Σs':PreStatus m cm. ? 893 917 (*CSC: bug here if one specified the two clock above*) 894 918 with … … 936 960 match other in False with [ ] 937 961 ] (subaddressing_modein … a). 938 // qed. 962 /6 by conj, False_ind/ 963 qed. 939 964 940 965 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝ 941 966 set_arg_8'. 942 967 943 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 944 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2 968 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 969 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 970 cases (set_arg_8' ?????) #s' * * * * // 971 qed. 972 973 lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v). 974 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 975 cases (set_arg_8' ?????) #s' * * * * // 976 qed. 977 978 lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v). 979 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 980 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 981 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 982 * * * * #_ #relevant #_ #_ #_ @relevant @I 983 qed. 984 985 lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v). 986 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 987 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 988 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 989 * * * * #_ #_ #relevant #_ #_ @relevant @I 990 qed. 991 992 lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v). 993 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 994 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 995 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 996 * * * * #_ #_ #_ #_ #relevant @relevant @I 945 997 qed. 946 998
Note: See TracChangeset
for help on using the changeset viewer.