Changeset 1692


Ignore:
Timestamp:
Feb 14, 2012, 1:18:25 PM (6 years ago)
Author:
mulligan
Message:

resolved conflict in asm costs this morning

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1691 r1692  
    600600  #start_status #final_status
    601601  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
    602   #recursive_assm @(trace_any_label_inv_ind … the_trace)
     602  #recursive_assm
     603  @(trace_any_label_inv_ind … the_trace)
    603604    [5:
    604605      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     
    742743  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
    743744  @(trace_any_label_inv_ind … the_trace)
    744   [1:
    745     #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     745  [5:
     746    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     747    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     748    #the_trace_refl destruct @⊥
     749  |1:
     750    #status_start #status_final #execute_assm #classifier_assm #costed_assm
    746751    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    747752    destruct
    748753    whd in match (trace_any_label_length … (tal_base_not_return …));
    749     whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
    750     whd in costed_assm;
    751     generalize in match costed_assm;
    752     generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … start_status')) cost_labels));
    753     generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' start_status')) cost_labels)
    754       in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    755     #lookup_assm cases lookup_assm
     754    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
    756755    [1:
    757       #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
    758       #absurd cases absurd
     756      %{(pred total_program_size)} whd in ⊢ (??%?);
     757      @S_pred
     758      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    759759    |2:
    760       #costlabel #Some_lookup_opt_assm normalize nodelta #ignore %
    761       [2: <FETCH %
    762       | cases daemon ]
     760      <FETCH %
    763761    ]
    764762  |2:
    765     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
    766     #start_status_refl #final_status_refl #the_trace_refl destruct @⊥
     763    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     764    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    767765  |3:
    768766    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    769767    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    770     #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     768    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    771769    destruct @⊥
    772770  |4:
    773771    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    774772    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    775     #costed_assm #trace_any_label_return #trace_ends_flag_refl #start_status_refl
    776     #final_status_refl #the_trace_refl destruct @⊥
    777   |5:
    778     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    779     #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     773    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    780774    #final_status_refl #the_trace_refl destruct @⊥
    781775  ]
     
    805799  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    806800  ∀classify_assm: ASM_classify0 instruction = cl_call.
    807   ∀pi1 : ℕ.
    808   if match lookup_opt costlabel 16 program_counter'' cost_labels with 
    809         [None ⇒ true|Some _ ⇒ false] 
     801  (∀pi1:ℕ
     802  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     803      [None ⇒ true | Some _ ⇒ false] 
    810804   then (∀start_status0:Status code_memory'
    811805             .∀final_status0:Status code_memory'
     
    832826    ∧ticks+pi1
    833827     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    834       start_status final_status the_trace.
     828      start_status final_status the_trace).
    835829  #code_memory' #program_counter' #total_program_size #cost_labels
    836830  #reachable_program_counter_witness #good_program_witness #program_size'
     
    839833  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
    840834  @(trace_any_label_inv_ind … the_trace)
    841   cases daemon
     835  [5:
     836    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     837    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     838    #the_trace_refl destruct @⊥
     839  |1:
     840    #status_start #status_final #execute_assm #classifier_assm #costed_assm
     841    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     842    destruct @⊥
     843  |2:
     844    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     845    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
     846  |3:
     847    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     848    #classifier_assm #after_return_assm #trace_label_return #costed_assm
     849    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     850    destruct
     851    whd in match (trace_any_label_length … (tal_base_call …));
     852    whd in match (compute_paid_trace_any_label … (tal_base_call …));
     853    whd in costed_assm;
     854    generalize in match costed_assm;
     855    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
     856    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
     857      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     858    #lookup_assm cases lookup_assm
     859    [1:
     860      #None_lookup_opt normalize nodelta #absurd cases absurd
     861    |2:
     862      #costlabel #Some_lookup_opt normalize nodelta #ignore
     863      generalize in match recursive_assm;
     864      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
     865      [1:
     866        whd in after_return_assm; <after_return_assm; (* XXX: here *)
     867        cases daemon
     868      |2:
     869        #program_counter_assm >program_counter_assm <Some_lookup_opt
     870        normalize nodelta #new_recursive_assm >new_recursive_assm %
     871        [1:
     872          %{(pred total_program_size)} whd in ⊢ (??%?);
     873          @S_pred
     874          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     875        |2:
     876          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
     877          [1:
     878            <FETCH %
     879          |2:
     880            #ticks_refl_assm >ticks_refl_assm
     881            <plus_n_O %
     882          ]
     883        ]
     884      ]
     885    ]
     886  |4:
     887    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     888    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     889    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     890    #final_status_refl #the_trace_refl destruct
     891    whd in match (trace_any_label_length … (tal_step_call …));
     892    whd in match (compute_paid_trace_any_label … (tal_step_call …));
     893    whd in costed_assm:(?%);
     894    generalize in match costed_assm;
     895    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
     896    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
     897      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     898    #lookup_assm cases lookup_assm
     899    [1:
     900      #None_lookup_opt_assm normalize nodelta #ignore
     901      generalize in match recursive_assm;
     902      cut(program_counter'' = program_counter … status_after_fun_call)
     903      [1:
     904        cases daemon
     905      |2:
     906        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
     907        normalize nodelta #new_recursive_assm %
     908        cases (new_recursive_assm … trace_any_label ?)
     909        [1,3:
     910          #exists_assm #recursive_block_cost_assm
     911          [2:
     912            >recursive_block_cost_assm
     913            @plus_right_monotone
     914            whd in ⊢ (???%); <FETCH %
     915          |1:
     916            (*
     917            cases exists_assm #recursive_n #new_exists_assm
     918            <new_exists_assm
     919           
     920            %
     921            [1:
     922              @(recursive_n - current_instruction_cost … status_pre_fun_call)
     923            |2:
     924             
     925              cut(current_instruction_cost … status_pre_fun_call =
     926                (nat_of_bitvector 16
     927  (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call)
     928  -nat_of_bitvector 16
     929   (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
     930              [1:
     931              |2:
     932                #eq_assm <eq_assm -eq_assm -new_exists_assm -recursive_block_cost_assm
     933                <plus_n_Sm <plus_n_Sm @eq_f
     934                >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?);
     935                >associative_plus @eq_f
     936                <plus_minus_m_m [1: % ]
     937              ]
     938            ] *)
     939            cases daemon
     940          ]
     941        |2,4:
     942          %
     943        ]
     944      ]
     945    |2:
     946      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
     947      cases absurd #absurd cases (absurd I)
     948    ]
     949  ]
     950  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     951  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     952  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     953  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     954  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
     955  #absurd destruct(absurd)
    842956qed.
    843957
     
    9241038          ])
    9251039  ].
     1040  cases daemon (*
    9261041  [1:
    9271042    cases reachable_program_counter_witness #_ #hyp
     
    10421157    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    10431158    >(le_to_leb_true … program_counter_lt') %
    1044   |97,100:
    1045     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1046     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1047     <FETCH normalize nodelta <instr normalize nodelta
    1048     try(<real_instruction_refl <instr normalize nodelta) *
    1049     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    1050     @(transitive_le
    1051       total_program_size
    1052       ((S program_size') + nat_of_bitvector … program_counter')
    1053       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    1054     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    1055     >plus_n_Sm
    1056     @monotonic_le_plus_r
    1057     change with (
    1058       nat_of_bitvector … program_counter' <
    1059         nat_of_bitvector … program_counter'')
    1060     assumption
    10611159  |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,
    10621160   94:
     
    10821180      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
    10831181    [1:
    1084       @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness …
    1085         recursive_case … instruction program_counter' … FETCH)
     1182      #recursive_block_cost #recursive_assm
     1183      @(trace_any_label_inv_ind … the_trace)
     1184      [1:
     1185        #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     1186        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     1187        destruct @⊥
     1188      |2:
     1189        #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     1190        #start_status_refl #final_status_refl #the_trace_refl destruct
     1191        whd in match (trace_any_label_length … (tal_base_return …));
     1192        whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
     1193        [1:
     1194          %{(pred total_program_size)} whd in ⊢ (??%?);
     1195          @S_pred
     1196          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     1197        |2:
     1198          <FETCH %
     1199        ]
     1200      |3:
     1201        #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     1202        #classifier_assm #after_return_assm #trace_label_return #costed_assm
     1203        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     1204        destruct @⊥
     1205      |4:
     1206        #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     1207        #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     1208        #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     1209        #final_status_refl #the_trace_refl
     1210        destruct @⊥
     1211      |5:
     1212        #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     1213        #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     1214        #final_status_refl #the_trace_refl destruct @⊥
     1215      ]
     1216      try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     1217      try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     1218      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     1219      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     1220      <FETCH in classifier_assm;
     1221      try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
     1222      whd in ⊢ (?(??%?)(??%?) → ?); #absurd
     1223      cases absurd #absurd destruct(absurd)
    10861224    |2:
     1225      cases daemon (* XXX: ??? *)
    10871226    ]
    1088   ]
    1089 qed.
    1090  
    1091  
    1092  
    1093  
     1227  |62,63,64,65,66,67,68,69,70,101,102,103:
     1228    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1229    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
     1230      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
     1231    try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %)
     1232    cases daemon (* XXX: ???, same as above case *)
     1233  |96,99:
    10941234    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10951235    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1096     <FETCH normalize nodelta
    1097     <real_instruction_refl <instr normalize nodelta *
    1098     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     1236    <FETCH normalize nodelta <instr normalize nodelta *
     1237    #program_counter_lt' #program_counter_lt_tps' %
     1238    [1,3:
     1239      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1240      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1241      >(le_to_leb_true … program_counter_lt') %
     1242    |2,4:
     1243      assumption
     1244    ]
     1245  |98,104,107:
     1246    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1247    cases(block_cost' ?????????) -block_cost'
     1248    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …)
     1249    destruct %
     1250  |105:
     1251    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1252    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1253    <FETCH normalize nodelta <instr normalize nodelta
     1254    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     1255    * * * * #n'
     1256    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     1257    %
     1258    [1:
     1259      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1260      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1261      >(le_to_leb_true … program_counter_lt') %
     1262    |2:
     1263      assumption
     1264    ]
     1265  |106:
     1266    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1267    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1268    <FETCH normalize nodelta <instr normalize nodelta
     1269    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     1270    * * * * #n'
     1271    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    10991272    @(transitive_le
    11001273      total_program_size
     
    11081281        nat_of_bitvector … program_counter'')
    11091282    assumption
    1110   |4:
    1111     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1112     cases(block_cost' ??? ? ?????) -block_cost'
    1113     #recursive_block_cost #recursive_assm
    1114     @(trace_any_label_inv_ind … the_trace)
    1115     [1:
    1116       #status_start #status_final #execute_assm #classifier_assm #costed_assm
    1117       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1118       destruct
    1119       whd in match (trace_any_label_length … (tal_base_not_return …));
    1120       whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
    1121       whd in costed_assm;
    1122     |2:
    1123       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
    1124       #start_status_refl #final_status_refl #the_trace_assm destruct
    1125       whd in classifier_assm;
    1126       whd in classifier_assm:(??%?);
    1127       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1128       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1129       @⊥ <FETCH in classifier_assm; normalize nodelta
    1130       #absurd destruct(absurd)
    1131     |3:
    1132       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1133       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1134       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1135       destruct
    1136       whd in classifier_assm;
    1137       whd in classifier_assm:(??%?);
    1138       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1139       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1140       @⊥ <FETCH in classifier_assm; normalize nodelta
    1141       #absurd destruct(absurd)
    1142     |4:
    1143       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1144       #status_final #execute_assm #classifier_assm #after_return_assm
    1145       #trace_label_return #costed_assm #trace_any_label #ends_flag_refl
    1146       #start_status_refl #final_status_refl #the_trace_refl
    1147       destruct
    1148       whd in classifier_assm;
    1149       whd in classifier_assm:(??%?);
    1150       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1151       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1152       @⊥ <FETCH in classifier_assm; normalize nodelta
    1153       #absurd destruct(absurd)
    1154     ]
    1155    
    1156    
    1157    
    1158    
    1159    
    1160    
    1161    
    1162    
    1163    
    1164    
    1165    
    1166    
    1167    
    1168    
    1169    
    1170    
    1171    
    1172    
    1173    
    1174    
    1175    
    1176    
    1177    
    1178    
    1179    
    1180    
    1181    
    1182    
    1183    
    1184     |3:
    1185       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1186       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1187       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1188       destruct
    1189       whd in match (compute_paid_trace_any_label … (tal_base_call …));
    1190       whd in match (trace_any_label_length … (tal_base_call …));
    1191       cases(recursive_assm …
    1192         (tal_base_call (ASM_abstract_status code_memory' cost_labels)
    1193          status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …)
    1194          classifier_assm after_return_assm trace_label_return costed_assm) ?)
    1195       [1:
    1196         * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
    1197         [1:
    1198           %{(pred total_program_size)}
    1199           whd in ⊢ (??%?);
    1200           >S_pred [1: % ]
    1201           <recursive_trace_total
    1202           @lt_O_S
    1203         |2:
    1204           >recursive_block_cost_assm
    1205           whd in ⊢ (??(??%)?); <FETCH
    1206           (* XXX: ??? *)
    1207         ]
    1208       |2:
    1209         cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call))))
    1210         [1:
    1211           cases FETCH %
    1212         |2:
    1213           #program_counter_hyp'' >program_counter_hyp''
    1214           whd in after_return_assm; <after_return_assm
    1215           whd in match (current_instruction_cost status_pre_fun_call);
    1216           @fetch_half_add
    1217         ]
    1218       ]
    1219     |4:
    1220       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1221       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1222       #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    1223       #final_status_refl #the_trace_refl
    1224       generalize in match execute_assm; destruct #execute_assm
    1225       whd in match (compute_paid_trace_any_label … (tal_step_call …));
    1226       whd in match (trace_any_label_length … (tal_step_call …));
    1227       cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
    1228       [1:
    1229         * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
    1230         [1:
    1231           <recursive_trace_total %
    1232           [1:
    1233             @(recursive_n - (current_instruction_cost status_pre_fun_call))
    1234           |2:
    1235             whd in after_return_assm; cases after_return_assm
    1236             >half_add_minus_right in ⊢ (??%?);
    1237             >commutative_plus in ⊢ (???%);
    1238             >commutative_plus in ⊢ (??%?);
    1239             <associative_plus in ⊢ (??%?);
    1240             @plus_right_monotone
    1241             cut(current_instruction_cost status_pre_fun_call ≤ recursive_n)
    1242             [1:
    1243               (* XXX: ??? *)
    1244             |2:
    1245               #current_instruction_cost_assm
    1246               <minus_Sn_m in ⊢ (??%?); [2: assumption ]
    1247               >minus_plus_cancel [1: % ]
    1248               @le_S assumption
    1249             ]
    1250           ]
    1251         |2:
    1252           >recursive_block_cost_assm
    1253           @plus_right_monotone
    1254           whd in match (current_instruction_cost status_pre_fun_call);
    1255           <FETCH %
    1256         ]
    1257      
    1258       |2:
    1259         lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
    1260         #hyp cases (hyp trace_label_return)
    1261         @as_execute_preserves_code_memory whd %
    1262       |3:
    1263         cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
    1264         [1:
    1265           cases FETCH %
    1266         |2:
    1267           #program_counter_hyp'' >program_counter_hyp''
    1268           whd in after_return_assm; <after_return_assm
    1269           whd in match (current_instruction_cost status_pre_fun_call);
    1270           @fetch_half_add
    1271         ]
    1272       ]
    1273     |5:
    1274       #end_flag #status_pre #status_init #status_end #execute_assm #the_trace'
    1275       #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    1276       #final_status_refl #trace_refl
    1277       generalize in match the_trace; destruct #the_trace
    1278       whd in classifier_assm;
    1279       whd in classifier_assm:(??%?);
    1280       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1281       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1282       @⊥ <FETCH in classifier_assm; normalize nodelta
    1283       #absurd destruct(absurd)
    1284     ]
    1285   |7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61,
    1286     64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107:
    1287     cases daemon (* XXX: massive terms *)
    1288   |2:
    1289     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1290     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1291     <FETCH normalize nodelta <instr normalize nodelta
    1292     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1293     cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    1294     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1295     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1296     #_ #_ #program_counter_lt' #program_counter_lt_tps'     
    1297     @(transitive_le
    1298       total_program_size
    1299       ((S program_size') + nat_of_bitvector … program_counter')
    1300       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    1301     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    1302     >plus_n_Sm
    1303     @monotonic_le_plus_r
    1304     change with (
    1305       nat_of_bitvector … program_counter' <
    1306         nat_of_bitvector … program_counter'')
    1307     assumption
    1308   |3:
     1283  |108:
    13091284    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    13101285    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    13231298      assumption
    13241299    ]
    1325   |5:
     1300  |109:
    13261301    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    13271302    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1328       <FETCH normalize nodelta <instr normalize nodelta
    1329     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1330     * * * * #n'
    1331     #_ #_ #program_counter_lt' #program_counter_lt_tps'     
     1303    <FETCH normalize nodelta <instr normalize nodelta
     1304    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     1305    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     1306    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     1307    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     1308    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    13321309    @(transitive_le
    13331310      total_program_size
     
    13411318        nat_of_bitvector … program_counter'')
    13421319    assumption
    1343   |6:
    1344     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1345     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1346       <FETCH normalize nodelta <instr normalize nodelta
    1347     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1348     * * * * #n'
    1349     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1350     %
    1351     [1:
    1352       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1353       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1354       >(le_to_leb_true … program_counter_lt') %
    1355     |2:
    1356       assumption
    1357     ]
    1358   |11,14: (* JMP and MOVC *)
     1320  |97,100:
    13591321    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    13601322    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    13731335        nat_of_bitvector … program_counter'')
    13741336    assumption
    1375   |12,15:
    1376     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1377     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1378     <FETCH normalize nodelta <instr normalize nodelta *
    1379     #program_counter_lt' #program_counter_lt_tps' %
    1380     [1,3:
    1381       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1382       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1383       >(le_to_leb_true … program_counter_lt') %
    1384     |2,4:
    1385       assumption
    1386     ]
    1387   |17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98,
    1388    102,105:
    1389     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1390     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1391     <FETCH normalize nodelta
    1392     <real_instruction_refl <instr normalize nodelta *
    1393     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    1394     @(transitive_le
    1395       total_program_size
    1396       ((S program_size') + nat_of_bitvector … program_counter')
    1397       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    1398     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    1399     >plus_n_Sm
    1400     @monotonic_le_plus_r
    1401     change with (
    1402       nat_of_bitvector … program_counter' <
    1403         nat_of_bitvector … program_counter'')
    1404     assumption
    1405   |18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78,
    1406     81,84,87,90,93,96,99,103,106:
    1407     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1408     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1409     <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    1410     #program_counter_lt' #program_counter_lt_tps' %
    1411     try assumption
    1412     [*:
    1413       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1414       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1415       >(le_to_leb_true … program_counter_lt') %
    1416     ]
    1417   [1:
    1418     #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
    1419     cases(block_cost' ?????? ?? ?) -block_cost'
    1420     #recursive_block_cost #recursive_assm
    1421     @(trace_any_label_inv_ind … the_trace)
    1422     [1:
    1423       #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
    1424       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
    1425       cases classifier_assm
    1426       whd in match (as_classifier ? ? ?);
    1427       whd in ⊢ (??%? → ?);
    1428       whd in match current_instruction; normalize nodelta
    1429       whd in match current_instruction0; normalize nodelta
    1430       #absurd @⊥ >p1 in absurd; normalize nodelta
    1431       #absurd destruct(absurd)
    1432     |2:
    1433       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
    1434       #start_status_refl #final_status_refl #the_trace_assm destruct
    1435       whd in classifier_assm;
    1436       whd in classifier_assm:(??%?);
    1437       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1438       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1439       @⊥
    1440       >p1 in classifier_assm; normalize nodelta
    1441       #absurd destruct(absurd)
    1442     |3:
    1443       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1444       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1445       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1446       destruct
    1447       cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
    1448         (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
    1449           (execute_1 status_pre_fun_call) status_final
    1450           (refl Status (execute_1 status_pre_fun_call)) classifier_assm
    1451           after_return_assm trace_label_return costed_assm) ? ?)
    1452       [2: %
    1453       |3:
    1454       |1:
    1455       ]
    1456     |4:
    1457       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1458       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1459       #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
    1460       #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
    1461     |5:
    1462       #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
    1463       #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
    1464       #the_trace_refl -the_trace_refl destruct
    1465       whd in classifier_assm;
    1466       whd in classifier_assm:(??%?);
    1467       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1468       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1469       @⊥ >p1 in classifier_assm; normalize nodelta
    1470       #absurd destruct(absurd)
    1471     ]
    1472   [1:
    1473     #start_status #final_status #trace_ends_flag #the_trace
    1474     #code_memory_refl #program_counter_refl
    1475     cases(block_cost' ?????? ?? ?) -block_cost'
    1476     #recursive_block_cost #recursive_assm
    1477     @(trace_any_label_inv_ind … the_trace)
    1478     [1:
    1479       #start_status' #final_status' #execute_assm #not_return_assm
    1480       #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
    1481       #the_trace_assm
    1482       cases daemon (* XXX: bug in notion of traces here *)
    1483     |2:
    1484 
    1485     |3:
    1486       cases daemon (* XXX *)
    1487     |4:
    1488     ]
    1489   |108:
    1490     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1491     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1492     <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    1493     #program_counter_lt' #program_counter_lt_tps' %
    1494     try assumption
    1495     [*:
    1496       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1497       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1498       >(le_to_leb_true … program_counter_lt') %
    1499     ]
    1500   [1:
    1501     cases reachable_program_counter_witness #_ #hyp
    1502     @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    1503     @(le_to_lt_to_lt … base_case hyp)
    1504   |2:
    1505     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1506     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1507       <FETCH normalize nodelta <instr normalize nodelta
    1508     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1509     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    1510     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1511     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1512     #_ #_ #program_counter_lt' #program_counter_lt_tps'     
    1513     @(transitive_le
    1514       total_program_size
    1515       ((S program_size') + nat_of_bitvector … program_counter)
    1516       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    1517     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    1518     >plus_n_Sm
    1519     @monotonic_le_plus_r
    1520     change with (
    1521       nat_of_bitvector … program_counter <
    1522         nat_of_bitvector … program_counter')
    1523     assumption
    1524   |3:
    1525     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1526     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1527       <FETCH normalize nodelta <instr normalize nodelta
    1528     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1529     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    1530     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1531     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1532     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1533     %
    1534     [1:
    1535       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1536       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1537       >(le_to_leb_true … program_counter_lt') %
    1538     |2:
    1539       assumption
    1540     ]
    1541   |4:
    1542     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1543     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1544       <FETCH normalize nodelta <instr normalize nodelta
    1545     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1546     * * * * #n'
    1547     #_ #_ #program_counter_lt' #program_counter_lt_tps'     
    1548     @(transitive_le
    1549       total_program_size
    1550       ((S program_size') + nat_of_bitvector … program_counter)
    1551       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    1552     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    1553     >plus_n_Sm
    1554     @monotonic_le_plus_r
    1555     change with (
    1556       nat_of_bitvector … program_counter <
    1557         nat_of_bitvector … program_counter')
    1558     assumption
    1559   |5:
    1560     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1561     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1562       <FETCH normalize nodelta <instr normalize nodelta
    1563     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1564     * * * * #n'
    1565     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1566     %
    1567     [1:
    1568       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1569       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1570       >(le_to_leb_true … program_counter_lt') %
    1571     |2:
    1572       assumption
    1573     ]
    1574   |6,8: (* JMP and MOVC *)
    1575     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1576     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1577     <FETCH normalize nodelta <instr normalize nodelta
    1578     try(<real_instruction_refl <instr normalize nodelta) *
    1579     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    1580     @(transitive_le
    1581       total_program_size
    1582       ((S program_size') + nat_of_bitvector … program_counter)
    1583       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    1584     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    1585     >plus_n_Sm
    1586     @monotonic_le_plus_r
    1587     change with (
    1588       nat_of_bitvector … program_counter <
    1589         nat_of_bitvector … program_counter')
    1590     assumption
    1591   |7,9:
    1592     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1593     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1594     <FETCH normalize nodelta <instr normalize nodelta *
    1595     #program_counter_lt' #program_counter_lt_tps' %
    1596     [1,3:
    1597       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1598       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1599       >(le_to_leb_true … program_counter_lt') %
    1600     |2,4:
    1601       assumption
    1602     ]
    1603   |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
    1604     55,57,59,61,63:
    1605     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1606     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1607     <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    1608     #program_counter_lt' #program_counter_lt_tps' %
    1609     try assumption
    1610     [*:
    1611       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1612       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1613       >(le_to_leb_true … program_counter_lt') %
    1614     ]
    1615   |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
    1616     54,56,58,60,62:
    1617     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1618     lapply(good_program_witness program_counter reachable_program_counter_witness)
    1619     <FETCH normalize nodelta
    1620     <real_instruction_refl <instr normalize nodelta *
    1621     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    1622     @(transitive_le
    1623       total_program_size
    1624       ((S program_size') + nat_of_bitvector … program_counter)
    1625       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    1626     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    1627     >plus_n_Sm
    1628     @monotonic_le_plus_r
    1629     change with (
    1630       nat_of_bitvector … program_counter <
    1631         nat_of_bitvector … program_counter')
    1632     assumption
    1633   ]
     1337  ] *)
    16341338qed.
    16351339
  • src/ASM/CostsProof.ma

    r1658 r1692  
    1313
    1414definition current_instruction ≝
    15   λs: Status.
    16     current_instruction0 (code_memory … s) (program_counter … s).
     15  λcm.
     16  λs: Status cm.
     17    current_instruction0 cm (program_counter … s).
    1718
    1819definition ASM_classify0: instruction → status_class ≝
     
    4243   ].
    4344
    44 definition ASM_classify: Status → status_class ≝
    45   λs: Status.
    46     ASM_classify0 (current_instruction s).
     45definition ASM_classify: ∀cm. Status cm → status_class ≝
     46  λcm.
     47  λs: Status cm.
     48    ASM_classify0 (current_instruction cm s).
    4749
    4850definition current_instruction_is_labelled ≝
     51  λcm.
    4952  λcost_labels: BitVectorTrie costlabel 16.
    50   λs: Status.
    51   let pc ≝ program_counter s in
     53  λs: Status cm.
     54  let pc ≝ program_counter ? cm s in
    5255    match lookup_opt … pc cost_labels with
    5356    [ None ⇒ False
     
    5659
    5760definition next_instruction_properly_relates_program_counters ≝
    58   λbefore: Status.
    59   λafter : Status.
    60   let size ≝ current_instruction_cost before in
    61   let pc_before ≝ program_counter … before in
    62   let pc_after ≝ program_counter … after in
     61  λcm.
     62  λbefore: Status cm.
     63  λafter : Status cm.
     64  let size ≝ current_instruction_cost cm before in
     65  let pc_before ≝ program_counter … cm before in
     66  let pc_after ≝ program_counter … cm after in
    6367  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    6468    sum = pc_after.
    6569
    66 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    67  λcost_labels.
     70definition ASM_abstract_status: ∀cm. BitVectorTrie costlabel 16 → abstract_status ≝
     71  λcm.
     72  λcost_labels.
    6873  mk_abstract_status
    69    Status
    70    (λs,s'. (execute_1 s) = s')
    71    (λs,class. ASM_classify s = class)
    72    (current_instruction_is_labelled cost_labels)
    73    next_instruction_properly_relates_program_counters.
     74   (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).
    7479
    7580let rec compute_max_trace_label_label_cost
     81  (cm: ?)
    7682  (cost_labels: BitVectorTrie costlabel 16)
    7783   (trace_ends_flag: trace_ends_with_ret)
    78     (start_status: Status) (final_status: Status)
    79       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     84    (start_status: Status cm) (final_status: Status cm)
     85      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    8086        start_status final_status) on the_trace: nat ≝
    8187  match the_trace with
     
    8490  ]
    8591and compute_max_trace_any_label_cost
     92  (cm: ?)
    8693  (cost_labels: BitVectorTrie costlabel 16)
    8794  (trace_ends_flag: trace_ends_with_ret)
    88    (start_status: Status) (final_status: Status)
    89      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     95   (start_status: Status cm) (final_status: Status cm)
     96     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    9097       on the_trace: nat ≝
    9198  match the_trace with
    9299  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    93100  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     101  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     102      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     103      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     104        call_trace_cost + current_instruction_cost
    94105  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    95      _ _ _ call_trace final_trace ⇒
    96       let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     106     _ _ _ call_trace _ final_trace ⇒
     107      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
    97108      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    98109      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    99110        call_trace_cost + current_instruction_cost + final_trace_cost
    100111  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    101       let current_instruction_cost ≝ current_instruction_cost status_pre in
     112      let current_instruction_cost ≝ current_instruction_cost cm status_pre in
    102113      let tail_trace_cost ≝
    103114       compute_max_trace_any_label_cost cost_labels end_flag
     
    107118  ]
    108119and compute_max_trace_label_return_cost
    109   (cost_labels: BitVectorTrie costlabel 16)
    110   (start_status: Status) (final_status: Status)
    111     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     120  (cm: ?)
     121  (cost_labels: BitVectorTrie costlabel 16)
     122  (start_status: Status cm) (final_status: Status cm)
     123    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    112124      on the_trace: nat ≝
    113125  match the_trace with
     
    575587qed.
    576588   
    577 
    578589let rec block_cost_trace_any_label_static_dynamic_ok
    579590  (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
Note: See TracChangeset for help on using the changeset viewer.