Changeset 1692
 Timestamp:
 Feb 14, 2012, 1:18:25 PM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1691 r1692 600 600 #start_status #final_status 601 601 #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost 602 #recursive_assm @(trace_any_label_inv_ind … the_trace) 602 #recursive_assm 603 @(trace_any_label_inv_ind … the_trace) 603 604 [5: 604 605 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label … … 742 743 #trace_ends_flag #the_trace #program_counter_refl #classify_assm 743 744 @(trace_any_label_inv_ind … the_trace) 744 [1: 745 #start_status' #final_status' #execute_assm #classifier_assm #costed_assm 745 [5: 746 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label 747 #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl 748 #the_trace_refl destruct @⊥ 749 1: 750 #status_start #status_final #execute_assm #classifier_assm #costed_assm 746 751 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 747 752 destruct 748 753 whd in match (trace_any_label_length … (tal_base_not_return …)); 749 whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); 750 whd in costed_assm; 751 generalize in match costed_assm; 752 generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … start_status')) cost_labels)); 753 generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' start_status')) cost_labels) 754 in ⊢ (??%? → (match % with [ _ ⇒ ?  _ ⇒ ? ]) → ?); 755 #lookup_assm cases lookup_assm 754 whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); % 756 755 [1: 757 #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm 758 #absurd cases absurd 756 %{(pred total_program_size)} whd in ⊢ (??%?); 757 @S_pred 758 @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) 759 759 2: 760 #costlabel #Some_lookup_opt_assm normalize nodelta #ignore % 761 [2: <FETCH % 762  cases daemon ] 760 <FETCH % 763 761 ] 764 762 2: 765 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_ flag_refl766 #start_status_refl #final_status_refl #the_trace_ refldestruct @⊥763 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm 764 #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ 767 765 3: 768 766 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 769 767 #classifier_assm #after_return_assm #trace_label_return #costed_assm 770 # trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl768 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 771 769 destruct @⊥ 772 770 4: 773 771 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 774 772 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 775 #costed_assm #trace_any_label_return #trace_ends_flag_refl #start_status_refl 776 #final_status_refl #the_trace_refl destruct @⊥ 777 5: 778 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label 779 #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl 773 #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl 780 774 #final_status_refl #the_trace_refl destruct @⊥ 781 775 ] … … 805 799 ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). 806 800 ∀classify_assm: ASM_classify0 instruction = cl_call. 807 ∀pi1 : ℕ.808 if match lookup_opt costlabel 16 program_counter'' cost_labels with809 [None ⇒ trueSome _ ⇒ false]801 (∀pi1:ℕ 802 .if match lookup_opt costlabel 16 program_counter'' cost_labels with 803 [None ⇒ true  Some _ ⇒ false] 810 804 then (∀start_status0:Status code_memory' 811 805 .∀final_status0:Status code_memory' … … 832 826 ∧ticks+pi1 833 827 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag 834 start_status final_status the_trace .828 start_status final_status the_trace). 835 829 #code_memory' #program_counter' #total_program_size #cost_labels 836 830 #reachable_program_counter_witness #good_program_witness #program_size' … … 839 833 #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm 840 834 @(trace_any_label_inv_ind … the_trace) 841 cases daemon 835 [5: 836 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label 837 #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl 838 #the_trace_refl destruct @⊥ 839 1: 840 #status_start #status_final #execute_assm #classifier_assm #costed_assm 841 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 842 destruct @⊥ 843 2: 844 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm 845 #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ 846 3: 847 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 848 #classifier_assm #after_return_assm #trace_label_return #costed_assm 849 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 850 destruct 851 whd in match (trace_any_label_length … (tal_base_call …)); 852 whd in match (compute_paid_trace_any_label … (tal_base_call …)); 853 whd in costed_assm; 854 generalize in match costed_assm; 855 generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels)); 856 generalize in match (lookup_opt … (program_counter … status_final) cost_labels) 857 in ⊢ (??%? → (match % with [ _ ⇒ ?  _ ⇒ ? ]) → ?); 858 #lookup_assm cases lookup_assm 859 [1: 860 #None_lookup_opt normalize nodelta #absurd cases absurd 861 2: 862 #costlabel #Some_lookup_opt normalize nodelta #ignore 863 generalize in match recursive_assm; 864 cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final)) 865 [1: 866 whd in after_return_assm; <after_return_assm; (* XXX: here *) 867 cases daemon 868 2: 869 #program_counter_assm >program_counter_assm <Some_lookup_opt 870 normalize nodelta #new_recursive_assm >new_recursive_assm % 871 [1: 872 %{(pred total_program_size)} whd in ⊢ (??%?); 873 @S_pred 874 @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) 875 2: 876 cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call))) 877 [1: 878 <FETCH % 879 2: 880 #ticks_refl_assm >ticks_refl_assm 881 <plus_n_O % 882 ] 883 ] 884 ] 885 ] 886 4: 887 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 888 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 889 #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl 890 #final_status_refl #the_trace_refl destruct 891 whd in match (trace_any_label_length … (tal_step_call …)); 892 whd in match (compute_paid_trace_any_label … (tal_step_call …)); 893 whd in costed_assm:(?%); 894 generalize in match costed_assm; 895 generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels)); 896 generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels) 897 in ⊢ (??%? → ?(match % with [ _ ⇒ ?  _ ⇒ ? ]) → ?); 898 #lookup_assm cases lookup_assm 899 [1: 900 #None_lookup_opt_assm normalize nodelta #ignore 901 generalize in match recursive_assm; 902 cut(program_counter'' = program_counter … status_after_fun_call) 903 [1: 904 cases daemon 905 2: 906 #program_counter_refl >program_counter_refl <None_lookup_opt_assm 907 normalize nodelta #new_recursive_assm % 908 cases (new_recursive_assm … trace_any_label ?) 909 [1,3: 910 #exists_assm #recursive_block_cost_assm 911 [2: 912 >recursive_block_cost_assm 913 @plus_right_monotone 914 whd in ⊢ (???%); <FETCH % 915 1: 916 (* 917 cases exists_assm #recursive_n #new_exists_assm 918 <new_exists_assm 919 920 % 921 [1: 922 @(recursive_n  current_instruction_cost … status_pre_fun_call) 923 2: 924 925 cut(current_instruction_cost … status_pre_fun_call = 926 (nat_of_bitvector 16 927 (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call) 928 nat_of_bitvector 16 929 (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call))) 930 [1: 931 2: 932 #eq_assm <eq_assm eq_assm new_exists_assm recursive_block_cost_assm 933 <plus_n_Sm <plus_n_Sm @eq_f 934 >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?); 935 >associative_plus @eq_f 936 <plus_minus_m_m [1: % ] 937 ] 938 ] *) 939 cases daemon 940 ] 941 2,4: 942 % 943 ] 944 ] 945 2: 946 #cost_label #Some_lookup_opt_assm normalize nodelta #absurd 947 cases absurd #absurd cases (absurd I) 948 ] 949 ] 950 try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) 951 try (change with (ASM_classify0 ? = ?) in classifier_assm;) 952 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 953 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 954 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd 955 #absurd destruct(absurd) 842 956 qed. 843 957 … … 924 1038 ]) 925 1039 ]. 1040 cases daemon (* 926 1041 [1: 927 1042 cases reachable_program_counter_witness #_ #hyp … … 1042 1157 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1043 1158 >(le_to_leb_true … program_counter_lt') % 1044 97,100:1045 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp1046 lapply(good_program_witness program_counter' reachable_program_counter_witness)1047 <FETCH normalize nodelta <instr normalize nodelta1048 try(<real_instruction_refl <instr normalize nodelta) *1049 #pc_pc_lt_hyp' #pc_tps_lt_hyp'1050 @(transitive_le1051 total_program_size1052 ((S program_size') + nat_of_bitvector … program_counter')1053 (program_size' + nat_of_bitvector … program_counter'') recursive_case)1054 normalize in match (S program_size' + nat_of_bitvector … program_counter');1055 >plus_n_Sm1056 @monotonic_le_plus_r1057 change with (1058 nat_of_bitvector … program_counter' <1059 nat_of_bitvector … program_counter'')1060 assumption1061 1159 6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91, 1062 1160 94: … … 1082 1180 reachable_program_counter_witness good_program_witness first_time_around ?) block_cost' 1083 1181 [1: 1084 @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … 1085 recursive_case … instruction program_counter' … FETCH) 1182 #recursive_block_cost #recursive_assm 1183 @(trace_any_label_inv_ind … the_trace) 1184 [1: 1185 #start_status' #final_status' #execute_assm #classifier_assm #costed_assm 1186 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1187 destruct @⊥ 1188 2: 1189 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl 1190 #start_status_refl #final_status_refl #the_trace_refl destruct 1191 whd in match (trace_any_label_length … (tal_base_return …)); 1192 whd in match (compute_paid_trace_any_label … (tal_base_return …)); % 1193 [1: 1194 %{(pred total_program_size)} whd in ⊢ (??%?); 1195 @S_pred 1196 @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) 1197 2: 1198 <FETCH % 1199 ] 1200 3: 1201 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 1202 #classifier_assm #after_return_assm #trace_label_return #costed_assm 1203 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1204 destruct @⊥ 1205 4: 1206 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 1207 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 1208 #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl 1209 #final_status_refl #the_trace_refl 1210 destruct @⊥ 1211 5: 1212 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label 1213 #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl 1214 #final_status_refl #the_trace_refl destruct @⊥ 1215 ] 1216 try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) 1217 try (change with (ASM_classify0 ? = ?) in classifier_assm;) 1218 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1219 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1220 <FETCH in classifier_assm; 1221 try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd)) 1222 whd in ⊢ (?(??%?)(??%?) → ?); #absurd 1223 cases absurd #absurd destruct(absurd) 1086 1224 2: 1225 cases daemon (* XXX: ??? *) 1087 1226 ] 1088 ] 1089 qed. 1090 1091 1092 1093 1227 62,63,64,65,66,67,68,69,70,101,102,103: 1228 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1229 cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels 1230 reachable_program_counter_witness good_program_witness first_time_around ?) block_cost' 1231 try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %) 1232 cases daemon (* XXX: ???, same as above case *) 1233 96,99: 1094 1234 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1095 1235 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1096 <FETCH normalize nodelta 1097 <real_instruction_refl <instr normalize nodelta * 1098 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 1236 <FETCH normalize nodelta <instr normalize nodelta * 1237 #program_counter_lt' #program_counter_lt_tps' % 1238 [1,3: 1239 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1240 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1241 >(le_to_leb_true … program_counter_lt') % 1242 2,4: 1243 assumption 1244 ] 1245 98,104,107: 1246 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1247 cases(block_cost' ?????????) block_cost' 1248 @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …) 1249 destruct % 1250 105: 1251 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1252 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1253 <FETCH normalize nodelta <instr normalize nodelta 1254 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1255 * * * * #n' 1256 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1257 % 1258 [1: 1259 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1260 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1261 >(le_to_leb_true … program_counter_lt') % 1262 2: 1263 assumption 1264 ] 1265 106: 1266 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1267 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1268 <FETCH normalize nodelta <instr normalize nodelta 1269 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1270 * * * * #n' 1271 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1099 1272 @(transitive_le 1100 1273 total_program_size … … 1108 1281 nat_of_bitvector … program_counter'') 1109 1282 assumption 1110 4: 1111 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1112 cases(block_cost' ??? ? ?????) block_cost' 1113 #recursive_block_cost #recursive_assm 1114 @(trace_any_label_inv_ind … the_trace) 1115 [1: 1116 #status_start #status_final #execute_assm #classifier_assm #costed_assm 1117 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1118 destruct 1119 whd in match (trace_any_label_length … (tal_base_not_return …)); 1120 whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); 1121 whd in costed_assm; 1122 2: 1123 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm 1124 #start_status_refl #final_status_refl #the_trace_assm destruct 1125 whd in classifier_assm; 1126 whd in classifier_assm:(??%?); 1127 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1128 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1129 @⊥ <FETCH in classifier_assm; normalize nodelta 1130 #absurd destruct(absurd) 1131 3: 1132 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 1133 #classifier_assm #after_return_assm #trace_label_return #costed_assm 1134 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1135 destruct 1136 whd in classifier_assm; 1137 whd in classifier_assm:(??%?); 1138 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1139 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1140 @⊥ <FETCH in classifier_assm; normalize nodelta 1141 #absurd destruct(absurd) 1142 4: 1143 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 1144 #status_final #execute_assm #classifier_assm #after_return_assm 1145 #trace_label_return #costed_assm #trace_any_label #ends_flag_refl 1146 #start_status_refl #final_status_refl #the_trace_refl 1147 destruct 1148 whd in classifier_assm; 1149 whd in classifier_assm:(??%?); 1150 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1151 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1152 @⊥ <FETCH in classifier_assm; normalize nodelta 1153 #absurd destruct(absurd) 1154 ] 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 3: 1185 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 1186 #classifier_assm #after_return_assm #trace_label_return #costed_assm 1187 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1188 destruct 1189 whd in match (compute_paid_trace_any_label … (tal_base_call …)); 1190 whd in match (trace_any_label_length … (tal_base_call …)); 1191 cases(recursive_assm … 1192 (tal_base_call (ASM_abstract_status code_memory' cost_labels) 1193 status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …) 1194 classifier_assm after_return_assm trace_label_return costed_assm) ?) 1195 [1: 1196 * #recursive_n #recursive_trace_total #recursive_block_cost_assm % 1197 [1: 1198 %{(pred total_program_size)} 1199 whd in ⊢ (??%?); 1200 >S_pred [1: % ] 1201 <recursive_trace_total 1202 @lt_O_S 1203 2: 1204 >recursive_block_cost_assm 1205 whd in ⊢ (??(??%)?); <FETCH 1206 (* XXX: ??? *) 1207 ] 1208 2: 1209 cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call)))) 1210 [1: 1211 cases FETCH % 1212 2: 1213 #program_counter_hyp'' >program_counter_hyp'' 1214 whd in after_return_assm; <after_return_assm 1215 whd in match (current_instruction_cost status_pre_fun_call); 1216 @fetch_half_add 1217 ] 1218 ] 1219 4: 1220 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 1221 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 1222 #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl 1223 #final_status_refl #the_trace_refl 1224 generalize in match execute_assm; destruct #execute_assm 1225 whd in match (compute_paid_trace_any_label … (tal_step_call …)); 1226 whd in match (trace_any_label_length … (tal_step_call …)); 1227 cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?) 1228 [1: 1229 * #recursive_n #recursive_trace_total #recursive_block_cost_assm % 1230 [1: 1231 <recursive_trace_total % 1232 [1: 1233 @(recursive_n  (current_instruction_cost status_pre_fun_call)) 1234 2: 1235 whd in after_return_assm; cases after_return_assm 1236 >half_add_minus_right in ⊢ (??%?); 1237 >commutative_plus in ⊢ (???%); 1238 >commutative_plus in ⊢ (??%?); 1239 <associative_plus in ⊢ (??%?); 1240 @plus_right_monotone 1241 cut(current_instruction_cost status_pre_fun_call ≤ recursive_n) 1242 [1: 1243 (* XXX: ??? *) 1244 2: 1245 #current_instruction_cost_assm 1246 <minus_Sn_m in ⊢ (??%?); [2: assumption ] 1247 >minus_plus_cancel [1: % ] 1248 @le_S assumption 1249 ] 1250 ] 1251 2: 1252 >recursive_block_cost_assm 1253 @plus_right_monotone 1254 whd in match (current_instruction_cost status_pre_fun_call); 1255 <FETCH % 1256 ] 1257 1258 2: 1259 lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call) 1260 #hyp cases (hyp trace_label_return) 1261 @as_execute_preserves_code_memory whd % 1262 3: 1263 cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call)))) 1264 [1: 1265 cases FETCH % 1266 2: 1267 #program_counter_hyp'' >program_counter_hyp'' 1268 whd in after_return_assm; <after_return_assm 1269 whd in match (current_instruction_cost status_pre_fun_call); 1270 @fetch_half_add 1271 ] 1272 ] 1273 5: 1274 #end_flag #status_pre #status_init #status_end #execute_assm #the_trace' 1275 #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl 1276 #final_status_refl #trace_refl 1277 generalize in match the_trace; destruct #the_trace 1278 whd in classifier_assm; 1279 whd in classifier_assm:(??%?); 1280 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1281 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1282 @⊥ <FETCH in classifier_assm; normalize nodelta 1283 #absurd destruct(absurd) 1284 ] 1285 7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61, 1286 64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107: 1287 cases daemon (* XXX: massive terms *) 1288 2: 1289 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1290 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1291 <FETCH normalize nodelta <instr normalize nodelta 1292 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1293 cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta 1294 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1295 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1296 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1297 @(transitive_le 1298 total_program_size 1299 ((S program_size') + nat_of_bitvector … program_counter') 1300 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 1301 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 1302 >plus_n_Sm 1303 @monotonic_le_plus_r 1304 change with ( 1305 nat_of_bitvector … program_counter' < 1306 nat_of_bitvector … program_counter'') 1307 assumption 1308 3: 1283 108: 1309 1284 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1310 1285 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 1323 1298 assumption 1324 1299 ] 1325  5:1300 109: 1326 1301 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1327 1302 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1328 <FETCH normalize nodelta <instr normalize nodelta 1329 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1330 * * * * #n' 1331 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1303 <FETCH normalize nodelta <instr normalize nodelta 1304 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1305 cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta 1306 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1307 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1308 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1332 1309 @(transitive_le 1333 1310 total_program_size … … 1341 1318 nat_of_bitvector … program_counter'') 1342 1319 assumption 1343 6: 1344 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1345 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1346 <FETCH normalize nodelta <instr normalize nodelta 1347 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1348 * * * * #n' 1349 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1350 % 1351 [1: 1352 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1353 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1354 >(le_to_leb_true … program_counter_lt') % 1355 2: 1356 assumption 1357 ] 1358 11,14: (* JMP and MOVC *) 1320 97,100: 1359 1321 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1360 1322 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 1373 1335 nat_of_bitvector … program_counter'') 1374 1336 assumption 1375 12,15: 1376 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1377 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1378 <FETCH normalize nodelta <instr normalize nodelta * 1379 #program_counter_lt' #program_counter_lt_tps' % 1380 [1,3: 1381 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1382 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1383 >(le_to_leb_true … program_counter_lt') % 1384 2,4: 1385 assumption 1386 ] 1387 17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98, 1388 102,105: 1389 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1390 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1391 <FETCH normalize nodelta 1392 <real_instruction_refl <instr normalize nodelta * 1393 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 1394 @(transitive_le 1395 total_program_size 1396 ((S program_size') + nat_of_bitvector … program_counter') 1397 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 1398 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 1399 >plus_n_Sm 1400 @monotonic_le_plus_r 1401 change with ( 1402 nat_of_bitvector … program_counter' < 1403 nat_of_bitvector … program_counter'') 1404 assumption 1405 18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78, 1406 81,84,87,90,93,96,99,103,106: 1407 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1408 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1409 <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * 1410 #program_counter_lt' #program_counter_lt_tps' % 1411 try assumption 1412 [*: 1413 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1414 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1415 >(le_to_leb_true … program_counter_lt') % 1416 ] 1417 [1: 1418 #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl 1419 cases(block_cost' ?????? ?? ?) block_cost' 1420 #recursive_block_cost #recursive_assm 1421 @(trace_any_label_inv_ind … the_trace) 1422 [1: 1423 #start_status' #final_status' #execute_assm #classifier_assm #costed_assm 1424 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct 1425 cases classifier_assm 1426 whd in match (as_classifier ? ? ?); 1427 whd in ⊢ (??%? → ?); 1428 whd in match current_instruction; normalize nodelta 1429 whd in match current_instruction0; normalize nodelta 1430 #absurd @⊥ >p1 in absurd; normalize nodelta 1431 #absurd destruct(absurd) 1432 2: 1433 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm 1434 #start_status_refl #final_status_refl #the_trace_assm destruct 1435 whd in classifier_assm; 1436 whd in classifier_assm:(??%?); 1437 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1438 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1439 @⊥ 1440 >p1 in classifier_assm; normalize nodelta 1441 #absurd destruct(absurd) 1442 3: 1443 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 1444 #classifier_assm #after_return_assm #trace_label_return #costed_assm 1445 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 1446 destruct 1447 cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret 1448 (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call 1449 (execute_1 status_pre_fun_call) status_final 1450 (refl Status (execute_1 status_pre_fun_call)) classifier_assm 1451 after_return_assm trace_label_return costed_assm) ? ?) 1452 [2: % 1453 3: 1454 1: 1455 ] 1456 4: 1457 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 1458 #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return 1459 #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl 1460 #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label)); 1461 5: 1462 #end_flag #status_pre #status_init #status_end #execute_assm #the_trace 1463 #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl 1464 #the_trace_refl the_trace_refl destruct 1465 whd in classifier_assm; 1466 whd in classifier_assm:(??%?); 1467 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 1468 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 1469 @⊥ >p1 in classifier_assm; normalize nodelta 1470 #absurd destruct(absurd) 1471 ] 1472 [1: 1473 #start_status #final_status #trace_ends_flag #the_trace 1474 #code_memory_refl #program_counter_refl 1475 cases(block_cost' ?????? ?? ?) block_cost' 1476 #recursive_block_cost #recursive_assm 1477 @(trace_any_label_inv_ind … the_trace) 1478 [1: 1479 #start_status' #final_status' #execute_assm #not_return_assm 1480 #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm 1481 #the_trace_assm 1482 cases daemon (* XXX: bug in notion of traces here *) 1483 2: 1484 1485 3: 1486 cases daemon (* XXX *) 1487 4: 1488 ] 1489 108: 1490 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1491 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1492 <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * 1493 #program_counter_lt' #program_counter_lt_tps' % 1494 try assumption 1495 [*: 1496 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1497 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1498 >(le_to_leb_true … program_counter_lt') % 1499 ] 1500 [1: 1501 cases reachable_program_counter_witness #_ #hyp 1502 @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) 1503 @(le_to_lt_to_lt … base_case hyp) 1504 2: 1505 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1506 lapply(good_program_witness program_counter reachable_program_counter_witness) 1507 <FETCH normalize nodelta <instr normalize nodelta 1508 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1509 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 1510 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1511 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1512 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1513 @(transitive_le 1514 total_program_size 1515 ((S program_size') + nat_of_bitvector … program_counter) 1516 (program_size' + nat_of_bitvector … program_counter') recursive_case) 1517 normalize in match (S program_size' + nat_of_bitvector … program_counter); 1518 >plus_n_Sm 1519 @monotonic_le_plus_r 1520 change with ( 1521 nat_of_bitvector … program_counter < 1522 nat_of_bitvector … program_counter') 1523 assumption 1524 3: 1525 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1526 lapply(good_program_witness program_counter reachable_program_counter_witness) 1527 <FETCH normalize nodelta <instr normalize nodelta 1528 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1529 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 1530 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1531 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1532 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1533 % 1534 [1: 1535 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1536 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1537 >(le_to_leb_true … program_counter_lt') % 1538 2: 1539 assumption 1540 ] 1541 4: 1542 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1543 lapply(good_program_witness program_counter reachable_program_counter_witness) 1544 <FETCH normalize nodelta <instr normalize nodelta 1545 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1546 * * * * #n' 1547 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1548 @(transitive_le 1549 total_program_size 1550 ((S program_size') + nat_of_bitvector … program_counter) 1551 (program_size' + nat_of_bitvector … program_counter') recursive_case) 1552 normalize in match (S program_size' + nat_of_bitvector … program_counter); 1553 >plus_n_Sm 1554 @monotonic_le_plus_r 1555 change with ( 1556 nat_of_bitvector … program_counter < 1557 nat_of_bitvector … program_counter') 1558 assumption 1559 5: 1560 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1561 lapply(good_program_witness program_counter reachable_program_counter_witness) 1562 <FETCH normalize nodelta <instr normalize nodelta 1563 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1564 * * * * #n' 1565 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1566 % 1567 [1: 1568 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1569 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1570 >(le_to_leb_true … program_counter_lt') % 1571 2: 1572 assumption 1573 ] 1574 6,8: (* JMP and MOVC *) 1575 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1576 lapply(good_program_witness program_counter reachable_program_counter_witness) 1577 <FETCH normalize nodelta <instr normalize nodelta 1578 try(<real_instruction_refl <instr normalize nodelta) * 1579 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 1580 @(transitive_le 1581 total_program_size 1582 ((S program_size') + nat_of_bitvector … program_counter) 1583 (program_size' + nat_of_bitvector … program_counter') recursive_case) 1584 normalize in match (S program_size' + nat_of_bitvector … program_counter); 1585 >plus_n_Sm 1586 @monotonic_le_plus_r 1587 change with ( 1588 nat_of_bitvector … program_counter < 1589 nat_of_bitvector … program_counter') 1590 assumption 1591 7,9: 1592 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1593 lapply(good_program_witness program_counter reachable_program_counter_witness) 1594 <FETCH normalize nodelta <instr normalize nodelta * 1595 #program_counter_lt' #program_counter_lt_tps' % 1596 [1,3: 1597 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1598 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1599 >(le_to_leb_true … program_counter_lt') % 1600 2,4: 1601 assumption 1602 ] 1603 11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53, 1604 55,57,59,61,63: 1605 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1606 lapply(good_program_witness program_counter reachable_program_counter_witness) 1607 <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * 1608 #program_counter_lt' #program_counter_lt_tps' % 1609 try assumption 1610 [*: 1611 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1612 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1613 >(le_to_leb_true … program_counter_lt') % 1614 ] 1615 10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52, 1616 54,56,58,60,62: 1617 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1618 lapply(good_program_witness program_counter reachable_program_counter_witness) 1619 <FETCH normalize nodelta 1620 <real_instruction_refl <instr normalize nodelta * 1621 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 1622 @(transitive_le 1623 total_program_size 1624 ((S program_size') + nat_of_bitvector … program_counter) 1625 (program_size' + nat_of_bitvector … program_counter') recursive_case) 1626 normalize in match (S program_size' + nat_of_bitvector … program_counter); 1627 >plus_n_Sm 1628 @monotonic_le_plus_r 1629 change with ( 1630 nat_of_bitvector … program_counter < 1631 nat_of_bitvector … program_counter') 1632 assumption 1633 ] 1337 ] *) 1634 1338 qed. 1635 1339 
src/ASM/CostsProof.ma
r1658 r1692 13 13 14 14 definition current_instruction ≝ 15 λs: Status. 16 current_instruction0 (code_memory … s) (program_counter … s). 15 λcm. 16 λs: Status cm. 17 current_instruction0 cm (program_counter … s). 17 18 18 19 definition ASM_classify0: instruction → status_class ≝ … … 42 43 ]. 43 44 44 definition ASM_classify: Status → status_class ≝ 45 λs: Status. 46 ASM_classify0 (current_instruction s). 45 definition ASM_classify: ∀cm. Status cm → status_class ≝ 46 λcm. 47 λs: Status cm. 48 ASM_classify0 (current_instruction cm s). 47 49 48 50 definition current_instruction_is_labelled ≝ 51 λcm. 49 52 λcost_labels: BitVectorTrie costlabel 16. 50 λs: Status .51 let pc ≝ program_counter …s in53 λs: Status cm. 54 let pc ≝ program_counter ? cm s in 52 55 match lookup_opt … pc cost_labels with 53 56 [ None ⇒ False … … 56 59 57 60 definition next_instruction_properly_relates_program_counters ≝ 58 λbefore: Status. 59 λafter : Status. 60 let size ≝ current_instruction_cost before in 61 let pc_before ≝ program_counter … before in 62 let pc_after ≝ program_counter … after in 61 λcm. 62 λbefore: Status cm. 63 λafter : Status cm. 64 let size ≝ current_instruction_cost cm before in 65 let pc_before ≝ program_counter … cm before in 66 let pc_after ≝ program_counter … cm after in 63 67 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 64 68 sum = pc_after. 65 69 66 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ 67 λcost_labels. 70 definition ASM_abstract_status: ∀cm. BitVectorTrie costlabel 16 → abstract_status ≝ 71 λcm. 72 λcost_labels. 68 73 mk_abstract_status 69 Status70 (λs,s'. (execute_1 s) = s')71 (λs,class. ASM_classify s = class)72 (current_instruction_is_labelled c ost_labels)73 next_instruction_properly_relates_program_counters.74 (Status cm) 75 (λs,s'. (execute_1 cm s) = s') 76 (λs,class. ASM_classify cm s = class) 77 (current_instruction_is_labelled cm cost_labels) 78 (next_instruction_properly_relates_program_counters cm). 74 79 75 80 let rec compute_max_trace_label_label_cost 81 (cm: ?) 76 82 (cost_labels: BitVectorTrie costlabel 16) 77 83 (trace_ends_flag: trace_ends_with_ret) 78 (start_status: Status ) (final_status: Status)79 (the_trace: trace_label_label (ASM_abstract_status c ost_labels) trace_ends_flag84 (start_status: Status cm) (final_status: Status cm) 85 (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag 80 86 start_status final_status) on the_trace: nat ≝ 81 87 match the_trace with … … 84 90 ] 85 91 and compute_max_trace_any_label_cost 92 (cm: ?) 86 93 (cost_labels: BitVectorTrie costlabel 16) 87 94 (trace_ends_flag: trace_ends_with_ret) 88 (start_status: Status ) (final_status: Status)89 (the_trace: trace_any_label (ASM_abstract_status c ost_labels) trace_ends_flag start_status final_status)95 (start_status: Status cm) (final_status: Status cm) 96 (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status) 90 97 on the_trace: nat ≝ 91 98 match the_trace with 92 99 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status 93 100  tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status 101  tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 102 let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in 103 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 104 call_trace_cost + current_instruction_cost 94 105  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 95 _ _ _ call_trace final_trace ⇒96 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in106 _ _ _ call_trace _ final_trace ⇒ 107 let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in 97 108 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 98 109 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in 99 110 call_trace_cost + current_instruction_cost + final_trace_cost 100 111  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 101 let current_instruction_cost ≝ current_instruction_cost status_pre in112 let current_instruction_cost ≝ current_instruction_cost cm status_pre in 102 113 let tail_trace_cost ≝ 103 114 compute_max_trace_any_label_cost cost_labels end_flag … … 107 118 ] 108 119 and compute_max_trace_label_return_cost 109 (cost_labels: BitVectorTrie costlabel 16) 110 (start_status: Status) (final_status: Status) 111 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 120 (cm: ?) 121 (cost_labels: BitVectorTrie costlabel 16) 122 (start_status: Status cm) (final_status: Status cm) 123 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) 112 124 on the_trace: nat ≝ 113 125 match the_trace with … … 575 587 qed. 576 588 577 578 589 let rec block_cost_trace_any_label_static_dynamic_ok 579 590 (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
Note: See TracChangeset
for help on using the changeset viewer.