- Timestamp:
- May 22, 2012, 5:37:09 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1983 r1984 1435 1435 [ nil ⇒ eq_bv … pc final_pc = true 1436 1436 | cons i tl ⇒ 1437 (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧ 1437 let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in 1438 (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧ 1438 1439 fetch_many code_memory final_pc pc' tl) 1439 1440 ]. … … 1507 1508 lapply (conjunction_true ?? H3) * #H4 #H5 1508 1509 lapply (conjunction_true … H4) * #B1 #B2 1509 %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)1510 >(eqb_true_to_refl … B2) %try % @IH @H21510 >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) % 1511 >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2 1511 1512 ] 1512 1513 qed. … … 2364 2365 // 2365 2366 qed. 2367 2368 (* XXX: easy but tedious *) 2369 axiom assembly1_lt_128: 2370 ∀i: instruction. 2371 |(assembly1 i)| < 128. 2372 2373 axiom most_significant_bit_zero: 2374 ∀size, m: nat. 2375 ∀size_proof: 0 < size. 2376 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false. 2377 normalize in size_proof; /2/ 2378 qed. 2379 2380 lemma bitvector_of_nat_sign_extension_equivalence: 2381 ∀m: nat. 2382 ∀size_proof: m < 128. 2383 sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m. 2384 #m #size_proof whd in ⊢ (??%?); 2385 >most_significant_bit_zero 2386 [1: 2387 cases daemon 2388 |2: 2389 assumption 2390 |3: 2391 // 2392 ] 2393 qed. -
src/ASM/AssemblyProofSplit.ma
r1983 r1984 95 95 qed. 96 96 97 lemma program_counter_set_arg_1: 98 ∀M: Type[0]. 99 ∀cm: M. 100 ∀s: PreStatus M cm. 101 ∀addr: [[bit_addr; carry]]. 102 ∀b: Bit. 103 program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s. 104 #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta 105 #addr #b 106 @(subaddressing_mode_elim … [[bit_addr; carry]] … [[bit_addr; carry]]) [1: // ] 107 [1: 108 #byte cases (split ????) #nu #nl normalize nodelta 109 cases (split ????) #ignore #three_bits normalize nodelta 110 cases (get_index_v bool ????) normalize nodelta 111 [1: 112 @program_counter_set_bit_addressable_sfr 113 |2: 114 @program_counter_set_low_internal_ram 115 ] 116 |2: 117 cases (split ????) // 118 ] 119 qed. 120 97 121 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 98 122 #P #A #a #abs destruct … … 166 190 fetch_many code_memory final_pc start_pc [i] → 167 191 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc. 168 #code_memory #final_pc #start_pc #i * #new_pc *169 #fetch_ refl #fetch_many_assm whd in fetch_many_assm;192 #code_memory #final_pc #start_pc #i * #new_pc 193 #fetch_many_assm whd in fetch_many_assm; 170 194 cases (eq_bv_eq … fetch_many_assm) assumption 171 195 qed. … … 184 208 ∀costs : BitVectorTrie costlabel 16. 185 209 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉. 186 ∀assembled : list Byte.187 ∀costs' : BitVectorTrie costlabel 16.188 ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉.189 ∀EQassembled : assembled=\fst (assembly cm sigma policy).190 210 ∀newppc : Word. 191 211 ∀lookup_labels : Identifier→Word. 192 ∀EQlookup_labels : lookup_labels = (λx:Identifier. sigma (address_of_word_labels_code_mem instr_list x)).212 ∀EQlookup_labels : lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 193 213 ∀lookup_datalabels : identifier ASMTag→Word. 194 214 ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). … … 205 225 (add 16 ppc (bitvector_of_nat 16 1))). 206 226 ∀P. 207 ∀EQP: 208 P = (λs. 209 execute (|expand_relative_jump lookup_labels sigma ppc instr|) 210 (code_memory_of_pseudo_assembly_program cm sigma 211 policy) 212 (status_of_pseudo_status M cm ps sigma policy) 213 =status_of_pseudo_status M' cm s sigma policy). 227 ∀EQP: P = (λinstr, s. 214 228 sigma (add 16 ppc (bitvector_of_nat 16 1)) 215 229 =add 16 (sigma ppc) … … 224 238 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels 225 239 (Instruction instr)) 226 →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm 240 → ∃n. execute n 241 (code_memory_of_pseudo_assembly_program cm sigma 242 policy) 243 (status_of_pseudo_status M cm ps sigma policy) 244 =status_of_pseudo_status M' cm s sigma policy). 245 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm 227 246 addr_of instr s). 228 247 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 229 #costs #create_label_cost_refl # assembled #costs' #assembly_refl #EQassembled #newppc248 #costs #create_label_cost_refl #newppc 230 249 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr 231 250 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP 232 #sigma_increment_commutation #maps_assm #fetch_many_assm251 (*#sigma_increment_commutation #maps_assm #fetch_many_assm *) 233 252 letin a ≝ Identifier letin m ≝ pseudo_assembly_program 234 cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s))253 cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s)) 235 254 [2: * // ] 236 255 @( … … 644 663 whd in match execute_1_preinstruction; normalize nodelta 645 664 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) 665 (* XXX: work on the right hand side *) 646 666 lapply (subaddressing_modein ???) 647 667 <EQaddr normalize nodelta #irrelevant 648 668 try (>p normalize nodelta) 649 669 try (>p1 normalize nodelta) 650 (* XXX: start work on the left hand side *) 651 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 652 (* XXX: work on fetch_many *) 653 <instr_refl in fetch_many_assm; #fetch_many_assm 654 <(fetch_many_singleton … fetch_many_assm) whd in ⊢ (??%?); 655 (* XXX: work on sigma commutation *) 656 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 657 (* XXX: work on both sides *) 670 (* XXX: switch to the left hand side *) 671 -instr_refl >EQP -P normalize nodelta 672 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 673 whd in ⊢ (??%?); 674 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 675 (* XXX: work on the left hand side *) 658 676 [1,2,3,4,5: 659 677 generalize in ⊢ (??(???(?%))?); … … 666 684 try @(jmpair_as_replace ?????????? p) 667 685 [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ] 668 normalize nodelta 669 (* XXX: work on ticks (of all kinds) *) 670 <instr_refl in EQticks; #EQticks >EQticks 671 (* XXX: removes status 's' *) 672 normalize nodelta >EQs -s -ticks 686 (* XXX: switch to the right hand side *) 687 normalize nodelta >EQs -s >EQticks -ticks 673 688 whd in ⊢ (??%%); 674 (* XXX: simplify the left hand side*)689 (* XXX: finally, prove the equality using sigma commutation *) 675 690 cases daemon 676 691 (* XXX: work on both sides *) 677 692 |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 678 (* XXX: simplifythe right hand side *)693 (* XXX: work on the right hand side *) 679 694 >p normalize nodelta 680 695 try (>p1 normalize nodelta) 681 (* XXX: start work on the left hand side *) 682 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 683 (* XXX: work on fetch_many *) 684 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 685 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 686 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 687 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 688 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 689 >(eq_bv_eq … fetch_many_assm) -newpc 690 >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); 691 (* XXX: work on sigma commutation *) 692 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 693 (* XXX: work on ticks (of all kinds) *) 694 >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks 695 (* XXX: simplify the left hand side *) 696 (* XXX: switch to the left hand side *) 697 -instr_refl >EQP -P normalize nodelta 698 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 699 whd in ⊢ (??%?); 700 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 701 (* XXX: work on the left hand side *) 696 702 @(pair_replace ?????????? p) 697 703 [1,3,5,7,9,11,13,15,17: … … 704 710 ] 705 711 ] 706 (* XXX: removes status 's'*)707 normalize nodelta >EQs -s -ticks712 (* XXX: switch to the right hand side *) 713 normalize nodelta >EQs -s >EQticks -ticks 708 714 whd in ⊢ (??%%); 709 (* XXX: work on both sides*)715 (* XXX: finally, prove the equality using sigma commutation *) 710 716 cases daemon (* 711 717 @split_eq_status try % … … 715 721 ] *) 716 722 |10,42,43,44,45,49,52,56: (* MUL *) 717 (* XXX: simplify the right hand side *) 718 (* XXX: start work on the left hand side *) 719 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 720 (* XXX: work on fetch_many *) 721 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 722 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 723 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 724 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 725 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 726 >(eq_bv_eq … fetch_many_assm) -newpc 727 >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); 728 (* XXX: work on sigma commutation *) 729 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 730 (* XXX: work on ticks (of all kinds) *) 731 >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks 732 (* XXX: removes status 's' *) 733 normalize nodelta >EQs -s -ticks 723 (* XXX: work on the right hand side *) 724 (* XXX: switch to the left hand side *) 725 -instr_refl >EQP -P normalize nodelta 726 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 727 whd in ⊢ (??%?); 728 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 729 (* XXX: work on the left hand side *) 730 (* XXX: switch to the right hand side *) 731 normalize nodelta >EQs -s >EQticks -ticks 734 732 whd in ⊢ (??%%); 735 (* XXX: work on both sides *) 736 (* @split_eq_status try % *) 733 (* XXX: finally, prove the equality using sigma commutation *) 737 734 cases daemon 738 735 |11,12: (* DIV *) 736 (* XXX: work on the right hand side *) 739 737 normalize nodelta in p; 740 738 >p normalize nodelta 741 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 742 (* XXX: work on fetch_many *) 743 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 744 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 745 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 746 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 747 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 748 >(eq_bv_eq … fetch_many_assm) -newpc 749 >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); 750 (* XXX: work on sigma commutation *) 751 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 752 (* XXX: work on ticks (of all kinds) *) 753 >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks 754 (* XXX: work on both sides *) 739 (* XXX: switch to the left hand side *) 740 -instr_refl >EQP -P normalize nodelta 741 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 742 whd in ⊢ (??%?); 743 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 755 744 @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl 756 >(?: pose_assm = 0) 745 >(?: pose_assm = 0) normalize nodelta 757 746 [2,4: 758 747 <p >pose_refl 759 748 cases daemon 760 749 |1,3: 761 (* XXX: removes status 's'*)762 normalize nodelta >EQs -s -ticks750 (* XXX: switch to the right hand side *) 751 >EQs -s >EQticks -ticks 763 752 whd in ⊢ (??%%); 764 (* XXX: work on both sides*)753 (* XXX: finally, prove the equality using sigma commutation *) 765 754 @split_eq_status try % 766 755 cases daemon 767 756 ] 768 757 |13,14,15: (* DA *) 758 (* XXX: work on the right hand side *) 769 759 >p normalize nodelta 770 760 >p1 normalize nodelta … … 773 763 try (>p4 normalize nodelta 774 764 try (>p5 normalize nodelta)))) 775 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 776 (* XXX: work on fetch_many *) 777 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 778 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 779 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 780 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 781 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 782 >(eq_bv_eq … fetch_many_assm) -newpc 783 >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); 784 (* XXX: work on sigma commutation *) 785 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 786 (* XXX: work on ticks (of all kinds) *) 787 >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks 788 (* XXX: work on both sides *) 765 (* XXX: switch to the left hand side *) 766 -instr_refl >EQP -P normalize nodelta 767 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 768 whd in ⊢ (??%?); 769 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 770 (* XXX: work on the left hand side *) 789 771 @(pair_replace ?????????? p) 790 772 [1,3,5: … … 804 786 ] 805 787 ] 806 (* XXX: removes status 's' *) 807 normalize nodelta >EQs -s -ticks 788 (* XXX: switch to the right hand side *) 789 normalize nodelta >EQs -s >EQticks -ticks 790 whd in ⊢ (??%%); 791 (* XXX: finally, prove the equality using sigma commutation *) 792 @split_eq_status try % 793 cases daemon 794 ] 795 |33,34,35,48: (* ANL, ORL, XRL, MOVX *) 796 (* XXX: work on the right hand side *) 797 cases addr #addr' normalize nodelta 798 [1,3: 799 cases addr' #addr'' normalize nodelta 800 ] 801 @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta 802 (* XXX: switch to the left hand side *) 803 -instr_refl >EQP -P normalize nodelta 804 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 805 whd in ⊢ (??%?); 806 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 807 (* XXX: work on the left hand side *) 808 (* XXX: switch to the right hand side *) 809 normalize nodelta >EQs -s >EQticks -ticks 810 whd in ⊢ (??%%); 811 (* XXX: finally, prove the equality using sigma commutation *) 812 cases daemon 813 |47: (* MOV *) 814 (* XXX: work on the right hand side *) 815 cases addr -addr #addr normalize nodelta 816 [1: 817 cases addr #addr normalize nodelta 818 [1: 819 cases addr #addr normalize nodelta 820 [1: 821 cases addr #addr normalize nodelta 822 [1: 823 cases addr #addr normalize nodelta 824 ] 825 ] 826 ] 827 ] 828 cases addr #lft #rgt normalize nodelta 829 (* XXX: switch to the left hand side *) 830 >EQP -P normalize nodelta 831 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 832 whd in ⊢ (??%?); 833 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 834 (* XXX: work on the left hand side *) 835 (* XXX: switch to the right hand side *) 836 normalize nodelta >EQs -s >EQticks -ticks 837 whd in ⊢ (??%%); 838 (* XXX: finally, prove the equality using sigma commutation *) 839 cases daemon 840 |16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *) 841 (* XXX: work on the right hand side *) 842 >p normalize nodelta 843 (* XXX: switch to the left hand side *) 844 -instr_refl >EQP -P normalize nodelta 845 #sigma_increment_commutation #maps_assm #fetch_many_assm 846 847 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 848 whd in match (expand_relative_jump ????); 849 <EQppc in fetch_many_assm; 850 @pair_elim #result #flags #sub16_refl 851 @pair_elim #upper #lower #split_refl 852 cases (eq_bv ???) normalize nodelta 853 [1,3,5,7,9,11,13: 854 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 855 whd in ⊢ (??%?); 856 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 857 (* XXX: work on the left hand side *) 858 @(if_then_else_replace ???????? p) normalize nodelta 859 [1,3,5,7,9,11,13: 860 cases daemon 861 ] 862 (* XXX: switch to the right hand side *) 863 normalize nodelta >EQs -s >EQticks -ticks 808 864 whd in ⊢ (??%%); 809 (* XXX: work on both sides*)865 (* XXX: finally, prove the equality using sigma commutation *) 810 866 @split_eq_status try % 811 867 cases daemon 812 ] 813 |33,34,35,48: (* ANL, ORL, XRL, MOVX *) 814 (* XXX: simplify the right hand side *) 815 inversion addr #addr' #EQaddr normalize nodelta 816 [1,3: 817 inversion addr' #addr'' #EQaddr' normalize nodelta 818 ] 819 @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta 820 (* XXX: start work on the left hand side *) 821 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 822 (* XXX: work on fetch_many *) 823 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 824 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 825 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 826 <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 827 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 828 >(eq_bv_eq … fetch_many_assm) -newpc 829 >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); 830 (* XXX: work on sigma commutation *) 831 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 832 (* XXX: work on ticks (of all kinds) *) 833 >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks 834 (* XXX: simplify the left hand side *) 835 >EQaddr normalize nodelta try (>EQaddr' normalize nodelta) 836 >lft_rgt_refl normalize nodelta 837 (* XXX: removes status 's' *) 838 normalize nodelta >EQs -s -ticks 839 whd in ⊢ (??%%); 840 (* XXX: work on both sides *) 841 cases daemon 842 |47: (* MOV *) 843 |* (* JUMPS!!! *) 868 |2,4,6,8,10,12,14: 869 >EQppc 870 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 871 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' 872 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' 873 #fetch_many_assm whd in fetch_many_assm; %{2} 874 change with (execute_1 ?? = ?) 875 @(pose … (execute_1 ? (status_of_pseudo_status …))) 876 #status_after_1 #EQstatus_after_1 877 <(?: ? = status_after_1) 878 [3,6,9,12,15,18,21: 879 >EQstatus_after_1 in ⊢ (???%); 880 whd in ⊢ (???%); 881 [1: <fetch_refl in ⊢ (???%); 882 |2: <fetch_refl in ⊢ (???%); 883 |3: <fetch_refl in ⊢ (???%); 884 |4: <fetch_refl in ⊢ (???%); 885 |5: <fetch_refl in ⊢ (???%); 886 |6: <fetch_refl in ⊢ (???%); 887 |7: <fetch_refl in ⊢ (???%); 888 ] 889 whd in ⊢ (???%); 890 @(if_then_else_replace ???????? p) 891 [1,3,5,7,9,11,13: 892 cases daemon 893 |2,4,6,8,10,12,14: 894 normalize nodelta 895 whd in match (addr_of_relative ????); 896 >set_clock_mk_Status_commutation 897 [5: 898 (* XXX: demodulation not working in this case *) 899 >program_counter_set_arg_1 in ⊢ (???%); 900 >program_counter_set_program_counter in ⊢ (???%); 901 |*: 902 /demod/ 903 ] 904 whd in ⊢ (???%); 905 change with (add ???) in match (\snd (half_add ???)); 906 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 907 [2,4,6,8,10,12,14: 908 >bitvector_of_nat_sign_extension_equivalence 909 [1,3,5,7,9,11,13: 910 >EQintermediate_pc' % 911 |*: 912 repeat @le_S_S @le_O_n 913 ] 914 ] 915 % 916 ] 917 |1,4,7,10,13,16,19: 918 skip 919 ] 920 -status_after_1 921 @(pose … (execute_1 ? (mk_PreStatus …))) 922 #status_after_1 #EQstatus_after_1 923 <(?: ? = status_after_1) 924 [3,6,9,12,15,18,21: 925 >EQstatus_after_1 in ⊢ (???%); 926 whd in ⊢ (???%); 927 (* XXX: matita bug with patterns across multiple goals *) 928 [1: <fetch_refl'' in ⊢ (???%); 929 |2: <fetch_refl'' in ⊢ (???%); 930 |3: <fetch_refl'' in ⊢ (???%); 931 |4: <fetch_refl'' in ⊢ (???%); 932 |5: <fetch_refl'' in ⊢ (???%); 933 |6: <fetch_refl'' in ⊢ (???%); 934 |7: <fetch_refl'' in ⊢ (???%); 935 ] 936 whd in ⊢ (???%); 937 [5: 938 |*: 939 /demod/ 940 ] % 941 |1,4,7,10,13,16,19: 942 skip 943 ] 944 -status_after_1 whd in ⊢ (??%?); 945 (* XXX: switch to the right hand side *) 946 normalize nodelta >EQs -s >EQticks -ticks 947 whd in ⊢ (??%%); 948 (* XXX: finally, prove the equality using sigma commutation *) 949 @split_eq_status try % 950 [3,7,11,15,20,28,32: 951 >program_counter_set_program_counter >set_clock_mk_Status_commutation 952 [5: >program_counter_set_program_counter ] 953 >EQaddr_of normalize nodelta 954 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta 955 >EQcm % 956 |*: 957 cases daemon 958 ] 844 959 ] 845 960 qed.
Note: See TracChangeset
for help on using the changeset viewer.