Changeset 1910 for src/ASM/ASMCosts.ma
- Timestamp:
- Apr 27, 2012, 5:48:20 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1909 r1910 224 224 qed. 225 225 226 (*227 226 (* XXX: indexing bug *) 228 lemma fetch_twice_fetch_execute_1:227 lemma execute_1_and_program_counter_after_other_in_lockstep: 229 228 ∀code_memory: BitVectorTrie Byte 16. 230 229 ∀start_status: Status code_memory. 231 230 ASM_classify code_memory start_status = cl_other → 232 \snd (\fst (fetch code_memory (program_counter … start_status))) = 233 program_counter … (execute_1 … start_status). 231 let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in 232 program_counter ? ? (execute_1 … start_status) = 233 program_counter_after_other pc instruction. 234 234 #code_memory #start_status #classify_assm 235 235 whd in match execute_1; normalize nodelta 236 236 cases (execute_1' code_memory start_status) #the_status 237 * #_ #classify_assm' @classify_assm' assumption 237 * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm; 238 cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks 239 #classify_assm #classify_assm' @classify_assm' assumption 238 240 qed-. 239 *)240 241 241 242 lemma reachable_program_counter_to_0_lt_total_program_size: … … 268 269 ∀program_counter'' : Word. 269 270 ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). 271 let program_counter''' ≝ program_counter_after_other program_counter'' instruction in 270 272 ∀start_status : (Status code_memory'). 271 273 ∀final_status : (Status code_memory'). … … 275 277 ∀classify_assm: ASM_classify0 instruction = cl_other. 276 278 ∀pi1 : ℕ. 277 (if match lookup_opt costlabel 16 program_counter'' cost_labels with279 (if match lookup_opt costlabel 16 program_counter''' cost_labels with 278 280 [None ⇒ true 279 281 |Some _ ⇒ false … … 284 286 ∀trace_ends_flag0:trace_ends_with_ret. 285 287 ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0. 286 program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →288 program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 → 287 289 pi1 288 290 =compute_paid_trace_any_label code_memory' cost_labels … … 313 315 #lookup_assm cases lookup_assm 314 316 [1: 315 #None_lookup_opt_assm normalize nodelta # ignore317 #None_lookup_opt_assm normalize nodelta #_ 316 318 generalize in match recursive_assm; 317 cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre))) 318 [1: 319 <fetch_twice_fetch_execute_1 320 [1: 321 <FETCH % 322 |2: 323 >classifier_assm % 324 ] 319 lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm) 320 <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm; 321 #None_lookup_opt_assm <None_lookup_opt_assm 322 normalize nodelta #new_recursive_assm 323 cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end 324 end_flag trace_any_label ?) try % 325 whd in match (current_instruction_cost … status_pre); 326 cut(ticks = \snd (fetch code_memory' 327 (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) 328 [1,3: 329 <FETCH % 325 330 |2: 326 #program_counter_assm >program_counter_assm <None_lookup_opt_assm 327 normalize nodelta #new_recursive_assm 328 cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end 329 end_flag trace_any_label ?) try % 330 whd in match (current_instruction_cost … status_pre); 331 cut(ticks = \snd (fetch code_memory' 332 (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) 333 [1: 334 <FETCH % 335 |2: 336 #ticks_refl_assm >ticks_refl_assm % 337 ] 331 #ticks_refl_assm >ticks_refl_assm % 332 |4: 333 #ticks_refl_assm 334 >rewrite_assm % 338 335 ] 339 336 |2: … … 359 356 #costlabel #Some_lookup_opt_assm normalize nodelta #ignore 360 357 generalize in match recursive_assm; 361 c ut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))358 cases classifier_assm 362 359 [1: 363 <fetch_twice_fetch_execute_1 364 [1: 365 <FETCH % 366 |2: 367 cases classifier_assm 368 [1: 369 whd in ⊢ (% → ?); 370 whd in ⊢ (??%? → ?); 371 whd in match (current_instruction code_memory' status_start); 372 <FETCH generalize in match classify_assm; 373 cases instruction 374 [8: 375 #preinstruction normalize nodelta 376 whd in match ASM_classify0; normalize nodelta 377 #contradiction >contradiction #absurd destruct(absurd) 378 ] 379 try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) 380 try(#addr normalize nodelta #ignore #absurd destruct(absurd)) 381 normalize in ignore; destruct(ignore) 382 |2: 383 #classifier_assm' >classifier_assm' % 384 ] 360 whd in ⊢ (% → ?); 361 whd in ⊢ (??%? → ?); 362 whd in match (current_instruction code_memory' status_start); 363 <FETCH generalize in match classify_assm; 364 cases instruction 365 [8: 366 #preinstruction normalize nodelta 367 whd in match ASM_classify0; normalize nodelta 368 #contradiction >contradiction #absurd destruct(absurd) 385 369 ] 370 try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) 371 try(#addr normalize nodelta #ignore #absurd destruct(absurd)) 372 normalize in ignore; destruct(ignore) 386 373 |2: 387 #program_counter_assm >program_counter_assm <Some_lookup_opt_assm 374 -classifier_assm #classifier_assm 375 lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm) 376 <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm; 377 #Some_lookup_opt_assm <Some_lookup_opt_assm 388 378 normalize nodelta #new_recursive_assm >new_recursive_assm 389 379 cut(ticks = \snd (fetch code_memory' … … 415 405 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 416 406 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) 417 qed. *)407 qed. 418 408 419 409 lemma trace_compute_paid_trace_cl_jump: … … 674 664 675 665 let rec block_cost' 676 (code_memory': BitVectorTrie Byte 16) (program_counter': Word) 666 (code_memory': BitVectorTrie Byte 16) (program_counter': Word) (visited: list Word) 677 667 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 678 668 (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter') … … 691 681 (cost_of_block = 0) ≝ 692 682 match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with 693 [ O ⇒ λbase_case. ⊥ 683 [ O ⇒ λbase_case. ⊥ (* XXX: dummy to be inserted here *) 694 684 | S program_size' ⇒ λrecursive_case. 695 685 let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in … … 723 713 | DJNZ src_trgt relative ⇒ λinstr. ticks 724 714 | _ ⇒ λinstr. 725 726 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? 715 ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 727 716 ] (refl …) 728 717 | ACALL addr ⇒ λinstr. 729 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?718 ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 730 719 | AJMP addr ⇒ λinstr. 731 ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ? 720 let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in 721 ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 732 722 | LCALL addr ⇒ λinstr. 733 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? 734 | LJMP addr ⇒ λinstr. ticks 735 | SJMP addr ⇒ λinstr. ticks 723 ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 724 | LJMP addr ⇒ λinstr. 725 let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in 726 ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 727 | SJMP addr ⇒ λinstr. 728 let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in 729 ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 736 730 | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) 737 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?731 ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 738 732 | MOVC src trgt ⇒ λinstr. 739 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?733 ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ? 740 734 ] (refl …)) 741 735 else … … 754 748 ]) 755 749 ]. 756 [1: 750 [2: 751 change with (if to_continue then ? else (? = 0)) 752 >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta 753 @pi2 754 |1: 757 755 cases reachable_program_counter_witness #_ #hyp 758 756 @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) 759 757 @(le_to_lt_to_lt … base_case hyp) 760 |2:761 change with (if to_continue then ? else (? = 0))762 >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta763 @pi2764 758 |3: 765 759 change with (if to_continue then ? else (0 = 0)) … … 769 763 @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) 770 764 destruct % 771 |96,10 2,105:765 |96,108,111: 772 766 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 773 cases(block_cost' ????????? ) -block_cost'767 cases(block_cost' ??????????) -block_cost' 774 768 @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl) 775 769 destruct % 776 770 |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87, 777 90,93 :771 90,93,99,102,105: 778 772 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 779 cases(block_cost' ????????? ) -block_cost'780 @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH …the_trace program_counter_refl)781 destruct%782 |60,61,62,63,64,65,66,67,68 ,69,99,101,100,102:773 cases(block_cost' ??????????) -block_cost' 774 lapply (trace_compute_paid_trace_cl_other ???? reachable_program_counter_witness good_program_witness ? recursive_case ??? FETCH ??? the_trace program_counter_refl) 775 normalize nodelta destruct #assm @assm % 776 |60,61,62,63,64,65,66,67,68: 783 777 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 784 778 @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) 785 779 destruct % 786 |103: 780 ] 781 -block_cost' 782 [63: 787 783 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 788 784 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 799 795 assumption 800 796 ] 801 | 104:797 |64: 802 798 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 803 799 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 817 813 nat_of_bitvector … program_counter'') 818 814 assumption 819 | 106:815 |65: 820 816 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 821 817 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 834 830 assumption 835 831 ] 836 | 107:832 |66: 837 833 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 838 834 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 854 850 nat_of_bitvector … program_counter'') 855 851 assumption 856 | 94,97:852 |53,55: 857 853 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 858 854 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 866 862 assumption 867 863 ] 868 |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73, 869 76,79,82,85,88,91: 864 |54,56: 865 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 866 lapply(good_program_witness program_counter' reachable_program_counter_witness) 867 <FETCH normalize nodelta <instr normalize nodelta 868 try(<real_instruction_refl <instr normalize nodelta) * 869 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 870 @(transitive_le 871 total_program_size 872 ((S program_size') + nat_of_bitvector … program_counter') 873 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 874 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 875 >plus_n_Sm 876 @monotonic_le_plus_r 877 change with ( 878 nat_of_bitvector … program_counter' < 879 nat_of_bitvector … program_counter'') 880 assumption 881 |1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53, 882 55: 870 883 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 871 884 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 876 889 <FETCH normalize nodelta whd in match ltb; normalize nodelta 877 890 >(le_to_leb_true … program_counter_lt') % 878 | 6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,879 92:891 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54, 892 56: 880 893 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 881 894 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 894 907 nat_of_bitvector … program_counter'') 895 908 assumption 896 |95,98: 897 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 898 lapply(good_program_witness program_counter' reachable_program_counter_witness) 899 <FETCH normalize nodelta <instr normalize nodelta 900 try(<real_instruction_refl <instr normalize nodelta) * 901 #pc_pc_lt_hyp' #pc_tps_lt_hyp' 902 @(transitive_le 903 total_program_size 904 ((S program_size') + nat_of_bitvector … program_counter') 905 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 906 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 907 >plus_n_Sm 908 @monotonic_le_plus_r 909 change with ( 910 nat_of_bitvector … program_counter' < 911 nat_of_bitvector … program_counter'') 912 assumption 909 |*: 910 normalize nodelta 911 cases daemon (* XXX: new goals using jump_target *) 913 912 ] 914 913 qed. … … 934 933 λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. 935 934 λgood_program_witness: good_program code_memory total_program_size. ?. 936 cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels935 cases(block_cost' code_memory program_counter [ ] total_program_size total_program_size cost_labels 937 936 reachable_program_counter_witness good_program_witness true ?) 938 937 [1:
Note: See TracChangeset
for help on using the changeset viewer.