include "joint/semanticsUtils.ma".
include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
include alias "common/Identifiers.ma".

definition ertl_reg_env ≝ register_env beval × hw_register_env.

definition ps_reg_store: ? → ? → ? → res ? ≝
 λr,v.λlocal_env : ertl_reg_env.
  let res ≝ reg_store r v (\fst local_env) in
  OK … 〈res, \snd local_env〉.

definition ps_reg_retrieve ≝
 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).

definition hw_reg_store ≝
 λr,v.λlocal_env:ertl_reg_env.
  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.

definition hw_reg_retrieve ≝
 λlocal_env:ertl_reg_env.λreg.
  OK … (hwreg_retrieve … (\snd local_env) reg).


definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
  λlocal_env,a.
  match a with
  [ Reg r ⇒ ps_reg_retrieve local_env r
  | Imm b ⇒ return BVByte b
  ]. 

definition get_hwsp : ertl_reg_env → res xpointer ≝
 λst.hwreg_retrieve_sp (\snd st).

definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.

definition ERTL_state : sem_state_params ≝
  mk_sem_state_params
 (* framesT ≝ *) (list (register_env beval × (Σb:block.block_region b=Code)))
 (* empty_framesT ≝ *) [ ]
 (* regsT ≝ *) ertl_reg_env
 (* empty_regsT ≝ *) (λsp.〈empty_map …, init_hw_register_env sp〉)
 (*load_sp ≝ *) get_hwsp
 (*save_sp ≝ *) set_hwsp.

(* we ignore need_spilled_no as we never move framesize based values around in the
   translation *)
definition ertl_eval_move ≝ λenv,pr.
      ! v ←
        match \snd pr with
        [ Reg src ⇒
          match src with
          [ PSD r ⇒ ps_reg_retrieve env r
          | HDW r ⇒ hw_reg_retrieve env r
          ]
        | Imm b ⇒ return BVByte b ] ;
      match \fst pr with
      [ PSD r ⇒ ps_reg_store r v env
      | HDW r ⇒ hw_reg_store r v env
      ].

definition ertl_allocate_local ≝
  λreg.λlenv : ertl_reg_env.
  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.

definition ertl_save_frame:
 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
 λ_.λ_.λst. 
  ! st' ← push_ra … st (pc … st) ;
  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
  return 
  (set_frms ERTL_state 
  (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).

definition ertl_pop_frame:
 state ERTL_state →
   res (state ERTL_state × program_counter) ≝
 λst.
 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
 match frms with
 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
 | cons hd tl ⇒
   let 〈local_mem, bl〉 ≝ hd in
   let st' ≝ set_regs ERTL_state 〈local_mem, \snd (regs … st)〉
      (set_frms ERTL_state tl st) in
   ! 〈st'', pc〉 ← pop_ra … st' ;
   if eq_block bl (pc_block pc) then
     OK … 〈st'', pc〉
   else Error ? [MSG BlockInFramesCorrupted]
 ].

(*CSC: XXXX, for external functions only*)
axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
(* I think there should be a list beval in place of list val here
  λvals.λ_.λst.
  (* set all RegisterRets to 0 *)
  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)

(*CSC: here we should use helper_def_store from Joint/semantics.ma,
  but it is not visible *)
definition ps_reg_store_status : register → beval → state ERTL_state →
  res (state ERTL_state) ≝
 λdst,v,st.
  let env ≝ regs … st in
  ! env' ← ps_reg_store dst v env ;
  return set_regs ERTL_state env' st.

definition eval_ertl_seq:
 ∀F. ∀globals. genv_gen F globals →
  ertl_seq → ident → state ERTL_state →
   res (state ERTL_state) ≝
 λF,globals,ge,stm,id,st.
 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
  match stm with
   [ ertl_new_frame ⇒
      ! sp ← sp … st ;
      let newsp ≝ neg_shift_pointer … sp framesize in
      return set_sp … newsp st
   | ertl_del_frame ⇒
      ! sp ← sp … st ;
      let newsp ≝ shift_pointer … sp framesize in
      return set_sp … newsp st
   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  

definition ERTL_sem_uns ≝  
λF. mk_sem_unserialized_params ERTL ?
  (* st_pars            ≝ *) ERTL_state
  (* acca_store_        ≝ *) ps_reg_store
  (* acca_retrieve_     ≝ *) ps_reg_retrieve
  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* accb_store_        ≝ *) ps_reg_store
  (* accb_retrieve_     ≝ *) ps_reg_retrieve
  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* dpl_store_         ≝ *) ps_reg_store
  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* dph_store_         ≝ *) ps_reg_store
  (* dph_retrieve_      ≝ *) ps_reg_retrieve
  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* pair_reg_move_     ≝ *) ertl_eval_move
  (* save_frame         ≝ *) ertl_save_frame
  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
  (* fetch_external_args≝ *) ertl_fetch_external_args
  (* set_result         ≝ *) ertl_set_result
  (* call_args_for_main ≝ *) 0
  (* call_dest_for_main ≝ *) it
  (* read_result        ≝ *) (λ_.λ_.λ_.
     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).

definition ERTL_semantics ≝
  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.