Changeset 901
 Timestamp:
 Jun 8, 2011, 5:27:35 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r897 r901 672 672 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. 673 673 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 674 (* 674 675 675 axiom half_add_SO: 676 676 ∀pc. 677 677 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). 678 678 679 (* 679 680 axiom not_eqvb_S: 680 681 ∀pc. … … 714 715 ]. 715 716 716 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. 717 lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2. 718 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) → 719 let intermediate_pc ≝ pc + length … l1 in 720 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧ 721 encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. 722 #code_memory #final_pc #l1 elim l1 723 [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/ 724  #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm 725 #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ] 726 qed. 727 728 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. 717 729 718 730 axiom bitvector_3_elim_prop: … … 722 734 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 723 735 724 lemma test:736 axiom fetch_assembly: 725 737 ∀pc,i,code_memory,assembled. 726 738 assembled = assembly1 i → … … 731 743 let 〈instr,pc'〉 ≝ instr_pc in 732 744 (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 733 #pc #i #code_memory #assembled cases i [8: *]745 (* #pc #i #code_memory #assembled cases i [8: *] 734 746 [16,20,29: * * 18,19: * * [1,2,4,5: *] 28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] 735 747 [47,48,49: … … 755 767 69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2] 756 768 whd >eq_instruction_refl >H4 @eq_bv_refl 757 qed. 758 769 qed. *) 770 771 let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝ 772 match expected with 773 [ nil ⇒ eq_bv … pc final_pc = true 774  cons i tl ⇒ 775 let fetched ≝ fetch code_memory pc in 776 let 〈instr_pc, ticks〉 ≝ fetched in 777 let 〈instr,pc'〉 ≝ instr_pc in 778 eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl]. 779 780 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. 781 #A #a #b #EQ destruct // 782 qed. 783 784 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2. 785 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/ 786 qed. 787 788 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2. 789 790 lemma fetch_assembly_pseudo: 791 ∀program,ppc,lookup_labels,lookup_datalabels. 792 ∀pi,code_memory,len,assembled,instructions,pc. 793 let expansion ≝ jump_expansion_policy program ppc in 794 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → 795 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → 796 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 797 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 798 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 799 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2; #EQ2a #EQ2b 800 >EQ2a >EQ2b EQ2a EQ2b; 801 generalize in match (pc + flatten … (map … assembly1 instructions)); #final_pc 802 generalize in match pc elim instructions 803 [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl 804  #i #tl #IH #pc #H whd cases (encoding_check_append … H); H; #H1 #H2 whd 805 generalize in match (fetch_assembly pc i code_memory … (refl …) H1) 806 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) 807 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) K; #K1 #K2 % // 808 >(eq_bv_to_eq … K2) @IH @H2 ] 809 qed. 810 811 lemma fetch_assembly_pseudo: 812 ∀program,ppc,lookup_labels,lookup_datalabels. 813 ∀pc,pi,code_memory,instructions,len,assembled. 814 let expansion ≝ jump_expansion_policy program ppc in 815 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → 816 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → 817 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 818 fetch_many code_memory len (bitvector_of_nat … pc) instructions. 819 #program #ppc #lookup_labels #lookup_datalabels #pc #pi #code_memory #instructions #len #assembled 820 #EQ1 #EQ2 generalize in match EQ1 EQ1; generalize in match pc pc; elim instructions 821 [ #pc #EQ1 #H whd whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2 822 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2; #EQ2a #EQ2b >EQ2b 823 whd in ⊢ (% → %) #H >EQ2a <plus_n_O 824 (* OK, ARITHMETIC *) cases daemon 825  #i #tl #IH #pc #EQ1 whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2 826 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2 #EQ2a #EQ2b 827 change in EQ2b with (? = ?@flatten …) >EQ2b in IH ⊢ %; assembled; #IH #H 828 cases (encoding_check_append … H); H; #H1 #H2 whd 829 generalize in match (fetch_assembly pc i code_memory … (refl …) H1) 830 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) 831 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) K; #K1 #K2 % // 832 >(eq_bv_to_eq … K2) @IH 833 [ 834  @H2 835 ] 836 ] 837 qed. 838 759 839 (* This establishes the correspondence between pseudo program counters and 760 840 program counters. It is at the heart of the proof. *)
Note: See TracChangeset
for help on using the changeset viewer.