1 | include "joint/semantics.ma". |
---|
2 | include alias "common/Identifiers.ma". |
---|
3 | include "utilities/hide.ma". |
---|
4 | include "ASM/BitVectorTrie.ma". |
---|
5 | |
---|
6 | record hw_register_env : Type[0] ≝ |
---|
7 | { reg_env : BitVectorTrie beval 6 |
---|
8 | ; other_bit : bebit |
---|
9 | }. |
---|
10 | |
---|
11 | definition empty_hw_register_env: hw_register_env ≝ |
---|
12 | mk_hw_register_env (Stub …) BBundef. |
---|
13 | |
---|
14 | include alias "ASM/BitVectorTrie.ma". |
---|
15 | |
---|
16 | definition hwreg_retrieve: hw_register_env → Register → beval ≝ |
---|
17 | λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef. |
---|
18 | |
---|
19 | definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ |
---|
20 | λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env)) |
---|
21 | (other_bit env). |
---|
22 | |
---|
23 | definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝ |
---|
24 | λv,env.mk_hw_register_env (reg_env env) v. |
---|
25 | |
---|
26 | definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝ |
---|
27 | λenv. |
---|
28 | let spl ≝ hwreg_retrieve env RegisterSPL in |
---|
29 | let sph ≝ hwreg_retrieve env RegisterSPH in |
---|
30 | ! ptr ← pointer_of_address 〈spl, sph〉 ; |
---|
31 | match ptype ptr return λx.ptype ptr = x → res xpointer with |
---|
32 | [ XData ⇒ λprf.return «ptr, prf» |
---|
33 | | _ ⇒ λ_.Error … [MSG BadPointer] |
---|
34 | ] (refl …). |
---|
35 | |
---|
36 | definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝ |
---|
37 | λenv,sp. |
---|
38 | let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in |
---|
39 | hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env). |
---|
40 | |
---|
41 | (*** Store/retrieve on pseudo-registers ***) |
---|
42 | include alias "common/Identifiers.ma". |
---|
43 | |
---|
44 | record reg_sp : Type[0] ≝ |
---|
45 | { reg_sp_env :> identifier_map RegisterTag beval |
---|
46 | ; stackp : xpointer |
---|
47 | }. |
---|
48 | |
---|
49 | axiom BadRegister : String. |
---|
50 | |
---|
51 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
52 | |
---|
53 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
54 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
55 | |
---|
56 | definition reg_sp_store ≝ λreg,v,locals. |
---|
57 | ! locals' ← reg_store reg v (reg_sp_env locals) ; |
---|
58 | return mk_reg_sp locals' (stackp locals). |
---|
59 | |
---|
60 | definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals. |
---|
61 | |
---|
62 | (*** Store/retrieve on hardware registers ***) |
---|
63 | |
---|
64 | definition init_hw_register_env: xpointer → hw_register_env ≝ |
---|
65 | λsp.hwreg_store_sp empty_hw_register_env sp. |
---|
66 | |
---|
67 | (******************************** GRAPHS **************************************) |
---|
68 | |
---|
69 | definition make_sem_graph_params : |
---|
70 | ∀pars : unserialized_params. |
---|
71 | ∀g_pars : ∀F.sem_unserialized_params pars F. |
---|
72 | sem_params ≝ |
---|
73 | λpars,spars. |
---|
74 | let g_pars ≝ mk_graph_params pars in |
---|
75 | mk_sem_params |
---|
76 | g_pars |
---|
77 | (mk_more_sem_params |
---|
78 | g_pars |
---|
79 | (spars ?) |
---|
80 | (word_of_identifier ?) |
---|
81 | (an_identifier ?) |
---|
82 | ? (refl …) |
---|
83 | ). |
---|
84 | * #p % qed. |
---|
85 | |
---|
86 | (******************************** LINEAR **************************************) |
---|
87 | |
---|
88 | lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p. |
---|
89 | @pos_elim [%] |
---|
90 | #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. |
---|
91 | |
---|
92 | |
---|
93 | definition make_sem_lin_params : |
---|
94 | ∀pars : unserialized_params. |
---|
95 | (∀F.sem_unserialized_params pars F) → |
---|
96 | sem_params ≝ |
---|
97 | λpars,spars. |
---|
98 | let lin_pars ≝ mk_lin_params pars in |
---|
99 | mk_sem_params |
---|
100 | lin_pars |
---|
101 | (mk_more_sem_params |
---|
102 | lin_pars |
---|
103 | (spars ?) |
---|
104 | succ_pos_of_nat |
---|
105 | (λp.pred (nat_of_pos p)) |
---|
106 | ?? |
---|
107 | ). |
---|
108 | [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos |
---|
109 | | #n >nat_succ_pos % |
---|
110 | ] qed. |
---|