Context Navigation

Status.ma @ 1576

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

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

Download in other formats:

Original Format