source: src/joint/Traces.ma @ 2529

include "joint/semantics.ma".
include "common/StructuredTraces.ma".

record evaluation_params : Type[1] ≝
 { globals: list ident
 ; sparams:> sem_params
 ; exit: program_counter
 ; ev_genv: genv sparams globals
(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
 }.
 


record prog_params : Type[1] ≝
 { prog_spars : sem_params
 ; prog : joint_program prog_spars
 ; stack_sizes : ident → option ℕ
(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
 }.

lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
#A #B #f #P #l elim l -l [*]
#hd #tl #IH *
[ #Phd %1{Phd}
| #Ptl %2{(IH Ptl)}
]
qed.

lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
#A #P #l elim l -l [*] #hd #tl #IH *
[ #Phd %{hd} %{Phd} %1 %
| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
]
qed.

lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
[ #EQ >EQ #H %1{H}
| #Intl #Px %2{(IH … Intl Px)}
]
qed.

lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed. 

definition make_global : prog_params → evaluation_params
≝
λpars.
(* Invariant: a -1 block is unused in common/Globalenvs *)
let b ≝ mk_block Code (-1) in
let ptr ≝ mk_program_counter «b, refl …» one in
let p ≝ prog pars in
mk_evaluation_params
  (prog_var_names … p)
  (prog_spars pars)
  ptr
  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
 (* (prog_io pars) *).
#s #H
elim (find_symbol_exists … p s ?)
[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
@Exists_append_r
@(Exists_mp … H) //
qed.

coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
≝ make_global on _p : prog_params to evaluation_params.

axiom BadMain : String.

definition make_initial_state :
 ∀pars: prog_params.res (state_pc pars) ≝
λpars.let p ≝ prog pars in
  let sem_globals : evaluation_params ≝ pars in
  let ge ≝ ev_genv sem_globals in
  let m ≝ alloc_mem … p in
  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
  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)),
     pi2 … spb» in
(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
  let main ≝ prog_main … p in
  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
  (* use exit sem_globals as ra and call_dest_for_main as dest *)
  let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
  ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc 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? *)
  ].

definition joint_classify_seq :
  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
  λp,st,stmt.
  match stmt with
  [ CALL f args dest ⇒
    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
      ]
    | Error _ ⇒ cl_other
    ]
  | _ ⇒ cl_other
  ].

definition joint_classify_step :
  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
  λp,st,stmt.
  match stmt with
  [ step_seq s ⇒ joint_classify_seq p st s
  | COND _ _ ⇒ cl_jump
  ].

definition joint_classify_final :
  ∀p : evaluation_params.joint_fin_step p → status_class ≝
  λp,stmt.
  match stmt with
  [ GOTO _ ⇒ cl_other
  | RETURN ⇒ cl_return
  | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
  ].

definition joint_classify :
  ∀p : evaluation_params.state_pc p → status_class ≝
  λp,st.
  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
    ]
  | Error _ ⇒ cl_other
  ].

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 →
  ∃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 … (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' %
    ]
  ]
]
#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
qed.

definition joint_after_ret : ∀p:evaluation_params.
  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
λp,s1,s2.
match fetch_statement … (ev_genv p) (pc … s1) with
[ OK x ⇒
  match \snd x with
  [ sequential s next ⇒
    pc … s2 = succ_pc p (pc … s1) next
  | _ ⇒ False (* never happens *)
  ]
| _ ⇒ False (* never happens *)
].

definition joint_call_ident : ∀p:evaluation_params.
  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
(* this is a definition without a dummy ident :
λp,st.
match ?
return λx.
  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
  match s with
  [ sequential s next ⇒
    match s with
    [ step_seq s ⇒
      match s with
      [ CALL f' args dest ⇒
        function_of_call … (ev_genv p) st f'
      | _ ⇒ Error … [ ]
      ]
    | _ ⇒ Error … [ ]
    ]
  | _ ⇒ Error … [ ]
  ] = x → ? with
[ OK v ⇒ λ_.v
| Error e ⇒ λABS.⊥
] (refl …).
@hide_prf
elim (joint_classify_call … (pi2 … st))
#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
lapply ABS -ABS
>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
qed. *)
(* with a dummy ident (which is never used as seen above in the commented script)
   I think handling of the function is easier *)
λp,st.
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
  [ sequential s next ⇒
    match s with
    [ step_seq s ⇒
      match s with
      [ CALL f' args dest ⇒
        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
        ]
      | _ ⇒ dummy
      ]
    | _ ⇒ dummy
    ]
  | _ ⇒ dummy
  ]
| _ ⇒ dummy
].

definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
[ #EQ destruct % #H %
| * #NEQ % #ABS destruct elim (NEQ ?) %
]
qed.

(*
let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
  match c with
  [ Value x ⇒ OK … x
  | Interact o f ⇒
    ! i ← env o ;
    io_evaluate O I X env (f i)
  | Wrong e ⇒ Error … e
  ].
*)

definition cost_label_of_stmt :
  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
  λp,s.match s with
  [ sequential s _ ⇒
    match s with
    [ step_seq s ⇒
      match s with
      [ COST_LABEL lbl ⇒ Some ? lbl
      | _ ⇒ None ?
      ]
    | _ ⇒ None ?
    ]
  | _ ⇒ 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 :
 ∀p : evaluation_params.
 abstract_status ≝
 λp.
 mk_abstract_status
   (* as_status ≝ *) (state_pc p)
   (* as_execute ≝ *)
    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
   (* as_pc ≝ *) pcDeq
   (* as_pc_of ≝ *) (pc …)
   (* as_classify ≝ *) (joint_classify p)
   (* as_label_of_pc ≝ *)
    (λpc.
      match fetch_statement … (ev_genv p) pc with
      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
      | _ ⇒ None ?
      ])
   (* as_after_return ≝ *) (joint_after_ret p)
   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
   (* as_call_ident ≝ *) (joint_call_ident p).