include "joint/semantics_paolo.ma". include alias "common/Identifiers.ma". include "utilities/hide.ma". (*** Store/retrieve on pseudo-registers ***) 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) 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 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.