Changeset 1579 for src/ASM/CostsProof.ma
- Timestamp:
- Dec 1, 2011, 2:11:37 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1577 r1579 249 249 qed. 250 250 251 axiom clock_execute_1: 252 ∀s: Status. 253 clock … (execute_1 s) = current_instruction_cost s + clock … s. 254 255 axiom plus_le_le: 251 lemma m_le_plus_n_m: 252 ∀m, n: nat. 253 m ≤ n + m. 254 #m #n // 255 qed. 256 257 lemma n_plus_m_le_o_to_m_le_o: 256 258 ∀m, n, o: nat. 257 m + n ≤ o → n ≤ o. 259 n + m ≤ o → m ≤ o. 260 #m #n #o #assm /2 by le_plus_b/ 261 qed. 262 263 lemma m_minus_n_plus_o_m_minus_n_minus_o: 264 ∀m, n, o: nat. 265 m - (n + o) = m - n - o. 266 #m #n #o /2 by / 267 qed. 268 269 let rec compute_max_trace_label_label_cost_is_ok 270 (cost_labels: BitVectorTrie costlabel 16) 271 (trace_ends_flag: trace_ends_with_ret) 272 (start_status: Status) (final_status: Status) 273 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 274 start_status final_status) on the_trace: 275 clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ? 276 and compute_max_trace_any_label_cost_is_ok 277 (cost_labels: BitVectorTrie costlabel 16) 278 (trace_ends_flag: trace_ends_with_ret) 279 (start_status: Status) (final_status: Status) 280 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 281 on the_trace: 282 clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ? 283 and compute_max_trace_label_return_cost_is_ok 284 (cost_labels: BitVectorTrie costlabel 16) 285 (start_status: Status) (final_status: Status) 286 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 287 on the_trace: 288 clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?. 289 [1: 290 cases the_trace 291 #ends_flag #start_status #end_status #any_label_trace #is_costed 292 normalize @compute_max_trace_any_label_cost_is_ok 293 |2: 294 cases the_trace 295 [1,2: 296 #start_status #final_status #is_next #is_not_return try (#is_costed) 297 change with (current_instruction_cost start_status) in ⊢ (???(?%?)); 298 cases(is_next) 299 cases(execute_1 start_status) 300 whd in match eject; normalize nodelta; 301 #the_status #assm >assm % 302 |3: 303 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 304 #status_final #is_next #is_call #is_after_return #call_trace #final_trace 305 change with ( 306 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 307 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 308 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in 309 call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?)); 310 normalize nodelta; 311 >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call 312 status_final final_trace) 313 >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call 314 status_after_fun_call call_trace) 315 cases(is_next) in match (clock … status_start_fun_call); 316 cases(execute_1 status_pre_fun_call); 317 #the_status 318 whd in match eject; normalize nodelta; 319 #assm >assm 320 <associative_plus in ⊢ (??%?); 321 <commutative_plus in match ( 322 compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace 323 + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace); 324 >associative_plus in ⊢ (??%?); 325 <commutative_plus in match ( 326 compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace 327 + (current_instruction_cost status_pre_fun_call 328 + clock (BitVectorTrie Byte 16) status_pre_fun_call)); 329 >associative_plus in ⊢ (??%?); 330 <commutative_plus in match ( 331 clock (BitVectorTrie Byte 16) status_pre_fun_call 332 + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace); 333 <(associative_plus ( 334 (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace))) 335 <associative_plus in ⊢ (??%?); % 336 |4: 337 #end_flag #status_pre #status_init #status_end #is_next 338 #trace_any_label #is_other #is_not_costed 339 change with ( 340 let current_instruction_cost ≝ current_instruction_cost status_pre in 341 let tail_trace_cost ≝ 342 compute_max_trace_any_label_cost cost_labels end_flag 343 status_init status_end trace_any_label 344 in 345 current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?)); 346 normalize nodelta; 347 >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag 348 status_init status_end trace_any_label) 349 cases(is_next) in match (clock … status_init); 350 cases(execute_1 status_pre) 351 #the_status whd in match eject; normalize nodelta; 352 #assm >assm <associative_plus in ⊢ (??%?); 353 >commutative_plus in match ( 354 compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label 355 + current_instruction_cost status_pre); 356 % 357 ] 358 |3: 359 cases the_trace 360 [1: 361 #status_before #status_after #trace_to_lift 362 normalize @compute_max_trace_label_label_cost_is_ok 363 |2: 364 #status_initial #status_labelled #status_final #labelled_trace #ret_trace 365 normalize 366 >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace); 367 >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace); 368 <associative_plus in ⊢ (??%?); 369 >commutative_plus in match ( 370 compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace 371 + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace); 372 % 373 ] 374 ]. 375 qed. 258 376 259 377 let rec compute_max_trace_label_label_cost_is_ok … … 291 409 cases(is_next) 292 410 @conj 411 cases(execute_1 start_status) 412 #the_status #assm 413 whd in match eject; normalize nodelta 414 >assm 293 415 [1: 294 cases(execute_1 start_status) 295 #the_status #assm 296 whd in match eject; normalize nodelta 297 cases(assm) 298 #eq_hyp #le_hyp 299 >eq_hyp % 416 @minus_plus_m_m 300 417 |2: 301 cases(execute_1 start_status) 302 #the_status #assm 303 whd in match eject; normalize nodelta 304 cases(assm) 305 #eq_hyp #le_hyp 306 assumption 418 @m_le_plus_n_m 307 419 ] 308 420 |2: … … 311 423 cases(is_next) 312 424 @conj 425 cases(execute_1 start_status) 426 #the_status #assm 427 whd in match eject; normalize nodelta 428 >assm 313 429 [1: 314 cases(execute_1 start_status) 430 @minus_plus_m_m 431 |2: 432 @m_le_plus_n_m 433 ] 434 |3: 435 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 436 #status_final #is_next #is_call #is_after_return #call_trace #final_trace 437 change with ( 438 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 439 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 440 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in 441 call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?); 442 normalize nodelta; 443 @conj 444 [1: 445 cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call 446 status_after_fun_call call_trace) 447 #trace_label_return_eq #trace_label_return_le 448 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call 449 status_final final_trace) 450 #trace_any_label_eq #trace_any_label_le 451 >trace_any_label_eq >trace_label_return_eq 452 cases(is_next) 453 cases(execute_1 status_pre_fun_call) 315 454 #the_status #assm 316 whd in match eject; normalize nodelta 317 cases(assm) 318 #eq_hyp #le_hyp 319 >eq_hyp % 455 whd in match eject; normalize nodelta; 456 >assm >commutative_plus in match 457 (current_instruction_cost status_pre_fun_call 458 + clock (BitVectorTrie Byte 16) status_pre_fun_call); 459 >m_minus_n_plus_o_m_minus_n_minus_o 460 <(plus_minus_m_m 461 (clock (BitVectorTrie Byte 16) status_after_fun_call 462 - clock (BitVectorTrie Byte 16) status_pre_fun_call) 463 (current_instruction_cost status_pre_fun_call)) 464 [1: 465 @plus_minus_rearrangement_1 466 lapply(transitive_le 467 (clock … status_pre_fun_call) 468 (clock … status_start_fun_call) 469 (clock … status_after_fun_call) ? trace_label_return_le) 470 [1,3: 471 cases(is_next) 472 cases(execute_1 status_pre_fun_call) 473 whd in match eject; normalize nodelta; 474 #the_new_status #assm >assm @m_le_plus_n_m 475 |2,4: 476 #assm assumption 477 ] 478 |2: 479 cases(is_next) 480 assumption 320 481 |2: 321 cases(execute_1 start_status) 482 cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call 483 status_after_fun_call call_trace) 484 #trace_label_return_eq 485 cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call 486 status_final final_trace) 487 #trace_any_label_eq cases(is_next) 488 cases(execute_1 status_pre_fun_call) 322 489 #the_status #assm 323 whd in match eject; normalize nodelta 324 cases(assm) 325 #eq_hyp #le_hyp 490 whd in match eject; normalize nodelta; 491 >assm #after_final_le #pre_after_le 492 lapply(n_plus_m_le_o_to_m_le_o 493 (clock … status_pre_fun_call) 494 (current_instruction_cost status_pre_fun_call) 495 (clock … status_after_fun_call) pre_after_le); 496 #pre_after_le' 497 @(transitive_le 498 (clock … status_pre_fun_call) 499 (clock … status_after_fun_call) 500 (clock … status_final)) 326 501 assumption 327 502 ] 328 | 3:503 |*: cases daemon (* XXX: for now 329 504 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 330 505 #status_final #is_next #is_call #is_after_return #call_trace #final_trace … … 414 589 >clock_execute_1 415 590 @plus_le_le 416 ] 591 ]*) 417 592 ] 418 593 |3:
Note: See TracChangeset
for help on using the changeset viewer.