source: src/ASM/ASM.ma @ 2757

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

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