source: src/joint/semanticsUtils.ma @ 2681

include "joint/joint_semantics.ma".
include alias "common/Identifiers.ma".
include "utilities/hide.ma".
include "ASM/BitVectorTrie.ma".
include "joint/TranslateUtils.ma".

record hw_register_env : Type[0] ≝
  { reg_env : BitVectorTrie beval 6
  ; other_bit : bebit
  }.

definition empty_hw_register_env: hw_register_env ≝
  mk_hw_register_env (Stub …) BBundef.

include alias "ASM/BitVectorTrie.ma".

definition hwreg_retrieve: hw_register_env → Register → beval ≝
 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.

definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
  (other_bit env).

definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
λv,env.mk_hw_register_env (reg_env env) v.

definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
λenv.
let spl ≝ hwreg_retrieve env RegisterSPL in
let sph ≝ hwreg_retrieve env RegisterSPH in
! ptr ← pointer_of_address 〈spl, sph〉 ;
match ptype ptr return λx.ptype ptr = x → res xpointer with
[ XData ⇒ λprf.return «ptr, prf»
| _ ⇒ λ_.Error … [MSG BadPointer]
] (refl …).

definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
λenv,sp.
let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).

(*** Store/retrieve on pseudo-registers ***)
include alias "common/Identifiers.ma".

record reg_sp : Type[0] ≝
{ reg_sp_env :> identifier_map RegisterTag beval
; stackp : xpointer
}.

definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.

definition reg_retrieve : register_env beval → register → res beval ≝
 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).

definition reg_sp_store ≝ λreg,v,locals.
! locals' ← reg_store reg v (reg_sp_env locals) ;
return mk_reg_sp locals' (stackp locals).

definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.

(*** Store/retrieve on hardware registers ***)

definition init_hw_register_env: xpointer → hw_register_env ≝
 λsp.hwreg_store_sp empty_hw_register_env sp.

(******************************** GRAPHS **************************************)

record sem_graph_params : Type[1] ≝
{ sgp_pars : unserialized_params
; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
}.

definition sem_graph_params_to_graph_params :
  ∀pars : sem_graph_params.graph_params ≝
  λpars.mk_graph_params (sgp_pars pars).

coercion graph_params_from_sem_graph_params nocomposites :
  ∀pars : sem_graph_params.
  graph_params ≝ sem_graph_params_to_graph_params
  on _pars : sem_graph_params to graph_params.

definition sem_graph_params_to_sem_params :
  ∀pars : sem_graph_params.
  sem_params ≝
  λpars.
  mk_sem_params
    (pars : graph_params)
    (sgp_sup pars ?)
    (word_of_identifier ?)
    (an_identifier ?)
    ? (refl …).
* #p % qed.

coercion sem_params_from_sem_graph_params :
  ∀pars : sem_graph_params.
  sem_params ≝ sem_graph_params_to_sem_params
  on _pars : sem_graph_params to sem_params.


(******************************** LINEAR **************************************)

lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
@pos_elim [%]
#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.

record sem_lin_params : Type[1] ≝
{ slp_pars : unserialized_params
; slp_sup : ∀F.sem_unserialized_params slp_pars F
}.

definition sem_lin_params_to_lin_params :
  ∀pars : sem_lin_params.lin_params ≝
  λpars.mk_lin_params (slp_pars pars).

coercion lin_params_from_sem_lin_params nocomposites :
  ∀pars : sem_lin_params.
  lin_params ≝ sem_lin_params_to_lin_params
  on _pars : sem_lin_params to lin_params.

definition sem_lin_params_to_sem_params :
  ∀pars : sem_lin_params.
  sem_params ≝
  λpars.
  mk_sem_params
    (pars : lin_params)
    (slp_sup pars ?)
    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.

coercion sem_params_from_sem_lin_params :
  ∀pars : sem_lin_params.
  sem_params ≝ sem_lin_params_to_sem_params
  on _pars : sem_lin_params to sem_params.


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.

axiom b_graph_transform_program_props :
 ∀src,dst:sem_graph_params.
 ∀data : ∀globals.joint_closed_internal_function src globals →
  bind_new register (b_graph_translate_data src dst globals).
 ∀prog_in : joint_program src.
 let prog_out ≝ b_graph_transform_program … data prog_in in
 let src_genv ≝ globalenv_noinit ? prog_in in
 let dst_genv ≝ globalenv_noinit ? prog_out in
 ∃init_regs : ident → list register.
 ∃f_lbls : ident → label → option (list label).
 ∃f_regs : ident → label → option (list register).
 ∀bl,id,def_in.
 fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
 ∃init_data,def_out.
 fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
 bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
 b_graph_translate_props src dst ? init_data (init_regs id)
    def_in def_out (f_lbls id) (f_regs id).