Changeset 1709 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 17, 2012, 11:52:36 AM (8 years ago)
Author:
mulligan
Message:

Changes to the execution of the MOVC instruction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1697 r1709  
    331331qed.
    332332
     333(* XXX: todo *)
    333334lemma subaddressing_mode_elim':
    334335  ∀T: Type[2].
     
    349350qed.
    350351
     352(* XXX: todo *)
    351353axiom subaddressing_mode_elim:
    352354  ∀T: Type[2].
     
    360362    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    361363      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 with
    376    [ RealInstruction pre ⇒
    377      match pre with
    378       [ RET ⇒ cl_return
    379       | JZ _ ⇒ cl_jump
    380       | JNZ _ ⇒ cl_jump
    381       | JC _ ⇒ cl_jump
    382       | JNC _ ⇒ cl_jump
    383       | JB _ _ ⇒ cl_jump
    384       | JNB _ _ ⇒ cl_jump
    385       | JBC _ _ ⇒ cl_jump
    386       | CJNE _ _ ⇒ cl_jump
    387       | DJNZ _ _ ⇒ cl_jump
    388       | _ ⇒ cl_other
    389       ]
    390    | ACALL _ ⇒ cl_call
    391    | LCALL _ ⇒ cl_call
    392    | JMP _ ⇒ cl_call
    393    | AJMP _ ⇒ cl_jump
    394    | LJMP _ ⇒ cl_jump
    395    | SJMP _ ⇒ cl_jump
    396    | _ ⇒ cl_other
    397    ].
    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).
    403364
    404365definition current_instruction_is_labelled ≝
     
    505466
    506467(* XXX: indexing bug *)
    507 example fetch_twice_fetch_execute_1:
     468lemma fetch_twice_fetch_execute_1:
    508469  ∀code_memory: BitVectorTrie Byte 16.
    509470  ∀start_status: Status code_memory.
     471    ASM_classify code_memory start_status = cl_other →
    510472    \snd (\fst (fetch code_memory (program_counter … start_status))) =
    511473      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
     484qed-.
    514485
    515486lemma reachable_program_counter_to_0_lt_total_program_size:
Note: See TracChangeset for help on using the changeset viewer.