Changeset 1669 for src/ASM/ASMCosts.ma
- Timestamp:
- Feb 1, 2012, 3:36:08 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1665 r1669 363 363 364 364 definition current_instruction ≝ 365 λs: Status. 366 current_instruction0 (code_memory … s) (program_counter … s). 365 λcode_memory. 366 λs: Status code_memory. 367 current_instruction0 code_memory (program_counter … s). 367 368 368 369 definition ASM_classify0: instruction → status_class ≝ … … 392 393 ]. 393 394 394 definition ASM_classify: Status → status_class ≝ 395 λs: Status. 396 ASM_classify0 (current_instruction s). 395 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝ 396 λcode_memory. 397 λs: Status code_memory. 398 ASM_classify0 (current_instruction … s). 397 399 398 400 definition current_instruction_is_labelled ≝ 401 λcode_memory. 399 402 λcost_labels: BitVectorTrie costlabel 16. 400 λs: Status .401 let pc ≝ program_counter … s in403 λs: Status code_memory. 404 let pc ≝ program_counter … code_memory s in 402 405 match lookup_opt … pc cost_labels with 403 406 [ None ⇒ False … … 406 409 407 410 definition next_instruction_properly_relates_program_counters ≝ 408 λbefore: Status. 409 λafter : Status. 410 let size ≝ current_instruction_cost before in 411 let pc_before ≝ program_counter … before in 412 let pc_after ≝ program_counter … after in 411 λcode_memory. 412 λbefore: Status code_memory. 413 λafter : Status code_memory. 414 let size ≝ current_instruction_cost code_memory before in 415 let pc_before ≝ program_counter … code_memory before in 416 let pc_after ≝ program_counter … code_memory after in 413 417 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 414 418 sum = pc_after. 415 419 416 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ 417 λcost_labels. 418 mk_abstract_status 419 Status 420 (λs,s'. (execute_1 s) = s') 421 (λs,class. ASM_classify s = class) 422 (current_instruction_is_labelled cost_labels) 423 next_instruction_properly_relates_program_counters. 420 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ 421 λcode_memory. 422 λcost_labels. 423 mk_abstract_status 424 (Status code_memory) 425 (λs,s'. (execute_1 … s) = s') 426 (λs,class. ASM_classify … s = class) 427 (current_instruction_is_labelled … cost_labels) 428 (next_instruction_properly_relates_program_counters code_memory). 424 429 425 430 let rec trace_any_label_length 426 (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) 427 (start_status: Status) (final_status: Status) 428 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 431 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 432 (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) 433 (final_status: Status code_memory) 434 (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) 429 435 on the_trace: nat ≝ 430 436 match the_trace with … … 443 449 444 450 let rec compute_paid_trace_any_label 445 (co st_labels: BitVectorTrie costlabel 16)446 (trace_ends_flag: trace_ends_with_ret)447 (start_status: Status) (final_status: Status)448 (the_trace: trace_any_label (ASM_abstract_statuscost_labels) trace_ends_flag start_status final_status)451 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 452 (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) 453 (final_status: Status code_memory) 454 (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) 449 455 on the_trace: nat ≝ 450 456 match the_trace with 451 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status452 | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status453 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost pre_fun_call457 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status 458 | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status 459 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call 454 460 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 455 461 _ _ _ call_trace _ final_trace ⇒ 456 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in457 let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in462 let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in 463 let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in 458 464 current_instruction_cost + final_trace_cost 459 465 | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 460 let current_instruction_cost ≝ current_instruction_cost status_pre in466 let current_instruction_cost ≝ current_instruction_cost … status_pre in 461 467 let tail_trace_cost ≝ 462 compute_paid_trace_any_label cost_labels end_flag468 compute_paid_trace_any_label … cost_labels end_flag 463 469 status_init status_end tail_trace 464 470 in … … 467 473 468 474 definition compute_paid_trace_label_label ≝ 469 λcost_labels: BitVectorTrie costlabel 16. 475 λcode_memory: BitVectorTrie Byte 16. 476 λcost_labels: BitVectorTrie costlabel 16. 470 477 λtrace_ends_flag: trace_ends_with_ret. 471 λstart_status: Status. 472 λfinal_status: Status. 473 λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 474 start_status final_status. 478 λstart_status: Status code_memory. 479 λfinal_status: Status code_memory. 480 λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 475 481 match the_trace with 476 482 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ … … 487 493 qed. 488 494 489 axiom as_execute_preserves_code_memory:490 ∀cost_labels : BitVectorTrie costlabel 16.491 ∀start_status: ASM_abstract_status cost_labels.492 ∀final_status: ASM_abstract_status cost_labels.493 as_execute … start_status final_status →494 code_memory … start_status = code_memory … final_status.495 496 axiom trace_label_return_preserves_code_memory:497 ∀cost_labels : BitVectorTrie costlabel 16.498 ∀start_status: ASM_abstract_status cost_labels.499 ∀final_status: ASM_abstract_status cost_labels.500 ∀the_trace : trace_label_return … start_status final_status.501 code_memory … start_status = code_memory … final_status.502 503 495 (* XXX: indexing bug re-emerges! *) 504 496 example fetch_half_add: 497 ∀code_memory: BitVectorTrie Byte 16. 505 498 ∀cost_labels: BitVectorTrie costlabel 16. 506 ∀the_status : ASM_abstract_status co st_labels.507 \snd (\fst (fetch (code_memory … the_status)(program_counter … the_status))) =508 \snd (half_add 16 (program_counter (BitVectorTrie Byte 16)the_status)509 (bitvector_of_nat … (\snd (fetch (code_memory … the_status)(program_counter … the_status))))).499 ∀the_status : ASM_abstract_status code_memory cost_labels. 500 \snd (\fst (fetch code_memory (program_counter … the_status))) = 501 \snd (half_add 16 (program_counter … the_status) 502 (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))). 510 503 cases daemon 511 504 qed. … … 523 516 (m - n) + n = m. 524 517 #m #n #proof /2 by plus_minus/ 518 qed. 519 520 (* XXX: indexing bug *) 521 example fetch_twice_fetch_execute_1: 522 ∀code_memory: BitVectorTrie Byte 16. 523 ∀start_status: Status code_memory. 524 \snd (\fst (fetch code_memory (program_counter … start_status))) = 525 program_counter … (execute_1 … start_status). 526 cases daemon 527 qed. (* 528 #code_memory #start_status 529 whd in match (execute_1 code_memory start_status); 530 whd in match (execute_1' code_memory start_status); normalize nodelta 531 cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks 532 cases instruction_pc #instruction #pc normalize nodelta *) 533 534 lemma blah: 535 ∀code_memory' : (BitVectorTrie Byte 16). 536 ∀program_counter' : Word. 537 ∀total_program_size : ℕ. 538 ∀cost_labels : (BitVectorTrie costlabel 16). 539 ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). 540 ∀good_program_witness : (good_program code_memory' total_program_size). 541 ∀program_size' : ℕ. 542 ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). 543 ∀ticks : ℕ. 544 ∀instruction : instruction. 545 ∀program_counter'' : Word. 546 ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). 547 ∀real_instruction : (preinstruction [[relative]]). 548 ∀real_instruction_refl : (RealInstruction … real_instruction = instruction). 549 ∀start_status : (Status code_memory'). 550 ∀final_status : (Status code_memory'). 551 ∀trace_ends_flag : trace_ends_with_ret. 552 ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). 553 ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). 554 ∀classify_assm: ASM_classify0 instruction = cl_other. 555 ∀pi1 : ℕ. 556 (if match lookup_opt costlabel 16 program_counter'' cost_labels with 557 [None ⇒ true 558 |Some _ ⇒ false 559 ] 560 then 561 ∀start_status0:Status code_memory'. 562 ∀final_status0:Status code_memory'. 563 ∀trace_ends_flag0:trace_ends_with_ret. 564 ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0. 565 program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 → 566 (∃n:ℕ 567 .trace_any_label_length code_memory' cost_labels 568 trace_ends_flag0 start_status0 final_status0 the_trace0 569 +S n 570 =total_program_size) 571 ∧pi1 572 =compute_paid_trace_any_label code_memory' cost_labels 573 trace_ends_flag0 start_status0 final_status0 the_trace0 574 else (pi1=O) ) 575 →(∃n:ℕ 576 .trace_any_label_length code_memory' cost_labels trace_ends_flag 577 start_status final_status the_trace 578 +S n 579 =total_program_size) 580 ∧ticks+pi1 581 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag 582 start_status final_status the_trace. 583 #code_memory' #program_counter' #total_program_size #cost_labels 584 #reachable_program_counter_witness #good_program_witness 585 #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH 586 #real_instruction #real_instruction_refl #start_status #final_status 587 #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost 588 #recursive_assm @(trace_any_label_inv_ind … the_trace) 589 [5: 590 #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label 591 #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl 592 #the_trace_refl 593 destruct 594 whd in match (trace_any_label_length … (tal_step_default …)); 595 whd in match (compute_paid_trace_any_label … (tal_step_default …)); 596 whd in costed_assm:(?%); 597 generalize in match costed_assm; 598 generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)); 599 generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels) 600 in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); 601 #lookup_assm cases lookup_assm 602 [1: 603 #None_lookup_opt_assm normalize nodelta #ignore 604 generalize in match recursive_assm; 605 cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre))) 606 [1: 607 <fetch_twice_fetch_execute_1 <FETCH % 608 |2: 609 #program_counter_assm >program_counter_assm <None_lookup_opt_assm 610 normalize nodelta #new_recursive_assm 611 cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end 612 end_flag trace_any_label ?) [2: % ] 613 #exists_assm #recursive_block_cost_assm % 614 [1: 615 cases exists_assm #exists_n #total_program_size_refl 616 <total_program_size_refl 617 %{(exists_n - current_instruction_cost … status_pre)} 618 |2: 619 >recursive_block_cost_assm 620 whd in match (current_instruction_cost … status_pre); 621 cut(ticks = \snd (fetch code_memory' 622 (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) 623 [1: 624 <FETCH % 625 |2: 626 #ticks_refl_assm >ticks_refl_assm % 627 ] 628 ] 629 ] 630 |2: 631 #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta 632 #absurd cases absurd #absurd cases(absurd I) 633 ] 634 |1: 635 #status_start #status_final #execute_assm #classifier_assm #costed_assm 636 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 637 destruct 638 whd in match (trace_any_label_length … (tal_base_not_return …)); 639 whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); 640 whd in costed_assm; 641 generalize in match costed_assm; 642 generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)); 643 generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels) 644 in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); 645 #lookup_assm cases lookup_assm 646 [1: 647 #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm 648 #absurd cases absurd 649 |2: 650 #costlabel #Some_lookup_opt_assm normalize nodelta #ignore 651 generalize in match recursive_assm; 652 cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start))) 653 [1: 654 <fetch_twice_fetch_execute_1 <FETCH % 655 |2: 656 #program_counter_assm >program_counter_assm <Some_lookup_opt_assm 657 normalize nodelta #new_recursive_assm >new_recursive_assm % 658 [1: 659 %{(pred total_program_size)} whd in ⊢ (??%?); 660 @S_pred 661 generalize in match good_program_witness; 662 whd in match (good_program … total_program_size); 663 #good_program_hyp 664 lapply(good_program_hyp (program_counter … status_start) reachable_program_counter_witness) 665 <FETCH normalize nodelta -good_program_hyp (* XXX: Claudio here *) 666 |2: 667 cut(ticks = \snd (fetch code_memory' 668 (program_counter (BitVectorTrie Byte 16) code_memory' status_start))) 669 [1: 670 <FETCH % 671 |2: 672 #ticks_refl_assm >ticks_refl_assm 673 <plus_n_O % 674 ] 675 ] 676 ] 677 |2: 678 #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta 679 #absurd cases absurd #absurd cases(absurd I) 680 ] 681 |2: 682 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm 683 #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ 684 |3: 685 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 686 #classifier_assm #after_return_assm #trace_label_return #costed_assm 687 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 688 destruct @⊥ 689 ] 690 change with ( 691 ASM_classify0 ? = ?) in classifier_assm; 692 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 693 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 694 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) 525 695 qed. 526 696 … … 533 703 total_program_size ≤ program_size + nat_of_bitvector … program_counter' → 534 704 Σcost_of_block: nat. 535 ∀start_status: Status. 536 ∀final_status: Status. 705 if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then 706 ∀start_status: Status code_memory'. 707 ∀final_status: Status code_memory'. 537 708 ∀trace_ends_flag. 538 ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 539 code_memory' = code_memory … start_status → 540 program_counter' = program_counter … start_status → 541 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 542 cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ 709 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 710 program_counter' = program_counter … start_status → 711 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 712 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace 713 else 714 (cost_of_block = 0) ≝ 543 715 match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with 544 716 [ O ⇒ λbase_case. ⊥ … … 546 718 let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in 547 719 let to_continue ≝ 548 match lookup_opt … program_counter' 'cost_labels with720 match lookup_opt … program_counter' cost_labels with 549 721 [ None ⇒ true 550 722 | Some _ ⇒ first_time_around 551 723 ] 552 724 in 553 if to_continue then554 725 ((if to_continue then 726 pi1 … (match instruction return λx. x = instruction → ? with 555 727 [ RealInstruction real_instruction ⇒ λreal_instruction_refl. 556 728 match real_instruction return λx. x = real_instruction → 557 729 Σcost_of_block: nat. 558 ∀start_status: Status .559 ∀final_status: Status .730 ∀start_status: Status code_memory'. 731 ∀final_status: Status code_memory'. 560 732 ∀trace_ends_flag. 561 ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status. 562 code_memory' = code_memory … start_status → 563 program_counter' = program_counter … start_status → 564 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 565 cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace with 733 ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status. 734 program_counter' = program_counter … start_status → 735 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 736 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with 566 737 [ RET ⇒ λinstr. ticks 567 738 | JC relative ⇒ λinstr. ticks … … 575 746 | DJNZ src_trgt relative ⇒ λinstr. ticks 576 747 | _ ⇒ λinstr. 748 577 749 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? 578 750 ] (refl …) … … 588 760 | MOVC src trgt ⇒ λinstr. 589 761 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? 590 ] (refl …) 762 ] (refl …)) 591 763 else 592 (0 : (Σn: nat. ?)) 764 0) 765 : Σcost_of_block: nat. 766 match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with 767 [ true ⇒ 768 ∀start_status: Status code_memory'. 769 ∀final_status: Status code_memory'. 770 ∀trace_ends_flag. 771 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 772 program_counter' = program_counter … start_status → 773 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ 774 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace 775 | false ⇒ 776 (cost_of_block = 0) 777 ]) 593 778 ]. 594 779 [1: … … 596 781 @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) 597 782 @(le_to_lt_to_lt … base_case hyp) 783 |2: 784 change with ( 785 if to_continue then 786 ? 787 else 788 (? = 0)) >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta 789 @pi2 790 |3: 791 change with ( 792 if to_continue then 793 ? 794 else 795 (0 = 0)) >p normalize nodelta % 598 796 |4: 599 #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl 797 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 798 cases(block_cost' ?????????) -block_cost' 799 @(blah … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …) 800 destruct % 801 |4: 802 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 600 803 cases(block_cost' ?????????) -block_cost' 601 804 #recursive_block_cost #recursive_assm 602 805 @(trace_any_label_inv_ind … the_trace) 603 806 [1: 604 #start_status' #final_status' #execute_assm #classifier_assm #costed_assm 605 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct 606 cases classifier_assm 607 whd in match (as_classifier ???); 608 whd in ⊢ (??%? → ?); 609 whd in match current_instruction; normalize nodelta 610 whd in match current_instruction0; normalize nodelta 611 #absurd @⊥ <FETCH in absurd; normalize nodelta 612 #absurd destruct(absurd) 807 #status_start #status_final #execute_assm #classifier_assm #costed_assm 808 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 809 destruct 810 whd in match (trace_any_label_length … (tal_base_not_return …)); 811 whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); 812 whd in costed_assm; 613 813 |2: 614 814 #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm … … 623 823 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 624 824 #classifier_assm #after_return_assm #trace_label_return #costed_assm 825 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 826 destruct 827 whd in classifier_assm; 828 whd in classifier_assm:(??%?); 829 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 830 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 831 @⊥ <FETCH in classifier_assm; normalize nodelta 832 #absurd destruct(absurd) 833 |4: 834 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 835 #status_final #execute_assm #classifier_assm #after_return_assm 836 #trace_label_return #costed_assm #trace_any_label #ends_flag_refl 837 #start_status_refl #final_status_refl #the_trace_refl 838 destruct 839 whd in classifier_assm; 840 whd in classifier_assm:(??%?); 841 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 842 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 843 @⊥ <FETCH in classifier_assm; normalize nodelta 844 #absurd destruct(absurd) 845 |5: 846 ] 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 |3: 877 #status_pre_fun_call #status_start_fun_call #status_final #execute_assm 878 #classifier_assm #after_return_assm #trace_label_return #costed_assm 625 879 #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 626 880 destruct 627 881 whd in match (compute_paid_trace_any_label … (tal_base_call …)); 628 882 whd in match (trace_any_label_length … (tal_base_call …)); 629 cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret 630 (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call 631 (execute_1 status_pre_fun_call) status_final 632 (refl Status (execute_1 status_pre_fun_call)) classifier_assm 633 after_return_assm trace_label_return costed_assm) ? ?) 883 cases(recursive_assm … 884 (tal_base_call (ASM_abstract_status code_memory' cost_labels) 885 status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …) 886 classifier_assm after_return_assm trace_label_return costed_assm) ?) 634 887 [1: 635 * #recursive_n #recursive_trace_total #recursive_block_cost_assm % 888 * #recursive_n #recursive_trace_total #recursive_block_cost_assm % 636 889 [1: 637 890 %{(pred total_program_size)} … … 646 899 ] 647 900 |2: 648 % 649 |3: 650 cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call)))) 901 cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call)))) 651 902 [1: 652 903 cases FETCH % … … 658 909 ] 659 910 ] 660 [1:661 911 |4: 662 912 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call … … 697 947 <FETCH % 698 948 ] 949 699 950 |2: 700 951 lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
Note: See TracChangeset
for help on using the changeset viewer.