Changeset 2208 for src/joint/semanticsUtils_paolo.ma
- Timestamp:
- Jul 18, 2012, 1:26:43 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semanticsUtils_paolo.ma
r2200 r2208 14 14 (*** Store/retrieve on hardware registers ***) 15 15 16 definition init_hw_register_env: address → hw_register_env ≝ 17 λaddr. 18 let 〈dpl,dph〉 ≝ addr in 16 definition init_hw_register_env: xpointer → hw_register_env ≝ 17 λsp. 18 let 〈dpl,dph〉 ≝ 19 match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with 20 [ OK p ⇒ λ_.p 21 | _ ⇒ λprf.⊥ 22 ] (refl …) in 19 23 let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in 20 24 hwreg_store RegisterDPL dpl env. 25 @hide_prf 26 normalize in prf; destruct(prf) 27 qed. 21 28 22 29 (******************************** GRAPHS **************************************)
Note: See TracChangeset
for help on using the changeset viewer.