Changeset 1711 for src/ASM/ASMCosts.ma
- Timestamp:
- Feb 20, 2012, 11:15:52 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1710 r1711 1114 1114 @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) 1115 1115 destruct % 1116 |6 2,63,64,65,66,67,68,69,99,101,102:1116 |60,61,62,63,64,65,66,67,68,69,99,101,100,102: 1117 1117 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1118 1118 @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) … … 1211 1211 >(le_to_leb_true … program_counter_lt') % 1212 1212 (* XXX: got to here *) 1213 |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,1214 9 4:1213 |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, 1214 92: 1215 1215 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1216 1216 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 1229 1229 nat_of_bitvector … program_counter'') 1230 1230 assumption 1231 |62,63,64,65,66,67,68,69,70,101,102,103: 1232 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1233 cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels 1234 reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost' 1235 try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %) 1236 cases daemon (* XXX: ???, same as above case *) 1237 |96,99: 1238 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1239 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1240 <FETCH normalize nodelta <instr normalize nodelta * 1241 #program_counter_lt' #program_counter_lt_tps' % 1242 [1,3: 1243 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1244 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1245 >(le_to_leb_true … program_counter_lt') % 1246 |2,4: 1247 assumption 1248 ] 1249 |98,104,107: 1250 #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 1251 cases(block_cost' ?????????) -block_cost' 1252 @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …) 1253 destruct % 1254 |105: 1255 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1256 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1257 <FETCH normalize nodelta <instr normalize nodelta 1258 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1259 * * * * #n' 1260 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1261 % 1262 [1: 1263 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1264 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1265 >(le_to_leb_true … program_counter_lt') % 1266 |2: 1267 assumption 1268 ] 1269 |106: 1270 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1271 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1272 <FETCH normalize nodelta <instr normalize nodelta 1273 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1274 * * * * #n' 1275 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1276 @(transitive_le 1277 total_program_size 1278 ((S program_size') + nat_of_bitvector … program_counter') 1279 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 1280 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 1281 >plus_n_Sm 1282 @monotonic_le_plus_r 1283 change with ( 1284 nat_of_bitvector … program_counter' < 1285 nat_of_bitvector … program_counter'') 1286 assumption 1287 |108: 1288 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1289 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1290 <FETCH normalize nodelta <instr normalize nodelta 1291 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1292 cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta 1293 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1294 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1295 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1296 % 1297 [1: 1298 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1299 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1300 >(le_to_leb_true … program_counter_lt') % 1301 |2: 1302 assumption 1303 ] 1304 |109: 1305 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1306 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1307 <FETCH normalize nodelta <instr normalize nodelta 1308 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1309 cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta 1310 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1311 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1312 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1313 @(transitive_le 1314 total_program_size 1315 ((S program_size') + nat_of_bitvector … program_counter') 1316 (program_size' + nat_of_bitvector … program_counter'') recursive_case) 1317 normalize in match (S program_size' + nat_of_bitvector … program_counter'); 1318 >plus_n_Sm 1319 @monotonic_le_plus_r 1320 change with ( 1321 nat_of_bitvector … program_counter' < 1322 nat_of_bitvector … program_counter'') 1323 assumption 1324 |97,100: 1231 |95,98: 1325 1232 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1326 1233 lapply(good_program_witness program_counter' reachable_program_counter_witness) … … 1341 1248 ] 1342 1249 qed. 1343 1344 (*1345 (code_memory': BitVectorTrie Byte 16) (program_counter': Word)1346 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)1347 (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')1348 (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)1349 on program_size:1350 total_program_size ≤ program_size + nat_of_bitvector … program_counter' →1351 Σcost_of_block: nat.1352 if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then1353 ∀start_status: Status code_memory'.1354 ∀final_status: Status code_memory'.1355 ∀trace_ends_flag.1356 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.1357 program_counter' = program_counter … start_status →1358 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧1359 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace1360 else1361 (cost_of_block = 0)1362 *)1363 1250 1364 1251 definition block_cost:
Note: See TracChangeset
for help on using the changeset viewer.