source: src/joint/SemanticUtils.ma @ 2309

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
  ; carry_bit : bebit
  ; other_bit : bebit
  }.

definition empty_hw_register_env: hw_register_env ≝
  mk_hw_register_env (Stub …) BBundef 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))
  (carry_bit env) (other_bit env).

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

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


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

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

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

definition init_hw_register_env: xpointer → hw_register_env ≝
 λsp.
  let 〈dpl,dph〉 ≝
    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
    [ OK p ⇒ λ_.p
    | _ ⇒ λprf.⊥
    ] (refl …) in
  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
   hwreg_store RegisterDPL dpl env.
@hide_prf
normalize in prf; destruct(prf)
qed.

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

definition bitvector_from_pos :
  ∀n.Pos → BitVector n ≝
  λn,p.bitvector_of_Z n (Zpred (pos p)).

definition pos_from_bitvector :
  ∀n.BitVector n → Pos ≝
  λn,v.
  match Zsucc (Z_of_unsigned_bitvector n v)
  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
  with
  [ OZ ⇒ λprf.⊥
  | pos x ⇒ λ_. x
  | neg x ⇒ λprf.⊥
  ] (refl …).
@hide_prf
elim v in prf;
[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.

lemma pos_pos_from_bitvector :
  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
#n #bv elim bv -n
[ %
| #n * #bv #IH [ % | @IH ]
]
qed.

lemma bitvector_from_pos_from_bitvector :
  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
>Zpred_Zsucc //
qed.

lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
  (∀q,r.
    ppos m = natp_plus (natp_times q (ppos n)) r →
    natp_lt r n →
    P (〈q,r〉)) →
  P (divide m n).
#P #m #n #H
lapply (refl … (divide m n))
cases (divide ??) in ⊢ (???%→%);
#q #r #EQ elim (divide_ok … EQ) -EQ @H
qed.

lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
  p < q → \snd (divide p q) = ppos p.
#p #q #H @divide_elim * [2: #quot ]
* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
[ @(transitive_le … (quot*q)) ] /2 by /
qed.

lemma pos_from_bitvector_from_pos :
  ∀n,p.
  p ≤ two_power_nat n →
  pos_from_bitvector n (bitvector_from_pos n p) = p.
#n #p #H
cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
>pos_pos_from_bitvector
whd in match (bitvector_from_pos ??);
>Z_of_unsigned_bitvector_of_Z
cases p in H ⊢ %;
[ #_ %
|*: #p' #H
  whd in match (Zpred ?);
  whd in match (Z_two_power_nat ?);
  whd in ⊢ (??(?%)?);
  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
  whd
  <succ_pred_n try assumption % #ABS destruct(ABS)
]
qed.

lemma pos_from_bitvector_max : ∀n,bv.
  pos_from_bitvector n bv ≤ two_power_nat n.
#n #bv
change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
>pos_pos_from_bitvector
@Zlt_to_Zle
@bv_Z_unsigned_max
qed.

definition graph_offset_of_label : label → option offset ≝
  λl.let p ≝ word_of_identifier … l in
  if leb p (two_power_nat offset_size) then
    return mk_offset (bitvector_from_pos … p)
  else
    None ?.

definition graph_label_of_offset: offset → label ≝
 λo.an_identifier ? (pos_from_bitvector ? (offv o)).

definition make_sem_graph_params :
  ∀pars : graph_params.
  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      graph_offset_of_label
      graph_label_of_offset
      ??
    ).
whd in match graph_label_of_offset;
whd in match graph_offset_of_label;
whd in match word_of_identifier;
normalize nodelta * #x
@(leb_elim ? (two_power_nat ?)) normalize nodelta
[ #_ >bitvector_from_pos_from_bitvector %
| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
| #H whd >(pos_from_bitvector_from_pos … H) %
| #_ %
]
qed.

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

definition lin_offset_of_nat : ℕ → option offset ≝
  λn.
  if leb (S n) (2^offset_size) then
    return mk_offset (bitvector_of_nat ? n)
  else
    None ?.

definition lin_nat_of_offset : offset → ℕ ≝
  λo.nat_of_bitvector ? (offv o).


definition make_sem_lin_params :
  ∀pars : lin_params.
  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      lin_offset_of_nat
      lin_nat_of_offset
      ??
    ).
[ * ] #x
whd in match lin_offset_of_nat;
whd in match lin_nat_of_offset;
normalize nodelta
@leb_elim normalize nodelta #H
[ >bitvector_of_nat_inverse_nat_of_bitvector %
| @⊥ cases H #H @H -H -H //
| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
| %
]
qed.