1 | include "joint/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 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
50 | |
---|
51 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
52 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
53 | |
---|
54 | definition reg_sp_store ≝ λreg,v,locals. |
---|
55 | ! locals' ← reg_store reg v (reg_sp_env locals) ; |
---|
56 | return mk_reg_sp locals' (stackp locals). |
---|
57 | |
---|
58 | definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals. |
---|
59 | |
---|
60 | (*** Store/retrieve on hardware registers ***) |
---|
61 | |
---|
62 | definition init_hw_register_env: xpointer → hw_register_env ≝ |
---|
63 | λsp.hwreg_store_sp empty_hw_register_env sp. |
---|
64 | |
---|
65 | (******************************** GRAPHS **************************************) |
---|
66 | |
---|
67 | definition make_sem_graph_params : |
---|
68 | ∀pars : unserialized_params. |
---|
69 | ∀g_pars : ∀F.sem_unserialized_params pars F. |
---|
70 | sem_params ≝ |
---|
71 | λpars,spars. |
---|
72 | let g_pars ≝ mk_graph_params pars in |
---|
73 | mk_sem_params |
---|
74 | g_pars |
---|
75 | (spars ?) |
---|
76 | (word_of_identifier ?) |
---|
77 | (an_identifier ?) |
---|
78 | ? (refl …). |
---|
79 | * #p % qed. |
---|
80 | |
---|
81 | (******************************** LINEAR **************************************) |
---|
82 | |
---|
83 | lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p. |
---|
84 | @pos_elim [%] |
---|
85 | #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. |
---|
86 | |
---|
87 | definition make_sem_lin_params : |
---|
88 | ∀pars : unserialized_params. |
---|
89 | (∀F.sem_unserialized_params pars F) → |
---|
90 | sem_params ≝ |
---|
91 | λpars,spars. |
---|
92 | let lin_pars ≝ mk_lin_params pars in |
---|
93 | mk_sem_params |
---|
94 | lin_pars |
---|
95 | (spars ?) |
---|
96 | succ_pos_of_nat |
---|
97 | (λp.pred (nat_of_pos p)) |
---|
98 | ??. |
---|
99 | [ #n >nat_succ_pos % |
---|
100 | | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos |
---|
101 | ] qed. |
---|
102 | |
---|
103 | |
---|
104 | |
---|
105 | |
---|
106 | lemma fetch_statement_eq : ∀p:sem_params.∀g. |
---|
107 | ∀ge : genv_t (joint_function p g).∀ptr : program_counter. |
---|
108 | ∀i,fn,s. |
---|
109 | fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → |
---|
110 | let pt ≝ point_of_pc … ptr in |
---|
111 | stmt_at … (joint_if_code … fn) pt = Some ? s → |
---|
112 | fetch_statement … ge ptr = OK … 〈i, fn, s〉. |
---|
113 | #p #g #ge #ptr #i #f #s #EQ1 #EQ2 |
---|
114 | whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind |
---|
115 | >EQ2 % |
---|
116 | qed. |
---|
117 | |
---|
118 | lemma fetch_statement_inv : ∀p:sem_params.∀g. |
---|
119 | ∀ge : genv_t (joint_function p g).∀ptr : program_counter. |
---|
120 | ∀i,fn,s. |
---|
121 | fetch_statement … ge ptr = OK … 〈i, fn, s〉 → |
---|
122 | fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧ |
---|
123 | let pt ≝ point_of_pc p ptr in |
---|
124 | stmt_at … (joint_if_code … fn) pt = Some ? s. |
---|
125 | #p #g #ge #ptr #i #fn #s #H |
---|
126 | elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H |
---|
127 | elim (bind_inversion ????? H) #s' * #H |
---|
128 | lapply (opt_eq_from_res ???? H) -H #EQ2 |
---|
129 | whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} |
---|
130 | qed. |
---|
131 | |
---|