Changeset 2151
- Timestamp:
- Jul 3, 2012, 6:12:24 PM (6 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2148 r2151 708 708 ∧ 709 709 (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16 710 (*nat_of_bitvector … pc < nat_of_bitvector … next_pc*) ∨ 711 S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …). 710 ∨ 711 S (nat_of_bitvector … ppc) = |instr_list| ∧ 712 nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16). 713 714 715 (*CSC: move elsewhere*) 716 axiom add_bitvector_of_nat: 717 ∀n,m1,m2. 718 bitvector_of_nat n (m1 + m2) = 719 add n (bitvector_of_nat n m1) (bitvector_of_nat n m2). 720 721 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels: 722 ∀lookup_labels,sigma,policy,ppc,pi. 723 ∀lookup_datalabels1,lookup_datalabels2. 724 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) = 725 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi). 726 #lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2 727 cases pi // 728 qed. 729 730 lemma fst_snd_assembly_1_pseudoinstruction: 731 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled. 732 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi 733 = 〈len,assembled〉 → 734 len = |assembled|. 735 #lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled 736 inversion (assembly_1_pseudoinstruction ??????) #len' #assembled' 737 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct % 738 qed. 712 739 713 740 definition assembly: … … 736 763 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) 737 764 assembled K 738 ≝ ?. cases daemon(*765 ≝ 739 766 λp. 740 767 λsigma. 741 768 λpolicy. 742 769 deplet 〈preamble, instr_list〉 as p_refl ≝ p in 743 let 〈labels_to_ppc,ppc_to_costs〉≝ create_label_cost_map instr_list in770 deplet 〈labels_to_ppc,ppc_to_costs〉 as eq_create_label_cost_map ≝ create_label_cost_map instr_list in 744 771 let datalabels ≝ construct_datalabels preamble in 745 772 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in … … 753 780 let 〈ppc,code〉 ≝ ppc_code in 754 781 ppc = bitvector_of_nat … (|pre|) ∧ 782 |code| ≤ 2^16 ∧ 755 783 (nat_of_bitvector … (sigma ppc) = |code| ∨ 756 784 sigma ppc = zero … ∧ |code| = 2^16) ∧ … … 760 788 let 〈len,assembledi〉 ≝ 761 789 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 790 |assembledi| ≤ |reverse … code| ∧ 762 791 ∀j:nat. ∀H: j < |assembledi|. ∀K. 763 792 nth_safe ? j assembledi H = … … 773 802 〈reverse … revcode, 774 803 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 775 [ cases (foldl_strong ? (λx.Σy.?) ???) in p 2; #ignore_revcode #Hfold #EQignore_revcode804 [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode 776 805 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 777 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd % 806 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold3 #Hfold2 whd 807 <eq_create_label_cost_map whd % 778 808 [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16) 779 809 [ #limit %2 @limit 780 810 | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 781 811 @not_eq_to_le_to_lt assumption ] 782 | >length_reverse <Hfold3 % 783 [ @(transitive_le … (S (nat_of_bitvector … (sigma next_pc)))) 784 [ // | change with (? < ?); @lt_nat_of_bitvector ] 785 | >Hfold1 % ]] 812 | >length_reverse % try assumption cases Hfold3 -Hfold3 813 [ #Hfold3 <Hfold3 % >Hfold1 % 814 | #Hfold5 %2 <Hfold1 assumption ]] 786 815 | * #sigma_pol_ok1 #_ #instr_list_ok % 787 [ % // >sigma_pol_ok1 % ]816 [ % % // >sigma_pol_ok1 % ] 788 817 #ppc' #ppc_ok' #abs @⊥ cases abs 789 818 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip] 790 819 |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ] 791 820 | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code 792 #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [% 821 #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH 822 * * #IH1 #IH2 * 823 [2: #H @⊥ cases daemon (*CSC: impossible case, using Jaaps's ? *)] 824 #IH3 #IH5 825 cut (|prefix| < |instr_list|) 826 [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list 827 cut (|prefix| < 2^16) 828 [ @(lt_to_le_to_lt … (|instr_list|)) assumption ] #prefix_ok 829 cut (nat_of_bitvector … ppc < |instr_list|) 830 [ >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ] #ppc_ok 831 cut (\snd hd = \fst (fetch_pseudo_instruction instr_list ppc ppc_ok)) 832 [ >prf in ppc_ok; >IH1 >(add_zero … (bitvector_of_nat … (|prefix|))) 833 >fetch_pseudo_instruction_append 834 [ #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 835 whd in match (nth_safe ????); [ cases hd // | normalize // ] 836 | <add_zero >nat_of_bitvector_bitvector_of_nat_inverse 837 [ <prf assumption | assumption ] 838 | skip 839 | <prf assumption 840 ]] #eq_fetch_pseudo_instruction 841 lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta 842 cut (pc_delta < 2^16) 843 [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok 844 % [ % [% ] ] 845 [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat 846 | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*) 847 | cases (sigma_pol_ok2 … ppc_ok) 848 whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction 849 <eq_create_label_cost_map 850 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] 851 #sigma_ok >sigma_ok #sigma_pol_ok3 -sigma_pol_ok2 852 >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol_ok3 853 [ #LT %1 >nat_of_bitvector_add 854 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption] 855 >nat_of_bitvector_bitvector_of_nat_inverse try assumption // 856 | * #EQ1 #EQ2 %2 % 857 [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus 858 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero 859 | >commutative_plus assumption ]] 860 | cases daemon 861 ] 862 863 (* 864 865 % [% 793 866 [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon 794 867 |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]] -
src/ASM/AssemblyProof.ma
r2149 r2151 179 179 | _ ⇒ True 180 180 ]. 181 182 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:183 ∀lookup_labels,sigma,policy,ppc,pi.184 ∀lookup_datalabels1,lookup_datalabels2.185 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =186 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).187 #lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2188 cases pi //189 qed.190 191 lemma fst_snd_assembly_1_pseudoinstruction:192 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.193 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi194 = 〈len,assembled〉 →195 len = |assembled|.196 #lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled197 inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'198 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %199 qed.200 181 201 182 (* XXX: easy but tedious *) … … 355 336 ] 356 337 | * #EQ1 #EQ2 %2 % 357 [ <add_bitvector_of_nat_Sm >add_commutative assumption 338 [ <add_bitvector_of_nat_Sm >add_commutative >H 339 lapply (eq_f … (bitvector_of_nat 16) … EQ2) 340 <add_bitvector_of_nat_plus 341 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero 358 342 | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption 359 343 ]]] … … 437 421 [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled'; 438 422 <add_bitvector_of_nat_Sm >add_commutative 439 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 assumption ] 423 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 424 lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2 425 <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector 426 #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ] 440 427 cases (le_to_or_lt_eq … instr_list_ok) 441 428 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
Note: See TracChangeset
for help on using the changeset viewer.