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