source: src/joint/semantics.ma @ 2486

include "common/Globalenvs.ma".
include "common/IO.ma".
(* include "common/SmallstepExec.ma". *)
include "joint/BEMem.ma".
include "joint/Joint.ma".
include "ASM/I8051bis.ma".
include "common/extraGlobalenvs.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_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ
}.

definition stack_sizes_lift :
∀pars_in, pars_out : params.
∀trans : ∀globals.joint_closed_internal_function pars_in globals →
                  joint_closed_internal_function pars_out globals.
∀prog_in : program (joint_function pars_in) ℕ.
let prog_out ≝
  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
λpars_in,pars_out,prog_in,trans,stack_sizes.
λi.stack_sizes «i, if_propagate … (pi2 … i)».

definition genv ≝ λp.genv_gen (joint_closed_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 ?.

record sem_state_params : Type[1] ≝
 { framesT: Type[0]
 ; empty_framesT: framesT
 ; regsT : Type[0]
 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
 ; load_sp : regsT → res xpointer
 ; save_sp : regsT → xpointer → regsT
 }.

inductive internal_stack : Type[0] ≝
| empty_is : internal_stack
| one_is : beval → internal_stack
| both_is : beval → beval → internal_stack.

axiom InternalStackFull : String.
axiom InternalStackEmpty : String.

definition is_push : internal_stack → beval → res internal_stack ≝
λis,bv.match is with
[ empty_is ⇒ return one_is bv
| one_is bv' ⇒ return both_is bv' bv
| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
].

definition is_pop : internal_stack → res (beval × internal_stack) ≝
λis.match is with
[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
| one_is bv' ⇒ return 〈bv', empty_is〉
| both_is bv bv' ⇒ return 〈bv', one_is bv〉
].

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

definition sp ≝ λp,st.load_sp p (regs ? st).

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

definition set_m: ∀p. bemem → state p → state p ≝
 λp,m,st. mk_state p (st_frms …st) (istack … 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) (istack … st) (carry … st) regs (m … st).

definition set_sp: ∀p. ? → state p → state p ≝
 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).

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

definition set_istack: ∀p. internal_stack → state p → state p ≝
 λp,is,st. mk_state … (st_frms … st) is (carry … st) (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 (istack … st) (carry … st) (regs … st) (m … st).

axiom BadProgramCounter : String.

(*
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 *)
*)

(* bevals hold a function pointer (BVptr) *)
definition funct_of_bevals : ∀F,ge.
  beval → beval → option (Σi.is_function F ge i) ≝
λF,ge,dpl,dph.
! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *)
   funct_of_block … (pblock ptr)
else None ?.

axiom ProgramCounterOutOfCode : String.
axiom PointNotFound : String.
axiom LabelNotFound : String.
axiom MissingSymbol : String.
axiom FailedLoad : String.
axiom BadFunction : String.
axiom SuccessorNotProvided : String.
axiom BadPointer : String.

(* this can replace graph_fetch function and lin_fetch_function *)
definition fetch_function:
 ∀F.
 ∀ge : genv_t (fundef F).
  program_counter →
  res (Σi.is_internal_function … ge i) ≝
 λpars,ge,p.
 opt_to_res … [MSG BadFunction; MSG BadPointer]
    (int_funct_of_block … ge (pc_block p)).

record sem_unserialized_params
  (uns_pars : unserialized_params)
  (F : list ident → Type[0]) : 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)

  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
  ; save_frame: call_dest uns_pars → state_pc 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 → call_args … uns_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)
  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars)
  }.

definition allocate_locals :
  ∀p,F.∀sup : sem_unserialized_params p F.
  list (localsT p) → state sup → state sup ≝
  λp,F,sup,l,st.
  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
  set_regs … r st. 

definition helper_def_retrieve : 
  ∀X : ? → ? → ? → Type[0].
  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
  ∀up,F.∀p : 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 : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
  ∀up,F.∀p : 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 : 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 FailedStore: String.

definition push: ∀p.state p → beval → res (state p) ≝
 λp,st,v.
 ! is ← is_push (istack … st) v ;
 return set_istack … is st.

definition pop: ∀p. state p → res (beval × (state p)) ≝
 λp,st.
 ! 〈bv, is〉 ← is_pop (istack … st) ;
 return 〈bv, set_istack … is st〉.

definition save_ra : ∀p. state p → program_counter → res (state p) ≝
 λp,st,l.
  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
  ! st' ← push … st addrl;
  push … st' addrh.

definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
 λp,st.
  ! 〈addrh, st'〉 ← pop … st;
  ! 〈addrl, st''〉 ← pop … st';
  ! pr ← pc_of_bevals [addrh; addrl];
  return 〈pr, st''〉.

(* parameters that are defined by serialization *)
record more_sem_params (pp : params) : Type[1] ≝
  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
  ; offset_of_point : code_point pp → Pos
  ; point_of_offset : Pos → code_point pp
  ; point_of_offset_of_point :
    ∀pt.point_of_offset (offset_of_point pt) = pt
  ; offset_of_point_of_offset :
    ∀o.offset_of_point (point_of_offset o) = 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.*)

definition pc_of_point : ∀p.more_sem_params p →
  program_counter → code_point p → program_counter ≝
  λp,msp,ptr,pt.
  mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).

definition point_of_pc :
  ∀p.more_sem_params p → program_counter → code_point p ≝
  λp,msp,ptr.point_of_offset p msp (pc_offset ptr).

lemma point_of_pointer_of_point :
  ∀p,msp.∀ptr,pt.
  point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
#p #msp #ptr #pt normalize // qed.

lemma pointer_of_point_block :
  ∀p,msp,ptr,pt.
  pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
#p #msp #ptr #pt % qed. (* can probably do without *)

lemma pointer_of_point_uses_block :
  ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
    pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
#p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.

lemma pointer_of_point_of_pointer :
  ∀p,msp.∀ptr1,ptr2.
    pc_block ptr1 = pc_block ptr2 →
    pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
#p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.

definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
  ∀ge : genv_t (joint_function p globals). program_counter →
  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
  λp,msp,globals,ge,ptr.
  ! f ← fetch_function … ge ptr ;
  let fn ≝ if_of_function … f in
  let pt ≝ point_of_pc ? msp ptr in
  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
  return 〈f, stmt〉.

definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
  genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
  λp,msp,globals,ge,ptr,lbl.
  ! f ← fetch_function … ge ptr ;
  let fn ≝ if_of_function …  ge f in
  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
            (point_of_label … (joint_if_code … fn) lbl) ;
  return pc_of_point p msp ptr pt.

definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
  program_counter → succ p → program_counter ≝
  λp,msp,ptr,nxt.
  let curr ≝ point_of_pc p msp ptr in
  pc_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: ∀p : sem_params.∀globals.
  genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
 λp,globals,ge,l,st,b.
  ! newpc ← pc_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_pc p → state_pc p ≝
 λp,l,st.
 let newpc ≝ succ_pc ? p … (pc … st) l in
 mk_state_pc … st newpc.


definition function_of_call ≝ λp:sem_params.λglobals.
  λge: genv_t (joint_function p globals).λst : state p.λf.
  match f with
  [ inl id ⇒
    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
  | inr addr ⇒
    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
  ].

(* Paolo: why external calls do not need args?? *)
definition eval_external_call ≝
λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
      ! params ← fetch_external_args … p' fn st args : 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
      set_result … p' vs dest st.

definition eval_internal_call_pc ≝
λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
let fn ≝ if_of_function … ge i in
let l' ≝ joint_if_entry ?? fn in
mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
[ @block_of_funct_ident_is_code
| cases i /2 by internal_function_is_function/
]
qed.

definition eval_internal_call_no_pc ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
let fn ≝ if_of_function … ge i in
let stack_size ≝ stack_sizes … ge i in
! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
return allocate_locals … p (joint_if_locals … fn) st.

definition eval_seq_no_pc :
 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
  state p → 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_block ≝ opt_safe ? (find_symbol … ge id) ? in
    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
    ! 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 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 ⇒
    ! 〈v, st'〉 ← 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 f args dest ⇒
    ! fn ← function_of_call … ge st f : IO ???;
    match description_of_function … fn return λx.description_of_function … fn = x → ? with
    [ Internal fd ⇒ λprf.
      eval_internal_call_no_pc … ge «fn, ?» args st  (* only pc changes *)
    | External fd ⇒ λ_.eval_external_call … fd args dest st
    ] (refl …)
  | _ ⇒ return st
  ].
[ @hide_prf
  @find_symbol_in_globals
  lapply prf
  elim globals [*]
  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
  #G %2 @IH @G
| @(description_of_internal_function … prf)
]
qed.

definition eval_seq_pc : 
 ∀p:sem_params.∀globals.∀ge:genv p globals.
  state_pc p → ? → joint_seq p globals →
  res (state_pc p) ≝
  λp,globals,ge,st,nxt,s.
  match s with
  [ CALL f args dest ⇒
    ! fn ← function_of_call … ge st f;
    match ? return λx.description_of_function … fn = x → ? with
    [ Internal _ ⇒ λprf.
      let pc ≝ eval_internal_call_pc … ge «fn, ?» in
      ! st' ← save_frame … dest st ;
      return mk_state_pc … st' pc
    | External _ ⇒ λ_.return next p nxt st
    ] (refl …)
  | _ ⇒ return next p nxt st
  ].
@(description_of_internal_function … prf)
qed.

definition eval_statement :
 ∀p:sem_params.∀globals.∀ge:genv p globals.
 (Σi.is_internal_function … ge i) → state_pc p →
  ∀s:joint_statement p globals.
  IO io_out io_in (state_pc p) ≝
  λp,g,ge,curr_fn,st,s.
  match s with
  [ sequential s next ⇒
    match s return λ_.IO ??? with
    [ step_seq s ⇒
      ! st' ← eval_seq_no_pc … ge curr_fn st s ;
      let st'' ≝ mk_state_pc … st' (pc … st) in
      eval_seq_pc ?? ge st'' next s
    | COND a l ⇒
      ! v ← acca_retrieve … st a ;
      ! b ← bool_of_beval … v ;
      ! pc' ←
        if b then
          pc_of_label ? p … ge (pc … st) l
        else
          return succ_pc ? p (pc … st) next ;
      return mk_state_pc … st pc'
    ]
  | final s ⇒
    match s with
    [ GOTO l ⇒
      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
      return mk_state_pc … st pc'
    | RETURN ⇒ pop_frame … curr_fn st
    | TAILCALL _ f args ⇒
      ! fn ← function_of_call … ge st f : IO ???;
      match ? return λx.description_of_function … fn = x → ? with
      [ Internal _ ⇒ λprf.
        let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
        return mk_state_pc … st pc'
      | External fd ⇒ λ_.
        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
        ! st' ← eval_external_call ??? fd args curr_dest st ;
        pop_frame … curr_fn st'
      ] (refl …)
    ]
  ].
@(description_of_internal_function … prf)
qed.

definition eval_state : ∀p:sem_params. ∀globals: list ident.
  genv p globals →
  state_pc p → IO io_out io_in (state_pc p) ≝
  λp,globals,ge,st.
  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
  eval_statement … ge fn st 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: ∀p: sem_params.∀globals.
  genv p globals → program_counter → state_pc p → option int ≝
 λp,globals,ge,exit,st.res_to_opt ? (
  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
  let fn ≝ if_of_function … f in
  match s with
  [ final s' ⇒
    match s' with
    [ RETURN ⇒ 
      do st' ← pop_frame … ge f st;
      if eq_program_counter (pc … st') 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: program_counter
 ; 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).
*)