source: src/ASM/ASM.ma @ 2708

Last change on this file since 2708 was 2708, checked in by tranquil, 7 years ago

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File size: 32.7 KB
Line 
1include "ASM/BitVector.ma".
2include "common/Identifiers.ma".
3include "common/CostLabel.ma".
4include "common/LabelledObjects.ma".
5include "joint/String.ma".
6
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_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
260qed.
261
262corollary 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  ]
279qed.
280
281lemma 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 ]
305qed.
306
307lemma 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  ]
344qed.
345
346record 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
352coercion 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
355coercion 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
360lemma 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  ]
403qed.
404
405(* XXX: move back into ASM.ma *)
406lemma 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  ]
429qed.
430
431let 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
468qed.
469
470lemma 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  ]
487qed.
488
489lemma 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  ]
500qed.
501 
502inductive 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| JMP: [[indirect_dptr]] → preinstruction A.
565
566definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
567  λi, j.
568  match i with
569  [ ADD arg1 arg2 ⇒
570    match j with
571    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
572    | _ ⇒ false
573    ]
574  | ADDC arg1 arg2 ⇒
575    match j with
576    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
577    | _ ⇒ false
578    ]
579  | SUBB arg1 arg2 ⇒
580    match j with
581    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
582    | _ ⇒ false
583    ]
584  | INC arg ⇒
585    match j with
586    [ INC arg' ⇒ eq_addressing_mode arg arg'
587    | _ ⇒ false
588    ]
589  | DEC arg ⇒
590    match j with
591    [ DEC arg' ⇒ eq_addressing_mode arg arg'
592    | _ ⇒ false
593    ]
594  | MUL arg1 arg2 ⇒
595    match j with
596    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
597    | _ ⇒ false
598    ]
599  | DIV arg1 arg2 ⇒
600    match j with
601    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
602    | _ ⇒ false
603    ]
604  | DA arg ⇒
605    match j with
606    [ DA arg' ⇒ eq_addressing_mode arg arg'
607    | _ ⇒ false
608    ]
609  | JC arg ⇒
610    match j with
611    [ JC arg' ⇒ eq_addressing_mode arg arg'
612    | _ ⇒ false
613    ]
614  | JNC arg ⇒
615    match j with
616    [ JNC arg' ⇒ eq_addressing_mode arg arg'
617    | _ ⇒ false
618    ]
619  | JB arg1 arg2 ⇒
620    match j with
621    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
622    | _ ⇒ false
623    ]
624  | JNB arg1 arg2 ⇒
625    match j with
626    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
627    | _ ⇒ false
628    ]
629  | JBC arg1 arg2 ⇒
630    match j with
631    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
632    | _ ⇒ false
633    ]
634  | JZ arg ⇒
635    match j with
636    [ JZ arg' ⇒ eq_addressing_mode arg arg'
637    | _ ⇒ false
638    ]
639  | JNZ arg ⇒
640    match j with
641    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
642    | _ ⇒ false
643    ]
644  | JMP arg ⇒
645    match j with
646    [ JMP arg' ⇒ eq_addressing_mode arg arg'
647    | _ ⇒ false
648    ]
649  | CJNE arg1 arg2 ⇒
650    match j with
651    [ CJNE arg1' arg2' ⇒
652      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
653      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
654      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
655        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
656    | _ ⇒ false
657    ]
658  | DJNZ arg1 arg2 ⇒
659    match j with
660    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
661    | _ ⇒ false
662    ]
663  | CLR arg ⇒
664    match j with
665    [ CLR arg' ⇒ eq_addressing_mode arg arg'
666    | _ ⇒ false
667    ]
668  | CPL arg ⇒
669    match j with
670    [ CPL arg' ⇒ eq_addressing_mode arg arg'
671    | _ ⇒ false
672    ]
673  | RL arg ⇒
674    match j with
675    [ RL arg' ⇒ eq_addressing_mode arg arg'
676    | _ ⇒ false
677    ]
678  | RLC arg ⇒
679    match j with
680    [ RLC arg' ⇒ eq_addressing_mode arg arg'
681    | _ ⇒ false
682    ]
683  | RR arg ⇒
684    match j with
685    [ RR arg' ⇒ eq_addressing_mode arg arg'
686    | _ ⇒ false
687    ]
688  | RRC arg ⇒
689    match j with
690    [ RRC arg' ⇒ eq_addressing_mode arg arg'
691    | _ ⇒ false
692    ]
693  | SWAP arg ⇒
694    match j with
695    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
696    | _ ⇒ false
697    ]
698  | SETB arg ⇒
699    match j with
700    [ SETB arg' ⇒ eq_addressing_mode arg arg'
701    | _ ⇒ false
702    ]
703  | PUSH arg ⇒
704    match j with
705    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
706    | _ ⇒ false
707    ]
708  | POP arg ⇒
709    match j with
710    [ POP arg' ⇒ eq_addressing_mode arg arg'
711    | _ ⇒ false
712    ]
713  | XCH arg1 arg2 ⇒
714    match j with
715    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
716    | _ ⇒ false
717    ]
718  | XCHD arg1 arg2 ⇒
719    match j with
720    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
721    | _ ⇒ false
722    ]
723  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
724  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
725  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
726  | MOVX arg ⇒
727    match j with
728    [ MOVX arg' ⇒
729      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
730      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
731      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
732        sum_eq arg arg'
733    | _ ⇒ false
734    ]
735  | XRL arg ⇒
736    match j with
737    [ XRL arg' ⇒
738      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
739      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
740      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
741        sum_eq arg arg'
742    | _ ⇒ false
743    ]
744  | ORL arg ⇒
745    match j with
746    [ ORL arg' ⇒
747      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
748      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
749      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
750      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
751      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
752        sum_eq arg arg'
753    | _ ⇒ false
754    ]
755  | ANL arg ⇒
756    match j with
757    [ ANL arg' ⇒
758      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
759      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
760      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
761      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
762      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
763        sum_eq arg arg'
764    | _ ⇒ false
765    ]
766  | MOV arg ⇒
767    match j with
768    [ MOV arg' ⇒
769      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
770      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
771      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
772      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
773      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
774      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
775      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
776      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
777      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
778      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
779      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
780        sum_eq_5 arg arg'
781    | _ ⇒ false
782    ]
783  ].
784
785lemma eq_preinstruction_refl:
786  ∀i.
787    eq_preinstruction i i = true.
788  #i cases i try #arg1 try #arg2
789  try @eq_addressing_mode_refl
790  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
791    whd in ⊢ (??%?); try %
792    >eq_addressing_mode_refl
793    >eq_addressing_mode_refl %
794  |13,15:
795    whd in ⊢ (??%?);
796    cases arg1
797    [*:
798      #arg1_left normalize nodelta
799      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
800    ]
801  |11,12:
802    whd in ⊢ (??%?);
803    cases arg1
804    [1:
805      #arg1_left normalize nodelta
806      >(eq_sum_refl …)
807      [1: % | 2,3: #arg @eq_prod_refl ]
808      @eq_addressing_mode_refl
809    |2:
810      #arg1_left normalize nodelta
811      @eq_prod_refl [*: @eq_addressing_mode_refl ]
812    |3:
813      #arg1_left normalize nodelta
814      >(eq_sum_refl …)
815      [1:
816        %
817      |2,3:
818        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
819      ]
820    |4:
821      #arg1_left normalize nodelta
822      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
823    ]
824  |14:
825    whd in ⊢ (??%?);
826    cases arg1
827    [1:
828      #arg1_left normalize nodelta
829      @eq_sum_refl
830      [1:
831        #arg @eq_sum_refl
832        [1:
833          #arg @eq_sum_refl
834          [1:
835            #arg @eq_sum_refl
836            [1:
837              #arg @eq_prod_refl
838              [*:
839                @eq_addressing_mode_refl
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        #arg @eq_prod_refl
861        [*:
862          #arg @eq_addressing_mode_refl
863        ]
864      ]
865    |2:
866      #arg1_right normalize nodelta
867      @eq_prod_refl
868      [*:
869        #arg @eq_addressing_mode_refl
870      ]
871    ]
872  |*:
873    whd in ⊢ (??%?);
874    cases arg1
875    [*:
876      #arg1 >eq_sum_refl
877      [1,4:
878        @eq_addressing_mode_refl
879      |2,3,5,6:
880        #arg @eq_prod_refl
881        [*:
882          #arg @eq_addressing_mode_refl
883        ]
884      ]
885    ]
886  ]
887qed.
888
889inductive instruction: Type[0] ≝
890  | ACALL: [[addr11]] → instruction
891  | LCALL: [[addr16]] → instruction
892  | AJMP: [[addr11]] → instruction
893  | LJMP: [[addr16]] → instruction
894  | SJMP: [[relative]] → instruction
895  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
896  | RealInstruction: preinstruction [[ relative ]] → instruction.
897 
898coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
899  RealInstruction on _p: preinstruction ? to instruction.
900
901definition eq_instruction: instruction → instruction → bool ≝
902  λi, j.
903  match i with
904  [ ACALL arg ⇒
905    match j with
906    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
907    | _ ⇒ false
908    ]
909  | LCALL arg ⇒
910    match j with
911    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
912    | _ ⇒ false
913    ]
914  | AJMP arg ⇒
915    match j with
916    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
917    | _ ⇒ false
918    ]
919  | LJMP arg ⇒
920    match j with
921    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
922    | _ ⇒ false
923    ]
924  | SJMP arg ⇒
925    match j with
926    [ SJMP 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 
941lemma 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 %
948qed.
949
950lemma 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) % *)
971qed.
972
973inductive word_side : Type[0] ≝ HIGH : word_side | LOW : word_side.
974
975inductive pseudo_instruction: Type[0] ≝
976  | Instruction: preinstruction Identifier → pseudo_instruction
977  | Comment: String → pseudo_instruction
978  | Cost: costlabel → pseudo_instruction
979  | Jmp: Identifier → pseudo_instruction
980  | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction
981  | MovSuccessor : [[ acc_a ; direct ; registr ]] → word_side → Identifier → pseudo_instruction
982  | Call: Identifier → pseudo_instruction
983  | Mov: [[dptr]] → Identifier → pseudo_instruction.
984
985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
986definition preamble ≝ list (Identifier × Word).
987definition assembly_program ≝ list instruction.
988definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
989
990(* labels & instructions *)
991definition instruction_has_label ≝
992  λid: Identifier.
993  λi.
994  match i with
995  [ Jmp j ⇒ j = id
996  | Call j ⇒ j = id
997  | Instruction instr ⇒
998    match instr with
999    [ JC j ⇒ j = id
1000    | JNC j ⇒ j = id
1001    | JZ j ⇒ j = id
1002    | JNZ j ⇒ j = id
1003    | JB _ j ⇒ j = id
1004    | JNB _ j ⇒ j = id
1005    | JBC _ j ⇒ j = id
1006    | DJNZ _ j ⇒ j = id
1007    | CJNE _ j ⇒ j = id
1008    | _ ⇒ False
1009    ]
1010  | _ ⇒ False
1011  ].
1012
1013
1014(* If instruction i is a jump, then there will be something in the policy at
1015 * position i *)
1016definition is_jump' ≝
1017  λx:preinstruction Identifier.
1018  match x with
1019  [ JC _ ⇒ true
1020  | JNC _ ⇒ true
1021  | JZ _ ⇒ true
1022  | JNZ _ ⇒ true
1023  | JB _ _ ⇒ true
1024  | JNB _ _ ⇒ true
1025  | JBC _ _ ⇒ true
1026  | CJNE _ _ ⇒ true
1027  | DJNZ _ _ ⇒ true
1028  | _ ⇒ false
1029  ].
1030
1031definition is_relative_jump ≝
1032  λinstr:pseudo_instruction.
1033  match instr with
1034  [ Instruction i ⇒ is_jump' i
1035  | _             ⇒ false
1036  ].
1037   
1038definition is_jump ≝
1039  λinstr:pseudo_instruction.
1040  match instr with
1041  [ Instruction i   ⇒ is_jump' i
1042  | Call _ ⇒ true
1043  | Jmp _ ⇒ true
1044  | _ ⇒ false
1045  ].
1046
1047definition is_call ≝
1048  λinstr:pseudo_instruction.
1049  match instr with
1050  [ Call _ ⇒ true
1051  | _ ⇒ false
1052  ].
1053 
1054definition is_jump_to ≝
1055  λx:pseudo_instruction.λd:Identifier.
1056  match x with
1057  [ Instruction i ⇒ match i with
1058    [ JC j ⇒ d = j
1059    | JNC j ⇒ d = j
1060    | JZ j ⇒ d = j
1061    | JNZ j ⇒ d = j
1062    | JB _ j ⇒ d = j
1063    | JNB _ j ⇒ d = j
1064    | JBC _ j ⇒ d = j
1065    | CJNE _ j ⇒ d = j
1066    | DJNZ _ j ⇒ d = j
1067    | _ ⇒ False
1068    ]
1069  | Call c ⇒ d = c
1070  | Jmp j ⇒ d = j
1071  | _ ⇒ False
1072  ].
Note: See TracBrowser for help on using the repository browser.