include "common/StructuredTraces.ma". (* includes "basics/lists/listb.ma".*)

include "ASM/Status.ma". (* includes "ASM/ASM.ma". *)
include "ASM/Fetch.ma".

definition ASM_classify00: ∀a. preinstruction a → status_class ≝
  λa, pre.
  match pre with
  [ RET ⇒ cl_return
  | RETI ⇒ cl_return
  | JZ _ ⇒ cl_jump
  | JNZ _ ⇒ cl_jump
  | JC _ ⇒ cl_jump
  | JNC _ ⇒ cl_jump
  | JB _ _ ⇒ cl_jump
  | JNB _ _ ⇒ cl_jump
  | JBC _ _ ⇒ cl_jump
  | CJNE _ _ ⇒ cl_jump
  | DJNZ _ _ ⇒ cl_jump
  | JMP _ ⇒ cl_call
  | _ ⇒ cl_other
  ].

definition ASM_classify0: instruction → status_class ≝
  λi.
  match i with
   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
   | ACALL _ ⇒ cl_call
   | LCALL _ ⇒ cl_call
   | AJMP _ ⇒ cl_other
   | LJMP _ ⇒ cl_other
   | SJMP _ ⇒ cl_other
   | _ ⇒ cl_other
   ].

definition current_instruction0 ≝
  λcode_memory: BitVectorTrie Byte 16.
  λprogram_counter: Word.
    \fst (\fst (fetch … code_memory program_counter)).

definition current_instruction ≝
  λcode_memory.
  λs: Status code_memory.
    current_instruction0 code_memory (program_counter … s).
    
definition current_instruction_label ≝
  λcode_memory.
  λcost_labels: BitVectorTrie costlabel 16.
  λs: Status code_memory.
  let pc ≝ program_counter … code_memory s in
    lookup_opt … pc cost_labels.

definition next_instruction_properly_relates_program_counters ≝
  λcode_memory.
  λbefore: Status code_memory.
  λafter : Status code_memory.
    let program_counter_before ≝ program_counter ? code_memory before in
    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
      program_counter ? code_memory after = program_counter_after.

definition word_deqset: DeqSet ≝
  mk_DeqSet Word (eq_bv 16) ?.
  @refl_iff_eq_bv_true
qed.
    
definition OC_classify: ∀code_memory. Status code_memory → status_class ≝
  λcode_memory.
  λs: Status code_memory.
    ASM_classify0 (current_instruction … s).