include "common/Globalenvs.ma".
include "common/IO.ma".
(* include "common/SmallstepExec.ma". *)
include "joint/BEMem.ma".
include "joint/Joint.ma".
include "ASM/I8051bis.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) ??? *)

(* Paolo: I'll put in this record the property about genv we need *)
record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
{ ge :> genv_t (fundef (F globals))
; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
}.

definition genv ≝ λp.genv_gen (joint_internal_function p).
coercion genv_to_genv_t :
  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.

definition cpointer ≝ Σp.ptype p = Code.
definition xpointer ≝ Σp.ptype p = XData.
unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer 	(λp.ptype p = XData).

record sem_state_params : Type[1] ≝
 { framesT: Type[0]
 ; empty_framesT: framesT
 ; regsT : Type[0]
 ; empty_regsT: xpointer → regsT (* Stack pointer *)
 }.

record state (semp: sem_state_params): Type[0] ≝
 { st_frms: framesT semp 
 ; sp: xpointer
 ; isp: xpointer
 ; carry: bebit
 ; regs: regsT semp
 ; m: bemem
 }.

coercion sem_state_params_to_state nocomposites:
  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].

record state_pc (semp : sem_state_params) : Type[0] ≝
  { st_no_pc :> state semp
  ; pc : cpointer
  }.

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

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

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

definition set_isp: ∀p. ? → state p → state p ≝
 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).

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

definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.

definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
 λp,s,st. mk_state_pc … s (pc … st).

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

axiom BadProgramCounter : String.

definition function_of_block :
 ∀pars : params.
 ∀globals.
  genv pars globals →
  block →
  res (joint_internal_function pars globals) ≝
  λpars,globals,ge,b.
  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
  match def with
  [ Internal def' ⇒ OK … def'
  | External _ ⇒ Error … [MSG BadProgramCounter]].
 
(* this can replace graph_fetch function and lin_fetch_function *)
definition fetch_function:
 ∀pars : params.
 ∀globals.
  genv pars globals →
  cpointer →
  res (joint_internal_function pars globals) ≝
 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).

inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)

inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
  | FEnd2  : fin_step_flow p F Call. (* end flow *)

record more_sem_unserialized_params
  (uns_pars : unserialized_params)
  (F : list ident → Type[0]) : Type[1] ≝
  { st_pars :> sem_state_params (* automatic coercion has issues *)
  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)

  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
     type of arguments. To be fixed using a dependent type *)
  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
      state st_pars → res (state st_pars)
  ; fetch_external_args: external_function → state st_pars →
      res (list val)
  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
  ; call_args_for_main: call_args uns_pars
  ; call_dest_for_main: call_dest uns_pars

  (* from now on, parameters that use the type of functions *)
  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
  (* change of pc must be left to *_flow execution *)
  ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
      F globals → state st_pars → IO io_out io_in (state st_pars)
  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
  ; eval_ext_call: ∀globals.genv_gen F globals →
      ext_call uns_pars → state st_pars →
      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
  (* do something more in some op2 calculations (e.g. mark a register for correction
     with spilled_no in ERTL) *)
  ; post_op2 : ∀globals.genv_gen F globals →
    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
    state st_pars → state st_pars
  }.

(*coercion msu_pars_to_ss_pars nocomposites :
∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
 ≝ st_pars
on _msup : more_sem_unserialized_params ?? to sem_state_params.*)


definition helper_def_retrieve : 
  ∀X : ? → ? → ? → Type[0].
  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
    λX,f,up,F,p,st.f ?? p (regs … st).

definition helper_def_store :
  ∀X : ? → ? → ? → Type[0].
  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.

definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
definition acca_store ≝ helper_def_store ? acca_store_.
definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
definition accb_store ≝ helper_def_store ? accb_store_.
definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
definition dpl_store ≝ helper_def_store ? dpl_store_.
definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
definition dph_store ≝ helper_def_store ? dph_store_.
definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
definition pair_reg_move ≝
  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    return set_regs ? r st.

 
axiom BadPointer : String.

(* this is preamble to all calls (including tail ones). The optional argument in
   input tells the function whether it has to save the frame for internal
   calls.
   the first element of the triple is the entry point of the function if
   it is an internal one, or false in case of an external one.
   The actual update of the pc is left to later, as it depends on
   serialization and on whether the call is a tail one. *)
definition eval_call_block:
 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
 λp,F,p',globals,ge,st,b,args,dest.
  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
    match fd with
    [ Internal fd ⇒
      return 〈Init ?? (block_id b) fd args dest, st〉
    | External fn ⇒
      ! params ← fetch_external_args … p' fn st : IO ???;
      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
      ! 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. To be
         fixed once we fully implement external functions. *)
      let vs ≝ [mk_val ? evres] in
      ! st ← set_result … p' vs dest st : IO ???;
      return 〈Proceed ???, st〉
      ].

axiom FailedStore: String.

definition push: ∀p.state p → beval → res (state p) ≝
 λp,st,v.
  let isp' ≝ isp ? st in
  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
  return set_m … m (set_isp … isp'' st).
  normalize elim (isp p st) #p #H @H
qed.

definition pop: ∀p. state p → res ((state p ) × beval) ≝
 λp,st.
  let isp' ≝ isp ? st in
  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
  let ist ≝ set_isp … isp'' st in
  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
  OK ? 〈ist,v〉.
  normalize elim (isp p st) #p #H @H
qed.

definition save_ra : ∀p. state p → cpointer → res (state p) ≝
 λp,st,l.
  ! 〈addrl,addrh〉 ← address_of_pointer l ; (* always succeeds *)
  ! st' ← push … st addrl;
  push … st' addrh.

definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
 λp,st.
  do 〈st',addrh〉 ← pop … st;
  do 〈st'',addrl〉 ← pop … st';
  do pr ← pointer_of_address 〈addrh, addrl〉;
  match ptype pr return λx.ptype pr = x → res (? × cpointer) with
  [ Code ⇒ λprf.return 〈st'', «pr,prf»〉
  | _ ⇒ λ_.Error … [MSG BadPointer]
  ] (refl …).

(* parameters that are defined by serialization *)
record more_sem_params (pp : params) : Type[1] ≝
  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
  ; offset_of_point : code_point pp → option offset (* can overflow *)
  ; point_of_offset : offset → code_point pp
  ; point_of_offset_of_point :
    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
  ; offset_of_point_of_offset :
    ∀o.offset_of_point (point_of_offset o) = Some ? o
  }.

(*
coercion ms_pars_to_msu_pars nocomposites :
∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
 ≝ msu_pars
on _msp : more_sem_params ? to more_sem_unserialized_params ??.

definition ss_pars_of_ms_pars ≝
  λp.λpp : more_sem_params p.
  st_pars … (msu_pars … pp).
coercion ms_pars_to_ss_pars nocomposites :
∀p : params.∀msp : more_sem_params p.sem_state_params ≝
ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)

axiom CodePointerOverflow : String.

definition pointer_of_point : ∀p.more_sem_params p →
  cpointer→ code_point p → res cpointer ≝
  λp,msp,ptr,pt.
  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
  return «mk_pointer (pblock ptr) o, ?».
elim ptr #ptr' #EQ <EQ % qed.

definition point_of_pointer :
  ∀p.more_sem_params p → cpointer → code_point p ≝
  λp,msp,ptr.point_of_offset p msp (poff ptr).

lemma point_of_pointer_of_point :
  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
  pointer_of_point p msp ptr1 pt = return ptr2 →
  point_of_pointer p msp ptr2 = pt.
#p #msp #ptr1 #ptr2 #pt normalize
lapply (point_of_offset_of_point p msp pt)
cases (offset_of_point ???) normalize
[ * #ABS destruct(ABS)
| #o #EQ1 #EQ2 destruct %
]
qed.

lemma pointer_of_point_block :
  ∀p,msp,ptr1,ptr2,pt.
  pointer_of_point p msp ptr1 pt = return ptr2 →
  pblock ptr2 = pblock ptr1.
#p #msp #ptr1 #ptr2 #pt normalize
cases (offset_of_point ???) normalize
[ #ABS destruct(ABS)
| #o #EQ destruct(EQ) %
]
qed.

lemma pointer_of_point_uses_block :
  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
#p #msp ** #b1 #o1 #EQ1
        ** #b2 #o2 #EQ2
#pt #EQ3 destruct normalize //
qed.

lemma pointer_of_point_of_pointer :
  ∀p,msp.∀ptr1,ptr2 : cpointer.
    pblock ptr1 = pblock ptr2 →
    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
#p #msp ** #b1 #o1 #EQ1
        ** #b2 #o2 #EQ2
#EQ3 destruct
normalize >offset_of_point_of_offset normalize %
qed.

axiom ProgramCounterOutOfCode : String.
axiom PointNotFound : String.
axiom LabelNotFound : String.

definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv p globals → cpointer →
  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
  λp,msp,globals,ge,ptr.
  let pt ≝ point_of_pointer ? msp ptr in
  ! fn ← fetch_function … ge ptr ;
  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
  return 〈fn, stmt〉.
  
definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv p globals → cpointer → label → res cpointer ≝
  λp,msp,globals,ge,ptr,lbl.
  ! fn ← fetch_function … ge ptr ;
  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
            (point_of_label … (joint_if_code … fn) lbl) ;
  pointer_of_point p msp ptr pt.

definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
  cpointer → succ p → res cpointer ≝
  λp,msp,ptr,nxt.
  let curr ≝ point_of_pointer p msp ptr in
  pointer_of_point p msp ptr (point_of_succ p curr nxt).

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

(* definition msu_pars_of_s_pars :
∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
≝ λp : sem_params.
  msu_pars … (more_sem_pars p).
coercion s_pars_to_msu_pars nocomposites :
∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
msu_pars_of_s_pars
on p : sem_params to more_sem_unserialized_params ??.

definition ss_pars_of_s_pars :
∀p : sem_params.sem_state_params
≝ λp : sem_params.
  st_pars … (msu_pars … (more_sem_pars p)).
coercion s_pars_to_ss_pars nocomposites :
∀p : sem_params.sem_state_params ≝
ss_pars_of_s_pars
on _p : sem_params to sem_state_params.

definition ms_pars_of_s_pars :
∀p : sem_params.more_sem_params (spp p)
≝ more_sem_pars.
coercion s_pars_to_ms_pars nocomposites :
∀p : sem_params.more_sem_params (spp p) ≝
ms_pars_of_s_pars
on p : sem_params to more_sem_params ?.*)

(* definition address_of_label: ∀globals. ∀p:sem_params.
  genv globals p → pointer → label → res address ≝
 λglobals,p,ge,ptr,l.
  do newptr ← pointer_of_label … p ? ge … ptr l ;
  OK … (address_of_code_pointer newptr). *)

definition goto: ∀globals.∀p : sem_params.
  genv p globals → label → state p → cpointer → res (state_pc p) ≝
 λglobals,p,ge,l,st,b.
  ! newpc ← pointer_of_label ? p … ge b l ;
  return mk_state_pc ? st newpc.

(*
definition empty_state: ∀p. more_sem_params p → state p ≝
 mk_state … (empty_framesT …) 
*)

definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
 λp,l,st,pc.
 ! newpc ← succ_pc ? p … pc l ;
 return mk_state_pc … st newpc.

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

definition eval_seq_no_pc :
 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
  state p → ∀s:joint_seq p globals.
  IO io_out io_in (state p) ≝
 λp,globals,ge,curr_fn,st,seq.
 match seq return λx.IO ??? with
  [ extension_seq c ⇒
    eval_ext_seq … ge c curr_fn st
  | LOAD dst addrl addrh ⇒
    ! vaddrh ← dph_arg_retrieve … st addrh ;
    ! vaddrl ← dpl_arg_retrieve … st addrl;
    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    acca_store p … dst v st
 | STORE addrl addrh src ⇒
    ! vaddrh ← dph_arg_retrieve … st addrh;
    ! vaddrl ← dpl_arg_retrieve … st addrl;
    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    ! v ← acca_arg_retrieve … st src;
    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    return set_m … m' st
  | ADDRESS id prf ldest hdest ⇒
    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
    ! st' ← dpl_store … ldest laddr st;
    dph_store … hdest haddr st'
  | OP1 op dacc_a sacc_a ⇒
    ! v ← acca_retrieve … st sacc_a;
    ! v' ← be_op1 op v ;
    acca_store … dacc_a v' st
  | OP2 op dacc_a sacc_a src ⇒
    ! v1 ← acca_arg_retrieve … st sacc_a;
    ! v2 ← snd_arg_retrieve … st src;
    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
    ! st' ← acca_store … dacc_a v' st;
    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
  | CLEAR_CARRY ⇒
    return set_carry … (BBbit false) st
  | SET_CARRY ⇒
    return set_carry … (BBbit true) st
  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
    ! st' ← acca_store … dacc_a_reg v1' st;
    accb_store … dacc_b_reg v2' st'
  | POP dst ⇒
    ! 〈st',v〉 ← pop p st;
    acca_store … p dst v st'
  | PUSH src ⇒
    ! v ← acca_arg_retrieve … st src;
    push … st v
  | MOVE dst_src ⇒
    pair_reg_move … st dst_src
  | CALL_ID id args dest ⇒
    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    return st'
  | extension_call s ⇒
    !〈flow, st'〉 ← eval_ext_call … ge s st ;
    return st'
  | _ ⇒ return st
  ].
  @find_symbol_exists
  lapply prf
  elim globals [*]
  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
  #G %2 @IH @G
  qed.

definition eval_seq_pc :
 ∀p:sem_params.∀globals. genv p globals → state p →
  ∀s:joint_seq p globals.
  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
  [ CALL_ID id args dest ⇒
    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    return flow
  | extension_call s ⇒
    !〈flow, st'〉 ← eval_ext_call … ge s st ;
    return flow
  | _ ⇒ return Proceed ???
  ].

definition eval_step :
 ∀p:sem_params.∀globals. genv p globals →
  joint_internal_function p globals → state p →
  ∀s:joint_step p globals.
  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
  λp,globals,ge,curr_fn,st,s.
  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
  [ step_seq s ⇒
    ! flow ← eval_seq_pc ?? ge st s ;
    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
    return 〈flow,st'〉
  | COND src ltrue ⇒
    ! v ← acca_retrieve … st src;
    ! b ← bool_of_beval v;
    if b then
      return 〈Redirect ??? ltrue, st〉
    else
      return 〈Proceed ???, st〉
  ].
  %1 % qed.

definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
  IO io_out io_in (state p) ≝
 λp,globals,ge,curr_fn,st,s.
  match s return λx.IO ??? with
    [ tailcall c ⇒
      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
      return st'
    | _ ⇒ return st
    ].

definition eval_fin_step_pc :
 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
  ∀s:joint_fin_step p.
  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
  λp,g,ge,curr_fn,st,s.
  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
  [ tailcall c ⇒
    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    return flow  
  | GOTO l ⇒ return FRedirect … l
  | RETURN ⇒ return FEnd1 ??
  ]. %1 % qed.

definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
  state p → Z → joint_internal_function p globals → call_args p →
  res (state_pc p) ≝
  λp,globals,ge,st,id,fn,args.
    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
              args st ;
    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
    let l' ≝ joint_if_entry … fn in
    let st' ≝ set_regs p regs st in
    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
    return mk_state_pc ? st' pc. % qed.

(* The pointer provided is the one to the *next* instruction. *)
definition eval_step_flow :
 ∀p:sem_params.∀globals.∀flows.genv p globals →
 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
 λp,globals,flows,ge,st,nxt,cmd.
 match cmd with
  [ Redirect _ l ⇒
    goto … ge l st nxt
  | Init id fn args dest ⇒
    ! st' ← save_frame … nxt dest st ;
    do_call ?? ge st' id fn args
  | Proceed _ ⇒
    return mk_state_pc ? st nxt
  ].

definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
  λp,globals,lbls,ge,st,curr,cmd.
  match cmd with
  [ FRedirect _ l ⇒ goto … ge l st curr
  | FTailInit id fn args ⇒
    do_call … ge st id fn args
  | _ ⇒
    ! 〈st',ra〉 ← fetch_ra … st ;
    ! fn ← fetch_function … ge curr ;
    ! st'' ← pop_frame … ge fn st';
    return mk_state_pc ? st'' ra
  ].

definition eval_statement :
 ∀globals.∀p:sem_params.genv p globals →
  state_pc p → joint_internal_function p globals → joint_statement p globals →
    IO io_out io_in (state_pc p) ≝
 λglobals,p,ge,st,curr_fn,stmt.
 match stmt with
 [ sequential s nxt ⇒
   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
   eval_step_flow … ge st' nxtptr flow
 | final s ⇒
   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
   eval_fin_step_flow … ge st' (pc … st) flow
 ].

definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
  state_pc p → IO io_out io_in (state_pc p) ≝
  λglobals,p,ge,st.
  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
  eval_statement … ge st fn s.

(* Paolo: what if in an intermediate language main finishes with an external
  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
  not static... *)
definition is_final: ∀globals:list ident. ∀p: sem_params.
  genv p globals → cpointer → state_pc p → option int ≝
 λglobals,p,ge,exit,st.res_to_opt ? (
  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
  match s with
  [ final s' ⇒
    match s' with
    [ RETURN ⇒ 
      do 〈st',ra〉 ← fetch_ra … st;
      if eq_pointer ra exit then 
       do vals ← read_result … ge (joint_if_result … fn) st' ;
       Word_of_list_beval vals
      else
       Error ? [ ]
   | _ ⇒ Error ? [ ]
   ]
 | _ ⇒ Error ? [ ]
 ]).

(*
record evaluation_parameters : Type[1] ≝
 { globals: list ident
 ; sparams:> sem_params
 ; exit: cpointer
 ; genv2: genv globals sparams
 }.

(* Paolo: with structured traces, eval need not emit labels. However, this
  changes trans_system. For now, just putting a dummy thing for
  the transition. *)
definition joint_exec: trans_system io_out io_in ≝
  mk_trans_system … evaluation_parameters (λG. state_pc G)
   (λG.is_final (globals G) G (genv2 G) (exit G))
   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).

definition make_global :
 ∀pars: sem_params.
  joint_program pars → evaluation_parameters
≝
 λpars.
 (* Invariant: a -1 block is unused in common/Globalenvs *)
 let b ≝ mk_block Code (-1) in
 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
  (λp. mk_evaluation_parameters
    (prog_var_names … p)
    (mk_sem_params … pars)
    ptr
    (globalenv_noinit … p)
  ).
% qed.

axiom ExternalMain: String.

definition make_initial_state :
 ∀pars: sem_params.
 ∀p: joint_program … pars. res (state_pc pars) ≝
λpars,p.
  let sem_globals ≝ make_global pars p in
  let ge ≝ genv2 sem_globals in
  let m ≝ alloc_mem … p in
  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
  let main ≝ prog_main … p in
  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
  (* use exit sem_globals as ra and call_dest_for_main as dest *)
  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; 
  match main_fd with
  [ Internal fn ⇒
    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
qed.

definition joint_fullexec :
 ∀pars:sem_params.fullexec io_out io_in ≝
 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
*)