Changeset 1710 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 20, 2012, 10:04:54 AM (8 years ago)
Author:
mulligan
Message:

changes from friday afternoon

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1709 r1710  
    474474  #code_memory #start_status #classify_assm
    475475  whd in match execute_1; normalize nodelta
    476   whd in match execute_1'; normalize nodelta
    477   whd in match execute_1_0; normalize nodelta
    478   generalize in match (refl … (fetch code_memory
    479     (program_counter (BitVectorTrie Byte 16) code_memory start_status)));
    480   cases (fetch code_memory
    481     (program_counter (BitVectorTrie Byte 16) code_memory start_status)) in ⊢ (??%? → ?);
    482   #instr_pc #ticks #fetch_rewrite <fetch_rewrite
    483   cases
     476  cases (execute_1' code_memory start_status) #the_status
     477  * #_ #classify_assm' @classify_assm' assumption
    484478qed-.
    485479
     
    572566        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
    573567        [1:
    574           <fetch_twice_fetch_execute_1 <FETCH %
     568          <fetch_twice_fetch_execute_1
     569          [1:
     570            <FETCH %
     571          |2:
     572            >classifier_assm %
     573          ]
    575574        |2:
    576575          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
     
    621620        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
    622621        [1:
    623           <fetch_twice_fetch_execute_1 <FETCH %
     622          <fetch_twice_fetch_execute_1
     623          [1:
     624            <FETCH %
     625          |2:
     626            cases classifier_assm
     627            [1:
     628              whd in ⊢ (% → ?);
     629              whd in ⊢ (??%? → ?);
     630              whd in match (current_instruction code_memory' status_start);
     631              <FETCH generalize in match classify_assm;
     632              cases instruction
     633              [8:
     634                #preinstruction normalize nodelta
     635                whd in match ASM_classify0; normalize nodelta
     636                #contradiction >contradiction #absurd destruct(absurd)
     637              ]
     638              try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
     639              try(#addr normalize nodelta #ignore #absurd destruct(absurd))
     640              normalize in ignore; destruct(ignore)
     641            |2:
     642              #classifier_assm' >classifier_assm' %
     643            ]
     644          ]
    624645        |2:
    625646          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
     
    908929qed.
    909930
     931lemma trace_compute_paid_trace_cl_return:
     932  ∀code_memory' : (BitVectorTrie Byte 16).
     933  ∀program_counter' : Word.
     934  ∀total_program_size : ℕ.
     935  ∀cost_labels : (BitVectorTrie costlabel 16).
     936  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
     937  ∀good_program_witness : (good_program code_memory' total_program_size).
     938  ∀program_size' : ℕ.
     939  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
     940  ∀ticks : ℕ.
     941  ∀instruction : instruction.
     942  ∀program_counter'' : Word.
     943  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     944  ∀start_status : (Status code_memory').
     945  ∀final_status : (Status code_memory').
     946  ∀trace_ends_flag : trace_ends_with_ret.
     947  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     948  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     949  ∀classify_assm: ASM_classify0 instruction = cl_return.
     950    (∃n:ℕ
     951     .trace_any_label_length code_memory' cost_labels trace_ends_flag
     952      start_status final_status the_trace
     953      +S n
     954      =total_program_size)
     955    ∧ticks
     956     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     957      start_status final_status the_trace.
     958  #code_memory' #program_counter' #total_program_size #cost_labels
     959  #reachable_program_counter_witness #good_program_witness #program_size'
     960  #recursive_case #ticks #instruction #program_counter'' #FETCH
     961  #start_status #final_status #trace_ends_flag
     962  #the_trace #program_counter_refl #classify_assm
     963  @(trace_any_label_inv_ind … the_trace)
     964  [1:
     965    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     966    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     967    destruct @⊥
     968  |2:
     969    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     970    #start_status_refl #final_status_refl #the_trace_refl destruct
     971    whd in match (trace_any_label_length … (tal_base_return …));
     972    whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
     973    [1:
     974      %{(pred total_program_size)} whd in ⊢ (??%?);
     975      @S_pred
     976      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     977    |2:
     978      <FETCH %
     979    ]
     980  |3:
     981    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     982    #classifier_assm #after_return_assm #trace_label_return #costed_assm
     983    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     984    destruct @⊥
     985  |4:
     986    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     987    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     988    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     989    #final_status_refl #the_trace_refl
     990    destruct @⊥
     991  |5:
     992    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     993    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     994    #final_status_refl #the_trace_refl destruct @⊥
     995  ]
     996  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     997  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     998  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     999  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     1000  <FETCH in classifier_assm; >classify_assm
     1001  #absurd try (destruct(absurd))
     1002  cases absurd
     1003  #absurd destruct(absurd)
     1004qed.
     1005     
     1006     
    9101007let rec block_cost'
    9111008  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
     
    9491046                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
    9501047          [ RET                    ⇒ λinstr. ticks
     1048          | RETI                   ⇒ λinstr. ticks
    9511049          | JC   relative          ⇒ λinstr. ticks
    9521050          | JNC  relative          ⇒ λinstr. ticks
     
    9901088          ])
    9911089  ].
    992   cases daemon (*
    9931090  [1:
    9941091    cases reachable_program_counter_witness #_ #hyp
     
    10021099    change with (if to_continue then ? else (0 = 0))
    10031100    >p normalize nodelta %
    1004   |98,104,107:
     1101  |7,8:
     1102    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1103    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     1104    destruct %
     1105  |96,102,105:
    10051106    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10061107    cases(block_cost' ?????????) -block_cost'
    10071108    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
    10081109    destruct %
    1009   |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
    1010    92,95:
     1110  |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,
     1111   90,93:
    10111112    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10121113    cases(block_cost' ?????????) -block_cost'
    10131114    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    10141115    destruct %
    1015   |62,63,64,65,66,67,68,69,101,102,103:
     1116  |62,63,64,65,66,67,68,69,99,101,102:
    10161117    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10171118    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    10181119    destruct %
    1019   |96,99:
    1020     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1021     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1022     <FETCH normalize nodelta <instr normalize nodelta *
    1023     #program_counter_lt' #program_counter_lt_tps' %
    1024     [1,3:
    1025       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1026       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1027       >(le_to_leb_true … program_counter_lt') %
    1028     |2,4:
    1029       assumption
    1030     ]
    1031   |105:
     1120  |103:
    10321121    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10331122    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10441133      assumption
    10451134    ]
    1046   |106:
     1135  |104:
    10471136    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10481137    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10621151        nat_of_bitvector … program_counter'')
    10631152    assumption
    1064   |108:
     1153  |106:
    10651154    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10661155    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10791168      assumption
    10801169    ]
    1081   |109:
     1170  |107:
    10821171    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10831172    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10991188        nat_of_bitvector … program_counter'')
    11001189    assumption
    1101   |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
    1102    78,81,84,87,90,93:
     1190  |94,97:
     1191    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1192    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1193    <FETCH normalize nodelta <instr normalize nodelta *
     1194    #program_counter_lt' #program_counter_lt_tps' %
     1195    [1,3:
     1196      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1197      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1198      >(le_to_leb_true … program_counter_lt') %
     1199    |2,4:
     1200      assumption
     1201    ]
     1202  |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73,
     1203   76,79,82,85,88,91:
    11031204    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    11041205    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    11091210    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    11101211    >(le_to_leb_true … program_counter_lt') %
     1212    (* XXX: got to here *)
    11111213  |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,
    11121214   94:
     
    11271229        nat_of_bitvector … program_counter'')
    11281230    assumption
    1129   |10:
    1130     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1131     cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
    1132       reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
    1133     [1:
    1134       #recursive_block_cost #recursive_assm
    1135       @(trace_any_label_inv_ind … the_trace)
    1136       [1:
    1137         #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
    1138         #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1139         destruct @⊥
    1140       |2:
    1141         #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
    1142         #start_status_refl #final_status_refl #the_trace_refl destruct
    1143         whd in match (trace_any_label_length … (tal_base_return …));
    1144         whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
    1145         [1:
    1146           %{(pred total_program_size)} whd in ⊢ (??%?);
    1147           @S_pred
    1148           @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    1149         |2:
    1150           <FETCH %
    1151         ]
    1152       |3:
    1153         #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1154         #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1155         #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1156         destruct @⊥
    1157       |4:
    1158         #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1159         #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1160         #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    1161         #final_status_refl #the_trace_refl
    1162         destruct @⊥
    1163       |5:
    1164         #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    1165         #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    1166         #final_status_refl #the_trace_refl destruct @⊥
    1167       ]
    1168       try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    1169       try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    1170       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1171       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1172       <FETCH in classifier_assm;
    1173       try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
    1174       whd in ⊢ (?(??%?)(??%?) → ?); #absurd
    1175       cases absurd #absurd destruct(absurd)
    1176     |2:
    1177       cases daemon (* XXX: ??? *)
    1178     ]
    11791231  |62,63,64,65,66,67,68,69,70,101,102,103:
    11801232    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     
    12871339        nat_of_bitvector … program_counter'')
    12881340    assumption
    1289   ] *)
     1341  ]
    12901342qed.
    12911343
Note: See TracChangeset for help on using the changeset viewer.