include "ASM/Interpret.ma".
include "common/SmallstepExec.ma".
include "common/IO.ma".

(* Transition system on the assembly code *)

(*CSC: waiting for Jaap's code to compile or to be splitted from Assembly.ma *)
axiom policy: pseudo_assembly_program → Type[0].
(*CSC: problem here: mk_policy should be allowed to fail, but mk_fullexec does
  not allow make_global to fail too *)
axiom mk_policy: ∀p:pseudo_assembly_program. policy p.

(*CSC: already implemented in AssemblyProof.ma: move elsewhere *)
axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat.

definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝
 λp. ticks_of … (mk_policy p).

definition execute_1_pseudo_instruction_trace:
 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
λticks_of,s.
 let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in
 let s ≝ execute_1_pseudo_instruction ticks_of s in
 match instr with
 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
 | _ ⇒ ret ? 〈E0, s〉 ].

axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.

definition pseudo_exec: trans_system io_out io_in ≝
 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.

definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
 mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)).

(* Transition system on the object code *)

(*CSC: move this definition elsewhere *)
definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).

definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.

definition execute_1_instruction:
 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
λcosts,s.
 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
 let 〈instr,pc〉 ≝ instr_pc in
 let s ≝ eject … (execute_1 s) in
 match lookup_opt … pc costs with
 [ None ⇒ ret … 〈E0, s〉
 | Some cst ⇒ ret … 〈Echarge cst, s〉 ].

axiom is_final: BitVectorTrie costlabel 16 → Status → option int.

definition exec: trans_system io_out io_in ≝
 mk_trans_system … is_final execute_1_instruction.

definition ASM_fullexec: fullexec io_out io_in ≝
 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).