source: src/ASM/ASM.ma @ 2124

Last change on this file since 2124 was 2124, checked in by sacerdot, 8 years ago

Much more shuffling around to proper places

File size: 29.9 KB
Line 
1include "ASM/BitVector.ma".
2include "common/Identifiers.ma".
3include "common/CostLabel.ma".
4include "common/LabelledObjects.ma".
5
6axiom ASMTag : String.
7definition Identifier ≝ identifier ASMTag.
8definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
9
10inductive 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
31definition 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
99lemma 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 %
105qed.
106
107(* dpm: renamed register to registr to avoid clash with brian's types *)
108inductive 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
129definition 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
153lemma 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 %
161qed.
162
163lemma eq_a_reflexive:
164  ∀a. eq_a a a = true.
165  #a cases a %
166qed.
167
168let 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
177lemma 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 //
184qed.
185
186lemma 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)
201qed.
202
203(* to avoid expansion... *)
204let 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
227lemma is_a_decidable:
228  ∀hd.
229  ∀element.
230    is_a hd element = true ∨ is_a hd element = false.
231  #hd #element //
232qed.
233
234let 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
240definition 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/
246qed.
247
248lemma is_a_to_mem_to_is_in:
249 ∀he,a,m,q.
250   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
251 #he #a #m #q
252 elim q
253 [1:
254   #_ #K assumption
255 |2:
256   #m' #t #q' #II #H1 #H2
257   normalize
258   change with (orb ??) in H2:(??%?);
259   cases (inclusive_disjunction_true … H2)
260   [1:
261     #K
262     <(eq_a_to_eq … K) >H1 %
263   |2:
264     #K
265     >II
266     try assumption
267     cases (is_a t a)
268     normalize
269     %
270   ]
271 ]
272qed.
273
274lemma is_a_true_to_is_in:
275  ∀n: nat.
276  ∀x: addressing_mode.
277  ∀tag: addressing_mode_tag.
278  ∀supervector: Vector addressing_mode_tag n.
279  mem addressing_mode_tag eq_a n supervector tag →
280    is_a tag x = true →
281      is_in … supervector x.
282  #n #x #tag #supervector
283  elim supervector
284  [1:
285    #absurd cases absurd
286  |2:
287    #n' #hd #tl #inductive_hypothesis
288    whd in match (mem … eq_a (S n') (hd:::tl) tag);
289    @eq_a_elim normalize nodelta
290    [1:
291      #tag_hd_eq #irrelevant
292      whd in match (is_in (S n') (hd:::tl) x);
293      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
294      @I
295    |2:
296      #tag_hd_neq
297      whd in match (is_in (S n') (hd:::tl) x);
298      change with (
299        mem … eq_a n' tl tag)
300          in match (fold_right … n' ? false tl);
301      #mem_hyp #is_a_hyp
302      cases(is_a hd x)
303      [1:
304        normalize nodelta //
305      |2:
306        normalize nodelta
307        @inductive_hypothesis assumption
308      ]
309    ]
310  ]
311qed.
312
313record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
314{
315  subaddressing_modeel:> addressing_mode;
316  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
317}.
318
319coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
320 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
321
322coercion mk_subaddressing_mode :
323 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
324  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
325 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
326
327lemma is_in_subvector_is_in_supervector:
328  ∀m, n: nat.
329  ∀subvector: Vector addressing_mode_tag m.
330  ∀supervector: Vector addressing_mode_tag n.
331  ∀element: addressing_mode.
332    subvector_with … eq_a subvector supervector →
333      is_in m subvector element → is_in n supervector element.
334  #m #n #subvector #supervector #element
335  elim subvector
336  [1:
337    #subvector_with_proof #is_in_proof
338    cases is_in_proof
339  |2:
340    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
341    whd in match (is_in … (hd':::tl') element);
342    cases (is_a_decidable hd' element)
343    [1:
344      #is_a_true >is_a_true
345      #irrelevant
346      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
347      @(is_a_true_to_is_in … is_a_true)
348      lapply(subvector_with_proof)
349      cases(mem … eq_a n supervector hd') //
350    |2:
351      #is_a_false >is_a_false normalize nodelta
352      #assm
353      @inductive_hypothesis
354      [1:
355        generalize in match subvector_with_proof;
356        whd in match (subvector_with … eq_a (hd':::tl') supervector);
357        cases(mem_decidable n supervector hd')
358        [1:
359          #mem_true >mem_true normalize nodelta
360          #assm assumption
361        |2:
362          #mem_false >mem_false #absurd
363          cases absurd
364        ]
365      |2:
366        assumption
367      ]
368    ]
369  ]
370qed.
371
372
373let rec subaddressing_mode_elim_type
374  (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
375    (Q: fixed_v → Prop)
376     (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
377       on v: Prop ≝
378  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
379  [ VEmpty         ⇒ λm_refl. λv_refl. Q origaddr
380  | VCons n' hd tl ⇒ λm_refl. λv_refl.
381    let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
382    in
383    match hd return λa: addressing_mode_tag. a = hd → ? with
384    [ addr11            ⇒ λhd_refl. (∀w: Word11.      Q (ADDR11 w)) → tail_call
385    | addr16            ⇒ λhd_refl. (∀w: Word.        Q (ADDR16 w)) → tail_call
386    | direct            ⇒ λhd_refl. (∀w: Byte.        Q (DIRECT w)) → tail_call
387    | indirect          ⇒ λhd_refl. (∀w: Bit.         Q (INDIRECT w)) → tail_call
388    | ext_indirect      ⇒ λhd_refl. (∀w: Bit.         Q (EXT_INDIRECT w)) → tail_call
389    | acc_a             ⇒ λhd_refl.                  Q ACC_A → tail_call
390    | registr           ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
391    | acc_b             ⇒ λhd_refl.                  Q ACC_B → tail_call
392    | dptr              ⇒ λhd_refl.                  Q DPTR → tail_call
393    | data              ⇒ λhd_refl. (∀w: Byte.        Q (DATA w))  → tail_call
394    | data16            ⇒ λhd_refl. (∀w: Word.        Q (DATA16 w)) → tail_call
395    | acc_dptr          ⇒ λhd_refl.                  Q ACC_DPTR → tail_call
396    | acc_pc            ⇒ λhd_refl.                  Q ACC_PC → tail_call
397    | ext_indirect_dptr ⇒ λhd_refl.                  Q EXT_INDIRECT_DPTR → tail_call
398    | indirect_dptr     ⇒ λhd_refl.                  Q INDIRECT_DPTR → tail_call
399    | carry             ⇒ λhd_refl.                  Q CARRY → tail_call
400    | bit_addr          ⇒ λhd_refl. (∀w: Byte.        Q (BIT_ADDR w)) → tail_call
401    | n_bit_addr        ⇒ λhd_refl. (∀w: Byte.        Q (N_BIT_ADDR w)) → tail_call
402    | relative          ⇒ λhd_refl. (∀w: Byte.        Q (RELATIVE w)) → tail_call
403    ] (refl … hd)
404  ] (refl … n) (refl_jmeq … v).
405  [20:
406    generalize in match proof; destruct
407    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
408    cases (mem … eq_a ? fixed_v hd) normalize nodelta
409    [1:
410      whd in match (subvector_with … eq_a tl fixed_v);
411      #assm assumption
412    |2:
413      normalize in ⊢ (% → ?);
414      #absurd cases absurd
415    ]
416  ]
417  @(is_in_subvector_is_in_supervector … proof)
418  destruct @I
419qed.
420
421lemma subaddressing_mode_elim0:
422  ∀n: nat.
423  ∀v: Vector addressing_mode_tag (S n).
424  ∀addr: v.
425  ∀Q: v → Prop.
426  ∀m,w,H.
427  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
428   subaddressing_mode_elim_type n v addr Q m w H.
429 #n #v #addr #Q #m #w elim w
430 [ /2/
431 | #n' #hd #tl #IH cases hd #H
432   #INV whd #PO @IH #xaddr cases xaddr *
433   try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
434   @ALREADYSEEN ]
435qed.
436
437lemma subaddressing_mode_elim:
438  ∀n: nat.
439  ∀v: Vector addressing_mode_tag (S n).
440  ∀addr: v.
441  ∀Q: v → Prop.
442   subaddressing_mode_elim_type n v addr Q (S n) v ?.
443[ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
444| @subvector_with_refl @eq_a_reflexive
445]
446qed.
447 
448inductive preinstruction (A: Type[0]) : Type[0] ≝
449  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
450| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
451| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
452| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
453| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
454| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
455| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
456| DA: [[acc_a]] → preinstruction A
457
458(* conditional jumps *)
459| JC: A → preinstruction A
460| JNC: A → preinstruction A
461| JB: [[bit_addr]] → A → preinstruction A
462| JNB: [[bit_addr]] → A → preinstruction A
463| JBC: [[bit_addr]] → A → preinstruction A
464| JZ: A → preinstruction A
465| JNZ: A → preinstruction A
466| CJNE:
467   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
468| DJNZ: [[registr ; direct]] → A → preinstruction A
469 (* logical operations *)
470| ANL:
471   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
472   [[direct]] × [[ acc_a ; data ]] ⊎
473   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
474| ORL:
475   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
476   [[direct]] × [[ acc_a ; data ]] ⊎
477   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
478| XRL:
479   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
480   [[direct]] × [[ acc_a ; data ]] → preinstruction A
481| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
482| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
483| RL: [[acc_a]] → preinstruction A
484| RLC: [[acc_a]] → preinstruction A
485| RR: [[acc_a]] → preinstruction A
486| RRC: [[acc_a]] → preinstruction A
487| SWAP: [[acc_a]] → preinstruction A
488
489 (* data transfer *)
490| MOV:
491    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
492    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
493    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
494    [[dptr]] × [[data16]] ⊎
495    [[carry]] × [[bit_addr]] ⊎
496    [[bit_addr]] × [[carry]] → preinstruction A
497| MOVX:
498    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
499    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
500| SETB: [[ carry ; bit_addr ]] → preinstruction A
501| PUSH: [[direct]] → preinstruction A
502| POP: [[direct]] → preinstruction A
503| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
504| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
505
506 (* program branching *)
507| RET: preinstruction A
508| RETI: preinstruction A
509| NOP: preinstruction A.
510
511definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
512  λi, j.
513  match i with
514  [ ADD arg1 arg2 ⇒
515    match j with
516    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
517    | _ ⇒ false
518    ]
519  | ADDC arg1 arg2 ⇒
520    match j with
521    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
522    | _ ⇒ false
523    ]
524  | SUBB arg1 arg2 ⇒
525    match j with
526    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
527    | _ ⇒ false
528    ]
529  | INC arg ⇒
530    match j with
531    [ INC arg' ⇒ eq_addressing_mode arg arg'
532    | _ ⇒ false
533    ]
534  | DEC arg ⇒
535    match j with
536    [ DEC arg' ⇒ eq_addressing_mode arg arg'
537    | _ ⇒ false
538    ]
539  | MUL arg1 arg2 ⇒
540    match j with
541    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
542    | _ ⇒ false
543    ]
544  | DIV arg1 arg2 ⇒
545    match j with
546    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
547    | _ ⇒ false
548    ]
549  | DA arg ⇒
550    match j with
551    [ DA arg' ⇒ eq_addressing_mode arg arg'
552    | _ ⇒ false
553    ]
554  | JC arg ⇒
555    match j with
556    [ JC arg' ⇒ eq_addressing_mode arg arg'
557    | _ ⇒ false
558    ]
559  | JNC arg ⇒
560    match j with
561    [ JNC arg' ⇒ eq_addressing_mode arg arg'
562    | _ ⇒ false
563    ]
564  | JB arg1 arg2 ⇒
565    match j with
566    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
567    | _ ⇒ false
568    ]
569  | JNB arg1 arg2 ⇒
570    match j with
571    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
572    | _ ⇒ false
573    ]
574  | JBC arg1 arg2 ⇒
575    match j with
576    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
577    | _ ⇒ false
578    ]
579  | JZ arg ⇒
580    match j with
581    [ JZ arg' ⇒ eq_addressing_mode arg arg'
582    | _ ⇒ false
583    ]
584  | JNZ arg ⇒
585    match j with
586    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
587    | _ ⇒ false
588    ]
589  | CJNE arg1 arg2 ⇒
590    match j with
591    [ CJNE arg1' arg2' ⇒
592      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
593      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
594      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
595        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
596    | _ ⇒ false
597    ]
598  | DJNZ arg1 arg2 ⇒
599    match j with
600    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
601    | _ ⇒ false
602    ]
603  | CLR arg ⇒
604    match j with
605    [ CLR arg' ⇒ eq_addressing_mode arg arg'
606    | _ ⇒ false
607    ]
608  | CPL arg ⇒
609    match j with
610    [ CPL arg' ⇒ eq_addressing_mode arg arg'
611    | _ ⇒ false
612    ]
613  | RL arg ⇒
614    match j with
615    [ RL arg' ⇒ eq_addressing_mode arg arg'
616    | _ ⇒ false
617    ]
618  | RLC arg ⇒
619    match j with
620    [ RLC arg' ⇒ eq_addressing_mode arg arg'
621    | _ ⇒ false
622    ]
623  | RR arg ⇒
624    match j with
625    [ RR arg' ⇒ eq_addressing_mode arg arg'
626    | _ ⇒ false
627    ]
628  | RRC arg ⇒
629    match j with
630    [ RRC arg' ⇒ eq_addressing_mode arg arg'
631    | _ ⇒ false
632    ]
633  | SWAP arg ⇒
634    match j with
635    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
636    | _ ⇒ false
637    ]
638  | SETB arg ⇒
639    match j with
640    [ SETB arg' ⇒ eq_addressing_mode arg arg'
641    | _ ⇒ false
642    ]
643  | PUSH arg ⇒
644    match j with
645    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
646    | _ ⇒ false
647    ]
648  | POP arg ⇒
649    match j with
650    [ POP arg' ⇒ eq_addressing_mode arg arg'
651    | _ ⇒ false
652    ]
653  | XCH arg1 arg2 ⇒
654    match j with
655    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
656    | _ ⇒ false
657    ]
658  | XCHD arg1 arg2 ⇒
659    match j with
660    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
661    | _ ⇒ false
662    ]
663  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
664  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
665  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
666  | MOVX arg ⇒
667    match j with
668    [ MOVX arg' ⇒
669      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
670      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
671      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
672        sum_eq arg arg'
673    | _ ⇒ false
674    ]
675  | XRL arg ⇒
676    match j with
677    [ XRL arg' ⇒
678      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
679      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
680      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
681        sum_eq arg arg'
682    | _ ⇒ false
683    ]
684  | ORL arg ⇒
685    match j with
686    [ ORL arg' ⇒
687      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
688      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
689      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
690      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
691      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
692        sum_eq arg arg'
693    | _ ⇒ false
694    ]
695  | ANL arg ⇒
696    match j with
697    [ ANL arg' ⇒
698      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
699      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
700      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
701      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
702      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
703        sum_eq arg arg'
704    | _ ⇒ false
705    ]
706  | MOV arg ⇒
707    match j with
708    [ MOV arg' ⇒
709      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
710      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
711      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
712      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
713      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
714      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
715      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
716      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
717      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
718      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
719      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
720        sum_eq_5 arg arg'
721    | _ ⇒ false
722    ]
723  ].
724
725lemma eq_preinstruction_refl:
726  ∀i.
727    eq_preinstruction i i = true.
728  #i cases i try #arg1 try #arg2
729  try @eq_addressing_mode_refl
730  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
731    whd in ⊢ (??%?); try %
732    >eq_addressing_mode_refl
733    >eq_addressing_mode_refl %
734  |13,15:
735    whd in ⊢ (??%?);
736    cases arg1
737    [*:
738      #arg1_left normalize nodelta
739      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
740    ]
741  |11,12:
742    whd in ⊢ (??%?);
743    cases arg1
744    [1:
745      #arg1_left normalize nodelta
746      >(eq_sum_refl …)
747      [1: % | 2,3: #arg @eq_prod_refl ]
748      @eq_addressing_mode_refl
749    |2:
750      #arg1_left normalize nodelta
751      @eq_prod_refl [*: @eq_addressing_mode_refl ]
752    |3:
753      #arg1_left normalize nodelta
754      >(eq_sum_refl …)
755      [1:
756        %
757      |2,3:
758        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
759      ]
760    |4:
761      #arg1_left normalize nodelta
762      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
763    ]
764  |14:
765    whd in ⊢ (??%?);
766    cases arg1
767    [1:
768      #arg1_left normalize nodelta
769      @eq_sum_refl
770      [1:
771        #arg @eq_sum_refl
772        [1:
773          #arg @eq_sum_refl
774          [1:
775            #arg @eq_sum_refl
776            [1:
777              #arg @eq_prod_refl
778              [*:
779                @eq_addressing_mode_refl
780              ]
781            |2:
782              #arg @eq_prod_refl
783              [*:
784                #arg @eq_addressing_mode_refl
785              ]
786            ]
787          |2:
788            #arg @eq_prod_refl
789            [*:
790              #arg @eq_addressing_mode_refl
791            ]
792          ]
793        |2:
794          #arg @eq_prod_refl
795          [*:
796            #arg @eq_addressing_mode_refl
797          ]
798        ]
799      |2:
800        #arg @eq_prod_refl
801        [*:
802          #arg @eq_addressing_mode_refl
803        ]
804      ]
805    |2:
806      #arg1_right normalize nodelta
807      @eq_prod_refl
808      [*:
809        #arg @eq_addressing_mode_refl
810      ]
811    ]
812  |*:
813    whd in ⊢ (??%?);
814    cases arg1
815    [*:
816      #arg1 >eq_sum_refl
817      [1,4:
818        @eq_addressing_mode_refl
819      |2,3,5,6:
820        #arg @eq_prod_refl
821        [*:
822          #arg @eq_addressing_mode_refl
823        ]
824      ]
825    ]
826  ]
827qed.
828
829inductive instruction: Type[0] ≝
830  | ACALL: [[addr11]] → instruction
831  | LCALL: [[addr16]] → instruction
832  | AJMP: [[addr11]] → instruction
833  | LJMP: [[addr16]] → instruction
834  | SJMP: [[relative]] → instruction
835  | JMP: [[indirect_dptr]] → instruction
836  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
837  | RealInstruction: preinstruction [[ relative ]] → instruction.
838 
839coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
840  RealInstruction on _p: preinstruction ? to instruction.
841
842definition eq_instruction: instruction → instruction → bool ≝
843  λi, j.
844  match i with
845  [ ACALL arg ⇒
846    match j with
847    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
848    | _ ⇒ false
849    ]
850  | LCALL arg ⇒
851    match j with
852    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
853    | _ ⇒ false
854    ]
855  | AJMP arg ⇒
856    match j with
857    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
858    | _ ⇒ false
859    ]
860  | LJMP arg ⇒
861    match j with
862    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
863    | _ ⇒ false
864    ]
865  | SJMP arg ⇒
866    match j with
867    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
868    | _ ⇒ false
869    ]
870  | JMP arg ⇒
871    match j with
872    [ JMP arg' ⇒ eq_addressing_mode arg arg'
873    | _ ⇒ false
874    ]
875  | MOVC arg1 arg2 ⇒
876    match j with
877    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
878    | _ ⇒ false
879    ]
880  | RealInstruction instr ⇒
881    match j with
882    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
883    | _ ⇒ false
884    ]
885  ].
886 
887lemma eq_instruction_refl:
888  ∀i. eq_instruction i i = true.
889  #i cases i [*: #arg1 ]
890  try @eq_addressing_mode_refl
891  try @eq_preinstruction_refl
892  #arg2 whd in ⊢ (??%?);
893  >eq_addressing_mode_refl >eq_addressing_mode_refl %
894qed.
895
896lemma eq_instruction_to_eq:
897  ∀i1, i2: instruction.
898    eq_instruction i1 i2 = true → i1 ≃ i2.
899  #i1 #i2
900  cases i1 cases i2 cases daemon (* easy but tedious
901  [1,10,19,28,37,46:
902    #arg1 #arg2
903    whd in match (eq_instruction ??);
904    cases arg1 #subaddressing_mode
905    cases subaddressing_mode
906    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
907    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
908    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
909    #word11 #irrelevant
910    cases arg2 #subaddressing_mode
911    cases subaddressing_mode
912    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
913    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
914    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
915    #word11' #irrelevant normalize nodelta
916    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
917qed.
918
919inductive pseudo_instruction: Type[0] ≝
920  | Instruction: preinstruction Identifier → pseudo_instruction
921  | Comment: String → pseudo_instruction
922  | Cost: costlabel → pseudo_instruction
923  | Jmp: Identifier → pseudo_instruction
924  | Call: Identifier → pseudo_instruction
925  | Mov: [[dptr]] → Identifier → pseudo_instruction.
926
927definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
928definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
929definition assembly_program ≝ list instruction.
930definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
931
932(* labels & instructions *)
933definition instruction_has_label ≝
934  λid: Identifier.
935  λi.
936  match i with
937  [ Jmp j ⇒ j = id
938  | Call j ⇒ j = id
939  | Instruction instr ⇒
940    match instr with
941    [ JC j ⇒ j = id
942    | JNC j ⇒ j = id
943    | JZ j ⇒ j = id
944    | JNZ j ⇒ j = id
945    | JB _ j ⇒ j = id
946    | JBC _ j ⇒ j = id
947    | DJNZ _ j ⇒ j = id
948    | CJNE _ j ⇒ j = id
949    | _ ⇒ False
950    ]
951  | _ ⇒ False
952  ].
Note: See TracBrowser for help on using the repository browser.