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