Changeset 2457

Timestamp:

Nov 13, 2012, 11:30:23 AM (7 years ago)

Author:

tranquil

Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

Location:

src

Files:

• common/StatusSimulation.ma (modified) (18 diffs)
• joint/Joint.ma (modified) (4 diffs)
• joint/Traces.ma (modified) (6 diffs)
• joint/semantics.ma (modified) (13 diffs)
• joint/semanticsUtils.ma (moved) (moved from src/joint/SemanticUtils.ma)

src/common/StatusSimulation.ma

@@ -31 +31 @@
      necessary for as_after_return (typically just the program counter)
      maybe what function is called too? *)
-  ; call_rel : (Σs.as_classifier S1 s cl_call) →
-               (Σs.as_classifier S2 s cl_call) → Prop
+  ; ret_rel : S1 → S2 → Prop
   ; sim_final :
     ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
@@ -48 +47 @@
 definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
 
-definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
-  ∀s1_pre,s2_pre.call_rel … R s1_pre s2_pre →
-                 as_after_return S1 s1_pre s1 →
-                 as_after_return S2 s2_pre s2.
+definition call_rel ≝ λS1,S2.λR : status_rel S1 S2.
+  λs1_pre,s2_pre.
+  ∀s1_ret,s2_ret.as_after_return S1 s1_pre s1_ret →
+                 ret_rel ?? R s1_ret s2_ret →
+                 as_after_return S2 s2_pre s2_ret.
 
 (* the equivalent of a collapsable trace_any_label where we do not force
@@ -70 +70 @@
    S will mark semantic relation, C call relation, L label relation, R return relation *)
 
-record status_simulation
-  (S1 : abstract_status)
-  (S2 : abstract_status)
-  : Type[1] ≝
-  { sim_status_rel :> status_rel S1 S2
-  ; sim_execute :
+definition status_simulation ≝
+  λS1 : abstract_status.
+  λS2 : abstract_status.
+  λsim_status_rel : status_rel S1 S2.
     ∀st1,cl,st1',st2.as_execute S1 st1 st1' →
     sim_status_rel st1 st2 →
@@ -141 +139 @@
       sim_status_rel st1' st2' ∧
       label_rel … st1' st2'
-    ] prf
-  }.
+    ] prf.
 
 
@@ -287 +284 @@
 include alias "basics/logic.ma".
 
-let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)
+let rec status_simulation_produce_tlr S1 S2 R
 (* we start from this situation
      st1 →→→→tlr→→→→ st1'
@@ -306 +303 @@
   (tlr1 : trace_label_return S1 st1 st1')
   (taa2_pre : trace_any_any S2 st2_lab st2)
+  (sim_execute : status_simulation S1 S2 R)
   on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
   ∃st2_mid.∃st2'.
@@ -317 +315 @@
  | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
  ]
-and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)
+and status_simulation_produce_tll S1 S2 R
 (* we start from this situation
      st1 →→→→tll→→→ st1'
@@ -336 +334 @@
   (tll1 : trace_label_label S1 fl st1 st1')
   (taa2_pre : trace_any_any S2 st2_lab st2)
-  on tll1 : R st1 st2 → label_rel … st1 st2_lab → 
+  (sim_execute : status_simulation S1 S2 R)
+   on tll1 : R st1 st2 → label_rel … st1 st2_lab → 
     match fl with
     [ ends_with_ret ⇒
@@ -352 +351 @@
   [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
   ]
-and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)
+and status_simulation_produce_tal S1 S2 R
 (* we start from this situation
      st1 →→tal→→ st1'
@@ -380 +379 @@
   fl st1 st1' st2
   (tal1 : trace_any_label S1 fl st1 st1')
-  on tal1 : R st1 st2 →
+  (sim_execute : status_simulation S1 S2 R)
+   on tal1 : R st1 st2 →
     match fl with
     [ ends_with_ret ⇒
@@ -405 +405 @@
 [1,2,3: #st1_L_st2_lab ]
 [ (* tlr_base *)
-  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
+  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
   #st2_mid * #st2' * #tll2 #H
   %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
 | (* tlr_step *)
-  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
+  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
   #st2_mid * #tll2 ** #H1 #H2 #H3
-  elim (status_simulation_produce_tlr … tl1 (taa_base …) H1 H2)
+  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
   #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
   %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
   %{H4} %{H3 H5}
 | (* tll_base *)
-  lapply (status_simulation_produce_tal ?? R ??? st2 tal1 st1_R_st2)
+  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
   cases fl1' in tal1; normalize nodelta #tal1 *
   [3: * #_ #ABS elim (absurd … H ABS) ]
@@ -431 +431 @@
 | (* tal_base_non_return *) whd
   cases G #G'
-  elim (sim_execute … R … H st1_R_st2 G')
+  elim (sim_execute … H st1_R_st2 G')
   #st2' ** -st2 -st2'
   [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
@@ -445 +445 @@
   ]
 | (* tal_base_return *) whd
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
   ***** #ncost #J2 #K2
@@ -453 +453 @@
   %[ % | %[|%[|%[|%[| % ]]]]]]]
 | (* tal_base_call *) whd
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
   #st1_R_st2_mid #st1_L_st2_after_call
-  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
+  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
   #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
   [ #st2' #tlr2 *****
@@ -474 +474 @@
     ]
   ]
-  [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
+  [1,3: @(st1_C_st2 … st1_Rret_st2') assumption
   |*: whd <st1_L_st2' assumption
   ]
 | (* tal_step_call *)
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
   #st1_R_st2_mid #st1_L_st2_after_call
-  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
+  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
   #st2_after_ret * #st2' * #tlr2 * #taa2''
   ****
   #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
-  lapply (status_simulation_produce_tal … tl1 st1_R_st2')
+  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
   cases fl1' in tl1; #tl1 *
   [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
@@ -514 +514 @@
     ]
   ]
-  [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
+  [1,4,7,9: @(st1_C_st2 … st1_Rret_st2') assumption
   |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
     [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
@@ -523 +523 @@
   ]
 | (* step_default *)
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
-  lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid)
+  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
   cases fl1' in tl1; #tl1 *
   [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
@@ -728 +728 @@
 *)
   ∀S1,S2.
-  ∀R : status_simulation S1 S2.
+  ∀R.
   ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
-  label_rel … st1 st2 → R st1 st2 →
+  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
   ∃st2_lab,st2'.
   ∃ft2 : flat_trace S2 st2 st2_lab stack.
   ∃taa : trace_any_any S2 st2_lab st2'.
   label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
-#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 -st1' -stack
+#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl

src/joint/Joint.ma

@@ -28 +28 @@
 params : adds type of code and related properties *)
 
+(*
 inductive possible_flows : Type[0] ≝
 | Labels : list label → possible_flows
 | Call : possible_flows.
+*)
 
 inductive argument (T : Type[0]) : Type[0] ≝
@@ -82 +84 @@
  (* other instructions not fitting in the general framework *)
  ; ext_seq : Type[0]
-(* ; ext_branch : Type[0]
- ; ext_branch_labels : ext_branch → list label*)
- ; ext_call : Type[0]
- ; ext_tailcall : Type[0]
+ ; has_tailcalls : bool
  (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
  ; paramsT : Type[0]
@@ -143 +142 @@
   step_seq on _s : joint_seq ?? to joint_step ??.
 
-definition step_flows ≝ λp,globals.λs : joint_step p globals.
-  match s with
-  [ step_seq s ⇒
-    match s with
-    [ CALL _ _ _ ⇒ Call
-    | _ ⇒ Labels … [ ]
-    ]
-  | COND _ l ⇒ Labels … [l]
-  ].
-
 definition step_labels ≝
   λp, globals.λs : joint_step p globals.
-    match step_flows … s with
-    [ Labels lbls ⇒ lbls
-    | Call ⇒ [ ]
-    ].
+  match s with
+  [ step_seq s ⇒ [ ]
+  | COND _ l ⇒ [l]
+  ].
 
 definition step_forall_labels : ∀p.∀globals.
@@ -173 +162 @@
   | GOTO: label → joint_fin_step p
   | RETURN: joint_fin_step p
-  | tailcall : ext_tailcall p → joint_fin_step p.
-
-definition fin_step_flows ≝ λp.λs : joint_fin_step p.
+  | TAILCALL :
+    has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p)) →
+    call_args p → joint_fin_step p.
+
+definition fin_step_labels ≝ λp.λs : joint_fin_step p.
   match s with
-  [ GOTO l ⇒ Labels … [l]
-  | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
-  | _ ⇒ Labels … [ ]
+  [ GOTO l ⇒ [l]
+  | _ ⇒ [ ]
   ].
-
-definition fin_step_labels ≝
-  λp.λs : joint_fin_step p.
-    match fin_step_flows … s with
-    [ Labels lbls ⇒ lbls
-    | Call ⇒ [ ]
-    ].
 
 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
   | sequential: joint_step p globals → succ p → joint_statement p globals
   | final: joint_fin_step p → joint_statement p globals.
-
-coercion extension_fin_to_fin_step : ∀p : stmt_params.
-  ∀s : ext_tailcall p.joint_fin_step p ≝
-  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
 
 coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.

src/joint/Traces.ma

@@ -9 +9 @@
 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
  }.
- 
+
+axiom is_internal_function_of_program :
+  ∀p:params.joint_program p → ident → Prop.
+
+axiom is_internal_function_of_program_ok :
+  ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i →
+  is_internal_function_of_program p prog i.
+
 record prog_params : Type[1] ≝
  { prog_spars : sem_params
  ; prog : joint_program prog_spars
+ ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
  }.
@@ -27 +35 @@
   (prog_spars pars)
   «ptr, refl …»
-  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
+  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
  (* (prog_io pars) *).
-(* TODO or TOBEFOUND *)
-cases daemon
+[ @is_internal_function_of_program_ok @(pi2 … i)
+| (* TODO or TOBEFOUND *)
+  cases daemon
+]
 qed.
 
@@ -36 +46 @@
 ≝ make_global on _p : prog_params to evaluation_params.
 
-
-axiom ExternalMain : String.
+axiom BadMain : String.
 
 definition make_initial_state :
@@ -56 +65 @@
   ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
   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? *)
-  ].
+  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
+  match ? return λx.description_of_function … main = x → ? with
+  [ Internal fn ⇒ λprf.
+    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
+    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
+    ! pc' ← eval_internal_call_pc … ge main ;
+    return mk_state_pc … st' pc'
+  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
+  ] (refl …).
   [ %
+  | @(description_of_internal_function … prf)
   | cases spb normalize //
   ]
 qed.
 
-definition step_flow_classifier :
-  ∀p : evaluation_params.∀F,flows.
-  step_flow p F flows → status_class ≝
-  λp,F,flows,flow.match flow with
-  [ Redirect _ _ ⇒ cl_jump
-  | Init bl _ _ _ ⇒
-    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
-    [ Some f ⇒ cl_call
-    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
-    ]
-  | Proceed flows ⇒
-    match flows with
-    [ Labels lbls ⇒
-      match lbls with
-      [ nil ⇒ cl_other
-      | _ ⇒ cl_jump
-      ]
-    | _ ⇒ cl_other
-    ]
+definition joint_classify :
+  ∀p : evaluation_params.state_pc p → status_class ≝
+  λp,st.
+  match fetch_statement ? p … (ev_genv p) (pc … st) with
+  [ OK f_s ⇒
+    let 〈f, s〉 ≝ f_s in
+    match s with
+    [ sequential s _ ⇒
+      match s with
+      [ step_seq s ⇒
+        match s with
+        [ CALL f' args dest ⇒
+          match function_of_call ?? (ev_genv p) st f' with
+          [ OK fn ⇒
+            match description_of_function … fn with
+            [ Internal _ ⇒ cl_call
+            | External _ ⇒ cl_other
+            ]
+          | Error _ ⇒ cl_other
+          ]
+        | _ ⇒ cl_other
+        ]
+      | COND _ _ ⇒ cl_jump
+      ]
+    | final s ⇒
+      match s with
+      [ GOTO _ ⇒ cl_other
+      | RETURN ⇒ cl_return
+      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
+      ]
+    ]
+  | Error _ ⇒ cl_other
   ].
 
-definition fin_step_flow_classifier :
-  ∀p : evaluation_params.∀F,flows.
-  fin_step_flow p F flows → status_class ≝
-  λp,F,flows,flow.match flow with
-  [ FRedirect lbls _ ⇒
-    match lbls with
-    [ nil ⇒ (* not really possible, we don't care *) cl_other
-    | cons _ tl ⇒
-      match tl with
-      [ nil ⇒ (* only one label *) cl_other
-      | _ ⇒ (* fork *) cl_jump
-      ]
-    ]
-  | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
-    cl_other
-  | _ ⇒ cl_return
-  ].
+lemma joint_classify_call : ∀p : evaluation_params.∀st.
+  joint_classify p st = cl_call →
+  ∃f,f',args,dest,next,fn,fd.
+  fetch_statement ? p … (ev_genv p) (pc … st) =
+    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
+  function_of_call … (ev_genv p) st f' = OK ? fn ∧
+  description_of_function … (ev_genv p) fn = Internal … fd.
+#p #st
+whd in match joint_classify; normalize nodelta
+lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
+elim (fetch_statement ?????) in ⊢ (???%→%);
+[ * #f * [| * [ #lbl || #b #f #args ]]
+  [ * [| #a #lbl #next ]
+    [ *
+      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
+      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
+      | #ext ] #next
+      [ normalize nodelta
+        lapply (refl … (function_of_call … (ev_genv p) st f'))
+        elim (function_of_call ?????) in ⊢ (???%→%);
+        [ #fn normalize nodelta
+          lapply (refl … (description_of_function … (ev_genv p) fn))
+          elim (description_of_function ????) in ⊢ (???%→%); #fd
+          #EQfd
+        | #e
+        ] #EQfn
+      ]
+    ]
+  ]
+| #e
+] #EQfetch
+[|*: #ABS normalize in ABS; destruct(ABS) ]
+normalize nodelta #_
+%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
+qed.
+
+definition joint_call_ident : ∀p:evaluation_params.
+  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
+λp,st.
+match ?
+return λx.
+  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
+  match s with
+  [ sequential s next ⇒
+    match s with
+    [ step_seq s ⇒
+      match s with
+      [ CALL f' args dest ⇒
+        function_of_call … (ev_genv p) st f'
+      | _ ⇒ Error … [ ]
+      ]
+    | _ ⇒ Error … [ ]
+    ]
+  | _ ⇒ Error … [ ]
+  ] = x → ? with
+[ OK v ⇒ λ_.v
+| Error e ⇒ λABS.⊥
+] (refl …).
+@hide_prf
+elim (joint_classify_call … (pi2 … st))
+#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
+lapply ABS -ABS
+>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
+qed.
 
 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
@@ -150 +222 @@
    (* as_pc ≝ *) cpointerDeq
    (* as_pc_of ≝ *) (pc …)
-   (* as_classify ≝ *)
-    (λs.
-      match (
-        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
-        match stmt with
-        [ sequential stp nxt ⇒
-          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
-          return step_flow_classifier … flow
-        | final stp ⇒
-          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
-          return fin_step_flow_classifier … flow
-        ]) with
-      [ Value c ⇒ c
-      | _ ⇒ cl_other
-      ])
+   (* as_classify ≝ *) (joint_classify p)
    (* as_label_of_pc ≝ *)
     (λpc.
@@ -177 +235 @@
       succ_pc p p (pc … s1) nxt = return pc … s2)
    (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
-   (* as_call_ident_≝ *)
-   (λst.?). cases daemon (* TODO *) qed.
+   (* as_call_ident ≝ *) (joint_call_ident p).

src/joint/semantics.ma

@@ -11 +11 @@
    only the head is kept (or Undef if the list is empty) ??? *)
 
+definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
+  λi : ident.∃fd.
+    ! bl ← find_symbol … ge i ;
+    find_funct_ptr … ge bl = Some ? fd.
+
+definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) →
+fundef (F globals) ≝
+λF,globals,ge,i.
+match ! bl ← find_symbol … ge i ;
+        find_funct_ptr … ge bl
+return λx.(∃fd.x = ?) → ?
+with
+[ Some fd ⇒ λ_.fd
+| None ⇒ λprf.⊥
+] (pi2 … i).
+cases prf #fd #ABS destruct
+qed.
+
+definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
+  λi : ident.∃fd.
+    ! bl ← find_symbol … ge i ;
+    find_funct_ptr … ge bl = Some ? (Internal ? fd).
+
+lemma description_of_internal_function : ∀F,globals,ge,i,fn.
+  description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i.
+#F #globals #ge * #i * #fd #EQ
+#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
+%{EQ}
+qed.
+
+lemma internal_function_is_function : ∀F,globals,ge,i.
+  is_internal_function F globals ge i → is_function … ge i.
+#F #globals #ge #i * #fn #prf %{prf} qed.
+
+definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) →
+F globals ≝
+λF,globals,ge,i.
+match ! bl ← find_symbol … ge i ;
+        find_funct_ptr … ge bl
+return λx.(∃fn.x = ?) → ?
+with
+[ Some fd ⇒
+  match fd return λx.(∃fn.Some ? x = ?) → ? with
+  [ Internal fn ⇒ λ_.fn
+  | External _ ⇒ λprf.⊥
+  ]
+| None ⇒ λprf.⊥
+] (pi2 … i).
+cases prf #fn #ABS destruct
+qed.
+
 (* Paolo: I'll put in this record the property about genv we need *)
 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
 { ge :> genv_t (fundef (F globals))
 ; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
+; stack_sizes : (Σi.is_internal_function F globals ge i) → ℕ
 }.
 
@@ -102 +154 @@
 axiom BadProgramCounter : String.
 
-definition function_of_block :
- ∀pars : params.
- ∀globals.
-  genv pars globals →
-  block →
-  res (joint_closed_internal_function pars globals) ≝
-  λpars,globals,ge,b.
-  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
-  match def with
-  [ Internal def' ⇒ OK … def'
-  | External _ ⇒ Error … [MSG BadProgramCounter]].
- 
-(* this can replace graph_fetch function and lin_fetch_function *)
-definition fetch_function:
- ∀pars : params.
- ∀globals.
-  genv pars globals →
-  cpointer →
-  res (joint_closed_internal_function pars globals) ≝
- λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
-
+(*
 inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
   | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
@@ -133 +165 @@
   | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
   | FEnd2  : fin_step_flow p F Call. (* end flow *)
+*)
+
+definition funct_of_ident : ∀F,globals,ge.
+  ident → option (Σi.is_function F globals ge i)
+≝ λF,globals,ge,i.
+match ?
+return λx.! bl ← find_symbol … ge i ;
+    find_funct_ptr … ge bl = x → ?
+with
+[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
+| None ⇒ λ_.None ?
+] (refl …).
+
+lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.
+∀Q : option A → Prop.
+∀c1 : ∀a.Q (Some ? a) → B.
+∀c2 : Q (None ?) → B.
+∀P : B → Prop.
+(∀a,prf.P (c1 a prf)) →
+(∀prf.P (c2 prf)) →
+∀prf : Q m.
+P (match m return λx.Q x → ? with
+   [ Some a ⇒ λprf.c1 a prf
+   | None ⇒ λprf.c2 prf
+   ] prf).
+#A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
+normalize [@H1 | @H2]
+qed.
+
+lemma symbol_of_function_block_ok :
+  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
+#F #ge #b #FFP
+whd in ⊢ (???(??%));
+@match_opt_prf_elim [//] #H @⊥
+(* cut and paste from global env *)
+whd in H:(??%?);
+cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
+cases (functions_inv … ge b FFP)
+#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
+lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
+cases (find ????)
+[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
+| * #id' #b' #_ normalize #_ #E destruct
+] qed.
+
+definition funct_of_block : ∀F,globals,ge.
+  block → option  (Σi.is_function F globals ge i) ≝
+λF,globals,ge,bl.
+   match find_funct_ptr … ge bl
+   return λx.find_funct_ptr … ge bl = x → ? with
+   [ Some fd ⇒ λprf.return mk_Sig
+        ident (λi.is_function F globals ge i)
+        (symbol_of_function_block … ge bl ?)
+        (ex_intro … fd ?)
+   | None ⇒ λ_.None ?
+   ] (refl …).
+[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
+| >prf % #ABS destruct(ABS)
+]
+qed.
+
+definition int_funct_of_block : ∀F,globals,ge.
+  block → option (Σi.is_internal_function F globals ge i) ≝
+  λF,globals,ge,bl.
+  ! f ← funct_of_block … ge bl ;
+  match ?
+  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
+  with
+  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
+  | External fn ⇒ λ_.None ?
+  ] (refl …).
+@(description_of_internal_function … prf)
+qed.
+
+definition funct_of_bevals : ∀F,globals,ge.
+  beval → beval → option (Σi.is_function F globals ge i) ≝
+λF,globals,ge,dpl,dph.
+! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
+if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
+   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then
+   funct_of_block … (pblock ptr)
+else None ?.
+
+definition block_of_funct_ident ≝ λF,globals,ge.
+  λi : Σi.is_function F globals ge i.
+  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
+  [ Some bl ⇒ λ_.bl
+  | None ⇒ λprf.⊥
+  ] (pi2 … i).
+cases prf #fd normalize #ABS destruct(ABS)
+qed.
+
+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:
+ ∀pars : params.
+ ∀globals.
+ ∀ge : genv pars globals.
+  cpointer →
+  res (Σi.is_internal_function … ge i) ≝
+ λpars,globals,ge,p.
+ opt_to_res … [MSG BadFunction; MSG BadPointer]
+    (int_funct_of_block … ge (pblock p)).
 
 record sem_unserialized_params
@@ -138 +281 @@
   (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
@@ -161 +305 @@
   ; 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 →
+  ; 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)
@@ -170 +314 @@
   ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
   (* change of pc must be left to *_flow execution *)
-  ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
-      F globals → state st_pars → IO io_out io_in (state st_pars)
-  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
-      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
-  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
-      state st_pars → IO io_out io_in ident
-  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
-  (* do something more in some op2 calculations (e.g. mark a register for correction
-     with spilled_no in ERTL) *)
-  ; post_op2 : ∀globals.genv_gen F globals →
-    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
-    state st_pars → state st_pars
+  ; 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 st_pars)
   }.
 
@@ -220 +356 @@
     return set_regs ? r st.
  
-axiom BadPointer : String.
-
-(* this is preamble to all calls (including tail ones). The optional argument in
-   input tells the function whether it has to save the frame for internal
-   calls.
-   the first element of the triple is the entry point of the function if
-   it is an internal one, or false in case of an external one.
-   The actual update of the pc is left to later, as it depends on
-   serialization and on whether the call is a tail one. *)
-definition eval_call_block:
- ∀p,F.∀p':sem_unserialized_params p F.∀globals.
-  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
-    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
- λp,F,p',globals,ge,st,b,args,dest.
-  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
-    match fd with
-    [ Internal fd ⇒
-      return 〈Init ?? (block_id b) fd args dest, st〉
-    | External fn ⇒
-      ! params ← fetch_external_args … p' fn st : IO ???;
-      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
-      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
-      (* CSC: XXX bug here; I think I should split it into Byte-long
-         components; instead I am making a singleton out of it. To be
-         fixed once we fully implement external functions. *)
-      let vs ≝ [mk_val ? evres] in
-      ! st ← set_result … p' vs dest st : IO ???;
-      return 〈Proceed ???, st〉
-      ].
-
 axiom FailedStore: String.
 
@@ -355 +461 @@
 qed.
 
-axiom ProgramCounterOutOfCode : String.
-axiom PointNotFound : String.
-axiom LabelNotFound : String.
-
 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv p globals → cpointer →
-  res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
+  ∀ge:genv p globals. cpointer →
+  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
   λp,msp,globals,ge,ptr.
+  let bl ≝ pblock ptr in
+  ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer]
+    (int_funct_of_block … ge bl) ;
+  let fn ≝ if_of_function … f in
   let pt ≝ point_of_pointer ? msp ptr in
-  ! fn ← fetch_function … ge ptr ;
   ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
-  return 〈fn, stmt〉.
-  
+  return 〈f, stmt〉.
+
 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
   genv p globals → cpointer → label → res cpointer ≝
   λp,msp,globals,ge,ptr,lbl.
-  ! fn ← fetch_function … ge ptr ;
+  ! 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) ;
@@ -435 +541 @@
  return mk_state_pc … st newpc.
 
-axiom MissingSymbol : String.
-axiom FailedLoad : String.
-axiom BadFunction : String.
-axiom SuccessorNotProvided : String.
-
-definition block_of_call ≝ λp:sem_params.λglobals.
+
+definition function_of_call ≝ λp:sem_params.λglobals.
   λge: genv p globals.λst : state p.λf.
   match f with
   [ inl id ⇒
-    opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge 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) ;
-    ! ptr ← pointer_of_bevals [addr_l ; addr_h] ;
-    if eq_bv … (bv_zero …) (offv (poff … ptr)) then
-      return pblock ptr
-    else Error … [MSG BadFunction]
+    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.
+
+lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.
+  block_region (block_of_funct_ident F globals ge i) = Code.
+#F #globals #ge * #i * #fd
+whd in ⊢ (?→??(?%)?);
+cases (find_symbol ???)
+[ #ABS normalize in ABS; destruct(ABS) ]
+#bl normalize nodelta >m_return_bind
+whd in ⊢ (??%?→?); cases (block_region bl)
+[ #ABS normalize in ABS; destruct(ABS) ]
+#_ %
+qed.
+
+definition eval_internal_call_pc ≝
+λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
+let fn ≝ if_of_function … ge i in
+let l' ≝ joint_if_entry ?? fn in
+let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in
+pointer_of_point ? p … pointer_in_fn 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 ;
+let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
+return set_regs p regs st.
+
 definition eval_seq_no_pc :
- ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals →
-  state p → ∀s:joint_seq p globals.
+ ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
+  state p → cpointer → joint_seq p globals →
   IO io_out io_in (state p) ≝
- λp,globals,ge,curr_fn,st,seq.
+ λp,globals,ge,curr_fn,st,next,seq.
  match seq return λx.IO ??? with
   [ extension_seq c ⇒
@@ -489 +631 @@
     ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
     ! st' ← acca_store … dacc_a v' st;
-    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
+    return set_carry … carry st'
   | CLEAR_CARRY ⇒
     return set_carry … (BBbit false) st
@@ -509 +651 @@
     pair_reg_move … st dst_src
   | CALL f args dest ⇒
-    ! b ← block_of_call … ge st f : IO ???;
-    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
-    return st'
+    ! fn ← function_of_call … ge st f : IO ???;
+    match description_of_function … fn return λx.description_of_function … fn = x → ? with
+    [ Internal fd ⇒ λprf.
+      ! st' ← save_frame … next dest st ;
+      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
+    | External fd ⇒ λ_.eval_external_call … fd args dest st
+    ] (refl …)
   | _ ⇒ return st
   ].
-  @find_symbol_exists
+[ @find_symbol_exists
   lapply prf
   elim globals [*]
   #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
   #G %2 @IH @G
-  qed.
-
-definition eval_seq_pc :
- ∀p:sem_params.∀globals. genv p globals → state p →
-  ∀s:joint_seq p globals.
-  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
-  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
+| @(description_of_internal_function … prf)
+]
+qed.
+
+definition eval_seq_pc : 
+ ∀p:sem_params.∀globals.∀ge:genv p globals.
+  state p → cpointer → joint_seq p globals →
+  res cpointer ≝
+  λp,globals,ge,st,next,s.
+  match s with
   [ CALL f args dest ⇒
-    ! b ← block_of_call … ge st f : IO ???;
-    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
-    return flow
-  | _ ⇒ return Proceed ???
+    ! fn ← function_of_call … ge st f;
+    match ? return λx.description_of_function … fn = x → ? with
+    [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?»
+    | External _ ⇒ λ_.return next
+    ] (refl …)
+  | _ ⇒ return next
   ].
-
-definition eval_step :
- ∀p:sem_params.∀globals. genv p globals →
-  joint_closed_internal_function p globals → state p →
-  ∀s:joint_step p globals.
-  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
-  λp,globals,ge,curr_fn,st,s.
-  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
-  [ step_seq s ⇒
-    ! flow ← eval_seq_pc ?? ge st s ;
-    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
-    return 〈flow,st'〉
-  | COND src ltrue ⇒
-    ! v ← acca_retrieve … st src;
-    ! b ← bool_of_beval v;
-    if b then
-      return 〈Redirect ??? ltrue, st〉
-    else
-      return 〈Proceed ???, st〉
+@(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 ⇒
+    ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;
+    match s return λ_.IO ??? with
+    [ step_seq s ⇒
+      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
+      ! pc' ← eval_seq_pc … ge st next_ptr s ;
+      return mk_state_pc … st' pc'
+    | COND a l ⇒
+      ! v ← acca_retrieve … st a ;
+      ! b ← bool_of_beval … v ;
+      ! pc' ←
+        if b then
+          pointer_of_label ? p … ge (pc … st) l
+        else
+          succ_pc ? p (pc … st) next ;
+      return mk_state_pc … st pc'
+    ]
+  | final s ⇒
+    match s with
+    [ GOTO l ⇒
+      ! pc' ← pointer_of_label ? p ? ge (pc … st) l ;
+      return mk_state_pc … st pc'
+    | RETURN ⇒
+      ! st' ← pop_frame … curr_fn st ;
+      ! 〈pc', st''〉 ← fetch_ra … p st' ;
+      return mk_state_pc … st'' pc'
+    | TAILCALL _ f args ⇒
+      ! fn ← function_of_call … ge st f : IO ???;
+      match ? return λx.description_of_function … fn = x → ? with
+      [ Internal _ ⇒ λprf.
+        ! pc' ← eval_internal_call_pc … ge «fn, ?» ;
+        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 ;
+        ! st'' ← pop_frame … curr_fn st ;
+        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
+        return mk_state_pc … st''' pc'
+      ] (refl …)
+    ]
   ].
-  %1 % qed.
-
-definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
-  (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
-  IO io_out io_in (state p) ≝
- λp,globals,ge,curr_fn,st,s.
-  match s return λx.IO ??? with
-    [ tailcall c ⇒
-      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
-      return st'
-    | _ ⇒ return st
-    ].
-
-definition eval_fin_step_pc :
- ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
-  ∀s:joint_fin_step p.
-  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
-  λp,g,ge,curr_fn,st,s.
-  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
-  [ tailcall c ⇒
-    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
-    return flow  
-  | GOTO l ⇒ return FRedirect … l
-  | RETURN ⇒ return FEnd1 ??
-  ]. %1 % qed.
-
-definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
-  state p → Z → joint_closed_internal_function p globals → call_args p →
-  res (state_pc p) ≝
-  λp,globals,ge,st,id,fn,args.
-    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
-              args st ;
-    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
-    let l' ≝ joint_if_entry … fn in
-    let st' ≝ set_regs p regs st in
-    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
-    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
-    return mk_state_pc ? st' pc. % qed.
-
-(* The pointer provided is the one to the *next* instruction. *)
-definition eval_step_flow :
- ∀p:sem_params.∀globals.∀flows.genv p globals →
- state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
- λp,globals,flows,ge,st,nxt,cmd.
- match cmd with
-  [ Redirect _ l ⇒
-    goto … ge l st nxt
-  | Init id fn args dest ⇒
-    ! st' ← save_frame … nxt dest st ;
-    do_call ?? ge st' id fn args
-  | Proceed _ ⇒
-    return mk_state_pc ? st nxt
-  ].
-
-definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
-  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
-  λp,globals,lbls,ge,st,curr,cmd.
-  match cmd with
-  [ FRedirect _ l ⇒ goto … ge l st curr
-  | FTailInit id fn args ⇒
-    do_call … ge st id fn args
-  | _ ⇒
-    ! 〈ra, st'〉 ← fetch_ra … st ;
-    ! fn ← fetch_function … ge curr ;
-    ! st'' ← pop_frame … ge fn st';
-    return mk_state_pc ? st'' ra
-  ].
-
-definition eval_statement :
- ∀globals.∀p:sem_params.genv p globals →
-  state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
-    IO io_out io_in (state_pc p) ≝
- λglobals,p,ge,st,curr_fn,stmt.
- match stmt with
- [ sequential s nxt ⇒
-   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
-   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
-   eval_step_flow … ge st' nxtptr flow
- | final s ⇒
-   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
-   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
-   eval_fin_step_flow … ge st' (pc … st) flow
- ].
+@(description_of_internal_function … prf)
+qed.
 
 definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
@@ -640 +741 @@
   λglobals,p,ge,st.
   ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
-  eval_statement … ge st fn s.
+  eval_statement … ge fn st s.
 
 (* Paolo: what if in an intermediate language main finishes with an external
@@ -648 +749 @@
   genv p globals → cpointer → state_pc p → option int ≝
  λglobals,p,ge,exit,st.res_to_opt ? (
-  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
+  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
+  let fn ≝ if_of_function … f in
   match s with
   [ final s' ⇒