source: src/joint/joint_semantics.ma @ 2876

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 : ident → option ℕ
; get_pc_from_label : ident (* current function *) → label → res program_counter
}.

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 called at the start of each function call *)
 ; 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.

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: option(framesT semp) 
 ; istack : internal_stack
 ; carry: bebit
 ; regs: regsT semp
 ; stack_usage : ℕ
 ; 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
  (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
  ; last_pop : program_counter
  }.

(* special program counter that is guaranteed to not correspond to anything *)
definition exit_pc : program_counter ≝
  mk_program_counter «mk_block (-1), refl …» one.

definition null_pc : Pos →  program_counter ≝ λpos.
    mk_program_counter «dummy_block_code, refl …» pos.

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

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

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

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

definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
 λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.

definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st)
 (stack_usage … st) (m … st).

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

(* this can replace graph_fetch function and lin_fetch_function *)
definition fetch_function:
 ∀F.
 ∀ge : genv_t F.
  (Σb.block_region b = Code) →
  res (ident×F) ≝
 λF,ge,bl.
 opt_to_res … [MSG BadFunction]
  (! id ← symbol_for_block … ge bl ;
   ! fd ← find_funct_ptr … ge bl ;
   return 〈id, fd〉).

definition fetch_internal_function :
 ∀F.
 ∀ge : genv_t (fundef F).
  (Σb.block_region b = Code) →
  res (ident×F) ≝
 λF,ge,bl.
 ! 〈id, fd〉 ← fetch_function … ge bl ;
 match fd with
 [ Internal ifd ⇒ return 〈id, ifd〉
 | _ ⇒ Error … [MSG BadFunction]
 ].
 
lemma fetch_internal_function_no_minus_one :
  ∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #id #EQ1 #EQ2 destruct
 whd in match fetch_internal_function;
  whd in match fetch_function; normalize nodelta
  >globalenv_no_minus_one
  cases (symbol_for_block ???) normalize //
qed.

inductive call_kind : Type[0] ≝
| PTR : call_kind
| ID : call_kind.

definition kind_of_call :
  ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝
  λp,f.match f with [ inl _ ⇒ ID | inr _ ⇒ PTR ].

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)
  
  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
  ; save_frame: call_kind → 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_t (fundef (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 →
    ident (* current *) → state st_pars → res (state st_pars)
  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    ident (* current *) → call_dest uns_pars (* current ret *) →
      state st_pars → res (state st_pars × program_counter)
  }.

(*
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.
 
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 push_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 pop_ra : ∀p.state p → res (state p × program_counter) ≝
 λp,st.
  ! 〈addrh, st'〉 ← pop … st;
  ! 〈addrl, st''〉 ← pop … st';
  ! pr ← pc_of_bevals [addrl; addrh];
  return 〈st'',pr〉.

(* parameters that are defined by serialization *)
record sem_params : Type[1] ≝
  { spp :> params
  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
  ; offset_of_point : code_point spp → Pos
  ; point_of_offset : Pos → code_point spp
  ; 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:sem_params.(Σb.block_region b = Code) →
  code_point p → program_counter ≝
  λp,bl,pt.
  mk_program_counter bl (offset_of_point p pt).

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

lemma point_of_pc_of_point :
  ∀p,bl,pt.
  point_of_pc p (pc_of_point p bl pt) = pt.
#p #bl #pt normalize // qed.

lemma pc_of_point_of_pc :
  ∀p,ptr.
    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
#p * #bl #off normalize >offset_of_point_of_offset % qed.

definition fetch_statement: ∀p : sem_params.∀globals.
  ∀ge : genv_t (joint_function p globals). program_counter →
  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
  λp,globals,ge,ptr.
  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
  let pt ≝ point_of_pc p ptr in
  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
  return 〈id, fn, stmt〉.

definition pc_of_label : ∀p : sem_params.∀globals.
  genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
  λp,globals,ge,bl,lbl.
  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
            (point_of_label … (joint_if_code … fn) lbl) ;
  return mk_program_counter bl (offset_of_point p pt).

definition succ_pc : ∀p : sem_params.
  program_counter → succ p → program_counter ≝
  λp,ptr,nxt.
  let curr ≝ point_of_pc p ptr in
  pc_of_point p (pc_block 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_pc p → res (state_pc p) ≝
 λp,globals,ge,l,st.
  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
  return set_pc … newpc st.

(*
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 … (pc … st) l in
 set_pc … newpc st.

definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
  program_counter → res (succ p) ≝
λp,globals,ge,pc.
  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
  match stmt with
  [ sequential s nxt ⇒
    match s with
    [ CALL _ _ _ ⇒ return nxt
    | _ ⇒ Error … [MSG NoSuccessor]
    ]
  | _ ⇒ Error … [MSG NoSuccessor]
  ].

lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A.
(x = y → P true) → (x ≠ y → P false) → P (x == y).
#A #P #x #y #H1 #H2 inversion (x == y) #EQ
[ @H1 @(proj1 … (eqb_true … ) EQ) | @H2 % #EQ' destruct
  >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed.

definition eval_seq_no_pc :
 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
  joint_seq p globals → state p →
  res (state p) ≝
 λp,globals,ge,curr_id,seq,st.
 match seq with
  [ extension_seq c ⇒
    eval_ext_seq … ge c curr_id 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
  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
  ].
  @hide_prf
  @find_symbol_in_globals
  lapply prf
  elim globals [*]
  #hd #tl #IH #H elim (orb_Prop_true … H) -H
  [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ]
qed.

definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
λbl.match block_region bl
  return λx.block_region bl = x → option (Σb.block_region b = Code) with
  [ Code ⇒ λprf.Some ? «bl, prf»
  | XData ⇒ λ_.None ?
  ] (refl …).

definition block_of_funct_id ≝  λF.λsp:sem_state_params.
  λge: genv_t F.λid.
  opt_to_res … [MSG BadFunction; CTX … id] (
    ! bl ← find_symbol … ge id; 
    code_block_of_block bl).
  
definition block_of_call ≝ λp : sem_params.
  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
  ! bl ← match f with
    [ inl id ⇒
      opt_to_res … [MSG BadFunction; CTX … id]
        (find_symbol … ge id)
    | inr addr ⇒
      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
      if eq_bv … (bv_zero …) (offv (poff ptr)) then
        return pblock ptr
      else
        Error … [MSG BadFunction; MSG BadPointer]
    ] ;
  opt_to_res … [MSG BadFunction; MSG BadPointer]
    (code_block_of_block bl).

definition eval_external_call ≝
λp : sem_params.λ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 increment_stack_usage : ∀p.ℕ → state p → state p ≝
λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
  (stack_usage … st + n) (m … st).

definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
  (stack_usage … st - n) (m … st).

definition eval_internal_call ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
λst : state p.
! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
return increment_stack_usage … stack_size st'.

definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].

definition eval_call ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
λst : state_pc p.
! bl ← block_of_call … ge f st : IO ???;
! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
match fd with
[ Internal ifd ⇒
  ! st' ← save_frame … (kind_of_call … f) dest st ;
  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
  return mk_state_pc … st'' pc (last_pop … st)
| External efd ⇒
  ! st' ← eval_external_call … efd args dest st ;
  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
].

definition eval_statement_no_pc :
 ∀p:sem_params.∀globals.∀ge:genv p globals.
 ident (* current *) →
 joint_statement p globals → state p → res (state p) ≝
 λp,globals,ge,curr_id,s,st.
  match s with
  [ sequential s next ⇒
    match s with
    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st 
    | _ ⇒ return st
    ]
  | _ ⇒ return st
  ].

definition eval_return ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.
λcurr_id.λcurr_ret : call_dest p.
λst : state p.
! st' ← pop_frame … ge curr_id curr_ret st ;
! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
let st'' ≝ decrement_stack_usage … stack_size (\fst st') in
! nxt ← next_of_call_pc … ge (\snd … st') ;
return
  next … nxt (set_last_pop … (\snd … st') 〈st'', \snd st'〉) (* now address pushed on stack are calling ones! *).

definition eval_tailcall ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
λcurr_ret : call_dest p.
λst : state_pc p.
! bl ← block_of_call … ge f st : IO ???;
! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
match fd with
[ Internal ifd ⇒
  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
  let st' ≝ decrement_stack_usage … stack_size st in
  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
  return mk_state_pc … st'' pc (last_pop … st)
| External efd ⇒
  ! st' ← eval_external_call … efd args curr_ret st ;
  eval_return … ge curr_f curr_ret st
].

definition eval_statement_advance :
 ∀p:sem_params.∀globals.∀ge:genv p globals.
 ident → joint_closed_internal_function p globals →
  joint_statement p globals → state_pc p →
  IO io_out io_in (state_pc p) ≝
  λp,g,ge,curr_id,curr_fn,s,st.
  match s return λ_.IO ??? with
  [ sequential s nxt ⇒
    match s return λ_.IO ??? with
    [ COND a l ⇒
      ! v ← acca_retrieve … st a ;
      ! b ← bool_of_beval … v ;
      if b then
        goto … ge l st
      else
        return next … nxt st
    | CALL f args dest ⇒
      eval_call … ge f args dest nxt st
    | _ ⇒ return next … nxt st
    ]
  | final s ⇒
    let curr_ret ≝ joint_if_result … curr_fn in
    match s with
    [ GOTO l ⇒ goto … ge l st
    | RETURN ⇒ eval_return … ge curr_id curr_ret st
    | TAILCALL _ f args ⇒
      eval_tailcall … ge f args curr_id curr_ret st
    ]
  | FCOND _ a lbltrue lblfalse ⇒
    ! v ← acca_retrieve … st a ;
    ! b ← bool_of_beval … v ;
    if b then
      goto … ge lbltrue st
    else
      goto … ge lblfalse st
  ].

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.
  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
  let st'' ≝ set_no_pc … st' st in
  eval_statement_advance … ge id fn s st''.

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 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
  match s with
  [ final s' ⇒
    match s' with
    [ RETURN ⇒
      let curr_ret ≝ joint_if_result … fn in
      do st' ← pop_frame … ge id curr_ret st;
      if eq_program_counter (\snd … st') exit then 
      do vals ← read_result … ge curr_ret st ;
        Word_of_list_beval vals
      else
        Error ? [ ]
   | _ ⇒ Error ? [ ]
   ]
 | _ ⇒ Error ? [ ]
 ]).