source: src/joint/semantics_blocks.ma @ 2244

include "joint/blocks.ma".
include "joint/Traces.ma".

(* 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
  ].*)

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.

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
  (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 (globals p) p (ev_genv p) st hd) ;
    repeat_eval_seq_no_pc p env 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 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 (globals p) 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.

let rec produce_trace_any_any
  (p : evaluation_params)
  (st : state_pc p) fd
  (src : code_point p)
  (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 →
  point_of_pointer p p (pc … st) = return src →
  if list_not_empty ? b then
    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
  else
    True →
  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) b st = return st' →
  trace_any_any (joint_abstract_status p) st
    (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
  match b
  return λx.?→?→?→?→?→?→?→?→?→?
  with
  [ nil ⇒
    λl,dst,st',fd_prf,src_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 (joint_abstract_status p) st
        (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
  | cons hd tl ⇒
    λl.
    match l return λx.?→?→?→?→?→?→?→?→? with
    [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
    | cons mid rest ⇒
      λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
      with
      [ OK st_mid ⇒ λEQ2.
        taa_step (joint_abstract_status p) st ?
          (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
          (produce_trace_any_any ?
            (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
            fd mid tl rest dst ???????)
      | Error _ ⇒ λEQ2.⊥
      ] (refl …)
    ]
  ].
  [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
    cases st in src_prf EQ1; -st #st #pc
    #src_prf normalize in ⊢ (%→?); #EQ1 destruct
    >(pointer_of_point_of_pointer … src_prf) %
  | elim in_code
  |12: lapply EQ1 whd in ⊢ (??%?→?);
    >EQ2 normalize #ABS destruct(ABS)
  |*:
    elim in_code
    * #nxt * #EQ3 #EQ4 #Hrest
    elim all_other
    #hd_other #tl_other
    [ whd whd in match eval_state; normalize nodelta
      >(fetch_statement_eq … fd_prf src_prf EQ3) >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 succ_pc; normalize nodelta
      >m_bind_bind >src_prf >m_return_bind >m_return_bind
      whd in match eval_step_flow; normalize nodelta
      whd in ⊢ (??%%); >EQ4
      >EQ2 %
    | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
      cases all_other #hd_other #_
      whd in match stmt_classifier; normalize nodelta
      @no_call_nor_label_other assumption
    | %* #H @H -H whd in ⊢ (??%?);
      cases tl in Hrest tl_other;
      [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
        lapply dst_prf
        whd in match (as_pc_of ??);
        whd in match fetch_statement; normalize nodelta
        whd in match point_of_pointer; normalize nodelta
        >point_of_offset_of_point
        >m_return_bind
        >fetch_function_from_block_eq
        [ >fd_prf
          >m_return_bind
          cases (stmt_at ????)
          [ #_ %
          | #stmt #H @H
          ]
        | %
        |
        ]
      | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
        #_ * #hd_other' #_
        >fetch_statement_eq try assumption
        [ @no_call_nor_label_uncosted assumption
        | whd in match (as_pc_of ??);
          whd in ⊢ (??%?);
          >point_of_offset_of_point %
        ]
      ]
    | change with (! x ← ?;?) in EQ1 : (??%?);
      >EQ2 in EQ1; #H @H
    | assumption
    | assumption
    | cases (list_not_empty ??) [ assumption | % ]
    | @point_of_pointer_of_point
    | <fd_prf @fetch_function_from_block_eq %
    ]
  ]
qed.