include "joint/blocks.ma".
include "joint/semantics_paolo.ma".


axiom ExecutingInternalCallInBlock : String.

let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
  match b with
  [ nil ⇒ [ ]
  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
  ].

definition step_flow_change_labels :
  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    step_flow p g lbls1 → step_flow p g lbls2 ≝
  λp,g,lbls1,lbls2,prf,flow.
  match flow with
  [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
  | Init id b args dest ⇒ Init … id b args dest
  | Proceed ⇒ Proceed ???
  ].

coercion step_flow_diff_lbls :
  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
  ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
  step_flow_change_labels on _flow : step_flow ??? to step_flow ???.

definition monad_step_flow_times_coerc :
  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
    λp,g,lbls1,lbls2,M,A,H,m.
    ! 〈flow,a〉 ← m ;
    return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.

coercion step_flow_monad_times :
  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
  monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).

let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
  (st : state p) (b : list (joint_step p globals)) on b :
    IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
    match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
    [ nil ⇒ return 〈Proceed ???, st〉
    | cons hd tl ⇒
      ! 〈flow, st'〉 ← eval_step … ge st hd ;
      match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
      [ Proceed ⇒ eval_seq_list globals p ge st' tl
      | _ ⇒ return 〈flow, st'〉
      ]
    ]. /2 by Exists_append_r, Exists_append_l/ qed.

definition fin_step_flow_change_labels :
  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
  λp,g,lbls1,lbls2,prf,flow.
  match flow with
  [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
  | FTailInit id b args ⇒ FTailInit … id b args
  | FEnd ⇒ FEnd ???
  ].

coercion fin_step_flow_diff_lbls :
  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
  ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
  fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.

definition monad_fin_step_flow_times_coerc :
  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
    λp,g,lbls1,lbls2,M,A,H,m.
    ! 〈flow,a〉 ← m ;
    return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.

coercion fin_step_flow_monad_times :
  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
  monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).

definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
  seq_list_labels … (\fst b) @
  match ty return λx.stmt_type_if ? x ??? → ? with
  [ SEQ ⇒ step_labels …
  | FIN ⇒ fin_step_labels …
  ] (\snd b).

definition eval_block_cont :
  ∀globals.∀p : sem_params.∀ty.genv globals p →
  state p → ∀b : block_cont p globals ty.
  IO io_out io_in (
    (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
    (state p)) ≝ λglobals,p,ty,ge,st.
  match ty return λx.∀b : block_cont p globals x.
    IO io_out io_in (
      (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
      (state p))
  with
  [ SEQ ⇒ λb.
    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
    [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    | Proceed ⇒ eval_step … ge st' (\snd b)
    | Init _ _ _ _ ⇒
      Error … (msg ExecutingInternalCallInBlock)
    ]
  | FIN ⇒ λb.
    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
    [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    | Proceed ⇒ eval_fin_step … ge st' (\snd b)
    | Init _ _ _ _ ⇒
      Error … (msg ExecutingInternalCallInBlock)
    ]
  ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.

(*
lemma m_pred

lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
  ∀f : X → monad M Y.m_pred MP P … m →
  ! x ← m ; f x = ! x ←  
*)

definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
  λp,globals,lbls,A,flp.
  match \fst flp with
  [ Init _ _ _ _ ⇒ False
  | _ ⇒ True
  ].

definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
  λp,globals,lbls,A,flp.
  match \fst flp with
  [ Proceed ⇒ True
  | _ ⇒ False
  ].

definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
λp,globals,ge,s.match s with
[ CALL_ID f args dest ⇒
  Try
    ! b ← find_symbol … ge f ;
    ! fd ← find_funct_ptr … ge b ;
    match fd with
    [ Internal _ ⇒ return False
    | External _ ⇒ return True
    ]
  catch ⇒
    True
| extension c ⇒
  ∀st : state p.
  pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
| _ ⇒ True
].

definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].

lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
  err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
#O #I #X #Y * //
qed.

lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
#O #I #X #m elim m // qed.

(*
lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
#X #m elim m // qed.
*)

(*
lemma never_calls_no_init : ∀p,globals,ge,s.
  never_calls p globals ge s →
  ∀st : state p.
  pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
#p#g#ge * //
[10,12:
|*:
  #a #b #c try #d try #e try #f try #g
  @res_io_pred
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st *  try (@mp_return @I)
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st * [9: elim st] normalize nodelta try (@mp_return @I)
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st *  try (@mp_return @I)
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
  try (@mp_return @I)
  @(mp_bind … (λ_.True) … (pred_res_True …))
  #st * @mp_return @I
]
[ #id #args #dest #H whd in H;
  #st change with (! x ← ? ; ?) in match (eval_step ?????);
  elim (find_symbol ???) in H ⊢ %; [//]
  #b >m_return_bind  >m_return_bind
  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
  elim (find_funct_ptr ???) [//]
  #fd >m_return_bind  >m_return_bind
  elim fd #fn normalize nodelta *
  @(mp_bind … (λ_.True)) [//]
  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
  #st * @mp_return %
| #s #H @H
]
qed.

lemma unbranching_truly_sequential : ∀p,globals,ge,s.
  unbranching p globals ge s →
  ∀st : state p.
  pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
#p#globals#ge#s * #H #G #st
lapply (never_calls_no_init … H st) @m_pred_mp
>G * *
[ * #lbl * | #id #fd #args #dest ] #st * %
qed.
*)

lemma seq_list_labels_append : ∀p,globals,b1,b2.
  seq_list_labels p globals (b1 @ b2) =
  seq_list_labels … b1 @ seq_list_labels … b2.
#p #g #b1 elim b1
[ //
| #hd #tl #IH #b2 whd in ⊢ (??%%);
  >associative_append <IH %
]
qed.

(*
lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
  eval_seq_list globals p ge st (b1@b2) =
  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
  match flow with
  [ Proceed ⇒
    ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
    return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
  | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
  ].
[2,3,4:
  #lbl #H >seq_list_labels_append
  [1,2: @Exists_append_l | @Exists_append_r ] @H ]
#globals#p#ge#st#b1 lapply st -st elim b1
[ #st #b2 >m_return_bind normalize nodelta
  <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
  @m_bind_ext_eq ** 
  [ * #lbl #H | #id #fd #args #dest ] #st' %
| #hd #tl #IH #st #b2
  whd in match (? @ b2);
  whd in match (eval_seq_list ?????);
  whd in match (eval_seq_list ???? (hd :: tl));
  >m_bind_bind
  @m_bind_ext_eq
  ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
  [1,2: @m_return_bind]
  >m_bind_bind
  >IH >m_bind_bind
  @m_bind_ext_eq **
  [#lbl | #id #fd #args #dest ] #st' normalize nodelta
  >m_return_bind
  [1,2: @m_return_bind ]
  >m_bind_bind normalize nodelta
  @m_bind_ext_eq **
  [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
]
qed.

lemma eval_seq_list_unbranching :
∀globals,p,ge,st,b.
  All ? (unbranching … ge) b →
  pred_io … (λ_.True) (truly_sequential …)
    (eval_seq_list globals p ge st b).
#globals#p#ge#st #b lapply st -st elim b
[ #st * %
| #hd #tl #IH #st * #hd_ok #tl_ok
  @mp_bind
  [2: @(unbranching_truly_sequential … hd_ok st) |]
  ** [#lbl|#id#fd#args#dest] #st' *
  normalize nodelta
  @mp_bind [2: @(IH st' tl_ok)|]
  ** [#lbl|#id#fd#args#dest] #st'' * %
]
qed.

lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
  pred_io O I A Perr P v →
  rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
#O #I #A #Perr #P #v elim v
[ #o #f #IH whd in ⊢ (%→%);
  #H %{(refl …)} #i @IH @H
|*: /2/
]
qed.

lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
  All ? (unbranching … ge) b1 →
  eval_seq_list globals p ge st (b1@b2) =
  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
  ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
  return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
[2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
#globals #p #ge #st #b1 #b2 #H
>eval_seq_list_append
@mr_bind
[2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
** [#lbl|#id#fd#args#dest] #st
#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
qed.
*)
lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
  block_cont_labels p globals ty (b1 @ b2) =
  block_cont_labels … b1 @ block_cont_labels … b2.
#p #g #ty * #l1 #s1 * #l2 #s2
whd in match (〈?,?〉@?); whd in ⊢ (??%?);
>seq_list_labels_append
>associative_append
>associative_append
>associative_append %
qed.
(*
lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
  eval_block_cont ??? ge st (b1@b2) =
  ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
  match ty return λx.
    block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
  [ SEQ ⇒ λb2.
    match flow with
    [ Proceed ⇒ 
      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
      return 〈?, st''〉
    | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    ]
  | FIN ⇒ λb2.
    match flow with
    [ Proceed ⇒ 
      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
      return 〈?, st''〉
    | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    ]
  ] b2.
[3,5: whd in flow'; @flow'
  #lbl >block_cont_labels_append @Exists_append_r
|2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
]
#globals#p * whd in match stmt_type_if; normalize nodelta
#ge#st * #l1 #s1 * #l2 #s2
whd in match (〈?,?〉@?);
whd in match eval_block_cont; normalize nodelta
>m_bind_bind
>eval_seq_list_append
>m_bind_bind
@m_bind_ext_eq

 whd in ⊢ (??%?);
    match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
    [ SEQ ⇒ 
    | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
    ]
  | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
  ].
#globals#p#ty#ge#st*#l1#s1*#l2#s2
whd in match (〈?,?〉@?);
whd in match eval_block_cont; normalize nodelta
>m_bind_bind
>eval_seq_list_append
>m_bind_bind
@m_bind_ext_eq
** [#l|#id#fd#args#dest] normalize nodelta #st'
[1,2:>m_return_bind normalize nodelta
  [ >m_return_bind ] % ]
change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
>m_bind_bind whd in match stmt_type_if;
normalize nodelta
>m_bind_bind
@m_bind_ext_eq
**[#l|#id#fd#args#dest] normalize nodelta #st''
[1,2: >m_return_bind normalize nodelta % | % ]
qed.
*)


(* just like repeat, but without the full_exec infrastructure, and it
   stops upon a non-proceed flow cmd *)
let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
  (st : state_pc p) on n :
    IO io_out io_in (bool × (state_pc p)) ≝
match n with
[ O ⇒ return 〈false,st〉
| S k ⇒
  ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
  if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
].

definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
λp,g,ty,b.S (|\fst b|).

interpretation "block cont size" 'norm b = (block_size ??? b).

lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
  repeat_eval_state_flag (n1 + n2) globals p ge st =
  ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
  if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
#n1 elim n1 -n1 [| #n1 #IH]
#n2 #globals #p #ge #st
[ @m_return_bind
| change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
  >m_bind_bind in ⊢ (???%);
  @m_bind_ext_eq ** #st' normalize nodelta
  [ % | @IH ]
]
qed.

lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
  repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
#globals #p #ge #st
change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
<(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
@m_bind_ext_eq ** #st %
qed.

lemma eval_tunnel_step :
  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
  fetch_function … ge (pc … st) = OK … fn →
  point_of_pointer ? p … (pc … st) = OK … src →
  src ~~> dst in joint_if_code … fn →
  eval_state_flag g p ge st =
    return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
change with (! s ← ? ; ?) in match (eval_state_flag ????);
change with (! fn ← ? ; ?) in match (fetch_statement ?????);
>pc_pt in ⊢ (??%?); >m_return_bind
>fetch_fn in ⊢ (??%?); >m_return_bind
>EQ1 in ⊢ (??%?);  >m_return_bind
>EQ2 in ⊢ (??%?);
change with (! st ← ? ; ?) in match (eval_statement ?????);
whd in match eval_fin_step; normalize nodelta
>m_return_bind
whd in match eval_fin_step_flow; normalize nodelta
change with (! ptr ← ? ; ?) in match (goto ??????);
whd in match pointer_of_label_in_block; normalize nodelta
whd in match fetch_function in fetch_fn;
normalize nodelta in fetch_fn; 
>fetch_fn in ⊢ (??%?); >m_return_bind
>EQ2 in ⊢ (??%?); >m_return_bind
cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
elim (pointer_compat_from_ind … H) %
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.

(*
lemma eval_tunnel :
  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
  fetch_function … ge (pc … st) = OK … fn →
  point_of_pointer ? p … (pc … st) = OK … src →
  src ~~>^* dst in joint_if_code … fn →
  ∃n.repeat_eval_state n g p ge st =
    return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
elim through [2: #hd #tl #IH]
#st #src #fetch_fn #pc_pt
[2: #EQ <EQ %{0}
  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
* #H1 #H2
letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
elim (IH st' … H2)
[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
  @pointer_of_point_block
|2:
  whd in match st'; >point_of_pointer_of_point %
]
#n' #EQ %{(S n')}
change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
>EQ %
qed.

lemma eval_tunnel_plus :
  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
  fetch_function … ge (pc … st) = OK … fn →
  point_of_pointer ? p … (pc … st) = OK … src →
  src ~~>^+ dst in joint_if_code … fn →
  ∃n.repeat_eval_state (S n) g p ge st =
    return set_pc … (pointer_of_point ? p (pc … st) dst) st.
#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
elim (eval_tunnel … ge st' … H2)
[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
  @pointer_of_point_block
|2:
  whd in match st'; >point_of_pointer_of_point %
]
#n #EQ %{n}
change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
>EQ %
qed.
*)

lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
  ∀fn,pt,s.
  fetch_function … ge ptr = OK … fn →
  point_of_pointer ? p … ptr = OK … pt →
  stmt_at … (joint_if_code … fn) pt = Some ? s →
  fetch_statement ? p … ge ptr = OK … s.
#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind
>EQ1 >m_return_bind >EQ3 %
qed.
(*
lemma eval_seq_list_in_code :
  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
  fetch_function … ge (pc … st) = OK … fn →
  point_of_pointer ? p … (pc … st) = OK … src →
  All ? (never_calls … ge) B →
  seq_list_in_code … (joint_if_code … fn) src B dst →
  repeat_eval_state_flag (|B|) g p ge st =
   ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
   match flow with
   [ Redirect l ⇒
     ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
     return 〈true, st''〉
   | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
       (* dummy, never happens *)
   | Proceed ⇒
     let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
     return 〈false, mk_state_pc ? st' nxt_ptr〉
   ].
#p #g #ge #st #fn #src #B lapply src -src
lapply st -st elim B [|#hd #tl #IH]
#st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
[2: #EQ normalize in EQ; <EQ
  whd in match (eval_seq_list ???? [ ]);
  >m_return_bind normalize nodelta
  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
|1: * #n * #EQat #H
  change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
  >m_bind_bind
  >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
  >m_bind_bind >m_bind_bind
  lapply (never_calls_no_init … hd_ok st) #hd_ok'
  @(mr_bind …
    (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
  [ lapply hd_ok' elim (eval_step ?????)
    [ #o #f #IH'
      whd in ⊢ (%→%); #G
      %{(refl …)} #i @IH' @G
    |*: #v whd in ⊢ (%→%); #H
      % [ % ] @H
    ]
  | ** [#lbl | #id #fd #args #dest ] #st'
    #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
    whd in match succ_pc; normalize nodelta
    >pc_pt >m_return_bind
    letin src' ≝ (point_of_succ p src n) in H ⊢ %;
    letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
    [>m_return_bind whd in match eval_step_flow; normalize nodelta
     whd in match (pblock ?);
     elim (goto … ge lbl st' ?)
     [ #st'' >m_return_bind %
     | #e %
     ]
    | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
      [ @fetch_fn
      | @point_of_pointer_of_point
      ]
    ]
  ]
]
qed.

definition eval_block_cont_pc :
  ∀globals.∀p : sem_params.∀ty.genv globals p →
  state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
  IO io_out io_in (bool × (state_pc p)) ≝
  λglobals,p,ty,ge,st,b,nxt.
  ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
  match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
  [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
        (pointer_of_point ? p (pc ? st) nxt) flow
  | FIN ⇒ λflow.λ_.
    ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
    return 〈true, st'〉
  ] flow nxt.

lemma eval_block_cont_in_code :
  ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
  fetch_function … ge (pc … st) = OK … fn →
  point_of_pointer ? p … (pc … st) = OK … src →
  All ? (never_calls … ge) (\fst B) →
  src ~❨B❩~> dst in joint_if_code … fn →
  repeat_eval_state_flag (|B|) g p ge st =
    eval_block_cont_pc g p ty ge st B dst.
#p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
* #mid * #l_in_code #s_in_code
change with (1 + |l|) in match (|?|);
>commutative_plus
>repeat_eval_state_flag_plus
change with (! x ← ? ; ?) in ⊢ (???%);
>m_bind_bind
>(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
>m_bind_bind
@m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
normalize nodelta
[ -s_in_code lapply dst -dst cases ty
  whd in match stmt_type_if; normalize nodelta
  #dst >m_return_bind
  [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
  normalize nodelta
  whd in match (pblock ?);
  elim (goto g p ge lbl st' ?) #x //
| %
| >m_return_bind normalize nodelta
  >repeat_eval_state_flag_one
  >m_bind_bind
  lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
  whd in match stmt_type_if; normalize nodelta
  #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
  whd in match eval_state_flag; normalize nodelta
  letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
  letin st_pc' ≝ (mk_state_pc ? st' pc')
  >(fetch_statement_eq … ?? s_in_code)
  [2,5: @point_of_pointer_of_point
  |3,6: @fetch_fn
  |*: >m_return_bind
    whd in match eval_statement; normalize nodelta
    @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
    whd in match succ_pc; normalize nodelta
    >point_of_pointer_of_point >m_return_bind
    >pointer_of_point_of_pointer [2: @refl |*:]
    [ >point_of_pointer_of_point >n_is_dst %
    | %
    ]
  ]
]
qed.
     cases dst [*] #z @eval_tunnel assumption
| cases dst [2: #z *]]
* #mid * #tunn [#H | * #n * #H #G ]
  elim (eval_tunnel … fetch_fn pc_pt tunn)
  #n
  letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
  #EQ1
  cut (point_of_pointer ? p … (pc … st') = OK … mid)
  [1,3: 
    whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
  cut (fetch_function p … ge (pc … st') = OK … fn)
  [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
    @pointer_of_point_block] #fetch_fn'
  [ %{(n + 1)} 
  >repeat_eval_state_plus >EQ1 >m_return_bind
  >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
  change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
  change with (! s ← ? ; ?) in match (eval_state ????);
  >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
  >m_bind_bind
  change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
  cases s *
  
  @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
  >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
  change with (! fn ← ? ; ?) in match (fetch_statement ?????);
  >m_bind_bind in ⊢ (??%?);
  change with (pointer_of_point ????) in match (pc ??);
  >point_of_pointer_of_point >m_return_bind
  >(fetch_function_from_block_eq ???? (pc … st))
  [2: @pointer_of_point_block ]
  >fetch_fn >m_return_bind >H2 >m_return_bind
  >m_bind_bind
  change with (! x ← ? ; ?) in ⊢ (???%);
  >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
  >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
  >H1 in ⊢ (??(????%?)?);
  whd in ⊢ (??(λ_.???%));
elim b
[ #st #dst #fetch_fn #prf #through
  #H elim (block_cont_to_tunnel … H) #dst'
  * #EQdst >EQdst >m_return_bind #G
  elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
  >EQ %
| 

 #dst #fetch_fn #prf #through
lapply prf -prf lapply fetch_fn -fetch_fn
lapply b -b lapply st -st
elim through [2: #hd #tl #IH]
[2:
  
#st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
normalize in ⊢(%→?);
[8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
[ * || * | * #lbl
 * #lbl * [*] #H1 #H2 [#H3]
  
let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
  (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
  match b with
  [ Skip ⇒
    match following with
    [ Some l ⇒ succ_pc p p 
*)