1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "ASM/Assembly.ma". |
---|
16 | include "ASM/Interpret.ma". |
---|
17 | include "ASM/StatusProofs.ma". |
---|
18 | include alias "arithmetics/nat.ma". |
---|
19 | include "ASM/AssemblyProof.ma". |
---|
20 | |
---|
21 | lemma set_program_counter_status_of_pseudo_status: |
---|
22 | ∀M. |
---|
23 | ∀cm. |
---|
24 | ∀ps. |
---|
25 | ∀sigma. |
---|
26 | ∀policy. |
---|
27 | ∀new_ppc. |
---|
28 | set_program_counter (BitVectorTrie Byte 16) |
---|
29 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
30 | (status_of_pseudo_status M cm ps sigma policy) |
---|
31 | (sigma new_ppc) = |
---|
32 | status_of_pseudo_status M cm (set_program_counter … cm ps new_ppc) sigma policy. |
---|
33 | // |
---|
34 | qed. |
---|
35 | |
---|
36 | lemma set_p1_latch_status_of_pseudo_status: |
---|
37 | ∀M. |
---|
38 | ∀code_memory. |
---|
39 | ∀sigma. |
---|
40 | ∀policy. |
---|
41 | ∀s. |
---|
42 | ∀v. |
---|
43 | set_p1_latch (BitVectorTrie Byte 16) |
---|
44 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
45 | (status_of_pseudo_status M code_memory s sigma policy) v = |
---|
46 | status_of_pseudo_status M code_memory |
---|
47 | (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
48 | // |
---|
49 | qed. |
---|
50 | |
---|
51 | lemma set_p3_latch_status_of_pseudo_status: |
---|
52 | ∀M. |
---|
53 | ∀code_memory. |
---|
54 | ∀sigma. |
---|
55 | ∀policy. |
---|
56 | ∀s. |
---|
57 | ∀v. |
---|
58 | set_p3_latch (BitVectorTrie Byte 16) |
---|
59 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
60 | (status_of_pseudo_status M code_memory s sigma policy) v = |
---|
61 | status_of_pseudo_status M code_memory |
---|
62 | (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
63 | // |
---|
64 | qed. |
---|
65 | |
---|
66 | definition map_acc_a_using_internal_pseudo_address_map: |
---|
67 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝ |
---|
68 | λM, sigma, v. |
---|
69 | match \snd M with |
---|
70 | [ data ⇒ v |
---|
71 | | address upper_lower word ⇒ |
---|
72 | let mapped ≝ sigma word in |
---|
73 | let 〈high, low〉 ≝ vsplit bool 8 8 mapped in |
---|
74 | if eq_upper_lower upper_lower upper then |
---|
75 | high |
---|
76 | else |
---|
77 | low |
---|
78 | ]. |
---|
79 | |
---|
80 | (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *) |
---|
81 | definition map_internal_ram_address_using_pseudo_address_map: |
---|
82 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ |
---|
83 | λM: internal_pseudo_address_map. |
---|
84 | λsigma: Word → Word. |
---|
85 | λaddress: Byte. |
---|
86 | λvalue: Byte. |
---|
87 | match assoc_list_lookup ?? address (eq_bv …) (\fst M) with |
---|
88 | [ None ⇒ value |
---|
89 | | Some upper_lower_word ⇒ |
---|
90 | let 〈upper_lower, word〉 ≝ upper_lower_word in |
---|
91 | let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in |
---|
92 | if eq_upper_lower upper_lower upper then |
---|
93 | high |
---|
94 | else |
---|
95 | low |
---|
96 | ]. |
---|
97 | |
---|
98 | definition map_address_using_internal_pseudo_address_map: |
---|
99 | ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝ |
---|
100 | λM, sigma, sfr, v. |
---|
101 | match sfr with |
---|
102 | [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v |
---|
103 | | _ ⇒ v |
---|
104 | ]. |
---|
105 | |
---|
106 | lemma set_index_set_index_overwrite: |
---|
107 | ∀A: Type[0]. |
---|
108 | ∀n: nat. |
---|
109 | ∀v: Vector A n. |
---|
110 | ∀index: nat. |
---|
111 | ∀e, e': A. |
---|
112 | ∀proof. |
---|
113 | ∀proof'. |
---|
114 | set_index A n v index e proof = |
---|
115 | set_index A n (set_index A n v index e' proof') index e proof. |
---|
116 | #A #n #v elim v normalize |
---|
117 | [1: |
---|
118 | #index #e #e' #absurd cases (lt_to_not_zero … absurd) |
---|
119 | |2: |
---|
120 | #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof' |
---|
121 | normalize // |
---|
122 | ] |
---|
123 | qed. |
---|
124 | |
---|
125 | lemma set_index_set_index_commutation: |
---|
126 | ∀A: Type[0]. |
---|
127 | ∀n: nat. |
---|
128 | ∀v: Vector A n. |
---|
129 | ∀m, o: nat. |
---|
130 | ∀m_lt_proof: m < n. |
---|
131 | ∀o_lt_proof: o < n. |
---|
132 | ∀e, f: A. |
---|
133 | m ≠ o → |
---|
134 | set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof = |
---|
135 | set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof. |
---|
136 | #A #n #v elim v |
---|
137 | [1: |
---|
138 | #m #o #m_lt_proof |
---|
139 | normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof) |
---|
140 | |2: |
---|
141 | #n' #hd #tl #inductive_hypothesis |
---|
142 | #m #o |
---|
143 | cases m cases o |
---|
144 | [1: |
---|
145 | #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant |
---|
146 | @relevant % |
---|
147 | |2,3: |
---|
148 | #o' normalize // |
---|
149 | |4: |
---|
150 | #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm |
---|
151 | normalize @eq_f @inductive_hypothesis @nmk #relevant |
---|
152 | >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) % |
---|
153 | ] |
---|
154 | ] |
---|
155 | qed. |
---|
156 | |
---|
157 | (* XXX: move elsewhere *) |
---|
158 | lemma get_index_v_set_index_miss: |
---|
159 | ∀a: Type[0]. |
---|
160 | ∀n: nat. |
---|
161 | ∀v: Vector a n. |
---|
162 | ∀i, j: nat. |
---|
163 | ∀e: a. |
---|
164 | ∀i_proof: i < n. |
---|
165 | ∀j_proof: j < n. |
---|
166 | i ≠ j → |
---|
167 | get_index_v a n (set_index a n v i e i_proof) j j_proof = |
---|
168 | get_index_v a n v j j_proof. |
---|
169 | #a #n #v elim v |
---|
170 | [1: |
---|
171 | #i #j #e #i_proof |
---|
172 | cases (lt_to_not_zero … i_proof) |
---|
173 | |2: |
---|
174 | #n' #hd #tl #inductive_hypothesis #i #j |
---|
175 | cases i cases j |
---|
176 | [1: |
---|
177 | #e #i_proof #j_proof #neq_assm |
---|
178 | cases (absurd ? (refl … 0) neq_assm) |
---|
179 | |2,3: |
---|
180 | #i' #e #i_proof #j_proof #_ % |
---|
181 | |4: |
---|
182 | #i' #j' #e #i_proof #j_proof #neq_assm |
---|
183 | @inductive_hypothesis @nmk #eq_assm |
---|
184 | >eq_assm in neq_assm; #neq_assm |
---|
185 | cases (absurd ? (refl ??) neq_assm) |
---|
186 | ] |
---|
187 | ] |
---|
188 | qed. |
---|
189 | |
---|
190 | lemma set_index_status_of_pseudo_status: |
---|
191 | ∀M, code_memory, sigma, policy, s, sfr, v, v'. |
---|
192 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
193 | (set_index Byte 19 |
---|
194 | (special_function_registers_8051 (BitVectorTrie Byte 16) |
---|
195 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
196 | (status_of_pseudo_status M code_memory s sigma policy)) |
---|
197 | (sfr_8051_index sfr) v' (sfr8051_index_19 sfr) |
---|
198 | =sfr_8051_of_pseudo_sfr_8051 M |
---|
199 | (special_function_registers_8051 pseudo_assembly_program code_memory |
---|
200 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma). |
---|
201 | #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm |
---|
202 | whd in match status_of_pseudo_status; normalize nodelta |
---|
203 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
204 | inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta |
---|
205 | [1: |
---|
206 | <sfr_neq_acc_a_assm cases sfr |
---|
207 | [18: |
---|
208 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
209 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
210 | >sndM_refl % |
---|
211 | ] |
---|
212 | % |
---|
213 | |2: |
---|
214 | @pair_elim #high #low #high_low_refl normalize nodelta |
---|
215 | inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta |
---|
216 | <sfr_neq_acc_a_assm cases sfr |
---|
217 | [18,37: |
---|
218 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
219 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
220 | >sndM_refl normalize nodelta >high_low_refl normalize nodelta |
---|
221 | >eq_upper_lower_refl normalize nodelta |
---|
222 | whd in match (set_8051_sfr ?????); |
---|
223 | [1: |
---|
224 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
225 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
226 | |2: |
---|
227 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
228 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
229 | ] |
---|
230 | ] |
---|
231 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
232 | whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize |
---|
233 | @nmk #absurd destruct(absurd) |
---|
234 | ] |
---|
235 | qed. |
---|
236 | |
---|
237 | lemma get_index_v_status_of_pseudo_status: |
---|
238 | ∀M, code_memory, sigma, policy, s, sfr. |
---|
239 | (get_index_v Byte 19 |
---|
240 | (special_function_registers_8051 (BitVectorTrie Byte 16) |
---|
241 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
242 | (status_of_pseudo_status M code_memory s sigma policy)) |
---|
243 | (sfr_8051_index sfr) (sfr8051_index_19 sfr) = |
---|
244 | map_address_using_internal_pseudo_address_map M sigma sfr |
---|
245 | (get_index_v Byte 19 |
---|
246 | (special_function_registers_8051 pseudo_assembly_program code_memory s) |
---|
247 | (sfr_8051_index sfr) (sfr8051_index_19 sfr))). |
---|
248 | #M #code_memory #sigma #policy #s #sfr |
---|
249 | whd in match status_of_pseudo_status; normalize nodelta |
---|
250 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
251 | inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta |
---|
252 | [1: |
---|
253 | cases sfr |
---|
254 | [18: |
---|
255 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
256 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
257 | >sndM_refl % |
---|
258 | ] |
---|
259 | % |
---|
260 | |2: |
---|
261 | @pair_elim #high #low #high_low_refl normalize nodelta |
---|
262 | inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta |
---|
263 | cases sfr |
---|
264 | [18,37: |
---|
265 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
266 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
267 | >sndM_refl normalize nodelta >high_low_refl normalize nodelta |
---|
268 | >eq_upper_lower_refl normalize nodelta |
---|
269 | whd in match (set_8051_sfr ?????); // |
---|
270 | ] |
---|
271 | @get_index_v_set_index_miss whd in ⊢ (?(??%%)); |
---|
272 | @nmk #absurd destruct(absurd) |
---|
273 | ] |
---|
274 | qed. |
---|
275 | |
---|
276 | lemma set_8051_sfr_status_of_pseudo_status: |
---|
277 | ∀M, code_memory, sigma, policy, s, sfr, v,v'. |
---|
278 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
279 | (set_8051_sfr (BitVectorTrie Byte 16) |
---|
280 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
281 | (status_of_pseudo_status M code_memory s sigma policy) sfr v' |
---|
282 | =status_of_pseudo_status M code_memory |
---|
283 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). |
---|
284 | #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok |
---|
285 | whd in ⊢ (??%%); @split_eq_status try % /2/ |
---|
286 | qed. |
---|
287 | |
---|
288 | lemma get_8051_sfr_status_of_pseudo_status: |
---|
289 | ∀M, code_memory, sigma, policy, s, sfr. |
---|
290 | (get_8051_sfr (BitVectorTrie Byte 16) |
---|
291 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
292 | (status_of_pseudo_status M code_memory s sigma policy) sfr = |
---|
293 | map_address_using_internal_pseudo_address_map M sigma sfr |
---|
294 | (get_8051_sfr pseudo_assembly_program code_memory s sfr)). |
---|
295 | #M #code_memory #sigma #policy #s #sfr |
---|
296 | whd in match get_8051_sfr; normalize nodelta |
---|
297 | @get_index_v_status_of_pseudo_status |
---|
298 | qed. |
---|
299 | |
---|
300 | lemma get_8052_sfr_status_of_pseudo_status: |
---|
301 | ∀M, code_memory, sigma, policy, s, sfr. |
---|
302 | (get_8052_sfr (BitVectorTrie Byte 16) |
---|
303 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
304 | (status_of_pseudo_status M code_memory s sigma policy) sfr = |
---|
305 | (get_8052_sfr pseudo_assembly_program code_memory s sfr)). |
---|
306 | // |
---|
307 | qed. |
---|
308 | |
---|
309 | lemma set_8052_sfr_status_of_pseudo_status: |
---|
310 | ∀M, code_memory, sigma, policy, s, sfr, v. |
---|
311 | (set_8052_sfr (BitVectorTrie Byte 16) |
---|
312 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
313 | (status_of_pseudo_status M code_memory s sigma policy) sfr v |
---|
314 | =status_of_pseudo_status M code_memory |
---|
315 | (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). |
---|
316 | // |
---|
317 | qed. |
---|
318 | |
---|
319 | definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ |
---|
320 | λb: Byte. |
---|
321 | let address ≝ nat_of_bitvector … b in |
---|
322 | if (eqb address 128) then None ? |
---|
323 | else if (eqb address 144) then Some … (inl … SFR_P1) |
---|
324 | else if (eqb address 160) then None ? |
---|
325 | else if (eqb address 176) then Some … (inl … SFR_P3) |
---|
326 | else if (eqb address 153) then Some … (inl … SFR_SBUF) |
---|
327 | else if (eqb address 138) then Some … (inl … SFR_TL0) |
---|
328 | else if (eqb address 139) then Some … (inl … SFR_TL1) |
---|
329 | else if (eqb address 140) then Some … (inl … SFR_TH0) |
---|
330 | else if (eqb address 141) then Some … (inl … SFR_TH1) |
---|
331 | else if (eqb address 200) then Some … (inr … SFR_T2CON) |
---|
332 | else if (eqb address 202) then Some … (inr … SFR_RCAP2L) |
---|
333 | else if (eqb address 203) then Some … (inr … SFR_RCAP2H) |
---|
334 | else if (eqb address 204) then Some … (inr … SFR_TL2) |
---|
335 | else if (eqb address 205) then Some … (inr … SFR_TH2) |
---|
336 | else if (eqb address 135) then Some … (inl … SFR_PCON) |
---|
337 | else if (eqb address 136) then Some … (inl … SFR_TCON) |
---|
338 | else if (eqb address 137) then Some … (inl … SFR_TMOD) |
---|
339 | else if (eqb address 152) then Some … (inl … SFR_SCON) |
---|
340 | else if (eqb address 168) then Some … (inl … SFR_IE) |
---|
341 | else if (eqb address 184) then Some … (inl … SFR_IP) |
---|
342 | else if (eqb address 129) then Some … (inl … SFR_SP) |
---|
343 | else if (eqb address 130) then Some … (inl … SFR_DPL) |
---|
344 | else if (eqb address 131) then Some … (inl … SFR_DPH) |
---|
345 | else if (eqb address 208) then Some … (inl … SFR_PSW) |
---|
346 | else if (eqb address 224) then Some … (inl … SFR_ACC_A) |
---|
347 | else if (eqb address 240) then Some … (inl … SFR_ACC_B) |
---|
348 | else None ?. |
---|
349 | |
---|
350 | definition set_bit_addressable_sfr: |
---|
351 | ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → |
---|
352 | PreStatus M code_memory ≝ |
---|
353 | λM: Type[0]. |
---|
354 | λcode_memory:M. |
---|
355 | λs: PreStatus M code_memory. |
---|
356 | λb: Byte. |
---|
357 | λv: Byte. |
---|
358 | match sfr_of_Byte b with |
---|
359 | [ None ⇒ match not_implemented in False with [ ] |
---|
360 | | Some sfr8051_8052 ⇒ |
---|
361 | match sfr8051_8052 with |
---|
362 | [ inl sfr ⇒ |
---|
363 | match sfr with |
---|
364 | [ SFR_P1 ⇒ |
---|
365 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
366 | set_p1_latch ?? s v |
---|
367 | | SFR_P3 ⇒ |
---|
368 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
369 | set_p3_latch ?? s v |
---|
370 | | _ ⇒ set_8051_sfr ?? s sfr v ] |
---|
371 | | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. |
---|
372 | |
---|
373 | definition map_address_Byte_using_internal_pseudo_address_map ≝ |
---|
374 | λM,sigma,d,v. |
---|
375 | match sfr_of_Byte d with |
---|
376 | [ None ⇒ v |
---|
377 | | Some sfr8051_8052 ⇒ |
---|
378 | match sfr8051_8052 with |
---|
379 | [ inl sfr ⇒ |
---|
380 | map_address_using_internal_pseudo_address_map M sigma sfr v |
---|
381 | | inr _ ⇒ v ]]. |
---|
382 | |
---|
383 | lemma set_bit_addressable_sfr_status_of_pseudo_status': |
---|
384 | let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte. |
---|
385 | Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'. |
---|
386 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
387 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
388 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
389 | (status_of_pseudo_status M code_memory s sigma policy) d v' |
---|
390 | =status_of_pseudo_status M code_memory |
---|
391 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
392 | whd in match set_bit_addressable_sfr; |
---|
393 | whd in match map_address_Byte_using_internal_pseudo_address_map; |
---|
394 | normalize nodelta |
---|
395 | @(let M ≝ pseudo_assembly_program in |
---|
396 | λcode_memory:M. |
---|
397 | λs: PreStatus M code_memory. |
---|
398 | λb: Byte. |
---|
399 | λv: Byte. |
---|
400 | match sfr_of_Byte b with |
---|
401 | [ None ⇒ match not_implemented in False with [ ] |
---|
402 | | Some sfr8051_8052 ⇒ |
---|
403 | match sfr8051_8052 with |
---|
404 | [ inl sfr ⇒ |
---|
405 | match sfr with |
---|
406 | [ SFR_P1 ⇒ |
---|
407 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
408 | set_p1_latch ?? s v |
---|
409 | | SFR_P3 ⇒ |
---|
410 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
411 | set_p3_latch ?? s v |
---|
412 | | _ ⇒ set_8051_sfr ?? s sfr v ] |
---|
413 | | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) |
---|
414 | normalize nodelta |
---|
415 | /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ |
---|
416 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta // |
---|
417 | qed. |
---|
418 | |
---|
419 | lemma set_bit_addressable_sfr_status_of_pseudo_status: |
---|
420 | ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte. |
---|
421 | ∀M. ∀sigma. ∀policy. ∀v'. |
---|
422 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
423 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
424 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
425 | (status_of_pseudo_status M code_memory s sigma policy) d v' |
---|
426 | =status_of_pseudo_status M code_memory |
---|
427 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
428 | #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ |
---|
429 | #H @H |
---|
430 | qed. |
---|
431 | |
---|
432 | lemma set_low_internal_ram_status_of_pseudo_status: |
---|
433 | ∀cm,sigma,policy,M,s,ram. |
---|
434 | set_low_internal_ram (BitVectorTrie Byte 16) |
---|
435 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
436 | (status_of_pseudo_status M cm s sigma policy) |
---|
437 | (low_internal_ram_of_pseudo_low_internal_ram M ram) |
---|
438 | = status_of_pseudo_status M cm |
---|
439 | (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. |
---|
440 | // |
---|
441 | qed. |
---|
442 | |
---|
443 | (* Real axiom ATM *) |
---|
444 | axiom insert_low_internal_ram_of_pseudo_low_internal_ram: |
---|
445 | ∀M,sigma,cm,s,addr,v,v'. |
---|
446 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
447 | insert Byte 7 addr v' |
---|
448 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
449 | (low_internal_ram pseudo_assembly_program cm s)) |
---|
450 | =low_internal_ram_of_pseudo_low_internal_ram M |
---|
451 | (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). |
---|
452 | |
---|
453 | lemma insert_low_internal_ram_status_of_pseudo_status: |
---|
454 | ∀M,cm,sigma,policy,s,addr,v,v'. |
---|
455 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
456 | insert Byte 7 addr v' |
---|
457 | (low_internal_ram (BitVectorTrie Byte 16) |
---|
458 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
459 | (status_of_pseudo_status M cm s sigma policy)) |
---|
460 | = low_internal_ram_of_pseudo_low_internal_ram M |
---|
461 | (insert Byte 7 addr v |
---|
462 | (low_internal_ram pseudo_assembly_program cm s)). |
---|
463 | /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/ |
---|
464 | qed. |
---|
465 | |
---|
466 | (* Real axiom ATM *) |
---|
467 | axiom insert_high_internal_ram_of_pseudo_high_internal_ram: |
---|
468 | ∀M,sigma,cm,s,addr,v,v'. |
---|
469 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' → |
---|
470 | insert Byte 7 addr v' |
---|
471 | (high_internal_ram_of_pseudo_high_internal_ram M |
---|
472 | (high_internal_ram pseudo_assembly_program cm s)) |
---|
473 | =high_internal_ram_of_pseudo_high_internal_ram M |
---|
474 | (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)). |
---|
475 | |
---|
476 | lemma insert_high_internal_ram_status_of_pseudo_status: |
---|
477 | ∀M,cm,sigma,policy,s,addr,v,v'. |
---|
478 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' → |
---|
479 | insert Byte 7 addr v' |
---|
480 | (high_internal_ram (BitVectorTrie Byte 16) |
---|
481 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
482 | (status_of_pseudo_status M cm s sigma policy)) |
---|
483 | = high_internal_ram_of_pseudo_high_internal_ram M |
---|
484 | (insert Byte 7 addr v |
---|
485 | (high_internal_ram pseudo_assembly_program cm s)). |
---|
486 | /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/ |
---|
487 | qed. |
---|
488 | |
---|
489 | lemma bit_address_of_register_status_of_pseudo_status: |
---|
490 | ∀M,cm,s,sigma,policy,r. |
---|
491 | bit_address_of_register … |
---|
492 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
493 | (status_of_pseudo_status M cm s sigma policy) r = |
---|
494 | bit_address_of_register … cm s r. |
---|
495 | #M #cm #s #sigma #policy #r whd in ⊢ (??%%); |
---|
496 | >get_8051_sfr_status_of_pseudo_status |
---|
497 | @pair_elim #un #ln #_ |
---|
498 | @pair_elim #r1 #r0 #_ % |
---|
499 | qed. |
---|
500 | |
---|
501 | (*CSC: provable using the axiom in AssemblyProof, but this one seems more |
---|
502 | primitive *) |
---|
503 | axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: |
---|
504 | ∀M,sigma,cm,s,addr. |
---|
505 | lookup Byte 7 addr |
---|
506 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
507 | (low_internal_ram pseudo_assembly_program cm s)) (zero 8) |
---|
508 | = |
---|
509 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) |
---|
510 | (lookup Byte 7 addr |
---|
511 | (low_internal_ram pseudo_assembly_program cm s) (zero 8)). |
---|
512 | |
---|
513 | (*CSC: provable using the axiom in AssemblyProof, but this one seems more |
---|
514 | primitive *) |
---|
515 | axiom lookup_high_internal_ram_of_pseudo_high_internal_ram: |
---|
516 | ∀M,sigma,cm,s,addr. |
---|
517 | lookup Byte 7 addr |
---|
518 | (high_internal_ram_of_pseudo_high_internal_ram M |
---|
519 | (high_internal_ram pseudo_assembly_program cm s)) (zero 8) |
---|
520 | = |
---|
521 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) |
---|
522 | (lookup Byte 7 addr |
---|
523 | (high_internal_ram pseudo_assembly_program cm s) (zero 8)). |
---|
524 | |
---|
525 | lemma get_register_status_of_pseudo_status: |
---|
526 | ∀M,cm,sigma,policy,s,r. |
---|
527 | get_register … |
---|
528 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
529 | (status_of_pseudo_status M cm s sigma policy) r = |
---|
530 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) |
---|
531 | (get_register … cm s r). |
---|
532 | #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta |
---|
533 | whd in match status_of_pseudo_status; normalize nodelta |
---|
534 | >bit_address_of_register_status_of_pseudo_status |
---|
535 | @lookup_low_internal_ram_of_pseudo_low_internal_ram |
---|
536 | qed. |
---|
537 | |
---|
538 | lemma external_ram_status_of_pseudo_status: |
---|
539 | ∀M,cm,s,sigma,policy. |
---|
540 | external_ram … |
---|
541 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
542 | (status_of_pseudo_status M cm s sigma policy) = |
---|
543 | external_ram … cm s. |
---|
544 | // |
---|
545 | qed. |
---|
546 | |
---|
547 | lemma set_external_ram_status_of_pseudo_status: |
---|
548 | ∀M,cm,ps,sigma,policy,ram. |
---|
549 | set_external_ram … |
---|
550 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
551 | (status_of_pseudo_status M cm ps sigma policy) |
---|
552 | ram = |
---|
553 | status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy. |
---|
554 | // |
---|
555 | qed. |
---|
556 | |
---|
557 | lemma set_register_status_of_pseudo_status: |
---|
558 | ∀M,cm,s,sigma,policy,r,v,v'. |
---|
559 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
560 | (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' → |
---|
561 | set_register (BitVectorTrie Byte 16) |
---|
562 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
563 | (status_of_pseudo_status M cm s sigma policy) r v' |
---|
564 | = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v) |
---|
565 | sigma policy. |
---|
566 | #M #cm #s #sigma #policy #r #v #v' #v_ok |
---|
567 | whd in match set_register; normalize nodelta |
---|
568 | >bit_address_of_register_status_of_pseudo_status |
---|
569 | >(insert_low_internal_ram_status_of_pseudo_status … v_ok) |
---|
570 | @set_low_internal_ram_status_of_pseudo_status |
---|
571 | qed. |
---|
572 | |
---|
573 | definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ |
---|
574 | λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr. |
---|
575 | match addr with |
---|
576 | [ INDIRECT i ⇒ |
---|
577 | assoc_list_lookup ?? |
---|
578 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … |
---|
579 | | EXT_INDIRECT e ⇒ |
---|
580 | assoc_list_lookup ?? |
---|
581 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … |
---|
582 | | ACC_DPTR ⇒ |
---|
583 | (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer |
---|
584 | in the ACC_A *) |
---|
585 | map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = |
---|
586 | get_8051_sfr … cm s SFR_ACC_A |
---|
587 | | ACC_PC ⇒ |
---|
588 | (* XXX: as above *) |
---|
589 | map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = |
---|
590 | get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s |
---|
591 | | _ ⇒ True ]. |
---|
592 | |
---|
593 | definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝ |
---|
594 | λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v. |
---|
595 | match addr with |
---|
596 | [ DIRECT d ⇒ |
---|
597 | let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in |
---|
598 | match head' … bit_one with |
---|
599 | [ true ⇒ |
---|
600 | map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v |
---|
601 | | false ⇒ |
---|
602 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] |
---|
603 | | INDIRECT i ⇒ |
---|
604 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
605 | map_internal_ram_address_using_pseudo_address_map M sigma register v |
---|
606 | | REGISTER r ⇒ |
---|
607 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
608 | (false:::bit_address_of_register … s r) v |
---|
609 | | ACC_A ⇒ |
---|
610 | map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v |
---|
611 | | _ ⇒ v ]. |
---|
612 | |
---|
613 | definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; |
---|
614 | acc_a ; acc_b ; ext_indirect ; |
---|
615 | ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝ |
---|
616 | λm, cm, s, a, v. |
---|
617 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
618 | acc_a ; acc_b ; ext_indirect ; |
---|
619 | ext_indirect_dptr ]] x) → |
---|
620 | PreStatus m cm |
---|
621 | with |
---|
622 | [ DIRECT d ⇒ |
---|
623 | λdirect: True. |
---|
624 | let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in |
---|
625 | match head' … bit_one with |
---|
626 | [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v |
---|
627 | | false ⇒ |
---|
628 | let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in |
---|
629 | set_low_internal_ram ?? s memory |
---|
630 | ] |
---|
631 | | INDIRECT i ⇒ |
---|
632 | λindirect: True. |
---|
633 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
634 | let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in |
---|
635 | match head' … bit_one with |
---|
636 | [ false ⇒ |
---|
637 | let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in |
---|
638 | set_low_internal_ram ?? s memory |
---|
639 | | true ⇒ |
---|
640 | let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in |
---|
641 | set_high_internal_ram ?? s memory |
---|
642 | ] |
---|
643 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
644 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
645 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
646 | | EXT_INDIRECT e ⇒ |
---|
647 | λext_indirect: True. |
---|
648 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
649 | let padded_address ≝ pad 8 8 address in |
---|
650 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
651 | set_external_ram ?? s memory |
---|
652 | | EXT_INDIRECT_DPTR ⇒ |
---|
653 | λext_indirect_dptr: True. |
---|
654 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
655 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
656 | set_external_ram ?? s memory |
---|
657 | | _ ⇒ |
---|
658 | λother: False. |
---|
659 | match other in False with [ ] |
---|
660 | ] (subaddressing_modein … a). |
---|
661 | |
---|
662 | (*CSC: move elsewhere*) |
---|
663 | lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v. |
---|
664 | #A #n #v inversion v in ⊢ ?; |
---|
665 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/ |
---|
666 | | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ] |
---|
667 | qed. |
---|
668 | |
---|
669 | (*CSC: move elsewhere*) |
---|
670 | lemma tail_singleton: ∀A,v. tail A 0 v = [[]]. |
---|
671 | #A #v inversion v in ⊢ ?; |
---|
672 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H) |
---|
673 | | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize |
---|
674 | /2 by jmeq_to_eq/ |
---|
675 | ] |
---|
676 | qed. |
---|
677 | |
---|
678 | (*CSC: move elsewhere*) |
---|
679 | lemma eq_cons_head_append: |
---|
680 | ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n. |
---|
681 | head' A 0 hd:::tl = hd@@tl. |
---|
682 | #A #n #hd #tl >(eq_head' … hd) >tail_singleton % |
---|
683 | qed. |
---|
684 | |
---|
685 | lemma set_arg_8_status_of_pseudo_status: |
---|
686 | ∀cm. |
---|
687 | ∀ps. |
---|
688 | ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. |
---|
689 | ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. |
---|
690 | map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → |
---|
691 | map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → |
---|
692 | set_arg_8 (BitVectorTrie Byte 16) |
---|
693 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
694 | (status_of_pseudo_status M cm ps sigma policy) |
---|
695 | addr value' = |
---|
696 | status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. |
---|
697 | whd in match set_arg_8; normalize nodelta |
---|
698 | @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ; |
---|
699 | acc_a ; acc_b ; ext_indirect ; |
---|
700 | ext_indirect_dptr ]]. λv. |
---|
701 | match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
702 | acc_a ; acc_b ; ext_indirect ; |
---|
703 | ext_indirect_dptr ]] addr) → |
---|
704 | Σp.? |
---|
705 | with |
---|
706 | [ DIRECT d ⇒ |
---|
707 | λdirect: True. |
---|
708 | deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in |
---|
709 | match head' … bit_one with |
---|
710 | [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v |
---|
711 | | false ⇒ |
---|
712 | let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in |
---|
713 | set_low_internal_ram ?? s memory |
---|
714 | ] |
---|
715 | | INDIRECT i ⇒ |
---|
716 | λindirect: True. |
---|
717 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
718 | let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in |
---|
719 | match head' … bit_one with |
---|
720 | [ false ⇒ |
---|
721 | let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in |
---|
722 | set_low_internal_ram ?? s memory |
---|
723 | | true ⇒ |
---|
724 | let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in |
---|
725 | set_high_internal_ram ?? s memory |
---|
726 | ] |
---|
727 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
728 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
729 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
730 | | EXT_INDIRECT e ⇒ |
---|
731 | λext_indirect: True. |
---|
732 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
733 | let padded_address ≝ pad 8 8 address in |
---|
734 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
735 | set_external_ram ?? s memory |
---|
736 | | EXT_INDIRECT_DPTR ⇒ |
---|
737 | λext_indirect_dptr: True. |
---|
738 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
739 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
740 | set_external_ram ?? s memory |
---|
741 | | _ ⇒ |
---|
742 | λother: False. |
---|
743 | match other in False with [ ] |
---|
744 | ] (subaddressing_modein … a)) normalize nodelta |
---|
745 | #M #sigma #policy #v' |
---|
746 | whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta |
---|
747 | whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta |
---|
748 | [1,2: |
---|
749 | <vsplit_refl normalize nodelta >p normalize nodelta |
---|
750 | [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status |
---|
751 | | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] |
---|
752 | |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; |
---|
753 | >get_register_status_of_pseudo_status |
---|
754 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
755 | >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta |
---|
756 | [ >(insert_high_internal_ram_status_of_pseudo_status … v) |
---|
757 | | >(insert_low_internal_ram_status_of_pseudo_status … v) ] |
---|
758 | // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % |
---|
759 | |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status |
---|
760 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
761 | >EQ1 normalize nodelta |
---|
762 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status |
---|
763 | |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/ |
---|
764 | |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/ |
---|
765 | |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status % |
---|
766 | |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status |
---|
767 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] |
---|
768 | qed. |
---|
769 | |
---|
770 | definition get_bit_addressable_sfr: |
---|
771 | ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝ |
---|
772 | λM: Type[0]. |
---|
773 | λcode_memory:M. |
---|
774 | λs: PreStatus M code_memory. |
---|
775 | λb: Byte. |
---|
776 | λl: bool. |
---|
777 | match sfr_of_Byte b with |
---|
778 | [ None ⇒ match not_implemented in False with [ ] |
---|
779 | | Some sfr8051_8052 ⇒ |
---|
780 | match sfr8051_8052 with |
---|
781 | [ inl sfr ⇒ |
---|
782 | match sfr with |
---|
783 | [ SFR_P1 ⇒ |
---|
784 | if l then |
---|
785 | p1_latch … s |
---|
786 | else |
---|
787 | get_8051_sfr … s SFR_P1 |
---|
788 | | SFR_P3 ⇒ |
---|
789 | if l then |
---|
790 | p3_latch … s |
---|
791 | else |
---|
792 | get_8051_sfr … s SFR_P3 |
---|
793 | | _ ⇒ get_8051_sfr … s sfr |
---|
794 | ] |
---|
795 | | inr sfr ⇒ get_8052_sfr M code_memory s sfr |
---|
796 | ] |
---|
797 | ]. |
---|
798 | |
---|
799 | definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ; |
---|
800 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
801 | acc_pc ; ext_indirect ; |
---|
802 | ext_indirect_dptr ]] → Byte ≝ |
---|
803 | λm, cm, s, l, a. |
---|
804 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
805 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
806 | acc_pc ; ext_indirect ; |
---|
807 | ext_indirect_dptr ]] x) → ? with |
---|
808 | [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A |
---|
809 | | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B |
---|
810 | | DATA d ⇒ λdata: True. d |
---|
811 | | REGISTER r ⇒ λregister: True. get_register ?? s r |
---|
812 | | EXT_INDIRECT_DPTR ⇒ |
---|
813 | λext_indirect_dptr: True. |
---|
814 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
815 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
816 | | EXT_INDIRECT e ⇒ |
---|
817 | λext_indirect: True. |
---|
818 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
819 | let padded_address ≝ pad 8 8 address in |
---|
820 | lookup ? 16 padded_address (external_ram ?? s) (zero 8) |
---|
821 | | ACC_DPTR ⇒ |
---|
822 | λacc_dptr: True. |
---|
823 | let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
824 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
825 | let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in |
---|
826 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
827 | | ACC_PC ⇒ |
---|
828 | λacc_pc: True. |
---|
829 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
830 | let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in |
---|
831 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
832 | | DIRECT d ⇒ |
---|
833 | λdirect: True. |
---|
834 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in |
---|
835 | match head' … hd with |
---|
836 | [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l |
---|
837 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
838 | ] |
---|
839 | | INDIRECT i ⇒ |
---|
840 | λindirect: True. |
---|
841 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in |
---|
842 | match head' … hd with |
---|
843 | [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) |
---|
844 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
845 | ] |
---|
846 | | _ ⇒ λother. |
---|
847 | match other in False with [ ] |
---|
848 | ] (subaddressing_modein … a). |
---|
849 | |
---|
850 | lemma p1_latch_status_of_pseudo_status: |
---|
851 | ∀M. |
---|
852 | ∀code_memory: pseudo_assembly_program. |
---|
853 | ∀s: PreStatus … code_memory. |
---|
854 | ∀sigma. |
---|
855 | ∀policy. |
---|
856 | (p1_latch (BitVectorTrie Byte 16) |
---|
857 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
858 | (status_of_pseudo_status M code_memory s sigma policy) = |
---|
859 | (p1_latch pseudo_assembly_program code_memory s)). |
---|
860 | // |
---|
861 | qed. |
---|
862 | |
---|
863 | lemma p3_latch_status_of_pseudo_status: |
---|
864 | ∀M. |
---|
865 | ∀code_memory: pseudo_assembly_program. |
---|
866 | ∀s: PreStatus … code_memory. |
---|
867 | ∀sigma. |
---|
868 | ∀policy. |
---|
869 | (p3_latch (BitVectorTrie Byte 16) |
---|
870 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
871 | (status_of_pseudo_status M code_memory s sigma policy) = |
---|
872 | (p3_latch pseudo_assembly_program code_memory s)). |
---|
873 | // |
---|
874 | qed. |
---|
875 | |
---|
876 | lemma get_bit_addressable_sfr_status_of_pseudo_status': |
---|
877 | let M ≝ pseudo_assembly_program in |
---|
878 | ∀code_memory: M. |
---|
879 | ∀s: PreStatus M code_memory. |
---|
880 | ∀d: Byte. |
---|
881 | ∀l: bool. |
---|
882 | Σp: Byte. ∀M. ∀sigma. ∀policy. |
---|
883 | (get_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
884 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
885 | (status_of_pseudo_status M code_memory s sigma policy) d l = |
---|
886 | map_address_Byte_using_internal_pseudo_address_map M sigma |
---|
887 | d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). |
---|
888 | whd in match get_bit_addressable_sfr; |
---|
889 | whd in match map_address_Byte_using_internal_pseudo_address_map; |
---|
890 | normalize nodelta |
---|
891 | @(let M ≝ pseudo_assembly_program in |
---|
892 | λcode_memory:M. |
---|
893 | λs: PreStatus M code_memory. |
---|
894 | λb: Byte. |
---|
895 | λl: bool. |
---|
896 | match sfr_of_Byte b with |
---|
897 | [ None ⇒ match not_implemented in False with [ ] |
---|
898 | | Some sfr8051_8052 ⇒ |
---|
899 | match sfr8051_8052 with |
---|
900 | [ inl sfr ⇒ |
---|
901 | match sfr with |
---|
902 | [ SFR_P1 ⇒ |
---|
903 | if l then |
---|
904 | p1_latch … s |
---|
905 | else |
---|
906 | get_8051_sfr … s SFR_P1 |
---|
907 | | SFR_P3 ⇒ |
---|
908 | if l then |
---|
909 | p3_latch … s |
---|
910 | else |
---|
911 | get_8051_sfr … s SFR_P3 |
---|
912 | | _ ⇒ get_8051_sfr … s sfr |
---|
913 | ] |
---|
914 | | inr sfr ⇒ get_8052_sfr M code_memory s sfr |
---|
915 | ] |
---|
916 | ]) |
---|
917 | #M #sigma #policy normalize nodelta |
---|
918 | /by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/ |
---|
919 | qed. |
---|
920 | |
---|
921 | lemma get_bit_addressable_sfr_status_of_pseudo_status: |
---|
922 | let M ≝ pseudo_assembly_program in |
---|
923 | ∀code_memory: M. |
---|
924 | ∀s: PreStatus M code_memory. |
---|
925 | ∀d: Byte. |
---|
926 | ∀l: bool. |
---|
927 | ∀M. ∀sigma. ∀policy. |
---|
928 | (get_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
929 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
930 | (status_of_pseudo_status M code_memory s sigma policy) d l = |
---|
931 | map_address_Byte_using_internal_pseudo_address_map M sigma |
---|
932 | d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). |
---|
933 | #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ |
---|
934 | #H @H |
---|
935 | qed. |
---|
936 | |
---|
937 | lemma program_counter_status_of_pseudo_status: |
---|
938 | ∀code_memory: pseudo_assembly_program. |
---|
939 | ∀s: PreStatus ? code_memory. |
---|
940 | ∀M. ∀sigma. ∀policy. |
---|
941 | program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
942 | (status_of_pseudo_status M code_memory s sigma policy) = |
---|
943 | sigma (program_counter … s). |
---|
944 | // |
---|
945 | qed. |
---|
946 | |
---|
947 | lemma get_cy_flag_status_of_pseudo_status: |
---|
948 | ∀M, cm, sigma, policy, s. |
---|
949 | (get_cy_flag (BitVectorTrie Byte 16) |
---|
950 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
951 | (status_of_pseudo_status M cm s sigma policy) = |
---|
952 | get_cy_flag pseudo_assembly_program cm s). |
---|
953 | #M #cm #sigma #policy #s |
---|
954 | whd in match get_cy_flag; normalize nodelta |
---|
955 | >get_index_v_status_of_pseudo_status % |
---|
956 | qed. |
---|
957 | |
---|
958 | lemma get_arg_8_status_of_pseudo_status: |
---|
959 | ∀cm. |
---|
960 | ∀ps. |
---|
961 | ∀l. |
---|
962 | ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. |
---|
963 | Σp: Byte. ∀M. ∀sigma. ∀policy. |
---|
964 | map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → |
---|
965 | get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
966 | (status_of_pseudo_status M cm ps sigma policy) l addr = |
---|
967 | map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr). |
---|
968 | whd in match get_arg_8; normalize nodelta |
---|
969 | @(let m ≝ pseudo_assembly_program in |
---|
970 | λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]]. |
---|
971 | match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with |
---|
972 | [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A |
---|
973 | | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B |
---|
974 | | DATA d ⇒ λdata: True. d |
---|
975 | | REGISTER r ⇒ λregister: True. get_register ?? s r |
---|
976 | | EXT_INDIRECT_DPTR ⇒ |
---|
977 | λext_indirect_dptr: True. |
---|
978 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
979 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
980 | | EXT_INDIRECT e ⇒ |
---|
981 | λext_indirect: True. |
---|
982 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
983 | let padded_address ≝ pad 8 8 address in |
---|
984 | lookup ? 16 padded_address (external_ram ?? s) (zero 8) |
---|
985 | | ACC_DPTR ⇒ |
---|
986 | λacc_dptr: True. |
---|
987 | let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
988 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
989 | let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in |
---|
990 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
991 | | ACC_PC ⇒ |
---|
992 | λacc_pc: True. |
---|
993 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
994 | let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in |
---|
995 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
996 | | DIRECT d ⇒ |
---|
997 | λdirect: True. |
---|
998 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in |
---|
999 | match head' … hd with |
---|
1000 | [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l |
---|
1001 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
1002 | ] |
---|
1003 | | INDIRECT i ⇒ |
---|
1004 | λindirect: True. |
---|
1005 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in |
---|
1006 | match head' … hd with |
---|
1007 | [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) |
---|
1008 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
1009 | ] |
---|
1010 | | _ ⇒ λother: False. |
---|
1011 | match other in False with [ ] |
---|
1012 | ] (subaddressing_modein … a)) normalize nodelta |
---|
1013 | #M #sigma #policy |
---|
1014 | whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta |
---|
1015 | whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta |
---|
1016 | [1: |
---|
1017 | #_ >p normalize nodelta >p1 normalize nodelta |
---|
1018 | @get_bit_addressable_sfr_status_of_pseudo_status |
---|
1019 | |2: |
---|
1020 | #_>p normalize nodelta >p1 normalize nodelta |
---|
1021 | @lookup_low_internal_ram_of_pseudo_low_internal_ram |
---|
1022 | |3,4: |
---|
1023 | #assoc_list_assm >get_register_status_of_pseudo_status |
---|
1024 | whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta |
---|
1025 | >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta |
---|
1026 | [1: |
---|
1027 | >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma) |
---|
1028 | |2: |
---|
1029 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
1030 | ] |
---|
1031 | @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % |
---|
1032 | |5: |
---|
1033 | #assoc_list_assm >get_register_status_of_pseudo_status |
---|
1034 | whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta |
---|
1035 | >assoc_list_assm normalize nodelta % |
---|
1036 | |6,7,8,9: |
---|
1037 | #_ /2/ |
---|
1038 | |10: |
---|
1039 | #acc_a_assm >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status |
---|
1040 | >get_8051_sfr_status_of_pseudo_status |
---|
1041 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
1042 | >acc_a_assm >p normalize nodelta // |
---|
1043 | |11: |
---|
1044 | * #map_acc_a_assm #sigma_assm >get_8051_sfr_status_of_pseudo_status >program_counter_status_of_pseudo_status |
---|
1045 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
1046 | >sigma_assm >map_acc_a_assm >p normalize nodelta // |
---|
1047 | |12: |
---|
1048 | #_ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status |
---|
1049 | >external_ram_status_of_pseudo_status // |
---|
1050 | ] |
---|
1051 | qed. |
---|
1052 | |
---|
1053 | lemma get_arg_16_status_of_pseudo_status: |
---|
1054 | ∀cm. |
---|
1055 | ∀ps. |
---|
1056 | ∀addr: [[data16]]. |
---|
1057 | ∀M. ∀sigma. ∀policy. |
---|
1058 | get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
1059 | (status_of_pseudo_status M cm ps sigma policy) addr = |
---|
1060 | (get_arg_16 … cm ps addr). |
---|
1061 | // |
---|
1062 | qed. |
---|
1063 | |
---|
1064 | lemma set_arg_16_status_of_pseudo_status: |
---|
1065 | ∀cm. |
---|
1066 | ∀ps. |
---|
1067 | ∀addr: [[dptr]]. |
---|
1068 | ∀v: Word. |
---|
1069 | ∀M. ∀sigma. ∀policy. |
---|
1070 | set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
1071 | (status_of_pseudo_status M cm ps sigma policy) v addr = |
---|
1072 | status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. |
---|
1073 | #cm #ps #addr #v #M #sigma #policy |
---|
1074 | @(subaddressing_mode_elim … addr) |
---|
1075 | whd in match set_arg_16; normalize nodelta |
---|
1076 | whd in match set_arg_16'; normalize nodelta |
---|
1077 | @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta |
---|
1078 | >(set_8051_sfr_status_of_pseudo_status … bu) |
---|
1079 | [1: >(set_8051_sfr_status_of_pseudo_status … bl) ] |
---|
1080 | // |
---|
1081 | qed. |
---|
1082 | |
---|
1083 | definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] → |
---|
1084 | bool → bool ≝ |
---|
1085 | λm, cm, s, a, l. |
---|
1086 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; |
---|
1087 | n_bit_addr ; |
---|
1088 | carry ]] x) → ? with |
---|
1089 | [ BIT_ADDR b ⇒ |
---|
1090 | λbit_addr: True. |
---|
1091 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
1092 | match head' … bit_1 with |
---|
1093 | [ true ⇒ |
---|
1094 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1095 | let d ≝ address ÷ 8 in |
---|
1096 | let m ≝ address mod 8 in |
---|
1097 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1098 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
1099 | get_index_v … sfr m ? |
---|
1100 | | false ⇒ |
---|
1101 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1102 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1103 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1104 | get_index_v … t (modulus address 8) ? |
---|
1105 | ] |
---|
1106 | | N_BIT_ADDR n ⇒ |
---|
1107 | λn_bit_addr: True. |
---|
1108 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in |
---|
1109 | match head' … bit_1 with |
---|
1110 | [ true ⇒ |
---|
1111 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1112 | let d ≝ address ÷ 8 in |
---|
1113 | let m ≝ address mod 8 in |
---|
1114 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1115 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
1116 | ¬(get_index_v … sfr m ?) |
---|
1117 | | false ⇒ |
---|
1118 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1119 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1120 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1121 | ¬(get_index_v … t (modulus address 8) ?) |
---|
1122 | ] |
---|
1123 | | CARRY ⇒ λcarry: True. get_cy_flag ?? s |
---|
1124 | | _ ⇒ λother. |
---|
1125 | match other in False with [ ] |
---|
1126 | ] (subaddressing_modein … a). |
---|
1127 | @modulus_less_than |
---|
1128 | qed. |
---|
1129 | |
---|
1130 | definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝ |
---|
1131 | λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl. |
---|
1132 | match addr with |
---|
1133 | [ BIT_ADDR b ⇒ |
---|
1134 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
1135 | match head' … bit_1 with |
---|
1136 | [ true ⇒ |
---|
1137 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1138 | let d ≝ address ÷ 8 in |
---|
1139 | let m ≝ address mod 8 in |
---|
1140 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1141 | map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l |
---|
1142 | | false ⇒ |
---|
1143 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1144 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1145 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1146 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
1147 | (false:::address') t = t |
---|
1148 | ] |
---|
1149 | | N_BIT_ADDR b ⇒ |
---|
1150 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
1151 | match head' … bit_1 with |
---|
1152 | [ true ⇒ |
---|
1153 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1154 | let d ≝ address ÷ 8 in |
---|
1155 | let m ≝ address mod 8 in |
---|
1156 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1157 | map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l |
---|
1158 | | false ⇒ |
---|
1159 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1160 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1161 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1162 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
1163 | (false:::address') t = t |
---|
1164 | ] |
---|
1165 | | _ ⇒ True ]. |
---|
1166 | |
---|
1167 | lemma get_arg_1_status_of_pseudo_status': |
---|
1168 | ∀cm. |
---|
1169 | ∀ps. |
---|
1170 | ∀addr: [[bit_addr; n_bit_addr; carry]]. |
---|
1171 | ∀l. |
---|
1172 | Σb: bool. ∀M. ∀sigma. ∀policy. |
---|
1173 | map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → |
---|
1174 | get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
1175 | (status_of_pseudo_status M cm ps sigma policy) addr l = |
---|
1176 | (get_arg_1 … cm ps addr l). |
---|
1177 | whd in match get_arg_1; normalize nodelta |
---|
1178 | @(let m ≝ pseudo_assembly_program in |
---|
1179 | λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl. |
---|
1180 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; |
---|
1181 | n_bit_addr ; |
---|
1182 | carry ]] x) → Σb: bool. ? with |
---|
1183 | [ BIT_ADDR b ⇒ |
---|
1184 | λbit_addr: True. |
---|
1185 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
1186 | match head' … bit_1 with |
---|
1187 | [ true ⇒ |
---|
1188 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1189 | let d ≝ address ÷ 8 in |
---|
1190 | let m ≝ address mod 8 in |
---|
1191 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1192 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
1193 | get_index_v … sfr m ? |
---|
1194 | | false ⇒ |
---|
1195 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1196 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1197 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1198 | get_index_v … t (modulus address 8) ? |
---|
1199 | ] |
---|
1200 | | N_BIT_ADDR n ⇒ |
---|
1201 | λn_bit_addr: True. |
---|
1202 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in |
---|
1203 | match head' … bit_1 with |
---|
1204 | [ true ⇒ |
---|
1205 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1206 | let d ≝ address ÷ 8 in |
---|
1207 | let m ≝ address mod 8 in |
---|
1208 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1209 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
1210 | ¬(get_index_v … sfr m ?) |
---|
1211 | | false ⇒ |
---|
1212 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1213 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1214 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1215 | ¬(get_index_v … t (modulus address 8) ?) |
---|
1216 | ] |
---|
1217 | | CARRY ⇒ λcarry: True. get_cy_flag ?? s |
---|
1218 | | _ ⇒ λother. |
---|
1219 | match other in False with [ ] |
---|
1220 | ] (subaddressing_modein … a)) normalize nodelta |
---|
1221 | try @modulus_less_than |
---|
1222 | #M #sigma #policy |
---|
1223 | [1: |
---|
1224 | #_ @get_cy_flag_status_of_pseudo_status |
---|
1225 | |2,4: |
---|
1226 | whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta |
---|
1227 | >get_bit_addressable_sfr_status_of_pseudo_status #map_address_assm |
---|
1228 | >map_address_assm % |
---|
1229 | |3,5: |
---|
1230 | whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta |
---|
1231 | whd in match status_of_pseudo_status; normalize nodelta |
---|
1232 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
1233 | #map_address_assm >map_address_assm % |
---|
1234 | ] |
---|
1235 | qed. |
---|
1236 | |
---|
1237 | lemma get_arg_1_status_of_pseudo_status: |
---|
1238 | ∀cm. |
---|
1239 | ∀ps. |
---|
1240 | ∀addr: [[bit_addr; n_bit_addr; carry]]. |
---|
1241 | ∀l. |
---|
1242 | ∀M. ∀sigma. ∀policy. |
---|
1243 | map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → |
---|
1244 | get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
1245 | (status_of_pseudo_status M cm ps sigma policy) addr l = |
---|
1246 | (get_arg_1 … cm ps addr l). |
---|
1247 | #cm #ps #addr #l |
---|
1248 | cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm |
---|
1249 | @assm |
---|
1250 | qed. |
---|
1251 | |
---|
1252 | definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝ |
---|
1253 | λm: Type[0]. |
---|
1254 | λcm. |
---|
1255 | λs: PreStatus m cm. |
---|
1256 | λa: [[bit_addr; carry]]. |
---|
1257 | λv: Bit. |
---|
1258 | match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with |
---|
1259 | [ BIT_ADDR b ⇒ λbit_addr: True. |
---|
1260 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1261 | match head' … bit_1 with |
---|
1262 | [ true ⇒ |
---|
1263 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1264 | let d ≝ address ÷ 8 in |
---|
1265 | let m ≝ address mod 8 in |
---|
1266 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1267 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
1268 | let new_sfr ≝ set_index … sfr m v ? in |
---|
1269 | set_bit_addressable_sfr … s new_sfr t |
---|
1270 | | false ⇒ |
---|
1271 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1272 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1273 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1274 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
1275 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
1276 | set_low_internal_ram … s memory |
---|
1277 | ] |
---|
1278 | | CARRY ⇒ |
---|
1279 | λcarry: True. |
---|
1280 | let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1281 | let new_psw ≝ v:::seven_bits in |
---|
1282 | set_8051_sfr ?? s SFR_PSW new_psw |
---|
1283 | | _ ⇒ |
---|
1284 | λother: False. |
---|
1285 | match other in False with |
---|
1286 | [ ] |
---|
1287 | ] (subaddressing_modein … a). |
---|
1288 | try (repeat @le_S_S @le_O_n) |
---|
1289 | try @modulus_less_than |
---|
1290 | /by/ |
---|
1291 | cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *) |
---|
1292 | qed. |
---|
1293 | |
---|
1294 | definition set_arg_1: |
---|
1295 | ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → |
---|
1296 | Bit → PreStatus M code_memory ≝ set_arg_1'. |
---|
1297 | |
---|
1298 | definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ |
---|
1299 | λM: internal_pseudo_address_map. |
---|
1300 | λcm: pseudo_assembly_program. |
---|
1301 | λs: PreStatus ? cm. |
---|
1302 | λsigma: Word → Word. |
---|
1303 | λaddr: [[bit_addr; carry]]. |
---|
1304 | λv: Bit. |
---|
1305 | match addr with |
---|
1306 | [ BIT_ADDR b ⇒ |
---|
1307 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1308 | match head' … bit_1 with |
---|
1309 | [ true ⇒ |
---|
1310 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1311 | let d ≝ address ÷ 8 in |
---|
1312 | let m ≝ address mod 8 in |
---|
1313 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1314 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
1315 | map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr |
---|
1316 | | false ⇒ |
---|
1317 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1318 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1319 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1320 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
1321 | (false:::address') t = t |
---|
1322 | ] |
---|
1323 | | CARRY ⇒ True |
---|
1324 | | _ ⇒ True |
---|
1325 | ]. |
---|
1326 | |
---|
1327 | definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝ |
---|
1328 | λM: internal_pseudo_address_map. |
---|
1329 | λcm: pseudo_assembly_program. |
---|
1330 | λs: PreStatus ? cm. |
---|
1331 | λsigma: Word → Word. |
---|
1332 | λaddr: [[bit_addr; carry]]. |
---|
1333 | λv: Bit. |
---|
1334 | match addr with |
---|
1335 | [ BIT_ADDR b ⇒ |
---|
1336 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1337 | match head' … bit_1 with |
---|
1338 | [ true ⇒ |
---|
1339 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1340 | let d ≝ address ÷ 8 in |
---|
1341 | let m ≝ address mod 8 in |
---|
1342 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1343 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
1344 | let new_sfr ≝ set_index … sfr m v ? in |
---|
1345 | map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t |
---|
1346 | | false ⇒ |
---|
1347 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1348 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1349 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1350 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
1351 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
1352 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
1353 | (false:::address') n_bit = n_bit |
---|
1354 | ] |
---|
1355 | | CARRY ⇒ True |
---|
1356 | | _ ⇒ True |
---|
1357 | ]. |
---|
1358 | @modulus_less_than |
---|
1359 | qed. |
---|
1360 | |
---|
1361 | lemma set_arg_1_status_of_pseudo_status: |
---|
1362 | ∀cm: pseudo_assembly_program. |
---|
1363 | ∀ps: PreStatus pseudo_assembly_program cm. |
---|
1364 | ∀addr: [[bit_addr; carry]]. |
---|
1365 | ∀b: Bit. |
---|
1366 | Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. |
---|
1367 | map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → |
---|
1368 | map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b → |
---|
1369 | set_arg_1 (BitVectorTrie Byte 16) |
---|
1370 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
1371 | (status_of_pseudo_status M cm ps sigma policy) addr b = |
---|
1372 | status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy. |
---|
1373 | whd in match set_arg_1; normalize nodelta |
---|
1374 | whd in match set_arg_1'; normalize nodelta |
---|
1375 | whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta |
---|
1376 | whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta |
---|
1377 | @(let m ≝ pseudo_assembly_program in |
---|
1378 | λcm. |
---|
1379 | λs: PreStatus m cm. |
---|
1380 | λa: [[bit_addr; carry]]. |
---|
1381 | λv: Bit. |
---|
1382 | match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with |
---|
1383 | [ BIT_ADDR b ⇒ λbit_addr: True. |
---|
1384 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1385 | match head' … bit_1 with |
---|
1386 | [ true ⇒ |
---|
1387 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1388 | let d ≝ address ÷ 8 in |
---|
1389 | let m ≝ address mod 8 in |
---|
1390 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
1391 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
1392 | let new_sfr ≝ set_index … sfr m v ? in |
---|
1393 | set_bit_addressable_sfr … s new_sfr t |
---|
1394 | | false ⇒ |
---|
1395 | let address ≝ nat_of_bitvector … seven_bits in |
---|
1396 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
1397 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
1398 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
1399 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
1400 | set_low_internal_ram … s memory |
---|
1401 | ] |
---|
1402 | | CARRY ⇒ |
---|
1403 | λcarry: True. |
---|
1404 | let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
1405 | let new_psw ≝ v:::seven_bits in |
---|
1406 | set_8051_sfr ?? s SFR_PSW new_psw |
---|
1407 | | _ ⇒ |
---|
1408 | λother: False. |
---|
1409 | match other in False with |
---|
1410 | [ ] |
---|
1411 | ] (subaddressing_modein … a)) normalize nodelta |
---|
1412 | try @modulus_less_than #M #sigma #policy |
---|
1413 | [1: |
---|
1414 | #_ #_ >get_8051_sfr_status_of_pseudo_status |
---|
1415 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
1416 | >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % |
---|
1417 | |2,3: |
---|
1418 | >get_8051_sfr_status_of_pseudo_status |
---|
1419 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
1420 | >p normalize nodelta >p1 normalize nodelta |
---|
1421 | #map_bit_address_assm_1 #map_bit_address_assm_2 |
---|
1422 | [1: |
---|
1423 | >get_bit_addressable_sfr_status_of_pseudo_status |
---|
1424 | >map_bit_address_assm_1 |
---|
1425 | >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) % |
---|
1426 | |2: |
---|
1427 | whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta |
---|
1428 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
1429 | >map_bit_address_assm_1 |
---|
1430 | >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2) |
---|
1431 | >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); % |
---|
1432 | ] |
---|
1433 | ] |
---|
1434 | qed. |
---|