include "basics/lists/list.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
include "joint/BEMem.ma".
include "joint/Joint_paolo.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) ??? *)

definition genv ≝ λglobals.λp:params. genv_t (joint_function globals p).
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: beval
 ; regs: regsT semp
 ; m: bemem
 }.

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. beval → 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 globals pars →
  block →
  res (joint_internal_function … pars) ≝
  λpars,blobals,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 globals pars →
  cpointer →
  res (joint_internal_function … pars) ≝
 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).

inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
  | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
  | Proceed  : step_flow p globals labels. (* go to implicit successor *)

definition step_flow_cons : ∀p,globals,l,lbls.
  step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
  λp,globals,l1,l2,flow.match flow with
  [ Redirect l ⇒ Redirect … «l, ?»
  | Init id f args dest ⇒ Init … id f args dest
  | Proceed ⇒ Proceed ???
  ]. cases l /2 by or_intror/ qed.
coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
  step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).

definition step_flow_append_l : ∀p,globals,l1,l2.
  step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
  λp,globals,l1,l2,flow.match flow with
  [ Redirect l ⇒ Redirect … «l, ?»
  | Init id f args dest ⇒ Init … id f args dest
  | Proceed ⇒ Proceed ???
  ]. cases l /2 by Exists_append_l/ qed.
coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
  step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).

definition step_flow_append_r : ∀p,globals,l1,l2.
  step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
  λp,globals,l1,l2,flow.match flow with
  [ Redirect l ⇒ Redirect … «l, ?»
  | Init id f args dest ⇒ Init … id f args dest
  | Proceed ⇒ Proceed ???
  ]. cases l /2 by Exists_append_r/ qed.
coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
  step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).

inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
  | FEnd  : fin_step_flow p globals labels. (* end flow *)

definition fin_step_flow_cons : ∀p,globals,l,lbls.
  fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
  λp,globals,l1,l2,flow.match flow with
  [ FRedirect l ⇒ FRedirect … «l, ?»
  | FTailInit id f args ⇒ FTailInit … id f args
  | FEnd ⇒ FEnd ???
  ]. cases l /2 by or_intror/ qed.
coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
  fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).

definition fin_step_flow_append_l : ∀p,globals,l1,l2.
  fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
  λp,globals,l1,l2,flow.match flow with
  [ FRedirect l ⇒ FRedirect … «l, ?»
  | FTailInit id f args ⇒ FTailInit … id f args
  | FEnd ⇒ FEnd ???
  ]. cases l /2 by Exists_append_l/ qed.
coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
  fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).

definition fin_step_flow_append_r : ∀p,globals,l1,l2.
  fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
  λp,globals,l1,l2,flow.match flow with
  [ FRedirect l ⇒ FRedirect … «l, ?»
  | FTailInit id f args ⇒ FTailInit … id f args
  | FEnd ⇒ FEnd ???
  ]. cases l /2 by Exists_append_r/ qed.
coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
  fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).

record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
  { st_pars :> sem_state_params
  ; 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 → framesT 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 → state st_pars → res (state st_pars)
  ; call_args_for_main: call_args uns_pars
  ; call_dest_for_main: call_dest uns_pars
 }.


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

definition helper_def_store :
  ∀X : ? → ? → Type[0].
  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
  λX,f,up,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.λp : more_sem_unserialized_params up.λst : state 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:
 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
  genv globals p → state p' → block → call_args p → call_dest p →
    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
 λglobals,p,p',lbls,ge,st,b,args,dest.
  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge b) : IO ? io_in ?); 
    match fd with
    [ Internal fn ⇒
      return 〈Init … (block_id b) fn 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 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) //
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) //
qed.
  
definition save_ra : ∀p. state p → cpointer → res (state p) ≝
 λp,st,l.
  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
  ! 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 ← code_pointer_of_address 〈addrh, addrl〉;
  return 〈st'', pr〉.

(* parameters that need full params to have type of functions,
   but are still independent of serialization *)
record more_sem_genv_params (pp : params) : Type[1] ≝
  { msu_pars :> more_sem_unserialized_params pp
  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
  (* change of pc must be left to *_flow execution *)
  ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
      state msu_pars →
      IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
  ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
      state msu_pars →
      IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
  }.

(* parameters that are defined by serialization *)
record more_sem_params (pp : params) : Type[1] ≝
  { msg_pars :> more_sem_genv_params pp
  ; offset_of_point : code_point pp → offset
  ; point_of_offset : offset → option (code_point pp)
  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
  }.

definition pointer_of_point : ∀p.more_sem_params p →
  cpointer→ code_point p → cpointer ≝
  λp,msp,ptr,pt.
    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
[ elim ptr #ptr' #EQ <EQ @pok
| %] qed.

axiom BadOffsetForCodePoint : String.

definition point_of_pointer :
  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
    (point_of_offset p msp (poff ptr)).

lemma point_of_pointer_of_point :
  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
#p #msp #ptr #pt normalize
>point_of_offset_of_point %
qed.

lemma pointer_of_point_block :
  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
/ by refl/
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 ** #ty1 #bl1 #H1 #o1 #EQ1
        ** #ty2 #bl2 #H2 #o2 #EQ2
#pt #EQ3 destruct normalize //
qed.

lemma pointer_of_point_of_pointer :
  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
    pointer_of_point p msp ptr2 pt = ptr1.
#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
destruct
lapply (offset_of_point_of_offset p msp o1)
normalize
elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
#pt' #EQ #EQ' destruct %
qed.


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

definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv globals p → cpointer → res (joint_statement p globals) ≝
  λp,msp,globals,ge,ptr.
  ! pt ← point_of_pointer ? msp ptr ;
  ! fn ← fetch_function … ge ptr ;
  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
  
definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv globals p → block → label → res cpointer ≝
  λp,msp,globals,ge,b,lbl.
  ! fn ← function_of_block … ge b ;
  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
            (point_of_label … (joint_if_code … fn) lbl) ;
  return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.

definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv globals p → cpointer → label → res cpointer ≝
  λp,msp,globals,ge,ptr.
  pointer_of_label_in_block p msp globals ge (pblock ptr).

definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
  cpointer → succ p → res cpointer ≝
  λp,msp,ptr,nxt.
  ! curr ← point_of_pointer p msp ptr ;
  return 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 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 globals p → label → state p → block → res (state_pc p) ≝
 λglobals,p,ge,l,st,b.
  ! newpc ← pointer_of_label_in_block ? 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.

(* the optional point must be given only for calls *)
definition eval_step :
 ∀globals.∀p:sem_params. genv globals p → state p →
  ∀s:joint_step p globals.
  IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
 λglobals,p,ge,st,seq.
  match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
  [ extension c ⇒
    exec_extended … ge c st
  | COST_LABEL cl ⇒
    return 〈Proceed ???, st〉
  | COMMENT c ⇒
    return 〈Proceed ???, 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);
    ! st ← acca_store p … dst v st ;
    return 〈Proceed ???, 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 〈Proceed ???, set_m … m' 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〉
  | ADDRESS ident prf ldest hdest ⇒
    let addr ≝ opt_safe ? (find_symbol … ge ident) ? in
    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
    ! st' ← dpl_store … ldest laddr st;
    ! st'' ← dph_store … hdest haddr st';
    return 〈Proceed ???, 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 … dacc_a v' st;
    return 〈Proceed ???, st〉
  | OP2 op dacc_a sacc_a src ⇒
    ! v1 ← acca_arg_retrieve … st sacc_a;
    ! v1 ← Byte_of_val v1;
    ! v2 ← snd_arg_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 … dacc_a v' st;
      let st'' ≝ set_carry … carry st' in
    return 〈Proceed ???, st''〉
  | CLEAR_CARRY ⇒
    let st' ≝ set_carry … BVfalse st in
    return 〈Proceed ???, st'〉
  | SET_CARRY ⇒
    let st' ≝ set_carry … BVtrue st in
    return 〈Proceed ???, st'〉
  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
    ! v1 ← Byte_of_val v1;
    ! v2 ← accb_arg_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 … dacc_a_reg v1' st;
    ! st'' ← accb_store … dacc_b_reg v2' st';
    return 〈Proceed ???, st''〉
  | POP dst ⇒
    ! 〈st',v〉 ← pop p st;
    ! st'' ← acca_store p p dst v st';
    return 〈Proceed ???, st''〉
  | PUSH src ⇒
    ! v ← acca_arg_retrieve … st src;
    ! st ← push … st v;
    return 〈Proceed ???, st〉
  | MOVE dst_src ⇒
    ! st ← pair_reg_move … st dst_src ;
    return 〈Proceed ???, st〉
  | CALL_ID id args dest ⇒
    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    eval_call_block … ge st b args dest
  ].
  [ cases addr //
  | (* TODO: to prove *)
    elim daemon
  | %1 %
  ] qed.

definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
  state p → ∀s : joint_fin_step … p globals.
  IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
 λglobals,p,ge,st,s.
  match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
    [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
    | RETURN ⇒ return 〈FEnd ???, st〉
    | extension_fin c ⇒ exec_fin_extended … ge c st
    ]. %1 % qed.


definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
  state p → Z → joint_internal_function globals p → call_args p →
  res (state_pc p) ≝
  λglobals,p,ge,st,id,fn,args.
    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
              args st ;
    let regs ≝ foldr ?? (allocate_local p 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 Code (mk_block Code id) ? (mk_offset 0) in
    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
    return mk_state_pc ? st' pc. % qed.

(* The pointer provided is the one to the *next* instruction.
   The boolean tells wether a flow changement has occurred (i.e.
   a non Proceed cmd was issued). Used in linking block evaluation
   with regular one *)
definition eval_step_flow :
 ∀globals.∀p:sem_params.∀lbls.genv globals p →
  state p → cpointer → step_flow p globals lbls →
    res (bool × (state_pc p)) ≝
 λglobals,p,lbls,ge,st,nxt,cmd.
 match cmd with
  [ Redirect l ⇒
    ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
  | Init id fn args dest ⇒
    let st' ≝ set_frms … (save_frame … nxt dest st) st in
    ! st ← do_call ?? ge st' id fn args ;
    return 〈true, st〉
  | Proceed ⇒
    return 〈false, mk_state_pc ? st nxt〉
  ].

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

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

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

definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
  state_pc p → IO io_out io_in (state_pc p) ≝
  λglobals,p,ge,st.
  ! 〈flag,st'〉 ← eval_state_flag … ge st ;
  return st'.

(* 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 globals p → cpointer → state_pc p → option int ≝
 λglobals,p,ge,exit,st.res_to_opt ? (
  do 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 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).