Changeset 1709 for src/ASM/ASMCosts.ma
- Timestamp:
- Feb 17, 2012, 11:52:36 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1697 r1709 331 331 qed. 332 332 333 (* XXX: todo *) 333 334 lemma subaddressing_mode_elim': 334 335 ∀T: Type[2]. … … 349 350 qed. 350 351 352 (* XXX: todo *) 351 353 axiom subaddressing_mode_elim: 352 354 ∀T: Type[2]. … … 360 362 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 361 363 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 362 363 definition current_instruction0 ≝364 λcode_memory: BitVectorTrie Byte 16.365 λprogram_counter: Word.366 \fst (\fst (fetch … code_memory program_counter)).367 368 definition current_instruction ≝369 λcode_memory.370 λs: Status code_memory.371 current_instruction0 code_memory (program_counter … s).372 373 definition ASM_classify0: instruction → status_class ≝374 λi: instruction.375 match i with376 [ RealInstruction pre ⇒377 match pre with378 [ RET ⇒ cl_return379 | JZ _ ⇒ cl_jump380 | JNZ _ ⇒ cl_jump381 | JC _ ⇒ cl_jump382 | JNC _ ⇒ cl_jump383 | JB _ _ ⇒ cl_jump384 | JNB _ _ ⇒ cl_jump385 | JBC _ _ ⇒ cl_jump386 | CJNE _ _ ⇒ cl_jump387 | DJNZ _ _ ⇒ cl_jump388 | _ ⇒ cl_other389 ]390 | ACALL _ ⇒ cl_call391 | LCALL _ ⇒ cl_call392 | JMP _ ⇒ cl_call393 | AJMP _ ⇒ cl_jump394 | LJMP _ ⇒ cl_jump395 | SJMP _ ⇒ cl_jump396 | _ ⇒ cl_other397 ].398 399 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝400 λcode_memory.401 λs: Status code_memory.402 ASM_classify0 (current_instruction … s).403 364 404 365 definition current_instruction_is_labelled ≝ … … 505 466 506 467 (* XXX: indexing bug *) 507 examplefetch_twice_fetch_execute_1:468 lemma fetch_twice_fetch_execute_1: 508 469 ∀code_memory: BitVectorTrie Byte 16. 509 470 ∀start_status: Status code_memory. 471 ASM_classify code_memory start_status = cl_other → 510 472 \snd (\fst (fetch code_memory (program_counter … start_status))) = 511 473 program_counter … (execute_1 … start_status). 512 cases daemon 513 qed. 474 #code_memory #start_status #classify_assm 475 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 484 qed-. 514 485 515 486 lemma reachable_program_counter_to_0_lt_total_program_size:
Note: See TracChangeset
for help on using the changeset viewer.