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

(* WARNING: all the following breaks apart if statements are allowed to depend
   on flow. Execution of blocks does not update flow information in the state
   (e.g. the program counter) until the end *)

definition goto_no_seq : ∀g.∀p:sem_params.genv g p → label →
  state p → Z → res (state_pc p) ≝ λg,p,ge,lbl,st,id.
      ! newpc ← pointer_of_label ? p … ge
        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) lbl ;
      return mk_state_pc … st newpc. % qed.

lemma goto_no_seq_to_normal : ∀p : sem_params.∀g,ge.∀st : state_pc p.∀id,lbl.
  block_id (pblock (pc p st)) = id →
  goto_no_seq g p ge lbl st id = goto g p ge lbl st.
#p #g #ge * #st ** #typ * #r #id
#H inversion H [1,3: #r'] #id'
#EQ1 #EQ2 #EQ3 #o #EQ4 #id'' #lbl #EQ5 destruct
whd in match goto_no_seq;
whd in match goto; normalize nodelta //
qed.

(* executes a block of instructions, until its end or before if a
   function call or a redirection is encountered. If executed until end,
   or is a non-tail call is encountered, the next program counter must be
   provided *)
let rec eval_block_cont globals (p:sem_params) (ge : genv globals p)
  (st : state p) id (b : block_cont p globals) (dst : option cpointer) on b :
    IO io_out io_in (trace×(state_pc p)) ≝
  match b with
  [ Skip ⇒
    ! nxt ← opt_to_res … (msg SuccessorNotProvided) dst ;
    return 〈E0, mk_state_pc ? st nxt〉
  | Final s ⇒
    ! 〈flow, tr, st'〉 ← eval_statement_no_seq … ge st s;
    ! st ← eval_stmt_flow_no_seq … ge st' id flow;
    return 〈tr, st〉
  | Cons hd tl ⇒
    ! 〈flow, tr1, st'〉 ← eval_step ?? ge st hd ;
    match flow with
    [ Proceed ⇒
      ! 〈tr2, st〉 ← eval_block_cont globals p ge st id tl dst ;
      return 〈tr1 ⧺ tr2, st〉
    | Init id fn args dest ⇒
      ! ra ← opt_to_res … (msg SuccessorNotProvided) dst ;
      let st' ≝ set_frms … (save_frame … ra dest st) st in
      ! st ← do_call ?? ge st' id fn args ;
      return 〈tr1, st〉
    | Redirect l ⇒
      ! st ← goto_no_seq ? p … ge l st id ;
      return 〈tr1, st〉
    ]
  ].
  
lemma Eapp_E0 : ∀tr1 : trace.tr1 ⧺ E0 = tr1 ≝ append_nil ….

(* just like repeat, but without the full_exec infrastructure *)
let rec repeat_eval_state n globals (p:sem_params) (ge : genv globals p)
  (st : state_pc p) on n :
    IO io_out io_in (trace×(state_pc p)) ≝
match n with
[ O ⇒ return 〈E0, st〉
| S k ⇒
  ! 〈tr1, st〉 ← eval_state globals p ge st ;
  ! 〈tr2, st〉 ← repeat_eval_state k globals p ge st ;
  return 〈tr1 ⧺ tr2, st〉
].

lemma repeat_eval_state_plus : ∀n1,n2,globals, p, ge, st.
  repeat_eval_state (n1 + n2) globals p ge st =
  ! 〈tr1, st〉 ← repeat_eval_state n1 globals p ge st ;
  ! 〈tr2, st〉 ← repeat_eval_state n2 globals p ge st ;
  return 〈tr1 ⧺ tr2, st〉.
#n1 elim n1 -n1 [| #n1 #IH]
#n2 #globals #p #ge #st
[ >m_return_bind change with n2 in match (0 + n2);
  change with (! x ← ? ; ?) in ⊢ (???%);
  <(m_bind_return … (repeat_eval_state ?????)) in ⊢ (??%?);
  @m_bind_ext_eq * //
| change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
  change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S n1) ????);
  >m_bind_bind in ⊢ (???%);
  @m_bind_ext_eq * #tr1 #st1
  >IH >m_bind_bind in ⊢ (??%?); >m_bind_bind in ⊢ (???%);
  @m_bind_ext_eq * #tr2 #st2 >m_return_bind
  >m_bind_bind @m_bind_ext_eq * #tr3 #st3 >m_return_bind >Eapp_assoc %
]
qed.

lemma repeat_eval_state_one : ∀globals, p, ge, st.
  repeat_eval_state 1 globals p ge st = eval_state globals p ge st.
#globals #p #ge #st
change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
<(m_bind_return … (eval_state ????)) in ⊢ (???%);
@m_bind_ext_eq * #tr1 #st1 >m_return_bind >Eapp_E0 %
qed.

lemma If_true : ∀A.∀b : bool.∀f : b → A.∀g.∀prf' : bool_to_Prop b.If b then with prf do f prf else with prf do g prf = f prf'.
#A * #f #g * normalize % 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 g p ge st =
    OK … 〈E0, 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 ????);
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 ⊢ (??%?);  >m_return_bind
change with (! st ← ? ; ?) in ⊢ (??%?);
whd in match eval_stmt_flow; normalize nodelta
change with (! ptr ← ? ; ?) in match (goto ?????);
whd in match pointer_of_label; normalize nodelta 
>fetch_fn in ⊢ (??%?); >m_return_bind
>EQ2 in ⊢ (??%?); >m_return_bind %
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 =
    OK … 〈E0, 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 (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
>EQ  >m_return_bind %
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 =
    OK … 〈E0, 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 (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
>EQ  >m_return_bind %
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_block_cont_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 →
  src ~❨B❩~> dst in joint_if_code … fn →
  ∃n.repeat_eval_state n g p ge st =
    eval_block_cont g p ge st (block_id (pblock (pc … st))) B (! x ← dst; return pointer_of_point … p (pc … st) x).
#p #g #ge #st #fn #src #B lapply src -src
lapply st -st elim B [|#s|#s #B' #IH]
#st #src #dst #fetch_fn #pc_pt
[ 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