Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

ASM.ma @ 3558

Last change on this file since 3558 was 2514, checked in by sacerdot, 8 years ago
All .ma files committed: some of them are just in-progress.
File size: 32.5 KB

Line
1	include "ASM/BitVector.ma".
2	include "common/Identifiers.ma".
3	include "common/CostLabel.ma".
4	include "common/LabelledObjects.ma".
5
6	axiom ASMTag : String.
7	definition Identifier ≝ identifier ASMTag.
8	definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
9
10	inductive addressing_mode: Type[0] ≝
11	DIRECT: Byte → addressing_mode
12	\| INDIRECT: Bit → addressing_mode
13	\| EXT_INDIRECT: Bit → addressing_mode
14	\| REGISTER: BitVector 3 → addressing_mode
15	\| ACC_A: addressing_mode
16	\| ACC_B: addressing_mode
17	\| DPTR: addressing_mode
18	\| DATA: Byte → addressing_mode
19	\| DATA16: Word → addressing_mode
20	\| ACC_DPTR: addressing_mode
21	\| ACC_PC: addressing_mode
22	\| EXT_INDIRECT_DPTR: addressing_mode
23	\| INDIRECT_DPTR: addressing_mode
24	\| CARRY: addressing_mode
25	\| BIT_ADDR: Byte → addressing_mode
26	\| N_BIT_ADDR: Byte → addressing_mode
27	\| RELATIVE: Byte → addressing_mode
28	\| ADDR11: Word11 → addressing_mode
29	\| ADDR16: Word → addressing_mode.
30
31	definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
32	λa, b: addressing_mode.
33	match a with
34	[ DIRECT d ⇒
35	match b with
36	[ DIRECT e ⇒ eq_bv ? d e
37	\| _ ⇒ false
38	]
39	\| INDIRECT b' ⇒
40	match b with
41	[ INDIRECT e ⇒ eq_b b' e
42	\| _ ⇒ false
43	]
44	\| EXT_INDIRECT b' ⇒
45	match b with
46	[ EXT_INDIRECT e ⇒ eq_b b' e
47	\| _ ⇒ false
48	]
49	\| REGISTER bv ⇒
50	match b with
51	[ REGISTER bv' ⇒ eq_bv ? bv bv'
52	\| _ ⇒ false
53	]
54	\| ACC_A ⇒ match b with [ ACC_A ⇒ true \| _ ⇒ false ]
55	\| ACC_B ⇒ match b with [ ACC_B ⇒ true \| _ ⇒ false ]
56	\| DPTR ⇒ match b with [ DPTR ⇒ true \| _ ⇒ false ]
57	\| DATA b' ⇒
58	match b with
59	[ DATA e ⇒ eq_bv ? b' e
60	\| _ ⇒ false
61	]
62	\| DATA16 w ⇒
63	match b with
64	[ DATA16 e ⇒ eq_bv ? w e
65	\| _ ⇒ false
66	]
67	\| ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true \| _ ⇒ false ]
68	\| ACC_PC ⇒ match b with [ ACC_PC ⇒ true \| _ ⇒ false ]
69	\| EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
70	\| INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
71	\| CARRY ⇒ match b with [ CARRY ⇒ true \| _ ⇒ false ]
72	\| BIT_ADDR b' ⇒
73	match b with
74	[ BIT_ADDR e ⇒ eq_bv ? b' e
75	\| _ ⇒ false
76	]
77	\| N_BIT_ADDR b' ⇒
78	match b with
79	[ N_BIT_ADDR e ⇒ eq_bv ? b' e
80	\| _ ⇒ false
81	]
82	\| RELATIVE n ⇒
83	match b with
84	[ RELATIVE e ⇒ eq_bv ? n e
85	\| _ ⇒ false
86	]
87	\| ADDR11 w ⇒
88	match b with
89	[ ADDR11 e ⇒ eq_bv ? w e
90	\| _ ⇒ false
91	]
92	\| ADDR16 w ⇒
93	match b with
94	[ ADDR16 e ⇒ eq_bv ? w e
95	\| _ ⇒ false
96	]
97	].
98
99	lemma eq_addressing_mode_refl:
100	∀a. eq_addressing_mode a a = true.
101	#a
102	cases a try #arg1 try #arg2
103	try @eq_bv_refl try @eq_b_refl
104	try normalize %
105	qed.
106
107	(* dpm: renamed register to registr to avoid clash with brian's types *)
108	inductive addressing_mode_tag : Type[0] ≝
109	direct: addressing_mode_tag
110	\| indirect: addressing_mode_tag
111	\| ext_indirect: addressing_mode_tag
112	\| registr: addressing_mode_tag
113	\| acc_a: addressing_mode_tag
114	\| acc_b: addressing_mode_tag
115	\| dptr: addressing_mode_tag
116	\| data: addressing_mode_tag
117	\| data16: addressing_mode_tag
118	\| acc_dptr: addressing_mode_tag
119	\| acc_pc: addressing_mode_tag
120	\| ext_indirect_dptr: addressing_mode_tag
121	\| indirect_dptr: addressing_mode_tag
122	\| carry: addressing_mode_tag
123	\| bit_addr: addressing_mode_tag
124	\| n_bit_addr: addressing_mode_tag
125	\| relative: addressing_mode_tag
126	\| addr11: addressing_mode_tag
127	\| addr16: addressing_mode_tag.
128
129	definition eq_a ≝
130	λa, b: addressing_mode_tag.
131	match a with
132	[ direct ⇒ match b with [ direct ⇒ true \| _ ⇒ false ]
133	\| indirect ⇒ match b with [ indirect ⇒ true \| _ ⇒ false ]
134	\| ext_indirect ⇒ match b with [ ext_indirect ⇒ true \| _ ⇒ false ]
135	\| registr ⇒ match b with [ registr ⇒ true \| _ ⇒ false ]
136	\| acc_a ⇒ match b with [ acc_a ⇒ true \| _ ⇒ false ]
137	\| acc_b ⇒ match b with [ acc_b ⇒ true \| _ ⇒ false ]
138	\| dptr ⇒ match b with [ dptr ⇒ true \| _ ⇒ false ]
139	\| data ⇒ match b with [ data ⇒ true \| _ ⇒ false ]
140	\| data16 ⇒ match b with [ data16 ⇒ true \| _ ⇒ false ]
141	\| acc_dptr ⇒ match b with [ acc_dptr ⇒ true \| _ ⇒ false ]
142	\| acc_pc ⇒ match b with [ acc_pc ⇒ true \| _ ⇒ false ]
143	\| ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true \| _ ⇒ false ]
144	\| indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true \| _ ⇒ false ]
145	\| carry ⇒ match b with [ carry ⇒ true \| _ ⇒ false ]
146	\| bit_addr ⇒ match b with [ bit_addr ⇒ true \| _ ⇒ false ]
147	\| n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true \| _ ⇒ false ]
148	\| relative ⇒ match b with [ relative ⇒ true \| _ ⇒ false ]
149	\| addr11 ⇒ match b with [ addr11 ⇒ true \| _ ⇒ false ]
150	\| addr16 ⇒ match b with [ addr16 ⇒ true \| _ ⇒ false ]
151	].
152
153	lemma eq_a_to_eq:
154	∀a,b.
155	eq_a a b = true → a = b.
156	#a #b
157	cases a cases b
158	#K
159	try cases (eq_true_false K)
160	%
161	qed.
162
163	lemma eq_a_reflexive:
164	∀a. eq_a a a = true.
165	#a cases a %
166	qed.
167
168	let rec member_addressing_mode_tag
169	(n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
170	on v: Prop ≝
171	match v with
172	[ VEmpty ⇒ False
173	\| VCons n' hd tl ⇒
174	bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
175	].
176
177	lemma mem_decidable:
178	∀n: nat.
179	∀v: Vector addressing_mode_tag n.
180	∀element: addressing_mode_tag.
181	mem … eq_a n v element = true ∨
182	mem … eq_a … v element = false.
183	#n #v #element //
184	qed.
185
186	lemma eq_a_elim:
187	∀tag.
188	∀hd.
189	∀P: bool → Prop.
190	(tag = hd → P (true)) →
191	(tag ≠ hd → P (false)) →
192	P (eq_a tag hd).
193	#tag #hd #P
194	cases tag
195	cases hd
196	#true_hyp #false_hyp
197	try @false_hyp
198	try @true_hyp
199	try %
200	#absurd destruct(absurd)
201	qed.
202
203	(* to avoid expansion... *)
204	let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
205	match d with
206	[ direct ⇒ match A with [ DIRECT _ ⇒ true \| _ ⇒ false ]
207	\| indirect ⇒ match A with [ INDIRECT _ ⇒ true \| _ ⇒ false ]
208	\| ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true \| _ ⇒ false ]
209	\| registr ⇒ match A with [ REGISTER _ ⇒ true \| _ ⇒ false ]
210	\| acc_a ⇒ match A with [ ACC_A ⇒ true \| _ ⇒ false ]
211	\| acc_b ⇒ match A with [ ACC_B ⇒ true \| _ ⇒ false ]
212	\| dptr ⇒ match A with [ DPTR ⇒ true \| _ ⇒ false ]
213	\| data ⇒ match A with [ DATA _ ⇒ true \| _ ⇒ false ]
214	\| data16 ⇒ match A with [ DATA16 _ ⇒ true \| _ ⇒ false ]
215	\| acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true \| _ ⇒ false ]
216	\| acc_pc ⇒ match A with [ ACC_PC ⇒ true \| _ ⇒ false ]
217	\| ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
218	\| indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true \| _ ⇒ false ]
219	\| carry ⇒ match A with [ CARRY ⇒ true \| _ ⇒ false ]
220	\| bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true \| _ ⇒ false ]
221	\| n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true \| _ ⇒ false ]
222	\| relative ⇒ match A with [ RELATIVE _ ⇒ true \| _ ⇒ false ]
223	\| addr11 ⇒ match A with [ ADDR11 _ ⇒ true \| _ ⇒ false ]
224	\| addr16 ⇒ match A with [ ADDR16 _ ⇒ true \| _ ⇒ false ]
225	].
226
227	lemma is_a_decidable:
228	∀hd.
229	∀element.
230	is_a hd element = true ∨ is_a hd element = false.
231	#hd #element //
232	qed.
233
234	let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
235	match l return λm.λ_:Vector addressing_mode_tag m.bool with
236	[ VEmpty ⇒ false
237	\| VCons m he (tl: Vector addressing_mode_tag m) ⇒
238	is_a he A ∨ is_in ? tl A ].
239
240	definition is_in_cons_elim:
241	∀len.∀hd,tl.∀m:addressing_mode
242	.is_in (S len) (hd:::tl) m →
243	(bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
244	#len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
245	cases (is_a hd am) in ISIN; /2/
246	qed.
247
248	lemma is_in_monotonic_wrt_append:
249	∀m, n: nat.
250	∀p: Vector addressing_mode_tag m.
251	∀q: Vector addressing_mode_tag n.
252	∀to_search: addressing_mode.
253	bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
254	#m #n #p #q #to_search #assm
255	elim q try assumption
256	#n' #hd #tl #inductive_hypothesis
257	normalize
258	cases (is_a ??) try @I
259	>inductive_hypothesis @I
260	qed.
261
262	corollary is_in_hd_tl:
263	∀to_search: addressing_mode.
264	∀hd: addressing_mode_tag.
265	∀n: nat.
266	∀v: Vector addressing_mode_tag n.
267	bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
268	#to_search #hd #n #v
269	elim v
270	[1:
271	#absurd
272	normalize in absurd; cases absurd
273	\|2:
274	#n' #hd' #tl #inductive_hypothesis #assm
275	>vector_cons_append >(vector_cons_append … hd' tl)
276	@(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
277	assumption
278	]
279	qed.
280
281	lemma is_a_to_mem_to_is_in:
282	∀he,a,m,q.
283	is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
284	#he #a #m #q
285	elim q
286	[1:
287	#_ #K assumption
288	\|2:
289	#m' #t #q' #II #H1 #H2
290	normalize
291	change with (orb ??) in H2:(??%?);
292	cases (inclusive_disjunction_true … H2)
293	[1:
294	#K
295	<(eq_a_to_eq … K) >H1 %
296	\|2:
297	#K
298	>II
299	try assumption
300	cases (is_a t a)
301	normalize
302	%
303	]
304	]
305	qed.
306
307	lemma is_a_true_to_is_in:
308	∀n: nat.
309	∀x: addressing_mode.
310	∀tag: addressing_mode_tag.
311	∀supervector: Vector addressing_mode_tag n.
312	mem addressing_mode_tag eq_a n supervector tag →
313	is_a tag x = true →
314	is_in … supervector x.
315	#n #x #tag #supervector
316	elim supervector
317	[1:
318	#absurd cases absurd
319	\|2:
320	#n' #hd #tl #inductive_hypothesis
321	whd in match (mem … eq_a (S n') (hd:::tl) tag);
322	@eq_a_elim normalize nodelta
323	[1:
324	#tag_hd_eq #irrelevant
325	whd in match (is_in (S n') (hd:::tl) x);
326	<tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
327	@I
328	\|2:
329	#tag_hd_neq
330	whd in match (is_in (S n') (hd:::tl) x);
331	change with (
332	mem … eq_a n' tl tag)
333	in match (fold_right … n' ? false tl);
334	#mem_hyp #is_a_hyp
335	cases(is_a hd x)
336	[1:
337	normalize nodelta //
338	\|2:
339	normalize nodelta
340	@inductive_hypothesis assumption
341	]
342	]
343	]
344	qed.
345
346	record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
347	{
348	subaddressing_modeel:> addressing_mode;
349	subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
350	}.
351
352	coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
353	≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
354
355	coercion mk_subaddressing_mode :
356	∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
357	∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
358	≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
359
360	lemma is_in_subvector_is_in_supervector:
361	∀m, n: nat.
362	∀subvector: Vector addressing_mode_tag m.
363	∀supervector: Vector addressing_mode_tag n.
364	∀element: addressing_mode.
365	subvector_with … eq_a subvector supervector →
366	is_in m subvector element → is_in n supervector element.
367	#m #n #subvector #supervector #element
368	elim subvector
369	[1:
370	#subvector_with_proof #is_in_proof
371	cases is_in_proof
372	\|2:
373	#n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
374	whd in match (is_in … (hd':::tl') element);
375	cases (is_a_decidable hd' element)
376	[1:
377	#is_a_true >is_a_true
378	#irrelevant
379	whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
380	@(is_a_true_to_is_in … is_a_true)
381	lapply(subvector_with_proof)
382	cases(mem … eq_a n supervector hd') //
383	\|2:
384	#is_a_false >is_a_false normalize nodelta
385	#assm
386	@inductive_hypothesis
387	[1:
388	generalize in match subvector_with_proof;
389	whd in match (subvector_with … eq_a (hd':::tl') supervector);
390	cases(mem_decidable n supervector hd')
391	[1:
392	#mem_true >mem_true normalize nodelta
393	#assm assumption
394	\|2:
395	#mem_false >mem_false #absurd
396	cases absurd
397	]
398	\|2:
399	assumption
400	]
401	]
402	]
403	qed.
404
405	(* XXX: move back into ASM.ma *)
406	lemma subvector_with_to_subvector_with_tl:
407	∀n: nat.
408	∀m: nat.
409	∀v.
410	∀fixed_v.
411	∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v).
412	∀n': nat.
413	∀hd: addressing_mode_tag.
414	∀tl: Vector addressing_mode_tag n'.
415	∀m_refl: S n'=n.
416	∀v_refl: v≃hd:::tl.
417	subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v.
418	#n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl
419	generalize in match proof; destruct
420	whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
421	cases (mem … eq_a ? fixed_v hd) normalize nodelta
422	[1:
423	whd in match (subvector_with … eq_a tl fixed_v);
424	#assm assumption
425	\|2:
426	normalize in ⊢ (% → ?);
427	#absurd cases absurd
428	]
429	qed.
430
431	let rec subaddressing_mode_elim_type
432	(m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
433	(Q: fixed_v → Prop)
434	(n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
435	on v: Prop ≝
436	match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
437	[ VEmpty ⇒ λm_refl. λv_refl. Q origaddr
438	\| VCons n' hd tl ⇒ λm_refl. λv_refl.
439	let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
440	in
441	match hd return λa: addressing_mode_tag. a = hd → ? with
442	[ addr11 ⇒ λhd_refl. (∀w: Word11. Q (ADDR11 w)) → tail_call
443	\| addr16 ⇒ λhd_refl. (∀w: Word. Q (ADDR16 w)) → tail_call
444	\| direct ⇒ λhd_refl. (∀w: Byte. Q (DIRECT w)) → tail_call
445	\| indirect ⇒ λhd_refl. (∀w: Bit. Q (INDIRECT w)) → tail_call
446	\| ext_indirect ⇒ λhd_refl. (∀w: Bit. Q (EXT_INDIRECT w)) → tail_call
447	\| acc_a ⇒ λhd_refl. Q ACC_A → tail_call
448	\| registr ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
449	\| acc_b ⇒ λhd_refl. Q ACC_B → tail_call
450	\| dptr ⇒ λhd_refl. Q DPTR → tail_call
451	\| data ⇒ λhd_refl. (∀w: Byte. Q (DATA w)) → tail_call
452	\| data16 ⇒ λhd_refl. (∀w: Word. Q (DATA16 w)) → tail_call
453	\| acc_dptr ⇒ λhd_refl. Q ACC_DPTR → tail_call
454	\| acc_pc ⇒ λhd_refl. Q ACC_PC → tail_call
455	\| ext_indirect_dptr ⇒ λhd_refl. Q EXT_INDIRECT_DPTR → tail_call
456	\| indirect_dptr ⇒ λhd_refl. Q INDIRECT_DPTR → tail_call
457	\| carry ⇒ λhd_refl. Q CARRY → tail_call
458	\| bit_addr ⇒ λhd_refl. (∀w: Byte. Q (BIT_ADDR w)) → tail_call
459	\| n_bit_addr ⇒ λhd_refl. (∀w: Byte. Q (N_BIT_ADDR w)) → tail_call
460	\| relative ⇒ λhd_refl. (∀w: Byte. Q (RELATIVE w)) → tail_call
461	] (refl … hd)
462	] (refl … n) (refl_jmeq … v).
463	[20:
464	@(subvector_with_to_subvector_with_tl … proof … m_refl v_refl)
465	]
466	@(is_in_subvector_is_in_supervector … proof)
467	destruct @I
468	qed.
469
470	lemma subaddressing_mode_elim0:
471	∀n: nat.
472	∀v: Vector addressing_mode_tag (S n).
473	∀addr: v.
474	∀Q: v → Prop.
475	∀m,w,H.
476	(∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
477	subaddressing_mode_elim_type n v addr Q m w H.
478	#n #v #addr #Q #m #w elim w
479	[1:
480	/2/
481	\|2:
482	#n' #hd #tl #IH cases hd #H
483	#INV whd #PO @IH #xaddr cases xaddr *
484	try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
485	@ALREADYSEEN
486	]
487	qed.
488
489	lemma subaddressing_mode_elim:
490	∀n: nat.
491	∀v: Vector addressing_mode_tag (S n).
492	∀addr: v.
493	∀Q: v → Prop.
494	subaddressing_mode_elim_type n v addr Q (S n) v ?.
495	[1:
496	#n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
497	\|2:
498	@subvector_with_refl @eq_a_reflexive
499	]
500	qed.
501
502	inductive preinstruction (A: Type[0]) : Type[0] ≝
503	ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
504	\| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
505	\| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
506	\| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
507	\| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
508	\| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
509	\| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
510	\| DA: [[acc_a]] → preinstruction A
511
512	(* conditional jumps *)
513	\| JC: A → preinstruction A
514	\| JNC: A → preinstruction A
515	\| JB: [[bit_addr]] → A → preinstruction A
516	\| JNB: [[bit_addr]] → A → preinstruction A
517	\| JBC: [[bit_addr]] → A → preinstruction A
518	\| JZ: A → preinstruction A
519	\| JNZ: A → preinstruction A
520	\| CJNE:
521	[[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
522	\| DJNZ: [[registr ; direct]] → A → preinstruction A
523	(* logical operations *)
524	\| ANL:
525	[[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
526	[[direct]] × [[ acc_a ; data ]] ⊎
527	[[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
528	\| ORL:
529	[[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
530	[[direct]] × [[ acc_a ; data ]] ⊎
531	[[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
532	\| XRL:
533	[[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
534	[[direct]] × [[ acc_a ; data ]] → preinstruction A
535	\| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
536	\| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
537	\| RL: [[acc_a]] → preinstruction A
538	\| RLC: [[acc_a]] → preinstruction A
539	\| RR: [[acc_a]] → preinstruction A
540	\| RRC: [[acc_a]] → preinstruction A
541	\| SWAP: [[acc_a]] → preinstruction A
542
543	(* data transfer *)
544	\| MOV:
545	[[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
546	[[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
547	[[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
548	[[dptr]] × [[data16]] ⊎
549	[[carry]] × [[bit_addr]] ⊎
550	[[bit_addr]] × [[carry]] → preinstruction A
551	\| MOVX:
552	[[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
553	[[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
554	\| SETB: [[ carry ; bit_addr ]] → preinstruction A
555	\| PUSH: [[direct]] → preinstruction A
556	\| POP: [[direct]] → preinstruction A
557	\| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
558	\| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
559
560	(* program branching *)
561	\| RET: preinstruction A
562	\| RETI: preinstruction A
563	\| NOP: preinstruction A.
564
565	definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
566	λi, j.
567	match i with
568	[ ADD arg1 arg2 ⇒
569	match j with
570	[ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
571	\| _ ⇒ false
572	]
573	\| ADDC arg1 arg2 ⇒
574	match j with
575	[ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
576	\| _ ⇒ false
577	]
578	\| SUBB arg1 arg2 ⇒
579	match j with
580	[ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
581	\| _ ⇒ false
582	]
583	\| INC arg ⇒
584	match j with
585	[ INC arg' ⇒ eq_addressing_mode arg arg'
586	\| _ ⇒ false
587	]
588	\| DEC arg ⇒
589	match j with
590	[ DEC arg' ⇒ eq_addressing_mode arg arg'
591	\| _ ⇒ false
592	]
593	\| MUL arg1 arg2 ⇒
594	match j with
595	[ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
596	\| _ ⇒ false
597	]
598	\| DIV arg1 arg2 ⇒
599	match j with
600	[ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
601	\| _ ⇒ false
602	]
603	\| DA arg ⇒
604	match j with
605	[ DA arg' ⇒ eq_addressing_mode arg arg'
606	\| _ ⇒ false
607	]
608	\| JC arg ⇒
609	match j with
610	[ JC arg' ⇒ eq_addressing_mode arg arg'
611	\| _ ⇒ false
612	]
613	\| JNC arg ⇒
614	match j with
615	[ JNC arg' ⇒ eq_addressing_mode arg arg'
616	\| _ ⇒ false
617	]
618	\| JB arg1 arg2 ⇒
619	match j with
620	[ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
621	\| _ ⇒ false
622	]
623	\| JNB arg1 arg2 ⇒
624	match j with
625	[ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
626	\| _ ⇒ false
627	]
628	\| JBC arg1 arg2 ⇒
629	match j with
630	[ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
631	\| _ ⇒ false
632	]
633	\| JZ arg ⇒
634	match j with
635	[ JZ arg' ⇒ eq_addressing_mode arg arg'
636	\| _ ⇒ false
637	]
638	\| JNZ arg ⇒
639	match j with
640	[ JNZ arg' ⇒ eq_addressing_mode arg arg'
641	\| _ ⇒ false
642	]
643	\| CJNE arg1 arg2 ⇒
644	match j with
645	[ CJNE arg1' arg2' ⇒
646	let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
647	let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
648	let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
649	arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
650	\| _ ⇒ false
651	]
652	\| DJNZ arg1 arg2 ⇒
653	match j with
654	[ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
655	\| _ ⇒ false
656	]
657	\| CLR arg ⇒
658	match j with
659	[ CLR arg' ⇒ eq_addressing_mode arg arg'
660	\| _ ⇒ false
661	]
662	\| CPL arg ⇒
663	match j with
664	[ CPL arg' ⇒ eq_addressing_mode arg arg'
665	\| _ ⇒ false
666	]
667	\| RL arg ⇒
668	match j with
669	[ RL arg' ⇒ eq_addressing_mode arg arg'
670	\| _ ⇒ false
671	]
672	\| RLC arg ⇒
673	match j with
674	[ RLC arg' ⇒ eq_addressing_mode arg arg'
675	\| _ ⇒ false
676	]
677	\| RR arg ⇒
678	match j with
679	[ RR arg' ⇒ eq_addressing_mode arg arg'
680	\| _ ⇒ false
681	]
682	\| RRC arg ⇒
683	match j with
684	[ RRC arg' ⇒ eq_addressing_mode arg arg'
685	\| _ ⇒ false
686	]
687	\| SWAP arg ⇒
688	match j with
689	[ SWAP arg' ⇒ eq_addressing_mode arg arg'
690	\| _ ⇒ false
691	]
692	\| SETB arg ⇒
693	match j with
694	[ SETB arg' ⇒ eq_addressing_mode arg arg'
695	\| _ ⇒ false
696	]
697	\| PUSH arg ⇒
698	match j with
699	[ PUSH arg' ⇒ eq_addressing_mode arg arg'
700	\| _ ⇒ false
701	]
702	\| POP arg ⇒
703	match j with
704	[ POP arg' ⇒ eq_addressing_mode arg arg'
705	\| _ ⇒ false
706	]
707	\| XCH arg1 arg2 ⇒
708	match j with
709	[ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
710	\| _ ⇒ false
711	]
712	\| XCHD arg1 arg2 ⇒
713	match j with
714	[ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
715	\| _ ⇒ false
716	]
717	\| RET ⇒ match j with [ RET ⇒ true \| _ ⇒ false ]
718	\| RETI ⇒ match j with [ RETI ⇒ true \| _ ⇒ false ]
719	\| NOP ⇒ match j with [ NOP ⇒ true \| _ ⇒ false ]
720	\| MOVX arg ⇒
721	match j with
722	[ MOVX arg' ⇒
723	let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
724	let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
725	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
726	sum_eq arg arg'
727	\| _ ⇒ false
728	]
729	\| XRL arg ⇒
730	match j with
731	[ XRL arg' ⇒
732	let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
733	let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
734	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
735	sum_eq arg arg'
736	\| _ ⇒ false
737	]
738	\| ORL arg ⇒
739	match j with
740	[ ORL arg' ⇒
741	let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
742	let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
743	let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
744	let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
745	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
746	sum_eq arg arg'
747	\| _ ⇒ false
748	]
749	\| ANL arg ⇒
750	match j with
751	[ ANL arg' ⇒
752	let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
753	let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
754	let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
755	let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
756	let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
757	sum_eq arg arg'
758	\| _ ⇒ false
759	]
760	\| MOV arg ⇒
761	match j with
762	[ MOV arg' ⇒
763	let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
764	let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
765	let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
766	let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
767	let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
768	let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
769	let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
770	let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
771	let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
772	let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
773	let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
774	sum_eq_5 arg arg'
775	\| _ ⇒ false
776	]
777	].
778
779	lemma eq_preinstruction_refl:
780	∀i.
781	eq_preinstruction i i = true.
782	#i cases i try #arg1 try #arg2
783	try @eq_addressing_mode_refl
784	[1,2,3,4,5,6,7,8,10,16,17,18,19,20:
785	whd in ⊢ (??%?); try %
786	>eq_addressing_mode_refl
787	>eq_addressing_mode_refl %
788	\|13,15:
789	whd in ⊢ (??%?);
790	cases arg1
791	[*:
792	#arg1_left normalize nodelta
793	>eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
794	]
795	\|11,12:
796	whd in ⊢ (??%?);
797	cases arg1
798	[1:
799	#arg1_left normalize nodelta
800	>(eq_sum_refl …)
801	[1: % \| 2,3: #arg @eq_prod_refl ]
802	@eq_addressing_mode_refl
803	\|2:
804	#arg1_left normalize nodelta
805	@eq_prod_refl [*: @eq_addressing_mode_refl ]
806	\|3:
807	#arg1_left normalize nodelta
808	>(eq_sum_refl …)
809	[1:
810	%
811	\|2,3:
812	#arg @eq_prod_refl #arg @eq_addressing_mode_refl
813	]
814	\|4:
815	#arg1_left normalize nodelta
816	@eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
817	]
818	\|14:
819	whd in ⊢ (??%?);
820	cases arg1
821	[1:
822	#arg1_left normalize nodelta
823	@eq_sum_refl
824	[1:
825	#arg @eq_sum_refl
826	[1:
827	#arg @eq_sum_refl
828	[1:
829	#arg @eq_sum_refl
830	[1:
831	#arg @eq_prod_refl
832	[*:
833	@eq_addressing_mode_refl
834	]
835	\|2:
836	#arg @eq_prod_refl
837	[*:
838	#arg @eq_addressing_mode_refl
839	]
840	]
841	\|2:
842	#arg @eq_prod_refl
843	[*:
844	#arg @eq_addressing_mode_refl
845	]
846	]
847	\|2:
848	#arg @eq_prod_refl
849	[*:
850	#arg @eq_addressing_mode_refl
851	]
852	]
853	\|2:
854	#arg @eq_prod_refl
855	[*:
856	#arg @eq_addressing_mode_refl
857	]
858	]
859	\|2:
860	#arg1_right normalize nodelta
861	@eq_prod_refl
862	[*:
863	#arg @eq_addressing_mode_refl
864	]
865	]
866	\|*:
867	whd in ⊢ (??%?);
868	cases arg1
869	[*:
870	#arg1 >eq_sum_refl
871	[1,4:
872	@eq_addressing_mode_refl
873	\|2,3,5,6:
874	#arg @eq_prod_refl
875	[*:
876	#arg @eq_addressing_mode_refl
877	]
878	]
879	]
880	]
881	qed.
882
883	inductive instruction: Type[0] ≝
884	\| ACALL: [[addr11]] → instruction
885	\| LCALL: [[addr16]] → instruction
886	\| AJMP: [[addr11]] → instruction
887	\| LJMP: [[addr16]] → instruction
888	\| SJMP: [[relative]] → instruction
889	\| JMP: [[indirect_dptr]] → instruction
890	\| MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
891	\| RealInstruction: preinstruction [[ relative ]] → instruction.
892
893	coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
894	RealInstruction on _p: preinstruction ? to instruction.
895
896	definition eq_instruction: instruction → instruction → bool ≝
897	λi, j.
898	match i with
899	[ ACALL arg ⇒
900	match j with
901	[ ACALL arg' ⇒ eq_addressing_mode arg arg'
902	\| _ ⇒ false
903	]
904	\| LCALL arg ⇒
905	match j with
906	[ LCALL arg' ⇒ eq_addressing_mode arg arg'
907	\| _ ⇒ false
908	]
909	\| AJMP arg ⇒
910	match j with
911	[ AJMP arg' ⇒ eq_addressing_mode arg arg'
912	\| _ ⇒ false
913	]
914	\| LJMP arg ⇒
915	match j with
916	[ LJMP arg' ⇒ eq_addressing_mode arg arg'
917	\| _ ⇒ false
918	]
919	\| SJMP arg ⇒
920	match j with
921	[ SJMP arg' ⇒ eq_addressing_mode arg arg'
922	\| _ ⇒ false
923	]
924	\| JMP arg ⇒
925	match j with
926	[ JMP arg' ⇒ eq_addressing_mode arg arg'
927	\| _ ⇒ false
928	]
929	\| MOVC arg1 arg2 ⇒
930	match j with
931	[ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
932	\| _ ⇒ false
933	]
934	\| RealInstruction instr ⇒
935	match j with
936	[ RealInstruction instr' ⇒ eq_preinstruction instr instr'
937	\| _ ⇒ false
938	]
939	].
940
941	lemma eq_instruction_refl:
942	∀i. eq_instruction i i = true.
943	#i cases i [*: #arg1 ]
944	try @eq_addressing_mode_refl
945	try @eq_preinstruction_refl
946	#arg2 whd in ⊢ (??%?);
947	>eq_addressing_mode_refl >eq_addressing_mode_refl %
948	qed.
949
950	lemma eq_instruction_to_eq:
951	∀i1, i2: instruction.
952	eq_instruction i1 i2 = true → i1 ≃ i2.
953	#i1 #i2
954	cases i1 cases i2 cases daemon (* easy but tedious
955	[1,10,19,28,37,46:
956	#arg1 #arg2
957	whd in match (eq_instruction ??);
958	cases arg1 #subaddressing_mode
959	cases subaddressing_mode
960	try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
961	try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
962	try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
963	#word11 #irrelevant
964	cases arg2 #subaddressing_mode
965	cases subaddressing_mode
966	try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
967	try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
968	try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
969	#word11' #irrelevant normalize nodelta
970	#eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
971	qed.
972
973	inductive pseudo_instruction: Type[0] ≝
974	\| Instruction: preinstruction Identifier → pseudo_instruction
975	\| Comment: String → pseudo_instruction
976	\| Cost: costlabel → pseudo_instruction
977	\| Jmp: Identifier → pseudo_instruction
978	\| Call: Identifier → pseudo_instruction
979	\| Mov: [[dptr]] → Identifier → pseudo_instruction.
980
981	definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
982	definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
983	definition assembly_program ≝ list instruction.
984	definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
985
986	(* labels & instructions *)
987	definition instruction_has_label ≝
988	λid: Identifier.
989	λi.
990	match i with
991	[ Jmp j ⇒ j = id
992	\| Call j ⇒ j = id
993	\| Instruction instr ⇒
994	match instr with
995	[ JC j ⇒ j = id
996	\| JNC j ⇒ j = id
997	\| JZ j ⇒ j = id
998	\| JNZ j ⇒ j = id
999	\| JB _ j ⇒ j = id
1000	\| JNB _ j ⇒ j = id
1001	\| JBC _ j ⇒ j = id
1002	\| DJNZ _ j ⇒ j = id
1003	\| CJNE _ j ⇒ j = id
1004	\| _ ⇒ False
1005	]
1006	\| _ ⇒ False
1007	].
1008
1009
1010	(* If instruction i is a jump, then there will be something in the policy at
1011	* position i *)
1012	definition is_jump' ≝
1013	λx:preinstruction Identifier.
1014	match x with
1015	[ JC _ ⇒ true
1016	\| JNC _ ⇒ true
1017	\| JZ _ ⇒ true
1018	\| JNZ _ ⇒ true
1019	\| JB _ _ ⇒ true
1020	\| JNB _ _ ⇒ true
1021	\| JBC _ _ ⇒ true
1022	\| CJNE _ _ ⇒ true
1023	\| DJNZ _ _ ⇒ true
1024	\| _ ⇒ false
1025	].
1026
1027	definition is_relative_jump ≝
1028	λinstr:pseudo_instruction.
1029	match instr with
1030	[ Instruction i ⇒ is_jump' i
1031	\| _ ⇒ false
1032	].
1033
1034	definition is_jump ≝
1035	λinstr:pseudo_instruction.
1036	match instr with
1037	[ Instruction i ⇒ is_jump' i
1038	\| Call _ ⇒ true
1039	\| Jmp _ ⇒ true
1040	\| _ ⇒ false
1041	].
1042
1043	definition is_call ≝
1044	λinstr:pseudo_instruction.
1045	match instr with
1046	[ Call _ ⇒ true
1047	\| _ ⇒ false
1048	].
1049
1050	definition is_jump_to ≝
1051	λx:pseudo_instruction.λd:Identifier.
1052	match x with
1053	[ Instruction i ⇒ match i with
1054	[ JC j ⇒ d = j
1055	\| JNC j ⇒ d = j
1056	\| JZ j ⇒ d = j
1057	\| JNZ j ⇒ d = j
1058	\| JB _ j ⇒ d = j
1059	\| JNB _ j ⇒ d = j
1060	\| JBC _ j ⇒ d = j
1061	\| CJNE _ j ⇒ d = j
1062	\| DJNZ _ j ⇒ d = j
1063	\| _ ⇒ False
1064	]
1065	\| Call c ⇒ d = c
1066	\| Jmp j ⇒ d = j
1067	\| _ ⇒ False
1068	].

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

Download in other formats:

Original Format