source: src/joint/SemanticUtils.ma @ 2446

Last change on this file since 2446 was 2443, checked in by tranquil, 7 years ago

changed joint's stack pointer and internal stack

File size: 6.3 KB
Line 
1include "joint/semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5
6record hw_register_env : Type[0] ≝
7  { reg_env : BitVectorTrie beval 6
8  ; other_bit : bebit
9  }.
10
11definition empty_hw_register_env: hw_register_env ≝
12  mk_hw_register_env (Stub …) BBundef.
13
14include alias "ASM/BitVectorTrie.ma".
15
16definition hwreg_retrieve: hw_register_env → Register → beval ≝
17 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
18
19definition 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
23definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
24λv,env.mk_hw_register_env (reg_env env) v.
25
26definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
27λenv.
28let spl ≝ hwreg_retrieve env RegisterSPL in
29let sph ≝ hwreg_retrieve env RegisterSPH in
30! ptr ← pointer_of_address 〈spl, sph〉 ;
31match ptype ptr return λx.ptype ptr = x → res xpointer with
32[ XData ⇒ λprf.return «ptr, prf»
33| _ ⇒ λ_.Error … [MSG BadPointer]
34] (refl …).
35
36definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
37λenv,sp.
38let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
39hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
40
41(*** Store/retrieve on pseudo-registers ***)
42include alias "common/Identifiers.ma".
43
44record reg_sp : Type[0] ≝
45{ reg_sp_env :> identifier_map RegisterTag beval
46; stackp : xpointer
47}.
48
49axiom BadRegister : String.
50
51definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
52
53definition reg_retrieve : register_env beval → register → res beval ≝
54 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
55
56definition reg_sp_store ≝ λreg,v,locals.
57! locals' ← reg_store reg v (reg_sp_env locals) ;
58return mk_reg_sp locals' (stackp locals).
59
60definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
61
62(*** Store/retrieve on hardware registers ***)
63
64definition init_hw_register_env: xpointer → hw_register_env ≝
65 λsp.hwreg_store_sp empty_hw_register_env sp.
66
67(******************************** GRAPHS **************************************)
68
69definition bitvector_from_pos :
70  ∀n.Pos → BitVector n ≝
71  λn,p.bitvector_of_Z n (Zpred (pos p)).
72
73definition pos_from_bitvector :
74  ∀n.BitVector n → Pos ≝
75  λn,v.
76  match Zsucc (Z_of_unsigned_bitvector n v)
77  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
78  with
79  [ OZ ⇒ λprf.⊥
80  | pos x ⇒ λ_. x
81  | neg x ⇒ λprf.⊥
82  ] (refl …).
83@hide_prf
84elim v in prf;
85[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
86
87lemma pos_pos_from_bitvector :
88  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
89#n #bv elim bv -n
90[ %
91| #n * #bv #IH [ % | @IH ]
92]
93qed.
94
95lemma bitvector_from_pos_from_bitvector :
96  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
97#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
98>Zpred_Zsucc //
99qed.
100
101lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
102  (∀q,r.
103    ppos m = natp_plus (natp_times q (ppos n)) r →
104    natp_lt r n →
105    P (〈q,r〉)) →
106  P (divide m n).
107#P #m #n #H
108lapply (refl … (divide m n))
109cases (divide ??) in ⊢ (???%→%);
110#q #r #EQ elim (divide_ok … EQ) -EQ @H
111qed.
112
113lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
114  p < q → \snd (divide p q) = ppos p.
115#p #q #H @divide_elim * [2: #quot ]
116* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
117@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
118[ @(transitive_le … (quot*q)) ] /2 by /
119qed.
120
121lemma pos_from_bitvector_from_pos :
122  ∀n,p.
123  p ≤ two_power_nat n →
124  pos_from_bitvector n (bitvector_from_pos n p) = p.
125#n #p #H
126cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
127[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
128>pos_pos_from_bitvector
129whd in match (bitvector_from_pos ??);
130>Z_of_unsigned_bitvector_of_Z
131cases p in H ⊢ %;
132[ #_ %
133|*: #p' #H
134  whd in match (Zpred ?);
135  whd in match (Z_two_power_nat ?);
136  whd in ⊢ (??(?%)?);
137  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
138  whd
139  <succ_pred_n try assumption % #ABS destruct(ABS)
140]
141qed.
142
143lemma pos_from_bitvector_max : ∀n,bv.
144  pos_from_bitvector n bv ≤ two_power_nat n.
145#n #bv
146change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
147>pos_pos_from_bitvector
148@Zlt_to_Zle
149@bv_Z_unsigned_max
150qed.
151
152definition graph_offset_of_label : label → option offset ≝
153  λl.let p ≝ word_of_identifier … l in
154  if leb p (two_power_nat offset_size) then
155    return mk_offset (bitvector_from_pos … p)
156  else
157    None ?.
158
159definition graph_label_of_offset: offset → label ≝
160 λo.an_identifier ? (pos_from_bitvector ? (offv o)).
161
162definition make_sem_graph_params :
163  ∀pars : unserialized_params.
164  ∀g_pars : ∀F.sem_unserialized_params pars F.
165  sem_params ≝
166  λpars,spars.
167  let g_pars ≝ mk_graph_params pars in
168  mk_sem_params
169    g_pars
170    (mk_more_sem_params
171      g_pars
172      (spars ?)
173      graph_offset_of_label
174      graph_label_of_offset
175      ??
176    ).
177whd in match graph_label_of_offset;
178whd in match graph_offset_of_label;
179whd in match word_of_identifier;
180normalize nodelta * #x
181@(leb_elim ? (two_power_nat ?)) normalize nodelta
182[ #_ >bitvector_from_pos_from_bitvector %
183| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
184| #H whd >(pos_from_bitvector_from_pos … H) %
185| #_ %
186]
187qed.
188
189(******************************** LINEAR **************************************)
190
191definition lin_offset_of_nat : ℕ → option offset ≝
192  λn.
193  if leb (S n) (2^offset_size) then
194    return mk_offset (bitvector_of_nat ? n)
195  else
196    None ?.
197
198definition lin_nat_of_offset : offset → ℕ ≝
199  λo.nat_of_bitvector ? (offv o).
200
201definition make_sem_lin_params :
202  ∀pars : unserialized_params.
203  (∀F.sem_unserialized_params pars F) →
204  sem_params ≝
205  λpars,spars.
206  let lin_pars ≝ mk_lin_params pars in
207  mk_sem_params
208    lin_pars
209    (mk_more_sem_params
210      lin_pars
211      (spars ?)
212      lin_offset_of_nat
213      lin_nat_of_offset
214      ??
215    ).
216[ * ] #x
217whd in match lin_offset_of_nat;
218whd in match lin_nat_of_offset;
219normalize nodelta
220@leb_elim normalize nodelta #H
221[ >bitvector_of_nat_inverse_nat_of_bitvector %
222| @⊥ cases H #H @H -H -H //
223| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
224| %
225]
226qed.
Note: See TracBrowser for help on using the repository browser.