Context Navigation

AssemblyProof.ma @ 991

Last change on this file since 991 was 991, checked in by mulligan, 8 years ago
loads of axioms related to equality on instructions closed
File size: 96.4 KB

Line
1	include "ASM/Assembly.ma".
2	include "ASM/Interpret.ma".
3
4	definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
5	λP.
6	P true ∧ P false.
7
8	let rec bitvector_elim_prop_internal
9	(n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
10	match m return λm. m ≤ n → BitVector (n - m) → Prop with
11	[ O ⇒ λprf1. λprefix. P ?
12	\| S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
13	].
14	[ applyS prefix
15	\| letin res ≝ (bit ::: prefix)
16	< (minus_S_S ? ?)
17	> (minus_Sn_m ? ?)
18	[ @ res
19	\| @ prf2
20	]
21	\| /2/
22	].
23	qed.
24
25	definition bitvector_elim_prop ≝
26	λn: nat.
27	λP: BitVector n → Prop.
28	bitvector_elim_prop_internal n P n ? ?.
29	[ @ (le_n ?)
30	\| < (minus_n_n ?)
31	@ [[ ]]
32	]
33	qed.
34
35	lemma bool_eq_internal_eq:
36	∀b, c.
37	(λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
38	#b #c
39	cases b
40	[ normalize //
41	\| normalize
42	cases c
43	[ normalize //
44	\| normalize //
45	]
46	]
47	qed.
48
49	definition bit_elim: ∀P: bool → bool. bool ≝
50	λP.
51	P true ∧ P false.
52
53	let rec bitvector_elim_internal
54	(n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
55	match m return λm. m ≤ n → BitVector (n - m) → bool with
56	[ O ⇒ λprf1. λprefix. P ?
57	\| S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
58	].
59	[ applyS prefix
60	\| letin res ≝ (bit ::: prefix)
61	< (minus_S_S ? ?)
62	> (minus_Sn_m ? ?)
63	[ @ res
64	\| @ prf2
65	]
66	\| /2/
67	].
68	qed.
69
70	definition bitvector_elim ≝
71	λn: nat.
72	λP: BitVector n → bool.
73	bitvector_elim_internal n P n ? ?.
74	[ @ (le_n ?)
75	\| < (minus_n_n ?)
76	@ [[ ]]
77	]
78	qed.
79
80	axiom vector_associative_append:
81	∀A: Type[0].
82	∀n, m, o: nat.
83	∀v: Vector A n.
84	∀q: Vector A m.
85	∀r: Vector A o.
86	((v @@ q) @@ r)
87	≃
88	(v @@ (q @@ r)).
89
90	lemma vector_cons_append:
91	∀A: Type[0].
92	∀n: nat.
93	∀e: A.
94	∀v: Vector A n.
95	e ::: v = [[ e ]] @@ v.
96	# A # N # E # V
97	elim V
98	[ normalize %
99	\| # NN # AA # VV # IH
100	normalize
101	%
102	]
103	qed.
104
105	lemma super_rewrite2:
106	∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
107	∀P: ∀m. Vector A m → Prop.
108	n=m → v1 ≃ v2 → P n v1 → P m v2.
109	#A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
110	qed.
111
112	lemma mem_middle_vector:
113	∀A: Type[0].
114	∀m, o: nat.
115	∀eq: A → A → bool.
116	∀reflex: ∀a. eq a a = true.
117	∀p: Vector A m.
118	∀a: A.
119	∀r: Vector A o.
120	mem A eq ? (p@@(a:::r)) a = true.
121	# A # M # O # EQ # REFLEX # P # A
122	elim P
123	[ normalize
124	> (REFLEX A)
125	normalize
126	# H
127	%
128	\| # NN # AA # PP # IH
129	normalize
130	cases (EQ A AA) //
131	@ IH
132	]
133	qed.
134
135	lemma mem_monotonic_wrt_append:
136	∀A: Type[0].
137	∀m, o: nat.
138	∀eq: A → A → bool.
139	∀reflex: ∀a. eq a a = true.
140	∀p: Vector A m.
141	∀a: A.
142	∀r: Vector A o.
143	mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
144	# A # M # O # EQ # REFLEX # P # A
145	elim P
146	[ #R #H @H
147	\| #NN #AA # PP # IH #R #H
148	normalize
149	cases (EQ A AA)
150	[ normalize %
151	\| @ IH @ H
152	]
153	]
154	qed.
155
156	lemma subvector_multiple_append:
157	∀A: Type[0].
158	∀o, n: nat.
159	∀eq: A → A → bool.
160	∀refl: ∀a. eq a a = true.
161	∀h: Vector A o.
162	∀v: Vector A n.
163	∀m: nat.
164	∀q: Vector A m.
165	bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
166	# A # O # N # EQ # REFLEX # H # V
167	elim V
168	[ normalize
169	# M # V %
170	\| # NN # AA # VV # IH # MM # QQ
171	change with (bool_to_Prop (andb ??))
172	cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
173	[
174	\| # HH > HH
175	> (vector_cons_append ? ? AA VV)
176	change with (bool_to_Prop (subvector_with ??????))
177	@(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
178	(λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
179	?
180	(vector_associative_append A ? ? ? QQ [[AA]] VV))
181	[ >associative_plus //
182	\| @IH ]
183	]
184	@(mem_monotonic_wrt_append)
185	[ @ REFLEX
186	\| @(mem_monotonic_wrt_append)
187	[ @ REFLEX
188	\| normalize
189	> REFLEX
190	normalize
191	%
192	]
193	]
194	qed.
195
196	lemma vector_cons_empty:
197	∀A: Type[0].
198	∀n: nat.
199	∀v: Vector A n.
200	[[ ]] @@ v = v.
201	# A # N # V
202	elim V
203	[ normalize %
204	\| # NN # HH # VV #H %
205	]
206	qed.
207
208	corollary subvector_hd_tl:
209	∀A: Type[0].
210	∀o: nat.
211	∀eq: A → A → bool.
212	∀refl: ∀a. eq a a = true.
213	∀h: A.
214	∀v: Vector A o.
215	bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
216	# A # O # EQ # REFLEX # H # V
217	> (vector_cons_append A ? H V)
218	< (vector_cons_empty A ? ([[H]] @@ V))
219	@ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
220	qed.
221
222	lemma eq_a_reflexive:
223	∀a. eq_a a a = true.
224	# A
225	cases A
226	%
227	qed.
228
229	lemma is_in_monotonic_wrt_append:
230	∀m, n: nat.
231	∀p: Vector addressing_mode_tag m.
232	∀q: Vector addressing_mode_tag n.
233	∀to_search: addressing_mode.
234	bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
235	# M # N # P # Q # TO_SEARCH
236	# H
237	elim Q
238	[ normalize
239	@ H
240	\| # NN # PP # QQ # IH
241	normalize
242	cases (is_a PP TO_SEARCH)
243	[ normalize
244	%
245	\| normalize
246	normalize in IH
247	@ IH
248	]
249	]
250	qed.
251
252	corollary is_in_hd_tl:
253	∀to_search: addressing_mode.
254	∀hd: addressing_mode_tag.
255	∀n: nat.
256	∀v: Vector addressing_mode_tag n.
257	bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
258	# TO_SEARCH # HD # N # V
259	elim V
260	[ # H
261	normalize in H;
262	cases H
263	\| # NN # HHD # VV # IH # HH
264	> vector_cons_append
265	> (vector_cons_append ? ? HHD VV)
266	@ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
267	@ HH
268	]
269	qed.
270
271	let rec list_addressing_mode_tags_elim
272	(n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
273	match l return λx.match x with [O ⇒ λl: Vector … O. bool \| S x' ⇒ λl: Vector addressing_mode_tag (S x').
274	(l → bool) → bool ] with
275	[ VEmpty ⇒ true
276	\| VCons len hd tl ⇒ λP.
277	let process_hd ≝
278	match hd return λhd. ∀P: hd:::tl → bool. bool with
279	[ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
280	\| indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
281	\| ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
282	\| registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
283	\| acc_a ⇒ λP.P ACC_A
284	\| acc_b ⇒ λP.P ACC_B
285	\| dptr ⇒ λP.P DPTR
286	\| data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
287	\| data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
288	\| acc_dptr ⇒ λP.P ACC_DPTR
289	\| acc_pc ⇒ λP.P ACC_PC
290	\| ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
291	\| indirect_dptr ⇒ λP.P INDIRECT_DPTR
292	\| carry ⇒ λP.P CARRY
293	\| bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
294	\| n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
295	\| relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
296	\| addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
297	\| addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
298	]
299	in
300	andb (process_hd P)
301	(match len return λx. x = len → bool with
302	[ O ⇒ λprf. true
303	\| S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
304	].
305	try %
306	[ 2: cases (sym_eq ??? prf); @tl
307	\| generalize in match H; generalize in match tl; cases prf;
308	(* cases prf in tl H; : ??? WAS WORKING BEFORE *)
309	#tl
310	normalize in ⊢ (∀_: %. ?)
311	# H
312	whd
313	normalize in ⊢ (match % with [ _ ⇒ ? \| _ ⇒ ?])
314	cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
315	qed.
316
317	definition product_elim ≝
318	λm, n: nat.
319	λv: Vector addressing_mode_tag (S m).
320	λq: Vector addressing_mode_tag (S n).
321	λP: (v × q) → bool.
322	list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
323
324	definition union_elim ≝
325	λA, B: Type[0].
326	λelimA: (A → bool) → bool.
327	λelimB: (B → bool) → bool.
328	λelimU: A ⊎ B → bool.
329	elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
330
331	(*
332	definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
333	λP.
334	list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
335	list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
336	list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
337	list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
338	list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
339	list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
340	list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
341	list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
342	list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
343	list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
344	P (DA ? ACC_A) ∧
345	bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
346	bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
347	bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
348	bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
349	bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
350	bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
351	bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
352	list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
353	P (RL ? ACC_A) ∧
354	P (RLC ? ACC_A) ∧
355	P (RR ? ACC_A) ∧
356	P (RRC ? ACC_A) ∧
357	P (SWAP ? ACC_A) ∧
358	P (RET ?) ∧
359	P (RETI ?) ∧
360	P (NOP ?) ∧
361	bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
362	list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
363	bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
364	bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
365	union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
366	(product_elim ? ? [[ registr; indirect ]] [[ data ]])
367	(λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
368	list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
369	union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
370	(product_elim ? ? [[direct]] [[ acc_a ; data ]])
371	(λd. P (XRL ? d)) ∧
372	union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
373	(product_elim ? ? [[direct]] [[ acc_a ; data ]]))
374	(product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
375	(λd. P (ANL ? d)) ∧
376	union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
377	(product_elim ? ? [[direct]] [[ acc_a ; data ]]))
378	(product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
379	(λd. P (ORL ? d)) ∧
380	union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
381	(product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
382	(λd. P (MOVX ? d)) ∧
383	union_elim ? ? (
384	union_elim ? ? (
385	union_elim ? ? (
386	union_elim ? ? (
387	union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
388	(product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
389	(product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
390	(product_elim ? ? [[dptr]] [[data16]]))
391	(product_elim ? ? [[carry]] [[bit_addr]]))
392	(product_elim ? ? [[bit_addr]] [[carry]])
393	(λd. P (MOV ? d)).
394	%
395	qed.
396
397	definition instruction_elim: ∀P: instruction → bool. bool ≝
398	λP. (*
399	bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
400	bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
401	bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
402	bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
403	bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (* ∧
404	P (JMP INDIRECT_DPTR) ∧
405	list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
406	preinstruction_elim (λp. P (RealInstruction p)). *)
407	%
408	qed.
409
410
411	axiom instruction_elim_complete:
412	∀P. instruction_elim P = true → ∀i. P i = true.
413	*)
414	(*definition eq_instruction ≝
415	λi, j: instruction.
416	true.*)
417
418	definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
419	λa, b: addressing_mode.
420	match a with
421	[ DIRECT d ⇒
422	match b with
423	[ DIRECT e ⇒ eq_bv ? d e
424	\| _ ⇒ false
425	]
426	\| INDIRECT b' ⇒
427	match b with
428	[ INDIRECT e ⇒ eq_b b' e
429	\| _ ⇒ false
430	]
431	\| EXT_INDIRECT b' ⇒
432	match b with
433	[ EXT_INDIRECT e ⇒ eq_b b' e
434	\| _ ⇒ false
435	]
436	\| REGISTER bv ⇒
437	match b with
438	[ REGISTER bv' ⇒ eq_bv ? bv bv'
439	\| _ ⇒ false
440	]
441	\| ACC_A ⇒ match b with [ ACC_A ⇒ true \| _ ⇒ false ]
442	\| ACC_B ⇒ match b with [ ACC_B ⇒ true \| _ ⇒ false ]
443	\| DPTR ⇒ match b with [ DPTR ⇒ true \| _ ⇒ false ]
444	\| DATA b' ⇒
445	match b with
446	[ DATA e ⇒ eq_bv ? b' e
447	\| _ ⇒ false
448	]
449	\| DATA16 w ⇒
450	match b with
451	[ DATA16 e ⇒ eq_bv ? w e
452	\| _ ⇒ false
453	]
454	\| ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true \| _ ⇒ false ]
455	\| ACC_PC ⇒ match b with [ ACC_PC ⇒ true \| _ ⇒ false ]
456	\| EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
457	\| INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
458	\| CARRY ⇒ match b with [ CARRY ⇒ true \| _ ⇒ false ]
459	\| BIT_ADDR b' ⇒
460	match b with
461	[ BIT_ADDR e ⇒ eq_bv ? b' e
462	\| _ ⇒ false
463	]
464	\| N_BIT_ADDR b' ⇒
465	match b with
466	[ N_BIT_ADDR e ⇒ eq_bv ? b' e
467	\| _ ⇒ false
468	]
469	\| RELATIVE n ⇒
470	match b with
471	[ RELATIVE e ⇒ eq_bv ? n e
472	\| _ ⇒ false
473	]
474	\| ADDR11 w ⇒
475	match b with
476	[ ADDR11 e ⇒ eq_bv ? w e
477	\| _ ⇒ false
478	]
479	\| ADDR16 w ⇒
480	match b with
481	[ ADDR16 e ⇒ eq_bv ? w e
482	\| _ ⇒ false
483	]
484	].
485
486	lemma eq_bv_refl:
487	∀n, b.
488	eq_bv n b b = true.
489	#n #b cases b //
490	qed.
491
492	lemma eq_b_refl:
493	∀b.
494	eq_b b b = true.
495	#b cases b //
496	qed.
497
498	lemma eq_addressing_mode_refl:
499	∀a. eq_addressing_mode a a = true.
500	#a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl
501	try normalize %
502	qed.
503
504	definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
505	λlt, rt, leq, req, left, right.
506	match left with
507	[ inl l ⇒
508	match right with
509	[ inl l' ⇒ leq l l'
510	\| _ ⇒ false
511	]
512	\| inr r ⇒
513	match right with
514	[ inr r' ⇒ req r r'
515	\| _ ⇒ false
516	]
517	].
518
519	definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
520	λlt, rt, leq, req, left, right.
521	let 〈l, r〉 ≝ left in
522	let 〈l', r'〉 ≝ right in
523	leq l l' ∧ req r r'.
524
525	definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
526	λi, j.
527	match i with
528	[ ADD arg1 arg2 ⇒
529	match j with
530	[ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
531	\| _ ⇒ false
532	]
533	\| ADDC arg1 arg2 ⇒
534	match j with
535	[ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
536	\| _ ⇒ false
537	]
538	\| SUBB arg1 arg2 ⇒
539	match j with
540	[ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
541	\| _ ⇒ false
542	]
543	\| INC arg ⇒
544	match j with
545	[ INC arg' ⇒ eq_addressing_mode arg arg'
546	\| _ ⇒ false
547	]
548	\| DEC arg ⇒
549	match j with
550	[ DEC arg' ⇒ eq_addressing_mode arg arg'
551	\| _ ⇒ false
552	]
553	\| MUL arg1 arg2 ⇒
554	match j with
555	[ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
556	\| _ ⇒ false
557	]
558	\| DIV arg1 arg2 ⇒
559	match j with
560	[ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
561	\| _ ⇒ false
562	]
563	\| DA arg ⇒
564	match j with
565	[ DA arg' ⇒ eq_addressing_mode arg arg'
566	\| _ ⇒ false
567	]
568	\| JC arg ⇒
569	match j with
570	[ JC arg' ⇒ eq_addressing_mode arg arg'
571	\| _ ⇒ false
572	]
573	\| JNC arg ⇒
574	match j with
575	[ JNC arg' ⇒ eq_addressing_mode arg arg'
576	\| _ ⇒ false
577	]
578	\| JB arg1 arg2 ⇒
579	match j with
580	[ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
581	\| _ ⇒ false
582	]
583	\| JNB arg1 arg2 ⇒
584	match j with
585	[ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
586	\| _ ⇒ false
587	]
588	\| JBC arg1 arg2 ⇒
589	match j with
590	[ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
591	\| _ ⇒ false
592	]
593	\| JZ arg ⇒
594	match j with
595	[ JZ arg' ⇒ eq_addressing_mode arg arg'
596	\| _ ⇒ false
597	]
598	\| JNZ arg ⇒
599	match j with
600	[ JNZ arg' ⇒ eq_addressing_mode arg arg'
601	\| _ ⇒ false
602	]
603	\| CJNE arg1 arg2 ⇒
604	match j with
605	[ CJNE arg1' arg2' ⇒
606	let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
607	let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
608	let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
609	arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
610	\| _ ⇒ false
611	]
612	\| DJNZ arg1 arg2 ⇒
613	match j with
614	[ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
615	\| _ ⇒ false
616	]
617	\| CLR arg ⇒
618	match j with
619	[ CLR arg' ⇒ eq_addressing_mode arg arg'
620	\| _ ⇒ false
621	]
622	\| CPL arg ⇒
623	match j with
624	[ CPL arg' ⇒ eq_addressing_mode arg arg'
625	\| _ ⇒ false
626	]
627	\| RL arg ⇒
628	match j with
629	[ RL arg' ⇒ eq_addressing_mode arg arg'
630	\| _ ⇒ false
631	]
632	\| RLC arg ⇒
633	match j with
634	[ RLC arg' ⇒ eq_addressing_mode arg arg'
635	\| _ ⇒ false
636	]
637	\| RR arg ⇒
638	match j with
639	[ RR arg' ⇒ eq_addressing_mode arg arg'
640	\| _ ⇒ false
641	]
642	\| RRC arg ⇒
643	match j with
644	[ RRC arg' ⇒ eq_addressing_mode arg arg'
645	\| _ ⇒ false
646	]
647	\| SWAP arg ⇒
648	match j with
649	[ SWAP arg' ⇒ eq_addressing_mode arg arg'
650	\| _ ⇒ false
651	]
652	\| SETB arg ⇒
653	match j with
654	[ SETB arg' ⇒ eq_addressing_mode arg arg'
655	\| _ ⇒ false
656	]
657	\| PUSH arg ⇒
658	match j with
659	[ PUSH arg' ⇒ eq_addressing_mode arg arg'
660	\| _ ⇒ false
661	]
662	\| POP arg ⇒
663	match j with
664	[ POP arg' ⇒ eq_addressing_mode arg arg'
665	\| _ ⇒ false
666	]
667	\| XCH arg1 arg2 ⇒
668	match j with
669	[ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
670	\| _ ⇒ false
671	]
672	\| XCHD arg1 arg2 ⇒
673	match j with
674	[ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
675	\| _ ⇒ false
676	]
677	\| RET ⇒ match j with [ RET ⇒ true \| _ ⇒ false ]
678	\| RETI ⇒ match j with [ RETI ⇒ true \| _ ⇒ false ]
679	\| NOP ⇒ match j with [ NOP ⇒ true \| _ ⇒ false ]
680	\| MOVX arg ⇒
681	match j with
682	[ MOVX arg' ⇒
683	let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
684	let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
685	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
686	sum_eq arg arg'
687	\| _ ⇒ false
688	]
689	\| XRL arg ⇒
690	match j with
691	[ XRL arg' ⇒
692	let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
693	let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
694	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
695	sum_eq arg arg'
696	\| _ ⇒ false
697	]
698	\| ORL arg ⇒
699	match j with
700	[ ORL arg' ⇒
701	let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
702	let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
703	let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
704	let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
705	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
706	sum_eq arg arg'
707	\| _ ⇒ false
708	]
709	\| ANL arg ⇒
710	match j with
711	[ ANL arg' ⇒
712	let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
713	let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
714	let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
715	let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
716	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
717	sum_eq arg arg'
718	\| _ ⇒ false
719	]
720	\| MOV arg ⇒
721	match j with
722	[ MOV arg' ⇒
723	let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
724	let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
725	let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
726	let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
727	let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
728	let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
729	let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
730	let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
731	let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
732	let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
733	let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
734	sum_eq_5 arg arg'
735	\| _ ⇒ false
736	]
737	].
738
739	lemma eq_sum_refl:
740	∀A, B: Type[0].
741	∀leq, req.
742	∀s.
743	∀leq_refl: (∀t. leq t t = true).
744	∀req_refl: (∀u. req u u = true).
745	eq_sum A B leq req s s = true.
746	#A #B #leq #req #s #leq_refl #req_refl
747	cases s whd in ⊢ (? → ??%?) //
748	qed.
749
750	lemma eq_prod_refl:
751	∀A, B: Type[0].
752	∀leq, req.
753	∀s.
754	∀leq_refl: (∀t. leq t t = true).
755	∀req_refl: (∀u. req u u = true).
756	eq_prod A B leq req s s = true.
757	#A #B #leq #req #s #leq_refl #req_refl
758	cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl
759	qed.
760
761	lemma eq_preinstruction_refl:
762	∀i.
763	eq_preinstruction i i = true.
764	#i cases i try #arg1 try #arg2
765	try @eq_addressing_mode_refl
766	[1,2,3,4,5,6,7,8,10,16,17,18,19,20:
767	whd in ⊢ (??%?)
768	try %
769	>eq_addressing_mode_refl
770	>eq_addressing_mode_refl %
771	\|13,15:
772	whd in ⊢ (??%?)
773	cases arg1
774	[*:
775	#arg1_left normalize nodelta
776	>eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
777	]
778	\|11,12:
779	whd in ⊢ (??%?)
780	cases arg1
781	[1:
782	#arg1_left normalize nodelta
783	>(eq_sum_refl …)
784	[1: % \| 2,3: #arg @eq_prod_refl ]
785	@eq_addressing_mode_refl
786	\|2:
787	#arg1_left normalize nodelta
788	@eq_prod_refl [*: @eq_addressing_mode_refl ]
789	\|3:
790	#arg1_left normalize nodelta
791	>(eq_sum_refl …) [1: %
792	\|2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
793	\|4:
794	#arg1_left normalize nodelta
795	@eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
796	]
797	\|14:
798	whd in ⊢ (??%?)
799	cases arg1
800	[ #arg1_left normalize nodelta
801	@eq_sum_refl
802	[1: #arg @eq_sum_refl
803	[1: #arg @eq_sum_refl
804	[1: #arg @eq_sum_refl
805	[1: #arg @eq_prod_refl
806	[*: @eq_addressing_mode_refl ]
807	\|2: #arg @eq_prod_refl
808	[*: #arg @eq_addressing_mode_refl ]
809	]
810	\|2: #arg @eq_prod_refl
811	[*: #arg @eq_addressing_mode_refl ]
812	]
813	\|2: #arg @eq_prod_refl
814	[*: #arg @eq_addressing_mode_refl ]
815	]
816	\|2: #arg @eq_prod_refl
817	[*: #arg @eq_addressing_mode_refl ]
818	]
819	\|2: #arg1_right normalize nodelta
820	@eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
821	]
822	\|*:
823	whd in ⊢ (??%?)
824	cases arg1
825	[*: #arg1 >eq_sum_refl
826	[1,4: normalize @eq_addressing_mode_refl
827	\|2,3,5,6: #arg @eq_prod_refl
828	[*: #arg @eq_addressing_mode_refl ]
829	]
830	]
831	]
832	qed.
833
834	definition eq_instruction: instruction → instruction → bool ≝
835	λi, j.
836	match i with
837	[ ACALL arg ⇒
838	match j with
839	[ ACALL arg' ⇒ eq_addressing_mode arg arg'
840	\| _ ⇒ false
841	]
842	\| LCALL arg ⇒
843	match j with
844	[ LCALL arg' ⇒ eq_addressing_mode arg arg'
845	\| _ ⇒ false
846	]
847	\| AJMP arg ⇒
848	match j with
849	[ AJMP arg' ⇒ eq_addressing_mode arg arg'
850	\| _ ⇒ false
851	]
852	\| LJMP arg ⇒
853	match j with
854	[ LJMP arg' ⇒ eq_addressing_mode arg arg'
855	\| _ ⇒ false
856	]
857	\| SJMP arg ⇒
858	match j with
859	[ SJMP arg' ⇒ eq_addressing_mode arg arg'
860	\| _ ⇒ false
861	]
862	\| JMP arg ⇒
863	match j with
864	[ JMP arg' ⇒ eq_addressing_mode arg arg'
865	\| _ ⇒ false
866	]
867	\| MOVC arg1 arg2 ⇒
868	match j with
869	[ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
870	\| _ ⇒ false
871	]
872	\| RealInstruction instr ⇒
873	match j with
874	[ RealInstruction instr' ⇒ eq_preinstruction instr instr'
875	\| _ ⇒ false
876	]
877	].
878
879	lemma eq_instruction_refl:
880	∀i. eq_instruction i i = true.
881	#i cases i
882	[1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
883	\|7: #arg1 #arg2
884	whd in ⊢ (??%?)
885	>eq_addressing_mode_refl
886	>eq_addressing_mode_refl
887	%
888	\|8: #arg @eq_preinstruction_refl
889	]
890	qed.
891
892	let rec vect_member
893	(A: Type[0]) (n: nat) (eq: A → A → bool)
894	(v: Vector A n) (a: A) on v: bool ≝
895	match v with
896	[ VEmpty ⇒ false
897	\| VCons len hd tl ⇒
898	eq hd a ∨ (vect_member A ? eq tl a)
899	].
900
901	let rec list_addressing_mode_tags_elim_prop
902	(n: nat)
903	(l: Vector addressing_mode_tag (S n))
904	on l:
905	∀P: l → Prop.
906	∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
907	∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
908	∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
909	∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
910	∀x: l. P x ≝
911	match l return
912	λy.
913	match y with
914	[ O ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
915	\| S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
916	∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
917	∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
918	∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
919	∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
920	∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
921	∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
922	∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
923	∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
924	∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
925	∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
926	∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
927	∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
928	∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
929	∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
930	∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
931	∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
932	∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
933	∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
934	∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
935	∀x:l. P x
936	] with
937	[ VEmpty ⇒ λAbsurd. ⊥
938	\| VCons len hd tl ⇒ λProof. ?
939	] (refl ? (S n)). cases daemon. qed. (*
940	[ destruct(Absurd)
941	\| # A1 # A2 # A3 # A4 # A5 # A6 # A7
942	# A8 # A9 # A10 # A11 # A12 # A13 # A14
943	# A15 # A16 # A17 # A18 # A19 # X
944	cases X
945	# SUB cases daemon ] qed.
946	cases SUB
947	[ # BYTE
948	normalize
949	].
950
951
952	(* let prepare_hd ≝
953	match hd with
954	[ direct ⇒ λdirect_prf. ?
955	\| indirect ⇒ λindirect_prf. ?
956	\| ext_indirect ⇒ λext_indirect_prf. ?
957	\| registr ⇒ λregistr_prf. ?
958	\| acc_a ⇒ λacc_a_prf. ?
959	\| acc_b ⇒ λacc_b_prf. ?
960	\| dptr ⇒ λdptr_prf. ?
961	\| data ⇒ λdata_prf. ?
962	\| data16 ⇒ λdata16_prf. ?
963	\| acc_dptr ⇒ λacc_dptr_prf. ?
964	\| acc_pc ⇒ λacc_pc_prf. ?
965	\| ext_indirect_dptr ⇒ λext_indirect_prf. ?
966	\| indirect_dptr ⇒ λindirect_prf. ?
967	\| carry ⇒ λcarry_prf. ?
968	\| bit_addr ⇒ λbit_addr_prf. ?
969	\| n_bit_addr ⇒ λn_bit_addr_prf. ?
970	\| relative ⇒ λrelative_prf. ?
971	\| addr11 ⇒ λaddr11_prf. ?
972	\| addr16 ⇒ λaddr16_prf. ?
973	]
974	in ? *)
975	].
976	[ 1: destruct(absd)
977	\| 2: # A1 # A2 # A3 # A4 # A5 # A6
978	# A7 # A8 # A9 # A10 # A11 # A12
979	# A13 # A14 # A15 # A16 # A17 # A18
980	# A19 *
981	].
982
983
984	match l return λx.match x with [O ⇒ λl: Vector … O. bool \| S x' ⇒ λl: Vector addressing_mode_tag (S x').
985	(l → bool) → bool ] with
986	[ VEmpty ⇒ true
987	\| VCons len hd tl ⇒ λP.
988	let process_hd ≝
989	match hd return λhd. ∀P: hd:::tl → bool. bool with
990	[ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
991	\| indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
992	\| ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
993	\| registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
994	\| acc_a ⇒ λP.P ACC_A
995	\| acc_b ⇒ λP.P ACC_B
996	\| dptr ⇒ λP.P DPTR
997	\| data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
998	\| data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
999	\| acc_dptr ⇒ λP.P ACC_DPTR
1000	\| acc_pc ⇒ λP.P ACC_PC
1001	\| ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
1002	\| indirect_dptr ⇒ λP.P INDIRECT_DPTR
1003	\| carry ⇒ λP.P CARRY
1004	\| bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
1005	\| n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
1006	\| relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
1007	\| addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
1008	\| addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
1009	]
1010	in
1011	andb (process_hd P)
1012	(match len return λx. x = len → bool with
1013	[ O ⇒ λprf. true
1014	\| S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
1015	].
1016	try %
1017	[ 2: cases (sym_eq ??? prf); @tl
1018	\| generalize in match H; generalize in match tl; cases prf;
1019	(* cases prf in tl H; : ??? WAS WORKING BEFORE *)
1020	#tl
1021	normalize in ⊢ (∀_: %. ?)
1022	# H
1023	whd
1024	normalize in ⊢ (match % with [ _ ⇒ ? \| _ ⇒ ?])
1025	cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
1026	qed.
1027	*)
1028
1029	definition load_code_memory_aux ≝
1030	fold_left_i_aux … (
1031	λi, mem, v.
1032	insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
1033
1034	axiom split_elim:
1035	∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
1036	(∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
1037
1038	example half_add_SO:
1039	∀pc.
1040	\snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
1041	cases daemon.
1042	qed.
1043
1044	(*
1045	axiom not_eqvb_S:
1046	∀pc.
1047	(¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
1048
1049	axiom not_eqvb_SS:
1050	∀pc.
1051	(¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
1052
1053	axiom bitvector_elim_complete:
1054	∀n,P. bitvector_elim n P = true → ∀bv. P bv.
1055
1056	lemma bitvector_elim_complete':
1057	∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
1058	#n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
1059	generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
1060	qed.
1061	*)
1062
1063	(*
1064	lemma andb_elim':
1065	∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
1066	#b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
1067	qed.
1068	*)
1069
1070	let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
1071	(encoding: list Byte) on encoding: Prop ≝
1072	match encoding with
1073	[ nil ⇒ final_pc = pc
1074	\| cons hd tl ⇒
1075	let 〈new_pc, byte〉 ≝ next code_memory pc in
1076	hd = byte ∧ encoding_check code_memory new_pc final_pc tl
1077	].
1078
1079	lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
1080	encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
1081	let intermediate_pc ≝ pc + length … l1 in
1082	encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
1083	encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
1084	#code_memory #final_pc #l1 elim l1
1085	[ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
1086	\| #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
1087	#K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
1088	qed.
1089
1090	axiom bitvector_3_elim_prop:
1091	∀P: BitVector 3 → Prop.
1092	P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
1093	P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
1094	P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
1095
1096	definition ticks_of_instruction ≝
1097	λi.
1098	let trivial_code_memory ≝ assembly1 i in
1099	let trivial_status ≝ load_code_memory trivial_code_memory in
1100	\snd (fetch trivial_status (zero ?)).
1101
1102	axiom fetch_assembly:
1103	∀pc,i,code_memory,assembled.
1104	assembled = assembly1 i →
1105	let len ≝ length … assembled in
1106	encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1107	let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
1108	let 〈instr_pc, ticks〉 ≝ fetched in
1109	let 〈instr,pc'〉 ≝ instr_pc in
1110	(eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
1111	(* #pc #i #code_memory #assembled cases i [8: *]
1112	[16,20,29: * * \|18,19: * * [1,2,4,5: ] \|28: * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
1113	[47,48,49:
1114	\|*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
1115	[2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
1116	59,60,63,64,65,66,67: #ARG]]
1117	[4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
1118	56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
1119	[1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
1120	39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
1121	68,69,70,71: #ARG2]]
1122	[1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
1123	normalize in ⊢ (???% → ?)
1124	[92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
1125	normalize in ⊢ (???% → ?)]
1126	#H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
1127	try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
1128	change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
1129	whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
1130	[17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
1131	[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
1132	30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
1133	69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
1134	whd >eq_instruction_refl >H4 @eq_bv_refl
1135	qed. *)
1136
1137	let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
1138	match expected with
1139	[ nil ⇒ eq_bv … pc final_pc = true
1140	\| cons i tl ⇒
1141	let fetched ≝ fetch code_memory pc in
1142	let 〈instr_pc, ticks〉 ≝ fetched in
1143	let 〈instr,pc'〉 ≝ instr_pc in
1144	eq_instruction instr i = true ∧
1145	ticks = (ticks_of_instruction i) ∧
1146	fetch_many code_memory final_pc pc' tl].
1147
1148	lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1149	#A #a #b #EQ destruct //
1150	qed.
1151
1152	axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
1153
1154	lemma fetch_assembly_pseudo:
1155	∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
1156	∀pi,code_memory,len,assembled,instructions,pc.
1157	let expansion ≝ pol ppc in
1158	Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
1159	Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
1160	encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1161	fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
1162	#program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
1163	#EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
1164	cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
1165	>EQ2a >EQ2b -EQ2a EQ2b;
1166	generalize in match (pc + \|flatten … (map … assembly1 instructions)\|); #final_pc
1167	generalize in match pc elim instructions
1168	[ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
1169	\| #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
1170	generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
1171	cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
1172	cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
1173	cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
1174	[ @K1 \| @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 \| >(eq_bv_eq … K3) @IH @H2 ]
1175	qed.
1176
1177	(*
1178	lemma rev_preserves_length:
1179	∀A.∀l. length … (rev A l) = length … l.
1180	#A #l elim l
1181	[ %
1182	\| #hd #tl #IH normalize >length_append normalize /2/ ]
1183	qed.
1184
1185	lemma rev_append:
1186	∀A.∀l1,l2.
1187	rev A (l1@l2) = rev A l2 @ rev A l1.
1188	#A #l1 elim l1 normalize //
1189	qed.
1190
1191	lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
1192	#A #l elim l
1193	[ //
1194	\| #hd #tl #IH normalize >rev_append normalize // ]
1195	qed.
1196
1197	lemma split_len_Sn:
1198	∀A:Type[0].∀l:list A.∀len.
1199	length … l = S len →
1200	Σl'.Σa. l = l'@[a] ∧ length … l' = len.
1201	#A #l elim l
1202	[ normalize #len #abs destruct
1203	\| #hd #tl #IH #len
1204	generalize in match (rev_rev … tl)
1205	cases (rev A tl) in ⊢ (??%? → ?)
1206	[ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/
1207	\| #a #l' #H <H normalize #EQ
1208	%[@(hd::rev … l')] %[@a] % //
1209	>length_append in EQ #EQ normalize in EQ; normalize;
1210	generalize in match (injective_S … EQ) #EQ2 /2/ ]]
1211	qed.
1212
1213	lemma list_elim_rev:
1214	∀A:Type[0].∀P:list A → Type[0].
1215	P [ ] → (∀l,a. P l → P (l@[a])) →
1216	∀l. P l.
1217	#A #P #H1 #H2 #l
1218	generalize in match (refl … (length … l))
1219	generalize in ⊢ (???% → ?) #n generalize in match l
1220	elim n
1221	[ #L cases L [ // \| #x #w #abs (normalize in abs) @⊥ // ]
1222	\| #m #IH #L #EQ
1223	cases (split_len_Sn … EQ) #l' * #a * /3/ ]
1224	qed.
1225
1226	axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
1227	axiom prefix_of_append:
1228	∀A:Type[0].∀l,l1,l2:list A.
1229	is_prefix … l l1 → is_prefix … l (l1@l2).
1230	axiom prefix_reflexive: ∀A,l. is_prefix A l l.
1231	axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
1232
1233	record Propify (A:Type[0]) : Type[0] (Prop) ≝ { in_propify: A }.
1234
1235	definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
1236	λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
1237
1238	definition app ≝
1239	λA:Type[0].λl1:Propify (list A).λl2:list A.
1240	match l1 with
1241	[ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
1242
1243	lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
1244	#A * /3/
1245	qed.
1246
1247	lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
1248	#A * #l1 normalize //
1249	qed.
1250	*)
1251
1252	axiom assembly_ok:
1253	∀program,pol,assembled.
1254	let 〈labels,costs〉 ≝ build_maps program pol in
1255	Some … 〈assembled,costs〉 = assembly program pol →
1256	let code_memory ≝ load_code_memory assembled in
1257	let preamble ≝ \fst program in
1258	let datalabels ≝ construct_datalabels preamble in
1259	let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1260	let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1261	∀ppc,len,assembledi.
1262	let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1263	Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
1264	encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
1265	sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
1266
1267	axiom bitvector_of_nat_nat_of_bitvector:
1268	∀n,v.
1269	bitvector_of_nat n (nat_of_bitvector n v) = v.
1270
1271	axiom assembly_ok_to_expand_pseudo_instruction_ok:
1272	∀program,pol,assembled,costs.
1273	Some … 〈assembled,costs〉 = assembly program pol →
1274	∀ppc.
1275	let code_memory ≝ load_code_memory assembled in
1276	let preamble ≝ \fst program in
1277	let data_labels ≝ construct_datalabels preamble in
1278	let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1279	let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1280	let expansion ≝ pol ppc in
1281	let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1282	∃instructions.
1283	Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
1284
1285	axiom pair_elim':
1286	∀A,B,C: Type[0].
1287	∀T: A → B → C.
1288	∀p.
1289	∀P: A×B → C → Prop.
1290	(∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
1291	P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
1292
1293	axiom pair_elim'':
1294	∀A,B,C,C': Type[0].
1295	∀T: A → B → C.
1296	∀T': A → B → C'.
1297	∀p.
1298	∀P: A×B → C → C' → Prop.
1299	(∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
1300	P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
1301
1302	axiom split_elim':
1303	∀A: Type[0].
1304	∀B: Type[1].
1305	∀l, m, v.
1306	∀T: Vector A l → Vector A m → B.
1307	∀P: B → Prop.
1308	(∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
1309	P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
1310
1311	axiom split_elim'':
1312	∀A: Type[0].
1313	∀B,B': Type[1].
1314	∀l, m, v.
1315	∀T: Vector A l → Vector A m → B.
1316	∀T': Vector A l → Vector A m → B'.
1317	∀P: B → B' → Prop.
1318	(∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
1319	P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
1320	(let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
1321
1322	lemma fetch_assembly_pseudo2:
1323	∀program,pol,assembled.
1324	let 〈labels,costs〉 ≝ build_maps program pol in
1325	Some … 〈assembled,costs〉 = assembly program pol →
1326	∀ppc.
1327	let code_memory ≝ load_code_memory assembled in
1328	let preamble ≝ \fst program in
1329	let data_labels ≝ construct_datalabels preamble in
1330	let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1331	let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1332	let expansion ≝ pol ppc in
1333	let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1334	∃instructions.
1335	Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
1336	fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
1337	#program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
1338	generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
1339	letin code_memory ≝ (load_code_memory assembled)
1340	letin preamble ≝ (\fst program)
1341	letin data_labels ≝ (construct_datalabels preamble)
1342	letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
1343	letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1344	whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
1345	cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
1346	generalize in match (fetch_assembly_pseudo program pol ppc
1347	(λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
1348	(load_code_memory assembled));
1349	whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
1350	whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
1351	normalize nodelta in EXPAND; (* HERE *)
1352	generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
1353	>bitvector_of_nat_nat_of_bitvector in H1; #H1
1354	<EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
1355	#H1 #H2
1356	cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
1357	generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
1358	[ #K3 % [2: % [% \| @K3]] \| @K1 ]
1359	qed.
1360
1361	(* OLD?
1362	definition assembly_specification:
1363	∀assembly_program: pseudo_assembly_program.
1364	∀code_mem: BitVectorTrie Byte 16. Prop ≝
1365	λpseudo_assembly_program.
1366	λcode_mem.
1367	∀pc: Word.
1368	let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1369	let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1370	let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1371	let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1372	let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1373	(sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1374	match pre_assembled with
1375	[ None ⇒ True
1376	\| Some pc_code ⇒
1377	let 〈new_pc,code〉 ≝ pc_code in
1378	encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1379
1380	axiom assembly_meets_specification:
1381	∀pseudo_assembly_program.
1382	match assembly pseudo_assembly_program with
1383	[ None ⇒ True
1384	\| Some code_mem_cost ⇒
1385	let 〈code_mem, cost〉 ≝ code_mem_cost in
1386	assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1387	].
1388	(*
1389	# PROGRAM
1390	[ cases PROGRAM
1391	# PREAMBLE
1392	# INSTR_LIST
1393	elim INSTR_LIST
1394	[ whd
1395	whd in ⊢ (∀_. %)
1396	# PC
1397	whd
1398	\| # INSTR
1399	# INSTR_LIST_TL
1400	# H
1401	whd
1402	whd in ⊢ (match % with [ _ ⇒ ? \| _ ⇒ ?])
1403	]
1404	\| cases not_implemented
1405	] *)
1406	*)
1407
1408	definition internal_pseudo_address_map ≝ list (BitVector 8).
1409
1410	axiom low_internal_ram_of_pseudo_low_internal_ram:
1411	∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1412
1413	axiom high_internal_ram_of_pseudo_high_internal_ram:
1414	∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1415
1416	axiom low_internal_ram_of_pseudo_internal_ram_hit:
1417	∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
1418	member ? (eq_bv 8) (false:::addr) M = true →
1419	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1420	let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1421	let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1422	let bl ≝ lookup ? 7 addr ram (zero 8) in
1423	let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1424	bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
1425
1426	(* changed from add to sub *)
1427	axiom low_internal_ram_of_pseudo_internal_ram_miss:
1428	∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
1429	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1430	let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1431	let carr ≝ get_index_v ? ? flags 1 ? in
1432	carr = false →
1433	member ? (eq_bv 8) (false:::Saddr) M = false →
1434	member ? (eq_bv 8) (false:::addr) M = false →
1435	lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1436	//
1437	qed.
1438
1439	definition addressing_mode_ok ≝
1440	λT.λM:internal_pseudo_address_map.λs:PreStatus T.
1441	λaddr:addressing_mode.
1442	match addr with
1443	[ DIRECT d ⇒
1444	¬(member ? (eq_bv 8) d M) ∧
1445	¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1446	\| INDIRECT i ⇒
1447	let d ≝ get_register ? s [[false;false;i]] in
1448	¬(member ? (eq_bv 8) d M) ∧
1449	¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1450	\| EXT_INDIRECT _ ⇒ true
1451	\| REGISTER _ ⇒ true
1452	\| ACC_A ⇒ true
1453	\| ACC_B ⇒ true
1454	\| DPTR ⇒ true
1455	\| DATA _ ⇒ true
1456	\| DATA16 _ ⇒ true
1457	\| ACC_DPTR ⇒ true
1458	\| ACC_PC ⇒ true
1459	\| EXT_INDIRECT_DPTR ⇒ true
1460	\| INDIRECT_DPTR ⇒ true
1461	\| CARRY ⇒ true
1462	\| BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1463	\| N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1464	\| RELATIVE _ ⇒ true
1465	\| ADDR11 _ ⇒ true
1466	\| ADDR16 _ ⇒ true ].
1467
1468	definition next_internal_pseudo_address_map0 ≝
1469	λT.
1470	λfetched.
1471	λM: internal_pseudo_address_map.
1472	λs: PreStatus T.
1473	match fetched with
1474	[ Comment _ ⇒ Some ? M
1475	\| Cost _ ⇒ Some … M
1476	\| Jmp _ ⇒ Some … M
1477	\| Call _ ⇒
1478	Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1479	\| Mov _ _ ⇒ Some … M
1480	\| Instruction instr ⇒
1481	match instr with
1482	[ ADD addr1 addr2 ⇒
1483	if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1484	Some ? M
1485	else
1486	None ?
1487	\| ADDC addr1 addr2 ⇒
1488	if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1489	Some ? M
1490	else
1491	None ?
1492	\| SUBB addr1 addr2 ⇒
1493	if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1494	Some ? M
1495	else
1496	None ?
1497	\| _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1498
1499
1500	definition next_internal_pseudo_address_map ≝
1501	λM:internal_pseudo_address_map.
1502	λs:PseudoStatus.
1503	next_internal_pseudo_address_map0 ?
1504	(\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1505
1506	definition status_of_pseudo_status:
1507	internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
1508	λM,ps,pol.
1509	let pap ≝ code_memory … ps in
1510	match assembly pap pol with
1511	[ None ⇒ None …
1512	\| Some p ⇒
1513	let cm ≝ load_code_memory (\fst p) in
1514	let pc ≝ sigma pap pol (program_counter ? ps) in
1515	let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1516	let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1517	Some …
1518	(mk_PreStatus (BitVectorTrie Byte 16)
1519	cm
1520	lir
1521	hir
1522	(external_ram … ps)
1523	pc
1524	(special_function_registers_8051 … ps)
1525	(special_function_registers_8052 … ps)
1526	(p1_latch … ps)
1527	(p3_latch … ps)
1528	(clock … ps)) ].
1529
1530	(*
1531	definition write_at_stack_pointer':
1532	∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1533	λM: Type[0].
1534	λs: PreStatus M.
1535	λv: Byte.
1536	let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1537	let bit_zero ≝ get_index_v… nu O ? in
1538	let bit_1 ≝ get_index_v… nu 1 ? in
1539	let bit_2 ≝ get_index_v… nu 2 ? in
1540	let bit_3 ≝ get_index_v… nu 3 ? in
1541	if bit_zero then
1542	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1543	v (low_internal_ram ? s) in
1544	set_low_internal_ram ? s memory
1545	else
1546	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1547	v (high_internal_ram ? s) in
1548	set_high_internal_ram ? s memory.
1549	[ cases l0 %
1550	\|2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1551	qed.
1552
1553	definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1554	Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1555	≝
1556	λticks_of.
1557	λs.
1558	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1559	let ticks ≝ ticks_of (program_counter ? s) in
1560	let s ≝ set_clock ? s (clock ? s + ticks) in
1561	let s ≝ set_program_counter ? s pc in
1562	match instr with
1563	[ Instruction instr ⇒
1564	execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1565	\| Comment cmt ⇒ s
1566	\| Cost cst ⇒ s
1567	\| Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1568	\| Call call ⇒
1569	let a ≝ address_of_word_labels s call in
1570	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1571	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1572	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1573	let s ≝ write_at_stack_pointer' ? s pc_bl in
1574	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1575	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1576	let s ≝ write_at_stack_pointer' ? s pc_bu in
1577	set_program_counter ? s a
1578	\| Mov dptr ident ⇒
1579	set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1580	].
1581	[
1582	\|2,3,4: %
1583	\| <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1584	\|
1585	\| %
1586	]
1587	cases not_implemented
1588	qed.
1589	*)
1590
1591	axiom execute_1_pseudo_instruction_preserves_code_memory:
1592	∀ticks_of,ps.
1593	code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1594
1595	(*
1596	lemma execute_code_memory_unchanged:
1597	∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1598	#ticks #ps whd in ⊢ (??? (??%))
1599	cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1600	(program_counter pseudo_assembly_program ps)) #instr #pc
1601	whd in ⊢ (??? (??%)) cases instr
1602	[ #pre cases pre
1603	[ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1604	cases (split ????) #z1 #z2 %
1605	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1606	cases (split ????) #z1 #z2 %
1607	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1608	cases (split ????) #z1 #z2 %
1609	\| #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1610	[ #x1 whd in ⊢ (??? (??%))
1611	\| *: cases not_implemented
1612	]
1613	\| #comment %
1614	\| #cost %
1615	\| #label %
1616	\| #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1617	cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1618	whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1619	whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1620	(* CSC: ??? *)
1621	\| #dptr #label (* CSC: ??? *)
1622	]
1623	cases not_implemented
1624	qed.
1625	*)
1626
1627	lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1628	∀M:internal_pseudo_address_map.
1629	∀ps,ps': PseudoStatus.
1630	∀pol.
1631	∀prf:code_memory … ps = code_memory … ps'.
1632	let pol' ≝ ? in
1633	match status_of_pseudo_status M ps pol with
1634	[ None ⇒ status_of_pseudo_status M ps' pol' = None …
1635	\| Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1636	].
1637	[2: <prf @pol]
1638	#M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? \| _ ⇒ ? ])
1639	generalize in match (refl … (assembly (code_memory … ps) pol))
1640	cases (assembly ??) in ⊢ (???% → %)
1641	[ #K whd whd in ⊢ (??%?) <H >K %
1642	\| #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1643	qed.
1644
1645	definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
1646	λprogram: pseudo_assembly_program.λpol.
1647	λppc: Word.
1648	λfetched.
1649	match fetched with
1650	[ Instruction instr ⇒
1651	match instr with
1652	[ JC lbl ⇒
1653	match pol ppc with
1654	[ short_jump ⇒ 〈2, 2〉
1655	\| medium_jump ⇒ ?
1656	\| long_jump ⇒ 〈4, 4〉
1657	]
1658	\| JNC lbl ⇒
1659	match pol ppc with
1660	[ short_jump ⇒ 〈2, 2〉
1661	\| medium_jump ⇒ ?
1662	\| long_jump ⇒ 〈4, 4〉
1663	]
1664	\| JB bit lbl ⇒
1665	match pol ppc with
1666	[ short_jump ⇒ 〈2, 2〉
1667	\| medium_jump ⇒ ?
1668	\| long_jump ⇒ 〈4, 4〉
1669	]
1670	\| JNB bit lbl ⇒
1671	match pol ppc with
1672	[ short_jump ⇒ 〈2, 2〉
1673	\| medium_jump ⇒ ?
1674	\| long_jump ⇒ 〈4, 4〉
1675	]
1676	\| JBC bit lbl ⇒
1677	match pol ppc with
1678	[ short_jump ⇒ 〈2, 2〉
1679	\| medium_jump ⇒ ?
1680	\| long_jump ⇒ 〈4, 4〉
1681	]
1682	\| JZ lbl ⇒
1683	match pol ppc with
1684	[ short_jump ⇒ 〈2, 2〉
1685	\| medium_jump ⇒ ?
1686	\| long_jump ⇒ 〈4, 4〉
1687	]
1688	\| JNZ lbl ⇒
1689	match pol ppc with
1690	[ short_jump ⇒ 〈2, 2〉
1691	\| medium_jump ⇒ ?
1692	\| long_jump ⇒ 〈4, 4〉
1693	]
1694	\| CJNE arg lbl ⇒
1695	match pol ppc with
1696	[ short_jump ⇒ 〈2, 2〉
1697	\| medium_jump ⇒ ?
1698	\| long_jump ⇒ 〈4, 4〉
1699	]
1700	\| DJNZ arg lbl ⇒
1701	match pol ppc with
1702	[ short_jump ⇒ 〈2, 2〉
1703	\| medium_jump ⇒ ?
1704	\| long_jump ⇒ 〈4, 4〉
1705	]
1706	\| ADD arg1 arg2 ⇒
1707	let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1708	〈ticks, ticks〉
1709	\| ADDC arg1 arg2 ⇒
1710	let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1711	〈ticks, ticks〉
1712	\| SUBB arg1 arg2 ⇒
1713	let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1714	〈ticks, ticks〉
1715	\| INC arg ⇒
1716	let ticks ≝ ticks_of_instruction (INC ? arg) in
1717	〈ticks, ticks〉
1718	\| DEC arg ⇒
1719	let ticks ≝ ticks_of_instruction (DEC ? arg) in
1720	〈ticks, ticks〉
1721	\| MUL arg1 arg2 ⇒
1722	let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1723	〈ticks, ticks〉
1724	\| DIV arg1 arg2 ⇒
1725	let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1726	〈ticks, ticks〉
1727	\| DA arg ⇒
1728	let ticks ≝ ticks_of_instruction (DA ? arg) in
1729	〈ticks, ticks〉
1730	\| ANL arg ⇒
1731	let ticks ≝ ticks_of_instruction (ANL ? arg) in
1732	〈ticks, ticks〉
1733	\| ORL arg ⇒
1734	let ticks ≝ ticks_of_instruction (ORL ? arg) in
1735	〈ticks, ticks〉
1736	\| XRL arg ⇒
1737	let ticks ≝ ticks_of_instruction (XRL ? arg) in
1738	〈ticks, ticks〉
1739	\| CLR arg ⇒
1740	let ticks ≝ ticks_of_instruction (CLR ? arg) in
1741	〈ticks, ticks〉
1742	\| CPL arg ⇒
1743	let ticks ≝ ticks_of_instruction (CPL ? arg) in
1744	〈ticks, ticks〉
1745	\| RL arg ⇒
1746	let ticks ≝ ticks_of_instruction (RL ? arg) in
1747	〈ticks, ticks〉
1748	\| RLC arg ⇒
1749	let ticks ≝ ticks_of_instruction (RLC ? arg) in
1750	〈ticks, ticks〉
1751	\| RR arg ⇒
1752	let ticks ≝ ticks_of_instruction (RR ? arg) in
1753	〈ticks, ticks〉
1754	\| RRC arg ⇒
1755	let ticks ≝ ticks_of_instruction (RRC ? arg) in
1756	〈ticks, ticks〉
1757	\| SWAP arg ⇒
1758	let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1759	〈ticks, ticks〉
1760	\| MOV arg ⇒
1761	let ticks ≝ ticks_of_instruction (MOV ? arg) in
1762	〈ticks, ticks〉
1763	\| MOVX arg ⇒
1764	let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1765	〈ticks, ticks〉
1766	\| SETB arg ⇒
1767	let ticks ≝ ticks_of_instruction (SETB ? arg) in
1768	〈ticks, ticks〉
1769	\| PUSH arg ⇒
1770	let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1771	〈ticks, ticks〉
1772	\| POP arg ⇒
1773	let ticks ≝ ticks_of_instruction (POP ? arg) in
1774	〈ticks, ticks〉
1775	\| XCH arg1 arg2 ⇒
1776	let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1777	〈ticks, ticks〉
1778	\| XCHD arg1 arg2 ⇒
1779	let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1780	〈ticks, ticks〉
1781	\| RET ⇒
1782	let ticks ≝ ticks_of_instruction (RET ?) in
1783	〈ticks, ticks〉
1784	\| RETI ⇒
1785	let ticks ≝ ticks_of_instruction (RETI ?) in
1786	〈ticks, ticks〉
1787	\| NOP ⇒
1788	let ticks ≝ ticks_of_instruction (NOP ?) in
1789	〈ticks, ticks〉
1790	]
1791	\| Comment comment ⇒ 〈0, 0〉
1792	\| Cost cost ⇒ 〈0, 0〉
1793	\| Jmp jmp ⇒ 〈2, 2〉
1794	\| Call call ⇒ 〈2, 2〉
1795	\| Mov dptr tgt ⇒ 〈2, 2〉
1796	].
1797	cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1798	qed.
1799
1800	definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
1801	λprogram: pseudo_assembly_program.λpol.
1802	λppc: Word.
1803	let 〈preamble, pseudo〉 ≝ program in
1804	let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1805	ticks_of0 program pol ppc fetched.
1806
1807	lemma get_register_set_program_counter:
1808	∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1809	#T #s #pc %
1810	qed.
1811
1812	lemma get_8051_sfr_set_program_counter:
1813	∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1814	#T #s #pc %
1815	qed.
1816
1817	lemma get_bit_addressable_sfr_set_program_counter:
1818	∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1819	#T #s #pc %
1820	qed.
1821
1822	lemma low_internal_ram_set_program_counter:
1823	∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1824	#T #s #pc %
1825	qed.
1826
1827	lemma get_arg_8_set_program_counter:
1828	∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
1829	∀T,s,pc,b.∀arg:l.
1830	get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
1831	[2,3: cases arg; *; normalize //]
1832	#n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
1833	qed.
1834
1835	lemma set_bit_addressable_sfr_set_code_memory:
1836	∀T, U: Type[0].
1837	∀ps: PreStatus ?.
1838	∀code_mem.
1839	∀x.
1840	∀val.
1841	set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
1842	set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
1843	#T #U #ps #code_mem #x #val
1844	whd in ⊢ (??%?)
1845	whd in ⊢ (???(???%?))
1846	cases (eqb ? 128) [ normalize nodelta cases not_implemented
1847	\| normalize nodelta
1848	cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1849	\| normalize nodelta
1850	cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1851	\| normalize nodelta
1852	cases (eqb ? 176) [ normalize nodelta %
1853	\| normalize nodelta
1854	cases (eqb ? 153) [ normalize nodelta %
1855	\| normalize nodelta
1856	cases (eqb ? 138) [ normalize nodelta %
1857	\| normalize nodelta
1858	cases (eqb ? 139) [ normalize nodelta %
1859	\| normalize nodelta
1860	cases (eqb ? 140) [ normalize nodelta %
1861	\| normalize nodelta
1862	cases (eqb ? 141) [ normalize nodelta %
1863	\| normalize nodelta
1864	cases (eqb ? 200) [ normalize nodelta %
1865	\| normalize nodelta
1866	cases (eqb ? 202) [ normalize nodelta %
1867	\| normalize nodelta
1868	cases (eqb ? 203) [ normalize nodelta %
1869	\| normalize nodelta
1870	cases (eqb ? 204) [ normalize nodelta %
1871	\| normalize nodelta
1872	cases (eqb ? 205) [ normalize nodelta %
1873	\| normalize nodelta
1874	cases (eqb ? 135) [ normalize nodelta %
1875	\| normalize nodelta
1876	cases (eqb ? 136) [ normalize nodelta %
1877	\| normalize nodelta
1878	cases (eqb ? 137) [ normalize nodelta %
1879	\| normalize nodelta
1880	cases (eqb ? 152) [ normalize nodelta %
1881	\| normalize nodelta
1882	cases (eqb ? 168) [ normalize nodelta %
1883	\| normalize nodelta
1884	cases (eqb ? 184) [ normalize nodelta %
1885	\| normalize nodelta
1886	cases (eqb ? 129) [ normalize nodelta %
1887	\| normalize nodelta
1888	cases (eqb ? 130) [ normalize nodelta %
1889	\| normalize nodelta
1890	cases (eqb ? 131) [ normalize nodelta %
1891	\| normalize nodelta
1892	cases (eqb ? 208) [ normalize nodelta %
1893	\| normalize nodelta
1894	cases (eqb ? 224) [ normalize nodelta %
1895	\| normalize nodelta
1896	cases (eqb ? 240) [ normalize nodelta %
1897	\| normalize nodelta
1898	cases not_implemented
1899	]]]]]]]]]]]]]]]]]]]]]]]]]]
1900	qed.
1901
1902	lemma set_arg_8_set_code_memory:
1903	∀n:nat.
1904	∀l:Vector addressing_mode_tag (S n).
1905	¬(is_in ? l ACC_PC) →
1906	∀T: Type[0].
1907	∀U: Type[0].
1908	∀ps: PreStatus ?.
1909	∀code_mem.
1910	∀val.
1911	∀b: l.
1912	set_arg_8 ? (set_code_memory T U ps code_mem) b val =
1913	set_code_memory T U (set_arg_8 ? ps b val) code_mem.
1914	[2,3: cases b; *; normalize //]
1915	#n #l #prf #T #U #ps #code_mem #val * *;
1916	[*:
1917	[1,2,3,4,8,9,15,16,17,18,19: #x]
1918	try #y whd in ⊢ (??(%)?)
1919	whd in ⊢ (???(???(%)?))
1920	[1,2:
1921	cases (split bool 4 4 ?)
1922	#nu' #nl'
1923	normalize nodelta
1924	cases (split bool 1 3 nu')
1925	#bit1' #ignore'
1926	normalize nodelta
1927	cases (get_index_v bool 4 nu' 0 ?)
1928	[1,2,3,4:
1929	normalize nodelta
1930	try %
1931	try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
1932	try (normalize in ⊢ (???(???%?)))
1933	]
1934	\|3,4: %
1935	\|*:
1936	try normalize nodelta
1937	normalize cases (not_implemented)
1938	]
1939	]
1940
1941
1942	qed.
1943
1944	axiom set_arg_8_set_program_counter:
1945	∀n:nat.
1946	∀l:Vector addressing_mode_tag (S n).
1947	¬(is_in ? l ACC_PC) →
1948	∀T: Type[0].
1949	∀ps: PreStatus ?.
1950	∀pc.
1951	∀val.
1952	∀b: l.
1953	set_arg_8 ? (set_program_counter T ps pc) b val =
1954	set_program_counter T (set_arg_8 ? ps b val) pc.
1955	[1,2: cases b; *; normalize //]
1956	qed.
1957
1958
1959	lemma get_arg_8_set_code_memory:
1960	∀T1,T2,s,code_mem,b,arg.
1961	get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
1962	#T1 #T2 #s #code_mem #b #arg %
1963	qed.
1964
1965	lemma set_code_memory_set_flags:
1966	∀T1,T2,s,f1,f2,f3,code_mem.
1967	set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
1968	set_flags … (set_code_memory … s code_mem) f1 f2 f3.
1969	#T1 #T2 #s #f1 #f2 #f3 #code_mem %
1970	qed.
1971
1972	lemma set_program_counter_set_flags:
1973	∀T1,s,f1,f2,f3,pc.
1974	set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
1975	set_flags … (set_program_counter … s pc) f1 f2 f3.
1976	#T1 #s #f1 #f2 #f3 #pc %
1977	qed.
1978
1979	lemma program_counter_set_flags:
1980	∀T1,s,f1,f2,f3.
1981	program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
1982	#T1 #s #f1 #f2 #f3 %
1983	qed.
1984
1985	lemma special_function_registers_8051_write_at_stack_pointer:
1986	∀T,s,x.
1987	special_function_registers_8051 T (write_at_stack_pointer T s x)
1988	= special_function_registers_8051 T s.
1989	#T #s #x whd in ⊢ (??(??%)?)
1990	cases (split ????) #nu #nl normalize nodelta;
1991	cases (get_index_v bool ????) %
1992	qed.
1993
1994	lemma get_8051_sfr_write_at_stack_pointer:
1995	∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
1996	#T #s #x #y whd in ⊢ (??%%) //
1997	qed.
1998
1999	lemma code_memory_write_at_stack_pointer:
2000	∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
2001	#T #s #x whd in ⊢ (??(??%)?)
2002	cases (split ????) #nu #nl normalize nodelta;
2003	cases (get_index_v bool ????) %
2004	qed.
2005
2006	axiom low_internal_ram_write_at_stack_pointer:
2007	∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2008	get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2009	low_internal_ram ? s2 = low_internal_ram T2 s3 →
2010	sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2011	sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2012	bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
2013	low_internal_ram T1
2014	(write_at_stack_pointer ?
2015	(set_8051_sfr ?
2016	(write_at_stack_pointer ?
2017	(set_8051_sfr ?
2018	(set_low_internal_ram ? s1
2019	(low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
2020	SFR_SP sp1)
2021	bl)
2022	SFR_SP sp2)
2023	bu)
2024	= low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
2025	(low_internal_ram ?
2026	(write_at_stack_pointer ?
2027	(set_8051_sfr ?
2028	(write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2029	SFR_SP sp2)
2030	pbu)).
2031
2032	axiom high_internal_ram_write_at_stack_pointer:
2033	∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2034	get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2035	high_internal_ram ? s2 = high_internal_ram T2 s3 →
2036	sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2037	sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2038	bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
2039	high_internal_ram T1
2040	(write_at_stack_pointer ?
2041	(set_8051_sfr ?
2042	(write_at_stack_pointer ?
2043	(set_8051_sfr ?
2044	(set_high_internal_ram ? s1
2045	(high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
2046	SFR_SP sp1)
2047	bl)
2048	SFR_SP sp2)
2049	bu)
2050	= high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2051	(high_internal_ram ?
2052	(write_at_stack_pointer ?
2053	(set_8051_sfr ?
2054	(write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2055	SFR_SP sp2)
2056	pbu)).
2057
2058	lemma set_program_counter_set_low_internal_ram:
2059	∀T,s,x,y.
2060	set_program_counter T (set_low_internal_ram … s x) y =
2061	set_low_internal_ram … (set_program_counter … s y) x.
2062	//
2063	qed.
2064
2065	lemma set_clock_set_low_internal_ram:
2066	∀T,s,x,y.
2067	set_clock T (set_low_internal_ram … s x) y =
2068	set_low_internal_ram … (set_clock … s y) x.
2069	//
2070	qed.
2071
2072	lemma set_program_counter_set_high_internal_ram:
2073	∀T,s,x,y.
2074	set_program_counter T (set_high_internal_ram … s x) y =
2075	set_high_internal_ram … (set_program_counter … s y) x.
2076	//
2077	qed.
2078
2079	lemma set_clock_set_high_internal_ram:
2080	∀T,s,x,y.
2081	set_clock T (set_high_internal_ram … s x) y =
2082	set_high_internal_ram … (set_clock … s y) x.
2083	//
2084	qed.
2085
2086	lemma set_low_internal_ram_set_high_internal_ram:
2087	∀T,s,x,y.
2088	set_low_internal_ram T (set_high_internal_ram … s x) y =
2089	set_high_internal_ram … (set_low_internal_ram … s y) x.
2090	//
2091	qed.
2092
2093	lemma external_ram_write_at_stack_pointer:
2094	∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
2095	#T #s #x whd in ⊢ (??(??%)?)
2096	cases (split ????) #nu #nl normalize nodelta;
2097	cases (get_index_v bool ????) %
2098	qed.
2099
2100	lemma special_function_registers_8052_write_at_stack_pointer:
2101	∀T,s,x.
2102	special_function_registers_8052 T (write_at_stack_pointer T s x)
2103	= special_function_registers_8052 T s.
2104	#T #s #x whd in ⊢ (??(??%)?)
2105	cases (split ????) #nu #nl normalize nodelta;
2106	cases (get_index_v bool ????) %
2107	qed.
2108
2109	lemma p1_latch_write_at_stack_pointer:
2110	∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
2111	#T #s #x whd in ⊢ (??(??%)?)
2112	cases (split ????) #nu #nl normalize nodelta;
2113	cases (get_index_v bool ????) %
2114	qed.
2115
2116	lemma p3_latch_write_at_stack_pointer:
2117	∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
2118	#T #s #x whd in ⊢ (??(??%)?)
2119	cases (split ????) #nu #nl normalize nodelta;
2120	cases (get_index_v bool ????) %
2121	qed.
2122
2123	lemma clock_write_at_stack_pointer:
2124	∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
2125	#T #s #x whd in ⊢ (??(??%)?)
2126	cases (split ????) #nu #nl normalize nodelta;
2127	cases (get_index_v bool ????) %
2128	qed.
2129
2130	axiom get_index_v_set_index:
2131	∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
2132
2133	lemma get_8051_sfr_set_8051_sfr:
2134	∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
2135	#T ; #A #B #C #D #E #F #G #H #I #J ; #y whd in ⊢ (??(??%?)?)
2136	whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
2137	qed.
2138
2139	lemma program_counter_set_8051_sfr:
2140	∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
2141	//
2142	qed.
2143
2144	axiom get_arg_8_set_low_internal_ram:
2145	∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
2146
2147	lemma eq_rect_Type1_r:
2148	∀A: Type[1].
2149	∀a:A.
2150	∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2151	#A #a #P #H #x #p
2152	generalize in match H
2153	generalize in match P
2154	cases p
2155	//
2156	qed.
2157
2158	lemma split_eq_status:
2159	∀T.
2160	∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
2161	∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
2162	A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
2163	mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
2164	mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
2165	//
2166	qed.
2167
2168	axiom split_append:
2169	∀A: Type[0].
2170	∀m, n: nat.
2171	∀v, v': Vector A m.
2172	∀q, q': Vector A n.
2173	let 〈v', q'〉 ≝ split A m n (v@@q) in
2174	v = v' ∧ q = q'.
2175
2176	axiom split_vector_singleton:
2177	∀A: Type[0].
2178	∀n: nat.
2179	∀v: Vector A (S n).
2180	∀rest: Vector A n.
2181	∀s: Vector A 1.
2182	∀prf.
2183	v = s @@ rest →
2184	((get_index_v A ? v 0 prf) ::: rest) = v.
2185
2186	example sub_minus_one_seven_eight:
2187	∀v: BitVector 7.
2188	false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
2189	\fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
2190	cases daemon.
2191	qed.
2192
2193	lemma pair_destruct_1:
2194	∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
2195	#A #B #a #b *; /2/
2196	qed.
2197
2198	lemma pair_destruct_2:
2199	∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
2200	#A #B #a #b *; /2/
2201	qed.
2202
2203	(*
2204	lemma blah:
2205	∀m: internal_pseudo_address_map.
2206	∀s: PseudoStatus.
2207	∀arg: Byte.
2208	∀b: bool.
2209	addressing_mode_ok m s (DIRECT arg) = true →
2210	get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2211	get_arg_8 ? s b (DIRECT arg).
2212	[2, 3: normalize % ]
2213	#m #s #arg #b #hyp
2214	whd in ⊢ (??%%)
2215	@split_elim''
2216	#nu' #nl' #arg_nu_nl_eq
2217	normalize nodelta
2218	generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2219	cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2220	#get_index_v_eq
2221	normalize nodelta
2222	[2:
2223	normalize nodelta
2224	@split_elim''
2225	#bit_one' #three_bits' #bit_one_three_bit_eq
2226	generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2227	normalize nodelta
2228	generalize in match (refl ? (sub_7_with_carry ? ? ?))
2229	cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2230	#Saddr #carr' #Saddr_carr_eq
2231	normalize nodelta
2232	#carr_hyp'
2233	@carr_hyp'
2234	[1:
2235	\|2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2236	generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2237	cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2238	#member_eq
2239	normalize nodelta
2240	[2: #destr destruct(destr)
2241	\|1: -carr_hyp';
2242	>arg_nu_nl_eq
2243	<(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2244	[1: >get_index_v_eq in ⊢ (??%? → ?)
2245	\|2: @le_S @le_S @le_S @le_n
2246	]
2247	cases (member (BitVector 8) ? (\fst ?) ?)
2248	[1: #destr normalize in destr; destruct(destr)
2249	\|2:
2250	]
2251	]
2252	\|3: >get_index_v_eq in ⊢ (??%?)
2253	change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2254	>(split_vector_singleton … bit_one_three_bit_eq)
2255	<arg_nu_nl_eq
2256	whd in hyp:(??%?)
2257	cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2258	normalize nodelta [*: #ignore @sym_eq ]
2259	]
2260	\|
2261	].
2262	*)
2263	(*
2264	map_address0 ... (DIRECT arg) = Some .. →
2265	get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2266	get_arg_8 (internal_ram ...) (DIRECT arg)
2267
2268	((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2)
2269	then Some internal_pseudo_address_map M
2270	else None internal_pseudo_address_map )
2271	=Some internal_pseudo_address_map M')
2272	*)
2273
2274	lemma main_thm:
2275	∀M,M',ps,s,s'',pol.
2276	next_internal_pseudo_address_map M ps = Some … M' →
2277	status_of_pseudo_status M ps pol = Some … s →
2278	status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some … s'' →
2279	∃n. execute n s = s''.
2280	[2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
2281	#M #M' #ps #s #s'' #pol
2282	generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
2283	whd in ⊢ (? → ? → ??%? → ??%? → ?)
2284	>execute_1_pseudo_instruction_preserves_code_memory
2285	generalize in match (refl … (assembly (code_memory … ps) pol))
2286	generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
2287	cases (build_maps (code_memory … ps) pol)
2288	#labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
2289	generalize in match pol; -pol;
2290	@(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
2291	#EQ0 #pol normalize nodelta;
2292	generalize in ⊢ (???(match % with [_ ⇒ ? \| _ ⇒ ?]) → ?) *; normalize nodelta;
2293	[ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
2294	* #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
2295	#H generalize in match (H ? (refl …)) -H; #H;
2296	#MAP
2297	#H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
2298	#H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
2299	change with
2300	(∃n.
2301	execute n
2302	(set_low_internal_ram ?
2303	(set_high_internal_ram ?
2304	(set_program_counter ?
2305	(set_code_memory ?? ps (load_code_memory assembled))
2306	(sigma 〈preamble,instr_list〉 pol (program_counter ? ps)))
2307	(high_internal_ram_of_pseudo_high_internal_ram M ?))
2308	(low_internal_ram_of_pseudo_low_internal_ram M ?))
2309	= set_low_internal_ram ?
2310	(set_high_internal_ram ?
2311	(set_program_counter ?
2312	(set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
2313	(sigma ???))
2314	?)
2315	?)
2316	whd in match (\snd 〈preamble,instr_list〉) in H;
2317	whd in match (\fst 〈preamble,instr_list〉) in H;
2318	whd in match (\snd 〈final_pc,assembled〉) in H;
2319	whd in match (\snd 〈preamble,instr_list〉) in MAP;
2320	-s s'' labels costs final_ppc final_pc;
2321	letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps)
2322	(* NICE STATEMENT HERE *)
2323	generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
2324	#K <K generalize in match K; -K;
2325	(* STATEMENT WITH EQUALITY HERE *)
2326	whd in ⊢ (???(?%?) → ?)
2327	whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
2328	cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
2329	#pi #newppc normalize nodelta; #MAP * #instructions *;
2330	cases pi in MAP; normalize nodelta;
2331	[2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
2332	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
2333	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2334	#H2 >(eq_bv_eq … H2) >EQ %
2335	(* \|6: (* Mov *) #arg1 #arg2
2336	#H1 #H2 #EQ %[@1]
2337	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2338	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2339	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2340	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2341	>H2b >(eq_instruction_to_eq … H2a)
2342	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2343	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2344	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2345	normalize nodelta;
2346	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
2347	#result #flags
2348	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
2349	(* \|5: (* Call *) #label #MAP
2350	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
2351	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2352	[ (* short *) #abs @⊥ destruct (abs)
2353	\|3: (* long *) #H1 #H2 #EQ %[@1]
2354	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2355	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2356	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2357	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2358	>H2b >(eq_instruction_to_eq … H2a)
2359	generalize in match EQ; -EQ;
2360	whd in ⊢ (???% → ??%?);
2361	generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
2362	>(eq_bv_eq … H2c)
2363	change with
2364	((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
2365	(let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2366	generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
2367	generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
2368	>get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
2369	>get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
2370	generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
2371	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2372	@split_eq_status;
2373	[ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
2374	>code_memory_write_at_stack_pointer %
2375	\| >set_program_counter_set_low_internal_ram
2376	>set_clock_set_low_internal_ram
2377	@low_internal_ram_write_at_stack_pointer
2378	[ >EQ0 @pol \| % \| %
2379	\| @(pair_destruct_2 … EQ1)
2380	\| @(pair_destruct_2 … EQ2)
2381	\| >(pair_destruct_1 ????? EQpc)
2382	>(pair_destruct_2 ????? EQpc)
2383	@split_elim #x #y #H <H -x y H;
2384	>(pair_destruct_1 ????? EQppc)
2385	>(pair_destruct_2 ????? EQppc)
2386	@split_elim #x #y #H <H -x y H;
2387	>EQ0 % ]
2388	\| >set_low_internal_ram_set_high_internal_ram
2389	>set_program_counter_set_high_internal_ram
2390	>set_clock_set_high_internal_ram
2391	@high_internal_ram_write_at_stack_pointer
2392	[ >EQ0 @pol \| % \| %
2393	\| @(pair_destruct_2 … EQ1)
2394	\| @(pair_destruct_2 … EQ2)
2395	\| >(pair_destruct_1 ????? EQpc)
2396	>(pair_destruct_2 ????? EQpc)
2397	@split_elim #x #y #H <H -x y H;
2398	>(pair_destruct_1 ????? EQppc)
2399	>(pair_destruct_2 ????? EQppc)
2400	@split_elim #x #y #H <H -x y H;
2401	>EQ0 % ]
2402	\| >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
2403	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
2404	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
2405	>external_ram_write_at_stack_pointer %
2406	\| change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
2407	>EQ0 %
2408	\| >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
2409	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2410	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2411	>special_function_registers_8051_write_at_stack_pointer %
2412	\| >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
2413	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2414	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2415	>special_function_registers_8052_write_at_stack_pointer %
2416	\| >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
2417	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2418	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2419	>p1_latch_write_at_stack_pointer %
2420	\| >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
2421	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2422	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2423	>p3_latch_write_at_stack_pointer %
2424	\| >clock_write_at_stack_pointer whd in ⊢ (??%?)
2425	>clock_write_at_stack_pointer whd in ⊢ (???%)
2426	>clock_write_at_stack_pointer whd in ⊢ (???%)
2427	>clock_write_at_stack_pointer %]
2428	(\| ( medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2429	@pair_elim' #fst_5_addr #rest_addr #EQ1
2430	@pair_elim' #fst_5_pc #rest_pc #EQ2
2431	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2432	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2433	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2434	change in ⊢ (? →??%?) with (execute_1_0 ??)
2435	@pair_elim' * #instr #newppc' #ticks #EQn
2436	* * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
2437	generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2438	@pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
2439	@split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
2440	@pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
2441	change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
2442	@split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
2443	>get_8051_sfr_set_8051_sfr
2444
2445	whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2446	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2447	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2448	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2449	generalize in match (refl … (split bool 4 4 pc_bu))
2450	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2451	generalize in match (refl … (split bool 3 8 rest_addr))
2452	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2453	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2454	generalize in match
2455	(refl …
2456	(half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2457	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2458	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2459	@split_eq_status try %
2460	[ change with (? = sigma ? (address_of_word_labels ps label))
2461	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2462	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2463	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
2464	\|4: (* Jmp *) #label #MAP
2465	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
2466	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2467	[3: (* long *) #H1 #H2 #EQ %[@1]
2468	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2469	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2470	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2471	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2472	>H2b >(eq_instruction_to_eq … H2a)
2473	generalize in match EQ; -EQ;
2474	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2475	cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2476	\|1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2477	generalize in match
2478	(refl ?
2479	(sub_16_with_carry
2480	(sigma 〈preamble,instr_list〉 pol (program_counter … ps))
2481	(sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
2482	false))
2483	cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2484	generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2485	generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2486	#EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2487	generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2488	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2489	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2490	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2491	>H2b >(eq_instruction_to_eq … H2a)
2492	generalize in match EQ; -EQ;
2493	whd in ⊢ (???% → ?);
2494	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2495	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
2496	generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
2497	cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2498	@split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
2499	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2500	\| (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2501	generalize in match
2502	(refl …
2503	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
2504	cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2505	generalize in match
2506	(refl …
2507	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
2508	cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2509	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2510	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2511	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2512	change in ⊢ (? →??%?) with (execute_1_0 ??)
2513	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2514	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2515	>H2b >(eq_instruction_to_eq … H2a)
2516	generalize in match EQ; -EQ;
2517	whd in ⊢ (???% → ?);
2518	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2519	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2520	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
2521	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2522	generalize in match (refl … (split bool 4 4 pc_bu))
2523	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2524	generalize in match (refl … (split bool 3 8 rest_addr))
2525	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2526	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2527	generalize in match
2528	(refl …
2529	(half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
2530	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2531	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2532	@split_eq_status try %
2533	[ change with (? = sigma ?? (address_of_word_labels ps label))
2534	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2535	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2536	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2537	) \| ( Instruction ) -pi; whd in ⊢ (? → ??%? → ?) ; normalize nodelta;
2538	[1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2539	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2540	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2541	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2542	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2543	>H2b >(eq_instruction_to_eq … H2a)
2544	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2545	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2546	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2547	normalize nodelta; #MAP; (*
2548	[1: change in ⊢ (? → %) with
2549	((let 〈result,flags〉 ≝
2550	add_8_with_carry
2551	(get_arg_8 ? ps false ACC_A)
2552	(get_arg_8 ?
2553	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2554	false (DIRECT ARG2))
2555	? in ?) = ?)
2556	[2,3: %]
2557	change in ⊢ (???% → ?) with
2558	(let 〈result,flags〉 ≝ add_8_with_carry ?((get_arg_8 ? ps false ACC_A)) ?? in ?)
2559	>get_arg_8_set_clock *)
2560	[1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
2561	[2,4: #abs @⊥ normalize in abs; destruct (abs)
2562	\|*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
2563	[ change in ⊢ (? → %) with
2564	((let 〈result,flags〉 ≝
2565	add_8_with_carry
2566	(get_arg_8 ? ps false ACC_A)
2567	(get_arg_8 ?
2568	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2569	false (DIRECT ARG2))
2570	? in ?) = ?)
2571	>get_arg_8_set_low_internal_ram
2572
2573	cases (add_8_with_carry ???)
2574
2575	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
2576	#result #flags
2577	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2578	(\| ( INC *) #arg1 #H1 #H2 #EQ %[@1]
2579	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2580	change in ⊢ (? → ??%?) with (execute_1_0 ??)
2581	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2582	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
2583	>H2b >(eq_instruction_to_eq … H2a)
2584	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2585	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2586	[1,2,3,4: cases (half_add ???) #carry #result
2587	\| cases (half_add ???) #carry #bl normalize nodelta;
2588	cases (full_add ????) #carry' #bu normalize nodelta ]
2589	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
2590	[5: %
2591	\|1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2592	(set_program_counter pseudo_assembly_program ps newppc)
2593	(\fst (ticks_of0 〈preamble,instr_list〉
2594	(program_counter pseudo_assembly_program ps)
2595	(Instruction (INC Identifier (DIRECT ARG))))
2596	+clock pseudo_assembly_program
2597	(set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2598	[2,3: // ]
2599	<(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2600	whd in ⊢ (??%%)
2601	cases (split bool 4 4 ARG)
2602	#nu' #nl'
2603	normalize nodelta
2604	cases (split bool 1 3 nu')
2605	#bit_1' #ignore'
2606	normalize nodelta
2607	cases (get_index_v bool 4 nu' ? ?)
2608	[ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2609	\|
2610	] *)

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

Download in other formats:

Original Format