Changeset 1693
- Timestamp:
- Feb 14, 2012, 4:38:06 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1692 r1693 1338 1338 qed. 1339 1339 1340 definition block_cost ≝ 1340 (* 1341 (code_memory': BitVectorTrie Byte 16) (program_counter': Word) 1342 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 1343 (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter') 1344 (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool) 1345 on program_size: 1346 total_program_size ≤ program_size + nat_of_bitvector … program_counter' → 1347 Σcost_of_block: nat. 1348 if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then 1349 ∀start_status: Status code_memory'. 1350 ∀final_status: Status code_memory'. 1351 ∀trace_ends_flag. 1352 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 1353 program_counter' = program_counter … start_status → 1354 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 1355 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace 1356 else 1357 (cost_of_block = 0) 1358 *) 1359 1360 definition block_cost: 1361 ∀code_memory': BitVectorTrie Byte 16. 1362 ∀program_counter': Word. 1363 ∀total_program_size: nat. 1364 ∀cost_labels: BitVectorTrie costlabel 16. 1365 ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. 1366 ∀good_program_witness: good_program code_memory' total_program_size. 1367 Σcost_of_block: nat. 1368 ∀start_status: Status code_memory'. 1369 ∀final_status: Status code_memory'. 1370 ∀trace_ends_flag. 1371 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 1372 program_counter' = program_counter … start_status → 1373 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 1374 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝ 1341 1375 λcode_memory: BitVectorTrie Byte 16. 1342 1376 λprogram_counter: Word. … … 1344 1378 λcost_labels: BitVectorTrie costlabel 16. 1345 1379 λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. 1346 λgood_program_witness: good_program code_memory total_program_size. 1347 block_cost' code_memory program_counter total_program_size total_program_size cost_labels 1348 reachable_program_counter_witness good_program_witness true ?. 1349 @le_plus_n_r 1380 λgood_program_witness: good_program code_memory total_program_size. ?. 1381 cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels 1382 reachable_program_counter_witness good_program_witness true ?) 1383 [1: 1384 #cost_of_block #block_cost_hyp 1385 %{cost_of_block} 1386 cases(lookup_opt … cost_labels) in block_cost_hyp; 1387 [2: #cost_label] normalize nodelta 1388 #hyp assumption 1389 |2: 1390 @le_plus_n_r 1391 ] 1350 1392 qed. 1351 1393 -
src/ASM/CostsProof.ma
r1692 r1693 7 7 include alias "basics/logic.ma". 8 8 9 definition current_instruction0 ≝10 λcode_memory: BitVectorTrie Byte 16.11 λprogram_counter: Word.12 \fst (\fst (fetch … code_memory program_counter)).13 14 definition current_instruction ≝15 λcm.16 λs: Status cm.17 current_instruction0 cm (program_counter … s).18 19 definition ASM_classify0: instruction → status_class ≝20 λi: instruction.21 match i with22 [ RealInstruction pre ⇒23 match pre with24 [ RET ⇒ cl_return25 | JZ _ ⇒ cl_jump26 | JNZ _ ⇒ cl_jump27 | JC _ ⇒ cl_jump28 | JNC _ ⇒ cl_jump29 | JB _ _ ⇒ cl_jump30 | JNB _ _ ⇒ cl_jump31 | JBC _ _ ⇒ cl_jump32 | CJNE _ _ ⇒ cl_jump33 | DJNZ _ _ ⇒ cl_jump34 | _ ⇒ cl_other35 ]36 | ACALL _ ⇒ cl_call37 | LCALL _ ⇒ cl_call38 | JMP _ ⇒ cl_call39 | AJMP _ ⇒ cl_jump40 | LJMP _ ⇒ cl_jump41 | SJMP _ ⇒ cl_jump42 | _ ⇒ cl_other43 ].44 45 definition ASM_classify: ∀cm. Status cm → status_class ≝46 λcm.47 λs: Status cm.48 ASM_classify0 (current_instruction cm s).49 50 definition current_instruction_is_labelled ≝51 λcm.52 λcost_labels: BitVectorTrie costlabel 16.53 λs: Status cm.54 let pc ≝ program_counter ? cm s in55 match lookup_opt … pc cost_labels with56 [ None ⇒ False57 | _ ⇒ True58 ].59 60 definition next_instruction_properly_relates_program_counters ≝61 λcm.62 λbefore: Status cm.63 λafter : Status cm.64 let size ≝ current_instruction_cost cm before in65 let pc_before ≝ program_counter … cm before in66 let pc_after ≝ program_counter … cm after in67 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in68 sum = pc_after.69 70 definition ASM_abstract_status: ∀cm. BitVectorTrie costlabel 16 → abstract_status ≝71 λcm.72 λcost_labels.73 mk_abstract_status74 (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).79 80 9 let rec compute_max_trace_label_label_cost 81 10 (cm: ?) … … 97 26 on the_trace: nat ≝ 98 27 match the_trace with 99 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status100 | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status28 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost cm the_status 29 | tal_base_return the_status _ _ _ ⇒ current_instruction_cost cm the_status 101 30 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 102 31 let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in … … 107 36 let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in 108 37 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 109 let final_trace_cost ≝ compute_max_trace_any_label_cost c ost_labels end_flag … final_trace in38 let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in 110 39 call_trace_cost + current_instruction_cost + final_trace_cost 111 40 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 112 41 let current_instruction_cost ≝ current_instruction_cost cm status_pre in 113 42 let tail_trace_cost ≝ 114 compute_max_trace_any_label_cost c ost_labels end_flag43 compute_max_trace_any_label_cost cm cost_labels end_flag 115 44 status_init status_end tail_trace 116 45 in … … 134 63 135 64 let rec compute_max_trace_label_label_cost_is_ok 65 (cm: ?) 136 66 (cost_labels: BitVectorTrie costlabel 16) 137 67 (trace_ends_flag: trace_ends_with_ret) 138 (start_status: Status ) (final_status: Status)139 (the_trace: trace_label_label (ASM_abstract_status c ost_labels) trace_ends_flag68 (start_status: Status cm) (final_status: Status cm) 69 (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag 140 70 start_status final_status) on the_trace: 141 clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock… start_status) ≝ ?71 clock … cm … final_status = (compute_max_trace_label_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ? 142 72 and compute_max_trace_any_label_cost_is_ok 73 (cm: ?) 143 74 (cost_labels: BitVectorTrie costlabel 16) 144 75 (trace_ends_flag: trace_ends_with_ret) 145 (start_status: Status ) (final_status: Status)146 (the_trace: trace_any_label (ASM_abstract_status c ost_labels) trace_ends_flag start_status final_status)76 (start_status: Status cm) (final_status: Status cm) 77 (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status) 147 78 on the_trace: 148 clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock… start_status) ≝ ?79 clock … cm … final_status = (compute_max_trace_any_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ? 149 80 and compute_max_trace_label_return_cost_is_ok 150 (cost_labels: BitVectorTrie costlabel 16) 151 (start_status: Status) (final_status: Status) 152 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 81 (cm: ?) 82 (cost_labels: BitVectorTrie costlabel 16) 83 (start_status: Status cm) (final_status: Status cm) 84 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) 153 85 on the_trace: 154 clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock… start_status ≝ ?.86 clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?. 155 87 [1: 156 88 cases the_trace … … 161 93 [1,2: 162 94 #start_status #final_status #is_next #is_not_return try (#is_costed) 163 change with (current_instruction_cost start_status) in ⊢ (???(?%?));95 change with (current_instruction_cost cm start_status) in ⊢ (???(?%?)); 164 96 cases(is_next) @execute_1_ok 165 97 |3: 98 #status_pre_fun_call #status_start_fun_call #status_final #is_next 99 #classifier_assm #after_return_assm #call_trace #costed_assm 100 whd in match (compute_max_trace_any_label_cost … (tal_base_call …)); 101 >(compute_max_trace_label_return_cost_is_ok … call_trace) 102 >associative_plus @eq_f cases(is_next) 103 >execute_1_ok % 104 |4: 166 105 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 167 #status_final #is_next #is_call #is_after_return #call_trace # final_trace106 #status_final #is_next #is_call #is_after_return #call_trace #not_costed #final_trace 168 107 change with ( 169 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in170 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in171 let final_trace_cost ≝ compute_max_trace_any_label_cost c ost_labels end_flag … final_trace in108 let current_instruction_cost ≝ current_instruction_cost cm status_pre_fun_call in 109 let call_trace_cost ≝ compute_max_trace_label_return_cost cm … call_trace in 110 let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in 172 111 call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?)); 173 112 normalize nodelta; 174 >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call113 >(compute_max_trace_any_label_cost_is_ok … cost_labels end_flag status_after_fun_call 175 114 status_final final_trace) 176 >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call115 >(compute_max_trace_label_return_cost_is_ok … cost_labels status_start_fun_call 177 116 status_after_fun_call call_trace) 178 cases(is_next) in match (clock … status_start_fun_call);179 >(execute_1_ok status_pre_fun_call)117 cases(is_next) in match (clock … cm status_start_fun_call); 118 >(execute_1_ok … status_pre_fun_call) 180 119 <associative_plus in ⊢ (??%?); 181 120 <commutative_plus in match ( 182 compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace 183 + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace); 184 >associative_plus in ⊢ (??%?); 185 <commutative_plus in match ( 186 compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace 187 + (current_instruction_cost status_pre_fun_call 188 + clock (BitVectorTrie Byte 16) status_pre_fun_call)); 189 >associative_plus in ⊢ (??%?); 190 <commutative_plus in match ( 191 clock (BitVectorTrie Byte 16) status_pre_fun_call 192 + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace); 193 <(associative_plus ( 194 (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace))) 195 <associative_plus in ⊢ (??%?); % 196 |4: 121 compute_max_trace_any_label_cost cm cost_labels end_flag status_after_fun_call status_final final_trace 122 + compute_max_trace_label_return_cost cm cost_labels status_start_fun_call status_after_fun_call call_trace); 123 >associative_plus in ⊢ (??%?); >associative_plus in ⊢ (???%); >associative_plus in ⊢ (???%); 124 @eq_f >commutative_plus in ⊢ (??%?); >associative_plus in ⊢ (??%?); 125 @eq_f @commutative_plus 126 |5: 197 127 #end_flag #status_pre #status_init #status_end #is_next 198 128 #trace_any_label #is_other #is_not_costed 199 129 change with ( 200 let current_instruction_cost ≝ current_instruction_cost status_pre in130 let current_instruction_cost ≝ current_instruction_cost cm status_pre in 201 131 let tail_trace_cost ≝ 202 compute_max_trace_any_label_cost c ost_labels end_flag132 compute_max_trace_any_label_cost cm cost_labels end_flag 203 133 status_init status_end trace_any_label 204 134 in 205 135 current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?)); 206 136 normalize nodelta; 207 >(compute_max_trace_any_label_cost_is_ok c ost_labels end_flag137 >(compute_max_trace_any_label_cost_is_ok cm cost_labels end_flag 208 138 status_init status_end trace_any_label) 209 cases(is_next) in match (clock … status_init);210 >(execute_1_ok status_pre)139 cases(is_next) in match (clock … cm status_init); 140 >(execute_1_ok cm status_pre) 211 141 >commutative_plus >associative_plus >associative_plus @eq_f 212 142 @commutative_plus … … 220 150 #status_initial #status_labelled #status_final #labelled_trace #ret_trace 221 151 normalize 222 >(compute_max_trace_label_return_cost_is_ok c ost_labels status_labelled status_final ret_trace);223 >(compute_max_trace_label_label_cost_is_ok c ost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);152 >(compute_max_trace_label_return_cost_is_ok cm cost_labels status_labelled status_final ret_trace); 153 >(compute_max_trace_label_label_cost_is_ok cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace); 224 154 <associative_plus in ⊢ (??%?); 225 155 >commutative_plus in match ( 226 compute_max_trace_label_return_cost c ost_labels status_labelled status_final ret_trace227 + compute_max_trace_label_label_cost c ost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);156 compute_max_trace_label_return_cost cm cost_labels status_labelled status_final ret_trace 157 + compute_max_trace_label_label_cost cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace); 228 158 % 229 159 ] 230 ]. 231 qed. 232 233 (* XXX: work below here: *) 234 235 let rec compute_paid_trace_any_label 160 ] 161 qed. 162 163 let rec compute_trace_label_label_cost_using_paid 164 (cm: ?) 165 (cost_labels: BitVectorTrie costlabel 16) 166 (trace_ends_flag: trace_ends_with_ret) 167 (start_status: Status cm) (final_status: Status cm) 168 (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag 169 start_status final_status) on the_trace: nat ≝ 170 match the_trace with 171 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 172 compute_paid_trace_label_label cm cost_labels … the_trace + 173 compute_trace_any_label_cost_using_paid … given_trace 174 ] 175 and compute_trace_any_label_cost_using_paid 176 (cm: ?) 236 177 (cost_labels: BitVectorTrie costlabel 16) 237 178 (trace_ends_flag: trace_ends_with_ret) 238 (start_status: Status) (final_status: Status) 239 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 240 on the_trace: nat ≝ 241 match the_trace with 242 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status 243 | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status 244 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 245 _ _ _ call_trace final_trace ⇒ 246 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in 247 let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in 248 current_instruction_cost + final_trace_cost 249 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 250 let current_instruction_cost ≝ current_instruction_cost status_pre in 251 let tail_trace_cost ≝ 252 compute_paid_trace_any_label cost_labels end_flag 253 status_init status_end tail_trace 254 in 255 current_instruction_cost + tail_trace_cost 256 ]. 257 258 definition compute_paid_trace_label_label ≝ 259 λcost_labels: BitVectorTrie costlabel 16. 260 λtrace_ends_flag: trace_ends_with_ret. 261 λstart_status: Status. 262 λfinal_status: Status. 263 λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 264 start_status final_status. 265 match the_trace with 266 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 267 compute_paid_trace_any_label … given_trace 268 ]. 269 270 let rec compute_trace_label_label_cost_using_paid 271 (cost_labels: BitVectorTrie costlabel 16) 272 (trace_ends_flag: trace_ends_with_ret) 273 (start_status: Status) (final_status: Status) 274 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 275 start_status final_status) on the_trace: nat ≝ 276 match the_trace with 277 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 278 compute_paid_trace_label_label cost_labels … the_trace + 279 compute_trace_any_label_cost_using_paid … given_trace 280 ] 281 and compute_trace_any_label_cost_using_paid 282 (cost_labels: BitVectorTrie costlabel 16) 283 (trace_ends_flag: trace_ends_with_ret) 284 (start_status: Status) (final_status: Status) 285 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 179 (start_status: Status cm) (final_status: Status cm) 180 (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status) 286 181 on the_trace: nat ≝ 287 182 match the_trace with 288 183 [ tal_base_not_return the_status _ _ _ _ ⇒ 0 289 184 | tal_base_return the_status _ _ _ ⇒ 0 185 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 186 compute_trace_label_return_cost_using_paid … call_trace 290 187 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 291 _ _ _ call_trace final_trace ⇒188 _ _ _ call_trace _ final_trace ⇒ 292 189 let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in 293 let final_trace_cost ≝ compute_trace_any_label_cost_using_paid c ost_labels end_flag … final_trace in190 let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cm cost_labels end_flag … final_trace in 294 191 call_trace_cost + final_trace_cost 295 192 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 296 compute_trace_any_label_cost_using_paid c ost_labels end_flag193 compute_trace_any_label_cost_using_paid cm cost_labels end_flag 297 194 status_init status_end tail_trace 298 195 ] 299 196 and compute_trace_label_return_cost_using_paid 300 (cost_labels: BitVectorTrie costlabel 16) 301 (start_status: Status) (final_status: Status) 302 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 197 (cm: ?) 198 (cost_labels: BitVectorTrie costlabel 16) 199 (start_status: Status cm) (final_status: Status cm) 200 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) 303 201 on the_trace: nat ≝ 304 202 match the_trace with … … 311 209 312 210 let rec compute_trace_label_label_cost_using_paid_ok 211 (cm: ?) 313 212 (cost_labels: BitVectorTrie costlabel 16) 314 213 (trace_ends_flag: trace_ends_with_ret) 315 (start_status: Status ) (final_status: Status)316 (the_trace: trace_label_label (ASM_abstract_status c ost_labels) trace_ends_flag214 (start_status: Status cm) (final_status: Status cm) 215 (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag 317 216 start_status final_status) on the_trace: 318 compute_trace_label_label_cost_using_paid c ost_labels … the_trace =217 compute_trace_label_label_cost_using_paid cm cost_labels … the_trace = 319 218 compute_max_trace_label_label_cost … the_trace ≝ ? 320 219 and compute_trace_any_label_cost_using_paid_ok 220 (cm: ?) 321 221 (cost_labels: BitVectorTrie costlabel 16) 322 222 (trace_ends_flag: trace_ends_with_ret) 323 (start_status: Status ) (final_status: Status)324 (the_trace: trace_any_label (ASM_abstract_status c ost_labels)223 (start_status: Status cm) (final_status: Status cm) 224 (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) 325 225 trace_ends_flag start_status final_status) on the_trace: 326 compute_paid_trace_any_label c ost_labels trace_ends_flag … the_trace327 +compute_trace_any_label_cost_using_paid c ost_labels trace_ends_flag … the_trace328 =compute_max_trace_any_label_cost c ost_labels trace_ends_flag … the_trace ≝ ?226 compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace 227 +compute_trace_any_label_cost_using_paid cm cost_labels trace_ends_flag … the_trace 228 =compute_max_trace_any_label_cost cm cost_labels trace_ends_flag … the_trace ≝ ? 329 229 and compute_trace_label_return_cost_using_paid_ok 330 (cost_labels: BitVectorTrie costlabel 16) 331 (start_status: Status) (final_status: Status) 332 (the_trace: trace_label_return (ASM_abstract_status cost_labels) 230 (cm: ?) 231 (cost_labels: BitVectorTrie costlabel 16) 232 (start_status: Status cm) (final_status: Status cm) 233 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) 333 234 start_status final_status) on the_trace: 334 compute_trace_label_return_cost_using_paid c ost_labels … the_trace =335 compute_max_trace_label_return_cost c ost_labels … the_trace ≝ ?.235 compute_trace_label_return_cost_using_paid cm cost_labels … the_trace = 236 compute_max_trace_label_return_cost cm cost_labels … the_trace ≝ ?. 336 237 [ cases the_trace #endsf #ss #es #tr #H normalize 337 238 @compute_trace_any_label_cost_using_paid_ok … … 339 240 [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O % 340 241 | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O % 341 | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%); 242 | 243 #sp #ss #sf #H1 #H2 #tr1 #tr2 #H3 244 whd in ⊢ (???%); whd in ⊢ (??(??%)?); whd in ⊢ (??(?%?)?); 245 >compute_trace_label_return_cost_using_paid_ok in ⊢ (??%?); 246 >commutative_plus in ⊢ (??%?); @eq_f % 247 | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #H4 #tr2 whd in ⊢ (??(?%%)%); 342 248 <compute_trace_any_label_cost_using_paid_ok 343 249 <compute_trace_label_return_cost_using_paid_ok … … 374 280 *) 375 281 282 include alias "ASM/BitVectorTrie.ma". 283 376 284 let rec compute_cost_trace_label_label 285 (cm: BitVectorTrie Byte 16) 377 286 (cost_labels: BitVectorTrie costlabel 16) 378 287 (trace_ends_flag: trace_ends_with_ret) 379 (start_status: Status ) (final_status: Status)380 (the_trace: trace_label_label (ASM_abstract_status c ost_labels) trace_ends_flag288 (start_status: Status cm) (final_status: Status cm) 289 (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag 381 290 start_status final_status) on the_trace: 382 list (Σk:costlabel. ∃pc . lookup_opt … pc cost_labels = Some … k) ≝291 list (Σk:costlabel. ∃pc: Word. lookup_opt … pc cost_labels = Some … k) ≝ 383 292 match the_trace with 384 293 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 385 let pc ≝ program_counter …initial in294 let pc ≝ program_counter ? cm initial in 386 295 let label ≝ 387 match lookup_opt … pc cost_labels return λx . match x with [None ⇒ False | Some _ ⇒ True] → costlabel with296 match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with 388 297 [ None ⇒ λabs. ⊥ 389 298 | Some l ⇒ λ_. l ] labelled_proof in 390 (mk_Sig … label ?)::compute_cost_trace_any_label … given_trace299 (mk_Sig ?? label ?)::compute_cost_trace_any_label cm cost_labels ends_flag initial final … given_trace 391 300 ] 392 301 and compute_cost_trace_any_label 302 (cm: BitVectorTrie Byte 16) 393 303 (cost_labels: BitVectorTrie costlabel 16) 394 304 (trace_ends_flag: trace_ends_with_ret) 395 (start_status: Status ) (final_status: Status)396 (the_trace: trace_any_label (ASM_abstract_status c ost_labels) trace_ends_flag start_status final_status)305 (start_status: Status cm) (final_status: Status cm) 306 (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status) 397 307 on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝ 398 308 match the_trace with 399 [ tal_base_not_return the_status _ _ _ _ ⇒ [] 400 | tal_base_return the_status _ _ _ ⇒ [] 309 [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] 310 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 311 compute_cost_trace_label_return … call_trace 312 | tal_base_return the_status _ _ _ ⇒ [ ] 401 313 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 402 _ _ _ call_trace final_trace ⇒314 _ _ _ call_trace _ final_trace ⇒ 403 315 let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in 404 let final_cost_trace ≝ compute_cost_trace_any_label c ost_labels end_flag … final_trace in316 let final_cost_trace ≝ compute_cost_trace_any_label cm cost_labels end_flag … final_trace in 405 317 call_cost_trace @ final_cost_trace 406 318 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 407 compute_cost_trace_any_label c ost_labels end_flag319 compute_cost_trace_any_label cm cost_labels end_flag 408 320 status_init status_end tail_trace 409 321 ] 410 322 and compute_cost_trace_label_return 411 (cost_labels: BitVectorTrie costlabel 16) 412 (start_status: Status) (final_status: Status) 413 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 323 (cm: BitVectorTrie Byte 16) 324 (cost_labels: BitVectorTrie costlabel 16) 325 (start_status: Status cm) (final_status: Status cm) 326 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) 414 327 on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝ 415 328 match the_trace with 416 [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift329 [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label cm … trace_to_lift 417 330 | tlr_step initial labelled final labelled_trace ret_trace ⇒ 418 let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in419 let return_cost ≝ compute_cost_trace_label_return … ret_trace in331 let labelled_cost ≝ compute_cost_trace_label_label cm … labelled_trace in 332 let return_cost ≝ compute_cost_trace_label_return cm … ret_trace in 420 333 labelled_cost @ return_cost 421 334 ]. … … 425 338 | // ] 426 339 qed. 427 428 (* XXX: zero in base cases (where the trace is a singleton transition) because429 we are counting until one from end430 *)431 let rec trace_any_label_length432 (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)433 (start_status: Status) (final_status: Status)434 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)435 on the_trace: nat ≝436 match the_trace with437 [ tal_base_not_return the_status _ _ _ _ ⇒ 0438 | tal_base_return the_status _ _ _ ⇒ 0439 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒440 let tail_length ≝ trace_any_label_length … final_trace in441 let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in442 pc_difference + tail_length443 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒444 let tail_length ≝ trace_any_label_length … tail_trace in445 let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in446 pc_difference + tail_length447 ].448 340 449 341 (* XXX: commented out in favour of above … … 586 478 ] 587 479 qed. 588 589 let rec block_cost_trace_any_label_static_dynamic_ok590 (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)591 (trace_ends_flag: ?) (start_status: Status) (final_status: Status)592 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)593 on the_trace:594 let code_memory ≝ code_memory … start_status in595 let program_counter ≝ program_counter … start_status in596 ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.597 ∀good_program_witness: good_program code_memory total_program_size.598 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧599 block_cost code_memory program_counter total_program_size cost_labels reachable_program_counter_witness good_program_witness =600 compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ ?.601 letin code_memory ≝ (code_memory … start_status)602 letin program_counter ≝ (program_counter … start_status)603 #reachable_program_counter_witness #good_program_witness604 generalize in match (refl … final_status);605 generalize in match (refl … start_status);606 cases the_trace in ⊢ (???% → ???% → %);607 [1:608 #start_status' #final_status' #execute_hyp #classifier_hyp #costed_hyp609 #start_status_refl #final_status_refl destruct610 whd in match (trace_any_label_length ? ? ? ? ?);611 whd in match (compute_paid_trace_any_label ? ? ? ? ?);612 @and_intro_right613 [1:614 generalize in match reachable_program_counter_witness;615 whd in match (reachable_program_counter code_memory total_program_size program_counter);616 * #irrelevant #relevant617 lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)618 #hyp assumption619 |2:620 * #n #trace_length_hyp621 whd in match block_cost; normalize nodelta622 generalize in match reachable_program_counter_witness;623 generalize in match good_program_witness;624 <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);625 -reachable_program_counter_witness #reachable_program_counter_witness626 -good_program_witness #good_program_witness627 whd in ⊢ (??%?); @pair_elim628 ]629 |2:630 #start_status' #final_status' #execute_hyp #classified_hyp631 #start_status_refl #final_status_refl destruct632 whd in match (trace_any_label_length ? ? ? ? ?);633 whd in match (compute_paid_trace_any_label ? ? ? ? ?);634 @and_intro_right635 [1:636 generalize in match reachable_program_counter_witness;637 whd in match (reachable_program_counter code_memory total_program_size program_counter);638 * #irrelevant #relevant639 lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)640 #hyp assumption641 |2:642 * #n #trace_length_hyp643 whd in match block_cost; normalize nodelta644 generalize in match reachable_program_counter_witness;645 generalize in match good_program_witness;646 <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);647 -reachable_program_counter_witness #reachable_program_counter_witness648 -good_program_witness #good_program_witness649 whd in match (0 + S n); whd in ⊢ (??%?);650 ]651 |3:652 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call653 #status_final #execute_hyp #classifier_hyp #after_return_hyp654 #trace_label_return #trace_any_label #start_status_refl #final_status_refl655 destruct656 whd in match (trace_any_label_length ? ? ? ? ?);657 whd in match (compute_paid_trace_any_label ? ? ? ? ?);658 @and_intro_right659 [1:660 |2:661 ]662 |4:663 #end_flag #status_pre #status_init #status_end #execute_hyp #trace_any_label664 #classifier_hyp #costed_hyp #start_status_refl #final_status_refl665 destruct666 whd in match (trace_any_label_length ? ? ? ? ?);667 whd in match (compute_paid_trace_any_label ? ? ? ? ?);668 @and_intro_right669 [1:670 |2:671 ]672 ]673 ]674 675 corollary block_cost_trace_label_labelstatic_dynamic_ok:676 ∀program_size: nat.677 ∀cost_labels: BitVectorTrie costlabel 16.678 ∀trace_ends_flag.679 ∀start_status: Status.680 ∀final_status: Status.681 ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.682 let code_memory ≝ code_memory … start_status in683 let program_counter ≝ program_counter … start_status in684 ∀reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter.685 ∀good_program_witness: good_program code_memory program_size.686 (∃n: nat. trace_length start_status final_status + n = program_size) ∧687 block_cost code_memory program_counter program_size program_size cost_labels reachable_program_counter_witness good_program_witness ? =688 compute_paid_trace_label_label cost_labels trace_ends_flag start_status final_status the_trace.689 [2:690 @le_plus_n_r691 |1:692 #program_size #cost_labels #trace_ends_flag #start_status #final_status693 #the_trace normalize nodelta694 #reachable_program_counter_witness #good_program_witness695 generalize in match start_status;696 qed.697 480 698 481 (* … … 703 486 *) 704 487 488 include alias "arithmetics/bigops.ma". 489 705 490 (* This shoudl go in bigops! *) 706 491 theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B. 707 492 \big[op,nil]_{i<k1+k2|p i} (f i) = 708 493 op \big[op,nil]_{i<k2|p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1|p i} (f i). 709 #k1 #k2 #p #B #nil #op #f >bigop_sum >commutative_plus @same_bigop #i @leb_elim normalize 494 #k1 #k2 #p #B #nil #op #f >bigop_sum 495 >commutative_plus @same_bigop #i @leb_elim normalize 710 496 [2,4: // 711 497 | #H1 #H2 <plus_minus_m_m // … … 751 537 with precedence 20 752 538 for @{'bigop $n plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f)}. 753 754 axiom code_memory_ro_label_label:755 ∀cost_labels. ∀ends_flag.756 ∀initial,final. trace_label_label (ASM_abstract_status cost_labels) ends_flag initial final →757 code_memory … initial = code_memory … final.758 759 (*760 axiom code_memory_ro_label_return:761 ∀cost_labels.762 ∀initial,final. trace_label_return (ASM_abstract_status cost_labels) initial final →763 code_memory … initial = code_memory … final.764 *)765 539 766 540 definition tech_cost_of_label0: … … 870 644 871 645 let rec compute_max_trace_label_return_cost_ok_with_trace 646 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size) 872 647 (cost_labels: BitVectorTrie costlabel 16) 873 648 (cost_map: identifier_map CostTag nat) 874 (initial: Status ) (final: Status)875 (trace: trace_label_return (ASM_abstract_status c ost_labels) initial final)649 (initial: Status cm) (final: Status cm) 650 (trace: trace_label_return (ASM_abstract_status cm cost_labels) initial final) 876 651 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 877 652 on trace: 878 653 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 879 block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres). 880 let ctrace ≝ compute_cost_trace_label_return … trace in 881 compute_max_trace_label_return_cost … trace = 654 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 655 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres). 656 let ctrace ≝ compute_cost_trace_label_return cm … trace in 657 compute_max_trace_label_return_cost cm … trace = 882 658 (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 883 659 ≝ ? 884 660 and compute_max_trace_label_label_cost_ok_with_trace 661 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size) 885 662 (cost_labels: BitVectorTrie costlabel 16) 886 663 (trace_ends_flag: trace_ends_with_ret) 887 664 (cost_map: identifier_map CostTag nat) 888 (initial: Status ) (final: Status)889 (trace: trace_label_label (ASM_abstract_status c ost_labels) trace_ends_flag initial final)665 (initial: Status cm) (final: Status cm) 666 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final) 890 667 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 891 668 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 892 block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres)) 669 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 670 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres)) 893 671 on trace: 894 672 let ctrace ≝ compute_cost_trace_label_label … trace in … … 896 674 (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)) 897 675 ≝ ?. 898 cases trace 899 [ #sb #sa #tr #dom_codom 900 @compute_max_trace_label_label_cost_ok_with_trace @dom_codom901 | #si #sl #sf #tr1 #tr2 #dom_codom whd in ⊢ (let ctrace ≝ % in ??%?); 902 change with (let ctrace ≝ ? in ? = bigop (|? @ ?|) ?????) 903 >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????));904 change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2905 [ >(compute_max_trace_label_return_cost_ok_with_trace … cost_map … codom_dom)906 -compute_max_trace_label_return_cost_ok_with_trace907 [2:lapply (code_memory_ro_label_label … tr1) #E2 <E2 @dom_codom]676 cases trace normalize nodelta 677 [ #sb #sa #tr #dom_codom whd in ⊢ (??%?); 678 whd in match (compute_cost_trace_label_return ?????); 679 @(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness) @dom_codom 680 | #si #sl #sf #tr1 #tr2 #dom_codom 681 whd in ⊢ (??%?); 682 whd in match (compute_cost_trace_label_return ?????); 683 >append_length >bigop_sum_rev >commutative_plus @eq_f2 684 [ >(compute_max_trace_label_return_cost_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom) 685 -compute_max_trace_label_return_cost_ok_with_trace 908 686 @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift // 909 | >(compute_max_trace_label_label_cost_ok_with_trace … cost_map … codom_dom … dom_codom) 687 | >(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom) 688 -compute_max_trace_label_return_cost_ok_with_trace 910 689 @same_bigop [//] #i #H #_ 911 690 ]
Note: See TracChangeset
for help on using the changeset viewer.