source: src/ASM/ASM.ma @ 2645

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