Context Navigation

Status.ma @ 1891

Last change on this file since 1891 was 1882, checked in by tranquil, 9 years ago
big update, alas incomplete: joint changed a bit, and all BE languages need to be updated started development of blocks to aid preservation results, but still incomplete if it breaks too many things, feel free to roll back
File size: 40.3 KB

Line
1	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2	(* Interpret.ma: Operational semantics for the 8051/8052 processor. *)
3	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5	include "ASM/ASM.ma".
6	include "ASM/Arithmetic.ma".
7	include "ASM/BitVectorTrie.ma".
8	include "basics/russell.ma".
9
10	definition Time ≝ nat.
11
12	inductive SerialBufferType: Type[0] ≝
13	Eight: Byte → SerialBufferType
14	\| Nine: Bit → Byte → SerialBufferType.
15
16	inductive LineType: Type[0] ≝
17	P1: Byte → LineType
18	\| P3: Byte → LineType
19	\| SerialBuffer: SerialBufferType → LineType.
20
21	(* What is a continuation, now? *)
22
23	inductive SFR8051: Type[0] ≝
24	SFR_SP: SFR8051
25	\| SFR_DPL: SFR8051
26	\| SFR_DPH: SFR8051
27	\| SFR_PCON: SFR8051
28	\| SFR_TCON: SFR8051
29	\| SFR_TMOD: SFR8051
30	\| SFR_TL0: SFR8051
31	\| SFR_TL1: SFR8051
32	\| SFR_TH0: SFR8051
33	\| SFR_TH1: SFR8051
34	\| SFR_P1: SFR8051
35	\| SFR_SCON: SFR8051
36	\| SFR_SBUF: SFR8051
37	\| SFR_IE: SFR8051
38	\| SFR_P3: SFR8051
39	\| SFR_IP: SFR8051
40	\| SFR_PSW: SFR8051
41	\| SFR_ACC_A: SFR8051
42	\| SFR_ACC_B: SFR8051.
43
44	definition sfr_8051_index ≝
45	λs: SFR8051.
46	match s with
47	[ SFR_SP ⇒ O
48	\| SFR_DPL ⇒ 1
49	\| SFR_DPH ⇒ 2
50	\| SFR_PCON ⇒ 3
51	\| SFR_TCON ⇒ 4
52	\| SFR_TMOD ⇒ 5
53	\| SFR_TL0 ⇒ 6
54	\| SFR_TL1 ⇒ 7
55	\| SFR_TH0 ⇒ 8
56	\| SFR_TH1 ⇒ 9
57	\| SFR_P1 ⇒ 10
58	\| SFR_SCON ⇒ 11
59	\| SFR_SBUF ⇒ 12
60	\| SFR_IE ⇒ 13
61	\| SFR_P3 ⇒ 14
62	\| SFR_IP ⇒ 15
63	\| SFR_PSW ⇒ 16
64	\| SFR_ACC_A ⇒ 17
65	\| SFR_ACC_B ⇒ 18
66	].
67
68	inductive SFR8052: Type[0] ≝
69	SFR_T2CON: SFR8052
70	\| SFR_RCAP2L: SFR8052
71	\| SFR_RCAP2H: SFR8052
72	\| SFR_TL2: SFR8052
73	\| SFR_TH2: SFR8052.
74
75	definition sfr_8052_index ≝
76	λs: SFR8052.
77	match s with
78	[ SFR_T2CON ⇒ O
79	\| SFR_RCAP2L ⇒ 1
80	\| SFR_RCAP2H ⇒ 2
81	\| SFR_TL2 ⇒ 3
82	\| SFR_TH2 ⇒ 4
83	].
84
85	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
86	(* Processor status. *)
87	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
88	record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝
89	{
90	low_internal_ram: BitVectorTrie Byte 7;
91	high_internal_ram: BitVectorTrie Byte 7;
92	external_ram: BitVectorTrie Byte 16;
93
94	program_counter: Word;
95
96	special_function_registers_8051: Vector Byte 19;
97	special_function_registers_8052: Vector Byte 5;
98
99	p1_latch: Byte;
100	p3_latch: Byte;
101
102	clock: Time
103	}.
104
105	definition Status ≝ PreStatus (BitVectorTrie Byte 16).
106	definition PseudoStatus ≝ PreStatus (pseudo_assembly_program).
107
108	lemma sfr8051_index_19:
109	∀i: SFR8051.
110	sfr_8051_index i < 19.
111	# i
112	cases i
113	normalize
114	repeat (@ le_S_S)
115	@ le_O_n
116	qed.
117
118	lemma sfr8052_index_5:
119	∀i: SFR8052.
120	sfr_8052_index i < 5.
121	# i
122	cases i
123	normalize
124	repeat (@ le_S_S)
125	@ le_O_n
126	qed.
127
128	definition set_clock ≝
129	λM: Type[0].
130	λcode_memory:M.
131	λs: PreStatus M code_memory.
132	λt: Time.
133	let old_low_internal_ram ≝ low_internal_ram ?? s in
134	let old_high_internal_ram ≝ high_internal_ram ?? s in
135	let old_external_ram ≝ external_ram ?? s in
136	let old_program_counter ≝ program_counter ?? s in
137	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
138	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
139	let old_p1_latch ≝ p1_latch ?? s in
140	let old_p3_latch ≝ p3_latch ?? s in
141	mk_PreStatus M code_memory
142	old_low_internal_ram
143	old_high_internal_ram
144	old_external_ram
145	old_program_counter
146	old_special_function_registers_8051
147	old_special_function_registers_8052
148	old_p1_latch
149	old_p3_latch
150	t.
151
152	definition set_p1_latch ≝
153	λM: Type[0].
154	λcode_memory:M.
155	λs: PreStatus M code_memory.
156	λb: Byte.
157	let old_low_internal_ram ≝ low_internal_ram ?? s in
158	let old_high_internal_ram ≝ high_internal_ram ?? s in
159	let old_external_ram ≝ external_ram ?? s in
160	let old_program_counter ≝ program_counter ?? s in
161	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
162	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
163	let old_p3_latch ≝ p3_latch ?? s in
164	let old_clock ≝ clock ?? s in
165	mk_PreStatus M code_memory
166	old_low_internal_ram
167	old_high_internal_ram
168	old_external_ram
169	old_program_counter
170	old_special_function_registers_8051
171	old_special_function_registers_8052
172	b
173	old_p3_latch
174	old_clock.
175
176	definition set_p3_latch ≝
177	λM: Type[0].
178	λcode_memory:M.
179	λs: PreStatus M code_memory.
180	λb: Byte.
181	let old_low_internal_ram ≝ low_internal_ram ?? s in
182	let old_high_internal_ram ≝ high_internal_ram ?? s in
183	let old_external_ram ≝ external_ram ?? s in
184	let old_program_counter ≝ program_counter ?? s in
185	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
186	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
187	let old_p1_latch ≝ p1_latch ?? s in
188	let old_clock ≝ clock ?? s in
189	mk_PreStatus M code_memory
190	old_low_internal_ram
191	old_high_internal_ram
192	old_external_ram
193	old_program_counter
194	old_special_function_registers_8051
195	old_special_function_registers_8052
196	old_p1_latch
197	b
198	old_clock.
199
200	definition get_8051_sfr ≝
201	λM: Type[0].
202	λcode_memory:M.
203	λs: PreStatus M code_memory.
204	λi: SFR8051.
205	let sfr ≝ special_function_registers_8051 ?? s in
206	let index ≝ sfr_8051_index i in
207	get_index_v … sfr index ?.
208	@ sfr8051_index_19
209	qed.
210
211	definition get_8052_sfr ≝
212	λM: Type[0].
213	λcode_memory:M.
214	λs: PreStatus M code_memory.
215	λi: SFR8052.
216	let sfr ≝ special_function_registers_8052 ?? s in
217	let index ≝ sfr_8052_index i in
218	get_index_v … sfr index ?.
219	@ sfr8052_index_5
220	qed.
221
222	definition set_8051_sfr ≝
223	λM: Type[0].
224	λcode_memory:M.
225	λs: PreStatus M code_memory.
226	λi: SFR8051.
227	λb: Byte.
228	let index ≝ sfr_8051_index i in
229	let old_low_internal_ram ≝ low_internal_ram ?? s in
230	let old_high_internal_ram ≝ high_internal_ram ?? s in
231	let old_external_ram ≝ external_ram ?? s in
232	let old_program_counter ≝ program_counter ?? s in
233	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
234	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
235	let new_special_function_registers_8051 ≝
236	set_index Byte 19 old_special_function_registers_8051 index b ? in
237	let old_p1_latch ≝ p1_latch ?? s in
238	let old_p3_latch ≝ p3_latch ?? s in
239	let old_clock ≝ clock ?? s in
240	mk_PreStatus M code_memory
241	old_low_internal_ram
242	old_high_internal_ram
243	old_external_ram
244	old_program_counter
245	new_special_function_registers_8051
246	old_special_function_registers_8052
247	old_p1_latch
248	old_p3_latch
249	old_clock.
250	@ (sfr8051_index_19 i)
251	qed.
252
253	definition set_8052_sfr ≝
254	λM: Type[0].
255	λcode_memory:M.
256	λs: PreStatus M code_memory.
257	λi: SFR8052.
258	λb: Byte.
259	let index ≝ sfr_8052_index i in
260	let old_low_internal_ram ≝ low_internal_ram ?? s in
261	let old_high_internal_ram ≝ high_internal_ram ?? s in
262	let old_external_ram ≝ external_ram ?? s in
263	let old_program_counter ≝ program_counter ?? s in
264	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
265	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
266	let new_special_function_registers_8052 ≝
267	set_index Byte 5 old_special_function_registers_8052 index b ? in
268	let old_p1_latch ≝ p1_latch ?? s in
269	let old_p3_latch ≝ p3_latch ?? s in
270	let old_clock ≝ clock ?? s in
271	mk_PreStatus M code_memory
272	old_low_internal_ram
273	old_high_internal_ram
274	old_external_ram
275	old_program_counter
276	old_special_function_registers_8051
277	new_special_function_registers_8052
278	old_p1_latch
279	old_p3_latch
280	old_clock.
281	@ (sfr8052_index_5 i)
282	qed.
283
284	definition set_program_counter ≝
285	λM: Type[0].
286	λcode_memory:M.
287	λs: PreStatus M code_memory.
288	λw: Word.
289	let old_low_internal_ram ≝ low_internal_ram ?? s in
290	let old_high_internal_ram ≝ high_internal_ram ?? s in
291	let old_external_ram ≝ external_ram ?? s in
292	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
293	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
294	let old_p1_latch ≝ p1_latch ?? s in
295	let old_p3_latch ≝ p3_latch ?? s in
296	let old_clock ≝ clock ?? s in
297	mk_PreStatus M code_memory
298	old_low_internal_ram
299	old_high_internal_ram
300	old_external_ram
301	w
302	old_special_function_registers_8051
303	old_special_function_registers_8052
304	old_p1_latch
305	old_p3_latch
306	old_clock.
307
308	definition set_code_memory ≝
309	λM,M': Type[0].
310	λcode_memory:M.
311	λs: PreStatus M code_memory.
312	λr: M'.
313	let old_low_internal_ram ≝ low_internal_ram ?? s in
314	let old_high_internal_ram ≝ high_internal_ram ?? s in
315	let old_external_ram ≝ external_ram ?? s in
316	let old_program_counter ≝ program_counter ?? s in
317	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
318	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
319	let old_p1_latch ≝ p1_latch ?? s in
320	let old_p3_latch ≝ p3_latch ?? s in
321	let old_clock ≝ clock ?? s in
322	mk_PreStatus M' r
323	old_low_internal_ram
324	old_high_internal_ram
325	old_external_ram
326	old_program_counter
327	old_special_function_registers_8051
328	old_special_function_registers_8052
329	old_p1_latch
330	old_p3_latch
331	old_clock.
332
333	definition set_low_internal_ram ≝
334	λM: Type[0].
335	λcode_memory:M.
336	λs: PreStatus M code_memory.
337	λr: BitVectorTrie Byte 7.
338	let old_high_internal_ram ≝ high_internal_ram ?? s in
339	let old_external_ram ≝ external_ram ?? s in
340	let old_program_counter ≝ program_counter ?? s in
341	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
342	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
343	let old_p1_latch ≝ p1_latch ?? s in
344	let old_p3_latch ≝ p3_latch ?? s in
345	let old_clock ≝ clock ?? s in
346	mk_PreStatus M code_memory
347	r
348	old_high_internal_ram
349	old_external_ram
350	old_program_counter
351	old_special_function_registers_8051
352	old_special_function_registers_8052
353	old_p1_latch
354	old_p3_latch
355	old_clock.
356
357	definition set_high_internal_ram ≝
358	λM: Type[0].
359	λcode_memory:M.
360	λs: PreStatus M code_memory.
361	λr: BitVectorTrie Byte 7.
362	let old_low_internal_ram ≝ low_internal_ram ?? s in
363	let old_high_internal_ram ≝ high_internal_ram ?? s in
364	let old_external_ram ≝ external_ram ?? s in
365	let old_program_counter ≝ program_counter ?? s in
366	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
367	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
368	let old_p1_latch ≝ p1_latch ?? s in
369	let old_p3_latch ≝ p3_latch ?? s in
370	let old_clock ≝ clock ?? s in
371	mk_PreStatus M code_memory
372	old_low_internal_ram
373	r
374	old_external_ram
375	old_program_counter
376	old_special_function_registers_8051
377	old_special_function_registers_8052
378	old_p1_latch
379	old_p3_latch
380	old_clock.
381
382	definition set_external_ram ≝
383	λM: Type[0].
384	λcode_memory:M.
385	λs: PreStatus M code_memory.
386	λr: BitVectorTrie Byte 16.
387	let old_low_internal_ram ≝ low_internal_ram ?? s in
388	let old_high_internal_ram ≝ high_internal_ram ?? s in
389	let old_program_counter ≝ program_counter ?? s in
390	let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
391	let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
392	let old_p1_latch ≝ p1_latch ?? s in
393	let old_p3_latch ≝ p3_latch ?? s in
394	let old_clock ≝ clock ?? s in
395	mk_PreStatus M code_memory
396	old_low_internal_ram
397	old_high_internal_ram
398	r
399	old_program_counter
400	old_special_function_registers_8051
401	old_special_function_registers_8052
402	old_p1_latch
403	old_p3_latch
404	old_clock.
405
406	definition get_cy_flag ≝
407	λM: Type[0].
408	λcode_memory:M.
409	λs: PreStatus M code_memory.
410	let sfr ≝ special_function_registers_8051 ?? s in
411	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
412	get_index_v bool 8 psw O ?.
413	normalize
414	@ (le_S_S ? ?)
415	[ @ le_O_n
416	\| repeat (@ (le_S_S));
417	//
418	]
419	qed.
420
421	definition get_ac_flag ≝
422	λM: Type[0].
423	λcode_memory:M.
424	λs: PreStatus M code_memory.
425	let sfr ≝ special_function_registers_8051 ?? s in
426	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
427	get_index_v bool 8 psw 1 ?.
428	normalize
429	repeat (@ (le_S_S ? ?))
430	@ le_O_n
431	qed.
432
433	definition get_fo_flag ≝
434	λM: Type[0].
435	λcode_memory:M.
436	λs: PreStatus M code_memory.
437	let sfr ≝ special_function_registers_8051 ?? s in
438	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
439	get_index_v bool 8 psw 2 ?.
440	normalize
441	repeat (@ (le_S_S ? ?))
442	@ le_O_n
443	qed.
444
445	definition get_rs1_flag ≝
446	λM: Type[0].
447	λcode_memory:M.
448	λs: PreStatus M code_memory.
449	let sfr ≝ special_function_registers_8051 ?? s in
450	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
451	get_index_v bool 8 psw 3 ?.
452	normalize
453	repeat (@ (le_S_S ? ?))
454	@ le_O_n
455	qed.
456
457	definition get_rs0_flag ≝
458	λM: Type[0].
459	λcode_memory:M.
460	λs: PreStatus M code_memory.
461	let sfr ≝ special_function_registers_8051 ?? s in
462	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
463	get_index_v bool 8 psw 4 ?.
464	normalize
465	repeat (@ (le_S_S ? ?))
466	@ le_O_n
467	qed.
468
469	definition get_ov_flag ≝
470	λM: Type[0].
471	λcode_memory:M.
472	λs: PreStatus M code_memory.
473	let sfr ≝ special_function_registers_8051 ?? s in
474	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
475	get_index_v bool 8 psw 5 ?.
476	normalize
477	repeat (@ (le_S_S ? ?))
478	@ le_O_n
479	qed.
480
481	definition get_ud_flag ≝
482	λM: Type[0].
483	λcode_memory:M.
484	λs: PreStatus M code_memory.
485	let sfr ≝ special_function_registers_8051 ?? s in
486	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
487	get_index_v bool 8 psw 6 ?.
488	normalize
489	repeat (@ (le_S_S ? ?))
490	@ le_O_n
491	qed.
492
493	definition get_p_flag ≝
494	λM: Type[0].
495	λcode_memory:M.
496	λs: PreStatus M code_memory.
497	let sfr ≝ special_function_registers_8051 ?? s in
498	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
499	get_index_v bool 8 psw 7 ?.
500	normalize
501	repeat (@ (le_S_S ? ?))
502	@ le_O_n
503	qed.
504
505	definition set_flags ≝
506	λM: Type[0].
507	λcode_memory:M.
508	λs: PreStatus M code_memory.
509	λcy: Bit.
510	λac: option Bit.
511	λov: Bit.
512	let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in
513	let old_cy ≝ get_index_v ?? sfr_psw O ? in
514	let old_ac ≝ get_index_v ?? sfr_psw 1 ? in
515	let old_fo ≝ get_index_v ?? sfr_psw 2 ? in
516	let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in
517	let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in
518	let old_ov ≝ get_index_v ?? sfr_psw 5 ? in
519	let old_ud ≝ get_index_v ?? sfr_psw 6 ? in
520	let old_p ≝ get_index_v ?? sfr_psw 7 ? in
521	let new_ac ≝ match ac with [ None ⇒ old_ac \| Some j ⇒ j ] in
522	set_8051_sfr ?? s SFR_PSW
523	[[ old_cy ; new_ac ; old_fo ; old_rs1 ;
524	old_rs0 ; old_ov ; old_ud ; old_p ]].
525	[1,2,3,4,5,6,7,8:
526	normalize
527	repeat (@ le_S_S)
528	@ le_O_n
529	]
530	qed.
531
532	definition initialise_status ≝
533	λM: Type[0].
534	λcode_mem: M.
535	let status ≝ mk_PreStatus M code_mem (* Code mem. *)
536	(Stub Byte 7) (* Low mem. *)
537	(Stub Byte 7) (* High mem. *)
538	(Stub Byte 16) (* Ext mem. *)
539	(zero 16) (* PC. *)
540	(replicate Byte 19 (zero 8)) (* 8051 SFR. *)
541	(replicate Byte 5 (zero 8)) (* 8052 SFR. *)
542	(zero 8) (* P1 latch. *)
543	(zero 8) (* P3 latch. *)
544	O (* Clock. *)
545	in
546	set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
547
548	definition get_bit_addressable_sfr ≝
549	λM: Type[0].
550	λcode_memory:M.
551	λs: PreStatus M code_memory.
552	λn: nat.
553	λb: BitVector n.
554	λl: bool.
555	let address ≝ nat_of_bitvector … b in
556	if (eqb address 128) then
557	?
558	else if (eqb address 144) then
559	if l then
560	(p1_latch ?? s)
561	else
562	(get_8051_sfr ?? s SFR_P1)
563	else if (eqb address 160) then
564	?
565	else if (eqb address 176) then
566	if l then
567	(p3_latch ?? s)
568	else
569	(get_8051_sfr ?? s SFR_P3)
570	else if (eqb address 153) then
571	get_8051_sfr ?? s SFR_SBUF
572	else if (eqb address 138) then
573	get_8051_sfr ?? s SFR_TL0
574	else if (eqb address 139) then
575	get_8051_sfr ?? s SFR_TL1
576	else if (eqb address 140) then
577	get_8051_sfr ?? s SFR_TH0
578	else if (eqb address 141) then
579	get_8051_sfr ?? s SFR_TH1
580	else if (eqb address 200) then
581	get_8052_sfr ?? s SFR_T2CON
582	else if (eqb address 202) then
583	get_8052_sfr ?? s SFR_RCAP2L
584	else if (eqb address 203) then
585	get_8052_sfr ?? s SFR_RCAP2H
586	else if (eqb address 204) then
587	get_8052_sfr ?? s SFR_TL2
588	else if (eqb address 205) then
589	get_8052_sfr ?? s SFR_TH2
590	else if (eqb address 135) then
591	get_8051_sfr ?? s SFR_PCON
592	else if (eqb address 136) then
593	get_8051_sfr ?? s SFR_TCON
594	else if (eqb address 137) then
595	get_8051_sfr ?? s SFR_TMOD
596	else if (eqb address 152) then
597	get_8051_sfr ?? s SFR_SCON
598	else if (eqb address 168) then
599	get_8051_sfr ?? s SFR_IE
600	else if (eqb address 184) then
601	get_8051_sfr ?? s SFR_IP
602	else if (eqb address 129) then
603	get_8051_sfr ?? s SFR_SP
604	else if (eqb address 130) then
605	get_8051_sfr ?? s SFR_DPL
606	else if (eqb address 131) then
607	get_8051_sfr ?? s SFR_DPH
608	else if (eqb address 208) then
609	get_8051_sfr ?? s SFR_PSW
610	else if (eqb address 224) then
611	get_8051_sfr ?? s SFR_ACC_A
612	else if (eqb address 240) then
613	get_8051_sfr ?? s SFR_ACC_B
614	else
615	?.
616	cases not_implemented
617	qed.
618
619	definition set_bit_addressable_sfr ≝
620	λM: Type[0].
621	λcode_memory:M.
622	λs: PreStatus M code_memory.
623	λb: Byte.
624	λv: Byte.
625	let address ≝ nat_of_bitvector … b in
626	if (eqb address 128) then
627	?
628	else if (eqb address 144) then
629	let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
630	let status_2 ≝ set_p1_latch ?? s v in
631	status_2
632	else if (eqb address 160) then
633	?
634	else if (eqb address 176) then
635	let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
636	let status_2 ≝ set_p3_latch ?? s v in
637	status_2
638	else if (eqb address 153) then
639	set_8051_sfr ?? s SFR_SBUF v
640	else if (eqb address 138) then
641	set_8051_sfr ?? s SFR_TL0 v
642	else if (eqb address 139) then
643	set_8051_sfr ?? s SFR_TL1 v
644	else if (eqb address 140) then
645	set_8051_sfr ?? s SFR_TH0 v
646	else if (eqb address 141) then
647	set_8051_sfr ?? s SFR_TH1 v
648	else if (eqb address 200) then
649	set_8052_sfr ?? s SFR_T2CON v
650	else if (eqb address 202) then
651	set_8052_sfr ?? s SFR_RCAP2L v
652	else if (eqb address 203) then
653	set_8052_sfr ?? s SFR_RCAP2H v
654	else if (eqb address 204) then
655	set_8052_sfr ?? s SFR_TL2 v
656	else if (eqb address 205) then
657	set_8052_sfr ?? s SFR_TH2 v
658	else if (eqb address 135) then
659	set_8051_sfr ?? s SFR_PCON v
660	else if (eqb address 136) then
661	set_8051_sfr ?? s SFR_TCON v
662	else if (eqb address 137) then
663	set_8051_sfr ?? s SFR_TMOD v
664	else if (eqb address 152) then
665	set_8051_sfr ?? s SFR_SCON v
666	else if (eqb address 168) then
667	set_8051_sfr ?? s SFR_IE v
668	else if (eqb address 184) then
669	set_8051_sfr ?? s SFR_IP v
670	else if (eqb address 129) then
671	set_8051_sfr ?? s SFR_SP v
672	else if (eqb address 130) then
673	set_8051_sfr ?? s SFR_DPL v
674	else if (eqb address 131) then
675	set_8051_sfr ?? s SFR_DPH v
676	else if (eqb address 208) then
677	set_8051_sfr ?? s SFR_PSW v
678	else if (eqb address 224) then
679	set_8051_sfr ?? s SFR_ACC_A v
680	else if (eqb address 240) then
681	set_8051_sfr ?? s SFR_ACC_B v
682	else
683	?.
684	cases not_implemented
685	qed.
686
687	definition bit_address_of_register ≝
688	λM: Type[0].
689	λcode_memory:M.
690	λs: PreStatus M code_memory.
691	λr: BitVector 3.
692	let b ≝ get_index_v … r O ? in
693	let c ≝ get_index_v … r 1 ? in
694	let d ≝ get_index_v … r 2 ? in
695	let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
696	let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
697	let offset ≝
698	if ¬r1 ∧ ¬r0 then
699	O
700	else if ¬r1 ∧ r0 then
701	8
702	else if r1 ∧ r0 then
703	24
704	else
705	16
706	in
707	bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
708	[1,2,3,4,5:
709	normalize
710	repeat (@ le_S_S)
711	@ le_O_n;
712	]
713	qed.
714
715	definition get_register ≝
716	λM: Type[0].
717	λcode_memory:M.
718	λs: PreStatus M code_memory.
719	λr: BitVector 3.
720	let address ≝ bit_address_of_register … s r in
721	lookup ?? address (low_internal_ram … s) (zero 8).
722
723	definition set_register ≝
724	λM: Type[0].
725	λcode_memory:M.
726	λs: PreStatus M code_memory.
727	λr: BitVector 3.
728	λv: Byte.
729	let address ≝ bit_address_of_register … s r in
730	let old_low_internal_ram ≝ low_internal_ram ?? s in
731	let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
732	set_low_internal_ram … s new_low_internal_ram.
733
734	definition read_at_stack_pointer ≝
735	λM: Type[0].
736	λcode_memory:M.
737	λs: PreStatus M code_memory.
738	let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
739	let m ≝ get_index_v ?? nu O ? in
740	let r1 ≝ get_index_v ?? nu 1 ? in
741	let r2 ≝ get_index_v ?? nu 2 ? in
742	let r3 ≝ get_index_v ?? nu 3 ? in
743	let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
744	let memory ≝
745	if m then
746	(low_internal_ram ?? s)
747	else
748	(high_internal_ram ?? s)
749	in
750	lookup … address memory (zero 8).
751	[1,2,3,4:
752	normalize
753	repeat (@ le_S_S)
754	@ le_O_n
755	]
756	qed.
757
758	definition write_at_stack_pointer ≝
759	λM: Type[0].
760	λcode_memory:M.
761	λs: PreStatus M code_memory.
762	λv: Byte.
763	let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
764	let bit_zero ≝ get_index_v ?? nu O ? in
765	let bit_1 ≝ get_index_v ?? nu 1 ? in
766	let bit_2 ≝ get_index_v ?? nu 2 ? in
767	let bit_3 ≝ get_index_v ?? nu 3 ? in
768	if bit_zero then
769	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
770	v (low_internal_ram ?? s) in
771	set_low_internal_ram ?? s memory
772	else
773	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
774	v (high_internal_ram ?? s) in
775	set_high_internal_ram ?? s memory.
776	[1,2,3,4:
777	normalize
778	repeat (@ le_S_S)
779	@ le_O_n
780	]
781	qed.
782
783	definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝
784	λM,code_memory,s,v,a.
785	match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
786	[ DPTR ⇒ λ_:True.
787	let 〈 bu, bl 〉 ≝ split … 8 8 v in
788	let status ≝ set_8051_sfr … s SFR_DPH bu in
789	let status ≝ set_8051_sfr … status SFR_DPL bl in
790	status
791	\| _ ⇒ λK.
792	match K in False with
793	[
794	]
795	] (subaddressing_modein … a).
796	//
797	qed.
798
799	definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
800	set_arg_16'.
801
802	lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
803	#M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
804	qed.
805
806
807	definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
808	λm, cm, s, a.
809	match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
810	[ DATA16 d ⇒ λ_:True. d
811	\| _ ⇒ λK.
812	match K in False with
813	[
814	]
815	] (subaddressing_modein … a).
816
817	definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
818	acc_a ; acc_b ; data ; acc_dptr ;
819	acc_pc ; ext_indirect ;
820	ext_indirect_dptr ]] → Byte ≝
821	λm, cm, s, l, a.
822	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
823	acc_a ; acc_b ; data ; acc_dptr ;
824	acc_pc ; ext_indirect ;
825	ext_indirect_dptr ]] x) → ? with
826	[ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
827	\| ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
828	\| DATA d ⇒ λdata: True. d
829	\| REGISTER r ⇒ λregister: True. get_register ?? s r
830	\| EXT_INDIRECT_DPTR ⇒
831	λext_indirect_dptr: True.
832	let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
833	lookup ? 16 address (external_ram ?? s) (zero 8)
834	\| EXT_INDIRECT e ⇒
835	λext_indirect: True.
836	let address ≝ get_register ?? s [[ false; false; e ]] in
837	let padded_address ≝ pad 8 8 address in
838	lookup ? 16 padded_address (external_ram ?? s) (zero 8)
839	\| ACC_DPTR ⇒
840	λacc_dptr: True.
841	let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
842	let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
843	let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
844	lookup ? 16 address (external_ram ?? s) (zero 8)
845	\| ACC_PC ⇒
846	λacc_pc: True.
847	let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
848	let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
849	lookup ? 16 address (external_ram ?? s) (zero 8)
850	\| DIRECT d ⇒
851	λdirect: True.
852	let 〈 nu, nl 〉 ≝ split ? 4 4 d in
853	let bit_one ≝ get_index_v ? ? nu 0 ? in
854	let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
855	match bit_one with
856	[ false ⇒
857	let address ≝ three_bits @@ nl in
858	lookup ? 7 address (low_internal_ram ?? s) (zero 8)
859	\| true ⇒ get_bit_addressable_sfr ?? s 8 d l
860	]
861	\| INDIRECT i ⇒
862	λindirect: True.
863	let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
864	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
865	let bit_1 ≝ get_index_v ?? bit_one_v O ? in
866	match bit_1 with
867	[ false ⇒
868	lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
869	\| true ⇒
870	lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
871	]
872	\| _ ⇒ λother.
873	match other in False with [ ]
874	] (subaddressing_modein … a).
875	[1,2:
876	normalize
877	repeat (@ le_S_S)
878	@ le_O_n
879	]
880	qed.
881
882	axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
883
884	definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
885	acc_a ; acc_b ; ext_indirect ;
886	ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
887	clock … code_memory s = clock … code_memory s' ≝
888	λm, cm, s, a, v.
889	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
890	acc_a ; acc_b ; ext_indirect ;
891	ext_indirect_dptr ]] x) →
892	Σs':PreStatus m cm. clock m cm s = clock m cm s'
893	(CSC: bug here if one specified the two clock above)
894	with
895	[ DIRECT d ⇒
896	λdirect: True.
897	let 〈 nu, nl 〉 ≝ split … 4 4 d in
898	let bit_one ≝ get_index_v ? ? nu 0 ? in
899	let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
900	match bit_one with
901	[ true ⇒ set_bit_addressable_sfr ?? s d v
902	\| false ⇒
903	let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
904	set_low_internal_ram ?? s memory
905	]
906	\| INDIRECT i ⇒
907	λindirect: True.
908	let register ≝ get_register ?? s [[ false; false; i ]] in
909	let 〈nu, nl〉 ≝ split ? 4 4 register in
910	let bit_1 ≝ get_index_v … nu 0 ? in
911	let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
912	match bit_1 with
913	[ false ⇒
914	let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
915	set_low_internal_ram ?? s memory
916	\| true ⇒
917	let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
918	set_high_internal_ram ?? s memory
919	]
920	\| REGISTER r ⇒ λregister: True. set_register ?? s r v
921	\| ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
922	\| ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
923	\| EXT_INDIRECT e ⇒
924	λext_indirect: True.
925	let address ≝ get_register ?? s [[ false; false; e ]] in
926	let padded_address ≝ pad 8 8 address in
927	let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
928	set_external_ram ?? s memory
929	\| EXT_INDIRECT_DPTR ⇒
930	λext_indirect_dptr: True.
931	let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
932	let memory ≝ insert ? 16 address v (external_ram ?? s) in
933	set_external_ram ?? s memory
934	\| _ ⇒
935	λother: False.
936	match other in False with [ ]
937	] (subaddressing_modein … a).
938	// qed.
939
940	definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝
941	set_arg_8'.
942
943	lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
944	#M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
945	qed.
946
947	theorem modulus_less_than:
948	∀m,n: nat. (m mod (S n)) < S n.
949	#n #m
950	normalize
951	@ le_S_S
952	lapply (le_n n)
953	generalize in ⊢ (?%? → ?(??%?)?);
954	elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
955	[ normalize
956	#n
957	@ (less_than_or_equal_b_elim n m)
958	normalize
959	[ //
960	\| #H #K
961	@(le_inv_ind ?? K …)
962	[ # H1
963	< H1
964	//
965	\| #x #H1 #H2 #H3
966	destruct
967	]
968	]
969	\| normalize
970	# y # H1 # n # H2
971	@ (less_than_or_equal_b_elim n m)
972	normalize
973	[ //
974	\| # K
975	@ H1
976	cut (n ≤ S y → n - S m ≤ y)
977	/2 by/
978	cases n
979	normalize
980	//
981	# x # K1
982	lapply (le_S_S_to_le … K1)
983	generalize in match m;
984	elim x
985	normalize
986	//
987	# w1 # H # m
988	cases m
989	normalize
990	//
991	# q # K2
992	@H
993	/3/
994	]
995	]
996	qed.
997
998	definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
999	bool → bool ≝
1000	λm, cm, s, a, l.
1001	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1002	n_bit_addr ;
1003	carry ]] x) → ? with
1004	[ BIT_ADDR b ⇒
1005	λbit_addr: True.
1006	let 〈 nu, nl 〉 ≝ split … 4 4 b in
1007	let bit_1 ≝ get_index_v ? ? nu 0 ? in
1008	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
1009	match bit_1 with
1010	[ true ⇒
1011	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1012	let d ≝ address ÷ 8 in
1013	let m ≝ address mod 8 in
1014	let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1015	let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
1016	get_index_v … sfr m ?
1017	\| false ⇒
1018	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1019	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1020	let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1021	get_index_v … t (modulus address 8) ?
1022	]
1023	\| N_BIT_ADDR n ⇒
1024	λn_bit_addr: True.
1025	let 〈 nu, nl 〉 ≝ split … 4 4 n in
1026	let bit_1 ≝ get_index_v ? ? nu 0 ? in
1027	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
1028	match bit_1 with
1029	[ true ⇒
1030	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1031	let d ≝ address ÷ 8 in
1032	let m ≝ address mod 8 in
1033	let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1034	let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
1035	¬(get_index_v … sfr m ?)
1036	\| false ⇒
1037	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1038	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1039	let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1040	¬(get_index_v … trans (modulus address 8) ?)
1041	]
1042	\| CARRY ⇒ λcarry: True. get_cy_flag ?? s
1043	\| _ ⇒ λother.
1044	match other in False with [ ]
1045	] (subaddressing_modein … a).
1046	[3,6:
1047	normalize
1048	repeat (@ le_S_S)
1049	@ le_O_n
1050	\|1,2,4,5:
1051	@modulus_less_than
1052	]
1053	qed.
1054
1055	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' ≝
1056	λm: Type[0].
1057	λcm.
1058	λs: PreStatus m cm.
1059	λa: [[bit_addr; carry]].
1060	λv: Bit.
1061	match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
1062	[ BIT_ADDR b ⇒ λbit_addr: True.
1063	let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
1064	let bit_1 ≝ get_index_v ?? nu 0 ? in
1065	let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
1066	match bit_1 return λ_. ? with
1067	[ true ⇒
1068	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1069	let d ≝ address ÷ 8 in
1070	let m ≝ address mod 8 in
1071	let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1072	let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
1073	let new_sfr ≝ set_index … sfr m v ? in
1074	set_bit_addressable_sfr ?? s new_sfr t
1075	\| false ⇒
1076	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1077	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1078	let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1079	let n_bit ≝ set_index … t (modulus address 8) v ? in
1080	let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1081	set_low_internal_ram ?? s memory
1082	]
1083	\| CARRY ⇒
1084	λcarry: True.
1085	let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
1086	let bit_1 ≝ get_index_v… nu 1 ? in
1087	let bit_2 ≝ get_index_v… nu 2 ? in
1088	let bit_3 ≝ get_index_v… nu 3 ? in
1089	let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
1090	set_8051_sfr ?? s SFR_PSW new_psw
1091	\| _ ⇒
1092	λother: False.
1093	match other in False with
1094	[ ]
1095	] (subaddressing_modein … a).
1096	try (repeat @le_S_S @le_O_n)
1097	/by/
1098	qed.
1099
1100	definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
1101
1102	lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
1103	#M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2
1104	qed.
1105
1106	definition load_code_memory ≝
1107	fold_left_i … (
1108	λi, mem, v.
1109	insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
1110
1111	definition load ≝
1112	λl,cm.
1113	λstatus.
1114	set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
1115
1116	definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
1117	λcode_mem.
1118	λpc: Word.
1119	let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
1120	let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
1121	〈instr, new_pc〉.
1122	cases not_implemented.
1123	qed.
1124
1125	lemma snd_fetch_pseudo_instruction:
1126	∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
1127	#l #ppc whd in ⊢ (??(???%)?); @pair_elim
1128	#lft #rgt @pair_elim #x #y #_ #_ %
1129	qed.
1130
1131	definition address_of_word_labels_code_mem ≝
1132	λcode_mem : list labelled_instruction.
1133	λid: Identifier.
1134	bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
1135
1136	lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1137	occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
1138	address_of_word_labels_code_mem instr_list id =
1139	address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1140	#i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1141	>(index_of_internal_None ?????? H) %
1142	qed.
1143
1144	lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1145	eq_identifier ? id' id = false →
1146	occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
1147	address_of_word_labels_code_mem instr_list id =
1148	address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1149	#i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1150	>(index_of_internal_Some_miss ???????? H) [ @refl \| // ]
1151	qed.
1152
1153	lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1154	occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
1155	address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1156	= bitvector_of_nat … (\|instr_list\|).
1157	#i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
1158	>(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
1159	qed.
1160
1161	definition address_of_word_labels ≝
1162	λpr: pseudo_assembly_program.
1163	λid: Identifier.
1164	address_of_word_labels_code_mem (\snd pr) id.
1165
1166	definition construct_datalabels: preamble → ? ≝
1167	λthe_preamble: preamble.
1168	\fst (foldl ((identifier_map ASMTag Word) × Word) ? (
1169	λt. λpreamble.
1170	let 〈datalabels, addr〉 ≝ t in
1171	let 〈name, size〉 ≝ preamble in
1172	let 〈carry, sum〉 ≝ half_add … addr size in
1173	〈add ? ? datalabels name addr, sum〉)
1174	〈empty_map …, zero 16〉 (\snd the_preamble)).

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format