source: src/ASM/AssemblyProof.ma @ 2111

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

Cleanup: lemmas/theorems/axioms moved to the right places.

File size: 73.5 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6definition bit_elim: ∀P: bool → bool. bool ≝
7  λP.
8    P true ∧ P false.
9
10let rec bitvector_elim_internal
11  (n: nat) (P: BitVector n → bool) (m: nat)
12    on m:
13      m ≤ n → BitVector (n - m) → bool ≝
14  match m return λm. m ≤ n → BitVector (n - m) → bool with
15  [ O    ⇒ λprf1. λprefix. P ?
16  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
17  ].
18  /2/
19qed.
20
21definition bitvector_elim ≝
22  λn: nat.
23  λP: BitVector n → bool.
24    bitvector_elim_internal n P n ? ?.
25  try @le_n
26  <minus_n_n @[[]]
27qed.
28
29lemma mem_monotonic_wrt_append:
30  ∀A: Type[0].
31  ∀m, o: nat.
32  ∀eq: A → A → bool.
33  ∀reflex: ∀a. eq a a = true.
34  ∀p: Vector A m.
35  ∀a: A.
36  ∀r: Vector A o.
37    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
38  #A #m #o #eq #reflex #p #a
39  elim p try (#r #assm assumption)
40  #m' #hd #tl #inductive_hypothesis #r #assm
41  normalize
42  cases (eq ??) try %
43  @inductive_hypothesis assumption
44qed.
45
46lemma subvector_multiple_append:
47  ∀A: Type[0].
48  ∀o, n: nat.
49  ∀eq: A → A → bool.
50  ∀refl: ∀a. eq a a = true.
51  ∀h: Vector A o.
52  ∀v: Vector A n.
53  ∀m: nat.
54  ∀q: Vector A m.
55    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
56  #A #o #n #eq #reflex #h #v
57  elim v try (normalize #m #irrelevant @I)
58  #m' #hd #tl #inductive_hypothesis #m #q
59  change with (bool_to_Prop (andb ??))
60  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
61  [1:
62    @mem_monotonic_wrt_append try assumption
63    @mem_monotonic_wrt_append try assumption
64    normalize >reflex %
65  |2:
66    #assm >assm
67    >vector_cons_append
68    change with (bool_to_Prop (subvector_with ??????))
69    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
70    try @associative_plus
71    @inductive_hypothesis
72  ]
73qed.
74
75lemma vector_cons_empty:
76  ∀A: Type[0].
77  ∀n: nat.
78  ∀v: Vector A n.
79    [[ ]] @@ v = v.
80  #A #n #v
81  cases v try %
82  #n' #hd #tl %
83qed.
84
85lemma is_in_monotonic_wrt_append:
86  ∀m, n: nat.
87  ∀p: Vector addressing_mode_tag m.
88  ∀q: Vector addressing_mode_tag n.
89  ∀to_search: addressing_mode.
90    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
91  #m #n #p #q #to_search #assm
92  elim q try assumption
93  #n' #hd #tl #inductive_hypothesis
94  normalize
95  cases (is_a ??) try @I
96  >inductive_hypothesis @I
97qed.
98
99corollary is_in_hd_tl:
100  ∀to_search: addressing_mode.
101  ∀hd: addressing_mode_tag.
102  ∀n: nat.
103  ∀v: Vector addressing_mode_tag n.
104    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
105  #to_search #hd #n #v
106  elim v
107  [1:
108    #absurd
109    normalize in absurd; cases absurd
110  |2:
111    #n' #hd' #tl #inductive_hypothesis #assm
112    >vector_cons_append >(vector_cons_append … hd' tl)
113    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
114    assumption
115  ]
116qed.
117 
118let rec list_addressing_mode_tags_elim
119  (n: nat) (l: Vector addressing_mode_tag (S n))
120    on l: (l → bool) → bool ≝
121  match l return λx.
122    match x with
123    [ O ⇒ λl: Vector … O. bool
124    | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool
125    ] with
126  [ VEmpty      ⇒  true 
127  | VCons len hd tl ⇒ λP.
128    let process_hd ≝
129      match hd return λhd. ∀P: hd:::tl → bool. bool with
130      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
131      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
132      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
133      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
134      | acc_a ⇒ λP.P ACC_A
135      | acc_b ⇒ λP.P ACC_B
136      | dptr ⇒ λP.P DPTR
137      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
138      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
139      | acc_dptr ⇒ λP.P ACC_DPTR
140      | acc_pc ⇒ λP.P ACC_PC
141      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
142      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
143      | carry ⇒ λP.P CARRY
144      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
145      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
146      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
147      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
148      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
149      ]
150    in
151      andb (process_hd P)
152       (match len return λx. x = len → bool with
153         [ O ⇒ λprf. true
154         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
155  ].
156  try %
157  [2:
158    cases (sym_eq ??? prf); assumption
159  |1:
160    generalize in match H; generalize in match tl;
161    destruct #tl
162    normalize in ⊢ (∀_: %. ?);
163    #H
164    whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
165    cases (is_a hd (subaddressing_modeel y tl H))
166    whd try @I normalize nodelta //
167  ]
168qed.
169
170definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
171  λa, b: addressing_mode.
172  match a with
173  [ DIRECT d ⇒
174    match b with
175    [ DIRECT e ⇒ eq_bv ? d e
176    | _ ⇒ false
177    ]
178  | INDIRECT b' ⇒
179    match b with
180    [ INDIRECT e ⇒ eq_b b' e
181    | _ ⇒ false
182    ]
183  | EXT_INDIRECT b' ⇒
184    match b with
185    [ EXT_INDIRECT e ⇒ eq_b b' e
186    | _ ⇒ false
187    ]
188  | REGISTER bv ⇒
189    match b with
190    [ REGISTER bv' ⇒ eq_bv ? bv bv'
191    | _ ⇒ false
192    ]
193  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
194  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
195  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
196  | DATA b' ⇒
197    match b with
198    [ DATA e ⇒ eq_bv ? b' e
199    | _ ⇒ false
200    ]
201  | DATA16 w ⇒
202    match b with
203    [ DATA16 e ⇒ eq_bv ? w e
204    | _ ⇒ false
205    ]
206  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
207  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
208  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
209  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
210  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
211  | BIT_ADDR b' ⇒
212    match b with
213    [ BIT_ADDR e ⇒ eq_bv ? b' e
214    | _ ⇒ false
215    ]
216  | N_BIT_ADDR b' ⇒
217    match b with
218    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
219    | _ ⇒ false
220    ]
221  | RELATIVE n ⇒
222    match b with
223    [ RELATIVE e ⇒ eq_bv ? n e
224    | _ ⇒ false
225    ]
226  | ADDR11 w ⇒
227    match b with
228    [ ADDR11 e ⇒ eq_bv ? w e
229    | _ ⇒ false
230    ]
231  | ADDR16 w ⇒
232    match b with
233    [ ADDR16 e ⇒ eq_bv ? w e
234    | _ ⇒ false
235    ]
236  ].
237
238lemma eq_bv_refl:
239  ∀n, b.
240    eq_bv n b b = true.
241  #n #b cases b //
242qed.
243
244lemma eq_b_refl:
245  ∀b.
246    eq_b b b = true.
247  #b cases b //
248qed.
249
250lemma eq_addressing_mode_refl:
251  ∀a. eq_addressing_mode a a = true.
252  #a
253  cases a try #arg1 try #arg2
254  try @eq_bv_refl try @eq_b_refl
255  try normalize %
256qed.
257 
258definition eq_sum:
259    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
260  λlt, rt, leq, req, left, right.
261    match left with
262    [ inl l ⇒
263      match right with
264      [ inl l' ⇒ leq l l'
265      | _ ⇒ false
266      ]
267    | inr r ⇒
268      match right with
269      [ inr r' ⇒ req r r'
270      | _ ⇒ false
271      ]
272    ].
273
274definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
275  λlt, rt, leq, req, left, right.
276    let 〈l, r〉 ≝ left in
277    let 〈l', r'〉 ≝ right in
278      leq l l' ∧ req r r'.
279
280definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
281  λi, j.
282  match i with
283  [ ADD arg1 arg2 ⇒
284    match j with
285    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
286    | _ ⇒ false
287    ]
288  | ADDC arg1 arg2 ⇒
289    match j with
290    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
291    | _ ⇒ false
292    ]
293  | SUBB arg1 arg2 ⇒
294    match j with
295    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
296    | _ ⇒ false
297    ]
298  | INC arg ⇒
299    match j with
300    [ INC arg' ⇒ eq_addressing_mode arg arg'
301    | _ ⇒ false
302    ]
303  | DEC arg ⇒
304    match j with
305    [ DEC arg' ⇒ eq_addressing_mode arg arg'
306    | _ ⇒ false
307    ]
308  | MUL arg1 arg2 ⇒
309    match j with
310    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
311    | _ ⇒ false
312    ]
313  | DIV arg1 arg2 ⇒
314    match j with
315    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
316    | _ ⇒ false
317    ]
318  | DA arg ⇒
319    match j with
320    [ DA arg' ⇒ eq_addressing_mode arg arg'
321    | _ ⇒ false
322    ]
323  | JC arg ⇒
324    match j with
325    [ JC arg' ⇒ eq_addressing_mode arg arg'
326    | _ ⇒ false
327    ]
328  | JNC arg ⇒
329    match j with
330    [ JNC arg' ⇒ eq_addressing_mode arg arg'
331    | _ ⇒ false
332    ]
333  | JB arg1 arg2 ⇒
334    match j with
335    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
336    | _ ⇒ false
337    ]
338  | JNB arg1 arg2 ⇒
339    match j with
340    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
341    | _ ⇒ false
342    ]
343  | JBC arg1 arg2 ⇒
344    match j with
345    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
346    | _ ⇒ false
347    ]
348  | JZ arg ⇒
349    match j with
350    [ JZ arg' ⇒ eq_addressing_mode arg arg'
351    | _ ⇒ false
352    ]
353  | JNZ arg ⇒
354    match j with
355    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
356    | _ ⇒ false
357    ]
358  | CJNE arg1 arg2 ⇒
359    match j with
360    [ CJNE arg1' arg2' ⇒
361      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
362      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
363      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
364        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
365    | _ ⇒ false
366    ]
367  | DJNZ arg1 arg2 ⇒
368    match j with
369    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
370    | _ ⇒ false
371    ]
372  | CLR arg ⇒
373    match j with
374    [ CLR arg' ⇒ eq_addressing_mode arg arg'
375    | _ ⇒ false
376    ]
377  | CPL arg ⇒
378    match j with
379    [ CPL arg' ⇒ eq_addressing_mode arg arg'
380    | _ ⇒ false
381    ]
382  | RL arg ⇒
383    match j with
384    [ RL arg' ⇒ eq_addressing_mode arg arg'
385    | _ ⇒ false
386    ]
387  | RLC arg ⇒
388    match j with
389    [ RLC arg' ⇒ eq_addressing_mode arg arg'
390    | _ ⇒ false
391    ]
392  | RR arg ⇒
393    match j with
394    [ RR arg' ⇒ eq_addressing_mode arg arg'
395    | _ ⇒ false
396    ]
397  | RRC arg ⇒
398    match j with
399    [ RRC arg' ⇒ eq_addressing_mode arg arg'
400    | _ ⇒ false
401    ]
402  | SWAP arg ⇒
403    match j with
404    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
405    | _ ⇒ false
406    ]
407  | SETB arg ⇒
408    match j with
409    [ SETB arg' ⇒ eq_addressing_mode arg arg'
410    | _ ⇒ false
411    ]
412  | PUSH arg ⇒
413    match j with
414    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
415    | _ ⇒ false
416    ]
417  | POP arg ⇒
418    match j with
419    [ POP arg' ⇒ eq_addressing_mode arg arg'
420    | _ ⇒ false
421    ]
422  | XCH arg1 arg2 ⇒
423    match j with
424    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
425    | _ ⇒ false
426    ]
427  | XCHD arg1 arg2 ⇒
428    match j with
429    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
430    | _ ⇒ false
431    ]
432  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
433  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
434  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
435  | MOVX arg ⇒
436    match j with
437    [ MOVX arg' ⇒
438      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
439      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
440      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
441        sum_eq arg arg'
442    | _ ⇒ false
443    ]
444  | XRL arg ⇒
445    match j with
446    [ XRL arg' ⇒
447      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
448      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
449      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
450        sum_eq arg arg'
451    | _ ⇒ false
452    ]
453  | ORL arg ⇒
454    match j with
455    [ ORL arg' ⇒
456      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
457      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
458      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
459      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
460      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
461        sum_eq arg arg'
462    | _ ⇒ false
463    ]
464  | ANL arg ⇒
465    match j with
466    [ ANL arg' ⇒
467      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
468      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
469      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
470      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
471      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
472        sum_eq arg arg'
473    | _ ⇒ false
474    ]
475  | MOV arg ⇒
476    match j with
477    [ MOV arg' ⇒
478      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
479      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
480      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
481      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
482      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
483      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
484      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
485      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
486      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
487      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
488      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
489        sum_eq_5 arg arg'
490    | _ ⇒ false
491    ]
492  ].
493
494lemma eq_sum_refl:
495  ∀A, B: Type[0].
496  ∀leq, req.
497  ∀s.
498  ∀leq_refl: (∀t. leq t t = true).
499  ∀req_refl: (∀u. req u u = true).
500    eq_sum A B leq req s s = true.
501  #A #B #leq #req #s #leq_refl #req_refl
502  cases s assumption
503qed.
504
505lemma eq_prod_refl:
506  ∀A, B: Type[0].
507  ∀leq, req.
508  ∀s.
509  ∀leq_refl: (∀t. leq t t = true).
510  ∀req_refl: (∀u. req u u = true).
511    eq_prod A B leq req s s = true.
512  #A #B #leq #req #s #leq_refl #req_refl
513  cases s
514  whd in ⊢ (? → ? → ??%?);
515  #l #r
516  >leq_refl @req_refl
517qed.
518
519lemma eq_preinstruction_refl:
520  ∀i.
521    eq_preinstruction i i = true.
522  #i cases i try #arg1 try #arg2
523  try @eq_addressing_mode_refl
524  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
525    whd in ⊢ (??%?); try %
526    >eq_addressing_mode_refl
527    >eq_addressing_mode_refl %
528  |13,15:
529    whd in ⊢ (??%?);
530    cases arg1
531    [*:
532      #arg1_left normalize nodelta
533      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
534    ]
535  |11,12:
536    whd in ⊢ (??%?);
537    cases arg1
538    [1:
539      #arg1_left normalize nodelta
540      >(eq_sum_refl …)
541      [1: % | 2,3: #arg @eq_prod_refl ]
542      @eq_addressing_mode_refl
543    |2:
544      #arg1_left normalize nodelta
545      @eq_prod_refl [*: @eq_addressing_mode_refl ]
546    |3:
547      #arg1_left normalize nodelta
548      >(eq_sum_refl …)
549      [1:
550        %
551      |2,3:
552        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
553      ]
554    |4:
555      #arg1_left normalize nodelta
556      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
557    ]
558  |14:
559    whd in ⊢ (??%?);
560    cases arg1
561    [1:
562      #arg1_left normalize nodelta
563      @eq_sum_refl
564      [1:
565        #arg @eq_sum_refl
566        [1:
567          #arg @eq_sum_refl
568          [1:
569            #arg @eq_sum_refl
570            [1:
571              #arg @eq_prod_refl
572              [*:
573                @eq_addressing_mode_refl
574              ]
575            |2:
576              #arg @eq_prod_refl
577              [*:
578                #arg @eq_addressing_mode_refl
579              ]
580            ]
581          |2:
582            #arg @eq_prod_refl
583            [*:
584              #arg @eq_addressing_mode_refl
585            ]
586          ]
587        |2:
588          #arg @eq_prod_refl
589          [*:
590            #arg @eq_addressing_mode_refl
591          ]
592        ]
593      |2:
594        #arg @eq_prod_refl
595        [*:
596          #arg @eq_addressing_mode_refl
597        ]
598      ]
599    |2:
600      #arg1_right normalize nodelta
601      @eq_prod_refl
602      [*:
603        #arg @eq_addressing_mode_refl
604      ]
605    ]
606  |*:
607    whd in ⊢ (??%?);
608    cases arg1
609    [*:
610      #arg1 >eq_sum_refl
611      [1,4:
612        @eq_addressing_mode_refl
613      |2,3,5,6:
614        #arg @eq_prod_refl
615        [*:
616          #arg @eq_addressing_mode_refl
617        ]
618      ]
619    ]
620  ]
621qed.
622
623definition eq_instruction: instruction → instruction → bool ≝
624  λi, j.
625  match i with
626  [ ACALL arg ⇒
627    match j with
628    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
629    | _ ⇒ false
630    ]
631  | LCALL arg ⇒
632    match j with
633    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
634    | _ ⇒ false
635    ]
636  | AJMP arg ⇒
637    match j with
638    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
639    | _ ⇒ false
640    ]
641  | LJMP arg ⇒
642    match j with
643    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
644    | _ ⇒ false
645    ]
646  | SJMP arg ⇒
647    match j with
648    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
649    | _ ⇒ false
650    ]
651  | JMP arg ⇒
652    match j with
653    [ JMP arg' ⇒ eq_addressing_mode arg arg'
654    | _ ⇒ false
655    ]
656  | MOVC arg1 arg2 ⇒
657    match j with
658    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
659    | _ ⇒ false
660    ]
661  | RealInstruction instr ⇒
662    match j with
663    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
664    | _ ⇒ false
665    ]
666  ].
667 
668lemma eq_instruction_refl:
669  ∀i. eq_instruction i i = true.
670  #i cases i [*: #arg1 ]
671  try @eq_addressing_mode_refl
672  try @eq_preinstruction_refl
673  #arg2 whd in ⊢ (??%?);
674  >eq_addressing_mode_refl >eq_addressing_mode_refl %
675qed.
676
677let rec vect_member
678  (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A)
679    on v: bool ≝
680  match v with
681  [ VEmpty          ⇒ false
682  | VCons len hd tl ⇒
683      eq hd a ∨ (vect_member A ? eq tl a)
684  ].
685
686let rec list_addressing_mode_tags_elim_prop
687  (n: nat)
688  (l: Vector addressing_mode_tag (S n))
689  on l:
690  ∀P: l → Prop.
691  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
692  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
693  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
694  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
695  ∀x: l. P x ≝
696  match l return
697    λy.
698      match y with
699      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
700      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
701               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
702               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
703               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
704               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
705               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
706               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
707               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
708               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
709               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
710               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
711               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
712               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
713               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
714               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
715               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
716               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
717               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
718               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
719               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
720               ∀x:l. P x
721      ] with
722  [ VEmpty          ⇒ λAbsurd. ⊥
723  | VCons len hd tl ⇒ λProof. ?
724  ] (refl ? (S n)). cases daemon. qed. (*
725  [ destruct(Absurd)
726  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
727    # A8 # A9 # A10 # A11 # A12 # A13 # A14
728    # A15 # A16 # A17 # A18 # A19 # X
729    cases X
730    # SUB cases daemon ] qed.
731    cases SUB
732    [ # BYTE
733    normalize
734  ].
735 
736 
737(*    let prepare_hd ≝
738      match hd with
739      [ direct ⇒ λdirect_prf. ?
740      | indirect ⇒ λindirect_prf. ?
741      | ext_indirect ⇒ λext_indirect_prf. ?
742      | registr ⇒ λregistr_prf. ?
743      | acc_a ⇒ λacc_a_prf. ?
744      | acc_b ⇒ λacc_b_prf. ?
745      | dptr ⇒ λdptr_prf. ?
746      | data ⇒ λdata_prf. ?
747      | data16 ⇒ λdata16_prf. ?
748      | acc_dptr ⇒ λacc_dptr_prf. ?
749      | acc_pc ⇒ λacc_pc_prf. ?
750      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
751      | indirect_dptr ⇒ λindirect_prf. ?
752      | carry ⇒ λcarry_prf. ?
753      | bit_addr ⇒ λbit_addr_prf. ?
754      | n_bit_addr ⇒ λn_bit_addr_prf. ?
755      | relative ⇒ λrelative_prf. ?
756      | addr11 ⇒ λaddr11_prf. ?
757      | addr16 ⇒ λaddr16_prf. ?
758      ]
759    in ? *)
760  ].
761  [ 1: destruct(absd)
762  | 2: # A1 # A2 # A3 # A4 # A5 # A6
763       # A7 # A8 # A9 # A10 # A11 # A12
764       # A13 # A14 # A15 # A16 # A17 # A18
765       # A19 *
766  ].
767
768
769  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
770   (l → bool) → bool ] with
771  [ VEmpty      ⇒  true 
772  | VCons len hd tl ⇒ λP.
773    let process_hd ≝
774      match hd return λhd. ∀P: hd:::tl → bool. bool with
775      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
776      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
777      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
778      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
779      | acc_a ⇒ λP.P ACC_A
780      | acc_b ⇒ λP.P ACC_B
781      | dptr ⇒ λP.P DPTR
782      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
783      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
784      | acc_dptr ⇒ λP.P ACC_DPTR
785      | acc_pc ⇒ λP.P ACC_PC
786      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
787      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
788      | carry ⇒ λP.P CARRY
789      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
790      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
791      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
792      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
793      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
794      ]
795    in
796      andb (process_hd P)
797       (match len return λx. x = len → bool with
798         [ O ⇒ λprf. true
799         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
800  ].
801  try %
802  [ 2: cases (sym_eq ??? prf); @tl
803  | generalize in match H; generalize in match tl; cases prf;
804    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
805    #tl
806    normalize in ⊢ (∀_: %. ?)
807    # H
808    whd
809    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
810    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
811qed.
812*)
813
814definition load_code_memory_aux ≝
815 fold_left_i_aux … (
816   λi, mem, v.
817     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
818
819lemma vsplit_zero:
820  ∀A,m.
821  ∀v: Vector A m.
822    〈[[]], v〉 = vsplit A 0 m v.
823  #A #m #v
824  cases v try %
825  #n #hd #tl %
826qed.
827
828lemma Vector_O:
829  ∀A: Type[0].
830  ∀v: Vector A 0.
831    v ≃ VEmpty A.
832 #A #v
833 generalize in match (refl … 0);
834 cases v in ⊢ (??%? → ?%%??); //
835 #n #hd #tl #absurd
836 destruct(absurd)
837qed.
838
839lemma Vector_Sn:
840  ∀A: Type[0].
841  ∀n: nat.
842  ∀v: Vector A (S n).
843    ∃hd: A. ∃tl: Vector A n.
844      v ≃ VCons A n hd tl.
845  #A #n #v
846  generalize in match (refl … (S n));
847  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
848  [1:
849    #absurd destruct(absurd)
850  |2:
851    #m #hd #tl #eq
852    <(injective_S … eq)
853    %{hd} %{tl} %
854  ]
855qed.
856
857lemma vector_append_zero:
858  ∀A,m.
859  ∀v: Vector A m.
860  ∀q: Vector A 0.
861    v = q@@v.
862  #A #m #v #q
863  >(Vector_O A q) %
864qed.
865
866lemma prod_eq_left:
867  ∀A: Type[0].
868  ∀p, q, r: A.
869    p = q → 〈p, r〉 = 〈q, r〉.
870  #A #p #q #r #hyp
871  destruct %
872qed.
873
874lemma prod_eq_right:
875  ∀A: Type[0].
876  ∀p, q, r: A.
877    p = q → 〈r, p〉 = 〈r, q〉.
878  #A #p #q #r #hyp
879  destruct %
880qed.
881
882corollary prod_vector_zero_eq_left:
883  ∀A, n.
884  ∀q: Vector A O.
885  ∀r: Vector A n.
886    〈q, r〉 = 〈[[ ]], r〉.
887  #A #n #q #r
888  generalize in match (Vector_O A q …);
889  #hyp destruct %
890qed.
891
892lemma tail_head:
893  ∀a: Type[0].
894  ∀m, n: nat.
895  ∀hd: a.
896  ∀l: Vector a m.
897  ∀r: Vector a n.
898    tail a ? (hd:::(l@@r)) = l@@r.
899  #a #m #n #hd #l #r
900  cases l try %
901  #m' #hd' #tl' %
902qed.
903
904lemma head_head':
905  ∀a: Type[0].
906  ∀m: nat.
907  ∀hd: a.
908  ∀l: Vector a m.
909    hd = head' … (hd:::l).
910  #a #m #hd #l cases l try %
911  #m' #hd' #tl %
912qed.
913
914lemma vsplit_succ:
915  ∀A: Type[0].
916  ∀m, n: nat.
917  ∀l: Vector A m.
918  ∀r: Vector A n.
919  ∀v: Vector A (m + n).
920  ∀hd: A.
921    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
922  #A #m
923  elim m
924  [1:
925    #n #l #r #v #hd #eq #hyp
926    destruct >(Vector_O … l) %
927  |2:
928    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
929    destruct
930    cases (Vector_Sn … l) #hd' #tl'
931    whd in ⊢ (???%);
932    >tail_head
933    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
934    try (<hyp <head_head' %)
935    elim l normalize //
936  ]
937qed.
938
939lemma vsplit_prod:
940  ∀A: Type[0].
941  ∀m, n: nat.
942  ∀p: Vector A (m + n).
943  ∀v: Vector A m.
944  ∀q: Vector A n.
945    p = v@@q → 〈v, q〉 = vsplit A m n p.
946  #A #m elim m
947  [1:
948    #n #p #v #q #hyp
949    >hyp <(vector_append_zero A n q v)
950    >(prod_vector_zero_eq_left A …)
951    @vsplit_zero
952  |2:
953    #r #ih #n #p #v #q #hyp
954    >hyp
955    cases (Vector_Sn A r v) #hd #exists
956    cases exists #tl #jmeq
957    >jmeq @vsplit_succ try %
958    @ih %
959  ]
960qed.
961
962(*
963lemma vsplit_prod_exists:
964  ∀A, m, n.
965  ∀p: Vector A (m + n).
966  ∃v: Vector A m.
967  ∃q: Vector A n.
968    〈v, q〉 = vsplit A m n p.
969  #A #m #n #p
970  elim m
971  @ex_intro
972  [1:
973  |2: @ex_intro
974      [1:
975      |2:
976      ]
977  ]
978*)
979
980definition vsplit_elim:
981  ∀A: Type[0].
982  ∀l, m: nat.
983  ∀v: Vector A (l + m).
984  ∀P: (Vector A l) × (Vector A m) → Prop.
985    (∀vl: Vector A l.
986     ∀vm: Vector A m.
987      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
988  λa: Type[0].
989  λl, m: nat.
990  λv: Vector a (l + m).
991  λP. ?.
992  cases daemon
993qed.
994
995(*
996axiom not_eqvb_S:
997 ∀pc.
998 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
999
1000axiom not_eqvb_SS:
1001 ∀pc.
1002 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
1003 
1004axiom bitvector_elim_complete:
1005 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
1006
1007lemma bitvector_elim_complete':
1008 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
1009 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
1010 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
1011qed.
1012*)
1013
1014(*
1015lemma andb_elim':
1016 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
1017 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
1018qed.
1019*)
1020
1021let rec encoding_check
1022  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
1023    (encoding: list Byte)
1024      on encoding: Prop ≝
1025  match encoding with
1026  [ nil ⇒ final_pc = pc
1027  | cons hd tl ⇒
1028    let 〈new_pc, byte〉 ≝ next code_memory pc in
1029      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
1030  ].
1031
1032axiom add_commutative:
1033  ∀n: nat.
1034  ∀l, r: BitVector n.
1035    add n l r = add n r l.
1036
1037axiom add_bitvector_of_nat_Sm:
1038  ∀n, m: nat.
1039    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
1040      bitvector_of_nat n (S m).
1041
1042lemma encoding_check_append:
1043  ∀code_memory: BitVectorTrie Byte 16.
1044  ∀final_pc: Word.
1045  ∀l1: list Byte.
1046  ∀pc: Word.
1047  ∀l2: list Byte.
1048    encoding_check code_memory pc final_pc (l1@l2) →
1049      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
1050        encoding_check code_memory pc pc_plus_len l1 ∧
1051          encoding_check code_memory pc_plus_len final_pc l2.
1052  #code_memory #final_pc #l1 elim l1
1053  [1:
1054    #pc #l2
1055    whd in ⊢ (????% → ?); #H
1056    <add_zero
1057    whd whd in ⊢ (?%?); /2/
1058  |2:
1059    #hd #tl #IH #pc #l2 * #H1 #H2
1060(*    >add_SO in H2; #H2 *)
1061    cases (IH … H2) #E1 #E2 %
1062    [1:
1063      % try @H1
1064      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
1065      <add_associative #assm assumption
1066    |2:
1067      <add_associative in E2;
1068      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
1069      assumption
1070    ]
1071  ]
1072qed.
1073
1074lemma destruct_bug_fix_1:
1075  ∀n: nat.
1076    S n = 0 → False.
1077  #n #absurd destruct(absurd)
1078qed.
1079
1080lemma destruct_bug_fix_2:
1081  ∀m, n: nat.
1082    S m = S n → m = n.
1083  #m #n #refl destruct %
1084qed.
1085
1086definition bitvector_3_cases:
1087  ∀b: BitVector 3.
1088    ∃l, c, r: bool.
1089      b ≃ [[l; c; r]].
1090  #b
1091  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
1092  [1:
1093    #absurd @⊥ -b @(destruct_bug_fix_1 2)
1094    >absurd %
1095  |2:
1096    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
1097    cut (n = 2)
1098    [1:
1099      @destruct_bug_fix_2
1100      >size_refl %
1101    |2:
1102      #n_refl >n_refl in tl; #V
1103      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
1104      [1:
1105        #absurd @⊥ -V @(destruct_bug_fix_1 1)
1106        >absurd %
1107      |2:
1108        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
1109        cut (n' = 1)
1110        [1:
1111          @destruct_bug_fix_2 >size_refl' %
1112        |2:
1113          #n_refl' >n_refl' in tl'; #V'
1114          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
1115          [1:
1116            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
1117            >absurd %
1118          |2:
1119            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
1120            cut (n'' = 0)
1121            [1:
1122              @destruct_bug_fix_2 >size_refl'' %
1123            |2:
1124              #n_refl'' >n_refl'' in tl''; #tl'''
1125              >(Vector_O … tl''') %
1126            ]
1127          ]
1128        ]
1129      ]
1130    ]
1131  ]
1132qed.
1133
1134lemma bitvector_3_elim_prop:
1135  ∀P: BitVector 3 → Prop.
1136    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
1137    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
1138    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
1139  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
1140  cases (bitvector_3_cases … H9) #l #assm cases assm
1141  -assm #c #assm cases assm
1142  -assm #r #assm cases assm destruct
1143  cases l cases c cases r assumption
1144qed.
1145
1146definition ticks_of_instruction ≝
1147  λi.
1148    let trivial_code_memory ≝ assembly1 i in
1149    let trivial_status ≝ load_code_memory trivial_code_memory in
1150      \snd (fetch trivial_status (zero ?)).
1151
1152lemma fetch_assembly:
1153  ∀pc: Word.
1154  ∀i: instruction.
1155  ∀code_memory: BitVectorTrie Byte 16.
1156  ∀assembled: list Byte.
1157    assembled = assembly1 i →
1158      let len ≝ length … assembled in
1159      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1160        encoding_check code_memory pc pc_plus_len assembled →
1161          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
1162           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
1163  #pc #i #code_memory #assembled cases i [8: *]
1164 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
1165 [47,48,49:
1166 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
1167  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
1168   59,60,63,64,65,66,67: #ARG]]
1169 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
1170  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
1171  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
1172   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
1173   68,69,70,71: #ARG2]]
1174 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
1175 normalize in ⊢ (???% → ?);
1176 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
1177  normalize in ⊢ (???% → ?);]
1178 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
1179 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
1180 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
1181(*
1182 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
1183 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
1184 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
1185  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
1186  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
1187 whd >eq_instruction_refl >H4 @eq_bv_refl
1188*) (* XXX: not working! *)
1189qed.
1190
1191let rec fetch_many
1192  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
1193    (expected: list instruction)
1194      on expected: Prop ≝
1195  match expected with
1196  [ nil ⇒ eq_bv … pc final_pc = true
1197  | cons i tl ⇒
1198    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
1199      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
1200        fetch_many code_memory final_pc pc' tl)
1201  ].
1202
1203lemma option_destruct_Some:
1204  ∀A: Type[0].
1205  ∀a, b: A.
1206    Some A a = Some A b → a = b.
1207  #A #a #b #EQ
1208  destruct %
1209qed.
1210
1211lemma eq_instruction_to_eq:
1212  ∀i1, i2: instruction.
1213    eq_instruction i1 i2 = true → i1 ≃ i2.
1214  #i1 #i2
1215  cases i1 cases i2 cases daemon (*
1216  [1,10,19,28,37,46:
1217    #arg1 #arg2
1218    whd in match (eq_instruction ??);
1219    cases arg1 #subaddressing_mode
1220    cases subaddressing_mode
1221    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1222    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1223    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
1224    #word11 #irrelevant
1225    cases arg2 #subaddressing_mode
1226    cases subaddressing_mode
1227    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1228    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1229    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
1230    #word11' #irrelevant normalize nodelta
1231    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
1232qed.
1233         
1234lemma fetch_assembly_pseudo':
1235  ∀lookup_labels.
1236  ∀sigma: Word → Word.
1237  ∀policy: Word → bool.
1238  ∀ppc.
1239  ∀lookup_datalabels.
1240  ∀pi.
1241  ∀code_memory.
1242  ∀len.
1243  ∀assembled.
1244  ∀instructions.
1245    let pc ≝ sigma ppc in
1246      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
1247        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
1248          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1249            encoding_check code_memory pc pc_plus_len assembled →
1250              fetch_many code_memory pc_plus_len pc instructions.
1251  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
1252  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
1253  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
1254  >len_refl >assembled_refl -len_refl
1255  generalize in match (add 16 (sigma ppc)
1256    (bitvector_of_nat 16
1257     (|flatten (Vector bool 8)
1258       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
1259  #final_pc
1260  generalize in match (sigma ppc); elim instructions
1261  [1:
1262    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
1263  |2:
1264    #i #tl #IH #pc #H whd
1265    cases (encoding_check_append ????? H) -H #H1 #H2
1266    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
1267    cases (fetch ??) * #instr #pc' #ticks
1268    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
1269    lapply (conjunction_true ?? H3) * #H4 #H5
1270    lapply (conjunction_true … H4) * #B1 #B2
1271    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
1272    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
1273  ]
1274qed.
1275
1276lemma fetch_assembly_pseudo:
1277  ∀program: pseudo_assembly_program.
1278  ∀sigma: Word → Word.
1279  ∀policy: Word → bool.
1280  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
1281  ∀ppc.∀ppc_ok.
1282  ∀code_memory.
1283  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
1284  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
1285  let pc ≝ sigma ppc in
1286  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1287  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1288  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1289    encoding_check code_memory pc pc_plus_len assembled →
1290      fetch_many code_memory pc_plus_len pc instructions.
1291  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
1292  letin lookup_datalabels ≝ (λx.?)
1293  letin pi ≝ (fst ???)
1294  letin pc ≝ (sigma ?)
1295  letin instructions ≝ (expand_pseudo_instruction ??????)
1296  @pair_elim #len #assembled #assembled_refl normalize nodelta
1297  #H
1298  generalize in match
1299   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
1300  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
1301qed.
1302
1303definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
1304  λpseudo_instruction.
1305    match pseudo_instruction with
1306    [ Comment c ⇒ False
1307    | Cost c ⇒ False
1308    | _ ⇒ True
1309    ].
1310
1311(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
1312   function that load the code in memory is correct. The latter is based
1313   on missing properties from the standard library on the BitVectorTrie
1314   data structrure.
1315   
1316   Wrong at the moment, requires Jaap's precondition to ensure that the program
1317   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1318*)
1319
1320lemma load_code_memory_ok:
1321 ∀program.
1322 let program_size ≝ |program| in
1323  program_size ≤ 2^16 →
1324   ∀pc. ∀pc_ok: pc < program_size.
1325    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1326 #program elim program
1327 [ #_ #pc #abs normalize in abs; @⊥ /2/
1328 | #hd #tl #IH #size_ok *
1329   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
1330     whd in match next; normalize nodelta
1331   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
1332     whd in match next; normalize nodelta
1333   ]
1334 cases daemon (*CSC: complete! *)
1335qed.
1336(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
1337Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
1338e' come fetchare l'i-esimo bit dalla memoria.
1339Concludere assembly_ok come semplice corollario.
1340*)
1341lemma assembly_ok:
1342  ∀program.
1343  ∀length_proof: |\snd program| ≤ 2^16.
1344  ∀sigma: Word → Word.
1345  ∀policy: Word → bool.
1346  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
1347  ∀assembled.
1348  ∀costs': BitVectorTrie costlabel 16.
1349  let 〈preamble, instr_list〉 ≝ program in
1350  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
1351  let datalabels ≝ construct_datalabels preamble in
1352  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1353    〈assembled,costs'〉 = assembly program sigma policy →
1354      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
1355        let code_memory ≝ load_code_memory assembled in
1356        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
1357          ∀ppc.∀ppc_ok.
1358            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
1359            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1360            let pc ≝ sigma ppc in
1361            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1362              encoding_check code_memory pc pc_plus_len assembled ∧
1363                  sigma newppc = add … pc (bitvector_of_nat … len).
1364  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
1365  cases (assembly program sigma policy) * #assembled' #costs''
1366  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
1367  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
1368  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
1369  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
1370  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
1371  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
1372  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
1373  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
1374  >eq_fetch_pseudo_instruction
1375  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
1376  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
1377       (λx.address_of_word_labels_code_mem instr_list x)))
1378  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
1379      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
1380  >eq_assembly_1_pseudoinstruction
1381  whd in ⊢ (% → ?); #assembly_ok
1382  %
1383  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
1384      >snd_fetch_pseudo_instruction
1385      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
1386      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
1387      >eq_fetch_pseudo_instruction whd in match instruction_size;
1388      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
1389      cases daemon
1390  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
1391    #load_code_memory_ok
1392    cut (len=|assembled|)
1393    [1: (*CSC: provable before cleaning *)
1394        cases daemon
1395    ]
1396    #EQlen
1397    (* Nice statement here *)
1398    cut (∀j. ∀H: j < |assembled|.
1399          nth_safe Byte j assembled H =
1400          \snd (next (load_code_memory assembled')
1401          (bitvector_of_nat 16
1402           (nat_of_bitvector …
1403            (add … (sigma ppc) (bitvector_of_nat … j))))))
1404    [1:
1405      cases daemon
1406    |2:
1407      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
1408      elim assembled
1409      [1:
1410        #pc #_ whd <add_zero %
1411      | #hd #tl #IH #pc #H %
1412         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
1413           >H -H whd in ⊢ (??%?); <add_zero //
1414         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
1415           [2: <add_bitvector_of_nat_Sm @add_associative ]
1416           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
1417           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
1418           >add_associative % ]]
1419  ]]
1420qed.
1421
1422(* XXX: should we add that costs = costs'? *)
1423lemma fetch_assembly_pseudo2:
1424  ∀program.
1425  ∀length_proof: |\snd program| ≤ 2^16.
1426  ∀sigma.
1427  ∀policy.
1428  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1429  ∀ppc.∀ppc_ok.
1430  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1431  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
1432  let code_memory ≝ load_code_memory assembled in
1433  let data_labels ≝ construct_datalabels (\fst program) in
1434  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
1435  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
1436  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1437  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1438    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
1439  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
1440  @pair_elim #labels #costs #create_label_map_refl
1441  @pair_elim #assembled #costs' #assembled_refl
1442  letin code_memory ≝ (load_code_memory ?)
1443  letin data_labels ≝ (construct_datalabels ?)
1444  letin lookup_labels ≝ (λx. ?)
1445  letin lookup_datalabels ≝ (λx. ?)
1446  @pair_elim #pi #newppc #fetch_pseudo_refl
1447  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
1448  normalize nodelta try assumption
1449  @pair_elim #labels' #costs' #create_label_map_refl' #H
1450  lapply (H (sym_eq … assembled_refl)) -H
1451  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1452  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
1453  #len #assembledi #EQ4 #H
1454  lapply (H ppc) >fetch_pseudo_refl #H
1455  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
1456  >EQ4 #H1 cases (H ppc_ok)
1457  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
1458  >fetch_pseudo_refl in H1; #assm @assm assumption
1459qed.
1460
1461(* OLD?
1462definition assembly_specification:
1463  ∀assembly_program: pseudo_assembly_program.
1464  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1465  λpseudo_assembly_program.
1466  λcode_mem.
1467    ∀pc: Word.
1468      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1469      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1470      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1471      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1472      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1473       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1474      match pre_assembled with
1475       [ None ⇒ True
1476       | Some pc_code ⇒
1477          let 〈new_pc,code〉 ≝ pc_code in
1478           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1479
1480axiom assembly_meets_specification:
1481  ∀pseudo_assembly_program.
1482    match assembly pseudo_assembly_program with
1483    [ None ⇒ True
1484    | Some code_mem_cost ⇒
1485      let 〈code_mem, cost〉 ≝ code_mem_cost in
1486        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1487    ].
1488(*
1489  # PROGRAM
1490  [ cases PROGRAM
1491    # PREAMBLE
1492    # INSTR_LIST
1493    elim INSTR_LIST
1494    [ whd
1495      whd in ⊢ (∀_. %)
1496      # PC
1497      whd
1498    | # INSTR
1499      # INSTR_LIST_TL
1500      # H
1501      whd
1502      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1503    ]
1504  | cases not_implemented
1505  ] *)
1506*)
1507
1508(* XXX: changed this type.  Bool specifies whether byte is first or second
1509        component of an address, and the Word is the pseudoaddress that it
1510        corresponds to.  Second component is the same principle for the accumulator
1511        A.
1512*)
1513definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
1514
1515include alias "ASM/BitVectorTrie.ma".
1516 
1517include "common/AssocList.ma".
1518
1519axiom low_internal_ram_of_pseudo_low_internal_ram:
1520 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1521
1522axiom high_internal_ram_of_pseudo_high_internal_ram:
1523 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1524
1525axiom low_internal_ram_of_pseudo_internal_ram_hit:
1526 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
1527  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
1528   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1529   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1530   let bl ≝ lookup ? 7 addr ram (zero 8) in
1531   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
1532   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
1533     if high then
1534       (pbl = higher) ∧ (bl = phigher)
1535     else
1536       (pbl = lower) ∧ (bl = plower).
1537
1538(* changed from add to sub *)
1539axiom low_internal_ram_of_pseudo_internal_ram_miss:
1540 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
1541  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1542    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
1543      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1544
1545definition addressing_mode_ok ≝
1546 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
1547  λaddr:addressing_mode.
1548   match addr with
1549    [ DIRECT d ⇒
1550       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1551       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1552    | INDIRECT i ⇒
1553       let d ≝ get_register … s [[false;false;i]] in
1554       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1555       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1556    | EXT_INDIRECT _ ⇒ true
1557    | REGISTER _ ⇒ true
1558    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
1559    | ACC_B ⇒ true
1560    | DPTR ⇒ true
1561    | DATA _ ⇒ true
1562    | DATA16 _ ⇒ true
1563    | ACC_DPTR ⇒ true
1564    | ACC_PC ⇒ true
1565    | EXT_INDIRECT_DPTR ⇒ true
1566    | INDIRECT_DPTR ⇒ true
1567    | CARRY ⇒ true
1568    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1569    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1570    | RELATIVE _ ⇒ true
1571    | ADDR11 _ ⇒ true
1572    | ADDR16 _ ⇒ true ].
1573   
1574definition next_internal_pseudo_address_map0 ≝
1575  λT.
1576  λcm:T.
1577  λaddr_of: Identifier → PreStatus T cm → Word.
1578  λfetched.
1579  λM: internal_pseudo_address_map.
1580  λs: PreStatus T cm.
1581   match fetched with
1582    [ Comment _ ⇒ Some ? M
1583    | Cost _ ⇒ Some … M
1584    | Jmp _ ⇒ Some … M
1585    | Call a ⇒
1586      let a' ≝ addr_of a s in
1587      let 〈callM, accM〉 ≝ M in
1588         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
1589                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
1590    | Mov _ _ ⇒ Some … M
1591    | Instruction instr ⇒
1592       match instr with
1593        [ ADD addr1 addr2 ⇒
1594           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1595            Some ? M
1596           else
1597            None ?
1598        | ADDC addr1 addr2 ⇒
1599           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1600            Some ? M
1601           else
1602            None ?
1603        | SUBB addr1 addr2 ⇒
1604           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1605            Some ? M
1606           else
1607            None ?       
1608        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1609
1610definition next_internal_pseudo_address_map ≝
1611 λM:internal_pseudo_address_map.
1612 λcm.
1613 λaddr_of.
1614 λs:PseudoStatus cm.
1615 λppc_ok.
1616    next_internal_pseudo_address_map0 ? cm addr_of
1617     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1618
1619definition code_memory_of_pseudo_assembly_program:
1620    ∀pap:pseudo_assembly_program.
1621      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1622  λpap.
1623  λsigma.
1624  λpolicy.
1625    let p ≝ pi1 … (assembly pap sigma policy) in
1626      load_code_memory (\fst p).
1627
1628definition sfr_8051_of_pseudo_sfr_8051 ≝
1629  λM: internal_pseudo_address_map.
1630  λsfrs: Vector Byte 19.
1631  λsigma: Word → Word.
1632    match \snd M with
1633    [ None ⇒ sfrs
1634    | Some s ⇒
1635      let 〈high, address〉 ≝ s in
1636      let index ≝ sfr_8051_index SFR_ACC_A in
1637      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
1638        if high then
1639          set_index Byte 19 sfrs index upper ?
1640        else
1641          set_index Byte 19 sfrs index lower ?
1642    ].
1643  //
1644qed.
1645
1646definition status_of_pseudo_status:
1647    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1648      ∀sigma: Word → Word. ∀policy: Word → bool.
1649        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1650  λM.
1651  λpap.
1652  λps.
1653  λsigma.
1654  λpolicy.
1655  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1656  let pc ≝ sigma (program_counter … ps) in
1657  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1658  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1659     mk_PreStatus (BitVectorTrie Byte 16)
1660      cm
1661      lir
1662      hir
1663      (external_ram … ps)
1664      pc
1665      (special_function_registers_8051 … ps)
1666      (special_function_registers_8052 … ps)
1667      (p1_latch … ps)
1668      (p3_latch … ps)
1669      (clock … ps).
1670
1671(*
1672definition write_at_stack_pointer':
1673 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1674  λM: Type[0].
1675  λs: PreStatus M.
1676  λv: Byte.
1677    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1678    let bit_zero ≝ get_index_v… nu O ? in
1679    let bit_1 ≝ get_index_v… nu 1 ? in
1680    let bit_2 ≝ get_index_v… nu 2 ? in
1681    let bit_3 ≝ get_index_v… nu 3 ? in
1682      if bit_zero then
1683        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1684                              v (low_internal_ram ? s) in
1685          set_low_internal_ram ? s memory
1686      else
1687        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1688                              v (high_internal_ram ? s) in
1689          set_high_internal_ram ? s memory.
1690  [ cases l0 %
1691  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1692qed.
1693
1694definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1695 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1696
1697  λticks_of.
1698  λs.
1699  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1700  let ticks ≝ ticks_of (program_counter ? s) in
1701  let s ≝ set_clock ? s (clock ? s + ticks) in
1702  let s ≝ set_program_counter ? s pc in
1703    match instr with
1704    [ Instruction instr ⇒
1705       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1706    | Comment cmt ⇒ s
1707    | Cost cst ⇒ s
1708    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1709    | Call call ⇒
1710      let a ≝ address_of_word_labels s call in
1711      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1712      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1713      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1714      let s ≝ write_at_stack_pointer' ? s pc_bl in
1715      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1716      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1717      let s ≝ write_at_stack_pointer' ? s pc_bu in
1718        set_program_counter ? s a
1719    | Mov dptr ident ⇒
1720       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1721    ].
1722 [
1723 |2,3,4: %
1724 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1725 |
1726 | %
1727 ]
1728 cases not_implemented
1729qed.
1730*)
1731
1732(*
1733lemma execute_code_memory_unchanged:
1734 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1735 #ticks #ps whd in ⊢ (??? (??%))
1736 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1737  (program_counter pseudo_assembly_program ps)) #instr #pc
1738 whd in ⊢ (??? (??%)) cases instr
1739  [ #pre cases pre
1740     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1741       cases (vsplit ????) #z1 #z2 %
1742     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1743       cases (vsplit ????) #z1 #z2 %
1744     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1745       cases (vsplit ????) #z1 #z2 %
1746     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1747       [ #x1 whd in ⊢ (??? (??%))
1748     | *: cases not_implemented
1749     ]
1750  | #comment %
1751  | #cost %
1752  | #label %
1753  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1754    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1755    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1756    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1757    (* CSC: ??? *)
1758  | #dptr #label (* CSC: ??? *)
1759  ]
1760  cases not_implemented
1761qed.
1762*)
1763
1764(* DEAD CODE?
1765lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1766 ∀M:internal_pseudo_address_map.
1767 ∀ps,ps': PseudoStatus.
1768 ∀pol.
1769  ∀prf:code_memory … ps = code_memory … ps'.
1770   let pol' ≝ ? in
1771   match status_of_pseudo_status M ps pol with
1772    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1773    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1774    ].
1775 [2: <prf @pol]
1776 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1777 generalize in match (refl … (assembly (code_memory … ps) pol))
1778 cases (assembly ??) in ⊢ (???% → %)
1779  [ #K whd whd in ⊢ (??%?) <H >K %
1780  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1781qed.
1782*)
1783
1784definition ticks_of0:
1785    ∀p:pseudo_assembly_program.
1786      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1787  λprogram: pseudo_assembly_program.
1788  λsigma.
1789  λpolicy.
1790  λppc: Word.
1791  λfetched.
1792    match fetched with
1793    [ Instruction instr ⇒
1794      match instr with
1795      [ JC lbl ⇒ ? (*
1796        match pol lookup_labels ppc with
1797        [ short_jump ⇒ 〈2, 2〉
1798        | absolute_jump ⇒ ?
1799        | long_jump ⇒ 〈4, 4〉
1800        ] *)
1801      | JNC lbl ⇒ ? (*
1802        match pol lookup_labels ppc with
1803        [ short_jump ⇒ 〈2, 2〉
1804        | absolute_jump ⇒ ?
1805        | long_jump ⇒ 〈4, 4〉
1806        ] *)
1807      | JB bit lbl ⇒ ? (*
1808        match pol lookup_labels ppc with
1809        [ short_jump ⇒ 〈2, 2〉
1810        | absolute_jump ⇒ ?
1811        | long_jump ⇒ 〈4, 4〉
1812        ] *)
1813      | JNB bit lbl ⇒ ? (*
1814        match pol lookup_labels ppc with
1815        [ short_jump ⇒ 〈2, 2〉
1816        | absolute_jump ⇒ ?
1817        | long_jump ⇒ 〈4, 4〉
1818        ] *)
1819      | JBC bit lbl ⇒ ? (*
1820        match pol lookup_labels ppc with
1821        [ short_jump ⇒ 〈2, 2〉
1822        | absolute_jump ⇒ ?
1823        | long_jump ⇒ 〈4, 4〉
1824        ] *)
1825      | JZ lbl ⇒ ? (*
1826        match pol lookup_labels ppc with
1827        [ short_jump ⇒ 〈2, 2〉
1828        | absolute_jump ⇒ ?
1829        | long_jump ⇒ 〈4, 4〉
1830        ] *)
1831      | JNZ lbl ⇒ ? (*
1832        match pol lookup_labels  ppc with
1833        [ short_jump ⇒ 〈2, 2〉
1834        | absolute_jump ⇒ ?
1835        | long_jump ⇒ 〈4, 4〉
1836        ] *)
1837      | CJNE arg lbl ⇒ ? (*
1838        match pol lookup_labels ppc with
1839        [ short_jump ⇒ 〈2, 2〉
1840        | absolute_jump ⇒ ?
1841        | long_jump ⇒ 〈4, 4〉
1842        ] *)
1843      | DJNZ arg lbl ⇒ ? (*
1844        match pol lookup_labels ppc with
1845        [ short_jump ⇒ 〈2, 2〉
1846        | absolute_jump ⇒ ?
1847        | long_jump ⇒ 〈4, 4〉
1848        ] *)
1849      | ADD arg1 arg2 ⇒
1850        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1851         〈ticks, ticks〉
1852      | ADDC arg1 arg2 ⇒
1853        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1854         〈ticks, ticks〉
1855      | SUBB arg1 arg2 ⇒
1856        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1857         〈ticks, ticks〉
1858      | INC arg ⇒
1859        let ticks ≝ ticks_of_instruction (INC ? arg) in
1860         〈ticks, ticks〉
1861      | DEC arg ⇒
1862        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1863         〈ticks, ticks〉
1864      | MUL arg1 arg2 ⇒
1865        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1866         〈ticks, ticks〉
1867      | DIV arg1 arg2 ⇒
1868        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1869         〈ticks, ticks〉
1870      | DA arg ⇒
1871        let ticks ≝ ticks_of_instruction (DA ? arg) in
1872         〈ticks, ticks〉
1873      | ANL arg ⇒
1874        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1875         〈ticks, ticks〉
1876      | ORL arg ⇒
1877        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1878         〈ticks, ticks〉
1879      | XRL arg ⇒
1880        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1881         〈ticks, ticks〉
1882      | CLR arg ⇒
1883        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1884         〈ticks, ticks〉
1885      | CPL arg ⇒
1886        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1887         〈ticks, ticks〉
1888      | RL arg ⇒
1889        let ticks ≝ ticks_of_instruction (RL ? arg) in
1890         〈ticks, ticks〉
1891      | RLC arg ⇒
1892        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1893         〈ticks, ticks〉
1894      | RR arg ⇒
1895        let ticks ≝ ticks_of_instruction (RR ? arg) in
1896         〈ticks, ticks〉
1897      | RRC arg ⇒
1898        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1899         〈ticks, ticks〉
1900      | SWAP arg ⇒
1901        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1902         〈ticks, ticks〉
1903      | MOV arg ⇒
1904        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1905         〈ticks, ticks〉
1906      | MOVX arg ⇒
1907        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1908         〈ticks, ticks〉
1909      | SETB arg ⇒
1910        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1911         〈ticks, ticks〉
1912      | PUSH arg ⇒
1913        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1914         〈ticks, ticks〉
1915      | POP arg ⇒
1916        let ticks ≝ ticks_of_instruction (POP ? arg) in
1917         〈ticks, ticks〉
1918      | XCH arg1 arg2 ⇒
1919        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1920         〈ticks, ticks〉
1921      | XCHD arg1 arg2 ⇒
1922        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1923         〈ticks, ticks〉
1924      | RET ⇒
1925        let ticks ≝ ticks_of_instruction (RET ?) in
1926         〈ticks, ticks〉
1927      | RETI ⇒
1928        let ticks ≝ ticks_of_instruction (RETI ?) in
1929         〈ticks, ticks〉
1930      | NOP ⇒
1931        let ticks ≝ ticks_of_instruction (NOP ?) in
1932         〈ticks, ticks〉
1933      ]
1934    | Comment comment ⇒ 〈0, 0〉
1935    | Cost cost ⇒ 〈0, 0〉
1936    | Jmp jmp ⇒ 〈2, 2〉
1937    | Call call ⇒ 〈2, 2〉
1938    | Mov dptr tgt ⇒ 〈2, 2〉
1939    ].
1940    cases daemon
1941qed.
1942
1943definition ticks_of:
1944    ∀p:pseudo_assembly_program.
1945      (Word → Word) → (Word → bool) → ∀ppc:Word.
1946       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1947  λprogram: pseudo_assembly_program.
1948  λsigma.
1949  λpolicy.
1950  λppc: Word. λppc_ok.
1951    let pseudo ≝ \snd program in
1952    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1953     ticks_of0 program sigma policy ppc fetched.
1954
1955lemma eq_rect_Type1_r:
1956  ∀A: Type[1].
1957  ∀a: A.
1958  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1959  #A #a #P #H #x #p
1960  generalize in match H;
1961  generalize in match P;
1962  cases p //
1963qed.
1964
1965axiom vsplit_append:
1966  ∀A: Type[0].
1967  ∀m, n: nat.
1968  ∀v, v': Vector A m.
1969  ∀q, q': Vector A n.
1970    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
1971      v = v' ∧ q = q'.
1972
1973lemma vsplit_vector_singleton:
1974  ∀A: Type[0].
1975  ∀n: nat.
1976  ∀v: Vector A (S n).
1977  ∀rest: Vector A n.
1978  ∀s: Vector A 1.
1979    v = s @@ rest →
1980    ((get_index_v A ? v 0 ?) ::: rest) = v.
1981  [1:
1982    #A #n #v cases daemon (* XXX: !!! *)
1983  |2:
1984    @le_S_S @le_O_n
1985  ]
1986qed.
1987
1988example sub_minus_one_seven_eight:
1989  ∀v: BitVector 7.
1990  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1991  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1992 cases daemon.
1993qed.
1994
1995(*
1996lemma blah:
1997  ∀m: internal_pseudo_address_map.
1998  ∀s: PseudoStatus.
1999  ∀arg: Byte.
2000  ∀b: bool.
2001    addressing_mode_ok m s (DIRECT arg) = true →
2002      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2003      get_arg_8 ? s b (DIRECT arg).
2004  [2, 3: normalize % ]
2005  #m #s #arg #b #hyp
2006  whd in ⊢ (??%%)
2007  @vsplit_elim''
2008  #nu' #nl' #arg_nu_nl_eq
2009  normalize nodelta
2010  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2011  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2012  #get_index_v_eq
2013  normalize nodelta
2014  [2:
2015    normalize nodelta
2016    @vsplit_elim''
2017    #bit_one' #three_bits' #bit_one_three_bit_eq
2018    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2019    normalize nodelta
2020    generalize in match (refl ? (sub_7_with_carry ? ? ?))
2021    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2022    #Saddr #carr' #Saddr_carr_eq
2023    normalize nodelta
2024    #carr_hyp'
2025    @carr_hyp'
2026    [1:
2027    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2028        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2029        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2030        #member_eq
2031        normalize nodelta
2032        [2: #destr destruct(destr)
2033        |1: -carr_hyp';
2034            >arg_nu_nl_eq
2035            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2036            [1: >get_index_v_eq in ⊢ (??%? → ?)
2037            |2: @le_S @le_S @le_S @le_n
2038            ]
2039            cases (member (BitVector 8) ? (\fst ?) ?)
2040            [1: #destr normalize in destr; destruct(destr)
2041            |2:
2042            ]
2043        ]
2044    |3: >get_index_v_eq in ⊢ (??%?)
2045        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2046        >(vsplit_vector_singleton … bit_one_three_bit_eq)
2047        <arg_nu_nl_eq
2048        whd in hyp:(??%?)
2049        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2050        normalize nodelta [*: #ignore @sym_eq ]
2051    ]
2052  |
2053  ].
2054*)
2055(*
2056map_address0 ... (DIRECT arg) = Some .. →
2057  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2058  get_arg_8 (internal_ram ...) (DIRECT arg)
2059
2060((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
2061                     then Some internal_pseudo_address_map M 
2062                     else None internal_pseudo_address_map )
2063                    =Some internal_pseudo_address_map M')
2064
2065axiom low_internal_ram_write_at_stack_pointer:
2066 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
2067 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2068  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
2069  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
2070  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2071  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
2072  bu@@bl = sigma (pbu@@pbl) →
2073   low_internal_ram T1 cm1
2074     (write_at_stack_pointer …
2075       (set_8051_sfr …
2076         (write_at_stack_pointer …
2077           (set_8051_sfr …
2078             (set_low_internal_ram … s1
2079               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
2080             SFR_SP sp1)
2081          bl)
2082        SFR_SP sp2)
2083      bu)
2084   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
2085      (low_internal_ram …
2086       (write_at_stack_pointer …
2087         (set_8051_sfr …
2088           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
2089          SFR_SP sp2)
2090        pbu)).
2091
2092lemma high_internal_ram_write_at_stack_pointer:
2093 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
2094 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2095  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
2096  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
2097  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2098  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
2099  bu@@bl = sigma (pbu@@pbl) →
2100   high_internal_ram T1 cm1
2101     (write_at_stack_pointer …
2102       (set_8051_sfr …
2103         (write_at_stack_pointer …
2104           (set_8051_sfr …
2105             (set_high_internal_ram … s1
2106               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
2107             SFR_SP sp1)
2108          bl)
2109        SFR_SP sp2)
2110      bu)
2111   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2112      (high_internal_ram …
2113       (write_at_stack_pointer …
2114         (set_8051_sfr …
2115           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
2116          SFR_SP sp2)
2117        pbu)).
2118  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
2119  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
2120  cases daemon (* XXX: !!! *)
2121qed.
2122*)
2123
2124lemma Some_Some_elim:
2125 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
2126 #T #x #y #P #H #K @H @option_destruct_Some //
2127qed.
2128
2129lemma pair_destruct_right:
2130  ∀A: Type[0].
2131  ∀B: Type[0].
2132  ∀a, c: A.
2133  ∀b, d: B.
2134    〈a, b〉 = 〈c, d〉 → b = d.
2135  #A #B #a #b #c #d //
2136qed.
2137   
2138(*CSC: ???*)
2139(* XXX: we need a precondition here stating that the PPC is within the
2140        bounds of the instruction list in order for Jaap's specification to
2141        apply.
2142*)
2143lemma snd_assembly_1_pseudoinstruction_ok:
2144  ∀program: pseudo_assembly_program.
2145  ∀program_length_proof: |\snd program| ≤ 2^16.
2146  ∀sigma: Word → Word.
2147  ∀policy: Word → bool.
2148  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
2149  ∀ppc: Word.
2150  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
2151  ∀pi.
2152  ∀lookup_labels.
2153  ∀lookup_datalabels.
2154    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
2155    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
2156    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
2157    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
2158      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
2159  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
2160  #lookup_labels #lookup_datalabels
2161  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
2162  normalize nodelta
2163  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
2164  #fetch_pseudo_refl
2165  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
2166  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
2167  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
2168  @pair_elim #preamble #instr_list #program_refl
2169  @pair_elim #labels #costs' #create_label_cost_map_refl
2170  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
2171  lapply (H ppc ppc_in_bounds) -H
2172  @pair_elim #pi' #newppc #fetch_pseudo_refl'
2173  @pair_elim #len #assembled #assembly1_refl #H
2174  cases H
2175  #encoding_check_assm #sigma_newppc_refl
2176  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
2177  >pi_refl' in assembly1_refl; #assembly1_refl
2178  >lookup_labels_refl >lookup_datalabels_refl
2179  >program_refl normalize nodelta
2180  >assembly1_refl
2181  <sigma_newppc_refl
2182  generalize in match fetch_pseudo_refl';
2183  whd in match (fetch_pseudo_instruction ???);
2184  @pair_elim #lbl #instr #nth_refl normalize nodelta
2185  #G cases (pair_destruct_right ?????? G) %
2186qed.
2187
2188lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
2189  /2/
2190qed.
2191
2192(* To be moved in ProofStatus *)
2193lemma program_counter_set_program_counter:
2194  ∀T.
2195  ∀cm.
2196  ∀s.
2197  ∀x.
2198    program_counter T cm (set_program_counter T cm s x) = x.
2199  //
2200qed.
2201
2202(* XXX: easy but tedious *)
2203lemma assembly1_lt_128:
2204  ∀i: instruction.
2205    |(assembly1 i)| < 128.
2206  #i cases i
2207  try (#assm1 #assm2) try #assm1
2208  [8:
2209    cases assm1
2210    try (#assm1 #assm2) try #assm1
2211    whd in match assembly1; normalize nodelta
2212    whd in match assembly_preinstruction; normalize nodelta
2213    try @(subaddressing_mode_elim … assm2)
2214    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
2215    [32:
2216      cases assm1 -assm1 #assm1 normalize nodelta
2217      cases assm1 #addr1 #addr2 normalize nodelta
2218      [1:
2219        @(subaddressing_mode_elim … addr2)
2220      |2:
2221        @(subaddressing_mode_elim … addr1)
2222      ]
2223      #w
2224    |35,36,37:
2225      cases assm1 -assm1 #assm1 normalize nodelta
2226      [1,3:
2227        cases assm1 -assm1 #assm1 normalize nodelta
2228      ]
2229      cases assm1 #addr1 #addr2 normalize nodelta
2230      @(subaddressing_mode_elim … addr2) try #w
2231    |49:
2232      cases assm1 -assm1 #assm1 normalize nodelta
2233      [1:
2234        cases assm1 -assm1 #assm1 normalize nodelta
2235        [1:
2236          cases assm1 -assm1 #assm1 normalize nodelta
2237          [1:
2238            cases assm1 -assm1 #assm1 normalize nodelta
2239            [1:
2240              cases assm1 -assm1 #assm1 normalize nodelta
2241            ]
2242          ]
2243        ]
2244      ]
2245      cases assm1 #addr1 #addr2 normalize nodelta
2246      [1,3,4,5:
2247        @(subaddressing_mode_elim … addr2) try #w
2248      |*:
2249        @(subaddressing_mode_elim … addr1) try #w
2250        normalize nodelta
2251        [1,2:
2252          @(subaddressing_mode_elim … addr2) try #w
2253        ]
2254      ]
2255    |50:
2256      cases assm1 -assm1 #assm1 normalize nodelta
2257      cases assm1 #addr1 #addr2 normalize nodelta
2258      [1:
2259        @(subaddressing_mode_elim … addr2) try #w
2260      |2:
2261        @(subaddressing_mode_elim … addr1) try #w
2262      ]
2263    ]
2264    normalize repeat @le_S_S @le_O_n
2265  ]
2266  whd in match assembly1; normalize nodelta
2267  [6:
2268    normalize repeat @le_S_S @le_O_n
2269  |7:
2270    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
2271  |*:
2272    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
2273  ]
2274qed.
Note: See TracBrowser for help on using the repository browser.