 Timestamp:
 Jul 6, 2012, 11:34:09 AM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2156 r2157 731 731 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct % 732 732 qed. 733 734 (* XXX: easy but tedious *) 735 lemma assembly1_lt_128: 736 ∀i: instruction. 737 (assembly1 i) < 128. 738 cases daemon 739 (* XXX: commented out as takes ages to type check 740 #i cases i 741 try (#assm1 #assm2) try #assm1 742 [8: 743 cases assm1 744 try (#assm1 #assm2) try #assm1 745 whd in match assembly1; normalize nodelta 746 whd in match assembly_preinstruction; normalize nodelta 747 try @(subaddressing_mode_elim … assm2) 748 try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta 749 [32: 750 cases assm1 assm1 #assm1 normalize nodelta 751 cases assm1 #addr1 #addr2 normalize nodelta 752 [1: 753 @(subaddressing_mode_elim … addr2) 754 2: 755 @(subaddressing_mode_elim … addr1) 756 ] 757 #w 758 35,36,37: 759 cases assm1 assm1 #assm1 normalize nodelta 760 [1,3: 761 cases assm1 assm1 #assm1 normalize nodelta 762 ] 763 cases assm1 #addr1 #addr2 normalize nodelta 764 @(subaddressing_mode_elim … addr2) try #w 765 49: 766 cases assm1 assm1 #assm1 normalize nodelta 767 [1: 768 cases assm1 assm1 #assm1 normalize nodelta 769 [1: 770 cases assm1 assm1 #assm1 normalize nodelta 771 [1: 772 cases assm1 assm1 #assm1 normalize nodelta 773 [1: 774 cases assm1 assm1 #assm1 normalize nodelta 775 ] 776 ] 777 ] 778 ] 779 cases assm1 #addr1 #addr2 normalize nodelta 780 [1,3,4,5: 781 @(subaddressing_mode_elim … addr2) try #w 782 *: 783 @(subaddressing_mode_elim … addr1) try #w 784 normalize nodelta 785 [1,2: 786 @(subaddressing_mode_elim … addr2) try #w 787 ] 788 ] 789 50: 790 cases assm1 assm1 #assm1 normalize nodelta 791 cases assm1 #addr1 #addr2 normalize nodelta 792 [1: 793 @(subaddressing_mode_elim … addr2) try #w 794 2: 795 @(subaddressing_mode_elim … addr1) try #w 796 ] 797 ] 798 normalize repeat @le_S_S @le_O_n 799 ] 800 whd in match assembly1; normalize nodelta 801 [6: 802 normalize repeat @le_S_S @le_O_n 803 7: 804 @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n 805 *: 806 @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n 807 ] 808 *) 809 qed. 810 811 lemma assembly1_pseudoinstruction_lt_2_to_16: 812 ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi. 813 \snd (assembly_1_pseudoinstruction 814 lookup_labels sigma policy ppc lookup_datalabels pi) 815 < 2^16. 816 #lookup_labels #sigma #policy #ppc #lookup_datalabels * 817 [ cut (128 < 2^16) [@leb_true_to_le %] #LT 818 * whd in match (assembly_1_pseudoinstruction ??????); 819 whd in match (expand_pseudo_instruction ??????); 820 whd in match assembly_1_pseudoinstruction; normalize nodelta 821 try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1 822 whd in match (expand_pseudo_instruction ??????); 823 try 824 (change with (flatten ? [assembly1 ?] < ?) 825 >flatten_singleton 826 @(transitive_lt … (assembly1_lt_128 ?)) 827 @LT) 828 @pair_elim #x #y #_ cases x normalize nodelta 829 try 830 (change with (flatten ? [assembly1 ?] < ?) 831 >flatten_singleton 832 @(transitive_lt … (assembly1_lt_128 ?)) 833 @LT) 834 change with (flatten ? [assembly1 ?; assembly1 ?; assembly1 ?] < ?) 835 >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O 836 <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???)) 837 try @assembly1_lt_128 @leb_true_to_le % 838 2,3: #msg normalize in ⊢ (?%?); // 839  #label whd in match (assembly_1_pseudoinstruction ??????); 840 whd in match (expand_pseudo_instruction ??????); 841 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 842 [2: @pair_elim #x #y #_ cases (?∧?)] 843 normalize in ⊢ (?%?); // 844  #label whd in match (assembly_1_pseudoinstruction ??????); 845 whd in match (expand_pseudo_instruction ??????); 846 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 847 normalize in ⊢ (?%?); // 848  #dptr #id normalize in ⊢ (?%?); // 849 ] 850 qed. 851 852 733 853 734 854 definition assembly: 
src/ASM/AssemblyProof.ma
r2151 r2157 179 179  _ ⇒ True 180 180 ]. 181 182 (* XXX: easy but tedious *)183 lemma assembly1_lt_128:184 ∀i: instruction.185 (assembly1 i) < 128.186 cases daemon187 (* XXX: commented out as takes ages to type check188 #i cases i189 try (#assm1 #assm2) try #assm1190 [8:191 cases assm1192 try (#assm1 #assm2) try #assm1193 whd in match assembly1; normalize nodelta194 whd in match assembly_preinstruction; normalize nodelta195 try @(subaddressing_mode_elim … assm2)196 try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta197 [32:198 cases assm1 assm1 #assm1 normalize nodelta199 cases assm1 #addr1 #addr2 normalize nodelta200 [1:201 @(subaddressing_mode_elim … addr2)202 2:203 @(subaddressing_mode_elim … addr1)204 ]205 #w206 35,36,37:207 cases assm1 assm1 #assm1 normalize nodelta208 [1,3:209 cases assm1 assm1 #assm1 normalize nodelta210 ]211 cases assm1 #addr1 #addr2 normalize nodelta212 @(subaddressing_mode_elim … addr2) try #w213 49:214 cases assm1 assm1 #assm1 normalize nodelta215 [1:216 cases assm1 assm1 #assm1 normalize nodelta217 [1:218 cases assm1 assm1 #assm1 normalize nodelta219 [1:220 cases assm1 assm1 #assm1 normalize nodelta221 [1:222 cases assm1 assm1 #assm1 normalize nodelta223 ]224 ]225 ]226 ]227 cases assm1 #addr1 #addr2 normalize nodelta228 [1,3,4,5:229 @(subaddressing_mode_elim … addr2) try #w230 *:231 @(subaddressing_mode_elim … addr1) try #w232 normalize nodelta233 [1,2:234 @(subaddressing_mode_elim … addr2) try #w235 ]236 ]237 50:238 cases assm1 assm1 #assm1 normalize nodelta239 cases assm1 #addr1 #addr2 normalize nodelta240 [1:241 @(subaddressing_mode_elim … addr2) try #w242 2:243 @(subaddressing_mode_elim … addr1) try #w244 ]245 ]246 normalize repeat @le_S_S @le_O_n247 ]248 whd in match assembly1; normalize nodelta249 [6:250 normalize repeat @le_S_S @le_O_n251 7:252 @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n253 *:254 @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n255 ]256 *)257 qed.258 259 lemma assembly1_pseudoinstruction_lt_2_to_16:260 ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.261 \snd (assembly_1_pseudoinstruction262 lookup_labels sigma policy ppc lookup_datalabels pi)263 < 2^16.264 #lookup_labels #sigma #policy #ppc #lookup_datalabels *265 [ cut (128 < 2^16) [@leb_true_to_le %] #LT266 * whd in match (assembly_1_pseudoinstruction ??????);267 whd in match (expand_pseudo_instruction ??????);268 whd in match assembly_1_pseudoinstruction; normalize nodelta269 try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1270 whd in match (expand_pseudo_instruction ??????);271 try272 (change with (flatten ? [assembly1 ?] < ?)273 >flatten_singleton274 @(transitive_lt … (assembly1_lt_128 ?))275 @LT)276 @pair_elim #x #y #_ cases x normalize nodelta277 try278 (change with (flatten ? [assembly1 ?] < ?)279 >flatten_singleton280 @(transitive_lt … (assembly1_lt_128 ?))281 @LT)282 change with (flatten ? [assembly1 ?; assembly1 ?; assembly1 ?] < ?)283 >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O284 <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))285 try @assembly1_lt_128 @leb_true_to_le %286 2,3: #msg normalize in ⊢ (?%?); //287  #label whd in match (assembly_1_pseudoinstruction ??????);288 whd in match (expand_pseudo_instruction ??????);289 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_290 [2: @pair_elim #x #y #_ cases (?∧?)]291 normalize in ⊢ (?%?); //292  #label whd in match (assembly_1_pseudoinstruction ??????);293 whd in match (expand_pseudo_instruction ??????);294 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_295 normalize in ⊢ (?%?); //296  #dptr #id normalize in ⊢ (?%?); //297 ]298 qed.299 181 300 182 lemma monotone_sigma:
Note: See TracChangeset
for help on using the changeset viewer.