source: src/ASM/Interpret2.ma @ 3003

include "ASM/ASMCosts.ma".
include "common/Measurable.ma".

(* Move where abstract_status is defined! *)
definition mk_trans_system_of_abstract_status:
 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in
≝
 λS,as_eval.
  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
   (λ_.λstatus.
     let tr ≝
      match as_label … status with
      [ Some cst ⇒ Echarge cst
      | None ⇒ E0 ] in
     ! status' ← as_eval … status ;
     return 〈 tr, status' 〉).

definition mk_fullexec_of_abstract_status:
 ∀program: Type[0].
  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
≝ λprogram,S,as_eval,as_init.
   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 
    (λ_.return as_init).

definition mk_preclassified_system_of_abstract_status:
 ∀program: Type[0].
  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
≝ λprogram,S,as_eval,as_init.
   mk_preclassified_system
    (mk_fullexec_of_abstract_status program S as_eval as_init)
    (λ_.λst. ¬(is_none … (as_label … st)))
    (λ_.as_classify S)
    (λ_.λst,prf. as_call_ident S «st,?»).
 @hide_prf cases (as_classify ??) in prf; normalize // *
qed.

(* End move *)

definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
 λc:labelled_object_code.
  mk_preclassified_system_of_abstract_status
   labelled_object_code
   (OC_abstract_status c)
   (λst. return (execute_1 (cm c) … st))
   (initialise_status … (cm c)).

(* Pre-classified system for ASM *)

include "ASM/Assembly.ma".

(* Move next function in interpret? *)
definition execute_1_pseudo_instruction':
 ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
 λcm,sigma,policy,status.
  execute_1_pseudo_instruction cm
   (ticks_of cm  sigma policy) status ….
cases daemon (*CSC: we need to prove that we remain inside the program
 (code closed), which is impossible in case of function pointers.
 But the type does not allow to fail (yet?) *)
qed.

definition classify_pseudo_instruction: pseudo_instruction → status_class ≝
 λinstr.
  match instr with
  [ Instruction pre ⇒ ASM_classify00 … pre
  | Comment _ ⇒ cl_other
  | Cost _ ⇒ cl_other
  | Jmp _ ⇒ cl_other
  | Jnz _ _ _ ⇒ cl_jump
  | MovSuccessor _ _ _ ⇒ cl_other
  | Call _ ⇒ cl_call
  | Mov _ _ ⇒ cl_other ].

definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
λcm,s.
 classify_pseudo_instruction
  (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)).
cases daemon (*CSC: again*)
qed.

definition ASM_next_instruction_properly_relates_program_counters ≝
  λcm.
  λbefore: PseudoStatus cm.
  λafter : PseudoStatus cm.
    let 〈instruction, program_counter_after〉 ≝
     fetch_pseudo_instruction (code cm) (program_counter … before) ?
    in
     program_counter ?? after = program_counter_after.
cases daemon (*CSC: again*)
qed.

definition ASM_as_label_of_pc:
 ∀prog:pseudo_assembly_program. Word → option costlabel
≝
 λprog,pc.
 match \fst (fetch_pseudo_instruction (code prog) pc ?) with 
 [ Cost label ⇒ Some … label
 | _ ⇒ None ? ].
cases daemon (*CSC: again*)
qed.

definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝
 λprog,st.
  let finaladdr ≝ address_of_word_labels (code prog) (final_label … prog) in
   as_result_of_finaladdr … st finaladdr.

include "common/AssocList.ma".

definition ASM_as_call_ident:
 ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
≝
 λprog,sigma,policy,s0.
  let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
  match lbl with
  [ None ⇒ ⊥
  | Some lbl' ⇒
     match assoc_list_lookup ?? lbl' (eq_identifier …) (renamed_symbols prog) with
     [ None ⇒ ⊥ | Some id ⇒ id ]].
cases daemon (*CSC: we need a specification of the renamed_symbols for this *)
qed.

definition ASM_abstract_status:
 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
  λprog,sigma,policy.
    mk_abstract_status
      (PseudoStatus prog)
      (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
      word_deqset
      (program_counter …)
      (ASM_classify …)
      (ASM_as_label_of_pc prog …)
      (ASM_next_instruction_properly_relates_program_counters prog)
      (ASM_as_result …)
      (ASM_as_call_ident prog sigma policy …)
      ?.
 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
 normalize try (#x #y #abs) try (#x #abs) try #abs destruct (abs)
qed.

definition ASM_preclassified_system:
 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
 λc,sigma,policy.
  mk_preclassified_system_of_abstract_status
   (pseudo_assembly_program × (Word → Word) × (Word → bool))
   (ASM_abstract_status c sigma policy)
   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
   (initialise_status … c).