include "joint/semantics.ma".
include alias "common/Identifiers.ma".
include "utilities/hide.ma".
include "ASM/BitVectorTrie.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
}.

axiom BadRegister : String.

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 **************************************)

definition make_sem_graph_params :
  ∀pars : unserialized_params.
  ∀g_pars : ∀F.sem_unserialized_params pars F.
  sem_params ≝
  λpars,spars.
  let g_pars ≝ mk_graph_params pars in
  mk_sem_params
    g_pars
    (mk_more_sem_params
      g_pars
      (spars ?)
      (word_of_identifier ?)
      (an_identifier ?)
      ? (refl …)
    ).
* #p % qed.

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


definition make_sem_lin_params :
  ∀pars : unserialized_params.
  (∀F.sem_unserialized_params pars F) →
  sem_params ≝
  λpars,spars.
  let lin_pars ≝ mk_lin_params pars in
  mk_sem_params
    lin_pars
    (mk_more_sem_params
      lin_pars
      (spars ?)
      succ_pos_of_nat
      (λp.pred (nat_of_pos p))
      ??
    ).
[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
| #n >nat_succ_pos %
] qed.