source: src/ASM/ASM.ma

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

added invariant that costlabels are only assigned to NOPs (not proved
yet, assembly has a new cases daemon)

File size: 39.1 KB
Line 
1include "common/CostLabel.ma".
2include "common/LabelledObjects.ma".
3include "common/AST.ma".
4include "joint/String.ma".
5include "ASM/BitVectorTrie.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: [[acc_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  | Call: Identifier → pseudo_instruction
982  | Mov: ([[dptr]] ⊎ ([[ acc_a ; direct ; registr ]] × word_side)) →
983    Identifier → Word → pseudo_instruction.
984
985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
986
987definition assembly_program ≝ list instruction.
988
989definition fetch_pseudo_instruction:
990 ∀code_mem:list labelled_instruction. ∀pc:Word.
991  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
992  λcode_mem.
993  λpc: Word.
994  λpc_ok.
995    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
996    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
997      〈instr, new_pc〉.
998
999lemma snd_fetch_pseudo_instruction:
1000 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
1001 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
1002 #lft #rgt #_ %
1003qed.
1004
1005lemma fetch_pseudo_instruction_vsplit:
1006 ∀instr_list,ppc,ppc_ok.
1007  ∃pre,suff,lbl.
1008   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
1009#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
1010cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
1011lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
1012#EQ %{lbl0} @EQ
1013qed.
1014
1015lemma fetch_pseudo_instruction_append:
1016 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
1017  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
1018  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
1019  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
1020 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
1021 cut (|l1| + nat_of_bitvector … ppc < 2^16)
1022 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
1023 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
1024 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
1025 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
1026 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
1027 #lbl #instr normalize nodelta >add_associative %
1028qed.
1029
1030(* labels & instructions *)
1031definition instruction_has_label ≝
1032  λid: Identifier.
1033  λi.
1034  match i with
1035  [ Jmp j ⇒ j = id
1036  | Call j ⇒ j = id
1037  | Instruction instr ⇒
1038    match instr with
1039    [ JC j ⇒ j = id
1040    | JNC j ⇒ j = id
1041    | JZ j ⇒ j = id
1042    | JNZ j ⇒ j = id
1043    | JB _ j ⇒ j = id
1044    | JNB _ j ⇒ j = id
1045    | JBC _ j ⇒ j = id
1046    | DJNZ _ j ⇒ j = id
1047    | CJNE _ j ⇒ j = id
1048    | _ ⇒ False
1049    ]
1050  | _ ⇒ False
1051  ].
1052
1053(* If instruction i is a jump, then there will be something in the policy at
1054 * position i *)
1055definition is_jump' ≝
1056  λx:preinstruction Identifier.
1057  match x with
1058  [ JC _ ⇒ true
1059  | JNC _ ⇒ true
1060  | JZ _ ⇒ true
1061  | JNZ _ ⇒ true
1062  | JB _ _ ⇒ true
1063  | JNB _ _ ⇒ true
1064  | JBC _ _ ⇒ true
1065  | CJNE _ _ ⇒ true
1066  | DJNZ _ _ ⇒ true
1067  | _ ⇒ false
1068  ].
1069
1070definition is_relative_jump ≝
1071  λinstr:pseudo_instruction.
1072  match instr with
1073  [ Instruction i ⇒ is_jump' i
1074  | _             ⇒ false
1075  ].
1076   
1077definition is_jump ≝
1078  λinstr:pseudo_instruction.
1079  match instr with
1080  [ Instruction i   ⇒ is_jump' i
1081  | Call _ ⇒ true
1082  | Jmp _ ⇒ true
1083  | _ ⇒ false
1084  ].
1085
1086definition is_call ≝
1087  λinstr:pseudo_instruction.
1088  match instr with
1089  [ Call _ ⇒ true
1090  | _ ⇒ false
1091  ].
1092 
1093definition is_jump_to ≝
1094  λx:pseudo_instruction.λd:Identifier.
1095  match x with
1096  [ Instruction i ⇒ match i with
1097    [ JC j ⇒ d = j
1098    | JNC j ⇒ d = j
1099    | JZ j ⇒ d = j
1100    | JNZ j ⇒ d = j
1101    | JB _ j ⇒ d = j
1102    | JNB _ j ⇒ d = j
1103    | JBC _ j ⇒ d = j
1104    | CJNE _ j ⇒ d = j
1105    | DJNZ _ j ⇒ d = j
1106    | _ ⇒ False
1107    ]
1108  | Call c ⇒ d = c
1109  | Jmp j ⇒ d = j
1110  | _ ⇒ False
1111  ].
1112
1113definition is_well_labelled_p ≝
1114  λinstr_list.
1115  ∀id: Identifier.
1116  ∀ppc.
1117  ∀ppc_ok.
1118  ∀i.
1119    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
1120      (instruction_has_label id i →
1121        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
1122      (is_jump_to i id →
1123        occurs_exactly_once ASMTag pseudo_instruction id instr_list).
1124
1125definition asm_cost_label : ∀mem : list labelled_instruction.
1126  (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
1127λmem,w_prf.
1128match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
1129[ Cost c ⇒ Some ? c
1130| _ ⇒ None ?
1131].
1132
1133(* XXX JHM: avoid magic numbers! *)
1134definition ADDRESS_WIDTH ≝ 16.
1135definition MAX_CODE_SIZE ≝ 2^ADDRESS_WIDTH.
1136
1137definition code_size_p : list labelled_instruction → Prop ≝
1138  λcode. S (|code|) < MAX_CODE_SIZE.
1139 
1140definition code_size_opt : ∀code. option (code_size_p code) ≝
1141  λcode. nat_bound_opt MAX_CODE_SIZE (S (|code|)).
1142
1143(* The first associative list assigns symbol names to addresses in data memory.
1144   The second associative list assigns to Identifiers meant to be entry points
1145   of functions the name of the function (that lives in a different namespace) *)
1146
1147record pseudo_assembly_program : Type[0] ≝
1148{ preamble : list (Identifier × Word)
1149; code : list labelled_instruction
1150; code_size_ok: code_size_p code
1151; renamed_symbols : list (Identifier × ident)
1152; final_label : Identifier
1153(* properties *)
1154; asm_injective_costlabels :
1155  partial_injection … (asm_cost_label code)
1156; well_labelled_p : is_well_labelled_p code
1157}.
1158
1159definition object_code ≝ list Byte.
1160
1161include alias "ASM/BitVectorTrie.ma".
1162include alias "ASM/Arithmetic.ma".
1163
1164definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
1165  λpmem: BitVectorTrie Byte 16.
1166  λpc: Word.
1167    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
1168
1169definition load_code_memory0:
1170 ∀program: object_code. Σres: BitVectorTrie Byte 16.
1171  let program_size ≝ |program| in
1172   program_size ≤ 2^16 →
1173    ∀pc. ∀pc_ok: pc < program_size.
1174     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
1175
1176 λprogram. \snd
1177  (foldl_strong ?
1178   (λprefix.
1179     Σres: nat × Word × (BitVectorTrie Byte 16).
1180      let 〈i,bvi,mem〉 ≝ res in
1181      i = |prefix| ∧ bvi = bitvector_of_nat … i ∧
1182      (i ≤ 2^16 →
1183        ∀pc. ∀pc_ok: pc < |prefix|.
1184         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
1185   program
1186   (λprefix,v,tl,prf,i_mem.
1187     let 〈i,bvi,mem〉 ≝ i_mem in
1188      〈S i,increment … bvi,insert … bvi v mem〉)
1189  〈0,zero ?,Stub Byte 16〉).
1190[3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2
1191| % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*)
1192| cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ)
1193  cases H -H * #H1 #H3 #H2 destruct (p1) %
1194  [ % [ >length_append >H1 normalize //
1195      | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ]
1196  | #LE #pc #pc_ok
1197    cases (le_to_or_lt_eq … pc_ok)
1198    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
1199      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
1200      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
1201      <H1 <plus_n_O whd in ⊢ (???%); //
1202    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix
1203      [2: /2 by lt_plus_to_lt_l/]
1204      >H2 [2: @(transitive_le … LE) //]
1205      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
1206      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3
1207      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
1208      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
1209qed.
1210
1211definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
1212 λprogram.load_code_memory0 program.
1213
1214lemma load_code_memory_ok:
1215 ∀program: object_code.
1216  let program_size ≝ |program| in
1217   program_size ≤ 2^16 →
1218    ∀pc. ∀pc_ok: pc < program_size.
1219     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1220whd in match load_code_memory; normalize nodelta #program @pi2
1221qed.
1222
1223
1224definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
1225definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
1226record labelled_object_code : Type[0] ≝
1227{ oc : object_code
1228; cm: BitVectorTrie Byte 16
1229; cm_def: cm = load_code_memory oc
1230; costlabels : costlabel_map
1231; symboltable : symboltable_type
1232; final_pc : Word
1233(* properties *)
1234; oc_injective_costlabels :
1235  partial_injection … (λpc.lookup_opt … pc costlabels)
1236; oc_costlabels_are_zero : (* this will imply that cost labels are only assigned to nops *)
1237  ∀ppc,l.lookup_opt … ppc costlabels = Some ? l →
1238  lookup … ppc cm (zero …) = zero …
1239}.
Note: See TracBrowser for help on using the repository browser.