Changeset 1548 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 23, 2011, 11:15:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1544 r1548 43 43  _ ⇒ True 44 44 ]. 45 46 definition current_instruction_cost ≝47 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).48 45 49 46 definition next_instruction_properly_relates_program_counters ≝ … … 251 248 ]. 252 249 250 (*Useless now? 253 251 (* To be moved *) 254 252 lemma pred_minus_1: … … 278 276 S m = m + 1. 279 277 // 280 qed. 278 qed.*) 281 279 282 280 include alias "arithmetics/nat.ma". 283 281 282 (*Useless now? 284 283 lemma minus_m_n_minus_minus_plus_1: 285 284 ∀m, n: nat. … … 304 303 (m  n) + (n  o) = m  o. 305 304 /2 by plus_minus_rearrangement_1/ 306 qed. 307 308 lemma current_instruction_cost_is_ok: 309 ∀s: Status. 310 current_instruction_cost s = clock … (execute 1 s)  clock … s. 311 #s 312 change with (execute_1 s) in match (eject … (execute 1 s)); 313 change with ( 314 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 315 (program_counter (BitVectorTrie Byte 16) s) 316 in 317 eject … (execute_1_0 s instr_pc_ticks)) in match (eject … (execute_1 s)); 318 change with ( 319 \snd (fetch (code_memory … s) (program_counter … s))) in ⊢ (??%?); 320 normalize nodelta; 321 whd in match ( 322 execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) 323 (program_counter (BitVectorTrie Byte 16) s))); 324 normalize nodelta; 325 cases (fetch (code_memory (BitVectorTrie Byte 16) s) 326 (program_counter (BitVectorTrie Byte 16) s)); 327 #instr_pc #ticks normalize nodelta; 328 cases (\fst instr_pc) 329 [1: 330 #addr11 normalize nodelta; 331 cases addr11 #addressing_mode 332 cases addressing_mode 333 [1,2,3,4,8,9,15,16,17,19: 334 #assm whd in ⊢ (% → ?) 335 #absurd cases(absurd) 336 5,6,7,10,11,12,13,14: 337 whd in ⊢ (% → ?) 338 #absurd cases(absurd) 339 18: 340 #word11 #irrelevant normalize nodelta; 341 >set_program_counter_ignores_clock 342 >write_at_stack_pointer_ignores_clock 343 >set_8051_sfr_ignores_clock 344 >write_at_stack_pointer_ignores_clock 345 >set_8051_sfr_ignores_clock 346 >clock_set_clock 347 >set_program_counter_ignores_clock 348 >commutative_plus 349 <plus_minus 350 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 351 % 352 ] 353 2: 354 #addr16 cases addr16 #addressing_mode 355 normalize nodelta; cases addressing_mode 356 normalize nodelta; 357 [1,2,3,4,8,9,15,16,17,18: 358 #assm whd in ⊢ (% → ?) 359 #absurd cases(absurd) 360 5,6,7,10,11,12,13,14: 361 whd in ⊢ (% → ?) 362 #absurd cases(absurd) 363 19: 364 #addr16 #irrelevant 365 normalize nodelta; 366 >set_program_counter_ignores_clock 367 >write_at_stack_pointer_ignores_clock 368 >set_8051_sfr_ignores_clock 369 >write_at_stack_pointer_ignores_clock 370 >set_8051_sfr_ignores_clock 371 >clock_set_clock 372 >set_program_counter_ignores_clock 373 >commutative_plus 374 <plus_minus 375 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 376 % 377 ] 378 3: 379 #addr11 cases addr11 #addressing_mode 380 normalize nodelta; cases addressing_mode 381 normalize nodelta; 382 [1,2,3,4,8,9,15,16,17,19: 383 #assm whd in ⊢ (% → ?) 384 #absurd cases(absurd) 385 5,6,7,10,11,12,13,14: 386 whd in ⊢ (% → ?) 387 #absurd cases(absurd) 388 18: 389 #word11 #irrelevant 390 normalize nodelta; 391 >set_program_counter_ignores_clock 392 >clock_set_clock 393 >set_program_counter_ignores_clock 394 >commutative_plus 395 <plus_minus 396 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 397 % 398 ] 399 4: 400 #addr16 cases addr16 #addressing_mode 401 normalize nodelta; cases addressing_mode 402 normalize nodelta; 403 [1,2,3,4,8,9,15,16,17,18: 404 #assm whd in ⊢ (% → ?) 405 #absurd cases(absurd) 406 5,6,7,10,11,12,13,14: 407 whd in ⊢ (% → ?) 408 #absurd cases(absurd) 409 19: 410 #word #irrelevant 411 normalize nodelta; 412 >set_program_counter_ignores_clock 413 >clock_set_clock 414 >set_program_counter_ignores_clock 415 >commutative_plus 416 <plus_minus 417 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 418 % 419 ] 420 5: 421 #relative cases relative #addressing_mode 422 normalize nodelta; cases addressing_mode 423 normalize nodelta; 424 [1,2,3,4,8,9,15,16,18,19: 425 #assm whd in ⊢ (% → ?) 426 #absurd cases(absurd) 427 5,6,7,10,11,12,13,14: 428 whd in ⊢ (% → ?) 429 #absurd cases(absurd) 430 17: 431 #byte #irrelevant 432 normalize nodelta; 433 >set_program_counter_ignores_clock 434 >set_program_counter_ignores_clock 435 >clock_set_clock 436 >commutative_plus 437 <plus_minus 438 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 439 % 440 ] 441 6: 442 #indirect_dptr cases indirect_dptr #addressing_mode 443 normalize nodelta; cases addressing_mode 444 normalize nodelta; 445 [1,2,3,4,8,9,15,16,17,18,19: 446 #assm whd in ⊢ (% → ?) 447 #absurd cases(absurd) 448 5,6,7,10,11,12,14: 449 whd in ⊢ (% → ?) 450 #absurd cases(absurd) 451 13: 452 #irrelevant 453 normalize nodelta; 454 >set_program_counter_ignores_clock 455 >set_program_counter_ignores_clock 456 >clock_set_clock 457 >commutative_plus 458 <plus_minus 459 <(minus_n_n (clock (BitVectorTrie Byte 16) s)) 460 % 461 ] 462 7: 463 #acc_a cases acc_a #addressing_mode 464 normalize nodelta; cases addressing_mode 465 normalize nodelta; 466 [1,2,3,4,8,9,15,16,17,18,19: 467 #assm whd in ⊢ (% → ?) 468 #absurd cases(absurd) 469 6,7,10,11,12,13,14: 470 whd in ⊢ (% → ?) 471 #absurd cases(absurd) 472 5: 473 #irrelevant #acc_dptr_acc_pc 474 normalize nodelta; 475 cases daemon (* XXX: todo *) 476 ] 477 8: cases daemon (* XXX: todo *) 478 ] 479 qed. 305 qed.*) 480 306 481 307 let rec compute_max_trace_label_label_cost_is_ok
Note: See TracChangeset
for help on using the changeset viewer.