Context Navigation

Status.ma @ 1174

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

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

Download in other formats:

Original Format