Changeset 2529 for src/joint

Timestamp:

Dec 4, 2012, 6:16:25 PM (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/joint

Files:

• Traces.ma (modified) (12 diffs)
• linearise.ma (modified) (8 diffs)
• lineariseProof.ma (modified) (35 diffs)
• semantics.ma (modified) (16 diffs)
• semanticsUtils.ma (modified) (3 diffs)
• semantics_blocks.ma (modified) (2 diffs)

src/joint/Traces.ma

@@ -15 +15 @@
  { prog_spars : sem_params
  ; prog : joint_program prog_spars
- ; stack_sizes : (Σi.is_internal_function_of_program … prog i) → ℕ
+ ; stack_sizes : ident → option ℕ
 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
  }.
@@ -78 +78 @@
   let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
   let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
-  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
+  let spp : xpointer ≝
+    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
+     pi2 … spb» in
 (*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
   let main ≝ prog_main … p in
@@ -86 +88 @@
   ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
   let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
-  ! 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 ;
-    let pc' ≝ eval_internal_call_pc … ge main in
+  ! bl ← block_of_call … ge st_pc0 (inl … main) ;
+  ! 〈i, fn〉 ← fetch_function … ge bl ;
+  match fn with
+  [ Internal ifn ⇒
+    ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ;
+    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
     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.
+  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
+  ].
 
 definition joint_classify_seq :
@@ -105 +103 @@
   match stmt with
   [ CALL f args dest ⇒
-    match function_of_call ?? (ev_genv p) st f with
-    [ OK fn ⇒
-      match description_of_function … fn with
+    match (! bl ← block_of_call … (ev_genv p) st f ;
+            fetch_function … (ev_genv p) bl) with
+    [ OK id_fn ⇒
+      match \snd id_fn with
       [ Internal _ ⇒ cl_call
       | External _ ⇒ cl_other
@@ -136 +135 @@
   ∀p : evaluation_params.state_pc p → status_class ≝
   λp,st.
-  match fetch_statement ? p … (ev_genv p) (pc … st) with
-  [ OK f_s ⇒
-    match \snd f_s with
+  match fetch_statement … (ev_genv p) (pc … st) with
+  [ OK i_f_s ⇒
+    match \snd i_f_s with
     [ sequential s _ ⇒ joint_classify_step p st s
     | final s ⇒ joint_classify_final p s
@@ -145 +144 @@
   ].
 
+definition no_call : ∀p,g.joint_seq p g → Prop ≝
+  λp,g,s.match s with
+  [ CALL _ _ _ ⇒ False
+  | _ ⇒ True
+  ].
+
+definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
+  λp,g,s.match s with
+  [ COST_LABEL _ ⇒ False
+  | _ ⇒ True
+  ].
+
+lemma no_call_advance : ∀p : evaluation_params.
+∀s,nxt.∀st : state_pc p.
+no_call p (globals p) s →
+eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
+#p * // #f #args #dest #nxt #st *
+qed.
+
+lemma no_call_other : ∀p : evaluation_params.∀st,s.
+no_call p (globals p) s →
+joint_classify_seq … st s = cl_other.
+#p #st * // #f #args #dest *
+qed.
+
+lemma cond_call_other :
+  ∀p,globals.∀P : joint_step p globals → Prop.
+  (∀a,lbltrue.P (COND … a lbltrue)) →
+  (∀f,args,dest.P (CALL … f args dest)) →
+  (∀s.no_call ?? s → P s) →
+  ∀s.P s.
+#p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
+
 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.
+  ∃i_f,f',args,dest,next,bl,i',fd'.
+  fetch_statement … (ev_genv p) (pc … st) =
+    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
+  block_of_call … (ev_genv p) st f' = OK ? bl ∧
+  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
 #p #st
 whd in match joint_classify; normalize nodelta
-inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
-[ * #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
-      [ whd in match joint_classify_step; whd in match joint_classify_seq;
-        normalize nodelta
-        inversion (function_of_call ?????) normalize nodelta
-        [ #fn
-          inversion (description_of_function ?? fn) #fd
-          #EQfd
-        | #e
-        ] #EQfn
-      ]
+inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
+[2: #e #_ #ABS destruct(ABS) ]
+* #i_f * [2: * [ #lbl | | #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
+@cond_call_other
+[ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
+|3: #s #no_call #nxt #_ whd in match joint_classify_step;
+  normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS)
+]
+#f' #args #dest #nxt #fetch
+whd in match joint_classify_step; whd in match joint_classify_seq;
+normalize nodelta
+inversion (block_of_call ?????)
+[ #bl #block_of_c  >m_return_bind
+  inversion (fetch_function ???)
+  [ * #i' *
+    [ #fd' #fetch' #_
+      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
+      % [ %{block_of_c} % ]
+      whd in match fetch_internal_function; normalize nodelta
+      >fetch' %
     ]
   ]
-| #e
-] #EQfetch
-[|*: #ABS normalize in ABS; destruct(ABS) ]
-normalize nodelta #_
-%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
-%{EQfd} %{EQfn} % 
+]
+#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
 qed.
 
@@ -183 +215 @@
   (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
 λp,s1,s2.
-match fetch_statement ? p … (ev_genv p) (pc … s1) with
+match fetch_statement … (ev_genv p) (pc … s1) with
 [ OK x ⇒
   match \snd x with
   [ sequential s next ⇒
-    pc … s2 = succ_pc p p (pc … s1) next
+    pc … s2 = succ_pc p (pc … s1) next
   | _ ⇒ False (* never happens *)
   ]
@@ -225 +257 @@
    I think handling of the function is easier *)
 λp,st.
-let dummy : ident ≝ an_identifier ? one in
-match fetch_statement ? p … (ev_genv p) (pc … st) with
+let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
+match fetch_statement … (ev_genv p) (pc … st) with
 [ OK x ⇒
   match \snd x with
@@ -234 +266 @@
       match s with
       [ CALL f' args dest ⇒
-        match function_of_call … (ev_genv p) st f' with
-        [ OK f ⇒ f
+        match
+          (! bl ← block_of_call … (ev_genv p) st f' ;
+           fetch_internal_function … (ev_genv p) bl) with
+        [ OK i_f ⇒ \fst i_f
         | _ ⇒ dummy
         ]
@@ -279 +313 @@
   | _ ⇒ None ?
   ].
+
+
+lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
+no_cost_label p (globals p) s →
+cost_label_of_stmt … (sequential … s nxt) = None ?.
+#p * // #lbl #next *
+qed.
 
 definition joint_abstract_status :
@@ -293 +334 @@
    (* as_label_of_pc ≝ *)
     (λpc.
-      match fetch_statement ? p … (ev_genv p) pc with
+      match fetch_statement … (ev_genv p) pc with
       [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
       | _ ⇒ None ?
@@ -300 +341 @@
    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    (* as_call_ident ≝ *) (joint_call_ident p).
+

src/joint/linearise.ma

@@ -173 +173 @@
     ] n_prf
   ] (chop_ok ? (λx.x∈visited) visiting).
-(*cases daemon qed. *)
+(* cases daemon qed. *)
 whd
 [ (* base case, visiting is all visited *)
@@ -555 +555 @@
 qed.
 
-
 definition good_local_sigma :
   ∀p:unserialized_params.
@@ -565 +564 @@
   λp,globals,g,entry,c,sigma.
     sigma entry = Some ? 0 ∧
+    (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧
     ∀l,n.sigma l = Some ? n →
-      ∃s. lookup … g l = Some ? s ∧
-        opt_Exists ?
-          (λls.let 〈lopt, ts〉 ≝ ls in
-            opt_All ? (eq ? l) lopt ∧
-            ts = graph_to_lin_statement … s ∧
-            opt_All ?
-              (λnext.Or (sigma next = Some ? (S n))
-              (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
-              (stmt_implicit_label … s)) (nth_opt … n c). 
+      ∃s. stmt_at … g l = Some ? s ∧
+        All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
+        opt_All ?
+            (λnext.Or (sigma next = Some ? (S n))
+            (stmt_at … c (S n) = Some ? (GOTO … next)))
+            (stmt_implicit_label … s) ∧ 
+        stmt_at … c n = Some ? (graph_to_lin_statement … s).
 
 definition linearise_code:
@@ -624 +622 @@
 #entry_O #req_vis #last_fin #labels_in_req #sigma_prop
 %
-[ % [assumption]
-  #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
-  #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
-  % [2: % [ assumption ] |]
-  >nth_opt_filter_labels in ⊢ (???%);
-  >nth_opt_is_stmt >m_return_bind whd >m_return_bind
-  % [ % ]
-  [ elim (lbl ∈ required) %
-  | %
-  | lapply succ_is_in
-    lapply (refl … (stmt_implicit_label … stmt))
-    cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
-    #next #EQ_next *
-    [ #H %1{H} ]
-    #H %2
-    >nth_opt_filter_labels >H %
+[ % [ % [assumption]]
+  #lbl #n
+  [ change with (If ? then with prf do ? else ? = ? → ?)
+    @If_elim [2: #_ #ABS destruct(ABS) ]
+    #H lapply H
+    >occurs_exactly_once_filter_labels
+    elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?))
+    [1,2: #H1 >H1 |*:] [2: * ]
+    elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 *
+    lapply (in_map_domain … visited lbl) >(req_vis … H2)
+    * #n_lbl #EQsigma
+    elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_
+    >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H)
+    [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
+    | >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
+      >H2 %
+    ]
+  | #eq_lookup elim (sigma_prop ?? eq_lookup)
+    #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 
+    % [2: % [ % [ % [ assumption ]]] |]
+    [ @All_append
+      [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ]
+        #nxt #nxt_spec % [2: %] cases nxt_spec -nxt_spec
+        [ #EQ >EQ % #ABS destruct(ABS)
+        | #goto_in lapply (in_map_domain … visited nxt)
+          >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ]
+          @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
+          whd in ⊢ (??%?); >goto_in %
+        ]
+      | <graph_to_lin_labels @(All_mp … (labels_in_req …))
+        [ #lbl #H
+          lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS)
+        | whd in ⊢ (??%?); >nth_opt_is_stmt % |
+        ]
+      ]
+    | lapply succ_is_in
+      cases (stmt_implicit_label … stmt) [#_ %]
+      #next *
+      [ #H %1{H} ]
+      #H %2
+      >stmt_at_filter_labels whd in ⊢ (??%?); >H %
+    | >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt %
+    ]
   ]
 | #i #s
@@ -711 +736 @@
 [ @H2
 | @H1
-| cases H1 #H3 #H4 elim (H4 … H3)
-  #s * #_ >lin_code_has_point cases code
-  [ * | #hd #tl #_ % ]
+| cases H1 * #H3 #H4 #H5 elim (H5 … H3)
+  #s *** #_ #_ #_ >lin_code_has_point cases code
+  [ #ABS normalize in ABS; destruct(ABS) | #hd #tl #_ % ]
 ]
 qed.
@@ -724 +749 @@
     (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
 
-
+(*
 definition good_sigma :
   ∀p:unserialized_params.
@@ -742 +767 @@
 #p #prog
 letin sigma ≝ 
-  (λi : Σi.is_internal_function_of_program … prog i.
-    let fn_in ≝ if_of_function … i in
+  (λi : Σi.is_internal_function_of_program … prog i.    let fn_in ≝ if_of_function … i in
     \snd (linearise_int_fun … fn_in))
 %{sigma}
@@ -751 +775 @@
 normalize nodelta #prf @prf
 qed.
+*)

src/joint/lineariseProof.ma

@@ -26 +26 @@
   (∀F.sem_unserialized_params p F) →
     ∀prog : joint_program (mk_graph_params p).
-  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
+  (ident → option ℕ) → 
      abstract_status
  ≝
@@ -40 +40 @@
   (∀F.sem_unserialized_params p F) →
     ∀prog : joint_program (mk_lin_params p).
-  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
+  (ident → option ℕ) → 
      abstract_status
  ≝
@@ -97 +97 @@
 *)
 
+definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
+  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → 
+    label → option ℕ.
+    
 definition sigma_pc_opt:
- ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
-  ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ) →
+ ∀p,p'.∀graph_prog.
+  sigma_map p graph_prog →
    program_counter → option program_counter
  ≝
@@ -106 +109 @@
   let pars ≝ make_sem_graph_params p p' in
   let ge ≝ globalenv_noinit … prog in
-  ! f ← int_funct_of_block ? ge (pc_block pc) ;
-  ! lin_point ← sigma f (point_of_pc ? pars pc) ;
-  return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
+  ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
+  ! lin_point ← sigma fd (point_of_pc pars pc) ;
+  return pc_of_point 
+  (make_sem_lin_params ? p') (pc_block pc) lin_point.
 
 definition well_formed_pc:
  ∀p,p',graph_prog.
-  ((Σi.is_internal_function_of_program … graph_prog i) → 
-    label → option ℕ) →
+  sigma_map p graph_prog →
    program_counter → Prop
  ≝
@@ -122 +125 @@
 definition sigma_beval_opt :
  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
-  ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ) →
+  sigma_map p graph_prog →
   beval → option beval ≝
 λp,p',graph_prog,sigma,bv.
@@ -138 +140 @@
 definition sigma_is_opt :
  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
-  ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ) →
+  sigma_map p graph_prog →
   internal_stack → option internal_stack ≝
 λp,p',graph_prog,sigma,is.
@@ -167 +168 @@
 definition well_formed_mem :
  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
-  ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ) →
+  sigma_map p graph_prog →
  bemem → Prop ≝
 λp,p',graph_prog,sigma,m.
@@ -311 +311 @@
   (p : unserialized_params)
   (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
- (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
-    graph_prog i) → 
-      label → option ℕ) : Type[0] ≝
+  (sigma : sigma_map p graph_prog) : Type[0] ≝
 { well_formed_frames : framesT (make_sem_graph_params p p') → Prop
 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
@@ -340 +338 @@
 definition well_formed_state : 
  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
- ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ).
+ ∀sigma.
  good_sem_state_sigma p p' graph_prog sigma →
  state (make_sem_graph_params p p') → Prop ≝
@@ -352 +349 @@
 definition sigma_state : 
  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
- ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
-    code_point (mk_graph_params p) → option ℕ).
+ ∀sigma.
  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
  ∀st : state (make_sem_graph_params p p').
@@ -409 +405 @@
 definition sigma_pc :
 ∀p,p',graph_prog.
-∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
-    label → option ℕ).
+∀sigma.
 ∀pc.
 ∀prf : well_formed_pc p p' graph_prog sigma pc.
@@ -447 +442 @@
  let st' ≝ sigma_state … (proj2 … prf) in
  mk_state_pc ? st' pc'.
-
+(*
 definition sigma_function_name :
  ∀p,graph_prog.
@@ -454 +449 @@
   (Σf.is_internal_function_of_program … lin_prog f) ≝
 λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
-
+*)
 lemma m_list_map_All_ok :
   ∀M : MonadProps.∀X,Y,f,l.
@@ -520 +515 @@
   (p : unserialized_params)
   (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
- (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
-    graph_prog i) → 
-      label → option ℕ)
+  (sigma : sigma_map p graph_prog)
 : Type[0] ≝
 { gsss :> good_sem_state_sigma p p' graph_prog sigma 
@@ -557 +550 @@
 ; eval_ext_seq_commute :
   let lin_prog ≝ linearise p graph_prog in
-  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
-  let stack_sizes' ≝
-   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-     ? graph_prog stack_sizes in
-  ∀ext,fn,st1,st2,prf1.
-  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
-    ext fn st1 = return st2 →
+  ∀stack_sizes.
+  ∀ext,i,fn,st1,st2,prf1.
+  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
+    ext i fn st1 = return st2 →
   ∃prf2.
   eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
-    ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
+    ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    return sigma_state p p' graph_prog sigma gsss st2 prf2
 ; setup_call_commute :
@@ -586 +576 @@
 ; read_result_commute :
   let lin_prog ≝ linearise p graph_prog in
-  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
-  let stack_sizes' ≝
-   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-     ? graph_prog stack_sizes in
+  ∀stack_sizes.
   ∀call_dest , st1 , prf1, l1.
-  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
+  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     call_dest st1 = return l1 →
   ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
@@ -598 +585 @@
 ; pop_frame_commute :
   let lin_prog ≝ linearise p graph_prog in
-  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
-  let stack_sizes' ≝
-   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-     ? graph_prog stack_sizes in
-  ∀ st1 , prf1, curr_id ,st2.
-  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 
-            curr_id st1 = return st2 →
+  ∀stack_sizes.
+  ∀ st1 , prf1, curr_id , curr_fn ,st2.
+  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 
+            curr_id curr_fn st1 = return st2 →
  ∃prf2.
  let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
  let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
   pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
-            (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
+            curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
             return mk_state_pc ? st2' pc' 
 }.
@@ -672 +656 @@
 λgss : good_state_sigma p p' graph_prog sigma.
 store_commute … gss (acca_store__commute … gss).
-  
-    
-lemma acca_store_commute :
-  ∀p,p',graph_prog,sigma.
-  ∀gss : good_state_sigma p p' graph_prog sigma.
-  ∀a,bv,st,st',prf1,prf1'.
-  acca_store ?? (p' ?) a bv st = return st' → 
-  ∃prf2.
-  acca_store ?? (p' ?) a
-    (sigma_beval p p' graph_prog sigma bv prf1')
-    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
-λp,p',graph_prog,sigma,gss,a,bv.?.
-* #frms #is #carry #regs #m
-* #frms' #is' #carry' #regs' #m'
-*** #frms_ok #is_ok #regs_ok #mem_ok
-#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
-#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
-elim (acca_store__commute … gss … EQ1)
-[ #prf2 #EQ2
-  % [ whd /4 by conj/ ]
-  change with (! r ← ? ; ? = ?) >EQ2
-  whd in match (sigma_state ???????); normalize nodelta
-   >m_return_bind
-
-
-st,st',prf1,prf2,prf3.?.
-
-
-#p #p' #
+
 *)
 
@@ -729 +685 @@
 #A * #x #v normalize #EQ destruct % qed.
 
+(*
 lemma if_of_function_commute:
  ∀p.
@@ -739 +696 @@
  #p #graph_prog #graph_fun whd
  @prog_if_of_function_transform % qed.
-
-lemma bind_opt_inversion:
-  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
-  (! x ← f ; g x = Some … y) →
-  ∃x. (f = Some … x) ∧ (g x = Some … y).
-#A #B #f #g #y cases f normalize 
-[ #H destruct (H)
-| #a #e %{a} /2 by conj/
-] qed.
+*)
+lemma bind_option_inversion_star:
+  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
+  (∀x.f = Some … x → g x = Some … y → P) →
+  (! x ← f ; g x = Some … y) → P.
+#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
+
+interpretation "option bind inversion" 'bind_inversion =
+  (bind_option_inversion_star ???????).
 
 lemma sigma_pblock_eq_lemma : 
@@ -758 +715 @@
  #p #p' #graph_prog #sigma #pc #prf
  whd in match sigma_pc; normalize nodelta
- @opt_safe_elim #x #x_spec
- whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
- normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
- #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
+ @opt_safe_elim #x @'bind_inversion * #i #fn #_
+ @'bind_inversion #n #_ whd in ⊢ (??%?→?);
+ #EQ destruct %
 qed.
 
@@ -780 +736 @@
 *)
 
+(*
 lemma funct_of_block_transf :
 ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
@@ -887 +844 @@
 #A #B #progr #transf #bl #f #prf
 whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta 
-#H
-elim (bind_opt_inversion ??? ?? H) -H #x
-* #x_spec
+@'bind_inversion #x #x_spec
 @match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
 #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
@@ -899 +854 @@
 >(description_of_function_transf) [2: @x_prf ]
 >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
-
-
-lemma fetch_function_sigma_commute :
- ∀p,p',graph_prog.
- let lin_prog ≝ linearise p graph_prog in
- ∀sigma,pc_st,f.
-  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
- fetch_function … (globalenv_noinit … graph_prog) pc_st = 
-  return f
-→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
-  return sigma_function_name … f.
- #p #p' #graph_prog #sigma #st #f #prf
+*)
+
+axiom symbol_for_block_transf :
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ ∀bl, i.
+ symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
+ symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
+
+lemma fetch_function_transf :
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ ∀bl,i,f.
+ fetch_function … (globalenv … init prog_in) bl = 
+  return 〈i, f〉
+→ fetch_function … (globalenv … init prog_out) bl =
+  return 〈i, trans … f〉.
+#A #B #V #init #prog_in #trans #bl #i #f
  whd in match fetch_function; normalize nodelta
- >(sigma_pblock_eq_lemma … prf) #H
- lapply (opt_eq_from_res ???? H) -H #H
- >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
- //
+ #H lapply (opt_eq_from_res ???? H) -H
+ @'bind_inversion #id #eq_symbol_for_block
+ @'bind_inversion #fd #eq_find_funct
+ whd in ⊢ (??%?→?); #EQ destruct(EQ)
+ >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
+ >(find_funct_ptr_transf A B …  eq_find_funct) >m_return_bind %
+qed.
+
+lemma bind_inversion_star : ∀X,Y.∀P : Prop.
+∀m : res X.∀f : X → res Y.∀v : Y.
+(∀x. m = return x → f x = return v → P) →
+! x ← m ; f x = return v → P.
+#X #Y #P #m #f #v #H #G
+elim (bind_inversion ????? G) #x * @H qed.
+
+interpretation "res bind inversion" 'bind_inversion =
+  (bind_inversion_star ???????).
+
+lemma fetch_internal_function_transf :
+ ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
+ ∀bl,i,f.
+ fetch_internal_function … (globalenv_noinit … prog_in) bl = 
+  return 〈i, f〉
+→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
+  return 〈i, trans … f〉.
+#A #B #prog #trans #bl #i #f
+ whd in match fetch_internal_function; normalize nodelta
+ @'bind_inversion * #id * #fd normalize nodelta #EQfetch
+ whd in ⊢ (??%%→?); #EQ destruct(EQ)
+ >(fetch_function_transf … EQfetch) %
 qed.
  
@@ -978 +969 @@
 qed. *)
 
-lemma opt_Exists_elim:
- ∀A:Type[0].∀P:A → Prop.
-  ∀o:option A.
-   opt_Exists A P o →
-    ∃v:A. o = Some … v ∧ P v.
- #A #P * normalize /3/ *
-qed.
-
-
 lemma stmt_at_sigma_commute:
- ∀p,graph_prog,graph_fun,lbl,pt.
- let lin_prog ≝ linearise ? graph_prog in
- let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
- ∀sigma.good_sigma p graph_prog sigma →
- sigma graph_fun lbl = return pt →
+ ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
+ good_local_sigma p globals graph_code entry lin_code sigma →
+ sigma lbl = return pt →
  ∀stmt.
-   stmt_at …
-    (joint_if_code ?? (if_of_function ?? graph_fun))  
+   stmt_at … graph_code
     lbl = return stmt →
-   stmt_at ??
-    (joint_if_code ?? (if_of_function ?? lin_fun))
-    pt = return (graph_to_lin_statement … stmt).  
- #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
-cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
-#sigma_entry_is_zero #lin_stmt_spec
-lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
-#EQlookup_stmt1 #H
-elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt 
-* #EQnth_opt_graph_stmt normalize nodelta
-* #optEQlbl_optlbl_graph_stmt #next_spec
-whd in match (stmt_at ????) in ⊢ (% → ?);
-normalize nodelta
->EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
-whd in match (stmt_at ????); > EQnth_opt_graph_stmt 
-normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
-qed.
+ stmt_at ?? lin_code
+  pt = return graph_to_lin_statement … stmt ∧
+  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
+ match stmt with
+ [ final stmt ⇒ True
+ | sequential stmt nxt ⇒
+   (sigma nxt = Some ? (S pt) ∨
+    (stmt_at ?? lin_code
+     (S pt) = return final (mk_lin_params p) … (GOTO … nxt)))
+ ].  
+ #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
+ * #_ #lin_stmt_spec #prf
+elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at
+#All_succs_in #next_spec
+#EQstmt_at_graph_stmt
+#stmt >EQstmt_at
+whd in ⊢ (??%%→?); #EQ destruct(EQ)
+% [ % assumption ]
+cases stmt in next_spec; -stmt normalize nodelta [2: // ]
+#stmt #nxt
+whd in match opt_All;
+whd in match stmt_implicit_label;
+normalize nodelta //
+qed.
+  
 (*
 
@@ -1036 +1023 @@
  <sigma_pc_commute >lin_lookup_ok // *)
 
-lemma fetch_statement_sigma_commute:
-  ∀p,p',graph_prog,pc,fn,stmt.
+definition good_sigma :
+  ∀p.∀graph_prog : joint_program (mk_graph_params p).
+  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
+    label → option ℕ) → Prop ≝
+  λp,graph_prog,sigma.
+  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
+  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
+    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).
+
+lemma pc_of_label_sigma_commute :
+  ∀p,p',graph_prog,pc,lbl,i,fn.
   let lin_prog ≝ linearise ? graph_prog in
   ∀sigma.good_sigma p graph_prog sigma →
   ∀prf : well_formed_pc p p' graph_prog sigma pc.
-  fetch_statement ? (make_sem_graph_params p p') …
-    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
-  fetch_statement ? (make_sem_lin_params p p') …
+  fetch_internal_function …
+    (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 →
+  let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in
+  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
+  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
+    (pc_block (sigma_pc … pc prf)) lbl =
+        return sigma_pc p p' graph_prog sigma pc' prf'.
+#p #p' #graph_prog #pc #lbl #i #fn
+#sigma #good cases (good fn) -good * #_ #all_labels_in
+#good #prf #fetchfn >lin_code_has_label #lbl_in
+whd in match pc_of_label; normalize nodelta
+>sigma_pblock_eq_lemma
+> (fetch_internal_function_transf … fetchfn) >m_return_bind
+inversion (point_of_label ????)
+[ (*
+  change with (If ? then with prf do ? else ? = ? → ?)
+  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
+  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
+| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
+  %
+  [ @hide_prf whd %
+  | whd in match sigma_pc; normalize nodelta
+    @opt_safe_elim #pc'
+  ]
+  whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
+  >point_of_pc_of_point
+  >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) %
+]
+qed.
+
+lemma graph_pc_of_label :
+  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
+  ∀globals,ge,bl,i_fn,lbl.
+  fetch_internal_function ? ge bl = return i_fn →
+  pc_of_label pars globals ge bl lbl =
+    OK ? (pc_of_point pars bl lbl).
+#p #p' #globals #ge #bl #fn #lbl #fetchfn
+whd in match pc_of_label; normalize nodelta
+>fetchfn %
+qed.
+
+lemma graph_succ_pc :
+  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
+  ∀pc,lbl.
+  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
+normalize //
+qed.
+
+lemma fetch_statement_sigma_commute:
+  ∀p,p',graph_prog,pc,f,fn,stmt.
+  let lin_prog ≝ linearise ? graph_prog in
+  ∀sigma.good_sigma p graph_prog sigma →
+  ∀prf : well_formed_pc p p' graph_prog sigma pc.
+  fetch_statement (make_sem_graph_params p p') …
+    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
+  fetch_statement (make_sem_lin_params p p') …
     (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
-    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
- #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf 
- whd in match fetch_statement; normalize nodelta #H
- cases (bind_inversion ????? H) #id * -H #fetchfn
- >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
- #H cases (bind_inversion ????? H) #fstmt * -H #H
- lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
- >(stmt_at_sigma_commute … good … H) [%]
- whd in match sigma_pc; normalize nodelta
- @opt_safe_elim #pc' #H
- cases (bind_opt_inversion ????? H)
- #i * #EQ1 -H #H
- cases (bind_opt_inversion ????? H)
- #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
- whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
- lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
-qed.
+  return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧
+  All ? (λlbl.well_formed_pc p p' graph_prog sigma
+      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
+    (stmt_explicit_labels … stmt) ∧
+  match stmt with
+  [ sequential stmt nxt ⇒
+    ∃prf'.
+    let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
+    let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
+    (nxt_pc = sigma_nxt ∨
+     fetch_statement (make_sem_lin_params p p') …
+      (globalenv_noinit … lin_prog) nxt_pc =
+      return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
+  | final stmt ⇒ True
+  ].
+#p #p' #graph_prog #pc #f #fn #stmt #sigma #good
+elim (good fn) * #_ #all_labels_in #good_local #wfprf
+#H
+elim (fetch_statement_inv … H)
+#fetchfn #graph_stmt
+whd in match fetch_statement; normalize nodelta
+>sigma_pblock_eq_lemma
+>(fetch_internal_function_transf … fetchfn) >m_return_bind
+whd in match sigma_pc; normalize nodelta @opt_safe_elim
+#lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta
+>fetchfn in ⊢ (%→?); >m_return_bind
+inversion (sigma ??)
+[ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
+#lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
+cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) *
+#H1 #H2 #H3 % [ % ]
+[ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
+  >H1 %
+| @(All_mp … (All_append_r … H2)) #lbl #prf'
+ whd whd in match sigma_pc_opt; normalize nodelta
+ >fetchfn >m_return_bind >point_of_pc_of_point
+ >(opt_to_opt_safe … prf') % normalize
+ #ABS destruct(ABS)
+| cases stmt in H2 H3; normalize nodelta [2: // ]
+  -stmt #stmt #nxt * #next_in #_ #nxt_spec
+  %  
+  [ @hide_prf whd %
+  | @opt_safe_elim #pc'
+  ]
+  >graph_succ_pc whd in ⊢ (??%?→?);
+  >fetchfn normalize nodelta >point_of_pc_of_point
+  >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ)
+  cases nxt_spec
+  [ #EQsigma_nxt %1
+    whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta
+    >point_of_offset_of_point lapply next_in >EQsigma_nxt #N %
+  | #EQstmt_at_nxt %2
+    whd in match (succ_pc ???);
+    >(fetch_internal_function_transf … fetchfn) >m_return_bind
+    whd in match point_of_pc;
+    normalize nodelta >point_of_offset_of_point >point_of_offset_of_point
+    whd in match (point_of_succ ???);
+    >EQstmt_at_nxt %
+  ]
+]
+qed.  
 
 lemma point_of_pc_sigma_commute :
  ∀p,p',graph_prog.
  let lin_prog ≝ linearise p graph_prog in
- ∀sigma,pc,fn,n.
+ ∀sigma,pc,f,fn,n.
   ∀prf : well_formed_pc p p' graph_prog sigma pc.
- int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn →
- sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
- point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
-#p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
+ fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
+ sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
+ point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
+#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
 whd in match sigma_pc; normalize nodelta
 @opt_safe_elim #pc' whd in match sigma_pc_opt;
 normalize nodelta >EQfetch >m_return_bind >EQsigma
->m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
-change with (point_of_offset ??? = ?) @point_of_offset_of_point
+whd in ⊢ (??%?→?); #EQ destruct(EQ)
+@point_of_offset_of_point
 qed.
 
@@ -1082 +1175 @@
  ∀p,p',graph_prog.
  let lin_prog ≝ linearise p graph_prog in
- ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
- let stack_sizes' ≝
-  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-    ? graph_prog stack_sizes in
+ ∀stack_sizes.
  ∀sigma,gss.
  good_sigma p graph_prog sigma →
    status_rel
-    (graph_abstract_status p p' graph_prog stack_sizes')
+    (graph_abstract_status p p' graph_prog stack_sizes)
     (lin_abstract_status p p' lin_prog stack_sizes)
  ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
@@ -1114 +1204 @@
 
 lemma IO_bind_inversion:
-  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
-  (! x ← f ; g x = return y) →
-  ∃x. (f = return x) ∧ (g x = return y).
-#O #I #A #B #f #g #y cases f normalize 
-[ #o #f #H destruct
-| #a #e %{a} /2 by conj/
-| #m #H destruct (H)
+  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
+  (∀x.f = return x → g x = return y → P) →
+  (! x ← f ; g x = return y) → P.
+#O #I #A #B #P #f #g #y cases f normalize 
+[ #o #f #_ #H destruct
+| #a #G #H @(G ? (refl …) H)
+| #e #_ #H destruct
 ] qed.
+
+interpretation "IO bind inversion" 'bind_inversion =
+  (IO_bind_inversion ?????????).
 
 lemma err_eq_from_io : ∀O,I,X,m,v.
@@ -1144 +1237 @@
 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
 #EQ >EQ //
+qed.
+
+(* this should make things easier for ops using memory (where pc cant happen) *)
+definition bv_no_pc : beval → Prop ≝
+λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
+
+lemma bv_pc_other :
+  ∀P : beval → Prop.
+  (∀pc,p.P (BVpc pc p)) →
+  (∀bv.bv_no_pc bv → P bv) →
+  ∀bv.P bv.
+#P #H1 #H2 * /2/ qed.
+
+lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
+  bv_no_pc bv →
+  sigma_beval p p' graph_prog sigma bv prf = bv.
+#p #p' #graph_prog #sigma *
+[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
+#prf * whd in match sigma_beval; normalize nodelta
+@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
 qed.
 
@@ -1254 +1367 @@
  ∀p,p',graph_prog.
  let lin_prog ≝ linearise p graph_prog in
- ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
- let stack_sizes' ≝
-  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-    ? graph_prog stack_sizes in
- ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
- ∀fn,st,stmt,st'.
+ ∀stack_sizes.
+ ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
+ ∀f,fn,st,stmt,st'.
  ∀prf : well_formed_state … gss st.
-  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
-   fn st stmt = return st' →
+  eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
+   f fn stmt st = return st' →
   ∃prf'.
-  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
-    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
+  eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
+    f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
   return sigma_state … gss st' prf'.
   #p #p' #graph_prog #stack_sizes #sigma #gss
@@ -1393 +1503 @@
           inversion(sigma_beval_opt ???? y) 
           [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
+         xxxxxxxxxxxxxxxxxx
+        
+ qed.       
+
+lemma eval_statement_no_pc_sigma_commute :
+ ∀p,p',graph_prog.
+ let lin_prog ≝ linearise p graph_prog in
+ ∀stack_sizes.
+ ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
+ ∀f,fn,st,stmt,st'.
+ ∀prf : well_formed_state … gss st.
+  eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
+   f fn stmt st = return st' →
+  ∃prf'.
+  eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
+    f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
+       (sigma_state … gss st prf) =
+  return sigma_state … gss st' prf'.
+  #p #p' #graph_prog #stack_sizes #sigma #gss
+  #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
+  #st' #prf
+  whd in match eval_statement_no_pc; normalize nodelta
+  [ @eval_seq_no_pc_sigma_commute
+  |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
+  | (* tailcall, follow proof of CALL in previous lemma *)
+    cases daemon
+  ]
+qed.
+
+=======
            whd in match sigma_is_opt; >H normalize nodelta >ABS
            whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
@@ -1581 +1721 @@
   | (*C_OP1*)
     
+>>>>>>> .r2528
 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
@@ -1588 +1729 @@
  ∀p,p',graph_prog.
   let lin_prog ≝ linearise ? graph_prog in
- ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
- let graph_stack_sizes ≝
-  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
-    ? graph_prog lin_stack_sizes in
- (∀sigma.good_sigma_state p p' graph_prog sigma) →
+ ∀stack_sizes.
+ (∀sigma.good_state_sigma p p' graph_prog sigma) →
    ex_Type1 … (λR.
    status_simulation
-    (graph_abstract_status p p' graph_prog graph_stack_sizes)
-    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
+    (graph_abstract_status p p' graph_prog stack_sizes)
+    (lin_abstract_status p p' lin_prog stack_sizes) R).
  #p #p' #graph_prog
- cases (linearise_spec … graph_prog) #sigma #good
- #lin_stack_sizes
+ letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
+ cut (∀fn.good_local_sigma … (sigma fn))
+  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
+ #good
+ #stack_sizes
  #gss lapply (gss sigma) -gss #gss
- %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
+ %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
 whd in match graph_abstract_status;
 whd in match lin_abstract_status;
@@ -1616 +1757 @@
   (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
 whd in match eval_state in ⊢ (%→?); normalize nodelta
-change with (Σi.is_internal_function_of_program ? graph_prog i) in
-match (Sig ??) in ⊢ (%→?);
-letin globals ≝ (prog_var_names ?? graph_prog)
-change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
-  match (fetch_statement ?????) in ⊢ (%→?);
-#ex
-cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
-#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
-#EQfetch
-cases (bind_inversion ????? EQfetch)
-#f_id * #H lapply (opt_eq_from_res ???? H) -H
-#EQfunc_of_block
-#H elim (bind_inversion ????? H) -H #stmt' *
-#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
-whd in ⊢ (??%%→?); #EQ destruct(EQ)
-#EQeval
-cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
-letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
-#entry_0
-#good_local
-* * #wf_pc #wf_state #EQst2
+@'bind_inversion
+** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt
+cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_
+@'bind_inversion
+#st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance
+* #wf_prf #st2_EQ
+
+cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
+* #EQfetch_stmt' #all_labels_in
+
+letin lin_prog ≝ (linearise … graph_prog)
+lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
+whd in match eval_state in ⊢ (???%→?);
+>st2_EQ in ⊢ (???%→?); normalize nodelta
+>EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?);
+cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
+#wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
+
+whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
+>EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
+normalize nodelta
+
+cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement;
+normalize nodelta
+[ whd in match joint_classify_step; @cond_call_other 
+  [ (* COND *) #a #lbltrue #nxt
+    #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta
+    #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other
+    [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
+    #bv #bv_no_pc #EQretrieve
+    cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve)
+    #ignore >(sigma_bv_no_pc … bv_no_pc)
+    change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?)
+    #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?);
+    #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv
+    >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta
+    [ whd in match goto; normalize nodelta
+      >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?);
+      #EQ destruct(EQ) #ex_advance #ex_advance'
+      % [2: %{(tal_base_not_return …)} [3: @ex_advance'
+  | (* CALL *) #f #args #dest #nxt
+  | (* other *) #stmt #no_call #nxt
+  ] normalize nodelta
+  [ #ex 
+    #ex_advance #ex_advance'
+  | whd in ⊢ (??%%→?); #EQ destruct(EQ)
+    #H @('bind_inversion H) -H #called_block
+    #H lapply (err_eq_from_io ????? H) -H #EQcalled_block
+    #H @('bind_inversion H) -H * #called * #called_fn
+    #H lapply (err_eq_from_io ????? H) -H #EQcalled
+    normalize nodelta
+    [ #H lapply (err_eq_from_io ????? H) -H ]
+    #H @('bind_inversion H) -H
+     | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ]
+    #ex_advance #ex_advance'
+    whd in match joint_classify_seq; normalize nodelta
+    >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
+    
+    cut (∀p,p',graph_prog,sigma,gss,st,f,bl.
+        ∀prf : well_formed_state p p' graph_prog sigma gss st.
+        block_of_call (make_sem_graph_params p p') ?
+          (globalenv_noinit ? graph_prog) st f = return bl →
+        block_of_call (make_sem_lin_params p p') ?
+          (globalenv_noinit ? (linearise … graph_prog))
+          (sigma_state … st prf) f = return bl)
+      [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute
+      whd in match eval_seq_advance; normalize nodelta
+      >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?);
+      >m_return_bind in ⊢ (???%→?);
+      >(fetch_function_transf … EQcalled :
+        fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?);
+      >m_return_bind in ⊢ (???%→?);
+      whd in match (transf_fundef); normalize nodelta
+        
+        
+      #block_of_call_sigma_commute
+    @match_int_fun #called_descr #EQcalled_descr
+    [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ]
+    #ex_advance
+    cut 
+      (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ.
+      ∀trans : ∀vars.A vars → B vars.
+      let prog_out : program (λvars.fundef (B vars)) ℕ ≝
+        transform_program ??? prog (λvars.transf_fundef … (trans vars)) in
+      ∀i.is_function … (globalenv_noinit … prog) i →
+       is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ]
+    #f_propagate
+    letin sigma_function ≝ (λA,B,prog,trans.
+      λf : Σi.is_function ? (globalenv_noinit ? prog) i.
+      «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *)
+    cut (∀p,p',graph_prog.
+      let lin_prog ≝ linearise ? graph_prog in
+      ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
+      ∀f,st,fn.
+      ∀prf : well_formed_state … gss st.
+      function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog)
+        st f = return fn →
+      function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
+        (sigma_state … gss st prf) f = return sigma_function … fn)
+        [1,3: (* TODO lemma *) cases daemon ]
+    #function_of_call_sigma_commute
+    whd in match joint_classify_step; whd in match joint_classify_seq;
+    normalize nodelta #next_spec
+    >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?);
+    >m_return_bind in ⊢ (%→?);
+    @match_int_fun
+    [2,3: #EQdescr' lapply EQdescr'
+      >description_of_function_transf in EQdescr';
+      
+    
+    whd in match sigma_beval; normalize nodelta
+    cases bv
+    [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ]
+    whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?);
+    [7: #ignore #_ 
+    #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve
+    whd in match (bool_of_beval ?) in ⊢ (% → ?);
+    3: >no_call_advance [2: @no_call]
+  
+
+
 generalize in match wf_pc in ⊢ ?;
 whd in ⊢ (%→?);
@@ -1656 +1897 @@
 *
 #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
-letin lin_prog ≝ (linearise … graph_prog) 
-lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
 destruct(EQst2)
 whd in match eval_state in ⊢ (???%→?); normalize nodelta
-letin st2 ≝ (sigma_state_pc ????? st1 ?)
->(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
->m_return_bind in ⊢ (%→?);
-#ex'
 (* resolve classifier *)
-whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
->EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
-normalize nodelta
-cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
 [ *
   [ #stmt #nxt

src/joint/semantics.ma

@@ -16 +16 @@
 { 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) → ℕ
+; stack_sizes : ident → option ℕ
 }.
-
-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).
@@ -122 +110 @@
 *)
 
-(* 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.
@@ -144 +122 @@
 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).
-  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)).
+  (Σ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
@@ -171 +163 @@
   ; 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
-  (* 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
@@ -187 +179 @@
   ; 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)
+    ident → F globals (* current *) → state st_pars → res (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)
+    ident → F globals (* current *) → state st_pars → res (state_pc st_pars)
   }.
 
@@ -241 +233 @@
  return 〈bv, set_istack … is st〉.
 
-definition save_ra : ∀p. state p → program_counter → res (state p) ≝
+definition push_ra : ∀p. state p → program_counter → res (state p) ≝
  λp,st,l.
   let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
@@ -247 +239 @@
   push … st' addrh.
 
-definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
+definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝
  λp,st.
   ! 〈addrh, st'〉 ← pop … st;
@@ -255 +247 @@
 
 (* 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
+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
@@ -278 +271 @@
 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 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.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.
+  ∀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 ((Σ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
+  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 〈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
+  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 pc_of_point p msp ptr pt.
-
-definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
+  return mk_program_counter bl (offset_of_point p pt).
+
+definition succ_pc : ∀p : sem_params.
   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).
-
+  λ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))
@@ -371 +352 @@
 
 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.
+  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 mk_state_pc … st newpc.
 
 (*
@@ -383 +364 @@
 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
+ let newpc ≝ succ_pc … (pc … st) l in
  mk_state_pc … st newpc.
 
-
-definition function_of_call ≝ λp:sem_params.λglobals.
+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_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)
-  ].
+  ! 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).
 
 (* 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 ???;
+λ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));
@@ -408 +399 @@
          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.
+      set_result … p vs dest st.
+
+axiom MissingStackSize : String.
 
 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 ;
+λ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.
 
+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 _ nxt ⇒ return nxt
+  | _ ⇒ Error … [MSG NoSuccessor]
+  ].
+
 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
+ ∀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_fn st
+    eval_ext_seq … ge c curr_id curr_fn st
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -481 +474 @@
   | 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
+  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
   ].
-[ @hide_prf
+  @hide_prf
   @find_symbol_in_globals
   lapply prf
@@ -497 +483 @@
   [@eq_identifier_elim #H * >H %1 % ]
   #G %2 @IH @G
-| @(description_of_internal_function … prf)
-]
 qed.
 
-definition eval_seq_pc : 
+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 st f : IO ???;
+! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
+match fd with
+[ Internal ifd ⇒
+  ! st' ← save_frame … dest st ;
+  ! st'' ← eval_internal_call_no_pc 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
+| External efd ⇒
+  ! st' ← eval_external_call … efd args dest st ;
+  return mk_state_pc … st' (succ_pc p (pc … st) nxt)
+].
+
+definition eval_seq_advance : 
  ∀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.
+  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 ⇒
-    ! 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
+    eval_seq_call … ge f args dest nxt st
+  | _ ⇒ return next … nxt st
   ].
-@(description_of_internal_function … prf)
-qed.
-
-definition eval_statement :
+
+definition eval_statement_no_pc :
  ∀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.
+ 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
+    ]
+  | final s ⇒ 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 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 st f : IO ???;
+! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
+match fd with
+[ Internal ifd ⇒
+  ! st' ← eval_internal_call_no_pc 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
+| 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 with
+  [ sequential s nxt ⇒
     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
+      eval_seq_advance … ge s nxt st
     | 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'
+      if b then
+        goto … ge l st
+      else
+        return next … nxt st
     ]
   | 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
+    [ GOTO l ⇒ goto … ge l st
+    | RETURN ⇒ eval_return … ge curr_id 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 …)
+      eval_tailcall … ge f args curr_id curr_fn st
     ]
   ].
-@(description_of_internal_function … prf)
-qed.
 
 definition eval_state : ∀p:sem_params. ∀globals: list ident.
@@ -570 +583 @@
   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.
+  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
+  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
+  let st'' ≝ mk_state_pc … st' (pc … st) in
+  eval_statement_advance … ge id fn s st''.
 
 (* Paolo: what if in an intermediate language main finishes with an external
@@ -579 +594 @@
   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
+  do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
   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' ;
+      do st' ← pop_frame … ge id fn st;
+      ! nxt ← next_of_pc … ge (pc … st') ;
+      let pc' ≝ succ_pc … (pc … st') nxt in
+      if eq_program_counter pc' exit then 
+       do vals ← read_result … ge (joint_if_result … fn) st ;
        Word_of_list_beval vals
       else

src/joint/semanticsUtils.ma

@@ -75 +75 @@
   mk_sem_params
     g_pars
-    (mk_more_sem_params
-      g_pars
-      (spars ?)
-      (word_of_identifier ?)
-      (an_identifier ?)
-      ? (refl …)
-    ).
+    (spars ?)
+    (word_of_identifier ?)
+    (an_identifier ?)
+    ? (refl …).
 * #p % qed.
 
@@ -89 +86 @@
 @pos_elim [%]
 #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
-
 
 definition make_sem_lin_params :
@@ -99 +95 @@
   mk_sem_params
     lin_pars
-    (mk_more_sem_params
-      lin_pars
-      (spars ?)
-      succ_pos_of_nat
-      (λp.pred (nat_of_pos p))
-      ??
-    ).
-[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
-| #n >nat_succ_pos %
+    (spars ?)
+    succ_pos_of_nat
+    (λp.pred (nat_of_pos p))
+    ??.
+[ #n >nat_succ_pos %
+| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
 ] qed.
+
+
+
+
+lemma fetch_statement_eq : ∀p:sem_params.∀g.
+  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
+  ∀i,fn,s.
+  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
+  let pt ≝ point_of_pc … ptr in
+  stmt_at … (joint_if_code … fn) pt = Some ? s →
+  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
+#p #g #ge #ptr #i #f #s #EQ1 #EQ2
+whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
+>EQ2 %
+qed.
+
+lemma fetch_statement_inv : ∀p:sem_params.∀g.
+  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
+  ∀i,fn,s.
+  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
+  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
+  let pt ≝ point_of_pc p ptr in
+  stmt_at … (joint_if_code … fn) pt = Some ? s.
+#p #g #ge #ptr #i #fn #s #H
+elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
+elim (bind_inversion ????? H) #s' * #H
+lapply (opt_eq_from_res ???? H) -H #EQ2
+whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
+qed.
+

src/joint/semantics_blocks.ma

@@ -1 +1 @@
 include "joint/blocks.ma".
 include "joint/Traces.ma".
+include "joint/semanticsUtils.ma".
 
 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
@@ -8 +9 @@
   ].*)
 
-lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer.
-  ∀fn,pt,s.
-  fetch_function … ge ptr = OK … fn →
-  point_of_pointer ? p … ptr = pt →
-  stmt_at … (joint_if_code … fn) pt = Some ? s →
-  fetch_statement ? p … ge ptr = OK … 〈fn, s〉.
-#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
-whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
->EQ2 >EQ3 >m_return_bind %
-qed.
-
-include alias "basics/logic.ma".
-lemma io_evaluate_bind : ∀O,I,X,Y,env.
-∀m : IO O I X.∀f : X → IO O I Y.
-io_evaluate O I Y env (! x ← m ; f x) =
-! x ← io_evaluate O I X env m ;
-io_evaluate O I Y env (f x).
-#O #I #X #Y #env #m elim m
-[ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
-  change with (! y ← ? ; ?) in ⊢ (??%(????%?));
-  >m_bind_bind @m_bind_ext_eq #i @IH
-| #x #f %
-| #e #f %
-]
-qed.
-
-lemma fetch_function_from_block_eq :
-  ∀p,g,ge.
-  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
-  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
-#p #g #ge #ptr1 #ptr2 #EQ
-whd in match fetch_function; normalize nodelta >EQ
-@m_bind_ext_eq // qed.
-
-let rec repeat_eval_seq_no_pc
-  (p : evaluation_params) env curr_fn
-  (l : list (joint_seq p (globals p))) on l :
-  state p → res (state p) ≝
-  λst.match l with
-  [ nil ⇒ return st
-  | cons hd tl ⇒
-    ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ;
-    repeat_eval_seq_no_pc p env curr_fn tl st'
-  ].
-
-lemma err_to_io_evaluate : ∀O,I,X,env,m.
-  io_evaluate O I X env (err_to_io … m) = m.
-#O#I#X#env * // qed.
+definition repeat_eval_seq_no_pc ≝
+  λp : evaluation_params.λcurr_id,curr_fn.
+  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
 
 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
 
-definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
-  λp,g,s.match s with
-  [ COST_LABEL _ ⇒ false
-  | CALL_ID _ _ _ ⇒ false
-  | extension_call _ ⇒ false
-  | _ ⇒ true
-  ].
-
-lemma no_call_nor_label_proceed : ∀p : evaluation_params.
-∀st : state p. ∀s.
-no_call_nor_label p (globals p) s →
-eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.
-#p #st * // [ #f #args #dest | #c ] *
-qed.
-
-lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
-no_call_nor_label p (globals p) s →
-step_classifier … s = cl_other.
-#p * // [ #f #args #dest | #c ] *
-qed.
-
-lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
-no_call_nor_label p (globals p) s →
-cost_label_of_stmt … (sequential … s nxt) = None ?.
-#p * // #lbl#next *
-qed.
-
-definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝
-  λp,g,c.code_closed … c∧
-    ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.
-
-definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.
-  ∀c,pc,step,dst.
-  code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →
-  Σpc'.pointer_of_point p p pc dst = return pc' ≝
-  λp,g,c,pc,step,dst,c_compact,step_in.
-  match pointer_of_point p p pc dst
-  return λx.pointer_of_point p p pc dst = x → ?
-  with
-  [ OK pc' ⇒ mk_Sig ?? pc'
-  | Error e ⇒ λEQ.⊥
-  ] (refl …).
-cases step_in #nxt * #EQ1 #EQ2
-cases c_compact -c_compact #c_closed #c_compact
-elim (c_compact dst pc ?)
-[ >EQ #pc' normalize #ABS destruct(ABS)
-| elim (c_closed … EQ1) #_ whd in ⊢ (%→?);
-  >EQ2 #H @H
-]
-qed.
-
-let rec pointer_of_point_in_code 
-  p g c pc dst b on b :
-  ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →
-  Σpc'.pointer_of_point p p pc dst = return pc' ≝
-match b
-return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'
-with
-[ nil ⇒
-  λl,c_compact,in_code.
-  match pointer_of_point p p pc dst
-  return λx.pointer_of_point p p pc dst = x → ? with
-  [ OK ptr' ⇒ mk_Sig ?? ptr'
-  | Error e ⇒ λEQ.⊥
-  ] (refl …)
-| cons hd tl ⇒
-  λl.match l return λl.? → ? → Σptr'.? with
-  [ nil ⇒ λc_compact,in_code.⊥
-  | cons mid rest ⇒ λc_compact,in_code.
-    let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in
-    pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)
-  ]
-].
-[ cases l in in_code; [2: #mid #rest * ]
-  whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]
-  normalize #ABS destruct(ABS)
-| cases (pointer_of_point_in_code ?????????)
-  #ptr' >pointer_of_point_uses_block
-  [ #H @H |*:]
-  cases mid_pc -mid_pc #mid_pc @pointer_of_point_block
-| elim in_code
-| cases mid_pc -mid_pc #mid_pc #EQ
-  >(point_of_pointer_of_point … EQ)
-  cases in_code #_ #H @H
-| cases in_code #H #_ @H
-]
-qed.
-
 let rec produce_trace_any_any
   (p : evaluation_params)
-  (st : state_pc p) fd
+  (st : state_pc p)
+  curr_id curr_fn
   (b : list (joint_seq p (globals p))) on b :
   ∀l : list (code_point p).
   ∀dst : code_point p.
   ∀st' : state p.
-  fetch_function p ? (ev_genv p) (pc … st) = return fd →
-  ∀prf1 : code_compact p (globals p) (joint_if_code … fd).
-  let src ≝ point_of_pointer p p (pc … st) in
+  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
+    return 〈curr_id, curr_fn〉 →
+  let src ≝ point_of_pc p (pc … st) in
   if list_not_empty ? b then
-    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
+    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
   else
     True →
-  ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.
-  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
-  repeat_eval_seq_no_pc p (io_env p) fd b st = return st' →
+  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
+  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
+  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
   trace_any_any (joint_abstract_status p) st
-    (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝
-  match b
-  return λx.∀l,dst.?→?→?→?→?→?→?→?
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
+  return λb.∀l,dst.?→?→?→?→?→?→?
   with
   [ nil ⇒
-    λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
+    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
     (taa_base (joint_abstract_status p) st)
-      ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉
+    ⌈trace_any_any ??? ↦ ?⌉
   | cons hd tl ⇒
     λl.
-    match l return λx.?→?→?→?→?→?→?→?→? with
-    [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥
+    match l return λx.∀dst,st'.?→?→?→?→?→? with
+    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
     | cons mid rest ⇒
-      λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
-      let mid_pc ≝
-        pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st)
-          hd mid c_compact ? in
-      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd)
-      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ?
-      with
-      [ OK st_mid ⇒ λEQ2.
+      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
+      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
+      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
+      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
+      trace_any_any (joint_abstract_status p) st
+        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
+      [ Value st_mid ⇒ λEQ2.
         let tr_tl ≝ produce_trace_any_any ?
             (mk_state_pc ? st_mid mid_pc)
-            fd tl rest dst ??????? in
-        (* works fast only in interactive mode:
-        taa_step … tr_tl *) ?
-      | Error _ ⇒ λEQ2.⊥
+            curr_id curr_fn tl rest dst ?????? in
+        taa_step … tr_tl
+      | _ ⇒ λEQ2.⊥
       ] (refl …)
     ]
-  ].[3: @(taa_step … tr_tl) |*:]
-try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc)
-try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code)
-try (cases all_other #hd_other #tl_other)
+  ].
+[ whd in EQ1 : (??%%);
+  cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
+  >pc_of_point_of_pc cases st //
+| @in_code
+|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
+]
+change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
+>EQ2 in EQ1; >m_return_bind
+cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
+cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
+#EQ1
+try assumption
 [ whd whd in match eval_state; normalize nodelta
-  >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
+  >(fetch_statement_eq … fd_prf EQ_stmt_at)
   >m_return_bind
-  whd in match eval_statement; normalize nodelta
-  whd in match eval_step; normalize nodelta
-  >m_bind_bind
-  >(no_call_nor_label_proceed … hd_other) >m_return_bind
-  >m_bind_bind
-  >io_evaluate_bind >EQ2 >m_return_bind
-  >m_return_bind
+  whd in match eval_statement_no_pc; normalize nodelta
+  >EQ2 >m_return_bind
+  whd in match eval_statement_advance; normalize nodelta
+  >(no_call_advance … hd_no_call)
+  whd in match next; normalize nodelta 
   whd in match succ_pc; normalize nodelta
-  >EQ_mid >EQ_mid_pc >m_return_bind %
-| whd %{fd} %{(sequential … hd nxt)}
-  %{(no_call_nor_label_other … hd_other)}
-  @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
-|4: cases (pointer_of_point_in_code ?????????)
-  #dst_pc
-  cases l in in_code; [2: #mid #rest * ]
-  whd in ⊢ (%→?); #EQ' <EQ'
-  >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1
-  normalize in ⊢ (%→%→?);
-  #EQ1 #EQ'' destruct cases st //
-|5: >fetch_function_from_block_eq [ @fd_prf |*: ]
-  @(pointer_of_point_block … EQ_mid_pc)
-|6: cases tl [ % ] #hd' #tl' @dst_prf
-|7: assumption
-|8,9:
-  lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta
-  [ #H @H
-  | normalize #ABS destruct(ABS)
+  >EQ_mid %
+| whd whd in ⊢ (??%?);
+  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
+  @(no_call_other … hd_no_call)
+| whd in ⊢ (?%);
+  whd in match as_label; normalize nodelta
+  %* #H @H -H whd in ⊢ (??%?);
+  whd in match (as_pc_of ??);
+  inversion (fetch_statement ????) normalize nodelta
+  [2: // ]
+  ** #i' #f' #stmt' #EQ
+  elim (fetch_statement_inv … EQ)
+  >fd_prf
+  whd in ⊢ (??%?→?); #EQ destruct(EQ)
+  whd in ⊢ (%→?);
+  whd in match (point_of_pc ??); >point_of_offset_of_point
+  #EQ'
+  cases tl in tl_other rest_in_code;
+  [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
+    >EQ' in dst_prf; >m_return_bind #H @H
+  | #hd' #tl' ** #_ #hd_no_cost' #_
+    cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
+    >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
+    @(no_label_uncosted … hd_no_cost')
   ]
-|3:
-  %* #H @H -H
-  lapply tl_other lapply rest_in_code
-  cases tl [2: #hd' #tl' ]
-  cases rest [2,4: #mid' #rest']
-  [2,3: * ]
-  [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
-  | ** #nxt' * #at_mid #_ #_ * #mid_other #_
-  ]
-  whd in ⊢ (??%?);
-  [ lapply dst_prf ]
-  whd in match as_label;
-  whd in match (as_pc_of ??);
-  whd in match fetch_statement;
-  normalize nodelta
-  >(point_of_pointer_of_point … EQ_mid_pc)
-  >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc))
-  >fd_prf >m_return_bind
-  [ cases (stmt_at ????) [ #_ % ]
-    #stmt #H @H
-  | >at_mid >m_return_bind normalize nodelta
-    @(no_call_nor_label_uncosted … mid_other)
-  ]
+| >dst_prf cases (list_not_empty ??) %
+| normalize nodelta >point_of_pc_of_point assumption
 ]
 qed.