include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
include "joint/Joint.ma".
include "joint/BEMem.ma".

(* CSC: external functions never fail (??) and always return something of the
   size of one register, both in the frontend and in the backend.
   Is this reasonable??? In OCaml it always return a list, but in the frontend
   only the head is kept (or Undef if the list is empty) ??? *)

definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)

definition eq_address: address → address → bool ≝
 λaddr1,addr2.
  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).

record more_sem_params (p:params_): Type[1] ≝
 { framesT: Type[0]
 ; regsT: Type[0]

 ; succ_pc: succ p → address → address
 ; pop_frame_: framesT → res framesT
 ; save_frame_: framesT → regsT → framesT
 ; greg_store_: generic_reg p → beval → regsT → res regsT
 ; greg_retrieve_: regsT → generic_reg p → res beval
 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
 ; acca_retrieve_: regsT → acc_a_reg p → res beval
 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
 ; accb_retrieve_: regsT → acc_b_reg p → res beval
 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
 ; dpl_retrieve_: regsT → dpl_reg p → res beval
 ; dph_store_: dph_reg p → beval → regsT → res regsT
 ; dph_retrieve_: regsT → dph_reg p → res beval
 ; pair_reg_move_: regsT → pair_reg p → regsT
 
 ; pointer_of_label: label → Σp:pointer. ptype p = Code
 }.

record sem_params: Type[1] ≝
 { spp :> params_
 ; more_sem_pars :> more_sem_params spp
 }.

record state (p: sem_params): Type[0] ≝
 { st_frms: framesT ? p
 ; pc: address
 ; sp: pointer
 ; carry: beval
 ; regs: regsT ? p
 ; m: bemem
 }.

definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).

record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
 { more_sparams:> more_sem_params p

 ; init_locals : localsT p → regsT … more_sparams
 
 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val

 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
 }.

record sem_params2 (globals: list ident): Type[1] ≝
 { p2:> params globals
 ; more_sparams2:> more_sem_params2 globals p2
 }.

definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
(*
unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
   S ≟ sem_params_of_sem_params2 globals p
(* ---------------------------------------- *) ⊢
   pars_ (spp (mk_sem_params (p2 globals p)
    (more_sparams (p2 globals p) globals
    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
*)
definition address_of_label: sem_params → label → address.
 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
  [ #res #_ @res
  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
qed.

definition set_m: ∀p. bemem → state p → state p ≝
 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.

definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).

definition set_sp: ∀p. pointer → state p → state p ≝
 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).

definition set_carry: ∀p. beval → state p → state p ≝
 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).

definition set_pc: ∀p. address → state p → state p ≝
 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).

definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).

definition goto: ∀p:sem_params. label → state p → state p ≝
 λp,l,st. set_pc … (address_of_label p l) st.

definition next: ∀p:sem_params. succ … p → state p → state p ≝
 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.

definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs  ← greg_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
 λp,st,dst.greg_retrieve_ … (regs … st) dst.

definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← acca_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
 λp,st,dst.acca_retrieve_ … (regs … st) dst.

definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← accb_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
 λp,st,dst.accb_retrieve_ … (regs … st) dst.

definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← dpl_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
 λp,st,dst.dpl_retrieve_ … (regs … st) dst.

definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← dph_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
 λp,st,dst.dph_retrieve_ … (regs … st) dst.

definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.

definition save_frame: ∀p:sem_params. state p → state p ≝
 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.

(* removes the top frame from the frames list *)
definition pop_frame: ∀p. state p → res (state p) ≝
 λp,st.
  do frames ← pop_frame_ … p (st_frms … st);
  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).

axiom FailedStore: String.

definition push: ∀p. state p → beval → res (state p) ≝
 λp,st,v.
  let sp ≝ sp … st in
  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
  OK … (set_m … m (set_sp … sp st)).

definition pop: ∀p. state p → res (state p × beval) ≝
 λp,st.
  let sp ≝ sp ? st in
  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
  let st ≝ set_sp … sp st in
  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
  OK ? 〈st,v〉.

definition save_ra : ∀p. state p → succ p → res (state p) ≝
 λp,st,l.
  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
  do st ← push … st addrl;
  push … st addrh.

definition fetch_ra : ∀p.state p → res (state p × address) ≝
 λp,st.
  do 〈st,addrh〉 ← pop … st;
  do 〈st,addrl〉 ← pop … st;
  OK ? 〈st, 〈addrl,addrh〉〉.

axiom MissingSymbol : String.
axiom FailedLoad : String.
axiom BadFunction : String.

definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
 λglobals,p,ge,st.
  ! s ← fetch_statement … st;
  match s with
    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
    | sequential seq l ⇒
      match seq with
      [ extension c ⇒ exec_extended … p ge c st
      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
      | INT dest v ⇒
        ! st ← greg_store p dest (BVByte v) st;
          ret ? 〈E0, next … l st〉
      | LOAD dst addrl addrh ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
        ! st ← acca_store p … dst v st;
          ret ? 〈E0, next … l st〉
      | STORE addrl addrh src ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
        ! v ← acca_retrieve … st src;
        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
          ret ? 〈E0, next … l (set_m … m' st)〉
      | COND src ltrue ⇒
        ! v ← acca_retrieve … st src;
        ! b ← bool_of_beval v;
          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
      | ADDRESS ident prf ldest hdest ⇒
        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
        ! st ← dpl_store p ldest laddr st;
        ! st ← dph_store p hdest haddr st;
          ret ? 〈E0, next … l st〉
      | OP1 op dacc_a sacc_a ⇒
        ! v ← acca_retrieve … st sacc_a;
        ! v ← Byte_of_val v;
          let v' ≝ BVByte (op1 eval op v) in
        ! st ← acca_store p dacc_a v' st;
          ret ? 〈E0, next … l st〉
      | OP2 op dacc_a sacc_a src ⇒
        ! v1 ← acca_retrieve … st sacc_a;
        ! v1 ← Byte_of_val v1;
        ! v2 ← greg_retrieve … st src;
        ! v2 ← Byte_of_val v2;
        ! carry ← bool_of_beval (carry … st);
          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
          let v' ≝ BVByte v' in
          let carry ≝ beval_of_bool carry in
        ! st ← acca_store p dacc_a v' st;
          ret ? 〈E0, next … l (set_carry … carry st)〉
      | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
      | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
        ! v1 ← acca_retrieve … st sacc_a_reg;
        ! v1 ← Byte_of_val v1;
        ! v2 ← accb_retrieve … st sacc_b_reg;
        ! v2 ← Byte_of_val v2;
          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
          let v1' ≝ BVByte v1' in
          let v2' ≝ BVByte v2' in
        ! st ← acca_store p dacc_a_reg v1' st;
        ! st ← accb_store p dacc_b_reg v2' st;
          ret ? 〈E0, next … l st〉
      | POP dst ⇒
        ! 〈st,v〉 ← pop … st;
        ! st ← acca_store p dst v st;
          ret ? 〈E0, next … l st〉
      | PUSH src ⇒
        ! v ← acca_retrieve … st src;
        ! st ← push … st v;
          ret ? 〈E0, next … l st〉
      | MOVE dst_src ⇒
          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
      (*CSC: XXX bug here dest unused *)
      | CALL_ID id argsno dest ⇒
        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
          match fd with
          [ Internal fn ⇒
            ! st ← save_ra … st l;
              let st ≝ save_frame … st in
              let regs ≝ init_locals … (joint_if_locals … fn) in
              let l' ≝ joint_if_entry … fn in
             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
          | External fn ⇒
            ! params ← fetch_external_args … fn st;
            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
            (* CSC: XXX bug here; I think I should split it into Byte-long
               components; instead I am making a singleton out of it *)
              let vs ≝ [mk_val ? evres] in
            ! st ← set_result … vs st; 
              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
          ]]
    | RETURN ⇒
      ! st ← pop_frame … st;
      ! 〈st,pch〉 ← pop … st;
      ! 〈st,pcl〉 ← pop … st;
        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
cases addr //
qed.

definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
 λglobals,p,exit,registersno,st. res_to_opt … (
  do s ← fetch_statement … st;
  match s with
   [ RETURN ⇒
      do 〈st,l〉 ← fetch_ra … st;
      if eq_address l exit then
       do val ← fetch_result … st registersno;
       match val with
        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
        | _ ⇒ Error ? []]
      else
       Error ? []
   | _ ⇒ Error ? []]).

record evaluation_parameters : Type[1] ≝
 { globals: list ident
 ; sparams2: sem_params2 globals
 ; exit: address
 ; registersno: nat
 ; genv2: genv globals sparams2
 }.

definition joint_exec: trans_system io_out io_in ≝
  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).

definition make_global :
 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
  joint_program pars → evaluation_parameters
≝
 λpars,sparams.
  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
qed.

definition make_initial_state :
 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
λpars,sparams,p.
  let ge ≝ genv2 (make_global pars sparams p) in
  do m ← init_mem Genv … (λx.[Init_space x]) p;
  let main ≝ prog_main … p in
  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
cases daemon qed.
(*
RTL:
 init_prog == init_mem
 init_sp: inizializzare lo stack pointer
 init_isp: inizializzare l'altro stack pointer
 init_renv: inizializzare i registri fisici
 init_main_call: chiamata di funzione
   --- init_fun_call: cambia fra ERTL e LTL
 change_carry: a 0
*)

definition joint_fullexec :
 ∀pars:∀globals.params globals.
 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
 fullexec io_out io_in ≝
 λpars,sparams.
  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).