source: src/joint/semantics.ma @ 2557

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 ℕ
}.

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
  (* 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 Code (-1), refl …» one.

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 (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_pc p → state_pc p ≝
 λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s.

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

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 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]
 ].

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: bool (* ident or ptr *) → 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 → F globals (* current *) → state st_pars → res (state st_pars)
  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    ident → F globals (* 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 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 (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 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.

axiom NoSuccessor : String.
definition next_of_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
    [ step_seq _ => return nxt
    | COND _ _ => Error … [MSG NoSuccessor]
    ]
  | _ ⇒ Error … [MSG NoSuccessor]
  ].

definition eval_seq_no_pc :
 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
 joint_closed_internal_function p globals →
  joint_seq p globals → state p →
  res (state p) ≝
 λp,globals,ge,curr_id,curr_fn,seq,st.
 match seq with
  [ extension_seq c ⇒
    eval_ext_seq … ge c curr_id 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
  | _ ⇒ 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
  [@eq_identifier_elim #H * >H %1 % ]
  #G %2 @IH @G
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 …).

(* to be used in implementations *)
definition block_of_call_id ≝  λF.λsp:sem_state_params.
  λge: genv_t F.λid.λst:state sp.
  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.

axiom MissingStackSize : String.

definition eval_internal_call ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
! 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 allocate_locals … p (joint_if_locals … fn) st'.

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

definition eval_seq_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 … (is_inl … 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_seq_advance : 
 ∀p:sem_params.∀globals.∀ge:genv p globals.
  joint_seq p globals → succ p → state_pc p →
  IO io_out io_in (state_pc p) ≝
  λp,globals,ge,s,nxt,st.
  match s with
  [ CALL f args dest ⇒
    eval_seq_call … ge f args dest nxt st
  | _ ⇒ return next … nxt st
  ].

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

definition eval_return ≝
λp : sem_params.λglobals : list ident.λge : genv p globals.
λcurr_id.λcurr_fn : joint_closed_internal_function ??.
λst : state p.
! st' ← pop_frame … ge curr_id curr_fn st ;
! nxt ← next_of_pc … ge (pc … st') ;
return
  set_last_pop … (pc … st') (next … nxt 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_fn : joint_closed_internal_function ??.
λ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' ← 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 ⇒
  let curr_dest ≝ joint_if_result ?? curr_fn in
  ! st' ← eval_external_call … efd args curr_dest st ;
  eval_return … ge curr_f curr_fn 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
    [ step_seq s ⇒
      eval_seq_advance … ge s nxt st
    | 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
    ]
  | final s ⇒
    match s with
    [ GOTO l ⇒ goto … ge l st
    | RETURN ⇒ eval_return … ge curr_id curr_fn st
    | TAILCALL _ f args ⇒
      eval_tailcall … ge f args curr_id curr_fn 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 fn s st : IO ???;
  let st'' ≝ set_no_pc … st' st in
  eval_statement_advance … ge id fn s 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: ∀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 ⇒ 
      do st' ← pop_frame … ge id fn 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).
*)